SIG-598: add Echidna coverage for FixedPointMathU, ClmsrMath, FeeWaterfallLib

[worjs]

Context

Echidna coverage-guided fuzzing was limited to LazyMulSegmentTree only, leaving three numeric-critical libraries (FixedPointMathU, ClmsrMath, FeeWaterfallLib) without coverage-guided property testing. The numeric-security-spec.md lists Echidna as a mandatory gate, but no targets were defined beyond the segment tree. Linked to SIG-598.

Decisions

• Added three new Echidna target contracts rather than extending the existing EchidnaLazyMulTree — each library has distinct input domains and property sets that benefit from isolated corpus evolution
• FixedPointMathU uses seqLen: 1 (stateless pure functions) while ClmsrMath and FeeWaterfallLib use seqLen: 100 (stateful sequence exploration)
• EchidnaFeeWaterfallLib runs both the production FeeWaterfallLibHarness and the FeeWaterfallReference implementation, asserting parity across all 10 output fields
• EchidnaClmsrMath uses the existing ClmsrMathCostHarness and LazyMulSegmentTreeNoLink to compose realistic buy/sell/roundtrip sequences against the actual cost function
• TradeModule and LPVaultModule are not covered in this PR — their Echidna targets require multi-contract orchestration (module + core + position token) which is a separate effort

Risk Areas

• EchidnaClmsrMath drift tolerance constants (DRIFT_TOLERANCE_WAD_WEI = 1e12, REL_DRIFT_DENOM = 1e12) — if too loose, the fuzzer may miss genuine precision regressions; if too tight, false positives from compound rounding
• EchidnaFeeWaterfallLib._boundValidParams adjusts deltaEt and Bprev upward when grant need exceeds them — this prevents expected reverts but also narrows the input space for loss-dominant scenarios
• echidna_no_value_creation property allows proceeds <= cost + drift rather than strict proceeds <= cost — the tolerance accommodates rounding but could mask small value-creation bugs

[signals-reviewer]

Summary

This PR adds three new Echidna coverage-guided fuzzing targets for FixedPointMathU (19 properties), ClmsrMath (9 properties), and FeeWaterfallLib (7 properties). Each target operates in isolation with its own config and corpus directory. The targets exercise arithmetic ordering, roundtrip properties, monotonicity, conservation laws, and reference-parity checks. Production code is unchanged — all additions are in verification/foundry/.

Issues

No issues found.

Suggestions

No suggestions.

Verdict

APPROVE: The three Echidna targets are well-constructed. Specific technical observations:

1. Input bounding is correct across all three contracts. EchidnaClmsrMath._boundQuantity uses maxSafeChunkQuantity(alpha) to prevent FP_Overflow from _safeExp. EchidnaFeeWaterfallLib._boundValidParams adjusts deltaEt and Bprev upward to satisfy the GrantExceedsTailBudget and InsufficientBackstopForGrant guards, and caps absLt at Nprev + Ftot to prevent CatastrophicLoss. EchidnaFixedPointMath bounds all inputs to their valid domains (e.g., storedExpLnX in [WAD, MAX_EXP_INPUT_WAD]).

2. Error handling in _handleClmsrRevert catches FP_DivisionByZero and MathMulOverflow (both can originate from LazyMulSegmentTree and FixedPointMathU). Other error selectors (FP_Overflow, FP_InvalidInput) are not caught — this is correct because input bounding should prevent them, and if they somehow fire, they should be flagged as unexpected reverts.

3. Drift tolerances (DRIFT_TOLERANCE_WAD_WEI = 1e12, REL_DRIFT_DENOM = 1e12) yield a combined tolerance of ~1e12 + baseline/1e12 wei. For a typical lastRoundtripCost of 1e18 (1 WAD), the tolerance is ~1e12 + 1e6 ≈ 1e12 wei — about 1e-6 WAD ($0.000001). This is tight enough to catch genuine precision regressions while accommodating wDivUp (buy) vs wDiv (sell) rounding asymmetry.

