source: src/Clight/SimplifyCastsMeasurable.ma @ 3081

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

Tidy up recent work a little.

File size: 4.1 KB
Line 
1include "Clight/SimplifyCasts.ma".
2include "common/FEMeasurable.ma".
3include "Clight/Clight_classified_system.ma".
4
5lemma state_cast_labelled : ∀s,s'.
6  state_cast s s' →
7  Clight_labelled s = Clight_labelled s'.
8#Xs #Xs' * // #f * //
9qed.
10
11lemma return_E0 : ∀ge,s,tr,s'.
12  Clight_classify s = cl_return →
13  exec_step ge s = Value … 〈tr,s'〉 →
14  tr = E0.
15#ge *
16[ #f #s #k #e #m | #vf #fd #args #k #m | #res #k #m | #r ]
17#tr #s' #CL whd in CL:(??%?); destruct
18whd in ⊢ (??%? → ?);
19cases k [ | #s' #k' | #e' #s' #k' | #e' #s' #k' | #e' #s' #s'' #k' | #e' #s' #s'' #k' | #k' | #r' #f' #e' #k' ]
20#ST whd in ST:(??%?); destruct
21[ cases res in ST; [ | * #i | | #p ] #ST whd in ST:(??%?); destruct %
22| cases r' in ST;
23  [ #ST whd in ST:(??%?); destruct %
24  | * * #b #o #t #ST
25    cases (bindIO_inversion ??????? ST)
26    #m' * #ST' #E whd in E:(??%%); destruct %
27  ]
28] qed.
29
30(* Put cast simplification simulation into form that FEMeasurable needs.
31   Note that sim_call_label is just sticking together two normal steps - we
32   never add extra steps here, so we don't need to worry about moving cost
33   labels to the start of the function. *)
34
35definition simplify_measurable_sim : meas_sim ≝
36mk_meas_sim
37  Clight_pcs
38  Clight_pcs
39  (λp,p'. simplify_program p = p')
40  (λge,ge'. related_globals … simplify_fundef ge ge')
41  (λ_,_,_.λs,s'. state_cast s s')
42  ?
43  ?
44  ?
45  ?
46  ?
47  ?
48  ?
49  ?
50  ?
51  ?
52  ?
53  ?
54  ?
55  ?
56.
57[ (* rel_normal *)
58  #ge #ge' #RG #Xs1 #Xs2 * //
59| (* rel_labelled *)
60  #ge #ge' #RG @state_cast_labelled
61| (* rel_classify_call *)
62  #ge #ge' #RG #Xs1 #Xs2 * //
63  [ #f #s #k #k' #e #m #K | #res #k #k' #m #K | #r ]
64  whd in match (pcs_classify Clight_pcs ge ?); #E destruct
65| (* rel_classify_return *)
66  #ge #ge' #RG #Xs1 #Xs2 * //
67  [ #f #s #k #k' #e #m #K | #vf #fd #args #k #k' #m #K | #r ]
68  whd in match (pcs_classify Clight_pcs ge ?); #E destruct
69| (* rel_callee *)
70  #ge #ge' #RG #Xs1 #Xs2 *
71  [ #f #s #k #k' #e #m #K | #vf #fd #args #k #k' #m #K | #res #k #k' #m #K | #r ] *
72  * %
73| (* labelled_normal_1 *)
74  #ge * //
75| (* labelled_normal_2 *)
76  #ge * //
77| (* notailcalls *)
78  #ge *
79  [ #f #s #k #e #m | #vf #fd #args #k #m | #res #k #m | #r ]
80  normalize % #E destruct
81| (* sim_normal *)
82  #ge #ge' #RG #s1 #s1' #S1 #N1 #CS1 #s2 #tr #ST
83  cases (cast_correction … RG … S1 ST)
84  #s2' * #ST' #S2 %{1} whd
85  whd in match (is_final … s1'); >(cl_step_not_final … ST')
86  whd whd in match (step … Clight_pcs ge' s1'); >ST'
87  whd % [ % | assumption ]
88| (* sim_call_nolabel *)
89  #ge #ge' #RG #s1 #s1' #S1 #CL1 #NCS1 #s2 #tr #ST #NCS2
90  cases (cast_correction … RG … S1 ST)
91  #s2' * #ST' #S2 %{0} whd
92  whd in match (is_final … s1'); >(cl_step_not_final … ST')
93  whd whd in match (step … Clight_pcs ge' s1'); >ST'
94  whd % [ % | assumption ]
95| (* sim_call_label *)
96  #ge #ge' #RG #s1 #s1' #S1 #CL1 #NCS1 #s2 #tr2 #s3 #tr3 #ST1 #CS2 #ST2
97  cases (cast_correction … RG … S1 ST1)
98  #s2' * #ST1' #S2
99  cases (cast_correction … RG … S2 ST2)
100  #s3' * #ST2' #S3
101  %{1} whd
102  whd in match (is_final … s1'); >(cl_step_not_final … ST1')
103  whd whd in match (step … Clight_pcs ge' s1'); >ST1'
104  whd % [ % [ % | change with (Clight_labelled s2') in ⊢ (?%); <(state_cast_labelled … S2) assumption ] ]
105  whd whd in match (is_final … s2'); >(cl_step_not_final … ST2')
106  whd whd in match (step … Clight_pcs ge' s2'); >ST2'
107  whd % [ % | assumption ]
108| (* sim_return *)
109  #ge #ge' #RG #s1 #s1' #S1 #CL1 #NCS1 #s2 #tr #ST
110  cases (cast_correction … RG … S1 ST)
111  #s2' * #ST' #S2 %{0} % [ @(return_E0 … ST) assumption ]
112  whd
113  whd in match (is_final … s1'); >(cl_step_not_final … ST')
114  whd whd in match (step … Clight_pcs ge' s1'); >ST'
115  whd % [ >(return_E0 … ST) // assumption | assumption ]
116| (* sim_cost *)
117  #ge #ge' #RG #s1 #s1' #s2 #tr #S1 #CS1 #ST
118  cases (cast_correction … RG … S1 ST)
119  #s2' * #ST' #S2 whd
120  whd in match (is_final … s1'); >(cl_step_not_final … ST')
121  whd whd in match (step … Clight_pcs ge' s1'); >ST'
122  whd % [ % | assumption ]
123| (* sim_init *)
124  #p1 #p2 #s #COMPILE #INIT
125  cases (initial_state_casts … INIT)
126  #s' * * >COMPILE #INIT' #RG #S
127  %{s'} % [ @INIT' | %{RG} assumption ]
128] qed.
129
Note: See TracBrowser for help on using the repository browser.