source: src/RTLabs/CostMisc.ma @ 2475

Last change on this file since 2475 was 2313, checked in by campbell, 7 years ago

RTLabs cost checker correct.

File size: 3.8 KB
Line 
1include "RTLabs/CostSpec.ma".
2include "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
8inductive 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   
21lemma 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'
26qed.
27
28lemma 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
32qed.
33
34lemma 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
46lemma 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
59lemma 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/
64qed.
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   
70lemma 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
101lemma 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) //
108qed.
109
Note: See TracBrowser for help on using the repository browser.