1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
|
(** Refinement of BTL_SEtheory data-structures
in order to introduce (and prove correct) a lower-level specification of the simulation test.
Ceci est un "bac à sable". TODO: A REVOIR COMPLETEMENT. Introduire "fake" hash-consing
- On introduit une représentation plus concrète pour les types d'état symbolique [sistate] et [sstate].
- Etant donné une spécification intuitive "*_simu" pour tester la simulation sur cette représentation des états symboliques,
on essaye déjà de trouver les bonnes notions de raffinement "*_refines" qui permette de prouver les lemmes "*_simu_correct".
- Il faudra ensuite vérifier que l'exécution symbolique préserve ces relations de raffinement !
*)
Require Import Coqlib Maps Floats.
Require Import AST Integers Values Events Memory Globalenvs Smallstep.
Require Import Op Registers.
Require Import RTL BTL OptionMonad BTL_SEtheory.
(** * ... *)
Record sis_ok ctx (sis: sistate): Prop := {
OK_PRE: (sis.(si_pre) ctx);
OK_SMEM: eval_smem ctx sis.(si_smem) <> None;
OK_SREG: forall (r: reg), eval_sval ctx (si_sreg sis r) <> None
}.
Local Hint Resolve OK_PRE OK_SMEM OK_SREG: core.
Local Hint Constructors sis_ok: core.
Lemma sem_sok ctx sis rs m:
sem_sistate ctx sis rs m -> sis_ok ctx sis.
Proof.
unfold sem_sistate;
econstructor;
intuition congruence.
Qed.
(* NB: refinement of (symbolic) internal state *)
Record ristate :=
{
(** [ris_smem] represents the current smem symbolic evaluations.
(we also recover the history of smem in ris_smem) *)
ris_smem: smem;
(** For the values in registers:
1) we store a list of sval evaluations
2) we encode the symbolic regset by a PTree + a boolean indicating the default sval *)
ris_input_init: bool;
ris_ok_sval: list sval;
ris_sreg:> PTree.t sval
}.
Definition ris_sreg_get (ris: ristate) r: sval :=
match PTree.get r ris with
| None => if ris_input_init ris then Sinput r else Sundef
| Some sv => sv
end.
Coercion ris_sreg_get: ristate >-> Funclass.
Record ris_ok ctx (ris: ristate) : Prop := {
OK_RMEM: (eval_smem ctx (ris_smem ris)) <> None;
OK_RREG: forall sv, List.In sv (ris_ok_sval ris) -> eval_sval ctx sv <> None
}.
Local Hint Resolve OK_RMEM OK_RREG: core.
Local Hint Constructors ris_ok: core.
Record ris_refines ctx (ris: ristate) (sis: sistate): Prop := {
OK_EQUIV: sis_ok ctx sis <-> ris_ok ctx ris;
MEM_EQ: ris_ok ctx ris -> eval_smem ctx ris.(ris_smem) = eval_smem ctx sis.(si_smem);
REG_EQ: ris_ok ctx ris -> forall r, eval_sval ctx (ris_sreg_get ris r) = eval_sval ctx (si_sreg sis r);
(* the below invariant allows to evaluate operations in the initial memory of the path instead of the current memory *)
VALID_PRESERV: forall m b ofs, eval_smem ctx sis.(si_smem) = Some m -> Mem.valid_pointer m b ofs = Mem.valid_pointer (cm0 ctx) b ofs
}.
Local Hint Resolve OK_EQUIV MEM_EQ REG_EQ VALID_PRESERV: core.
Local Hint Constructors ris_refines: core.
Record ris_simu ris1 ris2: Prop := {
SIMU_FAILS: forall sv, List.In sv ris2.(ris_ok_sval) -> List.In sv ris1.(ris_ok_sval);
SIMU_MEM: ris1.(ris_smem) = ris2.(ris_smem);
SIMU_REG: forall r, ris_sreg_get ris1 r = ris_sreg_get ris2 r
}.
Local Hint Resolve SIMU_FAILS SIMU_MEM SIMU_REG: core.
Local Hint Constructors ris_simu: core.
Local Hint Resolve sge_match: core.
Lemma ris_simu_ok_preserv f1 f2 ris1 ris2 (ctx:simu_proof_context f1 f2):
ris_simu ris1 ris2 -> ris_ok (bctx1 ctx) ris1 -> ris_ok (bctx2 ctx) ris2.
Proof.
intros SIMU OK; econstructor; eauto.
- erewrite <- SIMU_MEM; eauto.
erewrite <- smem_eval_preserved; eauto.
- intros; erewrite <- eval_sval_preserved; eauto.
Qed.
Lemma ris_simu_correct f1 f2 ris1 ris2 (ctx:simu_proof_context f1 f2) sis1 sis2 rs m:
ris_simu ris1 ris2 ->
ris_refines (bctx1 ctx) ris1 sis1 ->
ris_refines (bctx2 ctx) ris2 sis2 ->
sem_sistate (bctx1 ctx) sis1 rs m ->
sem_sistate (bctx2 ctx) sis2 rs m.
Proof.
intros RIS REF1 REF2 SEM.
exploit sem_sok; eauto.
erewrite OK_EQUIV; eauto.
intros ROK1.
exploit ris_simu_ok_preserv; eauto.
intros ROK2. generalize ROK2; erewrite <- OK_EQUIV; eauto.
intros SOK2.
destruct SEM as (PRE & SMEM & SREG).
unfold sem_sistate; intuition eauto.
+ erewrite <- MEM_EQ, <- SIMU_MEM; eauto.
erewrite <- smem_eval_preserved; eauto.
erewrite MEM_EQ; eauto.
+ erewrite <- REG_EQ, <- SIMU_REG; eauto.
erewrite <- eval_sval_preserved; eauto.
erewrite REG_EQ; eauto.
Qed.
(* TODO:
Definition option_refines ctx (orsv: option sval) (osv: option sval) :=
match orsv, osv with
| Some rsv, Some sv => eval_sval ctx rsv = eval_sval ctx sv
| None, None => True
| _, _ => False
end.
Definition sum_refines ctx (rsi: sval + ident) (si: sval + ident) :=
match rsi, si with
| inl rsv, inl sv => eval_sval ctx rsv = eval_sval ctx sv
| inr id, inr id' => id = id'
| _, _ => False
end.
Definition bargs_refines ctx (rargs: list (builtin_arg sval)) (args: list (builtin_arg sval)): Prop :=
eval_list_builtin_sval ctx rargs = eval_list_builtin_sval ctx args.
Inductive rfv_refines ctx: sfval -> sfval -> Prop :=
| refines_Sgoto pc: rfv_refines ctx (Sgoto pc) (Sgoto pc)
| refines_Scall: forall sig rvos ros rargs args r pc
(SUM:sum_refines ctx rvos ros)
(LIST:eval_list_sval ctx rargs = eval_list_sval ctx args)
,rfv_refines ctx (Scall sig rvos rargs r pc) (Scall sig ros args r pc)
| refines_Stailcall: forall sig rvos ros rargs args
(SUM:sum_refines ctx rvos ros)
(LIST:eval_list_sval ctx rargs = eval_list_sval ctx args)
,rfv_refines ctx (Stailcall sig rvos rargs) (Stailcall sig ros args)
| refines_Sbuiltin: forall ef lbra lba br pc
(BARGS: bargs_refines ctx lbra lba)
,rfv_refines ctx (Sbuiltin ef lbra br pc) (Sbuiltin ef lba br pc)
| refines_Sjumptable: forall rsv sv lpc
(VAL: eval_sval ctx rsv = eval_sval ctx sv)
,rfv_refines ctx (Sjumptable rsv lpc) (Sjumptable sv lpc)
| refines_Sreturn: forall orsv osv
(OPT:option_refines ctx orsv osv)
,rfv_refines ctx (Sreturn orsv) (Sreturn osv)
.
Definition rfv_simu (rfv1 rfv2: sfval): Prop := rfv1 = rfv2.
Local Hint Constructors sem_sfval equiv_state: core.
Lemma rvf_simu_correct f1 f2 rfv1 rfv2 (ctx: simu_proof_context f1 f2) sfv1 sfv2 rs m t s:
rfv_simu rfv1 rfv2 ->
rfv_refines (bctx1 ctx) rfv1 sfv1 ->
rfv_refines (bctx2 ctx) rfv2 sfv2 ->
sem_sfval (bctx1 ctx) sfv1 rs m t s ->
exists s', sem_sfval (bctx2 ctx) sfv2 rs m t s' /\ equiv_state s s'.
Proof.
unfold rfv_simu; intros X REF1 REF2 SEM. subst.
unfold bctx2; destruct REF1; inv REF2; inv SEM; simpl.
- eexists; split; eauto; simpl.
(* eapply State_equiv; eauto. NE MARCHE PAS ! *)
Admitted.
(* refinement of (symbolic) state *)
Inductive rstate :=
| Rfinal (ris: ristate) (rfv: sfval)
| Rcond (cond: condition) (rargs: list_sval) (rifso rifnot: rstate)
| Rabort
.
Inductive rst_simu: rstate -> rstate -> Prop :=
| Rfinal_simu ris1 ris2 rfv1 rfv2:
ris_simu ris1 ris2 ->
rfv_simu rfv1 rfv2 ->
rst_simu (Rfinal ris1 rfv1) (Rfinal ris2 rfv2)
| Rcond_simu cond rargs rifso1 rifnot1 rifso2 rifnot2:
rst_simu rifso1 rifso2 ->
rst_simu rifnot1 rifnot2 ->
rst_simu (Rcond cond rargs rifso1 rifnot1) (Rcond cond rargs rifso2 rifnot2)
| Rabort_simu: rst_simu Rabort Rabort
(* TODO: extension à voir dans un second temps !
| Rcond_skip cond rargs rifso1 rifnot1 rst:
rst_simu rifso1 rst ->
rst_simu rifnot1 rst ->
rst_simu (Rcond cond rargs rifso1 rifnot1) rst
*)
.
(* Comment prend on en compte le ris en cours d'execution ??? *)
Inductive rst_refines ctx: (* Prop -> *) rstate -> sstate -> Prop :=
| refines_Sfinal ris sis rfv sfv (*ok: Prop*)
(*OK: ris_ok ctx ris -> ok*)
(RIS: ris_refines ctx ris sis)
(RFV: ris_ok ctx ris -> rfv_refines ctx rfv sfv)
: rst_refines ctx (*ok*) (Rfinal ris rfv) (Sfinal sis sfv)
| refines_Scond cond rargs args sm rifso rifnot ifso ifnot (*ok1 ok2: Prop*)
(*OK1: ok2 -> ok1*)
(RCOND: (* ok2 -> *) seval_condition ctx cond rargs Sinit = seval_condition ctx cond args sm)
(REFso: seval_condition ctx cond rargs Sinit = Some true -> rst_refines ctx (*ok2*) rifso ifso)
(REFnot: seval_condition ctx cond rargs Sinit = Some false -> rst_refines ctx (*ok2*) rifnot ifnot)
: rst_refines ctx (*ok1*) (Rcond cond rargs rifso rifnot) (Scond cond args sm ifso ifnot)
| refines_Sabort
: rst_refines ctx Rabort Sabort
.
Lemma rst_simu_correct rst1 rst2:
rst_simu rst1 rst2 ->
forall f1 f2 (ctx: simu_proof_context f1 f2) st1 st2 (*ok1 ok2*),
rst_refines (*ok1*) (bctx1 ctx) rst1 st1 ->
rst_refines (*ok2*) (bctx2 ctx) rst2 st2 ->
(* ok1 -> ok2 -> *)
sstate_simu ctx st1 st2.
Proof.
induction 1; simpl; auto.
- (* final *) intros f1 f2 ctx st1 st2 REF1 REF2 t s1 SEM1.
inv REF1. inv REF2. inv SEM1.
exploit sem_sok; eauto.
rewrite OK_EQUIV; eauto.
intros RIS_OK1.
exploit (ris_simu_ok_preserv f1 f2); eauto.
intros RIS_OK2. intuition.
exploit ris_simu_correct; eauto.
exploit rvf_simu_correct; eauto.
simpl. (*
eexists; split.
+ econstructor; eauto.
simpl.
clear SIS.
admit. (* TODO: condition sur les tr_inputs du simu_proof_context ! *)
(* TODO: le rfv_refines est trop sémantique ! *)
+ admit.
- (* cond *) intros f1 f2 ctx st1 st2 REF1 REF2 t s1 SEM1.
inv REF1. inv REF2. inv SEM1.
destruct b; simpl.
+ assert (TODO1: rst_refines (bctx1 ctx) rifso1 ifso). admit.
assert (TODO2: rst_refines (bctx2 ctx) rifso2 ifso0). admit.
exploit IHrst_simu1; eauto.
intros (s2 & X1 & X2).
exists s2; split; eauto.
econstructor; eauto.
* assert (TODO3: seval_condition (bctx2 ctx) cond args0 sm0 = Some true). admit.
eauto.
* simpl; eauto.
+ admit.
- (* abort *) intros f1 f2 ctx st1 st2 REF1 REF2 t s1 SEM1.
inv REF1. inv SEM1.
*)
Admitted.
*)
|
