source: src/Clight/casts.ma @ 1326

Last change on this file since 1326 was 961, checked in by campbell, 10 years ago

Use precise bitvector sizes throughout the front end, rather than 32bits
everywhere.

File size: 7.5 KB
Line 
1include "common/Values.ma".
2
3definition truncate : ∀m,n. BitVector (m+n) → BitVector n ≝
4λm,n,x. \snd (split … x).
5
6lemma split_O_n : ∀A,n,x. split A O n x = 〈[[ ]], x〉.
7#A #n cases n [ #x @(vector_inv_n … x) @refl | #m #x @(vector_inv_n … x) // ]
8qed.
9
10lemma truncate_eq : ∀n,x. truncate 0 n x = x.
11#n #x normalize >split_O_n @refl
12qed.
13
14lemma hdtl : ∀A,n. ∀x:Vector A (S n). x = (head' … x):::(tail … x).
15#A #n #x
16@(match x return λn.
17    match n return λn.Vector A n → Prop with
18    [ O ⇒ λ_.True
19    | S m ⇒ λx:Vector A (S m). x = (head' A m x):::(tail A m x) ]
20  with [ VEmpty ⇒ I | VCons p h t ⇒ ? ])
21@refl
22qed.
23
24lemma vempty : ∀A. ∀x:Vector A O. x = [[ ]].
25#A #x
26@(match x return λn.
27    match n return λn.Vector A n → Prop with
28    [ O ⇒ λx.x = [[ ]]
29    | _ ⇒ λ_.True ]
30  with [ VEmpty ⇒ ? | VCons _ _ _ ⇒ I ])
31@refl
32qed.
33
34lemma fold_right2_i_unfold : ∀A,B,C,n,hx,hy,f,a,x,y.
35  fold_right2_i A B C f a ? (hx:::x) (hy:::y) =
36  f ? hx hy (fold_right2_i A B C f a n x y).
37// qed.
38
39lemma add_with_carries_unfold : ∀n,x,y,c.
40  add_with_carries n x y c = fold_right2_i ????? n x y.
41// qed.
42
43lemma add_with_carries_extend : ∀n,hx,hy,x,y,c.
44  (let 〈rs,cs〉 ≝ add_with_carries (S n) (hx:::x) (hy:::y) c
45  in 〈tail ?? rs, tail ?? cs〉) = add_with_carries n x y c.
46#n #hx #hy #x #y #c
47>add_with_carries_unfold
48> (fold_right2_i_unfold ???? hx hy ? 〈[[ ]],[[ ]]〉 x y)
49<add_with_carries_unfold
50cases (add_with_carries n x y c)
51//
52qed.
53
54lemma tail_plus_1 : ∀n,hx,hy,x,y.
55  tail … (addition_n (S n) (hx:::x) (hy:::y)) = addition_n … x y.
56#n #hx #hy #x #y
57whd in ⊢ (??(???%)%)
58<(add_with_carries_extend n hx hy x y false)
59cases (add_with_carries (S n) (hx:::x) (hy:::y) false)
60//
61qed.
62
63lemma split_eq' : ∀A,m,n,v. split A m n v = split' A m n v.
64#A #m cases m
65[ #n cases n
66  [ #v >(vempty … v) @refl
67  | #n' #v >(hdtl … v) //
68  ]
69| #m' #n #v >(hdtl … v) //
70] qed. 
71
72lemma split_left : ∀A,m,n,h,t.
73  split A (S m) n (h:::t) = let 〈l,r〉 ≝ split A m n t in 〈h:::l,r〉.
74#A #m #n #h #t normalize >split_eq' @refl
75qed.
76
77lemma truncate_head : ∀m,n,h,t.
78  truncate (S m) n (h:::t) = truncate m n t.
79#m #n #h #t normalize >split_eq' cases (split' bool m n t) //
80qed.
81
82lemma truncate_tail : ∀m,n,v.
83  truncate (S m) n v = truncate m n (tail … v).
84#m #n #v @(vector_inv_n … v) #h #t >truncate_head @refl
85  qed.
86
87lemma truncate_add_with_carries : ∀m,n,x,y,c.
88  (let 〈rs,cs〉 ≝ add_with_carries … x y c in 〈truncate m n rs, truncate m n cs〉) =
89  add_with_carries … (truncate … x) (truncate … y) c.
90#m elim m
91[ #n #x #y #c >truncate_eq >truncate_eq cases (add_with_carries n x y c) #rs #cs
92  whd in ⊢ (??%?) >truncate_eq >truncate_eq  @refl
93| #m' #IH #n #x #y #c
94  >(hdtl … x) >(hdtl … y)
95  >truncate_head >truncate_head <IH
96  <(add_with_carries_extend ? (head' ?? x) (head' ?? y) (tail ?? x) (tail ?? y))
97  cases (add_with_carries ????) #rs #cs whd in ⊢ (??%%)
98  <truncate_tail <truncate_tail @refl
99] qed.
100
101lemma truncate_plus : ∀m,n,x,y.
102  truncate m n (addition_n … x y) = addition_n … (truncate … x) (truncate … y).
103#m #n #x #y whd in ⊢ (??(???%)%) <truncate_add_with_carries
104cases (add_with_carries ????) //
105qed.
106
107lemma truncate_pad : ∀m,n,x.
108  truncate m n (pad … x) = x.
109#m0 elim m0
110[ #n #x >truncate_eq //
111| #m #IH #n #x >truncate_tail normalize in ⊢ (??(???%)?) @IH
112] qed.
113
114theorem zero_plus_reduce : ∀m,n,x,y.
115  truncate m n (addition_n (m+n) (pad … x) (pad … y)) = addition_n n x y.
116#m #n #x #y <(truncate_pad m n x) in ⊢ (???%) <(truncate_pad m n y) in ⊢ (???%)
117@truncate_plus
118qed.
119
120definition sign : ∀m,n. BitVector m → BitVector (n+m) ≝
121λm,n,v. pad_vector ? (sign_bit ? v) ?? v.
122 
123lemma truncate_sign : ∀m,n,x.
124  truncate m n (sign … x) = x.
125#m0 elim m0
126[ #n #x >truncate_eq //
127| #m #IH #n #x >truncate_tail normalize in ⊢ (??(???%)?) @IH
128] qed.
129
130theorem sign_plus_reduce : ∀m,n,x,y.
131  truncate m n (addition_n (m+n) (sign … x) (sign … y)) = addition_n n x y.
132#m #n #x #y <(truncate_sign m n x) in ⊢ (???%) <(truncate_sign m n y) in ⊢ (???%)
133@truncate_plus
134qed.
135
136lemma sign_zero : ∀n,x.
137  sign n O x = x.
138#n #x @refl qed.
139
140lemma sign_vcons : ∀m,n,x.
141  sign m (S n) x = (sign_bit ? x):::(sign m n x).
142#m #n #x @refl
143qed.
144
145lemma sign_vcons_hd : ∀m,n,h,t.
146  sign (S m) (S n) (h:::t) = h:::(sign (S m) n (h:::t)).
147// qed.
148
149lemma zero_vcons : ∀m.
150  zero (S m) = false:::(zero m).
151// qed.
152
153lemma zero_sign : ∀m,n.
154  sign m n (zero ?) = zero ?.
155#m #n elim n
156[ //
157| #n' #IH >sign_vcons >IH elim m //
158] qed.
159
160lemma add_with_carries_vcons : ∀n,hx,hy,x,y,c.
161  add_with_carries (S n) (hx:::x) (hy:::y) c
162  = (let 〈rs,cs〉 ≝ add_with_carries n x y c in 〈?:::rs, ?:::cs〉).
163[ #n #hx #hy #x #y #c
164  >add_with_carries_unfold
165  > (fold_right2_i_unfold ???? hx hy ? 〈[[ ]],[[ ]]〉 x y)
166  <add_with_carries_unfold
167  cases (add_with_carries n x y c)
168  //
169| *: skip
170]
171qed.
172
173lemma sign_bitflip : ∀m,n,x.
174  negation_bv ? (sign (S m) n x) = sign (S m) n (negation_bv ? x).
175#m #n #x @(vector_inv_n … x) #h #t elim n
176[ @refl
177| #n' #IH >sign_vcons whd in IH:(??%?) ⊢ (??%?) >IH @refl
178] qed.
179
180lemma truncate_negation_bv : ∀m,n,x.
181  truncate m n (negation_bv ? x) = negation_bv ? (truncate m n x).
182#m #n elim m
183[ #x >truncate_eq >truncate_eq @refl
184| #m' #IH #x @(vector_inv_n … x) #h #t >truncate_tail >truncate_tail
185  >(IH t) @refl
186] qed.
187
188lemma truncate_zero : ∀m,n.
189  truncate m n (zero ?) = zero ?.
190#m #n elim m
191[ >truncate_eq @refl
192| #m' #IH >truncate_tail >zero_vcons <IH @refl
193] qed.
194
195lemma zero_negate_reduce : ∀m,n,x.
196  truncate m (S n) (two_complement_negation (m+S n) (pad … x)) = two_complement_negation ? x.
197#m #n #x whd in ⊢ (??(???%)%)
198lapply (truncate_add_with_carries m (S n) (negation_bv (m+S n) (pad m (S n) x)) (zero ?) true)
199cases (add_with_carries (m + S n) (negation_bv (m+S n) (pad m (S n) x)) (zero ?) true)
200#rs #cs whd in ⊢ (??%? → ??(???%)?)
201>truncate_negation_bv
202>truncate_pad >truncate_zero cases (add_with_carries ????)
203#rs' #cs' #E destruct //
204qed.
205
206lemma sign_negate_reduce : ∀m,n,x.
207  truncate m (S n) (two_complement_negation (m+S n) (sign … x)) = two_complement_negation ? x.
208#m #n #x whd in ⊢ (??(???%)%)
209>sign_bitflip <(zero_sign (S n) m)
210lapply (truncate_add_with_carries m (S n) (sign (S n) m (negation_bv (S n) x)) (sign (S n) m (zero (S n))) true)
211cases (add_with_carries (m + S n) (sign (S n) m (negation_bv (S n) x)) (sign (S n) m (zero (S n))) true)
212#rs #cs whd in ⊢ (??%? → ??(???%)?)
213>truncate_sign >truncate_sign cases (add_with_carries ????)
214#rs' #cs' #E destruct //
215qed.
216
217theorem zero_subtract_reduce : ∀m,n,x,y.
218  truncate m (S n) (subtraction … (pad … x) (pad … y)) = subtraction … x y.
219#m #n #x #y
220whd in ⊢ (??(???%)%)
221lapply (truncate_add_with_carries m (S n) (pad … x) (two_complement_negation (m+S n) (pad … y)) false)
222cases (add_with_carries (m+S n) (pad … x) (two_complement_negation (m+S n) (pad … y)) false)
223#rs #cs whd in ⊢ (??%? → ??(???%)?)
224>zero_negate_reduce >truncate_pad
225cases (add_with_carries ????)
226#rs' #cs' #E destruct @refl
227qed.
228
229theorem sign_subtract_reduce : ∀m,n,x,y.
230  truncate m (S n) (subtraction … (sign … x) (sign … y)) = subtraction … x y.
231#m #n #x #y
232whd in ⊢ (??(???%)%)
233lapply (truncate_add_with_carries m (S n) (sign (S n) m x) (two_complement_negation (m+S n) (sign (S n) m y)) false)
234cases (add_with_carries (m+S n) (sign (S n) m x) (two_complement_negation (m+S n) (sign (S n) m y)) false)
235#rs #cs whd in ⊢ (??%? → ??(???%)?)
236>sign_negate_reduce >truncate_sign
237cases (add_with_carries ????)
238#rs' #cs' #E destruct @refl
239qed.
Note: See TracBrowser for help on using the repository browser.