feat(sra): implement Service Rewards Actor (FIP-0118) - #24
Conversation
|
I squashed those branches. please rebase onto the latest main or swa branch |
|
Nice to see a lot of working through the design in that document! There's also this thread which I've been updating with some unresolved questions which you're taking a position on in here: #7 - we'll need to align on those. Your "deviation d" is an interesting one to consider. |
Thanks! Noted — I'll try to join the discussion on #7 and align the implementation once those settle. |
The bare 'pip install halmos' resolves to 0.3.3 on the GitHub Actions index (the local mirror lags at 0.1.13), and the 0.3 CLI dropped --no-test-constructor — the run failed at argument parsing (exit 2). Pin halmos==0.1.13 (the version verified locally: QuarterWindowCheck 2/2 PASS) on setup-python 3.11, and add an explicit forge build --force --extra-output metadata pass so the symbolic run reads a deterministic build-info (docs §5.10 already documents this path).
CI fuzz (invariant_NonZeroTotal_ValidShareMap, seed 0x8104...) hit a quarter-misaligned submission: submitShares(q) with q beyond the mirror's activeQ (a quarter already bound but never written — posting/verification elapsed with no contribution) treated q != activeQ as the previous-quarter mirror and collected the *older* quarter's prevFpv, overwriting the share map with a 2-recipient distribution against a stale snapshot count of 1. The mirror advances only as far as the last written quarter. Bound quarters with no write are all-zero by construction (no postVolume/correctVolume can reach them after the windows close), so the submission is a benign no-op: the quarter still counts as submitted (lastSubmittedQ = q + 1), the existing share map stands. q == activeQ reads the fpv slot; q == activeQ - 1 reads prevFpv; any other bound quarter is no-op (spec §4.2: latest bound quarter + all-zero no-op). Regression: test_Mirror_SubmitShares_FutureBoundQuarter_NoOp (Red before, Green after). 304 tests pass (17 suites incl. invariant fuzz); CI seed reproduced clean; halmos QuarterWindowCheck 2/2.
…the share map Two review findings (PR filecoin-project#24 review round 2): B1 (blocking): correctVolume/postVolume could regress activeQ. The advance guard assumed the mirror only moves forward, but the constructor did not enforce non-overlapping windows (POST + VERIFY <= EPOCHS). With overlapping windows a governance call to correctVolume(older q) legitimately fell inside the still-open verification window and _advanceMirror rewound activeQ, clearing the newer quarter's posted FPV, re-enabling duplicate posts and double-counting totalUsd. - constructor: require(postPeriod + verificationWindow <= epochsPerQuarter) to eliminate overlapping windows at the configuration level; - _assertMirrorWindow: q must be activeQ or activeQ + 1 (write entry semantics - a write can only target the current or the next quarter; skipping quarters would misalign prevFpv, same family as the A3 fix). Applied before the advance in postVolume and correctVolume as defense in depth. S1 (should fix): remove deducted totalUsd after the quarter was bound, drifting the aggregatedFPV historical snapshot. The exclusion boundary must mirror the share map collection, not the freeze boundary: remove drops the orchestrator from the admitted list (so the map no longer includes it), while freeze keeps it. Deduct only while the quarter is not yet bound (!_afterBinding): posting-window and verification-window removals both exclude the FPV from the aggregate, keeping aggregatedFPV == map sum; after binding the snapshot stays fixed. Regression tests (Red -> Green): - Ctor_WindowOverlap_Rejected / Ctor_WindowBoundary_Accepted - PostVolume_SkipQuarter_Reverts / CorrectVolume_SkipQuarter_Reverts - Remove_InPostingWindow_DeductsAggregate - Remove_InVerificationWindow_Excludes (probe scenario formalised) - Remove_AfterBinding_KeepsSnapshot 311 tests pass (17 suites incl. invariant fuzz); 3 seeds; halmos 2/2.
…the share map Two review findings (PR filecoin-project#24 review round 2): B1 (blocking): correctVolume/postVolume could regress activeQ. The advance guard assumed the mirror only moves forward, but the constructor did not enforce non-overlapping windows (POST + VERIFY <= EPOCHS). With overlapping windows a governance call to correctVolume(older q) legitimately fell inside the still-open verification window and _advanceMirror rewound activeQ, clearing the newer quarter's posted FPV, re-enabling duplicate posts and double-counting totalUsd. - constructor: require(postPeriod + verificationWindow <= epochsPerQuarter) to eliminate overlapping windows at the configuration level; - _assertMirrorWindow: q must be activeQ or activeQ + 1 (write entry semantics - a write can only target the current or the next quarter; skipping quarters would misalign prevFpv, same family as the A3 fix). Applied before the advance in postVolume and correctVolume as defense in depth. S1 (should fix): remove deducted totalUsd after the quarter was bound, drifting the aggregatedFPV historical snapshot. The exclusion boundary must mirror the share map collection, not the freeze boundary: remove drops the orchestrator from the admitted list (so the map no longer includes it), while freeze keeps it. Deduct only while the quarter is not yet bound (!_afterBinding): posting-window and verification-window removals both exclude the FPV from the aggregate, keeping aggregatedFPV == map sum; after binding the snapshot stays fixed. Regression tests (Red -> Green): - Ctor_WindowOverlap_Rejected / Ctor_WindowBoundary_Accepted - PostVolume_SkipQuarter_Reverts / CorrectVolume_SkipQuarter_Reverts - Remove_InPostingWindow_DeductsAggregate - Remove_InVerificationWindow_Excludes (probe scenario formalised) - Remove_AfterBinding_KeepsSnapshot 311 tests pass (17 suites incl. invariant fuzz); 3 seeds; halmos 2/2.
…time Two related fixes for the mirror's quarter progression (PR filecoin-project#24 reviews 3-4). The progression was write-driven (activeQ only advanced when someone wrote), but quarter progression is a time property: any consecutive quarter with no writes deadlocked the system and left time-sensitive guards reading a stale cache. Part 1 - gap quarter deadlock (review 3): The mirror-window guard (review B1) restricted writes to q in {activeQ, activeQ+1}, but postVolume rejects zero FPV - a quarter where every orchestrator has no volume is necessarily unwritten, so the guard made it a permanent barrier with no governance recovery path (probe: q0 post, q1 empty, q2 post reverts). - _assertMirrorWindow: relax to q >= activeQ (still blocks rewinds; the upper bound is enforced by the posting/verification window checks); - _advanceMirror: one-step jump - adjacent advance (q == activeQ + 1) backs up the active quarter (frozenAtPostEnd exclusion-fixed); a skip (q > activeQ + 1) sets prevFpv = 0, since the skipped quarter is a gap with no data and no exclusion targets. O(n) regardless of gap size. Part 2 - time-driven quarter clock (review 4): activeQ mixed two semantics: slot ownership (which quarter occupies the fpv/prevFpv slots) and time judgments (which quarter is the latest bound). The slot semantics were correct, but time judgments read the write-driven cache, which lags when nothing is written - _pendingSharesQuarter (remove guard) missed the true latest bound inside a gap window. - _quarterOf(nowE): pure time derivation of the current quarter, saturating to 0 before the activation epoch (covers the activation hold period; aligns with the genesis activeQ = 0); - _syncMirror(qt): write-path time correction - advance the cache to the current time quarter if it lags (one-step jump semantics, idempotent), called before the window guard in postVolume/correctVolume; - _pendingSharesQuarter: latest bound derived from _quarterOf(currentEpoch()) instead of the activeQ cache - remove correctly reverts PendingShares inside a gap window. Regression tests (Red -> Green): - PostVolume_SkipsGapQuarter / CorrectVolume_SkipsGapQuarter (rewritten) - GapQuarter_NoDeadlock (q1 empty, q2 write succeeds) - GapQuarter_SubmitShares_NoOp (gap quarter submission is an all-zero no-op) - Remove_PendingShares_GapWindow (q1 gap bound, remove reverts PendingShares) 314 tests pass (17 suites incl. invariant fuzz); 3 seeds; halmos 2/2.
Port 0f825a7 (feat(sra): replace address+successor chain with uint64 id identity) onto the mainline b521e61, which already carries all PR filecoin-project#24 review fixes (A3 three-state submitShares, B1 mirror-window guard + one-step jump, S1 remove exclusion semantics, time-driven _quarterOf/_syncMirror/ _pendingSharesQuarter). The identity layer is orthogonal to the mirror layer, so the port only rekeys the identity layer and keeps every review fix intact. Orchestrator identity becomes an internal monotonically allocated, never-reused uint64 id (activeIdOf/nextId/admittedIds); an address is only the current effective wallet. replace() is an O(1) wallet re-point that keeps mirror FPV continuity for already-posted quarters; re-admit allocates a fresh id, eliminating the alias-chain residual-state bug class (T10). binding/unclaimed checks read the bound id's admitted directly. - storage: OrchestratorInfo packs 30B into slot0 (wallet/admitted/ frozenAtPostEnd/frozenSince; successor removed); Registry rekeys to id (orchestrators:uint64, activeIdOf, bindings:uint64, nextId, admittedIds) - main contract: admit allocates a fresh id; remove keeps the id record (fpv/prevFpv retained for audit) and clears only the address mapping; replace = O(1) wallet re-point; all read/write paths resolve via activeIdOf; _isAdmitted/_resolve removed, _requireAdmittedId added; _swapRemove(uint64[]) - invariant handler: generation modeling (_idGen/_genSeq, PairRecord.gen) — an address hosts successive identities, so bindings are disambiguated by generation; replace moves only the current generation's pairs; I2/I3c re-aligned (A3 lesson: model must track the implementation) - tests: +5 (re-admit fresh identity, id monotonic never-reused, replace historical-FPV-kept, share-map writes current wallet, correctVolume via new address); existing replace/re-admit tests pass unchanged (same observable behavior) - docs: S13 decision record + sra-design.md id-model sync + impl/001/002 design & test-plan docs Verified: 319 tests (17 suites) + halmos 2/2 + 3-seed invariant; runtime 25,576B exceeds the EIP-170 cap — tracked in docs/sra-design.md §5.12, resolution is the planned contract split (logic-to-library / proxy split, filecoin-project#5).
Code comments: drop 'review B1/S1/S3/filecoin-project#7/Bug A' process wrappers per the comments/content instructions — keep the design rationale (quarter is a time property, mirror advances only forward, map/aggregate exclusion). The B1/S1/S3 numbering collided with the docs' own decision registry (minLot audit bound / QA-system fixes) — removing the code-side references resolves the ambiguity. Docs: replace line-number references (SRAQuarter:269, submitShares:547, admit:324, ...) with stable file::symbol anchors (test names / invariant names / function names). Line numbers are a fragile anchor — the id identity rework shifted them +56-69 lines; symbol anchors never drift. 41 insertions / 41 deletions across 7 files, zero logic changes.
|
@LinZexiao: I assume this PR can be marked as "ready for review". Please re-request review from reviewers when it's ready to be looked at again. |
Remove docs/impl/001-id-identity-on-mirror.md and 002-id-identity-test-plan.md — the design decision (S13) and the test plan are already consolidated in sra-design.md (§3.2 S13, §4.3.5); the separate impl documents were redundant with the main design doc.
| # QuarterWindowCheck only (the former ComputeSharesCheck was removed with | ||
| # the FixedU18 adoption — see docs/sra-design.md §4.5). Runs independently | ||
| # of the main test CI. |
| // current freeze state (0 = not frozen) for admission checks and freeze/unfreeze symmetry. | ||
| bool frozenAtPostEnd; // 1B | ||
| Epoch frozenSince; // current freeze state: 0 = not frozen; > 0 = frozen since this epoch — 8B | ||
| // 30B packed into slot0 (successor field removed — the id-keyed model needs no alias chain) |
There was a problem hiding this comment.
this isn't slot 0
you can note the packing in fewer words
| // Contribution slots (mirror): fpv = active-quarter contribution (0 = not posted), | ||
| // prevFpv = previous-quarter contribution mirror, exclusion-fixed at mirror advance | ||
| // (prevFpv <- frozenAtPostEnd ? 0 : fpv; fpv = 0). submitShares reads fpv for the | ||
| // active quarter (q == activeQ) and prevFpv for the previous one (q == activeQ - 1). | ||
| FixedU18 fpv; // slot1 | ||
| FixedU18 prevFpv; // slot2 |
There was a problem hiding this comment.
why do we mirror instead of using the totalUsd mapping?
| // current freeze state (0 = not frozen) for admission checks and freeze/unfreeze symmetry. | ||
| bool frozenAtPostEnd; // 1B | ||
| Epoch frozenSince; // current freeze state: 0 = not frozen; > 0 = frozen since this epoch — 8B | ||
| // 30B packed into slot0 (successor field removed — the id-keyed model needs no alias chain) |
There was a problem hiding this comment.
Don't fill the code with tombstones documenting previous versions. We won't need to do that until after we deploy the first version.
| // stands (previously any q != activeQ read prevFpv, misaligning the share map with the | ||
| // quarter: CI invariant_NonZeroTotal_ValidShareMap — 2 recipients against a snapshot count of 1). |
There was a problem hiding this comment.
don't leave tombstones in the code describing previous designs
| uint64 id = r.admittedIds[i]; | ||
| SraStorage.OrchestratorInfo storage o = r.orchestrators[id]; | ||
| if (usePrev) { | ||
| if (FixedU18.unwrap(o.prevFpv) == 0) continue; |
There was a problem hiding this comment.
Define a FixedU18 constant ZERO so we don't have to unwrap for this comparison.
| // 18-decimal fixed-point: usd * SHARE_TOTAL / total, mathematically identical to the | ||
| // integer-USD form (usd_f = usd, total_f = total are already 18-decimal). Type-safe | ||
| // against integer/fixed-point magnitude mixing. | ||
| FixedU18 shareF = usds[i] * ONE / total; |
There was a problem hiding this comment.
multiplying a FixedU18 by ONE is a no-op
| // remainder = (usd_f × 1e18) % total_f = (usd × 1e18 % total_int) × 1e18 — the integer-USD | ||
| // remainder scaled by 1e18; the common ×1e18 factor preserves relative ordering, so the | ||
| // largest-remainder assignment order is bit-identical to the integer formulation. | ||
| remainders[i] = FixedU18.unwrap(usds[i]) * ONE_WAD % totalUsd; |
There was a problem hiding this comment.
define modulus in FixedU18 for operator %
| uint64 private constant SERVICE_STREAM_ID = 2; | ||
|
|
||
| /// @dev Total share (f02 encoding constraint: Σ shares must be exactly == 1e18). | ||
| uint256 private constant SHARE_TOTAL = 1e18; |
| remainders[i] = FixedU18.unwrap(usds[i]) * ONE_WAD % totalUsd; | ||
| residue -= shares[i].share; | ||
| } | ||
| // Remainder descending: each round tops up +1 to the largest remaining remainder (n <= 64, O(n²) acceptable) |
There was a problem hiding this comment.
I don't think it makes sense to do this ONE. It doesn't have to be super-fair because it's not super-impactful.
| for (uint256 i = 0; i < n; i++) { | ||
| if (list[i] == id) { | ||
| list[i] = list[n - 1]; | ||
| list.pop(); | ||
| return; | ||
| } | ||
| } |
There was a problem hiding this comment.
We can make this constant-time by tracking the index. Can extend the activeIdOf id mapping to also track admittedIndex. There may be other good places to pack it; look for what fields also change in the same transactions.
| if (kept < shares.length) { | ||
| Share[] memory trimmed = new Share[](kept); | ||
| for (uint256 i = 0; i < kept; i++) { | ||
| trimmed[i] = shares[i]; | ||
| } | ||
| shares = trimmed; | ||
| } |
There was a problem hiding this comment.
There is a better way to trim to length kept
| if (kept < shares.length) { | |
| Share[] memory trimmed = new Share[](kept); | |
| for (uint256 i = 0; i < kept; i++) { | |
| trimmed[i] = shares[i]; | |
| } | |
| shares = trimmed; | |
| } | |
| if (kept < shares.length) { | |
| assembly ("memory-safe") { | |
| mstore(shares, kept) | |
| } | |
| } |
| qt.lastSubmittedQ = q + 1; | ||
| return; | ||
| } | ||
| address[] memory wallets = new address[](r.admittedIds.length); |
There was a problem hiding this comment.
allocate this as Shares to reduce the copywork in _computeShares
| // integer-USD form (usd_f = usd, total_f = total are already 18-decimal). Type-safe | ||
| // against integer/fixed-point magnitude mixing. | ||
| FixedU18 shareF = usds[i] * ONE / total; | ||
| shares[i] = Share({wallet: wallets[i], share: FixedU18.unwrap(shareF)}); |
There was a problem hiding this comment.
I think we can make Share.share type FixedU18
| // verification window closing after the next quarter has begun would let a governance | ||
| // CorrectVolume target an already-advanced quarter, rewinding activeQ (uint256 intermediate | ||
| // guards the addition against overflow). | ||
| require(uint256(postPeriod) + uint256(verificationWindow) <= uint256(epochsPerQuarter), InvalidParameter()); |
There was a problem hiding this comment.
| require(uint256(postPeriod) + uint256(verificationWindow) <= uint256(epochsPerQuarter), InvalidParameter()); | |
| require(uint256(postPeriod) + uint256(verificationWindow) < uint256(epochsPerQuarter), InvalidParameter()); |
The equal case seems to have a bug.
| EPOCHS_PER_QUARTER = Epoch.wrap(epochsPerQuarter); | ||
| POST_PERIOD = Epoch.wrap(postPeriod); | ||
| VERIFICATION_WINDOW = Epoch.wrap(verificationWindow); | ||
| SRA_CANCEL_HOLD = Epoch.wrap(cancelHold); | ||
| ACTIVATION_EPOCH = Epoch.wrap(activationEpoch); |
There was a problem hiding this comment.
The parameters can be of type Epoch.
Service Rewards Actor — FIP-0118 Reference Implementation
Background
FIP-0118 proposes the Service Rewards Actor (SRA): a quarter-windowed rewards reporting mechanism for Service Providers (SPs) — orchestrators report service volume per quarter, which after validation is converted into FVM rewards distributed to the orchestrator and its bound wallets. The draft is currently Open, with some rvagg review points not yet absorbed (Test Cases TODO, supply accounting "TO BE REVIEWED", SnapDeals data-presence TBD). This PR provides a compilable, testable reference implementation of the SRA; where the draft is underspecified, it follows the approved design decisions.
Changes
src/ServiceRewardsActor.sol):test/halmos/): formal properties of_computeSharesand the quarter-window state machineAggregatedFPVread semantics,MIN_LOT,MAX_PRICE_PERIODS,PRICE_BANDanchored reference,Replaceidentity transfer) — all addressed and recorded, see design doc and decision recorddocs/sra-design.md(design, decisions, test plan, security review)Correctness guarantees
_computeShares6/6 properties (conservation / monotonicity / floor bound / no overflow), quarter-window state machine 4/4replace+ re-admit, a frozen successor could receive shares via the resolve chain (re-admit = fresh identity semantics)References
docs/sra-design.md— consolidated design, decisions, test plan & registry, and security review