Library while

Require Import ssreflect ssrbool.

While: A Low-level Language

This section corresponds to Appendix A in [Saabas&Uustalu2007].

Our formalization of [Saabas&Uustalu2007] can be instantiated with any While-like language. In this section, we isolate more precisely what we expect from such a language.

Generic definition of then While Language and Hoare logic

Section Lang.

A state is a pair of a store and a mutable memory.

Variable store : Type.
Variable heap : Type.
Let state : Type := (store * heap)%type.

We are given one-step, non-branching instructions:

Variable cmd0 : Type.

One-step, non-branching instructions are given an appropriate operational semantics. We use an option type to model error-states.

Variable exec0 : option state -> cmd0 -> option state -> Prop.
Notation "s '--' c '---->' t" := (exec0 s c t) (at level 74 , no associativity) : lang_scope.
Local Open Scope lang_scope.

Structured commands (if-then-else's and while-loops) are parameterized by a type for boolean expressions.

Variable expr_b : Type.
Variable eval_b : expr_b -> state -> bool.

Using above types, we define the commands of While languages.

Inductive cmd : Type :=
| cmd_cmd0 : cmd0 -> cmd
| seq : cmd -> cmd -> cmd
| ifte : expr_b -> cmd -> cmd -> cmd
| while : expr_b -> cmd -> cmd.
Coercion cmd_cmd0 : cmd0 >-> cmd.
Notation "c ; d" := (seq c d) (at level 81, right associativity) : lang_scope.

We now define the operational semantics of While languages. Structured commands are given the textbook big-step operational semantics.

Reserved Notation "s -- c ---> t" (at level 74, no associativity).
Inductive exec : option state -> cmd -> option state -> Prop :=
| exec_none : forall c, None -- c ---> None
| exec_cmd0 : forall s c s', s -- c ----> s' -> s -- c ---> s'
| exec_seq : forall s s' s'' c d, s -- c ---> s' -> s' -- d ---> s'' -> s -- c ; d ---> s''
| exec_ifte_true : forall s s' t c d, eval_b t s -> Some s -- c ---> s' ->
  Some s -- ifte t c d ---> s'
| exec_ifte_false : forall s s' t c d, ~~ eval_b t s -> Some s -- d ---> s' ->
  Some s -- ifte t c d ---> s'
| exec_while_true : forall s s' s'' t c, eval_b t s -> Some s -- c ---> s' ->
  s' -- while t c ---> s'' -> Some s -- while t c ---> s''
| exec_while_false : forall s t c,
  ~~ eval_b t s -> Some s -- while t c ---> Some s
where "s -- c ---> t" := (exec s c t) : lang_scope.

We now come to the formalization of textbook Hoare logic. Actually, we allow for an extension of Hoare logic with a notion of pointer and mutable memory (or heap for short) known as Separation logic. Assertions are shallow-encoded.

Let assert := store -> heap -> Prop.

Definition TT : assert := fun _ _ => True.
Definition FF : assert := fun _ _ => False.
Definition And (P Q : assert) : assert := fun s h => P s h /\ Q s h.
Definition Or (P Q : assert) : assert := fun s h => P s h \/ Q s h.
Definition Not (P : assert) : assert := fun s h => ~ P s h.
Definition entails (P Q : assert) : Prop := forall s h, P s h -> Q s h.
Notation "P ===> Q" := (entails P Q) (at level 90, no associativity) : lang_scope.
Definition equiv (P Q : assert) : Prop := forall s h, P s h <-> Q s h.
Notation "P <==> Q" := (equiv P Q) (at level 90, no associativity) : lang_scope.

The axioms of Hoare logic are encoded as an inductive type, assuming given Hoare triples for one-step, non-branching instructions.

Variable hoare0 : assert -> cmd0 -> assert -> Prop.

Reserved Notation "{[ P ]} c {[ Q ]}" (at level 82, no associativity).
Inductive hoare : assert -> cmd -> assert -> Prop :=
| hoare_hoare0 : forall P Q c, hoare0 P c Q -> {[ P ]} c {[ Q ]}
| hoare_seq : forall P Q R c d, {[ P ]} c {[ Q ]} -> {[ Q ]} d {[ R ]} -> {[ P ]} c ; d {[ R ]}
| hoare_conseq : forall P P' Q Q' c, Q' ===> Q -> P ===> P' ->
  {[ P' ]} c {[ Q' ]} -> {[ P ]} c {[ Q ]}
| hoare_while : forall P t c, {[ fun s h => P s h /\ eval_b t (s, h) ]} c {[ P ]} ->
  {[ P ]} while t c {[ fun s h => P s h /\ ~~ eval_b t (s, h) ]}
| hoare_ifte : forall P Q t c d, {[ fun s h => P s h /\ eval_b t (s, h) ]} c {[ Q ]} ->
  {[ fun s h => P s h /\ ~~ eval_b t (s, h) ]} d {[ Q ]} ->
  {[ P ]} ifte t c d {[ Q ]}
where "{[ P ]} c {[ Q ]}" := (hoare P c Q) : lang_scope.

Definition hoare_semantics (P : assert) (c : cmd) (Q : assert) : Prop :=
  forall s h, P s h -> ~ Some (s, h) -- c ---> None /\
    (forall s' h', Some (s, h) -- c ---> Some (s', h') -> Q s' h').

Definition wp_semantics (c : cmd) (Q : assert) : assert :=
  fun s h => ~ (Some (s, h) -- c ---> None ) /\
    forall s' h', Some (s, h) -- c ---> Some (s', h') -> Q s' h'.

Reserved Notation "{{{[ P ]}}} c {{{[ Q ]}}}" (at level 82, no associativity).
Inductive hoare_total : assert -> cmd -> assert -> Prop :=
| hoaret_hoare0 : forall P Q c, hoare0 P c Q -> {{{[ P ]}}} c {{{[ Q ]}}}
| hoaret_seq : forall P Q R c d, {{{[ P ]}}} c {{{[ Q ]}}} -> {{{[ Q ]}}} d {{{[ R ]}}} -> {{{[ P ]}}} c ; d {{{[ R ]}}}
| hoaret_conseq : forall P P' Q Q' c, (Q' ===> Q) -> (P ===> P') ->
  {{{[ P' ]}}} c {{{[ Q' ]}}} -> {{{[ P ]}}} c {{{[ Q ]}}}
| hoaret_while : forall P t c
  A (R : A -> A -> Prop) (Rwf : well_founded R) (V : state -> A) a,
  (forall a, {{{[ fun s h => P s h /\ eval_b t (s, h) /\ V (s,h) = a ]}}}
    c {{{[ fun s h => P s h /\ R (V (s,h)) a ]}}}) ->
  {{{[ fun s h => P s h /\ V (s,h) = a ]}}}
    while t c {{{[ fun s h => P s h /\ ~~ eval_b t (s, h) ]}}}
| hoaret_ifte : forall P Q t c d,
  {{{[ fun s1 h => P s1 h /\ eval_b t (s1, h) ]}}} c {{{[ Q ]}}} ->
  {{{[ fun s1 h => P s1 h /\ ~~ eval_b t (s1, h) ]}}} d {{{[ Q ]}}} ->
  {{{[ P ]}}} ifte t c d {{{[ Q ]}}}
where "{{{[ P ]}}} c {{{[ Q ]}}}" := (hoare_total P c Q) : lang_scope.

Definition hoare_semantics_total (P : assert) (c : cmd) (Q : assert) : Prop :=
  forall s h, P s h ->
    exists s', exists h', Some (s, h) -- c ---> Some (s', h') /\ Q s' h'.

End Lang.

Implicit Arguments cmd [cmd0 expr_b].
Implicit Arguments cmd_cmd0 [cmd0 expr_b].
Implicit Arguments seq [cmd0 expr_b].
Implicit Arguments ifte [cmd0 expr_b].
Implicit Arguments while [cmd0 expr_b].

Implicit Arguments Not [store heap].

Generic Properties of the Operational Semantics of While

We pack the generic syntax and the corresponding operational semantics above as a module:

Module Type WHILE_SEMOP.

Parameter store : Type.
Parameter heap : Type.
Definition state : Type := (store * heap)%type.

Parameter cmd0 : Type.
Parameter exec0 : option state -> cmd0 -> option state -> Prop.
Notation "s -- c ----> t" := (exec0 s c t) (at level 74 , no associativity) : while_cmd_scope.
Local Open Scope while_cmd_scope.
Delimit Scope while_cmd_scope with while_cmd.

Parameter from_none0 : forall (c : cmd0) s, None -- c ----> s -> s = None.
Parameter cmd0_terminate : forall (c : cmd0) s, exists s', Some s -- c ----> s'.

Parameter expr_b : Type.
Parameter neg : expr_b -> expr_b.
Parameter eval_b : expr_b -> state -> bool.
Parameter eval_b_neg : forall t s, eval_b (neg t) s = ~~ eval_b t s.
Definition cmd := @cmd cmd0 expr_b.
Notation "c ; d" := (@seq cmd0 expr_b c d) (at level 81, right associativity) : while_cmd_scope.
Coercion cmd_cmd0_coercion := @cmd_cmd0 cmd0 expr_b.
Definition exec := (@exec store heap cmd0 exec0 expr_b eval_b).
Notation "s -- c ---> t" := (exec s c t) (at level 74, no associativity) : while_cmd_scope.

End WHILE_SEMOP.

We can derive some generic properties from the module above:

Module While_Semop_Prop (while_semop_m : WHILE_SEMOP).

Import while_semop_m.
Local Open Scope while_cmd_scope.

Lemma from_none : forall c s, None -- c ---> s -> s = None.

Lemma exec_cmd0_inv : forall s (c : cmd0) s',
  Some s -- c ---> s' -> Some s -- c ----> s'.

Lemma exec0_not_None_to_exec_not_None : forall s h (c:cmd0),
  ~ Some (s, h) -- cmd_cmd0 c ---> None -> ~ Some (s, h) -- c ----> None.

Lemma exec_seq_inv : forall c d s s', s -- c ; d ---> s' ->
  exists s'', s -- c ---> s'' /\ s'' -- d ---> s'.

Lemma exec_seq_inv_Some : forall c d s s',
  Some s -- c ; d ---> Some s' ->
  exists s'', Some s -- c ---> Some s'' /\ Some s'' -- d ---> Some s'.

Lemma exec_while_inv_false : forall b c s h s' h', ~~ eval_b b (s, h) ->
  Some (s, h) -- while b c ---> Some (s', h') -> s = s' /\ h = h'.

Lemma exec_while_inv_true : forall b s h, eval_b b (s, h) ->
  forall c s' h', Some (s, h) -- while b c ---> Some (s', h') ->
  exists s'', exists h'', Some (s, h) -- c ---> Some (s'', h'') /\
                          Some (s'', h'') -- while b c ---> Some (s', h').

Lemma exec_ifte_true_inv : forall t c1 c2 s h s', eval_b t (s, h) ->
  Some (s, h) -- ifte t c1 c2 ---> s' -> Some (s, h) -- c1 ---> s'.

Lemma exec_ifte_false_inv : forall t c1 c2 s h s', ~~ eval_b t (s, h) ->
  Some (s, h) -- ifte t c1 c2 ---> s' -> Some (s, h) -- c2 ---> s'.

Lemma exec_seq_assoc : forall s s' c0 c1 c2,
  s -- (c0 ; c1) ; c2 ---> s' -> s -- c0 ; c1 ; c2 ---> s'.

Lemma exec_seq_assoc' : forall s s' c0 c1 c2,
  s -- c0 ; c1 ; c2 ---> s' -> s -- (c0 ; c1) ; c2 ---> s'.

Lemma while_seq : forall s h t, eval_b t (s, h) -> forall s' c,
  Some (s, h) -- while t c ---> s' -> Some (s, h) -- c ; while t c ---> s'.

Lemma while_seq' : forall s h t, eval_b t (s, h) -> forall s' c,
  Some (s, h) -- c ; while t c ---> s' -> Some (s, h) -- while t c ---> s'.

Lemma exec_seq1_not_None : forall s h c1 c2,
  ~ Some (s, h) -- c1 ; c2 ---> None -> ~ Some (s, h) -- c1 ---> None.

Lemma exec_seq2_not_None : forall s h s' h' c1 c2,
  ~ Some (s, h) -- c1 ; c2 ---> None -> Some (s, h) -- c1 ---> Some (s', h') ->
  ~ Some (s', h') -- c2 ---> None.

Lemma exec_ifte1_not_None: forall s h c1 c2 t,
  ~ Some (s, h) -- ifte t c1 c2 ---> None -> eval_b t (s, h) ->
  ~ Some (s, h) -- c1 ---> None.

Lemma exec_ifte2_not_None: forall s h c1 c2 t,
  ~ Some (s, h) -- ifte t c1 c2 ---> None -> ~~ eval_b t (s, h) ->
  ~ Some (s, h) -- c2 ---> None.

Lemma exec_while1_not_None: forall s h t c,
  ~ Some (s, h) -- while t c ---> None -> eval_b t (s, h) ->
  ~ Some (s, h) -- c ---> None.

Lemma exec_while2_not_None: forall s h c t s0 h0,
  ~ Some (s, h) -- while t c ---> None -> eval_b t (s, h) ->
  Some (s, h) -- c ---> Some (s0, h0) -> ~ Some (s0, h0) -- while t c ---> None.

Lemma not_exec_seq_inv_Some : forall c d s h, ~ Some (s, h) -- c ; d ---> None ->
  ~ Some (s, h) -- c ---> None /\
  forall s', Some (s, h) -- c ---> Some s' -> ~ (Some s' -- d ---> None ).

Lemma not_exec_ifte_inv_Some : forall b c d s h,
  ~ Some (s, h) -- ifte b c d ---> None ->
  (eval_b b (s, h) -> ~ Some (s, h) -- c ---> None ) /\
  (~~ eval_b b (s, h) -> ~ Some (s, h) -- d ---> None ).

Lemma while_preserves : forall t c (P : store -> Prop) s h s' h', P s ->
  Some (s, h) -- while t c ---> Some (s', h') ->
  (forall s h s' h', P s -> eval_b t (s, h) -> Some (s, h) -- c ---> Some (s', h') -> P s') ->
  P s'.

Lemma while_condition_inv : forall s h s' h' b c,
  Some (s, h) -- while b c ---> Some (s', h') -> ~~ eval_b b (s', h').

End While_Semop_Prop.

Module Type WHILE_SEMOP_DETER.

Include WHILE_SEMOP.

Local Open Scope while_cmd_scope.

Parameter exec0_deter : forall (st : option state) (c : cmd0) (st' : option state),
  st -- c ----> st' -> forall st'', st -- c ----> st'' -> st' = st''.

End WHILE_SEMOP_DETER.

Module While_Semop_Deter_Prop (while_semop_deter_m : WHILE_SEMOP_DETER).

Import while_semop_deter_m.

Module Import while_semop_prop_m := While_Semop_Prop while_semop_deter_m.

Local Open Scope while_cmd_scope.

Lemma exec_deter : forall ST c ST', ST -- c ---> ST' ->
  forall ST'', ST -- c ---> ST'' -> ST' = ST''.

End While_Semop_Deter_Prop.

Generic Properties of the Hoare Logic of While

We then pack the generic Hoare logic above as a module:

Module Type WHILE_HOARE.

Include WHILE_SEMOP.

Local Open Scope while_cmd_scope.

Definition assert := store -> heap -> Prop.
Notation "'FF'" := (@FF store heap) (at level 80, no associativity) : while_assert_scope.
Notation "'TT'" := (@TT store heap) (at level 80, no associativity) : while_assert_scope.
Notation "P '//\\' Q" := (@And store heap P Q) (at level 80, no associativity) : while_assert_scope.
Notation "P ===> Q" := (@entails store heap P Q) (at level 90, no associativity) : while_assert_scope.
Notation "P <==> Q" := (@equiv store heap P Q) (at level 90, no associativity) : while_assert_scope.

Parameter hoare0 : assert -> cmd0 -> assert -> Prop.

Notation "'hoare_semantics'" := (@hoare_semantics store heap _ exec0 _ eval_b) : while_hoare_scope.

Local Open Scope while_hoare_scope.

Parameter soundness0 : forall P Q c, hoare0 P c Q -> hoare_semantics P c Q.

Definition hoare := @hoare store heap cmd0 _ eval_b hoare0.

Notation "{{ P }} c {{ Q }}" := (hoare P c Q) (at level 82, no associativity) : while_hoare_scope.

Notation "'wp_semantics'" := (@wp_semantics store heap _ exec0 _ eval_b) : while_hoare_scope.

Parameter wp_semantics_sound0 : forall (c : cmd0) Q, {{ wp_semantics c Q }} c {{ Q }}.

The definition of Hoare logic for SGoto will require a function to compute the weakest precondition of one-step, non-branching instructions:

Parameter wp0 : cmd0 -> assert -> assert.
Parameter wp0_no_err : forall s h c P, wp0 c P s h -> ~ (Some (s,h) -- c ----> None ).

End WHILE_HOARE.

Finally, the Hoare logic must be shown to be sound and (relatively) complete, as capture by this last module:

Module While_Hoare_Prop (while_hoare_m : WHILE_HOARE).

Import while_hoare_m.

Module Import while_semop_prop_m := While_Semop_Prop while_hoare_m.

Local Open Scope while_cmd_scope.
Local Open Scope while_assert_scope.
Local Open Scope while_hoare_scope.

Lemma entails_id : forall P, P ===> P.

Lemma entails_trans : forall P Q R, P ===> Q -> Q ===> R -> P ===> R.

Lemma ex_falso : forall Q, FF ===> Q.

Lemma ex_falso' : forall P, P ===> TT.

Lemma FF_is_not_TT : FF <==> Not (TT).

Lemma hoare_stren : forall P P' Q c,
  P ===> P' -> {{ P' }} c {{ Q }} -> {{ P }} c {{ Q }}.

Lemma hoare_stren_seq : forall (P P' Q Q' : assert) c c',
  {{ P' }} c {{ Q' }} -> P ===> P' -> {{ Q' }} c' {{ Q }} -> {{ P }} c; c' {{ Q }}.

