Skip to content

Update org profile README for the new repos #3

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
orda-aska merged 1 commit into from
Oct 28, 2026
Merged

Update org profile README for the new repos #3

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 9 additions & 7 deletions profile/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down
Loading