Add a positive-path conformance regression suite for native gzip header
optional fields — FEXTRA / FNAME / FCOMMENT / FHCRC — confirming
Zip.Native.GzipDecode.decompress correctly skips each populated optional
field and recovers the payload, both round-tripping to the original and agreeing
with the zlib FFI.

Current state

Zip/Native/Gzip.lean parses the four optional header fields gated by the FLG
byte (FEXTRA 0x04, FNAME 0x08, FCOMMENT 0x10, FHCRC 0x02; see
Zip/Native/Gzip.lean:63–78, using Binary.readUInt16LE for the FEXTRA
length and scanToZero for the NUL-terminated FNAME/FCOMMENT). No test in
ZipTest/ populates any of these fields — grep -rl 'FNAME\|FEXTRA' ZipTest/
is empty. Every existing gzip test uses a bare header (no optional fields).
The malformed-side is covered (fuzz #2584, framing-guards #2590) but the valid,
fully-populated path is unverified: a bug in the field-skip arithmetic (e.g. an
off-by-one in scanToZero+NUL or in pos + 2 + xlen) would silently corrupt
the inflate start offset and is currently untested on accepting inputs.

Deliverables

1. Fixture builder (in the new test module, deterministic — no
   Date.now/ambient entropy): a helper that hand-assembles a valid gzip member
   with a chosen subset of optional fields set in FLG and the corresponding bytes
   present — FEXTRA (a small XLEN-prefixed subfield blob), FNAME (a
   NUL-terminated name), FCOMMENT (a NUL-terminated comment), FHCRC (2-byte
   header-CRC; value need not be checked by the decoder, just skipped) — over a
   deflate body produced from a fixed payload, with correct trailing CRC32 + ISIZE.
   Follow the malformed-fixture-builder skill's builder shape/determinism
   checklist (this is the positive analogue).
2. Conformance assertions (ZipTest/NativeGzipOptional.lean, registered in
   ZipTest.lean): for each field individually, the union of all four, and a
   bare-header control, assert
   GzipDecode.decompress member == original payload and
   GzipDecode.decompress member == FFI decompress member (native ⊆ FFI on the
   accept side — both must accept and agree, since these are well-formed). Cover
   edge cases: empty FNAME (immediate NUL), empty FEXTRA (XLEN = 0), and an
   empty payload with all optional fields set.
3. Keep it tests-only — no library/spec change expected. If the suite
   surfaces a real decoder bug, fix it minimally in Zip/Native/Gzip.lean (no
   spec-statement change) and note it in the PR.

Context

This is the positive-path complement to the malformed gzip fuzz (#2584) and the
framing/trailer reject guards (#2590): those assert the decoder rejects
mutated headers; this asserts it accepts and correctly skips every valid
optional field. Distinct from the concatenated-member cap (#2594) and the
output-size cap (#2577). The native decoder must remain a faithful subset of the
FFI on well-formed input.

Verification

• lake build && lake exe test green; new module registered in ZipTest.lean.
• grep -rc sorry Zip/ = 0 (unchanged); no native_decide.
• New test file is ZipTest/NativeGzipOptional.lean; any decoder fix is confined
  to Zip/Native/Gzip.lean and changes no spec statement.
• PLAN.md / .claude/CLAUDE.md off-limits.