val lemma_wrap_instructions (is: list ins) (fuel: nat) (s: machine_state)
    : Lemma (requires True)
      (ensures
        (equiv_option_states (machine_eval_codes (wrap_instructions is) fuel s)
            (Some (eval_inss is s))))
let rec lemma_wrap_instructions (is:list ins) (fuel:nat) (s:machine_state) :
  Lemma
    (requires True)
    (ensures (
        equiv_option_states
          (machine_eval_codes (wrap_instructions is) fuel s)
          (Some (eval_inss is s)))) =
  match is with
  | [] -> ()
  | i :: is' ->
    reveal_opaque (`%machine_eval_code_ins) machine_eval_code_ins;
    lemma_eval_ins_equiv_states i s ({s with ms_trace = []});
    let Some s1 = machine_eval_code (Ins i) fuel s in
    let s2 = machine_eval_ins i s in
    lemma_wrap_instructions is' fuel s2;
    lemma_eval_codes_equiv_states (wrap_instructions is') fuel s1 s2
val lemma_wrap_instructions (is: list ins) (fuel: nat) (s: machine_state)
    : Lemma (requires True)
      (ensures
        (equiv_option_states (machine_eval_codes (wrap_instructions is) fuel s)
            (Some (eval_inss is s))))
let rec lemma_wrap_instructions (is: list ins) (fuel: nat) (s: machine_state)
    : Lemma (requires True)
      (ensures
        (equiv_option_states (machine_eval_codes (wrap_instructions is) fuel s)
            (Some (eval_inss is s)))) =
match is with
| [] -> ()
| i :: is' ->
  reveal_opaque (`%machine_eval_code_ins) machine_eval_code_ins;
  lemma_eval_ins_equiv_states i s ({ s with ms_trace = [] });
  let Some s1 = machine_eval_code (Ins i) fuel s in
  let s2 = machine_eval_ins i s in
  lemma_wrap_instructions is' fuel s2;
  lemma_eval_codes_equiv_states (wrap_instructions is') fuel s1 s2
Vale.Transformers.PeepHole.fst.checked
Vale.X64.StateLemmas.fsti.checked Vale.X64.Print_s.fst.checked Vale.X64.Machine_Semantics_s.fst.checked Vale.X64.Machine_s.fst.checked Vale.X64.Lemmas.fsti.checked Vale.X64.Instructions_s.fsti.checked Vale.X64.Instruction_s.fsti.checked Vale.X64.InsLemmas.fsti.checked Vale.X64.Decls.fst.checked Vale.X64.Decls.fst.checked Vale.X64.Bytes_Code_s.fst.checked Vale.Transformers.InstructionReorder.fst.checked Vale.Transformers.Common.fsti.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
Vale.Transformers.PeepHole.fst
Prims.list Vale.X64.Machine_Semantics_s.ins Prims.nat Vale.X64.Machine_Semantics_s.machine_state Vale.Transformers.InstructionReorder.lemma_eval_codes_equiv_states Vale.Transformers.PeepHole.wrap_instructions Prims.unit Vale.Transformers.PeepHole.lemma_wrap_instructions Vale.X64.Machine_Semantics_s.machine_eval_ins FStar.Pervasives.Native.option Vale.X64.Machine_Semantics_s.machine_eval_code Vale.X64.Machine_s.Ins Vale.X64.Bytes_Code_s.instruction_t Vale.X64.Machine_Semantics_s.instr_annotation Vale.X64.Bytes_Code_s.ocmp Vale.Transformers.InstructionReorder.lemma_eval_ins_equiv_states Vale.X64.Machine_Semantics_s.Mkmachine_state Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_ok Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_flags Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_heap Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_stack Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_stackTaint Prims.Nil Vale.X64.Machine_s.observation FStar.Pervasives.reveal_opaque Vale.X64.Machine_Semantics_s.machine_eval_code_ins Prims.l_True Prims.squash Vale.Transformers.InstructionReorder.equiv_option_states Vale.X64.Machine_Semantics_s.machine_eval_codes FStar.Pervasives.Native.Some Vale.Transformers.PeepHole.eval_inss FStar.Pervasives.pattern
module Vale.Transformers.PeepHole

open Vale.X64.Decls
friend Vale.X64.Decls

open Vale.X64.Lemmas
open Vale.X64.StateLemmas
open Vale.Transformers.Common

open Vale.X64.Bytes_Code_s
open Vale.X64.Instruction_s
open Vale.X64.Instructions_s
open Vale.X64.Machine_Semantics_s
open Vale.X64.Machine_s
open Vale.X64.Print_s

module L = FStar.List.Tot

open Vale.Transformers.InstructionReorder // open so that we don't
                                          // need to redefine things
                                          // equivalence etc.

open Vale.X64.InsLemmas

/// Now for the framework portion. This uses the provided [peephole]
/// to produce a new transformer that is proven correct. We also
/// require a "input_hint" which specifies the size of data that
/// should be passed into the peephole function, in terms of number of
/// instructions. This allows us to make the transformer faster.

/// First off, some metrics for proving termination.

let rec num_ins_in_code (c:code) : nat =
  match c with
  | Ins _ -> 1
  | Block l -> num_ins_in_codes l
  | IfElse c t f -> num_ins_in_code t + num_ins_in_code f
  | While c b -> num_ins_in_code b

and num_ins_in_codes (c:codes) : nat =
  match c with
  | [] -> 0
  | h :: t -> num_ins_in_code h + num_ins_in_codes t

let rec lemma_num_ins_in_codes_append (c1 c2:codes) :
  Lemma
    (ensures (num_ins_in_codes (c1 `L.append` c2) == num_ins_in_codes c1 + num_ins_in_codes c2)) =
  match c1 with
  | [] -> ()
  | x :: xs -> lemma_num_ins_in_codes_append xs c2

/// Next, we want to be able to "pull off" some instructions from
/// given code, and if necessary, "wrap" them back into code.

let rec pull_instructions_from_codes (cs:codes) (num:pos) :
  Pure (option (list ins & codes))
    (requires (True))
    (ensures (function
         | None -> True
         | Some (_, cs') -> num_ins_in_codes cs' < num_ins_in_codes cs))
    (decreases %[num_blocks_in_codes cs; num]) =
  match cs with
  | [] -> None
  | c :: cs' ->
    match c with
    | Ins i -> if num = 1 then (
        assert_norm (num_ins_in_codes cs' < num_ins_in_codes cs); (* OBSERVE *)
        Some ([i], cs')
      ) else (
        match pull_instructions_from_codes cs' (num - 1) with
        | None -> None
        | Some (is2, cs'') ->
          Some (i :: is2, cs'')
      )
    | Block l ->
      lemma_num_ins_in_codes_append l cs';
      assert_norm (num_ins_in_codes l + num_ins_in_codes cs' == num_ins_in_codes cs);
      pull_instructions_from_codes (l `L.append` cs') num
    | IfElse _ _ _ -> None
    | While _ _ -> None

let rec wrap_instructions (is:list ins) : Tot codes =
  match is with
  | [] -> []
  | i :: is' -> Ins i :: wrap_instructions is'

/// Finally, the implementation that repeatedly finds a group of
/// instructions and tries to apply the peephole transformation to
/// them.

let rec apply_peephole_to_codes (p:peephole) (cs:codes) :
  Tot codes
    (decreases %[num_ins_in_codes cs; cs]) =
  match cs with
  | [] -> []
  | c :: cs' ->
    match pull_instructions_from_codes cs p.input_hint with
    | None -> c :: apply_peephole_to_codes p cs'
    | Some (is, cs'') ->
      match p.ph is with
      | None -> c :: apply_peephole_to_codes p cs'
      | Some is' ->
        Block (wrap_instructions is') ::
        apply_peephole_to_codes p cs''

let rec apply_peephole_to_code (p:peephole) (c:code) :
  Tot code
    (decreases %[num_ins_in_code c; c]) =
  match c with
  | Ins i -> (
      if p.input_hint = 1 then (
        match p.ph [i] with
        | None -> c
        | Some is -> Block (wrap_instructions is)
      ) else (
        c
      )
    )
  | Block l -> (
      let l' = apply_peephole_to_codes p l in
      Block l'
    )
  | IfElse c t f -> (
      let t' = apply_peephole_to_code p t in
      let f' = apply_peephole_to_code p f in
      IfElse c t' f'
    )
  | While c b -> (
      let b' = apply_peephole_to_code p b in
      While c b'
    )

/// And now, for the proofs!

let rec lemma_wrap_instructions (is:list ins) (fuel:nat) (s:machine_state) :
  Lemma
    (requires True)
    (ensures (
        equiv_option_states
          (machine_eval_codes (wrap_instructions is) fuel s)
val lemma_wrap_instructions (is: list ins) (fuel: nat) (s: machine_state)
    : Lemma (requires True)
      (ensures
        (equiv_option_states (machine_eval_codes (wrap_instructions is) fuel s)
            (Some (eval_inss is s))))

    is: Prims.list Vale.X64.Machine_Semantics_s.ins ->
    fuel: Prims.nat ->
    s: Vale.X64.Machine_Semantics_s.machine_state
  -> FStar.Pervasives.Lemma
    (ensures
      Vale.Transformers.InstructionReorder.equiv_option_states (Vale.X64.Machine_Semantics_s.machine_eval_codes
            (Vale.Transformers.PeepHole.wrap_instructions is)
            fuel
            s)
        (FStar.Pervasives.Native.Some (Vale.Transformers.PeepHole.eval_inss is s)))