feat: adopt rust-refine runtime-enforced contracts on two pilot files (header.rs, varint.rs)

[iheitlager]

Description

Spike #371 (tests/spike/010_mvl_refinements/) concluded: rust-refine
(mvl-lang/mvl-rust) works and makes sense to adopt for runtime-enforced
contracts today. Across 6 rounds against successive releases, 5 real
upstream defects were found and fixed same-day by the maintainer. A
DatabaseHeader::parse-shaped postcondition now discharges 3 of 4
obligations at compile-time (L1), plus one pure-arithmetic proof at L4 —
the 4th falls back to a real assert! at every return path, which is
strictly stronger than today's unenforced doc comments.

This ticket adopts that pattern in production, scoped to exactly two
pilot files — not wider, until this closes and is reviewed.

Scope

1. src/header.rs — DatabaseHeader::parse and usable_page_size,
   using the corrected, already-proven annotations from the spike's
   src/lib.rs (not the issue's original, syntactically-invalid target
   annotation).
2. src/record/varint.rs — decode_varint: the loop bound 0..8
   (already informally documented via
   #[allow(clippy::arithmetic_side_effects, reason = "i ranges over the compile-time-constant 0..8, so i + 1 never overflows")]) and the
   returned length's 1..=9 range.

Plus:

• Add the mvl git dependency, pinned to the same rev the spike crate
  uses (tests/spike/010_mvl_refinements/Cargo.toml, currently v0.8.0 /
  3e3ade7).
• deny.toml: allow-git entry for mvl-lang/mvl-rust.
• CI: a build-from-git step for cargo-mvl, mirroring the existing
  mvl-limit gate's pattern in .github/workflows/ci.yml.

Complexity

Estimate: small
Reasoning: Both target functions and their annotations already
exist, verified working, in the spike crate — this is porting proven
annotations into production files plus routine dependency/CI wiring,
not new exploration. Two files only.

Context

See tests/spike/010_mvl_refinements/README.md for the full verdict and
findings.md for the round-by-round evidence. The spike crate stays in
place as the reference implementation — do not delete it when this
ticket lands.

Refs: 010_mvl_refinements spike, #371

Acceptance Criteria

• mvl dependency added, pinned, deny.toml updated
• DatabaseHeader::parse/usable_page_size annotated per the spike's
  proven form; cargo mvl prove src/header.rs output recorded in the
  PR description
• decode_varint annotated; cargo mvl prove src/record/varint.rs
  output recorded in the PR description
• CI wired to build cargo-mvl from the pinned rev, same pattern as
  mvl-limit
• Existing unit_header/unit_record (or equivalent varint) tests
  still pass with the runtime assert! injections live
• cargo clippy --all-targets / cargo fmt --check clean

Additional Notes

Not gated on full static proof — parse's 4th obligation stays
runtime-only pending a not-yet-filed upstream gap (same-function
return-site method-call reasoning, distinct from #110). That's fine:
the runtime-enforcement value is unconditional and doesn't need it.