source: src/Clight/toCminorCorrectness.ma @ 2500

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

Continuing work on simulation in Clight/Cminor?

File size: 22.0 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
283definition local_matching ≝
284  λE:embedding.
285  λm,m':mem.
286  λen:cl_env.
287  λvenv:cm_env.
288  λsp:block.
289  λvars:var_types.
290
291  ∀id,cl_blo. lookup SymbolTag ? en id = Some ? cl_blo →
292              match lookup ?? vars id with
293              [ Some kind ⇒
294                let 〈vtype, type〉 ≝ kind in
295                match vtype with
296                [ Stack n ⇒
297                  E cl_blo = Some ? 〈sp, offset_of_Z (Z_of_nat n)〉
298                | Local ⇒
299                  ∀v. load_value_of_type type m cl_blo zero_offset = Some ? v →
300                      ∃v'. lookup ?? venv id = Some ? v' ∧
301                           value_eq E v v'
302                | _ ⇒ False ]
303              | None ⇒ False ].
304             
305lemma type_should_eq_inversion :
306  ∀ty1,ty2,P,f,res.
307    type_should_eq ty1 ty2 P f = OK ? res →
308    ty1 = ty2 ∧ f ≃ res.
309#ty1 #ty2 #P #f #res normalize
310cases (type_eq_dec ty1 ty2) normalize nodelta
311[ 2: #Hneq #Habsurd destruct ]
312#Heq #Heq2 @conj try assumption
313destruct (Heq2) cases Heq normalize nodelta
314@eq_to_jmeq @refl
315qed.
316
317lemma load_value_of_type_by_ref :
318  ∀ty,m,b,off,val.
319    load_value_of_type ty m b off = Some ? val →
320    typ_of_type ty ≃ ASTptr →
321    access_mode ty ≃ By_reference →
322    val = Vptr (mk_pointer b off).
323*
324[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
325| #structname #fieldspec | #unionname #fieldspec | #id ]
326#m #b #off #val
327[ 1,6,7: normalize #Habsurd destruct (Habsurd)
328| 4,5: normalize #Heq #_ #_ destruct @refl
329| 2: #_ normalize #Heq destruct
330| *: #Hload normalize #_ #H
331      lapply (jmeq_to_eq ??? H) #Heq destruct
332] qed.       
333
334
335
336(* TODO : memory injections + link clight env+mem with local env+stack+mem *)
337lemma eval_expr_sim :
338  ∀(inv:clight_cminor_inv).
339
340  ∀(cl_env:cl_env).
341  ∀(cl_m:mem).
342
343  ∀(cm_env:cm_env).
344  ∀(sp:block).
345  ∀(cm_m:mem).
346  ∀(vars:var_types).
347
348  ∀E:embedding.
349  ∀minj:memory_inj E cl_m cm_m.
350  local_matching E cl_m cm_m cl_env cm_env sp vars →
351
352   (*vars = pi1 … (characterise_vars … [globals] [f]) →*)
353   (*local_matching en m venv sp m' →  *)
354
355  (∀(e:expr).
356   ∀(e':CMexpr (typ_of_type (typeof e))).
357   ∀Hexpr_vars.
358   translate_expr vars e = OK ? («e', Hexpr_vars») →
359   ∀cl_val,trace,Hyp_present.
360   exec_expr (ge_cl … inv) cl_env cl_m e = OK ? 〈cl_val, trace〉 →
361   ∃cm_val. eval_expr (ge_cm inv) (typ_of_type (typeof e)) e' cm_env Hyp_present sp cm_m = OK ? 〈trace, cm_val〉 ∧
362            value_eq E cl_val cm_val) ∧
363
364  (∀ed,ty.
365   ∀(e':CMexpr (typ_of_type ty)).
366   ∀Hexpr_vars.
367   translate_expr vars (Expr ed ty) = OK ? («e', Hexpr_vars») →
368   ∀resblo,resoff,trace,Hyp_present.
369   exec_lvalue' (ge_cl … inv) cl_env cl_m ed ty = OK ? 〈resblo, resoff, trace〉 →
370   (* TODO: shift 〈resblo, resoff〉 through E *)
371   eval_expr (ge_cm inv) (typ_of_type ty) e' cm_env Hyp_present sp cm_m = OK ? 〈trace, Vptr (mk_pointer resblo resoff)〉).
372#inv #cl_env #cl_m #cm_env #sp #cm_m #vars #E #Hinj #Hlocal_matching
373@expr_lvalue_ind_combined
374[ 1: (* Integer constant *)
375  #csz #ty cases ty
376  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
377  | #structname #fieldspec | #unionname #fieldspec | #id ] 
378  #i whd in match (typeof ?); #e' #Hexpr_vars #Htranslate
379  #val #trace #Hpresent #Hexec_cl
380  whd in Htranslate:(??%?);
381  [ 1,3,4,5,6,7,8: destruct ]
382  (* This intsize_eq_elim' is the proof-equivalent of eating a sandwich with
383     sand inside. *)
384  @cthulhu
385| 2: *
386  [ #sz #i | #var_id | #e1 | #e1 | #op #e1 | #op #e1 #e2 | #cast_ty #e1
387  | #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
388  try /2 by I/
389  #ty whd in ⊢ (% → ?); #Hind
390  whd in match (Plvalue ???);
391  whd in match (typeof ?);
392  #cm_expr #Hexpr_vars #Htranslate_expr #val #trace #Hyp_present #Hexec
393  whd in Hexec:(??%?);
394  whd in match (exec_lvalue' ?????) in Hexec:(??%?);
395  cases (bind_inversion ????? Hexec) -Hexec * * #cl_b #cl_o #cl_t * #Hcl_success #Hcl_load_success
396  whd in Hcl_success:(???%);
397  [ 1: (* var case *)
398
399       lapply Hcl_success -Hcl_success
400       (* Peform case analysis on presence of variable in local Clight env.
401        * if success, exec_expr/exec_lvalue tells us that it shoud be local. *)
402       @(match lookup SymbolTag block cl_env var_id
403         return λx.(lookup SymbolTag block cl_env var_id = x) → ?
404         with
405         [ None ⇒ λHcl_lookup. ?
406         | Some loc ⇒ λHcl_lookup. ?
407         ] (refl ? (lookup SymbolTag block cl_env var_id)))
408       normalize nodelta
409       [ 1: (* global case *)
410            @cthulhu (* TODO: case analysis on lookup in global, if so use Brian's invariant *)
411       | 2: (* local case *)
412            #Heq destruct (Heq)
413            lapply (bind2_eq_inversion ?????? Htranslate_expr) -Htranslate_expr
414            * #var_id_alloc_type * #var_id_type *
415            generalize in match var_id_alloc_type; * normalize nodelta
416            [ 1: (* Global case. This should be contradictory, right ?
417                  * If lookup succeeded, then our local shadows any global with the same
418                  * name, and [characterise_vars] should say so. TODO, this lemma. *)
419                 @cthulhu
420            | 2: (* Stack local *)
421                 lapply Hcl_load_success -Hcl_load_success
422                 lapply Hyp_present -Hyp_present
423                 lapply Hexpr_vars -Hexpr_vars
424                 lapply cm_expr -cm_expr inversion (access_mode ty)
425                 [ #typ_of_ty | | #typ_of_ty ]
426                 #Heq_typ_of_type #Heq_access_mode
427                 #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_success
428                 #stack_depth #Hlookup_vartype_success normalize nodelta
429                 whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
430                 lapply (Hlocal_matching … Hcl_lookup)
431                 whd in Hlookup_vartype_success:(??%?);
432                 cases (res_inversion ?????? Hlookup_vartype_success) -Hlookup_vartype_success
433                 * #var_id_alloc_type' #var_id_type' * #Hlookup' #Heq destruct (Heq)
434                 >Hlookup' normalize nodelta #Hembedding_eq
435                 cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success
436                 #loaded_val * #Hload_val
437                 whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
438                 lapply (opt_to_res_inversion ???? Hload_val) -Hload_val
439                 #Hload_success
440                 whd in match (eval_expr ???????);
441                 cut (pointer_translation (mk_pointer cl_b zero_offset) E =
442                      Some ? (mk_pointer sp (offset_of_Z stack_depth)))
443                 [ 1,3: whd in ⊢ (??%?); >Hembedding_eq normalize nodelta
444                        >offset_plus_0 @refl ]
445                 #Hpointer_translation       
446                 [ 2: (* By-ref *)
447                      whd in Hload_success:(??%?);
448                      lapply (load_value_of_type_by_ref … Hload_success … Heq_typ_of_type Heq_access_mode)
449                      #Heq_val
450                      >Heq_val
451                      %{(Vptr (mk_pointer sp (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 stack_depth))))}
452                      @conj try @refl
453                      %4 (* boring and trivial *)
454                      @cthulhu                     
455                 | 1: (* By value *)
456                      lapply (mi_inj … Hinj … Hpointer_translation … Hload_success)
457                      [ @(load_by_value_success_valid_pointer … Hload_success)
458                        lapply (jmeq_to_eq ??? Heq_typ_of_type)
459                        #Heq_typ_of_type'
460                        (* boring and trivial *)
461                        @cthulhu ]
462                      * #cm_val * #Hload_in_cm #Hvalue_eq
463                      %{cm_val} @conj try assumption
464                      (* unpack Hload_in_cm using Heq_access_mode as an hypothesis. profit *)
465                      @cthulhu ]
466            | 3: (* Register local variable *)
467                 #Hlookup_eq
468                 lapply (res_inversion ?????? Hlookup_eq)
469                 * * #var_id_alloc_type' #var_id_type' * #Hlookup' #Heq destruct (Heq)
470                 #Htype_eq
471                 cases (type_should_eq_inversion
472                            var_id_type
473                            ty
474                            (λt0:type.Σe':expr (typ_of_type t0).expr_vars (typ_of_type t0) e' (local_id vars))
475                            … Htype_eq) -Htype_eq
476                 (* Reverting all premises in order to perform type rewrite *)
477                 #Htype_eq
478                 lapply Hlookup' -Hlookup' lapply Hlookup_eq -Hlookup_eq
479                 lapply Hcl_load_success -Hcl_load_success
480                 lapply Hcl_lookup -Hcl_lookup
481                 lapply Hyp_present -Hyp_present
482                 lapply Hexpr_vars -Hexpr_vars
483                 lapply cm_expr
484                 destruct (Htype_eq)
485                 #cm_expr #Hexpr_vars #Hyp_present #Hcl_lookup #Hcl_load_success #Hlookup_eq #Hlookup'
486                 #Hexpr_eq lapply (jmeq_to_eq ??? Hexpr_eq) -Hexpr_eq #Hexpr_eq
487                 destruct (Hexpr_eq)
488                 whd in match (eval_expr ???????);
489                 whd in match (lookup_present ?????);
490                 lapply (Hlocal_matching … Hcl_lookup) >Hlookup' normalize nodelta
491                 cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success
492                 #loaded_val * #Hload_val
493                 whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
494                 lapply (opt_to_res_inversion ???? Hload_val) -Hload_val
495                 #Hload_success #Hlookup_in_cm_env
496                 cases (Hlookup_in_cm_env ? Hload_success) #val'
497                 * #Hlookup_in_cm #Hvalue_eq %{val'}
498                 cases Hyp_present
499                 >Hlookup_in_cm normalize nodelta #_ @conj try @refl try assumption
500                 (* seems ok *)
501            ]
502       ]
503  | 2: (* Deref case. Reduce the deref, exhibit the underlying load. *)
504       cases (bind_inversion ????? Hcl_success) -Hcl_success
505       * #cl_subexpr_val #cl_subexpr_trace *
506       whd in ⊢ (? → (???%) → ?);
507       @(match cl_subexpr_val
508         return λx. cl_subexpr_val = x → ?
509         with
510         [ Vundef ⇒ λHval_eq. ?
511         | Vint sz' i ⇒ λHval_eq. ?
512         | Vnull ⇒ λHval_eq. ?
513         | Vptr p ⇒ λHptr_eq. ? ] (refl ? cl_subexpr_val)) normalize nodelta
514       [ 1,2,3: #_ #Habsurd destruct ]
515       #Hcl_exec_to_pointer #Heq destruct (Heq)
516       (* Now that we have executed the Clight part, reduce the Cminor one *)
517       whd in Htranslate_expr:(??%?);
518       cases (bind_inversion ????? Htranslate_expr) -Htranslate_expr
519       * #cm_expr #Hexpr_vars * #Htranslate_expr
520       whd (* ... *)   @cthulhu
521  | 3: @cthulhu ]
522| *: @cthulhu
523] qed. 
524
525
526
527axiom clight_cminor_rel : clight_cminor_inv → Clight_state → Cminor_state → Prop.
528
529(* Conjectured simulation results
530
531   We split these based on the start state:
532   
533   1. ‘normal’ states take some [S n] normal steps and simulates them by [S m]
534      normal steps in Cminor;
535   2. call and return steps are simulated by a call/return step plus [m] normal
536      steps (to copy stack allocated parameters / results); and
537   3. lone cost label steps are simulates by a lone cost label step
538   
539   These should allow us to maintain enough structure to identify the Cminor
540   subtrace corresponding to a measurable Clight subtrace.
541 *)
542
543definition clight_normal : Clight_state → bool ≝
544λs. match Clight_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
545
546definition cminor_normal : Cminor_state → bool ≝
547λs. match Cminor_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
548
549axiom clight_cminor_normal :
550  ∀INV:clight_cminor_inv.
551  ∀s1,s1',s2,tr.
552  clight_cminor_rel INV s1 s1' →
553  clight_normal s1 →
554  ¬ Clight_labelled s1 →
555  ∃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〉) →
556  ∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'.
557    tr = tr' ∧
558    clight_cminor_rel INV s2 s2'
559  ).
560
561axiom clight_cminor_call_return :
562  ∀INV:clight_cminor_inv.
563  ∀s1,s1',s2,tr.
564  clight_cminor_rel INV s1 s1' →
565  match Clight_classify s1 with [ cl_call ⇒ true | cl_return ⇒ true | _ ⇒ false ] →
566  after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
567  ∃m. after_n_steps (S m) … Cminor_exec (ge_cm INV) s1' (λs.cminor_normal s) (λtr',s2'.
568    tr = tr' ∧
569    clight_cminor_rel INV s2 s2'
570  ).
571
572axiom clight_cminor_cost :
573  ∀INV:clight_cminor_inv.
574  ∀s1,s1',s2,tr.
575  clight_cminor_rel INV s1 s1' →
576  Clight_labelled s1 →
577  after_n_steps 1 … clight_exec (ge_cl INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
578  after_n_steps 1 … Cminor_exec (ge_cm INV) s1' (λs.true) (λtr',s2'.
579    tr = tr' ∧
580    clight_cminor_rel INV s2 s2'
581  ).
582
Note: See TracBrowser for help on using the repository browser.