fix(proofs): Kani proof CoverageEntry init missing exempt/exempt_ids (REQ-309, #848)

[avrabe]

The failure

Kani Proofs fails on every PR head off current main with a two-field struct-init mismatch:

error[E0063]: missing fields `exempt` and `exempt_ids`
              in initializer of `coverage::CoverageEntry`
   --> rivet-core/src/proofs.rs:216:21

Reproduces on main @ 83c7d91 and on my #864 head. Surfaced by the Kani check on that PR — the diff there doesn't touch rivet-core at all, so the failure isn't its.

Root cause

REQ-309 / #848 added two fields to CoverageEntry in rivet-core/src/coverage.rs:

pub struct CoverageEntry {
    ...
    pub covered: usize,
    pub exempt: usize,            // ← new in REQ-309
    pub exempt_ids: Vec<String>,  // ← new in REQ-309
    pub external_boundary: usize,
    ...
}

The Kani harness proof_coverage_percentage_bounds (rivet-core/src/proofs.rs:216) builds a CoverageEntry field-by-field and wasn't updated when the fields landed. mod proofs is gated on #[cfg(kani)], so plain cargo check -p rivet-core doesn't compile it — that's how the miss escaped the merge of #848.

The fix

Initialize both new fields to their empty values (exempt: 0, exempt_ids: vec[]). The proof asserts bounds on percentage(), which reads only covered and total, so the empty values are the correct inputs and preserve the existing proof's semantics.

Why it wasn't caught

Kani Proofs is continue-on-error: true and outside ci-gate's needs: (issue #839), so a red Kani doesn't block the merge and this regression rode along invisibly across every subsequent PR. #839 flags Kani's environmental flakes (exit 143 / SIGTERM); this failure is a different mode — a deterministic compile error — that #839's flake pattern was masking.

Verification

• cargo check -p rivet-core — clean before and after (the #[cfg(kani)] gate makes this insensitive to the change).
• Structural verification by inspection: the two added fields, in canonical order matching the struct at coverage.rs:59-95, exactly the fields the E0063 error names.
• The Kani check on this PR is itself the reproduction+fix loop.

Commit trailer

Fixes: REQ-309, Refs: #848, #839, #864.

---

Generated by Claude Code

[github-actions]

📐 Rivet artifact delta

No artifact changes in this PR. Code-only changes (renderer, CLI wiring, tests) don't touch the artifact graph.

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!

[avrabe]

CI Gate is green on c2be4a1 — the required rollup passed. Standing down on the two advisory reds:

Kani Proofs — runner shutdown, not the fix. The log shows rivet-core compiling successfully (past the original E0063), then:

##[error]Process completed with exit code 143.
##[error]The runner has received a shutdown signal. This can happen when the runner service is stopped, or a manually started runner is canceled.

Exit 143 = SIGTERM. This is precisely the self-hosted-fleet-restart pattern #862 documents (and one #839's failures were probably conflating). The fix itself compiled cleanly before the runner went away, so the E0063 is genuinely resolved. Will spend the one re-run for this per the drive-to-green rules.

Mutation Testing (rivet-core, PR-diff) — advisory, surviving mutant is in Kani-gated code. The log:

Surviving mutants in rivet-core (diff-scoped): 1
##[error]1 mutant(s) survived in code this PR changed — add tests to kill them
       (advisory — the workflow does not fail on this until promotion)
rivet-core/src/proofs.rs:209:9: replace proofs::proof_coverage_percentage_bounds with ()

Line 209 is the #[kani::proof] function body itself. Kani proof harnesses live inside #[cfg(kani)] mod proofs { ... }, so no cargo test-driven test exercises them and no property this PR added can kill this mutant — the coverage gap is structural, not introduced by this diff. The workflow explicitly labels this advisory-until-promotion. Would be worth a follow-up issue on how the mutation gate treats #[cfg(kani)]-gated code (skip it, or run cargo-mutants with --cfg kani), but that's out of scope here.

---

Generated by Claude Code