[quangvdao]

Summary

This PR proves constraint (26): honestWitness_ramOutputEqPublicIo, the public RAM output check in stage 2. On the public I/O interval, the honest final-RAM column equals the public I/O word. The interval runs from input_start up to, but not including, RAM_START_ADDRESS.

Stacked on #14 ((34)–(36)). Retarget to qvd/trace-assumptions (#18) once #14 merges.

Rebased onto #18. This branch (via #14) is now rebased onto #18 (qvd/trace-assumptions @ a3e7aad0fec915b7a887e4a73aef7a70245f7ea1), which replaces the vacuous JoltTrace.allAssumptions field with TraceAssumptions. lake build JoltConstraints (3565 jobs) plus every Tests/ module (3498 jobs) pass, and (26) and (34)–(36) keep the same axioms with no sorryAx. The proofs here do not use the dropped conjuncts, so these statements now hold for nonempty traces.

The proof has one premise, on the initial device: JoltIOState.AdviceBelowInput. It says:

• each advice buffer ends at or below input_start;
• input_start is a whole number of words above the lowest RAM address.

This PR also proves that Rust always satisfies the premise, instead of arguing it in prose. JoltIOState.AdviceBelowInput.of_memoryLayout derives it from a Lean transcription of MemoryLayout::new together with create_emulator's advice-length checks.

The sorry is gone, the stale FIXME row in model_review.md is removed, and constraints.md now reads 57 proved, 2 TODO ((38), (39)), 3 FIXME.

Diff metadata

