Commit 5f73e2f1 authored by Hai Dang's avatar Hai Dang
Browse files

WIP: fixing adequacy

parent 63cd7f42
......@@ -60,8 +60,7 @@ Inductive _sim_local_body_step (r_f : A) (sim_local_body : SIM)
(* 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))
(* Stack unchanged *)
(STACK: σt'.(sst) = σt.(sst)),
(STACK: σt'.(scs) = σt.(scs)),
idx', sim_local_body (rc r') idx'
(fill Ks (Val v_src)) σs'
(fill Kt (Val v_tgt)) σt' Φ).
......@@ -141,7 +140,10 @@ Definition sim_local_fun
end),
idx, sim_local_body r idx
(InitCall es) σs (InitCall et) σt
(λ r _ vs σs vt σt, esat r σs σt vrel r (of_result vs) (of_result vt)).
(λ r' _ vs' σs' vt' σt',
( c, σt'.(scs) = c :: σt.(scs))
esat r' σs' σt'
vrel r' (of_result vs') (of_result vt')).
Definition sim_local_funs (esat: A state state Prop) : Prop :=
name fn_tgt, fnt !! name = Some fn_tgt fn_src,
......
......@@ -2,7 +2,7 @@ From Coq Require Import Program.Equality Lia.
From Paco Require Import paco.
From stbor.lang Require Import steps_wf steps_inversion.
From stbor.sim Require Import behavior global local invariant sflib global_adequacy.
From stbor.sim Require Import behavior global local invariant sflib global_adequacy one_step.
Set Default Proof Using "Type".
......@@ -16,32 +16,16 @@ Proof.
Qed.
Section local.
Context {A: ucmraT}.
Variable (wsat esat: A state state Prop).
Variable (vrel: A expr expr Prop).
Variable (fns fnt: fn_env).
Hypothesis WSAT_PROPER: Proper (() ==> (=) ==> (=) ==> iff) wsat.
Hypothesis VREL_RESULT:
(r: A) (e1 e2: result), vrel r e1 e2 to_result e1 = Some e2.
Hypothesis VREL_VAL :
(r: A) (e1 e2: result),
vrel r e1 e2 v1 v2, e1 = ValR v1 e2 = ValR v2 vrel r (Val v1) (Val v2).
Hypothesis ENDCALL_RED:
r σs σt (vs vt: value) es' σs',
wsat r σs σt (EndCall vs, σs) ~{fns}~> (es', σs') reducible fnt (EndCall vt) σt.
Record frame: Type := mk_frame {
rc: A;
rc: resUR;
K_src: list (ectxi_language.ectx_item (bor_ectxi_lang fns));
K_tgt: list (ectxi_language.ectx_item (bor_ectxi_lang fnt));
}.
(* TODO: move *)
Notation PRED := (A nat result state result state Prop)%type.
Inductive sim_local_frames:
forall (r_f:A)
forall (r_f: resUR)
(K_src: list (ectxi_language.ectx_item (bor_ectxi_lang fns)))
(K_tgt: list (ectxi_language.ectx_item (bor_ectxi_lang fnt)))
(frames:list frame),
......@@ -59,12 +43,14 @@ Inductive sim_local_frames:
our local resource r and have world satisfaction *)
(WSAT' : wsat (r_f (frame.(rc) r')) σ_src' σ_tgt')
(* and the returned values are related w.r.t. (r r' r_f) *)
(VRET : vrel r' (Val v_src) (Val v_tgt)),
idx', sim_local_body wsat vrel fns fnt
(VRET : vrel_expr r' (Val v_src) (Val v_tgt)),
idx', sim_local_body wsat vrel_expr fns fnt
(frame.(rc) r') idx'
(fill frame.(K_src) (Val v_src)) σ_src'
(fill frame.(K_tgt) (Val v_tgt)) σ_tgt'
(λ r _ vs σs vt σt, vrel r (of_result vs) (of_result vt)))
(λ r _ vs σs vt σt,
end_call_sat r σs σt
vrel_expr r (of_result vs) (of_result vt)))
: sim_local_frames
(r_f frame.(rc))
(EndCallCtx :: frame.(K_src) ++ K_f_src)
......@@ -79,15 +65,17 @@ Inductive sim_local_conf:
rc idx e_src σ_src e_tgt σ_tgt
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 σs vt σt, esat r σs σt vrel r (of_result vs) (of_result vt)))
(LOCAL: sim_local_body wsat vrel_expr fns fnt rc idx e_src σ_src e_tgt σ_tgt
(λ r _ vs σs vt σt,
end_call_sat r σs σt
vrel_expr 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)
: sim_local_conf idx Ke_src σ_src Ke_tgt σ_tgt.
Lemma sim_local_conf_sim
(FUNS: sim_local_funs wsat vrel fns fnt esat)
(FUNS: sim_local_funs wsat vrel_expr fns fnt end_call_sat)
(idx:nat) (e_src:expr) (σ_src:state) (e_tgt:expr) (σ_tgt:state)
(SIM: sim_local_conf idx e_src σ_src e_tgt σ_tgt)
: sim fns fnt idx (e_src, σ_src) (e_tgt, σ_tgt)
......@@ -107,7 +95,7 @@ Proof.
{ apply fill_tstep_rtc. destruct SS' as [|[? Eq]].
by apply tc_rtc. clear -Eq. simplify_eq. constructor. }
have NT3:= never_stuck_tstep_rtc _ _ _ _ _ STEPK NEVER_STUCK.
clear -STEPK NT3 FRAMES WSAT' VREL ENDCALL_RED VREL_VAL.
clear -STEPK NT3 FRAMES WSAT' VREL.
inversion FRAMES. { left. rewrite to_of_result. by eexists. }
right. subst K_src0 K_tgt0.
move : NT3. simpl. intros NT3.
......@@ -117,14 +105,14 @@ Proof.
apply tstep_reducible_fill_inv in RED; [|done].
apply tstep_reducible_fill.
destruct RED as [e2 [σ2 Eq2]].
apply VREL_VAL in VREL as (v1 & v2 & ? & ? & ?). subst vs' vt.
move : Eq2. eapply ENDCALL_RED; eauto.
apply vrel_expr_result in VREL as (v1 & v2 & ? & ? & ?). subst vs' vt.
move : Eq2. eapply end_call_tstep_src_tgt; eauto.
- guardH sim_local_body_stuck.
s. i. apply fill_result in H. unfold terminal in H. des. subst. inv FRAMES. ss.
exploit sim_local_body_terminal; eauto. i. des.
esplits; eauto; ss.
+ rewrite to_of_result. esplits; eauto.
+ ii. clarify. eapply VREL_RESULT; eauto.
+ ii. clarify. eapply vrel_expr_to_result; eauto.
- guardH sim_local_body_stuck.
i. destruct eσ2_tgt as [e2_tgt σ2_tgt].
......@@ -134,14 +122,15 @@ Proof.
inv FRAMES; ss.
{ exfalso. apply result_tstep_stuck in H. naive_solver. }
destruct (fill_step_inv_2 _ _ _ _ _ _ H) as [?|?]; des; ss. subst.
apply fill_step_inv_2 in H. des; ss. subst.
apply tstep_end_call_inv in H0; cycle 1.
apply tstep_end_call_inv in H1; cycle 1.
{ unfold terminal. rewrite x0. eauto. }
des. subst.
destruct (VREL_VAL _ _ _ x3) as (vs1 & v1 & Eqvs1 & Eqv1 & VREL1).
destruct (vrel_expr_result _ _ _ x3) as (vs1 & vt1 & Eqvs1 & Eqv1 & VREL1).
have VR: vrel r' vs1 vt1. { SearchAbout vrel_expr vrel. admit. }
sim_body_end_call fns fnt r' idx' vs1 vt1 σs' σ_tgt _ VR x2
have STEPK: (fill (Λ:= bor_ectxi_lang fns)
(EndCallCtx :: K_src frame0 ++ K_f_src) e_src0, σ_src)
~{fns}~>* (fill (Λ:= bor_ectxi_lang fns)
......@@ -152,7 +141,8 @@ 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.
......@@ -165,6 +155,7 @@ Proof.
[|rewrite to_of_result; by eexists].
rewrite Eq4. rewrite Eqvs1 /= in Eq3. by inversion Eq3. } subst es.
esplits.
- left. eapply tc_rtc_l.
+ apply fill_tstep_rtc. instantiate (1 := σs'). instantiate (1 := EndCall vs').
......@@ -175,7 +166,8 @@ Proof.
* inversion EQ. econs.
+ (* EndCall step *)
apply tc_once; eauto.
- right. apply CIH. simpl in STEP1. 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,11 +197,18 @@ Proof.
{ econs. rewrite -fill_app. eapply (head_step_fill_tstep).
econs; econs; eauto. }
* right. apply CIH. econs.
{ econs 2; eauto. i. instantiate (1 := mk_frame _ _ _). ss.
destruct (CONT _ _ _ σ_src' σ_tgt' VRET). admit.
pclearbot. esplits; eauto.
(* eapply sim_local_body_post_mono; [|apply H]. simpl. naive_solver. *) }
{ rewrite -(fill_app [EndCallCtx]). eauto. }
{ rewrite -(fill_app [EndCallCtx]). eauto. }
{ econs 2; eauto. i. instantiate (1 := mk_frame _ _ _). ss.
destruct (CONT _ _ _ σ_src' σ_tgt' VRET).
pclearbot. esplits; eauto. admit. }
{ (* eapply sim_local_body_post_mono; [|apply SIMf]. simpl. naive_solver. *)
eauto. }
pclearbot. esplits; eauto.
(* eapply sim_local_body_post_mono; [|apply H]. simpl. naive_solver. *) }
{ eapply sim_local_body_post_mono; [|apply SIMf]. simpl. naive_solver. }
{ s. ss. }
{ s. rewrite -fill_app. eauto. }
{ s. rewrite -cmra_assoc; eauto. }
......
......@@ -127,6 +127,20 @@ Qed.
(** MEM STEP -----------------------------------------------------------------*)
(** Copy *)
Lemma sim_body_copy_public fs ft r n l t Ts Tt σs σt Φ
(EQS: tsize Ts = tsize Tt)
(PUBLIC: (h: heapletR), r.1 !! t Some (to_tagKindR tkPub, h)) :
( vs vt,
read_mem l (tsize Ts) σs.(shp) = Some vs
read_mem l (tsize Tt) σt.(shp) = Some vt
α', memory_read σt.(sst) σt.(scs) l (Tagged t) (tsize Tt) = Some α'
let σs' := mkState σs.(shp) α' σs.(scs) σs.(snp) σs.(snc) in
let σt' := mkState σt.(shp) α' σt.(scs) σt.(snp) σt.(snc) in
vrel r vs vt Φ r n (ValR vs) σs' (ValR vt) σt' : Prop)
r {n,fs,ft} (Copy (Place l (Tagged t) Ts), σs) (Copy (Place l (Tagged t) Tt), σt) : Φ.
Proof.
Abort.
Lemma sim_body_copy fs ft r n l tg Ts Tt σs σt Φ
(EQS: tsize Ts = tsize Tt) :
( vs vt,
......@@ -639,15 +653,22 @@ Proof.
econstructor. by econstructor. econstructor. by rewrite -Eqcs'.
Qed.
Lemma sim_body_end_call fs ft r n vs vt σs σt :
Lemma sim_body_end_call fs ft r n vs vt σs σt Φ :
(* return values are related *)
vrel r vs vt
(* and any private location w.r.t to the current call id ownership must be related *)
end_call_sat r σs σt
r {n,fs,ft} (EndCall (Val vs), σs) (EndCall (Val vt), σt) :
(λ r _ vs _ vt _, vrel_expr r (of_result vs) (of_result vt)).
( c1 c2 cids1 cids2, σs.(scs) = c1 :: cids1 σt.(scs) = c2 :: cids2
let σs' := mkState σs.(shp) σs.(sst) cids1 σs.(snp) σs.(snc) in
let σt' := mkState σt.(shp) σt.(sst) cids2 σt.(snp) σt.(snc) in
let r2' := match (r.2 !! c2) with
| Some (Cinl (Excl T)) => <[c2 := to_callStateR csPub]> r.2
| _ => r.2
end in
Φ (r.1, r2') n (ValR vs) σs' (ValR vt) σt' : Prop)
r {n,fs,ft} (EndCall (Val vs), σs) (EndCall (Val vt), σt) : Φ.
Proof.
intros VREL ESAT. pfold. intros NT r_f WSAT.
intros VREL ESAT POST. pfold. intros NT r_f WSAT.
split; [|done|].
{ right.
destruct (NT (EndCall #vs) σs) as [[]|[es' [σs' STEPS]]]; [done..|].
......@@ -668,10 +689,11 @@ Proof.
| Some (Cinl (Excl T)) => <[c := to_callStateR csPub]> r.2
| _ => r.2
end.
exists (r.1, r2'), (S n). split; last split.
exists (r.1, r2'), (S n).
destruct WSAT as (WFS & WFT & VALID & PINV & CINV & SREL).
split; last split.
{ left. by constructor 1. }
{ destruct WSAT as (WFS & WFT & VALID & PINV & CINV & SREL).
destruct r_f as [r_f1 r_f2].
{ destruct r_f as [r_f1 r_f2].
have VALID': ((r_f1, r_f2) (r.1, r2')).
{ apply (local_update_discrete_valid_frame _ _ _ VALID).
destruct (r.2 !! c) as [[[T|]| |]|] eqn:Eqr2; rewrite /r2'; [|by destruct r..].
......@@ -735,7 +757,8 @@ Proof.
exists (ValR vs). do 2 eexists. exists n. split; last split.
{ right. split; [lia|]. eauto. }
{ eauto. }
exists vs, vt. do 2 (split; [done|]). by apply (Forall2_impl _ _ _ _ VREL). }
destruct SREL as (?&?&Eqs&?).
eapply POST; eauto. by rewrite Eqs. }
{ left. by eexists. }
Qed.
......@@ -751,7 +774,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) (STACK: σt'.(sst) = σs.(sst)), n',
( r' vs vt σs' σt' (VRET: vrel r' vs vt), 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) : Φ.
......@@ -762,11 +785,9 @@ 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) STK. simplify_eq.
intros r' ? ? σs' σt' (vs&vt&?&?&VR). simplify_eq.
destruct (CONT _ _ _ σs' σt' VR) as [n' ?].
- destruct WSAT as (?&?&?&?&?&SREL).
destruct SREL as (Eqst&?&?). by rewrite Eqst.
- exists n'. by left.
exists n'. by left.
Qed.
(** Call - step into *)
......
......@@ -20,9 +20,19 @@ Proof.
- econs 1.
- ss.
- ss.
- eapply (sim_body_step_over_call _ _ [] [] init_res ε _ _ [] [] ebt ebt [] HCt);
- eapply (sim_body_step_into_call _ _ _ _ _ [] ebs HCs [] ebs [] ebt HCt [] ebt);
[done..|].
intros r' vs vt σs' σt' VREL'.
eapply (sim_body_bind _ _ _ _ [EndCallCtx] [EndCallCtx] (InitCall ebs) (InitCall ebt)).
eapply sim_local_body_post_mono; [|exact SIM].
clear SIM. simpl.
intros r1 idx1 vs σs vt σt ([c Eqc] & ESAT & (v1 & v2 & Eq1 & Eq2 & VREL)).
rewrite Eq1 Eq2. eapply (sim_body_end_call); [done..|].
intros c1 c2 cids1 cids2 Eqcs1 Eqcs2 σs' σt' r'.
split; last by do 2 eexists.
rewrite Eqc in Eqcs2. simplify_eq.
rewrite /end_call_sat /=.
intros ??. simplify_eq.
intros.
admit.
(* eapply (sim_body_step_into_call _ _ _ _ _ [] ebs HCs [] ebs [] ebt HCt [] ebt);
[done..|].
......@@ -31,5 +41,5 @@ Proof.
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. *)
- instantiate (1:=ε). rewrite right_id left_id. apply wsat_init_state.
- instantiate (1:=init_res). rewrite right_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