source: src/Clight/toCminorCorrectness.ma @ 2527

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

Progress on CL to CM.

File size: 40.2 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,allocty,ty.
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  lookup' vars var_id = OK ? 〈allocty, ty〉 →
429  ∃r.allocty = Global r.
430#env #env' #f #vars #stacksize #globals #var_id #allocty #ty #Hexec_alloc
431#Hcharacterise #Hlookup_fail #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
474lemma eval_expr_sim :
475  ∀(inv:clight_cminor_inv).
476  ∀(f:function).
477  ∀(vars:var_types).
478  ∀stacksize.
479  characterise_vars (globals inv) f = 〈vars, stacksize〉 →
480  ∀(cl_env:cl_env).
481  (∃m,m'. exec_alloc_variables empty_env m (fn_params f @ fn_vars f) = 〈cl_env,m'〉) →
482  ∀(cl_m:mem).
483  ∀(cm_env:cm_env).
484  ∀(sp:block).
485  ∀(cm_m:mem).
486  ∀E:embedding.
487  ∀minj:memory_inj E cl_m cm_m.
488  memory_matching E cl_m cm_m cl_env cm_env inv sp vars →
489  (∀(e:expr).
490   ∀(e':CMexpr (typ_of_type (typeof e))).
491   ∀Hexpr_vars.
492   translate_expr vars e = OK ? («e', Hexpr_vars») →
493   ∀cl_val,trace,Hyp_present.
494   exec_expr (ge_cl … inv) cl_env cl_m e = OK ? 〈cl_val, trace〉 →
495   ∃cm_val. eval_expr (ge_cm inv) (typ_of_type (typeof e)) e' cm_env Hyp_present sp cm_m = OK ? 〈trace, cm_val〉 ∧
496            value_eq E cl_val cm_val) ∧
497  (∀ed,ty.
498   ∀(e':CMexpr (typ_of_type ty)).
499   ∀Hexpr_vars.
500   translate_expr vars (Expr ed ty) = OK ? («e', Hexpr_vars») →
501   ∀cl_blo,cl_off,trace,Hyp_present.
502   exec_lvalue' (ge_cl … inv) cl_env cl_m ed ty = OK ? 〈cl_blo, cl_off, trace〉 →
503   match E cl_blo with
504   [ Some loc ⇒
505     let 〈cm_blo, delta〉 ≝ loc in
506     match access_mode ty with
507     [ By_value t ⇒
508        (∃cm_val. loadv t cm_m (Vptr (mk_pointer cm_blo (offset_plus cl_off delta))) = Some ? cm_val ∧
509                  eval_expr (ge_cm inv) (typ_of_type ty) e' cm_env Hyp_present sp cm_m = OK ? 〈trace, cm_val〉)
510     | By_reference ⇒
511        eval_expr (ge_cm inv) (typ_of_type ty) e' cm_env Hyp_present sp cm_m
512          = OK ? 〈trace, Vptr (mk_pointer cm_blo (offset_plus cl_off delta))〉             
513     | By_nothing _ ⇒ True ]
514   | None ⇒ False ]).
515#inv #f #vars #stacksize #Hcharacterise #cl_env #Hexec_alloc #cl_m #cm_env
516#sp #cm_m #E #Hinj #Hlocal_matching
517@expr_lvalue_ind_combined
518[ 1: (* Integer constant *)
519  #csz #ty cases ty
520  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
521  | #structname #fieldspec | #unionname #fieldspec | #id ] 
522  #i whd in match (typeof ?); #e' #Hexpr_vars #Htranslate
523  #val #trace #Hpresent #Hexec_cl
524  whd in Htranslate:(??%?);
525  [ 1,3,4,5,6,7,8: destruct ]
526  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))))
527  [ 2: * #H_err #H_neq_sz
528       lapply (H_err (OK ? «Cst (ASTint csz sg) (Ointconst csz sg i),I») (Error ? (msg TypeMismatch)))
529       >Htranslate #Habsurd destruct (Habsurd) ]
530  * #H_ok #Heq_sz lapply (H_ok (OK ? «Cst (ASTint csz sg) (Ointconst csz sg i),I») (Error ? (msg TypeMismatch)))
531  destruct (Heq_sz)
532  >Htranslate -Htranslate -H_ok #Heq destruct (Heq)
533  whd in Hexec_cl:(??%?); >eq_intsize_true in Hexec_cl; normalize nodelta
534  #Heq destruct (Heq) %{(Vint sz i)} @conj try @refl //
535| 2: *
536  [ #sz #i | #var_id | * #ed1 #ty1 | #e1 | #op #e1 | #op #e1 #e2 | #cast_ty #e1
537  | #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
538  try /2 by I/
539  #ty whd in ⊢ (% → ?); #Hind
540  whd in match (Plvalue ???);
541  whd in match (typeof ?);
542  #cm_expr #Hexpr_vars #Htranslate_expr #val #trace #Hyp_present #Hexec
543  whd in Hexec:(??%?);
544  whd in match (exec_lvalue' ?????) in Hexec:(??%?);
545  cases (bind_inversion ????? Hexec) -Hexec * * #cl_b #cl_o #cl_t * #Hcl_success #Hcl_load_success
546  whd in Hcl_success:(???%);
547  [ 1: (* var case *)
548       lapply Hcl_success -Hcl_success -Hind
549       (* Peform case analysis on presence of variable in local Clight env.
550        * if success, exec_expr/exec_lvalue tells us that it shoud be local. *)
551       @(match lookup SymbolTag block cl_env var_id
552         return λx.(lookup SymbolTag block cl_env var_id = x) → ?
553         with
554         [ None ⇒ λHcl_lookup. ?
555         | Some loc ⇒ λHcl_lookup. ?
556         ] (refl ? (lookup SymbolTag block cl_env var_id)))
557       normalize nodelta
558       [ 1: (* global case *)
559            #Hlookup_global
560            cases (bind_inversion ????? Hlookup_global) -Hlookup_global #global_block
561            * #Hopt lapply (opt_to_res_inversion ???? Hopt) #Hfind_symbol
562            #Heq whd in Heq:(???%); destruct (Heq)
563            lapply (bind2_eq_inversion ?????? Htranslate_expr) -Htranslate_expr
564            * #var_id_alloctype * #var_id_type * #Heq
565            cases (variable_not_in_env_but_in_vartypes_is_global …
566                        Hexec_alloc Hcharacterise Hcl_lookup Heq)
567            #r #Heq' destruct (Heq') normalize nodelta
568            lapply Hcl_load_success -Hcl_load_success
569            lapply Hyp_present -Hyp_present
570            lapply Hexpr_vars -Hexpr_vars
571            lapply cm_expr -cm_expr inversion (access_mode ty)
572            [ #typ_of_ty | | #typ_of_ty ]
573            #Heq_typ_of_type #Heq_access_mode
574            #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_success normalize nodelta
575            whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
576            whd in match (eval_expr ???????);
577            whd in match (eval_expr ???????);
578            whd in match (eval_constant ????);
579            <(eq_sym … inv) >Hfind_symbol normalize nodelta
580            cases (bind_inversion ????? Hcl_load_success) #x *
581            #Hopt_to_res whd in ⊢ (???% → ?); #Heq_val destruct (Heq_val)
582            lapply (opt_to_res_inversion ???? Hopt_to_res)
583            #Hcl_load_success
584            [ 2: %{(Vptr (mk_pointer cl_b (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 O))))}
585                 @conj try @refl
586                 whd in Hcm_load_success:(??%?);
587                 lapply (jmeq_to_eq ??? Heq_typ_of_type) #Heq_ty
588                 >(load_value_of_type_by_ref … Hcl_load_success)
589                 try assumption %4
590                 lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
591                 >Hfind_symbol normalize nodelta #Heq_embedding
592                 whd in match (shift_offset ???);
593                 >addition_n_0 whd in match (pointer_translation ??); >Heq_embedding
594                 normalize nodelta @refl
595            | 1: cut (access_mode ty=By_value (typ_of_type ty))
596                 [ @jmeq_to_eq lapply (jmeq_to_eq ??? Heq_typ_of_type) #Heqt
597                   lapply Heq_access_mode <Heqt // ] #Haccess
598                 lapply (load_by_value_success_valid_pointer … Haccess … Hcl_load_success)
599                 #Hvalid_ptr
600                 lapply (mi_inj … Hinj ?? cl_b zero_offset … Hvalid_ptr … Hcl_load_success)
601                 [ whd in ⊢ (??%?);
602                   lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
603                   >Hfind_symbol normalize nodelta #Heq_embedding >Heq_embedding @refl ]
604                 * #val' * #Hcm_load_success #Hvalue_eq
605                 lapply (load_value_of_type_by_value … Haccess … Hcm_load_success)
606                 #Hloadv lapply (jmeq_to_eq ??? Heq_typ_of_type) #Htypeq <Htypeq >Hloadv
607                 normalize %{val'} @conj try @refl assumption ]
608       | 2: (* local case *)
609            #Heq destruct (Heq)
610            lapply (bind2_eq_inversion ?????? Htranslate_expr) -Htranslate_expr
611            * #var_id_alloc_type * #var_id_type *
612            generalize in match var_id_alloc_type; * normalize nodelta
613            [ 1: #r #Hlookup_vartype
614                 lapply (characterise_vars_lookup_local … Hcharacterise … Hcl_lookup … Hexec_alloc)
615                 * #typ whd in match (local_id ???);
616                 >Hlookup_vartype normalize nodelta @False_ind
617            | 2: (* Stack local *)
618                 lapply Hcl_load_success -Hcl_load_success
619                 lapply Hyp_present -Hyp_present
620                 lapply Hexpr_vars -Hexpr_vars
621                 lapply cm_expr -cm_expr inversion (access_mode ty)
622                 [ #typ_of_ty | | #typ_of_ty ]
623                 #Heq_typ_of_type #Heq_access_mode
624                 #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_success
625                 #stack_depth #Hlookup_vartype_success normalize nodelta
626                 whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
627                 lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
628                 cases (res_inversion ?????? Hlookup_vartype_success) -Hlookup_vartype_success
629                 * #var_id_alloc_type' #var_id_type' * #Hlookup' #Heq destruct (Heq)
630                 >Hlookup' normalize nodelta #Hembedding_eq
631                 cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success
632                 #loaded_val * #Hload_val
633                 whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
634                 lapply (opt_to_res_inversion ???? Hload_val) -Hload_val
635                 #Hload_success whd in match (eval_expr ???????);
636                 cut (pointer_translation (mk_pointer cl_b zero_offset) E =
637                      Some ? (mk_pointer sp (mk_offset (repr I16 stack_depth))))
638                 [ 1,3: whd in ⊢ (??%?); >Hembedding_eq normalize nodelta
639                        >offset_plus_0 @refl ]
640                 #Hpointer_translation
641                 [ 2: (* By-ref *)
642                      whd in Hload_success:(??%?);
643                      lapply (load_value_of_type_by_ref … Hload_success … Heq_typ_of_type Heq_access_mode)
644                      #Heq_val
645                      >Heq_val
646                      %{(Vptr (mk_pointer sp (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 stack_depth))))}
647                      @conj try @refl
648                      %4 whd in match (shift_offset ???);
649                      whd in match zero_offset;
650                      >commutative_addition_n >addition_n_0 @Hpointer_translation
651                 | 1: (* By value *)
652                      lapply (jmeq_to_eq ??? Heq_typ_of_type) #Heq0                       
653                      lapply (mi_inj … Hinj … Hpointer_translation … Hload_success)
654                      [ @(load_by_value_success_valid_pointer … Hload_success)
655                        lapply Heq_access_mode <Heq0 /2 by jmeq_to_eq/ ]
656                      * #cm_val * #Hload_in_cm #Hvalue_eq
657                      %{cm_val} @conj try assumption
658                      lapply (load_value_of_type_by_value … Hload_in_cm)
659                      [ lapply Heq_access_mode <Heq0 #Heq1
660                        @(jmeq_to_eq ??? Heq1) ]
661                      #Hloadv <Heq0
662                      whd in match (shift_offset ???); >commutative_addition_n >addition_n_0
663                      >Hloadv @refl ]
664            | 3: (* Register local variable *)
665                 #Hlookup_eq
666                 lapply (res_inversion ?????? Hlookup_eq)
667                 * * #var_id_alloc_type' #var_id_type' * #Hlookup' #Heq destruct (Heq)
668                 #Htype_eq
669                 cases (type_should_eq_inversion
670                            var_id_type
671                            ty
672                            (λt0:type.Σe':expr (typ_of_type t0).expr_vars (typ_of_type t0) e' (local_id vars))
673                            … Htype_eq) -Htype_eq
674                 (* Reverting all premises in order to perform type rewrite *)
675                 #Htype_eq
676                 lapply Hlookup' -Hlookup' lapply Hlookup_eq -Hlookup_eq
677                 lapply Hcl_load_success -Hcl_load_success
678                 lapply Hcl_lookup -Hcl_lookup
679                 lapply Hyp_present -Hyp_present
680                 lapply Hexpr_vars -Hexpr_vars
681                 lapply cm_expr
682                 destruct (Htype_eq)
683                 #cm_expr #Hexpr_vars #Hyp_present #Hcl_lookup #Hcl_load_success #Hlookup_eq #Hlookup'
684                 #Hexpr_eq lapply (jmeq_to_eq ??? Hexpr_eq) -Hexpr_eq #Hexpr_eq
685                 destruct (Hexpr_eq)
686                 whd in match (eval_expr ???????);
687                 whd in match (lookup_present ?????);
688                 lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
689                 >Hlookup' normalize nodelta #Hmatching
690                 cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success
691                 #loaded_val * #Hload_val
692                 whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
693                 lapply (opt_to_res_inversion ???? Hload_val) -Hload_val
694                 #Hload_success
695                 cases (Hmatching … Hload_success) #val'
696                 * #Hlookup_in_cm #Hvalue_eq %{val'}
697                 cases Hyp_present
698                 >Hlookup_in_cm normalize nodelta #_ @conj try @refl try assumption
699                 (* seems ok *)
700            ]
701       ]       
702  | 2: whd in match (typeof ?) in Hind;
703       lapply (Hind cm_expr Hexpr_vars Htranslate_expr cl_b cl_o cl_t Hyp_present) -Hind
704       cases (bind_inversion ????? Hcl_success) -Hcl_success * #cl_subexpr_val #cl_trace *
705       #Hexec_expr
706       @(match cl_subexpr_val
707         return λx. cl_subexpr_val = x → ?
708         with
709         [ Vundef ⇒ λHval_eq. ?
710         | Vint sz' i ⇒ λHval_eq. ?
711         | Vnull ⇒ λHval_eq. ?
712         | Vptr p ⇒ λHptr_eq. ? ] (refl ? cl_subexpr_val)) normalize nodelta
713       whd in ⊢ ((???%) → ?);
714       [ 1,2,3: #Habsurd destruct ] #Heq destruct (Heq) destruct (Hptr_eq)
715       whd in match (exec_lvalue' ?????) in Hind; #Hind
716       cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success #cl_val
717       * #Hopt_to_res whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
718       lapply (opt_to_res_inversion ???? Hopt_to_res) -Hopt_to_res #Hload_success
719       whd in Hexec_expr:(???%); whd in match (exec_lvalue' ?????) in Hind;
720       lapply Hind -Hind >Hexec_expr normalize nodelta
721       #Hind lapply (Hind (refl ??)) -Hind
722       @(match E (pblock p)
723         return λx. (E (pblock p) = x) → ?
724         with
725         [ None ⇒ λHembed. ?
726         | Some loc ⇒ λHembed. ? ] (refl ? (E (pblock p))))
727       normalize nodelta
728       [ 1: @False_ind ]
729       cases loc in Hembed; normalize nodelta
730       lapply Hload_success -Hload_success
731       lapply Hexec_expr -Hexec_expr
732       lapply Hyp_present -Hyp_present
733       lapply Htranslate_expr -Htranslate_expr
734       lapply Hexpr_vars -Hexpr_vars
735       lapply cm_expr -cm_expr
736       cases ty
737       [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
738       | #structname #fieldspec | #unionname #fieldspec | #id ]
739       normalize nodelta
740       #cm_expr #Hexpr_vars #Htranslate_expr #Hyp_present #Hexec_expr
741       #Hload_success #BL #OFF #Hembed
742       [ 1,6,7: normalize in Hload_success; #_ destruct
743       | 4,5: whd in match (typ_of_type ?); #Heval >Heval
744              %{(Vptr (mk_pointer BL (offset_plus (poff p) OFF)))}
745              @conj try @refl
746              lapply (load_value_of_type_by_ref … Hload_success ??) try //
747              #Heq >Heq %4 whd in ⊢ (??%%); >Hembed @refl
748       | *: * #cm_val * #Hloadv #Heval_expr >Heval_expr
749              lapply (mi_inj … Hinj … (pblock p) (poff p) BL (offset_plus (poff p) OFF) … Hload_success)
750              [ 1,4,7: whd in ⊢ (??%?); >Hembed @refl
751              | 2,5,8: @(load_by_value_success_valid_pointer … Hload_success) // ]
752              * #cm_val' * >Hload_success #Hload_success' #Hvalue_eq'
753              %{cm_val'} @conj try assumption
754              whd in Hloadv:(??%?) Hload_success':(??%?); >Hloadv in Hload_success';
755              #Heq destruct @refl ]
756  | 3: lapply Hcl_load_success -Hcl_load_success lapply Hcl_success -Hcl_success
757       lapply (refl ? (typeof e1))
758       cases (typeof e1) in ⊢ ((???%) → %);
759       [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
760       | #structname #fieldspec | #unionname #fieldspec | #id ]
761       #Heq_typeof normalize nodelta
762       [ 1,2,3,4,5,8: #Habsurd destruct ]
763       #Hexec_compound_clight
764       lapply (Hind … Htranslate_expr) -Hind -Htranslate_expr
765       cases (bind_inversion ????? Hexec_compound_clight) -Hexec_compound_clight
766       * * #CLB #CLO #CLTR
767       * #Hexec_lvalue #Hfield_offset whd in match (exec_lvalue' ?????);
768       >Hexec_lvalue normalize nodelta >Heq_typeof normalize nodelta
769       whd in match (m_bind ?????);
770       [ 2: normalize in Hfield_offset; destruct (Hfield_offset)
771            #Hind lapply (Hind ??? Hyp_present (refl ??)) -Hind
772            @(match E cl_b
773            return λx. (E cl_b = x) → ?
774            with
775            [ None ⇒ λHembed. ?
776            | Some loc ⇒ λHembed. ? ] (refl ? (E cl_b))) normalize nodelta
777            [ 1: @False_ind ] cases loc in Hembed; #BLO #OFF #Hembed normalize nodelta
778            lapply Hyp_present -Hyp_present
779            lapply Hexpr_vars -Hexpr_vars
780            lapply cm_expr -cm_expr
781            cases ty normalize nodelta
782            [ | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain'
783            | #structname' #fieldspec' | #unionname' #fieldspec' | #id' ]
784            #cm_expr #Hexpr_vars #Hyp_present
785            [ 1,6,7: #_ #Hload_void cases (bind_inversion ????? Hload_void)
786                   #val * #Hopt_to_res #Hok lapply (opt_to_res_inversion ???? Hopt_to_res)
787                   normalize in ⊢ (% → ?); #Habsurd destruct                   
788            | 4,5: whd in match (typ_of_type ?); #Heval >Heval
789                   #Hload_success_hyp cases (bind_inversion ????? Hload_success_hyp)
790                   #cl_val * #Hopt_to_res whd in ⊢ ((???%) → ?);                   
791                   lapply (opt_to_res_inversion ???? Hopt_to_res)
792                   #Hload_success #Heq destruct (Heq)
793                   lapply (load_value_of_type_by_ref … Hload_success ??) try //
794                   #Hval_eq >Hval_eq                   
795                   %{(Vptr (mk_pointer BLO (offset_plus cl_o OFF)))}
796                   @conj try @refl
797                   %4 whd in ⊢ (??%%); >Hembed @refl
798            | 2,3,8: * #cm_val * #Hloadv #Heval_expr >Heval_expr
799                   #Hload_success_hyp cases (bind_inversion ????? Hload_success_hyp)
800                   #cl_val * #Hopt_to_res whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
801                   lapply (opt_to_res_inversion ???? Hopt_to_res)
802                   #Hload_success
803                   lapply (mi_inj … Hinj … cl_b cl_o BLO (offset_plus cl_o OFF) … Hload_success)
804                   [ 1,4,7: whd in ⊢ (??%?); >Hembed @refl
805                   | 2,5,8: @(load_by_value_success_valid_pointer … Hload_success) // ]
806                   * #cm_val' * >Hload_success #Hload_success' #Hvalue_eq'
807                   %{cm_val'} @conj try assumption
808                   whd in Hloadv:(??%?) Hload_success':(??%?); >Hloadv in Hload_success';
809                   #Heq destruct (Heq) @refl ]
810       | 1: cases (bind_inversion ????? Hfield_offset) -Hfield_offset #field_offset * #Hfield_offset_eq
811            #Heq whd in Heq:(???%); destruct (Heq) >Hfield_offset_eq normalize nodelta
812            #Hind lapply (Hind ??? Hyp_present (refl ??)) -Hind
813            @(match E cl_b
814            return λx. (E cl_b = x) → ?
815            with
816            [ None ⇒ λHembed. ?
817            | Some loc ⇒ λHembed. ? ] (refl ? (E cl_b)))
818            normalize nodelta
819            [ 1: @False_ind ] cases loc in Hembed; #BLO #OFF #Hembed normalize nodelta
820            lapply Hyp_present -Hyp_present
821            lapply Hexpr_vars -Hexpr_vars
822            lapply cm_expr -cm_expr
823            cases ty normalize nodelta
824            [ | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain'
825            | #structname' #fieldspec' | #unionname' #fieldspec' | #id' ]           
826            #cm_expr #Hexpr_vars #Hyp_present
827            [ 1,6,7: #_ #Hload_void cases (bind_inversion ????? Hload_void)
828                   #val * #Hopt_to_res #Hok lapply (opt_to_res_inversion ???? Hopt_to_res)
829                   normalize in ⊢ (% → ?); #Habsurd destruct
830            | 4,5: whd in match (typ_of_type ?); #Heval >Heval
831                   #Hload_success_hyp cases (bind_inversion ????? Hload_success_hyp) -Hload_success_hyp
832                   #cl_val * #Hopt_to_res whd in ⊢ ((???%) → ?);                   
833                   lapply (opt_to_res_inversion ???? Hopt_to_res)
834                   #Hload_success #Heq destruct (Heq)
835                   lapply (load_value_of_type_by_ref … Hload_success ??) try //
836                   #Hval_eq >Hval_eq                   
837                   %{(Vptr (mk_pointer BLO (offset_plus (shift_offset (bitsize_of_intsize I32) CLO (repr I32 field_offset)) OFF)))}
838                   @conj try @refl
839                   %4 whd in ⊢ (??%%); >Hembed @refl
840            | 2,3,8: * #cm_val * #Hloadv #Heval_expr >Heval_expr
841                   #Hload_success_hyp cases (bind_inversion ????? Hload_success_hyp)
842                   #cl_val * #Hopt_to_res whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
843                   lapply (opt_to_res_inversion ???? Hopt_to_res)
844                   #Hload_success
845                   lapply (mi_inj ??? Hinj
846                            cl_b
847                            (mk_offset
848                              (addition_n offset_size (offv CLO)
849                              (sign_ext (bitsize_of_intsize I32) offset_size (repr I32 field_offset))))
850                            BLO (offset_plus (mk_offset
851                              (addition_n offset_size (offv CLO)
852                              (sign_ext (bitsize_of_intsize I32) offset_size (repr I32 field_offset)))) OFF) ? val ?? Hload_success)
853                   [ 1,4,7: whd in ⊢ (??%?); >Hembed @refl
854                   | 2,5,8: @(load_by_value_success_valid_pointer … Hload_success) // ]
855                   * #cm_val' * >Hload_success #Hload_success' #Hvalue_eq'
856                   %{cm_val'} @conj try assumption
857                   whd in Hloadv:(??%?) Hload_success':(??%?); >Hloadv in Hload_success';
858                   #Heq destruct (Heq) @refl ]
859  ] ]
860| 3: #var #ty #cmexpr #Hexpr_vars #Htranslate_var #cl_blo #cl_off #trace #Hyp_present #Hexec_lvalue_var
861     whd in Hexec_lvalue_var:(??%?);
862     (* check whether var is local or global *)
863     lapply (Hlocal_matching var) cases (lookup ?? cl_env var) in Hexec_lvalue_var;
864     normalize nodelta
865     [ 1: (* global *)
866          #Hexec_opt
867          cases (bind_inversion ????? Hexec_opt) -Hexec_opt #varblock * #Hopt_to_res #Heq
868          whd in Heq:(???%) Hopt_to_res:(???%); destruct (Heq)
869          >(opt_to_res_inversion ???? Hopt_to_res) normalize nodelta
870          #Hembed >Hembed normalize nodelta
871          (* Standard stuff. *)
872          @cthulhu
873     | 2: (* local *)
874          @cthulhu
875     ]
876| *: @cthulhu
877] qed.
878
879
880
881axiom clight_cminor_rel : clight_cminor_inv → Clight_state → Cminor_state → Prop.
882
883(* Conjectured simulation results
884
885   We split these based on the start state:
886   
887   1. ‘normal’ states take some [S n] normal steps and simulates them by [S m]
888      normal steps in Cminor;
889   2. call and return steps are simulated by a call/return step plus [m] normal
890      steps (to copy stack allocated parameters / results); and
891   3. lone cost label steps are simulates by a lone cost label step
892   
893   These should allow us to maintain enough structure to identify the Cminor
894   subtrace corresponding to a measurable Clight subtrace.
895 *)
896
897definition clight_normal : Clight_state → bool ≝
898λs. match Clight_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
899
900definition cminor_normal : Cminor_state → bool ≝
901λs. match Cminor_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
902
903axiom clight_cminor_normal :
904  ∀INV:clight_cminor_inv.
905  ∀s1,s1',s2,tr.
906  clight_cminor_rel INV s1 s1' →
907  clight_normal s1 →
908  ¬ Clight_labelled s1 →
909  ∃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〉) →
910  ∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'.
911    tr = tr' ∧
912    clight_cminor_rel INV s2 s2'
913  ).
914
915axiom clight_cminor_call_return :
916  ∀INV:clight_cminor_inv.
917  ∀s1,s1',s2,tr.
918  clight_cminor_rel INV s1 s1' →
919  match Clight_classify s1 with [ cl_call ⇒ true | cl_return ⇒ true | _ ⇒ false ] →
920  after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
921  ∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'.
922    tr = tr' ∧
923    clight_cminor_rel INV s2 s2'
924  ).
925
926axiom clight_cminor_cost :
927  ∀INV:clight_cminor_inv.
928  ∀s1,s1',s2,tr.
929  clight_cminor_rel INV s1 s1' →
930  Clight_labelled s1 →
931  after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
932  after_n_steps 1 … Cminor_exec (ge_cm INV) s1' (λs.true) (λtr',s2'.
933    tr = tr' ∧
934    clight_cminor_rel INV s2 s2'
935  ).
936
Note: See TracBrowser for help on using the repository browser.