copilot-theorem-4.8: k-induction for Copilot.

Copyright | (c) Ben Selfridge 2020
Maintainer | benselfridge@galois.com
Stability | experimental
Portability | POSIX
Safe Haskell | None
Language | Haskell2010

Copilot.Theorem.What4

Contents

- Proving properties about Copilot specifications
- Bisimulation proofs about `copilot-c99` code
- What4 representations of Copilot expressions

Description

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.

The functions in this module are only designed to prove universally quantified propositions (i.e., propositions that use `forAll`). Attempting to prove an existentially quantified proposition (i.e., propositions that use `exists`) will cause a `UnexpectedExistentialProposition` exception to be thrown.

Synopsis

- prove :: Solver -> Spec -> IO [(Name, SatResult)]
- data Solver
  - = CVC4
  - | DReal
  - | Yices
  - | Z3
- data SatResult
  - = Valid
  - | Invalid
  - | Unknown
- proveWithCounterExample :: Solver -> Spec -> IO [(Name, SatResultCex)]
- data SatResultCex
  - = ValidCex
  - | InvalidCex CounterExample
  - | UnknownCex
- data CounterExample = CounterExample {
  - baseCases :: [Bool]
  - inductionStep :: Bool
  - concreteExternValues :: Map (Name, StreamOffset) (Some CopilotValue)
  - concreteStreamValues :: Map (Id, StreamOffset) (Some CopilotValue)
  }
- data ProveException = UnexpectedExistentialProposition
- 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 :: forall sym. SymExpr sym BaseBoolType -> XExpr sym
  - XInt8 :: forall sym. SymExpr sym (BaseBVType 8) -> XExpr sym
  - XInt16 :: forall sym. SymExpr sym (BaseBVType 16) -> XExpr sym
  - XInt32 :: forall sym. SymExpr sym (BaseBVType 32) -> XExpr sym
  - XInt64 :: forall sym. SymExpr sym (BaseBVType 64) -> XExpr sym
  - XWord8 :: forall sym. SymExpr sym (BaseBVType 8) -> XExpr sym
  - XWord16 :: forall sym. SymExpr sym (BaseBVType 16) -> XExpr sym
  - XWord32 :: forall sym. SymExpr sym (BaseBVType 32) -> XExpr sym
  - XWord64 :: forall sym. SymExpr sym (BaseBVType 64) -> XExpr sym
  - XFloat :: forall sym. SymExpr sym (SymInterpretedFloatType sym SingleFloat) -> XExpr sym
  - XDouble :: forall sym. SymExpr sym (SymInterpretedFloatType sym DoubleFloat) -> XExpr sym
  - XEmptyArray :: forall t sym. Typed t => Type t -> XExpr sym
  - XArray :: forall (n :: Nat) sym. (KnownNat n, 1 <= n) => Vector n (XExpr sym) -> XExpr sym
  - XStruct :: forall sym. [XExpr sym] -> XExpr sym
- data CopilotValue a where
  - CopilotValue :: forall a. Typed a => Type a -> a -> CopilotValue a
- data StreamOffset
  - = AbsoluteOffset !Integer
  - | RelativeOffset !Integer

# Proving properties about Copilot specifications

prove Source #

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.

PRE: All of the properties in the `Spec` use universally quantified propositions. Attempting to supply an existentially quantified proposition will cause a `UnexpectedExistentialProposition` exception to be thrown.

data Solver Source #

The solvers supported by the what4 backend.

Constructors

CVC4 |
DReal |
Yices |
Z3 |

data SatResult Source #

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

Constructors

Valid |
Invalid |
Unknown |

#### Instances

Instances details

Show SatResult Source # |
Instance details Defined in Copilot.Theorem.What4 Methods showsPrec :: Int -> SatResult -> ShowS Source # show :: SatResult -> String Source # showList :: [SatResult] -> ShowS Source #

proveWithCounterExample Source #

Arguments

:: Solver | Solver to use
-> Spec | Spec
-> IO [(Name, SatResultCex)] |

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.

