val lemma_eq_instr_write_outputs
      (outs: list instr_out)
      (args: list instr_operand)
      (vs: instr_ret_t outs)
      (oprs: instr_operands_t outs args)
      (s1_orig s1 s2_orig s2: machine_state)
    : Lemma (requires state_eq_S true s1_orig s2_orig /\ state_eq_S true s1 s2)
      (ensures
        state_eq_S true
          (BS.instr_write_outputs outs args vs oprs s1_orig s1)
          (BS.instr_write_outputs outs args vs oprs s2_orig s2))
let rec lemma_eq_instr_write_outputs
    (outs:list instr_out) (args:list instr_operand)
    (vs:instr_ret_t outs) (oprs:instr_operands_t outs args) (s1_orig s1 s2_orig s2:machine_state)
  : Lemma
  (requires state_eq_S true s1_orig s2_orig /\ state_eq_S true s1 s2)
  (ensures
    state_eq_S true
      (BS.instr_write_outputs outs args vs oprs s1_orig s1)
      (BS.instr_write_outputs outs args vs oprs s2_orig s2))
  =
  let open BS in
  use_machine_state_equal ();
  lemma_heap_ignore_ghost_machine s1.BS.ms_heap s2.BS.ms_heap;
  lemma_heap_ignore_ghost_machine s1_orig.BS.ms_heap s2_orig.BS.ms_heap;
  allow_inversion tmaddr;
  match outs with
  | [] -> ()
  | (_, i)::outs ->
    (
      let ((v:instr_val_t i), (vs:instr_ret_t outs)) =
        match outs with
        | [] -> (vs, ())
        | _::_ -> let vs = coerce vs in (fst vs, snd vs)
      in
      match i with
      | IOpEx i ->
        let oprs = coerce oprs in
        let s1 = instr_write_output_explicit i v (fst oprs) s1_orig s1 in
        let s2 = instr_write_output_explicit i v (fst oprs) s2_orig s2 in
        lemma_eq_instr_write_outputs outs args vs (snd oprs) s1_orig s1 s2_orig s2
      | IOpIm i ->
        let s1 = instr_write_output_implicit i v s1_orig s1 in
        let s2 = instr_write_output_implicit i v s2_orig s2 in
        allow_inversion operand64;
        allow_inversion operand128;
        lemma_eq_instr_write_outputs outs args vs (coerce oprs) s1_orig s1 s2_orig s2
    )
val lemma_eq_instr_write_outputs
      (outs: list instr_out)
      (args: list instr_operand)
      (vs: instr_ret_t outs)
      (oprs: instr_operands_t outs args)
      (s1_orig s1 s2_orig s2: machine_state)
    : Lemma (requires state_eq_S true s1_orig s2_orig /\ state_eq_S true s1 s2)
      (ensures
        state_eq_S true
          (BS.instr_write_outputs outs args vs oprs s1_orig s1)
          (BS.instr_write_outputs outs args vs oprs s2_orig s2))
let rec lemma_eq_instr_write_outputs
      (outs: list instr_out)
      (args: list instr_operand)
      (vs: instr_ret_t outs)
      (oprs: instr_operands_t outs args)
      (s1_orig s1 s2_orig s2: machine_state)
    : Lemma (requires state_eq_S true s1_orig s2_orig /\ state_eq_S true s1 s2)
      (ensures
        state_eq_S true
          (BS.instr_write_outputs outs args vs oprs s1_orig s1)
          (BS.instr_write_outputs outs args vs oprs s2_orig s2)) =
