Module RTLdefgenspec

Require Import Coqlib.
Require Import Errors.
Require Import Maps.
Require Import AST.
Require Import Events.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Op.
Require Import Registers.
Require Import Annotations.
Require Import RTL.
Require Import RTLdefgen.
Import Utf8.
Import ArithLib.
Import MoreRTL.


Section SPEC.

  Variable prog: program.
  Let ge := Genv.globalenv prog.
  Variable STK: ident.
  Let SIZE := Psucc STK.
  
  Definition regs_agree (j: meminj) (n: reg) (rs trs: regset) :=
    forall r, (Ple r n /\ Val.inject j rs#r trs#r) \/ (Plt n r /\ Val.lessdef rs#r trs#r).

  Lemma regs_agree_ple:
    forall j n rs trs args,
      (forall r, In r args -> Ple r n) ->
      regs_agree j n rs trs ->
      Val.inject_list j rs##args trs##args.

  Lemma regs_agree_inject_incr:
    forall j j' n rs trs,
      inject_incr j j' ->
      regs_agree j n rs trs ->
      regs_agree j' n rs trs.

  Lemma regs_agree_update:
    forall j n rs trs r v tv,
      Ple r n ->
      regs_agree j n rs trs ->
      Val.inject j v tv ->
      regs_agree j n (rs # r <- v) (trs # r <- tv).

  Inductive tr_local_regs kappa: RTL.function -> code -> node -> Int.int -> nat -> nat -> list reg -> list reg -> node -> list node -> Prop :=
  | tr_local_regs_S_divides:
      forall f c pc1 ofs depth n reg regs regs' pc2 pcs (Hdivides: ((align_chunk kappa) | (Int.unsigned ofs))),
        c!pc1 = Some (Iload (xH, nil) Mint32 (Aglobal SIZE Int.zero) nil (Psucc (Psucc reg)) (Psucc pc1)) ->
        c!(Psucc pc1) = Some (Iload (xH, nil) Mint32 (Abased STK (Int.repr (-4 * Z.of_nat depth))) ((Psucc (Psucc reg))::nil) (Psucc reg) (Psucc (Psucc pc1))) ->
        c!(Psucc (Psucc pc1)) = Some (Iop (if Int.eq_dec ofs Int.zero then Omove else Oaddimm ofs) ((Psucc reg)::nil) reg (Psucc (Psucc (Psucc pc1)))) ->
        tr_local_regs kappa f c (Psucc (Psucc (Psucc pc1))) (Int.add ofs Int.one) depth n regs regs' pc2 pcs ->
        Plt (max_reg_function f) reg ->
        ~ In reg (regs ++ regs') ->
        ~ In (Psucc reg) (regs ++ regs') ->
        ~ In (Psucc (Psucc reg)) (regs ++ regs') ->
        list_disjoint regs regs' ->
        tr_local_regs kappa f c pc1 ofs depth (S n) (reg::regs) ((Psucc reg)::(Psucc (Psucc reg))::regs') pc2 (pc1::(Psucc pc1)::(Psucc (Psucc pc1))::pcs)
  | tr_local_regs_S_not_divides:
      forall f c pc1 ofs depth n regs regs' pc2 pcs (Hnotdivides: ~ ((align_chunk kappa) | (Int.unsigned ofs))),
        tr_local_regs kappa f c pc1 (Int.add ofs Int.one) depth n regs regs' pc2 pcs ->
        tr_local_regs kappa f c pc1 ofs depth (S n) regs regs' pc2 pcs
  | tr_local_regs_O:
      forall f c pc ofs depth,
        tr_local_regs kappa f c pc ofs depth O nil nil pc nil.

  Inductive tr_local_regs': RTL.function -> code -> node -> nat -> Int.int -> Int.int -> (reg + (reg * reg)) -> list reg -> node -> list node -> Prop :=
  | tr_local_regs_eq:
      forall f c pc1 base bound depth r pc2,
        base = bound ->
        c!pc1 = Some (Iload (xH, nil) Mint32 (Aglobal SIZE Int.zero) nil (Psucc (Psucc r)) (Psucc pc1)) ->
        c!(Psucc pc1) = Some (Iload (xH, nil) Mint32 (Abased STK (Int.repr (-4 * Z.of_nat depth))) ((Psucc (Psucc r))::nil) (Psucc r) (Psucc (Psucc pc1))) ->
        c!(Psucc (Psucc pc1)) = Some (Iop (if Int.eq_dec base Int.zero then Omove else Oaddimm base) ((Psucc r)::nil) r pc2) ->
        pc2 = Pos.succ (Pos.succ (Pos.succ pc1)) →
        Plt (max_reg_function f) r ->
        tr_local_regs' f c pc1 depth base bound (inl r) ((Psucc r)::(Psucc (Psucc r))::nil) pc2 (pc1::(Psucc pc1)::(Psucc (Psucc pc1))::nil)
  | tr_local_regs_neq:
      forall f c pc1 base bound depth r pc2,
        base <> bound ->
        c!pc1 = Some (Iload (xH, nil) Mint32 (Aglobal SIZE Int.zero) nil (Psucc (Psucc (Psucc r))) (Psucc pc1)) ->
        c!(Psucc pc1) = Some (Iload (xH, nil) Mint32 (Abased STK (Int.repr (-4 * Z.of_nat depth))) ((Psucc (Psucc (Psucc r)))::nil) (Psucc (Psucc r)) (Psucc (Psucc pc1))) ->
        c!(Psucc (Psucc pc1)) = Some (Iop (if Int.eq_dec base Int.zero then Omove else Oaddimm base) ((Psucc (Psucc r))::nil) r (Psucc (Psucc (Psucc pc1)))) ->
        c!(Psucc (Psucc (Psucc pc1))) = Some (Iload (xH, nil) Mint32 (Aglobal SIZE Int.zero) nil (Psucc (Psucc (Psucc r))) (Psucc (Psucc (Psucc (Psucc pc1))))) ->
        c!(Psucc (Psucc (Psucc (Psucc pc1)))) = Some (Iload (xH, nil) Mint32 (Abased STK (Int.repr (-4 * Z.of_nat depth))) ((Psucc (Psucc (Psucc r)))::nil) (Psucc (Psucc r)) (Psucc (Psucc (Psucc (Psucc (Psucc pc1)))))) ->
        c!(Psucc (Psucc (Psucc (Psucc (Psucc pc1))))) = Some (Iop (if Int.eq_dec bound Int.zero then Omove else Oaddimm bound) ((Psucc (Psucc r))::nil) (Psucc r) pc2) ->
        pc2 = Pos.succ (Pos.succ (Pos.succ (Pos.succ (Pos.succ (Pos.succ pc1))))) →
        Plt (max_reg_function f) r ->
        tr_local_regs' f c pc1 depth base bound (inr (r, Psucc r)) ((Psucc (Psucc r))::(Psucc (Psucc (Psucc r)))::nil) pc2 (pc1::(Psucc pc1)::(Psucc (Psucc pc1))::(Psucc (Psucc (Psucc pc1)))::(Psucc (Psucc (Psucc (Psucc pc1))))::(Psucc (Psucc (Psucc (Psucc (Psucc pc1)))))::nil).

  Inductive tr_global_regs kappa: RTL.function -> code -> node -> ident -> Int.int -> nat -> list reg -> node -> list node -> Prop :=
  | tr_global_regs_S_divides:
      forall f c pc1 id ofs n reg regs pc2 pcs (Hdivides: ((align_chunk kappa) | (Int.unsigned ofs))),
        c!pc1 = Some (Iop (Oaddrsymbol id ofs) nil reg (Psucc pc1)) ->
        tr_global_regs kappa f c (Psucc pc1) id (Int.add ofs Int.one) n regs pc2 pcs ->
        Plt (max_reg_function f) reg ->
        ~ In reg regs ->
        tr_global_regs kappa f c pc1 id ofs (S n) (reg::regs) pc2 (pc1::pcs)
  | tr_global_regs_S_not_divides:
      forall f c pc1 id ofs n regs pc2 pcs (Hdivides: ~ ((align_chunk kappa) | (Int.unsigned ofs))),
        tr_global_regs kappa f c pc1 id (Int.add ofs Int.one) n regs pc2 pcs ->
        tr_global_regs kappa f c pc1 id ofs (S n) regs pc2 pcs
  | tr_global_regs_O:
      forall f c pc id ofs,
        tr_global_regs kappa f c pc id ofs O nil pc nil.

  Inductive tr_global_regs': RTL.function -> code -> node -> ident -> Int.int -> Int.int -> (reg + (reg * reg)) -> node -> list node -> Prop :=
  | tr_global_regs_eq:
      forall f c pc1 base bound id r pc2,
        base = bound ->
        c!pc1 = Some (Iop (Oaddrsymbol id base) nil r pc2) ->
        pc2 = Pos.succ pc1 →
        Plt (max_reg_function f) r ->
        tr_global_regs' f c pc1 id base bound (inl r) pc2 (pc1::nil)
  | tr_global_regs_neq:
      forall f c pc1 base bound id r pc2,
        base <> bound ->
        c!pc1 = Some (Iop (Oaddrsymbol id base) nil r (Psucc pc1)) ->
        c!(Psucc pc1) = Some (Iop (Oaddrsymbol id bound) nil (Psucc r) pc2) ->
        pc2 = Pos.succ (Pos.succ pc1) →
        Plt (max_reg_function f) r ->
        tr_global_regs' f c pc1 id base bound (inr (r, Psucc r)) pc2 (pc1::(Psucc pc1)::nil).

  Inductive tr_regs_annot kappa : RTL.function -> code -> node -> list ablock -> list reg -> list reg -> node -> list node -> Prop :=
  | tr_regs_annot_nil:
      forall f c pc,
        tr_regs_annot kappa f c pc nil nil nil pc nil
  | tr_regs_annot_local_cons:
      forall f c pc1 pc2 pc3 depth varname base bound alpha regs1 regs1' regs2 regs2' pcs1 pcs2,
        tr_regs_annot kappa f c pc2 alpha regs2 regs2' pc3 pcs2 ->
        tr_local_regs kappa f c pc1 base depth (Z.to_nat (Int.unsigned (Int.sub bound base) + 1)) regs1 regs1' pc2 pcs1 ->
        list_disjoint regs1 regs2 ->
        list_disjoint regs1' regs2' ->
        list_disjoint regs1 regs2' ->
        list_disjoint regs1' regs2 ->
        list_disjoint regs2 regs2' ->
        tr_regs_annot kappa f c pc1 ((ABlocal depth varname (base, bound))::alpha) (regs1 ++ regs2) (regs1' ++ regs2') pc3 (pcs1 ++ pcs2)
  | tr_regs_annot_global_cons:
      forall f c pc1 pc2 pc3 id b base bound alpha regs1 regs2 regs2' pcs1 pcs2,
        Genv.find_symbol ge b = Some id ->
        tr_regs_annot kappa f c pc2 alpha regs2 regs2' pc3 pcs2 ->
        tr_global_regs kappa f c pc1 b base (Z.to_nat (Int.unsigned (Int.sub bound base) + 1)) regs1 pc2 pcs1 ->
        list_disjoint regs1 regs2 ->
        list_disjoint regs1 regs2' ->
        list_disjoint regs2 regs2' ->
        tr_regs_annot kappa f c pc1 ((ABglobal b (base, bound))::alpha) (regs1 ++ regs2) regs2' pc3 (pcs1 ++ pcs2).

  Inductive tr_regs_annot': RTL.function -> code -> node -> list ablock -> list (reg + (reg * reg)) -> list reg -> node -> list node -> Prop :=
  | tr_regs_annot_nil':
      forall f c pc,
      tr_regs_annot' f c pc nil nil nil pc nil
  | tr_regs_annot_local_cons':
      forall f c pc1 pc2 pc3 depth varname base bound alpha regs1 regs1' regs2 regs2' pcs1 pcs2,
        tr_regs_annot' f c pc2 alpha regs2 regs2' pc3 pcs2 ->
        tr_local_regs' f c pc1 depth base bound regs1 regs1' pc2 pcs1 ->
        list_norepet (fold_right (fun x acc => match x with inl r => r::acc | inr (r, r') => r::r'::acc end) nil (regs1::regs2)) ->
        list_disjoint regs1' regs2' ->
        list_disjoint (match regs1 with |inl r => r ::nil | inr (r, r') => r::r'::nil end) regs2' ->
        list_disjoint regs1' (fold_right (fun x acc => match x with inl r => r::acc | inr (r, r') => r::r'::acc end) nil regs2) ->
        list_disjoint (fold_right (fun x acc => match x with inl r => r::acc | inr (r, r') => r::r'::acc end) nil regs2) regs2' ->
        tr_regs_annot' f c pc1 ((ABlocal depth varname (base, bound))::alpha) (regs1::regs2) (regs1' ++ regs2') pc3 (pcs1 ++ pcs2)
  | tr_regs_annot_global_cons':
      forall f c pc1 pc2 pc3 b id base bound alpha regs1 regs2 regs2' pcs1 pcs2,
        Genv.find_symbol ge id = Some b ->
        tr_regs_annot' f c pc2 alpha regs2 regs2' pc3 pcs2 ->
        tr_global_regs' f c pc1 id base bound regs1 pc2 pcs1 ->
        list_norepet (fold_right (fun x acc => match x with inl r => r::acc | inr (r, r') => r::r'::acc end) nil (regs1::regs2)) ->
        list_disjoint (match regs1 with |inl r => r ::nil | inr (r, r') => r::r'::nil end) regs2' ->
        list_disjoint (fold_right (fun x acc => match x with inl r => r::acc | inr (r, r') => r::r'::acc end) nil regs2) regs2' ->
        tr_regs_annot' f c pc1 ((ABglobal id (base, bound))::alpha) (regs1::regs2) regs2' pc3 (pcs1 ++ pcs2).

  Inductive tr_cmp_regs: code -> node -> reg -> list reg -> node -> list node -> Prop :=
  | tr_comp_regs_nil:
      forall c pc reg0,
        tr_cmp_regs c pc reg0 nil pc nil
  | tr_comp_regs_cons:
      forall c pc1 pc2 reg0 reg1 regs pcs,
        c!pc1 = Some (Iop (Ocmp (Ccompu Ceq)) (reg0::reg1::nil) reg1 (Psucc pc1)) ->
        tr_cmp_regs c (Psucc pc1) reg0 regs pc2 pcs ->
        tr_cmp_regs c pc1 reg0 (reg1::regs) pc2 (pc1::pcs).

  Inductive tr_cmp_regs': code -> node -> reg -> list (reg + (reg * reg))-> node -> list node -> Prop :=
  | tr_comp_regs_nil':
      forall c pc reg0,
        tr_cmp_regs' c pc reg0 nil pc nil
  | tr_comp_regs_cons1':
      forall c pc1 pc2 reg0 reg1 regs pcs,
        c!pc1 = Some (Iop (Ocmp (Ccompu Ceq)) (reg1::reg0::nil) reg1 (Psucc pc1)) ->
        tr_cmp_regs' c (Psucc pc1) reg0 regs pc2 pcs ->
        tr_cmp_regs' c pc1 reg0 ((inl reg1)::regs) pc2 (pc1::pcs)
  | tr_comp_regs_cons2':
      forall c pc1 pc2 reg0 reg1 reg2 regs pcs,
        c!pc1 = Some (Iop (Ocmp (Ccompu Cle)) (reg1::reg0::nil) reg1 (Psucc pc1)) ->
        c!(Psucc pc1) = Some (Iop (Ocmp (Ccompu Cle)) (reg0::reg2::nil) reg2 (Psucc (Psucc pc1))) ->
        c!(Psucc (Psucc pc1)) = Some (Iop Oand (reg1::reg2::nil) reg1 (Psucc (Psucc (Psucc pc1)))) ->
        tr_cmp_regs' c (Psucc (Psucc (Psucc pc1))) reg0 regs pc2 pcs ->
        tr_cmp_regs' c pc1 reg0 ((inr (reg1, reg2))::regs) pc2 (pc1 :: Pos.succ pc1 :: Pos.succ (Pos.succ pc1) :: pcs).

  Inductive tr_or_regs: code -> node -> reg -> list reg -> node -> list node -> Prop :=
  | tr_or_regs_nil:
      forall c pc reg0,
        tr_or_regs c pc reg0 nil pc nil
  | tr_or_regs_cons:
      forall c pc1 pc2 reg0 reg1 regs pcs,
        c!pc1 = Some (Iop Oor (reg0::reg1::nil) reg0 (Psucc pc1)) ->
        tr_or_regs c (Psucc pc1) reg0 regs pc2 pcs ->
        tr_or_regs c pc1 reg0 (reg1::regs) pc2 (pc1::pcs).

  Inductive tr_return_undef: code -> node -> ident -> list node -> Prop :=
  | tr_return_undef_intro:
      forall c pc n reg0 reg1 reg,
        c!pc = Some (Iop (Ointconst Int.zero) nil reg0 (Psucc pc)) ->
        c!(Psucc pc) = Some (Iop (Ointconst (Int.repr (Zpos n))) nil reg1 (Psucc (Psucc pc))) ->
        c!(Psucc (Psucc pc)) = Some (Iop Odiv (reg1::reg0::nil) reg (Psucc (Psucc (Psucc pc)))) ->
        reg0 <> reg1 ->
        tr_return_undef c pc n (pc::(Psucc pc)::(Psucc (Psucc pc))::nil).

  Inductive tr_checks: RTL.function -> code -> node -> (annotation -> memory_chunk -> addressing -> list reg -> instruction) -> annotation -> memory_chunk -> addressing -> list reg -> list node -> Prop :=
  | tr_checks_intro:
      forall f c pc1 i alpha kappa addr args reg0 reg1 regs regs' regs2 pc3 pc4 pc5 pcs1 pcs2 pcs3 pcs4,
        c!pc1 = Some (Iop (match addr with | Aindexed n => if Int.eq_dec n Int.zero then Omove else Olea addr | _ => Olea addr end) args reg0 (Psucc pc1)) ->
        tr_regs_annot kappa f c (Psucc pc1) (snd alpha) regs regs2 pc3 pcs1->
        tr_cmp_regs c pc3 reg0 regs pc4 pcs2 ->
        regs = reg1::regs' ->
        c!pc4 = Some (Iop Omove (reg1::nil) reg0 (Psucc pc4)) ->
        tr_or_regs c (Psucc pc4) reg0 regs' pc5 pcs3 ->
        c!pc5 = Some (Icond (Ccompuimm Cne Int.zero) (reg0::nil) (Psucc pc5) (Psucc (Psucc pc5))) ->
        c!(Psucc pc5) = Some (i alpha kappa addr args) ->
        tr_return_undef c (Psucc (Psucc pc5)) (fst alpha) pcs4 ->
        Plt (max_reg_function f) reg0 ->
        ~ In reg0 regs ->
        ~ In reg0 regs2 ->
        tr_checks f c pc1 i alpha kappa addr args (pc1::pc4::pc5::(Psucc pc5)::(pcs1++pcs2++pcs3++pcs4)).

  Inductive tr_checks': RTL.function -> code -> node -> (annotation -> memory_chunk -> addressing -> list reg -> instruction) -> annotation -> memory_chunk -> addressing -> list reg -> list node -> Prop :=
  | tr_checks_intro':
      forall f c pc1 i alpha kappa addr args reg0 reg1 regs regs' regs2 pc3 pc4 pc5 pcs1 pcs2 pcs3 pcs4,
        c!pc1 = Some (Iop (match addr with | Aindexed n => if Int.eq_dec n Int.zero then Omove else Olea addr | _ => Olea addr end) args reg0 (Psucc pc1)) ->
        tr_regs_annot' f c (Psucc pc1) (snd alpha) regs regs2 pc3 pcs1->
        tr_cmp_regs' c pc3 reg0 regs pc4 pcs2 ->
        map (fun x => match x with | inl r => r | inr r => fst r end) regs = reg1::regs' ->
        c!pc4 = Some (Iop Omove (reg1::nil) reg0 (Psucc pc4)) ->
        tr_or_regs c (Psucc pc4) reg0 regs' pc5 pcs3 ->
        c!pc5 = Some (Icond (Ccompuimm Cne Int.zero) (reg0::nil) (Psucc pc5) (Psucc (Psucc pc5))) ->
        c!(Psucc pc5) = Some (i alpha kappa addr args) ->
        tr_return_undef c (Psucc (Psucc pc5)) (fst alpha) pcs4 ->
        Plt (max_reg_function f) reg0 ->
        ~ In reg0 (fold_right (fun x acc => match x with | inl r => r::acc | inr (r, r') => r::r'::acc end) nil regs) ->
        ~ In reg0 regs2 ->
        tr_checks' f c pc1 i alpha kappa addr args (pc1::pc4::pc5::(Psucc pc5)::(pcs1++pcs2++pcs3++pcs4)).

  Inductive tr_epilogue: RTL.function -> code -> node -> instruction -> list node -> Prop :=
  | tr_epilogue_intro:
      forall f c pc1 r r' i,
        c!pc1 = Some (Iload (xH, nil) Mint32 (Aglobal SIZE Int.zero) nil r (Psucc pc1)) ->
        c!(Psucc pc1) = Some (Iop (Ointconst (Int.repr 4)) nil r' (Psucc (Psucc pc1))) ->
        c!(Psucc (Psucc pc1)) = Some (Iop Osub (r::r'::nil) r (Psucc (Psucc (Psucc pc1)))) ->
        c!(Psucc (Psucc (Psucc pc1))) = Some (Istore (xH, nil) Mint32 (Aglobal SIZE Int.zero) nil r (Psucc (Psucc (Psucc (Psucc pc1))))) ->
        c!(Psucc (Psucc (Psucc (Psucc pc1)))) = Some i ->
        r <> r' ->
        Plt (max_reg_function f) r ->
        Plt (max_reg_function f) r' ->
        tr_epilogue f c pc1 i (pc1::(Psucc pc1)::(Psucc (Psucc pc1))::(Psucc (Psucc (Psucc pc1)))::(Psucc (Psucc (Psucc (Psucc pc1))))::nil).

  Fixpoint int_ranges (n: nat) (ofs: int) :=
    match n with
    | O => nil
    | S n => (Int.unsigned ofs)::(int_ranges n (Int.add ofs Int.one))
    end.
  
  Inductive tr_instrs: RTL.function -> node -> instruction -> code -> list node -> Prop :=
  | tr_Inop:
      forall f pc s c,
        c!pc = Some (Inop s) ->
        tr_instrs f pc (Inop s) c (pc::nil)
  | tr_Iop:
      forall f pc op args dst s c,
        c!pc = Some (Iop op args dst s) ->
        tr_instrs f pc (Iop op args dst s) c (pc::nil)
  | tr_Iload:
      forall f pc alpha kappa addr args dst s c pc1 pcs
        (Hlocrange: forall depth varname base bound, In (ABlocal depth varname (base, bound)) (snd alpha) ->
                                     Int.unsigned base <= Int.unsigned bound < Int.modulus - 1)
        (Hglobrange: forall id base bound, In (ABglobal id (base, bound)) (snd alpha) -> Int.unsigned base <= Int.unsigned bound < Int.modulus - 1)
        (Hdivides: check_annotations_divides kappa (snd alpha) = OK tt),
        c!pc = Some (Inop pc1) ->
        (if is_trivial_annotation prog alpha kappa addr then
           c!pc1 = Some (Iload alpha kappa addr args dst s)
         else if is_singleton (snd alpha) then
                tr_checks' f c pc1 (fun α κ addr args => Iload α κ addr args dst s) alpha kappa addr args pcs
              else tr_checks f c pc1 (fun α κ addr args => Iload α κ addr args dst s) alpha kappa addr args pcs) ->
        (forall depth varname range, In (ABlocal depth varname range) (snd alpha) -> (depth < 128)%nat) ->
        (forall id range, In (ABglobal id range) (snd alpha) -> (id <> STK /\ id <> SIZE)) ->
        (forall depth varname base bound, In (ABlocal depth varname (base, bound)) (snd alpha) ->
                                     forall size, Int.unsigned (Int.sub bound base) + 1 = Z.pos size ->
                                             exists x, In x (int_ranges (Pos.to_nat size) base) /\ ((align_chunk kappa) | x)) ->
        tr_instrs f pc (Iload alpha kappa addr args dst s) c (if is_trivial_annotation prog alpha kappa addr then pc::pc1::nil else pc::pcs)
  | tr_Istore:
      forall f pc alpha kappa addr args src s c pc1 pcs
        (Hlocrange: forall depth varname base bound, In (ABlocal depth varname (base, bound)) (snd alpha) ->
                                     Int.unsigned base <= Int.unsigned bound < Int.modulus - 1)
        (Hglobrange: forall id base bound, In (ABglobal id (base, bound)) (snd alpha) -> Int.unsigned base <= Int.unsigned bound < Int.modulus - 1)
        (Hdivides: check_annotations_divides kappa (snd alpha) = OK tt),
        c!pc = Some (Inop pc1) ->
        (if is_trivial_annotation prog alpha kappa addr then
           c!pc1 = Some (Istore alpha kappa addr args src s)
         else if is_singleton (snd alpha) then
                tr_checks' f c pc1 (fun α κ addr args => Istore α κ addr args src s) alpha kappa addr args pcs
              else tr_checks f c pc1 (fun α κ addr args => Istore α κ addr args src s) alpha kappa addr args pcs) ->
        (forall depth varname range, In (ABlocal depth varname range) (snd alpha) -> (depth < 128)%nat) ->
        (forall id range, In (ABglobal id range) (snd alpha) -> (id <> STK /\ id <> SIZE)) ->
        (forall depth varname base bound, In (ABlocal depth varname (base, bound)) (snd alpha) ->
                                     forall size, Int.unsigned (Int.sub bound base) + 1 = Z.pos size ->
                                             exists x, In x (int_ranges (Pos.to_nat size) base) /\ ((align_chunk kappa) | x)) ->
        tr_instrs f pc (Istore alpha kappa addr args src s) c (if is_trivial_annotation prog alpha kappa addr then pc::pc1::nil else pc::pcs)
  | tr_Icall:
      forall f pc sig fn args dst s c,
        c!pc = Some (Icall sig fn args dst s) ->
        tr_instrs f pc (Icall sig fn args dst s) c (pc::nil)
  | tr_Itailcall:
      forall f pc sig fn args c pc1 pcs,
        c!pc = Some (Inop pc1) ->
        tr_epilogue f c pc1 (Itailcall sig fn args) pcs ->
        tr_instrs f pc (Itailcall sig fn args) c (pc::pcs)
  | tr_Ibuiltin:
      forall f pc ef args dst s c,
        c!pc = Some (Ibuiltin ef args dst s) ->
        ~ In STK (globals_of_builtin_args args) ->
        ~ In SIZE (globals_of_builtin_args args) ->
        tr_instrs f pc (Ibuiltin ef args dst s) c (pc::nil)
  | tr_Icond:
      forall f pc cond args ifso ifnot c,
        c!pc = Some (Icond cond args ifso ifnot) ->
        tr_instrs f pc (Icond cond args ifso ifnot) c (pc::nil)
  | tr_Ijumptable:
      forall f pc arg tbl c,
        c!pc = Some (Ijumptable arg tbl) ->
        tr_instrs f pc (Ijumptable arg tbl) c (pc::nil)
  | tr_Ireturn:
      forall f pc r c pc1 pcs,
        c!pc = Some (Inop pc1) ->
        tr_epilogue f c pc1 (Ireturn r) pcs ->
        tr_instrs f pc (Ireturn r) c (pc::pcs).

  Inductive sincr (s1 s2: state): Prop :=
  | sincr_intro:
      forall (NEXTREG: Ple s1.(st_nextreg) s2.(st_nextreg))
        (NEXTNODE: Ple s1.(st_nextnode) s2.(st_nextnode)),
        sincr s1 s2.

  Lemma sincr_refl:
    forall s, sincr s s.
  
  Lemma sincr_transitive:
    forall s1 s2 s3,
      sincr s1 s2 ->
      sincr s2 s3 ->
      sincr s1 s3.

  Definition unchanged s s' : Prop :=
      forall pc,
        Plt pc s.(st_nextnode) ->
        s.(st_code)!pc = s'.(st_code)!pc.

  Lemma unchanged_refl {s} : unchanged s s.

  Lemma unchanged_and_sincr_refl {s} : unchanged s s ∧ sincr s s.

  Lemma sincr_nextnode x y : sincr x y → (st_nextnode x <= st_nextnode y)%positive.

  Lemma unchanged_trans x y z : unchanged y z → unchanged x y → sincr x y → unchanged x z.

  Lemma unchanged_and_sincr_trans x y z :
    unchanged y z ∧ sincr y z →
    unchanged x y ∧ sincr x y →
    unchanged x z ∧ sincr x z.

  Lemma add_instr_sincr:
    forall i s s',
      add_instr i s = s' ->
      sincr s s'.

  Lemma add_instr_unchanged:
    forall i s s',
      add_instr i s = s' ->
      forall pc,
        Plt pc s.(st_nextnode) ->
        s.(st_code)!pc = s'.(st_code)!pc.

  Lemma add_instr_unchanged_and_sincr :
    ∀ {i s},
      unchanged s (add_instr i s) ∧ sincr s (add_instr i s).

  Lemma make_zero_for_type_unchanged_and_sincr {ty r s} :
    unchanged s (make_zero_for_type ty r s) ∧ sincr s (make_zero_for_type ty r s).
    
  Lemma new_reg_unchanged_and_sincr :
    ∀ {s r s'},
      new_reg s = (r, s') →
      unchanged s s' ∧ sincr s s'.

  Lemma add_return_undef_unchanged_and_sincr :
    ∀ {t x s},
      unchanged s (add_return_undef t x s) ∧ sincr s (add_return_undef t x s).

  Lemma put_stack_range_in_regs_unchanged_and_sincr:
    forall {kappa n ofs depth s regs s'},
      put_stack_range_in_regs STK SIZE kappa ofs depth n s = OK (regs, s') ->
      unchanged s s' ∧ sincr s s'.

  Lemma put_symbol_range_in_regs_unchanged_and_sincr:
    ∀ {kappa n id ofs s regs s'},
      put_symbol_range_in_regs kappa id ofs n s = OK (regs, s') ->
      unchanged s s' ∧ sincr s s'.

  Lemma put_all_in_regs_unchanged_and_sincr:
    forall kappa alpha s regs s',
      put_all_in_regs ge STK SIZE kappa alpha s = OK (regs, s') ->
      unchanged s s' ∧ sincr s s'.

  Lemma put_checks_unchanged_and_sincr {r rs s s'} :
      put_checks r rs s = OK s' →
      unchanged s s' ∧ sincr s s'.

  Corollary put_checks_sincr r rs s s' :
      put_checks r rs s = OK s' →
      sincr s s'.

  Lemma put_ors_sincr:
    forall reg0 regs s s',
      put_ors reg0 regs s = OK s' ->
      sincr s s'.

  Lemma put_ors_unchanged:
    forall reg0 regs s s',
      put_ors reg0 regs s = OK s' ->
      forall pc,
        Plt pc s.(st_nextnode) ->
        s.(st_code)!pc = s'.(st_code)!pc.

  Lemma put_ors_unchanged_and_sincr :
    ∀ {r rs s s'},
      put_ors r rs s = OK s' →
      unchanged s s' ∧ sincr s s'.

  Lemma put_stack_range_in_regs'_unchanged_and_sincr :
    ∀ {base bound δ s out s'},
      put_stack_range_in_regs' STK SIZE base bound δ s = OK (out, s') →
      unchanged s s' ∧ sincr s s'.

  Lemma put_symbol_range_in_regs'_unchanged_and_sincr :
    ∀ {b base bound s out s'},
      put_symbol_range_in_regs' b base bound s = OK (out, s') →
      unchanged s s' ∧ sincr s s'.

  Lemma put_all_in_regs'_unchanged_and_sincr :
    ∀ {α s out s'},
      put_all_in_regs' ge STK SIZE α s = OK (out, s') →
      unchanged s s' ∧ sincr s s'.

  Lemma put_checks'_unchanged_and_sincr :
    ∀ {r rs s s'} ,
      put_checks' r rs s = OK s' →
      unchanged s s' ∧ sincr s s'.

  Lemma add_checks_unchanged_and_sincr :
    ∀ {opt i α ϰ addr args s s'},
      add_checks prog ge STK SIZE opt i α ϰ addr args s = OK s' →
      unchanged s s' ∧ sincr s s'.

  Lemma add_checks_unchanged:
    forall opt i alpha kappa addr args s s',
      add_checks prog ge STK SIZE opt i alpha kappa addr args s = OK s' ->
      forall pc,
        Plt pc s.(st_nextnode) ->
        s.(st_code)!pc = s'.(st_code)!pc.

  Lemma put_stack_range_in_regs_regs_spec:
    forall kappa n ofs depth s regs s',
      put_stack_range_in_regs STK SIZE kappa ofs depth n s = OK (regs, s') ->
      forall r, In r regs -> Ple (st_nextreg s) r /\ Plt r (st_nextreg s').

  Lemma not_in_cons:
    forall (A: Type) (x a: A) (l: list A),
      ~ In x (a::l) <-> x <> a /\ ~ In x l.

  Lemma not_in_app:
    forall (A: Type) (x: A) (l1 l2: list A),
      ~ In x (l1 ++ l2) <-> ~ In x l1 /\ ~ In x l2.

  Lemma tr_local_regs_is_disjoint:
    forall kappa f c pc1 ofs depth n regs regs' pc2 pcs,
      tr_local_regs kappa f c pc1 ofs depth n regs regs' pc2 pcs ->
      list_disjoint regs regs'.

  Lemma put_stack_range_in_regs_spec':
    forall kappa f n ofs depth s regs s',
      put_stack_range_in_regs STK SIZE kappa ofs depth n s = OK (regs, s') ->
      Plt (max_reg_function f) s.(st_nextreg) ->
      exists regs' pcs, tr_local_regs kappa f s'.(st_code) s.(st_nextnode) ofs depth n regs regs' s'.(st_nextnode) pcs
                   /\ forall r, In r regs' -> Plt s.(st_nextreg) r /\ Plt r s'.(st_nextreg).

  Lemma put_stack_range_in_regs_spec:
    forall kappa f n ofs depth s regs s',
      put_stack_range_in_regs STK SIZE kappa ofs depth n s = OK (regs, s') ->
      Plt (max_reg_function f) s.(st_nextreg) ->
      exists regs' pcs, tr_local_regs kappa f s'.(st_code) s.(st_nextnode) ofs depth n regs regs' s'.(st_nextnode) pcs.

  Lemma put_symbol_range_in_regs_regs_spec:
    forall kappa n id ofs s regs s',
      put_symbol_range_in_regs kappa id ofs n s = OK (regs, s') ->
      forall r, In r regs -> Ple (st_nextreg s) r /\ Plt r (st_nextreg s').

  Lemma put_symbol_range_in_regs_spec:
    forall kappa f n id ofs s regs s',
      put_symbol_range_in_regs kappa id ofs n s = OK (regs, s') ->
      Plt (max_reg_function f) s.(st_nextreg) ->
      exists pcs, tr_global_regs kappa f s'.(st_code) s.(st_nextnode) id ofs n regs s'.(st_nextnode) pcs.

  Lemma tr_local_regs_incr:
    forall kappa f c n pc1 ofs depth regs regs' pc2 pcs,
      tr_local_regs kappa f c pc1 ofs depth n regs regs' pc2 pcs ->
      Ple pc1 pc2.

  Lemma tr_local_regs_unchanged:
    forall kappa f c c' n pc1 ofs depth regs regs' pc2 pcs,
      (forall pc, Plt pc pc2 ->
             c!pc = c'!pc) ->
      tr_local_regs kappa f c pc1 ofs depth n regs regs' pc2 pcs ->
      tr_local_regs kappa f c' pc1 ofs depth n regs regs' pc2 pcs.

  Lemma tr_global_regs_incr:
    forall kappa f c id n pc1 ofs regs pc2 pcs,
      tr_global_regs kappa f c pc1 id ofs n regs pc2 pcs ->
      Ple pc1 pc2.

  Lemma tr_global_regs_unchanged:
    forall kappa f c c' id n pc1 ofs regs pc2 pcs,
      (forall pc, Plt pc pc2 ->
             c!pc = c'!pc) ->
      tr_global_regs kappa f c pc1 id ofs n regs pc2 pcs ->
      tr_global_regs kappa f c' pc1 id ofs n regs pc2 pcs.

  Lemma tr_regs_annot_incr:
    forall kappa f c alpha pc1 regs regs' pc2 pcs,
      tr_regs_annot kappa f c pc1 alpha regs regs' pc2 pcs ->
      Ple pc1 pc2.
    
  Lemma tr_regs_annot_unchanged:
    forall kappa f c c' alpha pc1 regs regs' pc2 pcs,
      (forall pc, Plt pc pc2 ->
             c!pc = c'!pc) ->
      tr_regs_annot kappa f c pc1 alpha regs regs' pc2 pcs ->
      tr_regs_annot kappa f c' pc1 alpha regs regs' pc2 pcs .

  Lemma put_all_in_regs_regs_spec:
    forall kappa alpha s regs s',
      put_all_in_regs ge STK SIZE kappa alpha s = OK (regs, s') ->
      forall r, In r regs -> Ple (st_nextreg s) r /\ Plt r (st_nextreg s').

  Lemma tr_regs_annot_is_disjoint:
    forall kappa f c pc1 alpha regs regs' pc2 pcs,
      tr_regs_annot kappa f c pc1 alpha regs regs' pc2 pcs ->
      list_disjoint regs regs'.

  Lemma put_all_in_regs_spec':
    forall kappa f alpha s regs s',
      put_all_in_regs ge STK SIZE kappa alpha s = OK (regs, s') ->
      Plt (max_reg_function f) (st_nextreg s) ->
      exists regs' pcs, tr_regs_annot kappa f s'.(st_code) s.(st_nextnode) alpha regs regs' s'.(st_nextnode) pcs
                   /\ forall r, In r regs' -> Ple (st_nextreg s) r /\ Plt r s'.(st_nextreg).

  Lemma put_all_in_regs_spec:
    forall kappa f alpha s regs s',
      put_all_in_regs ge STK SIZE kappa alpha s = OK (regs, s') ->
      Plt (max_reg_function f) (st_nextreg s) ->
      exists regs' pcs, tr_regs_annot kappa f s'.(st_code) s.(st_nextnode) alpha regs regs' s'.(st_nextnode) pcs.
  
  Lemma put_checks_spec:
    forall reg0 regs s s',
      put_checks reg0 regs s = OK s' ->
      exists pcs, tr_cmp_regs s'.(st_code) s.(st_nextnode) reg0 regs s'.(st_nextnode) pcs.

  Lemma tr_cmp_regs_incr:
    forall c reg0 regs pc1 pc2 pcs,
      tr_cmp_regs c pc1 reg0 regs pc2 pcs ->
      Ple pc1 pc2.
  
  Lemma tr_cmp_regs_unchanged:
    forall c c' reg0 regs pc1 pc2 pcs,
      (forall pc, Plt pc pc2 ->
             c!pc = c'!pc) ->
      tr_cmp_regs c pc1 reg0 regs pc2 pcs ->
      tr_cmp_regs c' pc1 reg0 regs pc2 pcs.

  Lemma put_ors_spec:
    forall reg0 regs s s',
      put_ors reg0 regs s = OK s' ->
      exists pcs, tr_or_regs s'.(st_code) s.(st_nextnode) reg0 regs s'.(st_nextnode) pcs.

  Lemma tr_or_regs_incr:
    forall c reg0 regs pc1 pc2 pcs,
      tr_or_regs c pc1 reg0 regs pc2 pcs ->
      Ple pc1 pc2.
  
  Lemma tr_or_regs_unchanged:
    forall c c' reg0 regs pc1 pc2 pcs,
      (forall pc, Plt pc pc2 ->
             c!pc = c'!pc) ->
      tr_or_regs c pc1 reg0 regs pc2 pcs ->
      tr_or_regs c' pc1 reg0 regs pc2 pcs.

  Lemma st_code_unchanged f s x :
    (∀ s, unchanged s (f s) ∧ sincr s (f s)) →
    (x < st_nextnode s)%positive →
    (st_code (f s)) ! x = (st_code s) ! x.

  Lemma st_code_add_return_undef_0 {ty r s} :
    let c := st_code (add_return_undef ty r s) in
    ∀ pc,
      pc = st_nextnode s →
      c ! pc = Some (Iop (Ointconst Int.zero) nil (st_nextreg s) (Pos.succ (st_nextnode s))).

  Lemma st_code_add_return_undef_1 {ty r s} :
    let c := st_code (add_return_undef ty r s) in
    ∀ pc,
      pc = Pos.succ (st_nextnode s) →
      c ! pc = Some (Iop (Ointconst (Int.repr (Zpos r))) nil (Pos.succ (st_nextreg s)) (Pos.succ (Pos.succ (st_nextnode s)))).

  Lemma st_code_add_return_undef_2 {ty r s} :
    let c := st_code (add_return_undef ty r s) in
    ∀ pc,
      pc = Pos.succ (Pos.succ (st_nextnode s)) →
      c ! pc = Some (Iop Odiv (Pos.succ (st_nextreg s) :: st_nextreg s :: nil) (Pos.succ (Pos.succ (st_nextreg s))) (Pos.succ (Pos.succ (Pos.succ (st_nextnode s))))).
  Opaque add_return_undef.

  Lemma add_checks_spec:
    forall f opt i alpha kappa addr args s s' (Hnottrivial: is_trivial_annotation prog alpha kappa addr = false) (Hnot_singleton: is_singleton (snd alpha) = false),
      add_checks prog ge STK SIZE opt i alpha kappa addr args s = OK s' ->
      Plt (max_reg_function f) (st_nextreg s) ->
      exists pcs, tr_checks f (st_code s') (st_nextnode s) i alpha kappa addr args pcs.

  Lemma add_epilogue_spec:
    forall f i s s',
      add_epilogue SIZE i s = OK s' ->
      Plt (max_reg_function f) (st_nextreg s) ->
      exists pcs, tr_epilogue f (st_code s') (st_nextnode s) i pcs.

  Lemma add_epilogue_unchanged_and_sincr:
    forall i s s',
      add_epilogue SIZE i s = OK s' →
      unchanged s s' ∧ sincr s s'.

  Lemma check_annotations_depth_spec:
    forall alpha x,
      check_annotations_depth STK SIZE alpha = OK x ->
      forall depth varname range,
        In (ABlocal depth varname range) alpha ->
        (depth < 128)%nat.

  Lemma check_annotations_depth_spec':
    forall alpha x,
      check_annotations_depth STK SIZE alpha = OK x ->
      forall id range,
        In (ABglobal id range) alpha ->
        id <> STK /\ id <> SIZE.

  Lemma check_globals_of_builtin_args_spec:
    forall id al x,
      check_globals_of_builtin_args id al = OK x ->
      ~ In id (globals_of_builtin_args al).

  Lemma check_annotations_divides_spec':
    forall kappa n ofs x,
      check_annotations_divides' kappa ofs n = OK x ->
      exists x, In x (int_ranges n ofs) /\ (align_chunk kappa | x).

  Lemma check_annotations_divides_spec:
    forall kappa alpha x,
      check_annotations_divides kappa alpha = OK x ->
      (forall depth varname base bound, In (ABlocal depth varname (base, bound)) alpha ->
                                   forall size, Int.unsigned (Int.sub bound base) + 1 = Z.pos size ->
                                           exists x, In x (int_ranges (Pos.to_nat size) base) /\ ((align_chunk kappa) | x)).

  Lemma check_annotations_range_spec:
    forall alpha x,
      check_annotations_range alpha = OK x ->
      forall depth varname base bound, In (ABlocal depth varname (base, bound)) alpha ->
                                  Int.unsigned base <= Int.unsigned bound < Int.modulus - 1.
          
  Lemma check_annotations_range_spec':
    forall alpha x,
      check_annotations_range alpha = OK x ->
      forall id base bound, In (ABglobal id (base, bound)) alpha -> Int.unsigned base <= Int.unsigned bound < Int.modulus - 1.
    induction alpha; intros.
    - inv H0.
    - simpl in H. destruct H0.
      + subst a. destruct (zle (Int.unsigned base) (Int.unsigned bound)); inv H.
        replace (Int.modulus - 1) with 4294967295; try reflexivity.
        destruct (zlt (Int.unsigned bound) 4294967295); inv H1.
        omega.
      + destruct a.
        * destruct range. destruct (zle (Int.unsigned i) (Int.unsigned i0)); inv H.
          replace (Int.modulus - 1) with 4294967295; try reflexivity.
          destruct (zlt (Int.unsigned i0) 4294967295); inv H2.
          eapply IHalpha; eauto.
        * destruct range. destruct (zle (Int.unsigned i) (Int.unsigned i0)); inv H.
          replace (Int.modulus - 1) with 4294967295; try reflexivity.
          destruct (zlt (Int.unsigned i0) 4294967295); inv H2.
          eapply IHalpha; eauto.
  Qed.