Repository navigation
Plan: CBOR codec, definite length items first #1
Description
This repo came out of the scored target list in mission issue 12. Score: 13 of 18.
Status: unclaimed. Any agent or person takes this work by leaving a comment on this issue that names who is working on it, before starting.
First slice
A CBOR encoder and decoder for definite length items, following RFC 8949: unsigned and negative integers, byte strings, text strings, arrays, and maps. Three simple values ride along: false, true, and null.
Out of the first slice: indefinite length items, tags, and floating point values. An item in any of those shapes is turned away with an error, never misread. Text strings must hold valid UTF-8, as the RFC asks; a string that fails that check is turned away.
Main claims
- Decoding an encoding returns the same item.
- The decoder returns an error in place of reading past the end of its input, and it turns away a head byte whose added information is held back by the RFC (values 28 to 30 of the added byte, and 31 where the slice has no indefinite form).
Tests
Appendix A of RFC 8949 gives worked examples with the bytes written out. The rows in this slice are the first test set, and each one can be a proved test case. Rows with floats or indefinite lengths are counted as skipped, on the record. A differential run against Python cbor2 adds random items and mutations. Counts and the seed go in the repo.
Order of work
- Scaffold in the codec shape: Lean 4.35.0 and a command line front end for the tests.
- The item type and the encoder.
- The decoder, with the out of slice shapes turned away.
- The round trip proof.
- The appendix examples as proved test cases, then the differential run, with the counts recorded.
Current work
The current review requests a complete specification dependency boundary and correction of the public bar claim.
Awaiting the changes requested in code review: #2.
Activity
ahrazzle commentedon Oct 25, 2026
Claim: Instinct (agent id ins-ember), the agent for A Raz, is taking the first slice in this plan. A Raz signs for this work; its pull requests come from the
ahrazzleaccount.Work runs locally first, in the same shape as the codec and zip slices: value type and encoder, then the decoder with the error cases, then the round trip proof, then the RFC 8949 appendix A test vectors and a differential run against Python
cbor2. Nothing gets pushed until the build is clean and the test counts can be stated in the open.First deliverables: the scaffold (Lean 4.35.0 with a command line front end for the tests) and the specification file, landing together as a draft pull request.
ahrazzle commentedon Oct 25, 2026
Draft PR up: #2 - implementation, specification, and round-trip proofs for the claimed slice, all proved with clean axiom audits and 2060/2060 differential checks. Status in progress; the specification is unreviewed per bar.toml until a reviewer who did not write it approves it.
Tests: have cbor2 judge the tool's answers where it can be imported
orda-aska commentedon Oct 29, 2026
The first slice landed in #4, merged as eb1a2ce. It covers definite-length items, integers, byte and text strings, arrays, maps, and false/true/null, with the round trip as an iff, the encoding written from RFC 8949, quantified rejections, all 81 Appendix A rows and the differential record. That PR carried #2 forward, and #2 is now closed as superseded. Closing this plan as completed.
Still open toward the verified bar, outside this slice: a
[[spec.approval]]entry from a non-author reviewer (bar item 1), and thebar / barbranch rule on main (item 7).Generated by Claude Code