From 57af94978f87d9f0e58912fafb58988ddeea1364 Mon Sep 17 00:00:00 2001
From: Ferinko <silvasi.frantisek@gmail.com>
Date: Mon, 6 Feb 2023 18:00:21 +0100
Subject: [PATCH 1/7] Don't verify `@external`-generated wrapper functions

In this commit, we add a function `userAnnotatedSources` which replaces
`isStandardSource`. It generates a list of all the user annotated
ScopedFunctions. This list is used to filter modules for solving. This
requires a slight refactor within `FunctionAnalysis.hs`.

* Add `extern_remove_dirty` test.

The basic idea is this:
1. Find all wrapper functions.
2. Compute their respective set of reachable functions.
3. Mark them all as 'don't check' unless they are referenced from a
   different source as well.
---
 src/Horus/FunctionAnalysis.hs                 | 28 ++++++++--------
 src/Horus/Global.hs                           | 33 +++++++++++++++----
 .../golden/extern_remove_dirty.cairo          | 12 +++++++
 .../resources/golden/extern_remove_dirty.gold |  2 ++
 4 files changed, 53 insertions(+), 22 deletions(-)
 create mode 100644 tests/resources/golden/extern_remove_dirty.cairo
 create mode 100644 tests/resources/golden/extern_remove_dirty.gold

diff --git a/src/Horus/FunctionAnalysis.hs b/src/Horus/FunctionAnalysis.hs
index a283f2ee..f068eb05 100644
--- a/src/Horus/FunctionAnalysis.hs
+++ b/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
@@ -271,18 +274,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
@@ -304,9 +302,9 @@ inlinableFuns rows prog cd =
   notIsAnnotated sf = maybe False (isNotAnnotated cd) . Map.lookup (sf_scopedName sf) $ idents
   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
   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]
diff --git a/src/Horus/Global.hs b/src/Horus/Global.hs
index d902ec10..43c4a9e2 100644
--- a/src/Horus/Global.hs
+++ b/src/Horus/Global.hs
@@ -16,10 +16,12 @@ import Control.Monad (when)
 import Control.Monad.Except (MonadError (..))
 import Control.Monad.Free.Church (F, liftF)
 import Data.Foldable (for_)
-import Data.List (groupBy)
-import Data.Maybe (fromMaybe)
+import Data.Graph (reachable)
+import Data.List (groupBy, partition)
+import Data.Map qualified as Map
+import Data.Maybe (fromJust, fromMaybe)
 import Data.Set (Set, singleton, toAscList, (\\))
-import Data.Set qualified as Set (map)
+import Data.Set qualified as Set (fromList, map, member)
 import Data.Text (Text, unpack)
 import Data.Text qualified as Text (isPrefixOf)
 import Data.Traversable (for)
@@ -37,7 +39,7 @@ import Horus.CairoSemantics.Runner
 import Horus.CallStack (CallStack, initialWithFunc)
 import Horus.Expr qualified as Expr
 import Horus.Expr.Util (gatherLogicalVariables)
-import Horus.FunctionAnalysis (ScopedFunction (ScopedFunction, sf_pc), isWrapper)
+import Horus.FunctionAnalysis (ScopedFunction (ScopedFunction, sf_pc), callgraph, functionsOf, graphOfCG, isWrapper)
 import Horus.Logger qualified as L (LogL, logDebug, logError, logInfo, logWarning)
 import Horus.Module (Module (..), ModuleL, gatherModules, getModuleNameParts)
 import Horus.Preprocessor (HorusResult (..), PreprocessorL, SolverResult (..), goalListToTextList, optimizeQuery, solve)
@@ -49,6 +51,7 @@ import Horus.SW.Identifier (Function (..))
 import Horus.SW.ScopedName (ScopedName ())
 import Horus.SW.Std (trustedStdFuncs)
 import Horus.Util (tShow, whenJust)
+import Lens.Micro ((^.), _3)
 
 data Config = Config
   { cfg_verbose :: Bool
@@ -329,6 +332,7 @@ collapseAllUnsats infos@(SolvingInfo _ funcName result _ _ : _)
 
 {- | Return a solution of SMT queries corresponding with the contract.
 
+
   For the purposes of reporting results,
   we also remember which SMT query corresponding to a function was inlined.
 -}
@@ -343,7 +347,8 @@ solveContract = do
   let fs = toAscList inlinables
   cfgs <- for fs $ \f -> runCFGBuildL (buildCFG lInstructions $ inlinables \\ singleton f)
   for_ cfgs verbosePrint
-  modules <- concat <$> for ((cfg, isStandardSource inlinables) : zip cfgs (map (==) fs)) makeModules
+  sources <- userAnnotatedSources inlinables lInstructions
+  modules <- concat <$> for ((cfg, (`elem` sources)) : zip cfgs (map (==) fs)) makeModules
 
   identifiers <- getIdentifiers
   let isUntrusted :: Module -> Bool
@@ -359,8 +364,22 @@ solveContract = do
     )
       infos
  where
-  isStandardSource :: Set ScopedFunction -> ScopedFunction -> Bool
-  isStandardSource inlinables f = f `notElem` inlinables && not (isWrapper f)
+  userAnnotatedSources :: Set ScopedFunction -> [LabeledInst] -> GlobalL (Set ScopedFunction)
+  userAnnotatedSources inlinableFs rows =
+    getProgram >>= \prog ->
+      let functionsWithBodies = functionsOf rows prog
+          functions = Map.keys functionsWithBodies
+          (cg, vToLbl, lblToV) = graphOfCG . callgraph . Map.mapKeys sf_pc $ functionsWithBodies
+          (wrapperFunctions, nonwrapperFunctions) = partition isWrapper functions
+          reachableLabelsFromWrappers =
+            Set.fromList
+              . concatMap (concatMap ((^. _3) . vToLbl) . reachable cg . fromJust . lblToV . sf_pc)
+              $ wrapperFunctions
+          calledByWrappers =
+            Set.fromList
+              [ sf | sf <- functions, sf_pc sf `Set.member` reachableLabelsFromWrappers
+              ]
+       in pure (Set.fromList nonwrapperFunctions \\ inlinableFs \\ calledByWrappers)
 
   sameFuncName :: SolvingInfo -> SolvingInfo -> Bool
   sameFuncName (SolvingInfo _ nameA _ _ _) (SolvingInfo _ nameB _ _ _) = nameA == nameB
