chore: rewrite semantics to not have pattern match on structure (#171)

### Issues: This works around leanprover/lean4#5388, and removes uses of `simp (config := { ground := true }) ..`. This makes our proof states cleaner, since we no longer see proof states involving `Decidable.rec ...`. Peeled from #168 ### Testing: What tests have been run? Did `make all` succeed for your changes? Was conformance testing successful on an Aarch64 machine? `make all` succeeded, conformance succeeded. ### License: By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license. --------- Co-authored-by: Shilpi Goel <[email protected]>
leanprover · Sep 20, 2024 · f69c71f · f69c71f
1 parent 31a381d
commit f69c71f
Show file tree

Hide file tree

Showing 7 changed files with 21 additions and 21 deletions.
diff --git a/Arm/Insts/Common.lean b/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, 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]
@@ -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, 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]

diff --git a/Arm/Insts/DPI/Add_sub_imm.lean b/Arm/Insts/DPI/Add_sub_imm.lean
@@ -24,13 +24,18 @@ 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)
+    -- `carry, operand2` is written as a let binding followed by strucure projections to
+    -- work aroud a lean bug that desurgars `let (x, y) := if c then t else e` poorly:
+    -- https://github.com/leanprover/lean4/issues/5388
+    let carry := carryInAndOperand2.fst
+    let operand2 := carryInAndOperand2.snd
     let operand2         := BitVec.zeroExtend datasize operand2
-    let (result, pstate) := AddWithCarry operand1 operand2 carry_in
+    let (result, pstate) := 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'

diff --git a/Arm/Memory/SeparateProofs.lean b/Arm/Memory/SeparateProofs.lean
@@ -206,7 +206,6 @@ private theorem mem_subset_one_addr_region_lemma_helper (n1 addr1 addr2 : BitVec
 
 theorem mem_subset_one_addr_region_lemma (addr1 addr2 : BitVec 64) (h : n1 <= 2 ^ 64) :
   mem_subset addr1 (addr1 + (BitVec.ofNat 64 n1) - 1#64) addr2 addr2 → (n1 = 1) ∧ (addr1 = addr2) := by
-  -- simp (config := {ground := true}) at h
   simp [mem_subset]
   have h0 := mem_subset_one_addr_region_lemma_helper (BitVec.ofNat 64 n1) addr1 addr2
   have h1 : 0#64 ≠ 18446744073709551615#64 := by bv_omega

diff --git a/Proofs/Experiments/AddLoop/AddLoop.lean b/Proofs/Experiments/AddLoop/AddLoop.lean
@@ -307,7 +307,6 @@ theorem effects_of_nextc_from_0x4005a4
   obtain ⟨h_s0_pc, h_s0_program, h_s0_err, h_s0_sp_aligned⟩ := h_pre
   -- Symbolic simulation
   sym_n 2
-  simp (config := {ground := true}) only []
   rw [AddWithCarry.all_ones_zero_flag_64]
   done
 
@@ -588,8 +587,7 @@ theorem partial_correctness :
                 h_assert_x0 h_assert_x0_nz
         · apply And.intro
           · apply AddWithCarry.all_ones_zero_flag_64
-          · simp only [AddWithCarry.add_one_64]
-            rw [crock_lemma]
+          · rw [crock_lemma]
       case neg =>
         have h_effects :=
           @effects_of_nextc_from_0x4005b4_cond_holds_false s0 si sn

diff --git a/Proofs/Experiments/Max/MaxTandem.lean b/Proofs/Experiments/Max/MaxTandem.lean
@@ -150,15 +150,14 @@ theorem program.stepi_0x894_cut (s sn : ArmState)
   subst h_step
   have := Max.program.stepi_eq_0x894 h_program h_pc h_err
   -- clear Decidable.rec (...)
-  simp (config := { decide := true, ground := true }) only [minimal_theory] at this
+  simp only [minimal_theory] at this
   simp_all only [run, cut, this,
                  state_simp_rules, bitvec_rules, minimal_theory, pcs]
   simp only [List.mem_cons, BitVec.reduceEq, List.mem_singleton, or_self, not_false_eq_true,
     true_and, List.not_mem_nil, or_self, not_false_eq_true, true_and]
-  simp only [fst_AddWithCarry_eq_sub_neg, BitVec.reduceNot, true_and]
   /- Toy automation for deciding Aligned, will be converted to a decision procedure in a follow up PR -/
   repeat first
-  | simp (config := { ground := true, decide := true}) [aligned_rules, state_simp_rules]
+  | simp [aligned_rules, state_simp_rules]
   | apply Aligned_BitVecSub_64_4;
   | apply Aligned_BitVecAdd_64_4;
   | apply Aligned_AddWithCarry_64_4;
@@ -557,8 +556,8 @@ theorem program.stepi_0x8c8_cut (s sn : ArmState)
   have := program.stepi_eq_0x8c8 h_program h_pc h_err
   simp only [minimal_theory] at this
   simp_all only [run, cut, this, state_simp_rules, bitvec_rules, minimal_theory]
-  simp (config := {ground := true, decide := true})
-  simp only [fst_AddWithCarry_eq_add, true_and]
+  simp only [pcs, List.mem_cons, BitVec.reduceEq, List.mem_singleton, or_true, true_and, false_or,
+    true_or]
   apply Aligned_BitVecAdd_64_4
   · assumption
   · decide

diff --git a/Proofs/Popcount32.lean b/Proofs/Popcount32.lean
@@ -108,18 +108,18 @@ theorem popcount32_sym_meets_spec (s0 s_final : ArmState)
 
     -- (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]
+    sym_aggregate
     simp_mem
     rfl
-
+  · apply Aligned_BitVecSub_64_4
+    · assumption
+    · decide
+  · apply Aligned_BitVecAdd_64_4
+    · assumption
+    · decide
 
 -------------------------------------------------------------------------------
 

diff --git a/Proofs/SHA512/SHA512Sym.lean b/Proofs/SHA512/SHA512Sym.lean
@@ -75,9 +75,6 @@ theorem sha512_block_armv8_1block (s0 sf : ArmState)
   r (StateField.GPR 2#5) sf = 0#64 ∧
   r StateField.ERR sf = StateError.None := by
   sym_n 20
-
-  simp (config := {decide := true, ground := true}) only
-    [AddWithCarry, bitvec_rules, minimal_theory, Nat.reduceAdd]
   cse (config := { processHyps := .allHyps })
   sorry