Extend Verus with Logical Atomicity#2326

Open

slerpyyy wants to merge 159 commits into

mainfrom

Commits on Jul 7, 2025

Copy internal docs from branch logatom-syntax
slerpyyy
committed

Commits on Jul 21, 2025

Commits on Jul 23, 2025

Expand design document
slerpyyy
committed

Commits on Jul 28, 2025

Commits on Aug 5, 2025

Get atomic function calls into VIR
slerpyyy
committed

Commits on Aug 11, 2025

Update design document
slerpyyy
committed

Commits on Aug 13, 2025

Commits on Aug 20, 2025

Add WIP helping example to internal docs
slerpyyy
committed

Commits on Aug 26, 2025

Commits on Sep 2, 2025

A lot of progress on atomic calls
slerpyyy
committed

Commits on Sep 3, 2025

Some fixes, tests and updated documentation
slerpyyy
committed

Commits on Sep 8, 2025

Some fixes
slerpyyy
committed

Commits on Sep 13, 2025

Commits on Sep 21, 2025

Refactor SST generation and check for invalid update function use
slerpyyy
committed

Commits on Sep 30, 2025

Commits on Oct 6, 2025

Commits on Oct 8, 2025

Helping example mostly works
slerpyyy
committed

Commits on Oct 9, 2025

Show AUs resolve in helping example
slerpyyy
committed

Commits on Oct 27, 2025

Back from vacation, merging with main
slerpyyy
committed

Commits on Oct 28, 2025

More ergonomic way to assert function predicate arguments
slerpyyy
committed

Commits on Oct 29, 2025

Helping proof almost complete
slerpyyy
committed

Commits on Oct 30, 2025

Commits on Nov 6, 2025

Work towards AU resources in private ensures
slerpyyy
committed

Commits on Nov 12, 2025

Commits on Nov 15, 2025

Set all build and target directories
slerpyyy
committed

Commits on Nov 18, 2025

Add meeting notes
slerpyyy
committed

Commits on Nov 25, 2025

Commits on Nov 26, 2025

Better error messages for atomic update invariant masks
slerpyyy
committed

Commits on Dec 2, 2025

Commits on Dec 3, 2025

More flexible atomic specs and iris comparison
slerpyyy
committed

Commits on Dec 4, 2025

Commits on Dec 5, 2025

More docs and formatting fixes
slerpyyy
committed

Commits on Dec 15, 2025

Merge with upstream/main
slerpyyy
committed

Commits on Dec 18, 2025

Commits on Jan 2, 2026

Commits on Jan 3, 2026

Commits on Jan 5, 2026

Give users ghost access to AU in atomic call
slerpyyy
committed

Commits on Jan 6, 2026

Use arrow syntax for ghost AU in atomic call
slerpyyy
committed

Commits on Jan 10, 2026

Commits on Jan 12, 2026

Replace yield and no_abort with a more general system
slerpyyy
committed

Commits on Jan 13, 2026

Commits on Jan 14, 2026

Better testing and minor fixes
slerpyyy
committed

Commits on Jan 15, 2026

Add loop labels to atomically blocks
slerpyyy
committed

Commits on Jan 21, 2026

Merge with main
slerpyyy
committed

Commits on Jan 28, 2026

Commits on Feb 3, 2026

Commits on Feb 7, 2026

Commits on Feb 9, 2026

Fix mask checking for atomic update
slerpyyy
committed

Commits on Feb 26, 2026

Add syntax for list complement invariant masks
slerpyyy
committed

Commits on Mar 2, 2026

Commits on Mar 3, 2026

Add example atomic increment with direct encoding
slerpyyy
committed

Commits on Mar 6, 2026

Fix AU variance
slerpyyy
committed

Commits on Mar 9, 2026

Merge with main
slerpyyy
committed

Commits on Mar 10, 2026

Commits on Mar 11, 2026

Commits on Mar 18, 2026

Commits on Mar 20, 2026

Fix bug in vir lowering for function calls
slerpyyy
committed

Commits on Apr 1, 2026

Add unsound example
slerpyyy
committed

Commits on Apr 10, 2026

Commits on Apr 14, 2026

Commits on Apr 15, 2026

Some cleaning up
slerpyyy
committed

Commits on Apr 19, 2026

Merge with main
slerpyyy
committed

Commits on Apr 21, 2026

Commits on Apr 22, 2026

Commits on Apr 23, 2026

Commits on Apr 24, 2026

Commits on Apr 28, 2026

Commits on Apr 30, 2026

Commits on May 3, 2026

Commits on May 5, 2026

Commits on May 6, 2026

Commits on May 13, 2026

Commits on May 17, 2026

Merge with main
slerpyyy
committed