From 43f9a435478fa89a2d1c13a370767a450e83b640 Mon Sep 17 00:00:00 2001
From: Andrei <andrei@stefanescu.io>
Date: Thu, 21 Dec 2023 06:43:30 +0000
Subject: [PATCH] wip

---
 SAW/proof/Loop.cry      | 2 --
 SAW/proof/loop_test.saw | 6 +++---
 2 files changed, 3 insertions(+), 5 deletions(-)

diff --git a/SAW/proof/Loop.cry b/SAW/proof/Loop.cry
index 98cc78f2..bc7a278b 100644
--- a/SAW/proof/Loop.cry
+++ b/SAW/proof/Loop.cry
@@ -248,7 +248,6 @@ aesni_gcm_encrypt_impl_loop_step len in out key ivec ctr Xi
  where
   //next_prefetch_offset = prefetch_offset + (if prefetch_offset + 192 <= len then 96 else 0)
   next_prefetch_offset = prefetch_offset + (if prefetch_offset + 4096 <= len + 3904 then 96 else 0)
-  //next_prefetch_offset = prefetch_offset + (if prefetch_offset <= len - 192 then 96 else 0)
 
   [in_block0, in_block1, in_block2, in_block3, in_block4, in_block5] = split (join (arrayRangeLookup in (loop_index * 96 + 192)))
   (next_T1, [out_block0, out_block1, out_block2, out_block3, out_block4, out_block5]) = aes_encrypt_blocks_6_impl key ctr_least_byte T1 inout0 inout1 inout2 inout3 inout4 inout5 [in_block0, in_block1, in_block2, in_block3, in_block4, in_block5]
@@ -259,7 +258,6 @@ aesni_gcm_encrypt_impl_loop_step len in out key ivec ctr Xi
   enc_block3 = prefetch6 # prefetch7
   enc_block4 = prefetch8 # prefetch9
   enc_block5 = drop Z3
-
   blocks = [enc_block0, enc_block1, enc_block2, enc_block3, enc_block4, enc_block5]
   (next_spill_Z3, next_loop_Xi, next_Z0) = gcm_polyval_pmult4_impl key spill_Z3 (drop loop_Xi) (drop Z0) blocks
 
diff --git a/SAW/proof/loop_test.saw b/SAW/proof/loop_test.saw
index bce43a0a..6d034847 100644
--- a/SAW/proof/loop_test.saw
+++ b/SAW/proof/loop_test.saw
@@ -1,9 +1,8 @@
 enable_experimental;
 disable_debug_intrinsics;
 
-//import "../../../aws-lc-verification/cryptol-specs/Common/ByteArray.cry";
-import "../../../aws-lc-verification/cryptol-specs/Primitive/Symmetric/Cipher/Block/AES.cry";
-import "../../../aws-lc-verification/cryptol-specs/Primitive/Symmetric/Cipher/Authenticated/AES_256_GCM.cry";
+import "../../cryptol-specs/Primitive/Symmetric/Cipher/Block/AES.cry";
+import "../../cryptol-specs/Primitive/Symmetric/Cipher/Authenticated/AES_256_GCM.cry";
 import "../spec/AES/AES-GCM.cry";
 import "../spec/AES/X86.cry";
 import "../spec/AES/AES-GCM-implementation.cry";
@@ -97,6 +96,7 @@ include "AES/goal-rewrites.saw";
 include "AES/AES.saw";
 include "AES/GHASH.saw";
 //include "AES/AESNI-GCM.saw";
+let do_prove = true;
 
 let fresh_aes_key_st = do {
   crucible_fresh_var "key" (llvm_array aes_key_len (llvm_int 8));