implement comment injections

.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 [email protected]: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.

horus-check.cabal

@@ -85,6 +85,7 @@ library
       Horus.Preprocessor
       Horus.Preprocessor.Runner
       Horus.Preprocessor.Solvers
+      Horus.SMTHygiene
       Horus.SW.Builtin
       Horus.SW.CairoType
       Horus.SW.CairoType.JSON

src/Horus/CFGBuild.hs

@@ -13,6 +13,7 @@ module Horus.CFGBuild
   , mkInv
   , Vertex (..)
   , getVerts
+  , isOptimising
   , isPreCheckingVertex
   )
 where
@@ -81,6 +82,9 @@ data Vertex = Vertex
   }
   deriving (Show)
 
+isOptimising :: Vertex -> Bool
+isOptimising = isJust . v_preCheckedF
+
 instance Eq Vertex where
   (==) lhs rhs = v_name lhs == v_name rhs
 
@@ -273,7 +277,7 @@ addArcsFrom inlinables prog rows seg@(Segment s) vFrom
     -- in which Pre(G) is assumed to hold at the PC of the G call site, as it will have
     -- been checked by the module induced by the ghost vertex.
     ghostV <- addOptimisingVertex (nextSegmentLabel seg) callee
-    pre <- maybe (mkPre Expr.True) mkPre . fs'_pre <$> getFuncSpec callee
+    pre <- maybe (mkPre Expr.True) (mkPre . fst) . fs'_pre <$> getFuncSpec callee
 
     -- Important note on the way we deal with logical variables. These are @declare-d and
     -- their values can be bound in preconditions. They generate existentials which only occur
@@ -333,7 +337,7 @@ addAssertions inlinables identifiers = do
               (Nothing, Nothing) ->
                 when (fu_pc f `Set.notMember` Set.map sf_pc inlinables) $
                   for_ retVs (`addAssertion` mkPost Expr.True)
-              _ -> for_ retVs (`addAssertion` maybe (mkPost Expr.True) mkPost post)
+              _ -> for_ retVs (`addAssertion` maybe (mkPost Expr.True) (mkPost . fst) post)
     ILabel pc ->
       whenJustM (getInvariant idName) $ \inv ->
         getSalientVertex pc >>= (`addAssertion` mkInv inv)