Repository navigation
VmSpec: a VM-level spec and soundness substitution theorem - #309
Conversation
…on theorem Adds ApcOptimizer/VmSpec/, a VM-level correctness spec sitting alongside the existing single-circuit spec in Spec.lean. It defines the behavior of a collection of guest circuits running against a fixed host — memory, lookup tables, execution bridge, trace budget — and what it means for one guest-chip list to be an equivalent (sound + complete) replacement for another in that context (VmEquivalent, Basic.lean). vmSoundReplacement_of_forall₂ (Implementation/Connection.lean) shows the per-chip soundness an optimizer pass already proves lifts to this VM-level notion, given legality of the guest lists and the host's configured size bounds — almost closing the loop to the audited, chip-level optimizer, except that legality of the optimizer's *output* isn't derived by this theorem (see below). OpenVm.lean instantiates the framework for OpenVM (bus rules, host, degree bound); Audit/ is evidence for those instantiation choices, including RealApcLegality.lean's check of a real keccak-block APC through three stages of powdr's own optimizer pipeline. Fusion.lean adds a VM-level fact about chip fusion, powdr's autoprecompiles starting point: offering a fused two-instruction chip alongside its still-present ingredients is a sound and complete VM-level replacement, soundness gated only on an instance-budget hypothesis (unfusing doubles instance count). Audit surface: Basic.lean, Legal.lean, OpenVm.lean, Theorems.lean, plus Audit/ as evidence for those. Everything under Implementation/ needs no audit — its correctness is fully discharged by its own proof. Weakest part: Circuit.legalGuest's clauses all have the shape "true of every algebraically-satisfying assignment", necessarily, since a real AIR can't check them at runtime and so they can't be part of VmSat. But Circuit.isSoundReplacementOf, what a pass actually proves, only constrains assignments that are also bus-accepting, and only the net multiplicity of stateful messages — nothing about an individual message, nothing about stateless buses, nothing pointwise. A sound replacement can therefore admit an assignment that's algebraically satisfying but not bus-accepting and outright illegal — a chip sending a stateless message with a wholly unconstrained multiplicity is a sound replacement of one sending the same message at a legal, constant multiplicity, and violates statelessSendOnly outright. Audit/SoundnessGivesLegality.lean narrows this against OpenVM's real bus semantics but still exhibits a residual gap. So legality-preservation of an optimizer's output needs a genuinely separate, pass-by-pass argument that no pass proves today — the real missing link between the fully-proven chip-level Optimizer.isCorrect and a closed VM-level theorem. Excluded from the default lake build target and from ApcOptimizer.lean's import closure (see that file's comment) — build explicitly with `lake build ApcOptimizer.VmSpec`.
alex-ozdemir
changed the title
OpenVM — openvm-eth (100 basic blocks)
Per-case circuit sizes are identical between main and this branch. Slowest cases (out of top 10)
Per-stage runtime breakdown (out of top 10)
OpenVM — wasm-eth (100 basic blocks)
Per-case circuit sizes are identical between main and this branch. OpenVM — keccak (1 basic block)
Per-case circuit sizes are identical between main and this branch. OpenVM — sha256 (1 basic block)
Per-case circuit sizes are identical between main and this branch. SP1 — rsp (100 basic blocks)
Per-case circuit sizes are identical between main and this branch. SP1 — keccak (1 basic block)
Per-case circuit sizes are identical between main and this branch. openvm-eth + wasm-eth + keccak + sha256 + sp1/rsp + sp1/keccak, PR |
|
Very cool! This is a very exciting direction to reason about a VM -> VM transformation instead of Circuit -> Circuit. Among other things because it potentially enables more optimizations, like the optimizer deciding to add a new memory address space with a larger word size, to name one example. I spent a bit of time reading through the spec, but not enough yet. A few things that I think I understood so far:
I need to think about this more, but I wonder whether this is correct, and whether this can be simplified. In the context of a long computation across many computation shards (OpenVM calls a shard "segment"), the only thing that counts is the address space 3 values in the last segment. It is usually written at the end of the computation. But when considering a single segment, address space 3 might not be touched at all; instead, the VM might only modify the memory state, which is the input to the next segment. So it either seems like we'd have to make sure the entire memory image (pre and post) stays fixed, or we'd have to reason about VM execution across many segments? One potentially simpler - although overly restrictive - way to do this would be to say that the effect of the host chips (maybe "system chips" would be a better name) has to stay fixed. That would be similar to the circuit-level spec, where the net effect on the stateful buses has to stay the same. It would be less restrictive than the circuit-level spec, but more restrictive than needed. For example, the memory image would have to stay exactly the same (even the final time stamps, which prohibits time stamp compactification), but during the computation the optimizer could use memory in different ways (e.g. store different intermediate values). |
|
Good comments and questions.
Agreed, good point. Looking ahead: for completeness we'll need a forward mapping for each guest circuit and the hints. (So if the hints change, we'll need to know how to compute the new ones.) And, for knowledge soundness, we'll need reverse mappings.
Agreed. The multi-segment setting is a bit different that what I wrote down. In the multi-segment setting, preserving memory before/after each segment ensures that AS3 (the outputs) are preserved after all segments.
I love this idea. Of course, we explicitly want to change the effects of some host chips (table sinks). So, for each host chip we can indicate whether its effects must be fixed or not. Maybe this is what you meant by "system chips"? When developing Perhaps in the future, we could be slightly less restrictive by permitting some kinds of changes, for specific chips. (For example: to allow dead-register sends to be removed by the optimizer.) |
|
That makes sense to me!
One way would be to say the stateful buses have to stay fixed, and the stateless buses (a.k.a. lookups) can change. That's the route we went in the circuit-level spec. By "system chips" I mean anything that doesn't directly execute an instruction, basically lookup tables and memory and execution bus initialization and finalization. I think OpenVM also uses the term "periphery" for this, maybe that's a better name! |
This actually shrinks the spec.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* Proves a completeness theorem. * Moves to Arie's order-free admissibility (copied in-tree). * Strengthens legality, and audits it against more real APCs
|
Small update:
|
georgwiese
left a comment
georgwiese
left a comment
There was a problem hiding this comment.
Cool! I had a closer look, and some comments / questions so far.
Also, it doesn't currently build, does it? lake build ApcOptimizer.VmSpec fails for me (even after b472890).
| instanceBound : ℕ | ||
| /-- Whether this chip's effects are part of the whole VM's effects (`VmAssignment.effects`). | ||
| For example, memory initialization, finalization, hints... Non-examples: tables. -/ | ||
| isIo : Bool |
There was a problem hiding this comment.
Note that this is only used in VmAssignment.effects to essentially filter out lookup
table effects. Could we remove this entirely and instead rely on a isStateful (busId : Nat) : Bool
predicate?
There was a problem hiding this comment.
Yes, something like that seems reasonable, and it might be a good way to further simplify! We could define the VM effect to be the net effect of the guest (equivalently, host) on the stateful busses.
| /-- No timestamp overflow: a run of `maxInstances` instructions, each advancing the clock by less | ||
| than `maxWindow`, does not overflow. | ||
|
|
||
| TODO(AO): why the +1's? Are these bounds still tight? | ||
| -/ | ||
| noTimeOverflow : (maxInstances + 1) * (maxWindow + 1) < p | ||
| /-- No multiplicity overflow: a run of `maxInstances` instructions, each with at most | ||
| `maxInteractions` bus interactions, does not overflow. | ||
|
|
||
| The `+ 1` is for the exempt host chip's own touch. -/ | ||
| noMultOverflow : maxInteractions * maxInstances + 1 < p |
There was a problem hiding this comment.
It would be nice to relate these checks more closely to the "official" OpenVM assumptions and
verifier checks, namely:
- The timestamp delta is bounded by
num_interactions * num_rows_per_execution(source).num_rows_per_executionis always1for instruction chips and APCs. We currently do not ensure
that (we leave the time stamp delta constant and reduce the number of bus interactions), so this is a real soundness bug. We could fix this by adding dummy bus interactions (e.g. byte-checkingis_valid) until the number of bus interactions equals the delta. - The trace height constraints enforced by the verifier.
See also these docs.
I believe the current framework is too rigid in practice: We'd have to set a large maxWindow
in order to support large APCs, but then we'd have to lower maxInstances to meet the noTimeOverflow
requirement. But maxInstances would apply to all chips, even those with a low timestamp delta.
There was a problem hiding this comment.
I totally agree; my sizing approach was very arbitrary and loose. Hopefully, if you give better constraints, Claude can still prove they suffice or give a counterexample.
Feel free to edit the PR to use whatever constraints are best-aligned with OpenVM. You would probably be better at choosing the right constraints than I would be 😄 .
|
|
||
| /-- The net effect of the host instances. -/ | ||
| def HostAssignment.busEffect {host : Host p} (hA : HostAssignment p host) : BusState p := | ||
| fun message => ∑ t : Fin host.chips.length, ((hA t).map (fun effect => effect message)).sum |
There was a problem hiding this comment.
| fun message => ∑ t : Fin host.chips.length, ((hA t).map (fun effect => effect message)).sum | |
| fun message => ∑ t, ∑ i, (G.get t).allEffects ((gA t).get i) message |
I didn't know of this ∑ notation before, really cool! Much better than map + sum
| operand `a`, is a second chip type this host does not model yet — adding it is a new | ||
| `isIo := true` entry in `openVmHost.chips` rather than a reshape. -/ | ||
|
|
||
| structure InputRead (p : ℕ) where |
There was a problem hiding this comment.
I wonder to what level of detail we have to spell this out. Since the input chip is marked as
an I/O chip, the side effects must be held constant anyway. The only thing we need to say is
that the chip implements a byte check on the stored payload, no? If we didn't do that, the
optimizer could no longer rely on any word received from the memory bus being properly range-checked.
There was a problem hiding this comment.
There is probably a simpler way, agreed. We do need to capture exactly what effects the chip can have, but maybe some other approach is simpler.
There was a problem hiding this comment.
Right, we need to describe the effects the chip can have just by its own constraints. This is currently done by InputRead.interactions explicitly spelling out the concrete messages for a given InputRead record which is used in:
def inputHostChip (ptrReg maxInstances : Nat)
(execBusId : Nat := openVmExecBusId) (memBusId : Nat := openVmMemBusId) :
HostChip p where
canProduce contribution :=
∃ r : InputRead p, contribution = busStateOf (r.interactions ptrReg execBusId memBusId)I think we could also constrain contribution more directly. That would allow us to just ignore the pointer, for example, because this chip doesn't put a constraint on it.
I'm not decided, but interesting design space. What I like about the current approach is that it is close to zk proving paradigm of "there exists a witness such that the constraints are satisfied". Maybe there would even be a way to import the actual OpenVM constraints in an automated way, reducing duplication and shrinking the spec.
| /-- Memory holds bytes; see `memoryFinalizeHostChip`. Registers included — a peeked register is | ||
| a memory access like any other, so its limbs carry the same discipline. -/ | ||
| byteIsByte : isByte byte | ||
| oldWordIsBytes : ∀ d ∈ oldWord.toList, isByte d |
There was a problem hiding this comment.
I think this is wrong: Since the input chip does not range-check the old word, the chip can
produce a side effect where this is not the case. By saying it cannot, we're saying that this
chip implements a range check on the previously stored word, which could be exploited by the
optimizer to save a range check elsewhere.
There was a problem hiding this comment.
Good catch! I agree; fixed.
| to the send set"), not traffic outside the instruction stream. -/ | ||
| pcFrom : ZMod p | ||
| /-- The `pc` it hands on. -/ | ||
| pcTo : ZMod p |
There was a problem hiding this comment.
Does this not equal pcFrom + 4?
There was a problem hiding this comment.
It's a constant offset, agreed, see inputStepWindow in this file. I'm not sure what the constant is.
The fact that OpenVM's implementation of this chip calls its timestamp_pp function three times (looking here and doing a ctrl-f for timestamp_pp) makes me thinks it is 3, but I do not really know.
There was a problem hiding this comment.
Wait, but now you're talking about the time step! I agree that inputStepWindow is set correctly to 3 for the reasons you described.
The PC is actually incremented by 1 (not 4): The chip calls execute_and_increment_pc which sets the next PC to the previous PC + 1.
BTW, I think the input chip is a bit more complicated, because there is also an opcode to write an entire array of hints. That's why the time stamp difference is actually not a constant but depends on the rem_words witness, but getting that 100% right requires another deep dive...
There was a problem hiding this comment.
Oh, you're totally right on both counts. Agreed!
| `openVmRankShift`, which is what makes `<` well-founded and | ||
| `maintains_of_stateful_active`'s induction possible. Off the stateful buses the rank is `0`; | ||
| nothing there needs the induction. -/ | ||
| def openVmRank (memBusId : Nat := openVmMemBusId) : BusMessage p → ℕ := |
There was a problem hiding this comment.
I don't immediately understand this rank thing, but it seems like it could be moved to
the implementation section? E.g. openVmRank is only used there.
There was a problem hiding this comment.
Good catch! Agreed, it's implementation. Fixed.
| variable {P : OpenVmParams p} | ||
|
|
||
| /-- **Substitution soundness, for OpenVM.** -/ | ||
| theorem openVm_vmSoundReplacement {G G' : Guest p} |
There was a problem hiding this comment.
So, as I understand this, G is the original VM with the "trivial" autoprecompiles
(= concatenation of instruction circuits) already added. So we are assuming that this
step is sound, and proving that then applying the optimizer to the circuits does not
break soundness. Right?
There was a problem hiding this comment.
Yes, agreed.
But as an aside, I do think we should be able to prove that concatenation is correct under our VM-level definition. The bottom of Fusion.lean has a theorem that looks approximately right. If we tweak it, we should be able to verify concatenation+optimization, end-to-end.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
|
I wasn't able to reproduce the build failure. Could you give more information? I tried Of course, I'm a huge Lean noob, so I could be easily missing something. |
|
I don't have the build issue anymore, and I don't know what the issue was 😬 |
georgwiese
left a comment
georgwiese
left a comment
There was a problem hiding this comment.
On a higher level, I think we should merge this PR with minimal changes, even if the VM-level spec is still work in progress. It is very self-contained, doesn't interfere with the existing spec and only adds value IMO.
I we can remove the OpenVM white paper and link to it instead? That would be my biggest request; everything else I could also have a look into in a follow-up PR.
| | 7 => some (.tupleRangeChecker 256 2048) | ||
| | _ => none | ||
|
|
||
| /-- `1` is `defaultBusMap`'s only memory bus id — what `openVmGuestRules`'s `memPayloadOnly` field |
There was a problem hiding this comment.
Could we move the theorems here to either the implementation section or a special Audit module?
| import ApcOptimizer.Utils.Dsl | ||
| import ApcOptimizer.Utils.Size | ||
|
|
||
| -- `VmSpec` (a separate, still-WIP VM-level audit -- see `ApcOptimizer/VmSpec.lean`) is deliberately |
There was a problem hiding this comment.
I think it would be nice to include it here, e.g. to also check the VM-level spec in CI. I wonder how bad the compilation times really are (there should also be some caching). Including it here would also not blow up the unused-theorems.txt.
I can have a look into this after the PR is merged as well though.
Co-authored-by: Georg Wiese <georgwiese@gmail.com>
* drop the vendored whitepaper * move theorems off OpenVmSemantics * fix pcTo Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
|
I addressed your comments in this last commit @georgwiese, at least well enough to make this mergable; if you'd like to merge it, go ahead! |
2 participants
Summary
Adds a VM-level correctness spec (
ApcOptimizer/VmSpec/) alongside the existing single-circuitspec in
ApcOptimizer/Spec.lean. It defines the behavior of a collection of guest circuitsrunning against a fixed host — memory, lookup tables, execution bridge, trace budget — and, in
that context, what it means for one guest-chip list to be an equivalent (sound + complete)
replacement for another:
VmEquivalent.We show a soundness substitution theorem: that
Circuit.isSoundReplacementOfimplies our soundnessnotion, up to the legality of the guest chips and some host-determined size bounds. Legality is
necessary in some form, but our current treatment is non-ideal, as discussed below.
Separately, we prove a VM-level fact about chip fusion (powdr's
autoprecompilesstarting point):offering a fused two-instruction chip alongside its still-present ingredients is a sound and
complete VM-level replacement, again, modulo some sizing assumptions.
Where things live
ApcOptimizer/VmSpec/Basic.lean: VM semantics and equivalenceLegal.lean: legality for circuitsTheorems.lean: soundness substitution theoremOpenVm.lean: OpenVM host's specificationApcOptimizer/VmSpec/Implementation/Fusion.lean(
vmSoundReplacement_fuse_cons/vmCompleteReplacement_fuse_cons/vmEquivalent_fuse_cons).Audit/(it's a self-audit of sorts)Implementation/needs no audit — it's the proof of the theorems.Weakest part: legality
Our main theorem requires the initial and final circuits to be legal. This is worth considering
carefully for two reasons.
chips after they're fused and turned into the initial APC.
ApcOptimizer/VmSpec/Audit/RealApcLegality.lean(
apc2105000GatedPinned_legalGuestfor the is_valid removal of the final APC,apc2105000UnoptChained_legalGuestfor the timestamp linking of the initial one),checked against the real keccak-block APC at pc
2105000(
Audit/Apc2105000.lean, emitted byScripts/emit-apc-lean.py).and prove it is preserved under fusion.
with some tweaking.
Thanks to Claude for writing Lean and @1arie1 and @nafur for discussions :)