CI: run the bounded Kani harness set in the kani-smoke PR job

[lodyai]

Background

Roadmap 4.1.2 shipped the dedicated kani-smoke CI job (PR #308). As scoped
at the time, the job runs only the bounded smoke path — currently
make install-kani followed by make kani-check (a Kani version check) —
because no proof harnesses existed yet. Populating the bounded harness set was
explicitly deferred to the 4.2.* roadmap work (see
docs/execplans/4-1-2-kani-smoke-ci-job.md, Risk section).

Current gap

4.2.1 and 4.2.2 have since landed real harnesses (nine IR harnesses plus
four cycle-canonicalization harnesses; 13 #[kani::proof] total). However, the
kani-smoke PR job still runs only make kani-check, so those bounded
harnesses are not exercised on pull requests.

Proposed work

• Point the kani-smoke PR job at the bounded harness set (e.g. make kani-ir
  / make kani-full) instead of, or in addition to, make kani-check.
• Keep the existing build-test job unchanged and preserve the isolated Kani
  cache (.kani-cargo / .kani-home, keyed on tools/kani/VERSION).
• Confirm the cold-run wall-clock stays within the execplan tolerance (the
  4.1.2 plan flagged a 20-minute ceiling).

References

• docs/roadmap.md — 4.1.2 (third subtask signposts this issue).
• docs/execplans/4-1-2-kani-smoke-ci-job.md.
• .github/workflows/ci.yml — kani-smoke job.

[coderabbitai]

🔗 Related PRs

leynos/theoremc#15 - Add ExecPlan: Enforce non-vacuity defaults (Step 1.2.4) [closed]
leynos/theoremc#42 - Gate generated Kani harnesses (3.2.2) [closed]
#417 - Enable the CodeScene mode: check coverage gate [merged]
leynos/frankie#98 - Wire the CodeScene mode: check coverage gate [merged]
#444 - docs(roadmap): correct 4.1.2 CI claim and add implementor notes [open]

---

📝 Issue Planner

_{Check the box below or use the @coderabbitai plan command to generate an implementation plan and prompts that you can use with your favorite coding assistant.}

• Create Plan

---

🧪 Issue enrichment is currently in open beta.

You can configure auto-planning by selecting labels in the issue_enrichment configuration.

To disable automatic issue enrichment, add the following to your .coderabbit.yaml:

issue_enrichment:
  auto_enrich:
    enabled: false

💬 Have feedback or questions? Drop into our discord!