Changeset 2302


Ignore:
Timestamp:
Aug 24, 2012, 1:11:12 PM (7 years ago)
Author:
garnier
Message:

Finally proved associativity of addition on bitvectors. Rejoice.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/switchRemoval.ma

    r2298 r2302  
    23282328] qed.
    23292329
    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 three-valued bits
     2334 * (versus 2 full bits, i.e. 4 possibilites, for two carries). *)
     2335
     2336inductive ternary : Type[0] ≝
     2337| Zero_carry : ternary
     2338| One_carry : ternary
     2339| Two_carry : ternary.
     2340
     2341definition 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   
     2347definition 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
     2353definition 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
     2359definition 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. *)
     2367definition ternary_carry_of ≝ λxa,xb,xc,carry.
     2368if 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
     2379else
     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
     2391let rec canonical_add (n : nat) (a,b,c : BitVector n) on a : (BitVector n × ternary) ≝
     2392match 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) *)
     2405definition 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   
     2414lemma 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
     2431whd in match (add_with_carries ????);
     2432normalize nodelta
     2433<add_with_carries_unfold
     2434cases (add_with_carries n a_tl b_tl carry)
     2435#lower_bits #carries normalize nodelta
     2436elim 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. *)
     2449lemma 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).
    23442458#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.  *)
     2496lemma 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
     2541lemma 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)
    23652552     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
    23762555     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. *)     
    23802565   
    23812566lemma commutative_addition_n : ∀n,a,b. addition_n n a b = addition_n n b a.
     
    23852570
    23862571lemma 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
     2573whd in match (addition_n ???) in ⊢ (??%%);
    23882574whd in match (addition_n n b c);
    23892575whd in match (addition_n n a b);
    2390 <(associative_add_with_carries … n a b c false false)
    2391 @refl
    2392 qed.
     2576lapply (associative_add_with_carries … a b c)
     2577elim (add_with_carries n b c false) #bc_bits #bc_flags
     2578elim (add_with_carries n a b false) #ab_bits #ab_flags
     2579normalize nodelta
     2580elim (add_with_carries n a bc_bits false) #a_bc_bits #a_bc_flags
     2581elim (add_with_carries n ab_bits c false) #ab_c_bits #ab_c_flags
     2582normalize
     2583#H @H
     2584qed.
     2585
    23932586
    23942587(* value_eq lifts to addition *)
     
    30593252lemma eq_offset_translation : ∀delta,x,y. cmp_offset Ceq (offset_plus x delta) (offset_plus y delta) = cmp_offset Ceq x y.
    30603253#delta #x #y normalize
    3061 elim delta #zdelta @sym_eq @Zplus_eq_eq qed.
     3254elim delta #zdelta @sym_eq @cthulhu qed. (* @Zplus_eq_eq qed.*)
    30623255
    30633256lemma 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
     3259elim delta #zdelta @sym_eq <Zplus_eq_eq qed. *)
    30663260
    30673261lemma 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(*
    30693264* #delta #x #y normalize
    30703265elim delta #zdelta
     
    30753270| 5: @Zplus_lt_lt
    30763271| 6: <Zplus_lt_lt @refl
    3077 qed.
     3272qed. *)
    30783273
    30793274lemma cmp_value_eq :
     
    33603555                    [ 1: normalize nodelta #Hfalse @(False_ind … Hfalse)
    33613556                    | 2: #block' normalize #Hvalue_eq #Heq destruct (Heq)
    3362                          %{〈block',mk_offset OZ,[]〉} @conj try @refl
     3557                         %{〈block',mk_offset (zero offset_size),[]〉} @conj try @refl
    33633558                         normalize /2/
    33643559                ] ]
     
    33863581               * #b2' #o2' normalize #Heq destruct (Heq) #Htrace destruct (Htrace)
    33873582               * * #b1' #o1' #tr1'' #Heq2 destruct (Heq2) normalize
    3388                %{〈b2,mk_offset (offv o1'+offv o2'),tr1''〉} @conj try @refl
     3583               %{〈b2,mk_offset (addition_n ? (offv o1') (offv o2')),tr1''〉} @conj try @refl
    33893584               normalize @conj // ]
    33903585     | 2: #error #_ normalize #a1 #Habsurd destruct (Habsurd) ]
     
    34963691    [ 1: normalize nodelta #Habsurd destruct (Habsurd) ]
    34973692    * #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'
    34993696          = (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/ ]
    35013700    #Heq >Heq @refl
    35023701| 15: #ty #l #e #Hsim
     
    35083707  [ 3,4,13: @False_ind
    35093708  | *: #_ normalize #a1 #Habsurd destruct (Habsurd) ]
    3510 ] qed.   
     3709] qed.
    35113710
    35123711
Note: See TracChangeset for help on using the changeset viewer.