val va_wp_Move (dst src: va_operand_reg_opr) (va_s0: va_state) (va_k: (va_state -> unit -> Type0))
    : Type0
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_wp_Move (dst src: va_operand_reg_opr) (va_s0: va_state) (va_k: (va_state -> unit -> Type0))
    : Type0
let va_wp_Move (dst 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 (()))
)
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 Vale.PPC64LE.Machine_s.nat64 Vale.PPC64LE.Decls.va_eval_reg_opr 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
val va_wp_Move (dst src: va_operand_reg_opr) (va_s0: va_state) (va_k: (va_state -> unit -> Type0))
    : Type0

    dst: Vale.PPC64LE.Decls.va_operand_reg_opr ->
    src: 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