source: src/Clight/memoryInjections.ma @ 2438

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

Sync of the w.i.p. for switch removal.

File size: 106.6 KB
Line 
1include "Clight/Cexec.ma".
2include "Clight/frontend_misc.ma".
3
4(* This file contains some definitions and lemmas related to memory injections.
5   Could be useful for the Clight → Cminor. Needs revision: the definitions are
6   too lax and allow inconsistent embeddings (more precisely, these embeddings do
7   not allow to prove that the semantics for pointer less-than comparisons is
8   conserved). *)
9
10(* --------------------------------------------------------------------------- *)   
11(* Some general lemmas on bitvectors (offsets /are/ bitvectors) *)
12(* --------------------------------------------------------------------------- *)
13 
14lemma add_with_carries_n_O : ∀n,bv. add_with_carries n bv (zero n) false = 〈bv,zero n〉.
15#n #bv whd in match (add_with_carries ????); elim bv //
16#n #hd #tl #Hind whd in match (fold_right2_i ????????);
17>Hind normalize
18cases n in tl;
19[ 1: #tl cases hd normalize @refl
20| 2: #n' #tl cases hd normalize @refl ]
21qed.
22
23lemma addition_n_0 : ∀n,bv. addition_n n bv (zero n) = bv.
24#n #bv whd in match (addition_n ???);
25>add_with_carries_n_O //
26qed.
27
28lemma replicate_Sn : ∀A,sz,elt.
29  replicate A (S sz) elt = elt ::: (replicate A sz elt).
30// qed.
31
32lemma zero_Sn : ∀n. zero (S n) = false ::: (zero n). // qed.
33
34lemma negation_bv_Sn : ∀n. ∀xa. ∀a : BitVector n. negation_bv … (xa ::: a) = (notb xa) ::: (negation_bv … a).
35#n #xa #a normalize @refl qed.
36
37(* useful facts on carry_of *)
38lemma carry_of_TT : ∀x. carry_of true true x = true. // qed.
39lemma carry_of_TF : ∀x. carry_of true false x = x. // qed.
40lemma carry_of_FF : ∀x. carry_of false false x = false. // qed.
41lemma carry_of_lcomm : ∀x,y,z. carry_of x y z = carry_of y x z. * * * // qed.
42lemma carry_of_rcomm : ∀x,y,z. carry_of x y z = carry_of x z y. * * * // qed.
43
44
45
46definition one_bv ≝ λn. (\fst (add_with_carries … (zero n) (zero n) true)).
47
48lemma one_bv_Sn_aux : ∀n. ∀bits,flags : BitVector (S n).
49    add_with_carries … (zero (S n)) (zero (S n)) true = 〈bits, flags〉 →
50    add_with_carries … (zero (S (S n))) (zero (S (S n))) true = 〈false ::: bits, false ::: flags〉.
51#n elim n
52[ 1: #bits #flags elim (BitVector_Sn … bits) #hd_bits * #tl_bits #Heq_bits
53     elim (BitVector_Sn … flags) #hd_flags * #tl_flags #Heq_flags
54     >(BitVector_O … tl_flags) >(BitVector_O … tl_bits)
55     normalize #Heq destruct (Heq) @refl
56| 2: #n' #Hind #bits #flags elim (BitVector_Sn … bits) #hd_bits * #tl_bits #Heq_bits
57     destruct #Hind >add_with_carries_Sn >replicate_Sn
58     whd in match (zero ?) in Hind; lapply Hind
59     elim (add_with_carries (S (S n'))
60            (false:::replicate bool (S n') false)
61            (false:::replicate bool (S n') false) true) #bits #flags #Heq destruct
62            normalize >add_with_carries_Sn in Hind;
63     elim (add_with_carries (S n') (replicate bool (S n') false)
64                    (replicate bool (S n') false) true) #flags' #bits'
65     normalize
66     cases (match bits' in Vector return λsz:ℕ.(λfoo:Vector bool sz.bool) with 
67            [VEmpty⇒true|VCons (sz:ℕ)   (cy:bool)   (tl:(Vector bool sz))⇒cy])
68     normalize #Heq destruct @refl
69] qed.     
70
71lemma one_bv_Sn : ∀n. one_bv (S (S n)) = false ::: (one_bv (S n)).
72#n lapply (one_bv_Sn_aux n)
73whd in match (one_bv ?) in ⊢ (? → (??%%));
74elim (add_with_carries (S n) (zero (S n)) (zero (S n)) true) #bits #flags
75#H lapply (H bits flags (refl ??)) #H2 >H2 @refl
76qed.
77
78lemma increment_to_addition_n_aux : ∀n. ∀a : BitVector n.
79    add_with_carries ? a (zero n) true = add_with_carries ? a (one_bv n) false.
80#n   
81elim n
82[ 1: #a >(BitVector_O … a) normalize @refl
83| 2: #n' cases n'
84     [ 1: #Hind #a elim (BitVector_Sn ? a) #xa * #tl #Heq destruct
85          >(BitVector_O … tl) normalize cases xa @refl
86     | 2: #n'' #Hind #a elim (BitVector_Sn ? a) #xa * #tl #Heq destruct
87          >one_bv_Sn >zero_Sn
88          lapply (Hind tl)
89          >add_with_carries_Sn >add_with_carries_Sn
90          #Hind >Hind elim (add_with_carries (S n'') tl (one_bv (S n'')) false) #bits #flags
91          normalize nodelta elim (BitVector_Sn … flags) #flags_hd * #flags_tl #Hflags_eq >Hflags_eq
92          normalize nodelta @refl
93] qed.         
94
95(* In order to use associativity on increment, we hide it under addition_n. *)
96lemma increment_to_addition_n : ∀n. ∀a : BitVector n. increment ? a = addition_n ? a (one_bv n).
97#n
98whd in match (increment ??) in ⊢ (∀_.??%?);
99whd in match (addition_n ???) in ⊢ (∀_.???%);
100#a lapply (increment_to_addition_n_aux n a)
101#Heq >Heq cases (add_with_carries n a (one_bv n) false) #bits #flags @refl
102qed.
103
104(* Explicit formulation of addition *)
105
106(* Explicit formulation of the last carry bit *)
107let rec ith_carry (n : nat) (a,b : BitVector n) (init : bool) on n : bool ≝
108match n return λx. BitVector x → BitVector x → bool with
109[ O ⇒ λ_,_. init
110| S x ⇒ λa',b'.
111  let hd_a ≝ head' … a' in
112  let hd_b ≝ head' … b' in
113  let tl_a ≝ tail … a' in
114  let tl_b ≝ tail … b' in
115  carry_of hd_a hd_b (ith_carry x tl_a tl_b init)
116] a b.
117
118lemma ith_carry_unfold : ∀n. ∀init. ∀a,b : BitVector (S n).
119  ith_carry ? a b init = (carry_of (head' … a) (head' … b) (ith_carry ? (tail … a) (tail … b) init)).
120#n #init #a #b @refl qed.
121
122lemma ith_carry_Sn : ∀n. ∀init. ∀xa,xb. ∀a,b : BitVector n.
123  ith_carry ? (xa ::: a) (xb ::: b) init = (carry_of xa xb (ith_carry ? a b init)). // qed.
124
125(* correction of [ith_carry] *)
126lemma ith_carry_ok : ∀n. ∀init. ∀a,b,res_ab,flags_ab : BitVector (S n).
127  〈res_ab,flags_ab〉 = add_with_carries ? a b init →
128  head' … flags_ab = ith_carry ? a b init.
129#n elim n
130[ 1: #init #a #b #res_ab #flags_ab
131     elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a
132     elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b
133     elim (BitVector_Sn … res_ab) #hd_res * #tl_res #Heq_res
134     elim (BitVector_Sn … flags_ab) #hd_flags * #tl_flags #Heq_flags
135     destruct
136     >(BitVector_O … tl_a) >(BitVector_O … tl_b)
137     cases hd_a cases hd_b cases init normalize #Heq destruct (Heq)
138     @refl
139| 2: #n' #Hind #init #a #b #res_ab #flags_ab
140     elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a
141     elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b
142     elim (BitVector_Sn … res_ab) #hd_res * #tl_res #Heq_res
143     elim (BitVector_Sn … flags_ab) #hd_flags * #tl_flags #Heq_flags
144     destruct
145     lapply (Hind … init tl_a tl_b tl_res tl_flags)
146     >add_with_carries_Sn >(ith_carry_Sn (S n'))
147     elim (add_with_carries (S n') tl_a tl_b init) #res_ab #flags_ab
148     elim (BitVector_Sn … flags_ab) #hd_flags_ab * #tl_flags_ab #Heq_flags_ab >Heq_flags_ab
149     normalize nodelta cases hd_flags_ab normalize nodelta
150     whd in match (head' ? (S n') ?); #H1 #H2
151     destruct (H2) lapply (H1 (refl ??)) whd in match (head' ???); #Heq <Heq @refl
152] qed.
153
154(* Explicit formulation of ith bit of an addition, with explicit initial carry bit. *)
155definition ith_bit ≝ λ(n : nat).λ(a,b : BitVector n).λinit.
156match n return λx. BitVector x → BitVector x → bool with
157[ O ⇒ λ_,_. init
158| S x ⇒ λa',b'.
159  let hd_a ≝ head' … a' in
160  let hd_b ≝ head' … b' in
161  let tl_a ≝ tail … a' in
162  let tl_b ≝ tail … b' in
163  xorb (xorb hd_a hd_b) (ith_carry x tl_a tl_b init)
164] a b.
165
166lemma ith_bit_unfold : ∀n. ∀init. ∀a,b : BitVector (S n).
167  ith_bit ? a b init =  xorb (xorb (head' … a) (head' … b)) (ith_carry ? (tail … a) (tail … b) init).
168#n #a #b // qed.
169
170lemma ith_bit_Sn : ∀n. ∀init. ∀xa,xb. ∀a,b : BitVector n.
171  ith_bit ? (xa ::: a) (xb ::: b) init =  xorb (xorb xa xb) (ith_carry ? a b init). // qed.
172
173(* correction of ith_bit *)
174lemma ith_bit_ok : ∀n. ∀init. ∀a,b,res_ab,flags_ab : BitVector (S n).
175  〈res_ab,flags_ab〉 = add_with_carries ? a b init →
176  head' … res_ab = ith_bit ? a b init.
177#n
178cases n
179[ 1: #init #a #b #res_ab #flags_ab
180     elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a
181     elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b
182     elim (BitVector_Sn … res_ab) #hd_res * #tl_res #Heq_res
183     elim (BitVector_Sn … flags_ab) #hd_flags * #tl_flags #Heq_flags
184     destruct
185     >(BitVector_O … tl_a) >(BitVector_O … tl_b)
186     >(BitVector_O … tl_flags) >(BitVector_O … tl_res)
187     normalize cases init cases hd_a cases hd_b normalize #Heq destruct @refl
188| 2: #n' #init #a #b #res_ab #flags_ab
189     elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a
190     elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b
191     elim (BitVector_Sn … res_ab) #hd_res * #tl_res #Heq_res
192     elim (BitVector_Sn … flags_ab) #hd_flags * #tl_flags #Heq_flags
193     destruct
194     lapply (ith_carry_ok … init tl_a tl_b tl_res tl_flags)
195     #Hcarry >add_with_carries_Sn elim (add_with_carries ? tl_a tl_b init) in Hcarry;
196     #res #flags normalize nodelta elim (BitVector_Sn … flags) #hd_flags' * #tl_flags' #Heq_flags'
197     >Heq_flags' normalize nodelta cases hd_flags' normalize nodelta #H1 #H2 destruct (H2)
198     cases hd_a cases hd_b >ith_bit_Sn whd in match (head' ???) in H1 ⊢ %;
199     <(H1 (refl ??)) @refl
200] qed.
201
202(* Transform a function from bit-vectors to bits into a vector by folding *)
203let rec bitvector_fold (n : nat) (v : BitVector n) (f : ∀sz. BitVector sz → bool) on v : BitVector n ≝
204match v with
205[ VEmpty ⇒ VEmpty ?
206| VCons sz elt tl ⇒
207  let bit ≝ f ? v in
208  bit ::: (bitvector_fold ? tl f)
209].
210
211(* Two-arguments version *)
212let rec bitvector_fold2 (n : nat) (v1, v2 : BitVector n) (f : ∀sz. BitVector sz → BitVector sz → bool) on v1 : BitVector n ≝
213match v1  with
214[ VEmpty ⇒ λ_. VEmpty ?
215| VCons sz elt tl ⇒ λv2'.
216  let bit ≝ f ? v1 v2 in
217  bit ::: (bitvector_fold2 ? tl (tail … v2') f)
218] v2.
219
220lemma bitvector_fold2_Sn : ∀n,x1,x2,v1,v2,f.
221  bitvector_fold2 (S n) (x1 ::: v1) (x2 ::: v2) f = (f ? (x1 ::: v1) (x2 ::: v2)) ::: (bitvector_fold2 … v1 v2 f). // qed.
222
223(* These functions pack all the relevant information (including carries) directly. *)
224definition addition_n_direct ≝ λn,v1,v2,init. bitvector_fold2 n v1 v2 (λn,v1,v2. ith_bit n v1 v2 init).
225
226lemma addition_n_direct_Sn : ∀n,x1,x2,v1,v2,init.
227  addition_n_direct (S n) (x1 ::: v1) (x2 ::: v2) init = (ith_bit ? (x1 ::: v1) (x2 ::: v2) init) ::: (addition_n_direct … v1 v2 init). // qed.
228 
229lemma tail_Sn : ∀n. ∀x. ∀a : BitVector n. tail … (x ::: a) = a. // qed.
230
231(* Prove the equivalence of addition_n_direct with add_with_carries *)
232lemma addition_n_direct_ok : ∀n,carry,v1,v2.
233  (\fst (add_with_carries n v1 v2 carry)) = addition_n_direct n v1 v2 carry.
234#n elim n
235[ 1: #carry #v1 #v2 >(BitVector_O … v1) >(BitVector_O … v2) normalize @refl
236| 2: #n' #Hind #carry #v1 #v2
237     elim (BitVector_Sn … v1) #hd1 * #tl1 #Heq1
238     elim (BitVector_Sn … v2) #hd2 * #tl2 #Heq2
239     lapply (Hind carry tl1 tl2)
240     lapply (ith_bit_ok ? carry v1 v2)
241     lapply (ith_carry_ok ? carry v1 v2)
242     destruct
243     #Hind >addition_n_direct_Sn
244     >ith_bit_Sn >add_with_carries_Sn
245     elim (add_with_carries n' tl1 tl2 carry) #bits #flags normalize nodelta
246     cases (match flags in Vector return λsz:ℕ.(λfoo:Vector bool sz.bool) with 
247            [VEmpty⇒carry|VCons (sz:ℕ)   (cy:bool)   (tl:(Vector bool sz))⇒cy])
248     normalize nodelta #Hcarry' lapply (Hcarry' ?? (refl ??))
249     whd in match head'; normalize nodelta
250     #H1 #H2 >H1 >H2 @refl
251] qed.
252
253lemma addition_n_direct_ok2 : ∀n,carry,v1,v2.
254  (let 〈a,b〉 ≝ add_with_carries n v1 v2 carry in a) = addition_n_direct n v1 v2 carry.
255#n #carry #v1 #v2 <addition_n_direct_ok
256cases (add_with_carries ????) //
257qed.
258 
259(* trivially lift associativity to our new setting *)     
260lemma associative_addition_n_direct : ∀n. ∀carry1,carry2. ∀v1,v2,v3 : BitVector n.
261  addition_n_direct ? (addition_n_direct ? v1 v2 carry1) v3 carry2 =
262  addition_n_direct ? v1 (addition_n_direct ? v2 v3 carry1) carry2.
263#n #carry1 #carry2 #v1 #v2 #v3
264<addition_n_direct_ok <addition_n_direct_ok
265<addition_n_direct_ok <addition_n_direct_ok
266lapply (associative_add_with_carries … carry1 carry2 v1 v2 v3)
267elim (add_with_carries n v2 v3 carry1) #bits #carries normalize nodelta
268elim (add_with_carries n v1 v2 carry1) #bits' #carries' normalize nodelta
269#H @(sym_eq … H)
270qed.
271
272lemma commutative_addition_n_direct : ∀n. ∀v1,v2 : BitVector n.
273  addition_n_direct ? v1 v2 false = addition_n_direct ? v2 v1 false.
274#n #v1 #v2 /by associative_addition_n, addition_n_direct_ok/
275qed.
276
277definition increment_direct ≝ λn,v. addition_n_direct n v (one_bv ?) false.
278definition twocomp_neg_direct ≝ λn,v. increment_direct n (negation_bv n v).
279
280
281(* fold andb on a bitvector. *)
282let rec andb_fold (n : nat) (b : BitVector n) on b : bool ≝
283match b with
284[ VEmpty ⇒ true
285| VCons sz elt tl ⇒
286  andb elt (andb_fold ? tl)
287].
288
289lemma andb_fold_Sn : ∀n. ∀x. ∀b : BitVector n. andb_fold (S n) (x ::: b) = andb x (andb_fold … n b). // qed.
290
291lemma andb_fold_inversion : ∀n. ∀elt,x. andb_fold (S n) (elt ::: x) = true → elt = true ∧ andb_fold n x = true.
292#n #elt #x cases elt normalize #H @conj destruct (H) try assumption @refl
293qed.
294
295lemma ith_increment_carry : ∀n. ∀a : BitVector (S n).
296  ith_carry … a (one_bv ?) false = andb_fold … a.
297#n elim n
298[ 1: #a elim (BitVector_Sn … a) #hd * #tl #Heq >Heq >(BitVector_O … tl)
299     cases hd normalize @refl
300| 2: #n' #Hind #a
301     elim (BitVector_Sn … a) #hd * #tl #Heq >Heq
302     lapply (Hind … tl) #Hind >one_bv_Sn
303     >ith_carry_Sn whd in match (andb_fold ??);
304     cases hd >Hind @refl
305] qed.
306
307lemma ith_increment_bit : ∀n. ∀a : BitVector (S n).
308  ith_bit … a (one_bv ?) false = xorb (head' … a) (andb_fold … (tail … a)).
309#n #a
310elim (BitVector_Sn … a) #hd * #tl #Heq >Heq
311whd in match (head' ???);
312-a cases n in tl;
313[ 1: #tl >(BitVector_O … tl) cases hd normalize try //
314| 2: #n' #tl >one_bv_Sn >ith_bit_Sn
315     >ith_increment_carry >tail_Sn
316     cases hd try //
317] qed.
318
319(* Lemma used to prove involutivity of two-complement negation *)
320lemma twocomp_neg_involutive_aux : ∀n. ∀v : BitVector (S n).
321   (andb_fold (S n) (negation_bv (S n) v) =
322    andb_fold (S n) (negation_bv (S n) (addition_n_direct (S n) (negation_bv (S n) v) (one_bv (S n)) false))).
323#n elim n
324[ 1: #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq >(BitVector_O … tl) cases hd @refl
325| 2: #n' #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq
326     lapply (Hind tl) -Hind #Hind >negation_bv_Sn >one_bv_Sn >addition_n_direct_Sn
327     >andb_fold_Sn >ith_bit_Sn >negation_bv_Sn >andb_fold_Sn <Hind
328     cases hd normalize nodelta
329     [ 1: >xorb_false >(xorb_comm false ?) >xorb_false
330     | 2: >xorb_false >(xorb_comm true ?) >xorb_true ]
331     >ith_increment_carry
332     cases (andb_fold (S n') (negation_bv (S n') tl)) @refl
333] qed.
334   
335(* Test of the 'direct' approach: proof of the involutivity of two-complement negation. *)
336lemma twocomp_neg_involutive : ∀n. ∀v : BitVector n. twocomp_neg_direct ? (twocomp_neg_direct ? v) = v.
337#n elim n
338[ 1: #v >(BitVector_O v) @refl
339| 2: #n' cases n'
340     [ 1: #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq
341          >(BitVector_O … tl) normalize cases hd @refl
342     | 2: #n'' #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq
343          lapply (Hind tl) -Hind #Hind <Hind in ⊢ (???%);
344          whd in match twocomp_neg_direct; normalize nodelta
345          whd in match increment_direct; normalize nodelta
346          >(negation_bv_Sn ? hd tl) >one_bv_Sn >(addition_n_direct_Sn ? (¬hd) false ??)
347          >ith_bit_Sn >negation_bv_Sn >addition_n_direct_Sn >ith_bit_Sn
348          generalize in match (addition_n_direct (S n'')
349                                                   (negation_bv (S n'')
350                                                   (addition_n_direct (S n'') (negation_bv (S n'') tl) (one_bv (S n'')) false))
351                                                   (one_bv (S n'')) false); #tail
352          >ith_increment_carry >ith_increment_carry
353          cases hd normalize nodelta
354          [ 1: normalize in match (xorb false false); >(xorb_comm false ?) >xorb_false >xorb_false
355          | 2: normalize in match (xorb true false); >(xorb_comm true ?) >xorb_true >xorb_false ]
356          <twocomp_neg_involutive_aux
357          cases (andb_fold (S n'') (negation_bv (S n'') tl)) @refl
358      ]
359] qed.
360
361lemma bitvector_cons_inj_inv : ∀n. ∀a,b. ∀va,vb : BitVector n. a ::: va = b ::: vb → a =b ∧ va = vb.
362#n #a #b #va #vb #H destruct (H) @conj @refl qed.
363
364lemma bitvector_cons_eq : ∀n. ∀a,b. ∀v : BitVector n. a = b → a ::: v = b ::: v. // qed.
365
366(* Injectivity of increment *)
367lemma increment_inj : ∀n. ∀a,b : BitVector n.
368  increment_direct ? a = increment_direct ? b →
369  a = b ∧ (ith_carry n a (one_bv n) false = ith_carry n b (one_bv n) false).
370#n whd in match increment_direct; normalize nodelta elim n
371[ 1: #a #b >(BitVector_O … a) >(BitVector_O … b) normalize #_ @conj //
372| 2: #n' cases n'
373   [ 1: #_ #a #b
374        elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a >Heq_a
375        elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b >Heq_b
376        >(BitVector_O … tl_a) >(BitVector_O … tl_b) cases hd_a cases hd_b
377        normalize #H @conj try //
378   | 2: #n'' #Hind #a #b
379        elim (BitVector_Sn … a) #hd_a * #tl_a #Heq_a >Heq_a
380        elim (BitVector_Sn … b) #hd_b * #tl_b #Heq_b >Heq_b
381        lapply (Hind … tl_a tl_b) -Hind #Hind
382        >one_bv_Sn >addition_n_direct_Sn >ith_bit_Sn
383        >addition_n_direct_Sn >ith_bit_Sn >xorb_false >xorb_false
384        #H elim (bitvector_cons_inj_inv … H) #Heq1 #Heq2
385        lapply (Hind Heq2) * #Heq3 #Heq4
386        cut (hd_a = hd_b)
387        [ 1: >Heq4 in Heq1; #Heq5 lapply (xorb_inj (ith_carry ? tl_b (one_bv ?) false) hd_a hd_b)
388             * #Heq6 #_ >xorb_comm in Heq6; >(xorb_comm  ? hd_b) #Heq6 >(Heq6 Heq5)
389             @refl ]
390        #Heq5 @conj [ 1: >Heq3 >Heq5 @refl ]
391        >ith_carry_Sn >ith_carry_Sn >Heq4 >Heq5 @refl
392] qed.
393
394(* Inverse of injecivity of increment, does not lose information (cf increment_inj) *)
395lemma increment_inj_inv : ∀n. ∀a,b : BitVector n.
396  a = b → increment_direct ? a = increment_direct ? b. // qed.
397
398(* A more general result. *)
399lemma addition_n_direct_inj : ∀n. ∀x,y,delta: BitVector n.
400  addition_n_direct ? x delta false = addition_n_direct ? y delta false →
401  x = y ∧ (ith_carry n x delta false = ith_carry n y delta false).
402#n elim n
403[ 1: #x #y #delta >(BitVector_O … x) >(BitVector_O … y) >(BitVector_O … delta) * @conj @refl
404| 2: #n' #Hind #x #y #delta
405     elim (BitVector_Sn … x) #hdx * #tlx #Heqx >Heqx
406     elim (BitVector_Sn … y) #hdy * #tly #Heqy >Heqy
407     elim (BitVector_Sn … delta) #hdd * #tld #Heqd >Heqd
408     >addition_n_direct_Sn >ith_bit_Sn
409     >addition_n_direct_Sn >ith_bit_Sn
410     >ith_carry_Sn >ith_carry_Sn
411     lapply (Hind … tlx tly tld) -Hind #Hind #Heq
412     elim (bitvector_cons_inj_inv … Heq) #Heq_hd #Heq_tl
413     lapply (Hind Heq_tl) -Hind * #HindA #HindB
414     >HindA >HindB >HindB in Heq_hd; #Heq_hd
415     cut (hdx = hdy)
416     [ 1: cases hdd in Heq_hd; cases (ith_carry n' tly tld false)
417          cases hdx cases hdy normalize #H try @H try @refl
418          >H try @refl ]
419     #Heq_hd >Heq_hd @conj @refl
420] qed.
421
422(* We also need it the other way around. *)
423lemma addition_n_direct_inj_inv : ∀n. ∀x,y,delta: BitVector n.
424  x ≠ y → (* ∧ (ith_carry n x delta false = ith_carry n y delta false). *)
425   addition_n_direct ? x delta false ≠ addition_n_direct ? y delta false.
426#n elim n
427[ 1: #x #y #delta >(BitVector_O … x) >(BitVector_O … y) >(BitVector_O … delta) * #H @(False_ind … (H (refl ??)))
428| 2: #n' #Hind #x #y #delta
429     elim (BitVector_Sn … x) #hdx * #tlx #Heqx >Heqx
430     elim (BitVector_Sn … y) #hdy * #tly #Heqy >Heqy
431     elim (BitVector_Sn … delta) #hdd * #tld #Heqd >Heqd
432     #Hneq
433     cut (hdx ≠ hdy ∨ tlx ≠ tly)
434     [ @(eq_bv_elim … tlx tly)
435       [ #Heq_tl >Heq_tl >Heq_tl in Hneq;
436         #Hneq cut (hdx ≠ hdy) [ % #Heq_hd >Heq_hd in Hneq; *
437                                 #H @H @refl ]
438         #H %1 @H
439       | #H %2 @H ] ]
440     -Hneq #Hneq
441     >addition_n_direct_Sn >addition_n_direct_Sn
442     >ith_bit_Sn >ith_bit_Sn cases Hneq
443     [ 1: #Hneq_hd
444          lapply (addition_n_direct_inj … tlx tly tld)         
445          @(eq_bv_elim … (addition_n_direct ? tlx tld false) (addition_n_direct ? tly tld false))
446          [ 1: #Heq -Hind #Hind elim (Hind Heq) #Heq_tl >Heq_tl #Heq_carry >Heq_carry
447               % #Habsurd elim (bitvector_cons_inj_inv … Habsurd) -Habsurd
448               lapply Hneq_hd
449               cases hdx cases hdd cases hdy cases (ith_carry ? tly tld false)
450               normalize in ⊢ (? → % → ?); #Hneq_hd #Heq_hd #_
451               try @(absurd … Heq_hd Hneq_hd)
452               elim Hneq_hd -Hneq_hd #Hneq_hd @Hneq_hd
453               try @refl try assumption try @(sym_eq … Heq_hd)
454          | 2: #Htl_not_eq #_ % #Habsurd elim (bitvector_cons_inj_inv … Habsurd) #_
455               elim Htl_not_eq -Htl_not_eq #HA #HB @HA @HB ]
456     | 2: #Htl_not_eq lapply (Hind tlx tly tld Htl_not_eq) -Hind #Hind
457          % #Habsurd elim (bitvector_cons_inj_inv … Habsurd) #_
458          elim Hind -Hind #HA #HB @HA @HB ]
459] qed.
460
461lemma carry_notb : ∀a,b,c. notb (carry_of a b c) = carry_of (notb a) (notb b) (notb c). * * * @refl qed.
462
463lemma increment_to_carry_aux : ∀n. ∀a : BitVector (S n).
464   ith_carry (S n) a (one_bv (S n)) false
465   = ith_carry (S n) a (zero (S n)) true.
466#n elim n
467[ 1: #a elim (BitVector_Sn ? a) #hd_a * #tl_a #Heq >Heq >(BitVector_O … tl_a) @refl
468| 2: #n' #Hind #a elim (BitVector_Sn ? a) #hd_a * #tl_a #Heq >Heq
469     lapply (Hind tl_a) #Hind
470     >one_bv_Sn >zero_Sn >ith_carry_Sn >ith_carry_Sn >Hind @refl
471] qed.
472
473lemma neutral_addition_n_direct_aux : ∀n. ∀v. ith_carry n v (zero n) false = false.
474#n elim n //
475#n' #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq >zero_Sn
476>ith_carry_Sn >(Hind tl) cases hd @refl.
477qed.
478
479lemma neutral_addition_n_direct : ∀n. ∀v : BitVector n.
480  addition_n_direct ? v (zero ?) false = v.
481#n elim n
482[ 1: #v >(BitVector_O … v) normalize @refl
483| 2: #n' #Hind #v elim (BitVector_Sn … v) #hd * #tl #Heq >Heq
484     lapply (Hind … tl) #H >zero_Sn >addition_n_direct_Sn
485     >ith_bit_Sn >H >xorb_false >neutral_addition_n_direct_aux
486     >xorb_false @refl
487] qed.
488
489lemma increment_to_carry_zero : ∀n. ∀a : BitVector n. addition_n_direct ? a (one_bv ?) false = addition_n_direct ? a (zero ?) true.
490#n elim n
491[ 1: #a >(BitVector_O … a) normalize @refl
492| 2: #n' cases n'
493     [ 1: #_ #a elim (BitVector_Sn … a) #hd_a * #tl_a #Heq >Heq >(BitVector_O … tl_a) cases hd_a @refl
494     | 2: #n'' #Hind #a
495          elim (BitVector_Sn … a) #hd_a * #tl_a #Heq >Heq
496          lapply (Hind tl_a) -Hind #Hind
497          >one_bv_Sn >zero_Sn >addition_n_direct_Sn >ith_bit_Sn
498          >addition_n_direct_Sn >ith_bit_Sn
499          >xorb_false >Hind @bitvector_cons_eq
500          >increment_to_carry_aux @refl
501     ]
502] qed.
503
504lemma increment_to_carry : ∀n. ∀a,b : BitVector n.
505  addition_n_direct ? a (addition_n_direct ? b (one_bv ?) false) false = addition_n_direct ? a b true.
506#n #a #b >increment_to_carry_zero <associative_addition_n_direct
507>neutral_addition_n_direct @refl
508qed.
509
510lemma increment_direct_ok : ∀n,v. increment_direct n v = increment n v.
511#n #v whd in match (increment ??);
512>addition_n_direct_ok <increment_to_carry_zero @refl
513qed.
514
515(* Prove -(a + b) = -a + -b *)
516lemma twocomp_neg_plus : ∀n. ∀a,b : BitVector n.
517  twocomp_neg_direct ? (addition_n_direct ? a b false) = addition_n_direct ? (twocomp_neg_direct … a) (twocomp_neg_direct … b) false.
518whd in match twocomp_neg_direct; normalize nodelta
519lapply increment_inj_inv
520whd in match increment_direct; normalize nodelta
521#H #n #a #b
522<associative_addition_n_direct @H
523>associative_addition_n_direct >(commutative_addition_n_direct ? (one_bv n))
524>increment_to_carry
525-H lapply b lapply a -b -a
526cases n
527[ 1: #a #b >(BitVector_O … a) >(BitVector_O … b) @refl
528| 2: #n' #a #b
529     cut (negation_bv ? (addition_n_direct ? a b false)
530           = addition_n_direct ? (negation_bv ? a) (negation_bv ? b) true ∧
531          notb (ith_carry ? a b false) = (ith_carry ? (negation_bv ? a) (negation_bv ? b) true))
532     [ -n lapply b lapply a elim n'
533     [ 1: #a #b elim (BitVector_Sn … a) #hd_a * #tl_a #Heqa >Heqa >(BitVector_O … tl_a)
534          elim (BitVector_Sn … b) #hd_b * #tl_b #Heqb >Heqb >(BitVector_O … tl_b)
535          cases hd_a cases hd_b normalize @conj @refl
536     | 2: #n #Hind #a #b
537          elim (BitVector_Sn … a) #hd_a * #tl_a #Heqa >Heqa
538          elim (BitVector_Sn … b) #hd_b * #tl_b #Heqb >Heqb
539          lapply (Hind tl_a tl_b) * #H1 #H2
540          @conj
541          [ 2: >ith_carry_Sn >negation_bv_Sn >negation_bv_Sn >ith_carry_Sn
542               >carry_notb >H2 @refl
543          | 1: >addition_n_direct_Sn >ith_bit_Sn >negation_bv_Sn
544               >negation_bv_Sn >negation_bv_Sn
545               >addition_n_direct_Sn >ith_bit_Sn >H1 @bitvector_cons_eq
546               >xorb_lneg >xorb_rneg >notb_notb
547               <xorb_rneg >H2 @refl
548          ]
549      ] ]
550      * #H1 #H2 @H1
551] qed.
552
553lemma addition_n_direct_neg : ∀n. ∀a.
554 (addition_n_direct n a (negation_bv n a) false) = replicate ?? true
555 ∧ (ith_carry n a (negation_bv n a) false = false).
556#n elim n
557[ 1: #a >(BitVector_O … a) @conj @refl
558| 2: #n' #Hind #a elim (BitVector_Sn … a) #hd * #tl #Heq >Heq
559     lapply (Hind … tl) -Hind * #HA #HB
560     @conj
561     [ 2: >negation_bv_Sn >ith_carry_Sn >HB cases hd @refl
562     | 1: >negation_bv_Sn >addition_n_direct_Sn
563          >ith_bit_Sn >HB >xorb_false >HA
564          @bitvector_cons_eq elim hd @refl
565     ]
566] qed.
567
568(* -a + a = 0 *)
569lemma bitvector_opp_direct : ∀n. ∀a : BitVector n. addition_n_direct ? a (twocomp_neg_direct ? a) false = (zero ?).
570whd in match twocomp_neg_direct;
571whd in match increment_direct;
572normalize nodelta
573#n #a <associative_addition_n_direct
574elim (addition_n_direct_neg … a) #H #_ >H
575-H -a
576cases n try //
577#n'
578cut ((addition_n_direct (S n') (replicate bool ? true) (one_bv ?) false = (zero (S n')))
579       ∧ (ith_carry ? (replicate bool (S n') true) (one_bv (S n')) false = true))
580[ elim n'
581     [ 1: @conj @refl
582     | 2: #n' * #HA #HB @conj
583          [ 1: >replicate_Sn >one_bv_Sn  >addition_n_direct_Sn
584               >ith_bit_Sn >HA >zero_Sn @bitvector_cons_eq >HB @refl
585          | 2: >replicate_Sn >one_bv_Sn >ith_carry_Sn >HB @refl ]
586     ]
587] * #H1 #H2 @H1
588qed.
589
590(* Lift back the previous result to standard operations. *)
591lemma twocomp_neg_direct_ok : ∀n. ∀v. twocomp_neg_direct ? v = two_complement_negation n v.
592#n #v whd in match twocomp_neg_direct; normalize nodelta
593whd in match increment_direct; normalize nodelta
594whd in match two_complement_negation; normalize nodelta
595>increment_to_addition_n <addition_n_direct_ok
596whd in match addition_n; normalize nodelta
597elim (add_with_carries ????) #a #b @refl
598qed.
599
600lemma two_complement_negation_plus : ∀n. ∀a,b : BitVector n.
601  two_complement_negation ? (addition_n ? a b) = addition_n ? (two_complement_negation ? a) (two_complement_negation ? b).
602#n #a #b
603lapply (twocomp_neg_plus ? a b)
604>twocomp_neg_direct_ok >twocomp_neg_direct_ok >twocomp_neg_direct_ok
605<addition_n_direct_ok <addition_n_direct_ok
606whd in match addition_n; normalize nodelta
607elim (add_with_carries n a b false) #bits #flags normalize nodelta
608elim (add_with_carries n (two_complement_negation n a) (two_complement_negation n b) false) #bits' #flags'
609normalize nodelta #H @H
610qed.
611
612lemma bitvector_opp_addition_n : ∀n. ∀a : BitVector n. addition_n ? a (two_complement_negation ? a) = (zero ?).
613#n #a lapply (bitvector_opp_direct ? a)
614>twocomp_neg_direct_ok <addition_n_direct_ok
615whd in match (addition_n ???);
616elim (add_with_carries n a (two_complement_negation n a) false) #bits #flags #H @H
617qed.
618
619lemma neutral_addition_n : ∀n. ∀a : BitVector n. addition_n ? a (zero ?) = a.
620#n #a
621lapply (neutral_addition_n_direct n a)
622<addition_n_direct_ok
623whd in match (addition_n ???);
624elim (add_with_carries n a (zero n) false) #bits #flags #H @H
625qed.
626
627lemma injective_addition_n : ∀n. ∀x,y,delta : BitVector n.
628  addition_n ? x delta = addition_n ? y delta → x = y. 
629#n #x #y #delta 
630lapply (addition_n_direct_inj … x y delta)
631<addition_n_direct_ok <addition_n_direct_ok
632whd in match addition_n; normalize nodelta
633elim (add_with_carries n x delta false) #bitsx #flagsx
634elim (add_with_carries n y delta false) #bitsy #flagsy
635normalize #H1 #H2 elim (H1 H2) #Heq #_ @Heq
636qed.
637
638lemma injective_inv_addition_n : ∀n. ∀x,y,delta : BitVector n.
639  x ≠ y → addition_n ? x delta ≠ addition_n ? y delta. 
640#n #x #y #delta 
641lapply (addition_n_direct_inj_inv … x y delta)
642<addition_n_direct_ok <addition_n_direct_ok
643whd in match addition_n; normalize nodelta
644elim (add_with_carries n x delta false) #bitsx #flagsx
645elim (add_with_carries n y delta false) #bitsy #flagsy
646normalize #H1 #H2 @(H1 H2)
647qed.
648
649
650(* --------------------------------------------------------------------------- *)   
651(* Aux lemmas that are likely to be found elsewhere. *)
652(* --------------------------------------------------------------------------- *)   
653
654lemma zlt_succ : ∀a,b. Zltb a b = true → Zltb a (Zsucc b) = true.
655#a #b #HA
656lapply (Zltb_true_to_Zlt … HA) #HA_prop
657@Zlt_to_Zltb_true /2/
658qed.
659
660lemma zlt_succ_refl : ∀a. Zltb a (Zsucc a) = true.
661#a @Zlt_to_Zltb_true /2/ qed.
662(*
663definition le_offset : offset → offset → bool.
664  λx,y. Zleb (offv x) (offv y).
665*)
666lemma not_refl_absurd : ∀A:Type[0].∀x:A. x ≠ x → False. /2/. qed.
667
668lemma eqZb_reflexive : ∀x:Z. eqZb x x = true. #x /2/. qed.
669
670(* --------------------------------------------------------------------------- *)   
671(* In the definition of injections below, we maintain a list of blocks that are
672   writeable. We need some lemmas to reason on the fact that a block cannot be
673   both writeable and not writeable, etc. *)
674(* --------------------------------------------------------------------------- *)
675
676(* When equality on A is decidable, [mem A elt l] is too. *)
677lemma mem_dec : ∀A:Type[0]. ∀eq:(∀a,b:A. a = b ∨ a ≠ b). ∀elt,l. mem A elt l ∨ ¬ (mem A elt l).
678#A #dec #elt #l elim l
679[ 1: normalize %2 /2/
680| 2: #hd #tl #Hind
681     elim (dec elt hd)
682     [ 1: #Heq >Heq %1 /2/
683     | 2: #Hneq cases Hind
684        [ 1: #Hmem %1 /2/
685        | 2: #Hnmem %2 normalize
686              % #H cases H
687              [ 1: lapply Hneq * #Hl #Eq @(Hl Eq)
688              | 2: lapply Hnmem * #Hr #Hmem @(Hr Hmem) ]
689] ] ]
690qed.
691
692lemma block_eq_dec : ∀a,b:block. a = b ∨ a ≠ b.
693#a #b @(eq_block_elim … a b) /2/ qed.
694
695lemma mem_not_mem_neq : ∀l,elt1,elt2. (mem block elt1 l) → ¬ (mem block elt2 l) → elt1 ≠ elt2.
696#l #elt1 #elt2 elim l
697[ 1: normalize #Habsurd @(False_ind … Habsurd)
698| 2: #hd #tl #Hind normalize #Hl #Hr
699   cases Hl
700   [ 1: #Heq >Heq
701        @(eq_block_elim … hd elt2)
702        [ 1: #Heq >Heq /2 by not_to_not/
703        | 2: #x @x ]
704   | 2: #Hmem1 cases (mem_dec … block_eq_dec elt2 tl)
705        [ 1: #Hmem2 % #Helt_eq cases Hr #H @H %2 @Hmem2
706        | 2: #Hmem2 @Hind //
707        ]
708   ]
709] qed.
710
711lemma neq_block_eq_block_false : ∀b1,b2:block. b1 ≠ b2 → eq_block b1 b2 = false.
712#b1 #b2 * #Hb
713@(eq_block_elim … b1 b2)
714[ 1: #Habsurd @(False_ind … (Hb Habsurd))
715| 2: // ] qed.
716
717(* --------------------------------------------------------------------------- *)   
718(* Lemmas related to freeing memory and pointer validity. *)
719(* --------------------------------------------------------------------------- *)   
720(*
721lemma nextblock_free_ok : ∀m,b. nextblock m = nextblock (free m b).
722* #contents #next #posnext * #rg #id
723normalize @refl
724qed.
725
726lemma low_bound_free_ok : ∀m,b,ptr.
727   b ≠ (pblock ptr) →
728   Zleb (low_bound (free m b) (pblock ptr)) (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) =
729   Zleb (low_bound m (pblock ptr)) (Z_of_unsigned_bitvector offset_size (offv (poff ptr))).
730* #contents #next #nextpos * #brg #bid * * #prg #pid #poff normalize
731cases prg cases brg normalize nodelta try //
732@(eqZb_elim pid bid)
733[ 1,3: #Heq >Heq * #Habsurd @(False_ind … (Habsurd (refl ??)))
734| 2,4: #_ #_ @refl
735] qed.
736
737lemma high_bound_free_ok : ∀m,b,ptr.
738   b ≠ (pblock ptr) →
739   Zleb (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) (high_bound (free m b) (pblock ptr)) =
740   Zleb (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) (high_bound m (pblock ptr)).
741* #contents #next #nextpos * #brg #bid * * #prg #pid #poff normalize
742cases prg cases brg normalize nodelta try //
743@(eqZb_elim pid bid)
744[ 1,3: #Heq >Heq * #Habsurd @(False_ind … (Habsurd (refl ??)))
745| 2,4: #_ #_ @refl
746] qed.
747
748lemma valid_pointer_free_ok : ∀b : block. ∀m,ptr.
749   valid_pointer m ptr = true →
750   pblock ptr ≠ b →
751   valid_pointer (free m b) ptr = true.
752* #br #bid * #contents #next #posnext * * #pbr #pbid #poff
753normalize
754@(eqZb_elim pbid bid)
755[ 1: #Heqid >Heqid cases pbr cases br normalize
756     [ 1,4: #_ * #Habsurd @(False_ind … (Habsurd (refl ??))) ]
757     cases (Zltb bid next) normalize nodelta
758     [ 2,4: #Habsurd destruct (Habsurd) ]
759     //
760| 2: #Hneqid cases pbr cases br normalize try // ]
761qed.
762
763lemma valid_pointer_free_list_ok : ∀blocks : list block. ∀m,ptr.
764   valid_pointer m ptr = true →
765   ¬ mem ? (pblock ptr) blocks →
766   valid_pointer (free_list m blocks) ptr = true.
767#blocks
768elim blocks
769[ 1: #m #ptr normalize #H #_ @H
770| 2: #b #tl #Hind #m #ptr #Hvalid
771     whd in match (mem block (pblock ptr) ?);
772     >free_list_cons * #Hguard
773     @valid_pointer_free_ok
774     [ 2: % #Heq @Hguard %1 @Heq ]
775     @Hind
776     [ 1: @Hvalid
777     | 2: % #Hmem @Hguard %2 @Hmem ]
778] qed. *)
779
780lemma valid_pointer_ok_free : ∀b : block. ∀m,ptr.
781   valid_pointer m ptr = true →
782   pblock ptr ≠ b →
783   valid_pointer (free m b) ptr = true.
784* #br #bid * #contents #next #posnext * * #pbr #pbid #poff
785normalize
786@(eqZb_elim pbid bid)
787[ 1: #Heqid >Heqid cases pbr cases br normalize
788     [ 1,4: #_ * #Habsurd @(False_ind … (Habsurd (refl ??))) ]
789     cases (Zltb bid next) normalize nodelta
790     [ 2,4: #Habsurd destruct (Habsurd) ]
791     //
792| 2: #Hneqid cases pbr cases br normalize try // ]
793qed.
794
795lemma free_list_cons : ∀m,b,tl. free_list m (b :: tl) = (free (free_list m tl) b).
796#m #b #tl whd in match (free_list ??) in ⊢ (??%%);
797whd in match (free ??); @refl qed.
798
799lemma valid_pointer_free_ok : ∀b : block. ∀m,ptr.
800   valid_pointer (free m b) ptr = true →
801   pblock ptr ≠ b → (* This hypothesis is necessary to handle the cse of "valid" pointers to empty  *)
802   valid_pointer m ptr = true.
803* #br #bid * #contents #next #posnext * * #pbr #pbid #poff
804@(eqZb_elim pbid bid)
805[ 1: #Heqid >Heqid
806     cases pbr cases br normalize
807     [ 1,4: #_ * #Habsurd @(False_ind … (Habsurd (refl ??))) ]
808     cases (Zltb bid next) normalize nodelta
809     [ 2,4: #Habsurd destruct (Habsurd) ]
810     //
811| 2: #Hneqid cases pbr cases br normalize try //
812     >(eqZb_false … Hneqid) normalize nodelta try //
813qed.
814
815lemma valid_pointer_free_list_ok : ∀blocks : list block. ∀m,ptr.
816   valid_pointer (free_list m blocks) ptr = true →
817   ¬ mem ? (pblock ptr) blocks →
818   valid_pointer m ptr = true.
819#blocks
820elim blocks
821[ 1: #m #ptr normalize #H #_ @H
822| 2: #b #tl #Hind #m #ptr #Hvalid
823     whd in match (mem block (pblock ptr) ?);
824     >free_list_cons in Hvalid; #Hvalid * #Hguard
825     lapply (valid_pointer_free_ok … Hvalid) #H
826     @Hind
827     [ 2: % #Heq @Hguard %2 @Heq
828     | 1: @H % #Heq @Hguard %1 @Heq ]
829] qed.
830
831(* An alternative version without the gard on the equality of blocks. *)
832lemma valid_pointer_free_ok_alt : ∀b : block. ∀m,ptr.
833   valid_pointer (free m b) ptr = true →
834   (pblock ptr) = b ∨ (pblock ptr ≠ b ∧ valid_pointer m ptr = true).
835* #br #bid * #contents #next #posnext * * #pbr #pbid #poff
836@(eq_block_elim … (mk_block br bid) (mk_block pbr pbid))
837[ 1: #Heq #_ %1 @(sym_eq … Heq)
838| 2: cases pbr cases br normalize nodelta
839     [ 1,4: @(eqZb_elim pbid bid)
840         [ 1,3: #Heq >Heq * #H @(False_ind … (H (refl ??)))
841         | 2,4: #Hneq #_ normalize >(eqZb_false … Hneq) normalize nodelta
842                 #H %2 @conj try assumption
843                 % #Habsurd destruct (Habsurd) elim Hneq #Hneq @Hneq try @refl
844         ]
845     | *: #_ #H %2 @conj try @H % #Habsurd destruct (Habsurd) ]
846] qed.     
847
848(* Well in fact a valid pointer can be valid even after a free. Ah. *)
849(*
850lemma pointer_in_free_list_not_valid : ∀blocks,m,ptr.
851  mem ? (pblock ptr) blocks →
852  valid_pointer (free_list m blocks) ptr = false.
853*)
854(*
855#blocks elim blocks
856[ 1: #m #ptr normalize #Habsurd @(False_ind … Habsurd)
857| 2: #b #tl #Hind #m #ptr
858     whd in match (mem block (pblock ptr) ?);
859     >free_list_cons
860     *
861     [ 1: #Hptr_match whd in match (free ??);
862          whd in match (update_block ????);
863          whd in match (valid_pointer ??);
864          whd in match (low_bound ??);
865          whd in match (high_bound ??);
866          >Hptr_match >eq_block_identity normalize nodelta
867          whd in match (low ?);
868          cut (Zleb OZ (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) = true)
869          [ 1: elim (offv (poff ptr)) //
870               #n' #hd #tl cases hd normalize
871               [ 1: #_ try @refl
872               | 2: #H @H ] ]
873          #H >H
874          cut (Zleb (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) OZ = false)
875          [ 1: elim (offv (poff ptr)) normalize
876               #n' #hd #tl cases hd normalize
877               [ 1: normalize #_ try @refl
878               | 2: #H @H ] ]
879  valid_pointer (free_list m blocks) ptr = false.
880*)
881
882
883(* --------------------------------------------------------------------------- *)   
884(* Memory injections *)
885(* --------------------------------------------------------------------------- *)   
886
887(* An embedding is a function from blocks to (blocks × offset). *)
888definition embedding ≝ block → option (block × offset).
889
890definition offset_plus : offset → offset → offset ≝
891  λo1,o2. mk_offset (addition_n ? (offv o1) (offv o2)).
892
893lemma offset_plus_0 : ∀o. offset_plus o (mk_offset (zero ?)) = o.
894* #o
895whd in match (offset_plus ??);
896>addition_n_0 @refl
897qed.
898
899(* Translates a pointer through an embedding. *)
900definition pointer_translation : ∀p:pointer. ∀E:embedding. option pointer ≝
901λp,E.
902match p with
903[ mk_pointer pblock poff ⇒
904   match E pblock with
905   [ None ⇒ None ?
906   | Some loc ⇒
907    let 〈dest_block,dest_off〉 ≝ loc in
908    let ptr ≝ (mk_pointer dest_block (offset_plus poff dest_off)) in
909    Some ? ptr
910   ]
911].
912
913(* We parameterise the "equivalence" relation on values with an embedding. *)
914(* Front-end values. *)
915inductive value_eq (E : embedding) : val → val → Prop ≝
916| undef_eq : ∀v.
917  value_eq E Vundef v
918| vint_eq : ∀sz,i.
919  value_eq E (Vint sz i) (Vint sz i)
920| vfloat_eq : ∀f.
921  value_eq E (Vfloat f) (Vfloat f)
922| vnull_eq :
923  value_eq E Vnull Vnull
924| vptr_eq : ∀p1,p2.
925  pointer_translation p1 E = Some ? p2 →
926  value_eq E (Vptr p1) (Vptr p2).
927 
928(* [load_sim] states the fact that each successful load in [m1] is matched by a load in [m2] s.t.
929 * the values are equivalent. *)
930definition load_sim ≝
931λ(E : embedding).λ(m1 : mem).λ(m2 : mem).
932 ∀b1,off1,b2,off2,ty,v1.
933  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 *)
934  E b1 = Some ? 〈b2,off2〉 →
935  load_value_of_type ty m1 b1 off1 = Some ? v1 →
936  (∃v2. load_value_of_type ty m2 b2 (offset_plus off1 off2) = Some ? v2 ∧ value_eq E v1 v2).
937 
938definition load_sim_ptr ≝
939λ(E : embedding).λ(m1 : mem).λ(m2 : mem).
940 ∀b1,off1,b2,off2,ty,v1.
941  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 *)
942  pointer_translation (mk_pointer b1 off1) E = Some ? (mk_pointer b2 off2) →
943  load_value_of_type ty m1 b1 off1 = Some ? v1 →
944  (∃v2. load_value_of_type ty m2 b2 off2 = Some ? v2 ∧ value_eq E v1 v2).
945
946(* Definition of a memory injection *)
947record memory_inj (E : embedding) (m1 : mem) (m2 : mem) : Type[0] ≝
948{ (* Load simulation *)
949  mi_inj : load_sim_ptr E m1 m2;
950  (* Invalid blocks are not mapped *)
951  mi_freeblock : ∀b. ¬ (valid_block m1 b) → E b = None ?;
952  (* Valid pointers are mapped to valid pointers*)
953  mi_valid_pointers : ∀p,p'.
954                       valid_pointer m1 p = true →
955                       pointer_translation p E = Some ? p' →
956                       valid_pointer m2 p' = true;
957  (* Blocks in the codomain are valid *)
958  (* mi_incl : ∀b,b',o'. E b = Some ? 〈b',o'〉 → valid_block m2 b'; *)
959  (* Regions are preserved *)
960  mi_region : ∀b,b',o'. E b = Some ? 〈b',o'〉 → block_region b = block_region b';
961  (* Disjoint blocks are mapped to disjoint blocks. Note that our condition is stronger than compcert's.
962   * This may cause some problems if we reuse this def for the translation from Clight to Cminor, where
963   * all variables are allocated in the same block. *)
964  mi_disjoint : ∀b1,b2,b1',b2',o1',o2'.
965                b1 ≠ b2 →
966                E b1 = Some ? 〈b1',o1'〉 →
967                E b2 = Some ? 〈b2',o2'〉 →
968                b1' ≠ b2'
969}.
970
971(* Definition of a memory extension. /!\ Not equivalent to the compcert concept. /!\
972 * A memory extension is a [memory_inj] with some particular blocks designated as
973 * being writeable. *)
974
975alias id "meml" = "cic:/matita/basics/lists/list/mem.fix(0,2,1)".
976
977record memory_ext (E : embedding) (m1 : mem) (m2 : mem) : Type[0] ≝
978{ me_inj : memory_inj E m1 m2;
979  (* A list of blocks where we can write freely *)
980  me_writeable : list block;
981  (* These blocks are valid *)
982  me_writeable_valid : ∀b. meml ? b me_writeable → valid_block m2 b;
983  (* And pointers to m1 are oblivious to these blocks *)
984  me_writeable_ok : ∀p,p'.
985                     valid_pointer m1 p = true →
986                     pointer_translation p E = Some ? p' →
987                     ¬ (meml ? (pblock p') me_writeable)
988}.
989
990(* ---------------------------------------------------------------------------- *)
991(* End of the definitions on memory injections. Now, on to proving some lemmas. *)
992
993(* A particular inversion. *)
994lemma value_eq_ptr_inversion :
995  ∀E,p1,v. value_eq E (Vptr p1) v → ∃p2. v = Vptr p2 ∧ pointer_translation p1 E = Some ? p2.
996#E #p1 #v #Heq inversion Heq
997[ 1: #v #Habsurd destruct (Habsurd)
998| 2: #sz #i #Habsurd destruct (Habsurd)
999| 3: #f #Habsurd destruct (Habsurd)
1000| 4:  #Habsurd destruct (Habsurd)
1001| 5: #p1' #p2 #Heq #Heqv #Heqv2 #_ destruct
1002     %{p2} @conj try @refl try assumption
1003] qed.
1004
1005(* A cleaner version of inversion for [value_eq] *)
1006lemma value_eq_inversion :
1007  ∀E,v1,v2. ∀P : val → val → Prop. value_eq E v1 v2 →
1008  (∀v. P Vundef v) →
1009  (∀sz,i. P (Vint sz i) (Vint sz i)) →
1010  (∀f. P (Vfloat f) (Vfloat f)) →
1011  (P Vnull Vnull) →
1012  (∀p1,p2. pointer_translation p1 E = Some ? p2 → P (Vptr p1) (Vptr p2)) →
1013  P v1 v2.
1014#E #v1 #v2 #P #Heq #H1 #H2 #H3 #H4 #H5
1015inversion Heq
1016[ 1: #v #Hv1 #Hv2 #_ destruct @H1
1017| 2: #sz #i #Hv1 #Hv2 #_ destruct @H2
1018| 3: #f #Hv1 #Hv2 #_ destruct @H3
1019| 4: #Hv1 #Hv2 #_ destruct @H4
1020| 5: #p1 #p2 #Hembed #Hv1 #Hv2 #_ destruct @H5 // ] qed.
1021 
1022(* If we succeed to load something by value from a 〈b,off〉 location,
1023   [b] is a valid block. *)
1024lemma load_by_value_success_valid_block_aux :
1025  ∀ty,m,b,off,v.
1026    access_mode ty = By_value (typ_of_type ty) →
1027    load_value_of_type ty m b off = Some ? v →
1028    Zltb (block_id b) (nextblock m) = true.
1029#ty #m * #brg #bid #off #v
1030cases ty
1031[ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
1032| 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
1033whd in match (load_value_of_type ????);
1034[ 1,7,8: #_ #Habsurd destruct (Habsurd) ]
1035#Hmode
1036[ 1,2,3,6: [ 1: elim sz | 2: elim fsz ]
1037     normalize in match (typesize ?);
1038     whd in match (loadn ???);
1039     whd in match (beloadv ??);
1040     cases (Zltb bid (nextblock m)) normalize nodelta
1041     try // #Habsurd destruct (Habsurd)
1042| *: normalize in Hmode; destruct (Hmode)
1043] qed.
1044
1045(* If we succeed in loading some data from a location, then this loc is a valid pointer. *)
1046lemma load_by_value_success_valid_ptr_aux :
1047  ∀ty,m,b,off,v.
1048    access_mode ty = By_value (typ_of_type ty) →
1049    load_value_of_type ty m b off = Some ? v →
1050    Zltb (block_id b) (nextblock m) = true ∧
1051    Zleb (low_bound m b) (Z_of_unsigned_bitvector ? (offv off)) = true ∧
1052    Zltb (Z_of_unsigned_bitvector ? (offv off)) (high_bound m b) = true.
1053#ty #m * #brg #bid #off #v
1054cases ty
1055[ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
1056| 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
1057whd in match (load_value_of_type ????);
1058[ 1,7,8: #_ #Habsurd destruct (Habsurd) ]
1059#Hmode
1060[ 1,2,3,6: [ 1: elim sz | 2: elim fsz ]
1061     normalize in match (typesize ?);
1062     whd in match (loadn ???);
1063     whd in match (beloadv ??);
1064     cases (Zltb bid (nextblock m)) normalize nodelta
1065     cases (Zleb (low (blocks m (mk_block brg bid)))
1066                  (Z_of_unsigned_bitvector offset_size (offv off)))
1067     cases (Zltb (Z_of_unsigned_bitvector offset_size (offv off)) (high (blocks m (mk_block brg bid))))
1068     normalize nodelta
1069     #Heq destruct (Heq)
1070     try /3 by conj, refl/
1071| *: normalize in Hmode; destruct (Hmode)
1072] qed.
1073
1074
1075lemma valid_block_from_bool : ∀b,m. Zltb (block_id b) (nextblock m) = true → valid_block m b.
1076* #rg #id #m normalize
1077elim id /2/ qed.
1078
1079lemma valid_block_to_bool : ∀b,m. valid_block m b → Zltb (block_id b) (nextblock m) = true.
1080* #rg #id #m normalize
1081elim id /2/ qed.
1082
1083lemma load_by_value_success_valid_block :
1084  ∀ty,m,b,off,v.
1085    access_mode ty = By_value (typ_of_type ty) →
1086    load_value_of_type ty m b off = Some ? v →
1087    valid_block m b.
1088#ty #m #b #off #v #Haccess_mode #Hload
1089@valid_block_from_bool
1090elim (load_by_value_success_valid_ptr_aux ty m b off v Haccess_mode Hload) * //
1091qed.
1092
1093lemma load_by_value_success_valid_pointer :
1094  ∀ty,m,b,off,v.
1095    access_mode ty = By_value (typ_of_type ty) →
1096    load_value_of_type ty m b off = Some ? v →
1097    valid_pointer m (mk_pointer b off).
1098#ty #m #b #off #v #Haccess_mode #Hload normalize
1099elim (load_by_value_success_valid_ptr_aux ty m b off v Haccess_mode Hload)
1100* #H1 #H2 #H3 >H1 >H2 normalize nodelta >H3 @I
1101qed.
1102
1103(* Making explicit the contents of memory_inj for load_value_of_type *)
1104lemma load_value_of_type_inj : ∀E,m1,m2,b1,off1,v1,b2,off2,ty.
1105    memory_inj E m1 m2 →
1106    value_eq E (Vptr (mk_pointer b1 off1)) (Vptr (mk_pointer b2 off2)) →
1107    load_value_of_type ty m1 b1 off1 = Some ? v1 →
1108    ∃v2. load_value_of_type ty m2 b2 off2 = Some ? v2 ∧ value_eq E v1 v2.
1109#E #m1 #m2 #b1 #off1 #v1 #b2 #off2 #ty #Hinj #Hvalue_eq
1110lapply (value_eq_ptr_inversion … Hvalue_eq) * #p2 * #Hp2_eq #Hembed destruct
1111lapply (refl ? (access_mode ty))
1112cases ty
1113[ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
1114| 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
1115normalize in ⊢ ((???%) → ?); #Hmode #Hyp
1116[ 1,7,8: normalize in Hyp; destruct (Hyp)
1117| 5,6: normalize in Hyp ⊢ %; destruct (Hyp) /3 by ex_intro, conj, vptr_eq/ ]
1118lapply (load_by_value_success_valid_pointer … Hmode … Hyp) #Hvalid_pointer
1119lapply (mi_inj … Hinj b1 off1 b2 off2 … Hvalid_pointer Hembed Hyp) #H @H
1120qed.     
1121
1122(* -------------------------------------- *)
1123(* Lemmas pertaining to memory allocation *)
1124
1125(* A valid block stays valid after an alloc. *)
1126lemma alloc_valid_block_conservation :
1127  ∀m,m',z1,z2,r,new_block.
1128  alloc m z1 z2 r = 〈m', new_block〉 →
1129  ∀b. valid_block m b → valid_block m' b.
1130#m #m' #z1 #z2 #r * #b' #Hregion_eq
1131elim m #contents #nextblock #Hcorrect whd in match (alloc ????);
1132#Halloc destruct (Halloc)
1133#b whd in match (valid_block ??) in ⊢ (% → %); /2/
1134qed.
1135
1136(* Allocating a new zone produces a valid block. *)
1137lemma alloc_valid_new_block :
1138  ∀m,m',z1,z2,r,new_block.
1139  alloc m z1 z2 r = 〈m', new_block〉 →
1140  valid_block m' new_block.
1141* #contents #nextblock #Hcorrect #m' #z1 #z2 #r * #new_block #Hregion_eq
1142whd in match (alloc ????); whd in match (valid_block ??);
1143#Halloc destruct (Halloc) /2/
1144qed.
1145
1146(* All data in a valid block is unchanged after an alloc. *)
1147lemma alloc_beloadv_conservation :
1148  ∀m,m',block,offset,z1,z2,r,new_block.
1149    valid_block m block →
1150    alloc m z1 z2 r = 〈m', new_block〉 →
1151    beloadv m (mk_pointer block offset) = beloadv m' (mk_pointer block offset).
1152* #contents #next #Hcorrect #m' #block #offset #z1 #z2 #r #new_block #Hvalid #Halloc
1153whd in Halloc:(??%?); destruct (Halloc)
1154whd in match (beloadv ??) in ⊢ (??%%);
1155lapply (valid_block_to_bool … Hvalid) #Hlt
1156>Hlt >(zlt_succ … Hlt)
1157normalize nodelta whd in match (update_block ?????); whd in match (eq_block ??);
1158cut (eqZb (block_id block) next = false)
1159[ lapply (Zltb_true_to_Zlt … Hlt) #Hlt' @eqZb_false /2/ ] #Hneq
1160>Hneq cases (eq_region ??) normalize nodelta  @refl
1161qed.
1162
1163(* Lift [alloc_beloadv_conservation] to loadn *)
1164lemma alloc_loadn_conservation :
1165  ∀m,m',z1,z2,r,new_block.
1166    alloc m z1 z2 r = 〈m', new_block〉 →
1167    ∀n. ∀block,offset.
1168    valid_block m block →
1169    loadn m (mk_pointer block offset) n = loadn m' (mk_pointer block offset) n.
1170#m #m' #z1 #z2 #r #new_block #Halloc #n
1171elim n try //
1172#n' #Hind #block #offset #Hvalid_block
1173whd in ⊢ (??%%);
1174>(alloc_beloadv_conservation … Hvalid_block Halloc)
1175cases (beloadv m' (mk_pointer block offset)) //
1176#bev normalize nodelta
1177whd in match (shift_pointer ???); >Hind try //
1178qed.
1179
1180(* Memory allocation preserves [memory_inj] *)
1181lemma alloc_memory_inj :
1182  ∀E:embedding.∀m1,m2,m2',z1,z2,r,new_block. ∀H:memory_inj E m1 m2.
1183  alloc m2 z1 z2 r = 〈m2', new_block〉 →
1184  memory_inj E m1 m2'.
1185#E #m1 #m2 #m2' #z1 #z2 #r * #new_block #Hregion #Hmemory_inj #Halloc
1186%
1187[ 1:
1188  whd
1189  #b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Hembed #Hload
1190  elim (mi_inj E m1 m2 Hmemory_inj b1 off1 b2 off2 … ty v1 Hvalid Hembed Hload)
1191  #v2 * #Hload_eq #Hvalue_eq %{v2} @conj try //
1192  lapply (refl ? (access_mode ty))
1193  cases ty in Hload_eq;
1194  [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
1195  | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
1196  #Hload normalize in ⊢ ((???%) → ?); #Haccess
1197  [ 1,7,8: normalize in Hload; destruct (Hload)
1198  | 2,3,4,9: whd in match (load_value_of_type ????);
1199     whd in match (load_value_of_type ????);
1200     lapply (load_by_value_success_valid_block … Haccess Hload)
1201     #Hvalid_block
1202     whd in match (load_value_of_type ????) in Hload;
1203     <(alloc_loadn_conservation … Halloc … Hvalid_block)
1204     @Hload
1205  | 5,6: whd in match (load_value_of_type ????) in Hload ⊢ %; @Hload ]
1206| 2: @(mi_freeblock … Hmemory_inj)
1207| 3: #p #p' #Hvalid #Hptr_trans lapply (mi_valid_pointers … Hmemory_inj p p' Hvalid Hptr_trans)
1208     elim m2 in Halloc; #contentmap #nextblock #Hnextblock
1209     elim p' * #br' #bid' #o' #Halloc whd in Halloc:(??%?) ⊢ ?; destruct (Halloc)
1210     whd in match (valid_pointer ??) in ⊢ (% → %);
1211     @Zltb_elim_Type0
1212     [ 2: normalize #_ #Habsurd destruct (Habsurd) ]
1213     #Hbid' cut (Zltb bid' (Zsucc nextblock) = true) [ lapply (Zlt_to_Zltb_true … Hbid') @zlt_succ ]
1214     #Hbid_succ >Hbid_succ whd in match (low_bound ??) in ⊢ (% → %);
1215     whd in match (high_bound ??) in ⊢ (% → %);
1216     whd in match (update_block ?????);
1217     whd in match (eq_block ??);
1218     cut (eqZb bid' nextblock = false) [ 1: @eqZb_false /2 by not_to_not/ ]
1219     #Hbid_neq >Hbid_neq
1220     cases (eq_region br' r) normalize #H @H
1221| 4: @(mi_region … Hmemory_inj)
1222| 5: @(mi_disjoint … Hmemory_inj)
1223] qed.
1224
1225(* Memory allocation induces a memory extension. *)
1226lemma alloc_memory_ext :
1227  ∀E:embedding.∀m1,m2,m2',z1,z2,r,new_block. ∀H:memory_inj E m1 m2.
1228  alloc m2 z1 z2 r = 〈m2', new_block〉 →
1229  memory_ext E m1 m2'.
1230#E #m1 #m2 #m2' #z1 #z2 #r * #new_block #Hblock_region_eq #Hmemory_inj #Halloc
1231lapply (alloc_memory_inj … Hmemory_inj Halloc)
1232#Hinj' %
1233[ 1: @Hinj'
1234| 2: @[new_block]
1235| 3: #b normalize in ⊢ (%→ ?); * [ 2: #H @(False_ind … H) ]
1236      #Heq destruct (Heq) whd elim m2 in Halloc;
1237      #Hcontents #nextblock #Hnextblock
1238      whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
1239      /2/
1240| 4: * #b #o * #b' #o' #Hvalid_ptr #Hembed %
1241     normalize in ⊢ (% → ?); * [ 2: #H @H ]
1242     #Heq destruct (Heq)
1243     lapply (mi_valid_pointers … Hmemory_inj … Hvalid_ptr Hembed)
1244     whd in ⊢ (% → ?);
1245     (* contradiction because ¬ (valid_block m2 new_block)  *)
1246     elim m2 in Halloc;
1247     #contents_m2 #nextblock_m2 #Hnextblock_m2
1248     whd in ⊢ ((??%?) → ?);
1249     #Heq_alloc destruct (Heq_alloc)
1250     normalize
1251     lapply (irreflexive_Zlt nextblock_m2)
1252     @Zltb_elim_Type0
1253     [ #H * #Habsurd @(False_ind … (Habsurd H)) ] #_ #_ normalize #Habsurd destruct (Habsurd)
1254] qed.
1255
1256lemma bestorev_beloadv_conservation :
1257  ∀mA,mB,wb,wo,v.
1258    bestorev mA (mk_pointer wb wo) v = Some ? mB →
1259    ∀rb,ro. eq_block wb rb = false →
1260    beloadv mA (mk_pointer rb ro) = beloadv mB (mk_pointer rb ro).
1261#mA #mB #wb #wo #v #Hstore #rb #ro #Hblock_neq
1262whd in ⊢ (??%%);
1263elim mB in Hstore; #contentsB #nextblockB #HnextblockB
1264normalize in ⊢ (% → ?);
1265cases (Zltb (block_id wb) (nextblock mA)) normalize nodelta
1266[ 2: #Habsurd destruct (Habsurd) ]
1267cases (if Zleb (low (blocks mA wb)) (Z_of_unsigned_bitvector 16 (offv wo))
1268       then Zltb (Z_of_unsigned_bitvector 16 (offv wo)) (high (blocks mA wb)) 
1269       else false) normalize nodelta
1270[ 2: #Habsurd destruct (Habsurd) ]
1271#Heq destruct (Heq) elim rb in Hblock_neq; #rr #rid elim wb #wr #wid
1272cases rr cases wr normalize try //
1273@(eqZb_elim … rid wid)
1274[ 1,3: #Heq destruct (Heq) >(eqZb_reflexive wid) #Habsurd destruct (Habsurd) ]
1275try //
1276qed.
1277
1278(* lift [bestorev_beloadv_conservation to [loadn] *)
1279lemma bestorev_loadn_conservation :
1280  ∀mA,mB,n,wb,wo,v.
1281    bestorev mA (mk_pointer wb wo) v = Some ? mB →
1282    ∀rb,ro. eq_block wb rb = false →
1283    loadn mA (mk_pointer rb ro) n = loadn mB (mk_pointer rb ro) n.
1284#mA #mB #n
1285elim n
1286[ 1: #wb #wo #v #Hstore #rb #ro #Hblock_neq normalize @refl
1287| 2: #n' #Hind #wb #wo #v #Hstore #rb #ro #Hneq
1288     whd in ⊢ (??%%);
1289     >(bestorev_beloadv_conservation … Hstore … Hneq)
1290     >(Hind … Hstore … Hneq) @refl
1291] qed.
1292
1293(* lift [bestorev_loadn_conservation] to [load_value_of_type] *)
1294lemma bestorev_load_value_of_type_conservation :
1295  ∀mA,mB,wb,wo,v.
1296    bestorev mA (mk_pointer wb wo) v = Some ? mB →
1297    ∀rb,ro. eq_block wb rb = false →
1298    ∀ty.load_value_of_type ty mA rb ro = load_value_of_type ty mB rb ro.
1299#mA #mB #wb #wo #v #Hstore #rb #ro #Hneq #ty
1300cases ty
1301[ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
1302| 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ] try //
1303[ 1: elim sz | 2: elim fsz | 3: | 4: ]
1304whd in ⊢ (??%%);
1305>(bestorev_loadn_conservation … Hstore … Hneq) @refl
1306qed.
1307
1308(* Writing in the "extended" part of a memory preserves the underlying injection *)
1309lemma bestorev_memory_ext_to_load_sim :
1310  ∀E,mA,mB,mC.
1311  ∀Hext:memory_ext E mA mB.
1312  ∀wb,wo,v. meml ? wb (me_writeable … Hext) →
1313  bestorev mB (mk_pointer wb wo) v = Some ? mC →
1314  load_sim_ptr E mA mC.
1315#E #mA #mB #mC #Hext #wb #wo #v #Hwb #Hstore whd
1316#b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Hembed #Hload
1317(* Show that (wb ≠ b2) by showing b2 ∉ (me_writeable ...) *)
1318lapply (me_writeable_ok … Hext (mk_pointer b1 off1) (mk_pointer b2 off2) Hvalid Hembed) #Hb2
1319lapply (mem_not_mem_neq … Hwb Hb2) #Hwb_neq_b2
1320cut ((eq_block wb b2) = false) [ @neq_block_eq_block_false @Hwb_neq_b2 ] #Heq_block_false
1321<(bestorev_load_value_of_type_conservation … Hstore … Heq_block_false)
1322@(mi_inj … (me_inj … Hext) … Hvalid  … Hembed …  Hload)
1323qed.
1324
1325(* Writing in the "extended" part of a memory preserves the whole memory injection *)
1326lemma bestorev_memory_ext_to_memory_inj :
1327  ∀E,mA,mB,mC.
1328  ∀Hext:memory_ext E mA mB.
1329  ∀wb,wo,v. meml ? wb (me_writeable … Hext) →
1330  bestorev mB (mk_pointer wb wo) v = Some ? mC →
1331  memory_inj E mA mC.
1332#E #mA * #contentsB #nextblockB #HnextblockB #mC
1333#Hext #wb #wo #v #Hwb #Hstore
1334%
1335[ 1: @(bestorev_memory_ext_to_load_sim … Hext … Hwb Hstore) ]
1336elim Hext in Hwb; * #Hinj #Hvalid #Hcodomain #Hregion #Hdisjoint #writeable #Hwriteable_valid #Hwriteable_ok
1337#Hmem
1338[ 1: @Hvalid | 3: @Hregion | 4: @Hdisjoint ] -Hvalid -Hregion -Hdisjoint
1339whd in Hstore:(??%?); lapply (Hwriteable_valid … Hmem)
1340normalize in ⊢ (% → ?); #Hlt_wb
1341#p #p' #HvalidA #Hembed lapply (Hcodomain … HvalidA Hembed) -Hcodomain
1342normalize in match (valid_pointer ??) in ⊢ (% → %);
1343>(Zlt_to_Zltb_true … Hlt_wb) in Hstore; normalize nodelta
1344cases (Zleb (low (contentsB wb)) (Z_of_unsigned_bitvector offset_size (offv wo))
1345       ∧Zltb (Z_of_unsigned_bitvector offset_size (offv wo)) (high (contentsB wb)))
1346normalize nodelta
1347[ 2: #Habsurd destruct (Habsurd) ]
1348#Heq destruct (Heq)
1349cases (Zltb (block_id (pblock p')) nextblockB) normalize nodelta
1350[ 2: #H @H ]
1351whd in match (update_block ?????);
1352cut (eq_block (pblock p') wb = false)
1353[ 2: #Heq >Heq normalize nodelta #H @H ]
1354@neq_block_eq_block_false @sym_neq
1355@(mem_not_mem_neq writeable … Hmem)
1356@(Hwriteable_ok … HvalidA Hembed)
1357qed.
1358
1359(* It even preserves memory extensions, with the same writeable blocks.  *)
1360lemma bestorev_memory_ext_to_memory_ext :
1361  ∀E,mA,mB.
1362  ∀Hext:memory_ext E mA mB.
1363  ∀wb,wo,v. meml ? wb (me_writeable … Hext) →
1364  ∀mC.bestorev mB (mk_pointer wb wo) v = Some ? mC →
1365  ΣExt:memory_ext E mA mC.(me_writeable … Hext = me_writeable … Ext).
1366#E #mA #mB #Hext #wb #wo #v #Hmem #mC #Hstore
1367%{(mk_memory_ext …
1368      (bestorev_memory_ext_to_memory_inj … Hext … Hmem … Hstore)
1369      (me_writeable … Hext)
1370      ?
1371      (me_writeable_ok … Hext)
1372 )} try @refl
1373#b #Hmemb
1374lapply (me_writeable_valid … Hext b Hmemb)
1375lapply (me_writeable_valid … Hext wb Hmem)
1376elim mB in Hstore; #contentsB #nextblockB #HnextblockB #Hstore #Hwb_valid #Hb_valid
1377lapply Hstore normalize in Hwb_valid Hb_valid ⊢ (% → ?);
1378>(Zlt_to_Zltb_true … Hwb_valid) normalize nodelta
1379cases (if Zleb (low (contentsB wb)) (Z_of_unsigned_bitvector 16 (offv wo))
1380       then Zltb (Z_of_unsigned_bitvector 16 (offv wo)) (high (contentsB wb)) 
1381       else false)
1382normalize [ 2: #Habsurd destruct (Habsurd) ]
1383#Heq destruct (Heq) @Hb_valid
1384qed.
1385
1386(* Lift [bestorev_memory_ext_to_memory_ext] to storen *)
1387lemma storen_memory_ext_to_memory_ext :
1388  ∀E,mA,l,mB,mC.
1389  ∀Hext:memory_ext E mA mB.
1390  ∀wb,wo. meml ? wb (me_writeable … Hext) →
1391  storen mB (mk_pointer wb wo) l = Some ? mC →
1392  memory_ext E mA mC.
1393#E #mA #l elim l
1394[ 1: #mB #mC #Hext #wb #wo #Hmem normalize in ⊢ (% → ?); #Heq destruct (Heq)
1395     @Hext
1396| 2: #hd #tl #Hind #mB #mC #Hext #wb #wo #Hmem
1397     whd in ⊢ ((??%?) → ?);
1398     lapply (bestorev_memory_ext_to_memory_ext … Hext … wb wo hd Hmem)
1399     cases (bestorev mB (mk_pointer wb wo) hd)
1400     normalize nodelta
1401     [ 1: #H #Habsurd destruct (Habsurd) ]
1402     #mD #H lapply (H mD (refl ??)) * #HextD #Heq #Hstore
1403     @(Hind … HextD … Hstore)
1404     <Heq @Hmem
1405] qed.     
1406
1407(* Lift [storen_memory_ext_to_memory_ext] to store_value_of_type *)
1408lemma store_value_of_type_memory_ext_to_memory_ext :
1409  ∀E,mA,mB,mC.
1410  ∀Hext:memory_ext E mA mB.
1411  ∀wb,wo. meml ? wb (me_writeable … Hext) →
1412  ∀ty,v.store_value_of_type ty mB wb wo v = Some ? mC →
1413  memory_ext E mA mC.
1414#E #mA #mB #mC #Hext #wb #wo #Hmem #ty #v
1415cases ty
1416[ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
1417| 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
1418whd in ⊢ ((??%?) → ?);
1419[ 1,5,6,7,8: #Habsurd destruct (Habsurd) ]
1420#Hstore
1421@(storen_memory_ext_to_memory_ext … Hext … Hmem … Hstore)
1422qed.
1423
1424(* Commutation results of standard binary operations with value_eq. *)
1425lemma unary_operation_value_eq :
1426  ∀E,op,v1,v2,ty.
1427   value_eq E v1 v2 →
1428   ∀r1.
1429   sem_unary_operation op v1 ty = Some ? r1 →
1430    ∃r2.sem_unary_operation op v2 ty = Some ? r2 ∧ value_eq E r1 r2.
1431#E #op #v1 #v2 #ty #Hvalue_eq #r1
1432inversion Hvalue_eq
1433[ 1: #v #Hv1 #Hv2 #_ destruct
1434     cases op normalize
1435     [ 1: cases ty [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
1436          normalize #Habsurd destruct (Habsurd)
1437     | 3: cases ty [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
1438          normalize #Habsurd destruct (Habsurd)
1439     | 2: #Habsurd destruct (Habsurd) ]
1440| 2: #vsz #i #Hv1 #Hv2 #_
1441     cases op
1442     [ 1: cases ty
1443          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
1444          whd in ⊢ ((??%?) → ?); whd in match (sem_unary_operation ???);
1445          [ 2: cases (eq_intsize sz vsz) normalize nodelta #Heq1 destruct
1446               %{(of_bool (eq_bv (bitsize_of_intsize vsz) i (zero (bitsize_of_intsize vsz))))}
1447               cases (eq_bv (bitsize_of_intsize vsz) i (zero (bitsize_of_intsize vsz))) @conj
1448               //
1449          | *: #Habsurd destruct (Habsurd) ]
1450     | 2: whd in match (sem_unary_operation ???);     
1451          #Heq1 destruct %{(Vint vsz (exclusive_disjunction_bv (bitsize_of_intsize vsz) i (mone vsz)))} @conj //
1452     | 3: whd in match (sem_unary_operation ???);
1453          cases ty
1454          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
1455          normalize nodelta
1456          whd in ⊢ ((??%?) → ?);
1457          [ 2: cases (eq_intsize sz vsz) normalize nodelta #Heq1 destruct
1458               %{(Vint vsz (two_complement_negation (bitsize_of_intsize vsz) i))} @conj //
1459          | *: #Habsurd destruct (Habsurd) ] ]
1460| 3: #f #Hv1 #Hv2 #_ destruct  whd in match (sem_unary_operation ???);
1461     cases op normalize nodelta
1462     [ 1: cases ty
1463          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
1464          whd in match (sem_notbool ??);
1465          #Heq1 destruct
1466          cases (Fcmp Ceq f Fzero) /3 by ex_intro, vint_eq, conj/
1467     | 2: normalize #Habsurd destruct (Habsurd)
1468     | 3: cases ty
1469          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
1470          whd in match (sem_neg ??);
1471          #Heq1 destruct /3 by ex_intro, vfloat_eq, conj/ ]
1472| 4: #Hv1 #Hv2 #_ destruct  whd in match (sem_unary_operation ???);
1473     cases op normalize nodelta
1474     [ 1: cases ty
1475          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
1476          whd in match (sem_notbool ??);
1477          #Heq1 destruct /3 by ex_intro, vint_eq, conj/
1478     | 2: normalize #Habsurd destruct (Habsurd)
1479     | 3: cases ty
1480          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
1481          whd in match (sem_neg ??);
1482          #Heq1 destruct ]
1483| 5: #p1 #p2 #Hptr_translation #Hv1 #Hv2 #_  whd in match (sem_unary_operation ???);
1484     cases op normalize nodelta
1485     [ 1: cases ty
1486          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
1487          whd in match (sem_notbool ??);         
1488          #Heq1 destruct /3 by ex_intro, vint_eq, conj/
1489     | 2: normalize #Habsurd destruct (Habsurd)
1490     | 3: cases ty
1491          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
1492          whd in match (sem_neg ??);         
1493          #Heq1 destruct ]
1494]
1495qed.
1496
1497(* value_eq lifts to addition *)
1498lemma add_value_eq :
1499  ∀E,v1,v2,v1',v2',ty1,ty2.
1500   value_eq E v1 v2 →
1501   value_eq E v1' v2' →
1502   (* memory_inj E m1 m2 →  This injection seems useless TODO *)
1503   ∀r1. (sem_add v1 ty1 v1' ty2=Some val r1→
1504           ∃r2:val.sem_add v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2).
1505#E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1
1506@(value_eq_inversion E … Hvalue_eq1)
1507[ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ]
1508[ 1: whd in match (sem_add ????); normalize nodelta
1509     cases (classify_add ty1 ty2) normalize nodelta
1510     [ 1: #sz #sg | 2: #fsz | 3: #n #ty #sz #sg | 4: #n #sz #sg #ty | 5: #ty1' #ty2' ]
1511     #Habsurd destruct (Habsurd)
1512| 2: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
1513     cases (classify_add ty1 ty2) normalize nodelta     
1514     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
1515     [ 2,3,5: #Habsurd destruct (Habsurd) ]
1516     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
1517     [ 1,6: #v' | 2,7: #sz' #i' | 3,8: #f' | 4,9: | 5,10: #p1' #p2' #Hembed' ]
1518     [ 1,2,4,5,6,7,9: #Habsurd destruct (Habsurd) ]
1519     [ 1: @intsize_eq_elim_elim
1520          [ 1: #_ #Habsurd destruct (Habsurd)
1521          | 2: #Heq destruct (Heq) normalize nodelta
1522               #Heq destruct (Heq)
1523               /3 by ex_intro, conj, vint_eq/ ]
1524     | 2: @eq_bv_elim normalize nodelta #Heq1 #Heq2 destruct
1525          /3 by ex_intro, conj, vint_eq/
1526     | 3: #Heq destruct (Heq)
1527          normalize in Hembed'; elim p1' in Hembed'; #b1' #o1' normalize nodelta #Hembed
1528          %{(Vptr (shift_pointer_n (bitsize_of_intsize sz) p2' (sizeof ty) i))} @conj try @refl
1529          @vptr_eq whd in match (pointer_translation ??);
1530          cases (E b1') in Hembed;
1531          [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
1532          | 2: * #block #offset normalize nodelta #Heq destruct (Heq)
1533               whd in match (shift_pointer_n ????);
1534               cut (offset_plus (shift_offset_n (bitsize_of_intsize sz) o1' (sizeof ty) i) offset =
1535                    (shift_offset_n (bitsize_of_intsize sz) (mk_offset (addition_n ? (offv o1') (offv offset))) (sizeof ty) i))
1536               [ 1: whd in match (offset_plus ??);
1537                    whd in match (shift_offset_n ????) in ⊢ (??%%);
1538                    >commutative_addition_n >associative_addition_n
1539                    <(commutative_addition_n … (offv offset) (offv o1')) @refl ]
1540               #Heq >Heq @refl ]
1541     ]
1542| 3: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
1543     cases (classify_add ty1 ty2) normalize nodelta     
1544     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
1545     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
1546     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
1547     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
1548     [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
1549     #Heq destruct (Heq)
1550     /3 by ex_intro, conj, vfloat_eq/
1551| 4: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
1552     cases (classify_add ty1 ty2) normalize nodelta     
1553     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
1554     [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
1555     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
1556     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
1557     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
1558     @eq_bv_elim
1559     [ 1: normalize nodelta #Heq1 #Heq2 destruct /3 by ex_intro, conj, vnull_eq/
1560     | 2: #_ normalize nodelta #Habsurd destruct (Habsurd) ]
1561| 5: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
1562     cases (classify_add ty1 ty2) normalize nodelta
1563     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
1564     [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
1565     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
1566     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
1567     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
1568     #Heq destruct (Heq)
1569     %{(Vptr (shift_pointer_n (bitsize_of_intsize sz') p2 (sizeof ty) i'))} @conj try @refl
1570     @vptr_eq whd in match (pointer_translation ??) in Hembed ⊢ %;
1571     elim p1 in Hembed; #b1 #o1 normalize nodelta
1572     cases (E b1)
1573     [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
1574     | 2: * #block #offset normalize nodelta #Heq destruct (Heq)
1575          whd in match (shift_pointer_n ????);
1576          whd in match (shift_offset_n ????) in ⊢ (??%%);
1577          whd in match (offset_plus ??);
1578          whd in match (offset_plus ??);
1579          >commutative_addition_n >(associative_addition_n … offset_size ?)
1580          >(commutative_addition_n ? (offv offset) ?) @refl
1581     ]
1582] qed.
1583
1584lemma subtraction_delta : ∀x,y,delta.
1585  subtraction offset_size
1586    (addition_n offset_size x delta)
1587    (addition_n offset_size y delta) =
1588  subtraction offset_size x y.
1589#x #y #delta whd in match subtraction; normalize nodelta
1590(* Remove all the equal parts on each side of the equation. *)
1591<associative_addition_n
1592>two_complement_negation_plus
1593<(commutative_addition_n … (two_complement_negation ? delta))
1594>(associative_addition_n ? delta) >bitvector_opp_addition_n
1595>(commutative_addition_n ? (zero ?)) >neutral_addition_n
1596@refl
1597qed.
1598
1599(* Offset subtraction is invariant by translation *)
1600lemma sub_offset_translation :
1601 ∀n,x,y,delta. sub_offset n x y = sub_offset n (offset_plus x delta) (offset_plus y delta).
1602#n #x #y #delta
1603whd in match (sub_offset ???) in ⊢ (??%%);
1604elim x #x' elim y #y' elim delta #delta'
1605whd in match (offset_plus ??);
1606whd in match (offset_plus ??);
1607>subtraction_delta @refl
1608qed.
1609
1610(* value_eq lifts to subtraction *)
1611lemma sub_value_eq :
1612  ∀E,v1,v2,v1',v2',ty1,ty2.
1613   value_eq E v1 v2 →
1614   value_eq E v1' v2' →
1615   ∀r1. (sem_sub v1 ty1 v1' ty2=Some val r1→
1616           ∃r2:val.sem_sub v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2).
1617#E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1
1618@(value_eq_inversion E … Hvalue_eq1)
1619[ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ]
1620[ 1: whd in match (sem_sub ????); normalize nodelta
1621     cases (classify_sub ty1 ty2) normalize nodelta
1622     [ 1: #sz #sg | 2: #fsz | 3: #n #ty #sz #sg | 4: #n #sz #sg #ty | 5: #ty1' #ty2' ]
1623     #Habsurd destruct (Habsurd)
1624| 2: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta
1625     cases (classify_sub ty1 ty2) normalize nodelta     
1626     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
1627     [ 2,3,5: #Habsurd destruct (Habsurd) ]
1628     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
1629     [ 1,6: #v' | 2,7: #sz' #i' | 3,8: #f' | 4,9: | 5,10: #p1' #p2' #Hembed' ]
1630     [ 1,2,4,5,6,7,8,9,10: #Habsurd destruct (Habsurd) ]
1631     @intsize_eq_elim_elim
1632      [ 1: #_ #Habsurd destruct (Habsurd)
1633      | 2: #Heq destruct (Heq) normalize nodelta
1634           #Heq destruct (Heq)
1635          /3 by ex_intro, conj, vint_eq/           
1636      ]
1637| 3: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta
1638     cases (classify_sub ty1 ty2) normalize nodelta     
1639     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
1640     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
1641     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
1642     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
1643     [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
1644     #Heq destruct (Heq)
1645     /3 by ex_intro, conj, vfloat_eq/
1646| 4: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta
1647     cases (classify_sub ty1 ty2) normalize nodelta
1648     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
1649     [ 1,2,5: #Habsurd destruct (Habsurd) ]
1650     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
1651     [ 1,6: #v' | 2,7: #sz' #i' | 3,8: #f' | 4,9: | 5,10: #p1' #p2' #Hembed' ]
1652     [ 1,2,4,5,6,7,9,10: #Habsurd destruct (Habsurd) ]         
1653     [ 1: @eq_bv_elim [ 1: normalize nodelta #Heq1 #Heq2 destruct /3 by ex_intro, conj, vnull_eq/
1654                      | 2: #_ normalize nodelta #Habsurd destruct (Habsurd) ]
1655     | 2: #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/ ]
1656| 5: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta
1657     cases (classify_sub ty1 ty2) normalize nodelta
1658     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
1659     [ 1,2,5: #Habsurd destruct (Habsurd) ]
1660     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
1661     [ 1,6: #v' | 2,7: #sz' #i' | 3,8: #f' | 4,9: | 5,10: #p1' #p2' #Hembed' ]
1662     [ 1,2,4,5,6,7,8,9: #Habsurd destruct (Habsurd) ]
1663     #Heq destruct (Heq)
1664     [ 1: %{(Vptr (neg_shift_pointer_n (bitsize_of_intsize sz') p2 (sizeof ty) i'))} @conj try @refl
1665          @vptr_eq whd in match (pointer_translation ??) in Hembed ⊢ %;
1666          elim p1 in Hembed; #b1 #o1 normalize nodelta
1667          cases (E b1)
1668          [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
1669          | 2: * #block #offset normalize nodelta #Heq destruct (Heq)
1670               whd in match (offset_plus ??) in ⊢ (??%%);
1671               whd in match (neg_shift_pointer_n ????) in ⊢ (??%%);
1672               whd in match (neg_shift_offset_n ????) in ⊢ (??%%);
1673               whd in match (subtraction) in ⊢ (??%%); normalize nodelta
1674               generalize in match (short_multiplication ???); #mult
1675               /3 by associative_addition_n, commutative_addition_n, refl/
1676          ]
1677     | 2: lapply Heq @eq_block_elim
1678          [ 2: #_ normalize nodelta #Habsurd destruct (Habsurd)
1679          | 1: #Hpblock1_eq normalize nodelta
1680               elim p1 in Hpblock1_eq Hembed Hembed'; #b1 #off1
1681               elim p1' #b1' #off1' whd in ⊢ (% → % → ?); #Hpblock1_eq destruct (Hpblock1_eq)
1682               whd in ⊢ ((??%?) → (??%?) → ?);
1683               cases (E b1') normalize nodelta
1684               [ 1: #Habsurd destruct (Habsurd) ]
1685               * #dest_block #dest_off normalize nodelta
1686               #Heq_ptr1 #Heq_ptr2 destruct >eq_block_b_b normalize nodelta
1687               cases (eqb (sizeof tsg) O) normalize nodelta
1688               [ 1: #Habsurd destruct (Habsurd)
1689               | 2: >(sub_offset_translation 32 off1 off1' dest_off)
1690                    cases (division_u 31
1691                            (sub_offset 32 (offset_plus off1 dest_off) (offset_plus off1' dest_off))
1692                            (repr (sizeof tsg)))
1693                    [ 1: normalize nodelta #Habsurd destruct (Habsurd)
1694                    | 2: #r1' normalize nodelta #Heq2 destruct (Heq2)
1695                         /3 by ex_intro, conj, vint_eq/ ]
1696    ] ] ]
1697] qed.
1698
1699
1700lemma mul_value_eq :
1701  ∀E,v1,v2,v1',v2',ty1,ty2.
1702   value_eq E v1 v2 →
1703   value_eq E v1' v2' →
1704   ∀r1. (sem_mul v1 ty1 v1' ty2=Some val r1→
1705           ∃r2:val.sem_mul v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2).
1706#E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1
1707@(value_eq_inversion E … Hvalue_eq1)
1708[ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ]
1709[ 1: whd in match (sem_mul ????); normalize nodelta
1710     cases (classify_aop ty1 ty2) normalize nodelta
1711     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
1712     #Habsurd destruct (Habsurd)
1713| 2: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta
1714     cases (classify_aop ty1 ty2) normalize nodelta
1715     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
1716     [ 2,3: #Habsurd destruct (Habsurd) ]
1717     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
1718     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
1719     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
1720     @intsize_eq_elim_elim
1721      [ 1: #_ #Habsurd destruct (Habsurd)
1722      | 2: #Heq destruct (Heq) normalize nodelta
1723           #Heq destruct (Heq)
1724          /3 by ex_intro, conj, vint_eq/           
1725      ]
1726| 3: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta
1727     cases (classify_aop ty1 ty2) normalize nodelta
1728     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
1729     [ 1,3: #Habsurd destruct (Habsurd) ]
1730     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta     
1731     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
1732     [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
1733     #Heq destruct (Heq)
1734     /3 by ex_intro, conj, vfloat_eq/
1735| 4: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta
1736     cases (classify_aop ty1 ty2) normalize nodelta
1737     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
1738     #Habsurd destruct (Habsurd)
1739| 5: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta
1740     cases (classify_aop ty1 ty2) normalize nodelta
1741     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]     
1742     #Habsurd destruct (Habsurd)
1743] qed.
1744
1745lemma div_value_eq :
1746  ∀E,v1,v2,v1',v2',ty1,ty2.
1747   value_eq E v1 v2 →
1748   value_eq E v1' v2' →
1749   ∀r1. (sem_div v1 ty1 v1' ty2=Some val r1→
1750           ∃r2:val.sem_div v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2).
1751#E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1
1752@(value_eq_inversion E … Hvalue_eq1)
1753[ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ]
1754[ 1: whd in match (sem_div ????); normalize nodelta
1755     cases (classify_aop ty1 ty2) normalize nodelta
1756     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
1757     #Habsurd destruct (Habsurd)
1758| 2: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta
1759     cases (classify_aop ty1 ty2) normalize nodelta
1760     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
1761     [ 2,3: #Habsurd destruct (Habsurd) ]
1762     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
1763     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
1764     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
1765     elim sg normalize nodelta
1766     @intsize_eq_elim_elim
1767     [ 1,3: #_ #Habsurd destruct (Habsurd)
1768     | 2,4: #Heq destruct (Heq) normalize nodelta
1769            @(match (division_s (bitsize_of_intsize sz') i i') with
1770              [ None ⇒ ?
1771              | Some bv' ⇒ ? ])
1772            [ 1: normalize  #Habsurd destruct (Habsurd)
1773            | 2: normalize #Heq destruct (Heq)
1774                 /3 by ex_intro, conj, vint_eq/
1775            | 3,4: elim sz' in i' i; #i' #i
1776                   normalize in match (pred_size_intsize ?);
1777                   generalize in match division_u; #division_u normalize
1778                   @(match (division_u ???) with
1779                    [ None ⇒ ?
1780                    | Some bv ⇒ ?]) normalize nodelta
1781                   #H destruct (H)
1782                  /3 by ex_intro, conj, vint_eq/ ]
1783     ]
1784| 3: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta
1785     cases (classify_aop ty1 ty2) normalize nodelta
1786     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
1787     [ 1,3: #Habsurd destruct (Habsurd) ]
1788     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta     
1789     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
1790     [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
1791     #Heq destruct (Heq)
1792     /3 by ex_intro, conj, vfloat_eq/
1793| 4: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta
1794     cases (classify_aop ty1 ty2) normalize nodelta
1795     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
1796     #Habsurd destruct (Habsurd)
1797| 5: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta
1798     cases (classify_aop ty1 ty2) normalize nodelta
1799     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]     
1800     #Habsurd destruct (Habsurd)
1801] qed.
1802
1803lemma mod_value_eq :
1804  ∀E,v1,v2,v1',v2',ty1,ty2.
1805   value_eq E v1 v2 →
1806   value_eq E v1' v2' →
1807   ∀r1. (sem_mod v1 ty1 v1' ty2=Some val r1→
1808           ∃r2:val.sem_mod v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2).
1809#E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1
1810@(value_eq_inversion E … Hvalue_eq1)
1811[ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ]
1812[ 1: whd in match (sem_mod ????); normalize nodelta
1813     cases (classify_aop ty1 ty2) normalize nodelta
1814     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
1815     #Habsurd destruct (Habsurd)
1816| 2: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta
1817     cases (classify_aop ty1 ty2) normalize nodelta
1818     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
1819     [ 2,3: #Habsurd destruct (Habsurd) ]
1820     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
1821     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
1822     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
1823     elim sg normalize nodelta
1824     @intsize_eq_elim_elim
1825     [ 1,3: #_ #Habsurd destruct (Habsurd)
1826     | 2,4: #Heq destruct (Heq) normalize nodelta
1827            @(match (modulus_s (bitsize_of_intsize sz') i i') with
1828              [ None ⇒ ?
1829              | Some bv' ⇒ ? ])
1830            [ 1: normalize  #Habsurd destruct (Habsurd)
1831            | 2: normalize #Heq destruct (Heq)
1832                 /3 by ex_intro, conj, vint_eq/
1833            | 3,4: elim sz' in i' i; #i' #i
1834                   generalize in match modulus_u; #modulus_u normalize
1835                   @(match (modulus_u ???) with
1836                    [ None ⇒ ?
1837                    | Some bv ⇒ ?]) normalize nodelta
1838                   #H destruct (H)
1839                  /3 by ex_intro, conj, vint_eq/ ]
1840     ]
1841| 3: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta
1842     cases (classify_aop ty1 ty2) normalize nodelta
1843     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
1844     #Habsurd destruct (Habsurd)
1845| 4: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta
1846     cases (classify_aop ty1 ty2) normalize nodelta
1847     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
1848     #Habsurd destruct (Habsurd)
1849| 5: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta
1850     cases (classify_aop ty1 ty2) normalize nodelta
1851     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]     
1852     #Habsurd destruct (Habsurd)
1853] qed.
1854
1855(* boolean ops *)
1856lemma and_value_eq :
1857  ∀E,v1,v2,v1',v2'.
1858   value_eq E v1 v2 →
1859   value_eq E v1' v2' →
1860   ∀r1. (sem_and v1 v1'=Some val r1→
1861           ∃r2:val.sem_and v2 v2'=Some val r2∧value_eq E r1 r2).
1862#E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1
1863@(value_eq_inversion E … Hvalue_eq1)
1864[ 2: #sz #i
1865     @(value_eq_inversion E … Hvalue_eq2)
1866     [ 2: #sz' #i' whd in match (sem_and ??);
1867          @intsize_eq_elim_elim
1868          [ 1: #_ #Habsurd destruct (Habsurd)
1869          | 2: #Heq destruct (Heq) normalize nodelta
1870               #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/ ]
1871] ]
1872normalize in match (sem_and ??); #arg1 destruct
1873normalize in match (sem_and ??); #arg2 destruct
1874normalize in match (sem_and ??); #arg3 destruct
1875normalize in match (sem_and ??); #arg4 destruct
1876qed.
1877
1878lemma or_value_eq :
1879  ∀E,v1,v2,v1',v2'.
1880   value_eq E v1 v2 →
1881   value_eq E v1' v2' →
1882   ∀r1. (sem_or v1 v1'=Some val r1→
1883           ∃r2:val.sem_or v2 v2'=Some val r2∧value_eq E r1 r2).
1884#E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1
1885@(value_eq_inversion E … Hvalue_eq1)
1886[ 2: #sz #i
1887     @(value_eq_inversion E … Hvalue_eq2)
1888     [ 2: #sz' #i' whd in match (sem_or ??);
1889          @intsize_eq_elim_elim
1890          [ 1: #_ #Habsurd destruct (Habsurd)
1891          | 2: #Heq destruct (Heq) normalize nodelta
1892               #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/ ]
1893] ]
1894normalize in match (sem_or ??); #arg1 destruct
1895normalize in match (sem_or ??); #arg2 destruct
1896normalize in match (sem_or ??); #arg3 destruct
1897normalize in match (sem_or ??); #arg4 destruct
1898qed.
1899
1900lemma xor_value_eq :
1901  ∀E,v1,v2,v1',v2'.
1902   value_eq E v1 v2 →
1903   value_eq E v1' v2' →
1904   ∀r1. (sem_xor v1 v1'=Some val r1→
1905           ∃r2:val.sem_xor v2 v2'=Some val r2∧value_eq E r1 r2).
1906#E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1
1907@(value_eq_inversion E … Hvalue_eq1)
1908[ 2: #sz #i
1909     @(value_eq_inversion E … Hvalue_eq2)
1910     [ 2: #sz' #i' whd in match (sem_xor ??);
1911          @intsize_eq_elim_elim
1912          [ 1: #_ #Habsurd destruct (Habsurd)
1913          | 2: #Heq destruct (Heq) normalize nodelta
1914               #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/ ]
1915] ]
1916normalize in match (sem_xor ??); #arg1 destruct
1917normalize in match (sem_xor ??); #arg2 destruct
1918normalize in match (sem_xor ??); #arg3 destruct
1919normalize in match (sem_xor ??); #arg4 destruct
1920qed.
1921
1922lemma shl_value_eq :
1923  ∀E,v1,v2,v1',v2'.
1924   value_eq E v1 v2 →
1925   value_eq E v1' v2' →
1926   ∀r1. (sem_shl v1 v1'=Some val r1→
1927           ∃r2:val.sem_shl v2 v2'=Some val r2∧value_eq E r1 r2).
1928#E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1
1929@(value_eq_inversion E … Hvalue_eq1)
1930[ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ]
1931[ 2:
1932     @(value_eq_inversion E … Hvalue_eq2)
1933     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
1934     [ 2: whd in match (sem_shl ??);
1935          cases (lt_u ???) normalize nodelta
1936          [ 1: #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/
1937          | 2: #Habsurd destruct (Habsurd)
1938          ]
1939     | *: whd in match (sem_shl ??); #Habsurd destruct (Habsurd) ]
1940| *: whd in match (sem_shl ??); #Habsurd destruct (Habsurd) ]
1941qed.
1942
1943lemma shr_value_eq :
1944  ∀E,v1,v2,v1',v2',ty,ty'.
1945   value_eq E v1 v2 →
1946   value_eq E v1' v2' →
1947   ∀r1. (sem_shr v1 ty v1' ty'=Some val r1→
1948           ∃r2:val.sem_shr v2 ty v2' ty'=Some val r2∧value_eq E r1 r2).
1949#E #v1 #v2 #v1' #v2' #ty #ty' #Hvalue_eq1 #Hvalue_eq2 #r1
1950@(value_eq_inversion E … Hvalue_eq1)
1951[ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ]
1952whd in match (sem_shr ????); whd in match (sem_shr ????);
1953[ 1: cases (classify_aop ty ty') normalize nodelta
1954     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
1955     #Habsurd destruct (Habsurd)
1956| 2: cases (classify_aop ty ty') normalize nodelta
1957     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
1958     [ 2,3: #Habsurd destruct (Habsurd) ]
1959     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
1960     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
1961     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
1962     elim sg normalize nodelta
1963     cases (lt_u ???) normalize nodelta #Heq destruct (Heq)
1964     /3 by ex_intro, conj, refl, vint_eq/
1965| 3: cases (classify_aop ty ty') normalize nodelta
1966     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
1967     #Habsurd destruct (Habsurd)
1968| 4: cases (classify_aop ty ty') normalize nodelta
1969     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
1970     #Habsurd destruct (Habsurd)
1971| 5: cases (classify_aop ty ty') normalize nodelta
1972     [ 1: #sz #sg | 2: #fsz | 3: #ty1' #ty2' ]
1973     #Habsurd destruct (Habsurd)
1974] qed.
1975
1976lemma eq_offset_translation : ∀delta,x,y. cmp_offset Ceq (offset_plus x delta) (offset_plus y delta) = cmp_offset Ceq x y.
1977* #delta * #x * #y
1978whd in match (offset_plus ??);
1979whd in match (offset_plus ??);
1980whd in match cmp_offset; normalize nodelta
1981whd in match eq_offset; normalize nodelta
1982@(eq_bv_elim … x y)
1983[ 1: #Heq >Heq >eq_bv_true @refl
1984| 2: #Hneq lapply (injective_inv_addition_n  … x y delta Hneq)
1985     @(eq_bv_elim … (addition_n offset_size x delta) (addition_n offset_size y delta))
1986     [ 1: #H * #H' @(False_ind … (H' H)) | 2: #_ #_ @refl ]
1987] qed.     
1988
1989lemma neq_offset_translation : ∀delta,x,y. cmp_offset Cne (offset_plus x delta) (offset_plus y delta) = cmp_offset Cne x y.
1990* #delta * #x * #y
1991whd in match (offset_plus ??);
1992whd in match (offset_plus ??);
1993whd in match cmp_offset; normalize nodelta
1994whd in match eq_offset; normalize nodelta
1995@(eq_bv_elim … x y)
1996[ 1: #Heq >Heq >eq_bv_true @refl
1997| 2: #Hneq lapply (injective_inv_addition_n  … x y delta Hneq)
1998     @(eq_bv_elim … (addition_n offset_size x delta) (addition_n offset_size y delta))
1999     [ 1: #H * #H' @(False_ind … (H' H)) | 2: #_ #_ @refl ]
2000] qed.
2001
2002
2003(* /!\ Here is the source of all sadness (op = lt) /!\ *)
2004axiom cmp_offset_translation : ∀op,delta,x,y.
2005   cmp_offset op x y = cmp_offset op (offset_plus x delta) (offset_plus y delta).
2006
2007(* 5 Nov. 2012 : the rest of the stuff doesn't checks anymore. Not a big deal, it was here
2008 * for historical purposes, and for potential inspiration for Clight to Cminor. I leave the
2009 * code commented for future reference.
2010 *)
2011
2012(*
2013lemma cmp_value_eq :
2014  ∀E,v1,v2,v1',v2',ty,ty',m1,m2.
2015   value_eq E v1 v2 →
2016   value_eq E v1' v2' →
2017   memory_inj E m1 m2 →   
2018   ∀op,r1. (sem_cmp op v1 ty v1' ty' m1 = Some val r1→
2019           ∃r2:val.sem_cmp op v2 ty v2' ty' m2 = Some val r2∧value_eq E r1 r2).
2020#E #v1 #v2 #v1' #v2' #ty #ty' #m1 #m2 #Hvalue_eq1 #Hvalue_eq2 #Hinj #op #r1
2021elim m1 in Hinj; #contmap1 #nextblock1 #Hnextblock1 elim m2 #contmap2 #nextblock2 #Hnextblock2 #Hinj
2022whd in match (sem_cmp ??????) in ⊢ ((??%?) → %);
2023cases (classify_cmp ty ty') normalize nodelta
2024[ 1: #tsz #tsg
2025     @(value_eq_inversion E … Hvalue_eq1) normalize nodelta
2026     [ 1: #v #Habsurd destruct (Habsurd)
2027     | 3: #f #Habsurd destruct (Habsurd)
2028     | 4: #Habsurd destruct (Habsurd)
2029     | 5: #p1 #p2 #Hembed #Habsurd destruct (Habsurd) ]
2030     #sz #i
2031     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2032     [ 1: #v #Habsurd destruct (Habsurd)
2033     | 3: #f #Habsurd destruct (Habsurd)
2034     | 4: #Habsurd destruct (Habsurd)
2035     | 5: #p1 #p2 #Hembed #Habsurd destruct (Habsurd) ]
2036     #sz' #i' cases tsg normalize nodelta
2037     @intsize_eq_elim_elim
2038     [ 1,3: #Hneq #Habsurd destruct (Habsurd)
2039     | 2,4: #Heq destruct (Heq) normalize nodelta
2040            #Heq destruct (Heq)
2041            [ 1: cases (cmp_int ????) whd in match (of_bool ?);
2042            | 2: cases (cmpu_int ????) whd in match (of_bool ?); ]
2043              /3 by ex_intro, conj, vint_eq/ ]
2044| 3: #fsz
2045     @(value_eq_inversion E … Hvalue_eq1) normalize nodelta
2046     [ 1: #v #Habsurd destruct (Habsurd)
2047     | 2: #sz #i #Habsurd destruct (Habsurd)
2048     | 4: #Habsurd destruct (Habsurd)
2049     | 5: #p1 #p2 #Hembed #Habsurd destruct (Habsurd) ]
2050     #f
2051     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2052     [ 1: #v #Habsurd destruct (Habsurd)
2053     | 2: #sz #i #Habsurd destruct (Habsurd)
2054     | 4: #Habsurd destruct (Habsurd)
2055     | 5: #p1 #p2 #Hembed #Habsurd destruct (Habsurd) ]
2056     #f'
2057     #Heq destruct (Heq) cases (Fcmp op f f')
2058     /3 by ex_intro, conj, vint_eq/
2059| 4: #ty1 #ty2 #Habsurd destruct (Habsurd)
2060| 2: #optn #typ
2061     @(value_eq_inversion E … Hvalue_eq1) normalize nodelta
2062     [ 1: #v #Habsurd destruct (Habsurd)
2063     | 2: #sz #i #Habsurd destruct (Habsurd)
2064     | 3: #f #Habsurd destruct (Habsurd)
2065     | 5: #p1 #p2 #Hembed ]
2066     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
2067     [ 1,6: #v #Habsurd destruct (Habsurd)
2068     | 2,7: #sz #i #Habsurd destruct (Habsurd)
2069     | 3,8: #f #Habsurd destruct (Habsurd)
2070     | 5,10: #p1' #p2' #Hembed' ]
2071     [ 2,3: cases op whd in match (sem_cmp_mismatch ?);
2072          #Heq destruct (Heq)
2073          [ 1,3: %{Vfalse} @conj try @refl @vint_eq
2074          | 2,4: %{Vtrue} @conj try @refl @vint_eq ]
2075     | 4: cases op whd in match (sem_cmp_match ?);
2076          #Heq destruct (Heq)
2077          [ 2,4: %{Vfalse} @conj try @refl @vint_eq
2078          | 1,3: %{Vtrue} @conj try @refl @vint_eq ] ]
2079     lapply (mi_valid_pointers … Hinj p1' p2')
2080     lapply (mi_valid_pointers … Hinj p1 p2)         
2081     cases (valid_pointer (mk_mem ???) p1')
2082     [ 2: #_ #_ >commutative_andb normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ]
2083     cases (valid_pointer (mk_mem ???) p1)
2084     [ 2: #_ #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ]
2085     #H1 #H2 lapply (H1 (refl ??) Hembed) #Hvalid1 lapply (H2 (refl ??) Hembed') #Hvalid2
2086     >Hvalid1 >Hvalid2 normalize nodelta -H1 -H2
2087     elim p1 in Hembed; #b1 #o1
2088     elim p1' in Hembed'; #b1' #o1'
2089     whd in match (pointer_translation ??);
2090     whd in match (pointer_translation ??);
2091     @(eq_block_elim … b1 b1')
2092     [ 1: #Heq destruct (Heq)
2093          cases (E b1') normalize nodelta
2094          [ 1: #Habsurd destruct (Habsurd) ]
2095          * #eb1' #eo1' normalize nodelta
2096          #Heq1 #Heq2 #Heq3 destruct
2097          >eq_block_b_b normalize nodelta
2098          <cmp_offset_translation
2099          cases (cmp_offset ???) normalize nodelta         
2100          /3 by ex_intro, conj, vint_eq/
2101     | 2: #Hneq lapply (mi_disjoint … Hinj b1 b1')
2102          cases (E b1') [ 1: #_ normalize nodelta #Habsurd destruct (Habsurd) ]
2103          * #eb1 #eo1
2104          cases (E b1) [ 1: #_ normalize nodelta #_ #Habsurd destruct (Habsurd) ]
2105          * #eb1' #eo1' normalize nodelta #H #Heq1 #Heq2 destruct
2106          lapply (H ???? Hneq (refl ??) (refl ??))
2107          #Hneq_block >(neq_block_eq_block_false … Hneq_block) normalize nodelta
2108          elim op whd in match (sem_cmp_mismatch ?); #Heq destruct (Heq)
2109          /3 by ex_intro, conj, vint_eq/
2110     ]
2111] qed.    *)           
2112
2113(*
2114lemma binary_operation_value_eq :
2115  ∀E,op,v1,v2,v1',v2',ty1,ty2,m1,m2.
2116   value_eq E v1 v2 →
2117   value_eq E v1' v2' →
2118   memory_inj E m1 m2 →
2119   ∀r1.
2120   sem_binary_operation op v1 ty1 v1' ty2 m1 = Some ? r1 →
2121   ∃r2.sem_binary_operation op v2 ty1 v2' ty2 m2 = Some ? r2 ∧ value_eq E r1 r2.
2122#E #op #v1 #v2 #v1' #v2' #ty1 #ty2 #m1 #m2 #Hvalue_eq1 #Hvalue_eq2 #Hinj #r1
2123cases op
2124whd in match (sem_binary_operation ??????);
2125whd in match (sem_binary_operation ??????);
2126[ 1: @add_value_eq try assumption
2127| 2: @sub_value_eq try assumption
2128| 3: @mul_value_eq try assumption
2129| 4: @div_value_eq try assumption
2130| 5: @mod_value_eq try assumption
2131| 6: @and_value_eq try assumption
2132| 7: @or_value_eq try assumption
2133| 8: @xor_value_eq try assumption
2134| 9: @shl_value_eq try assumption
2135| 10: @shr_value_eq try assumption
2136| *: @cmp_value_eq try assumption
2137] qed. *)
2138
2139(*
2140lemma cast_value_eq :
2141 ∀E,m1,m2,v1,v2. (* memory_inj E m1 m2 → *) value_eq E v1 v2 →
2142  ∀ty,cast_ty,res. exec_cast m1 v1 ty cast_ty = OK ? res →
2143  ∃res'. exec_cast m2 v2 ty cast_ty = OK ? res' ∧ value_eq E res res'.
2144#E #m1 #m2 #v1 #v2 (* #Hmemory_inj *) #Hvalue_eq #ty #cast_ty #res
2145@(value_eq_inversion … Hvalue_eq)
2146[ 1: #v normalize #Habsurd destruct (Habsurd)
2147| 2: #vsz #vi whd in match (exec_cast ????);
2148     cases ty
2149     [ 1: | 2: #sz #sg | 3: #fl | 4: #ptrty | 5: #arrayty #n | 6: #tl #retty | 7: #id #fl | 8: #id #fl | 9: #comptrty ]
2150     normalize nodelta
2151     [ 1,3,7,8,9: #Habsurd destruct (Habsurd)
2152     | 2: @intsize_eq_elim_elim
2153          [ 1: #Hneq #Habsurd destruct (Habsurd)
2154          | 2: #Heq destruct (Heq) normalize nodelta
2155               cases cast_ty
2156               [ 1: | 2: #csz #csg | 3: #cfl | 4: #cptrty | 5: #carrayty #cn
2157               | 6: #ctl #cretty | 7: #cid #cfl | 8: #cid #cfl | 9: #ccomptrty ]
2158               normalize nodelta
2159               [ 1,7,8,9: #Habsurd destruct (Habsurd)
2160               | 2: #Heq destruct (Heq) /3 by ex_intro, conj, vint_eq/
2161               | 3: #Heq destruct (Heq) /3 by ex_intro, conj, vfloat_eq/
2162               | 4,5,6: whd in match (try_cast_null ?????); normalize nodelta
2163                    @eq_bv_elim
2164                    [ 1,3,5: #Heq destruct (Heq) >eq_intsize_identity normalize nodelta
2165                         whd in match (m_bind ?????);
2166                         #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/
2167                    | 2,4,6: #Hneq >eq_intsize_identity normalize nodelta
2168                         whd in match (m_bind ?????);
2169                         #Habsurd destruct (Habsurd) ] ]
2170          ]
2171     | 4,5,6: whd in match (try_cast_null ?????); normalize nodelta
2172          @eq_bv_elim
2173          [ 1,3,5: #Heq destruct (Heq) normalize nodelta
2174               whd in match (m_bind ?????); #Habsurd destruct (Habsurd)
2175          | 2,4,6: #Hneq normalize nodelta
2176               whd in match (m_bind ?????); #Habsurd destruct (Habsurd) ]
2177     ]
2178| 3: #f whd in match (exec_cast ????);
2179     cases ty
2180     [ 1: | 2: #sz #sg | 3: #fl | 4: #ptrty | 5: #arrayty #n
2181     | 6: #tl #retty | 7: #id #fl | 8: #id #fl | 9: #comptrty ]
2182     normalize nodelta
2183     [ 1,2,4,5,6,7,8,9: #Habsurd destruct (Habsurd) ]
2184     cases cast_ty
2185     [ 1: | 2: #csz #csg | 3: #cfl | 4: #cptrty | 5: #carrayty #cn
2186     | 6: #ctl #cretty | 7: #cid #cfl | 8: #cid #cfl | 9: #ccomptrty ]
2187     normalize nodelta
2188     [ 1,4,5,6,7,8,9: #Habsurd destruct (Habsurd) ]
2189     #Heq destruct (Heq)
2190     [ 1: /3 by ex_intro, conj, vint_eq/
2191     | 2: /3 by ex_intro, conj, vfloat_eq/ ]
2192| 4: whd in match (exec_cast ????);
2193     cases ty
2194     [ 1: | 2: #sz #sg | 3: #fl | 4: #ptrty | 5: #arrayty #n
2195     | 6: #tl #retty | 7: #id #fl | 8: #id #fl | 9: #comptrty ]
2196     normalize
2197     [ 1,2,3,7,8,9: #Habsurd destruct (Habsurd) ]
2198     cases cast_ty normalize nodelta
2199     [ 1,10,19: #Habsurd destruct (Habsurd)
2200     | 2,11,20: #csz #csg #Habsurd destruct (Habsurd)
2201     | 3,12,21: #cfl #Habsurd destruct (Habsurd)
2202     | 4,13,22: #cptrty #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/
2203     | 5,14,23: #carrayty #cn #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/
2204     | 6,15,24: #ctl #cretty #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/
2205     | 7,16,25: #cid #cfl #Habsurd destruct (Habsurd)
2206     | 8,17,26: #cid #cfl #Habsurd destruct (Habsurd)
2207     | 9,18,27: #ccomptrty #Habsurd destruct (Habsurd) ]
2208| 5: #p1 #p2 #Hembed whd in match (exec_cast ????);
2209     cases ty
2210     [ 1: | 2: #sz #sg | 3: #fl | 4: #ptrty | 5: #arrayty #n
2211     | 6: #tl #retty | 7: #id #fl | 8: #id #fl | 9: #comptrty ]
2212     normalize
2213     [ 1,2,3,7,8,9: #Habsurd destruct (Habsurd) ]
2214     cases cast_ty normalize nodelta
2215     [ 1,10,19: #Habsurd destruct (Habsurd)
2216     | 2,11,20: #csz #csg #Habsurd destruct (Habsurd)
2217     | 3,12,21: #cfl #Habsurd destruct (Habsurd)
2218     | 4,13,22: #cptrty #Heq destruct (Heq) %{(Vptr p2)} @conj try @refl @vptr_eq assumption
2219     | 5,14,23: #carrayty #cn #Heq destruct (Heq)
2220                %{(Vptr p2)} @conj try @refl @vptr_eq assumption
2221     | 6,15,24: #ctl #cretty #Heq destruct (Heq)
2222                %{(Vptr p2)} @conj try @refl @vptr_eq assumption
2223     | 7,16,25: #cid #cfl #Habsurd destruct (Habsurd)
2224     | 8,17,26: #cid #cfl #Habsurd destruct (Habsurd)
2225     | 9,18,27: #ccomptrty #Habsurd destruct (Habsurd) ]
2226qed.
2227
2228lemma bool_of_val_value_eq :
2229 ∀E,v1,v2. value_eq E v1 v2 →
2230   ∀ty,b.exec_bool_of_val v1 ty = OK ? b → exec_bool_of_val v2 ty = OK ? b.
2231#E #v1 #v2 #Hvalue_eq #ty #b
2232@(value_eq_inversion … Hvalue_eq) //
2233[ 1: #v #H normalize in H; destruct (H)
2234| 2: #p1 #p2 #Hembed #H @H ] qed.
2235
2236*)
2237(*
2238lemma sim_related_globals : ∀ge,ge',en1,m1,en2,m2,ext.
2239  ∀E:embedding.
2240  ∀Hext:memory_ext E m1 m2.
2241  switch_removal_globals E ? fundef_switch_removal ge ge' →
2242  disjoint_extension en1 m1 en2 m2 ext E Hext →
2243  ext_fresh_for_genv ext ge →
2244  (∀e. exec_expr_sim E (exec_expr ge en1 m1 e) (exec_expr ge' en2 m2 e)) ∧
2245  (∀ed, ty. exec_lvalue_sim E (exec_lvalue' ge en1 m1 ed ty) (exec_lvalue' ge' en2 m2 ed ty)).
2246#ge #ge' #en1 #m1 #en2 #m2 #ext #E #Hext #Hrelated #Hdisjoint #Hext_fresh_for_genv
2247@expr_lvalue_ind_combined
2248[ 1: #csz #cty #i #a1
2249     whd in match (exec_expr ????); elim cty
2250     [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
2251     normalize nodelta
2252     [ 2: cases (eq_intsize csz sz) normalize nodelta
2253          [ 1: #H destruct (H) /4 by ex_intro, conj, vint_eq/
2254          | 2: #Habsurd destruct (Habsurd) ]
2255     | 4,5,6: #_ #H destruct (H)
2256     | *: #H destruct (H) ]
2257| 2: #ty #fl #a1
2258     whd in match (exec_expr ????); #H1 destruct (H1) /4 by ex_intro, conj, vint_eq/
2259| 3: *
2260  [ 1: #sz #i | 2: #fl | 3: #var_id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1
2261  | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ]
2262  #ty whd in ⊢ (% → ?); #Hind try @I
2263  whd in match (Plvalue ???);
2264  [ 1,2,3: whd in match (exec_expr ????); whd in match (exec_expr ????); #a1
2265       cases (exec_lvalue' ge en1 m1 ? ty) in Hind;
2266       [ 2,4,6: #error #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
2267       | 1,3,5: #b1 #H elim (H b1 (refl ??)) #b2 *
2268           elim b1 * #bl1 #o1 #tr1 elim b2 * #bl2 #o2 #tr2
2269           #Heq >Heq normalize nodelta * #Hvalue_eq #Htrace_eq
2270           whd in match (load_value_of_type' ???);
2271           whd in match (load_value_of_type' ???);
2272           lapply (load_value_of_type_inj E … (\fst a1) … ty (me_inj … Hext) Hvalue_eq)
2273           cases (load_value_of_type ty m1 bl1 o1)
2274           [ 1,3,5: #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
2275           | 2,4,6: #v #Hyp normalize in ⊢ (% → ?); #Heq destruct (Heq)
2276                    elim (Hyp (refl ??)) #v2 * #Hload #Hvalue_eq >Hload
2277                    normalize /4 by ex_intro, conj/
2278  ] ] ]
2279| 4: #v #ty whd * * #b1 #o1 #tr1
2280     whd in match (exec_lvalue' ?????);
2281     whd in match (exec_lvalue' ?????);
2282     lapply (Hdisjoint v)
2283     lapply (Hext_fresh_for_genv v)
2284     cases (mem_assoc_env v ext) #Hglobal
2285     [ 1: * #vblock * * #Hlookup_en2 #Hwriteable #Hnot_in_en1
2286          >Hnot_in_en1 normalize in Hglobal ⊢ (% → ?);
2287          >(Hglobal (refl ??)) normalize
2288          #Habsurd destruct (Habsurd)
2289     | 2: normalize nodelta
2290          cases (lookup ?? en1 v) normalize nodelta
2291          [ 1: #Hlookup2 >Hlookup2 normalize nodelta
2292               lapply (rg_find_symbol … Hrelated v)
2293               cases (find_symbol ???) normalize
2294               [ 1: #_ #Habsurd destruct (Habsurd)
2295               | 2: #block cases (lookup ?? (symbols clight_fundef ge') v)
2296                    [ 1: normalize nodelta #Hfalse @(False_ind … Hfalse)
2297                    | 2: #block' normalize #Hvalue_eq #Heq destruct (Heq)
2298                         %{〈block',mk_offset (zero offset_size),[]〉} @conj try @refl
2299                         normalize /2/
2300                ] ]
2301         | 2: #block
2302              cases (lookup ?? en2 v) normalize nodelta
2303              [ 1: #Hfalse @(False_ind … Hfalse)
2304              | 2: #b * #Hvalid_block #Hvalue_eq #Heq destruct (Heq)
2305                   %{〈b, zero_offset, E0〉} @conj try @refl
2306                   normalize /2/
2307    ] ] ]
2308| 5: #e #ty whd in ⊢ (% → %);
2309     whd in match (exec_lvalue' ?????);
2310     whd in match (exec_lvalue' ?????);
2311     cases (exec_expr ge en1 m1 e)
2312     [ 1: * #v1 #tr1 #H elim (H 〈v1,tr1〉 (refl ??)) * #v1' #tr1' * #Heq >Heq normalize nodelta
2313          * elim v1 normalize nodelta
2314          [ 1: #_ #_ #a1 #Habsurd destruct (Habsurd)
2315          | 2: #sz #i #_ #_ #a1  #Habsurd destruct (Habsurd)
2316          | 3: #fl #_ #_ #a1 #Habsurd destruct (Habsurd)
2317          | 4: #_ #_ #a1 #Habsurd destruct (Habsurd)
2318          | 5: #ptr #Hvalue_eq lapply (value_eq_ptr_inversion … Hvalue_eq) * #p2 * #Hp2_eq
2319               >Hp2_eq in Hvalue_eq; elim ptr #b1 #o1 elim p2 #b2 #o2
2320               #Hvalue_eq normalize
2321               cases (E b1) [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ]
2322               * #b2' #o2' normalize #Heq destruct (Heq) #Htrace destruct (Htrace)
2323               * * #b1' #o1' #tr1'' #Heq2 destruct (Heq2) normalize
2324               %{〈b2,mk_offset (addition_n ? (offv o1') (offv o2')),tr1''〉} @conj try @refl
2325               normalize @conj // ]
2326     | 2: #error #_ normalize #a1 #Habsurd destruct (Habsurd) ]
2327| 6: #ty #e #ty'
2328     #Hsim @(exec_lvalue_expr_elim … Hsim)
2329     cases ty
2330     [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
2331     * #b1 #o1 * #b2 #o2 normalize nodelta try /2 by I/
2332     #tr #H @conj try @refl try assumption
2333| 7: #ty #op #e
2334     #Hsim @(exec_expr_expr_elim … Hsim) #v1 #v2 #trace #Hvalue_eq
2335     lapply (unary_operation_value_eq E op v1 v2 (typeof e) Hvalue_eq)
2336     cases (sem_unary_operation op v1 (typeof e)) normalize nodelta
2337     [ 1: #_ @I
2338     | 2: #r1 #H elim (H r1 (refl ??)) #r1' * #Heq >Heq
2339           normalize /2/ ]
2340| 8: #ty #op #e1 #e2 #Hsim1 #Hsim2
2341     @(exec_expr_expr_elim … Hsim1) #v1 #v2 #trace #Hvalue_eq
2342     cases (exec_expr ge en1 m1 e2) in Hsim2;
2343     [ 2: #error // ]
2344     * #val #trace normalize in ⊢ (% → ?); #Hsim2
2345     elim (Hsim2 ? (refl ??)) * #val2 #trace2 * #Hexec2 * #Hvalue_eq2 #Htrace >Hexec2
2346     whd in match (m_bind ?????); whd in match (m_bind ?????);
2347     lapply (binary_operation_value_eq E op … (typeof e1) (typeof e2) ?? Hvalue_eq Hvalue_eq2 (me_inj … Hext))
2348     cases (sem_binary_operation op v1 (typeof e1) val (typeof e2) m1)
2349     [ 1: #_ // ]
2350     #opval #Hop elim (Hop ? (refl ??)) #opval' * #Hopval_eq  #Hvalue_eq_opval
2351     >Hopval_eq normalize destruct /2 by conj/
2352| 9: #ty #cast_ty #e #Hsim @(exec_expr_expr_elim … Hsim)
2353     #v1 #v2 #trace #Hvalue_eq lapply (cast_value_eq E m1 m2 … Hvalue_eq (typeof e) cast_ty)
2354     cases (exec_cast m1 v1 (typeof e) cast_ty)
2355     [ 2: #error #_ normalize @I
2356     | 1: #res #H lapply (H res (refl ??)) whd in match (m_bind ?????);
2357          * #res' * #Hexec_cast >Hexec_cast #Hvalue_eq normalize nodelta
2358          @conj // ]
2359| 10: #ty #e1 #e2 #e3 #Hsim1 #Hsim2 #Hsim3
2360     @(exec_expr_expr_elim … Hsim1) #v1 #v2 #trace #Hvalue_eq
2361     lapply (bool_of_val_value_eq E v1 v2 Hvalue_eq (typeof e1))
2362     cases (exec_bool_of_val ? (typeof e1)) #b
2363     [ 2: #_ normalize @I ]
2364     #H lapply (H ? (refl ??)) #Hexec >Hexec normalize
2365     cases b normalize nodelta
2366     [ 1: (* true branch *)
2367          cases (exec_expr ge en1 m1 e2) in Hsim2;
2368          [ 2: #error normalize #_ @I
2369          | 1: * #e2v #e2tr normalize #H elim (H ? (refl ??))
2370               * #e2v' #e2tr' * #Hexec2 >Hexec2 * #Hvalue_eq2 #Htrace_eq2 normalize
2371                    destruct @conj try // ]
2372     | 2: (* false branch *)
2373          cases (exec_expr ge en1 m1 e3) in Hsim3;
2374          [ 2: #error normalize #_ @I
2375          | 1: * #e3v #e3tr normalize #H elim (H ? (refl ??))
2376               * #e3v' #e3tr' * #Hexec3 >Hexec3 * #Hvalue_eq3 #Htrace_eq3 normalize
2377               destruct @conj // ] ]
2378| 11,12: #ty #e1 #e2 #Hsim1 #Hsim2
2379     @(exec_expr_expr_elim … Hsim1) #v1 #v1' #trace #Hvalue_eq
2380     lapply (bool_of_val_value_eq E v1 v1' Hvalue_eq (typeof e1))     
2381     cases (exec_bool_of_val v1 (typeof e1))
2382     [ 2,4:  #error #_ normalize @I ]
2383     #b cases b #H lapply (H ? (refl ??)) #Heq >Heq
2384     whd in match (m_bind ?????);
2385     whd in match (m_bind ?????);
2386     [ 2,3: normalize @conj try @refl try @vint_eq ]
2387     cases (exec_expr ge en1 m1 e2) in Hsim2;
2388     [ 2,4: #error #_ normalize @I ]
2389     * #v2 #tr2 whd in ⊢ (% → %); #H2 normalize nodelta elim (H2 ? (refl ??))
2390     * #v2' #tr2' * #Heq2 * #Hvalue_eq2 #Htrace2 >Heq2 normalize nodelta
2391     lapply (bool_of_val_value_eq E v2 v2' Hvalue_eq2 (typeof e2))
2392     cases (exec_bool_of_val v2 (typeof e2))
2393     [ 2,4: #error #_ normalize @I ]
2394     #b2 #H3 lapply (H3 ? (refl ??)) #Heq3 >Heq3 normalize nodelta
2395     destruct @conj try @conj //
2396     cases b2 whd in match (of_bool ?); @vint_eq
2397| 13: #ty #ty' cases ty
2398     [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n
2399     | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
2400     whd in match (exec_expr ????); whd
2401     * #v #trace #Heq destruct %{〈Vint sz (repr sz (sizeof ty')), E0〉}
2402     @conj try @refl @conj //
2403| 14: #ty #ed #aggregty #i #Hsim whd * * #b #o #tr normalize nodelta
2404    whd in match (exec_lvalue' ?????);
2405    whd in match (exec_lvalue' ge' en2 m2 (Efield (Expr ed aggregty) i) ty);
2406    whd in match (typeof ?);
2407    cases aggregty in Hsim;
2408    [ 1: | 2: #sz' #sg' | 3: #fl' | 4: #ty' | 5: #ty' #n'
2409    | 6: #tl' #ty' | 7: #id' #fl' | 8: #id' #fl' | 9: #ty' ]
2410    normalize nodelta #Hsim
2411    [ 1,2,3,4,5,6,9: #Habsurd destruct (Habsurd) ]
2412    whd in match (m_bind ?????);
2413    whd in match (m_bind ?????);
2414    whd in match (exec_lvalue ge en1 m1 (Expr ed ?));
2415    cases (exec_lvalue' ge en1 m1 ed ?) in Hsim;
2416    [ 2,4: #error #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ]
2417    * * #b1 #o1 #tr1 whd in ⊢ (% → ?); #H elim (H ? (refl ??))
2418    * * #b1' #o1' #tr1' * #Hexec normalize nodelta * #Hvalue_eq #Htrace_eq
2419    whd in match (exec_lvalue ????); >Hexec normalize nodelta
2420    [ 2: #Heq destruct (Heq) %{〈 b1',o1',tr1'〉} @conj //
2421         normalize @conj // ]
2422    cases (field_offset i fl')
2423    [ 2: #error normalize #Habsurd destruct (Habsurd) ]
2424    #offset whd in match (m_bind ?????); #Heq destruct (Heq)
2425    whd in match (m_bind ?????);
2426    %{〈b1',shift_offset (bitsize_of_intsize I32) o1' (repr I32 offset),tr1'〉} @conj
2427    destruct // normalize nodelta @conj try @refl @vptr_eq
2428    -H lapply (value_eq_ptr_inversion … Hvalue_eq) * #p2 * #Hptr_eq
2429    whd in match (pointer_translation ??);     
2430    whd in match (pointer_translation ??);
2431    cases (E b)
2432    [ 1: normalize nodelta #Habsurd destruct (Habsurd) ]
2433    * #b' #o' normalize nodelta #Heq destruct (Heq) destruct (Hptr_eq)
2434    cut (offset_plus (mk_offset (addition_n offset_size
2435                                      (offv o1)
2436                                      (sign_ext (bitsize_of_intsize I32) offset_size (repr I32 offset)))) o'
2437          = (shift_offset (bitsize_of_intsize I32) (offset_plus o1 o') (repr I32 offset)))
2438    [ whd in match (shift_offset ???) in ⊢ (???%);
2439      whd in match (offset_plus ??) in ⊢ (??%%);
2440      /3 by associative_addition_n, commutative_addition_n, refl/ ]
2441    #Heq >Heq @refl
2442| 15: #ty #l #e #Hsim
2443     @(exec_expr_expr_elim … Hsim) #v1 #v2 #trace #Hvalue_eq normalize nodelta @conj //
2444| 16: *
2445  [ 1: #sz #i | 2: #fl | 3: #var_id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1
2446  | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ]
2447  #ty normalize in ⊢ (% → ?);
2448  [ 3,4,13: @False_ind
2449  | *: #_ normalize #a1 #Habsurd destruct (Habsurd) ]
2450] qed. *)
Note: See TracBrowser for help on using the repository browser.