Lemma hoare_weak : forall (P Q Q' : assert) c,
  Q' ===> Q -> {{ P }} c {{ Q' }} -> {{ P }} c {{ Q }}.

Lemma hoare_seq_inv : forall P Q c d, {{ P }} c ; d {{ Q }} ->
  exists R, {{ P }} c {{ R }} /\ {{ R }} d {{ Q }}.

Require Import ClassicalChoice.

Lemma hoare_seq_inv_special : forall (A : Type) (P Q : A -> assert) c d,
  (forall x, {{ P x }} c ; d {{ Q x }}) ->
  exists R : A -> assert ,
    (forall x, {{ P x }} c {{ R x }}) /\ (forall x, {{ R x }} d {{ Q x }}).

Lemma hoare_seq_assoc : forall P c0 c1 c2 Q,
  {{ P }} c0 ; c1 ; c2 {{ Q }} -> {{ P }} (c0 ; c1) ; c2 {{ Q }}.

Lemma hoare_seq_assoc' : forall P c0 c1 c2 Q,
  {{ P }} (c0 ; c1) ; c2 {{ Q }} -> {{ P }} c0 ; c1 ; c2 {{ Q }}.

Lemma hoare_ifte_inv : forall P Q b c d, {{ P }} ifte b c d {{ Q }} ->
  {{ fun s h => P s h /\ eval_b b (s, h) }} c {{ Q }} /\
  {{ fun s h => P s h /\ ~~ eval_b b (s, h) }} d {{ Q }}.

