"""Property-based tests for v3 correlation-aware clustering. Feature: math-core-v3-engine Uses Hypothesis to validate correctness properties of the v3 clustering layer: effective evidence count n_eff is bounded by cluster size, and cluster LLR is clamped to [-2.5, 2.5]. Validates: Requirements 4.2, 4.3, 4.4, 4.5, 21.4 """ from __future__ import annotations from hypothesis import given, settings from hypothesis import strategies as st from services.aggregation.worker import ( compute_cluster_llr, compute_n_eff, ) # --------------------------------------------------------------------------- # Hypothesis strategies # --------------------------------------------------------------------------- # LLR values for testing llr_values = st.floats(min_value=-5.0, max_value=5.0, allow_nan=False, allow_infinity=False) llr_lists = st.lists(llr_values, min_size=1, max_size=20) # Correlation values rho_values = st.floats(min_value=0.0, max_value=1.0, allow_nan=False, allow_infinity=False) def _symmetric_correlation_matrix(n: int) -> st.SearchStrategy[list[list[float]]]: """Generate an NxN symmetric correlation matrix with values in [0, 1]. Diagonal is 1.0, off-diagonal entries are symmetric rho in [0, 1]. """ if n <= 1: return st.just([[1.0]]) # Generate upper-triangle entries (n*(n-1)/2 values) n_pairs = n * (n - 1) // 2 upper_triangle = st.lists(rho_values, min_size=n_pairs, max_size=n_pairs) @st.composite def build_matrix(draw: st.DrawFn) -> list[list[float]]: entries = draw(upper_triangle) matrix = [[0.0] * n for _ in range(n)] idx = 0 for i in range(n): matrix[i][i] = 1.0 for j in range(i + 1, n): matrix[i][j] = entries[idx] matrix[j][i] = entries[idx] idx += 1 return matrix return build_matrix() # n_eff positive floats for property 6 n_eff_values = st.floats(min_value=0.1, max_value=20.0, allow_nan=False, allow_infinity=False) # --------------------------------------------------------------------------- # Property 5: Effective evidence count n_eff is bounded by cluster size # Feature: math-core-v3-engine, Property 5: Effective evidence count n_eff is bounded by cluster size # Validates: Requirements 4.2, 4.3, 21.4 # --------------------------------------------------------------------------- @settings(max_examples=100) @given(llrs=llr_lists) def test_property_5_n_eff_bounded_by_cluster_size_default_correlations( llrs: list[float], ) -> None: """Property 5: n_eff is bounded by cluster size (default correlations). For any cluster of N signals using default pairwise correlations (rho=0.80), the computed n_eff SHALL satisfy 0 < n_eff <= N. **Validates: Requirements 4.2, 4.3** """ n = len(llrs) n_eff = compute_n_eff(llrs) assert n_eff > 0.0, f"n_eff={n_eff} must be positive" assert n_eff <= n + 1e-9, f"n_eff={n_eff} exceeds cluster size N={n}" @settings(max_examples=100) @given( data=st.data(), llrs=st.lists(llr_values, min_size=2, max_size=10), ) def test_property_5_n_eff_bounded_with_explicit_correlations( data: st.DataObject, llrs: list[float], ) -> None: """Property 5: n_eff is bounded by cluster size (explicit correlation matrix). For any cluster of N signals with a symmetric NxN correlation matrix with values in [0, 1], the computed n_eff SHALL satisfy 0 < n_eff <= N. **Validates: Requirements 4.2, 4.3, 21.4** """ n = len(llrs) corr_matrix = data.draw(_symmetric_correlation_matrix(n)) n_eff = compute_n_eff(llrs, correlations=corr_matrix) assert n_eff > 0.0, f"n_eff={n_eff} must be positive" assert n_eff <= n + 1e-9, f"n_eff={n_eff} exceeds cluster size N={n}" # --------------------------------------------------------------------------- # Property 6: Cluster LLR is clamped to [-2.5, 2.5] # Feature: math-core-v3-engine, Property 6: Cluster LLR is clamped to [-2.5, 2.5] # Validates: Requirements 4.4, 4.5 # --------------------------------------------------------------------------- @settings(max_examples=100) @given( llrs=llr_lists, n_eff=n_eff_values, ) def test_property_6_cluster_llr_clamped( llrs: list[float], n_eff: float, ) -> None: """Property 6: Cluster LLR is clamped to [-2.5, 2.5]. For any cluster configuration with any number of signals and any LLR values, the computed cluster LLR_c SHALL be in [-2.5, 2.5]. **Validates: Requirements 4.4, 4.5** """ cluster_llr = compute_cluster_llr(llrs, n_eff) assert -2.5 <= cluster_llr <= 2.5, ( f"cluster_llr={cluster_llr} out of [-2.5, 2.5]" ) @settings(max_examples=100) @given(llrs=llr_lists) def test_property_6_cluster_llr_clamped_with_computed_n_eff( llrs: list[float], ) -> None: """Property 6: Cluster LLR is clamped when using computed n_eff. End-to-end: compute n_eff from the LLRs, then compute cluster LLR. The result SHALL still be in [-2.5, 2.5]. **Validates: Requirements 4.4, 4.5** """ n_eff = compute_n_eff(llrs) cluster_llr = compute_cluster_llr(llrs, n_eff) assert -2.5 <= cluster_llr <= 2.5, ( f"cluster_llr={cluster_llr} out of [-2.5, 2.5]" )