# Why3 certificates for Cubicle

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.