This post collects some of the helper lemmas and definitions used across the proofs in this series.

stateAfterWrite

In Plain English

stateAfterWrite s rd val returns a new SailState identical to s except that register rd now holds val. It is a specification-level way of describing a register write — without going through the monadic wX_bits. It also guarantees that the only change in state is the write to rd. See wX_bits_eq_stateAfterWrite later.

noncomputable def stateAfterWrite (s : SailState) (rd : regidx) (val : BitVec 64) : SailState :=
  { s with regs := wX_update_regs rd val s.regs }

wX_update_regs

wX_update_regs r v regs takes a register index r, a 64-bit value v, and the current register file hash map regs. It inserts v at the Register key corresponding to r. Writing to x0 (index 0) is a no-op — x0 is hardwired to zero in RISC-V.

noncomputable def wX_update_regs
    (r : regidx)                                    -- which register to write
    (v : BitVec 64)                                  -- the value to write
    (regs : Std.ExtDHashMap Register RegisterType)   -- the current register file
    : Std.ExtDHashMap Register RegisterType :=       -- returns updated register file
  match r with
  | ⟨i⟩ =>                          -- destructure regidx to get the 5-bit index
    let w := regval_into_reg v       -- convert BitVec 64 to register value type (identity)
    match i.toNat with               -- match on the natural number index
    | 0 => regs                      -- x0: no-op, hardwired to zero
    | 1 => regs.insert Register.x1 w  | 2 => regs.insert Register.x2 w
    | 3 => regs.insert Register.x3 w  | 4 => regs.insert Register.x4 w
    | 5 => regs.insert Register.x5 w  | 6 => regs.insert Register.x6 w
    | 7 => regs.insert Register.x7 w  | 8 => regs.insert Register.x8 w
    | 9 => regs.insert Register.x9 w  | 10 => regs.insert Register.x10 w
    | 11 => regs.insert Register.x11 w | 12 => regs.insert Register.x12 w
    | 13 => regs.insert Register.x13 w | 14 => regs.insert Register.x14 w
    | 15 => regs.insert Register.x15 w | 16 => regs.insert Register.x16 w
    | 17 => regs.insert Register.x17 w | 18 => regs.insert Register.x18 w
    | 19 => regs.insert Register.x19 w | 20 => regs.insert Register.x20 w
    | 21 => regs.insert Register.x21 w | 22 => regs.insert Register.x22 w
    | 23 => regs.insert Register.x23 w | 24 => regs.insert Register.x24 w
    | 25 => regs.insert Register.x25 w | 26 => regs.insert Register.x26 w
    | 27 => regs.insert Register.x27 w | 28 => regs.insert Register.x28 w
    | 29 => regs.insert Register.x29 w | 30 => regs.insert Register.x30 w
    | _ => regs.insert Register.x31 w

Note: _ here works because i comes from a BitVec 5 (via regidx), so i.toNat can only be 0–31. Cases 0–30 are matched explicitly, so _ can only match 31.

wX_shape

wX_shape says that writing to a register via wX_bits always succeeds — for any register r, value v, and state s, there exists a resulting state s' such that wX_bits r v s = .ok () s'. Register writes cannot fail. Unlike readReg (which can throw Error.Unreachable if a key is missing from the hash map), wX_bits always produces an .ok result. This is why we don't need a WellFormed-like precondition for writes.

theorem wX_shape (r : regidx) (v : BitVec 64) (s : SailState) :
    ∃ s', wX_bits r v s = .ok () s'

wX_bits_eq_stateAfterWrite

Running the monadic register write wX_bits produces exactly the same state as the pure stateAfterWrite. If wX_bits rd v s = .ok () s', then s' = stateAfterWrite s rd v. This lets us move between the monadic world (used in the actual computation) and the specification world (used in the proof).

theorem wX_bits_eq_stateAfterWrite (rd : regidx) (v : BitVec 64) (s s' : SailState)
    (hw : wX_bits rd v s = .ok () s') :
    s' = stateAfterWrite s rd v

wX_rX_roundtrip

After writing value v to register rd (where rd ≠ x0), reading rd back gives you v and does not change the state. This is needed because the W-variant Jolt decompositions do a write followed by a read-back (the VSEW step reads what the previous step wrote).

theorem wX_rX_roundtrip (r : regidx) (v : BitVec 64) (s s' : SailState)
    (hr : r ≠ regidx.Regidx 0)
    (hw : wX_bits r v s = .ok () s') :
    rX_bits r s' = .ok v s'

The hr : r ≠ regidx.Regidx 0 hypothesis is essential — x0 is hardwired to zero, so writing to it and reading back would give 0, not v.

wX_wX_collapse

Writing v1 to rd and then writing v2 to rd is the same as writing v2 to rd directly from the original state. The first write is irrelevant — it gets overwritten. This is needed because the W-variant Jolt decompositions write to rd twice: once with the raw computation result, and once with the sign-extended version (from VSEW).

theorem wX_wX_collapse (r : regidx) (v1 v2 : BitVec 64) (s s1 s2 : SailState)
    (hw1 : wX_bits r v1 s = .ok () s1) (hw2 : wX_bits r v2 s1 = .ok () s2) :
    wX_bits r v2 s = .ok () s2

When each helper is needed

HelperUsed in non-W (SLL, SRA, SRL)Used in W variants (ADDW, SLLW, ...)Used in main theorem plumbing
stateAfterWrite_concrete_concretemain theorem (rw [hj_sail])
wX_shape_concrete_concretemain theorem (collapse RHS match)
wX_bits_eq_stateAfterWrite_concrete_concretemain theorem (final exact)
wX_rX_roundtrip—_concrete—
wX_wX_collapse—_concrete—