Skip to content

fix(contracts): main is red on a property that is false for small-variance input - #2460

Open
noahgift wants to merge 1 commit into
mainfrom
fix/layernorm-proptest-eps-precondition
Open

fix(contracts): main is red on a property that is false for small-variance input#2460
noahgift wants to merge 1 commit into
mainfrom
fix/layernorm-proptest-eps-precondition

Conversation

@noahgift

Copy link
Copy Markdown
Contributor

fix(contracts): main is red on a property that is false for small-variance input

workspace-test failed on main at 9b19970:

Test failed: output variance = 0.99547684, expected ~1.0
minimal failing input: v = [-4.983007, -4.9585605, -4.9680285, -5.0763197]

Not a layernorm defect, and not introduced by the audit batches — the file was
last touched by #1545 and none of #2453/#2454/#2457/#2458 changed a line of it.
The arithmetic is exactly right:

LayerNorm divides by sqrt(var_in + eps), so
    var_out = var_in / (var_in + eps)
var_in for that input = 2.2e-3, eps = 1e-5
    2.2e-3 / 2.21e-3 = 0.99548     <- the observed value, to 5 digits

So var_out approaches 1.0 only as var_in grows large relative to eps, and is
BELOW 1.0 for every finite input. The property "output variance is ~1.0 within
1e-3" is simply FALSE once var_in drops near eps. The test was asserting
something untrue and had been waiting for proptest to draw the input that says so.

WHY THE EXISTING GUARD MISSED IT. There was one — it skipped vectors whose RANGE
was under 1e-6. Range is a proxy for the wrong quantity. The failing input had
range 0.12, five orders of magnitude above that guard, while its variance was
only ~220x eps. A guard on a proxy is how a latent flake survives review.

FIX: precondition on the quantity that actually governs the error. From

|1 - var_in/(var_in + eps)| = eps/(var_in + eps) < TOL
=>  var_in > eps/TOL - eps

so prop_assume!(var_in > EPS / TOL). EPS and TOL are now named constants used
by the kernel call, the precondition and the assertion, so changing either cannot
silently re-open the gap — the old code had 1e-5 and 1e-3 as unrelated literals.

VERIFIED:

  • 20 consecutive runs at PROPTEST_CASES=512 (10,240 cases): 0 failures.
  • NOT vacuous, which is the risk a prop_assume introduces. Mutating the kernel
    (denominator scaled by 0.9) turns it RED — "output variance = 0.8099979,
    expected ~1.0 (input variance 3.8552012)" — and restoring turns it GREEN. The
    precondition filters the regime where the property is false, not the inputs
    that would catch a bug.
  • The failure message now prints var_in too, so the next person sees immediately
    which regime they are in.

Refs #2373

…iance input

`workspace-test` failed on main at 9b19970:

    Test failed: output variance = 0.99547684, expected ~1.0
    minimal failing input: v = [-4.983007, -4.9585605, -4.9680285, -5.0763197]

Not a layernorm defect, and not introduced by the audit batches — the file was
last touched by #1545 and none of #2453/#2454/#2457/#2458 changed a line of it.
The arithmetic is exactly right:

    LayerNorm divides by sqrt(var_in + eps), so
        var_out = var_in / (var_in + eps)
    var_in for that input = 2.2e-3, eps = 1e-5
        2.2e-3 / 2.21e-3 = 0.99548     <- the observed value, to 5 digits

So var_out approaches 1.0 only as var_in grows large relative to eps, and is
BELOW 1.0 for every finite input. The property "output variance is ~1.0 within
1e-3" is simply FALSE once var_in drops near eps. The test was asserting
something untrue and had been waiting for proptest to draw the input that says so.

WHY THE EXISTING GUARD MISSED IT. There was one — it skipped vectors whose RANGE
was under 1e-6. Range is a proxy for the wrong quantity. The failing input had
range 0.12, five orders of magnitude above that guard, while its variance was
only ~220x eps. A guard on a proxy is how a latent flake survives review.

FIX: precondition on the quantity that actually governs the error. From

    |1 - var_in/(var_in + eps)| = eps/(var_in + eps) < TOL
    =>  var_in > eps/TOL - eps

so `prop_assume!(var_in > EPS / TOL)`. EPS and TOL are now named constants used
by the kernel call, the precondition and the assertion, so changing either cannot
silently re-open the gap — the old code had 1e-5 and 1e-3 as unrelated literals.

VERIFIED:
- 20 consecutive runs at PROPTEST_CASES=512 (10,240 cases): 0 failures.
- NOT vacuous, which is the risk a prop_assume introduces. Mutating the kernel
  (denominator scaled by 0.9) turns it RED — "output variance = 0.8099979,
  expected ~1.0 (input variance 3.8552012)" — and restoring turns it GREEN. The
  precondition filters the regime where the property is false, not the inputs
  that would catch a bug.
- The failure message now prints var_in too, so the next person sees immediately
  which regime they are in.

Refs #2373
@noahgift
noahgift enabled auto-merge August 13, 2026 17:11
@noahgift
noahgift added this pull request to the merge queue Aug 13, 2026
@github-merge-queue
github-merge-queue Bot removed this pull request from the merge queue due to failed status checks Aug 13, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant