Merge pull request #200 from lefterislazar/static_arrays

Support for static arrays in contract storage and constructor/behavior arguments

Author: lefterislazar

.github/workflows/build.yml

@@ -17,16 +17,18 @@ jobs:
       fail-fast: false
     runs-on: ${{ matrix.os }}
     steps:
-      - uses: actions/checkout@v2
-      - uses: cachix/install-nix-action@v22
+      - uses: actions/checkout@v4
+      - uses: cachix/install-nix-action@v31
         with:
-          skip_adding_nixpkgs_channel: false
-      - uses: cachix/cachix-action@v12
+          extra_nix_config: |
+            experimental-features = nix-command flakes
+            accept-flake-config = true
+      - uses: cachix/cachix-action@v16
         with:
           name: dapp
           skipPush: true
           signingKey: ''
       - name: test
-        run: nix develop --ignore-environment --command bash -c "cabal update && make test-ci"
+        run: nix develop --ignore-environment --accept-flake-config --command bash -lc "cabal update && make test-ci"
       - name: build
-        run: nix build -L .#act
+        run: nix build -L .#act --accept-flake-config

.gitignore

@@ -18,9 +18,9 @@ src/dist/
 *.vok
 *.vos
 *.glob
-**/CoqMakefile
-**/CoqMakefile.conf
-**/.CoqMakefile.d
+**/RocqMakefile
+**/RocqMakefile.conf
+**/.RocqMakefile.d
 **/.lia.cache
 *.aux
 **/.coqdeps.d
@@ -32,4 +32,4 @@ doc/book
 .direnv/
 
 *~
-*#
+*#

Makefile

@@ -53,7 +53,7 @@ hevm_slow=tests/hevm/pass/amm/amm.act tests/hevm/pass/amm-2/amm-2.act
 hevm_fast=$(filter-out $(hevm_slow), $(hevm_pass))
 
 # supposed to pass
-failing_typing=tests/frontend/pass/array/array.act tests/frontend/pass/dss/vat.act tests/frontend/pass/creation/createMultiple.act tests/frontend/pass/staticstore/staticstore.act
+failing_typing=tests/frontend/pass/dss/vat.act tests/frontend/pass/creation/createMultiple.act tests/frontend/pass/staticstore/staticstore.act
 
 
 coq-examples = tests/coq/transitions tests/coq/safemath tests/coq/exponent tests/coq/token tests/coq/ERC20-simple tests/coq/ERC20 tests/coq/multi

src/Act/Bounds.hs

@@ -4,7 +4,8 @@
 module Act.Bounds (addBounds) where
 
 import Data.Maybe
-import Data.List (nub)
+import Data.List (nub, partition)
+import Data.Type.Equality
 
 import Act.Syntax
 import Act.Syntax.TypedExplicit
