From 88f728cee48e44006332b1ecc2c318300f64b168 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 22 Apr 2017 11:21:51 +0200
Subject: [PATCH] prove newlock (just for completeness' sake)
---
theories/lang/lib/lock.v | 10 ++++++++++
1 file changed, 10 insertions(+)
diff --git a/theories/lang/lib/lock.v b/theories/lang/lib/lock.v
index adcdcffb..0f7ca357 100644
--- a/theories/lang/lib/lock.v
+++ b/theories/lang/lib/lock.v
@@ -61,6 +61,16 @@ Section proof.
iDestruct "HR" as "[_ $]".
Qed.
+ Lemma newlock_spec (R : iProp Σ) :
+ {{{ ▷ R }}} newlock [] {{{ l γ, RET #l; ▷ lock_proto γ l R ∗ † l … 1 }}}.
+ Proof.
+ (* FIXME: Why is there no space between (l : loc)(γ : gname) as printed? *)
+ iIntros (Φ) "HR HΦ". wp_lam. wp_alloc l vl as "Hl" "H†". inv_vec vl=>v.
+ rewrite heap_mapsto_vec_singleton -wp_fupd. wp_let. wp_write.
+ iMod (lock_proto_create with "Hl HR") as (γ) "Hproto".
+ iApply "HΦ". by iFrame.
+ Qed.
+
(* At this point, it'd be really nice to have some sugar for symmetric
accessors. *)
Lemma try_acquire_spec E γ l R P :
--
GitLab