Changeset 245


Ignore:
Timestamp:
Nov 16, 2010, 1:42:32 PM (9 years ago)
Author:
campbell
Message:

Some progress on whole-execution soundness.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/CexecIO.ma

    r239 r245  
    950950λp. exec_inf_aux (globalenv Genv ?? p) (! s ← make_initial_state p; ret ? 〈E0,sig_eject ?? s〉).
    951951
    952 (*
    953 FIXME: unfolding cofixpoints appears to be rather tricky.
    954 
    955952nremark execution_cases: ∀e.
    956953 e = match e with [ e_stop tr r ⇒ e_stop tr r | e_step tr s e ⇒ e_step tr s e
     
    967964| Interact out k' ⇒ e_interact out (λv. exec_inf_aux ge (k' v))
    968965].
    969 #ge s; nrewrite > (execution_cases (exec_inf_aux …));
    970 ncases s; //; napply refl;
    971 
    972 
    973 nlemma exec_inf_aux_wrong: ∀ge,s. exec_inf_aux ge s = e_wrong → s = Wrong ….
    974 #ge s; ncases s;
    975 ##[ #o k EXEC; nrewrite > (execution_cases (exec_inf_aux …)) in EXEC; #EXEC; nnormalize in EXEC;
    976     ndestruct;
    977 ##| #v; ncases v; #tr s'; #EXEC; nrewrite > (execution_cases (exec_inf_aux …)) in EXEC; #EXEC; nnormalize in EXEC;
    978     ncases (is_final_state s');
    979     ndestruct;
    980 *)
     966#ge s; nrewrite > (execution_cases (exec_inf_aux …)); ncases s;
     967##[ #o k
     968##| #x; ncases x; #tr s'; ncases s';
     969  ##[ #fn st k env m
     970  ##| #fd args k mem
     971  ##| #v k mem; (* for final state check *) ncases k;
     972    ##[ ncases v; ##[ ##2,3: #v' ##| ##4: #sp loc off ##]
     973    ##| #s' k' ##| ##3,4: #e s' k' ##| ##5,6: #e s' s'' k' ##| #k' ##| #a b c d ##]
     974  ##]
     975##| ##]
     976nwhd in ⊢ (??%%); //;
     977nqed.
    981978
    982979(* Finite number of steps without interaction. *)
     
    10251022    execution_matches_behavior e (Goes_wrong tr).
    10261023
     1024(* We don't morally need the cut, but the proof I tried without it failed the
     1025   guarded-by-constructors check and it wasn't apparent why. *)
     1026
     1027nlet corec silent_sound ge s e
     1028  (H0:execution_diverging e)
     1029  (EXEC:exec_inf_aux ge (Value ??? 〈E0,s〉) = e)
     1030  : forever_silent (mk_transrel ?? step) … ge s ≝ ?.
     1031ncut (∃s2.∃e2.execution_diverging e2 ∧ exec_inf_aux ge (exec_step ge s) = e_step E0 s2 e2);
     1032##[ ncases H0 in EXEC ⊢ %; #s1 e1 H1;
     1033    nrewrite > (exec_inf_aux_unfold …); nwhd in ⊢ (??%? → ?);
     1034    ncases (is_final_state s); #p EXEC; nwhd in EXEC:(??%?); ndestruct;
     1035    ninversion H1; #s2 e2 H2 EXEC2;
     1036    @ s2; @ e2; @; //;
     1037##| *; #s2; *; #e2; *; #H2 EXEC2;
     1038    napply (forever_silent_intro (mk_transrel ?? step) … ge s s2 ? (silent_sound ge s2 (e_step E0 s2 e2) ??));
     1039    ncut (∃p.exec_step ge s = Value ??? (sig_intro ?? 〈E0,s2〉 p));
     1040    ##[ ##1,3,5: nrewrite > (exec_inf_aux_unfold …) in EXEC2; nelim (exec_step ge s);
     1041      ##[ ##1,4,7: #o k IH EXEC2; nwhd in EXEC2:(??%?); ndestruct;
     1042      ##| ##2,5,8: #x; ncases x; #y; ncases y; #tr' s' p; nwhd in ⊢ (??%? → ?);
     1043          ncases (is_final_state s'); #p' EXEC2; nwhd in EXEC2:(??%?); ndestruct;
     1044          @ p; napply refl;
     1045      ##| ##3,6,9: #EXEC2; nwhd in EXEC2:(??%?); ndestruct
     1046      ##]
     1047    ##| *; #p EXEC1; napply p
     1048    ##| *; #p EXEC1; nrewrite > EXEC1 in EXEC2; #EXEC2; nwhd in EXEC2:(??(??%)?); napply EXEC2;
     1049    ##| *; #p EXEC1; @; napply H2;
     1050    ##]
     1051##]
     1052nqed.
     1053
    10271054(*
    1028 nlemma silent_sound: ∀ge,s,e.
    1029   execution_diverging e →
    1030   exec_inf_aux ge (Value ??? 〈E0,s〉) = e →
    1031   forever_silent (mk_transrel ?? step) … ge s.
    1032 #ge s e H; ncases H; #s1 e1 H' EXEC;
    1033 napply (forever_silent_intro (mk_transrel ?? step) … ge s s1);
    1034 ##[ nrewrite > (execution_cases (exec_inf_aux …)) in EXEC; #EXEC;
    1035     nnormalize in EXEC;
    1036  nnormalize in match exec_inf_aux in EXEC:(??%?);
    1037 
    10381055ntheorem exec_inf_sound: ∀p. ∃b.execution_matches_behavior (exec_inf p) b ∧ exec_program p b.
    10391056*)
Note: See TracChangeset for help on using the changeset viewer.