val va_wp_MulHigh64U
      (dst src1 src2: va_operand_reg_opr)
      (va_s0: va_state)
      (va_k: (va_state -> unit -> Type0))
    : Type0
let va_wp_MulHigh64U (dst:va_operand_reg_opr) (src1:va_operand_reg_opr) (src2:va_operand_reg_opr)
  (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_is_dst_reg_opr dst va_s0 /\ va_is_src_reg_opr src1 va_s0 /\ va_is_src_reg_opr src2 va_s0 /\
    va_get_ok va_s0 /\ (forall (va_x_dst:va_value_reg_opr) . let va_sM = va_upd_operand_reg_opr dst
    va_x_dst va_s0 in va_get_ok va_sM /\ va_eval_reg_opr va_sM dst == va_mul_nat (va_eval_reg_opr
    va_s0 src1) (va_eval_reg_opr va_s0 src2) `op_Division` pow2_64 ==> va_k va_sM (())))
val va_wp_MulHigh64U
      (dst src1 src2: va_operand_reg_opr)
      (va_s0: va_state)
      (va_k: (va_state -> unit -> Type0))
    : Type0
let va_wp_MulHigh64U
      (dst src1 src2: va_operand_reg_opr)
      (va_s0: va_state)
      (va_k: (va_state -> unit -> Type0))
    : Type0 =
(va_is_dst_reg_opr dst va_s0 /\ va_is_src_reg_opr src1 va_s0 /\ va_is_src_reg_opr src2 va_s0 /\
  va_get_ok va_s0 /\
  (forall (va_x_dst: va_value_reg_opr).
      let va_sM = va_upd_operand_reg_opr dst va_x_dst va_s0 in
      va_get_ok va_sM /\
      va_eval_reg_opr va_sM dst ==
      (va_mul_nat (va_eval_reg_opr va_s0 src1) (va_eval_reg_opr va_s0 src2))
      `op_Division`
      pow2_64 ==>
      va_k va_sM (())))
Vale.PPC64LE.InsBasic.fsti.checked
Vale.PPC64LE.State.fsti.checked Vale.PPC64LE.Stack_i.fsti.checked Vale.PPC64LE.QuickCode.fst.checked Vale.PPC64LE.Memory.fsti.checked Vale.PPC64LE.Machine_s.fst.checked Vale.PPC64LE.Decls.fsti.checked Vale.Arch.Types.fsti.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.PPC64LE.InsBasic.fsti
Vale.PPC64LE.Decls.va_operand_reg_opr Vale.PPC64LE.Decls.va_state Prims.unit Prims.l_and Vale.PPC64LE.Decls.va_is_dst_reg_opr Vale.PPC64LE.Decls.va_is_src_reg_opr Prims.b2t Vale.PPC64LE.Decls.va_get_ok Prims.l_Forall Vale.PPC64LE.Decls.va_value_reg_opr Prims.l_imp Prims.eq2 Prims.int Vale.PPC64LE.Decls.va_eval_reg_opr Prims.op_Division Vale.PPC64LE.Decls.va_mul_nat Vale.PPC64LE.Machine_s.pow2_64 Vale.PPC64LE.Machine_s.state Vale.PPC64LE.Decls.va_upd_operand_reg_opr
module Vale.PPC64LE.InsBasic
open FStar.Mul
open Vale.Arch.Types
open Vale.PPC64LE.Machine_s
open Vale.PPC64LE.State
open Vale.PPC64LE.Decls
open Vale.PPC64LE.QuickCode
unfold let vale_heap = Vale.PPC64LE.Memory.vale_heap
unfold let vale_stack = Vale.PPC64LE.Stack_i.vale_stack
//-- Move

val va_code_Move : dst:va_operand_reg_opr -> src:va_operand_reg_opr -> Tot va_code

val va_codegen_success_Move : dst:va_operand_reg_opr -> src:va_operand_reg_opr -> Tot va_pbool

val va_lemma_Move : va_b0:va_code -> va_s0:va_state -> dst:va_operand_reg_opr ->
  src:va_operand_reg_opr
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Move dst src) va_s0 /\ va_is_dst_reg_opr dst va_s0 /\
    va_is_src_reg_opr src va_s0 /\ va_get_ok 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_reg_opr va_sM dst == va_eval_reg_opr va_s0 src /\ va_state_eq va_sM (va_update_ok va_sM
    (va_update_operand_reg_opr dst va_sM va_s0))))
[@ va_qattr]
let va_wp_Move (dst:va_operand_reg_opr) (src:va_operand_reg_opr) (va_s0:va_state) (va_k:(va_state
  -> unit -> Type0)) : Type0 =
  (va_is_dst_reg_opr dst va_s0 /\ va_is_src_reg_opr src va_s0 /\ va_get_ok va_s0 /\ (forall
    (va_x_dst:va_value_reg_opr) . let va_sM = va_upd_operand_reg_opr dst va_x_dst va_s0 in
    va_get_ok va_sM /\ va_eval_reg_opr va_sM dst == va_eval_reg_opr va_s0 src ==> va_k va_sM (())))

val va_wpProof_Move : dst:va_operand_reg_opr -> src:va_operand_reg_opr -> va_s0:va_state ->
  va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Move dst src va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Move dst src) ([va_mod_reg_opr dst])
    va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_Move (dst:va_operand_reg_opr) (src:va_operand_reg_opr) : (va_quickCode unit
  (va_code_Move dst src)) =
  (va_QProc (va_code_Move dst src) ([va_mod_reg_opr dst]) (va_wp_Move dst src) (va_wpProof_Move dst
    src))
//--
//-- LoadImm64

val va_code_LoadImm64 : dst:va_operand_reg_opr -> src:simm16 -> Tot va_code

val va_codegen_success_LoadImm64 : dst:va_operand_reg_opr -> src:simm16 -> Tot va_pbool

val va_lemma_LoadImm64 : va_b0:va_code -> va_s0:va_state -> dst:va_operand_reg_opr -> src:simm16
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_LoadImm64 dst src) va_s0 /\ va_is_dst_reg_opr dst
    va_s0 /\ va_get_ok 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_reg_opr va_sM dst == src `op_Modulus` pow2_64 /\ va_state_eq va_sM (va_update_ok va_sM
    (va_update_operand_reg_opr dst va_sM va_s0))))
