[Formal][Property Annotation] Annotate fork--copied-slot invariant#691

Open

Basmet0 wants to merge 8 commits intoEPFL-LAP:mainfrom

Basmet0:invariant2

Commits on Jan 6, 2026

start of invariant 2 (copied slots of partially sent forks are full)
Bas Niekel
committed
traverse to copied slots without loop checking
Bas Niekel
committed
loop detection
Bas Niekel
committed
outputting invariant 2 to the smv model
Bas Niekel
committed
full_0 naming of single-slot buffers (including control merges)
Bas Niekel
committed
sensible naming of invariant 2
Bas Niekel
committed

Commits on Jan 15, 2026

invariants are usually turned off, unless flag is given
Bas Niekel
committed
explaining comment for the invariant
Bas Niekel
committed