Proposal: hash-based post-quantum signature lane (Generalized XMSS / leanSig) over the existing TweakableHash

[Abraxas1010]

Refiling here at maintainer direction: this lane was proposed as Verified-zkEVM/ArkLib#625 and closed on 25 July with "seems like this should be reserved for VCV?". That is the right call — every primitive the lane needs is already in this repository, and none of it is in ArkLib.

What the lane is

A verified development of the hash-based post-quantum signature family: Generalized XMSS in the shape used by SLH-DSA / SPHINCS+ and by the lean-Ethereum leanSig proposal, built over the existing TweakableHash abstraction. The interesting structural fact is that per-node/per-level domain separation is exactly what lets security rest on target-collision resistance rather than full collision resistance — so the abstraction CryptoFoundations/TweakableHash.lean plus the SM-PRE / SM-TCR games in HardnessAssumptions/MultiTarget.lean are the correct foundation, and both already exist here.

What already exists in VCVio

• CryptoFoundations/TweakableHash.lean — the tweakable hash abstraction.
• HardnessAssumptions/MultiTarget.lean — the SM-PRE / SM-TCR game surface.
• CryptoFoundations/MerkleTree/Inductive/* — the inductive Merkle tree, its completeness, its constructive collision kernel, its ROM extractability.
• CryptoFoundations/MerkleTree/Inductive/Batch/* — batch openings with completeness and uniqueness (feat(MerkleTree): add batch openings with completeness and uniqueness for inductive Merkle trees #473, merged 15 July). Batch openings are what an aggregated-signature verifier opens.

Phasing

1. Tweaked / node-addressed Merkle authentication paths. In review as feat(MerkleTree): add tweaked Merkle authentication paths with completeness and tweak-tagged collision binding #474: a node-addressed Merkle engine nodeHash : NodeAddress s → α → α → α of which the ordinary, level-separated and fully-addressed (XMSS-style) trees are instances, with completeness, a constructive collision kernel returning the collision tagged with the address at which it occurs, and an orientation theorem pinning the first collision endpoint to the honestly-precommitted child pair — the directional configuration a target-collision reduction consumes.
2. Winternitz / target-sum chains + incomparable encodings. The one-time signature layer, with chain-walk correctness and the encoding's incomparability property.
3. Generalized XMSS correctness. Key generation, signing, verification; honest signatures verify.
4. Unforgeability from SM-TCR. The reduction from EUF-CMA of the scheme to MultiTarget's target-collision game. This is the capstone, and I want to be honest that today it is a statement, not a proof — the address tag and orientation theorem from phase 1 exist specifically to make it reachable.
5. leanSig production instantiation. Poseidon2 / KoalaBear parameters plus a test-vector harness against the reference implementation.

Phases 2–5 are unstarted. Phase 1 is the only one with code in review.

What I am asking for

Chiefly a venue and shape decision before phase 2, so the follow-ups do not need re-homing the way this proposal did:

• Does the lane belong under CryptoFoundations/, or under a new Signatures/HashBased/ namespace? feat(MerkleTree): add tweaked Merkle authentication paths with completeness and tweak-tagged collision binding #474 currently sits at CryptoFoundations/MerkleTree/Addressed/, and I am happy to move it.
• For the SM-rTCR reduction specifically — does the probabilistic game packaging belong in-PR with the deterministic kernel, or as its own PR against HardnessAssumptions? This is the question I raised on feat(MerkleTree): add tweaked Merkle authentication paths with completeness and tweak-tagged collision binding #474 in July and it is still the gating decision for phase 2.
• Is there interest in this lane at all right now? If the answer is "not a priority", that is a perfectly good answer and I would rather hear it before writing phase 2 than after.

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