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.

The solvers supported by the what4 backend.

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

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.

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.

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. AbsoluteOffsets are used in the base cases of the proof, and RelativeOffsets 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.

Exceptions that can arise when attempting a proof.

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.

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

The state of a bisimulation proof at a particular step.

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.

A Copilot value paired with its Type.

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.