source: src/Clight/toCminorCorrectness.ma @ 2582

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

Some progress on CL to CM.

File size: 127.1 KB
RevLine 
[2458]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.
[2460]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.
[2466]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.
[2471]249
250include "Clight/Cexec.ma".
[2489]251include "Clight/abstract.ma".
252include "Cminor/abstract.ma".
[2471]253
[2489]254(* Invariants used in simulation *)
255
[2471]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}.
[2489]266
[2496]267include "Clight/CexecInd.ma".
268include "Clight/frontend_misc.ma".
269include "Clight/memoryInjections.ma".
[2489]270
[2510]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 ≝
[2496]275  λE:embedding.
276  λm,m':mem.
277  λen:cl_env.
278  λvenv:cm_env.
[2510]279  λcminv:clight_cminor_inv.
[2496]280  λsp:block.
281  λvars:var_types.
[2510]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    ].
[2500]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.
[2496]315
[2565]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
[2500]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
[2510]344] qed.
[2496]345
[2510]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.
[2500]360
[2510]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)
[2582]379     [ #Hlookup %1 <(lookup_add_miss SymbolTag ? init_env ?? blo (sym_neq ??? Hneq)) @Hlookup
[2510]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 :
[2545]423  ∀env,env',f,vars,stacksize,globals,var_id.
[2510]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 ? →       
[2545]427  ∀allocty,ty. lookup' vars var_id = OK ? 〈allocty, ty〉 →
[2510]428  ∃r.allocty = Global r.
[2545]429#env #env' #f #vars #stacksize #globals #var_id#Hexec_alloc
430#Hcharacterise #Hlookup_fail #allocty #ty #Hlookup_type_ok
[2510]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
[2527]461
[2554]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
[2582]593lemma classify_sub_inversion :
[2572]594  ∀ty1,ty2.
[2582]595    (∃sz,sg. ty1 = Tint sz sg ∧ ty2 = Tint sz sg ∧ classify_sub ty1 ty2 ≃ sub_case_ii sz sg) ∨
596    (∃n,ty',sz,sg. ty1 = ptr_type ty' n ∧ ty2 = Tint sz sg ∧ classify_sub ty1 ty2 ≃ sub_case_pi n ty' sz sg) ∨
597    (∃ty1',ty2',n1,n2. ty1 = ptr_type ty1' n1 ∧ ty2 = ptr_type ty2' n2 ∧ classify_sub ty1 ty2 ≃ sub_case_pp n1 n2 ty1' ty2') ∨
598    (classify_sub ty1 ty2 = sub_default ty1 ty2).
599#ty1 #ty2
600cases (classify_sub ty1 ty2)
601[ #sz #sg %1 %1 %1 %{sz} %{sg} @conj try @conj try @conj try @refl @refl_jmeq
602| #n #ty #sz #sg %1 %1 %2 %{n} %{ty} %{sz} %{sg} @conj try @conj try @refl @refl_jmeq
603| #n1 #n2 #t1 #t2 %1 %2 %{t1} %{t2} %{n1} %{n2} @conj try @conj try @refl @refl_jmeq
604| #tya #tyb %2 @refl ]
605qed.
[2572]606
[2565]607lemma classify_aop_inversion :
608  ∀ty1,ty2.
609    (∃sz,sg. ty1 = (Tint sz sg) ∧ ty2 = (Tint sz sg) ∧ classify_aop ty1 ty2 ≃ aop_case_ii sz sg) ∨
610    classify_aop ty1 ty2 = aop_default ty1 ty2.
611#ty1 #ty2
612cases (classify_aop ty1 ty2)
613[ #sz #sg %1 %{sz} %{sg} @conj try @conj try @refl_jmeq
614| #ty #ty' %2 @refl ]
[2554]615qed.
616
[2565]617lemma sem_add_ip_inversion :
618  ∀sz,sg,ty',optlen.
619  ∀v1,v2,res.
620  sem_add v1 (Tint sz sg) v2 (ptr_type ty' optlen) = Some ? res →
621  ∃sz',i. v1 = Vint sz' i ∧
[2569]622      ((∃p. v2 = Vptr p ∧ res = Vptr (shift_pointer_n ? p (sizeof ty') sg i)) ∨
[2565]623       (v2 = Vnull ∧ i = (zero ?) ∧ res = Vnull)).
624#tsz #tsg #ty' * [ | #n ]
625*
626[ | #sz' #i' | | #p'
627| | #sz' #i' | | #p' ]
628#v2 #res
629whd in ⊢ ((??%?) → ?);
630#H destruct
631cases v2 in H;
632[ | #sz2' #i2' | | #p2'
633| | #sz2' #i2' | | #p2' ] normalize nodelta
634#H destruct
635[ 1,3:
636  lapply H -H
637  @(eq_bv_elim … i' (zero ?)) normalize nodelta
638  #Hi #Heq destruct (Heq)
639  %{sz'} %{(zero ?)} @conj destruct try @refl
640  %2 @conj try @conj try @refl
641| *: %{sz'} %{i'} @conj try @refl
642  %1 %{p2'} @conj try @refl
643] qed.
[2554]644
[2565]645(* symmetric of the upper one *)
646lemma sem_add_pi_inversion :
647  ∀sz,sg,ty',optlen.
648  ∀v1,v2,res.
649  sem_add v1 (ptr_type ty' optlen) v2 (Tint sz sg) = Some ? res →
650  ∃sz',i. v2 = Vint sz' i ∧
[2569]651      ((∃p. v1 = Vptr p ∧ res = Vptr (shift_pointer_n ? p (sizeof ty') sg i)) ∨
[2565]652       (v1 = Vnull ∧ i = (zero ?) ∧ res = Vnull)).
653#tsz #tsg #ty' * [ | #n ]
654*
655[ | #sz' #i' | | #p'
656| | #sz' #i' | | #p' ]
657#v2 #res
658whd in ⊢ ((??%?) → ?);
659#H destruct
660cases v2 in H; normalize nodelta
661[ | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' ]
662#H destruct
663[ 2,4: %{sz2'} %{i2'} @conj try @refl %1
664  %{p'} @conj try @refl
665| *: lapply H -H
666  @(eq_bv_elim … i2' (zero ?)) normalize nodelta
667  #Hi #Heq destruct (Heq)
668  %{sz2'} %{(zero ?)} @conj destruct try @refl
669  %2 @conj try @conj try @refl
670] qed.
671
672(* Know that addition on integers gives an integer. Notice that there is no correlation
673   between the size in the types and the size of the integer values. *)
674lemma sem_add_ii_inversion :
675  ∀sz,sg.
676  ∀v1,v2,res.
677  sem_add v1 (Tint sz sg) v2 (Tint sz sg) = Some ? res →
678  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
679              res = Vint sz' (addition_n (bitsize_of_intsize sz') i1 i2).
680#sz #sg
681*
682[ | #sz' #i' | | #p' ]
683#v2 #res
684whd in ⊢ ((??%?) → ?); normalize in match (classify_add ??);
685cases sz cases sg normalize nodelta
686#H destruct
687cases v2 in H; normalize nodelta
688#H1 destruct
689#H2 destruct #Heq %{sz'} lapply Heq -Heq
690cases sz' in i'; #i' 
691whd in match (intsize_eq_elim ???????);
692cases H1 in H2; #j' normalize nodelta
693#Heq destruct (Heq)
694%{i'} %{j'} @conj try @conj try @conj try @refl
[2554]695qed.
696
[2582]697lemma sem_sub_pp_inversion :
698  ∀ty1,ty2,n1,n2.
699  ∀v1,v2,res.
700  sem_sub v1 (ptr_type ty1 n1) v2 (ptr_type ty2 n2) = Some ? res →
701  (∃p1,p2,i. v1 =  Vptr p1 ∧ v2 = Vptr p2 ∧ pblock p1 = pblock p2 ∧
702             division_u ? (sub_offset ? (poff p1) (poff p2)) (repr (sizeof ty1)) = Some ? i ∧
703             res = Vint I32 i) ∨
704  (v1 =  Vnull ∧ v2 = Vnull ∧ res = Vint I32 (zero ?)).
705#ty1 #ty2 #n1 #n2
706cases n1 cases n2
707[ | #n1 | #n2 | #n2 #n1 ]
708*
709[ | #sz #i | | #p
710| | #sz #i | | #p
711| | #sz #i | | #p
712| | #sz #i | | #p ]
713#v2 #res
714whd in ⊢ ((??%?) → ?);
715#H1 destruct
716cases v2 in H1;
717[ | #sz' #i' | | #p'
718| | #sz' #i' | | #p'
719| | #sz' #i' | | #p'
720| | #sz' #i' | | #p'
721| | #sz' #i' | | #p'
722| | #sz' #i' | | #p'
723| | #sz' #i' | | #p'
724| | #sz' #i' | | #p' ]
725normalize nodelta
726#H2 destruct
727try /4 by or_introl, or_intror, conj, refl/
728%1 %{p} %{p'}
729cases (if_opt_inversion ???? H2)
730#Hblocks_eq -H2
731@(eqb_elim … (sizeof ty1) 0) normalize nodelta
732#Heq_sizeof destruct #Heq destruct
733cases (division_u ???) in Heq; normalize nodelta
734#H3 destruct #H4 destruct
735%{H3} try @conj try @conj try @conj try @conj try @refl
736@(eq_block_to_refl … Hblocks_eq)
737qed.
738
739
740lemma sem_sub_pi_inversion :
741  ∀sz,sg,ty',optlen.
742  ∀v1,v2,res.
743  sem_sub v1 (ptr_type ty' optlen) v2 (Tint sz sg) = Some ? res →
744  ∃sz',i. v2 = Vint sz' i ∧
745      ((∃p. v1 = Vptr p ∧ res = Vptr (neg_shift_pointer_n ? p (sizeof ty') sg i)) ∨
746       (v1 = Vnull ∧ i = (zero ?) ∧ res = Vnull)).
747#tsz #tsg #ty' * [ | #n ]
748*
749[ | #sz' #i' | | #p'
750| | #sz' #i' | | #p' ]
751#v2 #res
752whd in ⊢ ((??%?) → ?);
753#H destruct
754cases v2 in H; normalize nodelta
755[ | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' | | #sz2' #i2' | | #p2' ]
756#H destruct
757[ 2,4: %{sz2'} %{i2'} @conj try @refl %1
758  %{p'} @conj try @refl
759| *: lapply H -H
760  @(eq_bv_elim … i2' (zero ?)) normalize nodelta
761  #Hi #Heq destruct (Heq)
762  %{sz2'} %{(zero ?)} @conj destruct try @refl
763  %2 @conj try @conj try @refl
764] qed.
765
766
767lemma sem_sub_ii_inversion :
768  ∀sz,sg.
769  ∀v1,v2,res.
770  sem_sub v1 (Tint sz sg) v2 (Tint sz sg) = Some ? res →
771  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
772              res = Vint sz' (subtraction (bitsize_of_intsize sz') i1 i2).
773#sz #sg *             
774[ | #sz' #i' | | #p' ]
775#v2 #res
776whd in ⊢ ((??%?) → ?); whd in match (classify_sub ??);
777cases sz cases sg normalize nodelta
778#H destruct
779cases v2 in H; normalize nodelta
780#H1 destruct
781#H2 destruct #Heq %{sz'} lapply Heq -Heq
782cases sz' in i'; #i' 
783whd in match (intsize_eq_elim ???????);
784cases H1 in H2; #j' normalize nodelta
785#Heq destruct (Heq)
786%{i'} %{j'} @conj try @conj try @conj try @refl
787qed.
788
789
[2565]790lemma sem_mul_inversion :
791  ∀sz,sg.
792  ∀v1,v2,res.
793  sem_mul v1 (Tint sz sg) v2 (Tint sz sg) = Some ? res →
794  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
795              res = Vint sz' (short_multiplication ? i1 i2).
796#sz #sg *
797[ | #sz' #i' | | #p' ]
798#v2 #res
799whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
800cases sz cases sg normalize nodelta
801#H destruct
802cases v2 in H; normalize nodelta
803#H1 destruct
804#H2 destruct #Heq %{sz'} lapply Heq -Heq
805cases sz' in i'; #i' 
806whd in match (intsize_eq_elim ???????);
807cases H1 in H2; #j' normalize nodelta
808#Heq destruct (Heq)
809%{i'} %{j'} @conj try @conj try @conj try @refl
810qed.
811
812
813lemma sem_div_inversion_s :
814  ∀sz.
815  ∀v1,v2,res.
816  sem_div v1 (Tint sz Signed) v2 (Tint sz Signed) = Some ? res →
817  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
818              match division_s ? i1 i2 with
819              [ Some q ⇒  res =  (Vint sz' q)
820              | None ⇒ False ].
821#sz *
822[ | #sz' #i' | | #p' ]
823#v2 #res
824whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
825>type_eq_dec_true normalize nodelta
826#H destruct
827cases v2 in H; normalize nodelta
828[ | #sz2' #i2' | | #p2' ]
829#Heq destruct
830%{sz'}
831lapply Heq -Heq
832cases sz' in i'; #i' 
833whd in match (intsize_eq_elim ???????);
834cases sz2' in i2'; #i2' normalize nodelta
835whd in match (option_map ????); #Hdiv destruct
836%{i'} %{i2'} @conj try @conj try @conj try @refl
837cases (division_s ???) in Hdiv;
838[ 2,4,6: #bv ] normalize #H destruct (H) try @refl
839qed.
840
841lemma sem_div_inversion_u :
842  ∀sz.
843  ∀v1,v2,res.
844  sem_div v1 (Tint sz Unsigned) v2 (Tint sz Unsigned) = Some ? res →
845  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
846              match division_u ? i1 i2 with
847              [ Some q ⇒  res =  (Vint sz' q)
848              | None ⇒ False ].
849#sz *
850[ | #sz' #i' | | #p' ]
851#v2 #res
852whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
853>type_eq_dec_true normalize nodelta
854#H destruct
855cases v2 in H; normalize nodelta
856[ | #sz2' #i2' | | #p2' ]
857#Heq destruct
858%{sz'}
859lapply Heq -Heq
860cases sz' in i'; #i' 
861whd in match (intsize_eq_elim ???????);
862cases sz2' in i2'; #i2' normalize nodelta
863whd in match (option_map ????); #Hdiv destruct
864%{i'} %{i2'} @conj try @conj try @conj try @refl
865cases (division_u ???) in Hdiv;
866[ 2,4,6: #bv ] normalize #H destruct (H) try @refl
867qed.
868
[2572]869lemma sem_mod_inversion_s :
870  ∀sz.
871  ∀v1,v2,res.
872  sem_mod v1 (Tint sz Signed) v2 (Tint sz Signed) = Some ? res →
873  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
874              match modulus_s ? i1 i2 with
875              [ Some q ⇒  res =  (Vint sz' q)
876              | None ⇒ False ].
877#sz *
878[ | #sz' #i' | | #p' ]
879#v2 #res
880whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
881>type_eq_dec_true normalize nodelta
882#H destruct
883cases v2 in H; normalize nodelta
884[ | #sz2' #i2' | | #p2' ]
885#Heq destruct
886%{sz'}
887lapply Heq -Heq
888cases sz' in i'; #i' 
889whd in match (intsize_eq_elim ???????);
890cases sz2' in i2'; #i2' normalize nodelta
891whd in match (option_map ????); #Hdiv destruct
892%{i'} %{i2'} @conj try @conj try @conj try @refl
893cases (modulus_s ???) in Hdiv;
894[ 2,4,6: #bv ] normalize #H destruct (H) try @refl
895qed.
896
897lemma sem_mod_inversion_u :
898  ∀sz.
899  ∀v1,v2,res.
900  sem_mod v1 (Tint sz Unsigned) v2 (Tint sz Unsigned) = Some ? res →
901  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
902              match modulus_u ? i1 i2 with
903              [ Some q ⇒  res =  (Vint sz' q)
904              | None ⇒ False ].
905#sz *
906[ | #sz' #i' | | #p' ]
907#v2 #res
908whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??);
909>type_eq_dec_true normalize nodelta
910#H destruct
911cases v2 in H; normalize nodelta
912[ | #sz2' #i2' | | #p2' ]
913#Heq destruct
914%{sz'}
915lapply Heq -Heq
916cases sz' in i'; #i' 
917whd in match (intsize_eq_elim ???????);
918cases sz2' in i2'; #i2' normalize nodelta
919whd in match (option_map ????); #Hdiv destruct
920%{i'} %{i2'} @conj try @conj try @conj try @refl
921cases (modulus_u ???) in Hdiv;
922[ 2,4,6: #bv ] normalize #H destruct (H) try @refl
923qed.
924
925lemma sem_and_inversion :
926  ∀v1,v2,res.
927  sem_and v1 v2 = Some ? res →
928  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
929              res = Vint sz' (conjunction_bv ? i1 i2).
930*
931[ | #sz' #i' | | #p' ]
932#v2 #res
933whd in ⊢ ((??%?) → ?);
934#H destruct
935cases v2 in H; normalize nodelta
936[ | #sz2' #i2' | | #p2' ]
937#Heq destruct
938%{sz'}
939lapply Heq -Heq
940cases sz' in i'; #i' 
941whd in match (intsize_eq_elim ???????);
942cases sz2' in i2'; #i2' normalize nodelta
943#H destruct
944%{i'} %{i2'} @conj try @conj try @conj try @refl
945qed.
946
947lemma sem_or_inversion :
948  ∀v1,v2,res.
949  sem_or v1 v2 = Some ? res →
950  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
951              res = Vint sz' (inclusive_disjunction_bv ? i1 i2).
952*
953[ | #sz' #i' | | #p' ]
954#v2 #res
955whd in ⊢ ((??%?) → ?);
956#H destruct
957cases v2 in H; normalize nodelta
958[ | #sz2' #i2' | | #p2' ]
959#Heq destruct
960%{sz'}
961lapply Heq -Heq
962cases sz' in i'; #i' 
963whd in match (intsize_eq_elim ???????);
964cases sz2' in i2'; #i2' normalize nodelta
965#H destruct
966%{i'} %{i2'} @conj try @conj try @conj try @refl
967qed.
968
969lemma sem_xor_inversion :
970  ∀v1,v2,res.
971  sem_xor v1 v2 = Some ? res →
972  ∃sz',i1,i2. v1 =  Vint sz' i1 ∧ v2 = Vint sz' i2 ∧
973              res = Vint sz' (exclusive_disjunction_bv ? i1 i2).
974*
975[ | #sz' #i' | | #p' ]
976#v2 #res
977whd in ⊢ ((??%?) → ?);
978#H destruct
979cases v2 in H; normalize nodelta
980[ | #sz2' #i2' | | #p2' ]
981#Heq destruct
982%{sz'}
983lapply Heq -Heq
984cases sz' in i'; #i' 
985whd in match (intsize_eq_elim ???????);
986cases sz2' in i2'; #i2' normalize nodelta
987#H destruct
988%{i'} %{i2'} @conj try @conj try @conj try @refl
989qed.
990
991lemma sem_shl_inversion :
992  ∀v1,v2,res.
993  sem_shl v1 v2 = Some ? res →
994  ∃sz1,sz2,i1,i2.
995              v1 =  Vint sz1 i1 ∧ v2 = Vint sz2 i2 ∧
996              res = Vint sz1 (shift_left bool (bitsize_of_intsize sz1)
997                                  (nat_of_bitvector (bitsize_of_intsize sz2) i2) i1 false) ∧
998              lt_u (bitsize_of_intsize sz2) i2
999                   (bitvector_of_nat (bitsize_of_intsize sz2) (bitsize_of_intsize sz1)) = true.
1000*
1001[ | #sz' #i' | | #p' ]
1002#v2 #res
1003whd in ⊢ ((??%?) → ?);
1004#H destruct
1005cases v2 in H; normalize nodelta
1006[ | #sz2' #i2' | | #p2' ]
1007#Heq destruct
1008%{sz'} %{sz2'}
1009lapply (if_opt_inversion ???? Heq) * #Hlt_u #Hres
1010%{i'} %{i2'}
1011>Hlt_u destruct (Hres) @conj try @conj try @conj try @refl
1012qed.
1013
1014lemma sem_shr_inversion :
1015  ∀v1,v2,sz,sg,res.
1016  sem_shr v1 (Tint sz sg) v2 (Tint sz sg) = Some ? res →
1017  ∃sz1,sz2,i1,i2.
1018              v1 =  Vint sz1 i1 ∧ v2 = Vint sz2 i2 ∧
1019              lt_u (bitsize_of_intsize sz2) i2
1020                   (bitvector_of_nat (bitsize_of_intsize sz2) (bitsize_of_intsize sz1)) = true ∧
1021              match sg with
1022              [ Signed ⇒
1023                 res =
1024                   (Vint sz1
1025                    (shift_right bool (7+pred_size_intsize sz1*8)
1026                     (nat_of_bitvector (bitsize_of_intsize sz2) i2) i1
1027                     (head' bool (7+pred_size_intsize sz1*8) i1)))               
1028              | Unsigned ⇒
1029                 res =
1030                   (Vint sz1
1031                    (shift_right bool (7+pred_size_intsize sz1*8)
1032                     (nat_of_bitvector (bitsize_of_intsize sz2) i2) i1 false))
1033              ].
1034*
1035[ | #sz' #i' | | #p' ]
1036#v2 #sz * #res
1037whd in ⊢ ((??%?) → ?);
1038whd in match (classify_aop ??);
1039>type_eq_dec_true normalize nodelta
1040#H destruct
1041cases v2 in H; normalize nodelta
1042[ | #sz2' #i2' | | #p2'
1043| | #sz2' #i2' | | #p2' ]
1044#Heq destruct
1045%{sz'} %{sz2'}
1046lapply (if_opt_inversion ???? Heq) * #Hlt_u #Hres
1047%{i'} %{i2'}
1048>Hlt_u destruct (Hres) @conj try @conj try @conj try @refl
1049qed.
1050
1051lemma complete_cmp_inversion :
1052  ∀ty:type.
1053  ∀e:expr (ASTint I8 Unsigned).
1054  ∀r:expr (typ_of_type ty).
1055   complete_cmp ty e = return r →
1056   ∃sz,sg. ty = Tint sz sg ∧
1057           r ≃ Op1 (ASTint I8 Unsigned) (ASTint sz sg) (Ocastint I8 Unsigned sz sg) e.
1058*
1059[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1060| #structname #fieldspec | #unionname #fieldspec | #id ]
1061#e whd in match (typ_of_type ?);
1062#r whd in ⊢ ((??%%) → ?);
1063#H destruct
1064%{sz} %{sg} @conj try @refl @refl_jmeq
1065qed.
1066
1067
1068lemma sem_cmp_int_inversion :
1069  ∀v1,v2,sz,sg,op,m,res.
1070   sem_cmp op v1 (Tint sz sg) v2 (Tint sz sg) m = Some ? res →
1071   ∃sz,i1,i2. v1 = Vint sz i1 ∧
1072              v2 = Vint sz i2 ∧
1073    match sg with
1074    [ Unsigned ⇒ of_bool (cmpu_int ? op i1 i2) = res
1075    | Signed   ⇒ of_bool (cmp_int ? op i1 i2) = res
1076    ].
1077#v1 #v2 #sz0 #sg #op * #contents #next #Hnext #res
1078whd in ⊢ ((??%?) → ?);
1079whd in match (classify_cmp ??); >type_eq_dec_true normalize nodelta
1080cases v1
1081[ | #sz #i | | #p ] normalize nodelta
1082#H destruct
1083cases v2 in H;
1084[ | #sz' #i' | | #p' ] normalize nodelta
1085#H destruct lapply H -H
1086cases sz in i; #i
1087cases sz' in i'; #i' cases sg normalize nodelta
1088whd in match (intsize_eq_elim ???????); #H destruct
1089[ 1,2: %{I8}
1090| 3,4: %{I16}
1091| 5,6: %{I32} ] 
1092%{i} %{i'} @conj try @conj try @refl
1093qed.
1094
1095lemma typ_of_ptr_type : ∀ty',n. typ_of_type (ptr_type ty' n) = ASTptr.
1096#ty' * // qed.
1097
1098lemma sem_cmp_ptr_inversion :
1099  ∀v1,v2,ty',n,op,m,res.
1100   sem_cmp op v1 (ptr_type ty' n) v2 (ptr_type ty' n) m = Some ? res →
1101   (∃p1,p2. v1 = Vptr p1 ∧ v2 = Vptr p2 ∧
1102                 valid_pointer m p1 = true ∧
1103                 valid_pointer m p2 = true ∧
1104                 (if eq_block (pblock p1) (pblock p2)
1105                  then Some ? (of_bool (cmp_offset op (poff p1) (poff p2)))
1106                  else sem_cmp_mismatch op) = Some ? res) ∨
1107   (∃p1. v1 = Vptr p1 ∧ v2 = Vnull ∧ sem_cmp_mismatch op = Some ? res) ∨                 
1108   (∃p2. v1 = Vnull ∧ v2 = Vptr p2 ∧ sem_cmp_mismatch op = Some ? res) ∨
1109   (v1 = Vnull ∧ v2 = Vnull ∧ sem_cmp_match op = Some ? res).
1110* [ | #sz #i | | #p ] normalize nodelta
1111#v2 #ty' #n #op
1112* #contents #nextblock #Hnextblock #res whd in ⊢ ((??%?) → ?);
1113whd in match (classify_cmp ??); cases n normalize nodelta
1114[ 2,4,6,8: #array_len ]
1115whd in match (ptr_type ty' ?);
1116whd in match (if_type_eq ?????);
1117>type_eq_dec_true normalize nodelta
1118#H destruct
1119cases v2 in H; normalize nodelta
1120[ | #sz' #i' | | #p'
1121| | #sz' #i' | | #p'
1122| | #sz' #i' | | #p'
1123| | #sz' #i' | | #p' ]
1124#H destruct
1125try /6 by or_introl, or_intror, ex_intro, conj/
1126[ 1: %1 %1 %2 %{p} @conj try @conj //
1127| 3: %1 %1 %2 %{p} @conj try @conj //
1128| *: %1 %1 %1 %{p} %{p'}
1129     cases (valid_pointer (mk_mem ???) p) in H; normalize nodelta
1130     cases (valid_pointer (mk_mem contents nextblock Hnextblock) p') normalize nodelta #H
1131     try @conj try @conj try @conj try @conj try @conj try @refl try @H
1132     destruct
1133] qed.
1134
1135lemma pointer_translation_eq_block :
1136  ∀E,p1,p2,p1',p2'.
1137  pointer_translation p1 E = Some ? p1' →
1138  pointer_translation p2 E = Some ? p2' →
1139  eq_block (pblock p1) (pblock p2) = true →
1140  eq_block (pblock p1') (pblock p2') = true.
1141#E * #b1 #o1 * #b2 #o2 * #b1' #o1' * #b2' #o2'
1142#H1 #H2 #Heq_block
1143lapply (eq_block_to_refl … Heq_block) #H destruct (H)
1144lapply H1 lapply H2 -H1 -H2
1145whd in ⊢ ((??%?) → (??%?) → ?);
1146cases (E b2) normalize nodelta
1147[ #Habsurd destruct ]
1148* #bx #ox normalize nodelta #Heq1 #Heq2 destruct
1149@eq_block_b_b
1150qed.
1151
1152
[2582]1153(* avoid a case analysis on type inside of a big proof *)
1154lemma match_type_inversion_aux : ∀ty,e,f.
1155 match ty in type return λty':type.(res (expr (typ_of_type ty'))) with 
1156  [Tvoid⇒Error (expr (ASTint I32 Unsigned)) (msg TypeMismatch)
1157  |Tint (sz:intsize)   (sg:signedness)⇒ f sz sg
1158  |Tpointer (x:type)⇒
1159   Error (expr (typ_of_type (Tpointer x))) (msg TypeMismatch)
1160  |Tarray (x:type)   (y:ℕ)⇒
1161   Error (expr (typ_of_type (Tarray x y))) (msg TypeMismatch)
1162  |Tfunction (x:typelist)   (y:type)⇒
1163   Error (expr (typ_of_type (Tfunction x y))) (msg TypeMismatch)
1164  |Tstruct (x:ident)   (y:fieldlist)⇒
1165   Error (expr (ASTint I32 Unsigned)) (msg TypeMismatch)
1166  |Tunion (x:ident)   (y:fieldlist)⇒
1167   Error (expr (ASTint I32 Unsigned)) (msg TypeMismatch)
1168  |Tcomp_ptr (x:ident)⇒
1169   Error (expr (typ_of_type (Tcomp_ptr x))) (msg TypeMismatch)]
1170  = OK ? e →
1171  ∃sz,sg. ty = Tint sz sg ∧ (f sz sg ≃ OK ? e).
1172*
1173[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1174| #structname #fieldspec | #unionname #fieldspec | #id ]
1175whd in match (typ_of_type Tvoid);
1176#e #f normalize nodelta #Heq destruct
1177%{sz} %{sg} % try @refl >Heq %
1178qed.
1179
1180 
1181
[2572]1182(* The two following lemmas are just noise. *)
1183
[2565]1184lemma expr_vars_fix_ptr_type :
1185  ∀ty',optlen.
1186  ∀e:expr (typ_of_type (ptr_type ty' optlen)).
1187  ∀P.
1188   expr_vars ASTptr (fix_ptr_type ty' optlen e) P →
1189   expr_vars
1190    (typ_of_type
1191        match optlen 
1192        in option 
1193        return λ_:(option ℕ).type with 
1194        [None⇒Tpointer ty'
1195        |Some (n':ℕ)⇒ Tarray ty' n']) e P.
1196#ty' * normalize
1197[ 2: #n ]
1198#e #P
1199@expr_vars_mp //
1200qed.
1201
1202lemma eval_expr_rewrite_aux :
1203  ∀genv.
1204  ∀optlen.
1205  ∀ty'.
1206  ∀e.
1207  ∀cm_env.
1208  ∀H.
1209  ∀sp.
1210  ∀m.
1211  ∀res.
1212  (eval_expr genv
1213             (typ_of_type
1214                 match optlen in option return λ_:(option ℕ).type with 
1215                 [None⇒Tpointer ty'|Some (n':ℕ)⇒Tarray ty' n'])
1216             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 →
1217   eval_expr genv ASTptr (fix_ptr_type ty' optlen e) cm_env H sp m = OK ? res.
1218#genv * [ 2: #n ] normalize nodelta
1219#ty' normalize in match (typ_of_type ?);
1220#e #cm_env whd in match (fix_ptr_type ???);
1221#H #sp #m #res #H @H
1222qed.
1223
1224
1225(* TODOs : there are some glitches between clight and cminor :
1226 * 1) some issues with shortcut and/or: the clight code returns a 32 bit constant
1227      in the shortcut case, the cminor code returns directly the outcome of the
1228      evaluated expr, with a possibly different size.
1229   2) another glitch is for the integer/pointer additions: Clight always performs
1230      a sign extension on i in expressions (ptr + i) whereas Cminor case splits on
1231      the sign of i, producing either a sign extension or a zero extension.
[2572]1232   3) something similar to 1) happens for binary comparison operators. Clight generates
1233      systematically a 32 bit value for the outcome of the comparison and lives with it,
1234      but toCminor actually generates something 8 bit and casts it back to the context type.
1235   4) we need some proof that we don't blow the stack during the transformation. Otherwise,
1236      a problem appears when we prove semantics preservation for pointer < comparison
1237      (we might wrap up the rhs and end SNAFU).
[2565]1238 *)
[2578]1239 
[2496]1240lemma eval_expr_sim :
[2578]1241  (* [cl_cm_inv] maps CL globals to CM globals, including functions *)
1242  ∀cl_cm_inv  : clight_cminor_inv.
1243  (* current function (defines local environment) *)
1244  ∀f          : function.
1245  (* [alloctype] maps variables to their allocation type (global, stack, register) *)
1246  ∀alloctype  : var_types.
1247  ∀stacksize  : ℕ.
1248  ∀alloc_hyp  : characterise_vars (globals cl_cm_inv) f = 〈alloctype, stacksize〉.
1249  (* environments *)
1250  ∀cl_env     : cl_env.
1251  ∀cm_env     : cm_env.
1252  (* Characterise clight environment. Needed to prove that some variable is either a parameter or a local.  *)
1253  ∀cl_env_hyp : ∃m,m'. exec_alloc_variables empty_env m (fn_params f @ fn_vars f) = 〈cl_env,m'〉.
1254  (* CL and CM memories *)
1255  ∀cl_m       : mem.
1256  ∀cm_m       : mem.
1257  (* memory injection and matching *)
1258  ∀embed      : embedding.
1259  ∀injection  : memory_inj embed cl_m cm_m.
1260  ∀stackptr   : block.
1261  ∀matching   : memory_matching embed cl_m cm_m cl_env cm_env cl_cm_inv stackptr alloctype.
[2545]1262  (* clight expr to cminor expr *)
[2496]1263  (∀(e:expr).
[2545]1264   ∀(e':CMexpr (typ_of_type (typeof e))).
[2496]1265   ∀Hexpr_vars.
[2578]1266   translate_expr alloctype e = OK ? («e', Hexpr_vars») →
[2500]1267   ∀cl_val,trace,Hyp_present.
[2578]1268   exec_expr (ge_cl … cl_cm_inv) cl_env cl_m e = OK ? 〈cl_val, trace〉 →
1269   ∃cm_val. eval_expr (ge_cm cl_cm_inv) (typ_of_type (typeof e)) e' cm_env Hyp_present stackptr cm_m = OK ? 〈trace, cm_val〉 ∧
1270            value_eq embed cl_val cm_val) ∧
[2545]1271   (* clight /lvalue/ to cminor /expr/ *)
[2496]1272  (∀ed,ty.
[2545]1273   ∀(e':CMexpr ASTptr).
[2496]1274   ∀Hexpr_vars.
[2578]1275   translate_addr alloctype (Expr ed ty) = OK ? («e', Hexpr_vars») →
[2527]1276   ∀cl_blo,cl_off,trace,Hyp_present.
[2578]1277   exec_lvalue' (ge_cl … cl_cm_inv) cl_env cl_m ed ty = OK ? 〈cl_blo, cl_off, trace〉 →
1278   ∃cm_val. eval_expr (ge_cm cl_cm_inv) ASTptr e' cm_env Hyp_present stackptr cm_m = OK ? 〈trace, cm_val〉 ∧
1279            value_eq embed (Vptr (mk_pointer cl_blo cl_off)) cm_val).
1280#inv #f #vars #stacksize #Hcharacterise #cl_env #cm_env #Hexec_alloc #cl_m #cm_m #E #Hinj #sp #Hlocal_matching
[2496]1281@expr_lvalue_ind_combined
[2565]1282[ 7: (* binary ops *)
1283     #ty
1284     #op #e1 #e2
1285     #Hind1 #Hind2 #e' #Hexpr_vars #Htranslate
1286     cases (bind_inversion ????? Htranslate) -Htranslate
1287     * #lhs #Hexpr_vars_lhs * #Htranslate_lhs #Htranslate
1288     cases (bind_inversion ????? Htranslate) -Htranslate
1289     * #rhs #Hexpr_vars_rhs * #Htranslate_rhs
1290     whd in ⊢ ((??%?) → ?);
1291     #Htranslate_binop
1292     cases (bind_as_inversion ????? Htranslate_binop) -Htranslate_binop
1293     #translated_binop * #Htranslated_binop whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1294     #cl_val #trace #Hyp_present #Hexec
1295     (* dump all the useless stuff after the turnstyle, in order to perform rewrites and so on. *)
1296     lapply (Hind1 lhs Hexpr_vars_lhs Htranslate_lhs) -Hind1
1297     lapply (Hind2 rhs Hexpr_vars_rhs Htranslate_rhs) -Hind2
1298     lapply Hyp_present -Hyp_present
1299     lapply Htranslate_lhs -Htranslate_lhs
1300     lapply Htranslate_rhs -Htranslate_rhs
1301     lapply Hexpr_vars_lhs -Hexpr_vars_lhs
1302     lapply Hexpr_vars_rhs -Hexpr_vars_rhs
1303     lapply Hexec -Hexec
1304     lapply Htranslated_binop -Htranslated_binop
1305     lapply rhs -rhs lapply lhs -lhs
1306     (* end of dump *)
1307     cases op
1308     whd in ⊢ (? → ? → (??%?) → ?);
1309     [ 1: (* add *)
1310       lapply (classify_add_inversion (typeof e1) (typeof e2))
1311       * [ 2: #Hclassify >Hclassify normalize nodelta #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
1312       (* trying to factorise as much stuff as possible ... *)
1313       lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2 whd in match (typeof ?); #e'
1314       * [ 1: * ]
1315       [ 1: * #sz * #sg * *
1316       | 2: * #optlen * #ty' * #sz * #sg * *
1317       | 3: * #optlen * #sz * #sg * #ty' * * ]
1318       whd in match (typeof ?) in ⊢ (% → % → ?);
1319       #Htypeof_e1 #Htypeof_e2
1320       >Htypeof_e1 >Htypeof_e2
1321       #Hclassify
1322       lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify
1323       normalize nodelta
1324       whd in match (typeof ?) in ⊢ (% → % → %);
1325       whd in match (typ_of_type (Tint ??));
1326       #lhs #rhs #Htyp_should_eq
1327       [ 1:   cases (typ_should_eq_inversion (ASTint sz sg) (typ_of_type ty) … Htyp_should_eq)
1328       | 2,3: cases (typ_should_eq_inversion ASTptr (typ_of_type ty) … Htyp_should_eq) ]
1329       -Htyp_should_eq
1330       #Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') -Heq_e' #Heq_e'
1331       <Heq_e' -Heq_e'
1332       #Hexec
1333       #Hexpr_vars_rhs #Hexpr_vars_lhs
1334       #Htranslate_rhs #Htranslate_lhs
1335       * [ #Hyp_present_lhs #Hyp_present_rhs
1336         | #Hyp_present_lhs * #Hyp_present_rhs #Hyp_present_cst
[2582]1337         | * #Hyp_present_lhs #Hyp_present_cst #Hyp_present_rhs ]
[2565]1338       whd in match (typeof ?);
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       [ 1,2: lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
1350       | 3: lapply (Hind_rhs … (expr_vars_fix_ptr_type … Hyp_present_rhs) Hexec_rhs) ]
1351       * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
1352       [ 1,3: lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
1353       | 2: lapply (Hind_lhs … (expr_vars_fix_ptr_type … Hyp_present_lhs) Hexec_lhs) ]
1354       * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
1355       whd in match (eval_expr ???????);
1356       whd in match (proj1 ???);
1357       [ 3: lapply (eval_expr_rewrite_aux … Heval_lhs) -Heval_lhs #Heval_lhs ]
1358       [ 1,2: >Heval_lhs normalize nodelta
1359              whd in match (eval_expr ???????);
1360              whd in match (eval_expr ???????);
1361              >Heval_rhs normalize nodelta
1362              whd in match (m_bind ?????);
1363       | 3: >(eval_expr_rewrite_aux … Heval_rhs) normalize nodelta
1364            whd in match (eval_expr ???????);
1365            whd in match (eval_expr ???????);
1366            >Heval_lhs normalize nodelta
1367       ]
1368       whd in match (proj1 ???); whd in match (proj2 ???);
1369       [ 2: (* standard int/int addition. *)
1370            whd in match (eval_binop ???????);
1371            whd in Hsem_binary:(??%?);
1372            lapply (add_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
1373            * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
1374            cases (sem_add_ii_inversion … Hsem_binary_translated)
1375            #cm_vsz * #cm_lhs_v * #cm_rhs_v * *
1376            #Hcm_lhs #Hcm_rhs #Hcm_val
1377            destruct (Hcm_lhs) destruct (Hcm_rhs) normalize nodelta
1378            >intsize_eq_elim_true normalize nodelta
1379            %{(Vint cm_vsz (addition_n (bitsize_of_intsize cm_vsz) cm_lhs_v cm_rhs_v))}
1380            @conj try @refl lapply Hsem_binary_translated
1381            whd in ⊢ ((??%?) → ?); normalize nodelta normalize in match (classify_add ??);
1382            >inttyp_eq_elim_true' normalize nodelta
1383            >intsize_eq_elim_true #H destruct (H) @Hvalue_eq_res
1384       | *: (* pointer/int int/pointer addition *)
1385            whd in Hsem_binary:(??%?);
1386            lapply (add_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
1387            * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
[2582]1388            (* >> *)             
1389            [ lapply (sem_add_pi_inversion … Hsem_binary_translated)
1390              * #cm_vsz * #cm_rhs_v * #Hcm_rhs *
1391              [ * #lhs_ptr * #Hcm_lhs_ptr #Hcm_val_shptr
1392              | * * #lhs_null #Hcm_rhs_zero #Hcm_val_null ]
1393            | lapply (sem_add_ip_inversion … Hsem_binary_translated)
1394              * #cm_vsz * #cm_lhs_v * #Hcm_lhs *
1395              [ * #rhs_ptr * #Hcm_rhs_ptr #Hcm_val_shptr
1396              | * * #rhs_null #Hcm_lhs_zero #Hcm_val_null ]
1397            ]
1398            destruct
1399            whd in match (eval_unop ????);
1400            @(match sg
1401              return λs. sg = s → ?
1402              with
1403              [ Unsigned ⇒ λHsg. ?
1404              | Signed ⇒ λHsg. ?
1405              ] (refl ??)) normalize nodelta
1406            whd in match (eval_binop ???????);
1407            whd in match (m_bind ?????);
1408            [ 1: %{(Vptr (shift_pointer (bitsize_of_intsize I16) lhs_ptr
1409                            (short_multiplication (bitsize_of_intsize I16)
1410                            (sign_ext (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16) cm_rhs_v)
1411                            (repr I16 (sizeof ty')))))}
1412            | 2: %{(Vptr (shift_pointer (bitsize_of_intsize I16) lhs_ptr
1413                          (short_multiplication (bitsize_of_intsize I16)
1414                          (zero_ext (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16) cm_rhs_v)
1415                          (repr I16 (sizeof ty')))))}
1416            | 5: %{(Vptr (shift_pointer (bitsize_of_intsize I16) rhs_ptr
1417                          (short_multiplication (bitsize_of_intsize I16)
1418                          (sign_ext (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16) cm_lhs_v)
1419                          (repr I16 (sizeof ty')))))}
1420            | 6: %{(Vptr (shift_pointer (bitsize_of_intsize I16) rhs_ptr
1421                          (short_multiplication (bitsize_of_intsize I16)
1422                          (zero_ext (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16) cm_lhs_v)
1423                          (repr I16 (sizeof ty')))))}
1424            ]
1425            [ 1,2,3,4: @conj whd in match (E0);
1426                        whd in match (Eapp trace_rhs ?);
1427                        whd in match (Eapp trace_lhs ?);
1428                        >(append_nil … trace_rhs) try @refl
1429                        >(append_nil … trace_lhs) try @refl
1430                        @(value_eq_triangle_diagram … Hvalue_eq_res)
1431                        whd in match (shift_pointer_n ?????);
1432                        whd in match (shift_offset_n ?????);
1433                        >Hsg normalize nodelta
1434                        >commutative_short_multiplication
1435                        whd in match (shift_pointer ???);
1436                        whd in match (shift_offset ???);
1437                        >sign_ext_same_size @refl
1438           | 5,7: >(sign_ext_zero (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16))
1439           | 6,8: >(zero_ext_zero (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16)) ]           
1440           >(short_multiplication_zero 16  (repr I16 (sizeof ty')))
1441           >(eq_bv_true … (zero 16)) normalize nodelta %{Vnull} @conj try assumption
1442           normalize >append_nil try @refl
[2565]1443       ]
[2582]1444     | 2: (* subtraction cases: not quite identical to add. *)
1445       lapply (classify_sub_inversion (typeof e1) (typeof e2))
1446       * [ 2: #Hclassify >Hclassify normalize nodelta #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
1447       lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2 whd in match (typeof ?); #e'
1448       * [ 1: * ]
1449       [ 1: * #sz * #sg * *
1450       | 2: * #optlen * #ty' * #sz * #sg * *
1451       | 3: * #t1 * #t2 * #n1 * #n2 * * ]
1452       whd in match (typeof ?) in ⊢ (% → % → ?);
1453       #Htypeof_e1 #Htypeof_e2
1454       >Htypeof_e1 >Htypeof_e2
1455       #Hclassify
1456       lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify
1457       normalize nodelta
1458       whd in match (typeof ?) in ⊢ (% → % → %);
1459       whd in match (typ_of_type (Tint ??));
1460       #lhs #rhs
1461       [ 1: #Htyp_should_eq cases (typ_should_eq_inversion (ASTint sz sg) (typ_of_type ty) … Htyp_should_eq)
1462            -Htyp_should_eq
1463       | 2: #Htyp_should_eq cases (typ_should_eq_inversion ASTptr (typ_of_type ty) … Htyp_should_eq)
1464            -Htyp_should_eq
1465       | 3: #Haux cases (match_type_inversion_aux … Haux) #ty_sz * #ty_sg * -Haux
1466            #Hty_eq #Heq_aux destruct (Hty_eq) lapply (jmeq_to_eq ??? Heq_aux) -Heq_aux
1467            #Heq_e' destruct (Heq_e') ]
1468       [ 1,2: #Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') -Heq_e' #Heq_e'
1469              <Heq_e' -Heq_e' | ]
1470       #Hexec
1471       #Hexpr_vars_rhs #Hexpr_vars_lhs
1472       #Htranslate_rhs #Htranslate_lhs
1473       * [ #Hyp_present_lhs #Hyp_present_rhs
1474         | #Hyp_present_lhs * #Hyp_present_rhs #Hyp_present_cst
1475         | * #Hyp_present_lhs #Hyp_present_rhs #Hyp_present_cst ]
1476       whd in match (typeof ?);
1477       #Hind_rhs #Hind_lhs
1478       cases (bind_inversion ????? Hexec) -Hexec
1479       * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
1480       cases (bind_inversion ????? Hexec) -Hexec
1481       * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
1482       cases (bind_inversion ????? Hexec) -Hexec
1483       #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1484       lapply (opt_to_res_inversion ???? Hsem) -Hsem
1485       whd in match (typeof ?); whd in match (typeof ?);
1486       #Hsem_binary
1487       whd in match (eval_expr ???????);
1488       whd in match (proj1 ???);
1489       whd in match (eval_expr ???????);
1490       whd in match (eval_expr ???????);
1491       whd in match (proj1 ???);
1492       [ 1: lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
1493       | 2,3: lapply (Hind_lhs … (expr_vars_fix_ptr_type … Hyp_present_lhs) Hexec_lhs) ]
1494       * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
1495       [ 1,2: lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
1496       | 3: lapply (Hind_rhs … (expr_vars_fix_ptr_type … Hyp_present_rhs) Hexec_rhs) ]
1497       * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
1498       [ 3: lapply (eval_expr_rewrite_aux … Heval_lhs) -Heval_lhs #Heval_lhs ]
1499       [ 1,2: >Heval_lhs normalize nodelta
1500              whd in match (eval_expr ???????);
1501              whd in match (eval_expr ???????);
1502              [ >(eval_expr_rewrite_aux … Heval_rhs)
1503              | >Heval_rhs ]
1504              whd in match (m_bind ?????);
1505              normalize nodelta
1506       | 3: >(eval_expr_rewrite_aux … Heval_lhs) normalize nodelta
1507            whd in match (eval_expr ???????);
1508            whd in match (eval_expr ???????);
1509            >Heval_rhs normalize nodelta
1510            whd in match (eval_unop ????);
1511       ]
1512       [ 1: (* ptr/ptr sub *)
1513            whd in Hsem_binary:(??%?);
1514            lapply (sub_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
1515            * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
1516            lapply (sem_sub_pp_inversion … Hsem_binary_translated) *
1517            [ (* regular pointers case *)
1518              * #lhs_ptr * #rhs_ptr * #resulting_offset * * * *
1519              #Hcm_lhs #Hcm_rhs #Hblocks_eq #Hoffset_eq #Hcm_val_eq
1520              whd in match (eval_binop ???????);
1521              >Hcm_lhs >Hcm_rhs normalize nodelta >Hblocks_eq >eq_block_b_b
1522              normalize nodelta
1523              whd in match (eval_expr ???????);
1524              whd in match (m_bind ?????);
1525              whd in match (eval_binop ???????);
1526              (* size mismatch between CL and CM. TODO *)
1527              @cthulhu
1528            | (* null pointers case *)
1529              * * #Hcm_lhs #Hcm_rhs #Hcm_val destruct
1530              whd in match (eval_binop ???????); normalize nodelta
1531              whd in match (eval_expr ???????);
1532              whd in match (m_bind ?????);
1533              whd in match (eval_binop ???????); normalize nodelta
1534              >division_u_zero normalize nodelta
1535              whd in match (eval_unop ????);
1536              whd in match (opt_to_res ???);
1537              whd in match (m_bind ?????);
1538              whd in match (pred_size_intsize ?);
1539              %{(zero_ext ty_sz (Vint I16 (zero (S (7+1*8)))))} @conj
1540              [ whd in match (Eapp ??); whd in match E0; >append_nil try @refl ]
1541              whd in Hsem_binary_translated:(??%?);
1542              normalize nodelta in Hsem_binary_translated:(??%?);
1543              lapply Hsem_binary_translated; -Hsem_binary_translated;
1544              cases n1 cases n2
1545              [ | 2,3: #n | #n1 #n2 ] normalize nodelta
1546              #Heq destruct (Heq)
1547              (* size mismatch between CL and CM. TODO *)
1548              @cthulhu
1549            ]
1550       | 2: (* int/int sub *)
1551            whd in match (eval_binop ???????);
1552            whd in Hsem_binary:(??%?);
1553            lapply (sub_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
1554            * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
1555            cases (sem_sub_ii_inversion … Hsem_binary_translated)
1556            #cm_vsz * #cm_lhs_v * #cm_rhs_v * *
1557            #Hcm_lhs #Hcm_rhs #Hcm_val
1558            destruct (Hcm_lhs) destruct (Hcm_rhs) normalize nodelta
1559            >intsize_eq_elim_true normalize nodelta
1560            %{(Vint cm_vsz (subtraction (bitsize_of_intsize cm_vsz) cm_lhs_v cm_rhs_v))}
1561            @conj try @refl lapply Hsem_binary_translated
1562            whd in ⊢ ((??%?) → ?); normalize nodelta whd in match (classify_sub ??);
1563            >type_eq_dec_true normalize nodelta
1564            >intsize_eq_elim_true #H destruct (H) @Hvalue_eq_res
1565       | 3: (* ptr/int sub *)
1566            whd in Hsem_binary:(??%?);
1567            lapply (sub_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
1568            * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
1569            lapply (sem_sub_pi_inversion … Hsem_binary_translated) -Hsem_binary_translated
1570            * #cm_vsz * #cm_rhs_v * #Hcm_rhs *
1571            [ * #lhs_ptr * #Hcm_lhs_ptr #Hcm_val_shptr
1572            | * * #lhs_null #Hcm_rhs_zero #Hcm_val_null ]
1573            whd in match (eval_unop ????);
1574            -Heval_lhs -Heval_rhs destruct
1575            whd in match (proj2 ???);           
1576            @(match sg
1577              return λs. sg = s → ?
1578              with
1579              [ Unsigned ⇒ λHsg. ?
1580              | Signed ⇒ λHsg. ?
1581              ] (refl ??)) normalize nodelta
1582            whd in match (eval_expr ???????);
1583            whd in match (m_bind ?????);
1584            whd in match (eval_binop ???????);
1585            [ 1,2:
1586                %{(Vptr
1587                  (neg_shift_pointer_n (bitsize_of_intsize cm_vsz) lhs_ptr (sizeof ty') sg
1588                   cm_rhs_v))} try @conj try assumption
1589                   (* TODO size mismatch (?) or insert zero/sign_ext in semantics *)
1590                   (*            [ 1,2,3,4: @conj whd in match (E0);
1591                        whd in match (Eapp trace_rhs ?);
1592                        whd in match (Eapp trace_lhs ?);                     
1593                        >(append_nil … trace_rhs) try @refl
1594                        >(append_nil … trace_lhs) try @refl
1595                        @(value_eq_triangle_diagram … Hvalue_eq_res)
1596                        whd in match (shift_pointer_n ?????);
1597                        whd in match (shift_offset_n ?????);
1598                        >Hsg normalize nodelta
1599                        >commutative_short_multiplication
1600                        whd in match (shift_pointer ???);
1601                        whd in match (shift_offset ???);
1602                        >sign_ext_same_size @refl *)                   
1603                @cthulhu ]
1604            [ >(sign_ext_zero (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16))
1605            | >(zero_ext_zero (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16)) ]
1606            >(short_multiplication_zero 16  (repr I16 (sizeof ty')))
1607            >(eq_bv_true … (zero 16)) normalize nodelta %{Vnull} @conj try assumption
1608           normalize >append_nil try @refl
1609       ]     
[2565]1610     | 3: (* mul *)
1611       lapply (classify_aop_inversion (typeof e1) (typeof e2)) *
1612       [ 2,4: #Hclassify >Hclassify normalize nodelta
1613            #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
1614       lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2
1615       whd in match (typeof ?); #e'
1616       * #sz * #sg * *
1617       whd in match (typeof ?) in ⊢ (% → % → ?);
1618       #Htypeof_e1 #Htypeof_e2
1619       >Htypeof_e1 >Htypeof_e2
1620       whd in match (typeof ?) in ⊢ (% → % → % → ?);
1621       #Hclassify
1622       lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify
1623       normalize nodelta
1624       whd in match (typ_of_type (Tint ??));
1625       #lhs #rhs #Htyp_should_eq
1626       cases (typ_should_eq_inversion (ASTint sz sg) (typ_of_type ty) … Htyp_should_eq)
1627       -Htyp_should_eq
1628       #Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') -Heq_e' #Heq_e'
1629       <Heq_e' -Heq_e'
1630       #Hexec
1631       #Hexpr_vars_rhs #Hexpr_vars_lhs
1632       #Htranslate_rhs #Htranslate_lhs
1633       * #Hyp_present_lhs #Hyp_present_rhs
1634       #Hind_rhs #Hind_lhs
1635       cases (bind_inversion ????? Hexec) -Hexec
1636       * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
1637       cases (bind_inversion ????? Hexec) -Hexec
1638       * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
1639       cases (bind_inversion ????? Hexec) -Hexec
1640       #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1641       lapply (opt_to_res_inversion ???? Hsem) -Hsem
1642       whd in match (typeof ?); whd in match (typeof ?);
1643       #Hsem_binary
1644       lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
1645       * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
1646       lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
1647       * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
1648       whd in match (eval_expr ???????);
1649       whd in match (proj1 ???);
1650       >Heval_lhs normalize nodelta
1651       >Heval_rhs normalize nodelta
1652       whd in match (m_bind ?????);
1653       whd in match (eval_binop ???????);
1654       whd in Hsem_binary:(??%?);
1655       lapply (mul_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
1656       * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
1657       cases (sem_mul_inversion … Hsem_binary)
1658       #cm_vsz * #cm_lhs_v * #cm_rhs_v * *
1659       #Hcm_lhs #Hcm_rhs #Hcm_val
1660       destruct (Hcm_lhs) destruct (Hcm_rhs) normalize nodelta
1661       >(value_eq_int_inversion … Hvalue_eq_lhs) normalize nodelta
1662       >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta
1663       >intsize_eq_elim_true normalize nodelta
1664       %{(Vint cm_vsz (short_multiplication (bitsize_of_intsize cm_vsz) cm_lhs_v cm_rhs_v))}
1665       @conj try @refl
1666       whd in Hsem_binary:(??%?);     
1667       whd in match (classify_aop ??) in Hsem_binary:(??%?);
1668       >type_eq_dec_true in Hsem_binary; normalize nodelta
1669       >intsize_eq_elim_true #Heq destruct (Heq)
1670       %2
[2572]1671     | 4,5: (* div *)
[2565]1672       lapply (classify_aop_inversion (typeof e1) (typeof e2)) *
1673       [ 2,4: #Hclassify >Hclassify normalize nodelta
1674            #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
1675       lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2
1676       whd in match (typeof ?); #e'
1677       * #sz * * * *
1678       whd in match (typeof ?) in ⊢ (% → % → ?);
1679       #Htypeof_e1 #Htypeof_e2
1680       >Htypeof_e1 >Htypeof_e2
1681       whd in match (typeof ?) in ⊢ (% → % → % → ?);
1682       #Hclassify
1683       lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify
1684       normalize nodelta
1685       whd in match (typ_of_type (Tint ??));
1686       #lhs #rhs #Htyp_should_eq
[2572]1687       [ 1,3: cases (typ_should_eq_inversion (ASTint sz Signed) (typ_of_type ty) … Htyp_should_eq)
1688       | 2,4: cases (typ_should_eq_inversion (ASTint sz Unsigned) (typ_of_type ty) … Htyp_should_eq) ]
[2565]1689       -Htyp_should_eq
1690       #Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') -Heq_e' #Heq_e'
1691       <Heq_e' -Heq_e'
1692       #Hexec
1693       #Hexpr_vars_rhs #Hexpr_vars_lhs
1694       #Htranslate_rhs #Htranslate_lhs
1695       * #Hyp_present_lhs #Hyp_present_rhs
1696       #Hind_rhs #Hind_lhs
1697       cases (bind_inversion ????? Hexec) -Hexec
1698       * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
1699       cases (bind_inversion ????? Hexec) -Hexec
1700       * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
1701       cases (bind_inversion ????? Hexec) -Hexec
1702       #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1703       lapply (opt_to_res_inversion ???? Hsem) -Hsem
1704       whd in match (typeof ?); whd in match (typeof ?);
1705       #Hsem_binary
1706       lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
1707       * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
1708       lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
1709       * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
1710       whd in match (eval_expr ???????);
1711       whd in match (proj1 ???);
1712       >Heval_lhs normalize nodelta
1713       >Heval_rhs normalize nodelta
1714       whd in match (m_bind ?????);
1715       whd in match (eval_binop ???????);
1716       whd in Hsem_binary:(??%?);
[2572]1717       [ 1,3: (* div*)
1718          lapply (div_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
1719          * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
1720          [ cases (sem_div_inversion_s … Hsem_binary)
1721          | cases (sem_div_inversion_u … Hsem_binary) ]
1722       | 2,4: (* mod *)
1723          lapply (mod_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
1724          * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
1725          [ cases (sem_mod_inversion_s … Hsem_binary)
1726          | cases (sem_mod_inversion_u … Hsem_binary) ]
1727       ]
[2565]1728       #cm_vsz * #cm_lhs_v * #cm_rhs_v * *
1729       #Hcm_lhs #Hcm_rhs #Hcm_val
1730       destruct (Hcm_lhs) destruct (Hcm_rhs) normalize nodelta
1731       >(value_eq_int_inversion … Hvalue_eq_lhs) normalize nodelta
1732       >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta
1733       >intsize_eq_elim_true normalize nodelta
[2572]1734       [ cases (division_s ???) in Hcm_val;
1735       | cases (division_u ???) in Hcm_val;
1736       | cases (modulus_s ???) in Hcm_val;
1737       | cases (modulus_u ???) in Hcm_val; ]
1738       normalize nodelta
1739       [ 1,3,5,7: @False_ind ]
1740       #i #Hcl_val destruct (Hcl_val) %{(Vint cm_vsz i)} @conj try @refl %2
1741     | 6,7,8: (* and,or,xor *)
1742       lapply (classify_aop_inversion (typeof e1) (typeof e2)) *
1743       [ 2,4,6: #Hclassify >Hclassify normalize nodelta
1744            #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
1745       lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2
1746       whd in match (typeof ?); #e'
1747       * #sz * #sg * *
1748       whd in match (typeof ?) in ⊢ (% → % → ?);
1749       #Htypeof_e1 #Htypeof_e2
1750       >Htypeof_e1 >Htypeof_e2
1751       whd in match (typeof ?) in ⊢ (% → % → % → ?);
1752       #Hclassify
1753       lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify
1754       normalize nodelta
1755       whd in match (typ_of_type (Tint ??));
1756       #lhs #rhs #Htyp_should_eq
1757       cases (typ_should_eq_inversion (ASTint sz sg) (typ_of_type ty) … Htyp_should_eq)
1758       -Htyp_should_eq
1759       #Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') -Heq_e' #Heq_e'
1760       <Heq_e' -Heq_e'
1761       #Hexec
1762       #Hexpr_vars_rhs #Hexpr_vars_lhs
1763       #Htranslate_rhs #Htranslate_lhs
1764       * #Hyp_present_lhs #Hyp_present_rhs
1765       #Hind_rhs #Hind_lhs
1766       cases (bind_inversion ????? Hexec) -Hexec
1767       * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
1768       cases (bind_inversion ????? Hexec) -Hexec
1769       * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
1770       cases (bind_inversion ????? Hexec) -Hexec
1771       #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1772       lapply (opt_to_res_inversion ???? Hsem) -Hsem
1773       whd in match (typeof ?); whd in match (typeof ?);
1774       #Hsem_binary
1775       lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
1776       * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
1777       lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
1778       * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
1779       whd in match (eval_expr ???????);
1780       whd in match (proj1 ???);
1781       >Heval_lhs normalize nodelta
1782       >Heval_rhs normalize nodelta
1783       whd in match (m_bind ?????);
1784       whd in match (eval_binop ???????);
1785       whd in Hsem_binary:(??%?);
1786       [ 1: (* and *)
1787          lapply (and_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
1788           * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
1789          cases (sem_and_inversion … Hsem_binary)
1790       | 2: (* or *)
1791          lapply (or_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
1792           * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
1793          cases (sem_or_inversion … Hsem_binary)
1794       | 3: (* xor *)
1795          lapply (xor_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
1796           * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
1797          cases (sem_xor_inversion … Hsem_binary)
1798       ]
1799       #cm_vsz * #cm_lhs_v * #cm_rhs_v * *
1800       #Hcm_lhs #Hcm_rhs #Hcm_val
1801       destruct (Hcm_lhs) destruct (Hcm_rhs) normalize nodelta
1802       >(value_eq_int_inversion … Hvalue_eq_lhs) normalize nodelta
1803       >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta
1804       >intsize_eq_elim_true normalize nodelta
1805       [ 1: %{(Vint cm_vsz (conjunction_bv … cm_lhs_v cm_rhs_v))}
1806       | 2: %{(Vint cm_vsz (inclusive_disjunction_bv … cm_lhs_v cm_rhs_v))}
1807       | 3: %{(Vint cm_vsz (exclusive_disjunction_bv … cm_lhs_v cm_rhs_v))}
1808       ]
1809       @conj try @refl >Hcm_val %2
1810     | 9,10: (* shl, shr *)
1811       lapply (classify_aop_inversion (typeof e1) (typeof e2)) *
1812       [ 2,4: #Hclassify >Hclassify normalize nodelta
1813            #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
1814       lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2
1815       whd in match (typeof ?); #e'
1816       * #sz * * * *
1817       whd in match (typeof ?) in ⊢ (% → % → ?);
1818       #Htypeof_e1 #Htypeof_e2
1819       >Htypeof_e1 >Htypeof_e2
1820       whd in match (typeof ?) in ⊢ (% → % → % → ?);
1821       #Hclassify
1822       lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify
1823       normalize nodelta
1824       whd in match (typ_of_type (Tint ??));
1825       #lhs #rhs #Htyp_should_eq
1826       [ 1,3: cases (typ_should_eq_inversion (ASTint sz Signed) (typ_of_type ty) … Htyp_should_eq)
1827       | 2,4: cases (typ_should_eq_inversion (ASTint sz Unsigned) (typ_of_type ty) … Htyp_should_eq) ]
1828       -Htyp_should_eq
1829       #Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') -Heq_e' #Heq_e'
1830       <Heq_e' -Heq_e'
1831       #Hexec
1832       #Hexpr_vars_rhs #Hexpr_vars_lhs
1833       #Htranslate_rhs #Htranslate_lhs
1834       * #Hyp_present_lhs #Hyp_present_rhs
1835       #Hind_rhs #Hind_lhs
1836       cases (bind_inversion ????? Hexec) -Hexec
1837       * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
1838       cases (bind_inversion ????? Hexec) -Hexec
1839       * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
1840       cases (bind_inversion ????? Hexec) -Hexec
1841       #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1842       lapply (opt_to_res_inversion ???? Hsem) -Hsem
1843       whd in match (typeof ?); whd in match (typeof ?);
1844       #Hsem_binary
1845       lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
1846       * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
1847       lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
1848       * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
1849       whd in match (eval_expr ???????);
1850       whd in match (proj1 ???);
1851       >Heval_lhs normalize nodelta
1852       >Heval_rhs normalize nodelta
1853       whd in match (m_bind ?????);
1854       whd in match (eval_binop ???????);
1855       whd in Hsem_binary:(??%?);
1856       [ 1,3: (* shl *)
1857          lapply (shl_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
1858          * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
1859          cases (sem_shl_inversion … Hsem_binary)
1860          #sz1 * #sz2 * #lhs_i * #rhs_i * * *
1861          #Hcl_lhs #Hcl_rhs #Hcl_val #Hshift_ok
1862          destruct (Hcl_lhs Hcl_rhs)
1863          >(value_eq_int_inversion … Hvalue_eq_lhs)
1864          >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta
1865          >Hshift_ok normalize nodelta
1866          %{(Vint sz1
1867               (shift_left bool (bitsize_of_intsize sz1)
1868               (nat_of_bitvector (bitsize_of_intsize sz2) rhs_i) lhs_i false))}
1869          @conj try @refl >Hcl_val %2
1870       | *: (* shr, translated to mod /!\ *)     
1871          lapply (shr_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
1872          * #cm_val * #Hsem_binary_translated #Hvalue_eq_res
1873          cases (sem_shr_inversion … Hsem_binary) normalize nodelta
1874          #sz1 * #sz2 * #lhs_i * #rhs_i * * *
1875          #Hcl_lhs #Hcl_rhs #Hshift_ok #Hcl_val
1876          destruct (Hcl_lhs Hcl_rhs)
1877          >(value_eq_int_inversion … Hvalue_eq_lhs)
1878          >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta
1879          >Hshift_ok normalize nodelta >Hcl_val
1880          /3 by ex_intro, conj, vint_eq/ ]
1881     | *: (* comparison operators *)
1882       lapply e' -e'
1883       cases e1 #ed1 #ety1
1884       cases e2 #ed2 #ety2
1885       whd in match (typeof ?) in ⊢ (% → % → % → %);
1886       #cm_expr whd in match (typeof ?);
1887       inversion (classify_cmp ety1 ety2)
1888       [ 3,6,9,12,15,18: #ety1' #ety2' #Hety1 #Hety2
1889            lapply (jmeq_to_eq ??? Hety1) #Hety1'
1890            lapply (jmeq_to_eq ??? Hety1) #Hety2'
1891            destruct #Hclassify >Hclassify normalize nodelta
1892            #cmexpr1 #cmexpr2
1893            whd in ⊢ ((???%) → ?);
1894            #Heq destruct (Heq)
1895       | 1,4,7,10,13,16:
1896            #sz #sg #Hety1 #Hety2 #Hclassify
1897            lapply (jmeq_to_eq ??? Hety1) #Hety1'
1898            lapply (jmeq_to_eq ??? Hety1) #Hety2' destruct
1899            >(jmeq_to_eq ??? Hclassify) -Hclassify normalize nodelta
1900            whd in match (typeof ?) in ⊢ (% → % → % → %);
1901            whd in match (typ_of_type ?) in ⊢ (% → % → ?);
1902            cases sg #cmexpr1 #cmexpr2 normalize nodelta
1903            #Hcast_to_bool #Hexec_expr
1904            cases (complete_cmp_inversion … Hcast_to_bool) -Hcast_to_bool
1905            #tysz * #tysg * #Htyis_int #Hcm_expr_aux
1906            destruct (Htyis_int)
1907            lapply (jmeq_to_eq ??? Hcm_expr_aux) #Hcm_expr -Hcm_expr_aux
1908            destruct (Hcm_expr)
1909            cases (bind_inversion ????? Hexec_expr) -Hexec_expr
1910            * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
1911            cases (bind_inversion ????? Hexec) -Hexec
1912            * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
1913            cases (bind_inversion ????? Hexec) -Hexec
1914            #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1915            lapply (opt_to_res_inversion ???? Hsem) -Hsem
1916            whd in match (typeof ?); whd in match (sem_binary_operation ??????);
1917            #Hsem_cmp lapply (sem_cmp_int_inversion … Hsem_cmp) -Hsem_cmp
1918            * #vsz * #lhs_val * #rhs_val * * #Hcl_lhs #Hcl_rhs normalize nodelta
1919            destruct (Hcl_lhs) destruct (Hcl_rhs)
1920            #Heq_bool whd in match (typ_of_type ?) in ⊢ (% → % → % → %);
1921            #Hexpr_vars_rhs #Hexpr_vars_lhs #Htranslate_rhs #Htranslate_lhs
1922            * #Hyp_present_lhs #Hyp_present_rhs
[2578]1923            #Hind_rhs #Hind_lhs
[2572]1924            lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
1925            * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
1926            lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
1927            * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
1928            whd in match (eval_expr ???????);
1929            whd in match (eval_expr ???????);
1930            >Heval_lhs normalize nodelta
1931            >Heval_rhs normalize nodelta
1932            whd in match (m_bind ?????);
1933            whd in match (eval_binop ???????);
1934            >(value_eq_int_inversion … Hvalue_eq_lhs)
1935            >(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta
1936            >intsize_eq_elim_true normalize nodelta
1937            destruct (Heq_bool)
1938            whd in match (eval_unop ????);
1939            whd in match (opt_to_res ???);
1940            whd in match (m_bind ?????);
1941            (* finished modulo glitch in integer widths *)
1942            @cthulhu
1943       | *:
1944            #n #ty' #Hety1 #Hety2 #Hclassify
1945            lapply (jmeq_to_eq ??? Hety1) #Hety1'
1946            lapply (jmeq_to_eq ??? Hety1) #Hety2' destruct
1947            >(jmeq_to_eq ??? Hclassify) -Hclassify normalize nodelta
1948            whd in match (typeof ?) in ⊢ (% → % → % → %);
1949            #cmexpr1 #cmexpr2
1950            #Hcast_to_bool #Hexec_expr
1951            cases (complete_cmp_inversion … Hcast_to_bool) -Hcast_to_bool
1952            #tysz * #tysg * #Htyis_int #Hcm_expr_aux
1953            destruct (Htyis_int)
1954            lapply (jmeq_to_eq ??? Hcm_expr_aux) #Hcm_expr -Hcm_expr_aux
1955            destruct (Hcm_expr)
1956            cases (bind_inversion ????? Hexec_expr) -Hexec_expr
1957            * #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
1958            cases (bind_inversion ????? Hexec) -Hexec
1959            * #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
1960            cases (bind_inversion ????? Hexec) -Hexec
1961            #val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1962            lapply (opt_to_res_inversion ???? Hsem) -Hsem
1963            whd in match (typeof ?); whd in match (sem_binary_operation ??????);
[2578]1964            #Hsem_cmp (* cut > *)
1965            #Hexpr_vars_rhs #Hexpr_vars_lhs #Htranslate_rhs #Htranslate_lhs
1966            * #Hyp_present_lhs #Hyp_present_rhs
1967            #Hind_rhs #Hind_lhs
1968            lapply (Hind_rhs … (expr_vars_fix_ptr_type … Hyp_present_rhs) Hexec_rhs)
1969            * #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
1970            lapply (Hind_lhs … (expr_vars_fix_ptr_type … Hyp_present_lhs) Hexec_lhs)
1971            * #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
1972            lapply (cmp_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs Hinj … Hsem_cmp)
1973            -Hvalue_eq_lhs -Hvalue_eq_rhs
1974            * #cm_val * #Hsem_cmp_cm #Hvalue_eq_res %{cm_val} @conj try assumption
1975            lapply (sem_cmp_ptr_inversion … Hsem_cmp_cm) -Hsem_cmp_cm -Hsem_cmp
[2572]1976            *
1977            [ 2,4,6,8,10,12:
1978              * * #Hcl_lhs #Hcl_rhs #Hsem_cmp destruct
1979            | *: *
1980              [ 2,4,6,8,10,12:
1981                * #p2 * * #Hcl_lhs #Hcl_rhs #Hsem_cmp destruct
1982              | *: *
1983                [ 2,4,6,8,10,12:
1984                  * #p1 * * #Hcl_lhs #Hcl_rhs #Hsem_cmp destruct
1985                | *: * #p1 * #p2 * * * * #Hcl_lhs #Hcl_rhs #Hvalid_p1 #Hvalid_p2 #Heq_block_outcome destruct
1986            ] ] ]
1987            whd in match (eval_expr ???????);
1988            whd in match (eval_expr ???????);
[2578]1989            whd in Hsem_cmp:(??%?);
1990            destruct (Hsem_cmp)                       
[2572]1991            >(eval_expr_rewrite_aux … Heval_lhs) normalize nodelta
1992            >(eval_expr_rewrite_aux … Heval_rhs) normalize nodelta
1993            whd in match (m_bind ?????);
1994            whd in match (eval_binop ???????);
[2578]1995            [ 1,2,3,4,5,6:
1996              (* qed modulo integer width glitch *)
[2572]1997              @cthulhu
[2578]1998            | *: >Hvalid_p1 >Hvalid_p2 normalize nodelta
1999                 lapply Heq_block_outcome -Heq_block_outcome
2000                 @(eq_block_elim … (pblock p1) (pblock p2))
2001                 normalize nodelta
2002                 [ 1,3,5,7,9,11:
2003                   #Hbocks_eq #Heq_cmp destruct (Heq_cmp)
2004                   whd in match (eval_unop ????);
2005                   whd in match (m_bind ?????);
2006                   cases (cmp_offset ???) normalize nodelta
2007                   (* glitch *)
2008                   @cthulhu
2009                 | *:
2010                   #_ whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
2011                   whd in match (eval_unop ????);
2012                   whd in match (m_bind ?????);
2013                   @cthulhu
2014                 ]
2015           ]
[2572]2016       ]
[2578]2017    ]
2018
[2565]2019| 1: (* Integer constant *)
[2496]2020  #csz #ty cases ty
2021  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
[2545]2022  | #structname #fieldspec | #unionname #fieldspec | #id ]
[2496]2023  #i whd in match (typeof ?); #e' #Hexpr_vars #Htranslate
2024  #val #trace #Hpresent #Hexec_cl
2025  whd in Htranslate:(??%?);
2026  [ 1,3,4,5,6,7,8: destruct ]
[2527]2027  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))))
2028  [ 2: * #H_err #H_neq_sz
2029       lapply (H_err (OK ? «Cst (ASTint csz sg) (Ointconst csz sg i),I») (Error ? (msg TypeMismatch)))
2030       >Htranslate #Habsurd destruct (Habsurd) ]
2031  * #H_ok #Heq_sz lapply (H_ok (OK ? «Cst (ASTint csz sg) (Ointconst csz sg i),I») (Error ? (msg TypeMismatch)))
2032  destruct (Heq_sz)
2033  >Htranslate -Htranslate -H_ok #Heq destruct (Heq)
2034  whd in Hexec_cl:(??%?); >eq_intsize_true in Hexec_cl; normalize nodelta
2035  #Heq destruct (Heq) %{(Vint sz i)} @conj try @refl //
[2496]2036| 2: *
[2527]2037  [ #sz #i | #var_id | * #ed1 #ty1 | #e1 | #op #e1 | #op #e1 #e2 | #cast_ty #e1
[2496]2038  | #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
[2500]2039  try /2 by I/
2040  #ty whd in ⊢ (% → ?); #Hind
[2496]2041  whd in match (Plvalue ???);
2042  whd in match (typeof ?);
2043  #cm_expr #Hexpr_vars #Htranslate_expr #val #trace #Hyp_present #Hexec
2044  whd in Hexec:(??%?);
2045  whd in match (exec_lvalue' ?????) in Hexec:(??%?);
2046  cases (bind_inversion ????? Hexec) -Hexec * * #cl_b #cl_o #cl_t * #Hcl_success #Hcl_load_success
2047  whd in Hcl_success:(???%);
2048  [ 1: (* var case *)
[2510]2049       lapply Hcl_success -Hcl_success -Hind
[2496]2050       (* Peform case analysis on presence of variable in local Clight env.
2051        * if success, exec_expr/exec_lvalue tells us that it shoud be local. *)
2052       @(match lookup SymbolTag block cl_env var_id
2053         return λx.(lookup SymbolTag block cl_env var_id = x) → ?
2054         with
2055         [ None ⇒ λHcl_lookup. ?
2056         | Some loc ⇒ λHcl_lookup. ?
2057         ] (refl ? (lookup SymbolTag block cl_env var_id)))
2058       normalize nodelta
2059       [ 1: (* global case *)
[2510]2060            #Hlookup_global
2061            cases (bind_inversion ????? Hlookup_global) -Hlookup_global #global_block
2062            * #Hopt lapply (opt_to_res_inversion ???? Hopt) #Hfind_symbol
2063            #Heq whd in Heq:(???%); destruct (Heq)
2064            lapply (bind2_eq_inversion ?????? Htranslate_expr) -Htranslate_expr
2065            * #var_id_alloctype * #var_id_type * #Heq
2066            cases (variable_not_in_env_but_in_vartypes_is_global …
[2545]2067                        Hexec_alloc Hcharacterise Hcl_lookup ?? Heq)
[2510]2068            #r #Heq' destruct (Heq') normalize nodelta
2069            lapply Hcl_load_success -Hcl_load_success
2070            lapply Hyp_present -Hyp_present
2071            lapply Hexpr_vars -Hexpr_vars
2072            lapply cm_expr -cm_expr inversion (access_mode ty)
2073            [ #typ_of_ty | | #typ_of_ty ]
2074            #Heq_typ_of_type #Heq_access_mode
2075            #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_success normalize nodelta
2076            whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2077            whd in match (eval_expr ???????);
2078            whd in match (eval_expr ???????);
2079            whd in match (eval_constant ????);
2080            <(eq_sym … inv) >Hfind_symbol normalize nodelta
2081            cases (bind_inversion ????? Hcl_load_success) #x *
2082            #Hopt_to_res whd in ⊢ (???% → ?); #Heq_val destruct (Heq_val)
2083            lapply (opt_to_res_inversion ???? Hopt_to_res)
2084            #Hcl_load_success
2085            [ 2: %{(Vptr (mk_pointer cl_b (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 O))))}
2086                 @conj try @refl
2087                 whd in Hcm_load_success:(??%?);
2088                 lapply (jmeq_to_eq ??? Heq_typ_of_type) #Heq_ty
2089                 >(load_value_of_type_by_ref … Hcl_load_success)
2090                 try assumption %4
2091                 lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
2092                 >Hfind_symbol normalize nodelta #Heq_embedding
2093                 whd in match (shift_offset ???);
2094                 >addition_n_0 whd in match (pointer_translation ??); >Heq_embedding
2095                 normalize nodelta @refl
2096            | 1: cut (access_mode ty=By_value (typ_of_type ty))
2097                 [ @jmeq_to_eq lapply (jmeq_to_eq ??? Heq_typ_of_type) #Heqt
2098                   lapply Heq_access_mode <Heqt // ] #Haccess
2099                 lapply (load_by_value_success_valid_pointer … Haccess … Hcl_load_success)
2100                 #Hvalid_ptr
2101                 lapply (mi_inj … Hinj ?? cl_b zero_offset … Hvalid_ptr … Hcl_load_success)
2102                 [ whd in ⊢ (??%?);
2103                   lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
2104                   >Hfind_symbol normalize nodelta #Heq_embedding >Heq_embedding @refl ]
2105                 * #val' * #Hcm_load_success #Hvalue_eq
2106                 lapply (load_value_of_type_by_value … Haccess … Hcm_load_success)
2107                 #Hloadv lapply (jmeq_to_eq ??? Heq_typ_of_type) #Htypeq <Htypeq >Hloadv
2108                 normalize %{val'} @conj try @refl assumption ]
[2496]2109       | 2: (* local case *)
2110            #Heq destruct (Heq)
[2500]2111            lapply (bind2_eq_inversion ?????? Htranslate_expr) -Htranslate_expr
2112            * #var_id_alloc_type * #var_id_type *
2113            generalize in match var_id_alloc_type; * normalize nodelta
[2510]2114            [ 1: #r #Hlookup_vartype
2115                 lapply (characterise_vars_lookup_local … Hcharacterise … Hcl_lookup … Hexec_alloc)
2116                 * #typ whd in match (local_id ???);
2117                 >Hlookup_vartype normalize nodelta @False_ind
[2496]2118            | 2: (* Stack local *)
[2500]2119                 lapply Hcl_load_success -Hcl_load_success
2120                 lapply Hyp_present -Hyp_present
2121                 lapply Hexpr_vars -Hexpr_vars
2122                 lapply cm_expr -cm_expr inversion (access_mode ty)
2123                 [ #typ_of_ty | | #typ_of_ty ]
2124                 #Heq_typ_of_type #Heq_access_mode
2125                 #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_success
2126                 #stack_depth #Hlookup_vartype_success normalize nodelta
2127                 whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
[2510]2128                 lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
[2500]2129                 cases (res_inversion ?????? Hlookup_vartype_success) -Hlookup_vartype_success
2130                 * #var_id_alloc_type' #var_id_type' * #Hlookup' #Heq destruct (Heq)
[2496]2131                 >Hlookup' normalize nodelta #Hembedding_eq
[2500]2132                 cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success
2133                 #loaded_val * #Hload_val
2134                 whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2135                 lapply (opt_to_res_inversion ???? Hload_val) -Hload_val
[2510]2136                 #Hload_success whd in match (eval_expr ???????);
[2500]2137                 cut (pointer_translation (mk_pointer cl_b zero_offset) E =
[2510]2138                      Some ? (mk_pointer sp (mk_offset (repr I16 stack_depth))))
[2500]2139                 [ 1,3: whd in ⊢ (??%?); >Hembedding_eq normalize nodelta
2140                        >offset_plus_0 @refl ]
[2510]2141                 #Hpointer_translation
[2500]2142                 [ 2: (* By-ref *)
2143                      whd in Hload_success:(??%?);
2144                      lapply (load_value_of_type_by_ref … Hload_success … Heq_typ_of_type Heq_access_mode)
2145                      #Heq_val
2146                      >Heq_val
2147                      %{(Vptr (mk_pointer sp (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 stack_depth))))}
2148                      @conj try @refl
[2510]2149                      %4 whd in match (shift_offset ???);
2150                      whd in match zero_offset;
2151                      >commutative_addition_n >addition_n_0 @Hpointer_translation
[2500]2152                 | 1: (* By value *)
[2510]2153                      lapply (jmeq_to_eq ??? Heq_typ_of_type) #Heq0                       
[2500]2154                      lapply (mi_inj … Hinj … Hpointer_translation … Hload_success)
2155                      [ @(load_by_value_success_valid_pointer … Hload_success)
[2510]2156                        lapply Heq_access_mode <Heq0 /2 by jmeq_to_eq/ ]
[2500]2157                      * #cm_val * #Hload_in_cm #Hvalue_eq
2158                      %{cm_val} @conj try assumption
[2510]2159                      lapply (load_value_of_type_by_value … Hload_in_cm)
2160                      [ lapply Heq_access_mode <Heq0 #Heq1
2161                        @(jmeq_to_eq ??? Heq1) ]
2162                      #Hloadv <Heq0
2163                      whd in match (shift_offset ???); >commutative_addition_n >addition_n_0
2164                      >Hloadv @refl ]
[2500]2165            | 3: (* Register local variable *)
2166                 #Hlookup_eq
2167                 lapply (res_inversion ?????? Hlookup_eq)
2168                 * * #var_id_alloc_type' #var_id_type' * #Hlookup' #Heq destruct (Heq)
2169                 #Htype_eq
2170                 cases (type_should_eq_inversion
2171                            var_id_type
2172                            ty
2173                            (λt0:type.Σe':expr (typ_of_type t0).expr_vars (typ_of_type t0) e' (local_id vars))
2174                            … Htype_eq) -Htype_eq
2175                 (* Reverting all premises in order to perform type rewrite *)
2176                 #Htype_eq
2177                 lapply Hlookup' -Hlookup' lapply Hlookup_eq -Hlookup_eq
2178                 lapply Hcl_load_success -Hcl_load_success
2179                 lapply Hcl_lookup -Hcl_lookup
2180                 lapply Hyp_present -Hyp_present
2181                 lapply Hexpr_vars -Hexpr_vars
2182                 lapply cm_expr
2183                 destruct (Htype_eq)
2184                 #cm_expr #Hexpr_vars #Hyp_present #Hcl_lookup #Hcl_load_success #Hlookup_eq #Hlookup'
2185                 #Hexpr_eq lapply (jmeq_to_eq ??? Hexpr_eq) -Hexpr_eq #Hexpr_eq
2186                 destruct (Hexpr_eq)
2187                 whd in match (eval_expr ???????);
2188                 whd in match (lookup_present ?????);
[2510]2189                 lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
2190                 >Hlookup' normalize nodelta #Hmatching
[2500]2191                 cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success
[2510]2192                 #loaded_val * #Hload_val
[2500]2193                 whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2194                 lapply (opt_to_res_inversion ???? Hload_val) -Hload_val
[2510]2195                 #Hload_success
2196                 cases (Hmatching … Hload_success) #val'
[2500]2197                 * #Hlookup_in_cm #Hvalue_eq %{val'}
2198                 cases Hyp_present
2199                 >Hlookup_in_cm normalize nodelta #_ @conj try @refl try assumption
2200                 (* seems ok *)
[2496]2201            ]
[2545]2202       ]
2203  | 2: lapply Hcl_success -Hcl_success
2204       lapply Htranslate_expr -Htranslate_expr
2205       lapply Hind -Hind cases ty1
2206       [ | #sz1 #sg1 | #ptr_ty1 | #array_ty1 #array_sz1 | #domain1 #codomain1
2207       | #structname1 #fieldspec1 | #unionname1 #fieldspec1 | #id1 ]
2208       #Hind #Htranslate_expr #Hexec_cl
2209       cases (bind_inversion ????? Htranslate_expr) -Htranslate_expr
2210       * whd in match (typ_of_type ?); normalize nodelta
2211       #cm_expr_ind #Hexpr_vars_ind * #Htranslate_expr_ind
[2527]2212       whd in ⊢ ((???%) → ?);
[2545]2213       [ 1,2,6,7: #Heq destruct (Heq) ]
2214       lapply (Hind cm_expr_ind Hexpr_vars_ind) -Hind
2215       whd in match (translate_addr ??); >Htranslate_expr_ind normalize nodelta
2216       #Hind lapply (Hind (refl ??) cl_b cl_o cl_t ?) -Hind
2217       [ 1,3,5,7: @cthulhu ]
2218       whd in match (exec_lvalue' ?????); >Hexec_cl normalize nodelta
2219       cases (bind_inversion ????? Hexec_cl) * #cl_ptr #cl_trace0 *
2220       #Hexec_cl_ind #Hcl_ptr
2221       cut (∃ptr. cl_ptr = Vptr ptr)
2222       [ 1,3,5,7: cases cl_ptr in Hcl_ptr; normalize
2223                  #H1 destruct #H2 destruct try /2 by ex_intro, refl/ #H3 destruct ]
2224       * * #cl_ptr_block #cl_ptr_off -Hcl_ptr
2225       #Hcl_ptr destruct (Hcl_ptr) normalize nodelta -Hexec_cl
[2527]2226       #Hind lapply (Hind (refl ??)) -Hind
[2545]2227       * #cm_ptr * #Hexec_cm_ind #Hvalue_eq_ind
2228       lapply (value_eq_ptr_inversion … Hvalue_eq_ind) * * #cm_ptr_block #cm_ptr_off * #Hcm_ptr
2229       destruct (Hcm_ptr) #Hpointer_translation
2230       cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success #cl_val * #Hopt_to_res
2231       whd in ⊢ ((???%) → ?); #Heq destruct (Heq) lapply (opt_to_res_inversion ???? Hopt_to_res)
2232       -Hopt_to_res
[2527]2233       lapply Hyp_present -Hyp_present
2234       lapply Hexpr_vars -Hexpr_vars
2235       lapply cm_expr -cm_expr
[2545]2236       inversion (access_mode ty)
2237       [ 1,3,4,6,7,9,10,12: #t ] #Htyp_of_type #Haccess_mode
2238       lapply (jmeq_to_eq ??? Htyp_of_type) #Htyp destruct (Htyp)
2239       #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_success normalize nodelta
2240       #Heq destruct (Heq)
2241       [ 1,2,3,4: (* By_value *)
2242           (* project Hcl_load_success in Cminor through memory_inj *)
2243           lapply (mi_inj ??? Hinj cl_b cl_o cm_ptr_block cm_ptr_off … Hpointer_translation … Hcl_load_success)
2244           [ 1,3,5,7: @(load_by_value_success_valid_pointer … Hcl_load_success) @jmeq_to_eq assumption ]
2245           * #cm_val * #Hcm_load_success #Hvalue_eq
2246           lapply (load_value_of_type_by_value … (jmeq_to_eq ??? Haccess_mode) … Hcm_load_success)
2247           #Hloadv_cm
2248           whd in match (eval_expr ???????); >Hexec_cm_ind normalize nodelta
2249           >Hloadv_cm normalize %{cm_val} @conj try @refl assumption
2250      | *: (* By reference *)
2251           >Hexec_cm_ind %{(Vptr (mk_pointer cm_ptr_block cm_ptr_off))} @conj try @refl
2252           lapply (load_value_of_type_by_ref … Hcl_load_success Htyp_of_type Haccess_mode)
2253           #Hval >Hval %4 assumption ]
[2527]2254  | 3: lapply Hcl_load_success -Hcl_load_success lapply Hcl_success -Hcl_success
2255       lapply (refl ? (typeof e1))
2256       cases (typeof e1) in ⊢ ((???%) → %);
[2545]2257       [ | #sz1 #sg1 | #ptr_ty1 | #array_ty1 #array_sz1 | #domain1 #codomain1
2258       | #structname1 #fieldspec1 | #unionname1 #fieldspec1 | #id1 ] normalize nodelta
[2527]2259       #Heq_typeof normalize nodelta
[2545]2260       [ 1,2,3,4,5,8: #Habsurd destruct ] #Hexec_cl #Hcl_load_success
2261       whd in Htranslate_expr:(??%?); >Heq_typeof in Htranslate_expr;
2262       normalize nodelta #Htranslate_expr
2263       cases (bind_inversion ????? Htranslate_expr) -Htranslate_expr
2264       * whd in match (typ_of_type ?); normalize nodelta
2265       #cm_expr_ind #Hexpr_vars_ind * #Htranslate_expr_ind #Htranslate_expr2
2266       [ cases (bind_inversion ????? Htranslate_expr2) -Htranslate_expr2
2267         #cm_field_off * #Hcm_field_off
2268       | lapply Htranslate_expr2 -Htranslate_expr2 ]
2269       cases (bind_inversion ????? Hexec_cl) -Hexec_cl
2270       * * #block_cl #offset_cl #trace0 * #Hexec_lvalue #Hexec_cl
2271       whd in Hexec_lvalue:(???%);
2272       [ cases (bind_inversion ????? Hexec_cl) -Hexec_cl
2273         #cl_field_off * #Hcl_field_off #Hoffset_eq ]
2274       cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success
2275       #cl_val * #Hopt_cl_val whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2276       lapply (opt_to_res_inversion ???? Hopt_cl_val) -Hopt_cl_val #Hcl_load_value
2277       [  (* Struct case *)
2278         lapply Hcl_load_value -Hcl_load_value
2279         lapply Hyp_present -Hyp_present
2280         lapply Hexpr_vars -Hexpr_vars
2281         lapply cm_expr -cm_expr
2282         lapply Hind -Hind
2283         cases ty
2284         [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
2285         | #structname #fieldspec | #unionname #fieldspec | #id ]
2286         #Hind #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_value
2287         normalize nodelta
2288         whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2289         whd in match (eval_expr ???????);
2290         (* applying the arguments of the induction hypothesis progressively *)
[2582]2291         lapply (Hind (Op2 ASTptr (ASTint I16 Signed) ASTptr (Oaddpi I16) cm_expr_ind
[2545]2292                          (Cst (ASTint I16 Signed) (Ointconst I16 Signed (repr I16 cm_field_off)))) ?)
2293         [ 1,3,5,7,9: whd @conj try assumption whd @I ] -Hind #Hind
2294         lapply (Hind ?)
2295         [ 1,3,5,7,9:
2296            whd in ⊢ (??%?); >Heq_typeof normalize nodelta
2297            >Htranslate_expr_ind whd in match (m_bind ?????);
2298            >Hcm_field_off normalize nodelta @refl ] -Hind #Hind
2299         whd in Hoffset_eq:(???%); destruct (offset_eq)
2300         cut (cl_field_off = cm_field_off)
2301         [ 1,3,5,7,9: lapply Hcl_field_off >Hcm_field_off
2302           normalize #Heq destruct (Heq) @refl ]
2303         #Heq destruct (Heq)
2304         lapply (Hind cl_b cl_o trace ?)
2305         [ 1,3,5,7,9: @Hyp_present ] -Hind #Hind
2306         lapply (Hind ?) -Hind
2307         [ 1,3,5,7,9: whd in ⊢ (??%?); >Heq_typeof normalize nodelta
2308           >Hexec_lvalue whd in match (m_bind ?????); >Hcm_field_off normalize nodelta
2309           @Hoffset_eq ]
2310         * #cm_val' * #Heval_expr #Hvalue_eq
2311         lapply (value_eq_ptr_inversion … Hvalue_eq) * * #cm_ptr_block #cm_ptr_off
2312         * #Heq_cm_val_ptr destruct (Heq_cm_val_ptr) #Hpointer_trans
2313         [ 1,2,5: (* by-value *)
2314            lapply (mi_inj … Hinj cl_b cl_o ?? … Hpointer_trans … Hcl_load_value)
2315            [ 1,3,5: @(load_by_value_success_valid_pointer … Hcl_load_value) // ]
2316            * #cm_val * #Hcm_load_value #Hvalue_eq
2317            lapply (load_value_of_type_by_value … Hcm_load_value)
2318            [ 1,3,5: @refl ]
2319            #Hcm_loadv %{cm_val} >Heval_expr normalize nodelta >Hcm_loadv normalize @conj
2320            try @refl try assumption
2321         | 3,4: (* by-ref *)
2322            whd in match (eval_expr ???????) in Heval_expr; >Heval_expr
2323            %{(Vptr (mk_pointer cm_ptr_block cm_ptr_off))} @conj try @refl
2324            whd in Hcl_load_value:(??%?); destruct (Hcl_load_value) assumption
2325         ]
2326      | (* union case *)
2327         lapply Hcl_load_value -Hcl_load_value
2328         lapply Hyp_present -Hyp_present
2329         lapply Hexpr_vars -Hexpr_vars
2330         lapply cm_expr -cm_expr
2331         lapply Hind -Hind
2332         cases ty
2333         [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
2334         | #structname #fieldspec | #unionname #fieldspec | #id ]
2335         whd in match (typ_of_type ?); normalize nodelta
2336         #Hind #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_value
2337         whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2338         [ 1,2,5: (* by-value *)
2339            whd in match (eval_expr ???????);
2340            lapply (Hind cm_expr_ind Hexpr_vars ?)
2341            [ 1,3,5: whd in ⊢ (??%?); >Heq_typeof normalize nodelta @Htranslate_expr_ind ]
2342            whd in match (exec_lvalue' ?????); >Heq_typeof normalize nodelta
2343            -Hind #Hind
2344            lapply (Hind block_cl offset_cl trace0 Hyp_present) -Hind >Hexec_lvalue normalize nodelta
2345            whd in match (m_bind ?????); #Hind
2346            cases (Hind (refl ??)) -Hind
2347            #cm_val * #Heval_expr #Hvalue_eq >Heval_expr normalize nodelta
2348            cases (value_eq_ptr_inversion … Hvalue_eq) * #cm_block #cm_offset * #Hcm_val #Hpointer_trans
2349            destruct (Hcm_val) whd in Hexec_cl:(???%); destruct (Hexec_cl)
2350            lapply (mi_inj … Hinj cl_b cl_o cm_block cm_offset … Hpointer_trans … Hcl_load_value)
2351            [ 1,3,5: @(load_by_value_success_valid_pointer … Hcl_load_value) // ]
2352            * #cm_val * #Hcm_load_value #Hvalue_eq           
2353            lapply (load_value_of_type_by_value … Hcm_load_value)
2354            [ 1,3,5: @refl ]
2355            #Hcm_loadv %{cm_val} >Hcm_loadv normalize @conj
2356            try @refl assumption
2357         | 3,4:
2358            whd in Hexec_cl:(???%); destruct (Hexec_cl)
2359            lapply (Hind cm_expr Hexpr_vars)
2360            whd in match (translate_addr ??); >Heq_typeof normalize nodelta -Hind #Hind
2361            lapply (Hind Htranslate_expr_ind) -Hind
2362            whd in match (exec_lvalue' ?????); >Heq_typeof normalize nodelta
2363            >Hexec_lvalue whd in match (m_bind ?????);
2364            #Hind cases (Hind … Hyp_present (refl ??))
2365            #cm_val * #Heval_expr #Hvalue_eq >Heval_expr %{cm_val} @conj
2366            try @refl whd in Hcl_load_value:(??%?); destruct (Hcl_load_value)
2367            assumption ]
2368    ]
2369  ]
[2527]2370| 3: #var #ty #cmexpr #Hexpr_vars #Htranslate_var #cl_blo #cl_off #trace #Hyp_present #Hexec_lvalue_var
2371     whd in Hexec_lvalue_var:(??%?);
2372     (* check whether var is local or global *)
[2545]2373     lapply (Hlocal_matching var)
2374     lapply (variable_not_in_env_but_in_vartypes_is_global  … var Hexec_alloc … Hcharacterise)
2375     cases (lookup ?? cl_env var) in Hexec_lvalue_var;
[2527]2376     normalize nodelta
2377     [ 1: (* global *)
[2545]2378          #Hexec_opt #H lapply (H (refl ??)) -H #Hvar_is_global
[2527]2379          cases (bind_inversion ????? Hexec_opt) -Hexec_opt #varblock * #Hopt_to_res #Heq
2380          whd in Heq:(???%) Hopt_to_res:(???%); destruct (Heq)
[2545]2381          lapply (opt_to_res_inversion ???? Hopt_to_res) -Hopt_to_res #Hfind_symbol >Hfind_symbol normalize nodelta
2382          #Hembed
2383          cases (bind_inversion ????? Htranslate_var) -Htranslate_var
2384          * #var_alloctype #var_type * #Hlookup_vartype #Hvar_alloctype
2385          cases (Hvar_is_global … Hlookup_vartype) #r #Halloctype >Halloctype in Hvar_alloctype;
2386          normalize nodelta whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2387          whd in match (eval_expr ???????);
2388          whd in match (eval_constant ????);
2389          <(eq_sym inv var) >Hfind_symbol normalize nodelta
2390          %{(Vptr (mk_pointer cl_blo (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 O))))}
2391          @conj try @refl %4 whd in match (pointer_translation ??);
2392          >Hembed normalize nodelta whd in match (shift_offset ???);
2393          >addition_n_0 @refl
[2527]2394     | 2: (* local *)
[2545]2395          #BL #Heq destruct (Heq) #_
2396          @(match (lookup ?? vars var)
2397            return λx. (lookup ?? vars var = x) → ?
2398            with
2399            [ None ⇒ ?
2400            | Some kind ⇒ ?
2401            ] (refl ??))
2402          normalize nodelta
2403          #Hlookup [ @False_ind ]
2404          cases kind in Hlookup; #var_alloctype #var_type normalize nodelta
2405          #Hlookup
2406          lapply (refl ? var_alloctype)
2407          cases var_alloctype in ⊢ ((???%) → %); normalize nodelta
2408          [ #reg #Heq @False_ind | #stacksize #Hvar_alloc #Hembed | #Hvar_alloc #Hlookup' ]
2409          [ (* stack alloc*)
2410            cases (bind_inversion ????? Htranslate_var) -Htranslate_var
2411            * #var_alloctype' #var_type' * #Hlookup_vartype'           
2412            whd in Hlookup_vartype':(??%?); >Hlookup in Hlookup_vartype'; normalize nodelta
2413            whd in ⊢ ((???%) → ?); #Heq destruct (Heq) >Hvar_alloc normalize nodelta
2414            whd in ⊢ ((???%) → ?); #Heq destruct (Heq) whd in match (eval_expr ???????);
2415            %{(Vptr (mk_pointer sp (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 stacksize))))}
2416            @conj try @refl %4 whd in match (pointer_translation ??);
2417            >Hembed @refl
2418          | (* local alloc *)
2419            cases (bind_inversion ????? Htranslate_var) -Htranslate_var
2420            * #var_alloctype' #var_type' * #Hlookup_vartype'
2421            whd in Hlookup_vartype':(??%?); >Hlookup in Hlookup_vartype'; normalize nodelta
2422            whd in ⊢ ((???%) → ?); #Heq destruct (Heq) >Hvar_alloc normalize nodelta
2423            whd in ⊢ ((???%) → ?); #Heq destruct (Heq) ] ]
2424(*| 4: #e #ty*)
2425| 4:
2426  * #ed #ety cases ety
2427  [ | #sz1 #sg1 | #ptr_ty1 | #array_ty1 #array_sz1 | #domain1 #codomain1
2428  | #structname1 #fieldspec1 | #unionname1 #fieldspec1 | #id1 ] normalize nodelta 
2429  whd in match (typeof ?);
2430  #ty #Hind #e' #Hexpr_vars #Htranslate #cl_blo #cl_off #trace #Hyp_present #Hexec_lvalue
2431  cases (bind_inversion ????? Htranslate) -Htranslate   
2432  * #cm_expr #Hexpr_vars_cm * #Htranslate_ind
2433  cases (bind_inversion ????? Hexec_lvalue) -Hexec_lvalue
2434  * #cl_val #trace0 * #Hexec_expr #Hcl_val
2435  whd in match (typeof ?); whd in match (typ_of_type ?); normalize nodelta
2436  whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2437  cut (cl_val = Vptr (mk_pointer cl_blo cl_off) ∧ trace = trace0)
2438  [ 1,3,5,7: cases cl_val in Hcl_val; normalize
2439    [ 1,5,9,13: #Heq destruct (Heq)
2440    | 2,6,10,14: #sz #vec #Heq destruct (Heq)
2441    | 3,7,11,15: #Heq destruct (Heq)
2442    | 4,8,12,16: * #BL #OFF #Heq destruct (Heq) @conj try @refl ] ]
2443  * #Heq_cl_val destruct (Heq_cl_val) #Htrace_eq destruct (Htrace_eq)
2444  cases (Hind e' Hexpr_vars Htranslate_ind … Hyp_present … Hexec_expr)
2445  #cm_val * #Heval_expr_cm #Hvalue_eq >Heval_expr_cm
2446  %{cm_val} @conj try @refl try assumption
2447| 5:
2448  #ty cases ty
2449  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
2450  | #structname #fieldspec | #unionname #fieldspec | #id ]
2451  #ed #ty' #Hind
2452  whd in match (typeof ?); whd in match (typ_of_type ?); #cm_expr
2453  #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec_expr
2454  cases (bind_inversion ????? Htranslate) -Htranslate
2455  * #cm_expr #Hexpr_vars_cm * #Htranslate_ind
2456  cases (bind_inversion ????? Hexec_expr) -Hexec_expr
2457  * * #cl_blo #cl_off #trace0 * #Hexec_lvalue normalize nodelta
2458  whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2459  whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2460  cases (Hind cm_expr Hexpr_vars Htranslate_ind ??? Hyp_present Hexec_lvalue)
2461  #cm_val * #Hexec_cm #Hvalue_eq >Hexec_cm
2462  %{cm_val} @conj try @refl assumption
2463| 6:
[2554]2464  #ty *
2465  [ cases ty
2466    [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
2467    | #structname #fieldspec | #unionname #fieldspec | #id ]
2468    #e #Hind
2469    whd in match (typeof ?);
2470    #e' whd in match (typ_of_type ?); #Hexpr_vars whd in ⊢ ((??%?) → ?);
2471    #Htranslate
2472    [ 3,4,5,8: destruct (Htranslate)
2473    | 2: lapply Htranslate -Htranslate lapply Hexpr_vars -Hexpr_vars lapply e' -e'
2474         cases sz normalize nodelta
2475         #e' #Hexpr_vars #Htranslate
2476         [ 1, 2: destruct (Htranslate) ] ]
2477    #cl_val #trace #Hyp_present #Hexec_expr
2478    cases (bind_inversion ????? Htranslate) -Htranslate
2479    #cmop * #Htranslate_unop #Hexec_arg
2480    cases (bind_inversion ????? Hexec_arg) -Hexec_arg
2481    * #cm_arg #Hexpr_vars_arg * #Htranslate whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2482    cases (bind_inversion ????? Hexec_expr) -Hexec_expr
2483    * #cl_arg #cl_trace * #Hexec_cl
2484    whd in ⊢ ((???%) → ?); #Hexec_unop
2485    cases (bind_inversion ????? Hexec_unop) -Hexec_unop
2486    #v * #Hopt whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2487    lapply (opt_to_res_inversion ???? Hopt) -Hopt
2488    #Hsem_cl whd in match (eval_expr ???????);
2489    cases (Hind cm_arg Hexpr_vars Htranslate … Hyp_present Hexec_cl)
2490    #cm_val * #Heval_cm #Hvalue_eq >Heval_cm normalize nodelta
2491    lapply (unary_operation_value_eq … Hvalue_eq … Hsem_cl)
2492    * #cl_val' * #Hcl_unop #Hvalue_eq %{cl_val'} @conj try assumption
2493    whd in match (typ_of_type Tvoid);
2494    lapply (translate_notbool_to_cminor … Htranslate_unop … Hcl_unop)
2495    #H >H @refl
2496  | *:
2497    cases ty
2498    [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id
2499    | | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id ]
2500    #e #Hind whd in match (typeof ?);  whd in match (typ_of_type ?); 
2501    #e' #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec
2502    whd in Htranslate:(??%?);
2503    [ 3,4,5,8,11,12,13,16: destruct (Htranslate) ]
2504    cases (bind_inversion ????? Htranslate) -Htranslate
2505    #cmop * #Htranslate_unop #Hexec_arg
2506    cases (bind_inversion ????? Hexec_arg) -Hexec_arg
2507    * #cm_arg #Hexpr_vars_arg * #Htranslate whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2508    cases (bind_inversion ????? Hexec) -Hexec
2509    * #cl_arg #cl_trace * #Hexec_cl
2510    whd in ⊢ ((???%) → ?); #Hexec_unop
2511    cases (bind_inversion ????? Hexec_unop) -Hexec_unop
2512    #v * #Hopt whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2513    lapply (opt_to_res_inversion ???? Hopt) -Hopt
2514    #Hcl_unop whd in match (eval_expr ???????);
2515    cases (Hind cm_arg Hexpr_vars Htranslate … Hyp_present Hexec_cl)
2516    #op_arg * #Heval_cm #Hvalue_eq >Heval_cm normalize nodelta
2517    lapply (unary_operation_value_eq … Hvalue_eq … Hcl_unop)
2518    * #op_res * #Hcl_sem #Hvalue_eq
2519    [ 1,2,3,4: >(translate_notint_to_cminor … Htranslate_unop … Hcl_sem)
2520       %{op_res} @conj try @refl assumption
2521    | 5,6,7,8: >(translate_negint_to_cminor … Htranslate_unop … Hcl_sem)
2522       %{op_res} @conj try @refl assumption
2523    ]
2524  ]
2525| 8: #ty #ty' * #ed #ety
2526  cases ety
2527  [ | #esz #esg | #eptr_ty | #earray_ty #earray_sz | #edomain #ecodomain
2528  | #estructname #efieldspec | #eunionname #efieldspec | #eid ]
2529  whd in match (typeof ?); whd in match (typ_of_type ?);
2530  #Hind whd in match (typeof ?);
2531  #cm_expr #Hexpr_vars #Htranslate
2532  cases (bind_inversion ????? Htranslate) -Htranslate
2533  * #cm_castee #Hexpr_vars_castee * #Htranslate_expr #Htranslate
2534  cases (bind_inversion ????? Htranslate) -Htranslate
2535  * #cm_cast #Hexpr_vars_cast * #Htranslate_cast #Htranslate 
2536  [ 1,5,6,7,8: whd in Htranslate_cast:(??%%); destruct (Htranslate_cast) ]
2537  cases (bind_inversion ????? Htranslate) -Htranslate
2538  * #cm_cast' #Hexpr_vars' * #Htyp_should_eq whd in ⊢ ((??%%) → ?);
2539  #Heq destruct (Heq)
2540  #cl_val #trace #Hyp_present #Hexec_cm
2541  cases (bind_inversion ????? Hexec_cm) -Hexec_cm
2542  * #cm_val #trace0 * #Hexec_cm #Hexec_cast
2543  cases (bind_inversion ????? Hexec_cast) -Hexec_cast
2544  #cast_val * #Hexec_cast
2545  whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
[2565]2546  cases (typ_should_eq_inversion (typ_of_type ty') (typ_of_type ty) … Htyp_should_eq) -Htyp_should_eq
2547  #Htype_eq
[2554]2548  lapply Hexec_cast -Hexec_cast
[2565]2549(*  lapply Htyp_should_eq -Htyp_should_eq *)
[2554]2550  lapply Htranslate_cast -Htranslate_cast
2551  lapply Hexpr_vars_cast -Hexpr_vars_cast
2552  lapply cm_cast -cm_cast
2553  lapply Hyp_present -Hyp_present
2554  lapply Hexpr_vars -Hexpr_vars
2555  lapply cm_expr -cm_expr
2556  <Htype_eq -Htype_eq
[2565]2557  whd in ⊢ (? → ? → ? → ? → ? → ? → (??%%) → ?);
2558  whd in match (typeof ?); normalize nodelta
[2554]2559  cases ty'
2560  [ | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain' | #structname' #fieldspec' | #unionname' #fieldspec' | #id'
2561  | | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain' | #structname' #fieldspec' | #unionname' #fieldspec' | #id'
2562  | | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain' | #structname' #fieldspec' | #unionname' #fieldspec' | #id' ]
[2565]2563  #cm_expr #Hexpr_vars #Hyp_present #cm_cast #Hexpr_vars_cast #Htranslate_cast normalize nodelta #Hexec_cast
2564  #Heq lapply (jmeq_to_eq ??? Heq) -Heq #Heq destruct (Heq)
[2554]2565  whd in Htranslate_cast:(??%%);
2566  whd in Hexpr_vars;
2567  destruct (Htranslate_cast)
2568  [ 1,2,3,4,7:
2569    lapply (Hind cm_castee Hexpr_vars Htranslate_expr … Hyp_present Hexec_cm)
[2565]2570    * #cm_val' * #Heval_castee
2571    lapply Hexec_cm -Hexec_cm
[2554]2572    whd in Hexec_cast:(??%%);
2573    cases cm_val in Hexec_cast; normalize nodelta
2574    [ | #vsz #vi | | #vp
2575    | | #vsz #vi | | #vp
2576    | | #vsz #vi | | #vp
2577    | | #vsz #vi | | #vp
2578    | | #vsz #vi | | #vp ]
2579    [ 2,6,10,14,18:
2580    | *: #Habsurd destruct (Habsurd) ]
2581    #Hexec_cast #Hexec_cm #Hvalue_eq
2582    [ 1,2,3:
2583      cases (intsize_eq_elim_inversion ??????? Hexec_cast) -Hexec_cast
2584      #Hsz_eq destruct (Hsz_eq) #Hcl_val_eq ]
2585    [ 2,3: lapply (sym_eq ??? Hcl_val_eq) -Hcl_val_eq #Hexec_cast ]
2586    [ 1,2,4,5:
2587      cases (bind_inversion ????? Hexec_cast)
2588      whd in match (typeof ?);
2589      #cast_val * whd in ⊢ ((??%%) → ?); normalize nodelta
2590      whd in match (eq_rect_r ??????);
2591      [ 3,4: cases (eq_bv ???) normalize nodelta #Heq destruct (Heq) ]
2592      @(eq_bv_elim … vi (zero (bitsize_of_intsize esz))) normalize nodelta
2593      [ 2,4: #foo #Habsurd destruct (Habsurd) ]
2594      #Heq_vi >eq_intsize_true normalize nodelta #Heq destruct (Heq)
2595      whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
2596      whd in match (typ_of_type ?); whd in match (eval_expr ???????);
2597      >Heval_castee normalize nodelta whd in match (eval_unop ????);
2598      >(value_eq_int_inversion … Hvalue_eq) normalize nodelta
2599      >Heq_vi >eq_bv_true normalize
2600      %{Vnull} @conj try @refl %3
2601    | 3: destruct (Hcl_val_eq)
2602          whd in match (eval_expr ???????);
2603          >Heval_castee normalize nodelta
2604          whd in match (eval_unop ????);
2605          cases esg normalize nodelta
2606          whd in match (opt_to_res ???); whd in match (m_bind ?????);
2607          [ %{(sign_ext sz' cm_val')} | %{(zero_ext sz' cm_val')} ] @conj try @refl
2608          whd in match (eq_rect_r ??????);
2609          -Hexpr_vars -Hyp_present -Hind -Hexec_cm -cm_castee
2610          (* cast_int_int is defined as a let rec on its first argument, we have to eliminate esz for
2611             this reason. *)
2612          lapply Hvalue_eq -Hvalue_eq lapply vi -vi
2613          cases esz normalize nodelta
2614          #vi #Hvalue_eq >(value_eq_int_inversion … Hvalue_eq)
2615          whd in match (sign_ext ??); whd in match (zero_ext ??);
2616          %2
2617    ]
2618 | *:
2619    lapply (Hind cm_expr Hexpr_vars Htranslate_expr … Hyp_present Hexec_cm)
[2565]2620    * #cm_val' * #Heval_expr #Hvalue_eq >Heval_expr
[2554]2621    %{cm_val'} @conj try @refl
[2565]2622    lapply Hexec_cast -Hexec_cast lapply Hvalue_eq -Hvalue_eq
[2554]2623    -Hind -Hexpr_vars -Hyp_present lapply Hexec_cm -Hexec_cm
2624    cases cm_val
2625    [ | #vsz #vi | | #vp
2626    | | #vsz #vi | | #vp
2627    | | #vsz #vi | | #vp
2628    | | #vsz #vi | | #vp ]
2629    #Hexec_cm #Hvalue_eq #Hexec_cast
2630    whd in Hexec_cast:(??%%);
2631    [ 1,5,9,13: destruct (Hexec_cast) ]
2632    [ 2,3,5,6,8,9,11,12: destruct (Hexec_cast) try assumption ]
[2565]2633    lapply Hexec_cast -Hexec_cast
[2554]2634    normalize cases (eq_v ?????) normalize
2635    #Habsurd destruct (Habsurd)
[2565]2636 ]
[2554]2637| 9: (* Econdition *) 
2638  #ty #e1 #e2 #e3 #Hind1 #Hind2 #Hind3 whd in match (typeof ?);
2639  #cm_expr #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present
2640  #Hexec_cm
2641  cases (bind_inversion ????? Hexec_cm) -Hexec_cm
2642  * #cm_cond_val #trace_cond0 * #Hexec_cond #Hexec_cm
2643  cases (bind_inversion ????? Hexec_cm) -Hexec_cm
2644  #bool_of_cm_cond_val * #Hexec_bool_of_val #Hexec_cm
2645  cases (bind_inversion ????? Hexec_cm) -Hexec_cm
2646  * #cm_ifthenelse_val #cm_ifthenelse_trace * #Hcm_ifthenelse
2647  whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2648  cases (bind_inversion ????? Htranslate) -Htranslate
2649  * #cm_expr_e1 #Hexpr_vars_e1 * #Htranslate_e1 #Htranslate
2650  cases (bind_inversion ????? Htranslate) -Htranslate
2651  * #cm_expr_e2 #Hexpr_vars_e2 * #Htranslate_e2 #Htranslate
2652  cases (bind_inversion ????? Htranslate) -Htranslate
2653  * #cm_expr_e2_welltyped #Hexpr2_vars_wt * #Htypecheck
[2568]2654  lapply (typ_should_eq_inversion (typ_of_type (typeof e2)) (typ_of_type ty) … Htypecheck) -Htypecheck
[2554]2655  *  #Htypeof_e2_eq_ty
2656  lapply (Hind2 cm_expr_e2 Hexpr_vars_e2 Htranslate_e2) -Hind2
2657  lapply Hexpr_vars_e2 -Hexpr_vars_e2 lapply cm_expr_e2 -cm_expr_e2
2658  >Htypeof_e2_eq_ty #cm_expr_e2 #Hexpr_vars_e2 #Hind2 
2659  #Hjm_type_eq lapply (jmeq_to_eq ??? Hjm_type_eq) -Hjm_type_eq
2660  #Hcmexpr_eq2 destruct (Hcm_expr_eq2) #Htranslate
2661  cases (bind_inversion ????? Htranslate) -Htranslate
2662  * #cm_expr_e3 #Hexpr_vars_e3 * #Htranslate_e3 #Htranslate 
2663  cases (bind_inversion ????? Htranslate) -Htranslate 
2664  * #cm_expr_e3_welltyped #Hexpr3_vars_wt * #Htypecheck
[2568]2665  lapply (typ_should_eq_inversion (typ_of_type (typeof e3)) (typ_of_type ty) … Htypecheck) -Htypecheck
[2554]2666  * #Htypeof_e3_eq_ty
2667  lapply (Hind3 cm_expr_e3 Hexpr_vars_e3 Htranslate_e3) -Hind3
2668  lapply Hexpr_vars_e3 -Hexpr_vars_e3 lapply cm_expr_e3 -cm_expr_e3
2669  >Htypeof_e3_eq_ty #cm_expr_e3 #Hexpr_vars_e3 #Hind3
2670  #Hjm_type_eq lapply (jmeq_to_eq ??? Hjm_type_eq) -Hjm_type_eq
2671  #Hcmexpr_eq3 destruct (Hcm_expr_eq2)
2672  lapply (Hind1 cm_expr_e1 Hexpr_vars_e1 Htranslate_e1) -Hind1 
2673  lapply Hexpr_vars_e1 -Hexpr_vars_e1 lapply cm_expr_e1 -cm_expr_e1
2674  lapply Hexec_bool_of_val -Hexec_bool_of_val
2675  cases (typeof e1) normalize nodelta
2676  [ | #esz #esg | #eptr_ty | #earray_ty #earray_sz | #edomain #ecodomain
2677  | #estructname #efieldspec | #eunionname #efieldspec | #eid ]
2678  #Hexec_bool_of_val #cm_expr_e1 #Hexpr_vars_e1 #Hind1 #Heq
2679  whd in Heq:(???%); destruct (Heq)
2680  whd in match (eval_expr ???????);
2681  whd in Hyp_present; cases Hyp_present * #Hyp1 #Hyp2 #Hyp3 -Hyp_present
2682  lapply (Hind1 … Hyp1 Hexec_cond) -Hind1 * #cm_val_e1 * #Heval_e1 #Hvalue_eq1
2683  >Heval_e1 normalize nodelta
2684  lapply Hcm_ifthenelse -Hcm_ifthenelse
2685  lapply Hexec_cond -Hexec_cond 
2686  lapply Hexec_bool_of_val -Hexec_bool_of_val
2687  lapply Hvalue_eq1 -Hvalue_eq1
2688  cases cm_cond_val
2689  [ | #vsz #vi | | #vp
2690  | | #vsz #vi | | #vp
2691  | | #vsz #vi | | #vp
2692  | | #vsz #vi | | #vp ]
2693  whd in ⊢ (? → (??%%) → ?);
2694  [ 6:
2695  | *: #_ #Habsurd destruct (Habsurd) ]
2696  #Hvalue_eq1 #Hsz_check
2697  lapply (intsize_eq_elim_inversion ??????? Hsz_check) -Hsz_check
2698  * #Hsz_eq destruct (Hsz_eq) whd in match (eq_rect_r ??????);
2699  #Heq destruct (Heq)
2700  #Hexec_expr_e1
2701  @(match (eq_bv (bitsize_of_intsize esz) vi (zero (bitsize_of_intsize esz)))
2702    return λx. ((eq_bv (bitsize_of_intsize esz) vi (zero (bitsize_of_intsize esz))) = x) → ?
2703    with
2704    [ true ⇒ λHeq. ?
2705    | false ⇒ λHeq. ?
2706    ] (refl ? (eq_bv (bitsize_of_intsize esz) vi (zero (bitsize_of_intsize esz)))))
2707  normalize nodelta
2708  >(value_eq_int_inversion … Hvalue_eq1) #Hexec_expr_body
2709  whd in match (eval_bool_of_val ?); whd in match (m_bind ?????);
2710  >Heq normalize nodelta
2711  [ -Heq -Hexec_expr_e1 -Hvalue_eq1 -Heval_e1 -cm_val_e1 -Hexpr_vars_e1 destruct (Hcmexpr_eq3)
2712    cases (Hind3 … Hyp3 Hexec_expr_body) #cm_val3 * #Heval_expr >Heval_expr #Hvalue_eq
2713    normalize %{cm_val3} @conj try @refl assumption
2714  | -Heq -Hexec_expr_e1 -Hvalue_eq1 -Heval_e1 -cm_val_e1 -Hexpr_vars_e1 destruct (Hcmexpr_eq2)
2715    cases (Hind2 … Hyp2 Hexec_expr_body) #cm_val2 * #Heval_expr >Heval_expr #Hvalue_eq
2716    normalize %{cm_val2} @conj try @refl assumption ]
2717| 10: (* andbool *)
[2545]2718  #ty cases ty
[2554]2719  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
[2545]2720  | #structname #fieldspec | #unionname #fieldspec | #id ]
[2554]2721  #e1 #e2 #Hind1 #Hind2 whd in match (typeof ?);
2722  #cm_expr #Hexpr_vars #Htranslate #cl_final_val #trace #Hyp_present #Hexec_expr
2723  (* decompose first slice of clight execution *)
2724  cases (bind_inversion ????? Hexec_expr) -Hexec_expr
2725  * #cl_val_e1 #cm_trace_e1 * #Hexec_e1 #Hexec_expr
2726  cases (bind_inversion ????? Hexec_expr) -Hexec_expr
2727  #b * #Hexec_bool_of_val #Hexec_expr
2728  (* decompose translation to Cminor *)
2729  cases (bind_inversion ????? Htranslate) -Htranslate normalize nodelta
2730  * #cm_expr_e1 #Hexpr_vars_e1 * #Htranslate_e1 #Htranslate
[2545]2731  cases (bind_inversion ????? Htranslate) -Htranslate
[2554]2732  * #cm_expr_e2 #Hexpr_vars_e2 * #Htranslate_e2 whd in ⊢ ((???%) → ?);
2733  [ 2: | *: #Heq destruct (Heq) ]
2734  (* discriminate I16 and I8 cases *)
2735(*  lapply Hyp_present -Hyp_present
2736  lapply Hexpr_vars -Hexpr_vars
2737  lapply cm_expr -cm_expr cases sz
2738  #cm_expr #Hexpr_vars #Hyp_present normalize nodelta
2739  [ 1,2: #Habsurd destruct (Habsurd) ]   *)
2740  (* go on with decomposition *)
2741  #Htranslate cases (bind_inversion ????? Htranslate) -Htranslate
2742  * #cm_expr_e2_welltyped #Hexpr_vars_e2_wt * #Htypecheck
2743  (* cleanup the type coercion *)
2744  lapply (type_should_eq_inversion (typeof e2) (Tint sz sg) … Htypecheck) -Htypecheck
2745  * #Htypeof_e2_eq_ty
2746  lapply (Hind2 cm_expr_e2 Hexpr_vars_e2 Htranslate_e2) -Hind2
2747  lapply Hexpr_vars_e2_wt -Hexpr_vars_e2_wt
2748  lapply cm_expr_e2_welltyped -cm_expr_e2_welltyped whd in match (typ_of_type ?);
2749  lapply Hexpr_vars_e2 -Hexpr_vars_e2
2750  lapply cm_expr_e2 -cm_expr_e2
2751  lapply Hexec_expr -Hexec_expr
2752  >Htypeof_e2_eq_ty normalize nodelta -Htypeof_e2_eq_ty
2753  #Hexec_expr #cm_expr_e2 #Hexpr_vars_e2 #cm_expr_e2_welltyped #Hexpr_vars_e2_wt #Hind2
2754  #Heq_e2_wt lapply (jmeq_to_eq ??? Heq_e2_wt) -Heq_e2_wt #Heq destruct (Heq)
2755  (* Cleanup terminated. We need to perform a case analysis on (typeof e1) in order
2756   * to proceed in decomposing translation. *)
2757  lapply (Hind1 cm_expr_e1 … Hexpr_vars_e1 Htranslate_e1) -Hind1
2758  lapply Hexpr_vars_e1 -Hexpr_vars_e1
2759  lapply cm_expr_e1 -cm_expr_e1
2760  lapply Hexec_bool_of_val -Hexec_bool_of_val
2761  cases (typeof e1)
2762  [ | #sz1 #sg1 | #ptr_ty1 | #array_ty1 #array_sz1 | #domain1 #codomain1
2763  | #structname1 #fieldspec1 | #unionname1 #fieldspec1 | #id1 ]
2764  #Hexec_bool_of_val #cm_expr_e1 #Hexpr_vars_e1 #Hind1
2765  normalize nodelta whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
2766  (* translation decomposition terminated. Reduce goal *)
2767  whd in match (eval_expr ???????);
2768  (* We need Hind1.  *)
2769  cases Hyp_present -Hyp_present * #Hyp1 #Hyp2 #Hyp
2770  lapply (Hind1 … Hyp1 Hexec_e1) -Hind1 * #cm_val_1 * #Heval_expr1 >Heval_expr1 #Hvalue_eq
2771  normalize nodelta
2772  (* peform case analysis to further reduce the goal. *)
2773  lapply Hvalue_eq -Hvalue_eq
2774  lapply Hexec_bool_of_val -Hexec_bool_of_val
2775  whd in match (proj2 ???);
2776  cases cl_val_e1
2777  [ | #vsz #vi | | #vp
2778  | | #vsz #vi | | #vp
2779  | | #vsz #vi | | #vp
2780  | | #vsz #vi | | #vp ]
2781  whd in ⊢ ((??%%) → ?);
2782  [ 6:
2783  | *: #Heq destruct (Heq) ]
2784  #Hsz_check #Hvalue_eq
2785  lapply (intsize_eq_elim_inversion ??????? Hsz_check) -Hsz_check
2786  * #Hsz_eq destruct (Hsz_eq) whd in match (eq_rect_r ??????);
2787  (* preparing case analysis on b *)
2788  lapply Hexec_expr -Hexec_expr
2789  cases b normalize nodelta
2790  [ 2: (* early exit *)
2791       #Heq_early whd in Heq_early:(??%%); destruct (Heq_early)
2792       #Heq_outcome destruct (Heq_outcome) -Heq_outcome
2793       >(value_eq_int_inversion … Hvalue_eq) whd in match (eval_bool_of_val ?);
2794       <e0 whd in match (m_bind ?????);
2795       @cthulhu
2796       (* Pb: incompatible semantics for cl and cm.
2797        * in Cexec/exec_expr : evaluation returns Vfalse:bvint 32 if
2798          first operand is false (for andbool)
2799          . solution 1 : change semantics to return actual value instead of Vfalse
2800          . solution 2 : change toCminor to introduce another test in the program,
2801            returning Vfalse in case of failure instead of actual value
2802        *) ]
2803  #Hexec_expr #Heq_outcome
2804  cases (bind_inversion ????? Hexec_expr) -Hexec_expr
2805  * #cl_val_e2 #trace2 * #Hexec_e2 #Hexec_expr
2806  cases (bind_inversion ????? Hexec_expr) -Hexec_expr
2807  #outcome_bool * #Hexec_bool_outcome whd in ⊢ ((???%) → ?);
2808  #Heq destruct (Heq)
2809  >(value_eq_int_inversion … Hvalue_eq)
2810  whd in match (eval_bool_of_val ?);
2811  destruct (Heq_outcome) <e0 whd in match (m_bind ?????);
2812  normalize nodelta
2813  cases (Hind2 … Hyp2 Hexec_e2) #cm_val_e2 * #Heval_expr #Hvalue_eq2
2814  >Heval_expr normalize nodelta
2815  %{cm_val_e2} @conj try @refl 
2816  whd in Hexec_bool_outcome:(??%%);
2817  normalize nodelta in Hexec_bool_outcome:(??%%);
2818  lapply Hvalue_eq2 -Hvalue_eq2
2819  -Heval_expr
2820  lapply Hexec_bool_outcome -Hexec_bool_outcome
2821  cases cl_val_e2
2822  [ | #vsz2 #vi2 | | #vp2 ] normalize nodelta
2823  #Heq destruct (Heq)
2824  cases (intsize_eq_elim_inversion ??????? Heq)
2825  #Hsz_eq destruct (Hsz_eq) whd in match (eq_rect_r ??????);
2826  cases outcome_bool normalize nodelta
2827  (* Problem. cf prev case. *)
[2545]2828  @cthulhu
[2554]2829| 11: @cthulhu (* symmetric to andbool, waiting to solve pb before copy/paste *)
2830| 12: (* sizeof *)
2831  #ty cases ty
2832  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
2833  | #structname #fieldspec | #unionname #fieldspec | #id ]
2834  #ty' #e #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec_expr
2835  whd in Hexec_expr:(??%?); destruct (Hexec_expr)
2836  normalize in match (typ_of_type ?);
2837  whd in Htranslate:(??%?); destruct (Htranslate)
2838  whd in match (eval_expr ???????);
2839  %{(Vint sz (repr sz (sizeof ty')))} @conj try @refl %2
2840| 13:
2841  #ty #ed #ty' cases ty'
2842  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
2843  | #structname #fieldspec | #unionname #fieldspec | #id ]
2844  #i #Hind #e #Hexpr_vars #Htranslate_addr #cl_blo #cl_off #trace #Hyp_present
2845  #Hexec_lvalue
2846  whd in Hexec_lvalue:(??%?); destruct
2847  [ whd in Htranslate_addr:(??%?);
2848    cases (bind_inversion ????? Htranslate_addr) -Htranslate_addr
2849    * #fieldexpr #Hexpr_vars_field * #Htranslate_field #Htranslate_addr
2850    cases (bind_inversion ????? Htranslate_addr) -Htranslate_addr
2851    #field_off * #Hfield_off whd in ⊢ ((???%) → ?);
2852    #Heq destruct (Heq)
2853    cases Hyp_present -Hyp_present #Hyp_present_fieldexpr #Hyp_present_cst
2854  ]
2855  cases (bind_inversion ????? Hexec_lvalue) -Hexec_lvalue
2856  * * #bl #off #tr * #Hexec_lvalue_ind #Hexec_lvalue   
2857  [ 1: cases (bind_inversion ????? Hexec_lvalue) -Hexec_lvalue #field_off' *
2858       #Hfield_off' whd in ⊢ ((???%) → ?); #H destruct (H)
2859       cases (Hind … Hexpr_vars_field Htranslate_field … Hyp_present_fieldexpr Hexec_lvalue_ind)
2860       #cm_val_field * #Heval_cm #Hvalue_eq
2861       whd in match (eval_expr ???????);
2862       >Heval_cm normalize nodelta
2863       whd in match (eval_expr ???????); whd in match (m_bind ?????);
2864       whd in match (eval_binop ???????); normalize nodelta
2865       cases (value_eq_ptr_inversion … Hvalue_eq) #cm_ptr * #Heq_cm_ptr >Heq_cm_ptr
2866       normalize nodelta #Hptr_translate
2867       %{(Vptr (shift_pointer (bitsize_of_intsize I16) cm_ptr (repr I16 field_off)))}
2868       @conj whd in match (Eapp ??); >(append_nil ? trace) try @refl
2869       %4 whd in Hptr_translate:(??%?) ⊢ (??%?);
2870       cases (E cl_blo) in Hptr_translate; normalize nodelta
2871       [ #H destruct (H) ]
2872       * #BL #OFF normalize nodelta #Heq destruct (Heq)
2873       >Hfield_off' in Hfield_off; normalize in ⊢ ((??%%) → ?);
2874       #H destruct (H)
2875       (* again, mismatch in the size of the integers *)
2876       @cthulhu
2877  | 2: normalize in Hexec_lvalue:(???%); destruct (Hexec_lvalue)
2878       cases (Hind … Hexpr_vars Htranslate_addr ??? Hyp_present Hexec_lvalue_ind)
2879       #cm_val * #Heval_expr >Heval_expr #Hvalue_eq
2880       cases (value_eq_ptr_inversion … Hvalue_eq) #cm_ptr * #Hcm_ptr_eq >Hcm_ptr_eq
2881       #Hpointer_translation
2882       %{cm_val} @conj try assumption
2883       destruct @refl
2884   ]
2885| 14: (* cost label *)
2886  #ty (* cases ty
2887  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
2888  | #structname #fieldspec | #unionname #fieldspec | #id ] *)
2889  #l * #ed #ety
2890  whd in match (typeof ?); whd in match (typeof ?);
2891  #Hind #e' #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec_expr
2892  cases (bind_inversion ????? Htranslate) -Htranslate * #cm_expr
2893  #Hexpr_vars * #Htranslate_ind #Htranslate
2894  cases (bind_inversion ????? Htranslate) -Htranslate * #cm_costexpr #Hexpr_vars_costexpr
2895  * whd in ⊢ ((???%) → ?); #H destruct (H) #Htyp_should_eq
2896  whd in match (typeof ?) in Htyp_should_eq:(??%?);
[2565]2897  cases (typ_should_eq_inversion (typ_of_type ety) (typ_of_type ty) ??? Htyp_should_eq)
[2554]2898  #Htyp_eq
2899  lapply Htranslate_ind -Htranslate_ind
2900  lapply Hexpr_vars_costexpr -Hexpr_vars_costexpr
2901  lapply Hexec_expr -Hexec_expr lapply Hyp_present -Hyp_present
2902  lapply Hexpr_vars -Hexpr_vars lapply e' -e'
2903  lapply Hind -Hind lapply cm_expr -cm_expr whd in match (typeof ?);
[2565]2904  <Htyp_eq
[2554]2905  #cm_expr #Hind #e' #Hexpr_vars #Hyp_present #Hexec_expr #Hexpr_vars_costexpr
[2565]2906  #Htranslate_ind #Heq lapply (jmeq_to_eq ??? Heq) -Heq #Heq destruct (Heq)
2907  whd in match (eval_expr ???????);
[2554]2908  cases (bind_inversion ????? Hexec_expr) * #cm_val #cm_trace * #Hexec_expr_ind
2909  whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2910  cases (Hind cm_expr Hexpr_vars Htranslate_ind … Hyp_present Hexec_expr_ind)
2911  #cm_val' * #Heval_expr' #Hvalue_eq
2912  >Heval_expr' normalize nodelta %{cm_val'} @conj try assumption
[2565]2913  >cons_to_append >(nil_append … cm_trace) @refl
[2554]2914| 15: *
2915  [ #sz #i | #var_id | #e1 | #e1 | #op #e1 | #op #e1 #e2 | #cast_ty #e1
2916  | #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
2917  #ty normalize in ⊢ (% → ?);
2918  [ 2,3,12: @False_ind
2919  | *: #_ #e' #Hexpr_vars #Htranslate_addr #cl_blo #cl_off #trace #Hyp_present
2920           normalize #Habsurd destruct (Habsurd) ]
[2527]2921] qed.
[2496]2922
2923
[2489]2924axiom clight_cminor_rel : clight_cminor_inv → Clight_state → Cminor_state → Prop.
2925
2926(* Conjectured simulation results
2927
2928   We split these based on the start state:
2929   
2930   1. ‘normal’ states take some [S n] normal steps and simulates them by [S m]
2931      normal steps in Cminor;
2932   2. call and return steps are simulated by a call/return step plus [m] normal
2933      steps (to copy stack allocated parameters / results); and
2934   3. lone cost label steps are simulates by a lone cost label step
2935   
2936   These should allow us to maintain enough structure to identify the Cminor
2937   subtrace corresponding to a measurable Clight subtrace.
2938 *)
2939
2940definition clight_normal : Clight_state → bool ≝
2941λs. match Clight_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
2942
2943definition cminor_normal : Cminor_state → bool ≝
2944λs. match Cminor_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
2945
2946axiom clight_cminor_normal :
2947  ∀INV:clight_cminor_inv.
2948  ∀s1,s1',s2,tr.
2949  clight_cminor_rel INV s1 s1' →
2950  clight_normal s1 →
2951  ¬ Clight_labelled s1 →
2952  ∃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〉) →
2953  ∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'.
2954    tr = tr' ∧
2955    clight_cminor_rel INV s2 s2'
2956  ).
2957
2958axiom clight_cminor_call_return :
2959  ∀INV:clight_cminor_inv.
2960  ∀s1,s1',s2,tr.
2961  clight_cminor_rel INV s1 s1' →
2962  match Clight_classify s1 with [ cl_call ⇒ true | cl_return ⇒ true | _ ⇒ false ] →
2963  after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
2964  ∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'.
2965    tr = tr' ∧
2966    clight_cminor_rel INV s2 s2'
2967  ).
2968
2969axiom clight_cminor_cost :
2970  ∀INV:clight_cminor_inv.
2971  ∀s1,s1',s2,tr.
2972  clight_cminor_rel INV s1 s1' →
2973  Clight_labelled s1 →
2974  after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
2975  after_n_steps 1 … Cminor_exec (ge_cm INV) s1' (λs.true) (λtr',s2'.
2976    tr = tr' ∧
2977    clight_cminor_rel INV s2 s2'
2978  ).
2979
Note: See TracBrowser for help on using the repository browser.