Background
PR #311 implemented roadmap item 4.1.3 ("Record the phase-1 Verus and Stateright boundary"). ExecPlan 4-1-3 was scoped as documentation-only and marked as approval-gated for any Makefile or CI modifications.
PR #311 introduced the following non-documentation changes:
- New
Makefile targets: install-kani, kani-check, install-verus, verus, with rust-prover-tools delegation via uv tool run.
- Updated
.github/workflows/ci.yml: installs uv, uses make install-kani, and revises the kani-smoke cache key.
- Deleted shell scripts:
scripts/install-kani.sh, scripts/check-kani-version.sh.
These changes were validated (tests pass, no CI failures after setup-uv fix) and a CodeRabbit agent review reported zero findings. However, no explicit on-record approval for the Makefile/CI scope extension under ExecPlan 4-1-3 was recorded in the ExecPlan document or the PR.
Required action
References
/cc @leynos
Background
PR #311 implemented roadmap item 4.1.3 ("Record the phase-1 Verus and Stateright boundary"). ExecPlan 4-1-3 was scoped as documentation-only and marked as approval-gated for any Makefile or CI modifications.
PR #311 introduced the following non-documentation changes:
Makefiletargets:install-kani,kani-check,install-verus,verus, withrust-prover-toolsdelegation viauv tool run..github/workflows/ci.yml: installsuv, usesmake install-kani, and revises thekani-smokecache key.scripts/install-kani.sh,scripts/check-kani-version.sh.These changes were validated (tests pass, no CI failures after setup-uv fix) and a CodeRabbit agent review reported zero findings. However, no explicit on-record approval for the Makefile/CI scope extension under ExecPlan 4-1-3 was recorded in the ExecPlan document or the PR.
Required action
docs/execplans/4-1-3-record-phase-1-scope-boundary-for-verus-and-stateright.mdthat the Makefile and CI changes were a necessary consequential extension of the documentation work, and note the approval decision (who approved, and when).References
docs/execplans/4-1-3-record-phase-1-scope-boundary-for-verus-and-stateright.md/cc @leynos