Unlike `prove`, `proveWithCounterExample` returns a `SatResultCex`. This means that if a result is invalid, then it will include a `CounterExample` which describes the circumstances under which the property was falsified. See the Haddocks for `CounterExample` for more details.

Note that this function does not currently support creating counterexamples involving struct values, so attempting to call `proveWithCounterExample` on a specification that uses structs will raise an error.

data SatResultCex Source #

The `proveWithCounterExample` function returns results of this form for each property in a spec. This is largely the same as `SatResult`, except that `InvalidCex` also records a `CounterExample`.

Constructors

ValidCex |
InvalidCex CounterExample |
UnknownCex |

#### Instances

Instances details

Show SatResultCex Source # |
Instance details Defined in Copilot.Theorem.What4 Methods showsPrec :: Int -> SatResultCex -> ShowS Source # show :: SatResultCex -> String Source # showList :: [SatResultCex] -> ShowS Source #

data CounterExample Source #

Concrete values that cause a property in a Copilot specification to be invalid. As a simple example, consider the following spec:

    spec :: Spec
    spec = do
      let s :: Stream Bool
          s = [False] ++ constant True
      void $ prop "should be invalid" (forAll s)

This defines a stream `s` where the first value is `False`, but all subsequent values are `True`'. This is used in a property that asserts that the values in `s` will be `True` at all possible time steps. This is clearly not true, given that `s`'s first value is `False`. As such, we would expect that proving this property would yield an `InvalidCex` result, where one of the base cases would state that the `s` stream contains a `False` value.

We can use the `proveWithCounterExample` function to query an SMT solver to compute a counterexample:

    CounterExample
      { baseCases =
          [False]
      , inductionStep =
          True
      , concreteExternVars =
          fromList []
      , concreteStreamValues =
          fromList
            [ ( (0, AbsoluteOffset 0), False )
            , ( (0, RelativeOffset 0), False )
            , ( (0, RelativeOffset 1), True )
            ]
      }

Let's go over what this counterexample is saying:

- The `inductionStep` of the proof is `True`, so that part of the proof was successful. On the other hand, the `baseCases` contain a `False`, so the proof was falsified when proving the base cases. (In this case, the list has only one element, so there is only a single base case.)
- `concreteStreamValues` reports the SMT solver's concrete values for each stream during relevant parts of the proof as a `Map`.

The keys of the map are pairs. The first element of the pair is the stream `Id`, and in this example, the only `Id` is `0`, corresponding to the stream `s`. The second element is the time offset. An `AbsoluteOffset` indicates an offset starting from the initial time step, and a `RelativeOffset` indicates an offset from an arbitrary point in time. `AbsoluteOffset`s are used in the base cases of the proof, and `RelativeOffset`s are used in the induction step of the proof.

The part of the map that is most interesting to us is the `( (0, `AbsoluteOffset` 0), False )` entry, which represents a base case where there is a value of `False` in the stream `s` during the initial time step. Sure enough, this is enough to falsify the property `forAll s`.

- There are no extern streams in this example, so `concreteExternVars` is empty.

We can also see an example of where a proof succeeds in the base cases, but fails during the induction step:

    spec :: Spec
    spec = do
      let t :: Stream Bool
          t = [True] ++ constant False
      void $ prop "should also be invalid" (forAll t)

With the `t` stream above, the base cases will succeed (`proveWithCounterExample` uses `k`-induction with a value of `k == 1` in this example, so there will only be a single base case). On the other hand, the induction step will fail, as later values in the stream will be `False`. If we try to `proveWithCounterExample` this property, then it will fail with:

    CounterExample
      { baseCases =
          [True]
      , inductionStep =
          False
      , concreteExternVars =
          fromList []
      , concreteStreamValues =
          fromList
            [ ( (0, AbsoluteOffset 0), True )
            , ( (0, RelativeOffset 0), True )
            , ( (0, RelativeOffset 1), False )
            ]
      }

This time, the `inductionStep` is `False`. If we look at the `concreteStreamValues`, we see the values at ``RelativeOffset` 0` and ``RelativeOffset` 1` (which are relevant to the induction step) are `True` and `False`, respectively. Since this is a proof by `k`-induction where `k == 1`, the fact that the value at `'RelativeOffset 1` is `False` indicates that the induction step was falsified.

