Use new support for invariants - #428

Open

jcp19 wants to merge 9 commits into

claude/gobra-syntax-update-pr412-fhghc8

Commits on Jan 25, 2026

remove ghost Mutex, change to invariants
jcp19
committed
4f6b5e3

Commits on Aug 6, 2026

Merge master into invariants; adapt to new Gobra pred expression syntax
claude
committed
a923d62

Commits on Sep 6, 2026

Merge master into invariants
claude
committed
bb37c2d
Do not require ReadBatch and WriteBatch to be atomic
claude
committed
0e12fb7
Extract the recv permission reasoning into a lemma
claude
committed
ec283f6
Merge master into invariants
claude
committed
93d309f
Stabilize the fold of writeMsgInv after WriteBatch
claude
committed
66f99a7
Raise the assertion timeout of the router package
claude
committed
aff08d3

Commits on Sep 7, 2026

Address review: trim comment and group the IO clauses of ReadBatch
claude
committed
1536d60