val va_quick_Adox_64 (dst: va_operand_dst_opr64) (src: va_operand_opr64)
    : (va_quickCode unit (va_code_Adox_64 dst src))
let va_quick_Adox_64 (dst:va_operand_dst_opr64) (src:va_operand_opr64) : (va_quickCode unit
  (va_code_Adox_64 dst src)) =
  (va_QProc (va_code_Adox_64 dst src) ([va_Mod_flags; va_mod_dst_opr64 dst]) (va_wp_Adox_64 dst
    src) (va_wpProof_Adox_64 dst src))
val va_quick_Adox_64 (dst: va_operand_dst_opr64) (src: va_operand_opr64)
    : (va_quickCode unit (va_code_Adox_64 dst src))
let va_quick_Adox_64 (dst: va_operand_dst_opr64) (src: va_operand_opr64)
    : (va_quickCode unit (va_code_Adox_64 dst src)) =
(va_QProc (va_code_Adox_64 dst src)
    ([va_Mod_flags; va_mod_dst_opr64 dst])
    (va_wp_Adox_64 dst src)
    (va_wpProof_Adox_64 dst src))
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.X64.Decls.va_operand_dst_opr64 Vale.X64.Decls.va_operand_opr64 Vale.X64.QuickCode.va_QProc Prims.unit Vale.Bignum.X64.va_code_Adox_64 Prims.Cons Vale.X64.QuickCode.mod_t Vale.X64.QuickCode.va_Mod_flags Vale.X64.QuickCode.va_mod_dst_opr64 Prims.Nil Vale.Bignum.X64.va_wp_Adox_64 Vale.Bignum.X64.va_wpProof_Adox_64 Vale.X64.QuickCode.va_quickCode
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'
let maintain_cf (f':flags_t) (f:flags_t) = flag_cf f' == flag_cf f /\ valid_cf f' == valid_cf f
let maintain_of (f':flags_t) (f:flags_t) = flag_of f' == flag_of f /\ valid_of f' == valid_of f
//-- reveal_flags

val reveal_flags : f:flags_t
  -> Lemma
  (requires true)
  (ensures (flag_cf f = 1 == Vale.X64.Decls.cf f /\ flag_of f = 1 == Vale.X64.Decls.overflow f))
//--
//-- lemma_add_hi_lo64

val lemma_add_hi_lo64 : dummy:int
  -> Lemma
  (requires true)
  (ensures (forall (a:nat64) (b:nat64) (c:nat1) . {:pattern(add_lo a b c); (add_hi a b
    c)}Vale.Bignum.Defs.add_lo a b c + va_mul_nat pow2_64 (Vale.Bignum.Defs.add_hi a b c) == a + b
    + c))
//--
//-- Adcx_64

val va_code_Adcx_64 : dst:va_operand_dst_opr64 -> src:va_operand_opr64 -> Tot va_code

val va_codegen_success_Adcx_64 : dst:va_operand_dst_opr64 -> src:va_operand_opr64 -> Tot va_pbool

val va_lemma_Adcx_64 : va_b0:va_code -> va_s0:va_state -> dst:va_operand_dst_opr64 ->
  src:va_operand_opr64
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Adcx_64 dst src) va_s0 /\ va_is_dst_dst_opr64 dst
    va_s0 /\ va_is_src_opr64 src va_s0 /\ va_get_ok va_s0 /\ adx_enabled /\ Vale.X64.Decls.valid_cf
    (va_get_flags va_s0)))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    va_eval_dst_opr64 va_sM dst == Vale.Bignum.Defs.add_lo (va_eval_dst_opr64 va_s0 dst)
    (va_eval_opr64 va_s0 src) (flag_cf (va_get_flags va_s0)) /\ update_cf (va_get_flags va_sM)
    (Vale.Bignum.Defs.add_hi (va_eval_dst_opr64 va_s0 dst) (va_eval_opr64 va_s0 src) (flag_cf
    (va_get_flags va_s0))) /\ maintain_of (va_get_flags va_sM) (va_get_flags va_s0) /\ va_state_eq
    va_sM (va_update_flags va_sM (va_update_ok va_sM (va_update_operand_dst_opr64 dst va_sM
    va_s0)))))
[@ va_qattr]
let va_wp_Adcx_64 (dst:va_operand_dst_opr64) (src:va_operand_opr64) (va_s0:va_state)
  (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_is_dst_dst_opr64 dst va_s0 /\ va_is_src_opr64 src va_s0 /\ va_get_ok va_s0 /\ adx_enabled /\
    Vale.X64.Decls.valid_cf (va_get_flags va_s0) /\ (forall (va_x_dst:va_value_dst_opr64)
    (va_x_efl:Vale.X64.Flags.t) . let va_sM = va_upd_flags va_x_efl (va_upd_operand_dst_opr64 dst
    va_x_dst va_s0) in va_get_ok va_sM /\ va_eval_dst_opr64 va_sM dst == Vale.Bignum.Defs.add_lo
    (va_eval_dst_opr64 va_s0 dst) (va_eval_opr64 va_s0 src) (flag_cf (va_get_flags va_s0)) /\
    update_cf (va_get_flags va_sM) (Vale.Bignum.Defs.add_hi (va_eval_dst_opr64 va_s0 dst)
    (va_eval_opr64 va_s0 src) (flag_cf (va_get_flags va_s0))) /\ maintain_of (va_get_flags va_sM)
    (va_get_flags va_s0) ==> va_k va_sM (())))

