val 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))
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
val 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))
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
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
Vale.X64.Machine_Semantics_s.codes Vale.X64.Bytes_Code_s.code_t Vale.X64.Machine_Semantics_s.instr_annotation Prims.list Vale.Transformers.PeepHole.lemma_num_ins_in_codes_append Prims.unit Prims.l_True Prims.squash Prims.eq2 Prims.int Vale.Transformers.PeepHole.num_ins_in_codes FStar.List.Tot.Base.append Prims.op_Addition Prims.Nil 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
val 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))
c1: Vale.X64.Machine_Semantics_s.codes -> c2: Vale.X64.Machine_Semantics_s.codes
  -> FStar.Pervasives.Lemma
    (ensures
      Vale.Transformers.PeepHole.num_ins_in_codes (c1 @ c2) ==
      Vale.Transformers.PeepHole.num_ins_in_codes c1 +
      Vale.Transformers.PeepHole.num_ins_in_codes c2)