4.1.1 follow-up: tests and documentation for Kani shell scripts

[coderabbitai]

Follow-up from PR #305

The Kani tooling and local smoke targets introduced in #305 require automated tests and improved documentation for the new shell scripts and Makefile targets.

Note: Tests for shell scripts must be written in Python using pytest and pytest-bdd (where appropriate), using:

• cuprum for shell execution
• cmd-mox for command mocking

---

❌ Errors

1. Testing (Overall)

Substantial functionality was added (installer, version checks, Makefile targets) with only manual smoke validation. No automated tests prevent future regressions or catch broken implementations.

Resolution: Add tests for:

• scripts/install-kani.sh — version format validation, missing-file handling
• scripts/check-kani-version.sh — version mismatch detection, missing pin file, malformed version output
• Makefile targets (kani, kani-full, formal-pr) via shell integration tests

2. Module-Level Documentation

New Bash scripts contain only single-line doc comments. The project requires comprehensive header comments explaining purpose, utility, function, and relationships to other components.

Resolution: Expand module-level documentation in:

• scripts/install-kani.sh
• scripts/check-kani-version.sh

Each script's header must cover: purpose, utility, function, parameters, exit codes, and Makefile integration.

---

⚠️ Warnings

3. Docstring Coverage

Docstring coverage is 0.00%, below the required threshold of 80.00%.

Resolution: Write docstrings for all functions in the new scripts (at minimum fail() and require_command() in scripts/install-kani.sh).

4. Testing (Unit and Behavioural)

PR adds Makefile targets and shell scripts for command-line execution but provides no tests for them. The project requires tests for system-level behaviour changes.

Resolution: Add tests covering:

• Shell scripts' error paths (e.g., missing cargo, malformed version pin, version mismatch)
• Edge cases and invariants for check-kani-version.sh
• Makefile target invocation and expected output

---

Raised by @leynos from review of #305.

[coderabbitai]

🔗 Related PRs

leynos/df12-documentation-skills#4 - Roadmap and Verification Refinements [merged]
leynos/rstest-bdd#488 - Extend first-party policy hint resolution (9.7.1) [merged]
leynos/prosidy-darn#9 - Create baseline developer docs and ADR locations (1.0.1) [merged]
leynos/beatcue#10 - Run Pylint through the PyPy shim [merged]
leynos/prosidy-darn#10 - Add PyPy-backed Pylint lint tier [closed]

---

📝 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!