let open BS in
use_machine_state_equal ();
lemma_heap_ignore_ghost_machine s1.BS.ms_heap s2.BS.ms_heap;
lemma_heap_ignore_ghost_machine s1_orig.BS.ms_heap s2_orig.BS.ms_heap;
allow_inversion tmaddr;
match outs with
| [] -> ()
| (_, i) :: outs ->
  (let (v: instr_val_t i), (vs: instr_ret_t outs) =
      match outs with
      | [] -> (vs, ())
      | _ :: _ ->
        let vs = coerce vs in
        (fst vs, snd vs)
    in
    match i with
    | IOpEx i ->
      let oprs = coerce oprs in
      let s1 = instr_write_output_explicit i v (fst oprs) s1_orig s1 in
      let s2 = instr_write_output_explicit i v (fst oprs) s2_orig s2 in
      lemma_eq_instr_write_outputs outs args vs (snd oprs) s1_orig s1 s2_orig s2
    | IOpIm i ->
      let s1 = instr_write_output_implicit i v s1_orig s1 in
      let s2 = instr_write_output_implicit i v s2_orig s2 in
      allow_inversion operand64;
      allow_inversion operand128;
      lemma_eq_instr_write_outputs outs args vs (coerce oprs) s1_orig s1 s2_orig s2)
Vale.X64.Lemmas.fst.checked
Vale.X64.StateLemmas.fsti.checked Vale.X64.State.fsti.checked Vale.X64.Memory.fsti.checked Vale.X64.Machine_Semantics_s.fst.checked Vale.X64.Machine_s.fst.checked Vale.X64.Instruction_s.fsti.checked Vale.X64.Flags.fsti.checked Vale.X64.Bytes_Code_s.fst.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.FunctionalExtensionality.fsti.checked
Vale.X64.Lemmas.fst
Prims.list Vale.X64.Instruction_s.instr_out Vale.X64.Instruction_s.instr_operand Vale.X64.Instruction_s.instr_ret_t Vale.X64.Instruction_s.instr_operands_t Vale.X64.StateLemmas.machine_state Vale.X64.Instruction_s.instr_operand_inout Vale.X64.Instruction_s.instr_val_t Vale.X64.Instruction_s.instr_operand_explicit Vale.X64.Lemmas.lemma_eq_instr_write_outputs FStar.Pervasives.Native.snd Vale.X64.Instruction_s.instr_operand_t Vale.X64.Machine_Semantics_s.machine_state Vale.X64.Machine_Semantics_s.instr_write_output_explicit FStar.Pervasives.Native.fst FStar.Pervasives.Native.tuple2 Vale.X64.Instruction_s.coerce Vale.X64.Instruction_s.instr_operand_implicit Prims.unit FStar.Pervasives.allow_inversion Vale.X64.Machine_s.operand128 Vale.X64.Machine_s.operand64 Vale.X64.Machine_Semantics_s.instr_write_output_implicit FStar.Pervasives.Native.Mktuple2 Vale.X64.Machine_s.tmaddr Vale.Arch.HeapLemmas.lemma_heap_ignore_ghost_machine Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_heap Vale.X64.StateLemmas.use_machine_state_equal Prims.l_and Vale.X64.Lemmas.state_eq_S Prims.squash Vale.X64.Machine_Semantics_s.instr_write_outputs Prims.Nil FStar.Pervasives.pattern
module Vale.X64.Lemmas
open FStar.Mul
open Vale.X64.Machine_s
open Vale.X64.State
open Vale.X64.StateLemmas
open Vale.X64.Instruction_s
open Vale.X64.Bytes_Code_s
module BS = Vale.X64.Machine_Semantics_s
module ME = Vale.X64.Memory

#reset-options "--initial_fuel 1 --max_fuel 1 --z3rlimit 100"

#restart-solver
let rec lemma_eq_instr_apply_eval_args
    (outs:list instr_out) (args:list instr_operand)
    (f:instr_args_t outs args) (oprs:instr_operands_t_args args) (s1 s2:machine_state)
  : Lemma
  (requires state_eq_S true s1 s2)
  (ensures
    BS.instr_apply_eval_args outs args f oprs s1 ==
    BS.instr_apply_eval_args outs args f oprs s2)
  =
  let open BS in
  lemma_heap_ignore_ghost_machine s1.BS.ms_heap s2.BS.ms_heap;
  match args with
  | [] -> ()
  | i::args ->
    (
      let (v, oprs) : option (instr_val_t i) & instr_operands_t_args args =
        match i with
        | IOpEx i -> let oprs = coerce oprs in (instr_eval_operand_explicit i (fst oprs) s1, snd oprs)
        | IOpIm i -> (instr_eval_operand_implicit i s1, coerce oprs)
        in
      let f:arrow (instr_val_t i) (instr_args_t outs args) = coerce f in
      match v with
        | None -> ()
        | Some v -> lemma_eq_instr_apply_eval_args outs args (f v) oprs s1 s2
    )

