Skip to content

fix(validation): preserve representable recovery metrics - #488

Draft
seonghobae wants to merge 802 commits into
fix/central-hourly-admission-contractfrom
fix/validation-bias-overflow-safe-mean
Draft

fix(validation): preserve representable recovery metrics#488
seonghobae wants to merge 802 commits into
fix/central-hourly-admission-contractfrom
fix/validation-bias-overflow-safe-mean

Conversation

@seonghobae

@seonghobae seonghobae commented Sep 3, 2026

Copy link
Copy Markdown
Contributor

Validation Evidence authority

#488 remains the owner-correct Validation Evidence landing vehicle, stacked on prerequisite #492@794ba9e6dda9f043aa499920fdf609b81b075d7e; protected release authority remains main@a243f18da4a4ca8a8d068c39922537f1f8ed6ad0. Current exact head is c74b7998adf19ea4bcc266726fdeb2f0bab4ed4a. The PR stays Draft/open/mergeable. No force update, destructive rebase, self-approval, gate weakening, coverage exclusion, mutable sibling dependency, or copied provider/scientific-owner logic is used.

Production validation_core::bias_standard_error keeps bounded represented-input exact admission for n=3..=16; n=2 retains its cheaper exact identity and n>16 remains characterization-only under #491. Reusable generalized psychometric arithmetic remains fast-mlsirm-owned.

Current exact-head evidence

c74b7998adf19ea4bcc266726fdeb2f0bab4ed4a completed Documentation Quality 34439763859 GREEN. Rust Foundation 34439763776 completed RED only at authored production line/branch coverage. Repository/Python contracts plus SBOM/provenance, Live PostgreSQL, rustfmt, Clippy, no-retry tests, doctests, warning-free rustdoc, and dependency/license/advisory/source policy are GREEN on this exact head.

