formal(refinement): prove verify_envelope fail-closed gates on the extracted Rust

[hartsock]

Summary

Extends the Tier-3 (Charon/Aeneas) refinement to the top-level verify_envelope — the 6-step signed-object verifier. The prior #263 obligations covered the authority algebra + admit/resolve/store_id on the extracted code, but not the verifier's own fail-closed order. These three theorems discharge it on the actual Rust as extracted, abstractly over ANY SignedEnvelopeCodec / CryptoBoundary trait instance (Aeneas threads them as explicit dictionary args):

• Gate 1 — verify_envelope_undecodable_fails_closed: decode = None ⇒ Err(Undecodable); nothing downstream (canonicalization, signature, cid) is reached.
• Gate 2 — verify_envelope_non_canonical_fails_closed: a decodable envelope whose canonical re-encode does not byte-equal the received bytes ⇒ Err(NonCanonicalEnvelope), before any version/algorithm/signature/cid check. This is the anti-malleability law — verify against the received bytes, never a re-encode — closing signature-stripping / re-serialization attacks.
• Gate 3 — verify_envelope_version_mismatch_fails_closed: a canonical envelope with a mismatched profile version ⇒ Err(VersionMismatch). Unlike 1–2, this reduction threads through a passing gate (the ne = false canonical branch), demonstrating the technique follows the accept path, not only immediate short-circuits.

ok_or axiom → definition

core.option.Option.ok_or was an opaque axiom in FunsExternal.lean (the "fill the holes" template), which stalled any reduction through verify_envelope's Try-operator chain. Filled it with its exact std semantics (None ⇒ Err(e), Some(x) ⇒ Ok(x)) — this unblocks the reduction and removes an axiom from the extracted-code proof base.

Test plan

• Full just check-refinement green locally: lake build completes, 1702 jobs, no errors and no sorry in project declarations (the only sorry warnings are inside the Aeneas library's own axiomatized slice ops).
• Axiom footprint via #print axioms on all three theorems: [propext, Classical.choice, Quot.sound] — mathlib's standard base, no sorryAx, and no dependence on the former ok_or axiom.
• The Tier-3 refinement gate is deliberately not in the mandatory pre-push hook (it pulls the heavy Aeneas + mathlib backend); the fast formal/ Ceremony gate + Rust suite (which this PR does not touch) passed on push.

Out of scope

• The remaining verify_envelope gates (hash/sig/codec admit, signature-invalid, cid-mismatch, body-domain, unknown-critical) and the full accept path (Ok(VerifiedEnvelope)). Each follows the identical reduction pattern with more passing-gate hypotheses; deferred per freeze-minimally.
• Claims language: this narrows but does not by itself close audit §12 — the gates proven here are the verifier's order, not the underlying crypto assumptions (CryptoBoundary stays abstract).

---

Note

Low Risk
Lean-only formal verification changes; no runtime Rust or crypto behavior is modified.

Overview
Extends Tier-3 Charon/Aeneas refinement to verify_envelope, proving three early fail-closed gates on the extracted generic verifier (any SignedEnvelopeCodec / CryptoBoundary instances): undecodable → Undecodable, non-canonical bytes → NonCanonicalEnvelope before later checks, and version mismatch → VersionMismatch after a passing canonical step.

FunsExternal.lean replaces the opaque Option.ok_or axiom with a definitional implementation (None/Some → Err/Ok) so proofs can simp through the ?/Try chain and drop one axiom from the proof base.

Proofs live in Refinement.lean as simp-only theorems parameterized by decode/encode/canonical hypotheses.

^{Reviewed by Cursor Bugbot for commit d0aed1e. Configure here.}