[1888] | 1 | |
---|
| 2 | include "Clight/label.ma". |
---|
| 3 | include "Clight/Cexec.ma". |
---|
[2019] | 4 | include "Clight/CexecInd.ma". |
---|
[1888] | 5 | |
---|
[1930] | 6 | (* Useful for breaking up the labeling functions, because we don't care about |
---|
| 7 | *which* cost labels are added here and so can throw away the resulting name |
---|
| 8 | generator. *) |
---|
[1888] | 9 | lemma shift_fst : ∀A,B,C,D:Type[0].∀e:A×B.∀F:A → C.∀G:B → D. |
---|
| 10 | \fst (let 〈x,y〉 ≝ e in 〈F x, G y〉) = F (\fst e). |
---|
| 11 | #A #B #C #D * // |
---|
| 12 | qed. |
---|
| 13 | |
---|
[1954] | 14 | |
---|
[1930] | 15 | (* Similarly, lemma to break up label_expr, label_exprs and label_statement in |
---|
| 16 | the labelling functions *) |
---|
[1920] | 17 | lemma label_gen_elim : ∀Syn:Type[0].∀syn,u.∀T:Type[0].∀L:Syn → universe CostTag → Syn × (universe CostTag). ∀F:Syn → universe CostTag → T. ∀P:T → Type[0]. |
---|
| 18 | (∀u'. P (F (\fst (L syn u)) u')) → |
---|
| 19 | P (let 〈syn',u'〉 ≝ L syn u in F syn' u'). |
---|
| 20 | #Syn #syn #u #T #L #F #P |
---|
| 21 | cases (L syn u) |
---|
| 22 | #syn' #u' #H @H |
---|
[1888] | 23 | qed. |
---|
| 24 | |
---|
| 25 | lemma add_cost_expr_elim : ∀e,u.∀T:Type[0].∀F:expr → universe CostTag → T. ∀P:T → Type[0]. |
---|
| 26 | (∀u',l. P (F (Expr (Ecost l e) (typeof e)) u')) → |
---|
| 27 | P (let 〈e',u'〉 ≝ add_cost_expr e u in F e' u'). |
---|
| 28 | #e #u #T #F #P #H whd in match (add_cost_expr ??); |
---|
| 29 | cases (fresh ??) #l #u' @H |
---|
| 30 | qed. |
---|
| 31 | |
---|
| 32 | |
---|
| 33 | lemma label_expr_type : ∀e,u. |
---|
| 34 | typeof (\fst (label_expr e u)) = typeof e. |
---|
| 35 | * #e #ty #u >shift_fst // |
---|
| 36 | qed. |
---|
| 37 | |
---|
[1930] | 38 | (* Formalise the notion of a trace with extra cost labels added. Note that |
---|
| 39 | we don't require the left trace to be cost free. *) |
---|
[1893] | 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 | |
---|
[1930] | 56 | theorem label_expr_ok : ∀ge,ge',en,m. |
---|
[2105] | 57 | related_globals … label_fundef ge ge' → |
---|
[1920] | 58 | (∀e,v,tr. |
---|
| 59 | exec_expr ge en m e = OK … 〈v,tr〉 → |
---|
| 60 | ∀u. ∃tr'. exec_expr ge' en m (\fst (label_expr e u)) = OK … 〈v,tr'〉 ∧ |
---|
| 61 | trace_with_extra_labels tr tr') ∧ |
---|
| 62 | (∀e,ty,b,o,tr. exec_lvalue' ge en m e ty = OK … 〈〈b,o〉,tr〉 → |
---|
| 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'). |
---|
[1930] | 65 | (* Proof goes by breaking up the execution in the hypothesis, breaking up the |
---|
| 66 | labelling function to get a new term and executing it by rewriting what we |
---|
| 67 | learned from the hypothesis. *) |
---|
[1920] | 68 | #ge #ge' #en #m #RG @expr_lvalue_ind_combined |
---|
[1893] | 69 | [ 1,2: normalize /3 by ex_intro, conj/ |
---|
[1888] | 70 | | * // |
---|
[1920] | 71 | [ #id #ty #IH #v #tr #EX #u |
---|
| 72 | cases (bind_inversion ????? EX) -EX * * #b #o #tr1 * #EX1 #EX |
---|
| 73 | cases (bind_inversion ????? EX) -EX #v2 * #EX2 #EX |
---|
| 74 | normalize in EX; destruct |
---|
| 75 | cases (IH … EX1 u) #tr1' * #EX1' #T1 |
---|
| 76 | %{(tr1')} % [ whd in ⊢ (??%?); >EX1' whd in ⊢ (??%?); >EX2 @refl | // ] |
---|
[1888] | 77 | | #e1 #ty #IH #v #tr #EX #u |
---|
| 78 | cases (bind_inversion ????? EX) * * #b #o #tr1 * #EX1 #EX1r |
---|
| 79 | cases (bind_inversion ????? EX1r) #v * #EXl #EXrem |
---|
| 80 | normalize in EXrem; destruct |
---|
[1893] | 81 | cases (IH … EX1 u) #tr1' * #EX1' #twel1 |
---|
| 82 | %{tr1'} >shift_fst in EX1'; >shift_fst >shift_fst #EX1' whd in ⊢ (?(??%?)?); >EX1' |
---|
| 83 | whd in ⊢ (?(??%?)?); >EXl /2/ |
---|
[1888] | 84 | | #e1 #id #ty #IH #v #tr #EX #u |
---|
| 85 | cases (bind_inversion ????? EX) * * #b #o #tr1 * #EX1 #EX1r |
---|
| 86 | cases (bind_inversion ????? EX1r) #v * #EXl #EXrem |
---|
| 87 | normalize in EXrem; destruct |
---|
[1893] | 88 | cases (IH … EX1 u) #tr1' * #EX1' #twel1 |
---|
| 89 | %{tr1'} >shift_fst in EX1'; >shift_fst >shift_fst #EX1' % // whd in ⊢ (??%?); >EX1' |
---|
[1888] | 90 | whd in ⊢ (??%?); >EXl @refl |
---|
| 91 | ] |
---|
[1920] | 92 | | #v #ty #b #o #tr #EX #u %{tr} % [ |
---|
| 93 | whd in EX:(??%?) ⊢ (??%?); cases (lookup ??? v) in EX ⊢ %; |
---|
| 94 | [ whd in ⊢ (??%? → ??%?); >(rg_find_symbol … RG) // |
---|
| 95 | | #b // ] |
---|
| 96 | | // ] |
---|
[1888] | 97 | | #e1 #ty #IH #b #o #tr #EX #u |
---|
| 98 | cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem |
---|
[1893] | 99 | cases (IH … EX1 u) #tr1' * #EX1' #twel1 |
---|
| 100 | %{tr1'} >shift_fst whd in ⊢ (?(??%?)?); >EX1' |
---|
| 101 | whd in ⊢ (?(??%?)?); |
---|
| 102 | cases v1 in EX1rem ⊢ %; normalize #A try #B try #C destruct /2/ |
---|
[1888] | 103 | | #ty' #e1 #ty #IH #v #tr #EX #u |
---|
| 104 | cases (bind_inversion ????? EX) * * #b1 #o1 #tr1 * #EX1 #EX1rem |
---|
[1893] | 105 | cases (IH … EX1 u) #tr1' * #EX1' #twel1 |
---|
| 106 | %{tr1'} >shift_fst >shift_fst >shift_fst whd in ⊢ (?(??%?)?); |
---|
| 107 | whd in ⊢ (?(??(match % with [_⇒?|_⇒?])?)?); >EX1' |
---|
| 108 | whd in ⊢ (?(??%?)?); |
---|
[1888] | 109 | cases ty' in EX1rem ⊢ %; |
---|
[1893] | 110 | [ 4: #r #ty' whd in ⊢ (??%? → ?(??%?)?); cases (pointer_compat_dec b1 r) |
---|
| 111 | #pc normalize #E destruct /2/ |
---|
[1888] | 112 | | *: normalize #A try #B try #C try #D destruct |
---|
| 113 | ] |
---|
| 114 | | #ty #op #e1 #IH #v #tr #EX #u |
---|
| 115 | cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem |
---|
| 116 | cases (bind_inversion ????? EX1rem) #v2 * #EX2 #EXrem |
---|
| 117 | normalize in EXrem; destruct |
---|
[1893] | 118 | cases (IH … EX1 u) #tr1' * #EX1' #twel1 |
---|
| 119 | %{tr1'} % // >shift_fst |
---|
[1888] | 120 | whd in ⊢ (??(????(?(???%)?))?); |
---|
[1920] | 121 | @label_gen_elim #u2 |
---|
[1888] | 122 | whd in ⊢ (??%?); >EX1' |
---|
| 123 | whd in ⊢ (??%?); >label_expr_type >EX2 @refl |
---|
| 124 | | #ty #op #e1 #e2 #IH1 #IH2 #v #tr #EX |
---|
| 125 | cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem |
---|
| 126 | cases (bind_inversion ????? EX1rem) * #v2 #tr2 * #EX2 #EX2rem |
---|
| 127 | cases (bind_inversion ????? EX2rem) #v' * #EXop #EXop' |
---|
| 128 | #u |
---|
[1893] | 129 | cases (IH1 … EX1 u) #tr1' * #EX1' #twel1 |
---|
[1888] | 130 | >shift_fst |
---|
[1893] | 131 | whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?)); |
---|
[1920] | 132 | @label_gen_elim #u2 |
---|
[1893] | 133 | cases (IH2 … EX2 u2) #tr2' * #EX2' #twel2 |
---|
[1920] | 134 | @label_gen_elim #u3 %{(tr1'⧺tr2')} |
---|
[1893] | 135 | whd in ⊢ (?(??%?)?); >EX1' |
---|
| 136 | whd in ⊢ (?(??%?)?); >EX2' |
---|
| 137 | whd in ⊢ (?(??%?)?); >label_expr_type >label_expr_type >EXop |
---|
| 138 | normalize in EXop'; destruct % /2/ |
---|
[1888] | 139 | | #ty #ty' #e1 #IH #v #tr #EX #u |
---|
| 140 | cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem |
---|
| 141 | cases (bind_inversion ????? EX1rem) #v2 * #EX2 #EX2rem |
---|
| 142 | normalize in EX2rem; destruct |
---|
[1893] | 143 | cases (IH … EX1 u) #tr1' * #EX1' #twel1 |
---|
| 144 | %{tr1'} % // >shift_fst >shift_fst |
---|
[1888] | 145 | whd in ⊢ (??%?); >EX1' |
---|
| 146 | whd in ⊢ (??%?); >label_expr_type >EX2 @refl |
---|
| 147 | | #ty #e1 #e2 #e3 #IH1 #IH2 #IH3 #v #tr #EX #u |
---|
| 148 | cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem |
---|
| 149 | cases (bind_inversion ????? EX1rem) * * #EXguard #EXguardrem |
---|
| 150 | cases (bind_inversion ????? EXguardrem) * #v2 #tr2 * #EX2 #EX2rem |
---|
| 151 | normalize in EX2rem; destruct |
---|
[1893] | 152 | cases (IH1 … EX1 u) #tr1' * #EX1' #twel1 |
---|
| 153 | >shift_fst whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?)); |
---|
[1920] | 154 | @label_gen_elim #u2 |
---|
| 155 | @label_gen_elim #u3 |
---|
[1888] | 156 | @add_cost_expr_elim #u4 #l4 |
---|
[1920] | 157 | @label_gen_elim #u5 |
---|
[1888] | 158 | @add_cost_expr_elim #u6 #l6 |
---|
[1893] | 159 | [ cases (IH2 … EX2 u2) | cases (IH3 … EX2 u4) ] #trx' * #EXx' #twelx |
---|
[1888] | 160 | [ %{(tr1'⧺trx'⧺(Echarge l4))} | %{(tr1'⧺trx'⧺(Echarge l6))} ] |
---|
[1893] | 161 | whd in ⊢ (?(??%?)?); >EX1' |
---|
| 162 | whd in ⊢ (?(??%?)?); >label_expr_type >EXguard |
---|
| 163 | whd in ⊢ (?(??%?)?); whd in ⊢ (?(??(match % with [_⇒?|_⇒?])?)?); >EXx' |
---|
| 164 | normalize % // @twel_app // <(E0_right tr2) @twel_app /2/ |
---|
[1888] | 165 | | #ty #e1 #e2 #IH1 #IH2 #v #tr #EX #u |
---|
| 166 | cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem |
---|
| 167 | cases (bind_inversion ????? EX1rem) * * #EXguard #EXguardrem |
---|
[1893] | 168 | >shift_fst whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?)); |
---|
[1920] | 169 | @label_gen_elim #u2 |
---|
| 170 | @label_gen_elim #u3 |
---|
[1888] | 171 | @add_cost_expr_elim #u4 #l4 |
---|
| 172 | @add_cost_expr_elim #u5 #l5 |
---|
| 173 | [ cases (bind_inversion ????? EXguardrem) * #v2 #tr2 * #EX2 #EX2rem |
---|
| 174 | cases (bind_inversion ????? EX2rem) * * #EX3 #EX3rem |
---|
[1893] | 175 | -EX1rem -EXguardrem -EX2rem |
---|
| 176 | cases (IH1 … EX1 u) #tr1' * #EX1' #twel1 |
---|
| 177 | cases (IH2 … EX2 u2) #tr2' * #EX2' #twel2 |
---|
[1888] | 178 | %{(tr1'⧺(tr2'⧺E0)⧺Echarge l4)} |
---|
[1893] | 179 | whd in ⊢ (?(??%?)?); >EX1' |
---|
| 180 | whd in ⊢ (?(??%?)?); >label_expr_type >EX2' >EXguard |
---|
| 181 | whd in ⊢ (?(??%?)?); whd in ⊢ (?(??(match % with [_⇒?|_⇒?])?)?); |
---|
| 182 | whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >EX2' |
---|
| 183 | whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >label_expr_type >EX3 |
---|
[2050] | 184 | whd in EX3rem:(??%%) ⊢ %; destruct % [ 1,3: @refl | *: @twel_app // <(E0_right tr2) @twel_app /2/ ] |
---|
[1893] | 185 | | cases (IH1 … EX1 u) #tr1' * #EX1' #twel1 |
---|
[1888] | 186 | %{(tr1'⧺E0⧺Echarge l5)} |
---|
[1893] | 187 | whd in ⊢ (?(??%?)?); >EX1' |
---|
| 188 | whd in ⊢ (?(??%?)?); >label_expr_type >EXguard |
---|
[2050] | 189 | whd in EXguardrem:(??%%); destruct % // <(E0_right tr) @twel_app /2/ |
---|
[1888] | 190 | ] |
---|
| 191 | | #ty #e1 #e2 #IH1 #IH2 #v #tr #EX #u |
---|
| 192 | cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem |
---|
| 193 | cases (bind_inversion ????? EX1rem) * * #EXguard #EXguardrem |
---|
[1893] | 194 | >shift_fst whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?)); |
---|
[1920] | 195 | @label_gen_elim #u2 |
---|
[1888] | 196 | @add_cost_expr_elim #u4 #l4 |
---|
[1920] | 197 | @label_gen_elim #u3 |
---|
[1888] | 198 | @add_cost_expr_elim #u5 #l5 |
---|
[1893] | 199 | [ cases (IH1 … EX1 u) #tr1' * #EX1' #twel1 |
---|
[1888] | 200 | %{(tr1'⧺Echarge l4)} |
---|
[1893] | 201 | whd in ⊢ (?(??%?)?); >EX1' |
---|
| 202 | whd in ⊢ (?(??%?)?); >label_expr_type >EXguard |
---|
[2050] | 203 | whd in EXguardrem:(??%%) ⊢ %; destruct % // <(E0_right tr) /3/ |
---|
[1888] | 204 | | cases (bind_inversion ????? EXguardrem) * #v2 #tr2 * #EX2 #EX2rem |
---|
| 205 | cases (bind_inversion ????? EX2rem) * * #EX3 #EX3rem |
---|
[1893] | 206 | cases (IH1 … EX1 u) #tr1' * #EX1' #twel1 |
---|
| 207 | cases (IH2 … EX2 u4) #tr2' * #EX2' #twel2 |
---|
[1888] | 208 | %{(tr1'⧺(tr2'⧺E0)⧺Echarge l5)} |
---|
[1893] | 209 | whd in ⊢ (?(??%?)?); >EX1' |
---|
| 210 | whd in ⊢ (?(??%?)?); >label_expr_type >EX2' >EXguard |
---|
| 211 | whd in ⊢ (?(??%?)?); whd in ⊢ (?(??(match % with [_⇒?|_⇒?])?)?); |
---|
| 212 | whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >EX2' |
---|
| 213 | whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >label_expr_type >EX3 |
---|
[2050] | 214 | whd in EX3rem:(??%%) ⊢ %; destruct % // @twel_app // <(E0_right tr2) @twel_app /2/ |
---|
[1888] | 215 | ] |
---|
[1893] | 216 | | #ty #ty' #v #tr normalize /3/ |
---|
[1888] | 217 | | #ty #e1 #ty' #id #IH #b #o #tr #EX #u cases ty' in IH EX ⊢ %; |
---|
| 218 | [ 7: #id #fl #IH #EX |
---|
| 219 | cases (bind_inversion ????? EX) * * #b1 #o1 #tr1 * #EX1 #EX1rem |
---|
| 220 | cases (bind_inversion ????? EX1rem) #n * #EXoff #EXoffrem |
---|
| 221 | whd in EXoffrem:(???%); destruct >shift_fst >shift_fst |
---|
[1893] | 222 | cases (IH … EX1 u) #tr1' * #EX1' #twel1 |
---|
| 223 | %{tr1'} % // |
---|
[1888] | 224 | whd in ⊢ (??%?); whd in ⊢ (??(match % with [_⇒?|_⇒?])?); >EX1' |
---|
| 225 | whd in ⊢ (??%?); >EXoff whd in ⊢ (??%?); @refl |
---|
| 226 | | 8: #id #fl #IH #EX |
---|
| 227 | cases (bind_inversion ????? EX) * * #b1 #o1 #tr1 * #EX1 #EX1rem |
---|
| 228 | whd in EX1rem:(???%); destruct >shift_fst >shift_fst |
---|
[1893] | 229 | cases (IH … EX1 u) #tr1' * #EX1' #twel1 |
---|
| 230 | %{tr1'} % // |
---|
[1888] | 231 | whd in ⊢ (??%?); whd in ⊢ (??(match % with [_⇒?|_⇒?])?); >EX1' |
---|
| 232 | whd in ⊢ (??%?); @refl |
---|
| 233 | | *: normalize #A #B try #C try #D try #F destruct |
---|
| 234 | ] |
---|
| 235 | | #ty #l #e1 #IH #v #tr #EX #u |
---|
| 236 | cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem |
---|
| 237 | whd in EX1rem:(???%); destruct |
---|
[1893] | 238 | cases (IH … EX1 u) #tr1' * #EX1' #twel1 %{(tr1'@Echarge l)} |
---|
| 239 | >shift_fst >shift_fst whd in ⊢ (?(??%?)?); >EX1' |
---|
| 240 | whd in ⊢ (?(??%?)?); /3/ |
---|
[1888] | 241 | | #e1 #ty #NLV #b #o #tr #EX @⊥ |
---|
| 242 | cases e1 in NLV EX; normalize // |
---|
| 243 | #A #B #C try #D try #F destruct |
---|
| 244 | ] qed. |
---|
[1893] | 245 | |
---|
[1920] | 246 | lemma label_exprs_ok : ∀ge,ge'. |
---|
[2105] | 247 | related_globals … label_fundef ge ge' → |
---|
[1920] | 248 | ∀en,m,es,vs,tr. |
---|
| 249 | exec_exprlist ge en m es = OK … 〈vs,tr〉 → |
---|
| 250 | ∀u. ∃tr'. exec_exprlist ge' en m (\fst (label_exprs es u)) = OK … 〈vs,tr'〉 ∧ |
---|
| 251 | trace_with_extra_labels tr tr'. |
---|
| 252 | #ge #ge' #RG #en #m #es elim es |
---|
| 253 | [ #vs #tr #EX whd in EX:(??%?); destruct #u %{E0} /2/ |
---|
| 254 | | #e #tl #IH #vs #tr #EX |
---|
| 255 | cases (bind_inversion ????? EX) -EX * #v1 #tr1 * #EX1 #EX |
---|
| 256 | cases (bind_inversion ????? EX) -EX * #tl' #tr' * #EX2 #EX |
---|
| 257 | whd in EX:(??%%); destruct |
---|
| 258 | #u whd in match (label_exprs ??); @label_gen_elim #u' >shift_fst |
---|
| 259 | cases (proj1 ?? (label_expr_ok ge ge' en m RG) ??? EX1 u) #tr1' * #EX1' #T1 |
---|
| 260 | cases (IH … EX2 u') #tr'' * #EX2' #T2 |
---|
| 261 | % [2: % [ whd in ⊢ (??%?); >EX1' in ⊢ (??%?); |
---|
| 262 | whd in ⊢ (??%?); >EX2' in ⊢ (??%?); @refl |
---|
| 263 | | /2/ ] | skip ] |
---|
| 264 | ] qed. |
---|
| 265 | |
---|
[1893] | 266 | |
---|
[1930] | 267 | (* Now we move on to describe the simulation relation. First, relate the |
---|
| 268 | continuations. *) |
---|
[1920] | 269 | inductive cont_with_labels : cont → cont → Prop ≝ |
---|
| 270 | | cwl_stop : cont_with_labels Kstop Kstop |
---|
| 271 | | cwl_seq : ∀u,s,k,k'. cont_with_labels k k' → cont_with_labels (Kseq s k) (Kseq (\fst (label_statement s u)) k') |
---|
| 272 | | cwl_while : ∀ue,e,us,s,cs,cpost,k,k'. |
---|
| 273 | cont_with_labels k k' → |
---|
| 274 | cont_with_labels (Kwhile e s k) (Kwhile (\fst (label_expr e ue)) (Scost cs (\fst (label_statement s us))) (Kseq (Scost cpost Sskip) k')) |
---|
| 275 | | cwl_dowhile : ∀ue,e,us,s,cs,cpost,k,k'. |
---|
| 276 | cont_with_labels k k' → |
---|
| 277 | cont_with_labels (Kdowhile e s k) (Kdowhile (\fst (label_expr e ue)) (Scost cs (\fst (label_statement s us))) (Kseq (Scost cpost Sskip) k')) |
---|
| 278 | | cwl_for1 : ∀ue,e,us1,s1,us2,s2,cs,cpost,k,k'. |
---|
| 279 | cont_with_labels k k' → |
---|
| 280 | cont_with_labels (Kseq (Sfor Sskip e s1 s2) k) (Kseq (Sfor Sskip (\fst (label_expr e ue)) (\fst (label_statement s1 us1)) (Scost cs (\fst (label_statement s2 us2)))) (Kseq (Scost cpost Sskip) k')) |
---|
| 281 | | cwl_for2 : ∀ue,e,us1,s1,us2,s2,cs,cpost,k,k'. cont_with_labels k k' → cont_with_labels (Kfor2 e s1 s2 k) (Kfor2 (\fst (label_expr e ue)) (\fst (label_statement s1 us1)) (Scost cs (\fst (label_statement s2 us2))) (Kseq (Scost cpost Sskip) k')) |
---|
| 282 | | cwl_for3 : ∀ue,e,us1,s1,us2,s2,cs,cpost,k,k'. cont_with_labels k k' → cont_with_labels (Kfor3 e s1 s2 k) (Kfor3 (\fst (label_expr e ue)) (\fst (label_statement s1 us1)) (Scost cs (\fst (label_statement s2 us2))) (Kseq (Scost cpost Sskip) k')) |
---|
| 283 | | cwl_switch : ∀k,k'. cont_with_labels k k' → cont_with_labels (Kswitch k) (Kswitch k') |
---|
| 284 | | cwl_call : ∀r,f,en,k,k'. cont_with_labels k k' → cont_with_labels (Kcall r f en k) (Kcall r (label_function f) en k') |
---|
| 285 | | cwl_seqls : ∀ls,u,k,k'. cont_with_labels k k' → |
---|
| 286 | cont_with_labels (Kseq (seq_of_labeled_statement ls) k) (Kseq (seq_of_labeled_statement (\fst (label_lstatements ls u))) k'). |
---|
[1893] | 287 | |
---|
[1920] | 288 | lemma call_cont_with_labels : ∀k,k'. |
---|
| 289 | cont_with_labels k k' → |
---|
| 290 | cont_with_labels (call_cont k) (call_cont k'). |
---|
| 291 | #k0 #k0' #K elim K /2/ |
---|
| 292 | qed. |
---|
| 293 | |
---|
[1930] | 294 | (* Now define almost all of the simulation relation... *) |
---|
[1922] | 295 | inductive state_with_labels_partial : state → state → Prop ≝ |
---|
| 296 | | swl_state : ∀f,us,s,k,k',e,m. cont_with_labels k k' → state_with_labels_partial (State f s k e m) (State (label_function f) (\fst (label_statement s us)) k' e m) |
---|
[1920] | 297 | (* Extra matching states that we can reach that don't quite correspond to the |
---|
| 298 | labelling function *) |
---|
| 299 | | swl_whilestate : ∀f,ua,a,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' → |
---|
[1922] | 300 | state_with_labels_partial (State f (Swhile a s) k e m) (State (label_function f) (Swhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m) |
---|
[1920] | 301 | | swl_dowhilestate : ∀f,ua,a,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' → |
---|
[1922] | 302 | state_with_labels_partial (State f (Sdowhile a s) k e m) (State (label_function f) (Sdowhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m) |
---|
[1920] | 303 | | swl_forstate : ∀f,ua2,a2,us3,s3,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' → |
---|
[1922] | 304 | state_with_labels_partial (State f (Sfor Sskip a2 s3 s) k e m) (State (label_function f) (Sfor Sskip (\fst (label_expr a2 ua2)) (\fst (label_statement s3 us3)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m) |
---|
| 305 | (* and the rest *) |
---|
| 306 | | swl_callstate : ∀fd,args,k,k',m. cont_with_labels k k' → state_with_labels_partial (Callstate fd args k m) (Callstate (label_fundef fd) args k' m) |
---|
| 307 | | swl_returnstate : ∀res,k,k',m. cont_with_labels k k' → state_with_labels_partial (Returnstate res k m) (Returnstate res k' m) |
---|
| 308 | | swl_finalstate : ∀r. state_with_labels_partial (Finalstate r) (Finalstate r) |
---|
[2011] | 309 | . |
---|
[1922] | 310 | |
---|
[1930] | 311 | (* ... and add the states where the cases from switch statements are expanded. |
---|
| 312 | We do these separately because in the LSdefault case we have to execute a |
---|
| 313 | cost label alongside an arbitrary statement, and we want to reuse the result |
---|
| 314 | on arbitrary statements we get for state_with_labels_partial. *) |
---|
[1922] | 315 | inductive state_with_labels : state → state → Prop ≝ |
---|
| 316 | | swl_partial : ∀s,s'. state_with_labels_partial s s' → state_with_labels s s' |
---|
[1920] | 317 | | swl_switchstate : ∀f,u,ls,k,k',e,m. cont_with_labels k k' → |
---|
| 318 | state_with_labels (State f (seq_of_labeled_statement ls) k e m) |
---|
| 319 | (State (label_function f) (seq_of_labeled_statement (\fst (label_lstatements ls u))) k' e m) |
---|
| 320 | . |
---|
| 321 | |
---|
[1930] | 322 | (* TODO: this (or something like it) ought to be elsewhere. *) |
---|
[1920] | 323 | inductive plus (ge:genv) : state → trace → state → Prop ≝ |
---|
| 324 | | plus_one : ∀s1,tr,s2. exec_step ge s1 = OK … 〈tr,s2〉 → plus ge s1 tr s2 |
---|
| 325 | | plus_succ : ∀s1,tr,s2,tr',s3. exec_step ge s1 = OK … 〈tr,s2〉 → plus ge s2 tr' s3 → plus ge s1 (tr⧺tr') s3. |
---|
| 326 | |
---|
[1930] | 327 | (* Some details are invariant under labelling. *) |
---|
[1920] | 328 | lemma label_function_return : ∀f. |
---|
| 329 | fn_return (label_function f) = fn_return f. |
---|
| 330 | * #rty #params #vars #body |
---|
| 331 | whd in ⊢ (??(?%)?); |
---|
| 332 | cases (label_statement ??) #body' #u' |
---|
| 333 | whd in ⊢ (??(?%)?); |
---|
| 334 | cases (add_cost_before ??) #body'' #u'' |
---|
| 335 | // |
---|
| 336 | qed. |
---|
| 337 | |
---|
| 338 | lemma label_expr_fun_typeof : ∀a,u. |
---|
| 339 | fun_typeof (\fst (label_expr a u)) = fun_typeof a. |
---|
| 340 | #a #u whd in ⊢ (??%?); >label_expr_type @refl |
---|
| 341 | qed. |
---|
| 342 | |
---|
| 343 | lemma label_fundef_typeof_fundef : ∀fd. |
---|
| 344 | type_of_fundef (label_fundef fd) = type_of_fundef fd. |
---|
| 345 | * // |
---|
| 346 | * #rty #args #vars #body |
---|
| 347 | normalize cases (label_statement ??) #body' #u |
---|
| 348 | normalize cases (fresh ??) // |
---|
| 349 | qed. |
---|
| 350 | |
---|
[1930] | 351 | lemma label_fn_params : ∀f. |
---|
| 352 | fn_params (label_function f) = fn_params f. |
---|
| 353 | * #rty #params #vars #s whd in ⊢ (??(?%)?); @breakup_pair @breakup_pair // |
---|
| 354 | qed. |
---|
| 355 | |
---|
| 356 | lemma label_fn_vars : ∀f. |
---|
| 357 | fn_vars (label_function f) = fn_vars f. |
---|
| 358 | * #rty #params #vars #s whd in ⊢ (??(?%)?); @breakup_pair @breakup_pair // |
---|
| 359 | qed. |
---|
| 360 | |
---|
| 361 | (* Some annoying rewrite rules *) |
---|
| 362 | lemma exec_lvalue_labelled : ∀ge,e,m,a,ty,u. |
---|
| 363 | exec_lvalue ge e m (\fst (label_expr (Expr a ty) u)) = |
---|
| 364 | exec_lvalue' ge e m (\fst (label_expr_descr a u ty)) ty. |
---|
| 365 | #ge #e #m #a #ty #u |
---|
| 366 | whd in ⊢ (??(????(???%))?); >shift_fst @refl |
---|
| 367 | qed. |
---|
| 368 | |
---|
[1920] | 369 | lemma opt_find_funct : ∀ge,ge',m,vf,fd. |
---|
[2105] | 370 | related_globals … label_fundef ge ge' → |
---|
[1986] | 371 | opt_to_io io_out io_in … m (find_funct … ge vf) = Value … fd → |
---|
| 372 | opt_to_io io_out io_in … m (find_funct … ge' vf) = Value … (label_fundef fd). |
---|
[1920] | 373 | #ge #ge' #m #vf #fd #RG |
---|
| 374 | lapply (rg_find_funct … RG … vf fd) |
---|
| 375 | cases (find_funct … vf) |
---|
| 376 | [ #_ #E normalize in E; destruct |
---|
| 377 | | #fd' #H #E normalize in E; destruct >(H (refl ??)) // |
---|
| 378 | ] qed. |
---|
| 379 | |
---|
| 380 | lemma labelled_not_skip : ∀s,u. |
---|
| 381 | s ≠ Sskip → |
---|
| 382 | (\fst (label_statement s u)) ≠ Sskip. |
---|
| 383 | * #u |
---|
| 384 | [ * #H cases (H (refl ??)) |
---|
| 385 | | *: #a try #b try #c try #d try #e |
---|
| 386 | (* Use the state-monad-like structure of the labelling function to break |
---|
| 387 | it up *) |
---|
| 388 | whd in match (label_statement ??); |
---|
| 389 | repeat @(breakup_pair ???? (λx.\fst x ≠ Sskip)) |
---|
| 390 | % #E destruct |
---|
| 391 | ] qed. |
---|
| 392 | |
---|
| 393 | lemma labelled_is_not_skip : ∀s,u. |
---|
| 394 | s ≠ Sskip → |
---|
| 395 | ∃pf. is_Sskip (\fst (label_statement s u)) = inr … pf. |
---|
| 396 | #s #u #NE |
---|
| 397 | cases (is_Sskip ?) |
---|
| 398 | [ #E @⊥ @(absurd ? E) @labelled_not_skip // |
---|
| 399 | | /2/ |
---|
| 400 | ] qed. |
---|
| 401 | |
---|
| 402 | lemma label_select_ls : ∀sz,i,ls,u. |
---|
| 403 | ∃u'. |
---|
| 404 | select_switch sz i (\fst (label_lstatements ls u)) = |
---|
| 405 | \fst (label_lstatements (select_switch sz i ls) u'). |
---|
| 406 | #sz #i #ls @(labeled_statements_ind … ls) |
---|
| 407 | [ #s #u % [2: whd in match (label_lstatements ??); |
---|
| 408 | @label_gen_elim #u1 >shift_fst @refl | skip ] |
---|
| 409 | | #sz' #i' #s #tl #IH #u |
---|
| 410 | whd in match (label_lstatements ??); |
---|
| 411 | whd in match (select_switch ?? (LScase ????)); |
---|
| 412 | @intsize_eq_elim_elim |
---|
| 413 | [ #NE |
---|
| 414 | @label_gen_elim #u1 @label_gen_elim #u2 @label_gen_elim #u3 |
---|
| 415 | cases (IH u2) |
---|
| 416 | #u4 #E %{u4} whd in ⊢ (??%?); |
---|
| 417 | >intsize_eq_elim_false // |
---|
| 418 | | #E <E in i' ⊢ %; #i' whd |
---|
| 419 | @eq_bv_elim |
---|
| 420 | [ #Ei >Ei |
---|
| 421 | %{u} |
---|
| 422 | whd in match (label_lstatements (if ? then ? else ?) ?); |
---|
| 423 | @label_gen_elim #u1 @label_gen_elim #u2 @label_gen_elim #u3 |
---|
| 424 | whd in ⊢ (??%?); |
---|
| 425 | >intsize_eq_elim_true |
---|
| 426 | >eq_bv_true |
---|
| 427 | @refl |
---|
| 428 | | #NEi |
---|
| 429 | @label_gen_elim #u1 @label_gen_elim #u2 @label_gen_elim #u3 |
---|
| 430 | whd in ⊢ (??(λ_.??%?)); |
---|
| 431 | >intsize_eq_elim_true |
---|
| 432 | >eq_bv_false // |
---|
| 433 | ] |
---|
| 434 | ] |
---|
| 435 | ] qed. |
---|
| 436 | |
---|
[1930] | 437 | (* Break up labelling function in one go for statements. *) |
---|
[1920] | 438 | lemma blindly_label : ∀u,s. ∀P:statement → Prop. |
---|
| 439 | match s with |
---|
| 440 | [ Sskip ⇒ P Sskip |
---|
| 441 | | Sassign e1 e2 ⇒ ∀u1,u2. P (Sassign (\fst (label_expr e1 u1)) (\fst (label_expr e2 u2))) |
---|
| 442 | | Scall eo e args ⇒ ∀u1,u2,u3. P (Scall (\fst (label_opt_expr eo u1)) (\fst (label_expr e u2)) (\fst (label_exprs args u3))) |
---|
| 443 | | Ssequence s1 s2 ⇒ ∀u1,u2. P (Ssequence (\fst (label_statement s1 u1)) (\fst (label_statement s2 u2))) |
---|
| 444 | | Sifthenelse e s1 s2 ⇒ ∀u1,u2,u3,c2,c3. P (Sifthenelse (\fst (label_expr e u1)) (Scost c2 (\fst (label_statement s1 u2))) (Scost c3 (\fst (label_statement s2 u3)))) |
---|
| 445 | | Swhile e s1 ⇒ ∀u1,u2,cs,cpost. P (Ssequence (Swhile (\fst (label_expr e u1)) (Scost cs (\fst (label_statement s1 u2)))) (Scost cpost Sskip)) |
---|
| 446 | | Sdowhile e s1 ⇒ ∀u1,u2,cs,cpost. P (Ssequence (Sdowhile (\fst (label_expr e u1)) (Scost cs (\fst (label_statement s1 u2)))) (Scost cpost Sskip)) |
---|
| 447 | | Sfor s1 e s2 s3 ⇒ ∀u1,u2,u3,u4,c3,c4. P (Ssequence (Sfor (\fst (label_statement s1 u1)) (\fst (label_expr e u2)) (\fst (label_statement s2 u3)) (Scost c3 (\fst (label_statement s3 u4)))) (Scost c4 Sskip)) |
---|
| 448 | | Sbreak ⇒ P Sbreak |
---|
| 449 | | Scontinue ⇒ P Scontinue |
---|
| 450 | | Sreturn eo ⇒ ∀u1. P (Sreturn (\fst (label_opt_expr eo u1))) |
---|
| 451 | | Sswitch e ls ⇒ ∀u1,u2. P (Sswitch (\fst (label_expr e u1)) (\fst (label_lstatements ls u2))) |
---|
| 452 | | Slabel l s1 ⇒ ∀u1,cs. P (Slabel l (Scost cs (\fst (label_statement s1 u1)))) |
---|
| 453 | | Sgoto l ⇒ P (Sgoto l) |
---|
| 454 | | Scost c s1 ⇒ ∀u1. P (Scost c (\fst (label_statement s1 u1))) |
---|
| 455 | ] → P (\fst (label_statement s u)). |
---|
| 456 | #u * // #A #B #C try #D try #E try #F whd in match (label_statement ??); |
---|
| 457 | @label_gen_elim #u1 // |
---|
| 458 | @label_gen_elim #u2 // |
---|
| 459 | [ 6: >shift_fst // |
---|
| 460 | | *: @label_gen_elim #u3 // |
---|
| 461 | @label_gen_elim #u4 |
---|
| 462 | [ @label_gen_elim #u5 >shift_fst >shift_fst // |
---|
| 463 | | 2,3: >shift_fst >shift_fst // |
---|
| 464 | | @label_gen_elim #u5 >shift_fst >shift_fst >shift_fst // |
---|
| 465 | ] |
---|
| 466 | ] qed. |
---|
| 467 | |
---|
[1930] | 468 | (* Apply induction hypothesis in label_find_label proof below while getting |
---|
| 469 | Matita to infer the continuations k0 and k0', and the universe u0, rather |
---|
| 470 | than having to give them explicitly. *) |
---|
[1920] | 471 | lemma lfl_IH : ∀s0,lbl. |
---|
| 472 | ∀C:option (statement×cont) → option (statement×cont) → Prop. |
---|
| 473 | ∀IH:cont → cont → universe CostTag → Prop. |
---|
| 474 | (∀k,k',u. cont_with_labels k k' → IH k k' u) → |
---|
| 475 | ∀k0,k0',u0. cont_with_labels k0 k0' → |
---|
| 476 | (IH k0 k0' u0 → |
---|
| 477 | C (find_label lbl s0 k0) (find_label lbl (\fst (label_statement s0 u0)) k0')) → |
---|
| 478 | C (find_label lbl s0 k0) (find_label lbl (\fst (label_statement s0 u0)) k0'). |
---|
| 479 | /3/ |
---|
| 480 | qed. |
---|
| 481 | |
---|
[1930] | 482 | (* Finding a goto label in a cost-labelled program gives a labelled version of |
---|
| 483 | the statement and continuation found by the original function, if any. *) |
---|
[1920] | 484 | lemma label_find_label : ∀lbl,s,k,k',u. |
---|
| 485 | cont_with_labels k k' → |
---|
| 486 | match find_label lbl s k with |
---|
| 487 | [ Some r' ⇒ let 〈s1,k1〉 ≝ r' in |
---|
| 488 | ∃u',cs,k1'. |
---|
| 489 | find_label lbl (\fst (label_statement s u)) k' = Some ? 〈Scost cs (\fst (label_statement s1 u')), k1'〉 ∧ |
---|
| 490 | cont_with_labels k1 k1' |
---|
| 491 | | None ⇒ find_label lbl (\fst (label_statement s u)) k' = None ? |
---|
| 492 | ]. |
---|
| 493 | #lbl #s @(statement_ind2 ? (λls. |
---|
| 494 | ∀k,k',u. |
---|
| 495 | cont_with_labels k k' → |
---|
| 496 | match find_label_ls lbl ls k with |
---|
| 497 | [ Some r' ⇒ let 〈s1,k1〉 ≝ r' in |
---|
| 498 | ∃u',cs,k1'. |
---|
| 499 | find_label_ls lbl (\fst (label_lstatements ls u)) k' = Some ? 〈Scost cs (\fst (label_statement s1 u')), k1'〉 ∧ |
---|
| 500 | cont_with_labels k1 k1' |
---|
| 501 | | None ⇒ find_label_ls lbl (\fst (label_lstatements ls u)) k' = None ? |
---|
| 502 | ]) |
---|
| 503 | … s) |
---|
| 504 | [ #k #k' #u #F @refl |
---|
| 505 | | #e1 #e2 #k #k' #u #K @blindly_label #u1 #u2 whd @refl |
---|
| 506 | | #e0 #e #args #k #k' #u #K @blindly_label #u1 #u2 #u3 whd @refl |
---|
| 507 | | #sA #sB #IH1 #IH2 #k #k' #u #K @blindly_label #u1 #u2 whd in match (find_label ???); |
---|
| 508 | whd in match (find_label ?? k'); |
---|
| 509 | @(lfl_IH sA … IH1) [ /2/ ] |
---|
| 510 | cases (find_label ???) |
---|
| 511 | [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND1' |
---|
| 512 | @(lfl_IH … IH2) [ // ] |
---|
| 513 | cases (find_label ???) |
---|
| 514 | [ whd in ⊢ (% → %); #FIND2' whd in ⊢ (??%?); >FIND1' >FIND2' @refl |
---|
| 515 | | * #s3 #k3 whd in ⊢ (% → %); * #u3 * #cs * #k1' * #FIND2' #K1' |
---|
| 516 | % [2: %{cs} %{k1'} % // whd in ⊢ (??%?); >FIND1' in ⊢ (??%?); >FIND2' in ⊢ (??%?); @refl | skip ] |
---|
| 517 | ] |
---|
| 518 | | * #sA' #kA' whd in ⊢ (% → %); |
---|
| 519 | * #u1' * #cs * #k1' * #FA' #K' |
---|
| 520 | % [2: %{cs} %{k1'} % [ whd in ⊢ (??%?); >FA' in ⊢ (??%?); @refl | // ] |skip] |
---|
| 521 | ] |
---|
| 522 | | #e #s1 #s2 #IH1 #IH2 #k #k' #u @blindly_label #u1 #u2 #u3 #c2 #c3 #K |
---|
| 523 | whd in match (find_label ?? k); whd in match (find_label ?? k'); |
---|
| 524 | whd in match (find_label ?? k'); |
---|
| 525 | @(lfl_IH … IH1) [ // ] cases (find_label ???) |
---|
| 526 | [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND1' |
---|
| 527 | lapply (IH2 k k' u3 K) cases (find_label ???) |
---|
| 528 | [ whd in ⊢ (% → %); #FIND2' |
---|
| 529 | whd in match (find_label ???); >FIND1' |
---|
| 530 | whd in match (find_label ???); >FIND2' @refl |
---|
| 531 | | * #s2' #k2' * #u4 * #cs * #k1' * #FIND2' #K2' |
---|
| 532 | % [2: % [2: % [2: % [ whd in ⊢ (??%?); |
---|
| 533 | whd in match (find_label ???); >FIND1' in ⊢ (??%?); |
---|
| 534 | whd in match (find_label ???); >FIND2' in ⊢ (??%?); @refl |
---|
| 535 | | // ]|skip]|skip]|skip] |
---|
| 536 | ] |
---|
| 537 | | * #s1' #k1 whd in ⊢ (% → %); * #u4 * #cs * #k1' * #FIND1' #K1' |
---|
| 538 | % [2: % [2: % [2: % [ |
---|
| 539 | whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' in ⊢ (??%?); |
---|
| 540 | @refl | // ] |skip ]| skip ]| skip ] |
---|
| 541 | ] |
---|
| 542 | | #e #s0 #IH #k #k' #u #K @blindly_label #u1 #u2 #cs #cpost |
---|
| 543 | whd in match (find_label ?? k); normalize in match (find_label ?? k'); |
---|
| 544 | @(lfl_IH s0 … IH) [ /2/ ] |
---|
| 545 | cases (find_label ???) |
---|
| 546 | [ whd in ⊢ (% → %); #FIND1' |
---|
| 547 | whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' @refl |
---|
| 548 | | * #s1 #k1 * #u4 * #cs * #k1' * #FIND1' #K1' |
---|
| 549 | % [2: % [2: % [2: % [ |
---|
| 550 | whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' in ⊢ (??%?); |
---|
| 551 | @refl | // ]| skip ]| skip ]| skip ] |
---|
| 552 | ] |
---|
| 553 | | #e #s0 #IH #k #k' #u #K @blindly_label #u1 #u2 #cs #cpost |
---|
| 554 | whd in match (find_label ?? k); normalize in match (find_label ?? k'); |
---|
| 555 | @(lfl_IH s0 … IH) [ /2/ ] |
---|
| 556 | cases (find_label ???) |
---|
| 557 | [ whd in ⊢ (% → %); #FIND1' |
---|
| 558 | whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' @refl |
---|
| 559 | | * #s1 #k1 * #u4 * #cs * #k1' * #FIND1' #K1' |
---|
| 560 | % [2: % [2: % [2: % [ |
---|
| 561 | whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' in ⊢ (??%?); |
---|
| 562 | @refl | // ]| skip ]| skip ]| skip ] |
---|
| 563 | ] |
---|
| 564 | | #s1 #e #s2 #s3 #IH1 #IH2 #IH3 #k #k' #u #K @blindly_label #u1 #u2 #u3 #u4 #c3 #c4 |
---|
| 565 | whd in match (find_label ???); normalize in match (find_label ?? k'); |
---|
| 566 | @(lfl_IH s1 … IH1) [ /2/ ] |
---|
| 567 | cases (find_label ???) |
---|
| 568 | [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND1' >FIND1' |
---|
| 569 | @(lfl_IH s3 … IH3) [ /2/ ] |
---|
| 570 | cases (find_label ???) |
---|
| 571 | [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND3' >FIND3' |
---|
| 572 | @(lfl_IH s2 … IH2) [ /2/ ] |
---|
| 573 | cases (find_label ???) |
---|
| 574 | [ whd in ⊢ (% → %); #FIND2' >FIND2' @refl |
---|
| 575 | | * #s2' #k2' * #u2' * #cs' * #k1' * #FIND2' #K2' |
---|
| 576 | % [2: % [2: % [2: % [ |
---|
| 577 | whd in ⊢ (??%?); >FIND2' in ⊢ (??%?); @refl |
---|
| 578 | | // ]| skip ]| skip ]| skip ] |
---|
| 579 | ] |
---|
| 580 | | * #s3' #k3' * #u3' * #cs' * #k1' * #FIND3' #K3' |
---|
| 581 | % [2: % [2: % [2: % [ |
---|
| 582 | >FIND3' in ⊢ (??%?); whd in ⊢ (??%?); @refl |
---|
| 583 | | // ]| skip ]| skip ]| skip ] |
---|
| 584 | ] |
---|
| 585 | | * #s1' #k1' * #u1' * #cs' * #k1' * #FIND1' #K1' |
---|
| 586 | % [2: % [2: % [2: % [ |
---|
| 587 | >FIND1' in ⊢ (??%?); whd in ⊢ (??%?); @refl |
---|
| 588 | | // ]| skip ]| skip ]| skip ] |
---|
| 589 | ] |
---|
| 590 | | // |
---|
| 591 | | // |
---|
| 592 | | #eo #k #k' #u @blindly_label #u1 // |
---|
| 593 | | #e #ls #IH #k #k' #u #K @blindly_label #u1 #u2 |
---|
| 594 | normalize in match (find_label ???); normalize in match (find_label ???); |
---|
| 595 | lapply (IH (Kswitch k) (Kswitch k') u2 ?) [/2/] cases (find_label_ls ???) |
---|
| 596 | [ whd in ⊢ (% → %); // |
---|
| 597 | | * #s1' #k1' * #u' * #cs * #k'' * #FIND' #K' |
---|
| 598 | % [2: % [2: % [2: % [ @FIND' | // ]|skip ]|skip]|skip] |
---|
| 599 | ] |
---|
| 600 | | #l #s0 #IH #k #k' #u #K @blindly_label #u1 #cs |
---|
| 601 | whd in match (find_label ???); whd in match (find_label ?? k'); |
---|
| 602 | cases (ident_eq lbl l) |
---|
| 603 | [ #E destruct whd |
---|
| 604 | % [2: % [2: % [2: % [ @refl | // ]|skip ]|skip ]| skip ] |
---|
| 605 | | #NE whd in ⊢ (match % with [_⇒?|_⇒?]); |
---|
| 606 | normalize in match (find_label ?? k'); |
---|
| 607 | @(lfl_IH s0 … IH) [ // ] |
---|
| 608 | cases (find_label ???) |
---|
| 609 | [ // |
---|
| 610 | | * #s0' #k0' * #u' * #cs0 * #k1' * #FIND0 #K0 |
---|
| 611 | % [2: % [2: % [2: % [ @FIND0 | // ]|skip ]|skip]|skip] |
---|
| 612 | ] |
---|
| 613 | ] |
---|
| 614 | | // |
---|
| 615 | | #l #s0 #IH #k #k' #u #K @blindly_label #u1 /2/ |
---|
| 616 | | #s0 #IH #k #k' #u whd in match (label_lstatements ??); |
---|
| 617 | @label_gen_elim #u1 >shift_fst >shift_fst |
---|
| 618 | whd in match (find_label_ls ???); whd in match (find_label_ls ???); |
---|
| 619 | @IH |
---|
| 620 | | #sz #i #s0 #tl #IH1 #IH2 #k #k' #u #K |
---|
| 621 | whd in match (label_lstatements ??); @label_gen_elim #u1 @label_gen_elim #u2 |
---|
| 622 | @label_gen_elim #u3 >shift_fst |
---|
| 623 | whd in match (find_label_ls ???); normalize in match (find_label_ls ?? k'); |
---|
| 624 | @(lfl_IH s0 … IH1) [ /2/ ] |
---|
| 625 | cases (find_label ???) |
---|
| 626 | [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND0 >FIND0 |
---|
| 627 | lapply (IH2 k k' u2 K) cases (find_label_ls ???) |
---|
| 628 | [ whd in ⊢ (% → %); #FINDtl >FINDtl @refl |
---|
| 629 | | * #stl #ktl // |
---|
| 630 | ] |
---|
| 631 | | * #s0' #k0' whd in ⊢ (% → %); |
---|
| 632 | * #u' * #cs * #k1' * #FIND0 #K0 >FIND0 |
---|
| 633 | % [2: % [2: % [2: % [ @refl | // ] | skip ] | skip ] | skip ] |
---|
| 634 | ] |
---|
| 635 | ] qed. |
---|
| 636 | |
---|
| 637 | lemma label_find_label_fn : ∀lbl,f,k,k',s1,k1. |
---|
| 638 | cont_with_labels k k' → |
---|
| 639 | find_label lbl (fn_body f) (call_cont k) = Some ? 〈s1,k1〉 → |
---|
| 640 | ∃u',cs,k1'. |
---|
| 641 | find_label lbl (fn_body (label_function f)) (call_cont k') = Some ? 〈Scost cs (\fst (label_statement s1 u')), k1'〉 ∧ |
---|
| 642 | cont_with_labels k1 k1'. |
---|
| 643 | #lbl * #rty #args #vars #s #k #k' #s1 #k1 #K #FIND |
---|
| 644 | whd in match (label_function ?); |
---|
| 645 | @label_gen_elim #u1 @label_gen_elim #u2 >shift_fst |
---|
| 646 | lapply (label_find_label lbl s (call_cont k) (call_cont k') (new_universe ?) ?) |
---|
| 647 | [ /2/ ] |
---|
| 648 | >FIND // |
---|
| 649 | qed. |
---|
| 650 | |
---|
[1930] | 651 | |
---|
[1922] | 652 | (* We show the main simulation in two stages. First, we show it for all states |
---|
| 653 | in the relation *except* those for labeled_statements, then we'll show the |
---|
| 654 | whole thing. This is so that we can appeal to the other cases in the proof |
---|
| 655 | for labeled_statements. *) |
---|
| 656 | lemma step_with_labels_partial : ∀ge,ge'. |
---|
[2105] | 657 | related_globals … label_fundef ge ge' → |
---|
[1920] | 658 | ∀s1,s1',tr,s2. |
---|
[1922] | 659 | state_with_labels_partial s1 s1' → |
---|
[1920] | 660 | exec_step ge s1 = Value … 〈tr,s2〉 → |
---|
[1922] | 661 | ∃tr',s2'. plus ge' s1' tr' s2' ∧ |
---|
| 662 | trace_with_extra_labels tr tr' ∧ |
---|
| 663 | state_with_labels s2 s2'. |
---|
[1930] | 664 | |
---|
| 665 | (* General plan is like the expressions result, except that we do case analysis |
---|
| 666 | on the simulation first, then: break up the original execution, break up the |
---|
| 667 | cost labelling, use the earlier results to deal with expressions, then |
---|
| 668 | run the labelled version for enough steps. We try to avoid having to write |
---|
| 669 | out the final trace and state and "skip" them afterwards. *) |
---|
[1920] | 670 | #ge #ge' #RG #Xs1 #Xs1' #tr #s2 * |
---|
| 671 | [ #f #us #s #k #k' #e #m #KL cases s |
---|
| 672 | [ #EX inversion KL |
---|
| 673 | [ #E1 #E2 #_ destruct %{tr} |
---|
| 674 | whd in EX:(??%?); |
---|
| 675 | lapply (refl ? (fn_return f)) cases (fn_return f) in ⊢ (???% → ?); |
---|
[2000] | 676 | [ #E >E in EX; whd in ⊢ (??%% → ?); #EX' destruct %{(Returnstate Vundef Kstop (free_list m (blocks_of_env e)))} |
---|
[1920] | 677 | % [ % [ @plus_one whd in ⊢ (??%?); >label_function_return >E @refl |
---|
[1922] | 678 | | // ] | /3/ ] |
---|
[1920] | 679 | | *: #A [ 1,3,5,6,7,8: #B | 4: #B #C ] #E >E in EX; #EX whd in EX:(??%%); destruct |
---|
| 680 | ] |
---|
| 681 | | #u #s0 #k0 #k0' #K #_ #E1 #E2 #E3 destruct %{tr} |
---|
| 682 | %{(State (label_function f) (\fst (label_statement s0 u)) k0' e m)} |
---|
| 683 | whd in EX:(??%%); destruct |
---|
[1922] | 684 | % [ % [ @plus_one @refl | // ] | /3/ ] |
---|
[1920] | 685 | | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct %{tr} |
---|
| 686 | whd in EX:(??%%); destruct |
---|
[1922] | 687 | % [ 2: % [ % [ @plus_one @refl | // ] | @swl_partial @swl_whilestate // ] | skip ] |
---|
[1920] | 688 | | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct |
---|
| 689 | cases (bindIO_inversion ??????? EX) * #ve #tre * #EXe #EXrem |
---|
| 690 | cases (bindIO_inversion ??????? EXrem) * * #EXb #EXbrem -EXrem |
---|
| 691 | normalize in EXbrem; destruct |
---|
| 692 | cases ((proj1 ?? (label_expr_ok ge ge' e m RG)) ??? EXe ue) #tre' * #EXe' #Te |
---|
| 693 | [ % [ 2: % [ 2: % [ % [ @plus_one |
---|
| 694 | whd in ⊢ (??%?); >EXe' in ⊢ (??%?); |
---|
| 695 | whd in ⊢ (??%?); >label_expr_type >EXb in ⊢ (??%?); |
---|
| 696 | whd in ⊢ (??%?); @refl |
---|
| 697 | | // ] |
---|
[1922] | 698 | | @swl_partial @swl_dowhilestate // ] | skip ] | skip ] |
---|
[1920] | 699 | | % [ 2: % [ 2: % [ % [ @plus_succ [ |
---|
| 700 | 4: whd in ⊢ (??%?); >EXe' in ⊢ (??%?); |
---|
| 701 | whd in ⊢ (??%?); >label_expr_type >EXb in ⊢ (??%?); |
---|
| 702 | whd in ⊢ (??%?); @refl |
---|
| 703 | | skip | skip |
---|
| 704 | | 5: @plus_succ [ 4: @refl | skip | skip |
---|
| 705 | | 5: @plus_one @refl | skip ] | skip ] |
---|
| 706 | | <(E0_right tr) @twel_app /2/ ] |
---|
[1922] | 707 | | /3/ ] | skip ] | skip ] |
---|
[1920] | 708 | ] |
---|
| 709 | | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct |
---|
| 710 | whd in EX:(??%?); destruct |
---|
| 711 | %{E0} % [2: % [ % [ @plus_one @refl | // ] | /3/ ] | skip ] |
---|
| 712 | | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct |
---|
| 713 | whd in EX:(??%?); destruct |
---|
[1922] | 714 | %{E0} % [2: % [ % [ @plus_one @refl | // ] | /4/ ] | skip ] |
---|
[1920] | 715 | | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct |
---|
| 716 | whd in EX:(??%?); destruct |
---|
[1922] | 717 | %{E0} % [2: % [ % [ @plus_one @refl | // ] | /4/ ] | skip ] |
---|
[1920] | 718 | | #k0 #k0' #K #_ #E1 #E2 #E3 destruct |
---|
| 719 | whd in EX:(??%?); destruct |
---|
[1922] | 720 | %{E0} % [2: % [ % [ @plus_one @refl | // ] | /4/ ] | skip ] |
---|
[1920] | 721 | | #r #f0 #en #k0 #k0' #K #_ #E1 #E2 #E3 destruct |
---|
| 722 | whd in EX:(??%?); |
---|
| 723 | lapply (refl ? (fn_return f)) cases (fn_return f) in ⊢ (???% → ?); |
---|
| 724 | [ #E >E in EX; whd in ⊢ (??%? → ?); #EX destruct |
---|
| 725 | %{E0} % [2: % [ % [ @plus_one whd in ⊢ (??%?); >label_function_return >E in ⊢ (??%?); |
---|
[1922] | 726 | @refl | // ] | /4/ ] | skip ] |
---|
[1920] | 727 | | *: #A [ 1,3,5,6,7,8: #B | 4: #B #C ] #E >E in EX; #EX whd in EX:(??%%); destruct |
---|
| 728 | ] |
---|
| 729 | | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct |
---|
[1922] | 730 | % [2: % [2: % [ % [ @plus_one @refl | // ] | /3/ ]| skip ]| skip ] |
---|
[1920] | 731 | ] |
---|
| 732 | | * #a1 #ty1 #a2 #EX |
---|
| 733 | cases (bindIO_inversion ??????? EX) -EX * * #b1 #o1 #tr1 * #EX1 #EX |
---|
| 734 | cases (bindIO_inversion ??????? EX) -EX * #v2 #tr2 * #EX2 #EX |
---|
| 735 | cases (bindIO_inversion ??????? EX) -EX #m3 * #EX3 #EX |
---|
| 736 | whd in EX:(??%%); destruct |
---|
| 737 | cases (proj2 ?? (label_expr_ok ge ge' e m RG) ????? EX1 us) #tr1' * #EX1' #T1 |
---|
| 738 | whd in match (label_statement ??); |
---|
| 739 | @label_gen_elim #ua1 @label_gen_elim #ua2 |
---|
| 740 | cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX2 ua1) #tr2' * #EX2' #T2 |
---|
| 741 | % [2: % [2: % [ % [ |
---|
| 742 | @plus_one whd in ⊢ (??%?); |
---|
| 743 | >exec_lvalue_labelled >EX1' in ⊢ (??%?); |
---|
| 744 | whd in ⊢ (??%?); >EX2' in ⊢ (??%?); |
---|
| 745 | whd in ⊢ (??%?); >label_expr_type >EX3 in ⊢ (??%?); |
---|
| 746 | @refl |
---|
[1922] | 747 | | @twel_app // ] | /3/ ] | skip ] | skip ] |
---|
[1920] | 748 | | * [2: * #er #tyr ] #ef #args #EX |
---|
| 749 | cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX |
---|
| 750 | cases (bindIO_inversion ??????? EX) -EX * #args' #tr2 * #EX2 #EX |
---|
| 751 | cases (bindIO_inversion ??????? EX) -EX #fd * #EX3 #EX |
---|
| 752 | cases (bindIO_inversion ??????? EX) -EX #E4 * #EX4 #EX |
---|
| 753 | whd in EX:(??%%); |
---|
| 754 | [ cases (bindIO_inversion ??????? EX) -EX * * #b5 #o5 #tr5 * #EX5 #EX whd in EX:(??%%); ] |
---|
| 755 | destruct |
---|
| 756 | whd in match (label_statement ??); |
---|
| 757 | whd in match (label_opt_expr ??); |
---|
| 758 | [ @(label_gen_elim … (Expr er tyr)) #u' @breakup_pair | letin u' ≝ us ] |
---|
| 759 | cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 u') #tr1' * #EX1' #T1 |
---|
| 760 | @label_gen_elim #u1 |
---|
| 761 | @label_gen_elim #u2 |
---|
| 762 | cases (label_exprs_ok ge ge' RG e m args args' ? EX2 u1) #tr2' * #EX2' #T2 |
---|
| 763 | [ cases (proj2 ?? (label_expr_ok ge ge' e m RG) ????? EX5 us) #tr5' * #EX5' #T5 ] |
---|
| 764 | % [2,4: % [2,4: % [1,3: % [1,3: |
---|
| 765 | @plus_one whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX why do I need the repetition? *) |
---|
| 766 | whd in ⊢ (??%?); [ >EX2' in ⊢ (??%?); | >EX2' in ⊢ (??%?); ] |
---|
| 767 | whd in ⊢ (??%?); >(opt_find_funct … RG … EX3) in ⊢ (??%?); |
---|
| 768 | whd in ⊢ (??%?); >label_fundef_typeof_fundef >label_expr_fun_typeof [ >EX4 in ⊢ (??%?); | >EX4 in ⊢ (??%?); ] |
---|
| 769 | whd in ⊢ (??%?); [ >exec_lvalue_labelled >EX5' in ⊢ (??%?); ] |
---|
[1922] | 770 | @refl | *: @twel_app /2/ ] | *: @swl_partial @swl_callstate /2/ ] | *: skip ] | *: skip ] |
---|
[1920] | 771 | | #st1 #st2 #EX |
---|
| 772 | whd in EX:(??%%); destruct |
---|
| 773 | whd in match (label_statement ??); @label_gen_elim #u1 @label_gen_elim #u2 |
---|
[1922] | 774 | %{E0} % [2: % [ % [ @plus_one @refl | // ] | @swl_partial @swl_state /2/ ] | skip ] |
---|
[1920] | 775 | | #a #st1 #st2 #EX |
---|
| 776 | cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX |
---|
| 777 | cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX |
---|
| 778 | normalize in EX; destruct |
---|
| 779 | whd in match (label_statement ??); @label_gen_elim #u1 |
---|
| 780 | @label_gen_elim #u2 @label_gen_elim #u3 @label_gen_elim #u4 |
---|
| 781 | @label_gen_elim #u5 |
---|
| 782 | whd in match (add_cost_before ??); cases (fresh ??) #c6 #u6 |
---|
| 783 | whd in match (add_cost_before ??); cases (fresh ??) #c7 #u7 |
---|
| 784 | cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1 |
---|
| 785 | % [2,4: % [2,4: % [1,3: % [1,3: @plus_succ [ 4,9: |
---|
| 786 | whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *) |
---|
| 787 | whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ] |
---|
| 788 | whd in ⊢ (??%?); @refl |
---|
| 789 | | 1,2,6,7: skip |
---|
| 790 | | 5,10: @plus_one @refl |
---|
| 791 | | *: skip |
---|
| 792 | ] |
---|
| 793 | | 2,4: <(E0_right tr) @twel_app /2/ |
---|
[1922] | 794 | ]| 2,4: /3/ ] | *: skip ] | *: skip ] |
---|
[1920] | 795 | | #a #st #EX |
---|
| 796 | cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX |
---|
| 797 | cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX |
---|
| 798 | normalize in EX; destruct |
---|
| 799 | whd in match (label_statement ??); @label_gen_elim #u1 |
---|
| 800 | @label_gen_elim #u2 |
---|
| 801 | whd in match (add_cost_before ??); cases (fresh ??) #c6 #u6 |
---|
| 802 | >shift_fst whd in match (add_cost_after ??); cases (fresh ??) #c7 #u7 |
---|
| 803 | >shift_fst |
---|
| 804 | cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1 |
---|
| 805 | % [2,4: % [2,4: % [1,3: % [1,3: @plus_succ [ 4,9: @refl | 1,2,6,7: skip |
---|
| 806 | | 5,10: @plus_succ [ 4,9: |
---|
| 807 | whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *) |
---|
| 808 | whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ] |
---|
| 809 | whd in ⊢ (??%?); @refl |
---|
| 810 | | 1,2,6,7: skip |
---|
| 811 | | 5: @plus_one @refl |
---|
| 812 | | 10: @plus_succ [ 4: @refl | 5: @plus_one @refl | *: skip ] |*: skip ] |
---|
| 813 | | *: skip |
---|
| 814 | ] |
---|
| 815 | | 2,4: <(E0_left tr) @twel_app // <(E0_right tr) @twel_app /2/ |
---|
[1922] | 816 | ]| 2,4: /4/ ] | *: skip ] | *: skip ] |
---|
[1920] | 817 | | #a #st #EX |
---|
| 818 | normalize in EX; destruct |
---|
| 819 | whd in match (label_statement ??); @label_gen_elim #u1 |
---|
| 820 | @label_gen_elim #u2 |
---|
| 821 | whd in match (add_cost_before ??); cases (fresh ??) #c6 #u6 >shift_fst |
---|
| 822 | whd in match (add_cost_after ??); cases (fresh ??) #c7 #u7 >shift_fst |
---|
| 823 | % [2: % [2: % [ % [ @plus_succ [ 4: @refl | 1,2: skip |
---|
| 824 | | 5: @plus_succ [ 4: @refl | 1,2: skip | 5: @plus_one // | skip ] | skip ] |
---|
[1922] | 825 | | /2/ ] | /4/ ] | skip ] | skip ] |
---|
[1920] | 826 | | #st1 #a #st2 #st #EX |
---|
| 827 | lapply (refl ? (is_Sskip st1)) cases (is_Sskip st1) in ⊢ (???% → ?); #Esk #Eskip |
---|
| 828 | whd in EX:(??%?); >Eskip in EX; #EX |
---|
| 829 | whd in match (label_statement ??); @label_gen_elim #u1 |
---|
| 830 | @label_gen_elim #u2 @label_gen_elim #u3 @label_gen_elim #u4 |
---|
| 831 | whd in match (add_cost_before ??); cases (fresh ??) #c5 #u5 >shift_fst |
---|
| 832 | whd in match (add_cost_after ??); cases (fresh ??) #c6 #u6 >shift_fst |
---|
| 833 | [ cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX |
---|
| 834 | cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX |
---|
| 835 | normalize in EX; destruct |
---|
| 836 | cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1 |
---|
| 837 | % [2,4: % [2,4: % [1,3: % [1,3: @plus_succ [ 4,9: @refl | 1,2,6,7: skip |
---|
| 838 | | 5,10: @plus_succ [ 4,9: |
---|
| 839 | whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *) |
---|
| 840 | whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ] |
---|
| 841 | whd in ⊢ (??%?); @refl |
---|
| 842 | | 1,2,6,7: skip |
---|
| 843 | | 5: @plus_one @refl |
---|
| 844 | | 10: @plus_succ [ 4: @refl | 5: @plus_one @refl | *: skip ] |*: skip ] |
---|
| 845 | | *: skip |
---|
| 846 | ] |
---|
| 847 | | 2,4: <(E0_left tr) @twel_app // <(E0_right tr) @twel_app /2/ |
---|
[1922] | 848 | ]| 2,4: /4/ ] | *: skip ] | *: skip ] |
---|
[1920] | 849 | | whd in EX:(??%%); destruct |
---|
| 850 | % [2: % [2: %[ %[ @plus_succ [ 4: @refl | 5: @plus_one |
---|
| 851 | whd in ⊢ (??%?); cases (labelled_is_not_skip ? u1 Esk) #Esk' #Eskip' |
---|
[1922] | 852 | >Eskip' whd in ⊢ (??%?); @refl | *: skip ]| // ] | @swl_partial @swl_state /2/ ] |
---|
[1920] | 853 | | skip ] | skip ] |
---|
| 854 | ] |
---|
| 855 | | #EX inversion KL |
---|
| 856 | [ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct |
---|
| 857 | |#u #s0 #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct |
---|
| 858 | | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct |
---|
| 859 | | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct |
---|
| 860 | | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct |
---|
| 861 | | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct |
---|
| 862 | | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct |
---|
| 863 | | #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct |
---|
| 864 | | #r #f0 #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct |
---|
| 865 | | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct |
---|
| 866 | ] |
---|
| 867 | whd in match (label_statement ??); |
---|
| 868 | % [2,4,6,8,10,12,14: % [2,4,6,8,10,12,14: % [1,3,5,7,9,11,13: % |
---|
| 869 | [1,11,13: @plus_one @refl | 2,12,14: // |
---|
| 870 | | @plus_succ [ 4: @refl | 5: @plus_succ [ 4: @refl | 5: @plus_one @refl |*:skip]|*:skip] | /2/ |
---|
| 871 | | @plus_succ [ 4: @refl | 5: @plus_succ [ 4: @refl | 5: @plus_one @refl |*:skip]|*:skip] | /2/ |
---|
| 872 | | @plus_succ [ 4: @refl | 5: @plus_one @refl |*:skip] | /2/ |
---|
| 873 | | @plus_succ [ 4: @refl | 5: @plus_succ [ 4: @refl | 5: @plus_one @refl |*:skip]|*:skip] | /2/ |
---|
[1922] | 874 | ]| *: /3/ ]|*: skip]|*: skip ] |
---|
[1920] | 875 | | #EX inversion KL |
---|
| 876 | [ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct |
---|
| 877 | |#u #s0 #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct |
---|
| 878 | | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct |
---|
| 879 | | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct |
---|
| 880 | | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct |
---|
| 881 | | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct |
---|
| 882 | | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct |
---|
| 883 | | #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct |
---|
| 884 | | #r #f0 #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct |
---|
| 885 | | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct |
---|
| 886 | ] |
---|
| 887 | whd in match (label_statement ??); |
---|
| 888 | [ 1,2,4,5,6,7: % [2,4,6,8,10,12: % [2,4,6,8,10,12: % [1,3,5,7,9,11: % |
---|
| 889 | [1,3,7,9,11: @plus_one @refl | 5: @plus_succ [4:@refl | 5:@plus_one @refl | *: skip ] |
---|
[1922] | 890 | | *: // ] | *: @swl_partial /3 by cwl_for3, swl_state, swl_whilestate/ ]| *:skip ]| *: skip ] |
---|
[1920] | 891 | | cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX |
---|
| 892 | cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX |
---|
| 893 | normalize in EX; destruct |
---|
| 894 | cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ue) #tr1' * #EX1' #T1 |
---|
| 895 | % [2,4: % [2,4: % [1,3: % [1,3: [ @plus_one | @plus_succ ] [ 1,5: |
---|
| 896 | whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *) |
---|
| 897 | whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ] |
---|
| 898 | whd in ⊢ (??%?); @refl |
---|
| 899 | | 6: @plus_succ [ 4: @refl | 5: @plus_one @refl | *: skip ] |*: skip ] |
---|
| 900 | | // | <(E0_right tr) @twel_app /2/ |
---|
| 901 | ] |
---|
[1922] | 902 | | /3/ | /3/ ] | *: skip ] | *: skip ] |
---|
[1920] | 903 | ] |
---|
| 904 | | * [2: #a ] #EX |
---|
| 905 | whd in EX:(??%?); cases (type_eq_dec (fn_return f) Tvoid) in EX; |
---|
| 906 | #Ety #EX whd in EX:(??%?); |
---|
| 907 | [ destruct |
---|
| 908 | | cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX |
---|
| 909 | cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1 |
---|
| 910 | | >Ety in EX; #EX |
---|
| 911 | | @⊥ cases (fn_return f) in Ety EX; |
---|
| 912 | [ * #H cases (H (refl ??)) |
---|
| 913 | | *: normalize #a #b #c try #d try #e destruct |
---|
| 914 | ] |
---|
| 915 | ] |
---|
| 916 | whd in match (label_statement ??); |
---|
| 917 | [ @label_gen_elim #u' whd in match (label_opt_expr ??); @label_gen_elim #u'' ] |
---|
| 918 | whd in EX:(??%%); destruct |
---|
| 919 | % [2,4: % [2,4: % [1,3: %[1,3: @plus_one |
---|
| 920 | whd in ⊢ (??%?); |
---|
| 921 | [ >label_function_return @(dec_false ? (type_eq_dec ??) Ety) #Ety'' |
---|
| 922 | whd in ⊢ (??%?); >EX1' in ⊢ (??%?); |
---|
| 923 | | >label_function_return >Ety in ⊢ (??%?); |
---|
| 924 | ] whd in ⊢ (??%?); @refl |
---|
[1922] | 925 | | *: // ]| *: @swl_partial @swl_returnstate /2/ ]|*:skip]|*:skip] |
---|
[1920] | 926 | | #a #ls #EX |
---|
| 927 | cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX |
---|
| 928 | cases v1 in EX1 EX; |
---|
| 929 | [ 2: #sz #i #EX1 #EX |
---|
| 930 | | *: normalize #A #B try #C destruct |
---|
| 931 | ] |
---|
| 932 | whd in EX:(??%%); destruct |
---|
| 933 | cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1 |
---|
| 934 | whd in match (label_statement ??); @label_gen_elim #u1 @label_gen_elim #u2 |
---|
| 935 | % [2: % [2: % [ % [ @plus_one whd in ⊢ (??%?); >EX1' in ⊢ (??%?); @refl |
---|
| 936 | | // ]| cases (label_select_ls … sz i ls u1) #u3 #Els >Els /3/ |
---|
| 937 | ]|skip ]| skip ] |
---|
| 938 | | #l #st #EX |
---|
| 939 | whd in EX:(??%?); destruct |
---|
| 940 | whd in match (label_statement ??); @label_gen_elim #u1 >shift_fst |
---|
| 941 | whd in match (add_cost_before ??); cases (fresh ??) #cs #u2 >shift_fst |
---|
| 942 | %[2: %[2: %[ %[ @plus_succ |
---|
| 943 | [ 4: @refl | 5: @plus_one @refl | *: skip ] |
---|
[1922] | 944 | | /2/ ] | /3/ ] |skip ]| skip ] |
---|
[1920] | 945 | | #l #EX |
---|
| 946 | whd in EX:(??%?); |
---|
| 947 | @blindly_label whd |
---|
| 948 | lapply (refl ? (find_label l (fn_body f) (call_cont k))) |
---|
| 949 | cases (find_label ???) in ⊢ (???% → ?); |
---|
| 950 | [ #F @⊥ >F in EX; #EX whd in EX:(??%?); destruct |
---|
| 951 | | * #s1 #k1 #F >F in EX; #EX whd in EX:(??%?); destruct |
---|
| 952 | cases (label_find_label_fn … KL F) |
---|
| 953 | #u' * #cs * #k1' * #F' #K' |
---|
| 954 | % [2: %[2: %[ %[ @plus_succ |
---|
| 955 | [ 4: whd in ⊢ (??%?); >F' in ⊢ (??%?); @refl | 5: @plus_one @refl | *: skip ] |
---|
[1922] | 956 | | /2/ ] | /3/ ] | skip ] | skip ] |
---|
[1920] | 957 | ] |
---|
| 958 | | #c #st #EX whd in EX:(??%?); destruct @blindly_label #u1 |
---|
[1922] | 959 | % [2: % [2: % [ % [ @plus_one @refl | // ] | /3/ ] | skip ]| skip ] |
---|
[1920] | 960 | ] |
---|
| 961 | | #f #ua #a #us #s #cs #cpost #k #k' #e #m #K #EX |
---|
| 962 | cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX |
---|
| 963 | cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX |
---|
| 964 | whd in EX:(??%%); destruct |
---|
| 965 | cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ua) #tr1' * #EX1' #T1 |
---|
| 966 | [ % [2: % [2: % [ % [ |
---|
| 967 | @plus_succ [4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?); |
---|
| 968 | whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl |
---|
| 969 | |5: @plus_one @refl | *: skip ] |
---|
[1922] | 970 | | <(E0_right tr) /3/ ]| /4/ ]| skip ]| skip ] |
---|
[1920] | 971 | | % [2: % [2: % [ % [ |
---|
| 972 | @plus_succ [4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?); |
---|
| 973 | whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl |
---|
| 974 | | 5: @plus_succ [4: @refl |
---|
| 975 | | 5: @plus_one @refl | *: skip ] | *: skip ] |
---|
[1922] | 976 | | <(E0_right tr) /3/ ]| /3/ ]| skip ]| skip ] |
---|
[1920] | 977 | ] |
---|
| 978 | | #f #ua #a #us #s #cs #cpost #k #k' #e #m #K #EX |
---|
| 979 | whd in EX:(??%%); destruct |
---|
| 980 | % [2: % [2: % [ % [ |
---|
| 981 | @plus_succ [4: % | 5: @plus_one % | *: skip ] |
---|
[1922] | 982 | | /2/ ]| /4/ ]| skip ]| skip ] |
---|
[1920] | 983 | | #f #ua2 #a2 #us3 #s3 #us #s #cs #cpost #k #k' #e #m #K #EX |
---|
| 984 | cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX |
---|
| 985 | cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX |
---|
| 986 | whd in EX:(??%%); destruct |
---|
| 987 | cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ua2) #tr1' * #EX1' #T1 |
---|
| 988 | [ % [2: % [2: % [ % [ |
---|
| 989 | @plus_succ [ 4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?); |
---|
| 990 | whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl |
---|
| 991 | | 5: whd in ⊢ (??(??%%??)??); @plus_one @refl |
---|
[1922] | 992 | | *: skip ]| <(E0_right tr) /3/ ] | /4/ ]| skip ]| skip ] |
---|
[1920] | 993 | | % [2: % [2: % [ % [ |
---|
| 994 | @plus_succ [ 4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?); |
---|
| 995 | whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl |
---|
| 996 | | 5: whd in ⊢ (??(??%%??)??); @plus_succ [4: @refl |
---|
[1922] | 997 | | 5: @plus_one @refl ]| *: skip ]| <(E0_right tr) /3/ ]| /3/ ]| skip ]| skip |
---|
[1920] | 998 | ] |
---|
| 999 | ] |
---|
[1922] | 1000 | | * |
---|
| 1001 | [ #f #args #k #k' #m #K whd in ⊢ (??%? → ?); @pair_elim #e #m1 #EX1 #EX |
---|
| 1002 | cases (bindIO_inversion ??????? EX) -EX #m2 * #EX2 #EX |
---|
| 1003 | whd in EX:(??%%); destruct |
---|
| 1004 | whd in match (label_fundef ?); |
---|
| 1005 | whd in match (label_function ?); |
---|
| 1006 | lapply (refl ? (label_function f)) whd in ⊢ (???% → ?); |
---|
| 1007 | @label_gen_elim #u1 @label_gen_elim #u2 >shift_fst #Ef |
---|
| 1008 | % [2: % [2: % [ % [ @plus_succ [4: whd in ⊢ (??%?); >EX1 in ⊢ (??%?); |
---|
| 1009 | whd in ⊢ (??%?); >EX2 in ⊢ (??%?); @refl |
---|
| 1010 | | 5: @plus_one @refl | *: skip ] | /2/ ]| <Ef @swl_partial @swl_state @K ]| skip ]| skip ] |
---|
| 1011 | | #id #tys #ty #args #k #k' #m #K #EX |
---|
| 1012 | cases (bindIO_inversion ??????? EX) -EX #vs * #EX1 #EX |
---|
| 1013 | cases (bindIO_inversion ??????? EX) -EX #ety * #EX2 #EX |
---|
| 1014 | whd in EX2:(??%%); destruct |
---|
| 1015 | ] |
---|
| 1016 | | #res #k #k' #m #K #EX inversion K |
---|
| 1017 | [ #E1 #E2 #E3 destruct cases res in EX ⊢ %; |
---|
| 1018 | [ 2: * #i #EX whd in EX:(??%?); destruct |
---|
| 1019 | | *: normalize #A try #B try #C destruct |
---|
| 1020 | ] |
---|
| 1021 | % [2: % [2: % [ % [ @plus_one @refl | // ]| /2/ ]| skip ]| skip ] |
---|
| 1022 | | 9: #r #f #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct cases r in EX ⊢ %; |
---|
| 1023 | [ #EX whd in EX:(??%?); destruct |
---|
| 1024 | % [2: % [2: % [ % [ @plus_one @refl | // ]| /3/ ]| skip ]| skip ] |
---|
| 1025 | | * * #b #o #ty #EX |
---|
| 1026 | cases (bindIO_inversion ??????? EX) -EX #m2 * #EX1 #EX |
---|
| 1027 | whd in EX:(??%%); destruct |
---|
| 1028 | % [2: % [2: % [ % [ @plus_one whd in ⊢ (??%?); >EX1 in ⊢ (??%?); @refl | // ]| /3/ ]| skip ]| skip ] |
---|
| 1029 | ] |
---|
| 1030 | | *: #A #B #C #D #E #F #G try #H try #I try #J try #L try #M try #N try #O |
---|
| 1031 | destruct whd in EX:(??%?); destruct |
---|
| 1032 | ] |
---|
| 1033 | | #r #EX whd in EX:(??%%); destruct |
---|
| 1034 | ] qed. |
---|
| 1035 | |
---|
[1930] | 1036 | |
---|
| 1037 | theorem step_with_labels : ∀ge,ge'. |
---|
[2105] | 1038 | related_globals … label_fundef ge ge' → |
---|
[1922] | 1039 | ∀s1,s1',tr,s2. |
---|
| 1040 | state_with_labels s1 s1' → |
---|
| 1041 | (exec_step ge s1 = Value … 〈tr,s2〉 → |
---|
| 1042 | ∃tr',s2'. plus ge' s1' tr' s2' ∧ |
---|
| 1043 | trace_with_extra_labels tr tr' ∧ |
---|
| 1044 | state_with_labels s2 s2'). |
---|
| 1045 | #ge #ge' #RG #Xs1 #Xs1' #tr #s2 * |
---|
| 1046 | [ #s1 #s1' @step_with_labels_partial // |
---|
| 1047 | | #f #u * |
---|
| 1048 | (* If we have LSdefault we need to smuggle the execution of the cost label in |
---|
| 1049 | before the actual statement. *) |
---|
| 1050 | [ #s #k #k' #e #m #K #EX |
---|
| 1051 | whd in EX:(??(??(??%???))?); |
---|
| 1052 | whd in match (label_lstatements ??); @label_gen_elim #u1 @label_gen_elim #u2 |
---|
| 1053 | >shift_fst whd in match (seq_of_labeled_statement ?); |
---|
| 1054 | cases (step_with_labels_partial … RG (State f s k e m) (State (label_function f) (\fst (label_statement s u)) k' e m) tr s2 (swl_state … K) EX) |
---|
| 1055 | #tr' * #s2' * * #P #T #S |
---|
| 1056 | % [2: % [2: % [ % [ @plus_succ [4: @refl | 5: @P | *: skip ] | /2/ ]| @S ]| skip ]| skip ] |
---|
| 1057 | (* but for LScase it's just like the cases in step_with_labels_partial *) |
---|
| 1058 | | #sz #i #s #ls #k #k' #e #m #K #EX |
---|
| 1059 | whd in EX:(??(??(??%???))?); |
---|
| 1060 | whd in match (label_lstatements ??); @label_gen_elim #u1 @label_gen_elim #u2 |
---|
| 1061 | @label_gen_elim #u3 >shift_fst whd in match (seq_of_labeled_statement ?); |
---|
| 1062 | whd in EX:(??%?); destruct |
---|
| 1063 | % [2: % [2: % [ % [ @plus_succ [4: @refl | 5: @plus_one @refl | *: skip ] | /2/ ]| /4/ ]| skip ]| skip ] |
---|
| 1064 | ] |
---|
| 1065 | ] qed. |
---|
| 1066 | |
---|
| 1067 | |
---|
[1954] | 1068 | lemma initial_state_in_simulation : ∀p,s. |
---|
| 1069 | make_initial_state p = OK ? s → |
---|
| 1070 | ∃s'. make_initial_state (clight_label p) = OK ? s' ∧ state_with_labels s s'. |
---|
| 1071 | * #vars #fns #main #s |
---|
| 1072 | whd in ⊢ (??%? → ?); letin ge ≝ (make_global ?) #EX |
---|
| 1073 | cases (bind_inversion ????? EX) -EX #m * #Em #EX |
---|
| 1074 | cases (bind_inversion ????? EX) -EX #b * #Emain #EX |
---|
| 1075 | cases (bind_inversion ????? EX) -EX #fd * #Emain' #EX |
---|
| 1076 | whd in EX:(??%%); destruct |
---|
| 1077 | whd in match (make_initial_state ?); |
---|
| 1078 | letin ge' ≝ (make_global ?) |
---|
[2105] | 1079 | cut (related_globals … label_fundef ge ge') |
---|
[1954] | 1080 | [ // ] #RG |
---|
| 1081 | % [2: % |
---|
| 1082 | [ whd in ⊢ (??%?); |
---|
[2103] | 1083 | change with (transform_program ??? (mk_program …) (λ_.label_fundef)) in match (mk_program ??? (transf_program ????) ?); |
---|
[2107] | 1084 | >init_mem_transf >Em in ⊢ (??%?); |
---|
[1954] | 1085 | whd in ⊢ (??%?); <(rg_find_symbol … RG) >Emain in ⊢ (??%?); |
---|
| 1086 | whd in ⊢ (??%?); >(rg_find_funct_ptr … RG … Emain') |
---|
| 1087 | whd in ⊢ (??%?); @refl |
---|
| 1088 | | /3/ |
---|
| 1089 | ] | skip ] |
---|
| 1090 | qed. |
---|
| 1091 | |
---|
[1922] | 1092 | |
---|
[1954] | 1093 | |
---|