cvlm test#33

Open

ronanyeah wants to merge 68 commits intomainfrom

Commits on Mar 5, 2026

Initial sanity checks

ericeil
authored and
ronanyeah
committed
WIP

ericeil
authored and
ronanyeah
committed
get_sui_amount equlivalence

ericeil
authored and
ronanyeah
committed
WIP

ericeil
authored and
ronanyeah
committed
WIP

ericeil
authored and
ronanyeah
committed
fix: duplicate summary for system state

kel-certora
authored and
ronanyeah
committed
Create dummy implementation for parametric rules

kel-certora
authored and
ronanyeah
committed
wip: solvency

kel-certora
authored and
ronanyeah
committed
Disable system summaries

kel-certora
authored and
ronanyeah
committed
Solvency: Assume only one validator

kel-certora
authored and
ronanyeah
committed
Summarize exchange rate

kel-certora
authored and
ronanyeah
committed
Update patches

kel-certora
authored and
ronanyeah
committed
Verify correct accounting of total sui supply

kel-certora
authored and
ronanyeah
committed
Remove invalid rule declaration

kel-certora
authored and
ronanyeah
committed
Fix solvency rules

kel-certora
authored and
ronanyeah
committed
Add basic integrity rules

kel-certora
authored and
ronanyeah
committed
Add integrity rules

kel-certora
authored and
ronanyeah
committed
Add rules for validator info consistency

kel-certora
authored and
ronanyeah
committed
Initial CI setup

kel-certora
authored and
ronanyeah
committed
Restructure rules

kel-certora
authored and
ronanyeah
committed
Remove invalid summary

kel-certora
authored and
ronanyeah
committed
Fix no sui iff no lst rule

kel-certora
authored and
ronanyeah
committed
Fix spurious cex in solvency rules

kel-certora
authored and
ronanyeah
committed
Value conservation rules

kel-certora
authored and
ronanyeah
committed
ci: Update conf files

kel-certora
authored and
ronanyeah
committed
ci: print sui version

kel-certora
authored and
ronanyeah
committed
ci: Fix sui version 1.53.2

kel-certora
authored and
ronanyeah
committed
Fix timeouts

kel-certora
authored and
ronanyeah
committed
Add accounting integrity rules

kel-certora
authored and
ronanyeah
committed
Cleanup

kel-certora
authored and
ronanyeah
committed
Rules for fees

kel-certora
authored and
ronanyeah
committed
Fix timeout in arbitrage opportunity rule

kel-certora
authored and
ronanyeah
committed
wip: add liveness rule for redemptions

kel-certora
authored and
ronanyeah
committed
chore: rename

kel-certora
authored and
ronanyeah
committed
Disable nondet summary of vector::contains

kel-certora
authored and
ronanyeah
committed
Simply fresh storage setup

kel-certora
authored and
ronanyeah
committed
chore: munge visibility

kel-certora
authored and
ronanyeah
committed
fix: timeouts in supply increase/decrease rules

kel-certora
authored and
ronanyeah
committed
Verify soundness of refresh summary

kel-certora
authored and
ronanyeah
committed
nondet summary for version upgrade

kel-certora
authored and
ronanyeah
committed
Add rule for spread fee rules

kel-certora
authored and
ronanyeah
committed
fix[ci]: renamed confs

kel-certora
authored and
ronanyeah
committed
fix: bad module name

kel-certora
authored and
ronanyeah
committed
fix: increase smt timeouts

kel-certora
authored and
ronanyeah
committed
fix: validator consistency soundness and missing rule

kel-certora
authored and
ronanyeah
committed
chore: add comments

kel-certora
authored and
ronanyeah
committed
chore: polishing

kel-certora
authored and
ronanyeah
committed
fix: invalid configurations

kel-certora
authored and
ronanyeah
committed
chore: Split CI steps to not hit resource limits

kel-certora
authored and
ronanyeah
committed
chore: Update CI job names

kel-certora
authored and
ronanyeah
committed
fix: Sui supply reconciles only in next epoch

kel-certora
authored and
ronanyeah
committed
fix: validator consistency invariant only holds across epoch boundary

kel-certora
authored and
ronanyeah
committed
chore: disable vacuity checks to mitigate timeout

kel-certora
authored and
ronanyeah
committed
chore: more accurate rule messages

kel-certora
authored and
ronanyeah
committed
Move CI test to Sui v1.62.1 and update certora dependencies to match

ericeil
authored and
ronanyeah
committed
chore: update comments

kel-certora
authored and
ronanyeah
committed
fix: Adjust patches

kel-certora
authored and
ronanyeah
committed
chore: add package_summaries to gitignore

kel-certora
authored and
ronanyeah
committed
chore: force Sui dependencies to match the versions in cvlm/certora_sui_summaries

kel-certora
authored and
ronanyeah
committed
chore[ci]: bump sui version

kel-certora
authored and
ronanyeah
committed
fix: method matching in confs

kel-certora
authored and
ronanyeah
committed
chore[ci]: trigger on PR against main

kel-certora
authored and
ronanyeah
committed
chore:

kel-certora
authored and
ronanyeah
committed
chore: add readme

kel-certora
authored and
ronanyeah
committed
Bump to sui 1.65.2

kel-certora
authored and
ronanyeah
committed
Pin cli version in CI

kel-certora
authored and
ronanyeah
committed
fix[ci]: missing conf

kel-certora
authored and
ronanyeah
committed
Workflow edit
ronanyeah
committed