source: src/RTLabs/CostInj.ma @ 3022

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

Make a couple of tests monadic for easier inversion.

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