val 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 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
    )
val 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 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)
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_args_t Vale.X64.Instruction_s.instr_operands_t_args Vale.X64.StateLemmas.machine_state FStar.Pervasives.Native.option Vale.X64.Instruction_s.instr_val_t Vale.X64.Lemmas.lemma_eq_instr_apply_eval_args Prims.unit Vale.X64.Instruction_s.arrow Vale.X64.Instruction_s.coerce FStar.Pervasives.Native.tuple2 Vale.X64.Instruction_s.instr_operand_explicit FStar.Pervasives.Native.Mktuple2 Vale.X64.Machine_Semantics_s.instr_eval_operand_explicit FStar.Pervasives.Native.fst Vale.X64.Instruction_s.instr_operand_t FStar.Pervasives.Native.snd Vale.X64.Instruction_s.instr_operand_implicit Vale.X64.Machine_Semantics_s.instr_eval_operand_implicit Vale.Arch.HeapLemmas.lemma_heap_ignore_ghost_machine Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_heap Vale.X64.Lemmas.state_eq_S Prims.squash Prims.eq2 Vale.X64.Instruction_s.instr_ret_t Vale.X64.Machine_Semantics_s.instr_apply_eval_args 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)
val 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
      )

    outs: Prims.list Vale.X64.Instruction_s.instr_out ->
    args: Prims.list Vale.X64.Instruction_s.instr_operand ->
    f: Vale.X64.Instruction_s.instr_args_t outs args ->
    oprs: Vale.X64.Instruction_s.instr_operands_t_args args ->
    s1: Vale.X64.StateLemmas.machine_state ->
    s2: Vale.X64.StateLemmas.machine_state
  -> FStar.Pervasives.Lemma (requires Vale.X64.Lemmas.state_eq_S true s1 s2)
      (ensures
        Vale.X64.Machine_Semantics_s.instr_apply_eval_args outs args f oprs s1 ==
        Vale.X64.Machine_Semantics_s.instr_apply_eval_args outs args f oprs s2)