Immutable branch artifact 10137604460 (sha256:1e5dbc11a6f606a6db8f9d86099de0d59dc29de28a8e1b6261cfa7235a59d8f7) folds under the checked-in crates/*/src/* unique-source/max rule to 4,458/4,480, 22 missing arms, all in crates/validation_core/src/bias.rs. Immutable line artifact 10137570220 (sha256:c745f4119fda6c07c3907e78a68b46a3a24e145e1c2f7b3fc164ab92cafa04dc) keeps the authored-line gate RED. The predecessor c1c136d... was 4,459/4,482, 23 missing; the source-invariant repair therefore produced the exact denominator-honest delta expected: total -2, covered -1, missing -1.

c74b7998... removes only the unreachable three-level call-site branch around exact_subnormal_rational_scale(exact_root, 1, 3). Reaching that direct path proves a positive exactly represented binary64 radicand and an exactly represented root. Any positive represented radicand is at least 2^-1074, hence exact_root >= 2^-537; dividing that root by 3 remains vastly above minimum normal 2^-1022. The shared helper remains intact for the genuinely reachable two-level rational-scale subnormal path.

Coverage attribution corrections retained

The retained bias_two_level_non_square_count_factor_contract.rs is useful ordinary n=4 regression evidence but did not reduce the branch frontier. Exact source mapping shows missing coordinate (145,12)-(145,44) is specifically denominator > usize::MAX as u128; the preceding non-square numerator/denominator predicates were already exercised.

Likewise the retained minimum-subnormal normalized-three-level regression is valid false-zero/permutation evidence, but missing (340,15)-(340,42) maps to !standard_error.is_finite(), not standard_error.is_subnormal(). The subnormal admission-refusal branch itself is already exercised. Coverage coordinates are assigned meaning only after mapping against the exact source head.

Next causal source frontier

On c74b7998..., normalized three-level admission gives max(|a|,|b|) in [1,2) after exact power-of-two scaling. The positive-definite quadratic a²+b²-ab is therefore at least 3/4 and below 12, so the correctly rounded normalized sqrt(radicand)/3 is positive finite and strictly below 2/sqrt(3). The scale is a finite power of two no larger than 2^1023; multiplication by a positive factor below 1.155 therefore cannot overflow binary64. Consequently !standard_error.is_finite() at the normalized three-level tail is structurally unreachable. A minimal follow-up may remove only that non-finite predicate while retaining the separate false-zero guard until its subnormal-grid lower bound is independently proved.

The line-145 denominator > usize::MAX predicate is not removed yet. Its reachability depends on the supported target integer width; current 64-bit runners make it redundant after the u128 bounds, but repository support for narrower targets must be resolved before source deletion.

General translated-path dispersion and final-result guards require analogous upstream-bound proofs rather than manufactured payloads.

Review / foundation / release boundary

Fresh review enumeration has historical COMMENTED submissions only and zero inline review threads; no qualifying current-head approval exists. Organization ruleset 18156473 requires one approving review, stale-review dismissal after push, review-thread resolution, central required workflows, and non-fast-forward protection.

#492 remains Draft/open/mergeable at exact 794ba9e6dda9f043aa499920fdf609b81b075d7e, stacked on protected main@a243f18da4a4ca8a8d068c39922537f1f8ed6ad0. TEPP and contextual-orchestrator currently expose no GitHub release; TEPP does not copy unpublished provider routing/credentials/model selection or consume mutable contextual-orchestrator source as production authority.

Before protected merge or any n>16 activation, require one exact current head with owned-production 100% authored line+branch coverage, current security/documentation/review gates, truthful route telemetry, release CPU/allocator/RSS evidence, code-current TRACEABILITY/product-technical-gap authority, and qualifying independent review.

@coderabbitai

coderabbitai Bot commented Sep 3, 2026

Copy link
Copy Markdown

Important

Draft PR not reviewed

Draft PRs are not automatically reviewed by default.

  • Trigger a manual review

To automatically review draft PRs, update your CodeRabbit configuration:

reviews:
  auto_review:
    drafts: true

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

Comment @coderabbitai help to get the list of available commands.

@seonghobae seonghobae changed the title fix(validation): preserve representable extreme bias fix(validation): preserve representable recovery metrics Sep 3, 2026
seonghobae added a commit that referenced this pull request Sep 4, 2026
Non-force restack of PR #488 onto protected main after #490. Preserves the complete Validation Evidence lineage while inheriting the centralized hourly-development workflow unchanged.

seonghobae commented Sep 9, 2026

Copy link
Copy Markdown
Contributor Author

Exact-head repair finding — normalized radicand finiteness is unreachable

Fresh exact-head review of 4af3205bba376930d682b356701d79889bef87f7 and branch-coverage artifact 10124083878 confirms the next missing production arm at crates/validation_core/src/bias.rs coordinate (320,8)-(320,40) is !normalized_radicand.is_finite() (true=0, false=6). This should not receive a manufactured payload.

The source-order invariant is sufficient to remove that predicate while retaining the following subtraction_roundoff(...) != 0.0 refusal:

  • normalized_three_level_standard_error has no independent external/direct-test call surface; production reaches it only from exact_three_level_standard_error after two distinct nonzero finite offsets have been established.
  • exact_power_of_two_scale(max_magnitude) returns the positive finite leading-binade power for that positive finite maximum. Each nonzero normalized offset is therefore finite with magnitude < 2; zero-underflow cases are handled earlier.
  • Consequently each normalized square has magnitude < 4 and the normalized cross-product has magnitude < 4. The square-sum is finite and < 8; its exact-addition/roundoff proof is retained.
  • Therefore normalized_square_sum - normalized_cross_product has finite magnitude < 12; it cannot be NaN or infinity. The finiteness branch encodes no reachable scientific state. The subsequent subtraction-roundoff predicate remains the actual admission proof and must stay fail-closed.

Chosen repair: remove only !normalized_radicand.is_finite() || and adjust the adjacent comment to document the <12 bound. The exact source delta is:

     let normalized_radicand = normalized_square_sum - normalized_cross_product;
-    if !normalized_radicand.is_finite()
-        || subtraction_roundoff(
-            normalized_square_sum,
-            normalized_cross_product,
-            normalized_radicand,
-        ) != 0.0
-    {
+    // The admitted normalized square sum has magnitude below 8 and the
+    // normalized cross-product below 4, so this subtraction is finite. Keep the
+    // error-free subtraction proof as the actual exact-admission boundary.
+    if subtraction_roundoff(
+        normalized_square_sum,
+        normalized_cross_product,
+        normalized_radicand,
+    ) != 0.0
+    {
         return Ok(None);
     }

Do not change formulae, route order, coverage denominator, tests, or fallback behavior.

Not chosen: removing or forcing coverage of the preceding normalized cross-product FMA predicate (302,12)-(302,89). Its missing true outcome remains unresolved because subnormal FMA residual rounding can erase an exact product error; a complete representability proof is required before simplifying that guard.

Acceptance for the source repair remains exact-head only: rustfmt/Clippy/no-retry tests/doctest/rustdoc/dependency policy, repository/Python and Live PostgreSQL must stay GREEN, and unique-source branch coverage must show denominator-honest removal of one two-outcome predicate with missing coverage decreasing by one. Predecessor artifacts are not transferable evidence.

Copy link
Copy Markdown
Contributor Author

Exact-head source repair pushed as 870248b54ceaea833e6c008de7c752f467614d16 (refactor(validation): remove unreachable normalized radicand finiteness guard), ordinary fast-forward from 4af3205... and still stacked on #492@794ba9e6dda9f043aa499920fdf609b81b075d7e.

The diff is intentionally limited to crates/validation_core/src/bias.rs: remove only !normalized_radicand.is_finite() and retain the subtraction_roundoff(...) != 0.0 exactness proof. Source-order bound: exact power-of-two normalization leaves admitted magnitudes <2; admitted exact squares/cross-product therefore have magnitude <4; the square sum has already passed exact-addition admission and is finite <8; subtracting the cross-product remains finite with magnitude <12. A non-finite normalized radicand is therefore not a reachable state at this point, while subtraction roundoff remains a real refusal mode.

4af3205... -> 870248b... is exactly one commit, one file, +9/-6; commit diff confirms no arithmetic/formula/admission/dependency/coverage-denominator change beyond removing that impossible predicate and adding the invariant comment. Documentation Quality 34410155982 is GREEN. Rust Foundation 34410155960 is currently queued, so no coverage-count reduction or exact-head Rust GREEN is claimed yet. Preserve Draft state and do not merge on predecessor evidence.

Copy link
Copy Markdown
Contributor Author

Predecessor repair 870248b54ceaea833e6c008de7c752f467614d16 now has complete exact-head evidence. Documentation Quality 34410155982 is GREEN; Rust Foundation 34410155960 is RED only at the owned-production line/branch 100% gates. Repository/Python contracts + SBOM/provenance, Live PostgreSQL, fmt, Clippy, no-retry tests, doctests, warning-free rustdoc, and dependency/license/advisory/source policy are GREEN.

Immutable branch artifact 10127073952 (sha256:2cd258ed06bf767c8a076db641ea1a3c705b8e5ba46dfd1a2801f4c7257e7c04) folds under the checked-in unique-source max semantics to 4,456/4,484, 28 uncovered arms, all in crates/validation_core/src/bias.rs. Parent 4af3205... was 4,457/4,486, 29 uncovered. Removing the impossible normalized-radicand finiteness predicate therefore produced the denominator-honest expected delta: total arms 4486→4484, covered 4457→4456, missing 29→28.

The next exact head is now c52d7058eb0d9499b936bcc86108c8860888338b (test(validation): cover normalized cross-product roundoff fallback), one ordinary fast-forward commit adding only bias_normalized_three_level_cross_product_roundoff_contract.rs. The public n=3 witness uses residuals [0, 1.5·2^600, nextafter(1,+∞)]: neutral-zero exact proof exceeds the bounded coefficient width and pairwise subtraction is inexact; normalized fallback has an underflowed minor square whose fused residual also rounds to zero, but a normal inexact cross-product with nonzero FMA residual. This targets the previously missing normalized cross-product exactness true arm without changing production arithmetic. Current-head CI is queued, so no causal coverage reduction is claimed yet.

Copy link
Copy Markdown
Contributor Author

Exact-head evidence for c52d7058eb0d9499b936bcc86108c8860888338b is now terminal. Documentation Quality 34410872962 is GREEN. Rust Foundation 34410872788 is RED only at owned-production 100% line/branch coverage; repository/Python contracts + SBOM/provenance, Live PostgreSQL, fmt, Clippy, no-retry tests, doctests, warning-free rustdoc, and dependency/license/advisory/source policy are GREEN.

Immutable branch artifact 10127356920 (sha256:e459c985ee41e8e4c06c10c1028b15d40e430364c918bdb6a39b153de430e32f) folds to 4,457/4,484, 27 uncovered arms, all in crates/validation_core/src/bias.rs. Predecessor 870248b... was 4,456/4,484, 28 uncovered. Target normalized cross-product exactness predicate (302,12)-(302,89) moved from (true=0,false=8) to (true=2,false=8). The public regression is therefore causal and keeps production arithmetic unchanged.

Fresh source-order review identifies the next repair candidate in exact_three_level_standard_error: !cross_product.is_finite() is evaluated only after first_square and second_square were both finite. For finite offsets, |x·y| <= max(x²,y²) in exact real arithmetic. A binary64 square that returned finite is below the same finite-to-infinity rounding threshold, so the cross-product cannot newly overflow after both square predicates were false. The current artifact confirms this third range predicate remains one-sided (true=0,false=14). This is an unreachable-state/source-model finding, not a payload target; preserve the reachable zero-product underflow predicates and the later FMA exactness proofs.

seonghobae commented Sep 9, 2026

Copy link
Copy Markdown
Contributor Author

2026-09-10 exact-head repair evidence

Live #488 head is c9c9ff0e2f9375d1d664807869bfddce9b2a3dfe on unchanged prerequisite #492@794ba9e6dda9f043aa499920fdf609b81b075d7e; the PR remains Draft/open/mergeable. The PR body head is stale, so this comment is the newer exact-head authority.

Predecessor c52d7058eb0d9499b936bcc86108c8860888338b had Documentation Quality GREEN (34410872962). Rust Foundation 34410872788 was RED only at owned-production line/branch coverage; repository/Python contracts + SBOM/provenance, fmt, Clippy, no-retry tests, doctests, rustdoc/dependency policy, and Live PostgreSQL were GREEN. Immutable branch artifact 10127356920 (sha256:e459c985ee41e8e4c06c10c1028b15d40e430364c918bdb6a39b153de430e32f) folds under checked-in unique-source max semantics to 4,457/4,484, leaving 27 uncovered arms, all in crates/validation_core/src/bias.rs. Target raw-radicand roundoff coordinate (395,8)-(395,72) was (true=0,false=6).

The first candidate 6fdb68f2f36857e577e38188f8b62103479134a6 used directly represented residuals [0,2^26,-(2^26-1)]. Source-order verification showed why it could not be causal: the public API is bias_se::bias_standard_error, whose bounded n=3..=16 neutral-zero exact proof can admit that small exact integer geometry before bias.rs is reached. Immutable branch artifact 10127927356 (sha256:a7e36d378b8e3a63fec849e9b9618930cb2421e440c53a6bfddea716602e0c8d) confirms the falsification exactly: 4,457/4,484, 27 uncovered, target still (true=0,false=6). Its line artifact also left the target return Ok(None) body at zero executions. The non-causal witness was repaired rather than counted as progress.

Current c9c9ff0e... (test(validation): route raw radicand fallback causally) changes only that public witness. It uses recovered=[1,1,1] and truth=[0,-A,+B], where A=2^26·2^-80=2^-54 and B=(2^26-1)·2^-80. Public subtraction rounds all three residual high parts to 1.0 but retains error-free low terms [0,+A,-B]; nonzero subtraction roundoff makes bias_se refuse and routes the low-term geometry into the production bias fallback. There , , A·B, and A²+B² are exact, while the radicand coefficient 13,510,798,680,784,897 is odd and above 2^53, so exact three-level admission must refuse specifically at the raw radicand subtraction-roundoff proof. The represented fallback result is pinned to correctly rounded bits 0x3c8279a74340fe34, with a permutation invariant.

Exact-head verification is now complete. Documentation Quality 34413059482 is GREEN. Rust Foundation 34413059718 is terminal RED only because owned-production authored coverage remains below 100%; repository/Python contracts + SBOM/provenance, fmt, Clippy, no-retry tests, doctests, warning-free rustdoc/dependency policy, and Live PostgreSQL are GREEN. Current line artifact 10128050213 (sha256:0ece6b49ef8f82a3493773b1fd2957335e51b36580fc0c31a5a2f6beb6482ab5) executes the raw-radicand refusal body twice, versus zero on 6fdb68f2.... Current branch artifact 10128093062 (sha256:3c2fde46707f6fc2be2f3853dcf1517dd6217b451b68aa8f952a6a3657d80e91) folds to 4,458/4,484, 26 uncovered arms, all in bias.rs; target (395,8)-(395,72) is now (true=2,false=6). This is a verified causal coverage repair: missing arms 27→26 without changing production arithmetic, route order, admission bounds, dependencies, fixtures, or coverage denominator/exclusions.

Fresh review enumeration has COMMENTED submissions only and zero inline review threads. Ruleset 18156473 remains active with one required approval, stale-review dismissal on push, thread resolution, central required workflows, deletion protection, and non-fast-forward protection. No bypass/self-approval/force update was used. Protected main remains a243f18da4a4ca8a8d068c39922537f1f8ed6ad0. TEPP and contextual-orchestrator still publish no GitHub releases, so no unpublished CO/provider-routing source was consumed.

Copy link
Copy Markdown
Contributor Author

Coverage RED candidate on exact head bd3506b793d7bcb0ed82ab11284761d4516f1742 (not yet GREEN evidence): added public contract bias_raw_three_level_cross_product_roundoff_contract.rs for the still-missing raw three-level cross-product FMA arm (380,12)-(380,70) from predecessor artifact 10129093190.

The represented sample is [0, x, y] with x = f64::from_bits(0x1e5f_ffff_fffe_7961) (just below 2^-537) and y = f64::from_bits(0x21f8_0000_0000_0000) (1.5 * 2^-480). On IEEE-754 binary64, rounds to the minimum positive subnormal and its FMA residual rounds to signed zero; is exact. The raw x*y is normal, while fma(x, y, -(x*y)) = -8 * 2^-1074, so the third product exactness predicate must refuse rather than treating the rounded cross-product as authoritative. Exact sample geometry gives SE(mean)^2=(x²+y²-xy)/9, whose correctly rounded binary64 result is 2^-481 (0x21e0_0000_0000_0000); the public test also checks permutation invariance.

This candidate intentionally tests the earlier unresolved subnormal-FMA concern rather than deleting the predicate. Current workflows 34419357958 (Rust Foundation) and 34419358033 (Documentation Quality) are queued. Do not transfer predecessor coverage or claim the arm closed until an immutable exact-head artifact changes the unique-source/max count.

Copy link
Copy Markdown
Contributor Author

Exact-head repair note (2026-09-10): predecessor ba9d285f6514ba68f502dde777474fe68c3ca896 added bias_normalized_three_level_subnormal_restore_contract.rs, but its immutable branch artifact 10131921920 (sha256:d586fd5c7c20a82ff76067f8b55e7001963651acbed521c235b78ce1c5fc081e) still folds under the repository unique-source/max rule to 4,458/4,482 covered arms, 24 missing, all in crates/validation_core/src/bias.rs. That test is retained as a useful regression, but it is not causal coverage evidence and must not be reported as 24 -> 23.

Current head 41634596d43ad394fec24cb9d947d7f06d7d2f4e adds a public represented-input witness for the actually missing combined-translation overflow arm. With u=2^968, the observation pairs produce exact residual coefficients [2^54+1, -3*2^54+5, 0]; rounded residual highs remain finite, but one anchor-relative high delta is f64::MAX while its exact low-term delta is 2^970, so high_delta + low_delta overflows and translated_residuals_from_anchor must refuse that anchor. The exact pair-distance numerator is 8_437_482_395_119_093_815_498_145_966_063_658; SE(mean)^2=P*u^2/18 correctly rounds to 0x7fd33ac782eb914d. The contract also checks permutation invariance and does not change production arithmetic, admission bounds, source exclusions, or the coverage denominator.

Documentation Quality 34424767393 is terminal GREEN on 41634596.... Rust Foundation 34424767437 is currently queued, so no exact-head Rust GREEN or causal 24 -> 23 coverage claim is made yet. Re-read its immutable branch artifact before the next source mutation.

Copy link
Copy Markdown
Contributor Author

Exact-head follow-up on 2ff249eb143fe572e7dc64bc3a97896aed4e72c1 adds one public Validation Evidence contract only: bias_translated_false_zero_rejection_contract.rs.

Witness: with u = 2^-1074, represented residuals [0, u, u, 2u] admit canonical translation [-u, 0, 0, u]. Their exact SE(mean) = sqrt(1/6) * u is strictly positive but below the half-minimum-subnormal rounding boundary. The bounded n=4 pair-distance proof seeds a zero candidate and therefore refuses; the general translated path must then reject the false-zero result rather than report perfect recovery. The permuted sample is required to fail identically.

This targets the currently missing general translated-path false-zero predicate around current bias.rs line 593. Predecessor immutable branch authority remains 10137604460 (4,458/4,480, 22 missing arms). No coverage decrease is claimed until an immutable artifact from this exact head proves it. Current-head Documentation Quality 34443713575 and Rust Foundation 34443713596 are queued. Production arithmetic, exact-proof sample budget, denominator/exclusion policy, fast-mlsirm ownership, and #492/CO dependency boundaries are unchanged.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant