Wave 11a-i: engine B-tracking schema (KL-FORK-ENGINE-B-TRACKING-1 PARTIALLY REVOKED)

[dcccrypto]

Summary

Schema-only foundation for the B-index bankruptcy-residual subsystem (spec §1.2 / §2.1 / §2.2, v12.20.6). Path A2: adds fields + accessors + defense-in-depth invariant, defers all writers to Wave 11a-ii.

Schema additions

• 2 new constants: SOCIAL_LOSS_DEN = 10^21, PUBLIC_B_CHUNK_ATOMS = MAX_VAULT_TVL
• Account +4 fields: loss_weight, b_snap, b_rem (all u128), b_epoch_snap (u64)
• RiskEngine +17 fields: 14 × u128 (b_long_num, b_short_num, b_epoch_start_, loss_weight_sum_, social_loss_remainder_, social_loss_dust_) + 3 × U128 (explicit_unallocated_loss_long/short/protocol) + 1 × u8 (saturated flag)
• 10 get/set accessors (toly:2859-2926)
• validate_b_tracking_shape invariant + assert_public_postconditions integration
• 2 new Kani harnesses

Schema growth: +280 bytes RiskEngine + 56 bytes Account.

Migration

NFT vendored bytes + wrapper SLAB_LEN follow in Wave 11b and 11c. Path B per FULL_SYNC_PLAN.md (force-resolve + rebuild J51cB2 during deployment prep, no on-chain migration instruction).

Verification

• cargo build --release --features test clean
• cargo test --features test --release: 335 / 0 / 0
• Engine Kani proof count: 313 → 315
• verify-engine-preservation.sh silent
• verify-engine-deferred-absent.sh silent
• KEEP_LIST.md: KL-FORK-ENGINE-B-TRACKING-1 marked PARTIALLY REVOKED

Test plan

• cargo build --release
• cargo test --features test --release
• verify scripts both silent
• CI green
• Admin-merge

Follow-ups (Wave 11 continuation)

• Wave 11a-ii: helpers (plan/book_bankruptcy_residual_chunk_to_side, b_target_for_account, account_has_unsettled_b, trigger_bankruptcy_hmax_lock, record_uninsured_protocol_loss, add_explicit_unallocated_loss_side) + bankrupt-close state-machine setters + account_has_unsettled_live_effects 5-predicate form + tests/proofs_b_index.rs port
• Wave 11b: NFT vendored-bytes mirror update
• Wave 11c: wrapper SLAB_LEN + test-helper BPF offsets bump (Wave 7b pattern)

🤖 Generated with Claude Code

Summary by CodeRabbit

• Chores

  • Enhanced internal risk-engine validation framework with new safeguards to detect corrupted state conditions.

• Tests

  • Added invariant proofs to verify baseline integrity conditions and rejection of invalid states in risk tracking systems.

[coderabbitai]

📝 Walkthrough

Walkthrough

This PR extends the persisted risk-engine schema with Wave 11a bankruptcy-residual (B-tracking) accounting by adding constants, struct fields to Account and RiskEngine, zero-initialization, internal helpers, and a defensive validator that rejects corrupted state at the public boundary. Kani proofs verify genesis initialization and overflow rejection.

Changes

Wave 11a B-Tracking Subsystem

Layer / File(s)	Summary
B-Tracking Schema Constants src/percolator.rs	Introduces SOCIAL_LOSS_DEN and derives PUBLIC_B_CHUNK_ATOMS budget constant.
Account Struct B-Tracking Fields src/percolator.rs	Extends Account with loss_weight, b_snap, b_rem, and b_epoch_snap for per-account loss tracking.
RiskEngine Struct B-Tracking Fields src/percolator.rs	Extends RiskEngine with B targets, epoch snapshots, social-loss remainder/dust accumulators, explicit unallocated loss buckets, and saturation flag.
Zero-Initialization Across Constructors src/percolator.rs	Initializes all new B-tracking fields to zero in empty_account(), new_with_market(), and init_in_place().
Invariant Validation & Internal Helpers src/percolator.rs	Adds getter/setter accessors and validate_b_tracking_shape() to enforce boundedness of accumulators and saturation state.
Public Postcondition Enforcement src/percolator.rs	Wires validate_b_tracking_shape() into assert_public_postconditions_fast().
B-Tracking Invariant Proofs tests/proofs_invariants.rs	Adds genesis zero-initialization proof and overflow rejection proof verifying state validation.

Estimated code review effort

🎯 3 (Moderate) | ⏱️ ~25 minutes

Possibly related PRs

• dcccrypto/percolator#60: Changes to in-memory layout of Percolator structs (RiskEngine/Account) with corresponding test offset updates relevant to this PR's struct extensions.

