perf(EthCommit): share the decoder's current-path set between levels

.github/workflows/ci.yml

@@ -224,6 +224,10 @@ jobs:
         run: |
           lake build log-rope-bench --wfail
           lake exe check-decls LogRopeBench
+      - name: Decoder depth diagnostic build and declaration audit
+        run: |
+          lake build decoder-depth-bench --wfail
+          lake exe check-decls DecoderDepthBench
       - name: Packed Keccak benchmark build, declaration audit and generator freshness
         run: |
           lake build packed-keccak-bench --wfail

STFSpec/Commit/Decoder.lean

@@ -4,22 +4,24 @@ Copyright (c) 2026 The STFspec Contributors. Licensed under Apache-2.0 OR MIT.
 import STFSpec.Commit.IncrementalMPT
 import STFSpec.Commit.NodeDB
 import STFSpec.Commit.Compact
-import Std.Data.HashSet.Lemmas
+import Std.Data.TreeSet.Lemmas
 
 /-!
 # Complete eager witness decoding
 
 Library `EthCommit`. Pinned EELS `src/ethereum/forks/amsterdam/incremental_mpt.py:885–1065`.
 Actual query answers and original raw encodings are retained. Database keys detect
-current-path cycles; siblings remain independent occurrences. The two termination
+current-path cycles; siblings remain independent occurrences. The current path is a
+persistent ordered set: each level shares its parent's set and adds O(log d) nodes, so
+a chain of depth d holds O(d log d) set nodes rather than O(d²) (EthCommit C17). The two termination
 measures occur only in proofs, imposing no runtime bound or admission predicate.
 Spec guidance: `STFSpec/informal/modules/EthCommit.md` C13–C17; Q55.
 -/
 
 namespace STFSpec.Commit
 open STFSpec.Base STFSpec.Hash STFSpec.Codec
 
-private theorem remaining_insert_lt (db : NodeDB) (path : Std.HashSet Hash32)
+private theorem remaining_insert_lt (db : NodeDB) (path : Std.TreeSet Hash32 compare)
     (key : Hash32) (present : db.map.contains key = true)
     (fresh : path.contains key = false) :
     (db.map.keys.filter (fun k => !(path.insert key).contains k)).length <
@@ -28,37 +30,36 @@ private theorem remaining_insert_lt (db : NodeDB) (path : Std.HashSet Hash32)
     rw [Std.HashMap.contains_keys]
     exact present
   obtain ⟨k, hk, hbeq⟩ := List.contains_iff_exists_mem_beq.mp hkeys
-  have hkfresh : path.contains k = false := by
-    rw [← Std.HashSet.contains_congr hbeq]
-    exact fresh
-  have hkmem : k ∈ db.map.keys.filter (fun k => !path.contains k) :=
-    List.mem_filter.mpr ⟨hk, by simp only [hkfresh, Bool.not_false]⟩
+  have hkk : key = k := by simpa using hbeq
+  subst hkk
+  have hkmem : key ∈ db.map.keys.filter (fun k => !path.contains k) :=
+    List.mem_filter.mpr ⟨hk, by simp only [fresh, Bool.not_false]⟩
   have filter_eq :
       (db.map.keys.filter (fun k => !path.contains k)).filter (fun k => !(key == k)) =
         db.map.keys.filter (fun k => !(path.insert key).contains k) := by
     rw [List.filter_filter]
     congr 1
     funext k
-    simp only [Std.HashSet.contains_insert, Bool.not_or]
+    simp only [Std.TreeSet.contains_insert, Std.compare_beq_eq_beq, Bool.not_or]
   rw [← filter_eq]
   have hle := List.length_filter_le (fun k => !(key == k))
     (db.map.keys.filter (fun k => !path.contains k))
   have hne : ((db.map.keys.filter (fun k => !path.contains k)).filter
       (fun k => !(key == k))).length ≠
       (db.map.keys.filter (fun k => !path.contains k)).length := by
     intro heq