[@ va_qattr]
let va_wp_LoadImm64 (dst:va_operand_reg_opr) (src:simm16) (va_s0:va_state) (va_k:(va_state -> unit
  -> Type0)) : Type0 =
  (va_is_dst_reg_opr dst va_s0 /\ va_get_ok va_s0 /\ (forall (va_x_dst:va_value_reg_opr) . let
    va_sM = va_upd_operand_reg_opr dst va_x_dst va_s0 in va_get_ok va_sM /\ va_eval_reg_opr va_sM
    dst == src `op_Modulus` pow2_64 ==> va_k va_sM (())))

val va_wpProof_LoadImm64 : dst:va_operand_reg_opr -> src:simm16 -> va_s0:va_state -> va_k:(va_state
  -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_LoadImm64 dst src va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_LoadImm64 dst src) ([va_mod_reg_opr
    dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_LoadImm64 (dst:va_operand_reg_opr) (src:simm16) : (va_quickCode unit
  (va_code_LoadImm64 dst src)) =
  (va_QProc (va_code_LoadImm64 dst src) ([va_mod_reg_opr dst]) (va_wp_LoadImm64 dst src)
    (va_wpProof_LoadImm64 dst src))
//--
//-- LoadImmShl64

val va_code_LoadImmShl64 : dst:va_operand_reg_opr -> src:simm16 -> Tot va_code

val va_codegen_success_LoadImmShl64 : dst:va_operand_reg_opr -> src:simm16 -> Tot va_pbool

val va_lemma_LoadImmShl64 : va_b0:va_code -> va_s0:va_state -> dst:va_operand_reg_opr -> src:simm16
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_LoadImmShl64 dst src) va_s0 /\ va_is_dst_reg_opr dst
    va_s0 /\ va_get_ok 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_reg_opr va_sM dst == Vale.Arch.Types.ishl64 (src `op_Modulus` pow2_64) 16 /\
    va_state_eq va_sM (va_update_ok va_sM (va_update_operand_reg_opr dst va_sM va_s0))))
[@ va_qattr]
let va_wp_LoadImmShl64 (dst:va_operand_reg_opr) (src:simm16) (va_s0:va_state) (va_k:(va_state ->
  unit -> Type0)) : Type0 =
  (va_is_dst_reg_opr dst va_s0 /\ va_get_ok va_s0 /\ (forall (va_x_dst:va_value_reg_opr) . let
    va_sM = va_upd_operand_reg_opr dst va_x_dst va_s0 in va_get_ok va_sM /\ va_eval_reg_opr va_sM
    dst == Vale.Arch.Types.ishl64 (src `op_Modulus` pow2_64) 16 ==> va_k va_sM (())))

val va_wpProof_LoadImmShl64 : dst:va_operand_reg_opr -> src:simm16 -> va_s0:va_state ->
  va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_LoadImmShl64 dst src va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_LoadImmShl64 dst src) ([va_mod_reg_opr
    dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_LoadImmShl64 (dst:va_operand_reg_opr) (src:simm16) : (va_quickCode unit
  (va_code_LoadImmShl64 dst src)) =
  (va_QProc (va_code_LoadImmShl64 dst src) ([va_mod_reg_opr dst]) (va_wp_LoadImmShl64 dst src)
    (va_wpProof_LoadImmShl64 dst src))
//--
//-- AddLa

val va_code_AddLa : dst:va_operand_reg_opr -> src1:va_operand_reg_opr -> src2:simm16 -> Tot va_code

val va_codegen_success_AddLa : dst:va_operand_reg_opr -> src1:va_operand_reg_opr -> src2:simm16 ->
  Tot va_pbool

val va_lemma_AddLa : va_b0:va_code -> va_s0:va_state -> dst:va_operand_reg_opr ->
  src1:va_operand_reg_opr -> src2:simm16
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_AddLa dst src1 src2) va_s0 /\ va_is_dst_reg_opr dst
    va_s0 /\ va_is_src_reg_opr src1 va_s0 /\ va_get_ok va_s0 /\ (0 <= va_eval_reg_opr va_s0 src1 +
    src2 /\ va_eval_reg_opr va_s0 src1 + src2 < pow2_64)))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    va_eval_reg_opr va_sM dst == va_eval_reg_opr va_s0 src1 + src2 /\ va_state_eq va_sM
    (va_update_ok va_sM (va_update_operand_reg_opr dst va_sM va_s0))))
[@ va_qattr]
let va_wp_AddLa (dst:va_operand_reg_opr) (src1:va_operand_reg_opr) (src2:simm16) (va_s0:va_state)
  (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_is_dst_reg_opr dst va_s0 /\ va_is_src_reg_opr src1 va_s0 /\ va_get_ok va_s0 /\ (0 <=
    va_eval_reg_opr va_s0 src1 + src2 /\ va_eval_reg_opr va_s0 src1 + src2 < pow2_64) /\ (forall
    (va_x_dst:va_value_reg_opr) . let va_sM = va_upd_operand_reg_opr dst va_x_dst va_s0 in
    va_get_ok va_sM /\ va_eval_reg_opr va_sM dst == va_eval_reg_opr va_s0 src1 + src2 ==> va_k
    va_sM (())))

val va_wpProof_AddLa : dst:va_operand_reg_opr -> src1:va_operand_reg_opr -> src2:simm16 ->
  va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_AddLa dst src1 src2 va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_AddLa dst src1 src2) ([va_mod_reg_opr
    dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_AddLa (dst:va_operand_reg_opr) (src1:va_operand_reg_opr) (src2:simm16) : (va_quickCode
  unit (va_code_AddLa dst src1 src2)) =
  (va_QProc (va_code_AddLa dst src1 src2) ([va_mod_reg_opr dst]) (va_wp_AddLa dst src1 src2)
    (va_wpProof_AddLa dst src1 src2))
//--
//-- Add

val va_code_Add : dst:va_operand_reg_opr -> src1:va_operand_reg_opr -> src2:va_operand_reg_opr ->
  Tot va_code

val va_codegen_success_Add : dst:va_operand_reg_opr -> src1:va_operand_reg_opr ->
  src2:va_operand_reg_opr -> Tot va_pbool

val va_lemma_Add : va_b0:va_code -> va_s0:va_state -> dst:va_operand_reg_opr ->
  src1:va_operand_reg_opr -> src2:va_operand_reg_opr
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Add dst src1 src2) va_s0 /\ va_is_dst_reg_opr dst
    va_s0 /\ va_is_src_reg_opr src1 va_s0 /\ va_is_src_reg_opr src2 va_s0 /\ va_get_ok va_s0 /\
    va_eval_reg_opr va_s0 src1 + va_eval_reg_opr va_s0 src2 < pow2_64))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    va_eval_reg_opr va_sM dst == va_eval_reg_opr va_s0 src1 + va_eval_reg_opr va_s0 src2 /\
    va_state_eq va_sM (va_update_ok va_sM (va_update_operand_reg_opr dst va_sM va_s0))))