@@ -37,10 +38,18 @@ addBoundsConstructor ctor@(Constructor _ (Interface _ decls) _ pre post invs sta
       pre' = pre
              <> mkCallDataBounds decls
              <> mkEthEnvBounds (ethEnvFromConstructor ctor)
-             <> mkStorageBoundsLoc (nub $ concatMap locsFromExp pre <> concatMap locsFromUpdateRHS stateUpdates)
+              -- The following is sound as values of locations outside local storage
+              -- already exist as the constructor starts executing,
+              -- and the constructor cannot modify non-local locations.
+             <> mkLocationBounds nonlocalLocs
       invs' = addBoundsInvariant ctor <$> invs
       post' = post <> mkStorageBounds stateUpdates Post
 
+      locs = concatMap locsFromExp (pre <> post)
+             <> concatMap locsFromInvariant invs
+             <> concatMap locsFromUpdate stateUpdates
+      nonlocalLocs = filter (not . isLocalLoc) locs
+
 -- | Adds type bounds for calldata, environment vars, and storage vars as preconditions
 addBoundsBehaviour :: Behaviour -> Behaviour
 addBoundsBehaviour behv@(Behaviour _ _ (Interface _ decls) _ pre cases post stateUpdates _) =
@@ -49,11 +58,14 @@ addBoundsBehaviour behv@(Behaviour _ _ (Interface _ decls) _ pre cases post stat
       pre' = pre
              <> mkCallDataBounds decls
              <> mkStorageBounds stateUpdates Pre
-             <> mkStorageBoundsLoc (nub $ concatMap locsFromExp (pre <> cases) <> concatMap locsFromUpdateRHS stateUpdates)
+             <> mkLocationBounds locs
              <> mkEthEnvBounds (ethEnvFromBehaviour behv)
       post' = post
               <> mkStorageBounds stateUpdates Post
 
+      locs = concatMap locsFromExp (pre <> post <> cases)
+             <> concatMap locsFromUpdate stateUpdates
+
 -- | Adds type bounds for calldata, environment vars, and storage vars
 addBoundsInvariant :: Constructor -> Invariant -> Invariant
 addBoundsInvariant (Constructor _ (Interface _ decls) _ _ _ _ _) inv@(Invariant _ preconds storagebounds (PredTimed predicate _)) =
@@ -62,8 +74,13 @@ addBoundsInvariant (Constructor _ (Interface _ decls) _ _ _ _ _) inv@(Invariant
       preconds' = preconds
                   <> mkCallDataBounds decls
                   <> mkEthEnvBounds (ethEnvFromExp predicate)
+                  <> mkLocationBounds nonlocalLocs
       storagebounds' = storagebounds
-                       <> mkStorageBoundsLoc (locsFromExp predicate)
+                       <> mkLocationBounds localLocs
+
+      locs = concatMap locsFromExp (preconds <> storagebounds)
+             <> locsFromExp predicate
+      (nonlocalLocs, localLocs) = partition (not . isLocalLoc) locs
 
 mkEthEnvBounds :: [EthEnv] -> [Exp ABoolean]
 mkEthEnvBounds vars = catMaybes $ mkBound <$> nub vars
@@ -94,21 +111,36 @@ mkStorageBounds :: [StorageUpdate] -> When -> [Exp ABoolean]
 mkStorageBounds refs t = concatMap mkBound refs
   where
     mkBound :: StorageUpdate -> [Exp ABoolean]
-    mkBound (Update SInteger item _) = [mkItemBounds t item]
+    mkBound (Update SInteger item _) = [mkSItemBounds t item]
+    mkBound (Update typ item@(Item _ (PrimitiveType at) _) _) | isNothing $ flattenArrayAbiType at =
+      maybe [] (\Refl -> mkSItemBounds t <$> expandItem item) $ testEquality (flattenSType typ) SInteger
     mkBound _ = []
 
-mkItemBounds :: When -> TItem AInteger Storage -> Exp ABoolean
-mkItemBounds whn item@(Item _ (PrimitiveType vt) _) = bound vt (VarRef nowhere whn SStorage item)
-mkItemBounds _ (Item _ (ContractType _) _) = LitBool nowhere True
+mkSItemBounds :: When -> TItem AInteger Storage -> Exp ABoolean
+mkSItemBounds whn item@(Item _ (PrimitiveType vt) _) = bound vt (VarRef nowhere whn SStorage item)
+mkSItemBounds _ (Item _ (ContractType _) _) = LitBool nowhere True
 
-mkStorageBoundsLoc :: [StorageLocation] -> [Exp ABoolean]
-mkStorageBoundsLoc refs = concatMap mkBound refs
+mkCItemBounds :: TItem AInteger Calldata -> Exp ABoolean
+mkCItemBounds item@(Item _ (PrimitiveType vt) _) = bound vt (VarRef nowhere Pre SCalldata item)
+mkCItemBounds (Item _ (ContractType _) _) = LitBool nowhere True
+
+mkLocationBounds :: [Location] -> [Exp ABoolean]
+mkLocationBounds refs = concatMap mkBound refs
   where
-    mkBound :: StorageLocation -> [Exp ABoolean]
-    mkBound (Loc SInteger item) = [mkItemBounds Pre item]
+    mkBound :: Location -> [Exp ABoolean]
+    mkBound (Loc SInteger rk item) = [mkItemBounds rk item]
+    mkBound (Loc typ rk item@(Item _ (PrimitiveType at) _)) | isNothing $ flattenArrayAbiType at =
+      maybe [] (\Refl -> mkItemBounds rk <$> expandItem item) $ testEquality (flattenSType typ) SInteger
     mkBound _ = []
 
+    mkItemBounds :: SRefKind k -> TItem AInteger k -> Exp ABoolean
+    mkItemBounds SStorage = mkSItemBounds Pre
+    mkItemBounds SCalldata = mkCItemBounds
+
 mkCallDataBounds :: [Decl] -> [Exp ABoolean]
-mkCallDataBounds = concatMap $ \(Decl typ name) -> case fromAbiType typ of
-  AInteger -> [bound typ (_Var typ name)]
-  _ -> []
+mkCallDataBounds = concatMap $ \(Decl typ name) -> case typ of
+  -- Array element bounds are applied lazily when needed in mkCalldataLocationBounds
+  (AbiArrayType _ _) -> []
+  _ -> case fromAbiType typ of
+        AInteger -> [bound typ (_Var typ name)]
+        _ -> []

src/Act/CLI.hs

@@ -145,7 +145,9 @@ type' :: FilePath -> Solvers.Solver -> Maybe Integer -> Bool -> IO ()
 type' f solver' smttimeout' debug' = do
   contents <- readFile f
   proceed contents (addBounds <$> compile contents) $ \claims -> do
+    checkArrayBounds claims solver' smttimeout' debug'
     checkCases claims solver' smttimeout' debug'
+    checkRewriteAliasing claims solver' smttimeout' debug'
     B.putStrLn $ encode claims
 
 parseSolver :: Maybe Text -> IO Solvers.Solver
@@ -161,7 +163,9 @@ prove file' solver' smttimeout' debug' = do
   let config = SMT.SMTConfig solver' (fromMaybe 20000 smttimeout') debug'
   contents <- readFile file'
   proceed contents (addBounds <$> compile contents) $ \claims -> do
+    checkArrayBounds claims solver' smttimeout' debug'
     checkCases claims solver' smttimeout' debug'
+    checkRewriteAliasing claims solver' smttimeout' debug'
     let
       catModels results = [m | Sat m <- results]
       catErrors results = [e | e@SMT.Error {} <- results]
@@ -215,7 +219,9 @@ coq' :: FilePath -> Solvers.Solver -> Maybe Integer -> Bool -> IO ()
 coq' f solver' smttimeout' debug' = do
   contents <- readFile f
   proceed contents (addBounds <$> compile contents) $ \claims -> do
+    checkArrayBounds claims solver' smttimeout' debug'
     checkCases claims solver' smttimeout' debug'
+    checkRewriteAliasing claims solver' smttimeout' debug'
     TIO.putStr $ coq claims
 
 decompile' :: FilePath -> Text -> Solvers.Solver -> Maybe Integer -> Bool -> IO ()