nx_p256_solinas_difftest.nx

nx_p256_solinas_difftest.nx -- DIFFERENTIAL correctness gate for the NIST P-256 Solinas fast reduction used by TLS ECDSA certificate verify. It proves the FAST Solinas reduction (_p256_solinas_reduce, reached via the public p256_field_reduce_solinas) is BIT-IDENTICAL, in every one of the 8 output limbs, to a trivially-correct bit-serial long-division reduction mod p -- over the FULL 512-bit product domain: * >= 2000 deterministic LCG-random 512-bit products (seeded from the loop index; NO Date.now/random -- the .nx runtime forbids them), and * the exact reduction boundary values: 0, p-1, p, p+1, 2p-1, 2p, 2p+1, 3p, 2^256-1, 2^256, (p-1)^2, p^2, p<<256, 2^512-1, 2^512-2, 2^512-1-p. Plus an end-to-end cross-check: p256_field_mul (fast) == p256_field_mul_slow (the retained bit-serial oracle) over random a,b. WHY THIS MATTERS: this reduction is on the cert-verify hot path (p256_field_mul -> point add/double -> scalar mul -> ECDSA verify). A single wrong reduction could let a FORGED signature verify. The test exits 0 ONLY if EVERY input is bit-identical; any mismatch exits 1. ORACLE INDEPENDENCE: the bit-serial oracle here (_dt_oracle_reduce) shares ZERO code with _p256_solinas_reduce except the prime-constant loader p256_field_load_p (both must reduce mod the same p). It is the SAME algorithm p256_field_mul_slow uses for its reduction step; the end-to-end section cross-checks it against p256_field_mul_slow so a faithful transcription is proven, not assumed. NOTE ON PREMISE: the Solinas reduction ALREADY existed and was ALREADY wired into p256_field_mul before this test (commit "ECDSA-P256 §1c"). This organ ADDS a far stronger correctness proof (>= 2000 random + full boundary set) than the pre-existing 606-case oracle test; it modifies no production logic. expect_exit: 0 license_tier: ORIGINAL