source: src/Clight/toCminorCorrectness.ma @ 2572

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

Progress on toCminorCorrectness.

File size: 116.3 KB
Line 
1include "Clight/toCminor.ma".
2
3(* When we characterise the local Clight variables, those that are stack
4   allocated are given disjoint regions of the stack. *)
5
6lemma characterise_vars_disjoint : ∀globals,f,vartypes,stacksize,id,n,ty.
7  characterise_vars globals f = 〈vartypes, stacksize〉 →
8  lookup ?? vartypes id = Some ? 〈Stack n,ty〉 →
9  ∀id',n',ty'. id ≠ id' →
10  lookup ?? vartypes id' = Some ? 〈Stack n',ty'〉 →
11  n' + sizeof ty' ≤ n ∨ n + sizeof ty ≤ n'.
12#globals * #ret #args #vars #body #vartypes #stacksize #id #n #ty
13whd in ⊢ (??%? → ?);
14generalize in match vartypes; -vartypes
15generalize in match stacksize; -stacksize
16elim (args@vars)
17[ #stacksize #vartypes #CHAR #L @⊥ whd in CHAR:(??%?); destruct
18  elim globals in L;
19  [ normalize #L destruct
20  | * * #id' #r #ty' #tl #IH
21    whd in match (foldr ?????);
22    #L cases (lookup_add_cases ??????? L)
23    [ * #E1 #E2 destruct
24    | @IH
25    ]
26  ]
27| * #id1 #ty1 #tl #IH #stacksize #vartypes
28  whd in match (foldr ?????);
29  (* Avoid writing out the definition again *)
30  letin ih ≝ (foldr ? (Prod ??) ?? tl) in IH ⊢ %;
31  lapply (refl ? ih) whd in match ih; -ih
32  cases (foldr ? (Prod ??) ?? tl) in ⊢ (???% → %);
33  #vartypes' #stack' #FOLD #IH
34  whd in ⊢ (??(match % with [_⇒?])? → ?);
35  cases (orb ??)
36  #CHAR whd in CHAR:(??%?); destruct
37  #L cases (lookup_add_cases ??????? L)
38  [ 1,3: * #E1 #E2 destruct
39    #id' #n' #ty' #NE >lookup_add_miss /2/
40    #L' %1 -L -IH
41    generalize in match vartypes' in FOLD L' ⊢ %; -vartypes'
42    generalize in match stack'; -stack'
43    elim tl
44    [ #stack' #vartypes2 whd in ⊢ (??%? → ?); #F destruct #L' @⊥
45      elim globals in L';
46      [ normalize #E destruct
47      | * * #id2 #r2 #ty2 #tl2 #IH whd in match (foldr ?????);
48        #L cases (lookup_add_cases ??????? L)
49        [ * #E1 #E2 destruct
50        | @IH
51        ]
52      ]
53    | * #id2 #ty2 #tl2 #IH #stack' #vartypes'
54      whd in ⊢ (??%? → ?); cases (foldr ? (Prod ??) ???) in IH ⊢ %;
55      #vartypes2 #stack2 #IH
56      whd in ⊢ (??%? → ?);
57      cases (orb ??)
58      [ #E whd in E:(??%?); destruct #L cases (lookup_add_cases ??????? L)
59        [ * #E1 #E2 destruct //
60        | #L'' lapply (IH ?? (refl ??) L'') /2/
61        ]
62      | #E whd in E:(??%?); destruct #L cases (lookup_add_cases ??????? L)
63        [ * #E1 #E2 destruct
64        | #L'' lapply (IH ?? (refl ??) L'') /2/
65        ]
66      ]
67    ]
68  | -L #L #id' #n' #ty' #NE #L'
69    cases (lookup_add_cases ??????? L')
70    [ * #E1 #E2 destruct
71      %2 -IH -L'
72      generalize in match vartypes' in FOLD L; -vartypes'
73      generalize in match stack'; -stack'
74      elim tl
75      [ #stack' #vartypes' whd in ⊢ (??%? → ?); #F destruct #L @⊥
76        elim globals in L;
77        [ normalize #E destruct
78        | * * #id1 #r1 #ty1 #tl1 #IH whd in match (foldr ?????);
79          #L cases (lookup_add_cases ??????? L)
80          [ * #E1 #E2 destruct
81          | @IH
82          ]
83        ]
84      | * #id1 #ty1 #tl1 #IH #stack' #vartypes'
85        whd in ⊢ (??%? → ?); cases (foldr ? (Prod ??) ???) in IH ⊢ %;
86        #vartypes2 #stack2 #IH
87        whd in ⊢ (??%? → ?);
88        cases (orb ??)
89        #E whd in E:(??%?); destruct
90        #L cases (lookup_add_cases ??????? L)
91        [ 1,3: * #E1 #E2 destruct //
92        | 2,4: #L' lapply (IH ?? (refl ??) L') /2/
93        ]
94      ]
95    | @(IH … (refl ??) L … NE)
96    ]
97  | -L #L #id' #n' #ty' #NE #L'
98    cases (lookup_add_cases ??????? L')
99    [ * #E1 #E2 destruct
100    | @(IH … (refl ??) L … NE)
101    ]
102  ]
103] qed.
104
105(* And everything is in the stack frame. *)
106
107lemma characterise_vars_in_range : ∀globals,f,vartypes,stacksize,id,n,ty.
108  characterise_vars globals f = 〈vartypes, stacksize〉 →
109  lookup ?? vartypes id = Some ? 〈Stack n,ty〉 →
110  n + sizeof ty ≤ stacksize.
111#globals * #ret #args #vars #body whd in match (characterise_vars ??);
112elim (args@vars)
113[ #vartypes #stacksize #id #n #ty #FOLD #L @⊥
114  whd in FOLD:(??%?); destruct elim globals in L;
115  [ #E normalize in E; destruct
116  | * * #id' #r' #ty' #tl' #IH
117    whd in match (foldr ?????); #L cases (lookup_add_cases ??????? L)
118    [ * #E1 #E2 destruct
119    | @IH
120    ]
121  ]
122| * #id' #ty' #tl #IH #vartypes #stacksize #id #n #ty
123  whd in match (foldr ?????); cases (foldr ? (Prod ??) ???) in IH ⊢ %;
124  #vartypes' #stackspace' #IH
125  whd in ⊢ (??(match % with [_⇒?])? → ?);
126  cases (orb ??) whd in ⊢ (??%? → ?);
127  #E destruct #L cases (lookup_add_cases ??????? L)
128  [ 1,3: * #E1 #E2 destruct //
129  | 2,4: #L' lapply (IH … (refl ??) L') /2/
130  ]
131] qed.
132
133(* Local variables show up in the variable characterisation as local. *)
134
135lemma characterise_vars_localid : ∀globals,f,vartypes,stacksize,id.
136  characterise_vars globals f = 〈vartypes, stacksize〉 →
137  Exists ? (λx. \fst x = id) (fn_params f @ fn_vars f) →
138  ∃t. local_id vartypes id t.
139#globals * #ret #args #vars #body
140whd in match (characterise_vars ??); elim (args@vars)
141[ #vartypes #stacksize #id #_ *
142| * #hd #ty #tl #IH
143  #vartypes #stacksize #id
144  whd in match (foldr ?????);
145  cases (foldr ? (Prod ??) ???) in IH ⊢ %;
146  #vartypes' #stackspace' #IH
147  whd in ⊢ (??(match % with [_⇒?])? → ?);
148  cases (orb ??)
149  #E whd in E:(??%?); destruct *
150  [ 1,3: #E destruct %{(typ_of_type ty)}
151    whd whd in match (lookup' ??); >lookup_add_hit //
152  | 2,4: #TL cases (IH … (refl ??) TL) #ty' #LC
153    cases (identifier_eq ? id hd)
154    [ 1,3: #E destruct %{(typ_of_type ty)} whd whd in match (lookup' ??); >lookup_add_hit //
155    | 2,4: #NE %{ty'} whd whd in match (lookup' ??); >lookup_add_miss //
156    ]
157  ]
158] qed.
159
160(* Put knowledge that Globals are global into a more useful form than the
161   one used for the invariant. *)
162
163lemma characterise_vars_global : ∀globals,f,vartypes,stacksize.
164  characterise_vars globals f = 〈vartypes, stacksize〉 →
165  ∀id,r,ty. lookup' vartypes id = OK ? 〈Global r,ty〉 →
166  Exists ? (λx.x = 〈〈id,r〉,ty〉) globals ∧
167  ¬ Exists ? (λx. \fst x = id) (fn_params f @ fn_vars f).
168#globals #f #vartypes #stacksize #CHAR #id #r #ty #L
169cases (characterise_vars_src … CHAR id ?)
170[ * #r' * #ty' >L
171  * #E1 destruct (E1) #EX
172  %
173  [ @EX
174  | % #EX' cases (characterise_vars_localid … CHAR EX')
175    #ty' whd in ⊢ (% → ?); >L *
176  ]
177| * #ty' whd in ⊢ (% → ?); >L *
178| whd >(opt_eq_from_res ???? L) % #E destruct
179] qed.
180
181
182(* Show how the global environments match up. *)
183
184lemma map_partial_All_to_All2 : ∀A,B,P,f,l,H,l'.
185  map_partial_All A B P f l H = OK ? l' →
186  All2 ?? (λa,b. ∃p. f a p = OK ? b) l l'.
187#A #B #P #f #l
188elim l
189[ #H #l' #MAP normalize in MAP; destruct //
190| #h #t #IH * #p #H #l'
191  whd in ⊢ (??%? → ?);
192  lapply (refl ? (f h p)) whd in match (proj1 ???);
193  cases (f h p) in ⊢ (???% → %);
194  [ #b #E #MAP cases (bind_inversion ????? MAP)
195    #tl' * #MAP' #E' normalize in E'; destruct
196    % [ %{p} @E | @IH [ @H | @MAP' ] ]
197  | #m #_ #X normalize in X; destruct
198  ]
199] qed.
200 
201
202definition clight_cminor_matching : clight_program → matching ≝
203λp.
204  let tmpuniverse ≝ universe_for_program p in
205  let fun_globals ≝ map ?? (λidf. 〈\fst idf,Code,type_of_fundef (\snd idf)〉) (prog_funct ?? p) in
206  let var_globals ≝ map ?? (λv. 〈\fst (\fst v), \snd (\fst v), \snd (\snd v)〉) (prog_vars ?? p) in
207  let globals ≝ fun_globals @ var_globals in
208  mk_matching
209    ?? (list init_data × type) (list init_data)
210    (λvs,f_clight,f_cminor. ∃H1,H2. translate_fundef tmpuniverse globals H1 f_clight H2 = OK ? f_cminor)
211    (λv,w. \fst v = w).
212
213lemma clight_to_cminor_varnames : ∀p,p'.
214  clight_to_cminor p = OK ? p' →
215  prog_var_names … p = prog_var_names … p'.
216* #vars #fns #main * #vars' #fns' #main'
217#TO cases (bind_inversion ????? TO) #fns'' * #MAP #E
218whd in E:(??%%); destruct
219-MAP normalize
220elim vars
221[ //
222| * * #id #r * #d #t #tl #IH normalize >IH //
223] qed.
224
225
226lemma clight_to_cminor_matches : ∀p,p'.
227  clight_to_cminor p = OK ? p' →
228  match_program (clight_cminor_matching p) p p'.
229* #vars #fns #main * #vars' #fns' #main'
230#TO cases (bind_inversion ????? TO) #fns'' * #MAP #E
231whd in E:(??%%); destruct
232%
233[ -MAP whd in match (m_V ?); whd in match (m_W ?);
234  elim vars
235  [ //
236  | * * #id #r * #init #ty #tl #IH %
237    [ % //
238    | @(All2_mp … IH) * * #a #b * #c #d * * #e #f #g * /2/
239    ]
240  ]
241| @(All2_mp … (map_partial_All_to_All2 … MAP)) -MAP
242  * #id #f * #id' #f' * #H #F cases (bind_inversion ????? F) #f'' * #TRANSF #E
243  normalize in E; destruct
244  <(clight_to_cminor_varnames … TO)
245  % whd
246  % [2: % [2: @TRANSF | skip ] | skip ]
247| %
248] qed.
249
250include "Clight/Cexec.ma".
251include "Clight/abstract.ma".
252include "Cminor/abstract.ma".
253
254(* Invariants used in simulation *)
255
256record clight_cminor_inv : Type[0] ≝ {
257  globals : list (ident × region × type);
258  ge_cl : genv_t clight_fundef;
259  ge_cm : genv_t (fundef internal_function);
260  eq_sym : ∀s. find_symbol … ge_cl s = find_symbol … ge_cm s;
261  trans_fn : ∀v,f. find_funct … ge_cl v = Some ? f →
262    ∃tmp_u,f',H1,H2.
263      translate_fundef tmp_u globals H1 f H2 = OK ? f' ∧
264      find_funct … ge_cm v = Some ? f'
265}.
266
267include "Clight/CexecInd.ma".
268include "Clight/frontend_misc.ma".
269include "Clight/memoryInjections.ma".
270
271(* Perhaps we will have to be more precise on what is allocated, etc.
272   cf [exec_alloc_variables]. For now this is conveniently hidden in
273   the [value_eq E v v'] *)
274definition memory_matching ≝
275  λE:embedding.
276  λm,m':mem.
277  λen:cl_env.
278  λvenv:cm_env.
279  λcminv:clight_cminor_inv.
280  λsp:block.
281  λvars:var_types.
282  ∀id.
283    match lookup SymbolTag ? en id with
284    [ None ⇒
285      match find_symbol ? (ge_cl cminv) id with
286      [ None ⇒ True
287      | Some cl_blo ⇒ E cl_blo = Some ? 〈cl_blo, zero_offset〉
288      ]
289    | Some cl_blo ⇒
290         match lookup ?? vars id with
291         [ Some kind ⇒
292            let 〈vtype, type〉 ≝ kind in
293            match vtype with
294            [ Stack n ⇒
295              E cl_blo = Some ? 〈sp, mk_offset (repr I16 n)〉
296            | Local ⇒
297              ∀v. load_value_of_type type m cl_blo zero_offset = Some ? v →
298                   ∃v'. lookup ?? venv id = Some ? v' ∧
299                        value_eq E v v'
300            | _ ⇒ False ]
301        | None ⇒ False ]
302    ].
303             
304lemma type_should_eq_inversion :
305  ∀ty1,ty2,P,f,res.
306    type_should_eq ty1 ty2 P f = OK ? res →
307    ty1 = ty2 ∧ f ≃ res.
308#ty1 #ty2 #P #f #res normalize
309cases (type_eq_dec ty1 ty2) normalize nodelta
310[ 2: #Hneq #Habsurd destruct ]
311#Heq #Heq2 @conj try assumption
312destruct (Heq2) cases Heq normalize nodelta
313@eq_to_jmeq @refl
314qed.
315
316lemma typ_should_eq_inversion :
317  ∀ty1,ty2,P,a,x.
318    typ_should_eq ty1 ty2 P a = OK ? x →
319    ty1 = ty2 ∧ a ≃ x.
320* [ #sz #sg ] * [ 1,3: #sz2 #sg2 ]
321[ 4: #P #a #x normalize #H destruct (H) @conj try @refl @refl_jmeq
322| 3: cases sz cases sg #P #A #x normalize #H destruct
323| 2: cases sz2 cases sg2 #P #a #x normalize #H destruct ]
324cases sz cases sz2 cases sg cases sg2
325#P #a #x #H normalize in H:(??%?); destruct (H)
326try @conj try @refl try @refl_jmeq
327qed.
328
329lemma load_value_of_type_by_ref :
330  ∀ty,m,b,off,val.
331    load_value_of_type ty m b off = Some ? val →
332    typ_of_type ty ≃ ASTptr →
333    access_mode ty ≃ By_reference →
334    val = Vptr (mk_pointer b off).
335*
336[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
337| #structname #fieldspec | #unionname #fieldspec | #id ]
338#m #b #off #val
339[ 1,6,7: normalize #Habsurd destruct (Habsurd)
340| 4,5: normalize #Heq #_ #_ destruct @refl
341| 2: #_ normalize #Heq destruct
342| *: #Hload normalize #_ #H
343      lapply (jmeq_to_eq ??? H) #Heq destruct
344] qed.
345
346lemma load_value_of_type_by_value :
347  ∀ty,m,b,off,val.
348  access_mode ty = By_value (typ_of_type ty) →
349  load_value_of_type ty m b off = Some ? val →
350  loadv (typ_of_type ty) m (Vptr (mk_pointer b off)) = Some ? val.
351
352[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
353| #structname #fieldspec | #unionname #fieldspec | #id ]
354#m #b #off #val
355normalize in match (access_mode ?);
356[ 1,4,5,6,7: #Habsurd destruct ]
357#_
358#H @H
359qed.
360
361lemma lookup_exec_alloc :
362  ∀source_variables, initial_env, env, var_id, clb, m, m'.
363  lookup ?? env var_id = Some ? clb →
364  exec_alloc_variables initial_env m source_variables = 〈env,m'〉 →
365  lookup ?? initial_env var_id = Some ? clb ∨
366  Exists ? (λx. \fst x = var_id) source_variables.
367#source_variables
368elim source_variables
369[ 1: #init_env #env #var #clb #m #m' #Hlookup #Hexec_alloc normalize in Hexec_alloc;
370     destruct (Hexec_alloc) %1 @Hlookup
371| 2: * #id #ty #tail #Hind
372     #init_env #env #var #clb #m #m' #Hlookup     
373     whd in ⊢ (??%? → ?);
374     cases (alloc m 0 (sizeof ty) XData) #m0 * #blo #Hreg normalize nodelta
375     #Hexec_alloc
376     @(match identifier_eq ? id var with [ inl Heq ⇒ ? | inr Hneq ⇒ ? ])
377     [ 1: destruct (Heq) %2 %1 @refl ]
378     cases (Hind … Hlookup Hexec_alloc)
379     [ @cthulhu (* standard reasoning on positive_maps. check lib. *)
380     | #Hexists %2 %2 @Hexists ]
381] qed.
382
383lemma characterise_vars_lookup_local :
384  ∀globals,f,vartypes,stacksize,id,clb,env.
385   characterise_vars globals f = 〈vartypes, stacksize〉 →
386   lookup ?? env id = Some ? clb →
387   (∃m,m'. exec_alloc_variables empty_env m (fn_params f @ fn_vars f) = 〈env,m'〉) →
388   ∃t. local_id vartypes id t.
389#globals #f #vartypes #stacksize #id #clb #env
390#Hchar #Hlookup * #m * #m' #Hexec
391cases (lookup_exec_alloc … Hlookup Hexec)
392[ normalize in ⊢ (% → ?); #Heq destruct
393| @(characterise_vars_localid … Hchar) ]
394qed.
395
396
397lemma exec_alloc_fail_antimonotonic : ∀variables,env,env',var_id.
398  (∃m,m'.exec_alloc_variables env m variables=〈env',m'〉) →
399  lookup ?? env' var_id = None ? →
400  lookup ?? env var_id = None ? ∧
401  ¬(Exists (ident×type) (λx:ident×type.\fst  x=var_id) variables). 
402#vars elim vars
403[ #env #env' #var_id normalize * #m * #m' #Heq destruct (Heq)
404  #H @conj try @H % //
405| * #id' #ty' #tl #Hind #env #env' #var * #m * #m'
406  whd in ⊢ ((??%?) → ? → ?);
407  cases (alloc m 0 (sizeof ty') XData) #m0 * #b #Hregion
408  normalize nodelta #Hexec #Hlookup
409  lapply (Hind …  (ex_intro … (ex_intro … Hexec)) Hlookup)
410  cases env #env cases id' #id' cases var #var normalize
411  @(eqb_elim … id' var)
412  [ 2: #Hneq * #Hlookup' #Hexists' lapply (lookup_opt_pm_set_miss ? (Some ? b) … env (sym_neq ??? Hneq))
413       #Heq <Heq @conj try @Hlookup' % *
414       [ #Heq' destruct (Heq') cases Hneq #H @H @refl
415       | cases Hexists' #H @H ]
416  | 1: #Heq destruct (Heq) * #Hlookup' #Hexists'   
417       lapply (lookup_opt_pm_set_hit … (Some ? b) var … env) #H1
418       >H1 in Hlookup'; #Heq destruct
419  ]
420] qed.
421
422lemma variable_not_in_env_but_in_vartypes_is_global :
423  ∀env,env',f,vars,stacksize,globals,var_id.
424  (∃m,m'.exec_alloc_variables env m (fn_params f@fn_vars f) =〈env',m'〉) →
425  characterise_vars globals f =〈vars,stacksize〉 →
426  lookup ?? env' var_id = None ? →       
427  ∀allocty,ty. lookup' vars var_id = OK ? 〈allocty, ty〉 →
428  ∃r.allocty = Global r.
429#env #env' #f #vars #stacksize #globals #var_id#Hexec_alloc
430#Hcharacterise #Hlookup_fail #allocty #ty #Hlookup_type_ok
431lapply (characterise_vars_src … Hcharacterise var_id ?)
432[ whd % cases (res_inversion ?????? Hlookup_type_ok) * #vt #t *
433 #Hlookup >Hlookup #_ #Habsurd destruct ]
434*
435[ 1: * #r * #ty' * #Hlookup' #Hex %{r}
436     >Hlookup' in Hlookup_type_ok; #Heq destruct @refl ]
437* #t whd in ⊢ (% → ?); >Hlookup_type_ok whd normalize nodelta
438@(match allocty
439  return λx. allocty = x → ?
440  with
441  [ Global r ⇒ λ_. ?
442  | Stack st' ⇒ λHalloc. ?
443  | Local ⇒ λHalloc. ?
444  ] (refl ? allocty))
445[ @False_ind ] normalize nodelta
446#Heq_typ
447(* Halloc is in contradiction with Hlookup_fail *)
448lapply (exec_alloc_fail_antimonotonic … Hexec_alloc … Hlookup_fail)
449* #Hlookup' #Hnot_exists
450lapply (characterise_vars_all … Hcharacterise var_id t ?)
451[ 1,3: whd destruct (Halloc) >Hlookup_type_ok // ]
452#Hexists @False_ind
453cut (Exists (ident×type) (λx:ident×type.\fst  x=var_id) (fn_params f@fn_vars f))
454[ 1,3: elim (fn_params f @ fn_vars f) in Hexists; //
455       * #id' #ty' #tl #Hind *
456       [ 1,3: * #Heq #_ %1 @Heq
457       | *: #H %2 @Hind @H ] ]
458#H cases Hnot_exists #H' @H' @H
459qed.
460
461
462lemma translate_notbool_to_cminor :
463  ∀t,sg,arg.
464  ∀cmop. translate_unop (typ_of_type t) (ASTint I32 sg) Onotbool = OK ? cmop →
465  ∀res. sem_unary_operation Onotbool arg t = Some ? res →
466        eval_unop (typ_of_type t) (ASTint I32 sg) cmop arg = Some ? res.
467*
468[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
469| #structname #fieldspec | #unionname #fieldspec | #id ]
470normalize in match (typ_of_type ?);
471#sg #arg #cmop
472whd in ⊢ (??%% → ?); #Heq destruct (Heq)
473cases arg
474[ | #vsz #vi | | #vp
475| | #vsz #vi | | #vp
476| | #vsz #vi | | #vp
477| | #vsz #vi | | #vp
478| | #vsz #vi | | #vp
479| | #vsz #vi | | #vp
480| | #vsz #vi | | #vp
481| | #vsz #vi | | #vp ]
482#res
483whd in ⊢ ((??%?) → ?);
484#Heq
485[ 6,11,12: | *: destruct (Heq) ]
486[ 2,3: destruct (Heq) whd in match (eval_unop ????); @refl
487| 1: lapply Heq -Heq @(eq_intsize_elim … sz vsz)
488     #H normalize nodelta #Heq destruct
489     whd in match (eval_unop ????);
490     cases (eq_bv (bitsize_of_intsize vsz) vi (zero (bitsize_of_intsize vsz))) @refl
491] qed.
492
493lemma translate_notint_to_cminor :
494  ∀t,t',arg.
495  ∀cmop. translate_unop (typ_of_type t) t' Onotint = OK ? cmop →
496  ∀res. sem_unary_operation Onotint arg t = Some ? res →
497        eval_unop (typ_of_type t) t' cmop arg = Some ? res.
498#ty *
499[ 2: #arg #cmop whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) ]
500#sz #sg #arg #cmop
501whd in match (translate_unop ???);
502@(match typ_eq (ASTint sz sg) (typ_of_type ty)
503  with
504  [ inl H ⇒ ?
505  | inr H ⇒ ? ])
506normalize nodelta
507[ 2: #Heq destruct ]
508lapply H -H
509lapply cmop -cmop
510cases ty
511[ | #sz' #sg' | #ptr_ty | #array_ty #array_sz | #domain #codomain
512| #structname #fieldspec | #unionname #fieldspec | #id ]
513normalize nodelta
514#cmop normalize in match (typ_of_type ?); #H destruct
515#H' normalize in H';
516destruct (H')
517#res
518whd in match (sem_unary_operation ???);
519cases arg
520[ | #vsz #vi | | #vp
521| | #vsz #vi | | #vp
522| | #vsz #vi | | #vp
523| | #vsz #vi | | #vp ]
524whd in match (sem_notint ?);
525#H destruct (H) @refl
526qed.
527
528
529lemma translate_negint_to_cminor :
530  ∀t,t',arg.
531  ∀cmop. translate_unop (typ_of_type t) t' Oneg = OK ? cmop →
532  ∀res. sem_unary_operation Oneg arg t = Some ? res →
533        eval_unop (typ_of_type t) t' cmop arg = Some ? res.
534#ty *
535[ 2: #arg #cmop whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) ]
536#sz #sg #arg #cmop
537whd in match (translate_unop ???);
538@(match typ_eq (ASTint sz sg) (typ_of_type ty)
539  with
540  [ inl H ⇒ ?
541  | inr H ⇒ ? ])
542normalize nodelta
543[ 2: #Heq destruct ]
544lapply H -H
545lapply cmop -cmop
546cases ty
547[ | #sz' #sg' | #ptr_ty | #array_ty #array_sz | #domain #codomain
548| #structname #fieldspec | #unionname #fieldspec | #id ]
549normalize nodelta
550#cmop normalize in match (typ_of_type ?); #H destruct
551#H' normalize in H';
552destruct (H')
553#res
554whd in match (sem_unary_operation ???);
555cases arg
556[ | #vsz #vi | | #vp
557| | #vsz #vi | | #vp
558| | #vsz #vi | | #vp
559| | #vsz #vi | | #vp ]
560whd in match (sem_neg ??);
561#H destruct (H)
562whd in match (eval_unop ????);
563cases (eq_intsize sz' vsz) in H; normalize nodelta
564#H destruct @refl
565qed.
566
567
568lemma translate_unop :
569  ∀ty,sg,op,cmop.
570  translate_unop (typ_of_type ty) (ASTint I32 sg) op = OK ? cmop →
571  ∀arg,res. sem_unary_operation op arg ty = Some ? res →
572            eval_unop (typ_of_type ty) (ASTint I32 sg) cmop arg = Some ? res.
573#ty #sg * #cmop #Htranslate #arg
574[ @translate_notbool_to_cminor assumption
575| @translate_notint_to_cminor assumption
576| @translate_negint_to_cminor assumption ]
577qed.
578
579lemma classify_add_inversion :
580  ∀ty1,ty2.
581    (∃sz,sg. ty1 = Tint sz sg ∧ ty2 = Tint sz sg ∧ classify_add ty1 ty2 ≃ add_case_ii sz sg) ∨
582    (∃n,ty',sz,sg. ty1 = ptr_type ty' n ∧ ty2 = Tint sz sg ∧ classify_add ty1 ty2 ≃ add_case_pi n ty' sz sg) ∨
583    (∃n,sz,sg,ty'. ty1 = Tint sz sg ∧ ty2 = ptr_type ty' n ∧ classify_add ty1 ty2 ≃ add_case_ip n sz sg ty') ∨
584    (classify_add ty1 ty2 = add_default ty1 ty2).
585#ty1 #ty2
586cases (classify_add ty1 ty2)
587[ #sz #sg %1 %1 %1 %{sz} %{sg} @conj try @conj try @conj try @refl @refl_jmeq
588| #n #ty #sz #sg %1 %1 %2 %{n} %{ty} %{sz} %{sg} @conj try @conj try @refl @refl_jmeq
589| #n #sz #sg #ty %1 %2 %{n} %{sz} %{sg} %{ty} @conj try @conj try @refl @refl_jmeq
590| #tya #tyb %2 @refl ]
591qed.
592
593(*
594lemma classify_cmp_inversion :
595  ∀ty1,ty2.
596    if_type_eq ty1 ty2 (λty1, ty2. classify_cmp_cases ty1 ty2)
597    ((∃sz,sg. ty1 = Tint sz sg ∧ ty2 = ty1 ∧ classify_cmp ty1 ty2 = cmp_case_ii sz sg) ∨
598     (∃ty'. ty1 = Tpointer ty' ∧ ty2 = ty1 ∧ classify_cmp ty1 ty2 = cmp_case_pp (None ?) ty') ∨
599     (∃ty',n'. ty1 = Tarray ty' n' ∧ ty2 = ty1 ∧ classify_cmp ty1 ty2 = cmp_case_pp (Some ? n') ty') ∨         
600    (classify_cmp ty1 ty2 = cmp_default …)
601*)   
602
603lemma classify_aop_inversion :
604  ∀ty1,ty2.
605    (∃sz,sg. ty1 = (Tint sz sg) ∧ ty2 = (Tint sz sg) ∧ classify_aop ty1 ty2 ≃ aop_case_ii sz sg) ∨
606    classify_aop ty1 ty2 = aop_default ty1 ty2.
607#ty1 #ty2
608cases (classify_aop ty1 ty2)
609[ #sz #sg %1 %{sz} %{sg} @conj try @conj try @refl_jmeq
610| #ty #ty' %2 @refl ]
611qed.
612
613lemma sem_add_ip_inversion :
614  ∀sz,sg,ty',optlen.
615  ∀v1,v2,res.
616  sem_add v1 (Tint sz sg) v2 (ptr_type ty' optlen) = Some ? res →
617  ∃sz',i. v1 = Vint sz' i ∧
618      ((∃p. v2 = Vptr p ∧ res = Vptr (shift_pointer_n ? p (sizeof ty') sg i)) ∨
619       (v2 = Vnull ∧ i = (zero ?) ∧ res = Vnull)).
620#tsz #tsg #ty' * [ | #n ]
621*
622[ | #sz' #i' | | #p'
623| | #sz' #i' | | #p' ]
624#v2 #res
625whd in ⊢ ((??%?) → ?);
626#H destruct
627cases v2 in H;
628[ | #sz2' #i2' | | #p2'
629| | #sz2' #i2' | | #p2' ] normalize nodelta
630#H destruct
631[ 1,3:
632  lapply H -H
633  @(eq_bv_elim … i' (zero ?)) normalize nodelta
634  #Hi #Heq destruct (Heq)
635  %{sz'} %{(zero ?)} @conj destruct try @refl
636  %2 @conj try @conj try @refl
637| *: %{sz'} %{i'} @conj try @refl
638  %1 %{p2'} @conj try @refl
639] qed.
640
641(* symmetric of the upper one *)
642lemma sem_add_pi_inversion :
643  ∀sz,sg,ty',optlen.
644  ∀v1,v2,res.
645  sem_add v1 (ptr_type ty' optlen) v2 (Tint sz sg) = Some ? res →
646  ∃sz',i. v2 = Vint sz' i ∧
647      ((∃p. v1 = Vptr p ∧ res = Vptr (shift_pointer_n ? p (sizeof ty') sg i)) ∨
648       (v1 = Vnull ∧ i = (zero ?) ∧ res = Vnull)).
649#tsz #tsg #ty' * [ | #n ]
650*
651[ | #sz' #i' | | #p'
652| | #sz' #i' | | #p' ]
653#v2 #res
654whd in ⊢ ((??%?) → ?);
655#H destruct
656cases v2 in H; normalize nodelta
657[ | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' ]
658#H destruct
659[ 2,4: %{sz2'} %{i2'} @conj try @refl %1
660  %{p'} @conj try @refl
661| *: lapply H -H
662  @(eq_bv_elim … i2' (zero ?)) normalize nodelta
663  #Hi #Heq destruct (Heq)
664  %{sz2'} %{(zero ?)} @conj destruct try @refl
665  %2 @conj try @conj try @refl
666] qed.
667
668(* Know that addition on integers gives an integer. Notice that there is no correlation
669   between the size in the types and the size of the integer values. *)
670lemma sem_add_ii_inversion :
671  ∀sz,sg.
672  ∀v1,v2,res.
673  sem_add v1 (Tint sz sg) v2 (Tint sz sg) = Some ? res →
674  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
675              res = Vint sz' (addition_n (bitsize_of_intsize sz') i1 i2).
676#sz #sg
677*
678[ | #sz' #i' | | #p' ]
679#v2 #res
680whd in ⊢ ((??%?) → ?); normalize in match (classify_add ??);
681cases sz cases sg normalize nodelta
682#H destruct
683cases v2 in H; normalize nodelta
684#H1 destruct
685#H2 destruct #Heq %{sz'} lapply Heq -Heq
686cases sz' in i'; #i' 
687whd in match (intsize_eq_elim ???????);
688cases H1 in H2; #j' normalize nodelta
689#Heq destruct (Heq)
690%{i'} %{j'} @conj try @conj try @conj try @refl
691qed.
692
693lemma sem_mul_inversion :
694  ∀sz,sg.
695  ∀v1,v2,res.
696  sem_mul v1 (Tint sz sg) v2 (Tint sz sg) = Some ? res →
697  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
698              res = Vint sz' (short_multiplication ? i1 i2).
699#sz #sg *
700[ | #sz' #i' | | #p' ]
701#v2 #res
702whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
703cases sz cases sg normalize nodelta
704#H destruct
705cases v2 in H; normalize nodelta
706#H1 destruct
707#H2 destruct #Heq %{sz'} lapply Heq -Heq
708cases sz' in i'; #i' 
709whd in match (intsize_eq_elim ???????);
710cases H1 in H2; #j' normalize nodelta
711#Heq destruct (Heq)
712%{i'} %{j'} @conj try @conj try @conj try @refl
713qed.
714
715
716lemma sem_div_inversion_s :
717  ∀sz.
718  ∀v1,v2,res.
719  sem_div v1 (Tint sz Signed) v2 (Tint sz Signed) = Some ? res →
720  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
721              match division_s ? i1 i2 with
722              [ Some q ⇒  res =  (Vint sz' q)
723              | None ⇒ False ].
724#sz *
725[ | #sz' #i' | | #p' ]
726#v2 #res
727whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
728>type_eq_dec_true normalize nodelta
729#H destruct
730cases v2 in H; normalize nodelta
731[ | #sz2' #i2' | | #p2' ]
732#Heq destruct
733%{sz'}
734lapply Heq -Heq
735cases sz' in i'; #i' 
736whd in match (intsize_eq_elim ???????);
737cases sz2' in i2'; #i2' normalize nodelta
738whd in match (option_map ????); #Hdiv destruct
739%{i'} %{i2'} @conj try @conj try @conj try @refl
740cases (division_s ???) in Hdiv;
741[ 2,4,6: #bv ] normalize #H destruct (H) try @refl
742qed.
743
744lemma sem_div_inversion_u :
745  ∀sz.
746  ∀v1,v2,res.
747  sem_div v1 (Tint sz Unsigned) v2 (Tint sz Unsigned) = Some ? res →
748  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
749              match division_u ? i1 i2 with
750              [ Some q ⇒  res =  (Vint sz' q)
751              | None ⇒ False ].
752#sz *
753[ | #sz' #i' | | #p' ]
754#v2 #res
755whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
756>type_eq_dec_true normalize nodelta
757#H destruct
758cases v2 in H; normalize nodelta
759[ | #sz2' #i2' | | #p2' ]
760#Heq destruct
761%{sz'}
762lapply Heq -Heq
763cases sz' in i'; #i' 
764whd in match (intsize_eq_elim ???????);
765cases sz2' in i2'; #i2' normalize nodelta
766whd in match (option_map ????); #Hdiv destruct
767%{i'} %{i2'} @conj try @conj try @conj try @refl
768cases (division_u ???) in Hdiv;
769[ 2,4,6: #bv ] normalize #H destruct (H) try @refl
770qed.
771
772lemma sem_mod_inversion_s :
773  ∀sz.
774  ∀v1,v2,res.
775  sem_mod v1 (Tint sz Signed) v2 (Tint sz Signed) = Some ? res →
776  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
777              match modulus_s ? i1 i2 with
778              [ Some q ⇒  res =  (Vint sz' q)
779              | None ⇒ False ].
780#sz *
781[ | #sz' #i' | | #p' ]
782#v2 #res
783whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
784>type_eq_dec_true normalize nodelta
785#H destruct
786cases v2 in H; normalize nodelta
787[ | #sz2' #i2' | | #p2' ]
788#Heq destruct
789%{sz'}
790lapply Heq -Heq
791cases sz' in i'; #i' 
792whd in match (intsize_eq_elim ???????);
793cases sz2' in i2'; #i2' normalize nodelta
794whd in match (option_map ????); #Hdiv destruct
795%{i'} %{i2'} @conj try @conj try @conj try @refl
796cases (modulus_s ???) in Hdiv;
797[ 2,4,6: #bv ] normalize #H destruct (H) try @refl
798qed.
799
800lemma sem_mod_inversion_u :
801  ∀sz.
802  ∀v1,v2,res.
803  sem_mod v1 (Tint sz Unsigned) v2 (Tint sz Unsigned) = Some ? res →
804  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
805              match modulus_u ? i1 i2 with
806              [ Some q ⇒  res =  (Vint sz' q)
807              | None ⇒ False ].
808#sz *
809[ | #sz' #i' | | #p' ]
810#v2 #res
811whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
812>type_eq_dec_true normalize nodelta
813#H destruct
814cases v2 in H; normalize nodelta
815[ | #sz2' #i2' | | #p2' ]
816#Heq destruct
817%{sz'}
818lapply Heq -Heq
819cases sz' in i'; #i' 
820whd in match (intsize_eq_elim ???????);
821cases sz2' in i2'; #i2' normalize nodelta
822whd in match (option_map ????); #Hdiv destruct
823%{i'} %{i2'} @conj try @conj try @conj try @refl
824cases (modulus_u ???) in Hdiv;
825[ 2,4,6: #bv ] normalize #H destruct (H) try @refl
826qed.
827
828lemma sem_and_inversion :
829  ∀v1,v2,res.
830  sem_and v1 v2 = Some ? res →
831  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
832              res = Vint sz' (conjunction_bv ? i1 i2).
833*
834[ | #sz' #i' | | #p' ]
835#v2 #res
836whd in ⊢ ((??%?) → ?);
837#H destruct
838cases v2 in H; normalize nodelta
839[ | #sz2' #i2' | | #p2' ]
840#Heq destruct
841%{sz'}
842lapply Heq -Heq
843cases sz' in i'; #i' 
844whd in match (intsize_eq_elim ???????);
845cases sz2' in i2'; #i2' normalize nodelta
846#H destruct
847%{i'} %{i2'} @conj try @conj try @conj try @refl
848qed.
849
850lemma sem_or_inversion :
851  ∀v1,v2,res.
852  sem_or v1 v2 = Some ? res →
853  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
854              res = Vint sz' (inclusive_disjunction_bv ? i1 i2).
855*
856[ | #sz' #i' | | #p' ]
857#v2 #res
858whd in ⊢ ((??%?) → ?);
859#H destruct
860cases v2 in H; normalize nodelta
861[ | #sz2' #i2' | | #p2' ]
862#Heq destruct
863%{sz'}
864lapply Heq -Heq
865cases sz' in i'; #i' 
866whd in match (intsize_eq_elim ???????);
867cases sz2' in i2'; #i2' normalize nodelta
868#H destruct
869%{i'} %{i2'} @conj try @conj try @conj try @refl
870qed.
871
872lemma sem_xor_inversion :
873  ∀v1,v2,res.
874  sem_xor v1 v2 = Some ? res →
875  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
876              res = Vint sz' (exclusive_disjunction_bv ? i1 i2).
877*
878[ | #sz' #i' | | #p' ]
879#v2 #res
880whd in ⊢ ((??%?) → ?);
881#H destruct
882cases v2 in H; normalize nodelta
883[ | #sz2' #i2' | | #p2' ]
884#Heq destruct
885%{sz'}
886lapply Heq -Heq
887cases sz' in i'; #i' 
888whd in match (intsize_eq_elim ???????);
889cases sz2' in i2'; #i2' normalize nodelta
890#H destruct
891%{i'} %{i2'} @conj try @conj try @conj try @refl
892qed.
893
894lemma sem_shl_inversion :
895  ∀v1,v2,res.
896  sem_shl v1 v2 = Some ? res →
897  ∃sz1,sz2,i1,i2.
898              v1 =  Vint sz1 i1 ∧ v2 = Vint sz2 i2 ∧
899              res = Vint sz1 (shift_left bool (bitsize_of_intsize sz1)
900                                  (nat_of_bitvector (bitsize_of_intsize sz2) i2) i1 false) ∧
901              lt_u (bitsize_of_intsize sz2) i2
902                   (bitvector_of_nat (bitsize_of_intsize sz2) (bitsize_of_intsize sz1)) = true.
903*
904[ | #sz' #i' | | #p' ]
905#v2 #res
906whd in ⊢ ((??%?) → ?);
907#H destruct
908cases v2 in H; normalize nodelta
909[ | #sz2' #i2' | | #p2' ]
910#Heq destruct
911%{sz'} %{sz2'}
912lapply (if_opt_inversion ???? Heq) * #Hlt_u #Hres
913%{i'} %{i2'}
914>Hlt_u destruct (Hres) @conj try @conj try @conj try @refl
915qed.
916
917lemma sem_shr_inversion :
918  ∀v1,v2,sz,sg,res.
919  sem_shr v1 (Tint sz sg) v2 (Tint sz sg) = Some ? res →
920  ∃sz1,sz2,i1,i2.
921              v1 =  Vint sz1 i1 ∧ v2 = Vint sz2 i2 ∧
922              lt_u (bitsize_of_intsize sz2) i2
923                   (bitvector_of_nat (bitsize_of_intsize sz2) (bitsize_of_intsize sz1)) = true ∧
924              match sg with
925              [ Signed ⇒
926                 res =
927                   (Vint sz1
928                    (shift_right bool (7+pred_size_intsize sz1*8)
929                     (nat_of_bitvector (bitsize_of_intsize sz2) i2) i1
930                     (head' bool (7+pred_size_intsize sz1*8) i1)))               
931              | Unsigned ⇒
932                 res =
933                   (Vint sz1
934                    (shift_right bool (7+pred_size_intsize sz1*8)
935                     (nat_of_bitvector (bitsize_of_intsize sz2) i2) i1 false))
936              ].
937*
938[ | #sz' #i' | | #p' ]
939#v2 #sz * #res
940whd in ⊢ ((??%?) → ?);
941whd in match (classify_aop ??);
942>type_eq_dec_true normalize nodelta
943#H destruct
944cases v2 in H; normalize nodelta
945[ | #sz2' #i2' | | #p2'
946| | #sz2' #i2' | | #p2' ]
947#Heq destruct
948%{sz'} %{sz2'}
949lapply (if_opt_inversion ???? Heq) * #Hlt_u #Hres
950%{i'} %{i2'}
951>Hlt_u destruct (Hres) @conj try @conj try @conj try @refl
952qed.
953
954lemma complete_cmp_inversion :
955  ∀ty:type.
956  ∀e:expr (ASTint I8 Unsigned).
957  ∀r:expr (typ_of_type ty).
958   complete_cmp ty e = return r →
959   ∃sz,sg. ty = Tint sz sg ∧
960           r ≃ Op1 (ASTint I8 Unsigned) (ASTint sz sg) (Ocastint I8 Unsigned sz sg) e.
961*
962[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
963| #structname #fieldspec | #unionname #fieldspec | #id ]
964#e whd in match (typ_of_type ?);
965#r whd in ⊢ ((??%%) → ?);
966#H destruct
967%{sz} %{sg} @conj try @refl @refl_jmeq
968qed.
969
970
971lemma sem_cmp_int_inversion :
972  ∀v1,v2,sz,sg,op,m,res.
973   sem_cmp op v1 (Tint sz sg) v2 (Tint sz sg) m = Some ? res →
974   ∃sz,i1,i2. v1 = Vint sz i1 ∧
975              v2 = Vint sz i2 ∧
976    match sg with
977    [ Unsigned ⇒ of_bool (cmpu_int ? op i1 i2) = res
978    | Signed   ⇒ of_bool (cmp_int ? op i1 i2) = res
979    ].
980#v1 #v2 #sz0 #sg #op * #contents #next #Hnext #res
981whd in ⊢ ((??%?) → ?);
982whd in match (classify_cmp ??); >type_eq_dec_true normalize nodelta
983cases v1
984[ | #sz #i | | #p ] normalize nodelta
985#H destruct
986cases v2 in H;
987[ | #sz' #i' | | #p' ] normalize nodelta
988#H destruct lapply H -H
989cases sz in i; #i
990cases sz' in i'; #i' cases sg normalize nodelta
991whd in match (intsize_eq_elim ???????); #H destruct
992[ 1,2: %{I8}
993| 3,4: %{I16}
994| 5,6: %{I32} ] 
995%{i} %{i'} @conj try @conj try @refl
996qed.
997
998lemma typ_of_ptr_type : ∀ty',n. typ_of_type (ptr_type ty' n) = ASTptr.
999#ty' * // qed.
1000
1001lemma sem_cmp_ptr_inversion :
1002  ∀v1,v2,ty',n,op,m,res.
1003   sem_cmp op v1 (ptr_type ty' n) v2 (ptr_type ty' n) m = Some ? res →
1004   (∃p1,p2. v1 = Vptr p1 ∧ v2 = Vptr p2 ∧
1005                 valid_pointer m p1 = true ∧
1006                 valid_pointer m p2 = true ∧
1007                 (if eq_block (pblock p1) (pblock p2)
1008                  then Some ? (of_bool (cmp_offset op (poff p1) (poff p2)))
1009                  else sem_cmp_mismatch op) = Some ? res) ∨
1010   (∃p1. v1 = Vptr p1 ∧ v2 = Vnull ∧ sem_cmp_mismatch op = Some ? res) ∨                 
1011   (∃p2. v1 = Vnull ∧ v2 = Vptr p2 ∧ sem_cmp_mismatch op = Some ? res) ∨
1012   (v1 = Vnull ∧ v2 = Vnull ∧ sem_cmp_match op = Some ? res).
1013* [ | #sz #i | | #p ] normalize nodelta
1014#v2 #ty' #n #op
1015* #contents #nextblock #Hnextblock #res whd in ⊢ ((??%?) → ?);
1016whd in match (classify_cmp ??); cases n normalize nodelta
1017[ 2,4,6,8: #array_len ]
1018whd in match (ptr_type ty' ?);
1019whd in match (if_type_eq ?????);
1020>type_eq_dec_true normalize nodelta
1021#H destruct
1022cases v2 in H; normalize nodelta
1023[ | #sz' #i' | | #p'
1024| | #sz' #i' | | #p'
1025| | #sz' #i' | | #p'
1026| | #sz' #i' | | #p' ]
1027#H destruct
1028try /6 by or_introl, or_intror, ex_intro, conj/
1029[ 1: %1 %1 %2 %{p} @conj try @conj //
1030| 3: %1 %1 %2 %{p} @conj try @conj //
1031| *: %1 %1 %1 %{p} %{p'}
1032     cases (valid_pointer (mk_mem ???) p) in H; normalize nodelta
1033     cases (valid_pointer (mk_mem contents nextblock Hnextblock) p') normalize nodelta #H
1034     try @conj try @conj try @conj try @conj try @conj try @refl try @H
1035     destruct
1036] qed.
1037
1038lemma pointer_translation_eq_block :
1039  ∀E,p1,p2,p1',p2'.
1040  pointer_translation p1 E = Some ? p1' →
1041  pointer_translation p2 E = Some ? p2' →
1042  eq_block (pblock p1) (pblock p2) = true →
1043  eq_block (pblock p1') (pblock p2') = true.
1044#E * #b1 #o1 * #b2 #o2 * #b1' #o1' * #b2' #o2'
1045#H1 #H2 #Heq_block
1046lapply (eq_block_to_refl … Heq_block) #H destruct (H)
1047lapply H1 lapply H2 -H1 -H2
1048whd in ⊢ ((??%?) → (??%?) → ?);
1049cases (E b2) normalize nodelta
1050[ #Habsurd destruct ]
1051* #bx #ox normalize nodelta #Heq1 #Heq2 destruct
1052@eq_block_b_b
1053qed.
1054
1055lemma pointer_translation_cmp_offset :
1056  ∀E,p1,p2,p1',p2',op.
1057  pblock p1 = pblock p2 →
1058  pointer_translation p1 E = Some ? p1' →
1059  pointer_translation p2 E = Some ? p2' →
1060  cmp_offset op (poff p1) (poff p2) = cmp_offset op (poff p1') (poff p2').
1061#E * #b1 #o1 * #b2 #o2 * #b1' #o1' * #b2' #o2' #op #Heq destruct
1062whd in ⊢ ((??%?) → (??%?) → ?);
1063cases (E b2) normalize nodelta
1064[ #H destruct ]
1065* #bx #ox normalize nodelta
1066#Heq1 #Heq2 destruct cases op
1067[ @sym_eq @eq_offset_translation
1068| @sym_eq @neq_offset_translation
1069| @cthulhu (* !!!! TODO !!!! *)
1070| @cthulhu (* !!!! TODO !!!! *)
1071| @cthulhu (* !!!! TODO !!!! *)
1072| @cthulhu (* !!!! TODO !!!! *)
1073] qed.
1074
1075(* The two following lemmas are just noise. *)
1076
1077lemma expr_vars_fix_ptr_type :
1078  ∀ty',optlen.
1079  ∀e:expr (typ_of_type (ptr_type ty' optlen)).
1080  ∀P.
1081   expr_vars ASTptr (fix_ptr_type ty' optlen e) P →
1082   expr_vars
1083    (typ_of_type
1084        match optlen 
1085        in option 
1086        return λ_:(option ℕ).type with 
1087        [None⇒Tpointer ty'
1088        |Some (n':ℕ)⇒ Tarray ty' n']) e P.
1089#ty' * normalize
1090[ 2: #n ]
1091#e #P
1092@expr_vars_mp //
1093qed.
1094
1095lemma eval_expr_rewrite_aux :
1096  ∀genv.
1097  ∀optlen.
1098  ∀ty'.
1099  ∀e.
1100  ∀cm_env.
1101  ∀H.
1102  ∀sp.
1103  ∀m.
1104  ∀res.
1105  (eval_expr genv
1106             (typ_of_type
1107                 match optlen in option return λ_:(option ℕ).type with 
1108                 [None⇒Tpointer ty'|Some (n':ℕ)⇒Tarray ty' n'])
1109             e cm_env (expr_vars_fix_ptr_type ty' optlen e (λid:ident.λty0:typ.present SymbolTag val cm_env id) H) sp m) = OK ? res →
1110   eval_expr genv ASTptr (fix_ptr_type ty' optlen e) cm_env H sp m = OK ? res.
1111#genv * [ 2: #n ] normalize nodelta
1112#ty' normalize in match (typ_of_type ?);
1113#e #cm_env whd in match (fix_ptr_type ???);
1114#H #sp #m #res #H @H
1115qed.
1116
1117
1118(* TODOs : there are some glitches between clight and cminor :
1119 * 1) some issues with shortcut and/or: the clight code returns a 32 bit constant
1120      in the shortcut case, the cminor code returns directly the outcome of the
1121      evaluated expr, with a possibly different size.
1122   2) another glitch is for the integer/pointer additions: Clight always performs
1123      a sign extension on i in expressions (ptr + i) whereas Cminor case splits on
1124      the sign of i, producing either a sign extension or a zero extension.
1125   3) something similar to 1) happens for binary comparison operators. Clight generates
1126      systematically a 32 bit value for the outcome of the comparison and lives with it,
1127      but toCminor actually generates something 8 bit and casts it back to the context type.
1128   4) we need some proof that we don't blow the stack during the transformation. Otherwise,
1129      a problem appears when we prove semantics preservation for pointer < comparison
1130      (we might wrap up the rhs and end SNAFU).
1131 *)
1132lemma eval_expr_sim :
1133  ∀(inv:clight_cminor_inv).
1134  ∀(f:function).
1135  ∀(vars:var_types).
1136  ∀stacksize.
1137  characterise_vars (globals inv) f = 〈vars, stacksize〉 →
1138  ∀(cl_env:cl_env).
1139  (∃m,m'. exec_alloc_variables empty_env m (fn_params f @ fn_vars f) = 〈cl_env,m'〉) →
1140  ∀(cl_m:mem).
1141  ∀(cm_env:cm_env).
1142  ∀(sp:block).
1143  ∀(cm_m:mem).
1144  ∀E:embedding.
1145  ∀minj:memory_inj E cl_m cm_m.
1146  memory_matching E cl_m cm_m cl_env cm_env inv sp vars →
1147  (* clight expr to cminor expr *)
1148  (∀(e:expr).
1149   ∀(e':CMexpr (typ_of_type (typeof e))).
1150   ∀Hexpr_vars.
1151   translate_expr vars e = OK ? («e', Hexpr_vars») →
1152   ∀cl_val,trace,Hyp_present.
1153   exec_expr (ge_cl … inv) cl_env cl_m e = OK ? 〈cl_val, trace〉 →
1154   ∃cm_val. eval_expr (ge_cm inv) (typ_of_type (typeof e)) e' cm_env Hyp_present sp cm_m = OK ? 〈trace, cm_val〉 ∧
1155            value_eq E cl_val cm_val) ∧
1156   (* clight /lvalue/ to cminor /expr/ *)
1157  (∀ed,ty.
1158   ∀(e':CMexpr ASTptr).
1159   ∀Hexpr_vars.
1160   translate_addr vars (Expr ed ty) = OK ? («e', Hexpr_vars») →
1161   ∀cl_blo,cl_off,trace,Hyp_present.
1162   exec_lvalue' (ge_cl … inv) cl_env cl_m ed ty = OK ? 〈cl_blo, cl_off, trace〉 →
1163   ∃cm_val. eval_expr (ge_cm inv) ASTptr e' cm_env Hyp_present sp cm_m = OK ? 〈trace, cm_val〉 ∧
1164            value_eq E (Vptr (mk_pointer cl_blo cl_off)) cm_val).
1165#inv #f #vars #stacksize #Hcharacterise #cl_env #Hexec_alloc #cl_m #cm_env #sp #cm_m #E #Hinj #Hlocal_matching
1166@expr_lvalue_ind_combined
1167[ 7: (* binary ops *)
1168     #ty
1169     #op #e1 #e2
1170     #Hind1 #Hind2 #e' #Hexpr_vars #Htranslate
1171     cases (bind_inversion ????? Htranslate) -Htranslate
1172     * #lhs #Hexpr_vars_lhs * #Htranslate_lhs #Htranslate
1173     cases (bind_inversion ????? Htranslate) -Htranslate
1174     * #rhs #Hexpr_vars_rhs * #Htranslate_rhs
1175     whd in ⊢ ((??%?) → ?);
1176     #Htranslate_binop
1177     cases (bind_as_inversion ????? Htranslate_binop) -Htranslate_binop
1178     #translated_binop * #Htranslated_binop whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1179     #cl_val #trace #Hyp_present #Hexec
1180     (* dump all the useless stuff after the turnstyle, in order to perform rewrites and so on. *)
1181     lapply (Hind1 lhs Hexpr_vars_lhs Htranslate_lhs) -Hind1
1182     lapply (Hind2 rhs Hexpr_vars_rhs Htranslate_rhs) -Hind2
1183     lapply Hyp_present -Hyp_present
1184     lapply Htranslate_lhs -Htranslate_lhs
1185     lapply Htranslate_rhs -Htranslate_rhs
1186     lapply Hexpr_vars_lhs -Hexpr_vars_lhs
1187     lapply Hexpr_vars_rhs -Hexpr_vars_rhs
1188     lapply Hexec -Hexec
1189     lapply Htranslated_binop -Htranslated_binop
1190     lapply rhs -rhs lapply lhs -lhs
1191     (* end of dump *)
1192     cases op
1193     whd in ⊢ (? → ? → (??%?) → ?);
1194     [ 1: (* add *)
1195       lapply (classify_add_inversion (typeof e1) (typeof e2))
1196       * [ 2: #Hclassify >Hclassify normalize nodelta #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
1197       (* trying to factorise as much stuff as possible ... *)
1198       lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2 whd in match (typeof ?); #e'
1199       * [ 1: * ]
1200       [ 1: * #sz * #sg * *
1201       | 2: * #optlen * #ty' * #sz * #sg * *
1202       | 3: * #optlen * #sz * #sg * #ty' * * ]
1203       whd in match (typeof ?) in ⊢ (% → % → ?);
1204       #Htypeof_e1 #Htypeof_e2
1205       >Htypeof_e1 >Htypeof_e2
1206       #Hclassify
1207       lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify
1208       normalize nodelta
1209       whd in match (typeof ?) in ⊢ (% → % → %);
1210       whd in match (typ_of_type (Tint ??));
1211       #lhs #rhs #Htyp_should_eq
1212       [ 1:   cases (typ_should_eq_inversion (ASTint sz sg) (typ_of_type ty) … Htyp_should_eq)
1213       | 2,3: cases (typ_should_eq_inversion ASTptr (typ_of_type ty) … Htyp_should_eq) ]
1214       -Htyp_should_eq
1215       #Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') -Heq_e' #Heq_e'
1216       <Heq_e' -Heq_e'
1217       #Hexec
1218       #Hexpr_vars_rhs #Hexpr_vars_lhs
1219       #Htranslate_rhs #Htranslate_lhs
1220       * [ #Hyp_present_lhs #Hyp_present_rhs
1221         | #Hyp_present_lhs * #Hyp_present_rhs #Hyp_present_cst
1222         | #Hyp_present_rhs * #Hyp_present_lhs #Hyp_present_cst  ]
1223       whd in match (typeof ?);
1224       #Hind_rhs #Hind_lhs
1225       cases (bind_inversion ????? Hexec) -Hexec
1226       * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
1227       cases (bind_inversion ????? Hexec) -Hexec
1228       * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
1229       cases (bind_inversion ????? Hexec) -Hexec
1230       #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1231       lapply (opt_to_res_inversion ???? Hsem) -Hsem
1232       whd in match (typeof ?); whd in match (typeof ?);
1233       #Hsem_binary
1234       [ 1,2: lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
1235       | 3: lapply (Hind_rhs … (expr_vars_fix_ptr_type … Hyp_present_rhs) Hexec_rhs) ]
1236       * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
1237       [ 1,3: lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
1238       | 2: lapply (Hind_lhs … (expr_vars_fix_ptr_type … Hyp_present_lhs) Hexec_lhs) ]
1239       * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
1240       whd in match (eval_expr ???????);
1241       whd in match (proj1 ???);
1242       [ 3: lapply (eval_expr_rewrite_aux … Heval_lhs) -Heval_lhs #Heval_lhs ]
1243       [ 1,2: >Heval_lhs normalize nodelta
1244              whd in match (eval_expr ???????);
1245              whd in match (eval_expr ???????);
1246              >Heval_rhs normalize nodelta
1247              whd in match (m_bind ?????);
1248       | 3: >(eval_expr_rewrite_aux … Heval_rhs) normalize nodelta
1249            whd in match (eval_expr ???????);
1250            whd in match (eval_expr ???????);
1251            >Heval_lhs normalize nodelta
1252       ]
1253       whd in match (proj1 ???); whd in match (proj2 ???);
1254       [ 2: (* standard int/int addition. *)
1255            whd in match (eval_binop ???????);
1256            whd in Hsem_binary:(??%?);
1257            lapply (add_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
1258            * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
1259            cases (sem_add_ii_inversion … Hsem_binary_translated)
1260            #cm_vsz * #cm_lhs_v * #cm_rhs_v * *
1261            #Hcm_lhs #Hcm_rhs #Hcm_val
1262            destruct (Hcm_lhs) destruct (Hcm_rhs) normalize nodelta
1263            >intsize_eq_elim_true normalize nodelta
1264            %{(Vint cm_vsz (addition_n (bitsize_of_intsize cm_vsz) cm_lhs_v cm_rhs_v))}
1265            @conj try @refl lapply Hsem_binary_translated
1266            whd in ⊢ ((??%?) → ?); normalize nodelta normalize in match (classify_add ??);
1267            >inttyp_eq_elim_true' normalize nodelta
1268            >intsize_eq_elim_true #H destruct (H) @Hvalue_eq_res
1269       | *: (* pointer/int int/pointer addition *)
1270            whd in Hsem_binary:(??%?);
1271            lapply (add_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
1272            * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
1273            [ 1: lapply (sem_add_pi_inversion … Hsem_binary_translated)
1274                 * #cm_vsz * #cm_rhs_v * #Hcm_rhs *
1275                 [ * #lhs_ptr * #Hcm_lhs_ptr #Hcm_val_shptr
1276                 | * * #lhs_null #Hcm_rhs_zero #Hcm_val_null ]
1277                 destruct
1278                 whd in match (eval_unop ????);
1279                 @(match sg
1280                   return λs. sg = s → ?
1281                   with
1282                   [ Unsigned ⇒ λHsg. ?
1283                   | Signed ⇒ λHsg. ?
1284                   ] (refl ??)) normalize nodelta
1285                   whd in match (eval_binop ???????);
1286                   whd in match (m_bind ?????);
1287                   [ 1: %{(Vptr (shift_pointer (bitsize_of_intsize I16) lhs_ptr
1288                                   (short_multiplication (bitsize_of_intsize I16)
1289                                   (sign_ext (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16) cm_rhs_v)
1290                                   (repr I16 (sizeof ty')))))}
1291                   | 2: %{(Vptr (shift_pointer (bitsize_of_intsize I16) lhs_ptr
1292                                   (short_multiplication (bitsize_of_intsize I16)
1293                                   (zero_ext (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16) cm_rhs_v)
1294                                   (repr I16 (sizeof ty')))))} ]
1295                   [ 1,2: @conj whd in match (E0); whd in match (Eapp trace_rhs ?);
1296                          >(append_nil … trace_rhs) try @refl
1297                          @(value_eq_triangle_diagram … Hvalue_eq_res)
1298                          whd in match (shift_pointer_n ????);
1299                          whd in match (shift_offset_n ????);
1300                          >commutative_short_multiplication
1301                          whd in match (shift_pointer ???);
1302                          whd in match (shift_offset ???);
1303                          @cthulhu (* cf problem description at top of lemma. *)
1304                   | 3: >(sign_ext_zero (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16))
1305                        >(short_multiplication_zero 16  (repr I16 (sizeof ty')))
1306                        >(eq_bv_true … (zero 16)) normalize nodelta %{Vnull} @conj try assumption
1307                        normalize >append_nil try @refl
1308                   | 4: >(zero_ext_zero (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16))
1309                        >(short_multiplication_zero 16 (repr I16 (sizeof ty')))
1310                        >(eq_bv_true … (zero 16)) normalize nodelta %{Vnull} @conj try assumption
1311                        normalize >append_nil try @refl ]
1312            | 2: (* integer/pointer add: symmetric to the case above. *) @cthulhu ]
1313       ]
1314     | 2: (* subtraction cases: identical to add *) @cthulhu
1315     | 3: (* mul *)
1316       lapply (classify_aop_inversion (typeof e1) (typeof e2)) *
1317       [ 2,4: #Hclassify >Hclassify normalize nodelta
1318            #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
1319       lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2
1320       whd in match (typeof ?); #e'
1321       * #sz * #sg * *
1322       whd in match (typeof ?) in ⊢ (% → % → ?);
1323       #Htypeof_e1 #Htypeof_e2
1324       >Htypeof_e1 >Htypeof_e2
1325       whd in match (typeof ?) in ⊢ (% → % → % → ?);
1326       #Hclassify
1327       lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify
1328       normalize nodelta
1329       whd in match (typ_of_type (Tint ??));
1330       #lhs #rhs #Htyp_should_eq
1331       cases (typ_should_eq_inversion (ASTint sz sg) (typ_of_type ty) … Htyp_should_eq)
1332       -Htyp_should_eq
1333       #Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') -Heq_e' #Heq_e'
1334       <Heq_e' -Heq_e'
1335       #Hexec
1336       #Hexpr_vars_rhs #Hexpr_vars_lhs
1337       #Htranslate_rhs #Htranslate_lhs
1338       * #Hyp_present_lhs #Hyp_present_rhs
1339       #Hind_rhs #Hind_lhs
1340       cases (bind_inversion ????? Hexec) -Hexec
1341       * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
1342       cases (bind_inversion ????? Hexec) -Hexec
1343       * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
1344       cases (bind_inversion ????? Hexec) -Hexec
1345       #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1346       lapply (opt_to_res_inversion ???? Hsem) -Hsem
1347       whd in match (typeof ?); whd in match (typeof ?);
1348       #Hsem_binary
1349       lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
1350       * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
1351       lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
1352       * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
1353       whd in match (eval_expr ???????);
1354       whd in match (proj1 ???);
1355       >Heval_lhs normalize nodelta
1356       >Heval_rhs normalize nodelta
1357       whd in match (m_bind ?????);
1358       whd in match (eval_binop ???????);
1359       whd in Hsem_binary:(??%?);
1360       lapply (mul_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
1361       * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
1362       cases (sem_mul_inversion … Hsem_binary)
1363       #cm_vsz * #cm_lhs_v * #cm_rhs_v * *
1364       #Hcm_lhs #Hcm_rhs #Hcm_val
1365       destruct (Hcm_lhs) destruct (Hcm_rhs) normalize nodelta
1366       >(value_eq_int_inversion … Hvalue_eq_lhs) normalize nodelta
1367       >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta
1368       >intsize_eq_elim_true normalize nodelta
1369       %{(Vint cm_vsz (short_multiplication (bitsize_of_intsize cm_vsz) cm_lhs_v cm_rhs_v))}
1370       @conj try @refl
1371       whd in Hsem_binary:(??%?);     
1372       whd in match (classify_aop ??) in Hsem_binary:(??%?);
1373       >type_eq_dec_true in Hsem_binary; normalize nodelta
1374       >intsize_eq_elim_true #Heq destruct (Heq)
1375       %2
1376     | 4,5: (* div *)
1377       lapply (classify_aop_inversion (typeof e1) (typeof e2)) *
1378       [ 2,4: #Hclassify >Hclassify normalize nodelta
1379            #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
1380       lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2
1381       whd in match (typeof ?); #e'
1382       * #sz * * * *
1383       whd in match (typeof ?) in ⊢ (% → % → ?);
1384       #Htypeof_e1 #Htypeof_e2
1385       >Htypeof_e1 >Htypeof_e2
1386       whd in match (typeof ?) in ⊢ (% → % → % → ?);
1387       #Hclassify
1388       lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify
1389       normalize nodelta
1390       whd in match (typ_of_type (Tint ??));
1391       #lhs #rhs #Htyp_should_eq
1392       [ 1,3: cases (typ_should_eq_inversion (ASTint sz Signed) (typ_of_type ty) … Htyp_should_eq)
1393       | 2,4: cases (typ_should_eq_inversion (ASTint sz Unsigned) (typ_of_type ty) … Htyp_should_eq) ]
1394       -Htyp_should_eq
1395       #Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') -Heq_e' #Heq_e'
1396       <Heq_e' -Heq_e'
1397       #Hexec
1398       #Hexpr_vars_rhs #Hexpr_vars_lhs
1399       #Htranslate_rhs #Htranslate_lhs
1400       * #Hyp_present_lhs #Hyp_present_rhs
1401       #Hind_rhs #Hind_lhs
1402       cases (bind_inversion ????? Hexec) -Hexec
1403       * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
1404       cases (bind_inversion ????? Hexec) -Hexec
1405       * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
1406       cases (bind_inversion ????? Hexec) -Hexec
1407       #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1408       lapply (opt_to_res_inversion ???? Hsem) -Hsem
1409       whd in match (typeof ?); whd in match (typeof ?);
1410       #Hsem_binary
1411       lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
1412       * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
1413       lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
1414       * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
1415       whd in match (eval_expr ???????);
1416       whd in match (proj1 ???);
1417       >Heval_lhs normalize nodelta
1418       >Heval_rhs normalize nodelta
1419       whd in match (m_bind ?????);
1420       whd in match (eval_binop ???????);
1421       whd in Hsem_binary:(??%?);
1422       [ 1,3: (* div*)
1423          lapply (div_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
1424          * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
1425          [ cases (sem_div_inversion_s … Hsem_binary)
1426          | cases (sem_div_inversion_u … Hsem_binary) ]
1427       | 2,4: (* mod *)
1428          lapply (mod_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
1429          * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
1430          [ cases (sem_mod_inversion_s … Hsem_binary)
1431          | cases (sem_mod_inversion_u … Hsem_binary) ]
1432       ]
1433       #cm_vsz * #cm_lhs_v * #cm_rhs_v * *
1434       #Hcm_lhs #Hcm_rhs #Hcm_val
1435       destruct (Hcm_lhs) destruct (Hcm_rhs) normalize nodelta
1436       >(value_eq_int_inversion … Hvalue_eq_lhs) normalize nodelta
1437       >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta
1438       >intsize_eq_elim_true normalize nodelta
1439       [ cases (division_s ???) in Hcm_val;
1440       | cases (division_u ???) in Hcm_val;
1441       | cases (modulus_s ???) in Hcm_val;
1442       | cases (modulus_u ???) in Hcm_val; ]
1443       normalize nodelta
1444       [ 1,3,5,7: @False_ind ]
1445       #i #Hcl_val destruct (Hcl_val) %{(Vint cm_vsz i)} @conj try @refl %2
1446     | 6,7,8: (* and,or,xor *)
1447       lapply (classify_aop_inversion (typeof e1) (typeof e2)) *
1448       [ 2,4,6: #Hclassify >Hclassify normalize nodelta
1449            #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
1450       lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2
1451       whd in match (typeof ?); #e'
1452       * #sz * #sg * *
1453       whd in match (typeof ?) in ⊢ (% → % → ?);
1454       #Htypeof_e1 #Htypeof_e2
1455       >Htypeof_e1 >Htypeof_e2
1456       whd in match (typeof ?) in ⊢ (% → % → % → ?);
1457       #Hclassify
1458       lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify
1459       normalize nodelta
1460       whd in match (typ_of_type (Tint ??));
1461       #lhs #rhs #Htyp_should_eq
1462       cases (typ_should_eq_inversion (ASTint sz sg) (typ_of_type ty) … Htyp_should_eq)
1463       -Htyp_should_eq
1464       #Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') -Heq_e' #Heq_e'
1465       <Heq_e' -Heq_e'
1466       #Hexec
1467       #Hexpr_vars_rhs #Hexpr_vars_lhs
1468       #Htranslate_rhs #Htranslate_lhs
1469       * #Hyp_present_lhs #Hyp_present_rhs
1470       #Hind_rhs #Hind_lhs
1471       cases (bind_inversion ????? Hexec) -Hexec
1472       * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
1473       cases (bind_inversion ????? Hexec) -Hexec
1474       * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
1475       cases (bind_inversion ????? Hexec) -Hexec
1476       #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1477       lapply (opt_to_res_inversion ???? Hsem) -Hsem
1478       whd in match (typeof ?); whd in match (typeof ?);
1479       #Hsem_binary
1480       lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
1481       * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
1482       lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
1483       * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
1484       whd in match (eval_expr ???????);
1485       whd in match (proj1 ???);
1486       >Heval_lhs normalize nodelta
1487       >Heval_rhs normalize nodelta
1488       whd in match (m_bind ?????);
1489       whd in match (eval_binop ???????);
1490       whd in Hsem_binary:(??%?);
1491       [ 1: (* and *)
1492          lapply (and_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
1493           * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
1494          cases (sem_and_inversion … Hsem_binary)
1495       | 2: (* or *)
1496          lapply (or_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
1497           * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
1498          cases (sem_or_inversion … Hsem_binary)
1499       | 3: (* xor *)
1500          lapply (xor_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
1501           * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
1502          cases (sem_xor_inversion … Hsem_binary)
1503       ]
1504       #cm_vsz * #cm_lhs_v * #cm_rhs_v * *
1505       #Hcm_lhs #Hcm_rhs #Hcm_val
1506       destruct (Hcm_lhs) destruct (Hcm_rhs) normalize nodelta
1507       >(value_eq_int_inversion … Hvalue_eq_lhs) normalize nodelta
1508       >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta
1509       >intsize_eq_elim_true normalize nodelta
1510       [ 1: %{(Vint cm_vsz (conjunction_bv … cm_lhs_v cm_rhs_v))}
1511       | 2: %{(Vint cm_vsz (inclusive_disjunction_bv … cm_lhs_v cm_rhs_v))}
1512       | 3: %{(Vint cm_vsz (exclusive_disjunction_bv … cm_lhs_v cm_rhs_v))}
1513       ]
1514       @conj try @refl >Hcm_val %2
1515     | 9,10: (* shl, shr *)
1516       lapply (classify_aop_inversion (typeof e1) (typeof e2)) *
1517       [ 2,4: #Hclassify >Hclassify normalize nodelta
1518            #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
1519       lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2
1520       whd in match (typeof ?); #e'
1521       * #sz * * * *
1522       whd in match (typeof ?) in ⊢ (% → % → ?);
1523       #Htypeof_e1 #Htypeof_e2
1524       >Htypeof_e1 >Htypeof_e2
1525       whd in match (typeof ?) in ⊢ (% → % → % → ?);
1526       #Hclassify
1527       lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify
1528       normalize nodelta
1529       whd in match (typ_of_type (Tint ??));
1530       #lhs #rhs #Htyp_should_eq
1531       [ 1,3: cases (typ_should_eq_inversion (ASTint sz Signed) (typ_of_type ty) … Htyp_should_eq)
1532       | 2,4: cases (typ_should_eq_inversion (ASTint sz Unsigned) (typ_of_type ty) … Htyp_should_eq) ]
1533       -Htyp_should_eq
1534       #Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') -Heq_e' #Heq_e'
1535       <Heq_e' -Heq_e'
1536       #Hexec
1537       #Hexpr_vars_rhs #Hexpr_vars_lhs
1538       #Htranslate_rhs #Htranslate_lhs
1539       * #Hyp_present_lhs #Hyp_present_rhs
1540       #Hind_rhs #Hind_lhs
1541       cases (bind_inversion ????? Hexec) -Hexec
1542       * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
1543       cases (bind_inversion ????? Hexec) -Hexec
1544       * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
1545       cases (bind_inversion ????? Hexec) -Hexec
1546       #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1547       lapply (opt_to_res_inversion ???? Hsem) -Hsem
1548       whd in match (typeof ?); whd in match (typeof ?);
1549       #Hsem_binary
1550       lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
1551       * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
1552       lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
1553       * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
1554       whd in match (eval_expr ???????);
1555       whd in match (proj1 ???);
1556       >Heval_lhs normalize nodelta
1557       >Heval_rhs normalize nodelta
1558       whd in match (m_bind ?????);
1559       whd in match (eval_binop ???????);
1560       whd in Hsem_binary:(??%?);
1561       [ 1,3: (* shl *)
1562          lapply (shl_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
1563          * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
1564          cases (sem_shl_inversion … Hsem_binary)
1565          #sz1 * #sz2 * #lhs_i * #rhs_i * * *
1566          #Hcl_lhs #Hcl_rhs #Hcl_val #Hshift_ok
1567          destruct (Hcl_lhs Hcl_rhs)
1568          >(value_eq_int_inversion … Hvalue_eq_lhs)
1569          >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta
1570          >Hshift_ok normalize nodelta
1571          %{(Vint sz1
1572               (shift_left bool (bitsize_of_intsize sz1)
1573               (nat_of_bitvector (bitsize_of_intsize sz2) rhs_i) lhs_i false))}
1574          @conj try @refl >Hcl_val %2
1575       | *: (* shr, translated to mod /!\ *)     
1576          lapply (shr_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
1577          * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
1578          cases (sem_shr_inversion … Hsem_binary) normalize nodelta
1579          #sz1 * #sz2 * #lhs_i * #rhs_i * * *
1580          #Hcl_lhs #Hcl_rhs #Hshift_ok #Hcl_val
1581          destruct (Hcl_lhs Hcl_rhs)
1582          >(value_eq_int_inversion … Hvalue_eq_lhs)
1583          >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta
1584          >Hshift_ok normalize nodelta >Hcl_val
1585          /3 by ex_intro, conj, vint_eq/ ]
1586     | *: (* comparison operators *)
1587       lapply e' -e'
1588       cases e1 #ed1 #ety1
1589       cases e2 #ed2 #ety2
1590       whd in match (typeof ?) in ⊢ (% → % → % → %);
1591       #cm_expr whd in match (typeof ?);
1592       inversion (classify_cmp ety1 ety2)
1593       [ 3,6,9,12,15,18: #ety1' #ety2' #Hety1 #Hety2
1594            lapply (jmeq_to_eq ??? Hety1) #Hety1'
1595            lapply (jmeq_to_eq ??? Hety1) #Hety2'
1596            destruct #Hclassify >Hclassify normalize nodelta
1597            #cmexpr1 #cmexpr2
1598            whd in ⊢ ((???%) → ?);
1599            #Heq destruct (Heq)
1600       | 1,4,7,10,13,16:
1601            #sz #sg #Hety1 #Hety2 #Hclassify
1602            lapply (jmeq_to_eq ??? Hety1) #Hety1'
1603            lapply (jmeq_to_eq ??? Hety1) #Hety2' destruct
1604            >(jmeq_to_eq ??? Hclassify) -Hclassify normalize nodelta
1605            whd in match (typeof ?) in ⊢ (% → % → % → %);
1606            whd in match (typ_of_type ?) in ⊢ (% → % → ?);
1607            cases sg #cmexpr1 #cmexpr2 normalize nodelta
1608            #Hcast_to_bool #Hexec_expr
1609            cases (complete_cmp_inversion … Hcast_to_bool) -Hcast_to_bool
1610            #tysz * #tysg * #Htyis_int #Hcm_expr_aux
1611            destruct (Htyis_int)
1612            lapply (jmeq_to_eq ??? Hcm_expr_aux) #Hcm_expr -Hcm_expr_aux
1613            destruct (Hcm_expr)
1614            cases (bind_inversion ????? Hexec_expr) -Hexec_expr
1615            * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
1616            cases (bind_inversion ????? Hexec) -Hexec
1617            * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
1618            cases (bind_inversion ????? Hexec) -Hexec
1619            #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1620            lapply (opt_to_res_inversion ???? Hsem) -Hsem
1621            whd in match (typeof ?); whd in match (sem_binary_operation ??????);
1622            #Hsem_cmp lapply (sem_cmp_int_inversion … Hsem_cmp) -Hsem_cmp
1623            * #vsz * #lhs_val * #rhs_val * * #Hcl_lhs #Hcl_rhs normalize nodelta
1624            destruct (Hcl_lhs) destruct (Hcl_rhs)
1625            #Heq_bool whd in match (typ_of_type ?) in ⊢ (% → % → % → %);
1626            #Hexpr_vars_rhs #Hexpr_vars_lhs #Htranslate_rhs #Htranslate_lhs
1627            * #Hyp_present_lhs #Hyp_present_rhs
1628            #Hind_rhs #Hind_lhs                       
1629            lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
1630            * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
1631            lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
1632            * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
1633            whd in match (eval_expr ???????);
1634            whd in match (eval_expr ???????);
1635            >Heval_lhs normalize nodelta
1636            >Heval_rhs normalize nodelta
1637            whd in match (m_bind ?????);
1638            whd in match (eval_binop ???????);
1639            >(value_eq_int_inversion … Hvalue_eq_lhs)
1640            >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta
1641            >intsize_eq_elim_true normalize nodelta
1642            destruct (Heq_bool)
1643            whd in match (eval_unop ????);
1644            whd in match (opt_to_res ???);
1645            whd in match (m_bind ?????);
1646            (* finished modulo glitch in integer widths *)
1647            @cthulhu
1648       | *:
1649            #n #ty' #Hety1 #Hety2 #Hclassify
1650            lapply (jmeq_to_eq ??? Hety1) #Hety1'
1651            lapply (jmeq_to_eq ??? Hety1) #Hety2' destruct
1652            >(jmeq_to_eq ??? Hclassify) -Hclassify normalize nodelta
1653            whd in match (typeof ?) in ⊢ (% → % → % → %);
1654            #cmexpr1 #cmexpr2
1655            #Hcast_to_bool #Hexec_expr
1656            cases (complete_cmp_inversion … Hcast_to_bool) -Hcast_to_bool
1657            #tysz * #tysg * #Htyis_int #Hcm_expr_aux
1658            destruct (Htyis_int)
1659            lapply (jmeq_to_eq ??? Hcm_expr_aux) #Hcm_expr -Hcm_expr_aux
1660            destruct (Hcm_expr)
1661            cases (bind_inversion ????? Hexec_expr) -Hexec_expr
1662            * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
1663            cases (bind_inversion ????? Hexec) -Hexec
1664            * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
1665            cases (bind_inversion ????? Hexec) -Hexec
1666            #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1667            lapply (opt_to_res_inversion ???? Hsem) -Hsem
1668            whd in match (typeof ?); whd in match (sem_binary_operation ??????);
1669            #Hsem_cmp lapply (sem_cmp_ptr_inversion … Hsem_cmp) -Hsem_cmp
1670            *
1671            [ 2,4,6,8,10,12:
1672              * * #Hcl_lhs #Hcl_rhs #Hsem_cmp destruct
1673            | *: *
1674              [ 2,4,6,8,10,12:
1675                * #p2 * * #Hcl_lhs #Hcl_rhs #Hsem_cmp destruct
1676              | *: *
1677                [ 2,4,6,8,10,12:
1678                  * #p1 * * #Hcl_lhs #Hcl_rhs #Hsem_cmp destruct
1679                | *: * #p1 * #p2 * * * * #Hcl_lhs #Hcl_rhs #Hvalid_p1 #Hvalid_p2 #Heq_block_outcome destruct
1680            ] ] ]
1681           
1682(*            #Heq_bool whd in match (typ_of_type ?) in ⊢ (% → % → % → %); *)
1683            #Hexpr_vars_rhs #Hexpr_vars_lhs #Htranslate_rhs #Htranslate_lhs
1684            * #Hyp_present_lhs #Hyp_present_rhs
1685            #Hind_rhs #Hind_lhs
1686            lapply (Hind_rhs … (expr_vars_fix_ptr_type … Hyp_present_rhs) Hexec_rhs)
1687            * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
1688            lapply (Hind_lhs … (expr_vars_fix_ptr_type … Hyp_present_lhs) Hexec_lhs)
1689            * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
1690            whd in match (eval_expr ???????);
1691            whd in match (eval_expr ???????);
1692            >(eval_expr_rewrite_aux … Heval_lhs) normalize nodelta
1693            >(eval_expr_rewrite_aux … Heval_rhs) normalize nodelta
1694            whd in match (m_bind ?????);
1695            -Heval_lhs -Heval_rhs -Hyp_present_rhs -Hyp_present_lhs
1696            -Hexpr_vars_lhs -Hexpr_vars_rhs
1697            whd in match (eval_binop ???????);
1698            [ 1,2,3,4,5,6:
1699              whd in Hsem_cmp:(??%?); destruct (Hsem_cmp)           
1700              >(value_eq_null_inversion … Hvalue_eq_lhs)
1701              >(value_eq_null_inversion … Hvalue_eq_rhs) normalize nodelta
1702              whd in match (eval_unop ????);
1703              whd in match (opt_to_res ???);
1704              whd in match (m_bind ?????);
1705              (* same glitch with integer widths *)
1706              @cthulhu
1707            | 7,8,9,10,11,12:
1708              whd in Hsem_cmp:(??%?); destruct (Hsem_cmp)
1709              >(value_eq_null_inversion … Hvalue_eq_lhs) normalize nodelta
1710              cases (value_eq_ptr_inversion … Hvalue_eq_rhs) #p2'
1711              * #Hcm_rhs_val #Hpointer_translation >Hcm_rhs_val normalize nodelta
1712              whd in match (eval_unop ????);
1713              whd in match (opt_to_res ???);
1714              whd in match (m_bind ?????);
1715              (* same glitch with integer widths *)
1716              @cthulhu
1717            | 13,14,15,16,17,18:
1718              whd in Hsem_cmp:(??%?); destruct (Hsem_cmp)
1719              >(value_eq_null_inversion … Hvalue_eq_rhs) normalize nodelta
1720              cases (value_eq_ptr_inversion … Hvalue_eq_lhs) #p1'
1721              * #Hcm_lhs_val #Hpointer_translation >Hcm_lhs_val normalize nodelta
1722              whd in match (eval_unop ????);
1723              whd in match (opt_to_res ???);
1724              whd in match (m_bind ?????);
1725              (* same glitch with integer widths *)
1726              @cthulhu
1727            | *:
1728              cases (value_eq_ptr_inversion … Hvalue_eq_lhs) #p1' * #Hcm_lhs #Hptr_translation_lhs
1729              cases (value_eq_ptr_inversion … Hvalue_eq_rhs) #p2' * #Hcm_rhs #Hptr_translation_rhs
1730              destruct (Hcm_lhs Hcm_rhs) normalize nodelta
1731              -Hvalue_eq_lhs -Hvalue_eq_rhs -Hexec_lhs -Hexec_rhs
1732              >(mi_valid_pointers … Hinj … Hvalid_p1 … Hptr_translation_lhs)
1733              >(mi_valid_pointers … Hinj … Hvalid_p2 … Hptr_translation_rhs) normalize nodelta
1734              lapply Heq_block_outcome -Heq_block_outcome
1735              @(match eq_block (pblock p1) (pblock p2)
1736                return λb. (eq_block (pblock p1) (pblock p2)) = b → ?
1737                with
1738                [ true ⇒ λH. ?
1739                | false ⇒ λH. ?
1740                ] (refl ? (eq_block (pblock p1) (pblock p2)))) normalize nodelta
1741              [ 1,3,5,7,9,11:
1742                 (* block equality in the Clight memory *)
1743                 (* entails block equality in the Cminor memory *)
1744                 >(pointer_translation_eq_block … Hptr_translation_lhs Hptr_translation_rhs H) normalize nodelta                 
1745                 #Hsem_cmp whd in Hsem_cmp:(??%?); destruct (Hsem_cmp)
1746                 whd in match (eval_unop ????);
1747                 whd in match (opt_to_res ???);
1748                 whd in match (m_bind ?????);
1749                 (* TODO !!! In order to finish this, we need an invariant on the fact that we don't blow the stack during
1750                  * transformation *)
1751                 @cthulhu
1752              | *: (* TBF. In the case of block inequality, we will have to use the no_aliasing property of the memory injection. *)
1753                 @cthulhu
1754              ]
1755            ]
1756       ]
1757 ]
1758     
1759| 1: (* Integer constant *)
1760  #csz #ty cases ty
1761  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1762  | #structname #fieldspec | #unionname #fieldspec | #id ]
1763  #i whd in match (typeof ?); #e' #Hexpr_vars #Htranslate
1764  #val #trace #Hpresent #Hexec_cl
1765  whd in Htranslate:(??%?);
1766  [ 1,3,4,5,6,7,8: destruct ]
1767  cases (intsize_eq_elim_dec csz sz (λsz0.λsz0'.res (Σe0':expr (typ_of_type (Tint sz0' sg)).expr_vars (typ_of_type (Tint sz0' sg)) e0' (local_id vars))))
1768  [ 2: * #H_err #H_neq_sz
1769       lapply (H_err (OK ? «Cst (ASTint csz sg) (Ointconst csz sg i),I») (Error ? (msg TypeMismatch)))
1770       >Htranslate #Habsurd destruct (Habsurd) ]
1771  * #H_ok #Heq_sz lapply (H_ok (OK ? «Cst (ASTint csz sg) (Ointconst csz sg i),I») (Error ? (msg TypeMismatch)))
1772  destruct (Heq_sz)
1773  >Htranslate -Htranslate -H_ok #Heq destruct (Heq)
1774  whd in Hexec_cl:(??%?); >eq_intsize_true in Hexec_cl; normalize nodelta
1775  #Heq destruct (Heq) %{(Vint sz i)} @conj try @refl //
1776| 2: *
1777  [ #sz #i | #var_id | * #ed1 #ty1 | #e1 | #op #e1 | #op #e1 #e2 | #cast_ty #e1
1778  | #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
1779  try /2 by I/
1780  #ty whd in ⊢ (% → ?); #Hind
1781  whd in match (Plvalue ???);
1782  whd in match (typeof ?);
1783  #cm_expr #Hexpr_vars #Htranslate_expr #val #trace #Hyp_present #Hexec
1784  whd in Hexec:(??%?);
1785  whd in match (exec_lvalue' ?????) in Hexec:(??%?);
1786  cases (bind_inversion ????? Hexec) -Hexec * * #cl_b #cl_o #cl_t * #Hcl_success #Hcl_load_success
1787  whd in Hcl_success:(???%);
1788  [ 1: (* var case *)
1789       lapply Hcl_success -Hcl_success -Hind
1790       (* Peform case analysis on presence of variable in local Clight env.
1791        * if success, exec_expr/exec_lvalue tells us that it shoud be local. *)
1792       @(match lookup SymbolTag block cl_env var_id
1793         return λx.(lookup SymbolTag block cl_env var_id = x) → ?
1794         with
1795         [ None ⇒ λHcl_lookup. ?
1796         | Some loc ⇒ λHcl_lookup. ?
1797         ] (refl ? (lookup SymbolTag block cl_env var_id)))
1798       normalize nodelta
1799       [ 1: (* global case *)
1800            #Hlookup_global
1801            cases (bind_inversion ????? Hlookup_global) -Hlookup_global #global_block
1802            * #Hopt lapply (opt_to_res_inversion ???? Hopt) #Hfind_symbol
1803            #Heq whd in Heq:(???%); destruct (Heq)
1804            lapply (bind2_eq_inversion ?????? Htranslate_expr) -Htranslate_expr
1805            * #var_id_alloctype * #var_id_type * #Heq
1806            cases (variable_not_in_env_but_in_vartypes_is_global …
1807                        Hexec_alloc Hcharacterise Hcl_lookup ?? Heq)
1808            #r #Heq' destruct (Heq') normalize nodelta
1809            lapply Hcl_load_success -Hcl_load_success
1810            lapply Hyp_present -Hyp_present
1811            lapply Hexpr_vars -Hexpr_vars
1812            lapply cm_expr -cm_expr inversion (access_mode ty)
1813            [ #typ_of_ty | | #typ_of_ty ]
1814            #Heq_typ_of_type #Heq_access_mode
1815            #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_success normalize nodelta
1816            whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1817            whd in match (eval_expr ???????);
1818            whd in match (eval_expr ???????);
1819            whd in match (eval_constant ????);
1820            <(eq_sym … inv) >Hfind_symbol normalize nodelta
1821            cases (bind_inversion ????? Hcl_load_success) #x *
1822            #Hopt_to_res whd in ⊢ (???% → ?); #Heq_val destruct (Heq_val)
1823            lapply (opt_to_res_inversion ???? Hopt_to_res)
1824            #Hcl_load_success
1825            [ 2: %{(Vptr (mk_pointer cl_b (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 O))))}
1826                 @conj try @refl
1827                 whd in Hcm_load_success:(??%?);
1828                 lapply (jmeq_to_eq ??? Heq_typ_of_type) #Heq_ty
1829                 >(load_value_of_type_by_ref … Hcl_load_success)
1830                 try assumption %4
1831                 lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
1832                 >Hfind_symbol normalize nodelta #Heq_embedding
1833                 whd in match (shift_offset ???);
1834                 >addition_n_0 whd in match (pointer_translation ??); >Heq_embedding
1835                 normalize nodelta @refl
1836            | 1: cut (access_mode ty=By_value (typ_of_type ty))
1837                 [ @jmeq_to_eq lapply (jmeq_to_eq ??? Heq_typ_of_type) #Heqt
1838                   lapply Heq_access_mode <Heqt // ] #Haccess
1839                 lapply (load_by_value_success_valid_pointer … Haccess … Hcl_load_success)
1840                 #Hvalid_ptr
1841                 lapply (mi_inj … Hinj ?? cl_b zero_offset … Hvalid_ptr … Hcl_load_success)
1842                 [ whd in ⊢ (??%?);
1843                   lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
1844                   >Hfind_symbol normalize nodelta #Heq_embedding >Heq_embedding @refl ]
1845                 * #val' * #Hcm_load_success #Hvalue_eq
1846                 lapply (load_value_of_type_by_value … Haccess … Hcm_load_success)
1847                 #Hloadv lapply (jmeq_to_eq ??? Heq_typ_of_type) #Htypeq <Htypeq >Hloadv
1848                 normalize %{val'} @conj try @refl assumption ]
1849       | 2: (* local case *)
1850            #Heq destruct (Heq)
1851            lapply (bind2_eq_inversion ?????? Htranslate_expr) -Htranslate_expr
1852            * #var_id_alloc_type * #var_id_type *
1853            generalize in match var_id_alloc_type; * normalize nodelta
1854            [ 1: #r #Hlookup_vartype
1855                 lapply (characterise_vars_lookup_local … Hcharacterise … Hcl_lookup … Hexec_alloc)
1856                 * #typ whd in match (local_id ???);
1857                 >Hlookup_vartype normalize nodelta @False_ind
1858            | 2: (* Stack local *)
1859                 lapply Hcl_load_success -Hcl_load_success
1860                 lapply Hyp_present -Hyp_present
1861                 lapply Hexpr_vars -Hexpr_vars
1862                 lapply cm_expr -cm_expr inversion (access_mode ty)
1863                 [ #typ_of_ty | | #typ_of_ty ]
1864                 #Heq_typ_of_type #Heq_access_mode
1865                 #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_success
1866                 #stack_depth #Hlookup_vartype_success normalize nodelta
1867                 whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1868                 lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
1869                 cases (res_inversion ?????? Hlookup_vartype_success) -Hlookup_vartype_success
1870                 * #var_id_alloc_type' #var_id_type' * #Hlookup' #Heq destruct (Heq)
1871                 >Hlookup' normalize nodelta #Hembedding_eq
1872                 cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success
1873                 #loaded_val * #Hload_val
1874                 whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1875                 lapply (opt_to_res_inversion ???? Hload_val) -Hload_val
1876                 #Hload_success whd in match (eval_expr ???????);
1877                 cut (pointer_translation (mk_pointer cl_b zero_offset) E =
1878                      Some ? (mk_pointer sp (mk_offset (repr I16 stack_depth))))
1879                 [ 1,3: whd in ⊢ (??%?); >Hembedding_eq normalize nodelta
1880                        >offset_plus_0 @refl ]
1881                 #Hpointer_translation
1882                 [ 2: (* By-ref *)
1883                      whd in Hload_success:(??%?);
1884                      lapply (load_value_of_type_by_ref … Hload_success … Heq_typ_of_type Heq_access_mode)
1885                      #Heq_val
1886                      >Heq_val
1887                      %{(Vptr (mk_pointer sp (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 stack_depth))))}
1888                      @conj try @refl
1889                      %4 whd in match (shift_offset ???);
1890                      whd in match zero_offset;
1891                      >commutative_addition_n >addition_n_0 @Hpointer_translation
1892                 | 1: (* By value *)
1893                      lapply (jmeq_to_eq ??? Heq_typ_of_type) #Heq0                       
1894                      lapply (mi_inj … Hinj … Hpointer_translation … Hload_success)
1895                      [ @(load_by_value_success_valid_pointer … Hload_success)
1896                        lapply Heq_access_mode <Heq0 /2 by jmeq_to_eq/ ]
1897                      * #cm_val * #Hload_in_cm #Hvalue_eq
1898                      %{cm_val} @conj try assumption
1899                      lapply (load_value_of_type_by_value … Hload_in_cm)
1900                      [ lapply Heq_access_mode <Heq0 #Heq1
1901                        @(jmeq_to_eq ??? Heq1) ]
1902                      #Hloadv <Heq0
1903                      whd in match (shift_offset ???); >commutative_addition_n >addition_n_0
1904                      >Hloadv @refl ]
1905            | 3: (* Register local variable *)
1906                 #Hlookup_eq
1907                 lapply (res_inversion ?????? Hlookup_eq)
1908                 * * #var_id_alloc_type' #var_id_type' * #Hlookup' #Heq destruct (Heq)
1909                 #Htype_eq
1910                 cases (type_should_eq_inversion
1911                            var_id_type
1912                            ty
1913                            (λt0:type.Σe':expr (typ_of_type t0).expr_vars (typ_of_type t0) e' (local_id vars))
1914                            … Htype_eq) -Htype_eq
1915                 (* Reverting all premises in order to perform type rewrite *)
1916                 #Htype_eq
1917                 lapply Hlookup' -Hlookup' lapply Hlookup_eq -Hlookup_eq
1918                 lapply Hcl_load_success -Hcl_load_success
1919                 lapply Hcl_lookup -Hcl_lookup
1920                 lapply Hyp_present -Hyp_present
1921                 lapply Hexpr_vars -Hexpr_vars
1922                 lapply cm_expr
1923                 destruct (Htype_eq)
1924                 #cm_expr #Hexpr_vars #Hyp_present #Hcl_lookup #Hcl_load_success #Hlookup_eq #Hlookup'
1925                 #Hexpr_eq lapply (jmeq_to_eq ??? Hexpr_eq) -Hexpr_eq #Hexpr_eq
1926                 destruct (Hexpr_eq)
1927                 whd in match (eval_expr ???????);
1928                 whd in match (lookup_present ?????);
1929                 lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
1930                 >Hlookup' normalize nodelta #Hmatching
1931                 cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success
1932                 #loaded_val * #Hload_val
1933                 whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1934                 lapply (opt_to_res_inversion ???? Hload_val) -Hload_val
1935                 #Hload_success
1936                 cases (Hmatching … Hload_success) #val'
1937                 * #Hlookup_in_cm #Hvalue_eq %{val'}
1938                 cases Hyp_present
1939                 >Hlookup_in_cm normalize nodelta #_ @conj try @refl try assumption
1940                 (* seems ok *)
1941            ]
1942       ]
1943  | 2: lapply Hcl_success -Hcl_success
1944       lapply Htranslate_expr -Htranslate_expr
1945       lapply Hind -Hind cases ty1
1946       [ | #sz1 #sg1 | #ptr_ty1 | #array_ty1 #array_sz1 | #domain1 #codomain1
1947       | #structname1 #fieldspec1 | #unionname1 #fieldspec1 | #id1 ]
1948       #Hind #Htranslate_expr #Hexec_cl
1949       cases (bind_inversion ????? Htranslate_expr) -Htranslate_expr
1950       * whd in match (typ_of_type ?); normalize nodelta
1951       #cm_expr_ind #Hexpr_vars_ind * #Htranslate_expr_ind
1952       whd in ⊢ ((???%) → ?);
1953       [ 1,2,6,7: #Heq destruct (Heq) ]
1954       lapply (Hind cm_expr_ind Hexpr_vars_ind) -Hind
1955       whd in match (translate_addr ??); >Htranslate_expr_ind normalize nodelta
1956       #Hind lapply (Hind (refl ??) cl_b cl_o cl_t ?) -Hind
1957       [ 1,3,5,7: @cthulhu ]
1958       whd in match (exec_lvalue' ?????); >Hexec_cl normalize nodelta
1959       cases (bind_inversion ????? Hexec_cl) * #cl_ptr #cl_trace0 *
1960       #Hexec_cl_ind #Hcl_ptr
1961       cut (∃ptr. cl_ptr = Vptr ptr)
1962       [ 1,3,5,7: cases cl_ptr in Hcl_ptr; normalize
1963                  #H1 destruct #H2 destruct try /2 by ex_intro, refl/ #H3 destruct ]
1964       * * #cl_ptr_block #cl_ptr_off -Hcl_ptr
1965       #Hcl_ptr destruct (Hcl_ptr) normalize nodelta -Hexec_cl
1966       #Hind lapply (Hind (refl ??)) -Hind
1967       * #cm_ptr * #Hexec_cm_ind #Hvalue_eq_ind
1968       lapply (value_eq_ptr_inversion … Hvalue_eq_ind) * * #cm_ptr_block #cm_ptr_off * #Hcm_ptr
1969       destruct (Hcm_ptr) #Hpointer_translation
1970       cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success #cl_val * #Hopt_to_res
1971       whd in ⊢ ((???%) → ?); #Heq destruct (Heq) lapply (opt_to_res_inversion ???? Hopt_to_res)
1972       -Hopt_to_res
1973       lapply Hyp_present -Hyp_present
1974       lapply Hexpr_vars -Hexpr_vars
1975       lapply cm_expr -cm_expr
1976       inversion (access_mode ty)
1977       [ 1,3,4,6,7,9,10,12: #t ] #Htyp_of_type #Haccess_mode
1978       lapply (jmeq_to_eq ??? Htyp_of_type) #Htyp destruct (Htyp)
1979       #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_success normalize nodelta
1980       #Heq destruct (Heq)
1981       [ 1,2,3,4: (* By_value *)
1982           (* project Hcl_load_success in Cminor through memory_inj *)
1983           lapply (mi_inj ??? Hinj cl_b cl_o cm_ptr_block cm_ptr_off … Hpointer_translation … Hcl_load_success)
1984           [ 1,3,5,7: @(load_by_value_success_valid_pointer … Hcl_load_success) @jmeq_to_eq assumption ]
1985           * #cm_val * #Hcm_load_success #Hvalue_eq
1986           lapply (load_value_of_type_by_value … (jmeq_to_eq ??? Haccess_mode) … Hcm_load_success)
1987           #Hloadv_cm
1988           whd in match (eval_expr ???????); >Hexec_cm_ind normalize nodelta
1989           >Hloadv_cm normalize %{cm_val} @conj try @refl assumption
1990      | *: (* By reference *)
1991           >Hexec_cm_ind %{(Vptr (mk_pointer cm_ptr_block cm_ptr_off))} @conj try @refl
1992           lapply (load_value_of_type_by_ref … Hcl_load_success Htyp_of_type Haccess_mode)
1993           #Hval >Hval %4 assumption ]
1994  | 3: lapply Hcl_load_success -Hcl_load_success lapply Hcl_success -Hcl_success
1995       lapply (refl ? (typeof e1))
1996       cases (typeof e1) in ⊢ ((???%) → %);
1997       [ | #sz1 #sg1 | #ptr_ty1 | #array_ty1 #array_sz1 | #domain1 #codomain1
1998       | #structname1 #fieldspec1 | #unionname1 #fieldspec1 | #id1 ] normalize nodelta
1999       #Heq_typeof normalize nodelta
2000       [ 1,2,3,4,5,8: #Habsurd destruct ] #Hexec_cl #Hcl_load_success
2001       whd in Htranslate_expr:(??%?); >Heq_typeof in Htranslate_expr;
2002       normalize nodelta #Htranslate_expr
2003       cases (bind_inversion ????? Htranslate_expr) -Htranslate_expr
2004       * whd in match (typ_of_type ?); normalize nodelta
2005       #cm_expr_ind #Hexpr_vars_ind * #Htranslate_expr_ind #Htranslate_expr2
2006       [ cases (bind_inversion ????? Htranslate_expr2) -Htranslate_expr2
2007         #cm_field_off * #Hcm_field_off
2008       | lapply Htranslate_expr2 -Htranslate_expr2 ]
2009       cases (bind_inversion ????? Hexec_cl) -Hexec_cl
2010       * * #block_cl #offset_cl #trace0 * #Hexec_lvalue #Hexec_cl
2011       whd in Hexec_lvalue:(???%);
2012       [ cases (bind_inversion ????? Hexec_cl) -Hexec_cl
2013         #cl_field_off * #Hcl_field_off #Hoffset_eq ]
2014       cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success
2015       #cl_val * #Hopt_cl_val whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2016       lapply (opt_to_res_inversion ???? Hopt_cl_val) -Hopt_cl_val #Hcl_load_value
2017       [  (* Struct case *)
2018         lapply Hcl_load_value -Hcl_load_value
2019         lapply Hyp_present -Hyp_present
2020         lapply Hexpr_vars -Hexpr_vars
2021         lapply cm_expr -cm_expr
2022         lapply Hind -Hind
2023         cases ty
2024         [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
2025         | #structname #fieldspec | #unionname #fieldspec | #id ]
2026         #Hind #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_value
2027         normalize nodelta
2028         whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2029         whd in match (eval_expr ???????);
2030         (* applying the arguments of the induction hypothesis progressively *)
2031         lapply (Hind (Op2 ASTptr (ASTint I16 Signed) ASTptr (Oaddp I16) cm_expr_ind
2032                          (Cst (ASTint I16 Signed) (Ointconst I16 Signed (repr I16 cm_field_off)))) ?)
2033         [ 1,3,5,7,9: whd @conj try assumption whd @I ] -Hind #Hind
2034         lapply (Hind ?)
2035         [ 1,3,5,7,9:
2036            whd in ⊢ (??%?); >Heq_typeof normalize nodelta
2037            >Htranslate_expr_ind whd in match (m_bind ?????);
2038            >Hcm_field_off normalize nodelta @refl ] -Hind #Hind
2039         whd in Hoffset_eq:(???%); destruct (offset_eq)
2040         cut (cl_field_off = cm_field_off)
2041         [ 1,3,5,7,9: lapply Hcl_field_off >Hcm_field_off
2042           normalize #Heq destruct (Heq) @refl ]
2043         #Heq destruct (Heq)
2044         lapply (Hind cl_b cl_o trace ?)
2045         [ 1,3,5,7,9: @Hyp_present ] -Hind #Hind
2046         lapply (Hind ?) -Hind
2047         [ 1,3,5,7,9: whd in ⊢ (??%?); >Heq_typeof normalize nodelta
2048           >Hexec_lvalue whd in match (m_bind ?????); >Hcm_field_off normalize nodelta
2049           @Hoffset_eq ]
2050         * #cm_val' * #Heval_expr #Hvalue_eq
2051         lapply (value_eq_ptr_inversion … Hvalue_eq) * * #cm_ptr_block #cm_ptr_off
2052         * #Heq_cm_val_ptr destruct (Heq_cm_val_ptr) #Hpointer_trans
2053         [ 1,2,5: (* by-value *)
2054            lapply (mi_inj … Hinj cl_b cl_o ?? … Hpointer_trans … Hcl_load_value)
2055            [ 1,3,5: @(load_by_value_success_valid_pointer … Hcl_load_value) // ]
2056            * #cm_val * #Hcm_load_value #Hvalue_eq
2057            lapply (load_value_of_type_by_value … Hcm_load_value)
2058            [ 1,3,5: @refl ]
2059            #Hcm_loadv %{cm_val} >Heval_expr normalize nodelta >Hcm_loadv normalize @conj
2060            try @refl try assumption
2061         | 3,4: (* by-ref *)
2062            whd in match (eval_expr ???????) in Heval_expr; >Heval_expr
2063            %{(Vptr (mk_pointer cm_ptr_block cm_ptr_off))} @conj try @refl
2064            whd in Hcl_load_value:(??%?); destruct (Hcl_load_value) assumption
2065         ]
2066      | (* union case *)
2067         lapply Hcl_load_value -Hcl_load_value
2068         lapply Hyp_present -Hyp_present
2069         lapply Hexpr_vars -Hexpr_vars
2070         lapply cm_expr -cm_expr
2071         lapply Hind -Hind
2072         cases ty
2073         [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
2074         | #structname #fieldspec | #unionname #fieldspec | #id ]
2075         whd in match (typ_of_type ?); normalize nodelta
2076         #Hind #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_value
2077         whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2078         [ 1,2,5: (* by-value *)
2079            whd in match (eval_expr ???????);
2080            lapply (Hind cm_expr_ind Hexpr_vars ?)
2081            [ 1,3,5: whd in ⊢ (??%?); >Heq_typeof normalize nodelta @Htranslate_expr_ind ]
2082            whd in match (exec_lvalue' ?????); >Heq_typeof normalize nodelta
2083            -Hind #Hind
2084            lapply (Hind block_cl offset_cl trace0 Hyp_present) -Hind >Hexec_lvalue normalize nodelta
2085            whd in match (m_bind ?????); #Hind
2086            cases (Hind (refl ??)) -Hind
2087            #cm_val * #Heval_expr #Hvalue_eq >Heval_expr normalize nodelta
2088            cases (value_eq_ptr_inversion … Hvalue_eq) * #cm_block #cm_offset * #Hcm_val #Hpointer_trans
2089            destruct (Hcm_val) whd in Hexec_cl:(???%); destruct (Hexec_cl)
2090            lapply (mi_inj … Hinj cl_b cl_o cm_block cm_offset … Hpointer_trans … Hcl_load_value)
2091            [ 1,3,5: @(load_by_value_success_valid_pointer … Hcl_load_value) // ]
2092            * #cm_val * #Hcm_load_value #Hvalue_eq           
2093            lapply (load_value_of_type_by_value … Hcm_load_value)
2094            [ 1,3,5: @refl ]
2095            #Hcm_loadv %{cm_val} >Hcm_loadv normalize @conj
2096            try @refl assumption
2097         | 3,4:
2098            whd in Hexec_cl:(???%); destruct (Hexec_cl)
2099            lapply (Hind cm_expr Hexpr_vars)
2100            whd in match (translate_addr ??); >Heq_typeof normalize nodelta -Hind #Hind
2101            lapply (Hind Htranslate_expr_ind) -Hind
2102            whd in match (exec_lvalue' ?????); >Heq_typeof normalize nodelta
2103            >Hexec_lvalue whd in match (m_bind ?????);
2104            #Hind cases (Hind … Hyp_present (refl ??))
2105            #cm_val * #Heval_expr #Hvalue_eq >Heval_expr %{cm_val} @conj
2106            try @refl whd in Hcl_load_value:(??%?); destruct (Hcl_load_value)
2107            assumption ]
2108    ]
2109  ]
2110| 3: #var #ty #cmexpr #Hexpr_vars #Htranslate_var #cl_blo #cl_off #trace #Hyp_present #Hexec_lvalue_var
2111     whd in Hexec_lvalue_var:(??%?);
2112     (* check whether var is local or global *)
2113     lapply (Hlocal_matching var)
2114     lapply (variable_not_in_env_but_in_vartypes_is_global  … var Hexec_alloc … Hcharacterise)
2115     cases (lookup ?? cl_env var) in Hexec_lvalue_var;
2116     normalize nodelta
2117     [ 1: (* global *)
2118          #Hexec_opt #H lapply (H (refl ??)) -H #Hvar_is_global
2119          cases (bind_inversion ????? Hexec_opt) -Hexec_opt #varblock * #Hopt_to_res #Heq
2120          whd in Heq:(???%) Hopt_to_res:(???%); destruct (Heq)
2121          lapply (opt_to_res_inversion ???? Hopt_to_res) -Hopt_to_res #Hfind_symbol >Hfind_symbol normalize nodelta
2122          #Hembed
2123          cases (bind_inversion ????? Htranslate_var) -Htranslate_var
2124          * #var_alloctype #var_type * #Hlookup_vartype #Hvar_alloctype
2125          cases (Hvar_is_global … Hlookup_vartype) #r #Halloctype >Halloctype in Hvar_alloctype;
2126          normalize nodelta whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2127          whd in match (eval_expr ???????);
2128          whd in match (eval_constant ????);
2129          <(eq_sym inv var) >Hfind_symbol normalize nodelta
2130          %{(Vptr (mk_pointer cl_blo (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 O))))}
2131          @conj try @refl %4 whd in match (pointer_translation ??);
2132          >Hembed normalize nodelta whd in match (shift_offset ???);
2133          >addition_n_0 @refl
2134     | 2: (* local *)
2135          #BL #Heq destruct (Heq) #_
2136          @(match (lookup ?? vars var)
2137            return λx. (lookup ?? vars var = x) → ?
2138            with
2139            [ None ⇒ ?
2140            | Some kind ⇒ ?
2141            ] (refl ??))
2142          normalize nodelta
2143          #Hlookup [ @False_ind ]
2144          cases kind in Hlookup; #var_alloctype #var_type normalize nodelta
2145          #Hlookup
2146          lapply (refl ? var_alloctype)
2147          cases var_alloctype in ⊢ ((???%) → %); normalize nodelta
2148          [ #reg #Heq @False_ind | #stacksize #Hvar_alloc #Hembed | #Hvar_alloc #Hlookup' ]
2149          [ (* stack alloc*)
2150            cases (bind_inversion ????? Htranslate_var) -Htranslate_var
2151            * #var_alloctype' #var_type' * #Hlookup_vartype'           
2152            whd in Hlookup_vartype':(??%?); >Hlookup in Hlookup_vartype'; normalize nodelta
2153            whd in ⊢ ((???%) → ?); #Heq destruct (Heq) >Hvar_alloc normalize nodelta
2154            whd in ⊢ ((???%) → ?); #Heq destruct (Heq) whd in match (eval_expr ???????);
2155            %{(Vptr (mk_pointer sp (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 stacksize))))}
2156            @conj try @refl %4 whd in match (pointer_translation ??);
2157            >Hembed @refl
2158          | (* local alloc *)
2159            cases (bind_inversion ????? Htranslate_var) -Htranslate_var
2160            * #var_alloctype' #var_type' * #Hlookup_vartype'
2161            whd in Hlookup_vartype':(??%?); >Hlookup in Hlookup_vartype'; normalize nodelta
2162            whd in ⊢ ((???%) → ?); #Heq destruct (Heq) >Hvar_alloc normalize nodelta
2163            whd in ⊢ ((???%) → ?); #Heq destruct (Heq) ] ]
2164(*| 4: #e #ty*)
2165| 4:
2166  * #ed #ety cases ety
2167  [ | #sz1 #sg1 | #ptr_ty1 | #array_ty1 #array_sz1 | #domain1 #codomain1
2168  | #structname1 #fieldspec1 | #unionname1 #fieldspec1 | #id1 ] normalize nodelta 
2169  whd in match (typeof ?);
2170  #ty #Hind #e' #Hexpr_vars #Htranslate #cl_blo #cl_off #trace #Hyp_present #Hexec_lvalue
2171  cases (bind_inversion ????? Htranslate) -Htranslate   
2172  * #cm_expr #Hexpr_vars_cm * #Htranslate_ind
2173  cases (bind_inversion ????? Hexec_lvalue) -Hexec_lvalue
2174  * #cl_val #trace0 * #Hexec_expr #Hcl_val
2175  whd in match (typeof ?); whd in match (typ_of_type ?); normalize nodelta
2176  whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2177  cut (cl_val = Vptr (mk_pointer cl_blo cl_off) ∧ trace = trace0)
2178  [ 1,3,5,7: cases cl_val in Hcl_val; normalize
2179    [ 1,5,9,13: #Heq destruct (Heq)
2180    | 2,6,10,14: #sz #vec #Heq destruct (Heq)
2181    | 3,7,11,15: #Heq destruct (Heq)
2182    | 4,8,12,16: * #BL #OFF #Heq destruct (Heq) @conj try @refl ] ]
2183  * #Heq_cl_val destruct (Heq_cl_val) #Htrace_eq destruct (Htrace_eq)
2184  cases (Hind e' Hexpr_vars Htranslate_ind … Hyp_present … Hexec_expr)
2185  #cm_val * #Heval_expr_cm #Hvalue_eq >Heval_expr_cm
2186  %{cm_val} @conj try @refl try assumption
2187| 5:
2188  #ty cases ty
2189  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
2190  | #structname #fieldspec | #unionname #fieldspec | #id ]
2191  #ed #ty' #Hind
2192  whd in match (typeof ?); whd in match (typ_of_type ?); #cm_expr
2193  #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec_expr
2194  cases (bind_inversion ????? Htranslate) -Htranslate
2195  * #cm_expr #Hexpr_vars_cm * #Htranslate_ind
2196  cases (bind_inversion ????? Hexec_expr) -Hexec_expr
2197  * * #cl_blo #cl_off #trace0 * #Hexec_lvalue normalize nodelta
2198  whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2199  whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2200  cases (Hind cm_expr Hexpr_vars Htranslate_ind ??? Hyp_present Hexec_lvalue)
2201  #cm_val * #Hexec_cm #Hvalue_eq >Hexec_cm
2202  %{cm_val} @conj try @refl assumption
2203| 6:
2204  #ty *
2205  [ cases ty
2206    [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
2207    | #structname #fieldspec | #unionname #fieldspec | #id ]
2208    #e #Hind
2209    whd in match (typeof ?);
2210    #e' whd in match (typ_of_type ?); #Hexpr_vars whd in ⊢ ((??%?) → ?);
2211    #Htranslate
2212    [ 3,4,5,8: destruct (Htranslate)
2213    | 2: lapply Htranslate -Htranslate lapply Hexpr_vars -Hexpr_vars lapply e' -e'
2214         cases sz normalize nodelta
2215         #e' #Hexpr_vars #Htranslate
2216         [ 1, 2: destruct (Htranslate) ] ]
2217    #cl_val #trace #Hyp_present #Hexec_expr
2218    cases (bind_inversion ????? Htranslate) -Htranslate
2219    #cmop * #Htranslate_unop #Hexec_arg
2220    cases (bind_inversion ????? Hexec_arg) -Hexec_arg
2221    * #cm_arg #Hexpr_vars_arg * #Htranslate whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2222    cases (bind_inversion ????? Hexec_expr) -Hexec_expr
2223    * #cl_arg #cl_trace * #Hexec_cl
2224    whd in ⊢ ((???%) → ?); #Hexec_unop
2225    cases (bind_inversion ????? Hexec_unop) -Hexec_unop
2226    #v * #Hopt whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2227    lapply (opt_to_res_inversion ???? Hopt) -Hopt
2228    #Hsem_cl whd in match (eval_expr ???????);
2229    cases (Hind cm_arg Hexpr_vars Htranslate … Hyp_present Hexec_cl)
2230    #cm_val * #Heval_cm #Hvalue_eq >Heval_cm normalize nodelta
2231    lapply (unary_operation_value_eq … Hvalue_eq … Hsem_cl)
2232    * #cl_val' * #Hcl_unop #Hvalue_eq %{cl_val'} @conj try assumption
2233    whd in match (typ_of_type Tvoid);
2234    lapply (translate_notbool_to_cminor … Htranslate_unop … Hcl_unop)
2235    #H >H @refl
2236  | *:
2237    cases ty
2238    [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id
2239    | | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id ]
2240    #e #Hind whd in match (typeof ?);  whd in match (typ_of_type ?); 
2241    #e' #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec
2242    whd in Htranslate:(??%?);
2243    [ 3,4,5,8,11,12,13,16: destruct (Htranslate) ]
2244    cases (bind_inversion ????? Htranslate) -Htranslate
2245    #cmop * #Htranslate_unop #Hexec_arg
2246    cases (bind_inversion ????? Hexec_arg) -Hexec_arg
2247    * #cm_arg #Hexpr_vars_arg * #Htranslate whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2248    cases (bind_inversion ????? Hexec) -Hexec
2249    * #cl_arg #cl_trace * #Hexec_cl
2250    whd in ⊢ ((???%) → ?); #Hexec_unop
2251    cases (bind_inversion ????? Hexec_unop) -Hexec_unop
2252    #v * #Hopt whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2253    lapply (opt_to_res_inversion ???? Hopt) -Hopt
2254    #Hcl_unop whd in match (eval_expr ???????);
2255    cases (Hind cm_arg Hexpr_vars Htranslate … Hyp_present Hexec_cl)
2256    #op_arg * #Heval_cm #Hvalue_eq >Heval_cm normalize nodelta
2257    lapply (unary_operation_value_eq … Hvalue_eq … Hcl_unop)
2258    * #op_res * #Hcl_sem #Hvalue_eq
2259    [ 1,2,3,4: >(translate_notint_to_cminor … Htranslate_unop … Hcl_sem)
2260       %{op_res} @conj try @refl assumption
2261    | 5,6,7,8: >(translate_negint_to_cminor … Htranslate_unop … Hcl_sem)
2262       %{op_res} @conj try @refl assumption
2263    ]
2264  ]
2265| 8: #ty #ty' * #ed #ety
2266  cases ety
2267  [ | #esz #esg | #eptr_ty | #earray_ty #earray_sz | #edomain #ecodomain
2268  | #estructname #efieldspec | #eunionname #efieldspec | #eid ]
2269  whd in match (typeof ?); whd in match (typ_of_type ?);
2270  #Hind whd in match (typeof ?);
2271  #cm_expr #Hexpr_vars #Htranslate
2272  cases (bind_inversion ????? Htranslate) -Htranslate
2273  * #cm_castee #Hexpr_vars_castee * #Htranslate_expr #Htranslate
2274  cases (bind_inversion ????? Htranslate) -Htranslate
2275  * #cm_cast #Hexpr_vars_cast * #Htranslate_cast #Htranslate 
2276  [ 1,5,6,7,8: whd in Htranslate_cast:(??%%); destruct (Htranslate_cast) ]
2277  cases (bind_inversion ????? Htranslate) -Htranslate
2278  * #cm_cast' #Hexpr_vars' * #Htyp_should_eq whd in ⊢ ((??%%) → ?);
2279  #Heq destruct (Heq)
2280  #cl_val #trace #Hyp_present #Hexec_cm
2281  cases (bind_inversion ????? Hexec_cm) -Hexec_cm
2282  * #cm_val #trace0 * #Hexec_cm #Hexec_cast
2283  cases (bind_inversion ????? Hexec_cast) -Hexec_cast
2284  #cast_val * #Hexec_cast
2285  whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
2286  cases (typ_should_eq_inversion (typ_of_type ty') (typ_of_type ty) … Htyp_should_eq) -Htyp_should_eq
2287  #Htype_eq
2288  lapply Hexec_cast -Hexec_cast
2289(*  lapply Htyp_should_eq -Htyp_should_eq *)
2290  lapply Htranslate_cast -Htranslate_cast
2291  lapply Hexpr_vars_cast -Hexpr_vars_cast
2292  lapply cm_cast -cm_cast
2293  lapply Hyp_present -Hyp_present
2294  lapply Hexpr_vars -Hexpr_vars
2295  lapply cm_expr -cm_expr
2296  <Htype_eq -Htype_eq
2297  whd in ⊢ (? → ? → ? → ? → ? → ? → (??%%) → ?);
2298  whd in match (typeof ?); normalize nodelta
2299  cases ty'
2300  [ | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain' | #structname' #fieldspec' | #unionname' #fieldspec' | #id'
2301  | | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain' | #structname' #fieldspec' | #unionname' #fieldspec' | #id'
2302  | | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain' | #structname' #fieldspec' | #unionname' #fieldspec' | #id' ]
2303  #cm_expr #Hexpr_vars #Hyp_present #cm_cast #Hexpr_vars_cast #Htranslate_cast normalize nodelta #Hexec_cast
2304  #Heq lapply (jmeq_to_eq ??? Heq) -Heq #Heq destruct (Heq)
2305  whd in Htranslate_cast:(??%%);
2306  whd in Hexpr_vars;
2307  destruct (Htranslate_cast)
2308  [ 1,2,3,4,7:
2309    lapply (Hind cm_castee Hexpr_vars Htranslate_expr … Hyp_present Hexec_cm)
2310    * #cm_val' * #Heval_castee
2311    lapply Hexec_cm -Hexec_cm
2312    whd in Hexec_cast:(??%%);
2313    cases cm_val in Hexec_cast; normalize nodelta
2314    [ | #vsz #vi | | #vp
2315    | | #vsz #vi | | #vp
2316    | | #vsz #vi | | #vp
2317    | | #vsz #vi | | #vp
2318    | | #vsz #vi | | #vp ]
2319    [ 2,6,10,14,18:
2320    | *: #Habsurd destruct (Habsurd) ]
2321    #Hexec_cast #Hexec_cm #Hvalue_eq
2322    [ 1,2,3:
2323      cases (intsize_eq_elim_inversion ??????? Hexec_cast) -Hexec_cast
2324      #Hsz_eq destruct (Hsz_eq) #Hcl_val_eq ]
2325    [ 2,3: lapply (sym_eq ??? Hcl_val_eq) -Hcl_val_eq #Hexec_cast ]
2326    [ 1,2,4,5:
2327      cases (bind_inversion ????? Hexec_cast)
2328      whd in match (typeof ?);
2329      #cast_val * whd in ⊢ ((??%%) → ?); normalize nodelta
2330      whd in match (eq_rect_r ??????);
2331      [ 3,4: cases (eq_bv ???) normalize nodelta #Heq destruct (Heq) ]
2332      @(eq_bv_elim … vi (zero (bitsize_of_intsize esz))) normalize nodelta
2333      [ 2,4: #foo #Habsurd destruct (Habsurd) ]
2334      #Heq_vi >eq_intsize_true normalize nodelta #Heq destruct (Heq)
2335      whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
2336      whd in match (typ_of_type ?); whd in match (eval_expr ???????);
2337      >Heval_castee normalize nodelta whd in match (eval_unop ????);
2338      >(value_eq_int_inversion … Hvalue_eq) normalize nodelta
2339      >Heq_vi >eq_bv_true normalize
2340      %{Vnull} @conj try @refl %3
2341    | 3: destruct (Hcl_val_eq)
2342          whd in match (eval_expr ???????);
2343          >Heval_castee normalize nodelta
2344          whd in match (eval_unop ????);
2345          cases esg normalize nodelta
2346          whd in match (opt_to_res ???); whd in match (m_bind ?????);
2347          [ %{(sign_ext sz' cm_val')} | %{(zero_ext sz' cm_val')} ] @conj try @refl
2348          whd in match (eq_rect_r ??????);
2349          -Hexpr_vars -Hyp_present -Hind -Hexec_cm -cm_castee
2350          (* cast_int_int is defined as a let rec on its first argument, we have to eliminate esz for
2351             this reason. *)
2352          lapply Hvalue_eq -Hvalue_eq lapply vi -vi
2353          cases esz normalize nodelta
2354          #vi #Hvalue_eq >(value_eq_int_inversion … Hvalue_eq)
2355          whd in match (sign_ext ??); whd in match (zero_ext ??);
2356          %2
2357    ]
2358 | *:
2359    lapply (Hind cm_expr Hexpr_vars Htranslate_expr … Hyp_present Hexec_cm)
2360    * #cm_val' * #Heval_expr #Hvalue_eq >Heval_expr
2361    %{cm_val'} @conj try @refl
2362    lapply Hexec_cast -Hexec_cast lapply Hvalue_eq -Hvalue_eq
2363    -Hind -Hexpr_vars -Hyp_present lapply Hexec_cm -Hexec_cm
2364    cases cm_val
2365    [ | #vsz #vi | | #vp
2366    | | #vsz #vi | | #vp
2367    | | #vsz #vi | | #vp
2368    | | #vsz #vi | | #vp ]
2369    #Hexec_cm #Hvalue_eq #Hexec_cast
2370    whd in Hexec_cast:(??%%);
2371    [ 1,5,9,13: destruct (Hexec_cast) ]
2372    [ 2,3,5,6,8,9,11,12: destruct (Hexec_cast) try assumption ]
2373    lapply Hexec_cast -Hexec_cast
2374    normalize cases (eq_v ?????) normalize
2375    #Habsurd destruct (Habsurd)
2376 ]
2377| 9: (* Econdition *) 
2378  #ty #e1 #e2 #e3 #Hind1 #Hind2 #Hind3 whd in match (typeof ?);
2379  #cm_expr #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present
2380  #Hexec_cm
2381  cases (bind_inversion ????? Hexec_cm) -Hexec_cm
2382  * #cm_cond_val #trace_cond0 * #Hexec_cond #Hexec_cm
2383  cases (bind_inversion ????? Hexec_cm) -Hexec_cm
2384  #bool_of_cm_cond_val * #Hexec_bool_of_val #Hexec_cm
2385  cases (bind_inversion ????? Hexec_cm) -Hexec_cm
2386  * #cm_ifthenelse_val #cm_ifthenelse_trace * #Hcm_ifthenelse
2387  whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2388  cases (bind_inversion ????? Htranslate) -Htranslate
2389  * #cm_expr_e1 #Hexpr_vars_e1 * #Htranslate_e1 #Htranslate
2390  cases (bind_inversion ????? Htranslate) -Htranslate
2391  * #cm_expr_e2 #Hexpr_vars_e2 * #Htranslate_e2 #Htranslate
2392  cases (bind_inversion ????? Htranslate) -Htranslate
2393  * #cm_expr_e2_welltyped #Hexpr2_vars_wt * #Htypecheck
2394  lapply (typ_should_eq_inversion (typ_of_type (typeof e2)) (typ_of_type ty) … Htypecheck) -Htypecheck
2395  *  #Htypeof_e2_eq_ty
2396  lapply (Hind2 cm_expr_e2 Hexpr_vars_e2 Htranslate_e2) -Hind2
2397  lapply Hexpr_vars_e2 -Hexpr_vars_e2 lapply cm_expr_e2 -cm_expr_e2
2398  >Htypeof_e2_eq_ty #cm_expr_e2 #Hexpr_vars_e2 #Hind2 
2399  #Hjm_type_eq lapply (jmeq_to_eq ??? Hjm_type_eq) -Hjm_type_eq
2400  #Hcmexpr_eq2 destruct (Hcm_expr_eq2) #Htranslate
2401  cases (bind_inversion ????? Htranslate) -Htranslate
2402  * #cm_expr_e3 #Hexpr_vars_e3 * #Htranslate_e3 #Htranslate 
2403  cases (bind_inversion ????? Htranslate) -Htranslate 
2404  * #cm_expr_e3_welltyped #Hexpr3_vars_wt * #Htypecheck
2405  lapply (typ_should_eq_inversion (typ_of_type (typeof e3)) (typ_of_type ty) … Htypecheck) -Htypecheck
2406  * #Htypeof_e3_eq_ty
2407  lapply (Hind3 cm_expr_e3 Hexpr_vars_e3 Htranslate_e3) -Hind3
2408  lapply Hexpr_vars_e3 -Hexpr_vars_e3 lapply cm_expr_e3 -cm_expr_e3
2409  >Htypeof_e3_eq_ty #cm_expr_e3 #Hexpr_vars_e3 #Hind3
2410  #Hjm_type_eq lapply (jmeq_to_eq ??? Hjm_type_eq) -Hjm_type_eq
2411  #Hcmexpr_eq3 destruct (Hcm_expr_eq2)
2412  lapply (Hind1 cm_expr_e1 Hexpr_vars_e1 Htranslate_e1) -Hind1 
2413  lapply Hexpr_vars_e1 -Hexpr_vars_e1 lapply cm_expr_e1 -cm_expr_e1
2414  lapply Hexec_bool_of_val -Hexec_bool_of_val
2415  cases (typeof e1) normalize nodelta
2416  [ | #esz #esg | #eptr_ty | #earray_ty #earray_sz | #edomain #ecodomain
2417  | #estructname #efieldspec | #eunionname #efieldspec | #eid ]
2418  #Hexec_bool_of_val #cm_expr_e1 #Hexpr_vars_e1 #Hind1 #Heq
2419  whd in Heq:(???%); destruct (Heq)
2420  whd in match (eval_expr ???????);
2421  whd in Hyp_present; cases Hyp_present * #Hyp1 #Hyp2 #Hyp3 -Hyp_present
2422  lapply (Hind1 … Hyp1 Hexec_cond) -Hind1 * #cm_val_e1 * #Heval_e1 #Hvalue_eq1
2423  >Heval_e1 normalize nodelta
2424  lapply Hcm_ifthenelse -Hcm_ifthenelse
2425  lapply Hexec_cond -Hexec_cond 
2426  lapply Hexec_bool_of_val -Hexec_bool_of_val
2427  lapply Hvalue_eq1 -Hvalue_eq1
2428  cases cm_cond_val
2429  [ | #vsz #vi | | #vp
2430  | | #vsz #vi | | #vp
2431  | | #vsz #vi | | #vp
2432  | | #vsz #vi | | #vp ]
2433  whd in ⊢ (? → (??%%) → ?);
2434  [ 6:
2435  | *: #_ #Habsurd destruct (Habsurd) ]
2436  #Hvalue_eq1 #Hsz_check
2437  lapply (intsize_eq_elim_inversion ??????? Hsz_check) -Hsz_check
2438  * #Hsz_eq destruct (Hsz_eq) whd in match (eq_rect_r ??????);
2439  #Heq destruct (Heq)
2440  #Hexec_expr_e1
2441  @(match (eq_bv (bitsize_of_intsize esz) vi (zero (bitsize_of_intsize esz)))
2442    return λx. ((eq_bv (bitsize_of_intsize esz) vi (zero (bitsize_of_intsize esz))) = x) → ?
2443    with
2444    [ true ⇒ λHeq. ?
2445    | false ⇒ λHeq. ?
2446    ] (refl ? (eq_bv (bitsize_of_intsize esz) vi (zero (bitsize_of_intsize esz)))))
2447  normalize nodelta
2448  >(value_eq_int_inversion … Hvalue_eq1) #Hexec_expr_body
2449  whd in match (eval_bool_of_val ?); whd in match (m_bind ?????);
2450  >Heq normalize nodelta
2451  [ -Heq -Hexec_expr_e1 -Hvalue_eq1 -Heval_e1 -cm_val_e1 -Hexpr_vars_e1 destruct (Hcmexpr_eq3)
2452    cases (Hind3 … Hyp3 Hexec_expr_body) #cm_val3 * #Heval_expr >Heval_expr #Hvalue_eq
2453    normalize %{cm_val3} @conj try @refl assumption
2454  | -Heq -Hexec_expr_e1 -Hvalue_eq1 -Heval_e1 -cm_val_e1 -Hexpr_vars_e1 destruct (Hcmexpr_eq2)
2455    cases (Hind2 … Hyp2 Hexec_expr_body) #cm_val2 * #Heval_expr >Heval_expr #Hvalue_eq
2456    normalize %{cm_val2} @conj try @refl assumption ]
2457| 10: (* andbool *)
2458  #ty cases ty
2459  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
2460  | #structname #fieldspec | #unionname #fieldspec | #id ]
2461  #e1 #e2 #Hind1 #Hind2 whd in match (typeof ?);
2462  #cm_expr #Hexpr_vars #Htranslate #cl_final_val #trace #Hyp_present #Hexec_expr
2463  (* decompose first slice of clight execution *)
2464  cases (bind_inversion ????? Hexec_expr) -Hexec_expr
2465  * #cl_val_e1 #cm_trace_e1 * #Hexec_e1 #Hexec_expr
2466  cases (bind_inversion ????? Hexec_expr) -Hexec_expr
2467  #b * #Hexec_bool_of_val #Hexec_expr
2468  (* decompose translation to Cminor *)
2469  cases (bind_inversion ????? Htranslate) -Htranslate normalize nodelta
2470  * #cm_expr_e1 #Hexpr_vars_e1 * #Htranslate_e1 #Htranslate
2471  cases (bind_inversion ????? Htranslate) -Htranslate
2472  * #cm_expr_e2 #Hexpr_vars_e2 * #Htranslate_e2 whd in ⊢ ((???%) → ?);
2473  [ 2: | *: #Heq destruct (Heq) ]
2474  (* discriminate I16 and I8 cases *)
2475(*  lapply Hyp_present -Hyp_present
2476  lapply Hexpr_vars -Hexpr_vars
2477  lapply cm_expr -cm_expr cases sz
2478  #cm_expr #Hexpr_vars #Hyp_present normalize nodelta
2479  [ 1,2: #Habsurd destruct (Habsurd) ]   *)
2480  (* go on with decomposition *)
2481  #Htranslate cases (bind_inversion ????? Htranslate) -Htranslate
2482  * #cm_expr_e2_welltyped #Hexpr_vars_e2_wt * #Htypecheck
2483  (* cleanup the type coercion *)
2484  lapply (type_should_eq_inversion (typeof e2) (Tint sz sg) … Htypecheck) -Htypecheck
2485  * #Htypeof_e2_eq_ty
2486  lapply (Hind2 cm_expr_e2 Hexpr_vars_e2 Htranslate_e2) -Hind2
2487  lapply Hexpr_vars_e2_wt -Hexpr_vars_e2_wt
2488  lapply cm_expr_e2_welltyped -cm_expr_e2_welltyped whd in match (typ_of_type ?);
2489  lapply Hexpr_vars_e2 -Hexpr_vars_e2
2490  lapply cm_expr_e2 -cm_expr_e2
2491  lapply Hexec_expr -Hexec_expr
2492  >Htypeof_e2_eq_ty normalize nodelta -Htypeof_e2_eq_ty
2493  #Hexec_expr #cm_expr_e2 #Hexpr_vars_e2 #cm_expr_e2_welltyped #Hexpr_vars_e2_wt #Hind2
2494  #Heq_e2_wt lapply (jmeq_to_eq ??? Heq_e2_wt) -Heq_e2_wt #Heq destruct (Heq)
2495  (* Cleanup terminated. We need to perform a case analysis on (typeof e1) in order
2496   * to proceed in decomposing translation. *)
2497  lapply (Hind1 cm_expr_e1 … Hexpr_vars_e1 Htranslate_e1) -Hind1
2498  lapply Hexpr_vars_e1 -Hexpr_vars_e1
2499  lapply cm_expr_e1 -cm_expr_e1
2500  lapply Hexec_bool_of_val -Hexec_bool_of_val
2501  cases (typeof e1)
2502  [ | #sz1 #sg1 | #ptr_ty1 | #array_ty1 #array_sz1 | #domain1 #codomain1
2503  | #structname1 #fieldspec1 | #unionname1 #fieldspec1 | #id1 ]
2504  #Hexec_bool_of_val #cm_expr_e1 #Hexpr_vars_e1 #Hind1
2505  normalize nodelta whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
2506  (* translation decomposition terminated. Reduce goal *)
2507  whd in match (eval_expr ???????);
2508  (* We need Hind1.  *)
2509  cases Hyp_present -Hyp_present * #Hyp1 #Hyp2 #Hyp
2510  lapply (Hind1 … Hyp1 Hexec_e1) -Hind1 * #cm_val_1 * #Heval_expr1 >Heval_expr1 #Hvalue_eq
2511  normalize nodelta
2512  (* peform case analysis to further reduce the goal. *)
2513  lapply Hvalue_eq -Hvalue_eq
2514  lapply Hexec_bool_of_val -Hexec_bool_of_val
2515  whd in match (proj2 ???);
2516  cases cl_val_e1
2517  [ | #vsz #vi | | #vp
2518  | | #vsz #vi | | #vp
2519  | | #vsz #vi | | #vp
2520  | | #vsz #vi | | #vp ]
2521  whd in ⊢ ((??%%) → ?);
2522  [ 6:
2523  | *: #Heq destruct (Heq) ]
2524  #Hsz_check #Hvalue_eq
2525  lapply (intsize_eq_elim_inversion ??????? Hsz_check) -Hsz_check
2526  * #Hsz_eq destruct (Hsz_eq) whd in match (eq_rect_r ??????);
2527  (* preparing case analysis on b *)
2528  lapply Hexec_expr -Hexec_expr
2529  cases b normalize nodelta
2530  [ 2: (* early exit *)
2531       #Heq_early whd in Heq_early:(??%%); destruct (Heq_early)
2532       #Heq_outcome destruct (Heq_outcome) -Heq_outcome
2533       >(value_eq_int_inversion … Hvalue_eq) whd in match (eval_bool_of_val ?);
2534       <e0 whd in match (m_bind ?????);
2535       @cthulhu
2536       (* Pb: incompatible semantics for cl and cm.
2537        * in Cexec/exec_expr : evaluation returns Vfalse:bvint 32 if
2538          first operand is false (for andbool)
2539          . solution 1 : change semantics to return actual value instead of Vfalse
2540          . solution 2 : change toCminor to introduce another test in the program,
2541            returning Vfalse in case of failure instead of actual value
2542        *) ]
2543  #Hexec_expr #Heq_outcome
2544  cases (bind_inversion ????? Hexec_expr) -Hexec_expr
2545  * #cl_val_e2 #trace2 * #Hexec_e2 #Hexec_expr
2546  cases (bind_inversion ????? Hexec_expr) -Hexec_expr
2547  #outcome_bool * #Hexec_bool_outcome whd in ⊢ ((???%) → ?);
2548  #Heq destruct (Heq)
2549  >(value_eq_int_inversion … Hvalue_eq)
2550  whd in match (eval_bool_of_val ?);
2551  destruct (Heq_outcome) <e0 whd in match (m_bind ?????);
2552  normalize nodelta
2553  cases (Hind2 … Hyp2 Hexec_e2) #cm_val_e2 * #Heval_expr #Hvalue_eq2
2554  >Heval_expr normalize nodelta
2555  %{cm_val_e2} @conj try @refl 
2556  whd in Hexec_bool_outcome:(??%%);
2557  normalize nodelta in Hexec_bool_outcome:(??%%);
2558  lapply Hvalue_eq2 -Hvalue_eq2
2559  -Heval_expr
2560  lapply Hexec_bool_outcome -Hexec_bool_outcome
2561  cases cl_val_e2
2562  [ | #vsz2 #vi2 | | #vp2 ] normalize nodelta
2563  #Heq destruct (Heq)
2564  cases (intsize_eq_elim_inversion ??????? Heq)
2565  #Hsz_eq destruct (Hsz_eq) whd in match (eq_rect_r ??????);
2566  cases outcome_bool normalize nodelta
2567  (* Problem. cf prev case. *)
2568  @cthulhu
2569| 11: @cthulhu (* symmetric to andbool, waiting to solve pb before copy/paste *)
2570| 12: (* sizeof *)
2571  #ty cases ty
2572  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
2573  | #structname #fieldspec | #unionname #fieldspec | #id ]
2574  #ty' #e #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec_expr
2575  whd in Hexec_expr:(??%?); destruct (Hexec_expr)
2576  normalize in match (typ_of_type ?);
2577  whd in Htranslate:(??%?); destruct (Htranslate)
2578  whd in match (eval_expr ???????);
2579  %{(Vint sz (repr sz (sizeof ty')))} @conj try @refl %2
2580| 13:
2581  #ty #ed #ty' cases ty'
2582  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
2583  | #structname #fieldspec | #unionname #fieldspec | #id ]
2584  #i #Hind #e #Hexpr_vars #Htranslate_addr #cl_blo #cl_off #trace #Hyp_present
2585  #Hexec_lvalue
2586  whd in Hexec_lvalue:(??%?); destruct
2587  [ whd in Htranslate_addr:(??%?);
2588    cases (bind_inversion ????? Htranslate_addr) -Htranslate_addr
2589    * #fieldexpr #Hexpr_vars_field * #Htranslate_field #Htranslate_addr
2590    cases (bind_inversion ????? Htranslate_addr) -Htranslate_addr
2591    #field_off * #Hfield_off whd in ⊢ ((???%) → ?);
2592    #Heq destruct (Heq)
2593    cases Hyp_present -Hyp_present #Hyp_present_fieldexpr #Hyp_present_cst
2594  ]
2595  cases (bind_inversion ????? Hexec_lvalue) -Hexec_lvalue
2596  * * #bl #off #tr * #Hexec_lvalue_ind #Hexec_lvalue   
2597  [ 1: cases (bind_inversion ????? Hexec_lvalue) -Hexec_lvalue #field_off' *
2598       #Hfield_off' whd in ⊢ ((???%) → ?); #H destruct (H)
2599       cases (Hind … Hexpr_vars_field Htranslate_field … Hyp_present_fieldexpr Hexec_lvalue_ind)
2600       #cm_val_field * #Heval_cm #Hvalue_eq
2601       whd in match (eval_expr ???????);
2602       >Heval_cm normalize nodelta
2603       whd in match (eval_expr ???????); whd in match (m_bind ?????);
2604       whd in match (eval_binop ???????); normalize nodelta
2605       cases (value_eq_ptr_inversion … Hvalue_eq) #cm_ptr * #Heq_cm_ptr >Heq_cm_ptr
2606       normalize nodelta #Hptr_translate
2607       %{(Vptr (shift_pointer (bitsize_of_intsize I16) cm_ptr (repr I16 field_off)))}
2608       @conj whd in match (Eapp ??); >(append_nil ? trace) try @refl
2609       %4 whd in Hptr_translate:(??%?) ⊢ (??%?);
2610       cases (E cl_blo) in Hptr_translate; normalize nodelta
2611       [ #H destruct (H) ]
2612       * #BL #OFF normalize nodelta #Heq destruct (Heq)
2613       >Hfield_off' in Hfield_off; normalize in ⊢ ((??%%) → ?);
2614       #H destruct (H)
2615       (* again, mismatch in the size of the integers *)
2616       @cthulhu
2617  | 2: normalize in Hexec_lvalue:(???%); destruct (Hexec_lvalue)
2618       cases (Hind … Hexpr_vars Htranslate_addr ??? Hyp_present Hexec_lvalue_ind)
2619       #cm_val * #Heval_expr >Heval_expr #Hvalue_eq
2620       cases (value_eq_ptr_inversion … Hvalue_eq) #cm_ptr * #Hcm_ptr_eq >Hcm_ptr_eq
2621       #Hpointer_translation
2622       %{cm_val} @conj try assumption
2623       destruct @refl
2624   ]
2625| 14: (* cost label *)
2626  #ty (* cases ty
2627  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
2628  | #structname #fieldspec | #unionname #fieldspec | #id ] *)
2629  #l * #ed #ety
2630  whd in match (typeof ?); whd in match (typeof ?);
2631  #Hind #e' #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec_expr
2632  cases (bind_inversion ????? Htranslate) -Htranslate * #cm_expr
2633  #Hexpr_vars * #Htranslate_ind #Htranslate
2634  cases (bind_inversion ????? Htranslate) -Htranslate * #cm_costexpr #Hexpr_vars_costexpr
2635  * whd in ⊢ ((???%) → ?); #H destruct (H) #Htyp_should_eq
2636  whd in match (typeof ?) in Htyp_should_eq:(??%?);
2637  cases (typ_should_eq_inversion (typ_of_type ety) (typ_of_type ty) ??? Htyp_should_eq)
2638  #Htyp_eq
2639  lapply Htranslate_ind -Htranslate_ind
2640  lapply Hexpr_vars_costexpr -Hexpr_vars_costexpr
2641  lapply Hexec_expr -Hexec_expr lapply Hyp_present -Hyp_present
2642  lapply Hexpr_vars -Hexpr_vars lapply e' -e'
2643  lapply Hind -Hind lapply cm_expr -cm_expr whd in match (typeof ?);
2644  <Htyp_eq
2645  #cm_expr #Hind #e' #Hexpr_vars #Hyp_present #Hexec_expr #Hexpr_vars_costexpr
2646  #Htranslate_ind #Heq lapply (jmeq_to_eq ??? Heq) -Heq #Heq destruct (Heq)
2647  whd in match (eval_expr ???????);
2648  cases (bind_inversion ????? Hexec_expr) * #cm_val #cm_trace * #Hexec_expr_ind
2649  whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2650  cases (Hind cm_expr Hexpr_vars Htranslate_ind … Hyp_present Hexec_expr_ind)
2651  #cm_val' * #Heval_expr' #Hvalue_eq
2652  >Heval_expr' normalize nodelta %{cm_val'} @conj try assumption
2653  >cons_to_append >(nil_append … cm_trace) @refl
2654| 15: *
2655  [ #sz #i | #var_id | #e1 | #e1 | #op #e1 | #op #e1 #e2 | #cast_ty #e1
2656  | #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
2657  #ty normalize in ⊢ (% → ?);
2658  [ 2,3,12: @False_ind
2659  | *: #_ #e' #Hexpr_vars #Htranslate_addr #cl_blo #cl_off #trace #Hyp_present
2660           normalize #Habsurd destruct (Habsurd) ]
2661] qed.
2662
2663
2664axiom clight_cminor_rel : clight_cminor_inv → Clight_state → Cminor_state → Prop.
2665
2666(* Conjectured simulation results
2667
2668   We split these based on the start state:
2669   
2670   1. ‘normal’ states take some [S n] normal steps and simulates them by [S m]
2671      normal steps in Cminor;
2672   2. call and return steps are simulated by a call/return step plus [m] normal
2673      steps (to copy stack allocated parameters / results); and
2674   3. lone cost label steps are simulates by a lone cost label step
2675   
2676   These should allow us to maintain enough structure to identify the Cminor
2677   subtrace corresponding to a measurable Clight subtrace.
2678 *)
2679
2680definition clight_normal : Clight_state → bool ≝
2681λs. match Clight_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
2682
2683definition cminor_normal : Cminor_state → bool ≝
2684λs. match Cminor_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
2685
2686axiom clight_cminor_normal :
2687  ∀INV:clight_cminor_inv.
2688  ∀s1,s1',s2,tr.
2689  clight_cminor_rel INV s1 s1' →
2690  clight_normal s1 →
2691  ¬ Clight_labelled s1 →
2692  ∃n. after_n_steps (S n) … clight_exec (ge_cl INV) s1 (λs.clight_normal s ∧ ¬ Clight_labelled s) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
2693  ∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'.
2694    tr = tr' ∧
2695    clight_cminor_rel INV s2 s2'
2696  ).
2697
2698axiom clight_cminor_call_return :
2699  ∀INV:clight_cminor_inv.
2700  ∀s1,s1',s2,tr.
2701  clight_cminor_rel INV s1 s1' →
2702  match Clight_classify s1 with [ cl_call ⇒ true | cl_return ⇒ true | _ ⇒ false ] →
2703  after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
2704  ∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'.
2705    tr = tr' ∧
2706    clight_cminor_rel INV s2 s2'
2707  ).
2708
2709axiom clight_cminor_cost :
2710  ∀INV:clight_cminor_inv.
2711  ∀s1,s1',s2,tr.
2712  clight_cminor_rel INV s1 s1' →
2713  Clight_labelled s1 →
2714  after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
2715  after_n_steps 1 … Cminor_exec (ge_cm INV) s1' (λs.true) (λtr',s2'.
2716    tr = tr' ∧
2717    clight_cminor_rel INV s2 s2'
2718  ).
2719
Note: See TracBrowser for help on using the repository browser.