val peephole_correct (p: pre_peephole) (is: list ins) (s: machine_state) : GTot Type0
let peephole_correct (p:pre_peephole) (is:list ins) (s:machine_state) : GTot Type0 =
  match p.ph is with
  | None -> True
  | Some is' ->
    let s1 = eval_inss is s in
    let s2 = eval_inss is' s in
    s1.ms_ok ==> equiv_states s1 s2
val peephole_correct (p: pre_peephole) (is: list ins) (s: machine_state) : GTot Type0
let peephole_correct (p: pre_peephole) (is: list ins) (s: machine_state) : GTot Type0 =
match p.ph is with
| None -> True
| Some is' ->
  let s1 = eval_inss is s in
  let s2 = eval_inss is' s in
  s1.ms_ok ==> equiv_states s1 s2
Vale.Transformers.PeepHole.fsti.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.fsti.checked Vale.X64.Bytes_Code_s.fst.checked Vale.Transformers.InstructionReorder.fst.checked Vale.Transformers.Common.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
Vale.Transformers.PeepHole.fsti
Vale.Transformers.PeepHole.pre_peephole Prims.list Vale.X64.Machine_Semantics_s.ins Vale.X64.Machine_Semantics_s.machine_state Vale.Transformers.PeepHole.__proj__Mkpre_peephole__item__ph Prims.l_True Prims.l_imp Prims.b2t Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_ok Vale.Transformers.InstructionReorder.equiv_states Vale.Transformers.PeepHole.eval_inss
(**

   This module defines a framework for peephole transformers. It needs
   to be instantiated with an actual pattern to generate a verified
   peephole transform. In particular, it needs to be provided a
   [peephole], and an [input_hint] to obtain a new transformer.

   A [peephole] is a function that converts a list of instructions
   into (optionally) another list of instructions.

   Usage:
     let foo = peephole_transform foo_ph
     let lemma_foo = lemma_peephole_transform foo_ph

*)
module Vale.Transformers.PeepHole

open Vale.Transformers.Common


open 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

/// Define what a peephole means, and what it means to be correct.

noeq
type pre_peephole = {
  ph: list ins -> Tot (option (list ins)); // The actual peephole transformer
  input_hint: pos; // The number of instructions it takes as input to transform
}

let rec eval_inss (is:list ins) (s:machine_state) : GTot machine_state =
  match is with
  | [] -> s
  | i :: is' -> eval_inss is' (machine_eval_ins i s)
val peephole_correct (p: pre_peephole) (is: list ins) (s: machine_state) : GTot Type0

    p: Vale.Transformers.PeepHole.pre_peephole ->
    is: Prims.list Vale.X64.Machine_Semantics_s.ins ->
    s: Vale.X64.Machine_Semantics_s.machine_state
  -> Prims.GTot Type0