copilot-theorem: k-induction for Copilot.

This is a package candidate release! Here you can preview how this package release will appear once published to the main package index (which can be accomplished via the 'maintain' link below). Please note that once a package has been published to the main package index it cannot be undone! Please consult the package uploading documentation for more information.

[maintain]

Some tools to prove properties on Copilot programs with k-induction model checking.


[Skip to ReadMe]

Properties

Versions2.2.0, 2.2.1, 3.0, 3.0
Change logNone available
Dependenciesansi-terminal (>=0.8 && <0.10), base (>=4.9 && <5), bimap (==0.3.*), containers (>=0.4 && <0.7), copilot-core (==3.0.*), data-default (==0.7.*), directory (==1.3.*), mtl (>=2.0 && <2.3), parsec (>=2.0 && <3.2), pretty (>=1.0 && <1.2), process (==1.6.*), random (==1.1.*), transformers (==0.5.*), xml (==1.3.*) [details]
LicenseBSD-3-Clause
AuthorJonathan Laurent
Maintainerjonathan.laurent@ens.fr
CategoryLanguage, Embedded
UploadedMon Apr 1 22:15:52 UTC 2019 by frankdedden

Modules

Downloads

Maintainers' corner

For package maintainers and hackage trustees


Readme for copilot-theorem-3.0

[back to package description]

Build Status

Copilot Theorem

Highly automated proof techniques are a necessary step for the widespread adoption of formal methods in the software industry. Moreover, it could provide a partial answer to one of its main issue which is scalability.

copilot-theorem is a Copilot library aimed at checking automatically some safety properties on Copilot programs. It includes:

A Tutorial

Installation instructions

copilot-theorem needs the following dependencies to be installed:

To build it, just clone this repository and use cabal install. You will find some examples in the examples folder, which can be built with cabal install too, producing an executable copilot-theorem-example in your .cabal/bin folder.

First steps

copilot-theorem is aimed at checking safety properties on Copilot programs. Intuitively, a safety property is a property which express the idea that nothing bad can happen. In particular, any invalid safety property can be disproved by a finite execution trace of the program called a counterexample. Safety properties are often opposed to liveness properties, which express the idea that something good will eventually happen. The latters are out of the scope of copilot-theorem.

Safety properties are simply expressed with standard boolean streams. In addition to triggers and observers declarations, it is possible to bind a boolean stream to a property name with the prop construct in the specification.

For instance, here is a straightforward specification declaring one property:

spec :: Spec
spec = do
  prop "gt0" (x > 0)
  where
    x = [1] ++ (1 + x)

Let's say we want to check that gt0 holds. For this, we use the prove :: Prover -> ProofScheme -> Spec -> IO () function exported by Copilot.Theorem. This function takes three arguments:

Here, we can just write

prove (lightProver def) (check "gt0") spec

where lightProver def stands for the light prover with default configuration.

The Prover interface

The Copilot.Theorem.Prover defines a general interface for provers. Therefore, it is really easy to add a new prover by creating a new object of type Prover. The latter is defined like this:

data Cex = Cex

type Infos = [String]

data Output = Output Status Infos

data Status
  = Valid
  | Invalid (Maybe Cex)
  | Unknown
  | Error

data Feature = GiveCex | HandleAssumptions

data Prover = forall r . Prover
  { proverName     :: String
  , hasFeature     :: Feature -> Bool
  , startProver    :: Core.Spec -> IO r
  , askProver      :: r -> [PropId] -> PropId -> IO Output
  , closeProver    :: r -> IO ()
  }

Each prover mostly has to provide a askProver function which takes as an argument

and checks if the assumptions logically entail the conclusion.

Two provers are provided by default: Light and Kind2.

The light prover

The light prover is a really simple prover which uses the Yices SMT solver with the QF_UFLIA theory and is limited to prove k-inductive properties, that is properties such that there exists some k such that:

For instance, in this example

spec :: Spec
spec = do
  prop "gt0"  (x > 0)
  prop "neq0" (x /= 0)
  where
    x = [1] ++ (1 + x)

the property "gt0" is inductive (1-inductive) but the property "neq0" is not.

The light prover is defined in Copilot.Theorem.Light. This module exports the lightProver :: Options -> Prover function which builds a prover from a record of type Options :

data Options = Options
  { kTimeout  :: Integer
  , onlyBmc   :: Bool
  , debugMode :: Bool }

Here,

Options is an instance of the Data.Default typeclass:

instance Default Options where
  def = Options
    { kTimeout  = 100
    , debugMode = False
    , onlyBmc   = False }

