ink

structure Mt.Thread (spec : Mt.Spec) : Type 1

• T : Type
• block_until : spec.State → Bool
• task : Mt.TaskM spec T

A single thread of the system. It consists of a task to execute and a blocking predicate. The system only iterates a thread if the blocking predicate holds

ink

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

Equations

• Mt.instIsReservationReservation = spec.is_reservation

ink

def Mt.mk_thread {spec : Mt.Spec} {T : Type} (task : Mt.TaskM spec T) : Mt.Thread spec

Equations

• Mt.mk_thread task = { T := T, block_until := fun x => true, task := task }

ink

inductive Mt.Thread.IterationResult (spec : Mt.Spec) : Type 1

• Done: {spec : Mt.Spec} → spec.State → Mt.Thread.IterationResult spec
• Panic: {spec : Mt.Spec} → spec.State → Mt.Thread.IterationResult spec
• Running: {spec : Mt.Spec} → spec.State → Mt.Thread spec → Mt.Thread.IterationResult spec

ink

def Mt.Thread.IterationResult.state {spec : Mt.Spec} : Mt.Thread.IterationResult spec → spec.State

Equations

• One or more equations did not get rendered due to their size.

ink

def Mt.Thread.iterate {spec : Mt.Spec} : Mt.Thread spec → spec.State → Mt.Thread.IterationResult spec

ink

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

Small wrapper around TaskM.valid. A thread is considered valid if its underlying task is valid and ensures that it drops its reservation in the end.

To prove Thread.valid, you should unfold Thread.valid, for example using rw [Thread.valid] and continue applying the validation theoreoms for TaskM.valid, like TaskM.valid_bind

Equations

• Mt.Thread.valid thread = Mt.TaskM.valid thread.task Mt.IsReservation.empty thread.block_until fun x r => r = Mt.IsReservation.empty