chore: explore changing read_mem_bytes and write_mem_bytes to read_me…

…m_bytes' and write_mem_bytes', this is a total disaster.

Arm/Insts/LDST/Reg_imm.lean

@@ -31,7 +31,7 @@ instance : ToString Reg_imm_cls where toString a := toString (repr a)
 @[state_simp_rules]
 def reg_imm_operation (inst_str : String) (op : BitVec 1)
   (wback : Bool) (postindex : Bool) (SIMD? : Bool)
-  (datasize : Nat) (regsize : Option Nat) (Rn : BitVec 5)
+  (datasize : Nat) (hdatasize : datasize < 2^64) (regsize : Option Nat) (Rn : BitVec 5)
   (Rt : BitVec 5) (offset : BitVec 64) (s : ArmState)
   (H : 8 ∣ datasize) : ArmState :=
   let address := read_gpr 64 Rn s
@@ -48,7 +48,15 @@ def reg_imm_operation (inst_str : String) (op : BitVec 1)
       match op with
       | 0#1 => -- STORE
         let data := ldst_read SIMD? datasize Rt s
-        write_mem_bytes (datasize / 8) address (BitVec.cast h.symm data) s
+        write_mem_bytes' (datasize / 8) address (data.cast (by 
+          simp [bv_toNat]
+          show _ = (BitVec.udiv _ _).toNat * 8
+          rw [BitVec.toNat_udiv]
+          simp
+          rw [Nat.mod_eq_of_lt (by omega)]
+          omega
+        )) s
+        -- write_mem_bytes (datasize / 8) address (BitVec.cast h.symm data) s
       | _ => -- LOAD
         let data := read_mem_bytes (datasize / 8) address s
         if SIMD? then write_sfp datasize Rt (BitVec.cast h data) s
@@ -79,12 +87,13 @@ def supported_reg_imm (size : BitVec 2) (opc : BitVec 2) (SIMD? : Bool) : Bool :
   | 0b00#2, 0b11#2, true => true -- LDR, 128-bit, SIMD&FP
   | _, _, _ => false -- other instructions that are not supported or illegal
 
+
 @[state_simp_rules]
 def exec_reg_imm_common
   (inst : Reg_imm_cls) (inst_str : String) (s : ArmState) : ArmState :=