Therefore, def stands for the default configuration.

The Kind2 prover

The Kind2 prover uses the model checker with the same name, from Iowa university. It translates the Copilot specification into a modular transition system (the Kind2 native format) and then calls the kind2 executable.

It is provided by the Copilot.Theorem.Kind2 module, which exports a kind2Prover :: Options -> Prover where the Options type is defined as

data Options = Options { bmcMax :: Int }

and where bmcMax corresponds to the --bmc_max option of kind2 and is equivalent to the kTimeout option of the light prover. Its default value is 0, which stands for infinity.

Combining provers

The combine :: Prover -> Prover -> Prover function lets you merge two provers A and B into a prover C which launches both A and B and returns the most precise output. It would be interesting to implement other merging behaviours in the future. For instance, a lazy one such that C launches B only if A has returns unknown or error.

As an example, the following prover is used in Driver.hs:

prover =
  lightProver def {onlyBmc = True, kTimeout = 5}
  `combine` kind2Prover def

We will discuss the internals and the experimental results of these provers later.

Proof schemes

Let's consider again this example:

spec :: Spec
spec = do
  prop "gt0"  (x > 0)
  prop "neq0" (x /= 0)
  where
    x = [1] ++ (1 + x)

and let's say we want to prove "neq0". Currently, the two available solvers fail at showing this non-inductive property (we will discuss this limitation later). Therefore, we can prove the more general inductive lemma "gt0" and deduce our main goal from this. For this, we use the proof scheme

assert "gt0" >> check "neq0"

instead of just check "neq0". A proof scheme is chain of primitives schemes glued by the >> operator. For now, the available primitives are:

We will discuss the limitations of this tool and a way to use it in practice later.

Some examples

Some examples are in the examples folder. The Driver.hs contains the main function to run any example. Each other example file exports a specification spec and a proof scheme scheme. You can change the example being run just by changing one import directive in Driver.hs.

These examples include:

Technical details

An introduction to SMT-based model checking

An introduction to the model-checking techniques used by copilot-theorem can be found in the doc folder of this repository. It consists in a self sufficient set of slides. You can find some additional readings in the References section.

Architecture of copilot-theorem

An overview of the proving process

Each prover first translates the Copilot specification into an intermediate representation best suited for model checking. Two representations are available:

For each of these formats, there is a folder in src/Copilot/Theorem which contains at least

These three formats share a simplified set of types and operators, defined respectively in Misc.Type and Misc.Operator.

An example

The following program:

spec = do
  prop "pos" (fib > 0)

  where
    fib :: Stream Word64
    fib = [1, 1] ++ (fib + drop 1 fib)

can be translated into this IL specification:

SEQUENCES
    s0 : Int

MODEL INIT
    s0[0] = 1
    s0[1] = 1

MODEL REC
    s0[n + 2] = s0[n] + s0[n + 1]

PROPERTIES
    'pos' : s0[n] > 0

or this modular transition system:

NODE 's0' DEPENDS ON []
DEFINES
    out : Int =
        1 -> pre out.1
    out.1 : Int =
        1 -> pre out.2
    out.2 : Int =
        (out) + (out.1)

NODE 'prop-pos' DEPENDS ON [s0]
IMPORTS
    (s0 : out) as 's0.out'
    (s0 : out.1) as 's0.out.1'
    (s0 : out.2) as 's0.out.2'
DEFINES
    out : Bool =
        (s0.out) > (0)

NODE 'top' DEPENDS ON [prop-pos, s0]
IMPORTS
    (prop-pos : out) as 'pos'
    (s0 : out) as 's0.out'
    (s0 : out.1) as 's0.out.1'
    (s0 : out.2) as 's0.out.2'

PROPS
'pos' is (top : pos)

Note that the names of the streams are lost in the Copilot reification process [7] and so we have no way to keep them.

Types

In these three formats, GADTs are used to statically ensure a part of the type-corectness of the specification, in the same spirit it is done in the other Copilot libraries. copilot-theorem handles only three types which are Integer, Real and Bool and which are handled by the SMTLib standard. copilot-theorem works with pure reals and integers. Thus, it is unsafe in the sense it ignores integer overflow problems and the loss of precision due to floating point arithmetic.

The rules of translation between Copilot types and copilot-theorem types are defined in Misc/Cast.

Operators

The operators provided by Misc.Operator mostly consists in boolean connectors, linear operators, equality and inequality operators. If other operators are used in the Copilot program, they are handled using non-determinism or uninterpreted functions.

