Skip to content

Commit

Permalink
Proving correctness for h0 of gcm_init_v8
Browse files Browse the repository at this point in the history
  • Loading branch information
pennyannn committed Sep 11, 2024
1 parent 4744656 commit f8a5a0f
Show file tree
Hide file tree
Showing 2 changed files with 79 additions and 4 deletions.
74 changes: 72 additions & 2 deletions Arm/Insts/Common.lean
Original file line number Diff line number Diff line change
Expand Up @@ -643,8 +643,7 @@ def RShr (unsigned : Bool) (value : Int) (shift : Nat) (round : Bool) (h : n > 0
BitVec.ofInt (n + 1) rounded
else
BitVec.ofInt (n + 1) value
have h₀ : n - 1 - 0 + 1 = n := by omega
BitVec.cast h₀ $ extractLsb (n-1) 0 (fn rounded_bv shift)
extractLsb' 0 n (fn rounded_bv shift)

@[state_simp_rules]
def Int_with_unsigned (unsigned : Bool) (value : BitVec n) : Int :=
Expand All @@ -664,6 +663,66 @@ def shift_right_common_aux
shift_right_common_aux (e + 1) info operand operand2 result
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
-/


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
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

theorem shift_right_common_aux_32_4_fff (operand : BitVec 128)
(shift : Nat) (result : BitVec 128):
shift_right_common_aux 0
{ esize := 32, elements := 4, shift := shift,
unsigned := false, round := false, accumulate := false,
h := (by omega) }
operand 0#128 result =
(sshiftRight (extractLsb' 96 32 operand) shift)
++ (sshiftRight (extractLsb' 64 32 operand) shift)
++ (sshiftRight (extractLsb' 32 32 operand) shift)
++ (sshiftRight (extractLsb' 0 32 operand) shift) := by sorry

@[state_simp_rules]
def shift_right_common
(info : ShiftInfo) (datasize : Nat) (Rn : BitVec 5) (Rd : BitVec 5)
Expand All @@ -686,6 +745,17 @@ def shift_left_common_aux
shift_left_common_aux (e + 1) info operand result
termination_by (info.elements - e)

theorem shift_left_common_aux_64_2 (operand : BitVec 128)
(shift : Nat) (unsigned: Bool) (round : Bool) (accumulate : Bool)
(result : BitVec 128):
shift_left_common_aux 0
{esize := 64, elements := 2, shift := shift,
unsigned := unsigned, round := round, accumulate := accumulate,
h := (by omega)}
operand result =
(extractLsb' 0 64 operand <<< shift)
++ (extractLsb' 64 64 operand <<< shift) := by sorry

@[state_simp_rules]
def shift_left_common
(info : ShiftInfo) (datasize : Nat) (Rn : BitVec 5) (s : ArmState)
Expand Down
9 changes: 7 additions & 2 deletions Proofs/AES-GCM/GCMInitV8Sym.lean
Original file line number Diff line number Diff line change
Expand Up @@ -60,7 +60,7 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState)
∧ H_addr sf = H_addr s0
-- v20 - v31 stores results of Htable
∧ read_sfp 128 20#5 sf = (GCMV8.GCMInitV8 (read_mem_bytes 16 (H_addr s0) s0)).get! 0
-- ∧ read_sfp 128 21#5 sf = (GCMV8.GCMInitV8 (read_mem_bytes 16 (H_addr s0) s0)).get! 1
--
-- TODO: Commenting out memory related conjuncts since it seems
-- to make symbolic execution stuck
-- -- First 12 elements in Htable is correct
Expand All @@ -73,6 +73,7 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState)
-- ∧ (∀ (f : StateField), ¬ (f = StateField.PC) ∧
-- ¬ (f = (StateField.GPR 29#5)) →
-- r f sf = r f s0)
--
-- -- Memory safety: memory location that should not change did
-- -- not change
-- -- The addr exclude output region Htable
Expand All @@ -86,4 +87,8 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState)
simp only [Htable_addr, state_value] -- TODO: state_value is needed, why
apply And.intro
· bv_decide
· sorry
· simp only
[shift_left_common_aux_64_2
, shift_right_common_aux_64_2_tff
, shift_right_common_aux_32_4_fff];
sorry

0 comments on commit f8a5a0f

Please sign in to comment.