Skip to Content
AI agents & assistants — machine-readable index at /llms.txt
Verify mecose-parse-nopanic

A COSE parser shown not to panic while parsing a signed envelope. 19 theorems, machine-checked.

cose-parse-nopanic@d4cd6dc  · transcript · PROOF.md  · Lean CI  · CI run 

Hashes, tests, Charon, Aeneas, Lean. 19 theorems. Lean reports three axioms.

Machine-checked for the parser model extracted by Aeneas. Correspondence to the Rust source rests on Charon and Aeneas at the pinned versions and on the external definitions Aeneas reported as unknown.

Watch

Needs: a browser.

CI: run ci, 2026-08-28 , executed by GitHub Actions, not by me.

You should see: jobs rust and lean, both green; rust covers PROOF.sha256 and the Rust tests, lean covers Lean. Charon and Aeneas are not part of it.

Would falsify: a failed job.

You should see: 19 theorems, axioms: propext, Classical.choice, Quot.sound then extra axioms: (none) PASS.

Would falsify: a fourth axiom or sorry in the axiom list, or extra axioms reporting anything other than none.

Typed replay of the local transcript of 2026-09-01 at pin d4cd6dc. Output timing is not execution timing. The viewer did not reproduce it.

Run

Needs: Rust 1.92 or newer, Charon 909ff09a, Aeneas c2015b86, Lean 4.31.0. CI’s lean job (build only, no Charon or Aeneas) took 8 min 50 s on a GitHub Actions runner; the Charon/Aeneas transpile step is not timed.

git clone https://github.com/dzatona/cose-parse-nopanic.git && cd cose-parse-nopanic && git checkout d4cd6dc
shasum -a 256 -c reports/PROOF.sha256
cd rust && cargo test --manifest-path Cargo.toml
charon cargo --preset=aeneas --dest-file ../llbc/cose_parse_nopanic.llbc
aeneas -backend lean -dest ../lean ../llbc/cose_parse_nopanic.llbc
cd ../lean && lake build
# 19 theorems in NoPanic.lean: axioms [propext, Classical.choice, Quot.sound]

You should see: lake build exit 0 and all 19 #print axioms lines showing only propext, Classical.choice, Quot.sound.

Would falsify: a non-zero exit from lake build, a hash checked by PROOF.sha256 reported FAILED, or a fourth axiom (or sorry) in any #print axioms line.

Read

Needs: nothing to install.

Local run on 2026-09-01: PROOF.sha256 OK, 53 Rust tests passed, Charon exit 0, Aeneas generated CoseParseNopanic.lean and warned that the crate contains extracted external, unknown definitions, lake build 1698 jobs exit 0, all 19 #print axioms lines are propext, Classical.choice, Quot.sound — Lean axiom dependencies, not the full modeling or trust boundary. Pins: Charon 909ff09a, Aeneas c2015b86, Lean 4.31.0 — TOOLCHAIN.md .

Theorems: read_uint_no_panic, read_bstr_no_panic, read_bstr_fixed_64_no_panic, read_array_header_no_panic, read_map_header_no_panic, read_sign1_envelope_no_panic, decode_protected_header_no_panic, build_sig_structure_no_panic, parse_sign1_no_panic, write_bytes_dest_len_eq, sig_structure_len_le_max, read_head_ai0_23, read_head_ai0_23_spec, write_head_ai0_23_eq, take_ok_eq, read_head_ok_smallest_form, read_uint_ok_is_canonical, slice_validated_uints_loop_no_div, slice_validated_uints_no_panic.

Does not establish

  • Ed25519
  • verify_strict
  • full RFC 8949 / 9052 / 9053
  • encode-then-decode
  • kntrl-license-core in place
  • that the Lean model matches the Rust source; that correspondence rests on Charon 909ff09a and Aeneas c2015b86, which CI does not re-run, and on the external definitions Aeneas reported as unknown

GitHub Actions runs Rust tests, PROOF.sha256, and Lean; it does not run Charon or Aeneas.

If this does not survive your check, write me.

Last updated on
Verify meAPL Protocol