From 16a1dd93aaf3ae1e41119fe2efcb5990800a2f3d Mon Sep 17 00:00:00 2001
From: Yan Peng <112029182+pennyannn@users.noreply.github.com>
Date: Tue, 12 Nov 2024 08:33:56 -0800
Subject: [PATCH] Update the gcm_init_v8 proof (#245)

### Description:

Update the gcm_init_v8 proof by using `Memory.read_bytes` and update the
autogenerated `simp only`.

### Testing:

What tests have been run? Did `make all` succeed for your changes? Was
conformance testing successful on an Aarch64 machine? Yes.

### License:

By submitting this pull request, I confirm that my contribution is
made under the terms of the Apache 2.0 license.
---
 Proofs/AES-GCM/GCMInitV8Sym.lean | 45 +++++++-------------------------
 1 file changed, 10 insertions(+), 35 deletions(-)

diff --git a/Proofs/AES-GCM/GCMInitV8Sym.lean b/Proofs/AES-GCM/GCMInitV8Sym.lean
index 97398f5b..c5edc1b6 100644
--- a/Proofs/AES-GCM/GCMInitV8Sym.lean
+++ b/Proofs/AES-GCM/GCMInitV8Sym.lean
@@ -16,25 +16,7 @@ set_option bv.ac_nf false
 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 maxRecDepth 8000 in
--- set_option profiler true in
-theorem gcm_init_v8_program_run_152 (s0 sf : ArmState)
-    (h_s0_program : s0.program = gcm_init_v8_program)
-    (h_s0_err : read_err s0 = .None)
-    (h_s0_pc : read_pc s0 = gcm_init_v8_program.min)
-    (h_s0_sp_aligned : CheckSPAlignment s0)
-    (h_run : sf = run gcm_init_v8_program.length s0)
-    (_h_mem : Memory.Region.pairwiseSeparate
-      [ ⟨(H_addr s0), 128⟩,
-        ⟨(Htable_addr s0), 2048⟩ ])
-    : read_err sf = .None := by
-  simp (config := {ground := true}) only at h_s0_pc
-  -- ^^ Still needed, because `gcm_init_v8_program.min` is somehow
-  --    unable to be reflected
-  sym_n 152
-  done
-
-set_option maxRecDepth 100000 in
+set_option maxRecDepth 2000 in
 set_option maxHeartbeats 500000 in
 set_option sat.timeout 120 in
 -- set_option pp.deepTerms true in
@@ -93,19 +75,15 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState)
   --    unable to be reflected
   sym_n 152
   simp only [Htable_addr, state_value] -- TODO: state_value is needed, why
-  apply And.intro  
+  apply And.intro
   · bv_decide
-  · sorry
-  -- [Shilpi] Commenting out the following because the CI fails with 
-  -- "INTERNAL PANIC: out of memory"
-  /-
-    simp only
+  · simp only
     [shift_left_common_aux_64_2
     , shift_right_common_aux_64_2_tff
     , shift_right_common_aux_32_4_fff
     , DPSFP.AdvSIMDExpandImm
     , DPSFP.dup_aux_0_4_32]
-    generalize read_mem_bytes 16 (r (StateField.GPR 1#5) s0) s0 = Hinit
+    generalize Memory.read_bytes 16 (r (StateField.GPR 1#5) s0) s0.mem = Hinit
     -- change the type of Hinit to be BitVec 128, assuming that's def-eq
     change BitVec 128 at Hinit
     simp only [GCMV8.GCMInitV8, GCMV8.lo, List.get!, GCMV8.hi,
@@ -113,12 +91,9 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState)
       GCMV8.reduce, GCMV8.degree, GCMV8.degree.degreeTR]
     simp only [Nat.reduceAdd, BitVec.ushiftRight_eq, BitVec.reduceExtracLsb',
       BitVec.reduceHShiftLeft, BitVec.reduceAppend, BitVec.reduceHShiftRight, BitVec.ofNat_eq_ofNat,
-      BitVec.reduceEq, ↓reduceIte, BitVec.zero_eq, Nat.sub_self, BitVec.ushiftRight_zero_eq,
-      BitVec.reduceAnd, BitVec.toNat_ofNat, Nat.pow_one, Nat.reduceMod, Nat.mul_zero, Nat.add_zero,
-      Nat.zero_mod, Nat.zero_add, Nat.sub_zero, Nat.mul_one, Nat.zero_mul, Nat.one_mul,
-      Nat.reduceSub, BitVec.reduceMul, BitVec.reduceXOr, BitVec.mul_one, Nat.add_one_sub_one,
-      BitVec.one_mul]
-    -- bv_check "lrat_files/GCMInitV8Sym.lean-GCMInitV8Program.gcm_init_v8_program_correct-117-4.lrat"
-    -- TODO: proof works in vscode but timeout in the CI -- need to investigate further
-    -/
-
+      BitVec.reduceEq, ↓reduceIte, Nat.sub_self, BitVec.ushiftRight_zero_eq, BitVec.reduceAnd,
+      BitVec.toNat_ofNat, Nat.pow_one, Nat.reduceMod, Nat.mul_zero, Nat.add_zero, Nat.zero_mod,
+      Nat.zero_add, Nat.sub_zero, Nat.mul_one, Nat.zero_mul, Nat.one_mul, Nat.reduceSub,
+      BitVec.and_self, BitVec.zero_and, BitVec.reduceMul, BitVec.xor_zero, BitVec.mul_one,
+      BitVec.zero_xor, Nat.add_one_sub_one, BitVec.one_mul, BitVec.reduceXOr]
+    bv_decide