Rename AES-CTR32 high-level functions

mamonet · May 29, 2024 · 1c57c38 · 1c57c38
1 parent f5a7543
commit 1c57c38
Show file tree

Hide file tree

Showing 9 changed files with 61 additions and 81 deletions.
diff --git a/code/aes/Hacl.AES_128.CTR32.NI.fst b/code/aes/Hacl.AES_128.CTR32.NI.fst
@@ -79,7 +79,7 @@ let context_free s =
   B.free s
 
 [@@ Comment "Initiate AES-128 context buffer with key expansion and nonce"]
-val aes128_init:
+val init:
     ctx: aes_ctx
   -> key: skey
   -> nonce: lbuffer uint8 12ul ->
@@ -92,11 +92,11 @@ val aes128_init:
     get_nonce_s MAES Spec.AES128 h1 ctx == state.block /\
     get_kex_s MAES Spec.AES128 h1 ctx == state.key_ex)))
 
-let aes128_init ctx key nonce = aes128_ni_init ctx key nonce
+let init ctx key nonce = aes128_ni_init ctx key nonce
 
 
 [@@ Comment "Set nonce in AES-128 context buffer"]
-val aes128_set_nonce:
+val set_nonce:
     ctx: aes_ctx
   -> nonce: lbuffer uint8 12ul ->
   Stack unit
@@ -106,7 +106,7 @@ val aes128_set_nonce:
       u8_16_to_le (LSeq.update_sub
       (LSeq.create 16 (u8 0)) 0 12 (as_seq h0 nonce))))
 
-let aes128_set_nonce ctx nonce = aes_set_nonce ctx nonce
+let set_nonce ctx nonce = aes_set_nonce ctx nonce
 
 
 [@@ Comment "Process 4-blocks (128-bit for each) in AES-CTR32 mode.
@@ -115,7 +115,7 @@ let aes128_set_nonce ctx nonce = aes_set_nonce ctx nonce
   
   `counter` is the current value of counter state."]
 inline_for_extraction noextract
-val aes128_update4:
+val update4:
     out: lbuffer uint8 64ul
   -> inp: lbuffer uint8 64ul
   -> ctx: aes_ctx
@@ -128,15 +128,15 @@ val aes128_update4:
       (get_nonce_s MAES Spec.AES128 h0 ctx)
       counter (as_seq h0 inp)))
 
-let aes128_update4 out inp ctx ctr = aes_update4 out inp ctx ctr
+let update4 out inp ctx ctr = aes_update4 out inp ctx ctr
 
 [@@ Comment "Process number of bytes in AES-CTR32 mode.
 
   Given that `ctx` is initiated with AES-128 key and nonce, and
   
   `counter` is the initial value of counter state."]
 inline_for_extraction noextract
-val aes128_ctr:
+val ctr:
   len: size_t
   -> out: lbuffer uint8 len
   -> inp: lbuffer uint8 len
@@ -151,15 +151,15 @@ val aes128_ctr:
       (get_nonce_s MAES Spec.AES128 h0 ctx)
       counter (as_seq h0 inp)))
 
-let aes128_ctr len out inp ctx c = aes_ctr #MAES #Spec.AES128 len out inp ctx c
+let ctr len out inp ctx c = aes_ctr #MAES #Spec.AES128 len out inp ctx c
 
 
 [@@ Comment "Initiate AES-CTR32-128 context with key and nonce, and
 
   encrypt number of bytes in AES-CTR32 mode.
   
   `counter` is the initial value of counter state."]
-val aes128_ctr_encrypt:
+val ctr_encrypt:
     len: size_t
   -> out: lbuffer uint8 len
   -> inp: lbuffer uint8 len
@@ -173,7 +173,7 @@ val aes128_ctr_encrypt:
     as_seq h1 out == Spec.aes_ctr32_encrypt_bytes_LE Spec.AES128
     (as_seq h0 k) (as_seq h0 n) counter (as_seq h0 inp)))
 
