diff --git a/docs/derived.tex b/docs/derived.tex
index 2e92cb831ffa9b9b87b904e36addad977326ec6e..3092ecdd5186e9aa31c20ff5693be7875821c992 100644
--- a/docs/derived.tex
+++ b/docs/derived.tex
@@ -9,19 +9,18 @@
\ralf{Sync this with Coq.}
Hoare triples and view shifts are syntactic sugar for weakest (liberal) preconditions and primitive view shifts, respectively:
-\[
-\hoare{\prop}{\expr}{\Ret\val.\propB}[\mask] \eqdef \always{(\prop \Ra \dynA{\expr}{\lambda\Ret\val.\propB}{\mask})}
-\qquad\qquad
-\begin{aligned}
-\prop \vs[\mask_1][\mask_2] \propB &\eqdef \always{(\prop \Ra \pvsA{\propB}{\mask_1}{\mask_2})} \\
-\prop \vsE[\mask_1][\mask_2] \propB &\eqdef \prop \vs[\mask_1][\mask_2] \propB \land \propB \vs[\mask2][\mask_1] \prop
-\end{aligned}
-\]
+% \[
+% \hoare{\prop}{\expr}{\Ret\val.\propB}[\mask] \eqdef \always{(\prop \Ra \dynA{\expr}{\lambda\Ret\val.\propB}{\mask})}
+% \qquad\qquad
+% \begin{aligned}
+% \prop \vs[\mask_1][\mask_2] \propB &\eqdef \always{(\prop \Ra \pvsA{\propB}{\mask_1}{\mask_2})} \\
+% \prop \vsE[\mask_1][\mask_2] \propB &\eqdef \prop \vs[\mask_1][\mask_2] \propB \land \propB \vs[\mask2][\mask_1] \prop
+% \end{aligned}
+% \]
We write just one mask for a view shift when $\mask_1 = \mask_2$.
The convention for omitted masks is generous:
An omitted $\mask$ is $\top$ for Hoare triples and $\emptyset$ for view shifts.
-We write $\provesalways$ to denote judgments that can only be extended with a boxed proof context, in contrast to our usual convention of allowing the context to be extended with any assertions.
\paragraph{Hoare triples.}
\begin{mathpar}
@@ -120,12 +119,12 @@ The following are easily derived by unfolding the sugar for Hoare triples and vi
{\All \var. (\prop \vs[\mask_1][\mask_2] \propB)}
{(\Exists \var. \prop) \vs[\mask_1][\mask_2] \propB}
\and
-\inferHB{BoxOut}
- {\always\propB \provesalways \hoare{\prop}{\expr}{\Ret\val.\propC}[\mask]}
+\inferHB{HtBox}
+ {\always\propB \proves \hoare{\prop}{\expr}{\Ret\val.\propC}[\mask]}
{\hoare{\prop \land \always{\propB}}{\expr}{\Ret\val.\propC}[\mask]}
\and
-\inferHB{VSBoxOut}
- {\always\propB \provesalways \prop \vs[\mask_1][\mask_2] \propC}
+\inferHB{VsBox}
+ {\always\propB \proves \prop \vs[\mask_1][\mask_2] \propC}
{\prop \land \always{\propB} \vs[\mask_1][\mask_2] \propC}
\and
\inferH{False}
diff --git a/docs/logic.tex b/docs/logic.tex
index caec709ccc15d20947ab39d9aabe6103b5c001c7..0af9326d88e450de865379cf71528ba0c71e41d4 100644
--- a/docs/logic.tex
+++ b/docs/logic.tex
@@ -115,8 +115,8 @@ Iris syntax is built up from a signature $\Sig$ and a countably infinite set $\t
\ownPhys{\term} \mid
\always\prop \mid
{\later\prop} \mid
- \pvsA{\prop}{\term}{\term} \mid
- \dynA{\term}{\pred}{\term}
+ \pvs[\term][\term] \prop\mid
+ \wpre{\term}{\pred}[\term]
\end{align*}
Recursive predicates must be \emph{guarded}: in $\MU \var. \pred$, the variable $\var$ can only appear under the later $\later$ modality.
@@ -263,7 +263,7 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $
\vctx \proves \wtt{\mask}{\textsort{InvMask}} \and
\vctx \proves \wtt{\mask'}{\textsort{InvMask}}
}{
- \vctx \proves \wtt{\pvsA{\prop}{\mask}{\mask'}}{\Prop}
+ \vctx \proves \wtt{\pvs[\mask][\mask'] \prop}{\Prop}
}
\and
\infer{
@@ -271,7 +271,7 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $
\vctx \proves \wtt{\pred}{\textsort{Val} \to \Prop} \and
\vctx \proves \wtt{\mask}{\textsort{InvMask}}
}{
- \vctx \proves \wtt{\dynA{\expr}{\pred}{\mask}}{\Prop}
+ \vctx \proves \wtt{\wpre{\expr}{\pred}[\mask]}{\Prop}
}
\end{mathparpagebreakable}
@@ -288,6 +288,7 @@ This is a \emph{meta-level} assertions about propositions, defined by the follow
The judgment $\vctx \mid \pfctx \proves \prop$ says that with free variables $\vctx$, proposition $\prop$ holds whenever all assumptions $\pfctx$ hold.
We implicitly assume that an arbitrary variable context, $\vctx$, is added to every constituent of the rules.
+Furthermore, an arbitrary \emph{boxed} assertion context $\always\pfctx$ may be added to every constituent.
Axioms $\prop \Ra \propB$ stand for judgments $\vctx \mid \cdot \proves \prop \Ra \propB$ with no assumptions.
(Bi-implications are analogous.)
@@ -500,17 +501,17 @@ This is entirely standard.
\subsection{Adequacy}
-~\\\ralf{Check if this is still accurate. Port to weakest-pre.}
The adequacy statement reads as follows:
\begin{align*}
- &\All \mask, \expr, \val, \pred, i, \state, \state', \tpool'.
- \\&( \proves \hoare{\ownPhys\state}{\expr}{x.\; \pred(x)}[\mask]) \implies
- \\&\cfg{\state}{[i \mapsto \expr]} \step^\ast
- \cfg{\state'}{[i \mapsto \val] \uplus \tpool'} \implies
+ &\All \mask, \expr, \val, \pred, i, \state, \melt, \state', \tpool'.
+ \\&(\All n. \melt \in \mval_n) \Ra
+ \\&( \ownPhys\state * \ownGGhost\melt \proves \wpre{\expr}{x.\; \pred(x)}[\mask]) \Ra
+ \\&\cfg{\state}{[\expr]} \step^\ast
+ \cfg{\state'}{[\val] \dplus \tpool'} \Ra
\\&\pred(\val)
\end{align*}
-where $\pred$ can mention neither resources nor invariants.
+where $\pred$ is a \emph{meta-level} predicate over values, \ie it can mention neither resources nor invariants.
% RJ: If we want this section back, we should port it to primitive view shifts and prove it in Coq.
diff --git a/docs/setup.tex b/docs/setup.tex
index 470eae4a9d541e4f56b147ca2f37a7df72c1aa59..404dc0c0c353c9eb040ff77179245b50ed8a186a 100644
--- a/docs/setup.tex
+++ b/docs/setup.tex
@@ -318,7 +318,6 @@
\def\Lam #1.{\lambda #1.\spac}%
\newcommand{\proves}{\vdash}
-\newcommand{\provesalways}{\vdash_{\!\!\boxempty}}
\newcommand{\wand}{\;{{\mbox{---}}\!\!{*}}\;}
@@ -327,12 +326,8 @@
\newcommand{\gmapsto}{\hookrightarrow}%
\newcommand{\fgmapsto}[1][\mathrm{-}]{\xhookrightarrow{#1}}%
-\newcommand{\dyn}[2]{\textlog{wp}({#1}, {#2})}
-\newcommand{\adyn}[2]{{#1}\;\llparenthesis{#2}\rrparenthesis}
-\newcommand{\dynpred}[2]{\textdom{wp}({#1}, {#2})}
-\newcommand{\dynA}[3]{\textlog{wp}_{#3}({#1}, {#2})}
-\newcommand{\pvs}[1]{\textlog{vs}({#1})}
-\newcommand{\pvsA}[3]{\textlog{vs}_{#2}^{#3}({#1})}
+\NewDocumentCommand\wpre{m m o}%
+ {{#1} \spac \{#2\}_{#3}}
\newcommand{\later}{\mathord{\triangleright}}
\newcommand{\always}{\Box{}}
@@ -369,6 +364,8 @@
\NewDocumentCommand \vsL {O{} O{}} {\vsGen[#1]{\Lleftarrow}[#2]}
\NewDocumentCommand \vsE {O{} O{}} %
{\vsGen[#1]{\Lleftarrow\!\!\!\Rrightarrow}[#2]}
+\NewDocumentCommand \pvs {O{} O{}} {\mathord{\vsGen[#1]{{\mid\kern-0.4ex\Rrightarrow}}[#2]}}
+
%% Hoare Triples
\newcommand*{\hoaresizebox}[1]{%
diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v
index 14c93e4d8d9a1f5809accff70b02a8429ef8733b..b824d58f4b3244c415bed1f7e56b7af06b93b45b 100644
--- a/program_logic/adequacy.v
+++ b/program_logic/adequacy.v
@@ -54,8 +54,8 @@ Proof.
apply uPred_weaken with (k + n) r2; eauto using cmra_included_l. }
by rewrite -Permutation_middle /= big_op_app.
Qed.
-Lemma ht_adequacy_steps P Φ k n e1 t2 σ1 σ2 r1 :
- {{ P }} e1 {{ Φ }} →
+Lemma wp_adequacy_steps P Φ k n e1 t2 σ1 σ2 r1 :
+ P ⊑ #> e1 {{ Φ }} →
nsteps step k ([e1],σ1) (t2,σ2) →
1 < n → wsat (k + n) ⊤ σ1 r1 →
P (k + n) r1 →
@@ -64,65 +64,89 @@ Proof.
intros Hht ????; apply (nsteps_wptp [Φ] k n ([e1],σ1) (t2,σ2) [r1]);
rewrite /big_op ?right_id; auto.
constructor; last constructor.
- move: Hht; rewrite /ht; uPred.unseal=> Hht.
- apply Hht with (k + n) r1; by eauto using cmra_included_unit.
+ apply Hht; by eauto using cmra_included_unit.
Qed.
-Lemma ht_adequacy_own Φ e1 t2 σ1 m σ2 :
+
+Lemma wp_adequacy_own Φ e1 t2 σ1 m σ2 :
✓ m →
- {{ ownP σ1 ★ ownG m }} e1 {{ Φ }} →
+ (ownP σ1 ★ ownG m) ⊑ #> e1 {{ Φ }} →
rtc step ([e1],σ1) (t2,σ2) →
∃ rs2 Φs', wptp 2 t2 (Φ :: Φs') rs2 ∧ wsat 2 ⊤ σ2 (big_op rs2).
Proof.
intros Hv ? [k ?]%rtc_nsteps.
- eapply ht_adequacy_steps with (r1 := (Res ∅ (Excl σ1) (Some m))); eauto; [|].
+ eapply wp_adequacy_steps with (r1 := (Res ∅ (Excl σ1) (Some m))); eauto; [|].
{ by rewrite Nat.add_comm; apply wsat_init, cmra_valid_validN. }
uPred.unseal; exists (Res ∅ (Excl σ1) ∅), (Res ∅ ∅ (Some m)); split_and?.
- by rewrite Res_op ?left_id ?right_id.
- rewrite /ownP; uPred.unseal; rewrite /uPred_holds //=.
- by apply ownG_spec.
Qed.
-Theorem ht_adequacy_result E φ e v t2 σ1 m σ2 :
+
+Theorem wp_adequacy_result E φ e v t2 σ1 m σ2 :
✓ m →
- {{ ownP σ1 ★ ownG m }} e @ E {{ λ v', ■φ v' }} →
+ (ownP σ1 ★ ownG m) ⊑ #> e @ E {{ λ v', ■φ v' }} →
rtc step ([e], σ1) (of_val v :: t2, σ2) →
φ v.
Proof.
intros Hv ? Hs.
- destruct (ht_adequacy_own (λ v', ■φ v')%I e (of_val v :: t2) σ1 m σ2)
+ destruct (wp_adequacy_own (λ v', ■φ v')%I e (of_val v :: t2) σ1 m σ2)
as (rs2&Qs&Hwptp&?); auto.
- { by rewrite -(ht_mask_weaken E ⊤). }
+ { by rewrite -(wp_mask_weaken E ⊤). }
inversion Hwptp as [|?? r ?? rs Hwp _]; clear Hwptp; subst.
move: Hwp. rewrite wp_eq. uPred.unseal=> /wp_value_inv Hwp.
rewrite pvs_eq in Hwp.
destruct (Hwp (big_op rs) 2 ∅ σ2) as [r' []]; rewrite ?right_id_L; auto.
Qed.
-Lemma ht_adequacy_reducible E Φ e1 e2 t2 σ1 m σ2 :
+
+Lemma ht_adequacy_result E φ e v t2 σ1 m σ2 :
✓ m →
- {{ ownP σ1 ★ ownG m }} e1 @ E {{ Φ }} →
+ {{ ownP σ1 ★ ownG m }} e @ E {{ λ v', ■φ v' }} →
+ rtc step ([e], σ1) (of_val v :: t2, σ2) →
+ φ v.
+Proof.
+ intros ? Hht. eapply wp_adequacy_result with (E:=E); first done.
+ move:Hht. by rewrite /ht uPred.always_elim=>/uPred.impl_entails.
+Qed.
+
+Lemma wp_adequacy_reducible E Φ e1 e2 t2 σ1 m σ2 :
+ ✓ m →
+ (ownP σ1 ★ ownG m) ⊑ #> e1 @ E {{ Φ }} →
rtc step ([e1], σ1) (t2, σ2) →
e2 ∈ t2 → to_val e2 = None → reducible e2 σ2.
Proof.
intros Hv ? Hs [i ?]%elem_of_list_lookup He.
- destruct (ht_adequacy_own Φ e1 t2 σ1 m σ2) as (rs2&Φs&?&?); auto.
- { by rewrite -(ht_mask_weaken E ⊤). }
+ destruct (wp_adequacy_own Φ e1 t2 σ1 m σ2) as (rs2&Φs&?&?); auto.
+ { by rewrite -(wp_mask_weaken E ⊤). }
destruct (Forall3_lookup_l (λ e Φ r, wp ⊤ e Φ 2 r) t2
(Φ :: Φs) rs2 i e2) as (Φ'&r2&?&?&Hwp); auto.
destruct (wp_step_inv ⊤ ∅ Φ' e2 1 2 σ2 r2 (big_op (delete i rs2)));
rewrite ?right_id_L ?big_op_delete; auto.
by rewrite -wp_eq.
Qed.
-Theorem ht_adequacy_safe E Φ e1 t2 σ1 m σ2 :
+
+Theorem wp_adequacy_safe E Φ e1 t2 σ1 m σ2 :
✓ m →
- {{ ownP σ1 ★ ownG m }} e1 @ E {{ Φ }} →
+ (ownP σ1 ★ ownG m) ⊑ #> e1 @ E {{ Φ }} →
rtc step ([e1], σ1) (t2, σ2) →
Forall (λ e, is_Some (to_val e)) t2 ∨ ∃ t3 σ3, step (t2, σ2) (t3, σ3).
Proof.
intros.
destruct (decide (Forall (λ e, is_Some (to_val e)) t2)) as [|Ht2]; [by left|].
apply (not_Forall_Exists _), Exists_exists in Ht2; destruct Ht2 as (e2&?&He2).
- destruct (ht_adequacy_reducible E Φ e1 e2 t2 σ1 m σ2) as (e3&σ3&ef&?);
+ destruct (wp_adequacy_reducible E Φ e1 e2 t2 σ1 m σ2) as (e3&σ3&ef&?);
rewrite ?eq_None_not_Some; auto.
destruct (elem_of_list_split t2 e2) as (t2'&t2''&->); auto.
right; exists (t2' ++ e3 :: t2'' ++ option_list ef), σ3; econstructor; eauto.
Qed.
+
+Lemma ht_adequacy_safe E Φ e1 t2 σ1 m σ2 :
+ ✓ m →
+ {{ ownP σ1 ★ ownG m }} e1 @ E {{ Φ }} →
+ rtc step ([e1], σ1) (t2, σ2) →
+ Forall (λ e, is_Some (to_val e)) t2 ∨ ∃ t3 σ3, step (t2, σ2) (t3, σ3).
+Proof.
+ intros ? Hht. eapply wp_adequacy_safe with (E:=E) (Φ:=Φ); first done.
+ move:Hht. by rewrite /ht uPred.always_elim=>/uPred.impl_entails.
+Qed.
+
End adequacy.