Skip to content

zkdsl compiler: remove the possibility for a range loop to mutate variables defined in external scope. Use manual buffers instead.#241

Merged
TomWambsgans merged 2 commits into
mainfrom
zkdsl-remove-loop-external-mutability
Jun 1, 2026
Merged

zkdsl compiler: remove the possibility for a range loop to mutate variables defined in external scope. Use manual buffers instead.#241
TomWambsgans merged 2 commits into
mainfrom
zkdsl-remove-loop-external-mutability

Conversation

@TomWambsgans
Copy link
Copy Markdown
Collaborator

@TomWambsgans TomWambsgans commented Jun 1, 2026

Before:

total: Mut = 0
for i in range(0, 11):
    total += i 
assert total == 55

After:

total_buf = Array(11) 
total_buf[0] = 0
for i in range(0, 11):
    v: Mut = total_buf[i]
    v += i
    total_buf[i + 1] = v
total = total_buf[10]
assert total == 55

…ariables defined in external scope. Use manual buffers instead.
@TomWambsgans TomWambsgans merged commit 07b3a3b into main Jun 1, 2026
2 of 3 checks passed
@TomWambsgans TomWambsgans deleted the zkdsl-remove-loop-external-mutability branch June 1, 2026 20:04
TomWambsgans added a commit that referenced this pull request Jun 1, 2026
…ariables defined in external scope. Use manual buffers instead. (#241)

* zkdsl compiler: remove the possibility for a `range` loop to mutate variables defined in external scope. Use manual buffers instead.

* make tests pass

---------

Co-authored-by: Tom Wambsgans <TomWambsgans@users.noreply.github.com>
TomWambsgans added a commit that referenced this pull request Jun 1, 2026
…241)

`range`/`parallel_range` loops may no longer reassign an enclosing-scope mutable;
accumulation must go through an explicit array buffer. Rewrite the affected
gadgets and handwritten faithfulness tests to the array-chain idiom (acc[i+1] =
acc[i] + x[i]), keeping their honest/violating models identical:

- Loop gadget: single range-loop array-chain accumulator
- NestedMutLoop gadget: two array chains across the nested loop (flat index),
  now exercising cross-iteration array data-dependencies instead of carried muts
- handwritten cases 6,11,15,17,24,25,27,29,30: range-loop mutable accumulators
  rewritten to array chains (unroll-carried mutables remain allowed and unchanged)

Validated by hard_kinds_isolate + the full compiler_fuzzer suite (40/40).

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant