Enrich CVL guidance with Codex experimnet: ERC‑4626 and rewards patterns (from Aave Stata specs) #436

omerlerinman · 2025-09-09T07:31:56Z

Summary

This PR updates Certora’s CVL documentation with practical, field-tested examples and tips derived from a recent formal verification effort. The additions sharpen guidance around methods, hooks, functions, ghosts, rules, and invariants, with solver-friendly rounding envelopes and storage patterns aligned to modern ERC‑4626 and rewards-controller designs.

Origin

Source materials: aave-v3-horizon/tree/main/certora/stata/specs
This PR is part of an experiment to assess whether Codex (AI) is suitable for augmenting Certora’s documentation using concrete CVL patterns extracted from customer formal verification projects.

Motivation

Bridge the gap between reference docs and real-world CVL practice.
Codify precision patterns for rounding envelopes, storage hooks, and ghost aggregates that reduce timeouts and avoid common vacuity/unsoundness traps.
Share safe, reusable patterns for ERC‑4626-like wrappers and rewards logic.

Key Updates

Methods
Added practical patterns for:
- Contract aliases via using to target receivers in multi-contract scenes.
- Using envfree for pure/view-like calls.
- Summarization to speed up verification (NONDET, DISPATCHER(true)).
- When to prefer with (env e) vs. envfree to keep models small.
Hooks
- Added real-world storage hooks:
  - Slot/offset Sload gating to reduce spurious models for aToken/underlying/reward token instances.
  - Sstore hook mirroring balance deltas into a ghost sum for scalable invariants.
  - Notes on when slot-level addressing is safe vs. named paths.
Functions
- Added math and rounding summaries:
  - mulDivCVL with explicit rounding direction.
  - Tight mulDiv up/down abstractions that are solver-friendly.
  - WAD helpers and discrete ratio/quotient models to constrain typical cases (2x/5x/100x).
  - Caution on ghost-based math axioms under fixed-point rounding.
Ghosts
- Added patterns from practice:
  - Single-ghost aggregations (sum of scaled balances) via Sstore updates.
  - Guidance on conservative axioms for ghost math to avoid over-constraining the model.
Rules
- Added examples and edge cases drawn from ERC‑4626 + rewards:
  - Preview equals actual (stronger than EIP requirement) and preview independence from allowance.
  - Joining/splitting additivity bounds within ±1 envelope.
  - Deposit upper bounds by index (index > RAY: +1 aToken; index == RAY: +0.5 aToken).
  - Non-zero mint condition when assets*RAY >= index.
  - Mint envelopes: receiver gets in [shares, shares+1].
  - Duplicate reward claim prevention (both sufficient and insufficient pool balances).
Invariants
- Added a practical solvency envelope invariant for ERC‑4626-style wrappers, with filtered/preserved blocks to avoid vacuity and control environment assumptions.
Patterns
- New page: docs/user-guide/patterns/rounding-envelopes.md centralizes ERC‑4626 rounding bounds and examples.

Files Touched

docs/cvl/methods.md — Practical patterns and tips for using, envfree, summaries.
docs/cvl/hooks.md — Slot-gated Sload hooks; Sstore + ghost aggregate pattern.
docs/cvl/functions.md — mulDiv rounding abstractions and WAD helpers.
docs/cvl/ghosts.md — Aggregate ghosts and guidance on math axioms.
docs/cvl/rules.md — ERC‑4626 and rewards examples; rounding envelopes.
docs/cvl/invariants.md — Solvency envelope invariant with filters/preserved blocks.
docs/user-guide/patterns/rounding-envelopes.md — New consolidated page.

Implementation Notes

Examples were integrated where they best contextualize the concepts (methods/hooks/functions/rules/invariants) and also centralized under a dedicated “rounding envelopes” pattern page.
Slot/offset hooks use stable storage layouts from the harness; included with cautions to prefer named access paths when available.

Build & QA

Local build: run in a venv
- python -m venv .venv && source .venv/bin/activate
- pip install -r requirements.txt
- make html
Spelling: make spelling; add domain terms to spelling_wordlist.txt as needed.
Links: make linkcheck; we fixed broken links found in link_output.txt; remaining warnings are about missing local example files not present in this repo (non-blocking).
Open local site: open build/html/index.html

Risks

Slot/offset hooks must match exact storage layouts; usage is documented with cautions.
Aggressive math axioms can introduce unsoundness; guidance favors inequalities and conservative bounds.

