vm: reorg instruction execution - #21
Merged
Merged
Conversation
TomWambsgans
added a commit
that referenced
this pull request
Sep 3, 2026
* zkDSL compiler: test that one source compiles to one program
The bytecode digest leads the Fiat-Shamir transcript, so two builds of one
source that disagree are two incompatible proof systems, and the symptom is a
proof that stops verifying rather than a crash. The compiler walks several
HashMaps whose iteration order is seeded per map instance; a single
sort_unstable in lower::scoped is what keeps that order out of the bytecode,
and nothing tested it. unified_guest also compiles repeatedly to find a fixed
point on its own log size, so a seed-dependent compiler could fail to converge
rather than merely produce a wrong transcript.
Two properties, both needed. Within a process, RandomState bumps its seed once
per map, so compiling twice hashes with different keys and is a real
perturbation (checked: two HashMaps built from the same keys in one process
iterate in different orders). Across processes, the checked-in digests were
produced under a different global seed, so matching them today is the check.
The fifteen programs in tests/programs pin digests; the guest gets the
reproducibility check without a digest, since it changes often and a golden
would be a chore rather than a signal.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL reference: drop a stale limitation and tidy one line
The "Not (yet) supported" list named runtime range-check bounds, which the
Assertions section two hundred lines above documents in detail and which
lower_assert_lt has implemented since LtBound::Runtime existed. The suite pins
it: range_check_runtime_bound and range_check_runtime_bound_at_bound_rejected.
A reference that contradicts itself is worse than one that says less.
The runtime-bound paragraph also ended in "WIthout this check => unsound",
which is a note to self rather than a sentence.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL compiler: stop reading syntax out of string literals
Two passes scanned the middle of a string literal for structure. Comments were
stripped with raw.split('#'), so a `#` in a hint stream name truncated the line,
and the shortened line usually still parsed into a different program. Bracket
depth was counted with no notion of a string, and depth0 feeds every top-level
splitter, so a `,` or a `]` inside a name moved an argument boundary: the call
hint_witness(b, "x,y") split into three arguments.
Both now treat a string as one opaque token. depth0 is the single fix for all
six splitters (arguments, additive, multiplicative, `**`, augmented assignment,
comparisons), since they all read it.
No existing program's bytecode moves: the fifteen digests are unchanged, and
nothing in the tree or the guest had a `,`, `#` or `]` inside a name. The test
uses all three at once and fails on the previous parser.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL compiler: decide index and branch by what a name means
A name can carry several readings at once. Binding `K = 3 + 1` records the
integer 4 and the field element 3 XOR 1 = 2, because index arithmetic is
integer arithmetic while a value expression folds in the field. Two places
read the integer and then acted as though it were the value.
array_ptr folded a product's constant factor through try_gpow_index, which
matched Expr::Var against the integer reading and took that integer's bit
position as a g exponent. So K was g^1 as a value and g^2 as an index, in the
same function. The old rule also silently read the wrong cell whenever the two
happened to differ: `K = 6 + 2` folded to g^3 while its value is g^2, and the
proof still verified.
lower_if folded a compile-time condition on the integer reading while the
runtime lowering tests a field XOR, so `if K == 4` entered the then arm. The
sharper form, `if K == 4: assert K == 4`, compiled clean and then died at
witness generation inside a branch whose own condition is false.
Neither is fixed by picking a reading. Both now act only where the readings
AGREE: const_gpow folds an address the compiler already tracks, or an integer
2^j whose field value really is g^j, so folding decides nothing; lower_if
declines the fold when the field contradicts the integer verdict and lets the
runtime test decide. Both recover cases the old code got wrong AND cases it
declined: `K = GEN ** 3` never folded as an index before, and `K = 2 ** 3`,
`16 // 2`, `12 - 4` and `len(TBL)` all fold again.
lower_if deliberately does not widen to every condition the field can decide.
Which branches fold is observable, since a folded arm is straight-line code
whose bindings persist while a runtime arm's are branch-local: widening it
rescopes tests/programs/scoping.py, which exists to pin exactly that, and the
guest relies on the same thing. That needs a distinct compile-time `if` first.
The heap-index rejection also claimed 4 was "not a g-power", which is false: 4
is g^2, and the reason to reject `hb[4]` is that the slice `hb[4:5]` reads the
same number as cell 4. It now says which of the two it is and what to write.
The fifteen bytecode digests are unchanged and the guest is still 328,716
instructions, so no program that compiled before compiles differently.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL compiler: one entry per name instead of five parallel maps
Scope kept vars, stacks, consts, gaddrs and fconsts side by side, all keyed by
the same name. Binding a name meant removing it from four maps and inserting
into one, so the invariant "a name has one meaning" was held up by every caller
remembering to clear the others. rebind cleared four of the five and each of
the six Let arms cleared consts itself.
They collapse into one map to one entry: the value binding, plus the optional
compile-time integer reading of the same expression. The integer really does
coexist with the value (`x = 2` names the field element 2 and the index 2),
which is why it is a field beside the binding rather than a fifth variant, and
why five maps was the wrong shape rather than merely a verbose one. A rebind is
now a single insert, and nothing can be left behind.
Two lookups get shorter rather than just moved: gaddr_of and try_field_const
each chained an or_else across two maps and are now one match on the entry.
One behaviour change, in the direction the code already documented. The integer
reading is attached after the value binding is made, because a rebind clears it
and the note at that arm says the RHS still has to see the name's old binding.
`x = 2` followed by `x = sa[x]` was rejected with "a StackBuf index must be a
compile-time integer", which was false: x was one, and consts.remove had run
before the RHS was lowered. It compiles now.
The fifteen bytecode digests are unchanged and the guest is still 328,716
instructions.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL compiler: revert the branch fold change, reject two more inputs
The branch fold fix in 4529d27b was wrong twice over and is reverted.
It was incomplete. The agreement check consults the field reading only when
both sides have one, and try_field_const has no arm for `-`, `//` or `%`, so
`if K == 8 // 2` with `K = 3 + 1` still folded into the arm. Every compile-time
`if` in the guest is written with `//` or `%`, so the guest was folding through
exactly the path the check could not see.
It was also harmful. Declining a fold changes meaning as surely as adding one,
which the commit argued about widening and failed to check about narrowing.
`if 1 + 1 == 2` folded to the then arm before and became a runtime branch that
takes the else arm, because `+` is XOR in a value expression. The same flip hits
`if i + 1 == n` in an unroll, which moves which iteration runs the arm, and
where the arm binds a name the program stops compiling, a runtime arm's
bindings being branch-local. No digest caught this: no condition in the tree
reaches the check.
Neither reading can win here. Deciding in the field breaks the unroll idiom and
cannot see integer-only operators; deciding in the integer keeps the original
bug. The trap is now written out where the fold happens, for the kind system to
fix by making the author say which arithmetic a condition means.
Two inputs that were accepted and should not be:
A repeated parameter name (`def f(a, a)`) bound twice. Before the scope
collapse the two bindings landed in different maps, so `a` was a StackBuf and a
scalar at once inside an @inline body; after it, last-wins. Neither is a
meaning worth having.
A placeholder value containing `"` reshapes the line exactly as `#` does now
that a string literal is one opaque token, so it joins the same guard.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL compiler: say which operator is missing an operand
`-3 + 5`, `1 +`, `* 2` and `4 //` all reported "cannot parse expression ``".
The top-level split hands the empty side to the expression parser, which has
nothing left to name. The split knows, so it says: which operator, which side,
and for a leading `-` that the language has no unary minus and field
subtraction is `+`.
Checked while deciding whether to replace the expression parser with a Pratt
parser, which the design note proposed. Not doing that: the tree shapes show
`**` right-associative, `-`, `//` and `%` left-associative, and `**` binding
tighter than `*` binding tighter than `+`, all correct, so the rewrite would
fix no bug. The reported left-associative `**` was a misreading.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL compiler: let a global constant be a g-power
The scalar path tried an f192 literal, then an integer expression, and stopped.
So `STEP = GEN ** 2` was rejected as "not a compile-time integer constant
expression" while `STEP = f192(4, 0, 0)`, naming the same element, was fine.
Every address and index in this ISA is a g-power, so that is the spelling an
author reaches for first.
It now falls back to the field evaluator, and renders the value as a decimal
wherever it fits the low two limbs. Rendering the decimal rather than an f192
literal keeps the constant usable in the positions that demand a literal (a
buffer size, a `**` exponent, a range-check bound) instead of only as a value,
and a literal's integer and field readings are the same bit pattern, so this
adds no new ambiguity of the kind `STEP = 3 + 1` already has.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL reference: warn that the integer/field trap follows a name
The reference explains that constant `+` is integer addition in an index and
XOR in a value, but not that a name crossing a boundary has the reading chosen
for it. A global constant and a Const argument are evaluated as integers and
substituted, and a compile-time `if` folds on the integer reading while the
runtime test compares field values. An author cannot infer any of that from the
rule as stated, and the guest already carries a six-line comment working around
one instance.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL: correct what the two arithmetic regimes are, and which one is a bug
The reference said a global constant is "evaluated to its field value". It is
not: it is evaluated as a compile-time integer expression, which is the whole
point, since that is what makes `N_TWEAK_WORDS = 2 + CHAIN_STEPS * V +
LOG_LIFETIME` come out right. The test pinning that derivation is the real XMSS
instance, so the behaviour is load-bearing and the sentence was simply wrong.
That also corrects this plan, which listed global constants and Const arguments
as instances of the read-an-integer-as-a-value bug. They are not. They are the
integer regime, deliberately, and a name crossing between the regimes is a wart
for the kind system to name rather than a miscompile. Tried rejecting a constant
whose two readings diverge, which is what that framing implies, and it rejects
the XMSS derivation on the first try.
One site does contradict itself and stands: the compile-time `if` folds on the
integer reading while the runtime test of the same condition compares field
values. Every available fix was tried and each breaks working programs, so it
needs the language change, not a compiler patch.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL compiler: one cache for every lazily-SET constant cell
Scope kept four caches for the same thing: const_cells keyed by field value,
plus a dedicated field for `1`, a dedicated field for `0`, and a map keyed by
range-check bound `k` holding `g^{k-1}`. Each is a constant SET into a frame
cell once per control-flow scope and reverted at a join, so each new one was a
field someone had to remember to add to `scoped`.
They are now one map. `one` and `zero` are `const_cell` calls, and `bound_cell`
is `const_cell(g^{k-1})`.
The separate caches were not only redundant, they lost sharing: nothing routed
`const_cell(F192::ZERO)` to `zero()`, so a program could hold two frame cells
both containing zero, and a range-check bound never shared with an equal
constant. Every program that changed got smaller (identities 12 to 10
instructions, runtime_loop 66 to 65, wots_walk 115 to 114), and the guest went
from 328,716 instructions and 577,539 cycles to 328,553 and 576,807. Cycles are
committed, so that is the part that costs. Three golden digests move, in that
direction.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL compiler: derive the frame's ABI prefix in one place
Eight sites computed offsets into the frame's fixed prefix by hand, and
`2 + n_args + n_ret_cells` appeared verbatim twice in lower_func, once as the
first local cell and once as the value handed to the assembler. A wrong offset
there reads a cell that exists, so nothing catches it.
An `Abi` type now names the two return slots and derives an argument, a return
cell and the end of the prefix. A caller writing into a callee's frame and the
callee reading its own go through the same three functions.
The escape state was two fields, `stack_runs` and `frame_escaped`, kept
consistent by whoever touched them: once a frame address escapes, every run is
sealed and the vector is drained, so "escaped with runs still unsealed" was
representable but wrong. One `Option` field says it instead, with `None` as the
escaped state.
Both are pure refactors: no digest moves and the guest is unchanged.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL compiler: separate compile-time evaluation from lowering
lower.rs was 3,123 lines with no internal boundary. The clearest one available
is already latent in the code: twelve methods answer "what is this expression
worth before anything runs", and every one of them takes &self and emits
nothing. That is what lets a caller ask the question without paying for the
answer, and it is why an index that folds costs no instruction.
They move to lower/eval.rs, where the module doc states the rule and &self makes
it structural: a function there cannot emit, because emitting needs &mut self.
lower.rs drops to 2,884 lines.
The module doc also states the thing the split makes visible: there are two
answers, not one, and the position of a use decides which is wanted.
try_const_int reads an expression as an integer, which is what a size, an index,
a bound and an exponent want; try_field_const reads the same expression as a
field element, where `+` is XOR, which is what a value wants. They disagree on
any sum of overlapping integers, and the language cannot yet say which was
meant.
A pure move: no digest changes, the guest is unchanged.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL: add `if const(...)`, and reject a branch whose two readings disagree
The compile-time fold decides on the integer reading of a condition while the
runtime test of the same condition compares field values, so the two contradict
each other whenever a side's readings do. `3 + 1` is the integer 4 and the field
element `3 XOR 1` = 2, so `if 3 + 1 == 4` folded into an arm whose own condition
is false as a value, and `if K == 4: assert K == 4` compiled clean and then died
at witness generation.
Neither reading can be made to win, which two earlier attempts established.
Deciding in the field flips `if 1 + 1 == 2` and moves which iteration of an
unroll runs an `if i + 1 == n` body, and cannot read `-`, `//` or `%` at all,
which is what most compile-time conditions are written with. Declining to fold
rescopes programs, a folded arm's bindings escaping where a runtime arm's do
not. Rejecting every divergence outright rejects those same idioms with no way
to say what was meant.
So the author says it. `if const(a == b):` asks for the branch to be decided
while compiling: the condition must be decidable then, and it is read with
integer arithmetic. An undeclared condition whose readings disagree is now an
error naming both readings and pointing at the wrapper. One whose readings agree
folds exactly as before, which is every such condition in the tree and in the
guest: 336 tests pass, no digest moves, and the guest is unchanged at 328,553
instructions.
The wrapper is also how a program states that a branch's bindings are meant to
outlive it, since only a folded arm's do.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL compiler: say why a for loop cannot carry a value
A `for` body that assigns to an enclosing name reads it before it binds it, and
the capture set drops every name the body binds, so the read reached lowering
with nothing behind it and reported "unbound variable `s`". That is the
loop-carry limitation rather than a typo: the tail-recursive helper threads its
captures in and never out, so an accumulator cannot come back.
The StackBuf form of the same limitation already says so, with a comment
explaining that it exists to avoid "the misleading unbound variable the capture
drop would otherwise trigger". The scalar form is the more common one and said
nothing. It now names the limitation and the two ways round it. A genuine
unbound variable outside a loop is unchanged.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL compiler: say what the merged constant cell can alias
Two gaps an adversarial review of the cache merge found, neither a bug.
The merge deleted the `one_off` field, and with it the comment explaining that
the cache reverts at a branch join and that hoisting `one()` above a branch is
therefore an optimization rather than the thing holding the invariant up. That
rationale now sits on `const_cell`, along with the reason the sharing is safe at
all: the `SET` is emitted where the cell is allocated, always before anything
can name it, so every later write is a write-once equality against a bytecode
constant.
`bound_cell` is now an ordinary `const_cell`, so a range check's product target
is shared with any plain use of the same constant. The sharpest case is `k = 1`,
which is legal: its target is `g^0 = 1`, so the cell is the one `one()` hands
out, and in `main` that is also `self_fp`. Nothing said so.
The cycle figures quoted for this change were measured with
`--xmss-per-leaf 4`, which is not one of the documented benchmarks, so they
could not be reproduced from AGENTS.md. The numbers here are for the
benchmarks that are documented.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL compiler: correct which recursion tests are ignored
aggregate_two_to_one is not #[ignore]d; it runs in the default suite, and
AGENTS.md calls it the fast end-to-end check. The fourth ignored test is
aggregate_three_levels, which this plan omitted, so a session following it would
have skipped the deepest recursion case. It passes.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL compiler: work out the loop-carry mechanism, and what blocks it
A carried value is a helper parameter that is also returned; the two exit paths
write the return cells exactly once between them, because a tail call inherits
the frame's retpc and retfp, so either the deepest iteration returns straight to
the original caller or this frame's Return runs, never both.
The blocker is that lower_func only sets tail_call when n_ret == 0 and the next
statement is an empty Return, so a helper that returns anything builds one frame
per iteration. Widening that test is the first and most delicate step, since it
is what keeps a mul_range loop from growing an unwind chain.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL compiler: check a branch condition per side, not by comparing verdicts
The check added with `if const(...)` had the hole its own commit message
described. It compared the two sides' verdicts, which needs a field reading for
BOTH sides, and try_field_const has no arm for `-`, `//` or `%`. So one missing
reading disabled the guard entirely: `n == 2` was rejected while `n == 3 - 1`,
the same condition, folded on the integer reading and produced a verifying proof
of the arm the value reading says is not taken. `if n == 3 - 1: assert n == 2`
compiled clean and died at witness generation, which is the exact failure the
feature was added to stop.
Checked per side now, and that is not merely a patch but the simpler rule: if
each side's own two readings agree then integer equality and field equality say
the same thing, so a side that disagrees with itself is the whole of the
ambiguity and no cross-check is needed. It also cannot be disabled by how the
other side is written.
`if const(...)` gains a field fallback, so it decides a condition only the field
can read (`GEN ** 3 == GEN ** 3`, or anything past u32), which it previously
rejected as "not a compile-time decision" although it plainly is. A plain `if`
must not fold those: it lowers them to a runtime branch today, and folding would
let the arm's bindings escape.
The loop capture analysis asked "does this branch fold?" with a syntactic
`Lit == Lit` test. `force_const` is that predicate exactly, so it now says so;
the mismatch was latent but its own comment records the bug it caused before.
Found by adversarial review, along with the two documentation sentences that
stated the pre-fix rule.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL compiler: name the function a diagnostic came from
The line alone is not the site when the function being lowered is one the author
never wrote. A rejection inside a Const monomorph reported a line in the
template with nothing saying which instantiation reached it, so changing a call
site produced an error pointing at code that had not changed. Diagnostics now
name the function unless it is main, which makes that read "line 2 in
last__L3_L4", the specialization's own constants identifying the call. An
@inline body is lowered through the caller and so reports the caller's line;
where there is an inline chain it is appended.
Near misses of `if const(...)` also say the word. `const (a == b)` with a space,
`const(a) == const(b)` and an unbalanced `const(a == b` were all correctly
rejected, but by the generic "an `if` condition must be `a == b` or `a != b`",
which never hints at what was meant. A name that merely begins with `const` is
not a near miss and still compiles as the ordinary comparison it is.
Both found by adversarial review.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL compiler: finish five diagnostics that were bare
A sweep of every message the lowerer can emit. Five said too little: an empty
runtime slice reported "empty slice" with no bounds, three arity errors were a
bare signature with no verb, and an unknown blake2s keyword named neither the
keyword nor the ones that exist. The rest read well and are left alone.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL compiler: close three ways to read a cell the program does not own
Each compiled clean and left a cell nothing writes, which the prover then
chooses, so an assert reading it proved nothing. Each is one omission in a place
that already had a checked counterpart.
copy_alias did not bounds-check its stack index, and it is on the store path, so
`c[0] = a[2]` on a StackBuf(2) aliased the next buffer's first cell and
`assert c[0] == GEN ** 7` PASSED, while a further index named a cell nothing
writes. The identical read in expression position was rejected, so one program
had two meanings depending on which side of an assignment it was written. List
literal elements take the same path.
lower_call never compared a call's argument count against the callee's
parameters. `check(0)` into `def check(a, b)` compiled, and `b` was
prover-chosen, so `assert a == b` was vacuous. Beyond that, caller and callee
place the return area from their own idea of the argument count, so a missing
argument makes the caller bind a callee parameter cell and a surplus one
overwrites the callee's first return slot. Only specialize checked this, and
only for a callee declaring Const parameters. The fused match_range dispatch had
the same hole, next to a return-arity check whose comment describes this exact
failure.
A runtime-start heap slice bounds-checked one cell rather than its length. A
start that folds, `GEN ** k` or a name bound to one, reaches that arm because it
is not an INTEGER even though its offset is known, so the span was never
checked: `hint_witness(hb[GEN ** 1:GEN ** 1 + 2], ...)` on a HeapBuf(2) wrote
into the next buffer, while `hb[1:3]`, the same run with integer bounds, was
rejected.
Found by an adversarial subagent hunting the areas no review had covered. It
also cleared cse.rs, the match dispatch, and the hint paths, which it fuzzed
with 14k generated programs against a value model.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL compiler: stop four names and calls picking a winner silently
A repeated `def` lowered both bodies and kept the last. A function whose name
contains `__` could take the place of one the compiler generates: a loop helper
is `__loopN` and a `Const` specialization of `f` is `f__L1`, so a user function
called `f__L1` was dispatched to instead of the specialization and the call ran
the wrong body. Both are now parse errors.
A call to something that will never be lowered died in the assembler indexing a
HashMap, as `no entry found for key`, with no line and no name the author would
recognise. Three ways in: a typo, a statement-only builtin used as a value
(`x = assert_in_k(a, b)`), and an `@inline` callee reached where inlining did
not happen. Caught at lowering now, where there is a line, and the message says
which of those it might be.
A compile-time field constant is capturable into a `for` body. It was dropped
from the capture set, so `c = 5` followed by a loop reading `c` failed as
"unbound variable", which named neither the cause nor a fix; worse since that
message now offers loop-carry advice that does not apply. The body becomes its
own function, so the constant is genuinely not in scope there, and the helper
takes it as a parameter the call site materializes with one SET.
All four found by the same adversarial hunt as the three soundness fixes.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL compiler: split lowering by the question each part answers
lower.rs was 3,124 lines at the start of this work and had no internal boundary.
It is now 1,824, with three more modules beside the eval one split out earlier.
Pure moves: no digest changes and the guest is unchanged.
The split is by invariant, not by size, because each of the four has one worth
stating once instead of rediscovering. eval asks what an expression is worth
before anything runs, and every function in it takes &self and emits nothing.
mem asks which cell a name means and what writing to it costs: every index is
bounds-checked in every position, and a deferred store is a value fact rather
than an instruction. call is the boundary where caller and callee must agree on
the arity, since they place the return area from their own idea of it.
builtins is the precompile and the hints, the two places a value arrives without
an instruction computing it.
Three of those sentences are the bugs found this week, written where the next
person will read them: the unchecked store index, the missing arity check, and
the hint destination that has to be materialised first.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL compiler: split the parser the same way
parser.rs was 1,581 lines and is now 861, with three modules beside it. Pure
moves: no digest changes, the guest is unchanged.
Split by the question each answers, and each doc states the rule its part lives
by. expr reads structure out of a line under one rule, that a string literal is
one opaque token and every scan goes through depth0; it also records that the
precedence there is correct as it stands, since that was measured rather than
assumed. consts evaluates a constant at parse time, which five syntactic
positions demand before lowering runs, and reads it as an INTEGER deliberately,
which is what makes a derived size right. subst substitutes an expression for a
name through a statement tree, which is how unroll and Const bind their
variable, and notes that a field dropped from one of its arms is a construct
that loses its meaning only inside a specialisation.
The two files that held nearly all of this crate are now nine modules, none over
900 lines.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL compiler: bounds-check a bit hint's heap destination too
The fourth instance of the same shape, found reviewing the fix for the first
three: one omission beside a checked counterpart. bits_dest rejected a StackBuf
destination too small for nbits, and checked nothing at all for a HeapBuf, so
hint_decompose_bits{,_exponent} wrote its bits on into the next buffer while the
identical call with a StackBuf destination was rejected. The guest uses the
shifted-alias form of that destination, which is checked here too.
Two things the same review found in the fixes themselves. The "no function
named" message advertised a case it cannot reach, since an @inline callee is in
`defs` and so never reaches that arm; what it could not diagnose was an @inline
callee used as a match_range arm, where the fused dispatch enters one real
function and there is no entry pc to jump to. That now says so instead of dying
in the assembler indexing a HashMap. And inserting arity_of had put it between
return_shapes_of's doc comment and its signature, so one function carried three
paragraphs describing three others.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL: let a multi-cell value be passed, not only returned
A function could always RETURN a StackBuf, the ABI flattening it across as many
return cells as its size asks for, and could never take one: a real call wrote
exactly one cell per argument, so a two-cell digest went in through a HeapBuf
pointer or an @inline expansion while coming back out whole. Only @inline could
bind a run, because it does not cross a frame at all. That asymmetry was the
language's, not the machine's.
`def f(s: StackBuf(n))` closes it with the mechanism that already existed. The
argument area becomes a WIDTH rather than a count, `Abi::arg` places argument i
after the widths of the ones before it, and a run argument is copied cell by
cell into the callee's frame, which owns it thereafter. A `StackBuf` return has
worked exactly this way all along, so the two directions are now one rule and
one type: ReturnShape is renamed Shape, since it was always answering "how many
cells does this value take" rather than anything about returning.
The shape is checked at the call in both directions of mismatch, and the fused
match_range dispatch checks that its arms share one argument layout, since they
share one frame and differing widths would put the return area in two places.
Nothing existing changes: every parameter without an annotation is one cell, so
no digest moves and the guest is unchanged at 328,553 instructions.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL compiler: a store into a run parameter is the assertion, not a store
The multi-cell parameter shipped with a critical bug, and the comment I wrote
was the bug: "binds the run the caller wrote, exactly as a local StackBuf(n)
binds one it allocated". It is not like a local. A local's cells are unwritten
at binding time and may take a deferred store, which emits nothing; a
parameter's are already written by the caller, so a store into one is the
write-once equality assertion instead and must be emitted.
Without seeding those cells as written, every store into a run parameter
recorded an alias and vanished. So the idiom that pins an unconstrained hint,
which is how a program constrains prover-supplied data at all, pinned nothing: a
callee asserting `s[0] = GEN ** 5` against a hinted buffer accepted whatever the
prover hinted, and the proof verified. `s[0] = s[1]` on distinct values likewise
published a sum of zero with the implied equality never checked.
Three more from the same review. The fused match_range dispatch resolves
arguments one cell each, so a scalar passed where a run is declared filled 1 of
n cells and left the rest prover-chosen; that path now rejects a run parameter
outright, since it cannot pass one anyway. A Const specialization discarded the
retained parameters' shapes, so a declared StackBuf(n) beside a Const became one
scalar cell with no diagnostic. And return-shape inference seeded every
parameter as a scalar, so `return s` on a run parameter reported it used as a
scalar.
The reference said the callee "owns" the run from then on, which is the wrong
mental model and is what the code got wrong; it now says the cells arrive
already written and what follows from that.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL: bind one hinted value without a buffer to put it in
hint_witness fills a destination that already exists, so a single hinted scalar
cost three lines: a one-cell StackBuf, a slice of it, and a read back out. The
guest declares thirty StackBuf(1) buffers and twenty-eight exist for nothing
else, which is the measure of the wart rather than a guess at it.
`m = hint_witness("m")` binds one value. It is pure sugar and costs exactly what
it replaces: the same eleven cycles, since the buffer was never an instruction
either. The value is as unconstrained as any hint, so a program still has to pin
it, and each binding pops one stream entry whose length must be one.
Found by counting what the guest actually repeats rather than by reading the
design note, which did not mention it.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL compiler: give five reachable panics a source line
An audit of every bounds check turned up no more missing ones, but five sites
reachable from source still used a bare `expect`, so they panicked with no line
and no name: a `hint_f192_limbs` or `addr()` destination that is not a StackBuf,
a run named unsliced by something that is not one, a slice length past u32, and
a blake2s counter past u64. Each now reports the offending expression and where
it is.
The counter's pinned test message moves with it, and now names the value.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL compiler: make the scalar hint a drop-in, and stop it stealing a line
Four findings from reviewing it, none a soundness bug.
Three StmtKind walkers have a catch-all arm and each swallowed the new variant,
so the sugar was not a drop-in for the idiom it replaces. `stmt_inline_safe`
rejected an @inline body that IS a single tail return; `binds_anywhere` raised
the StackBuf-capture false positive it exists to suppress, for a `for` body that
merely shadows a name from inside an arm; and return-shape inference lost the
binding, so a function returning one reported it used as a scalar. All three
fail closed, so the cost was a diagnostic naming the wrong cause. subst.rs's own
doc says every arm has to be exhaustive over StmtKind; these three catch-alls
are where nothing enforces that.
The parser matched any right-hand side that STARTS with `hint_witness(` and ENDS
with `)`, because that is what call_args does. So `x = hint_witness("a") * f("b")`
parsed as a hint whose stream name was `a") * f("b`, and the rest of the line
vanished with no diagnostic, failing only at witness generation. That is the
"used to be a parse error, now means something else" class. The call now has to
span the whole right-hand side, and the four compound spellings are parse errors
again.
The loop test's own bound was wrong: `mul_range(1, 4)` is two iterations, not
three, so its third witness entry sat unread and would have masked an off-by-one
in that direction.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL guest: bind hinted scalars directly, 28 fewer lines
The guest declared thirty StackBuf(1) buffers and twenty-three existed only to
receive one hinted value: declare the buffer, hint into a slice of it, read the
cell back out. Those twenty-three are now one line each.
Proved behaviour-preserving rather than argued: the guest's compiled bytecode is
bit-for-bit identical, digest 2bafd703 before and after, so the sugar lowers to
exactly what the idiom did. The four adversarial recursion tests pass and the
program is unchanged at 328,553 instructions.
The snark_lib stub takes both forms, so the guest still parses and type-checks
as plain Python, which is what the editor tooling relies on.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL guest: spell a Merkle level `lvl`, as the rest of the file does
Two loops called it `l`, which reads as a `1` and which the guest's own
neighbouring code and comments already spell `lvl`. The comments explaining
those loops used `l` too, so they move with it.
The compiled bytecode is unchanged, digest 2bafd703, which is what a rename of a
loop variable should be.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL compiler: one rule for what an @inline body may contain
The guard disagreed with itself. stmt_inline_safe allowed three of the five
statement builtins, omitting both hint_decompose_bits forms, and rejected a real
user call; but body_inlinable never inspects expressions and never checks the
tail return at all, so the SAME call was accepted written as `y = f(x)`,
`return f(x)`, `b[i] = f(x)` or inside an assert. Stricter than needed in one
position, leakier than documented in the other.
Relaxed to match, because the permissive side is the correct one: lower_call
builds the callee's frame from fresh() and writes retfp and retpc with
DerefMode::Fp and Pc, none of which assumes whose frame is current, so nothing
about a real call needs the caller's frame. Proven rather than argued: a
statement-position call and a hint_decompose_bits_exponent inside an @inline
body each publish the right value and reject a wrong one.
The reference described `assert a != b` as a conditional jump over a poison path
at `GEN ** -1`, needing "no inverse hint". That mechanism is gone: it is XOR,
a hinted inverse, MUL and SET, with the write-once conflict as the assertion and
no JUMP at all, so there is no branch setup to amortize either. Measured at 3
instructions, which is the only part the old text had right.
Also notes why cse::write_counts scans the fill blocks and lands their scratch
writes on the function's own cells: it only forgoes an optimization, but it is
why compile and compile_without_filler can differ for one source, which cost a
reviewer a false positive.
An audit of @inline expansion, Const specialization, the assert gadgets and the
fill blocks found no soundness bug: 10,800 generated programs across six call
spellings, and 24 hint-pinning spellings each lied to at four cells, all
rejected correctly.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL compiler: a branch join says what it produced
The first piece of the middle IR, and the one that stands on its own.
A branch's join has to materialize every deferred store the branch made into a
cell that outlives it. It found those by cloning the alias map, diffing it
afterwards, and sorting the result, and the sort was load-bearing: without it
the order of the emitted copies came from HashMap iteration, so two builds of
one source could differ, and the bytecode digest leads the Fiat-Shamir
transcript. That sort was the only thing standing between this compiler and a
nondeterministic program, which is why M0's determinism test exists.
The join now records the cells it aliases as it aliases them, so it says what it
produced instead of reconstructing it. Same output, proven by the fifteen golden
digests and the guest at 328,553 instructions. An inner branch gets its own
journal, since it restores the alias map at its own join and nothing it aliased
survives to be produced by the outer one.
With that, no HashMap iteration reaches the bytecode at all. The two that remain
build error messages, and they are now ordered too: an unknown blake2s keyword
and the name a heap-bounds error blames, both of which could otherwise read
differently between builds of the same program.
This is the shape the rest of the IR needs. `alias` and `phys` cannot merge into
one slot state while the join is a diff, because the two have different
lifetimes and the join is where that shows.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL compiler: one slot per frame cell, replacing two side tables
The middle IR's slot state, corrected by what building it taught. The design
called `alias` and `phys` mutually exclusive and had them collapsing into one
enum. They are not exclusive: a cell aliased before a branch and stored into
inside it is materialized there, so it is written, and has its alias restored at
the join, so it is also aliased. Both at once, and soundly, because the copy
wrote the alias's own value.
So a slot holds TWO ORTHOGONAL FACTS, not one state: the deferred store the cell
stands for, and whether anything has given it a value. That is the honest shape,
and having it in one type is what makes the second half sayable in one place:
the two have different LIFETIMES. An alias is a value fact true on one path and
reverts at a join; `written` is a fact about the code, conservative and
permanent, and reverting it would let a later store defer onto a cell an
instruction already writes and drop the assertion that second write is, which is
the first soundness bug this crate ever fixed. The join now says that in one
line instead of it being implicit in which map got restored.
Same output: the fifteen golden digests are unchanged and the guest is still
328,553 instructions.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL compiler: intern a pure result where the cell is minted
The guest drops 550 bytecode instructions and 2,886 cycles on the documented
recursion benchmark, 719,659 to 716,773. Cycles are committed, so that is the
part that costs.
A pure operation whose result goes in a fresh cell is now looked up before it is
computed, keyed by the operation and its sorted operands, cached in `Scope` so
it reverts at a branch join like every other lazily materialized cell. The rule
that makes sharing sound is that it only ever mints a FRESH cell: a pure op
whose destination already exists is an assertion rather than a computation, the
zero cell an `assert` XORs into or the `g^{k-1}` a range check multiplies into,
and those must never be shared away.
Interning `expr`'s two arms alone changed nothing, which was the measurement
that mattered: the duplicates are not source-level expressions but the pointer
MULs that heap_addr and array_ptr emit for a heap access. Interning those is
where the 550 come from.
It does not replace cse.rs, which the plan claimed it would. With interning in
place CSE still earns 1,198 instructions on the guest, because it folds
duplicates across paths that never mint a cell at all. Both passes earn their
keep; the earlier one now does the share it can prove.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL compiler: state the interning rule correctly
The rule I wrote for `pure` was that it only ever mints a fresh cell. That is
necessary and NOT sufficient, and the gap is a trap for whoever extends it:
`assert a != b` also mints a fresh cell for its `x·inv`, then writes it again
with `SET p = 1`, and that second write IS the assertion. Route it through
`pure` and the next `assert a != b` skips its MUL, finds the cell already
holding 1, and asserts nothing.
The rule is that the result cell must have no other writer. The doc now says
that, and names the five sites that must stay out and why: the zero cell an
`assert a == b` XORs into, a range check's `g^{k-1}`, `assert a != b`'s product,
a division's back-solve, and `expr_into`'s caller-chosen destination.
Found auditing my own claim against every remaining pure emit site rather than
trusting it.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL compiler: cargo fmt the files the redesign wrote by script
Several files added or rewritten during the redesign never went through
rustfmt, so `cargo fmt --all --check` failed on the tree. Formatting only,
no behaviour change.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL compiler: pool the constant a pointer multiply needs, so the multiply interns
Two of the five pointer-MUL sites minted the g-power constant with `fresh()`
plus `set_const` instead of `const_cell`. The interning key then held a cell
only that one call could name, so the lookup missed every time and the two
sites were dead weight: each also inserted an unreachable entry that every
branch clone copied. Naming the constant through `const_cell` shares the `SET`
as well, which is the larger half of the saving.
The guest goes from 328,003 to 326,685 instructions and the recursion
benchmark from 716,773 to 710,020 cycles. Eight golden digests move with it.
Two invariants the change leaned on are now written down: `pure_cells` has no
label-target invalidation and is sound only because every backward edge crosses
a function boundary, and `expr_into` must keep writing its caller's destination
directly, since a second write there is the write-once assertion.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL: say in the cost table that a repeated pure operation is free
The table charges every occurrence, but identical pure results are shared
within a function, so a second `hb[i]` costs nothing. The sharing stops at a
branch join, which is the part a program author has to know.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL compiler: intern the five remaining pure sites that had no second writer
An `if`'s condition XOR, `assert a != b`'s `a + b`, `CallIfNe`'s XOR, the match
dispatch's squaring and `pow_expr`'s square-and-multiply chain all minted a
fresh cell and emitted their operation unconditionally, so each can take the
cached result instead. `assert a != b`'s product stays a fresh cell: its second
write is the assertion.
The guest goes from 326,685 to 326,180 instructions and the recursion benchmark
from 710,020 to 709,038 cycles. Three golden digests move, because a cache hit
shrinks the frame and shifts every later cell offset.
The rule on `pure` was stricter than the code obeys, so it now says what is
actually load-bearing. A second writer is allowed: `q = x ** k / w` lowers the
division into the cell the squaring chain returned, which is safe because the
chain runs first and determines the value. What must not happen is a later
write that determines the value, or that is itself the assertion.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL: a runtime index through addr(sb) is unchecked and usually does not fault
The reference already says a runtime heap index is unchecked, but a frame
pointer is the quieter case: every frame cell is real, so a hinted index
reaches any of them without a wild deref or a write-once conflict. Say so where
`addr` is documented, and record the second interning review in the plan.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL compiler: delete cse.rs, whose work the lowerer now does
The value-numbering pass ran after lowering and had to rediscover which cells
were safe to fold, from write counts, jump targets, the ABI boundary and a list
of frame runs whose address had escaped. Sharing identical pure results at
allocation time knows all of that already, and once the g-power constants were
pooled the pass was folding 15 instructions in the recursion guest and none at
all in any of the fifteen test programs. Its 254 lines go, with the
`opaque_runs` invariant that existed only to feed it, the `abi_end` and
`filler_start` fields it read, the fill-block pc adjustment that compensated for
its dropping, and the `DBG_CSE` and `DBG_NO_CSE` knobs. `seal_run` was
`materialize_run` plus the dead push, so the two are one function now.
The guest goes from 326,180 to 326,195 instructions and the recursion benchmark
from 709,038 to 709,040 cycles. No golden digest moves, since the pass folded
nothing in those programs. Net 353 fewer lines in the crate.
The seven tests that pinned the pass are kept as `tests/suite/sharing.rs`: each
names a duplicate that is not dead, which is a fact about the sharing rather
than about where it happens. Mutation testing found that three of them did not
name it, so they are rewritten:
- Two compared `GEN ** k` literals, which fold, so the duplicate XOR they
claimed to create was never emitted. Skipping `assert a == b` on a cache hit
passed all 138 tests. They read their operands from a HeapBuf now, and the
failing one panics again under that mutation.
- The third put one constant in both arms of a branch whose condition was true,
so the arm that ran was the arm that minted the cell and no leak could reach
it. It passed with both caches leaking past the join and with the scope revert
deleted. It now runs the second arm and requires a wrong published value to be
rejected, which catches the leak.
One test was deleted instead: it asserted a MUL-count difference of exactly one
between two programs, which only the pass produced.
Added, because nothing covered it: a StackBuf declared after a frame address has
escaped must be sealed on the spot. Leaving that arm of `alloc_stack`
transparent makes the store defer as a constant alias, folds the assert to
`const == const`, and proves that a cell holding g^7 holds g^9. It is the only
test of 138 that fails under that mutation.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL compiler: move free-variable analysis to ast.rs, and repair two spliced docs
The four free-variable functions take no lowering state and answer a question
about the syntax tree, so they sat in lower.rs only because their one caller is
the `for` desugaring. In ast.rs they are 162 lines the walker no longer carries;
lower.rs is 1,825 lines, from 3,124. The golden digests are unchanged, so the
bytecode is identical.
Two doc comments in FnLower were spliced by an earlier scripted edit. The
removed `alias` map's summary was left dangling above `slots`, and the removed
`phys` field's doc was grafted onto `cur_line`, truncated mid-clause at "if
either arm gives the cell a" so that cur_line appeared to document branch
restoration. What that fragment said is on `Slot` already, correctly. Three
comments elsewhere still named `phys`; they name `Slot::written` now.
The plan's reason for deferring M4 was that it depended on M3. That was wrong,
and the correction is that monomorphisation and loop desugaring depend
on scope, not on M3. A loop's capture set is its free variables filtered by what
each name is bound to, and `specialize` evaluates a constant argument, so
neither can run over an AST with no bindings.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL: const(...) works in a value position, so a value can ask for integer arithmetic
`+` in a value position is XOR, so `lvl + 1` with `lvl = 3` is 2 and not 4, and
silently: the value is well-formed, just not the one the arithmetic reads like.
The SPHINCS guest could not write a Merkle level into a tweak because of it, and
carried SP_P_LEVEL, a Rust-generated table of one literal per level, to get the
integer reading by indexing instead. The reference told authors to do exactly
that.
`const(...)` already meant "decide this with integer arithmetic" as an `if`
condition. It now means the same thing in a value position, so there is one
construct rather than two, and the table and its generator are deleted. The
guest's bytecode is bit-identical, which is what says the folded literal is the
one the table held.
The wrapper reinterprets the OPERATORS. It cannot reinterpret a LEAF, so a leaf
whose own two readings diverge is rejected: `n = 2 + 3` leaves the cell holding
`2 XOR 3` = 1 while the name's integer reading is 5, and `assert n == 1` and
`assert const(n) == 5` both passed in one program. Arithmetic then runs on a
leaf's bit pattern, which the reference now states, since an element of a
field-valued constant array is read as the integer those bits spell.
Two more, found while reviewing it:
- A `def` may not take a builtin's name. The builtin wins at the call site, so
`def const(x)` with an `assert` in it was never called and its constraint
silently disappeared, and whether it disappeared depended on whether the
ARGUMENT folded, so one call site had two meanings. Already true of `f192`.
- The parser's near-miss guard for `if const(...)` no longer fires on a
condition carrying its own comparison. `const(...)` is a value expression now,
so `if const(k) == n:` is an ordinary runtime test, and rejecting it made the
two operand orders behave differently.
The reference's claim that `2 ** 64` is the tower element `y` was wrong for a
value position, where `**` is a field power: the literal is, `2 ** 64` is `x^64`
reduced, and `const(2 ** 64)` is the literal.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL: const(...) means the same thing in every position, transparent where the reading is already integer
Making it a value form left it accepted in a HeapBuf size, an unroll count, a
GEN ** exponent and a stack index, while being a parse error in a StackBuf size,
a log bound and a global constant. One construct with two meanings depending on
where it stood, which is the wart the wrapper exists to remove.
A size, a count, an exponent, a bound and an index have only the integer
reading, so `const(...)` there asks for what they already do. It is transparent
now, folded by the parse-time integer evaluator, which covers all three
rejecting positions in one place. Transparent means transparent: `assert log v <
const(0)` still fails as "range-check bound GEN ** 0 names the empty set",
exactly as the bare spelling does, so the wrapper is no route past a bound.
A stack index that does not fit in u32 also reports that again when it is
wrapped. It read the precise diagnostic off `Expr::Lit` alone, so
`sb[const(2 ** 33)]` fell through to "must be a compile-time integer" while
`sb[8589934592]` named the real problem.
The test asserts AST equality against the bare spelling, which is what pins
transparency rather than mere acceptance. An `unroll` count keeps its expression
for the lowerer in either spelling, so that one is pinned on the compiled size.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL compiler: point a stale comment at the reference
It said the language had no way to say which arithmetic regime was meant, which
`const(...)` now does, so it points at the reference instead.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL compiler: cut comment narration, and repair a third spliced doc
`Scope`'s description sat orphaned above `Bound`, so `struct Scope` had no doc at
all and `Bound`'s read as though it described the scope. That is the third doc
pair an earlier scripted edit spliced.
The rest is trimming. Comments that narrated the history of a bug (what the old
code did, what a review found) are the commit's job, not the source's, and the
same argument was written out three times over: the two-regime rule now sits in
one place per module with the worked example only where it is needed. Where a
comment restated the language reference, as most AST variant docs did, it now
says what the syntax is and points at `zkDSL.md` for what it means and at the
lowering function for how it works.
One measurement worth recording, since it contradicts why this started: at 28%
comment lines lean_compiler is not an outlier here. zk_alloc and parallel are at
30%, flock at 29%, lean_vm at 28%. The density was never the problem; the
duplication and the narration were.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL compiler: narrow the module boundaries, and restore three comments that were guarding something
An audit of the branch found the split re-exported almost everything: 77 of 79
items in the seven new modules were `pub(super)`, so the boundaries said nothing.
Twenty had no user outside their own file and are private now. Two functions were
in the wrong module: `const_arg` has both callers in call.rs and none where it
sat, and `blake2s_cv` was the one blake2s helper left out of builtins.rs.
`Slot` no longer derives `PartialEq`/`Eq`. Nothing compares one, and an equality
operator on a type whose doc opens "two orthogonal facts, not one exclusive
state" invites exactly the comparison that would be wrong.
Three comments went too far in the last commit and are back. The range check's
two `DEREF` destinations are unconstrained touches, and with that sentence gone
nothing said why reading nothing from them is correct rather than an omission.
`const_cell`'s revert is what holds the invariant up, and the hoisting of `one()`
above a branch is only an optimization; the remaining text guarded one misreading
and the removed sentence guarded the other. And the AST's `hint_witness` and
`match` docs lost pointers, one of them to a doc label, which AGENTS.md calls an
API.
Return-shape inference's `LetHintWitness` arm was live but untested: deleting it
left all 141 tests green, while the test covering it claims three walkers. Only a
program that REBINDS a StackBuf name to a scalar hint reaches it, which is the
case now added, and it is the only test of 141 that fails when the arm goes.
determinism.rs said a `sort_unstable` in `lower::scoped` was what kept hash
iteration out of the bytecode. That sort was deleted, nothing iterating a hash
container reaches the bytecode now, and reversing the branch-output order at a
join moves no digest. The doc claimed a property the table does not test; it now
says what the table is, a codegen snapshot, and why that still earns its place.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL: a stack store always emits, which deletes the value-tracking layer
`sa[k] = other` used to record an alias and emit nothing, forwarding every later
read to the source. That optimization is worth 646 instructions of 326,195 (0.2%)
and 8,026 cycles (1.1%), and it cost the whole apparatus that made it sound: the
`Alias` type, the `Slot` type, the alias journal, `word_src` / `cell_src` with
cycle detection, `copy_alias`, and the branch-join replay that materialized a
deferred store before its aliases were dropped. Two of the six soundness bugs
fixed on this branch lived in it.
Deleting it deletes more than itself. The only reason the compiler tracked which
cells were written was to decide whether a store MAY defer; with stores always
emitting, nothing reads that, so `written`, `is_written`, `mark_written` and the
per-instruction bookkeeping in `emit` go too. And the only reason a frame run had
to be SEALED when its address escaped through `addr()` was that a later store
would otherwise defer onto a cell a `DEREF` had written; with no deferral,
`unsealed_runs`, the seal-every-run rule and `materialize_run` go as well. The
machine's write-once memory distinguishes an assertion from a definition, so the
compiler no longer has to.
What the guest can express is unchanged, and `addr()` survives. lean_compiler's
src goes from 6,224 lines to 5,925. All fifteen golden digests move, since every
program's stack stores are now instructions.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL: a blake2s input operand may name its two words directly
The opcode addresses its four input chunks independently, so an operand whose
words live in different places never had to be gathered into a consecutive run;
the compiler was only able to avoid the gathering because a stack store of a
plain copy deferred, which no longer happens. `blake2s([a, b], [c, d], out)`
names the words instead, allocating nothing, and says at the call site what the
buffer idiom said in four lines.
Four guest sites use it. The measurable effect is small, 39 instructions, since
they sit in per-signature setup rather than a loop, but the spelling is the one
that matches what the instruction does.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* guests: name blake2s operand words at the call, instead of gathering them into a buffer
Fifteen sites allocated a two-cell buffer, filled it with plain copies, and hashed
it. The copies were free while a stack store deferred; they are instructions now,
and the operand never needed to be consecutive, so the words are named at the
call and the buffer is gone.
Two of them are the chain walks, `walk` and `sp_walk`, where the buffer was
reallocated every step to carry one word and a zero. They now thread the word
itself and pass `[word, 0]`, which drops a copy and a `SET` per chain step: the
hottest loop in both schemes.
Against the state before the deferral was deleted, this recovers most of what it
cost. `aggregate --sphincs 220` goes from 2,689,990 cycles to 2,404,450 against a
2,375,062 baseline, `recursion --n 2 --xmss-per-leaf 900` from 717,066 to 709,832
against 709,040, and `aggregate --xmss 900` from 1,922,299 to 1,575,694 against
1,537,846. The guest is 326,412 instructions.
One care point: the FORS secret buffer had its second cell zeroed explicitly, and
that zero is load-bearing, the hash reading both cells. It moved into the call as
`[secret[0], 0]` rather than being dropped, which would have left the cell
unwritten and so prover-chosen.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL: a multi-value target may be a StackBuf element, which pays for the deferral's removal
A single-value assignment has always written into its target: `sb[i] = f(x)`
passes `sb+i` as the callee's return cell, so no copy follows. A multi-value one
could not say the same, and the parser rejected it outright ("bind match_range
results to names, not a store target"), so `t, e = match_range(...); tips[i] = t`
paid a copy per element. In the WOTS digit loop that is V = 42 copies per
signature, which is the whole of what deleting the store deferral cost XMSS.
So the restriction goes. A target is a name or a `StackBuf` element, and
`ret_targets` resolves each to the cell the arms write into: a name still takes a
fresh cell and binds, an element IS its cell. The ABI needed nothing new; it
already returns into cells the caller picks.
Against the state before the deferral was deleted, the three documented
benchmarks are now level:
aggregate --xmss 900 1,537,846 -> 1,537,894 (+0.003%)
aggregate --sphincs 220 2,375,062 -> 2,376,730 (+0.07%)
recursion --n 2 ... 709,040 -> 709,832 (+0.11%)
lean_compiler's src is 5,985 lines, from 6,224 before the deferral went, so the
value-tracking layer, the written-cell bookkeeping and the escape sealing are
gone for 239 net lines and no measurable proving cost. The guest is 326,328
instructions, from 326,195.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* zkDSL compiler: a match_range name target is a binder, not a use
Letting a target be an expression made `subst` rewrite it, and the two halves of
that arm then contradicted each other: `shadow` reported the statement as
REBINDING the name, while the substitution had already turned the binder itself
into a literal. So `k, e = match_range(...)` inside a function with a `Const k`,
or `j, e = ...` inside `unroll(0, 2)`, stopped compiling with "a multi-value
target must be a name or a StackBuf element, got `Lit(3)`". A name target is
never substituted now; an index target still is, since `sb[k]` needs `k`.
Three things the change should have come with:
- The bounds check on a `StackBuf` target was untested, and it is load-bearing:
removed, a program that never as…
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.