...
 
Commits (41)
......@@ -27,10 +27,15 @@ variables:
## Build jobs
build-coq.8.11.1:
#build-coq.8.12.dev: # not compatible with iris-string-ident
# <<: *template
# variables:
# OPAM_PINS: "coq version 8.12.dev"
build-coq.8.11.2:
<<: *template
variables:
OPAM_PINS: "coq version 8.11.1"
OPAM_PINS: "coq version 8.11.2"
tags:
- fp-timing
......
All files in this development are distributed under the terms of the BSD
license, included below.
All files in this development are distributed under the terms of the 3-clause
BSD license (https://opensource.org/licenses/BSD-3-Clause), included below.
Copyright: Iris developers and contributors
......
# Permit local customization
-include Makefile.local
# Forward most targets to Coq makefile (with some trick to make this phony)
%: Makefile.coq phony
+@make -f Makefile.coq $@
......@@ -8,13 +11,13 @@ all: Makefile.coq
clean: Makefile.coq
+@make -f Makefile.coq clean
find theories tests \( -name "*.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
find theories tests exercises solutions \( -name "*.d" -o -name "*.vo" -o -name "*.vo[sk]" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
rm -f Makefile.coq .lia.cache
.PHONY: clean
# Create Coq Makefile.
Makefile.coq: _CoqProject Makefile
"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq
"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq $(EXTRA_COQFILES)
# Install build-dependencies
build-dep/opam: opam Makefile
......@@ -36,6 +39,7 @@ build-dep: build-dep/opam phony
Makefile: ;
_CoqProject: ;
opam: ;
Makefile.local: ;
# Phony wildcard targets
phony: ;
......
......@@ -26,5 +26,8 @@ hocap: $(filter theories/hocap/%,$(VOFILES))
logatom: $(filter theories/logatom/%,$(VOFILES))
.PHONY: logatom
array_based_queuing_lock: $(filter theories/array_based_queuing_lock/%,$(VOFILES))
.PHONY: array_based_queuing_lock
proph: $(filter theories/proph/%,$(VOFILES))
.PHONY: proph
......@@ -6,7 +6,7 @@ Some example verification demonstrating the use of Iris.
This version is known to compile with:
- Coq 8.11.1
- Coq 8.11.2
- A development version of [Iris](https://gitlab.mpi-sws.org/FP/iris-coq/)
- The coq86-devel branch of [Autosubst](https://github.com/uds-psl/autosubst)
......@@ -61,16 +61,21 @@ This repository contains the following case studies:
- Treiber Stack (by Zhen Zhang, and another version by Rodolphe Lepigre).
- Flat Combiner (by Zhen Zhang, also see
[this archived documentation](https://gitlab.mpi-sws.org/FP/iris-atomic/tree/master/docs)).
* [spanning-tree](theories/spanning_tree): Proof of a concurrent spanning tree
* [spanning_tree](theories/spanning_tree): Proof of a concurrent spanning tree
algorithm (by Amin Timany).
* [concurrent-stacks](theories/concurrent_stacks): Proof of an implementation of
* [concurrent_stacks](theories/concurrent_stacks): Proof of an implementation of
concurrent stacks with helping by Daniel Gratzer et. al., as described in the
[report](http://iris-project.org/pdfs/2017-case-study-concurrent-stacks-with-helping.pdf).
* [lecture-notes](theories/lecture_notes): Coq examples for the
* [lecture_notes](theories/lecture_notes): Coq examples for the
[Iris lecture notes](http://iris-project.org/tutorial-material.html).
* [hocap](theories/hocap): Formalizations of the concurrent bag and concurrent
runners libraries from the [HOCAP paper](https://dl.acm.org/citation.cfm?id=2450283)
(by Dan Frumin). See the associated [README](theories/hocap/README.md).
* [array_based_queuing_lock](/theories/array_based_queuing_lock): Proof of
safety of an implementation of the array-based queuing lock. This example is
also covered in the chapter ["Case study: The Array-Based Queueing
Lock"](https://iris-project.org/tutorial-pdfs/iris-lecture-notes.pdf#section.10)
in the Iris lecture notes.
## For Developers: How to update the Iris dependency
......
......@@ -20,6 +20,7 @@ theories/lecture_notes/coq_intro_example_2.v
theories/lecture_notes/lists.v
theories/lecture_notes/lists_guarded.v
theories/lecture_notes/lock.v
theories/lecture_notes/bag.v
theories/lecture_notes/lock_unary_spec.v
theories/lecture_notes/modular_incr.v
theories/lecture_notes/recursion_through_the_store.v
......@@ -108,3 +109,5 @@ theories/proph/lazy_coin_one_shot_typed.v
theories/proph/clairvoyant_coin_spec.v
theories/proph/clairvoyant_coin.v
theories/proph/clairvoyant_coin_typed.v
theories/array_based_queuing_lock/abql.v
......@@ -9,7 +9,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/FP/iris-examples.git"
synopsis: "A collection of case studies for Iris"
depends: [
"coq-iris" { (= "dev.2020-05-28.3.38f177d3") | (= "dev") }
"coq-iris" { (= "dev.2020-07-15.7.fa9d6a7c") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
"coq-iris-string-ident"
]
......
This diff is collapsed.
......@@ -2,7 +2,7 @@ From stdpp Require Import namespaces.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export proofmode notation.
(** General (HoCAP-style) spec for a concurrent bag ("per-elemt spec") *)
(** General (CAP-style) spec for a concurrent bag ("per-element spec") *)
Record concurrent_bag {Σ} `{!heapG Σ} := ConcurrentBag {
is_bag (P : val iProp Σ) (s : val) : iProp Σ;
bag_pers (P : val iProp Σ) (s : val) : Persistent (is_bag P s);
......@@ -20,7 +20,7 @@ Record concurrent_bag {Σ} `{!heapG Σ} := ConcurrentBag {
}.
Arguments concurrent_bag _ {_}.
(** General (CAP-style) spec for a concurrent stack *)
(** General (HoCAP-style) spec for a concurrent stack *)
Record concurrent_stack {Σ} `{!heapG Σ} := ConcurrentStack {
is_stack (N : namespace) (P : list val iProp Σ) (s : val) : iProp Σ;
......
(* This file contains Example 7.38 of the Iris Lecture Notes. We implement a
concurrent course grained bag based on the lock in `lock.v`.
*)
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import auth.
Import uPred.
From iris_examples.lecture_notes Require Import lock.
Definition newbag : val :=
λ: <>, let: "ℓ" := ref NONE in
let: "v" := newlock #() in ("ℓ", "v").
Definition insert : val :=
λ: "x" "e", let: "ℓ" := Fst "x" in
let: "lock" := Snd "x" in
acquire "lock" ;;
"ℓ" <- SOME ("e", !"ℓ") ;;
release "lock".
Definition remove : val :=
λ: "x", let: "ℓ" := Fst "x" in
let: "lock" := Snd "x" in
acquire "lock" ;;
let: "r" := !"ℓ" in
let: "res" := match: "r" with
NONE => NONE
| SOME "p" => "ℓ" <- Snd "p" ;; SOME (Fst "p")
end
in release "lock" ;; "res".
Section spec.
Context `{!heapG Σ, lockG Σ}.
Local Notation iProp := (iProp Σ).
Fixpoint isBag (Ψ : val iProp) (v : val) : iProp :=
match v with
| NONEV => True%I
| SOMEV (x, r) => (Ψ x isBag Ψ r)%I
| _ => False%I
end.
Definition is_bag (v : val) (Ψ : val iProp) :=
( ( : loc) (v : val) γ, v = (#, v)%V is_lock γ v ( u, u isBag Ψ u))%I.
Global Instance bag_persistent v Ψ: Persistent (is_bag v Ψ).
Proof. apply _. Qed.
Lemma newbag_triple_spec Ψ:
{{{ True }}} newbag #() {{{ b, RET b; is_bag b Ψ}}}.
Proof.
iIntros (ϕ) "_ Hcont".
wp_lam ; wp_alloc as "Hℓ"; wp_let.
wp_apply ((newlock_spec ( u, u isBag Ψ u))%I with "[Hℓ]").
{ iExists NONEV. auto. }
iIntros (v). iDestruct 1 as (γ) "IL".
wp_pures. iApply "Hcont".
iExists , v, γ. iFrame. done.
Qed.
Lemma bag_insert_triple_spec v Ψ e:
{{{ is_bag v Ψ Ψ e }}} insert v e {{{ RET #(); True }}}.
Proof.
iIntros (ϕ) "[Hb Hψ] Hcont".
iDestruct "Hb" as ( u γ) "[% #IL]"; subst.
wp_lam. wp_pures.
wp_apply (acquire_spec with "IL"); first done.
iIntros (v) "[P HLocked]".
iDestruct "P" as (b) "[Hp Hb]".
wp_load. wp_store.
iApply (release_spec with "[$IL $HLocked Hp Hψ Hb]"); first done.
{ iExists _. iFrame "Hp". iFrame. }
done.
Qed.
Lemma bag_remove_triple_spec v Ψ:
{{{ is_bag v Ψ }}} remove v {{{ u, RET u; u = NONEV x, u = SOMEV x Ψ x }}}.
Proof.
iIntros (ϕ) "Hb Hcont".
iDestruct "Hb" as ( u γ) "[% #IL]"; subst.
wp_lam. wp_pures.
wp_apply (acquire_spec with "IL"); first done.
iIntros (v) "[P HLocked]". iDestruct "P" as (b) "[Hp Hb]".
wp_load.
destruct b; try (iDestruct "Hb" as "%"; contradiction).
- wp_apply (release_spec with "[$IL $HLocked Hp Hb]"); first done.
{ iExists _. iFrame. }
iIntros. wp_pures. iApply "Hcont". iLeft. done.
- destruct b; try (iDestruct "Hb" as "%"; contradiction).
simpl. iDestruct "Hb" as "[Hψ Hb]".
wp_store.
wp_apply (release_spec with "[$IL $HLocked Hp Hb]"); first done.
{ iExists _. iFrame. }
iIntros (_).
wp_pures.
iApply "Hcont".
iRight. iExists _. by iFrame.
Qed.
End spec.
......@@ -3,7 +3,7 @@
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang proofmode notation.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import frac_auth.
From iris.algebra Require Import numbers frac_auth.
From iris_examples.lecture_notes Require Import modular_incr.
......
......@@ -9,6 +9,7 @@ From iris.base_logic.lib Require Export invariants.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode.
From iris.heap_lang Require Import notation lang.
From iris.algebra Require Import numbers.
From iris.heap_lang.lib Require Import par.
......@@ -356,7 +357,7 @@ End monotone_counter.
As we stated in an exercise in the counter modules section of the lecture
notes, the resource algebra we constructed above is nothing but Auth(N_max).
Auth and N_max are both part of the iris Coq library. They are called authR
and mnatUR (standing for authoritative Resource algebra and max nat Unital
and max_natUR (standing for authoritative Resource algebra and max nat Unital
Resource algebra). *)
(* Auth is defined in iris.algebra.auth. *)
......@@ -404,40 +405,44 @@ End auth_update.
Section monotone_counter'.
(* We tell Coq that our Iris instantiation has the following resource
algebras. Note that the only diffference from above is that we use authR
mnatUR in place of the resource algebra mcounterRA we constructed above. *)
Class mcounterG' Σ := MCounterG' { mcounter_inG' :> inG Σ (authR mnatUR)}.
Definition mcounterΣ' : gFunctors := #[GFunctor (authR mnatUR)].
max_natUR in place of the resource algebra mcounterRA we constructed above. *)
Class mcounterG' Σ := MCounterG' { mcounter_inG' :> inG Σ (authR max_natUR)}.
Definition mcounterΣ' : gFunctors := #[GFunctor (authR max_natUR)].
Instance subG_mcounterΣ' {Σ} : subG mcounterΣ' Σ mcounterG' Σ.
Proof. solve_inG. Qed.
(* We now prove the same three properties we claim were required from the resource
algebra in Section 7.7. *)
Instance mcounterRA_frag_core' (n : mnatUR): CoreId ( n).
Instance mcounterRA_frag_core' (n : max_natUR): CoreId ( n).
Proof.
apply _.
(* CoreID is a typeclass, so typeclass search can automatically deduce what
we want. Concretely, the proof follows by lemmas auth_frag_core_id and
mnat_core_id proved in the Iris Coq library. *)
max_nat_core_id proved in the Iris Coq library. *)
Qed.
Lemma mcounterRA_valid_auth_frag' (m n : mnatUR): ( m n) (n m)%nat.
Lemma mcounterRA_valid_auth_frag' (m n : max_natUR): ( m n) (max_nat_car n max_nat_car m)%nat.
Proof.
(* Use a simplified definition of validity for when the underlying CMRA is discrete, i.e., an RA.
The general definition also involves the use of step-indices, which is not needed in our case. *)
rewrite auth_both_valid.
split.
- intros [? _]; by apply mnat_included.
- intros ?%mnat_included; done.
- intros [? _]; by apply max_nat_included.
- intros ?%max_nat_included; done.
Qed.
Lemma mcounterRA_update' (m n : mnatUR): m n ~~> (S m : mnatUR) (S n : mnatUR).
Lemma max_nat_op_succ m : MaxNat (S m) = MaxNat m MaxNat (S m).
Proof. rewrite max_nat_op_max. apply f_equal. lia. Qed.
Lemma mcounterRA_update' (m n : max_natUR) :
m n ~~> MaxNat (S (max_nat_car m)) MaxNat (S (max_nat_car n)).
Proof.
replace (S m) with (m (S m)); last auto with arith.
replace (S n) with (n (S n)); last auto with arith.
apply cmra_update_valid0; intros ?%cmra_discrete_valid%mcounterRA_valid_auth_frag'.
apply auth_update_add'; first reflexivity.
exists (S m); symmetry; apply max_r; auto with arith.
destruct m as [m], n as [n]. simpl.
rewrite (max_nat_op_succ m) (max_nat_op_succ n).
apply cmra_update_valid0. intros ?%cmra_discrete_valid%mcounterRA_valid_auth_frag'.
simpl in *. apply auth_update_add'; first reflexivity.
exists (MaxNat (S m)). rewrite max_nat_op_max. apply f_equal. lia.
Qed.
(* We can now verify the programs. *)
......@@ -447,9 +452,9 @@ Section monotone_counter'.
(* The rest of this section is exactly the same as the preceding one. We use
the properties of the RA we have proved above. *)
Definition counter_inv' ( : loc) (γ : gname) : iProp := ( (m : mnatUR), #m own γ ( m))%I.
Definition counter_inv' ( : loc) (γ : gname) : iProp := ( (m : nat), #m own γ ( MaxNat m))%I.
Definition isCounter' ( : loc) (n : mnatUR) : iProp :=
Definition isCounter' ( : loc) (n : max_natUR) : iProp :=
( γ, own γ ( n) inv N (counter_inv' γ))%I.
Global Instance isCounter_persistent' n: Persistent (isCounter' n).
......@@ -457,12 +462,12 @@ Section monotone_counter'.
apply _.
Qed.
Lemma newCounter_spec': {{{ True }}} newCounter #() {{{ v, RET #v; isCounter' v 0%nat }}}.
Lemma newCounter_spec': {{{ True }}} newCounter #() {{{ v, RET #v; isCounter' v (MaxNat 0) }}}.
Proof.
iIntros (Φ) "_ HCont".
rewrite /newCounter -wp_fupd.
wp_lam.
iMod (own_alloc ( (0%nat : mnatUR) (0%nat : mnatUR))) as (γ) "[HAuth HFrac]".
iMod (own_alloc ( MaxNat 0 MaxNat 0)) as (γ) "[HAuth HFrac]".
- apply mcounterRA_valid_auth_frag'; auto.
- wp_alloc as "Hpt".
iMod (inv_alloc N _ (counter_inv' γ) with "[Hpt HAuth]") as "HInv".
......@@ -472,7 +477,7 @@ Section monotone_counter'.
Qed.
(* The read method specification. *)
Lemma read_spec' n: {{{ isCounter' n }}} read # {{{ m, RET #m; n m%nat }}}.
Lemma read_spec' n : {{{ isCounter' (MaxNat n) }}} read # {{{ m, RET #m; n m%nat }}}.
Proof.
iIntros (Φ) "HCounter HCont".
iDestruct "HCounter" as (γ) "[HOwnFrag HInv]".
......@@ -488,7 +493,7 @@ Section monotone_counter'.
Qed.
(* The read method specification. *)
Lemma incr_spec' n: {{{ isCounter' n }}} incr # {{{ RET #(); isCounter' (1 + n)%nat }}}.
Lemma incr_spec' n : {{{ isCounter' (MaxNat n) }}} incr # {{{ RET #(); isCounter' (MaxNat (1 + n)) }}}.
Proof.
iIntros (Φ) "HCounter HCont".
iDestruct "HCounter" as (γ) "[HOwnFrag #HInv]".
......@@ -507,7 +512,7 @@ Section monotone_counter'.
iInv N as (k) ">[Hpt HOwnAuth]" "HClose".
destruct (decide (k = m)); subst.
+ wp_cmpxchg_suc.
iMod (own_update γ (( m n)) ( (S m : mnatUR) ( (S n : mnatUR))) with "[HOwnFrag HOwnAuth]") as "[HOwnAuth HOwnFrag]".
iMod (own_update γ ( (MaxNat m) (MaxNat n)) ( (MaxNat (S m)) ( (MaxNat (S n)))) with "[HOwnFrag HOwnAuth]") as "[HOwnAuth HOwnFrag]".
{ apply mcounterRA_update'. }
{ rewrite own_op; iFrame. }
iMod ("HClose" with "[Hpt HOwnAuth]") as "_".
......
(* This file contains the specification of the lock module implemented as a simple spin lock and discussed in
section 7.6 in the invariants and ghost state chapter of the Iris Lecture Notes.
(* This file contains the specification of the lock module implemented as a
simple spin lock and discussed in section 7.6 in the invariants and ghost
state chapter of the Iris Lecture Notes.
*)
(* Contains definitions of the weakest precondition assertion, and its basic rules. *)
......@@ -10,9 +11,9 @@ From iris.program_logic Require Export weakestpre.
the lang file contains the actual language syntax. *)
From iris.heap_lang Require Export notation lang.
(* Files related to the interactive proof mode. The first import includes the
general tactics of the proof mode. The second provides some more specialized
tactics particular to the instantiation of Iris to a particular programming
(* Files related to the interactive proof mode. The first import includes the
general tactics of the proof mode. The second provides some more specialized
tactics particular to the instantiation of Iris to a particular programming
language. *)
From iris.proofmode Require Export tactics.
From iris.heap_lang Require Import proofmode.
......@@ -23,40 +24,39 @@ From iris.base_logic.lib Require Export invariants.
(* The exclusive resource algebra. *)
From iris.algebra Require Import excl.
Section lock_model.
Class lockG Σ := lock_G :> inG Σ (exclR unitR).
Section lock_model.
(* In order to do the proof we need to assume certain things about the
instantiation of Iris. The particular, even the heap is handled in an
analogous way as other ghost state. This line states that we assume the Iris
instantiation has sufficient structure to manipulate the heap, e.g., it
allows us to use the points-to predicate, and that the ghost state includes
the exclusive resource algebra over the singleton set (represented using the
unitR type). *)
unitR type). *)
Context `{heapG Σ, lockG Σ}.
Context `{heapG Σ}.
Context `{inG Σ (exclR unitR)}.
(* We use a ghost name with a token to model whether the lock is locked or not.
The the token is just exclusive ownerwhip of unit value. *)
Definition locked γ := own γ (Excl ()).
(* The name of a lock. *)
Definition lockN (l : loc) := nroot .@ "lock" .@ l.
Definition lockN (l : val) := nroot .@ "lock" .@ l.
(* The lock invariant *)
Definition is_lock γ l P :=
inv (lockN l) ((l (#false) P locked γ)
l (#true))%I.
Definition is_lock γ (v : val) P :=
( ( : loc), v = #ℓ⌝ inv (lockN v) ( #false P locked γ #true))%I.
(* The is_lock predicate is persistent *)
Global Instance is_lock_persistent γ l Φ : Persistent (is_lock γ l Φ).
Proof. apply _. Qed.
End lock_model.
Section lock_code.
(* Here is the standard spin lock code *)
(* The standard spin lock code *)
Definition newlock : val := λ: <>, ref #false.
Definition acquire : val :=
rec: "acquire" "l" :=
......@@ -66,11 +66,10 @@ Section lock_code.
End lock_code.
Section lock_spec.
Context `{heapG Σ}.
Context `{inG Σ (exclR unitR)}.
Context `{heapG Σ, lockG Σ}.
Lemma wp_newlock_t P:
{{{ P }}} newlock #() {{{v, RET v; (l: loc) γ, v = #l is_lock γ l P }}}.
Lemma newlock_spec P :
{{{ P }}} newlock #() {{{ l, RET l; γ, is_lock γ l P }}}.
Proof.
iIntros (φ) "Hi Hcont".
rewrite -wp_fupd /newlock.
......@@ -82,21 +81,21 @@ Section lock_spec.
as "Hinv"; last eauto.
{ iNext; iLeft; iFrame. }
iApply "Hcont".
iExists l, γ.
iModIntro. iSplit; first done.
iExists γ. iModIntro. iExists l. iSplit; first done.
iFrame.
Qed.
Lemma wp_acquire_t E γ l P :
Lemma acquire_spec E γ l P :
nclose (lockN l) E
{{{ is_lock γ l P }}} acquire (#l) @ E {{{v, RET #v; P locked γ}}}.
{{{ is_lock γ l P }}} acquire l @ E {{{ v, RET #v; P locked γ }}}.
Proof.
iIntros (HE φ) "#Hi Hcont"; rewrite /acquire.
iDestruct "Hi" as ( ->) "Hinv".
iLöb as "IH".
wp_rec.
wp_bind (CmpXchg _ _ _).
iInv (lockN l) as "[(Hl & HP & Ht)|Hl]" "Hcl".
- wp_cmpxchg_suc.
iInv (lockN #) as "[(Hl & HP & Ht)|Hl]" "Hcl".
- wp_cmpxchg_suc.
iMod ("Hcl" with "[Hl]") as "_"; first by iRight.
iModIntro.
wp_proj.
......@@ -108,17 +107,18 @@ Section lock_spec.
iModIntro.
wp_proj.
wp_if.
iApply ("IH" with "[$Hcont]").
iApply ("IH" with "Hcont").
Qed.
Lemma wp_release_t E γ l P :
Lemma release_spec E γ l P :
nclose (lockN l) E
{{{ is_lock γ l P locked γ P }}} release (#l) @ E {{{RET #(); True}}}.
{{{ is_lock γ l P locked γ P }}} release l @ E {{{ RET #(); True}}}.
Proof.
iIntros (HE φ) "(#Hi & Hld & HP) Hcont"; rewrite /release.
iDestruct "Hi" as ( ->) "Hinv".
wp_lam.
iInv (lockN l) as "[(Hl & HQ & >Ht)|Hl]" "Hcl".
- iDestruct (own_valid_2 with "Hld Ht") as %Hv. done.
iInv (lockN #) as "[(Hl & HQ & >Ht)|Hl]" "Hcl".
- iDestruct (own_valid_2 with "Hld Ht") as %Hv. done.
- wp_store.
iMod ("Hcl" with "[-Hcont]") as "_"; first by iNext; iLeft; iFrame.
iApply "Hcont".
......
From iris.algebra Require Import excl auth list gset gmap agree csum.
From iris.algebra Require Import numbers excl auth list gset gmap agree csum.
From iris.bi.lib Require Import fractional.
From iris.proofmode Require Import tactics.
From iris.base_logic.lib Require Export invariants proph_map saved_prop.
......@@ -116,7 +116,7 @@ Definition per_slot :=
Definition eltsUR := authR $ optionUR $ exclR $ listO locO.
Definition contUR := csumR (exclR unitR) (agreeR (prodO natO natO)).
Definition slotUR := authR $ gmapUR nat per_slot.
Definition backUR := authR mnatUR.
Definition backUR := authR max_natUR.
Class hwqG Σ :=
HwqG {
......@@ -182,12 +182,12 @@ Proof. iIntros "H1 H2". by iDestruct (own_valid_2 with "H1 H2") as %?. Qed.
(** Operations for the CMRA used to show that back only increases. *)
Definition back_value γb n := own γb ( (n : mnatUR) : backUR).
Definition back_lower_bound γb n := own γb ( (n : mnatUR) : backUR).
Definition back_value γb n := own γb ( MaxNat n).
Definition back_lower_bound γb n := own γb ( MaxNat n).
Lemma new_back : |==> γb, back_value γb 0.
Proof.
iMod (own_alloc ( (0 : mnatUR) : backUR)) as (γb) "H●".
iMod (own_alloc ( MaxNat 0)) as (γb) "H●".
- by rewrite auth_auth_valid.
- by iExists γb.
Qed.
......@@ -196,14 +196,14 @@ Lemma back_incr γb n :
back_value γb n == back_value γb (S n).
Proof.
iIntros "H●". iMod (own_update with "H●") as "[$ _]"; last done.
apply auth_update_alloc, (mnat_local_update _ _ (S n)). by lia.
apply auth_update_alloc, (max_nat_local_update _ _ (MaxNat (S n))). simpl. lia.
Qed.
Lemma back_snapshot γb n :
back_value γb n == back_value γb n back_lower_bound γb n.
Proof.
iIntros "H●". rewrite -own_op. iApply (own_update with "H●").
by apply auth_update_alloc, mnat_local_update.
by apply auth_update_alloc, max_nat_local_update.
Qed.
Lemma back_le γb n1 n2 :
......@@ -211,8 +211,7 @@ Lemma back_le γb n1 n2 :
Proof.
iIntros "H1 H2". iCombine "H1 H2" as "H".
iDestruct (own_valid with "H") as %Hvalid. iPureIntro.
apply auth_both_valid in Hvalid as [H1 H2].
by apply mnat_included.
apply auth_both_valid in Hvalid as [H1%max_nat_included _]. done.
Qed.
(* Stores a lower bound on the [i2] part of any contradiction that
......@@ -228,14 +227,14 @@ Lemma i2_lower_bound_update γi n m :
i2_lower_bound γi n == i2_lower_bound γi m.
Proof.
iIntros (H) "H●". iMod (own_update with "H●") as "[$ _]"; last done.
apply auth_update_alloc, (mnat_local_update _ _ m). by lia.
apply auth_update_alloc, (max_nat_local_update _ _ (MaxNat m)). simpl. lia.
Qed.
Lemma i2_lower_bound_snapshot γi n :
i2_lower_bound γi n == i2_lower_bound γi n no_contra_wit γi n.
Proof.
iIntros "H●". rewrite -own_op. iApply (own_update with "H●").
by apply auth_update_alloc, mnat_local_update.
by apply auth_update_alloc, max_nat_local_update.
Qed.
(** Operations for the one-shot CMRA used for contradiction states. *)
......
......@@ -2,8 +2,6 @@ From iris.proofmode Require Import tactics.
From iris.algebra Require Import auth gmap agree.
From iris_examples.logrel.F_mu_ref_conc Require Import logrel_binary.
Import uPred.
From iris.algebra Require deprecated.
Import deprecated.dec_agree.
Definition stackUR : ucmraT := gmapUR loc (agreeR valO).
......
From iris_examples.logrel.heaplang Require Export ltyping.
From iris.heap_lang.lib Require Import assert.
From iris.algebra Require Import auth.
From iris.algebra Require Import numbers auth.
From iris.base_logic.lib Require Import invariants.
From iris.heap_lang Require Import notation proofmode.
......@@ -13,8 +13,8 @@ Definition symbol_adt_ty `{heapG Σ} : lty Σ :=
(() A, (() A) * (A ()))%lty.
(* The required ghost theory *)
Class symbolG Σ := { symbol_inG :> inG Σ (authR mnatUR) }.
Definition symbolΣ : gFunctors := #[GFunctor (authR mnatUR)].
Class symbolG Σ := { symbol_inG :> inG Σ (authR max_natUR) }.
Definition symbolΣ : gFunctors := #[GFunctor (authR max_natUR)].
Instance subG_symbolΣ {Σ} : subG symbolΣ Σ symbolG Σ.
Proof. solve_inG. Qed.
......@@ -22,8 +22,8 @@ Proof. solve_inG. Qed.
Section symbol_ghosts.
Context `{!symbolG Σ}.
Definition counter (γ : gname) (n : nat) : iProp Σ := own γ ( (n : mnat)).
Definition symbol (γ : gname) (n : nat) : iProp Σ := own γ ( (S n : mnat)).
Definition counter (γ : gname) (n : nat) : iProp Σ := own γ ( (MaxNat n)).
Definition symbol (γ : gname) (n : nat) : iProp Σ := own γ ( (MaxNat (S n))).
Global Instance counter_timeless γ n : Timeless (counter γ n).
Proof. apply _. Qed.
......@@ -39,7 +39,7 @@ Section symbol_ghosts.
Lemma counter_alloc n : |==> γ, counter γ n.
Proof.
iMod (own_alloc ( (n:mnat) (n:mnat))) as (γ) "[Hγ Hγf]";
iMod (own_alloc ( MaxNat n MaxNat n)) as (γ) "[Hγ Hγf]";
first by apply auth_both_valid.
iExists γ. by iFrame.
Qed.
......@@ -47,14 +47,14 @@ Section symbol_ghosts.
Lemma counter_inc γ n : counter γ n == counter γ (S n) symbol γ n.
Proof.
rewrite -own_op.
apply own_update, auth_update_alloc, mnat_local_update. omega.
apply own_update, auth_update_alloc, max_nat_local_update. simpl. lia.
Qed.
Lemma symbol_obs γ s n : counter γ n - symbol γ s - (s < n)%nat.
Proof.
iIntros "Hc Hs".
iDestruct (own_valid_2 with "Hc Hs") as %[?%mnat_included _]%auth_both_valid.
iPureIntro. omega.
iDestruct (own_valid_2 with "Hc Hs") as %[?%max_nat_included _]%auth_both_valid.
simpl in *. iPureIntro. lia.
Qed.
End symbol_ghosts.
......