[@ va_qattr]
let va_wp_Add (dst:va_operand_reg_opr) (src1:va_operand_reg_opr) (src2:va_operand_reg_opr)
  (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_is_dst_reg_opr dst va_s0 /\ va_is_src_reg_opr src1 va_s0 /\ va_is_src_reg_opr src2 va_s0 /\
    va_get_ok va_s0 /\ va_eval_reg_opr va_s0 src1 + va_eval_reg_opr va_s0 src2 < pow2_64 /\ (forall
    (va_x_dst:va_value_reg_opr) . let va_sM = va_upd_operand_reg_opr dst va_x_dst va_s0 in
    va_get_ok va_sM /\ va_eval_reg_opr va_sM dst == va_eval_reg_opr va_s0 src1 + va_eval_reg_opr
    va_s0 src2 ==> va_k va_sM (())))

val va_wpProof_Add : dst:va_operand_reg_opr -> src1:va_operand_reg_opr -> src2:va_operand_reg_opr
  -> va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Add dst src1 src2 va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Add dst src1 src2) ([va_mod_reg_opr
    dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_Add (dst:va_operand_reg_opr) (src1:va_operand_reg_opr) (src2:va_operand_reg_opr) :
  (va_quickCode unit (va_code_Add dst src1 src2)) =
  (va_QProc (va_code_Add dst src1 src2) ([va_mod_reg_opr dst]) (va_wp_Add dst src1 src2)
    (va_wpProof_Add dst src1 src2))
//--
//-- AddWrap

val va_code_AddWrap : dst:va_operand_reg_opr -> src1:va_operand_reg_opr -> src2:va_operand_reg_opr
  -> Tot va_code

val va_codegen_success_AddWrap : dst:va_operand_reg_opr -> src1:va_operand_reg_opr ->
  src2:va_operand_reg_opr -> Tot va_pbool

val va_lemma_AddWrap : va_b0:va_code -> va_s0:va_state -> dst:va_operand_reg_opr ->
  src1:va_operand_reg_opr -> src2:va_operand_reg_opr
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_AddWrap dst src1 src2) va_s0 /\ va_is_dst_reg_opr dst
    va_s0 /\ va_is_src_reg_opr src1 va_s0 /\ va_is_src_reg_opr src2 va_s0 /\ va_get_ok 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_reg_opr va_sM dst == Vale.Arch.Types.add_wrap64 (va_eval_reg_opr va_s0 src1)
    (va_eval_reg_opr va_s0 src2) /\ va_state_eq va_sM (va_update_ok va_sM
    (va_update_operand_reg_opr dst va_sM va_s0))))
[@ va_qattr]
let va_wp_AddWrap (dst:va_operand_reg_opr) (src1:va_operand_reg_opr) (src2:va_operand_reg_opr)
  (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_is_dst_reg_opr dst va_s0 /\ va_is_src_reg_opr src1 va_s0 /\ va_is_src_reg_opr src2 va_s0 /\
    va_get_ok va_s0 /\ (forall (va_x_dst:va_value_reg_opr) . let va_sM = va_upd_operand_reg_opr dst
    va_x_dst va_s0 in va_get_ok va_sM /\ va_eval_reg_opr va_sM dst == Vale.Arch.Types.add_wrap64
    (va_eval_reg_opr va_s0 src1) (va_eval_reg_opr va_s0 src2) ==> va_k va_sM (())))

val va_wpProof_AddWrap : dst:va_operand_reg_opr -> src1:va_operand_reg_opr ->
  src2:va_operand_reg_opr -> va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_AddWrap dst src1 src2 va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_AddWrap dst src1 src2)
    ([va_mod_reg_opr dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_AddWrap (dst:va_operand_reg_opr) (src1:va_operand_reg_opr) (src2:va_operand_reg_opr) :
  (va_quickCode unit (va_code_AddWrap dst src1 src2)) =
  (va_QProc (va_code_AddWrap dst src1 src2) ([va_mod_reg_opr dst]) (va_wp_AddWrap dst src1 src2)
    (va_wpProof_AddWrap dst src1 src2))
//--
//-- AddImm

val va_code_AddImm : dst:va_operand_reg_opr -> src1:va_operand_reg_opr -> src2:simm16 -> Tot va_code

val va_codegen_success_AddImm : dst:va_operand_reg_opr -> src1:va_operand_reg_opr -> src2:simm16 ->
  Tot va_pbool

val va_lemma_AddImm : va_b0:va_code -> va_s0:va_state -> dst:va_operand_reg_opr ->
  src1:va_operand_reg_opr -> src2:simm16
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_AddImm dst src1 src2) va_s0 /\ va_is_dst_reg_opr dst
    va_s0 /\ va_is_src_reg_opr src1 va_s0 /\ va_get_ok va_s0 /\ va_eval_reg_opr va_s0 src1 +
    Vale.PPC64LE.Machine_s.int_to_nat64 src2 < pow2_64))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    va_eval_reg_opr va_sM dst == va_eval_reg_opr va_s0 src1 + Vale.PPC64LE.Machine_s.int_to_nat64
    src2 /\ va_state_eq va_sM (va_update_ok va_sM (va_update_operand_reg_opr dst va_sM va_s0))))
[@ va_qattr]
let va_wp_AddImm (dst:va_operand_reg_opr) (src1:va_operand_reg_opr) (src2:simm16) (va_s0:va_state)
  (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_is_dst_reg_opr dst va_s0 /\ va_is_src_reg_opr src1 va_s0 /\ va_get_ok va_s0 /\
    va_eval_reg_opr va_s0 src1 + Vale.PPC64LE.Machine_s.int_to_nat64 src2 < pow2_64 /\ (forall
    (va_x_dst:va_value_reg_opr) . let va_sM = va_upd_operand_reg_opr dst va_x_dst va_s0 in
    va_get_ok va_sM /\ va_eval_reg_opr va_sM dst == va_eval_reg_opr va_s0 src1 +
    Vale.PPC64LE.Machine_s.int_to_nat64 src2 ==> va_k va_sM (())))