Note that this proof does not say when exactly the time steps at ``RelativeOffset` 0` or ``RelativeOffset` 1` occur, only that that will occur relative to some arbitrary point in time. In this example, they occur relative to the initial time step, so ``RelativeOffset` 1` would occur at the second time step overall. In general, however, these time steps may occur far in the future, so it is possible that one would need to step through the execution of the streams for quite some time before finding the counterexample.

Be aware that counterexamples involving struct values are not currently supported.

Constructors

CounterExample |

Fields

- baseCases :: [Bool]

  A list of base cases in the proof, where each entry in the list corresponds to a particular time step. For instance, the first element in the list corresponds to the initial time step, the second element in the list corresponds to the second time step, and so on. A `False` entry anywhere in this list will cause the overall proof to be `InvalidCex`.

  Because the proof uses `k`-induction, the number of base cases (i.e., the number of entries in this list) is equal to the value of `k`, which is chosen using heuristics.

- inductionStep :: Bool

  Whether the induction step of the proof was valid or not. That is, given an arbitrary time step `n`, if the property is assumed to hold at time steps `n`, `n+1`, ..., `n+k`, then this will be `True` is the property can the be proven to hold at time step `n+k+1` (and `False` otherwise). If this is `False`, then the overall proof will be `InvalidCex`.

- concreteExternValues :: Map (Name, StreamOffset) (Some CopilotValue)

  The concrete values in the Copilot specification's extern streams that lead to the property being invalid.

  Each key in the `Map` is the `Name` of an extern stream paired with a `StreamOffset` representing the time step. The key's corresponding value is the concrete value of the extern stream at that time step.

- concreteStreamValues :: Map (Id, StreamOffset) (Some CopilotValue)

  The concrete values in the Copilot specification's streams (excluding extern streams) that lead to the property being invalid.

  Each key in the `Map` is the `Id` of a stream paired with a `StreamOffset` representing the time step. The key's corresponding value is the concrete value of the extern stream at that time step.

#### Instances

Instances details

Show CounterExample Source # |
Instance details Defined in Copilot.Theorem.What4 Methods showsPrec :: Int -> CounterExample -> ShowS Source # show :: CounterExample -> String Source # showList :: [CounterExample] -> ShowS Source #

data ProveException Source #

Exceptions that can arise when attempting a proof.

Constructors

UnexpectedExistentialProposition | The functions in Copilot.Theorem.What4 can only prove properties with universally quantified propositions. The functions in Copilot.Theorem.What4 will throw this exception if they encounter an existentially quantified proposition.

#### Instances

Instances details

Exception ProveException Source # |
Instance details Defined in Copilot.Theorem.What4 Methods toException :: ProveException -> SomeException Source # fromException :: SomeException -> Maybe ProveException Source # displayException :: ProveException -> String Source # backtraceDesired :: ProveException -> Bool Source #
Show ProveException Source # |
Instance details Defined in Copilot.Theorem.What4 Methods showsPrec :: Int -> ProveException -> ShowS Source # show :: ProveException -> String Source # showList :: [ProveException] -> ShowS Source #

# Bisimulation proofs about `copilot-c99` code

computeBisimulationProofBundle Source #

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.

PRE: All of the properties in the `Spec` use universally quantified propositions. Attempting to supply an existentially quantified proposition will cause a `UnexpectedExistentialProposition` exception to be thrown.

