val gf128_power (h:poly) (n:nat) : poly
let gf128_power h n = shift_gf128_key_1 (g_power h n)
val gf128_power (h:poly) (n:nat) : poly
let gf128_power h n =
shift_gf128_key_1 (g_power h n)
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.nat Vale.AES.GHash.shift_gf128_key_1 Vale.AES.GHash.g_power
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 = ()
val gf128_power (h:poly) (n:nat) : poly
h: Vale.Math.Poly2_s.poly -> n: Prims.nat -> Vale.Math.Poly2_s.poly