val va_wpProof_AddImm : dst:va_operand_reg_opr -> src1:va_operand_reg_opr -> src2:simm16 ->
  va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_AddImm dst src1 src2 va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_AddImm dst src1 src2) ([va_mod_reg_opr
    dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_AddImm (dst:va_operand_reg_opr) (src1:va_operand_reg_opr) (src2:simm16) :
  (va_quickCode unit (va_code_AddImm dst src1 src2)) =
  (va_QProc (va_code_AddImm dst src1 src2) ([va_mod_reg_opr dst]) (va_wp_AddImm dst src1 src2)
    (va_wpProof_AddImm dst src1 src2))
//--
//-- AddImmWrap

val va_code_AddImmWrap : dst:va_operand_reg_opr -> src1:va_operand_reg_opr -> src2:simm16 -> Tot
  va_code

val va_codegen_success_AddImmWrap : dst:va_operand_reg_opr -> src1:va_operand_reg_opr ->
  src2:simm16 -> Tot va_pbool

val va_lemma_AddImmWrap : va_b0:va_code -> va_s0:va_state -> dst:va_operand_reg_opr ->
  src1:va_operand_reg_opr -> src2:simm16
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_AddImmWrap dst src1 src2) va_s0 /\ va_is_dst_reg_opr
    dst va_s0 /\ va_is_src_reg_opr src1 va_s0 /\ va_get_ok 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_reg_opr va_sM dst == Vale.Arch.Types.add_wrap64 (va_eval_reg_opr va_s0 src1)
    (Vale.PPC64LE.Machine_s.int_to_nat64 src2) /\ va_state_eq va_sM (va_update_ok va_sM
    (va_update_operand_reg_opr dst va_sM va_s0))))
[@ va_qattr]
let va_wp_AddImmWrap (dst:va_operand_reg_opr) (src1:va_operand_reg_opr) (src2:simm16)
  (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_is_dst_reg_opr dst va_s0 /\ va_is_src_reg_opr src1 va_s0 /\ va_get_ok va_s0 /\ (forall
    (va_x_dst:va_value_reg_opr) . let va_sM = va_upd_operand_reg_opr dst va_x_dst va_s0 in
    va_get_ok va_sM /\ va_eval_reg_opr va_sM dst == Vale.Arch.Types.add_wrap64 (va_eval_reg_opr
    va_s0 src1) (Vale.PPC64LE.Machine_s.int_to_nat64 src2) ==> va_k va_sM (())))

val va_wpProof_AddImmWrap : dst:va_operand_reg_opr -> src1:va_operand_reg_opr -> src2:simm16 ->
  va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_AddImmWrap dst src1 src2 va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_AddImmWrap dst src1 src2)
    ([va_mod_reg_opr dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_AddImmWrap (dst:va_operand_reg_opr) (src1:va_operand_reg_opr) (src2:simm16) :
  (va_quickCode unit (va_code_AddImmWrap dst src1 src2)) =
  (va_QProc (va_code_AddImmWrap dst src1 src2) ([va_mod_reg_opr dst]) (va_wp_AddImmWrap dst src1
    src2) (va_wpProof_AddImmWrap dst src1 src2))
//--
//-- AddCarry

val va_code_AddCarry : dst:va_operand_reg_opr -> src1:va_operand_reg_opr -> src2:va_operand_reg_opr
  -> Tot va_code

val va_codegen_success_AddCarry : dst:va_operand_reg_opr -> src1:va_operand_reg_opr ->
  src2:va_operand_reg_opr -> Tot va_pbool

val va_lemma_AddCarry : va_b0:va_code -> va_s0:va_state -> dst:va_operand_reg_opr ->
  src1:va_operand_reg_opr -> src2:va_operand_reg_opr
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_AddCarry dst src1 src2) va_s0 /\ va_is_dst_reg_opr dst
    va_s0 /\ va_is_src_reg_opr src1 va_s0 /\ va_is_src_reg_opr src2 va_s0 /\ va_get_ok 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_reg_opr va_sM dst == Vale.Arch.Types.add_wrap64 (va_eval_reg_opr va_s0 src1)
    (va_eval_reg_opr va_s0 src2) /\ Vale.PPC64LE.Decls.xer_ca (va_get_xer va_sM) ==
    (va_eval_reg_opr va_s0 src1 + va_eval_reg_opr va_s0 src2 >= pow2_64) /\ va_state_eq va_sM
    (va_update_xer va_sM (va_update_ok va_sM (va_update_operand_reg_opr dst va_sM va_s0)))))
[@ va_qattr]
let va_wp_AddCarry (dst:va_operand_reg_opr) (src1:va_operand_reg_opr) (src2:va_operand_reg_opr)
  (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_is_dst_reg_opr dst va_s0 /\ va_is_src_reg_opr src1 va_s0 /\ va_is_src_reg_opr src2 va_s0 /\
    va_get_ok va_s0 /\ (forall (va_x_dst:va_value_reg_opr) (va_x_xer:xer_t) . let va_sM =
    va_upd_xer va_x_xer (va_upd_operand_reg_opr dst va_x_dst va_s0) in va_get_ok va_sM /\
    va_eval_reg_opr va_sM dst == Vale.Arch.Types.add_wrap64 (va_eval_reg_opr va_s0 src1)
    (va_eval_reg_opr va_s0 src2) /\ Vale.PPC64LE.Decls.xer_ca (va_get_xer va_sM) ==
    (va_eval_reg_opr va_s0 src1 + va_eval_reg_opr va_s0 src2 >= pow2_64) ==> va_k va_sM (())))

