[Formal][PropertyAnnotation] Annotating SingleEntryToken invariant#908

Open

Basmet0 wants to merge 13 commits into

EPFL-LAP:mainfrom

Basmet0:invariant8

Commits on Apr 30, 2026

boilerplate for effective slot namers
Bas Niekel
committed

Commits on May 1, 2026

annotate entry token order
Bas Niekel
committed

Commits on May 4, 2026

export-rtl for entry token order invariant
Bas Niekel
committed
determine which value is the entry value
Bas Niekel
committed

Commits on May 8, 2026

fixed smv generation to expect later slots empty
Bas Niekel
committed

Commits on May 9, 2026

Merge branch 'main' into invariant7
Bas Niekel
committed

Commits on May 11, 2026

cleanup of debug logs, cleanup and verification of smv output
Bas Niekel
committed
json using updated json
Bas Niekel
committed
annotate invariant 8
Bas Niekel
committed
invariant to smv
Bas Niekel
committed
fixed some bugs with json parsing of invariant
Bas Niekel
committed
removed git merge conflict
Bas Niekel
committed
fixed json, verification of invariant 8
Bas Niekel
committed