Module RTLdefgenproof

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.
Require Import RTLdefgenspec.
Require Import Behaviors.
Require Import MoreAxioms.

Theorem FSIM:
  forall p, forward_simulation (semantics_block' p) (RTL.semantics p).

Section PRESERVATION.

  Variable prog: program.
  Variable tprog: program.
  Hypothesis TRANSF: transf_program prog = OK tprog.
  Definition ge := Genv.globalenv prog.
  Definition tge := Genv.globalenv tprog.
  Let STK := Psucc (Psucc (fold_left Pmax ((map fst (prog_defs prog)) ++ prog_public prog) 1%positive)).
  Let SIZE := Psucc STK.
  
  Hypothesis DEFSAFE: forall beh, program_behaves (RTL.semantics tprog) beh -> not_wrong beh.
  Hypothesis SAFE: forall beh, program_behaves (RTL.semantics prog) beh -> not_wrong beh.

  Opaque Z.mul. Opaque Z.sub.

  Lemma TRANSF':
    transform_partial_augment_program (transf_fundef prog (Genv.globalenv prog) STK SIZE)
         (fun v : unit => OK v) ((STK, Gvar STK_globvar) :: (SIZE, Gvar SIZE_globvar) :: nil)
         (prog_main prog) prog = OK tprog.
  
  Lemma init_state_exists:
    exists s, initial_state prog s.

  Lemma init_state_exists':
    exists s, initial_state tprog s.

  Lemma SIZE_exists:
    exists b, Genv.find_symbol tge SIZE = Some b
         /\ Genv.find_var_info tge b = Some SIZE_globvar.

  Lemma STK_exists:
    exists b, Genv.find_symbol tge STK = Some b
         /\ Genv.find_var_info tge b = Some STK_globvar.
  
  Lemma symbols_preserved:
    forall (s: ident),
      ~ In s (STK::SIZE::nil) ->
      Genv.find_symbol tge s = Genv.find_symbol ge s.

  Lemma public_preserved:
    forall (s: ident),
      ~ In s (STK::SIZE::nil) ->
      Genv.public_symbol tge s = Genv.public_symbol ge s.

  Lemma varinfo_preserved:
    forall b v, Genv.find_var_info ge b = Some v ->
           Genv.find_var_info tge b = Some v.

  Lemma functions_translated:
    forall (v: val) (f: RTL.fundef),
      Genv.find_funct ge v = Some f ->
      exists tf,
        Genv.find_funct tge v = Some tf /\ transf_fundef prog ge STK SIZE f = OK tf.
  
  Lemma function_ptr_translated:
    forall (b: block) (f: RTL.fundef),
      Genv.find_funct_ptr ge b = Some f ->
      exists tf,
        Genv.find_funct_ptr tge b = Some tf /\ transf_fundef prog ge STK SIZE f = OK tf.
  
  Lemma sig_function_translated:
    forall f tf,
      transf_fundef prog ge STK SIZE f = OK tf ->
      funsig tf = funsig f.

  Lemma stacksize_translated:
    forall f tf,
      transf_function prog ge STK SIZE f = OK tf -> tf.(fn_stacksize) = f.(fn_stacksize).

  Lemma find_function_translated:
    forall j n ros rs fd trs,
      match ros with
      | inl r => rs#r = trs#r
      | inr s => ~ In s (STK::SIZE::nil)
      end ->
      find_function ge ros rs = Some fd ->
      regs_agree j n rs trs ->
      exists tfd, find_function tge ros trs = Some tfd /\ transf_fundef prog ge STK SIZE fd = OK tfd.
  
  Lemma fold_left_Pmax_invariant:
    forall l m n,
      Ple m n ->
      Ple m (fold_left Pmax l n).
    
  Lemma fold_left_Pmax_invariant_aux:
    forall l m n,
      Ple m n ->
      Ple (fold_left Pmax l m) (fold_left Pmax l n).

  Lemma new_globs_are_new:
    forall s l,
      In s l ->
      Ple s (fold_left Pmax l xH).
  
  Lemma STK_is_new:
    ~ In STK (List.map fst prog.(prog_defs)).

  Lemma SIZE_is_new:
    ~ In SIZE (List.map fst prog.(prog_defs)).

  Lemma STK_not_public:
    ~ In STK prog.(prog_public).
  
  Lemma SIZE_not_public:
    ~ In SIZE prog.(prog_public).

  Lemma STK_SIZE_are_new:
    forall id b,
      Genv.find_symbol ge id = Some b ->
      ~ In id (STK::SIZE::nil).

  Lemma norepet_prog_defs:
    list_norepet (map fst (prog_defs prog)).

  Lemma check_init_data_list_size_spec:
    forall l,
      check_init_data_list_size l = true ->
      forall gv, In (Gvar gv) l -> Genv.init_data_list_size (gvar_init gv) <= Int.max_unsigned.

  Lemma prog_defs_init_data_is_bounded:
    forall gv, In (Gvar gv) (map snd prog.(prog_defs)) -> Genv.init_data_list_size (gvar_init gv) <= Int.max_unsigned.
    
  Lemma tr_local_regs_correct:
    forall kappa j sp sp' stk f tf n pc1 ofs depth regs regs' pc2 pcs vals rs trs m,
      tr_local_regs STK kappa f (fn_code tf) pc1 ofs depth n regs regs' pc2 pcs ->
      addr_of_local kappa (Vptr sp' Int.zero) ofs n vals ->
      regs_agree j (max_reg_function f) rs trs ->
      (forall r : positive, Plt (max_reg_function f) r -> rs # r = Vundef) ->
      (exists n, Mem.loadv Mint32 m (Genv.symbol_address tge SIZE Int.zero) = Some (Vint n)
            /\ Mem.loadv Mint32 m (Val.add (Genv.symbol_address tge STK (Int.repr (-4 * Z.of_nat depth))) (Vint n)) = Some (Vptr sp' Int.zero)) ->
      exists trs', star step tge (State stk tf sp pc1 trs m) E0 (State stk tf sp pc2 trs' m) /\
              list_forall2 (fun reg val => trs' # reg = val) regs vals /\
              regs_agree j (max_reg_function f) rs trs' /\
              forall reg, ~ In reg (regs ++ regs') -> trs#reg = trs'#reg.
  
  Lemma tr_global_regs_correct:
    forall kappa j sp stk f tf id b n pc1 ofs regs pc2 pcs vals rs trs m,
      tr_global_regs kappa f (fn_code tf) pc1 id ofs n regs pc2 pcs ->
      addr_of_global kappa b ofs n vals ->
      regs_agree j (max_reg_function f) rs trs ->
      (forall r : positive, Plt (max_reg_function f) r -> rs # r = Vundef) ->
      Genv.find_symbol ge id = Some b ->
      ~ In id (STK::SIZE::nil) ->
      exists trs', star step tge (State stk tf sp pc1 trs m) E0 (State stk tf sp pc2 trs' m) /\
              list_forall2 (fun reg val => trs' # reg = val) regs vals /\
              regs_agree j (max_reg_function f) rs trs' /\
              forall reg, ~ In reg regs -> trs#reg = trs'#reg.

  Inductive shadowstack_is_sound (stk: list val) (m :mem): Prop :=
  | shadowstack_is_sound_intro:
      (let n := length stk in
       Mem.loadv Mint32 m (Genv.symbol_address tge SIZE Int.zero) = Some (Vint (Int.repr (4 * ((Z.of_nat n) - 1))))
       /\ (forall depth sp, pop depth stk = Some sp <->
                      ((depth < length stk)%nat /\ Mem.loadv Mint32 m (Val.add (Genv.symbol_address tge STK (Int.repr (-4 * Z.of_nat depth))) (Vint (Int.repr (4 * ((Z.of_nat n) - 1))))) = Some sp))) ->
      shadowstack_is_sound stk m.

  Lemma divides_none_implies_local:
    forall kappa f c n pc1 base depth regs regs' pc2 pcs,
      (forall x, In x (int_ranges n base) -> ~ (align_chunk kappa | x)) ->
      tr_local_regs STK kappa f c pc1 base depth n regs regs' pc2 pcs ->
      tr_local_regs STK kappa f c pc1 base depth n nil nil pc1 nil.

  Lemma divides_none_implies_global:
    forall kappa f c n pc1 id base regs pc2 pcs,
      (forall x, In x (int_ranges n base) -> ~ (align_chunk kappa | x)) ->
      tr_global_regs kappa f c pc1 id base n regs pc2 pcs ->
      tr_global_regs kappa f c pc1 id base n nil pc1 nil.
    
  Lemma tr_regs_annot_correct:
    forall kappa j sp stk f tf alpha pc1 regs regs' pc2 pcs vals rs trs m
      (PTRS: forall ptr,
          In ptr (sp::(List.map (fun s => match s with Stackframe res f sp pc rs => sp end) stk)) ->
          exists b, ptr = Vptr b Int.zero)
      (Hdivex: 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)),
      tr_regs_annot prog STK kappa f (fn_code tf) pc1 alpha regs regs' pc2 pcs ->
      addr_of_annotations kappa tge (sp::(List.map (fun s => match s with Stackframe res f sp pc rs => sp end) stk)) alpha vals ->
      regs_agree j (max_reg_function f) rs trs ->
      (forall r : positive, Plt (max_reg_function f) r -> rs # r = Vundef) ->
      shadowstack_is_sound (sp::(List.map (fun s => match s with Stackframe res f sp pc rs => sp end) stk)) m ->
      exists trs', star step tge (State stk tf sp pc1 trs m) E0 (State stk tf sp pc2 trs' m) /\
              list_forall2 (fun reg val => trs' # reg = val) regs vals /\
              regs_agree j (max_reg_function f) rs trs' /\
              forall reg, ~ In reg (regs ++ regs') -> trs#reg = trs'#reg.

  Inductive addr_of_annotations_singleton (ge: Genv.t fundef unit) (sps: list val): list ablock -> list (val + (val * val)) -> Prop :=
  | addr_of_annotations_singleton_local:
      forall depth varname sp base bound alpha vals,
        pop depth sps = Some sp ->
        addr_of_annotations_singleton ge sps alpha vals ->
        addr_of_annotations_singleton ge sps ((ABlocal depth varname (base, bound))::alpha) ((if Int.eq_dec base bound then inl (Val.add sp (Vint base)) else inr (Val.add sp (Vint base), Val.add sp (Vint bound)))::vals)
  | addr_of_annotations_singleton_global:
      forall id b base bound alpha vals,
        Genv.find_symbol ge b = Some id ->
        addr_of_annotations_singleton ge sps alpha vals ->
        addr_of_annotations_singleton ge sps ((ABglobal b (base, bound))::alpha) ((if Int.eq_dec base bound then inl (Vptr id base) else inr (Vptr id base, Vptr id bound))::vals)
  | addr_of_annotations_singleton_nil:
      addr_of_annotations_singleton ge sps nil nil.

  Definition match_reg_val rs (r: reg + (reg * reg)) (v: val + (val * val)): Prop :=
    match r with
    | inl r =>
      match v with
      | inl v => rs # r = v
      | _ => False
      end
    | inr (r, r') =>
      match v with
      | inr (v, v') => rs # r = v /\ rs # r' = v'
      | _ => False
      end
    end.

  Lemma tr_local_regs_singleton_correct:
    forall j sp sp' stk f tf pc1 depth base bound regs regs' pc2 pcs rs trs m,
      tr_local_regs' STK f (fn_code tf) pc1 depth base bound regs regs' pc2 pcs ->
      regs_agree j (max_reg_function f) rs trs ->
      (forall r : positive, Plt (max_reg_function f) r -> rs # r = Vundef) ->
      (exists n, Mem.loadv Mint32 m (Genv.symbol_address tge SIZE Int.zero) = Some (Vint n)
            /\ Mem.loadv Mint32 m (Val.add (Genv.symbol_address tge STK (Int.repr (-4 * Z.of_nat depth))) (Vint n)) = Some (Vptr sp' Int.zero)) ->
      exists trs', star step tge (State stk tf sp pc1 trs m) E0 (State stk tf sp pc2 trs' m) /\
              (match regs with inl r => trs'#r = Vptr sp' base | inr (r, r') => trs'#r = Vptr sp' base /\ trs'#r' = Vptr sp' bound end) /\
              regs_agree j (max_reg_function f) rs trs' /\
              forall reg, ~ In reg (match regs with inl r => r::regs' | inr (r, r') => r::r'::regs' end) -> trs#reg = trs'#reg.

  Lemma tr_global_regs_singleton_correct:
    forall j sp stk f tf id b pc1 base bound regs pc2 pcs rs trs m,
      tr_global_regs' f (fn_code tf) pc1 id base bound regs pc2 pcs ->
      regs_agree j (max_reg_function f) rs trs ->
      (forall r : positive, Plt (max_reg_function f) r -> rs # r = Vundef) ->
      Genv.find_symbol ge id = Some b ->
      ~ In id (STK::SIZE::nil) ->
      exists trs', star step tge (State stk tf sp pc1 trs m) E0 (State stk tf sp pc2 trs' m) /\
              (match regs with inl r => trs'#r = Vptr b base | inr (r, r') => trs'#r = Vptr b base /\ trs'#r' = Vptr b bound end) /\
              regs_agree j (max_reg_function f) rs trs' /\
              forall reg, ~ In reg (match regs with inl r => r::nil | inr (r, r') => r::r'::nil end) -> trs#reg = trs'#reg.

  Lemma tr_regs_annot_correct_singleton:
    forall j sp stk f tf alpha pc1 regs regs' pc2 pcs vals rs trs m
      (PTRS: forall ptr,
          In ptr (sp::(List.map (fun s => match s with Stackframe res f sp pc rs => sp end) stk)) ->
          exists b, ptr = Vptr b Int.zero),
      tr_regs_annot' prog STK f (fn_code tf) pc1 alpha regs regs' pc2 pcs ->
      addr_of_annotations_singleton tge (sp::(List.map (fun s => match s with Stackframe res f sp pc rs => sp end) stk)) alpha vals ->
      regs_agree j (max_reg_function f) rs trs ->
      (forall r : positive, Plt (max_reg_function f) r -> rs # r = Vundef) ->
      shadowstack_is_sound (sp::(List.map (fun s => match s with Stackframe res f sp pc rs => sp end) stk)) m ->
      exists trs', star step tge (State stk tf sp pc1 trs m) E0 (State stk tf sp pc2 trs' m) /\
              list_forall2 (match_reg_val trs') regs vals /\
              regs_agree j (max_reg_function f) rs trs' /\
              forall reg, ~ In reg ((fold_right (fun x acc => match x with inl r => r::acc | inr (r, r') => r::r'::acc end) nil regs) ++ regs') -> trs#reg = trs'#reg.

  Lemma tr_cmp_regs_correct:
    forall j ts sp f tf reg0 regs pc1 pc2 pcs m rs trs vals,
      tr_cmp_regs (fn_code tf) pc1 reg0 regs pc2 pcs ->
      ~ In reg0 regs ->
      list_forall2 (fun reg val => trs#reg = val) regs vals ->
      regs_agree j (max_reg_function f) rs trs ->
      (forall r, In r regs -> Plt (max_reg_function f) r) ->
      (forall r, Plt (max_reg_function f) r -> rs#r = Vundef) ->
      list_norepet regs ->
      exists trs', star step tge (State ts tf sp pc1 trs m) E0 (State ts tf sp pc2 trs' m) /\
              list_forall2 (fun reg val => trs'#reg = Val.of_optbool (eval_condition (Ccompu Ceq) ((trs#reg0)::val::nil) m)) regs vals /\
              forall reg, ~ In reg regs -> trs#reg = trs'#reg.

  Definition match_reg_val' m rs rs' (r0: reg) (r: reg + (reg * reg)) (v: val + (val * val)): Prop :=
    match r with
    | inl r =>
      match v with
      | inl v => rs'#r = Val.of_optbool (eval_condition (Ccompu Ceq) (v::(rs#r0)::nil) m)
      | _ => False
      end
    | inr (r, r') =>
      match v with
      | inr (v, v') => rs'#r = (Val.and (Val.of_optbool (Val.cmpu_bool (Mem.valid_pointer m) Cle v rs#r0)) (Val.of_optbool (Val.cmpu_bool (Mem.valid_pointer m) Cle rs#r0 v')))
      | _ => False
      end
    end.

  Lemma list_forall2_not_in':
    forall trs regs vl a v,
      list_forall2 (match_reg_val trs) regs vl ->
      ~ In a (fold_right (fun x acc => match x with | inl r => r::acc | inr (r, r') => r::r'::acc end) nil regs) ->
      list_forall2 (match_reg_val (trs # a <- v)) regs vl.

  Lemma list_forall2_not_in'':
    forall m trs trs' reg0 regs vl a v,
      list_forall2 (match_reg_val' m (trs # a <- v) trs' reg0) regs vl ->
      ~ In a (fold_right (fun x acc => match x with | inl r => r::acc | inr (r, r') => r::r'::acc end) nil regs) ->
      a <> reg0 ->
      list_forall2 (match_reg_val' m trs trs' reg0) regs vl.

  Lemma list_forall2_not_in_2:
    forall m trs trs' reg0 regs vl a v,
      list_forall2 (match_reg_val' m trs trs' reg0) regs vl ->
      ~ In a (fold_right (fun x acc => match x with | inl r => r::acc | inr (r, r') => r::r'::acc end) nil regs) ->
      list_forall2 (match_reg_val' m trs (trs'#a <- v) reg0) regs vl.

  Lemma tr_cmp_regs_correct_singleton:
    forall j ts sp f tf reg0 regs pc1 pc2 pcs m rs trs vals,
      tr_cmp_regs' (fn_code tf) pc1 reg0 regs pc2 pcs ->
      ~ In reg0 (fold_right (fun x acc => match x with | inl r => r::acc | inr (r, r') => r::r'::acc end) nil regs) ->
      list_forall2 (match_reg_val trs) regs vals ->
      regs_agree j (max_reg_function f) rs trs ->
      (forall r, In r regs -> match r with | inl r => Plt (max_reg_function f) r | inr (r, r') => Plt (max_reg_function f) r /\ Plt (max_reg_function f) r' end) ->
      (forall r, Plt (max_reg_function f) r -> rs#r = Vundef) ->
      list_norepet (fold_right (fun x acc => match x with | inl r => r::acc | inr (r, r') => r::r'::acc end) nil regs) ->
      exists trs', star step tge (State ts tf sp pc1 trs m) E0 (State ts tf sp pc2 trs' m) /\
              list_forall2 (match_reg_val' m trs trs' reg0) regs vals /\
              forall reg, ~ In reg (fold_right (fun x acc => match x with | inl r => r::acc | inr (r, r') => r::r'::acc end) nil regs) -> trs#reg = trs'#reg.

  Lemma tr_or_regs_true:
    forall ts tf m regs pc1 reg0 pc2 pcs sp trs,
      tr_or_regs (fn_code tf) pc1 reg0 regs pc2 pcs ->
      (forall r, In r regs -> trs#r = Vtrue \/ trs#r = Vfalse) ->
      ~ In reg0 regs ->
      trs#reg0 = Vtrue ->
      exists trs', star step tge (State ts tf (Vptr sp Int.zero) pc1 trs m) E0 (State ts tf (Vptr sp Int.zero) pc2 trs' m) /\ trs'#reg0 = Vtrue /\ forall r, r <> reg0 -> trs'#r = trs#r.
  
  Lemma tr_or_regs_correct:
    forall ts tf m regs pc1 reg0 pc2 pcs sp trs,
      tr_or_regs (fn_code tf) pc1 reg0 regs pc2 pcs ->
      (forall r, In r regs -> trs#r = Vtrue \/ trs#r = Vfalse) ->
      ~ In reg0 regs ->
      (exists r, In r regs /\ trs#r = Vtrue) ->
      trs#reg0 = Vtrue \/ trs#reg0 = Vfalse ->
      exists trs', star step tge (State ts tf (Vptr sp Int.zero) pc1 trs m) E0 (State ts tf (Vptr sp Int.zero) pc2 trs' m) /\ trs'#reg0 = Vtrue /\ forall r, r <> reg0 -> trs'#r = trs#r.
  
  Inductive match_stackframes: meminj -> stackframe -> stackframe -> Prop :=
  | match_stackframes_intro:
      forall j res f tf sp tsp pc rs trs
        (FUN: transf_function prog ge STK SIZE f = OK tf)
        (RES: regs_agree j (max_reg_function f) rs trs)
        (PLE: Ple res (max_reg_function f))
        (UNDEF: forall r, Plt (max_reg_function f) r -> rs#r = Vundef)
        (SPINJ: j sp = Some (tsp, 0)),
        match_stackframes j (Stackframe res f (Vptr sp Int.zero) pc rs)
                            (Stackframe res tf (Vptr tsp Int.zero) pc trs).

  Inductive match_states: RTL.state -> RTL.state -> Prop :=
  | match_regular_states:
      forall s ts f tf sp tsp pc rs trs j m tm
        (STACKS: list_forall2 (match_stackframes j) s ts)
        (FUN: transf_function prog ge STK SIZE f = OK tf)
        (RES: regs_agree j (max_reg_function f) rs trs)
        (STEP: forall s0, initial_state prog s0 -> exists t, star step_block' ge s0 t (State s f (Vptr sp Int.zero) pc rs m))
        (STEP': forall s0, initial_state tprog s0 -> exists t, star RTL.step tge s0 t (State ts tf (Vptr tsp Int.zero) pc trs tm))
        (UNDEF: forall r, Plt (max_reg_function f) r -> rs#r = Vundef)
        (MINJ: Mem.inject j m tm)
        (SPINJ: j sp = Some (tsp, 0))
        (GINJ: forall b, Plt b ge.(Genv.genv_next) -> j b = Some (b, 0))
        (STKNOTMAPPED: forall bSTK ofs, Genv.symbol_address tge STK ofs = Vptr bSTK ofs ->
                                   (forall b b' delta, j b = Some (b', delta) -> b' <> bSTK))
        (SIZENOTMAPPED: forall bSIZE ofs, Genv.symbol_address tge SIZE ofs = Vptr bSIZE ofs ->
                                     (forall b b' delta, j b = Some (b', delta) -> b' <> bSIZE))
        (BSTKPLT: forall bSTK, Genv.find_symbol tge STK = Some bSTK -> Plt bSTK (Mem.nextblock tm))
        (BSIZEPLT: forall bSIZE, Genv.find_symbol tge SIZE = Some bSIZE -> Plt bSIZE (Mem.nextblock tm))
        (STKPERM: forall bSTK, Genv.find_symbol tge STK = Some bSTK -> Mem.range_perm tm bSTK 0 512 Cur Writable)
        (SIZEPERM: forall bSIZE, Genv.find_symbol tge SIZE = Some bSIZE -> Mem.range_perm tm bSIZE 0 4 Cur Writable)
        (STKRANGE: forall bSTK, Genv.find_symbol tge STK = Some bSTK -> (forall ofs, Mem.perm tm bSTK ofs Cur Readable <-> 0 <= ofs < 512))
        (SIZERANGE: forall bSIZE, Genv.find_symbol tge SIZE = Some bSIZE -> (forall ofs, Mem.perm tm bSIZE ofs Cur Readable <-> 0 <= ofs < 4))
        (GINJ': forall b b' delta, Plt b ge.(Genv.genv_next) -> j b' = Some (b, delta) -> b = b')
        (NEXTBLOCK: Ple ge.(Genv.genv_next) (Mem.nextblock m))
        (NEXTBLOCK': Ple ge.(Genv.genv_next) (Mem.nextblock tm))
        (SHADOW: shadowstack_is_sound ((Vptr tsp Int.zero)::(List.map (fun s => match s with Stackframe res f sp pc rs => sp end) ts)) tm)
        (CALLSTACK: 4 * Z.of_nat (S (length s)) < 1024)
        (FLATINJ: forall b b' delta, j b = Some (b', delta) -> delta = 0)
        (FLATINJ': forall b1 b2 b, j b1 = Some (b, 0) -> j b2 = Some (b, 0) -> b1 = b2)
        (FLATPERM: forall b b' o k p, j b = Some (b', 0) -> (Mem.perm m b o k p <-> Mem.perm tm b' o k p)),
        match_states (State s f (Vptr sp Int.zero) pc rs m)
                     (State ts tf (Vptr tsp Int.zero) pc trs tm)
  | match_call_states:
      forall s ts f tf args targs j m tm
        (STACKS: list_forall2 (match_stackframes j) s ts)
        (FUN: transf_fundef prog ge STK SIZE f = OK tf)
        (STEP: forall s0, initial_state prog s0 -> exists t, star step_block' ge s0 t (Callstate s f args m))
        (STEP': forall s0, initial_state tprog s0 -> exists t, star RTL.step tge s0 t (Callstate ts tf targs tm))
        (MINJ: Mem.inject j m tm)
        (GINJ: forall b, Plt b ge.(Genv.genv_next) -> j b = Some (b, 0))
        (STKNOTMAPPED: forall bSTK ofs, Genv.symbol_address tge STK ofs = Vptr bSTK ofs ->
                                   (forall b b' delta, j b = Some (b', delta) -> b' <> bSTK))
        (SIZENOTMAPPED: forall bSIZE ofs, Genv.symbol_address tge SIZE ofs = Vptr bSIZE ofs ->
                                     (forall b b' delta, j b = Some (b', delta) -> b' <> bSIZE))
        (BSTKPLT: forall bSTK, Genv.find_symbol tge STK = Some bSTK -> Plt bSTK (Mem.nextblock tm))
        (BSIZEPLT: forall bSIZE, Genv.find_symbol tge SIZE = Some bSIZE -> Plt bSIZE (Mem.nextblock tm))
        (INJARGS: Val.inject_list j args targs)
        (STKPERM: forall bSTK, Genv.find_symbol tge STK = Some bSTK -> Mem.range_perm tm bSTK 0 512 Cur Writable)
        (SIZEPERM: forall bSIZE, Genv.find_symbol tge SIZE = Some bSIZE -> Mem.range_perm tm bSIZE 0 4 Cur Writable)
        (STKRANGE: forall bSTK, Genv.find_symbol tge STK = Some bSTK -> (forall ofs, Mem.perm tm bSTK ofs Cur Readable <-> 0 <= ofs < 512))
        (SIZERANGE: forall bSIZE, Genv.find_symbol tge SIZE = Some bSIZE -> (forall ofs, Mem.perm tm bSIZE ofs Cur Readable <-> 0 <= ofs < 4))
        (GINJ': forall b b' delta, Plt b ge.(Genv.genv_next) -> j b' = Some (b, delta) -> b = b')
        (NEXTBLOCK: Ple ge.(Genv.genv_next) (Mem.nextblock m))
        (NEXTBLOCK': Ple ge.(Genv.genv_next) (Mem.nextblock tm))
        (SHADOW: shadowstack_is_sound (List.map (fun s => match s with Stackframe res f sp pc rs => sp end) ts) tm)
        (CALLSTACK: 4 * Z.of_nat (length s) < 1024)
        (FLATINJ: forall b b' delta, j b = Some (b', delta) -> delta = 0)
        (FLATINJ': forall b1 b2 b, j b1 = Some (b, 0) -> j b2 = Some (b, 0) -> b1 = b2)
        (FLATPERM: forall b b' o k p, j b = Some (b', 0) -> (Mem.perm m b o k p <-> Mem.perm tm b' o k p)),
        match_states (Callstate s f args m)
                     (Callstate ts tf targs tm)
  | match_return_states:
      forall s ts v tv j m tm
        (STACKS: list_forall2 (match_stackframes j) s ts)
        (STEP: forall s0, initial_state prog s0 -> exists t, star step_block' ge s0 t (Returnstate s v m))
        (STEP': forall s0, initial_state tprog s0 -> exists t, star RTL.step tge s0 t (Returnstate ts tv tm))
        (MINJ: Mem.inject j m tm)
        (GINJ: forall b, Plt b ge.(Genv.genv_next) -> j b = Some (b, 0))
        (STKNOTMAPPED: forall bSTK ofs, Genv.symbol_address tge STK ofs = Vptr bSTK ofs ->
                                   (forall b b' delta, j b = Some (b', delta) -> b' <> bSTK))
        (SIZENOTMAPPED: forall bSIZE ofs, Genv.symbol_address tge SIZE ofs = Vptr bSIZE ofs ->
                                     (forall b b' delta, j b = Some (b', delta) -> b' <> bSIZE))
        (BSTKPLT: forall bSTK, Genv.find_symbol tge STK = Some bSTK -> Plt bSTK (Mem.nextblock tm))
        (BSIZEPLT: forall bSIZE, Genv.find_symbol tge SIZE = Some bSIZE -> Plt bSIZE (Mem.nextblock tm))
        (INJV: Val.inject j v tv)
        (STKPERM: forall bSTK, Genv.find_symbol tge STK = Some bSTK -> Mem.range_perm tm bSTK 0 512 Cur Writable)
        (SIZEPERM: forall bSIZE, Genv.find_symbol tge SIZE = Some bSIZE -> Mem.range_perm tm bSIZE 0 4 Cur Writable)
        (STKRANGE: forall bSTK, Genv.find_symbol tge STK = Some bSTK -> (forall ofs, Mem.perm tm bSTK ofs Cur Readable <-> 0 <= ofs < 512))
        (SIZERANGE: forall bSIZE, Genv.find_symbol tge SIZE = Some bSIZE -> (forall ofs, Mem.perm tm bSIZE ofs Cur Readable <-> 0 <= ofs < 4))
        (GINJ': forall b b' delta, Plt b ge.(Genv.genv_next) -> j b' = Some (b, delta) -> b = b')
        (NEXTBLOCK: Ple ge.(Genv.genv_next) (Mem.nextblock m))
        (NEXTBLOCK': Ple ge.(Genv.genv_next) (Mem.nextblock tm))
        (SHADOW: shadowstack_is_sound (List.map (fun s => match s with Stackframe res f sp pc rs => sp end) ts) tm)
        (CALLSTACK: 4 * Z.of_nat (length s) < 1024)
        (FLATINJ: forall b b' delta, j b = Some (b', delta) -> delta = 0)
        (FLATINJ': forall b1 b2 b, j b1 = Some (b, 0) -> j b2 = Some (b, 0) -> b1 = b2)
        (FLATPERM: forall b b' o k p, j b = Some (b', 0) -> (Mem.perm m b o k p <-> Mem.perm tm b' o k p)),
        match_states (Returnstate s v m)
                     (Returnstate ts tv tm).

  Lemma GINJ_implies:
    forall j,
      (forall b, Plt b ge.(Genv.genv_next) -> j b = Some (b, 0)) ->
      forall id b, Genv.find_symbol ge id = Some b -> j b = Some (b, 0).
  
  Lemma addr_of_annotations_translated:
    forall kappa j sps tsps alpha vals,
      list_forall2 (fun sp tsp => exists bsp btsp, sp = Vptr bsp Int.zero /\ tsp = Vptr btsp Int.zero /\ j bsp = Some (btsp, 0)) sps tsps ->
      (forall b id, Genv.find_symbol ge id = Some b -> j b = Some (b, 0)) ->
      addr_of_annotations kappa ge sps alpha vals ->
      exists tvals, addr_of_annotations kappa tge tsps alpha tvals /\ list_forall2 (Val.inject j) vals tvals.

  Lemma symbol_address_inject:
    forall j id ofs,
      (forall b id, Genv.find_symbol ge id = Some b -> j b = Some (b, 0)) ->
      Val.inject j (Genv.symbol_address ge id ofs) (Genv.symbol_address tge id ofs).

  Lemma match_stackframes_sps:
    forall j stk tstk,
      list_forall2 (match_stackframes j) stk tstk ->
      list_forall2 (fun sp tsp => exists bsp btsp, sp = Vptr bsp Int.zero /\ tsp = Vptr btsp Int.zero /\ j bsp = Some (btsp, 0)) (map (fun s => match s with | Stackframe _ _ sp _ _ => sp end) stk) (map (fun s => match s with | Stackframe _ _ sp _ _ => sp end) tstk).

  Lemma match_stackframes_sps_are_ptrs:
    forall j stk tstk,
      list_forall2 (match_stackframes j) stk tstk ->
      (forall sp, In sp (map (fun s => match s with | Stackframe _ _ sp _ _ => sp end) tstk) ->
             exists b, sp = Vptr b Int.zero).

  Lemma match_stackframes_sps_are_ptrs':
    forall j stk tstk,
      list_forall2 (match_stackframes j) stk tstk ->
      (forall sp, In sp (map (fun s => match s with | Stackframe _ _ sp _ _ => sp end) stk) ->
             exists b, sp = Vptr b Int.zero).
  
  Lemma eval_condition_translated:
    forall j a ta m tm vals tvals,
      Val.inject j a ta ->
      Mem.inject j m tm ->
      list_forall2 (Val.inject j) vals tvals ->
      (forall v, In v vals -> exists b ofs, v = Vptr b ofs) ->
      (forall (b : block) (ofs : int), In (Vptr b ofs) vals -> eval_condition (Ccompu Ceq) (a :: Vptr b ofs :: nil) m = Some true \/ eval_condition (Ccompu Ceq) (a :: Vptr b ofs :: nil) m = Some false) ->
      (forall (tb : block) (tofs : int), In (Vptr tb tofs) tvals -> eval_condition (Ccompu Ceq) (ta :: Vptr tb tofs :: nil) tm = Some true \/ eval_condition (Ccompu Ceq) (ta :: Vptr tb tofs :: nil) tm = Some false).

  Lemma not_is_trivial_annotation_implies:
    forall p alpha kappa addr,
      MoreRTL.is_trivial_annotation p alpha kappa addr = false ->
      snd alpha <> nil.
  
  Lemma shadowstack_is_sound_store:
    forall bSTK bSIZE sps m kappa b ofs v m',
      shadowstack_is_sound sps m ->
      Mem.store kappa m b ofs v = Some m' ->
      Genv.find_symbol tge SIZE = Some bSIZE ->
      Genv.find_symbol tge STK = Some bSTK ->
      b <> bSIZE -> b <> bSTK ->
      shadowstack_is_sound sps m'.

  Lemma tr_or_regs_undef:
    forall ts tf m regs pc1 reg0 pc2 pcs sp trs,
      tr_or_regs (fn_code tf) pc1 reg0 regs pc2 pcs ->
      ~ In reg0 regs ->
      trs#reg0 = Vundef ->
      exists trs', star step tge (State ts tf (Vptr sp Int.zero) pc1 trs m) E0 (State ts tf (Vptr sp Int.zero) pc2 trs' m) /\ trs'#reg0 = Vundef /\ forall r, r <> reg0 -> trs'#r = trs#r.

  Lemma tr_or_regs_undef':
    forall ts tf m regs pc1 reg0 pc2 pcs sp trs,
      tr_or_regs (fn_code tf) pc1 reg0 regs pc2 pcs ->
      ~ In reg0 regs ->
      (forall r, In r regs -> trs#r = Vtrue \/ trs#r = Vfalse \/ trs#r = Vundef) ->
      (exists r, trs#r = Vundef /\ In r regs) ->
      trs#reg0 = Vtrue \/ trs#reg0 = Vfalse ->
      exists trs', star step tge (State ts tf (Vptr sp Int.zero) pc1 trs m) E0 (State ts tf (Vptr sp Int.zero) pc2 trs' m) /\ trs'#reg0 = Vundef /\ forall r, r <> reg0 -> trs'#r = trs#r.

  Lemma not_undef:
    forall regs trs,
      (forall r, In r regs -> trs#r = Vtrue \/ trs#r = Vfalse \/ trs#r = Vundef) ->
      (~ (exists r, trs#r = Vundef /\ In r regs) <-> (forall r, In r regs -> trs#r = Vtrue \/ trs#r = Vfalse)).

  Lemma eval_condition_are_bools:
    forall regs vals a trs m,
      list_forall2 (fun reg val => trs#reg = Val.of_optbool (eval_condition (Ccompu Ceq) (a::val::nil) m)) regs vals ->
      (forall v, In v vals -> exists b ofs, v = Vptr b ofs) ->
      (forall r, In r regs -> trs#r = Vtrue \/ trs#r = Vfalse) ->
      forall b ofs, In (Vptr b ofs) vals -> eval_condition (Ccompu Ceq) (a::(Vptr b ofs)::nil) m = Some true \/
                                      eval_condition (Ccompu Ceq) (a::(Vptr b ofs)::nil) m = Some false.

  Lemma eval_condition_are_bools':
    forall reg0 regs vals trs trs' m,
      list_forall2 (match_reg_val' m trs trs' reg0) regs vals ->
      (forall v, In v vals -> match v with |inl v => exists b ofs, v = Vptr b ofs | inr (v, v') => exists b ofs ofs', v = Vptr b ofs /\ v' = Vptr b ofs' end) ->
      (forall r, In r regs -> match r with inl r => trs'#r = Vtrue \/ trs'#r = Vfalse | inr (r, r') => trs'#r = Vtrue \/ trs'#r = Vfalse end) ->
      forall v, In v vals -> match v with
                       | inl v => eval_condition (Ccompu Ceq) (v::trs#reg0::nil) m = Some true \/
                                 eval_condition (Ccompu Ceq) (v::trs#reg0::nil) m = Some false
                       | inr (v, v') => Val.and (Val.of_optbool (Val.cmpu_bool (Mem.valid_pointer m) Cle v trs # reg0))
                                               (Val.of_optbool (Val.cmpu_bool (Mem.valid_pointer m) Cle trs # reg0 v')) = Vtrue \/
                                       Val.and (Val.of_optbool (Val.cmpu_bool (Mem.valid_pointer m) Cle v trs # reg0))
                                               (Val.of_optbool (Val.cmpu_bool (Mem.valid_pointer m) Cle trs # reg0 v')) = Vfalse
                       end.

  Lemma eval_condition_are_false:
    forall regs vals b ofs trs m,
      list_forall2 (fun reg val => trs#reg = Val.of_optbool (eval_condition (Ccompu Ceq) ((Vptr b ofs)::val::nil) m)) regs vals ->
      (forall v, In v vals -> exists b ofs, v = Vptr b ofs) ->
      (forall r, In r regs -> trs#r = Vtrue \/ trs#r = Vfalse) ->
      ~ In (Vptr b ofs) vals ->
      forall r, In r regs -> trs#r = Vfalse.

  Lemma tr_or_regs_false:
    forall ts tf m regs pc1 reg0 pc2 pcs sp trs,
      tr_or_regs (fn_code tf) pc1 reg0 regs pc2 pcs ->
      ~ In reg0 regs ->
      (forall r, In r regs -> trs#r = Vfalse) ->
      trs#reg0 = Vfalse ->
      exists trs', star step tge (State ts tf (Vptr sp Int.zero) pc1 trs m) E0 (State ts tf (Vptr sp Int.zero) pc2 trs' m) /\ trs'#reg0 = Vfalse /\ forall r, r <> reg0 -> trs'#r = trs#r.

  Lemma regs_are_unknown:
    forall m kappa a v trs regs vals,
      Mem.loadv kappa m a = Some v ->
      list_forall2 (fun reg val => trs # reg = Val.of_optbool (eval_condition (Ccompu Ceq) (a::val::nil) m)) regs vals ->
      (forall v, In v vals -> exists b ofs, v = Vptr b ofs) ->
      forall r, In r regs -> trs#r = Vtrue \/ trs#r = Vfalse \/ trs#r = Vundef.

  Lemma regs_are_unknown_2:
    forall m trs trs' r0 regs vals,
      list_forall2 (match_reg_val' m trs trs' r0) regs vals ->
      forall r, In r (map (fun r => match r with inl r => r | inr r => fst r end) regs) -> trs'#r = Vtrue \/ trs'#r = Vfalse \/ trs'#r = Vundef.

  Lemma regs_are_unknown':
    forall m kappa a v m' trs regs vals,
      Mem.storev kappa m a v = Some m' ->
      list_forall2 (fun reg val => trs # reg = Val.of_optbool (eval_condition (Ccompu Ceq) (a::val::nil) m)) regs vals ->
      (forall v, In v vals -> exists b ofs, v = Vptr b ofs) ->
      forall r, In r regs -> trs#r = Vtrue \/ trs#r = Vfalse \/ trs#r = Vundef.

  Lemma list_forall2_in_1:
    forall A B P l1 l2 (x: A),
      list_forall2 P l1 l2 ->
      In x l1 ->
      exists (y: B), In y l2 /\ P x y.

  Lemma list_forall2_in_2:
    forall A B P l1 l2 (y: B),
      list_forall2 P l1 l2 ->
      In y l2 ->
      exists (x: A), In x l1 /\ P x y.

  Lemma is_singleton_implies:
    forall alpha,
      is_singleton alpha = true ->
      (exists d id, forall a, In a alpha -> exists ofs, a = ABlocal d id ofs) \/
      (exists id, forall a, In a alpha -> exists ofs, a = ABglobal id ofs).

  Lemma addr_of_local_are_ptrs':
    forall kappa sp o n ofs vals,
      addr_of_local kappa (Vptr sp o) ofs n vals ->
      forall v, In v vals -> exists ofs, v = Vptr sp ofs.

  Lemma addr_of_global_are_ptrs':
    forall kappa b n ofs vals,
      addr_of_global kappa b ofs n vals ->
      forall v, In v vals -> exists ofs, v = Vptr b ofs.

  Lemma addr_of_local_exists':
    forall kappa sp o n ofs vals,
      check_annotations_divides' kappa ofs n = OK tt ->
      addr_of_local kappa (Vptr sp o) ofs n vals ->
      exists v, In v vals.

  Lemma addr_of_global_exists':
    forall kappa b n ofs vals,
      check_annotations_divides' kappa ofs n = OK tt ->
      addr_of_global kappa b ofs n vals ->
      exists v, In v vals.

  Lemma addr_of_annotations_singleton':
    forall kappa ge sps alpha vals (Hdivides: check_annotations_divides kappa alpha = OK tt),
      (forall sp, In sp sps -> exists b, sp = Vptr b Int.zero) ->
      addr_of_annotations kappa ge sps alpha vals ->
      is_singleton alpha = true ->
      exists b, forall v, In v vals -> exists ofs, v = Vptr b ofs.

  Lemma addr_of_annotations_implies_singleton:
    forall kappa ge sps alpha vals (Hsps: forall sp, In sp sps -> exists b, sp = Vptr b Int.zero),
      check_annotations_range alpha = OK tt ->
      addr_of_annotations kappa ge sps alpha vals ->
      exists vals', addr_of_annotations_singleton ge sps alpha vals' /\
               forall b ofs, In (Vptr b ofs) vals -> In (inl (Vptr b ofs)) vals' \/
                                               exists ofs1 ofs2, In (inr (Vptr b ofs1, Vptr b ofs2)) vals' /\ (Int.unsigned ofs1 <= Int.unsigned ofs <= Int.unsigned ofs2).

  Lemma check_annotations_range_inv:
    forall alpha
      (Hlocrange : forall (depth : nat) (varname : ident) (base bound : int),
          In (ABlocal depth varname (base, bound)) alpha -> Int.unsigned base <= Int.unsigned bound < Int.modulus - 1)
      (Hglobrange : forall (id : ident) (base bound : int),
          In (ABglobal id (base, bound)) alpha -> Int.unsigned base <= Int.unsigned bound < Int.modulus - 1),
      check_annotations_range alpha = OK tt.

  Lemma tr_regs_annot_regs_singleton_plt:
    forall f c alpha pc1 regs regs' pc2 pcs,
      tr_regs_annot' prog STK f c pc1 alpha regs regs' pc2 pcs ->
      forall r, In r regs -> match r with | inl r => Plt (max_reg_function f) r | inr (r, r') => Plt (max_reg_function f) r /\ Plt (max_reg_function f) r' end.

  Lemma tr_regs_annot_regs'_singleton_plt:
    forall f c alpha pc1 regs regs' pc2 pcs,
      tr_regs_annot' prog STK f c pc1 alpha regs regs' pc2 pcs ->
      forall r, In r regs' -> Plt (max_reg_function f) r.

  Lemma tr_regs_annot_regs_singleton_norepet:
    forall f c alpha pc1 regs regs' pc2 pcs,
      tr_regs_annot' prog STK f c pc1 alpha regs regs' pc2 pcs ->
      list_norepet (fold_right (fun x acc => match x with | inl r => r::acc | inr (r, r') => r::r'::acc end) nil regs).

  Lemma alloc_store_zeros_cannot_fail_invariant:
    forall m n sz p m' b,
      Mem.alloc m 0 sz = (m', b) ->
      0 <= n + p <= sz ->
      0 <= p ->
      exists m'', store_zeros m' b p n = Some m''.

  Corollary alloc_store_zeros_cannot_fail:
    forall m sz m' b,
      Mem.alloc m 0 sz = (m', b) ->
      sz >= 0 ->
      exists m'', store_zeros m' b 0 sz = Some m''.

  Lemma alloc_global_STK_cannot_fail:
    forall m,
      exists m', Genv.alloc_global tge m (STK, Gvar STK_globvar) = Some m'.
  
  Lemma alloc_global_SIZE_cannot_fail:
    forall m,
      exists m', Genv.alloc_global tge m (SIZE, Gvar SIZE_globvar) = Some m'.

  Lemma epilogue_decrease_aux:
    forall n, 4 * Z.of_nat (S n) - 4 = 4 * Z.of_nat n.
  
  Lemma epilogue_decrease:
    forall n, Int.sub (Int.repr (4 * Z.of_nat (S n))) (Int.repr 4) = Int.repr (4 * Z.of_nat n).

  Lemma repr_add:
   forall a b,
     Int.add (Int.repr a) (Int.repr b) =
     Int.repr (a + b).

  Lemma repr_sub:
    forall a b,
      Int.sub (Int.repr a) (Int.repr b) =
      Int.repr (a - b).
    
  Lemma eval_builtin_arg_inject:
    forall n rs sp m j trs tsp tm a v,
      eval_builtin_arg ge (fun r => rs#r) (Vptr sp Int.zero) m a v ->
      j sp = Some (tsp, 0) ->
      regs_agree j n rs trs ->
      Mem.inject j m tm ->
      (forall id, In id (globals_of_builtin_arg a) -> ~ In id (STK::SIZE::nil)) ->
      (forall r, In r (params_of_builtin_arg a) -> Ple r n) ->
      (forall b, Plt b ge.(Genv.genv_next) -> j b = Some (b, 0)) ->
      exists tv, eval_builtin_arg tge (fun r => trs#r) (Vptr tsp Int.zero) tm a tv /\
            Val.inject j v tv.
      
  Lemma eval_builtin_args_inject:
    forall n rs sp m j trs tsp tm al vl,
      eval_builtin_args ge (fun r => rs#r) (Vptr sp Int.zero) m al vl ->
      j sp = Some (tsp, 0) ->
      regs_agree j n rs trs ->
      Mem.inject j m tm ->
      (forall id, In id (globals_of_builtin_args al) -> ~ In id (STK::SIZE::nil)) ->
      (forall r, In r (params_of_builtin_args al) -> Ple r n) ->
      (forall b, Plt b ge.(Genv.genv_next) -> j b = Some (b, 0)) ->
      exists tvl, eval_builtin_args tge (fun r => trs#r) (Vptr tsp Int.zero) tm al tvl /\
            Val.inject_list j vl tvl.

  Lemma symbols_preserved':
    forall s b,
      Genv.find_symbol ge s = Some b ->
      Genv.find_symbol tge s = Some b.

  Lemma public_preserved':
    forall s,
      Genv.public_symbol ge s = Genv.public_symbol tge s.

  Lemma match_stackframes_inject_incr:
    forall j j' stk tstk,
      match_stackframes j stk tstk ->
      inject_incr j j' ->
      match_stackframes j' stk tstk.

  Lemma forall_match_stackframes_inject_incr:
    forall j j' s ts,
      list_forall2 (match_stackframes j) s ts ->
      inject_incr j j' ->
      list_forall2 (match_stackframes j') s ts.

  Lemma fold_left_transf_instr_unchanged:
    forall opt l s s',
      fold_left (fun a p => transf_instr prog ge STK SIZE opt a (fst p) (snd p)) l (OK s) = OK s' ->
      forall pc i, ~ In pc (map fst l) -> (st_code s)!pc = Some i -> Plt pc (st_nextnode s) -> (st_code s')!pc = Some i.

  Lemma elements_complete:
    forall f pc,
      In pc (map fst (PTree.elements (fn_code f))) ->
      Ple pc (max_pc_function f).
      
  Lemma transf_function_new_entrypoint:
    forall f tf,
      transf_function prog ge STK SIZE f = OK tf ->
      exists r r' r'' pc1 pc2 pc3 pc4 pc5 pc6,
        Plt (max_reg_function f) r /\
        Plt r r' /\
        Plt r' r'' /\
        (fn_code tf)!(fn_entrypoint tf) = Some (Iload (xH, nil) Mint32 (Aglobal SIZE Int.zero) nil r pc1) /\
        (fn_code tf)!pc1 = Some (Iop (Oaddimm (Int.repr 4)) (r::nil) r pc2) /\
        (fn_code tf)!pc2 = Some (Istore (xH, nil) Mint32 (Aglobal SIZE Int.zero) nil r pc3) /\
        (fn_code tf)!pc3 = Some (Iload (xH, nil) Mint32 (Aglobal SIZE Int.zero) nil r' pc4) /\
        (fn_code tf)!pc4 = Some (Iop (Olea (Ainstack Int.zero)) nil r'' pc5) /\
        (fn_code tf)!pc5 = Some (Istore (xH, nil) Mint32 (Abased STK Int.zero) (r'::nil) r'' pc6) /\
        (fn_code tf)!pc6 = Some (Inop (fn_entrypoint f)).
  
  Lemma init_regs_inject:
    forall j args targs,
      Val.inject_list j args targs ->
      forall params r, Val.inject j (init_regs args params)#r (init_regs targs params)#r.

  Lemma pop_length:
    forall l n x,
      pop n l = Some x ->
      (n < length l)%nat.

  Lemma pop_implies:
    forall l n x,
      pop n l = Some x ->
      exists y, pop 0 l = Some y.

  Lemma STK_not_SIZE:
    forall bSTK bSIZE,
      Genv.find_symbol tge STK = Some bSTK ->
      Genv.find_symbol tge SIZE = Some bSIZE ->
      bSTK <> bSIZE.
  
  Lemma FSIM_implies:
    forall s1 s2 t,
      initial_state prog s1 ->
      star step_block' ge s1 t s2 ->
      star step ge s1 t s2.
    
  Lemma initial_states_exist:
    forall s1,
      initial_state tprog s1 -> exists s2, initial_state prog s2.

  Lemma not_fresh_find_symbol_ind:
    forall (F V: Type) gl (ge0: Genv.t F V),
      (forall b, Plt b (Genv.genv_next ge0) -> exists id, Genv.find_symbol ge0 id = Some b /\ ~ In id (map fst gl)) ->
      list_norepet (map fst gl) ->
      (forall ge id g gl1 gl2 , In (id, g) gl ->
                           map fst gl = gl1 ++ (id::gl2) ->
                           (forall b, Plt b (Genv.genv_next ge) -> exists id', Genv.find_symbol ge id' = Some b /\ ~ In id' (id::gl2)) ->
                           (forall b, Plt b (Genv.genv_next (Genv.add_global ge (id, g))) -> exists id', Genv.find_symbol (Genv.add_global ge (id, g)) id' = Some b /\ ~ In id' gl2)) ->
      forall b, Plt b (Genv.genv_next (Genv.add_globals ge0 gl)) -> exists id, Genv.find_symbol (Genv.add_globals ge0 gl) id = Some b.
  
  Lemma not_fresh_find_symbol:
    forall (F V: Type) (p: AST.program F V) (b: block),
      list_norepet (map fst (prog_defs p)) ->
      Plt b (Genv.genv_next (Genv.globalenv p)) ->
      exists id, Genv.find_symbol (Genv.globalenv p) id = Some b.
  
  Lemma initial_states_match:
    forall s1 s2,
      initial_state tprog s1 ->
      initial_state prog s2 ->
      exists s1', initial_state tprog s1' /\ match_states s2 s1'.

  Lemma transf_function_inv_aux:
    forall opt l s s' pc i,
      fold_left (fun acc pc_i => transf_instr prog ge STK SIZE opt acc (fst pc_i) (snd pc_i)) l (OK s) = OK s' ->
      In (pc, i) l ->
      exists s1 s2, transf_instr prog ge STK SIZE opt (OK s1) pc i = OK s2.

  Lemma transf_function_inv:
    forall f tf pc i,
      transf_function prog ge STK SIZE f = OK tf ->
      (fn_code f)!pc = Some i ->
      exists s s', transf_instr prog ge STK SIZE (sig_res (fn_sig f)) (OK s) pc i = OK s'.

  Lemma addr_of_local_exists:
    forall n kappa ofs sp,
    exists vptrs, addr_of_local kappa sp ofs n vptrs.

  Lemma addr_of_global_exists:
    forall b kappa n ofs,
    exists vptrs, addr_of_global kappa b ofs n vptrs.

  Lemma addr_of_local_translated':
    forall kappa j sp tsp n ofs tvals,
      j sp = Some (tsp, 0) ->
      addr_of_local kappa (Vptr tsp Int.zero) ofs n tvals ->
      exists vals, addr_of_local kappa (Vptr sp Int.zero) ofs n vals /\ list_forall2 (Val.inject j) vals tvals.

  Lemma addr_of_global_translated':
    forall kappa j b n ofs tvals,
      j b = Some (b, 0) ->
      addr_of_global kappa b ofs n tvals ->
      exists vals, addr_of_global kappa b ofs n vals /\ list_forall2 (Val.inject j) vals tvals.

  Lemma pop_inject':
    forall P sps tsps,
      list_forall2 P sps tsps ->
      forall tsp n, pop n tsps = Some tsp ->
               exists sp, pop n sps = Some sp /\
                     P sp tsp.

  Lemma addr_of_annotations_translated':
    forall kappa j sps tsps alpha tvals,
      list_forall2 (fun sp tsp => exists bsp btsp, sp = Vptr bsp Int.zero /\ tsp = Vptr btsp Int.zero /\ j bsp = Some (btsp, 0)) sps tsps ->
      (forall b id, Genv.find_symbol ge id = Some b -> j b = Some (b, 0)) ->
      (forall id range, In (ABglobal id range) alpha -> id <> STK /\ id <> SIZE) ->
      addr_of_annotations kappa tge tsps alpha tvals ->
      exists vals, addr_of_annotations kappa ge sps alpha vals /\ list_forall2 (Val.inject j) vals tvals.

  Lemma unsigned_p1:
    forall i, exists p, Int.unsigned i + 1 = Z.pos p.

  Lemma tr_local_regs_star:
    forall kappa sp stk f tf n ofs depth pc1 regs regs' pc2 pcs trs m,
      (forall s0, initial_state tprog s0 -> exists t : trace, star step tge s0 t (State stk tf sp pc1 trs m)) ->
      tr_local_regs STK kappa f (fn_code tf) pc1 ofs depth n regs regs' pc2 pcs ->
      exists trs', star step tge (State stk tf sp pc1 trs m) E0 (State stk tf sp pc2 trs' m).

  Lemma tr_global_regs_star:
    forall kappa sp stk f tf id n ofs pc1 regs pc2 pcs trs m,
      (forall s0, initial_state tprog s0 -> exists t : trace, star step tge s0 t (State stk tf sp pc1 trs m)) ->
      tr_global_regs kappa f (fn_code tf) pc1 id ofs n regs pc2 pcs ->
      exists trs', star step tge (State stk tf sp pc1 trs m) E0 (State stk tf sp pc2 trs' m).

  Lemma tr_regs_annot_star:
    forall kappa sp stk f tf alpha pc1 regs regs' pc2 pcs trs m,
      (forall s0, initial_state tprog s0 -> exists t : trace, star step tge s0 t (State stk tf sp pc1 trs m)) ->
      tr_regs_annot prog STK kappa f (fn_code tf) pc1 alpha regs regs' pc2 pcs ->
      exists trs', star step tge (State stk tf sp pc1 trs m) E0 (State stk tf sp pc2 trs' m).

  Lemma mod_neg:
    forall a b,
      b > 0 ->
      -b <= a < 0 ->
      a mod b = a + b.

  Lemma tr_local_regs_inv:
    forall kappa f n pc1 base depth regs regs' pc2 pcs stk tf tsp trs m,
      tr_local_regs STK kappa f (fn_code tf) pc1 base depth n regs regs' pc2 pcs ->
      (depth < 128)%nat ->
      shadowstack_is_sound (tsp::map (fun s => match s with | Stackframe _ _ sp _ _ => sp end) stk) m ->
      (exists x, In x (int_ranges n base) /\ ((align_chunk kappa) | x)) ->
      (forall s0, initial_state tprog s0 -> exists t : trace, star step tge s0 t (State stk tf tsp pc1 trs m)) ->
      (forall bSTK, Genv.find_symbol tge STK = Some bSTK -> forall ofs : Z, Mem.perm m bSTK ofs Cur Readable <-> 0 <= ofs < 512) ->
      exists sp, pop depth (tsp::map (fun s => match s with | Stackframe _ _ sp _ _ => sp end) stk) = Some sp.

  Lemma tr_regs_annot_inv:
    forall kappa sp stk f tf alpha pc1 regs regs' pc2 pcs trs m
      (Hex: 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)),
      (forall ptr, In ptr (sp::map (fun s => match s with | Stackframe _ _ sp _ _ => sp end) stk) ->
              exists b, ptr = Vptr b Int.zero) ->
      tr_regs_annot prog STK kappa f (fn_code tf) pc1 alpha regs regs' pc2 pcs ->
      shadowstack_is_sound (sp::map (fun s => match s with | Stackframe _ _ sp _ _ => sp end) stk) m ->
      (forall depth varname range, In (ABlocal depth varname range) alpha -> (depth < 128)%nat) ->
      (forall id range, In (ABglobal id range) alpha -> id <> STK /\ id <> SIZE) ->
      (forall s0, initial_state tprog s0 -> exists t : trace, star step tge s0 t (State stk tf sp pc1 trs m)) ->
      (forall bSTK, Genv.find_symbol tge STK = Some bSTK -> forall ofs : Z, Mem.perm m bSTK ofs Cur Readable <-> 0 <= ofs < 512) ->
      exists vals, addr_of_annotations kappa tge (sp::map (fun s => match s with | Stackframe _ _ sp _ _ => sp end) stk) alpha vals.

  Lemma valid_pointer_inject_inv:
    forall j m1 m2,
      Mem.inject j m1 m2 ->
      (forall b b' delta, j b = Some (b', delta) -> delta = 0) ->
      (forall b b' o k p, j b = Some (b', 0) -> (Mem.perm m1 b o k p <-> Mem.perm m2 b' o k p)) ->
      forall b b', j b = Some (b', 0) -> forall ofs, Mem.valid_pointer m2 b' ofs = Mem.valid_pointer m1 b ofs.
  
  Lemma eval_condition_translated':
    forall j a ta ofsa tofsa m tm tvals vals,
      Val.inject j (Vptr a ofsa) (Vptr ta tofsa) ->
      Mem.inject j m tm ->
      list_forall2 (Val.inject j) vals tvals ->
      (forall v : val, In v tvals -> exists (b : block) (ofs : int), v = Vptr b ofs) ->
      (forall b b' delta, j b = Some (b', delta) -> delta = 0) ->
      (forall b b1 b2, j b1 = Some (b, 0) -> j b2 = Some (b, 0) -> b1 = b2) ->
      (forall b b' o k p, j b = Some (b', 0) -> (Mem.perm m b o k p <-> Mem.perm tm b' o k p)) ->
      (forall (tb : block) (tofs : int),
          In (Vptr tb tofs) tvals ->
          eval_condition (Ccompu Ceq) ((Vptr ta tofsa) :: Vptr tb tofs :: nil) tm = Some true \/
          eval_condition (Ccompu Ceq) ((Vptr ta tofsa) :: Vptr tb tofs :: nil) tm = Some false) ->
      forall (b : block) (ofs : int),
        In (Vptr b ofs) vals ->
        eval_condition (Ccompu Ceq) ((Vptr a ofsa) :: Vptr b ofs :: nil) m = Some true \/
        eval_condition (Ccompu Ceq) ((Vptr a ofsa) :: Vptr b ofs :: nil) m = Some false.

  Lemma eval_condition_is_true_implies:
    forall a b m,
      Val.of_optbool (eval_condition (Ccompu Ceq) (a :: b :: nil) m) = Vtrue ->
      a = b.
  
  Lemma valid_access_in_bounds_invariant:
    forall p, list_norepet (prog_defs_names p) ->
         MoreSemantics.invariant (semantics p) (fun x => MoreRTL.valid_access_in_bounds p (MoreRTL.mem_of_state x)).

  Lemma range_leb_spec:
    forall a1 a2 b1 b2,
      range_leb (a1, a2) (b1, b2) = true ->
      Int.unsigned b1 <= Int.unsigned a1 /\ Int.unsigned a2 <= Int.unsigned b2.

  Opaque range_leb.

  Lemma addr_of_local_determ:
    forall kappa sp n base vals vals',
      addr_of_local kappa sp base n vals ->
      addr_of_local kappa sp base n vals' ->
      vals = vals'.

  Lemma addr_of_global_determ:
    forall kappa id n ofs vals vals',
      addr_of_global kappa id ofs n vals ->
      addr_of_global kappa id ofs n vals' ->
      vals = vals'.

  Lemma addr_of_annotations_determ:
    forall kappa ge sps alpha vals vals',
      addr_of_annotations kappa ge sps alpha vals ->
      addr_of_annotations kappa ge sps alpha vals' ->
      vals = vals'.

  Lemma load_align_chunk:
    forall kappa m b ofs v,
      Mem.load kappa m b ofs = Some v ->
      (align_chunk kappa | ofs).

  Lemma store_align_chunk:
    forall kappa m b ofs v m',
      Mem.store kappa m b ofs v = Some m' ->
      (align_chunk kappa | ofs).

  Lemma sizeof_prog:
    forall id,
      MoreRTL.sizeof prog id <= Int.max_unsigned.
  
  Lemma is_trivial_annotation_load_correct:
    forall s ts f tf sp tsp pc rs trs m tm alpha kappa addr args dst pc' a v,
      match_states (State s f sp pc rs m) (State ts tf tsp pc trs tm) ->
      MoreRTL.is_trivial_annotation prog alpha kappa addr = true ->
      (fn_code f)!pc = Some (Iload alpha kappa addr args dst pc') ->
      eval_addressing ge sp addr (rs##args) = Some a ->
      Mem.loadv kappa m a = Some v ->
      exists vals, addr_of_annotations kappa ge (sp::map (fun s => match s with | Stackframe _ _ sp _ _ => sp end) s) (snd alpha) vals /\
              (match snd alpha with | nil => True | _ => In a vals end).

  Lemma is_trivial_annotation_store_correct:
    forall s ts f tf sp tsp pc rs trs m tm alpha kappa addr args src pc' a m',
      match_states (State s f sp pc rs m) (State ts tf tsp pc trs tm) ->
      MoreRTL.is_trivial_annotation prog alpha kappa addr = true ->
      (fn_code f)!pc = Some (Istore alpha kappa addr args src pc') ->
      eval_addressing ge sp addr (rs##args) = Some a ->
      Mem.storev kappa m a (rs#src) = Some m' ->
      exists vals, addr_of_annotations kappa ge (sp::map (fun s => match s with | Stackframe _ _ sp _ _ => sp end) s) (snd alpha) vals /\
              (match snd alpha with | nil => True | _ => In a vals end).

  Lemma load_step:
    forall s ts f tf sp tsp pc rs trs m tm alpha kappa addr args dst pc' a v vals (Htriv: MoreRTL.is_trivial_annotation prog alpha kappa addr = false) (Hsingleton: is_singleton (snd alpha) = false),
      match_states (State s f sp pc rs m) (State ts tf tsp pc trs tm) ->
      (fn_code f)!pc = Some (Iload alpha kappa addr args dst pc') ->
      eval_addressing ge sp addr (rs##args) = Some a ->
      Mem.loadv kappa m a = Some v ->
      addr_of_annotations kappa ge (sp::map (fun s => match s with | Stackframe _ _ sp _ _ => sp end) s) (snd alpha) vals ->
      ((forall b ofs, In (Vptr b ofs) vals -> (eval_condition (Ccompu Ceq) (a::(Vptr b ofs)::nil) m = Some true \/ eval_condition (Ccompu Ceq) (a::(Vptr b ofs)::nil) m = Some false)) /\ (match snd alpha with | nil => True | _ => In a vals end)).

  Lemma store_step:
    forall s ts f tf sp tsp pc rs trs m tm alpha kappa addr args src pc' a m' vals (Htriv: MoreRTL.is_trivial_annotation prog alpha kappa addr = false) (Hsingleton: is_singleton (snd alpha) = false),
      match_states (State s f sp pc rs m) (State ts tf tsp pc trs tm) ->
      (fn_code f)!pc = Some (Istore alpha kappa addr args src pc') ->
      eval_addressing ge sp addr (rs##args) = Some a ->
      Mem.storev kappa m a (rs#src) = Some m' ->
      addr_of_annotations kappa ge (sp::map (fun s => match s with | Stackframe _ _ sp _ _ => sp end) s) (snd alpha) vals ->
      ((forall b ofs, In (Vptr b ofs) vals -> (eval_condition (Ccompu Ceq) (a::(Vptr b ofs)::nil) m = Some true \/ eval_condition (Ccompu Ceq) (a::(Vptr b ofs)::nil) m = Some false)) /\ (match snd alpha with | nil => True | _ => In a vals end)).

  Lemma tr_local_regs_inv_singleton:
    forall f pc1 base bound depth regs regs' pc2 pcs stk tf tsp trs m,
      tr_local_regs' STK f (fn_code tf) pc1 depth base bound regs regs' pc2 pcs ->
      (depth < 128)%nat ->
      shadowstack_is_sound (tsp::map (fun s => match s with | Stackframe _ _ sp _ _ => sp end) stk) m ->
      (forall s0, initial_state tprog s0 -> exists t : trace, star step tge s0 t (State stk tf tsp pc1 trs m)) ->
      (forall bSTK, Genv.find_symbol tge STK = Some bSTK -> forall ofs : Z, Mem.perm m bSTK ofs Cur Readable <-> 0 <= ofs < 512) ->
      exists sp, pop depth (tsp::map (fun s => match s with | Stackframe _ _ sp _ _ => sp end) stk) = Some sp.

  Lemma tr_local_regs_star_singleton:
    forall sp stk f tf base bound depth pc1 regs regs' pc2 pcs trs m,
      (forall s0, initial_state tprog s0 -> exists t : trace, star step tge s0 t (State stk tf sp pc1 trs m)) ->
      tr_local_regs' STK f (fn_code tf) pc1 depth base bound regs regs' pc2 pcs ->
      exists trs', star step tge (State stk tf sp pc1 trs m) E0 (State stk tf sp pc2 trs' m).

  Lemma tr_global_regs_star_singleton:
    forall sp stk f tf id base bound pc1 regs pc2 pcs trs m,
      (forall s0, initial_state tprog s0 -> exists t : trace, star step tge s0 t (State stk tf sp pc1 trs m)) ->
      tr_global_regs' f (fn_code tf) pc1 id base bound regs pc2 pcs ->
      exists trs', star step tge (State stk tf sp pc1 trs m) E0 (State stk tf sp pc2 trs' m).

  Lemma tr_regs_annot_inv_singleton:
    forall kappa sp stk f tf alpha pc1 regs regs' pc2 pcs trs m
      (Hex: check_annotations_divides kappa alpha = OK tt),
      (forall ptr, In ptr (sp::map (fun s => match s with | Stackframe _ _ sp _ _ => sp end) stk) ->
              exists b, ptr = Vptr b Int.zero) ->
      tr_regs_annot' prog STK f (fn_code tf) pc1 alpha regs regs' pc2 pcs ->
      shadowstack_is_sound (sp::map (fun s => match s with | Stackframe _ _ sp _ _ => sp end) stk) m ->
      (forall depth varname range, In (ABlocal depth varname range) alpha -> (depth < 128)%nat) ->
      (forall id range, In (ABglobal id range) alpha -> id <> STK /\ id <> SIZE) ->
      (forall s0, initial_state tprog s0 -> exists t : trace, star step tge s0 t (State stk tf sp pc1 trs m)) ->
      (forall bSTK, Genv.find_symbol tge STK = Some bSTK -> forall ofs : Z, Mem.perm m bSTK ofs Cur Readable <-> 0 <= ofs < 512) ->
      exists vals, addr_of_annotations_singleton tge (sp::map (fun s => match s with | Stackframe _ _ sp _ _ => sp end) stk) alpha vals.

  Inductive match_vals j: (val + val * val) -> (val + val * val) -> Prop :=
  | match_vals_intro1:
      forall v tv,
        Val.inject j v tv ->
        match_vals j (inl v) (inl tv)
  | match_vals_intro2:
      forall v1 v2 tv1 tv2,
        Val.inject j v1 tv1 ->
        Val.inject j v2 tv2 ->
        match_vals j (inr (v1, v2)) (inr (tv1, tv2)).

  Lemma addr_of_annotations_translated_singleton:
    forall j sps tsps alpha tvals,
      list_forall2 (fun sp tsp => exists bsp btsp, sp = Vptr bsp Int.zero /\ tsp = Vptr btsp Int.zero /\ j bsp = Some (btsp, 0)) sps tsps ->
      (forall b id, Genv.find_symbol ge id = Some b -> j b = Some (b, 0)) ->
      (forall id range, In (ABglobal id range) alpha -> id <> STK /\ id <> SIZE) ->
      addr_of_annotations_singleton tge tsps alpha tvals ->
      exists vals, addr_of_annotations_singleton ge sps alpha vals /\ list_forall2 (match_vals j) vals tvals.

  Lemma addr_of_annotations_singleton_determ:
    forall ge sps alpha vals1,
      addr_of_annotations_singleton ge sps alpha vals1 ->
      forall vals2, addr_of_annotations_singleton ge sps alpha vals2 ->
      vals1 = vals2.

  Lemma int_ranges_spec:
    forall n base x,
      Int.unsigned base + Z.of_nat n < Int.modulus ->
      In x (int_ranges n base) ->
      exists y, x = Int.unsigned y /\ Int.unsigned base <= x < Int.unsigned base + Z.of_nat n.

  Lemma check_annotations_divides_spec_2:
    forall kappa alpha x,
      check_annotations_divides kappa alpha = OK x ->
      (forall id base bound, In (ABglobal id (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 addr_of_annotations_singleton_implies:
    forall kappa ge sps alpha vals' (Hdivides: check_annotations_divides kappa alpha = OK tt),
      (forall sp, In sp sps -> exists b, sp = Vptr b Int.zero) ->
      check_annotations_range alpha = OK tt ->
      addr_of_annotations_singleton ge sps alpha vals' ->
      exists vals,
        addr_of_annotations kappa ge sps alpha vals /\
        (forall b ofs,
            In (Vptr b ofs) vals ->
            In (inl (Vptr b ofs)) vals' \/
            (exists ofs1 ofs2,
                In (inr (Vptr b ofs1, Vptr b ofs2)) vals' /\ Int.unsigned ofs1 <= Int.unsigned ofs <= Int.unsigned ofs2)) /\
        (forall v,
            In v vals' ->
            match v with
            | inl (Vptr b ofs) => In (Vptr b ofs) vals
            | inr (Vptr b ofs1, Vptr b' ofs2) => b = b' /\ exists ofs, In (Vptr b ofs) vals /\ Int.unsigned ofs1 <= Int.unsigned ofs <= Int.unsigned ofs2
            | _ => False
            end).

  Lemma valand_true:
    forall x y,
      Val.and (Val.of_optbool x) (Val.of_optbool y) = Vtrue ->
      Val.of_optbool x = Vtrue /\ Val.of_optbool y = Vtrue.

  Lemma valand_false:
    forall x y,
      Val.and (Val.of_optbool x) (Val.of_optbool y) = Vfalse ->
      Val.of_optbool x = Vfalse \/ Val.of_optbool y = Vfalse.

  Lemma optbool_true:
    forall x,
      Val.of_optbool x = Vtrue <-> x = Some true.

  Lemma optbool_false:
    forall x,
      Val.of_optbool x = Vfalse <-> x = Some false.

  Axiom valid_ptr_connected:
    forall m b ofs1 ofs2,
      Mem.valid_pointer m b ofs1 = true ->
      Mem.valid_pointer m b ofs2 = true ->
      forall ofs, ofs1 <= ofs <= ofs2 ->
             Mem.valid_pointer m b ofs = true.

  Lemma weak_valid_ptr_connected:
    forall m b ofs1 ofs2,
      Mem.weak_valid_pointer m b ofs1 = true ->
      Mem.weak_valid_pointer m b ofs2 = true ->
      forall ofs, ofs1 <= ofs <= ofs2 ->
             Mem.weak_valid_pointer m b ofs = true.

  Lemma singleton_true_false_implies:
    forall vals vals' a m,
      (forall b ofs,
          In (Vptr b ofs) vals ->
          In (inl (Vptr b ofs)) vals' \/
          (exists ofs1 ofs2,
              In (inr (Vptr b ofs1, Vptr b ofs2)) vals' /\ Int.unsigned ofs1 <= Int.unsigned ofs <= Int.unsigned ofs2)) ->
      (forall v, In v vals' ->
            match v with
            | inl v => Val.of_optbool (eval_condition (Ccompu Ceq) (v::a::nil) m) = Vtrue \/ Val.of_optbool (eval_condition (Ccompu Ceq) (v::a::nil) m) = Vfalse
            | inr (v, v') => Val.and (Val.of_optbool (Val.cmpu_bool (Mem.valid_pointer m) Cle v a)) (Val.of_optbool (Val.cmpu_bool (Mem.valid_pointer m) Cle a v')) = Vtrue \/ Val.and (Val.of_optbool (Val.cmpu_bool (Mem.valid_pointer m) Cle v a)) (Val.of_optbool (Val.cmpu_bool (Mem.valid_pointer m) Cle a v')) = Vfalse
            end) ->
      (forall b ofs,
          In (Vptr b ofs) vals ->
          eval_condition (Ccompu Ceq) (a :: Vptr b ofs :: nil) m = Some true \/
          eval_condition (Ccompu Ceq) (a :: Vptr b ofs :: nil) m = Some false).

  Lemma addr_of_annotations_singleton_in_implies:
    forall (ge : Genv.t fundef unit) (sps : list val) (alpha : list ablock) vals,
       addr_of_annotations_singleton ge sps alpha vals ->
       (forall sp : val, In sp sps -> exists b : block, sp = Vptr b Int.zero) ->
       forall v, In v vals -> match v with
                        | inl v =>
                          exists (b : block) (ofs : int),
                          v = Vptr b ofs /\
                          ((exists depth varname, nth_error sps depth = Some (Vptr b Int.zero) /\ In (ABlocal depth varname (ofs, ofs)) alpha) \/
                           (exists id, Genv.find_symbol ge id = Some b /\ In (ABglobal id (ofs, ofs)) alpha))
                        | inr (v, v') =>
                          exists (b : block) ofs1 ofs2,
                          v = Vptr b ofs1 /\ v' = Vptr b ofs2 /\
                          ((exists depth varname, nth_error sps depth = Some (Vptr b Int.zero) /\ In (ABlocal depth varname (ofs1, ofs2)) alpha) \/
                           (exists id, Genv.find_symbol ge id = Some b /\ In (ABglobal id (ofs1, ofs2)) alpha))
                        end.

  Lemma cmpu_bool_cle_true_implies:
    forall m b b' ofs ofs',
      Val.cmpu_bool (Mem.valid_pointer m) Cle (Vptr b ofs) (Vptr b' ofs') = Some true ->
      b = b' /\ Int.unsigned ofs <= Int.unsigned ofs'.

  Lemma addr_of_annotations_singleton_translated':
    forall j sps tsps alpha tvals,
      list_forall2 (fun sp tsp => exists bsp btsp, sp = Vptr bsp Int.zero /\ tsp = Vptr btsp Int.zero /\ j bsp = Some (btsp, 0)) sps tsps ->
      (forall b id, Genv.find_symbol ge id = Some b -> j b = Some (b, 0)) ->
      (forall id range, In (ABglobal id range) alpha -> id <> STK /\ id <> SIZE) ->
      addr_of_annotations_singleton tge tsps alpha tvals ->
      exists vals, addr_of_annotations_singleton ge sps alpha vals /\ list_forall2 (match_vals j) vals tvals.

  Lemma addr_of_annotations_singleton_translated:
    forall j sps tsps alpha vals,
      list_forall2 (fun sp tsp => exists bsp btsp, sp = Vptr bsp Int.zero /\ tsp = Vptr btsp Int.zero /\ j bsp = Some (btsp, 0)) sps tsps ->
      (forall b id, Genv.find_symbol ge id = Some b -> j b = Some (b, 0)) ->
      (forall id range, In (ABglobal id range) alpha -> id <> STK /\ id <> SIZE) ->
      addr_of_annotations_singleton ge sps alpha vals ->
      exists tvals, addr_of_annotations_singleton tge tsps alpha tvals /\ list_forall2 (match_vals j) vals tvals.

  Lemma load_step_singleton:
    forall s ts f tf sp tsp pc rs trs m tm alpha kappa addr args dst pc' a v vals (Htriv: MoreRTL.is_trivial_annotation prog alpha kappa addr = false) (Hsingleton: is_singleton (snd alpha) = true),
      match_states (State s f sp pc rs m) (State ts tf tsp pc trs tm) ->
      (fn_code f)!pc = Some (Iload alpha kappa addr args dst pc') ->
      eval_addressing ge sp addr (rs##args) = Some a ->
      Mem.loadv kappa m a = Some v ->
      addr_of_annotations_singleton ge (sp::map (fun s => match s with | Stackframe _ _ sp _ _ => sp end) s) (snd alpha) vals ->
      annot_sem (Genv.find_symbol ge) (sp::map (fun s => match s with | Stackframe _ _ sp _ _ => sp end) s) (snd alpha) a.

  Lemma store_step_singleton:
    forall s ts f tf sp tsp pc rs trs m m' tm alpha kappa addr args src pc' a vals (Htriv: MoreRTL.is_trivial_annotation prog alpha kappa addr = false) (Hsingleton: is_singleton (snd alpha) = true),
      match_states (State s f sp pc rs m) (State ts tf tsp pc trs tm) ->
      (fn_code f)!pc = Some (Istore alpha kappa addr args src pc') ->
      eval_addressing ge sp addr (rs##args) = Some a ->
      Mem.storev kappa m a rs#src = Some m' ->
      addr_of_annotations_singleton ge (sp::map (fun s => match s with | Stackframe _ _ sp _ _ => sp end) s) (snd alpha) vals ->
      annot_sem (Genv.find_symbol ge) (sp::map (fun s => match s with | Stackframe _ _ sp _ _ => sp end) s) (snd alpha) a.

  Lemma load_checks_are_correct:
    forall stk f sp pc rs m tstk tf tsp tpc trs tm alpha kappa addr args dst pc' a v,
      match_states (State stk f sp pc rs m) (State tstk tf tsp tpc trs tm) ->
      (fn_code f)!pc = Some (Iload alpha kappa addr args dst pc') ->
      eval_addressing ge sp addr (rs##args) = Some a ->
      Mem.loadv kappa m a = Some v ->
      annot_sem (Genv.find_symbol ge)
                (sp :: map (fun s : stackframe => match s with
                                               | Stackframe _ _ sp _ _ => sp
                                               end) stk) (snd alpha) a ->
      exists s2', plus step tge (State tstk tf tsp tpc trs tm) E0 s2' /\
             match_states (State stk f sp pc' (rs#dst <- v) m) s2'.

  Lemma store_checks_are_correct:
    forall stk f sp pc rs m tstk tf tsp tpc trs tm alpha kappa addr args src pc' a m',
      match_states (State stk f sp pc rs m) (State tstk tf tsp tpc trs tm) ->
      (fn_code f)!pc = Some (Istore alpha kappa addr args src pc') ->
      eval_addressing ge sp addr (rs##args) = Some a ->
      Mem.storev kappa m a rs#src = Some m' ->
      annot_sem (Genv.find_symbol ge)
                (sp :: map (fun s : stackframe => match s with
                                               | Stackframe _ _ sp _ _ => sp
                                               end) stk) (snd alpha) a ->
      exists s2', plus step tge (State tstk tf tsp tpc trs tm) E0 s2' /\
             match_states (State stk f sp pc' rs m') s2'.

  Theorem simulation:
    forall s1 t s1', step_block' ge s1 t s1' ->
                forall s2, match_states s1 s2 ->
                      exists s2', plus step tge s2 t s2' /\ match_states s1' s2'.

  Theorem progress:
    forall s1 s2,
      match_states s1 s2 ->
      safe (RTL.semantics tprog) s2 ->
      (exists r, final_state s1 r) \/
      (exists t s1', Step (semantics_block' prog) s1 t s1').
            
  Lemma final_states_match:
    forall s1 s2 r,
      match_states s1 s2 ->
      final_state s1 r ->
      final_state s2 r.
  
  Theorem bsim:
    backward_simulation (RTL.semantics tprog) (semantics_block' prog).

End PRESERVATION.

Theorem def_program_safe_implies_annotations_correct:
  forall p tp,
    transf_program p = OK tp ->
    (forall beh, program_behaves (RTL.semantics p) beh -> not_wrong beh) ->
    (forall beh, program_behaves (RTL.semantics tp) beh -> not_wrong beh) ->
    forall beh, program_behaves (RTL.semantics_safe p) beh -> not_wrong beh.