Commit 7f00eebc authored by Dan Frumin's avatar Dan Frumin

Add some experiments

parent e9796794
......@@ -48,4 +48,6 @@ theories/tests/typetest.v
theories/tests/ghosttp.v
theories/tests/tactics.v
theories/tests/tactics2.v
theories/tests/liftings.v
theories/tests/value.v
theories/examples/coqpl.v
From iris.proofmode Require Import tactics.
From iris_logrel Require Import logrel.
From iris.program_logic Require Import hoare.
From iris_logrel Require Import examples.counter.
Section liftings.
Context `{logrelG Σ}.
(* left-side hoare triples *)
Definition lhs_ht (P : iProp Σ) (e : expr) (Q : val iProp Σ) E Δ Γ :=
( K t τ, (P - ( v, Q v - {E;Δ;Γ} fill K (of_val v) log t : τ)
- {E;Δ;Γ} fill K e log t : τ))%I.
Lemma lift_ht (P : iProp Σ) (e : expr) (Q : val iProp Σ) E Δ Γ `{Closed e} :
({{ P }} e @ E {{ Q }}
lhs_ht P e Q E Δ Γ)%I.
Proof.
iIntros "#He" (K t τ).
iAlways. iIntros "HP"; iSpecialize ("He" with "HP").
iIntros "Hlog".
iApply bin_log_related_wp_l.
by iApply (wp_wand with "He").
Qed.
(* Definition taken from iris-atomic, strengthened a bit *)
Definition atomic_triple {A : Type}
(α: A iProp Σ) (* atomic pre-condition *)
(β: A val iProp Σ) (* atomic post-condition *)
(Ei Eo: coPset) (* inside/outside masks *)
(e: expr) : iProp Σ :=
( P Q, (P ={Eo, Ei}=> x:A,
α x
((α x ={Ei, Eo}= P)
( v, β x v ={Ei, Eo}= Q v))
) - {{ P }} e @ Eo {{ Q }})%I.
(* left-side logically atomic triples *)
(* Eo = E1, Ei = E2 *)
Definition atomic_logrel {A : Type}
(α: A iProp Σ) (* atomic pre-condition *)
(β: A val iProp Σ) (* atomic post-condition *)
(Ei Eo: coPset) (* inside/outside masks *)
(e: expr)
Δ Γ : iProp Σ :=
( K t τ R2 R1, (R2 (|={Eo,Ei}=> (x : A),
α x R1 x
((( x, α x R1 x) ={Ei, Eo}= True)
( y v, β y v R1 y R2 - {Ei,Eo;Δ;Γ} fill K (of_val v) log t : τ)))
) - {Eo;Δ;Γ} fill K e log t : τ)%I.
(* We can prove the atomic specification for the counter *)
Lemma counter_atomic x E1 E2 Δ Γ :
atomic_logrel
(fun (n : nat) => x ↦ᵢ #n)%I
(fun (n : nat) (v : val) => v = #() x ↦ᵢ #(S n))%I
E2 E1
((FG_increment $/ LitV (Loc x)) #())
Δ Γ.
Proof.
iIntros (K t τ R2 R1) "[HR2 #Hlog]".
iApply (bin_log_FG_increment_logatomic _ R1 with "HR2").
iAlways. iMod "Hlog" as (n) "(Hx & HR & Hlog)".
iModIntro. iExists _. iFrame.
iSplit.
- iDestruct "Hlog" as "[Hlog _]". done.
- iDestruct "Hlog" as "[_ Hlog]".
iIntros (m) "[Hx HR1] HR2".
iSpecialize ("Hlog" $! m #()). simpl.
iApply "Hlog". by iFrame.
Qed.
Lemma lift_atomic_ht {A : Type} (α : A iProp Σ) β Ei Eo e Δ
`{Closed e}:
(( atomic_triple α β Ei Eo e) -
atomic_logrel α β Ei Eo e Δ )%I.
Proof.
rewrite /atomic_triple.
iIntros "#HT" (K t τ).
iIntros (R2 R1) "[HR2 #Hlog]".
iSpecialize ("HT" $! R2 (fun v => {Eo; Δ; } fill K v log t : τ) with "[Hlog]").
- iAlways. iIntros "HR2".
iMod "Hlog" as (x) "(Hx & HR1 & Hlog)".
iModIntro. iExists _. iFrame "Hx".
iSplit.
+ iDestruct "Hlog" as "[Hlog _]".
iIntros "Hα".
iMod ("Hlog" with "[Hα HR1]"); last done.
iExists _; by iFrame.
+ iDestruct "Hlog" as "[_ Hlog]".
iIntros (v) "Hβ".
iSpecialize ("Hlog" with "[Hβ HR1 HR2]"). iFrame.
rewrite bin_log_related_eq /bin_log_related_def.
admit. (* we cannot really prove this: for our intents we might have to perform some operations on the RHS before we can close the invariant *)
- iApply (lift_ht with "HT HR2"). eauto.
Abort.
End liftings.
From iris.proofmode Require Import tactics.
From iris_logrel Require Import logrel.
From iris.program_logic Require Import hoare.
Section rr.
Context `{logrelG Σ}.
Notation D := (prodC valC valC -n> iProp Σ).
Notation "P ∗-∗ Q" := ((P - Q) (Q - P))%I (at level 50).
(* Question: Why cannot I use the internal equality here?
Would like to have intead of or -
*)
Lemma interp_val_arrow E τ σ Δ (v v' : val) ρ :
spec_ctx ρ -
τ σ Δ (v, v')
-
( ( (w w' : val), τ Δ (w, w')
- {E;Δ;} v w log v' w' : σ))%I.
Proof.
iIntros "#Hspec".
iSplitL.
- iIntros "/= #Hvv !#".
iIntros (w w') "#Hw".
iApply (related_ret E).
iApply ("Hvv" $! (w, w') with "Hw").
- iIntros "#Hvv /= !#".
iIntros ([w w']) "#Hww /=".
iSpecialize ("Hvv" with "Hww").
rewrite bin_log_related_eq /bin_log_related_def.
iIntros (j K) "Hj /=".
iSpecialize ("Hvv" $! ρ with "Hspec []").
{ iAlways. by iApply interp_env_nil. }
rewrite /interp_expr /=.
iSpecialize ("Hvv" $! j K).
rewrite /env_subst !fmap_empty !subst_p_empty.
iApply (fupd_mask_mono E); first done.
by iMod ("Hvv" with "Hj").
Qed.
End rr.
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