Module IPCFCproof

Require Import Coqlib List Maps Integers.
Import ListNotations.
Require Import AST Linking Smallstep.
Require Import Globalenvs Values.
Require Import Op Registers Memory.
Require Import RTL RTLtyping.
Require Import CounterMeasures IPCFC.

Static specification

Definition gsr f := Pos.succ (max_reg_function f).
Definition gsrv f := Pos.succ (gsr f).
Definition rts f := Pos.succ (gsrv f).
Definition tmp1 f := Pos.succ (rts f).
Definition tmp2 f := Pos.succ (tmp1 f).
Definition tmp3 f := Pos.succ (tmp2 f).

Lemma transf_init_prot_entry:
  forall id f f',
    transf_function_init_prot id f = Errors.OK f' ->
    exists seq abort,
      transf_init_prot id f = Errors.OK seq
      /\ spec_seq abort (fn_code f') (fn_entrypoint f') seq CNoExit.

Lemma transf_prot_entry protected:
  forall id id' f f',
    harden_name id = Errors.OK id' ->
    transf_function_prot protected id f = Errors.OK f' ->
    exists abort,
      spec_seq abort (fn_code f') (fn_entrypoint f')
        (prot_prologue (gsr f) (gsrv f) (rts f) id')
        (COneExit (fn_entrypoint f))
    /\ (fn_code f')!abort = Some (Ibuiltin EF_cm_catch [] BR_none abort).

Lemma transf_prot_spec protected:
  forall id id' f f',
    harden_name id = Errors.OK id' ->
    transf_function_prot protected id f = Errors.OK f' ->
    forall pc i,
      (fn_code f) ! pc = Some i ->
      exists abort res,
        transf_partial_instr
          transf_partial_nop_default transf_partial_op_default
          transf_partial_load_default transf_partial_store_default
          (transf_call protected (gsr f) (gsrv f) (tmp1 f))
          (fun _ _ _ => Errors.Error (Errors.msg "IPCFC: tail calls are not allowed"))
          transf_partial_builtin_default
          transf_partial_cond_default transf_partial_jumptable_default
          (transf_return id' (gsr f) (gsrv f) (rts f)) i = Errors.OK res
        /\ spec_seq abort (fn_code f') pc (fst (projT2 res)) (snd (projT2 res)).

Additional lemmas

Lemma check_params_length: forall params sig tt,
    check_params params sig = Errors.OK tt ->
    length params = length (sig_args sig).

Lemma check_params_norepet : forall params sig tt,
    check_params params sig = Errors.OK tt ->
    list_norepet params.

Weaker match_prog This ones passes linking !

Definition is_transf_function_prot (p: RTL.program) id f f' : Prop :=
  exists prot,
    (forall id, prot!.id = Some tt -> (protected p)!.id = Some tt)
    /\ transf_function_prot prot id f = Errors.OK f'.

Inductive match_def (p tp: RTL.program) (id: qualident) : Prop :=
| match_def_none1 :
    (prog_defmap p)!.id = None ->
    (prog_defmap tp)!.id = None ->
    match_def p tp id
| match_def_none2 : forall id' f f',
    (prog_defmap p)!.id = None ->
    harden_name id' = Errors.OK id ->
    (prog_defmap p)!.id' = Some (Gfun (Internal f)) ->
    (protected p)!.id' = Some tt ->
    is_transf_function_prot p id' f f' ->
    (prog_defmap tp)!.id = Some (Gfun (Internal f')) ->
    match_def p tp id
| match_def_var : forall v,
    (prog_defmap p)!.id = Some (Gvar v) ->
    (prog_defmap tp)!.id = Some (Gvar v) ->
    match_def p tp id
| match_def_unprot: forall f,
    (protected p)!.id = None ->
    (prog_defmap p)!.id = Some (Gfun f) ->
    (prog_defmap tp)!.id = Some (Gfun f) ->
    match_def p tp id
| match_def_prot: forall id' f f1 f2,
    (protected p)!.id = Some tt ->
    harden_name id = Errors.OK id' ->
    (prog_defmap p)!.id = Some (Gfun (Internal f)) ->
    transf_function_init_prot id f = Errors.OK f1 ->
    (prog_defmap tp)!.id = Some (Gfun (Internal f1)) ->
    is_transf_function_prot p id f f2 ->
    (prog_defmap tp)!.id' = Some (Gfun (Internal f2)) ->
    match_def p tp id.

Global Hint Constructors match_def : ipcfc.
Global Hint Unfold is_transf_function_prot : ipcfc.

Record match_prog (p tp: program) : Prop := {
    match_prog_main: tp.(prog_main) = p.(prog_main);
    match_prog_public: tp.(prog_public) = p.(prog_public);
    match_prog_public_in: forall id, In id (prog_public p) -> In id (map fst (prog_defs p));
    match_prog_def: forall id, match_def p tp id;
    match_prog_inv: forall id id' tf,
      harden_name id' = Errors.OK id ->
      (prog_defmap tp)!.id = Some (Gfun (Internal tf)) ->
      exists f, (prog_defmap p)!.id' = Some (Gfun (Internal f));
    match_prog_wt: wt_program p;
    match_prog_norepet1: list_norepet (prog_defs_names p);
    match_prog_norepet2: list_norepet (prog_defs_names tp);
    match_prog_npref: forall id, In id (map fst (prog_defs p)) -> ~qualident_prefixed id ipcfc_pre;
  }.

Lemma transf_program_match:
  forall prog tprog, transf_program prog = Errors.OK tprog -> match_prog prog tprog.


Lemma of_succ_nat_pred_id : forall p,
    Pos.of_succ_nat (Nat.pred (Pos.to_nat p)) = p.

Lemma match_prog_var p tp (TRANSL: match_prog p tp) :
  forall id v,
    (prog_defmap p)!.id = Some (Gvar v) <->
    (prog_defmap tp)!.id = Some (Gvar v).

Lemma match_prog_qualident_is_prefix : forall p tp id,
    match_prog p tp ->
    In id (prog_defs_names tp) ->
    ~In id (prog_defs_names p) ->
    qualident_prefixed id ipcfc_pre.

Ltac qualident_not_prefix id :=
  unfold prog_defmap in *;
  repeat
    (match goal with
     | H:harden_name _ = Errors.OK id |- _ => eapply harden_name_qualident_prefix in H
     | H1:QITree.get id (QITree_Properties.of_list (prog_defs ?p)) = Some _,
         H2:forall id, In id (map fst (prog_defs ?p)) -> _ |- _ =>
         eapply H2; eauto; eapply in_map_iff; do 2 esplit; [|eauto using in_prog_defmap]; auto
     end).

Section IPCFC.

Fact fold_max_ge : forall xs x0,
    Forall (Pos.ge (fold_left Pos.max xs x0)) xs.

Variable p: program.
Variable tp: program.
Hypothesis TRANSL: match_prog p tp.
Let ge := Genv.globalenv p.
Let tge := Genv.globalenv tp.


Lemma match_prog_harden_name_inv : forall id id' g,
    harden_name id = Errors.OK id' ->
    (prog_defmap tp)!.id' = Some g ->
    exists f, (prog_defmap p)!.id = Some (Gfun (Internal f)).

Lemma transf_init_prot_sig:
  forall id f f',
    transf_function_init_prot id f = Errors.OK f' ->
    fn_sig f' = fn_sig f.

Lemma transf_prot_sig protected:
  forall id f f',
    transf_function_prot protected id f = Errors.OK f' ->
    fn_sig f' = transf_sig (fn_sig f).

Lemma transf_init_prot_params :
  forall id f f',
    transf_function_init_prot id f = Errors.OK f' ->
    fn_params f' = fn_params f.

Lemma transf_prot_params protected:
  forall id f f',
    transf_function_prot protected id f = Errors.OK f' ->
    fn_params f' = (gsr f)::(rts f)::fn_params f.

Fact transf_init_prot_stacksize : forall id f f',
    transf_function_init_prot id f = Errors.OK f' ->
    fn_stacksize f' = size_chunk Mint32.

Fact transf_prot_stacksize protected : forall id f f',
    transf_function_prot protected id f = Errors.OK f' ->
    fn_stacksize f' = fn_stacksize f.


Fact prog_public_iff : forall id v,
    Genv.find_symbol (Genv.globalenv p) id = Some v ->
    In id (filter (fun x1 : QualIdent.t => in_dec QualIdent.eq x1 (map fst (prog_defs p))) (prog_public p))
    <-> In id (prog_public p).

Lemma public_symbol_preserved:
  forall id,
    Senv.public_symbol (symbolenv (semantics tp)) id = Senv.public_symbol (symbolenv (semantics p)) id.


Lemma transform_find_symbol_1:
  forall id b,
  Genv.find_symbol ge id = Some b -> exists b', Genv.find_symbol tge id = Some b'.

Lemma find_funct_ptr_init_prot:
  forall id b f,
    Genv.find_symbol ge id = Some b ->
    Genv.find_funct_ptr ge b = Some f ->
  exists b',
    Genv.find_symbol tge id = Some b'
    /\ match (protected p)!.id with
      | Some _ =>
          exists f1 f2,
          f = Internal f1
          /\ transf_function_init_prot id f1 = Errors.OK f2
          /\ Genv.find_funct_ptr tge b' = Some (Internal f2)
      | None => Genv.find_funct_ptr tge b' = Some f
      end.

Lemma find_funct_ptr_prot :
  forall id b f,
    Genv.find_symbol ge id = Some b ->
    Genv.find_funct_ptr ge b = Some f ->
    match (protected p)!.id with
    | Some _ =>
        exists id' b' f1 f2,
        f = Internal f1
        /\ harden_name id = Errors.OK id'
        /\ is_transf_function_prot p id f1 f2
        /\ Genv.find_symbol tge id' = Some b'
        /\ Genv.find_funct_ptr tge b' = Some (Internal f2)
    | None => True
    end.

Semantic correctness

Inductive match_gdef id : globdef fundef unit -> globdef fundef unit -> Prop :=
| match_gdef_var : forall v,
    match_gdef id (Gvar v) (Gvar v)
| match_gdef_external : forall f,
    (protected p)!.id = None ->
    match_gdef id (Gfun f) (Gfun f)
| match_gdef_prot : forall id' f f' fc' b,
    (protected p)!.id = Some tt ->
    harden_name id = Errors.OK id' ->
    transf_function_init_prot id f = Errors.OK f' ->
    is_transf_function_prot p id f fc' ->
    Genv.find_symbol tge id' = Some b ->
    Genv.find_def tge b = Some (Gfun (Internal fc')) ->
    match_gdef id (Gfun (Internal f)) (Gfun (Internal f')).

Open Scope Z.

Record meminj_preserves_globals (f: meminj) : Prop := {
  symbols_inject_1: forall id b b' delta,
    f b = Some(b', delta) -> Genv.find_symbol ge id = Some b ->
    delta = 0 /\ Genv.find_symbol tge id = Some b';
  symbols_inject_2: forall id b,
    Genv.find_symbol ge id = Some b ->
    exists b', Genv.find_symbol tge id = Some b' /\ f b = Some(b', 0);
  defs_inject: forall id b b' delta gd,
      Genv.find_symbol ge id = Some b ->
      Genv.find_def ge b = Some gd ->
      f b = Some(b', delta) ->
      exists gd',
        Genv.find_symbol tge id = Some b'
        /\ Genv.find_def tge b' = Some gd'
        /\ match_gdef id gd gd'
        /\ delta = 0;
  defs_rev_inject: forall id b b' delta gd,
      Genv.find_symbol tge id = Some b' ->
      Genv.find_def tge b' = Some gd ->
      f b = Some(b', delta) ->
      exists gd',
        Genv.find_def ge b = Some gd'
        /\ match_gdef id gd' gd
        /\ delta = 0
}.

Lemma globals_symbols_inject:
  forall j, meminj_preserves_globals j -> Events.symbols_inject j ge tge.

Fact ptrofs_add_repr_zero : forall x,
  Ptrofs.add x (Ptrofs.repr 0) = x.

Lemma symbol_address_inject : forall j id ofs,
    meminj_preserves_globals j ->
    Val.inject j (Genv.symbol_address ge id ofs) (Genv.symbol_address tge id ofs).


Definition match_regs (fn : function) j (rs rs' : regset) :=
    (forall r, (r <= RTL.max_reg_function fn)%positive -> Val.inject j rs#r rs'#r).

Definition match_gsr gsr rs' m m' inj bgsr vgsr :=
  rs' # gsr = Vptr bgsr Ptrofs.zero
  /\ Mem.valid_access m' Mint32 bgsr 0 Writable
  /\ Mem.load Mint32 m' bgsr 0 = Some (Vint vgsr)
  /\ (forall delta, Events.loc_out_of_reach inj m bgsr delta).

Inductive match_stacks_unprot (m m': mem) (j: meminj):
  list stackframe -> list stackframe -> block -> block -> Prop :=
| match_stacks_unprot_nil: forall bound bound',
    meminj_preserves_globals j ->
    Ple (Genv.genv_next ge) bound -> Ple (Genv.genv_next tge) bound' ->
    match_stacks_unprot m m' j [] [] bound bound'
| match_stacks_unprot_cons1:
  forall res f sp sp' pc rs rs' stk stk' bound bound'
    (STACKS: match_stacks_unprot m m' j stk stk' sp sp')
    (SPINJ: j sp = Some (sp', 0))
    (REGINJ: match_regs f j rs rs')
    (BELOW: Plt sp bound)
    (TBELOW: Plt sp' bound'),
    match_stacks_unprot m m' j
      (Stackframe res f (Vptr sp Ptrofs.zero) pc rs :: stk)
      (Stackframe res f (Vptr sp' Ptrofs.zero) pc rs' :: stk')
      bound bound'
| match_stacks_unprot_cons2:
  forall res id id' f f' sp sp' pc rs rs' stk stk' bound bound' bgsr vgsr vgsr'
    (REG_OK : (res <= max_reg_function f)%positive)
    (HARDEN: harden_name id = Errors.OK id')
    (TR: is_transf_function_prot p id f f')
    (STACKS: match_stacks_prot m m' j stk stk' sp sp' id' (sig_res (fn_sig f)) bgsr vgsr)
    (SPINJ: j sp = Some (sp', 0))
    (REGINJ: match_regs f j rs rs')
    (BELOW: Plt sp bound)
    (TBELOW: Plt sp' bound')
    (GSR: match_gsr (gsr f) rs' m m' j bgsr vgsr')
    (GSRBELOW: Plt bgsr bound')
    (GSRV: rs' # (gsrv f) = Vint vgsr')
    (RTS: rs' # (rts f) = Vint (Int.xor vgsr vgsr')),
    match_stacks_unprot m m' j
      (Stackframe res f (Vptr sp Ptrofs.zero) pc rs :: stk)
      (Stackframe res f' (Vptr sp' Ptrofs.zero) pc rs' :: stk')
      bound bound'

with match_stacks_init_prot (m m': mem) (j: meminj):
  list stackframe -> list stackframe -> block -> block -> Prop :=
| match_stacks_init_prot_nil: forall bound bound',
    meminj_preserves_globals j ->
    Ple (Genv.genv_next ge) bound -> Ple (Genv.genv_next tge) bound' ->
    match_stacks_init_prot m m' j [] [] bound bound'
| match_stacks_unprot_init_prot:
  forall bound bound' stk stk'
    (STACKS: match_stacks_unprot m m' j stk stk' bound bound'),
    match_stacks_init_prot m m' j stk stk' bound bound'
| match_stacks_init_prot_cons2:
  forall res id id' f f' sp sp' pc rs rs' stk stk' bound bound' bgsr vgsr vgsr'
    (REG_OK : (res <= max_reg_function f)%positive)
    (HARDEN: harden_name id = Errors.OK id')
    (TR: is_transf_function_prot p id f f')
    (STACKS: match_stacks_prot m m' j stk stk' sp sp' id' (sig_res (fn_sig f)) bgsr vgsr)
    (SPINJ: j sp = Some(sp', 0))
    (REGINJ: match_regs f j rs rs')
    (BELOW: Plt sp bound)
    (TBELOW: Plt sp' bound')
    (GSR: match_gsr (gsr f) rs' m m' j bgsr vgsr')
    (GSRBELOW: Plt bgsr bound')
    (GSRV: rs' # (gsrv f) = Vint vgsr')
    (RTS: rs' # (rts f) = Vint (Int.xor vgsr vgsr')),
    match_stacks_init_prot m m' j (Stackframe res f (Vptr sp Ptrofs.zero) pc rs :: stk)
      (Stackframe res f' (Vptr sp' Ptrofs.zero) pc rs' :: stk')
      bound bound'

with match_stacks_prot (m m': mem) (j: meminj):
  list stackframe -> list stackframe -> block -> block -> qualident -> xtype -> block -> int -> Prop :=
| match_stacks_prot_both:
  forall res id id' f f' sp sp' pc pc' rs rs' stk stk' bound bound' pcxor2 pccheck pcstore pcnop2 pcabort cid cid' rty bgsr vgsr vgsr'
    (REG_OK : (res <= max_reg_function f)%positive)
    (HARDEN1: harden_name cid = Errors.OK cid')
    (TR: is_transf_function_prot p cid f f')
    (HARDEN2: harden_name id = Errors.OK id')
    (STACKS: match_stacks_prot m m' j stk stk' sp sp' cid' (sig_res (fn_sig f)) bgsr vgsr')
    (SPINJ: j sp = Some(sp', 0))
    (REGINJ: match_regs f j rs rs')
    (BELOW: Plt sp bound)
    (TBELOW: Plt sp' bound')
    (GSR: rs' # (gsr f) = Vptr bgsr Ptrofs.zero)
    (GSRBELOW: Plt bgsr bound')
    (GSRV: rs' # (gsrv f) = Vint vgsr)
    (RTS: rs' # (rts f) = Vint (Int.xor vgsr' vgsr))
    (LOAD: (fn_code f') ! pc' = Some (Iload TRAP Mint32 (Aindexed' Int.zero) [gsr f] (tmp1 f) pcxor2))
    (XOR2: (fn_code f') ! pcxor2 = Some (Iop (Oxorimm (hash_exit_sig id')) [tmp1 f] (tmp1 f) pccheck))
    (CHECK: (fn_code f') ! pccheck = Some (Icond (Ccomp Cne) [tmp1 f; gsrv f] pcabort pcstore (Some false)))
    (STORE: (fn_code f') ! pcstore = Some (Istore Mint32 (Aindexed' Int.zero) [gsr f] (gsrv f) pcnop2))
    (NOP2: (fn_code f') ! pcnop2 = Some (Inop pc)),
    match_stacks_prot m m' j (Stackframe res f (Vptr sp Ptrofs.zero) pc rs :: stk)
      (Stackframe res f' (Vptr sp' Ptrofs.zero) pc' rs' :: stk')
      bound bound' id' rty bgsr vgsr
| match_stacks_prot_right:
  forall id id' f f' pc' rs' sp' stk stk' bound bound' pcxor2 pccheck pcstore pcret pcabort bgsr vgsr
    (HARDEN: harden_name id = Errors.OK id')
    (TR: transf_function_init_prot id f = Errors.OK f')
    (STACKS: match_stacks_init_prot m m' j stk stk' bound sp')
    (TBELOW: Plt sp' bound')
    (SPPERM: Mem.range_perm m' sp' 0 (fn_stacksize f') Cur Freeable)
    (SPOUT: forall off, 0 <= off < size_chunk Mint32 -> Events.loc_out_of_reach j m sp' off)
    (GSR: rs' # (gsr f) = Vptr bgsr Ptrofs.zero)
    (GSRABOVE: Ple sp' bgsr)
    (GSRBELOW: Plt bgsr bound')
    (GSRV: rs' # (gsrv f) = Vint vgsr)
    (LOAD: (fn_code f') ! pc' = Some (Iload TRAP Mint32 (Aindexed' Int.zero) [gsr f] (tmp1 f) pcxor2))
    (XOR2: (fn_code f') ! pcxor2 = Some (Iop (Oxorimm (hash_exit_sig id')) [tmp1 f] (tmp1 f) pccheck))
    (CHECK: (fn_code f') ! pccheck = Some (Icond (Ccomp Cne) [tmp1 f; gsrv f] pcabort pcstore (Some false)))
    (STORE: (fn_code f') ! pcstore = Some (Istore Mint32 (Aindexed' Int.zero) [gsr f] (gsrv f) pcret))
    (RET: (fn_code f') ! pcret = Some (Ireturn (match sig_res (fn_sig f) with Xvoid => None | _ => Some (tmp3 f) end))),
    match_stacks_prot m m' j stk
      (Stackframe (tmp3 f) f' (Vptr sp' Ptrofs.zero) pc' rs' :: stk')
      bound bound' id' (sig_res (fn_sig f)) bgsr vgsr.

Scheme match_stacks_unprot_ind2 := Induction for match_stacks_unprot Sort Prop
    with match_stacks_init_prot_ind2 := Induction for match_stacks_init_prot Sort Prop
    with match_stacks_prot_ind2 := Induction for match_stacks_prot Sort Prop.
Combined Scheme match_stacks_all_ind from
  match_stacks_unprot_ind2, match_stacks_init_prot_ind2, match_stacks_prot_ind2.

Inductive match_states: RTL.state -> RTL.state -> Prop :=
| match_states_unprot:
  forall stk stk' f sp sp' pc rs rs' m m' j
    (STACKS: match_stacks_unprot m m' j stk stk' sp sp')
    (SPINJ: j sp = Some(sp', 0))
    (BELOW: Plt sp (Mem.nextblock m))
    (TBELOW: Plt sp' (Mem.nextblock m'))
    (REGS: match_regs f j rs rs')
    (MEMINJ: Mem.inject j m m'),
    match_states
      (State stk f (Vptr sp Ptrofs.zero) pc rs m)
      (State stk' f (Vptr sp' Ptrofs.zero) pc rs' m')
| match_states_prot:
  forall stk stk' id id' f f' sp sp' pc rs rs' m m' j bgsr vgsr vgsr'
    (STACKS: match_stacks_prot m m' j stk stk' sp sp' id' (sig_res (fn_sig f)) bgsr vgsr')
    (HARDEN: harden_name id = Errors.OK id')
    (TR: is_transf_function_prot p id f f')
    (SPINJ: j sp = Some(sp', 0))
    (BELOW: Plt sp (Mem.nextblock m))
    (TBELOW: Plt sp' (Mem.nextblock m'))
    (REGS : match_regs f j rs rs')
    (MEMINJ: Mem.inject j m m')
    (GSR: match_gsr (gsr f) rs' m m' j bgsr vgsr)
    (GSRV: rs' # (gsrv f) = Vint vgsr)
    (RTS: rs' # (rts f) = Vint (Int.xor vgsr' vgsr)),
    match_states (State stk f (Vptr sp Ptrofs.zero) pc rs m)
      (State stk' f' (Vptr sp' Ptrofs.zero) pc rs' m')
| match_callstates_unprot:
  forall stk stk' f args args' m m' j
    (STACKS: match_stacks_unprot m m' j stk stk' (Mem.nextblock m) (Mem.nextblock m'))
    (AINJ: Val.inject_list j args args')
    (MEMINJ: Mem.inject j m m'),
    match_states (Callstate stk f args m) (Callstate stk' f args' m')
| match_callstates_init_prot:
  forall id id' f f' fc' stk stk' args args' m m' j
    (STACKS: match_stacks_init_prot m m' j stk stk' (Mem.nextblock m) (Mem.nextblock m'))
    (HARD: harden_name id = Errors.OK id')
    (TR: transf_function_init_prot id f = Errors.OK f')
    (FIND: forall rs, find_function tge (inr id) rs = Some (Internal f'))
    (TR': is_transf_function_prot p id f fc')
    (FIND': forall rs, find_function tge (inr id') rs = Some (Internal fc'))
    (AINJ: Val.inject_list j args args')
    (MEMINJ: Mem.inject j m m'),
    match_states (Callstate stk (Internal f) args m)
      (Callstate stk' (Internal f') args' m')
| match_callstates_prot:
  forall id id' f f' stk stk' args rs' arg1 arg2 args' m m' j bgsr vgsr
    (STACKS: match_stacks_prot m m' j stk stk' (Mem.nextblock m) (Mem.nextblock m') id' (sig_res (fn_sig f)) bgsr vgsr)
    (HARD: harden_name id = Errors.OK id')
    (TR: is_transf_function_prot p id f f')
    (AINJ: Val.inject_list j args rs' ## args')
    (MEMINJ: Mem.inject j m m')
    (GSR: match_gsr arg1 rs' m m' j bgsr vgsr)
    (ARG2: rs' # arg2 = Vint (Int.xor vgsr (hash_entry_sig id'))),
    match_states (Callstate stk (Internal f) args m)
      (Callstate stk' (Internal f') rs' ## (arg1 :: arg2 :: args') m')
| match_return_unprot:
  forall stk stk' v v' m m' j
    (STACKS: match_stacks_unprot m m' j stk stk' (Mem.nextblock m) (Mem.nextblock m'))
    (VINJ: Val.inject j v v')
    (MEMINJ: Mem.inject j m m'),
    match_states (Returnstate stk v m) (Returnstate stk' v' m')
| match_return_init_prot:
  forall stk stk' v v' m m' j
    (STACKS: match_stacks_init_prot m m' j stk stk' (Mem.nextblock m) (Mem.nextblock m'))
    (VINJ: Val.inject j v v')
    (MEMINJ: Mem.inject j m m'),
    match_states (Returnstate stk v m) (Returnstate stk' v' m')
| match_return_prot:
  forall stk stk' v v' m m' j cid bgsr vgsr rty
    (STACKS: match_stacks_prot m m' j stk stk' (Mem.nextblock m) (Mem.nextblock m') cid rty bgsr vgsr)
    (STKNNIL: stk <> [])
    (WTV: rty = Xvoid -> v = Vundef)
    (VINJ: Val.inject j v v')
    (MEMINJ: Mem.inject j m m')
    (GSRPERM: Mem.valid_access m' Mint32 bgsr 0 Writable)
    (GSRL: Mem.load Mint32 m' bgsr 0 = Some (Vint (Int.xor (hash_exit_sig cid) vgsr)))
    (GSROUT: forall delta, Events.loc_out_of_reach j m bgsr delta),
    match_states (Returnstate stk v m)
      (Returnstate stk' v' m').


Lemma match_regs_assign :
  forall f j rs rs' res v v',
    Val.inject j v v' ->
    match_regs f j rs rs' ->
    match_regs f j (rs # res <- v) (rs' # res <- v').

Lemma match_regs_assign' : forall f j rs rs' res v',
    (max_reg_function f < res)%positive ->
    match_regs f j rs rs' ->
    match_regs f j rs (rs' # res <- v').

Hint Resolve match_regs_assign match_regs_assign' : ipcfc.

Lemma match_regs_incr:
  forall f j j' rs rs', inject_incr j j' -> match_regs f j rs rs' -> match_regs f j' rs rs'.

Lemma match_regs_undef:
  forall fn j rs', match_regs fn j (Regmap.init Vundef) rs'.

Lemma match_regs_init: forall fn j params args args',
    Val.inject_list j args args' ->
    match_regs fn j (init_regs args params) (init_regs args' params).

Fact match_regs_init_twice: forall fn j params args args',
    Val.inject_list j args args' ->
    match_regs fn j (init_regs args params)
      (init_regs (init_regs args' params) ## params params).

Lemma match_regs_inject_list : forall f j rs rs' args,
    match_regs f j rs rs' ->
    (forall r, In r args -> (r <= max_reg_function f)%positive) ->
    Val.inject_list j rs ## args rs' ## args.

Lemma match_gsr_assign : forall gsr rs m m' j bgsr vgsr r v,
    r <> gsr ->
    match_gsr gsr rs m m' j bgsr vgsr ->
    match_gsr gsr (rs # r <- v) m m' j bgsr vgsr.

Lemma match_gsr_mem :
  forall f rs m1 m1' m2 m2' j bgsr vgsr,
    (Mem.load Mint32 m2' bgsr 0 = Mem.load Mint32 m1' bgsr 0) ->
    (forall b delta ofs kind perm, j b = Some (bgsr, delta) -> Mem.perm m2 b ofs kind perm -> Mem.perm m1 b ofs kind perm) ->
    (forall ofs kind perm, 0 <= ofs < size_chunk Mint32 -> Events.loc_out_of_reach j m1 bgsr ofs -> Mem.perm m1' bgsr ofs kind perm -> Mem.perm m2' bgsr ofs kind perm) ->
    match_gsr f rs m1 m1' j bgsr vgsr ->
    match_gsr f rs m2 m2' j bgsr vgsr.

Lemma match_gsr_external_call :
  forall f rs m1 m1' m2 m2' j j' bgsr vgsr ef vargs vargs' vres vres' t,
    Events.external_call ef ge vargs m1 t vres m2 ->
    Events.external_call ef tge vargs' m1' t vres' m2' ->
    Mem.inject j m1 m1' ->
    Mem.unchanged_on (Events.loc_unmapped j) m1 m2 ->
    Mem.unchanged_on (Events.loc_out_of_reach j m1) m1' m2' ->
    inject_incr j j' ->
    Events.inject_separated j j' m1 m1' ->
    match_gsr f rs m1 m1' j bgsr vgsr ->
    match_gsr f rs m2 m2' j' bgsr vgsr.

Lemma match_gsr_incr' : forall f rs m m' j j' bgsr vgsr,
    inject_incr j j' ->
    (forall b delta, j b = None -> j' b = Some (bgsr, delta) -> ~Mem.valid_block m b) ->
    match_gsr f rs m m' j bgsr vgsr ->
    match_gsr f rs m m' j' bgsr vgsr.

Corollary match_gsr_incr : forall f rs m m' j j' bgsr vgsr,
    inject_incr j j' ->
    Events.inject_separated j j' m m' ->
    match_gsr f rs m m' j bgsr vgsr ->
    match_gsr f rs m m' j' bgsr vgsr.

Lemma match_stacks_preserves_globals:
  forall m m' j s ts bound tbound,
    match_stacks_unprot m m' j s ts bound tbound
    \/ match_stacks_init_prot m m' j s ts bound tbound
    \/ (exists cid rty bgsr vgsr, match_stacks_prot m m' j s ts bound tbound rty cid bgsr vgsr) ->
    meminj_preserves_globals j.

Ltac extlia := unfold Mem.valid_block, tmp3, tmp2, tmp1, rts, gsrv, gsr in *; Coqlib.extlia.

Lemma match_stacks_incr:
  forall m m' j j',
    inject_incr j j' ->
    forall s ts bound tbound,
      (forall b1 b2 delta,
          j b1 = None -> j' b1 = Some(b2, delta) -> Ple bound b1 /\ Ple tbound b2) ->
      (match_stacks_unprot m m' j s ts bound tbound -> match_stacks_unprot m m' j' s ts bound tbound)
      /\ (match_stacks_init_prot m m' j s ts bound tbound -> match_stacks_init_prot m m' j' s ts bound tbound)
      /\ (forall cid rty bgsr vgsr, match_stacks_prot m m' j s ts bound tbound cid rty bgsr vgsr -> match_stacks_prot m m' j' s ts bound tbound cid rty bgsr vgsr).

Lemma match_stacks_bound:
  forall m m' j s ts bound tbound bound' tbound',
  Ple bound bound' -> Ple tbound tbound' ->
  (match_stacks_unprot m m' j s ts bound tbound -> match_stacks_unprot m m' j s ts bound' tbound')
  /\ (match_stacks_init_prot m m' j s ts bound tbound -> match_stacks_init_prot m m' j s ts bound' tbound')
  /\ (forall cid rty bgsr vgsr, match_stacks_prot m m' j s ts bound tbound cid rty bgsr vgsr -> match_stacks_prot m m' j s ts bound' tbound' cid rty bgsr vgsr).

Definition match_perm_1 (j: meminj) m1 m2 bound' :=
  (forall b size kind perm, (forall b' delta, j b = Some (b', delta) -> Plt b' bound') -> Mem.perm m2 b size kind perm -> Mem.perm m1 b size kind perm).

Definition match_perm_2 (j: meminj) m1 m1' m2' bound' :=
  (forall b' ofs kind perm, Plt b' bound' -> Events.loc_out_of_reach j m1 b' ofs -> Mem.perm m1' b' ofs kind perm -> Mem.perm m2' b' ofs kind perm).

Hint Unfold match_perm_1 match_perm_2 : ipcfc.

Lemma match_stacks_mem:
  forall m1 m2 m1' m2' j,
     (forall s ts bound tbound,
          match_stacks_unprot m1 m1' j s ts bound tbound ->
          match_perm_1 j m1 m2 tbound ->
          match_perm_2 j m1 m1' m2' tbound ->
          (forall b', Plt b' tbound -> (forall ofs, Events.loc_out_of_reach j m1 b' ofs) -> Mem.load Mint32 m2' b' 0 = Mem.load Mint32 m1' b' 0) ->
          match_stacks_unprot m2 m2' j s ts bound tbound)
    /\ (forall s ts bound tbound,
          match_stacks_init_prot m1 m1' j s ts bound tbound ->
          match_perm_1 j m1 m2 tbound ->
          match_perm_2 j m1 m1' m2' tbound ->
          (forall b', Plt b' tbound -> (forall ofs, Events.loc_out_of_reach j m1 b' ofs) -> Mem.load Mint32 m2' b' 0 = Mem.load Mint32 m1' b' 0) ->
          match_stacks_init_prot m2 m2' j s ts bound tbound)
    /\ (forall s ts bound tbound cid rty bgsr vgsr,
          match_stacks_prot m1 m1' j s ts bound tbound cid rty bgsr vgsr ->
          match_perm_1 j m1 m2 tbound ->
          match_perm_2 j m1 m1' m2' tbound ->
          (forall b', Plt b' bgsr -> Plt b' tbound -> (forall ofs, Events.loc_out_of_reach j m1 b' ofs) -> Mem.load Mint32 m2' b' 0 = Mem.load Mint32 m1' b' 0) ->
          match_stacks_prot m2 m2' j s ts bound tbound cid rty bgsr vgsr).

Lemma match_stacks_mem_external_call:
  forall ef vargs t vres m1 m2 m1' m2' j s ts bound tbound,
    Mem.inject j m1 m1' ->
    Events.external_call ef ge vargs m1 t vres m2 ->
    Mem.unchanged_on (Events.loc_out_of_reach j m1) m1' m2' ->
    (match_stacks_unprot m1 m1' j s ts bound tbound -> match_stacks_unprot m2 m2' j s ts bound tbound)
    /\ (match_stacks_init_prot m1 m1' j s ts bound tbound -> match_stacks_init_prot m2 m2' j s ts bound tbound)
    /\ (forall cid rty bgsr vgsr, match_stacks_prot m1 m1' j s ts bound tbound cid rty bgsr vgsr -> match_stacks_prot m2 m2' j s ts bound tbound cid rty bgsr vgsr).

Definition match_stacks_preserves m m' j bound bound' m1 m1' j1 bound1 bound1' :=
  forall stk stk',
    (match_stacks_unprot m m' j stk stk' bound bound' -> match_stacks_unprot m1 m1' j1 stk stk' bound1 bound1')
    /\ (match_stacks_init_prot m m' j stk stk' bound bound' -> match_stacks_init_prot m1 m1' j1 stk stk' bound1 bound1')
    /\ (forall cid rty bgsr vgsr, match_stacks_prot m m' j stk stk' bound bound' cid rty bgsr vgsr -> match_stacks_prot m1 m1' j1 stk stk' bound1 bound1' cid rty bgsr vgsr).

Lemma match_stacks_alloc : forall m m' sp sp' size m1 m1' j j1,
    Mem.alloc m 0 size = (m1, sp) ->
    Mem.alloc m' 0 size = (m1', sp') ->
    inject_incr j j1 ->
    j1 sp = Some (sp', 0) ->
    (forall b, b <> sp -> j1 b = j b) ->
    match_stacks_preserves m m' j (Mem.nextblock m) (Mem.nextblock m') m1 m1' j1 sp sp'.

Lemma match_stacks_free : forall m m' sp sp' size m1 m1' j,
    j sp = Some (sp', 0) ->
    Plt sp (Mem.nextblock m) ->
    Plt sp' (Mem.nextblock m') ->
    Mem.free m sp 0 size = Some m1 ->
    Mem.free m' sp' 0 size = Some m1' ->
    match_stacks_preserves m m' j sp sp' m1 m1' j (Mem.nextblock m1) (Mem.nextblock m1').


Lemma init_mem_exists:
  forall m, Genv.init_mem p = Some m ->
  exists tm, Genv.init_mem tp = Some tm.

Section INIT_MEM.

Variables m tm: mem.
Hypothesis IM: Genv.init_mem p = Some m.
Hypothesis TIM: Genv.init_mem tp = Some tm.

Definition init_meminj : meminj :=
  fun b =>
    match Genv.invert_symbol ge b with
    | Some id =>
        match Genv.find_symbol tge id with
        | Some b' => Some (b', 0)
        | None => None
        end
    | None => None
    end.

Remark init_meminj_eq:
  forall id b b',
  Genv.find_symbol ge id = Some b -> Genv.find_symbol tge id = Some b' ->
  init_meminj b = Some(b', 0).

Remark init_meminj_invert:
  forall b b' delta,
  init_meminj b = Some(b', delta) ->
  delta = 0 /\ exists id, Genv.find_symbol ge id = Some b /\ Genv.find_symbol tge id = Some b'.

Lemma init_meminj_preserves_globals:
  meminj_preserves_globals init_meminj.

Lemma init_meminj_invert_strong:
  forall b b' delta,
  init_meminj b = Some(b', delta) ->
  delta = 0 /\
  exists id gd gd',
     Genv.find_symbol ge id = Some b
  /\ Genv.find_symbol tge id = Some b'
  /\ Genv.find_def ge b = Some gd
  /\ Genv.find_def tge b' = Some gd'
  /\ match_gdef id gd gd'.

Lemma bytes_of_init_inject:
  forall il,
  list_forall2 (memval_inject init_meminj)
    (Genv.bytes_of_init_data_list ge il)
    (Genv.bytes_of_init_data_list tge il).

Lemma init_mem_inj_1:
  Mem.mem_inj init_meminj m tm.

Lemma init_mem_inj_2:
  Mem.inject init_meminj m tm.

End INIT_MEM.

Theorem init_mem_inject:
  forall m,
  Genv.init_mem p = Some m ->
  exists f tm, Genv.init_mem tp = Some tm /\ Mem.inject f m tm /\ meminj_preserves_globals f.

Lemma transf_initial_states:
  forall st1, initial_state p st1 -> exists st2, initial_state tp st2 /\ match_states st1 st2.


Lemma transf_final_states:
  forall st1 st2 r,
  match_states st1 st2 -> final_state st1 r -> final_state st2 r.


Lemma eval_builtin_arg_inject:
  forall f rs sp m j rs' sp' m' a v,
    Events.eval_builtin_arg ge (fun r => rs#r) (Vptr sp Ptrofs.zero) m a v ->
    (forall r, In r (params_of_builtin_arg a) -> (r <= max_reg_function f)%positive) ->
    j sp = Some(sp', 0) ->
    meminj_preserves_globals j ->
    match_regs f j rs rs' ->
    Mem.inject j m m' ->
    exists v',
      Events.eval_builtin_arg tge (fun r => rs'#r) (Vptr sp' Ptrofs.zero) m' a v'
      /\ Val.inject j v v'.

Lemma eval_builtin_args_inject:
  forall f rs sp m j rs' sp' m' al vl,
    Events.eval_builtin_args ge (fun r => rs#r) (Vptr sp Ptrofs.zero) m al vl ->
    (forall r, In r (params_of_builtin_args al) -> (r <= max_reg_function f)%positive) ->
    j sp = Some(sp', 0) ->
    meminj_preserves_globals j ->
    match_regs f j rs rs' ->
    Mem.inject j m m' ->
    exists vl',
      Events.eval_builtin_args tge (fun r => rs'#r) (Vptr sp' Ptrofs.zero) m' al vl'
      /\ Val.inject_list j vl vl'.

Lemma eval_assert_arg_inject:
  forall f rs sp m j rs' sp' m' a v,
    eval_assert_arg ge (Vptr sp Ptrofs.zero) rs m a v ->
    (forall r, In r (params_of_assert_arg a) -> (r <= max_reg_function f)%positive) ->
    j sp = Some(sp', 0) ->
    meminj_preserves_globals j ->
    match_regs f j rs rs' ->
    Mem.inject j m m' ->
    exists v',
      eval_assert_arg tge (Vptr sp' Ptrofs.zero) rs' m' a v'
      /\ Val.inject j v v'.

Lemma eval_assert_args_inject:
  forall f rs sp m j rs' sp' m' al vl,
    eval_assert_args ge (Vptr sp Ptrofs.zero) rs m al vl ->
    (forall r, In r (params_of_assert_args al) -> (r <= max_reg_function f)%positive) ->
    j sp = Some(sp', 0) ->
    meminj_preserves_globals j ->
    match_regs f j rs rs' ->
    Mem.inject j m m' ->
    exists vl',
      eval_assert_args tge (Vptr sp' Ptrofs.zero) rs' m' al vl'
      /\ Val.inject_list j vl vl'.

Lemma init_regs_gss : forall params args,
    length args = length params ->
    list_norepet params ->
    (init_regs args params) ## params = args.

Lemma protected_entry_step_simulation :
  forall id id' f f' stk args rs' stk' m m1 arg1 arg2 args' m' inj bgsr vgsr,
    harden_name id = Errors.OK id' ->
    is_transf_function_prot p id f f' ->
    match_regs f inj (init_regs args (fn_params f)) (init_regs rs' ## args' (fn_params f)) ->
    match_stacks_prot m m' inj stk stk' (Mem.nextblock m) (Mem.nextblock m') id' (sig_res (fn_sig f)) bgsr vgsr ->
    Mem.inject inj m m' ->
    match_gsr arg1 rs' m m' inj bgsr vgsr ->
    rs'#arg2 = Vint (Int.xor vgsr (hash_entry_sig id')) ->
    list_forall2 Val.has_argtype rs' ## args' (sig_args (fn_sig f)) ->
    Mem.alloc m 0 (fn_stacksize f) = (m1, Mem.nextblock m) ->
    exists s2' : RTL.state,
      plus step tge (Callstate stk' (Internal f') rs' ## (arg1 :: arg2 ::args') m') Events.E0 s2' /\
        match_states
          (State stk f (Vptr (Mem.nextblock m) Ptrofs.zero) (fn_entrypoint f) (init_regs args (fn_params f)) m1)
          s2'.

Fact plus_match_trans : forall s2 s1',
    (exists s2', plus step tge s1' [] s2' /\ exists s3', plus step tge s2' [] s3' /\ match_states s2 s3') ->
    exists s2', plus step tge s1' [] s2' /\ match_states s2 s2'.

Hint Resolve plus_one : ipcfc.
Hint Constructors step : ipcfc.
Hint Constructors match_stacks_unprot match_stacks_init_prot match_stacks_prot match_states : ipcfc.
Hint Resolve symbol_address_inject Mem.valid_pointer_inject_val Mem.weak_valid_pointer_inject_val Mem.weak_valid_pointer_inject_no_overflow Mem.different_pointers_inject : inject.
Hint Unfold transf_call transf_return : rtlcm.

Lemma step_simulation : forall s1 s2 t s1',
    wt_state s1 ->
    step ge s1 t s1' ->
    match_states s1 s2 ->
    exists s2', plus step tge s2 t s2' /\ match_states s1' s2'.


Theorem transf_program_correct:
  forward_simulation (semantics p) (semantics tp).

End IPCFC.


Transparent Linker_def Linker_fundef Linker_vardef.

Ltac destruct_conjs :=
  repeat
    match goal with
    | x:(_ * _) |- _ => destruct x
    end.

Ltac inv_equalities :=
  destruct_conjs;
  repeat
    match goal with
    | H:(_, _) = (_, _) |- _ => inv H
    | H:Some _ = Some _ |- _ => inv H
    | H:None = Some _ |- _ => inv H
    | H:Some _ = None |- _ => inv H
    end.

Ltac simpl_In :=
  repeat
    match goal with
    | H:In _ (map _ _) |- _ =>
        apply in_map_iff in H as (?&?F&H); destruct_conjs
    | H:In _ (map_filter _ _) |- _ =>
        apply map_filter_In in H as (?&?PRED&H); destruct_conjs
    | H:In _ (QITree.elements _) |- _ =>
        apply QITree.elements_complete in H
    | H:(QITree_Properties.of_list _)!._ = Some _ |- _ =>
        apply QITree_Properties.in_of_list in H
    end.

Ltac solve_In :=
  simpl_In;
  repeat
    match goal with
    | |- In _ (map _ _) =>
        apply in_map_iff; do 2 esplit; eauto with datatypes
    | |- In _ (map_filter _ _) =>
        apply map_filter_In; do 2 esplit; eauto with datatypes
    | |- In _ (QITree.elements _) =>
        apply QITree.elements_correct
    | |- (QITree_Properties.of_list _)!._ = Some _ =>
        apply QITree_Properties.of_list_norepet
    end.

Fact of_list_unit : forall l x,
    In x l ->
    (QITree_Properties.of_list (map (fun x => (x, tt)) l))!.x = Some tt.

Fact map_filter_norepet_fst A B C : forall (f: (A * B) -> option (A * C)) l,
    (forall a1 b a2 c, f (a1, b) = Some (a2, c) -> a2 = a1) ->
    list_norepet (map fst l) ->
    list_norepet (map fst (map_filter f l)).

Lemma prog_defmap_protected_None : forall prog id,
    (prog_defmap prog)!.id = None ->
    (protected prog)!.id = None.

Global Instance TransfLinkIPCFC : TransfLink IPCFCproof.match_prog.