val va_wpProof_AddCarry : dst:va_operand_reg_opr -> src1:va_operand_reg_opr ->
  src2:va_operand_reg_opr -> va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_AddCarry dst src1 src2 va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_AddCarry dst src1 src2) ([va_Mod_xer;
    va_mod_reg_opr dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_AddCarry (dst:va_operand_reg_opr) (src1:va_operand_reg_opr) (src2:va_operand_reg_opr)
  : (va_quickCode unit (va_code_AddCarry dst src1 src2)) =
  (va_QProc (va_code_AddCarry dst src1 src2) ([va_Mod_xer; va_mod_reg_opr dst]) (va_wp_AddCarry dst
    src1 src2) (va_wpProof_AddCarry dst src1 src2))
//--
//-- AddExtended

val va_code_AddExtended : dst:va_operand_reg_opr -> src1:va_operand_reg_opr ->
  src2:va_operand_reg_opr -> Tot va_code

val va_codegen_success_AddExtended : dst:va_operand_reg_opr -> src1:va_operand_reg_opr ->
  src2:va_operand_reg_opr -> Tot va_pbool

val va_lemma_AddExtended : va_b0:va_code -> va_s0:va_state -> dst:va_operand_reg_opr ->
  src1:va_operand_reg_opr -> src2:va_operand_reg_opr
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_AddExtended dst src1 src2) va_s0 /\ va_is_dst_reg_opr
    dst va_s0 /\ va_is_src_reg_opr src1 va_s0 /\ va_is_src_reg_opr src2 va_s0 /\ va_get_ok 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_reg_opr va_sM dst == Vale.Arch.Types.add_wrap64 (Vale.Arch.Types.add_wrap64
    (va_eval_reg_opr va_s0 src1) (va_eval_reg_opr va_s0 src2)) (if Vale.PPC64LE.Decls.xer_ca
    (va_get_xer va_s0) then 1 else 0) /\ Vale.PPC64LE.Decls.xer_ca (va_get_xer va_sM) ==
    (va_eval_reg_opr va_s0 src1 + va_eval_reg_opr va_s0 src2 + (if Vale.PPC64LE.Decls.xer_ca
    (va_get_xer va_s0) then 1 else 0) >= pow2_64) /\ va_state_eq va_sM (va_update_xer va_sM
    (va_update_ok va_sM (va_update_operand_reg_opr dst va_sM va_s0)))))
[@ va_qattr]
let va_wp_AddExtended (dst:va_operand_reg_opr) (src1:va_operand_reg_opr) (src2:va_operand_reg_opr)
  (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_is_dst_reg_opr dst va_s0 /\ va_is_src_reg_opr src1 va_s0 /\ va_is_src_reg_opr src2 va_s0 /\
    va_get_ok va_s0 /\ (forall (va_x_dst:va_value_reg_opr) (va_x_xer:xer_t) . let va_sM =
    va_upd_xer va_x_xer (va_upd_operand_reg_opr dst va_x_dst va_s0) in va_get_ok va_sM /\
    va_eval_reg_opr va_sM dst == Vale.Arch.Types.add_wrap64 (Vale.Arch.Types.add_wrap64
    (va_eval_reg_opr va_s0 src1) (va_eval_reg_opr va_s0 src2)) (va_if (Vale.PPC64LE.Decls.xer_ca
    (va_get_xer va_s0)) (fun _ -> 1) (fun _ -> 0)) /\ Vale.PPC64LE.Decls.xer_ca (va_get_xer va_sM)
    == (va_eval_reg_opr va_s0 src1 + va_eval_reg_opr va_s0 src2 + va_if (Vale.PPC64LE.Decls.xer_ca
    (va_get_xer va_s0)) (fun _ -> 1) (fun _ -> 0) >= pow2_64) ==> va_k va_sM (())))

val va_wpProof_AddExtended : dst:va_operand_reg_opr -> src1:va_operand_reg_opr ->
  src2:va_operand_reg_opr -> va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_AddExtended dst src1 src2 va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_AddExtended dst src1 src2)
    ([va_Mod_xer; va_mod_reg_opr dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_AddExtended (dst:va_operand_reg_opr) (src1:va_operand_reg_opr)
  (src2:va_operand_reg_opr) : (va_quickCode unit (va_code_AddExtended dst src1 src2)) =
  (va_QProc (va_code_AddExtended dst src1 src2) ([va_Mod_xer; va_mod_reg_opr dst])
    (va_wp_AddExtended dst src1 src2) (va_wpProof_AddExtended dst src1 src2))
//--
//-- AddExtendedOV

val va_code_AddExtendedOV : dst:va_operand_reg_opr -> src1:va_operand_reg_opr ->
  src2:va_operand_reg_opr -> Tot va_code

val va_codegen_success_AddExtendedOV : dst:va_operand_reg_opr -> src1:va_operand_reg_opr ->
  src2:va_operand_reg_opr -> Tot va_pbool

val va_lemma_AddExtendedOV : va_b0:va_code -> va_s0:va_state -> dst:va_operand_reg_opr ->
  src1:va_operand_reg_opr -> src2:va_operand_reg_opr
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_AddExtendedOV dst src1 src2) va_s0 /\
    va_is_dst_reg_opr dst va_s0 /\ va_is_src_reg_opr src1 va_s0 /\ va_is_src_reg_opr src2 va_s0 /\
    va_get_ok 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_reg_opr va_sM dst == Vale.Arch.Types.add_wrap64 (Vale.Arch.Types.add_wrap64
    (va_eval_reg_opr va_s0 src1) (va_eval_reg_opr va_s0 src2)) (if Vale.PPC64LE.Decls.xer_ov
    (va_get_xer va_s0) then 1 else 0) /\ Vale.PPC64LE.Decls.xer_ov (va_get_xer va_sM) ==
    (va_eval_reg_opr va_s0 src1 + va_eval_reg_opr va_s0 src2 + (if Vale.PPC64LE.Decls.xer_ov
    (va_get_xer va_s0) then 1 else 0) >= pow2_64) /\ va_state_eq va_sM (va_update_xer va_sM
    (va_update_ok va_sM (va_update_operand_reg_opr dst va_sM va_s0)))))
[@ va_qattr]
let va_wp_AddExtendedOV (dst:va_operand_reg_opr) (src1:va_operand_reg_opr)
  (src2:va_operand_reg_opr) (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_is_dst_reg_opr dst va_s0 /\ va_is_src_reg_opr src1 va_s0 /\ va_is_src_reg_opr src2 va_s0 /\
    va_get_ok va_s0 /\ (forall (va_x_dst:va_value_reg_opr) (va_x_xer:xer_t) . let va_sM =
    va_upd_xer va_x_xer (va_upd_operand_reg_opr dst va_x_dst va_s0) in va_get_ok va_sM /\
    va_eval_reg_opr va_sM dst == Vale.Arch.Types.add_wrap64 (Vale.Arch.Types.add_wrap64
    (va_eval_reg_opr va_s0 src1) (va_eval_reg_opr va_s0 src2)) (va_if (Vale.PPC64LE.Decls.xer_ov
    (va_get_xer va_s0)) (fun _ -> 1) (fun _ -> 0)) /\ Vale.PPC64LE.Decls.xer_ov (va_get_xer va_sM)
    == (va_eval_reg_opr va_s0 src1 + va_eval_reg_opr va_s0 src2 + va_if (Vale.PPC64LE.Decls.xer_ov
    (va_get_xer va_s0)) (fun _ -> 1) (fun _ -> 0) >= pow2_64) ==> va_k va_sM (())))

