add definition of a job's (precise) finish time

This small MR defines the notion of a job's "finish time". To get around the problem that a job may never finish, we reuse ssreflect's ex_minn facility to define finish_time under the assumption that the job eventually finishes.

This has no immediate users. The main point is to show that it can be done (and as an example for Lars).

Rendered spec: https://prosa.mpi-sws.org/branches/wip-finish-time/pretty/prosa.analysis.definitions.finish_time.html

requested review from @kbedarka

assigned to @bbb

added 1 commit

• 260faaea - to squash: one more corollary

Compare with previous version

changed the description

approved this merge request

added 1 commit

• d907c61a - fix comment

Compare with previous version

added 1 commit

• 1d1fe891 - fix comment

Compare with previous version

changed the description

added 2 commits

• ad62e9b8 - fix `t = 0` corner case in definition of `completes_at`
• 319404c2 - fixup finish_time proof to match changed `completes_at` definition

Compare with previous version

added 2 commits

• 00a1ec28 - fix `t = 0` cornercase in definition of `completes_at`
• d5f22a4e - add definition of a job's (precise) finish time

Compare with previous version

merged