-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | System for verifying the correctness of generated Copilot programs
--   
--   <tt>copilot-verifier</tt> is an add-on to the <a>Copilot Stream
--   DSL</a> for verifying the correctness of C code generated by the
--   <tt>copilot-c99</tt> package.
--   
--   <tt>copilot-verifier</tt> uses the <a>Crucible symbolic simulator</a>
--   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.
@package copilot-verifier
@version 4.2


-- | This will fail to verify since the verification does not assume the
--   <tt>notIntMin</tt> property, which is needed to prevent undefined
--   behavior when invoking the <a>abs</a> function.
module Copilot.Verifier.Examples.ShouldFail.Partial.AbsIntMin
spec :: Spec
verifySpec :: Verbosity -> IO ()


-- | This will fail to verify since the verification does not assume the
--   <tt>notIntMax</tt> property, which is needed to prevent signed integer
--   overflow.
module Copilot.Verifier.Examples.ShouldFail.Partial.AddSignedWrap
spec :: Spec
verifySpec :: Verbosity -> IO ()


-- | This will fail to verify since the verification does not assume the
--   <tt>nonzero</tt> property, which is needed to prevent a
--   division-by-zero error.
module Copilot.Verifier.Examples.ShouldFail.Partial.DivByZero
spec :: Spec
verifySpec :: Verbosity -> IO ()


-- | This will fail to verify since the verification does not assume the
--   <tt>withinBounds</tt> property, which is needed to prevent an
--   out-of-bounds array index.
module Copilot.Verifier.Examples.ShouldFail.Partial.IndexOutOfBounds
spec :: Spec
verifySpec :: Verbosity -> IO ()


-- | This will fail to verify since the verification does not assume the
--   <tt>nonzero</tt> property, which is needed to prevent a
--   division-by-zero error.
module Copilot.Verifier.Examples.ShouldFail.Partial.ModByZero
spec :: Spec
verifySpec :: Verbosity -> IO ()


-- | This will fail to verify since the verification does not assume the
--   <tt>withinRange</tt> property, which is needed to prevent signed
--   integer underflow or overflow.
module Copilot.Verifier.Examples.ShouldFail.Partial.MulSignedWrap
spec :: Spec
verifySpec :: Verbosity -> IO ()


-- | This will fail to verify since the verification does not assume the
--   <tt>lessThanBitWidth</tt> property, which is needed to prevent
--   shifting by too large of a value.
module Copilot.Verifier.Examples.ShouldFail.Partial.ShiftLTooLarge
spec :: Spec
verifySpec :: Verbosity -> IO ()


-- | This will fail to verify since the verification does not assume the
--   <tt>lessThanBitWidth</tt> property, which is needed to prevent
--   shifting by too large of a value.
module Copilot.Verifier.Examples.ShouldFail.Partial.ShiftRTooLarge
spec :: Spec
verifySpec :: Verbosity -> IO ()


-- | This will fail to verify since the verification does not assume the
--   <tt>notIntMin</tt> property, which is needed to prevent signed integer
--   underflow.
module Copilot.Verifier.Examples.ShouldFail.Partial.SubSignedWrap
spec :: Spec
verifySpec :: Verbosity -> IO ()

module Copilot.Verifier.Examples.ShouldPass.Arith
lastPrime :: Stream Word32
multRingSpec :: Spec
verifySpec :: Verbosity -> IO ()


-- | This is a simple example for arrays. As a program, it does not make
--   much sense, however it shows of the features of arrays nicely.
module Copilot.Verifier.Examples.ShouldPass.Array
arr :: Stream (Array 2 Bool)
spec :: Spec
verifySpec :: Verbosity -> IO ()

module Copilot.Verifier.Examples.ShouldPass.ArrayGen
spec :: Spec
verifySpec :: Verbosity -> IO ()

