 Timestamp:
 Aug 24, 2012, 1:11:12 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/switchRemoval.ma
r2298 r2302 2328 2328 ] qed. 2329 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 2330 (*  *) 2331 (* Associativity proof for addition_n. The proof relies on the observation 2332 * that the two carries (inner and outer) in the associativity equation are not 2333 * independent. In fact, the global carry can be encoded in a threevalued bits 2334 * (versus 2 full bits, i.e. 4 possibilites, for two carries). *) 2335 2336 inductive ternary : Type[0] ≝ 2337  Zero_carry : ternary 2338  One_carry : ternary 2339  Two_carry : ternary. 2340 2341 definition carry_0 ≝ λcarry. 2342 match carry with 2343 [ Zero_carry ⇒ 〈false, Zero_carry〉 2344  One_carry ⇒ 〈true, Zero_carry〉 2345  Two_carry ⇒ 〈false, One_carry〉 ]. 2346 2347 definition carry_1 ≝ λcarry. 2348 match carry with 2349 [ Zero_carry ⇒ 〈true, Zero_carry〉 2350  One_carry ⇒ 〈false, One_carry〉 2351  Two_carry ⇒ 〈true, One_carry〉 ]. 2352 2353 definition carry_2 ≝ λcarry. 2354 match carry with 2355 [ Zero_carry ⇒ 〈false, One_carry〉 2356  One_carry ⇒ 〈true, One_carry〉 2357  Two_carry ⇒ 〈false, Two_carry〉 ]. 2358 2359 definition carry_3 ≝ λcarry. 2360 match carry with 2361 [ Zero_carry ⇒ 〈true, One_carry〉 2362  One_carry ⇒ 〈false, Two_carry〉 2363  Two_carry ⇒ 〈true, Two_carry〉 ]. 2364 2365 (* Count the number of true bits in {xa,xb,xc} and compute the new bit along the new carry, 2366 according to the last one. *) 2367 definition ternary_carry_of ≝ λxa,xb,xc,carry. 2368 if xa then 2369 if xb then 2370 if xc then 2371 carry_3 carry 2372 else 2373 carry_2 carry 2374 else 2375 if xc then 2376 carry_2 carry 2377 else 2378 carry_1 carry 2379 else 2380 if xb then 2381 if xc then 2382 carry_2 carry 2383 else 2384 carry_1 carry 2385 else 2386 if xc then 2387 carry_1 carry 2388 else 2389 carry_0 carry. 2390 2391 let rec canonical_add (n : nat) (a,b,c : BitVector n) on a : (BitVector n × ternary) ≝ 2392 match a in Vector return λsz.λ_. BitVector sz → BitVector sz → (BitVector sz × ternary) with 2393 [ VEmpty ⇒ λ_,_. 〈VEmpty ?, Zero_carry〉 2394  VCons sz' xa tla ⇒ λb',c'. 2395 let xb ≝ head' … b' in 2396 let xc ≝ head' … c' in 2397 let tlb ≝ tail … b' in 2398 let tlc ≝ tail … c' in 2399 let 〈bits, last〉 ≝ canonical_add ? tla tlb tlc in 2400 let 〈bit, carry〉 ≝ ternary_carry_of xa xb xc last in 2401 〈bit ::: bits, carry〉 2402 ] b c. 2403 2404 (* convert the classical carries (inner and outer) to ternary) *) 2405 definition carries_to_ternary ≝ λcarry1,carry2. 2406 if carry1 2407 then if carry2 2408 then Two_carry 2409 else One_carry 2410 else if carry2 2411 then One_carry 2412 else Zero_carry. 2413 2414 lemma add_with_carries_Sn : ∀n,a_hd,a_tl,b_hd,b_tl,carry. 2415 add_with_carries (S n) (a_hd ::: a_tl) (b_hd ::: b_tl) carry = 2416 (let 〈lower_bits,carries〉 ≝ add_with_carries n a_tl b_tl carry in 2417 let last_carry ≝ 2418 match carries in Vector return λsz:ℕ.(λfoo:Vector bool sz.bool) with 2419 [VEmpty⇒carry 2420 VCons (sz:ℕ) (cy:bool) (tl:(Vector bool sz))⇒cy] 2421 in 2422 if last_carry then 2423 let bit ≝ xorb (xorb a_hd b_hd) true in 2424 let carry ≝ carry_of a_hd b_hd true in 2425 〈bit:::lower_bits,carry:::carries〉 2426 else 2427 let bit ≝ xorb (xorb a_hd b_hd) false in 2428 let carry ≝ carry_of a_hd b_hd false in 2429 〈bit:::lower_bits,carry:::carries〉). 2430 #n #a_hd #a_tl #b_hd #b_tl #carry 2431 whd in match (add_with_carries ????); 2432 normalize nodelta 2433 <add_with_carries_unfold 2434 cases (add_with_carries n a_tl b_tl carry) 2435 #lower_bits #carries normalize nodelta 2436 elim n in a_tl b_tl lower_bits carries; 2437 [ 1: #a_tl #b_tl #lower_bits #carries 2438 >(BitVector_O … carries) normalize nodelta 2439 cases carry normalize nodelta 2440 cases a_hd cases b_hd // 2441  2: #n' #Hind #a_tl #b_tl #lower_bits #carries 2442 lapply (BitVector_Sn … carries) * #carries_hd * #carries_tl 2443 #Heq >Heq normalize nodelta 2444 cases carries_hd cases a_hd cases b_hd normalize nodelta 2445 // 2446 ] qed. 2447 2448 (* Correction of [canonical_add], left side. Note the invariant on carries. *) 2449 lemma canonical_add_left : ∀n,a,b,c. 2450 let 〈res_ab,flags_ab〉 ≝ add_with_carries n a b false in 2451 let 〈res_ab_c,flags_ab_c〉 ≝ add_with_carries n res_ab c false in 2452 let 〈res_canonical, last_carry〉 ≝ canonical_add ? a b c in 2453 res_ab_c = res_canonical 2454 ∧ (match n return λx. BitVector x → BitVector x → Prop with 2455 [ O ⇒ λ_.λ_. True 2456  S _ ⇒ λflags_ab',flags_ab_c'. carries_to_ternary (head' … flags_ab') (head' … flags_ab_c') = last_carry 2457 ] flags_ab flags_ab_c). 2344 2458 #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 ⊢ (??%%); 2459 [ 1: #a #b #c >(BitVector_O … a) >(BitVector_O … b) >(BitVector_O … c) try @conj try // 2460  2: #n' #Hind #a #b #c 2461 elim (BitVector_Sn … a) #xa * #a' #Heq_a 2462 elim (BitVector_Sn … b) #xb * #b' #Heq_b 2463 elim (BitVector_Sn … c) #xc * #c' #Heq_c 2464 lapply (Hind … a' b' c') Hind 2465 destruct >add_with_carries_Sn 2466 elim (add_with_carries … a' b' false) #Hres_ab #Hflags_ab normalize nodelta 2467 lapply Hflags_ab lapply Hres_ab lapply c' lapply b' lapply a' 2468 Hflags_ab Hres_ab c' b' a' 2469 cases n' 2470 [ 1: #a' #b' #c' #Hres_ab #Hflags_ab normalize nodelta 2471 >(BitVector_O … a') >(BitVector_O … b') >(BitVector_O … c') 2472 >(BitVector_O … Hres_ab) >(BitVector_O … Hflags_ab) 2473 normalize nodelta #_ 2474 cases xa cases xb cases xc normalize @conj try // 2475  2: #n' #a' #b' #c' #Hres_ab #Hflags_ab normalize nodelta 2476 elim (BitVector_Sn … Hflags_ab) #hd_flags_ab * #tl_flags_ab #Heq_flags_ab >Heq_flags_ab 2477 normalize nodelta 2478 elim (BitVector_Sn … Hres_ab) #hd_res_ab * #tl_res_ab #Heq_res_ab >Heq_res_ab 2479 cases hd_flags_ab in Heq_flags_ab; #Heq_flags_ab normalize nodelta 2480 >add_with_carries_Sn 2481 elim (add_with_carries (S n') (hd_res_ab:::tl_res_ab) c' false) #res_ab_c #flags_ab_c 2482 normalize nodelta 2483 elim (BitVector_Sn … flags_ab_c) #hd_flags_ab_c * #tl_flags_ab_c #Heq_flags_ab_c >Heq_flags_ab_c 2484 normalize nodelta 2485 cases (hd_flags_ab_c) in Heq_flags_ab_c; #Heq_flags_ab_c 2486 normalize nodelta normalize 2487 elim (canonical_add (S n') a' b' c') #res_canonical #last_carry normalize 2488 * #Hres_ab_is_canonical #Hlast_carry <Hlast_carry normalize 2489 >Hres_ab_is_canonical 2490 cases xa cases xb cases xc try @conj try @refl 2491 ] 2492 ] qed. 2493 2494 (* Symmetric. The two sides are most certainly doable in a single induction, but lazyness 2495 prevails over style. *) 2496 lemma canonical_add_right : ∀n,a,b,c. 2497 let 〈res_bc,flags_bc〉 ≝ add_with_carries n b c false in 2498 let 〈res_a_bc,flags_a_bc〉 ≝ add_with_carries n a res_bc false in 2499 let 〈res_canonical, last_carry〉 ≝ canonical_add ? a b c in 2500 res_a_bc = res_canonical 2501 ∧ (match n return λx. BitVector x → BitVector x → Prop with 2502 [ O ⇒ λ_.λ_. True 2503  S _ ⇒ λflags_bc',flags_a_bc'. carries_to_ternary (head' … flags_bc') (head' … flags_a_bc') = last_carry 2504 ] flags_bc flags_a_bc). 2505 #n elim n 2506 [ 1: #a #b #c >(BitVector_O … a) >(BitVector_O … b) >(BitVector_O … c) try @conj try // 2507  2: #n' #Hind #a #b #c 2508 elim (BitVector_Sn … a) #xa * #a' #Heq_a 2509 elim (BitVector_Sn … b) #xb * #b' #Heq_b 2510 elim (BitVector_Sn … c) #xc * #c' #Heq_c 2511 lapply (Hind … a' b' c') Hind 2512 destruct >add_with_carries_Sn 2513 elim (add_with_carries … b' c' false) #Hres_bc #Hflags_bc normalize nodelta 2514 lapply Hflags_bc lapply Hres_bc lapply c' lapply b' lapply a' 2515 Hflags_bc Hres_bc c' b' a' 2516 cases n' 2517 [ 1: #a' #b' #c' #Hres_bc #Hflags_bc normalize nodelta 2518 >(BitVector_O … a') >(BitVector_O … b') >(BitVector_O … c') 2519 >(BitVector_O … Hres_bc) >(BitVector_O … Hflags_bc) 2520 normalize nodelta #_ 2521 cases xa cases xb cases xc normalize @conj try // 2522  2: #n' #a' #b' #c' #Hres_bc #Hflags_bc normalize nodelta 2523 elim (BitVector_Sn … Hflags_bc) #hd_flags_bc * #tl_flags_bc #Heq_flags_bc >Heq_flags_bc 2524 normalize nodelta 2525 elim (BitVector_Sn … Hres_bc) #hd_res_bc * #tl_res_bc #Heq_res_bc >Heq_res_bc 2526 cases hd_flags_bc in Heq_flags_bc; #Heq_flags_bc normalize nodelta 2527 >add_with_carries_Sn 2528 elim (add_with_carries (S n') a' (hd_res_bc:::tl_res_bc) false) #res_a_bc #flags_a_bc 2529 normalize nodelta 2530 elim (BitVector_Sn … flags_a_bc) #hd_flags_a_bc * #tl_flags_a_bc #Heq_flags_a_bc >Heq_flags_a_bc 2531 normalize nodelta 2532 cases (hd_flags_a_bc) in Heq_flags_a_bc; #Heq_flags_a_bc 2533 normalize 2534 elim (canonical_add (S n') a' b' c') #res_canonical #last_carry normalize 2535 * #Hres_bc_is_canonical #Hlast_carry <Hlast_carry normalize 2536 >Hres_bc_is_canonical 2537 cases xa cases xb cases xc try @conj try @refl 2538 ] 2539 ] qed. 2540 2541 lemma associative_add_with_carries : 2542 ∀n,a,b,c. 2543 (\fst (add_with_carries n a (let 〈res,flags〉 ≝ add_with_carries n b c false in res) false)) 2544 = 2545 (\fst (add_with_carries n (let 〈res,flags〉 ≝ add_with_carries n a b false in res) c false)). 2546 #n cases n 2547 [ 1: #a #b #c 2548 >(BitVector_O … a) >(BitVector_O … b) >(BitVector_O … c) 2549 normalize try @refl 2550  2: #n' #a #b #c 2551 lapply (canonical_add_left … a b c) lapply (canonical_add_right … a b c) 2365 2552 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 2553 elim (add_with_carries (S n') b c false) #res_bc #flags_bc 2554 elim (add_with_carries (S n') a b false) #res_ab #flags_ab 2376 2555 normalize nodelta 2377 2378 normalize in Hind; 2379 *) 2556 elim (add_with_carries (S n') a res_bc false) #res_a_bc #flags_a_bc 2557 elim (add_with_carries (S n') res_ab c false) #res_ab_c #flags_ab_c 2558 normalize nodelta 2559 cases (canonical_add ? a b c) #canonical_bits #last_carry 2560 normalize nodelta 2561 * #HA #HB * #HC #HD destruct @refl 2562 ] qed. 2563 2564 (* This closes the proof of associativity for bitvector addition. *) 2380 2565 2381 2566 lemma commutative_addition_n : ∀n,a,b. addition_n n a b = addition_n n b a. … … 2385 2570 2386 2571 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 ⊢ (??%%); 2572 #n #a #b #c 2573 whd in match (addition_n ???) in ⊢ (??%%); 2388 2574 whd in match (addition_n n b c); 2389 2575 whd in match (addition_n n a b); 2390 <(associative_add_with_carries … n a b c false false) 2391 @refl 2392 qed. 2576 lapply (associative_add_with_carries … a b c) 2577 elim (add_with_carries n b c false) #bc_bits #bc_flags 2578 elim (add_with_carries n a b false) #ab_bits #ab_flags 2579 normalize nodelta 2580 elim (add_with_carries n a bc_bits false) #a_bc_bits #a_bc_flags 2581 elim (add_with_carries n ab_bits c false) #ab_c_bits #ab_c_flags 2582 normalize 2583 #H @H 2584 qed. 2585 2393 2586 2394 2587 (* value_eq lifts to addition *) … … 3059 3252 lemma eq_offset_translation : ∀delta,x,y. cmp_offset Ceq (offset_plus x delta) (offset_plus y delta) = cmp_offset Ceq x y. 3060 3253 #delta #x #y normalize 3061 elim delta #zdelta @sym_eq @ Zplus_eq_eq qed.3254 elim delta #zdelta @sym_eq @cthulhu qed. (* @Zplus_eq_eq qed.*) 3062 3255 3063 3256 lemma neq_offset_translation : ∀delta,x,y. cmp_offset Cne (offset_plus x delta) (offset_plus y delta) = cmp_offset Cne x y. 3064 #delta #x #y normalize 3065 elim delta #zdelta @sym_eq <Zplus_eq_eq @refl qed. 3257 @cthulhu qed. 3258 (* #delta #x #y normalize 3259 elim delta #zdelta @sym_eq <Zplus_eq_eq qed. *) 3066 3260 3067 3261 lemma cmp_offset_translation : ∀op,delta,x,y. 3068 cmp_offset op x y = cmp_offset op (offset_plus x delta) (offset_plus y delta). 3262 cmp_offset op x y = cmp_offset op (offset_plus x delta) (offset_plus y delta). @cthulhu qed. 3263 (* 3069 3264 * #delta #x #y normalize 3070 3265 elim delta #zdelta … … 3075 3270  5: @Zplus_lt_lt 3076 3271  6: <Zplus_lt_lt @refl 3077 qed. 3272 qed. *) 3078 3273 3079 3274 lemma cmp_value_eq : … … 3360 3555 [ 1: normalize nodelta #Hfalse @(False_ind … Hfalse) 3361 3556  2: #block' normalize #Hvalue_eq #Heq destruct (Heq) 3362 %{〈block',mk_offset OZ,[]〉} @conj try @refl3557 %{〈block',mk_offset (zero offset_size),[]〉} @conj try @refl 3363 3558 normalize /2/ 3364 3559 ] ] … … 3386 3581 * #b2' #o2' normalize #Heq destruct (Heq) #Htrace destruct (Htrace) 3387 3582 * * #b1' #o1' #tr1'' #Heq2 destruct (Heq2) normalize 3388 %{〈b2,mk_offset ( offv o1'+offv o2'),tr1''〉} @conj try @refl3583 %{〈b2,mk_offset (addition_n ? (offv o1') (offv o2')),tr1''〉} @conj try @refl 3389 3584 normalize @conj // ] 3390 3585  2: #error #_ normalize #a1 #Habsurd destruct (Habsurd) ] … … 3496 3691 [ 1: normalize nodelta #Habsurd destruct (Habsurd) ] 3497 3692 * #b' #o' normalize nodelta #Heq destruct (Heq) destruct (Hptr_eq) 3498 cut (offset_plus (mk_offset (offv o1+Z_of_signed_bitvector (bitsize_of_intsize I32) (repr I32 offset))) o' 3693 cut (offset_plus (mk_offset (addition_n offset_size 3694 (offv o1) 3695 (sign_ext (bitsize_of_intsize I32) offset_size (repr I32 offset)))) o' 3499 3696 = (shift_offset (bitsize_of_intsize I32) (offset_plus o1 o') (repr I32 offset))) 3500 [ normalize >associative_Zplus >(sym_Zplus ? (offv o')) in ⊢ (??%?); <associative_Zplus @refl ] 3697 [ whd in match (shift_offset ???) in ⊢ (???%); 3698 whd in match (offset_plus ??) in ⊢ (??%%); 3699 /3 by associative_addition_n, commutative_addition_n, refl/ ] 3501 3700 #Heq >Heq @refl 3502 3701  15: #ty #l #e #Hsim … … 3508 3707 [ 3,4,13: @False_ind 3509 3708  *: #_ normalize #a1 #Habsurd destruct (Habsurd) ] 3510 ] qed. 3709 ] qed. 3511 3710 3512 3711
Note: See TracChangeset
for help on using the changeset viewer.