val va_wpProof_AddExtendedOV : dst:va_operand_reg_opr -> src1:va_operand_reg_opr ->
  src2:va_operand_reg_opr -> va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_AddExtendedOV dst src1 src2 va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_AddExtendedOV dst src1 src2)
    ([va_Mod_xer; va_mod_reg_opr dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_AddExtendedOV (dst:va_operand_reg_opr) (src1:va_operand_reg_opr)
  (src2:va_operand_reg_opr) : (va_quickCode unit (va_code_AddExtendedOV dst src1 src2)) =
  (va_QProc (va_code_AddExtendedOV dst src1 src2) ([va_Mod_xer; va_mod_reg_opr dst])
    (va_wp_AddExtendedOV dst src1 src2) (va_wpProof_AddExtendedOV dst src1 src2))
//--
//-- Sub

val va_code_Sub : dst:va_operand_reg_opr -> src1:va_operand_reg_opr -> src2:va_operand_reg_opr ->
  Tot va_code

val va_codegen_success_Sub : dst:va_operand_reg_opr -> src1:va_operand_reg_opr ->
  src2:va_operand_reg_opr -> Tot va_pbool

val va_lemma_Sub : va_b0:va_code -> va_s0:va_state -> dst:va_operand_reg_opr ->
  src1:va_operand_reg_opr -> src2:va_operand_reg_opr
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Sub dst src1 src2) va_s0 /\ va_is_dst_reg_opr dst
    va_s0 /\ va_is_src_reg_opr src1 va_s0 /\ va_is_src_reg_opr src2 va_s0 /\ va_get_ok va_s0 /\
    va_eval_reg_opr va_s0 src1 - va_eval_reg_opr va_s0 src2 >= 0))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    va_eval_reg_opr va_sM dst == va_eval_reg_opr va_s0 src1 - va_eval_reg_opr va_s0 src2 /\
    va_state_eq va_sM (va_update_ok va_sM (va_update_operand_reg_opr dst va_sM va_s0))))
[@ va_qattr]
let va_wp_Sub (dst:va_operand_reg_opr) (src1:va_operand_reg_opr) (src2:va_operand_reg_opr)
  (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_is_dst_reg_opr dst va_s0 /\ va_is_src_reg_opr src1 va_s0 /\ va_is_src_reg_opr src2 va_s0 /\
    va_get_ok va_s0 /\ va_eval_reg_opr va_s0 src1 - va_eval_reg_opr va_s0 src2 >= 0 /\ (forall
    (va_x_dst:va_value_reg_opr) . let va_sM = va_upd_operand_reg_opr dst va_x_dst va_s0 in
    va_get_ok va_sM /\ va_eval_reg_opr va_sM dst == va_eval_reg_opr va_s0 src1 - va_eval_reg_opr
    va_s0 src2 ==> va_k va_sM (())))

val va_wpProof_Sub : dst:va_operand_reg_opr -> src1:va_operand_reg_opr -> src2:va_operand_reg_opr
  -> va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Sub dst src1 src2 va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Sub dst src1 src2) ([va_mod_reg_opr
    dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_Sub (dst:va_operand_reg_opr) (src1:va_operand_reg_opr) (src2:va_operand_reg_opr) :
  (va_quickCode unit (va_code_Sub dst src1 src2)) =
  (va_QProc (va_code_Sub dst src1 src2) ([va_mod_reg_opr dst]) (va_wp_Sub dst src1 src2)
    (va_wpProof_Sub dst src1 src2))
//--
//-- SubWrap

val va_code_SubWrap : dst:va_operand_reg_opr -> src1:va_operand_reg_opr -> src2:va_operand_reg_opr
  -> Tot va_code

val va_codegen_success_SubWrap : dst:va_operand_reg_opr -> src1:va_operand_reg_opr ->
  src2:va_operand_reg_opr -> Tot va_pbool

val va_lemma_SubWrap : va_b0:va_code -> va_s0:va_state -> dst:va_operand_reg_opr ->
  src1:va_operand_reg_opr -> src2:va_operand_reg_opr
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_SubWrap dst src1 src2) va_s0 /\ va_is_dst_reg_opr dst
    va_s0 /\ va_is_src_reg_opr src1 va_s0 /\ va_is_src_reg_opr src2 va_s0 /\ va_get_ok 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_reg_opr va_sM dst == Vale.Arch.Types.sub_wrap64 (va_eval_reg_opr va_s0 src1)
    (va_eval_reg_opr va_s0 src2) /\ va_state_eq va_sM (va_update_ok va_sM
    (va_update_operand_reg_opr dst va_sM va_s0))))
[@ va_qattr]
let va_wp_SubWrap (dst:va_operand_reg_opr) (src1:va_operand_reg_opr) (src2:va_operand_reg_opr)
  (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_is_dst_reg_opr dst va_s0 /\ va_is_src_reg_opr src1 va_s0 /\ va_is_src_reg_opr src2 va_s0 /\
    va_get_ok va_s0 /\ (forall (va_x_dst:va_value_reg_opr) . let va_sM = va_upd_operand_reg_opr dst
    va_x_dst va_s0 in va_get_ok va_sM /\ va_eval_reg_opr va_sM dst == Vale.Arch.Types.sub_wrap64
    (va_eval_reg_opr va_s0 src1) (va_eval_reg_opr va_s0 src2) ==> va_k va_sM (())))