• Base: qvd/registers-34-36. The merge base is 0d9fa22a0a28cf7711c2460eabe1c7770481ad80, which now sits on a3e7aad0fec915b7a887e4a73aef7a70245f7ea1 (qvd/trace-assumptions, fix(trace)!: require only satisfiable row assumptions on JoltTrace #18).
• Head: 1a2e4bd0dc2aa2450a2cc8aaceca0c8d6b57f370
• Commits: 2
• Files changed: 6
• Diff: 488 insertions, 15 deletions

Motivation

The (26) target carried a FIXME. It said the Lean model did not enforce Rust's layout and buffer bounds, and that this boundary had to be audited before attempting a proof, without restricting Rust-valid executions.

Without some such bound, the statement is false. Take an advice buffer that runs past input_start with inputs empty. Its bytes land in finalRamWord inside the window, while ramPublicIoWord is 0 there.

How trivial is (26)?

It is mostly definitional, and that is faithful to Rust. final_ram_state (crates/jolt-witness/src/backend/trace/ram.rs#L134) builds the honest final RAM as layers taken from the device, in this order:

memory image → trusted advice → untrusted advice → inputs → outputs → panic → termination

The verifier's public word stacks the last four layers from the same device, and the Lean definitions copy this structure. So (26) says only that the first three layers stay out of the I/O window.

Whether the device's outputs/panic agree with what the program actually stored is the job of (38), not (26). A blind read-back of the statement independently reached the same conclusion.

The premise, and why Rust always satisfies it

JoltIOState.AdviceBelowInput, in Constraints/RamReadData.lean:

structure _root_.JoltIOState.AdviceBelowInput (io : JoltIOState) : Prop where
  inputWordAligned : (io.layout.input.1.toNat - ramLowestAddress io.layout) % 8 = 0
  trustedAdviceBelowInput :
    io.layout.trustedAdvice.1.toNat + io.trustedAdvice.size ≤ io.layout.input.1.toNat
  untrustedAdviceBelowInput :
    io.layout.untrustedAdvice.1.toNat + io.untrustedAdvice.size ≤ io.layout.input.1.toNat

This is exactly what overlayRamBytes_below_input consumes. Nothing about region ends, absolute alignment, advice-start alignment, or the output/panic/termination placement is assumed.

inputWordAligned is necessary. With 4 bytes of advice at the lowest address and input_start 4 bytes above it, the first masked word still contains advice.

Constraints/MemoryLayout.lean (new) transcribes MemoryLayout::new up to input_start (common/src/jolt_device.rs#L346-L438) as adviceInputLayout : MemoryConfig → Option AdviceInputLayout.

• Faithful parts: align_up, the checked sums, next_power_of_two and RAM_START_ADDRESS - io_bytes. Each Rust panic becomes none.
• Placement: the larger advice region goes first.
• Omitted: the power-of-two assertions and everything after input_start. These only add panics, so the Lean function succeeds on at least every configuration Rust accepts.

JoltIOState.AdviceBelowInput.of_memoryLayout then shows io.AdviceBelowInput from:

• adviceInputLayout config = some layout;
• the device's start addresses equal the computed ones;
• each advice length ≤ its configured maximum. This is the check in create_emulator, tracer/src/lib.rs#L382-L393.

Sanity check. #eval adviceInputLayout ⟨0, 0, 0, 8⟩ gives input_start = 0x7fffffe0. That matches the layout printed by the Rust tracer harness for the same MemoryConfig at a16z/jolt 754fc88.

The theorem keeps the weaker premise rather than taking "the layout is MemoryLayout::new config" as a hypothesis, so it applies to any device with the property. The bridge theorem connects it to Rust.

Proof structure

1. IOSetupFrame.lean (new). A frame calculus over JoltMonad: Same, Preserves, the pure/bind/lift/throw/get/modify rules, register, memory and device rules, execHostIO_rule and execInstr_rule. No instruction changes the layout or either advice buffer. finalTraceState_ioSame lifts this to the whole trace, which matters because finalRamWord remaps with the initial layout.
2. overlayRamBytes_below_input. An overlay whose bytes end at or below input_start is the identity from the input's first word onward. It needs no alignment of the overlay start: remapping rounds down, which only moves bytes lower.
3. finalRamWord_eq_ramPublicIoWord. Inside the mask, L + 8a < RAM_START_ADDRESS, so the memory-image layer is 0. Both advice layers drop out by step 2. The remaining overlays are syntactically equal.
4. honestWitness_ramOutputEqPublicIo. Closes with sub_self inside the mask.

Trust surface

• New premise: only adviceBelowInput, on the initial state, with the machine-checked bridge above.
• Transcription: adviceInputLayout is hand-transcribed from Rust, the same trust model as JoltISA.
• No new axioms, sorry, admit, native_decide or option changes (other than autoImplicit false).
• #print axioms honestWitness_ramOutputEqPublicIo: load_reservation, match_reservation, plat_term_write and sys_enable_experimental_extensions, which are existing LeanRV64D Sail platform axioms (I did not trace which lemma pulls them in), plus propext, Classical.choice and Quot.sound.
• #print axioms JoltIOState.AdviceBelowInput.of_memoryLayout: propext, Classical.choice, Quot.sound.
• Not checked:
  • Rust's final_ram_state remaps with preprocessing.memory_layout but reads start addresses from device.memory_layout. Lean uses one initial layout for both. If the two can differ, the model diverges.
  • That Rust's dram_start is always ≥ RAM_START_ADDRESS. Lean gates the memory image at RAM_START_ADDRESS.

Commit map

• 280da7e: I/O frame, the (26) proof, and a first pair of premises, JoltIOLayout.Valid and JoltIOState.AdviceFits.
• 1a2e4bd: replaces those with the single weaker AdviceBelowInput, and adds the MemoryLayout::new transcription plus of_memoryLayout.

Validation at 1a2e4bd

• Full lake build succeeded locally (8589 jobs).
• The axiom footprints are as listed above.
• #eval of the transcription matches the executed Rust layout.
• The diff against 0d9fa22 adds no sorry, admit, native_decide or axiom.
• CI status: see the checks tab.

Remaining work

• (38) and (39) remain TODO; (01), (16) and (37) remain FIXME, blocked by upstream Rust issues.
• The transcription stops at input_start. Later theorems, such as (38) and constraint soundness, will want the rest of MemoryLayout::new.

Reviewer map

1. Constraints/RamReadData.lean: AdviceBelowInput.
2. Constraints/MemoryLayout.lean: compare adviceInputLayout line by line with jolt_device.rs#L346-L438, then of_memoryLayout.
3. Constraints/RamOutputEqPublicIo.lean: the theorem statement, then the two lemmas.
4. Constraints/IOSetupFrame.lean: skim the rules; read execInstr_rule and finalTraceState_ioSame.
5. constraints.md, model_review.md.

AI usage

Claude Code (Opus) found the premise, checked it against the Rust source, transcribed MemoryLayout::new, and wrote the proofs under my direction. A separate Claude Code agent did a blind read-back of the statement. I reviewed the statement, the premise, the transcription and the Rust citations, and confirmed the build and axiom footprints locally.

🤖 Generated with Claude Code