Ignore:
Timestamp:
Mar 18, 2011, 4:28:26 PM (9 years ago)
Author:
campbell
Message:

Get Clight semantics going again (except for problems CexecEquiv? that I caused
earlier).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecEquiv.ma

    r487 r700  
    1 include "CexecComplete.ma".
    2 include "CexecSound.ma".
    3 include "extralib.ma".
     1include "Clight/CexecComplete.ma".
     2include "Clight/CexecSound.ma".
     3include "utilities/extralib.ma".
    44
    55include "basics/jmeq.ma".
     
    1010| se_step : trace → state → s_execution → s_execution
    1111| se_wrong : s_execution
    12 | se_interact : ∀o:io_out. (io_in o → execution) → io_in o → s_execution → s_execution.
    13 
    14 coinductive single_exec_of : execution → s_execution → Prop ≝
    15 | seo_stop : ∀tr,r,m. single_exec_of (e_stop tr r m) (se_stop tr r m)
     12| se_interact : ∀o:io_out. (io_in o → execution state io_out io_in) → io_in o → s_execution → s_execution.
     13
     14coinductive single_exec_of : execution state io_out io_in → s_execution → Prop ≝
     15| seo_stop : ∀tr,r,m. single_exec_of (e_stop ??? tr r m) (se_stop tr r m)
    1616| seo_step : ∀tr,s,e,se.
    1717    single_exec_of e se →
    18     single_exec_of (e_step tr s e) (se_step tr s se)
    19 | seo_wrong : single_exec_of e_wrong se_wrong
     18    single_exec_of (e_step ??? tr s e) (se_step tr s se)
     19| seo_wrong : single_exec_of (e_wrong ???) se_wrong
    2020| seo_interact : ∀o,k,i,se.
    2121    single_exec_of (k i) se →
    22     single_exec_of (e_interact o k) (se_interact o k i se).
     22    single_exec_of (e_interact ??? o k) (se_interact o k i se).
    2323
    2424(* starting after state s, zero or more steps of execution e reach state s'
     
    4949] qed.
    5050
    51 lemma exec_e_step: ∀ge,x,tr,s,e.
    52   exec_inf_aux ge x = e_step tr s e →
    53   exec_inf_aux ge (exec_step ge s) = e.
    54 #ge #x #tr #s #e
     51lemma exec_e_step: ∀p,ge,x,tr,s,e.
     52  exec_inf_aux (clight_exec p) ge x = e_step ??? tr s e →
     53  exec_inf_aux (clight_exec p) ge (exec_step ge s) = e.
     54#p #ge #x #tr #s #e
    5555>(exec_inf_aux_unfold …) cases x;
    5656[ #o #k #EXEC whd in EXEC:(??%?); destruct
    57 | #y cases y; #tr' #s' whd in ⊢ (??%? → ?);
     57| #y cases y; #tr' #s' whd in ⊢ (??%? → ?); >(?:? (clight_exec p) s' = is_final s'); whd in match (? (clight_exec) s') in ⊢ %; whd in ⊢ (??%? → ?);
    5858    cases (is_final_state s'); #FINAL #EXEC whd in EXEC:(??%?); destruct;
    5959    @refl
Note: See TracChangeset for help on using the changeset viewer.