source: src/Clight/casts.ma @ 961

Last change on this file since 961 was 961, checked in by campbell, 8 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.