verify: discharge lemma_le64_injective

[avrabe]

Summary

Replaces the assume(false) in lemma_le64_injective (src/lib/src/verus_proofs/dsse_proofs.rs) with an explicit four-step proof. Discharges one of the relabeled SPECIFICATION ONLY theorems from audit C-1; the remaining admits in dsse_proofs.rs and merkle_proofs.rs are unchanged.

Proof technique

1. Bit-vector tautology (Step 1). A single assert(...) by(bit_vector) proves the closed quantifier-free goal: if the eight 0xFF-masked shifts of a agree with the corresponding shifts of b, then a == b. This is a pure tautology in BitVec64 — every bit of a and b lives in exactly one byte-slice.

2. u8 <-> u64 bridge (Step 2). Eight concrete <==> asserts (also by(bit_vector)) lift each (x & 0xFF) as u8 == (y & 0xFF) as u8 to (x & 0xFF) == (y & 0xFF). The truncating cast is value-preserving because the mask already truncates to [0, 0xFF]. Concrete instantiations avoid trigger headaches.

3. spec_le64 unfolding (Step 3). Sixteen unfolding asserts expose spec_le64(x)[i] == (x >> 8*i) & 0xFF as u8 for each i in 0..8. These are pure macro/spec identities; they hold unconditionally.

4. Conditional contradiction (Step 4). Under sa == sb, congruence on == gives the eight byte equalities sa[i] == sb[i]. The bridges (Step 2) lift those to u64 mask equalities; the bv tautology (Step 1) forces a == b, contradicting requires a != b. Outside the branch, sa != sb is the goal directly.

Why this should work

• spec_le64 is pub open spec fn, so Verus sees through it.
• seq![x0..x7][i] reduces to xi by the seq! macro expansion.
• Z3's bit-vector backend (via by(bit_vector)) reliably decides the closed Step-1 goal; it is small (eight 8-bit slices of a 64-bit value).
• The if sa == sb { ... assert(a == b); } pattern is the standard Verus idiom for proof-by-contradiction over an equality goal.

Honesty notes

• Could not run bazel build //src/lib/src/verus_proofs:wsc_merkle_proofs locally — Bazel toolchain download failed (no space left on device). The proof must be validated by CI.
• The Verus job in .github/workflows/formal-verification.yml still has continue-on-error: true per the partial-closure plan (per the task brief, the CI mask should stay until more admits are discharged). So this PR's CI will not block on the Verus job, but the bazel build logs will reveal whether the proof actually verified.
• If CI reports the proof did not discharge, the next iteration starts by inspecting which assert(...) Verus rejected — the Step-1 bv assert is the most likely friction point (slicing reasoning vs Z3's bv decision procedure performance), with a fallback being eight per-byte bv asserts joined explicitly.

Test plan

• cargo build --workspace --release clean (verified locally — Verus annotations are inert outside Bazel).
• bazel build //src/lib/src/verus_proofs:wsc_merkle_proofs reports verification successful for lemma_le64_injective. Other admits in the file remain assume(false) so the file as a whole still verifies (because assume(false) makes the obligation vacuous).
• CI's Verus job log (under continue-on-error: true) shows one fewer admitted lemma.

Scope

• Only src/lib/src/verus_proofs/dsse_proofs.rs is touched.
• formal-verification.yml is intentionally left alone — CI mask removal is a follow-up after more admits land.

Refs: audit C-1
Verifies: CR-3 (parser injectivity property of PAE encoding)

Generated with Claude Code