Add missing range check bound to `assert_nn_le()` spec #195

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open

Julek wants to merge 12 commits into master from julek/assert_nn_le_spec_fix

.github/workflows/main.yml

-Original file line number
+Diff line change
@@ Expand Up / @@ -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:
@@ Expand Down @@

README.md

-Original file line number
+Diff line change
@@ Expand Up / @@ -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
@@ Expand Down Expand Up @@
       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.
@@ Expand Down @@

src/Horus/FunctionAnalysis.hs

            
                      Original file line number
                      Diff line number
                      Diff line change
                  
    @@ -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]

src/Horus/Global.hs

            
                      Original file line number
                      Diff line number
                      Diff line change
                  
    @@ -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,21 +332,27 @@ 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.

    -}

    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

      -- For every inlinable function `f`, build the CFG for all functions excluding `f`.

      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 +368,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

src/Horus/SW/Std.hs

-Original file line number
+Diff line change
@@ Expand Up / @@ -68,7 +68,7 @@ stdSpecsList = @@
       ,
         ( "starkware.cairo.common.math.assert_nn_le"
         , emptyFuncSpec
-            { fs_post = 0 .<= memory (fp - 4) .&& memory (fp - 4) .<= memory (fp - 3)
+            { fs_post = 0 .<= memory (fp - 4) .&& memory (fp - 4) .<= memory (fp - 3) .&& memory (fp - 3) .<= rcBound
             }
         )
       ,
@@ Expand Down @@

tests/resources/bats-template

-Original file line number
+Diff line change
@@ Expand Up / @@ -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"
@@ Expand Down @@

tests/resources/golden/extern_remove_dirty.cairo

-Original file line number
+Diff line change
@@ -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);
+    }

tests/resources/golden/extern_remove_dirty.gold

Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		f [inlined]
		Verified

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add missing range check bound to `assert_nn_le()` spec #195

Uh oh!

Diff view

Diff view

There are no files selected for viewing

Add missing range check bound to assert_nn_le() spec #195

Are you sure you want to change the base?

Uh oh!

Add missing range check bound to assert_nn_le() spec #195

Uh oh!

Uh oh!

Diff view

Diff view

There are no files selected for viewing

Add missing range check bound to `assert_nn_le()` spec #195

Add missing range check bound to `assert_nn_le()` spec #195