source: src/Clight/toCminorCorrectness.ma @ 2510

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

Some progress on the Cl -> Cm front

File size: 30.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
397lemma exec_alloc_hit_monotonic : ∀variables,env,env',var_id.
398  (∃m,m'.exec_alloc_variables env m variables=〈env',m'〉) →
399  ∀bl. lookup ?? env var_id = Some ? bl →
400  ∃bl'.lookup ?? env' var_id = Some ? bl'.
401#variables elim variables
402[ #env #env' #var_id * #m * #m' normalize #Heq destruct
403  #bl #H %{bl} @H
404| * #id #ty #tl #Hind #env #env' #var_id
405  * #m * #m'
406  whd in match (exec_alloc_variables ???);
407  cases (alloc ????) #m * #b' #Hregion normalize nodelta
408  @(match identifier_eq ? id var_id with [ inl Heq ⇒ ? | inr Hneq ⇒ ? ])
409  [ 2: #Hexec' #bl #Hlookup
410        lapply (Hind ?? var_id (ex_intro … (ex_intro … Hexec')) bl ?)
411        [ <Hlookup @lookup_add_miss @sym_neq @Hneq ] // ]
412  destruct (Heq) #Hexec' #bl' #Hlookup
413  @(Hind ?? var_id (ex_intro … (ex_intro … Hexec')) b' ?)
414  @lookup_add_hit
415] qed.
416
417lemma exec_alloc_fail_antimonotonic : ∀variables,env,env',var_id.
418  (∃m,m'.exec_alloc_variables env m variables=〈env',m'〉) →
419  lookup ?? env' var_id = None ? →
420  lookup ?? env var_id = None ? ∧
421  ¬(Exists (ident×type) (λx:ident×type.\fst  x=var_id) variables). 
422#vars elim vars
423[ #env #env' #var_id normalize * #m * #m' #Heq destruct (Heq)
424  #H @conj try @H % //
425| * #id' #ty' #tl #Hind #env #env' #var * #m * #m'
426  whd in ⊢ ((??%?) → ? → ?);
427  cases (alloc m 0 (sizeof ty') XData) #m0 * #b #Hregion
428  normalize nodelta #Hexec #Hlookup
429  lapply (Hind …  (ex_intro … (ex_intro … Hexec)) Hlookup)
430  cases env #env cases id' #id' cases var #var normalize
431  @(eqb_elim … id' var)
432  [ 2: #Hneq * #Hlookup' #Hexists' lapply (lookup_opt_pm_set_miss ? (Some ? b) … env (sym_neq ??? Hneq))
433       #Heq <Heq @conj try @Hlookup' % *
434       [ #Heq' destruct (Heq') cases Hneq #H @H @refl
435       | cases Hexists' #H @H ]
436  | 1: #Heq destruct (Heq) * #Hlookup' #Hexists'   
437       lapply (lookup_opt_pm_set_hit … (Some ? b) var … env) #H1
438       >H1 in Hlookup'; #Heq destruct
439  ]
440] qed.
441
442lemma variable_not_in_env_but_in_vartypes_is_global :
443  ∀env,env',f,vars,stacksize,globals,var_id,allocty,ty.
444  (∃m,m'.exec_alloc_variables env m (fn_params f@fn_vars f) =〈env',m'〉) →
445  characterise_vars globals f =〈vars,stacksize〉 →
446  lookup ?? env' var_id = None ? →       
447  lookup' vars var_id = OK ? 〈allocty, ty〉 →
448  ∃r.allocty = Global r.
449#env #env' #f #vars #stacksize #globals #var_id #allocty #ty #Hexec_alloc
450#Hcharacterise #Hlookup_fail #Hlookup_type_ok
451lapply (characterise_vars_src … Hcharacterise var_id ?)
452[ whd % cases (res_inversion ?????? Hlookup_type_ok) * #vt #t *
453 #Hlookup >Hlookup #_ #Habsurd destruct ]
454*
455[ 1: * #r * #ty' * #Hlookup' #Hex %{r}
456     >Hlookup' in Hlookup_type_ok; #Heq destruct @refl ]
457* #t whd in ⊢ (% → ?); >Hlookup_type_ok whd normalize nodelta
458@(match allocty
459  return λx. allocty = x → ?
460  with
461  [ Global r ⇒ λ_. ?
462  | Stack st' ⇒ λHalloc. ?
463  | Local ⇒ λHalloc. ?
464  ] (refl ? allocty))
465[ @False_ind ] normalize nodelta
466#Heq_typ
467(* Halloc is in contradiction with Hlookup_fail *)
468lapply (exec_alloc_fail_antimonotonic … Hexec_alloc … Hlookup_fail)
469* #Hlookup' #Hnot_exists
470lapply (characterise_vars_all … Hcharacterise var_id t ?)
471[ 1,3: whd destruct (Halloc) >Hlookup_type_ok // ]
472#Hexists @False_ind
473cut (Exists (ident×type) (λx:ident×type.\fst  x=var_id) (fn_params f@fn_vars f))
474[ 1,3: elim (fn_params f @ fn_vars f) in Hexists; //
475       * #id' #ty' #tl #Hind *
476       [ 1,3: * #Heq #_ %1 @Heq
477       | *: #H %2 @Hind @H ] ]
478#H cases Hnot_exists #H' @H' @H
479qed.
480 
481
482(* TODO : memory injections + link clight env+mem with local env+stack+mem *)
483lemma eval_expr_sim :
484  ∀(inv:clight_cminor_inv).
485  ∀(f:function).
486  ∀(vars:var_types).
487  ∀stacksize.
488  characterise_vars (globals inv) f = 〈vars, stacksize〉 →
489  ∀(cl_env:cl_env).
490  (∃m,m'. exec_alloc_variables empty_env m (fn_params f @ fn_vars f) = 〈cl_env,m'〉) →
491  ∀(cl_m:mem).
492  ∀(cm_env:cm_env).
493  ∀(sp:block).
494  ∀(cm_m:mem).
495  ∀E:embedding.
496  ∀minj:memory_inj E cl_m cm_m.
497  memory_matching E cl_m cm_m cl_env cm_env inv sp vars →
498  (∀(e:expr).
499   ∀(e':CMexpr (typ_of_type (typeof e))).
500   ∀Hexpr_vars.
501   translate_expr vars e = OK ? («e', Hexpr_vars») →
502   ∀cl_val,trace,Hyp_present.
503   exec_expr (ge_cl … inv) cl_env cl_m e = OK ? 〈cl_val, trace〉 →
504   ∃cm_val. eval_expr (ge_cm inv) (typ_of_type (typeof e)) e' cm_env Hyp_present sp cm_m = OK ? 〈trace, cm_val〉 ∧
505            value_eq E cl_val cm_val) ∧
506  (∀ed,ty.
507   ∀(e':CMexpr (typ_of_type ty)).
508   ∀Hexpr_vars.
509   translate_expr vars (Expr ed ty) = OK ? («e', Hexpr_vars») →
510   ∀resblo,resoff,trace,Hyp_present.
511   exec_lvalue' (ge_cl … inv) cl_env cl_m ed ty = OK ? 〈resblo, resoff, trace〉 →
512   (* TODO: shift 〈resblo, resoff〉 through E *)
513   eval_expr (ge_cm inv) (typ_of_type ty) e' cm_env Hyp_present sp cm_m = OK ? 〈trace, Vptr (mk_pointer resblo resoff)〉).
514#inv #f #vars #stacksize #Hcharacterise #cl_env #Hexec_alloc #cl_m #cm_env
515#sp #cm_m #E #Hinj #Hlocal_matching
516@expr_lvalue_ind_combined
517[ 1: (* Integer constant *)
518  #csz #ty cases ty
519  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
520  | #structname #fieldspec | #unionname #fieldspec | #id ] 
521  #i whd in match (typeof ?); #e' #Hexpr_vars #Htranslate
522  #val #trace #Hpresent #Hexec_cl
523  whd in Htranslate:(??%?);
524  [ 1,3,4,5,6,7,8: destruct ]
525  (* This intsize_eq_elim' is the proof-equivalent of eating a sandwich with
526     sand inside. *)
527  @cthulhu
528| 2: *
529  [ #sz #i | #var_id | #e1 | #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: (* Deref case. Reduce the deref, exhibit the underlying load. *)
696       cases (bind_inversion ????? Hcl_success) -Hcl_success
697       * #cl_subexpr_val #cl_subexpr_trace *
698       whd in ⊢ (? → (???%) → ?);
699       @(match cl_subexpr_val
700         return λx. cl_subexpr_val = x → ?
701         with
702         [ Vundef ⇒ λHval_eq. ?
703         | Vint sz' i ⇒ λHval_eq. ?
704         | Vnull ⇒ λHval_eq. ?
705         | Vptr p ⇒ λHptr_eq. ? ] (refl ? cl_subexpr_val)) normalize nodelta
706       [ 1,2,3: #_ #Habsurd destruct ]
707       #Hcl_exec_to_pointer #Heq destruct (Heq)
708       (* Now that we have executed the Clight part, reduce the Cminor one *)
709       whd in Htranslate_expr:(??%?);
710       cases (bind_inversion ????? Htranslate_expr) -Htranslate_expr
711       * #cm_expr #Hexpr_vars * #Htranslate_expr
712       whd (* ... *)   @cthulhu
713  | 3: @cthulhu ]
714| *: @cthulhu
715] qed. 
716
717
718
719axiom clight_cminor_rel : clight_cminor_inv → Clight_state → Cminor_state → Prop.
720
721(* Conjectured simulation results
722
723   We split these based on the start state:
724   
725   1. ‘normal’ states take some [S n] normal steps and simulates them by [S m]
726      normal steps in Cminor;
727   2. call and return steps are simulated by a call/return step plus [m] normal
728      steps (to copy stack allocated parameters / results); and
729   3. lone cost label steps are simulates by a lone cost label step
730   
731   These should allow us to maintain enough structure to identify the Cminor
732   subtrace corresponding to a measurable Clight subtrace.
733 *)
734
735definition clight_normal : Clight_state → bool ≝
736λs. match Clight_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
737
738definition cminor_normal : Cminor_state → bool ≝
739λs. match Cminor_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
740
741axiom clight_cminor_normal :
742  ∀INV:clight_cminor_inv.
743  ∀s1,s1',s2,tr.
744  clight_cminor_rel INV s1 s1' →
745  clight_normal s1 →
746  ¬ Clight_labelled s1 →
747  ∃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〉) →
748  ∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'.
749    tr = tr' ∧
750    clight_cminor_rel INV s2 s2'
751  ).
752
753axiom clight_cminor_call_return :
754  ∀INV:clight_cminor_inv.
755  ∀s1,s1',s2,tr.
756  clight_cminor_rel INV s1 s1' →
757  match Clight_classify s1 with [ cl_call ⇒ true | cl_return ⇒ true | _ ⇒ false ] →
758  after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
759  ∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'.
760    tr = tr' ∧
761    clight_cminor_rel INV s2 s2'
762  ).
763
764axiom clight_cminor_cost :
765  ∀INV:clight_cminor_inv.
766  ∀s1,s1',s2,tr.
767  clight_cminor_rel INV s1 s1' →
768  Clight_labelled s1 →
769  after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
770  after_n_steps 1 … Cminor_exec (ge_cm INV) s1' (λs.true) (λtr',s2'.
771    tr = tr' ∧
772    clight_cminor_rel INV s2 s2'
773  ).
774
Note: See TracBrowser for help on using the repository browser.