Repository navigation

Faster, more conclusive `hevm test` on spark-psm: invariant state merging, diamond merges, lemmas, memory fixes - #1248

Open

msooseth wants to merge 43 commits into

mainfrom

spark-psm-invariants

Open

Faster, more conclusive `hevm test` on spark-psm: invariant state merging, diamond merges, lemmas, memory fixes#1248
msooseth wants to merge 43 commits into
mainfrom
spark-psm-invariants

Commits on Oct 26, 2026
- Branch on symbolic prank addresses; short partial warnings in invariant tests
  
  msooseth
  and
  claude
  committed
  a41c37d
- Source locations in the progress log; fix source ids after incremental forge builds
  
  msooseth
  and
  claude
  committed
  e94b5f8
- Simplify literal mul overflow checks, chained bounds, term-level constant propagation; immutables in Foundry source lookup
  
  msooseth
  and
  claude
  committed
  649ec55
- Cap the default solver count by available memory
  
  msooseth
  and
  claude
  committed
  7a1a381
- Keep (c * x) / c == x guards: abstract arithmetic relies on them
  
  msooseth
  and
  claude
  committed
  77d508e
- Lemmas for ceilDiv by a symbolic divisor; recognise simplified mul overflow checks
  
  msooseth
  and
  claude
  committed
  a0bf7ff
Commits on Oct 27, 2026
- Invariant testing keeps only feasible new states, slimmed; fix space leaks in symbolic execution
  
  msooseth
  and
  claude
  committed
  f069bca
- Do not keep the Solidity ASTs, nothing reads them
  
  msooseth
  and
  claude
  committed
  8c76cf5
- Explore pending paths depth-first
  
  msooseth
  and
  claude
  committed
  908a120
- Invariant testing merges states that differ only in their path conditions
  
  msooseth
  and
  claude
  committed
  550cda9
- Shorten the disjunction of merged invariant states
  
  msooseth
  and
  claude
  committed
  925a3f5
- Abstract arithmetic lemmas for division by a constant, ceilDiv fraction reduction and remainders
  
  msooseth
  and
  claude
  committed
  f973796
- Simplify ITE c t k to t when t is k where c is 0
  
  msooseth
  and
  claude
  committed
  8847568
- Merge diamonds and follow decided branches while merging
  
  msooseth
  and
  claude
  committed
  40814e8
- Test options --run-log and --yul-verbosity, default test timeout
  
  msooseth
  and
  claude
  committed
  281ffbb
Commits on Oct 28, 2026
- Reuse simplified path conditions when deciding branches statically
  
  msooseth
  and
  claude
  committed
  d67488f
- Document invariant testing in a tutorial
  
  msooseth
  and
  claude
  committed
  6aa322e
- Shorten invariant target table
  
  msooseth
  and
  claude
  committed
  684e25f
- Shorter invariant example and explanation
  
  msooseth
  and
  claude
  committed
  64ef204
- Changelog entry for the invariant testing tutorial
  
  msooseth
  and
  claude
  committed
  8c64ae1
- Split an exponent chosen between two constants
  
  authored and
  msooseth
  committed
  67a4631
- Fold comparisons of a value with itself rounded down
  
  authored and
  msooseth
  committed
  3051b4b
- Fork on merged values used as memory offsets or sizes
  
  msooseth
  and
  claude
  committed
  d1840a9
Commits on Nov 5, 2026
- Fold operations through nested ITEs of literals
  
  msooseth
  and
  claude
  committed
  e8f3349
- Script reporting which source lines a fuzz run never reaches
  
  msooseth
  and
  claude
  committed
  bfdf680
- Traverse hash-consed expressions as DAGs
  
  msooseth
  and
  claude
  committed
  2f794d6
- Use path-condition bounds to clear impossible mask bits
  
  msooseth
  and
  claude
  committed
  8ba608e
- Log branches the simplifier keeps but the solver decides
  
  msooseth
  and
  claude
  committed
  7800fa6
- Drop bounded masks only when they fold away
  
  msooseth
  and
  claude
  committed
  6394a4b
- fuzz-coverage: do not report otherwise guards
  
  msooseth
  and
  claude
  committed
  bf5fb71
- Fold larger literal ITE trees, prune paths outside a sign-extended range
  
  msooseth
  and
  claude
  committed
  913331f
- Keep shifted bounds out of small-subterm enumeration
  
  msooseth
  and
  claude
  committed
  1c28e89
- Compare a symbolic CREATE init code size as a number
  
  msooseth
  and
  claude
  committed
  346a9ab
- Symbolic dynamic arrays of static types as arguments
  
  msooseth
  and
  claude
  committed
  57bcdae
Commits on Nov 6, 2026
- Visit shared nodes once in query preprocessing
  
  msooseth
  and
  claude
  committed
  320c43d
- Do not split memory arguments of an op that underruns the stack
  
  msooseth
  and
  claude
  committed
  ccd9255
- Share repeated word subterms in solver queries
  
  msooseth
  and
  claude
  committed
  1128de5
- Fork on small-range subterms of memory offsets and sizes
  
  msooseth
  and
  claude
  committed
  0fad503
- Keep arithmetic out of shared word definitions
  
  msooseth
  and
  claude
  committed
  a571ff5
- Set the split memory argument to its value in each branch
  
  msooseth
  and
  claude
  committed
  259c574
- Do not split memory arguments of RETURN and REVERT
  
  msooseth
  and
  claude
  committed
  b466738
- Compare an account's balance with 0 after simplifying it
  
  msooseth
  and
  claude
  committed
  caef3d1
Commits on Nov 7, 2026
- Name only the kinds of dynamic argument a caveat bounded
  
  msooseth
  and
  claude
  committed
  c88715d

Commits

Commits on Oct 26, 2026

Commits on Oct 27, 2026

Commits on Oct 28, 2026

Commits on Nov 5, 2026

Commits on Nov 6, 2026

Commits on Nov 7, 2026