val lemma_ghash_poly_unroll (h0 prev: poly) (data: (int -> poly128)) (k: int) (m: nat)
    : Lemma (requires degree h0 < 128 /\ degree prev < 128)
      (ensures ghash_poly_unroll h0 prev data k m 0 == ghash_poly h0 prev data k (k + m + 1))
let rec lemma_ghash_poly_unroll (h0:poly) (prev:poly) (data:int -> poly128) (k:int) (m:nat) : Lemma
  (requires degree h0 < 128 /\ degree prev < 128)
  (ensures ghash_poly_unroll h0 prev data k m 0 == ghash_poly h0 prev data k (k + m + 1))
  =
  let d = data (k + m) in
  let p1 = g_power h0 1 in
  let ghash0 = ghash_poly h0 prev data k (k + m) in
  if m = 0 then
    calc (==) {
      ghash_poly_unroll h0 prev data k m 0;
      == {}
      (prev +. d) *~ p1;
      == {}
      (ghash0 +. d) *~ h0;
      == {}
      ghash_poly h0 prev data k (k + m + 1);
    }
  else
    let unroll0 = ghash_poly_unroll h0 prev data k (m - 1) 0 in
    let unroll1 = ghash_poly_unroll h0 prev data k (m - 1) 1 in
    calc (==) {
      ghash_poly_unroll h0 prev data k m 0;
      == {}
      unroll1 +. d *~ p1;
      == {
        calc (==) {
          unroll1;
          == {lemma_ghash_poly_unroll_n h0 prev data k (m - 1) 0}
          unroll0 *~ h0;
          == {lemma_ghash_poly_unroll h0 prev data k (m - 1)}
          ghash0 *~ h0;
        }
      }
      ghash0 *~ h0 +. d *~ h0;
      == {lemma_gf128_mul_rev_distribute_left ghash0 d h0}
      (ghash0 +. d) *~ h0;
      == {}
      ghash_poly h0 prev data k (k + m + 1);
    }
val lemma_ghash_poly_unroll (h0 prev: poly) (data: (int -> poly128)) (k: int) (m: nat)
    : Lemma (requires degree h0 < 128 /\ degree prev < 128)
      (ensures ghash_poly_unroll h0 prev data k m 0 == ghash_poly h0 prev data k (k + m + 1))
let rec lemma_ghash_poly_unroll (h0 prev: poly) (data: (int -> poly128)) (k: int) (m: nat)
    : Lemma (requires degree h0 < 128 /\ degree prev < 128)
      (ensures ghash_poly_unroll h0 prev data k m 0 == ghash_poly h0 prev data k (k + m + 1)) =
let d = data (k + m) in
let p1 = g_power h0 1 in
let ghash0 = ghash_poly h0 prev data k (k + m) in
if m = 0
then
  calc ( == ) {
    ghash_poly_unroll h0 prev data k m 0;
    ( == ) { () }
    (prev +. d) *~ p1;
    ( == ) { () }
    (ghash0 +. d) *~ h0;
    ( == ) { () }
    ghash_poly h0 prev data k (k + m + 1);
  }
else
  let unroll0 = ghash_poly_unroll h0 prev data k (m - 1) 0 in
  let unroll1 = ghash_poly_unroll h0 prev data k (m - 1) 1 in
  calc ( == ) {
    ghash_poly_unroll h0 prev data k m 0;
    ( == ) { () }
    unroll1 +. d *~ p1;
    ( == ) { calc ( == ) {
      unroll1;
      ( == ) { lemma_ghash_poly_unroll_n h0 prev data k (m - 1) 0 }
      unroll0 *~ h0;
      ( == ) { lemma_ghash_poly_unroll h0 prev data k (m - 1) }
      ghash0 *~ h0;
    } }
    ghash0 *~ h0 +. d *~ h0;
    ( == ) { lemma_gf128_mul_rev_distribute_left ghash0 d h0 }
    (ghash0 +. d) *~ h0;
    ( == ) { () }
    ghash_poly h0 prev data k (k + m + 1);
  }
