You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
The rt branch has had the same changes made to the det_ext state and etcbs_of and etcb_at, so if this is done it should be done on both branches for consistency.
The text was updated successfully, but these errors were encountered:
After adjusting the
det_ext
state as part of #824, we no longer needed theekheap
and it was removed. To minimise the disruption to existing proofs, theetcbs_of
projection andetcb_at
predicate were redefined to be on top ofkheap
(see https://github.com/corlewis/l4v/blob/1e732c8e3156eff3147ec165293d7aa7b8a66de7/proof/invariant-abstract/DetSchedInvs_AI.thy#L39). However, while it seems reasonable to keep a version ofetcbs_of
,etcb_at
is equivalent totcb_at
and should be removed.The
rt
branch has had the same changes made to thedet_ext
state andetcbs_of
andetcb_at
, so if this is done it should be done on both branches for consistency.The text was updated successfully, but these errors were encountered: