ink

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

Equations

• Mt.System.instIsReservationReservation = spec.is_reservation

ink

def Mt.System.valid {spec : Mt.Spec} (s : Mt.System spec) : Prop

Central validation predicate for reasoning about systems.

A valid system has the following property: Given any future iteration of the system (or the system itself), the following holds:

• No threads have panicked yet (and they never will)
• Its current state is valid according to the specification

Equations

• Mt.System.valid s = ∀ (s' : Mt.System spec), Mt.System.reduces_to_or_eq s s' → s'.panics = 0 ∧ ∃ r, Mt.Spec.validate spec r s'.state

ink

theorem Mt.System.fundamental_validation_theorem {spec : Mt.Spec} (s : Mt.System spec) (no_panics_yet : s.panics = 0) (initial_valid : Mt.Spec.validate spec Mt.IsReservation.empty s.state) (threads_valid : ∀ (t : Mt.Thread spec), t ∈ s.threads → Mt.Thread.valid t) : Mt.System.valid s