1 | (* |
---|
2 | include "Csyntax.ma". |
---|
3 | include "AST.ma". |
---|
4 | |
---|
5 | nlet rec skippy_s (s:statement) : statement ≝ |
---|
6 | match s with |
---|
7 | [ Ssequence s1 s2 ⇒ Ssequence (skippy_s s1) (skippy_s s2) |
---|
8 | | Scall _ _ _ ⇒ Ssequence Sskip s |
---|
9 | | _ ⇒ s |
---|
10 | ]. |
---|
11 | |
---|
12 | ndefinition skippy_f : function → function ≝ λf. |
---|
13 | mk_function |
---|
14 | (fn_return f) |
---|
15 | (fn_params f) |
---|
16 | (fn_vars f) |
---|
17 | (skippy_s (fn_body f)). |
---|
18 | |
---|
19 | ndefinition skippy_fd : fundef → fundef ≝ λf. |
---|
20 | match f with |
---|
21 | [ CL_Internal fd ⇒ Internal (skippy_f fd) |
---|
22 | | CL_External id args res ⇒ External id args res |
---|
23 | ]. |
---|
24 | |
---|
25 | ndefinition skippy : program → program ≝ transform_program … skippy_fd. |
---|
26 | nremark rewrite_skippy : skippy = transform_program … skippy_fd. |
---|
27 | //; nqed. |
---|
28 | (* |
---|
29 | ndefinition skippy : program → program ≝ |
---|
30 | λp. |
---|
31 | mk_program ?? |
---|
32 | (map ?? (λfd. match snd ?? fd with |
---|
33 | [ CL_Internal f ⇒ |
---|
34 | 〈fst ?? fd, |
---|
35 | CL_Internal |
---|
36 | (mk_function (fn_return f) (fn_params f) (fn_vars f) (skippy_s (fn_body f)))〉 |
---|
37 | | CL_External _ _ _ ⇒ fd ]) |
---|
38 | (prog_funct ?? p)) |
---|
39 | (prog_main ?? p) |
---|
40 | (prog_vars ?? p). |
---|
41 | *) |
---|
42 | include "SmallstepExec.ma". |
---|
43 | include "CexecIO.ma". |
---|
44 | |
---|
45 | ndefinition Csem ≝ λp:program.mk_execstep |
---|
46 | ? |
---|
47 | ? |
---|
48 | ? |
---|
49 | ? |
---|
50 | (initial_state p) |
---|
51 | final_state |
---|
52 | exec_step. |
---|
53 | |
---|
54 | nlet rec skippy_k (k:cont) : cont ≝ |
---|
55 | match k with |
---|
56 | [ Kstop ⇒ Kstop |
---|
57 | | Kseq s k' ⇒ Kseq (skippy_s s) (skippy_k k') |
---|
58 | | Kwhile e s k' ⇒ Kwhile e (skippy_s s) (skippy_k k') |
---|
59 | | Kdowhile e s k' ⇒ Kdowhile e (skippy_s s) (skippy_k k') |
---|
60 | | Kfor2 e s1 s2 k' ⇒ Kfor2 e (skippy_s s1) (skippy_s s2) (skippy_k k') |
---|
61 | | Kfor3 e s1 s2 k' ⇒ Kfor3 e (skippy_s s1) (skippy_s s2) (skippy_k k') |
---|
62 | | Kswitch k' ⇒ Kswitch (skippy_k k') |
---|
63 | | Kcall r f e k' ⇒ Kcall r f e (skippy_k k') |
---|
64 | ]. |
---|
65 | |
---|
66 | |
---|
67 | include "Plogic/equality.ma". |
---|
68 | include "Plogic/connectives.ma". |
---|
69 | |
---|
70 | ndefinition skippy_state : state → state ≝ λs:state. |
---|
71 | match s with |
---|
72 | [ State f s k e m ⇒ State (skippy_f f) (skippy_s s) (skippy_k k) e m |
---|
73 | | Callstate fd args k m ⇒ Callstate (skippy_fd fd) args (skippy_k k) m |
---|
74 | | Returnstate res k m ⇒ Returnstate res (skippy_k k) m |
---|
75 | ]. |
---|
76 | (* |
---|
77 | ndefinition skippyeq : state → state → Prop ≝ λs,s':state. |
---|
78 | match s with |
---|
79 | [ State f s k e m ⇒ |
---|
80 | match s' with |
---|
81 | [ State f' s' k' e' m' ⇒ (skippy_f f) = f' ∧ (skippy_s s) = s' ∧ (skippy_k k) = k' ∧ m = m' |
---|
82 | | _ ⇒ False |
---|
83 | ] |
---|
84 | | Callstate fd args k m ⇒ |
---|
85 | match s' with |
---|
86 | [ Callstate fd' args' k' m' ⇒ (skippy_fd fd) = fd' ∧ args = args' ∧ (skippy_k k) = k' ∧ m = m' |
---|
87 | | _ ⇒ False |
---|
88 | ] |
---|
89 | | Returnstate res k m ⇒ |
---|
90 | match s' with |
---|
91 | [ Returnstate res' k' m' ⇒ res = res' ∧ (skippy_k k) = k' ∧ m = m' |
---|
92 | | _ ⇒ False |
---|
93 | ] |
---|
94 | ]. |
---|
95 | *) |
---|
96 | ndefinition skippy_eq : state → state → Prop ≝ λs,s':state. (skippy_state s) = s'. |
---|
97 | |
---|
98 | ndefinition skippysim ≝ λp:program. |
---|
99 | mk_simulation |
---|
100 | (mk_related_semantics |
---|
101 | (Csem p) |
---|
102 | (Csem (skippy p)) |
---|
103 | (globalenv Genv ?? p) |
---|
104 | (globalenv Genv ?? (skippy p)) |
---|
105 | ? |
---|
106 | ? |
---|
107 | ?) |
---|
108 | ?. |
---|
109 | ##[ ##3: napply skippy_eq; |
---|
110 | ##| #st1 st2 r e H; ninversion H; #i m e1 e2; ndestruct; //; |
---|
111 | ##| #st1 H; ninversion H; #b f H1 H2 e1; @ (skippy_state st1); |
---|
112 | nrewrite > e1; @; //; |
---|
113 | nwhd; nwhd in ⊢ (??%); napply (initial_state_intro … b); |
---|
114 | nrewrite > rewrite_skippy; |
---|
115 | ##[ nrewrite > (find_symbol_transf Genv …); napply H1; |
---|
116 | ##| nrewrite > (find_funct_ptr_transf Genv …); //; |
---|
117 | ##] |
---|
118 | ##| #st1 st2 t st1' H e; |
---|
119 | @ (skippy_state st1'); |
---|
120 | @; //; |
---|
121 | (* simulation proof *) |
---|
122 | (* First, get a hold of the states being executed. *) |
---|
123 | nelim st1 in H e ⊢ %; |
---|
124 | ##[ #f1 s1 k1 e1 m1; nelim s1; |
---|
125 | ##[ nelim k1; |
---|
126 | ##[ nelim f1; #ty args vars body; ncases ty; |
---|
127 | ##[ #H e; nwhd in H; |
---|
128 | nnormalize in e; @ (1); nrewrite < e; nwhd; ndestruct; //; |
---|
129 | ##| ##2,5,6,7,8: #A B H; nwhd in H; napply (False_ind … H); |
---|
130 | ##| ##3,4,9: #A H; nwhd in H; napply (False_ind … H); |
---|
131 | ##] |
---|
132 | ##| |
---|
133 | |
---|
134 | *) |
---|