Commit 63cd7f42 authored by Hai Dang's avatar Hai Dang
Browse files

WIP: different init state

parent 7adcabfc
......@@ -88,7 +88,7 @@ Definition never_stuck fs e σ :=
e' σ', (e, σ) ~{fs}~>* (e', σ') terminal e' reducible fs e' σ'.
Definition init_expr := (Call #["main"] []).
Definition init_state := (mkState [] O O).
Definition init_state := (mkState [O] O 1).
(*=================================== UNUSED =================================*)
(* Implicit Type (ρ: cfg bor_lang). *)
......
......@@ -6,7 +6,8 @@ Set Default Proof Using "Type".
Lemma wf_init_state : Wf init_state.
Proof.
constructor; simpl; try (intros ?; set_solver).
by apply NoDup_nil.
- by apply NoDup_singleton.
- intros ??%elem_of_list_singleton. subst. lia.
Qed.
(** Steps preserve wellformedness *)
......
......@@ -94,14 +94,20 @@ Definition end_call_sat (r: resUR) (σs σt: state) : Prop :=
l st, l dom (gset loc) h σt.(shp) !! l = Some st
ss, σs.(shp) !! l = Some ss arel (r_f r) ss st).
Lemma wsat_init_state : wsat ε init_state init_state.
Definition init_res : resUR := (ε, {[O := to_callStateR csPub]}).
Lemma wsat_init_state : wsat init_res init_state init_state.
Proof.
split; last split; last split; last split; last split.
- apply wf_init_state.
- apply wf_init_state.
- done.
- split; [done|]. intros ?; simpl. destruct i.
+ rewrite lookup_singleton //.
+ rewrite lookup_singleton_ne //.
- intros ??? HL. exfalso. move : HL. rewrite /= lookup_empty. inversion 1.
- intros ?? HL. exfalso. move : HL. rewrite /= lookup_empty. inversion 1.
- intros ??. simpl. destruct c.
+ rewrite lookup_singleton. intros Eq%Some_equiv_inj.
destruct cs as [[]| |]; [..|lia|]; inversion Eq.
+ rewrite lookup_singleton_ne //. inversion 1.
- repeat split. simpl. set_solver.
Qed.
......
......@@ -59,7 +59,9 @@ Inductive _sim_local_body_step (r_f : A) (sim_local_body : SIM)
(CONT: r' v_src v_tgt σs' σt'
(* For any new resource r' that supports the returned values are
related w.r.t. (r r' r_f) *)
(VRET: vrel r' (Val v_src) (Val v_tgt)),
(VRET: vrel r' (Val v_src) (Val v_tgt))
(* Stack unchanged *)
(STACK: σt'.(sst) = σt.(sst)),
idx', sim_local_body (rc r') idx'
(fill Ks (Val v_src)) σs'
(fill Kt (Val v_tgt)) σt' Φ).
......@@ -100,6 +102,27 @@ Qed.
Definition sim_local_body := paco7 _sim_local_body bot7.
Lemma sim_local_body_post_mono r n es σs et σt Φ Φ' :
Φ <6= Φ'
sim_local_body r n es σs et σt Φ sim_local_body r n es σs et σt Φ'.
Proof.
revert r n es σs et σt Φ Φ'. pcofix CIH. intros r0 n es σs et σt Φ Φ' LE SIM.
pfold. punfold SIM; [|apply sim_local_body_mono].
intros NT r_f WSAT. specialize (SIM NT r_f WSAT) as [NOTS TE SIM].
constructor; [done|..].
{ intros.
destruct (TE _ TERM) as (vs' & σs' & r' & idx' & STEP' & WSAT' & HΦ).
naive_solver. }
inversion SIM.
- left. intros.
specialize (STEP _ _ STEPT) as (es' & σs' & r' & idx' & STEP' & WSAT' & SIM').
exists es', σs', r', idx'. do 2 (split; [done|]).
pclearbot. right. eapply CIH; eauto.
- econstructor 2; eauto. intros.
destruct (CONT _ _ _ σs' σt' VRET STACK) as [idx' SIM'].
exists idx'. pclearbot. right. eapply CIH; eauto.
Qed.
(* Simulating functions:
- We start after the substitution.
- We assume the arguments are values related by [r]
......
......@@ -80,7 +80,7 @@ Inductive sim_local_conf:
Ke_src Ke_tgt
(FRAMES: sim_local_frames r_f K_src K_tgt frames)
(LOCAL: sim_local_body wsat vrel fns fnt rc idx e_src σ_src e_tgt σ_tgt
(λ r _ vs _ vt _, vrel r (of_result vs) (of_result vt)))
(λ r _ vs σs vt σt, esat r σs σt vrel r (of_result vs) (of_result vt)))
(KE_SRC: Ke_src = fill K_src e_src)
(KE_TGT: Ke_tgt = fill K_tgt e_tgt)
(WSAT: wsat (r_f rc) σ_src σ_tgt)
......@@ -101,7 +101,7 @@ Proof.
destruct sim_local_body_stuck as [vt Eqvt].
rewrite -(of_to_result _ _ Eqvt).
destruct (sim_local_body_terminal _ Eqvt)
as (vs' & σs' & r' & idx' & SS' & WSAT' & VREL).
as (vs' & σs' & r' & idx' & SS' & WSAT' & ESAT' & VREL).
have STEPK: (fill (Λ:=bor_ectxi_lang fns) K_src0 e_src0, σ_src)
~{fns}~>* (fill (Λ:=bor_ectxi_lang fns) K_src0 vs', σs').
{ apply fill_tstep_rtc. destruct SS' as [|[? Eq]].
......@@ -134,16 +134,13 @@ Proof.
inv FRAMES; ss.
{ exfalso. apply result_tstep_stuck in H. naive_solver. }
apply fill_step_inv_2 in H. des; ss. subst.
apply tstep_end_call_inv in H0; cycle 1.
{ unfold terminal. rewrite x0. eauto. }
des. subst.
destruct (VREL_VAL _ _ _ x2) as (vs1 & v1 & Eqvs1 & Eqv1 & VREL1).
exploit CONTINUATION; eauto.
{ rewrite cmra_assoc; eauto. }
i. des.
destruct (VREL_VAL _ _ _ x3) as (vs1 & v1 & Eqvs1 & Eqv1 & VREL1).
have STEPK: (fill (Λ:= bor_ectxi_lang fns)
(EndCallCtx :: K_src frame0 ++ K_f_src) e_src0, σ_src)
......@@ -155,6 +152,11 @@ Proof.
edestruct NT3 as [[? TERM]|[es [σs1 STEP1]]].
{ constructor 1. } { by rewrite /= fill_not_result in TERM. }
exploit CONTINUATION; eauto.
{ rewrite cmra_assoc; eauto. }
i. des.
have Eqes: es = fill (K_src frame0 ++ K_f_src) (Val vs1).
{ rewrite /= in STEP1.
apply fill_tstep_inv in STEP1 as [e2' [Eq2' STEP2']]; [|done]. subst es.
......@@ -173,7 +175,7 @@ Proof.
* inversion EQ. econs.
+ (* EndCall step *)
apply tc_once; eauto.
- right. apply CIH. econs; eauto; cycle 1.
- right. apply CIH. simpl in STEP1. econs; eauto; cycle 1.
+ rewrite fill_app. eauto.
+ rewrite fill_app. eauto.
+ admit. (* wsat after return HAI: property of wsat *)
......@@ -205,8 +207,9 @@ Proof.
* right. apply CIH. econs.
{ econs 2; eauto. i. instantiate (1 := mk_frame _ _ _). ss.
destruct (CONT _ _ _ σ_src' σ_tgt' VRET).
pclearbot. esplits; eauto. }
{ admit. }
pclearbot. esplits; eauto. admit. }
{ (* eapply sim_local_body_post_mono; [|apply SIMf]. simpl. naive_solver. *)
eauto. }
{ s. ss. }
{ s. rewrite -fill_app. eauto. }
{ s. rewrite -cmra_assoc; eauto. }
......
......@@ -27,28 +27,6 @@ Proof.
apply (UPD O (Some r_f)); [by apply cmra_discrete_valid_iff|by rewrite /= comm].
Qed.
Lemma sim_body_post_mono fs ft r n es σs et σt Φ Φ' :
Φ' <6= Φ
r {n,fs,ft} (es, σs) (et, σt) : Φ'
r {n,fs,ft} (es, σs) (et, σt) : Φ.
Proof.
revert r n es σs et σt Φ Φ'. pcofix CIH. intros r0 n es σs et σt Φ Φ' LE SIM.
pfold. punfold SIM.
intros NT r_f WSAT. specialize (SIM NT r_f WSAT) as [NOTS TE SIM].
constructor; [done|..].
{ intros.
destruct (TE _ TERM) as (vs' & σs' & r' & idx' & STEP' & WSAT' & HΦ').
naive_solver. }
inversion SIM.
- left. intros.
specialize (STEP _ _ STEPT) as (es' & σs' & r' & idx' & STEP' & WSAT' & SIM').
exists es', σs', r', idx'. do 2 (split; [done|]).
pclearbot. right. eapply CIH; eauto.
- econstructor 2; eauto. intros.
destruct (CONT _ _ _ σs' σt' VRET) as [idx' SIM'].
exists idx'. pclearbot. right. eapply CIH; eauto.
Qed.
Lemma sim_body_bind fs ft r n
(Ks: list (ectxi_language.ectx_item (bor_ectxi_lang fs)))
(Kt: list (ectxi_language.ectx_item (bor_ectxi_lang ft))) es et σs σt Φ :
......@@ -123,8 +101,8 @@ Proof.
{ pclearbot. left. eapply paco7_mon_bot; eauto. }
+ eapply (sim_local_body_step_over_call _ _ _ _ _ _ _ _ _ _ _ _ _
Ks1 Kt1 fid el_tgt _ _ _ _ CALLTGT); eauto; [by etrans|].
intros r4 vs4 vt4 σs4 σt4 VREL4.
destruct (CONT _ _ _ σs4 σt4 VREL4) as [idx4 CONT4].
intros r4 vs4 vt4 σs4 σt4 VREL4 STACK4.
destruct (CONT _ _ _ σs4 σt4 VREL4 STACK4) as [idx4 CONT4].
exists idx4. pclearbot. left. eapply paco7_mon_bot; eauto.
- (* et makes a step *)
constructor 1. intros.
......@@ -140,8 +118,8 @@ Proof.
eapply (sim_local_body_step_over_call _ _ _ _ _ _ _ _ _ _ _ _ _
(Ks1 ++ Ks) (Kt1 ++ Kt) fid el_tgt); [by rewrite CALLTGT fill_app|..];
eauto; [rewrite fill_app; by apply fill_tstep_rtc|].
intros r' vs' vt' σs' σt' VREL'.
destruct (CONT _ _ _ σs' σt' VREL') as [idx' CONT2]. clear CONT.
intros r' vs' vt' σs' σt' VREL' STACK'.
destruct (CONT _ _ _ σs' σt' VREL' STACK') as [idx' CONT2]. clear CONT.
exists idx'. rewrite 2!fill_app.
pclearbot. right. by apply CIH. }
Qed.
......@@ -773,7 +751,7 @@ Lemma sim_body_step_over_call fs ft
(FT: ft !! fid = Some (@FunV xlt et HCt))
(VT : Forall (λ ei, is_Some (to_value ei)) elt)
(ST: subst_l xlt elt et = Some et') :
( r' vs vt σs' σt' (VRET: vrel r' vs vt), n',
( r' vs vt σs' σt' (VRET: vrel r' vs vt) (STACK: σt'.(sst) = σs.(sst)), n',
rc r' {n',fs,ft} (fill Ks (Val vs), σs') (fill Kt (Val vt), σt') : Φ)
rc rv {n,fs,ft}
(fill Ks (Call #[ScFnPtr fid] els), σs) (fill Kt (Call #[ScFnPtr fid] elt), σt) : Φ.
......@@ -784,8 +762,11 @@ Proof.
{ intros vt. by rewrite fill_not_result. }
eapply (sim_local_body_step_over_call _ _ _ _ _ _ _ _ _ _ _ _ _
Ks _ fid elt els); eauto; [done|].
intros r' ? ? σs' σt' (vs&vt&?&?&VR). simplify_eq.
destruct (CONT _ _ _ σs' σt' VR) as [n' ?]. exists n'. by left.
intros r' ? ? σs' σt' (vs&vt&?&?&VR) STK. simplify_eq.
destruct (CONT _ _ _ σs' σt' VR) as [n' ?].
- destruct WSAT as (?&?&?&?&?&SREL).
destruct SREL as (Eqst&?&?). by rewrite Eqst.
- exists n'. by left.
Qed.
(** Call - step into *)
......
......@@ -16,16 +16,20 @@ Proof.
specialize (SIMf ε ebs ebt [] [] init_state init_state) as [idx SIM]; [done..|].
unfold behave_prog. eapply (adequacy _ _ idx); [apply _| |by apply wf_init_state..].
eapply sim_local_conf_sim; eauto.
econs; eauto; swap 2 4.
econs; swap 2 4.
- econs 1.
- ss.
- ss.
- eapply (sim_body_step_into_call _ _ _ _ _ [] ebs HCs [] ebs [] ebt HCt [] ebt);
- eapply (sim_body_step_over_call _ _ [] [] init_res ε _ _ [] [] ebt ebt [] HCt);
[done..|].
intros r' vs vt σs' σt' VREL'.
admit.
(* eapply (sim_body_step_into_call _ _ _ _ _ [] ebs HCs [] ebs [] ebt HCt [] ebt);
[done..|].
eapply (sim_body_bind _ _ _ _ [EndCallCtx] [EndCallCtx] (InitCall ebs) (InitCall ebt)).
eapply sim_body_post_mono; [|exact SIM].
eapply sim_local_body_post_mono; [|exact SIM].
clear SIM. simpl.
intros r1 idx1 vs σs vt σt [ESAT (v1 & v2 & Eq1 & Eq2 & VREL)].
rewrite Eq1 Eq2. by apply sim_body_end_call.
- rewrite right_id. apply wsat_init_state.
rewrite Eq1 Eq2. by apply sim_body_end_call. *)
- instantiate (1:=ε). rewrite right_id left_id. apply wsat_init_state.
Qed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment