Changeset 2032 for src/Clight


Ignore:
Timestamp:
Jun 8, 2012, 4:32:03 PM (8 years ago)
Author:
sacerdot
Message:

!! BEWARE: major commit !!

1) [affects everybody]

split for vectors renamed to vsplit to reduce ambiguity since split is
now also a function in the standard library.
Note: I have not been able to propagate the changes everywhere in
the front-end/back-end because some files do not compile

2) [affects everybody]

functions on Vectors copied both in the front and back-ends moved to
Vectors.ma

3) [affects only the back-end]

subaddressing_mode_elim redesigned from scratch and now also applied to
Policy.ma. Moreover, all daemons about that have been closed.
The new one is much simpler to apply since it behaves like a standard
elimination principle: @(subaddressing_mode_elim \ldots x) where x is
the thing to eliminate.

Location:
src/Clight
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Csem.ma

    r1988 r2032  
    197197      [ Vint sz1 n1 ⇒ match v2 with
    198198          [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
    199                           (λn1. Some ? (Vint sz2 (\snd (split ??? (multiplication ? n1 n2))))) (None ?)
     199                          (λn1. Some ? (Vint sz2 (\snd (vsplit ??? (multiplication ? n1 n2))))) (None ?)
    200200        | _ ⇒ None ? ]
    201201      | _ ⇒ None ? ]
  • src/Clight/SimplifyCasts.ma

    r2030 r2032  
    4646  reduce_bits n m exp v = Some ? v' → v' = truncate n (S m) v.
    4747#n #m elim n
    48 [ 1: #exp #v #v' #H normalize in v v' H; destruct normalize >split_O_n //
     48[ 1: #exp #v #v' #H normalize in v v' H; destruct normalize >vsplit_O_n //
    4949| 2: #n' #Hind #exp #v #v' #H >truncate_tail
    5050 > (Hind ??? (reduce_bits_ok ?? exp v v' H)) // ] qed.
     
    328328qed.
    329329 
    330 lemma split_eq : ∀A. ∀m,n. ∀v : Vector A ((S m) + n).  ∃v1:Vector A (S m). ∃v2:Vector A n. v = v1 @@ v2.
     330lemma vsplit_eq : ∀A. ∀m,n. ∀v : Vector A ((S m) + n).  ∃v1:Vector A (S m). ∃v2:Vector A n. v = v1 @@ v2.
    331331# A #m #n elim m
    332332[ 1: normalize #v
     
    343343] qed.
    344344
    345 lemma split_eq2 : ∀A. ∀m,n : nat. ∀v : Vector A (m + n).  ∃v1:Vector A m. ∃v2:Vector A n. v = v1 @@ v2.
     345lemma vsplit_eq2 : ∀A. ∀m,n : nat. ∀v : Vector A (m + n).  ∃v1:Vector A m. ∃v2:Vector A n. v = v1 @@ v2.
    346346# A #m #n elim m
    347347[ 1: normalize #v @(ex_intro … (VEmpty ?)) @(ex_intro … v) normalize //
     
    355355] qed.
    356356
    357 lemma split_zero:
     357lemma vsplit_zero:
    358358  ∀A,m.
    359359  ∀v: Vector A m.
    360     〈[[]], v〉 = split A 0 m v.
     360    〈[[]], v〉 = vsplit A 0 m v.
    361361  #A #m #v
    362362  elim v
     
    368368
    369369
    370 lemma split_zero2:
     370lemma vsplit_zero2:
    371371  ∀A,m.
    372372  ∀v: Vector A m.
    373     〈[[]], v〉 = split' A 0 m v.
     373    〈[[]], v〉 = vsplit' A 0 m v.
    374374  #A #m #v
    375375  elim v
     
    382382(* This is not very nice. Note that this axiom was copied verbatim from ASM/AssemblyProof.ma.
    383383 * TODO sync with AssemblyProof.ma, in a better world we shouldn't have to copy all of this. *)
    384 axiom split_succ:
     384axiom vsplit_succ:
    385385  ∀A, m, n.
    386386  ∀l: Vector A m.
     
    388388  ∀v: Vector A (m + n).
    389389  ∀hd.
    390     v = l@@r → (〈l, r〉 = split ? m n v → 〈hd:::l, r〉 = split ? (S m) n (hd:::v)).
    391 
    392 axiom split_succ2:
     390    v = l@@r → (〈l, r〉 = vsplit ? m n v → 〈hd:::l, r〉 = vsplit ? (S m) n (hd:::v)).
     391
     392axiom vsplit_succ2:
    393393  ∀A, m, n.
    394394  ∀l: Vector A m.
     
    396396  ∀v: Vector A (m + n).
    397397  ∀hd.
    398     v = l@@r → (〈l, r〉 = split' ? m n v → 〈hd:::l, r〉 = split' ? (S m) n (hd:::v)).
     398    v = l@@r → (〈l, r〉 = vsplit' ? m n v → 〈hd:::l, r〉 = vsplit' ? (S m) n (hd:::v)).
    399399     
    400 lemma split_prod2:
     400lemma vsplit_prod2:
    401401  ∀A,m,n.
    402402  ∀p: Vector A (m + n).
    403403  ∀v: Vector A m.
    404404  ∀q: Vector A n.
    405     p = v@@q → 〈v, q〉 = split' A m n p.
     405    p = v@@q → 〈v, q〉 = vsplit' A m n p.
    406406  #A #m
    407407  elim m
     
    409409    >hyp <(vector_append_zero A n q v)
    410410    >(prod_vector_zero_eq_left A …)
    411     @split_zero2
     411    @vsplit_zero2
    412412  | #r #ih #n #p #v #q #hyp
    413413    >hyp
     
    416416    cases exists
    417417    #tl #jmeq >jmeq
    418     @split_succ2 [1: % |2: @ih % ]
     418    @vsplit_succ2 [1: % |2: @ih % ]
    419419  ]
    420420qed.
    421421
    422 lemma split_prod:
     422lemma vsplit_prod:
    423423  ∀A,m,n.
    424424  ∀p: Vector A (m + n).
    425425  ∀v: Vector A m.
    426426  ∀q: Vector A n.
    427     p = v@@q → 〈v, q〉 = split A m n p.
     427    p = v@@q → 〈v, q〉 = vsplit A m n p.
    428428  #A #m
    429429  elim m
     
    431431    >hyp <(vector_append_zero A n q v)
    432432    >(prod_vector_zero_eq_left A …)
    433     @split_zero
     433    @vsplit_zero
    434434  | #r #ih #n #p #v #q #hyp
    435435    >hyp
     
    438438    cases exists
    439439    #tl #jmeq >jmeq
    440     @split_succ [1: % |2: @ih % ]
    441   ]
    442 qed.
    443 
    444 
    445 (* Stolen from AssemblyProof.ma *)
    446 lemma super_rewrite2:
    447  ∀A:Type[0].∀n,m.∀v1: Vector A n.∀v2: Vector A m.
    448   ∀P: ∀m. Vector A m → Prop.
    449    n=m → v1 ≃ v2 → P n v1 → P m v2.
    450  #A #n #m #v1 #v2 #P #EQ <EQ in v2; #V #JMEQ >JMEQ //
    451 qed.
    452 
    453 lemma vector_cons_append:
    454   ∀A: Type[0].
    455   ∀n: nat.
    456   ∀e: A.
    457   ∀v: Vector A n.
    458     e ::: v = [[ e ]] @@ v.
    459   # A # N # E # V
    460   elim V
    461   [ normalize %
    462   | # NN # AA # VV # IH
    463     normalize
    464     %
    465 qed.
    466 
    467 lemma vector_cons_append2:
    468   ∀A: Type[0].
    469   ∀n, m: nat.
    470   ∀v: Vector A n.
    471   ∀q: Vector A m.
    472   ∀hd: A.
    473     hd:::(v@@q) = (hd:::v)@@q.
    474   #A #n #m #v #q
    475   elim v
    476   [ #hd %
    477   | #n' #hd' #tl' #ih #hd' <ih %
    478   ]
    479 qed.
    480 
    481 lemma jmeq_cons_vector_monotone:
    482   ∀A: Type[0].
    483   ∀m, n: nat.
    484   ∀v: Vector A m.
    485   ∀q: Vector A n.
    486   ∀prf: m = n.
    487   ∀hd: A.
    488     v ≃ q → hd:::v ≃ hd:::q.
    489   #A #m #n #v #q #prf #hd #E
    490   @(super_rewrite2 A … E)
    491   [ assumption | % ]
    492 qed.
    493 
    494 lemma vector_associative_append:
    495   ∀A: Type[0].
    496   ∀n, m, o:  nat.
    497   ∀v: Vector A n.
    498   ∀q: Vector A m.
    499   ∀r: Vector A o.
    500     ((v @@ q) @@ r)
    501     ≃
    502     (v @@ (q @@ r)).
    503   #A #n #m #o #v #q #r
    504   elim v
    505   [ %
    506   | #n' #hd #tl #ih
    507     <(vector_cons_append2 A … hd)
    508     @jmeq_cons_vector_monotone
    509     //
     440    @vsplit_succ [1: % |2: @ih % ]
    510441  ]
    511442qed.
     
    514445#s1 #v normalize elim s1 normalize nodelta
    515446normalize in v;
    516 elim (split_eq ??? (v⌈Vector bool 32 ↦ Vector bool (16 + 16)⌉))
     447elim (vsplit_eq ??? (v⌈Vector bool 32 ↦ Vector bool (16 + 16)⌉))
    517448[ 2,4: //
    518449| 1,3: #l * #r normalize nodelta #Eq1
    519        <(split_prod bool 16 16 … Eq1)
    520        elim (split_eq ??? (r⌈Vector bool 16 ↦ Vector bool (8 + 8)⌉))
     450       <(vsplit_prod bool 16 16 … Eq1)
     451       elim (vsplit_eq ??? (r⌈Vector bool 16 ↦ Vector bool (8 + 8)⌉))
    521452       [ 2,4: //
    522453       | 1,3: #lr * #rr normalize nodelta #Eq2
    523               <(split_prod bool 8 8 … Eq2)
     454              <(vsplit_prod bool 8 8 … Eq2)
    524455              cut (v = (l @@ lr) @@ rr)
    525456              [ 1,3 : destruct >(vector_associative_append ? 16 8) //
    526457              | 2,4: #Hrewrite destruct
    527                      <(split_prod bool 24 8 … Hrewrite) @refl
     458                     <(vsplit_prod bool 24 8 … Hrewrite) @refl
    528459              ]
    529460       ]
     
    555486| 22: normalize elim b_sg elim a_sg normalize
    556487      normalize in val;
    557       elim (split_eq ??? (val⌈Vector bool 32 ↦ Vector bool (16 + 16)⌉))
     488      elim (vsplit_eq ??? (val⌈Vector bool 32 ↦ Vector bool (16 + 16)⌉))
    558489      [ 2,4,6,8: normalize //
    559490      | 1,3,5,7: #left * #right normalize #Eq1
    560                  <(split_prod bool 16 16 … Eq1)
    561                  elim (split_eq ??? (right⌈Vector bool 16 ↦ Vector bool (8 + 8)⌉))
     491                 <(vsplit_prod bool 16 16 … Eq1)
     492                 elim (vsplit_eq ??? (right⌈Vector bool 16 ↦ Vector bool (8 + 8)⌉))
    562493                 [ 2,4,6,8: //
    563494                 | 1,3,5,7: #rightleft * #rightright normalize #Eq2
    564                             <(split_prod bool 8 8 … Eq2)
     495                            <(vsplit_prod bool 8 8 … Eq2)
    565496                            cut (val = (left @@ rightleft) @@ rightright)
    566497                            [ 1,3,5,7: destruct >(vector_associative_append ? 16 8) //
    567498                            | 2,4,6,8: #Hrewrite destruct
    568                                        <(split_prod bool 24 8 … Hrewrite) @refl
     499                                       <(vsplit_prod bool 24 8 … Hrewrite) @refl
    569500                            ]
    570501                 ]
     
    616547>Heq in i; #i @i qed.
    617548
    618 (* cast_int_int behaves as truncate (≃ split) when downsizing *)
     549(* cast_int_int behaves as truncate (≃ vsplit) when downsizing *)
    619550(* ∀src_sz,target_sz,sg. ∀i. size_le target_sz src_sz → cast_int_int src_sz sg target_sz i = truncate *)
    620551
    621 lemma split_to_truncate : ∀m,n,i. (\snd  (split bool m n i)) = truncate  m n i.
     552lemma vsplit_to_truncate : ∀m,n,i. (\snd  (vsplit bool m n i)) = truncate  m n i.
    622553#m #n #i normalize // qed.
    623554
     
    640571  whd in match (addition_n ???);
    641572  whd in match (addition_n ???) in ⊢ (???%);
    642   >split_to_truncate >split_to_truncate
     573  >vsplit_to_truncate >vsplit_to_truncate
    643574  <truncate_add_with_carries
    644575  [ 1,2: normalize in match (plus 8 8); generalize in match (add_with_carries ? lint rint false);
     
    677608@(ex_intro … tl)
    678609>Heq >Heq
    679 elim (split_eq2 … tl) #l * #r #Eq
     610elim (vsplit_eq2 … tl) #l * #r #Eq
    680611normalize
    681  <(split_prod bool n m tl l r Eq)
    682  <(split_prod2 bool n m tl l r Eq)
     612 <(vsplit_prod bool n m tl l r Eq)
     613 <(vsplit_prod2 bool n m tl l r Eq)
    683614 normalize //
    684615qed.
     
    690621     whd in match (truncate ???);
    691622     whd in match (truncate ???) in ⊢ (???%);
    692      <split_zero <split_zero //
     623     <vsplit_zero <vsplit_zero //
    693624| 2: #m' #Hind #n #i normalize in i;
    694625     elim (Vector_Sn … i) #hd * #tl #Heq     
     
    713644          * #Left #Right normalize nodelta
    714645          #H generalize in ⊢ (???(???(????(???(match % with [ _ ⇒ ? | _ ⇒  ?])))));
    715           #b >(split_to_truncate (S m')) >truncate_tail
     646          #b >(vsplit_to_truncate (S m')) >truncate_tail
    716647          cases b
    717648          normalize nodelta
     
    736667  whd in match (subtraction ???);
    737668  whd in match (subtraction ???) in ⊢ (???%);
    738   >split_to_truncate >split_to_truncate
     669  >vsplit_to_truncate >vsplit_to_truncate
    739670  >integer_neg_trunc <truncate_add_with_carries
    740671  [ 1,2: normalize in match (plus 8 8); generalize in match (add_with_carries ? lint ? false);
  • src/Clight/casts.ma

    r1599 r2032  
    22
    33definition truncate : ∀m,n. BitVector (m+n) → BitVector n ≝
    4 λm,n,x. \snd (split … x).
    5 
    6 lemma split_O_n : ∀A,n,x. split A O n x = 〈[[ ]], x〉.
     4λm,n,x. \snd (vsplit … x).
     5
     6lemma vsplit_O_n : ∀A,n,x. vsplit A O n x = 〈[[ ]], x〉.
    77#A #n cases n [ #x @(vector_inv_n … x) @refl | #m #x @(vector_inv_n … x) // ]
    88qed.
    99
    1010lemma truncate_eq : ∀n,x. truncate 0 n x = x.
    11 #n #x normalize >split_O_n @refl
     11#n #x normalize >vsplit_O_n @refl
    1212qed.
    1313
     
    6666qed.
    6767
    68 lemma split_eq' : ∀A,m,n,v. split A m n v = split' A m n v.
     68lemma vsplit_eq' : ∀A,m,n,v. vsplit A m n v = vsplit' A m n v.
    6969#A #m cases m
    7070[ #n cases n
     
    7575] qed. 
    7676
    77 lemma split_left : ∀A,m,n,h,t.
    78   split A (S m) n (h:::t) = (let 〈l,r〉 ≝ split A m n t in 〈h:::l,r〉).
    79 #A #m #n #h #t normalize >split_eq' @refl
     77lemma vsplit_left : ∀A,m,n,h,t.
     78  vsplit A (S m) n (h:::t) = (let 〈l,r〉 ≝ vsplit A m n t in 〈h:::l,r〉).
     79#A #m #n #h #t normalize >vsplit_eq' @refl
    8080qed.
    8181
    8282lemma truncate_head : ∀m,n,h,t.
    8383  truncate (S m) n (h:::t) = truncate m n t.
    84 #m #n #h #t normalize >split_eq' cases (split' bool m n t) //
     84#m #n #h #t normalize >vsplit_eq' cases (vsplit' bool m n t) //
    8585qed.
    8686
Note: See TracChangeset for help on using the changeset viewer.