Ignore:
Timestamp:
Mar 18, 2011, 12:11:23 PM (9 years ago)
Author:
campbell
Message:

Separate out whole program executions from the clight semantics and start
setting it up for RTLabs too.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/SmallstepExec.ma

    r469 r693  
    44include "Integers.ma".
    55include "Events.ma".
     6include "Mem.ma".
    67
    7 nrecord execstep : Type[1] ≝
    8 { genv  : Type
    9 ; state : Type
    10 ; input : Type
    11 ; output : (input → Type)
     8record execstep : Type[1] ≝
     9{ genv  : Type[0]
     10; state : Type[0]
     11; output : Type[0]
     12; input : output → Type[0]
    1213; initial : state → Prop
    13 ; final : state → int → Prop
    14 ; step : genv → state → IO input output (trace×state)
     14; is_final : state → option int
     15; mem_of_state : state → mem
     16; step : genv → state → IO output input (trace×state)
    1517}.
    1618
    17 nlet rec repeat (n:nat) (exec:execstep) (g:genv exec) (s:state exec)
    18  : IO (input exec) (output exec) (trace × (state exec)) ≝
     19let rec repeat (n:nat) (exec:execstep) (g:genv exec) (s:state exec)
     20 : IO (output exec) (input exec) (trace × (state exec)) ≝
    1921match n with
    2022[ O ⇒ Value ??? 〈E0, s〉
     
    2325].
    2426
     27(* A (possibly non-terminating) execution.   *)
     28coinductive execution (state:Type[0]) (output:Type[0]) (input:output → Type[0]) : Type[0] ≝
     29| e_stop : trace → int → mem → execution state output input
     30| e_step : trace → state → execution state output input → execution state output input
     31| e_wrong : execution state output input
     32| e_interact : ∀o:output. (input o → execution state output input) → execution state output input.
     33
     34(* This definition is slightly awkward because of the need to provide resumptions.
     35   It records the last trace/state passed in, then recursively processes the next
     36   state. *)
     37
     38let corec exec_inf_aux (exec:execstep) (ge:genv exec)
     39                       (s:IO (output exec) (input exec) (trace×(state exec)))
     40                       : execution ??? ≝
     41match s with
     42[ Wrong ⇒ e_wrong ???
     43| Value v ⇒ match v with [ pair t s' ⇒
     44    match is_final exec s' with
     45    [ Some r ⇒ e_stop ??? t r (mem_of_state exec s')
     46    | None ⇒ e_step ??? t s' (exec_inf_aux ? ge (step exec ge s')) ] ]
     47| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ? ge (k' v))
     48].
     49
     50lemma execution_cases: ∀ex.∀e:execution (state ex) (output ex) (input ex).
     51 e = match e with [ e_stop tr r m ⇒ e_stop ??? tr r m
     52 | e_step tr s e ⇒ e_step ??? tr s e
     53 | e_wrong ⇒ e_wrong ??? | e_interact o k ⇒ e_interact ??? o k ].
     54#ex #e cases e; //; qed.
     55
     56axiom exec_inf_aux_unfold: ∀exec,ge,s. exec_inf_aux exec ge s =
     57match s with
     58[ Wrong ⇒ e_wrong ???
     59| Value v ⇒ match v with [ pair t s' ⇒
     60    match is_final exec s' with
     61    [ Some r ⇒ e_stop ??? t r (mem_of_state exec s')
     62    | None ⇒ e_step ??? t s' (exec_inf_aux ? ge (step exec ge s')) ] ]
     63| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ? ge (k' v))
     64].
     65(*
     66#exec #ge #s >(execution_cases ? (exec_inf_aux …)) cases s
     67[ #o #k
     68| #x cases x #tr #s' (* XXX Can't unfold exec_inf_aux here *)
     69| ]
     70whd in ⊢ (??%%); //;
     71qed.
     72*)
     73
     74
     75
    2576alias symbol "and" (instance 2) = "logical and".
    26 nrecord related_semantics : Type[1] ≝
     77record related_semantics : Type[1] ≝
    2778{ sem1 : execstep
    2879; sem2 : execstep
     
    3182; match_states : state sem1 → state sem2 → Prop
    3283; match_initial_states : ∀st1. (initial sem1) st1 → ∃st2. (initial sem2) st2 ∧ match_states st1 st2
    33 ; match_final_states : ∀st1,st2,r. match_states st1 st2 → (final sem1) st1 r → (final sem2) st2 r
     84; match_final_states : ∀st1,st2,r. match_states st1 st2 → (is_final sem1) st1 = Some ? r → (is_final sem2) st2 = Some ? r
    3485}.
    3586
    3687
    3788
    38 nrecord simulation : Type[1] ≝
     89record simulation : Type[1] ≝
    3990{ sems :> related_semantics
    4091; sim : ∀st1,st2,t,st1'.
Note: See TracChangeset for help on using the changeset viewer.