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
|
Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
Require Import AST Linking.
Require Import Memory Registers Op RTL.
Require Import Inject.
Require Import Lia.
Local Open Scope positive.
Lemma inject_list_preserves:
forall l prog pc dst pc0,
pc0 < pc ->
PTree.get pc0 (snd (inject_list prog pc dst l)) = PTree.get pc0 prog.
Proof.
induction l; intros; simpl.
- apply PTree.gso. lia.
- rewrite IHl by lia.
apply PTree.gso. lia.
Qed.
Fixpoint pos_add_nat x n :=
match n with
| O => x
| S n' => Pos.succ (pos_add_nat x n')
end.
Lemma pos_add_nat_increases : forall x n, x <= (pos_add_nat x n).
Proof.
induction n; simpl; lia.
Qed.
Lemma pos_add_nat_succ : forall n x,
Pos.succ (pos_add_nat x n) = pos_add_nat (Pos.succ x) n.
Proof.
induction n; simpl; intros; trivial.
rewrite IHn.
reflexivity.
Qed.
Lemma inject_list_increases:
forall l prog pc dst,
(fst (inject_list prog pc dst l)) = pos_add_nat pc (S (List.length l)).
Proof.
induction l; simpl; intros; trivial.
rewrite IHl.
simpl.
rewrite <- pos_add_nat_succ.
reflexivity.
Qed.
Program Fixpoint bounded_nth
{T : Type} (k : nat) (l : list T) (BOUND : (k < List.length l)%nat) : T :=
match k, l with
| O, h::_ => h
| (S k'), _::l' => bounded_nth k' l' _
| _, nil => _
end.
Obligation 1.
Proof.
simpl in BOUND.
lia.
Qed.
Obligation 2.
Proof.
simpl in BOUND.
lia.
Qed.
Program Definition bounded_nth_S_statement : Prop :=
forall {T : Type} (k : nat) (h : T) (l : list T) (BOUND : (k < List.length l)%nat),
bounded_nth (S k) (h::l) _ = bounded_nth k l BOUND.
Obligation 1.
lia.
Qed.
Lemma bounded_nth_proof_irr :
forall {T : Type} (k : nat) (l : list T)
(BOUND1 BOUND2 : (k < List.length l)%nat),
(bounded_nth k l BOUND1) = (bounded_nth k l BOUND2).
Proof.
induction k; destruct l; simpl; intros; trivial; lia.
Qed.
Lemma bounded_nth_S : bounded_nth_S_statement.
Proof.
unfold bounded_nth_S_statement.
induction k; destruct l; simpl; intros; trivial.
1, 2: lia.
apply bounded_nth_proof_irr.
Qed.
Lemma inject_list_injected:
forall l prog pc dst k (BOUND : (k < (List.length l))%nat),
PTree.get (pos_add_nat pc k) (snd (inject_list prog pc dst l)) =
Some (inject_instr (bounded_nth k l BOUND) (Pos.succ (pos_add_nat pc k))).
Proof.
induction l; simpl; intros.
- lia.
- simpl.
destruct k as [ | k].
+ admit.
+ simpl pos_add_nat.
rewrite pos_add_nat_succ.
erewrite IHl.
f_equal. f_equal.
simpl.
apply bounded_nth_proof_irr.
Qed.
Lemma inject_at_preserves :
forall prog pc extra_pc l pc0,
pc0 < extra_pc ->
pc0 <> pc ->
PTree.get pc0 (snd (inject_at prog pc extra_pc l)) = PTree.get pc0 prog.
Proof.
intros. unfold inject_at.
destruct (PTree.get pc prog) eqn:GET.
- rewrite inject_list_preserves; trivial.
apply PTree.gso; lia.
- apply inject_list_preserves; trivial.
Qed.
Lemma inject_at_redirects:
forall prog pc extra_pc l i,
pc < extra_pc ->
PTree.get pc prog = Some i ->
PTree.get pc (snd (inject_at prog pc extra_pc l)) =
Some (alter_successor i extra_pc).
Proof.
intros until i. intros BEFORE GET. unfold inject_at.
rewrite GET.
rewrite inject_list_preserves by trivial.
apply PTree.gss.
Qed.
Lemma inject_at_redirects_none:
forall prog pc extra_pc l,
pc < extra_pc ->
PTree.get pc prog = None ->
PTree.get pc (snd (inject_at prog pc extra_pc l)) = None.
Proof.
intros until l. intros BEFORE GET. unfold inject_at.
rewrite GET.
rewrite inject_list_preserves by trivial.
assumption.
Qed.
Lemma inject_at_increases:
forall prog pc extra_pc l,
(fst (inject_at prog pc extra_pc l)) = pos_add_nat extra_pc (S (List.length l)).
Proof.
intros. unfold inject_at.
destruct (PTree.get pc prog).
all: apply inject_list_increases.
Qed.
Definition inject_l (prog : code) extra_pc injections :=
List.fold_left (fun already (injection : node * (list inj_instr)) =>
inject_at' already (fst injection) (snd injection))
injections
(extra_pc, prog).
Lemma pair_expand:
forall { A B : Type } (p : A*B),
p = ((fst p), (snd p)).
Proof.
destruct p; simpl; trivial.
Qed.
Lemma inject_l_preserves :
forall injections prog extra_pc pc0,
pc0 < extra_pc ->
List.forallb (fun injection => if peq (fst injection) pc0 then false else true) injections = true ->
PTree.get pc0 (snd (inject_l prog extra_pc injections)) = PTree.get pc0 prog.
Proof.
induction injections;
intros until pc0; intros BEFORE ALL; simpl; trivial.
unfold inject_l.
destruct a as [pc l]. simpl.
simpl in ALL.
rewrite andb_true_iff in ALL.
destruct ALL as [NEQ ALL].
rewrite pair_expand with (p := inject_at prog pc extra_pc l).
fold (inject_l (snd (inject_at prog pc extra_pc l))
(fst (inject_at prog pc extra_pc l))
injections).
rewrite IHinjections; trivial.
- apply inject_at_preserves; trivial.
destruct (peq pc pc0); congruence.
- rewrite inject_at_increases.
pose proof (pos_add_nat_increases extra_pc (S (Datatypes.length l))).
lia.
Qed.
Lemma inject'_preserves :
forall injections prog extra_pc pc0,
pc0 < extra_pc ->
PTree.get pc0 injections = None ->
PTree.get pc0 (snd (inject' prog extra_pc injections)) = PTree.get pc0 prog.
Proof.
intros. unfold inject'.
rewrite PTree.fold_spec.
change (fold_left
(fun (a : node * code) (p : positive * list inj_instr) =>
inject_at' a (fst p) (snd p)) (PTree.elements injections)
(extra_pc, prog)) with (inject_l prog extra_pc (PTree.elements injections)).
apply inject_l_preserves; trivial.
rewrite List.forallb_forall.
intros injection IN.
destruct injection as [pc l].
simpl.
apply PTree.elements_complete in IN.
destruct (peq pc pc0); trivial.
congruence.
Qed.
Lemma inject_preserves :
forall injections prog extra_pc pc0,
pc0 < extra_pc ->
PTree.get pc0 injections = None ->
PTree.get pc0 (inject prog extra_pc injections) = PTree.get pc0 prog.
Proof.
unfold inject'.
apply inject'_preserves.
Qed.
|