The file CoreUtils/Operators contains helper functions to translate Copilot operators into copilot-theorem operators.

The Light prover

As said in the tutorial, the light prover is a simple tool implementing the basic k-induction algorithm [1]. The Light directory contains three files:

The code is both concise and simple and should be worth a look.

The prover first translates the copilot specification into the IL format. This translation is implemented in IL.Translate. It is straightforward as the IL format does not differ a lot from the copilot core format. This is the case because the reification process has transformed the copilot program such that the ++ operator only occurs at the top of a stream definition. Therefore, each stream definition directly gives us a recurrence equation and initial conditions for the associated sequence.

The translation process mostly:

The reader is invited to use the light prover on the examples with debugMode = true, in order to have a look at the SMTLib code produced. For instance, if we check the property "pos" on the previous example involving the Fibonacci sequence, we get:

<step>  (set-logic QF_UFLIA)
<step>  (declare-fun n () Int)
<step>  (declare-fun s0 (Int) Int)
<step>  (assert (= (s0 (+ n 2)) (+ (s0 (+ n 0)) (s0 (+ n 1)))))
<step>  (assert (= (s0 (+ n 3)) (+ (s0 (+ n 1)) (s0 (+ n 2)))))
<step>  (assert (> (s0 (+ n 0)) 0))
<step>  (push 1)
<step>  (assert (or false (not (> (s0 (+ n 1)) 0))))
<step>  (check-sat)
<step>  (pop 1)
<step>  (assert (= (s0 (+ n 4)) (+ (s0 (+ n 2)) (s0 (+ n 3)))))
<step>  (assert (> (s0 (+ n 1)) 0))
<step>  (push 1)
<step>  (assert (or false (not (> (s0 (+ n 2)) 0))))
<step>  (check-sat)
unsat
<step>  (pop 1)

Here, we just kept the outputs related to the <step> psolver, which is the solver trying to prove the continuation step.

You can see that the SMT solver is used in an incremental way (push and pop instructions), so we don't need to restart it at each step of the algorithm (see [2]).

The Kind2 prover

The Kind2 prover first translates the copilot specification into a modular transition system. Then, a chain of transformations is applied to this system (for instance, in order to remove dependency cycles among nodes). After this, the system is translated into the Kind2 native format and the kind2 executable is launched. The following sections will bring more details about this process.

Modular transition systems

Let's look at the definition of a modular transition systems, in the TransSys.Spec module:

type NodeId = String
type PropId = String

data Spec = Spec
  { specNodes         :: [Node]
  , specTopNodeId     :: NodeId
  , specProps         :: Map PropId ExtVar }

data Node = Node
  { nodeId            :: NodeId
  , nodeDependencies  :: [NodeId]
  , nodeLocalVars     :: Map Var LVarDescr
  , nodeImportedVars  :: Bimap Var ExtVar
  , nodeConstrs       :: [Expr Bool] }

data Var     =  Var {varName :: String}
                deriving (Eq, Show, Ord)

data ExtVar  =  ExtVar {extVarNode :: NodeId, extVarLocalPart :: Var }
                deriving (Eq, Ord)

data VarDescr = forall t . VarDescr
  { varType :: Type t
  , varDef  :: VarDef t }

data VarDef t =
    Pre t Var
  | Expr (Expr t)
  | Constrs [Expr Bool]

data Expr t where
  Const  :: Type t -> t -> Expr t
  Ite    :: Type t -> Expr Bool -> Expr t -> Expr t -> Expr t
  Op1    :: Type t -> Op1 x t -> Expr x -> Expr t
  Op2    :: Type t -> Op2 x y t -> Expr x -> Expr y -> Expr t
  VarE   :: Type t -> Var -> Expr t

A transition system (Spec type) is mostly made of a list of nodes. A node is just a set of variables living in a local namespace and corresponding to the Var type. The ExtVar type is used to identify a variable in the global namespace by specifying both a node name and a variable. A node contains two types of variables:

The translation process

First, a copilot specification is translated into a modular transition system. This process is defined in the TransSys.Translate module. Each stream is associated to a node. The most significant task of this translation process is to flatten the copilot specification so the value of all streams at time n only depends on the values of all the streams at time n - 1, which is not the case in the Fib example shown earlier. This is done by a simple program transformation which turns this:

fib = [1, 1] ++ (fib + drop 1 fib)

into this:

fib0 = [1] ++ fib1
fib1 = [1] ++ (fib1 + fib0)

and then into the node

