copilot-theorem 3.2 → 3.2.1

raw patch · 35 files changed

+1553/−104 lines, 35 filesdep +bv-sizeddep +filepathdep +panicdep ~copilot-corePVP ok

version bump matches the API change (PVP)

Dependencies added: bv-sized, filepath, panic, parameterized-utils, what4

Dependency ranges changed: copilot-core

API changes (from Hackage documentation)

Files

• CHANGELOG +4/−0
• copilot-theorem.cabal +9/−2
• src/Copilot/Theorem.hs +11/−0
• src/Copilot/Theorem/IL.hs +8/−0
• src/Copilot/Theorem/IL/PrettyPrint.hs +4/−0
• src/Copilot/Theorem/IL/Spec.hs +37/−9
• src/Copilot/Theorem/IL/Transform.hs +7/−1
• src/Copilot/Theorem/IL/Translate.hs +7/−2
• src/Copilot/Theorem/Kind2.hs +3/−0
• src/Copilot/Theorem/Kind2/AST.hs +24/−7
• src/Copilot/Theorem/Kind2/Output.hs +5/−1
• src/Copilot/Theorem/Kind2/PrettyPrint.hs +12/−1
• src/Copilot/Theorem/Kind2/Prover.hs +9/−1
• src/Copilot/Theorem/Kind2/Translate.hs +17/−1
• src/Copilot/Theorem/Misc/Error.hs +11/−2
• src/Copilot/Theorem/Misc/SExpr.hs +44/−10
• src/Copilot/Theorem/Misc/Utils.hs +16/−2
• src/Copilot/Theorem/Prove.hs +38/−7
• src/Copilot/Theorem/Prover/Backend.hs +16/−1
• src/Copilot/Theorem/Prover/SMT.hs +69/−13
• src/Copilot/Theorem/Prover/SMTIO.hs +17/−1
• src/Copilot/Theorem/Prover/SMTLib.hs +7/−0
• src/Copilot/Theorem/Prover/TPTP.hs +7/−0
• src/Copilot/Theorem/Tactics.hs +5/−0
• src/Copilot/Theorem/TransSys.hs +9/−0
• src/Copilot/Theorem/TransSys/Cast.hs +9/−0
• src/Copilot/Theorem/TransSys/Invariants.hs +4/−0
• src/Copilot/Theorem/TransSys/Operators.hs +68/−31
• src/Copilot/Theorem/TransSys/PrettyPrint.hs +2/−0
• src/Copilot/Theorem/TransSys/Renaming.hs +22/−1
• src/Copilot/Theorem/TransSys/Spec.hs +36/−4
• src/Copilot/Theorem/TransSys/Transform.hs +31/−6
• src/Copilot/Theorem/TransSys/Translate.hs +36/−0
• src/Copilot/Theorem/TransSys/Type.hs +7/−1
• src/Copilot/Theorem/What4.hs +942/−0

