[2418] | 1 | include "RTLabs/Traces.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 /3/ |
---|
| 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 ?) [/3/] #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 /2/ |
---|
| 93 | ] |
---|
| 94 | ] |
---|
| 95 | ] |
---|
| 96 | ] |
---|
| 97 | | whd #l #cl % |
---|
| 98 | [ * * #H cases (H (refl ??)) |
---|
| 99 | | #E normalize in E; destruct |
---|
| 100 | ] |
---|
| 101 | | cases r |
---|
| 102 | [ // |
---|
| 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 | |
---|