Commit 1e50fc87 by Dan Frumin

### Some comments

parent b3fce334
 ... @@ -70,6 +70,13 @@ Section a_wp. ... @@ -70,6 +70,13 @@ Section a_wp. Definition flock_resources (γ : flock_name) (I : gmap prop_id (iProp Σ * frac)) := Definition flock_resources (γ : flock_name) (I : gmap prop_id (iProp Σ * frac)) := ([∗ map] i ↦ p ∈ I, flock_res γ i p.1 p.2)%I. ([∗ map] i ↦ p ∈ I, flock_res γ i p.1 p.2)%I. (** DF: The outer `WP` here is needed to be able to preform some reductions inside a heap_lang context. Without this, the `a_wp_awp` rule is not provable. My intuitive explanation: we want to preform some reductions to `e` until it is actually a value that is a monadic computation. In some sense it is a form of CPSing on a logical level. But I still cannot precisely state why is it needed. *) Definition awp (e : expr) Definition awp (e : expr) (R : iProp Σ) (Φ : val → iProp Σ) : iProp Σ := (R : iProp Σ) (Φ : val → iProp Σ) : iProp Σ := tc_opaque (WP e {{ ev, tc_opaque (WP e {{ ev, ... ...
 ... @@ -24,6 +24,12 @@ Definition a_free_check : val := ... @@ -24,6 +24,12 @@ Definition a_free_check : val := "go" "env" "l" (#1 + "i") "n" "go" "env" "l" (#1 + "i") "n" else #(). else #(). (* DF: following the discussion with Robbert, it seems that we cannot prove this function right now, because our ghost state cannot account that we hold permission for the *whole* array. See the RustBelt paper for the trick to make it work. *) Definition a_free : val := λ: "x", Definition a_free : val := λ: "x", "v" ←ᶜ "x";;ᶜ "v" ←ᶜ "x";;ᶜ a_atomic_env (λ: "env", a_atomic_env (λ: "env", ... ...
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