Lemma hoare_while_invariant : forall P t c Q Inv, P ===> Inv ->
  (fun s h => Inv s h /\ ~~ eval_b t (s, h)) ===> Q ->
  {{ fun s h => Inv s h /\ eval_b t (s, h) }} c {{ Inv }} ->
  {{ P }} while t c {{ Q }}.

Lemma hoare_while_invariant_seq : forall b c I P Q c1,
  P ===> I ->
  {{ fun s h => I s h /\ eval_b b (s, h) }} c {{ I }} ->
  {{ fun s h => I s h /\ ~~ eval_b b (s, h) }} c1 {{ Q }} ->
  {{ P }} while b c; c1 {{ Q }}.

Lemma hoare_while_inv' : forall P Q b c, {{ P }} while b c {{ Q }} ->
  exists R, (P ===> R) /\
    {{ fun s h => R s h /\ eval_b b (s, h) }} c {{ R }} /\
    ((fun s h => R s h /\ ~~ eval_b b (s, h)) ===> Q).

Lemma hoare_while_inv_special : forall (A : Type) (P Q : A -> assert) b c,
  (forall x, {{ P x }} while b c {{ Q x }}) ->
  exists R : A -> assert ,
    (forall x, {{ fun s h => R x s h /\ eval_b b (s, h) }} c {{ R x }}) /\
    (forall x, (P x ===> R x)) /\
    (forall x, ((fun s h => R x s h /\ ~~ eval_b b (s, h)) ===> Q x)).

