feat(FreeWP): weakest preconditions for FreeM via Std.Do#62

Open

tannerduve wants to merge 7 commits into

Shreyas4991:mainfrom

tannerduve:feat/wp-free

Commits on Jun 2, 2026

feat(FreeWP): weakest preconditions for FreeM via Std.Do
tannerduve
committed
fix(FreeWP): state simp lemmas in simp-normal form, drop unused LawfulMonad
tannerduve
committed

Commits on Jun 3, 2026

test(FreeWP): add query-model WP examples on ReadOnlyVec
tannerduve
committed

Commits on Jun 4, 2026

feat(QueryModel): generic Model→WP bridge + verified bubble sort demo
tannerduve
committed
refactor(VecBubbleSort): use Std order typeclasses; module docstring before section
tannerduve
committed

Commits on Jun 5, 2026