-let aes128_ctr_encrypt len out inp k n c = aes_ctr_encrypt #MAES #Spec.AES128 len out inp k n c
+let ctr_encrypt len out inp k n c = aes_ctr_encrypt #MAES #Spec.AES128 len out inp k n c
 
 
 [@@ Comment "Initiate AES-CTR32-128 context with key and nonce, and
@@ -183,7 +183,7 @@ let aes128_ctr_encrypt len out inp k n c = aes_ctr_encrypt #MAES #Spec.AES128 le
   `counter` is the initial value of counter state.
   
   Decryption uses the forward version of AES cipher"]
-val aes128_ctr_decrypt:
+val ctr_decrypt:
     len: size_t
   -> out: lbuffer uint8 len
   -> inp: lbuffer uint8 len
@@ -196,5 +196,5 @@ val aes128_ctr_decrypt:
   (ensures (fun h0 _ h1 -> modifies (loc out) h0 h1 /\
     as_seq h1 out == Spec.aes_ctr32_decrypt_bytes_LE Spec.AES128
     (as_seq h0 k) (as_seq h0 n) counter (as_seq h0 inp)))
-let aes128_ctr_decrypt len out inp k n c = aes_ctr_decrypt #MAES #Spec.AES128 len out inp k n c
+let ctr_decrypt len out inp k n c = aes_ctr_decrypt #MAES #Spec.AES128 len out inp k n c
 
diff --git a/code/aes/Hacl.AES_256.CTR32.NI.fst b/code/aes/Hacl.AES_256.CTR32.NI.fst
@@ -80,7 +80,7 @@ let context_free s =
 
 
 [@@ Comment "Initiate AES-256 context buffer with key expansion and nonce"]
-val aes256_init:
+val init:
     ctx: aes_ctx
   -> key: skey 
   -> nonce: lbuffer uint8 12ul ->
@@ -93,13 +93,13 @@ val aes256_init:
     get_nonce_s MAES Spec.AES256 h1 ctx == state.block /\
     get_kex_s MAES Spec.AES256 h1 ctx == state.key_ex)))
 
-let aes256_init ctx key nonce = aes256_ni_init ctx key nonce
+let init ctx key nonce = aes256_ni_init ctx key nonce
 
 [@@ Comment "Encrypt a block (128-bit) with AES-256 cipher.
 
   Given that `ctx` is initiated with AES-256 key."]
 inline_for_extraction noextract
-val aes256_encrypt_block:
+val encrypt_block:
     ob: lbuffer uint8 16ul
   -> ctx: aes_ctx
   -> ib: lbuffer uint8 16ul ->
@@ -109,12 +109,12 @@ val aes256_encrypt_block:
     as_seq h1 ob == u8_16_to_le (Spec.aes_encrypt_block Spec.AES256
       (get_kex_s MAES Spec.AES256 h0 ctx) (u8_16_to_le (as_seq h0 ib)))))
 
-let aes256_encrypt_block ob ctx ib =
+let encrypt_block ob ctx ib =
     aes_encrypt_block #MAES #Spec.AES256 ob ctx ib
 
 
 [@@ Comment "Set nonce in AES-256 context buffer"]
-val aes256_set_nonce:
+val set_nonce:
     ctx: aes_ctx
   -> nonce: lbuffer uint8 12ul ->
   Stack unit
@@ -124,7 +124,7 @@ val aes256_set_nonce:
       u8_16_to_le (LSeq.update_sub
       (LSeq.create 16 (u8 0)) 0 12 (as_seq h0 nonce))))
 
-let aes256_set_nonce ctx nonce = aes_set_nonce ctx nonce
+let set_nonce ctx nonce = aes_set_nonce ctx nonce
 
 
 [@@ Comment "Process 4-blocks (128-bit for each) in AES-CTR32 mode.
@@ -133,7 +133,7 @@ let aes256_set_nonce ctx nonce = aes_set_nonce ctx nonce
   
   `counter` is the current value of counter state."]
 inline_for_extraction noextract
-val aes256_update4:
+val update4:
     out: lbuffer uint8 64ul
   -> inp: lbuffer uint8 64ul
   -> ctx: aes_ctx
@@ -146,15 +146,15 @@ val aes256_update4:
       (get_nonce_s MAES Spec.AES256 h0 ctx)
       counter (as_seq h0 inp)))
 
