# source:src/Clight/casts.ma@886

Last change on this file since 886 was 824, checked in by campbell, 10 years ago

Some work on showing that casts around integer operations can be removed.

File size: 7.5 KB
Line
1include "common/Integers.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 #x elim 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
40  add_with_carries n x y c = fold_right2_i ????? n x y.
41// qed.
42
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
48> (fold_right2_i_unfold ???? hx hy ? 〈[[ ]],[[ ]]〉 x y)
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
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  //
85  qed.
86
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)
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
105qed.
106
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.
116#m #n #x #y <(truncate_pad m n x) in ⊢ (???%) <(truncate_pad m n y) in ⊢ (???%)
117@truncate_plus
118qed.
119
120definition sign_bit : ∀n. BitVector n → bool ≝
121λn,v. match v with [ VEmpty ⇒ false | VCons _ h _ ⇒ h ].
122
123definition sign : ∀m,n. BitVector m → BitVector (n+m) ≝
124λm,n,v. pad_vector ? (sign_bit ? v) ?? v.
125
126lemma truncate_sign : ∀m,n,x.
127  truncate m n (sign … x) = x.
128#m0 elim m0
129[ #n #x >truncate_eq //
130| #m #IH #n #x >truncate_tail normalize in ⊢ (??(???%)?) @IH
131] qed.
132
133theorem sign_plus_reduce : ∀m,n,x,y.
134  truncate m n (addition_n (m+n) (sign … x) (sign … y)) = addition_n n x y.
135#m #n #x #y <(truncate_sign m n x) in ⊢ (???%) <(truncate_sign m n y) in ⊢ (???%)
136@truncate_plus
137qed.
138
139lemma sign_zero : ∀n,x.
140  sign n O x = x.
141#n #x @refl qed.
142
143lemma sign_vcons : ∀m,n,x.
144  sign m (S n) x = (sign_bit ? x):::(sign m n x).
145#m #n #x @refl
146qed.
147
148lemma sign_vcons_hd : ∀m,n,h,t.
149  sign (S m) (S n) (h:::t) = h:::(sign (S m) n (h:::t)).
150// qed.
151
152lemma zero_vcons : ∀m.
153  zero (S m) = false:::(zero m).
154// qed.
155
156lemma zero_sign : ∀m,n.
157  sign m n (zero ?) = zero ?.
158#m #n elim n
159[ //
160| #n' #IH >sign_vcons >IH elim m //
161] qed.
162
164  add_with_carries (S n) (hx:::x) (hy:::y) c
165  = (let 〈rs,cs〉 ≝ add_with_carries n x y c in 〈?:::rs, ?:::cs〉).
166[ #n #hx #hy #x #y #c
168  > (fold_right2_i_unfold ???? hx hy ? 〈[[ ]],[[ ]]〉 x y)
170  cases (add_with_carries n x y c)
171  //
172| *: skip
173]
174qed.
175
176lemma sign_bitflip : ∀m,n,x.
177  negation_bv ? (sign (S m) n x) = sign (S m) n (negation_bv ? x).
178#m #n #x @(vector_inv_n … x) #h #t elim n
179[ @refl
180| #n' #IH >sign_vcons whd in ⊢ (??%?) >IH @refl
181] qed.
182
183lemma truncate_negation_bv : ∀m,n,x.
184  truncate m n (negation_bv ? x) = negation_bv ? (truncate m n x).
185#m #n elim m
186[ #x >truncate_eq >truncate_eq @refl
187| #m' #IH #x @(vector_inv_n … x) #h #t >truncate_tail >truncate_tail
188  >(IH t) @refl
189] qed.
190
191lemma truncate_zero : ∀m,n.
192  truncate m n (zero ?) = zero ?.
193#m #n elim m
194[ >truncate_eq @refl
195| #m' #IH >truncate_tail >zero_vcons <IH @refl
196] qed.
197
198lemma zero_negate_reduce : ∀m,n,x.
199  truncate m (S n) (two_complement_negation (m+S n) (pad … x)) = two_complement_negation ? x.
200#m #n #x whd in ⊢ (??(???%)%)
201lapply (truncate_add_with_carries m (S n) (negation_bv (m+S n) (pad m (S n) x)) (zero ?) true)
202cases (add_with_carries (m + S n) (negation_bv (m+S n) (pad m (S n) x)) (zero ?) true)
203#rs #cs whd in ⊢ (??%? → ??(???%)?)
204>truncate_negation_bv
206#rs' #cs' #E destruct //
207qed.
208
209lemma sign_negate_reduce : ∀m,n,x.
210  truncate m (S n) (two_complement_negation (m+S n) (sign … x)) = two_complement_negation ? x.
211#m #n #x whd in ⊢ (??(???%)%)
212>sign_bitflip <(zero_sign (S n) m)
213lapply (truncate_add_with_carries m (S n) (sign (S n) m (negation_bv (S n) x)) (sign (S n) m (zero (S n))) true)
214cases (add_with_carries (m + S n) (sign (S n) m (negation_bv (S n) x)) (sign (S n) m (zero (S n))) true)
215#rs #cs whd in ⊢ (??%? → ??(???%)?)
217#rs' #cs' #E destruct //
218qed.
219
220theorem zero_subtract_reduce : ∀m,n,x,y.
221  truncate m (S n) (subtraction … (pad … x) (pad … y)) = subtraction … x y.
222#m #n #x #y
223whd in ⊢ (??(???%)%)
226#rs #cs whd in ⊢ (??%? → ??(???%)?)
229#rs' #cs' #E destruct @refl
230qed.
231
232theorem sign_subtract_reduce : ∀m,n,x,y.
233  truncate m (S n) (subtraction … (sign … x) (sign … y)) = subtraction … x y.
234#m #n #x #y
235whd in ⊢ (??(???%)%)
236lapply (truncate_add_with_carries m (S n) (sign (S n) m x) (two_complement_negation (m+S n) (sign (S n) m y)) false)
237cases (add_with_carries (m+S n) (sign (S n) m x) (two_complement_negation (m+S n) (sign (S n) m y)) false)
238#rs #cs whd in ⊢ (??%? → ??(???%)?)
239>sign_negate_reduce >truncate_sign