From 11ef66919514ccec10801a88de13086950ee6f12 Mon Sep 17 00:00:00 2001 From: "Thomas Marchand (agent)" Date: Sun, 11 Oct 2026 18:29:54 +0200 Subject: [PATCH] feat(solidity-import): support ECDSA Yul signature unpacking, StorageSlot raw string/bytes slots, and error scalar casts (slice 40) --- Compiler/SolidityImport/Import.lean | 157 +++++- ...saMerkleCheckpointsStorageSlotSequence.sol | 482 ++++++++++++++++++ ...leCheckpointsStorageSlotSequenceModel.lean | 39 ++ docs/SOLIDITY_IMPORT.md | 9 + lakefile.lean | 1 + .../solidity_differential/check_stateful.py | 56 ++ .../solidity_differential/check_storage.py | 13 +- .../check_storage_mutations.py | 36 +- .../check_storage_rejections.py | 21 + scripts/solidity_differential/programs.py | 33 ++ 10 files changed, 817 insertions(+), 30 deletions(-) create mode 100644 Contracts/SolidityImportSmoke/EcdsaMerkleCheckpointsStorageSlotSequence.sol create mode 100644 Contracts/SolidityImportSmoke/EcdsaMerkleCheckpointsStorageSlotSequenceModel.lean diff --git a/Compiler/SolidityImport/Import.lean b/Compiler/SolidityImport/Import.lean index 6132c0132..1590aea69 100644 --- a/Compiler/SolidityImport/Import.lean +++ b/Compiler/SolidityImport/Import.lean @@ -2614,6 +2614,50 @@ private def yulMemoryStructHash? (ptrNode sizeNode : Json) (lowerYulFn : Json let alloc := (AbiEncoding.staticWords pointer finish words).toArray return some { pre := pre ++ alloc, expr := .keccak256 (.localVar pointer) (.literal byteLen) } +private def yulByteBufferByName? (node : Json) : M (Option EncodedBytes) := do + if (← mKind node) != "YulIdentifier" then return none + let name ← mStr (← mField node "name") + let env ← get + if env.yulNames.contains name then return none + let some declId := env.yulMemoryStructs.find? name | return none + return env.byteBuffers.find? declId <|> env.stringBuffers.find? declId + +private def yulPositiveWordOffsetLiteral? (node : Json) : M (Option Nat) := do + if (← mKind node) != "YulLiteral" then return none + unless optStr node "kind" == some "number" && optStr node "type" == some "" do + return none + let raw ← mStr (← mField node "value") + let some value := Compiler.Hex.parseHexNat? raw <|> raw.toNat? | return none + unless value ≥ 32 && value < 2^256 && value % 32 == 0 do return none + return some value + +private def yulByteBufferLoad? (addrNode : Json) : M (Option Val) := do + if let some buf ← yulByteBufferByName? addrNode then + return some { pre := buf.pre, expr := buf.size } + if (← mKind addrNode) != "YulFunctionCall" then return none + let outerFn ← mStr (← mField (← mField addrNode "functionName") "name") + unless outerFn == "add" do return none + let outerArgs ← mArr (← mField addrNode "arguments") + unless outerArgs.size == 2 do return none + let matched? ← do + if let some off ← yulPositiveWordOffsetLiteral? outerArgs[1]! then + if let some buf ← yulByteBufferByName? outerArgs[0]! then + pure (some (buf, off)) + else + pure none + else if let some off ← yulPositiveWordOffsetLiteral? outerArgs[0]! then + if let some buf ← yulByteBufferByName? outerArgs[1]! then + pure (some (buf, off)) + else + pure none + else + pure none + let some (buf, off) := matched? | return none + return some { + pre := buf.pre, + expr := .mload (.add buf.pointer (.literal (off - 32))) + } + private partial def lowerYul (j : Json) : M Val := do match ← mKind j with | "YulLiteral" => @@ -2645,6 +2689,8 @@ private partial def lowerYul (j : Json) : M Val := do if args.size == 1 then if let some v ← yulMemoryArrayElementLoad? args[0]! lowerYul then return v + if let some v ← yulByteBufferLoad? args[0]! then + return v failAt j "unsupported Yul builtin mload" let expectedArity? : Option Nat := match fname with | "caller" | "address" | "timestamp" | "number" | "chainid" @@ -2778,6 +2824,26 @@ private def isFullWordYulScalar : ParamType → Bool | .uint256 | .int256 | .bytes32 => true | _ => false +private def isProvablyBoundedYulExpr (scalarType : ParamType) (expr : Expr) : Bool := + let bits? : Option Nat := match scalarType with + | .bool => some 1 + | .uint8 => some 8 + | .uint16 => some 16 + | .uintN bits => some bits + | .address => some 160 + | _ => none + match bits? with + | none => false + | some bits => + match expr with + | .literal n => n < 2 ^ bits + | .byte _ _ => bits ≥ 8 + | .lt _ _ | .gt _ _ | .slt _ _ | .sgt _ _ | .eq _ _ | .logicalNot _ => bits ≥ 1 + | .bitAnd (.literal mask) _ | .bitAnd _ (.literal mask) => mask < 2 ^ bits + | .shr (.literal shift) _ => shift ≥ 256 - bits + | .mod _ (.literal m) => 0 < m && m ≤ 2 ^ bits + | _ => false + private def cleanHelperResultExpr (ty : String) (v : Val) : Expr := if ty == "bool" then Expr.logicalNot (.logicalNot v.expr) else if ty == "bytes4" then Expr.bitAnd v.expr (.literal ((2 ^ 32 - 1) * 16 ^ 56)) @@ -2853,6 +2919,8 @@ private def lowerYulDirectAssignmentTarget (j stmt varNode : Json) (refs : Array else failAt stmt s!"Yul assignment target {vname} is shadowed" let some scalarType := env.scalarTy.find? targetId | failAt stmt s!"unknown scalar type for Yul assignment target {vname}" + if isProvablyBoundedYulExpr scalarType rhsVal.expr then + return .assignVar binding rhsVal.expr unless isFullWordYulScalar scalarType do failAt stmt s!"Yul assignment to narrow local {vname} is unsupported" return .assignVar binding rhsVal.expr @@ -6880,6 +6948,7 @@ private partial def bindHelperParams (params : Array Json) (args : Array CallArg { pre := #[], pointer := .localVar ptrBinding, size := .localVar sizeBinding } modify fun e => { e with byteBuffers := e.byteBuffers.insert pid retained, + yulMemoryStructs := if pname == "" then e.yulMemoryStructs else e.yulMemoryStructs.insert pname pid, nonLiteralByteLocals := if e.nonLiteralByteLocals.contains pid then e.nonLiteralByteLocals else e.nonLiteralByteLocals.push pid } if pname != "" then yul := yul.erase pname @@ -6893,6 +6962,7 @@ private partial def bindHelperParams (params : Array Json) (args : Array CallArg { pre := #[], pointer := .localVar ptrBinding, size := .localVar sizeBinding } modify fun e => { e with byteBuffers := e.byteBuffers.insert pid retained, + yulMemoryStructs := if pname == "" then e.yulMemoryStructs else e.yulMemoryStructs.insert pname pid, nonLiteralByteLocals := if e.nonLiteralByteLocals.contains pid then e.nonLiteralByteLocals else e.nonLiteralByteLocals.push pid } else unless pty == "string" && location == "memory" do @@ -6904,6 +6974,7 @@ private partial def bindHelperParams (params : Array Json) (args : Array CallArg { pre := #[], pointer := .localVar ptrBinding, size := .localVar sizeBinding } modify fun e => { e with stringBuffers := e.stringBuffers.insert pid retained, + yulMemoryStructs := if pname == "" then e.yulMemoryStructs else e.yulMemoryStructs.insert pname pid, nonLiteralByteLocals := if e.nonLiteralByteLocals.contains pid then e.nonLiteralByteLocals else e.nonLiteralByteLocals.push pid } if pname != "" then yul := yul.erase pname @@ -6934,10 +7005,12 @@ private partial def bindHelperParams (params : Array Json) (args : Array CallArg if descriptor.isString then modify fun e => { e with stringBuffers := e.stringBuffers.insert pid retained, + yulMemoryStructs := if pname == "" then e.yulMemoryStructs else e.yulMemoryStructs.insert pname pid, nonLiteralByteLocals := if e.nonLiteralByteLocals.contains pid then e.nonLiteralByteLocals else e.nonLiteralByteLocals.push pid } else modify fun e => { e with byteBuffers := e.byteBuffers.insert pid retained, + yulMemoryStructs := if pname == "" then e.yulMemoryStructs else e.yulMemoryStructs.insert pname pid, nonLiteralByteLocals := if e.nonLiteralByteLocals.contains pid then e.nonLiteralByteLocals else e.nonLiteralByteLocals.push pid } else failAt p s!"unsupported {pty} helper parameter location {location}" @@ -7065,10 +7138,12 @@ private partial def bindHelperParams (params : Array Json) (args : Array CallArg if isString then modify fun e => { e with stringBuffers := e.stringBuffers.insert pid retained, + yulMemoryStructs := if pname == "" then e.yulMemoryStructs else e.yulMemoryStructs.insert pname pid, nonLiteralByteLocals := if e.nonLiteralByteLocals.contains pid then e.nonLiteralByteLocals else e.nonLiteralByteLocals.push pid } else modify fun e => { e with byteBuffers := e.byteBuffers.insert pid retained, + yulMemoryStructs := if pname == "" then e.yulMemoryStructs else e.yulMemoryStructs.insert pname pid, nonLiteralByteLocals := if e.nonLiteralByteLocals.contains pid then e.nonLiteralByteLocals else e.nonLiteralByteLocals.push pid } if pname != "" then yul := yul.erase pname @@ -7813,19 +7888,39 @@ private partial def inlineStorageRefFn (fnId : Nat) (args : Array CallArg) (at_ let prefixPre ← lowerYulStmtSlice s prefixYstmts refs "" let slotVal ← lowerYul rhs modify fun e => { e with yulNames := savedAsmYul, yulScratch0 := savedScratch0, yulScratch32 := savedScratch32 } - let rawInfo ← resolveRawStructInfo retStructId fn - if !prefixYstmts.isEmpty then - unless prefixYstmts.size == 1 do - failAt s "storage pointer helper assembly must be a single slot assignment" - unless rawInfo.wordCount == 1 do - failAt s "Checkpoints._unsafeAccess requires a 1-slot struct element array" - let slotBinding ← freshFor "raw_slot" - pre := pre ++ extPre ++ prefixPre ++ slotVal.pre |>.push (.letVar slotBinding slotVal.expr) - let rpath := SPath.rawSlot retStructId (.localVar slotBinding) - if idx + 1 == stmts.size then - retPath? := some rpath + let sMembers ← mArr (← mField retStructDecl "members") + let rawBytesString? ← if prefixYstmts.isEmpty && sMembers.size == 1 then do + let m0 := sMembers[0]! + let m0Name ← mStr (← mField m0 "name") + let m0Ty ← mType m0 + if m0Name == "value" && (m0Ty == "string" || m0Ty == "bytes") then + pure (some (m0Ty == "string")) + else + pure none + else + pure none + if let some isString := rawBytesString? then + let slotBinding ← freshFor "raw_slot" + pre := pre ++ extPre ++ prefixPre ++ slotVal.pre |>.push (.letVar slotBinding slotVal.expr) + let bpath := SPath.bytesSlot ("", .localVar slotBinding) isString + if idx + 1 == stmts.size then + retPath? := some bpath + else + modify fun e => { e with paths := e.paths.insert retId bpath } else - modify fun e => { e with paths := e.paths.insert retId rpath } + let rawInfo ← resolveRawStructInfo retStructId fn + if !prefixYstmts.isEmpty then + unless prefixYstmts.size == 1 do + failAt s "storage pointer helper assembly must be a single slot assignment" + unless rawInfo.wordCount == 1 do + failAt s "Checkpoints._unsafeAccess requires a 1-slot struct element array" + let slotBinding ← freshFor "raw_slot" + pre := pre ++ extPre ++ prefixPre ++ slotVal.pre |>.push (.letVar slotBinding slotVal.expr) + let rpath := SPath.rawSlot retStructId (.localVar slotBinding) + if idx + 1 == stmts.size then + retPath? := some rpath + else + modify fun e => { e with paths := e.paths.insert retId rpath } | _ => failAt s "unsupported statement in storage pointer helper" let some finalPath := retPath? | failAt fn "storage pointer helper did not assign or return a storage slot" @@ -11365,7 +11460,16 @@ private partial def lowerErrorArguments (call : Json) : M (Array Stmt × String if ← isThisAddressConv argument then pure true else - pure false + let convArgs ← mArr (← mField argument "arguments") + if convArgs.size == 1 then + let inner ← stripParens convArgs[0]! + if (← mKind inner) == "Identifier" then + let innerId ← refInt inner + pure (innerId ≥ 0 && (← get).values.contains innerId.toNat) + else + pure false + else + pure false else if optStr argument "kind" == some "functionCall" then if (← mArr (← mField argument "arguments")).isEmpty then pure true @@ -11521,14 +11625,14 @@ private partial def lowerLocal (s : Json) : M (Array Stmt) := do nonLiteralByteLocals := if e.nonLiteralByteLocals.contains id then e.nonLiteralByteLocals else e.nonLiteralByteLocals.push id, yulNames := e.yulNames.erase name, yulMemoryArrays := e.yulMemoryArrays.erase name, - yulMemoryStructs := e.yulMemoryStructs.erase name } + yulMemoryStructs := e.yulMemoryStructs.insert name id } else modify fun e => { e with byteBuffers := e.byteBuffers.insert id retained, nonLiteralByteLocals := if e.nonLiteralByteLocals.contains id then e.nonLiteralByteLocals else e.nonLiteralByteLocals.push id, yulNames := e.yulNames.erase name, yulMemoryArrays := e.yulMemoryArrays.erase name, - yulMemoryStructs := e.yulMemoryStructs.erase name } + yulMemoryStructs := e.yulMemoryStructs.insert name id } return out let mut expectedTypes : Array (Option String) := #[] for d in decls do @@ -11604,7 +11708,8 @@ private partial def lowerLocal (s : Json) : M (Array Stmt) := do { e with byteBuffers := e.byteBuffers.insert id retained, nonLiteralByteLocals := if e.nonLiteralByteLocals.contains id then e.nonLiteralByteLocals else e.nonLiteralByteLocals.push id, encodingMemory := true, - yulNames := e.yulNames.erase name } + yulNames := e.yulNames.erase name, + yulMemoryStructs := e.yulMemoryStructs.insert name id } return effects unless loc == "default" do failAt d "uninitialized reference locals are outside this slice" @@ -11695,7 +11800,8 @@ private partial def lowerLocal (s : Json) : M (Array Stmt) := do modify fun e => { e with stringBuffers := e.stringBuffers.insert id retained, nonLiteralByteLocals := if isNonLiteralInit && !e.nonLiteralByteLocals.contains id then e.nonLiteralByteLocals.push id else e.nonLiteralByteLocals, - yulNames := e.yulNames.erase name } + yulNames := e.yulNames.erase name, + yulMemoryStructs := e.yulMemoryStructs.insert name id } return effects let effects := buffer.pre ++ #[.letVar pointer buffer.pointer, .letVar size buffer.size] let retained : EncodedBytes := @@ -11703,7 +11809,8 @@ private partial def lowerLocal (s : Json) : M (Array Stmt) := do modify fun e => { e with byteBuffers := e.byteBuffers.insert id retained, nonLiteralByteLocals := if isNonLiteralInit && !e.nonLiteralByteLocals.contains id then e.nonLiteralByteLocals.push id else e.nonLiteralByteLocals, - yulNames := e.yulNames.erase name } + yulNames := e.yulNames.erase name, + yulMemoryStructs := e.yulMemoryStructs.insert name id } return effects if loc == "memory" && (← mType d).contains "[]" then let some (elemStr, elemPty, abiKind) := scalarArrayElement? (← mType d) @@ -12289,7 +12396,12 @@ private def bindRoot (fn : Json) : M (Array SrcParam) := do { pre := #[], pointer := .add (.localVar memoryPointer) (.literal 32), size := .localVar lengthBinding } else e.byteBuffers - { e with calldataBytes := e.calldataBytes.insert id bound, byteBuffers } + let yulMemoryStructs := + if loc == "memory" && rawName != "" then + e.yulMemoryStructs.insert rawName id + else + e.yulMemoryStructs + { e with calldataBytes := e.calldataBytes.insert id bound, byteBuffers, yulMemoryStructs } else if ty == "string" then unless loc == "calldata" || loc == "memory" do failAt p s!"unsupported location {loc} for string" @@ -12320,7 +12432,12 @@ private def bindRoot (fn : Json) : M (Array SrcParam) := do { pre := #[], pointer := .add (.localVar memoryPointer) (.literal 32), size := .localVar lengthBinding } else e.stringBuffers - { e with calldataBytes := e.calldataBytes.insert id bound, stringBuffers } + let yulMemoryStructs := + if loc == "memory" && rawName != "" then + e.yulMemoryStructs.insert rawName id + else + e.yulMemoryStructs + { e with calldataBytes := e.calldataBytes.insert id bound, stringBuffers, yulMemoryStructs } else if let some (elemStr, elemPty, abiKind) := scalarArrayElement? ty then unless loc == "calldata" || loc == "memory" do failAt p s!"unsupported location {loc} for {ty}" diff --git a/Contracts/SolidityImportSmoke/EcdsaMerkleCheckpointsStorageSlotSequence.sol b/Contracts/SolidityImportSmoke/EcdsaMerkleCheckpointsStorageSlotSequence.sol new file mode 100644 index 000000000..139eb5380 --- /dev/null +++ b/Contracts/SolidityImportSmoke/EcdsaMerkleCheckpointsStorageSlotSequence.sol @@ -0,0 +1,482 @@ +// SPDX-License-Identifier: MIT +pragma solidity 0.8.34; + +library MathSlice40 { + function average(uint256 a, uint256 b) internal pure returns (uint256) { + return (a & b) + (a ^ b) / 2; + } + + function sqrt(uint256 a) internal pure returns (uint256) { + unchecked { + if (a <= 1) { + return a; + } + uint256 aa = a; + uint256 xn = 1; + if (aa >= (1 << 128)) { + aa >>= 128; + xn <<= 64; + } + if (aa >= (1 << 64)) { + aa >>= 64; + xn <<= 32; + } + if (aa >= (1 << 32)) { + aa >>= 32; + xn <<= 16; + } + if (aa >= (1 << 16)) { + aa >>= 16; + xn <<= 8; + } + if (aa >= (1 << 8)) { + aa >>= 8; + xn <<= 4; + } + if (aa >= (1 << 4)) { + aa >>= 4; + xn <<= 2; + } + if (aa >= (1 << 2)) { + xn <<= 1; + } + xn = (3 * xn) >> 1; + xn = (xn + a / xn) >> 1; + xn = (xn + a / xn) >> 1; + xn = (xn + a / xn) >> 1; + xn = (xn + a / xn) >> 1; + xn = (xn + a / xn) >> 1; + xn = (xn + a / xn) >> 1; + return xn - (xn > a / xn ? 1 : 0); + } + } +} + +library StorageSlotSlice40 { + struct AddressSlot { + address value; + } + + struct BooleanSlot { + bool value; + } + + struct Bytes32Slot { + bytes32 value; + } + + struct Uint256Slot { + uint256 value; + } + + struct StringSlot { + string value; + } + + struct BytesSlot { + bytes value; + } + + function getAddressSlot(bytes32 slot) internal pure returns (AddressSlot storage r) { + assembly ("memory-safe") { + r.slot := slot + } + } + + function getBooleanSlot(bytes32 slot) internal pure returns (BooleanSlot storage r) { + assembly ("memory-safe") { + r.slot := slot + } + } + + function getBytes32Slot(bytes32 slot) internal pure returns (Bytes32Slot storage r) { + assembly ("memory-safe") { + r.slot := slot + } + } + + function getUint256Slot(bytes32 slot) internal pure returns (Uint256Slot storage r) { + assembly ("memory-safe") { + r.slot := slot + } + } + + function getStringSlot(bytes32 slot) internal pure returns (StringSlot storage r) { + assembly ("memory-safe") { + r.slot := slot + } + } + + function getStringSlot(string storage store) internal pure returns (StringSlot storage r) { + assembly ("memory-safe") { + r.slot := store.slot + } + } + + function getBytesSlot(bytes32 slot) internal pure returns (BytesSlot storage r) { + assembly ("memory-safe") { + r.slot := slot + } + } + + function getBytesSlot(bytes storage store) internal pure returns (BytesSlot storage r) { + assembly ("memory-safe") { + r.slot := store.slot + } + } +} + +library ECDSASlice40 { + enum RecoverError { + NoError, + InvalidSignature, + InvalidSignatureLength, + InvalidSignatureS + } + + error ECDSAInvalidSignature(); + error ECDSAInvalidSignatureLength(uint256 length); + error ECDSAInvalidSignatureS(bytes32 s); + + function tryRecover(bytes32 hash, bytes memory signature) internal pure returns (address, RecoverError, bytes32) { + uint256 sigLen; + assembly ("memory-safe") { + sigLen := mload(signature) + } + if (sigLen == 65) { + bytes32 r; + bytes32 s; + uint8 v; + assembly ("memory-safe") { + r := mload(add(signature, 0x20)) + s := mload(add(signature, 0x40)) + v := byte(0, mload(add(signature, 0x60))) + } + return tryRecover(hash, v, r, s); + } else { + return (address(0), RecoverError.InvalidSignatureLength, bytes32(sigLen)); + } + } + + function recover(bytes32 hash, bytes memory signature) internal pure returns (address) { + (address recovered, RecoverError error, bytes32 errorArg) = tryRecover(hash, signature); + _throwError(error, errorArg); + return recovered; + } + + function tryRecover(bytes32 hash, bytes32 r, bytes32 vs) internal pure returns (address, RecoverError, bytes32) { + unchecked { + bytes32 s = vs & bytes32(0x7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff); + uint8 v = uint8((uint256(vs) >> 255) + 27); + return tryRecover(hash, v, r, s); + } + } + + function recover(bytes32 hash, bytes32 r, bytes32 vs) internal pure returns (address) { + (address recovered, RecoverError error, bytes32 errorArg) = tryRecover(hash, r, vs); + _throwError(error, errorArg); + return recovered; + } + + function tryRecover( + bytes32 hash, + uint8 v, + bytes32 r, + bytes32 s + ) internal pure returns (address, RecoverError, bytes32) { + if (uint256(s) > 0x7FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF5D576E7357A4501DDFE92F46681B20A0) { + return (address(0), RecoverError.InvalidSignatureS, s); + } + if ((v != 27 && v != 28) || r == bytes32(0) || s == bytes32(0)) { + return (address(0), RecoverError.InvalidSignature, bytes32(0)); + } + address signer = address(uint160(uint256(keccak256(abi.encode(hash, v, r, s))))); + if (signer == address(0)) { + return (address(0), RecoverError.InvalidSignature, bytes32(0)); + } + return (signer, RecoverError.NoError, bytes32(0)); + } + + function recover(bytes32 hash, uint8 v, bytes32 r, bytes32 s) internal pure returns (address) { + (address recovered, RecoverError error, bytes32 errorArg) = tryRecover(hash, v, r, s); + _throwError(error, errorArg); + return recovered; + } + + function _throwError(RecoverError error, bytes32 errorArg) private pure { + if (error == RecoverError.NoError) { + return; + } else if (error == RecoverError.InvalidSignature) { + revert ECDSAInvalidSignature(); + } else if (error == RecoverError.InvalidSignatureLength) { + revert ECDSAInvalidSignatureLength(uint256(errorArg)); + } else if (error == RecoverError.InvalidSignatureS) { + revert ECDSAInvalidSignatureS(errorArg); + } + } +} + +library MerkleProofSlice40 { + function verify(bytes32[] memory proof, bytes32 root, bytes32 leaf) internal pure returns (bool) { + return processProof(proof, leaf) == root; + } + + function processProof(bytes32[] memory proof, bytes32 leaf) internal pure returns (bytes32) { + bytes32 computedHash = leaf; + for (uint256 i = 0; i < proof.length; i++) { + computedHash = _hashPair(computedHash, proof[i]); + } + return computedHash; + } + + function _hashPair(bytes32 a, bytes32 b) private pure returns (bytes32 value) { + if (a < b) { + assembly ("memory-safe") { + mstore(0x00, a) + mstore(0x20, b) + value := keccak256(0x00, 0x40) + } + } else { + assembly ("memory-safe") { + mstore(0x00, b) + mstore(0x20, a) + value := keccak256(0x00, 0x40) + } + } + } +} + +library CheckpointsSlice40 { + struct Trace224 { + Checkpoint224[] _checkpoints; + } + + struct Checkpoint224 { + uint32 _key; + uint224 _value; + } + + error CheckpointUnorderedInsertion(); + + function push(Trace224 storage self, uint32 key, uint224 value) internal returns (uint224, uint224) { + return _insert(self._checkpoints, key, value); + } + + function lowerLookup(Trace224 storage self, uint32 key) internal view returns (uint224) { + uint256 len = self._checkpoints.length; + uint256 pos = _lowerBinaryLookup(self._checkpoints, key, 0, len); + return pos == len ? 0 : _unsafeAccess(self._checkpoints, pos)._value; + } + + function upperLookupRecent(Trace224 storage self, uint32 key) internal view returns (uint224) { + uint256 len = self._checkpoints.length; + uint256 low = 0; + uint256 high = len; + if (len > 5) { + uint256 mid = len - MathSlice40.sqrt(len); + if (key < _unsafeAccess(self._checkpoints, mid)._key) { + high = mid; + } else { + low = mid + 1; + } + } + uint256 pos = _upperBinaryLookup(self._checkpoints, key, low, high); + return pos == 0 ? 0 : _unsafeAccess(self._checkpoints, pos - 1)._value; + } + + function latest(Trace224 storage self) internal view returns (uint224) { + uint256 pos = self._checkpoints.length; + return pos == 0 ? 0 : _unsafeAccess(self._checkpoints, pos - 1)._value; + } + + function length(Trace224 storage self) internal view returns (uint256) { + return self._checkpoints.length; + } + + function _insert( + Checkpoint224[] storage self, + uint32 key, + uint224 value + ) private returns (uint224, uint224) { + uint256 pos = self.length; + if (pos > 0) { + Checkpoint224 memory last = _unsafeAccess(self, pos - 1); + if (last._key > key) { + revert CheckpointUnorderedInsertion(); + } + if (last._key == key) { + _unsafeAccess(self, pos - 1)._value = value; + return (last._value, value); + } + } + self.push(Checkpoint224({ _key: key, _value: value })); + return (pos == 0 ? 0 : _unsafeAccess(self, pos - 1)._value, value); + } + + function _upperBinaryLookup( + Checkpoint224[] storage self, + uint32 key, + uint256 low, + uint256 high + ) private view returns (uint256) { + while (low < high) { + uint256 mid = MathSlice40.average(low, high); + if (_unsafeAccess(self, mid)._key > key) { + high = mid; + } else { + low = mid + 1; + } + } + return high; + } + + function _lowerBinaryLookup( + Checkpoint224[] storage self, + uint32 key, + uint256 low, + uint256 high + ) private view returns (uint256) { + while (low < high) { + uint256 mid = MathSlice40.average(low, high); + if (_unsafeAccess(self, mid)._key < key) { + low = mid + 1; + } else { + high = mid; + } + } + return high; + } + + function _unsafeAccess( + Checkpoint224[] storage self, + uint256 pos + ) private pure returns (Checkpoint224 storage result) { + assembly ("memory-safe") { + mstore(0, self.slot) + result.slot := add(keccak256(0, 0x20), pos) + } + } +} + +contract SequenceFixture { + using StorageSlotSlice40 for bytes32; + using CheckpointsSlice40 for CheckpointsSlice40.Trace224; + + bytes32 private constant RAW_LABEL_SLOT = + 0x360894a13ba1a3210667c828492db98dca3e2076cc3735a920a3ca505d382bbc; + bytes32 private constant RAW_PAYLOAD_SLOT = + 0xb53127684a568b3173ae13b9f8a6016e243e63b6e8ee1178d6a717850b5d6103; + + event SignatureCheckpointRecorded( + address indexed signer, + uint256 indexed key, + uint256 value, + bytes32 merkleLeaf, + uint256 payloadLen + ); + + CheckpointsSlice40.Trace224 private _trace; + string private _fallbackLabel; + uint256 private _totalWeight; + bytes32 private _lastRecoveredHash; + + function recoverFromBytes(bytes32 hash, bytes memory signature) public pure returns (address) { + return ECDSASlice40.recover(hash, signature); + } + + function recoverFromCompact(bytes32 hash, bytes32 r, bytes32 vs) public pure returns (address) { + return ECDSASlice40.recover(hash, r, vs); + } + + function verifyMerkle(bytes32[] memory proof, bytes32 root, bytes32 leaf) public pure returns (bool) { + return MerkleProofSlice40.verify(proof, root, leaf); + } + + function rawSlotLabel() public view returns (string memory) { + return RAW_LABEL_SLOT.getStringSlot().value; + } + + function rawSlotPayload() public view returns (bytes memory) { + return RAW_PAYLOAD_SLOT.getBytesSlot().value; + } + + function checkpointUpperRecent(uint32 key) public view returns (uint224) { + return _trace.upperLookupRecent(key); + } + + function change(uint256 input) external returns (uint256) { + uint32 stepKey = uint32(_trace.length() * 10 + ((input & 7) + 1)); + uint224 stepVal = uint224(((input & 0xff) + 1) * 100); + (, uint224 newVal) = _trace.push(stepKey, stepVal); + + bytes32 msgHash = keccak256(abi.encode(msg.sender, stepKey, newVal)); + bytes32 r = keccak256(abi.encode("R", input, stepKey)); + bytes32 s = bytes32(uint256(keccak256(abi.encode("S", input, stepVal))) & + 0x3fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff); + uint8 v = (input & 1) == 0 ? 27 : 28; + bytes memory sig65 = abi.encodePacked(r, s, v); + address signer1 = ECDSASlice40.recover(msgHash, sig65); + + bytes32 vs = s | (v == 28 ? bytes32(uint256(1) << 255) : bytes32(0)); + address signer2 = ECDSASlice40.recover(msgHash, r, vs); + require(signer1 == signer2, "EMCS: signer mismatch"); + + bytes memory badSig = abi.encodePacked(r, s); + (, ECDSASlice40.RecoverError badErr, bytes32 badArg) = ECDSASlice40.tryRecover(msgHash, badSig); + require( + badErr == ECDSASlice40.RecoverError.InvalidSignatureLength && uint256(badArg) == 64, + "EMCS: expected length 64 error" + ); + + StorageSlotSlice40.StringSlot storage labelSlot = RAW_LABEL_SLOT.getStringSlot(); + StorageSlotSlice40.BytesSlot storage payloadSlot = RAW_PAYLOAD_SLOT.getBytesSlot(); + if ((input & 2) == 0) { + labelSlot.value = "ecdsa-merkle-short"; + payloadSlot.value = sig65; + } else { + labelSlot.value = "ecdsa-merkle-long-storage-slot-string-value-40"; + delete payloadSlot.value; + payloadSlot.value = abi.encodePacked(msgHash, r); + } + StorageSlotSlice40.getStringSlot(_fallbackLabel).value = labelSlot.value; + + uint256 payloadLen = payloadSlot.value.length; + uint224 recentVal = _trace.upperLookupRecent(stepKey); + uint224 lowerVal = _trace.lowerLookup(stepKey > 2 ? stepKey - 2 : 0); + + bytes32 sibling = keccak256(bytes(labelSlot.value)); + bytes32 leaf = keccak256(abi.encode(signer1, recentVal, lowerVal)); + bytes32 pairRoot = leaf < sibling + ? keccak256(abi.encodePacked(leaf, sibling)) + : keccak256(abi.encodePacked(sibling, leaf)); + + emit SignatureCheckpointRecorded(signer1, uint256(stepKey), uint256(recentVal), pairRoot, payloadLen); + + unchecked { + _totalWeight += + uint256(recentVal) + + uint256(lowerVal) + + payloadLen + + bytes(_fallbackLabel).length + + (uint256(uint160(signer1)) & 0xffff); + } + _lastRecoveredHash = pairRoot ^ bytes32(uint256(uint160(signer1))); + require(input != 20, "EMCS: rollback"); + return _totalWeight; + } + + function fail() external { + RAW_LABEL_SLOT.getStringSlot().value = "reverted-slot"; + _totalWeight += 777; + revert("EMCS: fail"); + } + + function read() external view returns (uint256, bytes32, uint256, uint256) { + return ( + _totalWeight, + _lastRecoveredHash, + _trace.length(), + RAW_PAYLOAD_SLOT.getBytesSlot().value.length + ); + } +} diff --git a/Contracts/SolidityImportSmoke/EcdsaMerkleCheckpointsStorageSlotSequenceModel.lean b/Contracts/SolidityImportSmoke/EcdsaMerkleCheckpointsStorageSlotSequenceModel.lean new file mode 100644 index 000000000..9455ea926 --- /dev/null +++ b/Contracts/SolidityImportSmoke/EcdsaMerkleCheckpointsStorageSlotSequenceModel.lean @@ -0,0 +1,39 @@ +import Compiler.SolidityImport.Import +import Compiler.SolidityImport.SequenceRunner +import Compiler.SolidityImport.Differential +import Compiler.CompilationModel +import Compiler.Codegen +import Compiler.Yul.PrettyPrint + +namespace SolidityImportSmoke.EcdsaMerkleCheckpointsStorageSlotSequenceModel +open Compiler.CompilationModel +solidity_import imported from "Contracts/SolidityImportSmoke" entry "EcdsaMerkleCheckpointsStorageSlotSequence.sol" + using { evmVersion := "osaka", viaIR := true, optimizerRuns := some 466, bytecodeHash := "none" } + contract SequenceFixture + function change(uint256) + function fail() + function read() + function recoverFromBytes(bytes32, bytes) + function recoverFromCompact(bytes32, bytes32, bytes32) + function verifyMerkle(«bytes32[]», bytes32, bytes32) + function rawSlotLabel() + function rawSlotPayload() + function checkpointUpperRecent(uint32) +def model : CompilationModel := imported.model +-- Mapping slots use the actual Keccak oracle shared with differential execution. +def oracle : Denote.DenoteOracle := SolidityImport.Differential.oracle +end SolidityImportSmoke.EcdsaMerkleCheckpointsStorageSlotSequenceModel + +def main (args : List String) : IO UInt32 := do + match args with + | ["compile", selectorsFile, output] => + let parsed ← IO.ofExcept (Lean.Json.parse (← IO.FS.readFile selectorsFile)) + let selectors ← IO.ofExcept do + (← parsed.getArr?).toList.mapM fun j => j.getNat? + let compiled ← IO.ofExcept (Compiler.CompilationModel.compile + SolidityImportSmoke.EcdsaMerkleCheckpointsStorageSlotSequenceModel.model selectors .osaka) + IO.FS.writeFile output (Compiler.Yul.render (Compiler.emitYul compiled)) + return 0 + | _ => + Compiler.CompilationModel.SolidityImport.SequenceRunner.run + SolidityImportSmoke.EcdsaMerkleCheckpointsStorageSlotSequenceModel.model SolidityImportSmoke.EcdsaMerkleCheckpointsStorageSlotSequenceModel.oracle args diff --git a/docs/SOLIDITY_IMPORT.md b/docs/SOLIDITY_IMPORT.md index 36ba2e1c2..1d89db329 100644 --- a/docs/SOLIDITY_IMPORT.md +++ b/docs/SOLIDITY_IMPORT.md @@ -857,3 +857,12 @@ prerequisite for the measured IdLib path, not an implementation of `storeInCode` | Decrementing `for (uint256 i = start; i > lower; --i)` loops (`Strings.toHexString`) | `lowerFor` supports `for (uint256 i = start; i > lower; --i)` (and `i--` / `i -= 1`) when `i` is not modified in the loop body and `lower` is an invariant literal, parameter, or unassigned local, evaluating `start` once, computing `count := start > lower ? start - lower : 0`, and executing `Stmt.forEach iterIdx count` with `i := start - iterIdx` bound in `values` and `yulNames`. | | `Arrays.findUpperBound(uint256[] storage, uint256)`, `BitMaps.setTo`, and `Strings.equal(string memory, string memory)` | `lowerWhile` binary-search recognition (`classifyBinarySearchBranch`) unwraps `UncheckedBlock` inside `if / else` branches (`unchecked { low = mid + 1; }` in `Arrays.findUpperBound`) and accepts helper calls (`Math.average(low, high)`) and storage dynamic array reads (`array.unsafeAccess(mid).value > element`) in the branch condition. `lowerYul` lowers `mstore(0x00, a)` / `keccak256(a, b)` in inline assembly (`Strings.equal` via `keccak256(add(a, 0x20), mload(a)) == keccak256(add(b, 0x20), mload(b))`) when `a` and `b` are header-backed `string` / `bytes` bindings in `yulNames` (`bindHelperParams` binds `string memory` / `bytes memory` parameters in `yulNames` to a materialized `[length, payload...]` header block). | +### Development slice: `ECDSA` Yul signature unpacking (`mload(signature)` / `mload(add(signature, 0x20/0x40/0x60))`), provably-bounded Yul narrow-local assignments (`v := byte(0, ...)`), custom-error scalar-cast arguments (`ECDSA._throwError`), and `StorageSlot.getStringSlot(bytes32)` / `StorageSlot.getBytesSlot(bytes32)` + +| Supported Solidity | Lowering boundary | +| --- | --- | +| Yul byte-buffer header and word loads (`mload(b)` and `mload(add(b, offset))`, `ECDSA.tryRecover(bytes32, bytes memory)`, `yulByteBufferLoad?`) | `bindRoot`, `bindHelperParams`, and `lowerLocal` record unshadowed `bytes memory` and `string memory` variables in `Env.yulMemoryStructs`. When `b` is not bound in `Env.yulNames` (`yulByteBufferByName?`), `lowerYul` lowers `mload(b)` to `{ pre := buf.pre, expr := buf.size }` and `mload(add(b, offset))` / `mload(add(offset, b))` for 32-byte-aligned positive word offsets (`offset >= 32 && offset % 32 == 0`, `yulPositiveWordOffsetLiteral?`) to `Expr.mload (.add buf.pointer (.literal (offset - 32)))`. Zero or unaligned offsets fail closed (`unsupported Yul builtin mload`). | +| Yul assignments of provably-bounded expressions to narrow non-enum scalar locals (`uint8 v; assembly { v := byte(0, mload(add(signature, 0x60))) }`, `isProvablyBoundedYulExpr`) | `lowerYulDirectAssignmentTarget` admits Yul assignments to narrow non-enum scalar locals/parameters (`bool`, `uint8`–`uint248`, `address`) when the lowered RHS expression is provably bounded by `2^bits` (`isProvablyBoundedYulExpr`: `.literal n` with `n < 2^bits`, `.byte _ _` for `bits >= 8`, `.lt`/`.gt`/`.slt`/`.sgt`/`.eq`/`.logicalNot` for `bits >= 1`, `.bitAnd` with a mask `< 2^bits`, `.shr` by `>= 256 - bits`, or `.mod` by `0 < m <= 2^bits`). Arbitrary unmasked Yul expressions (`narrow := add(narrow, 1)`, `v := mload(...)`) continue to fail closed (`Yul assignment to narrow local is unsupported`). | +| Scalar `typeConversion` casts in custom-error revert arguments (`revert ECDSAInvalidSignatureLength(uint256(errorArg))`) | `lowerErrorArguments` accepts single-argument `typeConversion` calls whose inner expression is an identifier bound in `Env.values` (such as `uint256(errorArg)` where `errorArg` is `bytes32`), lowering and converting the argument via `convert errorParamType (← mType argument) (← lowerExpr argument) argument`. | +| Raw `bytes32` slot wrappers `StorageSlot.getStringSlot(bytes32 slot)` and `StorageSlot.getBytesSlot(bytes32 slot)` (`inlineStorageStructFn`) | When an internal/private/library storage-pointer helper returns a 1-member wrapper struct `struct { string value; }` or `struct { bytes value; }` via a 1-statement `r.slot := slot` assembly block (`prefixYstmts.isEmpty && sMembers.size == 1 && m0Name == "value"`), `inlineStorageStructFn` binds `slot` to a fresh local and returns `SPath.bytesSlot ("", .localVar slotBinding) isString`, enabling `.value` reads, `.value.length`, `.value = ...` writes, `delete ...value`, and `string storage` / `bytes storage` helper arguments on raw `bytes32` slots. | + diff --git a/lakefile.lean b/lakefile.lean index 5daf9c177..b2bc9c5c9 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -111,6 +111,7 @@ lean_lib «SolidityImportSmoke» where .one `Contracts.SolidityImportSmoke.TimelockAndBytes4CastSequenceModel, .one `Contracts.SolidityImportSmoke.StringBytesMappingsUriStorageStringsSequenceModel, .one `Contracts.SolidityImportSmoke.StringsHexArraysBitmapsSequenceModel, + .one `Contracts.SolidityImportSmoke.EcdsaMerkleCheckpointsStorageSlotSequenceModel, .one `Compiler.SolidityImport.AbiByteLanes, .one `Compiler.SolidityImport.AbiMemory, .one `Contracts.SolidityImportSmoke.EnvironmentSequenceModel, diff --git a/scripts/solidity_differential/check_stateful.py b/scripts/solidity_differential/check_stateful.py index 31be8636d..ce9629cf2 100644 --- a/scripts/solidity_differential/check_stateful.py +++ b/scripts/solidity_differential/check_stateful.py @@ -303,6 +303,12 @@ def main(): 'checkStringEqual(string,string)', 'upperBound(uint256)', 'bitmapBit(uint256)', + 'recoverFromBytes(bytes32,bytes)', + 'recoverFromCompact(bytes32,bytes32,bytes32)', + 'verifyMerkle(bytes32[],bytes32,bytes32)', + 'rawSlotLabel()', + 'rawSlotPayload()', + 'checkpointUpperRecent(uint32)', ): if extra_name in source['methodIdentifiers']: names.append(extra_name) @@ -835,6 +841,34 @@ def mapping_slot(base, key): ] remaining_budget = max(0, args.transactions - len(calls)) calls.extend(strings_hex_prefix[:remaining_budget]) + if 'recoverFromBytes(bytes32,bytes)' in names: + ecdsa_merkle_prefix = [ + ('recoverFromBytes(bytes32,bytes)', [0x1111, 64, 65, 0x2222, 0x3333, 27 << 248]), + ('recoverFromBytes(bytes32,bytes)', [0x1111, 64, 65, 0x2222, 0x3333, 28 << 248]), + ('recoverFromBytes(bytes32,bytes)', [0x1111, 64, 64, 0x2222, 0x3333]), + ('recoverFromBytes(bytes32,bytes)', [0x1111, 64, 65, 0x2222, (1 << 255) + 1, 27 << 248]), + ('recoverFromBytes(bytes32,bytes)', [0x1111, 64, 65, 0x2222, 0x3333, 26 << 248]), + ('recoverFromCompact(bytes32,bytes32,bytes32)', [0x1111, 0x2222, 0x3333]), + ('recoverFromCompact(bytes32,bytes32,bytes32)', [0x1111, 0x2222, 0x3333 | (1 << 255)]), + ('recoverFromCompact(bytes32,bytes32,bytes32)', [0x1111, 0, 0x3333]), + ('verifyMerkle(bytes32[],bytes32,bytes32)', [96, 0x1234, 0x1234, 0]), + ('verifyMerkle(bytes32[],bytes32,bytes32)', [96, 0x1234, 0x5678, 0]), + ('verifyMerkle(bytes32[],bytes32,bytes32)', [96, 0x9999, 0x1234, 1, 0x5678]), + ('rawSlotLabel()', []), + ('rawSlotPayload()', []), + ('checkpointUpperRecent(uint32)', [10]), + ('change(uint256)', [0]), + ('rawSlotLabel()', []), + ('rawSlotPayload()', []), + ('checkpointUpperRecent(uint32)', [5]), + ('change(uint256)', [2]), + ('rawSlotLabel()', []), + ('rawSlotPayload()', []), + ('checkpointUpperRecent(uint32)', [65]), + ('read()', []), + ] + remaining_budget = max(0, args.transactions - len(calls)) + calls.extend(ecdsa_merkle_prefix[:remaining_budget]) while len(calls) < args.transactions: name = rng.choice(names) if name == names[0]: @@ -1092,6 +1126,28 @@ def mapping_slot(base, key): ]) elif name in ('upperBound(uint256)', 'bitmapBit(uint256)'): call_args = [rng.choice([0, 1, 5, 10, 20, 50, 255, 256])] + elif name == 'recoverFromBytes(bytes32,bytes)': + call_args = rng.choice([ + [0x1111, 64, 65, 0x2222, 0x3333, 27 << 248], + [0x1111, 64, 65, 0x2222, 0x3333, 28 << 248], + [0x1111, 64, 64, 0x2222, 0x3333], + [0x1111, 64, 65, 0x2222, (1 << 255) + 1, 27 << 248], + [0x1111, 64, 65, 0x2222, 0x3333, 26 << 248], + ]) + elif name == 'recoverFromCompact(bytes32,bytes32,bytes32)': + call_args = rng.choice([ + [0x1111, 0x2222, 0x3333], + [0x1111, 0x2222, 0x3333 | (1 << 255)], + [0x1111, 0, 0x3333], + ]) + elif name == 'verifyMerkle(bytes32[],bytes32,bytes32)': + call_args = rng.choice([ + [96, 0x1234, 0x1234, 0], + [96, 0x1234, 0x5678, 0], + [96, 0x9999, 0x1234, 1, 0x5678], + ]) + elif name == 'checkpointUpperRecent(uint32)': + call_args = [rng.choice([0, 1, 5, 15, 35, 65, 100, 1 << 32])] else: call_args = [] calls.append((name, call_args)) diff --git a/scripts/solidity_differential/check_storage.py b/scripts/solidity_differential/check_storage.py index 5d664e741..b6b55f3be 100644 --- a/scripts/solidity_differential/check_storage.py +++ b/scripts/solidity_differential/check_storage.py @@ -6,7 +6,7 @@ import tempfile from .engine import command, write_json -from .programs import stateful_storage_source, stateful_storage_word_source, stateful_mapping_source, stateful_short_circuit_source, stateful_imported_event_source, stateful_if_else_source, stateful_numeric_literal_source, stateful_constant_array_source, stateful_modulo_source, stateful_default_local_source, stateful_local_write_source, stateful_invariant_for_source, stateful_helper_loop_source, stateful_packed_member_write_source, stateful_helper_effect_source, stateful_fixed_array_source, stateful_array_write_order_source, stateful_discarded_helper_source, stateful_encoded_byte_local_source, stateful_named_helper_return_source, stateful_yul_numeric_source, stateful_solc_0810_source, stateful_inheritance_source, stateful_void_helper_guard_source, stateful_modifier_unchecked_compound_source, stateful_tuple_helper_source, stateful_int256_contract_type_source, stateful_fn_ptr_struct_delete_modifier_source, stateful_empty_array_bytes_calldata_source, stateful_overload_const_error_cond_tuple_tload_source, stateful_struct_fixed_array_and_fixed_return_source, stateful_msg_data_and_enum_source, stateful_exp_and_bitwise_shift_source, stateful_while_clz_and_struct_loc_source, stateful_yul_builtins_and_encode_selector_source, stateful_array_string_params_and_context_source, stateful_bytes_memory_and_abi_encode_call_source, stateful_dynamic_bytes_and_string_return_source, stateful_bytes_and_string_storage_source, stateful_yul_block_mulmod_tstore_source, stateful_merkle_and_nonces_source, stateful_multiproof_mapping_keys_ratifiers_source, stateful_udvt_param_assign_hashmarket_source, stateful_struct_mapping_and_bytes4_interface_source, stateful_erc2981_holders_arrays_msghash_source, stateful_enumerable_set_map_storage_arrays_source, stateful_checkpoints_and_struct_arrays_source, stateful_ticklib_and_three_key_mapping_source, stateful_offer_hash_and_domain_separator_source, stateful_abi_decode_and_ratifier_source, stateful_votes_checkpoints_arrays_bitmaps_source, stateful_public_getters_and_builtins_source, stateful_ecrecover_authorizer_arrays_map_source, stateful_market_params_balances_source, stateful_midnight_position_and_fee_source, stateful_timelock_and_bytes4_cast_source, stateful_string_bytes_mappings_uri_storage_strings_source, stateful_strings_hex_arrays_bitmaps_source +from .programs import stateful_storage_source, stateful_storage_word_source, stateful_mapping_source, stateful_short_circuit_source, stateful_imported_event_source, stateful_if_else_source, stateful_numeric_literal_source, stateful_constant_array_source, stateful_modulo_source, stateful_default_local_source, stateful_local_write_source, stateful_invariant_for_source, stateful_helper_loop_source, stateful_packed_member_write_source, stateful_helper_effect_source, stateful_fixed_array_source, stateful_array_write_order_source, stateful_discarded_helper_source, stateful_encoded_byte_local_source, stateful_named_helper_return_source, stateful_yul_numeric_source, stateful_solc_0810_source, stateful_inheritance_source, stateful_void_helper_guard_source, stateful_modifier_unchecked_compound_source, stateful_tuple_helper_source, stateful_int256_contract_type_source, stateful_fn_ptr_struct_delete_modifier_source, stateful_empty_array_bytes_calldata_source, stateful_overload_const_error_cond_tuple_tload_source, stateful_struct_fixed_array_and_fixed_return_source, stateful_msg_data_and_enum_source, stateful_exp_and_bitwise_shift_source, stateful_while_clz_and_struct_loc_source, stateful_yul_builtins_and_encode_selector_source, stateful_array_string_params_and_context_source, stateful_bytes_memory_and_abi_encode_call_source, stateful_dynamic_bytes_and_string_return_source, stateful_bytes_and_string_storage_source, stateful_yul_block_mulmod_tstore_source, stateful_merkle_and_nonces_source, stateful_multiproof_mapping_keys_ratifiers_source, stateful_udvt_param_assign_hashmarket_source, stateful_struct_mapping_and_bytes4_interface_source, stateful_erc2981_holders_arrays_msghash_source, stateful_enumerable_set_map_storage_arrays_source, stateful_checkpoints_and_struct_arrays_source, stateful_ticklib_and_three_key_mapping_source, stateful_offer_hash_and_domain_separator_source, stateful_abi_decode_and_ratifier_source, stateful_votes_checkpoints_arrays_bitmaps_source, stateful_public_getters_and_builtins_source, stateful_ecrecover_authorizer_arrays_map_source, stateful_market_params_balances_source, stateful_midnight_position_and_fee_source, stateful_timelock_and_bytes4_cast_source, stateful_string_bytes_mappings_uri_storage_strings_source, stateful_strings_hex_arrays_bitmaps_source, stateful_ecdsa_merkle_checkpoints_storage_slot_source from .stateful import validate_observation @@ -25,7 +25,7 @@ def canonical_observations(observations): def main(): parser = argparse.ArgumentParser(description=__doc__) - parser.add_argument('--fixture', choices=('packed', 'void', 'bytes', 'mapping', 'short-circuit', 'imported-event', 'narrow-event', 'if-else', 'numeric-literals', 'constant-arrays', 'modulo', 'default-locals', 'local-writes', 'invariant-for', 'helper-loops', 'packed-member-writes', 'helper-effects', 'fixed-arrays', 'array-write-order', 'discarded-helper', 'encoded-byte-locals', 'named-helper-returns', 'yul-numeric', 'solc-0810', 'inheritance', 'void-helper-guards', 'modifier-unchecked-compound', 'tuple-helper', 'int256-contract-types', 'fn-ptr-struct-delete-modifier', 'empty-array-bytes-calldata', 'overload-const-error-cond-tuple-tload', 'struct-fixed-array-and-fixed-return', 'msg-data-and-enum', 'exp-and-bitwise-shifts', 'while-clz-and-struct-loc', 'yul-builtins-and-encode-selector', 'array-string-params-and-context', 'bytes-memory-and-abi-encode-call', 'dynamic-bytes-and-string-return', 'bytes-and-string-storage', 'yul-block-mulmod-tstore', 'merkle-and-nonces', 'multiproof-mapping-keys-ratifiers', 'udvt-param-assign-hashmarket', 'struct-mapping-and-bytes4-interface', 'erc2981-holders-arrays-msghash', 'enumerable-set-map-storage-arrays', 'checkpoints-and-struct-arrays', 'ticklib-and-three-key-mapping', 'offer-hash-and-domain-separator', 'abi-decode-and-ratifier', 'votes-checkpoints-arrays-bitmaps', 'public-getters-and-builtins', 'ecrecover-authorizer-arrays-map', 'market-params-balances', 'midnight-position-and-fee', 'timelock-and-bytes4-cast', 'string-bytes-mappings-uri-storage-strings', 'strings-hex-arrays-bitmaps'), default='packed') + parser.add_argument('--fixture', choices=('packed', 'void', 'bytes', 'mapping', 'short-circuit', 'imported-event', 'narrow-event', 'if-else', 'numeric-literals', 'constant-arrays', 'modulo', 'default-locals', 'local-writes', 'invariant-for', 'helper-loops', 'packed-member-writes', 'helper-effects', 'fixed-arrays', 'array-write-order', 'discarded-helper', 'encoded-byte-locals', 'named-helper-returns', 'yul-numeric', 'solc-0810', 'inheritance', 'void-helper-guards', 'modifier-unchecked-compound', 'tuple-helper', 'int256-contract-types', 'fn-ptr-struct-delete-modifier', 'empty-array-bytes-calldata', 'overload-const-error-cond-tuple-tload', 'struct-fixed-array-and-fixed-return', 'msg-data-and-enum', 'exp-and-bitwise-shifts', 'while-clz-and-struct-loc', 'yul-builtins-and-encode-selector', 'array-string-params-and-context', 'bytes-memory-and-abi-encode-call', 'dynamic-bytes-and-string-return', 'bytes-and-string-storage', 'yul-block-mulmod-tstore', 'merkle-and-nonces', 'multiproof-mapping-keys-ratifiers', 'udvt-param-assign-hashmarket', 'struct-mapping-and-bytes4-interface', 'erc2981-holders-arrays-msghash', 'enumerable-set-map-storage-arrays', 'checkpoints-and-struct-arrays', 'ticklib-and-three-key-mapping', 'offer-hash-and-domain-separator', 'abi-decode-and-ratifier', 'votes-checkpoints-arrays-bitmaps', 'public-getters-and-builtins', 'ecrecover-authorizer-arrays-map', 'market-params-balances', 'midnight-position-and-fee', 'timelock-and-bytes4-cast', 'string-bytes-mappings-uri-storage-strings', 'strings-hex-arrays-bitmaps', 'ecdsa-merkle-checkpoints-storage-slot'), default='packed') parser.add_argument('--narrow-bits', type=int, choices=range(8, 257, 8), default=128) parser.add_argument('--transactions', type=int, default=32) parser.add_argument('--seed', type=int, default=2453) @@ -33,7 +33,7 @@ def main(): args = parser.parse_args() output = args.output.resolve() if args.output else Path(tempfile.mkdtemp(prefix='storage-', dir='.lake')).resolve() output.mkdir(parents=True, exist_ok=args.output is None) - name = {'packed': 'StorageSequence', 'void': 'StorageVoidSequence', 'bytes': 'StorageBytesSequence', 'mapping': 'MappingSequence', 'short-circuit': 'ShortCircuitSequence', 'imported-event': 'ImportedEventSequence', 'narrow-event': 'NarrowEventSequence', 'if-else': 'IfElseSequence', 'numeric-literals': 'NumericLiteralSequence', 'constant-arrays': 'ConstantArraySequence', 'modulo': 'ModuloSequence', 'default-locals': 'DefaultLocalSequence', 'local-writes': 'LocalWriteSequence', 'invariant-for': 'InvariantForSequence', 'helper-loops': 'HelperLoopSequence', 'packed-member-writes': 'PackedMemberWriteSequence', 'helper-effects': 'HelperEffectSequence', 'fixed-arrays': 'MappingFixedArraySequence', 'array-write-order': 'FixedArrayWriteOrderSequence', 'discarded-helper': 'DiscardedHelperSequence', 'encoded-byte-locals': 'EncodedByteLocalSequence', 'named-helper-returns': 'NamedHelperReturnSequence', 'yul-numeric': 'YulNumericSequence', 'solc-0810': 'Solc0810Sequence', 'inheritance': 'InheritanceSequence', 'void-helper-guards': 'VoidHelperGuardSequence', 'modifier-unchecked-compound': 'ModifierUncheckedCompoundSequence', 'tuple-helper': 'TupleHelperSequence', 'int256-contract-types': 'Int256ContractTypeSequence', 'fn-ptr-struct-delete-modifier': 'FnPtrStructDeleteModifierSequence', 'empty-array-bytes-calldata': 'EmptyArrayReturnBytesCalldataSequence', 'overload-const-error-cond-tuple-tload': 'OverloadConstErrorCondTupleTloadSequence', 'struct-fixed-array-and-fixed-return': 'StructFixedArrayAndFixedReturnSequence', 'msg-data-and-enum': 'MsgDataAndEnumSequence', 'exp-and-bitwise-shifts': 'ExpAndBitwiseShiftSequence', 'while-clz-and-struct-loc': 'WhileClzAndStructLocSequence', 'yul-builtins-and-encode-selector': 'YulBuiltinsAndEncodeSelectorSequence', 'array-string-params-and-context': 'ArrayStringParamsAndContextSequence', 'bytes-memory-and-abi-encode-call': 'BytesMemoryAndAbiEncodeCallSequence', 'dynamic-bytes-and-string-return': 'DynamicBytesAndStringReturnSequence', 'bytes-and-string-storage': 'BytesAndStringStorageSequence', 'yul-block-mulmod-tstore': 'YulBlockMulmodTstoreSequence', 'merkle-and-nonces': 'MerkleAndNoncesSequence', 'multiproof-mapping-keys-ratifiers': 'MultiProofMappingKeysRatifiersSequence', 'udvt-param-assign-hashmarket': 'UdvtParamAssignHashMarketSequence', 'struct-mapping-and-bytes4-interface': 'StructMappingAndBytes4InterfaceSequence', 'erc2981-holders-arrays-msghash': 'ERC2981HoldersArraysMsgHashSequence', 'enumerable-set-map-storage-arrays': 'EnumerableSetMapSequence', 'checkpoints-and-struct-arrays': 'CheckpointsAndStructArraysSequence', 'ticklib-and-three-key-mapping': 'TickLibAndThreeKeyMappingSequence', 'offer-hash-and-domain-separator': 'OfferHashAndDomainSeparatorSequence', 'abi-decode-and-ratifier': 'AbiDecodeAndRatifierSequence', 'votes-checkpoints-arrays-bitmaps': 'VotesCheckpointsArraysBitMapsSequence', 'public-getters-and-builtins': 'PublicGettersAndBuiltinsSequence', 'ecrecover-authorizer-arrays-map': 'EcrecoverAuthorizerArraysMapSequence', 'market-params-balances': 'MarketParamsBalancesSequence', 'midnight-position-and-fee': 'MidnightPositionAndFeeSequence', 'timelock-and-bytes4-cast': 'TimelockAndBytes4CastSequence', 'string-bytes-mappings-uri-storage-strings': 'StringBytesMappingsUriStorageStringsSequence', 'strings-hex-arrays-bitmaps': 'StringsHexArraysBitmapsSequence'}[args.fixture] + name = {'packed': 'StorageSequence', 'void': 'StorageVoidSequence', 'bytes': 'StorageBytesSequence', 'mapping': 'MappingSequence', 'short-circuit': 'ShortCircuitSequence', 'imported-event': 'ImportedEventSequence', 'narrow-event': 'NarrowEventSequence', 'if-else': 'IfElseSequence', 'numeric-literals': 'NumericLiteralSequence', 'constant-arrays': 'ConstantArraySequence', 'modulo': 'ModuloSequence', 'default-locals': 'DefaultLocalSequence', 'local-writes': 'LocalWriteSequence', 'invariant-for': 'InvariantForSequence', 'helper-loops': 'HelperLoopSequence', 'packed-member-writes': 'PackedMemberWriteSequence', 'helper-effects': 'HelperEffectSequence', 'fixed-arrays': 'MappingFixedArraySequence', 'array-write-order': 'FixedArrayWriteOrderSequence', 'discarded-helper': 'DiscardedHelperSequence', 'encoded-byte-locals': 'EncodedByteLocalSequence', 'named-helper-returns': 'NamedHelperReturnSequence', 'yul-numeric': 'YulNumericSequence', 'solc-0810': 'Solc0810Sequence', 'inheritance': 'InheritanceSequence', 'void-helper-guards': 'VoidHelperGuardSequence', 'modifier-unchecked-compound': 'ModifierUncheckedCompoundSequence', 'tuple-helper': 'TupleHelperSequence', 'int256-contract-types': 'Int256ContractTypeSequence', 'fn-ptr-struct-delete-modifier': 'FnPtrStructDeleteModifierSequence', 'empty-array-bytes-calldata': 'EmptyArrayReturnBytesCalldataSequence', 'overload-const-error-cond-tuple-tload': 'OverloadConstErrorCondTupleTloadSequence', 'struct-fixed-array-and-fixed-return': 'StructFixedArrayAndFixedReturnSequence', 'msg-data-and-enum': 'MsgDataAndEnumSequence', 'exp-and-bitwise-shifts': 'ExpAndBitwiseShiftSequence', 'while-clz-and-struct-loc': 'WhileClzAndStructLocSequence', 'yul-builtins-and-encode-selector': 'YulBuiltinsAndEncodeSelectorSequence', 'array-string-params-and-context': 'ArrayStringParamsAndContextSequence', 'bytes-memory-and-abi-encode-call': 'BytesMemoryAndAbiEncodeCallSequence', 'dynamic-bytes-and-string-return': 'DynamicBytesAndStringReturnSequence', 'bytes-and-string-storage': 'BytesAndStringStorageSequence', 'yul-block-mulmod-tstore': 'YulBlockMulmodTstoreSequence', 'merkle-and-nonces': 'MerkleAndNoncesSequence', 'multiproof-mapping-keys-ratifiers': 'MultiProofMappingKeysRatifiersSequence', 'udvt-param-assign-hashmarket': 'UdvtParamAssignHashMarketSequence', 'struct-mapping-and-bytes4-interface': 'StructMappingAndBytes4InterfaceSequence', 'erc2981-holders-arrays-msghash': 'ERC2981HoldersArraysMsgHashSequence', 'enumerable-set-map-storage-arrays': 'EnumerableSetMapSequence', 'checkpoints-and-struct-arrays': 'CheckpointsAndStructArraysSequence', 'ticklib-and-three-key-mapping': 'TickLibAndThreeKeyMappingSequence', 'offer-hash-and-domain-separator': 'OfferHashAndDomainSeparatorSequence', 'abi-decode-and-ratifier': 'AbiDecodeAndRatifierSequence', 'votes-checkpoints-arrays-bitmaps': 'VotesCheckpointsArraysBitMapsSequence', 'public-getters-and-builtins': 'PublicGettersAndBuiltinsSequence', 'ecrecover-authorizer-arrays-map': 'EcrecoverAuthorizerArraysMapSequence', 'market-params-balances': 'MarketParamsBalancesSequence', 'midnight-position-and-fee': 'MidnightPositionAndFeeSequence', 'timelock-and-bytes4-cast': 'TimelockAndBytes4CastSequence', 'string-bytes-mappings-uri-storage-strings': 'StringBytesMappingsUriStorageStringsSequence', 'strings-hex-arrays-bitmaps': 'StringsHexArraysBitmapsSequence', 'ecdsa-merkle-checkpoints-storage-slot': 'EcdsaMerkleCheckpointsStorageSlotSequence'}[args.fixture] fixture = Path(f'Contracts/SolidityImportSmoke/{name}.sol').read_text() template = Path(f'Contracts/SolidityImportSmoke/{name}Model.lean').read_text() if args.fixture == 'narrow-event': @@ -53,6 +53,8 @@ def main(): variants = ('baseline', 'renamed', 'assignment-step') if args.fixture in ('packed-member-writes', 'helper-effects', 'fixed-arrays'): variants = ('baseline', 'renamed', 'explicit-delete') + if args.fixture == 'ecdsa-merkle-checkpoints-storage-slot': + variants = ('baseline', 'renamed', 'expanded-ecdsa-merkle-checkpoints-storage-slot') if args.fixture == 'strings-hex-arrays-bitmaps': variants = ('baseline', 'renamed', 'expanded-strings-hex-arrays-bitmaps') if args.fixture == 'string-bytes-mappings-uri-storage-strings': @@ -158,6 +160,7 @@ def main(): Path('Contracts/SolidityImportSmoke/InheritanceBase.sol').read_text()) source = directory / 'Sequence.sol' source.write_text(stateful_imported_event_source(fixture, variant, args.fixture == "narrow-event") if args.fixture in ("imported-event", "narrow-event") + else stateful_ecdsa_merkle_checkpoints_storage_slot_source(fixture, variant) if args.fixture == "ecdsa-merkle-checkpoints-storage-slot" else stateful_strings_hex_arrays_bitmaps_source(fixture, variant) if args.fixture == "strings-hex-arrays-bitmaps" else stateful_string_bytes_mappings_uri_storage_strings_source(fixture, variant) if args.fixture == "string-bytes-mappings-uri-storage-strings" else stateful_timelock_and_bytes4_cast_source(fixture, variant) if args.fixture == "timelock-and-bytes4-cast" @@ -220,7 +223,7 @@ def main(): extra = ['--change-prefix', *map(str, list(range(9)) + [65535, 65536, (1 << 256) - 1])] if args.fixture == 'fixed-arrays' else [] if args.fixture == 'empty-array-bytes-calldata': extra = ['--change-prefix', *map(str, [0, 1, 2, 3, 16, 17, 18, (1 << 256) - 1])] - if args.fixture in ('inheritance', 'void-helper-guards', 'modifier-unchecked-compound', 'tuple-helper', 'int256-contract-types', 'fn-ptr-struct-delete-modifier', 'overload-const-error-cond-tuple-tload', 'struct-fixed-array-and-fixed-return', 'msg-data-and-enum', 'exp-and-bitwise-shifts', 'while-clz-and-struct-loc', 'yul-builtins-and-encode-selector', 'array-string-params-and-context', 'bytes-memory-and-abi-encode-call', 'dynamic-bytes-and-string-return', 'bytes-and-string-storage', 'yul-block-mulmod-tstore', 'merkle-and-nonces', 'multiproof-mapping-keys-ratifiers', 'udvt-param-assign-hashmarket', 'struct-mapping-and-bytes4-interface', 'erc2981-holders-arrays-msghash', 'enumerable-set-map-storage-arrays', 'checkpoints-and-struct-arrays', 'ticklib-and-three-key-mapping', 'offer-hash-and-domain-separator', 'abi-decode-and-ratifier', 'votes-checkpoints-arrays-bitmaps', 'public-getters-and-builtins', 'ecrecover-authorizer-arrays-map', 'market-params-balances', 'midnight-position-and-fee', 'timelock-and-bytes4-cast', 'string-bytes-mappings-uri-storage-strings', 'strings-hex-arrays-bitmaps'): + if args.fixture in ('inheritance', 'void-helper-guards', 'modifier-unchecked-compound', 'tuple-helper', 'int256-contract-types', 'fn-ptr-struct-delete-modifier', 'overload-const-error-cond-tuple-tload', 'struct-fixed-array-and-fixed-return', 'msg-data-and-enum', 'exp-and-bitwise-shifts', 'while-clz-and-struct-loc', 'yul-builtins-and-encode-selector', 'array-string-params-and-context', 'bytes-memory-and-abi-encode-call', 'dynamic-bytes-and-string-return', 'bytes-and-string-storage', 'yul-block-mulmod-tstore', 'merkle-and-nonces', 'multiproof-mapping-keys-ratifiers', 'udvt-param-assign-hashmarket', 'struct-mapping-and-bytes4-interface', 'erc2981-holders-arrays-msghash', 'enumerable-set-map-storage-arrays', 'checkpoints-and-struct-arrays', 'ticklib-and-three-key-mapping', 'offer-hash-and-domain-separator', 'abi-decode-and-ratifier', 'votes-checkpoints-arrays-bitmaps', 'public-getters-and-builtins', 'ecrecover-authorizer-arrays-map', 'market-params-balances', 'midnight-position-and-fee', 'timelock-and-bytes4-cast', 'string-bytes-mappings-uri-storage-strings', 'strings-hex-arrays-bitmaps', 'ecdsa-merkle-checkpoints-storage-slot'): extra = ['--change-prefix', *map(str, list(range(9)) + [19, 20, 21, 96, 97, 98, 99999, 100000, (1 << 256) - 1])] if args.fixture == 'timelock-and-bytes4-cast': extra = ['--change-prefix', *map(str, [0, 1, 2, 3, 20, 21, 22])] @@ -228,6 +231,8 @@ def main(): extra = ['--change-prefix', *map(str, [0, 1, 2, 4, 8, 20, 21])] if args.fixture == 'strings-hex-arrays-bitmaps': extra = ['--change-prefix', *map(str, [0, 1, 2, 3, 4, 20, 21])] + if args.fixture == 'ecdsa-merkle-checkpoints-storage-slot': + extra = ['--change-prefix', *map(str, [0, 1, 2, 3, 4, 5, 6, 20])] if args.fixture == 'solc-0810': extra = ['--solc-version', '0.8.10', '--change-prefix', *map(str, [0, 1, 2, 3, 19, 20, 21, 100, 1000, 50000, 100000, 999999, (1 << 256) - 1])] if args.fixture == 'yul-numeric': diff --git a/scripts/solidity_differential/check_storage_mutations.py b/scripts/solidity_differential/check_storage_mutations.py index fcdeb3a0b..626353c06 100644 --- a/scripts/solidity_differential/check_storage_mutations.py +++ b/scripts/solidity_differential/check_storage_mutations.py @@ -355,10 +355,16 @@ 'import-strings-hex-arrays-bitmaps-byte-buf-write-zero': (' let clearedWord := Expr.bitAnd (.mload wordAddr) (.bitNot byteMask)\n let updatedWord := if deleting then clearedWord else Expr.bitOr clearedWord (.shl shiftBits topByte)', ' let clearedWord := Expr.bitAnd (.mload wordAddr) (.bitNot byteMask)\n let _ := (shiftBits, topByte)\n let updatedWord := if deleting then clearedWord else clearedWord'), 'import-strings-hex-arrays-bitmaps-dec-for-count-zero': (' return startVal.pre ++ #[\n .letVar countBinding (.literal 0),\n .ite (.gt startVal.expr lowerVal.expr)\n [.assignVar countBinding (.sub startVal.expr lowerVal.expr)] [],\n .forEach iterIdx (.localVar countBinding) loopBodyStmts\n ]', ' return startVal.pre ++ #[\n .letVar countBinding (.literal 0),\n .ite (.gt startVal.expr lowerVal.expr)\n [.assignVar countBinding (.literal 0)] [],\n .forEach iterIdx (.localVar countBinding) loopBodyStmts\n ]'), 'import-strings-hex-arrays-bitmaps-stateful-fixed-bytes-index-guard': (' if statefulCallIn baseExpression (← get) || statefulCallIn indexExpression (← get) ||\n assignmentIn baseExpression || assignmentIn indexExpression then\n failAt j "stateful or assignment fixed-bytes index is unsupported"', ' if false then\n failAt j "stateful or assignment fixed-bytes index is unsupported"'), + 'import-ecdsa-merkle-checkpoints-storage-slot-yul-byte-buf-len-zero': (' if let some buf ← yulByteBufferByName? addrNode then\n return some { pre := buf.pre, expr := buf.size }', ' if let some buf ← yulByteBufferByName? addrNode then\n return some { pre := buf.pre, expr := .literal 0 }'), + 'import-ecdsa-merkle-checkpoints-storage-slot-yul-byte-buf-word-zero': (' let some (buf, off) := matched? | return none\n return some {\n pre := buf.pre,\n expr := .mload (.add buf.pointer (.literal (off - 32)))\n }', ' let some (buf, _off) := matched? | return none\n return some {\n pre := buf.pre,\n expr := .literal 0\n }'), + 'import-ecdsa-merkle-checkpoints-storage-slot-raw-bytes-slot-zero': (' if let some isString := rawBytesString? then\n let slotBinding ← freshFor "raw_slot"\n pre := pre ++ extPre ++ prefixPre ++ slotVal.pre |>.push (.letVar slotBinding slotVal.expr)\n let bpath := SPath.bytesSlot ("", .localVar slotBinding) isString', ' if let some isString := rawBytesString? then\n let slotBinding ← freshFor "raw_slot"\n pre := pre ++ extPre ++ prefixPre ++ slotVal.pre |>.push (.letVar slotBinding slotVal.expr)\n let bpath := SPath.bytesSlot ("", .literal 0) isString'), + 'import-ecdsa-merkle-checkpoints-storage-slot-unaligned-byte-mload-guard': (' unless value ≥ 32 && value < 2^256 && value % 32 == 0 do return none', ' unless value ≥ 16 && value < 2^256 do return none'), }) def run(directory, output, name): fixture = "StorageVoidSequence" if name == "import-void-fallthrough" else "StorageSequence" + if name.startswith("import-ecdsa-merkle-checkpoints-storage-slot-"): + fixture = "EcdsaMerkleCheckpointsStorageSlotSequence" if name.startswith("import-strings-hex-arrays-bitmaps-"): fixture = "StringsHexArraysBitmapsSequence" if name.startswith("import-string-bytes-mappings-uri-storage-strings-"): @@ -479,11 +485,11 @@ def run(directory, output, name): '--model-driver', f'Contracts/SolidityImportSmoke/{fixture}Model.lean', '--source-fixture', f'Contracts/SolidityImportSmoke/{fixture}.sol', '--argument-bits', '128' if fixture == 'NarrowEventSequence' else '256', - '--transactions', '64' if fixture in {'MappingFixedArraySequence', 'FixedArrayWriteOrderSequence', 'DiscardedHelperSequence', 'EncodedByteLocalSequence', 'NamedHelperReturnSequence', 'YulNumericSequence', 'Solc0810Sequence', 'InheritanceSequence', 'VoidHelperGuardSequence', 'ModifierUncheckedCompoundSequence', 'TupleHelperSequence', 'Int256ContractTypeSequence', 'FnPtrStructDeleteModifierSequence', 'EmptyArrayReturnBytesCalldataSequence', 'OverloadConstErrorCondTupleTloadSequence', 'StructFixedArrayAndFixedReturnSequence', 'MsgDataAndEnumSequence', 'ExpAndBitwiseShiftSequence', 'WhileClzAndStructLocSequence', 'YulBuiltinsAndEncodeSelectorSequence', 'ArrayStringParamsAndContextSequence', 'BytesMemoryAndAbiEncodeCallSequence', 'DynamicBytesAndStringReturnSequence', 'BytesAndStringStorageSequence', 'YulBlockMulmodTstoreSequence', 'MerkleAndNoncesSequence', 'MultiProofMappingKeysRatifiersSequence', 'UdvtParamAssignHashMarketSequence', 'StructMappingAndBytes4InterfaceSequence', 'ERC2981HoldersArraysMsgHashSequence', 'StorageStructParamsDequeShortStringsSequence', 'StorageSlotShortStringsTimeSequence', 'EnumerableSetMapSequence', 'CheckpointsAndStructArraysSequence', 'TickLibAndThreeKeyMappingSequence', 'OfferHashAndDomainSeparatorSequence', 'AbiDecodeAndRatifierSequence', 'VotesCheckpointsArraysBitMapsSequence', 'PublicGettersAndBuiltinsSequence', 'EcrecoverAuthorizerArraysMapSequence', 'MarketParamsBalancesSequence', 'MidnightPositionAndFeeSequence', 'TimelockAndBytes4CastSequence', 'StringBytesMappingsUriStorageStringsSequence', 'StringsHexArraysBitmapsSequence'} else '3', - '--seed', '2490' if fixture in {'MappingFixedArraySequence', 'FixedArrayWriteOrderSequence', 'DiscardedHelperSequence', 'EncodedByteLocalSequence', 'NamedHelperReturnSequence', 'YulNumericSequence', 'Solc0810Sequence', 'InheritanceSequence', 'VoidHelperGuardSequence', 'ModifierUncheckedCompoundSequence', 'TupleHelperSequence', 'Int256ContractTypeSequence', 'FnPtrStructDeleteModifierSequence', 'EmptyArrayReturnBytesCalldataSequence', 'OverloadConstErrorCondTupleTloadSequence', 'StructFixedArrayAndFixedReturnSequence', 'MsgDataAndEnumSequence', 'ExpAndBitwiseShiftSequence', 'WhileClzAndStructLocSequence', 'YulBuiltinsAndEncodeSelectorSequence', 'ArrayStringParamsAndContextSequence', 'BytesMemoryAndAbiEncodeCallSequence', 'DynamicBytesAndStringReturnSequence', 'BytesAndStringStorageSequence', 'YulBlockMulmodTstoreSequence', 'MerkleAndNoncesSequence', 'MultiProofMappingKeysRatifiersSequence', 'UdvtParamAssignHashMarketSequence', 'StructMappingAndBytes4InterfaceSequence', 'ERC2981HoldersArraysMsgHashSequence', 'StorageStructParamsDequeShortStringsSequence', 'StorageSlotShortStringsTimeSequence', 'EnumerableSetMapSequence', 'CheckpointsAndStructArraysSequence', 'TickLibAndThreeKeyMappingSequence', 'OfferHashAndDomainSeparatorSequence', 'AbiDecodeAndRatifierSequence', 'VotesCheckpointsArraysBitMapsSequence', 'PublicGettersAndBuiltinsSequence', 'EcrecoverAuthorizerArraysMapSequence', 'MarketParamsBalancesSequence', 'MidnightPositionAndFeeSequence', 'TimelockAndBytes4CastSequence', 'StringBytesMappingsUriStorageStringsSequence', 'StringsHexArraysBitmapsSequence'} else '2453', '--shrink-attempts', '100' if fixture in {'MappingFixedArraySequence', 'FixedArrayWriteOrderSequence', 'DiscardedHelperSequence', 'EncodedByteLocalSequence', 'NamedHelperReturnSequence', 'YulNumericSequence', 'Solc0810Sequence', 'InheritanceSequence', 'VoidHelperGuardSequence', 'ModifierUncheckedCompoundSequence', 'TupleHelperSequence', 'Int256ContractTypeSequence', 'FnPtrStructDeleteModifierSequence', 'EmptyArrayReturnBytesCalldataSequence', 'OverloadConstErrorCondTupleTloadSequence', 'StructFixedArrayAndFixedReturnSequence', 'MsgDataAndEnumSequence', 'ExpAndBitwiseShiftSequence', 'WhileClzAndStructLocSequence', 'YulBuiltinsAndEncodeSelectorSequence', 'ArrayStringParamsAndContextSequence', 'BytesMemoryAndAbiEncodeCallSequence', 'DynamicBytesAndStringReturnSequence', 'BytesAndStringStorageSequence', 'YulBlockMulmodTstoreSequence', 'MerkleAndNoncesSequence', 'MultiProofMappingKeysRatifiersSequence', 'UdvtParamAssignHashMarketSequence', 'StructMappingAndBytes4InterfaceSequence', 'ERC2981HoldersArraysMsgHashSequence', 'StorageStructParamsDequeShortStringsSequence', 'StorageSlotShortStringsTimeSequence', 'EnumerableSetMapSequence', 'CheckpointsAndStructArraysSequence', 'TickLibAndThreeKeyMappingSequence', 'OfferHashAndDomainSeparatorSequence', 'AbiDecodeAndRatifierSequence', 'VotesCheckpointsArraysBitMapsSequence', 'PublicGettersAndBuiltinsSequence', 'EcrecoverAuthorizerArraysMapSequence', 'MarketParamsBalancesSequence', 'MidnightPositionAndFeeSequence', 'TimelockAndBytes4CastSequence', 'StringBytesMappingsUriStorageStringsSequence', 'StringsHexArraysBitmapsSequence'} else '30', + '--transactions', '64' if fixture in {'MappingFixedArraySequence', 'FixedArrayWriteOrderSequence', 'DiscardedHelperSequence', 'EncodedByteLocalSequence', 'NamedHelperReturnSequence', 'YulNumericSequence', 'Solc0810Sequence', 'InheritanceSequence', 'VoidHelperGuardSequence', 'ModifierUncheckedCompoundSequence', 'TupleHelperSequence', 'Int256ContractTypeSequence', 'FnPtrStructDeleteModifierSequence', 'EmptyArrayReturnBytesCalldataSequence', 'OverloadConstErrorCondTupleTloadSequence', 'StructFixedArrayAndFixedReturnSequence', 'MsgDataAndEnumSequence', 'ExpAndBitwiseShiftSequence', 'WhileClzAndStructLocSequence', 'YulBuiltinsAndEncodeSelectorSequence', 'ArrayStringParamsAndContextSequence', 'BytesMemoryAndAbiEncodeCallSequence', 'DynamicBytesAndStringReturnSequence', 'BytesAndStringStorageSequence', 'YulBlockMulmodTstoreSequence', 'MerkleAndNoncesSequence', 'MultiProofMappingKeysRatifiersSequence', 'UdvtParamAssignHashMarketSequence', 'StructMappingAndBytes4InterfaceSequence', 'ERC2981HoldersArraysMsgHashSequence', 'StorageStructParamsDequeShortStringsSequence', 'StorageSlotShortStringsTimeSequence', 'EnumerableSetMapSequence', 'CheckpointsAndStructArraysSequence', 'TickLibAndThreeKeyMappingSequence', 'OfferHashAndDomainSeparatorSequence', 'AbiDecodeAndRatifierSequence', 'VotesCheckpointsArraysBitMapsSequence', 'PublicGettersAndBuiltinsSequence', 'EcrecoverAuthorizerArraysMapSequence', 'MarketParamsBalancesSequence', 'MidnightPositionAndFeeSequence', 'TimelockAndBytes4CastSequence', 'StringBytesMappingsUriStorageStringsSequence', 'StringsHexArraysBitmapsSequence', 'EcdsaMerkleCheckpointsStorageSlotSequence'} else '3', + '--seed', '2490' if fixture in {'MappingFixedArraySequence', 'FixedArrayWriteOrderSequence', 'DiscardedHelperSequence', 'EncodedByteLocalSequence', 'NamedHelperReturnSequence', 'YulNumericSequence', 'Solc0810Sequence', 'InheritanceSequence', 'VoidHelperGuardSequence', 'ModifierUncheckedCompoundSequence', 'TupleHelperSequence', 'Int256ContractTypeSequence', 'FnPtrStructDeleteModifierSequence', 'EmptyArrayReturnBytesCalldataSequence', 'OverloadConstErrorCondTupleTloadSequence', 'StructFixedArrayAndFixedReturnSequence', 'MsgDataAndEnumSequence', 'ExpAndBitwiseShiftSequence', 'WhileClzAndStructLocSequence', 'YulBuiltinsAndEncodeSelectorSequence', 'ArrayStringParamsAndContextSequence', 'BytesMemoryAndAbiEncodeCallSequence', 'DynamicBytesAndStringReturnSequence', 'BytesAndStringStorageSequence', 'YulBlockMulmodTstoreSequence', 'MerkleAndNoncesSequence', 'MultiProofMappingKeysRatifiersSequence', 'UdvtParamAssignHashMarketSequence', 'StructMappingAndBytes4InterfaceSequence', 'ERC2981HoldersArraysMsgHashSequence', 'StorageStructParamsDequeShortStringsSequence', 'StorageSlotShortStringsTimeSequence', 'EnumerableSetMapSequence', 'CheckpointsAndStructArraysSequence', 'TickLibAndThreeKeyMappingSequence', 'OfferHashAndDomainSeparatorSequence', 'AbiDecodeAndRatifierSequence', 'VotesCheckpointsArraysBitMapsSequence', 'PublicGettersAndBuiltinsSequence', 'EcrecoverAuthorizerArraysMapSequence', 'MarketParamsBalancesSequence', 'MidnightPositionAndFeeSequence', 'TimelockAndBytes4CastSequence', 'StringBytesMappingsUriStorageStringsSequence', 'StringsHexArraysBitmapsSequence', 'EcdsaMerkleCheckpointsStorageSlotSequence'} else '2453', '--shrink-attempts', '100' if fixture in {'MappingFixedArraySequence', 'FixedArrayWriteOrderSequence', 'DiscardedHelperSequence', 'EncodedByteLocalSequence', 'NamedHelperReturnSequence', 'YulNumericSequence', 'Solc0810Sequence', 'InheritanceSequence', 'VoidHelperGuardSequence', 'ModifierUncheckedCompoundSequence', 'TupleHelperSequence', 'Int256ContractTypeSequence', 'FnPtrStructDeleteModifierSequence', 'EmptyArrayReturnBytesCalldataSequence', 'OverloadConstErrorCondTupleTloadSequence', 'StructFixedArrayAndFixedReturnSequence', 'MsgDataAndEnumSequence', 'ExpAndBitwiseShiftSequence', 'WhileClzAndStructLocSequence', 'YulBuiltinsAndEncodeSelectorSequence', 'ArrayStringParamsAndContextSequence', 'BytesMemoryAndAbiEncodeCallSequence', 'DynamicBytesAndStringReturnSequence', 'BytesAndStringStorageSequence', 'YulBlockMulmodTstoreSequence', 'MerkleAndNoncesSequence', 'MultiProofMappingKeysRatifiersSequence', 'UdvtParamAssignHashMarketSequence', 'StructMappingAndBytes4InterfaceSequence', 'ERC2981HoldersArraysMsgHashSequence', 'StorageStructParamsDequeShortStringsSequence', 'StorageSlotShortStringsTimeSequence', 'EnumerableSetMapSequence', 'CheckpointsAndStructArraysSequence', 'TickLibAndThreeKeyMappingSequence', 'OfferHashAndDomainSeparatorSequence', 'AbiDecodeAndRatifierSequence', 'VotesCheckpointsArraysBitMapsSequence', 'PublicGettersAndBuiltinsSequence', 'EcrecoverAuthorizerArraysMapSequence', 'MarketParamsBalancesSequence', 'MidnightPositionAndFeeSequence', 'TimelockAndBytes4CastSequence', 'StringBytesMappingsUriStorageStringsSequence', 'StringsHexArraysBitmapsSequence', 'EcdsaMerkleCheckpointsStorageSlotSequence'} else '30', '--output', str(output)] - if fixture in {'MappingFixedArraySequence', 'FixedArrayWriteOrderSequence', 'DiscardedHelperSequence', 'EncodedByteLocalSequence', 'NamedHelperReturnSequence', 'YulNumericSequence', 'Solc0810Sequence', 'InheritanceSequence', 'VoidHelperGuardSequence', 'ModifierUncheckedCompoundSequence', 'TupleHelperSequence', 'Int256ContractTypeSequence', 'FnPtrStructDeleteModifierSequence', 'EmptyArrayReturnBytesCalldataSequence', 'OverloadConstErrorCondTupleTloadSequence', 'StructFixedArrayAndFixedReturnSequence', 'MsgDataAndEnumSequence', 'ExpAndBitwiseShiftSequence', 'WhileClzAndStructLocSequence', 'YulBuiltinsAndEncodeSelectorSequence', 'ArrayStringParamsAndContextSequence', 'BytesMemoryAndAbiEncodeCallSequence', 'DynamicBytesAndStringReturnSequence', 'BytesAndStringStorageSequence', 'YulBlockMulmodTstoreSequence', 'MerkleAndNoncesSequence', 'MultiProofMappingKeysRatifiersSequence', 'UdvtParamAssignHashMarketSequence', 'StructMappingAndBytes4InterfaceSequence', 'ERC2981HoldersArraysMsgHashSequence', 'StorageStructParamsDequeShortStringsSequence', 'StorageSlotShortStringsTimeSequence', 'EnumerableSetMapSequence', 'CheckpointsAndStructArraysSequence', 'TickLibAndThreeKeyMappingSequence', 'OfferHashAndDomainSeparatorSequence', 'AbiDecodeAndRatifierSequence', 'VotesCheckpointsArraysBitMapsSequence', 'PublicGettersAndBuiltinsSequence', 'EcrecoverAuthorizerArraysMapSequence', 'MarketParamsBalancesSequence', 'MidnightPositionAndFeeSequence', 'TimelockAndBytes4CastSequence', 'StringBytesMappingsUriStorageStringsSequence', 'StringsHexArraysBitmapsSequence'}: - argv.extend(['--change-prefix', *map(str, list(range(9)) + ([19, 20, 21, 25, 30, 40] if fixture in {'FixedArrayWriteOrderSequence', 'DiscardedHelperSequence', 'EncodedByteLocalSequence', 'NamedHelperReturnSequence', 'YulNumericSequence', 'Solc0810Sequence', 'InheritanceSequence', 'VoidHelperGuardSequence', 'ModifierUncheckedCompoundSequence', 'TupleHelperSequence', 'Int256ContractTypeSequence', 'FnPtrStructDeleteModifierSequence', 'EmptyArrayReturnBytesCalldataSequence', 'OverloadConstErrorCondTupleTloadSequence', 'StructFixedArrayAndFixedReturnSequence', 'MsgDataAndEnumSequence', 'ExpAndBitwiseShiftSequence', 'WhileClzAndStructLocSequence', 'YulBuiltinsAndEncodeSelectorSequence', 'ArrayStringParamsAndContextSequence', 'BytesMemoryAndAbiEncodeCallSequence', 'DynamicBytesAndStringReturnSequence', 'BytesAndStringStorageSequence', 'YulBlockMulmodTstoreSequence', 'MerkleAndNoncesSequence', 'MultiProofMappingKeysRatifiersSequence', 'UdvtParamAssignHashMarketSequence', 'StructMappingAndBytes4InterfaceSequence', 'ERC2981HoldersArraysMsgHashSequence', 'StorageStructParamsDequeShortStringsSequence', 'StorageSlotShortStringsTimeSequence', 'EnumerableSetMapSequence', 'CheckpointsAndStructArraysSequence', 'TickLibAndThreeKeyMappingSequence', 'OfferHashAndDomainSeparatorSequence', 'AbiDecodeAndRatifierSequence', 'VotesCheckpointsArraysBitMapsSequence', 'PublicGettersAndBuiltinsSequence', 'EcrecoverAuthorizerArraysMapSequence', 'MarketParamsBalancesSequence', 'MidnightPositionAndFeeSequence', 'TimelockAndBytes4CastSequence', 'StringBytesMappingsUriStorageStringsSequence', 'StringsHexArraysBitmapsSequence'} else [65535, 65536]) + [(1 << 256) - 1])]) + if fixture in {'MappingFixedArraySequence', 'FixedArrayWriteOrderSequence', 'DiscardedHelperSequence', 'EncodedByteLocalSequence', 'NamedHelperReturnSequence', 'YulNumericSequence', 'Solc0810Sequence', 'InheritanceSequence', 'VoidHelperGuardSequence', 'ModifierUncheckedCompoundSequence', 'TupleHelperSequence', 'Int256ContractTypeSequence', 'FnPtrStructDeleteModifierSequence', 'EmptyArrayReturnBytesCalldataSequence', 'OverloadConstErrorCondTupleTloadSequence', 'StructFixedArrayAndFixedReturnSequence', 'MsgDataAndEnumSequence', 'ExpAndBitwiseShiftSequence', 'WhileClzAndStructLocSequence', 'YulBuiltinsAndEncodeSelectorSequence', 'ArrayStringParamsAndContextSequence', 'BytesMemoryAndAbiEncodeCallSequence', 'DynamicBytesAndStringReturnSequence', 'BytesAndStringStorageSequence', 'YulBlockMulmodTstoreSequence', 'MerkleAndNoncesSequence', 'MultiProofMappingKeysRatifiersSequence', 'UdvtParamAssignHashMarketSequence', 'StructMappingAndBytes4InterfaceSequence', 'ERC2981HoldersArraysMsgHashSequence', 'StorageStructParamsDequeShortStringsSequence', 'StorageSlotShortStringsTimeSequence', 'EnumerableSetMapSequence', 'CheckpointsAndStructArraysSequence', 'TickLibAndThreeKeyMappingSequence', 'OfferHashAndDomainSeparatorSequence', 'AbiDecodeAndRatifierSequence', 'VotesCheckpointsArraysBitMapsSequence', 'PublicGettersAndBuiltinsSequence', 'EcrecoverAuthorizerArraysMapSequence', 'MarketParamsBalancesSequence', 'MidnightPositionAndFeeSequence', 'TimelockAndBytes4CastSequence', 'StringBytesMappingsUriStorageStringsSequence', 'StringsHexArraysBitmapsSequence', 'EcdsaMerkleCheckpointsStorageSlotSequence'}: + argv.extend(['--change-prefix', *map(str, list(range(9)) + ([19, 20, 21, 25, 30, 40] if fixture in {'FixedArrayWriteOrderSequence', 'DiscardedHelperSequence', 'EncodedByteLocalSequence', 'NamedHelperReturnSequence', 'YulNumericSequence', 'Solc0810Sequence', 'InheritanceSequence', 'VoidHelperGuardSequence', 'ModifierUncheckedCompoundSequence', 'TupleHelperSequence', 'Int256ContractTypeSequence', 'FnPtrStructDeleteModifierSequence', 'EmptyArrayReturnBytesCalldataSequence', 'OverloadConstErrorCondTupleTloadSequence', 'StructFixedArrayAndFixedReturnSequence', 'MsgDataAndEnumSequence', 'ExpAndBitwiseShiftSequence', 'WhileClzAndStructLocSequence', 'YulBuiltinsAndEncodeSelectorSequence', 'ArrayStringParamsAndContextSequence', 'BytesMemoryAndAbiEncodeCallSequence', 'DynamicBytesAndStringReturnSequence', 'BytesAndStringStorageSequence', 'YulBlockMulmodTstoreSequence', 'MerkleAndNoncesSequence', 'MultiProofMappingKeysRatifiersSequence', 'UdvtParamAssignHashMarketSequence', 'StructMappingAndBytes4InterfaceSequence', 'ERC2981HoldersArraysMsgHashSequence', 'StorageStructParamsDequeShortStringsSequence', 'StorageSlotShortStringsTimeSequence', 'EnumerableSetMapSequence', 'CheckpointsAndStructArraysSequence', 'TickLibAndThreeKeyMappingSequence', 'OfferHashAndDomainSeparatorSequence', 'AbiDecodeAndRatifierSequence', 'VotesCheckpointsArraysBitMapsSequence', 'PublicGettersAndBuiltinsSequence', 'EcrecoverAuthorizerArraysMapSequence', 'MarketParamsBalancesSequence', 'MidnightPositionAndFeeSequence', 'TimelockAndBytes4CastSequence', 'StringBytesMappingsUriStorageStringsSequence', 'StringsHexArraysBitmapsSequence', 'EcdsaMerkleCheckpointsStorageSlotSequence'} else [65535, 65536]) + [(1 << 256) - 1])]) if fixture == 'Solc0810Sequence': argv = argv[:argv.index('--change-prefix')] + ['--solc-version', '0.8.10', '--change-prefix', *map(str, [0, 1, 2, 3, 19, 20, 21, 100, 1000, 50000, 100000, 999999, (1 << 256) - 1])] if fixture == 'YulNumericSequence': @@ -491,7 +497,7 @@ def run(directory, output, name): if fixture == 'NamedHelperReturnSequence': prefix = argv.index('--change-prefix') argv = argv[:prefix] + ['--change-prefix', *map(str, [0, 1, 2, 3, 19, 20, 21, 30, 31, 40, 50, 60, 70, 255, 256, 257, (1 << 160) - 1, 1 << 160, (1 << 160) + 1, (1 << 256) - 1])] - if fixture in {'VoidHelperGuardSequence', 'ModifierUncheckedCompoundSequence', 'TupleHelperSequence', 'Int256ContractTypeSequence', 'FnPtrStructDeleteModifierSequence', 'OverloadConstErrorCondTupleTloadSequence', 'StructFixedArrayAndFixedReturnSequence', 'MsgDataAndEnumSequence', 'ExpAndBitwiseShiftSequence', 'WhileClzAndStructLocSequence', 'YulBuiltinsAndEncodeSelectorSequence', 'ArrayStringParamsAndContextSequence', 'BytesMemoryAndAbiEncodeCallSequence', 'DynamicBytesAndStringReturnSequence', 'BytesAndStringStorageSequence', 'YulBlockMulmodTstoreSequence', 'MerkleAndNoncesSequence', 'MultiProofMappingKeysRatifiersSequence', 'UdvtParamAssignHashMarketSequence', 'StructMappingAndBytes4InterfaceSequence', 'ERC2981HoldersArraysMsgHashSequence', 'StorageStructParamsDequeShortStringsSequence', 'StorageSlotShortStringsTimeSequence', 'EnumerableSetMapSequence', 'CheckpointsAndStructArraysSequence', 'TickLibAndThreeKeyMappingSequence', 'OfferHashAndDomainSeparatorSequence', 'AbiDecodeAndRatifierSequence', 'VotesCheckpointsArraysBitMapsSequence', 'PublicGettersAndBuiltinsSequence', 'EcrecoverAuthorizerArraysMapSequence', 'MarketParamsBalancesSequence', 'MidnightPositionAndFeeSequence', 'TimelockAndBytes4CastSequence', 'StringBytesMappingsUriStorageStringsSequence', 'StringsHexArraysBitmapsSequence'}: + if fixture in {'VoidHelperGuardSequence', 'ModifierUncheckedCompoundSequence', 'TupleHelperSequence', 'Int256ContractTypeSequence', 'FnPtrStructDeleteModifierSequence', 'OverloadConstErrorCondTupleTloadSequence', 'StructFixedArrayAndFixedReturnSequence', 'MsgDataAndEnumSequence', 'ExpAndBitwiseShiftSequence', 'WhileClzAndStructLocSequence', 'YulBuiltinsAndEncodeSelectorSequence', 'ArrayStringParamsAndContextSequence', 'BytesMemoryAndAbiEncodeCallSequence', 'DynamicBytesAndStringReturnSequence', 'BytesAndStringStorageSequence', 'YulBlockMulmodTstoreSequence', 'MerkleAndNoncesSequence', 'MultiProofMappingKeysRatifiersSequence', 'UdvtParamAssignHashMarketSequence', 'StructMappingAndBytes4InterfaceSequence', 'ERC2981HoldersArraysMsgHashSequence', 'StorageStructParamsDequeShortStringsSequence', 'StorageSlotShortStringsTimeSequence', 'EnumerableSetMapSequence', 'CheckpointsAndStructArraysSequence', 'TickLibAndThreeKeyMappingSequence', 'OfferHashAndDomainSeparatorSequence', 'AbiDecodeAndRatifierSequence', 'VotesCheckpointsArraysBitMapsSequence', 'PublicGettersAndBuiltinsSequence', 'EcrecoverAuthorizerArraysMapSequence', 'MarketParamsBalancesSequence', 'MidnightPositionAndFeeSequence', 'TimelockAndBytes4CastSequence', 'StringBytesMappingsUriStorageStringsSequence', 'StringsHexArraysBitmapsSequence', 'EcdsaMerkleCheckpointsStorageSlotSequence'}: prefix = argv.index('--change-prefix') argv = argv[:prefix] + ['--change-prefix', *map(str, [19, 0, 1, 2, 3, 20, 21, 96, 97, 98, 99999, 100000, (1 << 256) - 1])] if fixture == 'MidnightPositionAndFeeSequence': @@ -514,6 +520,11 @@ def run(directory, output, name): argv[tx_idx + 1] = '18' prefix = argv.index('--change-prefix') argv = argv[:prefix] + ['--change-prefix', *map(str, [0, 1, 2, 4, 15, 20, 21])] + if fixture == 'EcdsaMerkleCheckpointsStorageSlotSequence': + tx_idx = argv.index('--transactions') + argv[tx_idx + 1] = '24' + prefix = argv.index('--change-prefix') + argv = argv[:prefix] + ['--change-prefix', *map(str, [0, 1, 2, 3, 4, 5, 6, 20])] if fixture == 'EmptyArrayReturnBytesCalldataSequence': prefix = argv.index('--change-prefix') argv = argv[:prefix] + ['--change-prefix', *map(str, [0, 1, 2, 3, 16, 17, 18, (1 << 256) - 1])] @@ -1017,6 +1028,18 @@ def helper_order_control(directory, name, mutated): return uint256(uint8(HEX_DIGITS[y = 1])); } } +''') + elif name == 'import-ecdsa-merkle-checkpoints-storage-slot-unaligned-byte-mload-guard': + diagnostic = 'unsupported Yul builtin mload' + (target / 'Fixture.sol').write_text('''pragma solidity 0.8.34; +contract C { + function checked(uint256 x) external pure returns (uint256 r) { + bytes memory sig = abi.encode(x); + assembly { + r := mload(add(sig, 0x10)) + } + } +} ''') else: argument = name.endswith('argument-guard') @@ -1107,7 +1130,8 @@ def mutation_campaign(output, selected=None): 'import-midnight-position-and-fee-member-key-stateful-rhs-guard', 'import-timelock-and-bytes4-cast-encode-stateful-bytes-guard', 'import-string-bytes-mappings-uri-storage-strings-mapping-write-stateful-rhs-guard', - 'import-strings-hex-arrays-bitmaps-stateful-fixed-bytes-index-guard'} + 'import-strings-hex-arrays-bitmaps-stateful-fixed-bytes-index-guard', + 'import-ecdsa-merkle-checkpoints-storage-slot-unaligned-byte-mload-guard'} if order_guard: helper_order_control(directory, name, False) source = directory / ('Compiler/SolidityImport/SequenceRunner.lean' if name.startswith('observe-event-') diff --git a/scripts/solidity_differential/check_storage_rejections.py b/scripts/solidity_differential/check_storage_rejections.py index cfb91b48f..e995e1f9e 100644 --- a/scripts/solidity_differential/check_storage_rejections.py +++ b/scripts/solidity_differential/check_storage_rejections.py @@ -1288,6 +1288,26 @@ def main(): None, '{ evmVersion := "osaka", viaIR := true, optimizerRuns := some 466, bytecodeHash := "none" }', 'FunctionCall: [solidity-import:unsupported] unsupported cast source bytes16 for bytes1'), + ('ecdsa-merkle-checkpoints-storage-slot-positive', + (root / 'Contracts/SolidityImportSmoke/EcdsaMerkleCheckpointsStorageSlotSequence.sol').read_text().replace('contract SequenceFixture', 'contract C').replace('function change(', 'function checked('), + None, + '{ evmVersion := "osaka", viaIR := true, optimizerRuns := some 466, bytecodeHash := "none" }', + None), + ('ecdsa-merkle-checkpoints-storage-slot-unaligned-byte-mload-rejected', + "pragma solidity 0.8.34;\ncontract C {\n function checked(uint256 x) external pure returns (uint256 r) {\n bytes memory sig = abi.encode(x);\n assembly {\n r := mload(add(sig, 0x10))\n }\n }\n}\n", + None, + '{ evmVersion := "osaka", viaIR := true, optimizerRuns := some 466, bytecodeHash := "none" }', + 'YulFunctionCall: [solidity-import:unsupported] unsupported Yul builtin mload'), + ('ecdsa-merkle-checkpoints-storage-slot-zero-offset-byte-mload-rejected', + "pragma solidity 0.8.34;\ncontract C {\n function checked(uint256 x) external pure returns (uint256 r) {\n bytes memory sig = abi.encode(x);\n assembly {\n r := mload(add(sig, 0))\n }\n }\n}\n", + None, + '{ evmVersion := "osaka", viaIR := true, optimizerRuns := some 466, bytecodeHash := "none" }', + 'YulFunctionCall: [solidity-import:unsupported] unsupported Yul builtin mload'), + ('ecdsa-merkle-checkpoints-storage-slot-unbounded-narrow-yul-assign-rejected', + "pragma solidity 0.8.34;\ncontract C {\n function checked(uint256 x) external pure returns (uint256) {\n bytes memory sig = abi.encode(x);\n uint8 v;\n assembly {\n v := mload(add(sig, 0x20))\n }\n return uint256(v);\n }\n}\n", + None, + '{ evmVersion := "osaka", viaIR := true, optimizerRuns := some 466, bytecodeHash := "none" }', + 'YulAssignment: [solidity-import:unsupported] Yul assignment to narrow local v is unsupported'), ] for name, source_text, dep_text, profile_text, expected in solc_0810_cases: if args.only and args.only not in name: @@ -1328,6 +1348,7 @@ def main(): else 'checked(uint256)\n function supportsInterface(bytes4)\n function hashOperation(address,uint256,bytes,bytes32,bytes32)\n function getTimestamp(bytes32)\n function getOperationState(bytes32)\n function isOperation(bytes32)\n function isOperationPending(bytes32)\n function isOperationReady(bytes32)\n function isOperationDone(bytes32)\n function getMinDelay()' if name == 'timelock-and-bytes4-cast-positive' else 'checked(uint256)\n function tokenURI(uint256)\n function publicTokenURIs(uint256)\n function scopedPayloads(address,uint256)\n function formatDecimal(uint256)\n function formatHex(uint256)\n function formatAddress(address)\n function readFallbackTag()\n function readFallbackTagLength()' if name == 'string-bytes-mappings-uri-storage-strings-positive' else 'checked(uint256)\n function formatHex(uint256)\n function formatHexFixed(uint256,uint256)\n function formatAddressHex(address)\n function formatSignedDecimal(int256)\n function checkStringEqual(string,string)\n function upperBound(uint256)\n function bitmapBit(uint256)' if name == 'strings-hex-arrays-bitmaps-positive' + else 'checked(uint256)\n function recoverFromBytes(bytes32,bytes)\n function recoverFromCompact(bytes32,bytes32,bytes32)\n function verifyMerkle(«bytes32[]»,bytes32,bytes32)\n function rawSlotLabel()\n function rawSlotPayload()\n function checkpointUpperRecent(uint32)' if name == 'ecdsa-merkle-checkpoints-storage-slot-positive' else 'checked(uint256)' ) driver = directory / 'Check.lean' diff --git a/scripts/solidity_differential/programs.py b/scripts/solidity_differential/programs.py index bf8994a95..ceef0ac0d 100644 --- a/scripts/solidity_differential/programs.py +++ b/scripts/solidity_differential/programs.py @@ -2254,3 +2254,36 @@ def stateful_strings_hex_arrays_bitmaps_source(fixture: str, variant: str) -> st return fixture raise ValueError(f'unknown strings-hex-arrays-bitmaps variant: {variant}') + +def stateful_ecdsa_merkle_checkpoints_storage_slot_source(fixture: str, variant: str) -> str: + if variant == 'baseline': + return fixture + if variant == 'renamed': + import re + names = { + 'RAW_LABEL_SLOT', 'RAW_PAYLOAD_SLOT', + '_trace', '_fallbackLabel', '_totalWeight', '_lastRecoveredHash', + '_throwError', '_hashPair', '_insert', '_upperBinaryLookup', '_lowerBinaryLookup', '_unsafeAccess', + 'stepKey', 'stepVal', 'newVal', 'msgHash', 'sig65', 'signer1', 'signer2', + 'badSig', 'badErr', 'badArg', 'labelSlot', 'payloadSlot', 'payloadLen', + 'recentVal', 'lowerVal', 'sibling', 'leaf', 'pairRoot', + } + token = r'//[^\n]*|/\*[\s\S]*?\*/|"(?:\\.|[^"\\])*"|\'(?:\\.|[^\'\\])*\'|[A-Za-z_$][A-Za-z0-9_$]*' + return re.sub(token, lambda m: m.group(0) + '_renamed' + if m.group(0) in names else m.group(0), fixture) + if variant == 'expanded-ecdsa-merkle-checkpoints-storage-slot': + replacements = { + 'uint8 v = (input & 1) == 0 ? 27 : 28;': + 'uint8 v = (input & 1) != 0 ? 28 : 27;', + 'delete payloadSlot.value;': + 'payloadSlot.value = "";', + '_totalWeight += 777;': + '_totalWeight = _totalWeight + 777;', + } + for before, after in replacements.items(): + if fixture.count(before) != 1: + raise ValueError('ecdsa-merkle-checkpoints-storage-slot variant anchor changed') + fixture = fixture.replace(before, after) + return fixture + raise ValueError(f'unknown ecdsa-merkle-checkpoints-storage-slot variant: {variant}') +