source: src/common/SmallstepExec.ma @ 702

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

Refine small-step executable semantics abstraction a little.
Some progress on using the new definition in CexecEquiv?, but only partial
because of over-eager normalisation by the destruct tactic.
Whole program semantics for RTLabs using it.

File size: 3.5 KB
Line 
1
2include "utilities/extralib.ma".
3include "common/IOMonad.ma".
4include "common/Integers.ma".
5include "common/Events.ma".
6include "common/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; is_final : state → option int
14; mem_of_state : state → mem
15; step : genv → state → IO output input (trace×state)
16}.
17
18let rec repeat (n:nat) (exec:execstep) (g:genv exec) (s:state exec)
19 : IO (output exec) (input exec) (trace × (state exec)) ≝
20match n with
21[ O ⇒ Value ??? 〈E0, s〉
22| S n' ⇒ ! 〈t1,s1〉 ← step exec g s;
23         repeat n' exec g s1
24].
25
26(* A (possibly non-terminating) execution.   *)
27coinductive execution (state:Type[0]) (output:Type[0]) (input:output → Type[0]) : Type[0] ≝
28| e_stop : trace → int → mem → execution state output input
29| e_step : trace → state → execution state output input → execution state output input
30| e_wrong : execution state output input
31| e_interact : ∀o:output. (input o → execution state output input) → execution state output input.
32
33(* This definition is slightly awkward because of the need to provide resumptions.
34   It records the last trace/state passed in, then recursively processes the next
35   state. *)
36
37let corec exec_inf_aux (exec:execstep) (ge:genv exec)
38                       (s:IO (output exec) (input exec) (trace×(state exec)))
39                       : execution ??? ≝
40match s with
41[ Wrong ⇒ e_wrong ???
42| Value v ⇒ match v with [ pair t s' ⇒
43    match is_final exec s' with
44    [ Some r ⇒ e_stop ??? t r (mem_of_state exec s')
45    | None ⇒ e_step ??? t s' (exec_inf_aux ? ge (step exec ge s')) ] ]
46| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ? ge (k' v))
47].
48
49lemma execution_cases: ∀ex.∀e:execution (state ex) (output ex) (input ex).
50 e = match e with [ e_stop tr r m ⇒ e_stop ??? tr r m
51 | e_step tr s e ⇒ e_step ??? tr s e
52 | e_wrong ⇒ e_wrong ??? | e_interact o k ⇒ e_interact ??? o k ].
53#ex #e cases e; //; qed.
54
55axiom exec_inf_aux_unfold: ∀exec,ge,s. exec_inf_aux exec ge s =
56match s with
57[ Wrong ⇒ e_wrong ???
58| Value v ⇒ match v with [ pair t s' ⇒
59    match is_final exec s' with
60    [ Some r ⇒ e_stop ??? t r (mem_of_state exec s')
61    | None ⇒ e_step ??? t s' (exec_inf_aux ? ge (step exec ge s')) ] ]
62| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ? ge (k' v))
63].
64(*
65#exec #ge #s >(execution_cases ? (exec_inf_aux …)) cases s
66[ #o #k
67| #x cases x #tr #s' (* XXX Can't unfold exec_inf_aux here *)
68| ]
69whd in ⊢ (??%%); //;
70qed.
71*)
72
73record execstep' : Type[1] ≝
74{ es0 :> execstep
75; initial : state es0 → Prop
76}.
77
78
79alias symbol "and" (instance 2) = "logical and".
80record related_semantics : Type[1] ≝
81{ sem1 : execstep'
82; sem2 : execstep'
83; ge1 : genv sem1
84; ge2 : genv sem2
85; match_states : state sem1 → state sem2 → Prop
86; match_initial_states : ∀st1. (initial sem1) st1 → ∃st2. (initial sem2) st2 ∧ match_states st1 st2
87; match_final_states : ∀st1,st2,r. match_states st1 st2 → (is_final sem1) st1 = Some ? r → (is_final sem2) st2 = Some ? r
88}.
89
90
91
92record simulation : Type[1] ≝
93{ sems :> related_semantics
94; sim : ∀st1,st2,t,st1'.
95        P_io' ?? (trace × (state (sem1 sems))) (λr. r = 〈t,st1'〉) (step (sem1 sems) (ge1 sems) st1) →
96        match_states sems st1 st2 →
97        ∃st2':(state (sem2 sems)).(∃n:nat.P_io' ?? (trace × (state (sem2 sems))) (λr. r = 〈t,st2'〉) (repeat n (sem2 sems) (ge2 sems) st2)) ∧
98          match_states sems st1' st2'
99}.
Note: See TracBrowser for help on using the repository browser.