refactor: cleanup popcount proof

Arm/Insts/Common.lean

@@ -56,6 +56,7 @@ def AddWithCarry (x : BitVec n) (y : BitVec n) (carry_in : BitVec 1) :
   (result, (make_pstate N Z C V))
 
 /-- When the carry bit is `0`, `AddWithCarry x y 0 = x + y` -/
+@[bitvec_rules]
 theorem fst_AddWithCarry_eq_add (x : BitVec n) (y : BitVec n) :
   (AddWithCarry x y 0#1).fst = x + y := by
   simp  [AddWithCarry, zeroExtend_eq, zeroExtend_zero, zeroExtend_zero]
@@ -67,6 +68,7 @@ theorem fst_AddWithCarry_eq_add (x : BitVec n) (y : BitVec n) :
   rw [Nat.mod_eq_of_lt this]
 
 /-- When the carry bit is `1`, `AddWithCarry x y 1 = x - ~~~y` -/
+@[bitvec_rules]
 theorem fst_AddWithCarry_eq_sub_neg (x : BitVec n) (y : BitVec n) :
   (AddWithCarry x y 1#1).fst = x - ~~~y := by
   simp  [AddWithCarry, zeroExtend_eq, zeroExtend_zero, zeroExtend_zero]
@@ -551,7 +553,7 @@ def rev_elems (n esize : Nat) (x : BitVec n) (h₀ : esize ∣ n) (h₁ : 0 < es
     BitVec.cast h3 (element ++ rest_ans)
    termination_by n
 
-example : rev_elems 4 4 0xA#4 (by decide) (by decide) = 0xA#4 := by 
+example : rev_elems 4 4 0xA#4 (by decide) (by decide) = 0xA#4 := by
   native_decide
 example : rev_elems 8 4 0xAB#8 (by decide) (by decide) = 0xBA#8 := by native_decide
 example : rev_elems 8 4 (rev_elems 8 4 0xAB#8 (by decide) (by decide))

Arm/Insts/DPI/Add_sub_imm.lean

@@ -24,19 +24,21 @@ def exec_add_sub_imm (inst : Add_sub_imm_cls) (s : ArmState) : ArmState :=
                         else
                           imm <<< 12
     let operand1      := read_gpr datasize inst.Rn s
-    let (carry_in, operand2)
+    let carryInAndOperand2
                       := if sub_op then
                           (1#1, ~~~imm)
                         else
                           (0#1, imm)
+    let carry := carryInAndOperand2.fst
+    let operand2 := carryInAndOperand2.snd
     let operand2         := BitVec.zeroExtend datasize operand2
-    let (result, pstate) := AddWithCarry operand1 operand2 carry_in
+    let resultAndPState := AddWithCarry operand1 operand2 carry
     -- State Updates
     let s'            := write_pc ((read_pc s) + 4#64) s
-    let s'            := if setflags then write_pstate pstate s' else s'
+    let s'            := if setflags then write_pstate resultAndPState.snd s' else s'
     let s'            := if inst.Rd = 31#5 ∧ ¬ setflags
-                         then write_gpr datasize inst.Rd result s'
-                         else write_gpr_zr datasize inst.Rd result s'
+                         then write_gpr datasize inst.Rd resultAndPState.fst s'
+                         else write_gpr_zr datasize inst.Rd resultAndPState.fst s'
     s'
 
 ----------------------------------------------------------------------

Proofs/Popcount32.lean

@@ -68,7 +68,6 @@ def popcount32_program : Program :=
    (0x400618#64 , 0x910043ff#32), -- add sp, sp, #0x10
    (0x40061c#64 , 0xd65f03c0#32)] -- ret
 
-
 #genStepEqTheorems popcount32_program
 
 theorem popcount32_sym_meets_spec (s0 s_final : ArmState)
@@ -91,34 +90,18 @@ theorem popcount32_sym_meets_spec (s0 s_final : ArmState)
   -- Final Steps
   -- Split all the Ands in the conclusion.
   repeat' apply And.intro
-  · simp only [popcount32_spec,
-               fst_AddWithCarry_eq_add,
-               fst_AddWithCarry_eq_sub_neg]
-    simp only [popcount32_spec_rec]
+  · simp only [popcount32_spec, popcount32_spec_rec]
     bv_decide
   · sym_aggregate
-  · -- (TODO @alex) Let's do away with
-    -- ∀ (n : Nat) (addr : BitVec 64), read_mem_bytes n addr s₁ = read_mem_bytes n addr s₂
-    -- in favor of
-    -- s₁.mem = s₂.mem
-    -- as Sid said.
-    simp only [←Memory.mem_eq_iff_read_mem_bytes_eq] at *
+  · intro n addr h_separate
     simp only [memory_rules] at *
-    intro n addr h_separate
-
-    -- (TODO @alex/@bollu) Can we hope to make this shorter after the marriage
-    -- of `sym_n` and `simp_mem`?
-    simp (config := {ground := true}) only
-          [fst_AddWithCarry_eq_add, fst_AddWithCarry_eq_sub_neg]
-    simp only [*, bitvec_rules]
-    simp_mem
-    sym_aggregate
-
-    simp (config := {ground := true}) only
-          [fst_AddWithCarry_eq_add, fst_AddWithCarry_eq_sub_neg]
-    simp only [*, bitvec_rules]
-    simp_mem
-    rfl
+    repeat (simp_mem; sym_aggregate)
+  · apply Aligned_BitVecSub_64_4 -- TODO(@bollu): match goal.
+    · assumption
+    · decide
+  · apply Aligned_BitVecAdd_64_4
+    · assumption
+    · decide
 
 
 -------------------------------------------------------------------------------

Tactics/Aggregate.lean

@@ -68,12 +68,18 @@ elab "sym_aggregate" simpConfig?:(config)? loc?:(location)? : tactic => withMain
     let lctx ← getLCtx
     -- We keep `expectedRead`/`expectedAlign` as monadic values,
     -- so that we get new metavariables for each localdecl we check
-    let expectedRead := do
+    let expectedRead : MetaM Expr := do
       let fld ← mkFreshExprMVar (mkConst ``StateField)
       let state ← mkFreshExprMVar mkArmState
       let rhs ← mkFreshExprMVar none
       mkEq (mkApp2 (mkConst ``r) fld state) rhs
-    let expectedAlign := do
+    let expectedReadMem : MetaM Expr := do
+      let n ← mkFreshExprMVar (mkConst ``Nat)
+      let addr ← mkFreshExprMVar (mkApp (mkConst ``BitVec) (toExpr 64))
+      let mem ← mkFreshExprMVar (mkConst ``Memory)
+      let rhs ← mkFreshExprMVar none
+      mkEq (mkApp3 (mkConst ``Memory.read_bytes) n addr mem) rhs
+    let expectedAlign : MetaM Expr := do
       let state ← mkFreshExprMVar mkArmState
       return mkApp (mkConst ``CheckSPAlignment) state
 
@@ -84,12 +90,16 @@ elab "sym_aggregate" simpConfig?:(config)? loc?:(location)? : tactic => withMain
             trace[Tactic.sym] "checking {decl.toExpr} with type {type}"
             let expectedRead ← expectedRead
             let expectedAlign ← expectedAlign
+            let expectedReadMem ← expectedReadMem
             if ← isDefEq type expectedRead then
               trace[Tactic.sym] "{Lean.checkEmoji} match for {expectedRead}"
               return axHyps.push decl
             else if ← isDefEq type expectedAlign then
               trace[Tactic.sym] "{Lean.checkEmoji} match for {expectedAlign}"
               return axHyps.push decl
+            else if ← isDefEq type expectedReadMem then
+              trace[Tactic.sym] "{Lean.checkEmoji} match for {expectedReadMem}"
+              return axHyps.push decl
             else
               trace[Tactic.sym] "{Lean.crossEmoji} no match"
               return axHyps