diff --git a/cli/cli.hs b/cli/cli.hs index 34863e775..856c54915 100644 --- a/cli/cli.hs +++ b/cli/cli.hs @@ -103,6 +103,7 @@ data CommonOptions = CommonOptions , earlyAbort ::Bool , mergeMaxBudget :: Int , maxDynSize ::Int + , abstractArith ::Bool } commonOptions :: Parser CommonOptions @@ -135,6 +136,7 @@ commonOptions = CommonOptions <*> (switch $ long "early-abort" <> help "Stop exploration immediately upon finding the first counterexample") <*> (option auto $ long "merge-max-budget" <> showDefault <> value 100 <> help "Max instructions for speculative merge exploration during path merging") <*> (option auto $ long "max-dyn-size" <> showDefault <> value 64 <> help "Max byte length for concretized dynamic types (bytes, string) in symbolic arguments") + <*> (switch $ long "abstract-arith" <> help "Use uninterpreted functions for div/mod in SMT queries (Halmos-style two-phase solving)") data CommonExecOptions = CommonExecOptions { address ::Maybe Addr @@ -380,6 +382,7 @@ main = do , earlyAbort = cOpts.earlyAbort , mergeMaxBudget = cOpts.mergeMaxBudget , maxDynSize = cOpts.maxDynSize + , abstractArith = cOpts.abstractArith } } diff --git a/hevm.cabal b/hevm.cabal index f1c87f8e0..f34959399 100644 --- a/hevm.cabal +++ b/hevm.cabal @@ -98,6 +98,7 @@ library EVM.Dapp, EVM.Expr, EVM.SMT, + EVM.SMT.DivModEncoding, EVM.Solvers, EVM.Exec, EVM.Format, @@ -124,6 +125,8 @@ library EVM.CheatsTH, EVM.SMT.Types, EVM.SMT.SMTLIB, + EVM.SMT.AbstractBase, + EVM.SMT.AbstractLemmas, Paths_hevm autogen-modules: Paths_hevm @@ -272,7 +275,6 @@ common test-common ghc-options: -threaded "-with-rtsopts=-N -A32m" build-depends: test-utils, - vector, other-modules: EVM.Test.Utils EVM.Test.BlockchainTests @@ -307,6 +309,7 @@ test-suite test regex, tasty-quickcheck, text, + vector, -- these tests require network access so we split them into a separate test -- suite to make it easy to skip them when running nix-build @@ -319,6 +322,7 @@ test-suite rpc-tests rpc.hs build-depends: text, + vector, test-suite ethereum-tests import: test-common diff --git a/src/EVM/Effects.hs b/src/EVM/Effects.hs index ad6bec1d6..fb6131d1b 100644 --- a/src/EVM/Effects.hs +++ b/src/EVM/Effects.hs @@ -49,6 +49,7 @@ data Config = Config , earlyAbort :: Bool , mergeMaxBudget :: Int -- ^ Max instructions for speculative merge exploration , maxDynSize :: Int -- ^ Max byte length for concretized dynamic types (bytes, string) + , abstractArith :: Bool } deriving (Show, Eq) @@ -71,6 +72,7 @@ defaultConfig = Config , earlyAbort = False , mergeMaxBudget = 100 , maxDynSize = 64 + , abstractArith = False } -- Write to the console diff --git a/src/EVM/SMT.hs b/src/EVM/SMT.hs index 9de149d9c..9b3ec3eda 100644 --- a/src/EVM/SMT.hs +++ b/src/EVM/SMT.hs @@ -6,17 +6,19 @@ module EVM.SMT ( module EVM.SMT.Types, module EVM.SMT.SMTLIB, + module EVM.SMT.DivModEncoding, collapse, getVar, formatSMT2, declareIntermediates, assertProps, - exprToSMT, + assertPropsAbstract, + assertPropsHelperWith, + decompose, + exprToSMTWith, encodeConcreteStore, - zero, - one, - propToSMT, + propToSMTWith, parseVar, parseEAddr, parseBlockCtx, @@ -66,6 +68,7 @@ import EVM.Types import EVM.Effects import EVM.SMT.Types import EVM.SMT.SMTLIB +import EVM.SMT.DivModEncoding -- ** Encoding ** ---------------------------------------------------------------------------------- @@ -93,7 +96,10 @@ formatSMT2 (SMT2 (SMTScript entries) _ ps) = expr <> smt2 -- | Reads all intermediate variables from the builder state and produces SMT declaring them as constants declareIntermediates :: BufEnv -> StoreEnv -> Err [SMTEntry] -declareIntermediates bufs stores = do +declareIntermediates = declareIntermediatesWith ConcreteDivMod + +declareIntermediatesWith :: DivModEncoding -> BufEnv -> StoreEnv -> Err [SMTEntry] +declareIntermediatesWith enc bufs stores = do let encSs = Map.mapWithKey encodeStore stores encBs = Map.mapWithKey encodeBuf bufs snippets <- sequence $ Map.elems $ encSs <> encBs @@ -101,46 +107,56 @@ declareIntermediates bufs stores = do pure $ (SMTComment "intermediate buffers & stores") : decls where encodeBuf n expr = do - buf <- exprToSMT expr + buf <- exprToSMTWith enc expr bufLen <- encodeBufLen n expr pure [SMTCommand ("(define-fun buf" <> (Data.Text.Lazy.Builder.Int.decimal n) <> "() Buf " <> buf <> ")\n"), bufLen] encodeBufLen n expr = do - bufLen <- exprToSMT (bufLengthEnv bufs True expr) + bufLen <- exprToSMTWith enc (bufLengthEnv bufs True expr) pure $ SMTCommand ("(define-fun buf" <> (Data.Text.Lazy.Builder.Int.decimal n) <>"_length () (_ BitVec 256) " <> bufLen <> ")") encodeStore n expr = do - storage <- exprToSMT expr + storage <- exprToSMTWith enc expr pure [SMTCommand ("(define-fun store" <> (Data.Text.Lazy.Builder.Int.decimal n) <> " () Storage " <> storage <> ")")] +decompose :: Config -> [Prop] -> [Prop] +decompose conf props = if conf.decomposeStorage && safeExprs && safeProps + then fromMaybe props (mapM (mapPropM Expr.decomposeStorage) props) + else props + where + -- All in these lists must be a `Just ()` or we cannot decompose + safeExprs = all (isJust . mapPropM_ Expr.safeToDecompose) props + safeProps = all Expr.safeToDecomposeProp props + -- simplify to rewrite sload/sstore combos -- notice: it is VERY important not to concretize early, because Keccak assumptions -- need unconcretized Props assertProps :: Config -> [Prop] -> Err SMT2 assertProps conf ps = - if not conf.simp then assertPropsHelper False ps - else assertPropsHelper True (decompose ps) - where - decompose :: [Prop] -> [Prop] - decompose props = if conf.decomposeStorage && safeExprs && safeProps - then fromMaybe props (mapM (mapPropM Expr.decomposeStorage) props) - else props - where - -- All in these lists must be a `Just ()` or we cannot decompose - safeExprs = all (isJust . mapPropM_ Expr.safeToDecompose) props - safeProps = all Expr.safeToDecomposeProp props - + if not conf.simp then assertPropsHelperWith ConcreteDivMod False [] ps + else assertPropsHelperWith ConcreteDivMod True [] (decompose conf ps) + +-- | Assert props with abstract div/mod (uninterpreted functions + encoding constraints). +assertPropsAbstract :: Config -> [Prop] -> Err SMT2 +assertPropsAbstract conf ps = do + let mkBase s = assertPropsHelperWith AbstractDivMod s divModAbstractDecls + base <- if not conf.simp then mkBase False ps + else mkBase True (decompose conf ps) + shiftBounds <- divModEncoding (exprToSMTWith AbstractDivMod) ps + mulLemmas <- mulEncoding (exprToSMTWith AbstractDivMod) ps + pure $ base <> SMT2 (SMTScript (shiftBounds <> mulLemmas)) mempty mempty -- Note: we need a version that does NOT call simplify, -- because we make use of it to verify the correctness of our simplification -- passes through property-based testing. -assertPropsHelper :: Bool -> [Prop] -> Err SMT2 -assertPropsHelper simp psPreConc = do - encs <- mapM propToSMT psElim - intermediates <- declareIntermediates bufs stores +assertPropsHelperWith :: DivModEncoding -> Bool -> [SMTEntry] -> [Prop] -> Err SMT2 +assertPropsHelperWith divEnc simp extraDecls psPreConc = do + encs <- mapM (propToSMTWith divEnc) psElim + intermediates <- declareIntermediatesWith divEnc bufs stores readAssumes' <- readAssumes keccakAssertions' <- keccakAssertions frameCtxs <- (declareFrameContext . nubOrd $ foldl' (<>) [] frameCtx) blockCtxs <- (declareBlockContext . nubOrd $ foldl' (<>) [] blockCtx) pure $ prelude + <> SMT2 (SMTScript extraDecls) mempty mempty <> SMT2 (SMTScript (declareAbstractStores abstractStores)) mempty mempty <> declareConstrainAddrs addresses <> (declareBufs toDeclarePsElim bufs stores) @@ -163,9 +179,9 @@ assertPropsHelper simp psPreConc = do -- vars, frames, and block contexts in need of declaration allVars = fmap referencedVars toDeclarePsElim <> fmap referencedVars bufVals <> fmap referencedVars storeVals - frameCtx = fmap referencedFrameContext toDeclarePsElim <> fmap referencedFrameContext bufVals <> fmap referencedFrameContext storeVals + frameCtx = fmap (referencedFrameContext divEnc) toDeclarePsElim <> fmap (referencedFrameContext divEnc) bufVals <> fmap (referencedFrameContext divEnc) storeVals blockCtx = fmap referencedBlockContext toDeclarePsElim <> fmap referencedBlockContext bufVals <> fmap referencedBlockContext storeVals - gasOrder = enforceGasOrder psPreConc + gasOrder = enforceGasOrder divEnc psPreConc -- Buf, Storage, etc. declarations needed bufVals = Map.elems bufs @@ -181,13 +197,13 @@ assertPropsHelper simp psPreConc = do keccAssump = keccakAssumptions $ Set.toList allKeccaks keccComp = [(PEq (Lit l) (Keccak buf)) | (buf, l) <- Set.toList concreteKecc] keccakAssertions = do - assumps <- mapM assertSMT keccAssump - comps <- mapM assertSMT keccComp + assumps <- mapM (assertSMTWith divEnc) keccAssump + comps <- mapM (assertSMTWith divEnc) keccComp pure $ ((SMTComment "keccak assumptions") : assumps) <> ((SMTComment "keccak computations") : comps) -- assert that reads beyond size of buffer & storage is zero readAssumes = do - assumps <- mapM assertSMT $ assertReads psElim bufs stores + assumps <- mapM (assertSMTWith divEnc) $ assertReads psElim bufs stores pure (SMTComment "read assumptions" : assumps) cexInfo :: StorageReads -> CexVars @@ -224,8 +240,8 @@ referencedVars expr = nubOrd $ foldTerm go [] expr Var s -> [fromText s] _ -> [] -referencedFrameContext :: TraversableTerm a => a -> [(Builder, [Prop])] -referencedFrameContext expr = nubOrd $ foldTerm go [] expr +referencedFrameContext :: DivModEncoding -> TraversableTerm a => a -> [(Builder, [Prop])] +referencedFrameContext enc expr = nubOrd $ foldTerm go [] expr where go :: Expr a -> [(Builder, [Prop])] go = \case @@ -234,6 +250,8 @@ referencedFrameContext expr = nubOrd $ foldTerm go [] expr o@(Gas _ _) -> [(fromRight' $ exprToSMT o, [])] o@(CodeHash (LitAddr _)) -> [(fromRight' $ exprToSMT o, [])] _ -> [] + exprToSMT :: Expr x -> Err Builder + exprToSMT = exprToSMTWith enc referencedBlockContext :: TraversableTerm a => a -> [(Builder, [Prop])] referencedBlockContext expr = nubOrd $ foldTerm go [] expr @@ -357,14 +375,14 @@ declareConstrainAddrs names = SMT2 (SMTScript ([SMTComment "concrete and symboli -- The gas is a tuple of (prefix, index). Within each prefix, the gas is strictly decreasing as the -- index increases. This function gets a map of Prefix -> [Int], and for each prefix, -- enforces the order -enforceGasOrder :: [Prop] -> [SMTEntry] -enforceGasOrder ps = [SMTComment "gas ordering"] <> (concatMap (uncurry order) indices) +enforceGasOrder :: DivModEncoding -> [Prop] -> [SMTEntry] +enforceGasOrder enc ps = [SMTComment "gas ordering"] <> (concatMap (uncurry order) indices) where order :: TS.Text -> [Int] -> [SMTEntry] order prefix n = consecutivePairs (nubInt n) >>= \(x, y)-> -- The GAS instruction itself costs gas, so it's strictly decreasing - [SMTCommand $ "(assert (bvugt " <> fromRight' (exprToSMT (Gas prefix x)) <> " " <> - fromRight' ((exprToSMT (Gas prefix y))) <> "))"] + [SMTCommand $ "(assert (bvugt " <> fromRight' (exprToSMTWith enc (Gas prefix x)) <> " " <> + fromRight' ((exprToSMTWith enc (Gas prefix y))) <> "))"] consecutivePairs :: [Int] -> [(Int, Int)] consecutivePairs [] = [] consecutivePairs l@(_:t) = zip l t @@ -402,18 +420,18 @@ declareBlockContext names = do cexvars = (mempty :: CexVars){ blockContext = fmap (toLazyText . fst) names } assertSMT :: Prop -> Either String SMTEntry -assertSMT p = do - p' <- propToSMT p - pure $ SMTCommand ("(assert " <> p' <> ")") +assertSMT = assertSMTWith ConcreteDivMod -wordAsBV :: forall a. Integral a => a -> Builder -wordAsBV w = "(_ bv" <> Data.Text.Lazy.Builder.Int.decimal w <> " 256)" +assertSMTWith :: DivModEncoding -> Prop -> Either String SMTEntry +assertSMTWith enc p = do + p' <- propToSMTWith enc p + pure $ SMTCommand ("(assert " <> p' <> ")") byteAsBV :: Word8 -> Builder byteAsBV b = "(_ bv" <> Data.Text.Lazy.Builder.Int.decimal b <> " 8)" -exprToSMT :: Expr a -> Err Builder -exprToSMT = \case +exprToSMTWith :: DivModEncoding -> Expr a -> Err Builder +exprToSMTWith divEnc = \case Lit w -> pure $ wordAsBV w Var s -> pure $ fromText s GVar (BufVar n) -> pure $ fromString $ "buf" <> (show n) @@ -423,7 +441,7 @@ exprToSMT = \case eight nine ten eleven twelve thirteen fourteen fifteen sixteen seventeen eighteen nineteen twenty twentyone twentytwo twentythree twentyfour twentyfive twentysix twentyseven twentyeight twentynine thirty thirtyone - -> concatBytes [ + -> concatBytesWith divEnc [ z, o, two, three, four, five, six, seven , eight, nine, ten, eleven, twelve, thirteen, fourteen, fifteen , sixteen, seventeen, eighteen, nineteen, twenty, twentyone, twentytwo, twentythree @@ -431,7 +449,12 @@ exprToSMT = \case Add a b -> op2 "bvadd" a b Sub a b -> op2 "bvsub" a b - Mul a b -> op2 "bvmul" a b + Mul a b -> case (a, b) of + -- only genuinely symbolic products are abstracted; a concrete factor + -- (0/1/power-of-two/constant) is handled natively / by the simplifier + (Lit _, _) -> op2 "bvmul" a b + (_, Lit _) -> op2 "bvmul" a b + _ -> mulOp a b Exp a b -> case a of Lit 0 -> do benc <- exprToSMT b @@ -442,7 +465,7 @@ exprToSMT = \case pure $ "(bvshl " <> one `sp` benc <> ")" _ -> case b of -- b is limited below, otherwise SMT query will be huge, and eventually Haskell stack overflows - Lit b' | b' < 1000 -> expandExp a b' + Lit b' | b' < 1000 -> expandExpWith divEnc a b' _ -> Left $ "Cannot encode symbolic exponent into SMT. Offending symbolic value: " <> show b Min a b -> do aenc <- exprToSMT a @@ -490,10 +513,10 @@ exprToSMT = \case SAR a b -> op2 "bvashr" b a CLZ a -> op1 "clz256" a SEx a b -> op2 "signext" a b - Div a b -> op2CheckZero "bvudiv" a b - SDiv a b -> op2CheckZero "bvsdiv" a b - Mod a b -> op2CheckZero "bvurem" a b - SMod a b -> op2CheckZero "bvsrem" a b + Div a b -> divModOp "bvudiv" "abst_evm_bvudiv" a b + SDiv a b -> divModOp "bvsdiv" "abst_evm_bvsdiv" a b + Mod a b -> divModOp "bvurem" "abst_evm_bvurem" a b + SMod a b -> divModOp "bvsrem" "abst_evm_bvsrem" a b -- NOTE: this needs to do the MUL at a higher precision, then MOD, then downcast MulMod a b c -> do aExp <- exprToSMT a @@ -553,7 +576,7 @@ exprToSMT = \case ReadByte idx src -> op2 "select" src idx ConcreteBuf "" -> pure "((as const Buf) #b00000000)" - ConcreteBuf bs -> writeBytes bs mempty + ConcreteBuf bs -> writeBytesWith divEnc bs mempty AbstractBuf s -> pure $ fromText s ReadWord idx prev -> op2 "readWord" idx prev BufLength (AbstractBuf b) -> pure $ fromText b <> "_length" @@ -572,10 +595,10 @@ exprToSMT = \case CopySlice srcIdx dstIdx size src dst -> do srcSMT <- exprToSMT src dstSMT <- exprToSMT dst - copySlice srcIdx dstIdx size srcSMT dstSMT + copySliceWith divEnc srcIdx dstIdx size srcSMT dstSMT -- we need to do a bit of processing here. - ConcreteStore s -> encodeConcreteStore s + ConcreteStore s -> encodeConcreteStore divEnc s AbstractStore a idx -> pure $ storeName a idx SStore idx val prev -> do encIdx <- exprToSMT idx @@ -589,29 +612,35 @@ exprToSMT = \case a -> internalError $ "TODO: implement: " <> show a where + exprToSMT :: Expr x -> Err Builder + exprToSMT = exprToSMTWith divEnc + op1 :: Builder -> Expr x -> Err Builder op1 op a = do enc <- exprToSMT a pure $ "(" <> op `sp` enc <> ")" + op2 :: Builder -> Expr x -> Expr y -> Err Builder op2 op a b = do aenc <- exprToSMT a benc <- exprToSMT b pure $ "(" <> op `sp` aenc `sp` benc <> ")" + op2CheckZero :: Builder -> Expr x -> Expr y -> Err Builder op2CheckZero op a b = do aenc <- exprToSMT a benc <- exprToSMT b pure $ "(ite (= " <> benc <> " (_ bv0 256)) (_ bv0 256) " <> "(" <> op `sp` aenc `sp` benc <> "))" - -sp :: Builder -> Builder -> Builder -a `sp` b = a <> (fromText " ") <> b - -zero :: Builder -zero = "(_ bv0 256)" - -one :: Builder -one = "(_ bv1 256)" - -propToSMT :: Prop -> Err Builder -propToSMT = \case + divModOp :: Builder -> Builder -> Expr x -> Expr y -> Err Builder + divModOp concreteOp abstractOp a b = case divEnc of + ConcreteDivMod -> op2CheckZero concreteOp a b + AbstractDivMod -> op2 abstractOp a b + -- symbolic*symbolic multiplication: native under ConcreteDivMod, an + -- uninterpreted function under AbstractDivMod (no zero guard needed). + mulOp :: Expr x -> Expr y -> Err Builder + mulOp a b = case divEnc of + ConcreteDivMod -> op2 "bvmul" a b + AbstractDivMod -> op2 "abst_evm_bvmul" a b + +propToSMTWith :: DivModEncoding -> Prop -> Err Builder +propToSMTWith divEnc = \case PEq a b -> op2 "=" a b PLT a b -> op2 "bvult" a b PGT a b -> op2 "bvugt" a b @@ -634,19 +663,18 @@ propToSMT = \case pure $ "(=> " <> aenc <> " " <> benc <> ")" PBool b -> pure $ if b then "true" else "false" where + propToSMT :: Prop -> Err Builder + propToSMT = propToSMTWith divEnc + op2 :: Builder -> Expr x -> Expr y -> Err Builder op2 op a b = do - aenc <- exprToSMT a - benc <- exprToSMT b + aenc <- exprToSMTWith divEnc a + benc <- exprToSMTWith divEnc b pure $ "(" <> op <> " " <> aenc <> " " <> benc <> ")" - - -- ** Helpers ** --------------------------------------------------------------------------------- - --- | Stores a region of src into dst -copySlice :: Expr EWord -> Expr EWord -> Expr EWord -> Builder -> Builder -> Err Builder -copySlice srcOffset dstOffset (Lit size) src dst = do +copySliceWith :: DivModEncoding -> Expr EWord -> Expr EWord -> Expr EWord -> Builder -> Builder -> Err Builder +copySliceWith divEnc srcOffset dstOffset (Lit size) src dst = do sz <- internal size pure $ "(let ((src " <> src <> ")) " <> sz <> ")" where @@ -659,38 +687,35 @@ copySlice srcOffset dstOffset (Lit size) src dst = do pure $ "(store " <> child `sp` encDstOff `sp` "(select src " <> encSrcOff <> "))" offset :: W256 -> Expr EWord -> Err Builder offset o (Lit b) = pure $ wordAsBV $ o + b - offset o e = exprToSMT $ Expr.add (Lit o) e -copySlice _ _ _ _ _ = Left "CopySlice with a symbolically sized region not currently implemented, cannot execute SMT solver on this query" + offset o e = exprToSMTWith divEnc $ Expr.add (Lit o) e +copySliceWith _ _ _ _ _ _ = Left "CopySlice with a symbolically sized region not currently implemented, cannot execute SMT solver on this query" --- | Unrolls an exponentiation into a series of multiplications -expandExp :: Expr EWord -> W256 -> Err Builder -expandExp base expnt +expandExpWith :: DivModEncoding -> Expr EWord -> W256 -> Err Builder +expandExpWith divEnc base expnt -- in EVM, anything (including 0) to the power of 0 is 1 | expnt == 0 = pure one - | expnt == 1 = exprToSMT base + | expnt == 1 = exprToSMTWith divEnc base | otherwise = do - b <- exprToSMT base - n <- expandExp base (expnt - 1) + b <- exprToSMTWith divEnc base + n <- expandExpWith divEnc base (expnt - 1) pure $ "(bvmul " <> b `sp` n <> ")" --- | Concatenates a list of bytes into a larger bitvector -concatBytes :: [Expr Byte] -> Err Builder -concatBytes bytes = do +concatBytesWith :: DivModEncoding -> [Expr Byte] -> Err Builder +concatBytesWith divEnc bytes = do case List.uncons $ reverse bytes of Nothing -> Left "unexpected empty bytes" Just (h, t) -> do - a2 <- exprToSMT h + a2 <- exprToSMTWith divEnc h foldM wrap a2 t where wrap :: Builder -> Expr a -> Err Builder wrap inner byte = do - byteSMT <- exprToSMT byte + byteSMT <- exprToSMTWith divEnc byte pure $ "(concat " <> byteSMT `sp` inner <> ")" --- | Concatenates a list of bytes into a larger bitvector -writeBytes :: ByteString -> Expr Buf -> Err Builder -writeBytes bytes buf = do - smtText <- exprToSMT buf +writeBytesWith :: DivModEncoding -> ByteString -> Expr Buf -> Err Builder +writeBytesWith divEnc bytes buf = do + smtText <- exprToSMTWith divEnc buf let ret = BS.foldl wrap (0, smtText) bytes pure $ snd ret where @@ -704,13 +729,13 @@ writeBytes bytes buf = do where !idx' = idx + 1 -encodeConcreteStore :: Map W256 W256 -> Err Builder -encodeConcreteStore s = foldM encodeWrite ("((as const Storage) #x0000000000000000000000000000000000000000000000000000000000000000)") (Map.toList s) +encodeConcreteStore :: DivModEncoding -> Map W256 W256 -> Err Builder +encodeConcreteStore enc s = foldM encodeWrite ("((as const Storage) #x0000000000000000000000000000000000000000000000000000000000000000)") (Map.toList s) where encodeWrite :: Builder -> (W256, W256) -> Err Builder encodeWrite prev (key, val) = do - encKey <- exprToSMT $ Lit key - encVal <- exprToSMT $ Lit val + encKey <- exprToSMTWith enc $ Lit key + encVal <- exprToSMTWith enc $ Lit val pure $ "(store " <> prev `sp` encKey `sp` encVal <> ")" storeName :: Expr EAddr -> Maybe W256 -> Builder @@ -885,8 +910,8 @@ getStore getVal (StorageReads innerMap) = do queryValue :: ValGetter -> Expr EWord -> MaybeIO W256 queryValue _ (Lit w) = pure w queryValue getVal w = do - -- this exprToSMT should never fail, since we have already ran the solver - let expr = toLazyText $ fromRight' $ exprToSMT w + -- this exprToSMTWith should never fail, since we have already ran the solver, in refined mode + let expr = toLazyText $ fromRight' $ exprToSMTWith ConcreteDivMod w raw <- getVal expr hoistMaybe $ do valTxt <- extractValue raw diff --git a/src/EVM/SMT/AbstractBase.hs b/src/EVM/SMT/AbstractBase.hs new file mode 100644 index 000000000..b800f67b1 --- /dev/null +++ b/src/EVM/SMT/AbstractBase.hs @@ -0,0 +1,228 @@ +{- | + Module: EVM.SMT.AbstractBase + Description: Shared vocabulary for the abstract arithmetic encoding. + + Base layer for 'EVM.SMT.AbstractLemmas' (the lemma catalogue) and + 'EVM.SMT.DivModEncoding' (orchestration + div/mod ground truth): the div/mod + taxonomy, term collectors/matchers, signed-reconstruction helpers, and the + term /saturation/ ('saturate') that closes the set of div/mul terms the + lemmas range over. Lives below both so neither needs to import the other for + these definitions. +-} +module EVM.SMT.AbstractBase + ( Enc + , divModAbstractDecls + , mulNoOverflow + -- * Div/mod taxonomy + , DivModKind(..) + , DivModOp + , AbstractKey(..) + , isDiv + , isSigned + , abstFnName + , concFnName + , abstractKey + -- * Collectors and shape matchers + , collectDivMods + , collectMuls + , collectConstMuls + , hasAbstractMul + , asMul + , asConstMul + -- * Signed reconstruction helpers + , smtZeroGuard + , smtAbsolute + , signedFromUnsignedDiv + , signedFromUnsignedMod + -- * Abstract-term saturation + , AbstractCtx(..) + , saturate + ) where + +import Data.Containers.ListUtils (nubOrd) +import Data.Text.Lazy.Builder + +import EVM.SMT.SMTLIB (sp, zero) +import EVM.SMT.Types +import EVM.Traversals +import EVM.Types (Prop(..), EType(EWord), Err, W256, Expr, Expr(Lit)) +import EVM.Types qualified as T + +-- | The expression-to-SMT encoder threaded through every emitter. +type Enc = Expr EWord -> Err Builder + +-- | Uninterpreted-function declarations standing in for div/mod/mul. The +-- div/mod UFs are refined against the native ops in phase two; abst_evm_bvmul +-- is kept fully uninterpreted (no ground truth), constrained only by the +-- lemmas in "EVM.SMT.AbstractLemmas". +divModAbstractDecls :: [SMTEntry] +divModAbstractDecls = + [ SMTComment "abstract division/modulo/multiplication (uninterpreted functions; mul has no ground truth)" + , SMTCommand "(declare-fun abst_evm_bvsdiv ((_ BitVec 256) (_ BitVec 256)) (_ BitVec 256))" + , SMTCommand "(declare-fun abst_evm_bvsrem ((_ BitVec 256) (_ BitVec 256)) (_ BitVec 256))" + , SMTCommand "(declare-fun abst_evm_bvudiv ((_ BitVec 256) (_ BitVec 256)) (_ BitVec 256))" + , SMTCommand "(declare-fun abst_evm_bvurem ((_ BitVec 256) (_ BitVec 256)) (_ BitVec 256))" + , SMTCommand "(declare-fun abst_evm_bvmul ((_ BitVec 256) (_ BitVec 256)) (_ BitVec 256))" + ] + +-- | A /sufficient/ condition for x*y not to overflow 256 bits: both operands +-- fit in 128 bits. Deliberately cheaper than the exact predicate +-- @extract 511 256 (bvmul (zext x) (zext y)) = 0@, which forces a 512-bit +-- multiply per lemma instance and times out on large operands. SOUND: when the +-- guard holds there is genuinely no overflow; the cost is completeness for +-- operands above 2^128 (callers bound operands, e.g. @require(x < 2**128)@). +mulNoOverflow :: Builder -> Builder -> Builder +mulNoOverflow x y = + "(and (bvule " <> x <> " " <> maxU128 <> ") (bvule " <> y <> " " <> maxU128 <> "))" + where maxU128 = "(_ bv340282366920938463463374607431768211455 256)" + +-- | The four EVM division/modulo operations, kept in signed/unsigned groups so +-- the sign-reconstruction machinery is never applied to unsigned operands. +data DivModKind = IsSDiv | IsSMod | IsUDiv | IsUMod + deriving (Eq, Ord) + +type DivModOp = (DivModKind, Expr EWord, Expr EWord) + +data AbstractKey = AbstractKey (Expr EWord) (Expr EWord) DivModKind + deriving (Eq, Ord) + +isDiv :: DivModKind -> Bool +isDiv IsSDiv = True +isDiv IsUDiv = True +isDiv _ = False + +isSigned :: DivModKind -> Bool +isSigned IsSDiv = True +isSigned IsSMod = True +isSigned _ = False + +-- | Name of the uninterpreted function standing in for this op. +abstFnName :: DivModKind -> Builder +abstFnName IsSDiv = "abst_evm_bvsdiv" +abstFnName IsSMod = "abst_evm_bvsrem" +abstFnName IsUDiv = "abst_evm_bvudiv" +abstFnName IsUMod = "abst_evm_bvurem" + +-- | Name of the concrete SMT-LIB op refined against in phase two. +concFnName :: DivModKind -> Builder +concFnName IsSDiv = "bvsdiv" +concFnName IsSMod = "bvsrem" +concFnName IsUDiv = "bvudiv" +concFnName IsUMod = "bvurem" + +abstractKey :: DivModOp -> AbstractKey +abstractKey (kind, a, b) = AbstractKey a b kind + +collectDivMods :: Expr a -> [DivModOp] +collectDivMods = \case + T.SDiv a b -> [(IsSDiv, a, b)] + T.SMod a b -> [(IsSMod, a, b)] + T.Div a b -> [(IsUDiv, a, b)] + T.Mod a b -> [(IsUMod, a, b)] + _ -> [] + +collectMuls :: Expr a -> [(Expr EWord, Expr EWord)] +collectMuls = maybe [] pure . asMul + +collectConstMuls :: Expr a -> [(W256, Expr EWord)] +collectConstMuls = maybe [] pure . asConstMul + +-- | True if any prop contains a symbolic*symbolic multiplication. Because +-- abst_evm_bvmul has no ground truth, a satisfying model may assign it values +-- inconsistent with real multiplication; callers must downgrade SAT to Unknown +-- to stay sound. (UNSAT — the proof direction — is unaffected.) +hasAbstractMul :: [Prop] -> Bool +hasAbstractMul props = not $ null $ concatMap (foldProp collectMuls []) props + +-- | An abstracted symbolic*symbolic product. Products with a concrete factor +-- are handled natively, so only genuinely symbolic products are abstracted. +asMul :: Expr a -> Maybe (Expr EWord, Expr EWord) +asMul (T.Mul x y) | notLit x, notLit y = Just (x, y) +asMul _ = Nothing + +-- | A product by a non-trivial literal constant: c*x or x*c (excluding 0, 1). +-- These stay native @bvmul@; the const-mul lemmas range over them. +asConstMul :: Expr a -> Maybe (W256, Expr EWord) +asConstMul (T.Mul (Lit c) x) | notLit x, c /= 0, c /= 1 = Just (c, x) +asConstMul (T.Mul x (Lit c)) | notLit x, c /= 0, c /= 1 = Just (c, x) +asConstMul _ = Nothing + +notLit :: Expr a -> Bool +notLit (Lit _) = False +notLit _ = True + +-- | (ite (= divisor 0) 0 result) — the EVM's x/0 = 0 convention. +smtZeroGuard :: Builder -> Builder -> Builder +smtZeroGuard divisor nonZeroResult = + "(ite (=" `sp` divisor `sp` zero <> ")" `sp` zero `sp` nonZeroResult <> ")" + +smtAbsolute :: Builder -> Builder +smtAbsolute x = "(ite (bvsge" `sp` x `sp` zero <> ")" `sp` x `sp` "(bvsub" `sp` zero `sp` x <> "))" + +smtNeg :: Builder -> Builder +smtNeg x = "(bvsub" `sp` zero `sp` x <> ")" + +smtSameSign :: Builder -> Builder -> Builder +smtSameSign a b = "(=" `sp` "(bvslt" `sp` a `sp` zero <> ")" `sp` "(bvslt" `sp` b `sp` zero <> "))" + +smtIsNonNeg :: Builder -> Builder +smtIsNonNeg x = "(bvsge" `sp` x `sp` zero <> ")" + +-- | sdiv(a,b) = ITE(b = 0, 0, +-- ITE(sign(a) = sign(b), udiv(|a|,|b|), +-- -udiv(|a|,|b|))) +signedFromUnsignedDiv :: Builder -> Builder -> Builder -> Builder +signedFromUnsignedDiv aenc benc udivResult = + smtZeroGuard benc $ + "(ite" `sp` (smtSameSign aenc benc) `sp` + udivResult `sp` (smtNeg udivResult) <> ")" + +-- | smod(a,b) = ITE(b = 0, 0, +-- ITE(a ≥ 0, urem(|a|,|b|), +-- -urem(|a|,|b|))) +signedFromUnsignedMod :: Builder -> Builder -> Builder -> Builder +signedFromUnsignedMod aenc benc uremResult = + smtZeroGuard benc $ + "(ite" `sp` (smtIsNonNeg aenc) `sp` + uremResult `sp` (smtNeg uremResult) <> ")" + +-- | The saturated set of abstract arithmetic terms a property mentions, built +-- once by 'saturate'; the lemma catalogue ranges over these fields. +data AbstractCtx = AbstractCtx + { acUDivs :: [(Expr EWord, Expr EWord)] + -- ^ Unsigned divisions, including the synthetic ones added by 'saturate'. + , acMuls :: [(Expr EWord, Expr EWord)] + -- ^ Symbolic*symbolic products, including the div-mul link products. + , acConstMuls :: [(W256, Expr EWord)] + -- ^ Products @c*x@ by a non-trivial literal constant. + } + +-- | Close the set of div/mul terms the lemmas range over. Beyond the raw terms +-- a prop mentions, three synthetic families are added so single-level lemmas +-- can bridge multi-level code (SOUND — each synthetic term is an exact EVM +-- operation some lemma then equates to its closed form): +-- +-- * /synthetic divisions/: when a product @a*b@ reuses a factor that is a +-- divisor elsewhere, add @(a*b)/factor@ — lets mulDiv-bound and +-- div-monotonicity bridge cross-divisor round-trips. +-- * /nested-division collapse/: @(A/c1)/c2@ also contributes @A/(c1*c2)@, so +-- single-divide lemmas match code that splits precision across two divides. +-- * /div-mul link products/: every division @a/b@ contributes the product +-- @(a/b)*b@ that the link lemma bounds by @a@. +saturate :: [Prop] -> AbstractCtx +saturate props = + let udivs = [ (a, b) | (IsUDiv, a, b) <- nubOrd $ concatMap (foldProp collectDivMods []) props ] + muls = nubOrd $ concatMap (foldProp collectMuls []) props + constMuls = nubOrd $ concatMap (foldProp collectConstMuls []) props + divisors = nubOrd [ b | (_, b) <- udivs ] + synthDivs = nubOrd $ [ (T.Mul a b, b) | (a, b) <- muls, b `elem` divisors ] + <> [ (T.Mul a b, a) | (a, b) <- muls, a `elem` divisors ] + collapsedDivs = nubOrd + [ (innerA, Lit (c1 * c2)) + | (a, b) <- udivs <> synthDivs, Lit c2 <- [b] + , T.Div innerA (Lit c1) <- [a] + , c1 /= 0, c2 /= 0, toInteger c1 * toInteger c2 < 2 ^ (256 :: Int) ] + udivsAll = nubOrd (udivs <> synthDivs <> collapsedDivs) + linkMuls = [ (T.Div a b, b) | (a, b) <- udivsAll ] + allMuls = nubOrd (muls <> linkMuls) + in AbstractCtx { acUDivs = udivsAll, acMuls = allMuls, acConstMuls = constMuls } diff --git a/src/EVM/SMT/AbstractLemmas.hs b/src/EVM/SMT/AbstractLemmas.hs new file mode 100644 index 000000000..d28fb7147 --- /dev/null +++ b/src/EVM/SMT/AbstractLemmas.hs @@ -0,0 +1,253 @@ +{- | + Module: EVM.SMT.AbstractLemmas + Description: The catalogue of sound algebraic lemmas for abstract arithmetic. + + Multiplication is kept fully uninterpreted (no ground truth, so the solver + never bit-blasts a symbolic product); we add only /sound/ algebraic facts + about @abst_evm_bvmul@/@abst_evm_bvudiv@. Each lemma is a 'LemmaInst' + constructor, a 'collectLemmas' clause (its trigger) and an 'emitLemma' + clause (the SMT it emits + why it is sound); GHC's exhaustiveness checker + ties the three together. To audit soundness, read 'emitLemma': every + emitted assertion is true of ordinary arithmetic, so anything derived from + them holds for the real operations too. +-} +module EVM.SMT.AbstractLemmas + ( LemmaInst(..) + , collectLemmas + , emitLemma + ) where + +import Data.Containers.ListUtils (nubOrd) + +import EVM.SMT.AbstractBase +import EVM.SMT.SMTLIB (sp, zero, one, wordAsBV) +import EVM.SMT.Types (SMTEntry(..)) +import EVM.Types (EType(EWord), Err, W256, Expr, Expr(Lit)) +import EVM.Types qualified as T + +-- | A single firing of a lemma family, carrying the sub-terms it matched. +data LemmaInst + = Comm (Expr EWord) (Expr EWord) -- ^ a*b = b*a + | Identity (Expr EWord) (Expr EWord) -- ^ x*0, 0*y, x*1, 1*y + | DivMulLink (Expr EWord) (Expr EWord) -- ^ (a/b)*b <= a + | MulMono (Expr EWord) (Expr EWord) (Expr EWord) -- ^ x<=y => x*z<=y*z + | DivMono (Expr EWord) (Expr EWord) (Expr EWord) -- ^ x<=y => x/z<=y/z + | DivisorMono (Expr EWord) (Expr EWord) (Expr EWord) -- ^ y1<=y2 => x/y2<=x/y1 + | MulDivBound (Expr EWord) (Expr EWord) (Expr EWord) (Expr EWord) -- ^ (x*y)/z <= x or y + | ConstMulMono W256 (Expr EWord) (Expr EWord) -- ^ x<=y => c*x<=c*y + | ConstCancel (Expr EWord) W256 W256 (Expr EWord) -- ^ (c1*x)/c2 == (c1/c2)*x + | NestedDiv (Expr EWord) W256 W256 -- ^ (A/c1)/c2 == A/(c1*c2) + | FracReduce (Expr EWord) W256 W256 (Expr EWord) -- ^ (c1*x)/c2 == x/(c2/c1) + | CeilDivCancel (Expr EWord) W256 W256 (Expr EWord) -- ^ ceilDiv(c1*x,c2) inner divide + | Telescope (Expr EWord) (Expr EWord) W256 W256 -- ^ (a*b)/c - (a*(b-k))/c == a*(k/c) + deriving (Eq, Ord) + +-- | Every lemma instance triggered by the saturated term set, in emission +-- order. One clause per family; see 'emitLemma' for the math. +collectLemmas :: AbstractCtx -> [LemmaInst] +collectLemmas ctx = + -- commutativity + 0/1 identities over every product + [ Comm a b | (a, b) <- ctx.acMuls ] + <> [ Identity a b | (a, b) <- ctx.acMuls ] + -- the div<->mul link, one per division + <> [ DivMulLink a b | (a, b) <- ctx.acUDivs ] + -- monotonicities over shared-operand pairs + <> [ MulMono x y z | (x, y, z) <- sharedPairs (bothOrders (ctx.acMuls)) ] + <> [ DivMono x y z | (x, y, z) <- sharedPairs (ctx.acUDivs) ] + <> [ DivisorMono y1 y2 x | (y1, y2, x) <- divisorPairs (ctx.acUDivs) ] + -- product-over-divisor bound, for divisions whose dividend is a product + <> [ MulDivBound a x y b | (a, b) <- ctx.acUDivs, Just (x, y) <- [asMul a] ] + -- const-mul monotonicity over const-products sharing the same constant + <> [ ConstMulMono c x y | (c, x) <- ctx.acConstMuls, (c', y) <- ctx.acConstMuls, c == c', x /= y ] + -- constant cancellation / fraction reduction over constant divisions + <> [ ConstCancel a c1 c2 x + | (a, b) <- ctx.acUDivs, Just (c1, x) <- [asConstMul a] + , Lit c2 <- [b], c2 /= 0, c1 `mod` c2 == 0 ] + <> [ NestedDiv innerA c1 c2 + | (a, b) <- ctx.acUDivs, Lit c2 <- [b] + , T.Div innerA (Lit c1) <- [a] + , c1 /= 0, c2 /= 0, toInteger c1 * toInteger c2 < 2 ^ (256 :: Int) ] + <> [ FracReduce a c1 c2 x + | (a, b) <- ctx.acUDivs, Just (c1, x) <- [asConstMul a] + , Lit c2 <- [b], c2 /= 0, c1 /= 0, c2 `mod` c1 == 0, c2 /= c1 ] + <> [ CeilDivCancel a c1 c2 x + | (a, b) <- ctx.acUDivs, T.Sub inner (Lit 1) <- [a] + , Just (c1, x) <- [asConstMul inner] + , Lit c2 <- [b], c2 /= 0, c1 `mod` c2 == 0 ] + -- scaled-product telescoping (the only cross-product lemma) + <> [ Telescope a b k c | (a, b, k, c) <- telescopes ] + where + telescopes = nubOrd + [ (a, b, k, c) + | (sd, Lit c) <- ctx.acUDivs, c /= 0 + , Just (f1, f2) <- [asMul sd] + , (a, T.Sub b (Lit k)) <- [(f1, f2), (f2, f1)] + , k /= 0, k `mod` c == 0 + , any (`elem` ctx.acUDivs) [ (T.Mul a b, Lit c), (T.Mul b a, Lit c) ] ] + +-- | Emit the SMT assertion(s) for a single lemma instance. Each clause is the +-- sound fact, with its no-overflow / divisor guard where one is required. +emitLemma :: Enc -> LemmaInst -> Err [SMTEntry] + +-- commutativity: abst_evm_bvmul(a,b) = abst_evm_bvmul(b,a), so lemma terms +-- match the props regardless of operand order. +emitLemma enc (Comm a b) = do + aenc <- enc a; benc <- enc b + let m1 = "(abst_evm_bvmul" `sp` aenc `sp` benc <> ")" + m2 = "(abst_evm_bvmul" `sp` benc `sp` aenc <> ")" + pure [ SMTCommand $ "(assert (=" `sp` m1 `sp` m2 <> "))" ] + +-- 0/1 identities pinning the otherwise-free UF: x*0 = 0*y = 0, x*1 = x, 1*y = y +emitLemma enc (Identity a b) = do + aenc <- enc a; benc <- enc b + let m = "(abst_evm_bvmul" `sp` aenc `sp` benc <> ")" + pure [ SMTCommand $ "(assert (=> (=" `sp` aenc `sp` zero <> ") (=" `sp` m `sp` zero <> ")))" + , SMTCommand $ "(assert (=> (=" `sp` benc `sp` zero <> ") (=" `sp` m `sp` zero <> ")))" + , SMTCommand $ "(assert (=> (=" `sp` aenc `sp` one <> ") (=" `sp` m `sp` benc <> ")))" + , SMTCommand $ "(assert (=> (=" `sp` benc `sp` one <> ") (=" `sp` m `sp` aenc <> ")))" + ] + +-- div<->mul link (sound unconditionally, (a/b)*b <= a < 2^256 cannot +-- overflow): quotient*divisor <= dividend. Links the div and mul abstractions +-- and chains nested divisions. +emitLemma enc (DivMulLink a b) = do + aenc <- enc a; benc <- enc b + let q = "(abst_evm_bvudiv" `sp` aenc `sp` benc <> ")" + qb = "(abst_evm_bvmul" `sp` q `sp` benc <> ")" + pure [ SMTCommand $ "(assert (bvule" `sp` qb `sp` aenc <> "))" ] + +-- mul monotonicity (no-overflow guarded, hence sound): +-- x <= y => x*z <= y*z +emitLemma enc (MulMono x y z) = do + xenc <- enc x; yenc <- enc y; zenc <- enc z + let mxz = "(abst_evm_bvmul" `sp` xenc `sp` zenc <> ")" + myz = "(abst_evm_bvmul" `sp` yenc `sp` zenc <> ")" + pure [ SMTCommand $ "(assert (=> (and" `sp` mulNoOverflow xenc zenc `sp` mulNoOverflow yenc zenc + <> " (bvule" `sp` xenc `sp` yenc <> ")) (bvule" `sp` mxz `sp` myz <> ")))" ] + +-- div monotonicity in the dividend (sound unconditionally): +-- x <= y => floor(x/z) <= floor(y/z) +emitLemma enc (DivMono x y z) = do + xenc <- enc x; yenc <- enc y; zenc <- enc z + let dxz = "(abst_evm_bvudiv" `sp` xenc `sp` zenc <> ")" + dyz = "(abst_evm_bvudiv" `sp` yenc `sp` zenc <> ")" + pure [ SMTCommand $ "(assert (=> (bvule" `sp` xenc `sp` yenc <> ") (bvule" `sp` dxz `sp` dyz <> ")))" ] + +-- div anti-monotonicity in the divisor (sound for nonzero divisors): a bigger +-- divisor yields a smaller-or-equal quotient. +-- y1 <= y2 && y1 != 0 => x/y2 <= x/y1 +emitLemma enc (DivisorMono y1 y2 x) = do + y1e <- enc y1; y2e <- enc y2; xe <- enc x + let dxy1 = "(abst_evm_bvudiv" `sp` xe `sp` y1e <> ")" + dxy2 = "(abst_evm_bvudiv" `sp` xe `sp` y2e <> ")" + pure [ SMTCommand $ "(assert (=> (and (distinct" `sp` y1e `sp` zero <> ")" + <> " (bvule" `sp` y1e `sp` y2e <> ")) (bvule" `sp` dxy2 `sp` dxy1 <> ")))" ] + +-- mulDiv bound (sound under no-overflow of x*z): if one factor is <= the +-- divisor then dividing the product by it cannot exceed the other factor. +-- y <= z => (x*y)/z <= x x <= z => (x*y)/z <= y +-- `a` is the original product expr, so the div term matches the prop exactly. +emitLemma enc (MulDivBound a x y z) = do + ae <- enc a; xe <- enc x; ye <- enc y; ze <- enc z + let dv = "(abst_evm_bvudiv" `sp` ae `sp` ze <> ")" + pure [ SMTCommand $ "(assert (=> (and (bvule" `sp` ye `sp` ze <> ")" `sp` mulNoOverflow xe ze + <> ") (bvule" `sp` dv `sp` xe <> ")))" + , SMTCommand $ "(assert (=> (and (bvule" `sp` xe `sp` ze <> ")" `sp` mulNoOverflow ye ze + <> ") (bvule" `sp` dv `sp` ye <> ")))" ] + +-- const-mul monotonicity (sound, no-overflow guarded): x <= y => c*x <= c*y. +-- c is concrete, so the exact bound floor((2^256-1)/c) is computed at encode +-- time and the guard is one comparison. c*x stays a native bvmul; the lemma +-- lets the solver order two such products without bit-blasting the multiply. +emitLemma enc (ConstMulMono c x y) = do + xe <- enc x; ye <- enc y + let cbv = wordAsBV c + cx = "(bvmul" `sp` cbv `sp` xe <> ")" + cy = "(bvmul" `sp` cbv `sp` ye <> ")" + bnd = wordAsBV ((maxBound :: W256) `div` c) -- largest x with c*x < 2^256 + pure [ SMTCommand $ "(assert (=> (and (bvule" `sp` xe `sp` bnd <> ") (bvule" `sp` ye `sp` bnd <> ")" + <> " (bvule" `sp` xe `sp` ye <> ")) (bvule" `sp` cx `sp` cy <> ")))" ] + +-- const cancellation (sound, no-overflow guarded): (c1*x)/c2 == (c1/c2)*x +-- when c2 | c1 — the precision-scaling wrapper, e.g. amount*1e18/1e6. +-- `a` is the dividend expr (c1*x), kept so the div term matches the prop. +emitLemma enc (ConstCancel a c1 c2 x) = do + ae <- enc a; xe <- enc x + let c2bv = wordAsBV c2 + k = c1 `div` c2 -- exact, since c2 | c1 + rhs = if k == 1 then xe else "(bvmul" `sp` wordAsBV k `sp` xe <> ")" + dv = "(abst_evm_bvudiv" `sp` ae `sp` c2bv <> ")" + bnd = wordAsBV ((maxBound :: W256) `div` c1) -- largest x with c1*x < 2^256 + pure [ SMTCommand $ "(assert (=> (bvule" `sp` xe `sp` bnd <> ") (=" `sp` dv `sp` rhs <> ")))" ] + +-- nested-division collapse (sound floor identity, no guard needed): +-- (A/c1)/c2 == A/(c1*c2) for literal c1,c2 with c1*c2 < 2^256, +-- e.g. x*rate/1e9/1e18 == x*rate/1e27. +emitLemma enc (NestedDiv innerA c1 c2) = do + ae <- enc innerA + let inner = "(abst_evm_bvudiv" `sp` ae `sp` wordAsBV c1 <> ")" + outer = "(abst_evm_bvudiv" `sp` inner `sp` wordAsBV c2 <> ")" + collapsed = "(abst_evm_bvudiv" `sp` ae `sp` wordAsBV (c1 * c2) <> ")" + pure [ SMTCommand $ "(assert (=" `sp` outer `sp` collapsed <> "))" ] + +-- fraction-reduce (sound, no-overflow guarded): (c1*x)/c2 == x/(c2/c1) when +-- c1 | c2 — the mirror of const-cancel (multiply by small, divide by large, +-- e.g. x*1e6/1e18 == x/1e12). Under the guard c1*x is exact, and +-- floor(c1*x / (c1*k)) = floor(x/k). +emitLemma enc (FracReduce a c1 c2 x) = do + ae <- enc a; xe <- enc x + let k = c2 `div` c1 -- exact and >= 2, since c1 | c2 and c2 /= c1 + dv = "(abst_evm_bvudiv" `sp` ae `sp` wordAsBV c2 <> ")" -- (c1*x)/c2 + rhs = "(abst_evm_bvudiv" `sp` xe `sp` wordAsBV k <> ")" -- x/(c2/c1) + bnd = wordAsBV ((maxBound :: W256) `div` c1) -- largest x with c1*x < 2^256 + pure [ SMTCommand $ "(assert (=> (bvule" `sp` xe `sp` bnd <> ") (=" `sp` dv `sp` rhs <> ")))" ] + +-- ceilDiv-cancel (sound, guarded): pins the abstracted divide inside +-- OpenZeppelin's Math.ceilDiv(c1*x, c2) = (c1*x - 1)/c2 + 1. When c2 | c1, +-- write c1 = c2*m: floor((c2*m*x - 1)/c2) = m*x - 1 for m*x >= 1, so with the +-- ceilDiv's +1 the quote is exactly (c1/c2)*x. Guarded by x >= 1 (the ceilDiv +-- ITE handles x==0) and no-overflow. `a` is the (c1*x - 1) dividend expr. +emitLemma enc (CeilDivCancel a c1 c2 x) = do + ae <- enc a; xe <- enc x + let m = c1 `div` c2 -- exact, since c2 | c1 + mx = if m == 1 then xe else "(bvmul" `sp` wordAsBV m `sp` xe <> ")" + dv = "(abst_evm_bvudiv" `sp` ae `sp` wordAsBV c2 <> ")" -- (c1*x - 1)/c2 + rhs = "(bvsub" `sp` mx `sp` one <> ")" -- (c1/c2)*x - 1 + bnd = wordAsBV ((maxBound :: W256) `div` c1) -- largest x with c1*x < 2^256 + pure [ SMTCommand $ "(assert (=> (and (bvuge" `sp` xe `sp` one <> ")" + <> " (bvule" `sp` xe `sp` bnd <> ")) (=" `sp` dv `sp` rhs <> ")))" ] + +-- scaled-product telescoping (sound, no-overflow guarded). For products +-- sharing factor a whose other factors differ by a literal k with c | k: +-- floor(a*b/c) == floor(a*(b-k)/c) + a*(k/c) +-- Sound: a*b = a*(b-k) + a*k and a*k is an exact multiple of c, so removing it +-- shifts the floor by exactly a*(k/c). The only lemma pinning the EXACT +-- difference of two abstract products (value-change accounting, e.g. +-- susds*rate/1e27 - susds). b >= k in the guard rules out wraparound in b-k. +emitLemma enc (Telescope a b k c) = do + ae <- enc a; be <- enc b + let m = k `div` c -- exact, since c | k + cbv = wordAsBV c + full = "(abst_evm_bvmul" `sp` ae `sp` be <> ")" + stepped = "(abst_evm_bvmul" `sp` ae `sp` ("(bvsub" `sp` be `sp` wordAsBV k <> ")") <> ")" + dFull = "(abst_evm_bvudiv" `sp` full `sp` cbv <> ")" + dStep = "(abst_evm_bvudiv" `sp` stepped `sp` cbv <> ")" + coeff = if m == 1 then ae else "(bvmul" `sp` wordAsBV m `sp` ae <> ")" + rhs = "(bvadd" `sp` dStep `sp` coeff <> ")" + pure [ SMTCommand $ "(assert (=> (and" `sp` mulNoOverflow ae be + <> " (bvuge" `sp` be `sp` wordAsBV k <> ")) (=" `sp` dFull `sp` rhs <> ")))" ] + +-- | Both operand orders of each product, so monotonicity fires regardless of +-- how the simplifier ordered the operands. +bothOrders :: [(Expr EWord, Expr EWord)] -> [(Expr EWord, Expr EWord)] +bothOrders xs = nubOrd (xs <> [ (b, a) | (a, b) <- xs ]) + +-- | Ordered pairs (x, y, z) where (x,z) and (y,z) both occur (shared 2nd +-- operand): products by a common factor, or divisions by a common divisor. +sharedPairs :: [(Expr EWord, Expr EWord)] -> [(Expr EWord, Expr EWord, Expr EWord)] +sharedPairs xs = [ (x, y, z) | (x, z) <- xs, (y, z') <- xs, z == z', x /= y ] + +-- | Ordered pairs (y1, y2, x) where (x,y1) and (x,y2) both occur (shared 1st +-- operand): divisions of the same dividend by different divisors. +divisorPairs :: [(Expr EWord, Expr EWord)] -> [(Expr EWord, Expr EWord, Expr EWord)] +divisorPairs xs = [ (y1, y2, x) | (x, y1) <- xs, (x', y2) <- xs, x == x', y1 /= y2 ] diff --git a/src/EVM/SMT/DivModEncoding.hs b/src/EVM/SMT/DivModEncoding.hs new file mode 100644 index 000000000..74304bdaa --- /dev/null +++ b/src/EVM/SMT/DivModEncoding.hs @@ -0,0 +1,174 @@ +{- | Abstract div/mod encoding for two-phase SMT solving. + + Orchestration layer. The shared vocabulary (primitives, collectors, + 'saturate') lives in "EVM.SMT.AbstractBase"; the multiplication lemma + catalogue lives in "EVM.SMT.AbstractLemmas". This module wires them together + ('mulEncoding') and holds the div/mod /ground-truth/ encoding — the phase that + refines the abstract uninterpreted functions against real bvudiv/bvsdiv using + absolute values, shift bounds, and congruence. +-} +module EVM.SMT.DivModEncoding + ( divModGroundTruth + , divModEncoding + , divModAbstractDecls + , mulEncoding + , hasAbstractMul + ) where + +import Data.Bits (countTrailingZeros) +import Data.Containers.ListUtils (nubOrd) +import Data.List (groupBy, sortBy) +import Data.Ord (comparing) +import Data.Text.Lazy.Builder (Builder, fromString) + +import EVM.SMT.AbstractBase +import EVM.SMT.AbstractLemmas (collectLemmas, emitLemma) +import EVM.SMT.SMTLIB (sp, zero, wordAsBV) +import EVM.SMT.Types +import EVM.Traversals (foldProp) +import EVM.Types (Prop, EType(EWord), Err, W256, Expr, Expr(Lit), Expr(SHL)) + +-- | Lemmas for abstract multiplication. Multiplication is kept fully +-- uninterpreted (no ground truth, so the solver never bit-blasts a symbolic +-- product); we add only the sound algebraic facts catalogued in +-- "EVM.SMT.AbstractLemmas". 'saturate' closes the term set the lemmas range +-- over; 'collectLemmas' picks the instances; 'emitLemma' renders each to SMT. +mulEncoding :: Enc -> [Prop] -> Err [SMTEntry] +mulEncoding enc props = do + let ctx = saturate props + if null ctx.acUDivs && null ctx.acMuls && null ctx.acConstMuls then pure [] + else do + lemmas <- concat <$> mapM (emitLemma enc) (collectLemmas ctx) + pure $ (SMTComment "multiplication abstraction lemmas") : lemmas + +-- | Declare the magnitude variables and the unsigned result variable for a +-- group. For signed ops the magnitudes are the absolute values |a|, |b|; for +-- unsigned ops the operands are already non-negative, so the magnitude is the +-- operand itself (|x| = x). +declareAbsolute :: Enc -> DivModKind -> Int -> Expr EWord -> Expr EWord -> Builder -> Err ([SMTEntry], (Builder, Builder)) +declareAbsolute enc kind groupIdx firstA firstB unsignedResult = do + aenc <- enc firstA + benc <- enc firstB + let magnitude x = if isSigned kind then smtAbsolute x else x + absoluteAEnc = magnitude aenc + absoluteBEnc = magnitude benc + absoluteAName = fromString $ "absolute_a" <> show groupIdx + absoluteBName = fromString $ "absolute_b" <> show groupIdx + let decls = [ SMTCommand $ "(declare-const" `sp` absoluteAName `sp` "(_ BitVec 256))" + , SMTCommand $ "(declare-const" `sp` absoluteBName `sp` "(_ BitVec 256))" + , SMTCommand $ "(declare-const" `sp` unsignedResult `sp` "(_ BitVec 256))" + , SMTCommand $ "(assert (=" `sp` absoluteAName `sp` absoluteAEnc <> "))" + , SMTCommand $ "(assert (=" `sp` absoluteBName `sp` absoluteBEnc <> "))" + ] + pure (decls, (absoluteAName, absoluteBName)) + +-- | Assert "abstract div/mod(a,b)" = result derived from the unsigned result +-- variable. Signed ops reconstruct the sign from |a|/|b|; unsigned ops need +-- only the EVM divide-by-zero guard, since the unsigned result is the answer. +assertAbstEqResult :: Enc -> Builder -> DivModOp -> Err SMTEntry +assertAbstEqResult enc unsignedResult (kind, a, b) = do + aenc <- enc a + benc <- enc b + let abstract = "(" <> abstFnName kind `sp` aenc `sp` benc <> ")" + concrete = case kind of + IsSDiv -> signedFromUnsignedDiv aenc benc unsignedResult + IsSMod -> signedFromUnsignedMod aenc benc unsignedResult + IsUDiv -> smtZeroGuard benc unsignedResult + IsUMod -> smtZeroGuard benc unsignedResult + pure $ SMTCommand $ "(assert (=" `sp` abstract `sp` concrete <> "))" + +-- | Ground-truth axioms: for each sdiv/smod op, assert that the abstract +-- uninterpreted function equals the real bvsdiv/bvsrem. +-- e.g. (assert (= (abst_evm_bvsdiv a b) (bvsdiv a b))) +divModGroundTruth :: Enc -> [Prop] -> Err [SMTEntry] +divModGroundTruth enc props = do + let allDivMods = nubOrd $ concatMap (foldProp collectDivMods []) props + if null allDivMods then pure [] + else do + axioms <- mapM mkGroundTruthAxiom allDivMods + pure $ (SMTComment "division/modulo ground-truth refinement") : axioms + where + mkGroundTruthAxiom :: DivModOp -> Err SMTEntry + mkGroundTruthAxiom (kind, a, b) = do + aenc <- enc a + benc <- enc b + let abstract = "(" <> abstFnName kind `sp` aenc `sp` benc <> ")" + native = "(" <> concFnName kind `sp` aenc `sp` benc <> ")" + -- EVM defines x/0 = 0 and x%0 = 0, whereas SMT-LIB's native bvudiv/ + -- bvurem return non-zero on a zero divisor; guard the unsigned ops so + -- the axiom matches op2CheckZero and the encoding's zero guard. (The + -- signed reconstruction already applies the guard on its side.) + concrete = if isSigned kind then native else smtZeroGuard benc native + pure $ SMTCommand $ "(assert (=" `sp` abstract `sp` concrete <> "))" + +-- | Encode div/mod operations using abs values, shift-bounds, and congruence (no bvudiv). +divModEncoding :: Enc -> [Prop] -> Err [SMTEntry] +divModEncoding enc props = do + let allDivMods = nubOrd $ concatMap (foldProp collectDivMods []) props + if null allDivMods then pure [] + else do + let groups = groupBy (\a b -> abstractKey a == abstractKey b) $ sortBy (comparing abstractKey) allDivMods + indexedGroups = zip [0..] groups + let links = mkCongruenceLinks indexedGroups + entries <- concat <$> mapM (uncurry mkGroupEncoding) indexedGroups + pure $ (SMTComment "division/modulo encoding (abs + shift-bounds + congruence, no bvudiv)") : entries <> links + where + knownPow2Bound :: Expr EWord -> Maybe W256 + knownPow2Bound (SHL (Lit k) _) = Just k + knownPow2Bound (Lit n) | n > 0 = Just (fromIntegral $ countTrailingZeros n) + knownPow2Bound _ = Nothing + + mkGroupEncoding :: Int -> [DivModOp] -> Err [SMTEntry] + mkGroupEncoding _ [] = pure [] + mkGroupEncoding groupIdx lhs@((firstKind, firstA, firstB) : _) = do + let isDiv' = isDiv firstKind + prefix = if isDiv' then "udiv" else "urem" + unsignedResult = fromString $ prefix <> "_" <> show groupIdx + (decls, (absoluteA, absoluteB)) <- declareAbsolute enc firstKind groupIdx firstA firstB unsignedResult + + -- When the dividend is a left-shift (a = x << k, i.e. a = x * 2^k), + -- we can bound the unsigned division result using cheap bitshift + -- operations instead of the expensive bvudiv SMT theory. + -- The pivot point is |a| >> k (= |a| / 2^k): + -- - If |b| >= 2^k: result <= |a| >> k (upper bound) + -- - If |b| < 2^k and b != 0: result >= |a| >> k (lower bound) + let shiftBounds = case (isDiv', knownPow2Bound firstA) of + (True, Just k) -> + let kLit = wordAsBV k + -- twoPowK = 2^k + twoPowK = "(bvshl (_ bv1 256) " <> kLit <> ")" + -- shifted = |a| >> k = |a| / 2^k + shifted = "(bvlshr" `sp` absoluteA `sp` kLit <> ")" + in -- |b| >= 2^k => |a|/|b| <= |a|/2^k + [ SMTCommand $ "(assert (=> (bvuge" `sp` absoluteB `sp` twoPowK <> ") (bvule" `sp` unsignedResult `sp` shifted <> ")))" + -- |b| < 2^k and |b| != 0 => |a|/|b| >= |a|/2^k + , SMTCommand $ "(assert (=> " + <> "(and (bvult" `sp` absoluteB `sp` twoPowK <> ") (distinct " `sp` absoluteB `sp` zero <> "))" + <> "(bvuge" `sp` unsignedResult `sp` shifted <> ")))" + ] + _ -> [] + axioms <- mapM (assertAbstEqResult enc unsignedResult) lhs + pure $ decls <> shiftBounds <> axioms + +-- | Congruence: if two groups of the same kind have equal magnitude inputs, +-- their results are equal. Signed and unsigned groups are linked separately so +-- a signed op is never tied to an unsigned op (and vice versa). +mkCongruenceLinks :: [(Int, [DivModOp])] -> [SMTEntry] +mkCongruenceLinks indexedGroups = + let groupsOfKind want = [(i, ops) | (i, ops@((k,_,_):_)) <- indexedGroups , k == want] + in concatMap (mkPairLinks "udiv") (allPairs (groupsOfKind IsSDiv)) + <> concatMap (mkPairLinks "urem") (allPairs (groupsOfKind IsSMod)) + <> concatMap (mkPairLinks "udiv") (allPairs (groupsOfKind IsUDiv)) + <> concatMap (mkPairLinks "urem") (allPairs (groupsOfKind IsUMod)) + where + allPairs xs = [(a, b) | a <- xs, b <- xs, fst a < fst b] + mkPairLinks prefix' ((i, _), (j, _)) = + let absoluteAi = fromString $ "absolute_a" <> show i + abosluteBi = fromString $ "absolute_b" <> show i + absoluteAj = fromString $ "absolute_a" <> show j + absoluteBj = fromString $ "absolute_b" <> show j + absoluteResI = fromString $ prefix' <> "_" <> show i + absoluteRedJ = fromString $ prefix' <> "_" <> show j + in [ SMTCommand $ "(assert (=> " + <> "(and (=" `sp` absoluteAi `sp` absoluteAj <> ") (=" `sp` abosluteBi `sp` absoluteBj <> "))" + <> "(=" `sp` absoluteResI `sp` absoluteRedJ <> ")))" ] diff --git a/src/EVM/SMT/SMTLIB.hs b/src/EVM/SMT/SMTLIB.hs index e10325c91..bf64a759e 100644 --- a/src/EVM/SMT/SMTLIB.hs +++ b/src/EVM/SMT/SMTLIB.hs @@ -2,15 +2,33 @@ module EVM.SMT.SMTLIB ( prelude, toText, - hasDuplicateCommands + hasDuplicateCommands, + -- * Builder primitives + sp, + zero, + one, + wordAsBV ) where import Data.Containers.ListUtils (nubOrd) import Data.Text.Lazy (Text) import Data.Text.Lazy.Builder +import qualified Data.Text.Lazy.Builder.Int import EVM.SMT.Types +sp :: Builder -> Builder -> Builder +a `sp` b = a <> " " <> b + +zero :: Builder +zero = "(_ bv0 256)" + +one :: Builder +one = "(_ bv1 256)" + +wordAsBV :: forall a. Integral a => a -> Builder +wordAsBV w = "(_ bv" <> Data.Text.Lazy.Builder.Int.decimal w <> " 256)" + prelude :: SMT2 prelude = SMT2 src mempty mempty where diff --git a/src/EVM/SMT/Types.hs b/src/EVM/SMT/Types.hs index 57b9f95a1..3a595b079 100644 --- a/src/EVM/SMT/Types.hs +++ b/src/EVM/SMT/Types.hs @@ -11,6 +11,9 @@ import EVM.Types type MaybeIO = MaybeT IO +data DivModEncoding = ConcreteDivMod | AbstractDivMod + deriving (Show, Eq) + data SMTEntry = SMTCommand Builder | SMTComment Builder deriving (Eq) diff --git a/src/EVM/Solvers.hs b/src/EVM/Solvers.hs index e2938acfb..11e9a555e 100644 --- a/src/EVM/Solvers.hs +++ b/src/EVM/Solvers.hs @@ -128,9 +128,30 @@ checkSatWithProps sg props = do if psSimp == [PBool False] then pure Qed else do let concreteKeccaks = fmap (\(buf,val) -> PEq (Lit val) (Keccak buf)) (toList $ Keccak.concreteKeccaks props) - let smt2 = assertProps conf (if conf.simp then psSimp <> concreteKeccaks else psSimp) - if isLeft smt2 then pure $ Error $ getError smt2 - else liftIO $ checkSat sg (Just props) smt2 + let allProps = if conf.simp then psSimp <> concreteKeccaks else psSimp + if not conf.abstractArith then do + let smt2 = assertProps conf allProps + if isLeft smt2 then pure $ Error $ getError smt2 + else liftIO $ checkSat sg (Just props) smt2 + else liftIO $ do + -- Two-phase solving: assert the abstract (uninterpreted) div/mod/mul plus + -- the sound lemmas, then append the div/mod ground truth as refinement. + let smt2Abstract = assertPropsAbstract conf allProps + let refinement = divModGroundTruth (exprToSMTWith AbstractDivMod) allProps + if isLeft smt2Abstract then pure $ Error $ getError smt2Abstract + else if isLeft refinement then pure $ Error $ getError refinement + else do + let x = getNonError smt2Abstract <> SMT2 (SMTScript (getNonError refinement)) mempty mempty + res <- checkSat sg (Just props) (Right x) + -- SOUNDNESS: multiplication is abstracted as an uninterpreted function + -- with no ground truth, so a satisfying model may use product values + -- inconsistent with real multiplication. A QED stays sound (the lemmas + -- over-approximate), but a counterexample may be spurious, so downgrade + -- it to Unknown. + pure $ case res of + Cex _ | hasAbstractMul allProps -> + Unknown "counterexample unsound under multiplication abstraction (abst_evm_bvmul is uninterpreted)" + _ -> res -- When props is Nothing, the cache will not be filled or used checkSat :: SolverGroup -> Maybe [Prop] -> Err SMT2 -> IO SMTResult @@ -264,6 +285,9 @@ getMultiSol solver timeout maxMemory smt2@(SMT2 cmds cexvars _) multiSol r sem f ) getOneSol :: (MonadIO m, ReadConfig m) => Solver -> Maybe Natural -> Natural -> SMT2 -> Maybe [Prop] -> Chan SMTResult -> TChan CacheEntry -> QSem -> Int -> m () +-- the empty solver answers every query "unknown" without spawning a process +getOneSol EmptySolver _ _ _ _ r _ _ _ = + liftIO $ writeChan r (Unknown "Result unknown by SMT solver") getOneSol solver timeout maxMemory smt2@(SMT2 cmds cexvars _) props r cacheq sem fileCounter = do conf <- readConfig liftIO $ bracket_ diff --git a/test/clitest.hs b/test/clitest.hs index b84b8462f..0f6aa749e 100644 --- a/test/clitest.hs +++ b/test/clitest.hs @@ -163,7 +163,6 @@ main = do (T.count "Merged forward jump in file" (T.pack stderr)) `shouldBe` 4 stdout `shouldContain` "Counterexample:" exitCode `shouldBe` (ExitFailure 1) - it "crash-of-hevm" $ do let hexStrA = "608060405234801561001057600080fd5b506004361061002b5760003560e01c8063efa2978514610030575b600080fd5b61004361003e3660046102ad565b610045565b005b60006100508561007a565b9050600061005d866100a8565b905080821461006e5761006e61034c565b50505050505050505050565b600061008761032e6103aa565b8261009457610197610098565b61013e5b6100a291906103e2565b92915050565b60006100b561032e6103aa565b6100be906103aa565b6100c7906103aa565b82806100d1575060005b806100da575060005b61013157605a6100ea60006103aa565b6100f3906103aa565b6100ff6001605a610404565b61010b6001605a610404565b61011891166101976103e2565b6101229190610493565b61012c9190610493565b610149565b604061013f8161013e6103e2565b6101499190610493565b61015391906103e2565b61016061032e60006103e2565b83801561016b575060015b15801590610177575060015b80156101a05750831515801561018b575060015b15158015610197575060015b806101a0575060005b610251576101976101b3605a602d610493565b602d60006101c2600182610493565b6101cd906001610404565b6101d8906001610404565b6101e1906103aa565b6101ea906103aa565b6101f491906103e2565b6101ff90605a610404565b604e61020c8160016103e2565b6102169190610493565b61022490600116605a610404565b1661022e906103aa565b61023891906103e2565b6102429190610493565b61024c9190610493565b610283565b604561025f8161013e6103e2565b6102699190610493565b60456102778161013e6103e2565b6102819190610493565b165b61028d91906103e2565b1692915050565b80358015155b81146100a257600080fd5b80358061029a565b600080600080600080600080610100898b0312156102ca57600080fd5b6102d48a8a610294565b97506102e38a60208b01610294565b96506102f28a60408b016102a5565b95506103018a60608b016102a5565b94506103108a60808b01610294565b935061031f8a60a08b016102a5565b925061032e8a60c08b01610294565b915061033d8a60e08b016102a5565b90509295985092959890939650565b7f4e487b7100000000000000000000000000000000000000000000000000000000600052600160045260246000fd5b7f4e487b7100000000000000000000000000000000000000000000000000000000600052601160045260246000fd5b60007f800000000000000000000000000000000000000000000000000000000000000082036103db576103db61037b565b5060000390565b818103600083128015838313168383129190911617156100a2576100a261037b565b60008261043a577f4e487b7100000000000000000000000000000000000000000000000000000000600052601260045260246000fd5b7f800000000000000000000000000000000000000000000000000000000000000082147fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff8414161561048e5761048e61037b565b500590565b80820160008212801584831290811690159190911617156100a2576100a261037b56fea26469706673582212200a37769e5bf4b8b890caac8ab643126d55feb821a0201d2f674203f23fa666ad64736f6c634300081e0033" @@ -226,10 +225,9 @@ main = do shouldBe fileExists True removeFile filename it "early-abort" $ do - (exitcode, stdout, stderr) <- runForge "test/contracts/pass/early-abort.sol" ["--max-iterations", "1000"] - putStrLn $ "Exit code: " ++ show exitcode - putStrLn stderr - putStrLn stdout + (_, stdout, _) <- runForge "test/contracts/pass/early-abort.sol" ["--max-iterations", "1000"] + stdout `shouldContain` "[FAIL]" + (T.count "Counterexample:" (T.pack stdout)) `shouldBe` 9 it "rpc-cache" $ do (_, stdout, stderr) <- runForge "test/contracts/fail/rpc-test.sol" ["--rpc", "http://mock.mock", "--prefix", "test_attack_symbolic" diff --git a/test/test.hs b/test/test.hs index e10c098b6..d0ccebb5d 100644 --- a/test/test.hs +++ b/test/test.hs @@ -55,7 +55,7 @@ import EVM.Fetch qualified as Fetch import EVM.Format (hexText) import EVM.Precompiled import EVM.RLP -import EVM.SMT hiding (one) +import EVM.SMT import EVM.Solidity import EVM.Solvers import EVM.Stepper qualified as Stepper @@ -106,6 +106,10 @@ testNoSimplify :: TestName -> ReaderT Env IO () -> TestTree testNoSimplify a b = let testEnvNoSimp = Env { config = testEnv.config { simp = False } } in testCase a $ runEnv testEnvNoSimp b +testAbstractArith :: TestName -> ReaderT Env IO () -> TestTree +testAbstractArith a b = let testEnvAbstract = Env { config = testEnv.config { abstractArith = True } } + in testCase a $ runEnv testEnvAbstract b + prop :: Testable prop => ReaderT Env IO prop -> Property prop a = ioProperty $ runEnv testEnv a @@ -123,6 +127,9 @@ withCVC5Solver = withSolvers CVC5 3 Nothing defMemLimit withBitwuzlaSolver :: App m => (SolverGroup -> m a) -> m a withBitwuzlaSolver = withSolvers Bitwuzla 3 Nothing defMemLimit +withShortBitwuzlaSolver :: App m => (SolverGroup -> m a) -> m a +withShortBitwuzlaSolver = withSolvers Bitwuzla 3 (Just 5) defMemLimit + main :: IO () main = defaultMain tests @@ -914,6 +921,914 @@ tests = testGroup "hevm" let exprSimp = map Expr.simplify paths assertBoolM "expected partial execution" (any isPartial exprSimp) ] + -- NOTE: Foundry/Dapp tests moved to EVM.Test.FoundryTests + , testGroup "Arith" + -- Tests adapted from halmos (tests/regression/test/Arith.t.sol, tests/solver/test/SignedDiv.t.sol, tests/solver/test/Math.t.sol) + -- Run with abstractArith = True to exercise two-phase solving + [ test "math-avg" $ do + Just c <- solcRuntime "C" [i| + contract C { + function prove_Avg(uint a, uint b) external pure { + require(a + b >= a); + unchecked { + uint r1 = (a & b) + (a ^ b) / 2; + uint r2 = (a + b) / 2; + assert(r1 == r2); + } + } + } |] + (_, res) <- withBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertEqualM "Must be QED" [] res + , test "unsigned-div-by-zero" $ do + Just c <- solcRuntime "C" [i| + contract C { + function prove_unsigned_div_by_zero(uint256 a) external pure { + uint256 result; + assembly { result := div(a, 0) } + assert(result == 0); + } + } |] + (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertEqualM "Must be QED" [] res + , test "arith-div-pass" $ do + Just c <- solcRuntime "C" [i| + contract C { + function prove_Div_pass(uint x, uint y) external pure { + require(x > y); + require(y > 0); + uint q; + assembly { q := div(x, y) } + assert(q != 0); + } + } |] + (_, res) <- withBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertEqualM "Must be QED" [] res + , test "arith-div-fail" $ do + Just c <- solcRuntime "C" [i| + contract C { + function prove_Div_fail(uint x, uint y) external pure { + require(x > y); + uint q; + assembly { q := div(x, y) } + assert(q != 0); + } + } |] + (_, res) <- withBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertBoolM "Expected counterexample" (any isCex res) + , test "arith-mod-fail" $ do + Just c <- solcRuntime "C" [i| + contract C { + function prove_Div_fail(uint x, uint y) external pure { + require(x > y); + uint q; + assembly { q := mod(x, y) } + assert(q != 0); + } + } |] + (_, res) <- withBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertBoolM "Expected counterexample" (any isCex res) + ] + , testGroup "Abstract-Arith" + -- "make verify-hevm T=prove_div_negative_divisor" in https://github.com/gustavo-grieco/abdk-math-64.64-verification + [ testCase "prove_div_values-abdk" $ do + Just c <- solcRuntime "C" [i| + contract C { + bool public IS_TEST = true; + + int128 private constant MIN_64x64 = -0x80000000000000000000000000000000; + int128 private constant MAX_64x64 = 0x7FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF; + + // ABDKMath64x64.fromInt(0) == 0 + int128 private constant ZERO_FP = 0; + // ABDKMath64x64.fromInt(1) == 1 << 64 + int128 private constant ONE_FP = 0x10000000000000000; + + // ABDKMath64x64.div + function div(int128 x, int128 y) internal pure returns (int128) { + unchecked { + require(y != 0); + int256 result = (int256(x) << 64) / y; + require(result >= MIN_64x64 && result <= MAX_64x64); + return int128(result); + } + } + + // ABDKMath64x64.abs + function abs(int128 x) internal pure returns (int128) { + unchecked { + require(x != MIN_64x64); + return x < 0 ? -x : x; + } + } + + // Property: |x / y| <= |x| when |y| >= 1, and |x / y| >= |x| when |y| < 1 + function prove_div_values(int128 x, int128 y) public pure { + require(y != ZERO_FP); + + int128 x_y = abs(div(x, y)); + + if (abs(y) >= ONE_FP) { + assert(x_y <= abs(x)); + } else { + assert(x_y >= abs(x)); + } + } + } |] + let sig = (Just $ Sig "prove_div_values(int128,int128)" [AbiIntType 128, AbiIntType 128]) + let testEnvAbstract = Env { config = testEnv.config { abstractArith = True } } + runEnv testEnvAbstract $ do + (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts + -- with abstract arith, we prove it + assertEqualM "Must be QED" res [] + runEnv testEnv $ do + (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts + -- without abstract arith, we time out + liftIO $ assertBool "Must be unknown" (all isUnknown res) + -- "make verify-hevm T=prove_div_negative_divisor" in https://github.com/gustavo-grieco/abdk-math-64.64-verification + , testCase "prove_div_negative_divisor" $ do + Just c <- solcRuntime "C" [i| + contract C { + bool public IS_TEST = true; + + int128 private constant MIN_64x64 = -0x80000000000000000000000000000000; + int128 private constant MAX_64x64 = 0x7FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF; + + // ABDKMath64x64.fromInt(0) == 0 + int128 private constant ZERO_FP = 0; + + // ABDKMath64x64.div + function div(int128 x, int128 y) internal pure returns (int128) { + unchecked { + require(y != 0); + int256 result = (int256(x) << 64) / y; + require(result >= MIN_64x64 && result <= MAX_64x64); + return int128(result); + } + } + + // ABDKMath64x64.neg + function neg(int128 x) internal pure returns (int128) { + unchecked { + require(x != MIN_64x64); + return -x; + } + } + + // Property: x / (-y) == -(x / y) + function prove_div_negative_divisor(int128 x, int128 y) public pure { + require(y < ZERO_FP); + + int128 x_y = div(x, y); + int128 x_minus_y = div(x, neg(y)); + + assert(x_y == neg(x_minus_y)); + } + } |] + let sig = (Just $ Sig "prove_div_negative_divisor(int128,int128)" [AbiIntType 128, AbiIntType 128]) + let testEnvAbstract = Env { config = testEnv.config { abstractArith = True } } + runEnv testEnvAbstract $ do + (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts + -- with abstract arith, we prove it + assertEqualM "Must be QED" res [] + runEnv testEnv $ do + (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts + -- without abstract arith, we time out + liftIO $ assertBool "Must be unknown" (all isUnknown res) + + , testAbstractArith "sdiv-by-one" $ do + Just c <- solcRuntime "C" [i| + contract C { + function prove_sdiv_by_one(int256 a) external pure { + int256 result; + assembly { result := sdiv(a, 1) } + assert(result == a); + } + } |] + (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertEqualM "Must be QED" res [] + , testAbstractArith "sdiv-by-neg-one" $ do + Just c <- solcRuntime "C" [i| + contract C { + function prove_sdiv_by_neg_one(int256 a) external pure { + int256 result; + assembly { result := sdiv(a, sub(0, 1)) } + if (a == -170141183460469231731687303715884105728 * 2**128) { // type(int256).min + assert(result == a); + } else { + assert(result == -a); + } + } + } |] + (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertEqualM "Must be QED" res [] + , testAbstractArith "sdiv-intmin-by-two" $ do + Just c <- solcRuntime "C" [i| + contract C { + function prove_sdiv_intmin_by_two() external pure { + int256 result; + assembly { + let intmin := 0x8000000000000000000000000000000000000000000000000000000000000000 + result := sdiv(intmin, 2) + } + // -2**254 is 0xc000...0000 + assert(result == -0x4000000000000000000000000000000000000000000000000000000000000000); + } + } |] + (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertEqualM "Must be QED" [] res + , testAbstractArith "smod-by-zero" $ do + Just c <- solcRuntime "C" [i| + contract C { + function prove_smod_by_zero(int256 a) external pure { + int256 result; + assembly { result := smod(a, 0) } + assert(result == 0); + } + } |] + (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertEqualM "Must be QED" res [] + , testAbstractArith "smod-intmin-by-three" $ do + Just c <- solcRuntime "C" [i| + contract C { + function prove_smod_intmin_by_three() external pure { + int256 result; + assembly { result := smod(0x8000000000000000000000000000000000000000000000000000000000000000, 3) } + assert(result == -2); + } + } |] + (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertEqualM "Must be QED" res [] + , testAbstractArith "sdiv-by-zero" $ do + Just c <- solcRuntime "C" [i| + contract C { + function prove_sdiv_by_zero(int256 a) external pure { + int256 result; + assembly { result := sdiv(a, 0) } + assert(result == 0); + } + } |] + (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertEqualM "Must be QED" [] res + , testAbstractArith "sdiv-zero-dividend" $ do + Just c <- solcRuntime "C" [i| + contract C { + function prove_sdiv_zero_dividend(int256 b) external pure { + int256 result; + assembly { result := sdiv(0, b) } + assert(result == 0); + } + } |] + (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertEqualM "Must be QED" [] res + , testAbstractArith "sdiv-truncation" $ do + Just c <- solcRuntime "C" [i| + contract C { + function prove_sdiv_truncation() external pure { + int256 result; + assembly { result := sdiv(sub(0, 7), 2) } + assert(result == -3); + } + } |] + (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertEqualM "Must be QED" [] res + , testAbstractArith "sdiv-sign-symmetry" $ do + Just c <- solcRuntime "C" [i| + contract C { + function prove_sdiv_sign_symmetry(int256 a, int256 b) external pure { + if (a == -57896044618658097711785492504343953926634992332820282019728792003956564819968) return; + if (b == -57896044618658097711785492504343953926634992332820282019728792003956564819968) return; + if (b == 0) return; + int256 r1; + int256 r2; + assembly { + r1 := sdiv(a, b) + r2 := sdiv(sub(0, a), sub(0, b)) + } + assert(r1 == r2); + } + } |] + (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertEqualM "Must be QED" [] res + , testAbstractArith "sdiv-sign-antisymmetry" $ do + Just c <- solcRuntime "C" [i| + contract C { + function prove_sdiv_sign_antisymmetry(int256 a, int256 b) external pure { + if (a == -57896044618658097711785492504343953926634992332820282019728792003956564819968) return; + if (b == 0) return; + int256 r1; + int256 r2; + assembly { + r1 := sdiv(a, b) + r2 := sdiv(sub(0, a), b) + } + assert(r1 == -r2); + } + } |] + (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertEqualM "Must be QED" [] res + , testAbstractArith "smod-by-one" $ do + Just c <- solcRuntime "C" [i| + contract C { + function prove_smod_by_one(int256 a) external pure { + int256 r1; + int256 r2; + assembly { + r1 := smod(a, 1) + r2 := smod(a, sub(0, 1)) + } + assert(r1 == 0); + assert(r2 == 0); + } + } |] + (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertEqualM "Must be QED" [] res + , testAbstractArith "smod-zero-dividend" $ do + Just c <- solcRuntime "C" [i| + contract C { + function prove_smod_zero_dividend(int256 b) external pure { + int256 result; + assembly { result := smod(0, b) } + assert(result == 0); + } + } |] + (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertEqualM "Must be QED" [] res + , testAbstractArith "smod-sign-matches-dividend" $ do + Just c <- solcRuntime "C" [i| + contract C { + function prove_smod_sign_matches_dividend(int256 a, int256 b) external pure { + if (b == 0 || a == 0) return; + int256 result; + assembly { result := smod(a, b) } + if (result != 0) { + assert((a > 0 && result > 0) || (a < 0 && result < 0)); + } + } + } |] + (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertEqualM "Must be QED" [] res + , testAbstractArith "smod-intmin" $ do + Just c <- solcRuntime "C" [i| + contract C { + function prove_smod_intmin() external pure { + int256 result; + assembly { result := smod(0x8000000000000000000000000000000000000000000000000000000000000000, 2) } + assert(result == 0); + } + } |] + (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertEqualM "Must be QED" [] res + , testAbstractArith "sdiv-intmin-by-neg-one" $ do + Just c <- solcRuntime "C" [i| + contract C { + function prove_sdiv_intmin_by_neg_one() external pure { + int256 result; + assembly { + let intmin := 0x8000000000000000000000000000000000000000000000000000000000000000 + result := sdiv(intmin, sub(0, 1)) + } + // EVM defines sdiv(MIN_INT, -1) = MIN_INT (overflow) + assert(result == -57896044618658097711785492504343953926634992332820282019728792003956564819968); + } + } |] + (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertEqualM "Must be QED" [] res + , testAbstractArith "smod-intmin-by-neg-one" $ do + Just c <- solcRuntime "C" [i| + contract C { + function prove_smod_intmin_by_neg_one() external pure { + int256 result; + assembly { + let intmin := 0x8000000000000000000000000000000000000000000000000000000000000000 + result := smod(intmin, sub(0, 1)) + } + // smod(MIN_INT, -1) = 0 since MIN_INT is divisible by -1 + assert(result == 0); + } + } |] + (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertEqualM "Must be QED" [] res + , testAbstractArith "sdiv-intmin-by-intmin" $ do + Just c <- solcRuntime "C" [i| + contract C { + function prove_sdiv_intmin_by_intmin() external pure { + int256 result; + assembly { + let intmin := 0x8000000000000000000000000000000000000000000000000000000000000000 + result := sdiv(intmin, intmin) + } + assert(result == 1); + } + } |] + (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertEqualM "Must be QED" [] res + , testAbstractArith "arith-mod" $ do + Just c <- solcRuntime "C" [i| + contract C { + function unchecked_smod(int x, int y) internal pure returns (int ret) { + assembly { ret := smod(x, y) } + } + function prove_Mod(int x, int y) external pure { + unchecked { + assert(unchecked_smod(x, 0) == 0); + assert(x % 1 == 0); + assert(x % 2 < 2 && x % 2 > -2); + assert(x % 4 < 4 && x % 4 > -4); + int x_smod_y = unchecked_smod(x, y); + assert(x_smod_y <= y || y < 0);} + } + } |] + (_, res) <- withBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertEqualM "Must be QED" [] res + -- Unsigned div/mod exercise the abst_evm_bvudiv / abst_evm_bvurem + -- uninterpreted functions and the two-phase refinement. + , testAbstractArith "udiv-by-one" $ do + Just c <- solcRuntime "C" [i| + contract C { + function prove_udiv_by_one(uint256 a) external pure { + uint256 result = a / 1; + assert(result == a); + } + } |] + (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertEqualM "Must be QED" [] res + , testAbstractArith "udiv-by-zero" $ do + Just c <- solcRuntime "C" [i| + contract C { + function prove_udiv_by_zero(uint256 a) external pure { + // EVM div-by-zero yields 0; Solidity's `/` reverts, so use raw DIV + uint256 result; + assembly { result := div(a, 0) } + assert(result == 0); + } + } |] + (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertEqualM "Must be QED" [] res + , testAbstractArith "udiv-self" $ do + -- symbolic divisor: a genuine abst_evm_bvudiv application + Just c <- solcRuntime "C" [i| + contract C { + function prove_udiv_self(uint256 a) external pure { + require(a != 0); + uint256 result = a / a; + assert(result == 1); + } + } |] + (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertEqualM "Must be QED" [] res + , testAbstractArith "umod-by-one" $ do + Just c <- solcRuntime "C" [i| + contract C { + function prove_umod_by_one(uint256 a) external pure { + uint256 result = a % 1; + assert(result == 0); + } + } |] + (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertEqualM "Must be QED" [] res + , testAbstractArith "umod-range" $ do + -- a % b < b for b != 0; needs the ground-truth refinement of bvurem + Just c <- solcRuntime "C" [i| + contract C { + function prove_umod_range(uint256 a, uint256 b) external pure { + require(b != 0); + uint256 result = a % b; + assert(result < b); + } + } |] + (_, res) <- withBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertEqualM "Must be QED" [] res + , testAbstractArith "udiv-le-dividend" $ do + -- a / b <= a for b != 0; refines bvudiv (symbolic divisor) + Just c <- solcRuntime "C" [i| + contract C { + function prove_udiv_le_dividend(uint256 a, uint256 b) external pure { + require(b != 0); + uint256 r = a / b; + assert(r <= a); + } + } |] + (_, res) <- withBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertEqualM "Must be QED" [] res + , testAbstractArith "udiv-cex" $ do + -- false property: div(a,b) can be 0 (e.g. a=0). The abstract path must + -- still find a real counterexample after refinement. + Just c <- solcRuntime "C" [i| + contract C { + function prove_udiv_nonzero(uint256 a, uint256 b) external pure { + require(b != 0); + uint256 result = a / b; + assert(result != 0); + } + } |] + (_, res) <- withBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertBoolM "Expected counterexample" (any isCex res) + , testAbstractArith "vault-preview-shares" $ do + -- ERC-4626-style share pricing in 64.64 fixed point: + -- shares = (assets * 2^64) / price + -- When each share costs at least 1.0 (price >= 2^64), a deposit can + -- never mint more shares than assets. The power-of-two dividend + -- (assets << 64) lets the shift-bounds encoding discharge this without + -- the bvudiv theory; native bvudiv leaves the solver at "unknown". + Just c <- solcRuntime "C" [i| + contract C { + function previewShares(uint256 assets, uint256 price) internal pure returns (uint256 shares) { + shares = (assets << 64) / price; + } + function prove_vault_no_inflation(uint256 assets, uint256 price) external pure { + require(price >= (1 << 64)); // >= 1.0 per share + require(assets < (1 << 128)); // assets << 64 stays within 256 bits + uint256 shares = previewShares(assets, price); + assert(shares <= assets); + } + } |] + (_, res) <- withBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertEqualM "Must be QED" [] res + , ignoreTestBecause "Abstract arithmetic cannot find counterexample for this case" $ testAbstractArith "math-mint-fail" $ do + Just c <- solcRuntime "C" [i| + contract C { + function prove_mint(uint s, uint A1, uint S1) external pure { + uint a = (s * A1) / S1; + uint A2 = A1 + a; + uint S2 = S1 + s; + assert(A1 * S2 <= A2 * S1); + } + } |] + (_, res) <- withBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertBoolM "Expected counterexample" (any isCex res) + ] + , testGroup "Mul-Abstraction" + -- Symbolic*symbolic multiplication is abstracted as an uninterpreted + -- function (abst_evm_bvmul) with sound lemmas (commutativity, 0/1 + -- identities, quotient*divisor<=dividend, no-overflow-guarded monotonicity) + -- and NO ground truth. This proves vault-style properties native solving + -- cannot, while staying SOUND: a QED is a real proof; spurious or + -- overflow-dependent results are never reported as bugs (downgraded to + -- Unknown). Bounding (e.g. require(x < 2**128)) is supplied in Solidity. + [ testAbstractArith "mul-monotone" $ do + -- a1 <= a2 => a1*c <= a2*c, under no-overflow (mul-monotonicity lemma) + Just c <- solcRuntime "C" [i| + contract C { + function prove_mul_monotone(uint256 a1, uint256 a2, uint256 k) external pure { + require(a1 < (1<<128) && a2 < (1<<128) && k < (1<<128)); + require(a1 <= a2); + uint256 p1; uint256 p2; + assembly { p1 := mul(a1, k) p2 := mul(a2, k) } + assert(p1 <= p2); + } + } |] + (_, res) <- withBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertEqualM "Must be QED" [] res + , testAbstractArith "mul-by-zero" $ do + -- x*y == 0 when y == 0 (0-identity lemma; y is symbolic, not folded) + Just c <- solcRuntime "C" [i| + contract C { + function prove_mul_zero(uint256 x, uint256 y) external pure { + require(y == 0); + uint256 p; assembly { p := mul(x, y) } + assert(p == 0); + } + } |] + (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertEqualM "Must be QED" [] res + , testAbstractArith "mul-by-one" $ do + -- x*y == x when y == 1 (1-identity lemma) + Just c <- solcRuntime "C" [i| + contract C { + function prove_mul_one(uint256 x, uint256 y) external pure { + require(y == 1); + uint256 p; assembly { p := mul(x, y) } + assert(p == x); + } + } |] + (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertEqualM "Must be QED" [] res + , testAbstractArith "div-mul-link" $ do + -- (x/y)*y <= x for y != 0 (div x mul link lemma; needs commutativity) + Just c <- solcRuntime "C" [i| + contract C { + function prove_div_mul_link(uint256 x, uint256 y) external pure { + require(y != 0); + uint256 q; uint256 p; + assembly { q := div(x, y) p := mul(q, y) } + assert(p <= x); + } + } |] + (_, res) <- withBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertEqualM "Must be QED" [] res + , testCase "vault-shares-monotonic" $ do + -- ERC-4626: more assets deposited => at least as many shares. Provable + -- WITH abstraction, native solving times out (unknown). + Just c <- solcRuntime "C" [i| + contract C { + uint256 public totalAssets; + uint256 public totalShares; + function prove_shares_monotonic(uint256 a1, uint256 a2) external view { + require(totalAssets != 0); + require(a1 < (1<<128) && a2 < (1<<128) && totalShares < (1<<128)); + require(a1 <= a2); + uint256 ts = totalShares; uint256 ta = totalAssets; + uint256 s1; uint256 s2; + assembly { s1 := div(mul(a1, ts), ta) s2 := div(mul(a2, ts), ta) } + assert(s1 <= s2); + } + } |] + let testEnvAbstract = Env { config = testEnv.config { abstractArith = True } } + runEnv testEnvAbstract $ do + (_, res) <- withBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertEqualM "Must be QED with abstraction" [] res + runEnv testEnv $ do + (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + liftIO $ assertBool "Must be unknown natively" (all isUnknown res) + , testAbstractArith "mul-overflow-not-unsound" $ do + -- SOUNDNESS: unbounded monotonicity is FALSE (raw mul wraps); the + -- no-overflow guard must prevent a (bogus) QED -> Unknown, never QED. + Just c <- solcRuntime "C" [i| + contract C { + function prove_mul_monotone_overflow(uint256 a1, uint256 a2, uint256 k) external pure { + require(a1 <= a2); + uint256 p1; uint256 p2; + assembly { p1 := mul(a1, k) p2 := mul(a2, k) } + assert(p1 <= p2); + } + } |] + (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertBoolM "Must be Unknown, never QED (unsound proof avoided)" + (not (any isCex res) && any isUnknown res) + , testAbstractArith "mul-uint256-monotone-not-unsound" $ do + -- Same lemma shape as the uint128-bounded proof, but with full-width + -- uint256 inputs. The 128-bit no-overflow guard must not be assumed from + -- the type alone, so this can only be Unknown under abstract mul: never a + -- bogus QED and never a trusted counterexample from the uninterpreted UF. + Just c <- solcRuntime "C" [i| + contract C { + function prove_mul_uint256_monotone(uint256 a1, uint256 a2, uint256 k) external pure { + require(a1 <= a2); + uint256 p1; uint256 p2; + assembly { p1 := mul(a1, k) p2 := mul(a2, k) } + assert(p1 <= p2); + } + } |] + (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertBoolM "uint256 abstract mul must be Unknown, never QED or Cex" + (not (null res) && all isUnknown res) + , testAbstractArith "roundtrip-no-inflation" $ do + -- The cross-divisor round-trip convertToAssetValue(convertToShares(x)), + -- i.e. ((x*ts)/ta)*ta/ts <= x, is the stateless core of inflation-attack + -- safety: converting a value to shares and back never yields more than + -- you started with. It needs two nested divisions to be related, which + -- the cancellation synthesis (the synthetic (x*ts)/ts term plus div + -- monotonicity) discharges. SOUND: shares*ta <= x*ts (div-mul-link), so + -- floor(shares*ta/ts) <= floor(x*ts/ts) = x. + Just c <- solcRuntime "C" [i| + contract C { + uint256 public totalAssets; + uint256 public totalShares; + function prove_roundtrip(uint256 assets) external view { + require(totalAssets != 0 && totalShares != 0); + require(assets < (1<<128) && totalShares < (1<<128) && totalAssets < (1<<128)); + uint256 ts = totalShares; uint256 ta = totalAssets; + uint256 shares; uint256 outv; + assembly { shares := div(mul(assets, ts), ta) outv := div(mul(shares, ta), ts) } + assert(outv <= assets); + } + } |] + (_, res) <- withBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertEqualM "Must be QED" [] res + , testAbstractArith "div-cex-preserved" $ do + -- No symbolic*symbolic mul => div is exact => a real counterexample is + -- still reported (the Cex->Unknown downgrade must be precise). + Just c <- solcRuntime "C" [i| + contract C { + function prove_div_cex(uint256 a, uint256 b) external pure { + require(b != 0); + uint256 q; assembly { q := div(a, b) } + assert(q != 0); + } + } |] + (_, res) <- withBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertBoolM "Expected counterexample" (any isCex res) + , testAbstractArith "constmul-cex-preserved" $ do + -- Multiplication by a constant is NOT abstracted, so a real + -- counterexample is still reported. + Just c <- solcRuntime "C" [i| + contract C { + function prove_constmul_cex(uint256 x) external pure { + require(x < (1<<128)); + uint256 p; assembly { p := mul(x, 3) } + assert(p != 6); + } + } |] + (_, res) <- withBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertBoolM "Expected counterexample" (any isCex res) + , testAbstractArith "div-divisor-monotone" $ do + -- a bigger divisor yields a smaller-or-equal quotient (div anti-monotonicity) + Just c <- solcRuntime "C" [i| + contract C { + function prove_divisor_monotone(uint256 amt, uint256 p1, uint256 p2) external pure { + require(p1 != 0 && p2 != 0); + require(p1 <= p2); + uint256 q1; uint256 q2; + assembly { q1 := div(amt, p1) q2 := div(amt, p2) } + assert(q2 <= q1); + } + } |] + (_, res) <- withBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertEqualM "Must be QED" [] res + , testAbstractArith "muldiv-fee-cap" $ do + -- a fee of feeBps/10000 never exceeds the principal (mulDiv bound) + Just c <- solcRuntime "C" [i| + contract C { + function prove_fee_le(uint256 amount, uint256 feeBps) external pure { + require(amount < (1<<128) && feeBps <= 10000); + uint256 fee; assembly { fee := div(mul(amount, feeBps), 10000) } + assert(fee <= amount); + } + } |] + (_, res) <- withBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertEqualM "Must be QED" [] res + , testAbstractArith "muldiv-fee-uncapped-not-unsound" $ do + -- SOUNDNESS: without the feeBps <= 100% bound the property is false; the + -- mulDiv guard must not fire, so this must NOT be proved. + Just c <- solcRuntime "C" [i| + contract C { + function prove_fee_uncapped(uint256 amount, uint256 feeBps) external pure { + require(amount < (1<<128)); + uint256 fee; assembly { fee := div(mul(amount, feeBps), 10000) } + assert(fee <= amount); + } + } |] + (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertBoolM "Must be Unknown, never QED" (not (any isCex res) && any isUnknown res) + , testAbstractArith "constmul-div-monotone" $ do + -- (v * 1e27) / rate is monotonic in v. The dividend is a multiplication + -- by a large literal (1e27), which stays a native bvmul; const-mul + -- monotonicity lets the solver order the two dividends without + -- bit-blasting that multiply, which is otherwise the bottleneck. + Just c <- solcRuntime "C" [i| + contract C { + function prove_constmul_div_monotone(uint256 v1, uint256 v2, uint256 rate) external pure { + require(rate != 0); + require(v1 <= v2 && v2 < (1<<80)); + uint256 a1; uint256 a2; + assembly { + a1 := div(mul(v1, 1000000000000000000000000000), rate) + a2 := div(mul(v2, 1000000000000000000000000000), rate) + } + assert(a1 <= a2); + } + } |] + (_, res) <- withBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertEqualM "Must be QED" [] res + , testAbstractArith "const-cancel" $ do + -- (x * c) / c == x for a literal c (const-cancellation lemma). The + -- multiply by c stays a native bvmul but the divide is abstracted + -- (uninterpreted), so without the lemma this identity is not provable. + -- This is what discharges precision-scaling wrappers like + -- `amount * 1e18 / 1e18` that otherwise block round-trip properties. + Just c <- solcRuntime "C" [i| + contract C { + function prove_const_cancel(uint256 x) external pure { + require(x < (1<<128)); + uint256 y; assembly { y := div(mul(x, 1000000000000000000), 1000000000000000000) } + assert(y == x); + } + } |] + (_, res) <- withBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertEqualM "Must be QED" [] res + , testAbstractArith "const-cancel-scaled" $ do + -- generalized const-cancel: (c1*x)/c2 == (c1/c2)*x when c2 | c1. + -- (x*1e18)/1e6 == x*1e12 — discharges lossless precision scaling between + -- different decimals (e.g. _getUsdcValue). + Just c <- solcRuntime "C" [i| + contract C { + function prove_const_cancel_scaled(uint256 x) external pure { + require(x < (1<<80)); + uint256 y; uint256 z; + assembly { y := div(mul(x, 1000000000000000000), 1000000) z := mul(x, 1000000000000) } + assert(y == z); + } + } |] + (_, res) <- withBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertEqualM "Must be QED" [] res + , testAbstractArith "nested-div-collapse" $ do + -- (A/c1)/c2 == A/(c1*c2) for literals c1,c2 (floor identity). With A a + -- symbolic product the divisions are abstracted, so the lemma is what + -- collapses chained constant divisions like x*rate/1e9/1e18 to x*rate/1e27. + Just c <- solcRuntime "C" [i| + contract C { + function prove_nested_div_collapse(uint256 a, uint256 b) external pure { + uint256 lhs; uint256 rhs; + assembly { let p := mul(a, b) + lhs := div(div(p, 1000000000), 1000000000000000000) + rhs := div(p, 1000000000000000000000000000) } + assert(lhs == rhs); + } + } |] + (_, res) <- withBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertEqualM "Must be QED" [] res + , testAbstractArith "fraction-reduce" $ do + -- fraction-reduce: (c1*x)/c2 == x/(c2/c1) when c1 | c2 (mirror of + -- const-cancel, which needs c2 | c1). (x*1e6)/1e18 == x/1e12 — discharges + -- the precision step that scales DOWN to fewer decimals (convert-to-usdc). + Just c <- solcRuntime "C" [i| + contract C { + function prove_fraction_reduce(uint256 x) external pure { + require(x < (1<<128)); + uint256 y; uint256 z; + assembly { y := div(mul(x, 1000000), 1000000000000000000) z := div(x, 1000000000000) } + assert(y == z); + } + } |] + (_, res) <- withBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertEqualM "Must be QED" [] res + , testAbstractArith "fraction-reduce-cex" $ do + -- soundness guard: the fraction-reduce lemma must not over-prove. A wrong + -- closed form ((x*1e6)/1e18 == x/1e12 + 1) is false for every x, so it + -- must NOT come back QED (the lemma pins the LHS to x/1e12, exposing the + -- off-by-one as a real counterexample rather than a spurious proof). + Just c <- solcRuntime "C" [i| + contract C { + function prove_fraction_reduce_wrong(uint256 x) external pure { + require(x < (1<<128)); + uint256 y; uint256 z; + assembly { y := div(mul(x, 1000000), 1000000000000000000) z := add(div(x, 1000000000000), 1) } + assert(y == z); + } + } |] + (_, res) <- withBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertBoolM "Wrong closed form must not be QED" (not (null res)) + , testAbstractArith "ceildiv-cancel" $ do + -- ceilDiv-cancel: Math.ceilDiv(c1*x, c2) == (c1/c2)*x when c2 | c1 (the + -- product is always divisible, so round-up equals round-down). The divide is + -- abstracted over the (c1*x - 1) dividend, so the lemma pins it. Discharges + -- the round-up multiply-up in previewSwapExactOut (e.g. usds->usdc == x*1e12). + Just c <- solcRuntime "C" [i| + contract C { + function ceilDiv(uint256 a, uint256 b) internal pure returns (uint256) { + return a == 0 ? 0 : (a - 1) / b + 1; + } + function prove_ceildiv_cancel(uint256 x) external pure { + require(x < (1<<128)); + uint256 y = ceilDiv(x * 1000000000000000000, 1000000); + uint256 z; unchecked { z = x * 1000000000000; } + assert(y == z); + } + } |] + (_, res) <- withBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertEqualM "Must be QED" [] res + , testAbstractArith "ceildiv-cancel-cex" $ do + -- soundness guard: a wrong closed form (off by one) must NOT be QED. + Just c <- solcRuntime "C" [i| + contract C { + function ceilDiv(uint256 a, uint256 b) internal pure returns (uint256) { + return a == 0 ? 0 : (a - 1) / b + 1; + } + function prove_ceildiv_cancel_wrong(uint256 x) external pure { + require(x < (1<<128)); + uint256 y = ceilDiv(x * 1000000000000000000, 1000000); + uint256 z; unchecked { z = x * 1000000000000 + 1; } + assert(y == z); + } + } |] + (_, res) <- withBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertBoolM "Wrong closed form must not be QED" (not (null res)) + , testAbstractArith "scaled-product-telescope" $ do + -- scaled-product telescoping: a*b/c - a*(b-k)/c == a*(k/c) when c | k (here + -- c == k == 1e27, so the coefficient is a). This is the ONLY lemma that + -- relates two DISTINCT abstract products (a*b and a*(b-1e27), both + -- symbolic*symbolic), so it discharges value-change accounting identities + -- like s*rate/1e27 - s == s*(rate-1e27)/1e27 (the third assertion of an + -- ERC4626 conversionRate test). + Just c <- solcRuntime "C" [i| + contract C { + function prove_telescope(uint256 s, uint256 q) external pure { + require(s <= 1000000000000000000000000000000); // 1e30 + require(q >= 1000000000000000000000000000); // 1e27 + require(q <= 1000000000000000000000000000000); // 1e30 + assert(s * q / 1000000000000000000000000000 - s + == s * (q - 1000000000000000000000000000) / 1000000000000000000000000000); + } + } |] + (_, res) <- withBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertEqualM "Must be QED" [] res + , testAbstractArith "scaled-product-telescope-not-unsound" $ do + -- soundness guard: a wrong difference (+1) must stay Unknown, never QED. + -- Both products are abstract, so a violation downgrades SAT->Unknown rather + -- than producing a trusted Cex; the lemma must not over-prove the off-by-one. + Just c <- solcRuntime "C" [i| + contract C { + function prove_telescope_wrong(uint256 s, uint256 q) external pure { + require(s <= 1000000000000000000000000000000); + require(q >= 1000000000000000000000000000); + require(q <= 1000000000000000000000000000000); + assert(s * q / 1000000000000000000000000000 - s + == s * (q - 1000000000000000000000000000) / 1000000000000000000000000000 + 1); + } + } |] + (_, res) <- withBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts + assertBoolM "Wrong difference must be Unknown, never QED" (not (any isCex res) && any isUnknown res) + ] , testGroup "max-iterations" [ test "concrete-loops-reached" $ do Just c <- solcRuntime "C" @@ -3519,7 +4434,7 @@ tests = testGroup "hevm" [ testCase "encodeConcreteStore-overwrite" $ assertEqual "" (pure "(store (store ((as const Storage) #x0000000000000000000000000000000000000000000000000000000000000000) (_ bv1 256) (_ bv2 256)) (_ bv3 256) (_ bv4 256))") - (EVM.SMT.encodeConcreteStore $ Map.fromList [(W256 1, W256 2), (W256 3, W256 4)]) + (EVM.SMT.encodeConcreteStore ConcreteDivMod $ Map.fromList [(W256 1, W256 2), (W256 3, W256 4)]) ] , testGroup "calling-solvers" [ test "no-error-on-large-buf" $ do @@ -3824,4 +4739,3 @@ expectedConcVals nm val = case val of _ -> internalError $ "unsupported Abi type " <> show nm <> " val: " <> show val <> " val type: " <> showAlter val where mkWord = word . encodeAbiValue -