Commit e1bfea41 authored by Ralf Jung's avatar Ralf Jung

IntoResult

parent b51417bd
......@@ -71,6 +71,20 @@ Proof.
- intros Eq1 [? Eq2]. by rewrite Eq1 in Eq2.
Qed.
(** IntoResult is like IntoVal but works with our parameterized semantics. *)
Class IntoResult (e: expr) (r: result) := into_result : of_result r = e.
Global Instance val_into_result (v: value) : IntoResult v v.
Proof. done. Qed.
Global Instance place_into_result l tg ty : IntoResult (Place l tg ty) (PlaceR l tg ty).
Proof. done. Qed.
Global Instance result_into_result r : IntoResult (of_result r) r.
Proof. done. Qed.
Lemma into_result_terminal e r :
IntoResult e r terminal e.
Proof. intros <-. destruct r; eauto. Qed.
(** Thread steps *)
Inductive tstep (fns: fn_env) (eσ1 eσ2 : expr * state) : Prop :=
| ThreadStep ev efs
......
......@@ -35,26 +35,26 @@ Proof.
apply sim_simple_init_call=> c /= {css}.
(* Alloc *)
sim_apply sim_simple_alloc_local=> l t /=.
sim_apply sim_simple_let_place=>/=.
sim_apply sim_simple_let=>/=.
(* Write *)
rewrite (vrel_eq _ _ _ AREL).
sim_apply sim_simple_write_local; [done|solve_res|].
sim_apply sim_simple_write_local; [solve_sim..|].
intros arg ->. simpl.
sim_apply sim_simple_let_val=>/=.
apply sim_simple_place.
sim_apply sim_simple_let=>/=.
apply: sim_simple_result.
(* Retag. *)
sim_apply sim_simple_let_place=>/=.
sim_apply sim_simple_let=>/=.
destruct args as [|args args']; first by inversion AREL.
apply Forall2_cons_inv in AREL as [AREL ATAIL].
destruct args' as [|]; last by inversion ATAIL. clear ATAIL.
sim_apply sim_simple_retag_local; [solve_res|done|solve_res|].
sim_apply sim_simple_retag_local; [solve_sim..|].
move=>l_i tg_i hplt /= Hl_i.
(* Call *)
sim_apply sim_simple_let_val=>/=.
sim_apply (sim_simple_call 10 [] [] ε); [done|done|solve_res|].
intros rf frs frt _ _ _ _ FREL.
apply sim_simple_val. simpl.
sim_apply sim_simple_let_val=>/=.
sim_apply sim_simple_let=>/=.
sim_apply (sim_simple_call 10 [] [] ε); [solve_sim..|].
intros rf frs frt ??? ? _ _ FREL. simplify_eq/=.
apply: sim_simple_result. simpl.
sim_apply sim_simple_let=>/=.
(* Deref *)
Admitted.
......
......@@ -153,15 +153,16 @@ Proof.
simpl. apply HH.
Qed.
Lemma sim_body_result fs ft r n es et σs σt Φ :
( r Φ r n es σs et σt : Prop)
r {n,fs,ft} (of_result es, σs) (of_result et, σt) : Φ.
Lemma sim_body_result fs ft r n es rs et rt σs σt Φ :
IntoResult es rs IntoResult et rt
( r Φ r n rs σs rt σt : Prop)
r {n,fs,ft} (es, σs) (et, σt) : Φ.
Proof.
intros POST. pfold. split; last first.
intros <- <- POST. pfold. split; last first.
{ constructor 1. intros vt' ? STEPT'. exfalso.
apply result_tstep_stuck in STEPT'. by rewrite to_of_result in STEPT'. }
{ move => ? /= Eqvt'. symmetry in Eqvt'. simplify_eq.
exists es, σs, r. split; last split.
exists rs, σs, r. split; last split.
- constructor 1.
- eauto.
- rewrite to_of_result in Eqvt'. simplify_eq.
......
......@@ -30,7 +30,7 @@ Proof.
- eapply (sim_body_step_over_call _ _ init_res ε _ (ValR _) [] []); [done|..].
{ intros fid fn_src. specialize (FUNS fid fn_src). naive_solver. }
intros. simpl. exists 1%nat.
apply (sim_body_result _ _ _ _ (ValR vs) (ValR vt)).
apply: sim_body_result.
intros VALID.
have ?: rrel (init_res r') vs vt.
{ eapply rrel_mono; [done|apply cmra_included_r|exact VRET]. }
......
......@@ -175,7 +175,7 @@ Proof using Type*.
revert r. induction e using expr_ind; simpl; intros r.
- (* Value *)
move=>Hwf _ _ /=.
apply sim_simple_val.
apply: sim_simple_result.
do 3 (split; first done).
apply value_wf_soundness. done.
- (* Variable *)
......@@ -183,7 +183,7 @@ Proof using Type*.
rewrite !lookup_fmap. specialize (Hxswf x).
destruct (xs !! x); simplify_eq/=.
+ destruct p as [rs rt].
intros σs σt ??. eapply sim_body_result=>_.
intros σs σt ??. apply: sim_body_result.
do 3 (split; first done).
eapply (Hxswf (rs, rt)). done.
+ simpl. apply sim_simple_var.
......@@ -201,7 +201,7 @@ Proof using Type*.
eapply sim_simple_valid_post.
eapply sim_simple_call; [by auto..|].
intros rret vs vt vls vlt ? ??? Hrel''. simplify_eq.
apply sim_simple_val=>Hval'.
apply: sim_simple_result=>Hval'.
do 3 (split; first done). auto.
- (* InitCall: can't happen *) done.
- (* EndCall: can't happen *) done.
......
......@@ -191,7 +191,7 @@ Proof.
clear -Eq Eqrtm HNP. simplify_eq. do 4 (split; [done|]).
exists . rewrite Eqrtm lookup_op HNP left_id lookup_insert fmap_empty //. }
left.
apply (sim_body_result _ _ _ _ (PlaceR _ _ T) (PlaceR _ _ T)). intros.
apply: sim_body_result. intros.
apply POST; eauto.
Qed.
......@@ -323,7 +323,7 @@ Proof.
exists s. rewrite (_ : (fresh_block σt.(shp), Z.of_nat i) = l) //. }
rewrite HLt2 // HLs2 // Eqlst //. }
left.
apply (sim_body_result _ _ _ _ (PlaceR _ _ T) (PlaceR _ _ T)). intros.
apply: sim_body_result. intros.
apply POST; eauto. by rewrite /ts Eqnp.
Qed. *)
......@@ -479,7 +479,7 @@ Proof.
rewrite (EQt _ HLF).
by specialize (LINV _ _ Eqs) as (?&?&Eqa1&Eqas&?). }
left.
apply (sim_body_result _ _ _ _ (ValR vs) (ValR vt)). intros.
apply: sim_body_result. intros.
have VREL2: vrel (r (core (r_f r))) vs vt.
{ eapply vrel_mono; [done| |exact VREL']. apply cmra_included_r. }
apply POST; eauto.
......@@ -721,7 +721,7 @@ Proof.
* exfalso. move : Eq. rewrite lookup_insert_ne // lookup_empty /=.
by inversion 1. }
left.
eapply (sim_body_result _ _ _ _ (ValR [%S]) (ValR [%S])).
apply: sim_body_result.
intros. simpl. by apply POST.
Qed.
......@@ -1028,7 +1028,7 @@ Proof.
rewrite lookup_insert_ne //. by eexists.
}
left.
eapply (sim_body_result fs ft r' n (ValR [%S]) (ValR [%S])).
apply: sim_body_result.
intros. simpl. by apply POST.
Qed.
......@@ -1298,7 +1298,7 @@ Proof.
intros l InD SHR. by specialize (Eqhp _ InD SHR).
- intros ??. rewrite /=. by apply LINV. }
(* result *)
left. apply (sim_body_result _ _ _ _ (ValR vs) (ValR vt')).
left. apply: sim_body_result.
intros VALID'.
eapply POST; eauto. destruct SREL as (?&?&Eqs&?). by rewrite Eqs.
Qed.
......
......@@ -81,7 +81,7 @@ Proof.
exists (#[vi])%E, σs, r, n. split; last split; [|done|].
{ left. constructor 1. eapply (head_step_fill_tstep _ []).
by econstructor; econstructor. }
left. apply (sim_body_result _ _ _ _ (ValR _) (ValR _)). intros.
left. apply: sim_body_result. intros.
eapply POST; eauto.
Qed.
......@@ -102,7 +102,7 @@ Proof.
exists (#(v1 ++ v2))%E, σs, r, n. split; last split; [|done|].
{ left. constructor 1. eapply (head_step_fill_tstep _ []).
by econstructor; econstructor. }
left. apply (sim_body_result _ _ _ _ (ValR _) (ValR _)). intros.
left. apply: sim_body_result. intros.
eapply POST; eauto.
Qed.
......@@ -127,7 +127,7 @@ Proof.
{ left. constructor 1. eapply (head_step_fill_tstep _ []).
econstructor; econstructor; eauto.
eapply bin_op_eval_dom; [|eauto]. by rewrite (wsat_heap_dom _ _ _ WSAT). }
left. apply (sim_body_result _ _ _ _ (ValR _) (ValR _)). intros.
left. apply: sim_body_result. intros.
eapply POST; eauto.
Qed.
......@@ -160,12 +160,12 @@ Proof.
Qed.
(** Let *)
Lemma sim_body_let fs ft r n x es1 es2 et1 et2 σs σt Φ :
terminal es1 terminal et1
Lemma sim_body_let fs ft r n x es1 es2 et1 et2 vt1 vs1 σs σt Φ :
IntoResult es1 vs1 IntoResult et1 vt1
r {n,fs,ft} (subst' x es1 es2, σs) (subst' x et1 et2, σt) : Φ
r {n,fs,ft} (let: x := es1 in es2, σs) (let: x := et1 in et2, σt) : Φ.
Proof.
intros TS TT SIM. pfold.
intros TS%into_result_terminal TT%into_result_terminal SIM. pfold.
intros NT r_f WSAT. split; [|done|].
{ right. do 2 eexists. eapply (head_step_fill_tstep _ []).
econstructor 1. eapply LetBS; eauto. }
......@@ -177,16 +177,6 @@ Proof.
split; [done|]. by left.
Qed.
Lemma sim_body_let_val fs ft r n b (vs1 vt1: value) es2 et2 σs σt Φ :
r {n,fs,ft} (subst' b vs1 es2, σs) (subst' b vt1 et2, σt) : Φ
r {n,fs,ft} (let: b := vs1 in es2, σs) (let: b := vt1 in et2, σt) : Φ.
Proof. apply sim_body_let; eauto. Qed.
Lemma sim_body_let_place fs ft r n x ls lt ts tt tys tyt es2 et2 σs σt Φ :
r {n,fs,ft} (subst' x (Place ls ts tys) es2, σs) (subst' x (Place lt tt tyt) et2, σt) : Φ
r {n,fs,ft} (let: x := Place ls ts tys in es2, σs) ((let: x := Place lt tt tyt in et2), σt) : Φ.
Proof. apply sim_body_let; eauto. Qed.
(** Ref *)
Lemma sim_body_ref fs ft r n (pl: result) σs σt Φ :
( l t T, pl = PlaceR l t T
......@@ -214,7 +204,7 @@ Proof.
{ left. constructor 1. eapply (head_step_fill_tstep _ []).
by econstructor; econstructor. }
split; [done|]. left.
apply (sim_body_result _ _ _ _ (ValR _) (ValR _)).
apply: sim_body_result.
intros. by eapply POST.
Qed.
......@@ -243,6 +233,6 @@ Proof.
{ left. constructor 1. eapply (head_step_fill_tstep _ []).
by econstructor; econstructor. }
split; [done|].
left. apply (sim_body_result _ _ _ _ (PlaceR _ _ _) (PlaceR _ _ _)).
left. apply: sim_body_result.
intros. by eapply POST.
Qed.
......@@ -199,18 +199,12 @@ Proof.
clear. simpl. intros r n vs σs vt σt HH. exact: HH.
Qed.
Lemma sim_simple_val fs ft r n (vs vt: value) css cst Φ :
Lemma sim_simple_result fs ft r n (vs vt: result) es et css cst Φ :
IntoResult es vs IntoResult et vt
Φ r n vs css vt cst
r ⊨ˢ{n,fs,ft} (vs, css) (vt, cst) : Φ.
Proof.
intros HH σs σt <-<-. eapply (sim_body_result _ _ _ _ vs vt). done.
Qed.
Lemma sim_simple_place fs ft r n ls lt ts tt tys tyt css cst Φ :
Φ r n (PlaceR ls ts tys) css (PlaceR lt tt tyt) cst
r ⊨ˢ{n,fs,ft} (Place ls ts tys, css) (Place lt tt tyt, cst) : Φ.
r ⊨ˢ{n,fs,ft} (es, css) (et, cst) : Φ.
Proof.
intros HH σs σt <-<-. eapply (sim_body_result _ _ _ _ (PlaceR _ _ _) (PlaceR _ _ _)). done.
intros ?? HH σs σt <-<-. eapply sim_body_result; done.
Qed.
(** * Administrative *)
......@@ -226,7 +220,8 @@ Qed.
(* [Val <$> _] in the goal makes this not work with [apply], but
we'd need tactic support for anything better. *)
Lemma sim_simple_call n' rls rlt rv fs ft r r' n (fi: result) css cst Φ :
Lemma sim_simple_call n' rls rlt rv fs ft r r' n fe (fi: result) css cst Φ :
IntoResult fe fi
sim_local_funs_lookup fs ft
r r' rv
Forall2 (rrel rv) rls rlt
......@@ -236,9 +231,9 @@ Lemma sim_simple_call n' rls rlt rv fs ft r r' n (fi: result) css cst Φ :
vrel rret vs vt
r' rret ⊨ˢ{n',fs,ft} (Val vs, css) (Val vt, cst) : Φ)
r ⊨ˢ{n,fs,ft}
(Call fi (of_result <$> rls), css) (Call fi (of_result <$> rlt), cst) : Φ.
(Call fe (of_result <$> rls), css) (Call fe (of_result <$> rlt), cst) : Φ.
Proof.
intros Hfns Hres Hrel HH σs σt <-<-. rewrite Hres.
intros <- Hfns Hres Hrel HH σs σt <-<-. rewrite Hres.
apply: sim_body_step_over_call.
- done.
- done.
......@@ -344,21 +339,11 @@ Proof.
Admitted.
(** * Pure *)
Lemma sim_simple_let fs ft r n x (vs1 vt1: expr) es2 et2 css cst Φ :
terminal vs1 terminal vt1
r ⊨ˢ{n,fs,ft} (subst' x vs1 es2, css) (subst' x vt1 et2, cst) : Φ
r ⊨ˢ{n,fs,ft} (let: x := vs1 in es2, css) ((let: x := vt1 in et2), cst) : Φ.
Proof. intros ?? HH σs σt <-<-. apply sim_body_let; eauto. Qed.
Lemma sim_simple_let_val fs ft r n x (vs1 vt1: value) es2 et2 css cst Φ :
r ⊨ˢ{n,fs,ft} (subst' x vs1 es2, css) (subst' x vt1 et2, cst) : Φ
r ⊨ˢ{n,fs,ft} (let: x := vs1 in es2, css) ((let: x := vt1 in et2), cst) : Φ.
Proof. intros HH σs σt <-<-. apply sim_body_let; eauto. Qed.
Lemma sim_simple_let_place fs ft r n x ls lt ts tt tys tyt es2 et2 css cst Φ :
r ⊨ˢ{n,fs,ft} (subst' x (Place ls ts tys) es2, css) (subst' x (Place lt tt tyt) et2, cst) : Φ
r ⊨ˢ{n,fs,ft} (let: x := Place ls ts tys in es2, css) ((let: x := Place lt tt tyt in et2), cst) : Φ.
Proof. intros HH σs σt <-<-. apply sim_body_let; eauto. Qed.
Lemma sim_simple_let fs ft r n x (vs1 vt1: result) es1 et1 es2 et2 css cst Φ :
IntoResult es1 vs1 IntoResult et1 vt1
r ⊨ˢ{n,fs,ft} (subst' x es1 es2, css) (subst' x et1 et2, cst) : Φ
r ⊨ˢ{n,fs,ft} (let: x := es1 in es2, css) ((let: x := et1 in et2), cst) : Φ.
Proof. intros ?? HH σs σt <-<-. apply: sim_body_let. eauto. Qed.
Lemma sim_simple_ref fs ft r n (pl: result) css cst Φ :
( l t T, pl = PlaceR l t T
......@@ -376,13 +361,14 @@ Lemma sim_simple_var fs ft r n css cst var Φ :
r ⊨ˢ{n,fs,ft} (Var var, css) (Var var, cst) : Φ.
Proof. intros σs σt <-<-. apply sim_body_var; eauto. Qed.
Lemma sim_simple_proj fs ft r n (vr ir: result) css cst Φ :
Lemma sim_simple_proj fs ft r n (v i: expr) (vr ir: result) css cst Φ :
IntoResult v vr IntoResult i ir
( vi vv iv, vr = ValR vv ir = ValR [ScInt iv]
vv !! (Z.to_nat iv) = Some vi 0 iv
Φ r n (ValR [vi]) css (ValR [vi]) cst)
r ⊨ˢ{n,fs,ft} (Proj vr ir, css) (Proj vr ir, cst) : Φ.
Proof.
intros HH σs σt <-<-. apply sim_body_proj; eauto.
intros ?? HH σs σt <-<-. apply sim_body_proj; eauto.
Qed.
Lemma sim_simple_conc fs ft r n (r1 r2: result) css cst Φ :
......
......@@ -86,14 +86,14 @@ Tactic Notation "sim_apply" open_constr(lem) :=
reshape_expr es ltac:(fun Ks es =>
reshape_expr et ltac:(fun Kt et =>
sim_body_bind_core Ks Kt es et;
eapply lem
apply: lem
)
)
| |- _ ⊨ˢ{_,_,_} (?es, _) (?et, _) : _ =>
reshape_expr es ltac:(fun Ks es =>
reshape_expr et ltac:(fun Kt et =>
sim_simple_bind_core Ks Kt es et;
eapply lem
apply: lem
)
)
end.
......@@ -141,3 +141,6 @@ Ltac solve_res :=
simple eapply res_search_from_incl;
solve_res
end.
(** For example proofs. *)
Ltac solve_sim := solve [ fast_done | solve_res | done ].
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