Enforce strict gas ordering

src/EVM/SMT.hs

@@ -220,7 +220,6 @@ assertPropsNoSimp psPreConc = do
   <> smt2Line ""
   <> (declareAddrs addresses)
   <> smt2Line ""
-  -- <> declareGasVars psPreConc
   <> (declareBufs toDeclarePsElim bufs stores)
   <> smt2Line ""
   <> (declareVars . nubOrd $ foldl (<>) [] allVars)
@@ -233,6 +232,7 @@ assertPropsNoSimp psPreConc = do
   <> smt2Line ""
   <> keccakAssertions'
   <> readAssumes'
+  <> gasOrder
   <> smt2Line ""
   <> SMT2 (fmap (\p -> "(assert " <> p <> ")") encs) mempty mempty
   <> SMT2 smt mempty mempty
@@ -257,6 +257,7 @@ assertPropsNoSimp psPreConc = do
     allVars = fmap referencedVars toDeclarePsElim <> fmap referencedVars bufVals <> fmap referencedVars storeVals <> [abstrVars abst]
     frameCtx = fmap referencedFrameContext toDeclarePsElim <> fmap referencedFrameContext bufVals <> fmap referencedFrameContext storeVals
     blockCtx = fmap referencedBlockContext toDeclarePsElim <> fmap referencedBlockContext bufVals <> fmap referencedBlockContext storeVals
+    gasOrder = enforceGasOrder psPreConc
 
     abstrVars :: AbstState -> [Builder]
     abstrVars (AbstState b _) = map ((\v->fromString ("abst_" ++ show v)) . snd) (Map.toList b)
@@ -439,15 +440,22 @@ declareAddrs names = SMT2 (["; symbolic addresseses"] <> fmap declare names) cex
     declare n = "(declare-fun " <> n <> " () Addr)"
     cexvars = (mempty :: CexVars){ addrs = fmap toLazyText names }
 
--- declareGasVars :: [Prop] -> SMT2
--- declareGasVars ps = SMT2 (["; gas variables"] <> fmap declare names) mempty mempty
---   where
---     declare n = "(declare-fun gas_" <> n <> " () (_ BitVec 256))"
---     names :: [Builder] = nubOrd $ concatMap (foldProp go mempty) ps
---     go :: Expr a -> [Builder]
---     go e = case e of
---       Gas freshVar -> [fromLazyText $ T.pack $ show freshVar]
---       _ -> []
+enforceGasOrder :: [Prop] -> SMT2
+enforceGasOrder ps = SMT2 (["; gas ordering"] <> order names) mempty mempty
+  where
+    order :: [Int] -> [Builder]
+    order n = consecutivePairs n >>= \case
+      -- The GAS instruction itself costs gas, so it's strictly decreasing
+      (x, y) -> ["(assert (< gas_" <> (fromString . show $ x) <> " gas_" <> (fromString . show $ y) <> "))"]
+    consecutivePairs :: [Int] -> [(Int, Int)]
+    consecutivePairs [] = []
+    consecutivePairs [_] = []
+    consecutivePairs (x:y:xs) = (x, y) : consecutivePairs (y:xs)
+    names :: [Int] = nubOrd $ concatMap (foldProp go mempty) ps
+    go :: Expr a -> [Int]
+    go e = case e of
+      Gas freshVar -> [freshVar]
+      _ -> []
 
 declareFrameContext :: [(Builder, [Prop])] -> Err SMT2
 declareFrameContext names = do