Fixing proofs

pennyannn · Sep 27, 2024 · 646696e · 646696e
1 parent b191bcf
commit 646696e
Show file tree

Hide file tree

Showing 4 changed files with 13 additions and 16 deletions.
diff --git a/Proofs/Experiments/Abs/Abs.lean b/Proofs/Experiments/Abs/Abs.lean
@@ -24,7 +24,7 @@ def spec (x : BitVec 32) : BitVec 32 :=
   -- BitVec.ofNat 32 x.toInt.natAbs
   -- because the above has functions like `toInt` that do not play well with
   -- bitblasting/LeanSAT.
-  let msb := BitVec.extractLsb 31 31 x
+  let msb := BitVec.extractLsb' 31 1 x
   if msb == 0#1 then
     x
   else

diff --git a/Proofs/Experiments/Abs/AbsVCG.lean b/Proofs/Experiments/Abs/AbsVCG.lean
@@ -39,7 +39,7 @@ def spec (x : BitVec 32) : BitVec 32 :=
   -- BitVec.ofNat 32 x.toInt.natAbs
   -- because the above has functions like `toInt` that do not play well with
   -- bitblasting/LeanSAT.
-  let msb := BitVec.extractLsb 31 31 x
+  let msb := BitVec.extractLsb' 31 1 x
   if msb == 0#1 then
     x
   else
@@ -205,12 +205,12 @@ theorem effects_of_nextc_from_0x4005d0 (h_pre : abs_pre s0)
   r (StateField.GPR 0#5) sn =
     BitVec.zeroExtend 64
       (AddWithCarry (BitVec.zeroExtend 32 (r (StateField.GPR 0x0#5) s0))
-          (BitVec.replicate 32 (BitVec.extractLsb 31 31 (BitVec.zeroExtend 32 (r (StateField.GPR 0x0#5) s0))) &&&
+          (BitVec.replicate 32 (BitVec.extractLsb' 31 1 (BitVec.zeroExtend 32 (r (StateField.GPR 0x0#5) s0))) &&&
               0xfffffffe#32 |||
             (BitVec.zeroExtend 32 (r (StateField.GPR 0x0#5) s0)).rotateRight 31 &&& 0xffffffff#32 &&& 0x1#32)
           0x0#1).fst ^^^
     (BitVec.zeroExtend 64
-          (BitVec.replicate 32 (BitVec.extractLsb 31 31 (BitVec.zeroExtend 32 (r (StateField.GPR 0x0#5) s0)))) &&&
+          (BitVec.replicate 32 (BitVec.extractLsb' 31 1 (BitVec.zeroExtend 32 (r (StateField.GPR 0x0#5) s0)))) &&&
         0xfffffffe#64 |||
       BitVec.zeroExtend 64 ((BitVec.zeroExtend 32 (r (StateField.GPR 0x0#5) s0)).rotateRight 31) &&& 0xffffffff#64 &&&
         0x1#64) ∧

diff --git a/Proofs/Experiments/Abs/AbsVCGTandem.lean b/Proofs/Experiments/Abs/AbsVCGTandem.lean
@@ -37,7 +37,7 @@ def spec (x : BitVec 32) : BitVec 32 :=
   -- BitVec.ofNat 32 x.toInt.natAbs
   -- because the above has functions like `toInt` that do not play well with
   -- bitblasting/LeanSAT.
-  let msb := BitVec.extractLsb 31 31 x
+  let msb := BitVec.extractLsb' 31 1 x
   if msb == 0#1 then
     x
   else
@@ -124,7 +124,7 @@ theorem program.stepi_0x4005d4_cut (s sn : ArmState)
   abs_cut sn = false  ∧
   r (StateField.GPR 0#5) sn =
     (BitVec.zeroExtend 64
-            (BitVec.replicate 32 (BitVec.extractLsb 31 31 (BitVec.zeroExtend 32 (r (StateField.GPR 0x0#5) s)))) &&&
+            (BitVec.replicate 32 (BitVec.extractLsb' 31 1 (BitVec.zeroExtend 32 (r (StateField.GPR 0x0#5) s)))) &&&
           0xfffffffe#64 |||
         BitVec.zeroExtend 64 ((BitVec.zeroExtend 32 (r (StateField.GPR 0x0#5) s)).rotateRight 31) &&& 0xffffffff#64 &&&
           0x1#64) ∧

diff --git a/Proofs/Experiments/Memcpy/MemCpyVCG.lean b/Proofs/Experiments/Memcpy/MemCpyVCG.lean
@@ -268,11 +268,10 @@ theorem program.step_8e4_8e8_of_wellformed_of_stepped (scur snext : ArmState)
   obtain h_sp_aligned := hscur.h_sp_aligned
 
   have := program.stepi_eq_0x8e4 h_program h_pc h_err
-  simp [BitVec.extractLsb] at this
   obtain ⟨h_step⟩ := hstep
   subst h_step
   constructor <;> simp only [*, cut, state_simp_rules, minimal_theory, bitvec_rules]
-  · constructor <;> simp [*, state_simp_rules, minimal_theory, BitVec.extractLsb]
+  · constructor <;> simp [*, state_simp_rules, minimal_theory]
 
 -- 3/7 (0x8e8#64, 0x3c810444#32),  /- str q4, [x2], #16        -/
 structure Step_8e8_8ec (scur : ArmState) (snext : ArmState) extends WellFormedAtPc snext 0x8ec : Prop where
@@ -296,7 +295,6 @@ theorem program.step_8e8_8ec_of_wellformed (scur snext : ArmState)
   obtain h_sp_aligned := hscur.h_sp_aligned
 
   have := program.stepi_eq_0x8e8 h_program h_pc h_err
-  simp [BitVec.extractLsb] at this
   obtain ⟨h_step⟩ := hstep
   subst h_step
   constructor
@@ -335,11 +333,10 @@ theorem program.step_8ec_8f0_of_wellformed (scur snext : ArmState)
   obtain h_sp_aligned := hs.h_sp_aligned
 
   have := program.stepi_eq_0x8ec h_program h_pc h_err
-  simp [BitVec.extractLsb] at this
   obtain ⟨h_step⟩ := hstep
   subst h_step
   constructor <;> simp (config := { ground := true, decide := true}) [*,
-      state_simp_rules, minimal_theory, BitVec.extractLsb, fst_AddWithCarry_eq_sub_neg, memory_rules]
+      state_simp_rules, minimal_theory, fst_AddWithCarry_eq_sub_neg, memory_rules]
   · constructor <;> simp [*, state_simp_rules, minimal_theory, bitvec_rules, memory_rules]
 
 -- 5/7 (0x8f0#64, 0xf100001f#32),  /- cmp x0, #0x0             -/
@@ -364,7 +361,7 @@ theorem program.step_8f0_8f4_of_wellformed (scur snext : ArmState)
   obtain h_sp_aligned := hs.h_sp_aligned
 
   have := program.stepi_eq_0x8f0 h_program h_pc h_err
-  simp (config := { ground := true, decide := true}) [BitVec.extractLsb,
+  simp (config := { ground := true, decide := true}) [
     fst_AddWithCarry_eq_sub_neg,
     fst_AddWithCarry_eq_add] at this
   obtain ⟨h_step⟩ := hstep
@@ -396,14 +393,14 @@ theorem program.step_8f4_8e4_of_wellformed_of_z_eq_0 (scur snext : ArmState)
   obtain h_sp_aligned := hs.h_sp_aligned
 
   have := program.stepi_eq_0x8f4 h_program h_pc h_err
-  simp (config := { ground := true, decide := true}) [BitVec.extractLsb,
+  simp (config := { ground := true, decide := true}) [
     fst_AddWithCarry_eq_sub_neg,
     fst_AddWithCarry_eq_add] at this
   obtain ⟨h_step⟩ := hstep
   subst h_step
   constructor <;> solve
     | simp (config := { ground := true, decide := true}) [*,
-      state_simp_rules, minimal_theory, BitVec.extractLsb, fst_AddWithCarry_eq_sub_neg]
+      state_simp_rules, minimal_theory, fst_AddWithCarry_eq_sub_neg]
   · constructor <;> simp [*, state_simp_rules, minimal_theory, bitvec_rules]
 
 -- 6/7 (0x8f4#64, 0x54ffff81#32),  /- b.ne 8e4 <mem_copy_loop> -/
@@ -426,14 +423,14 @@ theorem program.step_8f4_8f8_of_wellformed_of_z_eq_1 (scur snext : ArmState)
   obtain h_sp_aligned := hs.h_sp_aligned
 
   have := program.stepi_eq_0x8f4 h_program h_pc h_err
-  simp (config := { ground := true, decide := true}) [BitVec.extractLsb,
+  simp (config := { ground := true, decide := true}) [
     fst_AddWithCarry_eq_sub_neg,
     fst_AddWithCarry_eq_add] at this
   obtain ⟨h_step⟩ := hstep
   subst h_step
   constructor <;>
     simp (config := { ground := true, decide := true}) [*, state_simp_rules, h_z,
-      minimal_theory, BitVec.extractLsb, fst_AddWithCarry_eq_sub_neg, cut]
+      minimal_theory, fst_AddWithCarry_eq_sub_neg, cut]
   · constructor <;> simp [*, h_z, state_simp_rules, minimal_theory, bitvec_rules, cut]
 
 end CutTheorems