# Module BTL_BlockSimulationproof

Proof of BTL Block Simulation modulo Gluing (Symbolic) Invariants. Simulation diagram (for the "main" lemma iblock_step_simulation)
```
(0) = Initial symbolic states: sis_source_correct & sis_target_correct
(1) = Source symbolic execution: sexec_correct
(2) = Symbolic simulation test
(3) = Coming back to concrete states: sexec_exact.
(4) = final_step_simulation + sfv_equiv

stk0          stk0                     stk1          stk1
f0            f0                       f1            f1
. . . . . . . . . . . . . . . . . . . . .
.                                           .
.                                               .
.    (0)                                     (0)    .
cs0 +++++++++ ss0                      ss1 ++++++++++ cs1
|             |                        |              |
|             |                        |              |
|             |                        |              |
|    (1)      |                        |      (3)     |
|             |                        |              |
|             |                        |              |
|             |                        |              |
|             |                        |              |
V             V          (2)           V              V
cf0' ++++++++ sf0 ==================== sf1' ++++++++ cf1'
|                                                     |
|                                                     |
|                        (4)                          |
V                                                     V
cs0' . . . . . . . . . . . . . . . . . . . . . . . . cs1'

Legend:
- cs* -> concrete states
- cf* -> concrete final states (i.e. concrete state + final value)
- ss* -> symbolic states
- sf* -> symbolic final states (i.e. symbolic state + symbolic final value)
- *0  -> Source initial state
- *1  -> Target initial state
- *0' -> Source final state
- *1' -> Target final state
- "...." is match_invs / match_states
- "++++" is sem_sistates (+ sfv_equiv for final states)
- "====" is match_sexec_si

Remark:
- cs0 = <sp,rs0,m0>
- tr_sis is used to define ssS and ssI using tr_sis_elim_match_si
and to deduce properties on the concrete states from match_sexec_si
using tr_sis_intro_match_si
```

Require Import AST Linking IPass Values Maps Globalenvs Smallstep Registers.
Require Import Coqlib Events Errors OptionMonad.
Require Import RTL BTL BTL_SEtheory.
Require Import BTLmatchRTL BTL_BlockSimulation.
Require Import ValueDomain.
Require BTL_ResetAnnots BTL_AnalysisLib.

Module BTL_BlockSimulationproof (B: BTL_BlockSimulationConfig).

Include BTL_BlockSimulation B.

Definition match_prog (p tp: program) :=
match_program (fun cu f tf => transf_fundef f = OK tf) eq p tp.

Definition pass := mkpass match_prog.

Lemma transf_program_match:
forall prog tprog, transf_program prog = OK tprog -> match_prog prog tprog.
Proof.
intros. eapply match_transform_partial_program_contextual; eauto.
Qed.

Section PRESERVATION.

Variable prog: program.
Variable tprog: program.

Hypothesis TRANSL: match_prog prog tprog.

Let pge := Genv.globalenv prog.
Let tpge := Genv.globalenv tprog.

Lemma symbols_preserved s: Genv.find_symbol tpge s = Genv.find_symbol pge s.
Proof.
rewrite <- (Genv.find_symbol_match TRANSL). reflexivity.
Qed.

Lemma senv_preserved:
Senv.equiv pge tpge.
Proof.
eapply (Genv.senv_match TRANSL).
Qed.

Lemma functions_translated:
forall (v: val) (f: fundef),
Genv.find_funct pge v = Some f ->
exists tf cunit,
transf_fundef f = OK tf /\
Genv.find_funct tpge v = Some tf /\
Proof.
intros. exploit (Genv.find_funct_match TRANSL); eauto.
intros (cu & tf & A & B & C).
exists tf. exists cu.
intuition eauto.
Qed.

