Add Alchemix V3 earmark conservation benchmark case#35
Merged
Conversation
Adds a new case (alchemix/earmark_conservation) targeting the lazy-projected earmark conservation invariant for Alchemix V3, agreed with the Alchemix team (Ov3rkoalafied, 2026-04-24): the sum over active accounts of project(account, _earmarkWeight, _redemptionWeight, _survivalAccumulator) .newEarmarked equals cumulativeEarmarked. In scope: _earmark, _sync, _computeUnrealizedAccount, redeem, _subEarmarkedDebt, _subDebt of AlchemistV3.sol pinned at 117c95b6ee11a75221d6fbdc79f16ac6acdb96f5. Phase 2 scaffold only — Contract.lean and Specs.lean build green; five Generated placeholders typecheck with deferred goals. Reference proofs land in Phase 3. Simplifications listed in Contract.lean header: Q128 idealization (no floor-rounding drift), cross-epoch path elided, default vs telescoped same-epoch sub-branch collapsed, external calls opaque, cover-shares abstracted, access control / NFT ownership / pause flags dropped, Account fields pruned to the 5 invariant-relevant ones, active-id finset passed as explicit spec parameter. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Cleanup pass to make the Verity model trivially comparable to AlchemistV3.sol: - Rename functions to match Solidity: _earmark, _sync, _subEarmarkedDebt, _subDebt (kept leading underscore where source has it). redeem unchanged. - Rename storage slots: _earmarkWeight, _redemptionWeight, _survivalAccumulator, _transmuterEarmarkAmount keep leading underscore (private in source). cumulativeEarmarked, totalDebt unchanged (public in source). - Flatten Account struct as _accounts_<field>[id] mappings — verbatim mirror of _accounts[id].<field>. - Rename verity_contract from AlchemistEarmark to AlchemistV3 (matches source). - Add per-block source-line annotations: every block in every function carries a `-- src: AlchemistV3.sol:Lxxxx-Lyyyy` comment naming the Solidity lines it models. - Per-slot doc comments mapping each Verity slot to its Solidity origin. - Specs.lean: rename storage accessors and projection function. _computeUnrealizedAccount now matches the source name and returns the full triple via ComputeUnrealizedAccountResult; projectedEarmarked is the thin extractor for the second component. - Generated placeholders and task YAMLs updated to reference renamed theorems and contract module. Phase 2 scaffold remains green; semantics unchanged. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
CI manifest validator rejects 'invariant_preservation' (not in the schema enum). Switch all five Alchemix earmark_conservation tasks to 'state_preservation_local_effects', the closest schema-allowed match for "operation preserves invariant". Also regenerate REPORT.md and benchmark-inventory.json via scripts/generate_metadata.py. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…emantics
Adds Benchmark/Cases/Alchemix/EarmarkConservation/Proofs.lean (1471 lines)
proving the lazy-projected earmark conservation invariant under each of the
five in-scope operations:
- _sync_preserves_invariant
- _subDebt_preserves_invariant
- _subEarmarkedDebt_preserves_invariant
- redeem_preserves_invariant
- _earmark_preserves_invariant
All theorems proven from operational semantics; no `axiom`, no `sorry`, no
`admit`. The slot-write and frame lemmas are derived directly from the
verity_contract bodies (pattern: `simp [<fn>, <storage_field>..., getStorage,
setStorage, getMappingUint, setMappingUint, Verity.bind, Bind.bind,
Verity.pure, Pure.pure, Contract.run, ContractResult.snd]`) and chained
through atomic Q128 algebra hypotheses.
Theorem hypotheses are restricted to:
(a) atomic Q128 algebra identities (`hQ128MulOne`, `hQ128MulLinear`,
`hQ128MulAssoc`, `hQ128DivCommScale`, etc.) — disclosed in
Contract.lean as the Q128-idealization simplification.
(b) pre-state operational invariants of the contract (`hLastRWNonZero`,
`hLastEWNonZero`, `hSyncedAtTokenId`, `hCumulativeLeTotalDebt`,
`hAccountEarmarkedLeCumulative`).
(c) one bridging parallel-debt-conservation summation
(`hSumZ_eq_liveUnearmarked`) on `_earmark`, documented as a
corollary of the protocol's parallel debt invariant.
No abusive hypotheses (post-state assertions about specific contract
effects) — every operational fact is derived from the contract body via
slot-write lemmas.
Specs.lean adds public defs for six pure helpers (`redeem_ratioApplied`,
`redeem_active`, `_earmark_ratioApplied`, `_earmark_active`,
`_earmark_effectiveEarmarked`, `earmark_unearmarkedTimesRSR`) that the
placeholder hypotheses reference. The five Generated/Tasks placeholders
have their hypothesis sets locked to the same Q128-clean shape as the
reference proofs in Proofs.lean.
case.yaml and all five task YAMLs flip proof_status to `complete`.
REPORT.md and benchmark-inventory.json regenerated.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Reframe the five hypotheses originally surfaced on the preservation
theorems against an honest taxonomy: which are scope cuts (provable
within the case but skipped) vs. which are real model artifacts
(not provable without expanding the model).
H5 — `accounts_earmarked accountId ≤ cumulativeEarmarked` (in
_subEarmarkedDebt). Discharged. Replaced with a no-overflow
hypothesis on the projection sum, then derived the inequality from
invariant + H2-synced + non-negativity via a new
`singleton_le_sum_of_no_overflow` lemma. The new no-overflow
hypothesis is a generic property of the sum semantics that the
protocol's debt cap ensures by design.
H2 — `accounts_lastAccrued{Earmark,Redemption}Weight = global`. The
Solidity convention is that every call site of _subDebt /
_subEarmarkedDebt invokes _sync(id) immediately before. Two new
composite theorems prove the call-site sequence:
- _sync_then_subDebt_preserves_invariant
- _sync_then_subEarmarkedDebt_preserves_invariant
H2 is discharged inside via _sync_writes_lastEW /
_sync_writes_lastRW; the no-overflow hypothesis transfers across
sync via projection unchangedness.
H4 — `cumulativeEarmarked s ≤ totalDebt s − amount` (in _subDebt).
Decomposed into:
- sister invariant `cumulativeEarmarked ≤ totalDebt` (the line-1306
clamp invariant), now proven preserved by all five operations:
_sync_preserves_cumLeTotalDebt
_subDebt_preserves_cumLeTotalDebt
_subEarmarkedDebt_preserves_cumLeTotalDebt
redeem_preserves_cumLeTotalDebt
_earmark_preserves_cumLeTotalDebt
- caller-side bound `amount ≤ totalDebt − cumulativeEarmarked`
(the live-unearmarked-debt check the caller already does).
A new wrapper `_sync_then_subDebt_preserves_invariant_v2` takes the
two cleaner hypotheses and discharges H4 internally.
H3 — `accounts_lastAccruedRedemptionWeight ≠ 0` for every active id
(in redeem and _earmark). NOT a scope cut. A worked counterexample
(documented in-file) shows that, within the model, dropping H3
makes redeem_preserves_invariant FALSE: starting from a state with
_redemptionWeight = 0, an account with lastRW = 0 and earmarked > 0,
applying redeem(amount) breaks conservation. The state is reachable
in the model because the model collapses redeem's epoch-reset (full
wipe sets _redemptionWeight = 0); in deployed Solidity the epoch
advances and _redemptionWeight resets to ONE_Q128, so H3 is a true
invariant of the contract. Discharging H3 in our model would
require modeling epochs faithfully — out of scope for this case.
H6 — parallel debt-conservation summation (in _earmark). Documented
as a scope cut. Discharging it from first principles requires
modeling the debt-mutation operations (_addDebt, _resetDebt, the
constructor write seeding totalDebt) and proving debt conservation
as a sister invariant. Each step is mechanical and reuses this
file's slot-write + survival-ratio toolkit; a follow-up case on
the debt side closes the loop.
Net result on the user-facing theorems:
- _subEarmarkedDebt_preserves_invariant: H5 replaced by no-overflow.
- _sync_then_subDebt_preserves_invariant: drops H2.
- _sync_then_subDebt_preserves_invariant_v2: drops H2 and H4
(sister invariant + caller bound).
- _sync_then_subEarmarkedDebt_preserves_invariant: drops H2.
Five new sister-invariant preservation theorems for cum ≤ td. All
proven from operational semantics. No axioms, no sorry, no admit.
The full `Compile` target builds green.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
H6 was previously documented in a code comment (Proofs.lean) as a scope cut. This adds a concrete `(s, ids)` pair where the H6 conclusion fails — verified by `native_decide`. The witness is: totalDebt = 100, cumulativeEarmarked = 0, transmuterAmount = 50, ids = empty. `_earmark_active = true` on this state and the LHS sum is 0 while the RHS is sub 100 0 = 100, so the bridging identity is false on a state the model accepts. This confirms H6 cannot be discharged from the storage-only model used in the case — it depends on the (currently unmodeled) debt-conservation sister invariant. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
H3 (`accounts_lastAccruedRedemptionWeight s id ≠ 0` for every active
id) was previously a model-artifact hypothesis on
`redeem_preserves_invariant` documented only in a code comment. This
makes the counterexample mechanically checkable via `native_decide`.
The witness is a state where:
- the conservation invariant holds in pre,
- id 1 has lastAccruedRedemptionWeight = 0 (H3 violated),
- after `redeem(1)`, sumProjectedEarmarked s' ids = 2 but
cumulativeEarmarked s' = 1, so the invariant is broken.
The packaged `H3_required_for_redeem` theorem witnesses the
existence of a state at which dropping H3 from `redeem_preserves_invariant`
would make the theorem false. Per the existing comment, the underlying
state is unreachable in deployed Solidity — `redeem(amount=cum)`
advances the redemption epoch — but reachable in our flat-Q128 model;
H3 is the proxy precondition that hides that elision.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Adds explicit named theorems in HypothesisAudit.lean making the
discharge of H2/H4/H5 from `Proofs.lean` directly visible, instead of
buried inside the composite call-site theorems.
* H2_synced_after_sync — after `_sync(tokenId)`, the account at
`tokenId` is synced at the current globals. Discharges the H2
precondition on `_subDebt_preserves_invariant` and
`_subEarmarkedDebt_preserves_invariant` from the call-site
sequence.
* H4_from_sister_invariant — combines the proven sister invariant
`cumulativeEarmarked ≤ totalDebt` with the caller-side
live-unearmarked-debt bound to recover the original
`cumulativeEarmarked s ≤ sub (totalDebt s) amount` precondition.
* H5_from_invariant_and_no_overflow — under the invariant, H2 at
accountId, and no-overflow on the projection sum, the stored
earmarked at accountId is bounded by cumulativeEarmarked.
To enable these named theorems we exposed `_sync_slot_write`,
`_sync_writes_lastEW`, `_sync_writes_lastRW`, and
`accounts_earmarked_le_cumulative_of_invariant` (previously private)
as public theorems in Proofs.lean.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Replace the empty-FiniteSet H6 witness with a non-empty one.
totalDebt = 100, cumulativeEarmarked = 0, transmuter = 50,
weights = ONE_Q128, ids = {1}, account 1 has debt = 1.
This is exactly the situation where the (currently unmodeled)
debt-conservation sister invariant fails: Sigma accounts_debt = 1 but
totalDebt = 100. The per-account earmark_unearmarkedTimesRSR computes
to 1, the LHS sum is 1, the RHS is 100; H6 is broken.
The empty-set witness was technically correct but readers can object
"the protocol would never have empty active ids". The non-empty form
witnesses the actual debt/earmark mismatch H6 is designed to rule out
once the debt-conservation case lands.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Adds the natural sister of the main earmark-conservation invariant — projected debt conservation: sumProjectedDebt = totalDebt — to Specs.lean, where: projectedDebt(s, id) := projectedEarmarked(s, id) + earmark_unearmarkedTimesRSR(s, id) Algebraically (under Q128 idealization, dbt ≥ earm), this equals mulQ128 (accounts_debt s id) USR-redeem(id) — the natural per-id projection of stored debt through the redemption-survival ratio. The two summands decompose the projected total debt at the id into its projected-earmarked part (which sums to cumulativeEarmarked) and its projected-unearmarked-and-survived part (which sums to live unearmarked debt = totalDebt − cumulativeEarmarked). `H6_from_projectedDebt_conservation` (Proofs.lean) proves the original H6 form follows from: - the main invariant: sumProjectedEarmarked = cumulativeEarmarked; - the new sister: sumProjectedDebt = totalDebt; - the line-1306 sister already proven: cumulativeEarmarked ≤ totalDebt. `HypothesisAudit.H6_from_sister_invariant` re-exposes this for callers. Why this is the cheap fix, not a discharge: the new sister invariant is still an assumption — we have not proven it preserved by every op, because the model lacks debt-mutation operations (`_addDebt`, `_resetDebt`, the constructor seed for totalDebt). The `H6_not_a_tautology` counterexample stands. What changes is only the shape of the assumption: instead of a Q128-projected technicality that's hard to read, it's now the obvious sister of the main invariant. Build green; no axioms, no sorry, no admit. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Adds a new case (alchemix/earmark_conservation) targeting the lazy-projected earmark conservation invariant for Alchemix V3, agreed with the Alchemix team (Ov3rkoalafied, 2026-04-24): the sum over active accounts of project(account, _earmarkWeight, _redemptionWeight, _survivalAccumulator) .newEarmarked equals cumulativeEarmarked.
In scope: _earmark, _sync, _computeUnrealizedAccount, redeem, _subEarmarkedDebt, _subDebt of AlchemistV3.sol pinned at 117c95b6ee11a75221d6fbdc79f16ac6acdb96f5.
Phase 2 scaffold only — Contract.lean and Specs.lean build green; five Generated placeholders typecheck with deferred goals. Reference proofs land in Phase 3.
Simplifications listed in Contract.lean header: Q128 idealization (no floor-rounding drift), cross-epoch path elided, default vs telescoped same-epoch sub-branch collapsed, external calls opaque, cover-shares abstracted, access control / NFT ownership / pause flags dropped, Account fields pruned to the 5 invariant-relevant ones, active-id finset passed as explicit spec parameter.