Changeset 2234 for src/Clight/switchRemoval.ma
- Timestamp:
- Jul 23, 2012, 7:31:11 PM (8 years ago)
- File:
-
- 1 edited
-
src/Clight/switchRemoval.ma (modified) (7 diffs)
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/switchRemoval.ma
r2227 r2234 1 1 include "Clight/Csyntax.ma". 2 2 include "Clight/fresh.ma". 3 3 include "basics/lists/list.ma". … … 1311 1311 %{p2} @conj try @refl try assumption 1312 1312 ] qed. 1313 1314 (* A cleaner version of inversion for [value_eq] *) 1315 lemma value_eq_inversion : 1316 ∀E,v1,v2. ∀P : val → val → Prop. value_eq E v1 v2 → 1317 (∀v. P Vundef v) → 1318 (∀sz,i. P (Vint sz i) (Vint sz i)) → 1319 (∀f. P (Vfloat f) (Vfloat f)) → 1320 (P Vnull Vnull) → 1321 (∀p1,p2. pointer_translation p1 E = Some ? p2 → P (Vptr p1) (Vptr p2)) → 1322 P v1 v2. 1323 #E #v1 #v2 #P #Heq #H1 #H2 #H3 #H4 #H5 1324 inversion Heq 1325 [ 1: #v #Hv1 #Hv2 #_ destruct @H1 1326 | 2: #sz #i #Hv1 #Hv2 #_ destruct @H2 1327 | 3: #f #Hv1 #Hv2 #_ destruct @H3 1328 | 4: #Hv1 #Hv2 #_ destruct @H4 1329 | 5: #p1 #p2 #Hembed #Hv1 #Hv2 #_ destruct @H5 // ] qed. 1313 1330 1314 1331 (* If we succeed to load something by value from a 〈b,off〉 location, … … 1318 1335 access_mode ty = By_value (typ_of_type ty) → 1319 1336 load_value_of_type ty m b off = Some ? v → 1320 Zltb (block_id b) (nextblock m) = true. (* → valid_block m b *)1321 #ty #m * #brg #bid #off #v whd in match (valid_block ??);1337 Zltb (block_id b) (nextblock m) = true. 1338 #ty #m * #brg #bid #off #v 1322 1339 cases ty 1323 1340 [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain … … 1335 1352 ] qed. 1336 1353 1354 (* If we succeed in loading some data from a location, then this loc is a valid pointer. *) 1355 lemma load_by_value_success_valid_ptr_aux : 1356 ∀ty,m,b,off,v. 1357 access_mode ty = By_value (typ_of_type ty) → 1358 load_value_of_type ty m b off = Some ? v → 1359 Zltb (block_id b) (nextblock m) = true ∧ 1360 Zleb (low_bound m b) (offv off) = true ∧ 1361 Zltb (offv off) (high_bound m b) = true. 1362 #ty #m * #brg #bid #off #v 1363 cases ty 1364 [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain 1365 | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ] 1366 whd in match (load_value_of_type ????); 1367 [ 1,7,8: #_ #Habsurd destruct (Habsurd) ] 1368 #Hmode 1369 [ 1,2,3,6: [ 1: elim sz | 2: elim fsz ] 1370 normalize in match (typesize ?); 1371 whd in match (loadn ???); 1372 whd in match (beloadv ??); 1373 cases (Zltb bid (nextblock m)) normalize nodelta 1374 cases (Zleb (low (blocks m (mk_block brg bid))) (offv off)) 1375 cases (Zleb (low (blocks m (mk_block brg bid))) (offv off)) 1376 cases (Zltb (offv off) (high (blocks m (mk_block brg bid)))) normalize nodelta 1377 #Heq destruct (Heq) 1378 try /3 by conj, refl/ 1379 | *: normalize in Hmode; destruct (Hmode) 1380 ] qed. 1381 1337 1382 1338 1383 lemma valid_block_from_bool : ∀b,m. Zltb (block_id b) (nextblock m) = true → valid_block m b. … … 1351 1396 #ty #m #b #off #v #Haccess_mode #Hload 1352 1397 @valid_block_from_bool 1353 @(load_by_value_success_valid_block_aux ty m b off v Haccess_mode Hload) 1354 qed. 1398 elim (load_by_value_success_valid_ptr_aux ty m b off v Haccess_mode Hload) * // 1399 qed. 1400 1401 lemma load_by_value_success_valid_pointer : 1402 ∀ty,m,b,off,v. 1403 access_mode ty = By_value (typ_of_type ty) → 1404 load_value_of_type ty m b off = Some ? v → 1405 valid_pointer m (mk_pointer b off). 1406 #ty #m #b #off #v #Haccess_mode #Hload normalize 1407 elim (load_by_value_success_valid_ptr_aux ty m b off v Haccess_mode Hload) 1408 * #H1 #H2 #H3 >H1 >H2 normalize nodelta 1409 >Zle_to_Zleb_true try // 1410 lapply (Zlt_to_Zle … (Zltb_true_to_Zlt … H3)) /2/ 1411 qed. 1412 1355 1413 1356 1414 (* Making explicit the contents of memory_inj for load_value_of_type *) … … 2196 2254 qed. 2197 2255 2198 (* A cleaner version of inversion for [value_eq] *)2199 lemma value_eq_inversion :2200 ∀E,v1,v2. ∀P : val → val → Prop. value_eq E v1 v2 →2201 (∀v. P Vundef v) →2202 (∀sz,i. P (Vint sz i) (Vint sz i)) →2203 (∀f. P (Vfloat f) (Vfloat f)) →2204 (P Vnull Vnull) →2205 (∀p1,p2. pointer_translation p1 E = Some ? p2 → P (Vptr p1) (Vptr p2)) →2206 P v1 v2.2207 #E #v1 #v2 #P #Heq #H1 #H2 #H3 #H4 #H52208 inversion Heq2209 [ 1: #v #Hv1 #Hv2 #_ destruct @H12210 | 2: #sz #i #Hv1 #Hv2 #_ destruct @H22211 | 3: #f #Hv1 #Hv2 #_ destruct @H32212 | 4: #Hv1 #Hv2 #_ destruct @H42213 | 5: #p1 #p2 #Hembed #Hv1 #Hv2 #_ destruct @H5 // ] qed.2214 2256 2215 2257 (* value_eq lifts to addition *) 2216 2258 lemma add_value_eq : 2217 ∀E,v1,v2,v1',v2',ty1,ty2 ,m1,m2.2259 ∀E,v1,v2,v1',v2',ty1,ty2. 2218 2260 value_eq E v1 v2 → 2219 2261 value_eq E v1' v2' → 2220 memory_inj E m1 m2 → (*This injection seems useless TODO *)2262 (* memory_inj E m1 m2 → This injection seems useless TODO *) 2221 2263 ∀r1. (sem_add v1 ty1 v1' ty2=Some val r1→ 2222 2264 ∃r2:val.sem_add v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2). 2223 #E #v1 #v2 #v1' #v2' #ty1 #ty2 # m1 #m2 #Hvalue_eq1 #Hvalue_eq2 #Hinj#r12265 #E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1 2224 2266 @(value_eq_inversion E … Hvalue_eq1) 2225 2267 [ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ] … … 2292 2334 ] 2293 2335 ] qed. 2294 2295 (* TODO all other 10 binary operations. Then wrap this in [binary_operation_value_eq] *) 2296 2297 2336 2337 (* Offset subtraction is invariant by translation *) 2338 lemma sub_offset_translation : 2339 ∀n,x,y,delta. sub_offset n x y = sub_offset n (offset_plus x delta) (offset_plus y delta). 2340 #n #x #y #delta 2341 whd in match (sub_offset ???) in ⊢ (??%%); 2342 elim x #x' elim y #y' elim delta #delta' 2343 normalize in match (offset_plus ??); 2344 normalize in match (offset_plus ??); 2345 cut ((x' - y') = (x'+delta'-(y'+delta'))) 2346 [ whd in match (Zminus ??) in ⊢ (??%%); 2347 >(Zopp_Zplus y' delta') <associative_Zplus /2/ ] 2348 #Heq >Heq @refl 2349 qed. 2350 2351 (* value_eq lifts to addition *) 2352 lemma sub_value_eq : 2353 ∀E,v1,v2,v1',v2',ty1,ty2. 2354 value_eq E v1 v2 → 2355 value_eq E v1' v2' → 2356 ∀r1. (sem_sub v1 ty1 v1' ty2=Some val r1→ 2357 ∃r2:val.sem_sub v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2). 2358 #E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1 2359 @(value_eq_inversion E … Hvalue_eq1) 2360 [ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ] 2361 [ 1: whd in match (sem_sub ????); normalize nodelta 2362 cases (classify_sub ty1 ty2) normalize nodelta 2363 [ 1: #sz #sg | 2: #fsz | 3: #n #ty #sz #sg | 4: #n #sz #sg #ty | 5: #ty1' #ty2' ] 2364 #Habsurd destruct (Habsurd) 2365 | 2: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta 2366 cases (classify_sub ty1 ty2) normalize nodelta 2367 [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ] 2368 [ 2,3,5: #Habsurd destruct (Habsurd) ] 2369 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 2370 [ 1,6: #v' | 2,7: #sz' #i' | 3,8: #f' | 4,9: | 5,10: #p1' #p2' #Hembed' ] 2371 [ 1,2,4,5,6,7,8,9,10: #Habsurd destruct (Habsurd) ] 2372 @intsize_eq_elim_elim 2373 [ 1: #_ #Habsurd destruct (Habsurd) 2374 | 2: #Heq destruct (Heq) normalize nodelta 2375 #Heq destruct (Heq) 2376 /3 by ex_intro, conj, vint_eq/ 2377 ] 2378 | 3: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta 2379 cases (classify_sub ty1 ty2) normalize nodelta 2380 [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ] 2381 [ 1,3,4,5: #Habsurd destruct (Habsurd) ] 2382 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 2383 [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ] 2384 [ 1,2,4,5: #Habsurd destruct (Habsurd) ] 2385 #Heq destruct (Heq) 2386 /3 by ex_intro, conj, vfloat_eq/ 2387 | 4: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta 2388 cases (classify_sub ty1 ty2) normalize nodelta 2389 [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ] 2390 [ 1,2,5: #Habsurd destruct (Habsurd) ] 2391 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 2392 [ 1,6: #v' | 2,7: #sz' #i' | 3,8: #f' | 4,9: | 5,10: #p1' #p2' #Hembed' ] 2393 [ 1,2,4,5,6,7,9,10: #Habsurd destruct (Habsurd) ] 2394 [ 1: @eq_bv_elim [ 1: normalize nodelta #Heq1 #Heq2 destruct /3 by ex_intro, conj, vnull_eq/ 2395 | 2: #_ normalize nodelta #Habsurd destruct (Habsurd) ] 2396 | 2: #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/ ] 2397 | 5: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta 2398 cases (classify_sub ty1 ty2) normalize nodelta 2399 [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ] 2400 [ 1,2,5: #Habsurd destruct (Habsurd) ] 2401 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 2402 [ 1,6: #v' | 2,7: #sz' #i' | 3,8: #f' | 4,9: | 5,10: #p1' #p2' #Hembed' ] 2403 [ 1,2,4,5,6,7,8,9: #Habsurd destruct (Habsurd) ] 2404 #Heq destruct (Heq) 2405 [ 1: %{(Vptr (neg_shift_pointer_n (bitsize_of_intsize sz') p2 (sizeof ty) i'))} @conj try @refl 2406 @vptr_eq whd in match (pointer_translation ??) in Hembed ⊢ %; 2407 elim p1 in Hembed; #b1 #o1 normalize nodelta 2408 cases (E b1) 2409 [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) 2410 | 2: * #block #offset normalize nodelta #Heq destruct (Heq) 2411 normalize >(sym_Zplus ? (offv offset)) <associative_Zplus >(sym_Zplus ? (offv offset)) 2412 @refl 2413 ] 2414 | 2: lapply Heq @eq_block_elim 2415 [ 2: #_ normalize nodelta #Habsurd destruct (Habsurd) 2416 | 1: #Hpblock1_eq normalize nodelta 2417 elim p1 in Hpblock1_eq Hembed Hembed'; #b1 #off1 2418 elim p1' #b1' #off1' whd in ⊢ (% → % → ?); #Hpblock1_eq destruct (Hpblock1_eq) 2419 whd in ⊢ ((??%?) → (??%?) → ?); 2420 cases (E b1') normalize nodelta 2421 [ 1: #Habsurd destruct (Habsurd) ] 2422 * #dest_block #dest_off normalize nodelta 2423 #Heq_ptr1 #Heq_ptr2 destruct >eq_block_identity normalize nodelta 2424 cases (eqb (sizeof tsg) O) normalize nodelta 2425 [ 1: #Habsurd destruct (Habsurd) 2426 | 2: >(sub_offset_translation 32 off1 off1' dest_off) 2427 cases (division_u 31 2428 (sub_offset 32 (offset_plus off1 dest_off) (offset_plus off1' dest_off)) 2429 (repr (sizeof tsg))) 2430 [ 1: normalize nodelta #Habsurd destruct (Habsurd) 2431 | 2: #r1' normalize nodelta #Heq2 destruct (Heq2) 2432 /3 by ex_intro, conj, vint_eq/ ] 2433 ] ] ] 2434 ] qed. 2435 2436 2437 lemma mul_value_eq : 2438 ∀E,v1,v2,v1',v2',ty1,ty2. 2439 value_eq E v1 v2 → 2440 value_eq E v1' v2' → 2441 ∀r1. (sem_mul v1 ty1 v1' ty2=Some val r1→ 2442 ∃r2:val.sem_mul v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2). 2443 #E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1 2444 @(value_eq_inversion E … Hvalue_eq1) 2445 [ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ] 2446 [ 1: whd in match (sem_mul ????); normalize nodelta 2447 cases (classify_aop ty1 ty2) normalize nodelta 2448 [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ] 2449 #Habsurd destruct (Habsurd) 2450 | 2: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta 2451 cases (classify_aop ty1 ty2) normalize nodelta 2452 [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ] 2453 [ 2,3: #Habsurd destruct (Habsurd) ] 2454 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 2455 [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ] 2456 [ 1,3,4,5: #Habsurd destruct (Habsurd) ] 2457 @intsize_eq_elim_elim 2458 [ 1: #_ #Habsurd destruct (Habsurd) 2459 | 2: #Heq destruct (Heq) normalize nodelta 2460 #Heq destruct (Heq) 2461 /3 by ex_intro, conj, vint_eq/ 2462 ] 2463 | 3: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta 2464 cases (classify_aop ty1 ty2) normalize nodelta 2465 [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ] 2466 [ 1,3: #Habsurd destruct (Habsurd) ] 2467 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 2468 [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ] 2469 [ 1,2,4,5: #Habsurd destruct (Habsurd) ] 2470 #Heq destruct (Heq) 2471 /3 by ex_intro, conj, vfloat_eq/ 2472 | 4: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta 2473 cases (classify_aop ty1 ty2) normalize nodelta 2474 [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ] 2475 #Habsurd destruct (Habsurd) 2476 | 5: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta 2477 cases (classify_aop ty1 ty2) normalize nodelta 2478 [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ] 2479 #Habsurd destruct (Habsurd) 2480 ] qed. 2481 2482 lemma div_value_eq : 2483 ∀E,v1,v2,v1',v2',ty1,ty2. 2484 value_eq E v1 v2 → 2485 value_eq E v1' v2' → 2486 ∀r1. (sem_div v1 ty1 v1' ty2=Some val r1→ 2487 ∃r2:val.sem_div v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2). 2488 #E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1 2489 @(value_eq_inversion E … Hvalue_eq1) 2490 [ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ] 2491 [ 1: whd in match (sem_div ????); normalize nodelta 2492 cases (classify_aop ty1 ty2) normalize nodelta 2493 [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ] 2494 #Habsurd destruct (Habsurd) 2495 | 2: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta 2496 cases (classify_aop ty1 ty2) normalize nodelta 2497 [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ] 2498 [ 2,3: #Habsurd destruct (Habsurd) ] 2499 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 2500 [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ] 2501 [ 1,3,4,5: #Habsurd destruct (Habsurd) ] 2502 elim sg normalize nodelta 2503 @intsize_eq_elim_elim 2504 [ 1,3: #_ #Habsurd destruct (Habsurd) 2505 | 2,4: #Heq destruct (Heq) normalize nodelta 2506 @(match (division_s (bitsize_of_intsize sz') i i') with 2507 [ None ⇒ ? 2508 | Some bv' ⇒ ? ]) 2509 [ 1: normalize #Habsurd destruct (Habsurd) 2510 | 2: normalize #Heq destruct (Heq) 2511 /3 by ex_intro, conj, vint_eq/ 2512 | 3,4: elim sz' in i' i; #i' #i 2513 normalize in match (pred_size_intsize ?); 2514 generalize in match division_u; #division_u normalize 2515 @(match (division_u ???) with 2516 [ None ⇒ ? 2517 | Some bv ⇒ ?]) normalize nodelta 2518 #H destruct (H) 2519 /3 by ex_intro, conj, vint_eq/ ] 2520 ] 2521 | 3: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta 2522 cases (classify_aop ty1 ty2) normalize nodelta 2523 [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ] 2524 [ 1,3: #Habsurd destruct (Habsurd) ] 2525 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 2526 [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ] 2527 [ 1,2,4,5: #Habsurd destruct (Habsurd) ] 2528 #Heq destruct (Heq) 2529 /3 by ex_intro, conj, vfloat_eq/ 2530 | 4: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta 2531 cases (classify_aop ty1 ty2) normalize nodelta 2532 [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ] 2533 #Habsurd destruct (Habsurd) 2534 | 5: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta 2535 cases (classify_aop ty1 ty2) normalize nodelta 2536 [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ] 2537 #Habsurd destruct (Habsurd) 2538 ] qed. 2539 2540 lemma mod_value_eq : 2541 ∀E,v1,v2,v1',v2',ty1,ty2. 2542 value_eq E v1 v2 → 2543 value_eq E v1' v2' → 2544 ∀r1. (sem_mod v1 ty1 v1' ty2=Some val r1→ 2545 ∃r2:val.sem_mod v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2). 2546 #E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1 2547 @(value_eq_inversion E … Hvalue_eq1) 2548 [ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ] 2549 [ 1: whd in match (sem_mod ????); normalize nodelta 2550 cases (classify_aop ty1 ty2) normalize nodelta 2551 [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ] 2552 #Habsurd destruct (Habsurd) 2553 | 2: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta 2554 cases (classify_aop ty1 ty2) normalize nodelta 2555 [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ] 2556 [ 2,3: #Habsurd destruct (Habsurd) ] 2557 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 2558 [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ] 2559 [ 1,3,4,5: #Habsurd destruct (Habsurd) ] 2560 elim sg normalize nodelta 2561 @intsize_eq_elim_elim 2562 [ 1,3: #_ #Habsurd destruct (Habsurd) 2563 | 2,4: #Heq destruct (Heq) normalize nodelta 2564 @(match (modulus_s (bitsize_of_intsize sz') i i') with 2565 [ None ⇒ ? 2566 | Some bv' ⇒ ? ]) 2567 [ 1: normalize #Habsurd destruct (Habsurd) 2568 | 2: normalize #Heq destruct (Heq) 2569 /3 by ex_intro, conj, vint_eq/ 2570 | 3,4: elim sz' in i' i; #i' #i 2571 generalize in match modulus_u; #modulus_u normalize 2572 @(match (modulus_u ???) with 2573 [ None ⇒ ? 2574 | Some bv ⇒ ?]) normalize nodelta 2575 #H destruct (H) 2576 /3 by ex_intro, conj, vint_eq/ ] 2577 ] 2578 | 3: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta 2579 cases (classify_aop ty1 ty2) normalize nodelta 2580 [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ] 2581 #Habsurd destruct (Habsurd) 2582 | 4: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta 2583 cases (classify_aop ty1 ty2) normalize nodelta 2584 [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ] 2585 #Habsurd destruct (Habsurd) 2586 | 5: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta 2587 cases (classify_aop ty1 ty2) normalize nodelta 2588 [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ] 2589 #Habsurd destruct (Habsurd) 2590 ] qed. 2591 2592 (* boolean ops *) 2593 lemma and_value_eq : 2594 ∀E,v1,v2,v1',v2'. 2595 value_eq E v1 v2 → 2596 value_eq E v1' v2' → 2597 ∀r1. (sem_and v1 v1'=Some val r1→ 2598 ∃r2:val.sem_and v2 v2'=Some val r2∧value_eq E r1 r2). 2599 #E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1 2600 @(value_eq_inversion E … Hvalue_eq1) 2601 [ 2: #sz #i 2602 @(value_eq_inversion E … Hvalue_eq2) 2603 [ 2: #sz' #i' whd in match (sem_and ??); 2604 @intsize_eq_elim_elim 2605 [ 1: #_ #Habsurd destruct (Habsurd) 2606 | 2: #Heq destruct (Heq) normalize nodelta 2607 #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/ ] 2608 ] ] 2609 normalize in match (sem_and ??); #arg1 destruct 2610 normalize in match (sem_and ??); #arg2 destruct 2611 normalize in match (sem_and ??); #arg3 destruct 2612 normalize in match (sem_and ??); #arg4 destruct 2613 qed. 2614 2615 lemma or_value_eq : 2616 ∀E,v1,v2,v1',v2'. 2617 value_eq E v1 v2 → 2618 value_eq E v1' v2' → 2619 ∀r1. (sem_or v1 v1'=Some val r1→ 2620 ∃r2:val.sem_or v2 v2'=Some val r2∧value_eq E r1 r2). 2621 #E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1 2622 @(value_eq_inversion E … Hvalue_eq1) 2623 [ 2: #sz #i 2624 @(value_eq_inversion E … Hvalue_eq2) 2625 [ 2: #sz' #i' whd in match (sem_or ??); 2626 @intsize_eq_elim_elim 2627 [ 1: #_ #Habsurd destruct (Habsurd) 2628 | 2: #Heq destruct (Heq) normalize nodelta 2629 #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/ ] 2630 ] ] 2631 normalize in match (sem_or ??); #arg1 destruct 2632 normalize in match (sem_or ??); #arg2 destruct 2633 normalize in match (sem_or ??); #arg3 destruct 2634 normalize in match (sem_or ??); #arg4 destruct 2635 qed. 2636 2637 lemma xor_value_eq : 2638 ∀E,v1,v2,v1',v2'. 2639 value_eq E v1 v2 → 2640 value_eq E v1' v2' → 2641 ∀r1. (sem_xor v1 v1'=Some val r1→ 2642 ∃r2:val.sem_xor v2 v2'=Some val r2∧value_eq E r1 r2). 2643 #E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1 2644 @(value_eq_inversion E … Hvalue_eq1) 2645 [ 2: #sz #i 2646 @(value_eq_inversion E … Hvalue_eq2) 2647 [ 2: #sz' #i' whd in match (sem_xor ??); 2648 @intsize_eq_elim_elim 2649 [ 1: #_ #Habsurd destruct (Habsurd) 2650 | 2: #Heq destruct (Heq) normalize nodelta 2651 #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/ ] 2652 ] ] 2653 normalize in match (sem_xor ??); #arg1 destruct 2654 normalize in match (sem_xor ??); #arg2 destruct 2655 normalize in match (sem_xor ??); #arg3 destruct 2656 normalize in match (sem_xor ??); #arg4 destruct 2657 qed. 2658 2659 lemma shl_value_eq : 2660 ∀E,v1,v2,v1',v2'. 2661 value_eq E v1 v2 → 2662 value_eq E v1' v2' → 2663 ∀r1. (sem_shl v1 v1'=Some val r1→ 2664 ∃r2:val.sem_shl v2 v2'=Some val r2∧value_eq E r1 r2). 2665 #E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1 2666 @(value_eq_inversion E … Hvalue_eq1) 2667 [ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ] 2668 [ 2: 2669 @(value_eq_inversion E … Hvalue_eq2) 2670 [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ] 2671 [ 2: whd in match (sem_shl ??); 2672 cases (lt_u ???) normalize nodelta 2673 [ 1: #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/ 2674 | 2: #Habsurd destruct (Habsurd) 2675 ] 2676 | *: whd in match (sem_shl ??); #Habsurd destruct (Habsurd) ] 2677 | *: whd in match (sem_shl ??); #Habsurd destruct (Habsurd) ] 2678 qed. 2679 2680 lemma shr_value_eq : 2681 ∀E,v1,v2,v1',v2',ty,ty'. 2682 value_eq E v1 v2 → 2683 value_eq E v1' v2' → 2684 ∀r1. (sem_shr v1 ty v1' ty'=Some val r1→ 2685 ∃r2:val.sem_shr v2 ty v2' ty'=Some val r2∧value_eq E r1 r2). 2686 #E #v1 #v2 #v1' #v2' #ty #ty' #Hvalue_eq1 #Hvalue_eq2 #r1 2687 @(value_eq_inversion E … Hvalue_eq1) 2688 [ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ] 2689 whd in match (sem_shr ????); whd in match (sem_shr ????); 2690 [ 1: cases (classify_aop ty ty') normalize nodelta 2691 [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ] 2692 #Habsurd destruct (Habsurd) 2693 | 2: cases (classify_aop ty ty') normalize nodelta 2694 [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ] 2695 [ 2,3: #Habsurd destruct (Habsurd) ] 2696 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 2697 [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ] 2698 [ 1,3,4,5: #Habsurd destruct (Habsurd) ] 2699 elim sg normalize nodelta 2700 cases (lt_u ???) normalize nodelta #Heq destruct (Heq) 2701 /3 by ex_intro, conj, refl, vint_eq/ 2702 | 3: cases (classify_aop ty ty') normalize nodelta 2703 [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ] 2704 #Habsurd destruct (Habsurd) 2705 | 4: cases (classify_aop ty ty') normalize nodelta 2706 [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ] 2707 #Habsurd destruct (Habsurd) 2708 | 5: cases (classify_aop ty ty') normalize nodelta 2709 [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ] 2710 #Habsurd destruct (Habsurd) 2711 ] qed. 2712 2713 (* We want to prove that, but we can't since valid_pointers can in fact be one off outside the block, 2714 and [memory_inj] handles only stuff that is loadable (i.e. inside a block). TODO *) 2715 lemma pointer_eq_valid : 2716 ∀E,m,m',p,p'. 2717 memory_inj E m m' → 2718 pointer_translation p E = Some ? p' → 2719 valid_pointer m p → 2720 valid_pointer m' p'. 2721 @cthulhu qed. 2722 2723 2724 lemma sem_cmp_value_eq : 2725 ∀E,v1,v2,v1',v2',ty,ty',m1,m2. 2726 value_eq E v1 v2 → 2727 value_eq E v1' v2' → 2728 memory_inj E m1 m2 → 2729 ∀op,r1. (sem_cmp op v1 ty v1' ty' m1 = Some val r1→ 2730 ∃r2:val.sem_cmp op v2 ty v2' ty' m2 = Some val r2∧value_eq E r1 r2). 2731 #E #v1 #v2 #v1' #v2' #ty #ty' #m1 #m2 #Hvalue_eq1 #Hvalue_eq2 #Hinj #op #r1 2732 cases op whd in match (sem_cmp ??????); whd in match (sem_cmp ??????); 2733 [ 1: 2734 cases (classify_cmp ty ty') normalize nodelta 2735 [ 1: #sz #sg | 2: #n #ty0 | 3: #fsz | 4: #ty0 #ty0' #Habsurd destruct (Habsurd) ] 2736 @(value_eq_inversion E … Hvalue_eq1) 2737 [ 1,6,11: #v | 2,7,12: #sz #i | 3,8,13: #f | 4,9,14: | 5,10,15: #p1 #p2 #Hembed ] 2738 normalize nodelta 2739 [ 1,2,3,5,6,7,8,10,12,13,15: #Habsurd destruct (Habsurd) ] 2740 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 2741 [ 1,6,11,16: #v' | 2,7,12,17: #sz' #i' | 3,8,13,18: #f' | 4,9,14,19: | 5,10,15,20: #p1' #p2' #Hembed' ] 2742 [ 5: elim sg normalize nodelta 2743 @intsize_eq_elim_elim 2744 [ 1,3: #_ #Habsurd destruct (Habsurd) 2745 | 2,4: #Heq destruct (Heq) normalize nodelta 2746 [ 1: cases (cmp_int ????) whd in match (of_bool ?); #Heq destruct (Heq) 2747 | 2: cases (cmpu_int ????) whd in match (of_bool ?); #Heq destruct (Heq) ] 2748 /3 by ex_intro, conj, vint_eq/ ] 2749 | 10: #Heq destruct (Heq) cases (Fcmp Ceq f f') /3 by ex_intro, conj, vint_eq/ 2750 | 15: whd in match (sem_cmp_match ?); #Heq destruct (Heq) 2751 /3 by ex_intro, conj, vint_eq/ 2752 | 16,19: whd in match (sem_cmp_mismatch ?); #Heq destruct (Heq) 2753 /3 by ex_intro, conj, vint_eq/ 2754 | 20: @cthulhu (* relies on [pointer_eq_valid] TODO *) 2755 | *: #Habsurd destruct (Habsurd) ] 2756 | *: @cthulhu ] 2757 qed. 2758 2298 2759 (* Commutation result for binary operators. *) 2299 2760 lemma binary_operation_value_eq :
Note: See TracChangeset
for help on using the changeset viewer.
