From bd20511e2ec9ae97ae8af533ba1ba4ad5f15b41a Mon Sep 17 00:00:00 2001 From: ahrazzle <38987266+ahrazzle@users.noreply.github.com> Date: Wed, 28 Oct 2026 03:05:33 -0500 Subject: [PATCH] Update org profile README for the new repos --- profile/README.md | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/profile/README.md b/profile/README.md index e9d35e0..fc6944b 100644 --- a/profile/README.md +++ b/profile/README.md @@ -34,13 +34,15 @@ One repo per library, named for the software it verifies. Each carries its own p | Area | Repos | | --- | --- | -| Encodings | [codec](https://github.com/Proven-Commons/codec) (base64, hex, CRC-32), [utf](https://github.com/Proven-Commons/utf) (UTF-8) | -| Data formats | [json](https://github.com/Proven-Commons/json), [toml](https://github.com/Proven-Commons/toml), [csv](https://github.com/Proven-Commons/csv) (RFC 4180), [cbor](https://github.com/Proven-Commons/cbor) (RFC 8949), [protobuf](https://github.com/Proven-Commons/protobuf) (wire format) | -| Archives and files | [zip](https://github.com/Proven-Commons/zip), [png](https://github.com/Proven-Commons/png) (chunks and CRC-32) | -| Network protocols | [http](https://github.com/Proven-Commons/http) (RFC 9112 request line and headers), [websocket](https://github.com/Proven-Commons/websocket) (RFC 6455 frames), [dns](https://github.com/Proven-Commons/dns) (RFC 1035 header and question), [ip](https://github.com/Proven-Commons/ip) (addresses) | -| Identifiers and versions | [uuid](https://github.com/Proven-Commons/uuid) (RFC 9562), [rfc](https://github.com/Proven-Commons/rfc) (RFC 3339 timestamps), [semver](https://github.com/Proven-Commons/semver), [pep440](https://github.com/Proven-Commons/pep440) | - -**Planned, 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. +| Encodings | [codec](https://github.com/Proven-Commons/codec) (base64, hex, CRC-32), [utf](https://github.com/Proven-Commons/utf) (UTF-8), [bech32](https://github.com/Proven-Commons/bech32) (BIP 173, BIP 350), [punycode](https://github.com/Proven-Commons/punycode), [der](https://github.com/Proven-Commons/der) (ASN.1 DER element reader, X.690) | +| Data formats | [json](https://github.com/Proven-Commons/json), [toml](https://github.com/Proven-Commons/toml), [csv](https://github.com/Proven-Commons/csv) (RFC 4180), [cbor](https://github.com/Proven-Commons/cbor) (RFC 8949), [protobuf](https://github.com/Proven-Commons/protobuf) (wire format), [messagepack](https://github.com/Proven-Commons/messagepack), [bencode](https://github.com/Proven-Commons/bencode), [xml](https://github.com/Proven-Commons/xml) (safe subset, no document type declarations, no entities) | +| Archives and files | [zip](https://github.com/Proven-Commons/zip), [png](https://github.com/Proven-Commons/png) (chunks and CRC-32), [path](https://github.com/Proven-Commons/path) (lexical path cleaning) | +| Network protocols | [http](https://github.com/Proven-Commons/http) (RFC 9112 request line and headers), [websocket](https://github.com/Proven-Commons/websocket) (RFC 6455 frames), [dns](https://github.com/Proven-Commons/dns) (RFC 1035 header and question), [ip](https://github.com/Proven-Commons/ip) (addresses), [mqtt](https://github.com/Proven-Commons/mqtt) (MQTT 5.0 packet framing), [ntp](https://github.com/Proven-Commons/ntp) (wire packet parser), [dhcpv4](https://github.com/Proven-Commons/dhcpv4) (wire message parser), [clienthello](https://github.com/Proven-Commons/clienthello) (TLS ClientHello, RFC 8446), [ssh](https://github.com/Proven-Commons/ssh) (wire types and key blobs), [uri](https://github.com/Proven-Commons/uri) (reference resolution, RFC 3986), [hpack](https://github.com/Proven-Commons/hpack) (stateless part, RFC 7541) | +| Identifiers and versions | [uuid](https://github.com/Proven-Commons/uuid) (RFC 9562), [rfc](https://github.com/Proven-Commons/rfc) (RFC 3339 timestamps), [semver](https://github.com/Proven-Commons/semver), [pep440](https://github.com/Proven-Commons/pep440), [hostname](https://github.com/Proven-Commons/hostname) | +| Tokens | [jws](https://github.com/Proven-Commons/jws) (compact serialization parser and claim checks) | +| Wave 1 | [redis](https://github.com/Proven-Commons/redis) (RESP parser and small key-value store), [sqlite](https://github.com/Proven-Commons/sqlite) (file-format reader: header, pages, records), [cedar](https://github.com/Proven-Commons/cedar) (Cedar-style policy engine) | + +Wave 1 is open, not planned: redis and sqlite have a first slice on main, and cedar has a repo. Most of the repos above have a first slice on main. These repos hold a plan and no Lean code on main yet: cbor, http, uri, cedar, jws, mqtt, ntp, dhcpv4, clienthello, xml. Each project sends reusable lemmas to [CSLib](https://github.com/leanprover/cslib) and [Mathlib](https://github.com/leanprover-community/mathlib4), the shared libraries for computer science and mathematics in Lean. The shared library grows. The next project starts cheaper.