Commit 291d150c authored by Yusuke Matsushita's avatar Yusuke Matsushita Committed by Ralf Jung
Browse files

Fix typos

parent a1f5f2f6
......@@ -406,7 +406,7 @@ Spies, and Tej Chajed. Thanks a lot to everyone involved!
* Make lemma `Excl_included` a bi-implication.
* Make `auth_update_core_id` work with any fraction of the authoritative
element.
* Add `min_nat`, a RA for natural numbers with `min` as the operation.
* Add `min_nat`, an RA for natural numbers with `min` as the operation.
* Add many missing `Proper`/non-expansiveness lemmas for maps and lists.
* Add `list_singletonM_included` and `list_lookup_singletonM_{lt,gt}` lemmas
about singletons in the list RA.
......
......@@ -91,11 +91,11 @@ from which we can derive
\subsection{Boxes}
The idea behind the \emph{boxes} is to have an proposition $\prop$ that is actually split into a number of pieces, each of which can be taken out and back in separately.
The idea behind the \emph{boxes} is to have a proposition $\prop$ that is actually split into a number of pieces, each of which can be taken out and back in separately.
In some sense, this is a replacement for having an ``authoritative PCM of Iris propositions itself''.
It is similar to the pattern involving saved propositions that was used for the barrier~\cite{iris2}, but more complicated because there are some operations that we want to perform without a later.
Roughly, the idea is that a \emph{box} is a container for an proposition $\prop$.
Roughly, the idea is that a \emph{box} is a container for a proposition $\prop$.
A box consists of a bunch of \emph{slices} which decompose $\prop$ into a separating conjunction of the propositions $\propB_\sname$ governed by the individual slices.
Each slice is either \emph{full} (it right now contains $\propB_\sname$), or \emph{empty} (it does not contain anything currently).
The proposition governing the box keeps track of the state of all the slices that make up the box.
......
......@@ -23,7 +23,7 @@ We assume to have the following four cameras available:
\end{align*}
The last two are the tokens used for managing invariants, $\textdom{Inv}$ is the monoid used to manage the invariants themselves.
We assume that at the beginning of the verification, instances named $\gname_{\textdom{State}}$, $\gname_{\textdom{Inv}}$, $\gname_{\textdom{En}}$ and $\gname_{\textdom{Dis}}$ of these cameras have been created, such that these names are globally known.
We assume that at the beginning of the verification, instances named $\gname_{\textdom{Inv}}$, $\gname_{\textdom{En}}$ and $\gname_{\textdom{Dis}}$ of these cameras have been created, such that these names are globally known.
\paragraph{World Satisfaction.}
We can now define the proposition $W$ (\emph{world satisfaction}) which ensures that the enabled invariants are actually maintained:
......
......@@ -308,7 +308,7 @@ Proof. intros. rewrite /MaybeFrame /=. apply: sep_elim_r. Qed.
The reason for this is that if given an evar, these typeclasses
would typically try to instantiate this evar with some arbitrary
logical constructs such as emp or True. Therefore, we use an Hint
logical constructs such as emp or True. Therefore, we use a Hint
Mode to disable all the instances that would have this behavior. *)
Class MakeEmbed {PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP) (Q : PROP') :=
make_embed : P Q.
......
Supports Markdown
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