From f8a5a0fe5a11dd45037f080693a055fd111fed15 Mon Sep 17 00:00:00 2001
From: Yan Peng <yppe@amazon.com>
Date: Wed, 11 Sep 2024 00:04:00 +0000
Subject: [PATCH] Proving correctness for h0 of gcm_init_v8

---
 Arm/Insts/Common.lean            | 74 +++++++++++++++++++++++++++++++-
 Proofs/AES-GCM/GCMInitV8Sym.lean |  9 +++-
 2 files changed, 79 insertions(+), 4 deletions(-)

diff --git a/Arm/Insts/Common.lean b/Arm/Insts/Common.lean
index 24b9a6fd..3f9f698a 100644
--- a/Arm/Insts/Common.lean
+++ b/Arm/Insts/Common.lean
@@ -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 :=
@@ -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)
@@ -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)
diff --git a/Proofs/AES-GCM/GCMInitV8Sym.lean b/Proofs/AES-GCM/GCMInitV8Sym.lean
index a17a8e41..87b40524 100644
--- a/Proofs/AES-GCM/GCMInitV8Sym.lean
+++ b/Proofs/AES-GCM/GCMInitV8Sym.lean
@@ -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
@@ -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
@@ -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