Lemma transf_function_correct f f':
transf_function f = OK f' -> match_function f f'.
Proof.
unfold transf_function. intros H.
assert (OH: transf_function f = OK f') by auto.
destruct (btl_optim_oracle f); destruct p;
exploit transf_function_only_liveness; intuition eauto.
simpl in *; econstructor; eauto.
eapply check_symbolic_simu_correct; eauto.
Qed.

Lemma transf_fundef_correct f f':
transf_fundef f = OK f' -> match_fundef f f'.
Proof.
intros TRANSF; destruct f; simpl; inv TRANSF.
+ monadInv H0. exploit transf_function_correct; eauto.
intros. econstructor; eauto.
+ eapply match_External.
Qed.

Lemma function_ptr_translated:
forall b f,
Genv.find_funct_ptr pge b = Some f ->
exists cunit tf, Genv.find_funct_ptr tpge b = Some tf
/\ transf_fundef f = OK tf
Proof.
intros.
exploit (Genv.find_funct_ptr_match TRANSL); eauto.
Qed.

Lemma function_sig_translated f tf: transf_fundef f = OK tf -> funsig tf = funsig f.
Proof.
intros H; apply transf_fundef_correct in H; destruct H; simpl; eauto.
symmetry; erewrite preserv_fnsig; eauto.
Qed.

Theorem transf_initial_states:
forall s1, initial_state prog s1 ->
exists s2, initial_state tprog s2 /\ match_states pge s1 s2.
Proof.
intros. inv H.
exploit function_ptr_translated; eauto. intros (cu & tf & FIND & TRANSF & LINK).
eexists. split.
- econstructor; eauto.
+ intros; apply (Genv.init_mem_match TRANSL); eauto.
+ replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved. eauto.
symmetry. eapply match_program_main. eauto.
+ erewrite function_sig_translated; eauto.
- apply transf_fundef_correct in TRANSF. inv TRANSF;
repeat (econstructor; eauto).
Qed.

Lemma transf_final_states s1 s2 r:
match_states pge s1 s2 -> final_state s1 r -> final_state s2 r.
Proof.
intros. inv H0. inv H. inv STACKS. constructor.
Qed.

Lemma symbols_preserved_rev s: Genv.find_symbol pge s = Genv.find_symbol tpge s.
Proof.
symmetry; apply symbols_preserved.
Qed.

Section FINAL_STEP.

Lemma find_function_v_preserved fp fd:
find_function_v pge fp = Some fd ->
exists tf,
find_function_v tpge fp = Some tf /\
transf_fundef fd = OK tf.
Proof.
destruct fp; simpl.
- intros; ecase functions_translated as (tf & cu & TF & TPGE & _); eauto.
- rewrite symbols_preserved. repeat autodestruct. intros.
ecase function_ptr_translated as (tf & cu & TF & TPGE & _); eauto.
Qed.

Variables (f0 f1 : function) (sp0 : val) (rs0 rs1 : regset)
(m0 m1 : Memory.Mem.mem) (bc : block_classification).

Let ctx := Bcctx pge sp0 rs0 rs1 m1 bc.

Lemma final_step_simulation stk0 stk1 (fin : finalA val) t s0
(MF : match_function f0 f1)
(STACK : list_forall2 (match_stackframes pge) stk0 stk1)
(MATCH_H : let (P, S) := si_sfv_set (fun pc => history (fn_gm f1 pc)) fin in
P /\ forall si, S si -> match_si ctx si rs0)
(MATCH_G : let (P, S) := si_sfv_set (fun pc => glue (fn_gm f1 pc)) fin in
P /\ forall si, S si -> match_si ctx si rs1)
(MATCH_M : let (P, S) := meminv_sfv_set (fun pc => meminv (fn_gm f1 pc)) fin in
P /\ forall im, S im -> match_meminv ctx im m0)
(FINAL : final_step_v pge stk0 f0 sp0 rs0 m0 bc fin t s0):
exists s1,
final_step_v tpge stk1 f1 sp0 rs1 m1 bc fin t s1 /\
match_states pge s0 s1.
Proof.
Local Ltac intro_goal :=
eexists; split; [econstructor; simpl; eauto|constructor; simpl; auto].
apply preserv_fnstacksize in MF as SZ.
assert (MATCH :
let (p_H, s_H) := si_sfv_set (fun pc => history (fn_gm f1 pc)) fin in
let (p_G, s_G) := si_sfv_set (fun pc => glue (fn_gm f1 pc)) fin in
let (p_M, s_M) := meminv_sfv_set (fun pc => meminv (fn_gm f1 pc)) fin in
p_H /\ p_G /\ p_M /\
forall inv, s_H inv.(history) -> s_G inv.(glue) -> s_M inv.(meminv) ->
match_invs ctx inv m0). {
do 3 autodestruct; intros; unfold match_invs; intuition.
}
(* This lemma prove the equality of the memories where it is needed (for instance before a call). *)
assert (MEM_EQ:
let (_, s) := meminv_sfv_set (fun pc => meminv (fn_gm f1 pc)) fin in
s nil -> m0 = cm1 ctx). {
autodestruct; intros _ NIL.
apply MATCH_M in NIL; injection NIL as ->; reflexivity.
}
clear MATCH_H MATCH_G MATCH_M.

inversion FINAL; subst; simpl in *;
try (case MEM_EQ; [reflexivity|]).
- intro_goal.
+ apply MATCH; eauto.
- intro_goal.
+ rewrite <- SZ. eassumption.
- eapply find_function_v_preserved in H as (tf & FIND & TF).
apply transf_fundef_correct in TF as TMF.
intro_goal.
+ eapply function_sig_translated; eassumption.
+ do 2 (constructor; auto); intros.
case MATCH as (? & ? & ? & INV).
eapply clobbered_compat_matchinvs_preserv; eauto using test_clobberable_correct.
- eapply find_function_v_preserved in H as (tf & FIND & TF).
apply transf_fundef_correct in TF as TMF.
intro_goal.
+ eapply function_sig_translated; eassumption.
+ rewrite <- SZ. eassumption.
- intro_goal.
+ eapply eval_builtin_args_preserved.
* apply senv_preserved.
* eassumption.
+ eapply external_call_symbols_preserved; eauto.
apply senv_preserved.
+ destruct (reg_builtin_res res) eqn:EQBR.
* replace res with (BR r)
by (destruct res eqn:HBR in EQBR; inv EQBR; auto).
case MATCH as (? & ? & ? & INV).
eapply clobbered_compat_matchinvs_preserv; eauto using test_clobberable_correct.
* assert (NORES: forall rs, regmap_setres res vres rs = rs)
by (revert EQBR; destruct res; try inversion 1; reflexivity).
rewrite !NORES.
case MATCH as (? & ? & ? & INV).
eapply matchinvs_update_m; eauto using test_csifreem_correct.
- intro_goal.
+ apply list_nth_z_in in H0 as PC.
apply MATCH; eauto.
Qed.

End FINAL_STEP.

Theorem iblock_step_simulation stk1 stk2 f1 f2 sp rs rs' m m' bc ibf1 t csE pc
(ISTEP: iblock_step AnnotUndef pge stk1 f1 sp rs m bc ibf1.(entry) t csE)
(PC: (fn_code f1) ! pc = Some ibf1)
(MF: match_function f1 f2)
(MATCHI: match_invs (Bcctx pge sp rs rs' m' bc) (f2.(fn_gm) pc) m)
(STACKS: list_forall2 (match_stackframes pge) stk1 stk2)
:exists ibf2 ssIE',
(fn_code f2) ! pc = Some ibf2
/\ iblock_step AnnotUndef tpge stk2 f2 sp rs' m' bc ibf2.(entry) t ssIE'
/\ match_states pge csE ssIE'.
Proof.
pose (ctx:=Sctx pge tpge symbols_preserved_rev sp rs rs' m' bc).
change ({| cge := pge |}) with (bcctx1 ctx) in MATCHI.
eapply match_sexec_ok in MF as IB_MATCH; eauto. case IB_MATCH as (ibf2 & -> & IB_MATCH).
exists ibf2.
destruct ibf1 as [ib1 ?], ibf2 as [ib2 ?]; simpl in *.
apply sis_source_correct in MATCHI as SIS_0.
apply sis_target_correct in MATCHI as SIS_I.
rewrite sem_sistate_preserved in SIS_I.
specialize (IB_MATCH (bcctx1 ctx)); unfold match_sexec_si in IB_MATCH.
case get_soutcome as [sis1E sfv1] eqn:OUT1 in IB_MATCH.
case IB_MATCH as (HYP1 & MATCH).
case ISTEP as (rsE & mE & fin1 & ISTEP1 & FIN1).
(* symbolic execution of the source iblock *)
eapply sexec_correct with (ctx := Bfctx f1 (bcctx1 ctx)) in SIS_0 as (SIS_1E & SFV1); simpl in *;
try solve [reflexivity | eassumption].
case get_soutcome as (sis2IE & sfv2) eqn:OUT2 in MATCH.
set (sisE := set_smem _ sis1E) in MATCH.
case MATCH as (HYP2 & OK2 & SFV_SIMU & MATCH_H & MATCH_G & MATCH_M).
{ eapply sem_sis_ok, SIS_1E. }
rewrite get_soutcome_preserved in OUT2.
rewrite okpred_preserved in HYP2.
rewrite sis_ok_preserved in OK2.
(* symbolic execution of the target iblock *)
eapply sexec_exact with (ctx := Bfctx f2 (bcctx2 ctx)) in SIS_I as SIS_IE; eauto.
case SIS_IE as (rsIE & mIE & fin2 & ISTEP2 & SIS_2IE & SFV2); simpl in *.
eapply sem_sistate_preserved in SIS_2IE.
assert (total_sreg sis2IE). {
apply sexec_total_sreg in OUT2; auto.
apply tr_sis_total.
}
(* state with the final regset of the source and the final memory of the target *)
assert (SIS_E : sem_sistate (bcctx1 ctx) sisE rsE mIE). {
split; [|split]; simpl.
- eapply sem_sis_ok, SIS_1E.
- apply SIS_2IE.
- apply SIS_1E.
}
assert (total_sreg sisE). {
apply sexec_total_sreg in OUT1; auto.
apply tr_sis_total.
}
(* final step *)
unfold sfv_equiv in SFV1, SFV2; simpl in SFV1, SFV2.
case SFV1 as (fin_v & FIN_V & FIN1_IFF); apply FIN1_IFF in FIN1.
apply ex_Some_iff in SFV2.
apply sfv_simu_eval in SFV_SIMU.
rewrite <- eval_final_sval_preserved, <- SFV_SIMU, FIN_V in SFV2; simpl in SFV2.
unfold match_tr_si_sfv in MATCH_H, MATCH_G.
erewrite -> si_sfv_set_map_final in MATCH_H, MATCH_G by exact FIN_V.
erewrite -> meminv_sfv_set_map_final in MATCH_M by exact FIN_V.

eapply final_step_simulation with (rs0 := rsE) (rs1 := rsIE) (m0 := mE) (m1 := mIE)
in FIN1 as (s1 & FIN2 & MATCH); eauto;
cycle 1. 1-3:autodestruct; intros _; split; [tauto|intros ? HP].
- apply MATCH_H in HP.
apply HP in SIS_E as SIS_H.
eapply match_si_rstrg_preserv. apply siof_trg_free.
eapply tr_sis_intro_match_si in SIS_H; eauto.
- apply MATCH_G in HP.
apply HP in SIS_2IE as SIS_G.
eapply match_si_rstrg_preserv. apply siof_trg_free.
eapply tr_sis_intro_match_si in SIS_G; eauto.
- apply MATCH_M in HP; unfold match_meminv.
case SIS_1E as (_ & <- & _).
rewrite HP.
erewrite sem_sis_sm_subst_trg by eauto.
eapply smdep_preserv.
intros [|] ? DEP. reflexivity. exfalso.
eapply imem_subst_src_free; eauto.
- apply SFV2 in FIN2; simpl in *.
exists s1; split; [|split]; auto.
exists rsIE, mIE, fin2; split; auto.
Qed.

Local Hint Constructors step: core.

Theorem step_simulation s1 s1' t s2
(STEP: step AnnotUndef pge s1 t s1')
(MS: match_states pge s1 s2)
:exists s2',
step AnnotUndef tpge s2 t s2'
/\ match_states pge s1' s2'.
Proof.
destruct STEP as [stack ibf f sp n rs m bc t s PC STEP | | | ]; inv MS.
- (* iblock *)
simplify_someHyps. intros PC.
exploit iblock_step_simulation; eauto.
intros (ibf' & s2 & PC2 & STEP2 & MS2).
eexists; split; eauto.
- (* function internal *)
inversion TRANSF as [xf tf MF |]; subst.
eexists; split.
+ econstructor. erewrite <- preserv_fnstacksize; eauto.
+ generalize (trivial_glueinv_entrypoint _ _ MF)
(trivial_histinv_entrypoint _ _ MF)
(trivial_meminv_entrypoint _ _ MF).
erewrite preserv_fnparams; eauto.
erewrite preserv_entrypoint; eauto.
intros ONLYh ONLYg ONLYm.
econstructor; eauto.
eapply only_liveness_match_invs; eauto.
- (* function external *)
inv TRANSF. eexists; split; econstructor; eauto.
eapply external_call_symbols_preserved; eauto. apply senv_preserved.
- (* return *)
inv STACKS. destruct b1 as [res' f' sp' pc' rs'].
eexists; split.
+ econstructor.
+ inv H1. econstructor; eauto.
Qed.

Theorem transf_program_correct:
forward_simulation (sem AnnotUndef prog) (sem AnnotUndef tprog).
Proof.
eapply forward_simulation_step with (match_states pge); simpl; eauto. (* lock-step with respect to match_states *)
- eapply senv_preserved.
- eapply transf_initial_states.
- eapply transf_final_states.
- intros; eapply step_simulation; eauto.
Qed.

End PRESERVATION.

Program Definition ipass : IPass (BTL.sem AnnotUndef) (BTL.sem AnnotUndef) :=
{|
ipass_spec := pass;
ipass_impl := transf_program;
|}.
Next Obligation.
apply transf_program_match; assumption. Qed.
Next Obligation.
apply transf_program_correct; assumption. Qed.

End BTL_BlockSimulationproof.

Module Type BTL_BlockSimulationCompConfig.
Include BTL_BlockSimulationConfig.
Parameter analyse : IPass (BTL.sem AnnotTrap) (BTL.sem AnnotTrap).
End BTL_BlockSimulationCompConfig.

Module BTL_BlockSimulationComp (B: BTL_BlockSimulationCompConfig).
Export B.
Module Simu := BTL_BlockSimulationproof B.

Local Open Scope ipass_scope.

Definition ipass : IPass (BTL.sem AnnotNone) (BTL.sem AnnotNone) :=
BTL_ResetAnnots.ipass _ :::
analyse :::
ipass_simu Trap_to_Undef.transf_program :::
Simu.ipass :::
ipass_simu Undef_to_Lax.transf_program.

End BTL_BlockSimulationComp.