Upload GHASH modules

Hacl.fst.config.json

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

Makefile

@@ -698,7 +698,9 @@ INTRINSIC_FLAGS = \
   -add-include 'Hacl_SHA2_Vec256.c:"libintvector.h"' \
   \
   -add-include 'Hacl_Hash_Blake2b_Simd256:"libintvector.h"' \
-  -add-include 'Hacl_MAC_Poly1305_Simd256:"libintvector.h"'
+  -add-include 'Hacl_MAC_Poly1305_Simd256:"libintvector.h"' \
+  \
+  -add-include 'Hacl_Gf128_NI:"libintvector.h"'
 
 # Disabled for distributions that don't include code based on intrinsics.
 INTRINSIC_INT_FLAGS = \
@@ -760,7 +762,8 @@ BUNDLE_FLAGS	=\
   $(INTTYPES_128_BUNDLE) \
   $(RSAPSS_BUNDLE) \
   $(FFDHE_BUNDLE) \
-  $(LEGACY_BUNDLE)
+  $(LEGACY_BUNDLE) \
+  $(GF128_BUNDLE)
 
 DEFAULT_FLAGS = \
   $(HAND_WRITTEN_LIB_FLAGS) \
@@ -772,6 +775,8 @@ DEFAULT_FLAGS = \
   $(REQUIRED_FLAGS) \
   $(TARGET_H_INCLUDE)
 
+IGNORE_GF128_BUNDLE = -bundle Hacl.Impl.Gf128.*,Hacl.Gf128.*
+
 # WASM distribution
 # -----------------
 #
@@ -830,6 +835,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

@@ -225,6 +225,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 @@
+This code was primarily written by Karthikeyan Bhargavan (INRIA).

code/gf128/Hacl.Gf128.NI.fst

@@ -0,0 +1,51 @@
+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
+
+
+[@CInline]
+let gcm_init : gf128_init_st Vec.NI =
+  gf128_init #Vec.NI
+
+
+[@CInline]
+let gcm_update_blocks: gf128_update_st Vec.NI =
+  gf128_update #Vec.NI
+
+
+[@CInline]
+let gcm_update_padded: gf128_update_st Vec.NI =
+  gcm_update_blocks
+
+
+[@CInline]
+let gcm_emit: gf128_emit_st Vec.NI =
+  gf128_emit #Vec.NI
+
+
+[@CInline]
+let ghash: ghash_st Vec.NI =
+  ghash #Vec.NI