val va_wpProof_SubWrap : dst:va_operand_reg_opr -> src1:va_operand_reg_opr ->
  src2:va_operand_reg_opr -> va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_SubWrap dst src1 src2 va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_SubWrap dst src1 src2)
    ([va_mod_reg_opr dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_SubWrap (dst:va_operand_reg_opr) (src1:va_operand_reg_opr) (src2:va_operand_reg_opr) :
  (va_quickCode unit (va_code_SubWrap dst src1 src2)) =
  (va_QProc (va_code_SubWrap dst src1 src2) ([va_mod_reg_opr dst]) (va_wp_SubWrap dst src1 src2)
    (va_wpProof_SubWrap dst src1 src2))
//--
//-- SubImm

val va_code_SubImm : dst:va_operand_reg_opr -> src1:va_operand_reg_opr -> src2:nsimm16 -> Tot
  va_code

val va_codegen_success_SubImm : dst:va_operand_reg_opr -> src1:va_operand_reg_opr -> src2:nsimm16
  -> Tot va_pbool

val va_lemma_SubImm : va_b0:va_code -> va_s0:va_state -> dst:va_operand_reg_opr ->
  src1:va_operand_reg_opr -> src2:nsimm16
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_SubImm dst src1 src2) va_s0 /\ va_is_dst_reg_opr dst
    va_s0 /\ va_is_src_reg_opr src1 va_s0 /\ va_get_ok va_s0 /\ va_eval_reg_opr va_s0 src1 -
    Vale.PPC64LE.Machine_s.int_to_nat64 src2 >= 0))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    va_eval_reg_opr va_sM dst == va_eval_reg_opr va_s0 src1 - Vale.PPC64LE.Machine_s.int_to_nat64
    src2 /\ va_state_eq va_sM (va_update_ok va_sM (va_update_operand_reg_opr dst va_sM va_s0))))
[@ va_qattr]
let va_wp_SubImm (dst:va_operand_reg_opr) (src1:va_operand_reg_opr) (src2:nsimm16) (va_s0:va_state)
  (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_is_dst_reg_opr dst va_s0 /\ va_is_src_reg_opr src1 va_s0 /\ va_get_ok va_s0 /\
    va_eval_reg_opr va_s0 src1 - Vale.PPC64LE.Machine_s.int_to_nat64 src2 >= 0 /\ (forall
    (va_x_dst:va_value_reg_opr) . let va_sM = va_upd_operand_reg_opr dst va_x_dst va_s0 in
    va_get_ok va_sM /\ va_eval_reg_opr va_sM dst == va_eval_reg_opr va_s0 src1 -
    Vale.PPC64LE.Machine_s.int_to_nat64 src2 ==> va_k va_sM (())))

val va_wpProof_SubImm : dst:va_operand_reg_opr -> src1:va_operand_reg_opr -> src2:nsimm16 ->
  va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_SubImm dst src1 src2 va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_SubImm dst src1 src2) ([va_mod_reg_opr
    dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_SubImm (dst:va_operand_reg_opr) (src1:va_operand_reg_opr) (src2:nsimm16) :
  (va_quickCode unit (va_code_SubImm dst src1 src2)) =
  (va_QProc (va_code_SubImm dst src1 src2) ([va_mod_reg_opr dst]) (va_wp_SubImm dst src1 src2)
    (va_wpProof_SubImm dst src1 src2))
//--
//-- SubImmWrap

val va_code_SubImmWrap : dst:va_operand_reg_opr -> src1:va_operand_reg_opr -> src2:nsimm16 -> Tot
  va_code

val va_codegen_success_SubImmWrap : dst:va_operand_reg_opr -> src1:va_operand_reg_opr ->
  src2:nsimm16 -> Tot va_pbool

val va_lemma_SubImmWrap : va_b0:va_code -> va_s0:va_state -> dst:va_operand_reg_opr ->
  src1:va_operand_reg_opr -> src2:nsimm16
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_SubImmWrap dst src1 src2) va_s0 /\ va_is_dst_reg_opr
    dst va_s0 /\ va_is_src_reg_opr src1 va_s0 /\ va_get_ok 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_reg_opr va_sM dst == Vale.Arch.Types.sub_wrap64 (va_eval_reg_opr va_s0 src1)
    (Vale.PPC64LE.Machine_s.int_to_nat64 src2) /\ va_state_eq va_sM (va_update_ok va_sM
    (va_update_operand_reg_opr dst va_sM va_s0))))
[@ va_qattr]
let va_wp_SubImmWrap (dst:va_operand_reg_opr) (src1:va_operand_reg_opr) (src2:nsimm16)
  (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_is_dst_reg_opr dst va_s0 /\ va_is_src_reg_opr src1 va_s0 /\ va_get_ok va_s0 /\ (forall
    (va_x_dst:va_value_reg_opr) . let va_sM = va_upd_operand_reg_opr dst va_x_dst va_s0 in
    va_get_ok va_sM /\ va_eval_reg_opr va_sM dst == Vale.Arch.Types.sub_wrap64 (va_eval_reg_opr
    va_s0 src1) (Vale.PPC64LE.Machine_s.int_to_nat64 src2) ==> va_k va_sM (())))

val va_wpProof_SubImmWrap : dst:va_operand_reg_opr -> src1:va_operand_reg_opr -> src2:nsimm16 ->
  va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_SubImmWrap dst src1 src2 va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_SubImmWrap dst src1 src2)
    ([va_mod_reg_opr dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_SubImmWrap (dst:va_operand_reg_opr) (src1:va_operand_reg_opr) (src2:nsimm16) :
  (va_quickCode unit (va_code_SubImmWrap dst src1 src2)) =
  (va_QProc (va_code_SubImmWrap dst src1 src2) ([va_mod_reg_opr dst]) (va_wp_SubImmWrap dst src1
    src2) (va_wpProof_SubImmWrap dst src1 src2))
//--
//-- MulLow64

val va_code_MulLow64 : dst:va_operand_reg_opr -> src1:va_operand_reg_opr -> src2:va_operand_reg_opr
  -> Tot va_code

val va_codegen_success_MulLow64 : dst:va_operand_reg_opr -> src1:va_operand_reg_opr ->
  src2:va_operand_reg_opr -> Tot va_pbool

val va_lemma_MulLow64 : va_b0:va_code -> va_s0:va_state -> dst:va_operand_reg_opr ->
  src1:va_operand_reg_opr -> src2:va_operand_reg_opr
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_MulLow64 dst src1 src2) va_s0 /\ va_is_dst_reg_opr dst
    va_s0 /\ va_is_src_reg_opr src1 va_s0 /\ va_is_src_reg_opr src2 va_s0 /\ va_get_ok va_s0 /\ (0
    <= va_mul_nat (va_eval_reg_opr va_s0 src1) (va_eval_reg_opr va_s0 src2) /\ va_mul_nat
    (va_eval_reg_opr va_s0 src1) (va_eval_reg_opr va_s0 src2) < pow2_64)))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    va_eval_reg_opr va_sM dst == va_mul_nat (va_eval_reg_opr va_s0 src1) (va_eval_reg_opr va_s0
    src2) /\ va_state_eq va_sM (va_update_ok va_sM (va_update_operand_reg_opr dst va_sM va_s0))))
