Import NI modules of GHASH from pnmadelaine_aes branch and adds specific proofs

Hacl.fst.config.json

@@ -19,6 +19,7 @@
     "specs/drbg",
     "specs/frodo",
     "specs/tests/p256",
+    "code/gf128",
     "code/hash",
     "code/hmac",
     "code/hkdf",

Makefile

@@ -700,7 +700,9 @@ INTRINSIC_FLAGS = \
   -add-include 'Hacl_Hash_Blake2b_Simd256:"libintvector.h"' \
   -add-include 'Hacl_MAC_Poly1305_Simd256:"libintvector.h"' \
   \
-  -add-include 'Hacl_Hash_SHA3_Simd256:"libintvector.h"'
+  -add-include 'Hacl_Hash_SHA3_Simd256:"libintvector.h"' \
+  \
+  -add-include 'Hacl_Gf128_NI:"libintvector.h"'
 
 # Disabled for distributions that don't include code based on intrinsics.
 INTRINSIC_INT_FLAGS = \
@@ -763,7 +765,8 @@ BUNDLE_FLAGS	=\
   $(INTTYPES_128_BUNDLE) \
   $(RSAPSS_BUNDLE) \
   $(FFDHE_BUNDLE) \
-  $(LEGACY_BUNDLE)
+  $(LEGACY_BUNDLE) \
+  $(GF128_BUNDLE)
 
 DEFAULT_FLAGS = \
   $(HAND_WRITTEN_LIB_FLAGS) \
@@ -775,6 +778,8 @@ DEFAULT_FLAGS = \
   $(REQUIRED_FLAGS) \
   $(TARGET_H_INCLUDE)
 
+IGNORE_GF128_BUNDLE = -bundle Hacl.Impl.Gf128.*,Hacl.Gf128.*
+
 # WASM distribution
 # -----------------
 #
@@ -833,6 +838,9 @@ dist/wasm/Makefile.basic: POLY_BUNDLE = \
   -bundle 'Hacl.Poly1305_128,Hacl.Poly1305_256,Hacl.Impl.Poly1305.*' \
   -bundle 'Hacl.Streaming.Poly1305_128,Hacl.Streaming.Poly1305_256'
 
+# Disabling GF128
+dist/wasm/Makefile.basic: GF128_BUNDLE = $(IGNORE_GF128_BUNDLE)
+
 dist/wasm/Makefile.basic: CTR_BUNDLE =
 dist/wasm/Makefile.basic: RSAPSS_BUNDLE = -bundle Hacl.RSAPSS,Hacl.Impl.RSAPSS.*,Hacl.Impl.RSAPSS
 dist/wasm/Makefile.basic: FFDHE_BUNDLE = -bundle Hacl.FFDHE,Hacl.Impl.FFDHE.*,Hacl.Impl.FFDHE

Makefile.common

@@ -226,6 +226,7 @@ BIGNUM_BUNDLE= \
   -bundle Hacl.Bignum.Base,Hacl.Bignum.Addition,Hacl.Bignum.Convert,Hacl.Bignum.Lib,Hacl.Bignum.Multiplication[rename=Hacl_Bignum_Base] \
   -static-header Hacl.Bignum.Base,Hacl.Bignum.Addition,Hacl.Bignum.Convert,Hacl.Bignum.Lib,Hacl.Bignum.Multiplication \
   -bundle Hacl.Bignum,Hacl.Bignum.*[rename=Hacl_Bignum]
+GF128_BUNDLE=-bundle Hacl.Gf128.NI=Hacl.Impl.Gf128.FieldNI
 
 # 3. OCaml
 

Makefile.include

@@ -14,7 +14,8 @@ VALE_BUNDLES=\
 LIB_DIR		= $(HACL_HOME)/lib
 SPECS_DIR 	= $(HACL_HOME)/specs $(addprefix $(HACL_HOME)/specs/,lemmas tests drbg frodo tests/p256)
 CODE_DIRS	= $(addprefix $(HACL_HOME)/code/,hash hmac hkdf drbg hpke sha3 sha2-mb ecdsap256 poly1305 streaming \
-  blake2 chacha20 chacha20poly1305 curve25519 tests ed25519 salsa20 nacl-box meta frodo fallback bignum rsapss ffdhe k256)
+  blake2 chacha20 chacha20poly1305 curve25519 tests ed25519 salsa20 nacl-box meta frodo fallback bignum rsapss ffdhe k256 \
+  gf128)
 EVERCRYPT_DIRS  = $(addprefix $(HACL_HOME)/providers/,evercrypt evercrypt/fst test test/vectors)
 # Vale dirs also include directories that only contain .vaf files
 # (for a in $(find vale -iname '*.fst' -or -iname '*.fsti' -or -iname '*.vaf'); do dirname $a; done) | sort | uniq

code/gf128/AUTHORS.md

@@ -0,0 +1,3 @@
+Proofs are written by Mamone Tarsha Kurdi (Cryspen).
+
+This code was primarily written by Karthikeyan Bhargavan (INRIA).

code/gf128/Hacl.Gf128.NI.fst

@@ -0,0 +1,68 @@
+module Hacl.Gf128.NI
+
+open FStar.HyperStack
+open FStar.HyperStack.All
+
+open Lib.IntTypes
+open Lib.Buffer
+open Lib.IntVector
+
+open Hacl.Impl.Gf128.Fields
+open Hacl.Impl.Gf128.Generic
+
+module ST = FStar.HyperStack.ST
+module Vec = Hacl.Spec.GF128.Vec
+
+#reset-options "--z3rlimit 50 --max_fuel 0 --max_ifuel 1"
+
+inline_for_extraction noextract
+let gcm_ctx_elem = vec_t U128 1
+inline_for_extraction noextract
+let gcm_ctx_len = 5ul
+
+inline_for_extraction noextract
+let gcm_ctx_elem_zero = vec_zero U128 1
+inline_for_extraction noextract
+let gcm_ctx = lbuffer gcm_ctx_elem gcm_ctx_len
+
+[@@ CPrologue
+"/*******************************************************************************
+
+A verified GHASH library.
+
+This is a 128-bit optimized version of GHASH algorithm over GF(2^128) for data
+authenticity that utilizes hardware-accelerated carry-less/polynomial multiplication.
+
+*******************************************************************************/
+
+/************************/
+/* GHASH API */
+/************************/\n";
+Comment
+"Initiate GHASH context with the following layout
+
+  Authentication Tag     -> CONTEXT.[0] (16-byte)
+  h * h^3                -> CONTEXT.[1] (16-byte)
+  h * h^2                -> CONTEXT.[2] (16-byte)
+  h * h                  -> CONTEXT.[3] (16-byte)
+  h (hash key)           -> CONTEXT.[4] (16-byte)"]
+let gcm_init : gf128_init_st Vec.NI =
+  gf128_init #Vec.NI
+
+
+[@@ Comment "Expand the input message to have a length of multiple of 16 and pad 
+  the extra bytes with zeros. The authentication tag is computed by feeding the
+  previous state and applying GHASH algorithm on expanded message"]
+let gcm_update_blocks: gf128_update_st Vec.NI =
+  gf128_update #Vec.NI
+
+
+[@@ Comment "Copy hash state from GHASH context to 16-byte output buffer"]
+let gcm_emit: gf128_emit_st Vec.NI =
+  gf128_emit #Vec.NI
+
+
+[@@ Comment "Initiate GHASH context, apply GHASH algorithm on input message,
+  and copy authentication tag to output buffer"]
+let ghash: ghash_st Vec.NI =
+  ghash #Vec.NI