merge: sync upstream aeyakovenko/percolator v12.1 (136 commits)

[dcccrypto]

Summary

• Merges 136 commits from aeyakovenko/percolator upstream/master into our fork
• All conflicts resolved — our fork additions preserved, upstream safety fixes adopted
• All tests pass (54 lib tests + all integration suites)

Upstream safety fixes adopted

• haircut overflow: returns 0 instead of panicking
• settlement circuit-breaker bypass: fixed 3 paths
• force_close_resolved bilateral OI decrement: critical liveness fix
• AccountKind enum→u8 soundness: eliminates UB risk
• ResolvePermissionless instruction: new capability
• 6 new Kani proof suites: proofs_arithmetic, proofs_audit, proofs_instructions, proofs_invariants, proofs_lazy_ak, proofs_liveness, proofs_safety, proofs_v1131

Our fork additions preserved

• PERC-8460: Premium funding
• PERC-8455: ADL (auto-deleveraging)
• PERC-8456: OI tracking
• PERC-8461: Maintenance fees
• PERC-8462: Ghost account / min deposit fix
• All Kani proofs for our additions

Fix included

RiskEngine::new_with_market(params, 0, 1) in skew_rebate_tests — new() is feature-gated and cargo test does not enable feature = test automatically.

Test plan

• cargo test --lib — 54 tests pass
• cargo test — all suites pass
• cargo test --features test — CI with test feature flag
• cargo kani — Kani proofs (separate CI step)

🤖 Generated with Claude Code

Summary by CodeRabbit

• New Features

  • Large formal verification suite added to validate engine arithmetic, invariants, and liveness properties.
  • Shared test helpers for deterministic scenario-driven tests.

• Bug Fixes

  • Aligned funding and liquidation behaviors with the new ADL K-coefficient model.
  • Fixed a wide-math parameter ordering issue to ensure correct calculations.
  • Strengthened conservation and invariant checks.

• Documentation

  • Updated audit report with expanded verification coverage.

• Tests

  • Refactored tests, updated fuzz regression corpus, and adjusted proof/audit test runner behavior.

[coderabbitai]

Warning

Rate limit exceeded

@dcccrypto has exceeded the limit for the number of commits that can be reviewed per hour. Please wait 7 minutes and 31 seconds before requesting another review.

Your organization is not enrolled in usage-based pricing. Contact your admin to enable usage-based pricing to continue reviews beyond the rate limit, or try again in 7 minutes and 31 seconds.

⌛ How to resolve this issue?

After the wait time has elapsed, a review can be triggered using the @coderabbitai review command as a PR comment. Alternatively, push new commits to this PR.

We recommend that you space out your commits to avoid hitting the rate limit.

🚦 How do rate limits work?

CodeRabbit enforces hourly rate limits for each developer per organization.

Our paid plans have higher rate limits than the trial, open-source and free plans. In all cases, we re-allow further reviews after a brief timeout.

Please see our FAQ for further information.

ℹ️ Review info

⚙️ Run configuration

Configuration used: defaults

Review profile: CHILL

Plan: Pro

Run ID: b5453130-30c7-4ba5-b4f9-02b9d8eafbf4

📥 Commits

Reviewing files that changed from the base of the PR and between 5f1f549 and dd8e946.

📒 Files selected for processing (1)

• src/percolator.rs

📝 Walkthrough

Walkthrough

This PR enables test when fuzz is selected, restructures tests (new shared helpers and many Kani proof modules), refactors src/wide_math.rs (including a parameter reorder), updates the fuzz harness and regression corpus, and adjusts the Kani discovery script and an AMM test file.

Changes

Cohort / File(s)	Summary
Feature Configuration Cargo.toml	Changed fuzz = [] → fuzz = ["test"], so enabling fuzz implicitly activates the test feature and its conditional compilation paths.
Wide Math src/wide_math.rs	Formatting and minor logic tweaks; swapped parameter order for wide_signed_mul_div_floor_from_k_pair (now (abs_basis, k_then, k_now, den)), replaced one overflow helper with checked_mul(...).unwrap_or(...), and simplified a divisibility check.
Test Helpers tests/common/mod.rs	New shared test helper module: re-exports crate symbols, defines model constants, deterministic PnL/AK helpers, and zero_fee_params / default_params.
Tests: Scenario & Fuzz tests/amm_tests.rs, tests/fuzzing.rs, tests/fuzzing.proptest-regressions	Reworked AMM tests to scenario-driven, gated under feature = "test"; fuzz harness simplified to new ADL K-coefficient model, updated invariants, switched to non-atomic engine API variants, and replaced saved Proptest corpus entries.
Kani Proofs (many files) tests/proofs_*.rs (tests/proofs_arithmetic.rs, ..._audit.rs, ..._instructions.rs, ..._invariants.rs, ..._lazy_ak.rs, ..._liveness.rs, ..._v1131.rs)	Added seven large Kani verification modules containing dozens to hundreds of #[kani::proof] harnesses covering arithmetic helpers, audit fixes, instruction semantics, invariants, A/K semantics, liveness, and spec-compliance proofs.
Harness Discovery Script scripts/run_kani_full_audit.sh	Changed discovery to scan tests/proofs_*.rs for #[kani::proof] and adjusted cargo kani invocation to include --tests.
Audit Report scripts/proof-strength-audit-results.md	Updated audit run metadata, increased harness counts and STRONG/UNIT tallies, added new sections and regression notes (doc-only).

Estimated code review effort

🎯 4 (Complex) | ⏱️ ~65 minutes

Possibly related PRs

