|
| 1 | +//! Pillar-7 — 3D EWA-sandwich certification probe. |
| 2 | +//! |
| 3 | +//! Certifies that the 3D EWA (Elliptical Weighted Average) sandwich update |
| 4 | +//! |
| 5 | +//! ```text |
| 6 | +//! Σ_{n+1} = M · Σ_n · Mᵀ |
| 7 | +//! ``` |
| 8 | +//! |
| 9 | +//! preserves symmetric positive-definiteness (SPD) across 1 000 random paths |
| 10 | +//! × 10 hops, where `M = sqrt(step_Σ_3d)` is a contractive `Spd3` drawn |
| 11 | +//! from the shared `prove_runner::random_contractive_spd3` helper. |
| 12 | +//! |
| 13 | +//! # Relationship to Pillar-6 |
| 14 | +//! |
| 15 | +//! Pillar-7 is the direct 3D twin of the Pillar-6 2D probe. Where Pillar-6 |
| 16 | +//! certifies `Σ' = M · Σ · Mᵀ` for 2×2 SPD matrices, Pillar-7 does the same |
| 17 | +//! for 3×3 SPD matrices using `crate::hpc::splat3d::spd3::sandwich` and the |
| 18 | +//! Smith-1961 closed-form eigendecomposition in `eig_sym::eig_sym_3`. |
| 19 | +//! |
| 20 | +//! # PASS criteria |
| 21 | +//! |
| 22 | +//! * PSD rate ≥ 0.999 over 1 000 paths × 10 hops (10 000 SPD checks). |
| 23 | +//! * Log-norm Frobenius KS-Thm-1 concentration: reported but not gated. |
| 24 | +//! |
| 25 | +//! # Parity gate |
| 26 | +//! |
| 27 | +//! `eig_sym_3` (PR-X10 A4) must produce eigenvalues bit-equivalent to |
| 28 | +//! `splat3d::Spd3::eig` (Smith-1961 in `splat3d/spd3.rs`). The |
| 29 | +//! `parity_eig_sym_3_vs_spd3_eig` test enforces max abs error < 1e-5 over |
| 30 | +//! 100 random SPD3 matrices drawn with the Pillar-7 SEED. |
| 31 | +//! |
| 32 | +//! # Feature gate |
| 33 | +//! |
| 34 | +//! Compiled under `#[cfg(feature = "pillar")]`. The parity gate test also |
| 35 | +//! requires `#[cfg(feature = "splat3d")]`. |
| 36 | +
|
| 37 | +use crate::hpc::linalg::eig_sym::eig_sym_3; |
| 38 | +use crate::hpc::pillar::prove_runner::{ |
| 39 | + assert_psd_rate, random_contractive_spd3, PillarReport, SplitMix64, |
| 40 | +}; |
| 41 | +use crate::hpc::splat3d::spd3::{sandwich, Spd3}; |
| 42 | + |
| 43 | +// ── Public constants ────────────────────────────────────────────────────────── |
| 44 | + |
| 45 | +/// SEED for the Pillar-7 splitmix64 RNG. All runs are SEED-anchored for |
| 46 | +/// cross-platform reproducibility and deterministic audit trails. |
| 47 | +pub const PILLAR_7_SEED: u64 = 0x_EDA_5A_DC_5A_DD; |
| 48 | + |
| 49 | +/// Minimum PSD preservation rate for the Pillar-7 probe to PASS. |
| 50 | +pub const PILLAR_7_PSD_THRESHOLD: f64 = 0.999; |
| 51 | + |
| 52 | +// ── Sandwich kernel ─────────────────────────────────────────────────────────── |
| 53 | + |
| 54 | +/// Convert a raw 3×3 array (from `random_contractive_spd3`) to an `Spd3`. |
| 55 | +/// |
| 56 | +/// Reads only the upper triangle (the helper guarantees symmetry) and wraps |
| 57 | +/// it in the `Spd3` repr. |
| 58 | +#[inline] |
| 59 | +fn array_to_spd3(m: [[f32; 3]; 3]) -> Spd3 { |
| 60 | + Spd3::new(m[0][0], m[0][1], m[0][2], m[1][1], m[1][2], m[2][2]) |
| 61 | +} |
| 62 | + |
| 63 | +/// Compute the EWA sandwich `M · Σ · Mᵀ` using `splat3d::spd3::sandwich`. |
| 64 | +/// |
| 65 | +/// `m` is the step matrix (square root of a contractive SPD3). |
| 66 | +/// `sigma` is the current 3×3 SPD covariance. |
| 67 | +/// |
| 68 | +/// The `sandwich` function from `splat3d::spd3` computes `M · N · Mᵀ` |
| 69 | +/// (since M is symmetric, `Mᵀ = M`), averaging the two off-diagonal |
| 70 | +/// halves to suppress f32 asymmetry. Output is always symmetric. |
| 71 | +#[inline] |
| 72 | +pub fn ewa_sandwich_3d(m: &Spd3, sigma: &Spd3) -> Spd3 { |
| 73 | + sandwich(m, sigma) |
| 74 | +} |
| 75 | + |
| 76 | +/// Check whether `sigma` is symmetric positive-definite via eigenvalue check. |
| 77 | +/// |
| 78 | +/// Uses `eig_sym_3` (Smith-1961 closed-form, same algorithm as `Spd3::eig`) |
| 79 | +/// and asserts that the smallest eigenvalue `λ₃ > 0`. This is numerically |
| 80 | +/// robust even when the matrix determinant underflows to zero in f32 (which |
| 81 | +/// can happen when all eigenvalues are tiny but positive, e.g. after many |
| 82 | +/// contractive sandwich steps). The eigenvalue computation works in terms of |
| 83 | +/// the trace and off-diagonal structure, which remain well-conditioned. |
| 84 | +#[inline] |
| 85 | +fn is_psd_eig(s: &Spd3) -> bool { |
| 86 | + let rows = s.to_rows(); |
| 87 | + let (_, _, l3, _) = eig_sym_3(&rows); |
| 88 | + l3 > 0.0 |
| 89 | +} |
| 90 | + |
| 91 | +/// Frobenius norm of log(Σ) — used for the KS-Thm-1 concentration metric. |
| 92 | +/// |
| 93 | +/// Computes the matrix logarithm via spectral lift (Smith-1961 eigenvalues), |
| 94 | +/// then returns `‖log(Σ)‖_F`. Eigenvalues are clamped to a small positive |
| 95 | +/// ε before `ln` so the output stays finite under f32 cancellation noise. |
| 96 | +#[inline] |
| 97 | +fn log_frob(s: &Spd3) -> f32 { |
| 98 | + let rows = s.to_rows(); |
| 99 | + let (l1, l2, l3, v) = eig_sym_3(&rows); |
| 100 | + let eps = 1e-30_f32; |
| 101 | + let ln1 = l1.max(eps).ln(); |
| 102 | + let ln2 = l2.max(eps).ln(); |
| 103 | + let ln3 = l3.max(eps).ln(); |
| 104 | + // ‖V · diag(ln λ) · Vᵀ‖_F = sqrt(ln1² + ln2² + ln3²) since V is orthonormal. |
| 105 | + (ln1 * ln1 + ln2 * ln2 + ln3 * ln3).sqrt() |
| 106 | +} |
| 107 | + |
| 108 | +// ── Main probe ──────────────────────────────────────────────────────────────── |
| 109 | + |
| 110 | +/// Run the Pillar-7 3D EWA-sandwich certification probe. |
| 111 | +/// |
| 112 | +/// Simulates 1 000 random paths × 10 cascade hops. On each hop the covariance |
| 113 | +/// is updated by the sandwich `Σ_{n+1} = M · Σ_n · Mᵀ` where `M = |
| 114 | +/// sqrt(step_Σ_3d)` is a random contractive `Spd3` drawn from the shared |
| 115 | +/// harness. PSD is checked after every hop via Sylvester's criterion. |
| 116 | +/// |
| 117 | +/// # PASS criteria |
| 118 | +/// |
| 119 | +/// * `psd_rate ≥ PILLAR_7_PSD_THRESHOLD` (= 0.999) |
| 120 | +/// |
| 121 | +/// # Determinism |
| 122 | +/// |
| 123 | +/// The RNG is seeded with `PILLAR_7_SEED` so every run on every platform |
| 124 | +/// produces the identical path sequence and the identical `PillarReport`. |
| 125 | +/// |
| 126 | +/// # Example |
| 127 | +/// |
| 128 | +/// ```rust |
| 129 | +/// use ndarray::hpc::pillar::ewa_sandwich_3d::prove_pillar_7; |
| 130 | +/// let report = prove_pillar_7(); |
| 131 | +/// report.print(); |
| 132 | +/// assert!(report.passed); |
| 133 | +/// ``` |
| 134 | +pub fn prove_pillar_7() -> PillarReport { |
| 135 | + const N_PATHS: u32 = 1_000; |
| 136 | + const N_HOPS: u32 = 10; |
| 137 | + const SIGMA_STEP: f32 = 0.1; // contractive step — keeps Σ bounded |
| 138 | + |
| 139 | + let mut rng = SplitMix64::new(PILLAR_7_SEED); |
| 140 | + |
| 141 | + let mut psd_passed: u32 = 0; |
| 142 | + let total_hops: u32 = N_PATHS * N_HOPS; |
| 143 | + |
| 144 | + // Log-norm Frobenius accumulator for KS-Thm-1 concentration. |
| 145 | + let mut log_frob_sum: f64 = 0.0; |
| 146 | + let mut log_frob_sum_sq: f64 = 0.0; |
| 147 | + let mut log_frob_count: u32 = 0; |
| 148 | + |
| 149 | + for _path in 0..N_PATHS { |
| 150 | + // Each path starts from the 3×3 identity covariance. |
| 151 | + let mut sigma = Spd3::I; |
| 152 | + |
| 153 | + for _hop in 0..N_HOPS { |
| 154 | + // Draw a random contractive SPD3 step matrix and take its sqrt. |
| 155 | + let step_raw = random_contractive_spd3(&mut rng, SIGMA_STEP); |
| 156 | + let step_spd = array_to_spd3(step_raw); |
| 157 | + let m = step_spd.sqrt(); |
| 158 | + |
| 159 | + // Apply the EWA sandwich: Σ_{n+1} = M · Σ_n · Mᵀ. |
| 160 | + sigma = ewa_sandwich_3d(&m, &sigma); |
| 161 | + |
| 162 | + // PSD check via Sylvester's criterion. |
| 163 | + if is_psd_eig(&sigma) { |
| 164 | + psd_passed += 1; |
| 165 | + |
| 166 | + // Accumulate log-norm Frobenius for concentration metric. |
| 167 | + let lf = log_frob(&sigma) as f64; |
| 168 | + log_frob_sum += lf; |
| 169 | + log_frob_sum_sq += lf * lf; |
| 170 | + log_frob_count += 1; |
| 171 | + } |
| 172 | + } |
| 173 | + } |
| 174 | + |
| 175 | + let psd_rate = (psd_passed as f64) / (total_hops as f64); |
| 176 | + let passed = assert_psd_rate(psd_passed, total_hops, PILLAR_7_PSD_THRESHOLD); |
| 177 | + |
| 178 | + // KS-Thm-1 concentration: sample std-dev of log-norm Frobenius values. |
| 179 | + // A well-concentrated distribution has small variance (near 0). |
| 180 | + let lognorm_concentration = if log_frob_count > 1 { |
| 181 | + let mean = log_frob_sum / log_frob_count as f64; |
| 182 | + let var = log_frob_sum_sq / log_frob_count as f64 - mean * mean; |
| 183 | + var.max(0.0).sqrt() |
| 184 | + } else { |
| 185 | + 0.0 |
| 186 | + }; |
| 187 | + |
| 188 | + PillarReport { |
| 189 | + pillar_id: 7, |
| 190 | + seed: PILLAR_7_SEED, |
| 191 | + n_paths: N_PATHS, |
| 192 | + n_hops: N_HOPS, |
| 193 | + psd_rate, |
| 194 | + lognorm_concentration, |
| 195 | + passed, |
| 196 | + } |
| 197 | +} |
| 198 | + |
| 199 | +// ── Tests ───────────────────────────────────────────────────────────────────── |
| 200 | + |
| 201 | +#[cfg(test)] |
| 202 | +mod tests { |
| 203 | + use super::*; |
| 204 | + |
| 205 | + // ── Smoke test: prove_pillar_7 must pass ────────────────────────────────── |
| 206 | + |
| 207 | + #[test] |
| 208 | + fn prove_pillar_7_passes() { |
| 209 | + let report = prove_pillar_7(); |
| 210 | + report.print(); |
| 211 | + assert!( |
| 212 | + report.passed, |
| 213 | + "Pillar-7 FAILED: psd_rate={:.6} < threshold={:.6}", |
| 214 | + report.psd_rate, PILLAR_7_PSD_THRESHOLD |
| 215 | + ); |
| 216 | + assert_eq!(report.pillar_id, 7); |
| 217 | + assert_eq!(report.seed, PILLAR_7_SEED); |
| 218 | + assert_eq!(report.n_paths, 1_000); |
| 219 | + assert_eq!(report.n_hops, 10); |
| 220 | + } |
| 221 | + |
| 222 | + // ── PSD rate meets the 0.999 threshold ─────────────────────────────────── |
| 223 | + |
| 224 | + #[test] |
| 225 | + fn psd_rate_at_or_above_threshold() { |
| 226 | + let report = prove_pillar_7(); |
| 227 | + assert!( |
| 228 | + report.psd_rate >= PILLAR_7_PSD_THRESHOLD, |
| 229 | + "psd_rate={:.6} below threshold={:.6}", |
| 230 | + report.psd_rate, PILLAR_7_PSD_THRESHOLD |
| 231 | + ); |
| 232 | + } |
| 233 | + |
| 234 | + // ── Determinism: two runs with the same seed produce identical results ───── |
| 235 | + |
| 236 | + #[test] |
| 237 | + fn prove_pillar_7_is_deterministic() { |
| 238 | + let r1 = prove_pillar_7(); |
| 239 | + let r2 = prove_pillar_7(); |
| 240 | + assert_eq!(r1.psd_rate.to_bits(), r2.psd_rate.to_bits(), "psd_rate not deterministic"); |
| 241 | + assert_eq!( |
| 242 | + r1.lognorm_concentration.to_bits(), |
| 243 | + r2.lognorm_concentration.to_bits(), |
| 244 | + "lognorm_concentration not deterministic" |
| 245 | + ); |
| 246 | + } |
| 247 | + |
| 248 | + // ── Identity step: sandwich with identity M should leave Σ unchanged ────── |
| 249 | + |
| 250 | + #[test] |
| 251 | + fn sandwich_with_identity_is_noop() { |
| 252 | + let sigma = Spd3::new(2.0, 0.5, 0.3, 3.0, 0.4, 1.5); |
| 253 | + let result = ewa_sandwich_3d(&Spd3::I, &sigma); |
| 254 | + // M = I → Σ' = I · Σ · I = Σ; check within f32 rounding (1e-5). |
| 255 | + assert!((result.a11 - sigma.a11).abs() < 1e-5, "a11 mismatch"); |
| 256 | + assert!((result.a12 - sigma.a12).abs() < 1e-5, "a12 mismatch"); |
| 257 | + assert!((result.a13 - sigma.a13).abs() < 1e-5, "a13 mismatch"); |
| 258 | + assert!((result.a22 - sigma.a22).abs() < 1e-5, "a22 mismatch"); |
| 259 | + assert!((result.a23 - sigma.a23).abs() < 1e-5, "a23 mismatch"); |
| 260 | + assert!((result.a33 - sigma.a33).abs() < 1e-5, "a33 mismatch"); |
| 261 | + } |
| 262 | + |
| 263 | + // ── SPD input + SPD step → SPD output ──────────────────────────────────── |
| 264 | + |
| 265 | + #[test] |
| 266 | + fn sandwich_preserves_spd_for_random_inputs() { |
| 267 | + let mut rng = SplitMix64::new(PILLAR_7_SEED ^ 0xDEAD_BEEF); |
| 268 | + for trial in 0..200 { |
| 269 | + let step_raw = random_contractive_spd3(&mut rng, 0.1); |
| 270 | + let step_spd = array_to_spd3(step_raw); |
| 271 | + let m = step_spd.sqrt(); |
| 272 | + let sigma_raw = random_contractive_spd3(&mut rng, 1.0); |
| 273 | + let sigma = array_to_spd3(sigma_raw); |
| 274 | + let result = ewa_sandwich_3d(&m, &sigma); |
| 275 | + assert!( |
| 276 | + is_psd_eig(&result), |
| 277 | + "trial {trial}: sandwich output not SPD: {:?}", |
| 278 | + result |
| 279 | + ); |
| 280 | + } |
| 281 | + } |
| 282 | + |
| 283 | + // ── eig_sym_3 parity gate vs Spd3::eig (Smith-1961 bit-equivalence) ────── |
| 284 | + // |
| 285 | + // Critical: both `eig_sym_3` (PR-X10 A4, `linalg::eig_sym`) and |
| 286 | + // `splat3d::Spd3::eig` implement the same Smith-1961 algorithm. The |
| 287 | + // parity gate verifies their eigenvalues agree within 1e-5 over 100 |
| 288 | + // random SPD3 matrices drawn with the Pillar-7 SEED, confirming that |
| 289 | + // calling the algorithm from either location produces the same result. |
| 290 | + |
| 291 | + #[cfg(feature = "splat3d")] |
| 292 | + #[test] |
| 293 | + fn parity_eig_sym_3_vs_spd3_eig() { |
| 294 | + let mut rng = SplitMix64::new(PILLAR_7_SEED); |
| 295 | + let mut max_err = 0.0f32; |
| 296 | + |
| 297 | + for trial in 0..100 { |
| 298 | + // Draw a random SPD3 via the contractive helper (always SPD). |
| 299 | + let raw = random_contractive_spd3(&mut rng, 1.0); |
| 300 | + let spd = array_to_spd3(raw); |
| 301 | + |
| 302 | + // Reference: Spd3::eig (Smith-1961 in splat3d/spd3.rs). |
| 303 | + let (ref_l1, ref_l2, ref_l3, _ref_v) = spd.eig(); |
| 304 | + |
| 305 | + // Under test: eig_sym_3 (Smith-1961 in linalg/eig_sym.rs). |
| 306 | + let rows = spd.to_rows(); |
| 307 | + let (l1, l2, l3, _v) = eig_sym_3(&rows); |
| 308 | + |
| 309 | + let err = (l1 - ref_l1).abs().max((l2 - ref_l2).abs()).max((l3 - ref_l3).abs()); |
| 310 | + max_err = max_err.max(err); |
| 311 | + |
| 312 | + assert!( |
| 313 | + err < 1e-5, |
| 314 | + "trial {trial}: eigenvalue parity error = {err:.2e} (want < 1e-5)\n \ |
| 315 | + Spd3::eig = ({ref_l1}, {ref_l2}, {ref_l3})\n \ |
| 316 | + eig_sym_3 = ({l1}, {l2}, {l3})" |
| 317 | + ); |
| 318 | + } |
| 319 | + // Global summary so the log shows the worst-case error. |
| 320 | + assert!( |
| 321 | + max_err < 1e-5, |
| 322 | + "Smith-1961 parity gate: max_err = {max_err:.2e} over 100 trials (want < 1e-5)" |
| 323 | + ); |
| 324 | + } |
| 325 | + |
| 326 | + // ── array_to_spd3 correctly reads the upper triangle ───────────────────── |
| 327 | + |
| 328 | + #[test] |
| 329 | + fn array_to_spd3_upper_triangle() { |
| 330 | + let m = [[1.0f32, 2.0, 3.0], [2.0, 4.0, 5.0], [3.0, 5.0, 6.0]]; |
| 331 | + let s = array_to_spd3(m); |
| 332 | + assert_eq!(s.a11, 1.0); |
| 333 | + assert_eq!(s.a12, 2.0); |
| 334 | + assert_eq!(s.a13, 3.0); |
| 335 | + assert_eq!(s.a22, 4.0); |
| 336 | + assert_eq!(s.a23, 5.0); |
| 337 | + assert_eq!(s.a33, 6.0); |
| 338 | + } |
| 339 | + |
| 340 | + // ── is_psd_eig rejects non-SPD matrices ──────────────────────────── |
| 341 | + |
| 342 | + #[test] |
| 343 | + fn psd_eig_rejects_indefinite() { |
| 344 | + // A matrix with a negative diagonal is clearly not SPD. |
| 345 | + let s = Spd3::new(-1.0, 0.0, 0.0, 1.0, 0.0, 1.0); |
| 346 | + assert!(!is_psd_eig(&s), "Should reject matrix with negative a11"); |
| 347 | + } |
| 348 | + |
| 349 | + #[test] |
| 350 | + fn psd_eig_accepts_identity() { |
| 351 | + assert!(is_psd_eig(&Spd3::I), "Identity must be SPD"); |
| 352 | + } |
| 353 | + |
| 354 | + // ── log_frob is finite for SPD inputs ──────────────────────────────────── |
| 355 | + |
| 356 | + #[test] |
| 357 | + fn log_frob_finite_for_spd() { |
| 358 | + let mut rng = SplitMix64::new(0xABCD_EF01_2345_6789); |
| 359 | + for _ in 0..50 { |
| 360 | + let raw = random_contractive_spd3(&mut rng, 1.0); |
| 361 | + let spd = array_to_spd3(raw); |
| 362 | + let lf = log_frob(&spd); |
| 363 | + assert!(lf.is_finite(), "log_frob returned non-finite: {lf}"); |
| 364 | + } |
| 365 | + } |
| 366 | +} |
0 commit comments