Changeset 1893
 Timestamp:
 Apr 20, 2012, 11:52:54 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/labelSimulation.ma
r1888 r1893 38 38 qed. 39 39 40 inductive trace_with_extra_labels : trace → trace → Prop ≝ 41  twel_0 : trace_with_extra_labels E0 E0 42  twel_both : ∀h,t1,t2. trace_with_extra_labels t1 t2 → trace_with_extra_labels (h::t1) (h::t2) 43  twel_new : ∀c,t1,t2. trace_with_extra_labels t1 t2 → trace_with_extra_labels t1 (EVcost c::t2). 44 45 lemma twel_refl : ∀tr. trace_with_extra_labels tr tr. 46 #tr elim tr /2/ 47 qed. 48 49 lemma twel_app : ∀tr1,tr2,tr1',tr2'. 50 trace_with_extra_labels tr1 tr1' → 51 trace_with_extra_labels tr2 tr2' → 52 trace_with_extra_labels (tr1⧺tr2) (tr1'⧺tr2'). 53 #tr1 #tr2 #tr1' #tr2' #twel1 elim twel1 /3/ 54 qed. 55 40 56 lemma label_expr_ok : ∀ge,en,m,e,v,tr. 41 57 exec_expr ge en m e = OK … 〈v,tr〉 → 42 ∀u. ∃tr'. exec_expr ge en m (\fst (label_expr e u)) = OK … 〈v,tr'〉. 58 ∀u. ∃tr'. exec_expr ge en m (\fst (label_expr e u)) = OK … 〈v,tr'〉 ∧ 59 trace_with_extra_labels tr tr'. 43 60 #ge #en #m #e 44 61 @(expr_lvalue_ind ? 45 62 (λe,ty. ∀b,o,tr. exec_lvalue' ge en m e ty = OK … 〈〈b,o〉,tr〉 → 46 ∀u. ∃tr'. exec_lvalue' ge en m (\fst (label_expr_descr e u ty)) ty = OK … 〈〈b,o〉,tr'〉) … e) 47 [ 1,2: normalize /2/ 63 ∀u. ∃tr'. exec_lvalue' ge en m (\fst (label_expr_descr e u ty)) ty = OK … 〈〈b,o〉,tr'〉 ∧ 64 trace_with_extra_labels tr tr') … e) 65 [ 1,2: normalize /3 by ex_intro, conj/ 48 66  * // 49 [ normalize / 2 by ex_intro/67 [ normalize /3 by ex_intro, conj/ 50 68  #e1 #ty #IH #v #tr #EX #u 51 69 cases (bind_inversion ????? EX) * * #b #o #tr1 * #EX1 #EX1r 52 70 cases (bind_inversion ????? EX1r) #v * #EXl #EXrem 53 71 normalize in EXrem; destruct 54 cases (IH … EX1 u) #tr1' #EX1'55 %{tr1'} >shift_fst in EX1'; >shift_fst >shift_fst #EX1' whd in ⊢ (? ?%?); >EX1'56 whd in ⊢ (? ?%?); >EXl @refl72 cases (IH … EX1 u) #tr1' * #EX1' #twel1 73 %{tr1'} >shift_fst in EX1'; >shift_fst >shift_fst #EX1' whd in ⊢ (?(??%?)?); >EX1' 74 whd in ⊢ (?(??%?)?); >EXl /2/ 57 75  #e1 #id #ty #IH #v #tr #EX #u 58 76 cases (bind_inversion ????? EX) * * #b #o #tr1 * #EX1 #EX1r 59 77 cases (bind_inversion ????? EX1r) #v * #EXl #EXrem 60 78 normalize in EXrem; destruct 61 cases (IH … EX1 u) #tr1' #EX1'62 %{tr1'} >shift_fst in EX1'; >shift_fst >shift_fst #EX1' whd in ⊢ (??%?); >EX1'79 cases (IH … EX1 u) #tr1' * #EX1' #twel1 80 %{tr1'} >shift_fst in EX1'; >shift_fst >shift_fst #EX1' % // whd in ⊢ (??%?); >EX1' 63 81 whd in ⊢ (??%?); >EXl @refl 64 82 ] 65  #v #ty #b #o #tr #EX #u %{tr} @EX83  #v #ty #b #o #tr #EX #u %{tr} % /2/ 66 84  #e1 #ty #IH #b #o #tr #EX #u 67 85 cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem 68 cases (IH … EX1 u) #tr1' #EX1'69 %{tr1'} >shift_fst whd in ⊢ (? ?%?); >EX1'70 whd in ⊢ (? ?%?);71 cases v1 in EX1rem ⊢ %; normalize #A try #B try #C destruct @refl86 cases (IH … EX1 u) #tr1' * #EX1' #twel1 87 %{tr1'} >shift_fst whd in ⊢ (?(??%?)?); >EX1' 88 whd in ⊢ (?(??%?)?); 89 cases v1 in EX1rem ⊢ %; normalize #A try #B try #C destruct /2/ 72 90  #ty' #e1 #ty #IH #v #tr #EX #u 73 91 cases (bind_inversion ????? EX) * * #b1 #o1 #tr1 * #EX1 #EX1rem 74 cases (IH … EX1 u) #tr1' #EX1'75 %{tr1'} >shift_fst >shift_fst >shift_fst whd in ⊢ (? ?%?);76 whd in ⊢ (? ?(match % with [_⇒?_⇒?])?); >EX1'77 whd in ⊢ (? ?%?);92 cases (IH … EX1 u) #tr1' * #EX1' #twel1 93 %{tr1'} >shift_fst >shift_fst >shift_fst whd in ⊢ (?(??%?)?); 94 whd in ⊢ (?(??(match % with [_⇒?_⇒?])?)?); >EX1' 95 whd in ⊢ (?(??%?)?); 78 96 cases ty' in EX1rem ⊢ %; 79 [ 4: #r #ty' whd in ⊢ (??%? → ? ?%?); cases (pointer_compat_dec b1 r)80 #pc normalize #E destruct @refl97 [ 4: #r #ty' whd in ⊢ (??%? → ?(??%?)?); cases (pointer_compat_dec b1 r) 98 #pc normalize #E destruct /2/ 81 99  *: normalize #A try #B try #C try #D destruct 82 100 ] … … 85 103 cases (bind_inversion ????? EX1rem) #v2 * #EX2 #EXrem 86 104 normalize in EXrem; destruct 87 cases (IH … EX1 u) #tr1' #EX1'88 %{tr1'} >shift_fst105 cases (IH … EX1 u) #tr1' * #EX1' #twel1 106 %{tr1'} % // >shift_fst 89 107 whd in ⊢ (??(????(?(???%)?))?); 90 108 @label_expr_elim #u2 … … 96 114 cases (bind_inversion ????? EX2rem) #v' * #EXop #EXop' 97 115 #u 98 cases (IH1 … EX1 u) #tr1' #EX1'116 cases (IH1 … EX1 u) #tr1' * #EX1' #twel1 99 117 >shift_fst 100 whd in ⊢ (??(λ_.? ?(????(?(???%)?))?));101 @label_expr_elim #u2 102 cases (IH2 … EX2 u2) #tr2' #EX2'118 whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?)); 119 @label_expr_elim #u2 120 cases (IH2 … EX2 u2) #tr2' * #EX2' #twel2 103 121 @label_expr_elim #u3 %{(tr1'⧺tr2')} 104 whd in ⊢ (? ?%?); >EX1'105 whd in ⊢ (? ?%?); >EX2'106 whd in ⊢ (? ?%?); >label_expr_type >label_expr_type >EXop107 normalize in EXop'; destruct @refl122 whd in ⊢ (?(??%?)?); >EX1' 123 whd in ⊢ (?(??%?)?); >EX2' 124 whd in ⊢ (?(??%?)?); >label_expr_type >label_expr_type >EXop 125 normalize in EXop'; destruct % /2/ 108 126  #ty #ty' #e1 #IH #v #tr #EX #u 109 127 cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem 110 128 cases (bind_inversion ????? EX1rem) #v2 * #EX2 #EX2rem 111 129 normalize in EX2rem; destruct 112 cases (IH … EX1 u) #tr1' #EX1'113 %{tr1'} >shift_fst >shift_fst130 cases (IH … EX1 u) #tr1' * #EX1' #twel1 131 %{tr1'} % // >shift_fst >shift_fst 114 132 whd in ⊢ (??%?); >EX1' 115 133 whd in ⊢ (??%?); >label_expr_type >EX2 @refl … … 119 137 cases (bind_inversion ????? EXguardrem) * #v2 #tr2 * #EX2 #EX2rem 120 138 normalize in EX2rem; destruct 121 cases (IH1 … EX1 u) #tr1' #EX1'122 >shift_fst whd in ⊢ (??(λ_.? ?(????(?(???%)?))?));139 cases (IH1 … EX1 u) #tr1' * #EX1' #twel1 140 >shift_fst whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?)); 123 141 @label_expr_elim #u2 124 142 @label_expr_elim #u3 … … 126 144 @label_expr_elim #u5 127 145 @add_cost_expr_elim #u6 #l6 128 [ cases (IH2 … EX2 u2)  cases (IH3 … EX2 u4) ] #trx' #EXx'146 [ cases (IH2 … EX2 u2)  cases (IH3 … EX2 u4) ] #trx' * #EXx' #twelx 129 147 [ %{(tr1'⧺trx'⧺(Echarge l4))}  %{(tr1'⧺trx'⧺(Echarge l6))} ] 130 whd in ⊢ (? ?%?); >EX1'131 whd in ⊢ (? ?%?); >label_expr_type >EXguard132 whd in ⊢ (? ?%?); whd in ⊢ (??(match % with [_⇒?_⇒?])?); >EXx'133 normalize @refl148 whd in ⊢ (?(??%?)?); >EX1' 149 whd in ⊢ (?(??%?)?); >label_expr_type >EXguard 150 whd in ⊢ (?(??%?)?); whd in ⊢ (?(??(match % with [_⇒?_⇒?])?)?); >EXx' 151 normalize % // @twel_app // <(E0_right tr2) @twel_app /2/ 134 152  #ty #e1 #e2 #IH1 #IH2 #v #tr #EX #u 135 153 cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem 136 154 cases (bind_inversion ????? EX1rem) * * #EXguard #EXguardrem 137 >shift_fst whd in ⊢ (??(λ_.? ?(????(?(???%)?))?));155 >shift_fst whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?)); 138 156 @label_expr_elim #u2 139 157 @label_expr_elim #u3 … … 142 160 [ cases (bind_inversion ????? EXguardrem) * #v2 #tr2 * #EX2 #EX2rem 143 161 cases (bind_inversion ????? EX2rem) * * #EX3 #EX3rem 144 cases (IH1 … EX1 u) #tr1' #EX1' 145 cases (IH2 … EX2 u2) #tr2' #EX2' 162 EX1rem EXguardrem EX2rem 163 cases (IH1 … EX1 u) #tr1' * #EX1' #twel1 164 cases (IH2 … EX2 u2) #tr2' * #EX2' #twel2 146 165 %{(tr1'⧺(tr2'⧺E0)⧺Echarge l4)} 147 whd in ⊢ (? ?%?); >EX1'148 whd in ⊢ (? ?%?); >label_expr_type >EX2' >EXguard149 whd in ⊢ (? ?%?); whd in ⊢ (??(match % with [_⇒?_⇒?])?);150 whd in ⊢ (? ?(match (match % with [_⇒?_⇒?]) with [_⇒?_⇒?])?); >EX2'151 whd in ⊢ (? ?(match (match % with [_⇒?_⇒?]) with [_⇒?_⇒?])?); >label_expr_type >EX3152 normalize in EX3rem ⊢ %; destruct @refl153  cases (IH1 … EX1 u) #tr1' #EX1'166 whd in ⊢ (?(??%?)?); >EX1' 167 whd in ⊢ (?(??%?)?); >label_expr_type >EX2' >EXguard 168 whd in ⊢ (?(??%?)?); whd in ⊢ (?(??(match % with [_⇒?_⇒?])?)?); 169 whd in ⊢ (?(??(match (match % with [_⇒?_⇒?]) with [_⇒?_⇒?])?)?); >EX2' 170 whd in ⊢ (?(??(match (match % with [_⇒?_⇒?]) with [_⇒?_⇒?])?)?); >label_expr_type >EX3 171 normalize in EX3rem ⊢ %; destruct % [ 1,3: @refl  *: @twel_app // <(E0_right tr2) @twel_app /2/ ] 172  cases (IH1 … EX1 u) #tr1' * #EX1' #twel1 154 173 %{(tr1'⧺E0⧺Echarge l5)} 155 whd in ⊢ (? ?%?); >EX1'156 whd in ⊢ (? ?%?); >label_expr_type >EXguard157 normalize in EXguardrem; destruct @refl174 whd in ⊢ (?(??%?)?); >EX1' 175 whd in ⊢ (?(??%?)?); >label_expr_type >EXguard 176 normalize in EXguardrem; destruct % // <(E0_right tr) @twel_app /2/ 158 177 ] 159 178  #ty #e1 #e2 #IH1 #IH2 #v #tr #EX #u 160 179 cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem 161 180 cases (bind_inversion ????? EX1rem) * * #EXguard #EXguardrem 162 >shift_fst whd in ⊢ (??(λ_.? ?(????(?(???%)?))?));181 >shift_fst whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?)); 163 182 @label_expr_elim #u2 164 183 @add_cost_expr_elim #u4 #l4 165 184 @label_expr_elim #u3 166 185 @add_cost_expr_elim #u5 #l5 167 [ cases (IH1 … EX1 u) #tr1' #EX1'186 [ cases (IH1 … EX1 u) #tr1' * #EX1' #twel1 168 187 %{(tr1'⧺Echarge l4)} 169 whd in ⊢ (? ?%?); >EX1'170 whd in ⊢ (? ?%?); >label_expr_type >EXguard171 normalize in EXguardrem ⊢ %; destruct @refl188 whd in ⊢ (?(??%?)?); >EX1' 189 whd in ⊢ (?(??%?)?); >label_expr_type >EXguard 190 normalize in EXguardrem ⊢ %; destruct % // <(E0_right tr) /3/ 172 191  cases (bind_inversion ????? EXguardrem) * #v2 #tr2 * #EX2 #EX2rem 173 192 cases (bind_inversion ????? EX2rem) * * #EX3 #EX3rem 174 cases (IH1 … EX1 u) #tr1' #EX1'175 cases (IH2 … EX2 u4) #tr2' #EX2'193 cases (IH1 … EX1 u) #tr1' * #EX1' #twel1 194 cases (IH2 … EX2 u4) #tr2' * #EX2' #twel2 176 195 %{(tr1'⧺(tr2'⧺E0)⧺Echarge l5)} 177 whd in ⊢ (? ?%?); >EX1'178 whd in ⊢ (? ?%?); >label_expr_type >EX2' >EXguard179 whd in ⊢ (? ?%?); whd in ⊢ (??(match % with [_⇒?_⇒?])?);180 whd in ⊢ (? ?(match (match % with [_⇒?_⇒?]) with [_⇒?_⇒?])?); >EX2'181 whd in ⊢ (? ?(match (match % with [_⇒?_⇒?]) with [_⇒?_⇒?])?); >label_expr_type >EX3182 normalize in EX3rem ⊢ %; destruct @refl183 ] 184  #ty #ty' #v #tr normalize / 2/196 whd in ⊢ (?(??%?)?); >EX1' 197 whd in ⊢ (?(??%?)?); >label_expr_type >EX2' >EXguard 198 whd in ⊢ (?(??%?)?); whd in ⊢ (?(??(match % with [_⇒?_⇒?])?)?); 199 whd in ⊢ (?(??(match (match % with [_⇒?_⇒?]) with [_⇒?_⇒?])?)?); >EX2' 200 whd in ⊢ (?(??(match (match % with [_⇒?_⇒?]) with [_⇒?_⇒?])?)?); >label_expr_type >EX3 201 normalize in EX3rem ⊢ %; destruct % // @twel_app // <(E0_right tr2) @twel_app /2/ 202 ] 203  #ty #ty' #v #tr normalize /3/ 185 204  #ty #e1 #ty' #id #IH #b #o #tr #EX #u cases ty' in IH EX ⊢ %; 186 205 [ 7: #id #fl #IH #EX … … 188 207 cases (bind_inversion ????? EX1rem) #n * #EXoff #EXoffrem 189 208 whd in EXoffrem:(???%); destruct >shift_fst >shift_fst 190 cases (IH … EX1 u) #tr1' #EX1'191 %{tr1'} 209 cases (IH … EX1 u) #tr1' * #EX1' #twel1 210 %{tr1'} % // 192 211 whd in ⊢ (??%?); whd in ⊢ (??(match % with [_⇒?_⇒?])?); >EX1' 193 212 whd in ⊢ (??%?); >EXoff whd in ⊢ (??%?); @refl … … 195 214 cases (bind_inversion ????? EX) * * #b1 #o1 #tr1 * #EX1 #EX1rem 196 215 whd in EX1rem:(???%); destruct >shift_fst >shift_fst 197 cases (IH … EX1 u) #tr1' #EX1'198 %{tr1'} 216 cases (IH … EX1 u) #tr1' * #EX1' #twel1 217 %{tr1'} % // 199 218 whd in ⊢ (??%?); whd in ⊢ (??(match % with [_⇒?_⇒?])?); >EX1' 200 219 whd in ⊢ (??%?); @refl … … 204 223 cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem 205 224 whd in EX1rem:(???%); destruct 206 cases (IH … EX1 u) #tr1' #EX1'%{(tr1'@Echarge l)}207 >shift_fst >shift_fst whd in ⊢ (? ?%?); >EX1'208 whd in ⊢ (? ?%?); @refl225 cases (IH … EX1 u) #tr1' * #EX1' #twel1 %{(tr1'@Echarge l)} 226 >shift_fst >shift_fst whd in ⊢ (?(??%?)?); >EX1' 227 whd in ⊢ (?(??%?)?); /3/ 209 228  #e1 #ty #NLV #b #o #tr #EX @⊥ 210 229 cases e1 in NLV EX; normalize // 211 230 #A #B #C try #D try #F destruct 212 231 ] qed. 232 233 (* Plan: 234  extend labelling functions to continuations and hence states 235 NO  this doesn't work because we don't know *which* cost labels to add 236 realistically we'll have to define erasure functions 237  build a simulation relation linking states to their labelled counterparts 238  write a predicate stating that two traces are the same except for some 239 extra costs 240  show some labelling relationship for global environments 241  prove that 242 exec_step ge s1 = = Value … 〈tr,s2〉 → 243 cost_related s1 s1' → 244 ∃tr'. equal_up_to_costs tr tr' ∧ 245 plus ge' s1' tr' s2' ∧ 246 cost_related s2 s2' 247 using some relationship between ge and ge'. 248 249 WAIT  do I really want functions to erase the labels? Or a predicate? 250 251 let rec erase_label_expr (e:expr) : expr ≝ 252 match e with 253 [ Expr ed ty ⇒ Expr (erase_label_expr_descr ed) ty 254 ] 255 and erase_label_expr_descr (e:expr_descr) : expr_descr ≝ 256 match e with 257 [ Ederef e' ⇒ Ederef (erase_label_expr_descr e') 258  Eaddrof e' ⇒ Eaddrof (erase_label_expr_descr e') 259  Eunop op e' 260 *)
Note: See TracChangeset
for help on using the changeset viewer.