Files
siloqy/prod/clean_arch/violet/test_violet_properties.py
Codex ba01b914ce VIOLET V2a: V-TYPES domain layer + hypothesis properties + divergence reject-at-source
domain.py: refined scalar aliases (BarsHeld kills the bars_held=-106
UInt16 poison class by construction), DivergenceRow (DDL-shaped, frozen,
extra=forbid), ExecDriverSettings (env boundary for the V2 driver; ttl
override exists because the shared router clamps TTLs >= 0.5s),
ExecGateReport schema, beartype 'typed' decorator with
DOLPHIN_VIOLET_BEARTYPE=0 kill-switch.

divergence.py: rows now parse through DivergenceRow before the sink —
malformed rows die at the source with a rate-limited WARNING + counter,
never at the head of the CH spool.

Properties (hypothesis, derandomized): ExecutionRouter state machine
(fill/retry mutual exclusion via pop-semantics, R1 exit escalation same
trade_id, bounded retry chains, <=1 working ENTER), LatencyHistogram
percentile laws (member-of-samples, monotone, extremes), DivergenceRow
parse laws. 34 new tests; violet suite 64 green; router 77 green; zero
shared-file edits.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-06-13 00:08:18 +02:00

242 lines
11 KiB
Python

"""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"]))