SBV (SMT Based Verification)

If you need to reason about infinite streams (the "uniform fragment"), do not use SList. Instead, represent streams as index functions of the type Nat → a.

This approach is the only viable method for handling infinite data in the current TP architecture because it avoids the complexities of SMT sequence theory and coinduction.

Advantages

• Pointwise Equality: Equality is defined as s ≅ t := ∀i. s i ≡ t i, which results in a standard first-order ∀i goal that SMT solvers handle well.
• Trivial Uniform Laws: Operations like map become simple function compositions. For example, map f (map g s) ≅ map (f∘g) s is handled via reflexivity.
• Arithmetic Streams: Streams produced by sEnum or enumFrom (e.g., λi. base + i·step) result in closed-form arithmetic goals that are highly efficient for solvers to process.

Limitations

• Uniform Fragment Only: This method is well-suited for map, zip, and enumerations.
• Difficult Operations: Non-uniform or structural operations like filter are awkward or impossible to implement using this index-function model.

To use SBV in a REPL environment, you can load it using cabal. SBV allows you to express properties about Haskell programs and verify them using SMT solvers.

Common tasks include:

• Proving properties: Use prove to check if a property holds for all inputs.
• Finding satisfying assignments: Use sat to find inputs that make a property true.
• Optimization: Use optimize to find values that minimize or maximize a cost function subject to constraints.
• Theorem Proving: Use runTP for inductive proofs and equational reasoning.

$ cabal repl --build-depends sbv

-- Proving a property (always true for unbounded integers)
import Data.SBV
prove $ \x -> x + 1 .> (x :: SInteger)

-- Finding a satisfying model (multiplicative inverse of 3 mod 256)
sat $ \x -> x * 3 .== (1 :: SWord8)

-- Optimization example
optimize Lexicographic $ do
    x <- sInteger "x"
    y <- sInteger "y"
    constrain $ x + y .== 20
    constrain $ x .>= 5
    constrain $ y .>= 5
    minimize "cost" $ x * y

You can use user-defined algebraic data types (including enumerations, recursive, and parametric types) by making them symbolically available with mkSymbolic.

To perform pattern matching on these symbolic types, use the sCase construct (for symbolic execution) or pCase (for proof case-splits in the theorem prover). sCase supports nested pattern matching, as-patterns, guards, and wildcards. Plain case expressions inside sCase are automatically treated as symbolic case-splits.

{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE TemplateHaskell #-}

import Data.SBV

data Expr a = Val a
            | Add (Expr a) (Expr a)
            | Mul (Expr a) (Expr a)
            deriving Show

-- Make Expr symbolically available, named SExpr
mkSymbolic [''Expr]

eval :: SymVal a => (SBV a -> SBV a -> SBV a) -> (SBV a -> SBV a -> SBV a) -> SBV (Expr a) -> SBV a
eval add mul = smtFunction "eval" $ \e ->
    [sCase| e of
       Val v   -> v
       Add x y -> eval add mul x `add` eval add mul y
       Mul x y -> eval add mul x `mul` eval add mul y
    |]