diff --git a/tests/resources/golden/extern_remove_dirty.cairo b/tests/resources/golden/extern_remove_dirty.cairo
new file mode 100644
index 00000000..0c2eb3e9
--- /dev/null
+++ b/tests/resources/golden/extern_remove_dirty.cairo
@@ -0,0 +1,12 @@
+%lang starknet
+
+@external
+func f() -> (array_len : felt, array : felt*) {
+    alloc_locals;
+    // An array of felts.
+    local felt_array: felt*;
+    assert felt_array[0] = 0;
+    assert felt_array[1] = 1;
+    assert felt_array[2] = 2;
+    return (array_len=3, array=felt_array);
+}
\ No newline at end of file
diff --git a/tests/resources/golden/extern_remove_dirty.gold b/tests/resources/golden/extern_remove_dirty.gold
new file mode 100644
index 00000000..8cfd00e4
--- /dev/null
+++ b/tests/resources/golden/extern_remove_dirty.gold
@@ -0,0 +1,2 @@
+f [inlined]
+Verified
\ No newline at end of file

From ba9abf3ecd1ec60be669a046d56da888a9269cc6 Mon Sep 17 00:00:00 2001
From: Malcolm Langfield <35980963+langfield@users.noreply.github.com>
Date: Fri, 17 Feb 2023 10:19:25 -0500
Subject: [PATCH 2/7] Add `README.md` section on details of `CairoSemanticsL`

---
 README.md | 83 +++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 83 insertions(+)

diff --git a/README.md b/README.md
index 310fc461..5eb87561 100644
--- a/README.md
+++ b/README.md
@@ -1478,6 +1478,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.

From 2485f9e5ec5e3fd11235029b9394b390c86735c1 Mon Sep 17 00:00:00 2001
From: Malcolm Langfield <35980963+langfield@users.noreply.github.com>
Date: Fri, 16 Dec 2022 10:26:49 -0500
Subject: [PATCH 3/7] Add some high-level comments in `FunctionAnalysis.hs` and
 `Global.hs`.

---
 src/Horus/FunctionAnalysis.hs | 9 +++++++++
 src/Horus/Global.hs           | 4 ++++
 2 files changed, 13 insertions(+)

diff --git a/src/Horus/FunctionAnalysis.hs b/src/Horus/FunctionAnalysis.hs
index f068eb05..b9ace7de 100644
--- a/src/Horus/FunctionAnalysis.hs
+++ b/src/Horus/FunctionAnalysis.hs
@@ -246,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
@@ -300,9 +305,13 @@ 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)
   isAcyclic cyclicFuns f cyclicLbls = f `notElem` cyclicFuns && null cyclicLbls
+  -- The functions that contain neither global nor local cycles.
   inlinable =
     Map.keys . Map.filterWithKey (isAcyclic . cyclicVerts $ callgraph (Map.mapKeys sf_pc functions)) $
       Map.mapKeys sf_pc (localCycles functions)
diff --git a/src/Horus/Global.hs b/src/Horus/Global.hs
index 43c4a9e2..dadecf6e 100644
--- a/src/Horus/Global.hs
+++ b/src/Horus/Global.hs
@@ -340,6 +340,10 @@ solveContract :: GlobalL [SolvingInfo]
 solveContract = do
   lInstructions <- getLabelledInstructions
   inlinables <- getInlinables
+  -- We take a function that was inlined away, pretend it is *not* inlinable,
+  -- since want to do analysis on it in isolation, which we must do for every
+  -- function. And we do this because we want a judgement for each so that we
+  -- don't propagate errors upward when we inline stuff.
   cfg <- runCFGBuildL $ buildCFG lInstructions inlinables
   verbosePrint cfg
 

From c63f054bb8cc0552bd4cafec9cb99294ff4d58ab Mon Sep 17 00:00:00 2001
From: langfield <35980963+langfield@users.noreply.github.com>
Date: Mon, 30 Jan 2023 11:06:56 -0500
Subject: [PATCH 4/7] Add FAQ about commenting-out annotations

---
 README.md | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

diff --git a/README.md b/README.md
index 310fc461..a0842377 100644
--- a/README.md
+++ b/README.md
@@ -1037,6 +1037,29 @@ 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). Make sure to add another
+set of `//` characters in front of any annotations that were associated with
+your commented-out function. Instead of:
+```cairo
+// @pre x == 0
+// @post 0 == 1
+// func f(x : felt) -> felt {
+//     return 0;
+// }
+```
+
+Try:
+```cairo
+// // @pre x == 0
+// // @post 0 == 1
+// func f(x : felt) -> felt {
+//     return 0;
+// }
+```
+
 
 ## Usage
 

From 18d43a8ca7dc2499ca09a5379c51c7f625c3ef8f Mon Sep 17 00:00:00 2001
From: Malcolm Langfield <35980963+langfield@users.noreply.github.com>
Date: Fri, 3 Feb 2023 13:44:19 -0500
Subject: [PATCH 5/7] Add `@external` decorator to code-commenting FAQ

