Preemption model compliance

In this MR, we prove that the ideal uniprocessor schedules that are implemented in prosa.implementation.definitions.ideal_uni_scheduler respect the preemption model.

Hi Laila, is this ready for review?

mentioned in merge request !111 (merged)

mentioned in merge request !117 (merged)

Hi Laila, when you get a chance, please rebase on top of the latest master version. The proof-state collector patches have already gone in as part of !117 (merged).

As Laila has disappeared, we'll have to help this MR over the final hump sooner or later. I don't want to lose the work, so the MR should go in in revised form before the main branch diverges too much.

I'm taking a stab at this.

added 23 commits

• dae7b9fe...271464a5 - 19 commits from branch RT-PROOFS:master
• 1a52af28 - added the np_respect_preemption_model lemma
• 8b22505b - extract schedule_up_to_identical_prefix corollary for reuse
• a76ae969 - polish prosa.implementation.facts.ideal_uni.prio_aware
• f3039ae5 - polish prosa.implementation.facts.ideal_uni.preemption_aware

Compare with previous version

resolved all threads

Ok, done with the first iteration. @mmaida @sbozhko — please review.

added 3 commits

• 6b15dbb0 - Now -> by
• 35ed3fa3 - Shortened, restructured, polished proofs
• 1fb9e77a - Removed empty lines causing some error in the spell check

Compare with previous version

Thank you, Marco.

Looks good to me. I left only two very minor comments (that can be ignored)

resolved all threads

added 1 commit

• 7846744b - Polish

Compare with previous version

resolved all threads

merged