Document BIP93 reference-helper edge cases

Problem

The inline BIP93 helpers can return misleading results when their input preconditions are missed, including recovery of an unintended payload that still passes checksum and header validation. The prose already states the recovery conditions and fresh-target requirement, but the helpers do not enforce them.

Our checked Lean API already handles these cases. This issue tracks reproducible reference-code examples, documentation improvements, and precise links to the existing tests and proofs.

Reference: vendored BIP93 revision 55083d36.

Findings and proposed changes

Points 5 and 6 are already documented upstream; point 9 is covered by an open PR. They are crossed out below. Local reproducer tasks remain in the acceptance criteria.

1. Make recovery-set validation explicit

ms32_interpolate / ms32_recover do not check matching thresholds, identifiers or lengths, distinct indices, or exact share count. With equal-length inputs, distinct indices and a fresh target, the weights sum to one and preserve checksum validity even when identifiers differ. A common valid threshold also survives, so the result can pass decoding.

Document that callers MUST validate the individual inputs and all stated set conditions before using the helpers. Include invalid recovery-set vectors for mismatched identifiers and duplicate indices. Identifier agreement is a consistency check; reused or colliding identifiers cannot establish common provenance.

Verified example: these two synthetic strings individually pass ms32_decode, but have different identifiers:

ms12aaaaaqqqqqqqqqqqqqqqqqqqqqqqqqqewgrmvtjj33fe
ms12cccccppppppppppppppppppppppppppk2f7m4eeqgz7u

Passing their complete data parts, including checksums, to the inline ms32_recover returns:

ms12sssssnnnnnnnnnnnnnnnnnnnnnnnnnnwsmcmf8m75wg5

That result passes both checksum verification and ms32_decode, despite the invalid recovery set. Our checked recovery API should reject the inputs with mismatchedIdentifier.

Duplicate indices require a separate explanation: the inline expression compares index values in i == j, so duplicate values do not create zero denominators at a fresh target. For example, bech32_lagrange([29, 29], 16) returns [1, 1]; two identical input strings then cancel to zero. Duplicates violate the interpolation preconditions and must be rejected.

2. Explain existing-index interpolation

bech32_lagrange([29, 24], 29) returns [0, 0]. At an existing target, the numerator vanishes and the inverse table maps zero to zero, so interpolation returns an all-zero data part. A conforming decoder rejects its header.

Put the existing fresh-target restriction beside the helper. Alternatively, use the standard Lagrange product excluding the current point, which agrees at fresh targets and correctly evaluates existing targets when input indices are pairwise distinct.

Our Field.lagrange uses the standard product; Shares.interpolate returns the validated existing message, while Shares.derive enforces a fresh target.

3. Check the checksum constructor's upper bound

Merged bitcoin/bips#2258 fixes the checksum selection bounds and verifier limit. The constructor guard below remains open.

The inline ms32_create_checksum returns a 15-symbol checksum for both 1,003 and 1,004 input symbols. Its verifier accepts the first completed codeword and rejects the second.

Proposed guard:

if MS32_HRP_EXPANDED_LENGTH + len(data) + 15 > 1023:
    raise ValueError("expanded codeword exceeds 1023 symbols")

The limit counts the five HRP expansion values, the data, and the checksum. At most 1,003 symbols may precede the checksum, including the six header symbols; the maximum payload is 997 symbols. Our checked Checksum.create already enforces this bound.

4. Explain why header interpolation works

Constant threshold and identifier columns are preserved because the weights sum to one. The index column represents f(x) = x, so reproducing the target requires at least two distinct input points. Sharing already requires a threshold of at least two. Add this explanation alongside the header-inheritance rationale.

5. Distinguish variant-only checksum verification from format validation

Addressed upstream: merged bitcoin/bips#2258 already documents variant-only verification versus automatic variant selection. The local reproducer remains to be added.

ms32_verify_long_checksum checks the long polymod residue and upper bound, but does not enforce the lower bound for selecting the long variant. Callers must use ms32_verify_checksum to select the variant required by the complete expanded length.

Concrete example: take the 32-symbol body consisting of 0qqqqs followed by 26 q symbols and append a long checksum. This gives 47 data symbols, 52 expanded values, and 50 printed characters. The long-only verifier accepts it, while the automatic selector rejects it.

Local follow-up: add this example to the pinned-snippet reproducer:

body = [CHARSET.index(c) for c in "0qqqqs" + "q" * 26]
data = body + ms32_create_long_checksum(body)
assert len(data) == 47
assert ms32_verify_long_checksum(data)
assert not ms32_verify_checksum(data)

The equivalent Lean calls were checked: Checksum.verifyLong returns true and Checksum.verify returns false. This is a low-level helper contract, not a newly found implementation defect.

6. Distinguish generic codex32 from master-seed decoding

Addressed upstream: merged bitcoin/bips#2258 explicitly identifies ms32_decode as a master-seed parser. Open bitcoin/bips#2285 further separates the format and application sections and removes the inline encode/decode helpers.

