Rust to lean bytecode expansiosn#1666
Conversation
Just making the grammar printable has given us a huge leg up
Things look like they'll work out but fuck only knows till we build it.
New CLI crate that runs the real bytecode expander (expand_instruction) for a source instruction and prints the result as a Lean Program, so the Rust expander is the source of truth for the hand-written Lean expansions in JoltISA/Expansions/. Both arms of the rd==x0 branch are emitted. - Classify each source-only kind as Expand / Unsupported / NotExpandable; leave System/CSR, load-reserved (LRW/LRD), store-conditional (SCW/SCD) and Inline hand-coded for now. - Split the LD fault class from the alignment-assert exception class: a plain store's read-modify-write read is a normal load (.normal), while only true atomics (AMO/LR/SC) use the .amo read side. The class is unreachable at runtime for the always-aligned internal read and only selects the Sail exception class the proof layer expects. - Expose is_source_only from jolt-program so the generator gates on the same expand-vs-native decision the expander uses. - Drop the superseded prototype dump-recipe tests now covered by the crate. Verified the generated output matches the hand-written Lean across all 57 supported instructions (DivRem, loads, atomics, ALU/Mul, stores); the only remaining divergences are the advice-load rd==x0 handling (a Lean-side bug) and the SRLIW/SRAIW bitmask spelling (provably equal values).
New CLI crate that runs the real bytecode expander (expand_instruction) for a source instruction and prints the result as a Lean Program, so the Rust expander is the source of truth for the hand-written Lean expansions in JoltISA/Expansions/. Both arms of the rd==x0 branch are emitted. - Classify each source-only kind as Expand / Unsupported / NotExpandable; leave System/CSR, load-reserved (LRW/LRD), store-conditional (SCW/SCD) and Inline hand-coded for now. - Split the LD fault class from the alignment-assert exception class: a plain store's read-modify-write read is a normal load (.normal), while only true atomics (AMO/LR/SC) use the .amo read side. The class is unreachable at runtime for the always-aligned internal read and only selects the Sail exception class the proof layer expects. - Expose is_source_only from jolt-program so the generator gates on the same expand-vs-native decision the expander uses. - Drop the superseded prototype dump-recipe tests now covered by the crate. Verified the generated output matches the hand-written Lean across all 57 supported instructions (DivRem, loads, atomics, ALU/Mul, stores); the only remaining divergences are the advice-load rd==x0 handling (a Lean-side bug) and the SRLIW/SRAIW bitmask spelling (provably equal values).
`--lean` prints one `<name>ProgramAuto` def per supported source instruction as a single Lean file (namespace JoltISA), mirroring the hand-written programs in JoltISA/Expansions/. rd-writing kinds render both arms of the rd==x0 branch as `if isX0 rd then … else …`; stores (no rd) render a single body. - Render registers as valid Lean terms: virtual temps as `inlineTmp n` (inlineTmp0 = v40), x0 as `regidx.Regidx 0`; source operands stay bare parameters rd/rs1/rs2 and the pass-through immediate a BitVec 12. - Reuse the immediate helpers (slliMultiplier/sraiBitmask/srliBitmask) from Expansions.ALU rather than inlining raw bitmasks. - Factor the fault-class/alignment logic into fault_info and the row rendering into arm_lines, shared by the existing --all dump. Verified the output builds: lake build JoltBytecode.JoltISA.ExpansionsAutomated.
Advice instructions (VirtualAdvice/VirtualAdviceLoad) carry an oracle value the trace supplies; the concrete immediate the expander emits there is only a placeholder. Baking it (e.g. 0) modelled the wrong program, so render each advice operand as a fresh symbolic `adviceN : BitVec 64` parameter instead. - Detect advice rows via the canonical `CircuitFlags::Advice` flag rather than matching opcode names. - Determine a def's parameters (rd/rs1/rs2/imm) from the expansion's row operand fields instead of scanning the rendered text. - Fault classification stays name-based (a Lean-side synthesized concept with no Rust source of truth). This makes the generated DivRem/advice programs general over the advice values, matching the hand-written Lean.
|
Warning This PR has more than 500 changed lines and does not include a spec. Large features and architectural changes benefit from a spec-driven workflow. If this PR is a bug fix, refactor, or doesn't warrant a spec, feel free to ignore this message. |
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
|
Claude code review session started: https://claude.ai/code/session_016Qo6PQsuB7iibP9csmddfX |
moodlezoup
left a comment
moodlezoup
left a comment
There was a problem hiding this comment.
Reviewed the jolt-lean-gen transpiler crate. This is a self-contained, offline dev tool: it doesn't touch the live prover, verifier, transcript, or constraint generation, and the only changes to existing code are making is_source_only public and adding #[derive(Debug)] — so none of the soundness/proof-correctness concerns apply here.
The transpiler logic itself checks out for the current instruction set: the recipe constants are all small values that don't collide with the immediate sentinel, and the shift-bitmask trailing_zeros recovery (sraiBitmask/srliBitmask/slliMultiplier) correctly reconstructs the shift amounts. Since translations are formally verified downstream against the hand-coded Lean, the _ best-effort arm and other heuristics are appropriately caught if wrong.
One non-blocking robustness note left inline on the SRC_IMM sentinel. Otherwise looks good.
Generated by Claude Code
| // Distinctive source-immediate sentinel: valid as a 6-bit shift amount and a | ||
| // 12-bit immediate, and unlikely to collide with a recipe constant. Any row whose | ||
| // immediate equals this is the source immediate passed through, printed as `imm`. | ||
| const SRC_IMM: i128 = 37; |
There was a problem hiding this comment.
Non-blocking, but worth guarding: this identifies the pass-through source immediate purely by value (imm == 37). Any recipe constant or derived immediate that happens to equal 37 gets silently rendered as imm instead of its literal, producing wrong Lean with no signal — which is exactly the failure mode this tool is meant to eliminate by replacing hand-coding. Today's recipes only bake small constants (-8, -1, 7, 3, 6, 0), so there's no collision now, but nothing enforces that as new instructions are added to the table. Consider at least a debug assert that no non-passthrough row in an expansion carries the sentinel value, or feeding a sentinel wide enough that a collision is implausible for any plausible recipe constant.
Generated by Claude Code
There was a problem hiding this comment.
Noted. I'll update this tomorrow. Thanks, Michael.
There was a problem hiding this comment.
I've resolved this by running the instruction with two immediate values -- 37 and 41 in this case (5 and 13 for smaller width instructions).
Now if any hardcoded immediate exists, it would be the same for both inputs, and we'd know that immediate should not be substituted with imm but the pretty printer.
The way we generate lean translations is by leveraging the existing expander. for LB rd imm, we give a fake value for rd=x1 and imm=37. And then tell the printer if you see imm=37 use imm else use the actual constant. Now if ANY expansion used 37 as the hardcoded value, we'd screw up. We would not use the harcoded value, we would use imm. And generate garbage. Currently it does not but it could later. So we add in a check by using both 37 and 41, and if in both cases the row.imm equals 37 and 41, then we know that immediate is not hardcoded.
2 participants
Summary
This crate is a lightweight wrapper around
jolt-riscvandjolt-programto automatically extract Jolt bytecode expansions in Lean.There is only 1 file
main.rsand it is heavily commented.Tracing the usage command listed below, and following the comments in an IDE should be self explanatory.
Testing
cargo clippyandcargo fmtpassSecurity Considerations
Does not touch live prover or verifier.
Breaking Changes
This is a source to source transpiler.
Does not touch live prover or verifier.