Certora · omerlerinman · Sep 9, 2025 · Sep 9, 2025 · Sep 9, 2025 · Sep 9, 2025
diff --git a/.gitignore b/.gitignore
@@ -20,4 +20,14 @@ __pycache__
 
 #direnv
 .envrc
-.direnv
+.direnv
+
+
+# Virtual environment
+.venv/
+
+# dev files
+reference_files/
+
+# error files
+errors.txt
diff --git a/AGENTS.md b/AGENTS.md
@@ -0,0 +1,131 @@
+# Repository guidelines
+
+You are a world-class formal verification expert, specialized in Certora's CVL.
+Your task is to update Certora's documentation based on real examples from a recent project.
+Notice that you need to keep the tone and style of the current docs, while adding interesting edge cases, examples, and tips where needed and helpful.
+Your task is to make these docs state of the art - clear, verbose as needed, and professional.
+This is a super important task - good luck!
+
+
+## Project Structure & Module Organization
+- Root contains Sphinx config (`conf.py`), entry page (`index.rst`), and build scripts (`Makefile`, `make.bat`).
+- `docs/` holds most content pages (reStructuredText and MyST Markdown).
+- `static/` contains images and custom CSS (e.g., `custom.css`, logos).
+- `Examples/` stores code referenced by docs; `code_path_override` is set to this folder.
+- `util/` has Sphinx helpers used in `conf.py`.
+- Built artifacts go to `build/` (created by Sphinx targets).
+
+## Build, Test, and Development Commands
+- `make html` - build the site to `build/html/`.
+- `make linkcheck` - verify external and internal links.
+- `make spelling` - spell-check docs using `spelling_wordlist.txt`.
+- `make` - runs `spelling` then `html` (default target).
+- Install deps: `python -m venv .venv && source .venv/bin/activate && pip install -r requirements.txt`.
+
+## Coding Style & Naming Conventions
+- Content format: prefer `.rst`; `.md` (MyST) is supported via `myst_parser`.
+- Headings: sentence case; one H1 per page; stable anchors.
+- Filenames: lowercase-with-dashes, group by topic inside `docs/`.
+- Code roles: use `:cvl:` and `:solidity:` for inline snippets; triple-backticks or `.. code-block::` for blocks.
+- Lists/notes: use Sphinx directives (`.. note::`, `.. warning::`) where appropriate.
+
+## Pull Requests & Review Checklist
+
+Use this lightweight checklist to keep PRs smooth and CI‑green.
+
+- Title and scope
+  - Clear, scannable subject in imperative mood, ≤72 chars.
+  - Limit scope; avoid mixing refactors with content edits.
+  - Example: `docs: add rounding envelopes; fix broken includes`.
+
+- Description structure
+  - Motivation: why this change improves the docs (e.g., reduces timeouts, avoids vacuity).
+  - Origin/source: link to real specs when applicable (e.g., `aave-v3-horizon/tree/main/certora/stata/specs`).
+  - Key updates: bullets of files/sections touched and notable patterns added.
+  - Validation: include `make spelling` and `make linkcheck` results.
+  - Risks and follow‑ups: slot/offset cautions, anchors, future pages.
+
+- Linking and anchors
+  - Prefer HTTPS and stable top‑level links. Avoid deep anchors that may 404.
+  - For external code examples, prefer GitHub permalinks over local `.. include::`.
+  - For new pages, add them to a relevant `.. toctree::` (or index) so RTD builds include them.
+  - Use ASCII hyphens (`-`) instead of non‑breaking dashes.
+
+- Backticks and code fences
+  - Inline code: use single backticks like `` `make spelling` ``.
+  - Code blocks: triple backticks with a language when possible.
+  - Prefer `:cvl:` and `:solidity:` roles for inline snippets in reST contexts.
+
+## Local Build & CI Runbook
+
+Run everything inside a virtual environment and verify locally before pushing.
+
+1) Create venv and install deps
+   - `python -m venv .venv && source .venv/bin/activate && pip install -r requirements.txt`
+
+2) Spelling (project files only)
+   - `make spelling`
+   - To emulate CI’s check and see errors inline:
+     - `find build/spelling -name "*.spelling" -type f | xargs cat > errors.txt`
+     - `[[ ! $(cat errors.txt) ]] || (echo && echo "errors:" && cat errors.txt && false)`
+   - Fix content first (typos, ASCII hyphens), only then add truly domain‑specific words to `spelling_wordlist.txt`.
+   - Do not add generic words; prefer content fixes.
+
+3) Links
+   - `make linkcheck`
+   - Replace broken or redirected URLs with stable destinations.
+   - Convert missing local includes to external links (GitHub) when Examples are not vendored.
+
+4) HTML build
+   - `make html` then open `build/html/index.html`.
+
+5) Read the Docs
+   - Ensure new pages are in a `toctree` and not excluded in `conf.py`.
+   - Exclude non‑doc files (like `AGENTS.md`) via `exclude_patterns` to avoid spelling noise.
+
+6) GitHub checks and status
+   - Use the GitHub UI or `gh pr view <branch> --json statusCheckRollup` to inspect failing jobs.
+   - Typical failures:
+     - Spelling: fix typos or add terms to `spelling_wordlist.txt`.
+     - Linkcheck: update or remove broken links, prefer HTTPS.
+     - RTD build: ensure includes/`toctree` coverage; avoid missing local files.
+
+## Patterns from this project
+
+- Avoid non‑breaking hyphens (U+2010–U+2015). Use `-` only.
+- Prefer external GitHub links over `literalinclude`/`cvlinclude` to local Examples not in the repo.
+- When adding a new pattern page (e.g., rounding envelopes), wire it into the relevant patterns `index.md`.
+- Slot/offset hooks are powerful but brittle; document storage layout assumptions and prefer named access paths.
+
+## PR message template (suggested)
+
+- Title: `Docs: <short outcome> (from <origin>)`
+- Description:
+  - Summary (what changed, why)
+  - Origin (e.g., `aave-v3-horizon/tree/main/certora/stata/specs`)
+  - Motivation (timeouts avoided, vacuity mitigations, clarity)
+  - Key updates (bulleted file list)
+  - Build & QA (spelling/linkcheck/HTML ok)
+  - Risks (slot/offset hooks, anchors)
+  - Follow‑ups (optional extractions, screenshots)
+
+## CI hygiene (what we changed in this repo)
+
+- `conf.py`: `exclude_patterns` includes `AGENTS.md` to keep meta‑guidance out of spelling/link builds.
+- Spelling: keep `spelling_wordlist.txt` tight; add only domain‑specific terms.
+- Links: use stable GitHub URLs for Examples, avoid brittle anchors.
+
+## Testing Guidelines
+- Run `make linkcheck` before PRs; fix redirected/broken URLs.
+- Run `make spelling`; add project terms to `spelling_wordlist.txt` instead of disabling checks.
+- Validate local build opens cleanly: `open build/html/index.html`.
+
+## Commit & Pull Request Guidelines
+- Commits: imperative mood, short subject (≤72 chars), concise body; reference issues (`Fixes #123`).
+- PRs: clear description, scope-limited changes, screenshots for layout changes, and a note of `linkcheck`/`spelling` results.
+- Keep diffs focused; avoid mixing refactors with content edits.
+
+## Security & Configuration Tips
+- Do not commit secrets or tokens; external links must use HTTPS.
+- `requirements.txt` is generated from `_requirements.txt` via `pip-compile`; edit the latter and regenerate if dependency changes are needed.
+- Read the Docs builds use `.readthedocs.yaml`; ensure new files are included by Sphinx (not excluded in `conf.py`).
diff --git a/conf.py b/conf.py
@@ -69,6 +69,8 @@
     "docs/cvl/cvl2/cvl2",
     ".github",
     "Examples/*",
