docs(sofi): the verification substrate, and the signature algorithm a foreign verifier cannot derive from the registry

[cryptskii]

Amendment 2c-C2 — the verification substrate. Second of the four sub-amendments the 2c-C decomposition fixed. Normative, encoder-free, documentation only.

The spine

The owner fixed C2's boundary as a three-way distinction that must not be blurred:

(1) canonical identity        what exact bytes / digest NAME a thing
(2) authenticated retrieval   how a verifier OBTAINS it and PROVES it is the one named
(3) verification semantics    what predicate applies once it HAS it

C2 owns (1) and (2) plus the reusable algorithms (3) consumes. ValidDlvSuccessor is not decided here — that is C3. Layers (1) and (2) have exactly one correct answer two implementations must agree on byte for byte, and no policy content. Layer (3) is where policy lives.

The finding that reframed the amendment

dsm/src/crypto/sphincs.rs uses BLAKE3 for all hash/PRF/thash operations instead of SHA2/SHAKE, and says in its own header that it "has NOT been formally audited." Structure and parameters match the standardized sets — so pk = 64 and sig = 49,856 are exactly FIPS-205 SLH-DSA-256f's sizes.

Registry §3.1 declares the member by name and those two sizes and nothing else. So a foreign verifier implemented from §3.1 links a standards-conformant SLH-DSA library, gets byte-identical key and signature lengths, and every DSM signature fails with no size mismatch to diagnose it. §3.1's own closing sentence — "the algorithm and the key bytes stand or fall together" — is false as written: matching widths do not identify an algorithm, and these particular widths coincide exactly with a different, incompatible one.

This is the single most likely point at which foreign verification actually fails, and it was missing from every research dimension until the completeness critic surfaced it.

Seven rulings

	Ruling
A	The authority-resolver contract is frozen; the seven predicates are not C2's
B	The root-register profile is a normative per-network parameter, published with literal values
C	Traversal limits are local resource policy, never validity
D	Two classes of vector, and only one is evidence
E	The signature primitive is part of the frozen substrate
F	The binding record is a frozen storage-wire grammar, not a protobuf exception
G	The formal debt is enumerated, not deferred vaguely

A. Rev 15 contains zero occurrences of P0 — verified against the 2,652-line spec after confirming the file was present and non-empty, since a silently-failed search is how this programme published a false claim once already. The numbering is code-local, describes general owner authority, and the economic layer adds no predicates of its own. C2 freezes the inputs, the normative stage order, the descent-never-frontier limit (which bounds what C4 may conclude), and the two facts returned. SoFi consumes authenticated identity authority; it does not redefine it.

E. C2 freezes the actual construction under a DSM BLAKE3-SPHINCS+-SPX256F designation, keeping id 0x0001 as a correction rather than burning a number. Signing determinism is deliberately not made normative — the shipped signer is deterministic and the write-once register currently depends on it, but that is a retry/object-identity defect fixed at that layer:

Once an exact signed candidate is prepared, its exact signature bytes and canonical object bytes are frozen and MUST be reused for retries, recovery and re-publication. A retry MUST NOT regenerate a signature and assume byte equality.

Requiring determinism would permanently exclude a hedged signer to paper over a retry rule.

D. A conformance vector is independent only if its expected bytes are produced without invoking the production encoder, decoder, canonicalization helper or digest helper whose behaviour it tests — otherwise it proves implementation == itself. ccb_conformance.rs already does this correctly for 0x0001–0x000A; C2 obligates extending it to 0x001B–0x0030 and the economic SMT. The executed vectors in this amendment are explicitly labelled the second class.

The substrate, pinned byte-exact

Read from source directly rather than from a research summary, because a backwards reading breaks every proof:

• get_bit(k,i) = (k[i/8] >> (7 - i%8)) & 1 — bit 0 is the MSB of byte 0
• bit 0 selects at the ROOT, bit 255 at the deepest level
• the sibling array is leaf-to-root; siblings[0] is deepest
• bit value 0 ⇒ left child
• the value at a leaf is H_dom(DSM/economic-leaf-state/v1, CCB(S)) — not the CCB itself, a step easy to miss that changes every root

All four leaf keys bind G ‖ DevID first, making the key space per-identity by construction. K_root identity-scopes a cell and is derivable by anyone who knows (G, DevID, position) — exclusivity comes from write-once storage plus attribution, never from the key.

Vectors were executed with three anti-transposition controls — reversed siblings, reversed key bytes, swapped econ_node arguments — each of which must and does differ from the true root. A single expected root can be reproduced by an implementation that is wrong twice.

Corrections to what shipped

• Req 15.3 is discharged for one of the walker's four fetches, not none and not all. The manifest is re-hashed; authority evidence, witness and successor evidence are not, and neither verify function recovers it internally. The module comment at peer_lineage.rs:61-62 asserts the opposite — worse than a silent gap, because it certifies an absent check.
• validate_peer_lineage has no test anywhere in the workspace. None of its conjuncts is proven load-bearing.
• RootRegisterProfile.quorum has no non-test reader. The economic register counts at a strict majority of the locally resolved member list — the same failure Req 6.10 forbids for Class K, in the one register with no vault state to read q from. This corrected the amendment's own draft, which had described the pinned threshold as operative.
• observe_cell does not defend its stated precondition and manufactures EmptyAtQuorum at q = 0, reachable because quorum_for(0) == 0.
• winning_faucet_ticket drops RegisterError::Conflict via .ok().flatten(), delivering a quarantined write-once cell as emptiness — the exact collapse the four-valued observation exists to prevent, reintroduced at the call site.
• The economic register read endpoints never emit x-dsm-register-incarnation, which the shipped client reader requires; the header is stamped only on the settlement-slot path.

Process

Research ran read-only under the rule adopted after the 2c-C1 contamination, and the tree was proved clean by git diff --exit-code before, during and after the fan-out. Every finding that reached a ruling was re-verified at source — and one of those checks corrected this amendment's own draft.

Verification, scope proof, and the enumerated implementation debts are in the amendment's own final sections.

Next: 2c-C3 (ValidDlvSuccessor), then 2c-C4 (the TA_B closure walk).