• feat(PERC-8266): introduce wide_math module (I256/U256) — unblocks ADL migration #64: Changes both modify src/wide_math.rs, including the wide_signed_mul_div_floor_from_k_pair API reorder.
• kani: PERC-8409 — edge-case proofs for settle_warmup, gc_dust, insurance floor, haircut extremes #75: Adds Kani verification proofs addressing overlapping engine behaviors and audit targets introduced here.
• feat(PERC-8270): two-phase keeper — LiquidationPolicy, ADL fields, settle helpers, accrue_market_to, new keeper_crank signature #68: Related test and wide-math helper additions; overlaps in test helper/API usage and wide-math expectations.

Poem

🐇 I hopped through proofs both long and bright,

swapped k‑pairs, stitched tests well into night.
Fuzz now brings test along for the ride,
wide math rearranged with tidy pride.
Cheers — a rabbit’s nibble on formal light.

🚥 Pre-merge checks | ✅ 3

✅ Passed checks (3 passed)

Check name	Status	Explanation
Title check	✅ Passed	The title 'merge: sync upstream aeyakovenko/percolator v12.1 (136 commits)' clearly describes the main change: syncing 136 commits from an upstream repository into the fork.
Description check	✅ Passed	The PR description comprehensively documents the merge: summarizes 136 upstream commits, lists critical safety fixes adopted, specifies fork additions preserved, includes a necessary test fix, and provides a detailed test plan matching the template structure.
Docstring Coverage	✅ Passed	Docstring coverage is 100.00% which is sufficient. The required threshold is 80.00%.

_{✏️ Tip: You can configure your own custom pre-merge checks in the settings.}

✨ Finishing Touches

🧪 Generate unit tests (beta)

• Create PR with unit tests
• Commit unit tests in branch merge/upstream-v12.1

---

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

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

[coderabbitai]

Actionable comments posted: 15

🧹 Nitpick comments (1)

tests/fuzzing.rs (1)

297-299: ExistingNonLp stops meaning “non-LP” after the second LP is added.

The harness only remembers one lp_idx, but Action::AddLp can create multiple LP accounts. After that, resolve_selector(IdxSel::ExistingNonLp) can still pick another LP as the "user" side of ExecuteTrade, which wastes fuzz budget on the wrong path and weakens LP-vs-user coverage.

Also applies to: 334-358, 424-458

🤖 Prompt for AI Agents

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

In `@tests/fuzzing.rs` around lines 297 - 299, The harness incorrectly tracks only
a single lp_idx so IdxSel::ExistingNonLp can later select another LP as the
"user"; change the state to track all LP accounts (e.g., replace lp_idx:
Option<usize> with lp_indices: Vec<usize> or a HashSet of account ids) and
update places that push a new LP (e.g., in the handler for Action::AddLp) to
append/register each new LP, then modify resolve_selector (and any selector
logic referencing IdxSel::ExistingNonLp) to consult that LP set and exclude
those indices when picking an ExistingNonLp user so the selector always returns
a non-LP account.

🤖 Prompt for all review comments with AI agents

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

Inline comments:
In `@scripts/proof-strength-audit-results.md`:
- Around line 31-45: The audit totals are internally inconsistent: reconcile and
correct the summary table counts (entries labeled STRONG, WEAK, UNIT TEST,
VACUOUS) so they sum to the documented total (175) and make the categorical
counts match the detailed sections; update any misclassified proofs referenced
under "Criterion 6: Inductive Strength -- Global Assessment" and "6a. State
Construction Method" so that the counts for fully symbolic/constructed state
(e.g., the 11 proofs and the 147 of 158 numbers) align with the table, and apply
the same corrections to the other affected blocks (notably the blocks around
lines referred to as 891-905 and 1266-1303) so the v11.31 summary and the
detailed per-proof labels (UNIT TEST/WEAK/STRONG/VACUOUS) are consistent across
the document.

In `@scripts/run_kani_full_audit.sh`:
- Around line 9-10: The PROOFS extraction uses grep -A 3 which misses functions
when four attribute lines follow #[kani::proof]; update the extraction so it
skips any number of attribute lines after #[kani::proof] and then captures the
following fn name (e.g., replace the current pipeline that uses grep -A 3 | grep
'^\s*fn ' | sed ... with a single attribute-aware command). Implement this by
scanning files matching tests/proofs_*.rs for lines with '#[kani::proof]' and
then advancing past all subsequent lines that match '^\s*#\[' until you hit a
line matching '^\s*fn ' and extract the function name into PROOFS (use awk,
perl, or grep -P with an appropriate regex to achieve this).

In `@src/wide_math.rs`:
- Around line 1313-1331: The function floor_div_signed_conservative_i128
currently rejects the valid boundary case i128::MIN because it asserts q_final
<= i128::MAX and then negates, which would overflow; change the negative branch
to handle q_final specially: if q_final == (i128::MAX as u128) + 1 then return
i128::MIN directly, otherwise assert q_final <= i128::MAX and return -(q_final
as i128). Apply the same pattern to the corresponding logic in
wide_signed_mul_div_floor_from_k_pair so the i128::MIN result is accepted and
not negated into overflow.

In `@tests/amm_tests.rs`:
- Around line 242-295: The test function test_e2e_negative_funding_rate is not
closed at top level and still uses the old API (deposit(..., 0) and
execute_trade(...)) which makes subsequent #[test]s inner items and fails
compilation; close this test as a top-level function, migrate all old API calls
inside it to the new signatures (use deposit(user, amount, oracle_price, slot)
instead of deposit(..., 0) and replace execute_trade(...) with
execute_trade_not_atomic(...) where used), and ensure fork-specific blocks
(lines referenced 296-495) are pulled back out as separate top-level tests;
specifically update calls to deposit and execute_trade/execute_trade_not_atomic,
and verify keeper_crank_not_atomic/keeper_crank call sites use the correct
slot/oracle_price parameters so the test builds and runs with the new API.

