From 280da7eea9263b029e3f51db5f7b7e9fb1e7302a Mon Sep 17 00:00:00 2001
From: Quang Dao <qvd@andrew.cmu.edu>
Date: Mon, 28 Sep 2026 17:24:44 -0400
Subject: [PATCH 1/2] Prove public RAM output constraint (26)

Execution preserves the device layout and both advice buffers
(JoltIOSetupFrame.execInstr_rule, finalTraceState_ioSame). With the
Rust-enforced JoltIOLayout.Valid and JoltIOState.AdviceFits premises on the
initial device, the honest final RAM word equals the public I/O word on the
public interval.
---
 JoltConstraints/Constraints/IOSetupFrame.lean | 249 ++++++++++++++++++
 .../Constraints/RamOutputEqPublicIo.lean      |  98 ++++++-
 JoltConstraints/Constraints/RamReadData.lean  |  34 ++-
 JoltConstraints/constraints.md                |  15 +-
 JoltConstraints/model_review.md               |   1 -
 5 files changed, 382 insertions(+), 15 deletions(-)
 create mode 100644 JoltConstraints/Constraints/IOSetupFrame.lean

diff --git a/JoltConstraints/Constraints/IOSetupFrame.lean b/JoltConstraints/Constraints/IOSetupFrame.lean
new file mode 100644
index 0000000..82a4489
--- /dev/null
+++ b/JoltConstraints/Constraints/IOSetupFrame.lean
@@ -0,0 +1,249 @@
+import JoltConstraints.Constraints.RamReadData
+
+/-!
+Execution never changes the device fields fixed when Rust builds its emulator:
+the memory layout and both advice buffers. Sail steps do not touch the device,
+device stores only change `outputs` and `panic`, and HostIO only appends to the
+advice tape. The trace-level result carries this from the program's initial
+state to the final recorded state.
+-/
+
+set_option autoImplicit false
+
+open Sail PreSail LeanRV64D.Functions
+
+namespace JoltIOSetupFrame
+
+open JoltISA
+
+/-- The device fields that Rust fixes in `create_emulator` and never updates.
+Rust: https://github.com/a16z/jolt/blob/754fc88214936801a7d8a2260d9fc73478be4cbd/tracer/src/lib.rs#L401-L404 -/
+def Same (a b : JoltIOState) : Prop :=
+  b.layout = a.layout ∧ b.trustedAdvice = a.trustedAdvice ∧
+    b.untrustedAdvice = a.untrustedAdvice
+
+theorem Same.refl (a : JoltIOState) : Same a a := ⟨rfl, rfl, rfl⟩
+
+theorem Same.trans {a b c : JoltIOState} (hab : Same a b) (hbc : Same b c) : Same a c :=
+  ⟨hbc.1.trans hab.1, hbc.2.1.trans hab.2.1, hbc.2.2.trans hab.2.2⟩
+
+def Preserves {α : Type} (m : JoltMonad α) : Prop :=
+  ∀ (s t : SailJoltState) (v : α), m s = .ok v t → Same s.io t.io
+
+theorem pure_rule {α : Type} (v : α) : Preserves (pure v) := by
+  intro s t x h
+  cases h
+  exact Same.refl _
+
+theorem bind_rule {α β : Type} {m : JoltMonad α} {f : α → JoltMonad β}
+    (hm : Preserves m) (hf : ∀ x, Preserves (f x)) : Preserves (m >>= f) := by
+  intro s t v h
+  cases hr : m s with
+  | error e s' => simp only [bind, EStateM.bind, hr] at h; cases h
+  | ok x s' =>
+    simp only [bind, EStateM.bind, hr] at h
+    exact (hm s s' x hr).trans (hf x s' t v h)
+
+theorem lift_rule {α : Type} (m : SailM α) : Preserves (liftSail m) := by
+  intro s t v h
+  cases hr : m s.sail with
+  | error e s' => simp only [liftSail, hr] at h; cases h
+  | ok x s' =>
+    simp only [liftSail, hr] at h
+    cases h
+    exact Same.refl _
+
+theorem throw_rule {α : Type} (e : Error exception) :
+    Preserves (throw e : JoltMonad α) := by
+  intro s t x h
+  cases h
+
+theorem get_rule : Preserves (get : JoltMonad SailJoltState) := by
+  intro s t x h
+  cases h
+  exact Same.refl _
+
+theorem modify_rule (f : SailJoltState → SailJoltState)
+    (hf : ∀ s, (f s).io = s.io) : Preserves (modify f : JoltMonad Unit) := by
+  intro s t x h
+  cases h
+  rw [hf s]
+  exact Same.refl _
+
+theorem read_rule (src : Src) : Preserves (readSrc src) := by
+  cases src with
+  | vreg vr =>
+    intro s t v h
+    simp only [readSrc, readVReg, bind, EStateM.bind, get, getThe, MonadStateOf.get,
+      EStateM.get, pure, EStateM.pure] at h
+    cases h
+    exact Same.refl _
+  | xreg rs => exact lift_rule _
+
+theorem write_rule (dst : Dst) (value : BitVec 64) : Preserves (writeDst dst value) := by
+  cases dst with
+  | vreg vr =>
+    by_cases hw : vr.toNat < 32
+    · simp only [writeDst, writeVReg, hw, ↓reduceIte]
+      exact throw_rule _
+    · simp only [writeDst, writeVReg, hw, ↓reduceIte]
+      exact modify_rule _ (fun _ => rfl)
+  | xreg rd => exact lift_rule _
+
+theorem storeDeviceByte_same (io io' : JoltIOState) (address : Nat) (value : BitVec 8)
+    (h : storeDeviceByte? io address value = some io') : Same io io' := by
+  unfold storeDeviceByte? at h
+  split_ifs at h <;> cases h <;> exact ⟨rfl, rfl, rfl⟩
+
+theorem storeDeviceWord_same (io io' : JoltIOState) (address value : BitVec 64)
+    (h : storeDeviceWord? io address value = some io') : Same io io' := by
+  unfold storeDeviceWord? at h
+  suffices hfold : ∀ (l : List Nat) (start : Option JoltIOState),
+      (∀ d, start = some d → Same io d) →
+      ∀ d, l.foldl (fun current k => current.bind fun device =>
+        storeDeviceByte? device (address.toNat + k) (value.extractLsb' (8 * k) 8)) start =
+          some d → Same io d from
+    hfold _ _ (fun d hd => by cases hd; exact Same.refl _) _ h
+  intro l
+  induction l with
+  | nil => intro start hstart d hd; exact hstart d hd
+  | cons k l ih =>
+    intro start hstart d hd
+    refine ih _ ?_ d hd
+    intro d' hd'
+    cases hs : start with
+    | none => rw [hs] at hd'; cases hd'
+    | some e =>
+      rw [hs] at hd'
+      exact (hstart e hs).trans (storeDeviceByte_same _ _ _ _ hd')
+
+theorem readMemoryWord_rule (address : BitVec 64) :
+    Preserves (readMemoryWord address) := by
+  intro s t v h
+  unfold readMemoryWord at h
+  split_ifs at h
+  · split at h <;> (cases h; exact Same.refl _)
+  · exact lift_rule _ s t v h
+
+theorem writeMemoryWord_rule (address value : BitVec 64) :
+    Preserves (writeMemoryWord address value) := by
+  intro s t v h
+  unfold writeMemoryWord at h
+  split_ifs at h
+  · split at h
+    · rename_i io hio
+      cases h
+      exact storeDeviceWord_same _ _ _ _ hio
+    · cases h
+      exact Same.refl _
+  · exact lift_rule _ s t v h
+
+theorem readMemoryByte_rule (address : BitVec 64) :
+    Preserves (readMemoryByte address) := by
+  intro s t v h
+  unfold readMemoryByte at h
+  dsimp only at h
+  split_ifs at h
+  · cases hb : deviceByte? s.io address.toNat with
+    | none => simp only [hb] at h; cases h
+    | some byte => simp only [hb] at h; cases h; exact Same.refl _
+  · exact lift_rule _ s t v h
+
+theorem readHostBytes_rule
+    (overflowChecks incrementAfterLast : Bool) {width : Nat}
+    (pointer : BitVec width) (n : Nat) (bytes : Array (BitVec 8)) :
+    Preserves (readHostBytes readMemoryByte overflowChecks incrementAfterLast pointer n bytes) := by
+  induction n generalizing pointer bytes with
+  | zero => exact pure_rule _
+  | succ n ih =>
+    dsimp only [readHostBytes]
+    refine bind_rule (readMemoryByte_rule _) (fun result => ?_)
+    cases result with
+    | Err e => exact pure_rule _
+    | Ok byte =>
+      split_ifs with h
+      · exact bind_rule (throw_rule _) (fun _ => ih _ _)
+      · exact bind_rule (pure_rule _) (fun _ => ih _ _)
+
+theorem execHostIO_rule : Preserves execHostIO := by
+  unfold execHostIO execHostIOWith
+  refine bind_rule get_rule (fun config => ?_)
+  dsimp only
+  split
+  · exact pure_rule _
+  · refine bind_rule (pure_rule _) (fun _ => ?_)
+    refine bind_rule (read_rule _) (fun callId => ?_)
+    repeat' first
+      | exact readHostBytes_rule _ _ _ _ _
+      | exact read_rule _
+      | exact pure_rule _
+      | exact throw_rule _
+      | exact modify_rule _ (fun _ => rfl)
+      | split
+      | refine bind_rule ?_ (fun x => ?_)
+
+macro "jolt_io_setup_auto" : tactic => `(tactic|
+  repeat' first
+  | exact read_rule _
+  | exact write_rule _ _
+  | exact pure_rule _
+  | exact throw_rule _
+  | exact get_rule
+  | exact lift_rule _
+  | exact readMemoryWord_rule _
+  | exact writeMemoryWord_rule _ _
+  | exact execHostIO_rule
+  | split
+  | refine bind_rule ?_ (fun x => ?_))
+
+/-- Every Jolt ISA instruction preserves the device setup fields. -/
+theorem execInstr_rule (instr : Instr) : Preserves (execInstr instr) := by
+  cases instr
+  case VirtualAdviceLoad dst byteCount =>
+    intro s t v h
+    simp only [execInstr] at h
+    cases hr : readAdviceTape s.adviceTape byteCount with
+    | none => simp only [hr] at h; cases h
+    | some pair =>
+      obtain ⟨value, tape⟩ := pair
+      simp only [hr] at h
+      exact (bind_rule (write_rule dst value) (fun _ => pure_rule _))
+        { s with adviceTape := tape } t v h
+  all_goals simp only [execInstr]
+  all_goals jolt_io_setup_auto
+
+end JoltIOSetupFrame
+
+namespace JoltConstraints
+
+open JoltIOSetupFrame
+
+/-- Every recorded pre-state has the program's initial device setup. -/
+theorem trace_preState_ioSame {program : JoltProgram} (trace : JoltTrace program)
+    (i : Nat) (hi : i < trace.rows.size) :
+    Same program.initialState.io (getElem trace.rows i hi).preState.io := by
+  induction i with
+  | zero =>
+    rw [trace.startsAtInitial (by omega)]
+    exact Same.refl _
+  | succ i ih =>
+    have hprev := ih (by omega)
+    have hexec := execInstr_rule _ _ _ _ (getElem trace.rows i (by omega)).executes
+    have hlink := trace.linked i (by omega) hi
+    dsimp only at hlink
+    rw [hlink]
+    split
+    · exact hprev.trans hexec
+    · exact hprev.trans hexec
+
+/-- The final recorded state has the program's initial device setup. -/
+theorem finalTraceState_ioSame {program : JoltProgram} (trace : JoltTrace program) :
+    Same program.initialState.io (HonestWitness.finalTraceState trace).io := by
+  unfold HonestWitness.finalTraceState
+  split
+  · rename_i nonempty
+    exact (trace_preState_ioSame trace _ _).trans
+      (execInstr_rule _ _ _ _ (getElem trace.rows (trace.rows.size - 1) _).executes)
+  · exact Same.refl _
+
+end JoltConstraints
diff --git a/JoltConstraints/Constraints/RamOutputEqPublicIo.lean b/JoltConstraints/Constraints/RamOutputEqPublicIo.lean
index 68f424e..fddc439 100644
--- a/JoltConstraints/Constraints/RamOutputEqPublicIo.lean
+++ b/JoltConstraints/Constraints/RamOutputEqPublicIo.lean
@@ -1,4 +1,4 @@
-import JoltConstraints.Constraints.RamReadData
+import JoltConstraints.Constraints.IOSetupFrame
 
 set_option autoImplicit false
 
@@ -15,19 +15,103 @@ def ramOutputEqPublicIo {F : Type} [Field F] {params : WitnessParams}
     ramPublicIoMask io address.val *
       (witness.RamValFinal address - ((ramPublicIoWord io address.val).toNat : F)) = 0
 
-/-- Completeness target for the honest witness; proof pending.
-FIXME (translation boundary): the honest public output is taken from the final
-recorded state, but the Lean model does not yet enforce Rust's valid,
-nonoverlapping layout and buffer bounds. Audit that boundary before attempting
-this theorem; do not restrict Rust-valid executions to make it hold. -/
+/-- An advice overlay whose buffer ends at or below `input_start` leaves every
+word from the input's first remapped word onward unchanged. -/
+theorem overlayRamBytes_advice_above_input (layout : JoltIOLayout) (valid : layout.Valid)
+    (start : BitVec 64) (bytes : Array (BitVec 8))
+    (startAligned : start.toNat % 8 = 0)
+    (startLow : ramLowestAddress layout ≤ start.toNat)
+    (fits : start.toNat + bytes.size ≤ layout.input.1.toNat)
+    (address : Nat)
+    (above : (layout.input.1.toNat - ramLowestAddress layout) / 8 ≤ address)
+    (previous : BitVec 64) :
+    HonestWitness.overlayRamBytes layout start bytes address previous = previous := by
+  have lowestAligned : ramLowestAddress layout % 8 = 0 := by
+    have := valid.trustedAdviceAligned
+    have := valid.untrustedAdviceAligned
+    unfold ramLowestAddress
+    omega
+  have inputAligned := valid.inputAligned
+  unfold ramLowestAddress at startLow above lowestAligned
+  unfold HonestWitness.overlayRamBytes HonestWitness.remapRamAddress
+  dsimp only
+  by_cases hnone : start.toNat = 0 ∨
+      start.toNat < min layout.trustedAdvice.1.toNat layout.untrustedAdvice.1.toNat
+  · rw [if_pos hnone]
+  · rw [if_neg hnone]
+    dsimp only
+    rw [if_neg]
+    omega
+
+/-- On the public I/O interval, the honest final RAM word is the public I/O word.
+Below `RAM_START_ADDRESS` the RAM image is zero, and both advice overlays end
+before the input's first word, so only the public overlays remain. -/
+theorem finalRamWord_eq_ramPublicIoWord {program : JoltProgram} (trace : JoltTrace program)
+    (layoutValid : program.initialState.io.layout.Valid)
+    (adviceFits : program.initialState.io.AdviceFits)
+    (address : Nat)
+    (lower : (program.initialState.io.layout.input.1.toNat -
+      ramLowestAddress program.initialState.io.layout) / 8 ≤ address)
+    (upper : address <
+      (JoltISA.ramStartAddress - ramLowestAddress program.initialState.io.layout) / 8) :
+    HonestWitness.finalRamWord trace address =
+      ramPublicIoWord (HonestWitness.finalTraceState trace).io address := by
+  obtain ⟨hlayout, htrusted, huntrusted⟩ := finalTraceState_ioSame trace
+  have trustedFits := adviceFits.trustedAdvice
+  have untrustedFits := adviceFits.untrustedAdvice
+  have := layoutValid.trustedAdviceOrdered
+  have := layoutValid.untrustedAdviceOrdered
+  have := layoutValid.trustedAdviceBelowInput
+  have := layoutValid.untrustedAdviceBelowInput
+  have hram : ¬ JoltISA.ramStartAddress ≤
+      min program.initialState.io.layout.trustedAdvice.1.toNat
+        program.initialState.io.layout.untrustedAdvice.1.toNat + 8 * address := by
+    unfold ramLowestAddress at upper
+    omega
+  have htrustedOverlay := overlayRamBytes_advice_above_input _ layoutValid
+    program.initialState.io.layout.trustedAdvice.1 program.initialState.io.trustedAdvice
+    layoutValid.trustedAdviceAligned (by unfold ramLowestAddress; omega) (by omega)
+    address lower
+  have huntrustedOverlay := overlayRamBytes_advice_above_input _ layoutValid
+    program.initialState.io.layout.untrustedAdvice.1 program.initialState.io.untrustedAdvice
+    layoutValid.untrustedAdviceAligned (by unfold ramLowestAddress; omega) (by omega)
+    address lower
+  unfold HonestWitness.finalRamWord ramPublicIoWord
+  dsimp only
+  rw [hlayout, htrusted, huntrusted, if_neg hram, htrustedOverlay, huntrustedOverlay]
+
+/-- Completeness of constraint (26) for the honest witness.
+
+The final device is the last recorded post-state's device. Execution preserves
+the layout and both advice buffers (`finalTraceState_ioSame`), so the final
+RAM image and the public I/O array share the input, output, panic, and
+termination overlays. They differ only below the input: the zero RAM image
+below `RAM_START_ADDRESS` and the advice buffers. The two premises below are
+exactly the Rust-enforced facts that keep the advice buffers out of the public
+interval; see their docstrings for the Rust source. Output growth needs no
+premise here: both sides overlay the same final output buffer. -/
 theorem honestWitness_ramOutputEqPublicIo
     {F : Type} [Field F] (params : WitnessParams)
     {program : JoltProgram} (trace : JoltTrace program)
     (ramFits : params.RamFits trace)
     (traceFits : params.ProverPaddedFor trace.rows.size)
     (bytecodeDomain : params.BytecodeDomainFor program.expandedBytecode.size)
+    (layoutValid : program.initialState.io.layout.Valid)
+    (adviceFits : program.initialState.io.AdviceFits)
     : ramOutputEqPublicIo (HonestWitness.finalTraceState trace).io
       (JoltProgram.honestWitness (F := F) params trace ramFits traceFits bytecodeDomain) := by
-  sorry
+  intro address
+  change ramPublicIoMask (HonestWitness.finalTraceState trace).io address.val *
+    (HonestWitness.RamValFinal (F := F) params trace address -
+      ((ramPublicIoWord (HonestWitness.finalTraceState trace).io address.val).toNat : F)) = 0
+  have hlayout := (finalTraceState_ioSame trace).1
+  unfold ramPublicIoMask
+  dsimp only
+  rw [hlayout]
+  split_ifs with hmask
+  · rw [HonestWitness.RamValFinal,
+      finalRamWord_eq_ramPublicIoWord trace layoutValid adviceFits address.val hmask.1 hmask.2,
+      sub_self, mul_zero]
+  · rw [zero_mul]
 
 end JoltConstraints
diff --git a/JoltConstraints/Constraints/RamReadData.lean b/JoltConstraints/Constraints/RamReadData.lean
index 48f9279..4202b1a 100644
--- a/JoltConstraints/Constraints/RamReadData.lean
+++ b/JoltConstraints/Constraints/RamReadData.lean
@@ -12,6 +12,38 @@ Rust: https://github.com/abiswas3/jolt/tree/main/common/src/jolt_device.rs#L491-
 def ramLowestAddress (layout : JoltIOLayout) : Nat :=
   min layout.trustedAdvice.1.toNat layout.untrustedAdvice.1.toNat
 
+/-- The part of Rust's memory-layout invariant used so far: both advice regions
+are well formed and end at or below `input_start`, and the advice and input
+starts are 8-byte aligned. Extend this structure with further Rust-enforced
+layout facts as later theorems need them.
+
+Rust constructs every layout with `MemoryLayout::new`: the advice sizes are
+rounded up to multiples of 8; the lower advice region starts at
+`RAM_START_ADDRESS - io_bytes`, where `io_bytes` is a multiple of 8; the other
+advice region starts at the first one's end; and `input_start` is the larger
+advice end. Every addition is checked, so each end is at least its start.
+Rust: https://github.com/a16z/jolt/blob/754fc88214936801a7d8a2260d9fc73478be4cbd/common/src/jolt_device.rs#L370-L438 -/
+structure _root_.JoltIOLayout.Valid (layout : JoltIOLayout) : Prop where
+  trustedAdviceAligned : layout.trustedAdvice.1.toNat % 8 = 0
+  untrustedAdviceAligned : layout.untrustedAdvice.1.toNat % 8 = 0
+  inputAligned : layout.input.1.toNat % 8 = 0
+  trustedAdviceOrdered : layout.trustedAdvice.1.toNat ≤ layout.trustedAdvice.2.toNat
+  untrustedAdviceOrdered : layout.untrustedAdvice.1.toNat ≤ layout.untrustedAdvice.2.toNat
+  trustedAdviceBelowInput : layout.trustedAdvice.2.toNat ≤ layout.input.1.toNat
+  untrustedAdviceBelowInput : layout.untrustedAdvice.2.toNat ≤ layout.input.1.toNat
+
+/-- Each advice buffer fits its layout region. Rust's `create_emulator` rejects
+longer advice before building the device, and `MemoryLayout::new` sizes each
+region to the configured maximum rounded up to a multiple of 8.
+Rust: https://github.com/a16z/jolt/blob/754fc88214936801a7d8a2260d9fc73478be4cbd/tracer/src/lib.rs#L382-L393
+and https://github.com/a16z/jolt/blob/754fc88214936801a7d8a2260d9fc73478be4cbd/common/src/jolt_device.rs#L370-L371 -/
+structure _root_.JoltIOState.AdviceFits (io : JoltIOState) : Prop where
+  trustedAdvice :
+    io.trustedAdvice.size ≤ io.layout.trustedAdvice.2.toNat - io.layout.trustedAdvice.1.toNat
+  untrustedAdvice :
+    io.untrustedAdvice.size ≤
+      io.layout.untrustedAdvice.2.toNat - io.layout.untrustedAdvice.1.toNat
+
 /-- The initial RAM image, including public inputs and both advice buffers.
 Advice words are execution inputs, not additional public constants. Reuse the
 existing image encoding; this function does not execute instructions.
@@ -22,7 +54,7 @@ noncomputable def ramInitialValue {F : Type} [Field F]
 
 /-- Public I/O mask: remapped words from input_start up to RAM_START_ADDRESS,
 excluding RAM_START_ADDRESS. As in Rust preprocessing, the layout must be valid;
-layout admissibility is a separate completeness obligation.
+completeness theorems assume the relevant part as `JoltIOLayout.Valid`.
 Rust: https://github.com/abiswas3/jolt/tree/main/crates/jolt-program/src/preprocess/public_io.rs#L20-L25 -/
 def ramPublicIoMask {F : Type} [Field F] (io : JoltIOState) (address : Nat) : F :=
   let lowest := ramLowestAddress io.layout
diff --git a/JoltConstraints/constraints.md b/JoltConstraints/constraints.md
index 28355eb..d12a9e3 100644
--- a/JoltConstraints/constraints.md
+++ b/JoltConstraints/constraints.md
@@ -8,7 +8,7 @@ unfinished proof or correspondence work, and `FIXME:` for a confirmed issue.
 This tracks proof status under each theorem's stated premises; it does not by
 itself establish that all Rust executions satisfy those premises. The Lean
 source and `#print axioms` were checked for the original 62 numbered targets.
-The current checklist has 56 proved targets, three `TODO:` targets, and three
+The current checklist has 57 proved targets, two `TODO:` targets, and three
 `FIXME:` targets.
 
 The `FIXME:` targets are (01), blocked by the confirmed
@@ -17,7 +17,7 @@ whose [taken self-branch counterexample](../bug-report/self-branch.md) leaves
 its unrestricted target as a statement rather than a theorem; and (37),
 blocked by the confirmed
 [termination-word RAM history bug](../bug-report/ram-val-termination/README.md).
-The three `TODO:` targets are (26), (38), and (39); they still need Rust–Lean
+The two `TODO:` targets are (38) and (39); they still need Rust–Lean
 correspondence checks.
 
 Constraint (12) has a proved conditional completeness theorem requiring
@@ -33,7 +33,10 @@ validity conditions.
 The completeness theorem for constraint (22) explicitly requires at least one padding cycle, as Rust's
 trace-length calculation guarantees. The completeness theorem for (58) requires
 at least one RAM chunk. The register targets (34)–(36) and (42) require zero
-initial registers.
+initial registers. Constraint (26) requires the initial device to satisfy
+`JoltIOLayout.Valid` (aligned advice regions ending at or below `input_start`)
+and `JoltIOState.AdviceFits` (each advice buffer fits its region); Rust's
+`MemoryLayout::new` and `create_emulator` enforce both.
 
 Equations (43)–(47) were rechecked against Rust commit `e012da54c3bb26a6436b5ca74e86c19bb39695ad`. Their honest-witness targets now require the exact Rust bytecode domain, including the leading no-op and power-of-two padding.
 
@@ -41,8 +44,8 @@ The remaining equations (23)–(26), (37)–(38), (40)–(41), (48)–(53), and
 were also checked against Rust commit `e012da54c3bb26a6436b5ca74e86c19bb39695ad`.
 This checklist covers the base RV64 relations; optional `akita` relations,
 including its extra instruction-address canonicality condition, are outside it.
-The final RAM and public-I/O completeness targets still need memory-history,
-layout, and termination assumptions. Constraint (53) takes the public entry slot
+The final-RAM completeness target (38) still needs memory-history and
+termination assumptions. Constraint (53) takes the public entry slot
 explicitly and requires the trace to start there. Constraint (50) selects the
 destination recorded in the final bytecode row, including x0. The
 [`JoltTraceRow` load-capture condition](trace.lean) separately requires a load's
@@ -190,7 +193,7 @@ Flag names mean the corresponding Rust `OpFlags(CircuitFlags::…)` or `Instruct
 
 ## RamOutputCheck — stage 2
 
-- [ ] (26) TODO: [Public RAM output](Constraints/RamOutputEqPublicIo.lean)
+- [x] (26) DONE: [Public RAM output](Constraints/RamOutputEqPublicIo.lean)
 
 [Rust: constraint](https://github.com/abiswas3/jolt/blob/e012da54c3bb26a6436b5ca74e86c19bb39695ad/crates/jolt-claims/src/protocols/jolt/relations/ram/output_check.rs#L115); [public arrays](https://github.com/abiswas3/jolt/blob/e012da54c3bb26a6436b5ca74e86c19bb39695ad/crates/jolt-program/src/preprocess/public_io.rs#L20).
 
diff --git a/JoltConstraints/model_review.md b/JoltConstraints/model_review.md
index f536fb2..8d4f429 100644
--- a/JoltConstraints/model_review.md
+++ b/JoltConstraints/model_review.md
@@ -221,7 +221,6 @@ are **deferred work or documented modeling choices**, not established proofs.
 | [LookupOutputEqInstructionReadRaf.lean](Constraints/LookupOutputEqInstructionReadRaf.lean), `FIXME` | Connect each now-defined fixed table entry to `HonestWitness.rowLookupOutput` for execution rows. |
 | [RamValEqInitialPlusPrefixRamInc.lean](Constraints/RamValEqInitialPlusPrefixRamInc.lean), `FIXME` | Relate captured RAM reads to initialized memory and prefix RAM history. |
 | [RamValFinalEqInitialPlusRamInc.lean](Constraints/RamValFinalEqInitialPlusRamInc.lean), `FIXME` | Establish Rust memory-history and terminal-state correspondence. |
-| [RamOutputEqPublicIo.lean](Constraints/RamOutputEqPublicIo.lean), `FIXME` | Relate Rust's final public output to the Lean witness. |
 | [RegisterAccess.lean](../JoltBytecode/JoltISA/RegisterAccess.lean), `WARNING` | Establish the source register range guard or proof noted by the existing comment. |
 | [RiscvInstruction.lean](../JoltBytecode/RiscvInstruction.lean), six `WARNING`s | Wire equivalence for ECALL, EBREAK, LR_W, SC_W, LR_D, and SC_D; their current statement branches are `False`. |
 | [Semantics.lean](../JoltBytecode/JoltISA/Semantics.lean), `WARNING` | Rust logs a warning at this execution path; logs are absent from Lean state. Revisit if logs become observable in the claimed correspondence. |

From 1a2e4bd0dc2aa2450a2cc8aaceca0c8d6b57f370 Mon Sep 17 00:00:00 2001
From: Quang Dao <qvd@andrew.cmu.edu>
Date: Mon, 28 Sep 2026 17:50:26 -0400
Subject: [PATCH 2/2] refactor(constraints): weaken (26) premise and derive it
 from Rust's layout

Replace JoltIOLayout.Valid and JoltIOState.AdviceFits with the single
premise the proof uses, JoltIOState.AdviceBelowInput: each advice buffer
ends at or below input_start, and input_start is word-aligned relative
to the lowest RAM address. Region ends and absolute alignment are no
longer assumed.

Add a transcription of MemoryLayout::new up to input_start and prove
AdviceBelowInput.of_memoryLayout: every device laid out by Rust whose
advice passes create_emulator's length checks satisfies the premise.
---
 JoltConstraints/Constraints/MemoryLayout.lean | 136 ++++++++++++++++++
 .../Constraints/RamOutputEqPublicIo.lean      |  49 +++----
 JoltConstraints/Constraints/RamReadData.lean  |  45 ++----
 JoltConstraints/constraints.md                |   8 +-
 4 files changed, 172 insertions(+), 66 deletions(-)
 create mode 100644 JoltConstraints/Constraints/MemoryLayout.lean

diff --git a/JoltConstraints/Constraints/MemoryLayout.lean b/JoltConstraints/Constraints/MemoryLayout.lean
new file mode 100644
index 0000000..f8c3788
--- /dev/null
+++ b/JoltConstraints/Constraints/MemoryLayout.lean
@@ -0,0 +1,136 @@
+import JoltConstraints.Constraints.RamReadData
+
+/-!
+Rust's `MemoryLayout::new`, restricted to the advice and input regions, and a
+proof that every device it lays out satisfies `JoltIOState.AdviceBelowInput`.
+
+Rust: https://github.com/a16z/jolt/blob/754fc88214936801a7d8a2260d9fc73478be4cbd/common/src/jolt_device.rs#L346-L438
+
+Arithmetic is on `Nat`. Each Rust `checked_*` call followed by `expect` becomes
+a guard that returns `none` where Rust panics. Everything after `input_start`
+in `new`, and its two power-of-two assertions on the advice sizes, only add
+further panics and leave these fields unchanged; they are omitted, so
+`adviceInputLayout` succeeds on at least every configuration Rust accepts.
+-/
+
+set_option autoImplicit false
+
+namespace JoltConstraints.RustMemoryLayout
+
+/-- The `MemoryConfig` fields that determine the advice and input regions. -/
+structure MemoryConfig where
+  maxTrustedAdviceSize : Nat
+  maxUntrustedAdviceSize : Nat
+  maxInputSize : Nat
+  maxOutputSize : Nat
+
+/-- Advice and input placement computed by `MemoryLayout::new`. -/
+structure AdviceInputLayout where
+  trustedAdviceStart : Nat
+  trustedAdviceEnd : Nat
+  untrustedAdviceStart : Nat
+  untrustedAdviceEnd : Nat
+  inputStart : Nat
+
+/-- Rust `u64::checked_add`. -/
+def checkedAdd (a b : Nat) : Option Nat :=
+  if a + b < 2 ^ 64 then some (a + b) else none
+
+/-- Rust `align_up(val, 8)`, which panics on overflow. -/
+def alignUp8 (val : Nat) : Option Nat :=
+  if val % 8 = 0 then some val else checkedAdd val (8 - val % 8)
+
+/-- `MemoryLayout::new` up to `input_start`. The larger (or equal) advice region
+goes first, at `RAM_START_ADDRESS - io_bytes`; the other starts where it ends;
+`input_start` is the larger end. -/
+def adviceInputLayout (config : MemoryConfig) : Option AdviceInputLayout := do
+  let trusted ← alignUp8 config.maxTrustedAdviceSize
+  let untrusted ← alignUp8 config.maxUntrustedAdviceSize
+  let input ← alignUp8 config.maxInputSize
+  let output ← alignUp8 config.maxOutputSize
+  let ioRegionBytes ← (checkedAdd input trusted).bind fun s =>
+    (checkedAdd s untrusted).bind fun s => (checkedAdd s output).bind fun s => checkedAdd s 16
+  let ioBytes := (ioRegionBytes / 8).nextPowerOfTwo * 8
+  if 2 ^ 64 ≤ ioBytes ∨ JoltISA.ramStartAddress < ioBytes then none else
+  let first := JoltISA.ramStartAddress - ioBytes
+  if untrusted ≤ trusted then
+    let trustedEnd ← checkedAdd first trusted
+    let untrustedEnd ← checkedAdd trustedEnd untrusted
+    pure { trustedAdviceStart := first, trustedAdviceEnd := trustedEnd,
+           untrustedAdviceStart := trustedEnd, untrustedAdviceEnd := untrustedEnd,
+           inputStart := max untrustedEnd trustedEnd }
+  else
+    let untrustedEnd ← checkedAdd first untrusted
+    let trustedEnd ← checkedAdd untrustedEnd trusted
+    pure { trustedAdviceStart := untrustedEnd, trustedAdviceEnd := trustedEnd,
+           untrustedAdviceStart := first, untrustedAdviceEnd := untrustedEnd,
+           inputStart := max untrustedEnd trustedEnd }
+
+theorem checkedAdd_eq_some {a b c : Nat} (h : checkedAdd a b = some c) : c = a + b := by
+  unfold checkedAdd at h
+  split at h <;> simp_all
+
+theorem alignUp8_eq_some {val aligned : Nat} (h : alignUp8 val = some aligned) :
+    val ≤ aligned ∧ aligned % 8 = 0 := by
+  unfold alignUp8 at h
+  split at h
+  · simp_all
+  · have := checkedAdd_eq_some h
+    omega
+
+/-- The arithmetic facts about a successful layout: each advice region has its
+aligned size, the two regions are adjacent, and `input_start` is the larger end. -/
+theorem adviceInputLayout_spec {config : MemoryConfig} {layout : AdviceInputLayout}
+    (h : adviceInputLayout config = some layout) :
+    ∃ trusted untrusted,
+      config.maxTrustedAdviceSize ≤ trusted ∧ trusted % 8 = 0 ∧
+      config.maxUntrustedAdviceSize ≤ untrusted ∧ untrusted % 8 = 0 ∧
+      layout.trustedAdviceEnd = layout.trustedAdviceStart + trusted ∧
+      layout.untrustedAdviceEnd = layout.untrustedAdviceStart + untrusted ∧
+      (layout.untrustedAdviceStart = layout.trustedAdviceEnd ∨
+        layout.trustedAdviceStart = layout.untrustedAdviceEnd) ∧
+      layout.inputStart = max layout.untrustedAdviceEnd layout.trustedAdviceEnd := by
+  unfold adviceInputLayout at h
+  simp only [Option.bind_eq_bind, Option.bind_eq_some_iff] at h
+  obtain ⟨trusted, htrusted, untrusted, huntrusted, _, _, _, _, _, _, h⟩ := h
+  obtain ⟨hT, hT8⟩ := alignUp8_eq_some htrusted
+  obtain ⟨hU, hU8⟩ := alignUp8_eq_some huntrusted
+  refine ⟨trusted, untrusted, hT, hT8, hU, hU8, ?_⟩
+  split at h
+  · simp at h
+  split at h
+  · simp only [Option.bind_eq_some_iff, Option.pure_def, Option.some.injEq] at h
+    obtain ⟨trustedEnd, htEnd, untrustedEnd, huEnd, rfl⟩ := h
+    have := checkedAdd_eq_some htEnd
+    have := checkedAdd_eq_some huEnd
+    simp only
+    simp only [true_or, and_true]
+    omega
+  · simp only [Option.bind_eq_some_iff, Option.pure_def, Option.some.injEq] at h
+    obtain ⟨untrustedEnd, huEnd, trustedEnd, htEnd, rfl⟩ := h
+    have := checkedAdd_eq_some htEnd
+    have := checkedAdd_eq_some huEnd
+    simp only
+    simp only [or_true, and_true]
+    omega
+
+end JoltConstraints.RustMemoryLayout
+
+open JoltConstraints JoltConstraints.RustMemoryLayout in
+/-- Every device Rust builds satisfies `AdviceBelowInput`: its layout comes from
+`MemoryLayout::new`, and `create_emulator` rejects advice longer than the
+configured maximum before execution starts.
+Rust: https://github.com/a16z/jolt/blob/754fc88214936801a7d8a2260d9fc73478be4cbd/tracer/src/lib.rs#L382-L393 -/
+theorem JoltIOState.AdviceBelowInput.of_memoryLayout
+    (io : JoltIOState) (config : MemoryConfig) (layout : AdviceInputLayout)
+    (built : adviceInputLayout config = some layout)
+    (trustedStart : io.layout.trustedAdvice.1.toNat = layout.trustedAdviceStart)
+    (untrustedStart : io.layout.untrustedAdvice.1.toNat = layout.untrustedAdviceStart)
+    (inputStart : io.layout.input.1.toNat = layout.inputStart)
+    (trustedLength : io.trustedAdvice.size ≤ config.maxTrustedAdviceSize)
+    (untrustedLength : io.untrustedAdvice.size ≤ config.maxUntrustedAdviceSize) :
+    io.AdviceBelowInput := by
+  obtain ⟨trusted, untrusted, hT, hT8, hU, hU8, htEnd, huEnd, hadj, hinput⟩ :=
+    adviceInputLayout_spec built
+  refine ⟨?_, ?_, ?_⟩ <;>
+    simp only [ramLowestAddress, trustedStart, untrustedStart, inputStart] <;> omega
diff --git a/JoltConstraints/Constraints/RamOutputEqPublicIo.lean b/JoltConstraints/Constraints/RamOutputEqPublicIo.lean
index fddc439..58943ba 100644
--- a/JoltConstraints/Constraints/RamOutputEqPublicIo.lean
+++ b/JoltConstraints/Constraints/RamOutputEqPublicIo.lean
@@ -1,4 +1,5 @@
 import JoltConstraints.Constraints.IOSetupFrame
+import JoltConstraints.Constraints.MemoryLayout
 
 set_option autoImplicit false
 
@@ -15,24 +16,18 @@ def ramOutputEqPublicIo {F : Type} [Field F] {params : WitnessParams}
     ramPublicIoMask io address.val *
       (witness.RamValFinal address - ((ramPublicIoWord io address.val).toNat : F)) = 0
 
-/-- An advice overlay whose buffer ends at or below `input_start` leaves every
-word from the input's first remapped word onward unchanged. -/
-theorem overlayRamBytes_advice_above_input (layout : JoltIOLayout) (valid : layout.Valid)
+/-- An overlay whose bytes end at or below `input_start` leaves every word from
+the input's first remapped word onward unchanged. The overlay start need not be
+aligned: remapping rounds it down, which only moves the bytes lower. -/
+theorem overlayRamBytes_below_input (layout : JoltIOLayout)
     (start : BitVec 64) (bytes : Array (BitVec 8))
-    (startAligned : start.toNat % 8 = 0)
-    (startLow : ramLowestAddress layout ≤ start.toNat)
+    (inputWordAligned : (layout.input.1.toNat - ramLowestAddress layout) % 8 = 0)
     (fits : start.toNat + bytes.size ≤ layout.input.1.toNat)
     (address : Nat)
     (above : (layout.input.1.toNat - ramLowestAddress layout) / 8 ≤ address)
     (previous : BitVec 64) :
     HonestWitness.overlayRamBytes layout start bytes address previous = previous := by
-  have lowestAligned : ramLowestAddress layout % 8 = 0 := by
-    have := valid.trustedAdviceAligned
-    have := valid.untrustedAdviceAligned
-    unfold ramLowestAddress
-    omega
-  have inputAligned := valid.inputAligned
-  unfold ramLowestAddress at startLow above lowestAligned
+  unfold ramLowestAddress at inputWordAligned above
   unfold HonestWitness.overlayRamBytes HonestWitness.remapRamAddress
   dsimp only
   by_cases hnone : start.toNat = 0 ∨
@@ -47,8 +42,7 @@ theorem overlayRamBytes_advice_above_input (layout : JoltIOLayout) (valid : layo
 Below `RAM_START_ADDRESS` the RAM image is zero, and both advice overlays end
 before the input's first word, so only the public overlays remain. -/
 theorem finalRamWord_eq_ramPublicIoWord {program : JoltProgram} (trace : JoltTrace program)
-    (layoutValid : program.initialState.io.layout.Valid)
-    (adviceFits : program.initialState.io.AdviceFits)
+    (adviceBelowInput : program.initialState.io.AdviceBelowInput)
     (address : Nat)
     (lower : (program.initialState.io.layout.input.1.toNat -
       ramLowestAddress program.initialState.io.layout) / 8 ≤ address)
@@ -57,25 +51,17 @@ theorem finalRamWord_eq_ramPublicIoWord {program : JoltProgram} (trace : JoltTra
     HonestWitness.finalRamWord trace address =
       ramPublicIoWord (HonestWitness.finalTraceState trace).io address := by
   obtain ⟨hlayout, htrusted, huntrusted⟩ := finalTraceState_ioSame trace
-  have trustedFits := adviceFits.trustedAdvice
-  have untrustedFits := adviceFits.untrustedAdvice
-  have := layoutValid.trustedAdviceOrdered
-  have := layoutValid.untrustedAdviceOrdered
-  have := layoutValid.trustedAdviceBelowInput
-  have := layoutValid.untrustedAdviceBelowInput
   have hram : ¬ JoltISA.ramStartAddress ≤
       min program.initialState.io.layout.trustedAdvice.1.toNat
         program.initialState.io.layout.untrustedAdvice.1.toNat + 8 * address := by
     unfold ramLowestAddress at upper
     omega
-  have htrustedOverlay := overlayRamBytes_advice_above_input _ layoutValid
+  have htrustedOverlay := overlayRamBytes_below_input _
     program.initialState.io.layout.trustedAdvice.1 program.initialState.io.trustedAdvice
-    layoutValid.trustedAdviceAligned (by unfold ramLowestAddress; omega) (by omega)
-    address lower
-  have huntrustedOverlay := overlayRamBytes_advice_above_input _ layoutValid
+    adviceBelowInput.inputWordAligned adviceBelowInput.trustedAdviceBelowInput address lower
+  have huntrustedOverlay := overlayRamBytes_below_input _
     program.initialState.io.layout.untrustedAdvice.1 program.initialState.io.untrustedAdvice
-    layoutValid.untrustedAdviceAligned (by unfold ramLowestAddress; omega) (by omega)
-    address lower
+    adviceBelowInput.inputWordAligned adviceBelowInput.untrustedAdviceBelowInput address lower
   unfold HonestWitness.finalRamWord ramPublicIoWord
   dsimp only
   rw [hlayout, htrusted, huntrusted, if_neg hram, htrustedOverlay, huntrustedOverlay]
@@ -86,9 +72,9 @@ The final device is the last recorded post-state's device. Execution preserves
 the layout and both advice buffers (`finalTraceState_ioSame`), so the final
 RAM image and the public I/O array share the input, output, panic, and
 termination overlays. They differ only below the input: the zero RAM image
-below `RAM_START_ADDRESS` and the advice buffers. The two premises below are
-exactly the Rust-enforced facts that keep the advice buffers out of the public
-interval; see their docstrings for the Rust source. Output growth needs no
+below `RAM_START_ADDRESS` and the advice buffers. `adviceBelowInput` keeps the
+advice buffers out of the public interval; `AdviceBelowInput.of_memoryLayout`
+proves that every Rust-constructed device satisfies it. Output growth needs no
 premise here: both sides overlay the same final output buffer. -/
 theorem honestWitness_ramOutputEqPublicIo
     {F : Type} [Field F] (params : WitnessParams)
@@ -96,8 +82,7 @@ theorem honestWitness_ramOutputEqPublicIo
     (ramFits : params.RamFits trace)
     (traceFits : params.ProverPaddedFor trace.rows.size)
     (bytecodeDomain : params.BytecodeDomainFor program.expandedBytecode.size)
-    (layoutValid : program.initialState.io.layout.Valid)
-    (adviceFits : program.initialState.io.AdviceFits)
+    (adviceBelowInput : program.initialState.io.AdviceBelowInput)
     : ramOutputEqPublicIo (HonestWitness.finalTraceState trace).io
       (JoltProgram.honestWitness (F := F) params trace ramFits traceFits bytecodeDomain) := by
   intro address
@@ -110,7 +95,7 @@ theorem honestWitness_ramOutputEqPublicIo
   rw [hlayout]
   split_ifs with hmask
   · rw [HonestWitness.RamValFinal,
-      finalRamWord_eq_ramPublicIoWord trace layoutValid adviceFits address.val hmask.1 hmask.2,
+      finalRamWord_eq_ramPublicIoWord trace adviceBelowInput address.val hmask.1 hmask.2,
       sub_self, mul_zero]
   · rw [zero_mul]
 
diff --git a/JoltConstraints/Constraints/RamReadData.lean b/JoltConstraints/Constraints/RamReadData.lean
index 4202b1a..0cfd3e2 100644
--- a/JoltConstraints/Constraints/RamReadData.lean
+++ b/JoltConstraints/Constraints/RamReadData.lean
@@ -12,37 +12,20 @@ Rust: https://github.com/abiswas3/jolt/tree/main/common/src/jolt_device.rs#L491-
 def ramLowestAddress (layout : JoltIOLayout) : Nat :=
   min layout.trustedAdvice.1.toNat layout.untrustedAdvice.1.toNat
 
-/-- The part of Rust's memory-layout invariant used so far: both advice regions
-are well formed and end at or below `input_start`, and the advice and input
-starts are 8-byte aligned. Extend this structure with further Rust-enforced
-layout facts as later theorems need them.
+/-- Both advice buffers of a device lie below `input_start`, and `input_start`
+is a whole number of words above the lowest RAM address. These are the only
+layout facts the public-output constraint (26) needs: together they keep every
+advice byte out of the public I/O interval.
 
-Rust constructs every layout with `MemoryLayout::new`: the advice sizes are
-rounded up to multiples of 8; the lower advice region starts at
-`RAM_START_ADDRESS - io_bytes`, where `io_bytes` is a multiple of 8; the other
-advice region starts at the first one's end; and `input_start` is the larger
-advice end. Every addition is checked, so each end is at least its start.
-Rust: https://github.com/a16z/jolt/blob/754fc88214936801a7d8a2260d9fc73478be4cbd/common/src/jolt_device.rs#L370-L438 -/
-structure _root_.JoltIOLayout.Valid (layout : JoltIOLayout) : Prop where
-  trustedAdviceAligned : layout.trustedAdvice.1.toNat % 8 = 0
-  untrustedAdviceAligned : layout.untrustedAdvice.1.toNat % 8 = 0
-  inputAligned : layout.input.1.toNat % 8 = 0
-  trustedAdviceOrdered : layout.trustedAdvice.1.toNat ≤ layout.trustedAdvice.2.toNat
-  untrustedAdviceOrdered : layout.untrustedAdvice.1.toNat ≤ layout.untrustedAdvice.2.toNat
-  trustedAdviceBelowInput : layout.trustedAdvice.2.toNat ≤ layout.input.1.toNat
-  untrustedAdviceBelowInput : layout.untrustedAdvice.2.toNat ≤ layout.input.1.toNat
-
-/-- Each advice buffer fits its layout region. Rust's `create_emulator` rejects
-longer advice before building the device, and `MemoryLayout::new` sizes each
-region to the configured maximum rounded up to a multiple of 8.
-Rust: https://github.com/a16z/jolt/blob/754fc88214936801a7d8a2260d9fc73478be4cbd/tracer/src/lib.rs#L382-L393
-and https://github.com/a16z/jolt/blob/754fc88214936801a7d8a2260d9fc73478be4cbd/common/src/jolt_device.rs#L370-L371 -/
-structure _root_.JoltIOState.AdviceFits (io : JoltIOState) : Prop where
-  trustedAdvice :
-    io.trustedAdvice.size ≤ io.layout.trustedAdvice.2.toNat - io.layout.trustedAdvice.1.toNat
-  untrustedAdvice :
-    io.untrustedAdvice.size ≤
-      io.layout.untrustedAdvice.2.toNat - io.layout.untrustedAdvice.1.toNat
+Rust establishes them before execution starts:
+`JoltIOState.AdviceBelowInput.of_memoryLayout` derives them from Rust's
+`MemoryLayout::new` and the advice-length checks in `create_emulator`. -/
+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
 
 /-- The initial RAM image, including public inputs and both advice buffers.
 Advice words are execution inputs, not additional public constants. Reuse the
@@ -54,7 +37,7 @@ noncomputable def ramInitialValue {F : Type} [Field F]
 
 /-- Public I/O mask: remapped words from input_start up to RAM_START_ADDRESS,
 excluding RAM_START_ADDRESS. As in Rust preprocessing, the layout must be valid;
-completeness theorems assume the relevant part as `JoltIOLayout.Valid`.
+completeness theorems assume the relevant part as `JoltIOState.AdviceBelowInput`.
 Rust: https://github.com/abiswas3/jolt/tree/main/crates/jolt-program/src/preprocess/public_io.rs#L20-L25 -/
 def ramPublicIoMask {F : Type} [Field F] (io : JoltIOState) (address : Nat) : F :=
   let lowest := ramLowestAddress io.layout
diff --git a/JoltConstraints/constraints.md b/JoltConstraints/constraints.md
index d12a9e3..0e4cad1 100644
--- a/JoltConstraints/constraints.md
+++ b/JoltConstraints/constraints.md
@@ -34,9 +34,11 @@ The completeness theorem for constraint (22) explicitly requires at least one pa
 trace-length calculation guarantees. The completeness theorem for (58) requires
 at least one RAM chunk. The register targets (34)–(36) and (42) require zero
 initial registers. Constraint (26) requires the initial device to satisfy
-`JoltIOLayout.Valid` (aligned advice regions ending at or below `input_start`)
-and `JoltIOState.AdviceFits` (each advice buffer fits its region); Rust's
-`MemoryLayout::new` and `create_emulator` enforce both.
+`JoltIOState.AdviceBelowInput`: both advice buffers end at or below
+`input_start`, which is a whole number of words above the lowest RAM address.
+`JoltIOState.AdviceBelowInput.of_memoryLayout` proves this for every device
+laid out by Rust's `MemoryLayout::new` whose advice passes `create_emulator`'s
+length checks.
 
 Equations (43)–(47) were rechecked against Rust commit `e012da54c3bb26a6436b5ca74e86c19bb39695ad`. Their honest-witness targets now require the exact Rust bytecode domain, including the leading no-op and power-of-two padding.