[@ va_qattr]
let va_wp_MulLow64 (dst:va_operand_reg_opr) (src1:va_operand_reg_opr) (src2:va_operand_reg_opr)
  (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_is_dst_reg_opr dst va_s0 /\ va_is_src_reg_opr src1 va_s0 /\ va_is_src_reg_opr src2 va_s0 /\
    va_get_ok va_s0 /\ (0 <= va_mul_nat (va_eval_reg_opr va_s0 src1) (va_eval_reg_opr va_s0 src2)
    /\ va_mul_nat (va_eval_reg_opr va_s0 src1) (va_eval_reg_opr va_s0 src2) < pow2_64) /\ (forall
    (va_x_dst:va_value_reg_opr) . let va_sM = va_upd_operand_reg_opr dst va_x_dst va_s0 in
    va_get_ok va_sM /\ va_eval_reg_opr va_sM dst == va_mul_nat (va_eval_reg_opr va_s0 src1)
    (va_eval_reg_opr va_s0 src2) ==> va_k va_sM (())))

val va_wpProof_MulLow64 : dst:va_operand_reg_opr -> src1:va_operand_reg_opr ->
  src2:va_operand_reg_opr -> va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_MulLow64 dst src1 src2 va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_MulLow64 dst src1 src2)
    ([va_mod_reg_opr dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_MulLow64 (dst:va_operand_reg_opr) (src1:va_operand_reg_opr) (src2:va_operand_reg_opr)
  : (va_quickCode unit (va_code_MulLow64 dst src1 src2)) =
  (va_QProc (va_code_MulLow64 dst src1 src2) ([va_mod_reg_opr dst]) (va_wp_MulLow64 dst src1 src2)
    (va_wpProof_MulLow64 dst src1 src2))
//--
//-- MulLow64Wrap

val va_code_MulLow64Wrap : dst:va_operand_reg_opr -> src1:va_operand_reg_opr ->
  src2:va_operand_reg_opr -> Tot va_code

val va_codegen_success_MulLow64Wrap : dst:va_operand_reg_opr -> src1:va_operand_reg_opr ->
  src2:va_operand_reg_opr -> Tot va_pbool

val va_lemma_MulLow64Wrap : va_b0:va_code -> va_s0:va_state -> dst:va_operand_reg_opr ->
  src1:va_operand_reg_opr -> src2:va_operand_reg_opr
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_MulLow64Wrap dst src1 src2) va_s0 /\ va_is_dst_reg_opr
    dst va_s0 /\ va_is_src_reg_opr src1 va_s0 /\ va_is_src_reg_opr src2 va_s0 /\ va_get_ok 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_reg_opr va_sM dst == va_mul_nat (va_eval_reg_opr va_s0 src1) (va_eval_reg_opr va_s0
    src2) `op_Modulus` pow2_64 /\ va_state_eq va_sM (va_update_ok va_sM (va_update_operand_reg_opr
    dst va_sM va_s0))))
[@ va_qattr]
let va_wp_MulLow64Wrap (dst:va_operand_reg_opr) (src1:va_operand_reg_opr) (src2:va_operand_reg_opr)
  (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_is_dst_reg_opr dst va_s0 /\ va_is_src_reg_opr src1 va_s0 /\ va_is_src_reg_opr src2 va_s0 /\
    va_get_ok va_s0 /\ (forall (va_x_dst:va_value_reg_opr) . let va_sM = va_upd_operand_reg_opr dst
    va_x_dst va_s0 in va_get_ok va_sM /\ va_eval_reg_opr va_sM dst == va_mul_nat (va_eval_reg_opr
    va_s0 src1) (va_eval_reg_opr va_s0 src2) `op_Modulus` pow2_64 ==> va_k va_sM (())))

val va_wpProof_MulLow64Wrap : dst:va_operand_reg_opr -> src1:va_operand_reg_opr ->
  src2:va_operand_reg_opr -> va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_MulLow64Wrap dst src1 src2 va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_MulLow64Wrap dst src1 src2)
    ([va_mod_reg_opr dst]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_MulLow64Wrap (dst:va_operand_reg_opr) (src1:va_operand_reg_opr)
  (src2:va_operand_reg_opr) : (va_quickCode unit (va_code_MulLow64Wrap dst src1 src2)) =
  (va_QProc (va_code_MulLow64Wrap dst src1 src2) ([va_mod_reg_opr dst]) (va_wp_MulLow64Wrap dst
    src1 src2) (va_wpProof_MulLow64Wrap dst src1 src2))
//--
//-- MulHigh64U

val va_code_MulHigh64U : dst:va_operand_reg_opr -> src1:va_operand_reg_opr ->
  src2:va_operand_reg_opr -> Tot va_code

val va_codegen_success_MulHigh64U : dst:va_operand_reg_opr -> src1:va_operand_reg_opr ->
  src2:va_operand_reg_opr -> Tot va_pbool

val va_lemma_MulHigh64U : va_b0:va_code -> va_s0:va_state -> dst:va_operand_reg_opr ->
  src1:va_operand_reg_opr -> src2:va_operand_reg_opr
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_MulHigh64U dst src1 src2) va_s0 /\ va_is_dst_reg_opr
    dst va_s0 /\ va_is_src_reg_opr src1 va_s0 /\ va_is_src_reg_opr src2 va_s0 /\ va_get_ok 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_reg_opr va_sM dst == va_mul_nat (va_eval_reg_opr va_s0 src1) (va_eval_reg_opr va_s0
    src2) `op_Division` pow2_64 /\ va_state_eq va_sM (va_update_ok va_sM (va_update_operand_reg_opr
    dst va_sM va_s0))))
[@ va_qattr]
let va_wp_MulHigh64U (dst:va_operand_reg_opr) (src1:va_operand_reg_opr) (src2:va_operand_reg_opr)
val va_wp_MulHigh64U
      (dst src1 src2: va_operand_reg_opr)
      (va_s0: va_state)
      (va_k: (va_state -> unit -> Type0))
    : Type0

    dst: Vale.PPC64LE.Decls.va_operand_reg_opr ->
    src1: Vale.PPC64LE.Decls.va_operand_reg_opr ->
    src2: Vale.PPC64LE.Decls.va_operand_reg_opr ->
    va_s0: Vale.PPC64LE.Decls.va_state ->
    va_k: (_: Vale.PPC64LE.Decls.va_state -> _: Prims.unit -> Type0)
  -> Type0