Follow-ups

Extend “Rounding Envelopes” with withdraw/redeem envelopes if desired.
Add call-trace snippets to reinforce counterexample intuition.

Acknowledgements

Patterns adapted from Aave Stata Token specs: aave-v3-horizon/tree/main/certora/stata/specs
This PR assesses Codex’s suitability for AI-assisted doc updates by harvesting CVL best practices from customer FV projects.

…3-horizon/tree/main/certora/stata/specs'

…integrate real-world hooks/math tips

…ub links); normalize heading levels; remove link_output.txt

…ave-style); minor spelling tolerances

shellygr

dear lord. almost 100% AI slop

shellygr · 2025-09-09T10:19:23Z

docs/cvl/functions.md

+
+  ```cvl
+  // Rounds up or down depending on a Math.Rounding enum
+  function mulDivCVL(uint256 x, uint256 y, uint256 denominator, Math.Rounding rounding) returns uint256 {


incomplete. Math is defined in OpenZeppelin's Math.sol, so if it is somehow not part of the project we work on, the Math.Rounding won't type check

shellygr · 2025-09-09T10:19:31Z

docs/cvl/functions.md

+  }
+  ```
+
+- Tight, solver-friendly models for up/down `mulDiv` used across specs:


I'm not sure what "Tight" means

shellygr · 2025-09-09T10:20:01Z

docs/cvl/functions.md