@@ -1,3 +1,7 @@+2021-03-07+        * Version bump (3.2.1). (#15).+        * Completed the documentation. (#11, #14).+ 2020-12-06         * Version bump (3.2).         * Update description, bug-reports and homepage field in cabal file

@@ -14,7 +14,7 @@   <https://copilot-language.github.io>.  -version                   : 3.2+version                   : 3.2.1 license                   : BSD3 license-file              : LICENSE maintainer                : jonathan.laurent@ens.fr@@ -55,18 +55,23 @@   build-depends           : base          >= 4.9 && < 5                           , ansi-terminal >= 0.8 && < 0.10                           , bimap         >= 0.3 && < 0.4+                          , bv-sized      >= 1.0.2 && < 1.1                           , containers    >= 0.4 && < 0.7                           , data-default  >= 0.7 && < 0.8                           , directory     >= 1.3 && < 1.4+                          , filepath      >= 1.4.2 && < 1.5                           , mtl           >= 2.0 && < 2.3+                          , panic         >= 0.4.0 && < 0.5                           , parsec        >= 2.0 && < 3.2+                          , parameterized-utils >= 2.1.1 && < 2.2                           , pretty        >= 1.0 && < 1.2                           , process       >= 1.6 && < 1.7                           , random        >= 1.1 && < 1.2                           , transformers  >= 0.5 && < 0.6                           , xml           >= 1.3 && < 1.4+                          , what4         >= 1.0 && < 1.1 -                          , copilot-core  >= 3.2 && < 3.3+                          , copilot-core  >= 3.2.1 && < 3.3    exposed-modules         : Copilot.Theorem                           , Copilot.Theorem.Prove@@ -74,6 +79,7 @@                           , Copilot.Theorem.Prover.SMT                           -- , Copilot.Theorem.Prover.Z3                           , Copilot.Theorem.Kind2.Prover+                          , Copilot.Theorem.What4    other-modules           : Copilot.Theorem.Tactics @@ -107,3 +113,4 @@                           , Copilot.Theorem.TransSys.Invariants                           , Copilot.Theorem.TransSys.Operators                           , Copilot.Theorem.TransSys.Type+

@@ -2,6 +2,17 @@  {-# LANGUAGE Safe #-} +-- | Highly automated proof techniques are a necessary step for the widespread+-- adoption of formal methods in the software industry. Moreover, it could+-- provide a partial answer to one of its main issue which is scalability.+--+-- Copilot-theorem is a Copilot library aimed at checking automatically some+-- safety properties on Copilot programs. It includes:+--+-- * A prover producing native inputs for the Kind2 model checker.+--+-- * A What4 backend that uses SMT solvers to prove safety properties.+ module Copilot.Theorem   ( module X   , Proof

@@ -2,6 +2,14 @@  {-# LANGUAGE Safe #-} +-- | Each prover first translates the Copilot specification into an+-- intermediate representation best suited for model checking.+--+-- This module and the ones in the same namespace implement the IL format. A+-- Copilot program is translated into a list of quantifier-free equations over+-- integer sequences, implicitly universally quantified by a free variable n.+-- Each sequence roughly corresponds to a stream.+ module Copilot.Theorem.IL (module X) where  import Copilot.Theorem.IL.Spec as X

@@ -3,6 +3,8 @@ {-# LANGUAGE NamedFieldPuns, GADTs #-} {-# LANGUAGE Safe #-} +-- | This module implements a pretty printer for the IL format, an intermediate+-- representation used in copilot-theorem to facilitate model checking. module Copilot.Theorem.IL.PrettyPrint (prettyPrint, printConstraint) where  import Copilot.Theorem.IL.Spec@@ -13,9 +15,11 @@  -------------------------------------------------------------------------------- +-- | Pretty print an IL specification. prettyPrint :: IL -> String prettyPrint = render . ppSpec +-- | Pretty print an IL constraint expression. printConstraint :: Expr -> String printConstraint = render . ppExpr 

@@ -3,6 +3,18 @@ {-# LANGUAGE ExistentialQuantification, GADTs, LambdaCase #-} {-# LANGUAGE Safe #-} +-- | This module implements the specification language for the IL format, an+-- intermediate representation used in copilot-theorem to facilitate model+-- checking.+--+-- A Copilot program is translated into a list of quantifier-free equations+-- over integer sequences, implicitly universally quantified by a free variable+-- n. Each sequence roughly corresponds to a stream.+--+-- This representation is partly inspired by the IL language described in+-- Hagen, G.E., /VERIFYING SAFETY PROPERTIES OF LUSTRE PROGRAMS: AN SMT-BASED/+-- /APPROACH/, 2008.+ module Copilot.Theorem.IL.Spec   ( Type (..)   , Op1  (..)@@ -25,11 +37,16 @@  -------------------------------------------------------------------------------- +-- | Identifier of a sequence. type SeqId    =  String -data SeqIndex = Fixed Integer | Var Integer+-- | Index within a sequence.+data SeqIndex = Fixed Integer -- ^ An absolute index in the sequence.+              | Var Integer   -- ^ An index relative to the current time-step.   deriving (Eq, Ord, Show) +-- | Idealized types. These differ from Copilot types in that, notionally,+-- reals actually denote real numbers. data Type = Bool  | Real   | SBV8 | SBV16 | SBV32 | SBV64   | BV8  | BV16 | BV32 | BV64@@ -48,19 +65,21 @@     BV32  -> "BV32"     BV64  -> "BV64" +-- | Idealized representation of a Copilot expression. data Expr-  = ConstB Bool-  | ConstR Double-  | ConstI Type Integer-  | Ite    Type Expr Expr Expr-  | Op1    Type Op1 Expr-  | Op2    Type Op2 Expr Expr-  | SVal   Type SeqId SeqIndex-  | FunApp Type String [Expr]+  = ConstB Bool                 -- ^ Constant boolean.+  | ConstR Double               -- ^ Constant real.+  | ConstI Type Integer         -- ^ Constant integer.+  | Ite    Type Expr Expr Expr  -- ^ If-then-else.+  | Op1    Type Op1 Expr        -- ^ Apply a unary operator.+  | Op2    Type Op2 Expr Expr   -- ^ Apply a binary operator.+  | SVal   Type SeqId SeqIndex  -- ^ Refer to a value in another sequence.+  | FunApp Type String [Expr]   -- ^ Function application.   deriving (Eq, Ord, Show)  -------------------------------------------------------------------------------- +-- | A description of a variable (or function) together with its type. data VarDescr = VarDescr   { varName :: String   , varType :: Type@@ -75,13 +94,16 @@  -------------------------------------------------------------------------------- +-- | Identifier for a property. type PropId = String +-- | Description of a sequence. data SeqDescr = SeqDescr   { seqId    :: SeqId   , seqType  :: Type   } +-- | An IL specification. data IL = IL   { modelInit   :: [Expr]   , modelRec    :: [Expr]@@ -91,10 +113,12 @@  -------------------------------------------------------------------------------- +-- | Unary operators. data Op1 = Not | Neg | Abs | Exp | Sqrt | Log | Sin | Tan | Cos | Asin | Atan          | Acos | Sinh | Tanh | Cosh | Asinh | Atanh | Acosh          deriving (Eq, Ord) +-- | Binary operators. data Op2 = Eq | And | Or | Le | Lt | Ge | Gt | Add | Sub | Mul | Mod | Fdiv | Pow          deriving (Eq, Ord) @@ -145,6 +169,7 @@  ------------------------------------------------------------------------------- +-- | Return the type of an expression. typeOf :: Expr -> Type typeOf e = case e of   ConstB _       -> Bool@@ -156,12 +181,15 @@   SVal   t _ _   -> t   FunApp t _ _   -> t +-- | An index to the current element of a sequence. _n_ :: SeqIndex _n_ = Var 0 +-- | An index to a future element of a sequence. _n_plus :: (Integral a) => a -> SeqIndex _n_plus d = Var (toInteger d) +-- | Evaluate an expression at specific index in the sequence. evalAt :: SeqIndex -> Expr -> Expr evalAt _ e@(ConstB _) = e evalAt _ e@(ConstR _) = e

@@ -1,11 +1,17 @@ {-# LANGUAGE LambdaCase #-} {-# LANGUAGE Safe #-} +-- | Simplify IL expressions by partly evaluating operations on booleans. module Copilot.Theorem.IL.Transform ( bsimpl ) where  import Copilot.Theorem.IL.Spec --- | A transformation intended to remove boolean literals.+-- | Simplify IL expressions by partly evaluating operations on booleans,+-- eliminating some boolean literals.+--+-- For example, an if-then-else in which the condition is literally the+-- constant True or the constant False can be reduced to an operation without+-- choice in which the appropriate branch of the if-then-else is used instead. bsimpl :: Expr -> Expr bsimpl = until (\x -> bsimpl' x == x) bsimpl'   where

@@ -4,6 +4,7 @@              LambdaCase #-} {-# LANGUAGE Safe #-} +-- | Translate Copilot specifications into IL specifications. module Copilot.Theorem.IL.Translate ( translate, translateWithBounds ) where  import Copilot.Theorem.IL.Spec@@ -44,11 +45,13 @@  -------------------------------------------------------------------------------- --- | Translates a Copilot specification to an IL specification-+-- | Translate a Copilot specification to an IL specification. translate :: C.Spec -> IL translate = translate' False +-- | Translate a Copilot specification to an IL specification, adding+-- constraints for limiting the values of numeric expressions to known bounds+-- based on their specific types (only for integers or natural numbers). translateWithBounds :: C.Spec -> IL translateWithBounds = translate' True @@ -273,6 +276,7 @@  -------------------------------------------------------------------------------- +-- | Translation state. data TransST = TransST   { localConstraints :: [Expr]   , muxes            :: [(Expr, (Expr, Type, Expr, Expr))]@@ -299,6 +303,7 @@           , Op2 Bool Or c (Op2 Bool Eq v e2)           ] +-- | A state monad over the translation state ('TransST'). type Trans = State TransST  fresh :: Trans Integer

@@ -2,6 +2,9 @@  {-# LANGUAGE Safe #-} +-- | Copilot backend for the <https://kind2-mc.github.io/kind2/ Kind 2> SMT+-- based model checker.+ module Copilot.Theorem.Kind2 (module X) where  import Copilot.Theorem.Kind2.AST as X

@@ -2,35 +2,52 @@  {-# LANGUAGE Safe #-} +-- | Abstract syntax tree of Kind2 files. module Copilot.Theorem.Kind2.AST where  -------------------------------------------------------------------------------- +-- | A file is a sequence of predicates and propositions. data File = File   { filePreds     :: [PredDef]   , fileProps     :: [Prop] } +-- | A proposition is defined by a term. data Prop = Prop   { propName      :: String   , propTerm      :: Term } +-- | A predicate definition. data PredDef = PredDef-  { predId        :: String-  , predStateVars :: [StateVarDef]-  , predInit      :: Term-  , predTrans     :: Term }+  { predId        :: String         -- ^ Identifier for the predicate.+  , predStateVars :: [StateVarDef]  -- ^ Variables identifying the states in the+                                    -- underlying state transition system.+  , predInit      :: Term           -- ^ Predicate that holds for initial+                                    -- states.+  , predTrans     :: Term           -- ^ Predicate that holds for two states, if+                                    -- there is state transition between them.+  } +-- | A definition of a state variable. data StateVarDef = StateVarDef-  { varId         :: String-  , varType       :: Type-  , varFlags      :: [StateVarFlag] }+  { varId         :: String           -- ^ Name of the variable.+  , varType       :: Type             -- ^ Type of the variable.+  , varFlags      :: [StateVarFlag] } -- ^ Flags for the variable. +-- | Types used in Kind2 files to represent Copilot types.+--+-- The Kind2 backend provides functions to, additionally, constrain the range+-- of numeric values depending on their Copilot type ('Int8', 'Int16', etc.). data Type = Int | Real | Bool +-- | Possible flags for a state variable. data StateVarFlag = FConst +-- | Type of the predicate, either belonging to an initial state or a pair of+-- states with a transition. data PredType = Init | Trans +-- | Datatype to describe a term in the Kind language. data Term =     ValueLiteral  String   | PrimedStateVar String

@@ -3,6 +3,7 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE Safe #-} +-- | Parse output of Kind2. module Copilot.Theorem.Kind2.Output (parseOutput) where  import Text.XML.Light       hiding (findChild)@@ -15,7 +16,10 @@  simpleName s = QName s Nothing Nothing -parseOutput :: String -> String -> P.Output+-- | Parse output of Kind2.+parseOutput :: String    -- ^ Property whose validity is being checked.+            -> String    -- ^ XML output of Kind2+            -> P.Output parseOutput prop xml = fromJust $ do   root <- parseXMLDoc xml   case findAnswer . findPropTag $ root of

@@ -2,6 +2,7 @@  {-# LANGUAGE Safe #-} +-- | Pretty print a Kind2 file defining predicates and propositions. module Copilot.Theorem.Kind2.PrettyPrint ( prettyPrint ) where  import Copilot.Theorem.Misc.SExpr@@ -12,19 +13,22 @@  -------------------------------------------------------------------------------- +-- | A tree of expressions, in which the leafs are strings. type SSExpr = SExpr String +-- | Reserved keyword prime. kwPrime = "prime"  -------------------------------------------------------------------------------- +-- | Pretty print a Kind2 file. prettyPrint :: File -> String prettyPrint =   intercalate "\n\n"   . map (SExpr.toString shouldIndent id)   . ppFile --- Defines the indentation policy of the S-Expressions+-- | Define the indentation policy of the S-Expressions shouldIndent :: SSExpr -> Bool shouldIndent (Atom _)                   = False shouldIndent (List [Atom a, Atom _])    = a `notElem` [kwPrime]@@ -32,15 +36,19 @@  -------------------------------------------------------------------------------- +-- | Convert a file into a sequence of expressions. ppFile :: File -> [SSExpr] ppFile (File preds props) = map ppPredDef preds ++ ppProps props +-- | Convert a sequence of propositions into command to check each of them. ppProps :: [Prop] -> [SSExpr] ppProps ps = [ node "check-prop" [ list $ map ppProp ps ] ] +-- | Convert a proposition into an expression. ppProp :: Prop -> SSExpr ppProp (Prop n t) = list [atom n, ppTerm t] +-- | Convert a predicate into an expression. ppPredDef :: PredDef -> SSExpr ppPredDef pd =   list [ atom "define-pred"@@ -49,15 +57,18 @@        , node "init"  [ppTerm $ predInit  pd]        , node "trans" [ppTerm $ predTrans pd] ] +-- | Convert a state variable definition into an expression. ppStateVarDef :: StateVarDef -> SSExpr ppStateVarDef svd =   list [atom (varId svd), ppType (varType svd)] +-- | Convert a type into an expression. ppType :: Type -> SSExpr ppType Int  = atom "Int" ppType Real = atom "Real" ppType Bool = atom "Bool" +-- | Convert a term into an expression. ppTerm :: Term -> SSExpr ppTerm (ValueLiteral  c) = atom c ppTerm (PrimedStateVar v) = list [atom kwPrime, atom v]

@@ -3,6 +3,7 @@ {-# LANGUAGE LambdaCase #-} {-# LANGUAGE Trustworthy #-} +-- | A prover backend based on Kind2. module Copilot.Theorem.Kind2.Prover   ( module Data.Default   , Options (..)@@ -27,9 +28,13 @@  -------------------------------------------------------------------------------- +-- | Options for Kind2 data Options = Options-  { bmcMax :: Int }+  { bmcMax :: Int -- ^ Upper bound on the number of unrolling that base and+                  --   step will perform. A value of 0 means /unlimited/.+  } +-- | Default options with unlimited unrolling for base and step. instance Default Options where   def = Options { bmcMax = 0 } @@ -37,6 +42,9 @@   { options  :: Options   , transSys :: TS.TransSys } +-- | A prover backend based on Kind2.+--+-- The executable @kind2@ must exist and its location be in the @PATH@. kind2Prover :: Options -> Prover kind2Prover opts = Prover   { proverName =  "Kind2"

@@ -3,6 +3,8 @@ {-# LANGUAGE RankNTypes, ViewPatterns, NamedFieldPuns, GADTs #-} {-# LANGUAGE Safe #-} +-- | Convert modular transition systems ('TransSys') into Kind2 file+-- specifications. module Copilot.Theorem.Kind2.Translate   ( toKind2   , Style (..)@@ -36,9 +38,23 @@  -------------------------------------------------------------------------------- +-- | Style of the Kind2 files produced: modular (with multiple separate nodes),+-- or all inlined (with only one node).+--+-- In the modular style, the graph is simplified to remove cycles by collapsing+-- all nodes participating in a strongly connected components.+--+-- In the inlined style, the structure of the modular transition system is+-- discarded and the graph is first turned into a /non-modular transition/+-- /system/ with only one node, which can be then converted into a Kind2 file. data Style = Inlined | Modular -toKind2 :: Style -> [PropId] -> [PropId] -> TransSys -> K.File+-- | Produce a Kind2 file that checks the properties specified.+toKind2 :: Style     -- ^ Style of the file (modular or inlined).+        -> [PropId]  -- ^ Assumptions+        -> [PropId]  -- ^ Properties to be checked+        -> TransSys  -- ^ Modular transition system holding the system spec+        -> K.File toKind2 style assumptions checkedProps spec =   addAssumptions spec assumptions   $ trSpec (complete spec') predCallsGraph assumptions checkedProps

@@ -2,6 +2,7 @@  {-# LANGUAGE Safe #-} +-- | Custom functions to report error messages to users. module Copilot.Theorem.Misc.Error   ( badUse   , impossible@@ -12,21 +13,29 @@  -------------------------------------------------------------------------------- +-- | Tag used with error messages to help users locate the component that+-- failed or reports the error. errorHeader :: String errorHeader = "[Copilot-kind ERROR]  " -badUse :: String -> a+-- | Report an error due to an error detected by Copilot (e.g., user error).+badUse :: String -- ^ Description of the error.+       -> a badUse s = error $ errorHeader ++ s -impossible :: String -> a+-- | Report an error due to a bug in Copilot.+impossible :: String -- ^ Error information to attach to the message.+           -> a impossible s = error $ errorHeader ++ "Unexpected internal error : " ++ s +-- | Report an error due to a bug in Copilot. impossible_ :: a impossible_ = error $ errorHeader ++ "Unexpected internal error"  notHandled :: String -> a notHandled s = error $ errorHeader ++ "Not handled : " ++ s +-- | Report an unrecoverable error (e.g., incorrect format). fatal :: String -> a fatal = error 

@@ -3,6 +3,8 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE Safe #-} +-- | A representation for structured expression trees, with support for pretty+-- printing and for parsing. module Copilot.Theorem.Misc.SExpr where  import Text.ParserCombinators.Parsec@@ -12,20 +14,34 @@  -------------------------------------------------------------------------------- +-- | A structured expression is either an atom, or a sequence of expressions,+-- where the first in the sequence denotes the tag or label of the tree. data SExpr a = Atom a              | List [SExpr a] -blank        = Atom ""-atom         = Atom                 -- s-unit         = List []              -- ()+-- | Empty string expression.+blank = Atom ""++-- | Atomic expression constructor.+atom = Atom                 -- s++-- | Empty expression (empty list).+unit = List []              -- ()++-- | Single expression. singleton a  = List [Atom a]        -- (s)-list         = List                 -- (ss)-node a l     = List (Atom a : l)    -- (s ss) ---------------------------------------------------------------------------------+-- | Sequence of expressions.+list = List                 -- (ss) --- A straightforward string representation+-- | Sequence of expressions with a root or main note, and a series of+-- additional expressions or arguments..+node a l = List (Atom a : l)    -- (s ss) +--------------------------------------------------------------------------------++-- A straightforward string representation for 'SExpr's of Strings that+-- parenthesizes lists of expressions. instance Show (SExpr String) where   show = PP.render . show'     where@@ -35,13 +51,22 @@  -- More advanced printing with some basic indentation +-- | Indent by a given number. indent = nest 1 -toString :: (SExpr a -> Bool) -> (a -> String) -> SExpr a -> String+-- | Pretty print a structured expression as a String.+toString :: (SExpr a -> Bool)  -- ^ True if an expression should be indented.+         -> (a -> String)      -- ^ Pretty print the value inside as 'SExpr'.+         -> SExpr a            -- ^ Root of 'SExpr' tree.+         -> String toString shouldIndent printAtom expr =   PP.render (toDoc shouldIndent printAtom expr) -toDoc :: (SExpr a -> Bool) -> (a -> String) -> SExpr a -> Doc+-- | Pretty print a structured expression as a 'Doc', or set of layouts.+toDoc :: (SExpr a -> Bool)  -- ^ True if an expression should be indented.+      -> (a -> String)      -- ^ Pretty print the value inside as 'SExpr'.+      -> SExpr a            -- ^ Root of 'SExpr' tree.+      -> Doc toDoc shouldIndent printAtom expr = case expr of   Atom a  -> text (printAtom a)   List l  -> parens (foldl renderItem empty l)@@ -54,6 +79,11 @@  -------------------------------------------------------------------------------- +-- | Parser for strings of characters separated by spaces into a structured+-- tree.+--+-- Parentheses are interpreted as grouping elements, that is, defining a+-- 'List', which may be empty. parser :: GenParser Char st (SExpr String) parser =   choice [try unitP, nodeP, leafP]@@ -72,7 +102,11 @@                         void $ char ')'                         return $ List st -+-- | Parser for strings of characters separated by spaces into a structured+-- tree.+--+-- Parentheses are interpreted as grouping elements, that is, defining a+-- 'List', which may be empty. parseSExpr :: String -> Maybe (SExpr String) parseSExpr str = case parse parser "" str of   Left s -> error (show s) -- Nothing

@@ -2,6 +2,7 @@  {-# LANGUAGE Safe #-} +-- | Utility / auxiliary functions. module Copilot.Theorem.Misc.Utils  ( isSublistOf, nub', nubBy', nubEq  , openTempFile@@ -23,22 +24,35 @@  -------------------------------------------------------------------------------- +-- | True if the given list is a subset of the second list, when both are+-- considered as sets. isSublistOf :: Ord a => [a] -> [a] -> Bool isSublistOf = Set.isSubsetOf `on` Set.fromList +-- | True if both lists contain the same elements, when both are considered as+-- sets. nubEq :: Ord a => [a] -> [a] -> Bool nubEq = (==) `on` Set.fromList --- An efficient version of 'nub'+-- | Remove duplicates from a list.+--+-- This is an efficient version of 'Data.List.nub' that works for lists with a+-- stronger constraint on the type (i.e., 'Ord', as opposed of+-- 'Data.List.nub''s 'Eq' constraint). nub' :: Ord a => [a] -> [a] nub' = map head . group . sort +-- | Variant of 'nub'' parameterized by the comparison function. nubBy' :: (a -> a -> Ordering) -> [a] -> [a] nubBy' f = map head . groupBy (\x y -> f x y == EQ) . sortBy f  -------------------------------------------------------------------------------- -openTempFile :: String -> String -> String -> IO (String, Handle)+-- | Create a temporary file and open it for writing.+openTempFile :: String  -- ^ Directory where the file should be created.+             -> String  -- ^ Base name for the file (prefix).+             -> String  -- ^ File extension.+             -> IO (String, Handle) openTempFile loc baseName extension = do    path   <- freshPath

@@ -3,6 +3,7 @@ {-# LANGUAGE NamedFieldPuns, ViewPatterns, ExistentialQuantification, GADTs #-} {-# LANGUAGE Safe #-} +-- | Connection to theorem provers. module Copilot.Theorem.Prove   ( Output  (..)   , Status  (..)@@ -24,17 +25,24 @@  -------------------------------------------------------------------------------- +-- | Output produced by a prover, containing the 'Status' of the proof and+-- additional information. data Output = Output Status [String] +-- | Status returned by a prover when given a specification and a property to+-- prove. data Status = Sat | Valid | Invalid | Unknown | Error -{- Each prover has to provide the following five functions.-   The most important is `askProver`, which takes 3 arguments :-   *  The prover descriptor-   *  A list of properties names which are assumptions-   *  A property name which has to be deduced from these assumptions--}-+-- | A connection to a prover able to check the satisfiability of+-- specifications.+--+-- The most important is `askProver`, which takes 3 arguments :+--+-- *  The prover descriptor+--+-- *  A list of properties names which are assumptions+--+-- *  A properties that have to be deduced from these assumptions data Prover = forall r . Prover   { proverName  :: String   , startProver :: Core.Spec -> IO r@@ -42,18 +50,28 @@   , closeProver :: r -> IO ()   } +-- | A unique property identifier type PropId = String +-- | Reference to a property. data PropRef a where   PropRef :: PropId -> PropRef a +-- | Empty datatype to mark proofs of universally quantified predicates. data Universal++-- | Empty datatype to mark proofs of existentially quantified predicates. data Existential +-- | A proof scheme with unit result. type Proof a = ProofScheme a () +-- | A sequence of computations that generate a trace of required prover+-- 'Action's. type UProof = Writer [Action] () +-- | A proof scheme is a sequence of computations that compute a result and+-- generate a trace of required prover 'Action's. data ProofScheme a b where   Proof :: Writer [Action] b -> ProofScheme a b @@ -68,6 +86,7 @@   (Proof p) >>= f = Proof $ p >>= (\a -> case f a of Proof p' -> p')   return a = Proof (return a) +-- | Prover actions. data Action where   Check  :: Prover -> Action   Assume :: PropId -> Action@@ -75,9 +94,14 @@  -------------------------------------------------------------------------------- +-- | Record a requirement for satisfiability checking. check :: Prover -> Proof a check prover = Proof $ tell [Check prover] +-- | Try to prove a property in a specification with a given proof scheme.+--+-- Return 'True' if a proof of satisfiability or validity is found, false+-- otherwise. prove :: Core.Spec -> PropId -> UProof -> IO Bool prove spec propId (execWriter -> actions) = do @@ -118,6 +142,13 @@           putStrLn $ propId ++ ": admitted"           processActions (propId : context) nextActions +-- | Combine two provers producing a new prover that will run both provers in+-- parallel and combine their outputs.+--+-- The results produced by the provers must be consistent. For example, if one+-- of the provers indicates that a property is 'Valid' while another indicates+-- that it is 'Invalid', the combination of both provers will return an+-- 'Error'. combine :: Prover -> Prover -> Prover combine   (Prover { proverName  = proverNameL

@@ -1,12 +1,26 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE Safe #-} +-- | Backend to  SMT solvers and theorem provers.+--+-- This module provides three definitions:+--+-- - A class ('SmtFormat') abstracting over the language used to communicate the+-- desired commands to an SMT solver or theorem prover.+--+-- - A class ('Backend') abstracting over the backend, which includes the name of+-- the executable, any options and flags necessary, and functions to parse the+-- results and close the communication.+--+-- - A type ('SatResult') representing a satisfiability result communicated by+-- the SMT solver or theorem prover. module Copilot.Theorem.Prover.Backend (SmtFormat(..), Backend(..), SatResult(..)) where  import Copilot.Theorem.IL  import System.IO +-- | Format of SMT-Lib commands. class Show a => SmtFormat a where    push            :: a    pop             :: a@@ -15,6 +29,7 @@    declFun         :: String -> Type -> [Type] -> a    assert          :: Expr -> a +-- | Backend to an SMT solver or theorem prover. data Backend a = Backend   { name            :: String   , cmd             :: String@@ -25,5 +40,5 @@   , interpret       :: String -> Maybe SatResult   } +-- | Satisfiability result communicated by the SMT solver or theorem prover. data SatResult = Sat | Unsat | Unknown-

@@ -3,13 +3,23 @@ {-# LANGUAGE LambdaCase, NamedFieldPuns, FlexibleInstances, RankNTypes, GADTs #-} {-# LANGUAGE Trustworthy #-} +-- | Connections to various SMT solvers and theorem provers. module Copilot.Theorem.Prover.SMT-  ( module Data.Default+  (++    -- * Backends+    Backend+  , SmtFormat+  , SmtLib+  , Tptp+  , yices, dReal, altErgo, metit, z3, cvc4, mathsat++    -- * Tactics   , Options (..)   , induction, kInduction, onlySat, onlyValidity-  , yices, dReal, altErgo, metit, z3, cvc4, mathsat-  , Backend, SmtFormat-  , SmtLib, Tptp++    -- * Auxiliary+  , module Data.Default   ) where  import Copilot.Theorem.IL.Translate@@ -42,19 +52,24 @@  -------------------------------------------------------------------------------- --- | Tactics+-- * Tactics +-- | Options to configure the provers. data Options = Options   { startK :: Word32-  -- The maximum number of steps of the k-induction algorithm the prover runs-  -- before giving up.-  , maxK   :: Word32+    -- ^ Initial @k@ for the k-induction algorithm. -  -- If `debug` is set to `True`, the SMTLib/TPTP queries produced by the-  -- prover are displayed in the standard output.-  , debug  :: Bool+  , maxK :: Word32+    -- ^ The maximum number of steps of the k-induction algorithm the prover runs+    -- before giving up.++  , debug :: Bool+    -- ^ If @debug@ is set to @True@, the SMTLib/TPTP queries produced by the+    -- prover are displayed in the standard output.   } +-- | Default 'Options' with a @0@ @k@ and a max of @10@ steps, and that produce+-- no debugging info. instance Default Options where   def = Options     { startK = 0@@ -62,6 +77,7 @@     , debug  = False     } +-- | Tactic to find only a proof of satisfiability. onlySat :: SmtFormat a => Options -> Backend a -> Proof Existential onlySat opts backend = check P.Prover   { P.proverName  = "OnlySat"@@ -70,6 +86,7 @@   , P.closeProver = const $ return ()   } +-- | Tactic to find only a proof of validity. onlyValidity :: SmtFormat a => Options -> Backend a -> Proof Universal onlyValidity opts backend = check P.Prover   { P.proverName  = "OnlyValidity"@@ -78,6 +95,9 @@   , P.closeProver = const $ return ()   } +-- | Tactic to find a proof by standard 1-induction.+--+-- The values for @startK@ and @maxK@ in the options are ignored. induction :: SmtFormat a => Options -> Backend a -> Proof Universal induction opts backend = check P.Prover   { P.proverName  = "Induction"@@ -86,6 +106,7 @@   , P.closeProver = const $ return ()   } +-- | Tactic to find a proof by k-induction. kInduction :: SmtFormat a => Options -> Backend a -> Proof Universal kInduction opts backend = check P.Prover   { P.proverName  = "K-Induction"@@ -96,8 +117,13 @@  ------------------------------------------------------------------------------- --- | Backends+-- * Backends +-- | Backend to the Yices 2 SMT solver.+--+-- It enables non-linear arithmetic (@QF_NRA@), which means MCSat will be used.+--+-- The command @yices-smt2@ must be in the user's @PATH@. yices :: Backend SmtLib yices = Backend   { name            = "Yices"@@ -109,6 +135,12 @@   , interpret       = SMTLib.interpret   } +-- | Backend to the cvc4 SMT solver.+--+-- It enables support for uninterpreted functions and mixed nonlinear+-- arithmetic (@QF_NIRA@).+--+-- The command @cvc4@ must be in the user's @PATH@. cvc4 :: Backend SmtLib cvc4 = Backend   { name            = "CVC4"@@ -120,6 +152,12 @@   , interpret       = SMTLib.interpret   } +-- | Backend to the Alt-Ergo SMT solver.+--+-- It enables support for uninterpreted functions and mixed nonlinear+-- arithmetic (@QF_NIRA@).+--+-- The command @alt-ergo.opt@ must be in the user's @PATH@. altErgo :: Backend SmtLib altErgo = Backend   { name            = "Alt-Ergo"@@ -131,6 +169,9 @@   , interpret       = SMTLib.interpret   } +-- | Backend to the Z3 theorem prover.+--+-- The command @z3@ must be in the user's @PATH@. z3 :: Backend SmtLib z3 = Backend   { name            = "Z3"@@ -142,6 +183,12 @@   , interpret       = SMTLib.interpret   } +-- | Backend to the dReal SMT solver.+--+-- It enables non-linear arithmetic (@QF_NRA@).+--+-- The libraries for dReal must be installed and @perl@ must be in the user's+-- @PATH@. dReal :: Backend SmtLib dReal = Backend   { name            = "dReal"@@ -153,6 +200,11 @@   , interpret       = SMTLib.interpret   } +-- | Backend to the Mathsat SMT solver.+--+-- It enables non-linear arithmetic (@QF_NRA@).+--+-- The command @mathsat@ must be in the user's @PATH@. mathsat :: Backend SmtLib mathsat = Backend   { name            = "MathSAT"@@ -164,7 +216,11 @@   , interpret       = SMTLib.interpret   } --- The argument is the path to the "tptp" subdirectory of the metitarski+-- | Backend to the MetiTaski theorem prover.+--+-- The command @metit@ must be in the user's @PATH@.+--+-- The argument string is the path to the @tptp@ subdirectory of the metitarski -- install location. metit :: String -> Backend Tptp metit installDir = Backend

@@ -3,9 +3,13 @@ {-# LANGUAGE LambdaCase, NamedFieldPuns, RankNTypes, ViewPatterns #-} {-# LANGUAGE Safe #-} +-- | Communication with SMT solvers or theorem provers.+--+-- A solver is a running process defined by a 'Backend'. module Copilot.Theorem.Prover.SMTIO   ( Solver-  , startNewSolver, assume, entailed, stop, declVars+  , startNewSolver, stop+  , assume, entailed, declVars   ) where  import Copilot.Theorem.IL@@ -21,6 +25,7 @@  -------------------------------------------------------------------------------- +-- | A connection with a running SMT solver or theorem prover. data Solver a = Solver   { solverName :: String   , inh        :: Handle@@ -34,6 +39,7 @@  -------------------------------------------------------------------------------- +-- | Output a debugging message if debugging is enabled for the solver. debug :: Bool -> Solver a -> String -> IO () debug printName s str = when (debugMode s) $   putStrLn $ (if printName then "<" ++ solverName s ++ ">  " else "") ++ str@@ -60,6 +66,10 @@  -------------------------------------------------------------------------------- +-- | Create a new solver implemented by the backend specified.+--+-- The error handle from the backend handle is immediately closed/discarded,+-- and the logic initialized as specifiied by the backend options. startNewSolver :: SmtFormat a => String -> Bool -> Backend a -> IO (Solver a) startNewSolver name dbgMode b = do   (i, o, e, p) <- runInteractiveProcess (cmd b) (cmdOpts b) Nothing Nothing@@ -68,6 +78,8 @@   send s $ setLogic $ logic b   return s +-- | Stop a solver, closing all communication handles and terminating the+-- process. stop :: Solver a -> IO () stop s = do   hClose $ inh s@@ -76,6 +88,7 @@  -------------------------------------------------------------------------------- +-- | Register the given expressions as assumptions or axioms with the solver. assume :: SmtFormat a => Solver a -> [Expr] -> IO (Solver a) assume s@(Solver { model }) cs = do   let newAxioms = elems $ fromList cs \\ model@@ -85,6 +98,8 @@ assume' :: SmtFormat a => Solver a -> [Expr] -> IO () assume' s cs = forM_ cs (send s . assert . bsimpl) +-- | Check if a series of expressions are entailed by the axioms or assumptions+-- already registered with the solver. entailed :: SmtFormat a => Solver a -> [Expr] -> IO SatResult entailed s cs = do   when (incremental $ backend s) $ send s push@@ -97,6 +112,7 @@   when (incremental $ backend s) $ send s pop   receive s +-- | Register the given variables with the solver. declVars :: SmtFormat a => Solver a -> [VarDescr] -> IO (Solver a) declVars s@(Solver { vars }) decls = do   let newVars = elems $ fromList decls \\ vars

@@ -3,6 +3,8 @@ {-# LANGUAGE GADTs, FlexibleInstances #-} {-# LANGUAGE Safe #-} +-- | A backend to the SMT-Lib format, enabling to produce commands for SMT-Lib+-- implementing solvers, and parse results. module Copilot.Theorem.Prover.SMTLib (SmtLib, interpret) where  import Copilot.Theorem.Prover.Backend (SmtFormat (..), SatResult (..))@@ -14,6 +16,9 @@  -------------------------------------------------------------------------------- +-- | Type used to represent SMT-lib commands.+--+-- Use the interface in 'SmtFormat' to create such commands. newtype SmtLib = SmtLib (SExpr String)  instance Show SmtLib where@@ -26,6 +31,7 @@  -------------------------------------------------------------------------------- +-- | Interface for SMT-Lib conforming backends. instance SmtFormat SmtLib where   push = SmtLib $ node "push" [atom "1"]   pop = SmtLib $ node "pop" [atom "1"]@@ -36,6 +42,7 @@     node "declare-fun" [atom name, (list $ map (atom . smtTy) args), atom (smtTy retTy)]   assert c = SmtLib $ node "assert" [expr c] +-- | Parse a satisfiability result. interpret :: String -> Maybe SatResult interpret "sat"   = Just Sat interpret "unsat" = Just Unsat

@@ -3,6 +3,8 @@ {-# LANGUAGE GADTs, LambdaCase #-} {-# LANGUAGE Safe #-} +-- | A backend to <http://www.tptp.org/ TPTP>, enabling to produce assertions+-- and to parse the results from TPTP. module Copilot.Theorem.Prover.TPTP (Tptp, interpret) where  import Copilot.Theorem.Prover.Backend (SmtFormat (..), SatResult (..))@@ -12,6 +14,10 @@  -------------------------------------------------------------------------------- +-- | Type used to represent TPTP expressions.+--+-- Although this type implements the 'SmtFormat' interface, only 'assert' is+-- actually used. data Tptp = Ax TptpExpr | Null  data TptpExpr = Bin TptpExpr String TptpExpr | Un String TptpExpr@@ -37,6 +43,7 @@   declFun  = const $ const $ const Null   assert c = Ax $ expr c +-- | Parse a satisfiability result. interpret :: String -> Maybe SatResult interpret str   | "SZS status Unsatisfiable" `isPrefixOf` str = Just Unsat

@@ -1,5 +1,7 @@ {-# LANGUAGE Safe #-} +-- | Utility functions to help write proof tactics.+ module Copilot.Theorem.Tactics   ( instantiate, assume, admit   ) where@@ -8,11 +10,14 @@  import Control.Monad.Writer +-- | Instantiate a universal proof into an existential proof. instantiate :: Proof Universal -> Proof Existential instantiate (Proof p) = Proof p +-- | Assume that a property, given by reference, holds. assume :: PropRef Universal -> Proof a assume (PropRef p) = Proof $ tell [Assume p] +-- | Assume that the current goal holds. admit :: Proof a admit = Proof $ tell [Admit]

@@ -2,6 +2,15 @@  {-# LANGUAGE Safe #-} +-- | Each prover first translates the Copilot specification into an+-- intermediate representation best suited for model checking.+--+-- This module and the ones in the same namespace implement the TransSys+-- format. A Copilot program is /flattened/ and translated into a /state/+-- /transition system/.  In order to keep some structure in this+-- representation, the variables of this system are grouped by /nodes/, each+-- node exporting and importing variables. The /Kind2 prover/ uses this format,+-- which can be easily translated into the native format. module Copilot.Theorem.TransSys (module X) where  import Copilot.Theorem.TransSys.Spec as X

@@ -3,6 +3,9 @@ {-# LANGUAGE RankNTypes, ScopedTypeVariables, GADTs #-} {-# LANGUAGE Safe #-} +-- | Casting of values with dynamic types and translating from Copilot core+-- types to Copilot theorem types.+ module Copilot.Theorem.TransSys.Cast   ( Dyn   , toDyn@@ -23,8 +26,11 @@  -------------------------------------------------------------------------------- +-- | Synonym for a dynamic type in Copilot core. type Dyn = Dynamic Type +-- | Translation of a Copilot type into Copilot theorem's internal+-- representation. castedType :: Type t -> K.U K.Type castedType t = case t of   Bool    -> K.U K.Bool@@ -39,6 +45,7 @@   Float   -> K.U K.Real   Double  -> K.U K.Real +-- | Cast a dynamic value to a given type. cast :: K.Type t -> Dyn -> t cast t v   | K.Integer <- t,  Just (vi :: Integer) <- _cast v = vi@@ -46,6 +53,8 @@   | K.Real    <- t,  Just (vr :: Double)  <- _cast v = vr   | otherwise = error "Bad type cast" +-- | Apply function to a corresponding type in Copilot theorem's internal+-- representation. casting :: Type t -> (forall t' . K.Type t' -> a) -> a casting t f = case castedType t of   K.U K.Bool    -> f K.Bool

@@ -1,11 +1,14 @@ {-# OPTIONS_GHC -O0 #-} {-# LANGUAGE Safe #-} +-- | Augment types with invariants.+ module Copilot.Theorem.TransSys.Invariants   ( HasInvariants (..)   , prop   ) where +-- | Type class for types with additional invariants or contraints. class HasInvariants a where    invariants :: a -> [(String, Bool)]@@ -13,5 +16,6 @@   checkInvs :: a -> Bool   checkInvs obj = all snd $ invariants obj +-- | Creates an invariant with a description. prop :: String -> Bool -> (String, Bool) prop = (,)

@@ -4,6 +4,7 @@              RankNTypes #-} {-# LANGUAGE Safe #-} +-- | Operators in modular transition systems and their translation. module Copilot.Theorem.TransSys.Operators where  import qualified Copilot.Core as C@@ -14,6 +15,7 @@  -------------------------------------------------------------------------------- +-- | Unary operators. data Op1 a where   Not   :: Op1 Bool   Neg   :: Op1 a@@ -34,6 +36,7 @@   Atanh :: Op1 a   Acosh :: Op1 a +-- | Binary operators. data Op2 a b where   Eq     :: Op2 a    Bool   And    :: Op2 Bool Bool@@ -93,37 +96,50 @@  ------------------------------------------------------------------------------- --- | Some high level utilities to translate a Copilot operator in a standard way--- | The unhandled operators are monomorphic, and their names are labeled so--- | that each name corresponds to a unique uninterpreted function with a--- | monomorphic type.-----------------------------------------------------------------------------------+-- | Unhandled unary operator.+--+--   Unhandled operators are monomorphic, and their names are labeled so that+--   each name corresponds to a unique uninterpreted function with a+--   monomorphic type. data UnhandledOp1 = forall a b .   UnhandledOp1 String (Type a) (Type b) +-- | Unhandled binary operator.+--+--   Unhandled operators are monomorphic, and their names are labeled so that+--   each name corresponds to a unique uninterpreted function with a+--   monomorphic type. data UnhandledOp2 = forall a b c .   UnhandledOp2 String (Type a) (Type b) (Type c) +-- | Translate an Op1.+--+-- This function is parameterized so that it can be used to translate+-- in different contexts and with different targets.+--+-- 'm' is the monad in which the computation is made+--+-- 'resT' is the desired return type of the expression being translated handleOp1 ::-  -- 'm' is the monad in which the computation is made-  -- 'resT' is the desired return type of the expression being translated-  forall m expr _a _b resT. (Functor m) =>-  -- The desired return type-  Type resT ->-  -- The unary operator encountered and its argument-  (C.Op1 _a _b, C.Expr _a) ->-  -- The monadic function to translate an expression-  -- (for recursive calls to be mmadess)-  (forall t t'. Type t -> C.Expr t' -> m (expr t)) ->-  -- A function to deal with a operators not handled by copilot-kind-  (UnhandledOp1 -> m (expr resT)) ->-  -- The Op1 constructor of the 'expr' type-  (forall t . Type t -> Op1 t -> expr t -> expr t) ->+  forall m expr _a _b resT. (Functor m) -  m (expr resT)+  => Type resT+     -- ^ The desired return type +  -> (C.Op1 _a _b, C.Expr _a)+     -- ^ The unary operator encountered and its argument++  -> (forall t t'. Type t -> C.Expr t' -> m (expr t))+     -- ^ The monadic function to translate an expression++  -> (UnhandledOp1 -> m (expr resT))+      -- ^ A function to deal with a operators not handled++  -> (forall t . Type t -> Op1 t -> expr t -> expr t)+     -- ^ The Op1 constructor of the 'expr' type++  -> m (expr resT)+ handleOp1 resT (op, e) handleExpr notHandledF mkOp = case op of    C.Not      -> boolOp Not (handleExpr Bool e)@@ -181,18 +197,38 @@  -------------------------------------------------------------------------------- --- See the 'handleOp1' function for documentation+-- | Translate an Op2.+--+-- This function is parameterized so that it can be used to translate+-- in different contexts and with different targets.+--+-- 'm' is the monad in which the computation is made+--+-- 'resT' is the desired return type of the expression being translated handleOp2 ::-  forall m expr _a _b _c resT . (Monad m) =>-  Type resT ->-  (C.Op2 _a _b _c, C.Expr _a, C.Expr _b) ->-  (forall t t'. Type t -> C.Expr t' -> m (expr t)) ->-  (UnhandledOp2 -> m (expr resT)) ->-  (forall t a . Type t -> Op2 a t -> expr a -> expr a -> expr t) ->-  (expr Bool -> expr Bool) ->-  m (expr resT)+  forall m expr _a _b _c resT . (Monad m) +  => Type resT+     -- ^ The desired return type +  -> (C.Op2 _a _b _c, C.Expr _a, C.Expr _b)+     -- ^ The binary operator encountered and its arguments++  -> (forall t t'. Type t -> C.Expr t' -> m (expr t))+     -- ^ The monadic function to translate an expression++  -> (UnhandledOp2 -> m (expr resT))+      -- ^ A function to deal with a operators not handled++  -> (forall t a . Type t -> Op2 a t -> expr a -> expr a -> expr t)+     -- ^ The Op2 constructor of the 'expr' type++  -> (expr Bool -> expr Bool)+     -- ^ The Op1 for boolean negation++  -> m (expr resT)++ handleOp2 resT (op, e1, e2) handleExpr notHandledF mkOp notOp = case op of    C.And        -> boolConnector And@@ -294,6 +330,7 @@  -------------------------------------------------------------------------------- +-- | Error message for unexpected behavior / internal errors. typeErrMsg :: String typeErrMsg = "Unexpected type error in 'Misc.CoreOperators'" 

@@ -3,6 +3,7 @@ {-# LANGUAGE NamedFieldPuns, GADTs #-} {-# LANGUAGE Safe #-} +-- | Pretty print a TransSys specification as a Kind2/Lustre specification. module Copilot.Theorem.TransSys.PrettyPrint ( prettyPrint ) where  import Copilot.Theorem.TransSys.Spec@@ -19,6 +20,7 @@ indent     = nest 4 emptyLine  = text "" +-- | Pretty print a TransSys specification as a Kind2/Lustre specification. prettyPrint :: TransSys -> String prettyPrint = render . pSpec 

@@ -2,6 +2,8 @@  {-# LANGUAGE Safe #-} +-- | A monad capable of keeping track of variable renames and of providing+-- fresh names for variables. module Copilot.Theorem.TransSys.Renaming   ( Renaming   , addReservedName@@ -25,18 +27,28 @@  -------------------------------------------------------------------------------- +-- | A monad capable of keeping track of variable renames and of providing+-- fresh names for variables. type Renaming = State RenamingST +-- | State needed to keep track of variable renames and reserved names. data RenamingST = RenamingST   { _reservedNames :: Set Var   , _renaming      :: Map ExtVar Var }  -------------------------------------------------------------------------------- +-- | Register a name as reserved or used. addReservedName :: Var -> Renaming () addReservedName v = modify $ \st ->     st {_reservedNames = Set.insert v (_reservedNames st)} +-- | Produce a fresh new name based on the variable names provided.+--+-- This function will try to pick a name from the given list and, if not, will+-- use one of the names in the list as a basis for new names.+--+-- PRE: the given list cannot be empty. getFreshName :: [Var] -> Renaming Var getFreshName vs = do   usedNames <- _reservedNames <$> get@@ -48,15 +60,24 @@   addReservedName v   return v -rename :: NodeId -> Var -> Var -> Renaming ()+-- | Map a name in the global namespace to a new variable name.+rename :: NodeId  -- ^ A node Id+       -> Var     -- ^ A variable within that node+       -> Var     -- ^ A new name for the variable+       -> Renaming () rename n v v' = modify $ \st ->     st {_renaming = Map.insert (ExtVar n v) v' (_renaming st)} +-- | Return a function that maps variables in the global namespace to their new+-- names if any renaming has been registered. getRenamingF :: Renaming (ExtVar -> Var) getRenamingF = do   mapping <- _renaming <$> get   return $ \extv -> fromMaybe (extVarLocalPart extv) (Map.lookup extv mapping) +-- | Run a computation in the 'Renaming' monad, providing a result and the+-- renaming function that maps variables in the global namespace to their new+-- local names. runRenaming :: Renaming a -> (a, ExtVar -> Var) runRenaming m =   evalState st' (RenamingST Set.empty Map.empty)

@@ -3,6 +3,7 @@ {-# LANGUAGE ExistentialQuantification, GADTs, RankNTypes #-} {-# LANGUAGE Safe #-} +-- | Specification of Copilot streams as modular transition systems. module Copilot.Theorem.TransSys.Spec   ( module Copilot.Theorem.TransSys.Operators   , module Copilot.Theorem.TransSys.Type@@ -45,35 +46,56 @@  -------------------------------------------------------------------------------- +-- | Unique name that identifies a node. type NodeId = String++-- | Unique name that identifies a property. type PropId = String +-- | A modular transition system is defined by a graph of nodes and a series+-- of properties, each mapped to a variable. data TransSys = TransSys   { specNodes         :: [Node]   , specTopNodeId     :: NodeId   , specProps         :: Map PropId ExtVar } -+-- | A node is a set of variables living in a local namespace and corresponding+-- to the 'Var' type. data Node = Node   { nodeId            :: NodeId-  , nodeDependencies  :: [NodeId]-  , nodeLocalVars     :: Map Var VarDescr-  , nodeImportedVars  :: Bimap Var ExtVar+  , nodeDependencies  :: [NodeId]          -- ^ Nodes from which variables are+                                           --   imported.+  , nodeLocalVars     :: Map Var VarDescr  -- ^ Locally defined variables,+                                           --   either as the previous value of+                                           --   another variable (using 'Pre'),+                                           --   an expression involving+                                           --   variables (using 'Expr') or a+                                           --   set of constraints (using+                                           --   'Constrs').+  , nodeImportedVars  :: Bimap Var ExtVar  -- ^ Binds each imported variable to+                                           --   its local name.   , nodeConstrs       :: [Expr Bool] }  +-- | Identifer of a variable in the local (within one node) namespace. data Var      =  Var {varName :: String}   deriving (Eq, Show, Ord) +-- | Identifer of a variable in the global namespace by specifying both a node+-- name and a variable. data ExtVar   =  ExtVar {extVarNode :: NodeId, extVarLocalPart :: Var }   deriving (Eq, Ord) +-- | A description of a variable together with its type. data VarDescr = forall t . VarDescr   { varType :: Type t   , varDef  :: VarDef t } +-- | A variable definition either as a delay, an operation on variables, or+-- a constraint. data VarDef t = Pre t Var | Expr (Expr t) | Constrs [Expr Bool] +-- | A point-wise (time-wise) expression. data Expr t where   Const :: Type t -> t -> Expr t   Ite   :: Type t -> Expr Bool -> Expr t -> Expr t -> Expr t@@ -83,6 +105,7 @@  -------------------------------------------------------------------------------- +-- | Constructor for variables identifiers in the global namespace. mkExtVar node name = ExtVar node (Var name)  foldExpr :: (Monoid m) => (forall t . Expr t -> m) -> Expr a -> m@@ -97,6 +120,7 @@ foldUExpr :: (Monoid m) => (forall t . Expr t -> m) -> U Expr -> m foldUExpr f (U e) = foldExpr f e +-- | Apply an arbitrary transformation to the leafs of an expression. transformExpr :: (forall a . Expr a -> Expr a) -> Expr t -> Expr t transformExpr f = tre   where@@ -108,6 +132,8 @@  -------------------------------------------------------------------------------- +-- | The set of variables related to a node (union of the local variables and+-- the imported variables after deferencing them). nodeVarsSet :: Node -> Set Var nodeVarsSet = liftA2 Set.union   nodeLocalVarsSet@@ -157,10 +183,13 @@ specNodesIds :: TransSys -> Set NodeId specNodesIds s = Set.fromList . map nodeId $ specNodes s +-- | Given a modular transition system, produce a map from each node to its+-- dependencies. specDependenciesGraph :: TransSys -> Map NodeId [NodeId] specDependenciesGraph s =   Map.fromList [ (nodeId n, nodeDependencies n) | n <- specNodes s ] +-- | Return the top node of a modular transition system. specTopNode :: TransSys -> Node specTopNode spec = fromJust $ List.find   ((== specTopNodeId spec) . nodeId)@@ -183,6 +212,9 @@     , prop "The nodes invariants hold" $ all checkInvs (specNodes s)     ] +-- | True if the graph is topologically sorted (i.e., if the dependencies of a+-- node appear in the list of 'specNodes' before the node that depends on+-- them). isTopologicallySorted :: TransSys -> Bool isTopologicallySorted spec =   isJust $ foldM inspect Set.empty (specNodes spec)

@@ -3,6 +3,7 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE Safe #-} +-- | Helper module to manipulate and simplify TransSys graphs. module Copilot.Theorem.TransSys.Transform   ( mergeNodes   , inline@@ -39,6 +40,9 @@  -------------------------------------------------------------------------------- +-- | Merge all the given nodes, replacing all references to the given node Ids+-- with a reference to a fresh node id (unless the nodes given as argument+-- contain the top node), in which case its ID is chosen instead. mergeNodes :: [NodeId] -> TransSys -> TransSys mergeNodes toMergeIds spec =   spec@@ -70,7 +74,9 @@       , id <- nodeDependencies n       , id `notElem` toMergeIds ] -    -- All the work of renaming is done in the monad with the same name+    -- All the work of renaming is done in the 'Misc.Renaming' monad. Some code+    -- complexity has been added so the variable names remains as clear as+    -- possible after merging two nodes.     (importedVars, renamingF) = runRenaming $ do       renameLocalVars toMerge       redirectLocalImports toMerge@@ -182,9 +188,27 @@  -------------------------------------------------------------------------------- +-- | Discard all the structure of a /modular transition system/ and turn it+-- into a /non-modular transition system/ with only one node. inline :: TransSys -> TransSys inline spec = mergeNodes [nodeId n | n <- specNodes spec] spec +-- | Remove cycles by merging nodes participating in strongly connected+-- components.+--+-- The transition system obtained by the 'TransSys.Translate' module is+-- perfectly consistent. However, it can't be directly translated into the+-- /Kind2 native file format/. Indeed, it is natural to bind each node to a+-- predicate but the Kind2 file format requires that each predicate only uses+-- previously defined predicates. However, some nodes in our transition system+-- could be mutually recursive. Therefore, the goal of 'removeCycles' is to+-- remove such dependency cycles.+--+-- The function 'removeCycles' computes the strongly connected components of+-- the dependency graph and merge each one into a single node using+-- 'mergeNodes'. The complexity of this process is high in the worst case (the+-- square of the total size of the system times the size of the biggest node)+-- but good in practice as few nodes are to be merged in most practical cases. removeCycles :: TransSys -> TransSys removeCycles spec =   topoSort $ foldr mergeComp spec (buildScc nodeId $ specNodes spec)@@ -202,11 +226,12 @@  -------------------------------------------------------------------------------- --- | Completes each node of a specification with imported variables such--- | that each node contains a copy of all its dependencies--- | The given specification should have its node sorted by topological--- | order.--- | The top nodes should have all the other nodes as its dependencies+-- | Completes each node of a specification with imported variables such that+-- each node contains a copy of all its dependencies.+--+-- The given specification should have its node sorted by topological order.+--+-- The top nodes should have all the other nodes as its dependencies.  complete :: TransSys -> TransSys complete spec =

@@ -4,6 +4,41 @@              ScopedTypeVariables, GADTs, FlexibleContexts #-} {-# LANGUAGE Safe #-} +-- | Translate Copilot specifications into a modular transition system.+--+-- Each stream is associated to a node. The most significant task of this+-- translation process is to /flatten/ the copilot specification so the value+-- of all streams at time @n@ only depends on the values of all the streams at+-- time @n - 1@. For example, for the following Fibonacci implementation in+-- Copilot:+--+-- @+-- fib = [1, 1] ++ (fib + drop 1 fib)+-- @+--+-- the translation, converts it into:+--+-- @+-- fib0 = [1] ++ fib1+-- fib1 = [1] ++ (fib1 + fib0)+-- @+--+-- and then into the node:+--+-- @+-- NODE 'fib' DEPENDS ON []+-- DEFINES+--     out : Int =+--         1 -> pre out.1+--     out.1 : Int =+--         1 -> pre out.2+--     out.2 : Int =+--         (out) + (out.1)+-- @+--+-- This flattening process is made easier by the fact that the @++@ Copilot+-- operator only occurs leftmost in a stream definition after the reification+-- process. module Copilot.Theorem.TransSys.Translate ( translate ) where  import Copilot.Theorem.TransSys.Spec@@ -47,6 +82,7 @@  -------------------------------------------------------------------------------- +-- | Translate Copilot specifications into a modular transition system. translate :: C.Spec -> TransSys translate cspec = 

@@ -3,6 +3,7 @@ {-# LANGUAGE ExistentialQuantification, GADTs #-} {-# LANGUAGE Safe #-} +-- | Types suported by the modular transition systems. module Copilot.Theorem.TransSys.Type   ( Type (..)   , U (..)@@ -13,11 +14,15 @@  -------------------------------------------------------------------------------- +-- | A type at both value and type level.+--+-- Real numbers are mapped to 'Double's. data Type a where   Bool    :: Type Bool   Integer :: Type Integer   Real    :: Type Double +-- | Proofs of type equality. instance EqualType Type where   Bool    =~= Bool     = Just Refl   Integer =~= Integer  = Just Refl@@ -26,8 +31,9 @@  -------------------------------------------------------------------------------- +-- | Unknown types.+-- -- For instance, 'U Expr' is the type of an expression of unknown type- data U f = forall t . U (f t) data U2 f g = forall t . U2 (f t) (g t) 

@@ -0,0 +1,942 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiWayIf #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}++-- |+-- Module      : Copilot.Theorem.What4+-- Description : Prove spec properties using What4.+-- Copyright   : (c) Ben Selfridge, 2020+-- Maintainer  : benselfridge@galois.com+-- Stability   : experimental+-- Portability : POSIX+--+-- Spec properties are translated into the language of SMT solvers using+-- @What4@. A backend solver is then used to prove the property is true. The+-- technique is sound, but incomplete. If a property is proved true by this+-- technique, then it can be guaranteed to be true. However, if a property is+-- not proved true, that does not mean it isn't true. Very simple specifications+-- are unprovable by this technique, including:+--+-- @+-- a = True : a+-- @+--+-- The above specification will not be proved true. The reason is that this+-- technique does not perform any sort of induction. When proving the inner @a@+-- expression, the technique merely allocates a fresh constant standing for+-- "@a@, one timestep in the past." Nothing is asserted about the fresh+-- constant.+--+-- An example of a property that is provable by this approach is:+--+-- @+-- a = True : b+-- b = not a+--+-- -- Property: a || b+-- @+--+-- By allocating a fresh constant, @b_-1@, standing for "the value of @b@ one+-- timestep in the past", the equation for @a || b@ at some arbitrary point in+-- the future reduces to @b_-1 || not b_-1@, which is always true.+--+-- In addition to proving that the stream expression is true at some arbitrary+-- point in the future, we also prove it for the first @k@ timesteps, where @k@+-- is the maximum buffer length of all streams in the given spec. This amounts+-- to simply interpreting the spec, although external variables are still+-- represented as constants with unknown values.++module Copilot.Theorem.What4+  ( prove, Solver(..), SatResult(..)+  ) where++import qualified Copilot.Core.Expr       as CE+import qualified Copilot.Core.Operators  as CE+import qualified Copilot.Core.Spec       as CS+import qualified Copilot.Core.Type       as CT+import qualified Copilot.Core.Type.Array as CT++import qualified What4.Config           as WC+import qualified What4.Expr.Builder     as WB+import qualified What4.Expr.GroundEval  as WG+import qualified What4.Interface        as WI+import qualified What4.BaseTypes        as WT+import qualified What4.Solver           as WS+import qualified What4.Solver.DReal     as WS++import qualified Control.Monad.Fail as Fail+import Control.Monad.State+import qualified Data.BitVector.Sized as BV+import Data.Foldable (foldrM)+import Data.List (elemIndex)+import Data.Maybe (fromJust)+import qualified Data.Map as Map+import Data.Parameterized.Classes+import Data.Parameterized.Context hiding (zipWithM)+import Data.Parameterized.NatRepr+import Data.Parameterized.Nonce+import Data.Parameterized.Some+import Data.Parameterized.SymbolRepr+import qualified Data.Parameterized.Vector as V+import Data.Word+import GHC.Float (castWord32ToFloat, castWord64ToDouble)+import GHC.TypeNats (KnownNat)+import qualified Panic as Panic++--------------------------------------------------------------------------------+-- 'prove' function+--+-- To prove properties of a spec, we translate them into What4 using the TransM+-- monad (transformer on top of IO), then negate each property and ask a backend+-- solver to produce a model for the negation.++-- | We assume round-near-even throughout, but this variable can be changed if+-- needed.+fpRM :: WI.RoundingMode+fpRM = WI.RNE++-- | No builder state needed.+data BuilderState a = EmptyState++-- | The solvers supported by the what4 backend.+data Solver = CVC4 | DReal | Yices | Z3++-- | The 'prove' function returns results of this form for each property in a+-- spec.+data SatResult = Valid | Invalid | Unknown+  deriving Show++type CounterExample = [(String, Some CopilotValue)]++-- | 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.+prove :: Solver+      -- ^ Solver to use+      -> CS.Spec+      -- ^ Spec+      -> IO [(CE.Name, SatResult)]+prove solver spec = do+  -- Setup symbolic backend+  Some ng <- newIONonceGenerator+  sym <- WB.newExprBuilder WB.FloatIEEERepr EmptyState ng++  -- Solver-specific options+  case solver of+    CVC4 -> WC.extendConfig WS.cvc4Options (WI.getConfiguration sym)+    DReal -> WC.extendConfig WS.drealOptions (WI.getConfiguration sym)+    Yices -> WC.extendConfig WS.yicesOptions (WI.getConfiguration sym)+    Z3 -> WC.extendConfig WS.z3Options (WI.getConfiguration sym)++  -- Build up initial translation state+  let streamMap = Map.fromList $+        (\stream -> (CS.streamId stream, stream)) <$> CS.specStreams spec+  pow <- WI.freshTotalUninterpFn sym (WI.safeSymbol "pow") knownRepr knownRepr+  logb <- WI.freshTotalUninterpFn sym (WI.safeSymbol "logb") knownRepr knownRepr+  let st = TransState Map.empty Map.empty Map.empty streamMap pow logb++  -- Define TransM action for proving properties. Doing this in TransM rather+  -- than IO allows us to reuse the state for each property.+  let proveProperties = forM (CS.specProperties spec) $ \pr -> do+        let bufLen (CS.Stream _ buf _ _) = length buf+            maxBufLen = maximum (0 : (bufLen <$> CS.specStreams spec))+        prefix <- forM [0 .. maxBufLen - 1] $ \k -> do+          XBool p <- translateExprAt sym k (CS.propertyExpr pr)+          return p+        XBool p <- translateExpr sym 0 (CS.propertyExpr pr)+        p_and_prefix <- liftIO $ foldrM (WI.andPred sym) p prefix+        not_p_and_prefix <- liftIO $ WI.notPred sym p_and_prefix++        let clauses = [not_p_and_prefix]+        case solver of+          CVC4 -> liftIO $ WS.runCVC4InOverride sym WS.defaultLogData clauses $ \case+            WS.Sat (_ge, _) -> return (CS.propertyName pr, Invalid)+            WS.Unsat _ -> return (CS.propertyName pr, Valid)+            WS.Unknown -> return (CS.propertyName pr, Unknown)+          DReal -> liftIO $ WS.runDRealInOverride sym WS.defaultLogData clauses $ \case+            WS.Sat (_ge, _) -> return (CS.propertyName pr, Invalid)+            WS.Unsat _ -> return (CS.propertyName pr, Valid)+            WS.Unknown -> return (CS.propertyName pr, Unknown)+          Yices -> liftIO $ WS.runYicesInOverride sym WS.defaultLogData clauses $ \case+            WS.Sat _ge -> return (CS.propertyName pr, Invalid)+            WS.Unsat _ -> return (CS.propertyName pr, Valid)+            WS.Unknown -> return (CS.propertyName pr, Unknown)+          Z3 -> liftIO $ WS.runZ3InOverride sym WS.defaultLogData clauses $ \case+            WS.Sat (_ge, _) -> return (CS.propertyName pr, Invalid)+            WS.Unsat _ -> return (CS.propertyName pr, Valid)+            WS.Unknown -> return (CS.propertyName pr, Unknown)++  -- Execute the action and return the results for each property+  (res, _) <- runStateT (unTransM proveProperties) st+  return res++--------------------------------------------------------------------------------+-- What4 translation++-- | the state for translating Copilot expressions into What4 expressions. As we+-- translate, we generate fresh symbolic constants for external variables and+-- for stream variables. We need to only generate one constant per variable, so+-- we allocate them in a map. When we need the constant for a particular+-- variable, we check if it is already in the map, and return it if it is; if it+-- isn't, we generate a fresh constant at that point, store it in the map, and+-- return it.+--+-- We also store three immutable fields in this state, rather than wrap them up+-- in another monad transformer layer. These are initialized prior to+-- translation and are never modified. They are the map from stream ids to the+-- core stream definitions, a symbolic uninterpreted function for "pow", and a+-- symbolic uninterpreted function for "logb".+data TransState t = TransState {+  -- | Map of all external variables we encounter during translation. These are+  -- just fresh constants. The offset indicates how many timesteps in the past+  -- this constant represents for that stream.+  externVars :: Map.Map (CE.Name, Int) (XExpr t),+  -- | Map of external variables at specific indices (positive), rather than+  -- offset into the past. This is for interpreting streams at specific offsets.+  externVarsAt :: Map.Map (CE.Name, Int) (XExpr t),+  -- | Map from (stream id, negative offset) to fresh constant. These are all+  -- constants representing the values of a stream at some point in the past.+  -- The offset (ALWAYS NEGATIVE) indicates how many timesteps in the past+  -- this constant represents for that stream.+  streamConstants :: Map.Map (CE.Id, Int) (XExpr t),+  -- | Map from stream ids to the streams themselves. This value is never+  -- modified, but I didn't want to make this an RWS, so it's represented as a+  -- stateful value.+  streams :: Map.Map CE.Id CS.Stream,+  -- | Binary power operator, represented as an uninterpreted function.+  pow :: WB.ExprSymFn t (WB.Expr t)+         (EmptyCtx ::> WT.BaseRealType ::> WT.BaseRealType)+         WT.BaseRealType,+  -- | Binary logarithm operator, represented as an uninterpreted function.+  logb :: WB.ExprSymFn t (WB.Expr t)+          (EmptyCtx ::> WT.BaseRealType ::> WT.BaseRealType)+          WT.BaseRealType+  }++newtype TransM t a = TransM { unTransM :: StateT (TransState t) IO a }+  deriving ( Functor+           , Applicative+           , Monad+           , MonadIO+           , MonadState (TransState t)+           )++instance Fail.MonadFail (TransM t) where+  fail = error++data CopilotWhat4 = CopilotWhat4++instance Panic.PanicComponent CopilotWhat4 where+  panicComponentName _ = "Copilot/What4 translation"+  panicComponentIssues _ = "https://github.com/Copilot-Language/copilot-theorem/issues"++  {-# NOINLINE Panic.panicComponentRevision #-}+  panicComponentRevision = $(Panic.useGitRevision)++-- | Use this function rather than an error monad since it indicates that+-- copilot-core's "reify" function did something incorrectly.+panic :: MonadIO m => m a+panic = Panic.panic CopilotWhat4 "Copilot.Theorem.What4"+        [ "Ill-typed core expression" ]++-- | 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 t' type. The only reason this is a GADT+-- is for the array case; we need to know that the array length is strictly+-- positive.+data XExpr t where+  XBool       :: WB.Expr t WT.BaseBoolType -> XExpr t+  XInt8       :: WB.Expr t (WT.BaseBVType 8) -> XExpr t+  XInt16      :: WB.Expr t (WT.BaseBVType 16) -> XExpr t+  XInt32      :: WB.Expr t (WT.BaseBVType 32) -> XExpr t+  XInt64      :: WB.Expr t (WT.BaseBVType 64) -> XExpr t+  XWord8      :: WB.Expr t (WT.BaseBVType 8) -> XExpr t+  XWord16     :: WB.Expr t (WT.BaseBVType 16) -> XExpr t+  XWord32     :: WB.Expr t (WT.BaseBVType 32) -> XExpr t+  XWord64     :: WB.Expr t (WT.BaseBVType 64) -> XExpr t+  XFloat      :: WB.Expr t (WT.BaseFloatType WT.Prec32) -> XExpr t+  XDouble     :: WB.Expr t (WT.BaseFloatType WT.Prec64) -> XExpr t+  XEmptyArray :: XExpr t+  XArray      :: 1 <= n => V.Vector n (XExpr t) -> XExpr t+  XStruct     :: [XExpr t] -> XExpr t+  -- XArray      :: NatRepr n+  --             -> BaseTypeRepr tp+  --             -> Some (WB.Expr t)+  -- XStruct     :: Assignment BaseTypeRepr tps+  --             -> WB.Expr t (BaseStructType tps)+  --             -> XExpr t++deriving instance Show (XExpr t)++data CopilotValue a = CopilotValue { cvType :: CT.Type a+                                   , cvVal :: a+                                   }++valFromExpr :: WG.GroundEvalFn t -> XExpr t -> IO (Some CopilotValue)+valFromExpr ge xe = case xe of+  XBool e -> Some . CopilotValue CT.Bool <$> WG.groundEval ge e+  XInt8 e -> Some . CopilotValue CT.Int8 . fromBV <$> WG.groundEval ge e+  XInt16 e -> Some . CopilotValue CT.Int16 . fromBV <$> WG.groundEval ge e+  XInt32 e -> Some . CopilotValue CT.Int32 . fromBV <$> WG.groundEval ge e+  XInt64 e -> Some . CopilotValue CT.Int64 . fromBV <$> WG.groundEval ge e+  XWord8 e -> Some . CopilotValue CT.Word8 . fromBV <$> WG.groundEval ge e+  XWord16 e -> Some . CopilotValue CT.Word16 . fromBV <$> WG.groundEval ge e+  XWord32 e -> Some . CopilotValue CT.Word32 . fromBV <$> WG.groundEval ge e+  XWord64 e -> Some . CopilotValue CT.Word64 . fromBV <$> WG.groundEval ge e+  XFloat e ->+    Some . CopilotValue CT.Float . castWord32ToFloat . fromBV <$> WG.groundEval ge e+  XDouble e ->+    Some . CopilotValue CT.Double . castWord64ToDouble . fromBV <$> WG.groundEval ge e+  _ -> error "valFromExpr unhandled case"+  where fromBV :: forall a w . Num a => BV.BV w -> a+        fromBV = fromInteger . BV.asUnsigned++-- | A view of an XExpr as a bitvector expression, a natrepr for its width, its+-- signed/unsigned status, and the constructor used to reconstruct an XExpr from+-- it. This is a useful view for translation, as many of the operations can be+-- grouped together for all words\/ints\/floats.+data SomeBVExpr t where+  SomeBVExpr :: 1 <= w+             => WB.BVExpr t w+             -> NatRepr w+             -> BVSign+             -> (WB.BVExpr t w -> XExpr t)+             -> SomeBVExpr t++-- | The sign of a bitvector -- this indicates whether it is to be interpreted+-- as a signed 'Int' or an unsigned 'Word'.+data BVSign = Signed | Unsigned++-- | If the inner expression can be viewed as a bitvector, we project out a view+-- of it as such.+asBVExpr :: XExpr t -> Maybe (SomeBVExpr t)+asBVExpr xe = case xe of+  XInt8 e -> Just (SomeBVExpr e knownNat Signed XInt8)+  XInt16 e -> Just (SomeBVExpr e knownNat Signed XInt16)+  XInt32 e -> Just (SomeBVExpr e knownNat Signed XInt32)+  XInt64 e -> Just (SomeBVExpr e knownNat Signed XInt64)+  XWord8 e -> Just (SomeBVExpr e knownNat Unsigned XWord8)+  XWord16 e -> Just (SomeBVExpr e knownNat Unsigned XWord16)+  XWord32 e -> Just (SomeBVExpr e knownNat Unsigned XWord32)+  XWord64 e -> Just (SomeBVExpr e knownNat Unsigned XWord64)+  _ -> Nothing++-- | Translate a constant expression by creating a what4 literal and packaging+-- it up into an 'XExpr'.+translateConstExpr :: forall a t st fs .+                      WB.ExprBuilder t st fs+                   -> CT.Type a+                   -> a+                   -> IO (XExpr t)+translateConstExpr sym tp a = case tp of+  CT.Bool -> case a of+    True  -> return $ XBool (WI.truePred sym)+    False -> return $ XBool (WI.falsePred sym)+  CT.Int8 -> XInt8 <$> WI.bvLit sym knownNat (BV.int8 a)+  CT.Int16 -> XInt16 <$> WI.bvLit sym knownNat (BV.int16 a)+  CT.Int32 -> XInt32 <$> WI.bvLit sym knownNat (BV.int32 a)+  CT.Int64 -> XInt64 <$> WI.bvLit sym knownNat (BV.int64 a)+  CT.Word8 -> XWord8 <$> WI.bvLit sym knownNat (BV.word8 a)+  CT.Word16 -> XWord16 <$> WI.bvLit sym knownNat (BV.word16 a)+  CT.Word32 -> XWord32 <$> WI.bvLit sym knownNat (BV.word32 a)+  CT.Word64 -> XWord64 <$> WI.bvLit sym knownNat (BV.word64 a)+  CT.Float -> XFloat <$> WI.floatLit sym knownRepr (toRational a)+  CT.Double -> XDouble <$> WI.floatLit sym knownRepr (toRational a)+  CT.Array tp -> do+    elts <- traverse (translateConstExpr sym tp) (CT.arrayelems a)+    Just (Some n) <- return $ someNat (length elts)+    case isZeroOrGT1 n of+      Left Refl -> return XEmptyArray+      Right LeqProof -> do+        let Just v = V.fromList n elts+        return $ XArray v+  CT.Struct _ -> do+    elts <- forM (CT.toValues a) $ \(CT.Value tp (CT.Field a)) ->+      translateConstExpr sym tp a+    return $ XStruct elts++arrayLen :: KnownNat n => CT.Type (CT.Array n t) -> NatRepr n+arrayLen _ = knownNat++-- | Generate a fresh constant for a given copilot type. This will be called+-- whenever we attempt to get the constant for a given external variable or+-- stream variable, but that variable has not been accessed yet and therefore+-- has no constant allocated.+freshCPConstant :: forall t st fs a .+                   WB.ExprBuilder t st fs+                -> String+                -> CT.Type a+                -> IO (XExpr t)+freshCPConstant sym nm tp = case tp of+  CT.Bool -> XBool <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr+  CT.Int8 -> XInt8 <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr+  CT.Int16 -> XInt16 <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr+  CT.Int32 -> XInt32 <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr+  CT.Int64 -> XInt64 <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr+  CT.Word8 -> XWord8 <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr+  CT.Word16 -> XWord16 <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr+  CT.Word32 -> XWord32 <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr+  CT.Word64 -> XWord64 <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr+  CT.Float -> XFloat <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr+  CT.Double -> XDouble <$> WI.freshConstant sym (WI.safeSymbol nm) knownRepr+  atp@(CT.Array itp) -> do+    n <- return $ arrayLen atp+    case isZeroOrGT1 n of+      Left Refl -> return XEmptyArray+      Right LeqProof -> do+        Refl <- return $ minusPlusCancel n (knownNat @1)+        elts :: V.Vector n (XExpr t) <- V.generateM (decNat n) (const (freshCPConstant sym "" itp))+        return $ XArray elts+  CT.Struct stp -> do+    elts <- forM (CT.toValues stp) $ \(CT.Value ftp _) -> freshCPConstant sym "" ftp+    return $ XStruct elts++-- | Get the constant for a given stream id and some offset into the past. This+-- should only be called with a strictly negative offset. When this function+-- gets called for the first time for a given (streamId, offset) pair, it+-- generates a fresh constant and stores it in an internal map. Thereafter, this+-- function will just return that constant when called with the same pair.+getStreamConstant :: WB.ExprBuilder t st fs -> CE.Id -> Int -> TransM t (XExpr t)+getStreamConstant sym streamId offset = do+  scs <- gets streamConstants+  case Map.lookup (streamId, offset) scs of+    Just xe -> return xe+    Nothing -> do+      CS.Stream _ _ _ tp <- getStreamDef streamId+      let nm = show streamId ++ "_" ++ show offset+      xe <- liftIO $ freshCPConstant sym nm tp+      modify (\st -> st { streamConstants = Map.insert (streamId, offset) xe scs })+      return xe++-- | Get the constant for a given external variable and some offset into the+-- past. This should only be called with a strictly negative offset. When this+-- function gets called for the first time for a given (var, offset) pair, it+-- generates a fresh constant and stores it in an internal map. Thereafter, this+-- function will just return that constant when called with the same pair.+getExternConstant :: WB.ExprBuilder t st fs+                  -> CT.Type a+                  -> CE.Name+                  -> Int+                  -> TransM t (XExpr t)+getExternConstant sym tp var offset = do+  es <- gets externVars+  case Map.lookup (var, offset) es of+    Just xe -> return xe+    Nothing -> do+      xe <- liftIO $ freshCPConstant sym var tp+      modify (\st -> st { externVars = Map.insert (var, offset) xe es} )+      return xe++-- | Get the constant for a given external variable at some specific timestep.+getExternConstantAt :: WB.ExprBuilder t st fs+                    -> CT.Type a+                    -> CE.Name+                    -> Int+                    -> TransM t (XExpr t)+getExternConstantAt sym tp var ix = do+  es <- gets externVarsAt+  case Map.lookup (var, ix) es of+    Just xe -> return xe+    Nothing -> do+      xe <- liftIO $ freshCPConstant sym var tp+      modify (\st -> st { externVarsAt = Map.insert (var, ix) xe es} )+      return xe++-- | Retrieve a stream definition given its id.+getStreamDef :: CE.Id -> TransM t CS.Stream+getStreamDef streamId = fromJust <$> gets (Map.lookup streamId . streams)++-- | Translate an expression into a what4 representation. The int offset keeps+-- track of how many timesteps into the past each variable is referring to.+-- Initially the value should be zero, but when we translate a stream, the+-- offset is recomputed based on the length of that stream's prefix (subtracted)+-- and the drop index (added).+translateExpr :: WB.ExprBuilder t st fs+              -> Int+              -- ^ number of timesteps in the past we are currently looking+              -- (must always be <= 0)+              -> CE.Expr a+              -> TransM t (XExpr t)+translateExpr sym offset e = case e of+  CE.Const tp a -> liftIO $ translateConstExpr sym tp a+  CE.Drop _tp ix streamId+    -- If we are referencing a past value of this stream, just return an+    -- unconstrained constant.+    | offset + fromIntegral ix < 0 ->+        getStreamConstant sym streamId (offset + fromIntegral ix)+    -- If we are referencing a current or future value of this stream, we need+    -- to translate the stream's expression, using an offset computed based on+    -- the current offset (negative or 0), the drop index (positive or 0), and+    -- the length of the stream's buffer (subtracted).+    | otherwise -> do+      CS.Stream _ buf e _ <- getStreamDef streamId+      translateExpr sym (offset + fromIntegral ix - length buf) e+  CE.Local _ _ _ _ _ -> error "translateExpr: Local unimplemented"+  CE.Var _ _ -> error "translateExpr: Var unimplemented"+  CE.ExternVar tp nm _prefix -> getExternConstant sym tp nm offset+  CE.Op1 op e -> liftIO . translateOp1 sym op =<< translateExpr sym offset e+  CE.Op2 op e1 e2 -> do+    xe1 <- translateExpr sym offset e1+    xe2 <- translateExpr sym offset e2+    powFn <- gets pow+    logbFn <- gets logb+    liftIO $ translateOp2 sym powFn logbFn op xe1 xe2+  CE.Op3 op e1 e2 e3 -> do+    xe1 <- translateExpr sym offset e1+    xe2 <- translateExpr sym offset e2+    xe3 <- translateExpr sym offset e3+    liftIO $ translateOp3 sym op xe1 xe2 xe3+  CE.Label _ _ _ -> error "translateExpr: Label unimplemented"++-- | Translate an expression into a what4 representation at a /specific/+-- timestep, rather than "at some indeterminate point in the future."+translateExprAt :: WB.ExprBuilder t st fs+                -> Int+                -- ^ Index of timestep+                -> CE.Expr a+                -- ^ stream expression+                -> TransM t (XExpr t)+translateExprAt sym k e = do+  case e of+    CE.Const tp a -> liftIO $ translateConstExpr sym tp a+    CE.Drop _tp ix streamId -> do+      CS.Stream _ buf e tp <- getStreamDef streamId+      if k' < length buf+        then liftIO $ translateConstExpr sym tp (buf !! k')+        else translateExprAt sym (k' - length buf) e+      where k' = k + fromIntegral ix+    CE.Local _ _ _ _ _ -> error "translateExpr: Local unimplemented"+    CE.Var _ _ -> error "translateExpr: Var unimplemented"+    CE.ExternVar tp nm _prefix -> getExternConstantAt sym tp nm k+    CE.Op1 op e -> liftIO . translateOp1 sym op =<< translateExprAt sym k e+    CE.Op2 op e1 e2 -> do+      xe1 <- translateExprAt sym k e1+      xe2 <- translateExprAt sym k e2+      powFn <- gets pow+      logbFn <- gets logb+      liftIO $ translateOp2 sym powFn logbFn op xe1 xe2+    CE.Op3 op e1 e2 e3 -> do+      xe1 <- translateExprAt sym k e1+      xe2 <- translateExprAt sym k e2+      xe3 <- translateExprAt sym k e3+      liftIO $ translateOp3 sym op xe1 xe2 xe3+    CE.Label _ _ _ -> error "translateExpr: Label unimplemented"++type BVOp1 w t = (KnownNat w, 1 <= w) => WB.BVExpr t w -> IO (WB.BVExpr t w)++type FPOp1 fpp t = KnownRepr WT.FloatPrecisionRepr fpp => WB.Expr t (WT.BaseFloatType fpp) -> IO (WB.Expr t (WT.BaseFloatType fpp))++type RealOp1 t = WB.Expr t WT.BaseRealType -> IO (WB.Expr t WT.BaseRealType)++fieldName :: KnownSymbol s => CT.Field s a -> SymbolRepr s+fieldName _ = knownSymbol++valueName :: CT.Value a -> Some SymbolRepr+valueName (CT.Value _ f) = Some (fieldName f)++translateOp1 :: forall t st fs a b .+                WB.ExprBuilder t st fs+             -> CE.Op1 a b+             -> XExpr t+             -> IO (XExpr t)+translateOp1 sym op xe = case (op, xe) of+  (CE.Not, XBool e) -> XBool <$> WI.notPred sym e+  (CE.Not, _) -> panic+  (CE.Abs _, xe) -> numOp bvAbs fpAbs xe+    where bvAbs :: BVOp1 w t+          bvAbs e = do zero <- WI.bvLit sym knownNat (BV.zero knownNat)+                       e_neg <- WI.bvSlt sym e zero+                       neg_e <- WI.bvSub sym zero e+                       WI.bvIte sym e_neg neg_e e+          fpAbs :: FPOp1 fpp t+          fpAbs e = do zero <- WI.floatLit sym knownRepr 0+                       e_neg <- WI.floatLt sym e zero+                       neg_e <- WI.floatSub sym fpRM zero e+                       WI.floatIte sym e_neg neg_e e+  (CE.Sign _, xe) -> numOp bvSign fpSign xe+    where bvSign :: BVOp1 w t+          bvSign e = do zero <- WI.bvLit sym knownRepr (BV.zero knownNat)+                        neg_one <- WI.bvLit sym knownNat (BV.mkBV knownNat (-1))+                        pos_one <- WI.bvLit sym knownNat (BV.mkBV knownNat 1)+                        e_zero <- WI.bvEq sym e zero+                        e_neg <- WI.bvSlt sym e zero+                        t <- WI.bvIte sym e_neg neg_one pos_one+                        WI.bvIte sym e_zero zero t+          fpSign :: FPOp1 fpp t+          fpSign e = do zero <- WI.floatLit sym knownRepr 0+                        neg_one <- WI.floatLit sym knownRepr (-1)+                        pos_one <- WI.floatLit sym knownRepr 1+                        e_zero <- WI.floatEq sym e zero+                        e_neg <- WI.floatLt sym e zero+                        t <- WI.floatIte sym e_neg neg_one pos_one+                        WI.floatIte sym e_zero zero t+  (CE.Recip _, xe) -> fpOp recip xe+    where recip :: FPOp1 fpp t+          recip e = do one <- WI.floatLit sym knownRepr 1+                       WI.floatDiv sym fpRM one e+  (CE.Exp _, xe) -> realOp (WI.realExp sym) xe+  (CE.Sqrt _, xe) -> fpOp (WI.floatSqrt sym fpRM) xe+  (CE.Log _, xe) -> realOp (WI.realLog sym) xe+  (CE.Sin _, xe) -> realOp (WI.realSin sym) xe+  (CE.Cos _, xe) -> realOp (WI.realCos sym) xe+  (CE.Tan _, xe) -> realOp (WI.realTan sym) xe+  (CE.Asin _, xe) -> realOp (realRecip <=< WI.realSin sym) xe+  (CE.Acos _, xe) -> realOp (realRecip <=< WI.realCos sym) xe+  (CE.Atan _, xe) -> realOp (realRecip <=< WI.realTan sym) xe+  (CE.Sinh _, xe) -> realOp (WI.realSinh sym) xe+  (CE.Cosh _, xe) -> realOp (WI.realCosh sym) xe+  (CE.Tanh _, xe) -> realOp (WI.realTanh sym) xe+  (CE.Asinh _, xe) -> realOp (realRecip <=< WI.realSinh sym) xe+  (CE.Acosh _, xe) -> realOp (realRecip <=< WI.realCosh sym) xe+  (CE.Atanh _, xe) -> realOp (realRecip <=< WI.realTanh sym) xe+  (CE.BwNot _, xe) -> case xe of+    XBool e -> XBool <$> WI.notPred sym e+    _ -> bvOp (WI.bvNotBits sym) xe+  (CE.Cast _ tp, xe) -> case (xe, tp) of+    (XBool e, CT.Bool) -> return $ XBool e+    (XBool e, CT.Word8) -> XWord8 <$> WI.predToBV sym e knownNat+    (XBool e, CT.Word16) -> XWord16 <$> WI.predToBV sym e knownNat+    (XBool e, CT.Word32) -> XWord32 <$> WI.predToBV sym e knownNat+    (XBool e, CT.Word64) -> XWord64 <$> WI.predToBV sym e knownNat+    (XBool e, CT.Int8) -> XInt8 <$> WI.predToBV sym e knownNat+    (XBool e, CT.Int16) -> XInt16 <$> WI.predToBV sym e knownNat+    (XBool e, CT.Int32) -> XInt32 <$> WI.predToBV sym e knownNat+    (XBool e, CT.Int64) -> XInt64 <$> WI.predToBV sym e knownNat+    (XInt8 e, CT.Int8) -> return $ XInt8 e+    (XInt8 e, CT.Int16) -> XInt16 <$> WI.bvSext sym knownNat e+    (XInt8 e, CT.Int32) -> XInt32 <$> WI.bvSext sym knownNat e+    (XInt8 e, CT.Int64) -> XInt64 <$> WI.bvSext sym knownNat e+    (XInt16 e, CT.Int16) -> return $ XInt16 e+    (XInt16 e, CT.Int32) -> XInt32 <$> WI.bvSext sym knownNat e+    (XInt16 e, CT.Int64) -> XInt64 <$> WI.bvSext sym knownNat e+    (XInt32 e, CT.Int32) -> return $ XInt32 e+    (XInt32 e, CT.Int64) -> XInt64 <$> WI.bvSext sym knownNat e+    (XInt64 e, CT.Int64) -> return $ XInt64 e+    (XWord8 e, CT.Int16) -> XInt16 <$> WI.bvZext sym knownNat e+    (XWord8 e, CT.Int32) -> XInt32 <$> WI.bvZext sym knownNat e+    (XWord8 e, CT.Int64) -> XInt64 <$> WI.bvZext sym knownNat e+    (XWord8 e, CT.Word8) -> return $ XWord8 e+    (XWord8 e, CT.Word16) -> XWord16 <$> WI.bvZext sym knownNat e+    (XWord8 e, CT.Word32) -> XWord32 <$> WI.bvZext sym knownNat e+    (XWord8 e, CT.Word64) -> XWord64 <$> WI.bvZext sym knownNat e+    (XWord16 e, CT.Int32) -> XInt32 <$> WI.bvZext sym knownNat e+    (XWord16 e, CT.Int64) -> XInt64 <$> WI.bvZext sym knownNat e+    (XWord16 e, CT.Word16) -> return $ XWord16 e+    (XWord16 e, CT.Word32) -> XWord32 <$> WI.bvZext sym knownNat e+    (XWord16 e, CT.Word64) -> XWord64 <$> WI.bvZext sym knownNat e+    (XWord32 e, CT.Int64) -> XInt64 <$> WI.bvZext sym knownNat e+    (XWord32 e, CT.Word32) -> return $ XWord32 e+    (XWord32 e, CT.Word64) -> XWord64 <$> WI.bvZext sym knownNat e+    (XWord64 e, CT.Word64) -> return $ XWord64 e+    _ -> panic+  (CE.GetField (CT.Struct s) _ftp extractor, XStruct xes) -> do+    let fieldNameRepr = fieldName (extractor undefined)+    let structFieldNameReprs = valueName <$> CT.toValues s+    let mIx = elemIndex (Some fieldNameRepr) structFieldNameReprs+    case mIx of+      Just ix -> return $ xes !! ix+      Nothing -> panic+  _ -> panic+  where numOp :: (forall w . BVOp1 w t)+              -> (forall fpp . FPOp1 fpp t)+              -> XExpr t+              -> IO (XExpr t)+        numOp bvOp fpOp xe = case xe of+          XInt8 e -> XInt8 <$> bvOp e+          XInt16 e -> XInt16 <$> bvOp e+          XInt32 e -> XInt32 <$> bvOp e+          XInt64 e -> XInt64 <$> bvOp e+          XWord8 e -> XWord8 <$> bvOp e+          XWord16 e -> XWord16 <$> bvOp e+          XWord32 e -> XWord32 <$> bvOp e+          XWord64 e -> XWord64 <$> bvOp e+          XFloat e -> XFloat <$> fpOp e+          XDouble e -> XDouble <$> fpOp e+          _ -> panic++        bvOp :: (forall w . BVOp1 w t) -> XExpr t -> IO (XExpr t)+        bvOp f xe = case xe of+          XInt8 e -> XInt8 <$> f e+          XInt16 e -> XInt16 <$> f e+          XInt32 e -> XInt32 <$> f e+          XInt64 e -> XInt64 <$> f e+          XWord8 e -> XWord8 <$> f e+          XWord16 e -> XWord16 <$> f e+          XWord32 e -> XWord32 <$> f e+          XWord64 e -> XWord64 <$> f e+          _ -> panic++        fpOp :: (forall fpp . FPOp1 fpp t) -> XExpr t -> IO (XExpr t)+        fpOp g xe = case xe of+          XFloat e -> XFloat <$> g e+          XDouble e -> XDouble <$> g e+          _ -> panic++        realOp :: RealOp1 t -> XExpr t -> IO (XExpr t)+        realOp h xe = fpOp hf xe+          where hf :: (forall fpp . FPOp1 fpp t)+                hf e = do re <- WI.floatToReal sym e+                          hre <- h re+                          WI.realToFloat sym knownRepr fpRM hre++        realRecip :: RealOp1 t+        realRecip e = do one <- WI.realLit sym 1+                         WI.realDiv sym one e++type BVOp2 w t = (KnownNat w, 1 <= w) => WB.BVExpr t w -> WB.BVExpr t w -> IO (WB.BVExpr t w)++type FPOp2 fpp t = KnownRepr WT.FloatPrecisionRepr fpp => WB.Expr t (WT.BaseFloatType fpp) -> WB.Expr t (WT.BaseFloatType fpp) -> IO (WB.Expr t (WT.BaseFloatType fpp))++type RealOp2 t = WB.Expr t WT.BaseRealType -> WB.Expr t WT.BaseRealType -> IO (WB.Expr t WT.BaseRealType)++type BoolCmp2 t = WB.BoolExpr t -> WB.BoolExpr t -> IO (WB.BoolExpr t)++type BVCmp2 w t = (KnownNat w, 1 <= w) => WB.BVExpr t w -> WB.BVExpr t w -> IO (WB.BoolExpr t)++type FPCmp2 fpp t = KnownRepr WT.FloatPrecisionRepr fpp => WB.Expr t (WT.BaseFloatType fpp) -> WB.Expr t (WT.BaseFloatType fpp) -> IO (WB.BoolExpr t)++translateOp2 :: forall t st fs a b c .+                WB.ExprBuilder t st fs+             -> (WB.ExprSymFn t (WB.Expr t)+                 (EmptyCtx ::> WT.BaseRealType ::> WT.BaseRealType)+                 WT.BaseRealType)+             -- ^ Pow function+             -> (WB.ExprSymFn t (WB.Expr t)+                 (EmptyCtx ::> WT.BaseRealType ::> WT.BaseRealType)+                 WT.BaseRealType)+             -- ^ Logb function+             -> CE.Op2 a b c+             -> XExpr t+             -> XExpr t+             -> IO (XExpr t)+translateOp2 sym powFn logbFn op xe1 xe2 = case (op, xe1, xe2) of+  (CE.And, XBool e1, XBool e2) -> XBool <$> WI.andPred sym e1 e2+  (CE.Or, XBool e1, XBool e2) -> XBool <$> WI.orPred sym e1 e2+  (CE.Add _, xe1, xe2) -> numOp (WI.bvAdd sym) (WI.floatAdd sym fpRM) xe1 xe2+  (CE.Sub _, xe1, xe2) -> numOp (WI.bvSub sym) (WI.floatSub sym fpRM) xe1 xe2+  (CE.Mul _, xe1, xe2) -> numOp (WI.bvMul sym) (WI.floatMul sym fpRM) xe1 xe2+  (CE.Mod _, xe1, xe2) -> bvOp (WI.bvSrem sym) (WI.bvUrem sym) xe1 xe2+  (CE.Div _, xe1, xe2) -> bvOp (WI.bvSdiv sym) (WI.bvUdiv sym) xe1 xe2+  (CE.Fdiv _, xe1, xe2) -> fpOp (WI.floatDiv sym fpRM) xe1 xe2+  (CE.Pow _, xe1, xe2) -> fpOp powFn' xe1 xe2+    where powFn' :: FPOp2 fpp t+          powFn' e1 e2 = do re1 <- WI.floatToReal sym e1+                            re2 <- WI.floatToReal sym e2+                            let args = (Empty :> re1 :> re2)+                            rpow <- WI.applySymFn sym powFn args+                            WI.realToFloat sym knownRepr fpRM rpow+  (CE.Logb _, xe1, xe2) -> fpOp logbFn' xe1 xe2+    where logbFn' :: FPOp2 fpp t+          logbFn' e1 e2 = do re1 <- WI.floatToReal sym e1+                             re2 <- WI.floatToReal sym e2+                             let args = (Empty :> re1 :> re2)+                             rpow <- WI.applySymFn sym logbFn args+                             WI.realToFloat sym knownRepr fpRM rpow+  (CE.Eq _, xe1, xe2) -> cmp (WI.eqPred sym) (WI.bvEq sym) (WI.floatEq sym) xe1 xe2+  (CE.Ne _, xe1, xe2) -> cmp neqPred bvNeq fpNeq xe1 xe2+    where neqPred :: BoolCmp2 t+          neqPred e1 e2 = do e <- WI.eqPred sym e1 e2+                             WI.notPred sym e+          bvNeq :: forall w . BVCmp2 w t+          bvNeq e1 e2 = do e <- WI.bvEq sym e1 e2+                           WI.notPred sym e+          fpNeq :: forall fpp . FPCmp2 fpp t+          fpNeq e1 e2 = do e <- WI.floatEq sym e1 e2+                           WI.notPred sym e+  (CE.Le _, xe1, xe2) -> numCmp (WI.bvSle sym) (WI.bvUle sym) (WI.floatLe sym) xe1 xe2+  (CE.Ge _, xe1, xe2) -> numCmp (WI.bvSge sym) (WI.bvUge sym) (WI.floatGe sym) xe1 xe2+  (CE.Lt _, xe1, xe2) -> numCmp (WI.bvSlt sym) (WI.bvUlt sym) (WI.floatLt sym) xe1 xe2+  (CE.Gt _, xe1, xe2) -> numCmp (WI.bvSgt sym) (WI.bvUgt sym) (WI.floatGt sym) xe1 xe2+  (CE.BwAnd _, xe1, xe2) -> bvOp (WI.bvAndBits sym) (WI.bvAndBits sym) xe1 xe2+  (CE.BwOr _, xe1, xe2) -> bvOp (WI.bvOrBits sym) (WI.bvOrBits sym) xe1 xe2+  (CE.BwXor _, xe1, xe2) -> bvOp (WI.bvXorBits sym) (WI.bvXorBits sym) xe1 xe2+  -- Note: For both shift operators, we are interpreting the shifter as an+  -- unsigned bitvector regardless of whether it is a word or an int.+  (CE.BwShiftL _ _, xe1, xe2) -> do+    Just (SomeBVExpr e1 w1 _ ctor1) <- return $ asBVExpr xe1+    Just (SomeBVExpr e2 w2 _ _    ) <- return $ asBVExpr xe2+    e2' <- case testNatCases w1 w2 of+      NatCaseLT LeqProof -> WI.bvTrunc sym w1 e2+      NatCaseEQ -> return e2+      NatCaseGT LeqProof -> WI.bvZext sym w1 e2+    ctor1 <$> WI.bvShl sym e1 e2'+  (CE.BwShiftR _ _, xe1, xe2) -> do+    Just (SomeBVExpr e1 w1 sgn1 ctor1) <- return $ asBVExpr xe1+    Just (SomeBVExpr e2 w2 _    _    ) <- return $ asBVExpr xe2+    e2' <- case testNatCases w1 w2 of+      NatCaseLT LeqProof -> WI.bvTrunc sym w1 e2+      NatCaseEQ -> return e2+      NatCaseGT LeqProof -> WI.bvZext sym w1 e2+    ctor1 <$> case sgn1 of+      Signed -> WI.bvAshr sym e1 e2'+      Unsigned -> WI.bvLshr sym e1 e2'+  -- Note: Currently, copilot does not check if array indices are out of bounds,+  -- even for constant expressions. The method of translation we are using+  -- simply creates a nest of if-then-else expression to check the index+  -- expression against all possible indices. If the index expression is known+  -- by the solver to be out of bounds (for instance, if it is a constant 5 for+  -- an array of 5 elements), then the if-then-else will trivially resolve to+  -- true.+  (CE.Index _, xe1, xe2) -> do+    case (xe1, xe2) of+      (XArray xes, XWord32 ix) -> buildIndexExpr sym 0 ix xes+      _ -> panic+  _ -> panic+  where numOp :: (forall w . BVOp2 w t)+              -> (forall fpp . FPOp2 fpp t)+              -> XExpr t+              -> XExpr t+              -> IO (XExpr t)+        numOp bvOp fpOp xe1 xe2 = case (xe1, xe2) of+          (XInt8 e1, XInt8 e2) -> XInt8 <$> bvOp e1 e2+          (XInt16 e1, XInt16 e2) -> XInt16 <$> bvOp e1 e2+          (XInt32 e1, XInt32 e2)-> XInt32 <$> bvOp e1 e2+          (XInt64 e1, XInt64 e2)-> XInt64 <$> bvOp e1 e2+          (XWord8 e1, XWord8 e2)-> XWord8 <$> bvOp e1 e2+          (XWord16 e1, XWord16 e2)-> XWord16 <$> bvOp e1 e2+          (XWord32 e1, XWord32 e2)-> XWord32 <$> bvOp e1 e2+          (XWord64 e1, XWord64 e2)-> XWord64 <$> bvOp e1 e2+          (XFloat e1, XFloat e2)-> XFloat <$> fpOp e1 e2+          (XDouble e1, XDouble e2)-> XDouble <$> fpOp e1 e2+          _ -> panic++        bvOp :: (forall w . BVOp2 w t)+             -> (forall w . BVOp2 w t)+             -> XExpr t+             -> XExpr t+             -> IO (XExpr t)+        bvOp opS opU xe1 xe2 = case (xe1, xe2) of+          (XInt8 e1, XInt8 e2) -> XInt8 <$> opS e1 e2+          (XInt16 e1, XInt16 e2) -> XInt16 <$> opS e1 e2+          (XInt32 e1, XInt32 e2) -> XInt32 <$> opS e1 e2+          (XInt64 e1, XInt64 e2) -> XInt64 <$> opS e1 e2+          (XWord8 e1, XWord8 e2) -> XWord8 <$> opU e1 e2+          (XWord16 e1, XWord16 e2) -> XWord16 <$> opU e1 e2+          (XWord32 e1, XWord32 e2) -> XWord32 <$> opU e1 e2+          (XWord64 e1, XWord64 e2) -> XWord64 <$> opU e1 e2+          _ -> panic++        fpOp :: (forall fpp . FPOp2 fpp t)+             -> XExpr t+             -> XExpr t+             -> IO (XExpr t)+        fpOp op xe1 xe2 = case (xe1, xe2) of+          (XFloat e1, XFloat e2) -> XFloat <$> op e1 e2+          (XDouble e1, XDouble e2) -> XDouble <$> op e1 e2+          _ -> panic++        cmp :: BoolCmp2 t+            -> (forall w . BVCmp2 w t)+            -> (forall fpp . FPCmp2 fpp t)+            -> XExpr t+            -> XExpr t+            -> IO (XExpr t)+        cmp boolOp bvOp fpOp xe1 xe2 = case (xe1, xe2) of+          (XBool e1, XBool e2) -> XBool <$> boolOp e1 e2+          (XInt8 e1, XInt8 e2) -> XBool <$> bvOp e1 e2+          (XInt16 e1, XInt16 e2) -> XBool <$> bvOp e1 e2+          (XInt32 e1, XInt32 e2)-> XBool <$> bvOp e1 e2+          (XInt64 e1, XInt64 e2)-> XBool <$> bvOp e1 e2+          (XWord8 e1, XWord8 e2)-> XBool <$> bvOp e1 e2+          (XWord16 e1, XWord16 e2)-> XBool <$> bvOp e1 e2+          (XWord32 e1, XWord32 e2)-> XBool <$> bvOp e1 e2+          (XWord64 e1, XWord64 e2)-> XBool <$> bvOp e1 e2+          (XFloat e1, XFloat e2)-> XBool <$> fpOp e1 e2+          (XDouble e1, XDouble e2)-> XBool <$> fpOp e1 e2+          _ -> panic++        numCmp :: (forall w . BVCmp2 w t)+               -> (forall w . BVCmp2 w t)+               -> (forall fpp . FPCmp2 fpp t)+               -> XExpr t+               -> XExpr t+               -> IO (XExpr t)+        numCmp bvSOp bvUOp fpOp xe1 xe2 = case (xe1, xe2) of+          (XInt8 e1, XInt8 e2) -> XBool <$> bvSOp e1 e2+          (XInt16 e1, XInt16 e2) -> XBool <$> bvSOp e1 e2+          (XInt32 e1, XInt32 e2)-> XBool <$> bvSOp e1 e2+          (XInt64 e1, XInt64 e2)-> XBool <$> bvSOp e1 e2+          (XWord8 e1, XWord8 e2)-> XBool <$> bvUOp e1 e2+          (XWord16 e1, XWord16 e2)-> XBool <$> bvUOp e1 e2+          (XWord32 e1, XWord32 e2)-> XBool <$> bvUOp e1 e2+          (XWord64 e1, XWord64 e2)-> XBool <$> bvUOp e1 e2+          (XFloat e1, XFloat e2)-> XBool <$> fpOp e1 e2+          (XDouble e1, XDouble e2)-> XBool <$> fpOp e1 e2+          _ -> panic++        buildIndexExpr :: 1 <= n+                       => WB.ExprBuilder t st fs+                       -> Word32+                       -- ^ Index+                       -> WB.Expr t (WT.BaseBVType 32)+                       -- ^ Index+                       -> V.Vector n (XExpr t)+                       -- ^ Elements+                       -> IO (XExpr t)+        buildIndexExpr sym curIx ix xelts = case V.uncons xelts of+          (xe, Left Refl) -> return xe+          (xe, Right xelts') -> do+            LeqProof <- return $ V.nonEmpty xelts'+            rstExpr <- buildIndexExpr sym (curIx+1) ix xelts'+            curIxExpr <- WI.bvLit sym knownNat (BV.word32 curIx)+            ixEq <- WI.bvEq sym curIxExpr ix+            mkIte sym ixEq xe rstExpr++        mkIte :: WB.ExprBuilder t st fs+              -> WB.Expr t WT.BaseBoolType+              -> XExpr t+              -> XExpr t+              -> IO (XExpr t)+        mkIte sym pred xe1 xe2 = case (xe1, xe2) of+              (XBool e1, XBool e2) -> XBool <$> WI.itePred sym pred e1 e2+              (XInt8 e1, XInt8 e2) -> XInt8 <$> WI.bvIte sym pred e1 e2+              (XInt16 e1, XInt16 e2) -> XInt16 <$> WI.bvIte sym pred e1 e2+              (XInt32 e1, XInt32 e2) -> XInt32 <$> WI.bvIte sym pred e1 e2+              (XInt64 e1, XInt64 e2) -> XInt64 <$> WI.bvIte sym pred e1 e2+              (XWord8 e1, XWord8 e2) -> XWord8 <$> WI.bvIte sym pred e1 e2+              (XWord16 e1, XWord16 e2) -> XWord16 <$> WI.bvIte sym pred e1 e2+              (XWord32 e1, XWord32 e2) -> XWord32 <$> WI.bvIte sym pred e1 e2+              (XWord64 e1, XWord64 e2) -> XWord64 <$> WI.bvIte sym pred e1 e2+              (XFloat e1, XFloat e2) -> XFloat <$> WI.floatIte sym pred e1 e2+              (XDouble e1, XDouble e2) -> XDouble <$> WI.floatIte sym pred e1 e2+              (XStruct xes1, XStruct xes2) ->+                XStruct <$> zipWithM (mkIte sym pred) xes1 xes2+              (XArray xes1, XArray xes2) ->+                case V.length xes1 `testEquality` V.length xes2 of+                  Just Refl -> XArray <$> V.zipWithM (mkIte sym pred) xes1 xes2+                  Nothing -> panic+              _ -> panic+++translateOp3 :: forall t st fs a b c d .+                WB.ExprBuilder t st fs+             -> CE.Op3 a b c d+             -> XExpr t+             -> XExpr t+             -> XExpr t+             -> IO (XExpr t)+translateOp3 sym (CE.Mux _) (XBool te) xe1 xe2 = case (xe1, xe2) of+  (XBool e1, XBool e2) -> XBool <$> WI.itePred sym te e1 e2+  (XInt8 e1, XInt8 e2) -> XInt8 <$> WI.bvIte sym te e1 e2+  (XInt16 e1, XInt16 e2) -> XInt16 <$> WI.bvIte sym te e1 e2+  (XInt32 e1, XInt32 e2) -> XInt32 <$> WI.bvIte sym te e1 e2+  (XInt64 e1, XInt64 e2) -> XInt64 <$> WI.bvIte sym te e1 e2+  (XWord8 e1, XWord8 e2) -> XWord8 <$> WI.bvIte sym te e1 e2+  (XWord16 e1, XWord16 e2) -> XWord16 <$> WI.bvIte sym te e1 e2+  (XWord32 e1, XWord32 e2) -> XWord32 <$> WI.bvIte sym te e1 e2+  (XWord64 e1, XWord64 e2) -> XWord64 <$> WI.bvIte sym te e1 e2+  (XFloat e1, XFloat e2) -> XFloat <$> WI.floatIte sym te e1 e2+  (XDouble e1, XDouble e2) -> XDouble <$> WI.floatIte sym te e1 e2+  _ -> panic+translateOp3 _ _ _ _ _ = panic