Current state

Zip/Native/Gzip.lean implements native gzip and zlib container
decode (Gzip.decompress / Zlib.decompress). Both have a full set of
framing/trailer rejection guards that are present but pinned by no
targeted regression test:

gzip (Gzip.decompress):

• data.size < 10 → "Gzip: input too short for gzip header"
• bad magic (id1/id2 ≠ 0x1f/0x8b) → "Gzip: invalid magic bytes"
• CM ≠ 8 → "Gzip: unsupported compression method"
• truncated FEXTRA / header / trailer → respective "truncated …" msgs
• CRC32 mismatch → "Gzip: CRC32 mismatch: expected …, got …"
• ISIZE mismatch → "Gzip: size mismatch: expected …, got …"

zlib (Zlib.decompress):

• data.size < 6 → "Zlib: input too short"
• check % 31 ≠ 0 → "Zlib: header check failed"
• CM ≠ 8 → "Zlib: unsupported compression method"
• CINFO > 7 → "Zlib: invalid window size {cinfo}"
• FDICT set → "Zlib: preset dictionaries not supported"
• truncated trailer → "Zlib: truncated trailer"
• Adler32 mismatch → "Zlib: Adler32 mismatch: expected …, got …"

The only malformed-input coverage today is random field-mutation fuzz
(#2584 gzip, #2585 zlib), which checks native↔FFI accept/reject
parity — it does not assert which guard fired or pin the exact
error wording, so a reworded or mis-routed guard would pass.

Deliverables

1. New ZipTest/FramingGuards.lean with a ZipTest.FramingGuards.tests
   entry, registered in ZipTest.lean (import + call in main).
2. For each guard above: craft a minimal malformed container — start from
   a valid native-compressed gzip/zlib output (Gzip.compress /
   Zlib.compress over a short payload) and surgically corrupt exactly
   the targeted byte(s) (magic, CM nibble, FDICT bit, the 31-check, a
   trailer byte, or truncate) — feed it to the native decompress, and
   assert .error with the exact documented substring.
3. Cover both namespaces in the one file (single concern: "native
   container-framing/trailer guard regression").

Context

• Complement to, not overlap with, #2584/#2585: those are random fuzz
  asserting accept/reject parity; this pins the exact guard message
  for each hand-targeted corruption — a regression ratchet the fuzz can't
  provide. Reference them in the PR description.
• Plan-conforming: pins the trusted boundary (PLAN.md Track-E philosophy).
• Skills: error-wording-catalogue (message matching), checksum helpers
  in Zip/Native/Crc32.lean / Adler32.lean to build a deliberately
  wrong trailer.

Verification

• lake build && lake exe test passes (new tests included).
• Each corrupted container is rejected with the asserted exact message.
• Locally flip one guard's wording in Gzip.lean and confirm the suite
  fails, then revert.
• sorry count unchanged (0).