Vale.AES.GHash.fst.checked
Vale.Math.Poly2.Words.fsti.checked Vale.Math.Poly2.Lemmas.fsti.checked Vale.Math.Bits.fsti.checked Vale.Def.Words.Four_s.fsti.checked Vale.Arch.TypesNative.fsti.checked Vale.AES.OptPublic.fst.checked prims.fst.checked FStar.UInt.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked FStar.BV.fsti.checked
Vale.AES.GHash.fst
Vale.Math.Poly2_s.poly Prims.int Vale.AES.GHash.poly128 Prims.nat Prims.op_Equality FStar.Calc.calc_finish Prims.eq2 Vale.AES.GHash.ghash_poly_unroll Vale.AES.GHash.ghash_poly Prims.op_Addition Prims.Cons FStar.Preorder.relation Prims.Nil Prims.unit FStar.Calc.calc_step Vale.AES.GF128.op_Star_Tilde Vale.Math.Poly2.op_Plus_Dot FStar.Calc.calc_init FStar.Calc.calc_pack Prims.squash Prims.bool Vale.AES.GHash.lemma_ghash_poly_unroll_n Prims.op_Subtraction Vale.AES.GHash.lemma_ghash_poly_unroll Vale.AES.GF128.lemma_gf128_mul_rev_distribute_left Vale.AES.GHash.g_power Prims.l_and Prims.b2t Prims.op_LessThan Vale.Math.Poly2_s.degree FStar.Pervasives.pattern
module Vale.AES.GHash
open FStar.Mul
open Vale.Math.Poly2.Lemmas
open Vale.Math.Poly2.Words

friend Vale.AES.OptPublic

#reset-options

let shift_gf128_key_1 (h:poly) : poly =
  shift_key_1 128 gf128_modulus_low_terms h

let rec g_power (a:poly) (n:nat) : poly =
  if n = 0 then zero else // arbitrary value for n = 0
  if n = 1 then a else
  a *~ g_power a (n - 1)

let lemma_g_power_1 a = ()
let lemma_g_power_n a n = ()

let gf128_power h n = shift_gf128_key_1 (g_power h n)
let lemma_gf128_power h n = ()

let rec ghash_poly_unroll (h:poly) (prev:poly) (data:int -> poly128) (k:int) (m n:nat) : poly =
  let d = data (k + m) in
  let p = g_power h (n + 1) in
  if m = 0 then (prev +. d) *~ p else
  ghash_poly_unroll h prev data k (m - 1) (n + 1) +. d *~ p

let lemma_hkeys_reqs_pub_priv (hkeys:seq quad32) (h_BE:quad32) : Lemma
  (hkeys_reqs_pub hkeys h_BE <==> hkeys_reqs_priv hkeys h_BE)
  =
  ()

let rec lemma_ghash_unroll_back_forward_rec (h:poly) (prev:poly) (data:int -> poly128) (k:int) (n m:nat) : Lemma
  (requires m < n)
  (ensures ghash_unroll h prev data k n 0 ==
    ghash_unroll h prev data k (n - 1 - m) (m + 1) +. ghash_unroll_back h prev data k (n + 1) m)
  =
  lemma_add_all ();
  if m > 0 then lemma_ghash_unroll_back_forward_rec h prev data k n (m - 1)

let lemma_ghash_unroll_back_forward (h:poly) (prev:poly) (data:int -> poly128) (k:int) (n:nat) : Lemma
  (ghash_unroll h prev data k n 0 == ghash_unroll_back h prev data k (n + 1) n)
  =
  lemma_add_all ();
  if n > 0 then lemma_ghash_unroll_back_forward_rec h prev data k n (n - 1)

