generalize preemption_time and priority-model compliance to any processor model

We've long had an accidental dependence on ideal uniprocessors in the priority-model compliance definitions since they depended on [preemption_time], which in turn simply destructured the ideal uniprocessor state. This is a very unfortunate limitation that is increasingly getting in the way. This patch series lifts it.

Closes: #76 (closed)

requested review from @proux1

assigned to @bbb

added 1 commit

• e7ea95bc - fixup: slightly shorten long proof now triggering CI length check

Compare with previous version

added 3 commits

• 460e9d6b - fix fallout from `preemption_time` generalization
• 48f9065a - remove ideal uniproc. model from priority facts
• 03542173 - remove ideal uni-processor assumption from task_schedule.v

Compare with previous version

Only reviewed the first two commits. Mostly nitpicking except maybe the question about arrivals_up_to

LGTM, great job!

approved this merge request

approved this merge request

added 3 commits

• 07979c45 - fixup facts/model/scheduled.v
• ec2529b4 - fixup shave off a few lines in iw_instantiation.v
• 73bb38ae - Makefile: add 'make proof-length'

Compare with previous version

added 4 commits

• 1ee334d6 - Makefile: add 'make proof-length'
• d8c06273 - introduce a generic notion of scheduled job(s)
• 7c8a1720 - relate ideal uniprocessor to `scheduled_job_at`
• 3a4bad28 - generalize a number of core definitions and facts

Compare with previous version

resolved all threads

added 1 commit

• 1b2552ce - generalize a number of core definitions and facts

Compare with previous version

enabled an automatic merge when the pipeline for 1b2552ce succeeds

merged

mentioned in commit 4a875f13

mentioned in merge request !289 (merged)

mentioned in commit eebdd8c8

mentioned in commit e476cf3a

mentioned in commit 51770d6e