Poem

In Wave Eleven, the rabbit prepares,
New fields for loss-weight, B-tracking cares,
Zero-init paths, validation so tight,
Boundaries guarded from wrong to right! 🐰✨

🚥 Pre-merge checks | ✅ 5

✅ Passed checks (5 passed)

Check name	Status	Explanation
Description Check	✅ Passed	Check skipped - CodeRabbit’s high-level summary is enabled.
Title check	✅ Passed	The title accurately describes the main change: introducing the B-tracking schema foundation for Wave 11a-i, with a note about partial revocation status.
Docstring Coverage	✅ Passed	Docstring coverage is 100.00% which is sufficient. The required threshold is 80.00%.
Linked Issues check	✅ Passed	Check skipped because no linked issues were found for this pull request.
Out of Scope Changes check	✅ Passed	Check skipped because no linked issues were found for this pull request.

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

✨ Finishing Touches

📝 Generate docstrings

• Create stacked PR
• Commit on current branch

🧪 Generate unit tests (beta)

• Create PR with unit tests
• Commit unit tests in branch feat/eng-b-tracking-wave11a

---

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: 1

🧹 Nitpick comments (2)

tests/proofs_invariants.rs (1)

1167-1178: ⚡ Quick win

Broaden the genesis proof to pin all newly added B-tracking fields.

This harness currently asserts zero-init for a subset of the Wave 11a schema. Since assert_public_postconditions() is mostly shape/bounds-oriented, add explicit assert_eq!(..., 0) checks for the remaining newly-added B-tracking fields (notably the epoch-start and explicit-unallocated-loss fields) so zero-init regressions are caught directly.

🤖 Prompt for AI Agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@tests/proofs_invariants.rs` around lines 1167 - 1178, Add explicit zero-init
assertions for the newly added B-tracking fields that aren't covered by
assert_public_postconditions(): add
assert_eq!(engine.social_loss_epoch_start_long_num, 0);
assert_eq!(engine.social_loss_epoch_start_short_num, 0);
assert_eq!(engine.explicit_unallocated_loss_long_num, 0); and
assert_eq!(engine.explicit_unallocated_loss_short_num, 0) (in the same block
after the existing asserts like engine.b_long_num and
engine.explicit_unallocated_loss_saturated) so epoch-start and
explicit-unallocated-loss regressions are caught directly.

src/percolator.rs (1)

3157-3191: ⚡ Quick win

validate_b_tracking_shape should be complemented with per-account B checks (debug scan path).

The new fast validator only covers engine aggregates. Per-account corruption (loss_weight, b_rem, and free-slot nonzero B fields) is still invisible in validate_public_account_postconditions, which is already doing the linear scan in test/audit builds.

💡 Suggested patch

diff --git a/src/percolator.rs b/src/percolator.rs
@@ fn validate_public_account_postconditions(&self) -> Result<()> {
             if !used {
                 if account.kind != Account::KIND_USER
                     || !account.capital.is_zero()
@@
                     || account.pending_horizon != 0
                     || account.pending_created_slot != 0
+                    || account.loss_weight != 0
+                    || account.b_snap != 0
+                    || account.b_rem != 0
+                    || account.b_epoch_snap != 0
                     || !Self::is_zero_bytes_32(&account.matcher_program)
                     || !Self::is_zero_bytes_32(&account.matcher_context)
                     || !Self::is_zero_bytes_32(&account.owner)
                 {
                     return Err(RiskError::CorruptState);
                 }
                 continue;
             }
@@
             self.validate_fee_credits_shape(idx)?;
             self.validate_reserve_shape(idx)?;
+            if account.loss_weight > SOCIAL_LOSS_DEN || account.b_rem >= SOCIAL_LOSS_DEN {
+                return Err(RiskError::CorruptState);
+            }

Also applies to: 4710-4714

🤖 Prompt for AI Agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@src/percolator.rs` around lines 3157 - 3191, The validate_b_tracking_shape
currently only checks engine-level aggregates; add a debug-only per-account scan
(used in test/audit builds) that iterates accounts and verifies each account's
loss_weight, b_rem, and B-related free-slot fields are consistent (e.g.,
per-account loss_weight within expected range, b_rem < SOCIAL_LOSS_DEN, and any
“free slot” B fields are zero when they must be); implement this as either an
extension to validate_b_tracking_shape under #[cfg(test)]/audit flag or by
calling the existing validate_public_account_postconditions logic from
validate_b_tracking_shape for debug builds, and ensure you reference and
validate the concrete fields named loss_weight, b_rem, social-loss-related B
fields and any explicit free-slot/B placeholders so per-account corruption is
detected during the debug scan.

