source: src/RTLabs/CostInj.ma @ 2677

Last change on this file since 2677 was 2601, checked in by sacerdot, 7 years ago

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

File size: 4.7 KB
Line 
1include "RTLabs/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
8definition 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
14definition function_cost_injectivity ≝
15λf. graph_cost_injectivity (f_graph f).
16
17definition 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
20definition 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
43definition check_fun_inj : internal_function → bool ≝
44λf.
45match reverse_label_map (f_graph f) with
46[ None ⇒ false
47| Some _ ⇒ true
48].
49
50
51lemma 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:(??%?);
58lapply (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
111lemma 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
127definition 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
130theorem 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
Note: See TracBrowser for help on using the repository browser.