From e9e91a2d373f5eae0ae0844fe2aca85adb9bad61 Mon Sep 17 00:00:00 2001 From: mamonet Date: Fri, 16 Feb 2024 22:35:42 +0200 Subject: [PATCH] Update Hacl.Impl.AES.Generic.fst --- code/aes/Hacl.Impl.AES.Generic.fst | 8 ++++---- specs/Spec.AES.fst | 4 ++-- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/code/aes/Hacl.Impl.AES.Generic.fst b/code/aes/Hacl.Impl.AES.Generic.fst index 23c8815e6b..d2716de40b 100644 --- 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 index f3a92d692f..993bcdc989 100644 --- 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