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