ink

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

Equations

• Mt.instIsReservationReservation_1 = spec.is_reservation

ink

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

• state : spec.State
• threads : List (Mt.Thread spec)
• panics : Nat

Describes a system of zero or more threads running in parallel

Systems can be iterated one atomic step at a time by choosing one of its threads. They keep track of the number of threads which panicked during execution

ink

def Mt.System.ThreadIndex {spec : Mt.Spec} (s : Mt.System spec) : Type

Equations

• Mt.System.ThreadIndex s = Fin (List.length s.threads)

ink

def Mt.System.done {spec : Mt.Spec} (s : Mt.System spec) : Bool

Equations

• Mt.System.done s = decide (List.length s.threads = 0)

ink

def Mt.System.iterate {spec : Mt.Spec} (s : Mt.System spec) : Mt.System.ThreadIndex s → Mt.System spec

Equations

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

ink

theorem Mt.System.iterate_threads {spec : Mt.Spec} (s : Mt.System spec) (thread_idx : Mt.System.ThreadIndex s) (blocked_until : Mt.Thread.block_until (List.get s.threads thread_idx) s.state = true) : (Mt.System.iterate s thread_idx).threads = let _discr := Mt.Thread.iterate (List.get s.threads thread_idx) s.state; match Mt.Thread.iterate (List.get s.threads thread_idx) s.state with | Mt.Thread.IterationResult.Done a => List.eraseIdx s.threads thread_idx.val | Mt.Thread.IterationResult.Panic a => List.eraseIdx s.threads thread_idx.val | Mt.Thread.IterationResult.Running a thread => List.set s.threads thread_idx.val thread

ink

theorem Mt.System.iterate_panics {spec : Mt.Spec} (s : Mt.System spec) (thread_idx : Mt.System.ThreadIndex s) (blocked_until : Mt.Thread.block_until (List.get s.threads thread_idx) s.state = true) : (Mt.System.iterate s thread_idx).panics = let _discr := Mt.Thread.iterate (List.get s.threads thread_idx) s.state; match Mt.Thread.iterate (List.get s.threads thread_idx) s.state with | Mt.Thread.IterationResult.Done a => s.panics | Mt.Thread.IterationResult.Panic a => s.panics + 1 | Mt.Thread.IterationResult.Running a a_1 => s.panics

ink

inductive Mt.System.reduces_to {spec : Mt.Spec} : Mt.System spec → Mt.System spec → Prop

• single: ∀ {spec : Mt.Spec} {a b : Mt.System spec} (idx : Mt.System.ThreadIndex a), Mt.System.iterate a idx = b → Mt.System.reduces_to a b
• trans: ∀ {spec : Mt.Spec} {a b c : Mt.System spec}, Mt.System.reduces_to a b → Mt.System.reduces_to b c → Mt.System.reduces_to a c

ink

def Mt.System.reduces_to_or_eq {spec : Mt.Spec} (a : Mt.System spec) (b : Mt.System spec) : Prop

Equations

• Mt.System.reduces_to_or_eq a b = (a = b ∨ Mt.System.reduces_to a b)

ink

theorem Mt.System.reduces_to_or_eq.refl {spec : Mt.Spec} (a : Mt.System spec) : Mt.System.reduces_to_or_eq a a

ink

theorem Mt.System.reduces_to_or_eq.trans {spec : Mt.Spec} {a : Mt.System spec} {b : Mt.System spec} {c : Mt.System spec} : Mt.System.reduces_to_or_eq a b → Mt.System.reduces_to_or_eq b c → Mt.System.reduces_to_or_eq a c