From 7a867d7a5cec2d28cf47b9df9b91ef61f3fbe475 Mon Sep 17 00:00:00 2001 From: ahrazzle <38987266+ahrazzle@users.noreply.github.com> Date: Sun, 25 Oct 2026 10:45:53 -0500 Subject: [PATCH 1/8] Add candidate list reference to README Added a candidate list section to the README. --- README.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/README.md b/README.md index 4ad21e0..5fdfac0 100644 --- a/README.md +++ b/README.md @@ -23,6 +23,8 @@ Pilot (complete): the tar extractor lives in its own repo, [tar](https://github. Wave 1: a policy engine in the style of AWS Cedar, a reader for the SQLite file format, and a parser for the Redis protocol with a small key-value store. +Candidate list: [CANDIDATES.md](CANDIDATES.md) holds every target, its score, its repo and plan, who claimed it, and its state. It is updated as targets ship and new candidates are proposed. + Each project sends reusable lemmas to CSLib and Mathlib, the shared libraries for computer science and mathematics in Lean. The shared library grows. The next project starts cheaper. ## Learn here From cf9591a148cf35112b9c44756f68212184042f6c Mon Sep 17 00:00:00 2001 From: ahrazzle <38987266+ahrazzle@users.noreply.github.com> Date: Sun, 25 Oct 2026 10:46:29 -0500 Subject: [PATCH 2/8] Add CANDIDATES.md --- CANDIDATES.md | 110 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 110 insertions(+) create mode 100644 CANDIDATES.md diff --git a/CANDIDATES.md b/CANDIDATES.md new file mode 100644 index 0000000..9ef4c98 --- /dev/null +++ b/CANDIDATES.md @@ -0,0 +1,110 @@ +# Candidate list + +This file is the permanent record of targets for Proven Commons. It holds +every target in one place: what it is, how it scored, where its repo and +plan live, who is working on it, and what state it is in. + +The list changes as work moves. A target moves through these states: +proposed, repo created, claimed, in progress, shipped, maintained. When a +target ships, move its row to Shipped and keep its links. Do not delete +shipped rows. When a new candidate is identified, add it to Proposed with +its score, slice, claim, and oracle, before any repo is created. + +This file integrates the earlier list in mission issue 12 in full. All +eight targets from that issue appear below, with their scores and slices, +plus the Base32 note folded into the codec row. Issue 12 stays as history. +This file is the living list from here on. Do not maintain a second living +list in issue comments. Update this file when a status changes. + +## Scoring + +Score each candidate 0 to 3 on each point, total out of 18, as the founding +brief sets out. + +- Harm if it fails: money moved, access granted, data exposed, safety affected. +- Reach: how much other software depends on it. +- Specification size: a short public specification scores high. A large or + disputed one scores low. +- Oracle: an original implementation and test suite exist to compare against. +- Slice: a useful part can be cut out and proved on its own. +- Upstream stance: the maintainers will read a submission and give feedback. + +Scores for the mission issue 12 targets come from that issue. Scores for +the new candidates in Proposed come from the proposal dated 2026-10-25 and +await org confirmation. + +## Shipped + +| Target | Score | Repo | State | +| --- | --- | --- | --- | +| Tar extractor (ustar) | Pilot, not scored in issue 12 | [tar](https://github.com/Proven-Commons/tar) | Pilot complete. Proved rule: no file in an archive can be written outside the destination folder. Bar audit still open in mission issue 1, so do not call it verified until that audit closes. | + +## In progress + +| Target | Score | Repo | Plan | Claimed by | State | +| --- | --- | --- | --- | --- | --- | +| Codec: hex, Base64, CRC-32 | Academy material, not scored in issue 12 | [codec](https://github.com/Proven-Commons/codec) | [codec#1](https://github.com/Proven-Commons/codec/issues/1) | Claude (import), hyd-nawab (Base32) | Import in codec PR 1. Base32 in codec PR 2, stacked on PR 1. Base32 does not get its own repo. | +| ZIP archive reader | 15 | [zip](https://github.com/Proven-Commons/zip) | [zip#1](https://github.com/Proven-Commons/zip/issues/1) | hyd-nawab | Stored entries only, with a proved path gate. Draft PR 2 states 3,058 checks, 0 failures, seed 20261025. | +| JSON parser and printer (RFC 8259) | 16 | [json](https://github.com/Proven-Commons/json) | [json#1](https://github.com/Proven-Commons/json/issues/1) | hyd-nawab | First slice in progress. Round trip is the main claim. | +| RFC 3339 timestamp parser | 16 | [rfc](https://github.com/Proven-Commons/rfc) | [rfc#1](https://github.com/Proven-Commons/rfc/issues/1) | Claude | First slice in PR 2, ready for review. CI green, awaiting a spec reviewer. | +| Protobuf wire format codec | 15 | [protobuf](https://github.com/Proven-Commons/protobuf) | [protobuf#1](https://github.com/Proven-Commons/protobuf/issues/1) | Claude | First slice in PR 2, ready for review, after the RFC 3339 slice is up for review. Wire layer only. | +| 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. | + +## 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. | + +## Planned, no repo yet (Wave 1) + +From the founding brief, months 4 to 9, one squad each. No scores published +for these three yet. + +- Policy engine in the style of AWS Cedar. Claims: a satisfied forbid gives + a deny, no satisfied permit gives a deny, and policy order does not change + the decision. +- SQLite file reader. Slice: 100-byte header, page header, and records. + Claims: the parser returns an error instead of reading outside the file, + and a record it reads stays inside its page. +- Redis protocol parser and small key-value store. Claims: reading what the + printer wrote gives the same command back, a get after a set returns the + set value, and a get after a delete returns nothing. + +## Proposed, no repo yet + +Proposed 2026-10-25 by amp-sai, agent for Ahraz Arifuddin. None of these +duplicates Wave 1, mission issue 12, tar, or codec. Org owners create a repo +only after confirming the score and slice. + +| Target | Score | Slice | Main claim | Oracle | +| --- | --- | --- | --- | --- | +| TOML 1.0 parser | 16 | Parse a TOML document into tables, arrays, strings, integers, floats, booleans, and datetimes. No printer in the first slice. | Parsing a document and reading a key back gives the value the document states, and a document outside the grammar is rejected. | Python tomllib, Rust toml crate, TOML test suite | +| IP address and CIDR parser | 16 | Parse IPv4 and IPv6 addresses and CIDR prefixes. No DNS lookup. | An address is inside a prefix exactly when its masked bits match the prefix bits. An address with an extra part, or a prefix length past the address size, is rejected. | Python ipaddress, Rust std IpAddr, RFC 4291 and RFC 4632 examples | +| HTTP/1.1 header parser | 15 | Parse a request line and headers only. No body, no chunked transfer, no server. | A header block is accepted exactly when it matches RFC 9112 framing rules. Duplicate Content-Length, a bare carriage return, and an obsolete folded line are rejected. | Python http.client in strict mode, httpbis test cases | +| MessagePack decoder | 15 | Decode MessagePack items with definite lengths: integers, strings, binary, arrays, and maps. No extension types in the first slice. | Decoding an encoding returns the same item, and the decoder returns an error instead of reading past the end of its input. | Python msgpack, official MessagePack test vectors | +| UUID parser | 15 | Parse the canonical text form in RFC 9562 and print it back. No generation in the first slice. | Print then parse returns the same UUID. A string with the wrong version or variant field, or a misplaced hyphen, is rejected. | Python uuid, Rust uuid, RFC 9562 examples | +| DNS wire message parser | 14 | Parse a DNS message header, questions, and records from RFC 1035 bytes, with compression pointers limited to earlier offsets in the same message. | The decoder never reads past the end of the message. A pointer loop, or a pointer forward in the message, is rejected. | Python dnspython, dig output for the same messages | +| Bencode parser | 13 | Parse integers, byte strings, lists, and dictionaries, with dictionary keys in sorted order. | Decoding an encoding returns the same value, and a dictionary with unsorted keys is rejected. | Python bencode libraries, torrent files in the wild | + +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. + +## How this list is maintained + +- Claim rule: take work by leaving a comment on the plan issue that names + who is working on it, before starting. Update this file in the same change + where the claim, repo creation, draft PR, merge, or shipped state lands, + or in a follow-up PR that states the change. +- One row per target. A target that ships moves to Shipped with its repo and + project page links. A target that is split keeps its original row and adds + a row for the new part, with a note on the split. +- A new candidate joins Proposed only with all six scores, a slice, a main + claim, and an oracle. A candidate with no repo is not work to claim yet. +- Check this file against the plan issues before reusing a status in a + report. Plan issues and draft PRs change faster than this list. +- Mission issue 12 is history, not a second list. Its eight targets are + fully integrated above. Future status changes go here, not there. From 909f8d09341dd80e7b82c3637fb425d35d2c05ed Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 25 Oct 2026 16:31:33 +0000 Subject: [PATCH 3/8] 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 4/8] 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 5/8] 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 6/8] 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 7/8] 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 8/8] 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