---
 README.md | 32 ++++++++++++++++++++++++--------
 1 file changed, 24 insertions(+), 8 deletions(-)

diff --git a/README.md b/README.md
index a0842377..68484f53 100644
--- a/README.md
+++ b/README.md
@@ -1040,12 +1040,27 @@ Horus does not yet fully support account contracts compiled with the
 #### 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). Make sure to add another
-set of `//` characters in front of any annotations that were associated with
-your commented-out function. Instead of:
+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;
 // }
@@ -1053,11 +1068,12 @@ your commented-out function. Instead of:
 
 Try:
 ```cairo
-// // @pre x == 0
-// // @post 0 == 1
-// func f(x : felt) -> felt {
-//     return 0;
-// }
+/// // @pre x == 0
+/// // @post 0 == 1
+/// @external
+/// func f(x : felt) -> felt {
+///     return 0;
+}
 ```
 
 

From 7e8c615f0eed1cbd8049ae1c6184f71c63fa7fd7 Mon Sep 17 00:00:00 2001
From: Malcolm Langfield <35980963+langfield@users.noreply.github.com>
Date: Tue, 28 Mar 2023 07:58:54 -0400
Subject: [PATCH 6/7] Add mathsat installation to Github actions workflow

* Use `ssh-agent` to clone with specific private key
* Set `0o400` permissions on private key file
* Add `mathsat` to list of solvers used in tests
---
 .github/workflows/main.yml    | 5 +++++
 tests/resources/bats-template | 2 +-
 2 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index c6a8cd06..486a9c14 100644
--- a/.github/workflows/main.yml
+++ b/.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:
diff --git a/tests/resources/bats-template b/tests/resources/bats-template
index e4da0475..db4506cc 100644
--- a/tests/resources/bats-template
+++ b/tests/resources/bats-template
@@ -26,7 +26,7 @@ test_case() {
     temp_file="${base}.temp"
 
     horus-compile "$test_file" --output "$compiled_file" --spec_output "$spec_file"
-    stack run horus-check "$compiled_file" "$spec_file" -- -s cvc5 -s z3 -t 100000 &> "$temp_file" || true
+    stack run horus-check "$compiled_file" "$spec_file" -- -s cvc5 -s mathsat -s z3 -t 100000 &> "$temp_file" || true
     compare "${gold_file}" "${temp_file}"
     rm "$compiled_file"
     rm "$spec_file"

From b96c5e8657515702883db40849aa1261c1e4e892 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Agust=C3=ADn=20Martinez=20Su=C3=B1=C3=A9?=
 <4691852+aemartinez@users.noreply.github.com>
Date: Thu, 19 Jan 2023 14:35:38 -0300
Subject: [PATCH 7/7] Add test cases for `@assert` notation

At a high-level, we add a bunch of tests and golds, break module name
formatting into two parts, and sort the `scopedNames` when constructing
module names.

This commit replaces the `normalizedName` function with several new
functions, removing use of partial helper functions like `init` and
`head`, and instead making use of `Data.List.NonEmpty`. The new
functions are:

* preprocessScopes
* formatScopes
* summarizeLabels

Additionally, we rename:
* summarizeLabels -> summarizeLabels'
* sansCommonAncestor -> detachCommonPrefix

This fixes a bug where a dot is not added between function name and
label for anonymous asserts.

We no longer generate the `prefix` and `labelsSummary` within the same
function, because that was kind of arbitrary.

Other things:

* Adjust gold files to remove assert label, inlined markers
* Add test `assert_let_minimal.cairo`
* Fix order of results in `assert_let.gold`

Notes from squashed intermediate commits
========================================
* Add precondition checking tags to golds
* Fix branch identifiers in golds
* Add `mathsat` back to `oneoff.sh` test running script.
* Fix `assert_let.gold`. It now correctly shows something other than
  `Verified` for the functions with faulty asserts. In particular, it
  shows `Contradictory premises`.
---
 src/Horus/Module.hs                           | 68 ++++++++++-------
 .../golden/assert_func_add_rec.cairo          | 73 +++++++++++++++++++
 .../resources/golden/assert_func_add_rec.gold | 63 ++++++++++++++++
 .../resources/golden/assert_func_chain.cairo  | 15 ++++
 tests/resources/golden/assert_func_chain.gold |  6 ++
 .../golden/assert_func_peano_prod.cairo       | 14 ++++
 .../golden/assert_func_peano_prod.gold        |  2 +
 .../resources/golden/assert_inline_many.cairo | 38 ++++++++++
 .../resources/golden/assert_inline_many.gold  | 15 ++++
 .../golden/assert_inline_pre_success.cairo    | 33 +++++++++
 .../golden/assert_inline_pre_success.gold     | 24 ++++++
 tests/resources/golden/assert_let.cairo       | 41 +++++++++++
 tests/resources/golden/assert_let.gold        | 26 +++++++
 .../resources/golden/assert_let_minimal.cairo |  7 ++
 .../resources/golden/assert_let_minimal.gold  |  2 +
 .../resources/golden/assert_lvar_basic.cairo  | 19 +++++
 tests/resources/golden/assert_lvar_basic.gold |  9 +++
 .../resources/golden/assert_lvar_struct.cairo | 22 ++++++
 .../resources/golden/assert_lvar_struct.gold  |  8 ++
 tests/resources/golden/assert_simple.cairo    | 31 ++++++++
 tests/resources/golden/assert_simple.gold     | 14 ++++
 .../golden/assert_stack_minimal.cairo         | 44 +++++++++++
 .../golden/assert_stack_minimal.gold          | 15 ++++
 tests/resources/golden/oneoff.sh              |  2 +-
 24 files changed, 564 insertions(+), 27 deletions(-)
 create mode 100644 tests/resources/golden/assert_func_add_rec.cairo
 create mode 100644 tests/resources/golden/assert_func_add_rec.gold
 create mode 100644 tests/resources/golden/assert_func_chain.cairo
 create mode 100644 tests/resources/golden/assert_func_chain.gold
 create mode 100644 tests/resources/golden/assert_func_peano_prod.cairo
 create mode 100644 tests/resources/golden/assert_func_peano_prod.gold
 create mode 100644 tests/resources/golden/assert_inline_many.cairo
 create mode 100644 tests/resources/golden/assert_inline_many.gold
 create mode 100644 tests/resources/golden/assert_inline_pre_success.cairo
 create mode 100644 tests/resources/golden/assert_inline_pre_success.gold
 create mode 100644 tests/resources/golden/assert_let.cairo
 create mode 100644 tests/resources/golden/assert_let.gold
 create mode 100644 tests/resources/golden/assert_let_minimal.cairo
 create mode 100644 tests/resources/golden/assert_let_minimal.gold
 create mode 100644 tests/resources/golden/assert_lvar_basic.cairo
 create mode 100644 tests/resources/golden/assert_lvar_basic.gold
 create mode 100644 tests/resources/golden/assert_lvar_struct.cairo
 create mode 100644 tests/resources/golden/assert_lvar_struct.gold
 create mode 100644 tests/resources/golden/assert_simple.cairo
 create mode 100644 tests/resources/golden/assert_simple.gold
 create mode 100644 tests/resources/golden/assert_stack_minimal.cairo
 create mode 100644 tests/resources/golden/assert_stack_minimal.gold

diff --git a/src/Horus/Module.hs b/src/Horus/Module.hs
index 900463c9..7faa2fbb 100644
--- a/src/Horus/Module.hs
+++ b/src/Horus/Module.hs
@@ -16,12 +16,14 @@ import Control.Monad (unless)
 import Control.Monad.Except (MonadError (..))
 import Control.Monad.Free.Church (F, liftF)
 import Data.Foldable (for_, traverse_)
-import Data.List.NonEmpty (NonEmpty)
+import Data.List qualified as L
+import Data.List.NonEmpty (NonEmpty (..))
+import Data.List.NonEmpty qualified as NE
 import Data.Map (Map)
-import Data.Map qualified as Map (elems, empty, insert, map, null, toList)
-import Data.Maybe (isJust)
+import Data.Map qualified as Map
+import Data.Maybe (isJust, mapMaybe)
 import Data.Text (Text)
-import Data.Text qualified as Text (concat, intercalate)
+import Data.Text qualified as Text (concat, intercalate, isPrefixOf)
 import Lens.Micro (ix, (^.))
 import Text.Printf (printf)
 
@@ -83,8 +85,8 @@ dropMain name = name
  example, `__main__.foo.bar` and `__main__.FOO.baz` you get a summarization
  of the scopes `fooFOO` and `bar|baz`.
 -}
