Update Hacl.Impl.AES.Generic.fst

mamonet · Feb 16, 2024 · e9e91a2 · e9e91a2
1 parent 9cf5c70
commit e9e91a2
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 6 deletions.
diff --git a/code/aes/Hacl.Impl.AES.Generic.fst b/code/aes/Hacl.Impl.AES.Generic.fst
@@ -140,11 +140,11 @@ val enc_rounds:
   Stack unit
   (requires (fun h -> live h s /\ live h key /\ disjoint s key))
   (ensures (fun h0 _ h1 -> modifies (loc s) h0 h1 /\
-    (let state' = (state_to_bytes m (as_seq h1 s) 0, state_to_bytes m (as_seq h1 s) 1,
+    (let state' = (state_to_bytes m (as_seq h0 s) 0, state_to_bytes m (as_seq h0 s) 1,
+      state_to_bytes m (as_seq h0 s) 2, state_to_bytes m (as_seq h0 s) 3) in
+    let state'' = (state_to_bytes m (as_seq h1 s) 0, state_to_bytes m (as_seq h1 s) 1,
       state_to_bytes m (as_seq h1 s) 2, state_to_bytes m (as_seq h1 s) 3) in
-    state' == Spec.aes_enc_rounds_4 a (keys_to_bytes m a (as_seq h0 key))
-      (state_to_bytes m (as_seq h0 s) 0) (state_to_bytes m (as_seq h0 s) 1)
-      (state_to_bytes m (as_seq h0 s) 2) (state_to_bytes m (as_seq h0 s) 3))))
+    state'' == Spec.aes_enc_rounds_4 a (keys_to_bytes m a (as_seq h0 key)) state')))
 
 let enc_rounds #m #a s key =
   [@ inline_let]

diff --git a/specs/Spec.AES.fst b/specs/Spec.AES.fst
@@ -310,8 +310,8 @@ let aes_enc_inner_4 (v:variant) (key:aes_ikey v) (i:size_nat{i < (num_rounds v-1
 val aes_enc_rounds_4_s: v:variant -> i:size_nat{i <= (num_rounds v-1)} -> Type0
 let aes_enc_rounds_4_s v i = block & block & block & block
 
-let aes_enc_rounds_4 (v:variant) (key:aes_ikey v) (s0 s1 s2 s3:block) : Tot (block & block & block & block) =
-  repeat_gen (num_rounds v-1) (aes_enc_rounds_4_s v) (aes_enc_inner_4 v key) (s0,s1,s2,s3)
+let aes_enc_rounds_4 (v:variant) (key:aes_ikey v) state : Tot (block & block & block & block) =
+  repeat_gen (num_rounds v-1) (aes_enc_rounds_4_s v) (aes_enc_inner_4 v key) state
 
 let aes_encrypt_block (v:variant) (key:aes_xkey v) (input:block) : Tot block =
   let state = input in