6 commits

Author	SHA1	Message	Date
Tobias Reinhard	fe5612cf4f	Extended lock invariants to justify safe access to ready tasks as well as scheduled task.	2022-11-30 15:52:00 -05:00
Tobias Reinhard	28fb658a59	Proved last case in lemma DLS_open_2. Will need to revisit once the lemma's postcondition has been strengtened.	2022-11-27 09:29:17 -05:00
Tobias Reinhard	53189c46d4	Added new version of DLS opening lemma that reduces case splits in DLS proofs. Proved 3/4 of it.	2022-11-26 12:15:34 -05:00
Tobias Reinhard	be9de4d570	Added lemma DLS_nonEndItem_next_close to help closing DLS opened with DLS_nonEndItem_next_open.	2022-11-23 11:28:27 -05:00
Tobias Reinhard	9e3ea9016e	Added lemma DLS_end_next_close to help closing DLS opened with DLS_end_next_open	2022-11-23 08:31:07 -05:00
Tobias Reinhard	f7e537a19f	Restructured proof. ... New proof opens the DLS predicate to justify accesses to `pxTaskItem->next` and proves that `pxTaskItem->next` points to a valid list item.	2022-11-22 10:10:41 -05:00