-let aes256_update4 out inp ctx ctr = aes_update4 out inp ctx ctr
+let update4 out inp ctx ctr = aes_update4 out inp ctx ctr
 
 
 [@@ Comment "Process number of bytes in AES-CTR32 mode.
 
   Given that `ctx` is initiated with AES-256 key and nonce, and
   
   `counter` is the initial value of counter state."]
-val aes256_ctr:
+val ctr:
   len: size_t
   -> out: lbuffer uint8 len
   -> inp: lbuffer uint8 len
@@ -169,15 +169,15 @@ val aes256_ctr:
       (get_nonce_s MAES Spec.AES256 h0 ctx)
       counter (as_seq h0 inp)))
 
-let aes256_ctr len out inp ctx c =  aes_ctr #MAES #Spec.AES256 len out inp ctx c
+let ctr len out inp ctx c =  aes_ctr #MAES #Spec.AES256 len out inp ctx c
 
 
 [@@ Comment "Initiate AES-CTR32-256 context with key and nonce, and
 
   encrypt number of bytes in AES-CTR32 mode.
   
   `counter` is the initial value of counter state."]
-val aes256_ctr_encrypt:
+val ctr_encrypt:
     len: size_t
   -> out: lbuffer uint8 len
   -> inp: lbuffer uint8 len
@@ -191,7 +191,7 @@ val aes256_ctr_encrypt:
     as_seq h1 out == Spec.aes_ctr32_encrypt_bytes_LE Spec.AES256
     (as_seq h0 k) (as_seq h0 n) counter (as_seq h0 inp)))
 
