Library ICSemantics

Semantics for IC

We define a small-step operation semantics and an axiomatic semantics for IC. For the axiomatic semantics we provide a recursively defined function computing the WP predicate. We show the equivalence of all three representations.
Require Import Facts States ICSyntax.
Set Implicit Arguments.

Module ICSemantics (Sigma : State).
Module ICSyn := ICSyntax.ICSyntax Sigma.
Export ICSyn.

Implicit Types (P : Pred state) (Q QQ : NPred state) (x y z : state).
Implicit Types (a : action) (b : guard) (s t : term).

Small-step Semantics

Definition conf := (term × state)%type.
Inductive step : confconfProp :=
| step_act a s x :
    step (Act a s, x) (s, a x)
| step_def s t x:
    step (Def s t, x) (t.[Def s s/], x)
| step_if_true b s t x :
    b x
    step (If b s t, x) (s, x)
| step_if_false b s t x :
    ~~b x
    step (If b s t, x) (t, x).
Notation mstep := (star step).

Axiomatic Semantics

Inductive eval Q : termPred state :=
| eval_act a s x :
    eval Q s (a x) →
    eval Q (Act a s) x
| eval_if_true b s t x :
    b x
    eval Q s x
    eval Q (If b s t) x
| eval_if_false b s t x :
    ~~b x
    eval Q t x
    eval Q (If b s t) x
| eval_jump f x :
    Q f x
    eval Q (Jump f) x
| eval_def P s t x :
    P <<= eval Q (Def s s) →
    eval (P .: Q) t x
    eval Q (Def s t) x.

WP Semantics

Fixpoint wp Q s :=
  match s with
    | Act a swp Q s \o a
    | If b s tfun sigmaif b sigma then wp Q s sigma else wp Q t sigma
    | Jump fQ f
    | Def s t
      let F P := wp (P .: Q) s in
      wp (Fix F .: Q) t

Lemma wp_mono Q QQ :
  ( n, Q n <<= QQ n) → ( s, wp Q s <<= wp QQ s).

Lemma wp_equiv Q QQ s x :
  ( n x, Q n x QQ n x) → (wp Q s x wp QQ s x).

Lemma wp_cons_mono Q s :
  monotone (fun Pwp (P .: Q) s).

Lemma wp_fix P Q s :
  wp (P .: Q) s <<= PFix (fun Pwp (P .: Q) s) <<= P.

Equivalence of the axiomatic and wp semantics

Lemma wp_eval Q s :
  wp Q s <<= eval Q s.

Lemma eval_wp Q s :
  eval Q s <<= wp Q s.

Theorem coincidence Q s x : eval Q s x wp Q s x.

Compatibility with substitutions

Lemma wp_ren Q (xi : varvar) s :
  wp Q s.[ren xi] = wp (xi >>> Q) s.

Lemma wp_weaken P Q s : wp (P .: Q) s.[ren (+1)] = wp Q s.

Lemma wp_subst Q (theta : varterm) s :
  wp Q s.[theta] = wp (wp Q \o theta) s.

Correspondence between the operational and axiomatic semantics

Lemma step_admissible Q s t x y :
  step (s,x) (t,y) → (wp Q s x wp Q t y).

Lemma mstep_admissible Q f s x y :
  mstep (s,x) (Jump f,y) → (wp Q s x Q f y).

Definition terminates s x :=
   f y, mstep (s,x) (Jump f,y).

Lemma step_terminates s t x y :
  step (s,x) (t,y)terminates t yterminates s x.

Lemma eval_terminates Q s x :
  eval Q s x theta,
    ( f, Q f <<= terminates (theta f)) →
    terminates s.[theta] x.

Corollary eval_terminates_id Q s :
  eval Q s <<= terminates s.

Theorem correspondence Q s x :
  wp Q s x f y, mstep (s,x) (Jump f,y) Q f y.

Consequences of the correspondence result

Definition point_pred f x : NPred state := fun g yf = g x = y.

Corollary wp_step_equiv f s x y :
  mstep (s,x) (Jump f,y) wp (point_pred f y) s x.

Corollary wp_terminates s x :
  wp (@Top _) s x terminates s x.

Corollary wp_det Q s x :
  wp Q s x f y, wp (point_pred f y) s x Q f y.

End ICSemantics.