Cabal-version: 2.2
Name:          copilot-verifier
Version:       3.19
Author:        Galois Inc.
Maintainer:    rscott@galois.com
Copyright:     (c) Galois, Inc 2021-2024
License:       BSD-3-Clause
License-file:  LICENSE
Build-type:    Simple
Category:      Language
Synopsis:      System for verifying the correctness of generated Copilot programs
Description:
  @copilot-verifier@ is an add-on to the [Copilot Stream
  DSL](https://copilot-language.github.io) for verifying the correctness of C
  code generated by the @copilot-c99@ package.
  .
  @copilot-verifier@ uses the [Crucible symbolic
  simulator](https://github.com/galoisinc/crucible) to interpret the semantics
  of the generated C program and and to produce verification conditions
  sufficient to guarantee that the meaning of the generated program corresponds
  in a precise way to the meaning of the original stream specification. The
  generated verification conditions are then dispatched to SMT solvers to be
  automatically solved.
extra-doc-files: CHANGELOG, README.md

source-repository head
  type:     git
  location: https://github.com/GaloisInc/copilot-verifier
  subdir:   copilot-verifier

common bldflags
  ghc-options: -Wall
               -Werror=incomplete-patterns
               -Werror=missing-methods
               -Werror=overlapping-patterns
               -Wpartial-fields
               -Wincomplete-uni-patterns
  ghc-prof-options: -O2 -fprof-auto-exported
  default-language: Haskell2010
  default-extensions:
     NondecreasingIndentation
  build-depends:
    aeson >= 1.5 && < 2.3,
    base >= 4.8 && < 4.18,
    bv-sized >= 1.0.0 && < 1.1,
    bytestring,
    containers >= 0.5.9.0,
    copilot >= 3.19 && < 3.20,
    copilot-c99 >= 3.19 && < 3.20,
    copilot-core >= 3.19 && < 3.20,
    copilot-libraries >= 3.19 && < 3.20,
    copilot-language >= 3.19 && < 3.20,
    copilot-prettyprinter >= 3.19 && < 3.20,
    copilot-theorem >= 3.19 && < 3.20,
    crucible >= 0.7 && < 0.8,
    crucible-llvm >= 0.6 && < 0.7,
    crux >= 0.7 && < 0.8,
    crux-llvm >= 0.8 && < 0.9,
    filepath,
    lens,
    llvm-pretty,
    mtl,
    panic >= 0.3,
    parameterized-utils >= 2.1.4 && < 2.2,
    prettyprinter >= 1.7.0,
    text,
    transformers,
    vector,
    what4 >= 0.4

library
  import: bldflags

  hs-source-dirs: src
  exposed-modules:
    Copilot.Verifier
    Copilot.Verifier.Log

library copilot-verifier-examples
  import: bldflags

  hs-source-dirs: examples
  build-depends:
    case-insensitive,
    copilot-verifier
  exposed-modules:
    Copilot.Verifier.Examples

    Copilot.Verifier.Examples.ShouldFail.Partial.AbsIntMin
    Copilot.Verifier.Examples.ShouldFail.Partial.AddSignedWrap
    Copilot.Verifier.Examples.ShouldFail.Partial.DivByZero
    Copilot.Verifier.Examples.ShouldFail.Partial.IndexOutOfBounds
    Copilot.Verifier.Examples.ShouldFail.Partial.ModByZero
    Copilot.Verifier.Examples.ShouldFail.Partial.MulSignedWrap
    Copilot.Verifier.Examples.ShouldFail.Partial.ShiftLTooLarge
    Copilot.Verifier.Examples.ShouldFail.Partial.ShiftRTooLarge
    Copilot.Verifier.Examples.ShouldFail.Partial.SubSignedWrap

    Copilot.Verifier.Examples.ShouldPass.Array
    Copilot.Verifier.Examples.ShouldPass.ArrayGen
    Copilot.Verifier.Examples.ShouldPass.ArrayOfStructs
    Copilot.Verifier.Examples.ShouldPass.ArrayTriggerArgument
    Copilot.Verifier.Examples.ShouldPass.Arith
    Copilot.Verifier.Examples.ShouldPass.Clock
    Copilot.Verifier.Examples.ShouldPass.Counter
    Copilot.Verifier.Examples.ShouldPass.Engine
    Copilot.Verifier.Examples.ShouldPass.FPOps
    Copilot.Verifier.Examples.ShouldPass.Heater
    Copilot.Verifier.Examples.ShouldPass.IntOps
    Copilot.Verifier.Examples.ShouldPass.Partial.AbsIntMin
    Copilot.Verifier.Examples.ShouldPass.Partial.AddSignedWrap
    Copilot.Verifier.Examples.ShouldPass.Partial.DivByZero
    Copilot.Verifier.Examples.ShouldPass.Partial.IndexOutOfBounds
    Copilot.Verifier.Examples.ShouldPass.Partial.ModByZero
    Copilot.Verifier.Examples.ShouldPass.Partial.MulSignedWrap
    Copilot.Verifier.Examples.ShouldPass.Partial.ShiftLTooLarge
    Copilot.Verifier.Examples.ShouldPass.Partial.ShiftRTooLarge
    Copilot.Verifier.Examples.ShouldPass.Partial.SubSignedWrap
    Copilot.Verifier.Examples.ShouldPass.Structs
    Copilot.Verifier.Examples.ShouldPass.Voting
    Copilot.Verifier.Examples.ShouldPass.WCV

executable verify-examples
  import: bldflags

  hs-source-dirs: exe
  main-is: VerifyExamples.hs
  build-depends:
    case-insensitive,
    copilot-verifier,
    copilot-verifier-examples,
    optparse-applicative

test-suite copilot-verifier-test
  import: bldflags

  type: exitcode-stdio-1.0
  hs-source-dirs: test
  build-depends:
    case-insensitive,
    copilot-verifier,
    copilot-verifier-examples,
    silently >= 1.2,
    tasty >= 0.10,
    tasty-expected-failure >= 0.12,
    tasty-hunit >= 0.10
  main-is: Test.hs