Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found

Target

Select target project
  • iris/iris
  • jeehoon.kang/iris-coq
  • amintimany/iris-coq
  • dfrumin/iris-coq
  • Villetaneuse/iris
  • gares/iris
  • shiatsumat/iris
  • Blaisorblade/iris
  • jihgfee/iris-coq
  • mrhaandi/iris
  • tlsomers/iris
  • Quarkbeast/iris-coq
  • janno/iris
  • amaurremi/iris-coq
  • proux/iris
  • tchajed/iris
  • herbelin/iris-coq
  • msammler/iris-coq
  • maximedenes/iris-coq
  • bpeters/iris
  • haidang/iris
  • lepigre/iris
  • lczch/iris
  • simonspies/iris
  • gpirlea/iris
  • dkhalanskiyjb/iris
  • gmalecha/iris
  • germanD/iris
  • aa755/iris
  • jules/iris
  • abeln/iris
  • simonfv/iris
  • atrieu/iris
  • arthuraa/iris
  • simonh/iris
  • jung/iris
  • mattam82/iris
  • Armael/iris
  • adamAndMath/iris
  • gmevel/iris
  • snyke7/iris
  • johannes/iris
  • NiklasM/iris
  • simonspies/iris-parametric-index
  • svancollem/iris
  • proux1/iris
  • wmansky/iris
  • LukeXuan/iris
  • ivanbakel/iris
  • SkySkimmer/iris
  • tjhance/iris
  • yiyunliu/iris
  • Lee-Janggun/iris
  • thomas-lamiaux/iris
  • dongjae/iris
  • dnezam/iris
  • Tragicus/iris
  • clef-men/iris
  • ffengyu/iris
