Move "classic" Prosa to rt.classic namespace and update documentation

As a first step towards completing #53 (closed) and #54 (closed), this MR moves the "old" Prosa to the rt.classic namespace and updates the documentation to reflect the "modern" Prosa.

scripts/known-long-proofs.json

@@ -2,13 +2,13 @@
     "manual_exceptions": {
     },
     "legacy_proofs": {
-        "./analysis/apa/bertogna_edf_comp.v": {
+        "./classic/analysis/apa/bertogna_edf_comp.v": {
             "bertogna_edf_comp_f_increases": 53,
             "bertogna_edf_comp_iteration_preserves_order": 159,
             "bertogna_edf_comp_rt_grows_too_much": 99,
             "edf_claimed_bounds_finds_fixed_point_of_list": 76
         },
-        "./analysis/apa/bertogna_edf_theory.v": {
+        "./classic/analysis/apa/bertogna_edf_theory.v": {
             "bertogna_cirinei_response_time_bound_edf": 49,
             "bertogna_edf_all_cpus_in_affinity_busy": 52,
             "bertogna_edf_all_cpus_in_subaffinity_busy": 51,
@@ -17,10 +17,10 @@
             "bertogna_edf_interference_in_non_full_processors": 133,
             "bertogna_edf_sum_exceeds_total_interference": 43
         },
-        "./analysis/apa/bertogna_fp_comp.v": {
+        "./classic/analysis/apa/bertogna_fp_comp.v": {
             "fp_analysis_yields_response_time_bounds": 107
         },
-        "./analysis/apa/bertogna_fp_theory.v": {
+        "./classic/analysis/apa/bertogna_fp_theory.v": {
             "bertogna_cirinei_response_time_bound_fp": 47,
             "bertogna_fp_all_cpus_in_affinity_busy": 54,
             "bertogna_fp_all_cpus_in_subaffinity_busy": 53,
@@ -30,128 +30,128 @@
             "bertogna_fp_sum_exceeds_total_interference": 42,
             "bertogna_fp_workload_bounds_interference": 44
         },
-        "./analysis/apa/interference_bound_edf.v": {
+        "./classic/analysis/apa/interference_bound_edf.v": {
             "interference_bound_edf_holds_for_single_job_that_completes_on_time": 86,
             "interference_bound_edf_many_periods_in_between": 40
         },
-        "./analysis/apa/workload_bound.v": {
+        "./classic/analysis/apa/workload_bound.v": {
             "W_monotonic": 51,
             "workload_bound_service_of_first_and_last_jobs": 45,
             "workload_bounded_by_W": 48
         },
-        "./analysis/global/basic/bertogna_edf_comp.v": {
+        "./classic/analysis/global/basic/bertogna_edf_comp.v": {
             "bertogna_edf_comp_f_increases": 53,
             "bertogna_edf_comp_iteration_preserves_order": 160,
             "bertogna_edf_comp_rt_grows_too_much": 100,
             "edf_claimed_bounds_finds_fixed_point_of_list": 76
         },
-        "./analysis/global/basic/bertogna_edf_theory.v": {
+        "./classic/analysis/global/basic/bertogna_edf_theory.v": {
             "bertogna_cirinei_response_time_bound_edf": 50,
             "bertogna_edf_interference_by_different_tasks": 43,
             "bertogna_edf_interference_in_non_full_processors": 129
         },
-        "./analysis/global/basic/bertogna_fp_comp.v": {
+        "./classic/analysis/global/basic/bertogna_fp_comp.v": {
             "fp_analysis_yields_response_time_bounds": 105
         },
-        "./analysis/global/basic/bertogna_fp_theory.v": {
+        "./classic/analysis/global/basic/bertogna_fp_theory.v": {
             "bertogna_cirinei_response_time_bound_fp": 48,
             "bertogna_fp_interference_by_different_tasks": 42,
             "bertogna_fp_interference_in_non_full_processors": 164,
             "bertogna_fp_workload_bounds_interference": 45
         },
-        "./analysis/global/basic/interference_bound_edf.v": {
+        "./classic/analysis/global/basic/interference_bound_edf.v": {
             "interference_bound_edf_holds_for_single_job_that_completes_on_time": 92,
             "interference_bound_edf_many_periods_in_between": 40
         },
-        "./analysis/global/basic/workload_bound.v": {
+        "./classic/analysis/global/basic/workload_bound.v": {
             "W_monotonic": 51,
             "workload_bound_service_of_first_and_last_jobs": 46,
             "workload_bounded_by_W": 48
         },
-        "./analysis/global/jitter/bertogna_edf_comp.v": {
+        "./classic/analysis/global/jitter/bertogna_edf_comp.v": {
             "bertogna_edf_comp_f_increases": 53,
             "bertogna_edf_comp_iteration_preserves_order": 160,
             "bertogna_edf_comp_rt_grows_too_much": 100,
             "edf_claimed_bounds_finds_fixed_point_of_list": 77
         },
-        "./analysis/global/jitter/bertogna_edf_theory.v": {
+        "./classic/analysis/global/jitter/bertogna_edf_theory.v": {
             "bertogna_cirinei_response_time_bound_edf": 60,
             "bertogna_edf_interference_by_different_tasks": 63,
             "bertogna_edf_interference_in_non_full_processors": 125
         },
-        "./analysis/global/jitter/bertogna_fp_comp.v": {
+        "./classic/analysis/global/jitter/bertogna_fp_comp.v": {
             "fp_analysis_yields_response_time_bounds": 120
         },
-        "./analysis/global/jitter/bertogna_fp_theory.v": {
+        "./classic/analysis/global/jitter/bertogna_fp_theory.v": {
             "bertogna_cirinei_response_time_bound_fp": 49,
             "bertogna_fp_all_cpus_are_busy": 40,
             "bertogna_fp_interference_by_different_tasks": 54,
             "bertogna_fp_interference_in_non_full_processors": 173,
             "bertogna_fp_workload_bounds_interference": 46
         },
-        "./analysis/global/jitter/interference_bound_edf.v": {
+        "./classic/analysis/global/jitter/interference_bound_edf.v": {
             "interference_bound_edf_holds_for_single_job_that_completes_on_time": 123,
             "interference_bound_edf_holds_for_single_job_with_small_slack": 55,
             "interference_bound_edf_j_fst_completed_on_time": 46,
             "interference_bound_edf_many_periods_in_between": 49
         },
-        "./analysis/global/jitter/workload_bound.v": {
+        "./classic/analysis/global/jitter/workload_bound.v": {
             "W_monotonic": 51,
             "workload_bound_many_periods_in_between": 41,
             "workload_bound_n_k_covers_middle_jobs": 40,
             "workload_bound_service_of_first_and_last_jobs": 50,
             "workload_bounded_by_W": 48
         },
-        "./analysis/global/parallel/bertogna_edf_comp.v": {
+        "./classic/analysis/global/parallel/bertogna_edf_comp.v": {
             "bertogna_edf_comp_f_increases": 53,
             "bertogna_edf_comp_iteration_preserves_order": 159,
             "bertogna_edf_comp_rt_grows_too_much": 96,
             "edf_claimed_bounds_finds_fixed_point_of_list": 76
         },
-        "./analysis/global/parallel/bertogna_edf_theory.v": {
+        "./classic/analysis/global/parallel/bertogna_edf_theory.v": {
             "bertogna_cirinei_response_time_bound_edf": 49,
             "bertogna_edf_interference_on_all_cpus": 75
         },
-        "./analysis/global/parallel/bertogna_fp_comp.v": {
+        "./classic/analysis/global/parallel/bertogna_fp_comp.v": {
             "fp_analysis_yields_response_time_bounds": 98
         },
-        "./analysis/global/parallel/bertogna_fp_theory.v": {
+        "./classic/analysis/global/parallel/bertogna_fp_theory.v": {
             "bertogna_cirinei_response_time_bound_fp": 41,
             "bertogna_fp_all_cpus_are_busy": 78
         },
-        "./analysis/global/parallel/interference_bound_edf.v": {
+        "./classic/analysis/global/parallel/interference_bound_edf.v": {
             "interference_bound_edf_many_periods_in_between": 40,
             "interference_bound_edf_n_k_covers_all_jobs": 45
         },
-        "./analysis/uni/arrival_curves/workload_bound.v": {
+        "./classic/analysis/uni/arrival_curves/workload_bound.v": {
             "total_workload_le_total_rbf": 45,
             "total_workload_le_total_rbf'": 41,
             "total_workload_le_total_rbf''": 41
         },
-        "./analysis/uni/basic/tdma_wcrt_analysis.v": {
+        "./classic/analysis/uni/basic/tdma_wcrt_analysis.v": {
             "formula_not_sched_St": 45,
             "formula_sched_St": 100,
             "response_time_le_WCRT": 52
         },
-        "./analysis/uni/susp/dynamic/jitter/jitter_schedule_properties.v": {
+        "./classic/analysis/uni/susp/dynamic/jitter/jitter_schedule_properties.v": {
             "sched_jitter_does_not_pick_j": 50,
             "sched_jitter_respects_policy": 77
         },
-        "./analysis/uni/susp/dynamic/jitter/jitter_schedule_service.v": {
+        "./classic/analysis/uni/susp/dynamic/jitter/jitter_schedule_service.v": {
             "jitter_reduction_inductive_step_case2": 96,
             "jitter_reduction_less_job_service_before_interval_case5": 44,
             "jitter_reduction_service_jitter": 51
         },
-        "./analysis/uni/susp/dynamic/jitter/taskset_rta.v": {
+        "./classic/analysis/uni/susp/dynamic/jitter/taskset_rta.v": {
             "valid_response_time_bound_of_tsk_i": 52
         },
-        "./analysis/uni/susp/dynamic/oblivious/reduction.v": {
+        "./classic/analysis/uni/susp/dynamic/oblivious/reduction.v": {
             "sched_new_completed_jobs_dont_execute": 42
         },
-        "./analysis/uni/susp/sustainability/allcosts/main_claim.v": {
+        "./classic/analysis/uni/susp/sustainability/allcosts/main_claim.v": {
             "policy_is_weakly_sustainable": 63
         },
-        "./analysis/uni/susp/sustainability/allcosts/reduction_properties.v": {
+        "./classic/analysis/uni/susp/sustainability/allcosts/reduction_properties.v": {
             "executes_before_suspension_in_sched_new": 42,
             "sched_new_has_shorter_total_suspension": 43,
             "sched_new_respects_policy": 77,
@@ -159,116 +159,116 @@
             "suspended_in_sched_new_no_service_since_execution": 46,
             "suspended_in_sched_new_suspension_starts_no_earlier": 56
         },
-        "./analysis/uni/susp/sustainability/singlecost/reduction_properties.v": {
+        "./classic/analysis/uni/susp/sustainability/singlecost/reduction_properties.v": {
             "sched_susp_highercost_depends_only_on_prefix": 56,
             "sched_susp_highercost_same_schedule": 81
         },
-        "./implementation/apa/bertogna_fp_example.v": {
+        "./classic/implementation/apa/bertogna_fp_example.v": {
             "schedulability_test_succeeds": 87
         },
-        "./implementation/apa/schedule.v": {
+        "./classic/implementation/apa/schedule.v": {
             "scheduler_has_no_duplicate_jobs": 55,
             "scheduler_mapping_is_work_conserving": 46,
             "scheduler_priority": 113
         },
-        "./implementation/global/basic/bertogna_fp_example.v": {
+        "./classic/implementation/global/basic/bertogna_fp_example.v": {
             "schedulability_test_succeeds": 40
         },
-        "./implementation/global/jitter/bertogna_fp_example.v": {
+        "./classic/implementation/global/jitter/bertogna_fp_example.v": {
             "schedulability_test_succeeds": 41
         },
-        "./implementation/global/parallel/bertogna_fp_example.v": {
+        "./classic/implementation/global/parallel/bertogna_fp_example.v": {
             "schedulability_test_succeeds": 59
         },
-        "./implementation/uni/basic/fp_rta_example.v": {
+        "./classic/implementation/uni/basic/fp_rta_example.v": {
             "RTA_yields_these_bounds": 45
         },
-        "./implementation/uni/basic/schedule_tdma.v": {
+        "./classic/implementation/uni/basic/schedule_tdma.v": {
             "respects_FIFO": 45
         },
-        "./implementation/uni/basic/tdma_rta_example.v": {
+        "./classic/implementation/uni/basic/tdma_rta_example.v": {
             "respects_TDMA_policy": 43
         },
-        "./implementation/uni/jitter/fp_rta_example.v": {
+        "./classic/implementation/uni/jitter/fp_rta_example.v": {
             "RTA_yields_these_bounds": 52
         },
-        "./implementation/uni/susp/dynamic/oblivious/fp_rta_example.v": {
+        "./classic/implementation/uni/susp/dynamic/oblivious/fp_rta_example.v": {
             "RTA_yields_these_bounds": 51
         },
-        "./implementation/uni/susp/schedule.v": {
+        "./classic/implementation/uni/susp/schedule.v": {
             "scheduler_depends_only_on_prefix": 52
         },
-        "./model/schedule/global/basic/constrained_deadlines.v": {
+        "./classic/model/schedule/global/basic/constrained_deadlines.v": {
             "platform_cpus_busy_with_interfering_tasks": 65,
             "platform_fp_cpus_busy_with_interfering_tasks": 82
         },
-        "./model/schedule/global/basic/platform.v": {
+        "./classic/model/schedule/global/basic/platform.v": {
             "work_conserving_eq_work_conserving_count": 67
         },
-        "./model/schedule/global/jitter/constrained_deadlines.v": {
+        "./classic/model/schedule/global/jitter/constrained_deadlines.v": {
             "platform_cpus_busy_with_interfering_tasks": 65,
             "platform_fp_cpus_busy_with_interfering_tasks": 85
         },
-        "./model/schedule/global/jitter/platform.v": {
+        "./classic/model/schedule/global/jitter/platform.v": {
             "work_conserving_eq_work_conserving_count": 68
         },
-        "./model/schedule/uni/jitter/busy_interval.v": {
+        "./classic/model/schedule/uni/jitter/busy_interval.v": {
             "busy_interval_is_bounded": 59,
             "exists_busy_interval_prefix": 68,
             "not_quiet_implies_exists_scheduled_hp_job": 46
         },
-        "./model/schedule/uni/limited/abstract_RTA/abstract_rta.v": {
+        "./classic/model/schedule/uni/limited/abstract_RTA/abstract_rta.v": {
             "in": 115
         },
-        "./model/schedule/uni/limited/abstract_RTA/abstract_seq_rta.v": {
+        "./classic/model/schedule/uni/limited/abstract_RTA/abstract_seq_rta.v": {
             "bound_for_cumulative_job_interference_actual": 140,
             "task_rbf_excl_tsk_bounds_task_workload_excl_j": 69
         },
-        "./model/schedule/uni/limited/busy_interval.v": {
+        "./classic/model/schedule/uni/limited/busy_interval.v": {
             "busy_interval_has_uninterrupted_service": 84,
             "busy_interval_is_bounded": 81,
             "exists_busy_interval_prefix": 75,
             "no_idle_time_within_non_quiet_time_interval": 76,
             "pending_hp_job_exists": 73
         },
-        "./model/schedule/uni/limited/edf/nonpr_reg/concrete_models/response_time_bound.v": {
+        "./classic/model/schedule/uni/limited/edf/nonpr_reg/concrete_models/response_time_bound.v": {
             "uniprocessor_response_time_bound_edf_with_fixed_preemption_points": 168,
             "uniprocessor_response_time_bound_edf_with_floating_nonpreemptive_regions": 81
         },
-        "./model/schedule/uni/limited/edf/nonpr_reg/response_time_bound.v": {
+        "./classic/model/schedule/uni/limited/edf/nonpr_reg/response_time_bound.v": {
             "priority_inversion_is_bounded": 56,
             "priority_inversion_is_bounded_by_blocking": 58
         },
-        "./model/schedule/uni/limited/edf/response_time_bound.v": {
+        "./classic/model/schedule/uni/limited/edf/response_time_bound.v": {
             "A_is_in_concrete_search_space": 85,
             "instantiated_task_interference_is_bounded": 163
         },
-        "./model/schedule/uni/limited/fixed_priority/nonpr_reg/concrete_models/response_time_bound.v": {
+        "./classic/model/schedule/uni/limited/fixed_priority/nonpr_reg/concrete_models/response_time_bound.v": {
             "uniprocessor_response_time_bound_fp_with_fixed_preemption_points": 168,
             "uniprocessor_response_time_bound_fp_with_floating_nonpreemptive_regions": 81
         },
-        "./model/schedule/uni/limited/fixed_priority/nonpr_reg/response_time_bound.v": {
+        "./classic/model/schedule/uni/limited/fixed_priority/nonpr_reg/response_time_bound.v": {
             "priority_inversion_is_bounded": 52
         },
-        "./model/schedule/uni/limited/fixed_priority/response_time_bound.v": {
+        "./classic/model/schedule/uni/limited/fixed_priority/response_time_bound.v": {
             "instantiated_task_interference_is_bounded": 47
         },
-        "./model/schedule/uni/limited/jlfp_instantiation.v": {
+        "./classic/model/schedule/uni/limited/jlfp_instantiation.v": {
             "cumulative_task_interference_split": 62,
             "instantiated_cumulative_interference_of_hep_jobs_equal_total_interference_of_hep_jobs": 114,
             "instantiated_cumulative_interference_of_hep_tasks_equal_total_interference_of_hep_tasks": 127,
             "instantiated_quiet_time_equivalent_edf_quiet_time": 102
         },
-        "./model/schedule/uni/limited/platform/limited.v": {
+        "./classic/model/schedule/uni/limited/platform/limited.v": {
             "model_with_fixed_preemption_points_is_model_with_bounded_nonpreemptive_regions": 83
         },
-        "./model/schedule/uni/limited/platform/priority_inversion_is_bounded.v": {
+        "./classic/model/schedule/uni/limited/platform/priority_inversion_is_bounded.v": {
             "=>": 119,
             "not_quiet_implies_exists_scheduled_hp_job_after_preemption_point": 55,
             "not_quiet_implies_exists_scheduled_hp_job_at_preemption_point": 90,
             "scheduling_of_any_segment_starts_with_preemption_time": 44
         },
-        "./model/schedule/uni/limited/platform/util.v": {
+        "./classic/model/schedule/uni/limited/platform/util.v": {
             "belonging_to_segment_of_seq_is_total": 46,
             "distance_between_neighboring_elements_le_max_distance_in_seq": 43,
             "domination_of_distances_implies_domination_of_seq": 58,
@@ -276,26 +276,26 @@
             "max_distance_in_seq_le_last_element_of_seq": 47,
             "max_of_dominating_seq": 47
         },
-        "./model/schedule/uni/nonpreemptive/schedule.v": {
+        "./classic/model/schedule/uni/nonpreemptive/schedule.v": {
             "j_is_not_scheduled_at_t_minus_service_minus_one": 54,
             "j_is_scheduled_at_t_minus_service": 74
         },
-        "./model/schedule/uni/service.v": {
+        "./classic/model/schedule/uni/service.v": {
             "all_jobs_have_completed_impl_workload_eq_service": 44,
             "incremental_service_during": 70
         },
-        "./model/schedule/uni/susp/build_suspension_table.v": {
+        "./classic/model/schedule/uni/susp/build_suspension_table.v": {
             "suspension_duration_matches_predicate_up_to_t_max": 95
         },
-        "./model/schedule/uni/susp/last_execution.v": {
+        "./classic/model/schedule/uni/susp/last_execution.v": {
             "last_execution_idempotent": 41,
             "same_service_implies_same_last_execution": 49
         },
-        "./model/schedule/uni/susp/suspension_intervals.v": {
+        "./classic/model/schedule/uni/susp/suspension_intervals.v": {
             "cumulative_suspension_eq_total_suspension": 86,
             "cumulative_suspension_le_total_suspension": 57
         },
-        "./model/schedule/uni/sustainability.v": {
+        "./classic/model/schedule/uni/sustainability.v": {
             "weak_sustainability_equivalence": 50
         },
         "./util/div_mod.v": {