🤖 Prompt for all review comments with AI agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

Inline comments:
In `@src/percolator.rs`:
- Around line 467-483: The new Account fields loss_weight, b_snap, b_rem and
b_epoch_snap must be explicitly zeroed wherever an account is
canonicalized/reset in-place; update each account-reset/canonicalization branch
that currently clears other per-account fields to also set loss_weight = 0,
b_snap = 0, b_rem = 0 and b_epoch_snap = 0 so the schema-only/all-zero invariant
holds (i.e., add these zero assignments alongside the existing resets in the
in-place account reset paths that touch other per-account state).

---

Nitpick comments:
In `@src/percolator.rs`:
- Around line 3157-3191: The validate_b_tracking_shape currently only checks
engine-level aggregates; add a debug-only per-account scan (used in test/audit
builds) that iterates accounts and verifies each account's loss_weight, b_rem,
and B-related free-slot fields are consistent (e.g., per-account loss_weight
within expected range, b_rem < SOCIAL_LOSS_DEN, and any “free slot” B fields are
zero when they must be); implement this as either an extension to
validate_b_tracking_shape under #[cfg(test)]/audit flag or by calling the
existing validate_public_account_postconditions logic from
validate_b_tracking_shape for debug builds, and ensure you reference and
validate the concrete fields named loss_weight, b_rem, social-loss-related B
fields and any explicit free-slot/B placeholders so per-account corruption is
detected during the debug scan.

In `@tests/proofs_invariants.rs`:
- Around line 1167-1178: Add explicit zero-init assertions for the newly added
B-tracking fields that aren't covered by assert_public_postconditions(): add
assert_eq!(engine.social_loss_epoch_start_long_num, 0);
assert_eq!(engine.social_loss_epoch_start_short_num, 0);
assert_eq!(engine.explicit_unallocated_loss_long_num, 0); and
assert_eq!(engine.explicit_unallocated_loss_short_num, 0) (in the same block
after the existing asserts like engine.b_long_num and
engine.explicit_unallocated_loss_saturated) so epoch-start and
explicit-unallocated-loss regressions are caught directly.

🪄 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: 0cf570e7-f284-4f2e-8352-187cd0af5edf

📥 Commits

Reviewing files that changed from the base of the PR and between 615a5f3 and eafa367.

📒 Files selected for processing (2)

• src/percolator.rs
• tests/proofs_invariants.rs

[coderabbitai]

⚠️ Potential issue | 🟠 Major | ⚡ Quick win

Reset new Account B-fields in every account-canonicalization path.

The new per-account B fields are added on Line [467], but they are not reset in the in-place account reset paths (e.g., Line [1885], Line [1996], Line [2148]). That can leak stale B snapshots across slot reuse/re-init and violates the “schema-only/all-zero until writers” contract.

💡 Suggested patch

diff --git a/src/percolator.rs b/src/percolator.rs
@@ fn init_in_place(
             a.f_snap = 0;
             a.adl_epoch_snap = 0;
+            a.loss_weight = 0;
+            a.b_snap = 0;
+            a.b_rem = 0;
+            a.b_epoch_snap = 0;
             a.matcher_program = [0; 32];
             a.matcher_context = [0; 32];
             a.owner = [0; 32];
@@ fn free_slot(&mut self, idx: u16) -> Result<()> {
         a.f_snap = 0;
         a.adl_epoch_snap = 0;
+        a.loss_weight = 0;
+        a.b_snap = 0;
+        a.b_rem = 0;
+        a.b_epoch_snap = 0;
         a.matcher_program = [0; 32];
         a.matcher_context = [0; 32];
         a.owner = [0; 32];
@@ fn materialize_at(&mut self, idx: u16, slot_anchor: u64) -> Result<()> {
             a.f_snap = 0i128;
             a.adl_epoch_snap = 0;
+            a.loss_weight = 0u128;
+            a.b_snap = 0u128;
+            a.b_rem = 0u128;
+            a.b_epoch_snap = 0;
             a.matcher_program = [0; 32];
             a.matcher_context = [0; 32];
             a.owner = [0; 32];

Also applies to: 1818-1832

🤖 Prompt for AI Agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@src/percolator.rs` around lines 467 - 483, The new Account fields
loss_weight, b_snap, b_rem and b_epoch_snap must be explicitly zeroed wherever
an account is canonicalized/reset in-place; update each
account-reset/canonicalization branch that currently clears other per-account
fields to also set loss_weight = 0, b_snap = 0, b_rem = 0 and b_epoch_snap = 0
so the schema-only/all-zero invariant holds (i.e., add these zero assignments
alongside the existing resets in the in-place account reset paths that touch
other per-account state).