certora: prove a market is not read before it is created - #1076

Merged

QGarchery merged 17 commits into

mainfrom

certora/market-not-read-before-created

Jul 28, 2026

Commits on Jul 23, 2026

certora: prove a market is not read before it is created
claude
committed
fd0fccd

Commits on Jul 24, 2026

certora: flag market reads value-independently, guard soundness via NotCreatedMarket invariants
claude
committed
9a8b358
certora: apply certoraCVLFormatter to MarketNotReadBeforeCreated.spec
claude
committed
1a32c75
certora: summarize take's external view calls to fix MNRB prover timeout
claude
committed
837e1c6
certora: drop the NotCreatedMarket requireInvariant assumptions from the read rule; clarify hook comment per review
claude
committed
07d7073
certora: exclude only pure getters by selector so computed views stay verified (review)
claude
committed
5f97e42
certora: prove updatePositionView and isHealthy are benign on uncreated markets
claude
committed
e319984
certora: move uncreated-market behavior rules into NotCreatedMarket.spec
claude
committed
b9065cb
Apply suggestion from @MathisGD
MathisGD
authored
f3ed9d1
Apply suggestion from @MathisGD
MathisGD
authored
e5d4994
Apply suggestion from @MathisGD
MathisGD
authored
140e9f1
Apply suggestions from code review
MathisGD
authored
719e7bb
Merge branch 'main' into certora/market-not-read-before-created
MathisGD
authored
774955d
certora: fix CVL formatting after comment trims
claude
committed
daa6ef2

Commits on Jul 27, 2026

Merge branch 'main' into certora/market-not-read-before-created
MathisGD
authored
12f55a5

Commits on Jul 28, 2026

certora: apply review suggestions from QGarchery
claude
committed
5ab9aea
certora: apply review suggestion from QGarchery
claude
committed
dbab021