feat: prove specification of Max program that manipulates memory via new VCG

Arm/Attr.lean

@@ -9,6 +9,11 @@ register_simp_attr state_simp_rules
 register_simp_attr bitvec_rules
 -- Rules for memory lemmas
 register_simp_attr memory_rules
+-- Rules for memory aligned lemmas
+register_simp_attr aligned_rules
+
+-- Rules for making proof states look more compact.
+register_simp_attr pretty_rules
 
 /-
 syntax "state_simp" : tactic

Arm/BitVec.lean

@@ -288,6 +288,25 @@ abbrev lsb (x : BitVec n) (i : Nat) : BitVec 1 :=
   -- by LeanSAT.
   (BitVec.extractLsb i i x).cast (by omega)
 
+section ForLean
+
+@[simp]
+theorem ofBool_eq_1_iff (x : Bool) : BitVec.ofBool x = 1#1 ↔ x = true := by
+  rcases x <;> simp
+
+@[simp]
+theorem ofBool_eq_0_iff (x : Bool) : BitVec.ofBool x = 0#1 ↔ x = false := by
+  rcases x <;> simp
+
+end ForLean
+
+theorem lsb_eq_ofBool_getLsb : lsb x i = BitVec.ofBool (x.getLsb i) := by
+  apply BitVec.eq_of_getLsb_eq
+  simp only [getLsb_cast, getLsb_extract, Nat.sub_self, Nat.le_zero_eq, getLsb_ofBool]
+  intros k
+  simp only [show k = 0 by omega, Fin.isValue, Fin.val_zero, decide_True, Nat.add_zero,
+    Bool.true_and]
+
 abbrev partInstall (hi lo : Nat) (val : BitVec (hi - lo + 1)) (x : BitVec n): BitVec n :=
   let mask := allOnes (hi - lo + 1)
   let val_aligned := (zeroExtend n val) <<< lo

Arm/Insts/Common.lean

@@ -7,18 +7,19 @@ Author(s): Shilpi Goel, Yan Peng, Nathan Wetzler
 import LeanSAT
 import Arm.BitVec
 import Arm.State
-
+import Arm.Attr
+import Lean
 section Common
 
 open BitVec
 
 ----------------------------------------------------------------------
 
-/-- 
+/--
 `GPRIndex.rand` picks a safe GPR index for Arm-based Apple platforms
 i.e., one not reserved on them. Use this function instead of
 `BitVec.rand` to pick an appropriate random index for a source and
-destination GPR during cosimulations. 
+destination GPR during cosimulations.
 
 See "NOTE: Considerations for running cosimulations on Arm-based Apple
 platforms" in Arm/Cosim.lean for details.
@@ -44,6 +45,19 @@ partial def GPRIndex.rand (lo := 0) (hi := 31) :
 
 ----------------------------------------------------------------------
 
+/-- Sum of bitvectors `x y : BitVec n` and `c : BitVec 1` in a large bitvector `unsigned_sum`.  -/
+def unsignedSum (x y : BitVec n) (c : BitVec 1) : BitVec (n + 1) :=
+  (zeroExtend (n + 1) x) + (zeroExtend (n + 1) y) + (zeroExtend (n + 1) c)
+
+def signedSum (x y : BitVec n) (c : BitVec 1) : BitVec (n + 1) :=
+  signExtend (n + 1) x + signExtend (n + 1) y + (signExtend (n + 1)) c
+
+@[bitvec_rules]
+theorem toNat_unsignedSum {x y : BitVec n} : (unsignedSum x y c).toNat = x.toNat + y.toNat + c.toNat := by
+  simp [unsignedSum]
+  rw [Nat.mod_eq_of_lt (by omega)]
+
+-- https://developer.arm.com/documentation/ddi0597/2023-12/Shared-Pseudocode/shared-functions-integer?lang=en#impl-shared.AddWithCarry.3
 def AddWithCarry (x : BitVec n) (y : BitVec n) (carry_in : BitVec 1) :
   (BitVec n × PState) :=
   let carry_in_ext := zeroExtend (n + 1) carry_in
