Commit 51f95bd3 authored by Dan Frumin's avatar Dan Frumin

add some comments

parent d91a46ea
......@@ -40,6 +40,7 @@ Work in progress.
+ `stack/module_refinement.v`, `stack/refinement.v` - Treiber stack refines sequential stack
+ `stack/helping.v` - stack with helping refines sequential stack
+ `various.v` - some examples with higher-order functions with local state, in the style of "The effects of higher-order state and control on local relational reasoning" paper
+ `symbol.v` and `generative.v` - generative ADTs examples from the "State-Dependent Representational Independence" paper
- `logrel` contains modules related to the relational interpretation
+ `threadpool.v` - definitions for the ghost threadpool RA
+ `rules_threadpool.v` - symbolic execution in the threadpool
......
......@@ -426,12 +426,14 @@ Section refinement.
iIntros "Hmb".
rel_rec_l.
unlock revoke_offer. rel_rec_l.
iDestruct (offerInv_excl with "HN Ho") as %Hbaz.
iApply fupd_logrel'.
iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
iModIntro.
rewrite {2}bin_log_related_eq /bin_log_related_def.
iIntros (vvs ρ) "#Hs #HΓ".
iIntros (j K) "Hj". cbn[snd fst].
rewrite {2}/env_subst Closed_subst_p_id.
iDestruct (offerInv_excl with "HN Ho") as %Hbaz.
iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
iMod (offerReg_alloc o #n γ j K with "HNown") as "[HNown Hfrag]"; eauto.
iMod ("Hcl" with "[-Hfrag Hγ]") as "_".
{ iNext. iExists _,_,_; iFrame.
......
......@@ -118,6 +118,7 @@ Section refinement.
rel_vals; eauto.
Qed.
(* Also known as "callback with lock" *)
Definition i3 x x' b b' : iProp Σ :=
(( (n : nat), x ↦ᵢ #n x' ↦ₛ #n
b ↦ᵢ #true b' ↦ₛ #true)
......
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