A certified WP calculus

Formalisation d’un langage impératif jouet

Syntaxe

theory Syntax

use export bool.Bool
use export int.Int

types and values

type datatype = TYunit | TYint | TYbool
type value = Vvoid | Vint int | Vbool bool

terms and formulas

type operator = Oplus | Ominus | Omult | Ole

type mident

lemma mident_decide :
  forall m1 m2: mident. m1 = m2 \/ m1 <> m2

type ident

lemma ident_decide :
  forall m1 m2: ident. m1 = m2 \/ m1 <> m2

type term =
  | Tvalue value
  | Tvar ident
  | Tderef mident
  | Tbin term operator term

type fmla =
  | Fterm term
  | Fand fmla fmla
  | Fnot fmla
  | Fimplies fmla fmla
  | Flet ident term fmla         (* let id = term in fmla *)
  | Fforall ident datatype fmla  (* forall id : ty, fmla *)

type stmt =
  | Sskip
  | Sassign mident term
  | Sseq stmt stmt
  | Sif term stmt stmt
  | Sassert fmla
  | Swhile term fmla stmt  (* while cond invariant inv body *)

lemma decide_is_skip:
  forall s:stmt. s = Sskip \/ s <> Sskip

end

Semantique Operationnelle

theory SemOp

use export Syntax
use map.Map as IdMap
use export list.List

type env = IdMap.map mident value  (* map global mutable variables to their value *)
function get_env (i:mident) (e:env) : value = IdMap.get e i

type stack = list (ident, value)  (* map local immutable variables to their value *)
function get_stack (i:ident) (pi:stack) : value =
  match pi with
  | Nil -> Vvoid
  | Cons (x,v) r -> if x=i then v else get_stack i r
  end

lemma get_stack_eq:
  forall x:ident, v:value, r:stack.
    get_stack x (Cons (x,v) r) = v

lemma get_stack_neq:
  forall x i:ident, v:value, r:stack.
    x <> i -> get_stack i (Cons (x,v) r) = get_stack i r

semantics of formulas

function eval_bin (x:value) (op:operator) (y:value) : value =
  match x,y with
  | Vint x,Vint y ->
     match op with
     | Oplus -> Vint (x+y)
     | Ominus -> Vint (x-y)
     | Omult -> Vint (x*y)
     | Ole -> Vbool (if x <= y then True else False)
     end
  | _,_ -> Vvoid
  end

function eval_term (sigma:env) (pi:stack) (t:term) : value =
  match t with
  | Tvalue v -> v
  | Tvar id  -> get_stack id pi
  | Tderef id  -> get_env id sigma
  | Tbin t1 op t2  ->
     eval_bin (eval_term sigma pi t1) op (eval_term sigma pi t2)
  end

predicate eval_fmla (sigma:env) (pi:stack) (f:fmla) =
  match f with
  | Fterm t -> eval_term sigma pi t = Vbool True
  | Fand f1 f2 -> eval_fmla sigma pi f1 /\ eval_fmla sigma pi f2
  | Fnot f -> not (eval_fmla sigma pi f)
  | Fimplies f1 f2 -> eval_fmla sigma pi f1 -> eval_fmla sigma pi f2
  | Flet x t f ->
      eval_fmla sigma (Cons (x,eval_term sigma pi t) pi) f
  | Fforall x TYint f ->
     forall n:int. eval_fmla sigma (Cons (x,Vint n) pi) f
  | Fforall x TYbool f ->
     forall b:bool. eval_fmla sigma (Cons (x,Vbool b) pi) f
  | Fforall x TYunit f ->  eval_fmla sigma (Cons (x,Vvoid) pi) f
  end

predicate valid_fmla (p:fmla) = forall sigma:env, pi:stack. eval_fmla sigma pi p

small-steps semantics for statements

