Commit 67d0a0ab authored by Dan Frumin's avatar Dan Frumin

Introduce a single typeclass for logical state for logical relations

parent c61b7c2a
From iris.program_logic Require Export weakestpre adequacy.
From iris_logrel.F_mu_ref_conc Require Export rules.
From iris.algebra Require Import auth.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Class heapPreG Σ := HeapPreG {
heap_preG_iris :> invPreG Σ;
heap_preG_heap :> gen_heapPreG loc val Σ
}.
Definition heapΣ : gFunctors := #[invΣ; gen_heapΣ loc val].
Instance subG_heapPreG {Σ} : subG heapΣ Σ heapPreG Σ.
Proof. solve_inG. Qed.
Definition heap_adequacy Σ `{heapPreG Σ} e σ φ :
( `{heapG Σ}, True WP e {{ v, ⌜φ v }})
adequate e σ φ.
Proof.
intros Hwp; eapply (wp_adequacy _ _); iIntros (?) "".
iMod (own_alloc ( to_gen_heap σ)) as (γ) "Hh".
{ apply: auth_auth_valid. exact: to_gen_heap_valid. }
iModIntro. iExists (λ σ, own γ ( to_gen_heap σ)); iFrame.
set (Hheap := GenHeapG loc val Σ _ _ _ γ).
iApply (Hwp (HeapG _ _ _)).
Qed.
...@@ -228,7 +228,7 @@ Ltac fold_interp := ...@@ -228,7 +228,7 @@ Ltac fold_interp :=
end. end.
Section bin_log_related_under_typed_ctx. Section bin_log_related_under_typed_ctx.
Context `{heapIG Σ, cfgSG Σ}. Context `{logrelG Σ}.
Ltac fundamental := Ltac fundamental :=
try (solve_ndisj); try (solve_ndisj);
......
...@@ -29,7 +29,7 @@ Definition FG_counter : expr := ...@@ -29,7 +29,7 @@ Definition FG_counter : expr :=
(FG_increment "x", counter_read "x"). (FG_increment "x", counter_read "x").
Section CG_Counter. Section CG_Counter.
Context `{heapIG Σ, cfgSG Σ}. Context `{logrelG Σ}.
(* Coarse-grained increment *) (* Coarse-grained increment *)
Lemma CG_increment_type Γ : Lemma CG_increment_type Γ :
...@@ -314,12 +314,6 @@ Theorem counter_ctx_refinement : ...@@ -314,12 +314,6 @@ Theorem counter_ctx_refinement :
FG_counter ctx CG_counter : FG_counter ctx CG_counter :
TProd (TArrow TUnit TUnit) (TArrow TUnit TNat). TProd (TArrow TUnit TUnit) (TArrow TUnit TNat).
Proof. Proof.
set (Σ := #[invΣ ; gen_heapΣ loc val ; authΣ cfgUR ]). eapply (logrel_ctxequiv logrelΣ); [solve_closed.. | intros ].
set (HG := HeapPreIG Σ _ _). apply FG_CG_counter_refinement.
eapply (logrel_ctxequiv Σ _).
(* TODO: how to get rid of this bullshit with closed conditions? *)
rewrite /FG_counter /CG_counter; try solve_closed.
rewrite /FG_counter /CG_counter; try solve_closed.
Transparent newlock. unfold newlock. solve_closed.
intros. apply FG_CG_counter_refinement.
Qed. Qed.
...@@ -17,7 +17,7 @@ Definition earlyChoice : val := λ: "x", ...@@ -17,7 +17,7 @@ Definition earlyChoice : val := λ: "x",
let: "r" := rand #() in "x" <- #n 0;; "r". let: "r" := rand #() in "x" <- #n 0;; "r".
Section Refinement. Section Refinement.
Context `{heapIG Σ, cfgSG Σ}. Context `{logrelG Σ}.
Definition choiceN : namespace := nroot .@ "choice". Definition choiceN : namespace := nroot .@ "choice".
......
...@@ -52,8 +52,7 @@ Qed. ...@@ -52,8 +52,7 @@ Qed.
Hint Resolve with_lock_type : typeable. Hint Resolve with_lock_type : typeable.
Section proof. Section proof.
Context `{cfgSG Σ}. Context `{logrelG Σ}.
Context `{heapIG Σ}.
Variable (E1 E2 : coPset). Variable (E1 E2 : coPset).
Lemma steps_newlock ρ j K Lemma steps_newlock ρ j K
......
...@@ -29,7 +29,7 @@ Qed. ...@@ -29,7 +29,7 @@ Qed.
Hint Resolve par_type : typeable. Hint Resolve par_type : typeable.
Section compatibility. Section compatibility.
Context `{heapIG Σ, cfgSG Σ}. Context `{logrelG Σ}.
Lemma bin_log_related_par Γ E e1 e2 e1' e2' τ1 τ2 : Lemma bin_log_related_par Γ E e1 e2 e1' e2' τ1 τ2 :
specN E specN E
......
...@@ -5,7 +5,7 @@ From iris.base_logic Require Export big_op. ...@@ -5,7 +5,7 @@ From iris.base_logic Require Export big_op.
From iris.program_logic Require Import ectx_lifting. From iris.program_logic Require Import ectx_lifting.
Section fundamental. Section fundamental.
Context `{heapIG Σ, cfgSG Σ}. Context `{logrelG Σ}.
Notation D := (prodC valC valC -n> iProp Σ). Notation D := (prodC valC valC -n> iProp Σ).
Implicit Types e : expr. Implicit Types e : expr.
Implicit Types Δ : listC D. Implicit Types Δ : listC D.
......
...@@ -25,7 +25,7 @@ Ltac inv_head_step := ...@@ -25,7 +25,7 @@ Ltac inv_head_step :=
end. end.
Section hax. Section hax.
Context `{heapIG Σ, cfgSG Σ}. Context `{logrelG Σ}.
Notation D := (prodC valC valC -n> iProp Σ). Notation D := (prodC valC valC -n> iProp Σ).
Implicit Types Δ : listC D. Implicit Types Δ : listC D.
......
...@@ -38,7 +38,7 @@ Definition logN : namespace := nroot .@ "logN". ...@@ -38,7 +38,7 @@ Definition logN : namespace := nroot .@ "logN".
(** interp : is a unary logical relation. *) (** interp : is a unary logical relation. *)
Section logrel. Section logrel.
Context `{heapIG Σ, cfgSG Σ}. Context `{logrelG Σ}.
Notation D := (prodC valC valC -n> iProp Σ). Notation D := (prodC valC valC -n> iProp Σ).
Implicit Types τi : D. Implicit Types τi : D.
Implicit Types Δ : listC D. Implicit Types Δ : listC D.
...@@ -372,7 +372,7 @@ Notation "⟦ τ ⟧ₑ" := (interp_expr ⊤ ⊤ ⟦ τ ⟧). ...@@ -372,7 +372,7 @@ Notation "⟦ τ ⟧ₑ" := (interp_expr ⊤ ⊤ ⟦ τ ⟧).
Notation "⟦ Γ ⟧*" := (interp_env Γ). Notation "⟦ Γ ⟧*" := (interp_env Γ).
Section bin_log_def. Section bin_log_def.
Context `{heapIG Σ, cfgSG Σ}. Context `{logrelG Σ}.
Notation D := (prodC valC valC -n> iProp Σ). Notation D := (prodC valC valC -n> iProp Σ).
Definition bin_log_related_def (E1 E2 : coPset) (Γ : stringmap type) (e e' : expr) (τ : type) : iProp Σ := ( Δ (vvs : stringmap (val * val)) ρ, Definition bin_log_related_def (E1 E2 : coPset) (Γ : stringmap type) (e e' : expr) (τ : type) : iProp Σ := ( Δ (vvs : stringmap (val * val)) ρ,
......
This diff is collapsed.
...@@ -5,7 +5,7 @@ From iris.program_logic Require Import ectx_lifting. ...@@ -5,7 +5,7 @@ From iris.program_logic Require Import ectx_lifting.
(** * Properties of the relational interpretation *) (** * Properties of the relational interpretation *)
Section properties. Section properties.
Context `{heapIG Σ, cfgSG Σ}. Context `{logrelG Σ}.
Notation D := (prodC valC valC -n> iProp Σ). Notation D := (prodC valC valC -n> iProp Σ).
Implicit Types e : expr. Implicit Types e : expr.
Implicit Types Δ : listC D. Implicit Types Δ : listC D.
......
...@@ -9,13 +9,13 @@ Import uPred. ...@@ -9,13 +9,13 @@ Import uPred.
(** The CMRA for the heap of the implementation. This is linked to the (** The CMRA for the heap of the implementation. This is linked to the
physical heap. *) physical heap. *)
Class heapIG Σ := HeapIG { Class heapG Σ := HeapG {
heapI_invG : invG Σ; heapG_invG : invG Σ;
heapI_gen_heapG :> gen_heapG loc val Σ; heapG_gen_heapG :> gen_heapG loc val Σ;
}. }.
Instance heapIG_irisG `{heapIG Σ} : irisG lang Σ := { Instance heapG_irisG `{heapG Σ} : irisG lang Σ := {
iris_invG := heapI_invG; iris_invG := heapG_invG;
state_interp := gen_heap_ctx state_interp := gen_heap_ctx
}. }.
Global Opaque iris_invG. Global Opaque iris_invG.
...@@ -25,7 +25,7 @@ Notation "l ↦ᵢ{ q } v" := (mapsto (L:=loc) (V:=val) l q v) ...@@ -25,7 +25,7 @@ Notation "l ↦ᵢ{ q } v" := (mapsto (L:=loc) (V:=val) l q v)
Notation "l ↦ᵢ v" := (mapsto (L:=loc) (V:=val) l 1 v) (at level 20) : uPred_scope. Notation "l ↦ᵢ v" := (mapsto (L:=loc) (V:=val) l 1 v) (at level 20) : uPred_scope.
Section lang_rules. Section lang_rules.
Context `{heapIG Σ}. Context `{heapG Σ}.
Implicit Types P Q : iProp Σ. Implicit Types P Q : iProp Σ.
Implicit Types Φ : val iProp Σ. Implicit Types Φ : val iProp Σ.
Implicit Types σ : state. Implicit Types σ : state.
......
...@@ -19,10 +19,14 @@ Fixpoint to_tpool_go (i : nat) (tp : list expr) : tpoolUR := ...@@ -19,10 +19,14 @@ Fixpoint to_tpool_go (i : nat) (tp : list expr) : tpoolUR :=
Definition to_tpool : list expr tpoolUR := to_tpool_go 0. Definition to_tpool : list expr tpoolUR := to_tpool_go 0.
(** The CMRA for the thread pool. *) (** The CMRA for the thread pool. *)
Class cfgSG Σ := CFGSG { cfg_inG :> inG Σ (authR cfgUR); cfg_name : gname }. Class logrelG Σ := LogrelG {
heap_inG :> heapG Σ;
cfg_inG :> inG Σ (authR cfgUR);
cfg_name : gname
}.
Section definitionsS. Section definitionsS.
Context `{cfgSG Σ, invG Σ}. Context `{logrelG Σ}.
Definition heapS_mapsto_def (l : loc) (q : Qp) (v: val) : iProp Σ := Definition heapS_mapsto_def (l : loc) (q : Qp) (v: val) : iProp Σ :=
own cfg_name ( (, {[ l := (q, to_agree v) ]})). own cfg_name ( (, {[ l := (q, to_agree v) ]})).
...@@ -51,7 +55,7 @@ Notation "l ↦ₛ v" := (heapS_mapsto l 1 v) (at level 20) : uPred_scope. ...@@ -51,7 +55,7 @@ Notation "l ↦ₛ v" := (heapS_mapsto l 1 v) (at level 20) : uPred_scope.
Notation "j ⤇ e" := (tpool_mapsto j e) (at level 20) : uPred_scope. Notation "j ⤇ e" := (tpool_mapsto j e) (at level 20) : uPred_scope.
Section conversions. Section conversions.
Context `{cfgSG Σ}. Context `{logrelG Σ}.
(** Conversion to tpools and back *) (** Conversion to tpools and back *)
Lemma to_tpool_valid es : to_tpool es. Lemma to_tpool_valid es : to_tpool es.
...@@ -112,7 +116,7 @@ Section conversions. ...@@ -112,7 +116,7 @@ Section conversions.
End conversions. End conversions.
Section cfg. Section cfg.
Context `{heapIG Σ, cfgSG Σ}. Context `{logrelG Σ}.
Implicit Types P Q : iProp Σ. Implicit Types P Q : iProp Σ.
Implicit Types Φ : val iProp Σ. Implicit Types Φ : val iProp Σ.
Implicit Types σ : state. Implicit Types σ : state.
......
From iris_logrel.F_mu_ref_conc Require Export context_refinement. From iris_logrel.F_mu_ref_conc Require Export context_refinement adequacy.
From iris.algebra Require Import auth frac agree. From iris.algebra Require Import auth frac agree.
From iris.base_logic Require Import big_op. From iris.base_logic Require Import big_op lib.auth.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris.program_logic Require Import adequacy.
Class heapPreIG Σ := HeapPreIG { Class logrelPreG Σ := LogrelPreG {
heap_preG_iris :> invPreG Σ; logrel_preG_heap :> heapPreG Σ;
heap_preG_heap :> gen_heapPreG loc val Σ logrel_preG_cfg :> inG Σ (authR cfgUR)
}. }.
Lemma logrel_adequate Σ `{heapPreIG Σ, inG Σ (authR cfgUR)} Definition logrelΣ : gFunctors := #[heapΣ; authΣ cfgUR].
Instance subG_heapPreG {Σ} : subG logrelΣ Σ logrelPreG Σ.
Proof. solve_inG. Qed.
Lemma logrel_adequate Σ `{logrelPreG Σ}
e e' τ σ : e e' τ σ :
( `{heapIG Σ, cfgSG Σ}, e log e' : τ) ( `{logrelG Σ}, e log e' : τ)
adequate e σ (λ v, thp' h v', rtc step ([e'], ) (of_val v' :: thp', h) adequate e σ (λ v, thp' h v', rtc step ([e'], ) (of_val v' :: thp', h)
(ObsType τ v = v')). (ObsType τ v = v')).
Proof. Proof.
intros Hlog. intros Hlog.
eapply (wp_adequacy Σ _); iIntros (Hinv). eapply (heap_adequacy Σ _); iIntros (Hinv).
iMod (own_alloc ( to_gen_heap σ)) as (γ) "Hh".
{ apply (auth_auth_valid _ (to_gen_heap_valid _ _ σ)). }
iMod (own_alloc ( (to_tpool [e'], ) iMod (own_alloc ( (to_tpool [e'], )
((to_tpool [e'] : tpoolUR, ) : cfgUR))) as (γc) "[Hcfg1 Hcfg2]". ((to_tpool [e'] : tpoolUR, ) : cfgUR))) as (γc) "[Hcfg1 Hcfg2]".
{ apply auth_valid_discrete_2. split=>//. split=>//. apply to_tpool_valid. } { apply auth_valid_discrete_2. split=>//. split=>//. apply to_tpool_valid. }
set (Hcfg := CFGSG _ _ γc). set (Hcfg := LogrelG _ _ _ γc).
iMod (inv_alloc specN _ (spec_inv ([e'], )) with "[Hcfg1]") as "#Hcfg". iMod (inv_alloc specN _ (spec_inv ([e'], )) with "[Hcfg1]") as "#Hcfg".
{ iNext. iExists [e'], . { iNext. iExists [e'], .
rewrite /to_gen_heap fin_maps.map_fmap_empty. auto. } rewrite /to_gen_heap fin_maps.map_fmap_empty. auto. }
set (HeapΣ := (HeapIG Σ Hinv (GenHeapG _ _ Σ _ _ _ γ))).
iExists (λ σ, own γ ( to_gen_heap σ)); iFrame.
iApply wp_fupd. iApply wp_wand_r. iApply wp_fupd. iApply wp_wand_r.
iSplitL. iSplitL.
- iPoseProof (Hlog _ _) as "Hrel". - iPoseProof (Hlog _) as "Hrel".
rewrite bin_log_related_eq /bin_log_related_def. rewrite bin_log_related_eq /bin_log_related_def.
iSpecialize ("Hrel" $! [] with "[$Hcfg] []"). iSpecialize ("Hrel" $! [] with "[$Hcfg] []").
{ iAlways. iApply logrel_binary.interp_env_nil. } { iApply logrel_binary.interp_env_nil. }
rewrite /env_subst !fmap_empty !subst_p_empty. rewrite /env_subst !fmap_empty !subst_p_empty.
iApply fupd_wp.
iApply ("Hrel" $! 0 []). simpl. iApply ("Hrel" $! 0 []). simpl.
rewrite tpool_mapsto_eq /tpool_mapsto_def. iFrame. rewrite tpool_mapsto_eq /tpool_mapsto_def. iFrame.
- iModIntro. iIntros (v1). - iIntros (v1).
iDestruct 1 as (v2) "[Hj #Hinterp]". iDestruct 1 as (v2) "[Hj #Hinterp]".
iInv specN as (tp σ') ">[Hown Hsteps]" "Hclose"; iDestruct "Hsteps" as %Hsteps'. iInv specN as (tp σ') ">[Hown Hsteps]" "Hclose"; iDestruct "Hsteps" as %Hsteps'.
rewrite tpool_mapsto_eq /tpool_mapsto_def /=. rewrite tpool_mapsto_eq /tpool_mapsto_def /=.
...@@ -52,8 +52,8 @@ Proof. ...@@ -52,8 +52,8 @@ Proof.
Qed. Qed.
Theorem logrel_typesafety Σ `{heapPreIG Σ, inG Σ (authR cfgUR)} e τ e' thp σ σ' : Theorem logrel_typesafety Σ `{logrelPreG Σ} e τ e' thp σ σ' :
( `{heapIG Σ, cfgSG Σ}, e log e : τ) ( `{logrelG Σ}, e log e : τ)
rtc step ([e], σ) (thp, σ') e' thp rtc step ([e], σ) (thp, σ') e' thp
is_Some (to_val e') reducible e' σ'. is_Some (to_val e') reducible e' σ'.
Proof. Proof.
...@@ -62,9 +62,9 @@ Proof. ...@@ -62,9 +62,9 @@ Proof.
eapply logrel_adequate; eauto. eapply logrel_adequate; eauto.
Qed. Qed.
Lemma logrel_simul Σ `{heapPreIG Σ, inG Σ (authR cfgUR)} Lemma logrel_simul Σ `{logrelPreG Σ}
e e' τ v thp hp : e e' τ v thp hp :
( `{heapIG Σ, cfgSG Σ}, e log e' : τ) ( `{logrelG Σ}, e log e' : τ)
rtc step ([e], ) (of_val v :: thp, hp) rtc step ([e], ) (of_val v :: thp, hp)
( thp' hp' v', rtc step ([e'], ) (of_val v' :: thp', hp') (ObsType τ v = v')). ( thp' hp' v', rtc step ([e'], ) (of_val v' :: thp', hp') (ObsType τ v = v')).
Proof. Proof.
...@@ -74,18 +74,17 @@ Proof. ...@@ -74,18 +74,17 @@ Proof.
eapply logrel_adequate; eauto. eapply logrel_adequate; eauto.
Qed. Qed.
Lemma logrel_ctxequiv Σ `{heapPreIG Σ, inG Σ (authR cfgUR)} Lemma logrel_ctxequiv Σ `{logrelPreG Σ} Γ e e' τ :
Γ e e' τ : Closed (dom _ Γ) e
(Closed (dom _ Γ) e) Closed (dom _ Γ) e'
(Closed (dom _ Γ) e') ( `{logrelG Σ}, Γ e log e' : τ)
( `{heapIG Σ, cfgSG Σ}, Γ e log e' : τ)
Γ e ctx e' : τ. Γ e ctx e' : τ.
Proof. Proof.
intros He He' Hlog K thp σ ? τ' ? ? Hstep. intros He He' Hlog K thp σ ? τ' ? ? Hstep.
cut ( thp' hp' v', rtc step ([fill_ctx K e'], ) (of_val v' :: thp', hp') (ObsType τ' v = v')). cut ( thp' hp' v', rtc step ([fill_ctx K e'], ) (of_val v' :: thp', hp') (ObsType τ' v = v')).
{ naive_solver. } { naive_solver. }
eapply (logrel_simul Σ _); last by apply Hstep. eapply (logrel_simul Σ _); last by apply Hstep.
intros ??. intros ?.
iApply (bin_log_related_under_typed_ctx _ _ _ _ ); eauto. iApply (bin_log_related_under_typed_ctx _ _ _ _ ); eauto.
iPoseProof (Hlog _ _) as "Hrel". auto. iPoseProof (Hlog _) as "Hrel". auto.
Qed. Qed.
This diff is collapsed.
...@@ -17,6 +17,7 @@ F_mu_ref_conc/logrel_binary.v ...@@ -17,6 +17,7 @@ F_mu_ref_conc/logrel_binary.v
F_mu_ref_conc/fundamental_binary.v F_mu_ref_conc/fundamental_binary.v
# F_mu_ref_conc/soundness_unary.v # F_mu_ref_conc/soundness_unary.v
F_mu_ref_conc/context_refinement.v F_mu_ref_conc/context_refinement.v
F_mu_ref_conc/adequacy.v
F_mu_ref_conc/soundness_binary.v F_mu_ref_conc/soundness_binary.v
F_mu_ref_conc/tactics.v F_mu_ref_conc/tactics.v
F_mu_ref_conc/rel_tactics.v F_mu_ref_conc/rel_tactics.v
......
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