Playing with the RShr proof

Arm/BitVec.lean

@@ -287,6 +287,7 @@ abbrev lsb (x : BitVec n) (i : Nat) : BitVec 1 :=
   -- by LeanSAT.
   (BitVec.extractLsb i i x).cast (by omega)
 
+@[state_simp_rules]
 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

@@ -643,7 +643,8 @@ def RShr (unsigned : Bool) (value : Int) (shift : Nat) (round : Bool) (h : n > 0
       BitVec.ofInt (n + 1) rounded
     else
       BitVec.ofInt (n + 1) value
-  extractLsb' 0 n (fn rounded_bv shift)
+  have h₀ : n - 1 - 0 + 1 = n := by omega
+  BitVec.cast h₀ $ extractLsb (n-1) 0 (fn rounded_bv shift)
 
 @[state_simp_rules]
 def Int_with_unsigned (unsigned : Bool) (value : BitVec n) : Int :=
@@ -664,52 +665,81 @@ def shift_right_common_aux
   termination_by (info.elements - e)
 
 
-theorem crock (operand : BitVec 128) :
-  (BitVec.ofNat 65 (operand.toNat % 18446744073709551616)) = zeroExtend 65 (extractLsb' 0 64 operand)
-  := by sorry
-
-theorem crock1 (operand : BitVec 128) :
-  (BitVec.ofNat 65 (operand.toNat >>> 64 % 18446744073709551616)) = zeroExtend 65 (extractLsb' 64 64 operand)
-  := by sorry
-
-
-/-
-unsolved goals
-
-operand : BitVec 128
-shift : Nat
-result : BitVec 128
-⊢ (result &&& 340282366920938463444927863358058659840#128 |||
-        zeroExtend 128
-          (extractLsb' 0 64 ((BitVec.ofNat 65 (operand.toNat % 18446744073709551616)).ushiftRight shift))) &&&
-      18446744073709551615#128 |||
-    zeroExtend 128
-        (extractLsb' 0 64 ((BitVec.ofNat 65 (operand.toNat >>> 64 % 18446744073709551616)).ushiftRight shift)) <<<
-      64 =
-  (extractLsb' 64 64 operand).ushiftRight shift ++ (extractLsb' 0 64 operand).ushiftRight shift
--/
-
-
+-- @[app_unexpander BitVec.ofNat] def unexpandBitVecOfNatToHex : Lean.PrettyPrinter.Unexpander
+--   | `($(_) $n:num $i:num) =>
+--       let i' := i.getNat
+--       let n' := n.getNat
+--       let trimmed_hex := -- Remove leading zeroes...
+--         String.dropWhile (BitVec.ofNat n' i').toHex
+--                          (fun c => c = '0')
+--                          -- ... but keep one if the literal is all zeros.
+--       let trimmed_hex := if trimmed_hex.isEmpty then "0" else trimmed_hex
+--       let bv := Lean.Syntax.mkNumLit s!"0x{trimmed_hex}#{n'}"
+--       `($bv:num)
+--   | _ => throw ()
+
+theorem crock1 (x : BitVec 64): BitVec.ofInt 65 (Int.ofNat x.toNat) = zeroExtend 65 x := by
+  simp only [Int.ofNat_eq_coe, ofInt_natCast, ofNat_toNat]
+
+theorem crock2 (operand : BitVec 128) (shift : Nat) (result : BitVec 128)
+  (x : BitVec 64) (y : BitVec 64)
+  : (result &&& 340282366920938463444927863358058659840#128 |||
+          zeroExtend 128 (extractLsb 63 0 (zeroExtend 65 x >>> shift))) &&&
+        18446744073709551615#128 |||
+      zeroExtend 128 (extractLsb 63 0 (zeroExtend 65 y >>> shift)) <<< 64 =
+    y >>> shift ++ x >>> shift := by
+    sorry
+
+-- (BitVec.cast ⋯ (extractLsb 63 0 operand)).toNat
+-- --> (operand.toNat % 18446744073709551616)
+-- extractLsb_toNat is the lemma that turned extractLsb into mod operation in Nat
+-- This makes it hard to use bv_decide
 theorem shift_right_common_aux_64_2_tff (operand : BitVec 128)
   (shift : Nat) (result : BitVec 128):
   shift_right_common_aux 0
     {esize := 64, elements := 2, shift := shift,
      unsigned := true, round := false, accumulate := false,
      h := (by omega)}
     operand 0#128 result =
-  (ushiftRight (extractLsb' 64 64 operand) shift)
-    ++ (ushiftRight (extractLsb' 0 64 operand) shift) := by
+  (ushiftRight (extractLsb 127 64 operand) shift)
+    ++ (ushiftRight (extractLsb 63 0 operand) shift) := by
   unfold shift_right_common_aux
   simp only [minimal_theory, bitvec_rules]
   unfold shift_right_common_aux
   simp only [minimal_theory, bitvec_rules]
   unfold shift_right_common_aux
   simp only [minimal_theory, bitvec_rules]
-  simp only [state_simp_rules, partInstall,
-             minimal_theory, bitvec_rules,
-             Nat.shiftRight_zero, Nat.zero_shiftRight,
-             crock, crock1]
-  -- bv_decide
+  simp only [-- -extractLsb_toNat,
+             state_simp_rules,
+             minimal_theory,
+             -- bitvec_rules,
+             BitVec.cast_eq,
+             Nat.shiftRight_zero,
+             Nat.zero_shiftRight,
+             Nat.reduceMul,
+             Nat.reduceAdd,
+             Nat.add_one_sub_one,
+             Nat.sub_zero,
+             reduceAllOnes,
+             reduceZeroExtend,
+             Nat.zero_mul,
+             shiftLeft_zero_eq,
+             reduceNot,
+             BitVec.extractLsb_ofNat,
+             Nat.reducePow,
+             Nat.zero_mod,
+             Int.ofNat_emod,
+             Int.Nat.cast_ofNat_Int,
+             BitVec.zero_add,
+             Nat.reduceSub,
+             Nat.one_mul,
+             reduceHShiftLeft,
+             ushiftRight_eq,
+             crock1
+    ]
+  generalize (extractLsb 63 0 operand) = x
+  generalize (extractLsb 127 64 operand) = y
+  apply crock2
 
 theorem shift_right_common_aux_32_4_fff (operand : BitVec 128)
   (shift : Nat) (result : BitVec 128):

Proofs/AES-GCM/GCMInitV8Sym.lean

@@ -14,7 +14,7 @@ namespace GCMInitV8Program
 abbrev H_addr (s : ArmState) : BitVec 64 := r (StateField.GPR 1#5) s
 abbrev Htable_addr (s : ArmState) : BitVec 64 := r (StateField.GPR 0#5) s
 
--- set_option debug.byAsSorry true in
+set_option debug.byAsSorry true in
 set_option maxRecDepth 1000000 in
 -- set_option profiler true in
 theorem gcm_init_v8_program_run_152 (s0 sf : ArmState)
@@ -35,6 +35,7 @@ theorem gcm_init_v8_program_run_152 (s0 sf : ArmState)
 
 set_option maxRecDepth 1000000 in
 set_option maxHeartbeats 2000000 in
+-- set_option linter.unusedVariables false
 -- set_option profiler true in
 theorem gcm_init_v8_program_correct (s0 sf : ArmState)
     (h_s0_program : s0.program = gcm_init_v8_program)