Remove explicit import lists for qualified imports

.github/workflows/main.yml

@@ -68,8 +68,13 @@ jobs:
 
       - name: Install SMT solvers
         run: |
+          echo "${{ secrets.MATHSAT_INSTALL_DEPLOY_KEY }}" >> mathsat_id_ed25519
+          chmod 400 mathsat_id_ed25519
+          ssh-agent bash -c 'ssh-add mathsat_id_ed25519; git clone git@github.com:NethermindEth/mathsat-install.git'
+          cp mathsat-install/install-mathsat.sh ./scripts/ci/install-mathsat.sh
           sh ./scripts/ci/install-z3-linux-amd64.sh
           sh ./scripts/ci/install-cvc5-linux.sh
+          sh ./scripts/ci/install-mathsat.sh
 
       - uses: actions/setup-python@v4
         with:

README.md

@@ -1037,6 +1037,45 @@ please open an issue!
 Horus does not yet fully support account contracts compiled with the
 `--account_contract` CLI flag.
 
+#### Why am I seeing `Unexpected annotation type` or `annotation is not allowed here` in my commented-out code?
+
+This can sometimes happen when you comment-out a function, but not its
+annotations (which are themselves already comments). It can also happen when
+you comment out a decorator, like `@external` (because then it looks like a
+Horus annotation: `// @external`).
+
+Make sure to add another set of `///` characters in front of any annotations
+that were associated with your commented-out function. Suppose we want to
+comment out an annotated function like this:
+```cairo
+// @pre x == 0
+// @post 0 == 1
+@external
+func f(x : felt) -> felt {
+    return 0;
+}
+```
+
+Instead of:
+```cairo
+// @pre x == 0
+// @post 0 == 1
+// @external
+// func f(x : felt) -> felt {
+//     return 0;
+// }
+```
+
+Try:
+```cairo
+/// // @pre x == 0
+/// // @post 0 == 1
+/// @external
+/// func f(x : felt) -> felt {
+///     return 0;
+}
+```
+
 
 ## Usage
 
@@ -1478,6 +1517,89 @@ Apart from `GlobalL`, there are several other sub-DSLs, which include:
   for a given module.
 * `PreprocessorL` -- preprocesses and runs SMT queries.
 
