Skip to content

Commit 12dbb3a

Browse files
Merge pull request #235 from rainlanguage/2026-06-13-issue-145
test: fuzz mantissa4
2 parents 73b17a3 + 1056ee3 commit 12dbb3a

1 file changed

Lines changed: 262 additions & 0 deletions

File tree

test/src/lib/implementation/LibDecimalFloatImplementation.internals.t.sol

Lines changed: 262 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -125,6 +125,268 @@ contract LibDecimalFloatImplementationInternalsTest is LogTest {
125125
assertEq(scale, 1);
126126
}
127127

128+
/// Exponent exactly -4: the coefficient is already the first 4 mantissa
129+
/// digits, so it is returned verbatim with no interpolation and unit scale,
130+
/// for any coefficient.
131+
function testMantissa4FuzzExponentMinus4(int256 signedCoefficient) external pure {
132+
(int256 idx, bool interpolate, int256 scale) = LibDecimalFloatImplementation.mantissa4(signedCoefficient, -4);
133+
assertEq(idx, signedCoefficient);
134+
assertFalse(interpolate);
135+
assertEq(scale, 1);
136+
}
137+
138+
/// Exponent in [-3, -1]: the coefficient is scaled UP to 4 digits by
139+
/// multiplying by 10^(4 + exponent). Never interpolates, unit scale.
140+
/// The coefficient is bounded so the scaled value stays in int256 range,
141+
/// matching the realistic fractional-part domain (its magnitude is always
142+
/// strictly less than 10^(-exponent)).
143+
function testMantissa4FuzzExponentMinus3ToMinus1(int256 signedCoefficient, int256 exponent) external pure {
144+
exponent = bound(exponent, -3, -1);
145+
// forge-lint: disable-next-line(unsafe-typecast)
146+
int256 factor = int256(10 ** uint256(4 + exponent));
147+
// Keep signedCoefficient * factor within int256 to avoid overflow that
148+
// the production code tolerates via `unchecked`.
149+
signedCoefficient = bound(signedCoefficient, type(int256).min / factor, type(int256).max / factor);
150+
151+
(int256 idx, bool interpolate, int256 scale) =
152+
LibDecimalFloatImplementation.mantissa4(signedCoefficient, exponent);
153+
assertEq(idx, signedCoefficient * factor);
154+
assertFalse(interpolate);
155+
assertEq(scale, 1);
156+
}
157+
158+
/// Exponent >= 0: there is no fractional mantissa to look up, so the index
159+
/// is always 0 with no interpolation and unit scale, for any coefficient.
160+
function testMantissa4FuzzExponentNonNegative(int256 signedCoefficient, int256 exponent) external pure {
161+
exponent = bound(exponent, 0, type(int256).max);
162+
(int256 idx, bool interpolate, int256 scale) =
163+
LibDecimalFloatImplementation.mantissa4(signedCoefficient, exponent);
164+
assertEq(idx, 0);
165+
assertFalse(interpolate);
166+
assertEq(scale, 1);
167+
}
168+
169+
/// Exponent in [-80, -5]: the coefficient is scaled DOWN to its first 4
170+
/// digits by truncating division against scale = 10^(-(exponent + 4)).
171+
/// Interpolation is required exactly when that division was lossy, i.e.
172+
/// rescaled * scale != signedCoefficient.
173+
function testMantissa4FuzzExponentMinus80ToMinus5(int256 signedCoefficient, int256 exponent) external pure {
174+
exponent = bound(exponent, -80, -5);
175+
// forge-lint: disable-next-line(unsafe-typecast)
176+
int256 scale = int256(10 ** uint256(-(exponent + 4)));
177+
int256 expectedRescaled = signedCoefficient / scale;
178+
bool expectedInterpolate = expectedRescaled * scale != signedCoefficient;
179+
180+
(int256 idx, bool interpolate, int256 resultScale) =
181+
LibDecimalFloatImplementation.mantissa4(signedCoefficient, exponent);
182+
assertEq(idx, expectedRescaled);
183+
assertEq(interpolate, expectedInterpolate);
184+
assertEq(resultScale, scale);
185+
}
186+
187+
/// Exponent < -80: the value is below the resolution of the 4-digit
188+
/// mantissa, so the index collapses to 0 with unit scale. Interpolation is
189+
/// flagged for any non-zero coefficient (there is some lost magnitude) and
190+
/// not for zero.
191+
function testMantissa4FuzzExponentBelowMinus80(int256 signedCoefficient, int256 exponent) external pure {
192+
exponent = bound(exponent, type(int256).min, -81);
193+
(int256 idx, bool interpolate, int256 scale) =
194+
LibDecimalFloatImplementation.mantissa4(signedCoefficient, exponent);
195+
assertEq(idx, 0);
196+
assertEq(interpolate, signedCoefficient != 0);
197+
assertEq(scale, 1);
198+
}
199+
200+
// -- mantissa4 adversarial boundary tests --
201+
//
202+
// These tests do NOT mirror the production arithmetic. Each one pins a
203+
// concrete, hand-derived (idx, interpolate, scale) triple, or asserts an
204+
// independent safety invariant, so that an internal mutation that the
205+
// production-faithful fuzz tests would silently track is still caught.
206+
207+
// int224 / int32 boundary constants (the real domain of a packed Float).
208+
int256 internal constant INT224_MAX = (int256(1) << 223) - 1;
209+
int256 internal constant INT224_MIN = -(int256(1) << 223);
210+
211+
/// Exponent exactly -4 is its own branch (`exponent == -4`), distinct from
212+
/// the neighbouring branches. Pin the exact int224 boundary coefficients so a
213+
/// mutant that widens/narrows the `== -4` check (e.g. to `<= -4` swallowing
214+
/// the scale branch, or `>= -4` swallowing the [-3,-1] branch) is caught: at
215+
/// -4 the coefficient passes through verbatim, scale 1, never interpolates.
216+
function testMantissa4ExponentMinus4BoundaryCoefficients() external pure {
217+
int256[4] memory coeffs = [INT224_MAX, INT224_MIN, int256(1), int256(-1)];
218+
for (uint256 i = 0; i < coeffs.length; i++) {
219+
(int256 idx, bool interpolate, int256 scale) = LibDecimalFloatImplementation.mantissa4(coeffs[i], -4);
220+
assertEq(idx, coeffs[i]);
221+
assertFalse(interpolate);
222+
assertEq(scale, 1);
223+
}
224+
}
225+
226+
/// The `exponent < -80` vs `>= -80` split is load-bearing: at -80 the scale
227+
/// is 10^76 (the largest power of ten that still fits in int256), at -81 it
228+
/// would be 10^77 which overflows int256 to a NEGATIVE number and corrupts
229+
/// the division. Pin both sides with concrete values so a mutant moving the
230+
/// bound (`< -80` -> `< -81`, `<= -80`, etc.) is killed deterministically
231+
/// rather than only probabilistically by the fuzzers.
232+
function testMantissa4ExponentMinus80IsScaleBranch() external pure {
233+
// -80 is INSIDE the scale branch: scale = 10^76. Note 10^76 is the
234+
// largest power of ten below int256.max, so the only single-digit
235+
// exact multiples that still fit are 1..5 (6 * 10^76 > int256.max).
236+
int256 scale76 = int256(10 ** 76);
237+
// A coefficient that divides exactly: 5 * 10^76 -> idx 5, no interpolation.
238+
(int256 idx, bool interpolate, int256 scale) = LibDecimalFloatImplementation.mantissa4(5 * scale76, -80);
239+
assertEq(idx, 5);
240+
assertFalse(interpolate);
241+
assertEq(scale, scale76);
242+
243+
// One above an exact multiple -> truncates -> interpolate.
244+
(idx, interpolate, scale) = LibDecimalFloatImplementation.mantissa4(5 * scale76 + 1, -80);
245+
assertEq(idx, 5);
246+
assertTrue(interpolate);
247+
assertEq(scale, scale76);
248+
}
249+
250+
/// -81 is INSIDE the below-resolution branch: idx collapses to 0, scale 1,
251+
/// interpolate iff coefficient != 0. If the `< -80` bound were widened to
252+
/// include -81 in the scale branch, scale would be 10^77 (negative int256)
253+
/// and idx would be a nonzero garbage value, failing these assertions.
254+
function testMantissa4ExponentMinus81IsBelowResolution() external pure {
255+
(int256 idx, bool interpolate, int256 scale) = LibDecimalFloatImplementation.mantissa4(INT224_MAX, -81);
256+
assertEq(idx, 0);
257+
assertTrue(interpolate);
258+
assertEq(scale, 1);
259+
260+
(idx, interpolate, scale) = LibDecimalFloatImplementation.mantissa4(0, -81);
261+
assertEq(idx, 0);
262+
assertFalse(interpolate);
263+
assertEq(scale, 1);
264+
}
265+
266+
/// The truncation-vs-interpolate flag at the exact edge of the scale branch.
267+
/// exponent -5 -> scale 10. A coefficient that is an exact multiple of 10
268+
/// must NOT interpolate; one digit above it MUST interpolate. This pins the
269+
/// `rescaled * scale != signedCoefficient` predicate independently of how
270+
/// production computes it (a flipped comparison or a wrong rounding mode
271+
/// breaks exactly one of the two assertions).
272+
function testMantissa4TruncationFlagEdgeMinus5() external pure {
273+
// 50000e-5 = 0.5 exactly -> idx 5000, no interpolation.
274+
(int256 idx, bool interpolate, int256 scale) = LibDecimalFloatImplementation.mantissa4(50000, -5);
275+
assertEq(idx, 5000);
276+
assertFalse(interpolate);
277+
assertEq(scale, 10);
278+
279+
// 50001e-5 has a fifth significant digit -> truncates -> interpolate.
280+
(idx, interpolate, scale) = LibDecimalFloatImplementation.mantissa4(50001, -5);
281+
assertEq(idx, 5000);
282+
assertTrue(interpolate);
283+
assertEq(scale, 10);
284+
}
285+
286+
/// Negative coefficients in the scale branch must truncate toward zero (as
287+
/// Solidity integer division does) and flag interpolation on any remainder.
288+
/// -50001e-5 -> idx -5000 (truncated toward zero), interpolate true.
289+
function testMantissa4NegativeTruncationMinus5() external pure {
290+
(int256 idx, bool interpolate, int256 scale) = LibDecimalFloatImplementation.mantissa4(-50001, -5);
291+
assertEq(idx, -5000);
292+
assertTrue(interpolate);
293+
assertEq(scale, 10);
294+
295+
(idx, interpolate, scale) = LibDecimalFloatImplementation.mantissa4(-50000, -5);
296+
assertEq(idx, -5000);
297+
assertFalse(interpolate);
298+
assertEq(scale, 10);
299+
}
300+
301+
/// int256.min in the scale branch: division never overflows (scale is always
302+
/// positive so `int256.min / scale` is safe), `rescaled * scale` cannot
303+
/// overflow because its magnitude is <= |int256.min|, and the lost low digit
304+
/// forces interpolate = true. Independent oracle: int256.min is not a
305+
/// multiple of 10, so truncation is always lossy here.
306+
function testMantissa4Int256MinScaleBranch() external pure {
307+
int256 scale10 = 10;
308+
(int256 idx, bool interpolate, int256 scale) = LibDecimalFloatImplementation.mantissa4(type(int256).min, -5);
309+
assertEq(idx, type(int256).min / scale10);
310+
assertTrue(interpolate);
311+
assertEq(scale, scale10);
312+
// Safety: idx really is the truncated quotient and reconstructing loses
313+
// the low digit (proving the interpolate flag is justified).
314+
assertTrue(idx * scale10 != type(int256).min);
315+
}
316+
317+
/// The [-3,-1] branch scales UP exactly (factor is a power of ten), so it
318+
/// must never interpolate and the result must be exactly divisible back by
319+
/// the factor. Pin the two endpoints -1 and -3, and the -4/-5 neighbours to
320+
/// guard the branch's lower edge.
321+
function testMantissa4ScaleUpBranchExact() external pure {
322+
// exponent -1 -> factor 10^3 = 1000. 7e-1 = 0.7 -> mantissa 7000.
323+
(int256 idx, bool interpolate, int256 scale) = LibDecimalFloatImplementation.mantissa4(7, -1);
324+
assertEq(idx, 7000);
325+
assertFalse(interpolate);
326+
assertEq(scale, 1);
327+
328+
// exponent -3 -> factor 10^1 = 10. 123e-3 = 0.123 -> mantissa 1230.
329+
(idx, interpolate, scale) = LibDecimalFloatImplementation.mantissa4(123, -3);
330+
assertEq(idx, 1230);
331+
assertFalse(interpolate);
332+
assertEq(scale, 1);
333+
}
334+
335+
/// The `exponent >= 0` branch: zero index, no interpolation, unit scale, even
336+
/// at the int32 / int256 exponent extremes and the int224 coefficient bounds.
337+
/// A mutant turning `>= 0` into `> 0` would push exponent 0 into the [-3,-1]
338+
/// else-branch, where it would multiply by 10^4 and (for a nonzero
339+
/// coefficient) return a nonzero idx, failing the exponent-0 assertion.
340+
function testMantissa4NonNegativeBoundaries() external pure {
341+
int256[3] memory exps = [int256(0), int256(type(int32).max), type(int256).max];
342+
for (uint256 i = 0; i < exps.length; i++) {
343+
(int256 idx, bool interpolate, int256 scale) = LibDecimalFloatImplementation.mantissa4(INT224_MAX, exps[i]);
344+
assertEq(idx, 0);
345+
assertFalse(interpolate);
346+
assertEq(scale, 1);
347+
}
348+
}
349+
350+
/// Independent safety invariant across the entire negative-exponent domain:
351+
/// whenever the function reports `interpolate == false`, the reported idx
352+
/// MUST losslessly reconstruct the input at the reported scale
353+
/// (idx * scale == signedCoefficient for the scale branch, idx == sc * factor
354+
/// implies exact for the others). Conversely, the value the mantissa stands
355+
/// for must be recoverable. This is the property the pow10 caller relies on:
356+
/// a false interpolate flag is a promise of exactness. Fuzzed across the
357+
/// realistic int224 coefficient / int32-style exponent domain.
358+
function testMantissa4InterpolateFalseImpliesExact(int256 signedCoefficient, int256 exponent) external pure {
359+
signedCoefficient = bound(signedCoefficient, INT224_MIN, INT224_MAX);
360+
exponent = bound(exponent, -80, -5);
361+
(int256 idx, bool interpolate, int256 scale) =
362+
LibDecimalFloatImplementation.mantissa4(signedCoefficient, exponent);
363+
if (!interpolate) {
364+
// No interpolation promised => the division was exact.
365+
assertEq(idx * scale, signedCoefficient);
366+
} else {
367+
// Interpolation flagged => there really was a remainder.
368+
assertTrue(idx * scale != signedCoefficient);
369+
}
370+
// The reported scale is always the exact power of ten for the exponent.
371+
// forge-lint: disable-next-line(unsafe-typecast)
372+
assertEq(scale, int256(10 ** uint256(-(exponent + 4))));
373+
}
374+
375+
/// Safety invariant for the below-resolution branch over the realistic
376+
/// int224 domain and full int32-style negative exponent range below -80:
377+
/// idx is always 0, scale always 1, and the interpolate flag is true exactly
378+
/// when information (a nonzero coefficient) was discarded. This is what makes
379+
/// the flag a faithful "we lost magnitude" signal.
380+
function testMantissa4BelowResolutionFlagIsFaithful(int256 signedCoefficient, int256 exponent) external pure {
381+
signedCoefficient = bound(signedCoefficient, INT224_MIN, INT224_MAX);
382+
exponent = bound(exponent, type(int32).min, -81);
383+
(int256 idx, bool interpolate, int256 scale) =
384+
LibDecimalFloatImplementation.mantissa4(signedCoefficient, exponent);
385+
assertEq(idx, 0);
386+
assertEq(scale, 1);
387+
assertEq(interpolate, signedCoefficient != 0);
388+
}
389+
128390
// -- unitLinearInterpolation --
129391

130392
function testUnitLinearInterpolationExact() external pure {

0 commit comments

Comments
 (0)