-let aes256_ctr_encrypt len out inp k n c = aes_ctr_encrypt #MAES #Spec.AES256 len out inp k n c
+let ctr_encrypt len out inp k n c = aes_ctr_encrypt #MAES #Spec.AES256 len out inp k n c
 
 
 [@@ Comment "Initiate AES-CTR32-256 context with key and nonce, and
@@ -201,7 +201,7 @@ let aes256_ctr_encrypt len out inp k n c = aes_ctr_encrypt #MAES #Spec.AES256 le
   `counter` is the initial value of counter state.
   
   Decryption uses the forward version of AES cipher"]
-val aes256_ctr_decrypt:
+val ctr_decrypt:
     len: size_t
   -> out: lbuffer uint8 len
   -> inp: lbuffer uint8 len
@@ -214,4 +214,4 @@ val aes256_ctr_decrypt:
   (ensures (fun h0 _ h1 -> modifies (loc out) h0 h1 /\
     as_seq h1 out == Spec.aes_ctr32_decrypt_bytes_LE Spec.AES256
     (as_seq h0 k) (as_seq h0 n) counter (as_seq h0 inp)))
-let aes256_ctr_decrypt len out inp k n c = aes_ctr_decrypt #MAES #Spec.AES256 len out inp k n c
+let ctr_decrypt len out inp k n c = aes_ctr_decrypt #MAES #Spec.AES256 len out inp k n c
diff --git a/dist/gcc-compatible/Hacl_AES_128_CTR32_NI.c b/dist/gcc-compatible/Hacl_AES_128_CTR32_NI.c
@@ -50,11 +50,7 @@ void Hacl_AES_128_CTR32_NI_context_free(Lib_IntVector_Intrinsics_vec128 *s)
 Initiate AES-128 context buffer with key expansion and nonce
 */
 void
-Hacl_AES_128_CTR32_NI_aes128_init(
-  Lib_IntVector_Intrinsics_vec128 *ctx,
-  uint8_t *key,
-  uint8_t *nonce
-)
+Hacl_AES_128_CTR32_NI_init(Lib_IntVector_Intrinsics_vec128 *ctx, uint8_t *key, uint8_t *nonce)
 {
   Lib_IntVector_Intrinsics_vec128 *kex = ctx + 1U;
   Lib_IntVector_Intrinsics_vec128 *n = ctx;
@@ -268,8 +264,7 @@ Hacl_AES_128_CTR32_NI_aes128_init(
 /**
 Set nonce in AES-128 context buffer
 */
-void
-Hacl_AES_128_CTR32_NI_aes128_set_nonce(Lib_IntVector_Intrinsics_vec128 *ctx, uint8_t *nonce)
+void Hacl_AES_128_CTR32_NI_set_nonce(Lib_IntVector_Intrinsics_vec128 *ctx, uint8_t *nonce)
 {
   Lib_IntVector_Intrinsics_vec128 *n = ctx;
   uint8_t nb[16U] = { 0U };
@@ -285,7 +280,7 @@ Initiate AES-CTR32-128 context with key and nonce, and
   `counter` is the initial value of counter state.
 */
 void
-Hacl_AES_128_CTR32_NI_aes128_ctr_encrypt(
+Hacl_AES_128_CTR32_NI_ctr_encrypt(
   uint32_t len,
   uint8_t *out,
   uint8_t *inp,
@@ -619,7 +614,7 @@ Initiate AES-CTR32-128 context with key and nonce, and
   Decryption uses the forward version of AES cipher
 */
 void
-Hacl_AES_128_CTR32_NI_aes128_ctr_decrypt(
+Hacl_AES_128_CTR32_NI_ctr_decrypt(
   uint32_t len,
   uint8_t *out,
   uint8_t *inp,

diff --git a/dist/gcc-compatible/Hacl_AES_128_CTR32_NI.h b/dist/gcc-compatible/Hacl_AES_128_CTR32_NI.h
@@ -55,17 +55,12 @@ void Hacl_AES_128_CTR32_NI_context_free(Lib_IntVector_Intrinsics_vec128 *s);
 Initiate AES-128 context buffer with key expansion and nonce
 */
 void
-Hacl_AES_128_CTR32_NI_aes128_init(
-  Lib_IntVector_Intrinsics_vec128 *ctx,
-  uint8_t *key,
-  uint8_t *nonce
-);
+Hacl_AES_128_CTR32_NI_init(Lib_IntVector_Intrinsics_vec128 *ctx, uint8_t *key, uint8_t *nonce);
 
 /**
 Set nonce in AES-128 context buffer
 */
-void
-Hacl_AES_128_CTR32_NI_aes128_set_nonce(Lib_IntVector_Intrinsics_vec128 *ctx, uint8_t *nonce);
+void Hacl_AES_128_CTR32_NI_set_nonce(Lib_IntVector_Intrinsics_vec128 *ctx, uint8_t *nonce);
 
 /**
 Initiate AES-CTR32-128 context with key and nonce, and
@@ -75,7 +70,7 @@ Initiate AES-CTR32-128 context with key and nonce, and
   `counter` is the initial value of counter state.
 */
 void
-Hacl_AES_128_CTR32_NI_aes128_ctr_encrypt(
+Hacl_AES_128_CTR32_NI_ctr_encrypt(
   uint32_t len,
   uint8_t *out,
   uint8_t *inp,
@@ -94,7 +89,7 @@ Initiate AES-CTR32-128 context with key and nonce, and
   Decryption uses the forward version of AES cipher
 */
 void
-Hacl_AES_128_CTR32_NI_aes128_ctr_decrypt(
+Hacl_AES_128_CTR32_NI_ctr_decrypt(
   uint32_t len,
   uint8_t *out,
   uint8_t *inp,

diff --git a/dist/gcc-compatible/Hacl_AES_256_CTR32_NI.c b/dist/gcc-compatible/Hacl_AES_256_CTR32_NI.c
@@ -50,11 +50,7 @@ void Hacl_AES_256_CTR32_NI_context_free(Lib_IntVector_Intrinsics_vec128 *s)
 Initiate AES-256 context buffer with key expansion and nonce
 */
 void
-Hacl_AES_256_CTR32_NI_aes256_init(
-  Lib_IntVector_Intrinsics_vec128 *ctx,
-  uint8_t *key,
-  uint8_t *nonce
-)
+Hacl_AES_256_CTR32_NI_init(Lib_IntVector_Intrinsics_vec128 *ctx, uint8_t *key, uint8_t *nonce)
 {
   Lib_IntVector_Intrinsics_vec128 *kex = ctx + 1U;
   Lib_IntVector_Intrinsics_vec128 *n = ctx;
@@ -326,8 +322,7 @@ Hacl_AES_256_CTR32_NI_aes256_init(
 /**
 Set nonce in AES-256 context buffer
 */
-void
-Hacl_AES_256_CTR32_NI_aes256_set_nonce(Lib_IntVector_Intrinsics_vec128 *ctx, uint8_t *nonce)
+void Hacl_AES_256_CTR32_NI_set_nonce(Lib_IntVector_Intrinsics_vec128 *ctx, uint8_t *nonce)
 {
   Lib_IntVector_Intrinsics_vec128 *n = ctx;
   uint8_t nb[16U] = { 0U };
@@ -343,7 +338,7 @@ Process number of bytes in AES-CTR32 mode.
   `counter` is the initial value of counter state.
 */
 void
-Hacl_AES_256_CTR32_NI_aes256_ctr(
+Hacl_AES_256_CTR32_NI_ctr(
   uint32_t len,
   uint8_t *out,
   uint8_t *inp,
@@ -467,7 +462,7 @@ Initiate AES-CTR32-256 context with key and nonce, and
   `counter` is the initial value of counter state.
 */
 void
-Hacl_AES_256_CTR32_NI_aes256_ctr_encrypt(
+Hacl_AES_256_CTR32_NI_ctr_encrypt(
   uint32_t len,
   uint8_t *out,
   uint8_t *inp,
@@ -859,7 +854,7 @@ Initiate AES-CTR32-256 context with key and nonce, and
   Decryption uses the forward version of AES cipher
 */
 void
-Hacl_AES_256_CTR32_NI_aes256_ctr_decrypt(
+Hacl_AES_256_CTR32_NI_ctr_decrypt(
   uint32_t len,
   uint8_t *out,
   uint8_t *inp,

diff --git a/dist/gcc-compatible/Hacl_AES_256_CTR32_NI.h b/dist/gcc-compatible/Hacl_AES_256_CTR32_NI.h
@@ -55,17 +55,12 @@ void Hacl_AES_256_CTR32_NI_context_free(Lib_IntVector_Intrinsics_vec128 *s);
 Initiate AES-256 context buffer with key expansion and nonce
 */
 void
-Hacl_AES_256_CTR32_NI_aes256_init(
-  Lib_IntVector_Intrinsics_vec128 *ctx,
-  uint8_t *key,
-  uint8_t *nonce
-);
+Hacl_AES_256_CTR32_NI_init(Lib_IntVector_Intrinsics_vec128 *ctx, uint8_t *key, uint8_t *nonce);
 
 /**
 Set nonce in AES-256 context buffer
 */
-void
-Hacl_AES_256_CTR32_NI_aes256_set_nonce(Lib_IntVector_Intrinsics_vec128 *ctx, uint8_t *nonce);
+void Hacl_AES_256_CTR32_NI_set_nonce(Lib_IntVector_Intrinsics_vec128 *ctx, uint8_t *nonce);
 
 /**
 Process number of bytes in AES-CTR32 mode.
@@ -75,7 +70,7 @@ Process number of bytes in AES-CTR32 mode.
   `counter` is the initial value of counter state.
 */
 void
-Hacl_AES_256_CTR32_NI_aes256_ctr(
+Hacl_AES_256_CTR32_NI_ctr(
   uint32_t len,
   uint8_t *out,
   uint8_t *inp,
@@ -91,7 +86,7 @@ Initiate AES-CTR32-256 context with key and nonce, and
   `counter` is the initial value of counter state.
 */
 void
-Hacl_AES_256_CTR32_NI_aes256_ctr_encrypt(
+Hacl_AES_256_CTR32_NI_ctr_encrypt(
   uint32_t len,
   uint8_t *out,
   uint8_t *inp,
@@ -110,7 +105,7 @@ Initiate AES-CTR32-256 context with key and nonce, and
   Decryption uses the forward version of AES cipher
 */
 void
-Hacl_AES_256_CTR32_NI_aes256_ctr_decrypt(
+Hacl_AES_256_CTR32_NI_ctr_decrypt(
   uint32_t len,
   uint8_t *out,
   uint8_t *inp,