feat: Weakest preconditions - Language interface and WP fixpoint (PR H)#8

Open

hxrts wants to merge 23 commits intomasterfrom

Commits on Feb 1, 2026

feat: coPset, gset, and namespace infrastructure for invariant masks
hxrts
committed
Add FiniteMap interface

lzy0505
authored and
hxrts
committed
Clean up list lemmas

lzy0505
authored and
hxrts
committed
Add code

lzy0505
authored and
hxrts
committed
Clean up BigOpL

lzy0505
authored and
hxrts
committed
Fix build

lzy0505
authored and
hxrts
committed
Clean up BigOpM

lzy0505
authored and
hxrts
committed
feat: Add BI-level big separating conjunction
hxrts
committed
feat: Auth CMRA with updates and functors
hxrts
committed
feat: Complete Heap and HeapView functor proofs
hxrts
committed
feat: Add world satisfaction (wsat) stubs
hxrts
committed
feat: Complete world satisfaction (wsat) proofs
hxrts
committed
feat: Add fancy update modality (fupd) stubs
hxrts
committed
feat: Complete fancy update modality (fupd) proofs
hxrts
committed
feat: Add invariants stubs
hxrts
committed
feat: Complete invariants proofs (inv_alloc, inv_acc, inv_alter, inv_iff)
hxrts
committed
feat: Add cancelable invariants stubs
hxrts
committed
Complete cancelable invariants
hxrts
committed
Mark cancelable invariants ported
hxrts
committed
Complete cancelable invariant lemmas
hxrts
committed
feat: Add weakest precondition stubs (PR H)
hxrts
committed
Complete WP and language port
hxrts
committed
feat: Complete weakest precondition proofs (PR H)
hxrts
committed