In `@tests/fuzzing.rs`:
- Around line 162-165: The new min_initial_deposit: U128::new(2) causes fuzz
tests fuzz_deposit_increases_balance and fuzz_withdraw_decreases_or_fails to
generate 0/1 amounts and hit rejection paths; update those fuzzers to respect
the minimum initial deposit or adjust the test inputs so deposit >=
min_initial_deposit: change the amount generation in
fuzz_deposit_increases_balance and fuzz_withdraw_decreases_or_fails to produce
values >= min_initial_deposit (or read the value from the same config constant
used to set min_initial_deposit) and ensure any unwraps/ignores of deposit
handle the failure branch if a smaller value is still possible.
- Around line 1218-1228: The test harness_rollback_simulation_test is missing
its closing brace, causing position_strategy (and the following proptest items)
to become nested inside it; add the missing closing '}' to terminate
harness_rollback_simulation_test so position_strategy() and the fork-specific
proptests remain top-level items, and verify surrounding braces for balance
(look for the harness_rollback_simulation_test function/method name and the
position_strategy symbol to locate where the brace should be inserted).

In `@tests/proofs_audit.rs`:
- Around line 768-783: The test only checks keeper_crank_not_atomic(...) is_ok()
but doesn't verify the liquidation applied ExactPartial vs a FullClose fallback;
record the account's pre-crank position (e.g. let eff_before =
engine.effective_pos_q(a as usize)) before calling keeper_crank_not_atomic, then
after the call assert that eff_after == eff_before - q and eff_after != 0 (or
otherwise assert eff_after > 0) to ensure the ExactPartial(q) approved by
LiquidationPolicy::ExactPartial(q) actually reduced the position by q and did
not full-close it; use the existing symbols keeper_crank_not_atomic,
LiquidationPolicy::ExactPartial, q (or q_close), and engine.effective_pos_q to
locate where to add these checks.
- Around line 293-302: Take a snapshot of the account's position before calling
keeper_crank_not_atomic and assert it is equal afterwards instead of only
checking nonzero; specifically call engine.effective_pos_q(a as usize) to save
original_pos, run engine.keeper_crank_not_atomic(...), then
assert_eq!(engine.effective_pos_q(a as usize), original_pos, "position must be
unchanged") to ensure no partial liquidation occurred (you can also snapshot OI
fields if preferred).

In `@tests/proofs_instructions.rs`:
- Around line 1425-1438: Add an assertion after computing released via
engine.released_pos(a as usize) to ensure the warmup release actually occurred
before proceeding; specifically, assert released > 0 || engine.accounts[a as
usize].reserved_pnl == 0 (following the pattern in Property `#50`) so the test
fails if warmup release should have produced profit but did not; then only call
engine.consume_released_pnl(a as usize, x) when that condition holds. This
targets the released variable, engine.released_pos, engine.consume_released_pnl,
and engine.accounts[..].reserved_pnl to prevent silent early returns masking
regressions.
- Around line 1152-1167: The test currently treats an Err from
engine.execute_trade_not_atomic as acceptable, making the proof vacuous and
never checking PnL; change the test so the Err branch fails the test
(panic/assert) rather than silently accept it, and before calling
engine.execute_trade_not_atomic snapshot the account's PNL (e.g., PNL_i or
engine.accounts[a as usize].pnl.get()) alongside fc_before, then in the Ok arm
assert both that fee_credits decreased as before and that the snapshot PNL is
unchanged after the trade; use the existing symbols
engine.execute_trade_not_atomic, fee_credits, PNL_i (or engine.accounts[a as
usize].pnl) and pos_size to locate and implement these checks.

In `@tests/proofs_invariants.rs`:
- Around line 67-105: The harness reimplements the math instead of exercising
the real logic in RiskEngine::check_conservation; update the test
t0_4_conservation_check_handles_overflow to instantiate a RiskEngine (or a
minimal test double) and call RiskEngine::check_conservation(...) with the
kani::any() u128 inputs (c_tot, insurance, vault) and deposit converted to u128,
rather than redoing checked_add locally, then assert/cover based on the
return/error of check_conservation to ensure both normal and overflow branches
in RiskEngine::check_conservation are exercised.
- Around line 606-629: The proof proof_fee_credits_never_i128_min is using i32
(`fc`, `credits`) so it never exercises the full i128 range; either change the
types of `fc` and `credits` to i128 (use kani::any() as i128) so the test can
reach i128::MIN and validate the boundary, or update the function doc/comments
to state it only tests i32-derived flows and leave `fee_debt_u128_checked`
validation to t0_4_fee_debt_no_overflow; refer to the function name
proof_fee_credits_never_i128_min and the symbols `fc`, `credits`, and
`fee_debt_u128_checked` when applying the change.
- Around line 195-200: The test currently uses kani::cover!(result.is_ok(), ...)
which only ensures some execution path succeeds and can hide regressions in
withdraw_not_atomic; change this to enforce correctness by replacing the cover
with an unconditional assert!(result.is_ok()) immediately after calling
engine.withdraw_not_atomic (the variables involved are w, result, and the
withdraw_not_atomic call) so that any unexpected rejections (beyond the
universal dust guard / MIN_INITIAL_DEPOSIT logic) fail the proof instead of
merely being covered.

In `@tests/proofs_liveness.rs`:
- Around line 417-439: Before calling engine.keeper_crank_not_atomic record the
pre-ADL state (e.g., snapshot values of the socialized-deficit/K and per-account
quantity/A that ADL should mutate) so you can assert a real change after the
crank; after the crank assert that either the K-like value or the A-like
quantity differ from the pre-ADL snapshot in addition to
engine.lifetime_liquidations > 0 (use the existing engine reference to read
those fields), and replace the loose kani::cover! check on result2 with a hard
assertion that engine.execute_trade_not_atomic(c, b, ...) returned Ok (i.e.,
assert result2.is_ok()) so the reopen trade must succeed while continuing to
assert engine.oi_eff_long_q == engine.oi_eff_short_q and
engine.check_conservation() afterwards.

