Repository navigation

CBOR codec: implementation, specification, and round-trip proofs (in progress) - #2

Merged

orda-aska merged 21 commits into

mainfrom

ins-ember/cbor-codec

Oct 29, 2026

Merged

CBOR codec: implementation, specification, and round-trip proofs (in progress)#2
orda-aska merged 21 commits into
mainfrom
ins-ember/cbor-codec

Commits on Oct 25, 2026
- Add Spec/Defs.lean (UTF-8 validator definitions)
  ahrazzle
  authored
  3e4a159
- Add .gitignore
  ahrazzle
  authored
  6532d76
- Add lean-toolchain
  ahrazzle
  authored
  77341e7
- Add lakefile.toml
  ahrazzle
  authored
  5fef46e
- Add Cbor.lean
  ahrazzle
  authored
  a80cfe6
- Add Main.lean
  ahrazzle
  authored
  6c2987e
- Add Proofs.lean
  ahrazzle
  authored
  9934353
- Add SPEC.md
  ahrazzle
  authored
  c404e22
- Add Spec.lean
  ahrazzle
  authored
  9e40ca6
- Add comparator.json
  ahrazzle
  authored
  9107170
- Add lake-manifest.json
  ahrazzle
  authored
  daab51f
- Add Cbor/Utf8.lean
  ahrazzle
  authored
  da25c40
- Add Cbor/Basic.lean
  ahrazzle
  authored
  7b76dce
- Add tests/TEST-RESULTS.md
  ahrazzle
  authored
  980d9e1
- Add tests/run_tests.py
  ahrazzle
  authored
  1e72eb6
- Add Proofs/Cbor.lean
  ahrazzle
  authored
  3d93756
- Spec/Defs.lean: correct spec status to unreviewed
  ahrazzle
  authored
  25921d2
- Add bar.toml
  ahrazzle
  authored
  5eda243
- README: CBOR codec slice overview and status
  ahrazzle
  authored
  5836258
- comparator.json: fix closing-brace indentation
  ahrazzle
  authored
  3318687
- Add Proofs/RoundTrip.lean (round-trip theorems)
  ahrazzle
  authored
  77ae41f