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.
The original cubicle files are available on Cubicle's website or are distributed as examples with the sources of Cubicle.