+### `CairoSemanticsL`
+
+As mentioned above, the purpose of the `CairoSemanticsL` eDSL is to construct
+the set of constraints which we will eventually transform into a solver query.
+
+At the time of writing, this is represented in a record type called
+`ConstraintsState`, which looks like this:
+
+```haskell
+data ConstraintsState = ConstraintsState
+  { cs_memoryVariables :: [MemoryVariable]
+  , cs_asserts :: [(AssertionBuilder, AssertionType)]
+  , cs_expects :: [(Expr TBool, AssertionType)]
+  , cs_nameCounter :: Int
+  , cs_callStack :: CallStack
+  }
+```
+
+So the asserts and expects are basically boolean expressions, and the
+preconditions and postconditions are encoded here. We have a list of memory
+variables as well. A memory variable is defined as follows:
+
+```haskell
+data MemoryVariable = MemoryVariable
+  { mv_varName :: Text
+  , mv_addrName :: Text
+  , mv_addrExpr :: Expr TFelt
+  }
+  deriving (Show)
+```
+
+We have a variable name, an address name, and an address expression, which
+is a felt. This is just an association between some variable name and an
+address in memory, along with its contents.
+
+When we print a memory variable, we see something like this:
+```console
+MEM!27 : (ap!<112=addr/root>@5 + 35)
+```
+The `27` in `MEM!27` is just a way to identify distinct memory variables. The
+`ap` stands for [allocation
+pointer](https://starknet.io/docs/how_cairo_works/cairo_intro.html#registers),
+and this indicates that this is the address in memory of some felt pushed on to
+the stack within a function body. The `@5` indicates the AP tracking group of
+this memory variable. The `+ 35` is the offset, specifically the offset from
+the beginning of the function context. Thus, an offset of `+ 0` indicates the
+first thing pushed onto the memory stack within that context.
+
+Here's an example:
+```cairo
+func foo:
+  [ap] = 0, ap++;  // <- this will be <foo/root>@x + 0
+  [ap] = 42, ap++; // <- this will be <foo/root>@x + 1
+  call bar;        // <- ^ now we're fp<bar/foo/root> + 0 and e.g. fp<bar/foo/root< - 3 = <foo/root>@x + 1 (remember call pushes 2 things on the stack)
+```
+
+The stuff in angle brackets, `<112=addr/root>`, is the current execution
+context, i.e. the stack frame. Each function call gets its own stack frame. The
+`addr/root` part is a representation of the call stack itself, where `root` is
+the execution context of top-level functions and subsequent stack frames are
+prepended, delimited with a `/`. The `112` is the program counter value, which
+tells us the instruction at which the current function was invoked.
+
+For example, consider:
+```cairo
+func foo [inlinable]             		root
+func bar [inlinable]
+
+func baz:
+  call bar -- inlining, push bar -> bar/root
+    ... (body of bar)
+    ret                 pop      -> root
+  ...
+  call foo -- inlining, push foo -> foo/root
+    ... (body of foo)
+    ret                 pop      -> root
+  ...
+```
+
+The stuff in the right-hand column is the context we're executing within. So
+when you refer to memory cells that have `<foo/root>`, you're referring to them
+from within the inlined function `foo`.
+
 ### Glossary
 
 * **contract** - a Starknet smart contract.

src/Horus/CFGBuild.hs

@@ -25,8 +25,8 @@ import Data.Coerce (coerce)
 import Data.Foldable (forM_, for_, toList)
 import Data.Functor ((<&>))
 import Data.List.NonEmpty (NonEmpty (..))
-import Data.List.NonEmpty qualified as NonEmpty (last, reverse, (<|))
-import Data.Map qualified as Map (lookup, toList)
+import Data.List.NonEmpty qualified as NonEmpty
+import Data.Map qualified as Map
 import Data.Maybe (isJust)
 import Data.Set (Set)
 import Data.Set qualified as Set

src/Horus/CFGBuild/Runner.hs

@@ -13,9 +13,9 @@ import Control.Monad.Reader (ReaderT, ask, asks, runReaderT)
 import Control.Monad.State (State, get, gets, runState)
 import Data.List (union)
 import Data.Map (Map)
-import Data.Map qualified as Map (empty)
+import Data.Map qualified as Map
 import Data.Text (Text)
-import Data.Text qualified as Text (pack)
+import Data.Text qualified as Text
 import Lens.Micro (Lens', at, (&), (^.), _Just)
 import Lens.Micro.GHC ()
 import Lens.Micro.Mtl ((%=), (<%=))

src/Horus/CairoSemantics.hs

@@ -16,11 +16,11 @@ import Data.Foldable (for_, toList, traverse_)
 import Data.Functor (($>), (<&>))
 import Data.List (tails)
 import Data.List.NonEmpty (NonEmpty, nonEmpty)
-import Data.List.NonEmpty qualified as NonEmpty (head, last, tail, toList)
+import Data.List.NonEmpty qualified as NonEmpty
 import Data.Map (Map)
-import Data.Map qualified as Map ((!?))
+import Data.Map qualified as Map
 import Data.Maybe (fromMaybe, isJust)
-import Data.Set qualified as Set (Set, member)
+import Data.Set qualified as Set
 import Data.Text (Text)
 import Data.Traversable (for)
 import Lens.Micro ((^.), _1)
@@ -59,12 +59,12 @@ import Horus.Label (Label (..), tShowLabel)
 import Horus.Module (Module (..), apEqualsFp, isPreChecking)
 import Horus.Program (ApTracking (..))
 import Horus.SW.Builtin (Builtin, BuiltinOffsets (..))
-import Horus.SW.Builtin qualified as Builtin (name)
+import Horus.SW.Builtin qualified as Builtin
 import Horus.SW.FuncSpec (FuncSpec (..), FuncSpec', toFuncSpec)
 import Horus.SW.ScopedName (ScopedName)
-import Horus.SW.ScopedName qualified as ScopedName (fromText)
+import Horus.SW.ScopedName qualified as ScopedName
 import Horus.SW.Storage (Storage)
-import Horus.SW.Storage qualified as Storage (equivalenceExpr)
+import Horus.SW.Storage qualified as Storage
 import Horus.Util (enumerate, safeLast, tShow, whenJust, whenJustM)
 
 data MemoryVariable = MemoryVariable

src/Horus/CairoSemantics/Runner.hs

@@ -20,13 +20,13 @@ import Control.Monad.State (MonadState (get), State, runState)
 import Data.Foldable (toList)
 import Data.Function ((&))
 import Data.Functor (($>))
-import Data.List qualified as List (find, tails)
-import Data.Map qualified as Map (map, null, unionWith)
+import Data.List qualified as List
+import Data.Map qualified as Map
 import Data.Maybe (mapMaybe)
 import Data.Singletons (sing)
 import Data.Some (foldSome)
 import Data.Text (Text)
-import Data.Text qualified as Text (intercalate)
+import Data.Text qualified as Text
 import Lens.Micro (Lens', (%~), (<&>), (^.))
 import Lens.Micro.GHC ()
 import Lens.Micro.Mtl (use, (%=), (.=), (<%=))
@@ -43,9 +43,9 @@ import Horus.Expr.Type (STy (..))
 import Horus.Expr.Util (gatherNonStdFunctions)
 import Horus.Expr.Vars (prime, rcBound)
 import Horus.FunctionAnalysis (ScopedFunction (sf_scopedName))
-import Horus.SW.Builtin qualified as Builtin (rcBound)
+import Horus.SW.Builtin qualified as Builtin
 import Horus.SW.Storage (Storage)
-import Horus.SW.Storage qualified as Storage (read)
+import Horus.SW.Storage qualified as Storage
 import Horus.Util (tShow)
 
 data AssertionBuilder

src/Horus/Command/SMT.hs

@@ -6,10 +6,10 @@ import SimpleSMT qualified as SMT
 import Text.Printf (printf)
 
 import Horus.Expr (Expr)
-import Horus.Expr.SMT qualified as Expr (toSMT)
+import Horus.Expr.SMT qualified as Expr
 import Horus.Expr.Std (Function (..))
 import Horus.Expr.Type (Ty (..))
-import Horus.Expr.Type.SMT qualified as Ty (toSMT)
+import Horus.Expr.Type.SMT qualified as Ty
 
 declare :: forall ty. Function ty -> Text
 declare (Function name) = pack (printf "(declare-fun %s (%s) %s)" name args res)

src/Horus/ContractInfo.hs

@@ -18,7 +18,7 @@ import Horus.Instruction (LabeledInst, callDestination, isRet, labelInstructions
 import Horus.Label (Label)
 import Horus.Program (ApTracking, DebugInfo (..), FlowTrackingData (..), ILInfo (..), Identifiers, Program (..), sizeOfType)
 import Horus.SW.Builtin (Builtin, BuiltinOffsets (..))
-import Horus.SW.Builtin qualified as Builtin (ptrName)
+import Horus.SW.Builtin qualified as Builtin
 import Horus.SW.CairoType (CairoType (..))
 import Horus.SW.FuncSpec
   ( FuncSpec (..)

src/Horus/Expr/SMT.hs

@@ -24,10 +24,10 @@ import Data.Constraint ((\\))
 import Data.Foldable (foldl')
 import Data.List.NonEmpty (NonEmpty (..))
 import Data.Map (Map)
-import Data.Map qualified as Map (empty, fromList)
+import Data.Map qualified as Map
 import Data.Some (Some (..), withSomeM)
 import Data.Text (Text, pack, unpack)
-import Data.Text qualified as Text (concat)
+import Data.Text qualified as Text
 import Data.Typeable (Typeable)
 import Lens.Micro (at, non, (&))
 import Lens.Micro.GHC ()

src/Horus/Expr/Util.hs

@@ -13,7 +13,7 @@ import Data.Set (Set)
 import Data.Set qualified as Set
 import Data.Some (Some (..))
 import Data.Text (Text)
-import Data.Text qualified as Text (isPrefixOf)
+import Data.Text qualified as Text
 import Data.Typeable (eqT, (:~:) (Refl))
 
 import Horus.Expr (Expr (..), isProper, transform_, (.&&), (.<), (.<=))

src/Horus/Expr/Vars.hs

@@ -34,7 +34,7 @@ import Horus.Expr qualified as Expr
 import Horus.Expr.Std (stdNames)
 import Horus.Instruction (PointerRegister (..))
 import Horus.SW.Builtin (Builtin (..))
-import Horus.SW.Builtin qualified as Builtin (name)
+import Horus.SW.Builtin qualified as Builtin
 
 prime :: Expr TFelt
 prime = Expr.const "prime"

src/Horus/FunctionAnalysis.hs

@@ -17,6 +17,9 @@ module Horus.FunctionAnalysis
   , isAuxFunc
   , scopedFOfPc
   , uncheckedScopedFOfPc
+  , functionsOf
+  , callgraph
+  , graphOfCG
   )
 where
 
@@ -25,7 +28,7 @@ import Control.Monad (liftM2, (<=<))
 import Data.Array (assocs)
 import Data.Coerce (coerce)
 import Data.Function ((&))
-import Data.Graph (Graph, Vertex, graphFromEdges', reachable)
+import Data.Graph (Graph, Vertex, graphFromEdges, reachable)
 import Data.List (foldl', sort, union)
 import Data.Map qualified as Map
   ( Map
@@ -109,8 +112,8 @@ cgMbInsertArc (CG verts arcs) (fro, to) =
     then Nothing
     else Just . CG verts $ Map.insertWith (++) fro [to] arcs
 
-graphOfCG :: CG -> (Graph, Vertex -> (Label, Label, [Label]))
-graphOfCG cg = graphFromEdges' . map named . Map.assocs $ cg_arcs cg
+graphOfCG :: CG -> (Graph, Vertex -> (Label, Label, [Label]), Label -> Maybe Vertex)
+graphOfCG cg = graphFromEdges . map named . Map.assocs $ cg_arcs cg
  where
   named (fro, tos) = (fro, fro, tos)
 
@@ -121,7 +124,7 @@ cycles g = map fst . filter (uncurry reachableSet) $ assocs g
 
 cyclicVerts :: CG -> [Label]
 cyclicVerts cg =
-  let (graph, vertToNode) = graphOfCG cg
+  let (graph, vertToNode, _) = graphOfCG cg
    in map ((\(lbl, _, _) -> lbl) . vertToNode) (cycles graph)
 
 pcToFunOfProg :: Program -> Map.Map Label ScopedFunction
@@ -243,6 +246,11 @@ isNotAnnotated cd = not . maybe False isAnnotated' . labelOfIdent
 wrapperScope :: Text
 wrapperScope = "__wrappers__"
 
+-- Identify decorator-generated wrapper functions.
+--
+-- If you write e.g. @extern, this means can be called externally, generates a
+-- wrapper function. We *don't* want to verify wrapper functions, so we want to
+-- be able to identify and exclude these.
 isWrapper :: ScopedFunction -> Bool
 isWrapper f = outerScope (sf_scopedName f) == wrapperScope
  where
@@ -271,18 +279,13 @@ isGeneratedName fname cd = fname `elem` generatedNames
 isSvarFunc :: ScopedName -> ContractDefinition -> Bool
 isSvarFunc fname cd = isGeneratedName fname cd || fname `elem` [fStorageRead, fStorageWrite]
 
-fHash2 :: ScopedName
-fHash2 = ScopedName ["starkware", "cairo", "common", "hash", "hash2"]
-
-fAssert250bit :: ScopedName
-fAssert250bit = ScopedName ["starkware", "cairo", "common", "math", "assert_250_bit"]
-
-fNormalizeAddress :: ScopedName
-fNormalizeAddress = ScopedName ["starkware", "starknet", "common", "storage", "normalize_address"]
-
 isAuxFunc :: ScopedFunction -> ContractDefinition -> Bool
 isAuxFunc (ScopedFunction fname _) cd =
   isSvarFunc fname cd || fname `elem` [fHash2, fAssert250bit, fNormalizeAddress]
+ where
+  fHash2 = ScopedName ["starkware", "cairo", "common", "hash", "hash2"]
+  fAssert250bit = ScopedName ["starkware", "cairo", "common", "math", "assert_250_bit"]
+  fNormalizeAddress = ScopedName ["starkware", "starknet", "common", "storage", "normalize_address"]
 
 sizeOfCall :: Int
 sizeOfCall = 2
@@ -302,11 +305,15 @@ inlinableFuns rows prog cd =
   idents = p_identifiers prog
   functions = functionsOf rows prog
   notIsAnnotated sf = maybe False (isNotAnnotated cd) . Map.lookup (sf_scopedName sf) $ idents
+
+  -- Annotated *later* by horus-checker because they come from e.g. the
+  -- standard library. These are things with default specs.
   notIsAnnotatedLater f = sf_scopedName f `notElem` map fst stdSpecsList
   localCycles = Map.map (cyclicVerts . jumpgraph)
-  isAcylic cyclicFuns f cyclicLbls = f `notElem` cyclicFuns && null cyclicLbls
+  isAcyclic cyclicFuns f cyclicLbls = f `notElem` cyclicFuns && null cyclicLbls
+  -- The functions that contain neither global nor local cycles.
   inlinable =
-    Map.keys . Map.filterWithKey (isAcylic . cyclicVerts $ callgraph (Map.mapKeys sf_pc functions)) $
+    Map.keys . Map.filterWithKey (isAcyclic . cyclicVerts $ callgraph (Map.mapKeys sf_pc functions)) $
       Map.mapKeys sf_pc (localCycles functions)
 
 uninlinableFuns :: [LabeledInst] -> Program -> ContractDefinition -> Map.Map ScopedFunction [LabeledInst]