Commit 864b447d authored by Jeehoon Kang's avatar Jeehoon Kang 😴
Browse files

Finish high-level structure of local adequacy

parent 3c1ec780
From Paco Require Import paco.
From stbor.lang Require Export defs.
From stbor.sim Require Export sflib.
CoInductive diverges
(step: expr * config expr * config Prop)
......@@ -38,7 +39,7 @@ Record sim_base (sim: SIM_CONFIG) (idx1: nat) (eσ1_src eσ1_tgt: expr * state)
(* (2) If [eσ1_tgt] is terminal, then [eσ1_src] terminates with some steps. *)
sim_terminal :
terminal eσ1_tgt.1 idx2 eσ2_src,
(eσ1_src ~{fns}~>+ eσ2_src ((idx2 < idx1)%nat eσ1_src = eσ2_src))
sflib.__guard__ (eσ1_src ~{fns}~>+ eσ2_src ((idx2 < idx1)%nat eσ1_src = eσ2_src))
terminal eσ2_src.1 sim_expr_terminal eσ2_src.1 eσ1_tgt.1 ;
(* (3) If [eσ1_tgt] steps to [eσ2_tgt] with 1 step,
then exists [eσ2_src] s.t. [eσ1_src] steps to [eσ2_src] with * step. *)
......
......@@ -75,12 +75,15 @@ Proof.
clear SIM. intro SIM. inv SIM. inv MAT.
+ exfalso. destruct sim_stuck as [[v TE]|ST].
* by apply (NT v).
* admit.
+ exploit sim_terminal; eauto. i. revert sim_stuck. intros _. pfold. des.
* econs; eauto. etrans. apply tc_rtc; eauto.
rename x2 into SE.
admit.
* econs; eauto. admit.
* unfold reducible in ST. des. eapply NS.
destruct x. eauto.
+ clear sim_stuck. exploit sim_terminal; eauto. i. des.
pfold. econs.
* instantiate (1 := eσ2_src). unguardH x0. des.
{ apply tc_rtc. eauto. }
{ subst. reflexivity. }
* unfold terminal in *. des.
econs 2. unfold term. erewrite x2; eauto.
+ pclearbot. exploit sim_step; eauto. i. revert sim_stuck. des.
* inv x1; ss.
exploit CIH; eauto. intros ?.
......
......@@ -2,6 +2,7 @@ From Paco Require Export paco.
From iris.algebra Require Import cmra gmap csum agree excl.
From stbor.lang Require Import defs.
From stbor.sim Require Import sflib.
Set Default Proof Using "Type".
......@@ -75,8 +76,8 @@ Record sim_local_body_base (r_f: A) (sim_local_body : SIM)
vt (TERM: to_result et = Some vt),
(* then src can get terminal *)
vs' σs' r' idx',
((es, σs) ~{fns}~>+ (of_result vs', σs')
((idx' < idx)%nat (of_result vs', σs') = (es, σs)))
sflib.__guard__ ((es, σs) ~{fns}~>+ (of_result vs', σs')
((idx' < idx)%nat (es, σs) = (of_result vs', σs')))
(* and re-establish wsat *)
wsat (r_f r') σs' σt Φ r' idx' vs' σs' vt σt ;
sim_local_body_step :
......
From Coq Require Import Program.Equality Lia.
From Paco Require Import paco.
From stbor.lang Require Import steps_wf.
From stbor.lang Require Import steps_wf steps_inversion.
From stbor.sim Require Import behavior global local invariant sflib global_adequacy.
Set Default Proof Using "Type".
......@@ -21,6 +21,13 @@ Lemma fill_step
Proof.
Admitted.
Lemma fill_item_steps
fn K e1 σ1 e2 σ2
(STEP: (e1, σ1) ~{fn}~>* (e2, σ2)):
(fill_item K e1, σ1) ~{fn}~>* (fill_item K e2, σ2).
Proof.
Admitted.
Lemma fill_steps
fn K e1 σ1 e2 σ2
(STEP: (e1, σ1) ~{fn}~>* (e2, σ2)):
......@@ -77,8 +84,8 @@ Inductive sim_local_frames:
(λ r _ vs _ vt _, vrel r (of_result vs) (of_result vt)))
: sim_local_frames
(r_f frame.(rc))
(frame.(K_src) ++ K_f_src)
(frame.(K_tgt) ++ K_f_tgt)
(EndCallCtx :: frame.(K_src) ++ K_f_src)
(EndCallCtx :: frame.(K_tgt) ++ K_f_tgt)
(frame :: frames)
.
......@@ -108,21 +115,44 @@ Proof.
{ admit. (* never_stuck *) }
clear LOCAL. intro LOCAL. inv LOCAL. econs.
- ii. admit. (* stuck_fill_rev *)
- s. i. subst. apply fill_result in H. revert sim_local_body_stuck. des.
unfold terminal in H. des. subst. ss.
exploit sim_local_body_terminal; eauto. intros ?. des.
clear NEVER_STUCK WSAT.
clear sim_local_body_terminal sim_local_body_step. intros _.
assert (VS': to_result vs' = Some x) by admit.
induction FRAMES; ss.
{ esplits; eauto; ss. ii. clarify. }
admit. (* global sim should have generalized index *)
admit.
- i. destruct eσ2_tgt as [e2_tgt σ2_tgt].
exploit fill_step_rev; eauto. i. revert sim_local_body_stuck. des; cycle 1.
- 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. admit. (* vrel, to_result *)
- guardH sim_local_body_stuck.
i. destruct eσ2_tgt as [e2_tgt σ2_tgt].
exploit fill_step_rev; eauto. i. des; cycle 1.
{ (* return *)
admit. (* similar to the above case *)
exploit sim_local_body_terminal; eauto. i. des.
inv FRAMES; ss.
{ admit. (* conflict: [(e_tgt0, σ_tgt) ~{fnt}~> (e2_tgt, σ2_tgt)] and [to_result e_tgt0 = Some v] *) }
apply fill_step_rev in H. des; ss. subst.
apply tstep_end_call_inv in H0; cycle 1.
{ unfold terminal. rewrite x0. eauto. }
des. subst.
exploit CONTINUATION; eauto.
{ admit. (* wsat assoc *) }
{ admit. (* vrel #? *) }
i. des.
esplits.
- left. eapply tc_rtc_l.
+ apply fill_steps. instantiate (1 := σs'). instantiate (1 := EndCall vs').
admit. (* EndCallCtx *)
+ econs 1. apply fill_step.
admit. (* EndCall step *)
- right. apply CIH. econs; eauto.
+ rewrite fill_app. eauto.
+ rewrite fill_app. eauto.
+ admit. (* wsat after return *)
}
subst. clear H. inv sim_local_body_step.
+ (* step *)
exploit STEP; eauto. intros (es' & σs' & r' & idx' & STEP' & WSAT' & SIM').
......@@ -133,11 +163,13 @@ Proof.
{ inv STEP'0. ss. }
* right. apply CIH. econs; eauto.
+ (* call *)
exploit fill_step_rev; eauto. i. des; ss.
exploit tstep_call_inv; try exact x2; eauto. i. des. subst.
esplits.
* left. eapply tc_rtc_l.
{ apply fill_steps. eauto. }
{ instantiate (1 := (fill K_src0 (fill Ks _), _)).
admit. (* call has a matching step *)
{ econs. apply fill_step.
admit. (* Call #[fid] has a step *)
}
* right. apply CIH. econs.
{ econs 2; eauto. i. instantiate (1 := mk_frame _ _ _). ss.
......@@ -146,8 +178,8 @@ Proof.
}
{ admit. (* sim_local_body for the call init *) }
{ s. rewrite fill_app. ss. }
{ s. rewrite fill_app. f_equal. admit. (* call ctx *) }
{ s. admit. (* from WSAT0, x1 *) }
{ s. rewrite fill_app. eauto. }
{ s. admit. (* from wsat_assoc *) }
Admitted.
End local.
......
......@@ -112,9 +112,11 @@ Proof.
destruct SS2 as [|[Lt Eq]].
- left. eapply tc_rtc_l; eauto.
- clear -SS' Eq Lt. inversion Eq as [Eq1]. clear Eq. subst. rewrite Eq1.
clear vs2 Eq1. destruct SS' as [SS'|[? SS']].
+ left. by apply fill_tstep_tc.
+ simplify_eq. right. split; [|done]. lia. }
admit.
(* clear vs2 Eq1. destruct SS' as [SS'|[? SS']]. *)
(* + left. by apply fill_tstep_tc. *)
(* + simplify_eq. right. split; [|done]. lia. *)
}
(* Kt[et] makes a step *)
inversion_clear ST as [|Ks1 Kt1].
{ (* step into Kt[et] *)
......@@ -164,7 +166,7 @@ Proof.
destruct (CONT _ _ _ σs' σt' VREL') as [idx' CONT2]. clear CONT.
exists idx'. rewrite 2!fill_app.
pclearbot. right. by apply CIH. }
Qed.
Admitted.
(** MEM STEP -----------------------------------------------------------------*)
......
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