Changeset 1244


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

Sort out Clight semantics equivalence proof for new SmallstepExec?.

Location:
src/Clight
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Cexec.ma

    r1231 r1244  
    499499axiom MainMissing : String.
    500500
    501 let rec make_global (p:clight_program) : genv ≝
    502   globalenv Genv ?? (fst ??) p.
     501definition make_global : clight_program → genv ≝
     502λp. globalenv Genv ?? (fst ??) p.
    503503
    504504let rec make_initial_state (p:clight_program) : res state ≝
  • src/Clight/CexecComplete.ma

    r1058 r1244  
    8181
    8282theorem the_initial_state:
    83   ∀p,s. initial_state p s → ∃ge. yields ? (make_initial_state p) 〈ge,s〉.
    84 #p #s cases p; #fns #main #globs #H
     83  ∀p,s. initial_state p s → yields ? (make_initial_state p) s.
     84#p #s cases p; #globs #fns #main #H
    8585inversion H;
    86 #b #f #ge #m #e1 #e2 #e3 #e4 #e5 %{ge}
    87 whd in ⊢ (??%?);
    88 >e1
     86#b #f #ge #m #e1 #e2 #e3 #e4 #e5
    8987whd in ⊢ (??%?);
    9088>e2
    9189whd in ⊢ (??%?);
     90change in e1:(??%?) with (make_global (mk_program ?? globs fns main))
     91>e1
    9292>e3
    9393whd in ⊢ (??%?);
  • 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);
  • src/Clight/CexecSound.ma

    r1224 r1244  
    533533qed.
    534534
    535 lemma make_initial_state_sound : ∀p. P_res ? (λgs.globalenv Genv ?? (fst ??) p = OK ? (\fst gs) ∧ initial_state p (\snd gs)) (make_initial_state p).
     535lemma make_initial_state_sound : ∀p. P_res ? (initial_state p) (make_initial_state p).
    536536#p cases p; #fns #main #vars
    537537whd in ⊢ (???%);
    538 @bind_OK #ge #Ege
    539538@bind_OK #m #Em
    540539@opt_bind_OK #x cases x; #sp #b #esb
    541540@opt_bind_OK #f #ef
    542 whd; % [ whd in ⊢ (???(??%)) @Ege | @(initial_state_intro … Ege Em esb ef) ]
     541@(initial_state_intro … Em esb ef) @refl
    543542qed.
    544543
Note: See TracChangeset for help on using the changeset viewer.