[2234] | 1 | include "Clight/Csyntax.ma". |
---|
[1883] | 2 | include "Clight/fresh.ma". |
---|
[2076] | 3 | include "common/Identifiers.ma". |
---|
[2332] | 4 | include "utilities/extralib.ma". |
---|
[2076] | 5 | include "Clight/Cexec.ma". |
---|
| 6 | include "Clight/CexecInd.ma". |
---|
[2227] | 7 | include "Clight/frontend_misc.ma". |
---|
[2332] | 8 | include "Clight/memoryInjections.ma". |
---|
[2441] | 9 | include "Clight/MemProperties.ma". |
---|
[2387] | 10 | include "basics/lists/list.ma". |
---|
| 11 | include "basics/lists/listb.ma". |
---|
[2298] | 12 | |
---|
[2076] | 13 | (* ----------------------------------------------------------------------------- |
---|
| 14 | ----------------------------------------------------------------------------*) |
---|
| 15 | |
---|
| 16 | (* ----------------------------------------------------------------------------- |
---|
| 17 | Documentation |
---|
| 18 | ----------------------------------------------------------------------------*) |
---|
| 19 | |
---|
| 20 | (* This file implements transformation of switches to linear sequences of |
---|
[1883] | 21 | * if/then/else. The implementation roughly follows the lines of the prototype. |
---|
| 22 | * /!\ We assume that the program is well-typed (the type of the evaluated |
---|
| 23 | * expression must match the constants on each branch of the switch). /!\ *) |
---|
| 24 | |
---|
[2076] | 25 | (* Documentation. Let the follwing be our input switch construct: |
---|
| 26 | // --------------------------------- |
---|
| 27 | switch(e) { |
---|
| 28 | case v1: |
---|
| 29 | stmt1 |
---|
| 30 | case v2: |
---|
| 31 | stmt2 |
---|
| 32 | . |
---|
| 33 | . |
---|
| 34 | . |
---|
| 35 | default: |
---|
| 36 | stmt_default |
---|
| 37 | } |
---|
| 38 | // --------------------------------- |
---|
| 39 | |
---|
| 40 | Note that stmt1,stmt2, ... stmt_default may contain "break" statements, wich have the effect of exiting |
---|
| 41 | the switch statement. In the absence of break, the execution falls through each case sequentially. |
---|
| 42 | |
---|
| 43 | Given such a statement, we produce an equivalent sequence of if-then-elses chained by gotos: |
---|
| 44 | |
---|
| 45 | // --------------------------------- |
---|
| 46 | fresh = e; |
---|
| 47 | if(fresh == v1) { |
---|
| 48 | stmt1'; |
---|
| 49 | goto lbl_case2; |
---|
| 50 | } |
---|
| 51 | if(fresh == v2) { |
---|
| 52 | lbl_case2: |
---|
| 53 | stmt2'; |
---|
| 54 | goto lbl_case2; |
---|
| 55 | } |
---|
| 56 | ... |
---|
| 57 | stmt_default'; |
---|
| 58 | exit_label: |
---|
| 59 | // --------------------------------- |
---|
| 60 | |
---|
| 61 | where stmt1', stmt2', ... stmt_default' are the statements where all top-level [break] statements |
---|
| 62 | were replaced by [goto exit_label]. Note that fresh, lbl_casei are fresh identifiers and labels. |
---|
| 63 | *) |
---|
| 64 | |
---|
| 65 | |
---|
| 66 | (* ----------------------------------------------------------------------------- |
---|
| 67 | Definitions allowing to state that the program resulting of the transformation |
---|
[2227] | 68 | is switch-free. |
---|
| 69 | ---------------------------------------------------------------------------- *) |
---|
[2076] | 70 | |
---|
[1915] | 71 | (* Property of a Clight statement of containing no switch. Could be generalized into a kind of |
---|
[1883] | 72 | * statement_P, if useful elsewhere. *) |
---|
| 73 | let rec switch_free (st : statement) : Prop ≝ |
---|
| 74 | match st with |
---|
| 75 | [ Sskip ⇒ True |
---|
| 76 | | Sassign _ _ ⇒ True |
---|
| 77 | | Scall _ _ _ ⇒ True |
---|
| 78 | | Ssequence s1 s2 ⇒ switch_free s1 ∧ switch_free s2 |
---|
| 79 | | Sifthenelse e s1 s2 ⇒ switch_free s1 ∧ switch_free s2 |
---|
[2391] | 80 | | Swhile e body ⇒ switch_free body |
---|
[1883] | 81 | | Sdowhile e body ⇒ switch_free body |
---|
| 82 | | Sfor s1 _ s2 s3 ⇒ switch_free s1 ∧ switch_free s2 ∧ switch_free s3 |
---|
| 83 | | Sbreak ⇒ True |
---|
| 84 | | Scontinue ⇒ True |
---|
| 85 | | Sreturn _ ⇒ True |
---|
| 86 | | Sswitch _ _ ⇒ False |
---|
| 87 | | Slabel _ body ⇒ switch_free body |
---|
| 88 | | Sgoto _ ⇒ True |
---|
| 89 | | Scost _ body ⇒ switch_free body |
---|
| 90 | ]. |
---|
| 91 | |
---|
| 92 | (* Property of a list of labeled statements of being switch-free *) |
---|
| 93 | let rec branches_switch_free (sts : labeled_statements) : Prop ≝ |
---|
| 94 | match sts with |
---|
[2227] | 95 | [ LSdefault st => |
---|
[1883] | 96 | switch_free st |
---|
| 97 | | LScase _ _ st tl => |
---|
| 98 | switch_free st ∧ branches_switch_free tl |
---|
| 99 | ]. |
---|
| 100 | |
---|
[2227] | 101 | let rec branches_ind |
---|
[1883] | 102 | (sts : labeled_statements) |
---|
| 103 | (H : labeled_statements → Prop) |
---|
| 104 | (defcase : ∀st. H (LSdefault st)) |
---|
| 105 | (indcase : ∀sz.∀int.∀st.∀sub_cases. H sub_cases → H (LScase sz int st sub_cases)) ≝ |
---|
| 106 | match sts with |
---|
| 107 | [ LSdefault st ⇒ |
---|
| 108 | defcase st |
---|
| 109 | | LScase sz int st tl ⇒ |
---|
[2227] | 110 | indcase sz int st tl (branches_ind tl H defcase indcase) |
---|
[1883] | 111 | ]. |
---|
| 112 | |
---|
[2076] | 113 | (* ----------------------------------------------------------------------------- |
---|
| 114 | Switch-removal code for statements, functions and fundefs. |
---|
| 115 | ----------------------------------------------------------------------------*) |
---|
| 116 | |
---|
| 117 | (* Converts the directly accessible ("free") breaks to gotos toward the [lab] label. *) |
---|
[1883] | 118 | let rec convert_break_to_goto (st : statement) (lab : label) : statement ≝ |
---|
| 119 | match st with |
---|
| 120 | [ Sbreak ⇒ |
---|
| 121 | Sgoto lab |
---|
| 122 | | Ssequence s1 s2 ⇒ |
---|
| 123 | Ssequence (convert_break_to_goto s1 lab) (convert_break_to_goto s2 lab) |
---|
| 124 | | Sifthenelse e iftrue iffalse ⇒ |
---|
| 125 | Sifthenelse e (convert_break_to_goto iftrue lab) (convert_break_to_goto iffalse lab) |
---|
| 126 | | Sfor init e update body ⇒ |
---|
| 127 | Sfor (convert_break_to_goto init lab) e update body |
---|
| 128 | | Slabel l body ⇒ |
---|
| 129 | Slabel l (convert_break_to_goto body lab) |
---|
| 130 | | Scost cost body ⇒ |
---|
| 131 | Scost cost (convert_break_to_goto body lab) |
---|
| 132 | | _ ⇒ st |
---|
| 133 | ]. |
---|
| 134 | |
---|
[2076] | 135 | (* Converting breaks preserves switch-freeness. *) |
---|
[1883] | 136 | lemma convert_break_lift : ∀s,label . switch_free s → switch_free (convert_break_to_goto s label). |
---|
| 137 | #s elim s // |
---|
| 138 | [ 1: #s1 #s2 #Hind1 #Hind2 #label * #Hsf1 #Hsf2 /3/ |
---|
| 139 | | 2: #e #s1 #s2 #Hind1 #Hind2 #label * #Hsf1 #Hsf2 /3/ |
---|
| 140 | | 3: #s1 #e #s2 #s3 #Hind1 #Hind2 #Hind3 #label * * #Hsf1 #Hsf2 #Hsf3 normalize |
---|
| 141 | try @conj try @conj /3/ |
---|
| 142 | | 4: #l #s0 #Hind #lab #Hsf whd in Hsf; normalize /2/ |
---|
| 143 | | 5: #l #s0 #Hind #lab #Hsf whd in Hsf; normalize /3/ |
---|
| 144 | ] qed. |
---|
| 145 | |
---|
[2227] | 146 | (* (def_case : ident × sf_statement) *) |
---|
| 147 | |
---|
| 148 | let rec produce_cond |
---|
| 149 | (e : expr) |
---|
| 150 | (switch_cases : labeled_statements) |
---|
| 151 | (u : universe SymbolTag) |
---|
| 152 | (exit : label) on switch_cases : statement × label × (universe SymbolTag) ≝ |
---|
| 153 | match switch_cases with |
---|
| 154 | [ LSdefault st ⇒ |
---|
| 155 | let 〈lab,u1〉 ≝ fresh ? u in |
---|
| 156 | let st' ≝ convert_break_to_goto st exit in |
---|
| 157 | 〈Slabel lab st', lab, u1〉 |
---|
| 158 | | LScase sz tag st other_cases ⇒ |
---|
| 159 | let 〈sub_statements, sub_label, u1〉 ≝ produce_cond e other_cases u exit in |
---|
| 160 | let st' ≝ convert_break_to_goto st exit in |
---|
| 161 | let 〈lab, u2〉 ≝ fresh ? u1 in |
---|
| 162 | let test ≝ Expr (Ebinop Oeq e (Expr (Econst_int sz tag) (typeof e))) (Tint I32 Signed) in |
---|
| 163 | let case_statement ≝ |
---|
| 164 | Sifthenelse test |
---|
| 165 | (Slabel lab (Ssequence st' (Sgoto sub_label))) |
---|
| 166 | Sskip |
---|
| 167 | in |
---|
| 168 | 〈Ssequence case_statement sub_statements, lab, u2〉 |
---|
| 169 | ]. |
---|
| 170 | |
---|
| 171 | definition simplify_switch ≝ |
---|
| 172 | λ(e : expr). |
---|
| 173 | λ(switch_cases : labeled_statements). |
---|
| 174 | λ(uv : universe SymbolTag). |
---|
[1883] | 175 | let 〈exit_label, uv1〉 ≝ fresh ? uv in |
---|
[2227] | 176 | let 〈result, useless_label, uv2〉 ≝ produce_cond e switch_cases uv1 exit_label in |
---|
| 177 | 〈Ssequence result (Slabel exit_label Sskip), uv2〉. |
---|
[1883] | 178 | |
---|
[2227] | 179 | lemma produce_cond_switch_free : ∀l.∀H:branches_switch_free l.∀e,lab,u.switch_free (\fst (\fst (produce_cond e l u lab))). |
---|
| 180 | #l @(labeled_statements_ind … l) |
---|
| 181 | [ 1: #s #Hsf #e #lab #u normalize cases (fresh ??) #lab0 #u1 |
---|
| 182 | normalize in Hsf ⊢ %; @(convert_break_lift … Hsf) |
---|
| 183 | | 2: #sz #i #hd #tl #Hind whd in ⊢ (% → ?); * #Hsf_hd #Hsf_tl |
---|
| 184 | #e #lab #u normalize |
---|
| 185 | lapply (Hind Hsf_tl e lab u) |
---|
| 186 | cases (produce_cond e tl u lab) * #cond #lab' #u' #Hsf normalize nodelta |
---|
| 187 | cases (fresh ??) #lab0 #u2 normalize nodelta |
---|
| 188 | normalize try @conj try @conj try @conj try // |
---|
| 189 | @(convert_break_lift … Hsf_hd) |
---|
| 190 | ] qed. |
---|
| 191 | |
---|
| 192 | lemma simplify_switch_switch_free : ∀e,l. ∀H:branches_switch_free l. ∀u. switch_free (\fst (simplify_switch e l u)). |
---|
| 193 | #e #l cases l |
---|
| 194 | [ 1: #def normalize #H #u cases (fresh ? u) #exit_label #uv normalize cases (fresh ? uv) #lab #uv' normalize nodelta |
---|
| 195 | whd @conj whd |
---|
| 196 | [ 1: @convert_break_lift assumption |
---|
| 197 | | 2: @I ] |
---|
| 198 | | 2: #sz #i #case #tl normalize * #Hsf #Hsftl #u |
---|
| 199 | cases (fresh ? u) #exit_label #uv1 normalize nodelta |
---|
| 200 | lapply (produce_cond_switch_free tl Hsftl e exit_label uv1) |
---|
| 201 | cases (produce_cond e tl uv1 exit_label) |
---|
| 202 | * #cond #lab #u1 #Hsf_cond normalize nodelta |
---|
| 203 | cases (fresh ??) #lab0 #u2 normalize nodelta |
---|
| 204 | normalize @conj try @conj try @conj try @conj try // |
---|
| 205 | @(convert_break_lift ?? Hsf) |
---|
[2438] | 206 | ] qed. |
---|
[2227] | 207 | |
---|
| 208 | (* Instead of using tuples, we use a special type to pack the results of [switch_removal]. We do that in |
---|
| 209 | order to circumvent the associativity problems in notations. *) |
---|
[2438] | 210 | (* |
---|
[2227] | 211 | record swret (A : Type[0]) : Type[0] ≝ { |
---|
| 212 | ret_st : A; |
---|
| 213 | ret_acc : list (ident × type); |
---|
| 214 | ret_u : universe SymbolTag |
---|
| 215 | }. |
---|
| 216 | |
---|
[2438] | 217 | notation > "vbox('let' 〈ident v1, ident v2, ident v3〉 ≝ e in break e')" with precedence 48 |
---|
| 218 | for @{ (λ${ident v1}.λ${ident v2}.λ${ident v3}. ${e'}) |
---|
| 219 | (ret_st ? ${e}) |
---|
| 220 | (ret_acc ? ${e}) |
---|
| 221 | (ret_u ? ${e}) }. |
---|
[2227] | 222 | |
---|
[2438] | 223 | definition ret ≝ λe1,e2,e3. mk_swret statement e1 e2 e3. *) |
---|
[2227] | 224 | |
---|
| 225 | (* Recursively convert a statement into a switch-free one. We /provide/ directly to the function a list |
---|
| 226 | of identifiers (supposedly fresh). The actual task of producing this identifier is decoupled in another |
---|
| 227 | 'twin' function. It is then proved that feeding [switch_removal] with the correct amount of free variables |
---|
| 228 | allows it to proceed without failing. This is all in order to ease the proof of simulation. *) |
---|
| 229 | let rec switch_removal |
---|
| 230 | (st : statement) (* the statement in which we will remove switches *) |
---|
[2438] | 231 | (u : universe SymbolTag) (* a fresh label and ident generator *) |
---|
| 232 | : statement × (list (ident × type)) × (universe SymbolTag) ≝ |
---|
[2227] | 233 | match st with |
---|
[2438] | 234 | [ Sskip ⇒ 〈st, [ ], u〉 |
---|
| 235 | | Sassign _ _ ⇒ 〈st, [ ], u〉 |
---|
| 236 | | Scall _ _ _ ⇒ 〈st, [ ], u〉 |
---|
[2227] | 237 | | Ssequence s1 s2 ⇒ |
---|
[2438] | 238 | let 〈s1', acc1, u'〉 ≝ switch_removal s1 u in |
---|
| 239 | let 〈s2', acc2, u''〉 ≝ switch_removal s2 u' in |
---|
| 240 | 〈Ssequence s1' s2', acc1 @ acc2, u''〉 |
---|
[2227] | 241 | | Sifthenelse e s1 s2 ⇒ |
---|
[2438] | 242 | let 〈s1', acc1, u'〉 ≝ switch_removal s1 u in |
---|
| 243 | let 〈s2', acc2, u''〉 ≝ switch_removal s2 u' in |
---|
| 244 | 〈Sifthenelse e s1' s2', acc1 @ acc2, u''〉 |
---|
[2391] | 245 | | Swhile e body ⇒ |
---|
[2438] | 246 | let 〈body', acc, u'〉 ≝ switch_removal body u in |
---|
| 247 | 〈Swhile e body', acc, u'〉 |
---|
[2227] | 248 | | Sdowhile e body ⇒ |
---|
[2438] | 249 | let 〈body', acc, u'〉 ≝ switch_removal body u in |
---|
| 250 | 〈Sdowhile e body', acc, u'〉 |
---|
[2227] | 251 | | Sfor s1 e s2 s3 ⇒ |
---|
[2438] | 252 | let 〈s1', acc1, u'〉 ≝ switch_removal s1 u in |
---|
| 253 | let 〈s2', acc2, u''〉 ≝ switch_removal s2 u' in |
---|
| 254 | let 〈s3', acc3, u'''〉 ≝ switch_removal s3 u'' in |
---|
| 255 | 〈Sfor s1' e s2' s3', acc1 @ acc2 @ acc3, u'''〉 |
---|
[2227] | 256 | | Sbreak ⇒ |
---|
[2438] | 257 | 〈st, [ ], u〉 |
---|
[2227] | 258 | | Scontinue ⇒ |
---|
[2438] | 259 | 〈st, [ ], u〉 |
---|
[2227] | 260 | | Sreturn _ ⇒ |
---|
[2438] | 261 | 〈st, [ ], u〉 |
---|
[2227] | 262 | | Sswitch e branches ⇒ |
---|
[2438] | 263 | let 〈sf_branches, acc, u'〉 ≝ switch_removal_branches branches u in |
---|
| 264 | let 〈switch_tmp, u''〉 ≝ fresh ? u' in |
---|
| 265 | let ident ≝ Expr (Evar switch_tmp) (typeof e) in |
---|
| 266 | let assign ≝ Sassign ident e in |
---|
| 267 | let 〈result, u'''〉 ≝ simplify_switch ident sf_branches u'' in |
---|
| 268 | 〈Ssequence assign result, (〈switch_tmp, typeof e〉 :: acc), u'''〉 |
---|
[2227] | 269 | | Slabel label body ⇒ |
---|
[2438] | 270 | let 〈body', acc, u'〉 ≝ switch_removal body u in |
---|
| 271 | 〈Slabel label body', acc, u'〉 |
---|
[2227] | 272 | | Sgoto _ ⇒ |
---|
[2438] | 273 | 〈st, [ ], u〉 |
---|
[2227] | 274 | | Scost cost body ⇒ |
---|
[2438] | 275 | let 〈body', acc, u'〉 ≝ switch_removal body u in |
---|
| 276 | 〈Scost cost body', acc, u'〉 |
---|
[2227] | 277 | ] |
---|
[1883] | 278 | |
---|
| 279 | and switch_removal_branches |
---|
| 280 | (l : labeled_statements) |
---|
[2227] | 281 | (u : universe SymbolTag) |
---|
[2438] | 282 | : (labeled_statements × (list (ident × type)) × (universe SymbolTag)) ≝ |
---|
[1883] | 283 | match l with |
---|
| 284 | [ LSdefault st ⇒ |
---|
[2438] | 285 | let 〈st', acc1, u'〉 ≝ switch_removal st u in |
---|
| 286 | 〈LSdefault st', acc1, u'〉 |
---|
| 287 | | LScase sz int st tl ⇒ |
---|
| 288 | let 〈tl_result, acc1, u'〉 ≝ switch_removal_branches tl u in |
---|
| 289 | let 〈st', acc2, u''〉 ≝ switch_removal st u' in |
---|
| 290 | 〈LScase sz int st' tl_result, acc1 @ acc2, u''〉 |
---|
[1883] | 291 | ]. |
---|
| 292 | |
---|
[2438] | 293 | definition ret_st : ∀A:Type[0]. (A × (list (ident × type)) × (universe SymbolTag)) → A ≝ |
---|
| 294 | λA,x. |
---|
| 295 | let 〈s,vars,u〉 ≝ x in s. |
---|
[2076] | 296 | |
---|
[2438] | 297 | definition ret_vars : ∀A:Type[0]. (A × (list (ident × type)) × (universe SymbolTag)) → list (ident × type) ≝ |
---|
| 298 | λA,x. |
---|
| 299 | let 〈s,vars,u〉 ≝ x in vars. |
---|
[2076] | 300 | |
---|
[2438] | 301 | definition ret_u : ∀A:Type[0]. (A × (list (ident × type)) × (universe SymbolTag)) → (universe SymbolTag) ≝ |
---|
| 302 | λA,x. |
---|
| 303 | let 〈s,vars,u〉 ≝ x in u. |
---|
[2076] | 304 | |
---|
[2227] | 305 | (* Proof that switch_removal_switch_free does its job. *) |
---|
[2438] | 306 | lemma switch_removal_switch_free : ∀st,u. switch_free (ret_st ? (switch_removal st u)). |
---|
| 307 | #st @(statement_ind2 ? (λls. ∀u. branches_switch_free (ret_st ? (switch_removal_branches ls u))) … st) |
---|
| 308 | try // |
---|
| 309 | [ 1: #s1 #s2 #H1 #H2 #u normalize |
---|
| 310 | lapply (H1 u) |
---|
| 311 | cases (switch_removal s1 u) * #st1 #vars1 #u' normalize #HA |
---|
| 312 | lapply (H2 u') |
---|
| 313 | cases (switch_removal s2 u') * #st2 #vars2 #u'' normalize #HB |
---|
| 314 | @conj assumption |
---|
[2227] | 315 | | *: |
---|
| 316 | (* TODO the first few cases show that the lemma is routinely proved. TBF later. *) |
---|
| 317 | @cthulhu ] |
---|
| 318 | qed. |
---|
| 319 | |
---|
[2076] | 320 | (* ----------------------------------------------------------------------------- |
---|
| 321 | Switch-removal code for programs. |
---|
| 322 | ----------------------------------------------------------------------------*) |
---|
| 323 | |
---|
| 324 | (* The functions in fresh.ma do not consider labels. Using [universe_for_program p] may lead to |
---|
| 325 | * name clashes for labels. We have no choice but to actually run through the function and to |
---|
| 326 | * compute the maximum of labels+identifiers. This way we can generate both fresh variables and |
---|
| 327 | * fresh labels using the same univ. While we're at it we also consider record fields. |
---|
| 328 | * Cost labels are not considered, though. They already live in a separate universe. |
---|
| 329 | * |
---|
| 330 | * Important note: this is partially redundant with fresh.ma. We take care of avoiding name clashes, |
---|
| 331 | * but in the end it might be good to move the following functions into fresh.ma. |
---|
| 332 | *) |
---|
| 333 | |
---|
[2227] | 334 | (* Least element in the total order of identifiers. *) |
---|
| 335 | definition least_identifier ≝ an_identifier SymbolTag one. |
---|
| 336 | |
---|
[2076] | 337 | (* This is certainly overkill: variables adressed in an expression should be declared in the |
---|
[2227] | 338 | * enclosing function's prototype. *) |
---|
| 339 | let rec max_of_expr (e : expr) : ident ≝ |
---|
[2076] | 340 | match e with |
---|
| 341 | [ Expr ed _ ⇒ |
---|
| 342 | match ed with |
---|
[2227] | 343 | [ Econst_int _ _ ⇒ least_identifier |
---|
| 344 | | Evar id ⇒ id |
---|
| 345 | | Ederef e1 ⇒ max_of_expr e1 |
---|
| 346 | | Eaddrof e1 ⇒ max_of_expr e1 |
---|
| 347 | | Eunop _ e1 ⇒ max_of_expr e1 |
---|
| 348 | | Ebinop _ e1 e2 ⇒ max_id (max_of_expr e1) (max_of_expr e2) |
---|
| 349 | | Ecast _ e1 ⇒ max_of_expr e1 |
---|
| 350 | | Econdition e1 e2 e3 ⇒ |
---|
| 351 | max_id (max_of_expr e1) (max_id (max_of_expr e2) (max_of_expr e3)) |
---|
[2076] | 352 | | Eandbool e1 e2 ⇒ |
---|
[2227] | 353 | max_id (max_of_expr e1) (max_of_expr e2) |
---|
[2076] | 354 | | Eorbool e1 e2 ⇒ |
---|
[2227] | 355 | max_id (max_of_expr e1) (max_of_expr e2) |
---|
| 356 | | Esizeof _ ⇒ least_identifier |
---|
| 357 | | Efield r f ⇒ max_id f (max_of_expr r) |
---|
| 358 | | Ecost _ e1 ⇒ max_of_expr e1 |
---|
[2076] | 359 | ] |
---|
| 360 | ]. |
---|
| 361 | |
---|
[2227] | 362 | (* Reasoning about this promises to be a serious pain. Especially the Scall case. *) |
---|
| 363 | let rec max_of_statement (s : statement) : ident ≝ |
---|
[2076] | 364 | match s with |
---|
[2227] | 365 | [ Sskip ⇒ least_identifier |
---|
| 366 | | Sassign e1 e2 ⇒ max_id (max_of_expr e1) (max_of_expr e2) |
---|
| 367 | | Scall r f args ⇒ |
---|
[2076] | 368 | let retmax ≝ |
---|
[2227] | 369 | match r with |
---|
| 370 | [ None ⇒ least_identifier |
---|
| 371 | | Some e ⇒ max_of_expr e ] |
---|
[2076] | 372 | in |
---|
[2227] | 373 | max_id (max_of_expr f) |
---|
| 374 | (max_id retmax |
---|
[2438] | 375 | (foldr ?? (λelt,acc. max_id (max_of_expr elt) acc) least_identifier args) ) |
---|
[2227] | 376 | | Ssequence s1 s2 ⇒ |
---|
| 377 | max_id (max_of_statement s1) (max_of_statement s2) |
---|
[2076] | 378 | | Sifthenelse e s1 s2 ⇒ |
---|
[2227] | 379 | max_id (max_of_expr e) (max_id (max_of_statement s1) (max_of_statement s2)) |
---|
[2391] | 380 | | Swhile e body ⇒ |
---|
[2227] | 381 | max_id (max_of_expr e) (max_of_statement body) |
---|
[2076] | 382 | | Sdowhile e body ⇒ |
---|
[2227] | 383 | max_id (max_of_expr e) (max_of_statement body) |
---|
[2076] | 384 | | Sfor init test incr body ⇒ |
---|
[2227] | 385 | max_id (max_id (max_of_statement init) (max_of_expr test)) (max_id (max_of_statement incr) (max_of_statement body)) |
---|
| 386 | | Sbreak ⇒ least_identifier |
---|
| 387 | | Scontinue ⇒ least_identifier |
---|
[2076] | 388 | | Sreturn opt ⇒ |
---|
| 389 | match opt with |
---|
[2227] | 390 | [ None ⇒ least_identifier |
---|
| 391 | | Some e ⇒ max_of_expr e |
---|
[2076] | 392 | ] |
---|
| 393 | | Sswitch e ls ⇒ |
---|
[2227] | 394 | max_id (max_of_expr e) (max_of_ls ls) |
---|
[2076] | 395 | | Slabel lab body ⇒ |
---|
[2227] | 396 | max_id lab (max_of_statement body) |
---|
[2076] | 397 | | Sgoto lab ⇒ |
---|
[2227] | 398 | lab |
---|
[2076] | 399 | | Scost _ body ⇒ |
---|
[2227] | 400 | max_of_statement body |
---|
[2076] | 401 | ] |
---|
[2227] | 402 | and max_of_ls (ls : labeled_statements) : ident ≝ |
---|
[2076] | 403 | match ls with |
---|
[2227] | 404 | [ LSdefault s ⇒ max_of_statement s |
---|
| 405 | | LScase _ _ s ls' ⇒ max_id (max_of_ls ls') (max_of_statement s) |
---|
[2076] | 406 | ]. |
---|
| 407 | |
---|
| 408 | definition max_id_of_function : function → ident ≝ |
---|
[2227] | 409 | λf. max_id (max_of_statement (fn_body f)) (max_id_of_fn f). |
---|
[2076] | 410 | |
---|
[2227] | 411 | (* We compute fresh universes on a function-by function basis, since there can't |
---|
| 412 | * be cross-functions gotos or stuff like that. *) |
---|
| 413 | definition function_switch_removal : function → function × (list (ident × type)) ≝ |
---|
| 414 | λf. |
---|
[2438] | 415 | let u ≝ universe_of_max (max_id_of_function f) in |
---|
| 416 | let 〈st, vars, u'〉 ≝ switch_removal (fn_body f) u in |
---|
| 417 | let result ≝ mk_function (fn_return f) (fn_params f) (vars @ (fn_vars f)) st in |
---|
| 418 | 〈result, vars〉. |
---|
[2076] | 419 | |
---|
[2227] | 420 | let rec fundef_switch_removal (f : clight_fundef) : clight_fundef ≝ |
---|
| 421 | match f with |
---|
| 422 | [ CL_Internal f ⇒ |
---|
| 423 | CL_Internal (\fst (function_switch_removal f)) |
---|
| 424 | | CL_External _ _ _ ⇒ |
---|
| 425 | f |
---|
| 426 | ]. |
---|
[2076] | 427 | |
---|
[1883] | 428 | let rec program_switch_removal (p : clight_program) : clight_program ≝ |
---|
| 429 | let prog_funcs ≝ prog_funct ?? p in |
---|
[2227] | 430 | let sf_funcs ≝ map ?? (λcl_fundef. |
---|
| 431 | let 〈fun_id, fun_def〉 ≝ cl_fundef in |
---|
| 432 | 〈fun_id, fundef_switch_removal fun_def〉 |
---|
| 433 | ) prog_funcs in |
---|
[1883] | 434 | mk_program ?? |
---|
| 435 | (prog_vars … p) |
---|
| 436 | sf_funcs |
---|
[2016] | 437 | (prog_main … p). |
---|
[1883] | 438 | |
---|
[2076] | 439 | (* ----------------------------------------------------------------------------- |
---|
[2227] | 440 | Applying two relations on all substatements and all subexprs (directly under). |
---|
| 441 | ---------------------------------------------------------------------------- *) |
---|
| 442 | |
---|
| 443 | let rec substatement_P (s1 : statement) (P : statement → Prop) (Q : expr → Prop) : Prop ≝ |
---|
| 444 | match s1 with |
---|
| 445 | [ Sskip ⇒ True |
---|
| 446 | | Sassign e1 e2 ⇒ Q e1 ∧ Q e2 |
---|
| 447 | | Scall r f args ⇒ |
---|
| 448 | match r with |
---|
| 449 | [ None ⇒ Q f ∧ (All … Q args) |
---|
| 450 | | Some r ⇒ Q r ∧ Q f ∧ (All … Q args) |
---|
| 451 | ] |
---|
| 452 | | Ssequence sub1 sub2 ⇒ P sub1 ∧ P sub2 |
---|
| 453 | | Sifthenelse e sub1 sub2 ⇒ P sub1 ∧ P sub2 |
---|
[2391] | 454 | | Swhile e sub ⇒ Q e ∧ P sub |
---|
[2227] | 455 | | Sdowhile e sub ⇒ Q e ∧ P sub |
---|
| 456 | | Sfor sub1 cond sub2 sub3 ⇒ P sub1 ∧ Q cond ∧ P sub2 ∧ P sub3 |
---|
| 457 | | Sbreak ⇒ True |
---|
| 458 | | Scontinue ⇒ True |
---|
| 459 | | Sreturn r ⇒ |
---|
| 460 | match r with |
---|
| 461 | [ None ⇒ True |
---|
| 462 | | Some r ⇒ Q r ] |
---|
| 463 | | Sswitch e ls ⇒ Q e ∧ (substatement_ls ls P) |
---|
| 464 | | Slabel _ sub ⇒ P sub |
---|
| 465 | | Sgoto _ ⇒ True |
---|
| 466 | | Scost _ sub ⇒ P sub |
---|
| 467 | ] |
---|
| 468 | and substatement_ls ls (P : statement → Prop) : Prop ≝ |
---|
| 469 | match ls with |
---|
| 470 | [ LSdefault sub ⇒ P sub |
---|
| 471 | | LScase _ _ sub tl ⇒ P sub ∧ (substatement_ls tl P) |
---|
| 472 | ]. |
---|
| 473 | |
---|
| 474 | (* ----------------------------------------------------------------------------- |
---|
| 475 | Freshness conservation results on switch removal. |
---|
| 476 | ---------------------------------------------------------------------------- *) |
---|
| 477 | |
---|
| 478 | (* Similar stuff in toCminor.ma. *) |
---|
| 479 | lemma fresh_for_univ_still_fresh : |
---|
| 480 | ∀u,i. fresh_for_univ SymbolTag i u → ∀v,u'. 〈v, u'〉 = fresh ? u → fresh_for_univ ? i u'. |
---|
| 481 | * #p * #i #H1 #v * #p' lapply H1 normalize |
---|
| 482 | #H1 #H2 destruct (H2) /2/ qed. |
---|
| 483 | |
---|
[2438] | 484 | definition fresher_than_or_equal : universe SymbolTag → universe SymbolTag → Prop ≝ |
---|
| 485 | λu1,u2. |
---|
| 486 | match u1 with |
---|
| 487 | [ mk_universe p1 ⇒ |
---|
| 488 | match u2 with |
---|
| 489 | [ mk_universe p2 ⇒ p2 ≤ p1 ] ]. |
---|
| 490 | |
---|
| 491 | definition fte ≝ fresher_than_or_equal. |
---|
| 492 | |
---|
| 493 | lemma transitive_fte : ∀u1,u2,u3. fte u1 u2 → fte u2 u3 → fte u1 u3. |
---|
| 494 | * #u1 * #u2 * #u3 normalize /2 by transitive_le/ |
---|
[2227] | 495 | qed. |
---|
| 496 | |
---|
[2438] | 497 | lemma reflexive_fte : ∀u. fte u u. |
---|
| 498 | * // qed. |
---|
| 499 | |
---|
| 500 | lemma fresher_for_univ : ∀u1,u2. fte u1 u2 → ∀i. fresh_for_univ ? i u2 → fresh_for_univ ? i u1. |
---|
| 501 | * #p * #p' normalize #H * #i normalize |
---|
| 502 | /2 by transitive_le/ |
---|
| 503 | qed. |
---|
| 504 | |
---|
| 505 | lemma fresh_fte : ∀u2,u1,fv. fresh ? u2 = 〈fv,u1〉 → fte u1 u2. |
---|
| 506 | * #u1 * #u2 * #fv normalize #H1 destruct // |
---|
| 507 | qed. |
---|
| 508 | |
---|
| 509 | lemma produce_cond_fte : ∀e,exit,ls,u. fte (\snd (produce_cond e ls u exit)) u. |
---|
[2227] | 510 | #e #exit #ls @(branches_ind … ls) |
---|
[2438] | 511 | [ 1: #st #u normalize lapply (fresh_fte u) |
---|
| 512 | cases (fresh ? u) #lab #u1 #H lapply (H u1 lab (refl ??)) normalize // |
---|
| 513 | | 2: #sz #i #hd #tl #Hind #u normalize |
---|
| 514 | lapply (Hind u) cases (produce_cond e tl u exit) * |
---|
| 515 | #subcond #sublabel #u1 #Hfte normalize |
---|
| 516 | lapply (fresh_fte u1) |
---|
| 517 | cases (fresh ? u1) #lab #u2 #H2 lapply (H2 u2 lab (refl ??)) |
---|
| 518 | #Hfte' normalize cases u2 in Hfte'; #u2 |
---|
| 519 | cases u in Hfte; #u cases u1 #u1 normalize |
---|
| 520 | /2 by transitive_le/ |
---|
[2227] | 521 | ] qed. |
---|
| 522 | |
---|
[2438] | 523 | lemma produce_cond_fresh : ∀e,exit,ls,u,i. fresh_for_univ ? i u → fresh_for_univ ? i (\snd (produce_cond e ls u exit)). |
---|
| 524 | #e #exit #ls #u #i @fresher_for_univ @produce_cond_fte qed. |
---|
| 525 | |
---|
| 526 | lemma simplify_switch_fte : ∀u,e,ls. |
---|
| 527 | fte (\snd (simplify_switch e ls u)) u. |
---|
| 528 | #u #e #ls normalize |
---|
| 529 | lapply (fresh_fte u) |
---|
| 530 | cases (fresh ? u) |
---|
| 531 | #exit_label #uv1 #Haux lapply (Haux uv1 exit_label (refl ??)) -Haux #Haux |
---|
[2227] | 532 | normalize |
---|
[2438] | 533 | lapply (produce_cond_fte e exit_label ls uv1) |
---|
| 534 | cases (produce_cond ????) * #stm #label #uv2 normalize nodelta |
---|
| 535 | cases uv2 #uv2 cases uv1 in Haux; #uv1 cases u #u normalize |
---|
| 536 | /2 by transitive_le/ |
---|
[2227] | 537 | qed. |
---|
| 538 | |
---|
[2438] | 539 | lemma simplify_switch_fresh : ∀u,i,e,ls. |
---|
| 540 | fresh_for_univ ? i u → |
---|
| 541 | fresh_for_univ ? i (\snd (simplify_switch e ls u)). |
---|
| 542 | #u #i #e #ls @fresher_for_univ @simplify_switch_fte qed. |
---|
| 543 | |
---|
| 544 | lemma switch_removal_fte : ∀st,u. |
---|
| 545 | fte (ret_u ? (switch_removal … st u)) u. |
---|
| 546 | #st @(statement_ind2 ? (λls. ∀u. fte (ret_u ? (switch_removal_branches ls u)) u) … st) |
---|
| 547 | try /2 by reflexive_fte/ |
---|
| 548 | [ 1: #s1 #s2 #Hind1 #Hind2 #u normalize |
---|
| 549 | lapply (Hind1 u) |
---|
| 550 | cases (switch_removal s1 u) * #s1' #fvs1 #u' normalize nodelta |
---|
| 551 | lapply (Hind2 u') |
---|
| 552 | cases (switch_removal s2 u') * #s2' #fvs2 #u'' normalize |
---|
| 553 | #HA #HB @(transitive_fte … HA HB) |
---|
| 554 | | 2: #e #s1 #s2 #Hind1 #Hind2 #u normalize |
---|
| 555 | lapply (Hind1 u) |
---|
| 556 | cases (switch_removal s1 u) * #s1' #fvs1 #u' normalize nodelta |
---|
| 557 | lapply (Hind2 u') |
---|
| 558 | cases (switch_removal s2 u') * #s2' #fvs2 #u'' normalize |
---|
| 559 | #HA #HB @(transitive_fte … HA HB) |
---|
| 560 | | 3,7,8: #e #s #Hind #u normalize |
---|
| 561 | lapply (Hind u) |
---|
| 562 | cases (switch_removal s u) * #s' #fvs #u' normalize #H @H |
---|
| 563 | | 4: #e #s #Hind #u normalize |
---|
| 564 | lapply (Hind u) |
---|
| 565 | cases (switch_removal s u) * #s' #fvs #u' normalize #H @H |
---|
| 566 | | 5: #s1 #e #s2 #s3 #Hind1 #Hind2 #Hind3 #u normalize |
---|
| 567 | lapply (Hind1 u) cases (switch_removal s1 u) * #s1' #fvs1 #u' #Hfte1 |
---|
| 568 | normalize nodelta |
---|
| 569 | lapply (Hind2 u') cases (switch_removal s2 u') * #s2' #fvs2 #u'' #Hfte2 |
---|
| 570 | normalize nodelta |
---|
| 571 | lapply (Hind3 u'') cases (switch_removal s3 u'') * #s2' #fvs2 #u'' #Hfte3 |
---|
| 572 | normalize nodelta |
---|
| 573 | /3 by transitive_fte/ |
---|
| 574 | | 6: #e #ls #Hind #u whd in match (switch_removal ??); |
---|
| 575 | lapply (Hind u) |
---|
| 576 | cases (switch_removal_branches ls u) * #ls #fvs #u' #Hfte1 |
---|
| 577 | normalize nodelta |
---|
| 578 | lapply (fresh_fte … u') cases (fresh ? u') #fv #u'' #H lapply (H u'' fv (refl ??)) #Hfte2 |
---|
| 579 | normalize nodelta |
---|
| 580 | lapply (simplify_switch_fte u'' (Expr (Evar fv) (typeof e)) ls) |
---|
| 581 | cases (simplify_switch ???) |
---|
| 582 | normalize nodelta |
---|
| 583 | #st' #u''' #Hfte3 |
---|
| 584 | /3 by transitive_fte/ |
---|
| 585 | | 9: #s #H #u normalize |
---|
| 586 | lapply (H u) cases (switch_removal s u) * #st' #fvs normalize #u' #H @H |
---|
| 587 | | 10: #sz #i #st #ls #Hind1 #Hind2 #u normalize |
---|
| 588 | lapply (Hind2 u) cases (switch_removal_branches ls u) * #ls' #fvs' #u' |
---|
| 589 | normalize nodelta #Hfte1 |
---|
| 590 | lapply (Hind1 … u') cases (switch_removal st u') * #st' #fvs'' #u'' |
---|
| 591 | normalize nodelta #Hfte2 |
---|
| 592 | /3 by transitive_fte/ |
---|
| 593 | ] qed. |
---|
| 594 | |
---|
| 595 | lemma switch_removal_fresh : ∀u,i,st. |
---|
| 596 | fresh_for_univ ? i u → |
---|
| 597 | fresh_for_univ ? i (ret_u … (switch_removal st u)). |
---|
| 598 | #u #i #st @fresher_for_univ @switch_removal_fte qed. |
---|
| 599 | |
---|
[2227] | 600 | (* ----------------------------------------------------------------------------- |
---|
[2076] | 601 | Simulation proof and related voodoo. |
---|
| 602 | ----------------------------------------------------------------------------*) |
---|
[2468] | 603 | (* |
---|
[2076] | 604 | definition expr_lvalue_ind_combined ≝ |
---|
| 605 | λP,Q,ci,cf,lv,vr,dr,ao,uo,bo,ca,cd,ab,ob,sz,fl,co,xx. |
---|
| 606 | conj ?? |
---|
| 607 | (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx) |
---|
[2468] | 608 | (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx).*) |
---|
[2076] | 609 | |
---|
| 610 | let rec expr_ind2 |
---|
| 611 | (P : expr → Prop) (Q : expr_descr → type → Prop) |
---|
| 612 | (IE : ∀ed. ∀t. Q ed t → P (Expr ed t)) |
---|
| 613 | (Iconst_int : ∀sz, i, t. Q (Econst_int sz i) t) |
---|
| 614 | (Ivar : ∀id, t. Q (Evar id) t) |
---|
| 615 | (Ideref : ∀e, t. P e → Q (Ederef e) t) |
---|
| 616 | (Iaddrof : ∀e, t. P e → Q (Eaddrof e) t) |
---|
| 617 | (Iunop : ∀op,arg,t. P arg → Q (Eunop op arg) t) |
---|
| 618 | (Ibinop : ∀op,arg1,arg2,t. P arg1 → P arg2 → Q (Ebinop op arg1 arg2) t) |
---|
| 619 | (Icast : ∀castt, e, t. P e → Q (Ecast castt e) t) |
---|
| 620 | (Icond : ∀e1,e2,e3,t. P e1 → P e2 → P e3 → Q (Econdition e1 e2 e3) t) |
---|
| 621 | (Iandbool : ∀e1,e2,t. P e1 → P e2 → Q (Eandbool e1 e2) t) |
---|
| 622 | (Iorbool : ∀e1,e2,t. P e1 → P e2 → Q (Eorbool e1 e2) t) |
---|
| 623 | (Isizeof : ∀sizeoft,t. Q (Esizeof sizeoft) t) |
---|
| 624 | (Ifield : ∀e,f,t. P e → Q (Efield e f) t) |
---|
| 625 | (Icost : ∀c,e,t. P e → Q (Ecost c e) t) |
---|
| 626 | (e : expr) on e : P e ≝ |
---|
| 627 | match e with |
---|
[2468] | 628 | [ Expr ed t ⇒ IE ed t (expr_desc_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost ed t) ] |
---|
[1883] | 629 | |
---|
[2076] | 630 | and expr_desc_ind2 |
---|
| 631 | (P : expr → Prop) (Q : expr_descr → type → Prop) |
---|
| 632 | (IE : ∀ed. ∀t. Q ed t → P (Expr ed t)) |
---|
| 633 | (Iconst_int : ∀sz, i, t. Q (Econst_int sz i) t) |
---|
| 634 | (Ivar : ∀id, t. Q (Evar id) t) |
---|
| 635 | (Ideref : ∀e, t. P e → Q (Ederef e) t) |
---|
| 636 | (Iaddrof : ∀e, t. P e → Q (Eaddrof e) t) |
---|
| 637 | (Iunop : ∀op,arg,t. P arg → Q (Eunop op arg) t) |
---|
| 638 | (Ibinop : ∀op,arg1,arg2,t. P arg1 → P arg2 → Q (Ebinop op arg1 arg2) t) |
---|
| 639 | (Icast : ∀castt, e, t. P e → Q (Ecast castt e) t) |
---|
| 640 | (Icond : ∀e1,e2,e3,t. P e1 → P e2 → P e3 → Q (Econdition e1 e2 e3) t) |
---|
| 641 | (Iandbool : ∀e1,e2,t. P e1 → P e2 → Q (Eandbool e1 e2) t) |
---|
| 642 | (Iorbool : ∀e1,e2,t. P e1 → P e2 → Q (Eorbool e1 e2) t) |
---|
| 643 | (Isizeof : ∀sizeoft,t. Q (Esizeof sizeoft) t) |
---|
| 644 | (Ifield : ∀e,f,t. P e → Q (Efield e f) t) |
---|
| 645 | (Icost : ∀c,e,t. P e → Q (Ecost c e) t) |
---|
| 646 | (ed : expr_descr) (t : type) on ed : Q ed t ≝ |
---|
| 647 | match ed with |
---|
| 648 | [ Econst_int sz i ⇒ Iconst_int sz i t |
---|
| 649 | | Evar id ⇒ Ivar id t |
---|
[2468] | 650 | | Ederef e ⇒ Ideref e t (expr_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e) |
---|
| 651 | | Eaddrof e ⇒ Iaddrof e t (expr_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e) |
---|
| 652 | | Eunop op e ⇒ Iunop op e t (expr_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e) |
---|
| 653 | | Ebinop op e1 e2 ⇒ Ibinop op e1 e2 t (expr_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e1) (expr_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e2) |
---|
| 654 | | Ecast castt e ⇒ Icast castt e t (expr_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e) |
---|
| 655 | | Econdition e1 e2 e3 ⇒ Icond e1 e2 e3 t (expr_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e1) (expr_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e2) (expr_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e3) |
---|
| 656 | | Eandbool e1 e2 ⇒ Iandbool e1 e2 t (expr_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e1) (expr_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e2) |
---|
| 657 | | Eorbool e1 e2 ⇒ Iorbool e1 e2 t (expr_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e1) (expr_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e2) |
---|
[2076] | 658 | | Esizeof sizeoft ⇒ Isizeof sizeoft t |
---|
[2468] | 659 | | Efield e field ⇒ Ifield e field t (expr_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e) |
---|
| 660 | | Ecost c e ⇒ Icost c e t (expr_ind2 P Q IE Iconst_int Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e) |
---|
[2076] | 661 | ]. |
---|
[1883] | 662 | |
---|
[2076] | 663 | (* Correctness: we can't use a lock-step simulation result. The exec_step for Sswitch will be matched |
---|
| 664 | by a non-constant number of evaluations in the converted program. More precisely, |
---|
| 665 | [seq_of_labeled_statement (select_switch sz n sl)] will be matched by all the steps |
---|
| 666 | necessary to execute all the "if-then-elses" corresponding to cases /before/ [n]. *) |
---|
| 667 | |
---|
[2227] | 668 | (* A version of simplify_switch hiding the ugly projs *) |
---|
| 669 | definition fresh_for_expression ≝ |
---|
[2332] | 670 | λe,u. fresh_for_univ SymbolTag (max_of_expr e) u. |
---|
[1883] | 671 | |
---|
[2076] | 672 | definition fresh_for_statement ≝ |
---|
[2332] | 673 | λs,u. fresh_for_univ SymbolTag (max_of_statement s) u. |
---|
[1883] | 674 | |
---|
[2227] | 675 | (* needed during mutual induction ... *) |
---|
| 676 | definition fresh_for_labeled_statements ≝ |
---|
[2332] | 677 | λls,u. fresh_for_univ ? (max_of_ls ls) u. |
---|
[2227] | 678 | |
---|
[2076] | 679 | definition fresh_for_function ≝ |
---|
[2332] | 680 | λf,u. fresh_for_univ SymbolTag (max_id_of_function f) u. |
---|
[1883] | 681 | |
---|
[2227] | 682 | (* misc properties of the max function on positives. *) |
---|
[1883] | 683 | |
---|
[2076] | 684 | lemma max_id_one_neutral : ∀v. max_id v (an_identifier ? one) = v. |
---|
| 685 | * #p whd in ⊢ (??%?); >max_one_neutral // qed. |
---|
| 686 | |
---|
| 687 | lemma max_id_commutative : ∀v1, v2. max_id v1 v2 = max_id v2 v1. |
---|
| 688 | * #p1 * #p2 whd in match (max_id ??) in ⊢ (??%%); |
---|
| 689 | >commutative_max // qed. |
---|
| 690 | |
---|
| 691 | lemma max_id_associative : ∀v1, v2, v3. max_id (max_id v1 v2) v3 = max_id v1 (max_id v2 v3). |
---|
| 692 | * #a * #b * #c whd in match (max_id ??) in ⊢ (??%%); >associative_max // |
---|
| 693 | qed. |
---|
[2332] | 694 | |
---|
[2227] | 695 | lemma fresh_max_split : ∀a,b,u. fresh_for_univ SymbolTag (max_id a b) u → fresh_for_univ ? a u ∧ fresh_for_univ ? b u. |
---|
| 696 | * #a * #b * #u normalize |
---|
| 697 | lapply (pos_compare_to_Prop a b) |
---|
| 698 | cases (pos_compare a b) whd in ⊢ (% → ?); #Hab |
---|
| 699 | [ 1: >(le_to_leb_true a b) try /2/ #Hbu @conj /2/ |
---|
| 700 | | 2: destruct >reflexive_leb /2/ |
---|
| 701 | | 3: >(not_le_to_leb_false a b) try /2/ #Hau @conj /2/ |
---|
| 702 | ] qed. |
---|
[2076] | 703 | |
---|
[2438] | 704 | lemma fresh_to_substatements : |
---|
| 705 | ∀s,u. fresh_for_statement s u → |
---|
| 706 | substatement_P s (λs'. fresh_for_statement s' u) (λe. fresh_for_expression e u). |
---|
| 707 | #s #u cases s |
---|
| 708 | whd in match (fresh_for_statement ??); |
---|
| 709 | whd in match (substatement_P ???); try /2/ |
---|
| 710 | [ 1: #e1 #e2 |
---|
| 711 | whd in match (fresh_for_statement ??); |
---|
| 712 | whd in match (substatement_P ???); |
---|
| 713 | #H lapply (fresh_max_split … H) * /2 by conj/ |
---|
| 714 | | 2: #e1 #e2 #args |
---|
| 715 | whd in match (fresh_for_statement ??); |
---|
| 716 | whd in match (substatement_P ???); |
---|
| 717 | cases e1 normalize nodelta |
---|
| 718 | [ 1: #H lapply (fresh_max_split … H) * #HA #HB @conj try @HA |
---|
| 719 | elim args in HB; try /2 by I/ #hd #tl normalize nodelta #Hind #HB |
---|
| 720 | elim (fresh_max_split … HB) #HC #HD |
---|
| 721 | whd in match (foldr ?????) in HD; |
---|
| 722 | elim (fresh_max_split … HD) #HE #HF |
---|
| 723 | @conj try assumption |
---|
| 724 | @Hind >max_id_commutative >max_id_one_neutral @HF |
---|
| 725 | | 2: #expr #H cases (fresh_max_split … H) #HA normalize nodelta #HB |
---|
| 726 | cases (fresh_max_split … HB) #HC #HD @conj try @conj try // elim args in HD; try // |
---|
| 727 | #e #l #Hind #HD |
---|
| 728 | whd in match (foldr ?????) in HD; |
---|
| 729 | elim (fresh_max_split … HD) #HE #HF |
---|
| 730 | @conj try assumption |
---|
| 731 | @Hind @HF ] |
---|
| 732 | | 3: #stmt1 #stmt2 whd in ⊢ (% → %); @fresh_max_split |
---|
| 733 | | 4: #e #s1 #s2 whd in ⊢ (% → %); #H lapply (fresh_max_split … H) * |
---|
| 734 | #H1 @fresh_max_split |
---|
| 735 | | 5: #e1 #s whd in ⊢ (% → %); #H @(fresh_max_split … H) |
---|
| 736 | | 6: #e1 #s whd in ⊢ (% → %); #H @(fresh_max_split … H) |
---|
| 737 | | 7: #s1 #e #s2 #s3 whd in ⊢ (% → %); #H lapply (fresh_max_split … H) * #H1 #H2 |
---|
| 738 | @conj try @conj try @I try @conj try @I |
---|
| 739 | elim (fresh_max_split … H1) elim (fresh_max_split … H2) /2/ |
---|
| 740 | | 8: #opt cases opt try /2/ |
---|
| 741 | | 9: #e #ls #H whd @conj lapply (fresh_max_split … H) * #HA #HB try // lapply HB |
---|
| 742 | @(labeled_statements_ind … ls) |
---|
| 743 | [ 1: #s' #H' // |
---|
| 744 | | 2: #sz #i #s' #tl #Hind #H lapply (fresh_max_split … H) * #H1 #H2 whd @conj |
---|
| 745 | [ 1: // |
---|
| 746 | | 2: @Hind @H1 ] ] |
---|
| 747 | | 10: #lab #stmt #H whd lapply (fresh_max_split … H) * // |
---|
| 748 | ] qed. |
---|
| 749 | |
---|
[2227] | 750 | (* Auxilliary commutation lemma used in [substatement_fresh]. *) |
---|
| 751 | lemma foldl_max : ∀l,a,b. |
---|
| 752 | foldl ?? (λacc,elt.max_id (max_of_expr elt) acc) (max_id a b) l = |
---|
| 753 | max_id a (foldl ?? (λacc,elt.max_id (max_of_expr elt) acc) b l). |
---|
| 754 | #l elim l |
---|
| 755 | [ 1: * #a * #b whd in match (foldl ?????) in ⊢ (??%%); @refl |
---|
| 756 | | 2: #hd #tl #Hind #a #b whd in match (foldl ?????) in ⊢ (??%%); |
---|
| 757 | <Hind <max_id_commutative >max_id_associative >(max_id_commutative b ?) @refl |
---|
| 758 | ] qed. |
---|
| 759 | |
---|
[2332] | 760 | (* Lookup functions in list environments (used to type local variables in functions) *) |
---|
| 761 | let rec mem_assoc_env (i : ident) (l : list (ident×type)) on l : bool ≝ |
---|
| 762 | match l with |
---|
| 763 | [ nil ⇒ false |
---|
| 764 | | cons hd tl ⇒ |
---|
| 765 | let 〈id, ty〉 ≝ hd in |
---|
| 766 | match identifier_eq SymbolTag i id with |
---|
| 767 | [ inl Hid_eq ⇒ true |
---|
| 768 | | inr Hid_neq ⇒ mem_assoc_env i tl |
---|
| 769 | ] |
---|
| 770 | ]. |
---|
[2227] | 771 | |
---|
[2332] | 772 | (* --------------------------------------------------------------------------- *) |
---|
| 773 | (* Memory extensions (limited form on memoryInjection.ma). Note that we state the |
---|
| 774 | properties at the back-end level. *) |
---|
| 775 | (* --------------------------------------------------------------------------- *) |
---|
| 776 | |
---|
[2387] | 777 | (* A writeable_block is a block that is: |
---|
| 778 | . valid |
---|
| 779 | . non-empty (i.e. it has been allocated a non-empty size) |
---|
| 780 | *) |
---|
| 781 | record nonempty_block (m : mem) (b : block) : Prop ≝ |
---|
| 782 | { |
---|
[2448] | 783 | wb_valid : valid_block m b; |
---|
| 784 | wb_nonempty : low (blocks m b) < high (blocks m b) |
---|
[2438] | 785 | }. |
---|
[2298] | 786 | |
---|
[2387] | 787 | (* Type stating that m2 is an extension of m1, parameterised by a list of blocks where we can write freely *) |
---|
| 788 | record sr_memext (m1 : mem) (m2 : mem) (writeable : list block) : Prop ≝ |
---|
| 789 | { (* Non-empty blocks are preserved as they are. This entails [load_sim]. *) |
---|
| 790 | me_nonempty : ∀b. nonempty_block m1 b → nonempty_block m2 b ∧ blocks m1 b = blocks m2 b; |
---|
| 791 | (* These blocks are valid in [m2] *) |
---|
| 792 | me_writeable_valid : ∀b. meml ? b writeable → nonempty_block m2 b; |
---|
| 793 | (* blocks in [m1] than can be validly pointed to cannot be in [me_writeable]. *) |
---|
[2438] | 794 | me_not_writeable : ∀b. nonempty_block m1 b → ¬ (meml ? b writeable) |
---|
| 795 | |
---|
| 796 | (* This field is not entailed [me_not_writeable] and is necessary to prove valid |
---|
[2387] | 797 | pointer conservation after a [free]. *) |
---|
[2438] | 798 | |
---|
[2387] | 799 | (* Extension blocks contain nothing in [m1] *) |
---|
| 800 | (* me_not_mapped : ∀b. meml … b me_writeable → blocks m1 b = empty_block OZ OZ; *) |
---|
[2332] | 801 | (* Valid pointers are still valid in m2. One could think that this is superfluous as |
---|
| 802 | being implied by me_inj, and it is but for a small detail: valid_pointer allows a pointer |
---|
| 803 | to be one off the end of a block bound. The internal check in beloadv does not. |
---|
| 804 | valid_pointer should be understood as "pointer making sense" rather than "pointer from |
---|
| 805 | which you can load stuff". [mi_valid_pointers] is used for instance when proving the |
---|
| 806 | semantics preservation for equality testing (where we check that the pointers we |
---|
| 807 | compare are valid before being equal). |
---|
| 808 | *) |
---|
[2438] | 809 | (* me_valid_pointers : ∀p. |
---|
[2332] | 810 | valid_pointer m1 p = true → |
---|
[2438] | 811 | valid_pointer m2 p = true *) |
---|
[2227] | 812 | }. |
---|
[2387] | 813 | |
---|
[2438] | 814 | (* Since we removed end_pointers, we can prove some stuff that was previously given as a field of |
---|
| 815 | sr_memext. *) |
---|
| 816 | lemma me_not_writeable_ptr : |
---|
| 817 | ∀m1,m2,writeable. |
---|
| 818 | sr_memext m1 m2 writeable → |
---|
| 819 | ∀p. valid_pointer m1 p = true → ¬ (meml ? (pblock p) writeable). |
---|
| 820 | #m1 #m2 #writeable #Hext #p #Hvalid |
---|
| 821 | cut (nonempty_block m1 (pblock p)) |
---|
| 822 | [ 1: cases (valid_pointer_to_Prop … Hvalid) * #HA #HB #HC % // |
---|
| 823 | /2 by Zle_to_Zlt_to_Zlt/ |
---|
| 824 | | 2: @(me_not_writeable … Hext) ] |
---|
| 825 | qed. |
---|
| 826 | |
---|
[2387] | 827 | (* If we have a memory extension, we can simulate loads *) |
---|
| 828 | lemma sr_memext_load_sim : ∀m1,m2,writeable. sr_memext m1 m2 writeable → load_sim m1 m2. |
---|
| 829 | #m1 #m2 #writeable #Hext #ptr #bev whd in match (beloadv ??) in ⊢ (% → %); |
---|
| 830 | #H cut (nonempty_block m1 (pblock ptr) ∧ |
---|
| 831 | Zle (low (blocks m1 (pblock ptr))) |
---|
| 832 | (Z_of_unsigned_bitvector 16 (offv (poff ptr))) ∧ |
---|
| 833 | Zlt (Z_of_unsigned_bitvector 16 (offv (poff ptr))) |
---|
| 834 | (high (blocks m1 (pblock ptr))) ∧ |
---|
| 835 | bev = (contents (blocks m1 (pblock ptr)) (Z_of_unsigned_bitvector 16 (offv (poff ptr))))) |
---|
| 836 | [ @conj try @conj try @conj try % |
---|
| 837 | [ 1: @Zltb_true_to_Zlt ] |
---|
| 838 | cases (Zltb (block_id (pblock ptr)) (nextblock m1)) in H; normalize nodelta |
---|
| 839 | [ 1: // |
---|
| 840 | | 2,4,6,8,10: #Habsurd destruct ] |
---|
| 841 | generalize in match (Z_of_unsigned_bitvector offset_size (offv (poff ptr))); #z |
---|
| 842 | lapply (Zleb_true_to_Zle (low (blocks m1 (pblock ptr))) z) |
---|
| 843 | lapply (Zltb_true_to_Zlt z (high (blocks m1 (pblock ptr)))) |
---|
| 844 | cases (Zleb (low (blocks m1 (pblock ptr))) z) |
---|
| 845 | cases (Zltb z (high (blocks m1 (pblock ptr)))) #H1 #H2 |
---|
| 846 | [ 2,3,4,6,7,8,10,11,12,14,15,16: normalize #Habsurd destruct ] normalize #Heq |
---|
| 847 | lapply (H1 (refl ??)) lapply (H2 (refl ??)) |
---|
| 848 | #Hle #Hlt destruct try assumption try @refl |
---|
| 849 | @(Zle_to_Zlt_to_Zlt … Hle Hlt) ] |
---|
| 850 | * * * #Hnonempty #Hlow #Hhigh #Hres lapply (me_nonempty … Hext … Hnonempty) * |
---|
| 851 | * #Hvalid #Hlt #Hblocks_eq |
---|
| 852 | >(Zlt_to_Zltb_true … Hvalid) normalize <Hblocks_eq |
---|
| 853 | >(Zle_to_Zleb_true … Hlow) >(Zlt_to_Zltb_true … Hhigh) normalize |
---|
| 854 | >Hres @refl |
---|
| 855 | qed. |
---|
| 856 | |
---|
[2438] | 857 | lemma me_valid_pointers : |
---|
| 858 | ∀m1,m2,writeable. |
---|
| 859 | sr_memext m1 m2 writeable → |
---|
| 860 | ∀p. valid_pointer m1 p = true → valid_pointer m2 p = true. |
---|
| 861 | * #contents1 #nextblock1 #Hnextblock_pos1 |
---|
| 862 | * #contents2 #nextblock2 #Hnextblock_pos2 #writeable #Hmemext * #pb #po #Hvalid |
---|
| 863 | cut (nonempty_block (mk_mem contents1 nextblock1 Hnextblock_pos1) pb) |
---|
| 864 | [ 1: cases (valid_pointer_to_Prop … Hvalid) * #HA #HB #HC % // |
---|
| 865 | /2 by Zle_to_Zlt_to_Zlt/ ] |
---|
| 866 | #Hnonempty lapply (me_nonempty … Hmemext … Hnonempty) * * #Hvalid_block #Hlow_lt_high |
---|
| 867 | #Hcontents_eq normalize >(Zlt_to_Zltb_true … Hvalid_block) normalize nodelta |
---|
| 868 | <Hcontents_eq cases (valid_pointer_to_Prop … Hvalid) * #_ #Hle #Hlt |
---|
| 869 | >(Zle_to_Zleb_true … Hle) normalize nodelta |
---|
| 870 | >(Zlt_to_Zltb_true … Hlt) @refl |
---|
| 871 | qed. |
---|
| 872 | |
---|
[2387] | 873 | (* --------------------------------------------------------------------------- *) |
---|
| 874 | (* Some lemmas on environments and their contents *) |
---|
| 875 | |
---|
| 876 | |
---|
| 877 | (* Definition of environment inclusion and equivalence *) |
---|
| 878 | (* Environment "inclusion". *) |
---|
| 879 | definition environment_sim ≝ λenv1,env2. |
---|
| 880 | ∀id, res. lookup SymbolTag block env1 id = Some ? res → |
---|
| 881 | lookup SymbolTag block env2 id = Some ? res. |
---|
| 882 | |
---|
| 883 | lemma environment_sim_invert_aux : ∀en1,en2. |
---|
| 884 | (∀id,res. lookup_opt block id en1 = Some ? res → lookup_opt ? id en2 = Some ? res) → |
---|
| 885 | ∀id. lookup_opt ? id en2 = None ? → lookup_opt ? id en1 = None ?. |
---|
| 886 | #en1 elim en1 try // |
---|
| 887 | #opt1 #left1 #right1 #Hindl1 #Hindr1 #en2 #Hsim |
---|
| 888 | normalize #id elim id normalize nodelta |
---|
| 889 | [ 1: #Hlookup cases opt1 in Hsim; try // #res #Hsim lapply (Hsim one res (refl ??)) |
---|
| 890 | #Hlookup2 >Hlookup2 in Hlookup; #H @H |
---|
| 891 | | 2: #id' cases en2 in Hsim; |
---|
| 892 | [ 1: normalize #Hsim #_ #_ lapply (Hsim (p1 id')) normalize nodelta |
---|
| 893 | cases (lookup_opt block id' right1) try // |
---|
| 894 | #res #Hsim' lapply (Hsim' ? (refl ??)) #Habsurd destruct |
---|
| 895 | | 2: #opt2 #left2 #right2 #Hsim #Hlookup whd in ⊢ ((??%?) → ?); #Hlookup' |
---|
| 896 | @(Hindr1 right2) try // #id0 #res0 |
---|
| 897 | lapply (Hsim (p1 id0) res0) normalize #Hsol #H @Hsol @H ] |
---|
| 898 | | 3: #id' cases en2 in Hsim; |
---|
| 899 | [ 1: normalize #Hsim #_ #_ lapply (Hsim (p0 id')) normalize nodelta |
---|
| 900 | cases (lookup_opt block id' left1) try // |
---|
| 901 | #res #Hsim' lapply (Hsim' ? (refl ??)) #Habsurd destruct |
---|
| 902 | | 2: #opt2 #left2 #right2 #Hsim #Hlookup whd in ⊢ ((??%?) → ?); #Hlookup' |
---|
| 903 | @(Hindl1 left2) try // #id0 #res0 |
---|
| 904 | lapply (Hsim (p0 id0) res0) normalize #Hsol #H @Hsol @H ] |
---|
| 905 | ] qed. |
---|
[2438] | 906 | |
---|
[2387] | 907 | lemma environment_sim_invert : |
---|
| 908 | ∀en1,en2. environment_sim en1 en2 → |
---|
| 909 | ∀id. lookup SymbolTag block en2 id = None ? → |
---|
| 910 | lookup SymbolTag block en1 id = None ?. |
---|
| 911 | * #en1 * #en2 #Hsim * #id @environment_sim_invert_aux |
---|
| 912 | #id' #res #Hlookup normalize in Hsim; |
---|
| 913 | lapply (Hsim (an_identifier … id') res) normalize #Hsol @Hsol @Hlookup |
---|
| 914 | qed. |
---|
| 915 | |
---|
| 916 | (* Environment equivalence. *) |
---|
| 917 | definition environment_eq ≝ λenv1,env2. environment_sim env1 env2 ∧ environment_sim env2 env1. |
---|
| 918 | |
---|
| 919 | lemma symmetric_environment_eq : ∀env1,env2. environment_eq env1 env2 → environment_eq env2 env1. |
---|
| 920 | #env1 #env2 * #Hsim1 #Hsim2 % // qed. |
---|
| 921 | |
---|
| 922 | lemma reflexive_environment_eq : ∀env. environment_eq env env. |
---|
| 923 | #env % // qed. |
---|
| 924 | |
---|
| 925 | (* An environment [e2] is a disjoint extension of [e1] iff (the new bindings are |
---|
| 926 | fresh and [e2] is equivalent to adding extension blocks to [e1]). *) |
---|
| 927 | definition disjoint_extension ≝ |
---|
| 928 | λ(e1, e2 : env). |
---|
| 929 | λ(new_vars : list (ident × type)). |
---|
| 930 | (∀id. mem_assoc_env id new_vars = true → lookup ?? e1 id = None ?) ∧ (* extension not in e1 *) |
---|
| 931 | (∀id. mem_assoc_env id new_vars = true → ∃res.lookup ?? e2 id = Some ? res) ∧ (* all of the extension is in e2 *) |
---|
| 932 | (∀id. mem_assoc_env id new_vars = false → lookup ?? e1 id = lookup ?? e2 id). (* only [new_vars] extends e2 *) |
---|
[2227] | 933 | |
---|
[2387] | 934 | lemma disjoint_extension_to_inclusion : |
---|
| 935 | ∀e1,e2,vars. disjoint_extension e1 e2 vars → |
---|
| 936 | environment_sim e1 e2. |
---|
| 937 | #e1 #e2 #vars * * #HA #HB #HC whd #id #res |
---|
| 938 | @(match (mem_assoc_env id vars) return λx.(mem_assoc_env id vars = x) → ? |
---|
| 939 | with |
---|
| 940 | [ true ⇒ λH. ? |
---|
| 941 | | false ⇒ λH. ? |
---|
| 942 | ] (refl ? (mem_assoc_env id vars))) |
---|
| 943 | [ 1: #Hlookup lapply (HA ? H) #Habsurd >Habsurd in Hlookup; #H destruct |
---|
| 944 | | 2: #Hlookup <(HC ? H) assumption ] |
---|
| 945 | qed. |
---|
| 946 | |
---|
| 947 | (* Small aux lemma to decompose folds on maps with list accumulators *) |
---|
| 948 | lemma fold_to_concat : ∀A:Type[0].∀m:positive_map A.∀l.∀f. |
---|
| 949 | (fold ?? (λx,a,el. 〈an_identifier SymbolTag (f x), a〉::el) m l) |
---|
| 950 | = (fold ?? (λx,a,el. 〈an_identifier SymbolTag (f x), a〉::el) m []) @ l. |
---|
| 951 | #A #m elim m |
---|
| 952 | [ 1: #l #f normalize @refl |
---|
| 953 | | 2: #optblock #left #right |
---|
| 954 | #Hind1 #Hind2 #l #f |
---|
| 955 | whd in match (fold ?????) in ⊢ (??%%); |
---|
| 956 | cases optblock |
---|
| 957 | [ 1: normalize nodelta >Hind1 >Hind2 >Hind2 in ⊢ (???%); |
---|
| 958 | >associative_append @refl |
---|
| 959 | | 2: #block normalize nodelta >Hind1 >Hind2 >Hind2 in ⊢ (???%); |
---|
| 960 | >Hind1 in ⊢ (???%); >append_cons <associative_append @refl |
---|
| 961 | ] |
---|
| 962 | ] qed. |
---|
| 963 | |
---|
| 964 | lemma map_proj_fold : ∀A:Type[0].∀m:positive_map A. ∀f. ∀l. |
---|
| 965 | map ?? (λx.\snd x) (fold ?? (λx,a,el.〈an_identifier SymbolTag x,a〉::el) m l) = |
---|
| 966 | map ?? (λx.\snd x) (fold ?? (λx,a,el.〈an_identifier SymbolTag (f x),a〉::el) m l). |
---|
| 967 | #A #m elim m |
---|
| 968 | [ 1: #f #l normalize @refl |
---|
| 969 | | 2: #opt #left #right #Hind1 #Hind2 #f #l |
---|
| 970 | normalize cases opt |
---|
| 971 | [ 1: normalize nodelta >fold_to_concat >fold_to_concat in ⊢ (???%); |
---|
| 972 | <map_append <map_append <Hind2 <Hind2 in ⊢ (???%); |
---|
| 973 | <Hind1 <Hind1 in ⊢ (???%); @refl |
---|
| 974 | | 2: #elt normalize nodelta >fold_to_concat >fold_to_concat in ⊢ (???%); |
---|
| 975 | <map_append <map_append <Hind2 <Hind2 in ⊢ (???%); |
---|
| 976 | <(Hind1 p0) <Hind1 in ⊢ (???%); |
---|
| 977 | >(fold_to_concat ?? (〈an_identifier SymbolTag one,elt〉::l)) |
---|
| 978 | >(fold_to_concat ?? (〈an_identifier SymbolTag (f one),elt〉::l)) |
---|
| 979 | <map_append <map_append normalize in match (map ??? (cons ???)); @refl |
---|
| 980 | ] |
---|
| 981 | ] qed. |
---|
| 982 | |
---|
| 983 | lemma lookup_entails_block : ∀en:env.∀id,res. |
---|
| 984 | lookup SymbolTag block en id = Some ? res → |
---|
| 985 | meml ? res (blocks_of_env en). |
---|
| 986 | * #map * #id #res |
---|
| 987 | whd in match (blocks_of_env ?); |
---|
| 988 | whd in match (elements ???); |
---|
| 989 | whd in match (lookup ????); |
---|
| 990 | normalize nodelta |
---|
| 991 | lapply res lapply id -id -res |
---|
| 992 | elim map |
---|
| 993 | [ 1: #id #res normalize #Habsurd destruct (Habsurd) |
---|
| 994 | | 2: #optblock #left #right #Hind1 #Hind2 #id #res #Hind3 |
---|
| 995 | whd in match (fold ?????); |
---|
| 996 | cases optblock in Hind3; |
---|
| 997 | [ 1: normalize nodelta |
---|
| 998 | whd in match (lookup_opt ???); |
---|
| 999 | cases id normalize nodelta |
---|
| 1000 | [ 1: #Habsurd destruct (Habsurd) |
---|
| 1001 | | 2: #p #Hright lapply (Hind2 … Hright) |
---|
| 1002 | normalize >fold_to_concat in ⊢ (? → %); |
---|
| 1003 | <map_append #Haux @mem_append_backwards %1 |
---|
| 1004 | <map_proj_fold @Haux |
---|
| 1005 | | 3: #p #Hleft lapply (Hind1 … Hleft) |
---|
| 1006 | normalize >fold_to_concat in ⊢ (? → %); |
---|
| 1007 | <map_append #Haux @mem_append_backwards %2 |
---|
| 1008 | <map_proj_fold @Haux ] |
---|
| 1009 | | 2: #blo whd in match (lookup_opt ???); |
---|
| 1010 | normalize >fold_to_concat <map_append |
---|
| 1011 | cases id normalize nodelta |
---|
| 1012 | [ 1: #Heq destruct (Heq) |
---|
| 1013 | @mem_append_backwards %2 >fold_to_concat |
---|
| 1014 | <map_append @mem_append_backwards %2 normalize %1 @refl |
---|
| 1015 | | 2: #p #Hlookup lapply (Hind2 … Hlookup) #H |
---|
| 1016 | @mem_append_backwards %1 |
---|
| 1017 | <map_proj_fold @H |
---|
| 1018 | | 3: #p #Hlookup lapply (Hind1 … Hlookup) #H |
---|
| 1019 | @mem_append_backwards %2 >fold_to_concat |
---|
| 1020 | <map_append @mem_append_backwards %1 |
---|
| 1021 | <map_proj_fold @H |
---|
| 1022 | ] |
---|
| 1023 | ] |
---|
| 1024 | ] qed. |
---|
| 1025 | |
---|
| 1026 | lemma blocks_of_env_cons : |
---|
| 1027 | ∀en,id,hd. mem ? hd (blocks_of_env (add SymbolTag block en id hd)). |
---|
| 1028 | #en #id #hd @(lookup_entails_block … id) |
---|
| 1029 | cases id #p elim p try /2/ qed. |
---|
| 1030 | |
---|
| 1031 | lemma in_blocks_exists_id : ∀env.∀bl. meml … bl (blocks_of_env env) → ∃id. lookup SymbolTag block env id = Some ? bl. |
---|
| 1032 | #env elim env #m elim m |
---|
| 1033 | [ 1: #bl normalize @False_ind |
---|
| 1034 | | 2: #opt #left #right #Hind1 #Hind2 #bl normalize |
---|
| 1035 | >fold_to_concat <map_append #H |
---|
| 1036 | elim (mem_append_forward ???? H) |
---|
| 1037 | [ 1: <map_proj_fold -H #H lapply (Hind2 … H) |
---|
| 1038 | * * #id #Hlookup normalize in Hlookup; |
---|
| 1039 | %{(an_identifier SymbolTag (p1 id))} normalize nodelta @Hlookup |
---|
| 1040 | | 2: <map_proj_fold cases opt |
---|
| 1041 | [ 1: normalize -H #H lapply (Hind1 … H) |
---|
| 1042 | * * #id #Hlookup normalize in Hlookup; |
---|
| 1043 | %{(an_identifier SymbolTag (p0 id))} normalize nodelta @Hlookup |
---|
| 1044 | | 2: #bl' normalize >fold_to_concat <map_append normalize |
---|
| 1045 | #H' elim (mem_append_forward ???? H') |
---|
| 1046 | [ 1: -H #H lapply (Hind1 … H) * * #id normalize #Hlookup |
---|
| 1047 | %{(an_identifier ? (p0 id))} normalize nodelta @Hlookup |
---|
| 1048 | | 2: normalize * [ 2: @False_ind ] |
---|
| 1049 | #Heq destruct (Heq) |
---|
| 1050 | %{(an_identifier SymbolTag one)} @refl |
---|
| 1051 | ] |
---|
| 1052 | ] |
---|
| 1053 | ] |
---|
| 1054 | ] qed. |
---|
| 1055 | |
---|
| 1056 | let rec inclusion_elim |
---|
| 1057 | (A : Type[0]) |
---|
| 1058 | (m1, m2 : positive_map A) |
---|
| 1059 | (P : positive_map A → positive_map A → Prop) |
---|
| 1060 | (H1 : ∀m2. P (pm_leaf A) m2) |
---|
| 1061 | (H2 : ∀opt1,left1,right1. P left1 (pm_leaf A) → P right1 (pm_leaf A) → P (pm_node A opt1 left1 right1) (pm_leaf A)) |
---|
| 1062 | (H3 : ∀opt1,left1,right1,opt2,left2,right2. P left1 left2 → P right1 right2 → P (pm_node A opt1 left1 right1) (pm_node A opt2 left2 right2)) |
---|
| 1063 | on m1 : P m1 m2 ≝ |
---|
| 1064 | match m1 with |
---|
| 1065 | [ pm_leaf ⇒ |
---|
| 1066 | H1 m2 |
---|
| 1067 | | pm_node opt1 left1 right1 ⇒ |
---|
| 1068 | match m2 with |
---|
| 1069 | [ pm_leaf ⇒ |
---|
| 1070 | H2 opt1 left1 right1 (inclusion_elim A left1 (pm_leaf A) P H1 H2 H3) (inclusion_elim A right1 (pm_leaf A) P H1 H2 H3) |
---|
| 1071 | | pm_node opt2 left2 right2 ⇒ |
---|
| 1072 | H3 opt1 left1 right1 opt2 left2 right2 (inclusion_elim A left1 left2 P H1 H2 H3) (inclusion_elim A right1 right2 P H1 H2 H3) |
---|
| 1073 | ] |
---|
| 1074 | ]. |
---|
| 1075 | |
---|
| 1076 | (* Environment inclusion entails block inclusion. *) |
---|
| 1077 | lemma environment_sim_blocks_inclusion : |
---|
| 1078 | ∀env1, env2. environment_sim env1 env2 → lset_inclusion ? (blocks_of_env env1) (blocks_of_env env2). |
---|
| 1079 | * #m1 * #m2 @(inclusion_elim … m1 m2) -m1 -m2 |
---|
| 1080 | [ 1: #m2 normalize #_ @I |
---|
| 1081 | | 2: #opt1 #left1 #right1 #Hind1 #Hind2 #Hsim |
---|
| 1082 | normalize >fold_to_concat in ⊢ (???%); <map_append @All_append |
---|
| 1083 | [ 1: <map_proj_fold @Hind2 #id #res elim id #id' #Hlookup @(Hsim (an_identifier ? (p1 id')) res Hlookup) |
---|
| 1084 | | 2: cases opt1 in Hsim; |
---|
| 1085 | [ 1: normalize nodelta #Hsim |
---|
| 1086 | <map_proj_fold @Hind1 #id #res elim id #id' #Hlookup @(Hsim (an_identifier ? (p0 id')) res Hlookup) |
---|
| 1087 | | 2: #bl #Hsim lapply (Hsim (an_identifier ? one) bl ?) normalize try @refl |
---|
| 1088 | #Habsurd destruct (Habsurd) |
---|
| 1089 | ] |
---|
| 1090 | ] |
---|
| 1091 | | 3: #opt1 #left1 #right1 #opt2 #left2 #right2 #Hind1 #Hind2 #Hsim |
---|
| 1092 | normalize >fold_to_concat >fold_to_concat in ⊢ (???%); |
---|
| 1093 | <map_append <map_append in ⊢ (???%); @All_append |
---|
| 1094 | [ 1: cases opt2; normalize nodelta |
---|
| 1095 | [ 1: <map_proj_fold <map_proj_fold in ⊢ (???%); <(map_proj_fold ?? p0) |
---|
| 1096 | cut (environment_sim (an_id_map SymbolTag block right1) (an_id_map SymbolTag block right2)) |
---|
| 1097 | [ 1: * #id' #res #Hlookup |
---|
| 1098 | lapply (Hsim (an_identifier ? (p1 id')) res) normalize #H @H @Hlookup ] |
---|
| 1099 | #Hsim' lapply (Hind2 Hsim') @All_mp |
---|
| 1100 | #a #Hmem @mem_append_backwards %1 @Hmem |
---|
| 1101 | | 2: #bl <map_proj_fold <map_proj_fold in ⊢ (???%); <(map_proj_fold ?? p0) |
---|
| 1102 | cut (environment_sim (an_id_map SymbolTag block right1) (an_id_map SymbolTag block right2)) |
---|
| 1103 | [ 1: * #id' #res #Hlookup |
---|
| 1104 | lapply (Hsim (an_identifier ? (p1 id')) res) normalize #H @H @Hlookup ] |
---|
| 1105 | #Hsim' lapply (Hind2 Hsim') @All_mp |
---|
| 1106 | #a #Hmem @mem_append_backwards %1 @Hmem ] |
---|
| 1107 | | 2: cut (environment_sim (an_id_map SymbolTag block left1) (an_id_map SymbolTag block left2)) |
---|
| 1108 | [ 1: * #id' #res #Hlookup |
---|
| 1109 | lapply (Hsim (an_identifier ? (p0 id')) res) normalize #H @H @Hlookup ] #Hsim' |
---|
| 1110 | lapply (Hind1 … Hsim') |
---|
| 1111 | <map_proj_fold <map_proj_fold in ⊢ (? → (???%)); <(map_proj_fold ?? p0) |
---|
| 1112 | cases opt1 in Hsim; normalize nodelta |
---|
| 1113 | [ 1: #Hsim @All_mp #a #Hmem @mem_append_backwards %2 |
---|
| 1114 | cases opt2 normalize nodelta |
---|
| 1115 | [ 1: @Hmem |
---|
| 1116 | | 2: #bl >fold_to_concat <map_append @mem_append_backwards %1 @Hmem ] |
---|
| 1117 | | 2: #bl #Hsim #Hmem >fold_to_concat in ⊢ (???%); <map_append @All_append |
---|
| 1118 | [ 2: normalize @conj try @I |
---|
| 1119 | cases opt2 in Hsim; |
---|
| 1120 | [ 1: #Hsim lapply (Hsim (an_identifier ? one) bl (refl ??)) |
---|
| 1121 | normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) |
---|
| 1122 | | 2: #bl2 #Hsim lapply (Hsim (an_identifier ? one) bl (refl ??)) |
---|
| 1123 | normalize in ⊢ (% → ?); #Heq >Heq normalize nodelta |
---|
| 1124 | @mem_append_backwards %2 >fold_to_concat <map_append |
---|
| 1125 | @mem_append_backwards %2 normalize %1 @refl ] |
---|
| 1126 | | 1: cases opt2 in Hsim; |
---|
| 1127 | [ 1: #Hsim lapply (Hsim (an_identifier ? one) bl (refl ??)) |
---|
| 1128 | normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) |
---|
| 1129 | | 2: #bl2 #Hsim lapply (Hsim (an_identifier ? one) bl (refl ??)) |
---|
| 1130 | normalize in ⊢ (% → ?); #Heq lapply (Hind1 Hsim') |
---|
| 1131 | @All_mp #a #Hmem >Heq normalize nodelta |
---|
| 1132 | @mem_append_backwards %2 >fold_to_concat <map_append |
---|
| 1133 | @mem_append_backwards %1 @Hmem ] ] |
---|
| 1134 | ] |
---|
| 1135 | ] |
---|
| 1136 | ] qed. |
---|
| 1137 | |
---|
| 1138 | |
---|
| 1139 | (* equivalent environments yield "equal" sets of block (cf. frontend_misc.ma) *) |
---|
| 1140 | lemma environment_eq_blocks_eq : ∀env1,env2. |
---|
| 1141 | environment_eq env1 env2 → |
---|
| 1142 | lset_eq ? (blocks_of_env env1) (blocks_of_env env2). |
---|
| 1143 | #env1 #env2 * #Hsim1 #Hsim2 @conj |
---|
| 1144 | @environment_sim_blocks_inclusion assumption |
---|
| 1145 | qed. |
---|
| 1146 | |
---|
| 1147 | (* [env_codomain env vars] is the image of vars through env seen as a function. *) |
---|
| 1148 | definition env_codomain : env → list (ident×type) → lset block ≝ λe,l. |
---|
| 1149 | foldi … (λid,block,acc. |
---|
| 1150 | if mem_assoc_env … id l then |
---|
| 1151 | block :: acc |
---|
| 1152 | else |
---|
| 1153 | acc |
---|
| 1154 | ) e [ ]. |
---|
| 1155 | |
---|
| 1156 | (* --------------------------------------------------------------------------- *) |
---|
| 1157 | |
---|
| 1158 | (* Two equivalent memories yield a trivial memory extension. *) |
---|
| 1159 | lemma memory_eq_to_mem_ext : ∀m1,m2. memory_eq m1 m2 → sr_memext m1 m2 [ ]. |
---|
| 1160 | * #contents1 #nextblock1 #Hpos * #contents2 #nextblock2 #Hpos' normalize * |
---|
| 1161 | #Hnextblock #Hcontents_eq destruct % |
---|
| 1162 | [ 1: #b #H @conj try % elim H try // |
---|
| 1163 | | 2: #b * |
---|
[2438] | 1164 | | 3: #b #_ normalize % // ] |
---|
| 1165 | qed. |
---|
[2387] | 1166 | |
---|
| 1167 | (* memory extensions form a preorder relation *) |
---|
| 1168 | |
---|
| 1169 | lemma memory_ext_transitive : |
---|
| 1170 | ∀m1,m2,m3,writeable1,writeable2. |
---|
| 1171 | sr_memext m1 m2 writeable1 → |
---|
| 1172 | sr_memext m2 m3 writeable2 → |
---|
| 1173 | sr_memext m1 m3 (writeable1 @ writeable2). |
---|
| 1174 | #m1 #m2 #m3 #writeable1 #writeable2 #H12 #H23 % |
---|
| 1175 | [ 1: #b #Hnonempty1 |
---|
| 1176 | lapply (me_nonempty … H12 b Hnonempty1) * #Hnonempty2 #Hblocks_eq |
---|
| 1177 | lapply (me_nonempty … H23 b Hnonempty2) * #Hnonempty3 #Hblocks_eq' @conj |
---|
| 1178 | try assumption >Hblocks_eq >Hblocks_eq' @refl |
---|
| 1179 | | 2: #b #Hmem lapply (mem_append_forward ???? Hmem) * |
---|
| 1180 | [ 1: #Hmem12 lapply (me_writeable_valid … H12 b Hmem12) #Hnonempty2 |
---|
| 1181 | elim (me_nonempty … H23 … Hnonempty2) // |
---|
| 1182 | | 2: #Hmem23 @(me_writeable_valid … H23 b Hmem23) ] |
---|
| 1183 | | 3: #b #Hvalid % #Hmem lapply (mem_append_forward ???? Hmem) * |
---|
| 1184 | [ 1: #Hmem12 |
---|
| 1185 | lapply (me_not_writeable … H12 … Hvalid) * #H @H assumption |
---|
| 1186 | | 2: #Hmem23 lapply (me_nonempty … H12 … Hvalid) * #Hvalid2 |
---|
| 1187 | lapply (me_not_writeable … H23 … Hvalid2) * #H #_ @H assumption |
---|
| 1188 | ] |
---|
[2438] | 1189 | ] qed. |
---|
[2387] | 1190 | |
---|
[2438] | 1191 | lemma memory_ext_reflexive : ∀m. sr_memext m m [ ]. |
---|
[2387] | 1192 | #m % /2/ #b * qed. |
---|
| 1193 | |
---|
| 1194 | (* --------------------------------------------------------------------------- *) |
---|
| 1195 | (* Lemmas relating memory extensions to [free] *) |
---|
| 1196 | |
---|
[2332] | 1197 | lemma beloadv_free_simulation : |
---|
[2387] | 1198 | ∀m1,m2,writeable,block,ptr,res. |
---|
| 1199 | ∀mem_hyp : sr_memext m1 m2 writeable. |
---|
[2332] | 1200 | beloadv (free m1 block) ptr = Some ? res → beloadv (free m2 block) ptr = Some ? res. |
---|
[2387] | 1201 | * #contents1 #nextblock1 #nextpos1 * #contents2 #nextblock2 #nextpos2 #writeable |
---|
| 1202 | * #br #bid * * #pr #pid #poff #res #Hext |
---|
| 1203 | (*#Hme_nonempty #Hme_writeable #Hme_nonempty #Hvalid_conserv*) |
---|
[2332] | 1204 | #Hload |
---|
| 1205 | lapply (beloadv_free_beloadv … Hload) #Hload_before_free |
---|
| 1206 | lapply (beloadv_free_blocks_neq … Hload) #Hblocks_neq |
---|
| 1207 | @beloadv_free_beloadv2 |
---|
| 1208 | [ 1: @Hblocks_neq ] |
---|
[2387] | 1209 | @(sr_memext_load_sim … Hext) assumption |
---|
[2227] | 1210 | qed. |
---|
| 1211 | |
---|
| 1212 | |
---|
[2438] | 1213 | (* Lifting the property of being valid after a free to memory extensions *) |
---|
[2387] | 1214 | lemma valid_pointer_free : ∀m1,m2,writeable. sr_memext m1 m2 writeable → ∀p,b. valid_pointer (free m1 b) p = true → valid_pointer (free m2 b) p = true. |
---|
| 1215 | #m1 #m2 #writeable #Hext #p #b #Hvalid |
---|
[2332] | 1216 | lapply (valid_free_to_valid … Hvalid) #Hvalid_before_free |
---|
| 1217 | lapply (me_valid_pointers … Hext … Hvalid_before_free) |
---|
| 1218 | lapply (valid_after_free … Hvalid) #Hneq |
---|
| 1219 | whd in match (free ??); |
---|
| 1220 | whd in match (update_block ????); |
---|
| 1221 | whd in match (valid_pointer ??) in ⊢ (% → %); |
---|
| 1222 | whd in match (low_bound ??) in ⊢ (% → %); |
---|
| 1223 | whd in match (high_bound ??) in ⊢ (% → %); |
---|
| 1224 | >(not_eq_block_rev … Hneq) normalize nodelta #H @H |
---|
[2227] | 1225 | qed. |
---|
| 1226 | |
---|
[2387] | 1227 | lemma nonempty_block_mismatch : ∀m,b,bl. |
---|
| 1228 | nonempty_block (free m bl) b → |
---|
| 1229 | nonempty_block m b ∧ b ≠ bl. |
---|
| 1230 | #m #b #bl #Hnonempty |
---|
| 1231 | @(eq_block_elim … b bl) |
---|
| 1232 | [ 1: #Heq >Heq in Hnonempty; * #_ normalize |
---|
| 1233 | cases (block_region bl) normalize >eqZb_reflexive normalize * |
---|
| 1234 | | 2: #Hneq @conj try assumption elim Hnonempty #Hvalid #Hlh % |
---|
| 1235 | [ 1: lapply Hvalid normalize // |
---|
| 1236 | | 2: lapply Hlh normalize |
---|
| 1237 | cases (block_region b) normalize nodelta |
---|
| 1238 | cases (block_region bl) normalize nodelta try // |
---|
| 1239 | @(eqZb_elim … (block_id b) (block_id bl)) |
---|
| 1240 | [ 1,3: * normalize * |
---|
| 1241 | | 2,4: #_ // ] ] ] |
---|
| 1242 | qed. |
---|
| 1243 | |
---|
| 1244 | lemma eqb_to_eq_block : ∀a,b : block. a == b = eq_block a b. |
---|
| 1245 | #a #b lapply (eqb_true ? a b) @(eq_block_elim … a b) |
---|
| 1246 | /2 by neq_block_eq_block_false, true_to_andb_true/ |
---|
| 1247 | qed. |
---|
| 1248 | |
---|
| 1249 | (* We can free in both sides of a memory extension if we take care of removing |
---|
| 1250 | the freed block from the set of writeable blocks. *) |
---|
| 1251 | lemma free_memory_ext : |
---|
| 1252 | ∀m1,m2,writeable,bl. |
---|
| 1253 | sr_memext m1 m2 writeable → |
---|
| 1254 | sr_memext (free m1 bl) (free m2 bl) (lset_remove ? writeable bl). |
---|
| 1255 | #m1 #m2 #writeable #bl #Hext % |
---|
| 1256 | [ 1: #b #Hnonempty lapply (nonempty_block_mismatch … Hnonempty) |
---|
| 1257 | * #Hnonempty' #Hblocks_neq lapply (me_nonempty … Hext … Hnonempty') * |
---|
| 1258 | #Hnonempty2 #Hcontents_eq @conj |
---|
| 1259 | [ 1: % try @(wb_valid … Hnonempty2) |
---|
| 1260 | whd in match (free ??); |
---|
| 1261 | whd in match (update_block ?????); |
---|
| 1262 | >(neq_block_eq_block_false … Hblocks_neq) normalize |
---|
| 1263 | try @(wb_nonempty … Hnonempty2) |
---|
| 1264 | | 2: whd in match (free ??) in ⊢ (??%%); |
---|
| 1265 | whd in match (update_block ?????) in ⊢ (??%%); |
---|
| 1266 | >(neq_block_eq_block_false … Hblocks_neq) |
---|
| 1267 | normalize nodelta assumption ] |
---|
| 1268 | | 2: #b #Hmem |
---|
| 1269 | cut (mem block b writeable ∧ b ≠ bl) |
---|
| 1270 | [ elim writeable in Hmem; |
---|
| 1271 | [ 1: normalize * |
---|
| 1272 | | 2: #hd #tl #Hind whd in match (filter ???); |
---|
| 1273 | >eqb_to_eq_block |
---|
| 1274 | @(eq_block_elim … hd bl) normalize in match (notb ?); normalize nodelta |
---|
| 1275 | [ 1: #Heq #H whd in match (meml ???); elim (Hind H) #H0 #H1 @conj |
---|
| 1276 | [ 1: %2 ] assumption |
---|
[2332] | 1277 | | 2: #Hneq whd in match (meml ???) in ⊢ (% → %); * |
---|
[2387] | 1278 | [ 1: #H destruct /3 by conj, or_introl, refl/ |
---|
| 1279 | | 2: #H elim (Hind H) #H1 #H2 /3 by conj, or_intror, refl/ ] ] ] |
---|
| 1280 | ] * #Hmem2 #Hblocks_neq |
---|
| 1281 | lapply (me_writeable_valid … Hext … Hmem2) * #Hvalid #Hnonempty % |
---|
| 1282 | try assumption whd in match (free ??); whd in match (update_block ?????); |
---|
| 1283 | >(neq_block_eq_block_false … Hblocks_neq) @Hnonempty |
---|
| 1284 | | 3: #p #Hvalid lapply (nonempty_block_mismatch … Hvalid) * #Hnonempty #Hblocks_neq |
---|
| 1285 | % #Hmem lapply (me_not_writeable … Hext … Hnonempty) * #H @H |
---|
| 1286 | elim writeable in Hmem; |
---|
| 1287 | [ 1: * |
---|
| 1288 | | 2: #hd #tl #Hind whd in match (filter ???) in ⊢ (% → ?); >eqb_to_eq_block |
---|
| 1289 | @(eq_block_elim … hd bl) normalize in match (notb ?); normalize nodelta |
---|
| 1290 | [ 1: #Heq #H normalize %2 @(Hind H) |
---|
| 1291 | | 2: #Hblocks_neq whd in match (meml ???); * |
---|
| 1292 | [ 1: #Hneq normalize %1 assumption |
---|
| 1293 | | 2: #Hmem normalize %2 @(Hind Hmem) ] |
---|
| 1294 | ] |
---|
| 1295 | ] |
---|
[2438] | 1296 | ] qed. |
---|
[2227] | 1297 | |
---|
[2438] | 1298 | |
---|
[2387] | 1299 | (* Freeing from an extension block is ok. *) |
---|
| 1300 | lemma memext_free_extended_conservation : |
---|
| 1301 | ∀m1,m2 : mem. |
---|
| 1302 | ∀writeable. |
---|
| 1303 | ∀mem_hyp : sr_memext m1 m2 writeable. |
---|
| 1304 | ∀b. meml ? b writeable → |
---|
| 1305 | sr_memext m1 (free m2 b) (lset_remove … writeable b). |
---|
| 1306 | #m1 #m2 #writeable #Hext #b #Hb_writeable % |
---|
| 1307 | [ 1: #bl #Hnonempty lapply (me_not_writeable … Hext … Hnonempty) #Hnot_mem |
---|
| 1308 | lapply (mem_not_mem_neq … Hb_writeable Hnot_mem) #Hblocks_neq |
---|
| 1309 | @conj |
---|
| 1310 | [ 2: whd in match (free ??); whd in match (update_block ?????); |
---|
| 1311 | >(neq_block_eq_block_false … (sym_neq … Hblocks_neq)) normalize |
---|
| 1312 | elim (me_nonempty … Hext … Hnonempty) // |
---|
| 1313 | | 1: % elim (me_nonempty … Hext … Hnonempty) * try // |
---|
| 1314 | #Hvalid2 #Hlh #Hcontents_eq whd in match (free ??); |
---|
| 1315 | whd in match (update_block ?????); |
---|
| 1316 | >(neq_block_eq_block_false … (sym_neq … Hblocks_neq)) normalize assumption |
---|
| 1317 | ] |
---|
| 1318 | | 2: #b' #Hmem (* contradiction in first premise *) |
---|
| 1319 | cut (mem block b' writeable ∧ b' ≠ b) |
---|
| 1320 | [ elim writeable in Hmem; |
---|
| 1321 | [ 1: normalize @False_ind |
---|
| 1322 | | 2: #hd #tl #Hind whd in match (filter ???); >eqb_to_eq_block |
---|
| 1323 | @(eq_block_elim … hd b) normalize in match (notb ?); normalize nodelta |
---|
| 1324 | [ 1: #Heq #H whd in match (meml ???); destruct |
---|
| 1325 | elim (Hind H) #Hmem #Hneq @conj try assumption %2 assumption |
---|
| 1326 | | 2: #Hneq whd in match (meml ???) in ⊢ (% → %); * |
---|
| 1327 | [ 1: #H @conj [ 1: %1 @H | 2: destruct @Hneq ] |
---|
| 1328 | | 2: #H elim (Hind H) #Hmem #Hneq' @conj try assumption %2 assumption ] |
---|
| 1329 | ] ] ] |
---|
| 1330 | * #Hb' #Hneq lapply (me_writeable_valid … Hext … Hb') #Hvalid % |
---|
| 1331 | [ 1: @(wb_valid … Hvalid) |
---|
| 1332 | | 2: whd in match (free ??); |
---|
| 1333 | whd in match (update_block ?????); |
---|
| 1334 | >(neq_block_eq_block_false … Hneq) |
---|
| 1335 | @(wb_nonempty … Hvalid) ] |
---|
| 1336 | | 3: #b' #Hnonempty % #Hmem |
---|
| 1337 | cut (mem block b' writeable ∧ b' ≠ b) |
---|
| 1338 | [ elim writeable in Hmem; |
---|
| 1339 | [ 1: normalize @False_ind |
---|
| 1340 | | 2: #hd #tl #Hind whd in match (filter ???); >eqb_to_eq_block |
---|
| 1341 | @(eq_block_elim … hd b) normalize in match (notb ?); normalize nodelta |
---|
| 1342 | [ 1: #Heq #H whd in match (meml ???); destruct |
---|
| 1343 | elim (Hind H) #Hmem #Hneq @conj try assumption %2 assumption |
---|
| 1344 | | 2: #Hneq whd in match (meml ???) in ⊢ (% → %); * |
---|
| 1345 | [ 1: #H @conj [ 1: %1 @H | 2: destruct @Hneq ] |
---|
| 1346 | | 2: #H elim (Hind H) #Hmem #Hneq' @conj try assumption %2 assumption ] |
---|
| 1347 | ] ] ] * #Hmem' #Hblocks_neq |
---|
| 1348 | lapply (me_not_writeable … Hext … Hnonempty) * #H @H assumption |
---|
| 1349 | ] qed. |
---|
| 1350 | |
---|
| 1351 | |
---|
| 1352 | lemma disjoint_extension_nil_eq_set : |
---|
| 1353 | ∀env1,env2. |
---|
| 1354 | disjoint_extension env1 env2 [ ] → |
---|
| 1355 | lset_eq ? (blocks_of_env env1) (blocks_of_env env2). |
---|
| 1356 | #env1 #env whd in ⊢ (% → ?); * * #_ #_ #H normalize in H; |
---|
| 1357 | @environment_eq_blocks_eq whd @conj |
---|
| 1358 | #id #res >(H id) // |
---|
| 1359 | qed. |
---|
| 1360 | |
---|
| 1361 | lemma free_list_equivalent_sets : |
---|
| 1362 | ∀m,set1,set2. |
---|
| 1363 | lset_eq ? set1 set2 → |
---|
| 1364 | memory_eq (free_list m set1) (free_list m set2). |
---|
| 1365 | #m #set1 #set2 #Heq whd in match (free_list ??) in ⊢ (?%%); |
---|
| 1366 | @(lset_eq_fold block_DeqSet mem memory_eq … Heq) |
---|
| 1367 | [ 1: @reflexive_memory_eq |
---|
| 1368 | | 2: @transitive_memory_eq |
---|
| 1369 | | 3: @symmetric_memory_eq |
---|
| 1370 | | 4: #x #acc1 #acc2 |
---|
| 1371 | whd in match (free ??) in ⊢ (? → (?%%)); |
---|
| 1372 | whd in match (memory_eq ??) in ⊢ (% → %); * |
---|
| 1373 | #Hnextblock_eq #Hcontents_eq @conj try assumption |
---|
| 1374 | #b normalize >Hcontents_eq @refl |
---|
| 1375 | | 5: #x1 #x2 #acc normalize @conj try @refl |
---|
| 1376 | * * #id normalize nodelta cases (block_region x1) |
---|
| 1377 | cases (block_region x2) normalize nodelta |
---|
| 1378 | @(eqZb_elim id (block_id x1)) #Hx1 normalize nodelta |
---|
| 1379 | @(eqZb_elim id (block_id x2)) #Hx2 normalize nodelta try @refl |
---|
| 1380 | | 6: * #r #i * #contents #nextblock #Hpos @conj |
---|
| 1381 | [ 1: @refl |
---|
| 1382 | | 2: #b normalize cases (block_region b) normalize |
---|
| 1383 | cases r normalize cases (eqZb (block_id b) i) |
---|
| 1384 | normalize @refl |
---|
| 1385 | ] |
---|
[2332] | 1386 | ] qed. |
---|
[2227] | 1387 | |
---|
[2387] | 1388 | lemma foldr_identity : ∀A:Type[0]. ∀l:list A. foldr A ? (λx:A.λl0.x::l0) [] l = l. |
---|
| 1389 | #A #l elim l // |
---|
| 1390 | #hd #tl #Hind whd in match (foldr ?????); >Hind @refl |
---|
[2227] | 1391 | qed. |
---|
| 1392 | |
---|
[2448] | 1393 | lemma mem_not_mem_diff_aux : |
---|
| 1394 | ∀s1,s2,s3,hd. |
---|
| 1395 | mem ? hd s1 → |
---|
| 1396 | ¬(mem ? hd s2) → |
---|
| 1397 | mem block hd (lset_difference ? s1 (s2@(filter block_DeqSet (λx:block_DeqSet.¬x==hd) s3))). |
---|
| 1398 | #s1 #s2 #s3 #hd #Hmem #Hnotmem lapply Hmem lapply s1 -s1 |
---|
| 1399 | elim s3 |
---|
| 1400 | [ 1: #s1 >append_nil elim s1 try // |
---|
| 1401 | #hd' #tl' #Hind * |
---|
| 1402 | [ 1: #Heq >lset_difference_unfold |
---|
| 1403 | @(match hd'∈s2 return λx. (hd'∈s2 = x) → ? with |
---|
| 1404 | [ true ⇒ λH. ? |
---|
| 1405 | | false ⇒ λH. ? |
---|
| 1406 | ] (refl ? (hd'∈s2))) normalize nodelta |
---|
| 1407 | [ 1: lapply (memb_to_mem … H) #Hmem elim Hnotmem #H' destruct |
---|
| 1408 | @(False_ind … (H' Hmem)) |
---|
| 1409 | | 2: whd %1 assumption ] |
---|
| 1410 | | 2: #Hmem >lset_difference_unfold |
---|
| 1411 | @(match hd'∈s2 return λx. (hd'∈s2 = x) → ? with |
---|
| 1412 | [ true ⇒ λH. ? |
---|
| 1413 | | false ⇒ λH. ? |
---|
| 1414 | ] (refl ? (hd'∈s2))) normalize nodelta |
---|
| 1415 | [ 1: @Hind @Hmem |
---|
| 1416 | | 2: %2 @Hind @Hmem ] ] |
---|
| 1417 | | 2: #hd' #tl' #H #s1 #Hmem >filter_cons_unfold >eqb_to_eq_block |
---|
| 1418 | @(eq_block_elim … hd' hd) |
---|
| 1419 | [ 1: >notb_true normalize nodelta #Heq @H @Hmem |
---|
| 1420 | | 2: #Hneq >notb_false normalize nodelta |
---|
| 1421 | >lset_difference_permute >(cons_to_append … hd') |
---|
| 1422 | >associative_append >lset_difference_unfold2 >nil_append |
---|
| 1423 | >lset_difference_permute @H |
---|
| 1424 | elim s1 in Hmem; try // |
---|
| 1425 | #hd'' #tl'' #Hind * |
---|
| 1426 | [ 1: #Heq destruct whd in match (lset_remove ???); |
---|
| 1427 | >eqb_to_eq_block >(neq_block_eq_block_false … (sym_neq … Hneq)) |
---|
| 1428 | >notb_false normalize nodelta %1 @refl |
---|
| 1429 | | 2: #Hmem whd in match (lset_remove ???); |
---|
| 1430 | cases (¬(hd''==hd')) normalize nodelta |
---|
| 1431 | [ 1: %2 @Hind @Hmem |
---|
| 1432 | | 2: @Hind @Hmem ] ] ] |
---|
| 1433 | ] qed. |
---|
| 1434 | |
---|
[2387] | 1435 | (* freeing equivalent sets of blocks on memory extensions yields memory extensions *) |
---|
| 1436 | lemma free_equivalent_sets : |
---|
| 1437 | ∀m1,m2,writeable,set1,set2. |
---|
| 1438 | lset_eq ? set1 set2 → |
---|
| 1439 | sr_memext m1 m2 writeable → |
---|
| 1440 | sr_memext (free_list m1 set1) (free_list m2 set2) (lset_difference ? writeable set1). |
---|
| 1441 | #m1 #m2 #writeable #set1 #set2 #Heq #Hext |
---|
| 1442 | lapply (free_list_equivalent_sets m2 … (symmetric_lset_eq … Heq)) |
---|
| 1443 | #Heq |
---|
| 1444 | lapply (memory_eq_to_mem_ext … (symmetric_memory_eq … Heq)) #Hext' |
---|
| 1445 | lapply (memory_ext_transitive (free_list m1 set1) (free_list m2 set1) (free_list m2 set2) (filter block_eq (λwb:block_eq.¬wb∈set1) writeable) [ ] ? Hext') |
---|
| 1446 | [ 2: >append_nil #H @H ] |
---|
| 1447 | elim set1 |
---|
| 1448 | [ 1: whd in match (free_list ??); whd in match (free_list ??); |
---|
| 1449 | normalize >foldr_identity @Hext |
---|
| 1450 | | 2: #hd #tl #Hind >free_list_cons >free_list_cons |
---|
| 1451 | lapply (free_memory_ext … hd … Hind) |
---|
| 1452 | cut ((lset_remove block_eq (filter block_eq (λwb:block_eq.¬wb∈tl) writeable) hd) = |
---|
| 1453 | (filter block_eq (λwb:block_eq.¬wb∈hd::tl) writeable)) |
---|
| 1454 | [ whd in match (lset_remove ???); elim writeable // |
---|
| 1455 | #hd' #tl' #Hind_cut >filter_cons_unfold >filter_cons_unfold |
---|
| 1456 | whd in match (memb ???) in ⊢ (???%); >eqb_to_eq_block |
---|
| 1457 | (* elim (eqb_true block_DeqSet hd' hd)*) |
---|
| 1458 | @(eq_block_elim … hd' hd) normalize nodelta |
---|
| 1459 | [ 1: #Heq |
---|
| 1460 | cases (¬hd'∈tl) normalize nodelta |
---|
| 1461 | [ 1: whd in match (foldr ?????); >Heq >eqb_to_eq_block >eq_block_b_b normalize in match (notb ?); |
---|
| 1462 | normalize nodelta |
---|
| 1463 | lapply Hind_cut destruct #H @H |
---|
| 1464 | | 2: lapply Hind_cut destruct #H @H ] |
---|
| 1465 | | 2: #Hneq cases (¬hd'∈tl) normalize nodelta try assumption |
---|
| 1466 | whd in match (foldr ?????); >eqb_to_eq_block |
---|
| 1467 | >(neq_block_eq_block_false … Hneq) |
---|
| 1468 | normalize in match (notb ?); normalize nodelta >Hind_cut @refl |
---|
| 1469 | ] |
---|
| 1470 | ] |
---|
| 1471 | #Heq >Heq #H @H |
---|
| 1472 | ] qed. |
---|
[2227] | 1473 | |
---|
[2387] | 1474 | (* Remove a writeable block. *) |
---|
| 1475 | lemma memory_ext_weaken : |
---|
| 1476 | ∀m1,m2,hd,writeable. |
---|
| 1477 | sr_memext m1 m2 (hd :: writeable) → |
---|
| 1478 | sr_memext m1 m2 writeable. |
---|
[2438] | 1479 | #m1 #m2 #hd #writeable * |
---|
| 1480 | #Hnonempty #Hwriteable_valid #Hnot_writeable % |
---|
[2387] | 1481 | try assumption |
---|
| 1482 | [ 1: #b #Hmem @Hwriteable_valid whd %2 assumption |
---|
| 1483 | | 2: #b #Hnonempty % #Hmem elim (Hnot_writeable … Hnonempty) #H @H whd %2 @Hmem |
---|
| 1484 | ] qed. |
---|
[2227] | 1485 | |
---|
[2387] | 1486 | (* Perform a "rewrite" using lset_eq on the writeable blocks *) |
---|
| 1487 | lemma memory_ext_writeable_eq : |
---|
| 1488 | ∀m1,m2,wr1,wr2. |
---|
| 1489 | sr_memext m1 m2 wr1 → |
---|
| 1490 | lset_eq ? wr1 wr2 → |
---|
| 1491 | sr_memext m1 m2 wr2. |
---|
| 1492 | #m1 #m2 #wr1 #wr2 #Hext #Hset_eq % |
---|
| 1493 | [ 1: @(me_nonempty … Hext) |
---|
| 1494 | | 2: #b #Hmem lapply (lset_eq_mem … (symmetric_lset_eq … Hset_eq) … Hmem) |
---|
| 1495 | @(me_writeable_valid … Hext) |
---|
| 1496 | | 3: #b #Hnonempty % #Hmem |
---|
| 1497 | lapply (lset_eq_mem … (symmetric_lset_eq … Hset_eq) … Hmem) #Hmem' |
---|
| 1498 | lapply (me_not_writeable … Hext … Hnonempty) * #H @H assumption |
---|
[2438] | 1499 | ] qed. |
---|
[2227] | 1500 | |
---|
[2387] | 1501 | |
---|
[2448] | 1502 | |
---|
[2438] | 1503 | lemma memory_eq_to_memory_ext_pre : |
---|
| 1504 | ∀m1,m1',m2,writeable. |
---|
| 1505 | memory_eq m1 m1' → |
---|
| 1506 | sr_memext m1' m2 writeable → |
---|
| 1507 | sr_memext m1 m2 writeable. |
---|
| 1508 | #m1 #m1' #m2 #writeable #Heq #Hext |
---|
| 1509 | lapply (memory_eq_to_mem_ext … Heq) #Hext' |
---|
| 1510 | @(memory_ext_transitive … Hext' Hext) |
---|
| 1511 | qed. |
---|
| 1512 | |
---|
| 1513 | lemma memory_eq_to_memory_ext_post : |
---|
| 1514 | ∀m1,m2,m2',writeable. |
---|
| 1515 | memory_eq m2' m2 → |
---|
| 1516 | sr_memext m1 m2' writeable → |
---|
| 1517 | sr_memext m1 m2 writeable. |
---|
| 1518 | #m1 #m2 #m2' #writeable #Heq #Hext |
---|
| 1519 | lapply (memory_eq_to_mem_ext … Heq) #Hext' |
---|
| 1520 | lapply (memory_ext_transitive … Hext Hext') >append_nil #H @H |
---|
| 1521 | qed. |
---|
| 1522 | |
---|
| 1523 | |
---|
[2387] | 1524 | lemma memext_free_extended_environment : |
---|
| 1525 | ∀m1,m2,writeable. |
---|
| 1526 | sr_memext m1 m2 writeable → |
---|
| 1527 | ∀env,env_ext,vars. |
---|
| 1528 | disjoint_extension env env_ext vars → |
---|
| 1529 | lset_inclusion ? (lset_difference ? (blocks_of_env env_ext) (blocks_of_env env)) writeable → |
---|
| 1530 | sr_memext |
---|
| 1531 | (free_list m1 (blocks_of_env env)) |
---|
| 1532 | (free_list m2 (blocks_of_env env_ext)) |
---|
| 1533 | (lset_difference ? writeable (blocks_of_env env_ext)). |
---|
| 1534 | #m1 #m2 #writeable #Hext #env #env_ext #vars #Hdisjoint #Hext_in_writeable |
---|
| 1535 | (* Disjoint extension induces environment "inclusion", i.e. simulation *) |
---|
| 1536 | lapply (disjoint_extension_to_inclusion … Hdisjoint) #Hincl |
---|
| 1537 | (* Environment inclusion entails set inclusion on the mapped blocks *) |
---|
| 1538 | lapply (environment_sim_blocks_inclusion … Hincl) #Hblocks_incl |
---|
| 1539 | (* This set inclusion can be decomposed on a common part and an extended part. *) |
---|
| 1540 | lapply (lset_inclusion_difference ??? Hblocks_incl) |
---|
| 1541 | * #extended_part * * #Hset_eq #Henv_disjoint_ext #Hextended_eq |
---|
| 1542 | lapply (lset_difference_lset_eq … writeable … Hset_eq) #HeqA |
---|
| 1543 | cut (lset_inclusion ? extended_part writeable) |
---|
| 1544 | [ 1: cases Hextended_eq #HinclA #_ @(transitive_lset_inclusion … HinclA … Hext_in_writeable) ] |
---|
| 1545 | -Hext_in_writeable #Hext_in_writeable |
---|
| 1546 | @(memory_ext_writeable_eq ????? (symmetric_lset_eq … HeqA)) |
---|
| 1547 | lapply (free_list_equivalent_sets m2 ?? Hset_eq) #Hmem_eq |
---|
| 1548 | @(memory_eq_to_memory_ext_post … (symmetric_memory_eq … Hmem_eq)) |
---|
| 1549 | (* Add extended ⊆ (lset_difference block_eq writeable (blocks_of_env env @ tl)) in Hind *) |
---|
| 1550 | cut (∀x. mem ? x extended_part → ¬ (mem ? x (blocks_of_env env))) |
---|
| 1551 | [ 1: cases Hextended_eq #Hincl_ext #_ @(lset_not_mem_difference … Hincl_ext) ] |
---|
| 1552 | lapply (proj2 … Hset_eq) lapply Hext_in_writeable |
---|
| 1553 | @(WF_rect ????? (filtered_list_wf block_DeqSet extended_part)) |
---|
| 1554 | * |
---|
| 1555 | [ 1: #_ #_ #_ #_ #_ >append_nil |
---|
| 1556 | @(free_equivalent_sets ???? (blocks_of_env env) (reflexive_lset_eq ??) Hext) |
---|
| 1557 | | 2: #hd #tl #Hwf_step #Hind_wf #Hext_in_writeable #Hset_incl #Hin_ext_not_in_env |
---|
| 1558 | cut (lset_eq ? (blocks_of_env env@hd::tl) (hd::(blocks_of_env env@tl))) |
---|
| 1559 | [ 1: >cons_to_append >cons_to_append in ⊢ (???%); |
---|
| 1560 | @lset_eq_concrete_to_lset_eq // ] |
---|
| 1561 | #Hpermute |
---|
| 1562 | lapply (free_list_equivalent_sets m2 ?? Hpermute) #Hmem_eq2 |
---|
| 1563 | @(memory_eq_to_memory_ext_post … (symmetric_memory_eq … Hmem_eq2)) |
---|
| 1564 | >free_list_cons |
---|
| 1565 | lapply (lset_difference_lset_eq … writeable … Hpermute) #HeqB |
---|
| 1566 | @(memory_ext_writeable_eq ????? (symmetric_lset_eq … HeqB)) |
---|
| 1567 | >lset_difference_unfold2 |
---|
| 1568 | lapply (lset_difference_lset_remove_commute ? hd writeable (blocks_of_env env@tl)) |
---|
| 1569 | #Heq_commute >Heq_commute |
---|
| 1570 | (* lapply (memory_ext_writeable_eq ????? (symmetric_lset_eq … Heq_commute)) *) |
---|
| 1571 | lapply (Hind_wf (filter … (λx.¬(x==hd)) tl) ????) |
---|
| 1572 | [ 2: @(transitive_lset_inclusion … Hset_incl) |
---|
| 1573 | @lset_inclusion_concat_monotonic |
---|
| 1574 | @cons_preserves_inclusion |
---|
| 1575 | @lset_inclusion_filter_self |
---|
| 1576 | | 3: @(transitive_lset_inclusion … Hext_in_writeable) |
---|
| 1577 | @cons_preserves_inclusion |
---|
| 1578 | @lset_inclusion_filter_self |
---|
| 1579 | | 4: whd whd in ⊢ (???%); |
---|
| 1580 | lapply (eqb_true ? hd hd) * #_ #H >(H (refl ??)) normalize in match (notb ?); |
---|
| 1581 | normalize nodelta @refl |
---|
| 1582 | | 1: #x #H @Hin_ext_not_in_env %2 elim tl in H; // |
---|
| 1583 | #hd' #tl' #Hind >filter_cons_unfold >eqb_to_eq_block @(eq_block_elim … hd' hd) |
---|
| 1584 | >notb_true >notb_false normalize nodelta |
---|
| 1585 | [ 1: #Heq >Heq #H %2 @Hind @H |
---|
| 1586 | | 2: #Hneq * |
---|
| 1587 | [ 1: #Heq destruct %1 @refl |
---|
| 1588 | | 2: #H %2 @Hind @H ] ] |
---|
| 1589 | ] |
---|
| 1590 | #Hext_ind |
---|
| 1591 | lapply (Hin_ext_not_in_env … hd (or_introl … (refl ??))) |
---|
| 1592 | #Hnot_in_env |
---|
| 1593 | lapply (memext_free_extended_conservation … Hext_ind hd ?) |
---|
| 1594 | [ 1: @mem_not_mem_diff_aux try assumption elim Hext_in_writeable #H #_ @H ] |
---|
| 1595 | -Hext_ind #Hext_ind |
---|
| 1596 | cut (memory_eq (free (free_list m2 (blocks_of_env env@filter block_DeqSet (λx:block_DeqSet.¬x==hd) tl)) hd) |
---|
| 1597 | (free (free_list m2 (blocks_of_env env@tl)) hd)) |
---|
| 1598 | [ 1: <free_list_cons <free_list_cons |
---|
| 1599 | @free_list_equivalent_sets @lset_eq_concrete_to_lset_eq |
---|
| 1600 | >cons_to_append >cons_to_append in ⊢ (???%); |
---|
| 1601 | @(transitive_lset_eq_concrete … (switch_lset_eq_concrete ????)) |
---|
| 1602 | @symmetric_lset_eq_concrete |
---|
| 1603 | @(transitive_lset_eq_concrete ????? (switch_lset_eq_concrete ????)) |
---|
| 1604 | @lset_eq_to_lset_eq_concrete |
---|
| 1605 | elim (blocks_of_env env) |
---|
| 1606 | [ 1: @symmetric_lset_eq @lset_eq_filter |
---|
| 1607 | | 2: #hd0 #tl0 #Hind >cons_to_append |
---|
| 1608 | >associative_append in ⊢ (??%%); |
---|
| 1609 | >associative_append in ⊢ (??%%); |
---|
| 1610 | @cons_monotonic_eq @Hind ] ] |
---|
| 1611 | #Hmem_eq3 @(memory_eq_to_memory_ext_post … Hmem_eq3) |
---|
| 1612 | @(memory_ext_writeable_eq … Hext_ind) |
---|
| 1613 | <lset_difference_lset_remove_commute <lset_difference_lset_remove_commute |
---|
| 1614 | <lset_difference_unfold2 <lset_difference_unfold2 |
---|
| 1615 | @lset_difference_lset_eq |
---|
| 1616 | (* Note: exactly identical to the proof in the cut. *) |
---|
| 1617 | @lset_eq_concrete_to_lset_eq |
---|
| 1618 | >cons_to_append >cons_to_append in ⊢ (???%); |
---|
| 1619 | @(transitive_lset_eq_concrete … (switch_lset_eq_concrete ????)) |
---|
| 1620 | @symmetric_lset_eq_concrete |
---|
| 1621 | @(transitive_lset_eq_concrete ????? (switch_lset_eq_concrete ????)) |
---|
| 1622 | @lset_eq_to_lset_eq_concrete |
---|
| 1623 | elim (blocks_of_env env) |
---|
| 1624 | [ 1: @symmetric_lset_eq @lset_eq_filter |
---|
| 1625 | | 2: #hd0 #tl0 #Hind >cons_to_append |
---|
| 1626 | >associative_append in ⊢ (??%%); |
---|
| 1627 | >associative_append in ⊢ (??%%); |
---|
| 1628 | @cons_monotonic_eq @Hind ] |
---|
| 1629 | ] qed. |
---|
| 1630 | |
---|
[2438] | 1631 | (* --------------------------------------------------------------------------- *) |
---|
| 1632 | (* Some lemmas allowing to reason on writes to extended memories. *) |
---|
[2387] | 1633 | |
---|
[2438] | 1634 | (* Writing in the extended part of the memory preserves the extension (that's the point) *) |
---|
| 1635 | lemma bestorev_writeable_memory_ext : |
---|
| 1636 | ∀m1,m2,writeable. |
---|
| 1637 | ∀Hext:sr_memext m1 m2 writeable. |
---|
| 1638 | ∀wb,wo,v. meml ? wb writeable → |
---|
| 1639 | ∀m2'.bestorev m2 (mk_pointer wb wo) v = Some ? m2' → |
---|
| 1640 | sr_memext m1 m2' writeable. |
---|
| 1641 | #m1 * #contents2 #nextblock2 #Hpos2 #writeable #Hext #wb #wo #v #Hmem #m2' |
---|
| 1642 | whd in ⊢ ((??%?) → ?); |
---|
| 1643 | lapply (me_writeable_valid … Hext ? Hmem) * whd in ⊢ (% → ?); #Hlt |
---|
| 1644 | >(Zlt_to_Zltb_true … Hlt) normalize nodelta #Hnonempty2 #H |
---|
| 1645 | lapply (if_opt_inversion ???? H) -H * #Hzltb |
---|
| 1646 | lapply (andb_inversion … Hzltb) * #Hleb #Hltb -Hzltb |
---|
| 1647 | #Heq destruct % |
---|
| 1648 | [ 1: #b #Hnonempty1 |
---|
| 1649 | lapply (me_nonempty … Hext b Hnonempty1) * * #Hvalid_b #Hnonempty_b |
---|
| 1650 | #Heq @conj |
---|
| 1651 | [ 1: % whd whd in Hvalid_b; try @Hvalid_b |
---|
| 1652 | normalize cases (block_region b) normalize nodelta |
---|
| 1653 | cases (block_region wb) normalize nodelta try // |
---|
| 1654 | @(eqZb_elim … (block_id b) (block_id wb)) normalize nodelta |
---|
| 1655 | try // |
---|
| 1656 | | 2: whd in ⊢ (??%%); |
---|
| 1657 | @(eq_block_elim … b wb) normalize nodelta // #Heq_b_wb |
---|
| 1658 | lapply (me_not_writeable … Hext b Hnonempty1) destruct (Heq_b_wb) |
---|
| 1659 | * #H @(False_ind … (H Hmem)) ] |
---|
| 1660 | | 2: #b #Hmem_writeable |
---|
| 1661 | lapply (me_writeable_valid … Hext … Hmem_writeable) #H % |
---|
| 1662 | [ 1: normalize cases H // |
---|
| 1663 | | 2: cases H normalize #Hb_lt #Hb_nonempty2 |
---|
| 1664 | cases (block_region b) |
---|
| 1665 | cases (block_region wb) normalize nodelta |
---|
| 1666 | // |
---|
| 1667 | @(eqZb_elim … (block_id b) (block_id wb)) normalize nodelta |
---|
| 1668 | // ] |
---|
| 1669 | | 3: #b #Hnonempty |
---|
| 1670 | lapply (me_not_writeable … Hext … Hnonempty) // |
---|
| 1671 | ] qed. |
---|
| 1672 | |
---|
| 1673 | (* If we manage to write in a block, then it is nonempty *) |
---|
| 1674 | lemma bestorev_success_nonempty : |
---|
| 1675 | ∀m,wb,wo,v,m'. |
---|
| 1676 | bestorev m (mk_pointer wb wo) v = Some ? m' → |
---|
| 1677 | nonempty_block m wb. |
---|
| 1678 | #m #wb #wo #v #m' normalize #Hstore |
---|
| 1679 | cases (if_opt_inversion ???? Hstore) -Hstore #block_valid1 #H |
---|
| 1680 | cases (if_opt_inversion ???? H) -H #nonempty #H % |
---|
| 1681 | [ 1: whd @Zltb_true_to_Zlt assumption |
---|
| 1682 | | 2: generalize in match (Z_of_unsigned_bitvector 16 (offv wo)) in nonempty; #z #H' |
---|
| 1683 | cut (Zleb (low (blocks m wb)) z = true) |
---|
| 1684 | [ 1: lapply H' cases (Zleb (low (blocks m wb)) z) // normalize #H @H ] |
---|
| 1685 | #Hleb >Hleb in H'; normalize nodelta #Hlt |
---|
| 1686 | lapply (Zleb_true_to_Zle … Hleb) lapply (Zltb_true_to_Zlt … Hlt) |
---|
| 1687 | /2 by Zle_to_Zlt_to_Zlt/ |
---|
| 1688 | ] qed. |
---|
| 1689 | |
---|
| 1690 | (* If we manage to write in a block, it is still non-empty after the write *) |
---|
| 1691 | lemma bestorev_success_nonempty2 : |
---|
| 1692 | ∀m,wb,wo,v,m'. |
---|
| 1693 | bestorev m (mk_pointer wb wo) v = Some ? m' → |
---|
| 1694 | nonempty_block m' wb. |
---|
| 1695 | #m #wb #wo #v #m' normalize #Hstore |
---|
| 1696 | cases (if_opt_inversion ???? Hstore) -Hstore #block_valid1 #H |
---|
| 1697 | cases (if_opt_inversion ???? H) -H #nonempty #H % |
---|
| 1698 | [ 1: whd destruct @Zltb_true_to_Zlt assumption |
---|
| 1699 | | 2: generalize in match (Z_of_unsigned_bitvector 16 (offv wo)) in nonempty; #z #H' |
---|
| 1700 | cut (Zleb (low (blocks m wb)) z = true) |
---|
| 1701 | [ 1: lapply H' cases (Zleb (low (blocks m wb)) z) // normalize #H @H ] |
---|
| 1702 | #Hleb >Hleb in H'; normalize nodelta #Hlt |
---|
| 1703 | lapply (Zleb_true_to_Zle … Hleb) lapply (Zltb_true_to_Zlt … Hlt) |
---|
| 1704 | destruct cases (block_region wb) normalize >eqZb_z_z normalize |
---|
| 1705 | /2 by Zle_to_Zlt_to_Zlt/ |
---|
| 1706 | ] qed. |
---|
| 1707 | |
---|
| 1708 | (* A nonempty block stays nonempty after a write. *) |
---|
| 1709 | lemma nonempty_block_update_ok : |
---|
| 1710 | ∀m,b,wb,offset,v. |
---|
| 1711 | nonempty_block m b → |
---|
| 1712 | nonempty_block |
---|
| 1713 | (mk_mem |
---|
| 1714 | (update_block ? wb |
---|
| 1715 | (mk_block_contents (low (blocks m wb)) (high (blocks m wb)) |
---|
| 1716 | (update beval offset v (contents (blocks m wb)))) (blocks m)) |
---|
| 1717 | (nextblock m) (nextblock_pos m)) b. |
---|
| 1718 | #m #b #wb #offset #v * #Hvalid #Hnonempty % // |
---|
| 1719 | cases b in Hvalid Hnonempty; #br #bid cases wb #wbr #wbid normalize |
---|
| 1720 | cases br normalize nodelta cases wbr normalize nodelta // |
---|
| 1721 | @(eqZb_elim … bid wbid) // #Heq #Hlt normalize // |
---|
| 1722 | qed. |
---|
| 1723 | |
---|
| 1724 | lemma nonempty_block_update_ok2 : |
---|
| 1725 | ∀m,b,wb,offset,v. |
---|
| 1726 | nonempty_block |
---|
| 1727 | (mk_mem |
---|
| 1728 | (update_block ? wb |
---|
| 1729 | (mk_block_contents (low (blocks m wb)) (high (blocks m wb)) |
---|
| 1730 | (update beval offset v (contents (blocks m wb)))) (blocks m)) |
---|
| 1731 | (nextblock m) (nextblock_pos m)) b → |
---|
| 1732 | nonempty_block m b. |
---|
| 1733 | #m #b #wb #offset #v * #Hvalid #Hnonempty % // |
---|
| 1734 | cases b in Hvalid Hnonempty; #br #bid cases wb #wbr #wbid normalize |
---|
| 1735 | cases br normalize nodelta cases wbr normalize nodelta // |
---|
| 1736 | @(eqZb_elim … bid wbid) // #Heq #Hlt normalize // |
---|
| 1737 | qed. |
---|
| 1738 | |
---|
| 1739 | (* Writing in the non-extended part of the memory preserves the extension as long |
---|
| 1740 | * as it's done identically in both memories. *) |
---|
| 1741 | lemma bestorev_not_writeable_memory_ext : |
---|
| 1742 | ∀m1,m2,writeable. |
---|
| 1743 | ∀Hext:sr_memext m1 m2 writeable. |
---|
| 1744 | ∀wb,wo,v. |
---|
| 1745 | ∀m1'. bestorev m1 (mk_pointer wb wo) v = Some ? m1' → |
---|
| 1746 | ∃m2'. bestorev m2 (mk_pointer wb wo) v = Some ? m2' ∧ |
---|
| 1747 | sr_memext m1' m2' writeable. |
---|
| 1748 | #m1 #m2 #writeable #Hext #wb #wo #v #m1' #Hstore1 |
---|
| 1749 | lapply (bestorev_success_nonempty … Hstore1) #Hwb_nonempty |
---|
| 1750 | cases (me_nonempty … Hext … Hwb_nonempty) #Hwb_nonempty2 #Hblocks_eq |
---|
| 1751 | cut (∃m2'. bestorev m2 (mk_pointer wb wo) v=Some mem m2') |
---|
| 1752 | [ cases Hwb_nonempty2 #Hwb_valid #Hnonempty normalize |
---|
| 1753 | normalize in Hwb_valid; >(Zlt_to_Zltb_true … Hwb_valid) normalize nodelta |
---|
| 1754 | whd in Hstore1:(??%%); normalize |
---|
| 1755 | cases (if_opt_inversion ???? Hstore1) -Hstore1 #block_valid1 #H |
---|
| 1756 | cases (if_opt_inversion ???? H) #Hin_bounds1 #Hm1' -H |
---|
| 1757 | cases (andb_inversion … Hin_bounds1) #Hleb1 #Hltb1 -Hin_bounds1 |
---|
| 1758 | >Hblocks_eq in Hleb1 Hltb1 ⊢ %; #Hleb1 #Hltb1 >Hleb1 >Hltb1 |
---|
| 1759 | normalize nodelta /2 by ex_intro/ ] |
---|
| 1760 | * #m2' #Hstore2 %{m2'} @conj try assumption |
---|
| 1761 | whd in Hstore1:(??%%); |
---|
| 1762 | whd in Hstore2:(??%%); |
---|
| 1763 | cases (if_opt_inversion ???? Hstore1) -Hstore1 #block_valid1 #H |
---|
| 1764 | cases (if_opt_inversion ???? H) #Hin_bounds1 #Hm1' -H |
---|
| 1765 | cases (if_opt_inversion ???? Hstore2) -Hstore2 #block_valid2 #H |
---|
| 1766 | cases (if_opt_inversion ???? H) #Hin_bounds2 #Hm2' -H |
---|
| 1767 | cases (andb_inversion … Hin_bounds1) #Hleb1 #Hltb1 -Hin_bounds1 |
---|
| 1768 | cases (andb_inversion … Hin_bounds2) #Hleb2 #Hltb2 -Hin_bounds2 |
---|
| 1769 | cut (valid_pointer m1 (mk_pointer wb wo)) |
---|
| 1770 | [ 1: normalize >block_valid1 normalize nodelta >Hleb1 normalize nodelta |
---|
| 1771 | >Hltb1 @I ] |
---|
| 1772 | #Hvalid |
---|
| 1773 | lapply (me_not_writeable_ptr … Hext … Hvalid) #Hnot_in_writeable |
---|
| 1774 | destruct % |
---|
| 1775 | [ 1: #b #Hnonempty lapply (me_nonempty … Hext … (nonempty_block_update_ok2 … Hnonempty)) * #HA #HB |
---|
| 1776 | @conj |
---|
| 1777 | [ 1: @nonempty_block_update_ok // |
---|
| 1778 | | 2: normalize cases b in HB; #br #bid cases wb #wbr #wbid |
---|
| 1779 | cases br cases wbr normalize nodelta |
---|
| 1780 | @(eqZb_elim … bid wbid) normalize nodelta // |
---|
| 1781 | #Hid_eq >Hid_eq #Hblock_eq >Hblock_eq @refl ] |
---|
| 1782 | | 2: #b #Hmem lapply (me_writeable_valid … Hext … Hmem) @nonempty_block_update_ok |
---|
| 1783 | | 3: #b #Hnonempty lapply (nonempty_block_update_ok2 … Hnonempty) |
---|
| 1784 | @(me_not_writeable … Hext) |
---|
| 1785 | ] qed. |
---|
| 1786 | |
---|
| 1787 | (* If we successfuly store something in the first memory, then we can store it in the |
---|
| 1788 | * second one and the memory extension is preserved. *) |
---|
| 1789 | lemma memext_store_value_of_type : |
---|
| 1790 | ∀m, m_ext, m', writeable, ty, loc, off, v. |
---|
| 1791 | sr_memext m m_ext writeable → |
---|
| 1792 | store_value_of_type ty m loc off v = Some ? m' → |
---|
| 1793 | ∃m_ext'. store_value_of_type ty m_ext loc off v = Some ? m_ext' ∧ |
---|
| 1794 | sr_memext m' m_ext' writeable. |
---|
| 1795 | #m #m_ext #m' #writeable #ty #loc #off #v #Hext |
---|
| 1796 | (* case analysis on access mode of [ty] *) |
---|
| 1797 | cases ty |
---|
[2468] | 1798 | [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain |
---|
| 1799 | | #structname #fieldspec | #unionname #fieldspec | #id ] |
---|
[2438] | 1800 | whd in ⊢ ((??%?) → (?%?)); |
---|
[2468] | 1801 | [ 1,4,5,6,7: #Habsurd destruct ] |
---|
[2438] | 1802 | whd in ⊢ (? → (??(λ_.?(??%?)?))); |
---|
| 1803 | lapply loc lapply off lapply Hext lapply m_ext lapply m lapply m' -loc -off -Hext -m_ext -m -m' |
---|
| 1804 | elim (fe_to_be_values ??) |
---|
[2468] | 1805 | [ 1,3,5: #m' #m #m_ext #Hext #off #loc normalize in ⊢ (% → ?); #Heq destruct (Heq) %{m_ext} @conj normalize // |
---|
| 1806 | | 2,4,6: #hd #tl #Hind #m' #m #m_ext #Hext #off #loc whd in ⊢ ((??%?) → ?); #H |
---|
| 1807 | cases (some_inversion ????? H) #m'' * #Hstore_eq #Hstoren_eq |
---|
| 1808 | lapply (bestorev_not_writeable_memory_ext … Hext … Hstore_eq) |
---|
| 1809 | * #m_ext'' * #Hstore_eq2 #Hext2 |
---|
| 1810 | lapply (Hind … Hext2 … Hstoren_eq) -Hind * #m_ext' * |
---|
| 1811 | #Hstoren' #Hext3 |
---|
| 1812 | %{m_ext'} @conj try assumption |
---|
| 1813 | whd in ⊢ (??%%); >Hstore_eq2 normalize nodelta |
---|
| 1814 | @Hstoren' |
---|
[2438] | 1815 | ] qed. |
---|
| 1816 | |
---|
| 1817 | lemma memext_store_value_of_type' : |
---|
| 1818 | ∀m, m_ext, m', writeable, ty, ptr, v. |
---|
| 1819 | sr_memext m m_ext writeable → |
---|
| 1820 | store_value_of_type' ty m ptr v = Some ? m' → |
---|
| 1821 | ∃m_ext'. store_value_of_type' ty m_ext ptr v = Some ? m_ext' ∧ |
---|
| 1822 | sr_memext m' m_ext' writeable. |
---|
| 1823 | #m #m_ext #m' #writeable #ty #p #v #Hext cases p #b #o |
---|
| 1824 | @memext_store_value_of_type @Hext qed. |
---|
| 1825 | |
---|
[2448] | 1826 | lemma memext_store_value_of_type_writeable : |
---|
| 1827 | ∀m1,m2,writeable. |
---|
| 1828 | ∀Hext:sr_memext m1 m2 writeable. |
---|
| 1829 | ∀wb. meml ? wb writeable → |
---|
| 1830 | ∀ty,off,v,m2'. store_value_of_type ty m2 wb off v = Some ? m2' → |
---|
| 1831 | sr_memext m1 m2' writeable. |
---|
| 1832 | #m1 #m2 #writeable #Hext #wb #Hmem |
---|
| 1833 | #ty #off #v #m2' |
---|
| 1834 | cases ty |
---|
[2468] | 1835 | [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain |
---|
| 1836 | | #structname #fieldspec | #unionname #fieldspec | #id ] |
---|
[2448] | 1837 | whd in ⊢ ((??%?) → ?); |
---|
[2468] | 1838 | [ 1,4,5,6,7: #Habsurd destruct ] |
---|
[2448] | 1839 | lapply Hext lapply m1 lapply m2 lapply m2' lapply off -Hext -m1 -m2 -m2' -off -ty |
---|
| 1840 | elim (fe_to_be_values ??) |
---|
[2468] | 1841 | [ 1,3,5: #o #m2' #m2 #m1 #Hext normalize #Heq destruct assumption |
---|
[2448] | 1842 | | *: #hd #tl #Hind #o #m2_end #m2 #m1 #Hext whd in match (storen ???); #Hbestorev |
---|
| 1843 | cases (some_inversion ????? Hbestorev) #m2' * #Hbestorev #Hstoren |
---|
| 1844 | lapply (bestorev_writeable_memory_ext … Hext … o hd Hmem … Hbestorev) #Hext' |
---|
| 1845 | @(Hind … Hstoren) // |
---|
[2468] | 1846 | ] qed. |
---|
[2448] | 1847 | |
---|
[2227] | 1848 | (* In proofs, [disjoint_extension] is not enough. When a variable lookup arises, if |
---|
| 1849 | * the variable is not in a local environment, then we search into the global one. |
---|
| 1850 | * A proper "extension" of a local environment should be such that the extension |
---|
| 1851 | * does not collide with a given global env. |
---|
| 1852 | * To see the details of why we need that, see [exec_lvalue'], Evar id case. |
---|
| 1853 | *) |
---|
| 1854 | definition ext_fresh_for_genv ≝ |
---|
| 1855 | λ(ext : list (ident × type)). λ(ge : genv). |
---|
| 1856 | ∀id. mem_assoc_env id ext = true → find_symbol … ge id = None ?. |
---|
| 1857 | |
---|
| 1858 | (* "generic" simulation relation on [res ?] *) |
---|
| 1859 | definition res_sim ≝ |
---|
| 1860 | λ(A : Type[0]). |
---|
| 1861 | λ(r1, r2 : res A). |
---|
[2332] | 1862 | ∀a. r1 = OK ? a → r2 = OK ? a. |
---|
[2227] | 1863 | |
---|
| 1864 | (* Specialisation of [res_sim] to match [exec_expr] *) |
---|
[2332] | 1865 | definition exec_expr_sim ≝ res_sim (val × trace). |
---|
[2227] | 1866 | |
---|
| 1867 | (* Specialisation of [res_sim] to match [exec_lvalue] *) |
---|
[2332] | 1868 | definition exec_lvalue_sim ≝ res_sim (block × offset × trace). |
---|
[2227] | 1869 | |
---|
| 1870 | lemma load_value_of_type_dec : ∀ty, m, b, o. load_value_of_type ty m b o = None ? ∨ ∃r. load_value_of_type ty m b o = Some ? r. |
---|
| 1871 | #ty #m #b #o cases (load_value_of_type ty m b o) |
---|
| 1872 | [ 1: %1 // | 2: #v %2 /2 by ex_intro/ ] qed. |
---|
| 1873 | |
---|
| 1874 | (* Simulation relations. *) |
---|
[2438] | 1875 | inductive switch_cont_sim : list (ident × type) → cont → cont → Prop ≝ |
---|
| 1876 | | swc_stop : |
---|
| 1877 | ∀new_vars. switch_cont_sim new_vars Kstop Kstop |
---|
| 1878 | | swc_seq : ∀s,k,k',u,s',new_vars. |
---|
[2227] | 1879 | fresh_for_statement s u → |
---|
[2438] | 1880 | switch_cont_sim new_vars k k' → |
---|
| 1881 | s' = ret_st ? (switch_removal s u) → |
---|
| 1882 | lset_inclusion ? (ret_vars ? (switch_removal s u)) new_vars → |
---|
| 1883 | switch_cont_sim new_vars (Kseq s k) (Kseq s' k') |
---|
| 1884 | | swc_while : ∀e,s,k,k',u,s',new_vars. |
---|
[2391] | 1885 | fresh_for_statement (Swhile e s) u → |
---|
[2438] | 1886 | switch_cont_sim new_vars k k' → |
---|
| 1887 | s' = ret_st ? (switch_removal s u) → |
---|
| 1888 | lset_inclusion ? (ret_vars ? (switch_removal s u)) new_vars → |
---|
| 1889 | switch_cont_sim new_vars (Kwhile e s k) (Kwhile e s' k') |
---|
| 1890 | | swc_dowhile : ∀e,s,k,k',u,s',new_vars. |
---|
[2227] | 1891 | fresh_for_statement (Sdowhile e s) u → |
---|
[2438] | 1892 | switch_cont_sim new_vars k k' → |
---|
| 1893 | s' = ret_st ? (switch_removal s u) → |
---|
| 1894 | lset_inclusion ? (ret_vars ? (switch_removal s u)) new_vars → |
---|
| 1895 | switch_cont_sim new_vars (Kdowhile e s k) (Kdowhile e s' k') |
---|
| 1896 | | swc_for1 : ∀e,s1,s2,k,k',u,s',new_vars. |
---|
[2227] | 1897 | fresh_for_statement (Sfor Sskip e s1 s2) u → |
---|
[2438] | 1898 | switch_cont_sim new_vars k k' → |
---|
| 1899 | s' = (ret_st ? (switch_removal (Sfor Sskip e s1 s2) u)) → |
---|
| 1900 | lset_inclusion ? (ret_vars ? (switch_removal (Sfor Sskip e s1 s2) u)) new_vars → |
---|
| 1901 | switch_cont_sim new_vars (Kseq (Sfor Sskip e s1 s2) k) (Kseq s' k') |
---|
| 1902 | | swc_for2 : ∀e,s1,s2,k,k',u,result1,result2,new_vars. |
---|
[2227] | 1903 | fresh_for_statement (Sfor Sskip e s1 s2) u → |
---|
[2438] | 1904 | switch_cont_sim new_vars k k' → |
---|
| 1905 | result1 = ret_st ? (switch_removal s1 u) → |
---|
| 1906 | result2 = ret_st ? (switch_removal s2 (ret_u ? (switch_removal s1 u))) → |
---|
| 1907 | lset_inclusion ? (ret_vars ? (switch_removal (Sfor Sskip e s1 s2) u)) new_vars → |
---|
| 1908 | switch_cont_sim new_vars (Kfor2 e s1 s2 k) (Kfor2 e result1 result2 k') |
---|
| 1909 | | swc_for3 : ∀e,s1,s2,k,k',u,result1,result2,new_vars. |
---|
[2227] | 1910 | fresh_for_statement (Sfor Sskip e s1 s2) u → |
---|
[2438] | 1911 | switch_cont_sim new_vars k k' → |
---|
| 1912 | result1 = ret_st ? (switch_removal s1 u) → |
---|
| 1913 | result2 = ret_st ? (switch_removal s2 (ret_u ? (switch_removal s1 u))) → |
---|
| 1914 | lset_inclusion ? (ret_vars ? (switch_removal (Sfor Sskip e s1 s2) u)) new_vars → |
---|
| 1915 | switch_cont_sim new_vars (Kfor3 e s1 s2 k) (Kfor3 e result1 result2 k') |
---|
| 1916 | | swc_switch : ∀k,k',new_vars. |
---|
| 1917 | switch_cont_sim new_vars k k' → |
---|
| 1918 | switch_cont_sim new_vars (Kswitch k) (Kswitch k') |
---|
| 1919 | | swc_call : ∀en,en',r,f,k,k',old_vars,new_vars. (* Warning: possible caveat with environments here. *) |
---|
| 1920 | switch_cont_sim old_vars k k' → |
---|
| 1921 | old_vars = \snd (function_switch_removal f) → |
---|
| 1922 | disjoint_extension en en' old_vars → |
---|
| 1923 | switch_cont_sim |
---|
| 1924 | new_vars |
---|
[2227] | 1925 | (Kcall r f en k) |
---|
| 1926 | (Kcall r (\fst (function_switch_removal f)) en' k'). |
---|
| 1927 | |
---|
[2332] | 1928 | record switch_removal_globals (F:Type[0]) (t:F → F) (ge:genv_t F) (ge':genv_t F) : Prop ≝ { |
---|
| 1929 | rg_find_symbol: ∀s. |
---|
| 1930 | find_symbol ? ge s = find_symbol ? ge' s; |
---|
| 1931 | rg_find_funct: ∀v,f. |
---|
| 1932 | find_funct ? ge v = Some ? f → |
---|
| 1933 | find_funct ? ge' v = Some ? (t f); |
---|
| 1934 | rg_find_funct_ptr: ∀b,f. |
---|
| 1935 | find_funct_ptr ? ge b = Some ? f → |
---|
| 1936 | find_funct_ptr ? ge' b = Some ? (t f) |
---|
| 1937 | }. |
---|
| 1938 | |
---|
| 1939 | inductive switch_state_sim (ge : genv) : state → state → Prop ≝ |
---|
| 1940 | | sws_state : |
---|
| 1941 | (* current statement *) |
---|
| 1942 | ∀sss_statement : statement. |
---|
| 1943 | (* label universe *) |
---|
| 1944 | ∀sss_lu : universe SymbolTag. |
---|
| 1945 | (* [sss_lu] must be fresh *) |
---|
| 1946 | ∀sss_lu_fresh : fresh_for_statement sss_statement sss_lu. |
---|
| 1947 | (* current function *) |
---|
| 1948 | ∀sss_func : function. |
---|
| 1949 | (* current function after translation *) |
---|
| 1950 | ∀sss_func_tr : function. |
---|
[2441] | 1951 | (* variables generated during conversion of the function *) |
---|
[2332] | 1952 | ∀sss_new_vars : list (ident × type). |
---|
[2441] | 1953 | (* statement of the transformation *) |
---|
[2332] | 1954 | ∀sss_func_hyp : 〈sss_func_tr, sss_new_vars〉 = function_switch_removal sss_func. |
---|
| 1955 | (* memory state before conversion *) |
---|
| 1956 | ∀sss_m : mem. |
---|
| 1957 | (* memory state after conversion *) |
---|
| 1958 | ∀sss_m_ext : mem. |
---|
| 1959 | (* environment before conversion *) |
---|
| 1960 | ∀sss_env : env. |
---|
| 1961 | (* environment after conversion *) |
---|
| 1962 | ∀sss_env_ext : env. |
---|
| 1963 | (* continuation before conversion *) |
---|
| 1964 | ∀sss_k : cont. |
---|
| 1965 | (* continuation after conversion *) |
---|
| 1966 | ∀sss_k_ext : cont. |
---|
[2387] | 1967 | (* writeable blocks *) |
---|
| 1968 | ∀sss_writeable : list block. |
---|
[2332] | 1969 | (* memory "injection" *) |
---|
[2387] | 1970 | ∀sss_mem_hyp : sr_memext sss_m sss_m_ext sss_writeable. |
---|
[2332] | 1971 | (* The extended environment does not interfer with the old one. *) |
---|
[2387] | 1972 | ∀sss_env_hyp : disjoint_extension sss_env sss_env_ext sss_new_vars. |
---|
[2441] | 1973 | (* The new variables are allocated to a size corresponding to their types. *) |
---|
| 1974 | ∀sss_new_alloc : |
---|
[2448] | 1975 | (∀v.meml ? v sss_new_vars → |
---|
[2441] | 1976 | ∀vb. lookup … sss_env_ext (\fst v) = Some ? vb → |
---|
[2448] | 1977 | valid_block sss_m_ext vb ∧ |
---|
[2441] | 1978 | low (blocks sss_m_ext vb) = OZ ∧ |
---|
[2448] | 1979 | high (blocks sss_m_ext vb) = sizeof (\snd v)). |
---|
| 1980 | (* Exit label for the enclosing switch, if any. Use for [break] conversion in switches. *) |
---|
| 1981 | ∀sss_enclosing_label : option label. |
---|
[2438] | 1982 | (* Extension blocks are writeable. *) |
---|
| 1983 | ∀sss_ext_write : lset_inclusion ? (lset_difference ? (blocks_of_env sss_env_ext) (blocks_of_env sss_env)) sss_writeable. |
---|
[2332] | 1984 | (* conversion of the current statement, using the variables produced during the conversion of the current function *) |
---|
[2438] | 1985 | ∀sss_result_rec. |
---|
| 1986 | ∀sss_result_hyp : switch_removal sss_statement sss_lu = sss_result_rec. |
---|
| 1987 | ∀sss_result. |
---|
| 1988 | sss_result = ret_st ? sss_result_rec → |
---|
| 1989 | (* inclusion of the locally produced new variables in the global new variables *) |
---|
| 1990 | lset_inclusion ? (ret_vars ? sss_result_rec) sss_new_vars → |
---|
[2332] | 1991 | (* simulation between the continuations before and after conversion. *) |
---|
[2438] | 1992 | ∀sss_k_hyp : switch_cont_sim sss_new_vars sss_k sss_k_ext. |
---|
[2332] | 1993 | ext_fresh_for_genv sss_new_vars ge → |
---|
[2227] | 1994 | switch_state_sim |
---|
[2332] | 1995 | ge |
---|
| 1996 | (State sss_func sss_statement sss_k sss_env sss_m) |
---|
[2438] | 1997 | (State sss_func_tr sss_result sss_k_ext sss_env_ext sss_m_ext) |
---|
| 1998 | | sws_callstate : |
---|
| 1999 | ∀ssc_fd. |
---|
| 2000 | ∀ssc_args. |
---|
| 2001 | ∀ssc_k. |
---|
| 2002 | ∀ssc_k_ext. |
---|
| 2003 | ∀ssc_m. |
---|
| 2004 | ∀ssc_m_ext. |
---|
| 2005 | ∀ssc_writeable. |
---|
| 2006 | ∀ssc_mem_hyp : sr_memext ssc_m ssc_m_ext ssc_writeable. |
---|
| 2007 | (match ssc_fd with |
---|
| 2008 | [ CL_Internal ssc_f ⇒ |
---|
| 2009 | switch_cont_sim (\snd (function_switch_removal ssc_f)) ssc_k ssc_k_ext |
---|
| 2010 | | _ ⇒ True ]) → |
---|
| 2011 | switch_state_sim ge (Callstate ssc_fd ssc_args ssc_k ssc_m) |
---|
| 2012 | (Callstate (fundef_switch_removal ssc_fd) ssc_args ssc_k_ext ssc_m_ext) |
---|
| 2013 | | sws_returnstate : |
---|
[2332] | 2014 | ∀ssr_result. |
---|
| 2015 | ∀ssr_k : cont. |
---|
| 2016 | ∀ssr_k_ext : cont. |
---|
| 2017 | ∀ssr_m : mem. |
---|
| 2018 | ∀ssr_m_ext : mem. |
---|
[2387] | 2019 | ∀ssr_writeable : list block. |
---|
| 2020 | ∀ssr_mem_hyp : sr_memext ssr_m ssr_m_ext ssr_writeable. |
---|
[2438] | 2021 | ∀ssr_vars. |
---|
[2332] | 2022 | switch_cont_sim ssr_vars ssr_k ssr_k_ext → |
---|
| 2023 | switch_state_sim ge (Returnstate ssr_result ssr_k ssr_m) (Returnstate ssr_result ssr_k_ext ssr_m_ext) |
---|
[2227] | 2024 | | sws_finalstate : ∀r. |
---|
[2332] | 2025 | switch_state_sim ge (Finalstate r) (Finalstate r). |
---|
[2227] | 2026 | |
---|
[2438] | 2027 | lemma call_cont_swremoval : ∀k,k',vars. |
---|
| 2028 | switch_cont_sim vars k k' → |
---|
| 2029 | switch_cont_sim vars (call_cont k) (call_cont k'). |
---|
| 2030 | #k0 #k0' #vars #K elim K /2/ |
---|
[2227] | 2031 | qed. |
---|
| 2032 | |
---|
| 2033 | (* [eventually ge P s tr] states that after a finite number of [exec_step], the |
---|
| 2034 | property P on states will be verified. *) |
---|
| 2035 | inductive eventually (ge : genv) (P : state → Prop) : state → trace → Prop ≝ |
---|
| 2036 | | eventually_base : ∀s,t,s'. |
---|
| 2037 | exec_step ge s = Value io_out io_in ? 〈t, s'〉 → |
---|
| 2038 | P s' → |
---|
| 2039 | eventually ge P s t |
---|
| 2040 | | eventually_step : ∀s,t,s',t',trace. |
---|
| 2041 | exec_step ge s = Value io_out io_in ? 〈t, s'〉 → |
---|
| 2042 | eventually ge P s' t' → |
---|
| 2043 | trace = (t ⧺ t') → |
---|
| 2044 | eventually ge P s trace. |
---|
[2387] | 2045 | |
---|
[2227] | 2046 | (* [eventually] is not so nice to use directly, we would like to make the mandatory |
---|
| 2047 | * [exec_step ge s = Value ??? 〈t, s'] visible - and in the end we would like not |
---|
| 2048 | to give [s'] ourselves, but matita to compute it. Hence this little intro-wrapper. *) |
---|
| 2049 | lemma eventually_now : ∀ge,P,s,t. |
---|
| 2050 | (∃s'.exec_step ge s = Value io_out io_in ? 〈t,s'〉 ∧ P s') → |
---|
| 2051 | eventually ge P s t. |
---|
| 2052 | #ge #P #s #t * #s' * #Hexec #HP %1{… Hexec HP} (* %{E0} normalize >(append_nil ? t) %1{????? Hexec HP} *) |
---|
| 2053 | qed. |
---|
[2332] | 2054 | |
---|
[2227] | 2055 | lemma eventually_later : ∀ge,P,s,t. |
---|
| 2056 | (∃s',tstep.exec_step ge s = Value io_out io_in ? 〈tstep,s'〉 ∧ ∃tnext. t = tstep ⧺ tnext ∧ eventually ge P s' tnext) → |
---|
| 2057 | eventually ge P s t. |
---|
| 2058 | #ge #P #s #t * #s' * #tstep * #Hexec_step * #tnext * #Heq #Heventually %2{s tstep s' tnext … Heq} |
---|
| 2059 | try assumption |
---|
[2448] | 2060 | qed. |
---|
[2227] | 2061 | |
---|
| 2062 | lemma exec_lvalue_expr_elim : |
---|
[2332] | 2063 | ∀r1,r2,Pok,Qok. |
---|
| 2064 | exec_lvalue_sim r1 r2 → |
---|
| 2065 | (∀val,trace. |
---|
| 2066 | match Pok 〈val,trace〉 with |
---|
[2227] | 2067 | [ Error err ⇒ True |
---|
[2332] | 2068 | | OK pvt ⇒ |
---|
| 2069 | let 〈pval,ptrace〉 ≝ pvt in |
---|
| 2070 | match Qok 〈val,trace〉 with |
---|
[2227] | 2071 | [ Error err ⇒ False |
---|
[2332] | 2072 | | OK qvt ⇒ |
---|
| 2073 | let 〈qval,qtrace〉 ≝ qvt in |
---|
| 2074 | ptrace = qtrace ∧ pval = qval |
---|
[2227] | 2075 | ] |
---|
[2332] | 2076 | ]) → |
---|
| 2077 | exec_expr_sim |
---|
[2227] | 2078 | (match r1 with [ OK x ⇒ Pok x | Error err ⇒ Error ? err ]) |
---|
| 2079 | (match r2 with [ OK x ⇒ Qok x | Error err ⇒ Error ? err ]). |
---|
[2332] | 2080 | #r1 #r2 #Pok #Qok whd in ⊢ (% → ?); |
---|
[2227] | 2081 | elim r1 |
---|
[2332] | 2082 | [ 2: #error #_ #_ normalize #a #Habsurd destruct (Habsurd) |
---|
| 2083 | | 1: normalize nodelta #a #H lapply (H a (refl ??)) |
---|
| 2084 | #Hr2 >Hr2 normalize #H #a' elim a * #b #o #tr |
---|
| 2085 | lapply (H 〈b, o〉 tr) #H1 #H2 >H2 in H1; |
---|
| 2086 | normalize nodelta elim a' in H2; #pval #ptrace #Hpok |
---|
| 2087 | normalize nodelta cases (Qok 〈b,o,tr〉) |
---|
| 2088 | [ 2: #error normalize #Habsurd @(False_ind … Habsurd) |
---|
| 2089 | | 1: * #qval #qtrace normalize nodelta * #Htrace #Hval |
---|
| 2090 | destruct @refl |
---|
| 2091 | ] ] qed. |
---|
[2227] | 2092 | |
---|
[2332] | 2093 | |
---|
[2227] | 2094 | lemma exec_expr_expr_elim : |
---|
[2332] | 2095 | ∀r1,r2,Pok,Qok. |
---|
| 2096 | exec_expr_sim r1 r2 → |
---|
| 2097 | (∀val,trace. |
---|
| 2098 | match Pok 〈val,trace〉 with |
---|
[2227] | 2099 | [ Error err ⇒ True |
---|
[2332] | 2100 | | OK pvt ⇒ |
---|
| 2101 | let 〈pval,ptrace〉 ≝ pvt in |
---|
| 2102 | match Qok 〈val,trace〉 with |
---|
[2227] | 2103 | [ Error err ⇒ False |
---|
[2332] | 2104 | | OK qvt ⇒ |
---|
| 2105 | let 〈qval,qtrace〉 ≝ qvt in |
---|
| 2106 | ptrace = qtrace ∧ pval = qval |
---|
[2227] | 2107 | ] |
---|
[2332] | 2108 | ]) → |
---|
| 2109 | exec_expr_sim |
---|
[2227] | 2110 | (match r1 with [ OK x ⇒ Pok x | Error err ⇒ Error ? err ]) |
---|
| 2111 | (match r2 with [ OK x ⇒ Qok x | Error err ⇒ Error ? err ]). |
---|
[2332] | 2112 | #r1 #r2 #Pok #Qok whd in ⊢ (% → ?); |
---|
[2227] | 2113 | elim r1 |
---|
| 2114 | [ 2: #error #_ #_ normalize #a1 #Habsurd destruct (Habsurd) |
---|
[2332] | 2115 | | 1: normalize nodelta #a #H lapply (H a (refl ??)) |
---|
| 2116 | #Hr2 >Hr2 normalize nodelta #H |
---|
| 2117 | elim a in Hr2; #val #trace |
---|
| 2118 | lapply (H … val trace) |
---|
| 2119 | cases (Pok 〈val, trace〉) |
---|
| 2120 | [ 2: #error normalize #_ #_ #a' #Habsurd destruct (Habsurd) |
---|
| 2121 | | 1: * #pval #ptrace normalize nodelta |
---|
| 2122 | cases (Qok 〈val,trace〉) |
---|
| 2123 | [ 2: #error normalize #Hfalse @(False_ind … Hfalse) |
---|
| 2124 | | 1: * #qval #qtrace normalize nodelta * #Htrace_eq #Hval_eq |
---|
| 2125 | #Hr2_eq destruct #a #H @H |
---|
[2227] | 2126 | ] ] ] qed. |
---|
| 2127 | |
---|
[2387] | 2128 | lemma load_value_of_type_inj : ∀m1,m2,writeable,b,off,ty. |
---|
| 2129 | sr_memext m1 m2 writeable → ∀v. |
---|
[2332] | 2130 | load_value_of_type ty m1 b off = Some ? v → |
---|
| 2131 | load_value_of_type ty m2 b off = Some ? v. |
---|
[2387] | 2132 | #m1 #m2 #writeable #b #off #ty #Hinj #v |
---|
| 2133 | @(load_sim_fe ?? (sr_memext_load_sim … Hinj) (mk_pointer b off)) |
---|
[2227] | 2134 | qed. |
---|
| 2135 | |
---|
[2438] | 2136 | (* Conservation of the semantics of binary operators under memory extensions. |
---|
| 2137 | Tried to factorise it a bit but the play with indexes just becomes too messy. *) |
---|
[2387] | 2138 | lemma sim_sem_binary_operation : ∀op,v1,v2,e1,e2,m1,m2,writeable. |
---|
| 2139 | ∀Hext:sr_memext m1 m2 writeable. ∀res. |
---|
[2332] | 2140 | sem_binary_operation op v1 (typeof e1) v2 (typeof e2) m1 = Some ? res → |
---|
| 2141 | sem_binary_operation op v1 (typeof e1) v2 (typeof e2) m2 = Some ? res. |
---|
[2387] | 2142 | #op #v1 #v2 #e1 #e2 #m1 #m2 #writeable #Hmemext #res cases op |
---|
[2332] | 2143 | whd in match (sem_binary_operation ??????); |
---|
| 2144 | try // |
---|
| 2145 | whd in match (sem_binary_operation ??????); |
---|
[2438] | 2146 | lapply (me_valid_pointers … Hmemext) |
---|
| 2147 | lapply (me_not_writeable_ptr … Hmemext) |
---|
[2332] | 2148 | elim m1 in Hmemext; #contents1 #nextblocks1 #Hnextpos1 |
---|
| 2149 | elim m2 #contents2 #nextblocks2 #Hnextpos2 |
---|
[2438] | 2150 | * #Hnonempty #Hwriteable #Hnot_writeable #Hnot_writeable_ptr #Hvalid |
---|
[2332] | 2151 | whd in match (sem_cmp ??????); |
---|
| 2152 | whd in match (sem_cmp ??????); |
---|
[2438] | 2153 | [ 1,2: cases (classify_cmp (typeof e1) (typeof e2)) |
---|
[2298] | 2154 | normalize nodelta |
---|
[2468] | 2155 | [ 1,4: #sz #sg try // |
---|
| 2156 | | 2,5: #opt #ty |
---|
[2332] | 2157 | cases v1 normalize nodelta |
---|
[2468] | 2158 | [ 1,5: | 2,6: #sz #i | 3,7: | 4,8: #ptr ] |
---|
| 2159 | [ 1,2,3,4: #Habsurd destruct (Habsurd) |
---|
| 2160 | | 5,6: #H @H ] |
---|
[2332] | 2161 | cases v2 normalize nodelta |
---|
[2468] | 2162 | [ 1,5: | 2,6: #sz' #i' | 3,7: | 4,8: #ptr' ] |
---|
| 2163 | [ 1,2,3,4: #Habsurd destruct (Habsurd) |
---|
| 2164 | | 5,6: #H @H ] |
---|
[2438] | 2165 | lapply (Hvalid ptr) |
---|
[2387] | 2166 | cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr) |
---|
[2438] | 2167 | [ 2,4: >andb_lsimpl_false normalize nodelta cases (eq_block ??) #_ normalize #Habsurd destruct (Habsurd) ] |
---|
| 2168 | #Hvalid' >(Hvalid' (refl ??)) |
---|
| 2169 | lapply (Hvalid ptr') |
---|
[2387] | 2170 | cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr') |
---|
[2438] | 2171 | [ 2,4: >andb_lsimpl_true #_ normalize nodelta cases (eq_block ??) normalize nodelta #Habsurd destruct (Habsurd) ] |
---|
| 2172 | #H' >(H' (refl ??)) >andb_lsimpl_true normalize nodelta #H @H |
---|
[2468] | 2173 | | 3,6: #ty1 #ty2 #H @H ] |
---|
[2438] | 2174 | | 3,4: cases (classify_cmp (typeof e1) (typeof e2)) |
---|
[2298] | 2175 | normalize nodelta |
---|
[2468] | 2176 | [ 1,4: #sz #sg try // |
---|
| 2177 | | 2,5: #opt #ty |
---|
[2332] | 2178 | cases v1 normalize nodelta |
---|
[2468] | 2179 | [ 1,5: | 2,6: #sz #i | 3,7: | 4,8: #ptr ] |
---|
| 2180 | [ 1,2,3,4: #Habsurd destruct (Habsurd) |
---|
| 2181 | | 5,6: #H @H ] |
---|
[2332] | 2182 | cases v2 normalize nodelta |
---|
[2468] | 2183 | [ 1,5: | 2,6: #sz' #i' | 3,7: | 4,8: #ptr' ] |
---|
| 2184 | [ 1,2,3,4: #Habsurd destruct (Habsurd) |
---|
| 2185 | | 5,6: #H @H ] |
---|
[2438] | 2186 | lapply (Hvalid ptr) |
---|
[2332] | 2187 | cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr) |
---|
[2438] | 2188 | [ 2,4: >andb_lsimpl_false normalize nodelta cases (eq_block ??) #_ normalize #Habsurd destruct (Habsurd) ] |
---|
| 2189 | #Hvalid' >(Hvalid' (refl ??)) |
---|
| 2190 | lapply (Hvalid ptr') |
---|
[2332] | 2191 | cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr') |
---|
[2438] | 2192 | [ 2,4: >andb_lsimpl_true #_ normalize nodelta cases (eq_block ??) normalize nodelta #Habsurd destruct (Habsurd) ] |
---|
| 2193 | #H' >(H' (refl ??)) >andb_lsimpl_true normalize nodelta #H @H |
---|
[2468] | 2194 | | 3,6: #ty1 #ty2 #H @H ] |
---|
[2438] | 2195 | | 5,6: cases (classify_cmp (typeof e1) (typeof e2)) |
---|
[2298] | 2196 | normalize nodelta |
---|
[2468] | 2197 | [ 1,4: #sz #sg try // |
---|
| 2198 | | 2,5: #opt #ty |
---|
[2332] | 2199 | cases v1 normalize nodelta |
---|
[2468] | 2200 | [ 1,5: | 2,6: #sz #i | 3,7: | 4,8: #ptr ] |
---|
| 2201 | [ 1,2,3,4: #Habsurd destruct (Habsurd) |
---|
| 2202 | | 5,6: #H @H ] |
---|
[2332] | 2203 | cases v2 normalize nodelta |
---|
[2468] | 2204 | [ 1,5: | 2,6: #sz' #i' | 3,7: | 4,8: #ptr' ] |
---|
| 2205 | [ 1,2,3,4: #Habsurd destruct (Habsurd) |
---|
| 2206 | | 5,6: #H @H ] |
---|
[2438] | 2207 | lapply (Hvalid ptr) |
---|
[2332] | 2208 | cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr) |
---|
[2438] | 2209 | [ 2,4: >andb_lsimpl_false normalize nodelta cases (eq_block ??) #_ normalize #Habsurd destruct (Habsurd) ] |
---|
| 2210 | #Hvalid' >(Hvalid' (refl ??)) |
---|
| 2211 | lapply (Hvalid ptr') |
---|
[2332] | 2212 | cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr') |
---|
[2438] | 2213 | [ 2,4: >andb_lsimpl_true #_ normalize nodelta cases (eq_block ??) normalize nodelta #Habsurd destruct (Habsurd) ] |
---|
| 2214 | #H' >(H' (refl ??)) >andb_lsimpl_true normalize nodelta #H @H |
---|
[2468] | 2215 | | 3,6: #ty1 #ty2 #H @H ] |
---|
[2302] | 2216 | ] qed. |
---|
| 2217 | |
---|
[2227] | 2218 | (* Simulation relation on expressions *) |
---|
[2387] | 2219 | lemma sim_related_globals : ∀ge,ge',en1,m1,en2,m2,writeable,ext. |
---|
| 2220 | ∀Hext:sr_memext m1 m2 writeable. |
---|
[2332] | 2221 | switch_removal_globals ? fundef_switch_removal ge ge' → |
---|
[2387] | 2222 | disjoint_extension en1 en2 ext → |
---|
| 2223 | (* disjoint_extension en1 en2 ext Hext → *) |
---|
[2227] | 2224 | ext_fresh_for_genv ext ge → |
---|
[2332] | 2225 | (∀e. exec_expr_sim (exec_expr ge en1 m1 e) (exec_expr ge' en2 m2 e)) ∧ |
---|
| 2226 | (∀ed, ty. exec_lvalue_sim (exec_lvalue' ge en1 m1 ed ty) (exec_lvalue' ge' en2 m2 ed ty)). |
---|
[2387] | 2227 | #ge #ge' #en1 #m1 #en2 #m2 #writeable #ext #Hext #Hrelated #Hdisjoint (* #Hdisjoint *) #Hext_fresh_for_genv |
---|
[2227] | 2228 | @expr_lvalue_ind_combined |
---|
| 2229 | [ 1: #csz #cty #i #a1 |
---|
| 2230 | whd in match (exec_expr ????); elim cty |
---|
[2468] | 2231 | [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ] |
---|
[2227] | 2232 | normalize nodelta |
---|
| 2233 | [ 2: cases (eq_intsize csz sz) normalize nodelta |
---|
| 2234 | [ 1: #H destruct (H) /4 by ex_intro, conj, vint_eq/ |
---|
| 2235 | | 2: #Habsurd destruct (Habsurd) ] |
---|
[2468] | 2236 | | 3,4,5: #_ #H destruct (H) |
---|
[2227] | 2237 | | *: #H destruct (H) ] |
---|
[2468] | 2238 | | 2: * |
---|
| 2239 | [ #sz #i | #var_id | #e1 | #e1 | #op #e1 | #op #e1 #e2 | #cast_ty #e1 |
---|
| 2240 | | #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ] |
---|
[2227] | 2241 | #ty whd in ⊢ (% → ?); #Hind try @I |
---|
| 2242 | whd in match (Plvalue ???); |
---|
| 2243 | [ 1,2,3: whd in match (exec_expr ????); whd in match (exec_expr ????); #a1 |
---|
| 2244 | cases (exec_lvalue' ge en1 m1 ? ty) in Hind; |
---|
| 2245 | [ 2,4,6: #error #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) |
---|
[2332] | 2246 | | 1,3,5: normalize nodelta #b1 #H lapply (H b1 (refl ??)) #Heq >Heq |
---|
| 2247 | normalize nodelta |
---|
| 2248 | elim b1 * #bl1 #o1 #tr1 (* elim b2 * #bl2 #o2 #tr2 *) |
---|
[2227] | 2249 | whd in match (load_value_of_type' ???); |
---|
| 2250 | whd in match (load_value_of_type' ???); |
---|
[2387] | 2251 | lapply (load_value_of_type_inj m1 m2 writeable bl1 o1 ty Hext) |
---|
[2227] | 2252 | cases (load_value_of_type ty m1 bl1 o1) |
---|
| 2253 | [ 1,3,5: #_ #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
[2332] | 2254 | | 2,4,6: #v #H normalize in ⊢ (% → ?); #Heq destruct (Heq) |
---|
| 2255 | >(H v (refl ??)) @refl |
---|
[2227] | 2256 | ] ] ] |
---|
[2468] | 2257 | | 3: #v #ty whd * * #b #o #tr |
---|
[2227] | 2258 | whd in match (exec_lvalue' ?????); |
---|
[2387] | 2259 | whd in match (exec_lvalue' ?????); cases Hdisjoint * |
---|
| 2260 | #HA #HB #HC lapply (HA v) lapply (HB v) lapply (HC v) -HA -HB -HC |
---|
[2227] | 2261 | lapply (Hext_fresh_for_genv v) |
---|
| 2262 | cases (mem_assoc_env v ext) #Hglobal |
---|
[2387] | 2263 | [ 1: >(Hglobal (refl ??)) #_ #HB #HA >(HA (refl ??)) normalize |
---|
| 2264 | #Habsurd destruct |
---|
| 2265 | | 2: normalize nodelta #Hsim #_ #_ |
---|
| 2266 | cases (lookup ?? en1 v) in Hsim; normalize nodelta |
---|
| 2267 | [ 1: #Hlookup2 <(Hlookup2 (refl ??)) normalize nodelta |
---|
[2332] | 2268 | lapply (rg_find_symbol … Hrelated v) #Heq_find_sym >Heq_find_sym |
---|
| 2269 | #H @H |
---|
[2387] | 2270 | | 2: #blo #Hlookup2 <(Hlookup2 (refl ??)) #Heq normalize nodelta @Heq ] ] |
---|
[2468] | 2271 | | 4: #e #ty whd in ⊢ (% → %); |
---|
[2227] | 2272 | whd in match (exec_lvalue' ?????); |
---|
| 2273 | whd in match (exec_lvalue' ?????); |
---|
| 2274 | cases (exec_expr ge en1 m1 e) |
---|
[2332] | 2275 | [ 1: * #v1 #tr1 #H elim (H 〈v1,tr1〉 (refl ??)) * #v1' #tr1' #H @H |
---|
[2227] | 2276 | | 2: #error #_ normalize #a1 #Habsurd destruct (Habsurd) ] |
---|
[2468] | 2277 | | 5: #ty #e #ty' |
---|
[2227] | 2278 | #Hsim @(exec_lvalue_expr_elim … Hsim) |
---|
| 2279 | cases ty |
---|
[2468] | 2280 | [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ] |
---|
[2332] | 2281 | * #b #o normalize nodelta try /2 by I/ |
---|
| 2282 | #tr @conj try @refl |
---|
[2468] | 2283 | | 6: #ty #op #e |
---|
[2332] | 2284 | #Hsim @(exec_expr_expr_elim … Hsim) #v #trace |
---|
| 2285 | cases (sem_unary_operation op v (typeof e)) normalize nodelta |
---|
| 2286 | try @I |
---|
| 2287 | #v @conj @refl |
---|
[2468] | 2288 | | 7: #ty #op #e1 #e2 #Hsim1 #Hsim2 |
---|
[2332] | 2289 | @(exec_expr_expr_elim … Hsim1) #v #trace |
---|
[2263] | 2290 | cases (exec_expr ge en1 m1 e2) in Hsim2; |
---|
| 2291 | [ 2: #error // ] |
---|
[2332] | 2292 | * #pval #ptrace normalize in ⊢ (% → ?); #Hsim2 |
---|
| 2293 | whd in match (m_bind ?????); |
---|
| 2294 | >(Hsim2 ? (refl ??)) |
---|
| 2295 | whd in match (m_bind ?????); |
---|
[2387] | 2296 | lapply (sim_sem_binary_operation op v pval e1 e2 m1 m2 writeable Hext) |
---|
[2332] | 2297 | cases (sem_binary_operation op v (typeof e1) pval (typeof e2) m1) |
---|
| 2298 | [ 1: #_ // ] #val #H >(H val (refl ??)) |
---|
| 2299 | normalize destruct @conj @refl |
---|
[2468] | 2300 | | 8: #ty #cast_ty #e #Hsim @(exec_expr_expr_elim … Hsim) |
---|
[2332] | 2301 | #v #tr |
---|
| 2302 | cut (exec_cast m1 v (typeof e) cast_ty = exec_cast m2 v (typeof e) cast_ty) |
---|
| 2303 | [ @refl ] |
---|
| 2304 | #Heq >Heq |
---|
| 2305 | cases (exec_cast m2 v (typeof e) cast_ty) |
---|
| 2306 | [ 2: // |
---|
| 2307 | | 1: #v normalize @conj @refl ] |
---|
[2468] | 2308 | | 9: #ty #e1 #e2 #e3 #Hsim1 #Hsim2 #Hsim3 |
---|
[2332] | 2309 | @(exec_expr_expr_elim … Hsim1) #v #tr |
---|
[2271] | 2310 | cases (exec_bool_of_val ? (typeof e1)) #b |
---|
[2332] | 2311 | [ 2: normalize @I ] |
---|
[2271] | 2312 | cases b normalize nodelta |
---|
[2332] | 2313 | whd in match (m_bind ?????); |
---|
| 2314 | whd in match (m_bind ?????); |
---|
| 2315 | normalize nodelta |
---|
[2271] | 2316 | [ 1: (* true branch *) |
---|
| 2317 | cases (exec_expr ge en1 m1 e2) in Hsim2; |
---|
| 2318 | [ 2: #error normalize #_ @I |
---|
[2332] | 2319 | | 1: * #e2v #e2tr normalize #H >(H ? (refl ??)) normalize nodelta |
---|
| 2320 | @conj @refl ] |
---|
[2271] | 2321 | | 2: (* false branch *) |
---|
| 2322 | cases (exec_expr ge en1 m1 e3) in Hsim3; |
---|
| 2323 | [ 2: #error normalize #_ @I |
---|
[2332] | 2324 | | 1: * #e3v #e3tr normalize #H >(H ? (refl ??)) normalize nodelta |
---|
| 2325 | @conj @refl ] ] |
---|
[2468] | 2326 | | 10,11: #ty #e1 #e2 #Hsim1 #Hsim2 |
---|
[2332] | 2327 | @(exec_expr_expr_elim … Hsim1) #v #tr |
---|
| 2328 | cases (exec_bool_of_val v (typeof e1)) |
---|
| 2329 | [ 2,4: #error normalize @I ] |
---|
| 2330 | * |
---|
[2271] | 2331 | whd in match (m_bind ?????); |
---|
| 2332 | whd in match (m_bind ?????); |
---|
[2332] | 2333 | [ 2,3: normalize @conj try @refl ] |
---|
[2271] | 2334 | cases (exec_expr ge en1 m1 e2) in Hsim2; |
---|
| 2335 | [ 2,4: #error #_ normalize @I ] |
---|
[2332] | 2336 | * #v2 #tr2 whd in ⊢ (% → %); #H2 normalize nodelta >(H2 ? (refl ??)) |
---|
| 2337 | normalize nodelta |
---|
[2271] | 2338 | cases (exec_bool_of_val v2 (typeof e2)) |
---|
[2332] | 2339 | [ 2,4: #error normalize @I ] |
---|
| 2340 | * normalize @conj @refl |
---|
[2468] | 2341 | | 12: #ty #ty' cases ty |
---|
| 2342 | [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ] |
---|
[2332] | 2343 | whd in match (exec_expr ????); whd #a #H @H |
---|
[2468] | 2344 | | 13: #ty #ed #aggregty #i #Hsim whd * * #b #o #tr |
---|
[2271] | 2345 | whd in match (exec_lvalue' ?????); |
---|
| 2346 | whd in match (exec_lvalue' ge' en2 m2 (Efield (Expr ed aggregty) i) ty); |
---|
| 2347 | whd in match (typeof ?); |
---|
| 2348 | cases aggregty in Hsim; |
---|
[2468] | 2349 | [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ] |
---|
[2271] | 2350 | normalize nodelta #Hsim |
---|
[2468] | 2351 | [ 1,2,3,4,5,8: #Habsurd destruct (Habsurd) ] |
---|
[2271] | 2352 | whd in match (m_bind ?????); |
---|
| 2353 | whd in match (m_bind ?????); |
---|
| 2354 | whd in match (exec_lvalue ge en1 m1 (Expr ed ?)); |
---|
| 2355 | cases (exec_lvalue' ge en1 m1 ed ?) in Hsim; |
---|
| 2356 | [ 2,4: #error #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ] |
---|
[2332] | 2357 | * * #b1 #o1 #tr1 whd in ⊢ (% → ?); #H |
---|
| 2358 | whd in match (exec_lvalue ge' en2 m2 (Expr ed ?)); |
---|
| 2359 | >(H ? (refl ??)) normalize nodelta #H @H |
---|
[2468] | 2360 | | 14: #ty #l #e #Hsim |
---|
[2332] | 2361 | @(exec_expr_expr_elim … Hsim) #v #tr normalize nodelta @conj // |
---|
[2468] | 2362 | | 15: * |
---|
| 2363 | [ #sz #i | #var_id | #e1 | #e1 | #op #e1 | #op #e1 #e2 | #cast_ty #e1 |
---|
| 2364 | | #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ] |
---|
[2227] | 2365 | #ty normalize in ⊢ (% → ?); |
---|
[2468] | 2366 | [ 2,3,12: @False_ind |
---|
[2332] | 2367 | | *: #_ normalize #a1 #Habsurd @Habsurd ] |
---|
[2302] | 2368 | ] qed. |
---|
[2227] | 2369 | |
---|
[2438] | 2370 | lemma exec_lvalue_sim_aux : ∀ge,ge',env,env_ext,m,m_ext. |
---|
| 2371 | (∀ed,ty. exec_lvalue_sim (exec_lvalue' ge env m ed ty) |
---|
| 2372 | (exec_lvalue' ge' env_ext m_ext ed ty)) → |
---|
| 2373 | ∀e. exec_lvalue_sim (exec_lvalue ge env m e) |
---|
| 2374 | (exec_lvalue ge' env_ext m_ext e). |
---|
| 2375 | #ge #ge' #env #env_ext #m #m_ext #H * #ed #ty @H qed. |
---|
| 2376 | |
---|
| 2377 | lemma exec_expr_sim_to_exec_exprlist : |
---|
| 2378 | ∀ge,ge',en1,en2,m1,m2. |
---|
| 2379 | (∀e. exec_expr_sim (exec_expr ge en1 m1 e) (exec_expr ge' en2 m2 e)) → |
---|
| 2380 | ∀l. res_sim ? (exec_exprlist ge en1 m1 l) (exec_exprlist ge' en2 m2 l). |
---|
| 2381 | #ge #ge' #en1 #en2 #m1 #m2 #Hsim #l elim l |
---|
| 2382 | [ 1: whd #a #Heq normalize in Heq ⊢ %; destruct @refl |
---|
| 2383 | | 2: #hd #tl #Hind whd * #lv #tr whd in ⊢ ((??%?) → (??%?)); |
---|
| 2384 | lapply (Hsim hd) |
---|
| 2385 | cases (exec_expr ge en1 m1 hd) |
---|
| 2386 | [ 2: #error normalize #_ #Habsurd destruct (Habsurd) |
---|
| 2387 | | 1: * #v #vtr whd in ⊢ (% → ?); #Hsim >(Hsim ? (refl ??)) |
---|
| 2388 | normalize nodelta |
---|
| 2389 | cases (exec_exprlist ge en1 m1 tl) in Hind; |
---|
| 2390 | [ 2: #error normalize #_ #Habsurd destruct (Habsurd) |
---|
| 2391 | | 1: #a normalize #H >(H ? (refl ??)) #Heq destruct normalize @refl |
---|
| 2392 | ] |
---|
| 2393 | ] |
---|
| 2394 | ] qed. |
---|
| 2395 | |
---|
[2227] | 2396 | (* The return type of any function is invariant under switch removal *) |
---|
| 2397 | lemma fn_return_simplify : ∀f. fn_return (\fst (function_switch_removal f)) = fn_return f. |
---|
[2438] | 2398 | #f elim f #ty #args #vars #body whd in match (function_switch_removal ?); |
---|
| 2399 | cases (switch_removal ??) * #stmt #fvs #u @refl |
---|
[2227] | 2400 | qed. |
---|
| 2401 | |
---|
| 2402 | (* Similar stuff for fundefs *) |
---|
| 2403 | lemma fundef_type_simplify : ∀clfd. type_of_fundef clfd = type_of_fundef (fundef_switch_removal clfd). |
---|
[2438] | 2404 | * // * #ty #args #vars #body whd in ⊢ (??%%); |
---|
| 2405 | whd in match (function_switch_removal ?); cases (switch_removal ??) * #st #u |
---|
| 2406 | normalize nodelta #u @refl |
---|
| 2407 | qed. |
---|
[2227] | 2408 | |
---|
[2391] | 2409 | lemma while_fresh_lift : ∀e,s,u. |
---|
| 2410 | fresh_for_expression e u → fresh_for_statement s u → fresh_for_statement (Swhile e s) u. |
---|
| 2411 | #e #s * #u whd in ⊢ (% → % → %); whd in match (max_of_statement (Swhile ??)); |
---|
[2227] | 2412 | cases (max_of_expr e) #e cases (max_of_statement s) #s normalize |
---|
| 2413 | cases (leb e s) try /2/ |
---|
[2076] | 2414 | qed. |
---|
| 2415 | |
---|
[2227] | 2416 | (* |
---|
| 2417 | lemma while_commute : ∀e0, s0, us0. Swhile e0 (switch_removal s0 us0) = (sw_rem (Swhile e0 s0) us0). |
---|
| 2418 | #e0 #s0 #us0 normalize |
---|
| 2419 | cases (switch_removal s0 us0) * #body #newvars #u' normalize // |
---|
| 2420 | qed.*) |
---|
| 2421 | |
---|
| 2422 | lemma dowhile_fresh_lift : ∀e,s,u. |
---|
| 2423 | fresh_for_expression e u → fresh_for_statement s u → fresh_for_statement (Sdowhile e s) u. |
---|
| 2424 | #e #s * #u whd in ⊢ (% → % → %); whd in match (max_of_statement (Sdowhile ??)); |
---|
| 2425 | cases (max_of_expr e) #e cases (max_of_statement s) #s normalize |
---|
| 2426 | cases (leb e s) try /2/ |
---|
| 2427 | qed. |
---|
[2438] | 2428 | |
---|
[2227] | 2429 | (* |
---|
| 2430 | lemma dowhile_commute : ∀e0, s0, us0. Sdowhile e0 (sw_rem s0 us0) = (sw_rem (Sdowhile e0 s0) us0). |
---|
| 2431 | #e0 #s0 #us0 normalize |
---|
| 2432 | cases (switch_removal s0 us0) * #body #newvars #u' normalize // |
---|
| 2433 | qed.*) |
---|
| 2434 | |
---|
| 2435 | lemma for_fresh_lift : ∀cond,step,body,u. |
---|
| 2436 | fresh_for_statement step u → |
---|
| 2437 | fresh_for_statement body u → |
---|
| 2438 | fresh_for_expression cond u → |
---|
| 2439 | fresh_for_statement (Sfor Sskip cond step body) u. |
---|
| 2440 | #cond #step #body #u |
---|
| 2441 | whd in ⊢ (% → % → % → %); whd in match (max_of_statement (Sfor ????)); |
---|
| 2442 | cases (max_of_statement step) #s |
---|
| 2443 | cases (max_of_statement body) #b |
---|
| 2444 | cases (max_of_expr cond) #c |
---|
| 2445 | whd in match (max_of_statement Sskip); |
---|
| 2446 | >(max_id_commutative least_identifier) |
---|
| 2447 | >max_id_one_neutral normalize nodelta |
---|
| 2448 | normalize elim u #u |
---|
| 2449 | cases (leb s b) cases (leb c b) cases (leb c s) try /2/ |
---|
| 2450 | qed. |
---|
| 2451 | |
---|
| 2452 | (* |
---|
| 2453 | lemma for_commute : ∀e,stm1,stm2,u,uA. |
---|
| 2454 | (uA=\snd (switch_removal stm1 u)) → |
---|
| 2455 | sw_rem (Sfor Sskip e stm1 stm2) u = (Sfor Sskip e (sw_rem stm1 u) (sw_rem stm2 uA)). |
---|
| 2456 | #e #stm1 #stm2 #u #uA #HuA |
---|
| 2457 | whd in match (sw_rem (Sfor ????) u); |
---|
| 2458 | whd in match (switch_removal ??); |
---|
| 2459 | destruct |
---|
| 2460 | normalize in match (\snd (switch_removal Sskip u)); |
---|
| 2461 | whd in match (sw_rem stm1 u); |
---|
| 2462 | cases (switch_removal stm1 u) |
---|
| 2463 | * #stm1' #fresh_vars #uA normalize nodelta |
---|
| 2464 | whd in match (sw_rem stm2 uA); |
---|
| 2465 | cases (switch_removal stm2 uA) |
---|
| 2466 | * #stm2' #fresh_vars2 #uB normalize nodelta |
---|
| 2467 | // |
---|
| 2468 | qed.*) |
---|
| 2469 | |
---|
[2438] | 2470 | lemma simplify_is_not_skip : ∀s. s ≠ Sskip → ∀u. ∃pf. is_Sskip (ret_st ? (switch_removal s u)) = inr ?? pf. |
---|
[2227] | 2471 | * |
---|
[2438] | 2472 | [ 1: * #H @(False_ind … (H (refl ??))) ] |
---|
| 2473 | try /2/ |
---|
| 2474 | [ 1: #s1 #s2 #_ #u normalize |
---|
[2227] | 2475 | cases (switch_removal ? ?) * #a #b #c normalize nodelta |
---|
[2438] | 2476 | cases (switch_removal ? ?) * #e #f #g normalize nodelta |
---|
| 2477 | /2 by ex_intro/ |
---|
| 2478 | | 2: #e #s1 #s2 #_ #u normalize |
---|
[2227] | 2479 | cases (switch_removal ? ?) * #a #b #c normalize nodelta |
---|
[2438] | 2480 | cases (switch_removal ? ?) * #e #f #g normalize nodelta |
---|
| 2481 | /2 by ex_intro/ |
---|
| 2482 | | 3,4: #e #s #_ #u normalize |
---|
| 2483 | cases (switch_removal ? ?) * #e #f #g normalize nodelta |
---|
| 2484 | /2 by ex_intro/ |
---|
| 2485 | | 5: #s1 #e #s2 #s3 #_ #u normalize |
---|
[2227] | 2486 | cases (switch_removal ? ?) * #a #b #c normalize nodelta |
---|
[2438] | 2487 | cases (switch_removal ? ?) * #e #f #g normalize nodelta |
---|
| 2488 | cases (switch_removal ? ?) * #h #i #j normalize nodelta |
---|
| 2489 | /2 by ex_intro/ |
---|
| 2490 | | 6: #e #ls #_ #u normalize |
---|
[2227] | 2491 | cases (switch_removal_branches ? ?) * #a #b #c normalize nodelta |
---|
| 2492 | cases (fresh ??) #e #f normalize nodelta |
---|
| 2493 | cases (fresh ? f) #g #h normalize nodelta |
---|
| 2494 | cases (produce_cond ????) * #k #l #m normalize nodelta |
---|
[2438] | 2495 | /2 by ex_intro/ |
---|
| 2496 | | 7,8: #ls #st #_ #u normalize |
---|
| 2497 | cases (switch_removal ? ?) * #e #f #g normalize nodelta |
---|
| 2498 | /2 by ex_intro/ |
---|
| 2499 | ] qed. |
---|
[2227] | 2500 | |
---|
| 2501 | (* |
---|
| 2502 | lemma sw_rem_commute : ∀stm,u. |
---|
| 2503 | (\fst (\fst (switch_removal stm u))) = sw_rem stm u. |
---|
| 2504 | #stm #u whd in match (sw_rem stm u); // qed. |
---|
| 2505 | *) |
---|
| 2506 | |
---|
| 2507 | lemma fresh_for_statement_inv : |
---|
| 2508 | ∀u,s. fresh_for_statement s u → |
---|
| 2509 | match u with |
---|
| 2510 | [ mk_universe p ⇒ le (p0 one) p ]. |
---|
| 2511 | * #p #s whd in match (fresh_for_statement ??); |
---|
| 2512 | cases (max_of_statement s) #s |
---|
| 2513 | normalize /2/ qed. |
---|
| 2514 | |
---|
| 2515 | lemma fresh_for_Sskip : |
---|
| 2516 | ∀u,s. fresh_for_statement s u → fresh_for_statement Sskip u. |
---|
| 2517 | #u #s #H lapply (fresh_for_statement_inv … H) elim u /2/ qed. |
---|
| 2518 | |
---|
| 2519 | lemma fresh_for_Sbreak : |
---|
| 2520 | ∀u,s. fresh_for_statement s u → fresh_for_statement Sbreak u. |
---|
| 2521 | #u #s #H lapply (fresh_for_statement_inv … H) elim u /2/ qed. |
---|
| 2522 | |
---|
| 2523 | lemma fresh_for_Scontinue : |
---|
| 2524 | ∀u,s. fresh_for_statement s u → fresh_for_statement Scontinue u. |
---|
| 2525 | #u #s #H lapply (fresh_for_statement_inv … H) elim u /2/ qed. |
---|
| 2526 | |
---|
| 2527 | (* |
---|
| 2528 | lemma switch_removal_eq : ∀s,u. ∃res,fvs,u'. switch_removal s u = 〈res, fvs, u'〉. |
---|
| 2529 | #s #u elim (switch_removal s u) * #res #fvs #u' |
---|
| 2530 | %{res} %{fvs} %{u'} // |
---|
| 2531 | qed. |
---|
| 2532 | |
---|
| 2533 | lemma switch_removal_branches_eq : ∀switchcases, u. ∃res,fvs,u'. switch_removal_branches switchcases u = 〈res, fvs, u'〉. |
---|
| 2534 | #switchcases #u elim (switch_removal_branches switchcases u) * #res #fvs #u' |
---|
| 2535 | %{res} %{fvs} %{u'} // |
---|
| 2536 | qed. |
---|
| 2537 | *) |
---|
| 2538 | |
---|
| 2539 | lemma produce_cond_eq : ∀e,ls,u,exit_label. ∃s,lab,u'. produce_cond e ls u exit_label = 〈s,lab,u'〉. |
---|
| 2540 | #e #ls #u #exit_label cases (produce_cond e ls u exit_label) * |
---|
| 2541 | #s #lab #u' %{s} %{lab} %{u'} // |
---|
| 2542 | qed. |
---|
| 2543 | |
---|
| 2544 | (* TODO: this lemma ought to be in a more central place, along with its kin of SimplifiCasts.ma ... *) |
---|
| 2545 | lemma neq_intsize : ∀s1,s2. s1 ≠ s2 → eq_intsize s1 s2 = false. |
---|
| 2546 | * * * |
---|
| 2547 | [ 1,5,9: #H @(False_ind … (H (refl ??))) |
---|
| 2548 | | *: #_ normalize @refl ] |
---|
| 2549 | qed. |
---|
| 2550 | |
---|
| 2551 | lemma exec_expr_int : ∀ge,e,m,expr. |
---|
| 2552 | (∃sz,n,tr. exec_expr ge e m expr = (OK ? 〈Vint sz n, tr〉)) ∨ (∀sz,n,tr. exec_expr ge e m expr ≠ (OK ? 〈Vint sz n, tr〉)). |
---|
| 2553 | #ge #e #m #expr cases (exec_expr ge e m expr) |
---|
| 2554 | [ 2: #error %2 #sz #n #tr % #H destruct (H) |
---|
| 2555 | | 1: * #val #trace cases val |
---|
| 2556 | [ 2: #sz #n %1 %{sz} %{n} %{trace} @refl |
---|
[2468] | 2557 | | 3: | 4: #ptr ] |
---|
[2227] | 2558 | %2 #sz #n #tr % #H destruct (H) |
---|
| 2559 | ] qed. |
---|
| 2560 | |
---|
[2438] | 2561 | lemma switch_removal_elim : ∀s,u. ∃s',fvs',u'. switch_removal s u = 〈s',fvs',u'〉. |
---|
| 2562 | #s #u cases (switch_removal s u) * #s' #fvs' #u' |
---|
| 2563 | %{s'} %{fvs'} %{u'} @refl |
---|
| 2564 | qed. |
---|
[2227] | 2565 | |
---|
[2438] | 2566 | lemma switch_removal_branches_elim : ∀ls,u. ∃ls',fvs',u'. switch_removal_branches ls u = 〈ls',fvs',u'〉. |
---|
| 2567 | #ls #u cases (switch_removal_branches ls u) * * #ls' #fvs' #u' /4 by ex_intro/ qed. |
---|
| 2568 | |
---|
| 2569 | lemma fresh_elim : ∀u. ∃fv',u'. fresh SymbolTag u = 〈fv', u'〉. #u /3 by ex_intro/ qed. |
---|
| 2570 | |
---|
| 2571 | lemma simplify_switch_elim : ∀e,ls,u. ∃res,u'. simplify_switch e ls u = 〈res, u'〉. |
---|
| 2572 | #e #ls #u cases (simplify_switch e ls u) #res #u /3 by ex_intro/ qed. |
---|
| 2573 | |
---|
[2448] | 2574 | lemma store_int_success : |
---|
| 2575 | ∀b,m,sz,sg,i. valid_block m b → low (blocks m b) = OZ → high (blocks m b) = sizeof (Tint sz sg) → |
---|
| 2576 | ∃m'. store_value_of_type (Tint sz sg) m b zero_offset (Vint sz i) = Some ? m'. |
---|
| 2577 | #b #m #sz #sg |
---|
| 2578 | cases sz |
---|
| 2579 | [ 1: #i #Hvalid #Hlow #Hhigh |
---|
| 2580 | whd in match (store_value_of_type ?????); |
---|
| 2581 | whd in match (fe_to_be_values ??); |
---|
| 2582 | normalize nodelta |
---|
| 2583 | normalize in match (size_intsize ?); |
---|
| 2584 | whd in match (bytes_of_bitvector ??); |
---|
| 2585 | lapply (vsplit_eq2 ? 8 0 i) * #li * #ri #Heq_i |
---|
| 2586 | <(vsplit_prod … Heq_i) normalize nodelta |
---|
| 2587 | >(BitVector_O … ri) whd in match (storen ???); |
---|
| 2588 | lapply (valid_pointer_to_bestorev_ok m (mk_pointer b zero_offset) (BVByte li) ?) |
---|
| 2589 | [ 1: whd in match (valid_pointer ??); >(Zlt_to_Zltb_true ?? Hvalid) >andb_lsimpl_true |
---|
| 2590 | >unfold_low_bound >unfold_high_bound >Hlow >Hhigh |
---|
| 2591 | >(Zle_to_Zleb_true … (reflexive_Zle OZ)) normalize nodelta |
---|
| 2592 | @Zlt_to_Zltb_true // ] |
---|
| 2593 | * #m' #Hbestorev >Hbestorev %{m'} @refl |
---|
| 2594 | | 2: #i #Hvalid #Hlow #Hhigh |
---|
| 2595 | whd in match (store_value_of_type ?????); |
---|
| 2596 | whd in match (fe_to_be_values ??); |
---|
| 2597 | normalize nodelta |
---|
| 2598 | normalize in match (size_intsize ?); |
---|
| 2599 | whd in match (bytes_of_bitvector ??); |
---|
| 2600 | lapply (vsplit_eq2 ? 8 (1*8) i) * #li * #ri #Heq_i |
---|
| 2601 | <(vsplit_prod … Heq_i) normalize nodelta whd in match (storen ???); |
---|
| 2602 | lapply (valid_pointer_to_bestorev_ok m (mk_pointer b zero_offset) (BVByte li) ?) |
---|
| 2603 | [ 1: whd in match (valid_pointer ??); >(Zlt_to_Zltb_true ?? Hvalid) >andb_lsimpl_true |
---|
| 2604 | >unfold_low_bound >unfold_high_bound >Hlow >Hhigh |
---|
| 2605 | >(Zle_to_Zleb_true … (reflexive_Zle OZ)) normalize nodelta |
---|
| 2606 | @Zlt_to_Zltb_true // ] |
---|
| 2607 | * #m0 #Hbestorev >Hbestorev normalize nodelta |
---|
| 2608 | whd in match (bytes_of_bitvector ??); |
---|
| 2609 | lapply (vsplit_eq2 ? 8 (0*8) ri) * #rli * #rri #Heq_ri |
---|
| 2610 | <(vsplit_prod … Heq_ri) normalize nodelta |
---|
| 2611 | cases (mem_bounds_invariant_after_bestorev … Hbestorev) * * * #Hnext0 #Hblocks0 #_ #_ #_ |
---|
| 2612 | lapply (valid_pointer_to_bestorev_ok m0 |
---|
| 2613 | (mk_pointer b (mk_offset |
---|
| 2614 | [[false; false; false; false; false; false; false; false; |
---|
| 2615 | false; false; false; false; false; false; false; true]])) |
---|
| 2616 | (BVByte rli) ?) |
---|
| 2617 | [ 1: whd in match (valid_pointer ??); >Hnext0 >(Zlt_to_Zltb_true ?? Hvalid) >andb_lsimpl_true |
---|
| 2618 | cases (Hblocks0 b) #HA #HB |
---|
| 2619 | >unfold_low_bound >unfold_high_bound >HA >HB >Hlow >Hhigh normalize nodelta |
---|
| 2620 | @Zlt_to_Zltb_true normalize // ] |
---|
| 2621 | * #m1 #Hbestorev1 %{m1} whd in ⊢ (??(???%)?); whd in match (storen ???); |
---|
| 2622 | normalize in match (shift_pointer ???); >Hbestorev1 normalize nodelta |
---|
| 2623 | @refl |
---|
| 2624 | | 3: #i #Hvalid #Hlow #Hhigh |
---|
| 2625 | whd in match (store_value_of_type ?????); |
---|
| 2626 | whd in match (fe_to_be_values ??); |
---|
| 2627 | normalize nodelta |
---|
| 2628 | normalize in match (size_intsize ?); |
---|
| 2629 | whd in match (bytes_of_bitvector ??); |
---|
| 2630 | lapply (vsplit_eq2 ? 8 (3*8) i) * #iA * #iB #Heq_i |
---|
| 2631 | <(vsplit_prod … Heq_i) normalize nodelta whd in match (storen ???); |
---|
| 2632 | lapply (valid_pointer_to_bestorev_ok m (mk_pointer b zero_offset) (BVByte iA) ?) |
---|
| 2633 | [ 1: whd in match (valid_pointer ??); >(Zlt_to_Zltb_true ?? Hvalid) >andb_lsimpl_true |
---|
| 2634 | >unfold_low_bound >unfold_high_bound >Hlow >Hhigh |
---|
| 2635 | >(Zle_to_Zleb_true … (reflexive_Zle OZ)) normalize nodelta |
---|
| 2636 | @Zlt_to_Zltb_true // ] |
---|
| 2637 | * #m0 #Hbestorev >Hbestorev normalize nodelta |
---|
| 2638 | whd in match (bytes_of_bitvector ??); |
---|
| 2639 | lapply (vsplit_eq2 ? 8 (2*8) iB) * #iC * #iD #Heq_iB |
---|
| 2640 | <(vsplit_prod … Heq_iB) normalize nodelta |
---|
| 2641 | cases (mem_bounds_invariant_after_bestorev … Hbestorev) * * * #Hnext0 #Hblocks0 #_ #_ #_ |
---|
| 2642 | lapply (valid_pointer_to_bestorev_ok m0 |
---|
| 2643 | (shift_pointer 2 (mk_pointer b zero_offset) (bitvector_of_nat 2 1)) |
---|
| 2644 | (BVByte iC) ?) |
---|
| 2645 | [ 1: whd in match (valid_pointer ??); >Hnext0 >(Zlt_to_Zltb_true ?? Hvalid) >andb_lsimpl_true |
---|
| 2646 | cases (Hblocks0 b) #HA #HB |
---|
| 2647 | >unfold_low_bound >unfold_high_bound >HA >HB >Hlow >Hhigh normalize nodelta |
---|
| 2648 | @Zlt_to_Zltb_true normalize // ] |
---|
| 2649 | * #m1 #Hbestorev1 whd in ⊢ (??(λ_.??(???%)?)); whd in match (storen ???); |
---|
| 2650 | normalize in match (shift_pointer 2 (mk_pointer b zero_offset) (bitvector_of_nat 2 1)); |
---|
| 2651 | >Hbestorev1 normalize nodelta |
---|
| 2652 | lapply (vsplit_eq2 ? 8 (1*8) iD) * #iE * #iF #Heq_iD |
---|
| 2653 | whd in match (bytes_of_bitvector ??); |
---|
| 2654 | <(vsplit_prod … Heq_iD) normalize nodelta |
---|
| 2655 | whd in ⊢ (??(λ_.??(???%)?)); |
---|
| 2656 | whd in match (storen ???); |
---|
| 2657 | cases (mem_bounds_invariant_after_bestorev … Hbestorev1) * * * #Hnext1 #Hblocks1 #_ #_ #_ |
---|
| 2658 | lapply (valid_pointer_to_bestorev_ok m1 |
---|
| 2659 | (shift_pointer 2 (mk_pointer b (mk_offset |
---|
| 2660 | [[ false; false; false; false; false; false; false; false; false; false; |
---|
| 2661 | false; false; false; false; false; true ]])) |
---|
| 2662 | (bitvector_of_nat 2 1)) |
---|
| 2663 | (BVByte iE) ?) |
---|
| 2664 | [ 1: normalize in match (shift_pointer ???); whd in match (valid_pointer ??); |
---|
| 2665 | >Hnext1 >Hnext0 >(Zlt_to_Zltb_true ?? Hvalid) |
---|
| 2666 | >andb_lsimpl_true cases (Hblocks1 b) #HA #HB cases (Hblocks0 b) #HC #HD |
---|
| 2667 | >unfold_low_bound >unfold_high_bound >HA >HB >HC >HD >Hlow >Hhigh normalize nodelta |
---|
| 2668 | @Zlt_to_Zltb_true normalize // ] |
---|
| 2669 | * #m2 #Hbestorev2 >Hbestorev2 normalize nodelta |
---|
| 2670 | whd in match (bytes_of_bitvector ??); |
---|
| 2671 | lapply (vsplit_eq2 ? 8 (0*8) iF) * #iG * #iH #Heq_iF |
---|
| 2672 | <(vsplit_prod … Heq_iF) normalize nodelta |
---|
| 2673 | >(BitVector_O … iH) whd in ⊢ (??(λ_.??(???%)?)); |
---|
| 2674 | whd in match (storen ???); |
---|
| 2675 | cases (mem_bounds_invariant_after_bestorev … Hbestorev2) * * * #Hnext2 #Hblocks2 #_ #_ #_ |
---|
| 2676 | lapply (valid_pointer_to_bestorev_ok m2 |
---|
| 2677 | (shift_pointer 2 (shift_pointer 2 (mk_pointer b (mk_offset |
---|
| 2678 | [[ false; false; false; false; false; false; false; false; false; false; |
---|
| 2679 | false; false; false; false; false; true ]])) |
---|
| 2680 | (bitvector_of_nat 2 1)) (bitvector_of_nat 2 1)) |
---|
| 2681 | (BVByte iG) ?) |
---|
| 2682 | [ 1: normalize in match (shift_pointer ???); whd in match (valid_pointer ??); |
---|
| 2683 | >Hnext2 >Hnext1 >Hnext0 >(Zlt_to_Zltb_true ?? Hvalid) |
---|
| 2684 | >andb_lsimpl_true cases (Hblocks2 b) #HA #HB cases (Hblocks1 b) #HC #HD cases (Hblocks0 b) #HE #HF |
---|
| 2685 | >unfold_low_bound >unfold_high_bound >HA >HB >HC >HD >HE >HF >Hlow >Hhigh normalize nodelta |
---|
| 2686 | @Zlt_to_Zltb_true normalize // ] |
---|
| 2687 | * #m3 #Hbestorev3 >Hbestorev3 normalize nodelta %{m3} @refl |
---|
| 2688 | ] qed. |
---|
[2438] | 2689 | |
---|
| 2690 | |
---|
[2449] | 2691 | (* Main theorem. |
---|
| 2692 | 9th November 2012 |
---|
| 2693 | We decided to interrupt the development of this particular proof. What follows is a description of what |
---|
| 2694 | has to be done in order to finish it. |
---|
| 2695 | |
---|
| 2696 | What has been done up to now is the simulation proof for all "easy" cases, that do not interact with the |
---|
| 2697 | switch removal per se, plus a bit of switch. This still implies propagating the memory extension through |
---|
| 2698 | each statement (except switch), as well as various invariants that are needed for the switch case. |
---|
| 2699 | |
---|
| 2700 | The proof for the switch case has been started. Here is how I picture the simulation proof. |
---|
| 2701 | The simulation proof must be broken down in several steps. The source statement executes as this for the first step : |
---|
| 2702 | |
---|
| 2703 | mem, env, k |
---|
| 2704 | ----------------------------------------------------- |
---|
| 2705 | switch(e) case_list ===> |
---|
| 2706 | e ⇓ Vint i, |
---|
[2450] | 2707 | case_list' ← select_switch i case_list; |
---|
[2449] | 2708 | Result = State (seq_of_labeled_statement case_list') (Kswitch k) env mem |
---|
| 2709 | |
---|
| 2710 | The resulting statement executes like this. |
---|
| 2711 | |
---|
| 2712 | mem ⊕ writeable, env ⊕ ext, k' |
---|
| 2713 | fresh ∈ dom(ext) |
---|
| 2714 | ext(fresh) ∈ writeable |
---|
| 2715 | ----------------------------------------------------- |
---|
| 2716 | fresh = e; |
---|
| 2717 | if(e == case0) { --- |
---|
| 2718 | substatement0; | |
---|
| 2719 | goto next0; | |
---|
| 2720 | } else { }; | |
---|
| 2721 | if(e == case1) { |- = converted_cases |
---|
| 2722 | label next0: | |
---|
| 2723 | substatement1; | |
---|
| 2724 | goto next1; | |
---|
| 2725 | } else { }; --- |
---|
| 2726 | ... ===> |
---|
| 2727 | Result = State (fresh = e) (Kseq converted_cases k) (env ⊕ ext) (mem ⊕ writeable) |
---|
| 2728 | ===> |
---|
| 2729 | fresh ⇓ Loc l; |
---|
| 2730 | e ⇓ Vint i; |
---|
| 2731 | m' → store_value_of_type' (typeof a1) m l (Vint i) |
---|
| 2732 | Result = State Sskip (Kseq converted_cases k) (env ⊕ ext) (m' ⊕ writeable) |
---|
| 2733 | ===> |
---|
| 2734 | Result = State converted_cases k (env ⊕ ext) (m' ⊕ writeable) |
---|
| 2735 | This has been done. But this state is still not equivalent with the source one. |
---|
| 2736 | TODO 1: we must prove that after a finite number of Ssequence in [converted_cases], we |
---|
| 2737 | stumble upon a "if(e == casen) { blahblah } else {}; foo" that corresponds to "(seq_of_labeled_statement case_list')" |
---|
| 2738 | (remember that "case_list'" has been truncated to the case corresponding to "i"). |
---|
| 2739 | TODO 2: the resulting pair of states will not be in the standard simulation relation currently defined in |
---|
| 2740 | [switch_state_sim]. We must come up with an additional set of relations with enough informations |
---|
| 2741 | to handle the gotos : |
---|
| 2742 | 1. the gotos from one if to the other avoiding the execution of conditions |
---|
| 2743 | 2. most importantly, the gotos into which "break"s have been converted ! |
---|
| 2744 | This particular subset of the simulation will need some equations allowing to prove that |
---|
| 2745 | the current continuation actually contains a label corresponding to the break. |
---|
| 2746 | Note that when encountering e.g. a while loop inside a converted case, breaks should stop |
---|
| 2747 | beeing converted to gotos and we should go to the 'standard' simulation relation. |
---|
| 2748 | TODO 3: some standard cases remain after that, nothing special (halt case ...). |
---|
| 2749 | |
---|
| 2750 | This should be about it. TODO 1 and 2 will probably require some form of induction over switch cases ... |
---|
| 2751 | *) |
---|
| 2752 | |
---|
[2332] | 2753 | theorem switch_removal_correction : |
---|
[2438] | 2754 | ∀ge,ge'. |
---|
[2332] | 2755 | switch_removal_globals ? fundef_switch_removal ge ge' → |
---|
[2438] | 2756 | ∀s1,s1',tr,s2. |
---|
[2332] | 2757 | switch_state_sim ge s1 s1' → |
---|
[2438] | 2758 | exec_step ge s1 = Value … 〈tr,s2〉 → |
---|
| 2759 | ∃n. after_n_steps (S n) … clight_exec ge' s1' |
---|
| 2760 | (λtr',s2'. tr = tr' ∧ switch_state_sim ge' s2 s2'). |
---|
| 2761 | #ge #ge' #Hrelated #s1 #s1' #tr #s2 #Hsim_state |
---|
[2076] | 2762 | inversion Hsim_state |
---|
| 2763 | [ 1: (* regular state *) |
---|
[2438] | 2764 | #sss_statement #sss_lu #sss_lu_fresh #sss_func #sss_func_tr #sss_new_vars |
---|
[2387] | 2765 | #sss_func_hyp #sss_m #sss_m_ext #sss_env #sss_env_ext #sss_k #sss_k_ext #sss_writeable #sss_mem_hyp |
---|
[2448] | 2766 | #sss_env_hyp #sss_new_alloc #sss_enclosing_label #sss_writeable_hyp #sss_result_rec #sss_result_hyp |
---|
| 2767 | #sss_result #sss_result_proj #sss_incl #sss_k_hyp #Hext_fresh_for_ge |
---|
[2438] | 2768 | #Hs1_eq #Hs1_eq' |
---|
[2387] | 2769 | elim (sim_related_globals … ge ge' |
---|
| 2770 | sss_env sss_m sss_env_ext sss_m_ext sss_writeable sss_new_vars |
---|
[2332] | 2771 | sss_mem_hyp Hrelated sss_env_hyp Hext_fresh_for_ge) |
---|
[2438] | 2772 | #Hsim_expr #Hsim_lvalue #_ |
---|
| 2773 | (* II. Case analysis on the statement. *) |
---|
[2332] | 2774 | cases sss_statement in sss_lu_fresh sss_result_hyp; |
---|
| 2775 | (* Perform the intros for the statements *) |
---|
[2227] | 2776 | [ 1: | 2: #lhs #rhs | 3: #retv #func #args | 4: #stm1 #stm2 | 5: #cond #iftrue #iffalse | 6: #cond #body |
---|
[2076] | 2777 | | 7: #cond #body | 8: #init #cond #step #body | 9,10: | 11: #retval | 12: #cond #switchcases | 13: #lab #body |
---|
| 2778 | | 14: #lab | 15: #cost #body ] |
---|
[2332] | 2779 | #sss_lu_fresh #sss_result_hyp |
---|
[2438] | 2780 | [ 1: (* Skip statement *) |
---|
| 2781 | whd in match (switch_removal ??) in sss_result_hyp; >sss_result_proj <sss_result_hyp |
---|
| 2782 | (* III. Case analysis on the continuation. *) |
---|
[2332] | 2783 | inversion sss_k_hyp normalize nodelta |
---|
[2438] | 2784 | [ 1: #new_vars #Hnew_vars_eq #Hk #Hk' #_ #Hexec_step %{0} whd whd in ⊢ (??%?); |
---|
[2332] | 2785 | >(prod_eq_lproj ????? sss_func_hyp) |
---|
| 2786 | >fn_return_simplify |
---|
| 2787 | whd in match (exec_step ??) in Hexec_step; |
---|
[2438] | 2788 | (* IV. Case analysis on the return type *) |
---|
[2468] | 2789 | cases (fn_return sss_func) in Hexec_step; |
---|
| 2790 | [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain |
---|
| 2791 | | #structname #fieldspec | #unionname #fieldspec | #id ] |
---|
[2076] | 2792 | normalize nodelta |
---|
[2332] | 2793 | whd in ⊢ ((??%?) → ?); |
---|
[2438] | 2794 | [ 1: #H destruct (H) % try @refl |
---|
| 2795 | /3 by sws_returnstate, swc_stop, memext_free_extended_environment, memory_ext_writeable_eq/ |
---|
| 2796 | | *: #Habsurd destruct (Habsurd) ] |
---|
| 2797 | | 2: #s #k #k' #u #s' #new_vars #Hfresh #Hsimcont #Heq_s' #Hincl #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #Hsss_k_hyp |
---|
| 2798 | #Hexec_step %{0} whd |
---|
| 2799 | >(prod_eq_lproj ????? sss_func_hyp) |
---|
| 2800 | whd in match (exec_step ??) in Hexec_step; destruct (Hexec_step) @conj try @refl |
---|
| 2801 | <sss_func_hyp |
---|
| 2802 | lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq') |
---|
| 2803 | %1{u (refl ? (switch_removal s u))} try assumption try @refl |
---|
| 2804 | #id #Hmem lapply (Hext_fresh_for_ge id Hmem) #Hfind <(rg_find_symbol … Hrelated id) @Hfind |
---|
| 2805 | | 3: #cond #body #k #k' #fgen #s' #new_vars #Hfresh #Hsimcont #Heq_s' #Hincl #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_ |
---|
| 2806 | lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq') |
---|
| 2807 | #Hexec_step %{0} whd whd in Hexec_step; |
---|
| 2808 | >(prod_eq_lproj ????? sss_func_hyp) |
---|
| 2809 | whd in match (exec_step ??) in Hexec_step; destruct (Hexec_step) @conj try @refl |
---|
| 2810 | %1{ ((switch_removal (Swhile cond body) fgen))} try assumption try @refl |
---|
| 2811 | [ 1: <sss_func_hyp @refl |
---|
| 2812 | | 2: destruct normalize cases (switch_removal ??) * #body' #fvs' #u' @refl |
---|
| 2813 | | 3: whd in match (switch_removal ??); |
---|
| 2814 | cases (switch_removal body fgen) in Hincl; * #body' #fvs' #fgen' normalize nodelta #H @H |
---|
| 2815 | | 4: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ] |
---|
| 2816 | | 4: #cond #body #k #k' #u #s' #new_vars #Hfresh #Hsimcont #Heq_s' #Hincl #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_ |
---|
| 2817 | lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq') |
---|
| 2818 | #Hexec_step %{0} whd whd in Hexec_step:(??%?) ⊢ (??%?); |
---|
| 2819 | cases (bindIO_inversion ??????? Hexec_step) #x1 * #Hexec |
---|
| 2820 | >(Hsim_expr … Hexec) |
---|
| 2821 | >bindIO_Value cases (exec_bool_of_val ??) |
---|
| 2822 | [ 2: #err normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ] |
---|
| 2823 | #b whd in match (m_bind ?????); whd in match (m_bind ?????); |
---|
| 2824 | cases b normalize nodelta #H whd in H:(??%%) ⊢ %; destruct (H) |
---|
| 2825 | try @conj try @refl |
---|
| 2826 | [ 1: %{u … (switch_removal (Sdowhile cond body) u)} try assumption try // |
---|
| 2827 | [ 1: destruct normalize cases (switch_removal body u) * #body' #fvs' #u' @refl |
---|
| 2828 | | 2: whd in match (switch_removal ??); |
---|
| 2829 | cases (switch_removal body u) in Hincl; * #body' #fvs' #u' normalize nodelta #H @H |
---|
| 2830 | | 3: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ] |
---|
| 2831 | | 2: %{u … (switch_removal Sskip u) } try assumption try // |
---|
| 2832 | [ 1: @(fresh_for_Sskip … Hfresh) |
---|
| 2833 | | 2: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ] ] |
---|
| 2834 | | 5: #cond #stmt1 #stmt2 #k #k' #u #s' #new_vars #Hfresh #Hsimcont #Heq_s' #Hincl #_ |
---|
| 2835 | #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_ |
---|
| 2836 | lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq') |
---|
| 2837 | #Hexec_step %{0} whd whd in Hresult:(??%?) Hexec_step:(??%?); destruct (Hexec_step) |
---|
| 2838 | @conj try @refl |
---|
[2441] | 2839 | %{u … new_vars … sss_mem_hyp … (switch_removal (Sfor Sskip cond stmt1 stmt2) u)} try // try assumption |
---|
[2438] | 2840 | #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem |
---|
| 2841 | | 6: #cond #stmt1 #stmt2 #k #k' #u #result1 #result2 #new_vars |
---|
| 2842 | #Hfresh #Hsimcont #Hresult1 #Hresult2 #Hincl #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_ |
---|
| 2843 | lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq') |
---|
| 2844 | #Hexec %{0} whd in Hexec:(??%?) ⊢ %; destruct (Hexec) @conj try @refl |
---|
| 2845 | %1{u … new_vars … sss_writeable (switch_removal stmt1 u)} try assumption try // |
---|
| 2846 | [ 1: lapply (fresh_to_substatements … Hfresh) normalize * * // |
---|
| 2847 | | 2: whd in match (switch_removal ??) in Hincl; |
---|
| 2848 | cases (switch_removal stmt1 u) in Hincl; * #stmt1' #fvs1' #u' normalize nodelta |
---|
| 2849 | cases (switch_removal stmt2 u') * #stmt2' #fvs2' #u'' normalize nodelta |
---|
| 2850 | whd in match (ret_vars ??); /2 by All_append_l/ |
---|
| 2851 | | 3: @(swc_for3 … u) // |
---|
| 2852 | | 4: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ] |
---|
| 2853 | | 7: #cond #stmt1 #stmt2 #k #k' #u #result1 #result2 #new_vars |
---|
| 2854 | #Hfresh #Hsimcont #Hresult1 #Hresult2 #Hincl #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_ |
---|
| 2855 | lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq') |
---|
| 2856 | #Hexec %{0} whd in Hexec:(??%?) ⊢ %; destruct (Hexec) @conj try @refl |
---|
| 2857 | %1{u … new_vars … sss_writeable … (switch_removal (Sfor Sskip cond stmt1 stmt2) u)} |
---|
[2441] | 2858 | try // try assumption |
---|
[2438] | 2859 | [ 1: whd in match (switch_removal ??) in ⊢ (??%%); destruct normalize |
---|
| 2860 | cases (switch_removal stmt1 u) * #stmt1' #fvs1' #u' normalize |
---|
| 2861 | cases (switch_removal stmt2 u') * #stmt2' #fvs2' #u'' @refl |
---|
| 2862 | | 2: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ] |
---|
| 2863 | | 8: #k #k' #new_vars #Hsimcont #_ #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_ |
---|
| 2864 | lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq') |
---|
| 2865 | #Hexec %{0} whd in Hexec:(??%?) ⊢ %; destruct (Hexec) @conj try @refl |
---|
| 2866 | %1{sss_lu … new_vars … sss_writeable} try // try assumption |
---|
| 2867 | [ 1: destruct (sss_result_hyp) @refl |
---|
| 2868 | | 2: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ] |
---|
| 2869 | | 9: #en #en' #r #f #k #k' #old_vars #new_vars #Hsimcont #Hnew_vars_eq #Hdisjoint_k #_ |
---|
| 2870 | #Hnew_vars_eq #Hsss_k #Hsss_k_ext #_ |
---|
| 2871 | lapply (jmeq_to_eq ??? Hnew_vars_eq) #Hnew_vars_eq' destruct (Hnew_vars_eq') |
---|
| 2872 | #Hexec %{0} whd in Hexec:(??%?) ⊢ %; whd in ⊢ (??%?); |
---|
| 2873 | >(prod_eq_lproj ????? sss_func_hyp) >fn_return_simplify |
---|
| 2874 | cases (fn_return sss_func) in Hexec; normalize nodelta |
---|
[2468] | 2875 | [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain |
---|
| 2876 | | #structname #fieldspec | #unionname #fieldspec | #id ] |
---|
| 2877 | (* [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain |
---|
| 2878 | | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ] *) |
---|
[2438] | 2879 | #Hexec whd in Hexec:(??%?); destruct (Hexec) whd @conj try @refl |
---|
| 2880 | /3 by sws_returnstate, swc_call, memext_free_extended_environment/ |
---|
| 2881 | ] |
---|
| 2882 | | 2: (* Assign statement *) |
---|
| 2883 | lapply (exec_lvalue_sim_aux … Hsim_lvalue) #Hsim |
---|
| 2884 | #Hexec %{0} whd in sss_result_hyp:(??%?); |
---|
| 2885 | cases (bindIO_inversion ??????? Hexec) #xl * #Heq_lhs #Hexec_lhs |
---|
[2448] | 2886 | cases (bindIO_inversion ??????? Hexec_lhs) #xr * #Heq_rhs #Hexec_rhs -Hexec_lhs |
---|
| 2887 | cases (bindIO_inversion ??????? Hexec_rhs) #m' * #Heq_store #Hexec_store -Hexec_rhs |
---|
[2438] | 2888 | whd whd in Hexec_store:(??%%) ⊢ (??%?); >sss_result_proj <sss_result_hyp normalize nodelta |
---|
| 2889 | >(Hsim … Heq_lhs) whd in match (m_bind ?????); |
---|
| 2890 | >(Hsim_expr … Heq_rhs) >bindIO_Value |
---|
[2448] | 2891 | lapply (memext_store_value_of_type' sss_m sss_m_ext m' sss_writeable (typeof lhs) (\fst xl) (\fst xr) sss_mem_hyp ?) |
---|
[2438] | 2892 | [ 1: cases (store_value_of_type' ????) in Heq_store; |
---|
| 2893 | [ 1: normalize #Habsurd destruct (Habsurd) |
---|
| 2894 | | 2: #m normalize #Heq destruct (Heq) @refl ] ] |
---|
[2448] | 2895 | * #m_ext' * #Heq_store' #Hnew_ext >Heq_store' whd in match (m_bind ?????); |
---|
[2438] | 2896 | whd destruct @conj try @refl |
---|
[2441] | 2897 | %1{sss_lu … sss_new_vars … sss_writeable … (switch_removal Sskip sss_lu) } |
---|
| 2898 | try // try assumption |
---|
[2438] | 2899 | [ 1: @(fresh_for_Sskip … sss_lu_fresh) |
---|
[2441] | 2900 | | 3: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem |
---|
[2448] | 2901 | | 2: #v #Hmem #vb #Hlookup lapply (sss_new_alloc v Hmem vb Hlookup) * * #Hvb #Hlow #Hhigh |
---|
| 2902 | cut (store_value_of_type' (typeof lhs) sss_m (\fst xl) (\fst xr) = Some ? m') |
---|
| 2903 | [ cases (store_value_of_type' (typeof lhs) sss_m (\fst xl) (\fst xr)) in Heq_store; |
---|
| 2904 | [ whd in ⊢ ((??%%) → ?); #Habsurd destruct |
---|
| 2905 | | #m0 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) @refl ] ] |
---|
| 2906 | #Hstore lapply (mem_bounds_after_store_value_of_type' … Heq_store') * |
---|
| 2907 | #HA #HB cases (HB vb) #Hlow' #Hhigh' @conj try @conj |
---|
| 2908 | [ 2: >Hlow' in Hlow; // |
---|
| 2909 | | 3: >Hhigh' in Hhigh; // |
---|
| 2910 | | 1: whd >HA @Hvb ] ] |
---|
[2438] | 2911 | | 3: (* Call statement *) |
---|
| 2912 | #Hexec %{0} whd in sss_result_hyp:(??%?); destruct (sss_result_hyp) |
---|
| 2913 | whd whd in ⊢ (??%?); >sss_result_proj normalize nodelta |
---|
| 2914 | whd in Hexec:(??%?); |
---|
| 2915 | cases (bindIO_inversion ??????? Hexec) #xfunc * #Heq_func #Hexec_func |
---|
| 2916 | cases (bindIO_inversion ??????? Hexec_func) #xargs * #Heq_args #Hexec_args |
---|
| 2917 | cases (bindIO_inversion ??????? Hexec_args) #called_fundef * #Heq_fundef #Hexec_typeeq |
---|
| 2918 | cases (bindIO_inversion ??????? Hexec_typeeq) #Htype_eq * #Heq_assert #Hexec_ret |
---|
| 2919 | >(Hsim_expr … Heq_func) whd in match (m_bind ?????); |
---|
| 2920 | >(exec_expr_sim_to_exec_exprlist … Hsim_expr … Heq_args) |
---|
| 2921 | whd in ⊢ (??%?); |
---|
| 2922 | >(rg_find_funct … Hrelated … (opt_to_io_Value … Heq_fundef)) |
---|
| 2923 | whd in ⊢ (??%?); <fundef_type_simplify >Heq_assert |
---|
| 2924 | whd in ⊢ (??%?); -Hexec -Hexec_func -Hexec_args -Hexec_typeeq lapply Hexec_ret -Hexec_ret |
---|
| 2925 | @(option_ind … retv) normalize nodelta |
---|
| 2926 | [ 1: whd in ⊢ ((??%%) → (??%%)); #Heq whd destruct (Heq) @conj try @refl |
---|
| 2927 | %2{sss_writeable … sss_mem_hyp} |
---|
| 2928 | cases called_fundef |
---|
| 2929 | [ 2: #id #tl #ty @I |
---|
| 2930 | | 1: #called_function whd |
---|
| 2931 | cut (sss_func_tr = \fst (function_switch_removal sss_func)) |
---|
| 2932 | [ 1: <sss_func_hyp @refl ] #H >H -H |
---|
| 2933 | cut (sss_new_vars = \snd (function_switch_removal sss_func)) |
---|
| 2934 | [ 1: <sss_func_hyp @refl ] #H >H -H |
---|
| 2935 | @(swc_call … sss_k_hyp) try assumption |
---|
| 2936 | <sss_func_hyp @refl ] |
---|
| 2937 | | 2: #ret_expr #Hexec_ret_expr |
---|
| 2938 | cases (bindIO_inversion ??????? Hexec_ret_expr) #xret * #Heq_ret |
---|
| 2939 | whd in ⊢ ((??%%) → (??%%)); #H destruct (H) |
---|
| 2940 | >(exec_lvalue_sim_aux … Hsim_lvalue … Heq_ret) |
---|
| 2941 | whd in ⊢ (??%?); whd @conj try @refl |
---|
| 2942 | cut (sss_func_tr = \fst (function_switch_removal sss_func)) |
---|
| 2943 | [ 1: <sss_func_hyp @refl ] #H >H -H |
---|
| 2944 | @(sws_callstate … sss_writeable … sss_mem_hyp) |
---|
| 2945 | cases called_fundef |
---|
| 2946 | [ 2: #id #tl #ty @I |
---|
| 2947 | | 1: #called_function whd |
---|
| 2948 | cut (sss_func_tr = \fst (function_switch_removal sss_func)) |
---|
| 2949 | [ 1: <sss_func_hyp @refl ] #H >H -H |
---|
| 2950 | cut (sss_new_vars = \snd (function_switch_removal sss_func)) |
---|
| 2951 | [ 1: <sss_func_hyp @refl ] #H >H -H |
---|
| 2952 | @(swc_call … sss_k_hyp) try assumption |
---|
| 2953 | <sss_func_hyp @refl ] ] |
---|
| 2954 | | 4: (* Sequence statement *) |
---|
| 2955 | #Hexec %{0} whd in sss_result_hyp:(??%?); whd whd in Hexec:(??%?) ⊢ (??%?); destruct (Hexec) |
---|
| 2956 | >sss_result_proj <sss_result_hyp |
---|
| 2957 | cases (switch_removal_elim stm1 sss_lu) #stm1' * #fvs1' * #u' #HeqA >HeqA normalize nodelta |
---|
| 2958 | cases (switch_removal_elim stm2 u') #stm2' * #fvs2' * #u'' #HeqB >HeqB normalize nodelta |
---|
[2441] | 2959 | normalize @conj try @refl %1{sss_lu … sss_func_hyp … sss_writeable … sss_mem_hyp … HeqA} |
---|
| 2960 | try // try assumption |
---|
[2438] | 2961 | [ 1: lapply (fresh_to_substatements … sss_lu_fresh) normalize * // |
---|
| 2962 | | 2: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta >HeqB normalize nodelta |
---|
| 2963 | /2 by All_append_l/ |
---|
| 2964 | | 4: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ] |
---|
| 2965 | @(swc_seq … u') try // |
---|
| 2966 | [ 2: >HeqB @refl |
---|
| 2967 | | 1: lapply (fresh_to_substatements … sss_lu_fresh) normalize * #_ @fresher_for_univ |
---|
| 2968 | lapply (switch_removal_fte stm1 sss_lu) >HeqA #H @H |
---|
| 2969 | | 3: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta >HeqB normalize nodelta |
---|
| 2970 | /2 by All_append_r/ |
---|
| 2971 | ] |
---|
| 2972 | | 5: (* If-then-else *) |
---|
| 2973 | #Hexec %{0} whd in sss_result_hyp:(??%?) Hexec:(??%?); >sss_result_proj <sss_result_hyp |
---|
| 2974 | cases (switch_removal_elim iftrue sss_lu) #iftrue' * #fvs1' * #u' #HeqA >HeqA normalize nodelta |
---|
| 2975 | cases (switch_removal_elim iffalse u') #iffalse' * #fvs2' * #u'' #HeqB >HeqB normalize nodelta |
---|
| 2976 | whd whd in ⊢ (??%?); |
---|
| 2977 | cases (bindIO_inversion ??????? Hexec) #condres * #Heq_cond #Hexec_cond |
---|
| 2978 | cases (bindIO_inversion ??????? Hexec_cond) #b * #Heq_bool #Hresult |
---|
| 2979 | whd in Hresult:(??%%); destruct (Hresult) |
---|
| 2980 | >(Hsim_expr … Heq_cond) >bindIO_Value |
---|
| 2981 | >Heq_bool whd in match (m_bind ?????); whd @conj try @refl |
---|
| 2982 | cases b normalize nodelta |
---|
| 2983 | [ 1: %1{sss_lu … sss_func_hyp … sss_writeable … sss_mem_hyp … HeqA} try assumption try // |
---|
| 2984 | [ 1: cases (fresh_to_substatements … sss_lu_fresh) normalize // |
---|
| 2985 | | 2: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta >HeqB normalize nodelta |
---|
| 2986 | /2 by All_append_l/ |
---|
| 2987 | | 3: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ] |
---|
| 2988 | | 2: %1{u' … sss_func_hyp … sss_writeable … sss_mem_hyp … HeqB} try assumption try // |
---|
| 2989 | [ 1: cases (fresh_to_substatements … sss_lu_fresh) normalize #_ |
---|
| 2990 | @fresher_for_univ lapply (switch_removal_fte iftrue sss_lu) >HeqA #H @H |
---|
| 2991 | | 2: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta >HeqB normalize nodelta |
---|
| 2992 | /2 by All_append_r/ |
---|
| 2993 | | 3: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ] ] |
---|
| 2994 | | 6: (* While loop *) |
---|
| 2995 | #Hexec %{0} whd in sss_result_hyp:(??%?) Hexec:(??%?); >sss_result_proj <sss_result_hyp |
---|
| 2996 | >sss_result_proj <sss_result_hyp whd |
---|
| 2997 | cases (bindIO_inversion ??????? Hexec) #condres * #Heq_cond #Hexec_cond |
---|
| 2998 | cases (bindIO_inversion ??????? Hexec_cond) #b * #Heq_bool whd in ⊢ ((??%%) → ?); |
---|
| 2999 | cases (switch_removal_elim body sss_lu) #body' * #fvs1' * #u' #HeqA >HeqA normalize nodelta |
---|
| 3000 | whd in ⊢ (? → (??%?)); |
---|
| 3001 | >(Hsim_expr … Heq_cond) >bindIO_Value >Heq_bool |
---|
| 3002 | whd in match (m_bind ?????); cases b normalize nodelta #Hresult destruct (Hresult) |
---|
| 3003 | whd @conj try @refl |
---|
| 3004 | [ 1: %1{sss_lu … sss_func_hyp … sss_writeable … sss_mem_hyp … HeqA} try assumption try // |
---|
| 3005 | [ 1: cases (fresh_to_substatements … sss_lu_fresh) normalize // |
---|
| 3006 | | 2: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta #H @H |
---|
| 3007 | | 4: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem |
---|
| 3008 | | 3: @(swc_while … sss_lu) try // |
---|
| 3009 | [ 1: >HeqA @refl |
---|
| 3010 | | 2: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta #H @H ] |
---|
| 3011 | ] |
---|
| 3012 | | 2: %{… sss_func_hyp … (switch_removal Sskip u')} try assumption try // |
---|
| 3013 | [ 1: lapply (switch_removal_fte body sss_lu) >HeqA #Hfte whd in match (ret_u ??) in Hfte; |
---|
| 3014 | @(fresher_for_univ … Hfte) @(fresh_for_Sskip … sss_lu_fresh) |
---|
| 3015 | | 2: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem ] ] |
---|
| 3016 | | 7: (* do while loop *) |
---|
| 3017 | #Hexec %{0} whd in sss_result_hyp:(??%?) Hexec:(??%?); >sss_result_proj <sss_result_hyp |
---|
| 3018 | >sss_result_proj <sss_result_hyp whd destruct (Hexec) whd in ⊢ (??%?); |
---|
| 3019 | cases (switch_removal_elim body sss_lu) #body' * #fvs1' * #u' #HeqA >HeqA normalize nodelta |
---|
| 3020 | whd @conj try @refl |
---|
| 3021 | %1{sss_lu … sss_func_hyp … (switch_removal body sss_lu) } |
---|
| 3022 | try assumption try // |
---|
| 3023 | [ 1: lapply (fresh_to_substatements … sss_lu_fresh) normalize * // |
---|
| 3024 | | 2: >HeqA @refl |
---|
| 3025 | | 3: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta #H @H |
---|
| 3026 | | 5: #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem |
---|
| 3027 | | 4: @(swc_dowhile … sss_lu) try assumption try // |
---|
| 3028 | [ 1: >HeqA @refl |
---|
| 3029 | | 2: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta #H @H |
---|
| 3030 | ] ] |
---|
| 3031 | | 8: (* for loop *) |
---|
| 3032 | #Hexec %{0} whd in sss_result_hyp:(??%?) Hexec:(??%?); >sss_result_proj <sss_result_hyp |
---|
| 3033 | >sss_result_proj <sss_result_hyp whd destruct (Hexec) whd in ⊢ (??%?); |
---|
| 3034 | cases (switch_removal_elim init sss_lu) #init' * #fvs1' * #u' #HeqA >HeqA normalize nodelta |
---|
| 3035 | cases (switch_removal_elim step u') #step' * #fvs2' * #u'' #HeqB >HeqB normalize nodelta |
---|
| 3036 | cases (switch_removal_elim body u'') #body' * #fvs3' * #u''' #HeqC >HeqC normalize nodelta |
---|
| 3037 | lapply Hexec |
---|
| 3038 | @(match is_Sskip init with |
---|
| 3039 | [ inl Heq ⇒ ? |
---|
| 3040 | | inr Hneq ⇒ ? |
---|
| 3041 | ]) normalize nodelta |
---|
| 3042 | [ 2: lapply (simplify_is_not_skip … Hneq sss_lu) >HeqA * #pf |
---|
| 3043 | whd in match (ret_st ??) in ⊢ ((??%%) → ?); #Hneq >Hneq normalize nodelta |
---|
| 3044 | #Hexec' whd in Hexec':(??%%); destruct (Hexec') whd @conj try @refl |
---|
| 3045 | %1{sss_lu … sss_func_hyp (switch_removal init sss_lu)} try assumption try // |
---|
| 3046 | [ 1: lapply (fresh_to_substatements … sss_lu_fresh) normalize * * * // |
---|
| 3047 | | 2: >HeqA @refl |
---|
| 3048 | | 3: lapply sss_incl <sss_result_hyp >HeqA normalize nodelta |
---|
| 3049 | >HeqB normalize nodelta >HeqC normalize nodelta |
---|
| 3050 | /2 by All_append_l/ |
---|
| 3051 | | 4: @(swc_for1 … u') try assumption try // |
---|
| 3052 | [ 1: lapply (fresh_to_substatements … sss_lu_fresh) * * * #HW #HX #HY #HZ |
---|
| 3053 | @for_fresh_lift |
---|
| 3054 | [ 1: @(fresher_for_univ … HY) |
---|
| 3055 | | 2: @(fresher_for_univ … HZ) |
---|
| 3056 | | 3: @(fresher_for_univ … HX) ] |
---|
| 3057 | lapply (switch_removal_fte init sss_lu) >HeqA #Hs @Hs |
---|
| 3058 | | 2: normalize >HeqB normalize nodelta >HeqC @refl |
---|
| 3059 | | 3: lapply sss_incl <sss_result_hyp |
---|
| 3060 | whd in match (ret_vars ??) in ⊢ (% → %); |
---|
| 3061 | whd in match (switch_removal ??) in ⊢ (% → %); |
---|
| 3062 | >HeqA normalize nodelta >HeqB normalize nodelta >HeqC |
---|
| 3063 | normalize nodelta #H /2 by All_append_r/ |
---|
| 3064 | ] ] |
---|
| 3065 | | 1: -Hexec #Hexec' cases (bindIO_inversion ??????? Hexec') #condres * #Heq_cond #Hexec_cond |
---|
| 3066 | cases (bindIO_inversion ??????? Hexec_cond) #b * #Heq_bool |
---|
| 3067 | destruct (Heq) normalize in HeqA; lapply HeqA #HeqA' destruct (HeqA') |
---|
| 3068 | normalize nodelta |
---|
| 3069 | >(Hsim_expr … Heq_cond) whd in ⊢ ((??%?) → ?); #Hexec' |
---|
| 3070 | whd in match (m_bind ?????); >Heq_bool |
---|
| 3071 | cases b in Hexec'; normalize nodelta whd in match (bindIO ??????); |
---|
| 3072 | normalize #Hexec'' destruct (Hexec'') @conj try @refl |
---|
| 3073 | [ 1: %1{u'' … sss_func_hyp (switch_removal body u'')} try assumption try // |
---|
| 3074 | [ 1: lapply (fresh_to_substatements … sss_lu_fresh) * * * #_ #_ #_ |
---|
| 3075 | @fresher_for_univ lapply (switch_removal_fte step u') >HeqB |
---|
| 3076 | #H @H |
---|
| 3077 | | 2: >HeqC @refl |
---|
| 3078 | | 3: lapply sss_incl <sss_result_hyp |
---|
| 3079 | whd in match (ret_vars ??) in ⊢ (% → %); |
---|
| 3080 | whd in match (switch_removal ??) in ⊢ (% → %); normalize nodelta |
---|
| 3081 | >HeqB normalize nodelta >HeqC normalize nodelta |
---|
| 3082 | /2 by All_append_r/ |
---|
| 3083 | | 4: @(swc_for2 … u') try assumption |
---|
| 3084 | [ 1: >HeqB @refl |
---|
| 3085 | | 2: >HeqB >HeqC @refl |
---|
| 3086 | | 3: lapply sss_incl <sss_result_hyp |
---|
| 3087 | whd in match (ret_vars ??) in ⊢ (% → %); |
---|
| 3088 | whd in match (switch_removal ??) in ⊢ (% → %); normalize nodelta |
---|
| 3089 | >HeqB normalize nodelta >HeqC normalize nodelta #H @H |
---|
| 3090 | ] |
---|
| 3091 | ] |
---|
| 3092 | | 2: %1{u' … sss_func_hyp … (switch_removal Sskip u')} try assumption try // |
---|
| 3093 | [ 1: @(fresh_for_Sskip … sss_lu_fresh) ] ] ] |
---|
| 3094 | #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem |
---|
| 3095 | | 9: (* break *) |
---|
[2448] | 3096 | (* sss_enclosing_label TODO : switch case *) |
---|
[2438] | 3097 | #Hexec %{0} whd whd in sss_result_hyp:(??%?); >sss_result_proj <sss_result_hyp normalize nodelta |
---|
| 3098 | lapply Hexec -Hexec |
---|
| 3099 | inversion sss_k_hyp |
---|
| 3100 | [ 1: #new_vars #Hv #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Habsurd destruct (Habsurd) |
---|
| 3101 | | 2: #sk #sss_k' #sss_k_ext' #uk #sk' #new_vars #Hfresh_suk #Hsimk' #Hsk_eq' #Hincl #_ #Hnew_vars_eq |
---|
| 3102 | #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) whd @conj try @refl |
---|
| 3103 | destruct |
---|
| 3104 | %1{sss_lu … (switch_removal Sbreak sss_lu)} try assumption try // |
---|
| 3105 | | 3,4: #e #sk #sss_k' #sss_k_ext' #uk #sk' #new_vars #Hfresh_suk #Hsimk' #Hsk_eq' #Hincl #_ |
---|
| 3106 | #Hnew_vars #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) whd @conj try @refl |
---|
| 3107 | destruct |
---|
| 3108 | %1{sss_lu … (switch_removal Sskip sss_lu)} try assumption try // |
---|
| 3109 | | 5: #e #s1k #s2k #sss_k' #sss_k_ext' #uk #sk' #new_vars #Hfresh_suk #Hsimk' #Hsk_eq' #Hincl #_ |
---|
| 3110 | #Hnew_vars #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) whd @conj try @refl |
---|
| 3111 | destruct |
---|
| 3112 | %1{sss_lu … (switch_removal Sbreak sss_lu)} try assumption try // |
---|
| 3113 | | 6,7: #e #s1k #s2k #sss_k' #sss_k_ext' #uk #result1 #result2 #new_vars #Hfresh_suk #Hsimk' |
---|
| 3114 | #Hres1 #Hres2 #Hincl #_ #Hnew_vars |
---|
| 3115 | #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) whd @conj try @refl |
---|
| 3116 | destruct |
---|
| 3117 | %1{sss_lu … (switch_removal Sskip sss_lu)} try assumption try // |
---|
| 3118 | | 8: #sss_k' #sss_k_ext' #new_vars #Hsimk' #_ #Hnew_vars #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); |
---|
| 3119 | #Heq destruct (Heq) whd @conj try @refl destruct |
---|
| 3120 | %1{sss_lu … (switch_removal Sskip sss_lu)} try assumption try // |
---|
| 3121 | | 9: #enk #enk' #rk #fk #sss_k' #sss_k_ext' #old_vars #new_vars #Hsimk' #Hold #Hdisjoint #_ |
---|
| 3122 | #Hnew_vars #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); |
---|
| 3123 | #Heq destruct (Heq) ] |
---|
| 3124 | #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem |
---|
| 3125 | | 10: (* continue *) |
---|
| 3126 | #Hexec %{0} whd whd in sss_result_hyp:(??%?); >sss_result_proj <sss_result_hyp normalize nodelta |
---|
| 3127 | lapply Hexec -Hexec |
---|
| 3128 | inversion sss_k_hyp |
---|
| 3129 | [ 1: #new_vars #Hv #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Habsurd destruct (Habsurd) |
---|
| 3130 | | 2: #sk #sss_k' #sss_k_ext' #uk #sk' #new_vars #Hfresh_suk #Hsimk' #Hsk_eq' #Hincl #_ #Hnew_vars_eq |
---|
| 3131 | #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) whd @conj try @refl |
---|
| 3132 | destruct |
---|
| 3133 | %1{sss_lu … (switch_removal Scontinue sss_lu)} try assumption try // |
---|
| 3134 | | 3: #ek #sk #sss_k' #sss_k_ext' #uk #sk' #new_vars #Hfresh_suk #Hsimk' #Hsk_eq' #Hincl #_ |
---|
| 3135 | #Hnew_vars #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) whd @conj try @refl |
---|
| 3136 | destruct |
---|
| 3137 | %1{uk … (switch_removal (Swhile ek sk) uk)} try assumption try // |
---|
| 3138 | [ 1: normalize cases (switch_removal sk uk) * #sk' #fvs' #uk' @refl |
---|
| 3139 | | 2: whd in match (switch_removal ??); lapply Hincl |
---|
| 3140 | cases (switch_removal sk uk) * #body' #fvs' #uk' |
---|
| 3141 | /2 by All_append_r/ ] |
---|
| 3142 | | 4: #ek #sk #sss_k' #sss_k_ext' #uk #sk' #new_vars #Hfresh_suk #Hsimk' #Hsk_eq' #Hincl #_ |
---|
| 3143 | #Hnew_vars_eq #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Hexec |
---|
| 3144 | cases (bindIO_inversion ??????? Hexec) #condres * #Heq_cond #Hexec_cond |
---|
| 3145 | cases (bindIO_inversion ??????? Hexec_cond) #b * #Heq_bool #Hexec_bool |
---|
| 3146 | >(Hsim_expr … Heq_cond) >bindIO_Value >Heq_bool whd in match (m_bind ?????); |
---|
| 3147 | cases b in Hexec_bool; normalize nodelta whd in ⊢ ((??%?) → ?); |
---|
| 3148 | #Heq whd whd in Heq:(??%%); destruct (Heq) @conj try @refl |
---|
| 3149 | [ 1: destruct %1{uk … (switch_removal (Sdowhile ek sk) uk)} try assumption try // |
---|
| 3150 | [ 1: normalize cases (switch_removal sk uk) * #body' #fvs' #uk' @refl |
---|
| 3151 | | 2: whd in match (switch_removal ??); lapply Hincl cases (switch_removal sk uk) |
---|
| 3152 | * #body' #fvs' #uk' #H @H |
---|
| 3153 | ] |
---|
| 3154 | | 2: destruct %1{uk … (switch_removal Sskip uk)} try assumption try // |
---|
| 3155 | try @(fresh_for_Sskip … Hfresh_suk) ] |
---|
| 3156 | | 5: #e #s1k #s2k #sss_k' #sss_k_ext' #uk #sk' #new_vars #Hfresh_suk #Hsimk' #Hsk_eq' #Hincl #_ |
---|
| 3157 | #Hnew_vars #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) whd @conj try @refl |
---|
| 3158 | destruct %1{sss_lu … (switch_removal Scontinue sss_lu)} try assumption try // |
---|
| 3159 | | 6,7: #e #s1k #s2k #sss_k' #sss_k_ext' #uk #result1 #result2 #new_vars #Hfresh_suk #Hsimk' #Hres1 #Hres2 #Hincl #_ |
---|
| 3160 | #Hnew_vars #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) whd @conj try @refl |
---|
| 3161 | destruct %1{uk … (switch_removal s1k uk)} try assumption try // |
---|
| 3162 | [ 1: cases (fresh_to_substatements … Hfresh_suk) * * // |
---|
| 3163 | | 2: lapply Hincl whd in match (ret_vars ??) in ⊢ (% → ?); |
---|
| 3164 | whd in match (switch_removal ??); |
---|
| 3165 | cases (switch_removal s1k uk) * #s1k' #fvs1' #uk' normalize nodelta |
---|
| 3166 | cases (switch_removal s2k uk') * #s2k' #fvs2' #uk'' normalize nodelta |
---|
| 3167 | /2 by All_append_l/ |
---|
| 3168 | | 3: @(swc_for3 … uk) try assumption try // |
---|
| 3169 | ] |
---|
| 3170 | | 8: #sss_k' #sss_k_ext' #new_vars #Hsimk #_ #Hnew_vars_eq #Hk #Hk' #_ |
---|
| 3171 | whd in ⊢ ((??%?) → (??%?)); #Heq destruct (Heq) |
---|
| 3172 | whd @conj try @refl destruct |
---|
| 3173 | %1{sss_lu … (switch_removal Scontinue sss_lu)} try assumption try // |
---|
| 3174 | | 9: #enk #enk' #rk #fk #sss_k' #sss_k_ext' #old_vars #new_vars #Hsimk' #Hold_vars_eq #Hdisjoint |
---|
| 3175 | #_ #Hnew_vars_eq #Hk #Hk' #_ whd in ⊢ ((??%?) → (??%?)); |
---|
| 3176 | #Heq destruct (Heq) ] |
---|
| 3177 | #id #Hmem <(rg_find_symbol … Hrelated) @Hext_fresh_for_ge @Hmem |
---|
| 3178 | | 11: (* return *) |
---|
| 3179 | #Hexec %{0} whd whd in sss_result_hyp:(??%?) Hexec:(??%?); lapply Hexec -Hexec |
---|
| 3180 | >sss_result_proj <sss_result_hyp normalize nodelta |
---|
| 3181 | cases retval in sss_lu_fresh sss_result_hyp; normalize nodelta |
---|
| 3182 | [ 1: #sss_lu_fresh #sss_result_hyp whd in ⊢ (? → (??%?)); |
---|
| 3183 | >(prod_eq_lproj ????? sss_func_hyp) |
---|
| 3184 | >fn_return_simplify |
---|
| 3185 | cases (fn_return sss_func) normalize nodelta |
---|
[2468] | 3186 | [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain |
---|
| 3187 | | #structname #fieldspec | #unionname #fieldspec | #id ] |
---|
[2438] | 3188 | [ 1: whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) whd @conj try @refl |
---|
| 3189 | /3 by sws_returnstate, call_cont_swremoval, memext_free_extended_environment, memory_ext_writeable_eq/ |
---|
| 3190 | | *: #Habsurd destruct (Habsurd) ] |
---|
| 3191 | | 2: #ret_expr #sss_lu_fresh #sss_result_hyp whd in ⊢ (? → (??%?)); |
---|
| 3192 | >(prod_eq_lproj ????? sss_func_hyp) |
---|
| 3193 | >fn_return_simplify |
---|
| 3194 | @(match type_eq_dec (fn_return sss_func) Tvoid with |
---|
| 3195 | [ inl H ⇒ ? |
---|
| 3196 | | inr H ⇒ ? ]) normalize nodelta |
---|
| 3197 | [ 1: #Habsurd destruct (Habsurd) |
---|
| 3198 | | 2: #Hexec |
---|
| 3199 | cases (bindIO_inversion ??????? Hexec) #retres * #Heq_ret #Hexec_ret |
---|
| 3200 | whd in Hexec_ret:(??%%); destruct (Hexec_ret) |
---|
| 3201 | >(Hsim_expr … Heq_ret) whd in match (m_bind ?????); whd |
---|
| 3202 | @conj try @refl |
---|
| 3203 | /3 by sws_returnstate, call_cont_swremoval, memext_free_extended_environment, memory_ext_writeable_eq/ |
---|
| 3204 | ] ] |
---|
| 3205 | | 12: (* switch ! at long last *) |
---|
| 3206 | #Hexec whd in sss_result_hyp:(??%?) Hexec:(??%?); lapply Hexec -Hexec |
---|
| 3207 | >sss_result_proj <sss_result_hyp normalize nodelta #Hexec |
---|
[2441] | 3208 | cases (bindIO_inversion ??????? Hexec) * #condval #condtrace -Hexec |
---|
[2438] | 3209 | cases condval normalize nodelta |
---|
| 3210 | [ 1: * #_ #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
[2468] | 3211 | | 3: * #_ #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
| 3212 | | 4: #ptr * #_ #Habsurd normalize in Habsurd; destruct (Habsurd) ] |
---|
[2441] | 3213 | #sz #i * #Hexec_eq #Heq |
---|
| 3214 | cut (∃sg. typeof cond = Tint sz sg) whd in Heq:(??%%); destruct (Heq) |
---|
| 3215 | [ 1: cases (typeof cond) in Heq; normalize nodelta |
---|
[2468] | 3216 | [ | #sz' #sg' | #ptrty | #arrayty #arraysz | #domain #codomain |
---|
| 3217 | | #structname #fieldspec | #unionname #fieldspec | #id ] |
---|
[2441] | 3218 | [ 2: cases (sz_eq_dec ??) normalize nodelta #H |
---|
| 3219 | [ 2: #Habsurd destruct |
---|
| 3220 | | 1: destruct (H) #_ %{sg'} try @refl ] |
---|
| 3221 | | *: #Habsurd destruct (Habsurd) ] ] |
---|
| 3222 | * #sg #Htypeof_cond >Htypeof_cond in Heq; normalize nodelta >sz_eq_identity normalize nodelta |
---|
| 3223 | #Heq whd in Heq:(??%%); |
---|
| 3224 | cases (bindIO_inversion ??????? Heq) #switchcases_truncated * #Heq1 #Heq2 -Heq |
---|
| 3225 | whd in Heq1:(??%%); whd in Heq2:(??%%); |
---|
| 3226 | cut (select_switch sz i switchcases = Some ? switchcases_truncated) |
---|
| 3227 | [ 1: cases (select_switch sz i switchcases) in Heq1; normalize nodelta |
---|
| 3228 | [ 1: #Habsurd destruct | 2: #ls #Heq destruct (Heq) @refl ] ] |
---|
| 3229 | -Heq1 #Heq_select_switch destruct (Heq2) |
---|
[2438] | 3230 | cases (switch_removal_branches_elim … switchcases sss_lu) #switchcases' * #fvs' * #u' #Hbranch_eq |
---|
| 3231 | >Hbranch_eq normalize nodelta |
---|
| 3232 | cases (fresh_elim … u') #new * #u'' #Hfresh_eq >Hfresh_eq normalize nodelta |
---|
[2441] | 3233 | cases (simplify_switch_elim (Expr (Evar new) (Tint sz sg)) switchcases' u'') #simplified * #u''' |
---|
[2438] | 3234 | #Hswitch_eq >Hswitch_eq normalize nodelta |
---|
[2448] | 3235 | %{2} whd whd in ⊢ (??%?); |
---|
[2438] | 3236 | (* A. Execute lhs of assign, i.e. fresh variable that will hold value of condition *) |
---|
| 3237 | whd in match (exec_lvalue ????); |
---|
| 3238 | (* show that the resulting ident is in the memory extension and that the lookup succeeds *) |
---|
[2441] | 3239 | >Hbranch_eq in sss_result_hyp; normalize nodelta |
---|
| 3240 | >Hfresh_eq normalize nodelta >Hswitch_eq normalize nodelta >Htypeof_cond >Hswitch_eq |
---|
| 3241 | normalize nodelta #sss_result_hyp |
---|
[2438] | 3242 | <sss_result_hyp in sss_incl; whd in match (ret_vars ??); #sss_incl |
---|
| 3243 | cases sss_env_hyp * |
---|
| 3244 | #Hlookup_new_in_old |
---|
| 3245 | #Hlookup_new_in_new |
---|
| 3246 | #Hlookup_old |
---|
[2448] | 3247 | cut (mem_assoc_env new sss_new_vars=true) |
---|
[2441] | 3248 | [ 1: cases sss_incl #Hmem #_ elim sss_new_vars in Hmem; |
---|
[2438] | 3249 | [ 1: @False_ind |
---|
| 3250 | | 2: * #hdv #hdty #tl #Hind whd in ⊢ (% → (??%?)); * |
---|
| 3251 | [ 1: #Heq destruct (Heq) |
---|
| 3252 | cases (identifier_eq_i_i … hdv) #Hrefl #Heq >Heq -Heq normalize nodelta |
---|
| 3253 | @refl |
---|
| 3254 | | 2: #Hmem lapply (Hind Hmem) #Hmem_in_tl |
---|
| 3255 | cases (identifier_eq ? new hdv) normalize nodelta |
---|
| 3256 | [ 1: #_ @refl | 2: #_ @Hmem_in_tl ] ] ] ] |
---|
[2448] | 3257 | #Hnew_in_new_vars |
---|
| 3258 | lapply (Hlookup_new_in_new new Hnew_in_new_vars) |
---|
[2438] | 3259 | * #res #Hlookup >Hlookup normalize nodelta whd in match (bindIO ??????); |
---|
| 3260 | (* B. Reduce rhs of assign, i.e. the condition. Do this using simulation hypothesis. *) |
---|
| 3261 | >(Hsim_expr … Hexec_eq) >bindIO_Value |
---|
| 3262 | (* C. Execute assign. We must prove that this cannot fail. In order for the proof to proceed, we need |
---|
| 3263 | to set up things so that loading from that fresh location will yield exactly the stored value. *) |
---|
| 3264 | normalize in match store_value_of_type'; normalize nodelta |
---|
[2441] | 3265 | whd in match (typeof ?); |
---|
[2448] | 3266 | lapply (sss_new_alloc 〈new,Tint sz sg〉 ? res Hlookup) |
---|
| 3267 | [ 1: cases sss_incl // ] * * #Hvalid #Hlow #Hhigh |
---|
| 3268 | lapply (store_int_success … i … Hvalid Hlow Hhigh) * #m_ext' #Hstore |
---|
| 3269 | lapply (store_value_load_value_ok … Hstore) // #Hload_value_correct |
---|
| 3270 | >Hstore whd in match (m_bind ?????); whd @conj try // |
---|
| 3271 | cut (mem block res sss_writeable) |
---|
| 3272 | [ 1: @cthulhu ] |
---|
| 3273 | (* lapply (memext_store_value_of_type_writeable … sss_mem_hyp … Hstore) *) |
---|
[2438] | 3274 | @cthulhu |
---|
| 3275 | | *: @cthulhu ] |
---|
| 3276 | | *: @cthulhu ] qed. |
---|