-  let scale :=
-    if inst.SIMD? then ((lsb inst.opc 1) ++ inst.size).toNat
-    else inst.size.toNat
+  let ⟨scale, hscale⟩ : { n : Nat //  n ≤ 10} :=
+    if inst.SIMD? then ⟨((lsb inst.opc 1) ++ inst.size).toNat, by bv_omega⟩
+    else ⟨inst.size.toNat, by bv_omega⟩
   -- Only allow supported LDST Reg immediate instructions
   if not $ supported_reg_imm inst.size inst.opc inst.SIMD? then
     write_err (StateError.Unimplemented "Unsupported instruction {inst_str} encountered!") s
@@ -100,6 +109,12 @@ def exec_reg_imm_common
       | Sum.inl imm12 => (BitVec.zeroExtend 64 imm12) <<< scale
       | Sum.inr imm9 => signExtend 64 imm9
     let datasize := 8 <<< scale
+    have : datasize < 2^64 := by 
+      simp [datasize]
+      rw [Nat.shiftLeft_eq]
+      have : 2^scale ≤ 2^10 := by apply Nat.pow_le_pow_of_le (by decide) (by omega)
+      simp at this
+      omega
     let regsize :=
       if inst.SIMD? then none
       else if inst.size = 0b11#2 then some 64 else some 32
@@ -108,7 +123,7 @@ def exec_reg_imm_common
     -- State Updates
     let s' := reg_imm_operation inst_str
               (lsb inst.opc 0) inst.wback inst.postindex
-              inst.SIMD? datasize regsize inst.Rn inst.Rt offset s (H)
+              inst.SIMD? datasize (by omega) regsize inst.Rn inst.Rt offset s (H)
     let s' := write_pc ((read_pc s) + 4#64) s'
     s'
 

Arm/State.lean

@@ -666,6 +666,10 @@ def read_mem_bytes (n : Nat) (addr : BitVec 64) (s : ArmState) : BitVec (n * 8)
     let rest := read_mem_bytes n' (addr + 1#64) s
     (rest ++ byte).cast (by omega)
 
+def read_mem_bytes' (n : BitVec 64) (addr : BitVec 64) (s : ArmState) : BitVec (n.toNat * 8) :=
+  read_mem_bytes n.toNat addr s
+
+
 /-- We export write_mem_bytes, not write_mem. FIXME: make private. -/
 def write_mem (addr : BitVec 64) (val : BitVec 8) (s : ArmState) : ArmState :=
   let new_mem := write_store addr val s.mem
@@ -680,6 +684,8 @@ def write_mem_bytes (n : Nat) (addr : BitVec 64) (val : BitVec (n * 8)) (s : Arm
     let val_rest := BitVec.zeroExtend (n' * 8) (val >>> 8)
     write_mem_bytes n' (addr + 1#64) val_rest s
 
+def write_mem_bytes' (n : BitVec 64) (addr : BitVec 64) (val : BitVec (n.toNat * 8)) (s : ArmState) : ArmState :=
+  write_mem_bytes n.toNat addr val s
 
 /-! # Memory accessors and updaters -/
 
@@ -703,6 +709,12 @@ theorem r_of_write_mem_bytes :
   case zero => rfl
   done
 
+@[state_simp_rules]
+theorem r_of_write_mem_bytes' :
+  r fld (write_mem_bytes' n addr val s) = r fld s := by
+  apply r_of_write_mem_bytes
+
+
 theorem fetch_inst_of_write_mem :
   fetch_inst addr1 (write_mem addr2 val s) = fetch_inst addr1 s := by
   unfold fetch_inst write_mem
@@ -719,6 +731,10 @@ theorem fetch_inst_of_write_mem_bytes :
     rw [n_ih, fetch_inst_of_write_mem]
   done
 
+@[state_simp_rules]
+theorem fetch_inst_of_write_mem_bytes' :
+  fetch_inst addr1 (write_mem_bytes' n addr2 val s) = fetch_inst addr1 s := by simp [write_mem_bytes', state_simp_rules]
+
 theorem read_mem_of_w :
   read_mem addr (w fld v s) = read_mem addr s := by
   unfold read_mem
@@ -745,6 +761,26 @@ theorem read_mem_bytes_w_of_read_mem_eq
     = read_mem_bytes n₁ addr₁ s₂ := by
   simp only [read_mem_bytes_of_w, h]
 
+
+
+private axiom read_mem_write_mem_n_lt_two_pow_64 (n : Nat) : n < 2^64
+
+@[state_simp_rules]
+theorem read_mem_bytes_w_of_read_mem_eq'
+    (h : ∀ n addr, read_mem_bytes' n addr s₁ = read_mem_bytes' n addr s₂)
+    (fld val n₁ addr₁) :
+    read_mem_bytes' n₁ addr₁ (w fld val s₁)
+    = read_mem_bytes' n₁ addr₁ s₂ := by
+  simp [read_mem_bytes'] at *
+  apply read_mem_bytes_w_of_read_mem_eq <;> try assumption
+  intros n addr
+  specialize (h n addr)
+  have : n < 2^64 := read_mem_write_mem_n_lt_two_pow_64 n
+  simp [BitVec.toNat_ofNat] at h
+  rw [BitVec.toNat_ofNat] at h
+  rw [show n % 2^64 = n by omega] at h
+  exact h
+
 @[state_simp_rules]
 theorem write_mem_bytes_program {n : Nat} (addr : BitVec 64) (bytes : BitVec (n * 8)):
     (write_mem_bytes n addr bytes s).program = s.program := by
@@ -756,6 +792,12 @@ theorem write_mem_bytes_program {n : Nat} (addr : BitVec 64) (bytes : BitVec (n
     rw [h_n]
     simp only [write_mem]
 
+
+@[state_simp_rules]
+theorem write_mem_bytes'_program :
+    (write_mem_bytes' n addr bytes s).program = s.program := by
+  apply write_mem_bytes_program
+
 /-! ### Memory RoW/WoW lemmas -/
 
 theorem read_mem_of_write_mem_same :
@@ -1177,6 +1219,22 @@ theorem read_mem_bytes_write_mem_bytes_of_read_mem_eq
   simp only [← Memory.mem_eq_iff_read_mem_bytes_eq] at h ⊢
   simp only [memory_rules, h]
 
+
+theorem read_mem_bytes_write_mem_bytes_of_read_mem_eq'
+    (h : ∀ n addr, read_mem_bytes' n addr s₁ = read_mem_bytes' n addr s₂)
+    (n₂ addr₂ val n₁ addr₁) :
+    read_mem_bytes' n₁ addr₁ (write_mem_bytes' n₂ addr₂ val s₁)
+    = read_mem_bytes' n₁ addr₁ (write_mem_bytes' n₂ addr₂ val s₂) := by
+  simp [read_mem_bytes', write_mem_bytes']
+  apply read_mem_bytes_write_mem_bytes_of_read_mem_eq <;> try assumption
+  · intros n addr
+    specialize h n addr
+    have : n < 2^64 := read_mem_write_mem_n_lt_two_pow_64 n
+    simp [read_mem_bytes'] at h
+    rw [BitVec.toNat_ofNat] at h
+    rw [show n % 2^64 = n by omega] at h
+    exact h
+
 /- Helper lemma for `state_eq_iff_components_eq` -/
 
 private theorem reads_equal_implies_gpr_equal (s1 s2 : ArmState)

Tactics/Sym/AxEffects.lean

@@ -134,7 +134,7 @@ def initial (state : Expr) : AxEffects where
       mkLambda `addr .default bv64 <|
         mkApp2 (.const ``Eq.refl [1])
           (mkApp (mkConst ``BitVec) <| mkNatMul (.bvar 1) (toExpr 8))
-          (mkApp3 (mkConst ``read_mem_bytes) (.bvar 1) (.bvar 0) state)
+          (mkApp3 (mkConst ``read_mem_bytes') (.bvar 1) (.bvar 0) state)
   programProof      :=
     -- `rfl`
     mkAppN (.const ``Eq.refl [1]) #[
@@ -251,15 +251,15 @@ private def update_write_mem (eff : AxEffects) (n addr val : Expr) :
 
   -- Update each field
   let fields ← eff.fields.toList.mapM fun ⟨fld, {value, proof}⟩ => do
-    let r_of_w := mkApp5 (mkConst ``r_of_write_mem_bytes)
+    let r_of_w := mkApp5 (mkConst ``r_of_write_mem_bytes')
                     (toExpr fld) n addr val eff.currentState
     let proof ← mkEqTrans r_of_w proof
     return ⟨fld, {value, proof}⟩
 
   -- Update the non-effects proof
   let nonEffectProof ← lambdaTelescope eff.nonEffectProof fun args proof => do
     let f := args[0]!
-    let r_of_w := mkApp5 (mkConst ``r_of_write_mem_bytes)
+    let r_of_w := mkApp5 (mkConst ``r_of_write_mem_bytes')
                     f n addr val eff.currentState
     let proof ← mkEqTrans r_of_w proof
     mkLambdaFVars args proof
@@ -268,21 +268,21 @@ private def update_write_mem (eff : AxEffects) (n addr val : Expr) :
   -- Update the memory effects proof
   let memoryEffectProof :=
     -- `read_mem_bytes_write_mem_bytes_of_read_mem_eq <memoryEffectProof> ...`
-    mkAppN (mkConst ``read_mem_bytes_write_mem_bytes_of_read_mem_eq)
+    mkAppN (mkConst ``read_mem_bytes_write_mem_bytes_of_read_mem_eq')
       #[eff.currentState, eff.memoryEffect, eff.memoryEffectProof, n, addr, val]
 
   -- Update the program proof
   let programProof ←
     -- `Eq.trans (@write_mem_bytes_program <currentState> ...) <programProof>`
     mkEqTrans
-      (mkAppN (mkConst ``write_mem_bytes_program)
+      (mkAppN (mkConst ``write_mem_bytes'_program)
         #[eff.currentState, n, addr, val])
       eff.programProof
 
   -- Assemble the result
   let addWrite (e : Expr) :=
     -- `@write_mem_bytes <n> <addr> <val> <e>`
-    mkApp4 (mkConst ``write_mem_bytes) n addr val e
+    mkApp4 (mkConst ``write_mem_bytes') n addr val e
   let eff := { eff with
     currentState    := addWrite eff.currentState
     fields          := .ofList fields
@@ -363,7 +363,7 @@ private def update_w (eff : AxEffects) (fld val : Expr) :
   -- Update the memory effect proof
   let memoryEffectProof :=
     -- `read_mem_bytes_w_of_read_mem_eq ...`
-    mkAppN (mkConst ``read_mem_bytes_w_of_read_mem_eq)
+    mkAppN (mkConst ``read_mem_bytes_w_of_read_mem_eq')
       #[eff.currentState, eff.memoryEffect, eff.memoryEffectProof, fld, val]
 
   -- Update the program proof
@@ -401,7 +401,7 @@ return an `AxEffects` where `e` is the new `currentState`. -/
 partial def updateWithExpr (eff : AxEffects) (e : Expr) : MetaM AxEffects := do
   let msg := m!"Updating effects with writes from: {e}"
   withTraceNode `Tactic.sym (fun _ => pure msg) <| do match_expr e with
-    | write_mem_bytes n addr val e =>
+    | write_mem_bytes' n addr val e =>
         let eff ← eff.updateWithExpr e
         eff.update_write_mem n addr val