NODE 'fib' DEPENDS ON []
DEFINES
    out : Int =
        1 -> pre out.1
    out.1 : Int =
        1 -> pre out.2
    out.2 : Int =
        (out) + (out.1)

Once again, this flattening process is made easier by the fact that the ++ operator only occurs leftmost in a stream definition after the reification process.

Some transformations over modular transition systems

The transition system obtained by the TransSys.Translate module is perfectly consistent. However, it can't be directly translated into the Kind2 native file format. Indeed, it is natural to bind each node to a predicate but the Kind2 file format requires that each predicate only uses previously defined predicates. However, some nodes in our transition system could be mutually recursive. Therefore, the goal of the removeCycles :: Spec -> Spec function defined in TransSys.Transform is to remove such dependency cycles.

This function relies on the mergeNodes :: [NodeId] -> Spec -> Spec function which signature is self-explicit. The latter solves name conflicts by using the Misc.Renaming monad. Some code complexity has been added so the variable names remains as clear as possible after merging two nodes.

The function removeCycles computes the strongly connected components of the dependency graph and merge each one into a single node. The complexity of this process is high in the worst case (the square of the total size of the system times the size of the biggest node) but good in practice as few nodes are to be merged in most practical cases.

After the cycles have been removed, it is useful to apply another transformation which makes the translation from TransSys.Spec to Kind2.AST easier. This transformation is implemented in the complete function. In a nutshell, it transforms a system such that

After this transformation, the translation from TransSys.Spec to Kind2.AST is almost only a matter of syntax.

Bonus track

Thanks to the mergeNodes function, we can get for free the function

inline :: Spec -> Spec
inline spec = mergeNodes [nodeId n | n <- specNodes spec] spec

which discards all the structure of a modular transition system and turns it into a non-modular transition system with only one node. In fact, when translating a copilot specification to a kind2 file, two styles are available: the Kind2.toKind2 function takes a Style argument which can take the value Inlined or Modular. The only difference is that in the first case, a call to removeCycles is replaced by a call to inline.

Limitations of copilot-theorem

Now, we will discuss some limitations of the copilot-theorem tool. These limitations are organized in two categories: the limitations related to the Copilot language itself and its implementation, and the limitations related to the model-checking techniques we are using.

Limitations related to Copilot implementation

The reification process used to build the Core.Spec object looses many informations about the structure of the original Copilot program. In fact, a stream is kept in the reified program only if it is recursively defined. Otherwise, all its occurences will be inlined. Moreover, let's look at the intCounter function defined in the example Grey.hs:

intCounter :: Stream Bool -> Stream Word64
intCounter reset = time
  where
    time = if reset then 0
           else [0] ++ if time == 3 then 0 else time + 1

If n counters are created with this function, the same code will be inlined n times and the structure of the original code will be lost.

There are many problems with this:

We can't rewrite the Copilot reification process in order to avoid these inconvenients as these informations are lost by GHC itself before it occurs. The only solution we can see would be to use Template Haskell to generate automatically some structural annotations, which might not be worth the dirt introduced.

Limitations related to the model-checking techniques used

##### Limitations of the IC3 algorithm

The IC3 algorithm was shown to be a very powerful tool for hardware certification. However, the problems encountered when verifying softwares are much more complex. For now, very few non-inductive properties can be proved by Kind2 when basic integer arithmetic is involved.

The critical point of the IC3 algorithm is the counterexample generalization and the lemma tightening parts of it. When encountering a counterexample to the inductiveness (CTI) for a property, these techniques are used to find a lemma discarding it which is general enough so that all CTIs can be discarded in a finite number of steps.

The lemmas found by the current version fo Kind2 are often too weak. Some suggestions to enhance this are presented in [1]. We hope some progress will be made in this area in a near future.

A workaround to this problem would be to write kind of an interactive mode where the user is invited to provide some additional lemmas when automatic techniques fail. Another solution would be to make the properties being checked quasi-inductive by hand. In this case, copilot-theorem is still a useful tool (especially for finding bugs) but the verification of a program can be long and requires a high level of technicity.

##### Limitations related to the SMT solvers

The use of SMT solvers introduces two kind of limitations:

  1. We are limited by the computing power needed by the SMT solvers
  2. SMT solvers can't handle quantifiers efficiently