module Copilot.Verifier.Examples.ShouldPass.ArrayOfStructs
data S
S :: Field "field" Int16 -> S
[field] :: S -> Field "field" Int16
spec :: Spec
verifySpec :: Verbosity -> IO ()
instance Copilot.Core.Type.Struct Copilot.Verifier.Examples.ShouldPass.ArrayOfStructs.S
instance Copilot.Core.Type.Typed Copilot.Verifier.Examples.ShouldPass.ArrayOfStructs.S


-- | A regression test for
--   <a>https://github.com/Copilot-Language/copilot/issues/431</a>.
module Copilot.Verifier.Examples.ShouldPass.ArrayTriggerArgument
spec :: Spec
verifySpec :: Verbosity -> IO ()


-- | Example showing usage of clocks to generate periodically recurring
--   truth values.
module Copilot.Verifier.Examples.ShouldPass.Clock

-- | We need to force a type for the argument of <a>period</a>.
p :: Word8

-- | Both have the same period, but a different phase.
clkStream :: Stream Bool
clkStream' :: Stream Bool
spec :: Spec
verifySpec :: Verbosity -> IO ()


-- | Example showing an implementation of a resettable counter.
module Copilot.Verifier.Examples.ShouldPass.Counter
counter :: (Typed a, Integral a) => Stream Bool -> Stream Bool -> Stream a
bytecounter :: Stream Int32
resetcounter :: Stream Word32
bytecounter2 :: Stream Int32
spec :: Spec
verifySpec :: Verbosity -> IO ()


-- | Example implementing an engine cooling control system.
module Copilot.Verifier.Examples.ShouldPass.Engine
engineMonitor :: Spec
verifySpec :: Verbosity -> IO ()

module Copilot.Verifier.Examples.ShouldPass.FPOps
mkSpecFor :: forall a proxy. (RealFloat a, Typed a) => proxy a -> String -> Spec
spec :: Spec
triggerOp1 :: (RealFloat a, Typed a) => String -> (Stream a -> Stream a) -> Stream a -> Spec
triggerOp2 :: (RealFloat a, Typed a) => String -> (Stream a -> Stream a -> Stream a) -> Stream a -> Spec
testOp1 :: (RealFloat a, Typed a) => (Stream a -> Stream a) -> Stream a -> Stream Bool
testOp2 :: (RealFloat a, Typed a) => (Stream a -> Stream a -> Stream a) -> Stream a -> Stream Bool
verifySpec :: Verbosity -> IO ()

module Copilot.Verifier.Examples.ShouldPass.Heater
temp :: Stream Word8
ctemp :: Stream Float
window :: Int
avgTemp :: Stream Float
spec :: Spec
verifySpec :: Verbosity -> IO ()

module Copilot.Verifier.Examples.ShouldPass.IntOps
spec :: Spec
triggerOp1 :: String -> (Stream Int16 -> Stream Int16) -> Stream Int16 -> Spec
triggerOp2 :: String -> (Stream Int16 -> Stream Int16 -> Stream Int16) -> Stream Int16 -> Stream Int16 -> Spec
testOp1 :: (Stream Int16 -> Stream Int16) -> Stream Int16 -> Stream Bool
testOp2 :: (Stream Int16 -> Stream Int16 -> Stream Int16) -> Stream Int16 -> Stream Int16 -> Stream Bool
verifySpec :: Verbosity -> IO ()


-- | This will succeed with <a>sideCondVerifierOptions</a>, as Copilot's
--   <tt>Abs</tt> operation is well defined precisely when C's <tt>abs</tt>
--   function is well defined.
module Copilot.Verifier.Examples.ShouldPass.Partial.AbsIntMin
verifySpec :: Verbosity -> IO ()


-- | This will succeed with <a>sideCondVerifierOptions</a>, as Copilot's
--   <tt>Add</tt> operation should overflow on signed integers precisely
--   when C addition does.
module Copilot.Verifier.Examples.ShouldPass.Partial.AddSignedWrap
verifySpec :: Verbosity -> IO ()


-- | This will succeed with <a>sideCondVerifierOptions</a>, as Copilot's
--   <tt>Div</tt> operation is well defined precisely when C division is
--   well defined.
module Copilot.Verifier.Examples.ShouldPass.Partial.DivByZero
verifySpec :: Verbosity -> IO ()


