test(contracts): solvency invariant suite + error-path coverage (H8)#7
Merged
Conversation
…reputation (H6)
Audit H6: 'batches stopped landing' was invisible without journalctl. A tiny
dep-free registry (counters/gauges) now records every load-bearing event and
serves two consumers from one place:
- Operations: GET /metrics renders Prometheus text (rate-limit-exempt, both
bins). Series: epochs_run, quorum_reached/failed, attestations_signed,
attestations_refused{verdict=forged|censored|fills-hash-mismatch|cancelled},
batches_submitted, submit_reverts, gossip_send_failures, pool_size (gauge),
settlement_fills, spend_keys/served/settled_tokens.
- Reputation: SurplusMetricsSource implements blueprint QoS MetricsSource, so
the attributable POSITIVE-work subset (batches settled, tokens served,
quorum participation) is ABI-encoded and submitted on-chain by the heartbeat
— the record reputation/reward/slashing read and the UI can render as
per-operator trust. Adversarial signals (censorship/fraud) are deliberately
NOT self-reported here; peers report those through the BSM challenge path.
Wire via QoSServiceBuilder::with_metrics_source in the blueprint runner.
15 operator tests green (+2).
A counter at 0 is a real datapoint; a missing series breaks rate() and flatline alerts. metrics::init() touches every known series at boot (both bins), so /metrics exposes the full set from a fresh start instead of only what has fired. Proven live: idle fleet shows all series at 0; after a settled batch the proposer (op5, Helsinki) shows epochs_run/batches_submitted=1 and the co-signers (op3/op4) show attestations_signed=1 — per-operator work attributed correctly across datacenters.
The audit traced the accounting by hand and found it sound; this proves it
across thousands of random sequences and closes the named coverage gaps.
Invariant suite (test/invariant/) — a handler drives random deposit / withdraw
/ collateral / settleFill / redeem / spend / default-reclaim / warp sequences,
each action tolerating its own reverts so the fuzzer composes deep states. The
properties:
- SOLVENCY: token.balanceOf(settlement) == Σbalances + Σcollateral. The
contract always holds exactly what it owes — every mutation just shuffles
between those buckets; no sequence makes it insolvent or strands tokens.
- REFUNDABILITY: collateral[issuer] >= liability[issuer] always. The 5%
penalty buffer minted at fill is exactly consumed by worst-case defaults,
never overdrawn.
- CONSERVATION: balance == deposited - withdrawn (no off-book mint/burn).
settleFill is deterministic-mint and in the selector set, so the fuzzer
reaches lot-bearing states by construction; HandlerSmoke.t.sol concretely
drives fill→redeem→spend→reclaim and asserts solvency at each step (foundry
reverts handler state between runs, so coverage is proven here, not via a
cumulative counter). foundry.toml gains the [invariant] config the audit noted
was missing.
Error paths (test/ErrorPaths.t.sol) — the audit flagged NotLotHolder (theft
guard), the ZeroAmount guards, and ServedExceedsRequested (over-serve dispute)
as having zero coverage. One test per revert, plus withdraw-above-balance.
92 forge tests green (was 80).
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Closes audit H8 (zero fuzz/invariant tests; named error paths uncovered). Contract-side only — no logic change, pure test artifacts. Off
main.Invariant suite — proves the accounting across random sequences
A handler drives random deposit/withdraw/collateral/settleFill/redeem/spend/default-reclaim/warp sequences. Properties:
token.balanceOf(settlement) == Σbalances + Σcollateral. The contract always holds exactly what it owes; every mutation just shuffles between those buckets. No sequence makes it insolvent or strands tokens.collateral[issuer] >= liability[issuer]always. The 5% penalty buffer minted at fill is exactly consumed by worst-case defaults, never overdrawn.balance == deposited - withdrawn(no off-book mint/burn).settleFillis deterministic-mint and in the selector set, so the fuzzer reaches lot-bearing states by construction.HandlerSmoke.t.solconcretely drives fill→redeem→spend→reclaim and asserts solvency at each step — foundry reverts handler state between runs, so coverage is proven there rather than via a cumulative counter.foundry.tomlgains the[invariant]config the audit noted was missing.Error paths
The audit flagged
NotLotHolder(theft guard), theZeroAmountguards, andServedExceedsRequested(over-serve dispute) as having zero coverage. One test per revert + withdraw-above-balance.92 forge tests green (was 80).
🤖 Generated with Claude Code