diff --git a/Compiler/SolidityImport/Import.lean b/Compiler/SolidityImport/Import.lean index a833b45d4..6132c0132 100644 --- a/Compiler/SolidityImport/Import.lean +++ b/Compiler/SolidityImport/Import.lean @@ -3523,12 +3523,27 @@ private partial def lowerRef (j : Json) : M Ref := do else if let some decl := env.numericConstants.find? n then if env.constantStack.contains n then failAt j "cyclic constant initializer" let declared ← mType decl + let initializer ← mField decl "value" + if declared.startsWith "bytes" then + if let some byteW := (declared.drop 5).toNat? then + if 1 ≤ byteW && byteW ≤ 32 && (← mKind initializer) == "Literal" && + (optStr initializer "kind" == some "string" || + optStr initializer "kind" == some "unicodeString" || + optStr initializer "kind" == some "hexString") then + let hex ← mStr (← mField initializer "hexValue") + unless hex.length % 2 == 0 && hex.length / 2 ≤ byteW do + failAt initializer s!"fixed-bytes literal constant exceeds {declared}" + let word ← if hex.isEmpty then pure 0 else do + let some v := Compiler.Hex.parseHexNat? ("0x" ++ hex) + | failAt initializer s!"invalid hexValue {hex}" + pure v + let aligned := word * 16 ^ (64 - hex.length) + return .expr { pre := #[], expr := .literal aligned } unless (declared.startsWith "uint" && (bitsOf declared).isSome) || declared == "bool" || declared == "bytes32" || declared == "bytes4" || declared == "int256" || declared == "int" || declared == "address" || declared == "address payable" do failAt j s!"unsupported numeric constant type {declared}" - let initializer ← mField decl "value" modify fun e => { e with constantStack := n :: e.constantStack } let rawValue ← lowerExpr initializer let value ← convert declared (← mType initializer) rawValue initializer @@ -3791,6 +3806,22 @@ private partial def lowerRef (j : Json) : M Ref := do let pre := (pre ++ key.pre).push (.ite (.lt key.expr (.localVar arr.lengthBinding)) [] [.panicCode (.literal 0x32)]) let value := Expr.mload (.add (.add (.localVar arr.memoryPointer) (.literal 32)) (.mul key.expr (.literal 32))) return .expr { pre, expr := value } + | .expr baseVal => + let baseTy ← mType baseExpression + if baseTy.startsWith "bytes" then + if let some byteW := (baseTy.drop 5).toNat? then + if 1 ≤ byteW && byteW ≤ 32 then + if statefulCallIn baseExpression (← get) || statefulCallIn indexExpression (← get) || + assignmentIn baseExpression || assignmentIn indexExpression then + failAt j "stateful or assignment fixed-bytes index is unsupported" + let idxTy ← mType indexExpression + unless (idxTy.startsWith "uint" && (bitsOf idxTy).isSome) || + (idxTy.startsWith "int_const" && !idxTy.startsWith "int_const -") do + failAt indexExpression "fixed-bytes index must be unsigned" + let bAtom ← atom baseVal + let pre := bAtom.pre ++ key.pre ++ #[.ite (.lt key.expr (.literal byteW)) [] [.panicCode (.literal 0x32)]] + return .expr { pre, expr := .shl (.literal 248) (.byte key.expr bAtom.expr) } + failAt j "index of a non-mapping or unsupported ABI value" | _ => failAt j "index of a non-mapping or unsupported ABI value" | "MemberAccess" => let member ← mStr (← mField j "memberName") @@ -4634,6 +4665,19 @@ private partial def lowerCast (j : Json) : M Val := do (src == "bytes" || src == "bytes memory" || src == "bytes calldata" || src == "bytes storage ref" || src == "bytes storage pointer") then return ← lowerBytesToFixedBytes args[0]! (if tname == "bytes32" then 32 else 4) j + if tname == "bytes1" then + let innerArg ← stripParens args[0]! + if (← mKind innerArg) == "Literal" then + let kind ← mStr (← mField innerArg "kind") + if kind == "string" || kind == "unicodeString" || kind == "hexString" then + let hex ← mStr (← mField innerArg "hexValue") + unless hex.length == 2 || hex.length == 0 do + failAt j s!"bytes1 string literal cast requires at most 1 byte, found {hex.length / 2}" + let byteVal ← if hex.isEmpty then pure 0 else + match Compiler.Hex.parseHexNat? ("0x" ++ hex) with + | some n => pure n + | none => failAt j "invalid bytes1 literal hexValue" + return { pre := #[], expr := .literal (byteVal * 2 ^ 248) } let v ← lowerExpr args[0]! if src.startsWith "int" && src != "int256" && src != "int" && !src.startsWith "int_const" then failAt j s!"unsupported cast source {src}" @@ -4642,6 +4686,41 @@ private partial def lowerCast (j : Json) : M Val := do (src.startsWith "uint" && (bitsOf src).isSome) do failAt j s!"unsupported cast source {src} for {tname}" return v + if tname == "bytes1" then + if src == "bytes1" then + return v + else if src == "uint8" then + let a ← atom v + let dest ← fresh + let shifted := Stmt.letVar dest (.shl (.literal 248) (.bitAnd a.expr (.literal 0xff))) + return { pre := a.pre.push shifted, expr := .localVar dest } + else if src == "bytes32" || src == "bytes4" then + let a ← atom v + let dest ← fresh + let bound := Stmt.letVar dest (.bitAnd a.expr (.literal (0xff * 2 ^ 248))) + return { pre := a.pre.push bound, expr := .localVar dest } + else if src.startsWith "int_const" && !src.startsWith "int_const -" then + let .literal n := v.expr + | failAt j s!"unsupported cast source {src} for bytes1" + let innerArg ← stripParens args[0]! + let raw := optStr innerArg "value" |>.getD "" + let hexDigits := ((raw.drop 2).toString.splitOn "_").foldl (· ++ ·) "" + unless v.pre.isEmpty && n < 256 && + (n == 0 || (raw.startsWith "0x" && hexDigits.length == 2)) do + failAt j s!"unsupported cast source {src} for bytes1" + return { pre := #[], expr := .literal (n * 2 ^ 248) } + else + failAt j s!"unsupported cast source {src} for bytes1" + if src == "bytes1" then + if tname == "bytes32" || tname == "bytes4" then + return v + else if tname == "uint8" then + let a ← atom v + let dest ← fresh + let shifted := Stmt.letVar dest (.shr (.literal 248) a.expr) + return { pre := a.pre.push shifted, expr := .localVar dest } + else + failAt j s!"unsupported cast target {tname} from bytes1" if tname == "bytes4" then if src == "bytes4" then return v @@ -8818,15 +8897,64 @@ private partial def lowerFor (s : Json) (lowerBody : Json → M (Array Stmt)) : let counter ← mNat (← mField d "id") let counterName ← mStr (← mField d "name") unless (← mType d) == "uint256" do failAt d "a for loop counter must be uint256" - if let some start := (field? init "initialValue").filter (!·.isNull) then - unless (← mType start) == "int_const 0" do failAt start "a for loop counter must start at 0" let body ← mField s "body" let writes := bodyAssignedIds body - if writes.contains counter then - failAt d "a for loop counter must not be assigned in the loop body" let isCounter (j : Json) : M Bool := do if (← mKind j) != "Identifier" then return false pure ((← refInt j) == counter) + let cond ← mField s "condition" + let isDecrementFor ← if (← mKind cond) == "BinaryOperation" && optStr cond "operator" == some ">" then + isCounter (← mField cond "leftExpression") + else + pure false + if isDecrementFor && !writes.contains counter then + let some startNode := (field? init "initialValue").filter (!·.isNull) + | failAt init "a decrementing for loop counter must have an initial value" + let step ← mField (← mField s "loopExpression") "expression" + let stepOk ← match ← mKind step with + | "UnaryOperation" => + pure (optStr step "operator" == some "--" && (← isCounter (← mField step "subExpression"))) + | "Assignment" => + pure (optStr step "operator" == some "-=" && (← isCounter (← mField step "leftHandSide")) && + (← mType (← mField step "rightHandSide")) == "int_const 1") + | _ => pure false + unless stepOk do failAt step "a decrementing for loop must decrement its counter by one" + let startVal ← atom (← lowerExpr startNode) + let lowerNode ← mField cond "rightExpression" + let lowerVal ← lowerExpr lowerNode + let lowerInvariant ← match lowerVal.expr with + | .literal _ | .param _ => pure true + | .localVar _ => + if (← mKind lowerNode) == "Identifier" then + pure (!writes.contains (← refInt lowerNode).toNat) + else pure false + | _ => pure false + unless lowerVal.pre.isEmpty && lowerInvariant do + failAt lowerNode "a for loop bound must be a literal, a parameter or an unassigned local" + let countBinding ← fresh + let iterIdx ← fresh + let decBinding ← freshFor counterName + let saved ← get + modify fun e => + { e with values := e.values.insert counter (.localVar decBinding), + yulNames := e.yulNames.insert counterName (.localVar decBinding) } + let bodyOut ← lowerBody body + modify fun e => + { e with values := saved.values, paths := saved.paths, + snapshots := saved.snapshots, mems := saved.mems, abiElements := saved.abiElements, calldataBytes := saved.calldataBytes, scalarArrays := saved.scalarArrays, byteBuffers := saved.byteBuffers, stringBuffers := saved.stringBuffers, storageBytesVars := saved.storageBytesVars, storageDynamicArrayVars := saved.storageDynamicArrayVars, flatStructs := saved.flatStructs, scalarTy := saved.scalarTy, + writableLocals := saved.writableLocals, zeroInitLocals := saved.zeroInitLocals.filter (!writes.contains ·), fnPtrs := saved.fnPtrs, yulNames := saved.yulNames, yulMemoryArrays := saved.yulMemoryArrays, yulMemoryStructs := saved.yulMemoryStructs } + let loopBodyStmts : List Stmt := + [.letVar decBinding (.sub startVal.expr (.localVar iterIdx))] ++ bodyOut.toList + return startVal.pre ++ #[ + .letVar countBinding (.literal 0), + .ite (.gt startVal.expr lowerVal.expr) + [.assignVar countBinding (.sub startVal.expr lowerVal.expr)] [], + .forEach iterIdx (.localVar countBinding) loopBodyStmts + ] + if let some start := (field? init "initialValue").filter (!·.isNull) then + unless (← mType start) == "int_const 0" do failAt start "a for loop counter must start at 0" + if writes.contains counter then + failAt d "a for loop counter must not be assigned in the loop body" let step ← mField (← mField s "loopExpression") "expression" let stepOk ← match ← mKind step with | "UnaryOperation" => @@ -8836,7 +8964,6 @@ private partial def lowerFor (s : Json) (lowerBody : Json → M (Array Stmt)) : (← mType (← mField step "rightHandSide")) == "int_const 1") | _ => pure false unless stepOk do failAt step "a for loop must increment its counter by one" - let cond ← mField s "condition" unless (← mKind cond) == "BinaryOperation" && optStr cond "operator" == some "<" do failAt cond "a for loop condition must be counter < bound" unless ← isCounter (← mField cond "leftExpression") do @@ -10368,6 +10495,47 @@ private partial def lowerEffect (statement : Json) : M (Array Stmt) := do return (value.pre ++ key.pre).push (.ite (.lt key.expr (.localVar arr.lengthBinding)) [] [.panicCode (.literal 0x32)]) |>.push (.mstore (.add (.add (.localVar arr.memoryPointer) (.literal 32)) (.mul key.expr (.literal 32))) stored) + let baseName ← mStr (← mField baseNode "name") + if let some buf := (← get).byteBuffers.find? baseId.toNat then + if (← get).yulNames.contains baseName then + let indexExpression ← mField target "indexExpression" + if statefulCallIn indexExpression (← get) || assignmentIn indexExpression then + failAt target "stateful or assignment array index is unsupported" + let indexTy ← mType indexExpression + unless indexTy.startsWith "uint" || indexTy.startsWith "int_const" do + failAt target "byte buffer index must be unsigned" + let value ← if deleting then pure ({ pre := #[], expr := (.literal 0 : Expr) } : Val) else do + let right ← mField expression "rightHandSide" + let innerRight ← stripParens right + if (← mKind innerRight) == "Literal" then + let rkind ← mStr (← mField innerRight "kind") + if rkind == "string" || rkind == "unicodeString" || rkind == "hexString" then + let hex ← mStr (← mField innerRight "hexValue") + unless hex.length == 2 || hex.length == 0 do + failAt right s!"bytes1 string literal requires at most 1 byte, found {hex.length / 2}" + let byteVal ← if hex.isEmpty then pure 0 else + match Compiler.Hex.parseHexNat? ("0x" ++ hex) with + | some n => pure n + | none => failAt right "invalid bytes1 literal hexValue" + pure ({ pre := #[], expr := .literal (byteVal * 2 ^ 248) } : Val) + else + failAt right "byte buffer element assignment requires a bytes1 value" + else + let rTy ← mType right + unless rTy == "bytes1" do + failAt right s!"byte buffer element assignment requires a bytes1 value, found {rTy}" + atom (← lowerExpr right) + let key ← atom (← lowerExpr indexExpression) + let addr := Expr.add buf.pointer key.expr + let wordAddr := AbiEncoding.byteWordOffset addr + let shiftBits := Expr.mul (.sub (.literal 31) (AbiEncoding.byteLane addr)) (.literal 8) + let topByte := Expr.bitAnd (.shr (.literal 248) value.expr) (.literal 0xff) + let byteMask := Expr.shl shiftBits (.literal 0xff) + let clearedWord := Expr.bitAnd (.mload wordAddr) (.bitNot byteMask) + let updatedWord := if deleting then clearedWord else Expr.bitOr clearedWord (.shl shiftBits topByte) + return (value.pre ++ key.pre).push (.ite (.lt key.expr buf.size) + [] [.panicCode (.literal 0x32)]) |>.push + (.mstore wordAddr updatedWord) let reference ← lowerRef target if let .fixedElement pre path index := reference then -- Under the pinned via-IR profile, assignment evaluates and captures @@ -11461,7 +11629,12 @@ private partial def lowerLocal (s : Json) : M (Array Stmt) := do pure ((← mArr (← mField init "names")).isEmpty && (← mKind (← mField init "expression")) == "NewExpression") else pure false - if isNewBytesInit && (← get).unchecked then + let isNewBytesBinaryLen ← if isNewBytesInit then do + let args ← mArr (← mField init "arguments") + if args.size == 1 then pure ((← mKind (← stripParens args[0]!)) == "BinaryOperation") else pure false + else + pure false + if isNewBytesInit && ((← get).unchecked || isNewBytesBinaryLen) then let initTy ← mType init let expectedBase := if isString then "string" else "bytes" unless initTy == expectedBase || initTy == expectedBase ++ " memory" do diff --git a/Contracts/SolidityImportSmoke/StringsHexArraysBitmapsSequence.sol b/Contracts/SolidityImportSmoke/StringsHexArraysBitmapsSequence.sol new file mode 100644 index 000000000..b4dd7d35e --- /dev/null +++ b/Contracts/SolidityImportSmoke/StringsHexArraysBitmapsSequence.sol @@ -0,0 +1,354 @@ +// SPDX-License-Identifier: MIT +pragma solidity 0.8.34; + +library MathSlice39 { + function average(uint256 a, uint256 b) internal pure returns (uint256) { + return (a & b) + (a ^ b) / 2; + } + + function log10(uint256 value) internal pure returns (uint256) { + uint256 result = 0; + unchecked { + if (value >= 10 ** 64) { + value /= 10 ** 64; + result += 64; + } + if (value >= 10 ** 32) { + value /= 10 ** 32; + result += 32; + } + if (value >= 10 ** 16) { + value /= 10 ** 16; + result += 16; + } + if (value >= 10 ** 8) { + value /= 10 ** 8; + result += 8; + } + if (value >= 10 ** 4) { + value /= 10 ** 4; + result += 4; + } + if (value >= 10 ** 2) { + value /= 10 ** 2; + result += 2; + } + if (value >= 10 ** 1) { + result += 1; + } + } + return result; + } + + function log256(uint256 value) internal pure returns (uint256) { + uint256 result = 0; + uint256 isGt; + unchecked { + isGt = value > (1 << 128) - 1 ? 1 : 0; + value >>= isGt * 128; + result += isGt * 16; + + isGt = value > (1 << 64) - 1 ? 1 : 0; + value >>= isGt * 64; + result += isGt * 8; + + isGt = value > (1 << 32) - 1 ? 1 : 0; + value >>= isGt * 32; + result += isGt * 4; + + isGt = value > (1 << 16) - 1 ? 1 : 0; + value >>= isGt * 16; + result += isGt * 2; + + result += value > (1 << 8) - 1 ? 1 : 0; + } + return result; + } +} + +library SignedMathSlice39 { + function abs(int256 n) internal pure returns (uint256) { + unchecked { + int256 mask = n >> 255; + return uint256((n + mask) ^ mask); + } + } +} + +library StorageSlotSlice39 { + struct AddressSlot { + address value; + } + + struct Uint256Slot { + uint256 value; + } + + function getAddressSlot(bytes32 slot) internal pure returns (AddressSlot storage r) { + assembly ("memory-safe") { + r.slot := slot + } + } + + function getUint256Slot(bytes32 slot) internal pure returns (Uint256Slot storage r) { + assembly ("memory-safe") { + r.slot := slot + } + } +} + +library ArraysSlice39 { + using StorageSlotSlice39 for bytes32; + + function findUpperBound(uint256[] storage array, uint256 element) internal view returns (uint256) { + uint256 low = 0; + uint256 high = array.length; + + if (high == 0) { + return 0; + } + + while (low < high) { + uint256 mid = MathSlice39.average(low, high); + if (unsafeAccess(array, mid).value > element) { + high = mid; + } else { + low = mid + 1; + } + } + + if (low > 0 && unsafeAccess(array, low - 1).value == element) { + return low - 1; + } else { + return low; + } + } + + function unsafeAccess(address[] storage arr, uint256 pos) internal pure returns (StorageSlotSlice39.AddressSlot storage) { + bytes32 slot; + assembly ("memory-safe") { + mstore(0, arr.slot) + slot := add(keccak256(0, 0x20), pos) + } + return slot.getAddressSlot(); + } + + function unsafeAccess(uint256[] storage arr, uint256 pos) internal pure returns (StorageSlotSlice39.Uint256Slot storage) { + bytes32 slot; + assembly ("memory-safe") { + mstore(0, arr.slot) + slot := add(keccak256(0, 0x20), pos) + } + return slot.getUint256Slot(); + } +} + +library BitMapsSlice39 { + struct BitMap { + mapping(uint256 bucket => uint256) _data; + } + + function get(BitMap storage bitmap, uint256 index) internal view returns (bool) { + uint256 bucket = index >> 8; + uint256 mask = 1 << (index & 0xff); + return bitmap._data[bucket] & mask != 0; + } + + function setTo(BitMap storage bitmap, uint256 index, bool value) internal { + if (value) { + set(bitmap, index); + } else { + unset(bitmap, index); + } + } + + function set(BitMap storage bitmap, uint256 index) internal { + uint256 bucket = index >> 8; + uint256 mask = 1 << (index & 0xff); + bitmap._data[bucket] |= mask; + } + + function unset(BitMap storage bitmap, uint256 index) internal { + uint256 bucket = index >> 8; + uint256 mask = 1 << (index & 0xff); + bitmap._data[bucket] &= ~mask; + } +} + +library StringsSlice39 { + bytes16 private constant HEX_DIGITS = "0123456789abcdef"; + uint8 private constant ADDRESS_LENGTH = 20; + + error StringsInsufficientHexLength(uint256 value, uint256 length); + + function toString(uint256 value) internal pure returns (string memory) { + unchecked { + uint256 length = MathSlice39.log10(value) + 1; + string memory buffer = new string(length); + uint256 ptr; + assembly ("memory-safe") { + ptr := add(buffer, add(32, length)) + } + while (true) { + ptr--; + assembly ("memory-safe") { + mstore8(ptr, byte(mod(value, 10), HEX_DIGITS)) + } + value /= 10; + if (value == 0) break; + } + return buffer; + } + } + + function toStringSigned(int256 value) internal pure returns (string memory) { + return string.concat(value < 0 ? "-" : "", toString(SignedMathSlice39.abs(value))); + } + + function toHexString(uint256 value) internal pure returns (string memory) { + unchecked { + return toHexString(value, MathSlice39.log256(value) + 1); + } + } + + function toHexString(uint256 value, uint256 length) internal pure returns (string memory) { + uint256 localValue = value; + bytes memory buffer = new bytes(2 * length + 2); + buffer[0] = "0"; + buffer[1] = "x"; + for (uint256 i = 2 * length + 1; i > 1; --i) { + buffer[i] = HEX_DIGITS[localValue & 0xf]; + localValue >>= 4; + } + if (localValue != 0) { + revert StringsInsufficientHexLength(value, length); + } + return string(buffer); + } + + function toHexString(address addr) internal pure returns (string memory) { + return toHexString(uint256(uint160(addr)), ADDRESS_LENGTH); + } + + function equal(string memory a, string memory b) internal pure returns (bool) { + return bytes(a).length == bytes(b).length && keccak256(bytes(a)) == keccak256(bytes(b)); + } + + function nibbleCode(uint256 idx) internal pure returns (uint8) { + return uint8(HEX_DIGITS[idx & 0x0f]) ^ uint8(bytes1(":")); + } +} + +contract SequenceFixture { + using ArraysSlice39 for uint256[]; + using ArraysSlice39 for address[]; + using BitMapsSlice39 for BitMapsSlice39.BitMap; + using StringsSlice39 for uint256; + using StringsSlice39 for int256; + using StringsSlice39 for address; + + event HexSnapshotRecorded(address indexed actor, uint256 indexed upperIdx, bytes32 hexDigest, bool bitEnabled); + + uint256[] private _checkpoints; + address[] private _signers; + BitMapsSlice39.BitMap private _bitmap; + mapping(address account => string) private _hexLabels; + + uint256 private totalDigestScore; + bytes32 private rollingDigest; + + function formatHex(uint256 value) public pure returns (string memory) { + return value.toHexString(); + } + + function formatHexFixed(uint256 value, uint256 length) public pure returns (string memory) { + return value.toHexString(length); + } + + function formatAddressHex(address account) public pure returns (string memory) { + return account.toHexString(); + } + + function formatSignedDecimal(int256 value) public pure returns (string memory) { + return value.toStringSigned(); + } + + function checkStringEqual(string memory a, string memory b) public pure returns (bool) { + return StringsSlice39.equal(a, b); + } + + function upperBound(uint256 element) public view returns (uint256) { + return _checkpoints.findUpperBound(element); + } + + function bitmapBit(uint256 index) public view returns (bool) { + return _bitmap.get(index); + } + + function change(uint256 input) external returns (uint256) { + uint256 step = (input & 0x0f) + 1; + uint256 len = _checkpoints.length; + uint256 nextCheckpoint = len == 0 ? step * 10 : ArraysSlice39.unsafeAccess(_checkpoints, len - 1).value + step * 10; + _checkpoints.push(nextCheckpoint); + _signers.push(msg.sender); + + if (_checkpoints.length > 1 && (input & 1) == 1) { + uint256 lastIdx = _checkpoints.length - 1; + ArraysSlice39.unsafeAccess(_checkpoints, lastIdx).value = nextCheckpoint + 3; + ArraysSlice39.unsafeAccess(_signers, lastIdx).value = address(uint160(uint256(uint160(msg.sender)) ^ 1)); + } + + uint256 bitIdx = input & 0x1ff; + bool enableBit = (input & 2) == 0; + _bitmap.setTo(bitIdx, enableBit); + + uint256 queryTarget = nextCheckpoint - (input & 7); + uint256 ub = _checkpoints.findUpperBound(queryTarget); + + string memory hexAuto = ((input & 0xffff) + 1).toHexString(); + string memory hexFixed = (input & 0xfff).toHexString(2); + string memory addrHex = ArraysSlice39.unsafeAccess(_signers, _signers.length - 1).value.toHexString(); + int256 signedVal = (input & 4) == 0 ? -int256((input & 0xff) + 1) : int256((input & 0xff) + 1); + string memory signedStr = signedVal.toStringSigned(); + + string memory combined = string.concat(hexAuto, ":", hexFixed, ":", signedStr); + _hexLabels[msg.sender] = combined; + bool sameLabel = StringsSlice39.equal(_hexLabels[msg.sender], combined); + uint8 nibXor = StringsSlice39.nibbleCode(input); + + bytes32 digest = keccak256(bytes(string.concat(combined, ":", addrHex))); + bool bitNow = _bitmap.get(bitIdx); + + emit HexSnapshotRecorded(msg.sender, ub, digest, bitNow); + + uint256 delta; + unchecked { + delta = + (uint256(digest) & 0xffffffff) + + ub * 1000 + + (bitNow ? 500 : 100) + + (sameLabel ? 77 : 0) + + uint256(nibXor) + + bytes(_hexLabels[msg.sender]).length; + totalDigestScore += delta; + } + rollingDigest = rollingDigest ^ digest ^ bytes32(ub); + require(input != 20, "SHAB: rollback"); + return totalDigestScore; + } + + function fail() external { + _bitmap.setTo(7, true); + totalDigestScore += 999; + revert("SHAB: fail"); + } + + function read() external view returns (uint256, bytes32, uint256, bool) { + return ( + totalDigestScore, + rollingDigest, + _checkpoints.length, + _bitmap.get(0) + ); + } +} diff --git a/Contracts/SolidityImportSmoke/StringsHexArraysBitmapsSequenceModel.lean b/Contracts/SolidityImportSmoke/StringsHexArraysBitmapsSequenceModel.lean new file mode 100644 index 000000000..3bb155a1b --- /dev/null +++ b/Contracts/SolidityImportSmoke/StringsHexArraysBitmapsSequenceModel.lean @@ -0,0 +1,40 @@ +import Compiler.SolidityImport.Import +import Compiler.SolidityImport.SequenceRunner +import Compiler.SolidityImport.Differential +import Compiler.CompilationModel +import Compiler.Codegen +import Compiler.Yul.PrettyPrint + +namespace SolidityImportSmoke.StringsHexArraysBitmapsSequenceModel +open Compiler.CompilationModel +solidity_import imported from "Contracts/SolidityImportSmoke" entry "StringsHexArraysBitmapsSequence.sol" + using { evmVersion := "osaka", viaIR := true, optimizerRuns := some 466, bytecodeHash := "none" } + contract SequenceFixture + function change(uint256) + function fail() + function read() + function formatHex(uint256) + function formatHexFixed(uint256, uint256) + function formatAddressHex(address) + function formatSignedDecimal(int256) + function checkStringEqual(string, string) + function upperBound(uint256) + function bitmapBit(uint256) +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.StringsHexArraysBitmapsSequenceModel + +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.StringsHexArraysBitmapsSequenceModel.model selectors .osaka) + IO.FS.writeFile output (Compiler.Yul.render (Compiler.emitYul compiled)) + return 0 + | _ => + Compiler.CompilationModel.SolidityImport.SequenceRunner.run + SolidityImportSmoke.StringsHexArraysBitmapsSequenceModel.model SolidityImportSmoke.StringsHexArraysBitmapsSequenceModel.oracle args diff --git a/docs/SOLIDITY_IMPORT.md b/docs/SOLIDITY_IMPORT.md index 805eb730a..36ba2e1c2 100644 --- a/docs/SOLIDITY_IMPORT.md +++ b/docs/SOLIDITY_IMPORT.md @@ -848,3 +848,12 @@ prerequisite for the measured IdLib path, not an implementation of `storeInCode` | Yul `mstore8(addr, val)` in `InlineAssembly` and `bytes1`–`bytes32` string/hex literal constants in Yul (`Strings.HEX_DIGITS`) | `lowerYulStmtSlice` lowers `mstore8(addr, val)` to an exact read-modify-write on the containing 32-byte word (`wordAddr := addr & ~31`, `shift := 8 * (31 - (addr & 31))`, `mstore(wordAddr, (mload(wordAddr) & ~(0xff << shift)) \| ((val & 0xff) << shift))`). `index` and `bindYulExternalConstants` admit `bytes1`–`bytes32` `constant` state variables initialized with string/hex literals (`bytes16 private constant HEX_DIGITS = "0123456789abcdef"`), left-aligning the hex payload to a 256-bit word (`word * 16^(64 - hex.length)`) in `Env.yulNames` for `byte(idx, HEX_DIGITS)`. `lowerStringHelperStmts` supports multi-statement `string memory` / `bytes memory` helpers containing `UncheckedBlock`, `ForStatement`, `WhileStatement`, `InlineAssembly`, `IfStatement` (including early-return or revert branches), and `RevertStatement`. | | Bounded `while (true)` division/right-shift loops with `if (v == 0) break;` (`Strings.toString`) and `int_const` subtraction folding (`(1 << 128) - 1` in `Math.log256`) | `lowerWhile` supports `while (true)` loops whose body contains no `return`, updates an unsigned writable local `v` (`uintN`, `bits <= 256`) only in the penultimate statement via `v /= d` / `v = v / d` (`d >= 2` literal) or `v >>= k` / `v = v >> k` (`1 <= k < 256` literal), and ends with `if (v == 0) break;` (with no other `break` or `continue`), lowering to a `doneVar`-guarded `Stmt.forEach` bounded by `bits` iterations. `lowerBinary` folds non-negative `int_const` subtractions `a - b` when `a >= b` and `a - b < 2^256`. | +### Development slice: `Strings.toHexString` (all overloads), `Strings.toStringSigned`, `Strings.equal`, `Arrays.findUpperBound`, `BitMaps.setTo`, fixed-bytes indexing (`HEX_DIGITS[idx]`), `bytes1` casts, `bytes memory` element writes (`buffer[i] = ...`), and decrementing `for` loops + +| Supported Solidity | Lowering boundary | +| --- | --- | +| Fixed-bytes indexing (`b[idx]` on `bytes1`–`bytes32`, `HEX_DIGITS[value & 0xf]`) and `bytes1` casts (`bytes1("0")`, `bytes1(uint8)`, `uint8(bytes1)`, `bytes1(bytes32)`, `bytes32(bytes1)`) | `lowerRef` and `lowerExpr` admit `bytes1`–`bytes32` literal `constant` declarations (`numericConstants`) as left-aligned 256-bit words (`word * 16^(64 - hex.length)`), and lower `base[idx]` on any pure/stateless `bytes1`–`bytes32` value with an unsigned index `idx` to a `idx < W` bounds check (`Panic(0x32)`) and `Expr.shl 248 (Expr.byte idx base)` (a left-aligned `bytes1` word). `lowerCast` supports `bytes1` casts from 1-byte string/hex literals (`byteVal * 2^248`), `uint8` (`(x & 0xff) << 248`), `bytes32` / `bytes4`, and `0xXX` hex integer literals, as well as `uint8(bytes1)` (`x >> 248`) and `bytes32(bytes1)` / `bytes4(bytes1)`. Stateful or assignment fixed-bytes base/index expressions and multi-byte string literal casts to `bytes1` fail closed with located diagnostics. | +| Dynamic `bytes memory` element writes (`buffer[i] = val` / `delete buffer[i]`) and `new bytes(a + b)` allocations (`Strings.toHexString(uint256, uint256)`, `Strings.toStringSigned`) | `lowerLocal` admits `bytes memory buf = new bytes(len)` / `string memory buf = new string(len)` outside `unchecked` blocks when `len` is a binary arithmetic expression (`2 * length + 2`), checking `len` before allocating a header-backed `(pointer := headerPtr + 32, size := len)` buffer with `buf` registered in `Env.yulNames`. `lowerEffect` supports `buffer[idx] = rhs` and `delete buffer[idx]` on `new bytes(...)` buffers (`byteBuffers` with `yulNames` entry) when `idx` is a pure/stateless unsigned expression and `rhs` is a `bytes1` expression or 1-byte string/hex literal (`"0"`, `"x"`, `HEX_DIGITS[...]`), enforcing `idx < buffer.size` (`Panic(0x32)`) and performing a single-byte read-modify-write at `buffer.pointer + idx`. | +| 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). | + diff --git a/lakefile.lean b/lakefile.lean index 370e5b50e..5daf9c177 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -110,6 +110,7 @@ lean_lib «SolidityImportSmoke» where .one `Contracts.SolidityImportSmoke.MidnightPositionAndFeeSequenceModel, .one `Contracts.SolidityImportSmoke.TimelockAndBytes4CastSequenceModel, .one `Contracts.SolidityImportSmoke.StringBytesMappingsUriStorageStringsSequenceModel, + .one `Contracts.SolidityImportSmoke.StringsHexArraysBitmapsSequenceModel, .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 267717ef4..31be8636d 100644 --- a/scripts/solidity_differential/check_stateful.py +++ b/scripts/solidity_differential/check_stateful.py @@ -297,6 +297,12 @@ def main(): 'formatAddress(address)', 'readFallbackTag()', 'readFallbackTagLength()', + 'formatHexFixed(uint256,uint256)', + 'formatAddressHex(address)', + 'formatSignedDecimal(int256)', + 'checkStringEqual(string,string)', + 'upperBound(uint256)', + 'bitmapBit(uint256)', ): if extra_name in source['methodIdentifiers']: names.append(extra_name) @@ -800,6 +806,35 @@ def mapping_slot(base, key): ] remaining_budget = max(0, args.transactions - len(calls)) calls.extend(uri_storage_prefix[:remaining_budget]) + if 'formatHexFixed(uint256,uint256)' in names: + strings_hex_prefix = [ + ('formatHex(uint256)', [0]), + ('formatHex(uint256)', [0xdeadbeef]), + ('formatHexFixed(uint256,uint256)', [0x1234, 2]), + ('formatHexFixed(uint256,uint256)', [0x12345, 2]), + ('formatAddressHex(address)', [int(senders[0], 16)]), + ('formatAddressHex(address)', [1 << 160]), + ('formatSignedDecimal(int256)', [0]), + ('formatSignedDecimal(int256)', [42]), + ('formatSignedDecimal(int256)', [(1 << 256) - 42]), + ('checkStringEqual(string,string)', [64, 128, 3, 0x616263 << 232, 3, 0x616263 << 232]), + ('checkStringEqual(string,string)', [64, 128, 3, 0x616263 << 232, 3, 0x616264 << 232]), + ('upperBound(uint256)', [10]), + ('bitmapBit(uint256)', [0]), + ('change(uint256)', [0]), + ('upperBound(uint256)', [5]), + ('upperBound(uint256)', [10]), + ('upperBound(uint256)', [25]), + ('bitmapBit(uint256)', [0]), + ('change(uint256)', [1]), + ('upperBound(uint256)', [15]), + ('bitmapBit(uint256)', [1]), + ('change(uint256)', [2]), + ('bitmapBit(uint256)', [0]), + ('read()', []), + ] + remaining_budget = max(0, args.transactions - len(calls)) + calls.extend(strings_hex_prefix[:remaining_budget]) while len(calls) < args.transactions: name = rng.choice(names) if name == names[0]: @@ -1042,8 +1077,21 @@ def mapping_slot(base, key): call_args = [rng.choice([0, 7, 42, 99999, 10**18, (1 << 256) - 1])] elif name == 'formatHex(uint256)': call_args = [rng.choice([0, 15, 255, 0x1234abcd, (1 << 128) - 1, (1 << 256) - 1])] - elif name == 'formatAddress(address)': + elif name in ('formatAddress(address)', 'formatAddressHex(address)'): call_args = [rng.choice([int(senders[0], 16), 0, 0xdeadbeef, 1 << 160])] + elif name == 'formatHexFixed(uint256,uint256)': + call_args = rng.choice([[0, 1], [0xab, 1], [0x1234, 2], [0x12345, 2], [0xdeadbeef, 4]]) + elif name == 'formatSignedDecimal(int256)': + call_args = [rng.choice([0, 1, 42, (1 << 256) - 1, (1 << 256) - 9999, 1 << 255])] + elif name == 'checkStringEqual(string,string)': + call_args = rng.choice([ + [64, 128, 0, 0], + [64, 128, 3, 0x616263 << 232, 3, 0x616263 << 232], + [64, 128, 3, 0x616263 << 232, 3, 0x616264 << 232], + [64, 128, 2, 0x6162 << 240, 3, 0x616263 << 232], + ]) + elif name in ('upperBound(uint256)', 'bitmapBit(uint256)'): + call_args = [rng.choice([0, 1, 5, 10, 20, 50, 255, 256])] 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 385e4aade..5d664e741 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 +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 .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'), 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'), 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'}[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'}[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 == 'strings-hex-arrays-bitmaps': + variants = ('baseline', 'renamed', 'expanded-strings-hex-arrays-bitmaps') if args.fixture == 'string-bytes-mappings-uri-storage-strings': variants = ('baseline', 'renamed', 'expanded-string-bytes-mappings-uri-storage-strings') if args.fixture == 'timelock-and-bytes4-cast': @@ -156,6 +158,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_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" else stateful_midnight_position_and_fee_source(fixture, variant) if args.fixture == "midnight-position-and-fee" @@ -217,12 +220,14 @@ 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'): + 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'): 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])] if args.fixture == 'string-bytes-mappings-uri-storage-strings': 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 == '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 734eee4ba..fcdeb3a0b 100644 --- a/scripts/solidity_differential/check_storage_mutations.py +++ b/scripts/solidity_differential/check_storage_mutations.py @@ -351,10 +351,16 @@ 'import-string-bytes-mappings-uri-storage-strings-mapping-slot-zero': (' if info.bytesStorage && info.keyCount == count then\n markField name\n let (slotStmts, slotExpr) ← computeSPathBaseSlot path info 0 j\n return some (pre ++ slotStmts, "", slotExpr, info.stringStorage)', ' if info.bytesStorage && info.keyCount == count then\n markField name\n let (slotStmts, _) ← computeSPathBaseSlot path info 0 j\n return some (pre ++ slotStmts, "", .literal 0, info.stringStorage)'), 'import-string-bytes-mappings-uri-storage-strings-while-true-break-immediately': (' let iterStmts := bodyOut.toList ++ [Stmt.ite breakCondVal.expr [.assignVar doneVar (.literal 1)] []]\n return #[\n .letVar doneVar (.literal 0),\n .forEach loopVar (.literal bits) [.ite (.eq (.localVar doneVar) (.literal 0)) iterStmts []]\n ]', ' let _ := breakCondVal.expr\n let iterStmts := bodyOut.toList ++ [Stmt.assignVar doneVar (.literal 1)]\n return #[\n .letVar doneVar (.literal 0),\n .forEach loopVar (.literal bits) [.ite (.eq (.localVar doneVar) (.literal 0)) iterStmts []]\n ]'), 'import-string-bytes-mappings-uri-storage-strings-mapping-write-stateful-rhs-guard': (' let right ← mField expression "rightHandSide"\n if !pre.isEmpty && (assignmentIn right || statefulCallIn right (← get)) then\n failAt target "mapping bytes/string write key prelude with stateful RHS is unsupported"\n return ← lowerStorageBytesWrite "" (pre ++ slotStmts) target right slotExpr (some info.stringStorage)', ' let right ← mField expression "rightHandSide"\n if false then\n failAt target "mapping bytes/string write key prelude with stateful RHS is unsupported"\n return ← lowerStorageBytesWrite "" (pre ++ slotStmts) target right slotExpr (some info.stringStorage)'), + 'import-strings-hex-arrays-bitmaps-fixed-bytes-index-zero': (' let bAtom ← atom baseVal\n let pre := bAtom.pre ++ key.pre ++ #[.ite (.lt key.expr (.literal byteW)) [] [.panicCode (.literal 0x32)]]\n return .expr { pre, expr := .shl (.literal 248) (.byte key.expr bAtom.expr) }', ' let bAtom ← atom baseVal\n let pre := bAtom.pre ++ key.pre ++ #[.ite (.lt key.expr (.literal byteW)) [] [.panicCode (.literal 0x32)]]\n return .expr { pre, expr := .literal 0 }'), + '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"'), }) def run(directory, output, name): fixture = "StorageVoidSequence" if name == "import-void-fallthrough" else "StorageSequence" + if name.startswith("import-strings-hex-arrays-bitmaps-"): + fixture = "StringsHexArraysBitmapsSequence" if name.startswith("import-string-bytes-mappings-uri-storage-strings-"): fixture = "StringBytesMappingsUriStorageStringsSequence" if name.startswith("import-timelock-and-bytes4-cast-"): @@ -473,11 +479,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'} 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'} 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'} 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'} 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', '--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'}: - 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'} 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'}: + 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 == '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': @@ -485,7 +491,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'}: + 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'}: 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': @@ -503,6 +509,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, 8, 20, 21])] + if fixture == 'StringsHexArraysBitmapsSequence': + tx_idx = argv.index('--transactions') + 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 == 'EmptyArrayReturnBytesCalldataSequence': prefix = argv.index('--change-prefix') argv = argv[:prefix] + ['--change-prefix', *map(str, [0, 1, 2, 3, 16, 17, 18, (1 << 256) - 1])] @@ -995,6 +1006,17 @@ def helper_order_control(directory, name, mutated): return bytes(uris[x]).length; } } +''') + elif name == 'import-strings-hex-arrays-bitmaps-stateful-fixed-bytes-index-guard': + diagnostic = 'stateful or assignment fixed-bytes index is unsupported' + (target / 'Fixture.sol').write_text('''pragma solidity 0.8.34; +contract C { + bytes16 private constant HEX_DIGITS = "0123456789abcdef"; + function checked(uint256 x) external pure returns (uint256) { + uint256 y = x; + return uint256(uint8(HEX_DIGITS[y = 1])); + } +} ''') else: argument = name.endswith('argument-guard') @@ -1084,7 +1106,8 @@ def mutation_campaign(output, selected=None): 'import-market-params-balances-struct-keccak-len-guard', '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-string-bytes-mappings-uri-storage-strings-mapping-write-stateful-rhs-guard', + 'import-strings-hex-arrays-bitmaps-stateful-fixed-bytes-index-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 32abbdac5..cfb91b48f 100644 --- a/scripts/solidity_differential/check_storage_rejections.py +++ b/scripts/solidity_differential/check_storage_rejections.py @@ -1268,6 +1268,26 @@ def main(): None, '{ evmVersion := "osaka", viaIR := true, optimizerRuns := some 466, bytecodeHash := "none" }', 'NewExpression: [solidity-import:unsupported] hash input must be a supported ABI encoding'), + ('strings-hex-arrays-bitmaps-positive', + (root / 'Contracts/SolidityImportSmoke/StringsHexArraysBitmapsSequence.sol').read_text().replace('contract SequenceFixture', 'contract C').replace('function change(', 'function checked('), + None, + '{ evmVersion := "osaka", viaIR := true, optimizerRuns := some 466, bytecodeHash := "none" }', + None), + ('strings-hex-arrays-bitmaps-decrement-for-step-rejected', + "pragma solidity 0.8.34;\ncontract C {\n function checked(uint256 x) external pure returns (uint256) {\n uint256 acc = 0;\n for (uint256 i = x + 4; i > 1; i -= 2) {\n acc += i;\n }\n return acc;\n }\n}\n", + None, + '{ evmVersion := "osaka", viaIR := true, optimizerRuns := some 466, bytecodeHash := "none" }', + 'Assignment: [solidity-import:unsupported] a decrementing for loop must decrement its counter by one'), + ('strings-hex-arrays-bitmaps-byte-buffer-assignment-index-rejected', + "pragma solidity 0.8.34;\ncontract C {\n function checked(uint256 x) external pure returns (uint256) {\n bytes memory buf = new bytes(x + 2);\n buf[x = 0] = \"0\";\n return buf.length;\n }\n}\n", + None, + '{ evmVersion := "osaka", viaIR := true, optimizerRuns := some 466, bytecodeHash := "none" }', + 'IndexAccess: [solidity-import:unsupported] stateful or assignment array index is unsupported'), + ('strings-hex-arrays-bitmaps-bytes16-to-bytes1-cast-rejected', + "pragma solidity 0.8.34;\ncontract C {\n bytes16 private constant HEX_DIGITS = \"0123456789abcdef\";\n function checked(uint256 x) external pure returns (uint256) {\n return uint256(uint8(bytes1(HEX_DIGITS))) + x;\n }\n}\n", + None, + '{ evmVersion := "osaka", viaIR := true, optimizerRuns := some 466, bytecodeHash := "none" }', + 'FunctionCall: [solidity-import:unsupported] unsupported cast source bytes16 for bytes1'), ] for name, source_text, dep_text, profile_text, expected in solc_0810_cases: if args.only and args.only not in name: @@ -1307,6 +1327,7 @@ def main(): else 'checked(uint256)\n function summaryCard()\n function bucketView(bytes32)\n function position(bytes32,address)\n function collateral(bytes32,address,uint256)\n function settlementFee(bytes32,uint256)\n function updatePositionView(bytes32,address,uint256)' if name == 'midnight-position-and-fee-positive' 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)' ) driver = directory / 'Check.lean' diff --git a/scripts/solidity_differential/programs.py b/scripts/solidity_differential/programs.py index e524d14ac..bf8994a95 100644 --- a/scripts/solidity_differential/programs.py +++ b/scripts/solidity_differential/programs.py @@ -2219,3 +2219,38 @@ def stateful_string_bytes_mappings_uri_storage_strings_source(fixture: str, vari return fixture raise ValueError(f'unknown string-bytes-mappings-uri-storage-strings variant: {variant}') + +def stateful_strings_hex_arrays_bitmaps_source(fixture: str, variant: str) -> str: + if variant == 'baseline': + return fixture + if variant == 'renamed': + import re + names = { + '_checkpoints', '_signers', '_bitmap', '_hexLabels', + 'totalDigestScore', 'rollingDigest', + 'step', 'nextCheckpoint', 'lastIdx', 'bitIdx', 'enableBit', + 'queryTarget', 'ub', 'hexAuto', 'hexFixed', 'addrHex', + 'signedVal', 'signedStr', 'combined', 'sameLabel', 'nibXor', + 'digest', 'bitNow', 'delta', + } + 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-strings-hex-arrays-bitmaps': + replacements = { + 'for (uint256 i = 2 * length + 1; i > 1; --i)': + 'for (uint256 i = 2 * length + 1; i > 1; i -= 1)', + 'localValue >>= 4;': + 'localValue = localValue >> 4;', + 'totalDigestScore += delta;': + 'totalDigestScore = totalDigestScore + delta;', + 'totalDigestScore += 999;': + 'totalDigestScore = totalDigestScore + 999;', + } + for before, after in replacements.items(): + if fixture.count(before) != 1: + raise ValueError('strings-hex-arrays-bitmaps variant anchor changed') + fixture = fixture.replace(before, after) + return fixture + raise ValueError(f'unknown strings-hex-arrays-bitmaps variant: {variant}') +