source: src/Clight/SimplifyCastsMeasurable.ma @ 3063

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

Remove measure function from FEMeasurable because we're not using it and
it would need to be generalised for clight to cminor. Sketch out rest
of clight to cminor meas_sim record.

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  ?
54  ?
55  ?
56  ?
57  ?
58  ?
59.
60[ (* rel_normal *)
61  #ge #ge' #RG #Xs1 #Xs2 * //
62| (* rel_labelled *)
63  #ge #ge' #RG @state_cast_labelled
64| (* rel_classify_call *)
65  #ge #ge' #RG #Xs1 #Xs2 * //
66  [ #f #s #k #k' #e #m #K | #res #k #k' #m #K | #r ]
67  whd in match (pcs_classify Clight_pcs ge ?); #E destruct
68| (* rel_classify_return *)
69  #ge #ge' #RG #Xs1 #Xs2 * //
70  [ #f #s #k #k' #e #m #K | #vf #fd #args #k #k' #m #K | #r ]
71  whd in match (pcs_classify Clight_pcs ge ?); #E destruct
72| (* rel_callee *)
73  #ge #ge' #RG #Xs1 #Xs2 *
74  [ #f #s #k #k' #e #m #K | #vf #fd #args #k #k' #m #K | #res #k #k' #m #K | #r ] *
75  * %
76| (* labelled_normal_1 *)
77  #ge * //
78| (* labelled_normal_2 *)
79  #ge * //
80| (* notailcalls *)
81  #ge *
82  [ #f #s #k #e #m | #vf #fd #args #k #m | #res #k #m | #r ]
83  normalize % #E destruct
84| (* sim_normal *)
85  #ge #ge' #RG #s1 #s1' #S1 #N1 #CS1 #s2 #tr #ST
86  cases (cast_correction … RG … S1 ST)
87  #s2' * #ST' #S2 %{1} whd
88  whd in match (is_final … s1'); >(step_not_final … ST')
89  whd whd in match (step … Clight_pcs ge' s1'); >ST'
90  whd % [ % | assumption ]
91| (* sim_call_nolabel *)
92  #ge #ge' #RG #s1 #s1' #S1 #CL1 #NCS1 #s2 #tr #ST #NCS2
93  cases (cast_correction … RG … S1 ST)
94  #s2' * #ST' #S2 %{0} whd
95  whd in match (is_final … s1'); >(step_not_final … ST')
96  whd whd in match (step … Clight_pcs ge' s1'); >ST'
97  whd % [ % | assumption ]
98| (* sim_call_label *)
99  #ge #ge' #RG #s1 #s1' #S1 #CL1 #NCS1 #s2 #tr2 #s3 #tr3 #ST1 #CS2 #ST2
100  cases (cast_correction … RG … S1 ST1)
101  #s2' * #ST1' #S2
102  cases (cast_correction … RG … S2 ST2)
103  #s3' * #ST2' #S3
104  %{1} whd
105  whd in match (is_final … s1'); >(step_not_final … ST1')
106  whd whd in match (step … Clight_pcs ge' s1'); >ST1'
107  whd % [ % [ % | change with (Clight_labelled s2') in ⊢ (?%); <(state_cast_labelled … S2) assumption ] ]
108  whd whd in match (is_final … s2'); >(step_not_final … ST2')
109  whd whd in match (step … Clight_pcs ge' s2'); >ST2'
110  whd % [ % | assumption ]
111| (* sim_return *)
112  #ge #ge' #RG #s1 #s1' #S1 #CL1 #NCS1 #s2 #tr #ST
113  cases (cast_correction … RG … S1 ST)
114  #s2' * #ST' #S2 %{0} % [ @(return_E0 … ST) assumption ]
115  whd
116  whd in match (is_final … s1'); >(step_not_final … ST')
117  whd whd in match (step … Clight_pcs ge' s1'); >ST'
118  whd % [ >(return_E0 … ST) // assumption | assumption ]
119| (* sim_cost *)
120  #ge #ge' #RG #s1 #s1' #s2 #tr #S1 #CS1 #ST
121  cases (cast_correction … RG … S1 ST)
122  #s2' * #ST' #S2 whd
123  whd in match (is_final … s1'); >(step_not_final … ST')
124  whd whd in match (step … Clight_pcs ge' s1'); >ST'
125  whd % [ % | assumption ]
126| (* sim_init *)
127  #p1 #p2 #s #COMPILE #INIT
128  cases (initial_state_casts … INIT)
129  #s' * * >COMPILE #INIT' #RG #S
130  %{s'} % [ @INIT' | %{RG} assumption ]
131] qed.
132
Note: See TracBrowser for help on using the repository browser.