4. FeeWaterfallLib reference parity runs both the production FeeWaterfallLibHarness and FeeWaterfallReference in executeCalculate, asserting exact equality across all 10 output fields — this is the strongest possible correctness check.

5. No cross-repo impact. All changes are under verification/foundry/ (test-only). No ABI, event, or interface changes. No downstream repos need updates.

[signals-reviewer]

Summary

This PR adds three new Echidna coverage-guided fuzzing targets for FixedPointMathU (19 properties), ClmsrMath (9 properties), and FeeWaterfallLib (7 properties). Each target operates in isolation with its own config and corpus directory. The targets exercise arithmetic ordering, roundtrip properties, monotonicity, conservation laws, and reference-parity checks. Production code is unchanged — all additions are in verification/foundry/.

Issues

No issues found.

Suggestions

No suggestions.

Verdict

APPROVE: The three Echidna targets are well-constructed. Specific technical observations:

1. Input bounding is correct across all three contracts. EchidnaClmsrMath._boundQuantity uses maxSafeChunkQuantity(alpha) to prevent FP_Overflow from _safeExp. EchidnaFeeWaterfallLib._boundValidParams adjusts deltaEt and Bprev upward to satisfy the GrantExceedsTailBudget and InsufficientBackstopForGrant guards, and caps absLt at Nprev + Ftot to prevent CatastrophicLoss. EchidnaFixedPointMath bounds all inputs to their valid domains (e.g., storedExpLnX in [WAD, MAX_EXP_INPUT_WAD]).

2. Error handling in _handleClmsrRevert catches FP_DivisionByZero and MathMulOverflow (both can originate from LazyMulSegmentTree and FixedPointMathU). Other error selectors (FP_Overflow, FP_InvalidInput) are not caught — this is correct because input bounding should prevent them, and if they somehow fire, they should be flagged as unexpected reverts.

3. Drift tolerances (DRIFT_TOLERANCE_WAD_WEI = 1e12, REL_DRIFT_DENOM = 1e12) yield a combined tolerance of ~1e12 + baseline/1e12 wei. For a typical lastRoundtripCost of 1e18 (1 WAD), the tolerance is ~1e12 + 1e6 ≈ 1e12 wei — about 1e-6 WAD ($0.000001). This is tight enough to catch genuine precision regressions while accommodating wDivUp (buy) vs wDiv (sell) rounding asymmetry.

4. FeeWaterfallLib reference parity runs both the production FeeWaterfallLibHarness and FeeWaterfallReference in executeCalculate, asserting exact equality across all 10 output fields — this is the strongest possible correctness check.

5. No cross-repo impact. All changes are under verification/foundry/ (test-only). No ABI, event, or interface changes. No downstream repos need updates.

[signals-reviewer]

Summary

This PR adds three new Echidna coverage-guided fuzzing targets for FixedPointMathU (19 properties), ClmsrMath (9 properties), and FeeWaterfallLib (7 properties). Each target operates in isolation with its own config and corpus directory. The targets exercise arithmetic ordering, roundtrip properties, monotonicity, conservation laws, and reference-parity checks. Production code is unchanged — all additions are in verification/foundry/.

Issues

No issues found.

Suggestions

No suggestions.

Verdict

APPROVE: The three Echidna targets are well-constructed. Specific technical observations:

1. Input bounding is correct across all three contracts. EchidnaClmsrMath._boundQuantity uses maxSafeChunkQuantity(alpha) to prevent FP_Overflow from _safeExp. EchidnaFeeWaterfallLib._boundValidParams adjusts deltaEt and Bprev upward to satisfy the GrantExceedsTailBudget and InsufficientBackstopForGrant guards, and caps absLt at Nprev + Ftot to prevent CatastrophicLoss. EchidnaFixedPointMath bounds all inputs to their valid domains (e.g., storedExpLnX in [WAD, MAX_EXP_INPUT_WAD]).

2. Error handling in _handleClmsrRevert catches FP_DivisionByZero and MathMulOverflow (both can originate from LazyMulSegmentTree and FixedPointMathU). Other error selectors (FP_Overflow, FP_InvalidInput) are not caught — this is correct because input bounding should prevent them, and if they somehow fire, they should be flagged as unexpected reverts.

