Ignore:
Timestamp:
Feb 21, 2012, 11:58:12 AM (8 years ago)
Author:
campbell
Message:

Add a distinguished final state to the front-end languages to match up
with the structured traces.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecEquiv.ma

    r1605 r1713  
    88(* A "single execution" - where all of the input values are made explicit. *)
    99coinductive s_execution : Type[0] ≝
    10 | se_stop : trace → int → mem → s_execution
     10| se_stop : trace → int → s_execution
    1111| se_step : trace → state → s_execution → s_execution
    1212| se_wrong : errmsg → s_execution
     
    1414
    1515coinductive single_exec_of : execution state io_out io_in → s_execution → Prop ≝
    16 | seo_stop : ∀tr,r,s. single_exec_of (e_stop ??? tr r s) (se_stop tr r (mem_of_state s))
     16| seo_stop : ∀tr,r,s. single_exec_of (e_stop ??? tr r s) (se_stop tr r)
    1717| seo_step : ∀tr,s,e,se.
    1818    single_exec_of e se →
     
    157157] qed.
    158158
    159 lemma exec_from_interact_stop : ∀ge,s,o,k,i,tr,r,m.
    160 exec_from ge s (se_interact o k i (se_stop tr r m)) →
    161 step ge s tr (Returnstate (Vint I32 r) Kstop m).
    162 #ge #s0 #o0 #k0 #i0 #tr0 #s0' #e0 #H inversion H;
     159lemma exec_from_interact_stop : ∀ge,s,o,k,i,tr,r.
     160exec_from ge s (se_interact o k i (se_stop tr r)) →
     161step ge s tr (Finalstate r).
     162#ge #s0 #o0 #k0 #i0 #tr0 #r0 #H inversion H
    163163[ #tr #r #m #E1 #E2 destruct
    164164| #tr #s #e #se #H1 #H2 #E destruct (E)
    165165| #msg #_ #E destruct
    166 | #o #k #i #se #H1 #H2 #E #_ destruct (E);
    167     lapply (exec_step_sound ge s0);
     166| #o #k #i #se #H1 #H2 #E #_ destruct (E)
     167    lapply (exec_step_sound ge s0)
    168168    >(exec_inf_aux_unfold …) in H2;
    169     cases (exec_step ge s0);
     169    cases (exec_step ge s0)
    170170    [ #o' #k'
    171171        #E' whd in E':(??%??); destruct (E');
     
    226226] qed.
    227227
    228 inductive execution_terminates : trace → state → s_execution → int → mem → Prop ≝
    229 | terminates : ∀s,s',tr,tr',r,e,m.
    230     execution_isteps tr s e s' (se_stop tr' r m) →
    231     execution_terminates (tr⧺tr') s (se_step E0 s e) r m
     228inductive execution_terminates : trace → state → s_execution → int → Prop ≝
     229| terminates : ∀s,s',tr,tr',r,e.
     230    execution_isteps tr s e s' (se_stop tr' r) →
     231    execution_terminates (tr⧺tr') s (se_step E0 s e) r
    232232(* We should only be able to get to here if main is an external function, which is silly. *)
    233 | annoying_corner_case_terminates: ∀s,s',tr,tr',r,e,m,o,k,i.
    234     execution_isteps tr s e s' (se_interact o k i (se_stop tr' r m)) →
    235     execution_terminates (tr⧺tr') s (se_step E0 s e) r m.
     233| annoying_corner_case_terminates: ∀s,s',tr,tr',r,e,o,k,i.
     234    execution_isteps tr s e s' (se_interact o k i (se_stop tr' r)) →
     235    execution_terminates (tr⧺tr') s (se_step E0 s e) r.
    236236
    237237coinductive execution_diverging : s_execution → Prop ≝
     
    278278] qed.
    279279
    280 lemma final_step: ∀ge,tr,r,m,s.
    281   exec_from ge s (se_stop tr r m) →
    282   step ge s tr (Returnstate (Vint I32 r) Kstop m).
    283 #ge #tr #r #m #s #EXEC
     280lemma final_step: ∀ge,tr,r,s.
     281  exec_from ge s (se_stop tr r) →
     282  step ge s tr (Finalstate r).
     283#ge #tr #r #s #EXEC
    284284whd in EXEC;
    285285inversion EXEC;
    286 [ #tr' #r' #m' #EXEC' #E #_ destruct (E);
    287     lapply (exec_step_sound ge s);
     286[ #tr' #r' #s' #EXEC' #E #_ destruct (E)
     287    lapply (exec_step_sound ge s)
    288288    >(exec_inf_aux_unfold …) in EXEC';
    289     cases (exec_step ge s);
     289    cases (exec_step ge s)
    290290    [ #o #k #EXEC' whd in EXEC':(??%??); destruct (EXEC');
    291291    | #x cases x; #tr'' #s' whd in ⊢ (??%?? → ?);
     
    294294    | #msg #EXEC' whd in EXEC':(??%??); destruct (EXEC');
    295295    ]
    296     inversion FINAL; #r''' #m'' #E1 #E2 #_ #H destruct (E1 E2);
     296    inversion FINAL #r''' #E1 #E2 #_ #H destruct (E1 E2);
    297297    @H
    298298| #tr' #s' #e' #se' #H #EXEC' #E destruct
     
    304304lemma e_stop_inv: ∀ge,x,tr,r,s.
    305305  exec_inf_aux ?? clight_exec ge x = e_stop ??? tr r s →
    306   x = Value ??? 〈tr,Returnstate (Vint I32 r) Kstop (mem_of_state s)〉.
     306  x = Value ??? 〈tr,Finalstate r〉.
    307307#ge #x #tr #r #s
    308308>(exec_inf_aux_unfold …) cases x;
    309309[ #o #k #EXEC whd in EXEC:(??%?); destruct;
    310310| #z cases z; #tr' #s' whd in ⊢ (??%? → ?); @is_final_elim'
    311   [ #r' #FINAL cases FINAL; #r'' #m' #EXEC whd in EXEC:(??%?);
     311  [ #r' #FINAL cases FINAL; #r'' #EXEC whd in EXEC:(??%?);
    312312      destruct (EXEC); @refl
    313313  | #F #EXEC whd in EXEC:(??%?); destruct (EXEC);
     
    316316] qed.
    317317
    318 lemma terminates_sound: ∀ge,tr,s,r,m,e.
    319   execution_terminates tr s (se_step E0 s e) r m
     318lemma terminates_sound: ∀ge,tr,s,r,e.
     319  execution_terminates tr s (se_step E0 s e) r
    320320  exec_from ge s e →
    321   star (mk_transrel … step) ge s tr (Returnstate (Vint I32 r) Kstop m).
    322 #ge #tr0 #s0 #r #m #e0 #H inversion H;
    323 [ #s #s' #tr #tr' #r' #e #m' #ESTEPS #E1 #E2 #E3 #E4 #E5 #_ #EXEC
     321  star (mk_transrel … step) ge s tr (Finalstate r).
     322#ge #tr0 #s0 #r #e0 #H inversion H;
     323[ #s #s' #tr #tr' #r' #e #ESTEPS #E1 #E2 #E3 #E4 #_ #EXEC
    324324    destruct (E1 E2 E3 E4 E5);
    325325    cases (several_steps … ESTEPS EXEC); #STARs' #EXECs'
    326326    @(star_right … STARs')
    327     [ 2: @(final_step ge tr' r' m' s' … EXECs')
     327    [ 2: @(final_step ge tr' r' s' … EXECs')
    328328    | skip
    329329    | @refl
    330330    ]
    331 | #s #s' #tr #tr' #r' #e #m' #o #k #i #ESTEPS #E1 #E2 #E3 #E4 #E5 #_ #EXEC
    332     destruct;
    333     cases (several_steps … ESTEPS EXEC); #STARs' #EXECs'
     331| #s #s' #tr #tr' #r' #e #o #k #i #ESTEPS #E1 #E2 #E3 #E4 #_ #EXEC
     332    destruct
     333    cases (several_steps … ESTEPS EXEC) #STARs' #EXECs'
    334334    @(star_right … STARs')
    335335    [ @tr'
     
    403403  ¬(∃r. final_state s' r).
    404404#ge #s #o #k #i #tr #s' #e #H
    405 % *; #r #F cases F in H; #r' #m #H
     405% *; #r #F cases F in H; #r' #H
    406406inversion H;
    407407[ #tr' #r #m #EXEC #E destruct
     
    469469
    470470inductive execution_characterisation : state → s_execution → Prop ≝
    471 | ec_terminates: ∀s,r,m,e,tr.
    472     execution_terminates tr s e r m
     471| ec_terminates: ∀s,r,e,tr.
     472    execution_terminates tr s e r
    473473    execution_characterisation s e
    474474| ec_diverges: ∀s,e,tr.
     
    543543  ]
    544544| #v #kk #m whd in ⊢ (???%); cases kk;
    545     [ 8: #x1 #x2 #x3 #x4 cases x1;
     545    [ cases v // * //
     546    | 8: #x1 #x2 #x3 #x4 cases x1;
    546547      [ whd in ⊢ (???%); cases v; // | #x5 whd in ⊢ (???%); cases x5;
    547548          #x6 #x7 @opt_does_not_interact // ]
    548549    | *: // ]
     550| #r //
    549551] qed.
    550552
     
    615617| eno_interact: ∀o,k,tr,s,e,i. execution_not_over (se_interact o k i (se_step tr s e)).
    616618
    617 lemma eno_stop: ∀tr,r,m. execution_not_over (se_stop tr r m) → False.
    618 #tr0 #r0 #m0 #H inversion H;
     619lemma eno_stop: ∀tr,r. execution_not_over (se_stop tr r) → False.
     620#tr0 #r0 #H inversion H;
    619621[ #tr #s #e #E destruct
    620622| #o #k #tr #s #e #i #E destruct
     
    635637lapply (NONTERMINATING E0 s e ?); //;
    636638cases e in UNREACTIVE NONTERMINATING CONTINUES ⊢ %;
    637 [ #tr #i #m #_ #_ #_ #ENO elim (eno_stop … ENO);
     639[ #tr #i #_ #_ #_ #ENO elim (eno_stop … ENO);
    638640| #tr #s' #e' #UNREACTIVE lapply (UNREACTIVE tr s' e' ?);
    639641  [ <(E0_right tr) in ⊢ (?%????);
     
    667669  single_exec_of e1 e2 →
    668670  match e1 with
    669   [ e_stop tr r s ⇒ match e2 with [ se_stop tr' r' m' ⇒ tr = tr' ∧ r = r' ∧ mem_of_state s = m' | _ ⇒ False ]
     671  [ e_stop tr r s ⇒ match e2 with [ se_stop tr' r' ⇒ tr = tr' ∧ r = r' | _ ⇒ False ]
    670672  | e_step tr s e1' ⇒ match e2 with [ se_step tr' s' e2' ⇒ tr = tr' ∧ s = s' ∧ single_exec_of e1' e2' | _ ⇒ False ]
    671673  | e_wrong _ ⇒ match e2 with [ se_wrong _ ⇒ True | _ ⇒ False ]
     
    859861    *; #e #NNT4 elim (imply_to_and classic … NNT4);
    860862    cases e;
    861     [ #tr' #r #m #STEPS #NOSTEP
    862         @(ec_terminates s r m ? (Eapp tr tr')) %
     863    [ #tr' #r #STEPS #NOSTEP
     864        @(ec_terminates s r ? (Eapp tr tr')) %
    863865        [ @s'
    864866        | @STEPS
     
    872874    | #o #k #i #e' #STEPS #NOSTEP
    873875        cases e' in STEPS NOSTEP;
    874         [ #tr' #r #m #STEPS #NOSTEP
     876        [ #tr' #r #STEPS #NOSTEP
    875877            @(ec_terminates s ???)
    876            [ 4: @(annoying_corner_case_terminates … STEPS) ]
     878           [ 3: @(annoying_corner_case_terminates … STEPS) ]
    877879        | #tr1 #s1 #e1 #STEPS *; #NOSTEP
    878880            @False_ind @NOSTEP //
     
    917919
    918920inductive execution_matches_behavior: s_execution → program_behavior → Prop ≝
    919 | emb_terminates: ∀s,e,tr,r,m.
    920     execution_terminates tr s e r m
     921| emb_terminates: ∀s,e,tr,r.
     922    execution_terminates tr s e r
    921923    execution_matches_behavior e (Terminates tr r)
    922924| emb_diverges: ∀s,e,tr.
     
    932934    execution_matches_behavior (se_wrong msg) (Goes_wrong E0).
    933935
    934 lemma exec_state_terminates: ∀tr,tr',s,s',e,r,m.
    935   execution_terminates tr s (se_step tr' s' e) r m → s = s'.
    936 #tr #tr' #s #s' #e #r #m #H inversion H;
    937 [ #s1 #s2 #tr1 #tr2 #r' #e' #m' #H' #E1 #E2 #E3 #E4 #E5 #_ destruct; @refl
    938 | #s1 #s2 #tr1 #tr2 #r' #e' #m' #o #k #i #H' #E1 #E2 #E3 #E4 #E5 #_ destruct; @refl
     936lemma exec_state_terminates: ∀tr,tr',s,s',e,r.
     937  execution_terminates tr s (se_step tr' s' e) r → s = s'.
     938#tr #tr' #s #s' #e #r #H inversion H;
     939[ #s1 #s2 #tr1 #tr2 #r' #e' #H' #E1 #E2 #E3 #E4 #_ destruct; @refl
     940| #s1 #s2 #tr1 #tr2 #r' #e' #o #k #i #H' #E1 #E2 #E3 #E4 #_ destruct; @refl
    939941] qed.
    940942
     
    959961#s0 #e0 #exec
    960962cases exec;
    961 [ #s #r #m #e #tr #TERM
     963[ #s #r #e #tr #TERM
    962964    %{ (Terminates tr r)}
    963965    @(emb_terminates … TERM)
     
    979981#b #f #ge #m #E1 #E2 #E3 #E4 % *; #r #H2
    980982inversion H2;
    981 #r' #m' #E5 #E6 destruct (E5);
     983#r' #E5 #E6 destruct (E5);
    982984qed.
    983985
     
    10131015        %{r} @F
    10141016    | #NOTFINAL whd in ⊢ (?%? → ?); cases e;
    1015         [ #tr #r #m #EXEC0 | #tr #s' #e0 #EXEC0 | #msg #EXEC0 | #o #k #i #e #EXEC0 ]
     1017        [ #tr #r #EXEC0 | #tr #s' #e0 #EXEC0 | #msg #EXEC0 | #o #k #i #e #EXEC0 ]
    10161018        cases (se_inv … EXEC0); *; #E1 #E2 <E1 <E2 #EXEC'
    10171019    lapply (behavior_of_execution ??
     
    10201022        #ge #Ege
    10211023        inversion MATCHES;
    1022         [ #s0 #e1 #tr1 #r #m #TERM #EXEC #BEHAVES <EXEC in TERM;
     1024        [ #s0 #e1 #tr1 #r #TERM #EXEC #BEHAVES <EXEC in TERM;
    10231025            #TERM
    10241026            lapply (exec_state_terminates … TERM); #E1
     
    10701072    [ whd in EXEC:(?%?);
    10711073        cases e in EXEC;
    1072         [ #tr #r #m #EXEC0 | #tr #s' #e0 #EXEC0 | #msg #EXEC0 | #o #k #i #e #EXEC0 ]
     1074        [ #tr #r #EXEC0 | #tr #s' #e0 #EXEC0 | #msg #EXEC0 | #o #k #i #e #EXEC0 ]
    10731075        cases (se_inv … EXEC0);
    10741076        @emb_initially_wrong
Note: See TracChangeset for help on using the changeset viewer.