-- | This will succeed with <a>sideCondVerifierOptions</a>, as Copilot's
--   indexing operation should be out of bounds precisely when C array
--   indexes are out of bounds.
module Copilot.Verifier.Examples.ShouldPass.Partial.IndexOutOfBounds
verifySpec :: Verbosity -> IO ()


-- | This will succeed with <a>sideCondVerifierOptions</a>, as Copilot's
--   <tt>Mod</tt> operation is well defined precisely when C's <tt>%</tt>
--   operator is well defined.
module Copilot.Verifier.Examples.ShouldPass.Partial.ModByZero
verifySpec :: Verbosity -> IO ()


-- | This will succeed with <a>sideCondVerifierOptions</a>, as Copilot's
--   <tt>Mul</tt> operation should wrap on signed integers precisely when C
--   multiplication does.
module Copilot.Verifier.Examples.ShouldPass.Partial.MulSignedWrap
verifySpec :: Verbosity -> IO ()


-- | This will succeed with <a>sideCondVerifierOptions</a>, as Copilot's
--   <tt>BwShiftL</tt> operation should only accept second arguments as
--   large as C's <tt>&lt;&lt;</tt> operation does.
module Copilot.Verifier.Examples.ShouldPass.Partial.ShiftLTooLarge
verifySpec :: Verbosity -> IO ()


-- | This will succeed with <a>sideCondVerifierOptions</a>, as Copilot's
--   <tt>BwShiftR</tt> operation should only accept second arguments as
--   large as C's <tt>&gt;&gt;</tt> operation does.
module Copilot.Verifier.Examples.ShouldPass.Partial.ShiftRTooLarge
verifySpec :: Verbosity -> IO ()


-- | This will succeed with <a>sideCondVerifierOptions</a>, as Copilot's
--   <tt>Sub</tt> operation should underflow on signed integers precisely
--   when C subtraction does.
module Copilot.Verifier.Examples.ShouldPass.Partial.SubSignedWrap
verifySpec :: Verbosity -> IO ()


-- | An example showing the usage of the What4 backend in copilot-theorem
--   for structs and arrays. Particular focus is on nested structs. For
--   general usage of structs, refer to the general structs example.
module Copilot.Verifier.Examples.ShouldPass.Structs

-- | Definition for <a>Volts</a>.
data Volts
Volts :: Field "numVolts" Word16 -> Field "flag" Bool -> Volts
[numVolts] :: Volts -> Field "numVolts" Word16
[flag] :: Volts -> Field "flag" Bool
data Battery
Battery :: Field "temp" Word16 -> Field "volts" (Array 10 Volts) -> Field "other" (Array 10 (Array 5 Word32)) -> Battery
[temp] :: Battery -> Field "temp" Word16
[volts] :: Battery -> Field "volts" (Array 10 Volts)
[other] :: Battery -> Field "other" (Array 10 (Array 5 Word32))
spec :: Spec
verifySpec :: Verbosity -> IO ()
instance Copilot.Core.Type.Struct Copilot.Verifier.Examples.ShouldPass.Structs.Battery
instance Copilot.Core.Type.Typed Copilot.Verifier.Examples.ShouldPass.Structs.Battery
instance Copilot.Core.Type.Struct Copilot.Verifier.Examples.ShouldPass.Structs.Volts
instance Copilot.Core.Type.Typed Copilot.Verifier.Examples.ShouldPass.Structs.Volts


-- | An example showing of using <tt>copilot-verifier</tt> to verify a
--   specification involving arrays where individual elements are updated.
module Copilot.Verifier.Examples.ShouldPass.UpdateArray
spec :: Spec
verifySpec :: Verbosity -> IO ()


-- | An example showing of using <tt>copilot-verifier</tt> to verify a
--   specification involving structs where individual fields are updated.
module Copilot.Verifier.Examples.ShouldPass.UpdateStruct

