val lemma_ghash_unroll_back_forward_rec (h 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)
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)
val lemma_ghash_unroll_back_forward_rec (h 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)
let rec lemma_ghash_unroll_back_forward_rec
      (h 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)
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_GreaterThan Vale.AES.GHash.lemma_ghash_unroll_back_forward_rec Prims.op_Subtraction Prims.bool Prims.unit Vale.Math.Poly2.Lemmas.lemma_add_all Prims.b2t Prims.op_LessThan Prims.squash Prims.eq2 Vale.AES.GHash.ghash_unroll Vale.Math.Poly2.op_Plus_Dot Prims.op_Addition Vale.AES.GHash.ghash_unroll_back Prims.Nil 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)
val lemma_ghash_unroll_back_forward_rec (h 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)

    h: Vale.Math.Poly2_s.poly ->
    prev: Vale.Math.Poly2_s.poly ->
    data: (_: Prims.int -> Vale.AES.GHash.poly128) ->
    k: Prims.int ->
    n: Prims.nat ->
    m: Prims.nat
  -> FStar.Pervasives.Lemma (requires m < n)
      (ensures
        Vale.AES.GHash.ghash_unroll h prev data k n 0 ==
        Vale.AES.GHash.ghash_unroll h prev data k (n - 1 - m) (m + 1) +.
        Vale.AES.GHash.ghash_unroll_back h prev data k (n + 1) m)