#restart-solver
let rec lemma_eq_instr_apply_eval_inouts
    (outs inouts:list instr_out) (args:list instr_operand)
    (f:instr_inouts_t outs inouts args) (oprs:instr_operands_t inouts args) (s1 s2:machine_state)
  : Lemma
  (requires state_eq_S true s1 s2)
  (ensures
    BS.instr_apply_eval_inouts outs inouts args f oprs s1 ==
    BS.instr_apply_eval_inouts outs inouts args f oprs s2)
  =
  let open BS in
  lemma_heap_ignore_ghost_machine s1.BS.ms_heap s2.BS.ms_heap;
  match inouts with
  | [] -> lemma_eq_instr_apply_eval_args outs args f oprs s1 s2
  | (Out, i)::inouts ->
    let oprs =
      match i with
      | IOpEx i -> snd #(instr_operand_t i) (coerce oprs)
      | IOpIm i -> coerce oprs
      in
    lemma_eq_instr_apply_eval_inouts outs inouts args (coerce f) oprs s1 s2
  | (InOut, i)::inouts ->
    (
      let (v, oprs) : option (instr_val_t i) & instr_operands_t inouts args =
        match i with
        | IOpEx i -> let oprs = coerce oprs in (instr_eval_operand_explicit i (fst oprs) s1, snd oprs)
        | IOpIm i -> (instr_eval_operand_implicit i s1, coerce oprs)
        in
      let f:arrow (instr_val_t i) (instr_inouts_t outs inouts args) = coerce f in
      match v with
      | None -> ()
      | Some v -> lemma_eq_instr_apply_eval_inouts outs inouts args (f v) oprs s1 s2
    )

#restart-solver
#push-options "--z3rlimit_factor 2"
let rec lemma_eq_instr_write_outputs
    (outs:list instr_out) (args:list instr_operand)
    (vs:instr_ret_t outs) (oprs:instr_operands_t outs args) (s1_orig s1 s2_orig s2:machine_state)
  : Lemma
  (requires state_eq_S true s1_orig s2_orig /\ state_eq_S true s1 s2)
  (ensures
    state_eq_S true
      (BS.instr_write_outputs outs args vs oprs s1_orig s1)
      (BS.instr_write_outputs outs args vs oprs s2_orig s2))
val lemma_eq_instr_write_outputs
      (outs: list instr_out)
      (args: list instr_operand)
      (vs: instr_ret_t outs)
      (oprs: instr_operands_t outs args)
      (s1_orig s1 s2_orig s2: machine_state)
    : Lemma (requires state_eq_S true s1_orig s2_orig /\ state_eq_S true s1 s2)
      (ensures
        state_eq_S true
          (BS.instr_write_outputs outs args vs oprs s1_orig s1)
          (BS.instr_write_outputs outs args vs oprs s2_orig s2))

    outs: Prims.list Vale.X64.Instruction_s.instr_out ->
    args: Prims.list Vale.X64.Instruction_s.instr_operand ->
    vs: Vale.X64.Instruction_s.instr_ret_t outs ->
    oprs: Vale.X64.Instruction_s.instr_operands_t outs args ->
    s1_orig: Vale.X64.StateLemmas.machine_state ->
    s1: Vale.X64.StateLemmas.machine_state ->
    s2_orig: Vale.X64.StateLemmas.machine_state ->
    s2: Vale.X64.StateLemmas.machine_state
  -> FStar.Pervasives.Lemma
      (requires
        Vale.X64.Lemmas.state_eq_S true s1_orig s2_orig /\ Vale.X64.Lemmas.state_eq_S true s1 s2)
      (ensures
        Vale.X64.Lemmas.state_eq_S true
          (Vale.X64.Machine_Semantics_s.instr_write_outputs outs args vs oprs s1_orig s1)
          (Vale.X64.Machine_Semantics_s.instr_write_outputs outs args vs oprs s2_orig s2))