Skip to content
Snippets Groups Projects
Commit 42e45f5a authored by Ralf Jung's avatar Ralf Jung
Browse files

proof of log_rel_adequacy (not quite closed yet)

parent 9838f340
No related branches found
No related tags found
No related merge requests found
...@@ -115,6 +115,13 @@ Proof. ...@@ -115,6 +115,13 @@ Proof.
- intros X Φ [x [Hv [a ]]]; eauto. - intros X Φ [x [Hv [a ]]]; eauto.
Qed. Qed.
Lemma isat_intro {M} (P : uPred M) : ( P) isat P.
Proof.
intros HP. exists ε. split; first by apply ucmra_unit_validN.
apply HP; first by apply ucmra_unit_validN.
uPred.unseal. done.
Qed.
Lemma isat_later_false {M}: isat (( False)%I: uPred M) False. Lemma isat_later_false {M}: isat (( False)%I: uPred M) False.
Proof. Proof.
unfold isat; uPred.unseal; intros [x [_ HF]]. unfold isat; uPred.unseal; intros [x [_ HF]].
......
...@@ -37,8 +37,8 @@ Section ctx_rel. ...@@ -37,8 +37,8 @@ Section ctx_rel.
<hole> will be the function argument. *) <hole> will be the function argument. *)
Definition gen_ctx_rel (e_t e_s : expr) := Definition gen_ctx_rel (e_t e_s : expr) :=
(C : ctx) (fname x : string) (p : prog), (C : ctx) (fname x : string) (p : prog),
map_Forall (λ _ K, gen_ectx_wf expr_head_wf K free_vars_ectx K = ) p
gen_ctx_wf expr_head_wf C gen_ctx_wf expr_head_wf C
map_Forall (const (gen_ectx_wf expr_head_wf)) p
free_vars (fill_ctx C e_t) free_vars (fill_ctx C e_s) {[x]} free_vars (fill_ctx C e_t) free_vars (fill_ctx C e_s) {[x]}
beh_rel (<[fname := (λ: x, fill_ctx C e_t)%E]> p) (<[fname := (λ: x, fill_ctx C e_s)%E]> p). beh_rel (<[fname := (λ: x, fill_ctx C e_t)%E]> p) (<[fname := (λ: x, fill_ctx C e_s)%E]> p).
......
...@@ -14,8 +14,8 @@ Section adequacy. ...@@ -14,8 +14,8 @@ Section adequacy.
) )
beh_rel p_t p_s. beh_rel p_t p_s.
Proof. Proof.
intros Hsat. eapply (slsls_adequacy (sat:=isat)). intros Hrel. eapply (slsls_adequacy (sat:=isat)).
intros σ_t σ_s. eapply sat_bupd, sat_mono, Hsat. clear Hsat. intros σ_t σ_s. eapply sat_bupd, sat_mono, Hrel. clear Hrel.
iIntros "Hprog_rel". iIntros "Hprog_rel".
iMod sheap_init as (HsheapGS) "Hinit". iMod sheap_init as (HsheapGS) "Hinit".
iMod ("Hprog_rel" $! HsheapGS) as (HsheapInv loc_rel) "(Hinv & Hunit & Hobs & Hprog_rel)". iMod ("Hprog_rel" $! HsheapGS) as (HsheapInv loc_rel) "(Hinv & Hunit & Hobs & Hprog_rel)".
......
...@@ -71,18 +71,25 @@ Section open_rel. ...@@ -71,18 +71,25 @@ Section open_rel.
thread_own π -∗ thread_own π -∗
subst_map (fst <$> map) e_t {π} subst_map (snd <$> map) e_s {{ λ v_t v_s, thread_own π val_rel v_t v_s }}. subst_map (fst <$> map) e_t {π} subst_map (snd <$> map) e_s {{ λ v_t v_s, thread_own π val_rel v_t v_s }}.
Lemma gen_log_rel_closed_1 e_t e_s π :
free_vars e_t free_vars e_s =
gen_log_rel e_t e_s
thread_own π -∗ e_t {π} e_s {{ λ v_t v_s, thread_own π val_rel v_t v_s }}.
Proof.
iIntros (Hclosed) "#Hrel". iSpecialize ("Hrel" $! π ).
rewrite ->!fmap_empty, ->!subst_map_empty.
rewrite Hclosed. iApply "Hrel". by iApply subst_map_rel_empty.
Qed.
Lemma gen_log_rel_closed e_t e_s : Lemma gen_log_rel_closed e_t e_s :
free_vars e_t = free_vars e_t free_vars e_s =
free_vars e_s = gen_log_rel e_t e_s ⊣⊢
gen_log_rel e_t e_s ⊣⊢ ( π, thread_own π -∗ e_t {π} e_s {{ λ v_t v_s, thread_own π val_rel v_t v_s }}). ( π, thread_own π -∗ e_t {π} e_s {{ λ v_t v_s, thread_own π val_rel v_t v_s }}).
Proof. Proof.
intros Hclosed_t Hclosed_s. iSplit. intros Hclosed. iSplit.
- iIntros "#Hrel !#" (π). iSpecialize ("Hrel" $! π ). { iIntros "#Hrel !#" (π). iApply gen_log_rel_closed_1; done. }
rewrite ->!fmap_empty, ->!subst_map_empty. iIntros "#Hsim" (π xs) "!# Hxs".
rewrite Hclosed_t Hclosed_s [ _]left_id_L. rewrite !subst_map_closed //; set_solver.
iApply "Hrel". by iApply subst_map_rel_empty.
- iIntros "#Hsim" (π xs) "!# Hxs".
rewrite !subst_map_closed //.
Qed. Qed.
(** Substitute away a single variable in an [gen_log_rel]. (** Substitute away a single variable in an [gen_log_rel].
...@@ -166,7 +173,7 @@ Section log_rel_structural. ...@@ -166,7 +173,7 @@ Section log_rel_structural.
([list] e_t';e_s' head_t.2; head_s.2, log_rel e_t' e_s') -∗ ([list] e_t';e_s' head_t.2; head_s.2, log_rel e_t' e_s') -∗
log_rel e_t e_s). log_rel e_t e_s).
Theorem log_rel_structural_refl e : Theorem gen_log_rel_refl e :
log_rel_structural log_rel_structural
gen_expr_wf expr_head_wf e gen_expr_wf expr_head_wf e
log_rel e e. log_rel e e.
...@@ -179,7 +186,7 @@ Section log_rel_structural. ...@@ -179,7 +186,7 @@ Section log_rel_structural.
all: naive_solver. all: naive_solver.
Qed. Qed.
Theorem log_rel_ectx K e_t e_s : Theorem gen_log_rel_ectx K e_t e_s :
log_rel_structural log_rel_structural
gen_ectx_wf expr_head_wf K gen_ectx_wf expr_head_wf K
log_rel e_t e_s -∗ log_rel e_t e_s -∗
...@@ -193,11 +200,11 @@ Section log_rel_structural. ...@@ -193,11 +200,11 @@ Section log_rel_structural.
destruct Ki; simpl; iApply He => //=; iFrame "IH". destruct Ki; simpl; iApply He => //=; iFrame "IH".
all: move: Hiwf; rewrite /= ?Forall_cons ?Forall_nil => Hiwf. all: move: Hiwf; rewrite /= ?Forall_cons ?Forall_nil => Hiwf.
all: repeat iSplit; try done. all: repeat iSplit; try done.
all: iApply log_rel_structural_refl; [done|]. all: iApply gen_log_rel_refl; [done|].
all: naive_solver. all: naive_solver.
Qed. Qed.
Theorem log_rel_ctx C e_t e_s : Theorem gen_log_rel_ctx C e_t e_s :
log_rel_structural log_rel_structural
gen_ctx_wf expr_head_wf C gen_ctx_wf expr_head_wf C
log_rel e_t e_s -∗ log_rel e_t e_s -∗
...@@ -211,7 +218,7 @@ Section log_rel_structural. ...@@ -211,7 +218,7 @@ Section log_rel_structural.
destruct Ci; simpl; iApply He => //=; iFrame "IH". destruct Ci; simpl; iApply He => //=; iFrame "IH".
all: move: Hiwf; rewrite /= ?Forall_cons ?Forall_nil => Hiwf. all: move: Hiwf; rewrite /= ?Forall_cons ?Forall_nil => Hiwf.
all: repeat iSplit; try done. all: repeat iSplit; try done.
all: iApply log_rel_structural_refl; [done|]. all: iApply gen_log_rel_refl; [done|].
all: naive_solver. all: naive_solver.
Qed. Qed.
End log_rel_structural. End log_rel_structural.
From stdpp Require Export gmap. From stdpp Require Export gmap.
From simuliris.simplang Require Import lang. From simuliris.simplang Require Import lang notation.
(** * Parallel substitution for SimpLang *) (** * Parallel substitution for SimpLang *)
(** Definitions and proofs mostly yoinked from https://gitlab.mpi-sws.org/FP/stacked-borrows/-/blob/master/theories/lang/subst_map.v *) (** Definitions and proofs mostly yoinked from https://gitlab.mpi-sws.org/FP/stacked-borrows/-/blob/master/theories/lang/subst_map.v *)
...@@ -118,6 +118,10 @@ Fixpoint free_vars (e : expr) : gset string := ...@@ -118,6 +118,10 @@ Fixpoint free_vars (e : expr) : gset string :=
free_vars e0 free_vars e1 free_vars e2 free_vars e0 free_vars e1 free_vars e2
end. end.
(* Just fill with any value, it does not make a difference. *)
Definition free_vars_ectx (K : ectx) : gset string :=
free_vars (fill K #()).
Local Lemma binder_delete_eq x y (xs1 xs2 : gmap string val) : Local Lemma binder_delete_eq x y (xs1 xs2 : gmap string val) :
(if y is BNamed s then s x xs1 !! x = xs2 !! x else xs1 !! x = xs2 !! x) (if y is BNamed s then s x xs1 !! x = xs2 !! x else xs1 !! x = xs2 !! x)
binder_delete y xs1 !! x = binder_delete y xs2 !! x. binder_delete y xs1 !! x = binder_delete y xs2 !! x.
...@@ -171,3 +175,12 @@ Lemma free_vars_subst x v e : ...@@ -171,3 +175,12 @@ Lemma free_vars_subst x v e :
Proof. Proof.
induction e=>/=; repeat case_decide; set_solver. induction e=>/=; repeat case_decide; set_solver.
Qed. Qed.
Lemma free_vars_fill K e :
free_vars (fill K e) = free_vars_ectx K free_vars e.
Proof.
revert e. induction K as [|Ki K] using rev_ind; intros e; simpl.
{ simpl. rewrite /free_vars_ectx /= left_id_L. done. }
rewrite /free_vars_ectx !fill_app /=. destruct Ki; simpl.
all: rewrite !IHK; set_solver+.
Qed.
...@@ -6,7 +6,7 @@ From iris.base_logic.lib Require Import gset_bij. ...@@ -6,7 +6,7 @@ From iris.base_logic.lib Require Import gset_bij.
From simuliris.logic Require Import satisfiable. From simuliris.logic Require Import satisfiable.
From simuliris.simulation Require Import slsls global_sim. From simuliris.simulation Require Import slsls global_sim.
From simuliris.simplang Require Import proofmode tactics. From simuliris.simplang Require Import proofmode tactics.
From simuliris.simplang Require Import gen_adequacy behavior wf parallel_subst. From simuliris.simplang Require Import gen_adequacy behavior wf parallel_subst gen_refl.
From simuliris.simplang.simple_inv Require Import inv refl. From simuliris.simplang.simple_inv Require Import inv refl.
(** Instantiate our notion of contextual refinement. *) (** Instantiate our notion of contextual refinement. *)
...@@ -23,7 +23,7 @@ Global Instance subG_sbijΣ Σ : ...@@ -23,7 +23,7 @@ Global Instance subG_sbijΣ Σ :
subG simpleΣ Σ simpleGpreS Σ. subG simpleΣ Σ simpleGpreS Σ.
Proof. solve_inG. Qed. Proof. solve_inG. Qed.
Lemma prog_rel_adequacy `{!simpleGpreS Σ} p_t p_s : Lemma prog_rel_adequacy `{!simpleGpreS Σ} (p_t p_s : prog) :
isat ( `(simpleGS Σ), prog_rel p_t p_s) isat ( `(simpleGS Σ), prog_rel p_t p_s)
beh_rel p_t p_s. beh_rel p_t p_s.
Proof. Proof.
...@@ -45,5 +45,28 @@ Theorem log_rel_adequacy `{!simpleGpreS Σ} e_t e_s : ...@@ -45,5 +45,28 @@ Theorem log_rel_adequacy `{!simpleGpreS Σ} e_t e_s :
isat ( `(simpleGS Σ), log_rel e_t e_s) isat ( `(simpleGS Σ), log_rel e_t e_s)
ctx_rel e_t e_s. ctx_rel e_t e_s.
Proof. Proof.
(* TODO *) intros Hrel C fname x p Hpwf HCwf Hvars.
Abort. apply prog_rel_adequacy. eapply sat_mono, Hrel. clear Hrel.
iIntros "#Hrel" (?) "!# %f %K_s %π".
iSpecialize ("Hrel" $! _).
destruct (decide (f = fname)) as [->|Hne].
- (* FIXME: wtf, why does it need a type annotation here?!? *)
rewrite !(lookup_insert (M:=gmap _)).
iIntros ([= <-]). iExists _. iSplitR; first done.
(* TODO Factor this into a general lemma? *)
iIntros (v_t v_s) "#Hval /=".
iApply log_rel_closed_1.
{ simpl. set_solver. }
iApply log_rel_let.
{ iApply log_rel_val. done. }
iApply log_rel_ctx; done.
- rewrite !(lookup_insert_ne (M:=gmap _)) //.
iIntros (Hf). rename K_s into K. iExists K. iSplit; first done.
specialize (Hpwf _ _ Hf). destruct Hpwf as [HKwf HKclosed].
(* TODO Factor this into a lemma? *)
iIntros (v_t v_s) "#Hval /=".
iApply log_rel_closed_1.
{ rewrite !free_vars_fill HKclosed. set_solver+. }
iApply log_rel_ectx; first done.
iApply log_rel_val; done.
Qed.
...@@ -13,6 +13,10 @@ Definition expr_head_wf (e : expr_head) : Prop := ...@@ -13,6 +13,10 @@ Definition expr_head_wf (e : expr_head) : Prop :=
| _ => True | _ => True
end. end.
Notation expr_wf := (gen_expr_wf expr_head_wf).
Notation ectx_wf := (gen_ectx_wf expr_head_wf).
Notation ctx_wf := (gen_ctx_wf expr_head_wf).
Section refl. Section refl.
Context `{!simpleGS Σ}. Context `{!simpleGS Σ}.
...@@ -55,4 +59,34 @@ Section refl. ...@@ -55,4 +59,34 @@ Section refl.
iIntros (???????) "Hl Hv Hcont". iApply (sim_bij_store with "Hl Hv"). by iApply "Hcont". iIntros (???????) "Hl Hv Hcont". iApply (sim_bij_store with "Hl Hv"). by iApply "Hcont".
Qed. Qed.
Corollary log_rel_refl e :
expr_wf e
log_rel e e.
Proof.
intros ?. iApply gen_log_rel_refl; first by apply simple_log_rel_structural. done.
Qed.
Corollary log_rel_ctx C e_t e_s :
ctx_wf C
log_rel e_t e_s -∗ log_rel (fill_ctx C e_t) (fill_ctx C e_s).
Proof.
intros ?. iApply gen_log_rel_ctx; first by apply simple_log_rel_structural. done.
Qed.
Corollary log_rel_ectx K e_t e_s :
ectx_wf K
log_rel e_t e_s -∗ log_rel (fill K e_t) (fill K e_s).
Proof.
intros ?. iApply gen_log_rel_ectx; first by apply simple_log_rel_structural. done.
Qed.
Lemma log_rel_closed_1 e_t e_s π :
free_vars e_t free_vars e_s =
log_rel e_t e_s e_t {π} e_s {{ λ v_t v_s, val_rel v_t v_s }}.
Proof.
iIntros (?) "#Hrel".
iApply sim_mono; last iApply (gen_log_rel_closed_1 with "Hrel"); [|done..].
iIntros (v_t v_s) "[_ $]".
Qed.
End refl. End refl.
...@@ -891,6 +891,23 @@ Section fix_lang. ...@@ -891,6 +891,23 @@ Section fix_lang.
by iPureIntro. by iPureIntro.
Qed. Qed.
(** Simulations on evaluation contexts *)
Lemma sim_ectx_mono Φ Φ' π :
( v_t v_s, Φ v_t v_s -∗ Φ' v_t v_s) -∗
E_s E_t, sim_ectx π E_t E_s Φ -∗ sim_ectx π E_t E_s Φ'.
Proof.
iIntros "Hmon" (E_s E_t) "HE %v_t %v_s Hv".
iApply (sim_mono with "Hmon"). iApply "HE". done.
Qed.
Lemma sim_expr_ectx_mono Φ Φ' π :
( v_t v_s, Φ v_t v_s -∗ Φ' v_t v_s) -∗
E_s E_t, sim_expr_ectx π E_t E_s Φ -∗ sim_expr_ectx π E_t E_s Φ'.
Proof.
iIntros "Hmon" (E_s E_t) "HE %v_t %v_s Hv".
iApply (sim_expr_mono with "Hmon"). iApply "HE". done.
Qed.
(** ** source_red judgment *) (** ** source_red judgment *)
(** source_red allows to focus the reasoning on the source value (** source_red allows to focus the reasoning on the source value
(while being able to switch back and forth to the full simulation at any point) *) (while being able to switch back and forth to the full simulation at any point) *)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment