PROSA v0.6: The aRSA Edition


Tested with Rocq 9.0.0, mathcomp 2.4.0, and mczify 1.5.0.

Update POET's support code to match the newer aRTA blocking bound

Add periodic task model

Formalization of Weakly Sustainable Policy

1) Formalize the notion of weakly sustainable policy, along with
its contrapositive, and prove the equivalence between the two.

2) Establish weak sustainability of self-suspending tasks w.r.t.
execution times and variable suspension times, based on the
transformation we had formalized.

Remove LoadPath from util/all.v

Replace nat with time + clean-up code