59 results
Show changes
Commits on Source (12)
...@@ -3,6 +3,16 @@ way the logic is used on paper. We also document changes in the Coq ...@@ -3,6 +3,16 @@ way the logic is used on paper. We also document changes in the Coq
development; every API-breaking change should be listed, but not every new development; every API-breaking change should be listed, but not every new
lemma. lemma.
## Iris master
**Changes in `algebra`:**
* Add lemma `ufrac_auth_update_surplus_cancel`.
**Changes in `heap_lang`:**
* Add `Inhabited lock_name` to `lock` class. (by Daniel Nezamabadi)
## Iris 4.3.0 (2024-10-30) ## Iris 4.3.0 (2024-10-30)
This Iris release mostly features quality-of-life improvements, such as This Iris release mostly features quality-of-life improvements, such as
......
...@@ -178,10 +178,9 @@ Getting along with Iris in Coq: ...@@ -178,10 +178,9 @@ Getting along with Iris in Coq:
Contacting the developers: Contacting the developers:
* Discussion about the Iris Coq development happens on the mailing list * Discussion about the Iris Coq development happens in the [Iris
[iris-club@lists.mpi-sws.org](https://lists.mpi-sws.org/listinfo/iris-club) Chat](https://iris-project.org/chat.html). This is also the right place to ask
and in the [Iris Chat](https://iris-project.org/chat.html). This is also the questions.
right place to ask questions.
* If you want to report a bug, please use the * If you want to report a bug, please use the
[issue tracker](https://gitlab.mpi-sws.org/iris/iris/issues), which requires [issue tracker](https://gitlab.mpi-sws.org/iris/iris/issues), which requires
an MPI-SWS GitLab account. The [chat page](https://iris-project.org/chat.html) an MPI-SWS GitLab account. The [chat page](https://iris-project.org/chat.html)
......
...@@ -144,14 +144,34 @@ Section ufrac_auth. ...@@ -144,14 +144,34 @@ Section ufrac_auth.
Qed. Qed.
Lemma ufrac_auth_update_surplus p q a b : Lemma ufrac_auth_update_surplus p q a b :
(a b) U_p a ~~> U_(p+q) (a b) U_q b. (a b) U_p a ~~> U_(p+q) (a b) U_q b.
Proof. Proof.
intros Hconsistent. apply: auth_update_alloc. intros Hconsistent. apply: auth_update_alloc. apply local_update_unital.
intros n m; simpl; intros [Hvalid1 Hvalid2] Heq. intros n mpa; simpl; intros [Hvalid1 Hvalid2] Heq; simplify_eq/=.
split. split.
- split; by apply cmra_valid_validN. - split; by apply cmra_valid_validN.
- rewrite pair_op Some_op Heq comm. - rewrite pair_op Some_op Heq comm.
destruct m; simpl; [rewrite left_id | rewrite right_id]; done. destruct mpa; simpl; [rewrite left_id | rewrite right_id]; done.
Qed.
Lemma ufrac_auth_update_surplus_cancel p q a b :
Cancelable b
U_(p+q) (a b) U_q b ~~> U_p a.
Proof.
intros. apply: auth_update_dealloc. apply local_update_unital.
intros n mpa; simpl; intros [Hvalid1 Hvalid2] Heq; simplify_eq/=.
split.
{ split; by eapply cmra_validN_op_l. }
rewrite (comm _ p) (comm _ a) in Heq.
destruct mpa as [[p' a']|]; simplify_eq/=.
- rewrite -Some_op in Heq.
apply (inj _) in Heq as [Hp%leibniz_equiv Ha]; simplify_eq/=.
apply (inj _) in Hp as ->.
apply (cancelableN _) in Ha; last by rewrite comm.
by repeat constructor.
- rewrite right_id in Heq.
apply (inj _) in Heq as [Hp%leibniz_equiv _]; simplify_eq/=.
by apply Qp.add_id_free in Hp.
Qed. Qed.
End ufrac_auth. End ufrac_auth.
......
...@@ -18,9 +18,9 @@ of the day (via [bupd_alt (■ P) ⊢ ■ P]). ...@@ -18,9 +18,9 @@ of the day (via [bupd_alt (■ P) ⊢ ■ P]).
We show that: We show that:
1. [bupd_alt] enjoys the usual rules of the basic update modality. 1. [bupd_alt] enjoys the usual rules of the basic update modality.
2. [bupd_alt] entails any other modality that enjoys the laws of a basic update 2. Any other modality that enjoys the laws of a basic update modality
modality (see [bupd_bupd_alt]). entails [bupd_alt] (see [bupd_bupd_alt]).
3. The ordinary basic update modality [|==>] on [uPred] entails [bupd_alt] 3. [bupd_alt] entails the ordinary basic update modality [|==>] on [uPred]
(see [bupd_alt_bupd]). This result is proven in the model of [uPred]. (see [bupd_alt_bupd]). This result is proven in the model of [uPred].
The first two points are shown for any BI with a plain modality. *) The first two points are shown for any BI with a plain modality. *)
......
...@@ -26,6 +26,7 @@ Class lock := Lock { ...@@ -26,6 +26,7 @@ Class lock := Lock {
lockG : gFunctors Type; lockG : gFunctors Type;
(** [name] is used to associate [locked] with [is_lock] *) (** [name] is used to associate [locked] with [is_lock] *)
lock_name : Type; lock_name : Type;
#[global] lock_name_inhabited :: Inhabited lock_name;
(** * Predicates *) (** * Predicates *)
(** No namespace [N] parameter because we only expose program specs, which (** No namespace [N] parameter because we only expose program specs, which
anyway have the full mask. *) anyway have the full mask. *)
......
...@@ -10,6 +10,7 @@ ...@@ -10,6 +10,7 @@
\RequirePackage{Tabbing} % Avoid the standard tabbing environment. Its \< conflicts with the semantic package. \RequirePackage{Tabbing} % Avoid the standard tabbing environment. Its \< conflicts with the semantic package.
\RequirePackage{xparse} \RequirePackage{xparse}
\RequirePackage{xcolor} \RequirePackage{xcolor}
\RequirePackage{mathpartir}
%% COLOR DEFINITIONS %% COLOR DEFINITIONS
\definecolor{rescolor}{HTML}{005504} \definecolor{rescolor}{HTML}{005504}
......