let lemma_gf128_mul_rev_mod_rev (a h:poly) : Lemma
  (requires degree a < 128 /\ degree h < 128)
  (ensures gf128_mul_rev a h == mod_rev 128 (a *. shift_gf128_key_1 h) gf128_modulus)
  =
  let h1 = shift_gf128_key_1 h in
  let rev x = reverse x 127 in
  let g = gf128_modulus in
  lemma_gf128_degree ();
  calc (==) {
    // gf128_mul_rev a h
    rev ((rev a *. rev h) %. g);
    == {lemma_mod_mul_mod_right (rev a) (rev h) g}
    rev ((rev a *. (rev h %. g)) %. g);
    == {lemma_shift_key_1 128 gf128_modulus_low_terms h}
    rev ((rev a *. (shift (rev h1) 1 %. g)) %. g);
    == {lemma_mod_mul_mod_right (rev a) (shift (rev h1) 1) g}
    rev ((rev a *. (shift (rev h1) 1)) %. g);
    == {lemma_shift_is_mul (rev h1) 1}
    rev ((rev a *. (rev h1 *. monomial 1)) %. g);
    == {lemma_mul_all ()}
    rev (((rev a *. rev h1) *. monomial 1) %. g);
    == {lemma_shift_is_mul (rev a *. rev h1) 1}
    rev (shift (rev a *. rev h1) 1 %. g);
    == {lemma_mul_reverse_shift_1 a h1 127}
    rev (reverse (a *. h1) 255 %. g);
  }

let rec lemma_ghash_poly_degree h init data j k =
  if k > j then lemma_ghash_poly_degree h init data j (k - 1)

let rec lemma_ghash_poly_unroll_n (h:poly) (prev:poly) (data:int -> poly128) (k:int) (m n:nat) : Lemma
  (ghash_poly_unroll h prev data k m (n + 1) == ghash_poly_unroll h prev data k m n *~ h)
  =
  let d = data (k + m) in
  let p0 = g_power h (n + 1) in
  let p1 = g_power h (n + 2) in
  if m = 0 then
    calc (==) {
      ghash_poly_unroll h prev data k m (n + 1);
      == {}
      (prev +. d) *~ p1;
      == {}
      (prev +. d) *~ (h *~ p0);
      == {lemma_gf128_mul_rev_commute p0 h}
      (prev +. d) *~ (p0 *~ h);
      == {lemma_gf128_mul_rev_associate (prev +. d) p0 h}
      ((prev +. d) *~ p0) *~ h;
      == {}
      ghash_poly_unroll h prev data k m n *~ h;
    }
  else
    let ghash0 = ghash_poly_unroll h prev data k (m - 1) (n + 1) in
    let ghash1 = ghash_poly_unroll h prev data k (m - 1) (n + 2) in
    calc (==) {
      ghash_poly_unroll h prev data k m (n + 1);
      == {}
      ghash1 +. d *~ p1;
      == {lemma_ghash_poly_unroll_n h prev data k (m - 1) (n + 1)}
      ghash0 *~ h +. d *~ p1;
      == {}
      ghash0 *~ h +. d *~ (h *~ p0);
      == {lemma_gf128_mul_rev_commute p0 h}
      ghash0 *~ h +. d *~ (p0 *~ h);
      == {lemma_gf128_mul_rev_associate d p0 h}
      ghash0 *~ h +. (d *~ p0) *~ h;
      == {lemma_gf128_mul_rev_distribute_left ghash0 (d *~ p0) h}
      (ghash0 +. d *~ p0) *~ h;
      == {}
      ghash_poly_unroll h prev data k m n *~ h;
    }

let rec lemma_ghash_poly_unroll (h0:poly) (prev:poly) (data:int -> poly128) (k:int) (m:nat) : Lemma
  (requires degree h0 < 128 /\ degree prev < 128)
val lemma_ghash_poly_unroll (h0 prev: poly) (data: (int -> poly128)) (k: int) (m: nat)
    : Lemma (requires degree h0 < 128 /\ degree prev < 128)
      (ensures ghash_poly_unroll h0 prev data k m 0 == ghash_poly h0 prev data k (k + m + 1))

    h0: Vale.Math.Poly2_s.poly ->
    prev: Vale.Math.Poly2_s.poly ->
    data: (_: Prims.int -> Vale.AES.GHash.poly128) ->
    k: Prims.int ->
    m: Prims.nat
  -> FStar.Pervasives.Lemma
      (requires Vale.Math.Poly2_s.degree h0 < 128 /\ Vale.Math.Poly2_s.degree prev < 128)
      (ensures
        Vale.AES.GHash.ghash_poly_unroll h0 prev data k m 0 ==
        Vale.AES.GHash.ghash_poly h0 prev data k (k + m + 1))