source: src/Clight/toCminorCorrectness.ma @ 2545

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

Comitting current progress of CL to CM

File size: 45.5 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
473(* TODO convert Clight unary ops to front-end ops ops, then prove correspondence for operators (with equal values). *)
474
475
476lemma eval_expr_sim :
477  ∀(inv:clight_cminor_inv).
478  ∀(f:function).
479  ∀(vars:var_types).
480  ∀stacksize.
481  characterise_vars (globals inv) f = 〈vars, stacksize〉 →
482  ∀(cl_env:cl_env).
483  (∃m,m'. exec_alloc_variables empty_env m (fn_params f @ fn_vars f) = 〈cl_env,m'〉) →
484  ∀(cl_m:mem).
485  ∀(cm_env:cm_env).
486  ∀(sp:block).
487  ∀(cm_m:mem).
488  ∀E:embedding.
489  ∀minj:memory_inj E cl_m cm_m.
490  memory_matching E cl_m cm_m cl_env cm_env inv sp vars →
491  (* clight expr to cminor expr *)
492  (∀(e:expr).
493   ∀(e':CMexpr (typ_of_type (typeof e))).
494   ∀Hexpr_vars.
495   translate_expr vars e = OK ? («e', Hexpr_vars») →
496   ∀cl_val,trace,Hyp_present.
497   exec_expr (ge_cl … inv) cl_env cl_m e = OK ? 〈cl_val, trace〉 →
498   ∃cm_val. eval_expr (ge_cm inv) (typ_of_type (typeof e)) e' cm_env Hyp_present sp cm_m = OK ? 〈trace, cm_val〉 ∧
499            value_eq E cl_val cm_val) ∧
500   (* clight /lvalue/ to cminor /expr/ *)
501  (∀ed,ty.
502   ∀(e':CMexpr ASTptr).
503   ∀Hexpr_vars.
504   translate_addr vars (Expr ed ty) = OK ? («e', Hexpr_vars») →
505   ∀cl_blo,cl_off,trace,Hyp_present.
506   exec_lvalue' (ge_cl … inv) cl_env cl_m ed ty = OK ? 〈cl_blo, cl_off, trace〉 →
507   ∃cm_val. eval_expr (ge_cm inv) ASTptr e' cm_env Hyp_present sp cm_m = OK ? 〈trace, cm_val〉 ∧
508            value_eq E (Vptr (mk_pointer cl_blo cl_off)) cm_val).
509#inv #f #vars #stacksize #Hcharacterise #cl_env #Hexec_alloc #cl_m #cm_env #sp #cm_m #E #Hinj #Hlocal_matching
510@expr_lvalue_ind_combined
511[ 1: (* Integer constant *)
512  #csz #ty cases ty
513  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
514  | #structname #fieldspec | #unionname #fieldspec | #id ]
515  #i whd in match (typeof ?); #e' #Hexpr_vars #Htranslate
516  #val #trace #Hpresent #Hexec_cl
517  whd in Htranslate:(??%?);
518  [ 1,3,4,5,6,7,8: destruct ]
519  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))))
520  [ 2: * #H_err #H_neq_sz
521       lapply (H_err (OK ? «Cst (ASTint csz sg) (Ointconst csz sg i),I») (Error ? (msg TypeMismatch)))
522       >Htranslate #Habsurd destruct (Habsurd) ]
523  * #H_ok #Heq_sz lapply (H_ok (OK ? «Cst (ASTint csz sg) (Ointconst csz sg i),I») (Error ? (msg TypeMismatch)))
524  destruct (Heq_sz)
525  >Htranslate -Htranslate -H_ok #Heq destruct (Heq)
526  whd in Hexec_cl:(??%?); >eq_intsize_true in Hexec_cl; normalize nodelta
527  #Heq destruct (Heq) %{(Vint sz i)} @conj try @refl //
528| 2: *
529  [ #sz #i | #var_id | * #ed1 #ty1 | #e1 | #op #e1 | #op #e1 #e2 | #cast_ty #e1
530  | #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
531  try /2 by I/
532  #ty whd in ⊢ (% → ?); #Hind
533  whd in match (Plvalue ???);
534  whd in match (typeof ?);
535  #cm_expr #Hexpr_vars #Htranslate_expr #val #trace #Hyp_present #Hexec
536  whd in Hexec:(??%?);
537  whd in match (exec_lvalue' ?????) in Hexec:(??%?);
538  cases (bind_inversion ????? Hexec) -Hexec * * #cl_b #cl_o #cl_t * #Hcl_success #Hcl_load_success
539  whd in Hcl_success:(???%);
540  [ 1: (* var case *)
541       lapply Hcl_success -Hcl_success -Hind
542       (* Peform case analysis on presence of variable in local Clight env.
543        * if success, exec_expr/exec_lvalue tells us that it shoud be local. *)
544       @(match lookup SymbolTag block cl_env var_id
545         return λx.(lookup SymbolTag block cl_env var_id = x) → ?
546         with
547         [ None ⇒ λHcl_lookup. ?
548         | Some loc ⇒ λHcl_lookup. ?
549         ] (refl ? (lookup SymbolTag block cl_env var_id)))
550       normalize nodelta
551       [ 1: (* global case *)
552            #Hlookup_global
553            cases (bind_inversion ????? Hlookup_global) -Hlookup_global #global_block
554            * #Hopt lapply (opt_to_res_inversion ???? Hopt) #Hfind_symbol
555            #Heq whd in Heq:(???%); destruct (Heq)
556            lapply (bind2_eq_inversion ?????? Htranslate_expr) -Htranslate_expr
557            * #var_id_alloctype * #var_id_type * #Heq
558            cases (variable_not_in_env_but_in_vartypes_is_global …
559                        Hexec_alloc Hcharacterise Hcl_lookup ?? Heq)
560            #r #Heq' destruct (Heq') normalize nodelta
561            lapply Hcl_load_success -Hcl_load_success
562            lapply Hyp_present -Hyp_present
563            lapply Hexpr_vars -Hexpr_vars
564            lapply cm_expr -cm_expr inversion (access_mode ty)
565            [ #typ_of_ty | | #typ_of_ty ]
566            #Heq_typ_of_type #Heq_access_mode
567            #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_success normalize nodelta
568            whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
569            whd in match (eval_expr ???????);
570            whd in match (eval_expr ???????);
571            whd in match (eval_constant ????);
572            <(eq_sym … inv) >Hfind_symbol normalize nodelta
573            cases (bind_inversion ????? Hcl_load_success) #x *
574            #Hopt_to_res whd in ⊢ (???% → ?); #Heq_val destruct (Heq_val)
575            lapply (opt_to_res_inversion ???? Hopt_to_res)
576            #Hcl_load_success
577            [ 2: %{(Vptr (mk_pointer cl_b (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 O))))}
578                 @conj try @refl
579                 whd in Hcm_load_success:(??%?);
580                 lapply (jmeq_to_eq ??? Heq_typ_of_type) #Heq_ty
581                 >(load_value_of_type_by_ref … Hcl_load_success)
582                 try assumption %4
583                 lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
584                 >Hfind_symbol normalize nodelta #Heq_embedding
585                 whd in match (shift_offset ???);
586                 >addition_n_0 whd in match (pointer_translation ??); >Heq_embedding
587                 normalize nodelta @refl
588            | 1: cut (access_mode ty=By_value (typ_of_type ty))
589                 [ @jmeq_to_eq lapply (jmeq_to_eq ??? Heq_typ_of_type) #Heqt
590                   lapply Heq_access_mode <Heqt // ] #Haccess
591                 lapply (load_by_value_success_valid_pointer … Haccess … Hcl_load_success)
592                 #Hvalid_ptr
593                 lapply (mi_inj … Hinj ?? cl_b zero_offset … Hvalid_ptr … Hcl_load_success)
594                 [ whd in ⊢ (??%?);
595                   lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
596                   >Hfind_symbol normalize nodelta #Heq_embedding >Heq_embedding @refl ]
597                 * #val' * #Hcm_load_success #Hvalue_eq
598                 lapply (load_value_of_type_by_value … Haccess … Hcm_load_success)
599                 #Hloadv lapply (jmeq_to_eq ??? Heq_typ_of_type) #Htypeq <Htypeq >Hloadv
600                 normalize %{val'} @conj try @refl assumption ]
601       | 2: (* local case *)
602            #Heq destruct (Heq)
603            lapply (bind2_eq_inversion ?????? Htranslate_expr) -Htranslate_expr
604            * #var_id_alloc_type * #var_id_type *
605            generalize in match var_id_alloc_type; * normalize nodelta
606            [ 1: #r #Hlookup_vartype
607                 lapply (characterise_vars_lookup_local … Hcharacterise … Hcl_lookup … Hexec_alloc)
608                 * #typ whd in match (local_id ???);
609                 >Hlookup_vartype normalize nodelta @False_ind
610            | 2: (* Stack local *)
611                 lapply Hcl_load_success -Hcl_load_success
612                 lapply Hyp_present -Hyp_present
613                 lapply Hexpr_vars -Hexpr_vars
614                 lapply cm_expr -cm_expr inversion (access_mode ty)
615                 [ #typ_of_ty | | #typ_of_ty ]
616                 #Heq_typ_of_type #Heq_access_mode
617                 #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_success
618                 #stack_depth #Hlookup_vartype_success normalize nodelta
619                 whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
620                 lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
621                 cases (res_inversion ?????? Hlookup_vartype_success) -Hlookup_vartype_success
622                 * #var_id_alloc_type' #var_id_type' * #Hlookup' #Heq destruct (Heq)
623                 >Hlookup' normalize nodelta #Hembedding_eq
624                 cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success
625                 #loaded_val * #Hload_val
626                 whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
627                 lapply (opt_to_res_inversion ???? Hload_val) -Hload_val
628                 #Hload_success whd in match (eval_expr ???????);
629                 cut (pointer_translation (mk_pointer cl_b zero_offset) E =
630                      Some ? (mk_pointer sp (mk_offset (repr I16 stack_depth))))
631                 [ 1,3: whd in ⊢ (??%?); >Hembedding_eq normalize nodelta
632                        >offset_plus_0 @refl ]
633                 #Hpointer_translation
634                 [ 2: (* By-ref *)
635                      whd in Hload_success:(??%?);
636                      lapply (load_value_of_type_by_ref … Hload_success … Heq_typ_of_type Heq_access_mode)
637                      #Heq_val
638                      >Heq_val
639                      %{(Vptr (mk_pointer sp (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 stack_depth))))}
640                      @conj try @refl
641                      %4 whd in match (shift_offset ???);
642                      whd in match zero_offset;
643                      >commutative_addition_n >addition_n_0 @Hpointer_translation
644                 | 1: (* By value *)
645                      lapply (jmeq_to_eq ??? Heq_typ_of_type) #Heq0                       
646                      lapply (mi_inj … Hinj … Hpointer_translation … Hload_success)
647                      [ @(load_by_value_success_valid_pointer … Hload_success)
648                        lapply Heq_access_mode <Heq0 /2 by jmeq_to_eq/ ]
649                      * #cm_val * #Hload_in_cm #Hvalue_eq
650                      %{cm_val} @conj try assumption
651                      lapply (load_value_of_type_by_value … Hload_in_cm)
652                      [ lapply Heq_access_mode <Heq0 #Heq1
653                        @(jmeq_to_eq ??? Heq1) ]
654                      #Hloadv <Heq0
655                      whd in match (shift_offset ???); >commutative_addition_n >addition_n_0
656                      >Hloadv @refl ]
657            | 3: (* Register local variable *)
658                 #Hlookup_eq
659                 lapply (res_inversion ?????? Hlookup_eq)
660                 * * #var_id_alloc_type' #var_id_type' * #Hlookup' #Heq destruct (Heq)
661                 #Htype_eq
662                 cases (type_should_eq_inversion
663                            var_id_type
664                            ty
665                            (λt0:type.Σe':expr (typ_of_type t0).expr_vars (typ_of_type t0) e' (local_id vars))
666                            … Htype_eq) -Htype_eq
667                 (* Reverting all premises in order to perform type rewrite *)
668                 #Htype_eq
669                 lapply Hlookup' -Hlookup' lapply Hlookup_eq -Hlookup_eq
670                 lapply Hcl_load_success -Hcl_load_success
671                 lapply Hcl_lookup -Hcl_lookup
672                 lapply Hyp_present -Hyp_present
673                 lapply Hexpr_vars -Hexpr_vars
674                 lapply cm_expr
675                 destruct (Htype_eq)
676                 #cm_expr #Hexpr_vars #Hyp_present #Hcl_lookup #Hcl_load_success #Hlookup_eq #Hlookup'
677                 #Hexpr_eq lapply (jmeq_to_eq ??? Hexpr_eq) -Hexpr_eq #Hexpr_eq
678                 destruct (Hexpr_eq)
679                 whd in match (eval_expr ???????);
680                 whd in match (lookup_present ?????);
681                 lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
682                 >Hlookup' normalize nodelta #Hmatching
683                 cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success
684                 #loaded_val * #Hload_val
685                 whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
686                 lapply (opt_to_res_inversion ???? Hload_val) -Hload_val
687                 #Hload_success
688                 cases (Hmatching … Hload_success) #val'
689                 * #Hlookup_in_cm #Hvalue_eq %{val'}
690                 cases Hyp_present
691                 >Hlookup_in_cm normalize nodelta #_ @conj try @refl try assumption
692                 (* seems ok *)
693            ]
694       ]
695  | 2: lapply Hcl_success -Hcl_success
696       lapply Htranslate_expr -Htranslate_expr
697       lapply Hind -Hind cases ty1
698       [ | #sz1 #sg1 | #ptr_ty1 | #array_ty1 #array_sz1 | #domain1 #codomain1
699       | #structname1 #fieldspec1 | #unionname1 #fieldspec1 | #id1 ]
700       #Hind #Htranslate_expr #Hexec_cl
701       cases (bind_inversion ????? Htranslate_expr) -Htranslate_expr
702       * whd in match (typ_of_type ?); normalize nodelta
703       #cm_expr_ind #Hexpr_vars_ind * #Htranslate_expr_ind
704       whd in ⊢ ((???%) → ?);
705       [ 1,2,6,7: #Heq destruct (Heq) ]
706       lapply (Hind cm_expr_ind Hexpr_vars_ind) -Hind
707       whd in match (translate_addr ??); >Htranslate_expr_ind normalize nodelta
708       #Hind lapply (Hind (refl ??) cl_b cl_o cl_t ?) -Hind
709       [ 1,3,5,7: @cthulhu ]
710       whd in match (exec_lvalue' ?????); >Hexec_cl normalize nodelta
711       cases (bind_inversion ????? Hexec_cl) * #cl_ptr #cl_trace0 *
712       #Hexec_cl_ind #Hcl_ptr
713       cut (∃ptr. cl_ptr = Vptr ptr)
714       [ 1,3,5,7: cases cl_ptr in Hcl_ptr; normalize
715                  #H1 destruct #H2 destruct try /2 by ex_intro, refl/ #H3 destruct ]
716       * * #cl_ptr_block #cl_ptr_off -Hcl_ptr
717       #Hcl_ptr destruct (Hcl_ptr) normalize nodelta -Hexec_cl
718       #Hind lapply (Hind (refl ??)) -Hind
719       * #cm_ptr * #Hexec_cm_ind #Hvalue_eq_ind
720       lapply (value_eq_ptr_inversion … Hvalue_eq_ind) * * #cm_ptr_block #cm_ptr_off * #Hcm_ptr
721       destruct (Hcm_ptr) #Hpointer_translation
722       cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success #cl_val * #Hopt_to_res
723       whd in ⊢ ((???%) → ?); #Heq destruct (Heq) lapply (opt_to_res_inversion ???? Hopt_to_res)
724       -Hopt_to_res
725       lapply Hyp_present -Hyp_present
726       lapply Hexpr_vars -Hexpr_vars
727       lapply cm_expr -cm_expr
728       inversion (access_mode ty)
729       [ 1,3,4,6,7,9,10,12: #t ] #Htyp_of_type #Haccess_mode
730       lapply (jmeq_to_eq ??? Htyp_of_type) #Htyp destruct (Htyp)
731       #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_success normalize nodelta
732       #Heq destruct (Heq)
733       [ 1,2,3,4: (* By_value *)
734           (* project Hcl_load_success in Cminor through memory_inj *)
735           lapply (mi_inj ??? Hinj cl_b cl_o cm_ptr_block cm_ptr_off … Hpointer_translation … Hcl_load_success)
736           [ 1,3,5,7: @(load_by_value_success_valid_pointer … Hcl_load_success) @jmeq_to_eq assumption ]
737           * #cm_val * #Hcm_load_success #Hvalue_eq
738           lapply (load_value_of_type_by_value … (jmeq_to_eq ??? Haccess_mode) … Hcm_load_success)
739           #Hloadv_cm
740           whd in match (eval_expr ???????); >Hexec_cm_ind normalize nodelta
741           >Hloadv_cm normalize %{cm_val} @conj try @refl assumption
742      | *: (* By reference *)
743           >Hexec_cm_ind %{(Vptr (mk_pointer cm_ptr_block cm_ptr_off))} @conj try @refl
744           lapply (load_value_of_type_by_ref … Hcl_load_success Htyp_of_type Haccess_mode)
745           #Hval >Hval %4 assumption ]
746  | 3: lapply Hcl_load_success -Hcl_load_success lapply Hcl_success -Hcl_success
747       lapply (refl ? (typeof e1))
748       cases (typeof e1) in ⊢ ((???%) → %);
749       [ | #sz1 #sg1 | #ptr_ty1 | #array_ty1 #array_sz1 | #domain1 #codomain1
750       | #structname1 #fieldspec1 | #unionname1 #fieldspec1 | #id1 ] normalize nodelta
751       #Heq_typeof normalize nodelta
752       [ 1,2,3,4,5,8: #Habsurd destruct ] #Hexec_cl #Hcl_load_success
753       whd in Htranslate_expr:(??%?); >Heq_typeof in Htranslate_expr;
754       normalize nodelta #Htranslate_expr
755       cases (bind_inversion ????? Htranslate_expr) -Htranslate_expr
756       * whd in match (typ_of_type ?); normalize nodelta
757       #cm_expr_ind #Hexpr_vars_ind * #Htranslate_expr_ind #Htranslate_expr2
758       [ cases (bind_inversion ????? Htranslate_expr2) -Htranslate_expr2
759         #cm_field_off * #Hcm_field_off
760       | lapply Htranslate_expr2 -Htranslate_expr2 ]
761       cases (bind_inversion ????? Hexec_cl) -Hexec_cl
762       * * #block_cl #offset_cl #trace0 * #Hexec_lvalue #Hexec_cl
763       whd in Hexec_lvalue:(???%);
764       [ cases (bind_inversion ????? Hexec_cl) -Hexec_cl
765         #cl_field_off * #Hcl_field_off #Hoffset_eq ]
766       cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success
767       #cl_val * #Hopt_cl_val whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
768       lapply (opt_to_res_inversion ???? Hopt_cl_val) -Hopt_cl_val #Hcl_load_value
769       [  (* Struct case *)
770         lapply Hcl_load_value -Hcl_load_value
771         lapply Hyp_present -Hyp_present
772         lapply Hexpr_vars -Hexpr_vars
773         lapply cm_expr -cm_expr
774         lapply Hind -Hind
775         cases ty
776         [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
777         | #structname #fieldspec | #unionname #fieldspec | #id ]
778         #Hind #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_value
779         normalize nodelta
780         whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
781         whd in match (eval_expr ???????);
782         (* applying the arguments of the induction hypothesis progressively *)
783         lapply (Hind (Op2 ASTptr (ASTint I16 Signed) ASTptr (Oaddp I16) cm_expr_ind
784                          (Cst (ASTint I16 Signed) (Ointconst I16 Signed (repr I16 cm_field_off)))) ?)
785         [ 1,3,5,7,9: whd @conj try assumption whd @I ] -Hind #Hind
786         lapply (Hind ?)
787         [ 1,3,5,7,9:
788            whd in ⊢ (??%?); >Heq_typeof normalize nodelta
789            >Htranslate_expr_ind whd in match (m_bind ?????);
790            >Hcm_field_off normalize nodelta @refl ] -Hind #Hind
791         whd in Hoffset_eq:(???%); destruct (offset_eq)
792         cut (cl_field_off = cm_field_off)
793         [ 1,3,5,7,9: lapply Hcl_field_off >Hcm_field_off
794           normalize #Heq destruct (Heq) @refl ]
795         #Heq destruct (Heq)
796         lapply (Hind cl_b cl_o trace ?)
797         [ 1,3,5,7,9: @Hyp_present ] -Hind #Hind
798         lapply (Hind ?) -Hind
799         [ 1,3,5,7,9: whd in ⊢ (??%?); >Heq_typeof normalize nodelta
800           >Hexec_lvalue whd in match (m_bind ?????); >Hcm_field_off normalize nodelta
801           @Hoffset_eq ]
802         * #cm_val' * #Heval_expr #Hvalue_eq
803         lapply (value_eq_ptr_inversion … Hvalue_eq) * * #cm_ptr_block #cm_ptr_off
804         * #Heq_cm_val_ptr destruct (Heq_cm_val_ptr) #Hpointer_trans
805         [ 1,2,5: (* by-value *)
806            lapply (mi_inj … Hinj cl_b cl_o ?? … Hpointer_trans … Hcl_load_value)
807            [ 1,3,5: @(load_by_value_success_valid_pointer … Hcl_load_value) // ]
808            * #cm_val * #Hcm_load_value #Hvalue_eq
809            lapply (load_value_of_type_by_value … Hcm_load_value)
810            [ 1,3,5: @refl ]
811            #Hcm_loadv %{cm_val} >Heval_expr normalize nodelta >Hcm_loadv normalize @conj
812            try @refl try assumption
813         | 3,4: (* by-ref *)
814            whd in match (eval_expr ???????) in Heval_expr; >Heval_expr
815            %{(Vptr (mk_pointer cm_ptr_block cm_ptr_off))} @conj try @refl
816            whd in Hcl_load_value:(??%?); destruct (Hcl_load_value) assumption
817         ]
818      | (* union case *)
819         lapply Hcl_load_value -Hcl_load_value
820         lapply Hyp_present -Hyp_present
821         lapply Hexpr_vars -Hexpr_vars
822         lapply cm_expr -cm_expr
823         lapply Hind -Hind
824         cases ty
825         [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
826         | #structname #fieldspec | #unionname #fieldspec | #id ]
827         whd in match (typ_of_type ?); normalize nodelta
828         #Hind #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_value
829         whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
830         [ 1,2,5: (* by-value *)
831            whd in match (eval_expr ???????);
832            lapply (Hind cm_expr_ind Hexpr_vars ?)
833            [ 1,3,5: whd in ⊢ (??%?); >Heq_typeof normalize nodelta @Htranslate_expr_ind ]
834            whd in match (exec_lvalue' ?????); >Heq_typeof normalize nodelta
835            -Hind #Hind
836            lapply (Hind block_cl offset_cl trace0 Hyp_present) -Hind >Hexec_lvalue normalize nodelta
837            whd in match (m_bind ?????); #Hind
838            cases (Hind (refl ??)) -Hind
839            #cm_val * #Heval_expr #Hvalue_eq >Heval_expr normalize nodelta
840            cases (value_eq_ptr_inversion … Hvalue_eq) * #cm_block #cm_offset * #Hcm_val #Hpointer_trans
841            destruct (Hcm_val) whd in Hexec_cl:(???%); destruct (Hexec_cl)
842            lapply (mi_inj … Hinj cl_b cl_o cm_block cm_offset … Hpointer_trans … Hcl_load_value)
843            [ 1,3,5: @(load_by_value_success_valid_pointer … Hcl_load_value) // ]
844            * #cm_val * #Hcm_load_value #Hvalue_eq           
845            lapply (load_value_of_type_by_value … Hcm_load_value)
846            [ 1,3,5: @refl ]
847            #Hcm_loadv %{cm_val} >Hcm_loadv normalize @conj
848            try @refl assumption
849         | 3,4:
850            whd in Hexec_cl:(???%); destruct (Hexec_cl)
851            lapply (Hind cm_expr Hexpr_vars)
852            whd in match (translate_addr ??); >Heq_typeof normalize nodelta -Hind #Hind
853            lapply (Hind Htranslate_expr_ind) -Hind
854            whd in match (exec_lvalue' ?????); >Heq_typeof normalize nodelta
855            >Hexec_lvalue whd in match (m_bind ?????);
856            #Hind cases (Hind … Hyp_present (refl ??))
857            #cm_val * #Heval_expr #Hvalue_eq >Heval_expr %{cm_val} @conj
858            try @refl whd in Hcl_load_value:(??%?); destruct (Hcl_load_value)
859            assumption ]
860    ]
861  ]
862| 3: #var #ty #cmexpr #Hexpr_vars #Htranslate_var #cl_blo #cl_off #trace #Hyp_present #Hexec_lvalue_var
863     whd in Hexec_lvalue_var:(??%?);
864     (* check whether var is local or global *)
865     lapply (Hlocal_matching var)
866     lapply (variable_not_in_env_but_in_vartypes_is_global  … var Hexec_alloc … Hcharacterise)
867     cases (lookup ?? cl_env var) in Hexec_lvalue_var;
868     normalize nodelta
869     [ 1: (* global *)
870          #Hexec_opt #H lapply (H (refl ??)) -H #Hvar_is_global
871          cases (bind_inversion ????? Hexec_opt) -Hexec_opt #varblock * #Hopt_to_res #Heq
872          whd in Heq:(???%) Hopt_to_res:(???%); destruct (Heq)
873          lapply (opt_to_res_inversion ???? Hopt_to_res) -Hopt_to_res #Hfind_symbol >Hfind_symbol normalize nodelta
874          #Hembed
875          cases (bind_inversion ????? Htranslate_var) -Htranslate_var
876          * #var_alloctype #var_type * #Hlookup_vartype #Hvar_alloctype
877          cases (Hvar_is_global … Hlookup_vartype) #r #Halloctype >Halloctype in Hvar_alloctype;
878          normalize nodelta whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
879          whd in match (eval_expr ???????);
880          whd in match (eval_constant ????);
881          <(eq_sym inv var) >Hfind_symbol normalize nodelta
882          %{(Vptr (mk_pointer cl_blo (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 O))))}
883          @conj try @refl %4 whd in match (pointer_translation ??);
884          >Hembed normalize nodelta whd in match (shift_offset ???);
885          >addition_n_0 @refl
886     | 2: (* local *)
887          #BL #Heq destruct (Heq) #_
888          @(match (lookup ?? vars var)
889            return λx. (lookup ?? vars var = x) → ?
890            with
891            [ None ⇒ ?
892            | Some kind ⇒ ?
893            ] (refl ??))
894          normalize nodelta
895          #Hlookup [ @False_ind ]
896          cases kind in Hlookup; #var_alloctype #var_type normalize nodelta
897          #Hlookup
898          lapply (refl ? var_alloctype)
899          cases var_alloctype in ⊢ ((???%) → %); normalize nodelta
900          [ #reg #Heq @False_ind | #stacksize #Hvar_alloc #Hembed | #Hvar_alloc #Hlookup' ]
901          [ (* stack alloc*)
902            cases (bind_inversion ????? Htranslate_var) -Htranslate_var
903            * #var_alloctype' #var_type' * #Hlookup_vartype'           
904            whd in Hlookup_vartype':(??%?); >Hlookup in Hlookup_vartype'; normalize nodelta
905            whd in ⊢ ((???%) → ?); #Heq destruct (Heq) >Hvar_alloc normalize nodelta
906            whd in ⊢ ((???%) → ?); #Heq destruct (Heq) whd in match (eval_expr ???????);
907            %{(Vptr (mk_pointer sp (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 stacksize))))}
908            @conj try @refl %4 whd in match (pointer_translation ??);
909            >Hembed @refl
910          | (* local alloc *)
911            cases (bind_inversion ????? Htranslate_var) -Htranslate_var
912            * #var_alloctype' #var_type' * #Hlookup_vartype'
913            whd in Hlookup_vartype':(??%?); >Hlookup in Hlookup_vartype'; normalize nodelta
914            whd in ⊢ ((???%) → ?); #Heq destruct (Heq) >Hvar_alloc normalize nodelta
915            whd in ⊢ ((???%) → ?); #Heq destruct (Heq) ] ]
916(*| 4: #e #ty*)
917| 4:
918  * #ed #ety cases ety
919  [ | #sz1 #sg1 | #ptr_ty1 | #array_ty1 #array_sz1 | #domain1 #codomain1
920  | #structname1 #fieldspec1 | #unionname1 #fieldspec1 | #id1 ] normalize nodelta 
921  whd in match (typeof ?);
922  #ty #Hind #e' #Hexpr_vars #Htranslate #cl_blo #cl_off #trace #Hyp_present #Hexec_lvalue
923  cases (bind_inversion ????? Htranslate) -Htranslate   
924  * #cm_expr #Hexpr_vars_cm * #Htranslate_ind
925  cases (bind_inversion ????? Hexec_lvalue) -Hexec_lvalue
926  * #cl_val #trace0 * #Hexec_expr #Hcl_val
927  whd in match (typeof ?); whd in match (typ_of_type ?); normalize nodelta
928  whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
929  cut (cl_val = Vptr (mk_pointer cl_blo cl_off) ∧ trace = trace0)
930  [ 1,3,5,7: cases cl_val in Hcl_val; normalize
931    [ 1,5,9,13: #Heq destruct (Heq)
932    | 2,6,10,14: #sz #vec #Heq destruct (Heq)
933    | 3,7,11,15: #Heq destruct (Heq)
934    | 4,8,12,16: * #BL #OFF #Heq destruct (Heq) @conj try @refl ] ]
935  * #Heq_cl_val destruct (Heq_cl_val) #Htrace_eq destruct (Htrace_eq)
936  cases (Hind e' Hexpr_vars Htranslate_ind … Hyp_present … Hexec_expr)
937  #cm_val * #Heval_expr_cm #Hvalue_eq >Heval_expr_cm
938  %{cm_val} @conj try @refl try assumption
939| 5:
940  #ty cases ty
941  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
942  | #structname #fieldspec | #unionname #fieldspec | #id ]
943  #ed #ty' #Hind
944  whd in match (typeof ?); whd in match (typ_of_type ?); #cm_expr
945  #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec_expr
946  cases (bind_inversion ????? Htranslate) -Htranslate
947  * #cm_expr #Hexpr_vars_cm * #Htranslate_ind
948  cases (bind_inversion ????? Hexec_expr) -Hexec_expr
949  * * #cl_blo #cl_off #trace0 * #Hexec_lvalue normalize nodelta
950  whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
951  whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
952  cases (Hind cm_expr Hexpr_vars Htranslate_ind ??? Hyp_present Hexec_lvalue)
953  #cm_val * #Hexec_cm #Hvalue_eq >Hexec_cm
954  %{cm_val} @conj try @refl assumption
955| 6:
956  #ty cases ty
957  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
958  | #structname #fieldspec | #unionname #fieldspec | #id ]
959  whd in match (typeof ?);
960  #op #e #Hind
961  whd in match (typeof ?); whd in match (typ_of_type ?); 
962  #e' #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec
963  cases (bind_inversion ????? Htranslate) -Htranslate
964  #op * #Htranslate_unop #Hexec_arg
965  cases (bind_inversion ????? Hexec_arg) -Hexec_arg
966  * #cm_arg #Hexpr_vars_arg * #Htranslate whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
967  cases (bind_inversion ????? Hexec) -Hexec
968  * #cl_val #cl_trace * #Hexec_cl
969  whd in ⊢ ((???%) → ?); #Hexec_unop
970  cases (bind_inversion ????? Hexec_unop) -Hexec_unop
971  #v * #Hopt whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
972  lapply (opt_to_res_inversion ???? Hopt) -Hopt
973  #Hsem_cl whd in match (eval_expr ???????);
974  cases (Hind cm_arg Hexpr_vars Htranslate … Hyp_present Hexec_cl)
975  #cm_val * #Heval_cm #Hvalue_eq >Heval_cm normalize nodelta
976  lapply (unary_operation_value_eq … Hvalue_eq … Hsem_cl)
977  @cthulhu
978| *: @cthulhu
979] qed.
980
981
982
983
984
985axiom clight_cminor_rel : clight_cminor_inv → Clight_state → Cminor_state → Prop.
986
987(* Conjectured simulation results
988
989   We split these based on the start state:
990   
991   1. ‘normal’ states take some [S n] normal steps and simulates them by [S m]
992      normal steps in Cminor;
993   2. call and return steps are simulated by a call/return step plus [m] normal
994      steps (to copy stack allocated parameters / results); and
995   3. lone cost label steps are simulates by a lone cost label step
996   
997   These should allow us to maintain enough structure to identify the Cminor
998   subtrace corresponding to a measurable Clight subtrace.
999 *)
1000
1001definition clight_normal : Clight_state → bool ≝
1002λs. match Clight_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
1003
1004definition cminor_normal : Cminor_state → bool ≝
1005λs. match Cminor_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
1006
1007axiom clight_cminor_normal :
1008  ∀INV:clight_cminor_inv.
1009  ∀s1,s1',s2,tr.
1010  clight_cminor_rel INV s1 s1' →
1011  clight_normal s1 →
1012  ¬ Clight_labelled s1 →
1013  ∃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〉) →
1014  ∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'.
1015    tr = tr' ∧
1016    clight_cminor_rel INV s2 s2'
1017  ).
1018
1019axiom clight_cminor_call_return :
1020  ∀INV:clight_cminor_inv.
1021  ∀s1,s1',s2,tr.
1022  clight_cminor_rel INV s1 s1' →
1023  match Clight_classify s1 with [ cl_call ⇒ true | cl_return ⇒ true | _ ⇒ false ] →
1024  after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
1025  ∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'.
1026    tr = tr' ∧
1027    clight_cminor_rel INV s2 s2'
1028  ).
1029
1030axiom clight_cminor_cost :
1031  ∀INV:clight_cminor_inv.
1032  ∀s1,s1',s2,tr.
1033  clight_cminor_rel INV s1 s1' →
1034  Clight_labelled s1 →
1035  after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
1036  after_n_steps 1 … Cminor_exec (ge_cm INV) s1' (λs.true) (λtr',s2'.
1037    tr = tr' ∧
1038    clight_cminor_rel INV s2 s2'
1039  ).
1040
Note: See TracBrowser for help on using the repository browser.