-summarizeLabels :: [Text] -> Text
-summarizeLabels labels =
+summarizeLabels' :: [Text] -> Text
+summarizeLabels' labels =
   let prettyLabels = Text.intercalate "|" labels
    in if length labels == 1
         then prettyLabels
@@ -104,18 +106,22 @@ commonPrefix (x : xs) (y : ys)
  We do this by computing the longest common prefix, dropping it from all the
  names, and then adding the prefix itself as a new name.
 -}
-sansCommonAncestor :: [[Text]] -> [[Text]]
-sansCommonAncestor xss = prefix : remainders
+detachCommonPrefix :: [[Text]] -> [[Text]]
+detachCommonPrefix [] = []
+detachCommonPrefix (xs : xss) = prefix : remainders
  where
-  prefix = foldl1 commonPrefix xss
-  remainders = map (drop (length prefix)) xss
+  prefix = L.foldl' commonPrefix xs xss
+  remainders = map (drop (length prefix)) (xs : xss)
 
-{- | Returns the function name parts, in particular the fully qualified
- function name and the label summary.
+-- | Extract list of scopes from each ScopedName, dropping `__main__`.
+preprocessScopes :: [ScopedName] -> [NonEmpty Text]
+preprocessScopes = mapMaybe NE.nonEmpty . detachCommonPrefix . map (sn_path . dropMain)
 
- We take as arguments a list of scoped names, and a boolean flag indicating
- whether the list of scoped names belongs to a function or a *floating label*
- (as distinct from a function label).
+{- | Get the formatted scopes from the preprocessed list of scopes.
+
+ The `isFloatingLabel` parameter is a boolean flag indicating whether the list
+ of scoped names belongs to a function or a *floating label* (as distinct from
+ a function label).
 
  A floating label is, for example, `add:` in the snippet below, which is
  taken from the `func_multiple_ret.cairo` test file at revision 89ddeb2:
@@ -134,16 +140,24 @@ sansCommonAncestor xss = prefix : remainders
  Note: we say "fully qualified", but we remove the `__main__` prefix from
  top-level function names, if it exists.
 -}
-normalizedName :: [ScopedName] -> Bool -> (Text, Text)
-normalizedName scopedNames isFloatingLabel = (Text.concat scopes, labelsSummary)
+formatScopes :: [NonEmpty Text] -> Bool -> Text
+formatScopes [] _ = ""
+formatScopes (ys : yss) isFloatingLabel
+  | isAssertName end || isFloatingLabel = Text.intercalate "." $ NE.init $ concat' names
+  | otherwise = Text.intercalate "." $ map (Text.intercalate "." . NE.toList) (ys : yss)
  where
-  -- Extract list of scopes from each ScopedName, dropping `__main__`.
-  names = filter (not . null) $ sansCommonAncestor $ map (sn_path . dropMain) scopedNames
-  -- If we have a floating label, we need to drop the last scope, because it is
-  -- the label name itself.
-  scopes = map (Text.intercalate ".") (if isFloatingLabel then map init names else names)
-  -- This will almost always just be the name of the single label.
-  labelsSummary = if isFloatingLabel then summarizeLabels (map last names) else ""
+  names = ys :| yss
+  end = NE.last names
+
+  concat' :: NonEmpty (NonEmpty a) -> NonEmpty a
+  concat' (x :| xs) = L.foldl' (<>) x xs
+
+  isAssertName :: NonEmpty Text -> Bool
+  isAssertName xs = length xs == 1 && all ("!anonymous_assert_label" `Text.isPrefixOf`) xs
+
+summarizeLabels :: [NonEmpty Text] -> Bool -> Text
+summarizeLabels [] _ = ""
+summarizeLabels names isFloatingLabel = if isFloatingLabel then summarizeLabels' (map NE.last names) else ""
 
 descrOfBool :: Bool -> Text
 descrOfBool True = "1"
@@ -179,7 +193,7 @@ descrOfOracle oracle =
 
  Nested control flow results in multiple `1` or `2` characters.
 
- See `normalizedName` for the definition of a floating label. Here, the label
+ See `formatScopes` for the definition of a floating label. Here, the label
  is floating if it is not a function declaration (i.e. equal to `calledF`),
  since these are the only two types of labels we may encounter.
 
@@ -193,7 +207,9 @@ getModuleNameParts idents (Module spec prog oracle calledF _ mbPreCheckedFuncAnd
     Just label ->
       let scopedNames = labelNamesOfPc idents label
           isFloatingLabel = label /= calledF
-          (prefix, labelsSummary) = normalizedName scopedNames isFloatingLabel
+          scopes = preprocessScopes $ L.sort scopedNames
+          prefix = formatScopes scopes isFloatingLabel
+          labelsSummary = summarizeLabels scopes isFloatingLabel
        in (prefix, labelsSummary, descrOfOracle oracle, preCheckingSuffix)
  where
   post = fs_post spec
diff --git a/tests/resources/golden/assert_func_add_rec.cairo b/tests/resources/golden/assert_func_add_rec.cairo
new file mode 100644
index 00000000..57263157
--- /dev/null
+++ b/tests/resources/golden/assert_func_add_rec.cairo
@@ -0,0 +1,73 @@
+// @pre True
+// @post [ap - 1] == m + n
+func add(m: felt, n: felt) -> (res: felt) {
+    if (n == 0) {
+        // @assert n == 0
+        return (res=m);
+    } else {
+        // @assert n != 0
+        let (res1) = add(m, n - 1);
+        // @assert res1 == m + n - 1
+        let (res2) = inc(res1);
+        // @assert res2 == m + n
+        return (res=res2);
+    }
+}
+
+// @pre True
+// @post [ap - 1] == m + n
+func add_broken_1(m: felt, n: felt) -> (res: felt) {
+    if (n == 0) {
+        // @assert n != 0
+        return (res=m);
+    } else {
+        let (res1) = add(m, n - 1);
+        let (res2) = inc(res1);
+        return (res=res2);
+    }
+}
+
+// @pre True
+// @post [ap - 1] == m + n
+func add_broken_2(m: felt, n: felt) -> (res: felt) {
+    if (n == 0) {
+        return (res=m);
+    } else {
+        // @assert n == 0
+        let (res1) = add(m, n - 1);
+        let (res2) = inc(res1);
+        return (res=res2);
+    }
+}
+
+// @pre True
+// @post [ap - 1] == m + n
+func add_broken_3(m: felt, n: felt) -> (res: felt) {
+    if (n == 0) {
+        return (res=m);
+    } else {
+        let (res1) = add(m, n - 1);
+        // @assert res1 == m + n
+        let (res2) = inc(res1);
+        return (res=res2);
+    }
+}
+
+// @pre True
+// @post [ap - 1] == m + n
+func add_broken_4(m: felt, n: felt) -> (res: felt) {
+    if (n == 0) {
+        return (res=m);
+    } else {
+        let (res1) = add(m, n - 1);
+        let (res2) = inc(res1);
+        // @assert res2 == m
+        return (res=res2);
+    }
+}
+
+// @pre True
+// @post [ap - 1] == x + 1
+func inc(x: felt) -> (res: felt) {
+    return (res=x + 1);
+}
diff --git a/tests/resources/golden/assert_func_add_rec.gold b/tests/resources/golden/assert_func_add_rec.gold
new file mode 100644
index 00000000..d70dadce
--- /dev/null
+++ b/tests/resources/golden/assert_func_add_rec.gold
@@ -0,0 +1,63 @@
+add
+Verified
+
+add_broken_1:::1 Pre<add|<19=add/root>>
+Verified
+
+add_broken_1:::1 Pre<inc|<21=inc/root>>
+Verified
+
+add_broken_1:::1
+Verified
+
+add_broken_1:::2
+False
+
+add_broken_1.!anonymous_assert_label_4
+False
+
+add_broken_2:::1
+False
+
+add_broken_2.!anonymous_assert_label_5 Pre<add|<31=add/root>>
+Verified
+
+add_broken_2.!anonymous_assert_label_5 Pre<inc|<33=inc/root>>
+Verified
+
+add_broken_2.!anonymous_assert_label_5
+Verified
+
+add_broken_2:::2
+Verified
+
+add_broken_3:::1 Pre<add|<43=add/root>>
+Verified
+
+add_broken_3:::1
+False
+
+add_broken_3.!anonymous_assert_label_6 Pre<inc|<45=inc/root>>
+Verified
+
+add_broken_3.!anonymous_assert_label_6
+False
+
+add_broken_3:::2
+Verified
+
+add_broken_4:::1 Pre<add|<55=add/root>>
+Verified
+
+add_broken_4:::1 Pre<inc|<57=inc/root>>
+Verified
+
+add_broken_4:::1
+False
+
+add_broken_4:::2
+Verified
+
+inc
+Verified
+
diff --git a/tests/resources/golden/assert_func_chain.cairo b/tests/resources/golden/assert_func_chain.cairo
new file mode 100644
index 00000000..c0db0558
--- /dev/null
+++ b/tests/resources/golden/assert_func_chain.cairo
@@ -0,0 +1,15 @@
+// @post [ap - 1] == 7
+func main() {
+    [ap] = 5, ap++;
+    call succ;
+    // @assert [ap - 1] == 6
+    call succ;
+    ret;
+}
+
+// @post $Return.res == [fp - 3] + 1
+func succ(x) -> (res: felt) {
+    [ap] = [fp - 3], ap++;
+    [ap] = [ap - 1] + 1, ap++;
+    ret;
+}
diff --git a/tests/resources/golden/assert_func_chain.gold b/tests/resources/golden/assert_func_chain.gold
new file mode 100644
index 00000000..ec9d2ddf
--- /dev/null
+++ b/tests/resources/golden/assert_func_chain.gold
@@ -0,0 +1,6 @@
+main
+Verified
+
+succ
+Verified
+
diff --git a/tests/resources/golden/assert_func_peano_prod.cairo b/tests/resources/golden/assert_func_peano_prod.cairo
new file mode 100644
index 00000000..5e068a69
--- /dev/null
+++ b/tests/resources/golden/assert_func_peano_prod.cairo
@@ -0,0 +1,14 @@
+// @post $Return.res == x * y
+func prod(x, y) -> (res: felt) {
+    [ap] = [fp - 4], ap++;
+    [ap] = [fp - 3], ap++;
+    [ap] = 0, ap++;
+
+    // @invariant [ap - 1] + [fp - 4] * [ap - 2] == [fp - 4] * [fp - 3]
+    loop:
+    [ap] = [ap - 2] - 1, ap++;
+    // @assert [ap - 2] + [fp - 4] * ([ap - 1] + 1) == [fp - 4] * [fp - 3]
+    [ap] = [ap - 2] + [fp - 4], ap++;
+    jmp loop if [ap - 2] != 0;
+    ret;
+}
diff --git a/tests/resources/golden/assert_func_peano_prod.gold b/tests/resources/golden/assert_func_peano_prod.gold
new file mode 100644
index 00000000..94654404
--- /dev/null
+++ b/tests/resources/golden/assert_func_peano_prod.gold
@@ -0,0 +1,2 @@
+prod
+Verified
diff --git a/tests/resources/golden/assert_inline_many.cairo b/tests/resources/golden/assert_inline_many.cairo
new file mode 100644
index 00000000..05dcd6fb
--- /dev/null
+++ b/tests/resources/golden/assert_inline_many.cairo
@@ -0,0 +1,38 @@
+func succ(x) {
+    [ap] = [fp - 3] + 1, ap++;
+    ret;
+}
+
+func pred(x) {
+    [ap] = [fp - 3] - 1, ap++;
+    ret;
+}
+
+func id(x) {
+    [ap] = [fp - 3], ap++;
+    call succ;
+    call pred;
+    ret;
+}
+
+func addtwo(x) {
+    [ap] = [fp - 3], ap++;
+    call succ;
+    call succ;
+    ret;
+}
+
+// @post [ap - 1] == 45
+func main() {
+    [ap] = 41, ap++;
+    call id;
+    // @assert [ap - 1] == 41
+    [ap] = [ap - 1] + 1, ap++;
+    call id;
+    // @assert [ap - 1] == 42
+    call succ;
+    // @assert [ap - 1] == 43
+    call addtwo;
+    // @assert [ap - 1] == 45
+    ret;
+}
diff --git a/tests/resources/golden/assert_inline_many.gold b/tests/resources/golden/assert_inline_many.gold
new file mode 100644
index 00000000..13d688a1
--- /dev/null
+++ b/tests/resources/golden/assert_inline_many.gold
@@ -0,0 +1,15 @@
+main
+Verified
+
+succ [inlined]
+Verified
+
+pred [inlined]
+Verified
+
+id [inlined]
+Verified
+
+addtwo [inlined]
+Verified
+
diff --git a/tests/resources/golden/assert_inline_pre_success.cairo b/tests/resources/golden/assert_inline_pre_success.cairo
new file mode 100644
index 00000000..fb63817a
--- /dev/null
+++ b/tests/resources/golden/assert_inline_pre_success.cairo
@@ -0,0 +1,33 @@
+func succ() {
+    [ap] = [fp - 3] + 1, ap++;
+    ret;
+}
+
+// @pre x > 255
+// @post [ap - 1] == [fp - 3] - 1
+func pred(x) -> (res: felt) {
+    [ap] = x - 1, ap++;
+    ret;
+}
+
+// @post [ap - 1] == 999
+func comp_id() {
+    [ap] = 1000, ap++;
+    call succ;
+    // @assert [ap - 1] == 1001
+    call pred;
+    // @assert [ap - 1] == 1000
+    call pred;
+    ret;
+}
+
+// @post [ap - 1] == 999
+func comp_id_broken() {
+    [ap] = 1000, ap++;
+    call succ;
+    // @assert [ap - 1] == 42
+    call pred;
+    // @assert [ap - 1] == 1000
+    call pred;
+    ret;
+}
diff --git a/tests/resources/golden/assert_inline_pre_success.gold b/tests/resources/golden/assert_inline_pre_success.gold
new file mode 100644
index 00000000..491a8e45
--- /dev/null
+++ b/tests/resources/golden/assert_inline_pre_success.gold
@@ -0,0 +1,24 @@
+comp_id
+Verified
+
+comp_id_broken:::default
+False
+
+comp_id_broken.!anonymous_assert_label_2 Pre<pred|<19=pred/root>> 
+False
+
+comp_id_broken.!anonymous_assert_label_2
+Verified
+
+comp_id_broken.!anonymous_assert_label_3 Pre<pred|<21=pred/root>>
+Verified
+
+comp_id_broken.!anonymous_assert_label_3
+Verified
+
+pred
+Verified
+
+succ [inlined]
+Verified
+
diff --git a/tests/resources/golden/assert_let.cairo b/tests/resources/golden/assert_let.cairo
new file mode 100644
index 00000000..522dfe36
--- /dev/null
+++ b/tests/resources/golden/assert_let.cairo
@@ -0,0 +1,41 @@
+%lang starknet
+
+func bar{syscall_ptr: felt*}() -> (res: felt) {
+    let s = 5;
+    // @assert s == 5
+    return (res=s);
+}
+
+func bar_broken{syscall_ptr: felt*}() -> (res: felt) {
+    let s = 5;
+    // @assert s == 6
+    return (res=s);
+}
+
+func baz{syscall_ptr: felt*}() -> (res: felt) {
+    let s = 5;
+    [ap] = 1, ap++;
+    // @assert s == 5
+    return (res=s);
+}
+
+func baz_broken{syscall_ptr: felt*}() -> (res: felt) {
+    let s = 5;
+    [ap] = 1, ap++;
+    // @assert s == 6
+    return (res=s);
+}
+
+func foo{syscall_ptr: felt*}() -> (res: felt) {
+    let s = 5;
+    // @assert s == 5
+    [ap] = 1, ap++;
+    return (res=s);
+}
+
+func foo_broken{syscall_ptr: felt*}() -> (res: felt) {
+    let s = 5;
+    // @assert s == 6
+    [ap] = 1, ap++;
+    return (res=s);
+}
diff --git a/tests/resources/golden/assert_let.gold b/tests/resources/golden/assert_let.gold
new file mode 100644
index 00000000..a1957e1d
--- /dev/null
+++ b/tests/resources/golden/assert_let.gold
@@ -0,0 +1,26 @@
+bar
+Verified
+
+empty: (= 5 6)
+False
+
+bar_broken
+Contradictory premises
+
+baz
+Verified
+
+baz_broken:::default
+False
+
+baz_broken.!anonymous_assert_label_3
+Contradictory premises
+
+foo
+Verified
+
+empty: (= 5 6)
+False
+
+foo_broken
+Contradictory premises
diff --git a/tests/resources/golden/assert_let_minimal.cairo b/tests/resources/golden/assert_let_minimal.cairo
new file mode 100644
index 00000000..42f86550
--- /dev/null
+++ b/tests/resources/golden/assert_let_minimal.cairo
@@ -0,0 +1,7 @@
+%lang starknet
+
+func bar{syscall_ptr: felt*}() -> (res: felt) {
+    let s = 5;
+    // @assert s == 5
+    return (res=s);
+}
diff --git a/tests/resources/golden/assert_let_minimal.gold b/tests/resources/golden/assert_let_minimal.gold
new file mode 100644
index 00000000..e744dbe6
--- /dev/null
+++ b/tests/resources/golden/assert_let_minimal.gold
@@ -0,0 +1,2 @@
+bar
+Verified
diff --git a/tests/resources/golden/assert_lvar_basic.cairo b/tests/resources/golden/assert_lvar_basic.cairo
new file mode 100644
index 00000000..f71abd3a
--- /dev/null
+++ b/tests/resources/golden/assert_lvar_basic.cairo
@@ -0,0 +1,19 @@
+// @declare $x : felt
+// @pre x == $x
+// @post $Return.res == $x + 1
+func inc(x: felt) -> (res: felt) {
+    alloc_locals;
+    local x = x + 1;
+    // @assert x == $x + 1
+    return (res=x);
+}
+
+// @declare $x : felt
+// @pre x == $x
+// @post $Return.res == $x + 1
+func inc_broken(x: felt) -> (res: felt) {
+    alloc_locals;
+    local x = x + 1;
+    // @assert x == $x
+    return (res=x);
+}
diff --git a/tests/resources/golden/assert_lvar_basic.gold b/tests/resources/golden/assert_lvar_basic.gold
new file mode 100644
index 00000000..4119a022
--- /dev/null
+++ b/tests/resources/golden/assert_lvar_basic.gold
@@ -0,0 +1,9 @@
+inc
+Verified
+
+inc_broken:::default
+False
+
+inc_broken.!anonymous_assert_label_1
+False
+
diff --git a/tests/resources/golden/assert_lvar_struct.cairo b/tests/resources/golden/assert_lvar_struct.cairo
new file mode 100644
index 00000000..2e235d81
--- /dev/null
+++ b/tests/resources/golden/assert_lvar_struct.cairo
@@ -0,0 +1,22 @@
+struct MyStruct {
+    x: felt,
+    y: felt,
+}
+
+// @declare $s : MyStruct
+// @pre s == $s
+// @post $Return.res == $s.x + $s.y
+func elem_sum(s: MyStruct) -> (res: felt) {
+    let res = s.x + s.y;
+    // @assert res == $s.x + $s.y
+    return (res=res);
+}
+
+// @declare $s : MyStruct
+// @pre s == $s
+// @post $Return.res == $s.x + $s.y + 1
+func elem_sum_broken(s: MyStruct) -> (res: felt) {
+    let res = s.x + s.y;
+    // @assert res == $s.x + $s.y + 1
+    return (res=s.x + s.y);
+}
diff --git a/tests/resources/golden/assert_lvar_struct.gold b/tests/resources/golden/assert_lvar_struct.gold
new file mode 100644
index 00000000..b24c7f3a
--- /dev/null
+++ b/tests/resources/golden/assert_lvar_struct.gold
@@ -0,0 +1,8 @@
+elem_sum
+Verified
+
+empty: (= (+ (memory (+ fp (- 4))) (memory (+ fp (- 3)))) (+ (+ $s.x $s.y) 1))
+False
+
+elem_sum_broken
+Verified
diff --git a/tests/resources/golden/assert_simple.cairo b/tests/resources/golden/assert_simple.cairo
new file mode 100644
index 00000000..d716face
--- /dev/null
+++ b/tests/resources/golden/assert_simple.cairo
@@ -0,0 +1,31 @@
+%lang starknet
+
+// @post $Return.res == 5
+func bar{syscall_ptr: felt*}() -> (res: felt) {
+    [ap] = 2, ap++;
+    // @assert [ap - 1] == 2
+    [ap] = 5, ap++;
+    ret;
+}
+
+// @post $Return.res == 5
+func bar_broken{syscall_ptr: felt*}() -> (res: felt) {
+    [ap] = 2, ap++;
+    // @assert [ap - 1] == 3
+    [ap] = 5, ap++;
+    ret;
+}
+
+// @post $Return.res == 2
+func foo{syscall_ptr: felt*}() -> (res: felt) {
+    [ap] = 2, ap++;
+    // @assert [ap - 1] == 2
+    ret;
+}
+
+// @post $Return.res == 2
+func foo_broken{syscall_ptr: felt*}() -> (res: felt) {
+    [ap] = 2, ap++;
+    // @assert [ap - 1] == 3
+    ret;
+}
diff --git a/tests/resources/golden/assert_simple.gold b/tests/resources/golden/assert_simple.gold
new file mode 100644
index 00000000..4e431770
--- /dev/null
+++ b/tests/resources/golden/assert_simple.gold
@@ -0,0 +1,14 @@
+bar
+Verified
+
+bar_broken:::default
+False
+
+bar_broken.!anonymous_assert_label_1
+Verified
+
+foo
+Verified
+
+foo_broken
+False
diff --git a/tests/resources/golden/assert_stack_minimal.cairo b/tests/resources/golden/assert_stack_minimal.cairo
new file mode 100644
index 00000000..1545a90e
--- /dev/null
+++ b/tests/resources/golden/assert_stack_minimal.cairo
@@ -0,0 +1,44 @@
+%lang starknet
+
+struct Stack {
+    value: felt,
+    next: Stack*,
+}
+
+namespace _Stack {
+    func empty() -> (stack: Stack*) {
+        return (cast(0, Stack*),);
+    }
+
+    // @post $Return.stack.value == stack.value + stack.next.value
+    // @post $Return.stack.next == stack.next.next
+    func add(stack: Stack*) -> (stack: Stack*) {
+        let x = stack.value;
+        let y = stack.next.value;
+        return (new Stack(value=x + y, next=stack.next.next),);
+    }
+
+    // @post $Return.stack.value == i
+    // @post $Return.stack.next == stack
+    func lit(stack: Stack*, i: felt) -> (stack: Stack*) {
+        return (new Stack(value=i, next=stack),);
+    }
+
+    // @post $Return.res == stack.value
+    func top(stack: Stack*) -> (res: felt) {
+        return (stack.value,);
+    }
+}
+
+// @post [ap - 1] == 11
+func main_() -> (res: felt) {
+    let (stack1) = _Stack.empty();
+    let (stack2) = _Stack.lit(stack1, 5);
+    // @assert stack2.value == 5 and stack2.next == stack1
+    let (stack3) = _Stack.lit(stack2, 6);
+    // @assert stack3.value == 6 and stack3.next == stack2 and stack2.value == 5
+    let (stack4) = _Stack.add(stack3);
+    // @assert stack4.value == 11
+    let (top) = _Stack.top(stack4);
+    return (top,);
+}
diff --git a/tests/resources/golden/assert_stack_minimal.gold b/tests/resources/golden/assert_stack_minimal.gold
new file mode 100644
index 00000000..c3b435cd
--- /dev/null
+++ b/tests/resources/golden/assert_stack_minimal.gold
@@ -0,0 +1,15 @@
+_Stack.add
+Verified
+
+_Stack.lit
+Verified
+
+_Stack.top
+Verified
+
+main_
+Verified
+
+_Stack.empty [inlined]
+Verified
+
diff --git a/tests/resources/golden/oneoff.sh b/tests/resources/golden/oneoff.sh
index 97141f40..b62b6ff6 100755
--- a/tests/resources/golden/oneoff.sh
+++ b/tests/resources/golden/oneoff.sh
@@ -8,7 +8,7 @@ temp_file="${base}.temp"
 spec_file="${base}_spec.json"
 
 horus-compile "$test_file" --output "$compiled_file" --spec_output "$spec_file"
-stack run horus-check "$compiled_file" "$spec_file" -- -s cvc5 -s z3 -t 100000 &> "$temp_file" || true
+stack run horus-check "$compiled_file" "$spec_file" -- -s cvc5 -s mathsat -s z3 -t 100000 &> "$temp_file" || true
 ansii="\x1B\[[0-9;]\{1,\}[A-Za-z]"
 sed -i "/^hint:/d" $temp_file
 sed -i "/^$ansii[h]int:/d" $temp_file