Let's consider the first point. SMT solving is costly and its performances are sometimes unpredictable. For instance, when running the SerialBoyerMoore example with the light prover, Yices2 does not terminate. However, the z3 SMT solver used by Kind2 solves the problem instantaneously. Note that this performance gap is not due to the use of the IC3 algorithm because the property to check is inductive. It could be related to the fact the SMT problem produced by the light prover uses uninterpreted functions for encoding streams instead of simple integer variables, which is the case when the copilot program is translated into a transition system. However, this wouldn't explain why the light prover still terminates instantaneously on the BoyerMoore example, which seems not simpler by far.

The second point keeps you from expressing or proving some properties universally quantified over a stream or a constant. Sometimes, this is still possible. For instance, in the Grey example, as we check a property like intCounter reset == greyCounter reset with reset an external stream (therefore totally unconstrained), we kind of show a universally quantified property. This fact could be used to enhance the proof scheme system (see the Future work section). However, this trick is not always possible. For instance, in the SerialBoyerMoore example, the property being checked should be quantified over all integer constants. Here, we can't just introduce an arbitrary constant stream because it is the quantified property which is inductive and not the property specialized for a given constant stream. That's why we have no other solution than replacing universal quantification by bounded universal quantification by assuming all the elements of the input stream are in the finite list allowed and using the function forAllCst defined in Copilot.Kind.Lib:

conj :: [Stream Bool] -> Stream Bool
conj = foldl (&&) true

forAllCst ::(Typed a) => [a] -> (Stream a -> Stream Bool) -> Stream Bool
forAllCst l f = conj $ map (f . constant) l

However, this solution isn't completely satisfying because the size of the property generated is proportionnal to the cardinal of allowed.

#### Some scalability issues

A standard way to prove large programs is to rely on its logical structure by writing a specification for each of its functions. This very natural approach is hard to follow in our case because of

Once again, copilot-theorem is still a very useful tool, especially for debugging purposes. However, we don't think it is adapted to write and check a complete specification for large scale programs.

Future work

Missing features in the Kind2 prover

These features are not currently provided due to the lack of important features in the Kind2 SMT solver.

Counterexamples displaying

Counterexamples are not displayed with the Kind2 prover because Kind2 doesn't support XML output of counterexamples. If the last feature is provided, it should be easy to implement counterexamples displaying in copilot-theorem. For this, we recommend to keep some informations about observers in TransSys.Spec and to add one variable per observer in the Kind2 output file.

Bad handling of non-linear operators and external functions

Non-linear Copilot operators and external functions are poorly handled because of the lack of support of uninterpreted functions in the Kind2 native format. A good way to handle these would be to use uninterpreted functions. With this solution, properties like

2 * sin x + 1 <= 3

with x any stream can't be proven but at least the following can be proved

let y = x in sin x == sin y

Currently, the Kind2 prover fail with the last example, as the results of unknown functions are turned into fresh unconstrained variables.

Simple extensions

The following extensions would be really simple to implement given the current architecture of Kind2.

Refactoring suggestions

More advanced enhancements

FAQ

Why does the light prover not deliver counterexamples ?

The problem is the light prover is using uninterpreted functions to represent streams and Yices2 can't give you values for uninterpreted functions when you ask it for a valid assignment. Maybe we could get better performances and easily counterexample display if we rewrite the light prover so that it works with transition systems instead of IL.

### Why does the code related to transition systems look so complex ?

It is true the code of TransSys is quite complex. In fact, it would be really straightforward to produce a flattened transition system and then a Kind2 file with just a single top predicate. In fact, It would be as easy as producing an IL specification.

To be honest, I'm not sure producing a modular Kind2 output is worth the complexity added. It's especially true at the time I write this in the sense that:

However, the current code offers some nice transformation tools (node merging, Renaming monad...) which could be useful if you intend to write a tool for simplifying or factorizing transition systems. Moreover, it becomes easier to write local transformations on transition systems as name conflicts can be avoided more easily when introducing more variables, as there is one namespace per node.

References

  1. An insight into SMT-based model checking techniques for formal software verification of synchronous dataflow programs, talk, Jonathan Laurent (see the doc folder of this repository)

  2. Scaling up the formal verification of Lustre programs with SMT-based techniques, G. Hagen, C. Tinelli

  3. SMT-based Unbounded Model Checking with IC3 and Approximate Quantifier Elimination, C. Sticksel, C. Tinelli

  4. Verifying safety properties of Lustre programs: an SMT-based approach, PhD thesis, G. Hagen

  5. Understanding IC3, Aaron R. Bradley

  6. IC3: Where Monolithic and Incremental Meet, F. Somenzi, A.R. Bradley

  7. Copilot: Monitoring Embedded Systems, L. Pike, N. Wegmann, S. Niller