source: src/Clight/toCminorCorrectness.ma @ 2562

Last change on this file since 2562 was 2554, checked in by garnier, 8 years ago

Proof of expression translation correctness "mostly" done for CL to CM. Some inconsistencies found in bit width for constants
regarding boolean operators need to be fixed (either by modifying CL semantics of by making CM code generation inefficient).
An inconsistency between clight and cminor expression evaluation was found for cost labels (placed before and after trace) - not
fixed yet, for fear of breaking proofs. One or two small lemmas missing, and most importantly, binary operators not done yet.

File size: 71.9 KB
Line 
1include "Clight/toCminor.ma".
2
3(* When we characterise the local Clight variables, those that are stack
4   allocated are given disjoint regions of the stack. *)
5
6lemma characterise_vars_disjoint : ∀globals,f,vartypes,stacksize,id,n,ty.
7  characterise_vars globals f = 〈vartypes, stacksize〉 →
8  lookup ?? vartypes id = Some ? 〈Stack n,ty〉 →
9  ∀id',n',ty'. id ≠ id' →
10  lookup ?? vartypes id' = Some ? 〈Stack n',ty'〉 →
11  n' + sizeof ty' ≤ n ∨ n + sizeof ty ≤ n'.
12#globals * #ret #args #vars #body #vartypes #stacksize #id #n #ty
13whd in ⊢ (??%? → ?);
14generalize in match vartypes; -vartypes
15generalize in match stacksize; -stacksize
16elim (args@vars)
17[ #stacksize #vartypes #CHAR #L @⊥ whd in CHAR:(??%?); destruct
18  elim globals in L;
19  [ normalize #L destruct
20  | * * #id' #r #ty' #tl #IH
21    whd in match (foldr ?????);
22    #L cases (lookup_add_cases ??????? L)
23    [ * #E1 #E2 destruct
24    | @IH
25    ]
26  ]
27| * #id1 #ty1 #tl #IH #stacksize #vartypes
28  whd in match (foldr ?????);
29  (* Avoid writing out the definition again *)
30  letin ih ≝ (foldr ? (Prod ??) ?? tl) in IH ⊢ %;
31  lapply (refl ? ih) whd in match ih; -ih
32  cases (foldr ? (Prod ??) ?? tl) in ⊢ (???% → %);
33  #vartypes' #stack' #FOLD #IH
34  whd in ⊢ (??(match % with [_⇒?])? → ?);
35  cases (orb ??)
36  #CHAR whd in CHAR:(??%?); destruct
37  #L cases (lookup_add_cases ??????? L)
38  [ 1,3: * #E1 #E2 destruct
39    #id' #n' #ty' #NE >lookup_add_miss /2/
40    #L' %1 -L -IH
41    generalize in match vartypes' in FOLD L' ⊢ %; -vartypes'
42    generalize in match stack'; -stack'
43    elim tl
44    [ #stack' #vartypes2 whd in ⊢ (??%? → ?); #F destruct #L' @⊥
45      elim globals in L';
46      [ normalize #E destruct
47      | * * #id2 #r2 #ty2 #tl2 #IH whd in match (foldr ?????);
48        #L cases (lookup_add_cases ??????? L)
49        [ * #E1 #E2 destruct
50        | @IH
51        ]
52      ]
53    | * #id2 #ty2 #tl2 #IH #stack' #vartypes'
54      whd in ⊢ (??%? → ?); cases (foldr ? (Prod ??) ???) in IH ⊢ %;
55      #vartypes2 #stack2 #IH
56      whd in ⊢ (??%? → ?);
57      cases (orb ??)
58      [ #E whd in E:(??%?); destruct #L cases (lookup_add_cases ??????? L)
59        [ * #E1 #E2 destruct //
60        | #L'' lapply (IH ?? (refl ??) L'') /2/
61        ]
62      | #E whd in E:(??%?); destruct #L cases (lookup_add_cases ??????? L)
63        [ * #E1 #E2 destruct
64        | #L'' lapply (IH ?? (refl ??) L'') /2/
65        ]
66      ]
67    ]
68  | -L #L #id' #n' #ty' #NE #L'
69    cases (lookup_add_cases ??????? L')
70    [ * #E1 #E2 destruct
71      %2 -IH -L'
72      generalize in match vartypes' in FOLD L; -vartypes'
73      generalize in match stack'; -stack'
74      elim tl
75      [ #stack' #vartypes' whd in ⊢ (??%? → ?); #F destruct #L @⊥
76        elim globals in L;
77        [ normalize #E destruct
78        | * * #id1 #r1 #ty1 #tl1 #IH whd in match (foldr ?????);
79          #L cases (lookup_add_cases ??????? L)
80          [ * #E1 #E2 destruct
81          | @IH
82          ]
83        ]
84      | * #id1 #ty1 #tl1 #IH #stack' #vartypes'
85        whd in ⊢ (??%? → ?); cases (foldr ? (Prod ??) ???) in IH ⊢ %;
86        #vartypes2 #stack2 #IH
87        whd in ⊢ (??%? → ?);
88        cases (orb ??)
89        #E whd in E:(??%?); destruct
90        #L cases (lookup_add_cases ??????? L)
91        [ 1,3: * #E1 #E2 destruct //
92        | 2,4: #L' lapply (IH ?? (refl ??) L') /2/
93        ]
94      ]
95    | @(IH … (refl ??) L … NE)
96    ]
97  | -L #L #id' #n' #ty' #NE #L'
98    cases (lookup_add_cases ??????? L')
99    [ * #E1 #E2 destruct
100    | @(IH … (refl ??) L … NE)
101    ]
102  ]
103] qed.
104
105(* And everything is in the stack frame. *)
106
107lemma characterise_vars_in_range : ∀globals,f,vartypes,stacksize,id,n,ty.
108  characterise_vars globals f = 〈vartypes, stacksize〉 →
109  lookup ?? vartypes id = Some ? 〈Stack n,ty〉 →
110  n + sizeof ty ≤ stacksize.
111#globals * #ret #args #vars #body whd in match (characterise_vars ??);
112elim (args@vars)
113[ #vartypes #stacksize #id #n #ty #FOLD #L @⊥
114  whd in FOLD:(??%?); destruct elim globals in L;
115  [ #E normalize in E; destruct
116  | * * #id' #r' #ty' #tl' #IH
117    whd in match (foldr ?????); #L cases (lookup_add_cases ??????? L)
118    [ * #E1 #E2 destruct
119    | @IH
120    ]
121  ]
122| * #id' #ty' #tl #IH #vartypes #stacksize #id #n #ty
123  whd in match (foldr ?????); cases (foldr ? (Prod ??) ???) in IH ⊢ %;
124  #vartypes' #stackspace' #IH
125  whd in ⊢ (??(match % with [_⇒?])? → ?);
126  cases (orb ??) whd in ⊢ (??%? → ?);
127  #E destruct #L cases (lookup_add_cases ??????? L)
128  [ 1,3: * #E1 #E2 destruct //
129  | 2,4: #L' lapply (IH … (refl ??) L') /2/
130  ]
131] qed.
132
133(* Local variables show up in the variable characterisation as local. *)
134
135lemma characterise_vars_localid : ∀globals,f,vartypes,stacksize,id.
136  characterise_vars globals f = 〈vartypes, stacksize〉 →
137  Exists ? (λx. \fst x = id) (fn_params f @ fn_vars f) →
138  ∃t. local_id vartypes id t.
139#globals * #ret #args #vars #body
140whd in match (characterise_vars ??); elim (args@vars)
141[ #vartypes #stacksize #id #_ *
142| * #hd #ty #tl #IH
143  #vartypes #stacksize #id
144  whd in match (foldr ?????);
145  cases (foldr ? (Prod ??) ???) in IH ⊢ %;
146  #vartypes' #stackspace' #IH
147  whd in ⊢ (??(match % with [_⇒?])? → ?);
148  cases (orb ??)
149  #E whd in E:(??%?); destruct *
150  [ 1,3: #E destruct %{(typ_of_type ty)}
151    whd whd in match (lookup' ??); >lookup_add_hit //
152  | 2,4: #TL cases (IH … (refl ??) TL) #ty' #LC
153    cases (identifier_eq ? id hd)
154    [ 1,3: #E destruct %{(typ_of_type ty)} whd whd in match (lookup' ??); >lookup_add_hit //
155    | 2,4: #NE %{ty'} whd whd in match (lookup' ??); >lookup_add_miss //
156    ]
157  ]
158] qed.
159
160(* Put knowledge that Globals are global into a more useful form than the
161   one used for the invariant. *)
162
163lemma characterise_vars_global : ∀globals,f,vartypes,stacksize.
164  characterise_vars globals f = 〈vartypes, stacksize〉 →
165  ∀id,r,ty. lookup' vartypes id = OK ? 〈Global r,ty〉 →
166  Exists ? (λx.x = 〈〈id,r〉,ty〉) globals ∧
167  ¬ Exists ? (λx. \fst x = id) (fn_params f @ fn_vars f).
168#globals #f #vartypes #stacksize #CHAR #id #r #ty #L
169cases (characterise_vars_src … CHAR id ?)
170[ * #r' * #ty' >L
171  * #E1 destruct (E1) #EX
172  %
173  [ @EX
174  | % #EX' cases (characterise_vars_localid … CHAR EX')
175    #ty' whd in ⊢ (% → ?); >L *
176  ]
177| * #ty' whd in ⊢ (% → ?); >L *
178| whd >(opt_eq_from_res ???? L) % #E destruct
179] qed.
180
181
182(* Show how the global environments match up. *)
183
184lemma map_partial_All_to_All2 : ∀A,B,P,f,l,H,l'.
185  map_partial_All A B P f l H = OK ? l' →
186  All2 ?? (λa,b. ∃p. f a p = OK ? b) l l'.
187#A #B #P #f #l
188elim l
189[ #H #l' #MAP normalize in MAP; destruct //
190| #h #t #IH * #p #H #l'
191  whd in ⊢ (??%? → ?);
192  lapply (refl ? (f h p)) whd in match (proj1 ???);
193  cases (f h p) in ⊢ (???% → %);
194  [ #b #E #MAP cases (bind_inversion ????? MAP)
195    #tl' * #MAP' #E' normalize in E'; destruct
196    % [ %{p} @E | @IH [ @H | @MAP' ] ]
197  | #m #_ #X normalize in X; destruct
198  ]
199] qed.
200 
201
202definition clight_cminor_matching : clight_program → matching ≝
203λp.
204  let tmpuniverse ≝ universe_for_program p in
205  let fun_globals ≝ map ?? (λidf. 〈\fst idf,Code,type_of_fundef (\snd idf)〉) (prog_funct ?? p) in
206  let var_globals ≝ map ?? (λv. 〈\fst (\fst v), \snd (\fst v), \snd (\snd v)〉) (prog_vars ?? p) in
207  let globals ≝ fun_globals @ var_globals in
208  mk_matching
209    ?? (list init_data × type) (list init_data)
210    (λvs,f_clight,f_cminor. ∃H1,H2. translate_fundef tmpuniverse globals H1 f_clight H2 = OK ? f_cminor)
211    (λv,w. \fst v = w).
212
213lemma clight_to_cminor_varnames : ∀p,p'.
214  clight_to_cminor p = OK ? p' →
215  prog_var_names … p = prog_var_names … p'.
216* #vars #fns #main * #vars' #fns' #main'
217#TO cases (bind_inversion ????? TO) #fns'' * #MAP #E
218whd in E:(??%%); destruct
219-MAP normalize
220elim vars
221[ //
222| * * #id #r * #d #t #tl #IH normalize >IH //
223] qed.
224
225
226lemma clight_to_cminor_matches : ∀p,p'.
227  clight_to_cminor p = OK ? p' →
228  match_program (clight_cminor_matching p) p p'.
229* #vars #fns #main * #vars' #fns' #main'
230#TO cases (bind_inversion ????? TO) #fns'' * #MAP #E
231whd in E:(??%%); destruct
232%
233[ -MAP whd in match (m_V ?); whd in match (m_W ?);
234  elim vars
235  [ //
236  | * * #id #r * #init #ty #tl #IH %
237    [ % //
238    | @(All2_mp … IH) * * #a #b * #c #d * * #e #f #g * /2/
239    ]
240  ]
241| @(All2_mp … (map_partial_All_to_All2 … MAP)) -MAP
242  * #id #f * #id' #f' * #H #F cases (bind_inversion ????? F) #f'' * #TRANSF #E
243  normalize in E; destruct
244  <(clight_to_cminor_varnames … TO)
245  % whd
246  % [2: % [2: @TRANSF | skip ] | skip ]
247| %
248] qed.
249
250include "Clight/Cexec.ma".
251include "Clight/abstract.ma".
252include "Cminor/abstract.ma".
253
254(* Invariants used in simulation *)
255
256record clight_cminor_inv : Type[0] ≝ {
257  globals : list (ident × region × type);
258  ge_cl : genv_t clight_fundef;
259  ge_cm : genv_t (fundef internal_function);
260  eq_sym : ∀s. find_symbol … ge_cl s = find_symbol … ge_cm s;
261  trans_fn : ∀v,f. find_funct … ge_cl v = Some ? f →
262    ∃tmp_u,f',H1,H2.
263      translate_fundef tmp_u globals H1 f H2 = OK ? f' ∧
264      find_funct … ge_cm v = Some ? f'
265}.
266
267include "Clight/CexecInd.ma".
268include "Clight/frontend_misc.ma".
269include "Clight/memoryInjections.ma".
270
271lemma intsize_eq_inversion :
272  ∀sz,sz'.
273  ∀A:Type[0].
274  ∀ok,not_ok.
275  intsize_eq_elim' sz sz' (λsz,sz'. res A)
276                          (OK ? ok)
277                          (Error ? not_ok) = (OK ? ok) →
278  sz = sz'.
279* * try // normalize
280#A #ok #not_ok #Habsurd destruct
281qed.
282
283(* Perhaps we will have to be more precise on what is allocated, etc.
284   cf [exec_alloc_variables]. For now this is conveniently hidden in
285   the [value_eq E v v'] *)
286definition memory_matching ≝
287  λE:embedding.
288  λm,m':mem.
289  λen:cl_env.
290  λvenv:cm_env.
291  λcminv:clight_cminor_inv.
292  λsp:block.
293  λvars:var_types.
294  ∀id.
295    match lookup SymbolTag ? en id with
296    [ None ⇒
297      match find_symbol ? (ge_cl cminv) id with
298      [ None ⇒ True
299      | Some cl_blo ⇒ E cl_blo = Some ? 〈cl_blo, zero_offset〉
300      ]
301    | Some cl_blo ⇒
302         match lookup ?? vars id with
303         [ Some kind ⇒
304            let 〈vtype, type〉 ≝ kind in
305            match vtype with
306            [ Stack n ⇒
307              E cl_blo = Some ? 〈sp, mk_offset (repr I16 n)〉
308            | Local ⇒
309              ∀v. load_value_of_type type m cl_blo zero_offset = Some ? v →
310                   ∃v'. lookup ?? venv id = Some ? v' ∧
311                        value_eq E v v'
312            | _ ⇒ False ]
313        | None ⇒ False ]
314    ].
315             
316lemma type_should_eq_inversion :
317  ∀ty1,ty2,P,f,res.
318    type_should_eq ty1 ty2 P f = OK ? res →
319    ty1 = ty2 ∧ f ≃ res.
320#ty1 #ty2 #P #f #res normalize
321cases (type_eq_dec ty1 ty2) normalize nodelta
322[ 2: #Hneq #Habsurd destruct ]
323#Heq #Heq2 @conj try assumption
324destruct (Heq2) cases Heq normalize nodelta
325@eq_to_jmeq @refl
326qed.
327
328lemma load_value_of_type_by_ref :
329  ∀ty,m,b,off,val.
330    load_value_of_type ty m b off = Some ? val →
331    typ_of_type ty ≃ ASTptr →
332    access_mode ty ≃ By_reference →
333    val = Vptr (mk_pointer b off).
334*
335[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
336| #structname #fieldspec | #unionname #fieldspec | #id ]
337#m #b #off #val
338[ 1,6,7: normalize #Habsurd destruct (Habsurd)
339| 4,5: normalize #Heq #_ #_ destruct @refl
340| 2: #_ normalize #Heq destruct
341| *: #Hload normalize #_ #H
342      lapply (jmeq_to_eq ??? H) #Heq destruct
343] qed.
344
345lemma load_value_of_type_by_value :
346  ∀ty,m,b,off,val.
347  access_mode ty = By_value (typ_of_type ty) →
348  load_value_of_type ty m b off = Some ? val →
349  loadv (typ_of_type ty) m (Vptr (mk_pointer b off)) = Some ? val.
350
351[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
352| #structname #fieldspec | #unionname #fieldspec | #id ]
353#m #b #off #val
354normalize in match (access_mode ?);
355[ 1,4,5,6,7: #Habsurd destruct ]
356#_
357#H @H
358qed.
359
360include "Clight/CexecSound.ma".
361
362lemma lookup_exec_alloc :
363  ∀source_variables, initial_env, env, var_id, clb, m, m'.
364  lookup ?? env var_id = Some ? clb →
365  exec_alloc_variables initial_env m source_variables = 〈env,m'〉 →
366  lookup ?? initial_env var_id = Some ? clb ∨
367  Exists ? (λx. \fst x = var_id) source_variables.
368#source_variables
369elim source_variables
370[ 1: #init_env #env #var #clb #m #m' #Hlookup #Hexec_alloc normalize in Hexec_alloc;
371     destruct (Hexec_alloc) %1 @Hlookup
372| 2: * #id #ty #tail #Hind
373     #init_env #env #var #clb #m #m' #Hlookup     
374     whd in ⊢ (??%? → ?);
375     cases (alloc m 0 (sizeof ty) XData) #m0 * #blo #Hreg normalize nodelta
376     #Hexec_alloc
377     @(match identifier_eq ? id var with [ inl Heq ⇒ ? | inr Hneq ⇒ ? ])
378     [ 1: destruct (Heq) %2 %1 @refl ]
379     cases (Hind … Hlookup Hexec_alloc)
380     [ @cthulhu (* standard reasoning on positive_maps. check lib. *)
381     | #Hexists %2 %2 @Hexists ]
382] qed.
383
384lemma characterise_vars_lookup_local :
385  ∀globals,f,vartypes,stacksize,id,clb,env.
386   characterise_vars globals f = 〈vartypes, stacksize〉 →
387   lookup ?? env id = Some ? clb →
388   (∃m,m'. exec_alloc_variables empty_env m (fn_params f @ fn_vars f) = 〈env,m'〉) →
389   ∃t. local_id vartypes id t.
390#globals #f #vartypes #stacksize #id #clb #env
391#Hchar #Hlookup * #m * #m' #Hexec
392cases (lookup_exec_alloc … Hlookup Hexec)
393[ normalize in ⊢ (% → ?); #Heq destruct
394| @(characterise_vars_localid … Hchar) ]
395qed.
396
397
398lemma exec_alloc_fail_antimonotonic : ∀variables,env,env',var_id.
399  (∃m,m'.exec_alloc_variables env m variables=〈env',m'〉) →
400  lookup ?? env' var_id = None ? →
401  lookup ?? env var_id = None ? ∧
402  ¬(Exists (ident×type) (λx:ident×type.\fst  x=var_id) variables). 
403#vars elim vars
404[ #env #env' #var_id normalize * #m * #m' #Heq destruct (Heq)
405  #H @conj try @H % //
406| * #id' #ty' #tl #Hind #env #env' #var * #m * #m'
407  whd in ⊢ ((??%?) → ? → ?);
408  cases (alloc m 0 (sizeof ty') XData) #m0 * #b #Hregion
409  normalize nodelta #Hexec #Hlookup
410  lapply (Hind …  (ex_intro … (ex_intro … Hexec)) Hlookup)
411  cases env #env cases id' #id' cases var #var normalize
412  @(eqb_elim … id' var)
413  [ 2: #Hneq * #Hlookup' #Hexists' lapply (lookup_opt_pm_set_miss ? (Some ? b) … env (sym_neq ??? Hneq))
414       #Heq <Heq @conj try @Hlookup' % *
415       [ #Heq' destruct (Heq') cases Hneq #H @H @refl
416       | cases Hexists' #H @H ]
417  | 1: #Heq destruct (Heq) * #Hlookup' #Hexists'   
418       lapply (lookup_opt_pm_set_hit … (Some ? b) var … env) #H1
419       >H1 in Hlookup'; #Heq destruct
420  ]
421] qed.
422
423lemma variable_not_in_env_but_in_vartypes_is_global :
424  ∀env,env',f,vars,stacksize,globals,var_id.
425  (∃m,m'.exec_alloc_variables env m (fn_params f@fn_vars f) =〈env',m'〉) →
426  characterise_vars globals f =〈vars,stacksize〉 →
427  lookup ?? env' var_id = None ? →       
428  ∀allocty,ty. lookup' vars var_id = OK ? 〈allocty, ty〉 →
429  ∃r.allocty = Global r.
430#env #env' #f #vars #stacksize #globals #var_id#Hexec_alloc
431#Hcharacterise #Hlookup_fail #allocty #ty #Hlookup_type_ok
432lapply (characterise_vars_src … Hcharacterise var_id ?)
433[ whd % cases (res_inversion ?????? Hlookup_type_ok) * #vt #t *
434 #Hlookup >Hlookup #_ #Habsurd destruct ]
435*
436[ 1: * #r * #ty' * #Hlookup' #Hex %{r}
437     >Hlookup' in Hlookup_type_ok; #Heq destruct @refl ]
438* #t whd in ⊢ (% → ?); >Hlookup_type_ok whd normalize nodelta
439@(match allocty
440  return λx. allocty = x → ?
441  with
442  [ Global r ⇒ λ_. ?
443  | Stack st' ⇒ λHalloc. ?
444  | Local ⇒ λHalloc. ?
445  ] (refl ? allocty))
446[ @False_ind ] normalize nodelta
447#Heq_typ
448(* Halloc is in contradiction with Hlookup_fail *)
449lapply (exec_alloc_fail_antimonotonic … Hexec_alloc … Hlookup_fail)
450* #Hlookup' #Hnot_exists
451lapply (characterise_vars_all … Hcharacterise var_id t ?)
452[ 1,3: whd destruct (Halloc) >Hlookup_type_ok // ]
453#Hexists @False_ind
454cut (Exists (ident×type) (λx:ident×type.\fst  x=var_id) (fn_params f@fn_vars f))
455[ 1,3: elim (fn_params f @ fn_vars f) in Hexists; //
456       * #id' #ty' #tl #Hind *
457       [ 1,3: * #Heq #_ %1 @Heq
458       | *: #H %2 @Hind @H ] ]
459#H cases Hnot_exists #H' @H' @H
460qed.
461
462lemma intsize_eq_elim_dec :
463  ∀sz1,sz2.
464  ∀P: ∀sz1,sz2. Type[0].
465  ((∀ifok,iferr. intsize_eq_elim' sz1 sz1 P ifok iferr = ifok) ∧ sz1 = sz2) ∨
466  ((∀ifok,iferr. intsize_eq_elim' sz1 sz2 P ifok iferr = iferr) ∧ sz1 ≠ sz2).
467* * #P normalize
468try /3 by or_introl, conj, refl/
469%2 @conj try //
470% #H destruct
471qed.
472
473lemma typ_eq_elim :
474  ∀t1,t2.
475  ∀(P: (t1=t2)+(t1≠t2) → Prop).
476  (∀H:t1 = t2. P (inl ?? H)) → (∀H:t1 ≠ t2. P (inr ?? H)) → P (typ_eq t1 t2).
477#t1 #t2 #P #Hl #Hr
478@(match typ_eq t1 t2
479  with
480  [ inl H ⇒ Hl H
481  | inr H ⇒ Hr H ])
482qed.
483
484
485lemma translate_notbool_to_cminor :
486  ∀t,sg,arg.
487  ∀cmop. translate_unop (typ_of_type t) (ASTint I32 sg) Onotbool = OK ? cmop →
488  ∀res. sem_unary_operation Onotbool arg t = Some ? res →
489        eval_unop (typ_of_type t) (ASTint I32 sg) cmop arg = Some ? res.
490*
491[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
492| #structname #fieldspec | #unionname #fieldspec | #id ]
493normalize in match (typ_of_type ?);
494#sg #arg #cmop
495whd in ⊢ (??%% → ?); #Heq destruct (Heq)
496cases arg
497[ | #vsz #vi | | #vp
498| | #vsz #vi | | #vp
499| | #vsz #vi | | #vp
500| | #vsz #vi | | #vp
501| | #vsz #vi | | #vp
502| | #vsz #vi | | #vp
503| | #vsz #vi | | #vp
504| | #vsz #vi | | #vp ]
505#res
506whd in ⊢ ((??%?) → ?);
507#Heq
508[ 6,11,12: | *: destruct (Heq) ]
509[ 2,3: destruct (Heq) whd in match (eval_unop ????); @refl
510| 1: lapply Heq -Heq @(eq_intsize_elim … sz vsz)
511     #H normalize nodelta #Heq destruct
512     whd in match (eval_unop ????);
513     cases (eq_bv (bitsize_of_intsize vsz) vi (zero (bitsize_of_intsize vsz))) @refl
514] qed.
515
516lemma translate_notint_to_cminor :
517  ∀t,t',arg.
518  ∀cmop. translate_unop (typ_of_type t) t' Onotint = OK ? cmop →
519  ∀res. sem_unary_operation Onotint arg t = Some ? res →
520        eval_unop (typ_of_type t) t' cmop arg = Some ? res.
521#ty *
522[ 2: #arg #cmop whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) ]
523#sz #sg #arg #cmop
524whd in match (translate_unop ???);
525@(match typ_eq (ASTint sz sg) (typ_of_type ty)
526  with
527  [ inl H ⇒ ?
528  | inr H ⇒ ? ])
529normalize nodelta
530[ 2: #Heq destruct ]
531lapply H -H
532lapply cmop -cmop
533cases ty
534[ | #sz' #sg' | #ptr_ty | #array_ty #array_sz | #domain #codomain
535| #structname #fieldspec | #unionname #fieldspec | #id ]
536normalize nodelta
537#cmop normalize in match (typ_of_type ?); #H destruct
538#H' normalize in H';
539destruct (H')
540#res
541whd in match (sem_unary_operation ???);
542cases arg
543[ | #vsz #vi | | #vp
544| | #vsz #vi | | #vp
545| | #vsz #vi | | #vp
546| | #vsz #vi | | #vp ]
547whd in match (sem_notint ?);
548#H destruct (H) @refl
549qed.
550
551
552lemma translate_negint_to_cminor :
553  ∀t,t',arg.
554  ∀cmop. translate_unop (typ_of_type t) t' Oneg = OK ? cmop →
555  ∀res. sem_unary_operation Oneg arg t = Some ? res →
556        eval_unop (typ_of_type t) t' cmop arg = Some ? res.
557#ty *
558[ 2: #arg #cmop whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) ]
559#sz #sg #arg #cmop
560whd in match (translate_unop ???);
561@(match typ_eq (ASTint sz sg) (typ_of_type ty)
562  with
563  [ inl H ⇒ ?
564  | inr H ⇒ ? ])
565normalize nodelta
566[ 2: #Heq destruct ]
567lapply H -H
568lapply cmop -cmop
569cases ty
570[ | #sz' #sg' | #ptr_ty | #array_ty #array_sz | #domain #codomain
571| #structname #fieldspec | #unionname #fieldspec | #id ]
572normalize nodelta
573#cmop normalize in match (typ_of_type ?); #H destruct
574#H' normalize in H';
575destruct (H')
576#res
577whd in match (sem_unary_operation ???);
578cases arg
579[ | #vsz #vi | | #vp
580| | #vsz #vi | | #vp
581| | #vsz #vi | | #vp
582| | #vsz #vi | | #vp ]
583whd in match (sem_neg ??);
584#H destruct (H)
585whd in match (eval_unop ????);
586cases (eq_intsize sz' vsz) in H; normalize nodelta
587#H destruct @refl
588qed.
589
590
591lemma translate_unop :
592  ∀ty,sg,op,cmop.
593  translate_unop (typ_of_type ty) (ASTint I32 sg) op = OK ? cmop →
594  ∀arg,res. sem_unary_operation op arg ty = Some ? res →
595            eval_unop (typ_of_type ty) (ASTint I32 sg) cmop arg = Some ? res.
596#ty #sg * #cmop #Htranslate #arg
597[ @translate_notbool_to_cminor assumption
598| @translate_notint_to_cminor assumption
599| @translate_negint_to_cminor assumption ]
600qed.
601
602lemma classify_add_inversion :
603  ∀ty1,ty2.
604    (∃sz,sg. ty1 = Tint sz sg ∧ ty2 = Tint sz sg ∧ classify_add ty1 ty2 ≃ add_case_ii sz sg) ∨
605    (∃n,ty',sz,sg. ty1 = ptr_type ty' n ∧ ty2 = Tint sz sg ∧ classify_add ty1 ty2 ≃ add_case_pi n ty' sz sg) ∨
606    (∃n,sz,sg,ty'. ty1 = Tint sz sg ∧ ty2 = ptr_type ty' n ∧ classify_add ty1 ty2 ≃ add_case_ip n sz sg ty') ∨
607    (classify_add ty1 ty2 = add_default ty1 ty2).
608#ty1 #ty2
609cases (classify_add ty1 ty2)
610[ #sz #sg %1 %1 %1 %{sz} %{sg} @conj try @conj try @conj try @refl @refl_jmeq
611| #n #ty #sz #sg %1 %1 %2 %{n} %{ty} %{sz} %{sg} @conj try @conj try @refl @refl_jmeq
612| #n #sz #sg #ty %1 %2 %{n} %{sz} %{sg} %{ty} @conj try @conj try @refl @refl_jmeq
613| #tya #tyb %2 @refl ]
614qed.
615
616lemma typ_should_eq_inversion : ∀ty1,ty2,P,a,x. typ_should_eq ty1 ty2 P a = OK ? x → ty1 = ty2.
617* [ #sz #sg ] * [ 1,3: #sz2 #sg2 ]
618[ 4: #P #a #x normalize #H destruct (H) @refl
619| 3: cases sz cases sg #P #A #x normalize #H destruct
620| 2: cases sz2 cases sg2 #P #a #x normalize #H destruct ]
621cases sz cases sz2 cases sg cases sg2
622#P #a #x #H normalize in H:(??%?); destruct (H)
623try @refl
624qed.
625
626lemma typ_eq_refl : ∀t. typ_eq t t = inl ?? (refl ? t).
627*
628[ * * normalize @refl
629| @refl ]
630qed.
631
632lemma intsize_eq_elim_inversion :
633  ∀A:Type[0].
634  ∀sz1,sz2.
635  ∀elt1,f,errmsg,res. 
636  intsize_eq_elim ? sz1 sz2 bvint elt1 f (Error A errmsg) = OK ? res →
637  ∃H:sz1 = sz2. OK ? res = (f (eq_rect_r ? sz1 sz2 (sym_eq ??? H) ? elt1)).
638#A * * #elt1 #f #errmsg #res normalize #H destruct (H)
639%{(refl ??)} normalize nodelta >H @refl
640qed.
641
642lemma eval_expr_sim :
643  ∀(inv:clight_cminor_inv).
644  ∀(f:function).
645  ∀(vars:var_types).
646  ∀stacksize.
647  characterise_vars (globals inv) f = 〈vars, stacksize〉 →
648  ∀(cl_env:cl_env).
649  (∃m,m'. exec_alloc_variables empty_env m (fn_params f @ fn_vars f) = 〈cl_env,m'〉) →
650  ∀(cl_m:mem).
651  ∀(cm_env:cm_env).
652  ∀(sp:block).
653  ∀(cm_m:mem).
654  ∀E:embedding.
655  ∀minj:memory_inj E cl_m cm_m.
656  memory_matching E cl_m cm_m cl_env cm_env inv sp vars →
657  (* clight expr to cminor expr *)
658  (∀(e:expr).
659   ∀(e':CMexpr (typ_of_type (typeof e))).
660   ∀Hexpr_vars.
661   translate_expr vars e = OK ? («e', Hexpr_vars») →
662   ∀cl_val,trace,Hyp_present.
663   exec_expr (ge_cl … inv) cl_env cl_m e = OK ? 〈cl_val, trace〉 →
664   ∃cm_val. eval_expr (ge_cm inv) (typ_of_type (typeof e)) e' cm_env Hyp_present sp cm_m = OK ? 〈trace, cm_val〉 ∧
665            value_eq E cl_val cm_val) ∧
666   (* clight /lvalue/ to cminor /expr/ *)
667  (∀ed,ty.
668   ∀(e':CMexpr ASTptr).
669   ∀Hexpr_vars.
670   translate_addr vars (Expr ed ty) = OK ? («e', Hexpr_vars») →
671   ∀cl_blo,cl_off,trace,Hyp_present.
672   exec_lvalue' (ge_cl … inv) cl_env cl_m ed ty = OK ? 〈cl_blo, cl_off, trace〉 →
673   ∃cm_val. eval_expr (ge_cm inv) ASTptr e' cm_env Hyp_present sp cm_m = OK ? 〈trace, cm_val〉 ∧
674            value_eq E (Vptr (mk_pointer cl_blo cl_off)) cm_val).
675#inv #f #vars #stacksize #Hcharacterise #cl_env #Hexec_alloc #cl_m #cm_env #sp #cm_m #E #Hinj #Hlocal_matching
676@expr_lvalue_ind_combined
677[ 1: (* Integer constant *)
678  #csz #ty cases ty
679  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
680  | #structname #fieldspec | #unionname #fieldspec | #id ]
681  #i whd in match (typeof ?); #e' #Hexpr_vars #Htranslate
682  #val #trace #Hpresent #Hexec_cl
683  whd in Htranslate:(??%?);
684  [ 1,3,4,5,6,7,8: destruct ]
685  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))))
686  [ 2: * #H_err #H_neq_sz
687       lapply (H_err (OK ? «Cst (ASTint csz sg) (Ointconst csz sg i),I») (Error ? (msg TypeMismatch)))
688       >Htranslate #Habsurd destruct (Habsurd) ]
689  * #H_ok #Heq_sz lapply (H_ok (OK ? «Cst (ASTint csz sg) (Ointconst csz sg i),I») (Error ? (msg TypeMismatch)))
690  destruct (Heq_sz)
691  >Htranslate -Htranslate -H_ok #Heq destruct (Heq)
692  whd in Hexec_cl:(??%?); >eq_intsize_true in Hexec_cl; normalize nodelta
693  #Heq destruct (Heq) %{(Vint sz i)} @conj try @refl //
694| 2: *
695  [ #sz #i | #var_id | * #ed1 #ty1 | #e1 | #op #e1 | #op #e1 #e2 | #cast_ty #e1
696  | #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
697  try /2 by I/
698  #ty whd in ⊢ (% → ?); #Hind
699  whd in match (Plvalue ???);
700  whd in match (typeof ?);
701  #cm_expr #Hexpr_vars #Htranslate_expr #val #trace #Hyp_present #Hexec
702  whd in Hexec:(??%?);
703  whd in match (exec_lvalue' ?????) in Hexec:(??%?);
704  cases (bind_inversion ????? Hexec) -Hexec * * #cl_b #cl_o #cl_t * #Hcl_success #Hcl_load_success
705  whd in Hcl_success:(???%);
706  [ 1: (* var case *)
707       lapply Hcl_success -Hcl_success -Hind
708       (* Peform case analysis on presence of variable in local Clight env.
709        * if success, exec_expr/exec_lvalue tells us that it shoud be local. *)
710       @(match lookup SymbolTag block cl_env var_id
711         return λx.(lookup SymbolTag block cl_env var_id = x) → ?
712         with
713         [ None ⇒ λHcl_lookup. ?
714         | Some loc ⇒ λHcl_lookup. ?
715         ] (refl ? (lookup SymbolTag block cl_env var_id)))
716       normalize nodelta
717       [ 1: (* global case *)
718            #Hlookup_global
719            cases (bind_inversion ????? Hlookup_global) -Hlookup_global #global_block
720            * #Hopt lapply (opt_to_res_inversion ???? Hopt) #Hfind_symbol
721            #Heq whd in Heq:(???%); destruct (Heq)
722            lapply (bind2_eq_inversion ?????? Htranslate_expr) -Htranslate_expr
723            * #var_id_alloctype * #var_id_type * #Heq
724            cases (variable_not_in_env_but_in_vartypes_is_global …
725                        Hexec_alloc Hcharacterise Hcl_lookup ?? Heq)
726            #r #Heq' destruct (Heq') normalize nodelta
727            lapply Hcl_load_success -Hcl_load_success
728            lapply Hyp_present -Hyp_present
729            lapply Hexpr_vars -Hexpr_vars
730            lapply cm_expr -cm_expr inversion (access_mode ty)
731            [ #typ_of_ty | | #typ_of_ty ]
732            #Heq_typ_of_type #Heq_access_mode
733            #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_success normalize nodelta
734            whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
735            whd in match (eval_expr ???????);
736            whd in match (eval_expr ???????);
737            whd in match (eval_constant ????);
738            <(eq_sym … inv) >Hfind_symbol normalize nodelta
739            cases (bind_inversion ????? Hcl_load_success) #x *
740            #Hopt_to_res whd in ⊢ (???% → ?); #Heq_val destruct (Heq_val)
741            lapply (opt_to_res_inversion ???? Hopt_to_res)
742            #Hcl_load_success
743            [ 2: %{(Vptr (mk_pointer cl_b (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 O))))}
744                 @conj try @refl
745                 whd in Hcm_load_success:(??%?);
746                 lapply (jmeq_to_eq ??? Heq_typ_of_type) #Heq_ty
747                 >(load_value_of_type_by_ref … Hcl_load_success)
748                 try assumption %4
749                 lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
750                 >Hfind_symbol normalize nodelta #Heq_embedding
751                 whd in match (shift_offset ???);
752                 >addition_n_0 whd in match (pointer_translation ??); >Heq_embedding
753                 normalize nodelta @refl
754            | 1: cut (access_mode ty=By_value (typ_of_type ty))
755                 [ @jmeq_to_eq lapply (jmeq_to_eq ??? Heq_typ_of_type) #Heqt
756                   lapply Heq_access_mode <Heqt // ] #Haccess
757                 lapply (load_by_value_success_valid_pointer … Haccess … Hcl_load_success)
758                 #Hvalid_ptr
759                 lapply (mi_inj … Hinj ?? cl_b zero_offset … Hvalid_ptr … Hcl_load_success)
760                 [ whd in ⊢ (??%?);
761                   lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
762                   >Hfind_symbol normalize nodelta #Heq_embedding >Heq_embedding @refl ]
763                 * #val' * #Hcm_load_success #Hvalue_eq
764                 lapply (load_value_of_type_by_value … Haccess … Hcm_load_success)
765                 #Hloadv lapply (jmeq_to_eq ??? Heq_typ_of_type) #Htypeq <Htypeq >Hloadv
766                 normalize %{val'} @conj try @refl assumption ]
767       | 2: (* local case *)
768            #Heq destruct (Heq)
769            lapply (bind2_eq_inversion ?????? Htranslate_expr) -Htranslate_expr
770            * #var_id_alloc_type * #var_id_type *
771            generalize in match var_id_alloc_type; * normalize nodelta
772            [ 1: #r #Hlookup_vartype
773                 lapply (characterise_vars_lookup_local … Hcharacterise … Hcl_lookup … Hexec_alloc)
774                 * #typ whd in match (local_id ???);
775                 >Hlookup_vartype normalize nodelta @False_ind
776            | 2: (* Stack local *)
777                 lapply Hcl_load_success -Hcl_load_success
778                 lapply Hyp_present -Hyp_present
779                 lapply Hexpr_vars -Hexpr_vars
780                 lapply cm_expr -cm_expr inversion (access_mode ty)
781                 [ #typ_of_ty | | #typ_of_ty ]
782                 #Heq_typ_of_type #Heq_access_mode
783                 #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_success
784                 #stack_depth #Hlookup_vartype_success normalize nodelta
785                 whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
786                 lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
787                 cases (res_inversion ?????? Hlookup_vartype_success) -Hlookup_vartype_success
788                 * #var_id_alloc_type' #var_id_type' * #Hlookup' #Heq destruct (Heq)
789                 >Hlookup' normalize nodelta #Hembedding_eq
790                 cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success
791                 #loaded_val * #Hload_val
792                 whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
793                 lapply (opt_to_res_inversion ???? Hload_val) -Hload_val
794                 #Hload_success whd in match (eval_expr ???????);
795                 cut (pointer_translation (mk_pointer cl_b zero_offset) E =
796                      Some ? (mk_pointer sp (mk_offset (repr I16 stack_depth))))
797                 [ 1,3: whd in ⊢ (??%?); >Hembedding_eq normalize nodelta
798                        >offset_plus_0 @refl ]
799                 #Hpointer_translation
800                 [ 2: (* By-ref *)
801                      whd in Hload_success:(??%?);
802                      lapply (load_value_of_type_by_ref … Hload_success … Heq_typ_of_type Heq_access_mode)
803                      #Heq_val
804                      >Heq_val
805                      %{(Vptr (mk_pointer sp (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 stack_depth))))}
806                      @conj try @refl
807                      %4 whd in match (shift_offset ???);
808                      whd in match zero_offset;
809                      >commutative_addition_n >addition_n_0 @Hpointer_translation
810                 | 1: (* By value *)
811                      lapply (jmeq_to_eq ??? Heq_typ_of_type) #Heq0                       
812                      lapply (mi_inj … Hinj … Hpointer_translation … Hload_success)
813                      [ @(load_by_value_success_valid_pointer … Hload_success)
814                        lapply Heq_access_mode <Heq0 /2 by jmeq_to_eq/ ]
815                      * #cm_val * #Hload_in_cm #Hvalue_eq
816                      %{cm_val} @conj try assumption
817                      lapply (load_value_of_type_by_value … Hload_in_cm)
818                      [ lapply Heq_access_mode <Heq0 #Heq1
819                        @(jmeq_to_eq ??? Heq1) ]
820                      #Hloadv <Heq0
821                      whd in match (shift_offset ???); >commutative_addition_n >addition_n_0
822                      >Hloadv @refl ]
823            | 3: (* Register local variable *)
824                 #Hlookup_eq
825                 lapply (res_inversion ?????? Hlookup_eq)
826                 * * #var_id_alloc_type' #var_id_type' * #Hlookup' #Heq destruct (Heq)
827                 #Htype_eq
828                 cases (type_should_eq_inversion
829                            var_id_type
830                            ty
831                            (λt0:type.Σe':expr (typ_of_type t0).expr_vars (typ_of_type t0) e' (local_id vars))
832                            … Htype_eq) -Htype_eq
833                 (* Reverting all premises in order to perform type rewrite *)
834                 #Htype_eq
835                 lapply Hlookup' -Hlookup' lapply Hlookup_eq -Hlookup_eq
836                 lapply Hcl_load_success -Hcl_load_success
837                 lapply Hcl_lookup -Hcl_lookup
838                 lapply Hyp_present -Hyp_present
839                 lapply Hexpr_vars -Hexpr_vars
840                 lapply cm_expr
841                 destruct (Htype_eq)
842                 #cm_expr #Hexpr_vars #Hyp_present #Hcl_lookup #Hcl_load_success #Hlookup_eq #Hlookup'
843                 #Hexpr_eq lapply (jmeq_to_eq ??? Hexpr_eq) -Hexpr_eq #Hexpr_eq
844                 destruct (Hexpr_eq)
845                 whd in match (eval_expr ???????);
846                 whd in match (lookup_present ?????);
847                 lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
848                 >Hlookup' normalize nodelta #Hmatching
849                 cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success
850                 #loaded_val * #Hload_val
851                 whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
852                 lapply (opt_to_res_inversion ???? Hload_val) -Hload_val
853                 #Hload_success
854                 cases (Hmatching … Hload_success) #val'
855                 * #Hlookup_in_cm #Hvalue_eq %{val'}
856                 cases Hyp_present
857                 >Hlookup_in_cm normalize nodelta #_ @conj try @refl try assumption
858                 (* seems ok *)
859            ]
860       ]
861  | 2: lapply Hcl_success -Hcl_success
862       lapply Htranslate_expr -Htranslate_expr
863       lapply Hind -Hind cases ty1
864       [ | #sz1 #sg1 | #ptr_ty1 | #array_ty1 #array_sz1 | #domain1 #codomain1
865       | #structname1 #fieldspec1 | #unionname1 #fieldspec1 | #id1 ]
866       #Hind #Htranslate_expr #Hexec_cl
867       cases (bind_inversion ????? Htranslate_expr) -Htranslate_expr
868       * whd in match (typ_of_type ?); normalize nodelta
869       #cm_expr_ind #Hexpr_vars_ind * #Htranslate_expr_ind
870       whd in ⊢ ((???%) → ?);
871       [ 1,2,6,7: #Heq destruct (Heq) ]
872       lapply (Hind cm_expr_ind Hexpr_vars_ind) -Hind
873       whd in match (translate_addr ??); >Htranslate_expr_ind normalize nodelta
874       #Hind lapply (Hind (refl ??) cl_b cl_o cl_t ?) -Hind
875       [ 1,3,5,7: @cthulhu ]
876       whd in match (exec_lvalue' ?????); >Hexec_cl normalize nodelta
877       cases (bind_inversion ????? Hexec_cl) * #cl_ptr #cl_trace0 *
878       #Hexec_cl_ind #Hcl_ptr
879       cut (∃ptr. cl_ptr = Vptr ptr)
880       [ 1,3,5,7: cases cl_ptr in Hcl_ptr; normalize
881                  #H1 destruct #H2 destruct try /2 by ex_intro, refl/ #H3 destruct ]
882       * * #cl_ptr_block #cl_ptr_off -Hcl_ptr
883       #Hcl_ptr destruct (Hcl_ptr) normalize nodelta -Hexec_cl
884       #Hind lapply (Hind (refl ??)) -Hind
885       * #cm_ptr * #Hexec_cm_ind #Hvalue_eq_ind
886       lapply (value_eq_ptr_inversion … Hvalue_eq_ind) * * #cm_ptr_block #cm_ptr_off * #Hcm_ptr
887       destruct (Hcm_ptr) #Hpointer_translation
888       cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success #cl_val * #Hopt_to_res
889       whd in ⊢ ((???%) → ?); #Heq destruct (Heq) lapply (opt_to_res_inversion ???? Hopt_to_res)
890       -Hopt_to_res
891       lapply Hyp_present -Hyp_present
892       lapply Hexpr_vars -Hexpr_vars
893       lapply cm_expr -cm_expr
894       inversion (access_mode ty)
895       [ 1,3,4,6,7,9,10,12: #t ] #Htyp_of_type #Haccess_mode
896       lapply (jmeq_to_eq ??? Htyp_of_type) #Htyp destruct (Htyp)
897       #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_success normalize nodelta
898       #Heq destruct (Heq)
899       [ 1,2,3,4: (* By_value *)
900           (* project Hcl_load_success in Cminor through memory_inj *)
901           lapply (mi_inj ??? Hinj cl_b cl_o cm_ptr_block cm_ptr_off … Hpointer_translation … Hcl_load_success)
902           [ 1,3,5,7: @(load_by_value_success_valid_pointer … Hcl_load_success) @jmeq_to_eq assumption ]
903           * #cm_val * #Hcm_load_success #Hvalue_eq
904           lapply (load_value_of_type_by_value … (jmeq_to_eq ??? Haccess_mode) … Hcm_load_success)
905           #Hloadv_cm
906           whd in match (eval_expr ???????); >Hexec_cm_ind normalize nodelta
907           >Hloadv_cm normalize %{cm_val} @conj try @refl assumption
908      | *: (* By reference *)
909           >Hexec_cm_ind %{(Vptr (mk_pointer cm_ptr_block cm_ptr_off))} @conj try @refl
910           lapply (load_value_of_type_by_ref … Hcl_load_success Htyp_of_type Haccess_mode)
911           #Hval >Hval %4 assumption ]
912  | 3: lapply Hcl_load_success -Hcl_load_success lapply Hcl_success -Hcl_success
913       lapply (refl ? (typeof e1))
914       cases (typeof e1) in ⊢ ((???%) → %);
915       [ | #sz1 #sg1 | #ptr_ty1 | #array_ty1 #array_sz1 | #domain1 #codomain1
916       | #structname1 #fieldspec1 | #unionname1 #fieldspec1 | #id1 ] normalize nodelta
917       #Heq_typeof normalize nodelta
918       [ 1,2,3,4,5,8: #Habsurd destruct ] #Hexec_cl #Hcl_load_success
919       whd in Htranslate_expr:(??%?); >Heq_typeof in Htranslate_expr;
920       normalize nodelta #Htranslate_expr
921       cases (bind_inversion ????? Htranslate_expr) -Htranslate_expr
922       * whd in match (typ_of_type ?); normalize nodelta
923       #cm_expr_ind #Hexpr_vars_ind * #Htranslate_expr_ind #Htranslate_expr2
924       [ cases (bind_inversion ????? Htranslate_expr2) -Htranslate_expr2
925         #cm_field_off * #Hcm_field_off
926       | lapply Htranslate_expr2 -Htranslate_expr2 ]
927       cases (bind_inversion ????? Hexec_cl) -Hexec_cl
928       * * #block_cl #offset_cl #trace0 * #Hexec_lvalue #Hexec_cl
929       whd in Hexec_lvalue:(???%);
930       [ cases (bind_inversion ????? Hexec_cl) -Hexec_cl
931         #cl_field_off * #Hcl_field_off #Hoffset_eq ]
932       cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success
933       #cl_val * #Hopt_cl_val whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
934       lapply (opt_to_res_inversion ???? Hopt_cl_val) -Hopt_cl_val #Hcl_load_value
935       [  (* Struct case *)
936         lapply Hcl_load_value -Hcl_load_value
937         lapply Hyp_present -Hyp_present
938         lapply Hexpr_vars -Hexpr_vars
939         lapply cm_expr -cm_expr
940         lapply Hind -Hind
941         cases ty
942         [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
943         | #structname #fieldspec | #unionname #fieldspec | #id ]
944         #Hind #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_value
945         normalize nodelta
946         whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
947         whd in match (eval_expr ???????);
948         (* applying the arguments of the induction hypothesis progressively *)
949         lapply (Hind (Op2 ASTptr (ASTint I16 Signed) ASTptr (Oaddp I16) cm_expr_ind
950                          (Cst (ASTint I16 Signed) (Ointconst I16 Signed (repr I16 cm_field_off)))) ?)
951         [ 1,3,5,7,9: whd @conj try assumption whd @I ] -Hind #Hind
952         lapply (Hind ?)
953         [ 1,3,5,7,9:
954            whd in ⊢ (??%?); >Heq_typeof normalize nodelta
955            >Htranslate_expr_ind whd in match (m_bind ?????);
956            >Hcm_field_off normalize nodelta @refl ] -Hind #Hind
957         whd in Hoffset_eq:(???%); destruct (offset_eq)
958         cut (cl_field_off = cm_field_off)
959         [ 1,3,5,7,9: lapply Hcl_field_off >Hcm_field_off
960           normalize #Heq destruct (Heq) @refl ]
961         #Heq destruct (Heq)
962         lapply (Hind cl_b cl_o trace ?)
963         [ 1,3,5,7,9: @Hyp_present ] -Hind #Hind
964         lapply (Hind ?) -Hind
965         [ 1,3,5,7,9: whd in ⊢ (??%?); >Heq_typeof normalize nodelta
966           >Hexec_lvalue whd in match (m_bind ?????); >Hcm_field_off normalize nodelta
967           @Hoffset_eq ]
968         * #cm_val' * #Heval_expr #Hvalue_eq
969         lapply (value_eq_ptr_inversion … Hvalue_eq) * * #cm_ptr_block #cm_ptr_off
970         * #Heq_cm_val_ptr destruct (Heq_cm_val_ptr) #Hpointer_trans
971         [ 1,2,5: (* by-value *)
972            lapply (mi_inj … Hinj cl_b cl_o ?? … Hpointer_trans … Hcl_load_value)
973            [ 1,3,5: @(load_by_value_success_valid_pointer … Hcl_load_value) // ]
974            * #cm_val * #Hcm_load_value #Hvalue_eq
975            lapply (load_value_of_type_by_value … Hcm_load_value)
976            [ 1,3,5: @refl ]
977            #Hcm_loadv %{cm_val} >Heval_expr normalize nodelta >Hcm_loadv normalize @conj
978            try @refl try assumption
979         | 3,4: (* by-ref *)
980            whd in match (eval_expr ???????) in Heval_expr; >Heval_expr
981            %{(Vptr (mk_pointer cm_ptr_block cm_ptr_off))} @conj try @refl
982            whd in Hcl_load_value:(??%?); destruct (Hcl_load_value) assumption
983         ]
984      | (* union case *)
985         lapply Hcl_load_value -Hcl_load_value
986         lapply Hyp_present -Hyp_present
987         lapply Hexpr_vars -Hexpr_vars
988         lapply cm_expr -cm_expr
989         lapply Hind -Hind
990         cases ty
991         [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
992         | #structname #fieldspec | #unionname #fieldspec | #id ]
993         whd in match (typ_of_type ?); normalize nodelta
994         #Hind #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_value
995         whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
996         [ 1,2,5: (* by-value *)
997            whd in match (eval_expr ???????);
998            lapply (Hind cm_expr_ind Hexpr_vars ?)
999            [ 1,3,5: whd in ⊢ (??%?); >Heq_typeof normalize nodelta @Htranslate_expr_ind ]
1000            whd in match (exec_lvalue' ?????); >Heq_typeof normalize nodelta
1001            -Hind #Hind
1002            lapply (Hind block_cl offset_cl trace0 Hyp_present) -Hind >Hexec_lvalue normalize nodelta
1003            whd in match (m_bind ?????); #Hind
1004            cases (Hind (refl ??)) -Hind
1005            #cm_val * #Heval_expr #Hvalue_eq >Heval_expr normalize nodelta
1006            cases (value_eq_ptr_inversion … Hvalue_eq) * #cm_block #cm_offset * #Hcm_val #Hpointer_trans
1007            destruct (Hcm_val) whd in Hexec_cl:(???%); destruct (Hexec_cl)
1008            lapply (mi_inj … Hinj cl_b cl_o cm_block cm_offset … Hpointer_trans … Hcl_load_value)
1009            [ 1,3,5: @(load_by_value_success_valid_pointer … Hcl_load_value) // ]
1010            * #cm_val * #Hcm_load_value #Hvalue_eq           
1011            lapply (load_value_of_type_by_value … Hcm_load_value)
1012            [ 1,3,5: @refl ]
1013            #Hcm_loadv %{cm_val} >Hcm_loadv normalize @conj
1014            try @refl assumption
1015         | 3,4:
1016            whd in Hexec_cl:(???%); destruct (Hexec_cl)
1017            lapply (Hind cm_expr Hexpr_vars)
1018            whd in match (translate_addr ??); >Heq_typeof normalize nodelta -Hind #Hind
1019            lapply (Hind Htranslate_expr_ind) -Hind
1020            whd in match (exec_lvalue' ?????); >Heq_typeof normalize nodelta
1021            >Hexec_lvalue whd in match (m_bind ?????);
1022            #Hind cases (Hind … Hyp_present (refl ??))
1023            #cm_val * #Heval_expr #Hvalue_eq >Heval_expr %{cm_val} @conj
1024            try @refl whd in Hcl_load_value:(??%?); destruct (Hcl_load_value)
1025            assumption ]
1026    ]
1027  ]
1028| 3: #var #ty #cmexpr #Hexpr_vars #Htranslate_var #cl_blo #cl_off #trace #Hyp_present #Hexec_lvalue_var
1029     whd in Hexec_lvalue_var:(??%?);
1030     (* check whether var is local or global *)
1031     lapply (Hlocal_matching var)
1032     lapply (variable_not_in_env_but_in_vartypes_is_global  … var Hexec_alloc … Hcharacterise)
1033     cases (lookup ?? cl_env var) in Hexec_lvalue_var;
1034     normalize nodelta
1035     [ 1: (* global *)
1036          #Hexec_opt #H lapply (H (refl ??)) -H #Hvar_is_global
1037          cases (bind_inversion ????? Hexec_opt) -Hexec_opt #varblock * #Hopt_to_res #Heq
1038          whd in Heq:(???%) Hopt_to_res:(???%); destruct (Heq)
1039          lapply (opt_to_res_inversion ???? Hopt_to_res) -Hopt_to_res #Hfind_symbol >Hfind_symbol normalize nodelta
1040          #Hembed
1041          cases (bind_inversion ????? Htranslate_var) -Htranslate_var
1042          * #var_alloctype #var_type * #Hlookup_vartype #Hvar_alloctype
1043          cases (Hvar_is_global … Hlookup_vartype) #r #Halloctype >Halloctype in Hvar_alloctype;
1044          normalize nodelta whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1045          whd in match (eval_expr ???????);
1046          whd in match (eval_constant ????);
1047          <(eq_sym inv var) >Hfind_symbol normalize nodelta
1048          %{(Vptr (mk_pointer cl_blo (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 O))))}
1049          @conj try @refl %4 whd in match (pointer_translation ??);
1050          >Hembed normalize nodelta whd in match (shift_offset ???);
1051          >addition_n_0 @refl
1052     | 2: (* local *)
1053          #BL #Heq destruct (Heq) #_
1054          @(match (lookup ?? vars var)
1055            return λx. (lookup ?? vars var = x) → ?
1056            with
1057            [ None ⇒ ?
1058            | Some kind ⇒ ?
1059            ] (refl ??))
1060          normalize nodelta
1061          #Hlookup [ @False_ind ]
1062          cases kind in Hlookup; #var_alloctype #var_type normalize nodelta
1063          #Hlookup
1064          lapply (refl ? var_alloctype)
1065          cases var_alloctype in ⊢ ((???%) → %); normalize nodelta
1066          [ #reg #Heq @False_ind | #stacksize #Hvar_alloc #Hembed | #Hvar_alloc #Hlookup' ]
1067          [ (* stack alloc*)
1068            cases (bind_inversion ????? Htranslate_var) -Htranslate_var
1069            * #var_alloctype' #var_type' * #Hlookup_vartype'           
1070            whd in Hlookup_vartype':(??%?); >Hlookup in Hlookup_vartype'; normalize nodelta
1071            whd in ⊢ ((???%) → ?); #Heq destruct (Heq) >Hvar_alloc normalize nodelta
1072            whd in ⊢ ((???%) → ?); #Heq destruct (Heq) whd in match (eval_expr ???????);
1073            %{(Vptr (mk_pointer sp (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 stacksize))))}
1074            @conj try @refl %4 whd in match (pointer_translation ??);
1075            >Hembed @refl
1076          | (* local alloc *)
1077            cases (bind_inversion ????? Htranslate_var) -Htranslate_var
1078            * #var_alloctype' #var_type' * #Hlookup_vartype'
1079            whd in Hlookup_vartype':(??%?); >Hlookup in Hlookup_vartype'; normalize nodelta
1080            whd in ⊢ ((???%) → ?); #Heq destruct (Heq) >Hvar_alloc normalize nodelta
1081            whd in ⊢ ((???%) → ?); #Heq destruct (Heq) ] ]
1082(*| 4: #e #ty*)
1083| 4:
1084  * #ed #ety cases ety
1085  [ | #sz1 #sg1 | #ptr_ty1 | #array_ty1 #array_sz1 | #domain1 #codomain1
1086  | #structname1 #fieldspec1 | #unionname1 #fieldspec1 | #id1 ] normalize nodelta 
1087  whd in match (typeof ?);
1088  #ty #Hind #e' #Hexpr_vars #Htranslate #cl_blo #cl_off #trace #Hyp_present #Hexec_lvalue
1089  cases (bind_inversion ????? Htranslate) -Htranslate   
1090  * #cm_expr #Hexpr_vars_cm * #Htranslate_ind
1091  cases (bind_inversion ????? Hexec_lvalue) -Hexec_lvalue
1092  * #cl_val #trace0 * #Hexec_expr #Hcl_val
1093  whd in match (typeof ?); whd in match (typ_of_type ?); normalize nodelta
1094  whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1095  cut (cl_val = Vptr (mk_pointer cl_blo cl_off) ∧ trace = trace0)
1096  [ 1,3,5,7: cases cl_val in Hcl_val; normalize
1097    [ 1,5,9,13: #Heq destruct (Heq)
1098    | 2,6,10,14: #sz #vec #Heq destruct (Heq)
1099    | 3,7,11,15: #Heq destruct (Heq)
1100    | 4,8,12,16: * #BL #OFF #Heq destruct (Heq) @conj try @refl ] ]
1101  * #Heq_cl_val destruct (Heq_cl_val) #Htrace_eq destruct (Htrace_eq)
1102  cases (Hind e' Hexpr_vars Htranslate_ind … Hyp_present … Hexec_expr)
1103  #cm_val * #Heval_expr_cm #Hvalue_eq >Heval_expr_cm
1104  %{cm_val} @conj try @refl try assumption
1105| 5:
1106  #ty cases ty
1107  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1108  | #structname #fieldspec | #unionname #fieldspec | #id ]
1109  #ed #ty' #Hind
1110  whd in match (typeof ?); whd in match (typ_of_type ?); #cm_expr
1111  #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec_expr
1112  cases (bind_inversion ????? Htranslate) -Htranslate
1113  * #cm_expr #Hexpr_vars_cm * #Htranslate_ind
1114  cases (bind_inversion ????? Hexec_expr) -Hexec_expr
1115  * * #cl_blo #cl_off #trace0 * #Hexec_lvalue normalize nodelta
1116  whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1117  whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1118  cases (Hind cm_expr Hexpr_vars Htranslate_ind ??? Hyp_present Hexec_lvalue)
1119  #cm_val * #Hexec_cm #Hvalue_eq >Hexec_cm
1120  %{cm_val} @conj try @refl assumption
1121| 6:
1122  #ty *
1123  [ cases ty
1124    [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1125    | #structname #fieldspec | #unionname #fieldspec | #id ]
1126    #e #Hind
1127    whd in match (typeof ?);
1128    #e' whd in match (typ_of_type ?); #Hexpr_vars whd in ⊢ ((??%?) → ?);
1129    #Htranslate
1130    [ 3,4,5,8: destruct (Htranslate)
1131    | 2: lapply Htranslate -Htranslate lapply Hexpr_vars -Hexpr_vars lapply e' -e'
1132         cases sz normalize nodelta
1133         #e' #Hexpr_vars #Htranslate
1134         [ 1, 2: destruct (Htranslate) ] ]
1135    #cl_val #trace #Hyp_present #Hexec_expr
1136    cases (bind_inversion ????? Htranslate) -Htranslate
1137    #cmop * #Htranslate_unop #Hexec_arg
1138    cases (bind_inversion ????? Hexec_arg) -Hexec_arg
1139    * #cm_arg #Hexpr_vars_arg * #Htranslate whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1140    cases (bind_inversion ????? Hexec_expr) -Hexec_expr
1141    * #cl_arg #cl_trace * #Hexec_cl
1142    whd in ⊢ ((???%) → ?); #Hexec_unop
1143    cases (bind_inversion ????? Hexec_unop) -Hexec_unop
1144    #v * #Hopt whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1145    lapply (opt_to_res_inversion ???? Hopt) -Hopt
1146    #Hsem_cl whd in match (eval_expr ???????);
1147    cases (Hind cm_arg Hexpr_vars Htranslate … Hyp_present Hexec_cl)
1148    #cm_val * #Heval_cm #Hvalue_eq >Heval_cm normalize nodelta
1149    lapply (unary_operation_value_eq … Hvalue_eq … Hsem_cl)
1150    * #cl_val' * #Hcl_unop #Hvalue_eq %{cl_val'} @conj try assumption
1151    whd in match (typ_of_type Tvoid);
1152    lapply (translate_notbool_to_cminor … Htranslate_unop … Hcl_unop)
1153    #H >H @refl
1154  | *:
1155    cases ty
1156    [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id
1157    | | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id ]
1158    #e #Hind whd in match (typeof ?);  whd in match (typ_of_type ?); 
1159    #e' #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec
1160    whd in Htranslate:(??%?);
1161    [ 3,4,5,8,11,12,13,16: destruct (Htranslate) ]
1162    cases (bind_inversion ????? Htranslate) -Htranslate
1163    #cmop * #Htranslate_unop #Hexec_arg
1164    cases (bind_inversion ????? Hexec_arg) -Hexec_arg
1165    * #cm_arg #Hexpr_vars_arg * #Htranslate whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1166    cases (bind_inversion ????? Hexec) -Hexec
1167    * #cl_arg #cl_trace * #Hexec_cl
1168    whd in ⊢ ((???%) → ?); #Hexec_unop
1169    cases (bind_inversion ????? Hexec_unop) -Hexec_unop
1170    #v * #Hopt whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1171    lapply (opt_to_res_inversion ???? Hopt) -Hopt
1172    #Hcl_unop whd in match (eval_expr ???????);
1173    cases (Hind cm_arg Hexpr_vars Htranslate … Hyp_present Hexec_cl)
1174    #op_arg * #Heval_cm #Hvalue_eq >Heval_cm normalize nodelta
1175    lapply (unary_operation_value_eq … Hvalue_eq … Hcl_unop)
1176    * #op_res * #Hcl_sem #Hvalue_eq
1177    [ 1,2,3,4: >(translate_notint_to_cminor … Htranslate_unop … Hcl_sem)
1178       %{op_res} @conj try @refl assumption
1179    | 5,6,7,8: >(translate_negint_to_cminor … Htranslate_unop … Hcl_sem)
1180       %{op_res} @conj try @refl assumption
1181    ]
1182  ]
1183| 7: (* binary ops *)
1184     #ty
1185     letin s ≝ (typ_of_type ty)
1186     #op #e1 #e2
1187     #Hind1 #Hind2 #e' #Hexpr_vars #Htranslate
1188     cases (bind_inversion ????? Htranslate) -Htranslate
1189     * #lhs #Hexpr_vars_lhs * #Htranslate_lhs #Htranslate
1190     cases (bind_inversion ????? Htranslate) -Htranslate
1191     * #rhs #Hexpr_vars_rhs * #Htranslate_rhs
1192     whd in ⊢ ((??%?) → ?);
1193     cases op whd in match (translate_binop ??????);
1194     @cthulhu (* PITA *)
1195| 8: #ty #ty' * #ed #ety
1196  cases ety
1197  [ | #esz #esg | #eptr_ty | #earray_ty #earray_sz | #edomain #ecodomain
1198  | #estructname #efieldspec | #eunionname #efieldspec | #eid ]
1199  whd in match (typeof ?); whd in match (typ_of_type ?);
1200  #Hind whd in match (typeof ?);
1201  #cm_expr #Hexpr_vars #Htranslate
1202  cases (bind_inversion ????? Htranslate) -Htranslate
1203  * #cm_castee #Hexpr_vars_castee * #Htranslate_expr #Htranslate
1204  cases (bind_inversion ????? Htranslate) -Htranslate
1205  * #cm_cast #Hexpr_vars_cast * #Htranslate_cast #Htranslate 
1206  [ 1,5,6,7,8: whd in Htranslate_cast:(??%%); destruct (Htranslate_cast) ]
1207  cases (bind_inversion ????? Htranslate) -Htranslate
1208  * #cm_cast' #Hexpr_vars' * #Htyp_should_eq whd in ⊢ ((??%%) → ?);
1209  #Heq destruct (Heq)
1210  #cl_val #trace #Hyp_present #Hexec_cm
1211  cases (bind_inversion ????? Hexec_cm) -Hexec_cm
1212  * #cm_val #trace0 * #Hexec_cm #Hexec_cast
1213  cases (bind_inversion ????? Hexec_cast) -Hexec_cast
1214  #cast_val * #Hexec_cast
1215  whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
1216  lapply (typ_should_eq_inversion (typ_of_type ty') (typ_of_type ty) … Htyp_should_eq) #Htype_eq
1217  lapply Hexec_cast -Hexec_cast
1218  lapply Htyp_should_eq -Htyp_should_eq
1219  lapply Htranslate_cast -Htranslate_cast
1220  lapply Hexpr_vars_cast -Hexpr_vars_cast
1221  lapply cm_cast -cm_cast
1222  lapply Hyp_present -Hyp_present
1223  lapply Hexpr_vars -Hexpr_vars
1224  lapply cm_expr -cm_expr
1225  <Htype_eq -Htype_eq
1226  whd in ⊢ (? → ? → ? → ? → ? → ? → (??%%) → ?); >typ_eq_refl normalize nodelta
1227  cases ty'
1228  [ | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain' | #structname' #fieldspec' | #unionname' #fieldspec' | #id'
1229  | | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain' | #structname' #fieldspec' | #unionname' #fieldspec' | #id'
1230  | | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain' | #structname' #fieldspec' | #unionname' #fieldspec' | #id' ]
1231  #cm_expr #Hexpr_vars #Hyp_present #cm_cast #Hexpr_vars_cast #Htranslate_cast
1232  whd in match (typ_of_type ?) in cm_castee cm_expr Hexpr_vars_castee;
1233  whd in match (typeof ?) in Htranslate_cast Hexec_cast;
1234  #Heq destruct (Heq)
1235  whd in Htranslate_cast:(??%%);
1236  whd in Hexpr_vars;
1237  destruct (Htranslate_cast)
1238  [ 1,2,3,4,7:
1239    lapply (Hind cm_castee Hexpr_vars Htranslate_expr … Hyp_present Hexec_cm)
1240    * #cm_val' * #Heval_castee #Hvalue_eq #Hexec_cast
1241    lapply Hvalue_eq -Hvalue_eq lapply Hexec_cm -Hexec_cm
1242    whd in Hexec_cast:(??%%);
1243    cases cm_val in Hexec_cast; normalize nodelta
1244    [ | #vsz #vi | | #vp
1245    | | #vsz #vi | | #vp
1246    | | #vsz #vi | | #vp
1247    | | #vsz #vi | | #vp
1248    | | #vsz #vi | | #vp ]
1249    [ 2,6,10,14,18:
1250    | *: #Habsurd destruct (Habsurd) ]
1251    #Hexec_cast #Hexec_cm #Hvalue_eq
1252    [ 1,2,3:
1253      cases (intsize_eq_elim_inversion ??????? Hexec_cast) -Hexec_cast
1254      #Hsz_eq destruct (Hsz_eq) #Hcl_val_eq ]
1255    [ 2,3: lapply (sym_eq ??? Hcl_val_eq) -Hcl_val_eq #Hexec_cast ]
1256    [ 1,2,4,5:
1257      cases (bind_inversion ????? Hexec_cast)
1258      whd in match (typeof ?);
1259      #cast_val * whd in ⊢ ((??%%) → ?); normalize nodelta
1260      whd in match (eq_rect_r ??????);
1261      [ 3,4: cases (eq_bv ???) normalize nodelta #Heq destruct (Heq) ]
1262      @(eq_bv_elim … vi (zero (bitsize_of_intsize esz))) normalize nodelta
1263      [ 2,4: #foo #Habsurd destruct (Habsurd) ]
1264      #Heq_vi >eq_intsize_true normalize nodelta #Heq destruct (Heq)
1265      whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
1266      whd in match (typ_of_type ?); whd in match (eval_expr ???????);
1267      >Heval_castee normalize nodelta whd in match (eval_unop ????);
1268      >(value_eq_int_inversion … Hvalue_eq) normalize nodelta
1269      >Heq_vi >eq_bv_true normalize
1270      %{Vnull} @conj try @refl %3
1271    | 3: destruct (Hcl_val_eq)
1272          whd in match (eval_expr ???????);
1273          >Heval_castee normalize nodelta
1274          whd in match (eval_unop ????);
1275          cases esg normalize nodelta
1276          whd in match (opt_to_res ???); whd in match (m_bind ?????);
1277          [ %{(sign_ext sz' cm_val')} | %{(zero_ext sz' cm_val')} ] @conj try @refl
1278          whd in match (eq_rect_r ??????);
1279          -Hexpr_vars -Hyp_present -Hind -Hexec_cm -cm_castee
1280          (* cast_int_int is defined as a let rec on its first argument, we have to eliminate esz for
1281             this reason. *)
1282          lapply Hvalue_eq -Hvalue_eq lapply vi -vi
1283          cases esz normalize nodelta
1284          #vi #Hvalue_eq >(value_eq_int_inversion … Hvalue_eq)
1285          whd in match (sign_ext ??); whd in match (zero_ext ??);
1286          %2
1287    ]
1288 | *:
1289    lapply (Hind cm_expr Hexpr_vars Htranslate_expr … Hyp_present Hexec_cm)
1290    * #cm_val' * #Heval_expr #Hvalue_eq #Hexec_cast >Heval_expr
1291    %{cm_val'} @conj try @refl
1292    lapply Hexec_cast -Hexec_cast lapply Hvalue_eq -Hvalue_eq
1293    -Hind -Hexpr_vars -Hyp_present lapply Hexec_cm -Hexec_cm
1294    cases cm_val
1295    [ | #vsz #vi | | #vp
1296    | | #vsz #vi | | #vp
1297    | | #vsz #vi | | #vp
1298    | | #vsz #vi | | #vp ]
1299    #Hexec_cm #Hvalue_eq #Hexec_cast
1300    whd in Hexec_cast:(??%%);
1301    [ 1,5,9,13: destruct (Hexec_cast) ]
1302    [ 2,3,5,6,8,9,11,12: destruct (Hexec_cast) try assumption ]
1303    lapply Hexec_cast -Hexec_cast 
1304    normalize cases (eq_v ?????) normalize
1305    #Habsurd destruct (Habsurd)
1306 ]     
1307| 9: (* Econdition *) 
1308  #ty #e1 #e2 #e3 #Hind1 #Hind2 #Hind3 whd in match (typeof ?);
1309  #cm_expr #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present
1310  #Hexec_cm
1311  cases (bind_inversion ????? Hexec_cm) -Hexec_cm
1312  * #cm_cond_val #trace_cond0 * #Hexec_cond #Hexec_cm
1313  cases (bind_inversion ????? Hexec_cm) -Hexec_cm
1314  #bool_of_cm_cond_val * #Hexec_bool_of_val #Hexec_cm
1315  cases (bind_inversion ????? Hexec_cm) -Hexec_cm
1316  * #cm_ifthenelse_val #cm_ifthenelse_trace * #Hcm_ifthenelse
1317  whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1318  cases (bind_inversion ????? Htranslate) -Htranslate
1319  * #cm_expr_e1 #Hexpr_vars_e1 * #Htranslate_e1 #Htranslate
1320  cases (bind_inversion ????? Htranslate) -Htranslate
1321  * #cm_expr_e2 #Hexpr_vars_e2 * #Htranslate_e2 #Htranslate
1322  cases (bind_inversion ????? Htranslate) -Htranslate
1323  * #cm_expr_e2_welltyped #Hexpr2_vars_wt * #Htypecheck
1324  lapply (type_should_eq_inversion (typeof e2) ty … Htypecheck) -Htypecheck
1325  *  #Htypeof_e2_eq_ty
1326  lapply (Hind2 cm_expr_e2 Hexpr_vars_e2 Htranslate_e2) -Hind2
1327  lapply Hexpr_vars_e2 -Hexpr_vars_e2 lapply cm_expr_e2 -cm_expr_e2
1328  >Htypeof_e2_eq_ty #cm_expr_e2 #Hexpr_vars_e2 #Hind2 
1329  #Hjm_type_eq lapply (jmeq_to_eq ??? Hjm_type_eq) -Hjm_type_eq
1330  #Hcmexpr_eq2 destruct (Hcm_expr_eq2) #Htranslate
1331  cases (bind_inversion ????? Htranslate) -Htranslate
1332  * #cm_expr_e3 #Hexpr_vars_e3 * #Htranslate_e3 #Htranslate 
1333  cases (bind_inversion ????? Htranslate) -Htranslate 
1334  * #cm_expr_e3_welltyped #Hexpr3_vars_wt * #Htypecheck
1335  lapply (type_should_eq_inversion (typeof e3) ty … Htypecheck) -Htypecheck
1336  * #Htypeof_e3_eq_ty
1337  lapply (Hind3 cm_expr_e3 Hexpr_vars_e3 Htranslate_e3) -Hind3
1338  lapply Hexpr_vars_e3 -Hexpr_vars_e3 lapply cm_expr_e3 -cm_expr_e3
1339  >Htypeof_e3_eq_ty #cm_expr_e3 #Hexpr_vars_e3 #Hind3
1340  #Hjm_type_eq lapply (jmeq_to_eq ??? Hjm_type_eq) -Hjm_type_eq
1341  #Hcmexpr_eq3 destruct (Hcm_expr_eq2)
1342  lapply (Hind1 cm_expr_e1 Hexpr_vars_e1 Htranslate_e1) -Hind1 
1343  lapply Hexpr_vars_e1 -Hexpr_vars_e1 lapply cm_expr_e1 -cm_expr_e1
1344  lapply Hexec_bool_of_val -Hexec_bool_of_val
1345  cases (typeof e1) normalize nodelta
1346  [ | #esz #esg | #eptr_ty | #earray_ty #earray_sz | #edomain #ecodomain
1347  | #estructname #efieldspec | #eunionname #efieldspec | #eid ]
1348  #Hexec_bool_of_val #cm_expr_e1 #Hexpr_vars_e1 #Hind1 #Heq
1349  whd in Heq:(???%); destruct (Heq)
1350  whd in match (eval_expr ???????);
1351  whd in Hyp_present; cases Hyp_present * #Hyp1 #Hyp2 #Hyp3 -Hyp_present
1352  lapply (Hind1 … Hyp1 Hexec_cond) -Hind1 * #cm_val_e1 * #Heval_e1 #Hvalue_eq1
1353  >Heval_e1 normalize nodelta
1354  lapply Hcm_ifthenelse -Hcm_ifthenelse
1355  lapply Hexec_cond -Hexec_cond 
1356  lapply Hexec_bool_of_val -Hexec_bool_of_val
1357  lapply Hvalue_eq1 -Hvalue_eq1
1358  cases cm_cond_val
1359  [ | #vsz #vi | | #vp
1360  | | #vsz #vi | | #vp
1361  | | #vsz #vi | | #vp
1362  | | #vsz #vi | | #vp ]
1363  whd in ⊢ (? → (??%%) → ?);
1364  [ 6:
1365  | *: #_ #Habsurd destruct (Habsurd) ]
1366  #Hvalue_eq1 #Hsz_check
1367  lapply (intsize_eq_elim_inversion ??????? Hsz_check) -Hsz_check
1368  * #Hsz_eq destruct (Hsz_eq) whd in match (eq_rect_r ??????);
1369  #Heq destruct (Heq)
1370  #Hexec_expr_e1
1371  @(match (eq_bv (bitsize_of_intsize esz) vi (zero (bitsize_of_intsize esz)))
1372    return λx. ((eq_bv (bitsize_of_intsize esz) vi (zero (bitsize_of_intsize esz))) = x) → ?
1373    with
1374    [ true ⇒ λHeq. ?
1375    | false ⇒ λHeq. ?
1376    ] (refl ? (eq_bv (bitsize_of_intsize esz) vi (zero (bitsize_of_intsize esz)))))
1377  normalize nodelta
1378  >(value_eq_int_inversion … Hvalue_eq1) #Hexec_expr_body
1379  whd in match (eval_bool_of_val ?); whd in match (m_bind ?????);
1380  >Heq normalize nodelta
1381  [ -Heq -Hexec_expr_e1 -Hvalue_eq1 -Heval_e1 -cm_val_e1 -Hexpr_vars_e1 destruct (Hcmexpr_eq3)
1382    cases (Hind3 … Hyp3 Hexec_expr_body) #cm_val3 * #Heval_expr >Heval_expr #Hvalue_eq
1383    normalize %{cm_val3} @conj try @refl assumption
1384  | -Heq -Hexec_expr_e1 -Hvalue_eq1 -Heval_e1 -cm_val_e1 -Hexpr_vars_e1 destruct (Hcmexpr_eq2)
1385    cases (Hind2 … Hyp2 Hexec_expr_body) #cm_val2 * #Heval_expr >Heval_expr #Hvalue_eq
1386    normalize %{cm_val2} @conj try @refl assumption ]
1387| 10: (* andbool *)
1388  #ty cases ty
1389  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1390  | #structname #fieldspec | #unionname #fieldspec | #id ]
1391  #e1 #e2 #Hind1 #Hind2 whd in match (typeof ?);
1392  #cm_expr #Hexpr_vars #Htranslate #cl_final_val #trace #Hyp_present #Hexec_expr
1393  (* decompose first slice of clight execution *)
1394  cases (bind_inversion ????? Hexec_expr) -Hexec_expr
1395  * #cl_val_e1 #cm_trace_e1 * #Hexec_e1 #Hexec_expr
1396  cases (bind_inversion ????? Hexec_expr) -Hexec_expr
1397  #b * #Hexec_bool_of_val #Hexec_expr
1398  (* decompose translation to Cminor *)
1399  cases (bind_inversion ????? Htranslate) -Htranslate normalize nodelta
1400  * #cm_expr_e1 #Hexpr_vars_e1 * #Htranslate_e1 #Htranslate
1401  cases (bind_inversion ????? Htranslate) -Htranslate
1402  * #cm_expr_e2 #Hexpr_vars_e2 * #Htranslate_e2 whd in ⊢ ((???%) → ?);
1403  [ 2: | *: #Heq destruct (Heq) ]
1404  (* discriminate I16 and I8 cases *)
1405(*  lapply Hyp_present -Hyp_present
1406  lapply Hexpr_vars -Hexpr_vars
1407  lapply cm_expr -cm_expr cases sz
1408  #cm_expr #Hexpr_vars #Hyp_present normalize nodelta
1409  [ 1,2: #Habsurd destruct (Habsurd) ]   *)
1410  (* go on with decomposition *)
1411  #Htranslate cases (bind_inversion ????? Htranslate) -Htranslate
1412  * #cm_expr_e2_welltyped #Hexpr_vars_e2_wt * #Htypecheck
1413  (* cleanup the type coercion *)
1414  lapply (type_should_eq_inversion (typeof e2) (Tint sz sg) … Htypecheck) -Htypecheck
1415  * #Htypeof_e2_eq_ty
1416  lapply (Hind2 cm_expr_e2 Hexpr_vars_e2 Htranslate_e2) -Hind2
1417  lapply Hexpr_vars_e2_wt -Hexpr_vars_e2_wt
1418  lapply cm_expr_e2_welltyped -cm_expr_e2_welltyped whd in match (typ_of_type ?);
1419  lapply Hexpr_vars_e2 -Hexpr_vars_e2
1420  lapply cm_expr_e2 -cm_expr_e2
1421  lapply Hexec_expr -Hexec_expr
1422  >Htypeof_e2_eq_ty normalize nodelta -Htypeof_e2_eq_ty
1423  #Hexec_expr #cm_expr_e2 #Hexpr_vars_e2 #cm_expr_e2_welltyped #Hexpr_vars_e2_wt #Hind2
1424  #Heq_e2_wt lapply (jmeq_to_eq ??? Heq_e2_wt) -Heq_e2_wt #Heq destruct (Heq)
1425  (* Cleanup terminated. We need to perform a case analysis on (typeof e1) in order
1426   * to proceed in decomposing translation. *)
1427  lapply (Hind1 cm_expr_e1 … Hexpr_vars_e1 Htranslate_e1) -Hind1
1428  lapply Hexpr_vars_e1 -Hexpr_vars_e1
1429  lapply cm_expr_e1 -cm_expr_e1
1430  lapply Hexec_bool_of_val -Hexec_bool_of_val
1431  cases (typeof e1)
1432  [ | #sz1 #sg1 | #ptr_ty1 | #array_ty1 #array_sz1 | #domain1 #codomain1
1433  | #structname1 #fieldspec1 | #unionname1 #fieldspec1 | #id1 ]
1434  #Hexec_bool_of_val #cm_expr_e1 #Hexpr_vars_e1 #Hind1
1435  normalize nodelta whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
1436  (* translation decomposition terminated. Reduce goal *)
1437  whd in match (eval_expr ???????);
1438  (* We need Hind1.  *)
1439  cases Hyp_present -Hyp_present * #Hyp1 #Hyp2 #Hyp
1440  lapply (Hind1 … Hyp1 Hexec_e1) -Hind1 * #cm_val_1 * #Heval_expr1 >Heval_expr1 #Hvalue_eq
1441  normalize nodelta
1442  (* peform case analysis to further reduce the goal. *)
1443  lapply Hvalue_eq -Hvalue_eq
1444  lapply Hexec_bool_of_val -Hexec_bool_of_val
1445  whd in match (proj2 ???);
1446  cases cl_val_e1
1447  [ | #vsz #vi | | #vp
1448  | | #vsz #vi | | #vp
1449  | | #vsz #vi | | #vp
1450  | | #vsz #vi | | #vp ]
1451  whd in ⊢ ((??%%) → ?);
1452  [ 6:
1453  | *: #Heq destruct (Heq) ]
1454  #Hsz_check #Hvalue_eq
1455  lapply (intsize_eq_elim_inversion ??????? Hsz_check) -Hsz_check
1456  * #Hsz_eq destruct (Hsz_eq) whd in match (eq_rect_r ??????);
1457  (* preparing case analysis on b *)
1458  lapply Hexec_expr -Hexec_expr
1459  cases b normalize nodelta
1460  [ 2: (* early exit *)
1461       #Heq_early whd in Heq_early:(??%%); destruct (Heq_early)
1462       #Heq_outcome destruct (Heq_outcome) -Heq_outcome
1463       >(value_eq_int_inversion … Hvalue_eq) whd in match (eval_bool_of_val ?);
1464       <e0 whd in match (m_bind ?????);
1465       @cthulhu
1466       (* Pb: incompatible semantics for cl and cm.
1467        * in Cexec/exec_expr : evaluation returns Vfalse:bvint 32 if
1468          first operand is false (for andbool)
1469          . solution 1 : change semantics to return actual value instead of Vfalse
1470          . solution 2 : change toCminor to introduce another test in the program,
1471            returning Vfalse in case of failure instead of actual value
1472        *) ]
1473  #Hexec_expr #Heq_outcome
1474  cases (bind_inversion ????? Hexec_expr) -Hexec_expr
1475  * #cl_val_e2 #trace2 * #Hexec_e2 #Hexec_expr
1476  cases (bind_inversion ????? Hexec_expr) -Hexec_expr
1477  #outcome_bool * #Hexec_bool_outcome whd in ⊢ ((???%) → ?);
1478  #Heq destruct (Heq)
1479  >(value_eq_int_inversion … Hvalue_eq)
1480  whd in match (eval_bool_of_val ?);
1481  destruct (Heq_outcome) <e0 whd in match (m_bind ?????);
1482  normalize nodelta
1483  cases (Hind2 … Hyp2 Hexec_e2) #cm_val_e2 * #Heval_expr #Hvalue_eq2
1484  >Heval_expr normalize nodelta
1485  %{cm_val_e2} @conj try @refl 
1486  whd in Hexec_bool_outcome:(??%%);
1487  normalize nodelta in Hexec_bool_outcome:(??%%);
1488  lapply Hvalue_eq2 -Hvalue_eq2
1489  -Heval_expr
1490  lapply Hexec_bool_outcome -Hexec_bool_outcome
1491  cases cl_val_e2
1492  [ | #vsz2 #vi2 | | #vp2 ] normalize nodelta
1493  #Heq destruct (Heq)
1494  cases (intsize_eq_elim_inversion ??????? Heq)
1495  #Hsz_eq destruct (Hsz_eq) whd in match (eq_rect_r ??????);
1496  cases outcome_bool normalize nodelta
1497  (* Problem. cf prev case. *)
1498  @cthulhu
1499| 11: @cthulhu (* symmetric to andbool, waiting to solve pb before copy/paste *)
1500| 12: (* sizeof *)
1501  #ty cases ty
1502  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1503  | #structname #fieldspec | #unionname #fieldspec | #id ]
1504  #ty' #e #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec_expr
1505  whd in Hexec_expr:(??%?); destruct (Hexec_expr)
1506  normalize in match (typ_of_type ?);
1507  whd in Htranslate:(??%?); destruct (Htranslate)
1508  whd in match (eval_expr ???????);
1509  %{(Vint sz (repr sz (sizeof ty')))} @conj try @refl %2
1510| 13:
1511  #ty #ed #ty' cases ty'
1512  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1513  | #structname #fieldspec | #unionname #fieldspec | #id ]
1514  #i #Hind #e #Hexpr_vars #Htranslate_addr #cl_blo #cl_off #trace #Hyp_present
1515  #Hexec_lvalue
1516  whd in Hexec_lvalue:(??%?); destruct
1517  [ whd in Htranslate_addr:(??%?);
1518    cases (bind_inversion ????? Htranslate_addr) -Htranslate_addr
1519    * #fieldexpr #Hexpr_vars_field * #Htranslate_field #Htranslate_addr
1520    cases (bind_inversion ????? Htranslate_addr) -Htranslate_addr
1521    #field_off * #Hfield_off whd in ⊢ ((???%) → ?);
1522    #Heq destruct (Heq)
1523    cases Hyp_present -Hyp_present #Hyp_present_fieldexpr #Hyp_present_cst
1524  ]
1525  cases (bind_inversion ????? Hexec_lvalue) -Hexec_lvalue
1526  * * #bl #off #tr * #Hexec_lvalue_ind #Hexec_lvalue   
1527  [ 1: cases (bind_inversion ????? Hexec_lvalue) -Hexec_lvalue #field_off' *
1528       #Hfield_off' whd in ⊢ ((???%) → ?); #H destruct (H)
1529       cases (Hind … Hexpr_vars_field Htranslate_field … Hyp_present_fieldexpr Hexec_lvalue_ind)
1530       #cm_val_field * #Heval_cm #Hvalue_eq
1531       whd in match (eval_expr ???????);
1532       >Heval_cm normalize nodelta
1533       whd in match (eval_expr ???????); whd in match (m_bind ?????);
1534       whd in match (eval_binop ???????); normalize nodelta
1535       cases (value_eq_ptr_inversion … Hvalue_eq) #cm_ptr * #Heq_cm_ptr >Heq_cm_ptr
1536       normalize nodelta #Hptr_translate
1537       %{(Vptr (shift_pointer (bitsize_of_intsize I16) cm_ptr (repr I16 field_off)))}
1538       @conj whd in match (Eapp ??); >(append_nil ? trace) try @refl
1539       %4 whd in Hptr_translate:(??%?) ⊢ (??%?);
1540       cases (E cl_blo) in Hptr_translate; normalize nodelta
1541       [ #H destruct (H) ]
1542       * #BL #OFF normalize nodelta #Heq destruct (Heq)
1543       >Hfield_off' in Hfield_off; normalize in ⊢ ((??%%) → ?);
1544       #H destruct (H)
1545       (* again, mismatch in the size of the integers *)
1546       @cthulhu
1547  | 2: normalize in Hexec_lvalue:(???%); destruct (Hexec_lvalue)
1548       cases (Hind … Hexpr_vars Htranslate_addr ??? Hyp_present Hexec_lvalue_ind)
1549       #cm_val * #Heval_expr >Heval_expr #Hvalue_eq
1550       cases (value_eq_ptr_inversion … Hvalue_eq) #cm_ptr * #Hcm_ptr_eq >Hcm_ptr_eq
1551       #Hpointer_translation
1552       %{cm_val} @conj try assumption
1553       destruct @refl
1554   ]
1555| 14: (* cost label *)
1556  #ty (* cases ty
1557  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
1558  | #structname #fieldspec | #unionname #fieldspec | #id ] *)
1559  #l * #ed #ety
1560  whd in match (typeof ?); whd in match (typeof ?);
1561  #Hind #e' #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec_expr
1562  cases (bind_inversion ????? Htranslate) -Htranslate * #cm_expr
1563  #Hexpr_vars * #Htranslate_ind #Htranslate
1564  cases (bind_inversion ????? Htranslate) -Htranslate * #cm_costexpr #Hexpr_vars_costexpr
1565  * whd in ⊢ ((???%) → ?); #H destruct (H) #Htyp_should_eq
1566  whd in match (typeof ?) in Htyp_should_eq:(??%?);
1567  lapply (typ_should_eq_inversion (typ_of_type ety) (typ_of_type ty) ??? Htyp_should_eq)
1568  #Htyp_eq
1569  lapply Htyp_should_eq -Htyp_should_eq
1570  lapply Htranslate_ind -Htranslate_ind
1571  lapply Hexpr_vars_costexpr -Hexpr_vars_costexpr
1572  lapply Hexec_expr -Hexec_expr lapply Hyp_present -Hyp_present
1573  lapply Hexpr_vars -Hexpr_vars lapply e' -e'
1574  lapply Hind -Hind lapply cm_expr -cm_expr whd in match (typeof ?);
1575  <(Htyp_eq)
1576  #cm_expr #Hind #e' #Hexpr_vars #Hyp_present #Hexec_expr #Hexpr_vars_costexpr
1577  #Htranslate_ind
1578  whd in ⊢ ((??%?) → ?); >typ_eq_refl normalize nodelta
1579  whd in ⊢ ((??%%) → ?); #H destruct (H) whd in match (eval_expr ???????);
1580  cases (bind_inversion ????? Hexec_expr) * #cm_val #cm_trace * #Hexec_expr_ind
1581  whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1582  cases (Hind cm_expr Hexpr_vars Htranslate_ind … Hyp_present Hexec_expr_ind)
1583  #cm_val' * #Heval_expr' #Hvalue_eq
1584  >Heval_expr' normalize nodelta %{cm_val'} @conj try assumption
1585  (* Inconsistency in clight and cminor executable semantics for expressions~:
1586     placement of the label is either before or after current trace.
1587     To be resolved.
1588   *)
1589  @cthulhu
1590| 15: *
1591  [ #sz #i | #var_id | #e1 | #e1 | #op #e1 | #op #e1 #e2 | #cast_ty #e1
1592  | #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
1593  #ty normalize in ⊢ (% → ?);
1594  [ 2,3,12: @False_ind
1595  | *: #_ #e' #Hexpr_vars #Htranslate_addr #cl_blo #cl_off #trace #Hyp_present
1596           normalize #Habsurd destruct (Habsurd) ]
1597] qed.
1598
1599
1600axiom clight_cminor_rel : clight_cminor_inv → Clight_state → Cminor_state → Prop.
1601
1602(* Conjectured simulation results
1603
1604   We split these based on the start state:
1605   
1606   1. ‘normal’ states take some [S n] normal steps and simulates them by [S m]
1607      normal steps in Cminor;
1608   2. call and return steps are simulated by a call/return step plus [m] normal
1609      steps (to copy stack allocated parameters / results); and
1610   3. lone cost label steps are simulates by a lone cost label step
1611   
1612   These should allow us to maintain enough structure to identify the Cminor
1613   subtrace corresponding to a measurable Clight subtrace.
1614 *)
1615
1616definition clight_normal : Clight_state → bool ≝
1617λs. match Clight_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
1618
1619definition cminor_normal : Cminor_state → bool ≝
1620λs. match Cminor_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
1621
1622axiom clight_cminor_normal :
1623  ∀INV:clight_cminor_inv.
1624  ∀s1,s1',s2,tr.
1625  clight_cminor_rel INV s1 s1' →
1626  clight_normal s1 →
1627  ¬ Clight_labelled s1 →
1628  ∃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〉) →
1629  ∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'.
1630    tr = tr' ∧
1631    clight_cminor_rel INV s2 s2'
1632  ).
1633
1634axiom clight_cminor_call_return :
1635  ∀INV:clight_cminor_inv.
1636  ∀s1,s1',s2,tr.
1637  clight_cminor_rel INV s1 s1' →
1638  match Clight_classify s1 with [ cl_call ⇒ true | cl_return ⇒ true | _ ⇒ false ] →
1639  after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
1640  ∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'.
1641    tr = tr' ∧
1642    clight_cminor_rel INV s2 s2'
1643  ).
1644
1645axiom clight_cminor_cost :
1646  ∀INV:clight_cminor_inv.
1647  ∀s1,s1',s2,tr.
1648  clight_cminor_rel INV s1 s1' →
1649  Clight_labelled s1 →
1650  after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
1651  after_n_steps 1 … Cminor_exec (ge_cm INV) s1' (λs.true) (λtr',s2'.
1652    tr = tr' ∧
1653    clight_cminor_rel INV s2 s2'
1654  ).
1655
Note: See TracBrowser for help on using the repository browser.