source: src/Clight/CexecSound.ma @ 2588

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

modified Cexec/Csem? semantics:
. force andbool and orbool types to be Tint sz sg, fail otherwise
. cast result of evaluation to (bitvector sz)
. in lvalue evaluation, field offset for structs is now 16 bit instead of 32
/!\ induction principles modified accordingly
. soundness and correctness adapted

modified label/labelSimulation:
. andbool and orbool are modified so that the true/false constants are

casted to the (integer) type of the enclosing expression, to match
Csem/Cexec?. If the type is not an integer, default on 32 bits.

. labelSimulation proof adapted to match changes.

proof of simulation for expressions Cl to Cm finished
. caveat : eats up all my RAM (8gb) when using matita (not matitac), barely typecheckable
. moved some lemmas from toCminorCorrectness.ma to new file toCminorOps.ma

and frontend_misc.ma to alleviate this, to no avail - more radical splitting required ?

slight modification in SimplifyCasts? to take into account modifications in semantics,
removed some duplicate lemmas and replaced them by wrappers to avoid breaking the
rest of the development.

File size: 20.2 KB
RevLine 
[700]1include "Clight/Cexec.ma".
[2019]2include "Clight/CexecInd.ma".
[399]3
[487]4lemma exec_bool_of_val_sound: ∀v,ty,r.
[399]5 exec_bool_of_val v ty = OK ? r → bool_of_val v ty (of_bool r).
[487]6#v #ty #r
[2468]7cases v; [ | #sz #i (*| #f*) |  | #ptr ]
8cases ty; [ 2,10,18,26: #sz' #sg | 3,11,19,27: #ty' | 4,12,20,28: (*#r*) #ty #n
9           | 5,13,21,29: #args #rty | 6,7,14,15,22,23,30,31: #id #fs | 8,16,24,32: (*#r*) #id ]
[1516]10whd in ⊢ (??%? → ?);
[961]11[ 2: @intsize_eq_elim_elim
12  [ #NE #H destruct
13  | *; whd @eq_bv_elim
14    [ #E1 #E2 destruct @bool_of_val_false @is_false_int
[1410]15    | #E1 #E2 destruct @bool_of_val_true @is_true_int_int @E1
[961]16    ]
[487]17  ]
[2468]18(*| 8: #H cases (eq_dec f Fzero)
[1516]19  [ #e >e in H ⊢ %; >Feq_zero_true #E destruct @bool_of_val_false @is_false_float
20  | #ne >Feq_zero_false in H; // #E destruct @bool_of_val_true @is_true_float @ne
[2468]21  ]*)
22| 7: #H destruct @bool_of_val_false @is_false_pointer
23| 8: #H destruct @bool_of_val_true @is_true_pointer_pointer
[961]24| *: #H destruct
[487]25] qed.
[399]26
[487]27lemma bool_val_distinct: Vtrue ≠ Vfalse.
[1410]28% normalize #H destruct
[487]29qed.
[399]30
[487]31lemma bool_of: ∀v,ty,b. bool_of_val v ty (of_bool b) →
[399]32  if b then is_true v ty else is_false v ty.
[1336]33#v #ty #b cases b; #H inversion H; #v' #ty' #H' #ev #et #ev' //;
34@⊥ cases (bool_val_distinct) #X @X [2: @sym_eq] @ev'
[487]35qed.
[399]36
[961]37lemma try_cast_null_sound: ∀m,sz,i,ty,ty',v'. try_cast_null m sz i ty ty' = OK ? v' → cast m (Vint sz i) ty ty' v'.
38#m #sz #i #ty #ty' #v'
[1516]39whd in ⊢ (??%? → ?);
[961]40@eq_bv_elim
[487]41[ #e >e
[2468]42    cases ty; [ | #sz' #sg (* | #fs *) | (*#sp*) #ty | (*#sp*) #ty #n | #args #rty | #id #fs | #id #fs | (*#r*) #id ]
[961]43    whd in ⊢ (??%? → ?); #H [ 2: | *: destruct ]
[2468]44    cases ty' in H ⊢ %; [ | #sz'' #sg (* | #fs*) | (*#sp*) #ty | (*#sp*) #ty #n | #args #rty | #id #fs | #id #fs | (*#r*) #id ]
[961]45    try (@eq_intsize_elim #E) whd in ⊢ (??%? → ?); #H destruct @cast_ip_z //
[487]46| #_ whd in ⊢ (??%? → ?); #H destruct
47]
[2468]48qed.
[399]49
[1410]50lemma exec_cast_sound : ∀m:mem. ∀v:val. ∀ty:type. ∀ty':type. ∀v':val. exec_cast m v ty ty' = OK ? v' → cast m v ty ty' v'.
51#m #v #ty #ty' #v'
[487]52cases v;
53[ #H whd in H:(??%?); destruct;
[961]54| #sz #i cases ty;
[487]55  [ #H whd in H:(??%?); destruct;
[2468]56(* | 3: #a #H whd in H:(??%?); destruct; *)
57  | 6,7,8: #a [ 1,2: #b ] #H whd in H:(??%?); destruct;
[487]58  | #sz1 #si1 cases ty';
[1516]59    [ whd in ⊢ (??%? → ?); @intsize_eq_elim_elim
[961]60      [ #NE #H destruct
61      | *; whd #H whd in H:(??%?); destruct;
62      ]
[2468]63     (* | 3: #a whd in ⊢ (??%? → ?); @intsize_eq_elim_elim
[961]64      [ #E #H whd in H:(??%?); destruct
65      | *; whd #H whd in H:(??%?); destruct; @cast_if
[2468]66      ] *)
67    | 2,6,7,8: #a [1,2,3: #b] whd in ⊢ (??%? → ?); @intsize_eq_elim_elim
[961]68      [ 1,3,5,7: #NE #H destruct
69      | *: *; whd #H whd in H:(??%?); destruct; //
70      ]
[2468]71    | 3,4,5: [ #ty'' letin t ≝ (Tpointer ty'')
[2176]72             | #ty'' #n letin t ≝ (Tarray ty'' n)
73             | #args #rty letin t ≝ (Tfunction args rty) ]
[1516]74        whd in ⊢ (??%? → ?); @intsize_eq_elim_elim
[961]75        [ 1,3,5: #NE #H destruct
76        | *: *; whd
77          lapply (try_cast_null_sound m sz i (Tint sz si1) t v');
78          cases (try_cast_null m sz i (Tint sz si1) t);
79          [ 1,3,5: #v'' #H' #e @H' @e
80          | *: #m #_ whd in ⊢ (??%? → ?); #H destruct (H);
81          ]
[487]82        ]
83    ]
[2176]84  | *: [ #ty'' letin t ≝ (Tpointer ty'')
85       | #ty'' #n letin t ≝ (Tarray ty'' n)
86       | #args #rty letin t ≝ (Tfunction args rty) ]
[487]87        whd in ⊢ (??%? → ?);
[961]88        lapply (try_cast_null_sound m sz i t ty' v');
89        cases (try_cast_null m sz i t ty');
[487]90        [ 1,3,5: #v'' #H' #e @H' @e
[797]91        | *: #m #_ whd in ⊢ (??%? → ?); #H destruct (H);
[487]92        ]
93  ]
[2468]94(*| #f cases ty;  [ 3,4,9: #x | 2,5,6,7,8: #x #y ]
[2176]95                    [ cases ty'; [ #e | 3,4,9: #a #e | 2,6,7,8: #a #b #e | #a #b #e ]
[487]96                        whd in e:(??%?); destruct; //;
97                    | *: #e whd in e:(??%?); destruct
[2468]98                    ] *)
99| cases ty; [ 3,8: #x | 2,4,5,6,7: #x #y ]
[2176]100    whd in ⊢ (??%? → ?); #H destruct
101    cases ty' in H; normalize; try #a try #b try #c try #d destruct;
[487]102    @cast_pp_z //;
[2176]103(*
[1545]104| #ptr whd in ⊢ (??%? → ?); #e
[500]105    elim (bind_inversion ????? e) #s * #es #e'
106    elim (bind_inversion ????? e') #u * #eu #e'' -e';
107    elim (bind_inversion ????? e'') #s' * #es' #e'''; -e'';
[487]108    cut (type_region ty s);
109    [ cases ty in es:(??%?) ⊢ %; [ #e | 3: #a #e | 2,4,6,7,8,9: #a #b #e | #a #b #c #e ]
[1647]110        whd in e:(??%%); destruct; //;
[487]111    | #Hty
112        cut (type_region ty' s');
113        [ cases ty' in es' ⊢ %; [ #e | 3: #a #e | 2,4,6,7,8,9: #a #b #e | #a #b #c #e ]
[1647]114            whd in e:(??%%); destruct; //;
[487]115        | #Hty'
[1545]116            cut (s = ptype ptr). elim (eq_region_dec (ptype ptr) s) in eu; //; normalize; #_ #e destruct.
[1516]117            #e >e in Hty; #Hty
[1545]118            cases (pointer_compat_dec (pblock ptr) s') in e''';
[1647]119            #Hcompat #e''' whd in e''':(??%%); destruct /2 by cast_pp/
[487]120        ]
121    ]
[2176]122*)
123| #ptr
[2468]124  cases ty;  [ 3,8: #x | 2,4,5,6,7: #x #y ]
[2176]125  #E whd in E:(??%?); destruct
126  cases ty' in E ⊢ %; normalize #A try #B try #C try #D destruct /2/
[1410]127] qed.
[399]128
129
[2468]130
131
[487]132theorem exec_expr_sound: ∀ge:genv. ∀en:env. ∀m:mem. ∀e:expr.
[399]133(P_res ? (λx.eval_expr ge en m e (\fst x) (\snd x)) (exec_expr ge en m e)).
[498]134#ge #en #m #e @(expr_lvalue_ind ? (λe',ty.P_res ? (λr.eval_lvalue ge en m (Expr e' ty) (\fst (\fst r)) (\snd (\fst r)) (\snd r)) (exec_lvalue' ge en m e' ty)) … e)
[1516]135[ #sz #ty #c whd in ⊢ (???%); cases ty try #sz' try #sg try #x try @I whd in ⊢ (???%);
[961]136  @eq_intsize_elim #E try @I <E whd %
[2468]137(*| #ty #c whd //*)
[399]138(* expressions that are lvalues *)
[487]139| #e' #ty cases e'; //; [ #i #He' | #e #He' | #e #i #He' ] whd in He' ⊢ %;
140    @bind2_OK #x cases x; #y cases y; #sp #loc #ofs #tr #H
141    @opt_bind_OK #vl #evl whd in evl:(??%?); @(eval_Elvalue … evl)
[1516]142    >H in He'; #He' @He'
[487]143| #v #ty
144    whd in ⊢ (???%);
[1058]145    lapply (refl ? (lookup SymbolTag block en v))
[1516]146    cases (lookup SymbolTag block en v) in ⊢ (???% → %);
[487]147    [ #eget @opt_bind_OK #sploc cases sploc; #sp #loc #efind
148        whd; @(eval_Evar_global … eget efind)
149    | #loc #eget @(eval_Evar_local … eget)
150    ]
[1516]151| #ty #e #He whd in ⊢ (???%);
[2176]152    @bind2_OK #v cases v / by / * #l #ofs #tr #Hv whd
[1516]153    >Hv in He; #He
[2176]154    @eval_Ederef @He
[891]155| #ty #e'' #ty'' #He'' @bind2_OK * #loc #ofs #tr #H
[2176]156  cases ty try (try #a try #b try #c @I)
157  #ty' whd
[1516]158  @eval_Eaddrof whd in H:(??%?); >H in He''; #He'' @He''
[487]159| #ty #op #e1 #He1 @bind2_OK #v1 #tr #Hv1
160    @opt_bind_OK #v #ev
161    @(eval_Eunop … ev)
[1516]162    >Hv1 in He1; #He1 @He1
[487]163| #ty #op #e1 #e2 #He1 #He2
[1516]164    @bind2_OK #v1 #tr1 #ev1 >ev1 in He1; #He1
165    @bind2_OK #v2 #tr2 #ev2 >ev2 in He2; #He2
[487]166    @opt_bind_OK #v #ev whd in He1 He2; whd;
167    @(eval_Ebinop … He1 He2 ev)
168| #ty #ty' #e' #He'
[1516]169    @bind2_OK #v #tr #Hv >Hv in He'; #He'
[487]170    @bind_OK #v' #ev'
171    @(eval_Ecast … He' ?)
172    (* XXX /2/; *)
173    @(exec_cast_sound … ev')
174| #ty #e1 #e2 #e3 #He1 #He2 #He3
[1516]175    @bind2_OK #vb #tr1 #Hvb >Hvb in He1; #He1
[487]176    @bind_OK #b
177    cases b; #eb lapply (exec_bool_of_val_sound … eb); #Hb
[1516]178    @bind2_OK #v #tr #Hv whd in Hv:(??%?);
179    [ >Hv in He2; #He2 whd in He2 Hv:(??%?) ⊢%;
[487]180        @(eval_Econdition_true … He1 ? He2) @(bool_of ??? Hb)
[1516]181    | >Hv in He3; #He3 whd in He3 Hv:(??%?) ⊢%;
[487]182        @(eval_Econdition_false … He1 ? He3) @(bool_of ??? Hb)
183    ]
184| #ty #e1 #e2 #He1 #He2
[1516]185    @bind2_OK #v1 #tr1 #Hv1 >Hv1 in He1; #He1
[487]186    @bind_OK #b1 cases b1; #eb1 lapply (exec_bool_of_val_sound … eb1); #Hb1
[2588]187    normalize nodelta
[1516]188    [ @bind2_OK #v2 #tr2 #Hv2 >Hv2 in He2; #He2
[2588]189        @bind_OK #b2 #eb2 whd in match (cast_bool_to_target ??);
190        cases ty
191        [ | #sz #sg | #ptr_ty | #arr_ty #arr_sz | #dom #codom | #sname #flspc | #uname #flspc | #id ]
192        try @I normalize nodelta
193        @(eval_Eandbool_2 … (of_bool b2) … He1 … He2)
194        [ @(bool_of … Hb1) | @(exec_bool_of_val_sound … eb2) | @refl ]
195    | cases ty
196      [ | #sz #sg | #ptr_ty | #arr_ty #arr_sz | #dom #codom | #sname #flspc | #uname #flspc | #id ]
197      try @I
198      @(eval_Eandbool_1 … He1) [ @(bool_of … Hb1) | @refl ]
[487]199    ]
200| #ty #e1 #e2 #He1 #He2
[1516]201    @bind2_OK #v1 #tr1 #Hv1 >Hv1 in He1; #He1
[487]202    @bind_OK #b1 cases b1; #eb1 lapply (exec_bool_of_val_sound … eb1); #Hb1
[2588]203    normalize nodelta
204    [ cases ty
205      [ | #sz #sg | #ptr_ty | #arr_ty #arr_sz | #dom #codom | #sname #flspc | #uname #flspc | #id ]
206      try @I
207      @(eval_Eorbool_1 … He1) [ @(bool_of … Hb1) | @refl ]
[1516]208    | @bind2_OK #v2 #tr2 #Hv2 >Hv2 in He2; #He2
[487]209        @bind_OK #b2 #eb2
[2588]210        cases ty
211        [ | #sz #sg | #ptr_ty | #arr_ty #arr_sz | #dom #codom | #sname #flspc | #uname #flspc | #id ]
212        try @I
213        @(eval_Eorbool_2 … (of_bool b2) … He1 … He2)
214        [ @(bool_of … Hb1) | @(exec_bool_of_val_sound … eb2) | @refl ]
[487]215    ]
[1410]216| #ty #ty' cases ty try #sz try #sg try #x //
[487]217| #ty #e' #ty' #i cases ty'; //;
218    [ #id #fs #He' @bind2_OK #x cases x; #sp #l #ofs #H
[1516]219        @bind_OK #delta #Hdelta whd in H:(??%?); >H in He'; #He'
[487]220        @(eval_Efield_struct …  He' (refl ??) Hdelta)
[1516]221    | #id #fs #He' @bind2_OK #x cases x; #sp #l #ofs #H whd in H:(??%?);
222        >H in He'; #He'
[487]223        @(eval_Efield_union … He' (refl ??))
224    ]
[1516]225| #ty #l #e' #He' @bind2_OK #v #tr1 #H >H in He'; #He'
[487]226    @(eval_Ecost … He')
[399]227(* exec_lvalue fails on non-lvalues. *)
[487]228| #e' #ty cases e';
[2468]229    [ 2,4,11: #a #H try @I @(False_ind … H) | 3: #a * | 12,13: #a #b * | 1,5,7,9,10: #a #b #H @I | 6,8: #a #b #c #H @I ]
230    try @I
[487]231] qed.
[399]232
[2176]233lemma addrof_eval_lvalue: ∀ge,en,m,e,loc,off,tr,ty.
234eval_expr ge en m (Expr (Eaddrof e) ty) (Vptr (mk_pointer loc off)) tr →
[498]235eval_lvalue ge en m e loc off tr.
[2176]236#ge #en #m #e #loc #off #tr #ty #H inversion H;
[2468]237[ 1,4: #a #b #c #H @False_ind destruct (H);
[1516]238| #a #b #c #d #e #f #H1 #g #H2 #E1 #E2 #E3 <H2 in H1; #H1 @False_ind
[487]239    @(eval_lvalue_inv_ind … H1)
240    [ #a #b #c #d #bad destruct (bad);
[498]241    | #a #b #c #d #e #bad destruct (bad);
[2176]242    | #a #b #c #d #e #f #bad destruct (bad);
[1672]243    | #a #b #c #d #e #f #g #h #i #j #k #l #bad @False_ind destruct (bad);
244    | #a #b #c #d #e #f #g #h #i #j #bad destruct (bad);
[487]245    ]
[2176]246| #e' #ty' #loc' #ofs' #tr' #H' #e1 #e2 #e3 destruct (e1 e2 e3); #E @H'
[487]247| #a #b #c #d #e #f #g #h #bad destruct (bad);
[1672]248| #a #b #c #d #e #f #g #h #i #j #k #l #bad destruct (bad);
249| #a #b #c #d #e #f #g #h #i #j #k #bad destruct (bad);
250| #a #b #c #d #e #f #g #h #i #j #k #bad destruct (bad);
[2588]251| #a #b #c #d #e #f #g #h #i #bad destruct (bad);
252| #a #b #c #d #e #f #g #h #i #j #k #l #m #n #bad destruct (bad);
253| #a #b #c #d #e #f #g #h #i #bad destruct (bad);
254| #a #b #c #d #e #f #g #h #i #j #k #l #m #n #bad  destruct (bad);
[487]255| #a #b #c #d #e #f #g #h #bad destruct (bad);
[1672]256| #a #b #c #d #e #f #bad destruct (bad);
[487]257] qed.
[399]258
[500]259lemma addrof_exec_lvalue: ∀ge,en,m,e,r,loc,off,tr.
260exec_lvalue ge en m e = OK ? 〈〈mk_block r loc,off〉,tr〉 →
[2176]261exec_expr ge en m (Expr (Eaddrof e) (Tpointer Tvoid)) = OK ? 〈Vptr (mk_pointer (mk_block r loc) off), tr〉.
[1516]262#ge #en #m #e #r #loc #off #tr #H whd in ⊢ (??%?);
263>H whd in ⊢ (??%?); cases r @refl
[487]264qed.
[399]265
[487]266theorem exec_lvalue_sound: ∀ge,en,m,e.
[498]267P_res ? (λr.eval_lvalue ge en m e (\fst (\fst r)) (\snd (\fst r)) (\snd r)) (exec_lvalue ge en m e).
[487]268#ge #en #m #e lapply (refl ? (exec_lvalue ge en m e));
269cases (exec_lvalue ge en m e) in ⊢ (???% → %);
[1516]270[ #x cases x #y cases y #loc #off #tr #H whd cases loc in H ⊢ %; #locr #loci #H
[2176]271    @(addrof_eval_lvalue … (Tpointer Tvoid))
[500]272    lapply (addrof_exec_lvalue … H) #H'
[2176]273    lapply (exec_expr_sound ge en m (Expr (Eaddrof e) (Tpointer Tvoid)))
[487]274    >H' #H'' @H''
[797]275| #msg #_ whd @I
[487]276] qed.
[399]277
278(* Plain equality versions of the above *)
279
[487]280definition exec_expr_sound' ≝ λge,en,m,e,v.
[399]281  λH:exec_expr ge en m e = OK ? v.
282  P_res_to_P ???? (exec_expr_sound ge en m e) H.
283
[498]284definition exec_lvalue_sound' ≝ λge,en,m,e,loc,off,tr.
285  λH:exec_lvalue ge en m e = OK ? 〈〈loc,off〉,tr〉.
[399]286  P_res_to_P ???? (exec_lvalue_sound ge en m e) H.
287
[487]288lemma exec_exprlist_sound: ∀ge,e,m,l. P_res ? (λvltr:list val×trace. eval_exprlist ge e m l (\fst vltr) (\snd vltr)) (exec_exprlist ge e m l).
289#ge #e #m #l elim l;
[1410]290 whd
[487]291[ %
292| #e1 #es #IH
293  @bind2_OK #v #tr1 #Hv
294  @bind2_OK #vs #tr2 #Hvs
295  whd; @eval_Econs
296  [ @(P_res_to_P … (exec_expr_sound ge e m e1) Hv)
297  | @(P_res_to_P … IH Hvs)
298  ]
299] qed.
[399]300
[487]301lemma exec_alloc_variables_sound : ∀l,en,m,en',m'.
302  exec_alloc_variables en m l = 〈en',m'〉 →
303  alloc_variables en m l en' m'.
304#l elim l
305[ #en #m #en' #m' #EXEC whd in EXEC:(??%?); destruct %
306| * #id #ty #t #IH #en #m #en' #m'
[2176]307  lapply (refl ? (alloc m O (sizeof ty) XData)) whd in ⊢ (? → ??%? → ?);
[2106]308  cases (alloc ????) in ⊢ (???% → %); #m'' #b #ALLOC #EXEC
[487]309 @(alloc_variables_cons … ALLOC)
310 @IH @EXEC
311qed.
312
313lemma exec_bind_parameters_sound : ∀ps,vs,en,m.
314  P_res ? (λm'. bind_parameters en m ps vs m') (exec_bind_parameters en m ps vs).
315#ps elim ps
316[ * //
317| * #id #ty #ps' #IH *
318    [ //
319    | #v #vs #en #m
320      @opt_bind_OK #b #GET
321      @opt_bind_OK #m' #STORE
322      lapply (refl ? (exec_bind_parameters en m' ps' vs))
[1516]323      cases (exec_bind_parameters en m' ps' vs) in ⊢ (???% → %); [2: #msg #_ %]
[487]324      #m'' #BIND
325      @(bind_parameters_cons … GET STORE)
[1516]326      lapply (IH vs en m') whd in ⊢ (% → ?); >BIND //
[487]327    ]
328] qed.
329
330lemma check_eventval_list_sound : ∀vs,tys.
331  P_res ? (λevs. eventval_list_match evs tys vs) (check_eventval_list vs tys).
332#vs0 elim vs0
333[ * //
334| #v #vs #IH *
335  [ //
[1516]336  | #ty #tys whd in ⊢ (???%);
[2468]337    cases ty [ #sz #sg | ] cases v //
338    #sz' #v @bind_OK #ev whd in ⊢ (??%? → ?);
339    @eq_intsize_elim #E #CHECKev whd in CHECKev:(??%?); destruct
340    @bind_OK #evs #CHECKevs
[961]341      @(evl_match_cons ??????? (P_res_to_P ???? (IH ?) CHECKevs))
342      //
[487]343  ]
344] qed.
345
346theorem exec_step_sound: ∀ge,st.
[399]347  P_io ??? (λr. step ge st (\fst r) (\snd r)) (exec_step ge st).
[487]348#ge #st cases st;
349[ #f #s #k #e #m cases s;
350  [ cases k;
351    [ whd in ⊢ (?????%);
352        lapply (refl ? (fn_return f)); cases (fn_return f) in ⊢ (???% → %);
353        //; #H whd;
354        @step_skip_call //;
[1410]355    | #s' #k' whd; //
[2391]356    | #ex #s' #k' @step_skip_or_continue_while % //;
[487]357    | #ex #s' #k'
358        @res_bindIO2_OK #v #tr #Hv
359        letin bexpr ≝ (exec_bool_of_val v (typeof ex));
360        lapply (refl ? bexpr);
361        cases bexpr in ⊢ (???% → %);
362        [ #b cases b; #eb lapply (exec_bool_of_val_sound … eb); #Hb
363            whd in ⊢ (?????%);
364            [ @(step_skip_or_continue_dowhile_true … (exec_expr_sound' … Hv))
365              [ % // | @(bool_of … Hb) ]
366            | @(step_skip_or_continue_dowhile_false … (exec_expr_sound' … Hv))
367              [ % // | @(bool_of … Hb) ]
368            ]
[797]369        | #msg #_ //;
[487]370        ]
371    | #ex #s1 #s2 #k' @step_skip_or_continue_for2 % //;
372    | #ex #s1 #s2 #k' @step_skip_for3
373    | #k' @step_skip_break_switch % //;
374    | #r #f' #e' #k' whd in ⊢ (?????%);
375        lapply (refl ? (fn_return f)); cases (fn_return f) in ⊢ (???% → %);
376        //; #H whd;
377        @step_skip_call //;
378    ]
379  | #ex1 #ex2
380    @res_bindIO2_OK #x cases x; #y cases y; #pcl #loc #ofs #tr1 #Hlval
381    @res_bindIO2_OK #v2 #tr2 #Hv2
382    @opt_bindIO_OK #m' #em'
383    whd; @(step_assign … (exec_lvalue_sound' … Hlval) (exec_expr_sound' … Hv2) em')
384  | #lex #fex #args
385    @res_bindIO2_OK #vf #tr1 #Hvf0 lapply (exec_expr_sound' … Hvf0); #Hvf
386    @res_bindIO2_OK #vargs #tr2 #Hvargs0 lapply (P_res_to_P ???? (exec_exprlist_sound …) Hvargs0); #Hvargs
387    @opt_bindIO_OK #fd #efd
388    @bindIO_OK #ety
389    cases lex; whd;
390    [ @(step_call_none … Hvf Hvargs efd ety)
391    | #lhs'
392        @res_bindIO2_OK #x cases x; #y cases y; #pcl #loc #ofs #tr3 #Hlocofs
393        whd; @(step_call_some … (exec_lvalue_sound' … Hlocofs) Hvf Hvargs efd ety)
394    ]
[1410]395  | #s1 #s2 //
[487]396  | #ex #s1 #s2
397    @res_bindIO2_OK #v #tr #Hv
398    letin bexpr ≝ (exec_bool_of_val v (typeof ex));
399    lapply (refl ? bexpr); cases bexpr in ⊢ (???% → %); //;
400    #b cases b; #eb lapply (exec_bool_of_val_sound … eb); #Hb
401    [ @(step_ifthenelse_true … (exec_expr_sound' … Hv)) @(bool_of … Hb)
402    | @(step_ifthenelse_false … (exec_expr_sound' … Hv)) @(bool_of … Hb)
403    ]
[2391]404  | #ex #s'
[487]405    @res_bindIO2_OK #v #tr #Hv
406    letin bexpr ≝ (exec_bool_of_val v (typeof ex));
407    lapply (refl ? bexpr); cases bexpr in ⊢ (???% → %); //;
408    #b cases b; #eb lapply (exec_bool_of_val_sound … eb); #Hb
409    [ @(step_while_true … (exec_expr_sound' … Hv)) @(bool_of … Hb)
410    | @(step_while_false … (exec_expr_sound' … Hv)) @(bool_of … Hb)
411    ]
[1410]412  | #ex #s' //
[487]413  | #s1 #ex #s2 #s3 whd in ⊢ (?????%); elim (is_Sskip s1); #Hs1 whd in ⊢ (?????%);
414    [ >Hs1
415      @res_bindIO2_OK #v #tr #Hv
416      letin bexpr ≝ (exec_bool_of_val v (typeof ex));
417      lapply (refl ? bexpr); cases bexpr in ⊢ (???% → %); //;
418      #b cases b; #eb lapply (exec_bool_of_val_sound … eb); #Hb
419      [ @(step_for_true … (exec_expr_sound' … Hv)) @(bool_of … Hb)
420      | @(step_for_false … (exec_expr_sound' … Hv)) @(bool_of … Hb)
421      ]
422    | @step_for_start //;
423    ]
[1342]424  | whd in ⊢ (?????%); cases k; // #k' @step_skip_break_switch %2 //
[487]425  | whd in ⊢ (?????%); cases k; //;
[2391]426    [ #ex #s' #k' whd; @step_skip_or_continue_while %2 ; //;
[487]427    | #ex #s' #k' whd;
428      @res_bindIO2_OK #v #tr #Hv
429      letin bexpr ≝ (exec_bool_of_val v (typeof ex));
430      lapply (refl ? bexpr); cases bexpr in ⊢ (???% → %); //;
431      #b cases b; #eb lapply (exec_bool_of_val_sound … eb); #Hb
432      [ @(step_skip_or_continue_dowhile_true … (exec_expr_sound' … Hv))
433        [ %2 ; // | @(bool_of … Hb) ]
434      | @(step_skip_or_continue_dowhile_false … (exec_expr_sound' … Hv))
435        [ %2 ; // | @(bool_of … Hb) ]
436      ]
437    | #ex #s1 #s2 #k' whd; @step_skip_or_continue_for2 %2 ; //
438    ]
439  | #r whd in ⊢ (?????%); cases r;
440    [ whd; lapply (refl ? (fn_return f)); cases (fn_return f) in ⊢ (???% → %); //; #H
441        @step_return_0 @H
442    | #ex cases (type_eq_dec (fn_return f) Tvoid); //; whd in ⊢ (% → ?????%); #Hnotvoid
443        @res_bindIO2_OK #v #tr #Hv
444        whd; @(step_return_1 … Hnotvoid (exec_expr_sound' … Hv))
445    ]
[961]446  | #ex #ls @res_bindIO2_OK * // #sz #n #tr #Hv
[2428]447    lapply (refl ? (typeof ex)) cases (typeof ex) in ⊢ (???% → %); // #sz' #sg #TY
448    whd in ⊢ (?????%); cases (sz_eq_dec sz sz') // #SZ destruct (SZ)
449    whd in ⊢ (?????%); @opt_bindIO_OK #ls' #LS
450    @(step_switch … TY LS) @(exec_expr_sound' … Hv)
[1410]451  | #l #s' //
[487]452  | #l whd in ⊢ (?????%); lapply (refl ? (find_label l (fn_body f) (call_cont k)));
453      cases (find_label l (fn_body f) (call_cont k)) in ⊢ (???% → %); //;
454      #sk cases sk; #s' #k' #H
455      @(step_goto … H)
[1410]456  | #l #s' //
[487]457  ]
458| #f0 #vargs #k #m whd in ⊢ (?????%); cases f0;
[1516]459  [ #fn whd in ⊢ (?????%);
[487]460    lapply (refl ? (exec_alloc_variables empty_env m (fn_params fn@fn_vars fn)))
[1516]461    cases (exec_alloc_variables empty_env m (fn_params fn@fn_vars fn)) in ⊢ (???% → %);
462    #en' #m' #ALLOC whd in ⊢ (?????%);
[487]463    @res_bindIO_OK #m2 #BIND
464    whd; @(step_internal_function … (exec_alloc_variables_sound … ALLOC))
465    @(P_res_to_P … (exec_bind_parameters_sound …) BIND)
[1647]466  | #id #argtys #rty @res_bindIO_OK #evs #Hevs #v'
467    @bindIO_OK #eres whd
[487]468    @step_external_function % [ @(P_res_to_P … (check_eventval_list_sound …) Hevs)
469                              | @mk_val_correct ]
470  ] 
471| #v #k' #m' whd in ⊢ (?????%); cases k'; //;
[1713]472  [ whd in ⊢ (?????%); cases v // * //
473  | #r #f #e #k whd in ⊢ (?????%); cases r //
474    * * #b #ofs #ty
475    @opt_bindIO_OK #m' #em' @step_returnstate_1 whd in em':(??%?); //
476    ]
477| //
[487]478]
479qed.
[399]480
[1244]481lemma make_initial_state_sound : ∀p. P_res ? (initial_state p) (make_initial_state p).
[487]482#p cases p; #fns #main #vars
483whd in ⊢ (???%);
484@bind_OK #m #Em
485@opt_bind_OK #x cases x; #sp #b #esb
486@opt_bind_OK #f #ef
[1244]487@(initial_state_intro … Em esb ef) @refl
[487]488qed.
[399]489
[487]490theorem exec_steps_sound: ∀ge,n,st.
[399]491 P_io ??? (λts:trace×state. star (mk_transrel ?? step) ge st (\fst ts) (\snd ts))
492 (exec_steps n ge st).
[487]493#ge #n elim n;
494[ #st whd in ⊢ (?????%); elim (is_final_state st); #H whd; %
495| #n' #IH #st whd in ⊢ (?????%); elim (is_final_state st); #H
496  [ whd; %
497  | @(P_bindIO2_OK ????????? (exec_step_sound …)) #t #s' cases s';
[1713]498      [ #f #s #k #e #m | #fd #args #k #m | #r #k #m | #r ] normalize
499      [ 1,2,3: cases m; #mc #mn #mp ] #Hstep normalize
[487]500      @(P_bindIO2_OK ????????? (IH …)) #t' #s'' #Hsteps
[1713]501      whd; @(star_step ????????? Hsteps) [ 2,5,8,11: @Hstep | 3,6,9,12: // ]
[487]502  ]
503qed.
[708]504
505lemma is_final_sound: ∀s,r. is_final s = Some ? r → final_state s r.
[1713]506* [ 4: #r #r' normalize #E destruct %
507  | *: normalize #x1 #x2 #x3 #x4 #x5 try #x6 try #x7 destruct
[1350]508  ] qed.
Note: See TracBrowser for help on using the repository browser.