Introduce restricted-supply abstract RTA

Depends on !311 (merged), !312 (merged), !314 (merged), !317 (merged)

assigned to @sbozhko

Final fixpoint for restricted-supply aRTA will be the following:

• local_IBF upper-bounds the amount of interference "inside a reservation." In this case, this is just higher-priority jobs.
• SBF is supply-bound function, a lower bound on the amount of supply in a given interval.

    Variable R : duration.
    Hypothesis H_R_is_maximum_rs :
      forall (A : duration),
        is_in_search_space_rs A ->
        exists (F : duration),
          task_rtct tsk + local_IBF tsk A F <= SBF F /\
          SBF F + (task_cost tsk - task_rtct tsk) <= SBF (A + R).

@bbb, @kbedarka, your opinion?

(maybe) unimportant technicality

currently the fixpoint is in this state, but I believe it can be transformed into the claimed one

    Variable R : duration.
    Hypothesis H_R_is_maximum_rs:
      forall (A : duration),
        is_in_search_space_rs A ->
        exists (F : duration),
          task_rtct tsk + (F - SBF F) + local_IBF tsk A F <= F /\
          F + (task_cost tsk - task_rtct tsk) + ((A+R - SBF (A + R)) - (F - SBF F)) <= A + R.

added 25 commits

• 0b8d8d31...2545ffb9 - 5 commits from branch RT-PROOFS:master
• 80d9aa4a - improve tactics
• e14685ff - improve tabulation and comments
• 05a47c22 - optimize imports
• 25459a19 - add reflection for negated priority inversion
• 0f7c4953 - replace [intros] with [move]
• 492aacc1 - add lemmas about job relations
• 3359e16e - generalize abstract RTA
• 887ca787 - [to squash] delete trailing whitespace
• 5f87c743 - [to squash]: apply Björn's suggestions
• cae81767 - [to squash] remove a TODO
• cb7fb708 - [to squash] fix outdated reference
• 05699976 - [to squash] apply Björn's suggestions
• 3281768a - [to squash] improve a comment
• a9722f79 - [to squash] improve comments in [abstract/definitions.v]
• 7c1aee85 - [to squash] fix a few more things
• 573c64a8 - [to squash] fix compilation
• 28013ee0 - [to squash] fix typo
• ad5cc6a9 - introduce "absence of speculative execution"
• 6d0fa0f1 - : add notion of service inversion
• fc8335d5 - : add restricted supply

Compare with previous version

added 1 commit

• f044e98d - admit all broken lemmas

Compare with previous version

added 11 commits

• f044e98d...246fba4d - 5 commits from branch RT-PROOFS:master
• 3fa7b87e - define restricted supply processor model
• 886bcf29 - : add notion of service inversion
• ebb68977 - : add restricted supply
• 61aef2cf - : admit all broken lemmas
• f1a71b1b - add definition of absence of speculative execution
• 53457000 - : supply lemmas

Compare with previous version

added 5 commits

• cfee42d5 - [to squash]: add facts about restricted supply
• 484b1dd7 - : add notion of service inversion
• cd1ab7ee - : add restricted supply
• fc5272cb - : admit all broken lemmas
• 257583d1 - add definition of absence of speculative execution

Compare with previous version

added 8 commits

• 19334756 - [to squash]: add Pierre's comments
• 4b4bff3c - [to squash]: fix a typo
• 966026ce - : add notion of service inversion
• a771013d - : add iw inst for rs
• 199d1f7d - : admit all broken lemmas
• 37ca4676 - : add restricted supply
• 8644e976 - : admit all broken lemmas
• e3a851cf - add definition of absence of speculative execution

Compare with previous version

added 13 commits

• e3a851cf...4eececb0 - 2 commits from branch RT-PROOFS:master
• c88bb14c - define restricted supply processor model
• 80c7ee2c - [to squash]: add facts about restricted supply
• 301b11bc - [to squash]: add Pierre's comments
• f18b1413 - [to squash]: fix a typo
• a5121f15 - : add notion of service inversion
• 883941a7 - : add iw inst for rs
• bf90b5f5 - : admit all broken lemmas
• 9f40143e - : add restricted supply
• 1b88c66d - : admit all broken lemmas
• 5fd2b706 - add definition of absence of speculative execution
• 1e4773fd - : fix typo

Compare with previous version

added 8 commits