In `@tests/proofs_v1131.rs`:
- Around line 23-27: The proof currently doesn't ensure
recompute_r_last_from_final_state actually succeeded (it could return Err and
leave defaults), so first assert the call returns Ok before checking state: call
engine.recompute_r_last_from_final_state(rate as i64) and assert its Result
indicates success (e.g., assert!(engine.recompute_r_last_from_final_state(rate
as i64).is_ok()) or similar), then proceed to assert
engine.funding_rate_bps_per_slot_last == rate as i64; reference the
recompute_r_last_from_final_state function, the rate variable, and
engine.funding_rate_bps_per_slot_last when making the change.

---

Nitpick comments:
In `@tests/fuzzing.rs`:
- Around line 297-299: The harness incorrectly tracks only a single lp_idx so
IdxSel::ExistingNonLp can later select another LP as the "user"; change the
state to track all LP accounts (e.g., replace lp_idx: Option<usize> with
lp_indices: Vec<usize> or a HashSet of account ids) and update places that push
a new LP (e.g., in the handler for Action::AddLp) to append/register each new
LP, then modify resolve_selector (and any selector logic referencing
IdxSel::ExistingNonLp) to consult that LP set and exclude those indices when
picking an ExistingNonLp user so the selector always returns a non-LP account.

🪄 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: defaults

Review profile: CHILL

Plan: Pro

Run ID: 66702f88-2871-4247-88d2-2bf87b1446e5

📥 Commits

Reviewing files that changed from the base of the PR and between b028f8c and d968fe5.

📒 Files selected for processing (19)

• Cargo.toml
• scripts/proof-strength-audit-results.md
• scripts/run_kani_full_audit.sh
• spec.md
• src/percolator.rs
• src/wide_math.rs
• tests/amm_tests.rs
• tests/common/mod.rs
• tests/fuzzing.proptest-regressions
• tests/fuzzing.rs
• tests/proofs_arithmetic.rs
• tests/proofs_audit.rs
• tests/proofs_instructions.rs
• tests/proofs_invariants.rs
• tests/proofs_lazy_ak.rs
• tests/proofs_liveness.rs
• tests/proofs_safety.rs
• tests/proofs_v1131.rs
• tests/unit_tests.rs

[coderabbitai]

⚠️ Potential issue | 🟠 Major

The audit report is internally inconsistent.

The updated totals no longer agree with each other: the top table says 11 + 162 + 3, which is 176 rather than 175; later sections still talk about 158/157/146 proofs; and the v11.31 summary reclassifies proofs that the detailed sections still label as UNIT TEST or WEAK. As written, this file is not a reliable source of record for audit coverage.

Also applies to: 891-905, 1266-1303

🤖 Prompt for AI Agents

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

In `@scripts/proof-strength-audit-results.md` around lines 31 - 45, The audit
totals are internally inconsistent: reconcile and correct the summary table
counts (entries labeled STRONG, WEAK, UNIT TEST, VACUOUS) so they sum to the
documented total (175) and make the categorical counts match the detailed
sections; update any misclassified proofs referenced under "Criterion 6:
Inductive Strength -- Global Assessment" and "6a. State Construction Method" so
that the counts for fully symbolic/constructed state (e.g., the 11 proofs and
the 147 of 158 numbers) align with the table, and apply the same corrections to
the other affected blocks (notably the blocks around lines referred to as
891-905 and 1266-1303) so the v11.31 summary and the detailed per-proof labels
(UNIT TEST/WEAK/STRONG/VACUOUS) are consistent across the document.

[coderabbitai]

⚠️ Potential issue | 🔴 Critical

🧩 Analysis chain

🏁 Script executed:

#!/bin/bash
set -euo pipefail

current=$(
  grep -rh '#\[kani::proof\]' tests/proofs_*.rs -A 3 \
    | grep '^[[:space:]]*fn ' \
    | sed -E 's/.*fn[[:space:]]+([A-Za-z0-9_]+).*/\1/' \
    | sort -u
)

expected=$(
python - <<'PY'
import pathlib, re
proofs = set()
for path in pathlib.Path("tests").glob("proofs_*.rs"):
    lines = path.read_text().splitlines()
    i = 0
    while i < len(lines):
        if "#[kani::proof]" in lines[i]:
            j = i + 1
            while j < len(lines) and re.match(r'^\s*#\[', lines[j]):
                j += 1
            if j < len(lines):
                m = re.match(r'^\s*fn\s+([A-Za-z0-9_]+)\s*\(', lines[j])
                if m:
                    proofs.add(m.group(1))
            i = j
        else:
            i += 1
for name in sorted(proofs):
    print(name)
PY
)

echo "Harnesses missed by current discovery:"
comm -13 <(printf '%s\n' "$current") <(printf '%s\n' "$expected")

Repository: dcccrypto/percolator

Length of output: 163

---

🏁 Script executed:

# Check if the script file exists and examine lines 9-10
if [ -f scripts/run_kani_full_audit.sh ]; then
  echo "=== File exists ===" 
  wc -l scripts/run_kani_full_audit.sh
  echo "=== Lines 1-15 ==="
  head -15 scripts/run_kani_full_audit.sh | cat -n
else
  echo "File does not exist"
fi

# Check what proof files exist
echo "=== Proof files in tests/ ==="
fd 'proofs_.*\.rs$' tests/ 2>/dev/null || find tests -name 'proofs_*.rs' 2>/dev/null || echo "No proofs files found"

