diff --git a/STFSpec/Conformance/Commit/deep_chain_probe.py b/STFSpec/Conformance/Commit/deep_chain_probe.py index 2d6f4f64..73400a3b 100644 --- a/STFSpec/Conformance/Commit/deep_chain_probe.py +++ b/STFSpec/Conformance/Commit/deep_chain_probe.py @@ -21,10 +21,13 @@ whose HEAD is not reference.toml's `release.commit` or which has local changes (tracked or untracked) under `src/`. -This is decode-level evidence from the probe's own shallow call stack on one host. In -the guest, decoding runs lazily inside block and EVM execution, so the guest's failing -depth is lower by the caller's frames, and it depends on the interpreter, its frame -layout and the node shape (DISC-001). +This is raw-decoder evidence from the probe's own shallow call stack on one host, not +evidence of guest reachability. Each witness node must first pass the normal serialized +guest's 1,024-byte SSZ node limit. The report gives root node_bytes, the largest DB +node's size and whether every node meets that per-node bound. Meeting the bound alone +is not full guest admission or validation (DISC-001). For admitted nodes, lazy decoding +inside block and EVM execution also depends on the caller's frames, interpreter and +node shape. """ import argparse @@ -109,6 +112,8 @@ def value_nest(depth): digest = hashlib.sha256( root + b"".join(k + v for k, v in sorted(db.items())) ).hexdigest() + max_node_bytes = max(len(raw) for raw in db.values()) + node_byte_bound_met = max_node_bytes <= 1024 for secured in (False, True): try: inc.decode_witness_to_mpt(db, root, secured, b"") @@ -116,7 +121,10 @@ def value_nest(depth): except Exception as error: # noqa: BLE001 (the guest catch-all, stateless.py:294) outcome = f"{type(error).__name__}: {str(error)[:60]}" mode = "secured" if secured else "plain" - print(f"{kind} {depth} sha256 {digest[:16]} {mode}: {outcome}") + print(f"{kind} {depth} node_bytes {len(node)} " + f"max_node_bytes {max_node_bytes} " + f"node_byte_bound_met {node_byte_bound_met} " + f"sha256 {digest[:16]} {mode}: {outcome}") if __name__ == "__main__": diff --git a/STFSpec/informal/DECISIONS.md b/STFSpec/informal/DECISIONS.md index 2a16a0b9..523d1d53 100644 --- a/STFSpec/informal/DECISIONS.md +++ b/STFSpec/informal/DECISIONS.md @@ -1,6 +1,6 @@ # Decisions -*Status: current. Date: 2026-11-11. This is the single register of design decisions and question dispositions: statuses are recorded only here. Other documents cite entries by ID (P1, D5, B8, F7, Q20) and never restate them.* +*Status: current. Date: 2026-11-13. This is the single register of design decisions and question dispositions: statuses are recorded only here. Other documents cite entries by ID (P1, D5, B8, F7, Q20) and never restate them.* | Status | Meaning | |---|---| @@ -104,7 +104,7 @@ Questions that do not affect interfaces, or that are resolved or tracked elsewhe |---|---|---| | Q3 | Taylor loop on adversarial `excessBlobGas` | Tracked as **DISC-002** (measured). Liveness only; no interface change. | | Q5 | Fork-activation check | Follow the reference, and keep the explicit exclusion (CONTRACT §5). | -| Q6, Q20 | Deep witness chains; deep RLP nesting | Tracked under **DISC-001** (O12 host resources) and **DISC-006** (why the error surfaces as O6). **Unresolved by design:** D14 does not decide it. The guest-process recursion limit is 100,000 (py_ecc raises it). RLP nesting of 20,000 levels decodes and 40,000 raises, and the resulting `RecursionError` becomes O6 on the guest path (observed by running the pinned EELS on deterministic probe inputs, 2026-09-29). Re-measured at `59c1473d` (DISC-001, 2026-11-11): for chains of trie nodes the recursion limit no longer decides the guest output, because every guest decode is secured and Q90 bounds the depth; deep RLP nesting inside a witness node's branch value still can. | +| Q6, Q20 | Deep witness chains; deep RLP nesting | Tracked under **DISC-001** (O12 host resources) and **DISC-006** (why a payload transaction error surfaces as O6). **Unresolved by design:** D14 does not decide it. DISC-001 owns the measured cases, guest-admission qualifications and remaining host-dependent investigations. Raw decoder probes alone do not establish a divergence of admitted serialized guest inputs. | | Q7 | Lean-native witness generator | Use the EELS host out of process for now; revisit when fuzzing throughput is measured. | | Q8 | Transition fixtures | Skip and count them in the stateful runner until a BPO2 instantiation exists. | | Q9 | EEST exception-name mapping | Warning-only; validity itself is decisive. | diff --git a/STFSpec/informal/DISCREPANCIES.md b/STFSpec/informal/DISCREPANCIES.md index ae786b19..5e791a8e 100644 --- a/STFSpec/informal/DISCREPANCIES.md +++ b/STFSpec/informal/DISCREPANCIES.md @@ -1,6 +1,6 @@ # Protocol discrepancy register -Status: no accepted deviations. Date: 2026-11-11. This register implements the recording part of [`CONTRACT.md`](CONTRACT.md) §6; an entry does not authorize a change or imply that an upstream report exists. Preserve the pinned reference until an accepted decision says otherwise. +Status: no accepted deviations. Date: 2026-11-13. This register implements the recording part of [`CONTRACT.md`](CONTRACT.md) §6; an entry does not authorize a change or imply that an upstream report exists. Preserve the pinned reference until an accepted decision says otherwise. ## DISC-001: Python host resource limits @@ -16,7 +16,8 @@ Status: no accepted deviations. Date: 2026-11-11. This register implements the r - **Recorded evidence (2026-11-11, at `59c1473d`, decode level; reproducer `STFSpec/Conformance/Commit/deep_chain_probe.py`, which checks the pin and prints each input's digest):** - Environment: CPython 3.12.11, ethereum-rlp 0.1.6, locked dependencies, recursion limit 100,000. The depths are measured from the probe's own call stack. In the guest, decoding runs lazily inside block and EVM execution, so the guest's failing depth is lower by the caller's frames; it also depends on the interpreter and the node shape. - Chains of trie nodes: a chain of branches with hashed children decodes to depth 49,994 and raises `RecursionError` at 49,995, secured or not (an independent run of the same probe, with the same interpreter and package versions in a smaller installed environment, gave 49,995 and 49,996 on every run, so the threshold depends on the installed environment). With `secured` true, depth 63 above a one-nibble leaf succeeds, and every deeper chain below that threshold fails the path check (`incremental_mpt.py:987–1013`) with `AssertionError`. Every guest decode is secured (`witness_state.py:88–93,162–167,172–177`), and both exceptions reach the catch-all at `stateless.py:294` with no earlier handler [I, by reading], so the guest output is `false`. The Q90 decoder (EthCommit C13) rejects every such chain with `.securedPathLength`, also `false` [I, by reading `STFSpec/Commit/Decoder.lean`]. For chains of trie nodes, the recursion limit no longer decides the guest output. - - RLP nesting inside a node: a branch with two stub children whose value (slot 16) is a list nested 33,330 deep decodes, secured or not, and EELS reads the value as `b""` (DISC-003); at 33,331 it raises `RecursionError`. The path check does not bound this, since the trie is one branch. The spec's decoder is total and reads the value as empty at any depth [I, by reading `STFSpec/Commit/Decoder.lean` and `STFSpec/Codec/RlpDecode.lean`], so this remains a guest-level divergence candidate on crafted inputs. + - RLP nesting inside a node: a branch with two stub children whose value (slot 16) is a list nested 33,330 deep decodes, secured or not, and EELS reads the value as `b""` (DISC-003); at 33,331 it raises `RecursionError`. The path check does not bound this, since the trie is one branch. The spec's decoder is total and reads the value as empty at any depth [I, by reading `STFSpec/Commit/Decoder.lean` and `STFSpec/Codec/RlpDecode.lean`]. + - This is raw-decoder evidence. The complete branch nodes at depths 33,330 and 33,331 are 111,280 and 111,284 bytes, exceeding the pinned normal guest's per-node SSZ ByteList[1024] limit (`stateless.py:35,46–49`). Serialized guest input decoding precedes validation (`stateless_guest.py:26–38,53–61`), so these particular nodes are rejected before witness-trie decoding. They establish no divergence on an admitted guest input. Admitted cross-node/DAG shapes and other host-resource cases remain open; a guest claim needs an admitted input and its complete guest path. - Still host-dependent: an `-O` host (no path check), memory or C-stack limits on other hosts, and the DAG blow-up (DISC-004). - Spec executable: the compiled Lean decoder accepts the nested branch value at every depth tried, up to 1,000,000, without exhausting its stack. Its memory grows with the square of chain depth: about 1 GB at depth 10,000, 22 GB at 50,000, and out of memory near 79 GB at 100,000 (measured by an independent review run, 2026-11-11, decoding each chain secured and unsecured; reproducer not committed). A wide trie of 40,000 nodes needs about 122 MB. The likely cause is that each level of `decodeEntry` inserts into a shared on-path `Std.HashSet`, which copies it (`STFSpec/Commit/Decoder.lean:172–183`) [I, by reading]. A chain of 100,000 nodes is about 10 MB of witness, and no node-count limit was found. So the definition rejects every deep chain, but the executable can run out of memory first; DEBT.md lists this as a known candidate. - **Open question:** which resource-independent interpretation, if any, upstream intends for valid finite inputs rejected only by host limits. “Unconstrained host” is not a computable or approved acceptance rule. diff --git a/STFSpec/informal/GAPS-CROSSCUTTING.md b/STFSpec/informal/GAPS-CROSSCUTTING.md index 646c1249..4786420f 100644 --- a/STFSpec/informal/GAPS-CROSSCUTTING.md +++ b/STFSpec/informal/GAPS-CROSSCUTTING.md @@ -1,6 +1,6 @@ ## Cross-cutting gaps and coordinated owners -*Status: live cross-cutting gap register. Date: 2026-11-11.* +*Status: live cross-cutting gap register. Date: 2026-11-13.* Maintained by hand. Each item says what is missing, the evidence, and who should own it. @@ -18,7 +18,7 @@ Under the reference's two catch-all handlers (`STFSpec/informal/CONTRACT.md` §4 ### X2. Adversarial inputs on which the reference effectively does not terminate The guest must terminate on *every* input. The design requires totality, which is not yet proved. DISC-002/004 already record the Taylor/DAG cases; host depth/resource acceptance needs a deliberate policy: - **Blob gas price Taylor loop.** `taylor_exponential` (`utils/numeric.py:177`) runs about 2.7·x iterations on growing integers, with x = excess / 11684671. Measured: 2,338 iterations at an excess of 10¹⁰. It is called for *every* block from `validate_header` → `calculate_excess_blob_gas(parent)` → `calculate_blob_gas_price` (`fork.py:448`, `vm/gas.py:921`, EIP-7918) whenever the parent's blob gas is at or above target. A crafted parent header with an excess near 2^64 needs about 4×10¹² iterations. The parent header is authenticated only externally (CONTRACT §7), so this is reachable in the guest. It is a liveness issue, not a soundness one. -- **Deep witness nesting.** Eager witness decoding (D19) recurses without a depth limit. For chains of trie nodes, the secured path check (Q90, EthCommit C13) bounds an accepted trie to 65 decoded nodes on a path, so a deeper chain gives `false` in both the spec and the reference. RLP nesting inside a witness node's branch value is not bounded by that check: the reference raises `RecursionError` (`false`) where a total spec accepts (EthStateless). Measurements and remaining host cases: DISC-001; the spec must decide deliberately. +- **Deep witness nesting.** Eager witness decoding (D19) has host-resource obligations. Secured trie paths are bounded by Q90/EthCommit C13/C17. The recorded within-node RLP nesting probes exceed normal guest SSZ node admission and do not establish an admitted guest divergence. DISC-001 owns their raw measurements, domain qualifications and remaining admitted cross-node/DAG or other host cases; O12 remains unresolved. - **Deep RLP nesting.** In the guest process, 20,000 nesting levels decode and 40,000 raise `RecursionError`, reachable through payload transactions. On the guest path, `is_valid_versioned_hashes` consumes that error, so the output is O6 (DISC-001, DISC-006; EthCodec). - **`MemoryError`:** host-dependent (CONTRACT O12). diff --git a/STFSpec/informal/GAPS.md b/STFSpec/informal/GAPS.md index c30414d9..3691b144 100644 --- a/STFSpec/informal/GAPS.md +++ b/STFSpec/informal/GAPS.md @@ -1,12 +1,12 @@ # Gap register -*Status: generated gap register. Source date: 2026-11-11.* +*Status: generated gap register. Source date: 2026-11-13.* *Generated by `scripts/gen_gaps.py` from `STFSpec/informal/GAPS-CROSSCUTTING.md` and the §10 Gaps section of each spec guidance document. Do not edit by hand: fix the source section, then regenerate.* ## Cross-cutting gaps and coordinated owners -*Status: live cross-cutting gap register. Date: 2026-11-11.* +*Status: live cross-cutting gap register. Date: 2026-11-13.* Maintained by hand. Each item says what is missing, the evidence, and who should own it. @@ -24,7 +24,7 @@ Under the reference's two catch-all handlers (`STFSpec/informal/CONTRACT.md` §4 ### X2. Adversarial inputs on which the reference effectively does not terminate The guest must terminate on *every* input. The design requires totality, which is not yet proved. DISC-002/004 already record the Taylor/DAG cases; host depth/resource acceptance needs a deliberate policy: - **Blob gas price Taylor loop.** `taylor_exponential` (`utils/numeric.py:177`) runs about 2.7·x iterations on growing integers, with x = excess / 11684671. Measured: 2,338 iterations at an excess of 10¹⁰. It is called for *every* block from `validate_header` → `calculate_excess_blob_gas(parent)` → `calculate_blob_gas_price` (`fork.py:448`, `vm/gas.py:921`, EIP-7918) whenever the parent's blob gas is at or above target. A crafted parent header with an excess near 2^64 needs about 4×10¹² iterations. The parent header is authenticated only externally (CONTRACT §7), so this is reachable in the guest. It is a liveness issue, not a soundness one. -- **Deep witness nesting.** Eager witness decoding (D19) recurses without a depth limit. For chains of trie nodes, the secured path check (Q90, EthCommit C13) bounds an accepted trie to 65 decoded nodes on a path, so a deeper chain gives `false` in both the spec and the reference. RLP nesting inside a witness node's branch value is not bounded by that check: the reference raises `RecursionError` (`false`) where a total spec accepts (EthStateless). Measurements and remaining host cases: DISC-001; the spec must decide deliberately. +- **Deep witness nesting.** Eager witness decoding (D19) has host-resource obligations. Secured trie paths are bounded by Q90/EthCommit C13/C17. The recorded within-node RLP nesting probes exceed normal guest SSZ node admission and do not establish an admitted guest divergence. DISC-001 owns their raw measurements, domain qualifications and remaining admitted cross-node/DAG or other host cases; O12 remains unresolved. - **Deep RLP nesting.** In the guest process, 20,000 nesting levels decode and 40,000 raise `RecursionError`, reachable through payload transactions. On the guest path, `is_valid_versioned_hashes` consumes that error, so the output is O6 (DISC-001, DISC-006; EthCodec). - **`MemoryError`:** host-dependent (CONTRACT O12). @@ -1093,7 +1093,7 @@ host dispatch with no corresponding Lean operation. A static call-graph pass ove - **`DecodingError` versus other exceptions in `_decode_header`.** The fallback fires only on `rlp.DecodingError`. If `ethereum-rlp` 0.1.6 raises another exception type for some malformed Amsterdam header (for example from a field constructor), EELS skips the fallback; the output is the same (inner failure), but the constructor differs. Unchecked. - **Missing BLOCKHASH ancestor** is a Python negative-index `IndexError` (`vm/instructions/block.py:58`), fixture-witnessed. It is O13 with the named constructor `VmFault.ancestorHashUnavailable` (`EthVmCore`/`EthVmInstructions`), not O4 or O6 (R5). Note that an ancestor deeper than the witness but within 256 blocks fails the block, while one beyond 256 returns zero without touching the witness. - **O2** has no fixture and no reachable spec path; L-root is unproved (open, DECISIONS §3 O2). If a future SSZ type made `hash_tree_root` partial (e.g. a resource limit), the constructor would be needed. -- **O12 candidates (DISC-001, unresolved).** The guest-process recursion limit is 100,000 (py_ecc raises it; `import ethereum` alone gives 12,288). (a) Deep RLP nesting in a witness header or transaction: 20,000 levels decode and 40,000 raise `RecursionError` in `ethereum-rlp` (witnessed by probe inputs). For a transaction it is caught inside `is_valid_versioned_hashes` and becomes O6 (DISC-006); for a header, in the inner phase. Since valid headers and transactions have bounded nesting, the output probably coincides with the spec's structural failure [I]. (b) Eager witness decoding (`incremental_mpt.py:885–1065`) recurses without a depth limit. For chains of trie nodes this no longer gives a divergence: every guest decode is secured, and EELS's path check (`incremental_mpt.py:987–1013`) or its recursion limit and the Q90 decoder all give `false` (EthCommit C17) [I, by reading]. RLP nesting inside a witness node's branch value is not bounded by the check: beyond a host-dependent depth EELS raises `RecursionError` (→ `false`), while the spec's total decoder accepts the node and reads the value as empty (DISC-003). This is a guest-level divergence on crafted inputs, uncovered by fixtures, and needs a decision with `EthStateWitness`; DISC-001 has the decode-level reproducer. +- **O12 candidates (DISC-001, unresolved).** DISC-001 owns the historical host measurements and their input/environment qualifications; DISC-006 owns the payload-transaction exception-catching phase. Secured deep trie-node chains remain subject to Q90/EthCommit C13/C17. Raw within-node RLP nesting is not bounded by that path check, but the recorded 33,330/33,331-depth nodes exceed the normal guest's per-node ByteList[1024] admission limit. They cannot demonstrate a guest divergence through that entrypoint. Witness headers are also byte-limited at SSZ admission; raw header probes likewise require that boundary to be checked before assigning a guest phase. Other admitted cross-node/DAG or host-resource cases remain separate investigations. A guest-level discrepancy requires an input admitted by the actual schema and observation of the complete guest path. - **Input size envelope.** Transactions, the BAL bytes and the progressive lists are unbounded in SSZ; the largest fixture input is 8.4 MB. There is no stated maximum input, memory or cycle envelope; `EthBase`'s `Envelope` record does not yet cover the guest. - **SSZ progressive types.** Correctness of `ProgressiveContainer`/progressive-list decoding and merkleization rests on `eth-remerkleable` 0.1.31 (EIP-7495/EIP-7916 as implemented there). EthCodec implements progressive merkleization, roots and forward encoding (Q75, Q79, Q80); progressive decoding is specified (Q88) but unimplemented, and no independent reference beyond `eth-remerkleable` 0.1.31 is pinned. - **`payloadHeader` totality** is inferred: EELS catches any exception there, and the spec asserts none can occur on decoded values. Needs a line-by-line check of `Header` field constructors (e.g. `Uint`/`U256` widening, `Bytes8`). diff --git a/STFSpec/informal/citation-remap.json b/STFSpec/informal/citation-remap.json index 699e5124..d2bd566c 100644 --- a/STFSpec/informal/citation-remap.json +++ b/STFSpec/informal/citation-remap.json @@ -941,12 +941,12 @@ {"doc": "STFSpec/informal/DECISIONS.md", "line": 251, "target": "src/ethereum/state.py", "kind": "path", "old": "src/ethereum/state.py:36,61–139", "new": "src/ethereum/state.py:30,55–133", "window": "4e34b6ff429df1abb7ac", "new_window": "f2f53ee11a064d9f085b"}, {"doc": "STFSpec/informal/DECISIONS.md", "line": 254, "target": "src/ethereum/forks/amsterdam/witness_state.py", "kind": "path", "old": "src/ethereum/forks/amsterdam/witness_state.py:205–213", "new": "src/ethereum/forks/amsterdam/witness_state.py:129–137", "window": "581792c95abca05bd161", "new_window": "9b2a352bd34456cc2cd9"}, {"doc": "STFSpec/informal/DECISIONS.md", "line": 257, "target": "src/ethereum/forks/amsterdam/state_tracker.py", "kind": "path", "old": "src/ethereum/forks/amsterdam/state_tracker.py:503–520,547–568", "new": "src/ethereum/forks/amsterdam/state_tracker.py:484–501,528–549", "window": "8bf8aab160fd7e27bddb", "new_window": "ada312777cf3f8fa06c1"}, - {"doc": "STFSpec/informal/DISCREPANCIES.md", "line": 28, "target": "src/ethereum/forks/amsterdam/fork.py", "kind": "path", "old": "fork.py:473", "new": "fork.py:448", "window": "c39ac175adc1278efc50", "new_window": "b031ea93a9b2665dd89a"}, - {"doc": "STFSpec/informal/DISCREPANCIES.md", "line": 28, "target": "src/ethereum/forks/amsterdam/vm/gas.py", "kind": "path", "old": "vm/gas.py:1011, 1046", "new": "vm/gas.py:996, 1031", "window": "3a7918a0d2dbeaf8a8a6", "new_window": "0f5fe77529a2cbbc387e"}, - {"doc": "STFSpec/informal/DISCREPANCIES.md", "line": 28, "target": "src/ethereum/forks/amsterdam/vm/gas.py", "kind": "path", "old": "vm/gas.py:146", "new": "vm/gas.py:137", "window": "a21b105959e02f24a5a2", "new_window": "86991b70166fd3acb09c"}, - {"doc": "STFSpec/informal/DISCREPANCIES.md", "line": 28, "target": "src/ethereum/forks/amsterdam/vm/gas.py", "kind": "path", "old": "vm/gas.py:936", "new": "vm/gas.py:921", "window": "33f2149d67f2924ccf5f", "new_window": "3d0e3e67748a85e3184c"}, - {"doc": "STFSpec/informal/DISCREPANCIES.md", "line": 54, "target": "src/ethereum/forks/amsterdam/vm/precompiled_contracts/ripemd160.py", "kind": "path", "old": "precompiled_contracts/ripemd160.py:52", "new": "precompiled_contracts/ripemd160.py:49", "window": "1b7e837599a00a872dca", "new_window": "2be1937b60d10bb1c2ee"}, - {"doc": "STFSpec/informal/DISCREPANCIES.md", "line": 61, "target": "src/ethereum/forks/amsterdam/execution_engine/new_payload.py", "kind": "path", "old": "execution_engine/new_payload.py:60–68", "new": "execution_engine/new_payload.py:55–63", "window": "5f5418430aa8c8717af3", "new_window": "c217efaf95c46881ac36"}, + {"doc": "STFSpec/informal/DISCREPANCIES.md", "line": 30, "target": "src/ethereum/forks/amsterdam/fork.py", "kind": "path", "old": "fork.py:473", "new": "fork.py:448", "window": "c39ac175adc1278efc50", "new_window": "b031ea93a9b2665dd89a"}, + {"doc": "STFSpec/informal/DISCREPANCIES.md", "line": 30, "target": "src/ethereum/forks/amsterdam/vm/gas.py", "kind": "path", "old": "vm/gas.py:1011, 1046", "new": "vm/gas.py:996, 1031", "window": "3a7918a0d2dbeaf8a8a6", "new_window": "0f5fe77529a2cbbc387e"}, + {"doc": "STFSpec/informal/DISCREPANCIES.md", "line": 30, "target": "src/ethereum/forks/amsterdam/vm/gas.py", "kind": "path", "old": "vm/gas.py:146", "new": "vm/gas.py:137", "window": "a21b105959e02f24a5a2", "new_window": "86991b70166fd3acb09c"}, + {"doc": "STFSpec/informal/DISCREPANCIES.md", "line": 30, "target": "src/ethereum/forks/amsterdam/vm/gas.py", "kind": "path", "old": "vm/gas.py:936", "new": "vm/gas.py:921", "window": "33f2149d67f2924ccf5f", "new_window": "3d0e3e67748a85e3184c"}, + {"doc": "STFSpec/informal/DISCREPANCIES.md", "line": 56, "target": "src/ethereum/forks/amsterdam/vm/precompiled_contracts/ripemd160.py", "kind": "path", "old": "precompiled_contracts/ripemd160.py:52", "new": "precompiled_contracts/ripemd160.py:49", "window": "1b7e837599a00a872dca", "new_window": "2be1937b60d10bb1c2ee"}, + {"doc": "STFSpec/informal/DISCREPANCIES.md", "line": 63, "target": "src/ethereum/forks/amsterdam/execution_engine/new_payload.py", "kind": "path", "old": "execution_engine/new_payload.py:60–68", "new": "execution_engine/new_payload.py:55–63", "window": "5f5418430aa8c8717af3", "new_window": "c217efaf95c46881ac36"}, {"doc": "STFSpec/informal/EXCLUDED.md", "line": 11, "target": "src/ethereum/forks/amsterdam/stateless.py", "kind": "path", "old": "stateless.py:78–83", "new": "stateless.py:76–81", "window": "16d87bc955579dadea03", "new_window": "d5860b5f3b90e15c544f"}, {"doc": "STFSpec/informal/EXCLUDED.md", "line": 13, "target": "src/ethereum/forks/amsterdam/execution_engine/forkchoice_update.py", "kind": "path", "old": "forkchoice_update.py:16–26", "new": "forkchoice_update.py:12–22", "window": "18e1d6e26067be5669d3", "new_window": "790f5540632f65078ff7"}, {"doc": "STFSpec/informal/GAPS-CROSSCUTTING.md", "line": 20, "target": "src/ethereum/forks/amsterdam/fork.py", "kind": "path", "old": "fork.py:473", "new": "fork.py:448", "window": "b49943e0fca70253d59f", "new_window": "734632475a4eae312301"}, diff --git a/STFSpec/informal/modules/EthCommit.md b/STFSpec/informal/modules/EthCommit.md index f33eebd1..1360d5a6 100644 --- a/STFSpec/informal/modules/EthCommit.md +++ b/STFSpec/informal/modules/EthCommit.md @@ -1,6 +1,6 @@ # `EthCommit`: Merkle Patricia tries over bytes — mathematical root, witness decoding, partial trie, incremental root -*Status: informal specification, draft; §3 lists the supplied declarations and §10 the remaining work. Date: 2026-11-11. Pin: `tests-zkevm@v21.0.6` @59c1473d. Architecture: `STFSpec/informal/ARCHITECTURE.md`.* +*Status: informal specification, draft; §3 lists the supplied declarations and §10 the remaining work. Date: 2026-11-13. Pin: `tests-zkevm@v21.0.6` @59c1473d. Architecture: `STFSpec/informal/ARCHITECTURE.md`.* *Navigation: interface findings F4, F5, F16, F19, F20 (DECISIONS §3) · gate: [REVIEW §3](../REVIEW.md) · decisions: D4, D5, D16, D18, D19, D20, D25 · questions: B3 (Q32/Q34), B15 (Q33/Q35), Q48, Q49, Q50, Q51, Q52, Q53, Q54, Q55, Q59, Q60, Q90; DISC-001, DISC-003, DISC-004.* Abbreviations: `mpt:` = `merkle_patricia_trie.py`, `inc:` = `forks/amsterdam/incremental_mpt.py`, `ws:` = `forks/amsterdam/witness_state.py`. "[verified]" = read in the pinned source; "[executed]" = additionally run against the pinned EELS with `ethereum_rlp`/`ethereum_types` from the pinned environment; "[inference]" = argued, not tested. EELS `file:line` citations are at `59c1473d` except where marked and those listed in `STFSpec/informal/citation-remap-manual.txt`, which are still at `e1a316a0` (`tests-zkevm@v21.0.0`); verified observations are at `e1a316a0` unless marked as at `59c1473d` (GAPS-CROSSCUTTING X16). @@ -44,7 +44,7 @@ Abbreviations: `mpt:` = `merkle_patricia_trie.py`, `inc:` = `forks/amsterdam/inc Whole RLP decoding at `inc:929` must succeed before either field-shape check; malformed second fields or trailing bytes therefore win over Q52. Raw empty compact bytes fail with `compactEmpty` before interpreting item 1, while an empty decoded extension path fails with `pathEmpty` before child resolution. A descendant failure propagates unchanged through `inc:953` before the parent child-kind check at `:954`. Branch item 16 remains lenient; `leafValueList` belongs only to a two-item leaf. The complete C14 dispatcher is implemented in §3; WitnessError/guest adapters remain unimplemented. - C15. `_resolve_child_ref` (`inc:885–907`): an empty string → no child; a string of length ≠ 32 → malformed; a 32-byte string present in the DB → decode that entry (recursively, eager); absent → an **unresolved stub** `HashedNode h` (not an error); an inline list → decode `rlp.encode(list)`. - C16. **Accepted non-canonical encodings** [executed; each reachable only with a trie that no canonical state produces]: (a) hex-prefix flag bits 2–3 set or a non-zero padding nibble (C3); (b) an inline child whose RLP is ≥ 32 bytes (it is then given a cached hash, C18); (c) a hash reference to a DB entry shorter than 32 bytes; (d) a branch value that is a list (read as empty); (e) a leaf with an empty value or a path whose length does not match its depth; (f) a child reference equal to `EMPTY_TRIE_ROOT`: if the DB contains the entry `0x80`, it decodes to **no child**, otherwise it is a stub — so adding the "unused" entry `0x80` can turn an accepted witness into a rejected one (occupancy drops below 2) [executed]. The Lean decoder must reproduce these outcomes exactly (P2), and the agreement theorem (§7.4) covers them through its collision disjunct. -- C17. **Cycles and sharing.** EELS recurses without a visited set: a reference cycle ends in `RecursionError`, caught as `false` (O12, classified O4 by CONTRACT); the Lean decoder tracks the hashes on the current path and returns `malformed` on a repeat. A DB built by C12 can contain a cycle only through a Keccak fixpoint chain, which cannot be ruled out in Lean without an assumption, so totality needs the check (ARCHITECTURE §5.4). A **shared** hash reached along two paths is decoded twice by EELS; on a DAG-shaped witness this is exponential in depth (16 identical children per level) [inference from `inc:885–907`]. Memoising completed, validated decodings must preserve mathematical decoding and raw encodings (§7.6). This is the DAG memo of DISC-004/B15, internal to one `decodeRoot`; it is not the per-root storage-trie memo of `EthStateWitness` (F6, open). Q55's mathematical traversal baseline has no completed-node memo: repeated sibling references are distinct occurrences. B15 does not select a memo here; effect suppression, shared stateful answers and path-dependent cached failures require explicit refinement premises. Its effect on host-resource acceptance requires D14/O12 treatment. Deep acyclic inputs can exceed Python's recursion limit in EELS (the guest-process limit is 100,000; py_ecc raises it, and 12,288 applies only after `import ethereum`). For chains of trie nodes the limit no longer decides the guest output: a chain beyond the secured bound (C13, Q90) is `.malformed .securedPathLength` here and `AssertionError` or `RecursionError` in EELS, all `false` at the guest. This holds for the definition; the executable's memory grows with the square of chain depth (DISC-001, DEBT.md). RLP nesting inside one node's branch value is not bounded by that check, and can exceed the limit in EELS where this decoder accepts (DISC-003). Measurements: DISC-001 (O12 unresolved). +- C17. **Cycles and sharing.** EELS recurses without a visited set: a reference cycle ends in `RecursionError`, caught as `false` (O12, classified O4 by CONTRACT); the Lean decoder tracks the hashes on the current path and returns `malformed` on a repeat. A DB built by C12 can contain a cycle only through a Keccak fixpoint chain, which cannot be ruled out in Lean without an assumption, so totality needs the check (ARCHITECTURE §5.4). A **shared** hash reached along two paths is decoded twice by EELS; on a DAG-shaped witness this is exponential in depth (16 identical children per level) [inference from `inc:885–907`]. Memoising completed, validated decodings must preserve mathematical decoding and raw encodings (§7.6). This is the DAG memo of DISC-004/B15, internal to one `decodeRoot`; it is not the per-root storage-trie memo of `EthStateWitness` (F6, open). Q55's mathematical traversal baseline has no completed-node memo: repeated sibling references are distinct occurrences. B15 does not select a memo here; effect suppression, shared stateful answers and path-dependent cached failures require explicit refinement premises. Its effect on host-resource acceptance requires D14/O12 treatment. Deep acyclic inputs can exceed Python's recursion limit in EELS (the guest-process limit is 100,000; py_ecc raises it, and 12,288 applies only after `import ethereum`). For chains of trie nodes the limit no longer decides the guest output: a chain beyond the secured bound (C13, Q90) is `.malformed .securedPathLength` here and `AssertionError` or `RecursionError` in EELS, all `false` at the guest. This holds for the definition; the executable's memory grows with the square of chain depth (DISC-001, DEBT.md). RLP nesting inside one branch value is not bounded by that path check. The recorded deep probes are raw-decoder observations outside normal guest node admission, as qualified in DISC-001; they establish no admitted guest divergence. Measurements and remaining host cases: DISC-001 (O12 unresolved). - C18. **Cached encodings.** A decoded node keeps its original bytes and, iff they are ≥ 32 bytes, their hash (`inc:925–927`, `:948–949`, `:960–961`, `:979–981`). Source child embedding (`inc:290–316`) uses empty bytes for none, the supplied hash for a stub, and an unmodified diff --git a/STFSpec/informal/modules/EthStateless.md b/STFSpec/informal/modules/EthStateless.md index 9d1f7585..a155f935 100644 --- a/STFSpec/informal/modules/EthStateless.md +++ b/STFSpec/informal/modules/EthStateless.md @@ -1,6 +1,6 @@ # `EthStateless`: the stateless guest (bytes → bytes), payload validation and header chain -*Status: informal specification, draft; protocol fork metadata, input wire-limit aliases, raw execution witness, five request-item carriers, request aggregate, raw payload/request carriers and actual witness/payload SSZ dictionaries with Q81 certificates, output record, serializer and zero sentinel supplied; guest unimplemented. Date: 2026-11-11. Pin: `tests-zkevm@v21.0.6` @59c1473d. Architecture: `STFSpec/informal/ARCHITECTURE.md`.* +*Status: informal specification, draft; protocol fork metadata, input wire-limit aliases, raw execution witness, five request-item carriers, request aggregate, raw payload/request carriers and actual witness/payload SSZ dictionaries with Q81 certificates, output record, serializer and zero sentinel supplied; guest unimplemented. Date: 2026-11-13. Pin: `tests-zkevm@v21.0.6` @59c1473d. Architecture: `STFSpec/informal/ARCHITECTURE.md`.* *Navigation: interface findings F1, F2, F4, F13, F14, F18, F20 (DECISIONS §3) · gate: [REVIEW §3](../REVIEW.md) · decisions: D3, D5, D8, D13, D14, D18, D19 · questions: B12 (Q4), Q5, Q6/Q20, Q88, O2, O13.* Source references are to `src/ethereum/forks/amsterdam/` unless another path is given. **[V]** marks a claim checked by reading the pinned source or by running the pinned EELS or the pinned fixtures (environment and reproduction: [REVIEW §2](../REVIEW.md)); **[I]** marks an inference. EELS `file:line` citations are at `59c1473d` except where marked and those listed in `STFSpec/informal/citation-remap-manual.txt`, which are still at `e1a316a0` (`tests-zkevm@v21.0.0`); verified observations are at `e1a316a0` unless marked as at `59c1473d` (GAPS-CROSSCUTTING X16). @@ -941,7 +941,7 @@ See [COMPOSITION](../COMPOSITION.md) for how these premises are supplied and [RE - **`DecodingError` versus other exceptions in `_decode_header`.** The fallback fires only on `rlp.DecodingError`. If `ethereum-rlp` 0.1.6 raises another exception type for some malformed Amsterdam header (for example from a field constructor), EELS skips the fallback; the output is the same (inner failure), but the constructor differs. Unchecked. - **Missing BLOCKHASH ancestor** is a Python negative-index `IndexError` (`vm/instructions/block.py:58`), fixture-witnessed. It is O13 with the named constructor `VmFault.ancestorHashUnavailable` (`EthVmCore`/`EthVmInstructions`), not O4 or O6 (R5). Note that an ancestor deeper than the witness but within 256 blocks fails the block, while one beyond 256 returns zero without touching the witness. - **O2** has no fixture and no reachable spec path; L-root is unproved (open, DECISIONS §3 O2). If a future SSZ type made `hash_tree_root` partial (e.g. a resource limit), the constructor would be needed. -- **O12 candidates (DISC-001, unresolved).** The guest-process recursion limit is 100,000 (py_ecc raises it; `import ethereum` alone gives 12,288). (a) Deep RLP nesting in a witness header or transaction: 20,000 levels decode and 40,000 raise `RecursionError` in `ethereum-rlp` (witnessed by probe inputs). For a transaction it is caught inside `is_valid_versioned_hashes` and becomes O6 (DISC-006); for a header, in the inner phase. Since valid headers and transactions have bounded nesting, the output probably coincides with the spec's structural failure [I]. (b) Eager witness decoding (`incremental_mpt.py:885–1065`) recurses without a depth limit. For chains of trie nodes this no longer gives a divergence: every guest decode is secured, and EELS's path check (`incremental_mpt.py:987–1013`) or its recursion limit and the Q90 decoder all give `false` (EthCommit C17) [I, by reading]. RLP nesting inside a witness node's branch value is not bounded by the check: beyond a host-dependent depth EELS raises `RecursionError` (→ `false`), while the spec's total decoder accepts the node and reads the value as empty (DISC-003). This is a guest-level divergence on crafted inputs, uncovered by fixtures, and needs a decision with `EthStateWitness`; DISC-001 has the decode-level reproducer. +- **O12 candidates (DISC-001, unresolved).** DISC-001 owns the historical host measurements and their input/environment qualifications; DISC-006 owns the payload-transaction exception-catching phase. Secured deep trie-node chains remain subject to Q90/EthCommit C13/C17. Raw within-node RLP nesting is not bounded by that path check, but the recorded 33,330/33,331-depth nodes exceed the normal guest's per-node ByteList[1024] admission limit. They cannot demonstrate a guest divergence through that entrypoint. Witness headers are also byte-limited at SSZ admission; raw header probes likewise require that boundary to be checked before assigning a guest phase. Other admitted cross-node/DAG or host-resource cases remain separate investigations. A guest-level discrepancy requires an input admitted by the actual schema and observation of the complete guest path. - **Input size envelope.** Transactions, the BAL bytes and the progressive lists are unbounded in SSZ; the largest fixture input is 8.4 MB. There is no stated maximum input, memory or cycle envelope; `EthBase`'s `Envelope` record does not yet cover the guest. - **SSZ progressive types.** Correctness of `ProgressiveContainer`/progressive-list decoding and merkleization rests on `eth-remerkleable` 0.1.31 (EIP-7495/EIP-7916 as implemented there). EthCodec implements progressive merkleization, roots and forward encoding (Q75, Q79, Q80); progressive decoding is specified (Q88) but unimplemented, and no independent reference beyond `eth-remerkleable` 0.1.31 is pinned. - **`payloadHeader` totality** is inferred: EELS catches any exception there, and the spec asserts none can occur on decoded values. Needs a line-by-line check of `Header` field constructors (e.g. `Uint`/`U256` widening, `Bytes8`).