1 | |
---|
2 | include "common/IO.ma". |
---|
3 | include "common/SmallstepExec.ma". |
---|
4 | include "arithmetics/nat.ma". |
---|
5 | |
---|
6 | (* Functions to allow programs to be executed up to some number of steps, given |
---|
7 | a predetermined set of input values. Note that we throw away the state if |
---|
8 | we stop at a continuation - it can be too large to work with. *) |
---|
9 | |
---|
10 | definition get_input : ∀o:io_out. eventval → res (io_in o) ≝ |
---|
11 | λo,ev. |
---|
12 | match io_in_typ o return λt. res (eventval_type t) with |
---|
13 | [ ASTint sz _ ⇒ match ev with [ EVint sz' i ⇒ intsize_eq_elim ? sz' sz ? i (λi.OK ? i) (Error ? (msg IllTypedEvent)) | _ ⇒ Error ? (msg IllTypedEvent) ] |
---|
14 | | ASTptr ⇒ Error ? (msg IllTypedEvent) |
---|
15 | ]. |
---|
16 | |
---|
17 | inductive snapshot (state:Type[0]) : Type[0] ≝ |
---|
18 | | running : trace → state → snapshot state |
---|
19 | | finished : trace → int → state → snapshot state |
---|
20 | | input_exhausted : trace → snapshot state. |
---|
21 | |
---|
22 | axiom StoppedMidIO : String. |
---|
23 | |
---|
24 | let rec up_to_nth_step (n:nat) (state:Type[0]) (input:list eventval) (e:execution state io_out io_in) (t:trace) : res (snapshot state) ≝ |
---|
25 | match n with |
---|
26 | [ O ⇒ match e with [ e_step tr s _ ⇒ OK ? (running ? (t⧺tr) s) |
---|
27 | | e_stop tr r m ⇒ OK ? (finished ? (t⧺tr) r m) |
---|
28 | | e_interact o k ⇒ Error ? (msg StoppedMidIO) |
---|
29 | | e_wrong m ⇒ Error ? m ] |
---|
30 | | S m ⇒ match e with [ e_step tr s e' ⇒ up_to_nth_step m state input e' (t⧺tr) |
---|
31 | | e_stop tr r m ⇒ OK ? (finished ? (t⧺tr) r m) |
---|
32 | | e_interact o k ⇒ |
---|
33 | match input with |
---|
34 | [ nil ⇒ OK ? (input_exhausted ? t) |
---|
35 | | cons h tl ⇒ do i ← get_input o h; |
---|
36 | up_to_nth_step m state tl (k i) t |
---|
37 | ] |
---|
38 | | e_wrong m ⇒ Error ? m |
---|
39 | ] |
---|
40 | ]. |
---|
41 | |
---|
42 | definition exec_up_to : ∀fx:fullexec io_out io_in. ∀p:program ?? fx. nat → list eventval → res (snapshot (state ?? fx (make_global … p))) ≝ |
---|
43 | λfx,p,n,i. up_to_nth_step n ? i (exec_inf ?? fx p) E0. |
---|
44 | |
---|
45 | (* A version of exec_up_to that reports the state prior to failure. *) |
---|
46 | |
---|
47 | inductive snapshot' (state:Type[0]) : Type[0] ≝ |
---|
48 | | running' : trace → state → snapshot' state |
---|
49 | | finished' : nat → trace → int → state → snapshot' state |
---|
50 | | input_exhausted' : trace → snapshot' state |
---|
51 | | failed' : errmsg → nat → state → snapshot' state |
---|
52 | | init_state_fail' : errmsg → snapshot' state. |
---|
53 | |
---|
54 | let rec up_to_nth_step' (n:nat) (total:nat) (state:Type[0]) (input:list eventval) (e:execution state io_out io_in) (prev:state) (t:trace) : snapshot' state ≝ |
---|
55 | match n with |
---|
56 | [ O ⇒ match e with [ e_step tr s _ ⇒ running' ? (t⧺tr) s |
---|
57 | | e_stop tr r m ⇒ finished' ? total (t⧺tr) r m |
---|
58 | | e_interact o k ⇒ failed' ? (msg StoppedMidIO) total prev |
---|
59 | | e_wrong m ⇒ failed' ? m total prev ] |
---|
60 | | S m ⇒ match e with [ e_step tr s e' ⇒ up_to_nth_step' m total state input e' s (t⧺tr) |
---|
61 | | e_stop tr r m ⇒ finished' ? (minus total n) (t⧺tr) r m |
---|
62 | | e_interact o k ⇒ |
---|
63 | match input with |
---|
64 | [ nil ⇒ input_exhausted' ? t |
---|
65 | | cons h tl ⇒ match get_input o h with |
---|
66 | [ OK i ⇒ up_to_nth_step' m total state tl (k i) prev t |
---|
67 | | Error m ⇒ failed' ? m (minus total n) prev |
---|
68 | ] |
---|
69 | ] |
---|
70 | | e_wrong m ⇒ failed' ? m (minus total n) prev |
---|
71 | ] |
---|
72 | ]. |
---|
73 | |
---|
74 | definition exec_up_to' : ∀fx:fullexec io_out io_in. ∀p:program ?? fx. nat → list eventval → snapshot' (state ?? fx (make_global … p)) ≝ |
---|
75 | λfx,p,n,i. |
---|
76 | match make_initial_state ?? fx p with |
---|
77 | [ OK s ⇒ up_to_nth_step' n n (state ?? fx (make_global … p)) i (exec_inf ?? fx p) s E0 |
---|
78 | | Error m ⇒ init_state_fail' ? m |
---|
79 | ]. |
---|
80 | |
---|
81 | (* Provide an easy way to get a term in proof mode for reduction. |
---|
82 | For example, |
---|
83 | |
---|
84 | example exec: result ? (exec_up_to myprog 20 [EVint (repr 12)]). |
---|
85 | normalize (* you can examine the result here *) |
---|
86 | % qed. |
---|
87 | |
---|
88 | *) |
---|
89 | |
---|
90 | inductive result (A:Type[0]) : A → Type[0] ≝ |
---|
91 | | witness : ∀a:A. result A a. |
---|
92 | |
---|
93 | inductive finishes_with : int → ∀S.res (snapshot S) → Prop ≝ |
---|
94 | fw_ok : ∀r,S,t,s. finishes_with r S (OK ? (finished S t r s)). |
---|
95 | |
---|
96 | include "common/GenMem.ma". |
---|
97 | |
---|
98 | (* Hide the representation of memory to make displaying the results easier. *) |
---|
99 | |
---|
100 | notation < "'MEM'" with precedence 1 for @{ 'mem }. |
---|
101 | interpretation "hide memory" 'mem = (mk_mem ???). |
---|