From f259fa27cf54cfd14c70eb11861557bd445bbfb5 Mon Sep 17 00:00:00 2001
From: mamonet <maamoun.tk@gmail.com>
Date: Thu, 18 Apr 2024 08:06:45 +0200
Subject: [PATCH] Rename AES create_ctx to state_alloca

---
 code/aes/Hacl.AES_128.CTR32.NI.fst |  4 ++--
 code/aes/Hacl.AES_256.CTR32.NI.fst |  4 ++--
 code/aes/Hacl.Impl.AES.Generic.fst | 23 -----------------------
 3 files changed, 4 insertions(+), 27 deletions(-)

diff --git a/code/aes/Hacl.AES_128.CTR32.NI.fst b/code/aes/Hacl.AES_128.CTR32.NI.fst
index 615ec42b14..55fabc5b4c 100644
--- a/code/aes/Hacl.AES_128.CTR32.NI.fst
+++ b/code/aes/Hacl.AES_128.CTR32.NI.fst
@@ -20,7 +20,7 @@ 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 /\
@@ -28,7 +28,7 @@ val create_ctx: unit ->
     (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
index f94da04560..1e4480165b 100644
--- a/code/aes/Hacl.AES_256.CTR32.NI.fst
+++ b/code/aes/Hacl.AES_256.CTR32.NI.fst
@@ -20,7 +20,7 @@ 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 /\
@@ -28,7 +28,7 @@ val create_ctx: unit ->
     (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
index 8cb341864f..53247a3b58 100644
--- 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