val va_wpProof_Adcx_64 : dst:va_operand_dst_opr64 -> src:va_operand_opr64 -> va_s0:va_state ->
  va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Adcx_64 dst src va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Adcx_64 dst src) ([va_Mod_flags;
    va_mod_dst_opr64 dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_Adcx_64 (dst:va_operand_dst_opr64) (src:va_operand_opr64) : (va_quickCode unit
  (va_code_Adcx_64 dst src)) =
  (va_QProc (va_code_Adcx_64 dst src) ([va_Mod_flags; va_mod_dst_opr64 dst]) (va_wp_Adcx_64 dst
    src) (va_wpProof_Adcx_64 dst src))
//--
//-- Adox_64

val va_code_Adox_64 : dst:va_operand_dst_opr64 -> src:va_operand_opr64 -> Tot va_code

val va_codegen_success_Adox_64 : dst:va_operand_dst_opr64 -> src:va_operand_opr64 -> Tot va_pbool

val va_lemma_Adox_64 : va_b0:va_code -> va_s0:va_state -> dst:va_operand_dst_opr64 ->
  src:va_operand_opr64
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Adox_64 dst src) va_s0 /\ va_is_dst_dst_opr64 dst
    va_s0 /\ va_is_src_opr64 src va_s0 /\ va_get_ok va_s0 /\ adx_enabled /\ Vale.X64.Decls.valid_of
    (va_get_flags va_s0)))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    va_eval_dst_opr64 va_sM dst == Vale.Bignum.Defs.add_lo (va_eval_dst_opr64 va_s0 dst)
    (va_eval_opr64 va_s0 src) (flag_of (va_get_flags va_s0)) /\ update_of (va_get_flags va_sM)
    (Vale.Bignum.Defs.add_hi (va_eval_dst_opr64 va_s0 dst) (va_eval_opr64 va_s0 src) (flag_of
    (va_get_flags va_s0))) /\ maintain_cf (va_get_flags va_sM) (va_get_flags va_s0) /\ va_state_eq
    va_sM (va_update_flags va_sM (va_update_ok va_sM (va_update_operand_dst_opr64 dst va_sM
    va_s0)))))
[@ va_qattr]
let va_wp_Adox_64 (dst:va_operand_dst_opr64) (src:va_operand_opr64) (va_s0:va_state)
  (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_is_dst_dst_opr64 dst va_s0 /\ va_is_src_opr64 src va_s0 /\ va_get_ok va_s0 /\ adx_enabled /\
    Vale.X64.Decls.valid_of (va_get_flags va_s0) /\ (forall (va_x_dst:va_value_dst_opr64)
    (va_x_efl:Vale.X64.Flags.t) . let va_sM = va_upd_flags va_x_efl (va_upd_operand_dst_opr64 dst
    va_x_dst va_s0) in va_get_ok va_sM /\ va_eval_dst_opr64 va_sM dst == Vale.Bignum.Defs.add_lo
    (va_eval_dst_opr64 va_s0 dst) (va_eval_opr64 va_s0 src) (flag_of (va_get_flags va_s0)) /\
    update_of (va_get_flags va_sM) (Vale.Bignum.Defs.add_hi (va_eval_dst_opr64 va_s0 dst)
    (va_eval_opr64 va_s0 src) (flag_of (va_get_flags va_s0))) /\ maintain_cf (va_get_flags va_sM)
    (va_get_flags va_s0) ==> va_k va_sM (())))

val va_wpProof_Adox_64 : dst:va_operand_dst_opr64 -> src:va_operand_opr64 -> va_s0:va_state ->
  va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Adox_64 dst src va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Adox_64 dst src) ([va_Mod_flags;
    va_mod_dst_opr64 dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_Adox_64 (dst:va_operand_dst_opr64) (src:va_operand_opr64) : (va_quickCode unit
val va_quick_Adox_64 (dst: va_operand_dst_opr64) (src: va_operand_opr64)
    : (va_quickCode unit (va_code_Adox_64 dst src))
dst: Vale.X64.Decls.va_operand_dst_opr64 -> src: Vale.X64.Decls.va_operand_opr64
  -> Vale.X64.QuickCode.va_quickCode Prims.unit (Vale.Bignum.X64.va_code_Adox_64 dst src)