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
|
(*
* Vericert: Verified high-level synthesis.
* Copyright (C) 2020-2022 Yann Herklotz <yann@yannherklotz.com>
*
* This program is free software: you can redistribute it and/or modify
* it under the terms of the GNU General Public License as published by
* the Free Software Foundation, either version 3 of the License, or
* (at your option) any later version.
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
* You should have received a copy of the GNU General Public License
* along with this program. If not, see <https://www.gnu.org/licenses/>.
*)
Require Import compcert.backend.Registers.
Require Import compcert.common.AST.
Require Import compcert.common.Events.
Require Import compcert.common.Globalenvs.
Require Import compcert.common.Memory.
Require Import compcert.common.Smallstep.
Require Import compcert.common.Values.
Require Import compcert.lib.Coqlib.
Require Import compcert.lib.Integers.
Require Import compcert.lib.Maps.
Require Import compcert.verilog.Op.
Require Import vericert.common.Vericertlib.
Require Import vericert.hls.Gible.
Require Import vericert.hls.Predicate.
(*|
========
GibleSeq
========
|*)
Module SeqBB <: BlockType.
Definition t := list instr.
Definition foldl {A: Type}: (A -> instr -> A) -> t -> A -> A := @fold_left A instr.
Definition length : t -> nat := @length instr.
(*|
Instruction list step
---------------------
The ``step_instr_list`` definition describes the execution of a list of
instructions in one big step, inductively traversing the list of instructions
and applying the ``step_instr``.
This is simply using the high-level function ``step_list``, which is a general
function that can execute lists of things, given their execution rule.
|*)
Definition step {A B: Type} (ge: Genv.t A B) := step_list (step_instr ge).
End SeqBB.
Module GibleSeq := Gible(SeqBB).
Export GibleSeq.
Fixpoint replace_section {A: Type} (f: A -> instr -> (A * SeqBB.t)) (s: A) (b: SeqBB.t): A * SeqBB.t :=
match b with
| i :: b' =>
let (s', b'') := replace_section f s b' in
let (s'', i') := f s' i in
(s'', i' ++ b'')
| nil => (s, nil)
end.
Lemma forbidden_term_trans :
forall A B ge sp i c b i' c',
~ @SeqBB.step A B ge sp (Iterm i c) b (Iterm i' c').
Proof. induction b; unfold not; intros; inv H. Qed.
Lemma step_instr_false :
forall A B ge sp i c a i0,
~ @step_instr A B ge sp (Iterm i c) a (Iexec i0).
Proof. destruct a; unfold not; intros; inv H. Qed.
Lemma step_list_false :
forall A B ge sp a i0 s,
~ step_list (@step_instr A B ge) sp s a (Iexec i0).
Proof. destruct a; unfold not; intros; inv H. Qed.
Lemma step_list2_false :
forall A B ge l0 sp i c i0',
~ step_list2 (@step_instr A B ge) sp (Iterm i c) l0 (Iexec i0').
Proof.
induction l0; unfold not; intros.
inv H. inv H. destruct i1. eapply step_instr_false in H4. auto.
eapply IHl0; eauto.
Qed.
Lemma append' :
forall A B l0 cf i0 i1 l1 sp ge i0',
step_list2 (@step_instr A B ge) sp (Iexec i0) l0 (Iexec i0') ->
@SeqBB.step A B ge sp (Iexec i0') l1 (Iterm i1 cf) ->
@SeqBB.step A B ge sp (Iexec i0) (l0 ++ l1) (Iterm i1 cf).
Proof.
induction l0; crush. inv H. eauto. inv H. destruct i3.
econstructor; eauto. eapply IHl0; eauto.
eapply step_list2_false in H7. exfalso; auto.
Qed.
Lemma append :
forall A B cf i0 i1 l0 l1 sp ge,
(exists i0', step_list2 (@step_instr A B ge) sp (Iexec i0) l0 (Iexec i0') /\
@SeqBB.step A B ge sp (Iexec i0') l1 (Iterm i1 cf)) ->
@SeqBB.step A B ge sp (Iexec i0) (l0 ++ l1) (Iterm i1 cf).
Proof. intros. simplify. eapply append'; eauto. Qed.
Lemma append2 :
forall A B l0 cf i0 i1 l1 sp ge,
@SeqBB.step A B ge sp (Iexec i0) l0 (Iterm i1 cf) ->
@SeqBB.step A B ge sp (Iexec i0) (l0 ++ l1) (Iterm i1 cf).
Proof.
induction l0; crush.
inv H.
inv H. econstructor; eauto. eapply IHl0; eauto.
constructor; auto.
Qed.
#[local] Notation "'mki'" := (mk_instr_state) (at level 1).
Lemma exec_rbexit_truthy :
forall A B bb ge sp rs pr m rs' pr' m' cf,
@SeqBB.step A B ge sp (Iexec (mki rs pr m)) bb (Iterm (mki rs' pr' m') cf) ->
exists p b1 b2,
truthy pr' p
/\ bb = b1 ++ (RBexit p cf) :: b2
/\ step_list2 (Gible.step_instr ge) sp (Iexec (mki rs pr m)) b1 (Iexec (mki rs' pr' m')).
Proof.
induction bb; crush.
inv H. inv H.
- destruct state'. exploit IHbb; eauto; simplify.
exists x. exists (a :: x0). exists x1. simplify; auto.
econstructor; eauto.
- inv H3.
exists p. exists nil. exists bb. crush.
constructor.
Qed.
#[local] Open Scope positive.
Lemma max_pred_function_use :
forall f pc bb i p,
f.(fn_code) ! pc = Some bb ->
In i bb ->
In p (pred_uses i) ->
p <= max_pred_function f.
Proof. Admitted.
Ltac truthy_falsy :=
match goal with
| H: instr_falsy ?ps (RBop ?p _ _ _), H2: truthy ?ps ?p |- _ =>
solve [inv H2; inv H; crush]
| H: instr_falsy ?ps (RBload ?p _ _ _ _), H2: truthy ?ps ?p |- _ =>
solve [inv H2; inv H; crush]
| H: instr_falsy ?ps (RBstore ?p _ _ _ _), H2: truthy ?ps ?p |- _ =>
solve [inv H2; inv H; crush]
| H: instr_falsy ?ps (RBexit ?p _), H2: truthy ?ps ?p |- _ =>
solve [inv H2; inv H; crush]
| H: instr_falsy ?ps (RBsetpred ?p _ _ _), H2: truthy ?ps ?p |- _ =>
solve [inv H2; inv H; crush]
end.
Lemma exec_determ :
forall A B ge sp s1 a s2 s2',
@step_instr A B ge sp s1 a s2 ->
step_instr ge sp s1 a s2' ->
s2 = s2'.
Proof.
inversion 1; subst; crush.
- inv H0; auto.
- inv H2; crush; truthy_falsy.
- inv H3; crush. truthy_falsy.
- inv H3; crush. truthy_falsy.
- inv H2; crush. truthy_falsy.
- inv H1; crush. truthy_falsy.
- destruct st; simplify. inv H1; crush; truthy_falsy.
Qed.
Lemma append3 :
forall A B l0 l1 sp ge s1 s2 s3,
step_list2 (step_instr ge) sp s1 l0 (Iexec s2) ->
@SeqBB.step A B ge sp s1 (l0 ++ l1) s3 ->
@SeqBB.step A B ge sp (Iexec s2) l1 s3.
Proof.
induction l0; crush. inv H. auto.
inv H0. inv H. assert (i1 = (Iexec state')) by (eapply exec_determ; eauto). subst. eauto.
inv H. assert (i1 = (Iterm state' cf)) by (eapply exec_determ; eauto). subst.
exfalso; eapply step_list2_false; eauto.
Qed.
|
