[alexanderlhicks]

The witness decoder's memory grew with the square of chain depth. This PR fixes that, following #408 (DISC-001, EthCommit C17).

Cause

The private decodeEntry tracked the hashes on the current path in a Std.HashSet. It inserted the child key inside a closure while the parent's set stayed live for the siblings, so every level copied the whole set. A chain of 100,000 nodes, about 10 MB of witness with no node-count limit, ran out of memory near 79 GB.

Change

• The set: the current path is now a persistent Std.TreeSet Hash32 compare.
  • Each level shares its parent's set and copies O(log d) tree nodes, so a chain of depth d costs O(d log d).
  • Hash32's lawful Ord (compareOn toNat, with LawfulEqOrd/TransOrd) makes compare-equality exactly Hash32 equality. Membership is therefore unchanged, and so is every result, error, query sequence and raw/cache field.
• Proofs: only private declarations change. The termination proof uses Std.TreeSet.contains_insert and Std.compare_beq_eq_beq. Every public law, guard and caller proof builds unchanged.
• Benchmark: new scripts/DecoderDepthBench.lean (lean_exe decoder-depth-bench), next to the other benches. CI builds it and runs the declaration audit on it, but does not run it.
  • Shapes: chain and wide.
  • Synthetic full-width keys and a constant oracle.
  • It checks the expected outcome before printing the time, and exits 1 on a mismatch.
• Docs: DISC-001 ("Spec executable") and EthCommit C17 and §3 describe the new set; the DEBT.md status line marks the 2026-11-11 candidate as resolved.

Measurements

Peak memory with decoder-depth-bench, Lean v4.35.0:

Input	Before	After
Chain of 10,000	1,007 MB	55 MB
Chain of 25,000	5,778 MB	92 MB
Chain of 100,000	out of memory near 79 GB (independent run)	299 MB
Chain of 200,000	—	583 MB
Wide trie, 640,001 entries	228 MB, 18.2 s decode	228 MB, 11.3 s decode

A separate runner with real Keccak, EELS-built inputs and two decodes per input measured, after the change:

• a chain of 49,996: 227 MB;
• a chain of 200,000: 689 MB;
• a branch value nested 1,000,000 deep: 555 MB, still accepted.

Time grows linearly with depth.

Verification

• decoder_differential.py at 59c1473d: 394 cases / 788 records, with full fields, query order and raw cache bytes, lean_exit 0.

• An independent check of 6,000 EELS-built tries (12,000 records): byte-identical output to the old decoder, and all agree with EELS.

• Repository checks:

  • lake build --wfail
  • scripts/check_decls.sh core (0 findings) and lake exe check-decls DecoderDepthBench (0 findings)
  • check_boundaries, check_spec, gen_gaps --check, remap_citations --check --eels and test_spec_checks
  • targeted leanchecker replay of the decoder, its guards and its caller proofs

• Independent adversarial review (CONTRIBUTING §5.5/§6.4) was CLEAN, with should-fixes:

  • O(d log d) wording;
  • the bench's correctness gate and CI audit;
  • full-width keys.

  All were applied. The delta review was CLEAN, and its lakefile-placement nit is applied.

Not in this PR

The nested-value divergence stays open (DISC-001, Q6/Q20): EELS raises RecursionError from 33,331 levels, and the spec accepts. Memory is no longer a factor, so the remaining choice is about matching EELS: a spec depth limit that matches the host, or an upstream report.

🤖 Generated with Claude Code

[alexanderlhicks]

Interim source review of bb5194f4a7452576c49e35eb58d0774d5a4325a8: one blocking documentation/evidence-scope finding under CONTRIBUTING §5.5. Full required validation is still pending; this is not a clean verdict.

The new description’s “Not in this PR” conclusion repeats the unresolved #408 finding: the oversized raw-decoder experiment does not establish an admitted-guest divergence or a choice of guest depth-limit policy. At the pin, stateless.py:35,46–49 limits each witness-state preimage to 1,024 bytes. A value nested 33,331 RLP-list levels exceeds that bound even before its branch wrapper. Guest SSZ admission rejects it before trie decoding.

Keep the direct-decoder measurements, but label their input domain explicitly. Correct the new description and qualify the edited C17/DISC-001 discussion so they do not infer guest disagreement from these inputs. The four inherited passages needing the same reconciliation are listed in the follow-up on #408. DAG expansion, cross-node chains and other resource questions remain separate; this finding does not settle them.

The complete seven-file source diff has not revealed a new decoder semantic defect: the private carrier replacement uses lawful Hash32 membership, while the traversal and query/error structure stay unchanged. This source assessment does not authenticate the reported historical runtime or timing campaigns. The 148 checklist commands and the two new benchmark build/audit commands still need current review validation.

Two nonblocking recommendations: qualify “Time grows linearly with depth” as an observation on the measured samples, and give every advertised benchmark mode an expected-outcome check (the current diagnostic explicitly only reports some modes).

[alexanderlhicks]

Final review of bb5194f4a7452576c49e35eb58d0774d5a4325a8 (tree 3d04980243adac0ef8e7b1d94dd5f61341a1ec8e): NOT_CLEAN. The material documentation finding in the earlier review remains open.

The new description and edited C17/DISC-001 discussion still infer an admitted-guest divergence or guest depth-policy choice from oversized raw-decoder probes. The pinned witness SSZ type limits each state preimage to 1,024 bytes; a single node with 33,331 nested list headers exceeds that domain. Retain the raw-decoder measurements with an explicit domain qualification, and reconcile the description and owned discussion with #408. Passing checks and the path-set improvement do not resolve this finding.

No new decoder semantic defect was identified. The private ancestor set now uses the lawful Hash32 ordering in a persistent TreeSet. Its membership contract preserves the same current-path keys, cycle checks, occurrence order, queries/errors and arbitrary-Monad action structure. Existing sibling/diamond, inline/root-seeded cycle, cache and first-error controls remain relevant; this review does not assert a newly proved whole-decoder equivalence theorem.

All 148 literal CONTRIBUTING §6.3 commands and both additional item-specific CI commands passed in each of three fresh isolated checkouts. Each lane audited 23,506 declarations with zero findings and replayed all 513 kernel modules. Both independent final reports, original closed command streams, all 22 checklist producer outputs per lane, source identities and byte-compared own-cache archives were authenticated. The two extra commands build and audit the diagnostic; they do not execute its performance workloads.

A separate bounded baseline/target diagnostic comparison was already reviewed and authenticated. Its synthetic keys, constant oracle, outcome gate, measured sizes and shared-host timing/RSS limits remain explicit. It establishes no general linear-time law, authenticated-trie or whole-guest/resource result. Please qualify the description's scaling statement as an observation at the measured sizes; this and the earlier request for expected-outcome checks in every advertised benchmark mode are nonblocking recommendations in addition to the material finding above. No historical differential/source campaign was repeated or credited as a current checklist pass.

The independent source audits retain their original chronology. Local uv 0.8.17 differs from CI's 0.13.6; literal uv/Python 3.12 commands were retained, without a claim of environment equivalence. No guest/EEST, source-world/dispatch, resource, security or readiness result is established. Current-main integration is separate. This review made no tracked edits, fixes, commits, pushes or merges.