+    "AGENTS.md",
+    "AGENTS",
 ]
 
 

diff --git a/docs/cvl/functions.md b/docs/cvl/functions.md
@@ -43,3 +43,77 @@ Using CVL functions
 -------------------
   CVL Function may be called from within a rule, or from within another CVL function.
 
+Math and rounding summaries
+---------------------------
+
+In real protocols, arithmetic often requires precise rounding envelopes. CVL functions are a clean way to centralize these rules as small, reusable summaries.
+
+- Round-aware `mulDiv` abstraction with explicit direction:
+
+  ```cvl
+  // Rounds up or down depending on a Math.Rounding enum
+  function mulDivCVL(uint256 x, uint256 y, uint256 denominator, Math.Rounding rounding) returns uint256 {
+      if (rounding == Math.Rounding.Floor) {
+          return mulDivDownAbstractPlus(x, y, denominator);
+      } else {
+          return mulDivUpAbstractPlus(x, y, denominator);
+      }
+  }
+  ```
+
+- Tight, solver-friendly models for up/down `mulDiv` used across specs:
+
+  ```cvl
+  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);
+  }
+  ```
+
+- Convenience wrappers for fixed‑point WAD arithmetic:
+
+  ```cvl
+  definition ONE18() returns uint256 = 1000000000000000000;
+  function mulDownWad(uint256 x, uint256 y) returns uint256 { return mulDivDownAbstractPlus(x, y, ONE18()); }
+  function mulUpWad(uint256 x, uint256 y)   returns uint256 { return mulDivUpAbstractPlus(x, y, ONE18()); }
+  function divDownWad(uint256 x, uint256 y) returns uint256 { return mulDivDownAbstractPlus(x, ONE18(), y); }
+  function divUpWad(uint256 x, uint256 y)   returns uint256 { return mulDivUpAbstractPlus(x, ONE18(), y); }
+  ```
+
+- Discrete ratio/quotient variants can drastically reduce search space by constraining common cases (e.g., 2x, 5x, 100x), while still allowing exact cases to pass through:
+
+  ```cvl
+  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;
+  }
+  ```
+
+```{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.
+```
diff --git a/docs/cvl/ghosts.md b/docs/cvl/ghosts.md
@@ -195,7 +195,8 @@ Restrictions on ghost axioms
 ----------------------------
 - A ghost axiom cannot refer to Solidity or CVL functions or to other ghosts. It can refer to the ghost itself.
 - Since the signature of a ghost contains just parameter types without names, it cannot refer to its parameters. 