The reference ms32_decode is an application parser: it accepts only the six printed master-seed lengths in MS32_VALID_LENGTHS. Generic codex32 permits other payload lengths. Accordingly, ms32_encode and ms32_decode are not unrestricted generic-format inverses.

For example, a valid regular string with a 69-symbol payload has 91 printed characters and 93 expanded values. Our Encoding.parse accepts it; Seed.parse and the reference ms32_decode reject its application size intentionally.

Local follow-up: add a generic-size example to the reproducer. The two API levels are already documented, and existing Lean generic-length regression coverage exercises the distinction.

7. Make random-share entropy and padding requirements explicit

Still open: the bytes-to-shares warning was discussed but explicitly deferred from bitcoin/bips#2285.

Random initial payloads must consist of independent, uniform GF(32) symbols across all shares and columns, including padding. Uniform random bytes followed by zero padding do not meet this requirement: encoding 16 bytes produces 26 symbols, with the final symbol's low two bits fixed.

Distinguish this from a supplied existing secret, whose padding may be zero or any other permitted value. Add a usage example showing full-symbol sampling and link the secrecy theorems' exact entropy assumptions. This clarifies the BIP's instruction to choose payload characters uniformly at random; it does not identify a new mandatory feature missing from the Lean library.

8. Record the complete-codeword reference-equivalence proof boundary

The BIP's ms32_interpolate interpolates every input data position, including the checksum when complete codewords are supplied. Our checked API evaluates payload columns, constructs the header, and regenerates the checksum during serialization.

The official vectors establish tested interoperability. A general Lean theorem equating these full results remains unproved. Record this separately from the existing caveat about directly proving the optimized BIP weights equal the standard Lagrange product at pairwise-distinct source indices and a fresh target.

A follow-up theorem should compare the complete serialized data parts for admissible common-metadata, equal-length, checksum-valid sources and fresh targets, for both checksum variants. Neither missing equivalence theorem is evidence that the existing recovery or secrecy results are incorrect: those results concern the actual Lean implementation.

9. Note the apparent probability-expression typo

Covered by an existing open PR: bitcoin/bips#2285 removes the sentence containing 1 - 2^65; the earlier probability statement is retained. No separate upstream proposal is needed. The vendored snapshot stays unchanged.

This does not prove a failure probability. Formalizing the larger-random-error probability claims and the 13/15 consecutive-erasure guarantees remains separate proof work.

Completed proof coverage

The following are now proved and are not outstanding gaps:

• Admissible initialization produces a validated source and connects through arbitrary distinct threshold-sized non-secret recovery selections: initializeFresh_valid, initializeExisting_valid, and recovery theorems.
• Generic and master-seed parser soundness/completeness against a declarative specification, including uppercase: parse_iff_spec, seed_parse_iff_spec, and uppercase results.
• Perfect secrecy under independently uniform full-symbol input entropy for fixed fewer-than-threshold non-secret observations: existing-secret distribution equality and fresh-secret joint-count symmetry. Public metadata and payload length are held fixed; external entropy quality is not proved.

These proofs were added in 8d27167. The four-substitution/eight-erasure uniqueness proofs are also complete; they do not implement a correction algorithm.

Acceptance criteria

• Add a reproducible example against the pinned, unmodified BIP Python snippets covering mixed identifiers, duplicate indices, existing targets, and the 1,003/1,004-symbol boundary.
• Include the concrete invalid recovery sets as fixtures and verify the checked Lean API returns the appropriate errors, reusing existing coverage where possible.
• Expand the implementation documentation with the caller-validation warning, corrected duplicate-index explanation, proposed constructor guard, and constant/linear header argument.
• Link the completed initialization, parser, and secrecy proofs, retaining their assumptions and distinguishing them from missing reference-equivalence theorems.
• Document variant selection, generic versus master-seed parsing, and full-symbol random-share padding requirements.
• Extend the pinned-snippet reproducer with the short long-checksum example and a valid generic payload rejected by the master-seed decoder.
• Add a full-symbol sampling usage example contrasting random-share padding with existing-secret padding.
• Prove the optimized BIP weights agree with the standard product for distinct source indices and a fresh target, then prove complete-codeword interpolation agrees with payload interpolation followed by checksum generation for both variants.
• Propose the probability-expression typo correction upstream. Covered by open bitcoin/bips#2285; retain the unmodified pinned snapshot.

Existing coverage: share validation and checked APIs, regression tests, checksum proofs, and documented specification boundaries.

Verification of the original findings: the mixed-identifier example, existing-target weights, duplicate weights/cancellation, and checksum boundary behavior above were reproduced by executing the exact Python blocks extracted from the vendored specification.

Verification of the added findings: the short long-checksum and 69-symbol generic-payload examples were evaluated with the Lean implementation. Their permanent reproductions against the pinned Python snippets remain open above. Independent review checked the entropy assumptions and the remaining theorem boundaries against the source and current proofs.