diff --git a/docs/project-status.md b/docs/project-status.md index d59a032..f709064 100644 --- a/docs/project-status.md +++ b/docs/project-status.md @@ -2,9 +2,9 @@ **Last Updated:** September 8, 2026 **Project Phase:** Solidity / Reference Implementation -**Current Implementation Slice:** GI — Full Stateful Invariant Verification (NEXT AUTHORIZED / NOT STARTED) -**Last Closed Gate:** G8D — Causal Finalization / Economic Finality Gate (CLOSED / PASS) -**Status:** F0 COMPLETE — F1 COMPLETE — F2 COMPLETE — F3 COMPLETE — F4 COMPLETE — F5 COMPLETE — F6A COMPLETE — F7 COMPLETE — F6B COMPLETE — F8A COMPLETE — F8B COMPLETE — F8C COMPLETE — F8D COMPLETE — GI NOT STARTED +**Current Implementation Slice:** F9 — Canonical Acceptance (NEXT AUTHORIZED / NOT STARTED) +**Last Closed Gate:** G-I — Full Stateful Invariant Gate (CLOSED / PASS) +**Status:** F0 COMPLETE — F1 COMPLETE — F2 COMPLETE — F3 COMPLETE — F4 COMPLETE — F5 COMPLETE — F6A COMPLETE — F7 COMPLETE — F6B COMPLETE — F8A COMPLETE — F8B COMPLETE — F8C COMPLETE — F8D COMPLETE — GI COMPLETE — F9 NOT STARTED --- @@ -41,15 +41,15 @@ Implementation proceeds through the verification-gated F0–F10 ladder defined i The next authorized slice is: -> **GI — Full Stateful Invariant Verification** +> **F9 — Canonical Acceptance** The last closed gate is: -> **G8D — Causal Finalization / Economic Finality Gate** +> **G-I — Full Stateful Invariant Gate** -F0, F1, F2, F3, F4, F5, F6A, F7, F6B, F8A, F8B, F8C and F8D have been implemented, verified, and explicitly gate-closed. The targeted G3 revalidation required by the F5 prospective-derivability correction also passed, and G3 remains closed. +F0, F1, F2, F3, F4, F5, F6A, F7, F6B, F8A, F8B, F8C, F8D and GI have been implemented, verified, and explicitly gate-closed. The targeted G3 revalidation required by the F5 prospective-derivability correction also passed, and G3 remains closed. -F8D was reviewed independently and G8D was explicitly closed. GI is the next authorized implementation slice and has not been started. +GI was reviewed independently and G-I was explicitly closed. F9 is the next authorized implementation slice and has not been started. --- @@ -72,8 +72,8 @@ Current implementation sequence: | F8B | O2 Exact-Output Execution + Causal Evidence | **COMPLETE — G8B CLOSED** | | F8C | O2 Input Settlement + Direct Beneficiary Delivery | **COMPLETE — G8C CLOSED** | | F8D | O2 Causal Finalization | **COMPLETE — G8D CLOSED** | -| GI | Full Stateful Invariant Verification | **NEXT / NOT STARTED** | -| F9 | Canonical Acceptance | NOT STARTED | +| GI | Full Stateful Invariant Verification | **COMPLETE — G-I CLOSED** | +| F9 | Canonical Acceptance | **NEXT / NOT STARTED** | | F10 | Demo Instrumentation | NOT STARTED | | F9T | Public Testnet Evidence | OPTIONAL / OFF CRITICAL PATH | @@ -371,14 +371,14 @@ G2 verified predicate independence, administrator authority, read fidelity, cros ## 10. Current Blocker -There is no unresolved F0, F1, F2, F3, F4, F5, F6A, F7, F6B, F8A, F8B, F8C or F8D implementation responsibility and no open gate. +There is no unresolved F0, F1, F2, F3, F4, F5, F6A, F7, F6B, F8A, F8B, F8C, F8D or GI implementation responsibility and no open gate. The next unstarted responsibility is: -> **GI — Full Stateful Invariant Verification.** +> **F9 — Canonical Acceptance.** -GI is authorized as the next implementation slice but has not been started. No further downstream slice — -F9 — is authorized. +F9 is authorized as the next implementation slice but has not been started. No further downstream slice — +F10 — is authorized. Known limitations carried forward from F0, none of which blocked G0: @@ -581,11 +581,11 @@ The root `CLAUDE.md` will define the repository operating rules and document aut ## 18. Next Action -G8D has been reviewed and closed, so the next action is: +G-I has been reviewed and closed, so the next action is: -> **GI — Full Stateful Invariant Verification.** +> **F9 — Canonical Acceptance.** -GI may begin when explicitly tasked. Its own verification gate governs advancement beyond the GI boundary. +F9 may begin when explicitly tasked. Its own verification gate governs advancement beyond the F9 boundary. --- @@ -608,15 +608,16 @@ GI may begin when explicitly tasked. Its own verification gate governs advanceme - F8B O2 Exact-Output Execution / Execution Evidence is complete and G8B is closed. - F8C O2 Input Settlement / Direct Beneficiary Delivery is complete and G8C is closed. - F8D O2 Causal Finalization / Remaining Entitlement Reduction is complete and G8D is closed. +- GI Full Stateful Invariant Verification is complete and G-I is closed. **Current Gate** -- G8D — CLOSED / PASS. No gate is currently open. +- G-I — CLOSED / PASS. No gate is currently open. **Next Blocker** -- GI — Full Stateful Invariant Verification has not been started. +- F9 — Canonical Acceptance has not been started. **Immediate Next Step** -- Begin GI when explicitly tasked. +- Begin F9 when explicitly tasked. diff --git a/docs/prompts/retrospective/session-15-chatgpt-record.md b/docs/prompts/retrospective/session-15-chatgpt-record.md new file mode 100644 index 0000000..f3e6af1 --- /dev/null +++ b/docs/prompts/retrospective/session-15-chatgpt-record.md @@ -0,0 +1,977 @@ +# Standby — Session 15 ChatGPT Reasoning Record + +## GI — Full Stateful Invariant Verification + +**Artifact type:** Non-normative curated retrospective record +**Session scope:** GI — Full Stateful Invariant Verification +**Gate:** G-I +**Outcome:** PASS / CLOSED +**Next authorized slice:** F9 — Canonical Acceptance + +--- + +## 1. Purpose of This Record + +This file preserves the substantive user ↔ ChatGPT reasoning associated with Session 15 and GI — Full Stateful Invariant Verification. + +It is intentionally non-normative. It does not define Standby protocol semantics, replace frozen artifacts, or supersede the implementation plan, invariant package, testing strategy, or project status. + +Its purpose is to retain contemporaneous evidence of: + +- the user’s questions, concerns, challenges, and decisions; +- ChatGPT’s derivation of the GI verification boundary; +- distinctions between GI and prior implementation/testing slices; +- the invariant architecture and oracle/ghost-state reasoning; +- the derivation of G-I; +- independent review of Claude’s actual implementation and evidence; +- corrections and process refinements made during the session; +- post-GI coverage reasoning and review; +- methodology observations that may matter for the later project retrospective. + +--- + +## 2. Session Starting Point + +Session 15 began after completion of the full O2 implementation chain through F8D. + +At entry: + +- F0 through F8D were complete. +- G8D had passed. +- Production semantics were presumed complete. +- GI — Full Stateful Invariant Verification was the current blocker. +- F9 — Canonical Acceptance and F10 — Demo / Submission Readiness were not yet authorized. +- Post-F8D engineering baselines already existed for gas and coverage. +- The major question was no longer “what production behavior remains to be implemented?” but instead “can arbitrary authoritative histories violate any frozen invariant or produce divergence from independently derived expected state?” + +The central shift in Session 15 was therefore from implementation construction to compositional verification. + +--- + +## 3. User Question: What Does GI Actually Own? + +The user asked an important responsibility-boundary question early in the session: + +> If GI is the full stateful invariant gate, does that mean it would only include tests, and is the Hook contract basically complete pending significant issues found during testing? + +### ChatGPT derivation + +The answer was yes, with an important qualification. + +GI is fundamentally a verification-side slice. It does not own new Standby semantics. By the time GI begins, production responsibility should already have converged through F8D. + +The derived principle was: + +> **GI verifies composition. It does not invent semantics.** + +Therefore: + +- GI should primarily add stateful invariant infrastructure and evidence. +- Production code should remain unchanged unless GI discovers a genuine counterexample against a frozen invariant. +- Any production defect found by GI must be traced back to the existing normative owner — for example F4, F5, F6B, F7, or F8A–F8D. +- A correction would reopen the affected prior gate before GI could be considered complete. + +This distinction prevented GI from becoming a catch-all “fix whatever the invariant campaign encounters” implementation slice. + +--- + +## 4. GI Responsibility Reconstruction + +The exact GI responsibility was derived as: + +> **GI is the production-path stateful compositional verification boundary for Standby. It must demonstrate that arbitrary sequences of successful and rejected O1, O2, O3, lifecycle, eligibility, and relevant external actions cannot drive the completed realization into an authoritative state that violates a frozen invariant, corrupts commitment history or attribution, releases obligation illegitimately, leaves reusable causal evidence, or creates a divergence between authoritative production derivations and independent verification oracles.** + +A more compact accepted formulation was: + +> **GI — Full Stateful Invariant Verification proves the temporal and compositional safety of the completed Standby realization by adversarially composing authoritative O1, O2, O3, lifecycle, eligibility, and relevant environmental actions through production interfaces. It uses independently derived oracle/history state to establish backing derivation equivalence, backing sufficiency, commitment conservation, fulfillment attribution and exactness, bounded-reference integrity, causal isolation, authority and rejection atomicity, custody integrity, and verification-domain completeness across canonical and generalized reachable-state campaigns. GI introduces no new protocol semantics.** + +This became the governing semantic boundary for the implementation prompt and later independent review. + +--- + +## 5. Distinguishing GI from Existing Testing + +A major derivation was that GI is not simply “more fuzzing.” + +The distinctions were: + +- **Unit tests** establish local behavior of individual functions or responsibilities. +- **Integration tests** establish fidelity across concrete component paths. +- **Fuzz tests** explore adversarial parameter variation. +- **GI stateful invariants** explore temporal and compositional adversariality across persistent histories. + +The practical consequence was that the existing large test suite could not by itself close GI. + +GI needed: + +- persistent state across actions; +- arbitrary action sequencing; +- successful and rejected transitions; +- histories containing multiple commitments; +- eligibility churn; +- expiry and reference reuse; +- partial and full exercise; +- backing-threatening swaps and liquidity actions; +- failure followed by later valid operations; +- independent expected-value derivation. + +This is where the first true Foundry stateful invariant suite belonged. + +--- + +## 6. Stateful Architecture Derived Before Implementation + +The required architecture was derived as: + +```text +production fixture + ↓ +adversarial handler + ↓ +production interfaces + ↓ +authoritative production state + ↓ +independent oracle / remembered history + ↓ +transition-local assertions + global invariant closure +``` + +The production fixture had to use: + +- real PoolManager; +- real StandbyHook; +- real ExerciseRouter; +- real EligibilityRegistry; +- real production swap/liquidity perimeters where needed; +- real canonical mock currencies; +- no StandbyHookHarness as authoritative GI evidence; +- no direct economic state mutation. + +The handler was explicitly defined as: + +> **an adversarial transaction generator, not a semantic pre-filter.** + +Invalid requests were expected and useful. Inputs could be bounded only to avoid mechanical nonsense such as impossible TickMath domains, unbounded numerical noise, or an unbounded actor universe. + +--- + +## 7. Ghost-State Boundary + +A central design risk was allowing the test suite to accidentally become a second implementation of Standby. + +The derived rule was: + +> **Ghost state may remember history the production system does not persist for verification purposes, or independently calculate an oracle; it may not prescribe what the production state ought to be by duplicating the protocol state machine.** + +Legitimate remembered state included: + +- successfully admitted commitment IDs; +- immutable admission fact snapshots; +- previous observed Remaining values; +- independently tracked successful fulfillment per commitment; +- independently observed Beneficiary deliveries; +- direct unrelated donations; +- campaign counters. + +The suite should not maintain parallel authoritative classifications such as: + +- ghost validity; +- ghost exercisability; +- ghost binding status; +- ghost expiry state; +- ghost obligation; +- ghost expected Remaining; +- ghost O2 lifecycle. + +That distinction became one of the most important independent-review criteria. + +--- + +## 8. Independent Oracle Requirement + +The frozen testing strategy requires independent normative derivation rather than expected values that reuse implementation logic. + +Two primary GI oracles were derived. + +### Supporting Capacity + +The reference S calculation had to derive from authoritative PoolManager state using independent arithmetic. + +It could not simply call the same production helper that StandbyHook uses. + +### Aggregate Capacity Obligation + +The reference O construction should differ structurally from production. + +The especially strong derived strategy was: + +- production may derive O by scanning the bounded live reference index; +- GI should independently walk the full allocated commitment identity history and calculate which commitments currently contribute obligation. + +That creates a meaningful disagreement surface: if a still-binding commitment ever escaped the bounded reference index, production O and reference O would diverge. + +This became one of the strongest elements of the final implementation. + +--- + +## 9. Actor and Action Universe + +A persistent bounded actor universe was preferred over arbitrary fuzzed addresses because authority relationships must remain stable across a history. + +The proposed roles included: + +- registry admin; +- commitment authority; +- Beneficiary A; +- Beneficiary B; +- authorized exerciser; +- unauthorized exerciser; +- eligible trader; +- ineligible trader; +- eligible liquidity provider; +- ineligible liquidity provider; +- outsider. + +The action universe needed to include at least: + +```text +establishCommitment +ordinaryProtectedSwap +ordinaryOppositeSwap +addLiquidity +removeLiquidity +exercise +advanceTime +setBeneficiaryEligibility +setTraderEligibility +setLiquidityEligibility +directTransferProtectedTokenToBeneficiary +``` + +The implementation later added an orphan-evidence probe to test O2 causal isolation behaviorally. + +--- + +## 10. Required Stateful Sequence Classes + +The session identified dangerous sequence classes that GI had to be capable of reaching. + +Examples included: + +### Reference churn + +```text +many O1 +→ partial/full fulfillment +→ expiry +→ bounded-reference reclamation +→ new O1 +→ old/new commitment interaction +``` + +### Causal churn + +```text +O2(C1) +→ failed O2(C2) +→ O2(C1) +→ O2(C2) +``` + +### Authority churn + +```text +O1 +→ Beneficiary eligibility off +→ destructive O3 attempt +→ eligibility on +→ O2 +``` + +### Backing-boundary churn + +```text +multiple O1 +→ protected swap toward S == O +→ liquidity removal attempt +→ opposite swap +→ partial O2 +→ protected swap again +``` + +The important point was not that every sequence had to be a deterministic test. Rather, the campaign architecture had to demonstrate that the corresponding semantic histories were actually reachable and verified. + +--- + +## 11. Post-F8D Coverage Observations Carried into GI + +The post-F8D coverage report identified several potentially interesting surfaces. + +They were evaluated individually rather than automatically converted into GI obligations. + +The resulting treatment was: + +1. **Untrusted-perimeter liquidity removal** — relevant behavioral GI input. +2. **Nested exercise attribution** — relevant causal-isolation property, but not necessarily a normal handler action if production structurally forbids nested O2. +3. **Causal-position read-surface refusal** — subsumed by broader causal-context verification; not a separate invariant. +4. **Extreme tick-bound clamping** — principally an F5 derivation concern; not a standalone GI obligation unless a reachable compositional counterexample touched it. +5. **Unresolved exercise-delta fail-closed behavior** — relevant only if reachable through adversarial O2; otherwise prior F8 evidence remains sufficient. + +This prevented coverage observations from redefining the frozen verification scope. + +--- + +## 12. Exact G-I Derivation + +The frozen implementation plan contained 23 detailed gate conditions. + +For implementation and review clarity, these were organized into seven families without replacing the exact checklist. + +### GI-A — Independent Economic Backing + +- reference S == production S; +- reference O == production O; +- reference S >= reference O. + +### GI-B — Commitment Conservation & Historical Integrity + +- immutable admitted facts; +- Remaining <= Original; +- Remaining monotonic non-increasing; +- Original - Remaining == independently tracked successful fulfillment; +- expiry, eligibility mutation, swaps, liquidity, direct transfers, and failed O2 do not manufacture fulfillment; +- history survives reference reclamation and slot reuse. + +### GI-C — Fulfillment Exclusivity & Exactness + +- only successful authoritative O2 creates fulfillment; +- exactly one commitment is reduced; +- exactly q is fulfilled; +- exactly q is delivered to the authoritative Beneficiary under canonical mock semantics. + +### GI-D — O2 Causal Isolation & Atomicity + +- no reusable causal evidence survives a completed top-level action; +- failed or prior O2 evidence cannot authorize a later reduction; +- post-failure histories remain clean. + +### GI-E — Reference & Lifecycle Integrity + +- at most 16 references; +- references are unique and non-dangling; +- historical identity survives reuse; +- reclamation occurs only for frozen permanent non-binding causes. + +### GI-F — Authority, Rejection Atomicity & Custody + +- invalid, unauthorized, ineligible, and backing-threatening requests cannot create prohibited authoritative mutations; +- rejected transitions preserve relevant state; +- Hook and ExerciseRouter do not retain protocol-created custody. + +### GI-G — Campaign Completeness & Generalization + +- canonical zeroForOne campaign; +- generalized oneForZero/different ordering campaign; +- heterogeneous decimals where supported; +- diagnostics must prove meaningful O1/O2/O3/lifecycle activity. + +The exact 23 criteria remained the final PASS/FAIL checklist. + +--- + +## 13. Clean-Rule Correction to the Claude Prompt + +The user caught an important process issue before implementation. + +Earlier draft language risked reintroducing permanent role/process guidance into the session prompt. + +The user reaffirmed the clean rule: + +> **CLAUDE.md owns permanent operating behavior.** +> **.claude/rules/* owns permanent Solidity/testing conventions.** +> **Session prompts own only slice-specific objective, scope, requirements, prohibitions, file boundaries, gate evidence, and completion boundary.** + +The implementation prompt was regenerated to follow the mature Session 13-style structure: + +- direct slice objective; +- repository instruction ownership; +- authoritative files to inspect; +- GI-specific semantic boundary; +- stateful architecture; +- action/actor universe; +- ghost/oracle constraints; +- G-I criteria; +- evidence requirements; +- file boundary; +- completion boundary. + +The standing “Working Model” / ChatGPT-vs-Claude role section was intentionally removed from the Claude implementation prompt. + +This was a useful methodology refinement: even a good recurring section should not remain in a slice prompt if permanent repository instructions already own it. + +--- + +## 14. Claude Implementation — Independent Review + +Claude implemented four GI test-side files: + +```text +test/invariant/StandbyInvariantHandler.sol +test/invariant/BaseStandbyInvariantTest.t.sol +test/invariant/StandbySequenceEvidence.t.sol +test/invariant/StandbyInvariant.t.sol +``` + +and updated the Session 15 log. + +No production code was changed. + +ChatGPT independently reviewed the actual diff rather than relying on Claude’s completion report alone. + +--- + +## 15. Independent Review Findings + +### Production-path fidelity + +PASS. + +The suite uses: + +- real PoolManager; +- production StandbyHook; +- production ExerciseRouter; +- real EligibilityRegistry; +- real production perimeters; +- canonical deployment/configuration; +- no direct mutation of economic state. + +### Handler adversariality + +PASS. + +The handler intentionally generates both successful and rejected actions. + +Action tuning based on independent backing headroom was reviewed carefully and accepted as campaign-shaping rather than a safety pre-filter because production still determines admissibility and substantial refusal activity remained. + +### Independent Supporting Capacity oracle + +PASS. + +Reference S uses independent Q64.96 arithmetic over authoritative PoolManager state and does not call the production StandbyMath derivation. + +### Independent Obligation oracle + +PASS, and notably strong. + +Reference O walks the full allocated commitment history while production derives from the bounded enforcement index. This creates a real disagreement surface if a binding obligation ever escapes the production index. + +### Ghost-state discipline + +PASS. + +No parallel validity/exercisability/binding/expiry/obligation state machine was found. + +### Fulfillment conservation + +PASS. + +After successful O2: + +- ghost fulfillment increases only after production success; +- exactly one commitment is reduced; +- reduction equals q; +- all other commitments remain unchanged; +- Beneficiary receives exactly q. + +Global closure checks: + +```text +Original - Remaining == ghostFulfilled +``` + +### Failure atomicity + +PASS. + +Rejected O2 paths assert no Remaining movement, no delivery, no O release, unchanged relevant pool state, zero protocol custody, and empty causal context. + +Directed sequences also test failure followed by valid later operations. + +### Causal isolation + +PASS. + +All causal-context fields are required to be empty after completed actions. + +An additional orphan-evidence action attempts authorization/finalization without valid causal context. + +Nested O2 itself is not artificially manufactured because production structurally forbids it; the reachable causal-isolation shape is tested instead. + +### Reference integrity + +PASS. + +The suite verifies: + +- <=16 live refs; +- uniqueness; +- non-dangling identity; +- binding commitments remain referenced; +- historical facts survive reclamation; +- IDs are not recycled. + +A deterministic sequence explicitly reaches slot exhaustion, expiry, reclamation, reuse, and historical verification. + +### Eligibility and expiry + +PASS. + +Eligibility mutation does not release O or alter Remaining. + +Expiry can release O without zeroing Remaining, preserving the distinction between non-enforceability and fulfillment. + +### Direct-transfer discrimination + +PASS. + +The suite separately tracks: + +```text +Standby-delivered protected output +unrelated donated protected output +``` + +This establishes that Beneficiary receipt by itself is not fulfillment. + +### Custody + +PASS. + +Hook and ExerciseRouter are checked for zero protocol-created custody in both currencies after actions and globally. + +### Generalization + +PASS. + +The generalized campaign materially differs from canonical: + +- oneForZero protected direction; +- protected output is currency0; +- 18/8 decimal currencies; +- different service ticks; +- different LP range; +- different fee; +- different liquidity. + +### Campaign quality + +PASS. + +The deterministic campaigns reached: + +- admitted and refused O1; +- completed and refused O2; +- partial and full exercise; +- protected and opposite swaps; +- backing-refused swaps and liquidity; +- successful liquidity additions/removals; +- eligibility churn; +- expiry; +- direct transfers; +- orphan causal probes; +- 16 simultaneous refs; +- reference reuse. + +This was sufficient to reject the possibility of a semantically empty all-revert campaign. + +--- + +## 16. Independent G-I Determination + +ChatGPT independently assessed all 23 conditions as satisfied. + +Final determination: + +> **GI — Full Stateful Invariant Verification: COMPLETE** +> **G-I: PASS / CLOSED** +> **No production correction required.** +> **F9 — Canonical Acceptance is the next authorized implementation slice.** + +This was an independent closure decision, not acceptance of Claude’s advisory assessment by default. + +--- + +## 17. Minor Non-Blocking Report Correction + +One wording issue was identified in Claude’s Session 15 log: + +> “Twelve generated actions, all of which can succeed and all of which can be refused.” + +This is not literally true for every action category. + +For example: + +- time advancement is not a production request with success/refusal semantics; +- orphan-evidence probing is intentionally expected to fail. + +The issue was classified as a non-blocking report wording problem, not a code or gate defect. + +A more precise description would be: + +> “Twelve generated action selectors spanning successful, rejected, lifecycle, environmental, and adversarial transitions.” + +No code change was required. + +--- + +## 18. User Decision: Re-run Coverage After GI + +After G-I closure, the user proposed re-running coverage. + +ChatGPT agreed, but explicitly classified it as: + +> **post-GI diagnostic evidence, not part of G-I closure.** + +The reasoning was: + +- GI added substantial new test infrastructure; +- production code did not change; +- coverage could reveal newly exercised production surfaces; +- coverage must not be used as semantic proof; +- no tests should be added merely to improve percentages; +- any newly observed uncovered branch should be classified against frozen obligations rather than automatically chased. + +The user also correctly challenged an initial prompt phrase: + +> “Use the same coverage methodology…” + +because Claude was operating in a fresh session and should not depend on conversational memory. + +The prompt was strengthened to require Claude to reconstruct the exact established coverage methodology from repository artifacts and stop if it could not do so unambiguously. + +This reinforced the project’s reconstructibility principle. + +--- + +## 19. Post-GI Coverage Execution + +Claude reconstructed the prior methodology as: + +```text +forge coverage +forge coverage --report debug +``` + +with: + +- default profile; +- no filtering; +- no `--match`; +- no `--ir-minimum`; +- no `foundry.toml` change; +- production aggregates recomputed from per-file rows; +- separate Standby core and all-src aggregates; +- lines/statements/branches/functions reported separately. + +The post-GI core result was: + +```text +Lines 99.42% -> 99.42% (514/517) +Statements 98.33% -> 98.52% (531/540 -> 532/540) +Branches 91.35% -> 92.31% (95/104 -> 96/104) +Functions 100% -> 100% (107/107) +``` + +Exactly one production surface became newly covered: + +> the `beforeRemoveLiquidity` refusal for liquidity removal proposed through an untrusted perimeter. + +This was significant because it was the first post-F8D candidate specifically identified as a meaningful GI input. + +No new frozen verification obligation was discovered. + +--- + +## 20. Coverage Compile Obstacle and Review + +The coverage run initially failed with `Stack too deep` in the invariant handler because `forge coverage` disables optimization. + +Claude had two options: + +1. use `--ir-minimum`, changing the reconstructed coverage methodology; +2. reduce the local stack frame in the test handler. + +Claude chose the second option by extracting generated swap amount and price-limit selection into helpers. + +ChatGPT independently reviewed this decision and accepted it because: + +- it was required to preserve the established coverage methodology; +- it was a test-side compile-time frame-size refactor; +- it did not change production; +- it did not add tests for coverage; +- deterministic campaign counters remained byte-for-byte identical; +- default and CI verification still passed. + +Therefore the change did not reopen G-I and was not considered scope leakage. + +--- + +## 21. Final Coverage Assessment + +The coverage outcome was considered excellent, but deliberately not treated as proof of correctness. + +The key interpretation was: + +- line coverage remained extremely high; +- statement and branch coverage improved; +- functions remained at 100%; +- the one newly covered branch was semantically meaningful; +- remaining gaps had already been classified; +- no reason existed to chase 100% branch coverage artificially. + +The stronger safety story is the combination of: + +- unit testing; +- integration testing; +- fuzz testing; +- independent derivation checks; +- stateful invariant verification; +- generalized direction/token-decimal testing; +- explicit coverage diagnostics. + +--- + +## 22. Gas / Coverage Baseline Decision + +The user asked whether gas and coverage should be rerun later now that production code was complete. + +The derived policy was: + +### Gas + +Keep the existing post-F8D production gas snapshot as the current baseline. + +Do not rerun merely because GI added tests. + +Rerun if: + +- production code changes; +- or at final F10 / submission readiness for a final engineering baseline. + +### Coverage + +The post-GI refresh becomes the primary current coverage baseline. + +F9 does not automatically require another refresh if it adds acceptance tests only. + +At F10, rerunning both gas and coverage is useful as a final submission-state evidence package. + +### General rule + +> **Any production-code change after GI should trigger renewed engineering baselines after the affected prior gate has been re-established.** + +--- + +## 23. User Assessment: Did the Project Do Well on Coverage and Gas? + +The user asked whether the project’s results should be considered strong or whether more improvement was warranted. + +The conclusion was: + +### Coverage + +Excellent. + +Not merely because of the percentages, but because remaining gaps were inspected and classified, and GI supplied semantic/global closure that raw coverage cannot provide. + +### Gas / size + +Healthy. + +No deployment-size pressure or concrete hot-path cost problem was identified. + +Further optimization may be theoretically possible, but no evidence showed that speculative optimization would have higher value than completing F9/F10. + +### Priority decision + +The highest-value next work is not chasing 100% branch coverage or arbitrary gas reduction. + +It is: + +> **F9 — Canonical Acceptance** + +because F9 demonstrates that a fresh system deterministically realizes the full canonical economic story through production interfaces. + +--- + +## 24. Status Transition + +After independent GI closure and the post-GI coverage refresh, the user authorized the normal status-only update. + +The intended status was: + +- **GI — Full Stateful Invariant Verification: COMPLETE** +- **G-I: PASS** +- **F9 — Canonical Acceptance: next authorized implementation slice / current blocker** + +The project-status update was intentionally restricted to status fields only. + +Coverage figures, invariant architecture, implementation details, review commentary, and retrospective observations were explicitly excluded from `docs/project-status.md`. + +--- + +## 25. Methodology Observations from Session 15 + +### Observation 1 — Stateful verification should begin only after responsibility convergence + +GI worked cleanly because production semantics had already been assigned and closed through F8D. + +This prevented invariant failures from becoming ambiguous “GI design work.” + +The sequence was: + +```text +semantic ownership +→ implementation ownership +→ local gate closure +→ compositional invariant verification +``` + +This supports the Implementation Convergence Principle. + +### Observation 2 — Independent oracle construction matters more than invariant syntax + +The strongest parts of GI were not the presence of `invariant_*` functions themselves. + +They were the intentional disagreement surfaces: + +- independent S arithmetic; +- full-history O reconstruction versus bounded-index production derivation; +- ghost fulfillment versus production Remaining; +- Beneficiary balance history versus protocol delivery accounting. + +A stateful invariant suite can still be weak if its expected state is derived from the same logic as production. + +### Observation 3 — Campaign diagnostics are part of evidence quality + +A green stateful campaign is insufficient if: + +- no O1 succeeds; +- O never becomes positive; +- no O2 completes; +- no backing-threatening O3 attempt occurs; +- no reference churn occurs. + +Session 15 treated reachability diagnostics as evidence-quality checks rather than protocol semantics. + +That distinction was productive. + +### Observation 4 — Coverage observations should be mapped to normative owners + +The post-F8D uncovered paths were not automatically converted into new tests. + +Each was evaluated against: + +- frozen invariant responsibility; +- production reachability; +- prior slice ownership; +- GI’s compositional boundary. + +This prevented coverage from silently becoming a new specification. + +### Observation 5 — Fresh implementation sessions must be repository-reconstructible + +The user’s challenge about “use the same coverage methodology” exposed a broader process rule: + +> A new implementation session should not need hidden conversational continuity to reproduce prior engineering procedure. + +Where a prior method matters, the prompt should require reconstruction from checked-in evidence. + +This strengthens auditability and handoff quality. + +### Observation 6 — Verification tooling may require non-semantic refactoring + +The coverage-only stack-depth issue showed that instrumentation can expose build constraints not present in the optimized verification profile. + +The correct response was not to change semantics or silently alter methodology. + +Instead: + +- preserve methodology; +- make the smallest behavior-preserving test-side refactor; +- rerun gate-relevant verification; +- disclose the change. + +This is a useful precedent for future engineering evidence work. + +### Observation 7 — “Complete production code” does not mean “never measure again” + +Post-F8D gas and post-GI coverage are milestone baselines. + +A later production change should trigger renewed measurements. + +F10 should produce the final submission-state baseline even if the implementation remains unchanged. + +--- + +## 26. Final Session 15 Determination + +Session 15 achieved its intended responsibility. + +### GI + +**COMPLETE** + +### G-I + +**PASS / CLOSED** + +### Production defects found + +**None** + +### Production changes required + +**None** + +### Post-GI coverage + +```text +Lines 99.42% +Statements 98.52% +Branches 92.31% +Functions 100% +``` + +### New verification obligation discovered by coverage + +**None** + +### Current blocker + +**F9 — Canonical Acceptance** + +--- + +## 27. Handoff State + +The repository is now in a strong verification state: + +```text +F0–F8D COMPLETE +GI COMPLETE +G-I PASS / CLOSED +F9 NEXT AUTHORIZED SLICE +F10 NOT YET AUTHORIZED +``` + +The next session should reconstruct and derive the exact F9 responsibility from the frozen acceptance requirements and implementation plan before authorizing implementation. + +F9 should remain distinct from GI: + +- GI proved adversarial temporal/compositional safety; +- F9 must prove deterministic realization of the canonical accepted economic story through production interfaces. + +That distinction should remain explicit in the next-session handoff. diff --git a/docs/prompts/session-15-gi-full-stateful-invariant-verification.md b/docs/prompts/session-15-gi-full-stateful-invariant-verification.md new file mode 100644 index 0000000..3ebd48a --- /dev/null +++ b/docs/prompts/session-15-gi-full-stateful-invariant-verification.md @@ -0,0 +1,1788 @@ +# Standby — Session 15 + +## GI — Full Stateful Invariant Verification + +You are implementing the next authorized Standby verification slice: + +> **GI — Full Stateful Invariant Verification** + +The preceding implementation slices are complete and independently gate-closed: + +```text +F0 — Foundation COMPLETE +F1 — Deterministic Economic Fixture COMPLETE +F2 — Eligibility Registry COMPLETE +F3 — StandbyHook Trust + PES Configuration COMPLETE +F4 — Commitment Storage / Bounded References COMPLETE +F5 — Authoritative Derivation Kernel COMPLETE +F6A — Preliminary O3 Enforcement COMPLETE +F7 — O1 Commitment Admission COMPLETE +F6B — O3 Bounded Enforcement COMPLETE +F8A — Exercise Authorization COMPLETE +F8B — Protected PoolManager Execution COMPLETE +F8C — Authoritative Settlement / Direct Delivery COMPLETE +F8D — O2 Causal Finalization / Remaining Reduction COMPLETE +GI — Full Stateful Invariant Verification CURRENT +F9 — Canonical Acceptance NOT AUTHORIZED +F10 — Demo Instrumentation NOT AUTHORIZED +``` + +The last closed gate is: + +> **G8D — PASS / CLOSED** + +GI is the only authorized current slice. + +No production semantic slice is intentionally incomplete before GI. + +--- + +# 1. Clean Rule / Authority Boundary + +Apply the established ownership rule: + +> **`CLAUDE.md` owns permanent operating behavior.** +> +> **`.claude/rules/*` owns permanent Solidity/testing conventions.** +> +> **Session prompts own only slice-specific objective, scope, requirements, prohibitions, file boundaries, gate evidence, and completion boundary.** + +Where permanent operating, Solidity, or testing behavior is already defined in those artifacts, follow it rather than restating or modifying it here. + +This session prompt owns only the GI-specific requirements below. + +--- + +# 2. Authoritative Sources + +Before changing tests or production code, inspect the relevant frozen artifacts: + +```text +docs/context.md +docs/economic-agreement.md +docs/mechanism.md +docs/spec.md +docs/architecture.md +docs/state-machine.md +docs/invariants.md +docs/testing-strategy.md +docs/uniswap-v4-realization.md +docs/implementation-plan.md +``` + +Inspect: + +```text +docs/project-status.md +``` + +for current status only. + +Also inspect the current production implementation and existing F0–F8D test suite. + +At minimum inspect the current production surfaces for: + +```text +StandbyHook +ExerciseRouter +EligibilityRegistry +PoolManager integration +commitment establishment +ordinary protected swaps +ordinary opposite-direction swaps +liquidity actions +O2 exercise +bounded commitment references +authoritative Supporting Capacity derivation +authoritative Capacity Obligation derivation +eligibility mutation +``` + +Inspect the existing deterministic fixture/deployer architecture before creating invariant fixture setup. + +If a material discrepancy exists between the frozen artifacts and current implementation, surface it rather than silently redefining Standby semantics. + +--- + +# 3. GI Objective + +Implement the exact accepted GI responsibility: + +> **GI verifies temporal and compositional safety of the completed Standby realization by adversarially composing authoritative O1, O2, O3, lifecycle, eligibility, and relevant environmental actions through production interfaces and independently checking that every reachable completed state preserves backing, commitment conservation, fulfillment attribution, bounded-reference integrity, causal isolation, authority/rejection atomicity, custody integrity, and required verification-domain completeness.** + +GI is the first slice that introduces true **stateful invariant testing**. + +Existing verification before GI principally includes: + +```text +unit +integration +fuzz +periphery / adversarial +``` + +GI adds: + +```text +persistent multi-operation histories ++ +adversarial action sequencing ++ +reachable-state exploration ++ +independent reference/oracle checks ++ +global invariant closure +``` + +GI does not define new protocol behavior. + +--- + +# 4. GI Verification Boundary + +GI must answer: + +> **Can arbitrary sequences of successful and rejected Standby-relevant actions drive the completed production realization into an authoritative state that violates a frozen invariant or authoritative derivation?** + +GI must therefore verify composition across: + +```text +O1 commitment establishment +O2 authorization / execution / settlement / delivery / finalization +O3 backing-affecting transitions +ordinary protected swaps +ordinary opposite-direction swaps +liquidity changes +eligibility mutation +time / expiry evolution +bounded-reference churn +repeated / partial fulfillment +failed transitions +relevant unrelated external token transfers +``` + +GI must not introduce: + +```text +new commitment semantics +new exercise semantics +new backing formulas +new eligibility rules +new lifecycle transitions +new obligation-release causes +new fulfillment semantics +new causal-state semantics +new custody semantics +``` + +Those responsibilities are already owned by the frozen artifacts and completed F0–F8D implementation. + +--- + +# 5. Required Stateful Invariant Architecture + +Implement a genuine Foundry handler-driven stateful invariant suite. + +The required conceptual structure is: + +```text +production fixture + ↓ +stateful adversarial handler + ↓ +production interfaces + ↓ +authoritative production state + ↓ +independent reference / history observations + ↓ +invariant assertions +``` + +A likely file shape is: + +```text +test/invariant/StandbyInvariant.t.sol +test/invariant/StandbyInvariantHandler.sol +``` + +Additional narrowly scoped invariant helpers or independent oracle helpers are permitted where necessary. + +Exact filenames are not normative. + +The required property is a real stateful invariant campaign, not deterministic tests merely named `invariant`. + +--- + +# 6. Production-Only Verification Environment + +GI evidence must exercise the production realization. + +Use the real production components required by the current architecture, including as applicable: + +```text +PoolManager +StandbyHook +EligibilityRegistry +ExerciseRouter +ActorAwareTestRouter where required +production commitment path +production ordinary swap path +production liquidity path +canonical mock currencies +canonical deployment/configuration path +``` + +Do not use: + +```text +StandbyHookHarness +``` + +as authoritative GI evidence. + +Do not directly seed or mutate economically authoritative state such as: + +```text +Remaining Entitlement +Original Entitlement +bounded commitment references +Supporting Capacity +Capacity Obligation +validity +exercisability +fulfillment +O2 causal lifecycle state +``` + +Fixture construction may initialize the production realization through its legitimate configuration/bootstrap paths. + +--- + +# 7. Stateful Handler Responsibility + +The handler is: + +> **an adversarial transaction generator, not a semantic safety pre-filter.** + +The handler must generate both actions that can succeed and actions that should reject. + +Expected reverts are part of GI evidence. + +Do not constrain inputs merely so that every operation succeeds. + +Bound only inputs that are mechanically impossible, structurally meaningless, or likely to create generator noise rather than useful semantic exploration, such as: + +```text +invalid TickMath domain +unbounded economically meaningless token amounts +unknown/unbounded actor identities +structurally impossible identifiers +``` + +Do not encode Standby's safety predicates into the handler merely to avoid reverts. + +--- + +# 8. Minimum Stateful Action Universe + +The handler must support, directly or through semantically equivalent production operations: + +```text +establishCommitment(...) +ordinaryProtectedSwap(...) +ordinaryOppositeSwap(...) +addLiquidity(...) +removeLiquidity(...) +exercise(...) +advanceTime(...) +setBeneficiaryEligibility(...) +setTraderEligibility(...) +setLiquidityEligibility(...) +directTransferProtectedTokenToBeneficiary(...) +``` + +Additional handler actions require a traceable GI verification need. + +Do not add actions solely to increase raw fuzz activity. + +`directTransferProtectedTokenToBeneficiary(...)` is intentionally not Standby fulfillment. + +It exists to verify that ordinary receipt of protected tokens by the Beneficiary cannot create fulfillment. + +--- + +# 9. Persistent Actor Universe + +Use a bounded persistent actor universe sufficient to test stable authority relationships across multi-operation histories. + +At minimum support logical identities capable of representing: + +```text +registry admin +commitment-establishment authority +Beneficiary A +Beneficiary B +authorized exerciser +unauthorized exerciser +eligible trader +ineligible trader +eligible LP +ineligible LP +outsider +``` + +One address may hold multiple roles in a particular campaign where legitimate. + +However, the invariant environment must preserve enough separation to verify that: + +```text +administrative authority +exercise authority +Beneficiary eligibility +trader eligibility +liquidity eligibility +ordinary invocation capability +``` + +cannot silently substitute for one another. + +Avoid unconstrained fuzzed caller addresses where doing so destroys stable authority relationships across the generated sequence. + +--- + +# 10. Authoritative Production State + +Treat the production realization as authoritative. + +Relevant production facts include, as applicable: + +## PoolManager + +```text +current pool state +price / tick +liquidity / executable topology +actual successful swap effects +``` + +## StandbyHook + +```text +configured PES facts +commitment facts +Original Entitlement +Remaining Entitlement +bounded live references +historical commitment identity +next commitment identity +production Supporting Capacity derivation +production Capacity Obligation derivation +transaction-scoped O2 causal state where behaviorally observable +``` + +## EligibilityRegistry + +```text +Beneficiary eligibility +trader eligibility +liquidity eligibility +``` + +## Token state + +```text +Beneficiary balances +StandbyHook balances +ExerciseRouter balances +other balances required for delivery/custody evidence +``` + +## Environment + +```text +block.timestamp +``` + +Do not create test-owned authoritative substitutes for production truth. + +--- + +# 11. Ghost / Reference State Boundary + +Ghost state is permitted only for independent verification and historical observation. + +The governing rule is: + +> **Ghost state may remember history that production does not persist for verification purposes, or independently calculate a normative oracle; it may not prescribe expected production state by duplicating the Standby state machine.** + +Permitted ghost/reference state includes, as needed: + +```text +successfully created commitment IDs +immutable original commitment snapshots +previously observed Remaining values +independently tracked successful fulfillment by commitment +successful action counters +failed / rejected action counters +observed Beneficiary delivery quantities +reference-slot / history observations +``` + +A permitted quantity is: + +```text +ghostFulfilled[commitmentId] +``` + +It may increase only after an independently observed successfully completed authoritative O2. + +GI may then assert: + +```text +Original - Remaining == ghostFulfilled +``` + +Do not maintain a parallel lifecycle such as: + +```text +ghostIsValid +ghostIsExercisable +ghostIsBinding +ghostIsExpired +ghostExpectedRemaining +ghostProtocolState +``` + +where those values merely duplicate Standby's own state machine. + +--- + +# 12. Independent Derivation Requirement + +Where GI compares a production-derived quantity against an expected result, the expected result must be independently expressed. + +In particular: + +```text +referenceS +referenceO +``` + +must not be calculated by calling the same production helper used to obtain: + +```text +productionS +productionO +``` + +The independent oracle may use: + +```text +authoritative PoolManager state +immutable commitment facts +current Remaining +current time +frozen qualification semantics +independent mathematical/reference calculations +``` + +but must remain sufficiently independent to detect a correlated production derivation defect. + +Do not create false independence through a wrapper around the production implementation. + +--- + +# 13. GI-A — Independent Economic Backing + +Across every completed generated action, verify where applicable: + +```text +referenceS == productionS +referenceO == productionO +referenceS >= referenceO +``` + +`referenceS` must be independently derived from authoritative production resource state. + +`referenceO` must be independently derived from authoritative commitment state and frozen binding/release semantics. + +These properties must remain true across histories involving: + +```text +multiple commitments +ordinary protected swaps +opposite-direction swaps +partial fulfillment +full fulfillment +eligibility mutation +liquidity changes +expiry +reference reuse +failed operations +``` + +Do not assume S or O is stable between handler actions. + +--- + +# 14. GI-B — Commitment Conservation + +For every known commitment verify: + +```text +Remaining <= Original +``` + +and: + +```text +Remaining is monotonic non-increasing +``` + +Verify immutable admitted commitment facts remain unchanged. + +Verify: + +```text +Original - Remaining + == +independently tracked successful attributable fulfillment +``` + +where applicable. + +The following must not manufacture fulfillment or reduce Remaining as though fulfillment occurred: + +```text +ordinary protected swap +ordinary opposite swap +liquidity add +liquidity removal +expiry +Beneficiary eligibility mutation +trader eligibility mutation +liquidity eligibility mutation +direct token transfer +failed O1 +failed O2 +failed O3 +``` + +Expiry may release backing obligation according to frozen non-fulfillment semantics without rewriting historical Remaining to zero. + +Eligibility loss must not release an otherwise binding obligation. + +--- + +# 15. GI-C — Fulfillment Attribution / Exactness + +For every successfully completed O2 verify: + +```text +exactly one commitment is affected +fulfillment amount == q +Remaining[target] decreases exactly q +ghostFulfilled[target] increases exactly q +unrelated commitments are not reduced +``` + +Under canonical mock-transfer semantics also verify: + +```text +authoritative Beneficiary protected-output increase == q +``` + +The following alone must not create fulfillment: + +```text +authorization +protected execution without completed O2 +settlement alone +delivery alone +ordinary swap +liquidity action +direct token transfer +expiry +eligibility mutation +failed O2 +``` + +One successful execution/delivery must not be attributed more than once. + +One commitment's fulfillment evidence must not reduce another commitment. + +Repeated partial exercise and final exhaustion must remain exact. + +--- + +# 16. GI-D — O2 Causal Isolation + +Verify across stateful histories that O2 causal evidence remains transaction-scoped and non-reusable. + +After every completed top-level handler action, no reusable O2 authorization/execution/finalization evidence may remain capable of later reducing entitlement. + +Campaigns must be capable of exposing contamination through histories equivalent to: + +```text +O2(C1) +→ failed O2(C2) +→ O2(C1) +→ O2(C2) +``` + +and: + +```text +failed O2(C1) +→ valid O2(C2) +``` + +and: + +```text +successful O2(C1) +→ later O2(C2) +``` + +Verify: + +```text +prior success cannot authorize later unrelated fulfillment +failed context cannot authorize later fulfillment +one commitment's context cannot substitute for another +replay cannot create a second Remaining reduction +completed top-level O2 leaves no reusable causal evidence +``` + +If nested O2 is structurally forbidden by the production lifecycle, verify that the production architecture remains fail-closed. + +Do not invent a new supported nested-exercise path solely for GI. + +--- + +# 17. GI-E — Bounded Reference Integrity + +Across commitment/lifecycle churn verify: + +```text +live bounded references <= 16 +``` + +For every nonzero reference verify: + +```text +reference is unique +reference resolves to a real historical commitment +reference is not dangling +``` + +Verify historical commitment identity remains valid after reference-slot reclamation and reuse. + +Relevant histories include equivalents of: + +```text +multiple O1 +→ partial fulfillment +→ full fulfillment +→ expiry +→ reference reclamation +→ new O1 +→ slot reuse +→ later old/new commitment interaction +``` + +Commitment IDs must not be recycled. + +Reference-slot reuse must not rewrite historical commitment facts. + +--- + +# 18. Reference Reclaimability + +Verify that bounded live reference capacity becomes reclaimable only through frozen permanent non-binding causes. + +For the current realization these include, as applicable: + +```text +Remaining == 0 through authoritative fulfillment +canonical expiry / non-fulfillment release +``` + +The following must not independently make an otherwise binding commitment reclaimable: + +```text +Beneficiary eligibility loss +trader eligibility mutation +liquidity eligibility mutation +resource pressure +ordinary swap +liquidity transition +direct token transfer +failed exercise +``` + +Do not convert slot-management convenience into a new lifecycle semantic. + +--- + +# 19. GI-F — Authority / Rejection Integrity + +Generate invalid, unauthorized, ineligible, and backing-threatening requests through production surfaces. + +Rejected transitions must leave no prohibited authoritative economic residue attributable to the failed attempt. + +Observe relevant pre/post state according to the attempted operation, including where applicable: + +```text +commitment existence +immutable commitment facts +Remaining +reference membership +reference count +aggregate O +Supporting Capacity +PoolManager state +Beneficiary balance +fulfillment observations +causal-context behavior +Hook / Router custody +``` + +The required property is: + +> **No failed Standby operation may leave a prohibited authoritative Standby economic consequence or latent state capable of changing later canonical behavior.** + +Do not require unrelated legitimate external state to remain unchanged merely because a later Standby call fails. + +--- + +# 20. O3 Stateful Enforcement + +GI must exercise histories in which authentic positive Capacity Obligation exists before backing-affecting operations are attempted. + +Required sequence classes include equivalents of: + +```text +O1 +→ ordinary protected swap toward backing boundary +→ destructive protected swap attempt +``` + +and: + +```text +multiple O1 +→ liquidity removal attempt +``` + +and: + +```text +O1 +→ Beneficiary eligibility loss +→ backing-threatening O3 attempt +``` + +Verify that rejection cannot make the request acceptable by: + +```text +reducing Remaining +manufacturing fulfillment +releasing a still-binding commitment +rewriting admitted terms +corrupting reference state +``` + +Equality at the backing boundary must remain accepted where existing F6B semantics permit exact sufficiency. + +--- + +# 21. Liquidity Perimeter + +The post-F8D coverage report identified untrusted-perimeter liquidity removal as a GI-relevant candidate because it intersects existing O3 enforcement and authority responsibilities. + +Where reachable through actual production interfaces, exercise sufficient variants of: + +```text +authorized liquidity action +unauthorized liquidity action +eligible LP action +ineligible LP action +backing-preserving removal +backing-threatening removal +``` + +to verify that caller/path variation cannot bypass effect-defined backing protection. + +Do not introduce new liquidity semantics merely to improve branch coverage. + +--- + +# 22. Direct Beneficiary Token Transfer + +Support unrelated direct protected-token transfers to the authoritative Beneficiary. + +After such a transfer: + +```text +Beneficiary balance may increase +``` + +but verify: + +```text +Remaining unchanged +ghostFulfilled unchanged +no Standby fulfillment created +no commitment fact rewritten +no obligation released solely because of receipt +``` + +This action exists to establish: + +> **Beneficiary token receipt is not sufficient Standby fulfillment.** + +Only the canonical attributable O2 path may create fulfillment. + +--- + +# 23. Custody Integrity + +Under protocol-controlled flows verify, where applicable: + +```text +StandbyHook protected-output balance == 0 +ExerciseRouter protected-output balance == 0 +``` + +Do not count deliberate unrelated donations as protocol-created custody. + +If unrelated donations are intentionally included, account for them separately so GI can distinguish: + +```text +protocol-created custody +``` + +from: + +```text +unrelated external donation +``` + +Do not use Router or Hook token custody as substitute Beneficiary-delivery evidence. + +--- + +# 24. Failed-Operation Sequence Integrity + +GI must verify not only immediate rollback but later sequence correctness. + +Required sequence classes include equivalents of: + +```text +failed O1 +→ later valid O1 +``` + +```text +failed O2(C1) +→ valid O2(C2) +``` + +```text +failed backing-threatening O3 +→ later valid O2 +``` + +```text +failed liquidity action +→ later valid ordinary swap +``` + +A failed operation must not leave: + +```text +stale causal evidence +partial commitment facts +hidden obligation change +false fulfillment +reference corruption +partial delivery +partial Remaining mutation +``` + +capable of changing a later authoritative result. + +--- + +# 25. Required Stateful Sequence Classes + +Ensure the campaigns can meaningfully reach sequence classes equivalent to: + +## Backing pressure + +```text +O1 +→ ordinary protected swap +→ backing-threatening ordinary swap attempt +→ opposite-direction swap +→ partial O2 +→ protected swap +``` + +## Eligibility churn + +```text +O1 +→ Beneficiary eligibility off +→ O3 attempt +→ Beneficiary eligibility on +→ O2 +``` + +## Multiple commitments + +```text +O1(C1) +→ O1(C2) +→ partial O2(C1) +→ ordinary swap +→ O2(C2) +→ later O2(C1) +``` + +## Expiry / reuse + +```text +O1 +→ advance time +→ expiry +→ new O1 +→ reference reuse +``` + +## Fulfillment churn + +```text +O1 +→ partial O2 +→ ordinary swap +→ second partial O2 +→ full exhaustion +``` + +## Causal contamination + +```text +failed O2(C1) +→ valid O2(C2) +``` + +## External-delivery discrimination + +```text +O1 +→ direct protected-token transfer to Beneficiary +→ verify no fulfillment +→ valid O2 +``` + +These are required semantic classes. + +They need not all be implemented as deterministic scripted tests if equivalent stateful histories are demonstrably reached by the campaign. + +--- + +# 26. Campaign Diagnostics + +A green invariant campaign is insufficient if it exercises little meaningful protocol behavior. + +Maintain diagnostic counters sufficient to report activity for: + +```text +successful O1 +rejected O1 + +successful O2 +failed O2 + +partial O2 +full O2 + +ordinary protected swaps +ordinary opposite-direction swaps +rejected backing-threatening swaps + +liquidity activity +rejected liquidity activity where applicable + +Beneficiary eligibility mutation +trader eligibility mutation +liquidity eligibility mutation + +time advancement / expiry +multiple commitments +reference reclamation / reuse where reachable +direct Beneficiary transfers +``` + +Counters are test diagnostics only. + +Do not turn exact counter thresholds into protocol semantics. + +However: + +> **A green campaign with zero successful O2 does not establish meaningful fulfillment-conservation evidence.** + +Similarly: + +> **A green campaign that never reaches authentic positive `O` does not establish meaningful O3-with-obligation evidence.** + +Tune action generation only enough to produce semantically useful reachable histories without converting the handler into a safety pre-filter. + +--- + +# 27. Canonical and Generalized Campaigns + +GI must not prove correctness only for the canonical demo identity/direction. + +At minimum provide: + +## Canonical campaign + +```text +MockUSTB = currency0 +MockUSDC = currency1 +protected direction = zeroForOne +``` + +## Generalized campaign + +Provide a supported non-canonical configuration sufficient to verify: + +```text +protected direction = oneForZero +different token ordering / protected-output identity where supported +``` + +Also preserve the frozen currency-denominational verification obligation. + +Where supported by the current realization, include asymmetric currency-decimal configuration sufficient to expose dependence on: + +```text +both currencies being 6 decimals +both currencies using equal decimals +1e6 being treated as a universal economic scale +``` + +Supporting Capacity and Capacity Obligation must remain denominated in the same raw units of the protected output currency. + +Do not invent support outside the frozen/current realization domain. + +--- + +# 28. Post-F8D Diagnostic Observations + +Post-F8D coverage observations may inform GI only where they intersect frozen responsibilities. + +Include behaviorally where appropriate: + +```text +untrusted-perimeter liquidity removal +nested / substituted exercise attribution +reachable unresolved exercise-delta fail-closed behavior +``` + +Do not create separate GI obligations merely to cover: + +```text +causal-position read-surface refusal +extreme tick-bound clamping +``` + +Extreme tick-bound handling remains principally an F5 derivation concern unless GI exposes a reachable compositional counterexample. + +Do not manufacture unreachable states solely to increase coverage. + +--- + +# 29. G-I — Full Stateful Invariant Gate + +Implementation and tests must provide evidence for all 23 conditions. + +Claude may provide an advisory assessment but does not close G-I. + +## G-I-1 — Supporting Capacity Equivalence + +Prove: + +```text +referenceS == productionS +``` + +across applicable reachable states. + +## G-I-2 — Capacity Obligation Equivalence + +Prove: + +```text +referenceO == productionO +``` + +across applicable reachable states. + +## G-I-3 — Backing Sufficiency + +Prove: + +```text +referenceS >= referenceO +``` + +in every reachable authoritative state with binding obligation. + +## G-I-4 — Remaining Bound + +Prove for every commitment: + +```text +Remaining <= Original +``` + +## G-I-5 — Immutable Commitment Facts + +Prove admitted immutable commitment facts never change. + +## G-I-6 — Remaining Monotonicity + +Prove: + +```text +Remaining never increases +``` + +## G-I-7 — Fulfillment Conservation + +Prove: + +```text +Original - Remaining + == +independently tracked successful attributable fulfillment +``` + +## G-I-8 — Expiry Is Not Fulfillment + +Prove expiry/non-fulfillment release does not manufacture fulfillment or rewrite Remaining as though fulfillment occurred. + +## G-I-9 — Eligibility Mutation Integrity + +Prove eligibility changes do not: + +```text +manufacture fulfillment +reduce Remaining +release otherwise binding O +``` + +## G-I-10 — Ordinary Swap Non-Fulfillment + +Prove ordinary swaps never create fulfillment. + +## G-I-11 — Liquidity Non-Fulfillment + +Prove liquidity actions never create fulfillment. + +## G-I-12 — Direct Transfer Non-Fulfillment + +Prove direct protected-token transfers never create fulfillment. + +## G-I-13 — Exact O2 Attribution + +For every successful O2 prove: + +```text +exactly one commitment +exactly q fulfillment +exactly q Remaining reduction +``` + +## G-I-14 — Exact Beneficiary Delivery + +Under canonical mock semantics prove successful O2 delivers exactly: + +```text +q +``` + +protected output to the authoritative Beneficiary. + +## G-I-15 — Failed O2 Integrity + +Prove failed O2 produces: + +```text +zero fulfillment +zero Remaining reduction +zero prohibited authoritative residue +``` + +## G-I-16 — Protocol Custody Integrity + +Under protocol-controlled flows prove no protected-output custody remains in: + +```text +StandbyHook +ExerciseRouter +``` + +excluding separately accounted unrelated donations. + +## G-I-17 — Reference Bound + +Prove: + +```text +live references <= 16 +``` + +## G-I-18 — Reference Validity + +Prove every nonzero reference is: + +```text +unique +non-dangling +historically valid +``` + +## G-I-19 — History Across Reuse + +Prove historical commitment identity and immutable facts survive bounded-reference slot reuse. + +## G-I-20 — Reclamation Cause Integrity + +Prove only frozen permanent non-binding causes permit economic live-reference reclamation. + +## G-I-21 — O2 Context Isolation + +Prove no reusable cross-transaction O2 authorization/execution/finalization context survives completed top-level actions. + +## G-I-22 — Generalization + +Prove canonical and supported generalized protected-direction/configuration campaigns pass. + +## G-I-23 — Campaign Quality + +Provide diagnostic evidence that campaigns actually exercise meaningful: + +```text +O1 +O2 +O3 +swap +liquidity +lifecycle +eligibility +success +rejection +multi-commitment +partial fulfillment +full fulfillment +``` + +behavior rather than achieving a trivial green result. + +--- + +# 30. Assertion Shape + +Not every G-I property must be encoded as a top-level Foundry: + +```solidity +function invariant_...() +``` + +Use the proof shape appropriate to the property. + +Continuous global properties naturally belong in invariant functions, for example: + +```text +S >= O +Remaining <= Original +reference integrity +custody +``` + +Transition-specific exactness may be checked immediately around handler operations, for example: + +```text +successful O2 changed exactly one Remaining by q +failed O2 changed no fulfillment state +direct transfer did not change fulfillment +failed operation left no prohibited residue +``` + +Assertions executed inside handler-generated histories are valid GI evidence. + +Do not weaken semantic proof coverage merely to fit a particular Foundry function shape. + +--- + +# 31. Production-Code Boundary + +GI is presumed to be a verification-only slice. + +Do not proactively modify production semantics to make the invariant suite easier to implement or pass. + +If GI discovers a genuine production counterexample: + +1. preserve or minimize the failing sequence; +2. identify the violated frozen invariant or verification obligation; +3. trace the defect to its existing normative implementation owner; +4. record the finding in the Session 15 log; +5. report the affected previous slice/gate; +6. do not invent a new GI-owned semantic repair. + +Potential existing owners include: + +```text +F4 +F5 +F6B +F7 +F8A +F8B +F8C +F8D +``` + +If a production correction is unambiguously required by already-frozen semantics, keep it minimal and explicitly report: + +```text +violated frozen property +existing normative owner +counterexample +root cause +production change +affected previous gate +``` + +Do not silently patch production code while constructing the invariant suite. + +--- + +# 32. Responsibility Leakage / Out of Scope + +GI verifies composition of already-owned responsibilities. + +It must not absorb those responsibilities. + +## F4 remains owner of + +```text +commitment identity +bounded-reference representation +historical commitment persistence +``` + +## F5 remains owner of + +```text +authoritative derivation kernel +Supporting Capacity derivation +Capacity Obligation derivation +prospective derivation +``` + +## F6B remains owner of + +```text +O3 backing enforcement with authentic O > 0 +``` + +## F7 remains owner of + +```text +O1 commitment admission +``` + +## F8A remains owner of + +```text +O2 authorization +exercise authority +validity / exercisability admission +Hook-owned causal authorization context +``` + +## F8B remains owner of + +```text +protected exact-output PoolManager execution +execution evidence +``` + +## F8C remains owner of + +```text +actual input settlement +authenticated exerciser payment +direct Beneficiary delivery +PoolManager delta closure +``` + +## F8D remains owner of + +```text +actual final backing +exact Remaining reduction +exact-once causal-context consumption +durable fulfillment +``` + +GI verifies their composition. + +Also out of scope: + +```text +F9 canonical acceptance +F10 demo instrumentation +frontend work +public testnet deployment +gas optimization +coverage maximization +unrelated refactoring +new protocol features +``` + +--- + +# 33. GI vs F9 + +Do not implement F9. + +GI asks: + +> **Does adversarial stateful composition preserve frozen safety and derivation properties?** + +F9 asks: + +> **Does a fresh deterministic production deployment reproduce the canonical A1 → A4 acceptance scenario exactly?** + +GI must not substitute a scripted A1→A4 acceptance test for stateful invariant verification. + +Do not begin F9 merely because the GI campaign reaches states similar to the canonical demo path. + +--- + +# 34. GI-Specific Verification Evidence + +Use the repository-standard verification already required by: + +```text +CLAUDE.md +.claude/rules/* +``` + +Do not duplicate or reinterpret those permanent verification requirements here. + +For GI specifically, also execute the stateful invariant campaigns required to establish G-I. + +Report the actual GI campaign configuration used, including as applicable: + +```text +runs +depth / calls +target contracts +target selectors +campaign variants +canonical configuration +generalized configuration +``` + +Report actual campaign results. + +Do not claim G-I evidence solely because the repository-standard suite passes. + +Do not claim G-I evidence from a campaign that failed to exercise meaningful O1/O2/O3 state evolution. + +--- + +# 35. Campaign Quality Check + +Before proposing G-I PASS, inspect the campaign diagnostics. + +Determine whether the runs actually achieved meaningful instances of: + +```text +successful commitment establishment +authentic positive O +successful O2 +failed O2 +partial fulfillment +full fulfillment where reachable +backing-threatening O3 rejection +ordinary protected swap +ordinary opposite-direction swap +liquidity activity +eligibility mutation +time / expiry activity +multiple commitments +reference churn / reuse where reachable +``` + +If important classes remain zero or effectively unreachable: + +1. report that fact; +2. determine whether handler construction or action weighting is the cause; +3. improve state exploration where possible without semantic pre-filtering; +4. identify any remaining reachability limitation. + +A green but semantically empty campaign is not sufficient G-I evidence. + +--- + +# 36. Oracle Independence Check + +Before completion, explicitly inspect the invariant implementation for correlated-oracle risk. + +Verify that expected/reference results for: + +```text +Supporting Capacity +Capacity Obligation +fulfillment conservation +commitment-history integrity +Beneficiary delivery +reference integrity +``` + +are not merely wrappers around the production values being checked. + +Document the independent basis used for each significant oracle. + +If a property cannot be checked independently without duplicating the entire protocol state machine, prefer a narrower independent historical/observable proof rather than creating a second authoritative Standby implementation. + +--- + +# 37. File Boundary + +GI should primarily add test-side files. + +Expected changes are likely to include: + +```text +test/invariant/* +``` + +and narrowly necessary invariant-specific helper files. + +Maintain: + +```text +docs/prompts/session-15-log.md +``` + +Do not update: + +```text +docs/project-status.md +``` + +during GI implementation. + +Do not modify frozen canonical artifacts. + +Production files should remain unchanged unless GI discovers a genuine implementation defect already governed by frozen semantics. + +--- + +# 38. Session Evidence / Post-Project Retrospective + +Maintain: + +```text +docs/prompts/session-15-log.md +``` + +as the Claude implementation-process record for GI. + +Preserve materially relevant: + +```text +invariant architecture +handler design +actor design +ghost/reference-state decisions +oracle-independence decisions +files changed +campaign configuration +action-selection tuning +counterexamples encountered +test failures and corrections +production defects discovered +production changes, if any +verification commands and results +campaign diagnostics +known reachability limitations +advisory G-I assessment +``` + +This log is non-normative. + +Do not update: + +```text +docs/project-status.md +``` + +during GI implementation. + +The status-only update occurs only after independent review and explicit G-I closure. + +A separate retrospective record will later be produced: + +```text +docs/prompts/retrospective/session-15-chatgpt-record.md +``` + +Do not create or modify that file during GI implementation. + +--- + +# 39. Completion Report + +When GI implementation is complete, report: + +1. files inspected; +2. files changed; +3. invariant architecture; +4. production components exercised; +5. handler actions implemented; +6. persistent actor model; +7. ghost/reference state used; +8. independent oracle strategy; +9. invariant functions added; +10. transition-local stateful assertions added; +11. canonical campaign configuration; +12. generalized campaign configuration; +13. campaign diagnostics / action counters; +14. GI-specific campaign commands executed; +15. repository verification results required by the permanent instructions; +16. all material counterexamples encountered during implementation; +17. any production defect discovered; +18. any production code changed; +19. advisory G-I-1 through G-I-23 assessment; +20. known limitations, reachability gaps, deviations, or discrepancies; +21. scope check; +22. recommended next step; +23. prompt audit. + +For every G-I condition, use: + +```text +PASS +FAIL +NOT YET PROVEN +``` + +with concise supporting evidence. + +Do not infer PASS merely because: + +```text +forge test succeeds +``` + +or: + +```text +no invariant failed +``` + +if campaign activity does not actually discharge the condition. + +Do not declare G-I closed. + +--- + +# 40. Counterexample Reporting + +If a stateful invariant or handler assertion fails, preserve the counterexample. + +Report: + +```text +generated action sequence +failing invariant / assertion +relevant authoritative pre-state +relevant authoritative post-state +independent expected result +actual production result +suspected normative owner +``` + +First determine whether the failure is caused by: + +```text +handler defect +oracle defect +fixture defect +invalid test assumption +production implementation defect +frozen-artifact discrepancy +``` + +Do not dismiss a counterexample as a test issue without establishing its cause. + +If unresolved, report G-I as not yet proven. + +--- + +# 41. Accepted GI Semantic Statement + +Before editing, preserve this accepted responsibility: + +> **GI does not introduce new Standby semantics. It subjects the F8D-complete production realization to adversarial multi-operation histories and independently verifies that backing, commitment state, fulfillment attribution, bounded references, causal evidence, authority boundaries, failure atomicity, and custody remain correct throughout the reachable state space required by the frozen verification domain.** + +The intended verification shape is: + +```text +Production Paths + + +Stateful Adversarial Sequences + + +Independent Reference / History Evidence + + +Global Invariant Closure +``` + +Implement that responsibility and nothing broader. + +--- + +# 42. Completion Boundary + +The GI completion boundary is: + +```text +stateful invariant architecture implemented +GI handler implemented +production-path campaigns implemented +independent oracle/history evidence implemented +G-I-1 through G-I-23 evidence collected +canonical campaign executed +generalized campaign executed +GI-specific campaign diagnostics reviewed +repository verification complete +session-15-log.md updated +completion report produced +``` + +Stop at the GI completion boundary. + +Do not begin F9. diff --git a/docs/prompts/session-15-log.md b/docs/prompts/session-15-log.md new file mode 100644 index 0000000..0d85247 --- /dev/null +++ b/docs/prompts/session-15-log.md @@ -0,0 +1,643 @@ +# Standby — Session 15 Log + +Implementation-process record for: + +> **GI — Full Stateful Invariant Verification** + +Initiating prompt: `docs/prompts/session-15-gi-full-stateful-invariant-verification.md`. + +This log is a non-normative audit artifact. It records material follow-up instructions, design decisions, +counterexamples, verification commands, and results. It defines no protocol semantics. + +--- + +## Material Prompts + +### Prompt 1 — Session authorization + +**Instruction:** + +> Read root CLAUDE.md, then execute docs/prompts/session-15-gi-full-stateful-invariant-verification.md as +> the authorized Session 15 task. Stop at the completion boundary defined by that prompt. + +**Consequence:** GI implementation proceeded under the Session 15 prompt scope: a production-only +handler-driven stateful invariant architecture, canonical and generalized campaigns, independent oracles, +the required stateful sequence classes, campaign diagnostics, and an advisory G-I assessment. + +### Prompt 2 — Post-GI coverage refresh + +**Instruction:** + +> Execute `docs/prompts/session-15-post-coverage-report.md`. Stop at the completion boundary defined by that +> prompt. + +That prompt authorizes a **diagnostic-only** post-GI refresh of the repository's established coverage +workflow, now that GI has passed independent review: reconstruct the exact post-F8D methodology from +repository evidence rather than assuming it, preserve it, update `docs/reports/coverage-summary.md` with the +post-F8D baseline, the post-GI result, the delta, newly covered production surfaces attributable to GI, and +the classification of what remains; record the commands, methodology, and result here; add no tests to +improve coverage; and modify no production code, invariant test, frozen artifact, or +`docs/project-status.md` in response to coverage percentages alone. + +**Consequence:** the coverage baseline was refreshed and reported. One test-side compile obstacle had to be +resolved to run the established workflow at all — recorded in full below. No production code, frozen +artifact, or `docs/project-status.md` was touched, and no test was added, removed, weakened, or suppressed. + +### Prompt 3 — Status-only project-status synchronization + +**Instruction:** + +> Update **status only** in `docs/project-status.md` to reflect the independently reviewed GI result: GI — +> Full Stateful Invariant Verification: COMPLETE; G-I: PASS; F9 — Canonical Acceptance: next authorized +> implementation slice / current blocker. Do not add implementation details, invariant architecture, +> campaign results, coverage results, design commentary, test summaries, gate reasoning, retrospective +> observations, or any other new descriptive content. Only make the minimum edits necessary to bring +> existing status fields, roadmap/ladder entries, current-blocker/next-action fields, and any now-stale +> status statements into consistency with that status. Also record this instruction in +> `docs/prompts/session-15-log.md` as the next material follow-up prompt and record the resulting +> status-only action, as audit chronology only. Do not modify any other files. + +**Consequence:** `docs/project-status.md` was synchronized with the externally reviewed and closed G-I, as a +status-only edit. Recorded below. + +**Material prompts recorded: 3.** + +--- + +## Design Record + +### Invariant architecture + +```text +production fixture (BaseStandbyInvariantTest) + ↓ +adversarial handler (StandbyInvariantHandler) + ↓ +production interfaces (StandbyHook / ExerciseRouter / EligibilityRegistry / perimeters / PoolManager) + ↓ +authoritative production state + ↓ +independent reference + remembered-history observations + ↓ +transition-local assertions (handler) + global invariant closure (campaign) +``` + +Files: + +- `test/invariant/StandbyInvariantHandler.sol` — the adversarial transaction generator, the ghost history, + the diagnostic counters, and every transition-local assertion. +- `test/invariant/BaseStandbyInvariantTest.t.sol` — the production-only parameterized environment, the two + independent oracles, and the nine global `invariant_` functions. +- `test/invariant/StandbySequenceEvidence.t.sol` — the required stateful sequence classes and the + deterministic diagnostic campaign, both driven through the same handler. +- `test/invariant/StandbyInvariant.t.sol` — the canonical and generalized campaign configurations. + +### Production-only decision + +No `StandbyHookHarness` and no privileged economic seeding anywhere. The Hook is deployed through the +canonical `DeployStandbyHook` procedure, the service is activated by `configureAndActivate`, the service is +activated with the production `ExerciseRouter` (not the F8A/F8B/F8C stand-ins), and the bootstrap liquidity +is added through the production `beforeAddLiquidity` path by an eligible provider routed through the trusted +liquidity perimeter. + +`DerivationTestCurrency` is imported from `test/shared/BaseDerivationTest.t.sol` for the generalized +campaign's asymmetric-decimal currencies. That file also declares the F5 derivation harness, which is +therefore a compile-time dependency of the generalized campaign — it is never deployed, never configured, +and contributes no GI evidence. + +### `fail_on_revert = true` + +Every production call the handler makes is wrapped, and refusals are recorded and asserted rather than +discarded. That makes an unwrapped revert — including a failed assertion inside a generated action — a +campaign failure rather than a silently dropped sequence. Verified empirically by injecting a deliberately +false conservation assertion into the handler and confirming the campaign failed with that message; the +injection was then reverted. + +### Ghost / reference state + +Remembered history only: admitted commitment identities, the immutable facts each admission recorded, the +last Remaining Entitlement observed, independently tracked successful fulfillment per commitment, protected +output delivered by completed O2 per Beneficiary, protected output donated by unrelated transfers per +Beneficiary (accounted separately), position custody per actor and range, and diagnostic counters. No +parallel validity, exercisability, binding, expiry, obligation, or lifecycle classification is maintained. + +### Oracle independence + +- **Supporting Capacity** — `ReferenceCalculations.referenceSupportingCapacity` over the authoritative + Slot0 square-root price and active liquidity, with its own Q64.96 arithmetic. It calls no `StandbyMath` + and no production derivation. +- **Aggregate Capacity Obligation** — `ReferenceCalculations.referenceCommitmentObligation` summed over the + whole allocated history `[1, nextCommitmentId)` read through the fact-only commitment surface. Production + sums the bounded index instead, so the two constructions differ: an obligation that escaped the index + would be a disagreement rather than a shared blind spot. +- **Fulfillment** — `ghostFulfilled[id]`, increased only after an independently observed successfully + completed O2, compared against `Original - Remaining`. +- **Beneficiary delivery** — Beneficiaries are funded with nothing and never trade, provide liquidity, or + exercise, so their protected-output balance is a complete independent history: it must equal + `ghostDelivered + ghostDonated` at all times. +- **Commitment history** — immutable facts snapshotted at admission and re-compared after every action, + which is what makes survival across bounded-reference reclamation and slot reuse checkable. + +### Action-selection tuning + +Three generation adjustments were made after observing that the first campaigns reached very little +completed fulfillment. None of them is a safety pre-filter; each shapes the magnitude or target of a +generated request, and production alone decides admissibility: + +1. generated amounts are drawn against the independently derived present backing headroom plus a margin, + rather than against twice the starting capacity, so both admissible and inadmissible proposals are + ordinary outcomes; +2. eligibility mutations grant three times as often as they revoke, because a history whose eligible + identities spent half their life ineligible refused almost everything; +3. generated exercises prefer recent commitments, with every identity still reachable. + +Time advancement was also softened from a 20% chance of a 31-day jump to 12.5%, so that expiry stays +reachable without ending every commitment's validity before it can be exercised. + +### Counterexamples encountered + +No production counterexample was found. The only failures encountered during implementation were the +campaign-quality floors of the deterministic diagnostic campaign (`full fulfillment` and then +`partial fulfillment` reaching zero), which were generator-shaping problems and were resolved by the tuning +above. No production code was changed. + +### Campaign configuration + +| Campaign | runs | depth | fail_on_revert | target | +| ----------------------------------- | ---- | ----- | -------------- | -------------------------- | +| default profile, both configurations | 256 | 96 | true | 12 handler action selectors | +| ci profile, both configurations | 512 | 192 | true | 12 handler action selectors | + +Set as inline `forge-config` on the campaign contracts rather than by changing `foundry.toml`, because each +invariant function re-runs the whole campaign and the repository-wide `ci` invariant configuration +(runs 1000 / depth 500) would make the GI suites the dominant cost of every CI run. + +### Verification results + +Recorded in the completion report below. + +--- + +## Required Task Completion Report + +### 1. Files Inspected + +Repository: + +- `CLAUDE.md`, `.claude/rules/solidity-style.md`, `.claude/rules/testing.md`; +- `docs/project-status.md`; `docs/implementation-plan.md` §18 (GI) and §19 (F9 boundary); +- `docs/invariants.md` and `docs/testing-strategy.md` structure; +- `src/StandbyHook.sol` (complete), `src/ExerciseRouter.sol`, `src/EligibilityRegistry.sol`, + `src/demo/ActorAwareTestRouter.sol`, `src/libraries/StandbyMath.sol`, `src/libraries/CommitmentRefs.sol`, + `src/mocks/MockFixtureCurrency.sol`, `src/mocks/MockUSTB.sol`; +- `script/DeployStandbyHook.s.sol`, `script/helpers/StandbyFixtureConfig.sol`, + `script/helpers/DeterministicFixtureDeployer.sol`; +- `test/shared/BaseStandbyServiceTest.t.sol`, `test/shared/BaseActorAwareStandbyTest.t.sol`, + `test/shared/BaseCommitmentAdmissionTest.t.sol`, `test/shared/BaseAuthenticBackingTest.t.sol`, + `test/shared/BaseExerciseAuthorizationTest.t.sol`, `test/shared/BaseExerciseSettlementTest.t.sol`, + `test/shared/BaseExerciseFinalizationTest.t.sol`, `test/shared/BaseDerivationTest.t.sol`, + `test/shared/ReferenceCalculations.sol`, `test/shared/BaseV4Test.t.sol`, + `test/integration/DerivationGeneralization.t.sol`; +- `foundry.toml`, `remappings.txt`. + +### 2. Files Changed + +Created: + +| File | Why | +| --- | --- | +| `test/invariant/StandbyInvariantHandler.sol` | The adversarial stateful transaction generator, the ghost history, the diagnostic counters, and every transition-local assertion. | +| `test/invariant/BaseStandbyInvariantTest.t.sol` | The production-only parameterized campaign environment, the two independent oracles, and the nine global `invariant_` functions. | +| `test/invariant/StandbySequenceEvidence.t.sol` | The required stateful sequence classes and the deterministic diagnostic campaign, driven through the same handler. | +| `test/invariant/StandbyInvariant.t.sol` | The canonical and generalized campaign configurations, with their inline campaign configuration. | +| `docs/prompts/session-15-log.md` | The Session 15 implementation-process record. | + +No production source, script, frozen document, existing test, or `docs/project-status.md` was modified. + +### 3. Invariant Architecture + +```text +production fixture (BaseStandbyInvariantTest) + ↓ +adversarial handler (StandbyInvariantHandler) + ↓ +production interfaces (StandbyHook / ExerciseRouter / EligibilityRegistry / perimeters / PoolManager) + ↓ +authoritative production state + ↓ +independent reference + remembered-history observations + ↓ +transition-local assertions (handler) + global invariant closure (campaign) +``` + +Campaigns run with `fail_on_revert = true`. The handler wraps every production call and records refusals +itself, so an unwrapped revert — including a failed assertion inside a generated action — fails the +campaign instead of being discarded as an uninteresting sequence. This was verified empirically by +injecting a deliberately false conservation assertion into the handler and confirming the campaign failed +with that message; the injection was then reverted. + +### 4. Production Components Exercised + +Real pinned `PoolManager`; production `StandbyHook` deployed through the canonical `DeployStandbyHook` +mining and deployment procedure; production `configureAndActivate`; production `establishCommitment`; +production `ExerciseRouter` (the complete one, not the F8A/F8B/F8C stand-ins) driving +`authorizeExercise` → protected PoolManager execution → settlement and direct Beneficiary delivery → +`finalizeExercise`; production `beforeSwap` / `afterSwap` / `beforeAddLiquidity` / `beforeRemoveLiquidity` +enforcement; real `EligibilityRegistry` under its own administrator; two separately deployed +`ActorAwareTestRouter` perimeters holding distinct trust roles; canonical `MockUSTB` / `MockUSDC` deployed +through `DeterministicFixtureDeployer`. + +No `StandbyHookHarness`, no privileged economic seeding, and no direct write of Remaining Entitlement, +admitted extent, bounded reference, capacity, obligation, validity, exercisability, fulfillment, or causal +context anywhere. + +### 5. Handler Actions Implemented + +Twelve generated actions, all of which can succeed and all of which can be refused: + +`establishCommitment`, `exercise`, `ordinaryProtectedSwap`, `ordinaryOppositeSwap`, `addLiquidity`, +`removeLiquidity`, `advanceTime`, `setBeneficiaryEligibility`, `setTraderEligibility`, +`setLiquidityEligibility`, `directTransferProtectedTokenToBeneficiary`, `attemptOrphanExerciseEvidence`. + +The twelfth is the traceable addition beyond the prompt's minimum set: it probes GI-D / G-I-21 behaviorally +by attempting `authorizeExercise` outside the configured ExerciseRouter and `finalizeExercise` with no +causally proven exercise behind it, including immediately after successful and failed exercises. + +Adversarial shaping inside the existing actions rather than as new actions: routing swaps through the +liquidity perimeter and liquidity actions through the swap perimeter; price limits beyond the service +domain; liquidity ranges with endpoints strictly inside the domain; removal sizes beyond the actor's own +position; `q = 0`, `q = Remaining`, and `q > Remaining`; cost bounds no real debt can satisfy; unauthorized +callers; a permanently ineligible Beneficiary; already-ended and impossible commitment windows. + +### 6. Persistent Actor Model + +Thirteen persistent identities, one role each: `registryAdmin`, `establishmentAuthority`, `beneficiaryA`, +`beneficiaryB`, `ineligibleBeneficiary`, `authorizedExerciser`, `unauthorizedExerciser`, `eligibleTrader`, +`ineligibleTrader`, `eligibleProvider`, `ineligibleProvider`, `donor`, `outsider` (plus the separate +`configurationAuthority`). Callers are never fuzzed addresses, so authority relationships stay stable +across a whole history. + +Funding is asymmetric on purpose: Beneficiaries are funded with nothing, exercisers hold input currency +only, the donor holds protected output and no Standby role. The three permanently ineligible identities are +never granted eligibility by any action. + +### 7. Ghost / Reference State Used + +Admitted commitment identities; the immutable facts each admission recorded; the last Remaining Entitlement +observed; independently tracked successful fulfillment per commitment; protected output delivered by +completed O2 per Beneficiary; protected output donated by unrelated transfers per Beneficiary, accounted +separately; position custody per actor and range; diagnostic counters. + +No parallel validity, exercisability, binding, expiry, obligation, or lifecycle classification is +maintained anywhere. + +### 8. Independent Oracle Strategy + +| Quantity | Independent basis | +| --- | --- | +| Supporting Capacity | `ReferenceCalculations` Q64.96 arithmetic over the authoritative Slot0 square-root price and active liquidity. Calls no `StandbyMath` and no production derivation. | +| Aggregate Capacity Obligation | `ReferenceCalculations.referenceCommitmentObligation` summed over the **whole allocated history** `[1, nextCommitmentId)` read through the fact-only commitment surface — production sums the bounded index instead, so the two constructions differ and an obligation that escaped the index shows up as disagreement. | +| Fulfillment | `ghostFulfilled[id]`, increased only after an independently observed completed O2, compared against `Original − Remaining`. | +| Beneficiary delivery | Beneficiary balances, which are a complete independent history because Beneficiaries start with nothing and never trade, provide liquidity, or exercise: balance must equal `delivered + donated`. | +| Commitment history | Immutable facts snapshotted at admission, re-compared after every action, including after reference reclamation and slot reuse. | +| Reference integrity | Structural properties of the index checked directly, plus the contrapositive of reclamation: a commitment still carrying obligation must still be referenced. | + +### 9. Invariant Functions Added (per configuration) + +`invariant_supportingCapacityEqualsIndependentReference`, +`invariant_capacityObligationEqualsIndependentReference`, +`invariant_supportingCapacityCoversCapacityObligation`, +`invariant_commitmentConservation`, +`invariant_beneficiaryHoldingsMatchIndependentDeliveryHistory`, +`invariant_boundedReferenceIntegrity`, +`invariant_bindingCommitmentsRetainALiveReference`, +`invariant_protocolHoldsNoCurrencyCustody`, +`invariant_noReusableCausalEvidenceSurvives`. + +### 10. Transition-Local Stateful Assertions Added + +Around every generated or scripted action: admitted facts unchanged for every historical commitment; +`Remaining ≤ Original`; Remaining never increases; `Original − Remaining == ghostFulfilled`; Beneficiary +holdings equal delivery plus donation; zero Hook and Router custody in both currencies; empty O2 causal +context. + +Around a successful O2 additionally: exactly one commitment reduced, by exactly `q`, every other commitment +untouched, and exactly `q` protected output delivered to the authoritative Beneficiary. + +Around a refused O2: no Remaining moved anywhere, nothing delivered, no obligation released, and the +authoritative pool state unchanged. + +Around a refused O1: no commitment identity consumed and the bounded reference index untouched, slot for +slot. + +Around every eligibility mutation: the Aggregate Capacity Obligation is unchanged. + +### 11. Canonical Campaign Configuration + +`MockUSTB` = currency0, `MockUSDC` = currency1, both six-decimal, deployed through the deterministic +ordered deployment path; protected direction `zeroForOne`; `tickQ = −240`, `tickO = +240`; LP range +`[−300, +300]`; tick spacing 10; fee 500; canonical liquidity 6,707,079,990,254; initial Supporting +Capacity 80,000.000000 MockUSDC. + +### 12. Generalized Campaign Configuration + +Protected direction `oneForZero`, so the protected output is currency0; eighteen- and eight-decimal +currencies, so neither `1e6` nor equal precision is a usable universal scale; `tickQ = +1200`, +`tickO = −600`; LP range `[−1200, +1800]`; tick spacing 60; fee 3000; liquidity 1e15. Supporting Capacity +and Capacity Obligation remain raw amounts of the protected output currency and the identical invariant +closure is asserted. + +### 13. Campaign Diagnostics + +Deterministic diagnostic campaign, 600 generated actions per configuration, fixed seed: + +| Diagnostic | Canonical | Generalized | +| --- | --- | --- | +| O1 admitted / refused | 18 / 26 | 16 / 28 | +| O2 completed / refused | 15 / 36 | 15 / 36 | +| O2 partial / full | 6 / 9 | 7 / 8 | +| protected swaps attempted / executed | 46 / 16 | 46 / 15 | +| opposite swaps attempted / executed | 60 / 40 | 60 / 35 | +| backing-refused swaps / liquidity actions | 1 / 6 | 5 / 4 | +| liquidity added / removed | 39 / 9 | 39 / 11 | +| eligibility mutations B / T / L | 49 / 25 / 52 | 49 / 25 / 52 | +| eligibility mutations refused | 18 | 18 | +| time advances / expiry events | 59 / 2 | 59 / 1 | +| direct Beneficiary transfers / orphan-evidence probes | 40 / 49 | 40 / 49 | +| reference reuse events | 2 | 0 | +| max simultaneous live references | 16 | 16 | +| max observed Aggregate Capacity Obligation | 606,322,699,893 | 652,582,229,995,934 | + +The generated Foundry campaigns additionally reported per-selector call metrics: all twelve action +selectors were exercised roughly uniformly (≈650–735 calls each per invariant at the default profile), with +0 reverts and 0 discards. + +### 14. GI-Specific Campaign Commands Executed + +```bash +forge test --match-contract StandbyCanonicalInvariantTest --match-test "invariant_" +forge test --match-contract StandbyGeneralizedInvariantTest --match-test "invariant_" +forge test --match-path test/invariant/StandbyInvariant.t.sol -vv +FOUNDRY_PROFILE=ci forge test --match-contract StandbyCanonicalInvariantTest --match-test "invariant_supportingCapacityEqualsIndependentReference" +``` + +Campaign configuration, set as inline `forge-config` on both campaign contracts: + +| Profile | runs | depth | calls per invariant | fail_on_revert | target | +| --- | --- | --- | --- | --- | --- | +| default | 256 | 96 | 24,576 | true | 12 handler selectors on the handler contract | +| ci | 512 | 192 | 98,304 | true | 12 handler selectors on the handler contract | + +`foundry.toml` was deliberately not changed: each invariant function re-runs the whole campaign, so the +repository-wide `ci` invariant setting (runs 1000 / depth 500) would have made the two GI suites the +dominant cost of every CI run. + +### 15. Repository Verification Results + +```bash +forge fmt --check # clean +forge build --sizes # successful +forge test # 579 passed, 0 failed, 0 skipped (60 suites, 43.8s) +FOUNDRY_PROFILE=ci forge test # 579 passed, 0 failed, 0 skipped (60 suites, 175.8s) +``` + +Canonical campaign: 9 invariants × 24,576 calls, 0 reverts, all passing. Generalized campaign: identical +configuration, all passing. All 20 scripted stateful sequence tests (10 per configuration) pass. + +### 16. Material Counterexamples Encountered + +None against production. The only failures encountered were campaign-quality floors in the deterministic +diagnostic campaign — first `full fulfillment` and then `partial fulfillment` reaching zero — which were +generator-shaping problems, not protocol behavior. They were resolved by drawing generated amounts against +the independently derived present backing headroom, biasing eligibility mutations toward granting, biasing +generated exercises toward recent commitments, and softening the frequency of the 31-day time jump. None of +these is a safety pre-filter: production alone decides whether any generated request is admissible, and +refusal rates remain high (26–28 refused O1 and 36 refused O2 per 600 actions). + +### 17. Production Defects Discovered + +None. + +### 18. Production Code Changed + +None. GI was verification-only, as presumed by the session prompt. + +### 19. Advisory G-I Assessment + +| Condition | Assessment | Evidence | +| --- | --- | --- | +| G-I-1 Supporting Capacity equivalence | **PASS** | `invariant_supportingCapacityEqualsIndependentReference` over 24,576 generated calls per configuration plus every scripted sequence's closure; oracle is independent Q64.96 arithmetic over authoritative pool state. | +| G-I-2 Capacity Obligation equivalence | **PASS** | `invariant_capacityObligationEqualsIndependentReference`; the oracle sums the whole allocated commitment history rather than the bounded index production scans. | +| G-I-3 Backing sufficiency | **PASS** | `invariant_supportingCapacityCoversCapacityObligation` over reference values, with authentic positive obligation reached throughout (max 6.06e11 canonical / 6.53e14 generalized). | +| G-I-4 Remaining bound | **PASS** | Global invariant and per-action observation over every historical commitment. | +| G-I-5 Immutable commitment facts | **PASS** | All six admitted facts re-compared against the admission snapshot after every action, including after slot reclamation. | +| G-I-6 Remaining monotonicity | **PASS** | Per-action comparison against the last observed remainder, then updated. | +| G-I-7 Fulfillment conservation | **PASS** | `Original − Remaining == ghostFulfilled` after every action, with 15 completed exercises per diagnostic campaign and many more in the generated campaigns. | +| G-I-8 Expiry is not fulfillment | **PASS** | Scripted expiry sequence: obligation falls to zero while Remaining stays at the admitted extent and tracked fulfillment stays zero; generated campaigns reach expiry too. | +| G-I-9 Eligibility mutation integrity | **PASS** | Every eligibility mutation asserts unchanged obligation and unchanged remainders; scripted churn sequence shows an ineligible Beneficiary's commitment still refusing a destructive O3 and still unexercisable, then exercisable again once restored. | +| G-I-10 Ordinary swap non-fulfillment | **PASS** | No-fulfillment assertion around every swap, successful or refused, in both directions. | +| G-I-11 Liquidity non-fulfillment | **PASS** | Same assertion around every liquidity addition and removal. | +| G-I-12 Direct transfer non-fulfillment | **PASS** | Same assertion around every direct transfer, plus the global delivery-accounting invariant that separates donation from delivery. | +| G-I-13 Exact O2 attribution | **PASS** | Every successful exercise asserts exactly one commitment reduced by exactly `q` with every other commitment untouched. | +| G-I-14 Exact Beneficiary delivery | **PASS** | Per-exercise delivery equality plus the global `balance == delivered + donated` invariant. | +| G-I-15 Failed O2 integrity | **PASS** | Refused exercises assert zero fulfillment, zero Remaining movement, zero delivery, no obligation release, unchanged pool state, zero protocol custody, and an empty causal context. | +| G-I-16 Protocol custody integrity | **PASS** | Both currencies, Hook and Router, after every action and as a global invariant. No campaign action donates to a protocol address, so any balance would be protocol-created. | +| G-I-17 Reference bound | **PASS** | Live reference count checked; the bound of 16 is reached in both diagnostic campaigns. | +| G-I-18 Reference validity | **PASS** | Every nonzero reference unique and resolving to an allocated identity. | +| G-I-19 History across reuse | **PASS** | Scripted sequence exhausts the index, expires it, reuses a slot, and proves the displaced commitment's facts and remainder intact and its identity unrecycled; the canonical generated campaign also reached reuse. | +| G-I-20 Reclamation cause integrity | **PASS** | `invariant_bindingCommitmentsRetainALiveReference` — every commitment still carrying obligation still occupies a reference, so eligibility loss, backing pressure, swaps, liquidity transitions, direct transfers, and failed exercises cannot reclaim one. | +| G-I-21 O2 context isolation | **PASS** | All seven causal-context fields asserted empty after every completed action; orphan authorization and orphan finalization probes refused; scripted contamination sequence covering failed→valid, valid→valid, and post-success attempts. | +| G-I-22 Generalization | **PASS** | Identical closure passes under the canonical `zeroForOne` six-decimal service and a generalized `oneForZero` service with 18/8-decimal currencies, different domain, spacing, fee, position, and liquidity. | +| G-I-23 Campaign quality | **PASS** | Diagnostics in §13: admitted and refused O1, completed and refused O2, partial and full fulfillment, protected and opposite swaps, backing refusals against authentic positive obligation, liquidity activity, all three eligibility domains, time advance and expiry, direct transfers, orphan probes, 16 simultaneous live references, and reference reuse. | + +This is an advisory assessment only. Claude does not close G-I. + +### 20. Known Limitations / Reachability Gaps + +- The generated generalized campaign did not reach bounded-reference slot reuse within 600 actions + (canonical reached it twice); both configurations reach it deterministically through the scripted + expiry/reuse sequence. +- Exact `S == O` boundary acceptance is reached by the scripted backing-boundary sequence rather than by + chance in the generated campaigns; the counter for spontaneous boundary states is zero. +- Nested O2 is not generated: the handler acts at top level, and production forbids nesting in both the + router's own attribution context and the Hook's authorization guard. GI probes the reachable shape of the + same property instead — orphan authorization and orphan finalization, after successful and after failed + exercises. +- Per §28 of the session prompt, causal-position read-surface refusal and extreme tick-bound clamping were + not given separate GI obligations; no compositional counterexample touching either was found. +- The generalized campaign's currencies reuse `DerivationTestCurrency` from `test/shared/BaseDerivationTest.t.sol`, + which also declares the F5 derivation harness. That harness is a compile-time dependency only: it is never + deployed, never configured, and contributes no GI evidence. + +### 21. Scope Check + +Work remained inside GI. No production semantics were changed. No frozen document was modified. +`docs/project-status.md` was not touched. F9 was not started, no acceptance test was written, and no +frontend or deployment work was performed. The only files added are test-side plus the Session 15 log. + +### 22. Recommended Next Step + +Independent review of this GI evidence and an explicit G-I closure decision. If G-I closes, the next +authorized responsibility would be F9 — Canonical Acceptance, which is neither started nor authorized. + +### 23. Prompt Audit + +All material follow-up instructions were captured in `docs/prompts/session-15-log.md`. +**1 material prompt recorded at the GI completion boundary** (the session authorization itself); no further +material follow-up instruction had been received at that point. Two further material prompts — the post-GI +coverage refresh and the status-only project-status synchronization — were received afterwards and are +recorded above; the session total is now **3**. + +--- + +## Post-GI Diagnostic Follow-Up — Coverage Refresh + +Captured under Prompt 2, after GI passed independent review. **Non-normative engineering evidence:** it +defines no protocol semantics and neither establishes, closes, nor reopens G-I. + +The detailed evidence lives in the report and is deliberately not duplicated here: + +```text +docs/reports/coverage-summary.md +``` + +### Methodology reconstructed from repository evidence + +Sources consulted before running anything: the previous revision of `docs/reports/coverage-summary.md` +(its "Command and Result" section, its limitation notes, and its computed-aggregate convention), +`docs/prompts/session-14-post-f8d-engineering-baseline.md` §5, and the coverage section of +`docs/prompts/session-14-log.md`. + +The reconstructed methodology is unambiguous: + +1. `forge coverage` — default profile, default summary report, no filtering, exclusion, `--match`, or + `--ir-minimum`, and no change to `foundry.toml`; +2. `forge coverage --report debug` — read-only, used only to locate individual uncovered items, producing no + repository artifact; +3. production aggregates computed by summing the per-file rows, because Foundry's `Total` row aggregates + `src/`, `script/` and `test/` together; +4. two computed aggregates reported: the Standby protocol core (Hook, ExerciseRouter, EligibilityRegistry, + and the three libraries) and all of `src/`; +5. the four coverage dimensions reported separately and never collapsed into one figure. + +That methodology was preserved exactly. + +### Measured state + +Branch `feat/gi-stateful-invariant-verification`, `HEAD` = `e698c22fb6396585cd7bd57cbe120be53b7724cc`, +Foundry `1.3.5-stable`, `default` profile. **The Session 15 GI work was staged but uncommitted when the +measurement was taken**, so the report does not describe commit `e698c22`; it enumerates the four +`test/invariant/` files and two `docs/prompts/` files it actually measured on top of it. No production +source, script, harness, existing test, frozen artifact, or configuration file differs from that commit. + +### Commands + +```bash +forge coverage +forge coverage --report debug +``` + +Both completed successfully — 60 suites, 579 tests passed, 0 failed, under coverage instrumentation +(110.85 s for the summary run). The debug invocation produced no repository artifact. + +### Compile obstacle and the one test-side change it required + +The first `forge coverage` invocation failed to compile with `Stack too deep` at +`test/invariant/StandbyInvariantHandler.sol:941`, inside the generated ordinary-swap action. `forge coverage` +disables the optimizer, and that frame held enough locals to exceed the unoptimized stack limit; the +optimized build the gates were verified against compiles it without difficulty, so the problem was visible +only under coverage instrumentation. + +Two resolutions existed. `--ir-minimum` would have changed the reconstructed procedure this refresh is +required to preserve. Splitting the generator's amount and price-limit selection into +`_generatedSwapAmount` and `_generatedSwapLimitTick` changes no behavior and restores the established +procedure, so that was done. It is a compile-time frame-size change, not a response to a coverage +percentage, and it changes nothing about what the campaigns generate, bound, or assert. + +Verified behavior-preserving before the measurement was taken: + +| Check | Result | +| --- | --- | +| GI deterministic campaign counters, both configurations | byte-for-byte identical to the pre-change run | +| `forge fmt --check` | clean | +| `forge build --sizes` | successful | +| `forge test` | 579 passed, 0 failed | +| `FOUNDRY_PROFILE=ci forge test` | 579 passed, 0 failed | + +### Result + +Standby protocol core, post-F8D baseline → post-GI: + +```text +Lines 99.42% -> 99.42% (514/517, unchanged) +Statements 98.33% -> 98.52% (531/540 -> 532/540, +1 statement) +Branches 91.35% -> 92.31% (95/104 -> 96/104, +1 branch) +Functions 100% -> 100% (107/107, unchanged) +``` + +Exactly one production surface moved from uncovered to covered: `src/StandbyHook.sol` L1668, the +`beforeRemoveLiquidity` refusal of a liquidity removal proposed through an untrusted perimeter — which was +**potential GI input #1** in the post-F8D report. Every other production file is identical to the baseline. + +Of the other four post-F8D potential GI inputs: nested exercise attribution was considered and is not +reachable by a top-level generator (recorded as a known GI reachability gap); the causal-position read-surface +refusal and the tick-bound clamps were deliberately excluded by §28 of the GI session prompt and no +compositional counterexample touching them appeared; the unresolved-delta guard remains structurally +unreachable on the production path. + +No coverage observation exposed a previously unrecognized frozen verification obligation. + +### Scope confirmation + +No production code, script, harness, fixture, frozen artifact, compiler, optimizer, EVM, or dependency +configuration was changed. `foundry.toml` was not changed. `docs/project-status.md` was not modified. No +test was added, removed, weakened, or suppressed to affect coverage, and no production code was excluded +from measurement. The single test-side change was a compile-time frame-size split required to run the +established coverage workflow at all, and is disclosed in both this log and the coverage report. F9 and F10 +were not started. + +--- + +## Post-GI Status Synchronization + +Recorded under Prompt 3, after G-I was independently reviewed and closed. **Audit chronology only.** This +entry records that a status-only synchronization occurred; it adds no evidence, no assessment, and no +normative content, and it does not itself close a gate or authorize any implementation slice. + +### Authorization + +External review closed G-I as PASS. Under the Project Status Synchronization rule in `CLAUDE.md`, that +closure is what permits `docs/project-status.md` to be brought into consistency with it. + +### File changed + +```text +docs/project-status.md +``` + +No other file was modified. + +### Status-only edits made + +| Field | Before | After | +| --- | --- | --- | +| Current Implementation Slice | GI (NEXT AUTHORIZED / NOT STARTED) | F9 — Canonical Acceptance (NEXT AUTHORIZED / NOT STARTED) | +| Last Closed Gate | G8D | G-I — Full Stateful Invariant Gate (CLOSED / PASS) | +| Status line | … F8D COMPLETE — GI NOT STARTED | … F8D COMPLETE — GI COMPLETE — F9 NOT STARTED | +| §2 next authorized slice / last closed gate | GI / G8D | F9 / G-I | +| §2 gate-closed list and review sentence | ends at F8D; GI not started | includes GI; GI reviewed and G-I closed, F9 next | +| §3 ladder — GI row | **NEXT / NOT STARTED** | **COMPLETE — G-I CLOSED** | +| §3 ladder — F9 row | NOT STARTED | **NEXT / NOT STARTED** | +| §10 Current Blocker | GI unstarted; F9 not authorized | F9 unstarted; F10 not authorized | +| §18 Next Action | GI | F9 | +| §19 Handoff — Validated State | ends at F8D / G8D | adds GI complete / G-I closed | +| §19 Handoff — Current Gate | G8D CLOSED / PASS | G-I CLOSED / PASS | +| §19 Handoff — Next Blocker / Next Step | GI not started / begin GI | F9 not started / begin F9 | + +### Scope confirmation + +No implementation detail, invariant architecture, campaign result, coverage result, design commentary, test +summary, gate reasoning, or retrospective observation was added to `docs/project-status.md`. No production +code, test, script, frozen artifact, or configuration was changed. The normative content, implementation +report, GI evidence, and post-GI coverage evidence already recorded in this log are unchanged. F9 was not +started. diff --git a/docs/prompts/session-15-post-coverage-report.md b/docs/prompts/session-15-post-coverage-report.md new file mode 100644 index 0000000..6786762 --- /dev/null +++ b/docs/prompts/session-15-post-coverage-report.md @@ -0,0 +1,68 @@ +Re-run the repository's established coverage workflow now that GI — Full Stateful Invariant Verification has passed independent review. + +This is a **diagnostic-only post-GI refresh**. + +Do not modify production code, invariant tests, frozen artifacts, or `docs/project-status.md` in response to coverage percentages alone. + +Before running coverage, inspect: + +```text +docs/reports/coverage-summary.md +docs/prompts/session-15-log.md +``` + +and the relevant prior session log, repository configuration, scripts, or commands referenced by the existing coverage report as necessary to reconstruct the exact coverage workflow that produced the current post-F8D baseline. + +Do not assume knowledge from a previous Claude session. + +Use the existing repository evidence to determine: + +- the coverage command(s); +- profile/configuration used; +- source/test inclusion or exclusion rules; +- any report-generation or parsing procedure; +- the existing `docs/reports/coverage-summary.md` structure and reporting conventions. + +Preserve that methodology for the post-GI run rather than introducing a new coverage procedure. + +If the exact prior methodology cannot be reconstructed from repository artifacts, stop and report the ambiguity rather than silently choosing a different methodology. + +Update: + +```text +docs/reports/coverage-summary.md +``` + +to reflect the post-GI repository state. + +Preserve comparison against the existing post-F8D baseline: + +```text +Lines 99.42% +Statements 98.33% +Branches 91.35% +Functions 100% +``` + +The report should distinguish: + +- post-F8D baseline; +- post-GI coverage result; +- delta; +- any newly covered production surfaces attributable to the GI stateful invariant suite; +- any remaining uncovered or partially covered production surfaces that appear semantically relevant; +- any remaining gaps that are merely diagnostic or structurally unreachable through the supported production domain. + +Do not treat coverage as proof of semantic correctness, invariant preservation, or G-I closure. + +Do not introduce new tests solely to improve coverage during this follow-up unless a coverage observation exposes an actual previously unrecognized frozen verification obligation. If such an issue appears, report it rather than expanding scope automatically. + +Also record the coverage command(s), methodology reconstructed from repository evidence, and result in: + +```text +docs/prompts/session-15-log.md +``` + +as a post-GI diagnostic follow-up. + +Stop after refreshing the coverage report and Session 15 log. diff --git a/docs/reports/coverage-summary.md b/docs/reports/coverage-summary.md index 4f09657..a23eb25 100644 --- a/docs/reports/coverage-summary.md +++ b/docs/reports/coverage-summary.md @@ -5,17 +5,20 @@ > **Status: Non-normative engineering evidence. This report does not define protocol semantics or independently establish a verification gate.** Coverage is a measure of what the test suite executed. It is not a measure of semantic correctness, and it -is not invariant proof. An uncovered line is not, on its own, a protocol defect. +is not invariant proof. An uncovered line is not, on its own, a protocol defect. Nothing in this report +establishes, closes, or reopens G-I. --- ## Checkpoint ```text -Post-F8D / Pre-GI +Post-GI ``` -The F0–F8D production path is complete and G8D is PASS / CLOSED. GI has not been started. +The F0–F8D production path is complete, G8D is PASS / CLOSED, and GI — Full Stateful Invariant Verification +has passed independent review. This is a diagnostic refresh of the post-F8D baseline recorded in the +previous revision of this report; that baseline is preserved below for comparison. --- @@ -24,8 +27,8 @@ The F0–F8D production path is complete and G8D is PASS / CLOSED. GI has not be | Item | Value | | ---------------------- | ----------------------------------------------------------------- | | Measurement date | 2026-09-08 | -| Git branch | `feat/f8d-o2-causal-finalization` | -| Git commit (`HEAD`) | `8938a85bb8036424c02c7cae57fc994371573933` | +| Git branch | `feat/gi-stateful-invariant-verification` | +| Git commit (`HEAD`) | `e698c22fb6396585cd7bd57cbe120be53b7724cc` | | Working tree | **Not clean — the measured state is uncommitted.** See below. | | Foundry | `1.3.5-stable`, commit `9979a41b5daa5da1572d973d7ac5a3dd2afc0221` | | Solidity / EVM | `0.8.26` / `cancun` | @@ -35,47 +38,39 @@ The F0–F8D production path is complete and G8D is PASS / CLOSED. GI has not be ### Working-tree state -`HEAD` is the F8C merge commit. **The Session 14 F8D work was uncommitted when this measurement was taken, -so this report does not describe the state of commit `8938a85`.** It describes that commit plus the -following working-tree changes: - -Modified: - -```text -foundry.toml -docs/setup.md -src/ExerciseRouter.sol -src/StandbyHook.sol -test/harness/UnfinalizedExerciseRouter.sol -test/integration/ExerciseSettlement.t.sol -``` - -Added: +`HEAD` is the F8D merge commit. **The Session 15 GI work was uncommitted when this measurement was taken, +so this report does not describe the state of commit `e698c22`.** It describes that commit plus the +following working-tree additions, all of which were staged at measurement time: ```text -docs/prompts/session-14-f8d-02-causal-finalization.md -docs/prompts/session-14-log.md -test/harness/MisdirectedFinalizationRouter.sol -test/harness/NonFinalizingExerciseRouter.sol -test/shared/BaseExerciseFinalizationTest.t.sol -test/unit/ExerciseFinalization.t.sol -test/integration/ExerciseFinalization.t.sol -test/fuzz/ExerciseFinalizationFuzz.t.sol +test/invariant/StandbyInvariantHandler.sol +test/invariant/BaseStandbyInvariantTest.t.sol +test/invariant/StandbySequenceEvidence.t.sol +test/invariant/StandbyInvariant.t.sol +docs/prompts/session-15-gi-full-stateful-invariant-verification.md +docs/prompts/session-15-log.md ``` -When the Session 14 work is committed, this baseline should be understood as belonging to that commit. +No production source, script, harness, existing test, frozen artifact, or configuration file differs from +`e698c22`. When the Session 15 work is committed, this measurement should be understood as belonging to that +commit. --- ## Command and Result +The post-F8D methodology was reconstructed from `docs/prompts/session-14-post-f8d-engineering-baseline.md` +§5, `docs/prompts/session-14-log.md`, and the previous revision of this report, and was preserved exactly: + ```bash forge coverage ``` -Completed successfully (exit 0): 58 suites, **539 tests passed, 0 failed, 0 skipped**, under coverage -instrumentation. The default summary report was used; no filtering, exclusion, or `--match` option was -applied. +Default profile, default summary report. No filtering, no exclusion, no `--match` option, no +`--ir-minimum`, and no change to `foundry.toml`. + +Completed successfully (exit 0): 60 suites, **579 tests passed, 0 failed, 0 skipped**, under coverage +instrumentation, in 110.85 s. A second, read-only invocation was used to locate the individual uncovered items reported below: @@ -85,6 +80,42 @@ forge coverage --report debug It produced no repository artifact. +### Compilation obstacle encountered, and what was done about it + +The first `forge coverage` invocation **failed to compile**: + +```text +Error: Compiler error (…/LValue.cpp:55): Stack too deep … + --> test/invariant/StandbyInvariantHandler.sol:941:82 +``` + +`forge coverage` disables the optimizer, and the GI handler's ordinary-swap generator held enough locals in +one frame to exceed the unoptimized stack limit. The optimized build the gates were verified against +compiles that frame without difficulty, so the failure was visible only under coverage instrumentation. + +Two resolutions were possible, and the methodology decided between them. Adding `--ir-minimum` would have +changed the reconstructed coverage procedure, which this refresh is required to preserve. Splitting the +generator's amount and price-limit selection into two helper functions changes no behavior and restores the +established procedure, so that was done: + +```text +test/invariant/StandbyInvariantHandler.sol — _ordinarySwap split into + _ordinarySwap / _generatedSwapAmount / _generatedSwapLimitTick +``` + +This is a compile-time frame-size change, not a response to a coverage percentage and not a change to what +the campaigns generate or assert. It was verified as behavior-preserving before this measurement was taken: +the deterministic diagnostic campaigns reproduce **identical counters** in both configurations, and both +profiles still pass in full. + +| Check after the change | Result | +| ---------------------- | ------ | +| `forge fmt --check` | clean | +| `forge build --sizes` | successful | +| `forge test` | 579 passed, 0 failed | +| `FOUNDRY_PROFILE=ci forge test` | 579 passed, 0 failed | +| GI diagnostic campaign counters | byte-for-byte identical to the pre-change run, both configurations | + ### Material limitations affecting interpretation 1. **Instrumented build differs from the verified build.** Foundry reports: @@ -96,26 +127,33 @@ It produced no repository artifact. files, so test and fixture code is counted alongside protocol code. Both are reported separately below, and the production aggregates are computed from the per-file rows rather than reported by Foundry. -3. **`src/mocks/MockUSDC.sol` and `src/mocks/MockUSTB.sol` report 0.00%.** The uncovered items are their - `name()` and `symbol()` overrides, which nothing in the suite calls. They are deterministic fixture +3. **The repository-level row is not comparable across these two checkpoints.** GI added four instrumented + test files, so the denominators moved (1361 → 1769 lines). Only the per-file and computed production + figures below are like-for-like. + +4. **`src/mocks/MockUSDC.sol` and `src/mocks/MockUSTB.sol` still report 0.00%.** The uncovered items are + their `name()` and `symbol()` overrides, which nothing in the suite calls. They are deterministic fixture currencies, not protocol code. -4. **Coverage counts execution, not intent.** A covered branch is one the suite reached; it is not evidence - that what the branch does is correct, and it is not evidence about any invariant. +5. **Coverage counts execution, not intent.** A covered branch is one the suite reached; it is not evidence + that what the branch does is correct, and it is not evidence about any invariant. In particular, the + stateful invariant campaigns contribute coverage exactly like any other test, and none of the figures + below is evidence for or against G-I. --- ## Repository-Level Coverage Reported by Foundry across all instrumented files (`src/`, `script/`, `test/`). The four dimensions are -distinct and are deliberately not collapsed into one number. +distinct and are deliberately not collapsed into one number. See limitation 3: the denominators changed, so +the post-F8D column is context rather than a comparison. -| Dimension | Coverage | -| ------------ | -------------------- | -| Lines | 95.52% (1300 / 1361) | -| Statements | 94.72% (1239 / 1308) | -| Branches | 79.47% (120 / 151) | -| Functions | 97.03% (294 / 303) | +| Dimension | Post-F8D | Post-GI | +| ------------ | -------------------- | -------------------- | +| Lines | 95.52% (1300 / 1361) | 96.21% (1702 / 1769) | +| Statements | 94.72% (1239 / 1308) | 95.92% (1694 / 1766) | +| Branches | 79.47% (120 / 151) | 86.94% (193 / 222) | +| Functions | 97.03% (294 / 303) | 97.01% (357 / 368) | --- @@ -123,9 +161,9 @@ distinct and are deliberately not collapsed into one number. ### Per file, as reported -| File | Lines | Statements | Branches | Functions | -| ------------------------------------ | ---------------- | ---------------- | -------------- | -------------- | -| `src/StandbyHook.sol` | 99.73% (366/367) | 98.52% (400/406) | 92.77% (77/83) | 100.00% (66/66) | +| File | Lines | Statements | Branches | Functions | +| ------------------------------------ | ---------------- | ---------------- | -------------- | --------------- | +| `src/StandbyHook.sol` | 99.73% (366/367) | 98.77% (401/406) | 93.98% (78/83) | 100.00% (66/66) | | `src/ExerciseRouter.sol` | 97.14% (68/70) | 95.31% (61/64) | 72.73% (8/11) | 100.00% (16/16) | | `src/EligibilityRegistry.sol` | 100.00% (20/20) | 100.00% (14/14) | 100.00% (2/2) | 100.00% (8/8) | | `src/libraries/StandbyMath.sol` | 100.00% (34/34) | 100.00% (28/28) | 100.00% (7/7) | 100.00% (9/9) | @@ -136,7 +174,10 @@ distinct and are deliberately not collapsed into one number. | `src/mocks/MockUSDC.sol` | 0.00% (0/4) | 0.00% (0/2) | 100.00% (0/0) | 0.00% (0/2) | | `src/mocks/MockUSTB.sol` | 0.00% (0/4) | 0.00% (0/2) | 100.00% (0/0) | 0.00% (0/2) | -Deployment and configuration sources, for completeness: +`src/StandbyHook.sol` is the only production file whose figures moved: statements 400 → 401 and branches +77 → 78, out of unchanged denominators. Every other production file is identical to the post-F8D baseline. + +Deployment and configuration sources, for completeness — all unchanged from the baseline: | File | Lines | Statements | Branches | Functions | | ------------------------------------------------- | --------------- | --------------- | ------------- | -------------- | @@ -144,102 +185,155 @@ Deployment and configuration sources, for completeness: | `script/helpers/DeterministicFixtureDeployer.sol` | 81.82% (18/22) | 85.19% (23/27) | 25.00% (1/4) | 100.00% (3/3) | | `script/helpers/HelperConfig.s.sol` | 100.00% (8/8) | 100.00% (8/8) | 100.00% (1/1) | 100.00% (2/2) | -### Computed aggregates +### Computed aggregates — post-F8D baseline, post-GI, delta -Summed from the per-file rows above. These are computed here, not reported by Foundry. +Summed from the per-file rows. These are computed here, not reported by Foundry. Standby protocol core — the Hook, the ExerciseRouter, the EligibilityRegistry, and the three libraries: -| Dimension | Coverage | -| ---------- | ------------------ | -| Lines | 99.42% (514 / 517) | -| Statements | 98.33% (531 / 540) | -| Branches | 91.35% (95 / 104) | -| Functions | 100.00% (107 / 107) | +| Dimension | Post-F8D baseline | Post-GI | Delta | +| ---------- | ------------------- | ------------------- | -------------------- | +| Lines | 99.42% (514 / 517) | 99.42% (514 / 517) | unchanged | +| Statements | 98.33% (531 / 540) | 98.52% (532 / 540) | +0.19 pp (+1 stmt) | +| Branches | 91.35% (95 / 104) | 92.31% (96 / 104) | +0.96 pp (+1 branch) | +| Functions | 100.00% (107 / 107) | 100.00% (107 / 107) | unchanged | All of `src/`, including the demo router and the fixture currencies: -| Dimension | Coverage | -| ---------- | ------------------ | -| Lines | 98.01% (590 / 602) | -| Statements | 97.39% (598 / 614) | -| Branches | 90.35% (103 / 114) | -| Functions | 96.90% (125 / 129) | +| Dimension | Post-F8D baseline | Post-GI | Delta | +| ---------- | ------------------- | ------------------- | -------------------- | +| Lines | 98.01% (590 / 602) | 98.01% (590 / 602) | unchanged | +| Statements | 97.39% (598 / 614) | 97.56% (599 / 614) | +0.17 pp (+1 stmt) | +| Branches | 90.35% (103 / 114) | 91.23% (104 / 114) | +0.88 pp (+1 branch) | +| Functions | 96.90% (125 / 129) | 96.90% (125 / 129) | unchanged | + +--- + +## Newly Covered Production Surfaces Attributable to GI + +Exactly one production surface moved from uncovered to covered: + +### `src/StandbyHook.sol` L1668 — `_beforeRemoveLiquidity` → `StandbyHook__UntrustedLiquidityPerimeter` + +The refusal of a **liquidity removal** proposed by a callback sender that is not the trusted liquidity +perimeter. It was **potential GI input #1** in the post-F8D report — the one uncovered item there identified +as intersecting an O3 authority boundary on a backing-affecting transition most directly. + +GI reaches it because the invariant handler routes a fraction of its generated liquidity actions through the +ordinary-swap perimeter rather than the liquidity perimeter, and because the scripted liquidity-perimeter +sequence performs a removal through the wrong perimeter against an authentic positive obligation. The +addition-side refusal was already covered before GI; both sides of the liquidity perimeter boundary are now +covered. + +That this branch is now executed says only that the suite reached it. What it is evidence *for* is recorded +in the GI evidence itself, not here. --- ## Material Uncovered Production Areas -Every uncovered production item is listed. Each is a rejection path or a defensive clamp; none is an -untested economic transition, and none is classified here as a defect. +Every uncovered production item is listed, as reported by `forge coverage --report debug`. Each is a +rejection path, a defensive clamp, or fixture metadata; none is an untested economic transition, and none is +classified here as a defect. -### `src/StandbyHook.sol` — 1 line, 6 statements, 6 branches +### `src/StandbyHook.sol` — 1 line, 5 statements, 5 branches (was 1 / 6 / 6) | Location | Construct | Note | | -------- | --------- | ---- | -| L1062 | `authorizeExercise` → `StandbyHook__ServiceNotConfigured` | O2 authorization against a Hook with no service. Every exercise fixture activates a service first. | -| L1218–1219 | `authorizedProtectedExecution` → `StandbyHook__ExerciseExecutionNotAuthorized` | The read surface consulted while the causal context is not `AUTHORIZED`. The equivalent refusal on the authoritative callback path *is* covered. | -| L1668 | `_beforeRemoveLiquidity` → `StandbyHook__UntrustedLiquidityPerimeter` | Liquidity **removal** proposed by an untrusted sender. The same refusal on **addition** is covered. | +| L1062 | `authorizeExercise` → `StandbyHook__ServiceNotConfigured` | O2 authorization against a Hook with no service. Every fixture, GI included, activates a service first. | +| L1218–1220 | `authorizedProtectedExecution` → `StandbyHook__ExerciseExecutionNotAuthorized` | The read surface consulted while the causal context is not `AUTHORIZED`. The equivalent refusal on the authoritative callback path *is* covered. | | L2217 | `_beginSwapDerivation` → `StandbyHook__ServiceNotConfigured` | Prospective swap derivation before activation. | | L2343 | `_nextSwapTargetTick` → `tickNext <= TickMath.MIN_TICK` clamp | Mirrors the pinned v4 swap loop's own clamping; reachable only at the extreme tick bound. | | L2344 | `_nextSwapTargetTick` → `tickNext >= TickMath.MAX_TICK` clamp | As above, at the opposite bound. | -### `src/ExerciseRouter.sol` — 2 lines, 3 statements, 3 branches +`L1668` — previously in this table — is now covered. + +### `src/ExerciseRouter.sol` — 2 lines, 3 statements, 3 branches (unchanged) | Location | Construct | Note | | -------- | --------- | ---- | -| L395–396 | `ExerciseRouter__InputTransferFailed` | Reached only when `transferFrom` returns `false` without reverting. The fixture currency reverts with its own typed errors instead, and those failure modes *are* covered. | +| L395–396 | `ExerciseRouter__InputTransferFailed` | Reached only when `transferFrom` returns `false` without reverting. The fixture currencies revert with typed errors instead, and those failure modes *are* covered. | | L441–443 | `ExerciseRouter__UnresolvedExerciseDelta` | The fail-closed guard for an exercise leaving an open PoolManager delta. Settlement and delivery close each side exactly, so no reachable path leaves one open. | | L475 | `ExerciseRouter__ExerciseContextAlreadyActive` | A nested `exercise()` while one is already in flight. | -### `src/demo/ActorAwareTestRouter.sol` — 2 statements, 2 branches +### `src/demo/ActorAwareTestRouter.sol` — 2 statements, 2 branches (unchanged) `ActorAwareTestRouter__NotPoolManager` (L195) and `ActorAwareTestRouter__SettlementTransferFailed` (L244). This contract is demo and test-perimeter instrumentation, not protocol. -### `src/mocks/` — fixture metadata +### `src/mocks/` — fixture metadata (unchanged) `MockUSDC.name/symbol` and `MockUSTB.name/symbol` are never called; `MockFixtureCurrency` L118 is the allowance-decrement path taken only when the allowance is not `type(uint256).max`. -### `script/DeployStandbyHook.s.sol` — 22 lines, 25 statements, 6 branches +### `script/DeployStandbyHook.s.sol` — 22 lines, 25 statements, 6 branches (unchanged) -The lowest production-adjacent figure in the repository. The mining and validation procedure is exercised -by every fixture, but the broadcasting `run()` entrypoint and its validation failure branches are not -reached by `forge test` — consistent with the limitation already recorded in `docs/project-status.md`, that -`run()` is verified in script simulation rather than against a live node. +The mining and validation procedure is exercised by every fixture, but the broadcasting `run()` entrypoint +and its validation failure branches are not reached by `forge test` — consistent with the limitation already +recorded in `docs/project-status.md`, that `run()` is verified in script simulation rather than against a +live node. --- -## Potential GI Inputs +## Classification of What Remains + +### Semantically relevant, and still uncovered + +- **`ExerciseRouter.sol` L475 — nested `exercise()` refusal.** This was **potential GI input #2** in the + post-F8D report and GI did not reach it. GI generates top-level actions, so it cannot nest one exercise + inside another; the Session 15 record states this as a known reachability gap rather than as covered. The + adjacent Hook-side restriction — a second authorization while one is unresolved — is covered, and the + router's one-originator-per-request discipline has its own periphery evidence + (`test/periphery/ActorAttribution.t.sol` covers the equivalent restriction on the shared perimeter). This + is the one remaining uncovered item that is a genuine authority-boundary rejection rather than a + defensive guard. + +- **`StandbyHook.sol` L1218–1220 — causal-position refusal on `authorizedProtectedExecution`.** A read + surface, whose equivalent refusal on the authoritative callback path is covered. §28 of the GI session + prompt deliberately declined to make this a GI obligation, and this refresh does not reopen that. + +### Diagnostic, defensive, or structurally unreachable through the supported production domain + +- **`StandbyHook.sol` L1062 and L2217 — `ServiceNotConfigured`.** Unreachable once a service exists, which + every fixture and every campaign establishes first. Their equivalents elsewhere in the Hook are covered. +- **`StandbyHook.sol` L2343–2344 — tick-bound clamps.** Reachable only outside the configured service + domain, which enforcement prevents any authoritative transition from entering. They mirror the pinned v4 + swap loop's own clamping and remain principally an F5 derivation concern. +- **`ExerciseRouter.sol` L395–396 — `InputTransferFailed`.** Requires a currency that returns `false` + instead of reverting; the supported fixture currencies revert. +- **`ExerciseRouter.sol` L441–443 — `UnresolvedExerciseDelta`.** Structurally unreachable on the production + path: settlement and delivery close each side exactly, and the guard exists to fail closed if they ever + did not. +- **`ActorAwareTestRouter` and `src/mocks/`.** Demo perimeter and fixture instrumentation, not protocol. +- **`script/DeployStandbyHook.s.sol` `run()`.** Broadcast entrypoint, already recorded as verified in script + simulation only. + +### Test-side instrumentation notes + +Two GI handler functions, `scriptedSetTraderEligibility` and `scriptedSetLiquidityEligibility`, are reported +as 0-hit *functions* while every statement inside them is covered. Both are called only internally by the +generated-action entry points, never through an external call, and the campaign counters record 25 and 52 +accepted mutations respectively — so this is a function-entry attribution artifact of the instrumentation, +not dead code. The remaining uncovered GI test statements are the `assertTrue(false, …)` arms that exist +precisely so that they never execute: the orphan-authorization and orphan-finalization success branches, the +"an admitted commitment must occupy a bounded enforcement reference" guard, and the ordered-currency +deployment fallback. -Recorded as **potential inputs to GI derivation, not as established GI requirements.** GI has not been -started and no derivation was performed here. Whether any of these belongs in GI is for GI's own derivation -to decide against `docs/invariants.md` and `docs/testing-strategy.md`. - -1. **Untrusted-perimeter liquidity removal** (`StandbyHook.sol` L1668). An O3 authority boundary on a - backing-affecting transition. A GI handler that generates liquidity actions from arbitrary senders would - intersect this path directly. - -2. **Nested exercise attribution** (`ExerciseRouter.sol` L475). The router's one-originator-per-request - discipline. It sits beside the Hook's own overlapping-authorization restriction, which is covered, and - the economic-reentrancy restriction of `uniswap-v4-realization.md` §16.3 is an invariant-relevant - property. - -3. **The causal-position refusal on the read surface** (`StandbyHook.sol` L1218–1219). A sequence-dependent - guard on a surface an adversarial handler could consult at any causal position. +--- -4. **Tick-bound clamping in the prospective swap derivation** (`StandbyHook.sol` L2343–2344). Reachable only - outside the configured service domain. A GI swap handler with deliberately extreme inputs is the kind of - generator that would reach it, and the prospective derivation is the authoritative input to backing - enforcement. +## Disposition of the Post-F8D "Potential GI Inputs" -5. **The unresolved-delta guard** (`ExerciseRouter.sol` L441–443). Structurally unreachable on the current - production path. Noted because it is the router's own fail-closed statement about exercise-local delta - isolation (RR-O2-15), and adversarial sequencing is what GI generates. +The previous revision recorded five uncovered items as **potential** GI inputs. GI has since been derived, +implemented, and independently reviewed. Their disposition, recorded here for continuity only: -Items 1 and 2 are the two that intersect an authority or state-transition boundary most directly. Items 3–5 -are noted for completeness. +| # | Item | Disposition | +| - | ---- | ----------- | +| 1 | Untrusted-perimeter liquidity removal (`StandbyHook.sol` L1668) | **Taken up by GI and now covered** — generated wrong-perimeter liquidity actions plus a scripted liquidity-perimeter sequence. | +| 2 | Nested exercise attribution (`ExerciseRouter.sol` L475) | **Considered, not reachable by GI.** GI acts at top level; recorded as a known reachability gap in `docs/prompts/session-15-log.md`. Still uncovered. | +| 3 | Causal-position refusal on the read surface (`StandbyHook.sol` L1218–1220) | **Deliberately excluded** by §28 of the GI session prompt. Still uncovered. | +| 4 | Tick-bound clamping (`StandbyHook.sol` L2343–2344) | **Deliberately excluded** by §28 unless GI exposed a reachable compositional counterexample; it did not. Still uncovered. | +| 5 | Unresolved-delta guard (`ExerciseRouter.sol` L441–443) | **Structurally unreachable** on the production path; GI's completed exercises resolve both sides exactly. Still uncovered. | -The two `ServiceNotConfigured` refusals and the fixture-currency metadata are **not** proposed as GI inputs: -GI operates against an activated service, and the mocks carry no protocol behavior. +No coverage observation in this refresh exposed a previously unrecognized frozen verification obligation. No +test was added, removed, weakened, or suppressed to affect coverage, and no production code was excluded +from measurement or changed in any way. diff --git a/test/invariant/BaseStandbyInvariantTest.t.sol b/test/invariant/BaseStandbyInvariantTest.t.sol new file mode 100644 index 0000000..9811806 --- /dev/null +++ b/test/invariant/BaseStandbyInvariantTest.t.sol @@ -0,0 +1,607 @@ +// SPDX-License-Identifier: MIT +pragma solidity 0.8.26; + +/*////////////////////////////////////////////////////////////// + IMPORTS +//////////////////////////////////////////////////////////////*/ + +import {Test} from "forge-std/Test.sol"; + +import {PoolManager} from "v4-core/PoolManager.sol"; +import {IHooks} from "v4-core/interfaces/IHooks.sol"; +import {IPoolManager} from "v4-core/interfaces/IPoolManager.sol"; +import {StateLibrary} from "v4-core/libraries/StateLibrary.sol"; +import {TickMath} from "v4-core/libraries/TickMath.sol"; +import {Currency} from "v4-core/types/Currency.sol"; +import {PoolId, PoolIdLibrary} from "v4-core/types/PoolId.sol"; +import {PoolKey} from "v4-core/types/PoolKey.sol"; +import {ModifyLiquidityParams} from "v4-core/types/PoolOperation.sol"; + +import {DeployStandbyHook} from "../../script/DeployStandbyHook.s.sol"; + +import {EligibilityRegistry} from "../../src/EligibilityRegistry.sol"; +import {ExerciseRouter} from "../../src/ExerciseRouter.sol"; +import {StandbyHook} from "../../src/StandbyHook.sol"; +import {ActorAwareTestRouter} from "../../src/demo/ActorAwareTestRouter.sol"; +import {IEligibilityRegistry} from "../../src/interfaces/IEligibilityRegistry.sol"; +import {MAX_LIVE_COMMITMENTS} from "../../src/libraries/CommitmentRefs.sol"; + +import {ReferenceCalculations} from "../shared/ReferenceCalculations.sol"; +import {IInvariantCurrency, StandbyInvariantHandler} from "./StandbyInvariantHandler.sol"; + +/*////////////////////////////////////////////////////////////// + CONTRACTS +//////////////////////////////////////////////////////////////*/ + +/// @notice Shared production-only environment and global invariant closure for the GI campaigns. +/// @dev Every contract this fixture stands up is the production one, and every fact it establishes is +/// established the way production establishes it: the real pinned `PoolManager`, the canonical +/// `DeployStandbyHook` mining and deployment procedure, the real `EligibilityRegistry` under its own +/// administrator, the production `ExerciseRouter` the service is activated with, a real +/// `PoolManager.initialize`, the production `configureAndActivate` transition, and bootstrap liquidity +/// added through the production `beforeAddLiquidity` path by an eligible provider routed through the +/// trusted liquidity perimeter. +/// +/// No `StandbyHookHarness` is involved anywhere. No Remaining Entitlement, admitted extent, bounded +/// reference, Supporting Capacity, Capacity Obligation, validity, exercisability, fulfillment, or O2 +/// causal state is written directly. The only thing this fixture decides is the configuration the +/// service is activated with; everything after activation is reached by generated production +/// transitions. +/// +/// The fixture is parameterized rather than canonical-only, because GI must not prove safety for one +/// demo identity and direction. A concrete campaign supplies its service geometry and its currencies. +/// +/// Two independent oracles carry the derivation equivalence. Supporting Capacity is recomputed by +/// `ReferenceCalculations` from authoritative PoolManager state with its own Q64.96 arithmetic. +/// Aggregate Capacity Obligation is recomputed from the persisted commitment *facts* of the whole +/// allocated history — every identity in `[1, nextCommitmentId)`, not the bounded index production +/// scans — so an obligation that silently escaped the index would be visible as a disagreement rather +/// than shared by both sides of the comparison. +abstract contract BaseStandbyInvariantTest is Test { + using PoolIdLibrary for PoolKey; + using StateLibrary for IPoolManager; + + /*////////////////////////////////////////////////////////////// + TYPE DECLARATIONS + //////////////////////////////////////////////////////////////*/ + + /// @notice The complete description of the Standby service one campaign runs against. + /// @param decimals0 The decimal precision of currency0. + /// @param decimals1 The decimal precision of currency1. + /// @param protectedZeroForOne The protected swap direction. + /// @param initialTick The tick whose exact price the pool is initialized at. + /// @param tickQ The protected execution-quality boundary. + /// @param tickO The opposite realization-domain boundary. + /// @param lpTickLower The lower endpoint of the bootstrap liquidity position. + /// @param lpTickUpper The upper endpoint of the bootstrap liquidity position. + /// @param tickSpacing The pool tick spacing. + /// @param lpFee The static LP fee, in pips. + /// @param liquidity The bootstrap liquidity added over the position. + struct InvariantServiceConfig { + uint8 decimals0; + uint8 decimals1; + bool protectedZeroForOne; + int24 initialTick; + int24 tickQ; + int24 tickO; + int24 lpTickLower; + int24 lpTickUpper; + int24 tickSpacing; + uint24 lpFee; + uint128 liquidity; + } + + /*////////////////////////////////////////////////////////////// + STATE VARIABLES + //////////////////////////////////////////////////////////////*/ + + /// @dev A realistic starting time, so both an already-open and a not-yet-open exercise window are + /// expressible against the same campaign. + uint256 internal constant FIXTURE_TIMESTAMP = 1_800_000_000; + + /// @dev Campaign funding. Far larger than any position, swap, or exercise a campaign can produce. + uint256 internal constant CAMPAIGN_FUNDING = 1e30; + + /// @dev The bound on the deterministic search for correctly ordered currency addresses. + uint256 internal constant MAX_CURRENCY_ORDERING_ATTEMPTS = 64; + + address internal configurationAuthority; + address internal registryAdmin; + address internal establishmentAuthority; + address internal beneficiaryA; + address internal beneficiaryB; + address internal ineligibleBeneficiary; + address internal authorizedExerciser; + address internal unauthorizedExerciser; + address internal eligibleTrader; + address internal ineligibleTrader; + address internal eligibleProvider; + address internal ineligibleProvider; + address internal donor; + address internal outsider; + + IPoolManager internal poolManager; + ActorAwareTestRouter internal swapPerimeter; + ActorAwareTestRouter internal liquidityPerimeter; + DeployStandbyHook internal hookDeployer; + StandbyHook internal hook; + EligibilityRegistry internal registry; + ExerciseRouter internal exerciseRouter; + + IInvariantCurrency internal currency0; + IInvariantCurrency internal currency1; + + PoolKey internal servicePoolKey; + PoolId internal servicePoolId; + + InvariantServiceConfig internal serviceConfig; + + StandbyInvariantHandler internal handler; + + /*////////////////////////////////////////////////////////////// + SETUP + //////////////////////////////////////////////////////////////*/ + + /// @notice Builds, activates, and bootstraps one production Standby service and its campaign handler. + function setUp() public virtual { + serviceConfig = _serviceConfig(); + + _createActors(); + + poolManager = IPoolManager(address(new PoolManager(address(this)))); + + swapPerimeter = new ActorAwareTestRouter(poolManager); + liquidityPerimeter = new ActorAwareTestRouter(poolManager); + + hookDeployer = new DeployStandbyHook(); + + (hook,) = hookDeployer.deployStandbyHook( + poolManager, + address(hookDeployer), + configurationAuthority, + address(swapPerimeter), + address(liquidityPerimeter) + ); + + registry = new EligibilityRegistry(registryAdmin); + exerciseRouter = new ExerciseRouter(hook); + + (currency0, currency1) = _deployCurrencies(); + + servicePoolKey = PoolKey({ + currency0: Currency.wrap(address(currency0)), + currency1: Currency.wrap(address(currency1)), + fee: serviceConfig.lpFee, + tickSpacing: serviceConfig.tickSpacing, + hooks: IHooks(address(hook)) + }); + servicePoolId = servicePoolKey.toId(); + + poolManager.initialize(servicePoolKey, TickMath.getSqrtPriceAtTick(serviceConfig.initialTick)); + + vm.prank(configurationAuthority); + hook.configureAndActivate( + servicePoolKey, + serviceConfig.protectedZeroForOne, + serviceConfig.tickQ, + serviceConfig.tickO, + IEligibilityRegistry(address(registry)), + address(exerciseRouter), + establishmentAuthority + ); + + _grantInitialEligibility(); + _fundActors(); + _addBootstrapLiquidity(); + + vm.warp(FIXTURE_TIMESTAMP); + + handler = new StandbyInvariantHandler(_environment(), _actors()); + + _targetCampaignActions(); + } + + /*////////////////////////////////////////////////////////////// + GI-A — ECONOMIC BACKING + //////////////////////////////////////////////////////////////*/ + + /// @notice Proves production Supporting Capacity equals its independent reconstruction. (G-I-1) + function invariant_supportingCapacityEqualsIndependentReference() public view { + assertEq( + hook.supportingCapacity(), + _referenceSupportingCapacity(), + "production Supporting Capacity must equal the independent reference" + ); + } + + /// @notice Proves production Aggregate Capacity Obligation equals its independent reconstruction. + /// (G-I-2) + /// @dev The reference sums the whole allocated commitment history rather than the bounded index, so an + /// obligation that vanished from the index is a disagreement rather than a shared blind spot. + function invariant_capacityObligationEqualsIndependentReference() public view { + assertEq( + hook.aggregateObligation(), + _referenceAggregateObligation(), + "production Aggregate Capacity Obligation must equal the independent reference" + ); + } + + /// @notice Proves the service stays backed in every reachable authoritative state. (G-I-3) + function invariant_supportingCapacityCoversCapacityObligation() public view { + assertGe( + _referenceSupportingCapacity(), + _referenceAggregateObligation(), + "Supporting Capacity must never fall below Aggregate Capacity Obligation" + ); + } + + /*////////////////////////////////////////////////////////////// + GI-B/C — COMMITMENT CONSERVATION + //////////////////////////////////////////////////////////////*/ + + /// @notice Proves every commitment's admitted facts, bound, monotonicity, and conservation. + /// (G-I-4, G-I-5, G-I-6, G-I-7) + function invariant_commitmentConservation() public view { + uint256 count = handler.commitmentCount(); + + for (uint256 i = 0; i < count; ++i) { + uint256 commitmentId = handler.knownCommitmentIds(i); + + StandbyHook.Commitment memory record = hook.commitment(commitmentId); + StandbyInvariantHandler.AdmittedFacts memory facts = handler.admittedCommitmentFacts(commitmentId); + + assertEq( + PoolId.unwrap(record.serviceId), + PoolId.unwrap(facts.serviceId), + "an admitted service identity must never change" + ); + assertEq(record.beneficiary, facts.beneficiary, "an admitted Beneficiary must never change"); + assertEq( + record.exerciseAuthority, facts.exerciseAuthority, "an admitted exercise authority must never change" + ); + assertEq( + uint256(record.exercisableFrom), + uint256(facts.exercisableFrom), + "an admitted exercise window must never change" + ); + assertEq(uint256(record.validUntil), uint256(facts.validUntil), "an admitted validity must never change"); + assertEq( + uint256(record.originalEntitlement), + uint256(facts.originalEntitlement), + "an admitted entitlement extent must never be rewritten" + ); + + assertLe( + uint256(record.remainingEntitlement), + uint256(facts.originalEntitlement), + "Remaining Entitlement must never exceed the admitted extent" + ); + assertLe( + uint256(record.remainingEntitlement), + uint256(handler.ghostLastRemaining(commitmentId)), + "Remaining Entitlement must never increase" + ); + assertEq( + uint256(facts.originalEntitlement) - uint256(record.remainingEntitlement), + handler.ghostFulfilled(commitmentId), + "the discharged portion must equal independently tracked successful fulfillment" + ); + } + } + + /// @notice Proves every Beneficiary holds exactly Standby delivery plus unrelated donation. + /// (G-I-12, G-I-14) + /// @dev No Beneficiary trades, provides liquidity, exercises, or holds protected output at campaign + /// start, so its balance is a complete independent history of everything that reached it. Standby + /// delivery and unrelated donation are accounted separately, so a direct transfer can never be + /// mistaken for fulfillment and fulfillment can never be satisfied by a donation. + function invariant_beneficiaryHoldingsMatchIndependentDeliveryHistory() public view { + _assertBeneficiaryHoldings(beneficiaryA); + _assertBeneficiaryHoldings(beneficiaryB); + _assertBeneficiaryHoldings(ineligibleBeneficiary); + } + + /*////////////////////////////////////////////////////////////// + GI-E — BOUNDED REFERENCE INTEGRITY + //////////////////////////////////////////////////////////////*/ + + /// @notice Proves the bounded index stays bounded, unique, and non-dangling. (G-I-17, G-I-18) + function invariant_boundedReferenceIntegrity() public view { + uint256[MAX_LIVE_COMMITMENTS] memory references = hook.enforcementReferences(); + uint256 nextCommitmentId = hook.nextCommitmentId(); + uint256 live; + + for (uint256 slot = 0; slot < MAX_LIVE_COMMITMENTS; ++slot) { + uint256 commitmentId = references[slot]; + + if (commitmentId == 0) continue; + + ++live; + + assertLt(commitmentId, nextCommitmentId, "a live reference must resolve to an allocated commitment"); + + for (uint256 other = slot + 1; other < MAX_LIVE_COMMITMENTS; ++other) { + assertTrue(references[other] != commitmentId, "a commitment must never occupy two references"); + } + } + + assertLe(live, MAX_LIVE_COMMITMENTS, "the live reference set must stay bounded"); + } + + /// @notice Proves only frozen permanent non-binding causes release a live reference. (G-I-20) + /// @dev Stated as its contrapositive, which is the checkable form: every commitment that still carries + /// a positive Capacity Obligation still occupies a reference. A binding commitment that had lost + /// its reference would have silently left the aggregate the whole service is enforced against. + function invariant_bindingCommitmentsRetainALiveReference() public view { + uint256 nextCommitmentId = hook.nextCommitmentId(); + + for (uint256 commitmentId = 1; commitmentId < nextCommitmentId; ++commitmentId) { + StandbyHook.Commitment memory record = hook.commitment(commitmentId); + + uint256 obligation = ReferenceCalculations.referenceCommitmentObligation( + record.remainingEntitlement, record.validUntil, block.timestamp + ); + + if (obligation == 0) continue; + + assertTrue(_isReferenced(commitmentId), "a commitment still carrying obligation must stay referenced"); + } + } + + /*////////////////////////////////////////////////////////////// + GI-D/GI-23 — CUSTODY / CAUSALITY + //////////////////////////////////////////////////////////////*/ + + /// @notice Proves the protocol holds no currency custody of any kind. (G-I-16) + /// @dev No campaign action donates to the Hook or the ExerciseRouter, so any balance either holds was + /// created by a protocol flow. Both currencies are checked, because a coordinator that briefly + /// held the input side would be a custodian just as much as one holding the output. + function invariant_protocolHoldsNoCurrencyCustody() public view { + assertEq(currency0.balanceOf(address(hook)), 0, "the Hook must hold no currency0"); + assertEq(currency1.balanceOf(address(hook)), 0, "the Hook must hold no currency1"); + assertEq(currency0.balanceOf(address(exerciseRouter)), 0, "the ExerciseRouter must hold no currency0"); + assertEq(currency1.balanceOf(address(exerciseRouter)), 0, "the ExerciseRouter must hold no currency1"); + } + + /// @notice Proves no reusable O2 causal evidence survives a completed transaction. (G-I-21) + function invariant_noReusableCausalEvidenceSurvives() public view { + StandbyHook.ExerciseAuthorizationContext memory context = hook.exerciseAuthorization(); + + assertEq( + uint256(context.state), + uint256(StandbyHook.ExerciseAuthorizationState.EMPTY), + "no causal context may survive its transaction" + ); + assertEq(PoolId.unwrap(context.serviceId), bytes32(0), "no surviving causal context may name a service"); + assertEq(context.commitmentId, 0, "no surviving causal context may name a commitment"); + assertEq(context.exerciseRouter, address(0), "no surviving causal context may name a coordinator"); + assertEq(context.exerciser, address(0), "no surviving causal context may name an exerciser"); + assertEq(context.beneficiary, address(0), "no surviving causal context may name a Beneficiary"); + assertEq(context.q, 0, "no surviving causal context may carry a quantity"); + } + + /*////////////////////////////////////////////////////////////// + INTERNAL FUNCTIONS + //////////////////////////////////////////////////////////////*/ + + /// @dev The service geometry this campaign runs against. + function _serviceConfig() internal view virtual returns (InvariantServiceConfig memory config); + + /// @dev Deploys the campaign's currencies, already satisfying the Uniswap ordering requirement. + function _deployCurrencies() + internal + virtual + returns (IInvariantCurrency deployed0, IInvariantCurrency deployed1); + + /// @dev Creates the bounded persistent actor universe, one identity per role. + function _createActors() internal { + configurationAuthority = makeAddr("configurationAuthority"); + registryAdmin = makeAddr("registryAdmin"); + establishmentAuthority = makeAddr("establishmentAuthority"); + beneficiaryA = makeAddr("beneficiaryA"); + beneficiaryB = makeAddr("beneficiaryB"); + ineligibleBeneficiary = makeAddr("ineligibleBeneficiary"); + authorizedExerciser = makeAddr("authorizedExerciser"); + unauthorizedExerciser = makeAddr("unauthorizedExerciser"); + eligibleTrader = makeAddr("eligibleTrader"); + ineligibleTrader = makeAddr("ineligibleTrader"); + eligibleProvider = makeAddr("eligibleProvider"); + ineligibleProvider = makeAddr("ineligibleProvider"); + donor = makeAddr("donor"); + outsider = makeAddr("outsider"); + } + + /// @dev Grants the eligibility the campaign starts from, through the registry's own administrator. + /// + /// The three permanently ineligible identities are never granted anything here and are never + /// candidates for a campaign eligibility mutation, so "ineligible" stays a stable relationship a + /// multi-operation history can be verified against. + function _grantInitialEligibility() internal { + vm.startPrank(registryAdmin); + + registry.setBeneficiaryEligibility(beneficiaryA, true); + registry.setBeneficiaryEligibility(beneficiaryB, true); + registry.setTraderEligibility(eligibleTrader, true); + registry.setLiquidityEligibility(eligibleProvider, true); + + vm.stopPrank(); + } + + /// @dev Funds the campaign actors by role, and only by role. + /// + /// The asymmetry is deliberate and load-bearing. Beneficiaries are funded with nothing at all, so + /// every unit of protected output they ever hold arrived through a Standby delivery or an + /// unrelated donation this campaign tracked. Exercisers hold input currency only, so an exercise + /// delivery can never have come out of the exerciser's own protected-output balance. The donor + /// holds protected output and no Standby role whatsoever. + function _fundActors() internal { + _fundTradingActor(eligibleTrader); + _fundTradingActor(ineligibleTrader); + _fundTradingActor(eligibleProvider); + _fundTradingActor(ineligibleProvider); + _fundTradingActor(outsider); + + _fundExerciser(authorizedExerciser); + _fundExerciser(unauthorizedExerciser); + + _protectedOutputCurrency().mint(donor, CAMPAIGN_FUNDING); + } + + /// @dev Funds an actor with both currencies and approves both trusted perimeters on its behalf. + function _fundTradingActor(address _account) internal { + currency0.mint(_account, CAMPAIGN_FUNDING); + currency1.mint(_account, CAMPAIGN_FUNDING); + + vm.startPrank(_account); + + currency0.approve(address(swapPerimeter), type(uint256).max); + currency1.approve(address(swapPerimeter), type(uint256).max); + currency0.approve(address(liquidityPerimeter), type(uint256).max); + currency1.approve(address(liquidityPerimeter), type(uint256).max); + + vm.stopPrank(); + } + + /// @dev Funds an exerciser with input currency only, and lets the production router coordinate payment. + function _fundExerciser(address _account) internal { + IInvariantCurrency inputCurrency = _inputCurrency(); + + inputCurrency.mint(_account, CAMPAIGN_FUNDING); + + vm.prank(_account); + inputCurrency.approve(address(exerciseRouter), type(uint256).max); + } + + /// @dev Adds the bootstrap liquidity through the production enforcement path. + function _addBootstrapLiquidity() internal { + ModifyLiquidityParams memory params = ModifyLiquidityParams({ + tickLower: serviceConfig.lpTickLower, + tickUpper: serviceConfig.lpTickUpper, + liquidityDelta: int256(uint256(serviceConfig.liquidity)), + salt: bytes32(0) + }); + + vm.prank(eligibleProvider); + liquidityPerimeter.modifyLiquidity(servicePoolKey, params, bytes("")); + } + + /// @dev Restricts the campaign to the handler's generated action surface. + /// + /// The scripted entry points the sequence suites use are deliberately excluded: they exist so a + /// required semantic sequence can be expressed directly, and letting the fuzzer call them with + /// unconstrained addresses would replace the persistent actor universe with anonymous callers. + function _targetCampaignActions() internal { + bytes4[] memory selectors = new bytes4[](12); + + selectors[0] = StandbyInvariantHandler.establishCommitment.selector; + selectors[1] = StandbyInvariantHandler.exercise.selector; + selectors[2] = StandbyInvariantHandler.ordinaryProtectedSwap.selector; + selectors[3] = StandbyInvariantHandler.ordinaryOppositeSwap.selector; + selectors[4] = StandbyInvariantHandler.addLiquidity.selector; + selectors[5] = StandbyInvariantHandler.removeLiquidity.selector; + selectors[6] = StandbyInvariantHandler.advanceTime.selector; + selectors[7] = StandbyInvariantHandler.setBeneficiaryEligibility.selector; + selectors[8] = StandbyInvariantHandler.setTraderEligibility.selector; + selectors[9] = StandbyInvariantHandler.setLiquidityEligibility.selector; + selectors[10] = StandbyInvariantHandler.directTransferProtectedTokenToBeneficiary.selector; + selectors[11] = StandbyInvariantHandler.attemptOrphanExerciseEvidence.selector; + + targetContract(address(handler)); + targetSelector(FuzzSelector({addr: address(handler), selectors: selectors})); + } + + /// @dev Assembles the production environment the handler drives. + function _environment() internal view returns (StandbyInvariantHandler.InvariantEnvironment memory environment) { + environment = StandbyInvariantHandler.InvariantEnvironment({ + poolManager: poolManager, + hook: hook, + exerciseRouter: exerciseRouter, + registry: registry, + swapPerimeter: swapPerimeter, + liquidityPerimeter: liquidityPerimeter, + currency0: currency0, + currency1: currency1, + poolKey: servicePoolKey, + protectedZeroForOne: serviceConfig.protectedZeroForOne, + tickQ: serviceConfig.tickQ, + tickO: serviceConfig.tickO, + tickSpacing: serviceConfig.tickSpacing, + lpTickLower: serviceConfig.lpTickLower, + lpTickUpper: serviceConfig.lpTickUpper, + initialLiquidity: serviceConfig.liquidity, + initialCapacity: _referenceSupportingCapacity() + }); + } + + /// @dev Assembles the bounded persistent actor universe the handler acts through. + function _actors() internal view returns (StandbyInvariantHandler.InvariantActors memory actors) { + actors = StandbyInvariantHandler.InvariantActors({ + registryAdmin: registryAdmin, + establishmentAuthority: establishmentAuthority, + beneficiaryA: beneficiaryA, + beneficiaryB: beneficiaryB, + ineligibleBeneficiary: ineligibleBeneficiary, + authorizedExerciser: authorizedExerciser, + unauthorizedExerciser: unauthorizedExerciser, + eligibleTrader: eligibleTrader, + ineligibleTrader: ineligibleTrader, + eligibleProvider: eligibleProvider, + ineligibleProvider: ineligibleProvider, + donor: donor, + outsider: outsider + }); + } + + /// @dev Independently derives Supporting Capacity from authoritative PoolManager state. + function _referenceSupportingCapacity() internal view returns (uint256 capacity) { + (uint160 sqrtPriceX96,,,) = poolManager.getSlot0(servicePoolId); + + capacity = ReferenceCalculations.referenceSupportingCapacity( + serviceConfig.protectedZeroForOne, + sqrtPriceX96, + serviceConfig.tickQ, + poolManager.getLiquidity(servicePoolId) + ); + } + + /// @dev Independently derives Aggregate Capacity Obligation over the whole allocated history. + function _referenceAggregateObligation() internal view returns (uint256 obligation) { + uint256 nextCommitmentId = hook.nextCommitmentId(); + + for (uint256 commitmentId = 1; commitmentId < nextCommitmentId; ++commitmentId) { + StandbyHook.Commitment memory record = hook.commitment(commitmentId); + + obligation += ReferenceCalculations.referenceCommitmentObligation( + record.remainingEntitlement, record.validUntil, block.timestamp + ); + } + } + + /// @dev Proves an account holds exactly what Standby delivered plus what unrelated transfers donated. + function _assertBeneficiaryHoldings(address _beneficiary) internal view { + assertEq( + _protectedOutputCurrency().balanceOf(_beneficiary), + handler.ghostDelivered(_beneficiary) + handler.ghostDonated(_beneficiary), + "a Beneficiary must hold exactly Standby delivery plus unrelated donation" + ); + } + + /// @dev Reports whether the bounded index currently references an identity. + function _isReferenced(uint256 _commitmentId) internal view returns (bool referenced) { + uint256[MAX_LIVE_COMMITMENTS] memory references = hook.enforcementReferences(); + + for (uint256 slot = 0; slot < MAX_LIVE_COMMITMENTS; ++slot) { + if (references[slot] == _commitmentId) return true; + } + } + + /// @dev The protected output currency, selected by the protected direction alone. + function _protectedOutputCurrency() internal view returns (IInvariantCurrency currency) { + currency = serviceConfig.protectedZeroForOne ? currency1 : currency0; + } + + /// @dev The protected input currency, selected by the protected direction alone. + function _inputCurrency() internal view returns (IInvariantCurrency currency) { + currency = serviceConfig.protectedZeroForOne ? currency0 : currency1; + } +} diff --git a/test/invariant/StandbyInvariant.t.sol b/test/invariant/StandbyInvariant.t.sol new file mode 100644 index 0000000..369dcdd --- /dev/null +++ b/test/invariant/StandbyInvariant.t.sol @@ -0,0 +1,129 @@ +// SPDX-License-Identifier: MIT +pragma solidity 0.8.26; + +/*////////////////////////////////////////////////////////////// + IMPORTS +//////////////////////////////////////////////////////////////*/ + +import {DeterministicFixtureDeployer} from "../../script/helpers/DeterministicFixtureDeployer.sol"; +import {StandbyFixtureConfig} from "../../script/helpers/StandbyFixtureConfig.sol"; + +import {MockUSDC} from "../../src/mocks/MockUSDC.sol"; +import {MockUSTB} from "../../src/mocks/MockUSTB.sol"; + +import {DerivationTestCurrency} from "../shared/BaseDerivationTest.t.sol"; +import {StandbySequenceEvidence} from "./StandbySequenceEvidence.t.sol"; +import {IInvariantCurrency} from "./StandbyInvariantHandler.sol"; + +/*////////////////////////////////////////////////////////////// + CONTRACTS +//////////////////////////////////////////////////////////////*/ + +/// @notice The canonical GI stateful invariant campaign. (G-I-1 … G-I-21, G-I-22 canonical half) +/// @dev The frozen canonical identity and direction: `MockUSTB` as currency0, `MockUSDC` as currency1, +/// both six-decimal, protected direction `zeroForOne`, the canonical domain, the canonical position, +/// and the canonical liquidity — reached through the real deterministic ordered deployment rather +/// than assumed. +/// +/// The campaign runs with `fail_on_revert = true`. That is not strictness for its own sake: the +/// handler wraps every production call and records the refusals itself, so the only way a generated +/// call can revert is a failed assertion or an unmodelled failure, and both must fail the campaign +/// rather than being silently discarded as an uninteresting sequence. +/// forge-config: default.invariant.runs = 256 +/// forge-config: default.invariant.depth = 96 +/// forge-config: default.invariant.fail_on_revert = true +/// forge-config: ci.invariant.runs = 512 +/// forge-config: ci.invariant.depth = 192 +/// forge-config: ci.invariant.fail_on_revert = true +contract StandbyCanonicalInvariantTest is StandbySequenceEvidence { + /*////////////////////////////////////////////////////////////// + INTERNAL FUNCTIONS + //////////////////////////////////////////////////////////////*/ + + /// @dev The frozen canonical deterministic fixture geometry. + function _serviceConfig() internal pure override returns (InvariantServiceConfig memory config) { + config = InvariantServiceConfig({ + decimals0: StandbyFixtureConfig.CURRENCY_DECIMALS, + decimals1: StandbyFixtureConfig.CURRENCY_DECIMALS, + protectedZeroForOne: StandbyFixtureConfig.PROTECTED_DIRECTION_ZERO_FOR_ONE, + initialTick: StandbyFixtureConfig.INITIAL_TICK, + tickQ: StandbyFixtureConfig.TICK_Q, + tickO: StandbyFixtureConfig.TICK_O, + lpTickLower: StandbyFixtureConfig.LP_TICK_LOWER, + lpTickUpper: StandbyFixtureConfig.LP_TICK_UPPER, + tickSpacing: StandbyFixtureConfig.TICK_SPACING, + lpFee: StandbyFixtureConfig.LP_FEE, + liquidity: StandbyFixtureConfig.CANONICAL_LIQUIDITY + }); + } + + /// @dev Deploys the canonical fixture currencies through the deterministic ordered deployment path. + function _deployCurrencies() + internal + override + returns (IInvariantCurrency deployed0, IInvariantCurrency deployed1) + { + (MockUSTB ustb, MockUSDC usdc,) = new DeterministicFixtureDeployer().deployOrderedFixtureCurrencies(); + + (deployed0, deployed1) = (IInvariantCurrency(address(ustb)), IInvariantCurrency(address(usdc))); + } +} + +/// @notice The generalized GI stateful invariant campaign. (G-I-22 generalized half) +/// @dev A supported configuration that shares nothing with the canonical one that could hide a +/// canonical-only assumption: the protected direction is `oneForZero`, so the protected output is +/// currency0 rather than currency1; the currencies are eighteen- and eight-decimal rather than both +/// six, so neither `1e6` nor equal precision is a usable universal scale; and the tick layout, +/// spacing, fee, and liquidity are all different. +/// +/// Supporting Capacity and Capacity Obligation stay raw amounts of whichever currency the protected +/// direction makes the output, and the same invariant closure is asserted over them. +/// forge-config: default.invariant.runs = 256 +/// forge-config: default.invariant.depth = 96 +/// forge-config: default.invariant.fail_on_revert = true +/// forge-config: ci.invariant.runs = 512 +/// forge-config: ci.invariant.depth = 192 +/// forge-config: ci.invariant.fail_on_revert = true +contract StandbyGeneralizedInvariantTest is StandbySequenceEvidence { + /*////////////////////////////////////////////////////////////// + INTERNAL FUNCTIONS + //////////////////////////////////////////////////////////////*/ + + /// @dev A protected `oneForZero` service with asymmetric decimal precision. + function _serviceConfig() internal pure override returns (InvariantServiceConfig memory config) { + config = InvariantServiceConfig({ + decimals0: 18, + decimals1: 8, + protectedZeroForOne: false, + initialTick: 0, + tickQ: 1_200, + tickO: -600, + lpTickLower: -1_200, + lpTickUpper: 1_800, + tickSpacing: 60, + lpFee: 3_000, + liquidity: 1_000_000_000_000_000 + }); + } + + /// @dev Deploys two currencies with the configured precisions, already in the required address order. + /// + /// The ordering is obtained by redeploying the pair rather than by relabelling one as the other, + /// because relabelling would silently swap the precisions this campaign intends. + function _deployCurrencies() + internal + override + returns (IInvariantCurrency deployed0, IInvariantCurrency deployed1) + { + for (uint256 attempt = 0; attempt < MAX_CURRENCY_ORDERING_ATTEMPTS; ++attempt) { + DerivationTestCurrency candidate0 = new DerivationTestCurrency(serviceConfig.decimals0); + DerivationTestCurrency candidate1 = new DerivationTestCurrency(serviceConfig.decimals1); + + if (address(candidate0) < address(candidate1)) { + return (IInvariantCurrency(address(candidate0)), IInvariantCurrency(address(candidate1))); + } + } + + assertTrue(false, "ordered currency deployment failed"); + } +} diff --git a/test/invariant/StandbyInvariantHandler.sol b/test/invariant/StandbyInvariantHandler.sol new file mode 100644 index 0000000..a3541b7 --- /dev/null +++ b/test/invariant/StandbyInvariantHandler.sol @@ -0,0 +1,1377 @@ +// SPDX-License-Identifier: MIT +pragma solidity 0.8.26; + +/*////////////////////////////////////////////////////////////// + IMPORTS +//////////////////////////////////////////////////////////////*/ + +import {Test} from "forge-std/Test.sol"; + +import {IPoolManager} from "v4-core/interfaces/IPoolManager.sol"; +import {StateLibrary} from "v4-core/libraries/StateLibrary.sol"; +import {TickMath} from "v4-core/libraries/TickMath.sol"; +import {PoolId, PoolIdLibrary} from "v4-core/types/PoolId.sol"; +import {PoolKey} from "v4-core/types/PoolKey.sol"; +import {ModifyLiquidityParams, SwapParams} from "v4-core/types/PoolOperation.sol"; + +import {EligibilityRegistry} from "../../src/EligibilityRegistry.sol"; +import {ExerciseRouter} from "../../src/ExerciseRouter.sol"; +import {StandbyHook} from "../../src/StandbyHook.sol"; +import {ActorAwareTestRouter} from "../../src/demo/ActorAwareTestRouter.sol"; +import {MAX_LIVE_COMMITMENTS} from "../../src/libraries/CommitmentRefs.sol"; + +import {ReferenceCalculations} from "../shared/ReferenceCalculations.sol"; + +/*////////////////////////////////////////////////////////////// + INTERFACES +//////////////////////////////////////////////////////////////*/ + +/// @notice The minimal exact-transfer fixture currency surface the invariant environment consumes. +/// @dev Deliberately narrow. GI never asks a currency anything economically meaningful: Supporting +/// Capacity and Capacity Obligation are raw amounts of the protected output currency, and no Standby +/// derivation may consult `decimals()`. The precision is read only so a campaign can state which +/// configuration it is running under. +interface IInvariantCurrency { + /// @notice Returns the decimal precision of the currency. + /// @return decimals_ The configured decimal precision. + function decimals() external view returns (uint8 decimals_); + + /// @notice Returns the raw balance an account holds. + /// @param _account The account to read. + /// @return balance The raw balance. + function balanceOf(address _account) external view returns (uint256 balance); + + /// @notice Mints fixture currency to an account. + /// @param _to The account receiving the minted currency. + /// @param _amount The raw amount minted. + function mint(address _to, uint256 _amount) external; + + /// @notice Approves a spender to transfer currency on behalf of the caller. + /// @param _spender The approved spender. + /// @param _amount The approved raw amount. + /// @return success Whether the approval succeeded. + function approve(address _spender, uint256 _amount) external returns (bool success); + + /// @notice Transfers currency from the caller to another account. + /// @param _to The recipient. + /// @param _amount The raw amount transferred. + /// @return success Whether the transfer succeeded. + function transfer(address _to, uint256 _amount) external returns (bool success); +} + +/*////////////////////////////////////////////////////////////// + CONTRACTS +//////////////////////////////////////////////////////////////*/ + +/// @title StandbyInvariantHandler +/// @notice The adversarial stateful transaction generator of the GI invariant campaigns. +/// @dev This contract is a transaction generator, not a safety pre-filter. It composes O1, O2, O3, +/// liquidity, eligibility, lifecycle, and unrelated-external actions into arbitrary multi-operation +/// histories, and it deliberately generates requests that must be refused: unauthorized callers, +/// ineligible actors, untrusted perimeters, inadmissible terms, over-extent quantities, breached cost +/// bounds, backing-destructive transitions, and evidence with no exercise behind it. Every one of +/// those rejections is GI evidence. +/// +/// Every action runs through a production interface. Commitments are admitted by +/// `StandbyHook.establishCommitment`, exercises are coordinated by the production `ExerciseRouter`, +/// ordinary swaps and liquidity actions arrive through the real trusted perimeters and the real +/// `PoolManager`, and eligibility is mutated through the real `EligibilityRegistry` administrator. No +/// economically authoritative state is ever written directly: not Remaining Entitlement, not the +/// admitted extent, not a bounded reference, not Supporting Capacity, not Capacity Obligation, not +/// validity, not exercisability, not fulfillment, and not the O2 causal context. +/// +/// Ghost state here remembers history and never prescribes it. It holds the identities admission +/// actually produced, the immutable facts those admissions actually recorded, the last Remaining +/// Entitlement actually observed, the quantity each successfully completed O2 actually fulfilled, and +/// the protected output actually delivered or donated to each Beneficiary. It maintains no parallel +/// validity, exercisability, binding, expiry, or obligation classification: those are Standby's own +/// state machine, and duplicating them would verify the duplicate rather than the protocol. +/// +/// Assertions are made where the property is: transition-local exactness immediately around the +/// transition that has to have it, and continuous properties in the campaign's invariant functions. +/// Every external production call is wrapped, so a refused Standby request is recorded rather than +/// discarded — which is what lets the campaigns run with `fail_on_revert = true` and treat any +/// unwrapped revert, including a failed assertion, as a campaign failure. +/// +/// Actors are a bounded persistent universe rather than fuzzed addresses, because the properties +/// under test are about stable authority relationships across a history: that administrative +/// authority, establishment authority, exercise authority, Beneficiary eligibility, trader +/// eligibility, liquidity eligibility, and ordinary invocation capability never substitute for one +/// another. A fresh random caller per call would destroy exactly the relationships GI is verifying. +contract StandbyInvariantHandler is Test { + using PoolIdLibrary for PoolKey; + using StateLibrary for IPoolManager; + + /*////////////////////////////////////////////////////////////// + TYPE DECLARATIONS + //////////////////////////////////////////////////////////////*/ + + /// @notice The complete production environment one campaign drives. + /// @param poolManager The real pinned PoolManager. + /// @param hook The production StandbyHook whose service is activated. + /// @param exerciseRouter The production ExerciseRouter the service was activated with. + /// @param registry The production EligibilityRegistry the service consumes. + /// @param swapPerimeter The trusted ordinary-swap perimeter. + /// @param liquidityPerimeter The trusted liquidity perimeter. + /// @param currency0 The pool's currency0. + /// @param currency1 The pool's currency1. + /// @param poolKey The activated service pool. + /// @param protectedZeroForOne The protected swap direction of the service. + /// @param tickQ The protected execution-quality boundary. + /// @param tickO The opposite realization-domain boundary. + /// @param tickSpacing The pool tick spacing. + /// @param lpTickLower The lower endpoint of the bootstrap liquidity position. + /// @param lpTickUpper The upper endpoint of the bootstrap liquidity position. + /// @param initialLiquidity The liquidity the bootstrap position contributed. + /// @param initialCapacity The independently derived Supporting Capacity at campaign start. + struct InvariantEnvironment { + IPoolManager poolManager; + StandbyHook hook; + ExerciseRouter exerciseRouter; + EligibilityRegistry registry; + ActorAwareTestRouter swapPerimeter; + ActorAwareTestRouter liquidityPerimeter; + IInvariantCurrency currency0; + IInvariantCurrency currency1; + PoolKey poolKey; + bool protectedZeroForOne; + int24 tickQ; + int24 tickO; + int24 tickSpacing; + int24 lpTickLower; + int24 lpTickUpper; + uint128 initialLiquidity; + uint256 initialCapacity; + } + + /// @notice The bounded persistent actor universe of one campaign. + /// @dev Each identity holds exactly one role, so no property can pass because two semantically + /// distinct authorities happened to be the same account. The three permanently ineligible + /// identities are never granted eligibility by any handler action, so "ineligible" stays a stable + /// relationship a multi-operation history can rely on. + /// @param registryAdmin The EligibilityRegistry administrator. + /// @param establishmentAuthority The per-service commitment-establishment authority. + /// @param beneficiaryA The first eligible Beneficiary. + /// @param beneficiaryB The second eligible Beneficiary. + /// @param ineligibleBeneficiary A Beneficiary that is never eligible. + /// @param authorizedExerciser The exercise authority admitted commitments name. + /// @param unauthorizedExerciser A funded exerciser that is never a commitment's exercise authority. + /// @param eligibleTrader An eligible ordinary trader. + /// @param ineligibleTrader A trader that is never eligible. + /// @param eligibleProvider The eligible liquidity provider that holds the bootstrap position. + /// @param ineligibleProvider A provider that is never eligible. + /// @param donor An account holding protected output currency and no Standby role at all. + /// @param outsider An account holding no authority, eligibility, or entitlement of any kind. + struct InvariantActors { + address registryAdmin; + address establishmentAuthority; + address beneficiaryA; + address beneficiaryB; + address ineligibleBeneficiary; + address authorizedExerciser; + address unauthorizedExerciser; + address eligibleTrader; + address ineligibleTrader; + address eligibleProvider; + address ineligibleProvider; + address donor; + address outsider; + } + + /// @notice The immutable facts one admission actually recorded. + /// @dev Remembered history, never prescribed state. It exists so that "the admitted facts never + /// changed" is checkable across bounded-reference reclamation and slot reuse. + /// @param serviceId The service the commitment was admitted under. + /// @param beneficiary The admitted Beneficiary. + /// @param exerciseAuthority The admitted exercise authority. + /// @param exercisableFrom The admitted exercise-window opening. + /// @param validUntil The admitted validity end. + /// @param originalEntitlement The admitted entitlement extent. + struct AdmittedFacts { + PoolId serviceId; + address beneficiary; + address exerciseAuthority; + uint64 exercisableFrom; + uint64 validUntil; + uint128 originalEntitlement; + } + + /// @notice Diagnostic activity counters for one campaign. + /// @dev Test diagnostics only. No counter is a protocol semantic and no threshold is a requirement; + /// they exist so a green campaign can be shown to have exercised meaningful protocol behavior + /// rather than trivial churn. + struct ActionCounters { + uint256 establishAttempts; + uint256 establishSuccesses; + uint256 establishRejections; + uint256 exerciseAttempts; + uint256 exerciseSuccesses; + uint256 exerciseRejections; + uint256 partialFulfillments; + uint256 fullFulfillments; + uint256 protectedSwapAttempts; + uint256 protectedSwapSuccesses; + uint256 swapBackingRejections; + uint256 oppositeSwapAttempts; + uint256 oppositeSwapSuccesses; + uint256 liquidityAddAttempts; + uint256 liquidityAddSuccesses; + uint256 liquidityRemoveAttempts; + uint256 liquidityRemoveSuccesses; + uint256 liquidityBackingRejections; + uint256 beneficiaryEligibilityMutations; + uint256 traderEligibilityMutations; + uint256 liquidityEligibilityMutations; + uint256 eligibilityMutationRejections; + uint256 timeAdvances; + uint256 expiryEvents; + uint256 directBeneficiaryTransfers; + uint256 orphanEvidenceAttempts; + uint256 referenceReuseEvents; + uint256 maxLiveReferences; + uint256 maxObservedObligation; + uint256 backingBoundaryObservations; + } + + /*////////////////////////////////////////////////////////////// + STATE VARIABLES + //////////////////////////////////////////////////////////////*/ + + /// @dev The candidate liquidity ranges a campaign may act on. + uint256 internal constant LIQUIDITY_RANGE_COUNT = 4; + + /// @dev How many of the most recent commitments a generated exercise prefers to target. + uint256 internal constant RECENT_COMMITMENT_WINDOW = 4; + + IPoolManager internal immutable i_poolManager; + StandbyHook internal immutable i_hook; + ExerciseRouter internal immutable i_exerciseRouter; + EligibilityRegistry internal immutable i_registry; + ActorAwareTestRouter internal immutable i_swapPerimeter; + ActorAwareTestRouter internal immutable i_liquidityPerimeter; + IInvariantCurrency internal immutable i_currency0; + IInvariantCurrency internal immutable i_currency1; + + bool internal immutable i_protectedZeroForOne; + int24 internal immutable i_tickQ; + int24 internal immutable i_tickO; + int24 internal immutable i_tickSpacing; + int24 internal immutable i_lpTickLower; + int24 internal immutable i_lpTickUpper; + uint256 internal immutable i_initialCapacity; + uint128 internal immutable i_initialLiquidity; + + address internal immutable i_registryAdmin; + address internal immutable i_establishmentAuthority; + address internal immutable i_beneficiaryA; + address internal immutable i_beneficiaryB; + address internal immutable i_ineligibleBeneficiary; + address internal immutable i_authorizedExerciser; + address internal immutable i_unauthorizedExerciser; + address internal immutable i_eligibleTrader; + address internal immutable i_ineligibleTrader; + address internal immutable i_eligibleProvider; + address internal immutable i_ineligibleProvider; + address internal immutable i_donor; + address internal immutable i_outsider; + + /// @dev The activated service pool this campaign drives. + PoolKey internal servicePoolKey; + + /// @dev The identity of the activated service pool. + PoolId internal servicePoolId; + + /// @notice Every commitment identity a successful production admission actually produced. + uint256[] public knownCommitmentIds; + + /// @dev The immutable facts each admission recorded, remembered at the moment it succeeded. + mapping(uint256 commitmentId => AdmittedFacts facts) internal admittedFacts; + + /// @dev The last Remaining Entitlement observed for a commitment, for monotonicity. + mapping(uint256 commitmentId => uint128 remaining) internal lastObservedRemaining; + + /// @dev Independently tracked successful attributable fulfillment, by commitment. + mapping(uint256 commitmentId => uint256 fulfilled) internal fulfilledByCommitment; + + /// @dev Protected output delivered to an account by successfully completed O2, independently tracked. + mapping(address beneficiary => uint256 delivered) internal deliveredToBeneficiary; + + /// @dev Protected output an unrelated direct transfer moved to an account, tracked separately. + mapping(address beneficiary => uint256 donated) internal donatedToBeneficiary; + + /// @dev Liquidity a given actor currently holds over a given range through the trusted perimeter. + mapping(bytes32 positionKey => uint128 liquidity) internal positionLiquidity; + + /// @dev The campaign's diagnostic activity counters. + ActionCounters internal actionCounters; + + /*////////////////////////////////////////////////////////////// + CONSTRUCTOR + //////////////////////////////////////////////////////////////*/ + + /// @notice Binds the handler to one activated production environment and its persistent actors. + /// @dev The bootstrap liquidity position is recorded as ghost custody bookkeeping only. It was created + /// before this contract existed, by the production `beforeAddLiquidity` path through the trusted + /// liquidity perimeter, and remembering who holds it lets removal requests be generated at + /// meaningful sizes rather than being rejected by position accounting every time. + /// @param _environment The activated production environment. + /// @param _actors The bounded persistent actor universe. + constructor(InvariantEnvironment memory _environment, InvariantActors memory _actors) { + i_poolManager = _environment.poolManager; + i_hook = _environment.hook; + i_exerciseRouter = _environment.exerciseRouter; + i_registry = _environment.registry; + i_swapPerimeter = _environment.swapPerimeter; + i_liquidityPerimeter = _environment.liquidityPerimeter; + i_currency0 = _environment.currency0; + i_currency1 = _environment.currency1; + + i_protectedZeroForOne = _environment.protectedZeroForOne; + i_tickQ = _environment.tickQ; + i_tickO = _environment.tickO; + i_tickSpacing = _environment.tickSpacing; + i_lpTickLower = _environment.lpTickLower; + i_lpTickUpper = _environment.lpTickUpper; + i_initialCapacity = _environment.initialCapacity; + i_initialLiquidity = _environment.initialLiquidity; + + i_registryAdmin = _actors.registryAdmin; + i_establishmentAuthority = _actors.establishmentAuthority; + i_beneficiaryA = _actors.beneficiaryA; + i_beneficiaryB = _actors.beneficiaryB; + i_ineligibleBeneficiary = _actors.ineligibleBeneficiary; + i_authorizedExerciser = _actors.authorizedExerciser; + i_unauthorizedExerciser = _actors.unauthorizedExerciser; + i_eligibleTrader = _actors.eligibleTrader; + i_ineligibleTrader = _actors.ineligibleTrader; + i_eligibleProvider = _actors.eligibleProvider; + i_ineligibleProvider = _actors.ineligibleProvider; + i_donor = _actors.donor; + i_outsider = _actors.outsider; + + servicePoolKey = _environment.poolKey; + servicePoolId = _environment.poolKey.toId(); + + positionLiquidity[_positionKey(_actors.eligibleProvider, _environment.lpTickLower, _environment.lpTickUpper)] = + _environment.initialLiquidity; + } + + /*////////////////////////////////////////////////////////////// + EXTERNAL FUNCTIONS — CAMPAIGN + //////////////////////////////////////////////////////////////*/ + + /// @notice Proposes one O1 commitment admission, valid or not. + /// @dev The caller, the proposed Beneficiary, the exercise authority, the extent, and the window are + /// all generated: unauthorized callers, a permanently ineligible Beneficiary, a zero extent, an + /// extent no backing could cover, an already-ended validity, and an impossible window are all + /// reachable and all must be refused by production rather than by this generator. + /// @param _seed The action-shaping seed. + /// @param _entitlement The proposed entitlement extent, bounded to the campaign's economic scale. + /// @param _fromDelay The proposed exercise-window delay. + /// @param _duration The proposed validity duration. + function establishCommitment(uint256 _seed, uint128 _entitlement, uint64 _fromDelay, uint64 _duration) external { + address caller = _seed % 8 == 0 ? _anyActor(_seed >> 3) : i_establishmentAuthority; + address beneficiary = _proposedBeneficiary(_seed >> 8); + address authority = (_seed >> 16) % 8 == 0 ? i_outsider : i_authorizedExerciser; + + uint128 entitlement = uint128(bound(uint256(_entitlement), 0, _economicScale())); + uint64 exercisableFrom = + uint64(block.timestamp) + ((_seed >> 24) % 4 == 0 ? uint64(bound(uint256(_fromDelay), 0, 3 days)) : 0); + uint64 validUntil = uint64(block.timestamp) + uint64(bound(uint256(_duration), 0, 45 days)); + + scriptedEstablish(caller, beneficiary, authority, entitlement, exercisableFrom, validUntil); + } + + /// @notice Requests one O2 exercise of a known commitment, valid or not. + /// @dev Quantity generation spans the whole admissible boundary and past it: exact exhaustion, a + /// partial amount, zero, and more than the commitment still carries. The caller is the commitment's + /// exercise authority most of the time and an unauthorized account otherwise, and the cost bound is + /// occasionally too small for any real debt. + /// @param _seed The action-shaping seed. + /// @param _q The requested protected-output quantity, bounded against authoritative Remaining. + /// @param _maxInput The exerciser's own cost bound. + function exercise(uint256 _seed, uint256 _q, uint256 _maxInput) external { + if (knownCommitmentIds.length == 0) return; + + uint256 commitmentId = _knownCommitment(_seed); + address exerciser = _exerciseCaller(_seed >> 8); + + uint256 remaining = uint256(i_hook.commitment(commitmentId).remainingEntitlement); + + uint256 pick = (_seed >> 16) % 8; + uint256 q; + + if (pick < 3) q = remaining; + else if (pick < 7) q = bound(_q, 0, remaining); + else q = bound(_q, remaining, remaining + 1 + remaining / 4); + + uint256 maxInput = (_seed >> 24) % 8 == 0 ? bound(_maxInput, 0, 1e6) : type(uint256).max; + + scriptedExercise(exerciser, commitmentId, q, maxInput); + } + + /// @notice Requests one ordinary swap in the protected direction, valid or not. + /// @param _seed The action-shaping seed. + /// @param _amount The requested amount, bounded to the campaign's economic scale. + function ordinaryProtectedSwap(uint256 _seed, uint256 _amount) external { + _ordinarySwap(_seed, _amount, true); + } + + /// @notice Requests one ordinary swap in the opposite direction, valid or not. + /// @param _seed The action-shaping seed. + /// @param _amount The requested amount, bounded to the campaign's economic scale. + function ordinaryOppositeSwap(uint256 _seed, uint256 _amount) external { + _ordinarySwap(_seed, _amount, false); + } + + /// @notice Requests one liquidity addition, valid or not. + /// @dev Reaches an ineligible provider, an untrusted perimeter, and a range whose endpoint would sit + /// strictly inside the configured service domain — each of which production must refuse. + /// @param _seed The action-shaping seed. + /// @param _liquidity The proposed liquidity, bounded to the bootstrap position's scale. + function addLiquidity(uint256 _seed, uint128 _liquidity) external { + (int24 tickLower, int24 tickUpper) = _candidateRange(_seed >> 8); + + scriptedModifyLiquidity( + _liquidityActor(_seed), + tickLower, + tickUpper, + int256(uint256(uint128(bound(uint256(_liquidity), 0, uint256(i_initialLiquidity))))), + (_seed >> 16) % 8 == 0 + ); + } + + /// @notice Requests one liquidity removal, valid or not. + /// @dev Removal sizes are generated slightly beyond what the actor actually holds, so both an + /// authoritative position-accounting refusal and a Standby backing refusal are reachable. + /// @param _seed The action-shaping seed. + /// @param _liquidity The proposed removal, bounded against the actor's own tracked position. + function removeLiquidity(uint256 _seed, uint128 _liquidity) external { + address actor = _liquidityActor(_seed); + + (int24 tickLower, int24 tickUpper) = _candidateRange(_seed >> 8); + + uint256 held = uint256(positionLiquidity[_positionKey(actor, tickLower, tickUpper)]); + uint256 removal = bound(uint256(_liquidity), 0, held + held / 4 + 1); + + scriptedModifyLiquidity(actor, tickLower, tickUpper, -int256(removal), (_seed >> 16) % 8 == 0); + } + + /// @notice Advances authoritative time, occasionally past the campaign's whole validity horizon. + /// @param _seed The action-shaping seed. + function advanceTime(uint256 _seed) external { + scriptedAdvanceTime(_seed % 8 == 0 ? 31 days : bound(_seed, 1 hours, 2 days)); + } + + /// @notice Mutates Beneficiary eligibility, from the registry administrator or from an outsider. + /// @dev The permanently ineligible Beneficiary is never a candidate, so "ineligible" remains a stable + /// relationship across the whole generated history. + /// @param _seed The action-shaping seed. + function setBeneficiaryEligibility(uint256 _seed) external { + scriptedSetBeneficiaryEligibility( + _eligibilityCaller(_seed), _mutableBeneficiary(_seed >> 8), _grantsEligibility(_seed >> 16) + ); + } + + /// @notice Mutates trader eligibility, from the registry administrator or from an outsider. + /// @param _seed The action-shaping seed. + function setTraderEligibility(uint256 _seed) external { + scriptedSetTraderEligibility( + _eligibilityCaller(_seed), + (_seed >> 8) % 2 == 0 ? i_eligibleTrader : i_outsider, + _grantsEligibility(_seed >> 16) + ); + } + + /// @notice Mutates liquidity-action eligibility, from the registry administrator or from an outsider. + /// @param _seed The action-shaping seed. + function setLiquidityEligibility(uint256 _seed) external { + scriptedSetLiquidityEligibility( + _eligibilityCaller(_seed), + (_seed >> 8) % 2 == 0 ? i_eligibleProvider : i_outsider, + _grantsEligibility(_seed >> 16) + ); + } + + /// @notice Transfers protected output currency directly to a Beneficiary, outside Standby entirely. + /// @dev Ordinary receipt of the protected output currency is not Standby fulfillment, and this action + /// exists to keep that claim behavioral rather than asserted. + /// @param _seed The action-shaping seed. + /// @param _amount The raw amount transferred. + function directTransferProtectedTokenToBeneficiary(uint256 _seed, uint256 _amount) external { + scriptedDirectTransfer(_mutableBeneficiary(_seed), bound(_amount, 0, _economicScale() / 4 + 1)); + } + + /// @notice Attempts to use O2 evidence that no exercise in this transaction produced. + /// @dev Two probes of the same frozen property. A direct `authorizeExercise` never arrives through the + /// configured ExerciseRouter, and a direct `finalizeExercise` has no causally proven exercise + /// behind it — including immediately after a successful one, which is the shape a surviving, + /// reusable context would take. + /// @param _seed The action-shaping seed. + function attemptOrphanExerciseEvidence(uint256 _seed) external { + uint256 commitmentId = (_seed % 4 == 0 || knownCommitmentIds.length == 0) + ? i_hook.nextCommitmentId() + : _knownCommitment(_seed >> 8); + + scriptedOrphanEvidence(_anyActor(_seed >> 16), commitmentId); + } + + /*////////////////////////////////////////////////////////////// + EXTERNAL FUNCTIONS — OBSERVATION + //////////////////////////////////////////////////////////////*/ + + /// @notice Returns the campaign's diagnostic activity counters. + /// @return counters_ The counters accumulated by this campaign. + function counters() external view returns (ActionCounters memory counters_) { + counters_ = actionCounters; + } + + /// @notice Returns how many commitments successful production admissions have produced. + /// @return count The number of known commitment identities. + function commitmentCount() external view returns (uint256 count) { + count = knownCommitmentIds.length; + } + + /// @notice Returns the immutable facts remembered for one admitted commitment. + /// @param _commitmentId The identity to read. + /// @return facts The facts the admission actually recorded. + function admittedCommitmentFacts(uint256 _commitmentId) external view returns (AdmittedFacts memory facts) { + facts = admittedFacts[_commitmentId]; + } + + /// @notice Returns the independently tracked successful fulfillment of one commitment. + /// @param _commitmentId The identity to read. + /// @return fulfilled The sum of the quantities successfully completed O2 exercises discharged. + function ghostFulfilled(uint256 _commitmentId) external view returns (uint256 fulfilled) { + fulfilled = fulfilledByCommitment[_commitmentId]; + } + + /// @notice Returns the protected output successfully completed O2 delivered to an account. + /// @param _beneficiary The account to read. + /// @return delivered The independently tracked delivered quantity. + function ghostDelivered(address _beneficiary) external view returns (uint256 delivered) { + delivered = deliveredToBeneficiary[_beneficiary]; + } + + /// @notice Returns the protected output unrelated direct transfers moved to an account. + /// @param _beneficiary The account to read. + /// @return donated The independently tracked donated quantity. + function ghostDonated(address _beneficiary) external view returns (uint256 donated) { + donated = donatedToBeneficiary[_beneficiary]; + } + + /// @notice Returns the last Remaining Entitlement this handler observed for a commitment. + /// @param _commitmentId The identity to read. + /// @return remaining The last observed remainder. + function ghostLastRemaining(uint256 _commitmentId) external view returns (uint128 remaining) { + remaining = lastObservedRemaining[_commitmentId]; + } + + /*////////////////////////////////////////////////////////////// + PUBLIC FUNCTIONS — SCRIPTED + //////////////////////////////////////////////////////////////*/ + + /// @notice Runs one production O1 admission with every term chosen explicitly. + /// @dev The single implementation of the action. The campaign entry point generates its arguments and + /// the scripted sequence suites choose them, so both prove properties of the same transition. + /// @param _caller The account attempting the admission. + /// @param _beneficiary The proposed Beneficiary. + /// @param _exerciseAuthority The proposed exercise authority. + /// @param _originalEntitlement The proposed entitlement extent. + /// @param _exercisableFrom The proposed exercise-window opening. + /// @param _validUntil The proposed validity end. + /// @return admitted Whether production admitted the commitment. + /// @return commitmentId The identity allocated when admitted, otherwise zero. + function scriptedEstablish( + address _caller, + address _beneficiary, + address _exerciseAuthority, + uint128 _originalEntitlement, + uint64 _exercisableFrom, + uint64 _validUntil + ) public returns (bool admitted, uint256 commitmentId) { + uint256[MAX_LIVE_COMMITMENTS] memory referencesBefore = i_hook.enforcementReferences(); + uint256 nextIdBefore = i_hook.nextCommitmentId(); + + ++actionCounters.establishAttempts; + + vm.prank(_caller); + try i_hook.establishCommitment( + _beneficiary, _exerciseAuthority, _originalEntitlement, _exercisableFrom, _validUntil + ) returns (uint256 admittedId) { + ++actionCounters.establishSuccesses; + + (admitted, commitmentId) = (true, admittedId); + + _recordAdmission(admittedId, referencesBefore); + } catch { + ++actionCounters.establishRejections; + + assertEq(i_hook.nextCommitmentId(), nextIdBefore, "a refused O1 must consume no commitment identity"); + + _assertReferencesUnchanged(referencesBefore, "a refused O1 must not touch the bounded reference index"); + } + + _observeAuthoritativeState(); + } + + /// @notice Runs one production O2 exercise request with every field chosen explicitly. + /// @dev The exactness claims are made here because they are transition-local: a successful exercise + /// must reduce exactly one commitment by exactly the exercised quantity and deliver exactly that + /// quantity to the authoritative Beneficiary, and a refused one must do neither. + /// @param _exerciser The account requesting the exercise. + /// @param _commitmentId The commitment the request names. + /// @param _q The requested protected-output quantity. + /// @param _maxInput The exerciser's own cost bound. + /// @return fulfilled Whether the exercise completed and fulfilled the commitment. + function scriptedExercise(address _exerciser, uint256 _commitmentId, uint256 _q, uint256 _maxInput) + public + returns (bool fulfilled) + { + address beneficiary = i_hook.commitment(_commitmentId).beneficiary; + + uint256[] memory remainingBefore = _remainingSnapshot(); + uint256 beneficiaryBefore = _protectedOutputBalance(beneficiary); + uint256 obligationBefore = i_hook.aggregateObligation(); + uint256 capacityBefore = _referenceCapacity(); + + ++actionCounters.exerciseAttempts; + + vm.prank(_exerciser); + try i_exerciseRouter.exercise(_commitmentId, _q, _maxInput) { + ++actionCounters.exerciseSuccesses; + + fulfilled = true; + + fulfilledByCommitment[_commitmentId] += _q; + deliveredToBeneficiary[beneficiary] += _q; + + _assertExactFulfillment(_commitmentId, beneficiary, _q, remainingBefore, beneficiaryBefore); + + if (i_hook.commitment(_commitmentId).remainingEntitlement == 0) ++actionCounters.fullFulfillments; + else ++actionCounters.partialFulfillments; + } catch { + ++actionCounters.exerciseRejections; + + _assertNoFulfillmentOccurred(remainingBefore, "a refused O2 must fulfil nothing"); + + assertEq( + _protectedOutputBalance(beneficiary), beneficiaryBefore, "a refused O2 must deliver nothing at all" + ); + assertEq(i_hook.aggregateObligation(), obligationBefore, "a refused O2 must release no obligation"); + assertEq(_referenceCapacity(), capacityBefore, "a refused O2 must leave the authoritative pool untouched"); + } + + _observeAuthoritativeState(); + } + + /// @notice Runs one ordinary swap with its actor, shape, and perimeter chosen explicitly. + /// @param _actor The originating user the perimeter authenticates. + /// @param _zeroForOne The proposed swap direction. + /// @param _amountSpecified The proposed amount, negative for exact input and positive for exact output. + /// @param _limitTick The tick whose exact price bounds the swap. + /// @param _throughLiquidityPerimeter Whether to route through the liquidity perimeter instead. + /// @return executed Whether the swap became an authoritative pool transition. + function scriptedSwap( + address _actor, + bool _zeroForOne, + int256 _amountSpecified, + int24 _limitTick, + bool _throughLiquidityPerimeter + ) public returns (bool executed) { + ActorAwareTestRouter perimeter = _throughLiquidityPerimeter ? i_liquidityPerimeter : i_swapPerimeter; + + SwapParams memory params = SwapParams({ + zeroForOne: _zeroForOne, + amountSpecified: _amountSpecified, + sqrtPriceLimitX96: TickMath.getSqrtPriceAtTick(_limitTick) + }); + + bool protectedDirection = _zeroForOne == i_protectedZeroForOne; + + if (protectedDirection) ++actionCounters.protectedSwapAttempts; + else ++actionCounters.oppositeSwapAttempts; + + uint256[] memory remainingBefore = _remainingSnapshot(); + + vm.prank(_actor); + try perimeter.swap(servicePoolKey, params, bytes("")) { + executed = true; + + if (protectedDirection) ++actionCounters.protectedSwapSuccesses; + else ++actionCounters.oppositeSwapSuccesses; + } catch (bytes memory reason) { + if (_reportsInsufficientProspectiveBacking(reason)) ++actionCounters.swapBackingRejections; + } + + _assertNoFulfillmentOccurred(remainingBefore, "an ordinary swap must never fulfil a commitment"); + + _observeAuthoritativeState(); + } + + /// @notice Runs one liquidity modification with its actor, range, and perimeter chosen explicitly. + /// @param _actor The originating user the perimeter authenticates. + /// @param _tickLower The lower endpoint of the range. + /// @param _tickUpper The upper endpoint of the range. + /// @param _liquidityDelta The proposed liquidity change. + /// @param _throughSwapPerimeter Whether to route through the ordinary-swap perimeter instead. + /// @return executed Whether the modification became an authoritative pool transition. + function scriptedModifyLiquidity( + address _actor, + int24 _tickLower, + int24 _tickUpper, + int256 _liquidityDelta, + bool _throughSwapPerimeter + ) public returns (bool executed) { + ActorAwareTestRouter perimeter = _throughSwapPerimeter ? i_swapPerimeter : i_liquidityPerimeter; + + ModifyLiquidityParams memory params = ModifyLiquidityParams({ + tickLower: _tickLower, + tickUpper: _tickUpper, + liquidityDelta: _liquidityDelta, + salt: bytes32(0) + }); + + if (_liquidityDelta > 0) ++actionCounters.liquidityAddAttempts; + else ++actionCounters.liquidityRemoveAttempts; + + uint256[] memory remainingBefore = _remainingSnapshot(); + + vm.prank(_actor); + try perimeter.modifyLiquidity(servicePoolKey, params, bytes("")) { + executed = true; + + _recordPositionChange(_actor, _tickLower, _tickUpper, _liquidityDelta); + + if (_liquidityDelta > 0) ++actionCounters.liquidityAddSuccesses; + else ++actionCounters.liquidityRemoveSuccesses; + } catch (bytes memory reason) { + if (_reportsInsufficientProspectiveBacking(reason)) ++actionCounters.liquidityBackingRejections; + } + + _assertNoFulfillmentOccurred(remainingBefore, "a liquidity action must never fulfil a commitment"); + + _observeAuthoritativeState(); + } + + /// @notice Advances authoritative time by an explicit amount. + /// @param _seconds The number of seconds to advance. + function scriptedAdvanceTime(uint256 _seconds) public { + uint256[] memory remainingBefore = _remainingSnapshot(); + uint256 bindingBefore = _bindingCommitmentCount(); + + vm.warp(block.timestamp + _seconds); + + ++actionCounters.timeAdvances; + + uint256 bindingAfter = _bindingCommitmentCount(); + + if (bindingAfter < bindingBefore) actionCounters.expiryEvents += bindingBefore - bindingAfter; + + _assertNoFulfillmentOccurred(remainingBefore, "expiry must never fulfil a commitment"); + + _observeAuthoritativeState(); + } + + /// @notice Mutates Beneficiary eligibility with its caller and target chosen explicitly. + /// @param _caller The account attempting the mutation. + /// @param _account The account whose eligibility is mutated. + /// @param _eligible The eligibility to set. + /// @return mutated Whether the registry accepted the mutation. + function scriptedSetBeneficiaryEligibility(address _caller, address _account, bool _eligible) + public + returns (bool mutated) + { + uint256 obligationBefore = i_hook.aggregateObligation(); + uint256[] memory remainingBefore = _remainingSnapshot(); + + vm.prank(_caller); + try i_registry.setBeneficiaryEligibility(_account, _eligible) { + mutated = true; + + ++actionCounters.beneficiaryEligibilityMutations; + } catch { + ++actionCounters.eligibilityMutationRejections; + } + + assertEq( + i_hook.aggregateObligation(), + obligationBefore, + "Beneficiary eligibility must release no Capacity Obligation" + ); + + _assertNoFulfillmentOccurred(remainingBefore, "eligibility mutation must never fulfil a commitment"); + + _observeAuthoritativeState(); + } + + /// @notice Mutates trader eligibility with its caller and target chosen explicitly. + /// @param _caller The account attempting the mutation. + /// @param _account The account whose eligibility is mutated. + /// @param _eligible The eligibility to set. + /// @return mutated Whether the registry accepted the mutation. + function scriptedSetTraderEligibility(address _caller, address _account, bool _eligible) + public + returns (bool mutated) + { + uint256 obligationBefore = i_hook.aggregateObligation(); + uint256[] memory remainingBefore = _remainingSnapshot(); + + vm.prank(_caller); + try i_registry.setTraderEligibility(_account, _eligible) { + mutated = true; + + ++actionCounters.traderEligibilityMutations; + } catch { + ++actionCounters.eligibilityMutationRejections; + } + + assertEq(i_hook.aggregateObligation(), obligationBefore, "trader eligibility must release no obligation"); + + _assertNoFulfillmentOccurred(remainingBefore, "trader eligibility must never fulfil a commitment"); + + _observeAuthoritativeState(); + } + + /// @notice Mutates liquidity-action eligibility with its caller and target chosen explicitly. + /// @param _caller The account attempting the mutation. + /// @param _account The account whose eligibility is mutated. + /// @param _eligible The eligibility to set. + /// @return mutated Whether the registry accepted the mutation. + function scriptedSetLiquidityEligibility(address _caller, address _account, bool _eligible) + public + returns (bool mutated) + { + uint256 obligationBefore = i_hook.aggregateObligation(); + uint256[] memory remainingBefore = _remainingSnapshot(); + + vm.prank(_caller); + try i_registry.setLiquidityEligibility(_account, _eligible) { + mutated = true; + + ++actionCounters.liquidityEligibilityMutations; + } catch { + ++actionCounters.eligibilityMutationRejections; + } + + assertEq(i_hook.aggregateObligation(), obligationBefore, "liquidity eligibility must release no obligation"); + + _assertNoFulfillmentOccurred(remainingBefore, "liquidity eligibility must never fulfil a commitment"); + + _observeAuthoritativeState(); + } + + /// @notice Transfers protected output currency directly to an account, outside Standby. + /// @param _beneficiary The recipient. + /// @param _amount The raw amount transferred. + /// @return transferred Whether the transfer succeeded. + function scriptedDirectTransfer(address _beneficiary, uint256 _amount) public returns (bool transferred) { + uint256[] memory remainingBefore = _remainingSnapshot(); + uint256 balanceBefore = _protectedOutputBalance(_beneficiary); + + vm.prank(i_donor); + try _protectedOutputCurrency().transfer(_beneficiary, _amount) { + transferred = true; + + donatedToBeneficiary[_beneficiary] += _amount; + + ++actionCounters.directBeneficiaryTransfers; + + assertEq( + _protectedOutputBalance(_beneficiary), + balanceBefore + _amount, + "an unrelated transfer must move exactly what it transferred" + ); + } catch {} + + _assertNoFulfillmentOccurred( + remainingBefore, "Beneficiary receipt of protected output must never be Standby fulfillment" + ); + + _observeAuthoritativeState(); + } + + /// @notice Attempts to consume O2 evidence this transaction did not produce. + /// @dev Both probes must be refused. The state assertions afterwards are what make "refused" mean "left + /// nothing behind" rather than merely "reverted". + /// @param _caller The account attempting to use the evidence. + /// @param _commitmentId The commitment the attempts name. + function scriptedOrphanEvidence(address _caller, uint256 _commitmentId) public { + uint256[] memory remainingBefore = _remainingSnapshot(); + + ++actionCounters.orphanEvidenceAttempts; + + vm.prank(_caller); + try i_hook.authorizeExercise(_commitmentId, 1) { + assertTrue(false, "authorization outside the configured ExerciseRouter must never succeed"); + } catch {} + + vm.prank(_caller); + try i_hook.finalizeExercise(_commitmentId) { + assertTrue(false, "finalization without a causally proven exercise must never succeed"); + } catch {} + + _assertNoFulfillmentOccurred(remainingBefore, "orphan O2 evidence must never fulfil a commitment"); + + _observeAuthoritativeState(); + } + + /*////////////////////////////////////////////////////////////// + INTERNAL FUNCTIONS + //////////////////////////////////////////////////////////////*/ + + /// @dev Generates one ordinary swap request in the requested direction relative to the protected one. + /// + /// The amount and the price limit are generated by their own helpers rather than inline, so that + /// this frame stays small enough to compile without the optimizer — which is what the repository's + /// coverage instrumentation builds with. + function _ordinarySwap(uint256 _seed, uint256 _amount, bool _protectedDirection) internal { + bool zeroForOne = _protectedDirection == i_protectedZeroForOne; + + scriptedSwap( + _swapActor(_seed), + zeroForOne, + _generatedSwapAmount(_seed, _amount), + _generatedSwapLimitTick(_seed, zeroForOne, _protectedDirection), + (_seed >> 8) % 8 == 0 + ); + } + + /// @dev The amount one generated ordinary swap requests, as exact input or exact output. + function _generatedSwapAmount(uint256 _seed, uint256 _amount) internal view returns (int256 amountSpecified) { + uint256 magnitude = bound(_amount, 0, _economicScale()); + + amountSpecified = (_seed >> 16) % 2 == 0 ? int256(magnitude) : -int256(magnitude); + } + + /// @dev The price limit one generated ordinary swap is bounded by. + /// + /// The domain boundary the swap moves toward most of the time, and a tick beyond that boundary + /// otherwise: the first is the ordinary supported shape, the second is a transition that would take + /// the pool out of the configured realization domain and must be refused as one. + function _generatedSwapLimitTick(uint256 _seed, bool _zeroForOne, bool _protectedDirection) + internal + view + returns (int24 limitTick) + { + if ((_seed >> 24) % 8 == 0) return _zeroForOne ? i_lpTickLower : i_lpTickUpper; + + limitTick = _protectedDirection ? i_tickQ : i_tickO; + } + + /// @dev Remembers the immutable facts one successful admission recorded, and any slot reuse it caused. + function _recordAdmission(uint256 _commitmentId, uint256[MAX_LIVE_COMMITMENTS] memory _referencesBefore) internal { + StandbyHook.Commitment memory record = i_hook.commitment(_commitmentId); + + admittedFacts[_commitmentId] = AdmittedFacts({ + serviceId: record.serviceId, + beneficiary: record.beneficiary, + exerciseAuthority: record.exerciseAuthority, + exercisableFrom: record.exercisableFrom, + validUntil: record.validUntil, + originalEntitlement: record.originalEntitlement + }); + + lastObservedRemaining[_commitmentId] = record.remainingEntitlement; + + knownCommitmentIds.push(_commitmentId); + + uint256[MAX_LIVE_COMMITMENTS] memory referencesAfter = i_hook.enforcementReferences(); + + for (uint256 slot = 0; slot < MAX_LIVE_COMMITMENTS; ++slot) { + if (referencesAfter[slot] != _commitmentId) continue; + + if (_referencesBefore[slot] != 0) ++actionCounters.referenceReuseEvents; + + return; + } + + assertTrue(false, "an admitted commitment must occupy a bounded enforcement reference"); + } + + /// @dev Records the position custody a successful liquidity modification produced. + function _recordPositionChange(address _actor, int24 _tickLower, int24 _tickUpper, int256 _liquidityDelta) + internal + { + bytes32 key = _positionKey(_actor, _tickLower, _tickUpper); + + if (_liquidityDelta > 0) { + positionLiquidity[key] += uint128(uint256(_liquidityDelta)); + + return; + } + + uint128 removed = uint128(uint256(-_liquidityDelta)); + uint128 held = positionLiquidity[key]; + + positionLiquidity[key] = held > removed ? held - removed : 0; + } + + /// @dev Re-observes every authoritative fact a completed action must have preserved. + /// + /// This is the continuous half of the transition-local evidence: whatever the action was, the + /// admitted facts of every historical commitment are still what admission recorded, no remainder + /// has grown, no remainder exceeds its admitted extent, the discharged portion of every commitment + /// still equals exactly the independently tracked successful fulfillment, every Beneficiary holds + /// exactly what Standby delivered plus what unrelated transfers donated, the protocol holds no + /// protected-output custody, and no reusable O2 causal evidence survives. + function _observeAuthoritativeState() internal { + uint256 count = knownCommitmentIds.length; + + for (uint256 i = 0; i < count; ++i) { + uint256 commitmentId = knownCommitmentIds[i]; + + StandbyHook.Commitment memory record = i_hook.commitment(commitmentId); + AdmittedFacts memory facts = admittedFacts[commitmentId]; + + assertEq( + PoolId.unwrap(record.serviceId), PoolId.unwrap(facts.serviceId), "the admitted service must not change" + ); + assertEq(record.beneficiary, facts.beneficiary, "the admitted Beneficiary must not change"); + assertEq( + record.exerciseAuthority, facts.exerciseAuthority, "the admitted exercise authority must not change" + ); + assertEq( + uint256(record.exercisableFrom), + uint256(facts.exercisableFrom), + "the admitted exercise window must not change" + ); + assertEq(uint256(record.validUntil), uint256(facts.validUntil), "the admitted validity must not change"); + assertEq( + uint256(record.originalEntitlement), + uint256(facts.originalEntitlement), + "the admitted entitlement extent must never be rewritten" + ); + + assertLe( + uint256(record.remainingEntitlement), + uint256(facts.originalEntitlement), + "Remaining Entitlement must never exceed the admitted extent" + ); + assertLe( + uint256(record.remainingEntitlement), + uint256(lastObservedRemaining[commitmentId]), + "Remaining Entitlement must never increase" + ); + assertEq( + uint256(facts.originalEntitlement) - uint256(record.remainingEntitlement), + fulfilledByCommitment[commitmentId], + "the discharged portion must equal independently tracked successful fulfillment" + ); + + lastObservedRemaining[commitmentId] = record.remainingEntitlement; + } + + _assertBeneficiaryHoldings(i_beneficiaryA); + _assertBeneficiaryHoldings(i_beneficiaryB); + _assertBeneficiaryHoldings(i_ineligibleBeneficiary); + + _assertNoProtocolCustody(); + + assertEq( + uint256(i_hook.exerciseAuthorization().state), + uint256(StandbyHook.ExerciseAuthorizationState.EMPTY), + "no reusable O2 causal context may survive a completed action" + ); + + _updateDiagnostics(); + } + + /// @dev Proves one successfully completed O2 had exactly the consequence it must have. + function _assertExactFulfillment( + uint256 _commitmentId, + address _beneficiary, + uint256 _q, + uint256[] memory _remainingBefore, + uint256 _beneficiaryBefore + ) internal view { + uint256 count = knownCommitmentIds.length; + + for (uint256 i = 0; i < count; ++i) { + uint256 commitmentId = knownCommitmentIds[i]; + uint256 remaining = uint256(i_hook.commitment(commitmentId).remainingEntitlement); + + if (commitmentId == _commitmentId) { + assertEq( + remaining, + _remainingBefore[i] - _q, + "a successful O2 must reduce its own commitment by exactly the exercised quantity" + ); + } else { + assertEq(remaining, _remainingBefore[i], "a successful O2 must reduce no other commitment"); + } + } + + assertEq( + _protectedOutputBalance(_beneficiary), + _beneficiaryBefore + _q, + "a successful O2 must deliver exactly the exercised quantity to the authoritative Beneficiary" + ); + } + + /// @dev Proves no commitment's Remaining Entitlement moved across an action. + function _assertNoFulfillmentOccurred(uint256[] memory _remainingBefore, string memory _context) internal view { + uint256 count = knownCommitmentIds.length; + + for (uint256 i = 0; i < count; ++i) { + assertEq( + uint256(i_hook.commitment(knownCommitmentIds[i]).remainingEntitlement), _remainingBefore[i], _context + ); + } + } + + /// @dev Proves the bounded enforcement-reference index is exactly what it was. + function _assertReferencesUnchanged(uint256[MAX_LIVE_COMMITMENTS] memory _referencesBefore, string memory _context) + internal + view + { + uint256[MAX_LIVE_COMMITMENTS] memory current = i_hook.enforcementReferences(); + + for (uint256 slot = 0; slot < MAX_LIVE_COMMITMENTS; ++slot) { + assertEq(current[slot], _referencesBefore[slot], _context); + } + } + + /// @dev Proves an account holds exactly the Standby deliveries plus the unrelated donations it received. + /// + /// Beneficiaries hold no protected output at campaign start, never trade, never provide liquidity, + /// and never exercise, so their balance is a complete independent history of what reached them. + function _assertBeneficiaryHoldings(address _beneficiary) internal view { + assertEq( + _protectedOutputBalance(_beneficiary), + deliveredToBeneficiary[_beneficiary] + donatedToBeneficiary[_beneficiary], + "a Beneficiary must hold exactly what Standby delivered plus what unrelated transfers donated" + ); + } + + /// @dev Proves neither the Hook nor the ExerciseRouter holds currency of either kind. + function _assertNoProtocolCustody() internal view { + assertEq(i_currency0.balanceOf(address(i_hook)), 0, "the Hook must hold no currency0 custody"); + assertEq(i_currency1.balanceOf(address(i_hook)), 0, "the Hook must hold no currency1 custody"); + assertEq( + i_currency0.balanceOf(address(i_exerciseRouter)), 0, "the ExerciseRouter must hold no currency0 custody" + ); + assertEq( + i_currency1.balanceOf(address(i_exerciseRouter)), 0, "the ExerciseRouter must hold no currency1 custody" + ); + } + + /// @dev Updates the campaign quality diagnostics that describe the reachable states actually visited. + function _updateDiagnostics() internal { + uint256 live; + + uint256[MAX_LIVE_COMMITMENTS] memory references = i_hook.enforcementReferences(); + + for (uint256 slot = 0; slot < MAX_LIVE_COMMITMENTS; ++slot) { + if (references[slot] != 0) ++live; + } + + if (live > actionCounters.maxLiveReferences) actionCounters.maxLiveReferences = live; + + uint256 obligation = i_hook.aggregateObligation(); + + if (obligation > actionCounters.maxObservedObligation) actionCounters.maxObservedObligation = obligation; + + if (obligation != 0 && _referenceCapacity() == obligation) ++actionCounters.backingBoundaryObservations; + } + + /// @dev Captures the Remaining Entitlement of every known commitment, positionally. + function _remainingSnapshot() internal view returns (uint256[] memory remaining) { + uint256 count = knownCommitmentIds.length; + + remaining = new uint256[](count); + + for (uint256 i = 0; i < count; ++i) { + remaining[i] = uint256(i_hook.commitment(knownCommitmentIds[i]).remainingEntitlement); + } + } + + /// @dev Counts the commitments that currently carry a positive Capacity Obligation, from facts alone. + function _bindingCommitmentCount() internal view returns (uint256 binding) { + uint256 count = knownCommitmentIds.length; + + for (uint256 i = 0; i < count; ++i) { + StandbyHook.Commitment memory record = i_hook.commitment(knownCommitmentIds[i]); + + if ( + ReferenceCalculations.referenceCommitmentObligation( + record.remainingEntitlement, record.validUntil, block.timestamp + ) != 0 + ) ++binding; + } + } + + /// @dev Independently derives Supporting Capacity from authoritative PoolManager state. + function _referenceCapacity() internal view returns (uint256 capacity) { + (uint160 sqrtPriceX96,,,) = i_poolManager.getSlot0(servicePoolId); + + capacity = ReferenceCalculations.referenceSupportingCapacity( + i_protectedZeroForOne, sqrtPriceX96, i_tickQ, i_poolManager.getLiquidity(servicePoolId) + ); + } + + /// @dev Independently derives the current Aggregate Capacity Obligation from commitment facts. + /// + /// Used only to shape generated amounts. Nothing decided by this value is a safety judgement: it + /// chooses the magnitude a proposal is drawn at, and production alone decides whether the proposal + /// is admissible. + function _referenceObligation() internal view returns (uint256 obligation) { + uint256 count = knownCommitmentIds.length; + + for (uint256 i = 0; i < count; ++i) { + StandbyHook.Commitment memory record = i_hook.commitment(knownCommitmentIds[i]); + + obligation += ReferenceCalculations.referenceCommitmentObligation( + record.remainingEntitlement, record.validUntil, block.timestamp + ); + } + } + + /// @dev The economic scale generated amounts are drawn against. + /// + /// Centred on the present backing headroom, independently derived, plus a margin. That is where + /// the interesting boundary is: an amount drawn from this range is frequently one the service can + /// still support and frequently one it cannot, so admission and refusal are both ordinary + /// outcomes rather than one being an accident. The margin keeps the range positive when the + /// service is fully committed, so backing-destructive proposals stay reachable there too. + function _economicScale() internal view returns (uint256 scale) { + uint256 capacity = _referenceCapacity(); + uint256 obligation = _referenceObligation(); + + scale = (capacity > obligation ? capacity - obligation : 0) + i_initialCapacity / 8 + 1; + } + + /// @dev The protected output currency, selected by the protected direction alone. + function _protectedOutputCurrency() internal view returns (IInvariantCurrency currency) { + currency = i_protectedZeroForOne ? i_currency1 : i_currency0; + } + + /// @dev Reads an account's protected-output balance. + function _protectedOutputBalance(address _account) internal view returns (uint256 balance) { + balance = _protectedOutputCurrency().balanceOf(_account); + } + + /// @dev Selects a known commitment identity. + /// + /// Recent identities are preferred, because a history that only ever targeted the oldest + /// commitment would spend most of its exercise attempts on expired or exhausted ones and would + /// reach very little completed fulfillment. Every identity stays reachable, so a stale target is + /// still generated. + function _knownCommitment(uint256 _seed) internal view returns (uint256 commitmentId) { + uint256 count = knownCommitmentIds.length; + + if (_seed % 4 == 0 || count <= RECENT_COMMITMENT_WINDOW) { + return knownCommitmentIds[(_seed >> 2) % count]; + } + + commitmentId = knownCommitmentIds[count - 1 - ((_seed >> 2) % RECENT_COMMITMENT_WINDOW)]; + } + + /// @dev Selects the account a generated ordinary swap originates from. + function _swapActor(uint256 _seed) internal view returns (address actor) { + uint256 pick = _seed % 8; + + if (pick < 5) actor = i_eligibleTrader; + else if (pick < 7) actor = i_ineligibleTrader; + else actor = i_outsider; + } + + /// @dev Selects the account a generated liquidity action originates from. + function _liquidityActor(uint256 _seed) internal view returns (address actor) { + uint256 pick = _seed % 8; + + if (pick < 5) actor = i_eligibleProvider; + else if (pick < 7) actor = i_ineligibleProvider; + else actor = i_outsider; + } + + /// @dev Selects the account a generated exercise request originates from. + function _exerciseCaller(uint256 _seed) internal view returns (address exerciser) { + uint256 pick = _seed % 8; + + if (pick < 6) exerciser = i_authorizedExerciser; + else if (pick < 7) exerciser = i_unauthorizedExerciser; + else exerciser = i_outsider; + } + + /// @dev Decides whether a generated eligibility mutation grants or revokes. + /// + /// Revocation stays reachable on every call, but a history in which every eligible identity spent + /// half its life ineligible would refuse almost everything and reach very little composition, so + /// grants are the more common draw. + function _grantsEligibility(uint256 _seed) internal pure returns (bool eligible) { + eligible = _seed % 4 != 0; + } + + /// @dev Selects the account a generated eligibility mutation originates from. + function _eligibilityCaller(uint256 _seed) internal view returns (address caller) { + caller = _seed % 8 == 0 ? i_outsider : i_registryAdmin; + } + + /// @dev Selects the Beneficiary a generated admission proposes. + function _proposedBeneficiary(uint256 _seed) internal view returns (address beneficiary) { + uint256 pick = _seed % 8; + + if (pick < 4) beneficiary = i_beneficiaryA; + else if (pick < 7) beneficiary = i_beneficiaryB; + else beneficiary = i_ineligibleBeneficiary; + } + + /// @dev Selects a Beneficiary whose eligibility the campaign is allowed to mutate. + function _mutableBeneficiary(uint256 _seed) internal view returns (address beneficiary) { + beneficiary = _seed % 2 == 0 ? i_beneficiaryA : i_beneficiaryB; + } + + /// @dev Selects any persistent identity, including ones with no authority at all. + function _anyActor(uint256 _seed) internal view returns (address actor) { + uint256 pick = _seed % 6; + + if (pick == 0) actor = i_outsider; + else if (pick == 1) actor = i_authorizedExerciser; + else if (pick == 2) actor = i_unauthorizedExerciser; + else if (pick == 3) actor = i_establishmentAuthority; + else if (pick == 4) actor = i_registryAdmin; + else actor = i_eligibleTrader; + } + + /// @dev Selects one candidate liquidity range. + /// + /// Four structurally different shapes: the bootstrap position, a position whose endpoints sit + /// exactly on the configured service boundaries, a position entirely outside the domain, and a + /// position whose endpoints sit strictly inside it — which the realization must refuse however + /// eligible the provider is. + function _candidateRange(uint256 _seed) internal view returns (int24 tickLower, int24 tickUpper) { + (int24 domainLow, int24 domainHigh) = i_tickQ < i_tickO ? (i_tickQ, i_tickO) : (i_tickO, i_tickQ); + + uint256 pick = _seed % LIQUIDITY_RANGE_COUNT; + + if (pick == 0) return (i_lpTickLower, i_lpTickUpper); + if (pick == 1) return (domainLow, domainHigh); + if (pick == 2) return (i_lpTickLower - 10 * i_tickSpacing, domainLow); + + return (domainLow + i_tickSpacing, domainHigh - i_tickSpacing); + } + + /// @dev The custody key of one actor's position over one range. + function _positionKey(address _actor, int24 _tickLower, int24 _tickUpper) internal pure returns (bytes32 key) { + key = keccak256(abi.encode(_actor, _tickLower, _tickUpper)); + } + + /// @dev Reports whether a rejection reason carries the Standby insufficient-backing refusal. + /// + /// A Hook rejection reaches a caller wrapped by the pinned `Hooks` library, so the Standby reason + /// is a payload inside it rather than the outer selector. This searches for it. It is diagnostic + /// only: no campaign outcome depends on the classification. + function _reportsInsufficientProspectiveBacking(bytes memory _reason) internal pure returns (bool reports) { + bytes4 selector = StandbyHook.StandbyHook__InsufficientProspectiveBacking.selector; + + if (_reason.length < 4) return false; + + for (uint256 offset = 0; offset + 4 <= _reason.length; ++offset) { + if ( + _reason[offset] == selector[0] && _reason[offset + 1] == selector[1] + && _reason[offset + 2] == selector[2] && _reason[offset + 3] == selector[3] + ) return true; + } + } +} diff --git a/test/invariant/StandbySequenceEvidence.t.sol b/test/invariant/StandbySequenceEvidence.t.sol new file mode 100644 index 0000000..76f71fb --- /dev/null +++ b/test/invariant/StandbySequenceEvidence.t.sol @@ -0,0 +1,802 @@ +// SPDX-License-Identifier: MIT +pragma solidity 0.8.26; + +/*////////////////////////////////////////////////////////////// + IMPORTS +//////////////////////////////////////////////////////////////*/ + +import {console2} from "forge-std/console2.sol"; + +import {StandbyHook} from "../../src/StandbyHook.sol"; +import {MAX_LIVE_COMMITMENTS} from "../../src/libraries/CommitmentRefs.sol"; + +import {BaseStandbyInvariantTest} from "./BaseStandbyInvariantTest.t.sol"; +import {StandbyInvariantHandler} from "./StandbyInvariantHandler.sol"; + +/*////////////////////////////////////////////////////////////// + CONTRACTS +//////////////////////////////////////////////////////////////*/ + +/// @notice The required GI stateful sequence classes, driven through the same adversarial handler. +/// @dev These are stateful histories, not unit tests. Each one composes several authoritative transitions +/// in a fixed order and asserts what the composition must have preserved — which is exactly what a +/// generated campaign explores, expressed here as the specific semantic classes GI is required to +/// reach rather than left to whether a particular seed happened to reach them. +/// +/// Every action runs through `StandbyInvariantHandler`, so each step in a sequence carries the same +/// transition-local evidence a generated action carries: exact fulfillment attribution, exact +/// Beneficiary delivery, unchanged commitment facts, monotone remainders, fulfillment conservation, +/// empty causal context, and zero protocol custody. The sequences add the ordering. +/// +/// Nothing here is configuration-specific. The economic quantities are derived from the campaign's own +/// independently reconstructed Supporting Capacity and Aggregate Capacity Obligation, so the same +/// sequences are meaningful under the canonical `zeroForOne` service and the generalized `oneForZero` +/// one with asymmetric decimal precision. +abstract contract StandbySequenceEvidence is BaseStandbyInvariantTest { + /*////////////////////////////////////////////////////////////// + STATE VARIABLES + //////////////////////////////////////////////////////////////*/ + + /// @dev The number of generated actions the deterministic diagnostic campaign performs. + uint256 internal constant DIAGNOSTIC_CAMPAIGN_STEPS = 600; + + /// @dev The default admitted validity duration of a scripted commitment. + uint64 internal constant SEQUENCE_VALIDITY = 30 days; + + /// @dev The number of generated action kinds the diagnostic campaign draws from. + uint256 internal constant CAMPAIGN_ACTION_COUNT = 12; + + /*////////////////////////////////////////////////////////////// + BACKING PRESSURE CLASS + //////////////////////////////////////////////////////////////*/ + + /// @notice Proves ordinary swaps respect an authentic obligation across a multi-step history. + /// @dev O1 -> backing-preserving protected swap -> backing-destructive protected swap attempt -> + /// opposite-direction swap -> partial O2 -> protected swap. + function test_backingPressureSequence_preservesBackingAcrossOrdinaryAndProtectedTransitions() public { + uint256 capacity = _referenceSupportingCapacity(); + uint128 entitlement = uint128(capacity / 2); + + uint256 commitmentId = _establishStandardCommitment(beneficiaryA, entitlement); + + assertEq(hook.aggregateObligation(), entitlement, "O1 must establish an authentic positive obligation"); + + assertTrue( + _protectedExactOutputSwap(eligibleTrader, (capacity - entitlement) / 2), + "a backing-preserving protected swap must be admitted" + ); + + uint256 pressured = _referenceSupportingCapacity(); + + assertLt(pressured, capacity, "the admitted swap must actually consume Supporting Capacity"); + assertGe(pressured, hook.aggregateObligation(), "backing must survive the admitted swap"); + + assertFalse( + _protectedExactOutputSwap(eligibleTrader, _destructiveProtectedOutput(pressured)), + "a backing-destructive protected swap must be refused" + ); + + assertEq(_referenceSupportingCapacity(), pressured, "a refused swap must leave the authoritative pool alone"); + assertEq(hook.aggregateObligation(), uint256(entitlement), "a refused swap must release no obligation"); + + assertTrue( + _oppositeExactInputSwap(eligibleTrader, capacity / 8), "an opposite-direction swap must remain admissible" + ); + assertGt(_referenceSupportingCapacity(), pressured, "the opposite-direction swap must restore capacity"); + + assertTrue( + handler.scriptedExercise(authorizedExerciser, commitmentId, entitlement / 2, type(uint256).max), + "a backed partial exercise must complete" + ); + + assertTrue( + _protectedExactOutputSwap(eligibleTrader, (_referenceSupportingCapacity() - hook.aggregateObligation()) / 2), + "a backing-preserving protected swap must remain admissible after fulfillment" + ); + + _assertGlobalClosure(); + } + + /*////////////////////////////////////////////////////////////// + ELIGIBILITY CHURN CLASS + //////////////////////////////////////////////////////////////*/ + + /// @notice Proves eligibility loss releases nothing and eligibility restoration fulfils nothing. + /// @dev O1 -> Beneficiary eligibility off -> backing-threatening O3 attempt -> O2 attempt -> + /// Beneficiary eligibility on -> O2. + function test_eligibilityChurnSequence_neverReleasesObligationOrManufacturesFulfillment() public { + uint256 capacity = _referenceSupportingCapacity(); + uint128 entitlement = uint128(capacity / 2); + + uint256 commitmentId = _establishStandardCommitment(beneficiaryA, entitlement); + + assertTrue( + handler.scriptedSetBeneficiaryEligibility(registryAdmin, beneficiaryA, false), + "the registry administrator must be able to revoke Beneficiary eligibility" + ); + + assertEq( + hook.aggregateObligation(), + uint256(entitlement), + "Beneficiary ineligibility must not release a binding obligation" + ); + + assertFalse( + _protectedExactOutputSwap(eligibleTrader, _destructiveProtectedOutput(_referenceSupportingCapacity())), + "an obligation held by an ineligible Beneficiary must still refuse a destructive swap" + ); + + assertFalse( + handler.scriptedExercise(authorizedExerciser, commitmentId, entitlement / 4, type(uint256).max), + "an ineligible Beneficiary must not be exercised for" + ); + + assertEq( + uint256(hook.commitment(commitmentId).remainingEntitlement), + uint256(entitlement), + "a refused exercise must fulfil nothing" + ); + + assertTrue( + handler.scriptedSetBeneficiaryEligibility(registryAdmin, beneficiaryA, true), + "the registry administrator must be able to restore Beneficiary eligibility" + ); + + assertTrue( + handler.scriptedExercise(authorizedExerciser, commitmentId, entitlement / 4, type(uint256).max), + "a restored Beneficiary must be exercisable again" + ); + + _assertGlobalClosure(); + } + + /*////////////////////////////////////////////////////////////// + MULTIPLE COMMITMENT CLASS + //////////////////////////////////////////////////////////////*/ + + /// @notice Proves fulfillment is attributed to exactly one commitment across interleaved exercises. + /// @dev O1(C1) -> O1(C2) -> partial O2(C1) -> ordinary swap -> O2(C2) -> later O2(C1). + function test_multipleCommitmentSequence_attributesEveryFulfillmentToExactlyOneCommitment() public { + uint256 capacity = _referenceSupportingCapacity(); + uint128 entitlement = uint128(capacity / 4); + + uint256 first = _establishStandardCommitment(beneficiaryA, entitlement); + uint256 second = _establishStandardCommitment(beneficiaryB, entitlement); + + assertEq(hook.aggregateObligation(), uint256(entitlement) * 2, "both commitments must be binding"); + + assertTrue( + handler.scriptedExercise(authorizedExerciser, first, entitlement / 2, type(uint256).max), + "the first commitment must be partially exercisable" + ); + + assertEq( + uint256(hook.commitment(second).remainingEntitlement), + uint256(entitlement), + "one commitment's fulfillment must not reduce another" + ); + + assertTrue( + _protectedExactOutputSwap(eligibleTrader, (_referenceSupportingCapacity() - hook.aggregateObligation()) / 2), + "an ordinary swap must remain admissible between exercises" + ); + + assertTrue( + handler.scriptedExercise(authorizedExerciser, second, entitlement, type(uint256).max), + "the second commitment must be exhaustible" + ); + + assertEq(uint256(hook.commitment(second).remainingEntitlement), 0, "full exercise must exhaust the remainder"); + + assertTrue( + handler.scriptedExercise(authorizedExerciser, first, entitlement / 2, type(uint256).max), + "the first commitment must remain exercisable afterwards" + ); + + assertEq(uint256(hook.commitment(first).remainingEntitlement), 0, "the first commitment must now be exhausted"); + assertEq(hook.aggregateObligation(), 0, "two exhausted commitments must impose nothing"); + + assertEq( + _protectedOutputCurrency().balanceOf(beneficiaryA), + uint256(entitlement), + "the first Beneficiary must hold exactly its own fulfillment" + ); + assertEq( + _protectedOutputCurrency().balanceOf(beneficiaryB), + uint256(entitlement), + "the second Beneficiary must hold exactly its own fulfillment" + ); + + _assertGlobalClosure(); + } + + /*////////////////////////////////////////////////////////////// + EXPIRY / REUSE CLASS + //////////////////////////////////////////////////////////////*/ + + /// @notice Proves expiry releases obligation without fulfilling, and that slots reuse without amnesia. + /// @dev 16 x O1 -> exhausted bounded index -> refused O1 -> advance time -> expiry -> new O1 -> + /// reference reuse -> historical commitment interaction. + function test_expiryAndReuseSequence_reclaimsReferencesWithoutRewritingHistory() public { + uint128 entitlement = uint128(_referenceSupportingCapacity() / 32); + uint64 validUntil = uint64(block.timestamp) + 1 days; + + uint256[] memory established = new uint256[](MAX_LIVE_COMMITMENTS); + + for (uint256 i = 0; i < MAX_LIVE_COMMITMENTS; ++i) { + (bool admitted, uint256 commitmentId) = handler.scriptedEstablish( + establishmentAuthority, + beneficiaryA, + authorizedExerciser, + entitlement, + uint64(block.timestamp), + validUntil + ); + + assertTrue(admitted, "the bounded index must admit sixteen live commitments"); + + established[i] = commitmentId; + } + + assertEq( + hook.aggregateObligation(), + uint256(entitlement) * MAX_LIVE_COMMITMENTS, + "sixteen live commitments must all be binding" + ); + + (bool overflowAdmitted,) = handler.scriptedEstablish( + establishmentAuthority, beneficiaryA, authorizedExerciser, entitlement, uint64(block.timestamp), validUntil + ); + + assertFalse(overflowAdmitted, "a full bounded index must refuse a seventeenth live commitment"); + + StandbyHook.Commitment memory displaced = hook.commitment(established[0]); + + handler.scriptedAdvanceTime(2 days); + + assertEq(hook.aggregateObligation(), 0, "expiry must release every obligation"); + assertEq( + uint256(hook.commitment(established[0]).remainingEntitlement), + uint256(entitlement), + "expiry must not rewrite Remaining Entitlement as though it were fulfilled" + ); + assertEq(handler.ghostFulfilled(established[0]), 0, "expiry must manufacture no fulfillment"); + + uint256 nextBefore = hook.nextCommitmentId(); + + (bool reusedAdmission, uint256 reusedId) = handler.scriptedEstablish( + establishmentAuthority, + beneficiaryB, + authorizedExerciser, + entitlement, + uint64(block.timestamp), + uint64(block.timestamp) + SEQUENCE_VALIDITY + ); + + assertTrue(reusedAdmission, "an expired reference must become reclaimable"); + assertEq(reusedId, nextBefore, "commitment identities must never be recycled"); + + StandbyHook.Commitment memory afterReuse = hook.commitment(established[0]); + + assertEq( + uint256(afterReuse.originalEntitlement), + uint256(displaced.originalEntitlement), + "slot reuse must not rewrite a historical admitted extent" + ); + assertEq( + uint256(afterReuse.remainingEntitlement), + uint256(displaced.remainingEntitlement), + "slot reuse must not rewrite a historical remainder" + ); + assertEq(afterReuse.beneficiary, displaced.beneficiary, "slot reuse must not rewrite a historical Beneficiary"); + assertEq( + uint256(afterReuse.validUntil), + uint256(displaced.validUntil), + "slot reuse must not rewrite a historical term" + ); + + assertFalse( + handler.scriptedExercise(authorizedExerciser, established[0], entitlement, type(uint256).max), + "an expired commitment must not be exercisable after its slot was reused" + ); + + assertTrue( + handler.scriptedExercise(authorizedExerciser, reusedId, entitlement, type(uint256).max), + "the commitment now holding the reused slot must be exercisable" + ); + + _assertGlobalClosure(); + } + + /*////////////////////////////////////////////////////////////// + FULFILLMENT CHURN CLASS + //////////////////////////////////////////////////////////////*/ + + /// @notice Proves repeated partial exercise and final exhaustion stay exact. + /// @dev O1 -> partial O2 -> ordinary swap -> second partial O2 -> full exhaustion. + function test_fulfillmentChurnSequence_staysExactAcrossRepeatedPartialExercise() public { + uint128 entitlement = uint128(_referenceSupportingCapacity() / 2); + + uint256 commitmentId = _establishStandardCommitment(beneficiaryA, entitlement); + + uint256 quarter = uint256(entitlement) / 4; + + assertTrue( + handler.scriptedExercise(authorizedExerciser, commitmentId, quarter, type(uint256).max), + "the first partial exercise must complete" + ); + + assertTrue( + _oppositeExactInputSwap(eligibleTrader, quarter), "an opposite-direction swap must remain admissible" + ); + + assertTrue( + handler.scriptedExercise(authorizedExerciser, commitmentId, quarter, type(uint256).max), + "the second partial exercise must complete" + ); + + uint256 remainder = uint256(hook.commitment(commitmentId).remainingEntitlement); + + assertEq(remainder, uint256(entitlement) - 2 * quarter, "two partial exercises must discharge exactly twice q"); + + assertTrue( + handler.scriptedExercise(authorizedExerciser, commitmentId, remainder, type(uint256).max), + "the final exercise must exhaust the remainder" + ); + + assertEq(uint256(hook.commitment(commitmentId).remainingEntitlement), 0, "the commitment must be exhausted"); + assertEq( + handler.ghostFulfilled(commitmentId), + uint256(entitlement), + "independently tracked fulfillment must equal the admitted extent" + ); + assertEq(hook.aggregateObligation(), 0, "an exhausted commitment must impose nothing"); + assertEq( + _protectedOutputCurrency().balanceOf(beneficiaryA), + uint256(entitlement), + "the Beneficiary must hold exactly the whole admitted extent" + ); + + assertFalse( + handler.scriptedExercise(authorizedExerciser, commitmentId, 1, type(uint256).max), + "an exhausted commitment must not be exercisable again" + ); + + _assertGlobalClosure(); + } + + /*////////////////////////////////////////////////////////////// + CAUSAL CONTAMINATION CLASS + //////////////////////////////////////////////////////////////*/ + + /// @notice Proves failed and completed O2 evidence never authorizes a later unrelated fulfillment. + /// @dev failed O2(C1) -> valid O2(C2) -> O2(C1) -> orphan evidence -> O2(C2). + function test_causalContaminationSequence_neverLetsOneExerciseAuthorizeAnother() public { + uint128 entitlement = uint128(_referenceSupportingCapacity() / 4); + + uint256 first = _establishStandardCommitment(beneficiaryA, entitlement); + uint256 second = _establishStandardCommitment(beneficiaryB, entitlement); + + assertFalse( + handler.scriptedExercise(unauthorizedExerciser, first, entitlement / 2, type(uint256).max), + "an unauthorized exerciser must be refused" + ); + + assertTrue( + handler.scriptedExercise(authorizedExerciser, second, entitlement / 2, type(uint256).max), + "a refused exercise must not contaminate an unrelated valid one" + ); + + assertEq( + uint256(hook.commitment(first).remainingEntitlement), + uint256(entitlement), + "the refused exercise's commitment must be untouched" + ); + + assertTrue( + handler.scriptedExercise(authorizedExerciser, first, entitlement / 2, type(uint256).max), + "the previously refused commitment must remain exercisable by its own authority" + ); + + handler.scriptedOrphanEvidence(authorizedExerciser, first); + handler.scriptedOrphanEvidence(outsider, second); + + assertTrue( + handler.scriptedExercise(authorizedExerciser, second, entitlement / 2, type(uint256).max), + "orphan evidence attempts must leave later valid exercise unaffected" + ); + + assertEq( + handler.ghostFulfilled(first) + handler.ghostFulfilled(second), + uint256(entitlement) / 2 * 3, + "exactly three half-exercises may have been attributed" + ); + + _assertGlobalClosure(); + } + + /*////////////////////////////////////////////////////////////// + EXTERNAL DELIVERY DISCRIMINATION + //////////////////////////////////////////////////////////////*/ + + /// @notice Proves Beneficiary receipt of protected output is not Standby fulfillment. + /// @dev O1 -> direct protected-token transfer to the Beneficiary -> O2. + function test_directTransferSequence_isNeverFulfillmentAndNeverSatisfiesAnEntitlement() public { + uint128 entitlement = uint128(_referenceSupportingCapacity() / 2); + + uint256 commitmentId = _establishStandardCommitment(beneficiaryA, entitlement); + + uint256 donation = uint256(entitlement) / 2; + + assertTrue(handler.scriptedDirectTransfer(beneficiaryA, donation), "an unrelated transfer must be possible"); + + assertEq( + _protectedOutputCurrency().balanceOf(beneficiaryA), + donation, + "the Beneficiary must have received the tokens" + ); + assertEq( + uint256(hook.commitment(commitmentId).remainingEntitlement), + uint256(entitlement), + "an unrelated transfer must not reduce Remaining Entitlement" + ); + assertEq(hook.aggregateObligation(), uint256(entitlement), "an unrelated transfer must release no obligation"); + assertEq(handler.ghostFulfilled(commitmentId), 0, "an unrelated transfer must create no fulfillment"); + + assertTrue( + handler.scriptedExercise(authorizedExerciser, commitmentId, entitlement, type(uint256).max), + "the whole entitlement must still be exercisable after the donation" + ); + + assertEq( + _protectedOutputCurrency().balanceOf(beneficiaryA), + donation + uint256(entitlement), + "the Beneficiary must hold the donation plus the whole fulfilled entitlement" + ); + + _assertGlobalClosure(); + } + + /*////////////////////////////////////////////////////////////// + FAILED-OPERATION SEQUENCE CLASS + //////////////////////////////////////////////////////////////*/ + + /// @notice Proves refused operations never change a later authoritative result. + /// @dev failed O1 -> valid O1 -> failed backing-threatening O3 -> valid O2 -> failed liquidity action -> + /// valid ordinary swap. + function test_failedOperationSequence_neverChangesALaterAuthoritativeResult() public { + uint128 entitlement = uint128(_referenceSupportingCapacity() / 2); + + (bool unauthorizedAdmission,) = handler.scriptedEstablish( + outsider, + beneficiaryA, + authorizedExerciser, + entitlement, + uint64(block.timestamp), + uint64(block.timestamp) + SEQUENCE_VALIDITY + ); + + assertFalse(unauthorizedAdmission, "an account without establishment authority must be refused"); + assertEq(hook.nextCommitmentId(), 1, "a refused O1 must consume no identity"); + + uint256 commitmentId = _establishStandardCommitment(beneficiaryA, entitlement); + + assertFalse( + _protectedExactOutputSwap(eligibleTrader, _destructiveProtectedOutput(_referenceSupportingCapacity())), + "a backing-threatening swap must be refused" + ); + + assertTrue( + handler.scriptedExercise(authorizedExerciser, commitmentId, entitlement / 2, type(uint256).max), + "a refused O3 must not disturb a later valid O2" + ); + + assertFalse( + handler.scriptedModifyLiquidity( + ineligibleProvider, + serviceConfig.lpTickLower, + serviceConfig.lpTickUpper, + int256(uint256(serviceConfig.liquidity)) / 8, + false + ), + "an ineligible provider must be refused" + ); + + assertTrue( + _protectedExactOutputSwap(eligibleTrader, (_referenceSupportingCapacity() - hook.aggregateObligation()) / 2), + "a refused liquidity action must not disturb a later valid ordinary swap" + ); + + _assertGlobalClosure(); + } + + /*////////////////////////////////////////////////////////////// + LIQUIDITY PERIMETER + //////////////////////////////////////////////////////////////*/ + + /// @notice Proves caller and path variation cannot bypass effect-defined backing protection. + /// @dev Untrusted perimeter, ineligible provider, prohibited interior topology, backing-threatening + /// removal, and backing-preserving removal, all against the same authentic obligation. + function test_liquidityPerimeterSequence_cannotBypassEffectDefinedBackingProtection() public { + uint128 entitlement = uint128((_referenceSupportingCapacity() * 3) / 4); + + _establishStandardCommitment(beneficiaryA, entitlement); + + int256 half = int256(uint256(serviceConfig.liquidity)) / 2; + + assertFalse( + handler.scriptedModifyLiquidity( + eligibleProvider, serviceConfig.lpTickLower, serviceConfig.lpTickUpper, -half, true + ), + "a removal routed through the ordinary-swap perimeter must be refused" + ); + + assertFalse( + handler.scriptedModifyLiquidity( + eligibleProvider, serviceConfig.lpTickLower, serviceConfig.lpTickUpper, -half, false + ), + "a backing-threatening removal must be refused whoever performs it" + ); + + assertFalse( + handler.scriptedModifyLiquidity( + eligibleProvider, + serviceConfig.tickQ < serviceConfig.tickO + ? serviceConfig.tickQ + serviceConfig.tickSpacing + : serviceConfig.tickO + serviceConfig.tickSpacing, + serviceConfig.tickQ < serviceConfig.tickO + ? serviceConfig.tickO - serviceConfig.tickSpacing + : serviceConfig.tickQ - serviceConfig.tickSpacing, + int256(uint256(serviceConfig.liquidity)) / 8, + false + ), + "a position introducing an interior boundary must be refused" + ); + + assertEq(hook.aggregateObligation(), uint256(entitlement), "no refused liquidity action may release obligation"); + + assertTrue( + handler.scriptedModifyLiquidity( + eligibleProvider, + serviceConfig.lpTickLower, + serviceConfig.lpTickUpper, + -int256(uint256(serviceConfig.liquidity)) / 16, + false + ), + "a backing-preserving removal must remain possible" + ); + + assertGe( + _referenceSupportingCapacity(), hook.aggregateObligation(), "the admitted removal must preserve backing" + ); + + _assertGlobalClosure(); + } + + /*////////////////////////////////////////////////////////////// + BACKING BOUNDARY CLASS + //////////////////////////////////////////////////////////////*/ + + /// @notice Proves exact sufficiency at the backing boundary stays accepted under composition. + /// @dev A commitment for the whole present Supporting Capacity leaves `S == O`, which preserves backing + /// and must be admitted. From there every capacity-reducing ordinary transition must be refused, + /// because any of them would leave `S < O` — while the exercise the commitment exists for stays + /// admissible, since a complete exercise releases exactly the obligation it consumes. + function test_exactBackingBoundarySequence_acceptsExactSufficiencyAndRefusesEverythingBeyondIt() public { + uint128 entitlement = uint128(_referenceSupportingCapacity()); + + uint256 commitmentId = _establishStandardCommitment(beneficiaryA, entitlement); + + assertEq( + hook.aggregateObligation(), + _referenceSupportingCapacity(), + "exact sufficiency must be admitted, leaving S equal to O" + ); + + assertFalse( + _protectedExactOutputSwap(eligibleTrader, 1), + "at exact sufficiency even the smallest capacity-reducing swap must be refused" + ); + + assertFalse( + handler.scriptedModifyLiquidity( + eligibleProvider, + serviceConfig.lpTickLower, + serviceConfig.lpTickUpper, + -int256(uint256(serviceConfig.liquidity)) / 8, + false + ), + "at exact sufficiency a liquidity removal must be refused" + ); + + assertTrue( + _oppositeExactInputSwap(eligibleTrader, uint256(entitlement) / 8), + "an opposite-direction swap must remain admissible at exact sufficiency" + ); + + assertTrue( + handler.scriptedExercise(authorizedExerciser, commitmentId, entitlement / 2, type(uint256).max), + "the exercise the commitment exists for must remain admissible" + ); + + _assertGlobalClosure(); + } + + /*////////////////////////////////////////////////////////////// + CAMPAIGN QUALITY EVIDENCE + //////////////////////////////////////////////////////////////*/ + + /// @notice Runs a deterministic generated campaign and reports what it actually exercised. (G-I-23) + /// @dev The same adversarial generator the stateful invariant campaigns drive, sequenced by a fixed + /// pseudo-random schedule so that the resulting activity is reproducible and reportable. Every + /// transition-local assertion the handler makes applies to every one of these actions. + /// + /// The floors asserted below are test-quality guards and nothing else: they say a green result was + /// produced by a campaign that actually admitted commitments, fulfilled them partially and + /// completely, refused unbacked transitions against an authentic positive obligation, and moved + /// through lifecycle and eligibility change. They are not protocol semantics, and no protocol + /// requirement is expressed as a counter threshold. + function test_deterministicCampaign_exercisesMeaningfulProtocolBehavior() public { + uint256 seed = uint256(keccak256("standby.gi.deterministic.campaign")); + + for (uint256 step = 0; step < DIAGNOSTIC_CAMPAIGN_STEPS; ++step) { + seed = uint256(keccak256(abi.encode(seed, step))); + + _performGeneratedAction(seed); + } + + StandbyInvariantHandler.ActionCounters memory counters = handler.counters(); + + _reportCampaign(counters); + + assertGt(counters.establishSuccesses, 0, "the campaign must admit commitments"); + assertGt(counters.establishRejections, 0, "the campaign must exercise refused admissions"); + assertGt(counters.maxObservedObligation, 0, "the campaign must reach an authentic positive obligation"); + assertGt(counters.maxLiveReferences, 1, "the campaign must hold several live commitments at once"); + + assertGt(counters.exerciseSuccesses, 0, "the campaign must complete real exercises"); + assertGt(counters.exerciseRejections, 0, "the campaign must exercise refused exercises"); + assertGt(counters.partialFulfillments, 0, "the campaign must reach partial fulfillment"); + assertGt(counters.fullFulfillments, 0, "the campaign must reach full fulfillment"); + + assertGt(counters.protectedSwapSuccesses, 0, "the campaign must execute ordinary protected swaps"); + assertGt(counters.oppositeSwapSuccesses, 0, "the campaign must execute opposite-direction swaps"); + assertGt(counters.swapBackingRejections, 0, "the campaign must refuse backing-destructive transitions"); + + assertGt(counters.liquidityAddSuccesses, 0, "the campaign must exercise liquidity additions"); + assertGt(counters.liquidityRemoveSuccesses, 0, "the campaign must exercise liquidity removals"); + + assertGt(counters.beneficiaryEligibilityMutations, 0, "the campaign must mutate Beneficiary eligibility"); + assertGt(counters.traderEligibilityMutations, 0, "the campaign must mutate trader eligibility"); + assertGt(counters.liquidityEligibilityMutations, 0, "the campaign must mutate liquidity eligibility"); + + assertGt(counters.timeAdvances, 0, "the campaign must advance time"); + assertGt(counters.expiryEvents, 0, "the campaign must reach expiry"); + assertGt(counters.directBeneficiaryTransfers, 0, "the campaign must transfer protected output directly"); + assertGt(counters.orphanEvidenceAttempts, 0, "the campaign must probe orphan O2 evidence"); + + _assertGlobalClosure(); + } + + /*////////////////////////////////////////////////////////////// + INTERNAL FUNCTIONS + //////////////////////////////////////////////////////////////*/ + + /// @dev Runs the production O1 transition for a commitment that is exercisable from admission. + function _establishStandardCommitment(address _beneficiary, uint128 _entitlement) + internal + returns (uint256 commitmentId) + { + bool admitted; + + (admitted, commitmentId) = handler.scriptedEstablish( + establishmentAuthority, + _beneficiary, + authorizedExerciser, + _entitlement, + uint64(block.timestamp), + uint64(block.timestamp) + SEQUENCE_VALIDITY + ); + + assertTrue(admitted, "a backed, authorized, eligible admission must be accepted"); + } + + /// @dev Requests an ordinary exact-output swap in the protected direction, bounded by the domain. + function _protectedExactOutputSwap(address _actor, uint256 _amountOut) internal returns (bool executed) { + executed = handler.scriptedSwap( + _actor, serviceConfig.protectedZeroForOne, int256(_amountOut), serviceConfig.tickQ, false + ); + } + + /// @dev Requests an ordinary exact-input swap in the opposite direction, bounded by the domain. + function _oppositeExactInputSwap(address _actor, uint256 _amountIn) internal returns (bool executed) { + executed = handler.scriptedSwap( + _actor, !serviceConfig.protectedZeroForOne, -int256(_amountIn), serviceConfig.tickO, false + ); + } + + /// @dev The smallest protected output that must break backing from a given capacity. + /// + /// Composed from the present headroom plus a margin, so the request is destructive under either + /// configuration's rounding rather than by a hard-coded amount. + function _destructiveProtectedOutput(uint256 _capacity) internal view returns (uint256 amountOut) { + amountOut = _capacity - hook.aggregateObligation() + _capacity / 100 + 2; + } + + /// @dev Performs one generated action of the deterministic campaign. + function _performGeneratedAction(uint256 _seed) internal { + uint256 action = _seed % CAMPAIGN_ACTION_COUNT; + + if (action == 0) { + handler.establishCommitment(_seed, uint128(_seed >> 32), uint64(_seed >> 96), uint64(_seed >> 160)); + } else if (action == 1) { + handler.exercise(_seed, _seed >> 32, _seed >> 64); + } else if (action == 2) { + handler.ordinaryProtectedSwap(_seed, _seed >> 32); + } else if (action == 3) { + handler.ordinaryOppositeSwap(_seed, _seed >> 32); + } else if (action == 4) { + handler.addLiquidity(_seed, uint128(_seed >> 32)); + } else if (action == 5) { + handler.removeLiquidity(_seed, uint128(_seed >> 32)); + } else if (action == 6) { + handler.advanceTime(_seed); + } else if (action == 7) { + handler.setBeneficiaryEligibility(_seed); + } else if (action == 8) { + handler.setTraderEligibility(_seed); + } else if (action == 9) { + handler.setLiquidityEligibility(_seed); + } else if (action == 10) { + handler.directTransferProtectedTokenToBeneficiary(_seed, _seed >> 32); + } else { + handler.attemptOrphanExerciseEvidence(_seed); + } + } + + /// @dev Re-asserts the whole global invariant closure at the end of a scripted history. + function _assertGlobalClosure() internal view { + invariant_supportingCapacityEqualsIndependentReference(); + invariant_capacityObligationEqualsIndependentReference(); + invariant_supportingCapacityCoversCapacityObligation(); + invariant_commitmentConservation(); + invariant_beneficiaryHoldingsMatchIndependentDeliveryHistory(); + invariant_boundedReferenceIntegrity(); + invariant_bindingCommitmentsRetainALiveReference(); + invariant_protocolHoldsNoCurrencyCustody(); + invariant_noReusableCausalEvidenceSurvives(); + } + + /// @dev Reports what the deterministic campaign actually exercised. + function _reportCampaign(StandbyInvariantHandler.ActionCounters memory _counters) internal pure { + console2.log("--- GI deterministic campaign diagnostics ---"); + console2.log("O1 admitted / refused:", _counters.establishSuccesses, _counters.establishRejections); + console2.log("O2 completed / refused:", _counters.exerciseSuccesses, _counters.exerciseRejections); + console2.log("O2 partial / full:", _counters.partialFulfillments, _counters.fullFulfillments); + console2.log( + "protected swaps attempted / executed:", _counters.protectedSwapAttempts, _counters.protectedSwapSuccesses + ); + console2.log( + "opposite swaps attempted / executed:", _counters.oppositeSwapAttempts, _counters.oppositeSwapSuccesses + ); + console2.log( + "backing-refused swaps / liquidity:", _counters.swapBackingRejections, _counters.liquidityBackingRejections + ); + console2.log("liquidity added / removed:", _counters.liquidityAddSuccesses, _counters.liquidityRemoveSuccesses); + console2.log( + "eligibility mutations B/T/L:", + _counters.beneficiaryEligibilityMutations, + _counters.traderEligibilityMutations, + _counters.liquidityEligibilityMutations + ); + console2.log("eligibility mutations refused:", _counters.eligibilityMutationRejections); + console2.log("time advances / expiry events:", _counters.timeAdvances, _counters.expiryEvents); + console2.log( + "direct transfers / orphan probes:", _counters.directBeneficiaryTransfers, _counters.orphanEvidenceAttempts + ); + console2.log("reference reuse events:", _counters.referenceReuseEvents); + console2.log("max live references:", _counters.maxLiveReferences); + console2.log("max observed obligation:", _counters.maxObservedObligation); + console2.log("backing-boundary observations:", _counters.backingBoundaryObservations); + } +}