data BisimulationProofBundle sym Source #

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 Source #

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 Source #

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 :: forall sym. SymExpr sym BaseBoolType -> XExpr sym |
XInt8 :: forall sym. SymExpr sym (BaseBVType 8) -> XExpr sym |
XInt16 :: forall sym. SymExpr sym (BaseBVType 16) -> XExpr sym |
XInt32 :: forall sym. SymExpr sym (BaseBVType 32) -> XExpr sym |
XInt64 :: forall sym. SymExpr sym (BaseBVType 64) -> XExpr sym |
XWord8 :: forall sym. SymExpr sym (BaseBVType 8) -> XExpr sym |
XWord16 :: forall sym. SymExpr sym (BaseBVType 16) -> XExpr sym |
XWord32 :: forall sym. SymExpr sym (BaseBVType 32) -> XExpr sym |
XWord64 :: forall sym. SymExpr sym (BaseBVType 64) -> XExpr sym |
XFloat :: forall sym. SymExpr sym (SymInterpretedFloatType sym SingleFloat) -> XExpr sym |
XDouble :: forall sym. SymExpr sym (SymInterpretedFloatType sym DoubleFloat) -> XExpr sym |
XEmptyArray :: forall t sym. Typed t => Type t -> XExpr sym | An empty array. The `Typed` constraint and accompanying `Type` field are necessary in order to record evidence that the array type can be used in a context where `Typed` is required.
XArray :: forall (n :: Nat) sym. (KnownNat n, 1 <= n) => Vector n (XExpr sym) -> XExpr sym | A non-empty array. The `KnownNat` constraint is necessary in order to record evidence that the array type can be used in a context for `Typed` is required.
XStruct :: forall sym. [XExpr sym] -> XExpr sym |

#### Instances

Instances details

IsExprBuilder sym => Show (XExpr sym) Source # |
Instance details Defined in Copilot.Theorem.What4.Translate Methods showsPrec :: Int -> XExpr sym -> ShowS Source # show :: XExpr sym -> String Source # showList :: [XExpr sym] -> ShowS Source #

data CopilotValue a where Source #

A Copilot value paired with its `Type`.

Constructors

CopilotValue :: forall a. Typed a => Type a -> a -> CopilotValue a |

#### Instances

Instances details

ShowF CopilotValue Source # |
Instance details Defined in Copilot.Theorem.What4 Methods withShow :: p CopilotValue -> q tp -> (Show (CopilotValue tp) => a) -> a Source # showF :: CopilotValue tp -> String Source # showsPrecF :: Int -> CopilotValue tp -> String -> String Source #
Show (CopilotValue a) Source # |
Instance details Defined in Copilot.Theorem.What4 Methods showsPrec :: Int -> CopilotValue a -> ShowS Source # show :: CopilotValue a -> String Source # showList :: [CopilotValue a] -> ShowS Source #

data StreamOffset Source #

Streams expressions are evaluated in two possible modes. The "absolute" mode computes the value of a stream expression relative to the beginning of time `t=0`. The "relative" mode is useful for inductive proofs and the offset values are conceptually relative to some arbitrary, but fixed, index `j>=0`. In both cases, negative indexes are not allowed.

The main difference between these modes is the interpretation of streams for the first values, which are in the "buffer" range. For absolute indices, the actual fixed values for the streams are returned; for relative indices, uninterpreted values are generated for the values in the stream buffer. For both modes, stream values after their buffer region are defined by their recurrence expression.

Constructors

AbsoluteOffset !Integer |
RelativeOffset !Integer |

#### Instances

Instances details

Show StreamOffset Source # |
Instance details Defined in Copilot.Theorem.What4.Translate Methods showsPrec :: Int -> StreamOffset -> ShowS Source # show :: StreamOffset -> String Source # showList :: [StreamOffset] -> ShowS Source #
Eq StreamOffset Source # |
Instance details Defined in Copilot.Theorem.What4.Translate Methods (==) :: StreamOffset -> StreamOffset -> Bool Source # (/=) :: StreamOffset -> StreamOffset -> Bool Source #
Ord StreamOffset Source # |

Instance details

Defined in Copilot.Theorem.What4.Translate

Methods

compare :: StreamOffset -> StreamOffset -> Ordering Source #

(<) :: StreamOffset -> StreamOffset -> Bool Source #

(<=) :: StreamOffset -> StreamOffset -> Bool Source #

(>) :: StreamOffset -> StreamOffset -> Bool Source #

(>=) :: StreamOffset -> StreamOffset -> Bool Source #

max :: StreamOffset -> StreamOffset -> StreamOffset Source #

min :: StreamOffset -> StreamOffset -> StreamOffset Source #