diff --git a/CANDIDATES.md b/CANDIDATES.md index 9ef4c98..0bbc0ed 100644 --- a/CANDIDATES.md +++ b/CANDIDATES.md @@ -51,12 +51,16 @@ 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. | +| 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 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 | 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 +97,40 @@ 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. 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, punycode and bech32 now +have repos, so their rows have moved up. + +| Target | Score | Slice | Main claim | Oracle | +| --- | --- | --- | --- | --- | +| 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. | +| 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) +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