s/LanguageSMTBranches/LanguageSymEval/g + comments

src/Language/Pirouette/Example.hs

@@ -36,6 +36,7 @@ import Pirouette.SMT.Base
 import Pirouette.SMT.Constraints
 import qualified PureSMT
 import Pirouette.Term.Syntax
+import Pirouette.Symbolic.Eval.Types
 import qualified Pirouette.Term.Syntax.SystemF as SystF
 import Prettyprinter (dquotes)
 import Text.Megaparsec
@@ -235,9 +236,25 @@ isConstant (BConstant _) = True
 isConstant (SConstant _) = True
 isConstant _ = False
 
--- | Finally, you might want to customize the behavior of the symbolic execution engine...
--- TODO: @serras, can you write a paragraph or two on this instance and why it is important?
-instance LanguageSMTBranches Ex where
+-- | Finally, you might need to customize the behavior of the symbolic execution engine. Take
+-- the interpretation of @if@ statements as an example. If you just rely on the SMT @ifthenelse@
+-- construct, you might end up generating bogus counter-examples due to the SMT assuming
+-- wrong things out of uninterpreted functions due to a lack of information.
+--
+-- Say we translate the builtin @if@ statement to its SMT counterpart and evaluate:
+--
+-- > (assert (= x (ifthenelse (isEven 5) 42 0)))
+-- > (assert (= x 0))
+-- > (check-sat)
+--
+-- The SMT will say the above is unsat, and will give a model that assumes @isEven 5@ to be true,
+-- yielding @x = 42@. That's because @isEven@ is an uninterpreted function, so the SMT has no information
+-- about it.
+--
+-- The rule of thumb is easy: any primitive of your language that should branch the symbolic execution engine
+-- should receive special treatment in 'LanguageSymEval'; branching should always be handled by the symbolic
+-- engine and never delegated to the SMT solver.
+instance LanguageSymEval Ex where
   -- translate arithmetic operations applied to constants
   branchesBuiltinTerm op _translator [SystF.TermArg (IConstant x), SystF.TermArg (IConstant y)]
     | exTermIsArithOp op =

src/Language/Pirouette/PlutusIR/SMT.hs

@@ -2,6 +2,7 @@ module Language.Pirouette.PlutusIR.SMT where
 
 import qualified Data.Text as Text
 import Language.Pirouette.PlutusIR.Syntax
+import Pirouette.Symbolic.Eval.Types
 import Pirouette.SMT.Base
 import Pirouette.SMT.Constraints
 import qualified PlutusCore as P
@@ -15,7 +16,7 @@ instance LanguageSMT PlutusIR where
   translateConstant = trPIRConstant
   isStuckBuiltin = error "isStuckBuiltin (t :: TermMeta PlutusIR meta): not yet impl"
 
-instance LanguageSMTBranches PlutusIR where
+instance LanguageSymEval PlutusIR where
   branchesBuiltinTerm _tm _translator _args = pure Nothing
 
 trPIRType :: PIRBuiltinType -> PureSMT.SExpr

src/Pirouette/SMT/Constraints.hs

@@ -61,19 +61,6 @@ data Branch lang meta = Branch
     newTerm :: TermMeta lang meta
   }
 
--- TODO: Maybe this should be merged with 'LanguageSMT'
-class (LanguageSMT lang) => LanguageSMTBranches lang where
-  -- | Injection of different cases in the symbolic evaluator.
-  -- For example, one can introduce a 'if_then_else' built-in
-  -- and implement this method to look at both possibilities.
-  branchesBuiltinTerm ::
-    (ToSMT meta, PirouetteReadDefs lang m) =>
-    BuiltinTerms lang ->
-    (TermMeta lang meta -> m (Maybe PureSMT.SExpr)) ->
-    [ArgMeta lang meta] ->
-    m (Maybe [Branch lang meta])
-  branchesBuiltinTerm _ _ _ = pure Nothing
-
 -- Essentially list concatenation, with the specificity that `Bot` is absorbing.
 andConstr :: Constraint lang meta -> Constraint lang meta -> Constraint lang meta
 andConstr Bot _ = Bot

src/Pirouette/SMT/Monadic.hs

@@ -33,7 +33,6 @@ module Pirouette.SMT.Monadic
     PureSMT.Result (..),
     module Base,
     Branch (..),
-    LanguageSMTBranches (..),
   )
 where
 

src/Pirouette/Symbolic/Eval.hs

