ink

structure Mt.Traced.TracedThread (spec : Mt.Spec) : Type 1

• thread : Mt.Thread spec
• reservation : spec.Reservation

ink

def Mt.Traced.instIsReservationReservation {spec : Mt.Spec} : Mt.IsReservation spec.Reservation

Equations

• Mt.Traced.instIsReservationReservation = spec.is_reservation

ink

def Mt.Traced.TracedThread.T {spec : Mt.Spec} (t : Mt.Traced.TracedThread spec) : Type

Equations

• Mt.Traced.TracedThread.T t = t.thread.T

ink

def Mt.Traced.TracedThread.block_until {spec : Mt.Spec} (t : Mt.Traced.TracedThread spec) : spec.State → Bool

Equations

• Mt.Traced.TracedThread.block_until t = t.thread.block_until

ink

def Mt.Traced.TracedThread.task {spec : Mt.Spec} (t : Mt.Traced.TracedThread spec) : Mt.TaskM spec (Mt.Traced.TracedThread.T t)

Equations

• Mt.Traced.TracedThread.task t = t.thread.task

ink

def Mt.Traced.TracedThread.iterate {spec : Mt.Spec} (t : Mt.Traced.TracedThread spec) : spec.State → Mt.Thread.IterationResult spec

Equations

• Mt.Traced.TracedThread.iterate t = Mt.Thread.iterate t.thread

ink

def Mt.Traced.TracedThread.valid {spec : Mt.Spec} (thread : Mt.Traced.TracedThread spec) : Prop

Equations

• Mt.Traced.TracedThread.valid thread = Mt.TaskM.valid thread.thread.task thread.reservation thread.thread.block_until fun x r => r = Mt.IsReservation.empty

ink

theorem Mt.Traced.TracedThread.valid_elim {spec : Mt.Spec} {thread : Mt.Traced.TracedThread spec} (is_valid : Mt.Traced.TracedThread.valid thread) (env_r : spec.Reservation) (s : spec.State) : Mt.Traced.TracedThread.block_until thread s = true → Mt.Spec.validate spec (env_r + thread.reservation) s → ∃ r', let _discr := Mt.Traced.TracedThread.iterate thread s; match Mt.Traced.TracedThread.iterate thread s with | Mt.Thread.IterationResult.Done s' => Mt.Spec.validate spec (env_r + r') s' ∧ r' = Mt.IsReservation.empty | Mt.Thread.IterationResult.Panic a => False | Mt.Thread.IterationResult.Running s' cont => Mt.Spec.validate spec (env_r + r') s' ∧ Mt.Traced.TracedThread.valid { thread := cont, reservation := r' }