source: src/Clight/SimplifyCastsMeasurable.ma @ 3053

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

Cast simplification preserves measurable subtraces.

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