1 | include "RTLabs/CostSpec.ma". |
---|
2 | |
---|
3 | (* Check that the RTLabs pc → cost label map is injective for a given RTLabs |
---|
4 | program. |
---|
5 | |
---|
6 | First we check functions individually, then lift to the whole program. *) |
---|
7 | |
---|
8 | definition graph_cost_injectivity : graph statement → Prop ≝ |
---|
9 | λg. ∀l1,l2,PR1,PR2,cl. |
---|
10 | cost_label_of (lookup_present ?? g l1 PR1) = Some ? cl → |
---|
11 | cost_label_of (lookup_present ?? g l2 PR2) = Some ? cl → |
---|
12 | l1 = l2. |
---|
13 | |
---|
14 | definition function_cost_injectivity ≝ |
---|
15 | λf. graph_cost_injectivity (f_graph f). |
---|
16 | |
---|
17 | definition program_cost_injectivity : RTLabs_program → Prop ≝ |
---|
18 | λp. All ? (λx. match \snd x with [ Internal f ⇒ function_cost_injectivity f | _ ⇒ True]) (prog_funct … p). |
---|
19 | |
---|
20 | definition reverse_label_map : graph statement → (option (identifier_map CostTag (identifier LabelTag))) ≝ |
---|
21 | λg. |
---|
22 | foldi |
---|
23 | statement |
---|
24 | (option (identifier_map CostTag (identifier LabelTag))) |
---|
25 | LabelTag |
---|
26 | (λl,s,m. |
---|
27 | match m with |
---|
28 | [ None ⇒ None ? |
---|
29 | | Some m ⇒ |
---|
30 | match cost_label_of s with |
---|
31 | [ Some cl ⇒ |
---|
32 | match lookup ?? m cl with |
---|
33 | [ None ⇒ Some ? (add … m cl l) |
---|
34 | | Some _ ⇒ None ? |
---|
35 | ] |
---|
36 | | None ⇒ Some ? m |
---|
37 | ] |
---|
38 | ]) |
---|
39 | g |
---|
40 | (Some ? (empty_map …)). |
---|
41 | |
---|
42 | |
---|
43 | definition check_fun_inj : internal_function → bool ≝ |
---|
44 | λf. |
---|
45 | match reverse_label_map (f_graph f) with |
---|
46 | [ None ⇒ false |
---|
47 | | Some _ ⇒ true |
---|
48 | ]. |
---|
49 | |
---|
50 | |
---|
51 | lemma reverse_label_map_ok : ∀g,r. |
---|
52 | reverse_label_map g = r → |
---|
53 | match r with |
---|
54 | [ None ⇒ ¬graph_cost_injectivity g |
---|
55 | | Some m ⇒ graph_cost_injectivity g |
---|
56 | ]. |
---|
57 | #g #r #F change with (foldi ??????) in F:(??%?); |
---|
58 | lapply (foldi_ind' ??????? (λm,ls. |
---|
59 | match m with |
---|
60 | [ None ⇒ ¬(graph_cost_injectivity g) |
---|
61 | | Some m ⇒ ∀l,cl. (present ?? ls l ∧ ∃PR. cost_label_of (lookup_present ?? g l PR) = Some ? cl) ↔ lookup ?? m cl = Some ? l |
---|
62 | ]) ?? F) |
---|
63 | [ #l #ls #s * |
---|
64 | [ #FR #L #H whd in H ⊢ %; @H |
---|
65 | | #m #FR #L #H whd in H ⊢ (match % with [_⇒?|_⇒?]); |
---|
66 | lapply (refl ? (cost_label_of s)) cases (cost_label_of s) in ⊢ (???% → %); |
---|
67 | [ #NCS whd #l' #cl cases (H l' cl) #H1 #H2 % |
---|
68 | [ * #H3 * #PR' #H4 cases (present_add_cases ?????? H3) |
---|
69 | [ #E destruct @⊥ >(lookup_present_eq ????? L ?) in H4; >NCS #E destruct |
---|
70 | | * #_ #PR'' @H1 % /2/ |
---|
71 | ] |
---|
72 | | #Lcl cases (H2 Lcl) #PR'' * #PR''' #CS % /2/ |
---|
73 | ] |
---|
74 | | #cl #CL whd in ⊢ (match % with [_⇒?|_⇒?]); |
---|
75 | lapply (refl ? (lookup ?? m cl)) cases (lookup ?? m cl) in ⊢ (???% → %); |
---|
76 | [ #Lcl whd #l' #cl' cases (H l' cl') #H1 #H2 % |
---|
77 | [ * #H3 * #PRg' #H4 cases (present_add_cases ?????? H3) |
---|
78 | [ #E destruct >(lookup_present_eq ????? L ?) in H4; >CL #E destruct |
---|
79 | @lookup_add_hit |
---|
80 | | * #NE #PR'' lapply (H1 ?) [% /2/] #Lcl' >lookup_add_miss [ // | % #E destruct >Lcl in Lcl'; #E destruct ] |
---|
81 | ] |
---|
82 | | #Lcl' cases (lookup_add_cases ??????? Lcl') |
---|
83 | [ * #E1 #E2 destruct % [ @present_add_hit | %{(lookup_is_present … L)} >(lookup_present_eq ????? L ?) assumption ] |
---|
84 | | #Lcl'' cases (H2 Lcl'') /3/ |
---|
85 | ] |
---|
86 | ] |
---|
87 | | #l' #L' whd % #GCI whd in GCI; |
---|
88 | cases (H l' cl) #H1 #H2 cases (H2 L') #PR' * #PRg' #CS' |
---|
89 | lapply (GCI l l' (lookup_is_present … L) PRg' cl ??) |
---|
90 | [ assumption |
---|
91 | | >(lookup_present_eq ????? L ?) assumption |
---|
92 | | #E destruct @(absurd … PR' FR) |
---|
93 | ] |
---|
94 | ] |
---|
95 | ] |
---|
96 | ] |
---|
97 | | whd #l #cl % |
---|
98 | [ * * #H cases (H (refl ??)) |
---|
99 | | #E normalize in E; destruct |
---|
100 | ] |
---|
101 | | cases r |
---|
102 | [ whd in ⊢ (% → %); // |
---|
103 | | #m whd in ⊢ (% → %); #H |
---|
104 | #l1 #l2 #PR1 #PR2 #cl #CL1 #CL2 |
---|
105 | cases (H l1 cl) #H1 #_ lapply (H1 ?) [ % [ @(proj1 … (domain_of_map_present … )) // | %{PR1} @CL1 ] ] |
---|
106 | cases (H l2 cl) #H2 #_ lapply (H2 ?) [ % [ @(proj1 … (domain_of_map_present … )) // | %{PR2} @CL2 ] ] |
---|
107 | #E >E #E' destruct % |
---|
108 | ] |
---|
109 | ] qed. |
---|
110 | |
---|
111 | lemma check_fun_inj_ok : ∀f. bool_to_Prop (check_fun_inj f) ↔ function_cost_injectivity f. |
---|
112 | #f % |
---|
113 | [ whd in ⊢ (?% → ?); |
---|
114 | lapply (reverse_label_map_ok (f_graph f)) |
---|
115 | cases (reverse_label_map ?) |
---|
116 | [ #_ * |
---|
117 | | #m #H #_ @(H (Some ? m)) % |
---|
118 | ] |
---|
119 | | lapply (reverse_label_map_ok (f_graph f)) |
---|
120 | whd in ⊢ (? → ? → ?%); |
---|
121 | cases (reverse_label_map ?) |
---|
122 | [ #H #INJ @(absurd … INJ (H (None ?) (refl ??))) |
---|
123 | | // |
---|
124 | ] |
---|
125 | ] qed. |
---|
126 | |
---|
127 | definition check_program_cost_injectivity : RTLabs_program → bool ≝ |
---|
128 | λp. all ? (λx. match \snd x with [ Internal f ⇒ check_fun_inj f | _ ⇒ true ]) (prog_funct … p). |
---|
129 | |
---|
130 | theorem check_project_cost_injectivity_ok : ∀p. |
---|
131 | bool_to_Prop (check_program_cost_injectivity p) ↔ program_cost_injectivity p. |
---|
132 | #p % |
---|
133 | [ #H whd in H:(?%) ⊢ %; |
---|
134 | @(All_mp ????? (proj1 … (all_All …) H)) |
---|
135 | * #_ * // #f @(proj1 … (check_fun_inj_ok f)) |
---|
136 | | whd in ⊢ (% → ?%); |
---|
137 | #H |
---|
138 | @(proj2 … (all_All …)) |
---|
139 | @(All_mp … H) |
---|
140 | * #_ * // #f |
---|
141 | @(proj2 … (check_fun_inj_ok f)) |
---|
142 | ] qed. |
---|
143 | |
---|
144 | |
---|
145 | |
---|