@@ -88,7 +88,7 @@ deriving instance PirouetteReadDefs lang m => PirouetteReadDefs lang (SymEvalT l
 deriving instance MonadError e m => MonadError e (SymEvalT lang m)
 
 type SymEvalConstr lang m =
-  (PirouetteDepOrder lang m, LanguagePretty lang, SMT.LanguageSMTBranches lang, MonadFail m, MonadIO m)
+  (PirouetteDepOrder lang m, LanguagePretty lang, LanguageSymEval lang, MonadFail m, MonadIO m)
 
 symevalT ::
   (SymEvalConstr lang m) =>
@@ -269,7 +269,7 @@ symEvalOneStep t@(R.App hd args) = case hd of
           case c' of
             Left _ -> pure Nothing
             Right (d, _) -> pure $ Just d
-    mayBranches <- lift $ SMT.branchesBuiltinTerm @lang builtin translator args
+    mayBranches <- lift $ branchesBuiltinTerm @lang builtin translator args
     case mayBranches of
       -- if successful, open all the branches
       Just branches -> asum $

src/Pirouette/Symbolic/Eval/Types.hs

@@ -1,24 +1,56 @@
-{-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE RecordWildCards #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE DeriveTraversable #-}
-{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE MonoLocalBinds #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE UndecidableInstances #-}
+
 module Pirouette.Symbolic.Eval.Types where
 
 import Data.Data hiding (eqT)
 import qualified Data.Map.Strict as M
+import qualified Data.Set as S
 import Data.String (IsString)
+import Pirouette.Monad
 import qualified Pirouette.SMT.Base as SMT
 import qualified Pirouette.SMT.Constraints as SMT
 import Pirouette.Term.Syntax
 import Prettyprinter hiding (Pretty (..))
-import qualified Data.Set as S
-
--- import Debug.Trace (trace)
+import qualified PureSMT
+
+-- | The 'LanguageSymEval' class is used to instruct the symbolic evaluator on how to branch on certain builtins.
+-- It is inherently different from 'SMT.LanguageSMT' in the sense that, for instance, the 'SMT.LanguageSMT'
+-- translation of a primitive @if@ statement might use the @ifthenelse@ SMT primitive. However, the
+-- 'LanguageSymEval' should instruct the symbolic evaluation engine on how to branch when that primitive is found.
+-- In particular, two branches should be created:
+--
+--   1. Add @condition = True@ to the list of known things, continue with the then term,
+--   2. Add @condition = False@ to the list of known things, continue with the else term.
+--
+-- This is the topmost class in the Pirouette universe, the relation between all the classes is:
+--
+-- > LanguageBuiltins --> defines the built-ins (both terms and types)
+-- >   |     \
+-- >   |      LanguageBuiltinTypes --> defines the typing rules of each built-in term
+-- >   |
+-- > LanguageSMT --> defines translation of built-ins into SMT
+-- >   |             (not every term can be translated)
+-- >   |
+-- > LanguageSymEval --> defines at which points the symbolic evaluator has to do sth. special
+class (SMT.LanguageSMT lang) => LanguageSymEval lang where
+  -- | Injection of different cases in the symbolic evaluator.
+  -- For example, one can introduce a 'if_then_else' built-in
+  -- and implement this method to look at both possibilities.
+  branchesBuiltinTerm ::
+    (SMT.ToSMT meta, PirouetteReadDefs lang m) =>
+    BuiltinTerms lang ->
+    (TermMeta lang meta -> m (Maybe PureSMT.SExpr)) ->
+    [ArgMeta lang meta] ->
+    m (Maybe [SMT.Branch lang meta])
+  branchesBuiltinTerm _ _ _ = pure Nothing
 
 newtype SymVar = SymVar {symVar :: Name}
   deriving (Eq, Show, Data, Typeable, IsString)

src/Pirouette/Symbolic/Prover/Runner.hs

@@ -6,7 +6,6 @@ module Pirouette.Symbolic.Prover.Runner where
 
 import Control.Monad.Reader
 import Pirouette.Monad
-import Pirouette.SMT.Constraints
 import Pirouette.Symbolic.Eval
 import Pirouette.Symbolic.Prover
 import Pirouette.Term.Syntax.Base
@@ -33,7 +32,7 @@ data IncorrectnessParams lang = IncorrectnessParams
   }
 
 runIncorrectnessLogic ::
-  (LanguagePretty lang, LanguageBuiltinTypes lang, LanguageSMTBranches lang) =>
+  (LanguagePretty lang, LanguageBuiltinTypes lang, LanguageSymEval lang) =>
   IncorrectnessParams lang ->
   IO (IncorrectnessResult lang)
 runIncorrectnessLogic
@@ -76,7 +75,7 @@ assertIRResult _ = return ()
 -- | Check for counterexamples for an incorrectness logic triple and
 -- pretty-print the result
 replIncorrectnessLogic ::
-  (LanguagePretty lang, LanguageBuiltinTypes lang, LanguageSMTBranches lang) =>
+  (LanguagePretty lang, LanguageBuiltinTypes lang, LanguageSymEval lang) =>
   IncorrectnessParams lang ->
   IO ()
 replIncorrectnessLogic params@IncorrectnessParams {..} =
@@ -85,7 +84,7 @@ replIncorrectnessLogic params@IncorrectnessParams {..} =
 -- | Assert a test failure (Tasty HUnit integration) when the result of the
 -- incorrectness logic execution reveals an error or a counterexample.
 assertIncorrectnessLogic ::
-  (LanguagePretty lang, LanguageBuiltinTypes lang, LanguageSMTBranches lang) =>
+  (LanguagePretty lang, LanguageBuiltinTypes lang, LanguageSymEval lang) =>
   IncorrectnessParams lang ->
   Test.Assertion
 assertIncorrectnessLogic params =