Commit f33a4e73 authored by Dan Frumin's avatar Dan Frumin

Add ghost threadpool tests

parent 7aceb1b3
......@@ -44,5 +44,6 @@ theories/examples/symbol.v
theories/examples/generative.v
theories/examples/Y.v
theories/tests/typetest.v
theories/tests/ghosttp.v
theories/tests/tactics.v
theories/tests/tactics2.v
From iris_logrel Require Export logrel.
From iris.proofmode Require Import tactics.
Section contents.
Context `{logrelG Σ}.
Lemma ex Δ Γ :
{,;Δ;Γ} (λ: "x", "x" <- #1)
log
(λ: "x", Fork ("x" <- #1);; Fork ("x" <- #0)) : TArrow (Tref TNat) TUnit.
Proof.
iApply bin_log_related_arrow_val; eauto.
iAlways. iIntros (? ?) "Hx".
simpl. iDestruct "Hx" as ([x1 x2]) "[% #Hx]"; simplify_eq/=.
rel_let_l. rel_let_r.
rel_store_l_atomic.
iInv (logN.@(x1,x2)) as ([v1 v2]) "(Hx1 & Hx2 & Hvs)" "Hcl".
iModIntro. iExists _. iFrame. iNext. iIntros "Hx1".
rel_fork_r as i "Hi". rel_seq_r.
rel_fork_r as j "Hj".
apply bin_log_related_spec_ctx. iDestruct 1 as (?) "?".
tp_store i.
iMod ("Hcl" with "[-]") as "_".
{ iNext. iExists (_,_); iFrame. iExists _; eauto. }
iApply bin_log_related_unit.
Qed.
End contents.
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