@@ -58,13 +72,103 @@ def AddWithCarry (x : BitVec n) (y : BitVec n) (carry_in : BitVec 1) :
   let V := if signExtend (n + 1) result = signed_sum then 0#1 else 1#1
   (result, (make_pstate N Z C V))
 
--- TODO: Is this rule helpful at all?
+@[bitvec_rules, state_simp_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]
+  apply BitVec.eq_of_toNat_eq
+  simp only [toNat_truncate, toNat_add, Nat.add_mod_mod, Nat.mod_add_mod]
+  have : 2^n < 2^(n + 1) := by
+    refine Nat.pow_lt_pow_of_lt (by omega) (by omega)
+  have : x.toNat + y.toNat < 2^(n + 1) := by omega
+  rw [Nat.mod_eq_of_lt this]
+
+@[bitvec_rules, state_simp_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]
+  apply BitVec.eq_of_toNat_eq
+  simp only [toNat_truncate, toNat_add, Nat.add_mod_mod, Nat.mod_add_mod, toNat_ofNat, Nat.pow_one,
+    Nat.reduceMod, toNat_sub, toNat_not]
+  simp only [show 2 ^ n - (2 ^ n - 1 - y.toNat) = 1 + y.toNat by omega]
+  have : 2^n < 2^(n + 1) := by
+    refine Nat.pow_lt_pow_of_lt (by omega) (by omega)
+  have : x.toNat + y.toNat + 1 < 2^(n + 1) := by omega
+  rw [Nat.mod_eq_of_lt this]
+  congr 1
+  omega
+
+@[bitvec_rules, state_simp_rules]
+theorem fst_AddWithCarry_eq (x : BitVec n) (y : BitVec n) {carry : BitVec 1} :
+  (AddWithCarry x y carry).fst = if carry = 1#1 then x - ~~~y else x + y := by
+  have : carry = 0#1 ∨ carry = 1#1 := by bv_decide
+  rcases this with rfl | rfl  <;> simp [state_simp_rules]
+
+/-- the `z` flag is `1` when the result is `0`. -/
+@[bitvec_rules, state_simp_rules]
+theorem z_snd_AddWithCarry_iff (x y : BitVec n) :
+    ((AddWithCarry x y c).snd.z = 1#1) ↔ ((x.toNat + y.toNat + c.toNat) % 2^n = 0) := by
+  simp [AddWithCarry, make_pstate]
+  have hxyc : x.toNat + y.toNat + c.toNat < 2^(n + 1) := by omega
+  constructor
+  · intros h
+    simp at h
+    obtain this
+      : (zeroExtend n (zeroExtend (n + 1) x + zeroExtend (n + 1) y + (zeroExtend (n + 1) c))).toNat = (0#n).toNat :=
+      by simp [h]
+    simp at this
+    simp only [Nat.mod_eq_of_lt hxyc] at this
+    exact this
+  · intros h
+    apply BitVec.eq_of_toNat_eq
+    simp only [toNat_truncate, toNat_add, Nat.add_mod_mod, Nat.mod_add_mod, Nat.mod_eq_of_lt hxyc,
+      h, toNat_ofNat, Nat.zero_mod]
+
 @[bitvec_rules]
 theorem zeroExtend_eq_of_AddWithCarry :
   zeroExtend n (AddWithCarry x y carry_in).fst =
   (AddWithCarry x y carry_in).fst := by
   simp only [zeroExtend_eq]
 
+-- https://github.com/awslabs/s2n-bignum/blob/main/arm/proofs/instruction.ml#L543C36-L543C62
+/- `x > y` iff `(N = V)` . -/
+theorem sgt_iff_n_eq_v_and_z_eq_0_64 (x y : BitVec 64) :
+  (((AddWithCarry x (~~~y) 1#1).snd.n = (AddWithCarry x (~~~y) 1#1).snd.v) ∧
+   (AddWithCarry x (~~~y) 1#1).snd.z = 0#1) ↔ BitVec.slt y x := by
+  simp [AddWithCarry, make_pstate]
+  split
+  · bv_decide
+  · bv_decide
+
+-- https://github.com/awslabs/s2n-bignum/blob/main/arm/proofs/instruction.ml#L543C36-L543C62
+/- `x > y` iff `(N = V) ∧ Z = 0` . -/
+theorem sgt_iff_n_eq_v_and_z_eq_0_32 (x y : BitVec 32) :
+  (((AddWithCarry x (~~~y) 1#1).snd.n = (AddWithCarry x (~~~y) 1#1).snd.v) ∧
+   (AddWithCarry x (~~~y) 1#1).snd.z = 0#1) ↔ BitVec.slt y x := by
+  simp [AddWithCarry, make_pstate]
+  split
+  · bv_decide
+  · bv_decide
+
+/- `x ≤ y` iff `¬ ((N = V) ∧ (Z = 0))`. -/
+theorem sle_iff_not_n_eq_v_and_z_eq_0_64 (x y : BitVec 64) :
+  (¬(((AddWithCarry x (~~~y) 1#1).snd.n = (AddWithCarry x (~~~y) 1#1).snd.v) ∧
+   (AddWithCarry x (~~~y) 1#1).snd.z = 0#1)) ↔ BitVec.sle x y := by
+  simp [AddWithCarry, make_pstate]
+  split
+  · bv_decide
+  · bv_decide
+
+/- `x ≤ y` iff `¬ ((N = V) ∧ (Z = 0))`. -/
+theorem sle_iff_not_n_eq_v_and_z_eq_0_32 (x y : BitVec 32) :
+  (¬(((AddWithCarry x (~~~y) 1#1).snd.n = (AddWithCarry x (~~~y) 1#1).snd.v) ∧
+   (AddWithCarry x (~~~y) 1#1).snd.z = 0#1)) ↔ BitVec.sle x y := by
+  simp [AddWithCarry, make_pstate]
+  split
+  · bv_decide
+  · bv_decide
+
+-- https://developer.arm.com/documentation/ddi0602/2023-09/Shared-Pseudocode/shared-functions-system?lang=en#impl-shared.ConditionHolds.1
 def ConditionHolds (cond : BitVec 4) (s : ArmState) : Bool :=
   open PFlag in
   let N := read_flag N s
@@ -73,18 +177,23 @@ def ConditionHolds (cond : BitVec 4) (s : ArmState) : Bool :=
   let V := read_flag V s
   let result :=
     match (extractLsb 3 1 cond) with
-      | 0b000#3 => Z = 1#1
-      | 0b001#3 => C = 1#1
-      | 0b010#3 => N = 1#1
-      | 0b011#3 => V = 1#1
-      | 0b100#3 => C = 1#1 ∧ Z = 0#1
-      | 0b101#3 => N = V
-      | 0b110#3 => N = V ∧ Z = 0#1
-      | 0b111#3 => true
+      | 0b000#3 => Z = 1#1           -- EQ or NE
+      | 0b001#3 => C = 1#1           -- CS or CC
+      | 0b010#3 => N = 1#1           -- MI or PL
+      | 0b011#3 => V = 1#1           -- VS or VC
+      | 0b100#3 => C = 1#1 ∧ Z = 0#1 -- HI or LS
+      | 0b101#3 => N = V             -- GE or LT
+      | 0b110#3 => (N = V) ∧ (Z = 0#1) -- GT or LE
+      | 0b111#3 => true                -- AL
   if (lsb cond 0) = 1#1 ∧ cond ≠ 0b1111#4 then
     not result
   else
     result
+  where
+  GT (s : ArmState) : Prop := (s.N = s.V) ∧ (s.Z = 0#1)
+  /-- The condition that tells us whether the compare instruction resulted in a LE. -/
+  LE (s : ArmState) : Prop := ¬ GT s
+
 
 /-- `Aligned x a` witnesses that the bitvector `x` is `a`-bit aligned. -/
 def Aligned (x : BitVec n) (a : Nat) : Prop :=
@@ -96,21 +205,98 @@ def Aligned (x : BitVec n) (a : Nat) : Prop :=
 instance : Decidable (Aligned x a) := by
   cases a <;> simp [Aligned] <;> infer_instance
 
+@[aligned_rules]
+theorem Aligned_BitVecSub_64_4 {x : BitVec 64} {y : BitVec 64}
+  (x_aligned : Aligned x 4)
+  (y_aligned : Aligned y 4)
+  : Aligned (x - y) 4 := by
+  simp_all [Aligned]
+  bv_decide
+
+@[aligned_rules]
 theorem Aligned_BitVecAdd_64_4 {x : BitVec 64} {y : BitVec 64}
   (x_aligned : Aligned x 4)
   (y_aligned : Aligned y 4)
   : Aligned (x + y) 4 := by
   simp_all [Aligned]
   bv_decide
 
+@[aligned_rules]
 theorem Aligned_AddWithCarry_64_4 (x : BitVec 64) (y : BitVec 64) (carry_in : BitVec 1)
   (x_aligned : Aligned x 4)
   (y_carry_in_aligned : Aligned (BitVec.add (extractLsb 3 0 y) (zeroExtend 4 carry_in)) 4)
   : Aligned (AddWithCarry x y carry_in).fst 4 := by
   unfold AddWithCarry Aligned at *
-  simp_all
+  simp_all only [Nat.sub_zero, zero_eq, add_eq]
+  bv_decide
+
+@[aligned_rules]
+theorem Aligned_AddWithCarry_64_4' (x : BitVec 64) (y : BitVec 64) (carry_in : BitVec 1)
+  (x_aligned : Aligned x 4)
+  (y_carry_in_aligned : Aligned (y + (carry_in.zeroExtend _)) 4)
+  : Aligned (AddWithCarry x y carry_in).fst 4 := by
+  unfold AddWithCarry Aligned at *
+  simp_all only [Nat.sub_zero, zero_eq, add_eq]
   bv_decide
 
+/- A bitvector `x` has alignment `n` if the least significant `n` bites are zero. -/
+@[aligned_rules]
+theorem Aligned_of_extractLsb_eq_zero {w n : Nat} {x : BitVec w} (hx : x.extractLsb (n - 1) 0 = 0 := by bv_decide) :
+    Aligned x n := by
+  simp [Aligned]
+  rcases n with rfl | n
+  · simp only
+  · simp only [Nat.add_one_sub_one, Nat.sub_zero, ofNat_eq_ofNat] at hx
+    simp only
+    rw [hx]
+
+/--
+When the alignment `n` is zero, the bitvector `x` is always aligned.
+For other alignments, then low `n` bits of `x` must be zero.
+Mathematically, this corresponds to the fact that `x % 2^n = 0`. When `n = 0`,
+we get `x % 1 = 0`, which is true for all numbers.
+TODO: this should be rewritten in terms of `extractLsb'` because we want to talk about 0 width bitvectors
+when `n = 0`.
+-/
+@[aligned_rules]
+theorem extractLsb_eq_zero_of_Aligned {w n : Nat} {x : BitVec w} (haligned : Aligned x n) :
+    (n = 0) ∨ x.extractLsb (n - 1) 0 = 0#(n - 1 + 1) := by
+  rw [Aligned] at haligned
+  rcases n with rfl | n
+  · simp at haligned
+    simp
+  · simp at haligned
+    simp
+    exact haligned
+
+/-- A bitvector `x` has alignment `n` if `x % 2^n = 0`. -/
+theorem Aligned_of_toNat_mod_eq_zero {w n : Nat} {x : BitVec w} (hx : x.toNat % 2 ^ n = 0 := by bv_omega) :
+    Aligned x n := by
+  simp [Aligned]
+  rcases n with rfl | n
+  · simp only
+  · apply BitVec.eq_of_toNat_eq
+    simp only [Nat.sub_zero, extractLsb_toNat, Nat.shiftRight_zero, hx, toNat_ofNat, Nat.zero_mod]
+
+theorem toNat_mod_eq_zero_of_Aligned {w n : Nat} {x : BitVec w} (hx : Aligned x n) :
+    x.toNat % 2 ^ n = 0 := by
+  simp [Aligned] at hx
+  rcases n with rfl | n
+  · simp only [Nat.pow_zero]
+    omega
+  · simp only at hx
+    have : (extractLsb n 0 x).toNat = (0#(n+1)).toNat := by
+      rw [hx]
+    simpa only [Nat.sub_zero, extractLsb_toNat, Nat.shiftRight_zero, toNat_ofNat,
+      Nat.zero_mod] using this
+
+@[bv_toNat]
+theorem Aligned_iff_toNat_mod_eq_zero {w n : Nat} {x : BitVec w} :
+    Aligned x n ↔ x.toNat % 2 ^ n = 0 := by
+  constructor
+  · apply toNat_mod_eq_zero_of_Aligned
+  · apply Aligned_of_toNat_mod_eq_zero
+
 /-- Check correct stack pointer (SP) alignment for AArch64 state; returns
 true when sp is aligned. -/
 def CheckSPAlignment (s : ArmState) : Prop :=
@@ -124,28 +310,41 @@ def CheckSPAlignment (s : ArmState) : Prop :=
 /-- We need to prove why the CheckSPAlignment predicate is Decidable. -/
 instance : Decidable (CheckSPAlignment s) := by unfold CheckSPAlignment; infer_instance
 
-@[state_simp_rules]
+@[state_simp_rules, aligned_rules]
 theorem CheckSPAligment_of_w_different (h : StateField.GPR 31#5 ≠ fld) :
   CheckSPAlignment (w fld v s) = CheckSPAlignment s := by
   simp_all only [CheckSPAlignment, state_simp_rules, minimal_theory, bitvec_rules]
 
-@[state_simp_rules]
+@[state_simp_rules, aligned_rules]
 theorem CheckSPAligment_of_w_sp :
   CheckSPAlignment (w (StateField.GPR 31#5) v s) = (Aligned v 4) := by
   simp_all only [CheckSPAlignment, state_simp_rules, minimal_theory, bitvec_rules]
 
-@[state_simp_rules]
+@[state_simp_rules, aligned_rules]
 theorem CheckSPAligment_of_write_mem_bytes :
   CheckSPAlignment (write_mem_bytes n addr v s) = CheckSPAlignment s := by
   simp_all only [CheckSPAlignment, state_simp_rules, minimal_theory, bitvec_rules]
 
-@[state_simp_rules]
+@[state_simp_rules, aligned_rules]
 theorem CheckSPAlignment_AddWithCarry_64_4 (st : ArmState) (y : BitVec 64) (carry_in : BitVec 1)
   (x_aligned : CheckSPAlignment st)
   (y_carry_in_aligned : Aligned (BitVec.add (extractLsb 3 0 y) (zeroExtend 4 carry_in)) 4)
   : Aligned (AddWithCarry (r (StateField.GPR 31#5) st) y carry_in).fst 4 := by
-  simp_all only [CheckSPAlignment, read_gpr, zeroExtend_eq, Nat.sub_zero, add_eq,
-    Aligned_AddWithCarry_64_4]
+  simp_all only [CheckSPAlignment, read_gpr, zeroExtend_eq, Nat.sub_zero, add_eq, Aligned_AddWithCarry_64_4]
+
+
+open Lean Elab Meta Macro in
+macro "solve_align" : tactic =>
+  `(tactic|
+      repeat solve
+      | simp (config := { ground := true, decide := true}) [aligned_rules, state_simp_rules]
+      | apply Aligned_BitVecSub_64_4;
+      | apply Aligned_BitVecAdd_64_4;
+      | apply Aligned_AddWithCarry_64_4;
+      | apply Aligned_AddWithCarry_64_4';
+      | apply Aligned_of_extractLsb_eq_zero; bv_decide
+      | apply Aligned_of_toNat_mod_eq_zero; bv_omega
+      | rfl)
 
 ----------------------------------------------------------------------