Changeset 2298


Ignore:
Timestamp:
Aug 16, 2012, 7:01:18 PM (7 years ago)
Author:
garnier
Message:

WIP: converting switch removal from Z to bitvectors. Does not compile, contains axioms.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/switchRemoval.ma

    r2271 r2298  
    66include "Clight/CexecInd.ma".
    77include "Clight/frontend_misc.ma".
     8include "Clight/casts.ma". (* lemmas related to bitvectors ... *)
     9
    810(*
    911include "Clight/maps_obsequiv.ma".
     
    11611163lemma zlt_succ_refl : ∀a. Zltb a (Zsucc a) = true.
    11621164#a @Zlt_to_Zltb_true /2/ qed.
    1163 
    1164 
    1165 definition le_offset : offset → offset → bool ≝
     1165(*
     1166definition le_offset : offset → offset → bool.
    11661167  λx,y. Zleb (offv x) (offv y).
    1167  
     1168*)
    11681169lemma not_refl_absurd : ∀A:Type[0].∀x:A. x ≠ x → False. /2/. qed.
    11691170
     
    12181219
    12191220definition 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)).
    12211222 
    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
     1226lemma 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
     1230cases n in tl;
     1231[ 1: #tl cases hd normalize @refl
     1232| 2: #n' #tl cases hd normalize @refl ]
     1233qed.
     1234
     1235lemma 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 //
     1238qed.
     1239
     1240lemma offset_plus_0 : ∀o. offset_plus o (mk_offset (zero ?)) = o.
     1241* #o
     1242whd in match (offset_plus ??);
     1243>addition_n_0 @refl
     1244qed.
     1245
    12241246
    12251247(* Translates a pointer through an embedding. *)
     
    12521274  value_eq E (Vptr p1) (Vptr p2).
    12531275
    1254 (* [load_sim] states the fact that each successful load in [m1] is matched by such a 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.
    12551277 * the values are equivalent. *)
    12561278definition load_sim ≝
     
    13751397    load_value_of_type ty m b off = Some ? v →
    13761398    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.
    13791401#ty #m * #brg #bid #off #v
    13801402cases ty
     
    13891411     whd in match (beloadv ??);
    13901412     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
    13941417     #Heq destruct (Heq)
    13951418     try /3 by conj, refl/
     
    15941617cases (Zltb (block_id wb) (nextblock mA)) normalize nodelta
    15951618[ 2: #Habsurd destruct (Habsurd) ]
    1596 cases (if Zleb (low (blocks mA wb)) (offv wo) 
    1597        then Zltb (offv wo) (high (blocks mA wb)) 
     1619cases (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)) 
    15981621       else false) normalize nodelta
    15991622[ 2: #Habsurd destruct (Habsurd) ]
     
    16711694normalize in match (valid_pointer ??) in ⊢ (% → %);
    16721695>(Zlt_to_Zltb_true … Hlt_wb) in Hstore; normalize nodelta
    1673 cases (Zleb (low (contentsB wb)) (offv wo)∧Zltb (offv wo) (high (contentsB wb)))
     1696cases (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)))
    16741698normalize nodelta
    16751699[ 2: #Habsurd destruct (Habsurd) ]
     
    17051729lapply Hstore normalize in Hwb_valid Hb_valid ⊢ (% → ?);
    17061730>(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)) 
     1731cases (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)) 
    17091733       else false)
    17101734normalize [ 2: #Habsurd destruct (Habsurd) ]
     
    22862310qed.
    22872311
     2312lemma 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
     2330axiom 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   
     2381lemma 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
     2384qed.
     2385
     2386lemma 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 ⊢ (??%%);
     2388whd in match (addition_n n b c);
     2389whd in match (addition_n n a b);
     2390<(associative_add_with_carries … n a b c false false)
     2391@refl
     2392qed.
    22882393
    22892394(* value_eq lifts to addition *)
     
    23252430               whd in match (shift_pointer_n ????);
    23262431               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 ]
    23292437               #Heq >Heq @refl ]
    23302438     ]
     
    23622470     [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
    23632471     | 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
    23662478     ]
    23672479] qed.
     2480
     2481lemma 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)
     2486normalize @refl
     2487qed.
     2488
     2489lemma 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
     2493lemma replicate_unfold : ∀A,sz,elt.
     2494  replicate A (S sz) elt = elt ::: (replicate A sz elt).
     2495// qed.
     2496
     2497axiom 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(*
     2503elim 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*)
    23682590
    23692591(* Offset subtraction is invariant by translation *)
     
    23732595whd in match (sub_offset ???) in ⊢ (??%%);
    23742596elim 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.   
     2597whd in match (offset_plus ??);
     2598whd in match (offset_plus ??);
     2599>subtraction_delta @refl
     2600qed.
    23822601
    23832602(* value_eq lifts to addition *)
     
    24412660          [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
    24422661          | 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/
    24452668          ]
    24462669     | 2: lapply Heq @eq_block_elim
Note: See TracChangeset for help on using the changeset viewer.