[strawgate]

Summary

Cherry-picked the valid parts from closed PR #638 (which had broken contracts and was not compiled/Kani-verified).

• kani::cover!() vacuity guards added to 11 existing Kani proofs across 5 files
• Kani Verification Requirements section added to AGENTS.md

What was dropped from #638

• Broken #[kani::ensures] contract on parse_cri_line (used unsafe in #![forbid(unsafe_code)] crate)
• Wrong hex_nibble contract (ensures result <= 15 but function returns 0xFF)
• Circular self-stub on bytes_field_size
• Unverified scan_string contract (no proof harness)
• Fabricated KANI_PATTERNS.md and VERIFICATION_GUIDE.md docs
• Deletion of SourceRegistry from Phase 5c

What vacuity guards do

kani::cover!() prevents proofs from being vacuously true. If kani::assume() constraints are too restrictive, the proof passes without testing any real paths. Cover guards assert that interesting cases are reachable:

kani::cover!(output.len() > 0, "non-empty output");
kani::cover!(output.len() == max_size, "max size reached");

If Kani reports a cover as unreachable, the proof's assumptions need loosening.

Test plan

• cargo check -p logfwd-core passes
• 218 tests pass across logfwd-core
• clippy clean
• cargo fmt clean
• CI passes

🤖 Generated with Claude Code

[coderabbitai]

Caution

Review failed

The pull request is closed.

ℹ️ Recent review info

⚙️ Run configuration

Configuration used: Organization UI

Review profile: ASSERTIVE

Plan: Pro

Run ID: 1b06e99d-e44c-47e0-b7de-f828cddc41a2

📥 Commits

Reviewing files that changed from the base of the PR and between 390b98c and 338e8ff.

📒 Files selected for processing (1)

• crates/logfwd-core/src/aggregator.rs

---

Walkthrough

This PR adds a "Kani Verification Requirements" section to AGENTS.md specifying when Kani proofs are required and the expected proof-quality rules, and it augments existing Kani verification harnesses by inserting kani::cover! assertions in aggregator.rs, byte_search.rs, cri.rs, json_scanner.rs, and scanner.rs to ensure non-vacuous coverage of boundary and branch outcomes. No runtime logic, control flow, exported APIs, or production code were changed.

Possibly related PRs

• PR 311: Edits the same Kani verification harnesses (aggregator, byte-search, cri, JSON/scanner) and introduces the proof functions that this PR tightens with coverage assertions.
• PR 575: Makes verification-focused changes across the same modules (aggregator, cri, json_scanner, byte_search, scanner), overlapping with the coverage additions here.
• PR 324: Touches Kani verification for crates/logfwd-core/src/cri.rs and introduces semantic proofs/behavioral changes to parsing that are closely related to the cri.rs coverage updates in this PR.

---

_{Comment @coderabbitai help to get the list of available commands and usage tips.}

[coderabbitai]

Actionable comments posted: 1

🤖 Prompt for all review comments with AI agents

Verify each finding against the current code and only fix it if needed.

Inline comments:
In `@crates/logfwd-core/src/aggregator.rs`:
- Around line 301-303: The third Kani coverage check is inverted: replace or add
to the current kani::cover!(out.len() < 24, "all parts fit") so it actually
checks the non-truncated case by using out.len() == 24 (or include both ==24 and
<24 explicitly), and ensure these kani::cover!() calls (including the existing
multi-partial and truncation covers referencing out.len() and max_size) remain
placed after the assertions that make the proof meaningful; update the message
string to "all parts fit" for the new ==24 condition so it covers the intended
no-truncation path.

🪄 Autofix (Beta)

Fix all unresolved CodeRabbit comments on this PR:

• Push a commit to this branch (recommended)
• Create a new PR with the fixes

---

ℹ️ Review info

⚙️ Run configuration

Configuration used: Organization UI

Review profile: ASSERTIVE

Plan: Pro

Run ID: 3981ddd5-cb0a-495e-855d-b214045f2eb6

📥 Commits

Reviewing files that changed from the base of the PR and between f6f9784 and 390b98c.

📒 Files selected for processing (6)

• AGENTS.md
• crates/logfwd-core/src/aggregator.rs
• crates/logfwd-core/src/byte_search.rs
• crates/logfwd-core/src/cri.rs
• crates/logfwd-core/src/json_scanner.rs
• crates/logfwd-core/src/scanner.rs