From 3eff2f53864d3f476c4df2e6334132bac22f2cc8 Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Fri, 13 Sep 2024 00:50:52 +0000 Subject: [PATCH] Playing with the RShr proof --- Arm/BitVec.lean | 1 + Arm/Insts/Common.lean | 119 ++++++++++++++++++++++--------- Proofs/AES-GCM/GCMInitV8Sym.lean | 3 +- 3 files changed, 88 insertions(+), 35 deletions(-) diff --git a/Arm/BitVec.lean b/Arm/BitVec.lean index 1e59e45a..ab68a46d 100644 --- a/Arm/BitVec.lean +++ b/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 diff --git a/Arm/Insts/Common.lean b/Arm/Insts/Common.lean index 3f9f698a..c92f959f 100644 --- a/Arm/Insts/Common.lean +++ b/Arm/Insts/Common.lean @@ -643,11 +643,12 @@ 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 := - if unsigned then value.toNat else value.toInt + if unsigned then Int.ofNat value.toNat else value.toInt def shift_right_common_aux (e : Nat) (info : ShiftInfo) (operand : BitVec datasize) @@ -664,32 +665,44 @@ 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 crock3 (x : BitVec 64) (shift : Nat) : + extractLsb 63 0 ((zeroExtend 65 x).ushiftRight shift) = ushiftRight x shift := by + sorry + +theorem crock2 (shift : Nat) (result : BitVec 128) + (x : BitVec 64) (y : BitVec 64) + : (result &&& 340282366920938463444927863358058659840#128 ||| + zeroExtend 128 (extractLsb 63 0 ((zeroExtend 65 x).ushiftRight shift))) &&& + 18446744073709551615#128 ||| + zeroExtend 128 (extractLsb 63 0 ((zeroExtend 65 y).ushiftRight shift)) <<< 64 = + y.ushiftRight shift ++ x.ushiftRight shift + := by + simp only [crock3] + generalize x.ushiftRight shift = x + generalize y.ushiftRight shift = y + bv_decide +-- (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 @@ -697,19 +710,57 @@ theorem shift_right_common_aux_64_2_tff (operand : BitVec 128) 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 + /- + operand : BitVec 128 + shift : Nat + result : BitVec 128 + x : BitVec (63 - 0 + 1) + y : BitVec (127 - 64 + 1) + ⊢ (result &&& 340282366920938463444927863358058659840#128 ||| + zeroExtend 128 (extractLsb 63 0 ((zeroExtend 65 x).ushiftRight shift))) &&& + 18446744073709551615#128 ||| + zeroExtend 128 (extractLsb 63 0 ((zeroExtend 65 y).ushiftRight shift)) <<< 64 = + y.ushiftRight shift ++ x.ushiftRight shift + -/ + generalize (extractLsb 127 64 operand) = y + apply crock2 theorem shift_right_common_aux_32_4_fff (operand : BitVec 128) (shift : Nat) (result : BitVec 128): diff --git a/Proofs/AES-GCM/GCMInitV8Sym.lean b/Proofs/AES-GCM/GCMInitV8Sym.lean index 87b40524..cffbe43b 100644 --- a/Proofs/AES-GCM/GCMInitV8Sym.lean +++ b/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)