- `forall` can be used in order to refer the storage referred to by the parameters. [Example](https://github.com/Certora/Examples/blob/61ac29b1128c68aff7e8d1e77bc80bfcbd3528d6/CVLByExample/summary/ghost-summary/ghost-mapping/certora/specs/WithGhostSummary.spec#L12).
+ `forall` can be used in order to refer the storage referred to by the parameters. Example: see the ghost-mapping summary spec on GitHub:
+ [ghost mapping summary example](https://github.com/Certora/Examples/blob/61ac29b1128c68aff7e8d1e77bc80bfcbd3528d6/CVLByExample/summary/ghost-summary/ghost-mapping/certora/specs/WithGhostSummary.spec)
 
 
 
@@ -314,3 +315,20 @@ for reverting behaviors of `noUserDefinedRevertFlows` and `emptyRequire`,
 which do not have user-defined revert messages. 
 This means that if `saw_user_defined_revert_msg` is not marked persistent, 
 the rule cannot distinguishing between methods that may revert with user-defined messages and methods that may not.
+
+Patterns from practice
+----------------------
+
+- Aggregate with a single ghost. Track the sum of scaled balances (or other per-account data) by updating a ghost in an `Sstore` hook. This enables global checks without iterating storage:
+
+  ```cvl
+  ghost mathint sumAllATokenScaledBalance {
+      init_state axiom sumAllATokenScaledBalance == 0;
+  }
+
+  hook Sstore _AToken._userState[KEY address a].(offset 0) uint128 balance (uint128 old_balance) {
+      sumAllATokenScaledBalance = sumAllATokenScaledBalance + balance - old_balance;
+  }
+  ```
+
+- Ghost math with conservative axioms. When introducing ghosts such as `_ghostPow(x,y)` for fixed-point exponentiation, prefer monotonicity and bound relations to exact equalities which may be broken by rounding. Keep axioms minimal and purposeful to avoid over-constraining the solver.
diff --git a/docs/cvl/hooks.md b/docs/cvl/hooks.md
@@ -204,6 +204,47 @@ was used as the key into the mapping `C.users`; the variable `v` will contain
 the value that is written, and the variable `old_value` will contain the value
 that was previously stored there.
 
+Real-world storage hooks
+------------------------
+
+Two patterns often help scale larger specs:
+
+- Gate storage reads to a single known instance using slot/offset addressing. This prevents spurious models where an arbitrary address is treated as the reward token, aToken, or underlying:
+
+  ```cvl
+  // Only allow a single registered reward token at the expected slot/index.
+  hook Sload address reward (slot 0x4fad66563f105be0bff96185c9058c4934b504d3ba15ca31e86294f0b01fd200).(offset 32)[INDEX uint256 i] /* _rewardTokens */ {
+      require reward == _DummyERC20_rewardToken;
+  }
+
+  // Constrain the aToken and underlying addresses to the harnessed instances.
+  hook Sload address aToken     (slot 0x55029d3f54709e547ed74b2fc842d93107ab1490ab7555dd9dd0bf6451101900).(offset 0)  /* aToken */ {
+      require aToken == _AToken;
+  }
+  hook Sload address underlying (slot 0x0773e532dfede91f04b12a73d3d2acd361424f41f76b4fb79f090161e36b4e00).(offset 0) /* _asset */ {
+      require underlying == _DummyERC20_aTokenUnderlying;
+  }
+  ```
+
+  ```{note}
+  Slot/offset hooks are low-level and must match the target layout exactly. Prefer named access paths when possible; fall back to slots when the layout is stable and names are unavailable.
+  ```
+
+- Mirror on-chain deltas into ghosts with `Sstore` hooks to enable global checks without scanning storage. For example, track the sum of scaled balances using a single ghost:
+
+  ```cvl
+  ghost mathint sumAllATokenScaledBalance {
+      init_state axiom sumAllATokenScaledBalance == 0;
+  }
+
+  // Update the ghost on every balance write: new minus old.
+  hook Sstore _AToken._userState[KEY address a].(offset 0) uint128 balance (uint128 old_balance) {
+      sumAllATokenScaledBalance = sumAllATokenScaledBalance + balance - old_balance;
+  }
+  ```
+
+  This enables invariants over the aggregate (e.g., conservation across actions) without enumerating all keys.
+
 There are a few restrictions on the available combinations of low-level and
 high-level access paths:
  - You cannot access struct fields on access paths that contain `slot` or
@@ -525,5 +566,3 @@ At this point, you may expect that the hook will be triggered a second time,
 but because there is already a hook executing, this second update to `x` will
 not trigger the hook.  Therefore the `xStoreCount` ghost will *not* be updated
 a second time, so its final value will be `1`.
-
-
diff --git a/docs/cvl/invariants.md b/docs/cvl/invariants.md
@@ -597,3 +597,62 @@ is always logically sound to add a `requireInvariant` to a `preserved` block,
 even for complicated interdependent invariants (as long as the required
 invariants have been verified).
 
+Practical example: solvency envelope
+------------------------------------
+
+It is common to assert a coarse solvency envelope and then use `filtered` and `preserved` to keep the proof tractable while avoiding vacuity. For an ERC-4626-style wrapper over an interest-bearing aToken, the following is effective:
+
+```cvl
+/// Total aTokens (scaled) covering totalSupply of shares
+invariant solvency_total_asset_geq_total_supply()
+    (_AToken.scaledBalanceOf(currentContract) >= totalSupply())
+    filtered { f ->
+        f.contract == currentContract
+        && !harnessMethodsMinusHarnessClaimMethods(f)
+        && !claimFunctions(f)
+        && f.selector != sig:emergencyEtherTransfer(address,uint256).selector
+        && f.selector != sig:claimDoubleRewardOnBehalfSame(address, address, address).selector } {
+
+    preserved withdraw(uint256 assets, address receiver, address owner) with (env e) {
+        require balanceOf(owner) <= totalSupply();
+    }
+
+    preserved depositWithPermit(uint256 assets, address receiver, uint256 deadline,
+                                IERC4626StataToken.SignatureParams signature, bool toAave) with (env e) {
+        require balanceOf(receiver) <= totalSupply();
+        require e.msg.sender != currentContract;
+    }
+
+    preserved depositATokens(uint256 assets, address receiver) with (env e) {
+        require balanceOf(receiver) <= totalSupply();
+        require e.msg.sender != currentContract;
+    }
+
+    preserved deposit(uint256 assets, address receiver) with (env e) {
+        require balanceOf(receiver) <= totalSupply();
+        require e.msg.sender != currentContract;
+    }
+
+    preserved mint(uint256 shares, address receiver) with (env e) {
+        require balanceOf(receiver) <= totalSupply();
+        require e.msg.sender != currentContract;
+    }
+
+    preserved redeem(uint256 shares, address receiver, address owner) with (env e) {
+        require balanceOf(owner) <= totalSupply();
+    }
+
+    preserved redeemATokens(uint256 shares, address receiver, address owner) with (env e) {
+        require balanceOf(owner) <= totalSupply();
+    }
+
+    preserved emergencyTokenTransfer(address asset, address to, uint256 amount) with (env e) {
+        require rate() >= RAY();
+    }
+}
+```
+
+This showcases a few practical points:
+- Use `filtered` to exclude methods irrelevant to the solvency relation (e.g., reward claims, emergency Ether transfers).
+- Express simple local side-conditions inside `preserved` blocks rather than as global invariants.
+- Guard sender assumptions explicitly to avoid degenerate self‑calls.