Ignore:
Timestamp:
Sep 21, 2011, 6:08:50 PM (9 years ago)
Author:
campbell
Message:

Sort out Clight semantics equivalence proof for new SmallstepExec?.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecEquiv.ma

    r1216 r1244  
    5959] qed.
    6060
    61 lemma is_final_elim': ∀s.∀P:option int → Type[0].
     61lemma is_final_elim': ∀ge,s.∀P:option int → Type[0].
    6262 (∀r. final_state s r → P (Some ? r)) →
    6363 ((¬∃r.final_state s r) → P (None ?)) →
    64 P (is_final io_out io_in clight_fullexec s).
    65 @is_final_elim qed.
     64P (is_final io_out io_in clight_fullexec ge s).
     65#ge @is_final_elim qed.
    6666
    6767lemma exec_e_step: ∀ge,x,tr,s,e.
     
    10211021whd in ⊢ (? → ? → ?(match % with [_ ⇒ ? | _ ⇒ ?])? → ?)
    10221022cases (make_initial_state p)
    1023 [ #gs cases gs; #ge #s #INITIAL' #INITIAL whd in INITIAL ⊢ (?%? → ?);
    1024     cases INITIAL; #Ege #INITIAL''
     1023[ #s #INITIAL' #INITIAL whd in INITIAL ⊢ (?%? → ?);
    10251024    >exec_inf_aux_unfold
    10261025    whd in ⊢ (?%? → ?)
    10271026    @is_final_elim'
    10281027    [ #r #F @False_ind
    1029         @(absurd ?? (initial_state_not_final … INITIAL''))
     1028        @(absurd ?? (initial_state_not_final … INITIAL))
    10301029        %{r} @F
    10311030    | #NOTFINAL whd in ⊢ (?%? → ?); cases e;
     
    10331032        cases (se_inv … EXEC0); *; #E1 #E2 <E1 <E2 #EXEC'
    10341033    lapply (behavior_of_execution ??
    1035               (execution_characterisation_complete classic constructive_indefinite_description ge s ? EXEC'));
     1034              (execution_characterisation_complete classic constructive_indefinite_description ? s ? EXEC'));
    10361035        *; #b #MATCHES %{b} % [ @MATCHES ]
    1037         #ge' >Ege #Ege' >(?:ge' = ge) [ 2: destruct (Ege') skip (INITIAL Ege EXEC0 EXEC'); // ]
     1036        #ge #Ege
    10381037        inversion MATCHES;
    10391038        [ #s0 #e1 #tr1 #r #m #TERM #EXEC #BEHAVES <EXEC in TERM
     
    10421041            >E1 in TERM #TERM
    10431042            @(program_terminates (mk_transrel … step) ?? ge s)
    1044             [ 2: @INITIAL''
    1045             | 3: @(terminates_sound … TERM EXEC')
     1043            [ 2: @INITIAL
     1044            | 3: <Ege @(terminates_sound … TERM EXEC')
    10461045            | skip
    10471046            | //;
     
    10551054            #E7 <E7 in INITSTEPS #INITSTEPS
    10561055            cases (several_steps … INITSTEPS EXEC'); #INITSTAR #EXECDIV
    1057             @(program_diverges (mk_transrel … step) ?? ge s … INITIAL'' INITSTAR)
    1058             @(silent_sound … DIVERGING EXECDIV)
     1056            @(program_diverges (mk_transrel … step) ?? ge s … INITIAL)
     1057            [ 2: <Ege @INITSTAR
     1058            | 3: <Ege @(silent_sound … DIVERGING EXECDIV)
     1059            ]
    10591060        | #s0 #e #tr #REACTS #EXEC #E2 <EXEC in REACTS #REACTS
    10601061            lapply (exec_state_reacts … REACTS);
     
    10641065            cut (e0 = e''); [ destruct (E6) skip (MATCHES EXEC0 EXEC'); // ]
    10651066            #E7 <E7 in REACTING #REACTING
    1066             @(program_reacts (mk_transrel … step) ?? ge s … INITIAL'')
    1067             @(reacts_sound … REACTING EXEC')
     1067            @(program_reacts (mk_transrel … step) ?? ge s … INITIAL)
     1068            <Ege @(reacts_sound … REACTING EXEC')
    10681069        | #e #s1 #s2 #tr #WRONG #EXEC #E2 <EXEC in WRONG #WRONG
    10691070            lapply (exec_state_wrong … WRONG);
     
    10741075            #E8 <E8 in GOESWRONG #GOESWRONG
    10751076            elim (wrong_sound … WRONG EXEC' NOTFINAL); *; #STAR #STOP #FINAL
    1076             @(program_goes_wrong (mk_transrel … step) ?? ge s … INITIAL'' STAR STOP)
     1077            <Ege
     1078            @(program_goes_wrong (mk_transrel … step) ?? ? s … INITIAL STAR STOP)
    10771079            #r % #F @(absurd ?? FINAL) %{r} @F
    10781080        | #msg #E destruct (E);
Note: See TracChangeset for help on using the changeset viewer.