Implement CLZ opcode

This also bumps the Solidity version used in tests to be able to
compile an example with CLZ

Author: elopez

CHANGELOG.md

@@ -9,6 +9,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## Added
 - We support RPC in equivalence checking now
+- New opcode: CLZ
 
 ## Fixed
 - Fix incorrect simplification rule for `PEq (Lit 1) (IsZero (LT a b))`

flake.lock

@@ -4,7 +4,11 @@
   inputs = {
     flake-utils.url = "github:numtide/flake-utils";
     nixpkgs.url = "github:nixos/nixpkgs/nixpkgs-unstable";
-    foundry.url = "github:shazow/foundry.nix/stable";
+    foundry = {
+      url = "github:shazow/foundry.nix/stable";
+      inputs.nixpkgs.follows = "nixpkgs";
+      inputs.flake-utils.follows = "flake-utils";
+    };
     solidity = {
       url = "github:argotorg/solidity/8a97fa7a1db1ec509221ead6fea6802c684ee887";
       flake = false;
@@ -24,6 +28,7 @@
     solc-pkgs = {
       url = "github:hellwolf/solc.nix";
       inputs.nixpkgs.follows = "nixpkgs";
+      inputs.flake-utils.follows = "flake-utils";
     };
   };
 
@@ -35,7 +40,7 @@
           overlays = [solc-pkgs.overlay];
           config = { allowBroken = true; };
         });
-        solc = (solc-pkgs.mkDefault pkgs pkgs.solc_0_8_26);
+        solc = (solc-pkgs.mkDefault pkgs pkgs.solc_0_8_31);
         testDeps = [
           solc
           foundry.defaultPackage.${system}

flake.nix

@@ -425,6 +425,7 @@ exec1 conf = do
         OpShl -> {-# SCC "OpShl" #-} stackOp2 g_verylow Expr.shl
         OpShr -> {-# SCC "OpShr" #-} stackOp2 g_verylow Expr.shr
         OpSar -> {-# SCC "OpSar" #-} stackOp2 g_verylow Expr.sar
+        OpClz -> {-# SCC "OpClz" #-} stackOp1 g_low Expr.clz
 
         -- more accurately referred to as KECCAK
         OpSha3 -> {-# SCC "OpSha3" #-}

src/EVM.hs

@@ -42,6 +42,7 @@ assemble os = V.fromList $ concatMap go os
       OpShl -> [LitByte 0x1B]
       OpShr -> [LitByte 0x1C]
       OpSar -> [LitByte 0x1D]
+      OpClz -> [LitByte 0x1E]
       OpSha3 -> [LitByte 0x20]
       OpAddress -> [LitByte 0x30]
       OpBalance -> [LitByte 0x31]

src/EVM/Assembler.hs

@@ -202,6 +202,9 @@ sar = op2 SAR (\x y ->
      else
        fromIntegral $ shiftR asSigned (fromIntegral x))
 
+clz :: Expr EWord -> Expr EWord
+clz = op1 CLZ (\x -> if x == 0 then 256 else fromIntegral $ countLeadingZeros x)
+
 
 -- Props
 
@@ -1236,6 +1239,9 @@ simplifyNoLitToKeccak e = untilFixpoint (mapExpr go) e
        | a == (Lit 0) = v
        | v == (Lit 0) = v
        | otherwise = sar a v
+    go (CLZ v)
+       | v == (Lit 0) = Lit 256
+       | otherwise = clz v
 
     -- Bitwise AND & OR. These MUST preserve bitwise equivalence
     go (And a b)

src/EVM/Expr.hs

@@ -662,6 +662,7 @@ formatExpr = go
       SHL a b -> fmt "SHL" [a, b]
       SHR a b -> fmt "SHR" [a, b]
       SAR a b -> fmt "SAR" [a, b]
+      CLZ a -> fmt "CLZ" [a]
 
       e@Origin -> T.pack (show e)
       e@Coinbase -> T.pack (show e)

src/EVM/Format.hs

@@ -45,6 +45,7 @@ intToOpName a =
     0x1b -> "SHL"
     0x1c -> "SHR"
     0x1d -> "SAR"
+    0x1e -> "CLZ"
     0x20 -> "SHA3"
     0x30 -> "ADDRESS"
     --
@@ -206,6 +207,7 @@ opString (i, o) = let showPc x | x < 0x10 = '0' : showHex x ""
   OpShl -> "SHL"
   OpShr -> "SHR"
   OpSar -> "SAR"
+  OpClz -> "CLZ"
   OpSha3 -> "SHA3"
   OpAddress -> "ADDRESS"
   OpBalance -> "BALANCE"
@@ -305,6 +307,7 @@ getOp x = case x of
   0x1b -> OpShl
   0x1c -> OpShr
   0x1d -> OpSar
+  0x1e -> OpClz
   0x20 -> OpSha3
   0x30 -> OpAddress
   0x31 -> OpBalance

src/EVM/Op.hs

@@ -478,6 +478,7 @@ exprToSMT = \case
   SHL a b -> op2 "bvshl" b a
   SHR a b -> op2 "bvlshr" b a
   SAR a b -> op2 "bvashr" b a
+  CLZ a -> op1 "clz" a
   SEx a b -> op2 "signext" a b
   Div a b -> op2CheckZero "bvudiv" a b
   SDiv a b -> op2CheckZero "bvsdiv" a b

src/EVM/SMT.hs

@@ -29,7 +29,8 @@ prelude =  SMT2 src mempty mempty
     ]) <> [(SMTComment "slot -> value"), SMTCommand "(define-sort Storage () (Array Word Word))"]
     <> (fmap SMTCommand [
         "(declare-fun keccak (Buf Word) Word)",
-        "(declare-fun sha256 (Buf Word) Word)"
+        "(declare-fun sha256 (Buf Word) Word)",
+        "(declare-fun clz (Word) Word)"
     ])
   macros = fmap SMTCommand [
     "(define-fun max ((a (_ BitVec 256)) (b (_ BitVec 256))) (_ BitVec 256) (ite (bvult a b) b a))",