source: src/Clight/memoryInjections.ma @ 2312

Last change on this file since 2312 was 2312, checked in by garnier, 7 years ago

Memory injections, to be revised

File size: 52.4 KB
Line 
1include "Clight/Cexec.ma".
2
3(* This file contains some definitions and lemmas related to memory injections.
4   Could be useful for the Clight → Cminor. Needs revision: the definitions are
5   too lax and allow inconsistent embeddings (more precisely, these embeddings do
6   not allow to prove that the semantics for pointer less-than comparisons is
7   conserved). *)
8
9(* --------------------------------------------------------------------------- *)   
10(* Some general lemmas on bitvectors (offsets /are/ bitvectors) *)
11(* --------------------------------------------------------------------------- *)
12 
13lemma add_with_carries_n_O : ∀n,bv. add_with_carries n bv (zero n) false = 〈bv,zero n〉.
14#n #bv whd in match (add_with_carries ????); elim bv //
15#n #hd #tl #Hind whd in match (fold_right2_i ????????);
16>Hind normalize
17cases n in tl;
18[ 1: #tl cases hd normalize @refl
19| 2: #n' #tl cases hd normalize @refl ]
20qed.
21
22lemma addition_n_0 : ∀n,bv. addition_n n bv (zero n) = bv.
23#n #bv whd in match (addition_n ???);
24>add_with_carries_n_O //
25qed.
26
27lemma replicate_Sn : ∀A,sz,elt.
28  replicate A (S sz) elt = elt ::: (replicate A sz elt).
29// qed.
30
31lemma zero_Sn : ∀n. zero (S n) = false ::: (zero n). // qed.
32
33lemma negation_bv_Sn : ∀n. ∀xa. ∀a : BitVector n. negation_bv … (xa ::: a) = (notb xa) ::: (negation_bv … a).
34#n #xa #a normalize @refl qed.
35
36(* useful facts on carry_of *)
37lemma carry_of_TT : ∀x. carry_of true true x = true. // qed.
38lemma carry_of_TF : ∀x. carry_of true false x = x. // qed.
39lemma carry_of_FF : ∀x. carry_of false false x = false. // qed.
40lemma carry_of_lcomm : ∀x,y,z. carry_of x y z = carry_of y x z. * * * // qed.
41lemma carry_of_rcomm : ∀x,y,z. carry_of x y z = carry_of x z y. * * * // qed.
42
43(* useful facts on various boolean operations *)
44lemma andb_lsimpl_true : ∀x. andb true x = x. // qed.
45lemma andb_lsimpl_false : ∀x. andb false x = false. normalize // qed.
46lemma andb_comm : ∀x,y. andb x y = andb y x. // qed.
47lemma notb_true : notb true = false. // qed.
48lemma notb_false : notb false = true. % #H destruct qed.
49lemma notb_fold : ∀x. if x then false else true = (¬x). // qed.
50
51definition one_bv ≝ λn. (\fst (add_with_carries … (zero n) (zero n) true)).
52
53lemma one_bv_Sn_aux : ∀n. ∀bits,flags : BitVector (S n).
54    add_with_carries … (zero (S n)) (zero (S n)) true = 〈bits, flags〉 →
55    add_with_carries … (zero (S (S n))) (zero (S (S n))) true = 〈false ::: bits, false ::: flags〉.
56#n elim n
57[ 1: #bits #flags elim (BitVector_Sn … bits) #hd_bits * #tl_bits #Heq_bits
58     elim (BitVector_Sn … flags) #hd_flags * #tl_flags #Heq_flags
59     >(BitVector_O … tl_flags) >(BitVector_O … tl_bits)
60     normalize #Heq destruct (Heq) @refl
61| 2: #n' #Hind #bits #flags elim (BitVector_Sn … bits) #hd_bits * #tl_bits #Heq_bits
62     destruct #Hind >add_with_carries_Sn >replicate_Sn
63     whd in match (zero ?) in Hind; lapply Hind
64     elim (add_with_carries (S (S n'))
65            (false:::replicate bool (S n') false)
66            (false:::replicate bool (S n') false) true) #bits #flags #Heq destruct
67            normalize >add_with_carries_Sn in Hind;
68     elim (add_with_carries (S n') (replicate bool (S n') false)
69                    (replicate bool (S n') false) true) #flags' #bits'
70     normalize
71     cases (match bits' in Vector return λsz:ℕ.(λfoo:Vector bool sz.bool) with 
72            [VEmpty⇒true|VCons (sz:ℕ)   (cy:bool)   (tl:(Vector bool sz))⇒cy])
73     normalize #Heq destruct @refl
74] qed.     
75
76lemma one_bv_Sn : ∀n. one_bv (S (S n)) = false ::: (one_bv (S n)).
77#n lapply (one_bv_Sn_aux n)
78whd in match (one_bv ?) in ⊢ (? → (??%%));
79elim (add_with_carries (S n) (zero (S n)) (zero (S n)) true) #bits #flags
80#H lapply (H bits flags (refl ??)) #H2 >H2 @refl
81qed.
82
83lemma increment_to_addition_n_aux : ∀n. ∀a : BitVector n.
84    add_with_carries ? a (zero n) true = add_with_carries ? a (one_bv n) false.
85#n   
86elim n
87[ 1: #a >(BitVector_O … a) normalize @refl
88| 2: #n' cases n'
89     [ 1: #Hind #a elim (BitVector_Sn ? a) #xa * #tl #Heq destruct
90          >(BitVector_O … tl) normalize cases xa @refl
91     | 2: #n'' #Hind #a elim (BitVector_Sn ? a) #xa * #tl #Heq destruct
92          >one_bv_Sn >zero_Sn
93          lapply (Hind tl)
94          >add_with_carries_Sn >add_with_carries_Sn
95          #Hind >Hind elim (add_with_carries (S n'') tl (one_bv (S n'')) false) #bits #flags
96          normalize nodelta elim (BitVector_Sn … flags) #flags_hd * #flags_tl #Hflags_eq >Hflags_eq
97          normalize nodelta @refl
98] qed.         
99
100(* In order to use associativity on increment, we hide it under addition_n. *)
101lemma increment_to_addition_n : ∀n. ∀a : BitVector n. increment ? a = addition_n ? a (one_bv n).
102#n
103whd in match (increment ??) in ⊢ (∀_.??%?);
104whd in match (addition_n ???) in ⊢ (∀_.???%);
105#a lapply (increment_to_addition_n_aux n a)
106#Heq >Heq cases (add_with_carries n a (one_bv n) false) #bits #flags @refl
107qed.
108
109(* Explicit formulation of addition *)
110
111(* Explicit formulation of the last carry bit *)
112let rec ith_carry (n : nat) (a,b : BitVector n) (init : bool) on n : bool ≝
113match n return λx. BitVector x → BitVector x → bool with
114[ O ⇒ λ_,_. init
115| S x ⇒ λa',b'.
116  let hd_a ≝ head' … a' in
117  let hd_b ≝ head' … b' in
118  let tl_a ≝ tail … a' in
119  let tl_b ≝ tail … b' in
120  carry_of hd_a hd_b (ith_carry x tl_a tl_b init)
121] a b.
122
123lemma ith_carry_unfold : ∀n. ∀init. ∀a,b : BitVector (S n).
124  ith_carry ? a b init = (carry_of (head' … a) (head' … b) (ith_carry ? (tail … a) (tail … b) init)).
125#n #init #a #b @refl qed.
126
127lemma ith_carry_Sn : ∀n. ∀init. ∀xa,xb. ∀a,b : BitVector n.
128  ith_carry ? (xa ::: a) (xb ::: b) init = (carry_of xa xb (ith_carry ? a b init)). // qed.
129
130(* correction of [ith_carry] *)
131lemma ith_carry_ok : ∀n. ∀init. ∀a,b,res_ab,flags_ab : BitVector (S n).
132  〈res_ab,flags_ab〉 = add_with_carries ? a b init →
133  head' … flags_ab = ith_carry ? a b init.
134#n elim n
135[ 1: #init #a #b #res_ab #flags_ab
136     elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a
137     elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b
138     elim (BitVector_Sn … res_ab) #hd_res * #tl_res #Heq_res
139     elim (BitVector_Sn … flags_ab) #hd_flags * #tl_flags #Heq_flags
140     destruct
141     >(BitVector_O … tl_a) >(BitVector_O … tl_b)
142     cases hd_a cases hd_b cases init normalize #Heq destruct (Heq)
143     @refl
144| 2: #n' #Hind #init #a #b #res_ab #flags_ab
145     elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a
146     elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b
147     elim (BitVector_Sn … res_ab) #hd_res * #tl_res #Heq_res
148     elim (BitVector_Sn … flags_ab) #hd_flags * #tl_flags #Heq_flags
149     destruct
150     lapply (Hind … init tl_a tl_b tl_res tl_flags)
151     >add_with_carries_Sn >(ith_carry_Sn (S n'))
152     elim (add_with_carries (S n') tl_a tl_b init) #res_ab #flags_ab
153     elim (BitVector_Sn … flags_ab) #hd_flags_ab * #tl_flags_ab #Heq_flags_ab >Heq_flags_ab
154     normalize nodelta cases hd_flags_ab normalize nodelta
155     whd in match (head' ? (S n') ?); #H1 #H2
156     destruct (H2) lapply (H1 (refl ??)) whd in match (head' ???); #Heq <Heq @refl
157] qed.
158
159(* Explicit formulation of ith bit of an addition, with explicit initial carry bit. *)
160definition ith_bit ≝ λ(n : nat).λ(a,b : BitVector n).λinit.
161match n return λx. BitVector x → BitVector x → bool with
162[ O ⇒ λ_,_. init
163| S x ⇒ λa',b'.
164  let hd_a ≝ head' … a' in
165  let hd_b ≝ head' … b' in
166  let tl_a ≝ tail … a' in
167  let tl_b ≝ tail … b' in
168  xorb (xorb hd_a hd_b) (ith_carry x tl_a tl_b init)
169] a b.
170
171lemma ith_bit_unfold : ∀n. ∀init. ∀a,b : BitVector (S n).
172  ith_bit ? a b init =  xorb (xorb (head' … a) (head' … b)) (ith_carry ? (tail … a) (tail … b) init).
173#n #a #b // qed.
174
175lemma ith_bit_Sn : ∀n. ∀init. ∀xa,xb. ∀a,b : BitVector n.
176  ith_bit ? (xa ::: a) (xb ::: b) init =  xorb (xorb xa xb) (ith_carry ? a b init). // qed.
177
178(* correction of ith_bit *)
179lemma ith_bit_ok : ∀n. ∀init. ∀a,b,res_ab,flags_ab : BitVector (S n).
180  〈res_ab,flags_ab〉 = add_with_carries ? a b init →
181  head' … res_ab = ith_bit ? a b init.
182#n
183cases n
184[ 1: #init #a #b #res_ab #flags_ab
185     elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a
186     elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b
187     elim (BitVector_Sn … res_ab) #hd_res * #tl_res #Heq_res
188     elim (BitVector_Sn … flags_ab) #hd_flags * #tl_flags #Heq_flags
189     destruct
190     >(BitVector_O … tl_a) >(BitVector_O … tl_b)
191     >(BitVector_O … tl_flags) >(BitVector_O … tl_res)
192     normalize cases init cases hd_a cases hd_b normalize #Heq destruct @refl
193| 2: #n' #init #a #b #res_ab #flags_ab
194     elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a
195     elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b
196     elim (BitVector_Sn … res_ab) #hd_res * #tl_res #Heq_res
197     elim (BitVector_Sn … flags_ab) #hd_flags * #tl_flags #Heq_flags
198     destruct
199     lapply (ith_carry_ok … init tl_a tl_b tl_res tl_flags)
200     #Hcarry >add_with_carries_Sn elim (add_with_carries ? tl_a tl_b init) in Hcarry;
201     #res #flags normalize nodelta elim (BitVector_Sn … flags) #hd_flags' * #tl_flags' #Heq_flags'
202     >Heq_flags' normalize nodelta cases hd_flags' normalize nodelta #H1 #H2 destruct (H2)
203     cases hd_a cases hd_b >ith_bit_Sn whd in match (head' ???) in H1 ⊢ %;
204     <(H1 (refl ??)) @refl
205] qed.
206
207(* Transform a function from bit-vectors to bits into a vector by folding *)
208let rec bitvector_fold (n : nat) (v : BitVector n) (f : ∀sz. BitVector sz → bool) on v : BitVector n ≝
209match v with
210[ VEmpty ⇒ VEmpty ?
211| VCons sz elt tl ⇒
212  let bit ≝ f ? v in
213  bit ::: (bitvector_fold ? tl f)
214].
215
216(* Two-arguments version *)
217let rec bitvector_fold2 (n : nat) (v1, v2 : BitVector n) (f : ∀sz. BitVector sz → BitVector sz → bool) on v1 : BitVector n ≝
218match v1  with
219[ VEmpty ⇒ λ_. VEmpty ?
220| VCons sz elt tl ⇒ λv2'.
221  let bit ≝ f ? v1 v2 in
222  bit ::: (bitvector_fold2 ? tl (tail … v2') f)
223] v2.
224
225lemma bitvector_fold2_Sn : ∀n,x1,x2,v1,v2,f.
226  bitvector_fold2 (S n) (x1 ::: v1) (x2 ::: v2) f = (f ? (x1 ::: v1) (x2 ::: v2)) ::: (bitvector_fold2 … v1 v2 f). // qed.
227
228(* These functions pack all the relevant information (including carries) directly. *)
229definition addition_n_direct ≝ λn,v1,v2,init. bitvector_fold2 n v1 v2 (λn,v1,v2. ith_bit n v1 v2 init).
230
231lemma addition_n_direct_Sn : ∀n,x1,x2,v1,v2,init.
232  addition_n_direct (S n) (x1 ::: v1) (x2 ::: v2) init = (ith_bit ? (x1 ::: v1) (x2 ::: v2) init) ::: (addition_n_direct … v1 v2 init). // qed.
233 
234lemma tail_Sn : ∀n. ∀x. ∀a : BitVector n. tail … (x ::: a) = a. // qed.
235
236(* Prove the equivalence of addition_n_direct with add_with_carries *)
237lemma addition_n_direct_ok : ∀n,carry,v1,v2.
238  (\fst (add_with_carries n v1 v2 carry)) = addition_n_direct n v1 v2 carry.
239#n elim n
240[ 1: #carry #v1 #v2 >(BitVector_O … v1) >(BitVector_O … v2) normalize @refl
241| 2: #n' #Hind #carry #v1 #v2
242     elim (BitVector_Sn … v1) #hd1 * #tl1 #Heq1
243     elim (BitVector_Sn … v2) #hd2 * #tl2 #Heq2
244     lapply (Hind carry tl1 tl2)
245     lapply (ith_bit_ok ? carry v1 v2)
246     lapply (ith_carry_ok ? carry v1 v2)
247     destruct
248     #Hind >addition_n_direct_Sn
249     >ith_bit_Sn >add_with_carries_Sn
250     elim (add_with_carries n' tl1 tl2 carry) #bits #flags normalize nodelta
251     cases (match flags in Vector return λsz:ℕ.(λfoo:Vector bool sz.bool) with 
252            [VEmpty⇒carry|VCons (sz:ℕ)   (cy:bool)   (tl:(Vector bool sz))⇒cy])
253     normalize nodelta #Hcarry' lapply (Hcarry' ?? (refl ??))
254     whd in match head'; normalize nodelta
255     #H1 #H2 >H1 >H2 @refl
256] qed.
257 
258(* trivially lift associativity to our new setting *)     
259lemma associative_addition_n_direct : ∀n. ∀carry1,carry2. ∀v1,v2,v3 : BitVector n.
260  addition_n_direct ? (addition_n_direct ? v1 v2 carry1) v3 carry2 =
261  addition_n_direct ? v1 (addition_n_direct ? v2 v3 carry1) carry2.
262#n #carry1 #carry2 #v1 #v2 #v3
263<addition_n_direct_ok <addition_n_direct_ok
264<addition_n_direct_ok <addition_n_direct_ok
265lapply (associative_add_with_carries … carry1 carry2 v1 v2 v3)
266elim (add_with_carries n v2 v3 carry1) #bits #carries normalize nodelta
267elim (add_with_carries n v1 v2 carry1) #bits' #carries' normalize nodelta
268#H @(sym_eq … H)
269qed.
270
271lemma commutative_addition_n_direct : ∀n. ∀v1,v2 : BitVector n.
272  addition_n_direct ? v1 v2 false = addition_n_direct ? v2 v1 false.
273#n #v1 #v2 /by associative_addition_n, addition_n_direct_ok/
274qed.
275
276definition increment_direct ≝ λn,v. addition_n_direct n v (one_bv ?) false.
277definition twocomp_neg_direct ≝ λn,v. increment_direct n (negation_bv n v).
278
279(* fold andb on a bitvector. *)
280let rec andb_fold (n : nat) (b : BitVector n) on b : bool ≝
281match b with
282[ VEmpty ⇒ true
283| VCons sz elt tl ⇒
284  andb elt (andb_fold ? tl)
285].
286
287lemma andb_fold_Sn : ∀n. ∀x. ∀b : BitVector n. andb_fold (S n) (x ::: b) = andb x (andb_fold … n b). // qed.
288
289lemma andb_fold_inversion : ∀n. ∀elt,x. andb_fold (S n) (elt ::: x) = true → elt = true ∧ andb_fold n x = true.
290#n #elt #x cases elt normalize #H @conj destruct (H) try assumption @refl
291qed.
292
293lemma ith_increment_carry : ∀n. ∀a : BitVector (S n).
294  ith_carry … a (one_bv ?) false = andb_fold … a.
295#n elim n
296[ 1: #a elim (BitVector_Sn … a) #hd * #tl #Heq >Heq >(BitVector_O … tl)
297     cases hd normalize @refl
298| 2: #n' #Hind #a
299     elim (BitVector_Sn … a) #hd * #tl #Heq >Heq
300     lapply (Hind … tl) #Hind >one_bv_Sn
301     >ith_carry_Sn whd in match (andb_fold ??);
302     cases hd >Hind @refl
303] qed.
304
305lemma ith_increment_bit : ∀n. ∀a : BitVector (S n).
306  ith_bit … a (one_bv ?) false = xorb (head' … a) (andb_fold … (tail … a)).
307#n #a
308elim (BitVector_Sn … a) #hd * #tl #Heq >Heq
309whd in match (head' ???);
310-a cases n in tl;
311[ 1: #tl >(BitVector_O … tl) cases hd normalize try //
312| 2: #n' #tl >one_bv_Sn >ith_bit_Sn
313     >ith_increment_carry >tail_Sn
314     cases hd try //
315] qed.
316
317(* Lemma used to prove involutivity of two-complement negation *)
318lemma twocomp_neg_involutive_aux : ∀n. ∀v : BitVector (S n).
319   (andb_fold (S n) (negation_bv (S n) v) =
320    andb_fold (S n) (negation_bv (S n) (addition_n_direct (S n) (negation_bv (S n) v) (one_bv (S n)) false))).
321#n elim n
322[ 1: #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq >(BitVector_O … tl) cases hd @refl
323| 2: #n' #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq
324     lapply (Hind tl) -Hind #Hind >negation_bv_Sn >one_bv_Sn >addition_n_direct_Sn
325     >andb_fold_Sn >ith_bit_Sn >negation_bv_Sn >andb_fold_Sn <Hind
326     cases hd normalize nodelta
327     [ 1: >xorb_false >(xorb_comm false ?) >xorb_false
328     | 2: >xorb_false >(xorb_comm true ?) >xorb_true ]
329     >ith_increment_carry
330     cases (andb_fold (S n') (negation_bv (S n') tl)) @refl
331] qed.
332   
333(* Test of the 'direct' approach: proof of the involutivity of two-complement negation. *)
334lemma twocomp_neg_involutive : ∀n. ∀v : BitVector n. twocomp_neg_direct ? (twocomp_neg_direct ? v) = v.
335#n elim n
336[ 1: #v >(BitVector_O v) @refl
337| 2: #n' cases n'
338     [ 1: #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq
339          >(BitVector_O … tl) normalize cases hd @refl
340     | 2: #n'' #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq
341          lapply (Hind tl) -Hind #Hind <Hind in ⊢ (???%);
342          whd in match twocomp_neg_direct; normalize nodelta
343          whd in match increment_direct; normalize nodelta
344          >(negation_bv_Sn ? hd tl) >one_bv_Sn >(addition_n_direct_Sn ? (¬hd) false ??)
345          >ith_bit_Sn >negation_bv_Sn >addition_n_direct_Sn >ith_bit_Sn
346          generalize in match (addition_n_direct (S n'')
347                                                   (negation_bv (S n'')
348                                                   (addition_n_direct (S n'') (negation_bv (S n'') tl) (one_bv (S n'')) false))
349                                                   (one_bv (S n'')) false); #tail
350          >ith_increment_carry >ith_increment_carry
351          cases hd normalize nodelta
352          [ 1: normalize in match (xorb false false); >(xorb_comm false ?) >xorb_false >xorb_false
353          | 2: normalize in match (xorb true false); >(xorb_comm true ?) >xorb_true >xorb_false ]
354          <twocomp_neg_involutive_aux
355          cases (andb_fold (S n'') (negation_bv (S n'') tl)) @refl
356      ]
357] qed.
358
359lemma bitvector_cons_inj_inv : ∀n. ∀a,b. ∀va,vb : BitVector n. a ::: va = b ::: vb → a =b ∧ va = vb.
360#n #a #b #va #vb #H destruct (H) @conj @refl qed.
361
362lemma bitvector_cons_eq : ∀n. ∀a,b. ∀v : BitVector n. a = b → a ::: v = b ::: v. // qed.
363
364(* Injectivity of increment *)
365lemma increment_inj : ∀n. ∀a,b : BitVector n.
366  increment_direct ? a = increment_direct ? b →
367  a = b ∧ (ith_carry n a (one_bv n) false = ith_carry n b (one_bv n) false).
368#n whd in match increment_direct; normalize nodelta elim n
369[ 1: #a #b >(BitVector_O … a) >(BitVector_O … b) normalize #_ @conj //
370| 2: #n' cases n'
371   [ 1: #_ #a #b
372        elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a >Heq_a
373        elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b >Heq_b
374        >(BitVector_O … tl_a) >(BitVector_O … tl_b) cases hd_a cases hd_b
375        normalize #H @conj try //
376   | 2: #n'' #Hind #a #b
377        elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a >Heq_a
378        elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b >Heq_b
379        lapply (Hind … tl_a tl_b) -Hind #Hind
380        >one_bv_Sn >addition_n_direct_Sn >ith_bit_Sn
381        >addition_n_direct_Sn >ith_bit_Sn >xorb_false >xorb_false
382        #H elim (bitvector_cons_inj_inv … H) #Heq1 #Heq2
383        lapply (Hind Heq2) * #Heq3 #Heq4
384        cut (hd_a = hd_b)
385        [ 1: >Heq4 in Heq1; #Heq5 lapply (xorb_inj (ith_carry ? tl_b (one_bv ?) false) hd_a hd_b)
386             * #Heq6 #_ >xorb_comm in Heq6; >(xorb_comm  ? hd_b) #Heq6 >(Heq6 Heq5)
387             @refl ]
388        #Heq5 @conj [ 1: >Heq3 >Heq5 @refl ]
389        >ith_carry_Sn >ith_carry_Sn >Heq4 >Heq5 @refl
390] qed.
391
392(* Inverse of injecivity of increment, does not lose information (cf increment_inj) *)
393lemma increment_inj_inv : ∀n. ∀a,b : BitVector n.
394  a = b → increment_direct ? a = increment_direct ? b. // qed.
395
396(* A more general result. *)
397lemma addition_n_direct_inj : ∀n. ∀x,y,delta: BitVector n.
398  addition_n_direct ? x delta false = addition_n_direct ? y delta false →
399  x = y ∧ (ith_carry n x delta false = ith_carry n y delta false).
400#n elim n
401[ 1: #x #y #delta >(BitVector_O … x) >(BitVector_O … y) >(BitVector_O … delta) * @conj @refl
402| 2: #n' #Hind #x #y #delta
403     elim (BitVector_Sn … x) #hdx * #tlx #Heqx >Heqx
404     elim (BitVector_Sn … y) #hdy * #tly #Heqy >Heqy
405     elim (BitVector_Sn … delta) #hdd * #tld #Heqd >Heqd
406     >addition_n_direct_Sn >ith_bit_Sn
407     >addition_n_direct_Sn >ith_bit_Sn
408     >ith_carry_Sn >ith_carry_Sn
409     lapply (Hind … tlx tly tld) -Hind #Hind #Heq
410     elim (bitvector_cons_inj_inv … Heq) #Heq_hd #Heq_tl
411     lapply (Hind Heq_tl) -Hind * #HindA #HindB
412     >HindA >HindB >HindB in Heq_hd; #Heq_hd
413     cut (hdx = hdy)
414     [ 1: cases hdd in Heq_hd; cases (ith_carry n' tly tld false)
415          cases hdx cases hdy normalize #H try @H try @refl
416          >H try @refl ]
417     #Heq_hd >Heq_hd @conj @refl
418] qed.
419
420(* We also need it the other way around. *)
421lemma addition_n_direct_inj_inv : ∀n. ∀x,y,delta: BitVector n.
422  x ≠ y → (* ∧ (ith_carry n x delta false = ith_carry n y delta false). *)
423   addition_n_direct ? x delta false ≠ addition_n_direct ? y delta false.
424#n elim n
425[ 1: #x #y #delta >(BitVector_O … x) >(BitVector_O … y) >(BitVector_O … delta) * #H @(False_ind … (H (refl ??)))
426| 2: #n' #Hind #x #y #delta
427     elim (BitVector_Sn … x) #hdx * #tlx #Heqx >Heqx
428     elim (BitVector_Sn … y) #hdy * #tly #Heqy >Heqy
429     elim (BitVector_Sn … delta) #hdd * #tld #Heqd >Heqd
430     #Hneq
431     cut (hdx ≠ hdy ∨ tlx ≠ tly)
432     [ @(eq_bv_elim … tlx tly)
433       [ #Heq_tl >Heq_tl >Heq_tl in Hneq;
434         #Hneq cut (hdx ≠ hdy) [ % #Heq_hd >Heq_hd in Hneq; *
435                                 #H @H @refl ]
436         #H %1 @H
437       | #H %2 @H ] ]
438     -Hneq #Hneq
439     >addition_n_direct_Sn >addition_n_direct_Sn
440     >ith_bit_Sn >ith_bit_Sn cases Hneq
441     [ 1: #Hneq_hd
442          lapply (addition_n_direct_inj … tlx tly tld)         
443          @(eq_bv_elim … (addition_n_direct ? tlx tld false) (addition_n_direct ? tly tld false))
444          [ 1: #Heq -Hind #Hind elim (Hind Heq) #Heq_tl >Heq_tl #Heq_carry >Heq_carry
445               % #Habsurd elim (bitvector_cons_inj_inv … Habsurd) -Habsurd
446               lapply Hneq_hd
447               cases hdx cases hdd cases hdy cases (ith_carry ? tly tld false)
448               normalize in ⊢ (? → % → ?); #Hneq_hd #Heq_hd #_
449               try @(absurd … Heq_hd Hneq_hd)
450               elim Hneq_hd -Hneq_hd #Hneq_hd @Hneq_hd
451               try @refl try assumption try @(sym_eq … Heq_hd)
452          | 2: #Htl_not_eq #_ % #Habsurd elim (bitvector_cons_inj_inv … Habsurd) #_
453               elim Htl_not_eq -Htl_not_eq #HA #HB @HA @HB ]
454     | 2: #Htl_not_eq lapply (Hind tlx tly tld Htl_not_eq) -Hind #Hind
455          % #Habsurd elim (bitvector_cons_inj_inv … Habsurd) #_
456          elim Hind -Hind #HA #HB @HA @HB ]
457] qed.
458
459lemma carry_notb : ∀a,b,c. notb (carry_of a b c) = carry_of (notb a) (notb b) (notb c). * * * @refl qed.
460
461lemma increment_to_carry_aux : ∀n. ∀a : BitVector (S n).
462   ith_carry (S n) a (one_bv (S n)) false
463   = ith_carry (S n) a (zero (S n)) true.
464#n elim n
465[ 1: #a elim (BitVector_Sn ? a) #hd_a * #tl_a #Heq >Heq >(BitVector_O … tl_a) @refl
466| 2: #n' #Hind #a elim (BitVector_Sn ? a) #hd_a * #tl_a #Heq >Heq
467     lapply (Hind tl_a) #Hind
468     >one_bv_Sn >zero_Sn >ith_carry_Sn >ith_carry_Sn >Hind @refl
469] qed.
470
471lemma neutral_addition_n_direct_aux : ∀n. ∀v. ith_carry n v (zero n) false = false.
472#n elim n //
473#n' #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq >zero_Sn
474>ith_carry_Sn >(Hind tl) cases hd @refl.
475qed.
476
477lemma neutral_addition_n_direct : ∀n. ∀v : BitVector n.
478  addition_n_direct ? v (zero ?) false = v.
479#n elim n
480[ 1: #v >(BitVector_O … v) normalize @refl
481| 2: #n' #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq
482     lapply (Hind … tl) #H >zero_Sn >addition_n_direct_Sn
483     >ith_bit_Sn >H >xorb_false >neutral_addition_n_direct_aux
484     >xorb_false @refl
485] qed.
486
487lemma increment_to_carry_zero : ∀n. ∀a : BitVector n. addition_n_direct ? a (one_bv ?) false = addition_n_direct ? a (zero ?) true.
488#n elim n
489[ 1: #a >(BitVector_O … a) normalize @refl
490| 2: #n' cases n'
491     [ 1: #_ #a elim (BitVector_Sn … a) #hd_a * #tl_a #Heq >Heq >(BitVector_O … tl_a) cases hd_a @refl
492     | 2: #n'' #Hind #a
493          elim (BitVector_Sn … a) #hd_a * #tl_a #Heq >Heq
494          lapply (Hind tl_a) -Hind #Hind
495          >one_bv_Sn >zero_Sn >addition_n_direct_Sn >ith_bit_Sn
496          >addition_n_direct_Sn >ith_bit_Sn
497          >xorb_false >Hind @bitvector_cons_eq
498          >increment_to_carry_aux @refl
499     ]
500] qed.
501
502lemma increment_to_carry : ∀n. ∀a,b : BitVector n.
503  addition_n_direct ? a (addition_n_direct ? b (one_bv ?) false) false = addition_n_direct ? a b true.
504#n #a #b >increment_to_carry_zero <associative_addition_n_direct
505>neutral_addition_n_direct @refl
506qed.
507
508(* Prove -(a + b) = -a + -b *)
509lemma twocomp_neg_plus : ∀n. ∀a,b : BitVector n.
510  twocomp_neg_direct ? (addition_n_direct ? a b false) = addition_n_direct ? (twocomp_neg_direct … a) (twocomp_neg_direct … b) false.
511whd in match twocomp_neg_direct; normalize nodelta
512lapply increment_inj_inv
513whd in match increment_direct; normalize nodelta
514#H #n #a #b
515<associative_addition_n_direct @H
516>associative_addition_n_direct >(commutative_addition_n_direct ? (one_bv n))
517>increment_to_carry
518-H lapply b lapply a -b -a
519cases n
520[ 1: #a #b >(BitVector_O … a) >(BitVector_O … b) @refl
521| 2: #n' #a #b
522     cut (negation_bv ? (addition_n_direct ? a b false)
523           = addition_n_direct ? (negation_bv ? a) (negation_bv ? b) true ∧
524          notb (ith_carry ? a b false) = (ith_carry ? (negation_bv ? a) (negation_bv ? b) true))
525     [ -n lapply b lapply a elim n'
526     [ 1: #a #b elim (BitVector_Sn … a) #hd_a * #tl_a #Heqa >Heqa >(BitVector_O … tl_a)
527          elim (BitVector_Sn … b) #hd_b * #tl_b #Heqb >Heqb >(BitVector_O … tl_b)
528          cases hd_a cases hd_b normalize @conj @refl
529     | 2: #n #Hind #a #b
530          elim (BitVector_Sn … a) #hd_a * #tl_a #Heqa >Heqa
531          elim (BitVector_Sn … b) #hd_b * #tl_b #Heqb >Heqb
532          lapply (Hind tl_a tl_b) * #H1 #H2
533          @conj
534          [ 2: >ith_carry_Sn >negation_bv_Sn >negation_bv_Sn >ith_carry_Sn
535               >carry_notb >H2 @refl
536          | 1: >addition_n_direct_Sn >ith_bit_Sn >negation_bv_Sn
537               >negation_bv_Sn >negation_bv_Sn
538               >addition_n_direct_Sn >ith_bit_Sn >H1 @bitvector_cons_eq
539               >xorb_lneg >xorb_rneg >notb_notb
540               <xorb_rneg >H2 @refl
541          ]
542      ] ]
543      * #H1 #H2 @H1
544] qed.
545
546lemma addition_n_direct_neg : ∀n. ∀a.
547 (addition_n_direct n a (negation_bv n a) false) = replicate ?? true
548 ∧ (ith_carry n a (negation_bv n a) false = false).
549#n elim n
550[ 1: #a >(BitVector_O … a) @conj @refl
551| 2: #n' #Hind #a elim (BitVector_Sn … a) #hd * #tl #Heq >Heq
552     lapply (Hind … tl) -Hind * #HA #HB
553     @conj
554     [ 2: >negation_bv_Sn >ith_carry_Sn >HB cases hd @refl
555     | 1: >negation_bv_Sn >addition_n_direct_Sn
556          >ith_bit_Sn >HB >xorb_false >HA
557          @bitvector_cons_eq elim hd @refl
558     ]
559] qed.
560
561(* -a + a = 0 *)
562lemma bitvector_opp_direct : ∀n. ∀a : BitVector n. addition_n_direct ? a (twocomp_neg_direct ? a) false = (zero ?).
563whd in match twocomp_neg_direct;
564whd in match increment_direct;
565normalize nodelta
566#n #a <associative_addition_n_direct
567elim (addition_n_direct_neg … a) #H #_ >H
568-H -a
569cases n try //
570#n'
571cut ((addition_n_direct (S n') (replicate bool ? true) (one_bv ?) false = (zero (S n')))
572       ∧ (ith_carry ? (replicate bool (S n') true) (one_bv (S n')) false = true))
573[ elim n'
574     [ 1: @conj @refl
575     | 2: #n' * #HA #HB @conj
576          [ 1: >replicate_Sn >one_bv_Sn  >addition_n_direct_Sn
577               >ith_bit_Sn >HA >zero_Sn @bitvector_cons_eq >HB @refl
578          | 2: >replicate_Sn >one_bv_Sn >ith_carry_Sn >HB @refl ]
579     ]
580] * #H1 #H2 @H1
581qed.
582
583(* Lift back the previous result to standard operations. *)
584lemma twocomp_neg_direct_ok : ∀n. ∀v. twocomp_neg_direct ? v = two_complement_negation n v.
585#n #v whd in match twocomp_neg_direct; normalize nodelta
586whd in match increment_direct; normalize nodelta
587whd in match two_complement_negation; normalize nodelta
588>increment_to_addition_n <addition_n_direct_ok
589whd in match addition_n; normalize nodelta
590elim (add_with_carries ????) #a #b @refl
591qed.
592
593lemma two_complement_negation_plus : ∀n. ∀a,b : BitVector n.
594  two_complement_negation ? (addition_n ? a b) = addition_n ? (two_complement_negation ? a) (two_complement_negation ? b).
595#n #a #b
596lapply (twocomp_neg_plus ? a b)
597>twocomp_neg_direct_ok >twocomp_neg_direct_ok >twocomp_neg_direct_ok
598<addition_n_direct_ok <addition_n_direct_ok
599whd in match addition_n; normalize nodelta
600elim (add_with_carries n a b false) #bits #flags normalize nodelta
601elim (add_with_carries n (two_complement_negation n a) (two_complement_negation n b) false) #bits' #flags'
602normalize nodelta #H @H
603qed.
604
605lemma bitvector_opp_addition_n : ∀n. ∀a : BitVector n. addition_n ? a (two_complement_negation ? a) = (zero ?).
606#n #a lapply (bitvector_opp_direct ? a)
607>twocomp_neg_direct_ok <addition_n_direct_ok
608whd in match (addition_n ???);
609elim (add_with_carries n a (two_complement_negation n a) false) #bits #flags #H @H
610qed.
611
612lemma neutral_addition_n : ∀n. ∀a : BitVector n. addition_n ? a (zero ?) = a.
613#n #a
614lapply (neutral_addition_n_direct n a)
615<addition_n_direct_ok
616whd in match (addition_n ???);
617elim (add_with_carries n a (zero n) false) #bits #flags #H @H
618qed.
619
620lemma injective_addition_n : ∀n. ∀x,y,delta : BitVector n.
621  addition_n ? x delta = addition_n ? y delta → x = y. 
622#n #x #y #delta 
623lapply (addition_n_direct_inj … x y delta)
624<addition_n_direct_ok <addition_n_direct_ok
625whd in match addition_n; normalize nodelta
626elim (add_with_carries n x delta false) #bitsx #flagsx
627elim (add_with_carries n y delta false) #bitsy #flagsy
628normalize #H1 #H2 elim (H1 H2) #Heq #_ @Heq
629qed.
630
631lemma injective_inv_addition_n : ∀n. ∀x,y,delta : BitVector n.
632  x ≠ y → addition_n ? x delta ≠ addition_n ? y delta. 
633#n #x #y #delta 
634lapply (addition_n_direct_inj_inv … x y delta)
635<addition_n_direct_ok <addition_n_direct_ok
636whd in match addition_n; normalize nodelta
637elim (add_with_carries n x delta false) #bitsx #flagsx
638elim (add_with_carries n y delta false) #bitsy #flagsy
639normalize #H1 #H2 @(H1 H2)
640qed.
641
642
643(* --------------------------------------------------------------------------- *)   
644(* Aux lemmas that are likely to be found elsewhere. *)
645(* --------------------------------------------------------------------------- *)   
646
647lemma zlt_succ : ∀a,b. Zltb a b = true → Zltb a (Zsucc b) = true.
648#a #b #HA
649lapply (Zltb_true_to_Zlt … HA) #HA_prop
650@Zlt_to_Zltb_true /2/
651qed.
652
653lemma zlt_succ_refl : ∀a. Zltb a (Zsucc a) = true.
654#a @Zlt_to_Zltb_true /2/ qed.
655(*
656definition le_offset : offset → offset → bool.
657  λx,y. Zleb (offv x) (offv y).
658*)
659lemma not_refl_absurd : ∀A:Type[0].∀x:A. x ≠ x → False. /2/. qed.
660
661lemma eqZb_reflexive : ∀x:Z. eqZb x x = true. #x /2/. qed.
662
663(* --------------------------------------------------------------------------- *)   
664(* In the definition of injections below, we maintain a list of blocks that are
665   writeable. We need some lemmas to reason on the fact that a block cannot be
666   both writeable and not writeable, etc. *)
667(* --------------------------------------------------------------------------- *)
668
669(* When equality on A is decidable, [mem A elt l] is too. *)
670lemma mem_dec : ∀A:Type[0]. ∀eq:(∀a,b:A. a = b ∨ a ≠ b). ∀elt,l. mem A elt l ∨ ¬ (mem A elt l).
671#A #dec #elt #l elim l
672[ 1: normalize %2 /2/
673| 2: #hd #tl #Hind
674     elim (dec elt hd)
675     [ 1: #Heq >Heq %1 /2/
676     | 2: #Hneq cases Hind
677        [ 1: #Hmem %1 /2/
678        | 2: #Hnmem %2 normalize
679              % #H cases H
680              [ 1: lapply Hneq * #Hl #Eq @(Hl Eq)
681              | 2: lapply Hnmem * #Hr #Hmem @(Hr Hmem) ]
682] ] ]
683qed.
684
685lemma block_eq_dec : ∀a,b:block. a = b ∨ a ≠ b.
686#a #b @(eq_block_elim … a b) /2/ qed.
687
688lemma mem_not_mem_neq : ∀l,elt1,elt2. (mem block elt1 l) → ¬ (mem block elt2 l) → elt1 ≠ elt2.
689#l #elt1 #elt2 elim l
690[ 1: normalize #Habsurd @(False_ind … Habsurd)
691| 2: #hd #tl #Hind normalize #Hl #Hr
692   cases Hl
693   [ 1: #Heq >Heq
694        @(eq_block_elim … hd elt2)
695        [ 1: #Heq >Heq /2 by not_to_not/
696        | 2: #x @x ]
697   | 2: #Hmem1 cases (mem_dec … block_eq_dec elt2 tl)
698        [ 1: #Hmem2 % #Helt_eq cases Hr #H @H %2 @Hmem2
699        | 2: #Hmem2 @Hind //
700        ]
701   ]
702] qed.
703
704lemma neq_block_eq_block_false : ∀b1,b2:block. b1 ≠ b2 → eq_block b1 b2 = false.
705#b1 #b2 * #Hb
706@(eq_block_elim … b1 b2)
707[ 1: #Habsurd @(False_ind … (Hb Habsurd))
708| 2: // ] qed.
709
710(* --------------------------------------------------------------------------- *)   
711(* Memory injections *)
712(* --------------------------------------------------------------------------- *)   
713
714(* An embedding is a function from blocks to (blocks × offset). *)
715definition embedding ≝ block → option (block × offset).
716
717definition offset_plus : offset → offset → offset ≝
718  λo1,o2. mk_offset (addition_n ? (offv o1) (offv o2)).
719
720lemma offset_plus_0 : ∀o. offset_plus o (mk_offset (zero ?)) = o.
721* #o
722whd in match (offset_plus ??);
723>addition_n_0 @refl
724qed.
725
726(* Translates a pointer through an embedding. *)
727definition pointer_translation : ∀p:pointer. ∀E:embedding. option pointer ≝
728λp,E.
729match p with
730[ mk_pointer pblock poff ⇒
731   match E pblock with
732   [ None ⇒ None ?
733   | Some loc ⇒
734    let 〈dest_block,dest_off〉 ≝ loc in
735    let ptr ≝ (mk_pointer dest_block (offset_plus poff dest_off)) in
736    Some ? ptr
737   ]
738].
739
740(* We parameterise the "equivalence" relation on values with an embedding. *)
741(* Front-end values. *)
742inductive value_eq (E : embedding) : val → val → Prop ≝
743| undef_eq : ∀v.
744  value_eq E Vundef v
745| vint_eq : ∀sz,i.
746  value_eq E (Vint sz i) (Vint sz i)
747| vfloat_eq : ∀f.
748  value_eq E (Vfloat f) (Vfloat f)
749| vnull_eq :
750  value_eq E Vnull Vnull
751| vptr_eq : ∀p1,p2.
752  pointer_translation p1 E = Some ? p2 →
753  value_eq E (Vptr p1) (Vptr p2).
754 
755(* [load_sim] states the fact that each successful load in [m1] is matched by a load in [m2] s.t.
756 * the values are equivalent. *)
757definition load_sim ≝
758λ(E : embedding).λ(m1 : mem).λ(m2 : mem).
759 ∀b1,off1,b2,off2,ty,v1.
760  valid_block m1 b1 →  (* We need this because it is not provable from [load_value_of_type ty m1 b1 off1] when loading by-ref *)
761  E b1 = Some ? 〈b2,off2〉 →
762  load_value_of_type ty m1 b1 off1 = Some ? v1 →
763  (∃v2. load_value_of_type ty m2 b2 (offset_plus off1 off2) = Some ? v2 ∧ value_eq E v1 v2).
764 
765definition load_sim_ptr ≝
766λ(E : embedding).λ(m1 : mem).λ(m2 : mem).
767 ∀b1,off1,b2,off2,ty,v1.
768  valid_pointer m1 (mk_pointer b1 off1) = true →  (* We need this because it is not provable from [load_value_of_type ty m1 b1 off1] when loading by-ref *)
769  pointer_translation (mk_pointer b1 off1) E = Some ? (mk_pointer b2 off2) →
770  load_value_of_type ty m1 b1 off1 = Some ? v1 →
771  (∃v2. load_value_of_type ty m2 b2 off2 = Some ? v2 ∧ value_eq E v1 v2).
772
773(* Definition of a memory injection *)
774record memory_inj (E : embedding) (m1 : mem) (m2 : mem) : Type[0] ≝
775{ (* Load simulation *)
776  mi_inj : load_sim_ptr E m1 m2;
777  (* Invalid blocks are not mapped *)
778  mi_freeblock : ∀b. ¬ (valid_block m1 b) → E b = None ?;
779  (* Valid pointers are mapped to valid pointers*)
780  mi_valid_pointers : ∀p,p'.
781                       valid_pointer m1 p = true →
782                       pointer_translation p E = Some ? p' →
783                       valid_pointer m2 p' = true;
784  (* Blocks in the codomain are valid *)
785  (* mi_incl : ∀b,b',o'. E b = Some ? 〈b',o'〉 → valid_block m2 b'; *)
786  (* Regions are preserved *)
787  mi_region : ∀b,b',o'. E b = Some ? 〈b',o'〉 → block_region b = block_region b';
788  (* Disjoint blocks are mapped to disjoint blocks. Note that our condition is stronger than compcert's.
789   * This may cause some problems if we reuse this def for the translation from Clight to Cminor, where
790   * all variables are allocated in the same block. *)
791  mi_disjoint : ∀b1,b2,b1',b2',o1',o2'.
792                b1 ≠ b2 →
793                E b1 = Some ? 〈b1',o1'〉 →
794                E b2 = Some ? 〈b2',o2'〉 →
795                b1' ≠ b2'
796}.
797
798(* Definition of a memory extension. /!\ Not equivalent to the compcert concept. /!\
799 * A memory extension is a [memory_inj] with some particular blocks designated as
800 * being writeable. *)
801
802alias id "meml" = "cic:/matita/basics/lists/list/mem.fix(0,2,1)".
803
804record memory_ext (E : embedding) (m1 : mem) (m2 : mem) : Type[0] ≝
805{ me_inj : memory_inj E m1 m2;
806  (* A list of blocks where we can write freely *)
807  me_writeable : list block;
808  (* These blocks are valid *)
809  me_writeable_valid : ∀b. meml ? b me_writeable → valid_block m2 b;
810  (* And pointers to m1 are oblivious to these blocks *)
811  me_writeable_ok : ∀p,p'.
812                     valid_pointer m1 p = true →
813                     pointer_translation p E = Some ? p' →
814                     ¬ (meml ? (pblock p') me_writeable)
815}.
816
817(* ---------------------------------------------------------------------------- *)
818(* End of the definitions on memory injections. Now, on to proving some lemmas. *)
819
820(* A particular inversion. *)
821lemma value_eq_ptr_inversion :
822  ∀E,p1,v. value_eq E (Vptr p1) v → ∃p2. v = Vptr p2 ∧ pointer_translation p1 E = Some ? p2.
823#E #p1 #v #Heq inversion Heq
824[ 1: #v #Habsurd destruct (Habsurd)
825| 2: #sz #i #Habsurd destruct (Habsurd)
826| 3: #f #Habsurd destruct (Habsurd)
827| 4:  #Habsurd destruct (Habsurd)
828| 5: #p1' #p2 #Heq #Heqv #Heqv2 #_ destruct
829     %{p2} @conj try @refl try assumption
830] qed.
831
832(* A cleaner version of inversion for [value_eq] *)
833lemma value_eq_inversion :
834  ∀E,v1,v2. ∀P : val → val → Prop. value_eq E v1 v2 →
835  (∀v. P Vundef v) →
836  (∀sz,i. P (Vint sz i) (Vint sz i)) →
837  (∀f. P (Vfloat f) (Vfloat f)) →
838  (P Vnull Vnull) →
839  (∀p1,p2. pointer_translation p1 E = Some ? p2 → P (Vptr p1) (Vptr p2)) →
840  P v1 v2.
841#E #v1 #v2 #P #Heq #H1 #H2 #H3 #H4 #H5
842inversion Heq
843[ 1: #v #Hv1 #Hv2 #_ destruct @H1
844| 2: #sz #i #Hv1 #Hv2 #_ destruct @H2
845| 3: #f #Hv1 #Hv2 #_ destruct @H3
846| 4: #Hv1 #Hv2 #_ destruct @H4
847| 5: #p1 #p2 #Hembed #Hv1 #Hv2 #_ destruct @H5 // ] qed.
848 
849(* If we succeed to load something by value from a 〈b,off〉 location,
850   [b] is a valid block. *)
851lemma load_by_value_success_valid_block_aux :
852  ∀ty,m,b,off,v.
853    access_mode ty = By_value (typ_of_type ty) →
854    load_value_of_type ty m b off = Some ? v →
855    Zltb (block_id b) (nextblock m) = true.
856#ty #m * #brg #bid #off #v
857cases ty
858[ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
859| 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
860whd in match (load_value_of_type ????);
861[ 1,7,8: #_ #Habsurd destruct (Habsurd) ]
862#Hmode
863[ 1,2,3,6: [ 1: elim sz | 2: elim fsz ]
864     normalize in match (typesize ?);
865     whd in match (loadn ???);
866     whd in match (beloadv ??);
867     cases (Zltb bid (nextblock m)) normalize nodelta
868     try // #Habsurd destruct (Habsurd)
869| *: normalize in Hmode; destruct (Hmode)
870] qed.
871
872(* If we succeed in loading some data from a location, then this loc is a valid pointer. *)
873lemma load_by_value_success_valid_ptr_aux :
874  ∀ty,m,b,off,v.
875    access_mode ty = By_value (typ_of_type ty) →
876    load_value_of_type ty m b off = Some ? v →
877    Zltb (block_id b) (nextblock m) = true ∧
878    Zleb (low_bound m b) (Z_of_unsigned_bitvector ? (offv off)) = true ∧
879    Zltb (Z_of_unsigned_bitvector ? (offv off)) (high_bound m b) = true.
880#ty #m * #brg #bid #off #v
881cases ty
882[ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
883| 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
884whd in match (load_value_of_type ????);
885[ 1,7,8: #_ #Habsurd destruct (Habsurd) ]
886#Hmode
887[ 1,2,3,6: [ 1: elim sz | 2: elim fsz ]
888     normalize in match (typesize ?);
889     whd in match (loadn ???);
890     whd in match (beloadv ??);
891     cases (Zltb bid (nextblock m)) normalize nodelta
892     cases (Zleb (low (blocks m (mk_block brg bid)))
893                  (Z_of_unsigned_bitvector offset_size (offv off)))
894     cases (Zltb (Z_of_unsigned_bitvector offset_size (offv off)) (high (blocks m (mk_block brg bid))))
895     normalize nodelta
896     #Heq destruct (Heq)
897     try /3 by conj, refl/
898| *: normalize in Hmode; destruct (Hmode)
899] qed.
900
901
902lemma valid_block_from_bool : ∀b,m. Zltb (block_id b) (nextblock m) = true → valid_block m b.
903* #rg #id #m normalize
904elim id /2/ qed.
905
906lemma valid_block_to_bool : ∀b,m. valid_block m b → Zltb (block_id b) (nextblock m) = true.
907* #rg #id #m normalize
908elim id /2/ qed.
909
910lemma load_by_value_success_valid_block :
911  ∀ty,m,b,off,v.
912    access_mode ty = By_value (typ_of_type ty) →
913    load_value_of_type ty m b off = Some ? v →
914    valid_block m b.
915#ty #m #b #off #v #Haccess_mode #Hload
916@valid_block_from_bool
917elim (load_by_value_success_valid_ptr_aux ty m b off v Haccess_mode Hload) * //
918qed.
919
920lemma load_by_value_success_valid_pointer :
921  ∀ty,m,b,off,v.
922    access_mode ty = By_value (typ_of_type ty) →
923    load_value_of_type ty m b off = Some ? v →
924    valid_pointer m (mk_pointer b off).
925#ty #m #b #off #v #Haccess_mode #Hload normalize
926elim (load_by_value_success_valid_ptr_aux ty m b off v Haccess_mode Hload)
927* #H1 #H2 #H3 >H1 >H2 normalize nodelta
928>Zle_to_Zleb_true try //
929lapply (Zlt_to_Zle … (Zltb_true_to_Zlt … H3)) /2/
930qed.
931
932
933(* Making explicit the contents of memory_inj for load_value_of_type *)
934lemma load_value_of_type_inj : ∀E,m1,m2,b1,off1,v1,b2,off2,ty.
935    memory_inj E m1 m2 →
936    value_eq E (Vptr (mk_pointer b1 off1)) (Vptr (mk_pointer b2 off2)) →
937    load_value_of_type ty m1 b1 off1 = Some ? v1 →
938    ∃v2. load_value_of_type ty m2 b2 off2 = Some ? v2 ∧ value_eq E v1 v2.
939#E #m1 #m2 #b1 #off1 #v1 #b2 #off2 #ty #Hinj #Hvalue_eq
940lapply (value_eq_ptr_inversion … Hvalue_eq) * #p2 * #Hp2_eq #Hembed destruct
941lapply (refl ? (access_mode ty))
942cases ty
943[ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
944| 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
945normalize in ⊢ ((???%) → ?); #Hmode #Hyp
946[ 1,7,8: normalize in Hyp; destruct (Hyp)
947| 5,6: normalize in Hyp ⊢ %; destruct (Hyp) /3 by ex_intro, conj, vptr_eq/ ]
948lapply (load_by_value_success_valid_pointer … Hmode … Hyp) #Hvalid_pointer
949lapply (mi_inj … Hinj b1 off1 b2 off2 … Hvalid_pointer Hembed Hyp) #H @H
950qed.     
951
952
953(* -------------------------------------- *)
954(* Lemmas pertaining to memory allocation *)
955
956(* A valid block stays valid after an alloc. *)
957lemma alloc_valid_block_conservation :
958  ∀m,m',z1,z2,r,new_block.
959  alloc m z1 z2 r = 〈m', new_block〉 →
960  ∀b. valid_block m b → valid_block m' b.
961#m #m' #z1 #z2 #r * #b' #Hregion_eq
962elim m #contents #nextblock #Hcorrect whd in match (alloc ????);
963#Halloc destruct (Halloc)
964#b whd in match (valid_block ??) in ⊢ (% → %); /2/
965qed.
966
967(* Allocating a new zone produces a valid block. *)
968lemma alloc_valid_new_block :
969  ∀m,m',z1,z2,r,new_block.
970  alloc m z1 z2 r = 〈m', new_block〉 →
971  valid_block m' new_block.
972* #contents #nextblock #Hcorrect #m' #z1 #z2 #r * #new_block #Hregion_eq
973whd in match (alloc ????); whd in match (valid_block ??);
974#Halloc destruct (Halloc) /2/
975qed.
976
977(* All data in a valid block is unchanged after an alloc. *)
978lemma alloc_beloadv_conservation :
979  ∀m,m',block,offset,z1,z2,r,new_block.
980    valid_block m block →
981    alloc m z1 z2 r = 〈m', new_block〉 →
982    beloadv m (mk_pointer block offset) = beloadv m' (mk_pointer block offset).
983* #contents #next #Hcorrect #m' #block #offset #z1 #z2 #r #new_block #Hvalid #Halloc
984whd in Halloc:(??%?); destruct (Halloc)
985whd in match (beloadv ??) in ⊢ (??%%);
986lapply (valid_block_to_bool … Hvalid) #Hlt
987>Hlt >(zlt_succ … Hlt)
988normalize nodelta whd in match (update_block ?????); whd in match (eq_block ??);
989cut (eqZb (block_id block) next = false)
990[ lapply (Zltb_true_to_Zlt … Hlt) #Hlt' @eqZb_false /2/ ] #Hneq
991>Hneq cases (eq_region ??) normalize nodelta  @refl
992qed.
993
994(* Lift [alloc_beloadv_conservation] to loadn *)
995lemma alloc_loadn_conservation :
996  ∀m,m',z1,z2,r,new_block.
997    alloc m z1 z2 r = 〈m', new_block〉 →
998    ∀n. ∀block,offset.
999    valid_block m block →
1000    loadn m (mk_pointer block offset) n = loadn m' (mk_pointer block offset) n.
1001#m #m' #z1 #z2 #r #new_block #Halloc #n
1002elim n try //
1003#n' #Hind #block #offset #Hvalid_block
1004whd in ⊢ (??%%);
1005>(alloc_beloadv_conservation … Hvalid_block Halloc)
1006cases (beloadv m' (mk_pointer block offset)) //
1007#bev normalize nodelta
1008whd in match (shift_pointer ???); >Hind try //
1009qed.
1010
1011(* Memory allocation preserves [memory_inj] *)
1012lemma alloc_memory_inj :
1013  ∀E:embedding.∀m1,m2,m2',z1,z2,r,new_block. ∀H:memory_inj E m1 m2.
1014  alloc m2 z1 z2 r = 〈m2', new_block〉 →
1015  memory_inj E m1 m2'.
1016#E #m1 #m2 #m2' #z1 #z2 #r * #new_block #Hregion #Hmemory_inj #Halloc
1017%
1018[ 1:
1019  whd
1020  #b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Hembed #Hload
1021  elim (mi_inj E m1 m2 Hmemory_inj b1 off1 b2 off2 … ty v1 Hvalid Hembed Hload)
1022  #v2 * #Hload_eq #Hvalue_eq %{v2} @conj try //
1023  lapply (refl ? (access_mode ty))
1024  cases ty in Hload_eq;
1025  [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
1026  | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
1027  #Hload normalize in ⊢ ((???%) → ?); #Haccess
1028  [ 1,7,8: normalize in Hload; destruct (Hload)
1029  | 2,3,4,9: whd in match (load_value_of_type ????);
1030     whd in match (load_value_of_type ????);
1031     lapply (load_by_value_success_valid_block … Haccess Hload)
1032     #Hvalid_block
1033     whd in match (load_value_of_type ????) in Hload;
1034     <(alloc_loadn_conservation … Halloc … Hvalid_block)
1035     @Hload
1036  | 5,6: whd in match (load_value_of_type ????) in Hload ⊢ %; @Hload ]
1037| 2: @(mi_freeblock … Hmemory_inj)
1038| 3: #p #p' #Hvalid #Hptr_trans lapply (mi_valid_pointers … Hmemory_inj p p' Hvalid Hptr_trans)
1039     elim m2 in Halloc; #contentmap #nextblock #Hnextblock
1040     elim p' * #br' #bid' #o' #Halloc whd in Halloc:(??%?) ⊢ ?; destruct (Halloc)
1041     whd in match (valid_pointer ??) in ⊢ (% → %);
1042     @Zltb_elim_Type0
1043     [ 2: normalize #_ #Habsurd destruct (Habsurd) ]
1044     #Hbid' cut (Zltb bid' (Zsucc nextblock) = true) [ lapply (Zlt_to_Zltb_true … Hbid') @zlt_succ ]
1045     #Hbid_succ >Hbid_succ whd in match (low_bound ??) in ⊢ (% → %);
1046     whd in match (high_bound ??) in ⊢ (% → %);
1047     whd in match (update_block ?????);
1048     whd in match (eq_block ??);
1049     cut (eqZb bid' nextblock = false) [ 1: @eqZb_false /2 by not_to_not/ ]
1050     #Hbid_neq >Hbid_neq
1051     cases (eq_region br' r) normalize #H @H
1052| 4: @(mi_region … Hmemory_inj)
1053| 5: @(mi_disjoint … Hmemory_inj)
1054] qed.
1055
1056(* Memory allocation induces a memory extension. *)
1057lemma alloc_memory_ext :
1058  ∀E:embedding.∀m1,m2,m2',z1,z2,r,new_block. ∀H:memory_inj E m1 m2.
1059  alloc m2 z1 z2 r = 〈m2', new_block〉 →
1060  memory_ext E m1 m2'.
1061#E #m1 #m2 #m2' #z1 #z2 #r * #new_block #Hblock_region_eq #Hmemory_inj #Halloc
1062lapply (alloc_memory_inj … Hmemory_inj Halloc)
1063#Hinj' %
1064[ 1: @Hinj'
1065| 2: @[new_block]
1066| 3: #b normalize in ⊢ (%→ ?); * [ 2: #H @(False_ind … H) ]
1067      #Heq destruct (Heq) whd elim m2 in Halloc;
1068      #Hcontents #nextblock #Hnextblock
1069      whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
1070      /2/
1071| 4: * #b #o * #b' #o' #Hvalid_ptr #Hembed %
1072     normalize in ⊢ (% → ?); * [ 2: #H @H ]
1073     #Heq destruct (Heq)
1074     lapply (mi_valid_pointers … Hmemory_inj … Hvalid_ptr Hembed)
1075     whd in ⊢ (% → ?);
1076     (* contradiction because ¬ (valid_block m2 new_block)  *)
1077     elim m2 in Halloc;
1078     #contents_m2 #nextblock_m2 #Hnextblock_m2
1079     whd in ⊢ ((??%?) → ?);
1080     #Heq_alloc destruct (Heq_alloc)
1081     normalize
1082     lapply (irreflexive_Zlt nextblock_m2)
1083     @Zltb_elim_Type0
1084     [ #H * #Habsurd @(False_ind … (Habsurd H)) ] #_ #_ normalize #Habsurd destruct (Habsurd)
1085] qed.
1086
1087lemma bestorev_beloadv_conservation :
1088  ∀mA,mB,wb,wo,v.
1089    bestorev mA (mk_pointer wb wo) v = Some ? mB →
1090    ∀rb,ro. eq_block wb rb = false →
1091    beloadv mA (mk_pointer rb ro) = beloadv mB (mk_pointer rb ro).
1092#mA #mB #wb #wo #v #Hstore #rb #ro #Hblock_neq
1093whd in ⊢ (??%%);
1094elim mB in Hstore; #contentsB #nextblockB #HnextblockB
1095normalize in ⊢ (% → ?);
1096cases (Zltb (block_id wb) (nextblock mA)) normalize nodelta
1097[ 2: #Habsurd destruct (Habsurd) ]
1098cases (if Zleb (low (blocks mA wb)) (Z_of_unsigned_bitvector 16 (offv wo))
1099       then Zltb (Z_of_unsigned_bitvector 16 (offv wo)) (high (blocks mA wb)) 
1100       else false) normalize nodelta
1101[ 2: #Habsurd destruct (Habsurd) ]
1102#Heq destruct (Heq) elim rb in Hblock_neq; #rr #rid elim wb #wr #wid
1103cases rr cases wr normalize try //
1104@(eqZb_elim … rid wid)
1105[ 1,3: #Heq destruct (Heq) >(eqZb_reflexive wid) #Habsurd destruct (Habsurd) ]
1106try //
1107qed.
1108
1109(* lift [bestorev_beloadv_conservation to [loadn] *)
1110lemma bestorev_loadn_conservation :
1111  ∀mA,mB,n,wb,wo,v.
1112    bestorev mA (mk_pointer wb wo) v = Some ? mB →
1113    ∀rb,ro. eq_block wb rb = false →
1114    loadn mA (mk_pointer rb ro) n = loadn mB (mk_pointer rb ro) n.
1115#mA #mB #n
1116elim n
1117[ 1: #wb #wo #v #Hstore #rb #ro #Hblock_neq normalize @refl
1118| 2: #n' #Hind #wb #wo #v #Hstore #rb #ro #Hneq
1119     whd in ⊢ (??%%);
1120     >(bestorev_beloadv_conservation … Hstore … Hneq)
1121     >(Hind … Hstore … Hneq) @refl
1122] qed.
1123
1124(* lift [bestorev_loadn_conservation] to [load_value_of_type] *)
1125lemma bestorev_load_value_of_type_conservation :
1126  ∀mA,mB,wb,wo,v.
1127    bestorev mA (mk_pointer wb wo) v = Some ? mB →
1128    ∀rb,ro. eq_block wb rb = false →
1129    ∀ty.load_value_of_type ty mA rb ro = load_value_of_type ty mB rb ro.
1130#mA #mB #wb #wo #v #Hstore #rb #ro #Hneq #ty
1131cases ty
1132[ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
1133| 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ] try //
1134[ 1: elim sz | 2: elim fsz | 3: | 4: ]
1135whd in ⊢ (??%%);
1136>(bestorev_loadn_conservation … Hstore … Hneq) @refl
1137qed.
1138
1139(* Writing in the "extended" part of a memory preserves the underlying injection *)
1140lemma bestorev_memory_ext_to_load_sim :
1141  ∀E,mA,mB,mC.
1142  ∀Hext:memory_ext E mA mB.
1143  ∀wb,wo,v. meml ? wb (me_writeable … Hext) →
1144  bestorev mB (mk_pointer wb wo) v = Some ? mC →
1145  load_sim_ptr E mA mC.
1146#E #mA #mB #mC #Hext #wb #wo #v #Hwb #Hstore whd
1147#b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Hembed #Hload
1148(* Show that (wb ≠ b2) by showing b2 ∉ (me_writeable ...) *)
1149lapply (me_writeable_ok … Hext (mk_pointer b1 off1) (mk_pointer b2 off2) Hvalid Hembed) #Hb2
1150lapply (mem_not_mem_neq … Hwb Hb2) #Hwb_neq_b2
1151cut ((eq_block wb b2) = false) [ @neq_block_eq_block_false @Hwb_neq_b2 ] #Heq_block_false
1152<(bestorev_load_value_of_type_conservation … Hstore … Heq_block_false)
1153@(mi_inj … (me_inj … Hext) … Hvalid  … Hembed …  Hload)
1154qed.
1155
1156(* Writing in the "extended" part of a memory preserves the whole memory injection *)
1157lemma bestorev_memory_ext_to_memory_inj :
1158  ∀E,mA,mB,mC.
1159  ∀Hext:memory_ext E mA mB.
1160  ∀wb,wo,v. meml ? wb (me_writeable … Hext) →
1161  bestorev mB (mk_pointer wb wo) v = Some ? mC →
1162  memory_inj E mA mC.
1163#E #mA * #contentsB #nextblockB #HnextblockB #mC
1164#Hext #wb #wo #v #Hwb #Hstore
1165%
1166[ 1: @(bestorev_memory_ext_to_load_sim … Hext … Hwb Hstore) ]
1167elim Hext in Hwb; * #Hinj #Hvalid #Hcodomain #Hregion #Hdisjoint #writeable #Hwriteable_valid #Hwriteable_ok
1168#Hmem
1169[ 1: @Hvalid | 3: @Hregion | 4: @Hdisjoint ] -Hvalid -Hregion -Hdisjoint
1170whd in Hstore:(??%?); lapply (Hwriteable_valid … Hmem)
1171normalize in ⊢ (% → ?); #Hlt_wb
1172#p #p' #HvalidA #Hembed lapply (Hcodomain … HvalidA Hembed) -Hcodomain
1173normalize in match (valid_pointer ??) in ⊢ (% → %);
1174>(Zlt_to_Zltb_true … Hlt_wb) in Hstore; normalize nodelta
1175cases (Zleb (low (contentsB wb)) (Z_of_unsigned_bitvector offset_size (offv wo))
1176       ∧Zltb (Z_of_unsigned_bitvector offset_size (offv wo)) (high (contentsB wb)))
1177normalize nodelta
1178[ 2: #Habsurd destruct (Habsurd) ]
1179#Heq destruct (Heq)
1180cases (Zltb (block_id (pblock p')) nextblockB) normalize nodelta
1181[ 2: #H @H ]
1182whd in match (update_block ?????);
1183cut (eq_block (pblock p') wb = false)
1184[ 2: #Heq >Heq normalize nodelta #H @H ]
1185@neq_block_eq_block_false @sym_neq
1186@(mem_not_mem_neq writeable … Hmem)
1187@(Hwriteable_ok … HvalidA Hembed)
1188qed.
1189
1190(* It even preserves memory extensions, with the same writeable blocks.  *)
1191lemma bestorev_memory_ext_to_memory_ext :
1192  ∀E,mA,mB.
1193  ∀Hext:memory_ext E mA mB.
1194  ∀wb,wo,v. meml ? wb (me_writeable … Hext) →
1195  ∀mC.bestorev mB (mk_pointer wb wo) v = Some ? mC →
1196  ΣExt:memory_ext E mA mC.(me_writeable … Hext = me_writeable … Ext).
1197#E #mA #mB #Hext #wb #wo #v #Hmem #mC #Hstore
1198%{(mk_memory_ext …
1199      (bestorev_memory_ext_to_memory_inj … Hext … Hmem … Hstore)
1200      (me_writeable … Hext)
1201      ?
1202      (me_writeable_ok … Hext)
1203 )} try @refl
1204#b #Hmemb
1205lapply (me_writeable_valid … Hext b Hmemb)
1206lapply (me_writeable_valid … Hext wb Hmem)
1207elim mB in Hstore; #contentsB #nextblockB #HnextblockB #Hstore #Hwb_valid #Hb_valid
1208lapply Hstore normalize in Hwb_valid Hb_valid ⊢ (% → ?);
1209>(Zlt_to_Zltb_true … Hwb_valid) normalize nodelta
1210cases (if Zleb (low (contentsB wb)) (Z_of_unsigned_bitvector 16 (offv wo))
1211       then Zltb (Z_of_unsigned_bitvector 16 (offv wo)) (high (contentsB wb)) 
1212       else false)
1213normalize [ 2: #Habsurd destruct (Habsurd) ]
1214#Heq destruct (Heq) @Hb_valid
1215qed.
1216
1217(* Lift [bestorev_memory_ext_to_memory_ext] to storen *)
1218lemma storen_memory_ext_to_memory_ext :
1219  ∀E,mA,l,mB,mC.
1220  ∀Hext:memory_ext E mA mB.
1221  ∀wb,wo. meml ? wb (me_writeable … Hext) →
1222  storen mB (mk_pointer wb wo) l = Some ? mC →
1223  memory_ext E mA mC.
1224#E #mA #l elim l
1225[ 1: #mB #mC #Hext #wb #wo #Hmem normalize in ⊢ (% → ?); #Heq destruct (Heq)
1226     @Hext
1227| 2: #hd #tl #Hind #mB #mC #Hext #wb #wo #Hmem
1228     whd in ⊢ ((??%?) → ?);
1229     lapply (bestorev_memory_ext_to_memory_ext … Hext … wb wo hd Hmem)
1230     cases (bestorev mB (mk_pointer wb wo) hd)
1231     normalize nodelta
1232     [ 1: #H #Habsurd destruct (Habsurd) ]
1233     #mD #H lapply (H mD (refl ??)) * #HextD #Heq #Hstore
1234     @(Hind … HextD … Hstore)
1235     <Heq @Hmem
1236] qed.     
1237
1238(* Lift [storen_memory_ext_to_memory_ext] to store_value_of_type *)
1239lemma store_value_of_type_memory_ext_to_memory_ext :
1240  ∀E,mA,mB,mC.
1241  ∀Hext:memory_ext E mA mB.
1242  ∀wb,wo. meml ? wb (me_writeable … Hext) →
1243  ∀ty,v.store_value_of_type ty mB wb wo v = Some ? mC →
1244  memory_ext E mA mC.
1245#E #mA #mB #mC #Hext #wb #wo #Hmem #ty #v
1246cases ty
1247[ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
1248| 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
1249whd in ⊢ ((??%?) → ?);
1250[ 1,5,6,7,8: #Habsurd destruct (Habsurd) ]
1251#Hstore
1252@(storen_memory_ext_to_memory_ext … Hext … Hmem … Hstore)
1253qed.
1254 
1255 
Note: See TracBrowser for help on using the repository browser.