Skip to content

audit: resurrect Kani proof suite + 6 audit-gap proofs (Phase F + F+) #85

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
dcccrypto merged 15 commits into from
Apr 18, 2026
Merged

audit: resurrect Kani proof suite + 6 audit-gap proofs (Phase F + F+) #85

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
15 commits
Select commit Hold shift + click to select a range
aa109eb
fix: rename duplicate charge_fee_to_insurance (1-arg) to sweep_fee_de…
dcccrypto Apr 6, 2026
f8f91ca
fix(hygiene): annotate keeper_crank best-effort let _ patterns + guar…
dcccrypto Apr 16, 2026
98052a4
test(kani): repair stale proof harnesses for Phase F compatibility
dcccrypto Apr 17, 2026
a580e02
feat(kani): Phase F — 5 audit-gap proofs (healthy-immune, fee-bounded,
dcccrypto Apr 17, 2026
6768216
test(kani): resurrect tests/kani.rs (202 proofs) from upstream-diverg…
dcccrypto Apr 17, 2026
ce5707c
test(kani): fix fast_maintenance_margin to include MM floor + pos_margin
dcccrypto Apr 17, 2026
b496ac5
test(kani): unwind bumps + LQ4 cap fix + fee_split zeroed in test_params
dcccrypto Apr 17, 2026
ae710d9
test(kani): 5 more proof fixes — unwind bumps + stale-crank rewrite +…
dcccrypto Apr 17, 2026
04ef31c
test(kani): proof_gap1 conditional no-mutation (overflow unreachable)
dcccrypto Apr 17, 2026
bc4394e
test(kani): MAX_VAULT_TVL deposit fix + 3 bitwise-NOT bugs + 2 missin…
dcccrypto Apr 17, 2026
7746f00
test(kani): Phase F+ — 3-account haircut cascade topology proof
dcccrypto Apr 17, 2026
8ee87a4
Merge remote-tracking branch 'origin/master' into audit/kani-resurrect
dcccrypto Apr 17, 2026
448516d
test(kani): adapt P8321 funding proofs to Phase 3B Result<i64> signature
dcccrypto Apr 17, 2026
1e21b9a
style: cargo fmt — satisfy CI fmt check on PR #85
dcccrypto Apr 18, 2026
0e7dda0
chore: untrack rust_out binary + add to .gitignore
dcccrypto Apr 18, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,3 +39,4 @@ desktop.ini
.env
.env.local
test-ledger/
rust_out
63 changes: 63 additions & 0 deletions Cargo.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@ name = "percolator"
version = "0.1.0"
edition = "2021"
license = "Apache-2.0"
autotests = false

[lints.rust]
unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)', 'cfg(target_os, values("solana"))'] }
Expand Down Expand Up @@ -42,3 +43,65 @@ unstable = { stubbing = true }
[[workspace.metadata.kani.proof]]
harness = ".*"
unwind = 70

# Explicit test targets. autotests = false disables Cargo auto-discovery so
# `cargo kani --tests` does not attempt to parse broken/feature-gated test
# files (amm_tests.rs, fuzzing.rs, kani.rs) that depend on removed symbols
# (AccountKind enum, NoOpMatcher) or dev-dep macros Kani's frontend cannot
# expand. The file `tests/kani.rs` is intentionally not listed — it is kept
# on disk for future resurrection but is NOT part of any build target.
Comment on lines +47 to +52

@coderabbitai coderabbitai Bot Apr 17, 2026

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⚠️ Potential issue | 🟡 Minor

Stale comment contradicts the explicit [[test]] entries below.

The comment states that kani.rs is "intentionally not listed — it is kept on disk for future resurrection but is NOT part of any build target," yet tests/kani.rs is declared as a [[test]] target at lines 89–91 (consistent with the PR objective of resurrecting the 202-proof suite). Likewise, amm_tests.rs is called out as broken/feature-gated here but is now listed at lines 97–99. Please update this comment so future readers aren't misled about which test targets are active.

