let maintain_of (f':flags_t) (f:flags_t) = flag_of f' == flag_of f /\ valid_of f' == valid_of f
let maintain_of (f' f: flags_t) =
flag_of f' == flag_of f /\ valid_of f' == valid_of f
Vale.Bignum.X64.fsti.checked
Vale.X64.State.fsti.checked Vale.X64.Stack_i.fsti.checked Vale.X64.QuickCodes.fsti.checked Vale.X64.QuickCode.fst.checked Vale.X64.Memory.fsti.checked Vale.X64.Machine_s.fst.checked Vale.X64.InsStack.fsti.checked Vale.X64.InsMem.fsti.checked Vale.X64.InsBasic.fsti.checked Vale.X64.Flags.fsti.checked Vale.X64.Decls.fsti.checked Vale.X64.CPU_Features_s.fst.checked Vale.Def.Words_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Bignum.Defs.fsti.checked Vale.Arch.Types.fsti.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Vale.Bignum.X64.fsti
Vale.Bignum.X64.flags_t Prims.l_and Prims.eq2 Vale.Def.Words_s.nat1 Vale.Bignum.X64.flag_of Prims.bool Vale.X64.Decls.valid_of Prims.logical
module Vale.Bignum.X64
open Vale.Def.Words_s
open Vale.Def.Types_s
open Vale.Arch.Types
open Vale.X64.Machine_s
open Vale.X64.Memory
open Vale.X64.Stack_i
open Vale.X64.State
open Vale.X64.Decls
open Vale.X64.InsBasic
open Vale.X64.InsMem
open Vale.X64.InsStack
open Vale.X64.QuickCode
open Vale.X64.QuickCodes
open Vale.X64.CPU_Features_s
open Vale.Bignum.Defs
let flags_t = Vale.X64.Flags.t
val flag_cf (f:flags_t) : nat1
val flag_of (f:flags_t) : nat1
let update_cf (f':flags_t) (c:nat1) = flag_cf f' == c /\ valid_cf f'
let update_of (f':flags_t) (o:nat1) = flag_of f' == o /\ valid_of f'
val maintain_of : f': Vale.Bignum.X64.flags_t -> f: Vale.Bignum.X64.flags_t -> Prims.logical
f': Vale.Bignum.X64.flags_t -> f: Vale.Bignum.X64.flags_t -> Prims.logical