Equations
- SampleMutex.Data.valid _fun_discr = match _fun_discr with | { x := x, y := y } => x = y
@[inline]
Equations
- unlocked: ∀ {data : SampleMutex.Data}, SampleMutex.Data.valid data → SampleMutex.validate Mt.Lock.Unlocked { data := data, locked := false }
- locked: ∀ (data : SampleMutex.Data), SampleMutex.validate (Mt.Lock.Locked data) { data := data, locked := true }
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
theorem
SampleMutex.validate.elim_unlocked
{r : SampleMutex.Reservation}
{s : SampleMutex.State}
:
SampleMutex.validate r s → s.locked = false → r = Mt.Lock.Unlocked ∧ SampleMutex.Data.valid s.data
theorem
SampleMutex.validate.elim_locked
{env_r : SampleMutex.Reservation}
{d : SampleMutex.Data}
{s' : SampleMutex.State}
:
SampleMutex.validate (env_r + Mt.Lock.Locked d) s' → env_r = Mt.Lock.Unlocked ∧ d = s'.data ∧ s'.locked = true
theorem
SampleMutex.valid_bind_mutex_lock
{T : Type}
{cont : Mt.TaskM SampleMutex.spec T}
{assuming : SampleMutex.spec.State → Bool}
{motive : T → SampleMutex.spec.Reservation → Prop}
(cont_valid : ∀ (x : Nat), Mt.TaskM.valid cont (Mt.Lock.Locked { x := x, y := x }) (fun x => true) motive)
:
Mt.TaskM.valid
(do
Mt.TaskM.atomic_blocking_rmr
(fun x =>
match x with
| { data := data, locked := locked } => decide (locked = false))
fun s => (PUnit.unit, { data := s.data, locked := true })
cont)
Mt.Lock.Unlocked assuming motive
theorem
SampleMutex.valid_mutex_release
{assuming : SampleMutex.spec.State → Bool}
{data : SampleMutex.Data}
(data_valid : SampleMutex.Data.valid data)
:
Mt.TaskM.valid (Mt.TaskM.atomic_read_modify fun s => { data := s.data, locked := false }) (Mt.Lock.Locked data) assuming
fun x r => r = Mt.Lock.Unlocked