3. Drift tolerances (DRIFT_TOLERANCE_WAD_WEI = 1e12, REL_DRIFT_DENOM = 1e12) yield a combined tolerance of ~1e12 + baseline/1e12 wei. For a typical lastRoundtripCost of 1e18 (1 WAD), the tolerance is ~1e12 + 1e6 ≈ 1e12 wei — about 1e-6 WAD ($0.000001). This is tight enough to catch genuine precision regressions while accommodating wDivUp (buy) vs wDiv (sell) rounding asymmetry.

4. FeeWaterfallLib reference parity runs both the production FeeWaterfallLibHarness and FeeWaterfallReference in executeCalculate, asserting exact equality across all 10 output fields — this is the strongest possible correctness check.

5. No cross-repo impact. All changes are under verification/foundry/ (test-only). No ABI, event, or interface changes. No downstream repos need updates.

[signals-reviewer]

Summary

This PR adds three new Echidna coverage-guided fuzzing targets for FixedPointMathU (19 properties), ClmsrMath (9 properties), and FeeWaterfallLib (7 properties). Each target operates in isolation with its own config and corpus directory. The targets exercise arithmetic ordering, roundtrip properties, monotonicity, conservation laws, and reference-parity checks. Production code is unchanged — all additions are in verification/foundry/.

Issues

No issues found.

Suggestions

No suggestions.

Verdict

APPROVE: The three Echidna targets are well-constructed. Specific technical observations:

1. Input bounding is correct across all three contracts. EchidnaClmsrMath._boundQuantity uses maxSafeChunkQuantity(alpha) to prevent FP_Overflow from _safeExp. EchidnaFeeWaterfallLib._boundValidParams adjusts deltaEt and Bprev upward to satisfy the GrantExceedsTailBudget and InsufficientBackstopForGrant guards, and caps absLt at Nprev + Ftot to prevent CatastrophicLoss. EchidnaFixedPointMath bounds all inputs to their valid domains (e.g., storedExpLnX in [WAD, MAX_EXP_INPUT_WAD]).

2. Error handling in _handleClmsrRevert catches FP_DivisionByZero and MathMulOverflow (both can originate from LazyMulSegmentTree and FixedPointMathU). Other error selectors (FP_Overflow, FP_InvalidInput) are not caught — this is correct because input bounding should prevent them, and if they somehow fire, they should be flagged as unexpected reverts.

3. Drift tolerances (DRIFT_TOLERANCE_WAD_WEI = 1e12, REL_DRIFT_DENOM = 1e12) yield a combined tolerance of ~1e12 + baseline/1e12 wei. For a typical lastRoundtripCost of 1e18 (1 WAD), the tolerance is ~1e12 + 1e6 ≈ 1e12 wei — about 1e-6 WAD ($0.000001). This is tight enough to catch genuine precision regressions while accommodating wDivUp (buy) vs wDiv (sell) rounding asymmetry.

4. FeeWaterfallLib reference parity runs both the production FeeWaterfallLibHarness and FeeWaterfallReference in executeCalculate, asserting exact equality across all 10 output fields — this is the strongest possible correctness check.

5. No cross-repo impact. All changes are under verification/foundry/ (test-only). No ABI, event, or interface changes. No downstream repos need updates.

[signals-reviewer]

Summary

This PR adds three new Echidna coverage-guided fuzzing targets for FixedPointMathU (19 properties), ClmsrMath (9 properties), and FeeWaterfallLib (7 properties). Each target operates in isolation with its own config and corpus directory. The targets exercise arithmetic ordering, roundtrip properties, monotonicity, conservation laws, and reference-parity checks. Production code is unchanged — all additions are in verification/foundry/.

Issues

No issues found.

Suggestions

No suggestions.

Verdict

APPROVE: The three Echidna targets are well-constructed. Specific technical observations:

