Index: /src/RTLabs/CostCheck.ma
===================================================================
 /src/RTLabs/CostCheck.ma (revision 2314)
+++ /src/RTLabs/CostCheck.ma (revision 2315)
@@ 3,4 +3,5 @@
include "utilities/bool.ma".
include "utilities/listb.ma".
+include "RTLabs/CostMisc.ma".
definition check_well_cost_fn : internal_function → bool ≝
@@ 118,5 +119,4 @@
check_label_bounded_spec g l tl toch toch.
(* TODO: move (or is it somewhere already?) *)
lemma check_label_bounded_s : ∀term_check,g,CL,checking,PR,checking_tail,to_check,TERM,to_check'.
@@ 255,4 +255,9 @@
qed.
+(* Show that when we remove labels from to_check we do actually find a bound
+ (if it exists). We need two extra facts: everything is "well" labelled,
+ so that we know that branches are followed by labels and we don't need to
+ follow them; and anything in the graph that isn't mentioned has already been
+ successfully checked. *)
lemma check_label_bounded_ok : ∀g,checking,checking_tail,to_check,to_check'.
@@ 328,5 +333,10 @@
] qed.
include "RTLabs/CostMisc.ma".
+
+(* When we reject a label it is because we found a loop without a cost label
+ when we followed its successors. We need the invariant that only the
+ initial label can be a cost label, and have two cases in the result: either
+ we found the entire loop and return that, or we haven't come back out of the
+ recursive calls to find the head again, so return part of the loop. *)
lemma check_label_bounded_bad : ∀g,CL,term_check,checking,PR,checking_tail,to_check,TERM.
@@ 390,5 +400,5 @@

+(* Now keep checking as long as there's some instruction we haven't checked. *)
let rec check_graph_bounded
@@ 485,4 +495,8 @@
] qed.
+(* The check_label_bounded_bad result gives us the loop, so we can use the
+ loop_soundness_contradiction result to show that there's no bound for the
+ head of the loop. *)
+
lemma check_graph_bounded_bad : ∀g.∀CL:graph_closed g. ∀term_check,to_check,SUB,start,PR,REMOVED,SMALLER,TERM.
check_graph_bounded g CL to_check SUB start PR REMOVED SMALLER term_check TERM = false →