Commit e2bca994 authored by Dan Frumin's avatar Dan Frumin

Seal off the definitions `heapS_mapsto` and `bin_log_related`

parent f2cd21a3
......@@ -34,6 +34,7 @@ Section masked.
Γ !! x = Some τ
{E,E;Γ} Var x log Var x : τ.
Proof.
rewrite bin_log_related_eq.
iIntros (? Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj".
iDestruct (interp_env_Some_l with "HΓ") as ([v v']) "[Hvv' ?]"; first done.
iDestruct "Hvv'" as %Hvv'.
......@@ -47,6 +48,7 @@ Section masked.
Lemma bin_log_related_unit Γ : {E,E;Γ} Unit log Unit : TUnit.
Proof.
rewrite bin_log_related_eq.
iIntros (Δ vvs ρ) "#Hs HΓ"; iIntros (j K) "Hj /=".
value_case.
iExists UnitV; eauto.
......@@ -54,6 +56,7 @@ Section masked.
Lemma bin_log_related_nat Γ n : {E,E;Γ} #n n log #n n : TNat.
Proof.
rewrite bin_log_related_eq.
iIntros (Δ vvs ρ) "#Hs HΓ"; iIntros (j K) "Hj /=".
value_case.
iExists (#nv _); eauto.
......@@ -61,6 +64,7 @@ Section masked.
Lemma bin_log_related_bool Γ b : {E,E;Γ} # b log # b : TBool.
Proof.
rewrite bin_log_related_eq.
iIntros (Δ vvs ρ) "#Hs HΓ"; iIntros (j K) "Hj /=".
value_case.
iExists (#v _); eauto.
......@@ -71,6 +75,7 @@ Section masked.
{E,E;Γ} e2 log e2' : τ2 -
{E,E;Γ} Pair e1 e2 log Pair e1' e2' : TProd τ1 τ2.
Proof.
rewrite bin_log_related_eq.
iIntros "IH1 IH2". iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
cbn.
smart_bind j (env_subst _ e1) (env_subst _ e1') "IH1" v1 w1 "IH1".
......@@ -86,6 +91,7 @@ Section masked.
{E,E;Γ} e log e' : TProd τ1 τ2 -
{E,E;Γ} Fst e log Fst e' : τ1.
Proof.
rewrite bin_log_related_eq.
iIntros (?) "IH".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
cbn.
......@@ -102,6 +108,7 @@ Section masked.
{E,E;Γ} e log e' : TProd τ1 τ2 -
{E,E;Γ} Snd e log Snd e' : τ2.
Proof.
rewrite bin_log_related_eq.
iIntros (?) "IH".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
cbn.
......@@ -118,6 +125,7 @@ Section masked.
{E,E;Γ} e2 log e2' : τ1 -
{E,E;Γ} App e1 e2 log App e1' e2' : τ2.
Proof.
rewrite bin_log_related_eq.
iIntros "IH1 IH2".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
smart_bind j (env_subst _ e1) (env_subst _ e1') "IH1" f f' "#IH1".
......@@ -132,6 +140,7 @@ Section masked.
({E,E;<[x:=τ1]>(<[f:=TArrow τ1 τ2]>Γ)} e log e' : τ2) -
{E,E;Γ} Rec f x e log Rec f x e' : TArrow τ1 τ2.
Proof.
rewrite bin_log_related_eq.
iIntros (??) "#Ht".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=". cbn.
iDestruct (interp_env_dom with "HΓ") as %Hdom.
......@@ -205,6 +214,7 @@ Section masked.
{E,E;Γ} e log e' : τ1 -
{E,E;Γ} InjL e log InjL e' : (TSum τ1 τ2).
Proof.
rewrite bin_log_related_eq.
iIntros (?) "IH".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
smart_bind j (env_subst _ e) (env_subst _ e') "IH" v w "IH".
......@@ -218,6 +228,7 @@ Section masked.
{E,E;Γ} e log e' : τ2 -
{E,E;Γ} InjR e log InjR e' : TSum τ1 τ2.
Proof.
rewrite bin_log_related_eq.
iIntros (?) "IH".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
smart_bind j (env_subst _ e) (env_subst _ e') "IH" v w "IH".
......@@ -233,6 +244,7 @@ Section masked.
{E,E;Γ} e2 log e2' : TArrow τ2 τ3 -
{E,E;Γ} Case e0 e1 e2 log Case e0' e1' e2' : τ3.
Proof.
rewrite bin_log_related_eq.
iIntros (?) "IH1 IH2 IH3".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
smart_bind j (env_subst _ e0) (env_subst _ e0') "IH1" v v' "IH1".
......@@ -269,6 +281,7 @@ Section masked.
{E,E;Γ} e2 log e2' : τ -
{E,E;Γ} If e0 e1 e2 log If e0' e1' e2' : τ.
Proof.
rewrite bin_log_related_eq.
iIntros (?) "IH1 IH2 IH3".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
smart_bind j (env_subst _ e0) (env_subst _ e0') "IH1" v v' "IH1".
......@@ -287,6 +300,7 @@ Section masked.
{E,E;Γ} e2 log e2' : TNat -
{E,E;Γ} BinOp op e1 e2 log BinOp op e1' e2' : binop_res_type op.
Proof.
rewrite bin_log_related_eq.
iIntros (?) "IH1 IH2".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
smart_bind j (env_subst _ e1) (env_subst _ e1') "IH1" v v' "IH1".
......@@ -308,6 +322,7 @@ Section masked.
({E,E;(Autosubst_Classes.subst (ren (+1)) <$> Γ)} e log e' : τ) -
{E,E;Γ} TLam e log TLam e' : TForall τ.
Proof.
rewrite bin_log_related_eq.
iIntros (???) "#IH".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
iDestruct (interp_env_dom with "HΓ") as %Hdom.
......@@ -331,6 +346,7 @@ Section masked.
{E,E;Γ} e log e' : TForall τ -
{E,E;Γ} TApp e log TApp e' : τ.[τ'/].
Proof.
rewrite bin_log_related_eq.
iIntros "IH".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
smart_bind j (env_subst _ e) (env_subst _ e') "IH" v v' "#IH".
......@@ -347,6 +363,7 @@ Section masked.
{E,E;Γ} e log e' : τ.[(TRec τ)/] -
{E,E;Γ} Fold e log Fold e' : TRec τ.
Proof.
rewrite bin_log_related_eq.
iIntros "IH".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
smart_bind j (env_subst _ e) (env_subst _ e') "IH" v v' "#IH".
......@@ -361,6 +378,7 @@ Section masked.
{E,E;Γ} e log e' : TRec τ -
{E,E;Γ} Unfold e log Unfold e' : τ.[(TRec τ)/].
Proof.
rewrite bin_log_related_eq.
iIntros (?) "IH".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
smart_bind j (env_subst _ e) (env_subst _ e') "IH" v v' "#IH".
......@@ -377,6 +395,7 @@ Section masked.
{E,E;Γ} e log e' : τ.[τ'/] -
{E,E;Γ} Pack e log Pack e' : TExists τ.
Proof.
rewrite bin_log_related_eq.
iIntros "IH".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
smart_bind j (env_subst _ e) (env_subst _ e') "IH" v v' "#IH".
......@@ -393,6 +412,7 @@ Section masked.
{E,E;(Autosubst_Classes.subst (ren (+1)) <$> Γ)} e2 log e2' : TArrow τ (Autosubst_Classes.subst (ren (+1)) τ2) -
{E,E;Γ} Unpack e1 e2 log Unpack e1' e2' : τ2.
Proof.
rewrite bin_log_related_eq.
iIntros "IH1 IH2".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
smart_bind j (env_subst _ e1) (env_subst _ e1') "IH1" v v' "IH1".
......@@ -422,6 +442,7 @@ Section masked.
{E,E;Γ} e log e' : TUnit -
{E,E;Γ} Fork e log Fork e' : TUnit.
Proof.
rewrite bin_log_related_eq.
iIntros (?) "IH".
iIntros (Δ vvs ρ) "#Hs HΓ"; iIntros (j K) "Hj /=".
tp_fork j as i "Hi". fold subst_p. iModIntro.
......@@ -439,6 +460,7 @@ Section masked.
{E,E;Γ} e log e' : τ -
{E,E;Γ} Alloc e log Alloc e' : Tref τ.
Proof.
rewrite bin_log_related_eq.
iIntros (?) "IH".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
smart_bind j (env_subst _ e) (env_subst _ e') "IH" v v' "IH".
......@@ -460,6 +482,7 @@ Section masked.
{E,E;Γ} e log e' : (Tref τ) -
{E,E;Γ} Load e log Load e' : τ.
Proof.
rewrite bin_log_related_eq.
iIntros (??) "IH".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
smart_bind j (env_subst _ e) (env_subst _ e') "IH" v v' "IH".
......@@ -482,6 +505,7 @@ Section masked.
{E,E;Γ} e2 log e2' : τ -
{E,E;Γ} Store e1 e2 log Store e1' e2' : TUnit.
Proof.
rewrite bin_log_related_eq.
iIntros (??) "IH1 IH2".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
smart_bind j (env_subst _ e1) (env_subst _ e1') "IH1" v v' "IH1".
......@@ -507,6 +531,7 @@ Section masked.
{E,E;Γ} e3 log e3' : τ -
{E,E;Γ} CAS e1 e2 e3 log CAS e1' e2' e3' : TBool.
Proof.
rewrite bin_log_related_eq.
iIntros (??) "IH1 IH2 IH3".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
smart_bind j (env_subst _ e1) (env_subst _ e1') "IH1" v v' "IH1".
......@@ -538,8 +563,6 @@ Section masked.
iExists (#v false); repeat iModIntro; eauto.
Qed.
Opaque bin_log_related.
Theorem binary_fundamental_masked Γ e τ :
specN E
logN E
......
......@@ -35,6 +35,7 @@ Section hax.
{E,E;Γ} (Rec f x e) log (Rec f' x' e') : TArrow τ τ'.
Proof.
iIntros "#H".
rewrite bin_log_related_eq.
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj".
cbn-[subst_p].
iModIntro.
......
......@@ -375,11 +375,15 @@ Section bin_log_def.
Context `{heapIG Σ, cfgSG Σ}.
Notation D := (prodC valC valC -n> iProp Σ).
Definition bin_log_related (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)) ρ,
spec_ctx ρ -
interp_env Γ Δ vvs
- interp_expr E1 E2 (interp τ) Δ
(env_subst (fst <$> vvs) e, env_subst (snd <$> vvs) e'))%I.
Definition bin_log_related_aux : seal bin_log_related_def. Proof. by eexists. Qed.
Definition bin_log_related := unseal bin_log_related_aux.
Definition bin_log_related_eq : bin_log_related = bin_log_related_def :=
seal_eq bin_log_related_aux.
End bin_log_def.
Notation "'{' E1 ',' E2 ';' Γ '}' ⊨ e '≤log≤' e' : τ" :=
......
......@@ -19,6 +19,7 @@ Section properties.
((|={E1,E2}=> ({E2,E2;Γ} e log e' : τ))
- {E1,E2;Γ} e log e' : τ)%I.
Proof.
rewrite bin_log_related_eq.
iIntros "H".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
iMod "H".
......@@ -38,6 +39,7 @@ Section properties.
to_val e' = Some v'
( Δ, |={E}=> interp τ Δ (v, v')) {E,E;Γ} e log e' : τ.
Proof.
rewrite bin_log_related_eq.
iIntros (Hv Hv') "IH".
iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
replace e with (of_val v); auto using of_to_val.
......@@ -58,6 +60,7 @@ Section properties.
({E,E;Γ} fill K' e' log t : τ)
{E,E;Γ} fill K' e log t : τ.
Proof.
rewrite bin_log_related_eq.
assert (to_val e = None) as Hval.
{ destruct (Hsafe ) as [e2 [σ2 [efs Hs]]].
by eapply val_stuck. }
......@@ -89,6 +92,7 @@ Section properties.
{E1,E2;Γ} fill K' e' log t : τ
{E1,E2;Γ} fill K' e log t : τ.
Proof.
rewrite bin_log_related_eq.
assert (to_val e = None) as Hval.
{ destruct (Hsafe ) as [e2 [σ2 [efs Hs]]].
by eapply val_stuck. }
......@@ -295,6 +299,7 @@ Section properties.
{E,E;Γ} fill K (of_val v) log e2 : τ }})%I -
{E,E;Γ} fill K e1 log e2 : τ.
Proof.
rewrite bin_log_related_eq.
iIntros "He".
iIntros (Δ vvs ρ) "#Hs #HΓ". iIntros (j K') "Hj /=".
rewrite /env_subst fill_subst /=.
......@@ -327,6 +332,7 @@ Section properties.
{E2,E1;Γ} fill K (of_val v) log e2 : τ }})%I -
{E1,E1;Γ} fill K e1 log e2 : τ.
Proof.
rewrite bin_log_related_eq.
iIntros "Hlog".
iIntros (Δ vvs ρ) "#Hs #HΓ". iIntros (j K') "Hj /=". iModIntro.
rewrite /env_subst fill_subst /=.
......@@ -540,6 +546,7 @@ Section properties.
{E1,E2;Γ} t log fill K' e' : τ
{E1,E2;Γ} t log fill K' e : τ.
Proof.
rewrite bin_log_related_eq.
iIntros (Hstep) "Hlog".
iIntros (Δ vvs ρ) "#Hs #HΓ".
iIntros (j K) "Hj /=".
......@@ -691,6 +698,7 @@ Section properties.
( v, Φ v - {E1,E2;Γ} e1 log fill K' (of_val v) : τ) -
{E1,E2;Γ} e1 log fill K' e2 : τ.
Proof.
rewrite bin_log_related_eq.
iIntros "He Hlog".
iIntros (Δ vvs ρ) "#Hs #HΓ". iIntros (j K) "Hj /=".
rewrite /env_subst fill_subst /= -fill_app.
......
......@@ -26,17 +26,17 @@ Section definitionsS.
Definition heapS_mapsto_def (l : loc) (q : Qp) (v: val) : iProp Σ :=
own cfg_name ( (, {[ l := (q, to_agree v) ]})).
Definition heapS_mapsto_aux : { x | x = @heapS_mapsto_def }. by eexists. Qed.
Definition heapS_mapsto := proj1_sig heapS_mapsto_aux.
Definition heapS_mapsto_aux : seal heapS_mapsto_def. by eexists. Qed.
Definition heapS_mapsto := unseal heapS_mapsto_aux.
Definition heapS_mapsto_eq :
@heapS_mapsto = @heapS_mapsto_def := proj2_sig heapS_mapsto_aux.
@heapS_mapsto = @heapS_mapsto_def := seal_eq heapS_mapsto_aux.
Definition tpool_mapsto_def (j : nat) (e: expr) : iProp Σ :=
own cfg_name ( ({[ j := Excl e ]}, )).
Definition tpool_mapsto_aux : { x | x = @tpool_mapsto_def }. by eexists. Qed.
Definition tpool_mapsto := proj1_sig tpool_mapsto_aux.
Definition tpool_mapsto_aux : seal tpool_mapsto_def. by eexists. Qed.
Definition tpool_mapsto := unseal tpool_mapsto_aux.
Definition tpool_mapsto_eq :
@tpool_mapsto = @tpool_mapsto_def := proj2_sig tpool_mapsto_aux.
@tpool_mapsto = @tpool_mapsto_def := seal_eq tpool_mapsto_aux.
Definition spec_inv (ρ : cfg lang) : iProp Σ :=
( tp σ, own cfg_name ( (to_tpool tp, to_gen_heap σ))
......
......@@ -31,6 +31,7 @@ Proof.
iApply wp_fupd. iApply wp_wand_r.
iSplitL.
- iPoseProof (Hlog _ _) as "Hrel".
rewrite bin_log_related_eq /bin_log_related_def.
iSpecialize ("Hrel" $! [] with "[$Hcfg] []").
{ iAlways. iApply logrel_binary.interp_env_nil. }
rewrite /env_subst !fmap_empty !subst_p_empty.
......
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