Repository navigation
fix: proof coverage round 2 — 5 Kani proofs, 1 contract, best practices docs - #591
Merged
Merged
Conversation
New proofs: - byte_search: FindByteIter exhaustiveness (all positions yielded, ascending order, no duplicates/omissions) on 8-byte inputs - structural_iter: advance() completeness (all structural positions from merged bitmask yielded exactly once, ascending) on 8-byte inputs - structural: StructuralIndex::new() line ranges validity (valid bounds, no newlines inside ranges, contiguous) on 8-byte inputs - pipeline/lifecycle: reverse-order ACK with 4 batches (worst case for pending-ACK queue, checkpoint advances through all 4 on final ack) Contract: - structural: skip_nested() ensures result <= end (prevents reading past line boundary). Existing bounds proof promoted to proof_for_contract.
|
Note Reviews pausedIt looks like this branch is under active development. To avoid overwhelming you with review comments due to an influx of new commits, CodeRabbit has automatically paused this review. You can configure this behavior by changing the Use the following commands to manage reviews:
Use the checkboxes below for quick actions:
WalkthroughThis PR adds Kani proofs and contract annotations across crates/logfwd-core: an exhaustive 8-byte proof for Possibly related PRs
Comment |
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 3
🤖 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/pipeline/lifecycle.rs`:
- Around line 777-787: The in_flight_count assertions after calling
running.apply_ack are wrong: each acked batch is removed from the in_flight set
by apply_ack, so update the three assertions after apply_ack(s4.ack()),
apply_ack(s3.ack()), and apply_ack(s2.ack()) to expect counts 3, 2, and 1
respectively (instead of 4), keeping the existing assert! messages or adjusting
them if desired; locate the checks near the calls to running.apply_ack and the
in_flight_count() method to make the change.
In `@crates/logfwd-core/src/structural.rs`:
- Around line 1285-1294: The contiguity check incorrectly requires next_start ==
end + 1, which fails for blank lines; update the check in the block that
iterates line_ranges (using symbols line_ranges, range_idx, end, buf) to assert
that next_start > end and that every byte in buf[end..next_start] is a newline
(b'\n') rather than insisting on a single-byte gap; replace the
assert_eq!(next_start, end + 1, ...) with a loop or iterator-based check that
verifies buf[i] == b'\n' for i in end..next_start and keep the existing newline
assertion on the byte at end only when next_start == end + 1 or adjust to only
check bounds (use end < buf.len() / next_start <= buf.len() appropriately).
- Around line 362-364: The Kani contract for skip_nested is too weak because it
only requires end <= buf.len() and allows pos > end; strengthen the precondition
on skip_nested by adding pos <= end to the #[cfg_attr(kani,
kani::requires(...))] attribute (so it requires both end <= buf.len() and pos <=
end) to ensure the function's postcondition #[cfg_attr(kani,
kani::ensures(|result: &usize| *result <= end))] holds; update the kani requires
clause on the skip_nested function accordingly.
🪄 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: 2a292a0e-2fba-4d31-8c9c-d366202db766
📒 Files selected for processing (4)
crates/logfwd-core/src/byte_search.rscrates/logfwd-core/src/pipeline/lifecycle.rscrates/logfwd-core/src/structural.rscrates/logfwd-core/src/structural_iter.rs
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Contributor
|
Addressed all currently unresolved review threads with targeted code fixes and pushed commit
Validation
Note: Note 🔒 Integrity filtering filtered 1 itemIntegrity filtering activated and filtered the following item during workflow execution.
What is this? | From workflow: AI: Address PR Review Feedback Give us feedback! React with 🚀 if perfect, 👍 if helpful, 👎 if not. |
…endent oracles Improvements inspired by s2n-quic and Firecracker Kani patterns: - Add kani::cover!() to all new proofs to guard against vacuous verification - Replace hardcoded reverse-order 4-batch ACK with symbolic exploration of all 24 permutations - Add independent byte-level oracle to structural iterator proof (not trusting remaining_bits) - Verify bytes outside line ranges are all newlines (completeness property) - Add #[kani::solver(kissat)] to complex proofs for faster verification Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
There was a problem hiding this comment.
Actionable comments posted: 2
🤖 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/pipeline/lifecycle.rs`:
- Around line 804-814: The test only checks in_flight_count after the first
three running.apply_ack(...) calls and only checks checkpoint on the final call;
update the test to assert the returned ApplyResult (the values returned by
running.apply_ack, e.g., a1/a2/a3/a4) includes the correct advanced flag and
checkpoint after each call against the highest contiguous acked prefix (not just
on the final ack), and also keep asserting in_flight_count(); specifically, for
each call to running.apply_ack(r_x) assert that the returned object's advanced
boolean and checkpoint Option match the expected contiguous checkpoint (e.g.,
None or Some(cpN) as appropriate) and that running.in_flight_count() reflects
the remaining in-flight messages.
In `@crates/logfwd-core/src/structural_iter.rs`:
- Around line 551-565: The test currently compares yielded_bits to expected_bits
(copied from iter.remaining_bits) which only proves advance() mirrors internal
state; instead compute an independent oracle_bitmask from buf by scanning each
byte and setting the corresponding bit positions for structural classes
(matching the same bit layout used by remaining_bits/yielded_bits), then replace
assertions that compare yielded_bits == expected_bits with yielded_bits ==
oracle_bitmask; update both occurrences (the block around the initial 8-byte
scan and the similar block at lines ~606-609) and ensure the oracle construction
uses the exact byte-to-bit mapping used by load_block()/remaining_bits so the
assertion validates load_block()’s output, not the iterator’s cached state.
🪄 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: 18e65c91-22dc-4fb9-932e-fb31c2cdb11d
📒 Files selected for processing (4)
crates/logfwd-core/src/byte_search.rscrates/logfwd-core/src/pipeline/lifecycle.rscrates/logfwd-core/src/structural.rscrates/logfwd-core/src/structural_iter.rs
Comment on lines
+804
to
+814
| running.apply_ack(r_a); | ||
| assert_eq!(running.in_flight_count(), 3); | ||
| running.apply_ack(r_b); | ||
| assert_eq!(running.in_flight_count(), 2); | ||
| running.apply_ack(r_c); | ||
| assert_eq!(running.in_flight_count(), 1); | ||
| let a4 = running.apply_ack(r_d); | ||
|
|
||
| // After all 4 acked in any order, checkpoint must be cp4 | ||
| assert_eq!(a4.checkpoint, Some(cp4)); | ||
| assert_eq!(running.in_flight_count(), 0); |
There was a problem hiding this comment.
Assert checkpoint progression after each ACK.
The first three calls only validate in_flight_count(). A regression that commits a checkpoint too early on an out-of-order ACK would still satisfy every assertion here as long as the fourth call ends at Some(cp4). Please assert advanced and checkpoint after each apply_ack() against the highest contiguous acked prefix, not just the final state.
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed.
In `@crates/logfwd-core/src/pipeline/lifecycle.rs` around lines 804 - 814, The
test only checks in_flight_count after the first three running.apply_ack(...)
calls and only checks checkpoint on the final call; update the test to assert
the returned ApplyResult (the values returned by running.apply_ack, e.g.,
a1/a2/a3/a4) includes the correct advanced flag and checkpoint after each call
against the highest contiguous acked prefix (not just on the final ack), and
also keep asserting in_flight_count(); specifically, for each call to
running.apply_ack(r_x) assert that the returned object's advanced boolean and
checkpoint Option match the expected contiguous checkpoint (e.g., None or
Some(cpN) as appropriate) and that running.in_flight_count() reflects the
remaining in-flight messages.
…tion usage Add new sections based on research of large-scale Kani deployments: - kani::cover!() patterns for guarding against vacuous proofs - Symbolic ordering exploration via kani::any() - Independent oracle construction for iterator proofs - Solver selection strategy (kissat for slow proofs) - Performance pitfalls (multiplication explosion, deep call chains) - Complete partition verification for range-producing functions - Kani vs proptest vs Miri decision framework - Autoharness and --prove-safety-only for automated safety sweeps - #[safety_constraint] attribute for Arbitrary derive - Updated CLI reference and section numbering Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
There was a problem hiding this comment.
Actionable comments posted: 3
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Inline comments:
In `@docs/references/kani-verification.md`:
- Around line 3-4: The version note incorrectly implies contracts are globally
enabled by default; clarify that "contracts enabled by default since v0.62"
applies only to the autoharness flow. Update the Version line so it reads that
function and loop contracts are enabled by default for `cargo kani autoharness`
(not for regular `cargo kani`), and reference the manual flags `-Z
function-contracts` and `-Z loop-contracts` guidance already present elsewhere
to avoid contradiction with the instructions in the document.
In `@docs/VERIFICATION_GUIDE.md`:
- Around line 97-101: The guidance about kissat’s performance lacks attribution;
update the sentence that reads "kissat is fastest for ~47% of slow harnesses,
with speedups up to 265x" (near the mention of #[kani::solver(kissat)]) to
either cite the external benchmark source (add a reference link or bibliographic
citation) or explicitly mark it as project-internal (e.g., "In our benchmarks,
kissat...") so readers know the provenance of the numbers; ensure the same
change appears alongside the recommendation to use z3 or bitwuzla for
arithmetic-heavy proofs if relevant.
- Around line 115-121: Update the sentence that currently reads "This converts
O(2^N) verification into O(N)." to a more accurate formulation: replace it with
text along the lines of "This prevents exponential state-space explosion by
decomposing verification into N independent proofs, each verifying a bounded
slice of the call graph." Keep the surrounding guidance about adding
#[kani::requires]/#[kani::ensures], using proof_for_contract on leaf functions,
and using stub_verified in higher-level proofs so readers still get the workflow
while the complexity claim is corrected.
🪄 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: ee685a92-cd54-4a2c-8ee7-24460c74079f
📒 Files selected for processing (2)
docs/VERIFICATION_GUIDE.mddocs/references/kani-verification.md
- lifecycle.rs: assert advanced flag and checkpoint after each ACK, not just the final one; verify intermediate progression - structural_iter.rs: replace internal remaining_bits oracle with independent byte-level bitmask computed from buf directly, so the proof validates load_block() correctness, not just advance() draining - kani-verification.md: clarify that -Z function-contracts and -Z loop-contracts still require explicit flags for cargo kani; only auto-enabled in cargo kani autoharness flow - VERIFICATION_GUIDE.md: cite published benchmark source for kissat performance claims; rephrase O(2^N) complexity claim accurately Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
There was a problem hiding this comment.
Actionable comments posted: 1
♻️ Duplicate comments (1)
crates/logfwd-core/src/pipeline/lifecycle.rs (1)
804-823:⚠️ Potential issue | 🟠 MajorStrengthen intermediate ACK assertions (
a2/a3) to lock checkpoint progression.Line 813 and Line 816 only assert
in_flight_count(). That still allows premature checkpoint advancement regressions to pass if Line 821–Line 823 final-state assertions hold. Please assert expectedadvancedandcheckpointafter eachapply_ack, based on the highest contiguous ACKed prefix at that step.🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@crates/logfwd-core/src/pipeline/lifecycle.rs` around lines 804 - 823, The test only checks in_flight_count after apply_ack calls for a2 and a3, allowing incorrect checkpoint progression to slip through; update the assertions after running.apply_ack(r_b) and running.apply_ack(r_c) to also assert a2.advanced/a3.advanced and that a2.checkpoint/a3.checkpoint equal the highest contiguous checkpoint after that ACK (e.g., None or Some(cp1/cp2/cp3) as appropriate given which prefixes are now fully ACKed), mirroring the stronger checks already present for a1 and a4 and using the existing symbols apply_ack, running, a2, a3, cp1..cp4.
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Duplicate comments:
In `@crates/logfwd-core/src/pipeline/lifecycle.rs`:
- Around line 804-823: The test only checks in_flight_count after apply_ack
calls for a2 and a3, allowing incorrect checkpoint progression to slip through;
update the assertions after running.apply_ack(r_b) and running.apply_ack(r_c) to
also assert a2.advanced/a3.advanced and that a2.checkpoint/a3.checkpoint equal
the highest contiguous checkpoint after that ACK (e.g., None or
Some(cp1/cp2/cp3) as appropriate given which prefixes are now fully ACKed),
mirroring the stronger checks already present for a1 and a4 and using the
existing symbols apply_ack, running, a2, a3, cp1..cp4.
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: ASSERTIVE
Plan: Pro
Run ID: 88aeb4b4-2d1a-4a88-abea-5edcc5ef14d7
📒 Files selected for processing (4)
crates/logfwd-core/src/pipeline/lifecycle.rscrates/logfwd-core/src/structural_iter.rsdocs/VERIFICATION_GUIDE.mddocs/references/kani-verification.md
…search New sections from deep research of Kani's own test suite, blog posts, and release notes v0.55-v0.67: - old() in ensures clauses for mutation verification - kani::modifies semantics and havocking behavior - kani::slice::any_slice_of_array for variable-length slice proofs - kani::PointerGenerator for bounded pointer verification - Input space partitioning macros for intractable types - Performance stubbing pattern (lookup tables) - Source-based coverage analysis (cargo kani --coverage) - Rust Analyzer compatibility workaround - Cargo.toml metadata configuration - stub_verified v0.66 breaking change (requires contract harness) - while let loop contracts now supported (v0.66) - Float precision details (f16/f128, basic ops bit-precise) Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
A raw byte-level oracle (counting all structural bytes) is semantically too broad: advance() correctly suppresses delimiters inside JSON strings via process_block's string exclusion logic. Using remaining_bits as the oracle is sound because process_block's correctness is independently proven by verify_compute_real_quotes, verify_process_block_compositional, and verify_in_string_exclusion. This proof verifies that advance() correctly drains the classified bitmask in ascending order with no duplicates or omissions. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
strawgate
changed the title
This was referenced Apr 2, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
FindByteIter,PipelineMachine4-batch ACK (all 24 orderings),StructuralIndex::new()line ranges,StructuralIter::advance(), andskip_nestedcontract promotionskip_nestedwithrequires(pos <= end && end <= buf.len())/ensures(result <= end)Proofs
verify_find_byte_iter_exhaustiveverify_symbolic_order_ack_4_batchesverify_line_ranges_validverify_advance_yields_all_structuralverify_skip_nested_boundsproof_for_contract— provesresult <= endcontractBest practices applied (from s2n-quic, Firecracker, verify-rust-std patterns)
kani::cover!()on all new proofs to guard against vacuous verificationkani::any_where()instead of hardcoded permutations#[kani::solver(kissat)]on complex proofs for faster verificationDocs additions (kani-verification.md + VERIFICATION_GUIDE.md)
old()in ensures clauses,kani::modifiessemantics/havockingkani::slice::any_slice_of_array,kani::PointerGenerator, input space partitioning--prove-safety-only,stub_verifiedv0.66 breaking changewhile letsupport), float precision detailsNo production code changes — all modifications in
#[cfg(kani)]verification blocks and docs.Test plan
cargo test -p logfwd-core— 94 unit + 41 compliance + 66 conformance tests passcargo fmt+cargo clippy -D warningscleancargo kanion new harnesses (requires Kani toolchain)🤖 Generated with Claude Code