New ghost state for mutex spec & implementation; give up `user` ghost state. - #173

Draft

dkxb wants to merge 47 commits into

mainfrom

Commits on Sep 10, 2026

Copy snapshot of atomic specs
pgiarrusso-sl
committed
83756a2
Notation -> Abbreviation
pgiarrusso-sl
committed
3e1ce8c
Spec: add missing modes
pgiarrusso-sl
committed
06eeefa
Add UnOp instance for num ++
pgiarrusso-sl
committed
9fd1809
TMP build rules (to redo)
pgiarrusso-sl
committed
779b857
tweak
pgiarrusso-sl
committed
97a7931
Remove __1
pgiarrusso-sl
committed
d086280
TMP for move from tests
pgiarrusso-sl
committed
7468a36
WIP on merging base classes
pgiarrusso-sl
committed
0c3d6a0
test_cpp_proof: adapt to alternative implementation
pgiarrusso-sl
committed
b07bed7
Disable pointer tests
pgiarrusso-sl
committed
60f6bd7
WIP on thread id
pgiarrusso-sl
committed
2360d14
atomic: fix namespacing
pgiarrusso-sl
committed
e2e5e34
WIP on thread_id proofs
pgiarrusso-sl
committed
d17add6
[mutex.v]: change token to user; comment out with_RepFor section

dkxb
authored and
pgiarrusso-sl
committed
c328fe8
replace appearance of mutex.token to user

dkxb
authored and
pgiarrusso-sl
committed
462cb75
check in layout of a custom mutex proof

dkxb
authored and
pgiarrusso-sl
committed
bcb91f7
[custom_mutex_hpp_proof.v] add do_lock lemma statement

dkxb
authored and
pgiarrusso-sl
committed
af6eb73
Tweak spec and client proof
pgiarrusso-sl
committed
41318df
Drop trailing whitespace
pgiarrusso-sl
committed
2e24af5
cleanups
pgiarrusso-sl
committed
18d609b
Fix parentheses in Rep
pgiarrusso-sl
committed
a4e43a3
custom_mutex: atomic<bool> -> atomic<int>
pgiarrusso-sl
committed
65013f9
Proof sketch
pgiarrusso-sl
committed
0e35894
progress on custom mutex proof

dkxb
authored and
pgiarrusso-sl
committed
9b60f53
custom mutex proof mostly done

dkxb
authored and
pgiarrusso-sl
committed
ff74e69
Import linearity, drop unused lemmas
pgiarrusso-sl
committed
8392c6c
Proof tweaks
pgiarrusso-sl
committed
acf9463
More proof tweaks
pgiarrusso-sl
committed
9e975fe
Spec tweaks
pgiarrusso-sl
committed
930e3ba
change mutex to use a fractional used_threads and another separate piece of exclusive my_mutex

dkxb
authored and
pgiarrusso-sl
committed
deda9a6
mutex proof WIP

dkxb
authored and
pgiarrusso-sl
committed
41dbfb3
complete mutex ghost refactor

dkxb
authored and
pgiarrusso-sl
committed
213bfc7
refactor mutex specs, std::mutex and custom mutex are both implemntation

dkxb
authored and
pgiarrusso-sl
committed
ec5892b
better model for my_mutex, all properties described in MUTEX_SETS

dkxb
authored and
pgiarrusso-sl
committed
1c16450
mutex ghost state module instantiation is now associated with implementation proof

dkxb
authored and
pgiarrusso-sl
committed
04bf5ed
rename MUTEX_STATE to MUTEX_PREDS

dkxb
authored and
pgiarrusso-sl
committed
1711628
code clean up

dkxb
authored and
pgiarrusso-sl
committed
8020b9b
more clean up

dkxb
authored and
pgiarrusso-sl
committed
8182147
add instances to MUTEX_PREDS

dkxb
authored and
pgiarrusso-sl
committed
0d81ece
add comments

dkxb
authored and
pgiarrusso-sl
committed
250308e

Commits on Sep 17, 2026