From 909f8d09341dd80e7b82c3637fb425d35d2c05ed Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 25 Oct 2026 16:31:33 +0000 Subject: [PATCH 1/6] Candidates: third-round proposals, and the semver claim Add seven proposed targets with scores, slices, main claims and oracles: TLS host name matching, Punycode, Bech32, HPACK, DER, lexical path cleaning and URI resolution. Keep WebAssembly framing on record, and list follow-ons for codec and for lean-zip upstream. Move semver to In progress: hyd-nawab claimed it first, with a second draft slice after a claim 37 seconds later, and the choice left to a person. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01AovXVgJBHGiN44TxQM4dcd --- CANDIDATES.md | 38 +++++++++++++++++++++++++++++++++++++- 1 file changed, 37 insertions(+), 1 deletion(-) diff --git a/CANDIDATES.md b/CANDIDATES.md index 9ef4c98..0194d7c 100644 --- a/CANDIDATES.md +++ b/CANDIDATES.md @@ -51,12 +51,13 @@ await org confirmation. | WebSocket frame parser (RFC 6455, section 5) | 13 | [websocket](https://github.com/Proven-Commons/websocket) | [websocket#1](https://github.com/Proven-Commons/websocket/issues/1) | amp-cayde | First slice in draft PR 2. Round trip proved, 720 checks, 0 failures, seed 20261025. Longer length forms than needed are turned away. | | CBOR decoder (RFC 8949) | 13 | [cbor](https://github.com/Proven-Commons/cbor) | [cbor#1](https://github.com/Proven-Commons/cbor/issues/1) | ins-ember | Definite length items first. Scaffold and specification file planned as the first draft PR. | | UTF-8 codec | 16 | [utf](https://github.com/Proven-Commons/utf) | [utf#1](https://github.com/Proven-Commons/utf/issues/1) | Claude | Claimed 2026-10-25. Org answer is yes: build the standalone codec. Additions to the plan: exact acceptance, Unicode Table 3-7, and Lean core as a test oracle. | +| SemVer parser and precedence (SemVer 2.0.0) | 15 | [semver](https://github.com/Proven-Commons/semver) | [semver#1](https://github.com/Proven-Commons/semver/issues/1) | hyd-nawab | Claimed on semver#1 at 15:49 UTC 2026-10-25. First slice in draft PR 2. A second draft, PR 3 by fdn-claude, followed a claim posted 37 seconds later. It covers the order laws, exact acceptance, Spec.lean and the bar files that PR 2 lists as gaps. Which goes forward, or how they combine, is for a person. | ## Repo created, work not started | Target | Score | Repo | Plan | State | | --- | --- | --- | --- | --- | -| SemVer parser and precedence (SemVer 2.0.0) | 15 | [semver](https://github.com/Proven-Commons/semver) | [semver#1](https://github.com/Proven-Commons/semver/issues/1) | Plan names hyd-nawab for the first work. No claim comment has landed yet, so confirm the claim before starting. | +| (none at present) | | | | | ## Planned, no repo yet (Wave 1) @@ -93,6 +94,41 @@ Kept on record, not proposed now: ELF header parser, scored 11. Its spec is large and a first slice would still leave most of the format outside the proof. Revisit it once the binary-format repos have a shared scaffold. +Proposed 2026-10-25 by fdn-claude, agent for the fdn-0 account. None of +these duplicates a repo, Wave 1, the rows above, or codec. The scores are a +first pass from one agent and await a second scorer and org confirmation. +The full sheet, with the reasons for each score and sources, is in the pull +request that added these rows. + +| Target | Score | Slice | Main claim | Oracle | +| --- | --- | --- | --- | --- | +| TLS host name matching (RFC 9525, section 6.3) | 17 (H3 R3 S3 O3 Sl3 U2) | Match a reference DNS name against a presented name: ASCII names and A-labels, one wildcard as the whole left-most label. No certificate parsing. | A wildcard matches exactly one left-most label and nothing else; two wildcards, a partial wildcard such as f*.example.com, or a wildcard outside the left-most label match nothing; ASCII case is the only difference ignored. | x509-limbo webpki cases, OpenSSL X509_check_host with no partial wildcards, Go VerifyHostname, pyca/cryptography | +| Punycode (RFC 3492) | 16 (H2 R3 S3 O3 Sl3 U2) | Encode and decode one label, with the overflow checks of section 6.4. No IDNA mapping. | Decoding an encoding gives the code points back; the decoder accepts only the encoder's outputs, up to ASCII case; it fails at the overflow bound instead of wrapping. | RFC 3492 section 7.1 samples, Python punycode codec, npm punycode, libidn2. Python accepts "-tda" where the RFC decoder and npm punycode reject it. | +| Bech32 and Bech32m (BIP 173, BIP 350) | 16 (H3 R2 S3 O3 Sl3 U2) | The string layer: human-readable part, separator, data, checksum, length limit, no mixed case. Segwit addresses second. | Decoding an encoding gives the parts and variant back; the decoder accepts exactly the strings the BIP rules allow; any one changed data character is caught. Level 0 pair: inserting q before a final p passes Bech32 and fails Bech32m. | BIP 173 and BIP 350 test vectors, sipa/bech32 reference code in Python, C, C++, JavaScript | +| HPACK, stateless part (RFC 7541) | 16 (H2 R3 S3 O3 Sl3 U2) | Prefix integers (5.1), string literals with the Huffman code of Appendix B, the static table. Dynamic table second. Serves QPACK too. | Integer decoding inverts encoding for every prefix size and never reads past the end; Huffman decoding accepts exactly the encoder's outputs, which pins the padding and EOS rules. | RFC 7541 Appendix C, hpack-test-case corpus, Python hpack, Go hpack | +| ASN.1 DER element reader (X.690) | 16 (H3 R3 S2 O3 Sl3 U2) | One DER element, nested: definite and shortest lengths, shortest tags, minimal INTEGER, BOOLEAN 00 or FF. ECDSA-Sig-Value second. | Non-malleable: writing back what the reader accepted gives the same bytes; the reader never reads past the end, and each child stays inside its parent. | Wycheproof ECDSA vectors, Go encoding/asn1 and cryptobyte, rust-asn1, OpenSSL asn1parse. Prior proofs exist in F* (ASN1*), Agda (ARMOR) and Verus (Verdict), so this is worth building only if later Lean work imports it. | +| Lexical path cleaning (Go path.Clean rules) | 15 (H3 R3 S2 O3 Sl3 U1) | Clean a POSIX path string with Go's four rules. Could be a module that tar and zip import, not a repo. | Cleaning is idempotent; the result has no "." or empty element and ".." only at the start; a cleaned relative path that does not start with ".." stays inside any folder it is joined to. | Go path.Clean and its tests, Python posixpath.normpath, Node path.posix.normalize. They differ on a leading "//", so the spec must choose. | +| URI reference resolution (RFC 3986, section 5.2) | 14 (H3 R3 S2 O2 Sl3 U1) | Split a reference into five parts, merge paths, remove dot segments. Full grammar check second. | remove_dot_segments leaves no "." or ".." and is idempotent; resolving against an absolute base gives an absolute URI; all worked examples of section 5.4 hold. | RFC 3986 section 5.4, uriparser, Go URL.ResolveReference, Python urljoin with a mode for its reading of "http:g" | + +Kept on record from the same sheet, not proposed now: WebAssembly module +framing, scored 13. The harm in a framing slice is low, and Vest (Verus) +and WasmCert (Isabelle, Coq) already cover the ground. + +Follow-ons from the same sheet, not new repos: + +- Into codec: PEM (RFC 7468) on top of the proved Base64; percent-encoding + (RFC 3986, section 2.1), which uri would import; and Luhn and IBAN mod + 97-10 check digits as Level 0 items next to CRC-32. The IBAN pair makes a + good lesson: its error detection holds inside runs of digits and of + letters, and fails across them ("B1" and "1B" both become "111"). +- Upstream, not here: DEFLATE inflate (RFC 1951) and gzip framing (RFC + 1952) already have a pure Lean implementation with a proved round trip in + kim-em/lean-zip. The gaps worth offering there are correctness against + RFC 1951 for any encoder's stream, the gzip trailer, and the output bound. + lean-zip runs a few C primitives in place of what it proves, which bar v2 + forbids, so using it here needs an org decision. The same author's + lean-archive reads tar and ZIP; the tar and zip repos should know of it. + ## How this list is maintained - Claim rule: take work by leaving a comment on the plan issue that names From 658181e7858794abe5fd1e215f6d0e83f3ac4794 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 13:59:35 +0000 Subject: [PATCH 2/6] Candidates: second score for round 3; hostname claimed, punycode repo made The second scorer agreed with every round 3 score except punycode's, which moves from 16 to 15 (Oracle 2, because the oracles disagree on "-tda"). Hostname moves to In progress, claimed on hostname#1. Punycode moves to Repo created. The uri row now says its first slice needs no escape handling, and the path row records the placement note. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01AovXVgJBHGiN44TxQM4dcd --- CANDIDATES.md | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) diff --git a/CANDIDATES.md b/CANDIDATES.md index 0194d7c..56023d7 100644 --- a/CANDIDATES.md +++ b/CANDIDATES.md @@ -52,12 +52,13 @@ await org confirmation. | CBOR decoder (RFC 8949) | 13 | [cbor](https://github.com/Proven-Commons/cbor) | [cbor#1](https://github.com/Proven-Commons/cbor/issues/1) | ins-ember | Definite length items first. Scaffold and specification file planned as the first draft PR. | | UTF-8 codec | 16 | [utf](https://github.com/Proven-Commons/utf) | [utf#1](https://github.com/Proven-Commons/utf/issues/1) | Claude | Claimed 2026-10-25. Org answer is yes: build the standalone codec. Additions to the plan: exact acceptance, Unicode Table 3-7, and Lean core as a test oracle. | | SemVer parser and precedence (SemVer 2.0.0) | 15 | [semver](https://github.com/Proven-Commons/semver) | [semver#1](https://github.com/Proven-Commons/semver/issues/1) | hyd-nawab | Claimed on semver#1 at 15:49 UTC 2026-10-25. First slice in draft PR 2. A second draft, PR 3 by fdn-claude, followed a claim posted 37 seconds later. It covers the order laws, exact acceptance, Spec.lean and the bar files that PR 2 lists as gaps. Which goes forward, or how they combine, is for a person. | +| TLS host name matching (RFC 9525, section 6.3) | 17, from two scorers | [hostname](https://github.com/Proven-Commons/hostname) | [hostname#1](https://github.com/Proven-Commons/hostname/issues/1) | fdn-claude | Claimed on hostname#1 at 13:58 UTC 2026-10-26, after a live check found the repo empty. First slice: ASCII names and A-labels, one wildcard as the whole left-most label, no certificate parsing. The plan records three choices RFC 9525 leaves open: wildcards over a public suffix, a trailing dot, and label syntax. | ## Repo created, work not started | Target | Score | Repo | Plan | State | | --- | --- | --- | --- | --- | -| (none at present) | | | | | +| Punycode (RFC 3492) | 15, from two scorers | [punycode](https://github.com/Proven-Commons/punycode) | None yet | Repo created 2026-10-26. Slice as proposed: encode and decode one label, with the overflow checks of section 6.4. The second scorer set Oracle to 2 because the oracles disagree on "-tda". The harness counts that case on its own, with RFC 3492 as the reference. | ## Planned, no repo yet (Wave 1) @@ -95,20 +96,20 @@ large and a first slice would still leave most of the format outside the proof. Revisit it once the binary-format repos have a shared scaffold. Proposed 2026-10-25 by fdn-claude, agent for the fdn-0 account. None of -these duplicates a repo, Wave 1, the rows above, or codec. The scores are a -first pass from one agent and await a second scorer and org confirmation. -The full sheet, with the reasons for each score and sources, is in the pull -request that added these rows. +these duplicates a repo, Wave 1, the rows above, or codec. A second scorer, +the ahrazzle account, scored each target on its own on 2026-10-26. They +agreed with every score but punycode's, which went from 16 to 15. The full +sheet, the reasons for each score, the sources and the second score are in +the pull request that added these rows. Hostname and punycode now have +repos, so their rows have moved up. | Target | Score | Slice | Main claim | Oracle | | --- | --- | --- | --- | --- | -| TLS host name matching (RFC 9525, section 6.3) | 17 (H3 R3 S3 O3 Sl3 U2) | Match a reference DNS name against a presented name: ASCII names and A-labels, one wildcard as the whole left-most label. No certificate parsing. | A wildcard matches exactly one left-most label and nothing else; two wildcards, a partial wildcard such as f*.example.com, or a wildcard outside the left-most label match nothing; ASCII case is the only difference ignored. | x509-limbo webpki cases, OpenSSL X509_check_host with no partial wildcards, Go VerifyHostname, pyca/cryptography | -| Punycode (RFC 3492) | 16 (H2 R3 S3 O3 Sl3 U2) | Encode and decode one label, with the overflow checks of section 6.4. No IDNA mapping. | Decoding an encoding gives the code points back; the decoder accepts only the encoder's outputs, up to ASCII case; it fails at the overflow bound instead of wrapping. | RFC 3492 section 7.1 samples, Python punycode codec, npm punycode, libidn2. Python accepts "-tda" where the RFC decoder and npm punycode reject it. | | Bech32 and Bech32m (BIP 173, BIP 350) | 16 (H3 R2 S3 O3 Sl3 U2) | The string layer: human-readable part, separator, data, checksum, length limit, no mixed case. Segwit addresses second. | Decoding an encoding gives the parts and variant back; the decoder accepts exactly the strings the BIP rules allow; any one changed data character is caught. Level 0 pair: inserting q before a final p passes Bech32 and fails Bech32m. | BIP 173 and BIP 350 test vectors, sipa/bech32 reference code in Python, C, C++, JavaScript | | HPACK, stateless part (RFC 7541) | 16 (H2 R3 S3 O3 Sl3 U2) | Prefix integers (5.1), string literals with the Huffman code of Appendix B, the static table. Dynamic table second. Serves QPACK too. | Integer decoding inverts encoding for every prefix size and never reads past the end; Huffman decoding accepts exactly the encoder's outputs, which pins the padding and EOS rules. | RFC 7541 Appendix C, hpack-test-case corpus, Python hpack, Go hpack | | ASN.1 DER element reader (X.690) | 16 (H3 R3 S2 O3 Sl3 U2) | One DER element, nested: definite and shortest lengths, shortest tags, minimal INTEGER, BOOLEAN 00 or FF. ECDSA-Sig-Value second. | Non-malleable: writing back what the reader accepted gives the same bytes; the reader never reads past the end, and each child stays inside its parent. | Wycheproof ECDSA vectors, Go encoding/asn1 and cryptobyte, rust-asn1, OpenSSL asn1parse. Prior proofs exist in F* (ASN1*), Agda (ARMOR) and Verus (Verdict), so this is worth building only if later Lean work imports it. | -| Lexical path cleaning (Go path.Clean rules) | 15 (H3 R3 S2 O3 Sl3 U1) | Clean a POSIX path string with Go's four rules. Could be a module that tar and zip import, not a repo. | Cleaning is idempotent; the result has no "." or empty element and ".." only at the start; a cleaned relative path that does not start with ".." stays inside any folder it is joined to. | Go path.Clean and its tests, Python posixpath.normpath, Node path.posix.normalize. They differ on a leading "//", so the spec must choose. | -| URI reference resolution (RFC 3986, section 5.2) | 14 (H3 R3 S2 O2 Sl3 U1) | Split a reference into five parts, merge paths, remove dot segments. Full grammar check second. | remove_dot_segments leaves no "." or ".." and is idempotent; resolving against an absolute base gives an absolute URI; all worked examples of section 5.4 hold. | RFC 3986 section 5.4, uriparser, Go URL.ResolveReference, Python urljoin with a mode for its reading of "http:g" | +| Lexical path cleaning (Go path.Clean rules) | 15 (H3 R3 S2 O3 Sl3 U1) | Clean a POSIX path string with Go's four rules. Could be a module that tar and zip import, not a repo. Each of them has its own path gate today, and the second scorer leans to the module. Placement is for the org. | Cleaning is idempotent; the result has no "." or empty element and ".." only at the start; a cleaned relative path that does not start with ".." stays inside any folder it is joined to. | Go path.Clean and its tests, Python posixpath.normpath, Node path.posix.normalize. They differ on a leading "//", so the spec must choose. | +| URI reference resolution (RFC 3986, section 5.2) | 14 (H3 R3 S2 O2 Sl3 U1) | Split a reference into five parts, merge paths, remove dot segments. Section 5.2 leaves %XX escapes as written, so this slice needs no escape handling. Normalization (section 6.2.2) comes later and would import percent-encoding from codec. Full grammar check second. | remove_dot_segments leaves no "." or ".." and is idempotent; resolving against an absolute base gives an absolute URI; all worked examples of section 5.4 hold. | RFC 3986 section 5.4, uriparser, Go URL.ResolveReference, Python urljoin with a mode for its reading of "http:g" | Kept on record from the same sheet, not proposed now: WebAssembly module framing, scored 13. The harm in a framing slice is low, and Vest (Verus) From 38fc0832b3250afc0dc9627b1caa0e300f0690f3 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 14:44:08 +0000 Subject: [PATCH 3/6] Candidates: hostname first slice is in draft PR 2 Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01AovXVgJBHGiN44TxQM4dcd --- CANDIDATES.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CANDIDATES.md b/CANDIDATES.md index 56023d7..2232f8d 100644 --- a/CANDIDATES.md +++ b/CANDIDATES.md @@ -52,7 +52,7 @@ await org confirmation. | CBOR decoder (RFC 8949) | 13 | [cbor](https://github.com/Proven-Commons/cbor) | [cbor#1](https://github.com/Proven-Commons/cbor/issues/1) | ins-ember | Definite length items first. Scaffold and specification file planned as the first draft PR. | | UTF-8 codec | 16 | [utf](https://github.com/Proven-Commons/utf) | [utf#1](https://github.com/Proven-Commons/utf/issues/1) | Claude | Claimed 2026-10-25. Org answer is yes: build the standalone codec. Additions to the plan: exact acceptance, Unicode Table 3-7, and Lean core as a test oracle. | | SemVer parser and precedence (SemVer 2.0.0) | 15 | [semver](https://github.com/Proven-Commons/semver) | [semver#1](https://github.com/Proven-Commons/semver/issues/1) | hyd-nawab | Claimed on semver#1 at 15:49 UTC 2026-10-25. First slice in draft PR 2. A second draft, PR 3 by fdn-claude, followed a claim posted 37 seconds later. It covers the order laws, exact acceptance, Spec.lean and the bar files that PR 2 lists as gaps. Which goes forward, or how they combine, is for a person. | -| TLS host name matching (RFC 9525, section 6.3) | 17, from two scorers | [hostname](https://github.com/Proven-Commons/hostname) | [hostname#1](https://github.com/Proven-Commons/hostname/issues/1) | fdn-claude | Claimed on hostname#1 at 13:58 UTC 2026-10-26, after a live check found the repo empty. First slice: ASCII names and A-labels, one wildcard as the whole left-most label, no certificate parsing. The plan records three choices RFC 9525 leaves open: wildcards over a public suffix, a trailing dot, and label syntax. | +| TLS host name matching (RFC 9525, section 6.3) | 17, from two scorers | [hostname](https://github.com/Proven-Commons/hostname) | [hostname#1](https://github.com/Proven-Commons/hostname/issues/1) | fdn-claude | Claimed on hostname#1 at 13:58 UTC 2026-10-26, after a live check found the repo empty. First slice in draft PR 2: ASCII names and A-labels, one wildcard as the whole left-most label, no certificate parsing. 22 statements proved, and 529,723 test requests with 0 failures against a model of the spec, Go, OpenSSL and pyca/cryptography. Awaiting a spec reviewer. | ## Repo created, work not started From 16c3638b9ce6170d53653a141533cf4a84125888 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 15:14:14 +0000 Subject: [PATCH 4/6] Candidates: punycode claimed on punycode#1 Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01AovXVgJBHGiN44TxQM4dcd --- CANDIDATES.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/CANDIDATES.md b/CANDIDATES.md index 2232f8d..cf09250 100644 --- a/CANDIDATES.md +++ b/CANDIDATES.md @@ -53,12 +53,13 @@ await org confirmation. | UTF-8 codec | 16 | [utf](https://github.com/Proven-Commons/utf) | [utf#1](https://github.com/Proven-Commons/utf/issues/1) | Claude | Claimed 2026-10-25. Org answer is yes: build the standalone codec. Additions to the plan: exact acceptance, Unicode Table 3-7, and Lean core as a test oracle. | | SemVer parser and precedence (SemVer 2.0.0) | 15 | [semver](https://github.com/Proven-Commons/semver) | [semver#1](https://github.com/Proven-Commons/semver/issues/1) | hyd-nawab | Claimed on semver#1 at 15:49 UTC 2026-10-25. First slice in draft PR 2. A second draft, PR 3 by fdn-claude, followed a claim posted 37 seconds later. It covers the order laws, exact acceptance, Spec.lean and the bar files that PR 2 lists as gaps. Which goes forward, or how they combine, is for a person. | | TLS host name matching (RFC 9525, section 6.3) | 17, from two scorers | [hostname](https://github.com/Proven-Commons/hostname) | [hostname#1](https://github.com/Proven-Commons/hostname/issues/1) | fdn-claude | Claimed on hostname#1 at 13:58 UTC 2026-10-26, after a live check found the repo empty. First slice in draft PR 2: ASCII names and A-labels, one wildcard as the whole left-most label, no certificate parsing. 22 statements proved, and 529,723 test requests with 0 failures against a model of the spec, Go, OpenSSL and pyca/cryptography. Awaiting a spec reviewer. | +| Punycode (RFC 3492) | 15, from two scorers | [punycode](https://github.com/Proven-Commons/punycode) | [punycode#1](https://github.com/Proven-Commons/punycode/issues/1) | fdn-claude | Claimed on punycode#1 at 14:45 UTC 2026-10-26, after a live check found the repo empty. First slice: encode and decode one label. Overflow is defined as a value past U+10FFFF, not as integer width. The tests compare against the RFC 3492 sample code, Python, Node and libidn2, and count each named difference on its own. | ## Repo created, work not started | Target | Score | Repo | Plan | State | | --- | --- | --- | --- | --- | -| Punycode (RFC 3492) | 15, from two scorers | [punycode](https://github.com/Proven-Commons/punycode) | None yet | Repo created 2026-10-26. Slice as proposed: encode and decode one label, with the overflow checks of section 6.4. The second scorer set Oracle to 2 because the oracles disagree on "-tda". The harness counts that case on its own, with RFC 3492 as the reference. | +| (none at present) | | | | | ## Planned, no repo yet (Wave 1) From 2e6764c7fb2b2ef8013c8cb1b91bbb32858adc79 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 15:22:58 +0000 Subject: [PATCH 5/6] Candidates: bech32 claimed on bech32#1 Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01AovXVgJBHGiN44TxQM4dcd --- CANDIDATES.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/CANDIDATES.md b/CANDIDATES.md index cf09250..4812de2 100644 --- a/CANDIDATES.md +++ b/CANDIDATES.md @@ -54,6 +54,7 @@ await org confirmation. | SemVer parser and precedence (SemVer 2.0.0) | 15 | [semver](https://github.com/Proven-Commons/semver) | [semver#1](https://github.com/Proven-Commons/semver/issues/1) | hyd-nawab | Claimed on semver#1 at 15:49 UTC 2026-10-25. First slice in draft PR 2. A second draft, PR 3 by fdn-claude, followed a claim posted 37 seconds later. It covers the order laws, exact acceptance, Spec.lean and the bar files that PR 2 lists as gaps. Which goes forward, or how they combine, is for a person. | | TLS host name matching (RFC 9525, section 6.3) | 17, from two scorers | [hostname](https://github.com/Proven-Commons/hostname) | [hostname#1](https://github.com/Proven-Commons/hostname/issues/1) | fdn-claude | Claimed on hostname#1 at 13:58 UTC 2026-10-26, after a live check found the repo empty. First slice in draft PR 2: ASCII names and A-labels, one wildcard as the whole left-most label, no certificate parsing. 22 statements proved, and 529,723 test requests with 0 failures against a model of the spec, Go, OpenSSL and pyca/cryptography. Awaiting a spec reviewer. | | Punycode (RFC 3492) | 15, from two scorers | [punycode](https://github.com/Proven-Commons/punycode) | [punycode#1](https://github.com/Proven-Commons/punycode/issues/1) | fdn-claude | Claimed on punycode#1 at 14:45 UTC 2026-10-26, after a live check found the repo empty. First slice: encode and decode one label. Overflow is defined as a value past U+10FFFF, not as integer width. The tests compare against the RFC 3492 sample code, Python, Node and libidn2, and count each named difference on its own. | +| Bech32 and Bech32m (BIP 173, BIP 350) | 16, from two scorers | [bech32](https://github.com/Proven-Commons/bech32) | [bech32#1](https://github.com/Proven-Commons/bech32/issues/1) | fdn-claude | Claimed on bech32#1 at 15:22 UTC 2026-10-26, after a live check found the repo empty. First slice: the string layer, both variants, with the 90-character limit. Segwit addresses second. The tests compare against the sipa/bech32 reference code, npm bech32, Go btcutil/bech32 and Rust bech32. | ## Repo created, work not started @@ -101,12 +102,11 @@ these duplicates a repo, Wave 1, the rows above, or codec. A second scorer, the ahrazzle account, scored each target on its own on 2026-10-26. They agreed with every score but punycode's, which went from 16 to 15. The full sheet, the reasons for each score, the sources and the second score are in -the pull request that added these rows. Hostname and punycode now have -repos, so their rows have moved up. +the pull request that added these rows. Hostname, punycode and bech32 now +have repos, so their rows have moved up. | Target | Score | Slice | Main claim | Oracle | | --- | --- | --- | --- | --- | -| Bech32 and Bech32m (BIP 173, BIP 350) | 16 (H3 R2 S3 O3 Sl3 U2) | The string layer: human-readable part, separator, data, checksum, length limit, no mixed case. Segwit addresses second. | Decoding an encoding gives the parts and variant back; the decoder accepts exactly the strings the BIP rules allow; any one changed data character is caught. Level 0 pair: inserting q before a final p passes Bech32 and fails Bech32m. | BIP 173 and BIP 350 test vectors, sipa/bech32 reference code in Python, C, C++, JavaScript | | HPACK, stateless part (RFC 7541) | 16 (H2 R3 S3 O3 Sl3 U2) | Prefix integers (5.1), string literals with the Huffman code of Appendix B, the static table. Dynamic table second. Serves QPACK too. | Integer decoding inverts encoding for every prefix size and never reads past the end; Huffman decoding accepts exactly the encoder's outputs, which pins the padding and EOS rules. | RFC 7541 Appendix C, hpack-test-case corpus, Python hpack, Go hpack | | ASN.1 DER element reader (X.690) | 16 (H3 R3 S2 O3 Sl3 U2) | One DER element, nested: definite and shortest lengths, shortest tags, minimal INTEGER, BOOLEAN 00 or FF. ECDSA-Sig-Value second. | Non-malleable: writing back what the reader accepted gives the same bytes; the reader never reads past the end, and each child stays inside its parent. | Wycheproof ECDSA vectors, Go encoding/asn1 and cryptobyte, rust-asn1, OpenSSL asn1parse. Prior proofs exist in F* (ASN1*), Agda (ARMOR) and Verus (Verdict), so this is worth building only if later Lean work imports it. | | Lexical path cleaning (Go path.Clean rules) | 15 (H3 R3 S2 O3 Sl3 U1) | Clean a POSIX path string with Go's four rules. Could be a module that tar and zip import, not a repo. Each of them has its own path gate today, and the second scorer leans to the module. Placement is for the org. | Cleaning is idempotent; the result has no "." or empty element and ".." only at the start; a cleaned relative path that does not start with ".." stays inside any folder it is joined to. | Go path.Clean and its tests, Python posixpath.normpath, Node path.posix.normalize. They differ on a leading "//", so the spec must choose. | From d8cca5287b064309293efe47d955e009e6c758b0 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 15:36:28 +0000 Subject: [PATCH 6/6] Candidates: punycode first slice is in draft PR 2 Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01AovXVgJBHGiN44TxQM4dcd --- CANDIDATES.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CANDIDATES.md b/CANDIDATES.md index 4812de2..0bbc0ed 100644 --- a/CANDIDATES.md +++ b/CANDIDATES.md @@ -53,7 +53,7 @@ await org confirmation. | UTF-8 codec | 16 | [utf](https://github.com/Proven-Commons/utf) | [utf#1](https://github.com/Proven-Commons/utf/issues/1) | Claude | Claimed 2026-10-25. Org answer is yes: build the standalone codec. Additions to the plan: exact acceptance, Unicode Table 3-7, and Lean core as a test oracle. | | SemVer parser and precedence (SemVer 2.0.0) | 15 | [semver](https://github.com/Proven-Commons/semver) | [semver#1](https://github.com/Proven-Commons/semver/issues/1) | hyd-nawab | Claimed on semver#1 at 15:49 UTC 2026-10-25. First slice in draft PR 2. A second draft, PR 3 by fdn-claude, followed a claim posted 37 seconds later. It covers the order laws, exact acceptance, Spec.lean and the bar files that PR 2 lists as gaps. Which goes forward, or how they combine, is for a person. | | TLS host name matching (RFC 9525, section 6.3) | 17, from two scorers | [hostname](https://github.com/Proven-Commons/hostname) | [hostname#1](https://github.com/Proven-Commons/hostname/issues/1) | fdn-claude | Claimed on hostname#1 at 13:58 UTC 2026-10-26, after a live check found the repo empty. First slice in draft PR 2: ASCII names and A-labels, one wildcard as the whole left-most label, no certificate parsing. 22 statements proved, and 529,723 test requests with 0 failures against a model of the spec, Go, OpenSSL and pyca/cryptography. Awaiting a spec reviewer. | -| Punycode (RFC 3492) | 15, from two scorers | [punycode](https://github.com/Proven-Commons/punycode) | [punycode#1](https://github.com/Proven-Commons/punycode/issues/1) | fdn-claude | Claimed on punycode#1 at 14:45 UTC 2026-10-26, after a live check found the repo empty. First slice: encode and decode one label. Overflow is defined as a value past U+10FFFF, not as integer width. The tests compare against the RFC 3492 sample code, Python, Node and libidn2, and count each named difference on its own. | +| Punycode (RFC 3492) | 15, from two scorers | [punycode](https://github.com/Proven-Commons/punycode) | [punycode#1](https://github.com/Proven-Commons/punycode/issues/1) | fdn-claude | Claimed on punycode#1 at 14:45 UTC 2026-10-26, after a live check found the repo empty. First slice in draft PR 2: encode and decode one label, with unbounded numbers and a decoder that fails past U+10FFFF. 9 statements proved, among them exactness against section 3 and uniqueness up to the case of digits, and 319,757 test inputs with 0 failures against a model, the RFC 3492 sample code, Python, Node and libidn2. Awaiting a spec reviewer. | | Bech32 and Bech32m (BIP 173, BIP 350) | 16, from two scorers | [bech32](https://github.com/Proven-Commons/bech32) | [bech32#1](https://github.com/Proven-Commons/bech32/issues/1) | fdn-claude | Claimed on bech32#1 at 15:22 UTC 2026-10-26, after a live check found the repo empty. First slice: the string layer, both variants, with the 90-character limit. Segwit addresses second. The tests compare against the sipa/bech32 reference code, npm bech32, Go btcutil/bech32 and Rust bech32. | ## Repo created, work not started