"""V2a: hypothesis property tests (V-TYPES doctrine). Three targets, highest value first: 1. ExecutionRouter state machine — the accounting-adjacent core: pop- semantics make fill-vs-retry mutually exclusive, EXITs are never suppressible by expiry, retry chains are bounded. 2. LatencyHistogram.percentile_ns — the gate numbers themselves (the nearest-rank/banker's-rounding bug class is live in this codebase's history). 3. DivergenceRow — NaN/inf/negative inputs always rejected; valid rows round-trip unchanged. """ from __future__ import annotations import math import sys sys.path.insert(0, "/mnt/dolphinng5_predict") import pytest from hypothesis import HealthCheck, given, settings, strategies as st from hypothesis.stateful import ( RuleBasedStateMachine, initialize, invariant, precondition, rule, ) from pydantic import ValidationError from prod.clean_arch.dita_v2.exec_router import ( ExecConfig, ExecutionRouter, MissAction, ) from prod.clean_arch.violet.clock import LatencyHistogram from prod.clean_arch.violet.domain import DivergenceRow # ── 1. router state machine ─────────────────────────────────────────────────── class RouterMachine(RuleBasedStateMachine): """Drives the REAL ExecutionRouter through plan/register/fill/cancel/ expiry sequences with a fake clock, asserting the V2 driver's load- bearing invariants.""" @initialize(retries=st.integers(min_value=0, max_value=3), exhaust=st.sampled_from(["skip", "market"])) def setup(self, retries, exhaust): self.now = 1000.0 self.cfg = ExecConfig(style="maker_both", entry_miss="retry", entry_retries=retries, retry_exhaust=exhaust) self.router = ExecutionRouter(self.cfg, clock=lambda: self.now) self.n = 0 self.filled: set[str] = set() self.retried: set[str] = set() # trade_ids consumed by a retry self.retry_count: dict[str, int] = {} # base_trade_id → retries used def _fresh_tid(self) -> str: self.n += 1 return f"T{self.n:04d}" @rule(px=st.floats(min_value=0.5, max_value=50_000, allow_nan=False)) def plan_and_register_entry(self, px): tid = self._fresh_tid() plan = self.router.plan_entry(trade_id=tid, asset="BTCUSDT", position_side="SHORT", reference_price=px) if self.router.has_working_entry() and plan.suppress: return # R2: slot spoken for assert not plan.suppress if plan.is_maker: assert plan.sane() and plan.order_type == "LIMIT" self.router.register_working(trade_id=tid, asset="BTCUSDT", position_side="SHORT", plan=plan) @rule(px=st.floats(min_value=0.5, max_value=50_000, allow_nan=False), reason=st.sampled_from(["TAKE_PROFIT", "STOP_LOSS", "MAX_HOLD", "CATASTROPHIC", "ADVSL"])) def plan_exit_never_stranded(self, px, reason): tid = self._fresh_tid() plan = self.router.plan_exit(trade_id=tid, asset="BTCUSDT", position_side="SHORT", reference_price=px, reason=reason) # RULE 1: with no same-trade working exit, an exit plan is never # suppressed — maker or MARKET, it reaches the venue. assert not plan.suppress assert plan.sane() if plan.is_maker: self.router.register_working(trade_id=tid, asset="BTCUSDT", position_side="SHORT", plan=plan) @precondition(lambda self: self.router.working_orders()) @rule(data=st.data()) def fill_working(self, data): wo = data.draw(st.sampled_from(self.router.working_orders())) self.router.note_fill(wo.trade_id) assert wo.trade_id not in self.retried, \ "a trade_id must never be both filled and retried" self.filled.add(wo.trade_id) assert self.router.working(wo.trade_id) is None # pop semantics @precondition(lambda self: any(w.action == "ENTER" for w in self.router.working_orders())) @rule(data=st.data(), px=st.floats(min_value=0.5, max_value=50_000, allow_nan=False)) def expire_entry_and_apply_miss_policy(self, data, px): entries = [w for w in self.router.working_orders() if w.action == "ENTER"] wo = data.draw(st.sampled_from(entries)) self.now += 1000.0 # everything expires action = self.router.entry_miss_action(wo) self.router.note_cancel(wo.trade_id) # runtime cancelled the quote assert wo.trade_id not in self.filled, \ "a filled trade must never reach the miss path (pop semantics)" if action == MissAction.RETRY: self.retried.add(wo.trade_id) used = self.retry_count.get(wo.base_trade_id, 0) + 1 self.retry_count[wo.base_trade_id] = used assert used <= self.cfg.entry_retries, "retry chain must be bounded" new_tid, plan = self.router.retry_plan(wo, reference_price=px) assert new_tid == f"{wo.base_trade_id}-r{wo.retry_n + 1}" assert plan.action == "ENTER" if plan.is_maker and not self.router.has_working_entry(): self.router.register_working( trade_id=new_tid, asset=wo.asset, position_side=wo.side, plan=plan, base_trade_id=wo.base_trade_id, retry_n=wo.retry_n + 1) elif action == MissAction.MARKET: new_tid, plan = self.router.market_fallback_plan(wo) assert new_tid == f"{wo.base_trade_id}-m" # ENTER → fresh lifecycle assert plan.action == "ENTER" and plan.order_type == "MARKET" else: assert action == MissAction.SKIP @precondition(lambda self: any(w.action == "EXIT" for w in self.router.working_orders())) @rule(data=st.data()) def expire_exit_escalates_market_same_trade(self, data): exits = [w for w in self.router.working_orders() if w.action == "EXIT"] wo = data.draw(st.sampled_from(exits)) self.now += 1000.0 new_tid, plan = self.router.market_fallback_plan(wo) # RULE 1: the MARKET escalation stays attached to the SAME trade. assert new_tid == wo.trade_id assert plan.action == "EXIT" and plan.order_type == "MARKET" assert not plan.suppress self.router.note_cancel(wo.trade_id) @invariant() def registry_is_consistent(self): wos = self.router.working_orders() assert len({w.trade_id for w in wos}) == len(wos) for w in wos: assert w.retries_left >= 0 assert w.trade_id not in self.filled # filled ⇒ popped, forever assert sum(1 for w in wos if w.action == "ENTER") <= 1 # R2 # derandomize: the suite must be reproducible run-to-run (the V0/V2 gates # assert determinism elsewhere; a flaky property is worse than a fixed one). # Health checks are suppressed because rule preconditions legitimately # filter often and CPU contention during the full suite trips too_slow. RouterMachine.TestCase.settings = settings( max_examples=30, stateful_step_count=30, deadline=None, derandomize=True, suppress_health_check=list(HealthCheck)) TestRouterMachine = RouterMachine.TestCase # ── 2. LatencyHistogram percentile laws ─────────────────────────────────────── @given(samples=st.lists(st.integers(min_value=0, max_value=10**12), min_size=1, max_size=500), p=st.floats(min_value=0.001, max_value=1.0)) @settings(max_examples=150, deadline=None, derandomize=True, suppress_health_check=[HealthCheck.too_slow]) def test_percentile_is_a_retained_sample(samples, p): h = LatencyHistogram("prop") for s in samples: h.record(s) assert h.percentile_ns(p) in samples @given(samples=st.lists(st.integers(min_value=0, max_value=10**12), min_size=1, max_size=500)) @settings(max_examples=100, deadline=None, derandomize=True, suppress_health_check=[HealthCheck.too_slow]) def test_percentile_monotone_and_extremes(samples): h = LatencyHistogram("prop") for s in samples: h.record(s) ps = [0.01, 0.25, 0.5, 0.9, 0.99, 0.999, 1.0] vals = [h.percentile_ns(p) for p in ps] assert vals == sorted(vals), "percentile must be monotone in p" assert vals[-1] == max(samples) assert h.percentile_ns(0.0000001) == min(samples) # ── 3. DivergenceRow parse laws ─────────────────────────────────────────────── _finite_px = st.floats(min_value=1e-9, max_value=1e9, allow_nan=False, allow_infinity=False) _any_float = st.floats(allow_nan=True, allow_infinity=True) @given(scan=_finite_px, mid=_finite_px, bps=st.floats(min_value=-1e6, max_value=1e6, allow_nan=False), sseq=st.integers(min_value=0, max_value=2**31), vseq=st.integers(min_value=0, max_value=2**31)) @settings(max_examples=150, deadline=None, derandomize=True, suppress_health_check=[HealthCheck.too_slow]) def test_valid_rows_round_trip(scan, mid, bps, sseq, vseq): src = dict(ts=1, session_id="s", asset="BTCUSDT", scan_price=scan, venue_mid=mid, divergence_bps=bps, scan_seq=sseq, venue_seq=vseq, mono_ns=0) assert DivergenceRow(**src).model_dump() == src @given(bad_px=_any_float) @settings(max_examples=150, deadline=None, derandomize=True, suppress_health_check=[HealthCheck.too_slow]) def test_nonpositive_or_nonfinite_prices_always_rejected(bad_px): if math.isfinite(bad_px) and bad_px > 0: return # valid by definition with pytest.raises(ValidationError): DivergenceRow(ts=1, session_id="s", asset="BTCUSDT", scan_price=bad_px, venue_mid=1.0, divergence_bps=0.0, scan_seq=0, venue_seq=0, mono_ns=0) @given(seq=st.integers(max_value=-1)) @settings(max_examples=50, deadline=None, derandomize=True, suppress_health_check=[HealthCheck.too_slow]) def test_negative_seqs_always_rejected(seq): with pytest.raises(ValidationError): DivergenceRow(ts=1, session_id="s", asset="BTCUSDT", scan_price=1.0, venue_mid=1.0, divergence_bps=0.0, scan_seq=seq, venue_seq=0, mono_ns=0) if __name__ == "__main__": raise SystemExit(pytest.main([__file__, "-v"]))