Rename AES create_ctx to state_alloca

mamonet · Apr 18, 2024 · f259fa2 · f259fa2
1 parent 6755bbf
commit f259fa2
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 27 deletions.
diff --git a/code/aes/Hacl.AES_128.CTR32.NI.fst b/code/aes/Hacl.AES_128.CTR32.NI.fst
@@ -20,15 +20,15 @@ let aes_ctx = aes_ctx MAES Spec.AES128
 let skey = skey Spec.AES128
 
 inline_for_extraction noextract
-val create_ctx: unit ->
+val state_alloca: unit ->
   StackInline aes_ctx
   (requires (fun h -> True))
   (ensures  (fun h0 f h1 -> live h1 f /\
     stack_allocated f h0 h1 (Seq.create (size_v (ctxlen MAES Spec.AES128))
     (elem_zero MAES))))
 
 inline_for_extraction noextract
-let create_ctx () = create_ctx MAES Spec.AES128
+let state_alloca () = create_ctx MAES Spec.AES128
 
 inline_for_extraction
 val state_malloc:

diff --git a/code/aes/Hacl.AES_256.CTR32.NI.fst b/code/aes/Hacl.AES_256.CTR32.NI.fst
@@ -20,15 +20,15 @@ let aes_ctx = aes_ctx MAES Spec.AES256
 let skey = skey Spec.AES256
 
 inline_for_extraction noextract
-val create_ctx: unit ->
+val state_alloca: unit ->
   StackInline aes_ctx
   (requires (fun h -> True))
   (ensures  (fun h0 f h1 -> live h1 f /\
     stack_allocated f h0 h1 (Seq.create (size_v (ctxlen MAES Spec.AES256))
     (elem_zero MAES))))
 
 inline_for_extraction noextract
-let create_ctx () = create_ctx MAES Spec.AES256
+let state_alloca () = create_ctx MAES Spec.AES256
 
 inline_for_extraction
 val state_malloc:

diff --git a/code/aes/Hacl.Impl.AES.Generic.fst b/code/aes/Hacl.Impl.AES.Generic.fst
@@ -1408,29 +1408,6 @@ let aes_encrypt_block #m #a ob ctx ib =
   pop_frame()
 
 
-inline_for_extraction noextract
-val aes_ctr32_key_block:
-    #m: m_spec
-  -> #a: Spec.variant
-  -> out: lbuffer uint8 16ul
-  -> kex: lbuffer (stelem m) ((nr a +! 1ul) *. klen m)
-  -> nonce: lbuffer (stelem m) (nlen m)
-  -> st: lbuffer (stelem m) (stlen m)
-  -> counter: uint32
-  -> Stack unit
-  (requires (fun h -> live h out /\ live h kex /\ live h nonce /\
-    live h st /\ disjoint st kex))
-  (ensures (fun h0 _ h1 -> modifies2 out st h0 h1 /\
-    as_seq h1 out == u8_16_to_le (Spec.aes_encrypt_block a
-      (as_kex m a h0 kex) (Spec.aes_ctr32_set_counter_LE
-      (as_nonce m h0 nonce) counter))))
-
-let aes_ctr32_key_block #m #a out kex nonce st counter =
-  load_state #m st nonce counter;
-  block_cipher #m #a st kex;
-  store_block0 #m out st
-
-
 val aes_ctr32_encrypt_block_lemma:
     #m:m_spec
   -> #a: Spec.variant