1. Input bounding is correct across all three contracts. EchidnaClmsrMath._boundQuantity uses maxSafeChunkQuantity(alpha) to prevent FP_Overflow from _safeExp. EchidnaFeeWaterfallLib._boundValidParams adjusts deltaEt and Bprev upward to satisfy the GrantExceedsTailBudget and InsufficientBackstopForGrant guards, and caps absLt at Nprev + Ftot to prevent CatastrophicLoss. EchidnaFixedPointMath bounds all inputs to their valid domains (e.g., storedExpLnX in [WAD, MAX_EXP_INPUT_WAD]).

2. Error handling in _handleClmsrRevert catches FP_DivisionByZero and MathMulOverflow (both can originate from LazyMulSegmentTree and FixedPointMathU). Other error selectors (FP_Overflow, FP_InvalidInput) are not caught — this is correct because input bounding should prevent them, and if they somehow fire, they should be flagged as unexpected reverts.

3. Drift tolerances (DRIFT_TOLERANCE_WAD_WEI = 1e12, REL_DRIFT_DENOM = 1e12) yield a combined tolerance of ~1e12 + baseline/1e12 wei. For a typical lastRoundtripCost of 1e18 (1 WAD), the tolerance is ~1e12 + 1e6 ≈ 1e12 wei — about 1e-6 WAD ($0.000001). This is tight enough to catch genuine precision regressions while accommodating wDivUp (buy) vs wDiv (sell) rounding asymmetry.

4. FeeWaterfallLib reference parity runs both the production FeeWaterfallLibHarness and FeeWaterfallReference in executeCalculate, asserting exact equality across all 10 output fields — this is the strongest possible correctness check.

5. No cross-repo impact. All changes are under verification/foundry/ (test-only). No ABI, event, or interface changes. No downstream repos need updates.

[signals-reviewer]

Summary

This PR adds three new Echidna coverage-guided fuzzing targets for FixedPointMathU (19 properties), ClmsrMath (9 properties), and FeeWaterfallLib (7 properties). Each target operates in isolation with its own config and corpus directory. The targets exercise arithmetic ordering, roundtrip properties, monotonicity, conservation laws, and reference-parity checks. Production code is unchanged — all additions are in verification/foundry/.

Issues

No issues found.

Suggestions

No suggestions.

Verdict

APPROVE: The three Echidna targets are well-constructed. Specific technical observations:

1. Input bounding is correct across all three contracts. EchidnaClmsrMath._boundQuantity uses maxSafeChunkQuantity(alpha) to prevent FP_Overflow from _safeExp. EchidnaFeeWaterfallLib._boundValidParams adjusts deltaEt and Bprev upward to satisfy the GrantExceedsTailBudget and InsufficientBackstopForGrant guards, and caps absLt at Nprev + Ftot to prevent CatastrophicLoss. EchidnaFixedPointMath bounds all inputs to their valid domains (e.g., storedExpLnX in [WAD, MAX_EXP_INPUT_WAD]).

2. Error handling in _handleClmsrRevert catches FP_DivisionByZero and MathMulOverflow (both can originate from LazyMulSegmentTree and FixedPointMathU). Other error selectors (FP_Overflow, FP_InvalidInput) are not caught — this is correct because input bounding should prevent them, and if they somehow fire, they should be flagged as unexpected reverts.

3. Drift tolerances (DRIFT_TOLERANCE_WAD_WEI = 1e12, REL_DRIFT_DENOM = 1e12) yield a combined tolerance of ~1e12 + baseline/1e12 wei. For a typical lastRoundtripCost of 1e18 (1 WAD), the tolerance is ~1e12 + 1e6 ≈ 1e12 wei — about 1e-6 WAD ($0.000001). This is tight enough to catch genuine precision regressions while accommodating wDivUp (buy) vs wDiv (sell) rounding asymmetry.

4. FeeWaterfallLib reference parity runs both the production FeeWaterfallLibHarness and FeeWaterfallReference in executeCalculate, asserting exact equality across all 10 output fields — this is the strongest possible correctness check.

5. No cross-repo impact. All changes are under verification/foundry/ (test-only). No ABI, event, or interface changes. No downstream repos need updates.