source: src/Clight/SmallstepExec.ma @ 694

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

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

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