Copilot.Verifier

Documentation

verify :: CSettings -> [String] -> String -> Spec -> IO ()

verify csettings props prefix spec verifies the Copilot specification spec under the assumptions props matches the behavior of the C program compiled with csettings within a directory prefixed by prefix.

verifyWithOptions :: VerifierOptions -> CSettings -> [String] -> String -> Spec -> IO ()

Like verify, but with VerifierOptions to more finely control the verifier's behavior.

data VerifierOptions

Options for configuring the behavior of the verifier.

Constructors

VerifierOptions

Fields

• verbosity :: Verbosity

  How much output the verifier should produce.

• assumePartialSideConds :: Bool

  If True, the verifier will determine the conditions under which a Copilot specification's partial operations are well defined and add these side conditions as assumptions. As a result, even if the generated C code performs a partial operation, the verification will succeed if this partial operation coincides with a corresponding operation on the Copilot side.

  If False, the verifier will not assume any side conditions related to partial operations in the Copilot specification. As a result, any use of a partial operation in the generated C code will cause verification to fail unless the user adds their own assumptions.

• logSmtInteractions :: Bool

  If True, create log files corresponding to the SMT solver interactions used to discharge each proof goal. The file will be named step-number-solver.smt2, where:

  • step will be either initial-step or transition-step, depending on which step of the proof the goal corresponds to.
  • number will be the number of the goal, starting at 0 and counting up. Note that each step of the proof has its own goal numbers. This means that there can be both an initial-step-0-solver.smt2 and a transition-step-0-solver.smt2, and similarly for other numbers.
  • solver is the name of the SMT solver used to discharge the proof goal. Currently, this will always be z3, although we might make this configurable in the future.

Instances

Show VerifierOptions

Defined in Copilot.Verifier

Methods

showsPrec :: Int -> VerifierOptions -> ShowS

show :: VerifierOptions -> String

showList :: [VerifierOptions] -> ShowS

defaultVerifierOptions :: VerifierOptions

The default VerifierOptions:

• Produce a reasonable amount of diagnostics as verification proceeds (Default).
• Do not assume any side conditions related to partial operations.
• Do not log any SMT solver interactions.

sideCondVerifierOptions :: VerifierOptions

Like defaultVerifierOptions, except that the verifier will assume side conditions related to partial operations used in the Copilot spec.

data Verbosity

How much output should verification produce?

The data constructors are listed in increasing order of how many diagnostics they produce.

Constructors

Quiet

Don't produce any diagnostics.

Default

Produce a reasonable amount of diagnostics as verification proceeds.

Noisy

Produce as many diagnostics as possible.

Instances

Show Verbosity

Defined in Copilot.Verifier

Methods

showsPrec :: Int -> Verbosity -> ShowS

show :: Verbosity -> String

showList :: [Verbosity] -> ShowS

Eq Verbosity

Defined in Copilot.Verifier

Methods

(==) :: Verbosity -> Verbosity -> Bool

(/=) :: Verbosity -> Verbosity -> Bool

Ord Verbosity

Defined in Copilot.Verifier

Methods

compare :: Verbosity -> Verbosity -> Ordering

(<) :: Verbosity -> Verbosity -> Bool

(<=) :: Verbosity -> Verbosity -> Bool

(>) :: Verbosity -> Verbosity -> Bool

(>=) :: Verbosity -> Verbosity -> Bool

max :: Verbosity -> Verbosity -> Verbosity

min :: Verbosity -> Verbosity -> Verbosity