## WP revisited in Why3

A WP calculus, certified using Why3, based on an original blocking semantics. See the research report for more details

Authors: Claude Marché / Asma Tafat

Tools: Why3 / Coq

see also the index (by topic, by tool, by reference, by year)

# 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
```

ident for mutable variables

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

type ident
```

ident for immutable variables

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

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

Terms

```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 *)
```

Formulas

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

Statements

```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
```

Operational semantic

```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
```

`valid_fmla f` is true when `f` is valid in any environment

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 ->```

blocking semantics

```      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 /\```

blocking semantics

```      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 /\```

blocking semantics

```        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
```

`fresh_in_term id t` is true when `id` does not occur in `t`

```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
```

partial correctness

```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

```

# Why3 Proof Results for Project "blocking_semantics5"

## Theory "Syntax": fully verified

 Obligations Alt-Ergo (0.95.1) mident_decide 0.01 ident_decide 0.00 decide_is_skip 0.01

## Theory "SemOp": fully verified

 Obligations Alt-Ergo (0.95.1) CVC3 (2.2) CVC3 (2.4.1) Coq (8.4pl2) Z3 (3.2) Z3 (4.3.1) get_stack_eq 0.01 0.03 0.02 --- 0.04 0.03 get_stack_neq 0.02 0.03 0.02 --- 0.20 0.20 steps_non_neg --- --- --- 1.02 --- ---

## Theory "TestSemantics": fully verified

 Obligations Alt-Ergo (0.95.1) CVC3 (2.4.1) CVC4 (1.2) Coq (8.4pl2) Test13 0.02 --- 0.03 --- Test42 0.03 --- --- --- Test0 0.05 --- --- --- Test55 --- --- 0.04 --- Ass42 0.05 0.05 --- --- If42 --- --- --- 1.85

## Theory "TypingAndSemantics": fully verified

 Obligations Alt-Ergo (0.95.1) CVC3 (2.2) CVC3 (2.4.1) Coq (8.4pl2) Z3 (3.2) Z3 (4.3.1) type_inversion 0.02 0.04 0.93 1.65 Timeout (5s) Timeout (5s) induction_ty_lex 1. 0.08 0.04 0.10 --- 0.07 0.07 eval_type_term --- --- --- --- --- --- induction_ty_lex 1. --- --- --- --- --- --- split_goal_wp 1. 0.07 0.04 0.06 --- Timeout (5s) Timeout (5s) 2. 0.06 0.04 0.04 --- Timeout (5s) Timeout (5s) 3. 0.08 0.04 0.05 --- Timeout (5s) Timeout (5s) 4. Timeout (5s) --- Timeout (5s) 2.52 Timeout (5s) Timeout (5s) type_preservation --- --- --- 2.53 --- ---

## Theory "FreshVariables": fully verified

 Obligations Alt-Ergo (0.95.1) CVC3 (2.2) CVC3 (2.4.1) Coq (8.4pl2) Z3 (3.2) Z3 (4.3.1) Cons_append 0.03 --- --- --- --- --- Append_nil_l 0.03 --- --- --- --- --- eval_msubst_term --- --- --- --- --- --- induction_ty_lex 1. --- --- --- --- --- --- split_goal_wp 1. 0.04 0.04 0.04 --- Timeout (5s) Timeout (5s) 2. 0.04 0.04 0.04 --- Timeout (5s) Timeout (5s) 3. 0.05 0.04 0.04 --- Timeout (5s) Timeout (5s) 4. 0.12 0.05 0.06 --- Timeout (5s) Timeout (5s) eval_msubst --- --- --- --- --- --- induction_ty_lex 1. --- --- --- --- --- --- split_goal_wp 1. 0.05 0.06 0.10 --- Timeout (30s) Out Of Memory (1000M) 2. 0.04 0.06 0.08 --- Timeout (30s) Out Of Memory (1000M) 3. 0.04 0.08 Timeout (30s) --- Timeout (30s) Out Of Memory (1000M) 4. 0.06 0.10 Timeout (30s) --- Timeout (30s) Out Of Memory (1000M) 5. 0.04 0.08 0.55 --- Timeout (30s) Out Of Memory (1000M) 6. 0.04 0.08 Timeout (30s) --- Timeout (30s) Out Of Memory (1000M) 7. 0.07 0.09 0.30 --- Timeout (30s) Out Of Memory (1000M) 8. 0.03 0.09 Timeout (30s) --- Timeout (30s) Out Of Memory (1000M) 9. 1.52 0.70 5.75 1.36 Timeout (30s) Out Of Memory (1000M) 10. 0.17 1.10 Timeout (30s) --- Timeout (30s) Out Of Memory (1000M) 11. Out Of Memory (1000M) Timeout (30s) Timeout (30s) 2.57 Out Of Memory (1000M) Out Of Memory (1000M) 12. 0.77 Timeout (30s) Timeout (30s) --- Timeout (30s) Out Of Memory (1000M) eval_swap_term --- --- --- --- --- --- induction_ty_lex 1. --- --- --- --- --- --- split_goal_wp 1. 0.04 0.04 0.08 --- Timeout (30s) Timeout (30s) 2. Timeout (30s) Timeout (30s) Timeout (30s) 2.00 Timeout (30s) Timeout (30s) 3. 0.05 0.06 0.05 --- Timeout (30s) Timeout (30s) 4. 0.03 0.05 0.25 --- Timeout (30s) Timeout (30s) eval_swap_gen --- --- --- --- --- --- induction_ty_lex 1. --- --- --- --- --- --- split_goal_wp 1. 0.04 0.05 0.24 --- Timeout (30s) Timeout (30s) 2. 0.15 0.05 0.23 --- Timeout (30s) Timeout (30s) 3. 0.10 0.26 0.43 --- Timeout (30s) Timeout (30s) 4. 0.11 0.27 0.46 --- Timeout (30s) Timeout (30s) 5. 0.05 0.22 0.37 --- Timeout (30s) Timeout (30s) 6. 0.16 0.21 0.34 --- Timeout (30s) Timeout (30s) 7. 0.04 0.25 0.41 --- Timeout (30s) Timeout (30s) 8. 0.04 0.24 0.42 --- Timeout (30s) Timeout (30s) 9. 0.14 Timeout (30s) Timeout (30s) --- Timeout (30s) Timeout (30s) 10. 0.15 Timeout (30s) Timeout (30s) --- Timeout (30s) Timeout (30s) 11. 9.52 Timeout (30s) Timeout (30s) 2.00 Timeout (30s) Timeout (30s) 12. 8.60 Timeout (30s) Timeout (30s) 2.00 Timeout (30s) Timeout (30s) eval_swap Timeout (5s) Timeout (5s) Timeout (5s) 1.07 Timeout (5s) Timeout (5s) eval_term_change_free --- --- --- --- --- --- induction_ty_lex 1. --- --- --- --- --- --- split_goal_wp 1. 0.04 0.04 0.05 --- Timeout (20s) Out Of Memory (1000M) 2. 0.04 0.11 0.06 --- Timeout (20s) Out Of Memory (1000M) 3. 0.04 0.03 0.04 --- Timeout (30s) Out Of Memory (1000M) 4. 0.07 0.03 0.05 --- Timeout (30s) Out Of Memory (1000M) eval_change_free --- --- --- --- --- --- induction_ty_lex 1. --- --- --- --- --- --- split_goal_wp 1. 0.05 0.05 0.06 --- Timeout (30s) Out Of Memory (1000M) 2. 0.06 0.04 0.15 --- Timeout (30s) Out Of Memory (1000M) 3. 0.08 0.05 0.07 --- Timeout (30s) Out Of Memory (1000M) 4. 0.12 0.06 0.07 --- Timeout (30s) Out Of Memory (1000M) 5. 0.05 0.05 0.06 --- Timeout (20s) Out Of Memory (1000M) 6. 0.06 0.05 0.06 --- Timeout (30s) Out Of Memory (1000M) 7. 0.07 0.06 0.07 --- Timeout (30s) Out Of Memory (1000M) 8. 0.04 0.06 0.07 --- Timeout (30s) Out Of Memory (1000M) 9. 0.58 --- 0.29 1.11 Timeout (20s) Out Of Memory (1000M) 10. 0.07 0.39 0.50 1.12 Timeout (20s) Out Of Memory (1000M) 11. Timeout (30s) Timeout (30s) Timeout (30s) 2.00 Timeout (30s) Out Of Memory (1000M) 12. 0.18 Timeout (30s) Timeout (30s) 1.53 Timeout (30s) Out Of Memory (1000M)

## Theory "HoareLogic": fully verified

 Obligations CVC3 (2.2) CVC3 (2.4.1) Coq (8.4pl2) Z3 (3.2) Z3 (4.3.1) many_steps_seq --- --- 1.73 --- --- consequence_rule 0.08 0.15 --- --- --- skip_rule --- --- 1.14 --- --- assign_rule --- --- 1.96 --- --- seq_rule --- --- --- 0.09 0.06 if_rule --- --- 1.71 --- --- assert_rule --- --- 1.23 --- --- assert_rule_ext --- --- 1.47 --- --- while_rule --- --- 1.39 --- ---

## Theory "WP": fully verified

 Obligations Alt-Ergo (0.95.1) CVC3 (2.2) CVC3 (2.4.1) CVC4 (1.2) Coq (8.4pl2) Eprover (1.6) Vampire (0.6) Z3 (3.2) Z3 (4.3.1) monotonicity --- --- --- --- --- --- --- --- --- induction_ty_lex 1. --- --- --- --- --- --- --- --- --- split_goal_wp 1. 0.04 0.06 0.08 --- --- --- --- 0.09 0.10 2. Timeout (5s) Timeout (5s) Timeout (5s) --- 1.67 --- --- Timeout (5s) Timeout (5s) 3. 0.06 0.11 0.14 --- --- --- --- Timeout (5s) Timeout (5s) 4. --- --- 0.24 Timeout (5s) 1.64 --- --- --- Timeout (5s) 5. Timeout (5s) 0.07 0.09 --- --- --- --- Timeout (5s) Timeout (5s) 6. Timeout (5s) Timeout (5s) Timeout (5s) --- 1.16 --- --- Timeout (5s) Timeout (5s) distrib_conj --- --- --- --- --- --- --- --- --- induction_ty_lex 1. --- --- --- --- --- --- --- --- --- split_goal_wp 1. 0.06 0.06 0.07 --- --- --- --- Timeout (5s) Timeout (5s) 2. 6.07 Timeout (5s) Timeout (5s) --- 2.03 --- --- Timeout (5s) Timeout (5s) 3. Timeout (5s) Timeout (5s) Timeout (5s) --- 1.62 --- --- Timeout (5s) Timeout (5s) 4. 0.96 0.58 Timeout (5s) 0.08 --- --- --- Timeout (5s) Timeout (5s) 5. 0.40 0.27 0.27 --- --- --- --- Timeout (5s) Timeout (5s) 6. Timeout (5s) Timeout (5s) Timeout (5s) --- 1.31 --- --- Timeout (5s) Timeout (5s) wp_preserved_by_reduction --- --- --- --- 4.74 --- --- --- --- progress --- --- --- --- --- --- --- --- --- induction_ty_lex 1. --- --- --- --- --- --- --- --- --- split_goal_wp 1. 0.04 0.05 0.06 --- --- --- --- 0.00 0.00 2. Timeout (5s) Timeout (5s) Timeout (5s) --- 1.17 --- --- Timeout (5s) Timeout (5s) 3. Timeout (5s) Timeout (5s) Timeout (5s) --- 1.56 --- --- Timeout (5s) Timeout (5s) 4. Timeout (5s) --- Timeout (5s) Timeout (5s) 1.45 --- --- Timeout (5s) Timeout (5s) 5. --- 0.31 --- --- 1.15 0.20 0.34 --- --- 6. Timeout (5s) Timeout (5s) Timeout (5s) --- 1.19 --- --- Timeout (5s) Timeout (5s) wp_soundness Timeout (5s) Timeout (5s) Timeout (5s) --- 1.27 --- --- Timeout (5s) Timeout (5s)