val shift_gf128_key_1 (h: poly) : poly
let shift_gf128_key_1 (h:poly) : poly =
  shift_key_1 128 gf128_modulus_low_terms h
val shift_gf128_key_1 (h: poly) : poly
let shift_gf128_key_1 (h: poly) : poly =
shift_key_1 128 gf128_modulus_low_terms h
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 Vale.AES.GF128.shift_key_1 Vale.AES.GF128_s.gf128_modulus_low_terms
module Vale.AES.GHash
open FStar.Mul
open Vale.Math.Poly2.Lemmas
open Vale.Math.Poly2.Words

friend Vale.AES.OptPublic

#reset-options
val shift_gf128_key_1 (h: poly) : poly
h: Vale.Math.Poly2_s.poly -> Vale.Math.Poly2_s.poly