Commit 44a8a8fa authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'iris-3.3-port' into 'master'

Iris 3.3 port

See merge request !1
parents 0a42f504 7315df35
......@@ -23,6 +23,8 @@ _*_.tex
*.fdb_latexmk
*.fls
*.vo
*.vos
*.vok
*.glob
*.v.d
*.vio
......
......@@ -9,8 +9,8 @@ This tutorial comes in two versions:
For the tutorial material you need to have the following dependencies installed:
- Coq 8.8.2 / 8.9.1 / 8.10.1
- A development version of [Iris](https://gitlab.mpi-sws.org/iris/iris)
- Coq 8.11.2
- [Iris 3.3.0](https://gitlab.mpi-sws.org/iris/iris)
*Note:* the tutorial material will not work with earlier versions of Iris, it
is important to install the exact versions as given above.
......@@ -19,11 +19,9 @@ is important to install the exact versions as given above.
The easiest, and recommend, way of installing Iris and its dependencies is via
the OCaml package manager opam (2.0.0 or newer). You first have to add the Coq
opam repository and the Iris development repository (if you have not already
done so earlier):
opam repository (if you have not already done so earlier):
opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
Then you can do `make build-dep` to install exactly the right version of Iris.
......
......@@ -29,7 +29,7 @@ Section compatibility.
(** * Compatibility rules for expression typing *)
(** * Variables *)
Lemma Var_sem_typed Γ (x : string) A : Γ !! x = Some A (Γ x : A)%I.
Lemma Var_sem_typed Γ (x : string) A : Γ !! x = Some A Γ x : A.
Proof.
iIntros (HΓx vs) "!# #HΓ /=".
iDestruct (env_sem_typed_lookup with "HΓ") as (v ->) "HA"; first done.
......@@ -159,11 +159,11 @@ Section compatibility.
(** * Compatibility rules for value typing *)
(** ** Base types *)
Lemma UnitV_sem_typed : ( #() : ())%I.
Lemma UnitV_sem_typed : #() : ().
Proof. by iPureIntro. Qed.
Lemma BoolV_sem_typed (b : bool) : ( #b : sem_ty_bool)%I.
Lemma BoolV_sem_typed (b : bool) : #b : sem_ty_bool.
Proof. by iExists b. Qed.
Lemma IntV_sem_typed (n : Z) : ( #n : sem_ty_int)%I.
Lemma IntV_sem_typed (n : Z) : #n : sem_ty_int.
Proof. (* FILL IN YOUR PROOF *) Admitted.
(** ** Products and sums *)
......
......@@ -35,9 +35,9 @@ Section fundamental.
such mutually inductive proofs, we need to make sure ourselves that the
induction hypotheses is only used on smaller derivations. *)
Theorem fundamental Γ e τ ρ
(Hty : Γ e : τ) : (interp_env Γ ρ e : τ ρ)%I
(Hty : Γ e : τ) : interp_env Γ ρ e : τ ρ
with fundamental_val v τ ρ
(Hty : v : τ) : ( v : τ ρ)%I.
(Hty : v : τ) : v : τ ρ.
Proof.
- destruct Hty; simpl.
+ iApply Var_sem_typed. by apply lookup_interp_env.
......
......@@ -291,7 +291,7 @@ Definition add_two : val := λ: "x",
(** While this function is rather convoluted, the specification is precisely
what you would expect---it adds [2]. *)
Lemma wp_add_two `{!heapG Σ} (x : Z) :
WP add_two #x {{ w, w = #(2 + x) }}%I.
WP add_two #x {{ w, w = #(2 + x) }}.
(** Note that this weakest precondition does not have a premise (i.e. the
lemma does not involve a magic wand [-∗] at the top-level, as we have seen in
previous examples). We thus use the scope [%I] ([I] of "Iris") to instruct Coq
......@@ -406,7 +406,7 @@ Definition add_two_fancy : val := λ: "x",
!"lx".
Lemma wp_add_two_fancy `{!heapG Σ} (x : Z) :
WP add_two_fancy #x {{ w, w = #(2 + x) }}%I.
WP add_two_fancy #x {{ w, w = #(2 + x) }}.
Proof. (* FILL IN YOUR PROOF *) Admitted.
(** * Reasoning about "unsafe" programs *)
......@@ -424,7 +424,7 @@ Definition unsafe_pure : val := λ: <>,
if: #true then #13 else #13 #37.
Lemma wp_unsafe_pure `{!heapG Σ} :
WP unsafe_pure #() {{ v, v = #13 }}%I.
WP unsafe_pure #() {{ v, v = #13 }}.
Proof.
rewrite /unsafe_pure.
wp_pures.
......@@ -437,5 +437,5 @@ Definition unsafe_ref : val := λ: <>,
let: "l" := ref #0 in "l" <- #true;; !"l".
Lemma wp_unsafe_ref `{!heapG Σ} :
WP unsafe_ref #() {{ v, v = #true }}%I.
WP unsafe_ref #() {{ v, v = #true }}.
Proof. (* FILL IN YOUR PROOF *) Admitted.
......@@ -6,7 +6,7 @@ Section parametricity.
(** * The polymorphic identity function *)
Lemma identity_param `{!heapPreG Σ} e (v : val) σ w es σ' :
( `{!heapG Σ}, ( e : A, A A)%I)
( `{!heapG Σ}, e : A, A A)
rtc erased_step ([e <_> v]%E, σ) (of_val w :: es, σ') w = v.
Proof.
intros He.
......@@ -24,20 +24,20 @@ Section parametricity.
(** * Exercise (empty_type_param, easy) *)
Lemma empty_type_param `{!heapPreG Σ} e (v : val) σ w es σ' :
( `{!heapG Σ}, ( e : A, A)%I)
( `{!heapG Σ}, e : A, A)
rtc erased_step ([e <_>]%E, σ) (of_val w :: es, σ')
False.
Proof. (* FILL IN YOUR PROOF *) Admitted.
(** * Exercise (boolean_param, moderate) *)
Lemma boolean_param `{!heapPreG Σ} e (v1 v2 : val) σ w es σ' :
( `{!heapG Σ}, ( e : A, A A A)%I)
( `{!heapG Σ}, e : A, A A A)
rtc erased_step ([e <_> v1 v2]%E, σ) (of_val w :: es, σ') w = v1 w = v2.
Proof. (* FILL IN YOUR PROOF *) Admitted.
(** * Exercise (nat_param, hard) *)
Lemma nat_param `{!heapPreG Σ} e σ w es σ' :
( `{!heapG Σ}, ( e : A, (A A) A A)%I)
( `{!heapG Σ}, e : A, (A A) A A)
rtc erased_step ([e <_> (λ: "n", "n" + #1)%V #0]%E, σ)
(of_val w :: es, σ') n : nat, w = #n.
Proof. (* FILL IN YOUR PROOF *) Admitted.
......@@ -45,10 +45,10 @@ Section parametricity.
(** * Exercise (strong_nat_param, hard) *)
Lemma strong_nat_param `{!heapPreG Σ} e σ w es σ' (vf vz : val) φ :
( `{!heapG Σ}, Φ : sem_ty Σ,
( e : A, (A A) A A)%I
( w, {{{ Φ w }}} vf w {{{ w', RET w'; Φ w' }}})%I
(Φ vz)%I
( w, Φ w - ⌜φ w)%I)
( e : A, (A A) A A)
( w, {{{ Φ w }}} vf w {{{ w', RET w'; Φ w' }}})
( Φ vz)
( w, Φ w - ⌜φ w))
rtc erased_step ([e <_> vf vz]%E, σ) (of_val w :: es, σ') φ w.
Proof. (* FILL IN YOUR PROOF *) Admitted.
End parametricity.
......@@ -20,21 +20,21 @@ The proposition [adequate NotStuck e σ (λ v σ, φ v)] (which is defined in th
Iris library) means that [e], starting in heap [σ] does not get stuck, and if
[e] reduces to a value [v], we have [φ v]. *)
Lemma sem_gen_type_safety `{!heapPreG Σ} e σ φ :
( `{!heapG Σ}, A : sem_ty Σ, ( v, A v - ⌜φ v) ( e : A)%I)
( `{!heapG Σ}, A : sem_ty Σ, ( v, A v - ⌜φ v) e : A)
adequate NotStuck e σ (λ v σ, φ v).
Proof.
intros Hty. apply (heap_adequacy Σ NotStuck e σ)=> // ?.
specialize (Hty _) as (A & HA & Hty).
iStartProof. iDestruct (Hty $! ) as "#He".
iSpecialize ("He" with "[]"); first by rewrite /env_sem_typed.
rewrite subst_map_empty. iApply (wp_wand with "He"); auto.
rewrite subst_map_empty. iIntros "?". iApply (wp_wand with "He"); auto.
by iIntros; iApply HA.
Qed.
(** The actual theorem for semantic type safety lemma states that semantically
typed closed programs do not get stuck. It is a simple consequence of the lemma [sem_gen_type_safety] above. *)
Theorem sem_type_safety `{!heapPreG Σ} e σ es σ' e' :
( `{!heapG Σ}, A, ( e : A)%I)
( `{!heapG Σ}, A, e : A)
rtc erased_step ([e], σ) (es, σ') e' es
is_Some (to_val e') reducible e' σ'.
Proof.
......
......@@ -90,7 +90,7 @@ Section sem_typed.
iIntros "#HA #HΓ". by iApply (big_sepM2_insert_2 with "[] HΓ").
Qed.
Lemma env_sem_typed_empty : env_sem_typed .
Lemma env_sem_typed_empty : env_sem_typed .
Proof. iIntros "". by rewrite /env_sem_typed. Qed.
Lemma env_sem_typed_empty_l_inv vs : env_sem_typed vs - vs = ∅⌝.
Proof. by iIntros "?"; iApply big_sepM2_empty_r. Qed.
......
From iris.algebra Require Import auth.
From iris.algebra Require Import auth numbers.
From iris.base_logic Require Import lib.own.
From iris.proofmode Require Export tactics.
......@@ -14,8 +14,8 @@ generic mechanism for ghost state. These resources satisfy the following laws:
>>
*)
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.
......@@ -23,8 +23,8 @@ Proof. solve_inG. Qed.
Section symbol_ghost.
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.
......@@ -34,9 +34,9 @@ Section symbol_ghost.
Global Instance symbol_persistent γ n : Persistent (symbol γ n).
Proof. apply _. Qed.
Lemma counter_alloc n : (|==> γ, counter γ n)%I.
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.
......@@ -49,14 +49,15 @@ Section symbol_ghost.
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.
iPureIntro. simpl in *. lia.
Qed.
End symbol_ghost.
......
......@@ -29,7 +29,7 @@ Section two_state_ghost.
Definition two_state_final (γ : gname) : iProp Σ :=
own γ ( (Some ())).
Lemma two_state_init : (|==> γ, two_state_auth γ false)%I.
Lemma two_state_init : |==> γ, two_state_auth γ false.
Proof. iApply own_alloc. by apply auth_auth_valid. Qed.
Lemma two_state_update γ b :
......
......@@ -10,7 +10,7 @@ Section unsafe.
if: #true then #13 else #13 #37.
>>
*)
Lemma sem_typed_unsafe_pure : ( unsafe_pure : (() sem_ty_int))%I.
Lemma sem_typed_unsafe_pure : unsafe_pure : (() sem_ty_int).
Proof.
iIntros (vs) "!# HΓ /=". iApply wp_value.
iIntros "!#" (? ->). wp_lam. wp_if.
......@@ -24,7 +24,7 @@ Section unsafe.
Definition unsafe_ref : val := λ: <>,
let: "l" := ref #0 in "l" <- #true;; !"l".
>> *)
Lemma sem_typed_unsafe_ref : ( unsafe_ref : (() sem_ty_bool))%I.
Lemma sem_typed_unsafe_ref : unsafe_ref : (() sem_ty_bool).
Proof.
iIntros (vs) "!# HΓ /=". iApply wp_value.
iIntros "!#" (? ->). wp_lam.
......@@ -41,7 +41,7 @@ Section unsafe.
(λ: <>, assert: !"l" #0)).
Lemma sem_typed_unsafe_ref_ne_0 :
( unsafe_ref_ne_0 : (() (sem_ty_int ()) * (() ())))%I.
unsafe_ref_ne_0 : (() (sem_ty_int ()) * (() ())).
Proof.
iIntros (vs) "!# HΓ /=". iApply wp_value.
iIntros "!#" (? ->).
......@@ -87,7 +87,7 @@ Section unsafe.
λ: <>, let: "l" := ref #0 in λ: <>, "l" <- #true;; !"l".
Lemma sem_typed_unsafe_ref_reuse `{!two_stateG Σ}:
( unsafe_ref_reuse : (() (() sem_ty_bool)))%I.
unsafe_ref_reuse : (() (() sem_ty_bool)).
Proof.
iIntros (vs) "!# HΓ /=". iApply wp_value.
iIntros "!#" (? ->). wp_lam.
......@@ -137,7 +137,7 @@ Section unsafe.
Definition sem_ty_symbol (γ : gname) : sem_ty Σ := SemTy (λ w,
n : nat, w = #n symbol γ n)%I.
Lemma sem_typed_symbol_adt Γ : (Γ symbol_adt : symbol_adt_ty)%I.
Lemma sem_typed_symbol_adt Γ : Γ symbol_adt : symbol_adt_ty.
Proof.
iIntros (vs) "!# _ /=". iApply wp_value.
iIntros "!#" (v ->). wp_lam. wp_alloc l as "Hl"; wp_pures.
......
......@@ -9,7 +9,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/tutorial-popl20.git"
synopsis: "The Iris tutorial at POPL 2020"
depends: [
"coq-iris" { (= "dev.2020-01-18.0.446bc644") | (= "dev") }
"coq-iris" { (= "3.3.0") | (= "dev") }
]
build: [make "-j%{jobs}%"]
......
......@@ -29,7 +29,7 @@ Section compatibility.
(** * Compatibility rules for expression typing *)
(** * Variables *)
Lemma Var_sem_typed Γ (x : string) A : Γ !! x = Some A (Γ x : A)%I.
Lemma Var_sem_typed Γ (x : string) A : Γ !! x = Some A Γ x : A.
Proof.
iIntros (HΓx vs) "!# #HΓ /=".
iDestruct (env_sem_typed_lookup with "HΓ") as (v ->) "HA"; first done.
......@@ -220,11 +220,11 @@ Section compatibility.
(** * Compatibility rules for value typing *)
(** ** Base types *)
Lemma UnitV_sem_typed : ( #() : ())%I.
Lemma UnitV_sem_typed : #() : ().
Proof. by iPureIntro. Qed.
Lemma BoolV_sem_typed (b : bool) : ( #b : sem_ty_bool)%I.
Lemma BoolV_sem_typed (b : bool) : #b : sem_ty_bool.
Proof. by iExists b. Qed.
Lemma IntV_sem_typed (n : Z) : ( #n : sem_ty_int)%I.
Lemma IntV_sem_typed (n : Z) : #n : sem_ty_int.
(* REMOVE *) Proof. by iExists n. Qed.
(** ** Products and sums *)
......
......@@ -35,9 +35,9 @@ Section fundamental.
such mutually inductive proofs, we need to make sure ourselves that the
induction hypotheses is only used on smaller derivations. *)
Theorem fundamental Γ e τ ρ
(Hty : Γ e : τ) : (interp_env Γ ρ e : τ ρ)%I
(Hty : Γ e : τ) : interp_env Γ ρ e : τ ρ
with fundamental_val v τ ρ
(Hty : v : τ) : ( v : τ ρ)%I.
(Hty : v : τ) : v : τ ρ.
Proof.
- destruct Hty; simpl.
+ iApply Var_sem_typed. by apply lookup_interp_env.
......
......@@ -293,7 +293,7 @@ Definition add_two : val := λ: "x",
(** While this function is rather convoluted, the specification is precisely
what you would expect---it adds [2]. *)
Lemma wp_add_two `{!heapG Σ} (x : Z) :
WP add_two #x {{ w, w = #(2 + x) }}%I.
WP add_two #x {{ w, w = #(2 + x) }}.
(** Note that this weakest precondition does not have a premise (i.e. the
lemma does not involve a magic wand [-∗] at the top-level, as we have seen in
previous examples). We thus use the scope [%I] ([I] of "Iris") to instruct Coq
......@@ -344,7 +344,7 @@ work operate both on the MoSeL proof goal and the MoSeL proof context. *)
iApply wp_twice.
wp_load. wp_store.
wp_load. wp_store.
rewrite (_ : 2 = (1 + 1)) // -Z.add_assoc.
rewrite Z.add_assoc (_ : (1 + 1)%Z = 2) //.
iFrame.
auto.
Qed.
......@@ -417,7 +417,7 @@ Definition add_two_fancy : val := λ: "x",
!"lx".
Lemma wp_add_two_fancy `{!heapG Σ} (x : Z) :
WP add_two_fancy #x {{ w, w = #(2 + x) }}%I.
WP add_two_fancy #x {{ w, w = #(2 + x) }}.
(* REMOVE *) Proof.
rewrite /add_two_fancy. wp_pures.
wp_alloc lf as "Hlf".
......@@ -446,7 +446,7 @@ Definition unsafe_pure : val := λ: <>,
if: #true then #13 else #13 #37.
Lemma wp_unsafe_pure `{!heapG Σ} :
WP unsafe_pure #() {{ v, v = #13 }}%I.
WP unsafe_pure #() {{ v, v = #13 }}.
Proof.
rewrite /unsafe_pure.
wp_pures.
......@@ -459,7 +459,7 @@ Definition unsafe_ref : val := λ: <>,
let: "l" := ref #0 in "l" <- #true;; !"l".
Lemma wp_unsafe_ref `{!heapG Σ} :
WP unsafe_ref #() {{ v, v = #true }}%I.
WP unsafe_ref #() {{ v, v = #true }}.
(* REMOVE *) Proof.
rewrite /unsafe_ref. wp_pures.
wp_alloc l.
......
......@@ -6,7 +6,7 @@ Section parametricity.
(** * The polymorphic identity function *)
Lemma identity_param `{!heapPreG Σ} e (v : val) σ w es σ' :
( `{!heapG Σ}, ( e : A, A A)%I)
( `{!heapG Σ}, e : A, A A)
rtc erased_step ([e <_> v]%E, σ) (of_val w :: es, σ') w = v.
Proof.
intros He.
......@@ -24,7 +24,7 @@ Section parametricity.
(** * Exercise (empty_type_param, easy) *)
Lemma empty_type_param `{!heapPreG Σ} e (v : val) σ w es σ' :
( `{!heapG Σ}, ( e : A, A)%I)
( `{!heapG Σ}, e : A, A)
rtc erased_step ([e <_>]%E, σ) (of_val w :: es, σ')
False.
(* REMOVE *) Proof.
......@@ -43,7 +43,7 @@ Section parametricity.
(** * Exercise (boolean_param, moderate) *)
Lemma boolean_param `{!heapPreG Σ} e (v1 v2 : val) σ w es σ' :
( `{!heapG Σ}, ( e : A, A A A)%I)
( `{!heapG Σ}, e : A, A A A)
rtc erased_step ([e <_> v1 v2]%E, σ) (of_val w :: es, σ') w = v1 w = v2.
(* REMOVE *) Proof.
intros He.
......@@ -65,7 +65,7 @@ Section parametricity.
(** * Exercise (nat_param, hard) *)
Lemma nat_param `{!heapPreG Σ} e σ w es σ' :
( `{!heapG Σ}, ( e : A, (A A) A A)%I)
( `{!heapG Σ}, e : A, (A A) A A)
rtc erased_step ([e <_> (λ: "n", "n" + #1)%V #0]%E, σ)
(of_val w :: es, σ') n : nat, w = #n.
(* REMOVE *) Proof.
......@@ -93,10 +93,10 @@ Section parametricity.
(** * Exercise (strong_nat_param, hard) *)
Lemma strong_nat_param `{!heapPreG Σ} e σ w es σ' (vf vz : val) φ :
( `{!heapG Σ}, Φ : sem_ty Σ,
( e : A, (A A) A A)%I
( w, {{{ Φ w }}} vf w {{{ w', RET w'; Φ w' }}})%I
(Φ vz)%I
( w, Φ w - ⌜φ w)%I)
( e : A, (A A) A A)
( w, {{{ Φ w }}} vf w {{{ w', RET w'; Φ w' }}})
( Φ vz)
( w, Φ w - ⌜φ w))
rtc erased_step ([e <_> vf vz]%E, σ) (of_val w :: es, σ') φ w.
(* REMOVE *) Proof.
intros He.
......
......@@ -20,21 +20,21 @@ The proposition [adequate NotStuck e σ (λ v σ, φ v)] (which is defined in th
Iris library) means that [e], starting in heap [σ] does not get stuck, and if
[e] reduces to a value [v], we have [φ v]. *)
Lemma sem_gen_type_safety `{!heapPreG Σ} e σ φ :
( `{!heapG Σ}, A : sem_ty Σ, ( v, A v - ⌜φ v) ( e : A)%I)
( `{!heapG Σ}, A : sem_ty Σ, ( v, A v - ⌜φ v) e : A)
adequate NotStuck e σ (λ v σ, φ v).
Proof.
intros Hty. apply (heap_adequacy Σ NotStuck e σ)=> // ?.
specialize (Hty _) as (A & HA & Hty).
iStartProof. iDestruct (Hty $! ) as "#He".
iSpecialize ("He" with "[]"); first by rewrite /env_sem_typed.
rewrite subst_map_empty. iApply (wp_wand with "He"); auto.
rewrite subst_map_empty. iIntros "?". iApply (wp_wand with "He"); auto.
by iIntros; iApply HA.
Qed.
(** The actual theorem for semantic type safety lemma states that semantically
typed closed programs do not get stuck. It is a simple consequence of the lemma [sem_gen_type_safety] above. *)
Theorem sem_type_safety `{!heapPreG Σ} e σ es σ' e' :
( `{!heapG Σ}, A, ( e : A)%I)
( `{!heapG Σ}, A, e : A)
rtc erased_step ([e], σ) (es, σ') e' es
is_Some (to_val e') reducible e' σ'.
Proof.
......
......@@ -90,7 +90,7 @@ Section sem_typed.
iIntros "#HA #HΓ". by iApply (big_sepM2_insert_2 with "[] HΓ").
Qed.
Lemma env_sem_typed_empty : env_sem_typed .
Lemma env_sem_typed_empty : env_sem_typed .
Proof. iIntros "". by rewrite /env_sem_typed. Qed.
Lemma env_sem_typed_empty_l_inv vs : env_sem_typed vs - vs = ∅⌝.
Proof. by iIntros "?"; iApply big_sepM2_empty_r. Qed.
......
From iris.algebra Require Import auth.
From iris.algebra Require Import auth numbers.
From iris.base_logic Require Import lib.own.
From iris.proofmode Require Export tactics.
......@@ -14,8 +14,8 @@ generic mechanism for ghost state. These resources satisfy the following laws:
>>
*)
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.
......@@ -23,8 +23,8 @@ Proof. solve_inG. Qed.
Section symbol_ghost.
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.
......@@ -34,9 +34,9 @@ Section symbol_ghost.
Global Instance symbol_persistent γ n : Persistent (symbol γ n).
Proof. apply _. Qed.
Lemma counter_alloc n : (|==> γ, counter γ n)%I.
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.
......@@ -49,14 +49,15 @@ Section symbol_ghost.
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.
iPureIntro. simpl in *. lia.
Qed.
End symbol_ghost.
......