certora: prove a market is not read before it is created by claude[bot] · Pull Request #1076 · morpho-org/midnight

claude · 2026-07-23T21:54:58Z

Requested by Mathis GD · Slack thread

Adds a Certora rule proving that no code path reads a market or position field before that market is created (its tickSpacing is still zero). This covers the "show that a market is not read before it is created" item in the verification wishlist (#109).

Interesting find:

updatePositionView and isHealthy technically break that rule (would have been better if they reverted). But we show that they return always the same thing (and something that makes sense).

Add a Certora rule showing that no code path reads a non-empty market or position field before the market is created (its tickSpacing is still zero). A persistent ghost is flipped by Sload hooks on every non-sentinel market state and position field, gated on the market being uncreated and the loaded value being non-zero. A parametric non-view rule asserts the ghost stays false across every entry point, filtering out the raw storage getters that legitimately read a field without requiring the market to exist.

…otCreatedMarket invariants Drop the val != 0 guard from every Sload hook so a read of an uncreated market's field is flagged regardless of value (previously near-vacuous, since uncreated fields are all zero). Assume the NotCreatedMarket empty-if-not-created invariants via requireInvariant to exclude unreachable prover states, and drop the redundant view-getter selector exclusions (already covered by !f.isView). Restrict the conf to the read rule so the assumed invariants are not re-verified here. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XBDthGpRnNF7tdNvCPhCXB

Inline the now-short filtered clause on the rule signature to satisfy the Certora CVL formatter (format CI check). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XBDthGpRnNF7tdNvCPhCXB

…the read rule; clarify hook comment per review

MathisGD

Nice!

… verified (review)

…ed markets Exclude the two computed views from marketNotReadBeforeCreated (they read position fields before any createdness check) and instead prove their uncreated-market behavior is benign: updatePositionView returns (0,0,0) and isHealthy returns true. Redeclare only the required empty-if-not-created invariants (proven in NotCreatedMarket.conf) as requireInvariant hypotheses. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XBDthGpRnNF7tdNvCPhCXB

Deduplicate by relocating updatePositionViewIsZeroIfMarketNotCreated and marketIsHealthyIfNotCreated into NotCreatedMarket.spec, reusing its in-file 'empty if not created' invariants instead of redeclaring them. Remove the isHealthy/mulDivDown/mulDivUp NONDET summaries there so the rules prove against the real functions. Strip the now-unused scaffolding (redeclared invariants, helpers, envfree getters) from MarketNotReadBeforeCreated.spec, keeping only marketNotReadBeforeCreated, and narrow its conf rule list accordingly.

Signed-off-by: MathisGD <74971347+MathisGD@users.noreply.github.com>

Co-authored-by: MathisGD <74971347+MathisGD@users.noreply.github.com> Signed-off-by: MathisGD <74971347+MathisGD@users.noreply.github.com>