val updated_cf (new_flags:Flags.t) (new_cf:bool) : Pure bool
  (requires True)
  (ensures fun b -> b <==> cf new_flags == new_cf /\ valid_cf new_flags)
let updated_cf new_flags new_cf = Lemmas.cf new_flags = Some new_cf
val updated_cf (new_flags:Flags.t) (new_cf:bool) : Pure bool
  (requires True)
  (ensures fun b -> b <==> cf new_flags == new_cf /\ valid_cf new_flags)
let updated_cf new_flags new_cf =
Lemmas.cf new_flags = Some new_cf
Vale.X64.Decls.fst.checked
Vale.X64.StateLemmas.fsti.checked Vale.X64.State.fsti.checked Vale.X64.Print_s.fst.checked Vale.X64.Memory_Sems.fsti.checked Vale.X64.Machine_Semantics_s.fst.checked Vale.X64.Machine_s.fst.checked Vale.X64.Lemmas.fsti.checked Vale.X64.Bytes_Code_s.fst.checked Vale.Def.PossiblyMonad.fst.checked prims.fst.checked FStar.UInt.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Map.fsti.checked FStar.IO.fst.checked
Vale.X64.Decls.fst
Vale.X64.Flags.t Prims.bool Prims.op_Equality FStar.Pervasives.Native.option Vale.X64.Lemmas.cf FStar.Pervasives.Native.Some
module Vale.X64.Decls
open FStar.Mul
open Vale.X64.Machine_s
open Vale.X64
open Vale.X64.State
open Vale.X64.StateLemmas
open FStar.UInt
module P = Vale.X64.Print_s
module BC = Vale.X64.Bytes_Code_s
module BS = Vale.X64.Machine_Semantics_s
#reset-options "--max_fuel 0 --max_ifuel 0 --smtencoding.elim_box true --smtencoding.l_arith_repr boxwrap --smtencoding.nl_arith_repr boxwrap --z3cliopt smt.arith.nl=true --using_facts_from 'Prims FStar.UInt Vale.Def.Words_s FStar.UInt64'"
let lemma_mul_in_bounds (x y:nat64) : Lemma (requires x * y < pow2_64) (ensures FStar.UInt.mul_mod #64 x y == x * y) = ()

#reset-options "--z3cliopt smt.arith.nl=true --using_facts_from Prims --using_facts_from FStar.Math"
let lemma_mul_nat (x:nat) (y:nat) : Lemma (ensures 0 <= (x * y)) = ()
#reset-options "--initial_fuel 2 --max_fuel 2"

let cf flags = match Lemmas.cf flags with | Some v -> v | None -> false
let overflow flags = match Lemmas.overflow flags with | Some v -> v | None -> false
let valid_cf flags = match Lemmas.cf flags with | Some v -> true | None -> false
val updated_cf (new_flags:Flags.t) (new_cf:bool) : Pure bool
  (requires True)
  (ensures fun b -> b <==> cf new_flags == new_cf /\ valid_cf new_flags)
new_flags: Vale.X64.Flags.t -> new_cf: Prims.bool -> Prims.Pure Prims.bool