Skip to content

test: replace no-value tests with exact oracles (#370) - #403

Merged
thedavidmeister merged 10 commits into
mainfrom
fix/370-oracle
Oct 10, 2026
Merged

thedavidmeister merged 10 commits into
mainfrom
fix/370-oracle

Conversation

@thedavidmeister

@thedavidmeister thedavidmeister commented Oct 9, 2026 •

Copy link
Copy Markdown
Contributor

Closes #370

Replaces the tests that only checked for no revert with exact oracles. Where a value fuzz already covers the value, the test is deleted instead.

  • add: testAddNeverRevert becomes testAddRoundsTheExactSum and testAddRoundsTheExactSumNearbyExponents. They check add's documented rule against the exact 512-bit sum: round to the larger operand's int256 unit, towards zero when the signs agree and away from zero when they differ. A same-signed sum past int256 must land at exponent T+1, rounded towards zero to ten units. This shed value was left out until add: keep the operands' carry when the sum overflows int256 (#394) #414 fixed add's carry, and is now asserted.
  • div: testDivMaxPositiveValueDenominatorNotRevert becomes an exact-quotient truncation oracle. This PR adds a fuzz near the int256 floor and the one-unit-at-the-floor case, because unbounded exponents never reach the window where the quotient sheds digits.
  • pow: 2^1e9 is checked against bc -l at scale 200.
  • packArithmeticResult: int224.max at exponent 2, in place of assertGt(coef, 0).
  • agree: the sub-underflow counterexample asserts its answers: forward is true and backward is false. testAgreeNeverRevertsOnValues is deleted. The no-revert property it stood for is covered by the Rust library_agree proptest (crates/tests) and by testAgreeAcrossTheWholeRange (see G2).
  • Deleted because value fuzzes in the same file cover them: testEqNotReverts, testWithTargetExponentLargerTargetExponentNoRevert, testFracNotReverts, testIntegerNotReverts, testFloorNotReverts, testCeilNotReverts.

No src changes.

QA

  • Discriminating tests: testAddRoundsTheExactSum(NearbyExponents), testDivMaxPositiveValueDenominatorTruncatesTheExactQuotient, testDivMaxPositiveValueDenominatorNearTheFloor, testDivMaxPositiveValueDenominatorOneUnitAtTheFloor, testPowIntegerExponentSquaringOverflow, testPackArithmeticResultToleratesCoefficientTruncation, testAgreeSurvivesTheSubUnderflowCounterexample. Each was probed with mutation-probe against its old version on main 8fcfeb3. The old versions kill only the revert-introducing mutants, and the new versions also kill the value mutants. See the matrix.
  • Mutations applied: 26 src mutants, listed in the matrix below. Each was probed against the touched test file on main and on this branch, and against the old and new test alone. Every mutant is KILLED by its file on this branch.
  • Oracle: exact 512-bit decimal arithmetic in test/lib/LibTestExactDecimal.sol for add and div. bc -l at scale 200 for 2^1e9. The int224 range for pack. Hand arithmetic in units of 1e-2147483648 for the agree counterexample. None of these is derived from the implementation.
  • Category check: test: tests that assert nothing beyond not reverting #370 lists 12 tests. 5 are converted to value assertions (add, div, pow 2^1e9, packArithmeticResult, agree counterexample). 7 are deleted with mutation evidence that their file still kills what they killed (eq, withTargetExponent, frac, integer, floor, ceil, agree never-revert). The add shed value is asserted since the merge of main at 783048c (add: keep the operands' carry when the sum overflows int256 (#394) #414). See "Overflow shed after add: keep the operands' carry when the sum overflows int256 (#394) #414" below.

Columns: old alone is the replaced or deleted test alone on main. new alone is the replacement alone. file main and file branch are the whole test file on each tree.

Mutant old alone new alone file main file branch
A1 zero operand returns the other's exponent survived KILLED KILLED KILLED
A2 swap ignores the shortfall tie-break survived survived¹ KILLED KILLED
A3 early-return boundary > → >= survived KILLED KILLED KILLED
A4 aligned sum off by one unit survived KILLED KILLED KILLED
A5 overflow never detected survived KILLED KILLED KILLED
A6 shed keeps the exponent survived KILLED KILLED KILLED
A7 shed keeps B's digit survived survived² KILLED KILLED
D1 small-divisor scale exponent 75 → 76 survived survived³ KILLED KILLED
D2 scale choice < → <= survived survived³ KILLED KILLED
D3 floor shed one digit short survived KILLED survived KILLED
D4 floor zero cutoff 76 → 75 survived KILLED survived KILLED
P1 coefficient shed lands one below survived KILLED survived KILLED
W1 squaring guard at 1e8 KILLED KILLED KILLED KILLED
W2 top bit dropped for a base in (1e8, 2e8) survived KILLED KILLED KILLED
G1 agree answer negated survived KILLED KILLED KILLED
G2 spread packed, reverting past the Float range survived⁴ survived KILLED KILLED⁴
Q1 eq rescale overflow reverts KILLED deleted KILLED KILLED
T1 larger target past 76 reverts KILLED deleted KILLED KILLED
T2 larger target divides one digit short survived deleted KILLED KILLED
F1 whole-fraction cutoff −76 → −75 survived deleted survived⁵ survived⁵
F2 fraction modulus one digit short survived deleted KILLED KILLED
F3 exponent below −76 reverts KILLED deleted KILLED KILLED
L1 negative integer floored down survived deleted KILLED KILLED
L2 negative fraction at −76 or below reverts KILLED deleted KILLED KILLED
C1 ceil adds ten survived deleted KILLED KILLED
C2 positive fraction at −76 or below reverts KILLED deleted KILLED KILLED
  1. The add oracle stays above the exponent floor, where shortfalls are zero. testAddAtFloor and testAddNearFloorMatchesShifted kill A2.
  2. This is the overflow-shed value. It was left out at the time of this probe, and testAddAtFloor and testAddingSmallToLargeReturnsLargeExamples killed A7. add: keep the operands' carry when the sum overflows int256 (#394) #414 rewrote that branch, so A7's target no longer exists. The table below probes the new branch.
  3. The divisor is fixed at int256.max ≥ 1e76, so the 1e75 scale branch cannot be reached. testDivAdjustExponentFullDivisor, testDivBy1 and others kill D1 and D2.
  4. The deleted testAgreeNeverRevertsOnValues did not kill G2. testAgreeAcrossTheWholeRange, testAgreeExtremeTolerance and the Rust library_agree proptest kill it. A probe with forge build && cargo test -p rain-math-float-tests library_agree as the suite killed both G1 and G2. The agree no-revert deletion relies on library_agree.
  5. At the public surface F1 is equivalent: an int224 coefficient is under 1e76, so at exponent −76 the integer part is zero either way. The unchanged testIntFracExamples and testIntFracNegExponentSmall kill it.

Overflow shed after #414

Merging main at 783048c brought in #414, which keeps add's carry past int256. checkAddRoundsTheExactSum now asserts the value it shed: |result| × 10^78 ≤ |sum| < (|result| + 1) × 10^78, in units of 10^(T-77). That is the exact sum rounded towards zero to ten units at T+1, which is add's NatSpec rule. The comment pointing at #363 is gone.

The S mutants target #414's overflow branch. They were probed with mutation-probe against three suites: the restored tests alone, the add test file on main 783048c, and the add test file on this branch (0afe3dd).

Mutant restored tests alone file main file branch
S1 positive shed drops the carry (A/10 + B/10) KILLED KILLED KILLED
S2 negative shed drops the carry (A/10 + B/10) KILLED KILLED KILLED
S3 negative shed offset +3 → +0 KILLED KILLED KILLED
S4 positive shed rounds away from zero (+9) KILLED KILLED KILLED
S5 negative shed offset +3 → +2 KILLED KILLED KILLED
S6 shed keeps the exponent KILLED KILLED KILLED
S7 overflow never detected KILLED KILLED KILLED

#414's own tests on main already kill every S mutant. The restored assertion also kills all 7 by itself. I did not probe the restored tests with the shed assertion removed, so this table does not separate what the assertion kills from what the rest of the check kills. Full suites at 0afe3dd: forge test passed 836 of 836 and cargo test (crates/tests) passed 152 of 152.

Scan recorded in audit/mutation-test-scans.json.

🤖 Generated with Claude Code

Summary by CodeRabbit

  • Tests
    • Strengthened decimal arithmetic checks to verify expected results, including addition, division, rounding, exponent handling, and agreement comparisons.
    • Removed broad “does not revert” tests that did not verify outcomes.

baku-ccron and others added 6 commits October 9, 2026 13:59
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
The shed case drops the carry against add's NatSpec. Its value is not
asserted until that ruling, rather than absorbed by a two-unit bound.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Unbounded exponents never reach the window where the quotient sheds
digits below the floor.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@coderabbitai

coderabbitai Bot commented Oct 9, 2026 •

Copy link
Copy Markdown
Contributor

Review in Change Stack →

Warning

Review limit reached

You've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository.

Next included review available in 29 minutes.

Check out review usage here.

View limit details

Limit details: You’ve used the included review currently available.

Learn how review limits work.

Review configuration:

⚙️ Run configuration
  • Configuration used: Organization UI
  • Review profile: ASSERTIVE
  • Plan: Advanced
  • Run ID: 38a8c913-40e4-4927-a947-8af425e93033

📥 Commits

Reviewing files that changed from the base of the PR and between 93f0c10 and a413a23.


📒 Files selected for processing (12)
  • audit/mutation-test-scans.json
  • test/src/lib/LibDecimalFloat.agree.t.sol
  • test/src/lib/LibDecimalFloat.ceil.t.sol
  • test/src/lib/LibDecimalFloat.floor.t.sol
  • test/src/lib/LibDecimalFloat.frac.t.sol
  • test/src/lib/LibDecimalFloat.integer.t.sol
  • test/src/lib/LibDecimalFloat.packArithmeticResult.t.sol
  • test/src/lib/LibDecimalFloat.pow.t.sol
  • test/src/lib/implementation/LibDecimalFloatImplementation.add.t.sol
  • test/src/lib/implementation/LibDecimalFloatImplementation.div.t.sol
  • test/src/lib/implementation/LibDecimalFloatImplementation.eq.t.sol
  • test/src/lib/implementation/LibDecimalFloatImplementation.withTargetExponent.t.sol

No actionable comments were generated in the recent review. 🎉

ℹ️ Recent review info
⚙️ Run configuration
  • Configuration used: Organization UI
  • Review profile: ASSERTIVE
  • Plan: Advanced
  • Run ID: cd01d925-3993-4b03-8dfc-3fa0c64394c7


📥 Commits

Reviewing files that changed from the base of the PR and between 8fcfeb3 and 93f0c10.



📒 Files selected for processing (12)
  • audit/mutation-test-scans.json
  • test/src/lib/LibDecimalFloat.agree.t.sol
  • test/src/lib/LibDecimalFloat.ceil.t.sol
  • test/src/lib/LibDecimalFloat.floor.t.sol
  • test/src/lib/LibDecimalFloat.frac.t.sol
  • test/src/lib/LibDecimalFloat.integer.t.sol
  • test/src/lib/LibDecimalFloat.packArithmeticResult.t.sol
  • test/src/lib/LibDecimalFloat.pow.t.sol
  • test/src/lib/implementation/LibDecimalFloatImplementation.add.t.sol
  • test/src/lib/implementation/LibDecimalFloatImplementation.div.t.sol
  • test/src/lib/implementation/LibDecimalFloatImplementation.eq.t.sol
  • test/src/lib/implementation/LibDecimalFloatImplementation.withTargetExponent.t.sol


💤 Files with no reviewable changes (6)
  • test/src/lib/implementation/LibDecimalFloatImplementation.eq.t.sol
  • test/src/lib/LibDecimalFloat.integer.t.sol
  • test/src/lib/implementation/LibDecimalFloatImplementation.withTargetExponent.t.sol
  • test/src/lib/LibDecimalFloat.ceil.t.sol
  • test/src/lib/LibDecimalFloat.floor.t.sol
  • test/src/lib/LibDecimalFloat.frac.t.sol


Included review availability: This review used your included allowance. Your plan provides up to 1 included review per hour; 0 remain after this review.




Walkthrough

This PR updates decimal-float tests to check exact or bounded results for addition, division, agreement, coefficient truncation, and exponentiation. It removes fuzz tests that only checked for non-reversion and adds an audit scan record for Issue #370.

Changes

Decimal-float test assertions

Layer / File(s) Summary
Addition and division oracles
test/src/lib/implementation/LibDecimalFloatImplementation.add.t.sol, test/src/lib/implementation/LibDecimalFloatImplementation.div.t.sol
Addition tests use an exact-sum oracle to check sign, rounding, and related boundary conditions. Division tests check quotient truncation, precision, and cases near the minimum exponent.
Targeted expected-value assertions
test/src/lib/LibDecimalFloat.agree.t.sol, test/src/lib/LibDecimalFloat.packArithmeticResult.t.sol, test/src/lib/LibDecimalFloat.pow.t.sol, audit/mutation-test-scans.json
The agreement counterexample now checks opposite results for the forward and reversed calls. The truncation test checks for type(int224).max, and the 2 ^ 1e9 test checks against a reference value. The scan record lists mutation outcomes and test counts.
Remove assertion-free fuzz tests
test/src/lib/LibDecimalFloat.agree.t.sol, test/src/lib/LibDecimalFloat.ceil.t.sol, test/src/lib/LibDecimalFloat.floor.t.sol, test/src/lib/LibDecimalFloat.frac.t.sol, test/src/lib/LibDecimalFloat.integer.t.sol, test/src/lib/implementation/LibDecimalFloatImplementation.eq.t.sol, test/src/lib/implementation/LibDecimalFloatImplementation.withTargetExponent.t.sol
Removed fuzz tests that called the operations without checking a result or expecting a revert.

Priority: ⬇️ Low

Estimated code review effort: 3 (Moderate) | ~20 minutes

Change: Other

Merge Risk: ⚪ Minimal · up to 93f0c

The reviewed test changes are mergeable after normal checks; no concrete regression remains identified.

🚥 Pre-merge checks | ✅ 4 | ❌ 1

❌ Failed checks (1 warning)

Check name Status Explanation Resolution
Linked Issues check Warning Issue #370 requires an exact mathematical assertion for each listed no-value test, or deletion when an existing value fuzz covers it. The changed tests add exact oracles for add, division, pow, packAr… Resolve the expected behavior under #363, then add an independent exact assertion for the same-signed overflow-shed coefficient in the add oracle. Do not leave this value unasserted while claiming completion of #370.
✅ Passed checks (4 passed)
Check name Status Explanation
Out of Scope Changes check Passed The reported changes are limited to tests for the no-value cases in #370 and to the mutation-scan record that documents their coverage. The changes add mathematical or documented-rule assertions, dele…
Docstring Coverage Passed No functions found in the changed files to evaluate docstring coverage. Skipping docstring coverage check. Docstring coverage is scoped to functions touched by this diff. Analyzed 0 functions across 0…
Description Check Passed Check skipped - CodeRabbit’s high-level summary is enabled.
Title check Passed The title clearly and concisely describes the main change: replacing tests that lacked value assertions with exact oracles. It matches the pull request objectives and changeset.


Full details: Linked Issues check

Explanation

Issue #370 requires an exact mathematical assertion for each listed no-value test, or deletion when an existing value fuzz covers it. The changed tests add exact oracles for add, division, pow, packArithmeticResult, and agree, and delete the tests covered by existing value fuzzes. However, the add oracle explicitly does not assert the coefficient for the same-signed overflow-shed case. It asserts only the shed condition and exponent. The PR description identifies this as pending #363, but #370 remains an active direct requirement and does not exclude this sub-case.




✨ Finishing Touches 💡 1
🛠️ Fix failing CI checks 💡
  • Commit to this branch
  • Create a new PR


🧪 Generate unit tests (beta)
  • Commit to this branch
  • Create a new PR



  • Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

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.

baku-ccron and others added 4 commits October 9, 2026 17:14
Restores the exact overflow-shed assertion in checkAddRoundsTheExactSum now
that #414 keeps add's carry: the shed sum rounds towards zero to ten units.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Resolve onto main's one-helper-per-job LibTestExactDecimal:
- add: testAddRoundsTheExactSum{,NearbyExponents} now assert checkAddExact
  (addPartsWide exact parts) in place of the local bound oracle
  checkAddRoundsTheExactSum; magnitudeAt, sub512 and sameValue (a copy of
  LibTestExactDecimal.eq) are dropped.
- div: checkDivByMaxTruncatesTheExactQuotient asserts the exact parts from
  divParts moved to the call's exponents and atFloor, in place of the
  local truncation bounds.
- audit/mutation-test-scans.json is the jq union of both sides.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@thedavidmeister
thedavidmeister merged commit 1047972 into main Oct 10, 2026
7 of 8 checks passed
@github-actions

Copy link
Copy Markdown

@coderabbitai assess this PR size classification for the totality of the PR with the following criterias and report it in your comment:

S/M/L PR Classification Guidelines:

This guide helps classify merged pull requests by effort and complexity rather than just line count. The goal is to assess the difficulty and scope of changes after they have been completed.

Small (S)

Characteristics:

  • Simple bug fixes, typos, or minor refactoring
  • Single-purpose changes affecting 1-2 files
  • Documentation updates
  • Configuration tweaks
  • Changes that require minimal context to review

Review Effort: Would have taken 5-10 minutes

Examples:

  • Fix typo in variable name
  • Update README with new instructions
  • Adjust configuration values
  • Simple one-line bug fixes
  • Import statement cleanup

Medium (M)

Characteristics:

  • Feature additions or enhancements
  • Refactoring that touches multiple files but maintains existing behavior
  • Breaking changes with backward compatibility
  • Changes requiring some domain knowledge to review

Review Effort: Would have taken 15-30 minutes

Examples:

  • Add new feature or component
  • Refactor common utility functions
  • Update dependencies with minor breaking changes
  • Add new component with tests
  • Performance optimizations
  • More complex bug fixes

Large (L)

Characteristics:

  • Major feature implementations
  • Breaking changes or API redesigns
  • Complex refactoring across multiple modules
  • New architectural patterns or significant design changes
  • Changes requiring deep context and multiple review rounds

Review Effort: Would have taken 45+ minutes

Examples:

  • Complete new feature with frontend/backend changes
  • Protocol upgrades or breaking changes
  • Major architectural refactoring
  • Framework or technology upgrades

Additional Factors to Consider

When deciding between sizes, also consider:

  • Test coverage impact: More comprehensive test changes lean toward larger classification
  • Risk level: Changes to critical systems bump up a size category
  • Team familiarity: Novel patterns or technologies increase complexity

Notes:

  • the assessment must be for the totality of the PR, that means comparing the base branch to the last commit of the PR
  • the assessment output must be exactly one of: S, M or L (single-line comment) in format of: SIZE={S/M/L}
  • do not include any additional text, only the size classification
  • your assessment comment must not include tips or additional sections
  • do NOT tag me or anyone else on your comment

@linear

linear Bot commented Oct 10, 2026

Copy link
Copy Markdown

RAI-3157

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.

test: tests that assert nothing beyond not reverting

1 participant