Repository: dcccrypto/percolator

Length of output: 945

---

🏁 Script executed:

# Sample harnesses from proofs_invariants.rs and proofs_audit.rs
echo "=== proofs_invariants.rs - first 100 lines ==="
head -100 tests/proofs_invariants.rs | cat -n

echo ""
echo "=== Check for #[kani::proof] patterns in proofs_invariants.rs ==="
grep -n '#\[kani' tests/proofs_invariants.rs | head -30

Repository: dcccrypto/percolator

Length of output: 5050

---

🏁 Script executed:

echo "=== Check for should_panic in proofs_audit.rs ==="
grep -n '#\[kani' tests/proofs_audit.rs | head -30

echo ""
echo "=== Sample harness with should_panic ==="
grep -B2 -A6 'should_panic' tests/proofs_audit.rs | head -30

Repository: dcccrypto/percolator

Length of output: 1594

---

🏁 Script executed:

echo "=== Find exact line numbers for should_panic harness ==="
grep -n "proof_config_rejects_oversized_max_accounts" tests/proofs_audit.rs

echo ""
echo "=== Show context around that harness ==="
sed -n '330,340p' tests/proofs_audit.rs | cat -n

echo ""
echo "=== Run the actual grep discovery command ==="
PROOFS=$(grep -rh '#\[kani::proof\]' tests/proofs_*.rs -A 3 | grep '^\s*fn ' | sed 's/.*fn \([a-z_0-9]*\).*/\1/' | sort -u)
echo "Discovered harnesses (showing only config_rejects ones):"
echo "$PROOFS" | grep "config_rejects" || echo "(none found with config_rejects)"

echo ""
echo "=== List all proof_* and config_* functions ==="
grep -h '^\s*fn ' tests/proofs_*.rs | sed 's/.*fn \([a-z_0-9]*\).*/\1/' | grep -E "(proof_|config_)" | sort

Repository: dcccrypto/percolator

Length of output: 7551

---

Harness discovery silently skips #[kani::should_panic] proofs.

The grep -A 3 pattern captures the matched line plus 3 lines after it (4 lines total). Harnesses with four attributes—#[kani::proof], #[kani::unwind], #[kani::solver], and #[kani::should_panic]—place the fn declaration at position +4, which is outside the capture range. This causes all config validation proofs (e.g., proof_config_rejects_oversized_max_accounts, proof_config_rejects_invalid_bps) to be silently dropped from the audit run.

Use an attribute-aware extraction that skips all #[…] lines following #[kani::proof]:

Suggested fix

- PROOFS=$(grep -rh '#\[kani::proof\]' tests/proofs_*.rs -A 3 | grep '^\s*fn ' | sed 's/.*fn \([a-z_0-9]*\).*/\1/' | sort -u)
+ PROOFS=$(
+   awk '
+     /#\[kani::proof\]/ { in_proof = 1; next }
+     in_proof && /^[[:space:]]*#\[/ { next }
+     in_proof && match($0, /^[[:space:]]*fn[[:space:]]+([A-Za-z0-9_]+)/, m) {
+       print m[1]
+       in_proof = 0
+     }
+   ' tests/proofs_*.rs | sort -u
+ )

📝 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

	# Collect all proof harness names from all proof files
	PROOFS=$(grep -rh '#\[kani::proof\]' tests/proofs_*.rs -A 3 | grep '^\s*fn ' | sed 's/.*fn \([a-z_0-9]*\).*/\1/' | sort -u)
	# Collect all proof harness names from all proof files
	PROOFS=$(
	awk '
	/#\[kani::proof\]/ { in_proof = 1; next }
	in_proof && /^[[:space:]]*#\[/ { next }
	in_proof && match($0, /^[[:space:]]*fn[[:space:]]+([A-Za-z0-9_]+)/, m) {
	print m[1]
	in_proof = 0
	}
	' tests/proofs_*.rs | sort -u
	)

🤖 Prompt for AI Agents

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

In `@scripts/run_kani_full_audit.sh` around lines 9 - 10, The PROOFS extraction
uses grep -A 3 which misses functions when four attribute lines follow
#[kani::proof]; update the extraction so it skips any number of attribute lines
after #[kani::proof] and then captures the following fn name (e.g., replace the
current pipeline that uses grep -A 3 | grep '^\s*fn ' | sed ... with a single
attribute-aware command). Implement this by scanning files matching
tests/proofs_*.rs for lines with '#[kani::proof]' and then advancing past all
subsequent lines that match '^\s*#\[' until you hit a line matching '^\s*fn '
and extract the function name into PROOFS (use awk, perl, or grep -P with an
appropriate regex to achieve this).

[coderabbitai]

⚠️ Potential issue | 🟠 Major

Handle the exact i128::MIN result instead of rejecting it.

floor_div_signed_conservative_i128(i128::MIN, 1) and wide_signed_mul_div_floor_from_k_pair(1, 0, i128::MIN, 1) should both return i128::MIN. The current <= i128::MAX guard rejects that valid boundary, and the following negation would overflow if it were reached.

Suggested fix

 pub fn floor_div_signed_conservative_i128(n: i128, d: u128) -> i128 {
@@
-        let q_final = if r != 0 { q + 1 } else { q };
-        assert!(q_final <= i128::MAX as u128,
-            "floor_div_signed_conservative_i128: result out of range");
-        -(q_final as i128)
+        let q_final = if r != 0 { q + 1 } else { q };
+        if q_final == (1u128 << 127) {
+            i128::MIN
+        } else {
+            assert!(q_final <= i128::MAX as u128,
+                "floor_div_signed_conservative_i128: result out of range");
+            -(q_final as i128)
+        }
     }
 }
@@
     if d.is_negative() {
@@
-        let mag_u128 = mag.try_into_u128().expect("mag exceeds u128");
-        assert!(mag_u128 <= i128::MAX as u128, "wide_signed_mul_div_floor_from_k_pair: mag > i128::MAX");
-        -(mag_u128 as i128)
+        let mag_u128 = mag.try_into_u128().expect("mag exceeds u128");
+        if mag_u128 == (1u128 << 127) {
+            i128::MIN
+        } else {
+            assert!(mag_u128 <= i128::MAX as u128, "wide_signed_mul_div_floor_from_k_pair: mag > i128::MAX");
+            -(mag_u128 as i128)
+        }
     } else {

Also applies to: 1498-1526

🤖 Prompt for AI Agents

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

In `@src/wide_math.rs` around lines 1313 - 1331, The function
floor_div_signed_conservative_i128 currently rejects the valid boundary case
i128::MIN because it asserts q_final <= i128::MAX and then negates, which would
overflow; change the negative branch to handle q_final specially: if q_final ==
(i128::MAX as u128) + 1 then return i128::MIN directly, otherwise assert q_final
<= i128::MAX and return -(q_final as i128). Apply the same pattern to the
corresponding logic in wide_signed_mul_div_floor_from_k_pair so the i128::MIN
result is accepted and not negated into overflow.

[coderabbitai]

⚠️ Potential issue | 🔴 Critical

Move this section back to top level and finish migrating it to the new test API.

test_e2e_negative_funding_rate never closes before the fork-specific section, so the last two #[test] functions become inner items instead of top-level integration tests. If you pull them back out, they still use the old deposit(..., 0) / execute_trade(&MATCHER, ...) flow while the rest of the file has already moved to deposit(..., oracle_price, slot) and execute_trade_not_atomic(...), so the block still won't build or run as intended.

Also applies to: 296-495

🤖 Prompt for AI Agents

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

In `@tests/amm_tests.rs` around lines 242 - 295, The test function
test_e2e_negative_funding_rate is not closed at top level and still uses the old
API (deposit(..., 0) and execute_trade(...)) which makes subsequent #[test]s
inner items and fails compilation; close this test as a top-level function,
migrate all old API calls inside it to the new signatures (use deposit(user,
amount, oracle_price, slot) instead of deposit(..., 0) and replace
execute_trade(...) with execute_trade_not_atomic(...) where used), and ensure
fork-specific blocks (lines referenced 296-495) are pulled back out as separate
top-level tests; specifically update calls to deposit and
execute_trade/execute_trade_not_atomic, and verify
keeper_crank_not_atomic/keeper_crank call sites use the correct
slot/oracle_price parameters so the test builds and runs with the new API.

[coderabbitai]

⚠️ Potential issue | 🟠 Major

This new initial-deposit floor breaks the deposit properties below.

fuzz_deposit_increases_balance and fuzz_withdraw_decreases_or_fails still generate 0/1 amounts and then ignore or unwrap deposit. With min_initial_deposit = 2, those tests now assert on valid rejection paths instead of successful deposits.

🤖 Prompt for AI Agents

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

In `@tests/fuzzing.rs` around lines 162 - 165, The new min_initial_deposit:
U128::new(2) causes fuzz tests fuzz_deposit_increases_balance and
fuzz_withdraw_decreases_or_fails to generate 0/1 amounts and hit rejection
paths; update those fuzzers to respect the minimum initial deposit or adjust the
test inputs so deposit >= min_initial_deposit: change the amount generation in
fuzz_deposit_increases_balance and fuzz_withdraw_decreases_or_fails to produce
values >= min_initial_deposit (or read the value from the same config constant
used to set min_initial_deposit) and ensure any unwraps/ignores of deposit
handle the failure branch if a smaller value is still possible.

[coderabbitai]

⚠️ Potential issue | 🟠 Major

🧩 Analysis chain

🏁 Script executed:

# First, confirm the test file exists and locate RiskEngine
git ls-files | grep -E "(proofs_invariants|risk)" | head -20

Repository: dcccrypto/percolator

Length of output: 90

---

🏁 Script executed:

# Search for RiskEngine definition
rg "struct RiskEngine" -A 10

Repository: dcccrypto/percolator

Length of output: 969

---

🏁 Script executed:

# Search for check_conservation method
rg "fn check_conservation" -B 2 -A 15

Repository: dcccrypto/percolator

Length of output: 2271

---

🏁 Script executed:

# Check if the test file calls check_conservation or RiskEngine methods
rg "check_conservation" tests/proofs_invariants.rs

Repository: dcccrypto/percolator

Length of output: 739

---

🏁 Script executed:

# Read the full test function to understand its structure
sed -n '67,105p' tests/proofs_invariants.rs | cat -n

Repository: dcccrypto/percolator

Length of output: 1874

---

🏁 Script executed:

# Check if any RiskEngine is constructed in the entire test file
rg "RiskEngine" tests/proofs_invariants.rs

Repository: dcccrypto/percolator

Length of output: 1431

---

🏁 Script executed:

# Look at context around the test to understand intent
sed -n '60,110p' tests/proofs_invariants.rs | cat -n

Repository: dcccrypto/percolator

Length of output: 2436

---

This harness does not call RiskEngine::check_conservation().

The test reimplements the conservation arithmetic locally and only covers the overflow branch. It never instantiates RiskEngine or calls the production method, so regressions in RiskEngine::check_conservation() would go undetected.

🤖 Prompt for AI Agents

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

In `@tests/proofs_invariants.rs` around lines 67 - 105, The harness reimplements
the math instead of exercising the real logic in RiskEngine::check_conservation;
update the test t0_4_conservation_check_handles_overflow to instantiate a
RiskEngine (or a minimal test double) and call
RiskEngine::check_conservation(...) with the kani::any() u128 inputs (c_tot,
insurance, vault) and deposit converted to u128, rather than redoing checked_add
locally, then assert/cover based on the return/error of check_conservation to
ensure both normal and overflow branches in RiskEngine::check_conservation are
exercised.

[coderabbitai]

⚠️ Potential issue | 🟠 Major

🧩 Analysis chain

🏁 Script executed:

find . -name "proofs_invariants.rs" -type f

Repository: dcccrypto/percolator

Length of output: 92

---

🏁 Script executed:

git ls-files | grep -E "(proofs|test)" | head -20

Repository: dcccrypto/percolator

Length of output: 387

---

🏁 Script executed:

ls -la

Repository: dcccrypto/percolator

Length of output: 1100

---

🏁 Script executed:

cat -n tests/proofs_invariants.rs | sed -n '190,210p'

Repository: dcccrypto/percolator

Length of output: 1001

---

🏁 Script executed:

wc -l tests/proofs_invariants.rs

Repository: dcccrypto/percolator

Length of output: 94

---

🏁 Script executed:

cat -n tests/proofs_invariants.rs | sed -n '180,220p'

Repository: dcccrypto/percolator

Length of output: 1806

---

🏁 Script executed:

rg "withdraw_not_atomic" --type rust -B 3 -A 15 | head -60

Repository: dcccrypto/percolator

Length of output: 3711

---

🏁 Script executed:

rg "dust" --type rust -B 2 -A 5

Repository: dcccrypto/percolator

Length of output: 50377

---

🏁 Script executed:

fd -e rs | xargs rg "withdraw_not_atomic" -l

Repository: dcccrypto/percolator

Length of output: 238

---

🌐 Web query:

kani verification framework cover! macro behavior vs assert

💡 Result:

In the Kani Rust Verifier framework, the kani::cover!(condition) macro checks if there exists at least one execution path from the proof harness where the specified condition holds true at that point in the code. It is used for coverage guidance, reachability analysis, and sanity checking harnesses. Key behaviors and results for kani::cover!: - SATISFIED: Found an execution satisfying the condition. - UNSATISFABLE: Proved no execution satisfies it (condition unreachable). - UNREACHABLE: The cover statement itself is unreachable. - UNDETERMINED: Could not decide. In contrast, assert!(condition) verifies that the condition holds on ALL execution paths (its negation should not be satisfiable). Kani checks reachability for assert macros among other properties. assert! failure means a bug (property violated on some path), while cover! UNSATISFIED/UNREACHABLE may indicate incomplete coverage or dead code. Example: #[kani::proof] fn example { let x: u16 = kani::any; if x > 8 { kani::cover!(x.wrapping_mul(x).wrapping_mul(x) == 8); // Checks if possible assert!(x > 0); // Checks must always hold } } They are inverses: cover!(p) succeeds if exists path with p; assert!(p) succeeds if forall paths p.

Citations:

• 1: https://model-checking.github.io/kani-verifier-blog/2023/01/30/reachability-and-sanity-checking-with-kani-cover.html
• 2: https://model-checking.github.io/kani/verification-results.html

---

🏁 Script executed:

cat -n tests/proofs_invariants.rs | sed -n '160,225p'

Repository: dcccrypto/percolator

Length of output: 2871

---

🏁 Script executed:

rg "withdraw_not_atomic" tests/ -A 3 | head -40

Repository: dcccrypto/percolator

Length of output: 2401

---

Using cover! weakens the proof and allows withdrawal regressions to hide.

kani::cover!(result.is_ok(), ...) only checks that at least one execution path succeeds, not that valid withdrawals always succeed. The constraint w >= 1 && w <= dep doesn't guarantee success—the universal dust guard (step 5 in withdraw_not_atomic) rejects withdrawals leaving 0 < capital < MIN_INITIAL_DEPOSIT. If the withdrawal logic regresses to reject more cases beyond dust violations, this proof stays green because cover! still finds a passing path. Use assert!(result.is_ok()) to catch such regressions.

🤖 Prompt for AI Agents

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

In `@tests/proofs_invariants.rs` around lines 195 - 200, The test currently uses
kani::cover!(result.is_ok(), ...) which only ensures some execution path
succeeds and can hide regressions in withdraw_not_atomic; change this to enforce
correctness by replacing the cover with an unconditional assert!(result.is_ok())
immediately after calling engine.withdraw_not_atomic (the variables involved are
w, result, and the withdraw_not_atomic call) so that any unexpected rejections
(beyond the universal dust guard / MIN_INITIAL_DEPOSIT logic) fail the proof
instead of merely being covered.

[coderabbitai]

⚠️ Potential issue | 🟠 Major

🧩 Analysis chain

🏁 Script executed:

# First, let's examine the test file at the specified lines
cat -n tests/proofs_invariants.rs | sed -n '600,640p'

Repository: dcccrypto/percolator

Length of output: 1453

---

🏁 Script executed:

# Now let's find and examine the fee_debt_u128_checked function
find . -name "*.rs" -type f | xargs rg -l "fee_debt_u128_checked"

Repository: dcccrypto/percolator

Length of output: 207

---

🏁 Script executed:

# Let's look at the implementation of fee_debt_u128_checked
rg -A 10 "fn fee_debt_u128_checked" --type rust

Repository: dcccrypto/percolator

Length of output: 597

---

🏁 Script executed:

# Search for settle_maintenance_fee and related code
rg -A 20 "settle_maintenance_fee" --type rust src/

Repository: dcccrypto/percolator

Length of output: 24277

---

🏁 Script executed:

# Check where checked_sub is used with full i128 values
rg "checked_sub" --type rust -B 3 -A 3 src/

Repository: dcccrypto/percolator

Length of output: 26722

---

🏁 Script executed:

# Look for other proofs testing fee_debt_u128_checked
rg -B 5 -A 15 "fee_debt_u128_checked" tests/ --type rust

Repository: dcccrypto/percolator

Length of output: 7687

---

The i128::MIN proof uses i32 values, which cannot represent the full i128 range.

Both fc and credits are i32 type, so when cast to i128 they range only from -2^31 to 2^31−1, never reaching −2^127 (i128::MIN). This means proof_fee_credits_never_i128_min() does not actually verify the boundary case its name and doc comment (lines 601–602) claim to test.

However, note that t0_4_fee_debt_no_overflow() in tests/proofs_arithmetic.rs already covers the full i128 range with kani::any(), so the function's safety is validated elsewhere. If this proof's intent is narrower (testing only i32-derived flows), its documentation should be clarified accordingly.

🤖 Prompt for AI Agents

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

In `@tests/proofs_invariants.rs` around lines 606 - 629, The proof
proof_fee_credits_never_i128_min is using i32 (`fc`, `credits`) so it never
exercises the full i128 range; either change the types of `fc` and `credits` to
i128 (use kani::any() as i128) so the test can reach i128::MIN and validate the
boundary, or update the function doc/comments to state it only tests i32-derived
flows and leave `fee_debt_u128_checked` validation to t0_4_fee_debt_no_overflow;
refer to the function name proof_fee_credits_never_i128_min and the symbols
`fc`, `credits`, and `fee_debt_u128_checked` when applying the change.

[coderabbitai]

⚠️ Potential issue | 🟠 Major

🧩 Analysis chain

🏁 Script executed:

# First, let's find and read the test file
git ls-files tests/ | grep liveness

Repository: dcccrypto/percolator

Length of output: 88

---

🏁 Script executed:

# Read the test function with context
cat -n tests/proofs_liveness.rs | sed -n '395,450p'

Repository: dcccrypto/percolator

Length of output: 2690

---

🏁 Script executed:

# Also check the complete structure around the ADL pipeline test
cat -n tests/proofs_liveness.rs | sed -n '380,450p'

Repository: dcccrypto/percolator

Length of output: 3479

---

Step 4 assertion does not verify ADL state mutations; Step 5 allows reopen to fail without test failure.

The comment at line 421–422 claims to verify that "K should have changed (deficit socialized to b) or A should have changed (quantity reduction)", but line 424 only asserts liqs > 0. This checks that a liquidation occurred, not that ADL actually mutated any state. A regression that executes liquidation without ADL state changes would still pass.

Additionally, line 431's trade attempt has no hard assertion—only a kani::cover! at line 438. Lines 435–436 check OI balance and conservation, which hold regardless of whether the reopen succeeds. If the trade is rejected, the test still passes, contradicting the docstring's promise of an "end-to-end ADL pipeline" with a reopen.

To properly test the full pipeline, add explicit assertions verifying that ADL state (K or quantities) changed, and require the reopen trade to succeed.

🤖 Prompt for AI Agents

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

In `@tests/proofs_liveness.rs` around lines 417 - 439, Before calling
engine.keeper_crank_not_atomic record the pre-ADL state (e.g., snapshot values
of the socialized-deficit/K and per-account quantity/A that ADL should mutate)
so you can assert a real change after the crank; after the crank assert that
either the K-like value or the A-like quantity differ from the pre-ADL snapshot
in addition to engine.lifetime_liquidations > 0 (use the existing engine
reference to read those fields), and replace the loose kani::cover! check on
result2 with a hard assertion that engine.execute_trade_not_atomic(c, b, ...)
returned Ok (i.e., assert result2.is_ok()) so the reopen trade must succeed
while continuing to assert engine.oi_eff_long_q == engine.oi_eff_short_q and
engine.check_conservation() afterwards.

[coderabbitai]

⚠️ Potential issue | 🟡 Minor

Assert the success path explicitly in this proof.

Right now this can still pass for rate == 0 if recompute_r_last_from_final_state regresses to Err and leaves the default value untouched. The property is stronger if it first proves the in-range call succeeds.

Suggested fix

-    engine.recompute_r_last_from_final_state(rate as i64);
+    let result = engine.recompute_r_last_from_final_state(rate as i64);
+    assert!(result.is_ok(), "in-range rate must be accepted");
     assert!(engine.funding_rate_bps_per_slot_last == rate as i64,
         "r_last must equal the supplied rate");

📝 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

	let rate: i16 = kani::any();
	kani::assume(rate.unsigned_abs() <= MAX_ABS_FUNDING_BPS_PER_SLOT as u16);
	engine.recompute_r_last_from_final_state(rate as i64);
	assert!(engine.funding_rate_bps_per_slot_last == rate as i64,
	let rate: i16 = kani::any();
	kani::assume(rate.unsigned_abs() <= MAX_ABS_FUNDING_BPS_PER_SLOT as u16);
	let result = engine.recompute_r_last_from_final_state(rate as i64);
	assert!(result.is_ok(), "in-range rate must be accepted");
	assert!(engine.funding_rate_bps_per_slot_last == rate as i64,

🤖 Prompt for AI Agents

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

In `@tests/proofs_v1131.rs` around lines 23 - 27, The proof currently doesn't
ensure recompute_r_last_from_final_state actually succeeded (it could return Err
and leave defaults), so first assert the call returns Ok before checking state:
call engine.recompute_r_last_from_final_state(rate as i64) and assert its Result
indicates success (e.g., assert!(engine.recompute_r_last_from_final_state(rate
as i64).is_ok()) or similar), then proceed to assert
engine.funding_rate_bps_per_slot_last == rate as i64; reference the
recompute_r_last_from_final_state function, the rate variable, and
engine.funding_rate_bps_per_slot_last when making the change.