Changeset 252


Ignore:
Timestamp:
Nov 22, 2010, 2:40:28 PM (9 years ago)
Author:
campbell
Message:

Separate out soundness of exec_step from definition.

Location:
C-semantics
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/CexecIO.ma

    r251 r252  
    836836    store_value_of_type ty m pcl loc ofs v ] ].
    837837
    838 nlet rec exec_step (ge:genv) (st:state) on st : (IO eventval io_out (Σr:trace × state. step ge st (\fst r) (\snd r))) ≝
     838nlet rec exec_step (ge:genv) (st:state) on st : (IO eventval io_out (trace × state)) ≝
    839839match st with
    840840[ State f s k e m ⇒
    841841  match s with
    842   [ Sassign a1 a2 ⇒ Some ? (
     842  [ Sassign a1 a2 ⇒
    843843    ! 〈l,tr1〉 ← exec_lvalue ge e m a1;
    844844    ! 〈v2,tr2〉 ← exec_expr ge e m a2;
    845845    ! m' ← store_value_of_type' (typeof a1) m l v2;
    846     ret ? 〈tr1⧺tr2, State f Sskip k e m'〉)
    847   | Scall lhs a al ⇒ Some ? (
     846    ret ? 〈tr1⧺tr2, State f Sskip k e m'〉
     847  | Scall lhs a al ⇒
    848848    ! 〈vf,tr2〉 ← exec_expr ge e m a;
    849849    ! 〈vargs,tr3〉 ← exec_exprlist ge e m al;
     
    864864           ! 〈locofs,tr1〉 ← exec_lvalue ge e m lhs';
    865865           ret ? 〈tr1⧺tr2⧺tr3, Callstate fd vargs (Kcall (Some ? 〈locofs, typeof lhs'〉) f e k) m〉
    866          ])
    867   | Ssequence s1 s2 ⇒ Some ? (ret ? 〈E0, State f s1 (Kseq s2 k) e m〉)
     866         ]
     867  | Ssequence s1 s2 ⇒ ret ? 〈E0, State f s1 (Kseq s2 k) e m〉
    868868  | Sskip ⇒
    869869      match k with
    870       [ Kseq s k' ⇒ Some ? (ret ? 〈E0, State  f s k' e m〉)
     870      [ Kseq s k' ⇒ ret ? 〈E0, State  f s k' e m〉
    871871      | Kstop ⇒
    872872          match fn_return f with
    873           [ Tvoid ⇒ Some ? (ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉)
    874           | _ ⇒ Some ? (Wrong ???)
     873          [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉
     874          | _ ⇒ Wrong ???
    875875          ]
    876876      | Kcall _ _ _ _ ⇒
    877877          match fn_return f with
    878           [ Tvoid ⇒ Some ? (ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉)
    879           | _ ⇒ Some ? (Wrong ???)
     878          [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉
     879          | _ ⇒ Wrong ???
    880880          ]
    881       | Kwhile a s' k' ⇒ Some ? (ret ? 〈E0, State f (Swhile a s') k' e m〉)
    882       | Kdowhile a s' k' ⇒ Some ? (
     881      | Kwhile a s' k' ⇒ ret ? 〈E0, State f (Swhile a s') k' e m〉
     882      | Kdowhile a s' k' ⇒
    883883          ! 〈v,tr〉 ← exec_expr ge e m a;
    884884          ! b ← err_to_io … (exec_bool_of_val v (typeof a));
     
    886886          [ true ⇒ ret ? 〈tr, State f (Sdowhile a s') k' e m〉
    887887          | false ⇒ ret ? 〈tr, State f Sskip k' e m〉
    888           ])
    889       | Kfor2 a2 a3 s' k' ⇒ Some ? (ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉)
    890       | Kfor3 a2 a3 s' k' ⇒ Some ? (ret ? 〈E0, State f (Sfor Sskip a2 a3 s') k' e m〉)
    891       | Kswitch k' ⇒ Some ? (ret ? 〈E0, State f Sskip k' e m〉)
    892       | _ ⇒ Some ? (Wrong ???)
     888          ]
     889      | Kfor2 a2 a3 s' k' ⇒ ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉
     890      | Kfor3 a2 a3 s' k' ⇒ ret ? 〈E0, State f (Sfor Sskip a2 a3 s') k' e m〉
     891      | Kswitch k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
     892      | _ ⇒ Wrong ???
    893893      ]
    894894  | Scontinue ⇒
    895895      match k with
    896       [ Kseq s' k' ⇒ Some ? (ret ? 〈E0, State f Scontinue k' e m〉)
    897       | Kwhile a s' k' ⇒ Some ? (ret ? 〈E0, State f (Swhile a s') k' e m〉)
    898       | Kdowhile a s' k' ⇒ Some ? (
     896      [ Kseq s' k' ⇒ ret ? 〈E0, State f Scontinue k' e m〉
     897      | Kwhile a s' k' ⇒ ret ? 〈E0, State f (Swhile a s') k' e m〉
     898      | Kdowhile a s' k' ⇒
    899899          ! 〈v,tr〉 ← exec_expr ge e m a;
    900900          ! b ← err_to_io … (exec_bool_of_val v (typeof a));
     
    902902          [ true ⇒ ret ? 〈tr, State f (Sdowhile a s') k' e m〉
    903903          | false ⇒ ret ? 〈tr, State f Sskip k' e m〉
    904           ])
    905       | Kfor2 a2 a3 s' k' ⇒ Some ? (ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉)
    906       | Kswitch k' ⇒ Some ? (ret ? 〈E0, State f Scontinue k' e m〉)
    907       | _ ⇒ Some ? (Wrong ???)
     904          ]
     905      | Kfor2 a2 a3 s' k' ⇒ ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉
     906      | Kswitch k' ⇒ ret ? 〈E0, State f Scontinue k' e m〉
     907      | _ ⇒ Wrong ???
    908908      ]
    909909  | Sbreak ⇒
    910910      match k with
    911       [ Kseq s' k' ⇒ Some ? (ret ? 〈E0, State f Sbreak k' e m〉)
    912       | Kwhile a s' k' ⇒ Some ? (ret ? 〈E0, State f Sskip k' e m〉)
    913       | Kdowhile a s' k' ⇒ Some ? (ret ? 〈E0, State f Sskip k' e m〉)
    914       | Kfor2 a2 a3 s' k' ⇒ Some ? (ret ? 〈E0, State f Sskip k' e m〉)
    915       | Kswitch k' ⇒ Some ? (ret ? 〈E0, State f Sskip k' e m〉)
    916       | _ ⇒ Some ? (Wrong ???)
     911      [ Kseq s' k' ⇒ ret ? 〈E0, State f Sbreak k' e m〉
     912      | Kwhile a s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
     913      | Kdowhile a s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
     914      | Kfor2 a2 a3 s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
     915      | Kswitch k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
     916      | _ ⇒ Wrong ???
    917917      ]
    918   | Sifthenelse a s1 s2 ⇒ Some ? (
     918  | Sifthenelse a s1 s2 ⇒
    919919      ! 〈v,tr〉 ← exec_expr ge e m a;
    920920      ! b ← err_to_io … (exec_bool_of_val v (typeof a));
    921       ret ? 〈tr, State f (if b then s1 else s2) k e m〉)
    922   | Swhile a s' ⇒ Some ? (
     921      ret ? 〈tr, State f (if b then s1 else s2) k e m〉
     922  | Swhile a s' ⇒
    923923      ! 〈v,tr〉 ← exec_expr ge e m a;
    924924      ! b ← err_to_io … (exec_bool_of_val v (typeof a));
    925925      ret ? 〈tr, if b then State f s' (Kwhile a s' k) e m
    926                       else State f Sskip k e m〉)
    927   | Sdowhile a s' ⇒ Some ? (ret ? 〈E0, State f s' (Kdowhile a s' k) e m〉)
     926                      else State f Sskip k e m〉
     927  | Sdowhile a s' ⇒ ret ? 〈E0, State f s' (Kdowhile a s' k) e m〉
    928928  | Sfor a1 a2 a3 s' ⇒
    929929      match is_Sskip a1 with
    930       [ inl _ ⇒ Some ? (
     930      [ inl _ ⇒
    931931          ! 〈v,tr〉 ← exec_expr ge e m a2;
    932932          ! b ← err_to_io … (exec_bool_of_val v (typeof a2));
    933           ret ? 〈tr, State f (if b then s' else Sskip) (if b then (Kfor2 a2 a3 s' k) else k) e m〉)
    934       | inr _ ⇒ Some ? (ret ? 〈E0, State f a1 (Kseq (Sfor Sskip a2 a3 s') k) e m〉)
     933          ret ? 〈tr, State f (if b then s' else Sskip) (if b then (Kfor2 a2 a3 s' k) else k) e m〉
     934      | inr _ ⇒ ret ? 〈E0, State f a1 (Kseq (Sfor Sskip a2 a3 s') k) e m〉
    935935      ]
    936936  | Sreturn a_opt ⇒
    937937    match a_opt with
    938938    [ None ⇒ match fn_return f with
    939       [ Tvoid ⇒ Some ? (ret ? 〈E0, Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e))〉)
    940       | _ ⇒ Some ? (Wrong ???)
     939      [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e))〉
     940      | _ ⇒ Wrong ???
    941941      ]
    942     | Some a ⇒ Some ? (
     942    | Some a ⇒
    943943        ! u ← err_to_io_sig … (is_not_void (fn_return f));
    944944        ! 〈v,tr〉 ← exec_expr ge e m a;
    945         ret ? 〈tr, Returnstate v (call_cont k) (free_list m (blocks_of_env e))〉)
     945        ret ? 〈tr, Returnstate v (call_cont k) (free_list m (blocks_of_env e))〉
    946946    ]
    947   | Sswitch a sl ⇒ Some ? (
     947  | Sswitch a sl ⇒
    948948      ! 〈v,tr〉 ← exec_expr ge e m a;
    949949      match v with [ Vint n ⇒ ret ? 〈tr, State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch k) e m〉
    950                    | _ ⇒ Wrong ??? ])
    951   | Slabel lbl s' ⇒ Some ? (ret ? 〈E0, State f s' k e m〉)
     950                   | _ ⇒ Wrong ??? ]
     951  | Slabel lbl s' ⇒ ret ? 〈E0, State f s' k e m〉
    952952  | Sgoto lbl ⇒
    953953      match find_label lbl (fn_body f) (call_cont k) with
    954       [ Some sk' ⇒ match sk' with [ mk_pair s' k' ⇒ Some ? (ret ? 〈E0, State f s' k' e m〉) ]
    955       | None ⇒ Some ? (Wrong ???)
     954      [ Some sk' ⇒ match sk' with [ mk_pair s' k' ⇒ ret ? 〈E0, State f s' k' e m〉 ]
     955      | None ⇒ Wrong ???
    956956      ]
    957   | Scost lbl s' ⇒ Some ? (ret ? 〈Echarge lbl, State f s' k e m〉)
     957  | Scost lbl s' ⇒ ret ? 〈Echarge lbl, State f s' k e m〉
    958958  ]
    959959| Callstate f0 vargs k m ⇒
    960960  match f0 with
    961   [ Internal f ⇒ Some ? (
     961  [ Internal f ⇒
    962962    match exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) with [ mk_pair e m1 ⇒
    963963      ! m2 ← err_to_io_sig … (exec_bind_parameters e m1 (fn_params f) vargs);
    964964      ret ? 〈E0, State f (fn_body f) k e m2〉
    965     ])
    966   | External f argtys retty ⇒ Some ? (
     965    ]
     966  | External f argtys retty ⇒
    967967      ! evargs ← err_to_io_sig … (check_eventval_list vargs (typlist_of_typelist argtys));
    968968      ! evres ← do_io f evargs;
    969969      ! vres ← err_to_io_sig … (check_eventval evres (proj_sig_res (signature_of_type argtys retty)));
    970       ret ? 〈(Eextcall f evargs evres), Returnstate vres k m〉)
     970      ret ? 〈(Eextcall f evargs evres), Returnstate vres k m〉
    971971  ]
    972972| Returnstate res k m ⇒
     
    976976    [ None ⇒
    977977      match res with
    978       [ Vundef ⇒ Some ? (ret ? 〈E0, (State f Sskip k' e m)〉)
    979       | _ ⇒ Some ? (Wrong ???)
     978      [ Vundef ⇒ ret ? 〈E0, (State f Sskip k' e m)〉
     979      | _ ⇒ Wrong ???
    980980      ]
    981981    | Some r' ⇒
    982982      match r' with [ mk_pair l ty ⇒
    983         Some ? (
     983       
    984984          ! m' ← store_value_of_type' ty m l res;
    985           ret ? 〈E0, (State f Sskip k' e m')〉)
     985          ret ? 〈E0, (State f Sskip k' e m')〉
    986986      ]
    987987    ]
    988   | _ ⇒ Some ? (Wrong ???)
     988  | _ ⇒ Wrong ???
    989989  ]
    990 ]. nwhd; //;
    991 ##[ nrewrite > c7; napply step_skip_call; //; napply c8;
    992 ##| napply step_skip_or_continue_while; @; //;
    993 ##| napply res_bindIO2_OK; #v tr Hv;
    994     nletin bexpr ≝ (exec_bool_of_val v (typeof c7));
    995     nlapply (refl ? bexpr);
    996     ncases bexpr in ⊢ (???% → %);
    997     ##[ #b; ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb;
    998         nwhd in ⊢ (?????%);
    999         ##[ napply (step_skip_or_continue_dowhile_true … (exec_expr_sound' … Hv));
    1000           ##[ @; // ##| napply (bool_of … Hb); ##]
    1001         ##| napply (step_skip_or_continue_dowhile_false … (exec_expr_sound' … Hv));
    1002           ##[ @; // ##| napply (bool_of … Hb); ##]
     990].
     991
     992ntheorem exec_step_sound: ∀ge,st.
     993  P_io ??? (λr. step ge st (\fst r) (\snd r)) (exec_step ge st).
     994#ge st; ncases st;
     995##[ #f s k e m; ncases s;
     996  ##[ ncases k;
     997    ##[ nwhd in ⊢ (?????%);
     998        nlapply (refl ? (fn_return f)); ncases (fn_return f) in ⊢ (???% → %);
     999        //; #H; nwhd;
     1000        napply step_skip_call; //;
     1001    ##| #s' k'; nwhd; //;
     1002    ##| #ex s' k'; napply step_skip_or_continue_while; @; //;
     1003    ##| #ex s' k';
     1004        napply res_bindIO2_OK; #v tr Hv;
     1005        nletin bexpr ≝ (exec_bool_of_val v (typeof ex));
     1006        nlapply (refl ? bexpr);
     1007        ncases bexpr in ⊢ (???% → %);
     1008        ##[ #b; ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb;
     1009            nwhd in ⊢ (?????%);
     1010            ##[ napply (step_skip_or_continue_dowhile_true … (exec_expr_sound' … Hv));
     1011              ##[ @; // ##| napply (bool_of … Hb); ##]
     1012            ##| napply (step_skip_or_continue_dowhile_false … (exec_expr_sound' … Hv));
     1013              ##[ @; // ##| napply (bool_of … Hb); ##]
     1014            ##]
     1015        ##| #_; //;
    10031016        ##]
    1004     ##| #_; //;
    1005     ##]
    1006 ##| napply step_skip_or_continue_for2; @; //;
    1007 ##| napply step_skip_break_switch; @; //;
    1008 ##| nrewrite > c11; napply step_skip_call; //; napply c12;
    1009 ##| napply res_bindIO2_OK; #x; ncases x; #y; ncases y; #pcl loc ofs tr1 Hlval;
     1017    ##| #ex s1 s2 k'; napply step_skip_or_continue_for2; @; //;
     1018    ##| #ex s1 s2 k'; napply step_skip_for3;
     1019    ##| #k'; napply step_skip_break_switch; @; //;
     1020    ##| #r f' e' k'; nwhd in ⊢ (?????%);
     1021        nlapply (refl ? (fn_return f)); ncases (fn_return f) in ⊢ (???% → %);
     1022        //; #H; nwhd;
     1023        napply step_skip_call; //;
     1024    ##]
     1025  ##| #ex1 ex2;
     1026    napply res_bindIO2_OK; #x; ncases x; #y; ncases y; #pcl loc ofs tr1 Hlval;
    10101027    napply res_bindIO2_OK; #v2 tr2 Hv2;
    10111028    napply opt_bindIO_OK; #m' em';
    10121029    nwhd; napply (step_assign … (exec_lvalue_sound' … Hlval) (exec_expr_sound' … Hv2) em');
    1013 ##| napply res_bindIO2_OK; #vf tr1 Hvf0; nlapply (exec_expr_sound' … Hvf0); #Hvf;
     1030  ##| #lex fex args;
     1031    napply res_bindIO2_OK; #vf tr1 Hvf0; nlapply (exec_expr_sound' … Hvf0); #Hvf;
    10141032    napply res_bindIO2_OK; #vargs tr2 Hvargs0; nlapply (P_res_to_P ???? (exec_exprlist_sound …) Hvargs0); #Hvargs;
    10151033    napply opt_bindIO_OK; #fd efd;
    10161034    napply bindIO_OK; #ety;
    1017     ncases c6; nwhd;
     1035    ncases lex; nwhd;
    10181036    ##[ napply (step_call_none … Hvf Hvargs efd ety);
    10191037    ##| #lhs';
     
    10211039        nwhd; napply (step_call_some … (exec_lvalue_sound' … Hlocofs) Hvf Hvargs efd ety);
    10221040    ##]
    1023 ##| napply res_bindIO2_OK; #v tr Hv;
    1024     nletin bexpr ≝ (exec_bool_of_val v (typeof c6));
     1041  ##| #s1 s2; nwhd; //;
     1042  ##| #ex s1 s2;
     1043    napply res_bindIO2_OK; #v tr Hv;
     1044    nletin bexpr ≝ (exec_bool_of_val v (typeof ex));
    10251045    nlapply (refl ? bexpr); ncases bexpr in ⊢ (???% → %); //;
    10261046    #b; ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb;
     
    10281048    ##| napply (step_ifthenelse_false … (exec_expr_sound' … Hv)); napply (bool_of … Hb)
    10291049    ##]
    1030 ##| napply res_bindIO2_OK; #v tr Hv;
    1031     nletin bexpr ≝ (exec_bool_of_val v (typeof c6));
     1050  ##| #ex s';
     1051    napply res_bindIO2_OK; #v tr Hv;
     1052    nletin bexpr ≝ (exec_bool_of_val v (typeof ex));
    10321053    nlapply (refl ? bexpr); ncases bexpr in ⊢ (???% → %); //;
    10331054    #b; ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb;
     
    10351056    ##| napply (step_while_false … (exec_expr_sound' … Hv)); napply (bool_of … Hb);
    10361057    ##]
    1037 ##| nrewrite > c11;
    1038     napply res_bindIO2_OK; #v tr Hv;
    1039     nletin bexpr ≝ (exec_bool_of_val v (typeof c7));
    1040     nlapply (refl ? bexpr); ncases bexpr in ⊢ (???% → %); //;
    1041     #b; ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb;
    1042     ##[ napply (step_for_true … (exec_expr_sound' … Hv)); napply (bool_of … Hb);
    1043     ##| napply (step_for_false … (exec_expr_sound' … Hv)); napply (bool_of … Hb);
    1044     ##]
    1045 ##| napply step_for_start; //;
    1046 ##| napply step_skip_break_switch; @2; //;
    1047 ##| napply step_skip_or_continue_while; @2; //;
    1048 ##| napply res_bindIO2_OK; #v tr Hv;
    1049     nletin bexpr ≝ (exec_bool_of_val v (typeof c7));
    1050     nlapply (refl ? bexpr); ncases bexpr in ⊢ (???% → %); //;
    1051     #b; ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb;
    1052     ##[ napply (step_skip_or_continue_dowhile_true … (exec_expr_sound' … Hv));
    1053       ##[ @2; // ##| napply (bool_of … Hb); ##]
    1054     ##| napply (step_skip_or_continue_dowhile_false … (exec_expr_sound' … Hv));
    1055       ##[ @2; // ##| napply (bool_of … Hb); ##]
    1056     ##]
    1057 ##| napply step_skip_or_continue_for2; @2; //
    1058 ##| napply step_return_0; napply c9;
    1059 ##| napply sig_bindIO_OK; #u Hnotvoid;
    1060     napply res_bindIO2_OK; #v tr Hv;
    1061     nwhd; napply (step_return_1 … Hnotvoid (exec_expr_sound' … Hv));
    1062 ##| napply res_bindIO2_OK; #v; ncases v; //; #n tr Hv;
     1058  ##| #ex s'; nwhd; //;
     1059  ##| #s1 ex s2 s3; nwhd in ⊢ (?????%); nelim (is_Sskip s1); #Hs1; nwhd in ⊢ (?????%);
     1060    ##[ nrewrite > Hs1;
     1061      napply res_bindIO2_OK; #v tr Hv;
     1062      nletin bexpr ≝ (exec_bool_of_val v (typeof ex));
     1063      nlapply (refl ? bexpr); ncases bexpr in ⊢ (???% → %); //;
     1064      #b; ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb;
     1065      ##[ napply (step_for_true … (exec_expr_sound' … Hv)); napply (bool_of … Hb);
     1066      ##| napply (step_for_false … (exec_expr_sound' … Hv)); napply (bool_of … Hb);
     1067      ##]
     1068    ##| napply step_for_start; //;
     1069    ##]
     1070  ##| nwhd in ⊢ (?????%); ncases k; //;
     1071    ##[ #s' k'; nwhd; //;
     1072    ##| #ex s' k'; nwhd; //;
     1073    ##| #ex s' k'; nwhd; //;
     1074    ##| #ex s1 s2 k'; nwhd; //;
     1075    ##| #k'; napply step_skip_break_switch; @2; //;
     1076    ##]
     1077  ##| nwhd in ⊢ (?????%); ncases k; //;
     1078    ##[ #s' k'; nwhd; //;
     1079    ##| #ex s' k'; nwhd; napply step_skip_or_continue_while; @2; //;
     1080    ##| #ex s' k'; nwhd;
     1081      napply res_bindIO2_OK; #v tr Hv;
     1082      nletin bexpr ≝ (exec_bool_of_val v (typeof ex));
     1083      nlapply (refl ? bexpr); ncases bexpr in ⊢ (???% → %); //;
     1084      #b; ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb;
     1085      ##[ napply (step_skip_or_continue_dowhile_true … (exec_expr_sound' … Hv));
     1086        ##[ @2; // ##| napply (bool_of … Hb); ##]
     1087      ##| napply (step_skip_or_continue_dowhile_false … (exec_expr_sound' … Hv));
     1088        ##[ @2; // ##| napply (bool_of … Hb); ##]
     1089      ##]
     1090    ##| #ex s1 s2 k'; nwhd; napply step_skip_or_continue_for2; @2; //
     1091    ##| #k'; nwhd; //;
     1092    ##]
     1093  ##| #r; nwhd in ⊢ (?????%); ncases r;
     1094    ##[ nwhd; nlapply (refl ? (fn_return f)); ncases (fn_return f) in ⊢ (???% → %); //; #H;
     1095        napply step_return_0; napply H;
     1096    ##| #ex; napply sig_bindIO_OK; #u Hnotvoid;
     1097        napply res_bindIO2_OK; #v tr Hv;
     1098        nwhd; napply (step_return_1 … Hnotvoid (exec_expr_sound' … Hv));
     1099    ##]
     1100  ##| #ex ls; napply res_bindIO2_OK; #v; ncases v; //; #n tr Hv;
    10631101    napply step_switch; napply (exec_expr_sound' … Hv);
    1064 ##| napply step_goto; nrewrite < c12; napply c9;
    1065 ##| napply extract_subset_pair_io; #e m1 ealloc Halloc;
     1102  ##| #l s'; nwhd; //;
     1103  ##| #l; nwhd in ⊢ (?????%); nlapply (refl ? (find_label l (fn_body f) (call_cont k)));
     1104      ncases (find_label l (fn_body f) (call_cont k)) in ⊢ (???% → %); //;
     1105      #sk; ncases sk; #s' k' H;
     1106      napply (step_goto … H);
     1107  ##| #l s'; nwhd; //;
     1108  ##]
     1109##| #f0 vargs k m; nwhd in ⊢ (?????%); ncases f0;
     1110  ##[ #fn;
     1111    napply extract_subset_pair_io; #e m1 ealloc Halloc;
    10661112    napply sig_bindIO_OK; #m2 Hbind;
    10671113    nwhd; napply (step_internal_function … Halloc Hbind);
    1068 ##| napply sig_bindIO_OK; #evs Hevs;
     1114  ##| #id argtys rty; napply sig_bindIO_OK; #evs Hevs;
    10691115    napply bindIO_OK; #eres;
    10701116    napply sig_bindIO_OK; #res Hres;
    1071     nwhd; napply step_external_function; @; ##[ napply Hevs; ##| napply Hres; ##] 
    1072 ##| ncases c11; #x; ncases x; #pcl b ofs;
     1117    nwhd; napply step_external_function; @; ##[ napply Hevs; ##| napply Hres; ##]
     1118  ##] 
     1119##| #v k' m'; nwhd in ⊢ (?????%); ncases k'; //;
     1120    #r f e k; nwhd in ⊢ (?????%); ncases r;
     1121  ##[ ncases v; nwhd; //;
     1122  ##| #x; ncases x; #y; ncases y; #z; ncases z; #pcl b ofs ty;
    10731123    napply opt_bindIO_OK; #m' em'; napply step_returnstate_1; nwhd in em':(??%?); //;
     1124  ##]
    10741125##]
    10751126nqed.
     
    11121163
    11131164nlet rec exec_steps (n:nat) (ge:genv) (s:state) :
    1114  IO eventval io_out (Σts:trace×state. star (mk_transrel ?? step) ge s (\fst ts) (\snd ts)) ≝
     1165 IO eventval io_out (trace×state) ≝
    11151166match is_final_state s with
    1116 [ inl _ ⇒ Some ? (ret ? 〈E0, s〉)
     1167[ inl _ ⇒ ret ? 〈E0, s〉
    11171168| inr _ ⇒
    11181169  match n with
    1119   [ O ⇒ Some ? (ret ? 〈E0, s〉)
    1120   | S n' ⇒ Some ? (
     1170  [ O ⇒ ret ? 〈E0, s〉
     1171  | S n' ⇒
    11211172      ! 〈t,s'〉 ← exec_step ge s;
    11221173(*      ! 〈t,s'〉 ← match s with
     
    11311182                 ] ;
    11321183(*      ! 〈t',s''〉 ← exec_steps n' ge s';*)
    1133       ret ? 〈t ⧺ t',s''〉)
     1184      ret ? 〈t ⧺ t',s''〉
    11341185  ]
    1135 ]. nwhd; /2/;
    1136 napply sig_bindIO2_OK; #t s'; ncases s'; ##[ #f st k e m; ##| #fd args k m; ##| #r k m; ##]
    1137 nwhd in ⊢ (? → ?????(??????%?));
    1138 ncases m; #mc mn mp; #H1;
    1139 nwhd in ⊢ (?????(??????%?));
    1140 napply sig_bindIO2_OK; #t' s'' IH;
    1141 nwhd; napply (star_step … IH); //;
     1186].
     1187
     1188ntheorem exec_steps_sound: ∀ge,n,st.
     1189 P_io ??? (λts:trace×state. star (mk_transrel ?? step) ge st (\fst ts) (\snd ts))
     1190 (exec_steps n ge st).
     1191#ge n; nelim n;
     1192##[ #st; nwhd in ⊢ (?????%); nelim (is_final_state st); #H; nwhd; //;
     1193##| #n' IH st; nwhd in ⊢ (?????%); nelim (is_final_state st); #H;
     1194  ##[ nwhd; //;
     1195  ##| napply (P_bindIO2_OK ????????? (exec_step_sound …)); #t s'; ncases s';
     1196      ##[ #f s k e m; ##| #fd args k m; ##| #r k m; ##]
     1197      nwhd in ⊢ (? → ?????(??????%?));
     1198      ncases m; #mc mn mp; #Hstep;
     1199      nwhd in ⊢ (?????(??????%?));
     1200      napply (P_bindIO2_OK ????????? (IH …)); #t' s'' Hsteps;
     1201      nwhd; napply (star_step ????????? Hsteps); ##[ ##2,5,8: napply Hstep; ##| ##3,6,9: // ##]
     1202  ##]
    11421203nqed.
    11431204(*
     
    12651326##| *; #s2; *; #e2; *; #H2 EXEC2;
    12661327    napply (forever_silent_intro (mk_transrel ?? step) … ge s s2 ? (silent_sound ge s2 (e_step E0 s2 e2) ??));
    1267     ncut (∃p.exec_step ge s = Value ??? (sig_intro ?? 〈E0,s2〉 p));
     1328    ncut (exec_step ge s = Value ??? 〈E0,s2〉);
    12681329    ##[ ##1,3,5: nrewrite > (exec_inf_aux_unfold …) in EXEC2; nelim (exec_step ge s);
    12691330      ##[ ##1,4,7: #o k IH EXEC2; nwhd in EXEC2:(??%?); ndestruct;
    1270       ##| ##2,5,8: #x; ncases x; #y; ncases y; #tr' s' p; nwhd in ⊢ (??%? → ?);
     1331      ##| ##2,5,8: #x; ncases x; #tr s'; nwhd in ⊢ (??%? → ?);
    12711332          ncases (is_final_state s'); #p' EXEC2; nwhd in EXEC2:(??%?); ndestruct;
    1272           @ p; napply refl;
     1333          napply refl;
    12731334      ##| ##3,6,9: #EXEC2; nwhd in EXEC2:(??%?); ndestruct
    12741335      ##]
    1275     ##| *; #p EXEC1; napply p
    1276     ##| *; #p EXEC1; nrewrite > EXEC1 in EXEC2; #EXEC2; nwhd in EXEC2:(??(??%)?); napply EXEC2;
    1277     ##| *; #p EXEC1; @; napply H2;
     1336    ##| #EXEC1; nlapply (exec_step_sound ge s); nrewrite > EXEC1; nwhd in ⊢ (% → %); //
     1337    ##| #EXEC1; nrewrite > EXEC1 in EXEC2; #EXEC2; napply EXEC2;
     1338    ##| #EXEC1; @; napply H2;
    12781339    ##]
    12791340##]
  • C-semantics/IOMonad.ma

    r251 r252  
    147147##] nqed.
    148148
     149nlemma bindIO2_OK: ∀I,O,A,B,C. ∀P:C → Prop. ∀e:IO I O (A×B). ∀f: A → B → IO I O C.
     150  (∀v1:A.∀v2:B. P_io I O ? P (f v1 v2)) →
     151  P_io I O ? P (bindIO2 I O A B C e f).
     152#I O A B C P e; nelim e;
     153##[ #out k IH; #f H; nwhd; #res; napply IH; //;
     154##| #v; ncases v; #v1 v2 f H; napply H;
     155##| //;
     156##] nqed.
     157
     158nlemma P_bindIO_OK: ∀I,O,A,B. ∀P':A → Prop. ∀P:B → Prop. ∀e:IO I O A. ∀f: A → IO I O B.
     159  P_io … P' e →
     160  (∀v:A. P' v → P_io I O ? P (f v)) →
     161  P_io I O ? P (bindIO I O A B e f).
     162#I O A B P' P e; nelim e;
     163##[ #out k IH f He H; nwhd in He ⊢ %; #res; napply IH; /2/;
     164##| #v f He H; napply H; napply He;
     165##| //;
     166##] nqed.
     167
     168nlemma P_bindIO2_OK: ∀I,O,A,B,C. ∀P':A×B → Prop. ∀P:C → Prop. ∀e:IO I O (A×B). ∀f: A → B → IO I O C.
     169  P_io … P' e →
     170  (∀v1:A.∀v2:B. P' 〈v1,v2〉 → P_io I O ? P (f v1 v2)) →
     171  P_io I O ? P (bindIO2 I O A B C e f).
     172#I O A B C P' P e; nelim e;
     173##[ #out k IH f He H; nwhd in He ⊢ %; #res; napply IH; /2/;
     174##| #v; ncases v; #v1 v2 f He H; napply H; napply He;
     175##| //;
     176##] nqed.
     177
     178
    149179(* TODO: is there a way to prove this without extensionality?
    150180
Note: See TracChangeset for help on using the changeset viewer.