+  function mulDivDownAbstractPlus(uint256 x, uint256 y, uint256 z) returns uint256 {
+      uint256 res;
+      require z != 0;
+      uint256 xy = require_uint256(x * y);
+      uint256 fz = require_uint256(res * z);
+      require xy >= fz;
+      require fz + z > to_mathint(xy);
+      return res;
+  }
+
+  function mulDivUpAbstractPlus(uint256 x, uint256 y, uint256 z) returns uint256 {
+      uint256 res;
+      require z != 0;
+      uint256 xy = require_uint256(x * y);
+      uint256 fz = require_uint256(res * z);
+      require xy >= fz;
+      require fz + z > to_mathint(xy);
+      if (xy == fz) { return res; }
+      return require_uint256(res + 1);


I would appreciate someone using thses summaries daily to say whether they're really good

shellygr · 2025-09-09T10:20:57Z

docs/cvl/functions.md

+  ```
+
+```{warning}
+Ghost-based math models can be powerful but require care. For example, a ghost power function `_ghostPow` with axioms like `x^0==1`, monotonicity, and bounds is useful for reasoning, but equality-like axioms may be invalid under fixed-point rounding. Keep axioms conservative and prefer inequality bounds.


did not understand this part

shellygr · 2025-09-09T10:21:50Z

docs/cvl/functions.md

+  function discreteQuotientMulDiv(uint256 x, uint256 y, uint256 z) returns uint256 {
+      uint256 res;
+      require z != 0 && noOverFlowMul(x, y);
+      require(
+          ((x == 0 || y == 0) && res == 0) ||
+          (x == z && res == y) ||
+          (y == z && res == x) ||
+          constQuotient(x, y, z, 2, res)   || // 1/2 or 2
+          constQuotient(x, y, z, 5, res)   || // 1/5 or 5
+          constQuotient(x, y, z, 100, res)    // 1/100 or 100
+      );
+      return res;


constQuotient is not defined

shellygr · 2025-09-09T10:33:27Z

docs/cvl/methods.md

+- Isolate environment explicitly with `with (env e)` when you need to pin `msg.sender`, `block.timestamp`, or similar for a particular call, and use plain `envfree` elsewhere. A consistent pattern across a spec keeps models smaller and avoids accidental dependencies between calls.
+
+```{tip}
+Heavyweight dependencies (Lending pools, incentive controllers) typically benefit from coarse summaries in the spec and fine-grained assertions on observable effects (balances, indices) in rules and invariants.


shellygr · 2025-09-09T10:34:02Z

docs/cvl/rules.md

+- Preview equals actual (ERC-4626). EIP-4626 requires preview functions to not exceed the actual action in the same transaction. In some implementations they are equal; this stronger property is easy to assert:
+
+  ```cvl
+  /// previewDeposit returns the exact deposit shares
+  rule previewDepositAmountCheck(){
+      env e1; env e2;
+      uint256 assets; address receiver;
+      uint256 previewShares = previewDeposit(e1, assets);
+      uint256 shares       = deposit(e2, assets, receiver);
+      assert previewShares == shares, "preview equals actual";
+  }
+  ```


that can be put maybe in the examples repository but not in the official docs

shellygr · 2025-09-09T10:34:27Z

docs/cvl/rules.md

+  }
+  ```
+
+- Deposit envelopes by index (Aave-style index RAY). Bound deposited aTokens relative to requested `assets` and index. For `index > RAY` the bound is `+1 aToken`; for `index == RAY` it tightens to `+0.5 aToken`:


what the hell is envelops and why does codex keep mentioning them?

shellygr · 2025-09-09T10:35:07Z

docs/cvl/rules.md

+  }
+  ```
+
+- Duplicate reward claims do not amplify payout. Whether the contract has sufficient funds or not, listing the same reward twice must not increase net rewards to a user beyond the computed claimable amount:


this is a legitimate rule but it's in the wrong section. Again, I think it should be in an examples repository for reward-distributing code

shellygr · 2025-09-09T10:36:04Z

docs/user-guide/patterns/rounding-envelopes.md

@@ -0,0 +1,102 @@
+# Rounding Envelopes


again bullshit terminology

but this needs to be reviewed by someone working daily on FV of protocols

omerlerinman added 4 commits September 9, 2025 09:32

feat: update the docs with codex iterating the spec files from aave-v…

ca456a8

…3-horizon/tree/main/certora/stata/specs'

chore: codex file to map the repo main repo components

adbd203

chore: .gitignore update

a133abc

docs: add rounding envelopes pattern; fix broken links and includes; …

d192f56

…integrate real-world hooks/math tips

omerlerinman marked this pull request as draft September 9, 2025 07:47

omerlerinman added the existing feature new documentation for an existing feature label Sep 9, 2025

omerlerinman changed the title ~~Docs: Enrich CVL guidance with real-world ERC‑4626 and rewards patterns (from Aave Stata specs)~~ Enrich CVL guidance with Codex experimnet: ERC‑4626 and rewards patterns (from Aave Stata specs) Sep 9, 2025

omerlerinman added 8 commits September 9, 2025 11:29

docs: fix linkcheck warnings (replace local includes with stable GitH…

ce11690

…ub links); normalize heading levels; remove link_output.txt

fix: spelling wordlist

3fe05c0

chore: fix AGENTS.md typos and casing; align with docs style and tone

c37163d

docs: normalize non-breaking hyphens to ASCII hyphens; fix wording (A…

0679371

…ave-style); minor spelling tolerances

fix: more spelling

bf903de

chore: ignore the AGENTS file in the spelling conf

6d7bc94

spelling

3db4b98

fix spelling

3b9ba92

omerlerinman marked this pull request as ready for review September 9, 2025 10:04

omerlerinman requested a review from shellygr September 9, 2025 10:06

shellygr requested changes Sep 9, 2025

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Enrich CVL guidance with Codex experimnet: ERC‑4626 and rewards patterns (from Aave Stata specs) #436

Enrich CVL guidance with Codex experimnet: ERC‑4626 and rewards patterns (from Aave Stata specs) #436

Uh oh!

omerlerinman commented Sep 9, 2025 •

edited

Loading

Uh oh!

shellygr left a comment

Uh oh!

shellygr Sep 9, 2025

Uh oh!

shellygr Sep 9, 2025

Uh oh!

shellygr Sep 9, 2025

Uh oh!

shellygr Sep 9, 2025

Uh oh!

shellygr Sep 9, 2025

Uh oh!

shellygr Sep 9, 2025

Uh oh!

shellygr Sep 9, 2025

Uh oh!

shellygr Sep 9, 2025

Uh oh!

shellygr Sep 9, 2025

Uh oh!

shellygr Sep 9, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Enrich CVL guidance with Codex experimnet: ERC‑4626 and rewards patterns (from Aave Stata specs) #436

Are you sure you want to change the base?

Enrich CVL guidance with Codex experimnet: ERC‑4626 and rewards patterns (from Aave Stata specs) #436

Uh oh!

Conversation

omerlerinman commented Sep 9, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Origin

Motivation

Key Updates

Files Touched

Implementation Notes

Build & QA

Risks

Follow-ups

Acknowledgements

Uh oh!

shellygr left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

omerlerinman commented Sep 9, 2025 •

edited

Loading