inductive one_step env stack stmt env stack stmt =

  | one_step_assign : forall sigma sigma':env, pi:stack, x:mident, t:term.
      sigma' = IdMap.set sigma x (eval_term sigma pi t) ->
      one_step sigma pi (Sassign x t) sigma' pi Sskip

  | one_step_seq_noskip: forall sigma sigma':env, pi pi':stack, s1 s1' s2:stmt.
      one_step sigma pi s1 sigma' pi' s1' ->
      one_step sigma pi (Sseq s1 s2) sigma' pi' (Sseq s1' s2)

  | one_step_seq_skip: forall sigma:env, pi:stack, s:stmt.
      one_step sigma pi (Sseq Sskip s) sigma pi s

  | one_step_if_true: forall sigma:env, pi:stack, t:term, s1 s2:stmt.
      eval_term sigma pi t = Vbool True ->
      one_step sigma pi (Sif t s1 s2) sigma pi s1

  | one_step_if_false: forall sigma:env, pi:stack, t:term, s1 s2:stmt.
      eval_term sigma pi t = Vbool False ->
      one_step sigma pi (Sif t s1 s2) sigma pi s2

  | one_step_assert: forall sigma:env, pi:stack, f:fmla.
      eval_fmla sigma pi f ->

      one_step sigma pi (Sassert f) sigma pi Sskip

  | one_step_while_true: forall sigma:env, pi:stack, cond:term, inv:fmla, body:stmt.
      eval_fmla sigma pi inv /\

      eval_term sigma pi cond = Vbool True ->
      one_step sigma pi (Swhile cond inv body) sigma pi (Sseq body (Swhile cond inv body))

  | one_step_while_false: forall sigma:env, pi:stack, cond:term, inv:fmla, body:stmt.
        eval_fmla sigma pi inv /\

        eval_term sigma pi cond = Vbool False ->
        one_step sigma pi (Swhile cond inv body) sigma pi Sskip

many steps of execution

inductive many_steps env stack stmt env stack stmt int =
  | many_steps_refl: forall sigma:env, pi:stack, s:stmt.
      many_steps sigma pi s sigma pi s 0
  | many_steps_trans: forall sigma1 sigma2 sigma3:env, pi1 pi2 pi3:stack, s1 s2 s3:stmt, n:int.
      one_step sigma1 pi1 s1 sigma2 pi2 s2 ->
      many_steps sigma2 pi2 s2 sigma3 pi3 s3 n ->
      many_steps sigma1 pi1 s1 sigma3 pi3 s3 (n+1)

lemma steps_non_neg: forall sigma1 sigma2:env, pi1 pi2:stack, s1 s2:stmt, n:int.
  many_steps sigma1 pi1 s1 sigma2 pi2 s2 n -> n >= 0

predicate reductible (sigma:env) (pi:stack) (s:stmt) =
  exists sigma':env, pi':stack, s':stmt. one_step sigma pi s sigma' pi' s'

end

theory TestSemantics

use SemOp
use map.Const

function my_sigma : env = Const.const (Vint 0)
constant x : ident
constant y : mident

function my_pi : stack = Cons (x, Vint 42) Nil

goal Test13 :
  eval_term my_sigma my_pi (Tvalue (Vint 13)) = Vint 13

goal Test42 :
  eval_term my_sigma my_pi (Tvar x) = Vint 42

goal Test0 :
  eval_term my_sigma my_pi (Tderef y) = Vint 0

goal Test55 :
  eval_term my_sigma my_pi (Tbin (Tvar x) Oplus (Tvalue (Vint 13))) = Vint 55

goal Ass42 :
  forall sigma':env, pi':stack.
    one_step my_sigma my_pi (Sassign y (Tvalue (Vint 42))) sigma' pi' Sskip ->
      IdMap.get sigma' y = Vint 42

goal If42 :
    forall sigma1 sigma2:env, pi1 pi2:stack, s:stmt.
      one_step my_sigma my_pi
        (Sif (Tbin (Tderef y) Ole (Tvalue (Vint 10)))
             (Sassign y (Tvalue (Vint 13)))
             (Sassign y (Tvalue (Vint 42))))
        sigma1 pi1 s ->
      one_step sigma1 pi1 s sigma2 pi2 Sskip ->
        IdMap.get sigma2 y = Vint 13

end

Typage

theory Typing

use export Syntax
use map.Map as IdMap
use export list.List

function type_value (v:value) : datatype =
  match v with
    | Vvoid  -> TYunit
    | Vint _ ->  TYint
    | Vbool _ -> TYbool
  end

inductive type_operator (op:operator) (ty1 ty2 ty: datatype) =
  | Type_plus : type_operator Oplus TYint TYint TYint
  | Type_minus : type_operator Ominus TYint TYint TYint
  | Type_mult : type_operator Omult TYint TYint TYint
  | Type_le : type_operator Ole TYint TYint TYbool

type type_stack = list (ident, datatype)  (* map local immutable variables to their type *)
function get_vartype (i:ident) (pi:type_stack) : datatype =
  match pi with
  | Nil -> TYunit
  | Cons (x,ty) r -> if x=i then ty else get_vartype i r
  end

type type_env = IdMap.map mident datatype  (* map global mutable variables to their type *)
function get_reftype (i:mident) (e:type_env) : datatype = IdMap.get e i

inductive type_term type_env type_stack term datatype =

  | Type_value : forall sigma: type_env, pi:type_stack, v:value.
      type_term sigma pi  (Tvalue v) (type_value v)

  | Type_var : forall sigma: type_env, pi:type_stack, v: ident, ty:datatype.
      (get_vartype v pi = ty) ->
      type_term sigma pi (Tvar v) ty

  | Type_deref : forall sigma: type_env, pi:type_stack, v: mident, ty:datatype.
      (get_reftype v sigma = ty) ->
      type_term sigma pi (Tderef v) ty

  | Type_bin : forall sigma: type_env, pi:type_stack, t1 t2 : term, op:operator, ty1 ty2 ty:datatype.
      type_term sigma pi t1 ty1 /\ type_term sigma pi t2 ty2 /\ type_operator op ty1 ty2 ty ->
      type_term sigma pi (Tbin t1 op t2) ty

inductive type_fmla type_env type_stack fmla =

  | Type_term : forall sigma: type_env, pi:type_stack, t:term.
        type_term sigma pi t TYbool ->
        type_fmla sigma pi (Fterm t)

  | Type_conj : forall sigma: type_env, pi:type_stack, f1 f2:fmla.
      type_fmla sigma pi f1 /\ type_fmla sigma pi f2 ->
      type_fmla sigma pi (Fand f1 f2)

  | Type_neg : forall sigma: type_env, pi:type_stack, f:fmla.
      type_fmla sigma pi f ->
      type_fmla sigma pi (Fnot f)

  | Type_implies : forall sigma: type_env, pi:type_stack, f1 f2:fmla.
       type_fmla sigma pi f1 ->
        type_fmla sigma pi f2 ->
        type_fmla sigma pi (Fimplies f1 f2)
  | Type_let :
      forall sigma: type_env, pi:type_stack, x:ident, t:term, f:fmla, ty:datatype.
        type_term sigma pi t ty ->
        type_fmla sigma (Cons (x,ty) pi) f ->
        type_fmla sigma pi (Flet x t f)
  | Type_forall :
      forall sigma: type_env, pi:type_stack, x:ident, f:fmla, ty:datatype.
        type_fmla sigma (Cons (x,ty) pi) f ->
        type_fmla sigma pi (Fforall x ty f)

inductive type_stmt type_env type_stack stmt =
  | Type_skip :
      forall sigma: type_env, pi:type_stack.
        type_stmt sigma pi Sskip
  | Type_seq :
      forall sigma: type_env, pi:type_stack, s1 s2:stmt.
        type_stmt sigma pi s1 ->
        type_stmt sigma pi s2 ->
        type_stmt sigma pi (Sseq s1 s2)
  | Type_assigns :
      forall sigma: type_env, pi:type_stack, x:mident, t:term, ty:datatype.
        (get_reftype x sigma = ty) ->
        type_term sigma pi t ty ->
        type_stmt sigma pi (Sassign x t)
  | Type_if :
      forall sigma: type_env, pi:type_stack, t:term, s1 s2:stmt.
        type_term sigma pi t TYbool ->
        type_stmt sigma pi s1 ->
        type_stmt sigma pi s2 ->
        type_stmt sigma pi (Sif t s1 s2)
  | Type_assert :
      forall sigma: type_env, pi:type_stack, p:fmla.
        type_fmla sigma pi p ->
        type_stmt sigma pi (Sassert p)
  | Type_while :
      forall sigma: type_env, pi:type_stack, cond:term, body:stmt, inv:fmla.
        type_fmla sigma pi inv ->
        type_term sigma pi cond TYbool ->
        type_stmt sigma pi body ->
        type_stmt sigma pi (Swhile cond inv body)

end

Relations entre typage et semantique operationnelle

theory TypingAndSemantics

use SemOp
use Typing

(*
inductive compatible datatype value =
    | Compatible_bool :
        forall b: bool. compatible TYbool (Vbool b)
    | Compatible_int :
        forall n: int. compatible TYint (Vint n)
    | Compatible_void :
        compatible TYunit Vvoid

*)

predicate compatible_env (sigma:env) (sigmat:type_env) (pi:stack) (pit: type_stack) =
  (forall id: mident. type_value (get_env id sigma) = get_reftype id sigmat) /\
  (forall id: ident. type_value (get_stack id pi) = get_vartype id pit)

lemma type_inversion : forall v [@induction]:value.
   match (type_value v) with
    | TYbool -> exists b: bool. v = Vbool b
    | TYint -> exists n: int. v = Vint n
    | TYunit -> v = Vvoid
  end

lemma eval_type_term:
  forall t:term, sigma:env, pi:stack, sigmat:type_env, pit:type_stack, ty:datatype.
    compatible_env sigma sigmat pi pit ->
    type_term sigmat pit t ty -> type_value (eval_term sigma pi t) = ty

lemma type_preservation :
  forall s1 s2:stmt, sigma1 sigma2:env, pi1 pi2:stack,
         sigmat:type_env, pit:type_stack.
     type_stmt sigmat pit s1 ->
     compatible_env sigma1 sigmat pi1 pit ->
     ([@induction] one_step sigma1 pi1 s1 sigma2 pi2 s2) ->
     type_stmt sigmat pit s2 /\
     compatible_env sigma2 sigmat pi2 pit

end

Problématique des variables fraîches

theory FreshVariables

use SemOp
use list.Append

lemma Cons_append: forall a: 'a, l1 l2: list 'a.
  Cons a (l1 ++ l2) = (Cons a l1) ++ l2

lemma Append_nil_l:
  forall l: list 'a. Nil ++ l = l

substitution of a reference x by a logic variable v warning: proper behavior only guaranted if v is fresh

function msubst_term (t:term) (x:mident) (v:ident) : term =
  match t with
  | Tvalue _ | Tvar _  -> t
  | Tderef y -> if x = y then Tvar v else t
  | Tbin t1 op t2  ->
      Tbin (msubst_term t1 x v) op (msubst_term t2 x v)
  end

function msubst (f:fmla) (x:mident) (v:ident) : fmla =
  match f with
  | Fterm e -> Fterm (msubst_term e x v)
  | Fand f1 f2 -> Fand (msubst f1 x v) (msubst f2 x v)
  | Fnot f -> Fnot (msubst f x v)
  | Fimplies f1 f2 -> Fimplies (msubst f1 x v) (msubst f2 x v)
  | Flet y t f -> Flet y (msubst_term t x v) (msubst f x v)
  | Fforall y ty f -> Fforall y ty (msubst f x v)
  end

predicate fresh_in_term (id:ident) (t:term) =
  match t with
  | Tvalue _ | Tderef _  -> true
  | Tvar i  -> id <> i
  | Tbin t1 _ t2 -> fresh_in_term id t1 /\ fresh_in_term id t2
  end

predicate fresh_in_fmla (id:ident) (f:fmla) =
  match f with
  | Fterm e -> fresh_in_term id e
  | Fand f1 f2   | Fimplies f1 f2 ->
      fresh_in_fmla id f1 /\ fresh_in_fmla id f2
  | Fnot f -> fresh_in_fmla id f
  | Flet y t f -> id <> y /\ fresh_in_term id t /\ fresh_in_fmla id f
  | Fforall y _ f -> id <> y /\ fresh_in_fmla id f
  end

(* Needed for monotonicity and wp_reduction *)
lemma eval_msubst_term:
  forall e [@induction]:term, sigma:env, pi:stack, x:mident, v:ident.
    fresh_in_term v e ->
    eval_term sigma pi (msubst_term e x v) =
    eval_term (IdMap.set sigma x (get_stack v pi)) pi e

lemma eval_msubst:
  forall f [@induction]:fmla, sigma:env, pi:stack, x:mident, v:ident.
    fresh_in_fmla v f ->
    (eval_fmla sigma pi (msubst f x v) <->
     eval_fmla (IdMap.set sigma x (get_stack v pi)) pi f)

lemma eval_swap_term:
  forall t [@induction]:term, sigma:env, pi l:stack, id1 id2:ident, v1 v2:value.
  id1 <> id2 ->
  (eval_term sigma (l++(Cons (id1,v1) (Cons (id2,v2) pi))) t =
   eval_term sigma (l++(Cons (id2,v2) (Cons (id1,v1) pi))) t)

lemma eval_swap_gen:
  forall f [@induction]:fmla, sigma:env, pi l:stack, id1 id2:ident, v1 v2:value.
    id1 <> id2 ->
    (eval_fmla sigma (l++(Cons (id1,v1) (Cons (id2,v2) pi))) f <->
    eval_fmla sigma (l++(Cons (id2,v2) (Cons (id1,v1) pi))) f)

lemma eval_swap:
  forall f:fmla, sigma:env, pi:stack, id1 id2:ident, v1 v2:value.
    id1 <> id2 ->
    (eval_fmla sigma (Cons (id1,v1) (Cons (id2,v2) pi)) f <->
    eval_fmla sigma (Cons (id2,v2) (Cons (id1,v1) pi)) f)

lemma eval_term_change_free :
  forall t [@induction]:term, sigma:env, pi:stack, id:ident, v:value.
    fresh_in_term id t ->
    eval_term sigma (Cons (id,v) pi) t = eval_term sigma pi t

 (* Need it for monotonicity*)
lemma eval_change_free :
  forall f [@induction]:fmla, sigma:env, pi:stack, id:ident, v:value.
    fresh_in_fmla id f ->
    (eval_fmla sigma (Cons (id,v) pi) f <-> eval_fmla sigma pi f)

end

Hoare logic

theory HoareLogic

use Syntax
use SemOp
use FreshVariables

(* Used by Hoare_logic/seq_rule*)
  lemma many_steps_seq:
    forall n:int, sigma1 sigma3:env, pi1 pi3:stack, s1 s2:stmt.
      many_steps sigma1 pi1 (Sseq s1 s2) sigma3 pi3 Sskip n ->
      exists sigma2:env, pi2:stack, n1 n2:int.
        many_steps sigma1 pi1 s1 sigma2 pi2 Sskip n1 /\
        many_steps sigma2 pi2 s2 sigma3 pi3 Sskip n2 /\
        n = 1 + n1 + n2

predicate valid_triple (p:fmla) (s:stmt) (q:fmla) =
    forall sigma:env, pi:stack. eval_fmla sigma pi p ->
      forall sigma':env, pi':stack, n:int.
        many_steps sigma pi s sigma' pi' Sskip n ->
          eval_fmla sigma' pi' q

predicate total_valid_triple (p:fmla) (s:stmt) (q:fmla) =
    forall sigma:env, pi:stack. eval_fmla sigma pi p ->
      exists sigma':env, pi':stack, n:int.
        many_steps sigma pi s sigma' pi' Sskip n /\
        eval_fmla sigma' pi' q

Hoare logic rules (partial correctness)

lemma consequence_rule:
  forall p p' q q':fmla, s:stmt.
  valid_fmla (Fimplies p' p) ->
  valid_triple p s q ->
  valid_fmla (Fimplies q q') ->
  valid_triple p' s q'

lemma skip_rule:
  forall q:fmla. valid_triple q Sskip q

lemma assign_rule:
  forall p:fmla, x:mident, id:ident, t:term.
  fresh_in_fmla id p ->
  valid_triple (Flet id t (msubst p x id)) (Sassign x t) p

lemma seq_rule:
  forall p q r:fmla, s1 s2:stmt.
  valid_triple p s1 r /\ valid_triple r s2 q ->
  valid_triple p (Sseq s1 s2) q

lemma if_rule:
  forall t:term, p q:fmla, s1 s2:stmt.
  valid_triple (Fand p (Fterm t)) s1 q /\
  valid_triple (Fand p (Fnot (Fterm t))) s2 q ->
  valid_triple p (Sif t s1 s2) q

lemma assert_rule:
  forall f p:fmla. valid_fmla (Fimplies p f) ->
  valid_triple p (Sassert f) p

lemma assert_rule_ext:
  forall f p:fmla.
  valid_triple (Fimplies f p) (Sassert f) p

lemma while_rule:
  forall e:term, inv:fmla, i:stmt.
  valid_triple (Fand (Fterm e) inv) i inv ->
  valid_triple inv (Swhile e inv i) (Fand (Fnot (Fterm e)) inv)

end

WP calculus

theory WP

use SemOp
use Typing
use TypingAndSemantics
use FreshVariables

function fresh_from (f:fmla) : ident

  (* Need it for monotonicity*)
axiom fresh_from_fmla: forall f:fmla.
fresh_in_fmla (fresh_from f) f

  (* intention:
       abstract_effects s f = "forall w. f"
     avec w = writes(s)
  *)
  function abstract_effects (s:stmt) (f:fmla) : fmla

  (* hypothese 1: si
       sigma, pi |= forall w. f
     alors
       sigma, pi |= f
  *)
  axiom abstract_effects_specialize :
     forall sigma:env, pi:stack, s:stmt, f:fmla.
        eval_fmla sigma pi (abstract_effects s f) ->
        eval_fmla sigma pi f

  (* hypothese 2: si
       sigma, pi |= (forall w, p) /\ (forall w, q)
     alors
       sigma, pi |= forall w, (f /\ q)
  *)
  axiom abstract_effects_distrib_conj :
     forall s:stmt, p q:fmla, sigma:env, pi:stack.
       eval_fmla sigma pi (abstract_effects s p) /\
       eval_fmla sigma pi (abstract_effects s q) ->
         eval_fmla sigma pi (abstract_effects s (Fand p q))

  (* hypothese 3: si
       |= p -> q
     alors
       |= (forall w, p) -> (forall w, q)

     remarque : il est essentiel de parler de validité dans tous les etats:
     on n'a pas
       sigma,pi |= p -> q
     implique
       sigma,pi |= (forall w, p) -> (forall w, q)

     contre-exemple: sigma(x) = 42 alors true -> x=42
        mais on n'a
             (forall x, true) -> (forall  x, x=42)
  *)

  axiom abstract_effects_monotonic :
     forall s:stmt, p q:fmla.
        valid_fmla (Fimplies p q) ->
        forall sigma:env, pi:stack.
           eval_fmla sigma pi (abstract_effects s p) ->
           eval_fmla sigma pi (abstract_effects s q)

function wp (s:stmt) (q:fmla) : fmla =
    match s with
    | Sskip -> q
    | Sassert f ->
        (* asymmetric and *)
        Fand f (Fimplies f q)
    | Sseq s1 s2 -> wp s1 (wp s2 q)
    | Sassign x t ->
        let id = fresh_from q in
        Flet id t (msubst q x id)
    | Sif t s1 s2 ->
        Fand (Fimplies (Fterm t) (wp s1 q))
             (Fimplies (Fnot (Fterm t)) (wp s2 q))
    | Swhile cond inv body ->
        Fand inv
          (abstract_effects body
            (Fand
              (Fimplies (Fand (Fterm cond) inv) (wp body inv))
              (Fimplies (Fand (Fnot (Fterm cond)) inv) q)))

    end

  axiom abstract_effects_writes :
     forall sigma:env, pi:stack, body:stmt, cond:term, inv q:fmla.
       let f =
         (abstract_effects body (Fand
            (Fimplies (Fand (Fterm cond) inv) (wp body inv))
            (Fimplies (Fand (Fnot (Fterm cond)) inv) q)))
       in
       eval_fmla sigma pi f -> eval_fmla sigma pi (wp body f)

  lemma monotonicity:
    forall s [@induction]:stmt, p q:fmla.
      valid_fmla (Fimplies p q)
     -> valid_fmla (Fimplies (wp s p) (wp s q) )

 (* remarque l'ordre des quantifications est essentiel, on n'a pas
       sigma,pi |= p -> q
     implique
       sigma,pi |= (wp s p) -> (wp s q)

     meme contre-exemple: sigma(x) = 42 alors true -> x=42
        mais
          wp (x := 7) true = true
          wp (x := 7) x=42 = 7=42
  *)

  lemma distrib_conj:
    forall s [@induction]:stmt, sigma:env, pi:stack, p q:fmla.
     (eval_fmla sigma pi (wp s p)) /\
     (eval_fmla sigma pi (wp s q)) ->
     eval_fmla sigma pi (wp s (Fand p q))

  lemma wp_preserved_by_reduction:
    forall sigma sigma':env, pi pi':stack, s s':stmt.
    one_step sigma pi s sigma' pi' s' ->
    forall q:fmla.
      eval_fmla sigma pi (wp s q) ->
      eval_fmla sigma' pi' (wp s' q)

  lemma progress:
    forall s [@induction]:stmt, sigma:env, pi:stack,
           sigmat: type_env, pit: type_stack, q:fmla.
      compatible_env sigma sigmat pi pit ->
      type_stmt sigmat pit s ->
      eval_fmla sigma pi (wp s q) ->
      s <> Sskip -> reductible sigma pi s

main soundness result

  lemma wp_soundness:
    forall n:int, sigma sigma':env, pi pi':stack, s s':stmt,
           sigmat: type_env, pit: type_stack, q:fmla.
      compatible_env sigma sigmat pi pit ->
      type_stmt sigmat pit s ->
      many_steps sigma pi s sigma' pi' s' n /\
      not (reductible sigma' pi' s') /\
      eval_fmla sigma pi (wp s q) ->
      s' = Sskip /\ eval_fmla sigma' pi' q

end