source: src/Clight/casts.ma @ 3178

Last change on this file since 3178 was 2032, checked in by sacerdot, 7 years ago

!! 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.

File size: 7.8 KB
Line 
1include "common/Values.ma".
2
3definition truncate : ∀m,n. BitVector (m+n) → BitVector n ≝
4λm,n,x. \snd (vsplit … x).
5
6lemma vsplit_O_n : ∀A,n,x. vsplit 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 >vsplit_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
43(* add_with_carries was changed to make it whd nicely in some places, but we
44   want to undo that for some lemmas. *)
45lemma bool_eta : ∀A:Type[0].∀b. ∀P:bool → A. if b then P true else P false = P b.
46#A * // qed.
47
48lemma add_with_carries_extend : ∀n,hx,hy,x,y,c.
49  (let 〈rs,cs〉 ≝ add_with_carries (S n) (hx:::x) (hy:::y) c
50  in 〈tail ?? rs, tail ?? cs〉) = add_with_carries n x y c.
51#n #hx #hy #x #y #c
52>add_with_carries_unfold
53> (fold_right2_i_unfold ???? hx hy ? 〈[[ ]],[[ ]]〉 x y)
54<add_with_carries_unfold
55cases (add_with_carries n x y c)
56#rs' #cs' whd in ⊢ (??(match % with [ _ ⇒ ? ])?); >bool_eta //
57qed.
58
59lemma tail_plus_1 : ∀n,hx,hy,x,y.
60  tail … (addition_n (S n) (hx:::x) (hy:::y)) = addition_n … x y.
61#n #hx #hy #x #y
62whd in ⊢ (??(???%)%);
63<(add_with_carries_extend n hx hy x y false)
64cases (add_with_carries (S n) (hx:::x) (hy:::y) false)
65//
66qed.
67
68lemma vsplit_eq' : ∀A,m,n,v. vsplit A m n v = vsplit' A m n v.
69#A #m cases m
70[ #n cases n
71  [ #v >(vempty … v) @refl
72  | #n' #v >(hdtl … v) //
73  ]
74| #m' #n #v >(hdtl … v) //
75] qed. 
76
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
80qed.
81
82lemma truncate_head : ∀m,n,h,t.
83  truncate (S m) n (h:::t) = truncate m n t.
84#m #n #h #t normalize >vsplit_eq' cases (vsplit' bool m n t) //
85qed.
86
87lemma truncate_tail : ∀m,n,v.
88  truncate (S m) n v = truncate m n (tail … v).
89#m #n #v @(vector_inv_n … v) #h #t >truncate_head @refl
90  qed.
91
92lemma truncate_add_with_carries : ∀m,n,x,y,c.
93  (let 〈rs,cs〉 ≝ add_with_carries … x y c in 〈truncate m n rs, truncate m n cs〉) =
94  add_with_carries … (truncate … x) (truncate … y) c.
95#m elim m
96[ #n #x #y #c >truncate_eq >truncate_eq cases (add_with_carries n x y c) #rs #cs
97  whd in ⊢ (??%?); >truncate_eq >truncate_eq  @refl
98| #m' #IH #n #x #y #c
99  >(hdtl … x) >(hdtl … y)
100  >truncate_head >truncate_head <IH
101  <(add_with_carries_extend ? (head' ?? x) (head' ?? y) (tail ?? x) (tail ?? y))
102  cases (add_with_carries ????) #rs #cs whd in ⊢ (??%%);
103  <truncate_tail <truncate_tail @refl
104] qed.
105
106lemma truncate_plus : ∀m,n,x,y.
107  truncate m n (addition_n … x y) = addition_n … (truncate … x) (truncate … y).
108#m #n #x #y whd in ⊢ (??(???%)%); <truncate_add_with_carries
109cases (add_with_carries ????) //
110qed.
111
112lemma truncate_pad : ∀m,n,x.
113  truncate m n (pad … x) = x.
114#m0 elim m0
115[ #n #x >truncate_eq //
116| #m #IH #n #x >truncate_tail normalize in ⊢ (??(???%)?); @IH
117] qed.
118
119theorem zero_plus_reduce : ∀m,n,x,y.
120  truncate m n (addition_n (m+n) (pad … x) (pad … y)) = addition_n n x y.
121#m #n #x #y <(truncate_pad m n x) in ⊢ (???%); <(truncate_pad m n y) in ⊢ (???%);
122@truncate_plus
123qed.
124
125definition sign : ∀m,n. BitVector m → BitVector (n+m) ≝
126λm,n,v. pad_vector ? (sign_bit ? v) ?? v.
127 
128lemma truncate_sign : ∀m,n,x.
129  truncate m n (sign … x) = x.
130#m0 elim m0
131[ #n #x >truncate_eq //
132| #m #IH #n #x >truncate_tail normalize in ⊢ (??(???%)?); @IH
133] qed.
134
135theorem sign_plus_reduce : ∀m,n,x,y.
136  truncate m n (addition_n (m+n) (sign … x) (sign … y)) = addition_n n x y.
137#m #n #x #y <(truncate_sign m n x) in ⊢ (???%); <(truncate_sign m n y) in ⊢ (???%);
138@truncate_plus
139qed.
140
141lemma sign_zero : ∀n,x.
142  sign n O x = x.
143#n #x @refl qed.
144
145lemma sign_vcons : ∀m,n,x.
146  sign m (S n) x = (sign_bit ? x):::(sign m n x).
147#m #n #x @refl
148qed.
149
150lemma sign_vcons_hd : ∀m,n,h,t.
151  sign (S m) (S n) (h:::t) = h:::(sign (S m) n (h:::t)).
152// qed.
153
154lemma zero_vcons : ∀m.
155  zero (S m) = false:::(zero m).
156// qed.
157
158lemma zero_sign : ∀m,n.
159  sign m n (zero ?) = zero ?.
160#m #n elim n
161[ //
162| #n' #IH >sign_vcons >IH elim m //
163] qed.
164
165lemma add_with_carries_vcons : ∀n,hx,hy,x,y,c.
166  add_with_carries (S n) (hx:::x) (hy:::y) c
167  = (let 〈rs,cs〉 ≝ add_with_carries n x y c in 〈?:::rs, ?:::cs〉).
168[ #n #hx #hy #x #y #c
169  >add_with_carries_unfold
170  > (fold_right2_i_unfold ???? hx hy ? 〈[[ ]],[[ ]]〉 x y)
171  <add_with_carries_unfold
172  cases (add_with_carries n x y c)
173  #lb #cs whd in ⊢ (??%%); >bool_eta
174  //
175| *: skip
176]
177qed.
178
179lemma sign_bitflip : ∀m,n,x.
180  negation_bv ? (sign (S m) n x) = sign (S m) n (negation_bv ? x).
181#m #n #x @(vector_inv_n … x) #h #t elim n
182[ @refl
183| #n' #IH >sign_vcons whd in IH:(??%?) ⊢ (??%?); >IH @refl
184] qed.
185
186lemma truncate_negation_bv : ∀m,n,x.
187  truncate m n (negation_bv ? x) = negation_bv ? (truncate m n x).
188#m #n elim m
189[ #x >truncate_eq >truncate_eq @refl
190| #m' #IH #x @(vector_inv_n … x) #h #t >truncate_tail >truncate_tail
191  >(IH t) @refl
192] qed.
193
194lemma truncate_zero : ∀m,n.
195  truncate m n (zero ?) = zero ?.
196#m #n elim m
197[ >truncate_eq @refl
198| #m' #IH >truncate_tail >zero_vcons <IH @refl
199] qed.
200
201lemma zero_negate_reduce : ∀m,n,x.
202  truncate m (S n) (two_complement_negation (m+S n) (pad … x)) = two_complement_negation ? x.
203#m #n #x whd in ⊢ (??(???%)%);
204lapply (truncate_add_with_carries m (S n) (negation_bv (m+S n) (pad m (S n) x)) (zero ?) true)
205cases (add_with_carries (m + S n) (negation_bv (m+S n) (pad m (S n) x)) (zero ?) true)
206#rs #cs whd in ⊢ (??%? → ??(???%)?);
207>truncate_negation_bv
208>truncate_pad >truncate_zero cases (add_with_carries ????)
209#rs' #cs' #E destruct //
210qed.
211
212lemma sign_negate_reduce : ∀m,n,x.
213  truncate m (S n) (two_complement_negation (m+S n) (sign … x)) = two_complement_negation ? x.
214#m #n #x whd in ⊢ (??(???%)%);
215>sign_bitflip <(zero_sign (S n) m)
216lapply (truncate_add_with_carries m (S n) (sign (S n) m (negation_bv (S n) x)) (sign (S n) m (zero (S n))) true)
217cases (add_with_carries (m + S n) (sign (S n) m (negation_bv (S n) x)) (sign (S n) m (zero (S n))) true)
218#rs #cs whd in ⊢ (??%? → ??(???%)?);
219>truncate_sign >truncate_sign cases (add_with_carries ????)
220#rs' #cs' #E destruct //
221qed.
222
223theorem zero_subtract_reduce : ∀m,n,x,y.
224  truncate m (S n) (subtraction … (pad … x) (pad … y)) = subtraction … x y.
225#m #n #x #y
226whd in ⊢ (??(???%)%);
227lapply (truncate_add_with_carries m (S n) (pad … x) (two_complement_negation (m+S n) (pad … y)) false)
228cases (add_with_carries (m+S n) (pad … x) (two_complement_negation (m+S n) (pad … y)) false)
229#rs #cs whd in ⊢ (??%? → ??(???%)?);
230>zero_negate_reduce >truncate_pad
231cases (add_with_carries ????)
232#rs' #cs' #E destruct @refl
233qed.
234
235theorem sign_subtract_reduce : ∀m,n,x,y.
236  truncate m (S n) (subtraction … (sign … x) (sign … y)) = subtraction … x y.
237#m #n #x #y
238whd in ⊢ (??(???%)%);
239lapply (truncate_add_with_carries m (S n) (sign (S n) m x) (two_complement_negation (m+S n) (sign (S n) m y)) false)
240cases (add_with_carries (m+S n) (sign (S n) m x) (two_complement_negation (m+S n) (sign (S n) m y)) false)
241#rs #cs whd in ⊢ (??%? → ??(???%)?);
242>sign_negate_reduce >truncate_sign
243cases (add_with_carries ????)
244#rs' #cs' #E destruct @refl
245qed.
Note: See TracBrowser for help on using the repository browser.