def
Mt.System.Traced.instIsReservationReservation
{spec : Mt.Spec}
:
Mt.IsReservation spec.Reservation
Equations
- Mt.System.Traced.instIsReservationReservation = spec.is_reservation
def
Mt.System.Traced.sum_reservations
{spec : Mt.Spec}
(l : List (Mt.Traced.TracedThread spec))
:
spec.Reservation
Equations
- Mt.System.Traced.sum_reservations l = List.foldl (fun env_r thread => env_r + thread.reservation) Mt.IsReservation.empty l
theorem
Mt.System.Traced.sum_reservations.helper
{spec : Mt.Spec}
(head : Mt.Traced.TracedThread spec)
(l : List (Mt.Traced.TracedThread spec))
:
Mt.System.Traced.sum_reservations (head :: l) = head.reservation + Mt.System.Traced.sum_reservations l
theorem
Mt.System.Traced.sum_reservations.helper.add
{spec : Mt.Spec}
(r : spec.Reservation)
(head : Mt.Traced.TracedThread spec)
(tail : List (Mt.Traced.TracedThread spec))
:
Mt.System.Traced.sum_reservations' r (head :: tail) = Mt.System.Traced.sum_reservations' (r + head.reservation) tail
theorem
Mt.System.Traced.sum_reservations.helper.assoc
{spec : Mt.Spec}
(r : spec.Reservation)
(l : List (Mt.Traced.TracedThread spec))
:
Mt.System.Traced.sum_reservations' r l = r + Mt.System.Traced.sum_reservations' Mt.IsReservation.empty l
theorem
Mt.System.Traced.decompose_reservation
{spec : Mt.Spec}
(l : List (Mt.Traced.TracedThread spec))
(idx : Fin (List.length l))
(t : Mt.Traced.TracedThread spec)
:
t = List.get l idx →
Mt.System.Traced.sum_reservations l = Mt.System.Traced.sum_reservations (List.eraseIdx l idx.val) + t.reservation