verify: attempt theorem_pae_injective_on_types proof (audit C-1 progress)

[avrabe]

Second Verus admit attempt, after PR #108's discharge of `lemma_le64_injective`.

Proof structure

Replaces `assume(false)` in `theorem_pae_injective_on_types` with an explicit ~70-line proof:

1. Establish lengths of every prefix in `spec_pae`'s `Seq::add` chain. `spec_le64` always produces a length-8 sequence (8 explicit elements in the `seq!` macro); `Seq::add` is length-additive.
2. Contrapositive on `pae1 == pae2`:
   a. Total-length equality → `|type1| == |type2|`
   b. For every index `i`, derive `pae1[16+i] == type1[i]` via the `Seq::add` indexing axiom, applied through the four `.add`s of `spec_pae`. Same chain for `pae2`.
   c. Extensionality (`=~=`) lifts byte-wise agreement to `type1 == type2`, contradicting the `requires type1 != type2`.

This is the natural next-easiest admit after `lemma_le64_injective`: no SHA-256, no crypto, just structural reasoning over `Seq::add`.

Honesty caveat

The proof has not been validated locally — Bazel + Verus tooling was unavailable in the agent's sandbox. The Verus CI job carries `continue-on-error: true` (audit C-1 mask) so the worst case is the proof doesn't discharge and the `assert` chain becomes diagnostic documentation rather than a hard verification gate. The structured `assert` chain in the proof body is itself useful for the next attempt regardless.

What CI tells us

• ✅ Verus accepts the proof → audit C-1 partial closure advances one step
• ❌ Verus rejects some step → the failing `assert` gives precise diagnostic info for a follow-up; the `continue-on-error` mask keeps the job from blocking merge

Either way, no regression risk.

Refs: audit C-1.
Verifies (if Verus accepts): CR-3 (parser injectivity, payload-type component of PAE).

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!