Proposal: hash-based post-quantum signature lane (Generalized XMSS / leanSig) over a tweakable hash

[Abraxas1010]

Per CONTRIBUTING's blueprint-first process for large contributions, this is a proposal for discussion before any implementation PR.

What

A Signatures/HashBased/ lane formalizing the Generalized XMSS / HyperTree signature over a tweakable hash — the scheme adopted for the lean-Ethereum consensus layer as leanSig (Drake–Khovratovich–Kudinov–Wagner, CiC 2025 / ePrint 2025/055, whose introduction explicitly calls for formal verification of the verifier). Together with the in-flight lattice work in VCV-io (Falcon Verified-zkEVM/VCVio#466, ML-DSA Verified-zkEVM/VCVio#467), this would complete hash-based coverage of the NIST-PQ triangle — and it is the leg whose security rests solely on symmetric primitives, i.e. the same trust base as the Merkle commitments underlying this repo's IOP stack.

What we bring

We hold a complete Lean 4 development of the scheme (kernel-checked, sorry-free) that we would re-author against VCV-io's OracleComp/game infrastructure rather than transplant:

• tweakable-hash abstraction with target collision resistance (TCR) as the single named assumption;
• target-sum Winternitz / incomparable encodings with a genuine encoding-soundness theorem;
• index-directed Merkle authentication paths with per-level tweaks, with completeness and a TCR-binding theorem that pins both the leaf and the path — with no random oracle (a deterministic complement to the ROM extractability development in MerkleTree/Inductive/);
• the full scheme correctness theorem verify ∘ sign = true, consuming the encoding and path theorems by name;
• executable decoders for the production leanSig wire format (KoalaBear field, 52-byte pk / 2536-byte sig), differentially tested against leanEthereum/leanSpec and leansig-test-keys — so the formalization is anchored to the real object, not a paper idealization;
• an explicit assumption ledger separating what is proven from what is stated (unforgeability from TCR is currently a typed statement; the VCV-io game framework is exactly where it should become a proof, and we propose it as the lane's capstone).

Proposed phasing (one reviewable PR each): (1) TweakableHash + TCR game; (2) tweaked Merkle paths + completeness/binding; (3) XMSS correctness; (4) unforgeability reduction; (5) leanSig production instantiation (Poseidon2/KoalaBear, ties into ArkLib/Data/Hash/Poseidon2.lean) + test-vector harness.

Context

First contribution in this direction is Verified-zkEVM/VCVio#473 (batch Merkle openings, issue #4's next checkbox). Methodology exhibit: our July 2026 paper Run and Prove at Once — every claim labeled proven/reported/open, per-theorem axiom footprints, provably-false naive residuals stated up front.

Asks

1. Is a hash-based signature lane welcome, and is VCV-io (beside Falcon/ML-DSA) the right home, with the leanSig instantiation possibly in ArkLib where Poseidon2 lives?
2. Feedback on reusing/parameterizing the MerkleTree/Inductive machinery for tweaked (per-level keyed) paths.
3. Any naming/structure preferences before phase 1.

---

Proposed by The Institute for Ontological Mathematics (IAOM) / Equation Capital dba Apoth3osis.

[Abraxas1010]

Two updates after a closer read of the VCV-io tree:

Blueprint correction. VCV-io already carries the two abstractions I listed as phase 1 — CryptoFoundations/TweakableHash.lean and the SM-PRE / SM-TCR games in HardnessAssumptions/MultiTarget.lean — so the lane starts one rung higher than proposed. Revised phasing: (1) tweaked Merkle paths over the existing TweakableHash; (2) Winternitz / target-sum chains + incomparable encodings; (3) Generalized XMSS correctness; (4) unforgeability from MultiTarget.TcrProblem; (5) leanSig production instantiation (Poseidon2/KoalaBear) + test-vector harness.

Phase 1 is now delivered as Verified-zkEVM/VCVio#474: tweaked build/putative-root with per-level tweaks, completeness (zero-axiom), and a constructive binding kernel returning a tweak-tagged collision — two distinct pairs colliding under the same tweak, which is literally the win-condition shape of MultiTarget.TcrProblem. So the bridge from tree binding to SM-TCR needs no new collision notion.

Also relevant to this lane: VCV-io#473 now includes BatchToSingle.lean, and batch openings are what an aggregated-signature verifier opens.

The Institute for Ontological Mathematics (IAOM) / Equation Capital dba Apoth3osis.

[alexanderlhicks]

seems like this should be reserved for VCV?

[Abraxas1010]

Understood, and agreed — every primitive this lane needs (TweakableHash, the SM-PRE / SM-TCR games in HardnessAssumptions/MultiTarget.lean, the Merkle development) lives in VCV, and none of it is in ArkLib.

Refiled there as Verified-zkEVM/VCVio#505, carrying over the revised phasing. Phase 1 remains Verified-zkEVM/VCVio#474. Nothing further is asked of ArkLib on this thread.

The Institute for Ontological Mathematics (IAOM) / Equation Capital dba Apoth3osis.