val set_to_one_LE (q: quad32) : quad32
let set_to_one_LE (q:quad32) : quad32 = four_insert q 1 0
val set_to_one_LE (q: quad32) : quad32
let set_to_one_LE (q: quad32) : quad32 =
four_insert q 1 0
Vale.AES.GCM.fsti.checked
Vale.Def.Words_s.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Words.Four_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Opaque_s.fsti.checked Vale.Arch.Types.fsti.checked Vale.AES.GHash_s.fst.checked Vale.AES.GHash.fsti.checked Vale.AES.GCTR_s.fst.checked Vale.AES.GCTR.fsti.checked Vale.AES.GCM_s.fst.checked Vale.AES.GCM_helpers.fsti.checked Vale.AES.AES_s.fst.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Calc.fsti.checked
Vale.AES.GCM.fsti
Vale.Def.Types_s.quad32 Vale.Def.Words.Four_s.four_insert Vale.Def.Types_s.nat32
module Vale.AES.GCM

open Vale.Def.Opaque_s
open Vale.Def.Types_s
open Vale.Arch.Types
open Vale.AES.GCM_s
open Vale.AES.AES_s
open Vale.AES.GCM_helpers
open Vale.AES.GCTR_s
open Vale.AES.GCTR
open Vale.AES.GHash_s
open FStar.Mul
open FStar.Seq
open Vale.Def.Words_s
open Vale.Def.Words.Seq_s
open FStar.Calc

open Vale.Def.Words.Four_s
val set_to_one_LE (q: quad32) : quad32
q: Vale.Def.Types_s.quad32 -> Vale.Def.Types_s.quad32