• 731e35ac - define restricted supply processor model
• 2e26eb23 - : add notion of service inversion
• 41b80a3b - : add iw inst for rs
• 7c077690 - : close proofs
• d077fd73 - : fix typo
• 623848db - : add restricted supply
• f226f5a7 - : admit all broken lemmas
• efde8249 - add definition of absence of speculative execution

Compare with previous version

added 85 commits

• efde8249...42a0a527 - 70 commits from branch RT-PROOFS:master
• 42a0a527...4f623a50 - 5 earlier commits
• 94164bb6 - fix CI (again, yes)
• bee8b1c8 - : add notion of service inversion
• 6fe9b4b5 - : add iw inst for rs
• b0fd5000 - : close proofs
• 39875b84 - : fix typo
• 6acda649 - : add restricted supply
• 7b722b90 - : admit all broken lemmas
• 3c978764 - add definition of absence of speculative execution
• 757ecbfa - fix proc. def
• 13d42e03 - abstract BI

Compare with previous version

added 12 commits

• 13d42e03...dd622279 - 2 earlier commits
• 1f2f4dfd - : add decidable notion of quiet time
• aa7d79cb - : add proof of abstract busy interval's existence
• a8b7326e - : add notion of service inversion
• f9419b47 - : add iw inst for rs
• 7fd2c330 - : close proofs
• 4493b02c - : fix typo
• df113b26 - : add restricted supply
• 17981ede - : admit all broken lemmas
• 979df131 - fix proc. def
• a76127fa - : clean up abstract busy interval

Compare with previous version

added 11 commits

• faa2dc21 - 1 earlier commit
• ceb75039 - define restricted supply processor model
• e0231043 - clean up in [workload.v]
• a2585e44 - define absence of "speculative execution
• a54b768c - : add proof of abstract busy interval's existence
• a94c06a2 - fwef
• e59d055a - : add notion of service inversion
• 02dd2027 - : add iw inst for rs
• 95940527 - : add restricted supply
• 04d2d9b6 - : admit all broken lemmas
• 9c953f12 - : clean up RS-RTA

Compare with previous version

added 1 commit

• 05beab1f - : restructure stuff

Compare with previous version

added 1 commit

• 71657b46 - : make progress

Compare with previous version

added 1 commit

• cc22cefa - : close big lemmas

Compare with previous version

added 17 commits

• cc22cefa...b19b4092 - 4 commits from branch RT-PROOFS:master
• b19b4092...faf4574f - 3 earlier commits
• 6dc6627b - : add proof of abstract busy interval's existence
• 948ace2b - : add notion of service inversion
• 328804f4 - : add iw inst for rs
• 298cfcdd - : add restricted supply
• c7337e21 - : admit all broken lemmas
• 1c8fdc68 - : clean up RS-RTA
• 1a7edea6 - : restructure stuff
• ac3cf482 - : make progress
• 0cd75b74 - : close big lemmas
• b742e91a - close a few small lemmas

Compare with previous version

added 16 commits

• b742e91a...4fd33f6b - 6 earlier commits
• 13623ba1 - : clean up RS-RTA
• 46c0dd29 - : restructure stuff
• 23076056 - : make progress
• e25ef063 - : close big lemmas
• 0e19e39c - close a few small lemmas
• c427cc6e - : add new field to Processor State
• e243bf96 - : finish all lemmas
• c5488636 - : move files
• 93518e7b - : move useless stuff
• 95f8c3d2 - : remove useless lemmas

Compare with previous version

added 10 commits

• 95f8c3d2...90387afb - 3 commits from branch RT-PROOFS:master
• b982bf78 - improve comment
• 3f04dc5c - remove unused import
• a7a840d7 - add notion of supply to processor state
• e4f4806a - improve consistency by adding types
• 4fcb37fa - add useful definitions and lemmas about supply
• 4e7b4aac - add notion of supply bound function (SBF)
• 708ee0ca - : finish all lemmas

Compare with previous version

added 2 commits

• d4721a51 - add notion of supply bound function (SBF)
• 6881a01e - : finish all lemmas

Compare with previous version

added 10 commits

• 6881a01e...93e70f81 - 2 commits from branch RT-PROOFS:master
• 3bdc4daf - improve comment
• fff793ff - remove unused import
• 0b26d12a - add notion of supply to processor state
• e4eaaa39 - improve consistency by adding types
• 7b099b1b - add useful definitions and lemmas about supply
• 99cd0337 - add notion of supply bound function (SBF)
• 12e82449 - : del after merge
• 089d3708 - : finish all lemmas

Compare with previous version