Documentation

Mt.System.Traced

structure Mt.Traced.TracedSystem (spec : Mt.Spec) :

Type 1

state : spec.State
threads : List (Mt.Traced.TracedThread spec)

Instances For

def Mt.Traced.TracedSystem.instIsReservationReservation {spec : Mt.Spec} :

Mt.IsReservation spec.Reservation

Equations

Mt.Traced.TracedSystem.instIsReservationReservation = spec.is_reservation

def Mt.Traced.TracedSystem.ThreadIndex {spec : Mt.Spec} (s : Mt.Traced.TracedSystem spec) :

Type

Equations

Mt.Traced.TracedSystem.ThreadIndex s = Fin (List.length s.threads)

def Mt.Traced.TracedSystem.done {spec : Mt.Spec} (s : Mt.Traced.TracedSystem spec) :

Equations

Mt.Traced.TracedSystem.done s = decide (List.length s.threads = 0)

def Mt.Traced.TracedSystem.iterate {spec : Mt.Spec} (s : Mt.Traced.TracedSystem spec) (idx : Mt.Traced.TracedSystem.ThreadIndex s) :

Mt.Thread.IterationResult spec

Equations

Mt.Traced.TracedSystem.iterate s idx = Mt.Traced.TracedThread.iterate (List.get s.threads idx) s.state

def Mt.Traced.TracedSystem.update_thread {spec : Mt.Spec} (s : Mt.Traced.TracedSystem spec) (idx : Nat) (state : spec.State) (r : spec.Reservation) (cont : Mt.Thread spec) :

Mt.Traced.TracedSystem spec

Equations

Mt.Traced.TracedSystem.update_thread s idx state r cont = { state := state, threads := List.set s.threads idx { thread := cont, reservation := r } }

def Mt.Traced.TracedSystem.remove_thread {spec : Mt.Spec} (s : Mt.Traced.TracedSystem spec) (idx : Nat) (state : spec.State) :

Mt.Traced.TracedSystem spec

Equations

Mt.Traced.TracedSystem.remove_thread s idx state = { state := state, threads := List.eraseIdx s.threads idx }

def Mt.Traced.TracedSystem.reservations {spec : Mt.Spec} (s : Mt.Traced.TracedSystem spec) :

spec.Reservation

Equations

Mt.Traced.TracedSystem.reservations s = List.foldl (fun env_r thread => env_r + thread.reservation) Mt.IsReservation.empty s.threads

def Mt.Traced.TracedSystem.other_reservations {spec : Mt.Spec} (s : Mt.Traced.TracedSystem spec) (idx : Nat) :

spec.Reservation

Equations

Mt.Traced.TracedSystem.other_reservations s idx = List.foldl (fun env_r thread => env_r + thread.reservation) Mt.IsReservation.empty (List.eraseIdx s.threads idx)

theorem Mt.Traced.TracedSystem.decompose_reservations {spec : Mt.Spec} (s : Mt.Traced.TracedSystem spec) (idx : Mt.Traced.TracedSystem.ThreadIndex s) :

Mt.Traced.TracedSystem.reservations s = Mt.Traced.TracedSystem.other_reservations s idx.val + (List.get s.threads idx).reservation

structure Mt.Traced.TracedSystem.valid {spec : Mt.Spec} (s : Mt.Traced.TracedSystem spec) :

Prop

currently_valid : Mt.Spec.validate spec (Mt.Traced.TracedSystem.reservations s) s.state
threads_valid : ∀ (t : Mt.Traced.TracedThread spec), t ∈ s.threads → Mt.Traced.TracedThread.valid t

Instances For

def Mt.Traced.TracedSystem.to_system {spec : Mt.Spec} (s : Mt.Traced.TracedSystem spec) :

Equations

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

def Mt.Traced.TracedSystem.mk_initial {spec : Mt.Spec} (s : Mt.System spec) :

Mt.Traced.TracedSystem spec

Equations

Mt.Traced.TracedSystem.mk_initial s = { state := s.state, threads := List.map (fun t => { thread := t, reservation := Mt.IsReservation.empty }) s.threads }

theorem Mt.Traced.TracedSystem.mk_initial.valid {spec : Mt.Spec} (s : Mt.System spec) (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.Traced.TracedSystem.valid (Mt.Traced.TracedSystem.mk_initial s)

theorem Mt.Traced.TracedSystem.mk_initial.cancels_to_system {spec : Mt.Spec} {s : Mt.System spec} (no_panics_yet : s.panics = 0) :

Mt.Traced.TracedSystem.to_system (Mt.Traced.TracedSystem.mk_initial s) = s

theorem Mt.Traced.TracedSystem.valid_by_iteration {spec : Mt.Spec} (s : Mt.System spec) (s' : Mt.System spec) {idx : Mt.System.ThreadIndex s} {ts : Mt.Traced.TracedSystem spec} (has_traced_system : s = Mt.Traced.TracedSystem.to_system ts) (ts_valid : Mt.Traced.TracedSystem.valid ts) (iteration : Mt.System.iterate s idx = s') :

∃ ts', Mt.Traced.TracedSystem.to_system ts' = s' ∧ Mt.Traced.TracedSystem.valid ts'