Rust witness-generation interpreter for the witness IR

[mitschabaude-bot]

Context

#403 makes witness generation serializable data: every witness in the library is expressed in a deep-embedded IR (Clean/Circuit/WitnessIR.lean), and Operations.witgenJson? / the #witgen_json command (Clean/Circuit/WitnessExport.lean) emit a versioned JSON payload — the flat operation list with each witness op carrying its IR program. What's missing is the consumer: a Rust witness-generation interpreter, so that provers (e.g. the plonky3 backend) can generate traces natively instead of shelling out to Lean.

Task

Implement a witgen interpreter in backends/plonky3 (or a shared crate) that:

1. Parses the export payload ({"version": 1, "localLength": n, "operations": [...]}). Schema reference: the golden test in Clean/Examples/WitnessExport.lean; encoders in Clean/Circuit/WitnessExport.lean. Each witness op is {"witness": m, "code": {"steps": [...], "output": <vexpr>}}; other ops (assert/lookup/interact) can be skipped for witgen purposes.
2. Evaluates witness programs in a single linear pass over a growing witness array, mirroring the Lean reference interpreter Circuit.witgen (Clean/Circuit/WitnessGeneration.lean):
   • sequential offsets: each witness op appends its m values; expressions read earlier values via expr/envGet nodes,
   • two-sorted expressions: field ops (add/mul/inv/ofNat/ite/...) and Nat ops (add/mul/div/mod/and/or/xor/shiftLeft/shiftRight), bridged by val (canonical ℕ embedding) and ofNat (its inverse — not plain reduction mod char; matters for binary fields, see FiniteField.fromNat),
   • steps are let-bindings referenced by localVar index; mapRange outputs bind the loop index for idx nodes,
   • out-of-range conventions are total: arrGet/dataGet/hintGet read 0 out of bounds, inv 0 = 0,
   • dataGet/hintGet read prover-supplied tables keyed by name (e.g. FemtoCairo "memory", width 2).
3. Differentially tests against Lean: generate witnesses for the exported circuits via Circuit.witgen (a lake env lean --run script, like the existing trace generation in backends/plonky3/tests/helpers/lean_runner.rs) and assert byte-for-byte agreement with the Rust interpreter on the same inputs/data. Good first targets: IsZeroField, Xor64, SHA256/Add32 (exercises steps + loops), FemtoCairo memory reads (exercises dataGet).

Notes

• Trust story: witgen bugs are completeness bugs, not soundness bugs — a wrong witness fails to prove, never proves a false statement. Differential testing against the verified Lean reference interpreter (witgen_eq_dynamicWitnesses) is the intended assurance level; no verified compilation needed.
• Background and design history: doc/witgen-ir-plan.md, doc/witgen-authoring.md, and the original direction discussion on [codex] Compile circuit witnesses to checked array writes #401.
• #assert_exportable (in CI via Clean/Examples/WitnessExport.lean) guarantees exported circuits contain no native closures, so the interpreter never needs an escape hatch.

🤖 Generated with Claude Code