feat(solidity-import): support ECDSA Yul signature unpacking, StorageSlot raw string/bytes slots, and error scalar casts (slice 40)

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

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 <name> 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. |
+

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,

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))