Decide if we should keep kani and restructure or remove it

[sysheap]

Currently we have a lot of conditional compilation in the kernel to make kani work with riscv64. We need to consider if it is worth the effort or if we want to remove kani. If the effort is worth it, we should somehow restrucutre, so we don't need the #[cfg] statements anymore.

[sysheap]

@claude Move that into one of the milestones and decide where it is appropriate. Also plan it in more detail.

[claude]

Claude finished @sysheap's task in 3m 30s —— View job

---

Analysis & Detailed Plan for Kani Integration

• Check existing milestones (blocked by API access restrictions — see note below)
• Examine Kani usage in codebase
• Develop detailed plan
• Assign milestone (needs manual action — see below)

---

Current State

The #[cfg(kani)] usage in the codebase is already minimal — only 5 locations:

File	Usage	Removable?
kernel/build.rs:13	Registers kani as valid cfg flag	Only if removing Kani
kernel/src/main.rs:9	feature(maybe_uninit_slice) for Kani's nightly toolchain	Only if removing Kani
kernel/src/main.rs:288	Empty fn main() stub (kernel is #![no_main])	Only if removing Kani
kernel/src/memory/address.rs:124	mod kani_proofs — 5 proof harnesses	Standard pattern
kernel/src/memory/page_table_entry.rs:166	mod kani_proofs — 4 proof harnesses	Standard pattern
kernel/src/klibc/util.rs:250	mod kani_proofs — alignment proofs	Standard pattern

The arch crate already has arch/src/stub/ providing no-op implementations for non-riscv64 targets, so Kani can compile the kernel without hardware dependencies.

Recommendation: Keep Kani

The value proposition is strong:

• Formal verification of memory-critical code (address types, page table entries, alignment utilities) — exactly the kind of code where off-by-one bugs are catastrophic
• Proofs are co-located with the code they verify (mod kani_proofs inside the same file), making them easy to maintain
• The 2 shims in main.rs are unavoidable given the no_std/no_main kernel architecture

Restructuring Plan

The mod kani_proofs pattern is already the idiomatic and correct structure (per CLAUDE.md). The only real "noise" is the two shims in main.rs. There are two restructuring options:

Option A: Separate kani-proofs crate (recommended)

• Create a new crate kani-proofs/ that depends on the kernel crate
• Move all proof harnesses there
• This eliminates #[cfg(kani)] from the kernel entirely (except build.rs)
• Con: Slightly more complex setup; proofs are no longer co-located with the code

Option B: Keep current structure, clean up main.rs shims

• The #[cfg(kani)] blocks in proof modules are idiomatic — leave them as-is
• The main.rs shims (2 lines) are the only non-standard part; these are unavoidable
• No meaningful restructuring needed — the issue may have been written before the current cleanup
• This is the minimal-effort path

Verdict: Option B — the current structure is already clean. Option A adds complexity for minimal gain. The #[cfg(kani)] pattern for proof modules is the Kani-recommended approach.

Detailed Task Breakdown

1. Investigate if there was previously more #[cfg(kani)] noise — check git history to confirm the current state is already post-cleanup (may already be done)
2. Add Kani to CI — confirm just kani runs in CI pipeline and document this in doc/ai/TESTING.md
3. Expand Kani coverage — identify more pure functions that would benefit from proofs (candidates: page_tables.rs VPN extraction, any new bit-manipulation code)
4. Close issue — document the decision and close as "won't fix / already done"

---

Milestone Recommendation

Note: I was unable to directly access the GitHub milestones API in this environment. You'll need to assign the milestone manually with: gh issue edit 188 --milestone "<milestone-name>" --repo sysheap/solaya

Based on the nature of this work (tooling/code quality, not user-facing), this belongs in a "Code Quality & Tooling" or "Infrastructure" milestone. It has low urgency since the current state is already acceptable — prioritize after any milestone focused on features or stability.

[sysheap]

Kani was removed