-- | Definition for <a>Volts</a>.
data Volts
Volts :: Field "numVolts" Word32 -> Field "flag" Bool -> Volts
[numVolts] :: Volts -> Field "numVolts" Word32
[flag] :: Volts -> Field "flag" Bool
data Battery
Battery :: Field "temp" Word32 -> Field "volts" (Array 10 Volts) -> Field "other" (Array 10 (Array 5 Word32)) -> Battery
[temp] :: Battery -> Field "temp" Word32
[volts] :: Battery -> Field "volts" (Array 10 Volts)
[other] :: Battery -> Field "other" (Array 10 (Array 5 Word32))
spec :: Spec
verifySpec :: Verbosity -> IO ()
instance Copilot.Core.Type.Struct Copilot.Verifier.Examples.ShouldPass.UpdateStruct.Battery
instance Copilot.Core.Type.Typed Copilot.Verifier.Examples.ShouldPass.UpdateStruct.Battery
instance Copilot.Core.Type.Struct Copilot.Verifier.Examples.ShouldPass.UpdateStruct.Volts
instance Copilot.Core.Type.Typed Copilot.Verifier.Examples.ShouldPass.UpdateStruct.Volts


-- | Fault-tolerant voting examples.
module Copilot.Verifier.Examples.ShouldPass.Voting
vote :: Spec
verifySpec :: Verbosity -> IO ()


-- | This example shows an implementation of the Well-Clear Violation
--   algorithm, it follows the implementation described in 'Analysis of
--   Well-Clear Bounday Models for the Integration of UAS in the NAS',
--   <a>https://ntrs.nasa.gov/citations/20140010078</a>.
module Copilot.Verifier.Examples.ShouldPass.WCV

-- | <a>dthr</a> is the horizontal distance threshold.
dthr :: Stream Double

-- | <a>tthr</a> is the horizontal time threshold.
tthr :: Stream Double

-- | <a>zthr</a> is the vertical distance / altitude threshold.
zthr :: Stream Double

-- | <a>tcoathr</a> is the vertical time threshold.
tcoathr :: Stream Double
type Vect2 = (Stream Double, Stream Double)

-- | Multiply two Vectors.
(|*|) :: Vect2 -> Vect2 -> Stream Double

-- | Calculate the square of a vector.
sq :: Vect2 -> Stream Double

-- | Calculate the length of a vector.
norm :: Vect2 -> Stream Double

-- | Calculate the determinant of two vectors.
det :: Vect2 -> Vect2 -> Stream Double

-- | Compare two vectors, taking into account the small error that is
--   introduced by the usage of <a>Type</a>s.
(~=) :: Stream Double -> Stream Double -> Stream Bool

-- | Negate a vector.
neg :: Vect2 -> Vect2
tau :: Vect2 -> Vect2 -> Stream Double
tcpa :: Vect2 -> Vect2 -> Stream Double
taumod :: Vect2 -> Vect2 -> Stream Double
tep :: Vect2 -> Vect2 -> Stream Double
delta :: Vect2 -> Vect2 -> Stream Double -> Stream Double
theta :: Vect2 -> Vect2 -> Stream Double -> Stream Double -> Stream Double
tcoa :: Stream Double -> Stream Double -> Stream Double
dcpa :: Vect2 -> Vect2 -> Stream Double

-- | Determines if the well clear property is violated or not.
wcv :: (Vect2 -> Vect2 -> Stream Double) -> Vect2 -> Stream Double -> Vect2 -> Stream Double -> Stream Bool
verticalWCV :: Stream Double -> Stream Double -> Stream Bool
horizontalWCV :: (Vect2 -> Vect2 -> Stream Double) -> Vect2 -> Vect2 -> Stream Bool
spec :: Spec
verifySpec :: Verbosity -> IO ()

module Copilot.Verifier.Examples
shouldFailExamples :: Verbosity -> Map (CI Text) (IO ())
shouldPassExamples :: Verbosity -> Map (CI Text) (IO ())