Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 13 additions & 5 deletions STFSpec/Conformance/Commit/deep_chain_probe.py
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -109,14 +112,19 @@ 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"")
outcome = "ok"
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__":
Expand Down
4 changes: 2 additions & 2 deletions STFSpec/informal/DECISIONS.md
Original file line number Diff line number Diff line change
@@ -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 |
|---|---|
Expand Down Expand Up @@ -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. |
Expand Down
5 changes: 3 additions & 2 deletions STFSpec/informal/DISCREPANCIES.md
Original file line number Diff line number Diff line change
@@ -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

Expand All @@ -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.
Expand Down
4 changes: 2 additions & 2 deletions STFSpec/informal/GAPS-CROSSCUTTING.md
Original file line number Diff line number Diff line change
@@ -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.

Expand All @@ -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).

Expand Down
8 changes: 4 additions & 4 deletions STFSpec/informal/GAPS.md
Original file line number Diff line number Diff line change
@@ -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.

Expand All @@ -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).

Expand Down Expand Up @@ -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`).
Expand Down
Loading
Loading