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.

Used in: Why Buran Had Four Computers, Not Three -- and What a Lean Proof Adds.

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: the 19th and last axiom line, 'NoPanic.slice_validated_uints_no_panic' depends on axioms: [propext, Classical.choice, Quot.sound], then Build completed successfully (1698 jobs). then extra axioms outside propext / Classical.choice / Quot.sound: (none) then PASS.

Would falsify: a fourth axiom or sorry in any axiom line, or extra axioms outside propext / Classical.choice / Quot.sound reporting anything other than (none) followed by PASS.

Typed replay of the verbatim local transcript of 2026-09-24 at pin d4cd6dc, run in a clean git worktree (the main checkout has an unrelated uncommitted change to llbc/cose_parse_nopanic.llbc): every command shown is the literal command run, every output line is the literal output. Two things are dropped, not rewritten: a worktree-specific absolute build path in the charon cargo step’s Compiling line, and Aeneas’s own \r-animated progress-bar spinner plus its two temp-path Info lines during aeneas -backend lean. One real difference from the original 2026-09-01 recording, kept rather than corrected: lake build’s 19 axiom-dependency lines now print before Build completed successfully, not after — a Lean/lake build-log ordering difference on this run, not a content change. 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-24: 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