-    have hkeep := List.length_filter_eq_length_iff.mp heq k hkmem
-    simp only [hbeq, Bool.not_true, Bool.false_eq_true] at hkeep
+    have hkeep := List.length_filter_eq_length_iff.mp heq key hkmem
+    simp only [beq_self_eq_true, Bool.not_true, Bool.false_eq_true] at hkeep
   omega
 
-private theorem inserted_key_on_path (onPath : Std.HashSet Hash32) (key : Hash32) :
+private theorem inserted_key_on_path (onPath : Std.TreeSet Hash32 compare) (key : Hash32) :
     (onPath.insert key).contains key = true := by
-  simp [Std.HashSet.contains_insert]
+  simp [Std.TreeSet.contains_insert, Std.ReflOrd.compare_self]
 
-private theorem ancestor_stays_on_path (onPath : Std.HashSet Hash32)
+private theorem ancestor_stays_on_path (onPath : Std.TreeSet Hash32 compare)
     (key ancestor : Hash32) (present : onPath.contains ancestor = true) :
     (onPath.insert key).contains ancestor = true := by
-  simp [Std.HashSet.contains_insert, present]
+  simp [Std.TreeSet.contains_insert, present]
 
 /-- Continuation form preserves the exact plain-Monad bind tree. -/
 private def acquire {m : Type → Type} [Monad m] [KeccakQuery m]
@@ -171,7 +172,7 @@ decreasing_by
   omega
 
 private def decodeEntry {m : Type → Type} [Monad m] [KeccakQuery m]
-    (db : NodeDB) (onPath : Std.HashSet Hash32) (key : Hash32)
+    (db : NodeDB) (onPath : Std.TreeSet Hash32 compare) (key : Hash32)
     (raw : ByteArray) (_hlookup : db.map[key]? = some raw) :
     m (Except TrieError Ref) :=
   if _hcycle : onPath.contains key then pure (.error (.malformed .cycle)) else
@@ -185,7 +186,7 @@ termination_by (db.map.keys.filter (fun k => !onPath.contains k)).length
 decreasing_by
   apply remaining_insert_lt
   · simp [Std.HashMap.contains_eq_isSome_getElem?, _hlookup]
-  · simpa using _hcycle
+  · exact Bool.eq_false_iff.mpr _hcycle
 
 private theorem acquire_short {m : Type → Type} [Monad m] [KeccakQuery m]
     (raw : ByteArray) (next : Option Hash32 → m (Except TrieError Ref))
@@ -211,7 +212,7 @@ private theorem resolveChildren_cons {m : Type → Type} [Monad m]
         pure (tail.map (child :: ·))) := rfl
 
 private theorem entry_cycle {m : Type → Type} [Monad m] [KeccakQuery m]
-    (db : NodeDB) (onPath : Std.HashSet Hash32) (key : Hash32)
+    (db : NodeDB) (onPath : Std.TreeSet Hash32 compare) (key : Hash32)
     (raw : ByteArray) (lookup : db.map[key]? = some raw)
     (cycle : onPath.contains key = true) :
     decodeEntry (m := m) db onPath key raw lookup = pure (.error (.malformed .cycle)) := by
@@ -226,7 +227,7 @@ private theorem resolve_empty {m : Type → Type} [Monad m] (db : NodeDB)
     resolveRef db (.bytes ByteArray.empty) entry inline = pure (.ok none) := rfl
 
 private theorem entry_fresh {m : Type → Type} [Monad m] [KeccakQuery m]
-    (db : NodeDB) (onPath : Std.HashSet Hash32) (key : Hash32)
+    (db : NodeDB) (onPath : Std.TreeSet Hash32 compare) (key : Hash32)
     (raw : ByteArray) (lookup : db.map[key]? = some raw)
     (fresh : onPath.contains key = false) :
     decodeEntry (m := m) db onPath key raw lookup =
@@ -286,7 +287,7 @@ def decodeRoot {m : Type → Type} [Monad m] [KeccakQuery m]
   if r = emptyRoot then pure (.ok none) else
     match h : db.map[r]? with
     | none => pure (.error (.missingRoot r))
