 Timestamp:
 Aug 16, 2012, 7:01:18 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/switchRemoval.ma
r2271 r2298 6 6 include "Clight/CexecInd.ma". 7 7 include "Clight/frontend_misc.ma". 8 include "Clight/casts.ma". (* lemmas related to bitvectors ... *) 9 8 10 (* 9 11 include "Clight/maps_obsequiv.ma". … … 1161 1163 lemma zlt_succ_refl : ∀a. Zltb a (Zsucc a) = true. 1162 1164 #a @Zlt_to_Zltb_true /2/ qed. 1163 1164 1165 definition le_offset : offset → offset → bool ≝ 1165 (* 1166 definition le_offset : offset → offset → bool. 1166 1167 λx,y. Zleb (offv x) (offv y). 1167 1168 *) 1168 1169 lemma not_refl_absurd : ∀A:Type[0].∀x:A. x ≠ x → False. /2/. qed. 1169 1170 … … 1218 1219 1219 1220 definition offset_plus : offset → offset → offset ≝ 1220 λo1,o2. mk_offset ( offv o1 + offv o2).1221 λo1,o2. mk_offset (addition_n ? (offv o1) (offv o2)). 1221 1222 1222 lemma offset_plus_O : ∀o. offset_plus o (mk_offset OZ) = o. 1223 * #z normalize // qed. 1223 1224 (* Prove that (zero n) is a neutral element for (addition_n n) *) 1225 1226 lemma add_with_carries_n_O : ∀n,bv. add_with_carries n bv (zero n) false = 〈bv,zero n〉. 1227 #n #bv whd in match (add_with_carries ????); elim bv // 1228 #n #hd #tl #Hind whd in match (fold_right2_i ????????); 1229 >Hind normalize 1230 cases n in tl; 1231 [ 1: #tl cases hd normalize @refl 1232  2: #n' #tl cases hd normalize @refl ] 1233 qed. 1234 1235 lemma addition_n_0 : ∀n,bv. addition_n n bv (zero n) = bv. 1236 #n #bv whd in match (addition_n ???); 1237 >add_with_carries_n_O // 1238 qed. 1239 1240 lemma offset_plus_0 : ∀o. offset_plus o (mk_offset (zero ?)) = o. 1241 * #o 1242 whd in match (offset_plus ??); 1243 >addition_n_0 @refl 1244 qed. 1245 1224 1246 1225 1247 (* Translates a pointer through an embedding. *) … … 1252 1274 value_eq E (Vptr p1) (Vptr p2). 1253 1275 1254 (* [load_sim] states the fact that each successful load in [m1] is matched by sucha load in [m2] s.t.1276 (* [load_sim] states the fact that each successful load in [m1] is matched by a load in [m2] s.t. 1255 1277 * the values are equivalent. *) 1256 1278 definition load_sim ≝ … … 1375 1397 load_value_of_type ty m b off = Some ? v → 1376 1398 Zltb (block_id b) (nextblock m) = true ∧ 1377 Zleb (low_bound m b) ( offv off) = true ∧1378 Zltb ( offv off) (high_bound m b) = true.1399 Zleb (low_bound m b) (Z_of_unsigned_bitvector ? (offv off)) = true ∧ 1400 Zltb (Z_of_unsigned_bitvector ? (offv off)) (high_bound m b) = true. 1379 1401 #ty #m * #brg #bid #off #v 1380 1402 cases ty … … 1389 1411 whd in match (beloadv ??); 1390 1412 cases (Zltb bid (nextblock m)) normalize nodelta 1391 cases (Zleb (low (blocks m (mk_block brg bid))) (offv off)) 1392 cases (Zleb (low (blocks m (mk_block brg bid))) (offv off)) 1393 cases (Zltb (offv off) (high (blocks m (mk_block brg bid)))) normalize nodelta 1413 cases (Zleb (low (blocks m (mk_block brg bid))) 1414 (Z_of_unsigned_bitvector offset_size (offv off))) 1415 cases (Zltb (Z_of_unsigned_bitvector offset_size (offv off)) (high (blocks m (mk_block brg bid)))) 1416 normalize nodelta 1394 1417 #Heq destruct (Heq) 1395 1418 try /3 by conj, refl/ … … 1594 1617 cases (Zltb (block_id wb) (nextblock mA)) normalize nodelta 1595 1618 [ 2: #Habsurd destruct (Habsurd) ] 1596 cases (if Zleb (low (blocks mA wb)) ( offv wo)1597 then Zltb ( offv wo) (high (blocks mA wb))1619 cases (if Zleb (low (blocks mA wb)) (Z_of_unsigned_bitvector 16 (offv wo)) 1620 then Zltb (Z_of_unsigned_bitvector 16 (offv wo)) (high (blocks mA wb)) 1598 1621 else false) normalize nodelta 1599 1622 [ 2: #Habsurd destruct (Habsurd) ] … … 1671 1694 normalize in match (valid_pointer ??) in ⊢ (% → %); 1672 1695 >(Zlt_to_Zltb_true … Hlt_wb) in Hstore; normalize nodelta 1673 cases (Zleb (low (contentsB wb)) (offv wo)∧Zltb (offv wo) (high (contentsB wb))) 1696 cases (Zleb (low (contentsB wb)) (Z_of_unsigned_bitvector offset_size (offv wo)) 1697 ∧Zltb (Z_of_unsigned_bitvector offset_size (offv wo)) (high (contentsB wb))) 1674 1698 normalize nodelta 1675 1699 [ 2: #Habsurd destruct (Habsurd) ] … … 1705 1729 lapply Hstore normalize in Hwb_valid Hb_valid ⊢ (% → ?); 1706 1730 >(Zlt_to_Zltb_true … Hwb_valid) normalize nodelta 1707 cases (if Zleb (low (contentsB wb)) ( offv wo)1708 then Zltb ( offv wo) (high (contentsB wb))1731 cases (if Zleb (low (contentsB wb)) (Z_of_unsigned_bitvector 16 (offv wo)) 1732 then Zltb (Z_of_unsigned_bitvector 16 (offv wo)) (high (contentsB wb)) 1709 1733 else false) 1710 1734 normalize [ 2: #Habsurd destruct (Habsurd) ] … … 2286 2310 qed. 2287 2311 2312 lemma commutative_add_with_carries : ∀n,a,b,carry. add_with_carries n a b carry = add_with_carries n b a carry. 2313 #n elim n 2314 [ 1: #a #b #carry 2315 lapply (BitVector_O … a) lapply (BitVector_O … b) #H1 #H2 destruct @refl 2316  2: #n' #Hind #a #b #carry 2317 lapply (BitVector_Sn … a) lapply (BitVector_Sn … b) 2318 * #bhd * #btl #Heqb 2319 * #ahd * #atl #Heqa destruct 2320 lapply (Hind atl btl carry) 2321 whd in match (add_with_carries ????) in ⊢ ((??%%) → (??%%)); 2322 normalize in match (rewrite_l ??????); 2323 normalize nodelta 2324 #Heq >Heq 2325 generalize in match (fold_right2_i ????????); * #res #carries 2326 normalize nodelta 2327 cases ahd cases bhd @refl 2328 ] qed. 2329 2330 axiom associative_add_with_carries : 2331 ∀n,a,b,c,carry1,carry2. 2332 ((let 〈res,flags〉 ≝ 2333 add_with_carries n a 2334 (let 〈res,flags〉 ≝add_with_carries n b c carry1 in res) carry2 in 2335 res) 2336 =(let 〈res,flags〉 ≝ 2337 add_with_carries n 2338 (let 〈res,flags〉 ≝add_with_carries n a b carry1 in res) c carry2 in 2339 res)). 2340 (* 2341 (\fst (add_with_carries n a (\fst (add_with_carries n b c carry1)) carry2)) = 2342 (\fst (add_with_carries n (\fst (add_with_carries n a b carry1)) c carry2)). 2343 2344 #n elim n 2345 [ 1: #a #b #c #carry1 #carry2 2346 lapply (BitVector_O … a) 2347 lapply (BitVector_O … b) 2348 lapply (BitVector_O … c) 2349 #Ha #Hb #Hc 2350 destruct // 2351  2: #n' #Hind #a #b #c #carry1 #carry2 2352 lapply (BitVector_Sn … a) 2353 lapply (BitVector_Sn … b) 2354 lapply (BitVector_Sn … c) 2355 * #chd * #ctl #Heqc 2356 * #bhd * #btl #Heqb 2357 * #ahd * #atl #Heqa 2358 lapply (Hind atl btl ctl carry2 carry1) #Hind 2359 lapply (BitVector_Sn … (\fst (add_with_carries (S n') b c carry1))) 2360 lapply (BitVector_Sn … (\fst (add_with_carries (S n') a b carry1))) 2361 * #ab1 * #abtl1 #Heq_ab 2362 * #bc1 * #bctl1 #Heq_bc 2363 >Heq_ab >Heq_bc destruct 2364 whd in match (add_with_carries) in ⊢ (??%%); 2365 normalize nodelta 2366 whd in match (add_with_carries) in Heq_bc Heq_ab; 2367 normalize nodelta in Heq_bc Heq_ab; 2368 <Heq_ab <Heq_bc 2369 >fold_right2_i_unfold 2370 >fold_right2_i_unfold 2371 lapply Hind; 2372 whd in match (add_with_carries ????) in ⊢ ((??%%) → ?); 2373 normalize in match (add_with_carries ????) in ⊢ ((??%%) → ?); 2374 normalize 2375 #Hind >Hind 2376 normalize nodelta 2377 2378 normalize in Hind; 2379 *) 2380 2381 lemma commutative_addition_n : ∀n,a,b. addition_n n a b = addition_n n b a. 2382 #n #a #b whd in match (addition_n ???) in ⊢ (??%%); >commutative_add_with_carries 2383 @refl 2384 qed. 2385 2386 lemma associative_addition_n : ∀n,a,b,c. addition_n n a (addition_n n b c) = addition_n n (addition_n n a b) c. 2387 #n #a #b #c whd in match (addition_n ???) in ⊢ (??%%); 2388 whd in match (addition_n n b c); 2389 whd in match (addition_n n a b); 2390 <(associative_add_with_carries … n a b c false false) 2391 @refl 2392 qed. 2288 2393 2289 2394 (* value_eq lifts to addition *) … … 2325 2430 whd in match (shift_pointer_n ????); 2326 2431 cut (offset_plus (shift_offset_n (bitsize_of_intsize sz) o1' (sizeof ty) i) offset = 2327 (shift_offset_n (bitsize_of_intsize sz) (mk_offset (offv o1'+offv offset)) (sizeof ty) i)) 2328 [ 1: normalize >sym_Zplus <associative_Zplus >(sym_Zplus (offv offset) (offv o1')) @refl ] 2432 (shift_offset_n (bitsize_of_intsize sz) (mk_offset (addition_n ? (offv o1') (offv offset))) (sizeof ty) i)) 2433 [ 1: whd in match (offset_plus ??); 2434 whd in match (shift_offset_n ????) in ⊢ (??%%); 2435 >commutative_addition_n >associative_addition_n 2436 <(commutative_addition_n … (offv offset) (offv o1')) @refl ] 2329 2437 #Heq >Heq @refl ] 2330 2438 ] … … 2362 2470 [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) 2363 2471  2: * #block #offset normalize nodelta #Heq destruct (Heq) 2364 normalize >(sym_Zplus ? (offv offset)) <associative_Zplus >(sym_Zplus ? (offv offset)) 2365 @refl 2472 whd in match (shift_pointer_n ????); 2473 whd in match (shift_offset_n ????) in ⊢ (??%%); 2474 whd in match (offset_plus ??); 2475 whd in match (offset_plus ??); 2476 >commutative_addition_n >(associative_addition_n … offset_size ?) 2477 >(commutative_addition_n ? (offv offset) ?) @refl 2366 2478 ] 2367 2479 ] qed. 2480 2481 lemma fold_right2_O : ∀A,B,C,f,init,vec1,vec2. 2482 fold_right2_i A B C f init 0 vec1 vec2 = init. 2483 #A #B #C #f #init #vec1 #vec2 2484 >(Vector_O … vec1) 2485 >(Vector_O … vec2) 2486 normalize @refl 2487 qed. 2488 2489 lemma map_unfold : ∀A,B:Type[0].∀n,f,hd.∀tl:Vector A n. 2490 map A B (S n) f (hd ::: tl) = (f hd) ::: (map A B n f tl). 2491 #A #B #n #f #hd #tl normalize @refl qed. 2492 2493 lemma replicate_unfold : ∀A,sz,elt. 2494 replicate A (S sz) elt = elt ::: (replicate A sz elt). 2495 // qed. 2496 2497 axiom subtraction_delta : ∀x,y,delta. 2498 subtraction offset_size 2499 (addition_n offset_size x delta) 2500 (addition_n offset_size y delta) = 2501 subtraction offset_size x y. 2502 (* 2503 elim offset_size 2504 [ 1: #x #y #delta 2505 >(BitVector_O … x) 2506 >(BitVector_O … y) 2507 >(BitVector_O … delta) 2508 // 2509 2510  2: #sz elim sz (* I would like to do this elim much later, but it fails. *) 2511 [ 1: #Hind #x #y #delta 2512 lapply (BitVector_Sn … x) 2513 lapply (BitVector_Sn … y) 2514 lapply (BitVector_Sn … delta) 2515 * #delta_hd * #delta_tl #Heq_delta 2516 * #y_hd * #y_tl #Heq_y 2517 * #x_hd * #x_tl #Heq_x 2518 destruct 2519 whd in match (addition_n ? (x_hd:::x_tl) ?); 2520 whd in match (addition_n ? (y_hd:::y_tl) ?); 2521 >add_with_carries_unfold 2522 >add_with_carries_unfold 2523 >fold_right2_i_unfold 2524 >fold_right2_i_unfold 2525 <add_with_carries_unfold 2526 <add_with_carries_unfold 2527 cases (add_with_carries 0 x_tl delta_tl false); 2528 #x_delta_res #x_delta_flags normalize nodelta 2529 cases (add_with_carries 0 y_tl delta_tl false) 2530 #y_delta_res #y_delta_flags normalize nodelta 2531 >(BitVector_O … x_delta_flags) 2532 >(BitVector_O … y_delta_flags) 2533 >(BitVector_O … x_delta_res) 2534 >(BitVector_O … y_delta_res) 2535 normalize nodelta 2536 whd in match (xorb ? false) in ⊢ (??(??%%)?); normalize nodelta 2537 whd in match (subtraction ???) in ⊢ (??%%); 2538 >add_with_carries_unfold 2539 whd in match (two_complement_negation ??); 2540 whd in match (negation_bv ??); 2541 whd in match (zero ?); 2542 >add_with_carries_unfold 2543 >fold_right2_i_unfold >fold_right2_O 2544 normalize nodelta 2545 >fold_right2_i_unfold >fold_right2_O 2546 normalize nodelta 2547 cases x_hd cases y_hd cases delta_hd normalize try @refl 2548  2: #sz' #HindA #HindB #x #y #delta 2549 lapply (BitVector_Sn … x) 2550 lapply (BitVector_Sn … y) 2551 lapply (BitVector_Sn … delta) 2552 * #delta_hd * #delta_tl #Heq_delta 2553 * #y_hd * #y_tl #Heq_y 2554 * #x_hd * #x_tl #Heq_x 2555 lapply (HindB x_tl y_tl delta_tl) 2556 destruct 2557 whd in match (addition_n ???) in ⊢ ((??(??%%)?) → ?); #Hind0 2558 whd in match (addition_n ? (x_hd:::x_tl) ?); 2559 whd in match (addition_n ? (y_hd:::y_tl) ?); 2560 >add_with_carries_unfold 2561 >add_with_carries_unfold 2562 >fold_right2_i_unfold 2563 >fold_right2_i_unfold 2564 <add_with_carries_unfold 2565 <add_with_carries_unfold 2566 cases (add_with_carries (S sz') x_tl delta_tl false) in Hind0; 2567 #x_delta_res #x_delta_flags normalize nodelta 2568 cases (add_with_carries (S sz') y_tl delta_tl false) 2569 #y_delta_res #y_delta_flags normalize nodelta 2570 elim (BitVector_Sn … x_delta_flags) #hd_x_delta * #tl_x_delta #Heq_xdelta >Heq_xdelta 2571 elim (BitVector_Sn … y_delta_flags) #hd_y_delta * #tl_y_delta #Heq_ydelta >Heq_ydelta 2572 #Heq_ind 2573 normalize nodelta 2574 cases hd_x_delta cases hd_y_delta normalize nodelta 2575 whd in match (subtraction ???) in ⊢ (??%%); 2576 whd in match (two_complement_negation ??) in ⊢ (??%%); 2577 whd in match (negation_bv ??) in ⊢ (??%%); 2578 whd in match (zero (S (S sz'))); 2579 >add_with_carries_unfold in match (\fst (add_with_carries ????)) in ⊢ (??%?); 2580 >add_with_carries_unfold in match (\fst (add_with_carries ????)) in ⊢ (???%); 2581 lapply (add_with_carries_unfold 2582 (S (S sz')) 2583 ((¬y_hd):::map bool bool (S sz') notb y_tl) 2584 (false:::replicate bool (S sz') false) 2585 true) #Heq >Heq 2586 >fold_right2_i_unfold >fold_right2_i_unfold 2587 >add_with_carries_unfold in ⊢ (???(match (???%?) with [ _ ⇒ ? ] )); 2588 2589 *) 2368 2590 2369 2591 (* Offset subtraction is invariant by translation *) … … 2373 2595 whd in match (sub_offset ???) in ⊢ (??%%); 2374 2596 elim x #x' elim y #y' elim delta #delta' 2375 normalize in match (offset_plus ??); 2376 normalize in match (offset_plus ??); 2377 cut ((x'  y') = (x'+delta'(y'+delta'))) 2378 [ whd in match (Zminus ??) in ⊢ (??%%); 2379 >(Zopp_Zplus y' delta') <associative_Zplus /2/ ] 2380 #Heq >Heq @refl 2381 qed. 2597 whd in match (offset_plus ??); 2598 whd in match (offset_plus ??); 2599 >subtraction_delta @refl 2600 qed. 2382 2601 2383 2602 (* value_eq lifts to addition *) … … 2441 2660 [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) 2442 2661  2: * #block #offset normalize nodelta #Heq destruct (Heq) 2443 normalize >(sym_Zplus ? (offv offset)) <associative_Zplus >(sym_Zplus ? (offv offset)) 2444 @refl 2662 whd in match (offset_plus ??) in ⊢ (??%%); 2663 whd in match (neg_shift_pointer_n ????) in ⊢ (??%%); 2664 whd in match (neg_shift_offset_n ????) in ⊢ (??%%); 2665 whd in match (subtraction) in ⊢ (??%%); normalize nodelta 2666 generalize in match (short_multiplication ???); #mult 2667 /3 by associative_addition_n, commutative_addition_n, refl/ 2445 2668 ] 2446 2669  2: lapply Heq @eq_block_elim
Note: See TracChangeset
for help on using the changeset viewer.