val g_power (a:poly) (n:nat) : poly
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)
val g_power (a:poly) (n:nat) : poly
let rec g_power (a: poly) (n: nat) : poly =
if n = 0 then zero else if n = 1 then a else a *~ g_power a (n - 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.nat Prims.op_Equality Prims.int Vale.Math.Poly2_s.zero Prims.bool Vale.AES.GF128.op_Star_Tilde Vale.AES.GHash.g_power Prims.op_Subtraction
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
val g_power (a:poly) (n:nat) : poly
a: Vale.Math.Poly2_s.poly -> n: Prims.nat -> Vale.Math.Poly2_s.poly