Document GHASH API

code/gf128/Hacl.Gf128.NI.fst

@@ -25,27 +25,44 @@ let gcm_ctx_elem_zero = vec_zero U128 1
 inline_for_extraction noextract
 let gcm_ctx = lbuffer gcm_ctx_elem gcm_ctx_len
 
+[@@ CPrologue
+"/*******************************************************************************
 
-[@CInline]
+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 (carry-less mul) h^3 -> CONTEXT.[1] (16-byte)
+  h (carry-less mul) h^2 -> CONTEXT.[2] (16-byte)
+  h (carry-less mul) h   -> CONTEXT.[3] (16-byte)
+  h                      -> CONTEXT.[4] (16-byte)"]
 let gcm_init : gf128_init_st Vec.NI =
   gf128_init #Vec.NI
 
 
-[@CInline]
+[@@ 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
 
 
-[@CInline]
-let gcm_update_padded: gf128_update_st Vec.NI =
-  gcm_update_blocks
-
-
-[@CInline]
+[@@ Comment "Copy hash state from GHASH context to 16-byte output buffer"]
 let gcm_emit: gf128_emit_st Vec.NI =
   gf128_emit #Vec.NI
 
 
-[@CInline]
+[@@ 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

code/gf128/Hacl.Impl.Gf128.Generic.fsti

@@ -51,7 +51,6 @@ let gf128_update_st (s:field_spec) =
   (ensures  fun h0 _ h1 ->
     modifies1 ctx h0 h1 /\ state_inv_t h1 ctx /\
     as_get_acc h1 ctx == S.gf128_update (as_seq h0 text) (as_get_acc h0 ctx) (as_get_r h0 ctx))
-//as_get_acc h1 ctx == Vec.gf128_update_vec s (as_seq h0 text) (as_get_acc h0 ctx) (as_get_r h0 ctx)
 
 
 inline_for_extraction noextract

code/gf128/Hacl.Spec.GF128.PolyLemmas_helpers.fst

@@ -122,11 +122,11 @@ let lemma_mul_h_2_zero a h =
       lemma_mul_monomials 60 64;
       lemma_add_zero (monomial 124);
       lemma_div_mod_unique ((monomial 124) +. zero) (monomial 64) (monomial 60) zero;
-      // --> monomial 126 %. monomial 64 == zero
+      // --> monomial 124 %. monomial 64 == zero
       lemma_mul_monomials 50 64;
       lemma_add_zero (monomial 114);
       lemma_div_mod_unique ((monomial 114) +. zero) (monomial 64) (monomial 50) zero
-      // --> monomial 126 %. monomial 64 == zero
+      // --> monomial 114 %. monomial 64 == zero
     }
     (a *. (zero +. zero +. zero)) %. monomial 64;
     == {lemma_add_zero zero}
@@ -417,9 +417,6 @@ let lemma_reduce_rev_helper a0 a1 h n =
   lemma_reduce_rev a0 zero a1 h n;
   ()
 
-let lemma_gf128_mul_accum z0 z1 a b c d =
-  admit()
-
 val lemma_add_helper1 (ac bc_m ad_m z_ac z_bc_m z_ad_m:poly) :
   Lemma (ensures (
     (z_ac +. ac) +.

code/gf128/Hacl.Spec.GF128.PolyLemmas_helpers.fsti

@@ -105,21 +105,6 @@ val lemma_reduce_rev_helper (a0 a1 h:poly) (n:pos) : Lemma
     reverse (x %. g) (nn - 1) == swap y_10c 64 +. mask y_10c 64 *. c +. a1
   ))
 
-val lemma_gf128_mul_accum (z0 z1 a b c d:poly) (n:nat) : Lemma
-  (ensures (
-    let z = shift z1 (n + n) +. z0 in
-    let m = monomial n in
-    let ab = a *. m +. b in
-    let cd = c *. m +. d in
-    let ac = a *. c in
-    let ad = a *. d in
-    let bc = b *. c in
-    let bd = b *. d in
-    z +. ab *. cd ==
-      shift (z1 +. ac +. bc /. m +. ad /. m) (n + n) +.
-      (z0 +. (bc %. m) *. m +. (ad %. m) *. m +. bd)
-  ))
-
 val lemma_gf128_mul_4 (a0 b0 c0 d0 a1 b1 c1 d1 a2 b2 c2 d2 a3 b3 c3 d3:poly) :
   Lemma (ensures (
     let m = monomial 64 in

specs/Spec.GF128.fst

@@ -18,9 +18,15 @@ let elem = felem gf128
 let load_elem (b:lbytes 16) : elem = load_felem_be #gf128 b
 let store_elem (e:elem) : lbytes 16 = store_felem_be #gf128 e
 
+/// Little-endian definitions for GF128 Field
+
+//Constant represents the irreducable polynomial for reduction over GF(2^128)
 let irred_le = mk_int #U128 #SEC 0x87
+
 let gf128_le = gf U128 irred_le
 let elem_le = felem gf128_le
+//Multiplication over GF(2^128), reverse the coefficients of operands to meet
+//little-endian requirement of GCM spec
 let fmul_le (a b:elem_le) = reverse (fmul (reverse a) (reverse b))
 
 (* GCM types and specs *)