Copyright | (c) Ben Selfridge 2020 |
---|---|
Maintainer | benselfridge@galois.com |
Stability | experimental |
Portability | POSIX |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
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.
Synopsis
- prove :: Solver -> Spec -> IO [(Name, SatResult)]
- data Solver
- data SatResult
- computeBisimulationProofBundle :: IsInterpretedFloatSymExprBuilder sym => sym -> [String] -> Spec -> IO (BisimulationProofBundle sym)
- data BisimulationProofBundle sym = BisimulationProofBundle {
- initialStreamState :: BisimulationProofState sym
- preStreamState :: BisimulationProofState sym
- postStreamState :: BisimulationProofState sym
- externalInputs :: [(Name, Some Type, XExpr sym)]
- triggerState :: [(Name, Pred sym, [(Some Type, XExpr sym)])]
- assumptions :: [Pred sym]
- sideConds :: [Pred sym]
- newtype BisimulationProofState sym = BisimulationProofState {
- streamState :: [(Id, Some Type, [XExpr sym])]
- data XExpr sym where
- 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
Proving properties about Copilot specifications
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.
The prove
function returns results of this form for each property in a
spec.
Bisimulation proofs about copilot-c99
code
computeBisimulationProofBundle Source #
:: 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 Source #
A collection of all of the symbolic states necessary to carry out a bisimulation proof.
BisimulationProofBundle | |
|
newtype BisimulationProofState sym Source #
The state of a bisimulation proof at a particular step.
BisimulationProofState | |
|
What4 representations of Copilot expressions
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.
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 |