📝 Proposed comment update 
-# Explicit test targets. autotests = false disables Cargo auto-discovery so
-# `cargo kani --tests` does not attempt to parse broken/feature-gated test
-# files (amm_tests.rs, fuzzing.rs, kani.rs) that depend on removed symbols
-# (AccountKind enum, NoOpMatcher) or dev-dep macros Kani's frontend cannot
-# expand. The file `tests/kani.rs` is intentionally not listed — it is kept
-# on disk for future resurrection but is NOT part of any build target.
+# Explicit test targets. autotests = false disables Cargo auto-discovery so
+# `cargo kani --tests` does not attempt to parse feature-gated test files
+# (notably `tests/fuzzing.rs`, whose `proptest!` macro bodies fail to parse
+# when proptest isn't in scope). All other test files — including the
+# resurrected `tests/kani.rs` — are enumerated explicitly below.
📝 Committable suggestion

‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.

Suggested change
# Explicit test targets. autotests = false disables Cargo auto-discovery so
# `cargo kani --tests` does not attempt to parse broken/feature-gated test
# files (amm_tests.rs, fuzzing.rs, kani.rs) that depend on removed symbols
# (AccountKind enum, NoOpMatcher) or dev-dep macros Kani's frontend cannot
# expand. The file `tests/kani.rs` is intentionally not listed — it is kept
# on disk for future resurrection but is NOT part of any build target.
# Explicit test targets. autotests = false disables Cargo auto-discovery so
# `cargo kani --tests` does not attempt to parse feature-gated test files
# (notably `tests/fuzzing.rs`, whose `proptest!` macro bodies fail to parse
# when proptest isn't in scope). All other test files — including the
# resurrected `tests/kani.rs` — are enumerated explicitly below.
🤖 Prompt for AI Agents 
Verify each finding against the current code and only fix it if needed.

In `@Cargo.toml` around lines 47 - 52, Update the stale block comment to reflect
the current explicit [[test]] entries: remove the claim that tests/kani.rs is
"intentionally not listed" and that amm_tests.rs is broken/omitted, and instead
state that tests/kani.rs and amm_tests.rs are now included as [[test]] targets
(per the entries later in the file) as part of the 202-proof resurrection;
reference the existing symbols tests/kani.rs and amm_tests.rs and note that
autotests = false still disables Cargo auto-discovery but does not prevent these
explicit [[test]] entries from being built.

[[test]]
name = "proofs_arithmetic"
path = "tests/proofs_arithmetic.rs"

[[test]]
name = "proofs_audit"
path = "tests/proofs_audit.rs"

[[test]]
name = "proofs_instructions"
path = "tests/proofs_instructions.rs"

[[test]]
name = "proofs_invariants"
path = "tests/proofs_invariants.rs"

[[test]]
name = "proofs_lazy_ak"
path = "tests/proofs_lazy_ak.rs"

[[test]]
name = "proofs_liveness"
path = "tests/proofs_liveness.rs"

[[test]]
name = "proofs_safety"
path = "tests/proofs_safety.rs"

[[test]]
name = "proofs_v1131"
path = "tests/proofs_v1131.rs"

[[test]]
name = "proofs_phase_f"
path = "tests/proofs_phase_f.rs"

[[test]]
name = "kani"
path = "tests/kani.rs"

[[test]]
name = "unit_tests"
path = "tests/unit_tests.rs"

[[test]]
name = "amm_tests"
path = "tests/amm_tests.rs"

# NOTE: tests/fuzzing.rs is intentionally NOT declared as a [[test]] target.
# Its proptest! macro bodies parse as invalid Rust when proptest is not in
# scope, and activating the `fuzz` feature transitively activates `test`
# which reveals 600+ stale compile errors in unit_tests.rs. To run the
# proptest fuzz suite, either restore this entry locally with
# `required-features = ["fuzz"]` or copy fuzzing.rs into a separate crate.

Loading
Loading