my-project-public

repository

loading code, commits, and activity

repositories

loading repo index

#1	//! Shared helpers, constants, and param factories for proof files.
#2
#3	pub use percolator::*;
#4	pub use percolator::i128::{I128, U128};
#5	pub use percolator::wide_math::{
#6	U256, I256,
#7	floor_div_signed_conservative,
#8	saturating_mul_u256_u64,
#9	fee_debt_u128_checked,
#10	mul_div_floor_u256,
#11	mul_div_floor_u256_with_rem,
#12	mul_div_ceil_u256,
#13	wide_signed_mul_div_floor,
#14	ceil_div_positive_checked,
#15	mul_div_floor_u128,
#16	mul_div_ceil_u128,
#17	wide_mul_div_floor_u128,
#18	wide_signed_mul_div_floor_from_k_pair,
#19	saturating_mul_u128_u64,
#20	};
#21
#22	// ============================================================================
#23	// Small-model constants
#24	// ============================================================================
#25
#26	/// Small-model scale factors (minimal bit-widths for CBMC tractability).
#27	/// All arithmetic stays within i32/u16 to avoid 64-bit SAT blowup.
#28	pub const S_POS_SCALE: u16 = 4;
#29	pub const S_ADL_ONE: u16 = 256;
#30
#31	// ============================================================================
#32	// Engine constants
#33	// ============================================================================
#34
#35	pub const DEFAULT_ORACLE: u64 = 1_000;
#36	pub const DEFAULT_SLOT: u64 = 100;
#37
#38	// ============================================================================
#39	// Small-model helpers
#40	// ============================================================================
#41
#42	/// Small-model: eager PnL for one mark event (long).
#43	pub fn eager_mark_pnl_long(q_base: i32, delta_p: i32) -> i32 {
#44	q_base * delta_p
#45	}
#46
#47	/// Small-model: eager PnL for one mark event (short).
#48	pub fn eager_mark_pnl_short(q_base: i32, delta_p: i32) -> i32 {
#49	-(q_base * delta_p)
#50	}
#51
#52	/// Small-model: lazy PnL from K difference.
#53	/// pnl_delta = floor(\|basis_q\| * (K_cur - k_snap) / (a_basis * POS_SCALE))
#54	pub fn lazy_pnl(basis_q_abs: u16, k_diff: i32, a_basis: u16) -> i32 {
#55	let den = (a_basis as i32) * (S_POS_SCALE as i32);
#56	if den == 0 { return 0; }
#57	let num = (basis_q_abs as i32) * k_diff;
#58	if num >= 0 {
#59	num / den
#60	} else {
#61	let abs_num = -num;
#62	-((abs_num + den - 1) / den)
#63	}
#64	}
#65
#66	/// Small-model: lazy effective quantity.
#67	pub fn lazy_eff_q(basis_q_abs: u16, a_cur: u16, a_basis: u16) -> u16 {
#68	if a_basis == 0 { return 0; }
#69	let product = (basis_q_abs as i32) * (a_cur as i32);
#70	(product / (a_basis as i32)) as u16
#71	}
#72
#73	/// Small-model: K update for mark event (long).
#74	pub fn k_after_mark_long(k_before: i32, a_long: u16, delta_p: i32) -> i32 {
#75	k_before + (a_long as i32) * delta_p
#76	}
#77
#78	/// Small-model: K update for mark event (short).
#79	pub fn k_after_mark_short(k_before: i32, a_short: u16, delta_p: i32) -> i32 {
#80	k_before - (a_short as i32) * delta_p
#81	}
#82
#83	/// Small-model: K update for funding event (long).
#84	pub fn k_after_fund_long(k_before: i32, a_long: u16, delta_f: i32) -> i32 {
#85	k_before - (a_long as i32) * delta_f
#86	}
#87
#88	/// Small-model: K update for funding event (short).
#89	pub fn k_after_fund_short(k_before: i32, a_short: u16, delta_f: i32) -> i32 {
#90	k_before + (a_short as i32) * delta_f
#91	}
#92
#93	/// Small-model: A update for ADL quantity shrink.
#94	pub fn a_after_adl(a_old: u16, oi_post: u16, oi: u16) -> u16 {
#95	if oi == 0 { return a_old; }
#96	let product = (a_old as i32) * (oi_post as i32);
#97	(product / (oi as i32)) as u16
#98	}
#99
#100	// ============================================================================
#101	// Engine param helpers
#102	// ============================================================================
#103
#104	pub fn zero_fee_params() -> RiskParams {
#105	RiskParams {
#106	warmup_period_slots: 100,
#107	maintenance_margin_bps: 500,
#108	initial_margin_bps: 1000,
#109	trading_fee_bps: 0,
#110	max_accounts: MAX_ACCOUNTS as u64,
#111	new_account_fee: U128::ZERO,
#112	maintenance_fee_per_slot: U128::ZERO,
#113	max_crank_staleness_slots: u64::MAX,
#114	liquidation_fee_bps: 0,
#115	liquidation_fee_cap: U128::ZERO,
#116	liquidation_buffer_bps: 50,
#117	min_liquidation_abs: U128::ZERO,
#118	min_initial_deposit: U128::new(2),
#119	min_nonzero_mm_req: 1,
#120	min_nonzero_im_req: 2,
#121	insurance_floor: U128::ZERO,
#122	}
#123	}
#124
#125	pub fn default_params() -> RiskParams {
#126	RiskParams {
#127	warmup_period_slots: 100,
#128	maintenance_margin_bps: 500,
#129	initial_margin_bps: 1000,
#130	trading_fee_bps: 10,
#131	max_accounts: MAX_ACCOUNTS as u64,
#132	new_account_fee: U128::new(1000),
#133	maintenance_fee_per_slot: U128::new(1),
#134	max_crank_staleness_slots: 1000,
#135	liquidation_fee_bps: 100,
#136	liquidation_fee_cap: U128::new(1_000_000),
#137	liquidation_buffer_bps: 50,
#138	min_liquidation_abs: U128::new(0),
#139	min_initial_deposit: U128::new(1000),
#140	min_nonzero_mm_req: 1,
#141	min_nonzero_im_req: 2,
#142	insurance_floor: U128::ZERO,
#143	}
#144	}
#145

z6Mkq5mY3JWtxoxUobWcfNHm7AkRubgSWEZTkBVqZXJviFZ5/my-project-public