Functions — github.com/aeyakovenko/percolator

Methodkani_burn_impaired_account_source_claim_fields

( account: &mut PortfolioV16ViewMut<'_>, slot: usize, burn_num: u128, )

src/v16_kani_api.rs:381

Methodkani_can_ignore_unrelated_loss_stale_for_trade

( &self, long_account: &PortfolioV16View<'_>, short_account: &PortfolioV16View<'_>,

src/v16_kani_api.rs:720

Methodkani_canonical_retired_asset_slot

( old_asset: AssetStateV16, )

src/v16_kani_api.rs:682

Methodkani_counterparty_cure_atoms_from_scaled_backing

(amount: u128)

src/v16_kani_api.rs:548

Methodkani_create_initial_margin_source_lien_if_needed

( &mut self, account: &mut PortfolioV16ViewMut<'_>, )

src/v16_kani_api.rs:582

Methodkani_credit_account_from_insurance_delta

( insurance: u128, budget_remaining: u128, c_tot: u128, capital: u128,

src/v16_kani_api.rs:441

Methodkani_credit_backing_provider_earnings_delta

( vault: u128, c_tot: u128, insurance: u128, earnings_total: u128, buc

src/v16_kani_api.rs:363

Methodkani_dynamic_asset_slot_stride

()

src/v16_kani_api.rs:294

Methodkani_ensure_initial_margin

(account: &PortfolioV16View<'_>)

src/v16_kani_api.rs:776

Methodkani_ensure_no_positive_credit_initial_margin

( account: &PortfolioV16View<'_>, )

src/v16_kani_api.rs:780

Functionkani_eq_engine_asset_slot_v16_account

( a: &EngineAssetSlotV16Account, b: &EngineAssetSlotV16Account, )

src/v16_kani_api.rs:1122

Functionkani_eq_market_group_v16_header_account

( a: &MarketGroupV16HeaderAccount, b: &MarketGroupV16HeaderAccount, )

src/v16_kani_api.rs:978

Functionkani_eq_portfolio_account_v16_account

( a: &PortfolioAccountV16Account, b: &PortfolioAccountV16Account, )

src/v16_kani_api.rs:1283

Methodkani_is_sparse_tail_default

(self)

src/v16_kani_api.rs:892

Functionkani_loss_weight_for_basis

(abs_basis_q: u128, a_basis: u128)

src/v16_kani_api.rs:1351

Functionkani_margin_requirement

( notional: u128, margin_bps: u64, min_nonzero_req: u128, )

src/v16_kani_api.rs:897

Methodkani_prepare_counterparty_backing_add_delta

( bucket: BackingBucketV16, source: SourceCreditStateV16, amount: u128, curren

src/v16_kani_api.rs:517

Methodkani_prepare_counterparty_backing_withdraw_delta

( bucket: BackingBucketV16, source: SourceCreditStateV16, amount: u128, )

src/v16_kani_api.rs:533

Methodkani_prepare_counterparty_lien_consume_delta

( bucket: BackingBucketV16, source: SourceCreditStateV16, amount: u128, )

src/v16_kani_api.rs:501

Methodkani_prepare_counterparty_lien_create_delta

( bucket: BackingBucketV16, source: SourceCreditStateV16, current_slot: u64, a

src/v16_kani_api.rs:492

Methodkani_prepare_counterparty_lien_terminal_release_delta

( bucket: BackingBucketV16, source: SourceCreditStateV16, amount: u128, )

src/v16_kani_api.rs:509

Methodkani_prepare_insurance_lien_consume_delta

( reservation: InsuranceCreditReservationV16, source: SourceCreditStateV16, domain_spe

src/v16_kani_api.rs:553

Methodkani_prepare_insurance_lien_terminal_release_delta

( reservation: InsuranceCreditReservationV16, source: SourceCreditStateV16, amount: u1

src/v16_kani_api.rs:574

Methodkani_realize_source_backed_claims_for_resolved_close_not_atomic

( &mut self, account: &mut PortfolioV16ViewMut<'_>, )

src/v16_kani_api.rs:866

Methodkani_resolved_receipt_claimable_against_ledger

( receipt: ResolvedPayoutReceiptV16, ledger: ResolvedPayoutLedgerV16, )

src/v16_kani_api.rs:859

Methodkani_restarted_asset_slot_preserving_insurance_budget

( old_slot: &EngineAssetSlotV16Account, market_id: u64, authenticated_price: u64,

src/v16_kani_api.rs:668

Methodkani_set_account_pnl

( &mut self, account: &mut PortfolioV16ViewMut<'_>, new_pnl: i128, )

src/v16_kani_api.rs:597

Methodkani_set_domain_insurance_budget_delta

( total_remaining: u128, insurance_limit: u128, old_budget: u128, spent: u128,

src/v16_kani_api.rs:405

Methodkani_set_domain_insurance_spent_delta

( total_remaining: u128, insurance: u128, budget: u128, old_spent: u128,

src/v16_kani_api.rs:389

Methodkani_solvency_envelope_holds_for_notional

(&self, n: u128)

src/v16_kani_api.rs:240

Methodkani_source_credit_lien_amounts_for_effective

( effective_credit: u128, credit_rate_num: u128, )

src/v16_kani_api.rs:541

Functionkani_trade_notional_floor

(size_q: u128, exec_price: u64)

src/v16_kani_api.rs:210

Methodkani_trade_signed_size_deltas

(size_q: i128)

src/v16_kani_api.rs:729

Methodkani_transfer_account_residual_reward_credit

( trader: &mut PortfolioV16ViewMut<'_>, lp: &mut PortfolioV16ViewMut<'_>, principal_at

src/v16_kani_api.rs:589

Methodkani_validate_dynamic_market_slots_len

( supplied_len: usize, capacity: usize, configured_market_slots: usize, )

src/v16_kani_api.rs:298

Methodkani_validate_source_domain_ledger_current

(&self, domain: usize)

src/v16_kani_api.rs:359

Methodkani_withdraw_domain_insurance_delta

( vault: u128, insurance: u128, source_reserved_atoms: u128, budget: u128,

src/v16_kani_api.rs:421

Methodkernel_accumulate_batch_trade

( mut outcome: BatchTradeOutcomeV16, risk_increasing: bool, long_has_source_claims: bo

src/v16.rs:910

Methodkernel_advance_close_ledger

PRODUCTION KERNEL (liveness rank): the close-progress ledger advance. Each partition category grows by exactly its delta; residual_remaining is recomp

src/v16.rs:948

Methodkernel_advance_leg_b_snap

( mut leg: PortfolioLegV16, delta_b: u128, new_remainder: u128, remaining_afte

src/v16.rs:1609

Methodkernel_attach_leg

( mut asset: AssetStateV16, side: SideV16, basis_pos_q: i128, loss_weight: u12

src/v16.rs:1862

Methodkernel_bresidual_step

( residual_remaining: u128, booked: Option<BResidualBookingOutcomeV16>, resolved: bool

src/v16.rs:1526

Methodkernel_cert_is_current

( cert: HealthCertV16, oracle_epoch: u64, funding_epoch: u64, risk_epoch: u64,

src/v16.rs:1330

Methodkernel_classify_position_delta

(current: i128, new: i128)

src/v16.rs:1120

Methodkernel_clear_leg

( leg: PortfolioLegV16, mut asset: AssetStateV16, )

src/v16.rs:1710

Methodkernel_consume_insurance_layer

( domain_available: u128, insurance: u128, spent: u128, pnl: i128, )

src/v16.rs:1066

Methodkernel_economically_valid_trade_admits

( evt: EconomicallyValidTradeV16, )

src/v16_kani_api.rs:1702

Methodkernel_initial_margin_gate

(cert: HealthCertV16)

src/v16.rs:846

Methodkernel_locked_margin_gate

( capital: u128, pnl: i128, fee_credits: i128, certified_initial_req: u128,

src/v16.rs:873

Methodkernel_reduce_position_delta

( pre_basis_signed: i128, side: SideV16, requested: u128, )

src/v16.rs:1157

Methodkernel_resize_leg_same_side

( mut leg: PortfolioLegV16, mut asset: AssetStateV16, new_signed: i128, new_we

src/v16.rs:799

Methodkernel_resolved_close_progress

( rank: ResolvedCloseRankV16, )

src/v16_kani_api.rs:1611

Methodkernel_resolved_payout_step

(claimable: u128, vault: u128)

src/v16.rs:1102

Methodkernel_settle_principal

( capital: u128, c_tot: u128, pnl: i128, )

src/v16.rs:1025

Methodkernel_settle_resolved_pnl_after_booking

( pnl: i128, booked_loss: u128, explicit_loss: u128, )

src/v16.rs:1569

Methodkernel_social_loss_chunk_cap

( residual_remaining: u128, public_chunk_cap: u128, )

src/v16.rs:1395

Methodkernel_trade_admit

( guards: TradeGuardSummaryV16, )

src/v16_kani_api.rs:1659

Methodkernel_trade_preflight_admits

PROOF-ONLY FIDELITY MODEL (cfg(kani) harness only)

src/v16_kani_api.rs:1727

Methodkf_target_for_leg_from_asset

( asset: AssetStateV16, leg: PortfolioLegV16, )

src/v16.rs:10091

Methodleg_kf_delta_components_for_settlement_from_asset

( asset: AssetStateV16, leg: PortfolioLegV16, )

src/v16.rs:10162

Methodleg_kf_delta_for_settlement_from_asset

( asset: AssetStateV16, leg: PortfolioLegV16, )

src/v16.rs:10208

Methodliquidation_progress_from_scores

(before: RiskScoreV16, after: RiskScoreV16)

src/v16.rs:499

Functionlive_market_with_pool

Live single-asset market holding only junior surplus.

tests/backing_double_claim_fuzz.rs:539

Functionliveness_b_stale_leg_has_advancing_chunk

()

src/v16_proofs.rs:2068

Functionliveness_pending_close_has_rank_decreasing_advance

()

src/v16_proofs.rs:2007

Methodloss_stale_trade_scope_allowed

( market_loss_stale_active: bool, trade_asset_loss_stale: bool, long_account_loss_stal

src/v16.rs:373

Methodmul

(self, rhs: Self)

src/wide_math.rs:471

Functionmul_div_ceil_u128

Native multiply-divide ceil. Product a*b must not overflow u128. Panics on d==0.

src/wide_math.rs:1607

Functionmul_div_floor_u128

Native multiply-divide floor. Product a*b must not overflow u128. Panics on d==0.

src/wide_math.rs:1600

Methodmul_u256

Widening multiply of two U256 values into U512.

src/wide_math.rs:1165

Methodneg

(self)

src/wide_math.rs:1040

Methodnew

( market_group_id: [u8; 32], portfolio_account_id: [u8; 32], owner: [u8; 32], )

src/v16.rs:2709

Methodnew

(lo: u128, hi: u128)

src/wide_math.rs:34

Methodnew_dynamic

( market_group_id: [u8; 32], config: V16Config, asset_slot_capacity: u32, init

src/v16.rs:6169

Methodpartial_cmp

(&self, other: &Self)

src/wide_math.rs:435

Methodposition_delta_lookup_for_asset

( account: &PortfolioV16View<'_>, asset_index: usize, delta_q: i128, )

src/v16.rs:12309

Methodprepare_asset_recovery_transition

( mut asset: AssetStateV16, asset_set_epoch: u64, risk_epoch: u64, )

src/v16.rs:385

Methodprepare_counterparty_backing_add_delta

( mut bucket: BackingBucketV16, mut source: SourceCreditStateV16, amount: u128,

src/v16.rs:1973

Methodprepare_counterparty_backing_withdraw_delta

( mut bucket: BackingBucketV16, mut source: SourceCreditStateV16, amount: u128, )

src/v16.rs:2027

Methodprepare_counterparty_lien_consume_delta

( mut bucket: BackingBucketV16, mut source: SourceCreditStateV16, amount: u128, )

src/v16.rs:2148

Methodprepare_counterparty_lien_create_delta

( mut bucket: BackingBucketV16, mut source: SourceCreditStateV16, current_slot: u64,

src/v16.rs:1930

Methodprepare_counterparty_lien_impair_delta

( mut bucket: BackingBucketV16, mut source: SourceCreditStateV16, amount: u128, )

src/v16.rs:2202

Methodprepare_counterparty_lien_release_delta

( mut bucket: BackingBucketV16, mut source: SourceCreditStateV16, current_slot: u64,

src/v16.rs:2071

Methodprepare_counterparty_lien_terminal_release_delta

( mut bucket: BackingBucketV16, mut source: SourceCreditStateV16, amount: u128, )

src/v16.rs:2115

Methodprepare_insurance_lien_consume_delta

( mut reservation: InsuranceCreditReservationV16, mut source: SourceCreditStateV16, do

src/v16.rs:2233

Methodprepare_insurance_lien_create_delta

( mut reservation: InsuranceCreditReservationV16, mut source: SourceCreditStateV16, am

src/v16.rs:2289

Methodprepare_insurance_lien_impair_delta

( mut reservation: InsuranceCreditReservationV16, mut source: SourceCreditStateV16, am

src/v16.rs:2423

Methodprepare_insurance_lien_release_delta

( mut reservation: InsuranceCreditReservationV16, mut source: SourceCreditStateV16, am

src/v16.rs:2334

Methodprepare_insurance_lien_terminal_release_delta

( mut reservation: InsuranceCreditReservationV16, mut source: SourceCreditStateV16, am

src/v16.rs:2376

Methodprepare_source_credit_domain_recompute_for_epoch

( mut source: SourceCreditStateV16, risk_epoch: u64, )

src/v16.rs:671

Methodprepare_source_positive_claim_bound_delta

( mut source: SourceCreditStateV16, claim_bound_num: u128, exact_claim_num: u128,

src/v16.rs:700

Functionproof_v16_active_bitmap_set_get_count_is_exact_and_bounds_checked

()

tests/proofs_v16.rs:186

Functionproof_v16_adjust_u128_applies_exact_delta_or_fails_closed

()

tests/proofs_v16_arithmetic.rs:254

Functionproof_v16_adjust_u128_applies_exact_delta_or_fails_closed

()

tests/proofs_v16.rs:3168

Functionproof_v16_asset_recovery_transition_freezes_price_and_bumps_once

()

tests/proofs_v16.rs:729

Functionproof_v16_asset_recovery_transition_is_idempotent_after_recovery

()

tests/proofs_v16.rs:763

Functionproof_v16_auto_crank_refresh_is_unique_observation_requiring_plan

()

tests/proofs_v16.rs:14430

Functionproof_v16_available_source_support_excludes_liened_and_encumbered_amounts

()

tests/proofs_v16.rs:6456

Functionproof_v16_backing_domain_fee_split_for_lien_delta_is_exact_and_conservative

()

tests/proofs_v16.rs:4100

Functionproof_v16_backing_provider_earnings_credit_requires_vault_slack

()

tests/proofs_v16.rs:5249

Functions1,205 in github.com/aeyakovenko/percolator