-    | some raw => decodeEntry db {} r raw h
+    | some raw => decodeEntry db ∅ r raw h
 
 /-- The 64-nibble key length of a secured trie (`SECURED_TRIE_KEY_NIBBLES`).
 EELS `src/ethereum/forks/amsterdam/incremental_mpt.py:47` at the pin. -/

STFSpec/informal/DEBT.md

@@ -1,6 +1,6 @@
 # Technical-debt register (D18)
 
-**Status (2026-11-11):** current register under D18. The P3 move to Lean v4.35.0 (2026-11-05) triggered the toolchain-update reviews below. After normalizing variable numbering, the generated C of each cited function is identical on v4.35.0 and v4.34.0, so the static code-shape evidence still holds. Outside the cited functions, v4.35.0 drops one dead bounds test (`n ≤ n`) from the private `FixedBytes` `decodeFast`. The timing, peak-memory and allocation measurements below were made on Lean 4.34.0 and were not repeated. v4.35.0 changes the runtime allocator and scalar-array copying, and bundles clang 23.1.0 in place of 22.1.4. The outstanding entries below record local performance exceptions. Known candidates: per-query storage-trie decoding in the witness backend, pending the memo design (DECISIONS F6); and the witness decoder's on-path set, copied at every level of `decodeEntry`, which makes memory grow with the square of chain depth (EthCommit C17, DISC-001). An entry needs a committed reproducer and benchmark.
+**Status (2026-11-13):** current register under D18. The P3 move to Lean v4.35.0 (2026-11-05) triggered the toolchain-update reviews below. After normalizing variable numbering, the generated C of each cited function is identical on v4.35.0 and v4.34.0, so the static code-shape evidence still holds. Outside the cited functions, v4.35.0 drops one dead bounds test (`n ≤ n`) from the private `FixedBytes` `decodeFast`. The timing, peak-memory and allocation measurements below were made on Lean 4.34.0 and were not repeated. v4.35.0 changes the runtime allocator and scalar-array copying, and bundles clang 23.1.0 in place of 22.1.4. The outstanding entries below record local performance exceptions. Known candidate: per-query storage-trie decoding in the witness backend, pending the memo design (DECISIONS F6). The witness decoder's on-path set, a candidate from 2026-11-11 whose copies made memory grow with the square of chain depth, became a persistent set on 2026-11-13 (EthCommit C17, DISC-001).
 
 Use one entry per local, correct and complete implementation whose data structure or algorithm is **not** performance-appropriate, justified on grounds of legibility or drastic proof-friendliness (D18). Missing semantics, proof holes required for release, unproved fuel sufficiency and protocol deviations are not performance debt. Protocol discrepancies belong in [`STFSpec/informal/DISCREPANCIES.md`](DISCREPANCIES.md).
 

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
 
@@ -18,7 +18,7 @@ Status: no accepted deviations. Date: 2026-11-11. This register implements the r
   - 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.
   - 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.
+  - 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 used to grow with the square of chain depth, because each level of `decodeEntry` copied a shared on-path `Std.HashSet`; a chain of 100,000 nodes, about 10 MB of witness with no node-count limit, ran out of memory near 79 GB (independent review run, 2026-11-11). Since 2026-11-13 the on-path set is a persistent `Std.TreeSet` (EthCommit C17), costing O(d log d) set nodes for a chain of depth d. Measured with `scripts/DecoderDepthBench.lean` (Lean v4.35.0, 2026-11-13; synthetic full-width keys, constant oracle), peak memory went from 1,007 MB to 55 MB at depth 10,000 and from 5,778 MB to 92 MB at 25,000; it is 299 MB at 100,000 and 583 MB at 200,000, about 3 KB per level. A wide trie of 640,001 entries peaks at 228 MB either way [V, by running].
 - **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.
 - **Resolution:** pending reproducer, upstream issue/response and accepted decision record. D14 confirmation alone must not silently authorize an unspecified O12 deviation.