source: Deliverables/D3.1/C-semantics/SmallstepExec.ma @ 693

Last change on this file since 693 was 693, checked in by campbell, 9 years ago

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

File size: 3.4 KB
RevLine 
[24]1
2include "extralib.ma".
3include "IOMonad.ma".
4include "Integers.ma".
5include "Events.ma".
[693]6include "Mem.ma".
[24]7
[693]8record execstep : Type[1] ≝
9{ genv  : Type[0]
10; state : Type[0]
11; output : Type[0]
12; input : output → Type[0]
[24]13; initial : state → Prop
[693]14; is_final : state → option int
15; mem_of_state : state → mem
16; step : genv → state → IO output input (trace×state)
[24]17}.
18
[693]19let rec repeat (n:nat) (exec:execstep) (g:genv exec) (s:state exec)
20 : IO (output exec) (input exec) (trace × (state exec)) ≝
[24]21match n with
[25]22[ O ⇒ Value ??? 〈E0, s〉
[469]23| S n' ⇒ ! 〈t1,s1〉 ← step exec g s;
[24]24         repeat n' exec g s1
25].
26
[693]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
[24]76alias symbol "and" (instance 2) = "logical and".
[693]77record related_semantics : Type[1] ≝
[24]78{ sem1 : execstep
79; sem2 : execstep
80; ge1 : genv sem1
81; ge2 : genv sem2
82; match_states : state sem1 → state sem2 → Prop
83; match_initial_states : ∀st1. (initial sem1) st1 → ∃st2. (initial sem2) st2 ∧ match_states st1 st2
[693]84; match_final_states : ∀st1,st2,r. match_states st1 st2 → (is_final sem1) st1 = Some ? r → (is_final sem2) st2 = Some ? r
[24]85}.
86
87
88
[693]89record simulation : Type[1] ≝
[24]90{ sems :> related_semantics
91; sim : ∀st1,st2,t,st1'.
[25]92        P_io' ?? (trace × (state (sem1 sems))) (λr. r = 〈t,st1'〉) (step (sem1 sems) (ge1 sems) st1) →
[24]93        match_states sems st1 st2 →
[25]94        ∃st2':(state (sem2 sems)).(∃n:nat.P_io' ?? (trace × (state (sem2 sems))) (λr. r = 〈t,st2'〉) (repeat n (sem2 sems) (ge2 sems) st2)) ∧
[24]95          match_states sems st1' st2'
96}.
Note: See TracBrowser for help on using the repository browser.