1 | include "RTLabs/CostSpec.ma". |
---|
2 | include "basics/lists/listb.ma". |
---|
3 | |
---|
4 | (* We aim to extract a loop without a cost label to contradict the reappearance |
---|
5 | of a pc within a trace_any_label. This data structure represents the tail |
---|
6 | of a loop purely in terms of the RTLabs function body graph. *) |
---|
7 | |
---|
8 | inductive bad_label_list (g:graph statement) (head:label) : label → Prop ≝ |
---|
9 | | gl_end : bad_label_list g head head |
---|
10 | | gl_step : ∀l1,l2,H. |
---|
11 | l2 ∈ successors (lookup_present … g l1 H) → |
---|
12 | ¬ is_cost_label (lookup_present … g l1 H) → |
---|
13 | bad_label_list g head l2 → |
---|
14 | bad_label_list g head l1. |
---|
15 | |
---|
16 | (* Some inversion lemmas on the bounds. |
---|
17 | |
---|
18 | For the first step just get a bound after the step; we don't care what it is, |
---|
19 | just that it exists. *) |
---|
20 | |
---|
21 | lemma bound_step1 : ∀g,l1,n. |
---|
22 | bound_on_instrs_to_cost g l1 n → |
---|
23 | ∀l2,H. Exists ? (λl.l = l2) (successors (lookup_present … g l1 H)) → |
---|
24 | ∃m. bound_on_instrs_to_cost' g l2 m. |
---|
25 | #g #l1X #nX * #l #n #H #EX #l2 #H' #EX' %{n} @EX @EX' |
---|
26 | qed. |
---|
27 | |
---|
28 | lemma bound_zero1 : ∀g,l. |
---|
29 | ¬ bound_on_instrs_to_cost g l 0. |
---|
30 | #g #l % #B lapply (refl ? O) cases B in ⊢ (???% → ?); |
---|
31 | #l' #n #H #_ whd in ⊢ (???% → ?); #E destruct |
---|
32 | qed. |
---|
33 | |
---|
34 | lemma bound_zero : ∀g,l. |
---|
35 | bound_on_instrs_to_cost' g l 0 → |
---|
36 | ∃H. bool_to_Prop (is_cost_label (lookup_present … g l H)). |
---|
37 | #g #l #B |
---|
38 | @(match B return λl,n,B. n = O → ∃H. bool_to_Prop (is_cost_label (lookup_present … g l H)) with |
---|
39 | [ boitc_here l n H CS ⇒ ? |
---|
40 | | boitc_later _ _ _ _ B' ⇒ ? |
---|
41 | ] (refl ? O)) |
---|
42 | [ #E >E %{H} @CS |
---|
43 | | #E >E in B'; #B' @⊥ @(absurd … B' (bound_zero1 …)) |
---|
44 | ] qed. |
---|
45 | |
---|
46 | lemma bound_step : ∀g,l,n. |
---|
47 | bound_on_instrs_to_cost' g l (S n) → |
---|
48 | ∃H. (bool_to_Prop (is_cost_label (lookup_present … g l H)) ∨ |
---|
49 | (let stmt ≝ lookup_present … g l H in |
---|
50 | ∀l'. Exists label (λl0. l0 = l') (successors stmt) → |
---|
51 | bound_on_instrs_to_cost' g l' n)). |
---|
52 | #g #lX #n #B lapply (refl ? (S n)) cases B in ⊢ (???% → %); |
---|
53 | [ #l #n #H #CS #E %{H} %1 @CS |
---|
54 | | #l #m #H #CS * |
---|
55 | #l' #n' #H' #EX #E destruct %{H'} %2 |
---|
56 | #l'' #EX' @EX @EX' |
---|
57 | ] qed. |
---|
58 | |
---|
59 | lemma bad_label_list_no_cost : ∀g,l1,l2. |
---|
60 | bad_label_list g l1 l2 → |
---|
61 | ∀H1. ¬ is_cost_label (lookup_present … g l1 H1) → |
---|
62 | ∃H2. bool_to_Prop (¬ is_cost_label (lookup_present … g l2 H2)). |
---|
63 | #g #l1 #l2 * /2/ |
---|
64 | qed. |
---|
65 | |
---|
66 | (* Show that a bad_label_list is incompatible with a bound on the number of |
---|
67 | instructions to a cost label, by induction on the bound and the invariant |
---|
68 | that none of the instructions involved are a cost label. *) |
---|
69 | |
---|
70 | lemma loop_soundness_contradiction_aux : ∀g,l1,l2,H1. |
---|
71 | Exists ? (λl.l = l2) (successors (lookup_present … g l1 H1)) → |
---|
72 | ¬ is_cost_label (lookup_present … g l1 H1) → |
---|
73 | bad_label_list g l1 l2 → |
---|
74 | ∀n,l'. |
---|
75 | bad_label_list g l1 l' → |
---|
76 | ¬ bound_on_instrs_to_cost' g l' n. |
---|
77 | #g #l1 #l2 #H1 #SC1 #NCS1 #BLL2 |
---|
78 | #n elim n |
---|
79 | [ #l #BLL % #BOUND |
---|
80 | cases (bound_zero … BOUND) #H' #ICS |
---|
81 | cases (bad_label_list_no_cost … BLL H1 NCS1) #H'' |
---|
82 | >ICS * |
---|
83 | | #m #IH #l #BLL % #BOUND |
---|
84 | cases (bound_step … BOUND) #H' * |
---|
85 | [ #ICS cases (bad_label_list_no_cost … BLL H1 NCS1) #H'' >ICS * |
---|
86 | | #EX_BOUND inversion BLL |
---|
87 | [ #E1 #E2 destruct |
---|
88 | lapply (IH l2 BLL2) |
---|
89 | lapply (EX_BOUND … SC1) |
---|
90 | @absurd |
---|
91 | | #l3 #l4 #H3 #SC2 #NCS3 #BLL4 #_ #E1 #E2 destruct |
---|
92 | lapply (IH l4 BLL4) |
---|
93 | cut (Exists ? (λl.l=l4) (successors (lookup_present … H3))) |
---|
94 | [ cases (memb_exists … SC2) #left * #right #E >E @Exists_mid % ] |
---|
95 | #SC2' lapply (EX_BOUND … SC2') |
---|
96 | @absurd |
---|
97 | ] |
---|
98 | ] |
---|
99 | ] qed. |
---|
100 | |
---|
101 | lemma loop_soundness_contradiction : ∀g,l1,l2,H1. |
---|
102 | Exists ? (λl.l = l2) (successors (lookup_present … g l1 H1)) → |
---|
103 | ¬ is_cost_label (lookup_present … g l1 H1) → |
---|
104 | bad_label_list g l1 l2 → |
---|
105 | ∀n. ¬ bound_on_instrs_to_cost' g l2 n. |
---|
106 | #g #l1 #l2 #H1 #EX #NCS #BLL #n |
---|
107 | @(loop_soundness_contradiction_aux … BLL … BLL) // |
---|
108 | qed. |
---|
109 | |
---|