Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Remove etcb_at #838

Open
corlewis opened this issue Dec 12, 2024 · 0 comments
Open

Remove etcb_at #838

corlewis opened this issue Dec 12, 2024 · 0 comments
Labels

Comments

@corlewis
Copy link
Member

After adjusting the det_ext state as part of #824, we no longer needed the ekheap and it was removed. To minimise the disruption to existing proofs, the etcbs_of projection and etcb_at predicate were redefined to be on top of kheap (see https://github.com/corlewis/l4v/blob/1e732c8e3156eff3147ec165293d7aa7b8a66de7/proof/invariant-abstract/DetSchedInvs_AI.thy#L39). However, while it seems reasonable to keep a version of etcbs_of, etcb_at is equivalent to tcb_at and should be removed.

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

1 participant