fix(Security): pin the tree-based extractor and guard distinctShape arity

.agents/upstream-texts/issue.md

@@ -0,0 +1,142 @@
+Title: Tree special soundness: existential extractor carries no algorithmic content; distinctShape admits arity 0
+
+Body:
+
+> Not done in this wave: no issue or pull request was filed upstream, and no full-repository build
+> was run locally. The subsequent fork CI clean-build for head `8ffa15d0` in
+> [fork CI run 30519277986](https://github.com/Eduardogbg/ArkLib/actions/runs/30519277986)
+> passed with `Build completed successfully (4122 jobs)`. The overall workflow remained red only
+> because its later validation-wrapper step reported the unrelated knowledge-base error
+> `Paper page without matching BibTeX key: docs/kb/papers/NOZ26.md`. This wave rebuilt the fix as
+> two independent branches from `main` at `fad5cbf808774838924dc8273715724c6a6caa1f`, reran the
+> probe below, and completed targeted builds of every touched Security module. The sorry delta is
+> zero.
+
+Two related observations concern
+[`Verifier.treeSpecialSound`](https://github.com/Verified-zkEVM/ArkLib/blob/fad5cbf808774838924dc8273715724c6a6caa1f/ArkLib/OracleReduction/Security/TranscriptTree/Basic.lean#L292-L316)
+and
+[`distinctShape` / `specialSound`](https://github.com/Verified-zkEVM/ArkLib/blob/fad5cbf808774838924dc8273715724c6a6caa1f/ArkLib/OracleReduction/Security/SpecialSoundness.lean#L38-L93).
+
+## 1. The existential extractor carries no algorithmic content
+
+`Verifier.treeSpecialSound` quantifies the extractor existentially over a bare function:
+
+```lean
+∃ E : Extractor.TreeBased StmtIn WitIn pSpec S.arity,
+∀ stmtIn tree, tree.IsStructured S → tree.IsAccepting … →
+  (stmtIn, E stmtIn tree) ∈ relIn
+```
+There is no computability or cost condition on `E`. With `[Inhabited WitIn]`, this is classically
+equivalent to the extractor-free implication that every statement admitting a structured accepting
+tree lies in `relIn.language`: `Classical.choice` manufactures the function. The `Inhabited`
+assumption is needed only in the reverse direction, to define the function away from structured
+accepting trees. The forward implication needs no such assumption.
+
+This matters for the planned rewinding layer: that reduction must run one concrete extractor on the
+tree it produces, so an existentially hidden function is not a usable interface. The
+signature-preserving fix is to expose
+
+```lean
+def treeSpecialSoundWith … (E : Extractor.TreeBased …) : Prop := …
+def treeSpecialSound … : Prop := ∃ E, treeSpecialSoundWith … E
+```
+
+and certify the old inline statement with `treeSpecialSound_iff : … := Iff.rfl`.
+
+There is already an upstream consumer pointing in this direction. PR
+[#602](https://github.com/Verified-zkEVM/ArkLib/pull/602) added
+[`treeSpecialSound_of_isEmpty_challengeIdx`](https://github.com/Verified-zkEVM/ArkLib/blob/fad5cbf808774838924dc8273715724c6a6caa1f/ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/NoChallenge.lean#L104-L114):
+it takes concrete extractor data `e`, builds the corresponding tree extractor, and immediately
+closes the existential. The pinned predicate makes that concrete data available to downstream
+consumers instead of hiding it again.
+
+## 2. `distinctShape` admits arity zero
+
+At `arity i = 0`, a challenge node has no children. Consequently:
+
+- `IsStructured (distinctShape fun _ => 0)` is vacuous (`Function.Injective` on `Fin 0`);
+- `IsAccepting` is vacuous for every verifier and statement because `fullTranscripts` is empty.
+
+Therefore `specialSound` at arity zero requires an input witness for every statement and is
+unsatisfiable for any relation whose language is not universal. The coordinate-wise notion already
+rules this out with `CWSSStructure.soundnessParam : … → {k // 2 ≤ k}`.
+
+The proposed guard uses the same subtype:
+
+```lean
+def distinctShape (k : pSpec.ChallengeIdx → {k : ℕ // 2 ≤ k}) : …
+```
+
+`1 ≤ k` would remove the empty-tree vacuity, but `2` is the smallest arity with special-soundness
+extraction content and matches the existing CWSS convention. This is not a new downstream
+assumption: the existing bridge theorem
+[`toShape_ofSpecialSound_eq_distinctShape`](https://github.com/Verified-zkEVM/ArkLib/blob/fad5cbf808774838924dc8273715724c6a6caa1f/ArkLib/OracleReduction/Security/Implications.lean#L224-L243)
+already takes `hk : ∀ i, 2 ≤ k i` at line 229. The fix moves that existing consumer hypothesis onto
+the notion.
+
+## Machine-checked probe
+
+At `main` (`fad5cbf8`):
+
+```text
+$ lake env lean probes/TreeSpecialSoundProbes.lean
+$ echo $?
+0
+```
+
+On `fix/distinct-shape-arity-guard`, probe 1 elaborates before probe 2 and the first arity-zero use
+is rejected:
+
+```text
+probes/TreeSpecialSoundProbes.lean:78:55: error(lean.synthInstanceFailed):
+failed to synthesize instance of type class
+  OfNat { k // 2 ≤ k } 0
+```
+
+On the independent `fix/tree-special-sound-pinned` branch, the complete probe still exits zero:
+that branch deliberately preserves the original arity API and only exposes the pinned extractor
+form. The arity rejection belongs to the sibling guard branch.
+
+The relevant probe declarations are:
+
+```lean
+theorem treeSpecialSound_iff_language [Inhabited WitIn] … :
+    verifier.treeSpecialSound init impl S relIn relOut ↔
+      ∀ stmtIn,
+        (∃ tree, tree.IsStructured S ∧
+          tree.IsAccepting init impl verifier stmtIn relOut.language) →
+        stmtIn ∈ relIn.language := by
+  classical
+  unfold Verifier.treeSpecialSound
+  constructor
+  · rintro ⟨E, hE⟩ stmtIn ⟨tree, hStructured, hAccepting⟩
+    exact (Set.mem_language_iff relIn stmtIn).mpr
+      ⟨E stmtIn tree, hE stmtIn tree hStructured hAccepting⟩
+  · intro h
+    refine ⟨fun stmtIn tree =>
+      if h' : tree.IsStructured S ∧
+          tree.IsAccepting init impl verifier stmtIn relOut.language
+      then ((Set.mem_language_iff relIn stmtIn).mp (h stmtIn ⟨tree, h'⟩)).choose
+      else default,
+      fun stmtIn tree hStructured hAccepting => ?_⟩
+    have h' := And.intro hStructured hAccepting
+    simp only [dif_pos h']
+    exact ((Set.mem_language_iff relIn stmtIn).mp (h stmtIn ⟨tree, h'⟩)).choose_spec
+
+def zeroArityTree : ChallengeTree oneChalSpec (fun _ => 0) 0 :=
+  .chalNode 0 rfl Fin.elim0 Fin.elim0
+
+theorem zeroArityTree_isStructured :
+    zeroArityTree.IsStructured (distinctShape fun _ => 0) :=
+  ⟨fun a => a.elim0, fun j => j.elim0⟩
+
+theorem specialSound_zeroArity_forces_trivial_language …
+    (h : verifier.specialSound init impl (fun _ => 0) relIn relOut) :
+    ∀ stmtIn, stmtIn ∈ relIn.language := by
+  obtain ⟨E, hE⟩ := h
+  intro stmtIn
+  exact (Set.mem_language_iff relIn stmtIn).mpr
+    ⟨E stmtIn zeroArityTree,
+      hE stmtIn zeroArityTree zeroArityTree_isStructured
+        (zeroArityTree_isAccepting init impl verifier stmtIn relOut.language)⟩
+```

.agents/upstream-texts/pr-arity-guard.md

@@ -0,0 +1,91 @@
+Title: fix(security): guard distinct-shape arity
+
+Body:
+
+> Not done in this wave: no upstream PR was opened and no full-repository build was run. The
+> previously combined fork change passed fork CI on 2026-07-15. This split branch was rebuilt from
+> `main` at `fad5cbf808774838924dc8273715724c6a6caa1f`; targeted builds and the arity probe were rerun
+> here. The first two cold targeted-build invocations reached the 7200-second cap while populating
+> dependencies; the repeated command completed successfully. Sorry delta: `+0 / -0`.
+
+## Degenerate satisfaction at the current signature
+
+At arity zero, the challenge node has no children. The probe constructs such a tree and proves both
+obligations without using the verifier:
+
+```lean
+def zeroArityTree : ChallengeTree oneChalSpec (fun _ => 0) 0 :=
+  .chalNode 0 rfl Fin.elim0 Fin.elim0
+
+theorem zeroArityTree_isStructured :
+    zeroArityTree.IsStructured (distinctShape fun _ => 0) :=
+  ⟨fun a => a.elim0, fun j => j.elim0⟩
+
+theorem zeroArityTree_isAccepting … :
+    zeroArityTree.IsAccepting init impl verifier stmtIn langOut := by
+  intro tr htr
+  simp [zeroArityTree, ChallengeTree.fullTranscripts, ChallengeTree.transcripts] at htr
+```
+Thus arity-zero `specialSound` forces every statement into the input language and is unsatisfiable
+for non-universal languages.
+
+## Minimal fix
+
+Require the existing CWSS subtype at the three plain entry points:
+
+```lean
+def distinctShape (k : pSpec.ChallengeIdx → {k : ℕ // 2 ≤ k}) : …
+def Verifier.specialSound (k : pSpec.ChallengeIdx → {k : ℕ // 2 ≤ k}) …
+def OracleVerifier.specialSound (k : pSpec.ChallengeIdx → {k : ℕ // 2 ≤ k}) …
+```
+
+`ChallengeTree` and `ChallengeTreeShape` remain fully general. The bridge statements only package
+their already-present hypothesis as `fun i => ⟨k i, hk i⟩`; their proofs are otherwise unchanged.
+In particular,
+[`Implications.lean:229`](https://github.com/Verified-zkEVM/ArkLib/blob/fad5cbf808774838924dc8273715724c6a6caa1f/ArkLib/OracleReduction/Security/Implications.lean#L224-L243)
+already carries `hk : ∀ i, 2 ≤ k i` on
+`toShape_ofSpecialSound_eq_distinctShape`. This fix moves an existing consumer hypothesis onto the
+notion.
+
+The subtype excludes both the empty arity and the one-transcript case, matches
+`CWSSStructure.soundnessParam`, and leaves the `ℓ = 1` shape equality definitional after packaging
+`hk`.
+
+## Verification
+
+The exact baseline probe exits zero at `main`; on this branch the arity-zero instantiation is
+type-rejected:
+
+```text
+probes/TreeSpecialSoundProbes.lean:78:55: error(lean.synthInstanceFailed):
+failed to synthesize instance of type class
+  OfNat { k // 2 ≤ k } 0
+```
+
+Targeted build:
+
+```text
+$ lake build ArkLib.OracleReduction.Security.SpecialSoundness \
+    ArkLib.OracleReduction.Security.Implications
+⚠ [2969/2969] Built ArkLib.OracleReduction.Security.Implications (58s)
+warning: ArkLib/OracleReduction/Security/Implications.lean:48:8: declaration uses `sorry`
+…
+warning: ArkLib/OracleReduction/Security/Implications.lean:179:8: declaration uses `sorry`
+Build completed successfully (2969 jobs).
+```
+
+Those `Implications.lean` sorries predate this change. No touched declaration adds a sorry.
+
+`#print axioms`:
+
+```text
+'distinctShape' does not depend on any axioms
+'Verifier.specialSound' depends on axioms: [propext, Classical.choice, Quot.sound]
+'OracleVerifier.specialSound' depends on axioms: [propext, Classical.choice, Quot.sound]
+'toShape_ofSpecialSound_eq_distinctShape' depends on axioms:
+  [propext, Classical.choice, Quot.sound]
+'Verifier.coordinateWiseSpecialSound_ofSpecialSound_iff' depends on axioms:
+  [propext, Classical.choice, Quot.sound]
+'OracleVerifier.coordinateWiseSpecialSound_ofSpecialSound_iff' depends on axioms:
+  [propext, Classical.choice, Quot.sound]
+```

.agents/upstream-texts/pr-pinning.md

@@ -0,0 +1,115 @@
+Title: fix(security): pin tree-special-sound extractor
+
+Body:
+
+> Not done in this wave: no upstream PR was opened and no full-repository build was run locally.
+> The subsequent fork CI clean-build for head `8ffa15d0` in
+> [fork CI run 30519277986](https://github.com/Eduardogbg/ArkLib/actions/runs/30519277986)
+> passed with `Build completed successfully (4122 jobs)`. The overall workflow remained red only
+> because its later validation-wrapper step reported the unrelated knowledge-base error
+> `Paper page without matching BibTeX key: docs/kb/papers/NOZ26.md`. This independent branch was
+> rebuilt from `main` at `fad5cbf808774838924dc8273715724c6a6caa1f`; the touched Security module,
+> the compatibility probe, the positive witness, and guarded axiom reports were compiled locally
+> in this wave. Sorry delta: `+0 / -0`.
+
+## Degenerate satisfaction at the current signature
+
+The issue probe compiles at current `main` and proves that, with `[Inhabited WitIn]`, the bare
+existential is classically equivalent to an extractor-free language implication:
+
+```lean
+theorem treeSpecialSound_iff_language [Inhabited WitIn] … :
+    verifier.treeSpecialSound init impl S relIn relOut ↔
+      ∀ stmtIn,
+        (∃ tree, tree.IsStructured S ∧ tree.IsAccepting …) →
+        stmtIn ∈ relIn.language
+```
+
+The forward direction is hypothesis-free. The reverse direction uses `Classical.choice` to
+manufacture an extractor and `default` only away from structured accepting trees. Therefore the
+existential over a bare function has no computability or cost content.
+
+## Signature-preserving fix
+
+Expose the pinned form and keep the existing property as its existential closure:
+
+```lean
+def treeSpecialSoundWith … (E : Extractor.TreeBased …) : Prop :=
+  ∀ stmtIn tree, tree.IsStructured S → tree.IsAccepting … →
+    (stmtIn, E stmtIn tree) ∈ relIn
+
+def treeSpecialSound … : Prop :=
+  ∃ E, verifier.treeSpecialSoundWith init impl S relIn relOut E
+
+theorem treeSpecialSound_iff … : treeSpecialSound … ↔ ∃ E, ∀ stmtIn tree, … :=
+  Iff.rfl
+```
+
+No existing caller's statement changes. Composition code continues to consume the existential
+closure; future rewinding code can take `treeSpecialSoundWith` and run the concrete extractor.
+
+This seam matches an existing upstream use. PR
+[#602](https://github.com/Verified-zkEVM/ArkLib/pull/602) added
+[`treeSpecialSound_of_isEmpty_challengeIdx`](https://github.com/Verified-zkEVM/ArkLib/blob/fad5cbf808774838924dc8273715724c6a6caa1f/ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/NoChallenge.lean#L104-L114),
+which takes extractor data `e`, constructs a concrete tree extractor, and closes the existential
+immediately. The pinned form exposes exactly the intermediate fact that theorem already builds.
+
+## Positive non-vacuity witness
+
+Mirroring the role of `Verifier.id_knowledgeSoundness` in
+[#569](https://github.com/Verified-zkEVM/ArkLib/pull/569), this change proves the strengthened
+predicate at a concrete extractor:
+
+```lean
+theorem Verifier.id_treeSpecialSoundWith (S : ChallengeTreeShape !p[])
+    (relOut : Set (StmtIn × WitOut)) :
+    (Verifier.id : Verifier oSpec StmtIn StmtIn !p[]).treeSpecialSoundWith
+      init impl S {pair | pair.1 = pair.2} relOut (fun stmtIn _ => stmtIn) := by
+  intro stmtIn _ _ _
+  rfl
+```
+
+The identity verifier and the extractor that returns the input statement inhabit
+`treeSpecialSoundWith` for the diagonal relation. No assumption was added to make this theorem
+provable.
+
+## Verification
+
+On this branch, the complete issue probe exits zero:
+
+```text
+$ lake env lean probes/TreeSpecialSoundProbes.lean
+$ echo $?
+0
+```
+
+That includes probe 1 after the refactor. It also intentionally includes the arity-zero probe:
+this branch does not contain the independent arity guard. The sibling
+`fix/distinct-shape-arity-guard` branch is where that instantiation is type-rejected.
+
+Targeted build:
+
+```text
+$ lake build ArkLib.OracleReduction.Security.TranscriptTree.Basic
+✔ [2953/2953] Built ArkLib.OracleReduction.Security.TranscriptTree.Basic (7.0s)
+Build completed successfully (2953 jobs).
+```
+
+The in-file `#guard_msgs` checks compile these exact axiom reports:
+
+```text
+'Verifier.treeSpecialSoundWith' depends on axioms:
+  [propext, Classical.choice, Quot.sound]
+'Verifier.treeSpecialSound' depends on axioms:
+  [propext, Classical.choice, Quot.sound]
+'Verifier.treeSpecialSound_iff' depends on axioms:
+  [propext, Classical.choice, Quot.sound]
+'Verifier.id_treeSpecialSoundWith' depends on axioms:
+  [propext, Classical.choice, Quot.sound]
+```
+
+This follows the same validation shape as the merged vacuity fixes
+[#569](https://github.com/Verified-zkEVM/ArkLib/pull/569) and
+[#577](https://github.com/Verified-zkEVM/ArkLib/pull/577): compiled degenerate satisfaction first,
+minimal signature-preserving repair, a positive witness in the same change, and an explicit sorry
+and axiom report.