From 6ba36cd6f5f089eadbf5e8d06bcdc0eb8c633c79 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 18 Mar 2020 16:14:46 +0100
Subject: [PATCH] mention that masks in Coq are a bit different than on paper

---
 tex/program-logic.tex | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/tex/program-logic.tex b/tex/program-logic.tex
index 338acd4ca..73ced65c1 100644
--- a/tex/program-logic.tex
+++ b/tex/program-logic.tex
@@ -47,6 +47,9 @@ The following proposition states that an invariant with name $\iname$ exists and
 Next, we define \emph{fancy updates}, which are essentially the same as the basic updates of the base logic ($\Sref{sec:base-logic}$), except that they also have access to world satisfaction and can enable and disable invariants:
 \[ \pvs[\mask_1][\mask_2] \prop \eqdef W * \ownGhost{\gname_{\textmon{En}}}{\mask_1} \wand \upd\diamond (W * \ownGhost{\gname_{\textmon{En}}}{\mask_2} * \prop) \]
 Here, $\mask_1$ and $\mask_2$ are the \emph{masks} of the view update, defining which invariants have to be (at least!) available before and after the update.
+Masks are sets of natural numbers, \ie they are subsets of $\mathbb{N}$.%
+\footnote{Actually, in the Coq development masks are restricted to a class of sets of natural numbers that contains all finite sets and is closed under union, intersection, difference and complement.
+The restriction is necessary for engineering reasons to still obtain representation independence: two masks should be \emph{definitionally} equal iff they contain the same invariant names.}
 We use $\top$ as symbol for the largest possible mask, $\nat$, and $\bot$ for the smallest possible mask $\emptyset$.
 We will write $\pvs[\mask] \prop$ for $\pvs[\mask][\mask]\prop$.
 %
-- 
GitLab