feat: Fancy Update Modality (PR E)#6

Open

hxrts wants to merge 18 commits intomasterfrom

fork/iris/invariants

Commits on Jan 29, 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
Merge remote-tracking branch 'origin/fork/iris/big-op' into fork/iris/vendor
hxrts
committed
Merge remote-tracking branch 'origin/fork/iris/auth-updates' into fork/iris/vendor
hxrts
committed
feat: Add world satisfaction (wsat) stubs
hxrts
committed