Repository navigation

Proof of a custom mutex implementation. - #160

Closed

dkxb wants to merge 16 commits into

paolo/atomic-specsfrom

Closed

Proof of a custom mutex implementation.#160
dkxb wants to merge 16 commits into
paolo/atomic-specsfrom
ke/mutex_impl

Commits on Sep 1, 2026
- [mutex.v]: change token to user; comment out with_RepFor section
  
  dkxb
  authored and
  pgiarrusso-sl
  committed
  8129f5e
- replace appearance of mutex.token to user
  
  dkxb
  authored and
  pgiarrusso-sl
  committed
  c14bc58
- check in layout of a custom mutex proof
  
  dkxb
  authored and
  pgiarrusso-sl
  committed
  2588395
- [custom_mutex_hpp_proof.v] add do_lock lemma statement
  
  dkxb
  authored and
  pgiarrusso-sl
  committed
  441bd7d
- Tweak spec and client proof
  pgiarrusso-sl
  committed
  3120853
- Drop trailing whitespace
  pgiarrusso-sl
  committed
  5c0b508
- cleanups
  pgiarrusso-sl
  committed
  9f95718
- Fix parentheses in Rep
  pgiarrusso-sl
  committed
  9e6b955
- custom_mutex: atomic<bool> -> atomic<int>
  pgiarrusso-sl
  committed
  f34aa7c
- Proof sketch
  pgiarrusso-sl
  committed
  bfc0f31
- progress on custom mutex proof
  dkxb
  committed
  13f1a01
Commits on Sep 2, 2026
- custom mutex proof mostly done
  dkxb
  committed
  e7f35d7
- Import linearity, drop unused lemmas
  pgiarrusso-sl
  committed
  7b078ec
- Proof tweaks
  pgiarrusso-sl
  committed
  3ffdfb3
- More proof tweaks
  pgiarrusso-sl
  committed
  c5aec84
Commits on Sep 4, 2026
- Spec tweaks
  pgiarrusso-sl
  committed
  6a75fb6