Port more service and completion facts

Here are a couple more service and completion facts. Sergey, please review.

CC: @sbozhko

added 3 commits

• c147ae4b - port cumulative_service_implies_scheduled
• 714944fe - port service_is_a_step_function
• 92d3838c - port only_one_job_scheduled for the ideal schedule

Compare with previous version

added 2 commits

• 0fc63758 - make processor state instances global and transparent
• 2706335e - port only_one_job_scheduled for the ideal schedule

Compare with previous version

added 2 commits

• 83294a3f - Re-organize facts layout
• 3d0a1d46 - make all behavioral facts available as rt.behavior.facts.all.

Compare with previous version

Please note that I reorganized the 'facts' files: they are now in behavior/facts/ to avoid cluttering up the spec. I've also created a file behavior/facts/all.v for easy import.

Since the reorganization might be interesting to all: CC @mlesourd @sophie

added 1 commit

• af3c44b8 - move fact about ideal schedules to proper file

Compare with previous version

added 3 commits

• 8dc21345 - add helper lemmas about zero sums
• 4ef667dc - add some helper lemmas on guaranteed service
• 5f8de108 - port same_service_implies_scheduled_at_earlier_times

Compare with previous version

added 2 commits

• f4a6a66c - remove stray 'Search' from proof script
• 51a4e572 - port scheduler_executes_job_with_earliest_arrival

Compare with previous version

With the latest push, I've finished porting all lemmas from model/schedule/uni/schedule.v. Unless there are any objections, I'd like to merge this.

added 1 commit

• 753bc26a - fix spacing

Compare with previous version

added 1 commit

• 0f55c2e9 - fix stray TAB character

Compare with previous version

added 11 commits

• 9e04d483 - port service_is_a_step_function
• 7ce22bb3 - make processor state instances global and transparent
• 2be29bdb - port only_one_job_scheduled for the ideal schedule
• 0dfa8477 - Re-organize facts layout
• 1472b91e - make all behavioral facts available as rt.behavior.facts.all.
• 05bdd805 - move fact about ideal schedules to proper file
• 04eb8be5 - add helper lemmas about zero sums
• db1cd908 - add some helper lemmas on guaranteed service
• a0c1a71e - port same_service_implies_scheduled_at_earlier_times
• 99849914 - port scheduler_executes_job_with_earliest_arrival
• ae0f9ce0 - fix indentation

Compare with previous version

resolved all discussions

added 9 commits

• 1f6c31c0 - add helper lemmas about zero sums
• 601cc94a - expand on the relation of service to scheduled_at
• 7ba40605 - Port lemmas from model/schedule/uni/schedule.v
• 8915b81d - make processor state instances global and transparent
• ca7d8ed3 - Re-organize facts layout
• fa44871c - make all behavioral facts available as rt.behavior.facts.all.
• 2d5026a8 - port same_service_implies_scheduled_at_earlier_times
• 780f7045 - port only_one_job_scheduled for the ideal schedule
• bd5383a1 - port scheduler_executes_job_with_earliest_arrival

Compare with previous version

merged