Copilot.Theorem.What4

Spec properties are translated into the language of SMT solvers using What4. A backend solver is then used to prove the property is true. The technique is sound, but incomplete. If a property is proved true by this technique, then it can be guaranteed to be true. However, if a property is not proved true, that does not mean it isn't true; the proof may fail because the given property is not inductive.

We perform k-induction on all the properties in a given specification where k is chosen to be the maximum amount of delay on any of the involved streams. This is a heuristic choice, but often effective.

Proving properties about Copilot specifications

prove

Arguments

:: Solver

Solver to use

-> Spec

Spec

-> IO [(Name, SatResult)]

Attempt to prove all of the properties in a spec via an SMT solver (which must be installed locally on the host). Return an association list mapping the names of each property to the result returned by the solver.

data Solver

The solvers supported by the what4 backend.

Constructors

CVC4

DReal

Yices

Z3

data SatResult

The prove function returns results of this form for each property in a spec.

Constructors

Valid

Invalid

Unknown

Instances

Show SatResult

Defined in Copilot.Theorem.What4

Methods

showsPrec :: Int -> SatResult -> ShowS

show :: SatResult -> String

showList :: [SatResult] -> ShowS

Bisimulation proofs about copilot-c99 code

computeBisimulationProofBundle

Arguments

:: IsInterpretedFloatSymExprBuilder sym

=> sym

-> [String]

Names of properties to assume during verification

-> Spec

The input Copilot specification

-> IO (BisimulationProofBundle sym)

Given a Copilot specification, compute all of the symbolic states necessary to carry out a bisimulation proof that establishes a correspondence between the states of the Copilot stream program and the C code that copilot-c99 would generate for that Copilot program.

data BisimulationProofBundle sym

A collection of all of the symbolic states necessary to carry out a bisimulation proof.

Constructors

BisimulationProofBundle

Fields

• initialStreamState :: BisimulationProofState sym

  The state of the global variables at program startup

• preStreamState :: BisimulationProofState sym

  The stream state prior to invoking the step function

• postStreamState :: BisimulationProofState sym

  The stream state after invoking the step function

• externalInputs :: [(Name, Some Type, XExpr sym)]

  A list of external streams, where each tuple contains:

  1. The name of the stream
  2. The type of the stream
  3. The value of the stream represented as a fresh constant
• triggerState :: [(Name, Pred sym, [(Some Type, XExpr sym)])]

  A list of trigger functions, where each tuple contains:

  1. The name of the function
  2. A formula representing the guarded condition
  3. The arguments to the function, where each argument is represented as a type-value pair
• assumptions :: [Pred sym]

  User-provided property assumptions

• sideConds :: [Pred sym]

  Side conditions related to partial operations

newtype BisimulationProofState sym

The state of a bisimulation proof at a particular step.

Constructors

BisimulationProofState

Fields

• streamState :: [(Id, Some Type, [XExpr sym])]

  A list of tuples containing:

  1. The name of a stream
  2. The type of the stream
  3. The list of values in the stream description

What4 representations of Copilot expressions

data XExpr sym where

The What4 representation of a copilot expression. We do not attempt to track the type of the inner expression at the type level, but instead lump everything together into the XExpr sym type. The only reason this is a GADT is for the array case; we need to know that the array length is strictly positive.

Constructors

XBool :: SymExpr sym BaseBoolType -> XExpr sym

XInt8 :: SymExpr sym (BaseBVType 8) -> XExpr sym

XInt16 :: SymExpr sym (BaseBVType 16) -> XExpr sym

XInt32 :: SymExpr sym (BaseBVType 32) -> XExpr sym

XInt64 :: SymExpr sym (BaseBVType 64) -> XExpr sym

XWord8 :: SymExpr sym (BaseBVType 8) -> XExpr sym

XWord16 :: SymExpr sym (BaseBVType 16) -> XExpr sym

XWord32 :: SymExpr sym (BaseBVType 32) -> XExpr sym

XWord64 :: SymExpr sym (BaseBVType 64) -> XExpr sym

XFloat :: SymExpr sym (SymInterpretedFloatType sym SingleFloat) -> XExpr sym

XDouble :: SymExpr sym (SymInterpretedFloatType sym DoubleFloat) -> XExpr sym

XEmptyArray :: XExpr sym

XArray :: 1 <= n => Vector n (XExpr sym) -> XExpr sym

XStruct :: [XExpr sym] -> XExpr sym

Instances

IsExprBuilder sym => Show (XExpr sym)

Defined in Copilot.Theorem.What4.Translate

Methods

showsPrec :: Int -> XExpr sym -> ShowS

show :: XExpr sym -> String

showList :: [XExpr sym] -> ShowS