Why3 certificates for Cubicle

Table of Contents

Cubicle can generate certificates in Why3's input language. The system is described as a transition relation in first order logic (predicate tau) and relates symbols that materialize the values of the variables before and after execution of the transition relation.

Another special predicate characterizes the initial states: predicate init.

1 Example: Bakery

A certificate is composed of several theories.

A theory defines the types and function symbols used to expressed the system. 

theory Bakery_defs

use import int.Int

type t = Idle | Wait | Crit | Crash

function a int : t
function a' int : t

end

Another one describes the system. Here we have three transitions, and tau is defined as the disjunction of those. 

theory Bakery_trdefs

use import int.Int
use import Bakery_defs

predicate transition__tr3 =
(* transition tr3 *)
(exists z:int. 
( (* requires *)
(a z) = Crit) /\
( (* actions *)
(forall j:int.
if j = z then
 a' j = Idle
else a' j = (a j))))


predicate transition__tr2 =
(* transition tr2 *)
(exists z:int. 
( (* requires *)
(a z) = Wait) /\
( (* actions *)
(forall j:int.
if j = z then
 a' j = Crit
else if z < j then
 a' j = (a j)
else if j < z /\
(a j) = Idle then
 a' j = Idle
else a' j = Crash)))


predicate transition__tr1 =
(* transition tr1 *)
(exists z:int. 
( (* requires *)
(a z) = Idle) /\
( (* actions *)
(forall j:int.
if j = z then
 a' j = Wait
else if j < z then
 a' j = (a j)
else if z < j /\
(a j) = Idle then
 a' j = (a j)
else a' j = Crash)))


predicate tau =
(transition__tr1 \/ transition__tr2 \/ transition__tr3)


end

The inductive invariant of the system is defined by yet another theory. 

theory Bakery_invpreds

use import int.Int
use import Bakery_defs

predicate invariant1 =
not (exists z1 z2:int. z1 <> z2 /\ (a z1) = Crit /\
(a z2) = Crit)

predicate invariant1' =
not (exists z1 z2:int. z1 <> z2 /\ (a' z1) = Crit /\
(a' z2) = Crit)

predicate invariant3 =
not (exists z1 z2:int. z1 <> z2 /\ z2 < z1 /\
(a z1) = Crit /\
(a z2) = Wait)

predicate invariant3' =
not (exists z1 z2:int. z1 <> z2 /\ z2 < z1 /\
(a' z1) = Crit /\
(a' z2) = Wait)

end

The verification of the certificate is then expressed as three goals (each in their own theory to keep the logical context separated) that amounts to an inductive proof of the original property.

Intermediate lemmas are also produced by Cubicle to help (greatly) the solver prove the preservation of the inductive invariant. 

theory Bakery_initialisation

use import int.Int
use import Bakery_defs
use import Bakery_invpreds

predicate init =
    forall z:int. ((a z) = Idle)

goal initialisation:
    init -> (invariant3 /\ invariant1)

end


theory Bakery_property

use import int.Int
use import Bakery_defs
use import Bakery_invpreds

goal property:
    (invariant3 /\ invariant1) -> (not (exists z1 z2:int. z1 <> z2 /\ (a z1) = Crit /\
(a z2) = Crit))

end


theory Bakery_hint_1

use import int.Int
use import Bakery_defs
use import Bakery_invpreds
use import Bakery_trdefs

lemma hint_1:
    (invariant1 /\ invariant3 /\ tau)
    -> invariant1'

end


theory Bakery_hint_2

use import int.Int
use import Bakery_defs
use import Bakery_invpreds
use import Bakery_trdefs

lemma hint_2:
    (invariant3 /\ tau)
    -> invariant3'

end


theory Bakery_preservation

use import int.Int
use import Bakery_defs
use import Bakery_invpreds
use import Bakery_trdefs
use import Bakery_hint_2
use import Bakery_hint_1

goal preservation:
    (invariant3 /\ invariant1 /\ tau)
    ->
    (invariant3' /\ invariant1')

end

2 Results

The following table gives an overview of the results of our certification process for a number of benchmarks. Each certificate is accessible (excepted hirr_pvcoherence for IP reasons) as well as the report generated by Why3 for the verification. Notice that all proofs are performed automatically.

Certificate Why3 report
Bakery ./bakery_certif/why3session.html
Bakery ./bakery_certif/why3session.html
Flash_abstr ./flash_abstr_certif/why3session.html
Flash_nodata ./flash_nodata_certif/why3session.html
German.ctc ./german.ctc_certif/why3session.html
German_baukus ./german_baukus_certif/why3session.html
German_pfs ./german_pfs_certif/why3session.html
Hirr_pvcoherence_abstrdata ./hirr_pvcoherence_abstrdata_certif/why3session.html
Hirr_pvcoherence_nodata ./hirr_pvcoherence_nodata_certif/why3session.html
Ricart_abdulla_int ./ricart_abdulla_int_certif/why3session.html
Szymanski_at ./szymanski_at_certif/why3session.html
Szymanski_na ./szymanski_na_certif/why3session.html

The original cubicle files are available on Cubicle's website or are distributed as examples with the sources of Cubicle.