diff --git a/CHANGELOG.md b/CHANGELOG.md
index 9a6df74fba6060b839082cb6790f22eef3a20e42..ed02034fc608e38fe9db7c5de6c3d573d739beb5 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -11,7 +11,7 @@ Changes in and extensions of the theory:
   the quantification over the next states and the later modality. This makes it
   possible to prove more powerful lifting lemmas: The new versions feature an
   "update that takes a step".
-* [#] Weaken the semantics of CAS in heap_lang to be efficiently implementable:
+* Weaken the semantics of CAS in heap_lang to be efficiently implementable:
   CAS may only be used to compare "unboxed" values that can be represented in a
   single machine word.
 * Add weakest preconditions for total program correctness.
@@ -19,7 +19,7 @@ Changes in and extensions of the theory:
   longer considered experimental.
 * The adequacy statement for weakest preconditions now also involves the
   final state.
-* [#] Add the notion of an "observation" to the language interface, so that
+* Add the notion of an "observation" to the language interface, so that
   every reduction step can optionally be marked with an event, and an execution
   trace has a matching list of events.  Change WP so that it is told the entire
   future trace of observations from the beginning.  Use this in heap_lang to
@@ -29,9 +29,9 @@ Changes in and extensions of the theory:
   functions.
 * Add atomic updates and logically atomic triples, including tactic support.
   See `heap_lang/lib/increment.v` for an example.
-* [#] heap_lang now uses right-to-left evaluation order. This makes it
+* heap_lang now uses right-to-left evaluation order. This makes it
   significantly easier to write specifications of curried functions.
-* [#] heap_lang values are now injected in heap_lang expressions via a specific
+* heap_lang values are now injected in heap_lang expressions via a specific
   constructor of the expr inductive type. This simplifies much the tactical
   infrastructure around the language. In particular, this allow us to get rid
   the reflection mechanism that was needed for proving closedness, atomicity and
diff --git a/docs/iris.sty b/docs/iris.sty
index f54bb99b6ff6a543d290f0a132acb63d8d94f125..702c2203b35b9f4d4549ac15c48829e4dbcbf7d2 100644
--- a/docs/iris.sty
+++ b/docs/iris.sty
@@ -7,8 +7,8 @@
 \RequirePackage{array}
 \RequirePackage{dashbox}
 \RequirePackage{tensor}
+\RequirePackage{xifthen}
 \RequirePackage{xparse}
-\RequirePackage{xstring}
 \RequirePackage{mathtools}
 
 \usetikzlibrary{shapes}
@@ -23,7 +23,7 @@
 
 \newcommand{\nat}{\mathbb{N}}
 
-\newcommand*{\Sep}{\scalerel*{\ast}{\sum}}
+\newcommand*{\Sep}[1][]{\scalerel*{\ast}{\sum}\ifthenelse{\isempty{#1}}{}{_{#1}\;}}
 \newcommand*{\disj}[1][]{\mathrel{\#_{#1}}}
 \newcommand\pord{\sqsubseteq}
 
@@ -141,12 +141,6 @@
 \newcommand{\iPreProp}{\textdom{iPreProp}}
 \newcommand{\Wld}{\textdom{Wld}}
 \newcommand{\Res}{\textdom{Res}}
-\newcommand{\State}{\textdom{State}}
-\newcommand{\Val}{\textdom{Val}}
-\newcommand{\Loc}{\textdom{Loc}}
-\newcommand{\Expr}{\textdom{Expr}}
-\newcommand{\Var}{\textdom{Var}}
-\newcommand{\ThreadPool}{\textdom{ThreadPool}}
 
 % List
 \newcommand{\List}{\ensuremath{\textdom{List}}}
@@ -381,11 +375,21 @@
 \newcommand{\val}{v}
 \newcommand{\valB}{w}
 \newcommand{\state}{\sigma}
-\newcommand{\step}{\ra_{\mathsf{t}}}
-\newcommand{\hstep}{\ra_{\mathsf{h}}}
-\newcommand{\tpstep}{\ra_{\mathsf{tp}}}
+\newcommand{\step}[1][]{\xrightarrow{{#1}}_{\mathsf{t}}}
+\newcommand{\hstep}[1][]{\xrightarrow{{#1}}_{\mathsf{h}}}
+\newcommand{\tpstep}[1][]{\xrightarrow{{#1}}_{\mathsf{tp}}}
+\newcommand{\tpsteps}[1][]{\xrightarrow{{#1}}\mathrel{\vphantom{\to}^{*}_{\mathsf{tp}}}}
 \newcommand{\lctx}{K}
 \newcommand{\Lctx}{\textdom{Ctx}}
+\newcommand{\obs}{\kappa}
+
+\newcommand{\State}{\textdom{State}}
+\newcommand{\Val}{\textdom{Val}}
+\newcommand{\Loc}{\textdom{Loc}}
+\newcommand{\Expr}{\textdom{Expr}}
+\newcommand{\Var}{\textdom{Var}}
+\newcommand{\Obs}{\textdom{Obs}}
+\newcommand{\ThreadPool}{\textdom{ThreadPool}}
 
 \newcommand{\toval}{\mathrm{expr\any to\any val}}
 \newcommand{\ofval}{\mathrm{val\any to\any expr}}
diff --git a/docs/language.tex b/docs/language.tex
index 5e59c5b3e9723dea26ac2e886e864feeb1c038fc..8c48bca9b797cbb41429b63387795fefc9d5a434 100644
--- a/docs/language.tex
+++ b/docs/language.tex
@@ -1,30 +1,30 @@
 \section{Language}
 \label{sec:language}
 
-A \emph{language} $\Lang$ consists of a set \Expr{} of \emph{expressions} (metavariable $\expr$), a set \Val{} of \emph{values} (metavariable $\val$), and a nonempty set $\State$ of \emph{states} (metavariable $\state$) such that
+A \emph{language} $\Lang$ consists of a set \Expr{} of \emph{expressions} (metavariable $\expr$), a set \Val{} of \emph{values} (metavariable $\val$), a set $\Obs$ of \emph{observations} and a set $\State$ of \emph{states} (metavariable $\state$) such that
 \begin{itemize}[itemsep=0pt]
 \item There exist functions $\ofval : \Val \to \Expr$ and $\toval : \Expr \pfn \Val$ (notice the latter is partial), such that
 \begin{mathpar}
 {\All \expr, \val. \toval(\expr) = \val \Ra \ofval(\val) = \expr} \and
 {\All\val. \toval(\ofval(\val)) = \val} 
 \end{mathpar}
-\item There exists a \emph{primitive reduction relation} \[(-,- \step -,-,-) \subseteq \Expr \times \State \times \Expr \times \State \times \List(\Expr)\]
-  A reduction $\expr_1, \state_1 \step \expr_2, \state_2, \overline\expr$ indicates that, when $\expr_1$ reduces to $\expr_2$, the new threads in the list $\overline\expr$ is forked off.
-  We will write $\expr_1, \state_1 \step \expr_2, \state_2$ for $\expr_1, \state_1 \step \expr_2, \state_2, ()$, \ie when no threads are forked off. \\
+\item There exists a \emph{primitive reduction relation} \[(-,- \;\step[-]\; -,-,-) \subseteq (\Expr \times \State) \times \List(\Obs) \times (\Expr \times \State \times \List(\Expr))\]
+  A reduction $\expr_1, \state_1 \step[\vec\obs] \expr_2, \state_2, \vec\expr$ indicates that, when $\expr_1$ in state $\state_1$ reduces to $\expr_2$ with new state $\state_2$, the new threads in the list $\vec\expr$ is forked off and the observations $\vec\obs$ are made.
+  We will write $\expr_1, \state_1 \step \expr_2, \state_2$ for $\expr_1, \state_1 \step[()] \expr_2, \state_2, ()$, \ie when no threads are forked off and no observations are made. \\
 \item All values are stuck:
 \[ \expr, \_ \step  \_, \_, \_ \Ra \toval(\expr) = \bot \]
 \end{itemize}
 
 \begin{defn}
   An expression $\expr$ and state $\state$ are \emph{reducible} (written $\red(\expr, \state)$) if
-  \[ \Exists \expr_2, \state_2, \vec\expr. \expr,\state \step \expr_2,\state_2,\vec\expr \]
+  \[ \Exists \vec\obs, \expr_2, \state_2, \vec\expr. \expr,\state \step[\vec\obs] \expr_2,\state_2,\vec\expr \]
 \end{defn}
 
 \begin{defn}
   An expression $\expr$ is \emph{weakly atomic} if it reduces in one step to something irreducible:
-  \[ \atomic(\expr) \eqdef \All\state_1, \expr_2, \state_2, \vec\expr. \expr, \state_1 \step \expr_2, \state_2, \vec\expr \Ra \lnot \red(\expr_2, \state_2) \]
+  \[ \atomic(\expr) \eqdef \All\state_1, \vec\obs, \expr_2, \state_2, \vec\expr. \expr, \state_1 \step[\vec\obs] \expr_2, \state_2, \vec\expr \Ra \lnot \red(\expr_2, \state_2) \]
   It is \emph{strongly atomic} if it reduces in one step to a value:
-  \[ \stronglyAtomic(\expr) \eqdef \All\state_1, \expr_2, \state_2, \vec\expr. \expr, \state_1 \step \expr_2, \state_2, \vec\expr \Ra \toval(\expr_2) \neq \bot \]
+  \[ \stronglyAtomic(\expr) \eqdef \All\state_1, \vec\obs, \expr_2, \state_2, \vec\expr. \expr, \state_1 \step[\vec\obs] \expr_2, \state_2, \vec\expr \Ra \toval(\expr_2) \neq \bot \]
 \end{defn}
 We need two notions of atomicity to accommodate both kinds of weakest preconditions that we will define later:
 If the weakest precondition ensures that the program cannot get stuck, weak atomicity is sufficient.
@@ -34,11 +34,14 @@ Otherwise, we need strong atomicity.
   A function $\lctx : \Expr \to \Expr$ is a \emph{context} if the following conditions are satisfied:
   \begin{enumerate}[itemsep=0pt]
   \item $\lctx$ does not turn non-values into values:\\
-    $\All\expr. \toval(\expr) = \bot \Ra \toval(\lctx(\expr)) = \bot $
+    $$\All\expr. \toval(\expr) = \bot \Ra \toval(\lctx(\expr)) = \bot $$
   \item One can perform reductions below $\lctx$:\\
-    $\All \expr_1, \state_1, \expr_2, \state_2, \vec\expr. \expr_1, \state_1 \step \expr_2,\state_2,\vec\expr \Ra \lctx(\expr_1), \state_1 \step \lctx(\expr_2),\state_2,\vec\expr $
+    $$\All \expr_1, \state_1, \vec\obs, \expr_2, \state_2, \vec\expr. \expr_1, \state_1 \step[\vec\obs] \expr_2,\state_2,\vec\expr \Ra \lctx(\expr_1), \state_1 \step[\vec\obs] \lctx(\expr_2),\state_2,\vec\expr $$
   \item Reductions stay below $\lctx$ until there is a value in the hole:\\
-    $\All \expr_1', \state_1, \expr_2, \state_2, \vec\expr. \toval(\expr_1') = \bot \land \lctx(\expr_1'), \state_1 \step \expr_2,\state_2,\vec\expr \Ra \Exists\expr_2'. \expr_2 = \lctx(\expr_2') \land \expr_1', \state_1 \step \expr_2',\state_2,\vec\expr $
+    \begin{align*}
+      &\All \expr_1', \state_1, \vec\obs, \expr_2, \state_2, \vec\expr. \toval(\expr_1') = \bot \land \lctx(\expr_1'), \state_1 \step[\vec\obs] \expr_2,\state_2,\vec\expr \Ra {}\\
+      &\qquad \Exists\expr_2'. \expr_2 = \lctx(\expr_2') \land \expr_1', \state_1 \step[\vec\obs] \expr_2',\state_2,\vec\expr 
+    \end{align*}
   \end{enumerate}
 \end{defn}
 
@@ -51,15 +54,17 @@ For any language $\Lang$, we define the corresponding thread-pool semantics.
 	\tpool \in \ThreadPool \eqdef \List(\Expr)
 \]
 
-\judgment[Machine reduction]{\cfg{\tpool}{\state} \step
+\judgment[Machine reduction]{\cfg{\tpool}{\state} \tpstep[\vec\obs]
   \cfg{\tpool'}{\state'}}
 \begin{mathpar}
 \infer
-  {\expr_1, \state_1 \step \expr_2, \state_2, \vec\expr}
-  {\cfg{\tpool \dplus [\expr_1] \dplus \tpool'}{\state_1} \step
+  {\expr_1, \state_1 \step[\vec\obs] \expr_2, \state_2, \vec\expr}
+  {\cfg{\tpool \dplus [\expr_1] \dplus \tpool'}{\state_1} \tpstep[\vec\obs]
      \cfg{\tpool \dplus [\expr_2] \dplus \tpool' \dplus \vec\expr}{\state_2}}
 \end{mathpar}
 
+We use $\tpsteps[-]$ for the reflexive transitive closure of $\tpstep[-]$, as usual concatenating the lists of observations of the individual steps.
+
 
 %%% Local Variables:
 %%% mode: latex
diff --git a/docs/program-logic.tex b/docs/program-logic.tex
index 0b6a79b1e48b4ab502a2fc360eb8e7dc67ba9560..7f1c6a59fe8cb1505b1704506b801938d9cb15b0 100644
--- a/docs/program-logic.tex
+++ b/docs/program-logic.tex
@@ -156,17 +156,17 @@ Finally, we can define the core piece of the program logic, the proposition that
 
 \paragraph{Defining weakest precondition.}
 We assume that everything making up the definition of the language, \ie values, expressions, states, the conversion functions, reduction relation and all their properties, are suitably reflected into the logic (\ie they are part of the signature $\Sig$).
-We further assume (as a parameter) a predicate $\stateinterp : \State \times \mathbb N \to \iProp$ that interprets the machine state as an Iris proposition, and a predicate $\pred_F: \Val \to \iProp$ that serves as postcondition for forked-of threads.
-The state interpretation can depend on the current physical state as well as the total number of \emph{forked} threads (that is one less that the total number of threads).
+We further assume (as a parameter) a predicate $\stateinterp : \State \times \List(\Obs) \times \mathbb N \to \iProp$ that interprets the machine state as an Iris proposition, and a predicate $\pred_F: \Val \to \iProp$ that serves as postcondition for forked-of threads.
+The state interpretation can depend on the current physical state, the list of \emph{future} observations as well as the total number of \emph{forked} threads (that is one less that the total number of threads).
 This can be instantiated, for example, with ownership of an authoritative RA to tie the physical state to fragments that are used for user-level proofs.
 Finally, weakest precondition takes a parameter $\stuckness \in \set{\NotStuck, \MaybeStuck}$ indicating whether program execution is allowed to get stuck.
 
 \begin{align*}
   \textdom{wp}(\stateinterp, \pred_F, \stuckness) \eqdef{}& \MU \textdom{wp\any rec}. \Lam \mask, \expr, \pred. \\
         & (\Exists\val. \toval(\expr) = \val \land \pvs[\mask] \pred(\val)) \lor {}\\
-        & \Bigl(\toval(\expr) = \bot \land \All \state, n. \stateinterp(\state, n) \vsW[\mask][\emptyset] {}\\
-        &\qquad (s = \NotStuck \Ra \red(\expr, \state)) * \All \expr', \state', \vec\expr. (\expr, \state \step \expr', \state', \vec\expr) \vsW[\emptyset][\emptyset]\later\pvs[\emptyset][\mask] {}\\
-        &\qquad\qquad \stateinterp(\state', n + |\vec\expr|) * \textdom{wp\any rec}(\mask, \expr', \pred) * \Sep_{\expr'' \in \vec\expr} \textdom{wp\any rec}(\top, \expr'', \pred_F)\Bigr) \\
+        & \Bigl(\toval(\expr) = \bot \land \All \state, \vec\obs, \vec\obs', n. \stateinterp(\state, \vec\obs \dplus \vec\obs', n) \vsW[\mask][\emptyset] {}\\
+        &\qquad (s = \NotStuck \Ra \red(\expr, \state)) * \All \expr', \state', \vec\expr. (\expr, \state \step[\vec\obs] \expr', \state', \vec\expr) \vsW[\emptyset][\emptyset]\later\pvs[\emptyset][\mask] {}\\
+        &\qquad\qquad \stateinterp(\state', \vec\obs', n + |\vec\expr|) * \textdom{wp\any rec}(\mask, \expr', \pred) * \Sep[\expr'' \in \vec\expr] \textdom{wp\any rec}(\top, \expr'', \pred_F)\Bigr) \\
   \wpre[\stateinterp;\pred_F]\expr[\stuckness;\mask]{\Ret\val. \prop} \eqdef{}& \textdom{wp}(\stateinterp,\pred_F,\stuckness)(\mask, \expr, \Lam\val.\prop)
 \end{align*}
 The $\stateinterp$ and $\pred_F$ will always be set by the context; typically, when instantiating Iris with a language, we also pick the corresponding state interpretation $\stateinterp$ and fork-postcondition $\pred_F$.
@@ -209,13 +209,15 @@ The following rules can all be derived:
 \end{mathpar}
 
 We will also want a rule that connect weakest preconditions to the operational semantics of the language.
+This basically just copies the second branch (the non-value case) of the definition of weakest preconditions.
+
 \begin{mathpar}
   \infer[wp-lift-step]
   {\toval(\expr_1) = \bot}
   { {\begin{inbox} % for some crazy reason, LaTeX is actually sensitive to the space between the "{ {" here and the "} }" below...
-        ~~\All \state_1,n. \stateinterp(\state_1,n) \vsW[\mask][\emptyset] (\stuckness = \NotStuck \Ra \red(\expr_1,\state_1)) * {}\\
-        \qquad~~ \All \expr_2, \state_2, \vec\expr.  (\expr_1, \state_1 \step \expr_2, \state_2, \vec\expr)  \vsW[\emptyset][\emptyset]\later\pvs[\emptyset][\mask]
-        \Bigl(\stateinterp(\state_2,n+|\vec\expr|) * \wpre[\stateinterp;\pred_F]{\expr_2}[\stuckness;\mask]{\Ret\var.\prop} * \Sep_{\expr_\f \in \vec\expr} \wpre[\stateinterp\pred_F]{\expr_\f}[\stuckness;\top]{\pred_F}\Bigr)  {}\\
+        ~~\All \state_1,\vec\obs,\vec\obs',n. \stateinterp(\state_1,\vec\obs \dplus \vec\obs', n) \vsW[\mask][\emptyset] (\stuckness = \NotStuck \Ra \red(\expr_1,\state_1)) * {}\\
+        \qquad~ \All \expr_2, \state_2, \vec\expr.  (\expr_1, \state_1 \step[\vec\obs] \expr_2, \state_2, \vec\expr)  \vsW[\emptyset][\emptyset]\later\pvs[\emptyset][\mask] {}\\
+        \qquad\qquad\Bigl(\stateinterp(\state_2,\vec\obs',n+|\vec\expr|) * \wpre[\stateinterp;\pred_F]{\expr_2}[\stuckness;\mask]{\Ret\var.\prop} * \Sep[\expr_\f \in \vec\expr] \wpre[\stateinterp\pred_F]{\expr_\f}[\stuckness;\top]{\pred_F}\Bigr)  {}\\
         \proves \wpre[\stateinterp\pred_F]{\expr_1}[\stuckness;\mask]{\Ret\var.\prop}
       \end{inbox}} }
 \end{mathpar}
@@ -253,7 +255,7 @@ There are two properties we are looking for: First of all, the postcondition sho
 Second, a proof of a weakest precondition with any postcondition should imply that the program is \emph{safe}, \ie that it does not get stuck.
 
 \begin{defn}[Adequacy]
-  A program $\expr$ in some initial state $\state$ is \emph{adequate} for stuckness  $\stuckness$ and a set $V \subseteq \Val \times \State$ of legal return-value-final-state combinations (written $\expr, \state \vDash_\stuckness V$) if for all $\tpool', \state'$ such that $([\expr], \state) \tpstep^\ast (\tpool', \state')$ we have
+  A program $\expr$ in some initial state $\state$ is \emph{adequate} for stuckness  $\stuckness$ and a set $V \subseteq \Val \times \State$ of legal return-value-final-state combinations (written $\expr, \state \vDash_\stuckness V$) if for all $\tpool', \state'$ such that $([\expr], \state) \tpsteps[\vec\obs] (\tpool', \state')$ we have
 \begin{enumerate}
 \item Safety: If $\stuckness = \NotStuck$, then for any $\expr' \in \tpool'$ we have that either $\expr'$ is a
   value, or \(\red(\expr'_i,\state')\):
@@ -274,19 +276,20 @@ Furthermore, we assume that the \emph{interpretation} $\Sem\pred$ of $\pred$ ref
 The signature can of course state arbitrary additional properties of $\pred$, as long as they are proven sound.
 The adequacy statement now reads as follows:
 \begin{align*}
- &\All \mask, \expr, \val, \state.
- \\&( \TRUE \proves \pvs[\mask] \Exists \stateinterp, \pred_F. \stateinterp(\state,0) * \wpre[\stateinterp;\pred_F]{\expr}[\stuckness;\mask]{x.\; \All \state, m. \stateinterp(\state', m) \vsW[\top][\emptyset] \pred(x,\state')}) \Ra
+ &\All \mask, \expr, \state.
+ \\&( \TRUE \proves \All\vec\obs. \pvs[\mask] \Exists \stateinterp, \pred_F. \stateinterp(\state,\vec\obs,0) * \wpre[\stateinterp;\pred_F]{\expr}[\stuckness;\mask]{x.\; \All \state, m. \stateinterp(\state', (), m) \vsW[\top][\emptyset] \pred(x,\state')}) \Ra
  \\&\expr, \state \vDash_\stuckness V
 \end{align*}
 Notice that the state invariant $S$ used by the weakest precondition is chosen \emph{after} doing a fancy update, which allows it to depend on the names of ghost variables that are picked in that initial fancy update.
+Also, notice that the proof of $\expr$ must be performed with a universally quantified list of observations $\vec\obs$, but the \emph{entire} list is known to the proof from the beginning.
 
 The following variant of adequacy also allows exploiting the second parameter of $\stateinterp$, the number of threads, but only applies when \emph{all} threads have reduced to a value:
 \begin{align*}
- &\All \mask, \expr, \val, \state.
- \\&( \TRUE \proves \pvs[\mask] \Exists \stateinterp, \pred_F. \stateinterp(\state,0) * \wpre[\stateinterp;\pred_F]{\expr}[\stuckness;\mask]%
-      {x.\; \stateinterp(\state',|\vec\val|) * \Sep_{y \in \vec\val} \pred_F(y) \vsW[\top][\emptyset]  \pred(x)}) \Ra
- \\&([\expr], \state) \tpstep^\ast (\val :: \vec\val, \state') \Ra
- \\&\val \in V
+ &\All \mask, \expr, \state, \vec\obs, \val, \vec\val, \state'.
+ \\&( \TRUE \proves \pvs[\mask] \Exists \stateinterp, \pred_F. \stateinterp(\state,\vec\obs,0) * \wpre[\stateinterp;\pred_F]{\expr}[\stuckness;\mask]%
+      {x.\; \stateinterp(\state',(),|\vec\val|) * \Sep_{y \in \vec\val} \pred_F(y) \vsW[\top][\emptyset]  \pred(x,\state')}) \Ra
+ \\&([\expr], \state) \tpsteps[\vec\obs] (\val :: \vec\val, \state') \Ra
+ \\&(\val,\state') \in V
 \end{align*}
 
 \paragraph{Hoare triples.}