Module ProductSimulation

Require VCGen.
Require RTLperm.
Require AssocList.
Import Sylvie.
Import Utf8.
Import Coqlib Maps.
Import Smallstep.
Import MoreRTL.
Import AST Globalenvs Memory Integers Floats Values.
Import RTL.
Import RTLperm.
Import Extra AssocList.
Import Product ProductProof.
Import MoreRelations.
Import MoreSemantics.

Lemma eq_fst {A B} {p: A * B} {a b} (H: p = (a, b)) : a = fst p.

Definition not_None_ex {X} (o: option X) :
  o ≠ None → ∃ x, o = Some x :=
  match o with
  | Some x => λ _, ex_intro _ x eq_refl
  | None => λ H, False_ind _ (H eq_refl)
  end.

Lemma list_norepet_rev {A} (m: list A) :
  list_norepet (rev m) → list_norepet m.

Lemma last_cons {A} {a d: A} {m: list A} :
  last (a :: m) d = last m a.

Section FL.
Context (A B C: Type) (f: C → A → B → C)
        (eA: C → list A → C) (eB: C → list B → C).
Inductive FoldLeft2 : list A → list B → C → C → Prop :=
| FLnil c : FoldLeft2 nil nil c c
| FLeA ma c `(match ma with nil => False | _ => True end) : FoldLeft2 ma nil c (eA c ma)
| FLeB mb c `(match mb with nil => False | _ => True end) : FoldLeft2 nil mb c (eB c mb)
| FL a ma b mb c d `(FoldLeft2 ma mb (f c a b) d) :
    FoldLeft2 (a :: ma) (b :: mb) c d
.

Lemma fold_left2P ma mb acc :
  FoldLeft2 ma mb acc (Util.fold_left2 f eA eB ma mb acc).

End FL.

Definition init_data_dec (i i': init_data) : { i = i' } + { i ≠ i' }.

Definition gvar_beq (v v': globvar unit) : bool :=
  let 'mkglobvar _ idl ro vol := v in
  let 'mkglobvar _ idl' ro' vol' := v' in
  if eqb ro ro'
  then if eqb vol vol'
       then if list_eq_dec init_data_dec idl idl'
            then true
            else false
       else false
  else false.

Lemma gvarP v v' : reflect (v = v') (gvar_beq v v').

Definition valid_pointer_of_permission (pe: perm_t) : block → Z → bool :=
  λ b o, Mem.perm_order'_dec (pe b o Cur) Nonempty.

Lemma valid_pointer_of_permission_ext pe m :
  pe =3 mem_perm m →
  ∀ b o, valid_pointer_of_permission pe b o = Mem.valid_pointer m b o.

Section REGISTER.

Context (reg: Type).
Context (reg_dec: EqDec reg).
Context (left right: Registers.reg → reg).
Context (ger: reg → Registers.reg + Registers.reg + unit).

Hypothesis ger_left : ∀ x, ger (left x) = inl (inl x).
Hypothesis ger_right : ∀ x, ger (right x) = inl (inr x).

Remark left_injective x y :
  left x = left y → x = y.

Remark right_injective x y :
  right x = right y → x = y.

Remark left_not_right x y :
  left x ≠ right y.

  Section SKIP_FAKE_BRANCHES.

    Context (funL funR: RTL.function) (funP: Sylvie.function reg).
    Context (ppmap: PPTree.t (list node)) (deco: hashmap (decoration reg)).
    Context (cps: code_product_spec reg left right funL funR funP ppmap deco).

    Definition is_fake (pc: pc_triple) : Prop :=
      ∃ pc', PPPTree.get pc (cut_points cps) = Some (FB pc').

    Variable pc: RTL.node * RTL.node.

    Remark skip_fake_branches'_decreases {π} π' :
      code_product_branch_witness_denote
        reg left right (fn_code funL) (fn_code funR) (Sylvie.fn_code funP) ppmap deco
        (pc, π) (FB π') →
      Plt (snd π') π.

    Definition get_fake (π: Sylvie.node) : { π' | PPPTree.get (pc, π) (cut_points cps) = Some (FB π') ∧ fake_branch reg (Sylvie.fn_code funP) ppmap (pc, π) π' } + { ¬ is_fake (pc, π) }.

    Fixpoint skip_fake_branches' (jumps: list node) (π: node) (H: Acc Plt π) {struct H} : node * list node :=
      let 'Acc_intro H' := H in
      match get_fake π with
      | inleft Fake =>
        let 'exist π' (conj Hw Hfake) := Fake in
        skip_fake_branches' (π :: jumps) (snd π') (H' _ (skip_fake_branches'_decreases π' Hfake))
      | inright _ => (π, jumps)
      end.

    Definition skip_fake_branches π : node * list node := skip_fake_branches' nil π (Plt_wf π).

    Fixpoint skip_fake_branches'_not_fake jumps π (H: Acc Plt π) {struct H} :
      ¬ is_fake (fst pc, snd pc, fst (skip_fake_branches' jumps π H)).

    Corollary skip_fake_branches_not_fake π :
      ¬ is_fake (fst pc, snd pc, fst (skip_fake_branches π)).

    Fixpoint goto_sequence (tgt: node) (seq: list node) : Prop :=
      match seq with
      | nil => True
      | src :: seq' =>
        (Sylvie.fn_code funP) ! src = Some (Egoto tgt) ∧ goto_sequence src seq'
      end.

    Fixpoint skip_fake_branches'_goto_sequence jumps π H {struct H} :
      let '(π', seq) := skip_fake_branches' jumps π H in
      goto_sequence π jumps →
      goto_sequence π' seq.

    Corollary skip_fake_branches_goto_sequence π :
      let '(π', seq) := skip_fake_branches π in
      goto_sequence π' seq.

    Fixpoint skip_fake_branches'_start jumps π H {struct H} :
      let '(π', seq) := skip_fake_branches' jumps π H in
      (seq = nil → jumps = nil) ∧ last seq π' = last jumps π.

    Corollary skip_fake_branches_start π :
      let '(π', seq) := skip_fake_branches π in
      last seq π' = π.

    Fixpoint skip_fake_branches'_cut_points jumps π (H: Acc Plt π) {struct H} :
      (fst pc, snd pc, π) ∈ keys (cut_points cps) →
      (fst pc, snd pc, fst (skip_fake_branches' jumps π H)) ∈ keys (cut_points cps).

    Corollary skip_fake_branches_cut_points π :
      (fst pc, snd pc, π) ∈ keys (cut_points cps) →
      (fst pc, snd pc, fst (skip_fake_branches π)) ∈ keys (cut_points cps).

  End SKIP_FAKE_BRANCHES.

  Arguments is_fake {_ _ _ _ _ } cps pc.
  Arguments skip_fake_branches {_ _ _ _ _} cps pc π.
  Arguments skip_fake_branches_goto_sequence {_ _ _ _ _} cps pc π.
  Arguments skip_fake_branches_start {_ _ _ _ _} cps pc π.
  Arguments skip_fake_branches_cut_points {_ _ _ _ _} cps pc π _ _.
  Arguments skip_fake_branches_not_fake {_ _ _ _ _} _ _ _ _.

Section RELATION.

  Context (find_symbol: ident → option block).

  Definition pred f : Sylvie.hashmap _ := Kildall.make_predecessors f RTL.successors_instr.

  Definition match_pc idx funL funR funP ppmap deco cps (pc pc' π: node) : Prop :=
      (pc, pc', π) ∈ keys (@cut_points reg left right funL funR funP ppmap deco cps) ∧
      get_height (cut_point_heights cps) (pc, pc', π) = idx.

  Definition match_function (funP: Sylvie.function reg) ppmap (deco: hashmap _) epa (fn fn': RTL.function)
    (cps: ProductProof.code_product_spec reg left right fn fn' funP ppmap deco)
    : Prop :=
    list_norepet (fn_params fn) ∧
    list_norepet (fn_params fn') ∧
    fn_stacksize fn = fn_stacksize fn' ∧
    ep_annot left right (fn_params fn) (fn_params fn') = Errors.OK epa ∧
    ∀ sp pe,
    well_annotated_function reg_dec find_symbol sp
                            (valid_pointer_of_permission pe) funP
                            (get_assertions deco)
                            (pre_of_assertion_list _ find_symbol sp (valid_pointer_of_permission pe) epa)
  .

  Definition match_fundef (f f': fundef) : Prop :=
    funsig f = funsig f' ∧
    match f, f' with
    | Internal fn, Internal fn' =>
      ∃ prod ppmap deco epa cps, match_function prod ppmap deco epa fn fn' cps
    | External ef, External ef' => ef = ef'
    | _, _ => False
    end.

  Definition match_sp (sp sp': Values.val) : Prop :=
    sp = sp'.

  Definition joint_regset (rs rs': regset) (x: reg) : Values.val :=
    match ger x with
    | inl (inl y) => PMap.get y rs
    | inl (inr y) => PMap.get y rs'
    | inr tt => Vundef
    end.

  Definition regset_agree (ρ: env reg) (ι: Registers.reg → reg) (rs: regset) : Prop :=
    ∀ r, rs !! r = ρ (ι r).

  Lemma regset_agree_map {ρ ι rs} :
    regset_agree ρ ι rs →
    ∀ m, map (λ r, rs !! r) m = map ρ (map ι m).

  Definition match_regset (sp: Values.val) epa (pe: perm_t) (fn: Sylvie.function reg) (π: node) (rs rs': regset) : Prop :=
  ∃ ρ : env reg,
    Sylvie.reachable reg_dec find_symbol sp (valid_pointer_of_permission pe) fn
                     (pre_of_assertion_list _ find_symbol sp (valid_pointer_of_permission pe) epa)
                     (Run (Sylvie.State π ρ))
    ∧ regset_agree ρ left rs
    ∧ regset_agree ρ right rs'
.

  Definition match_stackframe (s: RTLperm.stackframe) (s': RTL.stackframe) : Prop :=
    let 'RTLperm.SF pe (RTL.Stackframe r f sp pc rs) := s in
    let 'RTL.Stackframe r' f' sp' pc' rs' := s' in
    match_sp sp sp' ∧
    ∃ funP ppmap deco epa cps,
      match_function funP ppmap deco epa f f' cps ∧
      ∃ pc'' π' π'',
        right_branch reg right (RTL.fn_code f') (Sylvie.fn_code funP) ((pc, pc''), π'') ((pc, pc'), π') ∧
        (pc, pc'', π'') ∈ keys (cut_points cps) ∧
        ∀ v,
          match_regset sp epa pe funP π' (Registers.Regmap.set r v rs) (Registers.Regmap.set r' v rs').

  Inductive match_stack : list RTLperm.stackframe → list RTL.stackframe → Prop :=
  | MS_nil : match_stack nil nil
  | MS_push σ σ'
            `(match_stack σ σ')
            s s'
            `(match_stackframe s s')
    : match_stack (s :: σ) (s' :: σ')
  .

  Lemma match_stack_cons x stk stk' :
    match_stack (x :: stk) stk' →
    ∃ y stk'',
      stk' = y :: stk'' ∧
      match_stack stk stk'' ∧
      match_stackframe x y.

  Definition match_mem (m m': mem) : Prop :=
    m = m'.

  Definition match_args (args args': list val) : Prop :=
    Forall2 (λ a a', match a, a' with Vundef, _ | _, Vundef => Logic.True | _, _ => a = a' end)
            args args'.

  Definition match_state p (idx: nat) (x: RTLperm.state) (x': RTL.state) : Prop :=
    reachable (RTLperm.semantics p) x ∧
    match x with
    | RTLperm.State σ pe fn sp pc rs m =>
      match x' with
      | RTL.State σ' fn' sp' pc' rs' m' =>
        match_stack σ σ' ∧
        match_sp sp sp' ∧
        match_mem m m' ∧
        ∃ prod ppmap deco epa cps,
          match_function prod ppmap deco epa fn fn' cps ∧
          ∃ π, match_pc idx fn fn' prod ppmap deco cps pc pc' π ∧
               match_regset sp epa pe prod π rs rs' ∧
               ¬ is_fake cps (pc, pc', π)
      | _ => False
      end
    | RTLperm.Callstate σ fd args m =>
      match x' with
      | RTL.Callstate σ' fd' args' m' =>
        match_stack σ σ' ∧
        match_fundef fd fd' ∧
        args = args' ∧
        match_mem m m'
      | _ => False
      end
    | RTLperm.Returnstate σ v m =>
      match x' with
      | RTL.Returnstate σ' v' m' =>
        match_stack σ σ' ∧
        v = v' ∧
        match_mem m m'
      | _ => False
      end
    end.

End RELATION.

Unset Elimination Schemes.

Section Main.
  Import String.
  Import Errors.
  Local Open Scope error_monad_scope.

  Context (time : ∀ {A B: Type} (name: string) (f: A → B), A → B).
  Arguments time {A B} _ _ _.
  Hypothesis time_id : ∀ A B n (f: A → B) a, time n f a = f a.

  Context (reg_max: reg → reg → reg).
  Context (reg_succ: reg → reg).
  Context (reg_le: reg → reg → Prop).
  Hypothesis reg_le_refl : ∀ x, reg_le x x.
  Hypothesis reg_le_trans : ∀ x y z, reg_le x y → reg_le y z → reg_le x z.
  Hypothesis reg_max_le : ∀ x y z, reg_le z x ∨ reg_le z y → reg_le z (reg_max x y).
  Hypothesis reg_succ_le_ne : ∀ x y, reg_le x y → x ≠ reg_succ y.

  Context (progL progR : RTL.program).

  Context (fuel: nat).

  Let geL := Genv.globalenv progL.
  Let geR := Genv.globalenv progR.

  Let find_symbol: ident → option block := Senv.find_symbol geL.

Definition build (f1 f2: RTL.function) : Errors.res ({ pmd : _ & code_product_spec _ left right f1 f2 (fst (fst pmd)) (snd (fst pmd)) (snd pmd) } * _) :=
  let '(rel, pred1, pred2) := Rel.guess f1 f2 in
  do st <-
     time "Product generation"%string
     (mk_prod left right (RTL.fn_code f1) (RTL.fn_code f2) pred1 pred2
              (RTL.fn_entrypoint f1) (RTL.fn_entrypoint f2)
              init_state)
     fuel;
  do st <- add_invariants left right rel st;
  let f := Sylvie.Function st.(Product.code) xH in
  do cps <-
     time "Product validation"%string
     (validate _ _ left right f1 f2 f st.(ppmap) st.(deco) st.(hints))
     fuel;
  do epa <- ep_annot left right (RTL.fn_params f1) (RTL.fn_params f2);
  do vc <-
     time "VC generation"%string
       (VCGen.doit _ _ reg_max reg_succ st.(Product.code) st.(deco) epa)
       fuel;
  if vc
  then OK (existT _ (f, st.(ppmap), st.(deco)) cps, epa)
  else Error (msg "Cannot prove all VC")
.

Lemma build_correct f1 f2 funP ppmap deco cps epa :
  build f1 f2 = OK (existT _ (funP, ppmap, deco) cps, epa) →
  ep_annot left right (RTL.fn_params f1) (RTL.fn_params f2) = Errors.OK epa ∧
  ∀ sp pe,
    Sylvie.well_annotated_function
      _ find_symbol sp pe funP (get_assertions deco)
      (pre_of_assertion_list _ find_symbol sp pe epa).

  Context (print_product : ident → Sylvie.function reg → hashmap (decoration reg) → bool).

  Definition match_fundef_b (i: ident) (fd fd': fundef) : res unit :=
    do _ <- if eq_dec (funsig fd) (funsig fd') then OK tt else Error (msg "funsig mismatch");
    match fd, fd' with
    | Internal fn, Internal fn' =>
      do _ <- if list_norepet_dec eq_dec (fn_params fn) then OK tt else Error (msg "repet in params");
      do _ <- if list_norepet_dec eq_dec (fn_params fn') then OK tt else Error (msg "repet in params'");
      do _ <- if eq_dec (fn_stacksize fn) (fn_stacksize fn') then OK tt else Error (msg "stacksize mismatch");
      do p <- build fn fn';
      let '(existT (f, _, d) _, _) := p in
      if print_product i f d then OK tt else Error (msg "printer should return true")
    | External ef, External ef' => if eq_dec ef ef' then OK tt else Error (msg "external function mismatch")
    | _, _ => Error (msg "fundef mismatch")
    end.

  Lemma match_fundef_b_true i fd fd' :
    match_fundef_b i fd fd' = OK tt →
    match_fundef find_symbol fd fd'.

  Definition match_globdef (gd gd': ident * globdef fundef unit) : Prop :=
    let '(i, gd) := gd in
    let '(i', gd') := gd' in
    i = i' ∧
    match gd with
    | Gfun fn =>
      match gd' with
      | Gfun fn' => match_fundef find_symbol fn fn'
      | Gvar _ => False
      end
    | Gvar v => gd' = Gvar v
    end.

  Definition match_globdef_b (gd gd': ident * globdef fundef unit) : res unit :=
    let '(i, gd) := gd in
    let '(i', gd') := gd' in
    if ident_eq i i'
    then
      match gd, gd' with
      | Gfun fn, Gfun fn' => match_fundef_b i fn fn'
      | Gvar v, Gvar v' =>
        if gvar_beq v v' then OK tt else Error (msg "gvar mismatch")
      | _, _ => Error (msg "globdef mismatch")
      end
    else Error (msg "identifier mismatch in globdef").

  Definition match_globdef_b_true (gd gd': ident * globdef fundef unit) :
    match_globdef_b gd gd' = OK tt →
    match_globdef gd gd'.

  Definition forall2_res' {A B} (f: A → B → res unit) (m: list A) (n: list B) : res unit → res unit :=
    fold_left2 (λ r a b, do _ <- r; f a b)
               (λ _ _, Error (msg "list length mismatch"))
               (λ _ _, Error (msg "list length mismatch"))
               m n.

  Lemma forall2_res'_forall {A B} (f: A → B → res unit) m n i :
    match forall2_res' f m n i with
    | Error _ => True
    | OK _ => i = OK tt ∧ Forall2 (λ a b, f a b = OK tt) m n
    end.

  Definition forall2_res {A B} (f: A → B → res unit) (m: list A) (n: list B) : res unit :=
    forall2_res' f m n (OK tt).

  Lemma forall2_res_forall {A B} f (m: list A) (n: list B) u :
    forall2_res f m n = OK u →
    Forall2 (λ a b, f a b = OK tt) m n.

  Definition validate : res unit :=
    do _ <- if Pos.eqb (prog_main progR) (prog_main progL) then OK tt else Error (msg "main functions differ");
    do _ <- if proj_sumbool (list_eq_dec ident_eq (Genv.genv_public geR) (Genv.genv_public geL))
                            then OK tt else Error (msg "public symbols differ");
    do _ <- forall2_res match_globdef_b (prog_defs progL) (prog_defs progR);
    do _ <- if PTree.beq ident_eq (Genv.genv_symb geL) (Genv.genv_symb geR) then OK tt else Error (msg "symbols differ");
    if list_norepet_dec ident_eq (rev_map fst (prog_defs progL)) then OK tt else Error (msg "repet in prog defs").

  Hypothesis validated : validate = OK tt.

  Record hypotheses_t : Prop := {
      same_main: prog_main progR = prog_main progL;
      same_genv_public : Genv.genv_public geR = Genv.genv_public geL;
      same_prog_defs : Forall2 (λ a b, match_globdef_b a b = OK tt) (prog_defs progL) (prog_defs progR);
      same_find_symbol_L : ∀ s, Senv.find_symbol geL s = find_symbol s;
      same_find_symbol_R : ∀ s, Senv.find_symbol geR s = find_symbol s;
      defs_norepet_L : list_norepet (map fst (prog_defs progL));
      defs_norepet_R : list_norepet (map fst (prog_defs progR))
                               }.

  Lemma hypotheses : hypotheses_t.

  Global Opaque validate.

  Lemma same_find_symbol :
   ∀ s, Senv.find_symbol geR s = Senv.find_symbol geL s.

  Lemma same_public_symbols :
    ∀ s, Senv.public_symbol geR s = Senv.public_symbol geL s.

  Lemma match_genvs_is_implied:
    Genv.match_genvs (match_fundef find_symbol) (@eq _) nil geL geR.

  Lemma same_funs :
    ∀ s fd,
      (Genv.genv_funs geL) ! s = Some fd →
      ∃ fd',
        (Genv.genv_funs geR) ! s = Some fd' ∧
        match_fundef find_symbol fd fd'.

  Lemma same_volatiles b:
    Genv.block_is_volatile geR b = Genv.block_is_volatile geL b.

  Lemma symbol_preserved_L :
    ∀ s o, Genv.symbol_address geL s o = Sexpr.symbol_address find_symbol s o.

  Lemma symbol_preserved_R :
    ∀ s o, Genv.symbol_address geR s o = Sexpr.symbol_address find_symbol s o.

  Ltac precious i H :=
    assert (H := exist _ i eq_refl).

  Ltac mapeq :=
    repeat match goal with
           | H : _ ! _ = Some _, K : _ ! _ = Some _ |- _ =>
             rewrite H in K; eq_some_inv
           end.

  Lemma match_regset_egoto sp epa pe prod pc rs rs' pc' :
    match_regset find_symbol sp epa pe prod pc rs rs' →
    (Sylvie.fn_code prod) ! pc = Some (Sylvie.Egoto pc') →
    match_regset find_symbol sp epa pe prod pc' rs rs'.

  Lemma match_regset_goto_sequence sp epa pe prod seq rs rs' tgt :
    match_regset find_symbol sp epa pe prod (last seq tgt) rs rs' →
    goto_sequence prod tgt seq →
    match_regset find_symbol sp epa pe prod tgt rs rs'.

  Lemma match_eval_addressing (geX: Genv.t fundef unit) sp rs addr args v :
    (∀ s o, Genv.symbol_address geX s o = Sexpr.symbol_address find_symbol s o) →
    ∀ ρ ι,
      regset_agree ρ ι rs →
      ∀ pe,
        Op.eval_addressing geX sp addr (map (λ r, rs !! r) args) = Some v ↔
        Sexpr.eval_sexpr find_symbol sp pe ρ (Sexpr.Oper (Op.Olea addr) (map (Sexpr.Reg ∘ ι) args)) = Some v.

  Arguments match_eval_addressing [_ _ _ _ _ _] _ [ρ ι] _ _.

  Lemma match_eval_condition rs m cond args b :
    ∀ ρ ι,
      regset_agree ρ ι rs →
      Op.eval_condition cond (map (λ r, rs !! r) args) m = Some b ↔
      Sexpr.eval_condition (Mem.valid_pointer m) cond (map ρ (map ι args)) = Some b.

  Arguments match_eval_condition [_ _ _ _ _ ρ ι] _.

  Lemma match_eval_operation (geX: Genv.t fundef unit) sp rs m op args v :
    (∀ s o, Genv.symbol_address geX s o = Sexpr.symbol_address find_symbol s o) →
    ∀ ρ ι,
      regset_agree ρ ι rs →
      Op.eval_operation geX sp op (map (λ r, rs !! r) args) m = Some v ↔
      Sexpr.eval_operation find_symbol sp (Mem.valid_pointer m) op (map ρ (map ι args)) = Some v.

  Arguments match_eval_operation [_ _ _ _ _ _ _] _ [ρ ι] _.

  Lemma match_regset_eop_left sp epa pe prod pc rs rs' res op args m v pc' :
    match_regset find_symbol sp epa pe prod pc rs rs' →
    Op.eval_operation geL sp op (map (λ r, rs !! r) args) m = Some v →
    (Sylvie.fn_code prod) ! pc = Some (Sylvie.Eop (left res) (Operation op) (map left args) pc') →
    (∀ b o, valid_pointer_of_permission pe b o = Mem.valid_pointer m b o) →
    match_regset find_symbol sp epa pe prod pc' (Registers.Regmap.set res v rs) rs'.

  Lemma match_regset_eop_right sp epa pe prod pc rs rs' res op args m v pc' :
    match_regset find_symbol sp epa pe prod pc rs rs' →
    Op.eval_operation geR sp op (map (λ r, rs' !! r) args) m = Some v →
    (Sylvie.fn_code prod) ! pc = Some (Sylvie.Eop (right res) (Operation op) (map right args) pc') →
    (∀ b o, valid_pointer_of_permission pe b o = Mem.valid_pointer m b o) →
    match_regset find_symbol sp epa pe prod pc' rs (Registers.Regmap.set res v rs').

  Opaque is_dangerous.

  Local Open Scope string_scope.
  Lemma ep_annot_aux p p' acc :
    match fold_left2 (ep_annot_fun left right) (ep_annot_err _ "1") (ep_annot_err _ "2") p p' acc with
    | Errors.OK epa => ∀ a, In a epa →
                            match acc with Errors.OK acc => In a acc | _ => False end
                            ∨ ∃ n x x', nth_error p n = Some x ∧ nth_error p' n = Some x' ∧ a = Sexpr.assert_eq_reg (left x) (right x')
    | _ => True
    end.

  Lemma ep_annot_joint_regset params params' epa :
    list_norepet params →
    list_norepet params' →
    ep_annot left right params params' = Errors.OK epa →
    ∀ sp pe args,
      pre_of_assertion_list _ find_symbol sp pe epa (joint_regset (init_regs args params) (init_regs args params')).

  Hypothesis consistent_permissions : MoreSemantics.invariant (semantics progL) RTLperm.invariant.

  Lemma goto_sequence_reachable π gs sp vp prod pre ρ π' :
    goto_sequence prod π' gs →
    last gs π' = π →
    Sylvie.reachable reg_dec find_symbol sp vp prod pre (Run {| pc := π; e := ρ |}) →
    Sylvie.reachable reg_dec find_symbol sp vp prod pre (Run {| pc := π'; e := ρ |}).

  Lemma same_init_mem :
    Forall2 (λ x y, match_globdef_b x y = OK tt) (prog_defs progL) (prog_defs progR) →
    Genv.init_mem progL = Genv.init_mem progR.

  Lemma run_right_branch' stack pe epa rsL f sp rs m prod n to from :
    pe =3 mem_perm m →
    iter_rel n (right_branch_rel reg right (RTL.fn_code f) (Sylvie.fn_code prod)) to from →
    match_regset find_symbol sp epa pe prod (snd from) rsL rs →
    ∃ pcR' pc',
      to = (fst (fst from), pcR', pc') ∧
      ∃ rs',
        iter_rel' n (λ α, RTL.step geR α nil)
                 (RTL.State stack f sp (snd (fst from)) rs m) (RTL.State stack f sp pcR' rs' m) ∧
        match_regset find_symbol sp epa pe prod pc' rsL rs'.

  Lemma run_right_branch stack pe epa rsL f sp rs m prod to from :
    pe =3 mem_perm m →
    right_branch reg right (RTL.fn_code f) (Sylvie.fn_code prod) to from →
    match_regset find_symbol sp epa pe prod (snd from) rsL rs →
    ∃ pcR' pc',
      to = (fst (fst from), pcR', pc') ∧
      ∃ rs',
        star RTL.step geR (RTL.State stack f sp (snd (fst from)) rs m) nil (RTL.State stack f sp pcR' rs' m) ∧
        match_regset find_symbol sp epa pe prod pc' rsL rs'.

  Lemma right_branch_same_left {f p pc pc'} :
    right_branch reg right f p pc pc' →
    fst (fst pc) = fst (fst pc').

  Hypothesis external_calls_do_not_change_the_permissions :
    ∀ name sg args m tr vres m',
    Events.external_functions_sem name sg geL args m tr vres m' →
    mem_perm m =3 mem_perm m'.

  Lemma allowed_builtin_same_perm ef vargs m t vres m' :
    RTLperm.allowed_builtin ef = true →
    Events.external_call ef geL vargs m t vres m' →
    mem_perm m =3 mem_perm m'.

  Theorem simulation :
    forward_simulation (RTLperm.semantics progL) (RTL.semantics progR).

End Main.

End REGISTER.