Loop invariants#43

Merged

raghav198 merged 13 commits into

raghav/weakest-preconditionfrom

raghav/loop-invariants

Jun 24, 2026

Commits on Jun 20, 2026

Single loop invariant inference done
Raghav Malik
committed

Commits on Jun 23, 2026

Loop invariants now mostly strengthening to prove postcondition, things look better
Raghav Malik
committed
Added circom examples
Raghav Malik
committed
New verification results with proper alignment
Raghav Malik
committed
Proper while->for conversion
Raghav Malik
committed
Fixing some errors as they come up
Raghav Malik
committed
Latest results
Raghav Malik
committed
Added demo script
Raghav Malik
committed
Latest results
Raghav Malik
committed

Commits on Jun 24, 2026

Nested loop support and symbolic store added to WP
Raghav Malik
committed
Added back missing slice invariant strengthening
Raghav Malik
committed
New results, added {signal} attribute to mux_ep
Raghav Malik
committed
Removed unused StrongestPostcondition
Raghav Malik
committed