Lemma hoare_and'' : (forall P Q c, hoare0 P c Q ->
  forall P' Q', {{P'}} c {{Q'}} -> {{ P //\\ P' }} cmd_cmd0 c {{ Q //\\ Q' }}) ->
  forall c P Q, {{ P }} c {{ Q }} ->
    forall P' Q' d, {{ P' }} d {{ Q' }} ->
      c = d -> {{ P //\\ P' }} c {{ Q //\\ Q' }}.

Lemma hoare_and' : (forall P Q c, hoare0 P c Q ->
  forall P' Q', {{P'}} c {{Q'}} ->{{P //\\ P'}}cmd_cmd0 c {{Q //\\ Q'}}) ->
forall c P Q P' Q',
  {{ P }} c {{ Q }} -> {{ P' }} c {{ Q' }} ->
  {{ P //\\ P' }} c {{ Q //\\ Q' }}.

Lemma hoare_false' : (forall (c0 : cmd0) P, {{ FF }} c0 {{ P }}) -> forall c P, {{ FF }} c {{ P }}.

Lemma pull_out_conjunction' : (forall (c0 : cmd0) P, {{ FF }} c0 {{ P }}) -> forall (A : Prop) P Q c,
  (A -> {{ P }} c {{ Q }}) ->
  {{ fun s h => A /\ P s h }} c {{ Q }}.

The statement of this lemma as well as the proof idea of using ClassicalChoice comes from Andrew W. Appel, septacs.pdf

Lemma extract_exists :
  (forall (c : cmd0) (A : Type) (P Q : A -> assert),
    (forall x, {{ P x }} c {{ Q x }}) ->
    {{ fun s h => exists x, P x s h }} c {{ fun s h => exists x, Q x s h }}) ->
  forall (A : Type) (P Q : A -> assert) c,
  (forall x, {{ P x }} c {{ Q x}}) ->
  {{ fun s h => exists x, P x s h}} c {{ fun s h => exists x, Q x s h }}.

Lemma pull_out_exists' :
  (forall (c : cmd0) (A : Type) (P Q : A -> assert),
    (forall x, {{ P x }} c {{ Q x }}) ->
    {{ fun s h => exists x, P x s h }} c {{ fun s h => exists x, Q x s h }}) ->
  forall (A : Type) (P : A -> assert) c (Q : assert),
  (forall x, {{ P x }} c {{ Q }}) ->
  {{ fun s h => exists x, P x s h }} c {{ Q }}.

Lemma soundness : forall P Q c, {{ P }} c {{ Q }} -> hoare_semantics P c Q.

from a triple and a termination proof, we can deduce that the program does not fail

Lemma termi : forall c P Q, {{ P }} c {{ Q }} ->
  (forall s h, P s h -> {s' | Some (s, h) -- c ---> s' } ) ->
  forall s h, P s h ->
    {s' | Some (s, h) -- c ---> Some s' }.

Lemma wp_semantics_sound : forall c Q, {{ wp_semantics c Q }} c {{ Q }}.

Lemma hoare_complete : forall P Q c, hoare_semantics P c Q -> {{ P }} c {{ Q }}.

Notation "'hoare_semantics_total'" := (@hoare_semantics_total store heap _ exec0 _ eval_b)
  : while_hoare_scope.

Notation "{{{ P }}} c {{{ Q }}}" := (@hoare_total store heap _ _ eval_b hoare0 P c Q) (at level 82, no associativity)
  : while_hoare_scope.

Lemma hoare_total_sound' :
  (forall (P Q : assert) c, hoare0 P c Q ->
    hoare_semantics_total P c Q) ->
  forall P Q c, {{{ P }}} c {{{ Q }}} -> hoare_semantics_total P c Q.

End While_Hoare_Prop.

Module Type WHILE_HOARE_DETER.

Include WHILE_HOARE.

Local Open Scope while_cmd_scope.

Parameter exec0_deter : forall (st : option state) (c : cmd0) (st' : option state),
  st -- c ----> st' ->
  forall st'', st -- c ----> st'' -> st' = st''.

Parameter exec0_wp0 : forall s h (c : cmd0) s' h', Some (s, h) -- c ----> Some (s', h') ->
  forall (P : assert), wp0 c P s h <-> P s' h'.

End WHILE_HOARE_DETER.