|
1
|
(* ---------------------------------------------------------- *)
|
|
2
|
(* --- Global Definitions --- *)
|
|
3
|
(* ---------------------------------------------------------- *)
|
|
4
|
|
|
5
|
Require Import ZArith.
|
|
6
|
Require Import Reals.
|
|
7
|
Require Import BuiltIn.
|
|
8
|
Require Import bool.Bool.
|
|
9
|
Require Import int.Int.
|
|
10
|
Require Import int.Abs.
|
|
11
|
Require Import int.ComputerDivision.
|
|
12
|
Require Import real.Real.
|
|
13
|
Require Import real.RealInfix.
|
|
14
|
Require Import real.FromInt.
|
|
15
|
Require Import map.Map.
|
|
16
|
Require Import Qedlib.
|
|
17
|
Require Import Qed.
|
|
18
|
Require Import S_g_mem_pack.
|
|
19
|
Require Import Cint.
|
|
20
|
|
|
21
|
Definition P_clock_g__g_2 : Prop := True.
|
|
22
|
|
|
23
|
Require Import S_g_reg.
|
|
24
|
|
|
25
|
Definition P_trans_g__g_2 (mem_out_0 : S_g_mem_pack) (y : Z) : Prop :=
|
|
26
|
(y = (F_g_reg___g_2 (F_g_mem_pack__reg mem_out_0)))%Z.
|
|
27
|
|
|
28
|
Definition P_clock_gout (c_in_0 : Z) : Prop := (0 = c_in_0)%Z.
|
|
29
|
|
|
30
|
Definition P_trans_gout (out_out_0 : Z) (y : Z) : Prop := (out_out_0 = y)%Z.
|
|
31
|
|
|
32
|
Definition P_trans_gA : Prop := True.
|
|
33
|
|
|
34
|
Definition P_clock_g__g_1 : Prop := True.
|
|
35
|
|
|
36
|
Require Import S__arrow_mem_pack.
|
|
37
|
Require Import S__arrow_reg.
|
|
38
|
|
|
39
|
Definition P_trans_arrow (mem_in_0 : S__arrow_mem_pack)
|
|
40
|
(mem_out_0 : S__arrow_mem_pack) (out_0 : Z) : Prop :=
|
|
41
|
let x := (F__arrow_reg__first (F__arrow_mem_pack__reg mem_in_0))%Z in
|
|
42
|
let x_1 := (F__arrow_reg__first (F__arrow_mem_pack__reg mem_out_0))%Z in
|
|
43
|
itep (((out_0 = x)%Z) /\ ((0 <> x)%Z)) ((0 = x_1)%Z) ((x = x_1)%Z).
|
|
44
|
|
|
45
|
Definition P_trans_g__g_1 (mem_in_0 : S_g_mem_pack)
|
|
46
|
(mem_out_0 : S_g_mem_pack) (__g_1_0 : Z) : Prop :=
|
|
47
|
(P_trans_arrow (F_g_mem_pack_ni_1 mem_in_0) (F_g_mem_pack_ni_1 mem_out_0)
|
|
48
|
__g_1_0%Z).
|
|
49
|
|
|
50
|
Definition P_trans_gB (mem_in_0 : S_g_mem_pack) (mem_out_0 : S_g_mem_pack)
|
|
51
|
(__g_1_0 : Z) : Prop :=
|
|
52
|
(P_trans_gA) /\
|
|
53
|
((P_clock_g__g_1) -> ((P_trans_g__g_1 mem_in_0 mem_out_0 __g_1_0%Z))).
|
|
54
|
|
|
55
|
Definition P_clock_glast_y : Prop := True.
|
|
56
|
|
|
57
|
Definition P_trans_glast_y (mem_in_0 : S_g_mem_pack) (__g_1_0 : Z)
|
|
58
|
(last_y_0 : Z) : Prop :=
|
|
59
|
itep ((0 = __g_1_0)%Z)
|
|
60
|
((last_y_0 = (F_g_reg___g_2 (F_g_mem_pack__reg mem_in_0)))%Z)
|
|
61
|
((0 = last_y_0)%Z).
|
|
62
|
|
|
63
|
Definition P_trans_gC (mem_in_0 : S_g_mem_pack) (mem_out_0 : S_g_mem_pack)
|
|
64
|
(last_y_0 : Z) : Prop :=
|
|
65
|
exists i : Z, ((is_uint32 i%Z)) /\
|
|
66
|
((P_trans_gB mem_in_0 mem_out_0 i%Z)) /\
|
|
67
|
((P_clock_glast_y) -> ((P_trans_glast_y mem_in_0 i%Z last_y_0%Z))).
|
|
68
|
|
|
69
|
Definition P_clock_gt : Prop := True.
|
|
70
|
|
|
71
|
Definition P_trans_gt (c_in_0 : Z) (x_in_0 : Z) (last_y_0 : Z) (t : Z)
|
|
72
|
: Prop := itep ((0 = c_in_0)%Z) ((last_y_0 = t)%Z) ((t = x_in_0)%Z).
|
|
73
|
|
|
74
|
Definition P_trans_gD (c_in_0 : Z) (x_in_0 : Z) (mem_in_0 : S_g_mem_pack)
|
|
75
|
(mem_out_0 : S_g_mem_pack) (t : Z) : Prop :=
|
|
76
|
exists i : Z, ((is_sint32 i%Z)) /\
|
|
77
|
((P_trans_gC mem_in_0 mem_out_0 i%Z)) /\
|
|
78
|
((P_clock_gt) -> ((P_trans_gt c_in_0%Z x_in_0%Z i%Z t%Z))).
|
|
79
|
|
|
80
|
Definition P_clock_gy : Prop := True.
|
|
81
|
|
|
82
|
Require Import S_f_mem_pack.
|
|
83
|
|
|
84
|
Definition P_clock_f__f_2 : Prop := True.
|
|
85
|
|
|
86
|
Require Import S_f_reg.
|
|
87
|
|
|
88
|
Definition P_trans_f__f_2 (mem_out_0 : S_f_mem_pack) (cpt_out_0 : Z)
|
|
89
|
: Prop := (cpt_out_0 = (F_f_reg___f_2 (F_f_mem_pack__reg mem_out_0)))%Z.
|
|
90
|
|
|
91
|
Definition P_clock_fcpt : Prop := True.
|
|
92
|
|
|
93
|
Definition P_trans_fcpt (__f_3_0 : Z) (cpt_out_0 : Z) : Prop :=
|
|
94
|
(cpt_out_0 = (1 + __f_3_0))%Z.
|
|
95
|
|
|
96
|
Definition P_trans_fA : Prop := True.
|
|
97
|
|
|
98
|
Definition P_clock_fy : Prop := True.
|
|
99
|
|
|
100
|
Definition P_trans_fy (x_in_0 : Z) (y_out_0 : Z) : Prop :=
|
|
101
|
(y_out_0 = (1 + x_in_0))%Z.
|
|
102
|
|
|
103
|
Definition P_trans_fB (x_in_0 : Z) (y_out_0 : Z) : Prop :=
|
|
104
|
(P_trans_fA) /\ ((P_clock_fy) -> ((P_trans_fy x_in_0%Z y_out_0%Z))).
|
|
105
|
|
|
106
|
Definition P_clock_f__f_1 : Prop := True.
|
|
107
|
|
|
108
|
Definition P_trans_f__f_1 (mem_in_0 : S_f_mem_pack)
|
|
109
|
(mem_out_0 : S_f_mem_pack) (__f_1_0 : Z) : Prop :=
|
|
110
|
(P_trans_arrow (F_f_mem_pack_ni_2 mem_in_0) (F_f_mem_pack_ni_2 mem_out_0)
|
|
111
|
__f_1_0%Z).
|
|
112
|
|
|
113
|
Definition P_trans_fC (x_in_0 : Z) (mem_in_0 : S_f_mem_pack)
|
|
114
|
(mem_out_0 : S_f_mem_pack) (y_out_0 : Z) (__f_1_0 : Z) : Prop :=
|
|
115
|
((P_trans_fB x_in_0%Z y_out_0%Z)) /\
|
|
116
|
((P_clock_f__f_1) -> ((P_trans_f__f_1 mem_in_0 mem_out_0 __f_1_0%Z))).
|
|
117
|
|
|
118
|
Definition P_clock_f__f_3 : Prop := True.
|
|
119
|
|
|
120
|
Definition P_trans_f__f_3 (mem_in_0 : S_f_mem_pack) (__f_1_0 : Z)
|
|
121
|
(__f_3_0 : Z) : Prop :=
|
|
122
|
itep ((0 = __f_1_0)%Z)
|
|
123
|
((__f_3_0 = (F_f_reg___f_2 (F_f_mem_pack__reg mem_in_0)))%Z)
|
|
124
|
((0 = __f_3_0)%Z).
|
|
125
|
|
|
126
|
Definition P_trans_fD (x_in_0 : Z) (mem_in_0 : S_f_mem_pack)
|
|
127
|
(mem_out_0 : S_f_mem_pack) (y_out_0 : Z) (__f_3_0 : Z) : Prop :=
|
|
128
|
exists i : Z, ((is_uint32 i%Z)) /\
|
|
129
|
((P_trans_fC x_in_0%Z mem_in_0 mem_out_0 y_out_0%Z i%Z)) /\
|
|
130
|
((P_clock_f__f_3) -> ((P_trans_f__f_3 mem_in_0 i%Z __f_3_0%Z))).
|
|
131
|
|
|
132
|
Definition P_trans_fE (x_in_0 : Z) (mem_in_0 : S_f_mem_pack)
|
|
133
|
(mem_out_0 : S_f_mem_pack) (y_out_0 : Z) (cpt_out_0 : Z) : Prop :=
|
|
134
|
exists i : Z, ((is_sint32 i%Z)) /\
|
|
135
|
((P_clock_fcpt) -> ((P_trans_fcpt i%Z cpt_out_0%Z))) /\
|
|
136
|
((P_trans_fD x_in_0%Z mem_in_0 mem_out_0 y_out_0%Z i%Z)).
|
|
137
|
|
|
138
|
Definition P_trans_fF (x_in_0 : Z) (mem_in_0 : S_f_mem_pack)
|
|
139
|
(mem_out_0 : S_f_mem_pack) (y_out_0 : Z) (cpt_out_0 : Z) : Prop :=
|
|
140
|
((P_clock_f__f_2) -> ((P_trans_f__f_2 mem_out_0 cpt_out_0%Z))) /\
|
|
141
|
((P_trans_fE x_in_0%Z mem_in_0 mem_out_0 y_out_0%Z cpt_out_0%Z)).
|
|
142
|
|
|
143
|
Definition P_trans_gy (mem_in_0 : S_g_mem_pack) (mem_out_0 : S_g_mem_pack)
|
|
144
|
(t : Z) (y : Z) (cpt_0 : Z) : Prop :=
|
|
145
|
(P_trans_fF t%Z (F_g_mem_pack_ni_0 mem_in_0)
|
|
146
|
(F_g_mem_pack_ni_0 mem_out_0) y%Z cpt_0%Z).
|
|
147
|
|
|
148
|
Definition P_trans_gE (c_in_0 : Z) (x_in_0 : Z) (mem_in_0 : S_g_mem_pack)
|
|
149
|
(mem_out_0 : S_g_mem_pack) (y : Z) : Prop :=
|
|
150
|
exists i_1 : Z, exists i : Z, ((is_sint32 i%Z)) /\ ((is_sint32 i_1%Z)) /\
|
|
151
|
((P_trans_gD c_in_0%Z x_in_0%Z mem_in_0 mem_out_0 i_1%Z)) /\
|
|
152
|
((P_clock_gy) -> ((P_trans_gy mem_in_0 mem_out_0 i_1%Z y%Z i%Z))).
|
|
153
|
|
|
154
|
Definition P_trans_gF (c_in_0 : Z) (x_in_0 : Z) (mem_in_0 : S_g_mem_pack)
|
|
155
|
(mem_out_0 : S_g_mem_pack) (out_out_0 : Z) (y : Z) : Prop :=
|
|
156
|
(((P_clock_gout c_in_0%Z)) -> ((P_trans_gout out_out_0%Z y%Z))) /\
|
|
157
|
((P_trans_gE c_in_0%Z x_in_0%Z mem_in_0 mem_out_0 y%Z)).
|
|
158
|
|
|
159
|
Definition P_trans_gG (c_in_0 : Z) (x_in_0 : Z) (mem_in_0 : S_g_mem_pack)
|
|
160
|
(mem_out_0 : S_g_mem_pack) (out_out_0 : Z) : Prop :=
|
|
161
|
exists i : Z, ((is_sint32 i%Z)) /\
|
|
162
|
((P_clock_g__g_2) -> ((P_trans_g__g_2 mem_out_0 i%Z))) /\
|
|
163
|
((P_trans_gF c_in_0%Z x_in_0%Z mem_in_0 mem_out_0 out_out_0%Z i%Z)).
|
|
164
|
Require Import Memory.
|
|
165
|
|
|
166
|
Require Import Compound.
|
|
167
|
|
|
168
|
Definition P_valid_f (Malloc_0 : array Z) (Mptr_0 : farray addr addr)
|
|
169
|
(self_0 : addr) : Prop :=
|
|
170
|
((valid_rw Malloc_0 self_0 2%Z)) /\
|
|
171
|
((valid_rw Malloc_0 (Mptr_0.[ (shiftfield_F_f_mem_ni_2 self_0) ]) 1%Z)).
|
|
172
|
|
|
173
|
Definition P_valid_g (Malloc_0 : array Z) (Mptr_0 : farray addr addr)
|
|
174
|
(self_0 : addr) : Prop :=
|
|
175
|
let a := Mptr_0.[ (shiftfield_F_g_mem_ni_0 self_0) ] in
|
|
176
|
((valid_rw Malloc_0 self_0 3%Z)) /\ ((valid_rw Malloc_0 a 2%Z)) /\
|
|
177
|
((valid_rw Malloc_0 (Mptr_0.[ (shiftfield_F_g_mem_ni_1 self_0) ]) 1%Z)) /\
|
|
178
|
((P_valid_f Malloc_0 Mptr_0 a)).
|
|
179
|
|
|
180
|
Definition P_g_pack0 : Prop := True.
|
|
181
|
|
|
182
|
Definition P__arrow_pack (Mint_0 : farray addr Z)
|
|
183
|
(memp_0 : S__arrow_mem_pack) (mem_0 : addr) : Prop :=
|
|
184
|
((F__arrow_reg__first (F__arrow_mem_pack__reg memp_0))
|
|
185
|
= (Mint_0.[ (shiftfield_F__arrow_reg__first
|
|
186
|
((shiftfield_F__arrow_mem__reg mem_0))) ]))%Z.
|
|
187
|
|
|
188
|
Definition P_g_pack1 (Mptr_0 : farray addr addr) (Mint_0 : farray addr Z)
|
|
189
|
(memp_0 : S_g_mem_pack) (mem_0 : addr) : Prop :=
|
|
190
|
(P_g_pack0) /\
|
|
191
|
((P__arrow_pack Mint_0 (F_g_mem_pack_ni_1 memp_0)
|
|
192
|
(Mptr_0.[ (shiftfield_F_g_mem_ni_1 mem_0) ]))).
|
|
193
|
|
|
194
|
Definition P_f_pack0 : Prop := True.
|
|
195
|
|
|
196
|
Definition P_f_pack1 (Mptr_0 : farray addr addr) (Mint_0 : farray addr Z)
|
|
197
|
(memp_0 : S_f_mem_pack) (mem_0 : addr) : Prop :=
|
|
198
|
(P_f_pack0) /\
|
|
199
|
((P__arrow_pack Mint_0 (F_f_mem_pack_ni_2 memp_0)
|
|
200
|
(Mptr_0.[ (shiftfield_F_f_mem_ni_2 mem_0) ]))).
|
|
201
|
|
|
202
|
Definition P_f_pack2 (Mptr_0 : farray addr addr) (Mint_0 : farray addr Z)
|
|
203
|
(memp_0 : S_f_mem_pack) (mem_0 : addr) : Prop :=
|
|
204
|
((P_f_pack1 Mptr_0 Mint_0 memp_0 mem_0)) /\
|
|
205
|
(((F_f_reg___f_2 (F_f_mem_pack__reg memp_0))
|
|
206
|
= (Mint_0.[ (shiftfield_F_f_reg___f_2
|
|
207
|
((shiftfield_F_f_mem__reg mem_0))) ]))%Z).
|
|
208
|
|
|
209
|
Definition P_g_pack2 (Mptr_0 : farray addr addr) (Mint_0 : farray addr Z)
|
|
210
|
(memp_0 : S_g_mem_pack) (mem_0 : addr) : Prop :=
|
|
211
|
((P_g_pack1 Mptr_0 Mint_0 memp_0 mem_0)) /\
|
|
212
|
((P_f_pack2 Mptr_0 Mint_0 (F_g_mem_pack_ni_0 memp_0)
|
|
213
|
(Mptr_0.[ (shiftfield_F_g_mem_ni_0 mem_0) ]))).
|
|
214
|
|
|
215
|
Definition P_g_pack3 (Mptr_0 : farray addr addr) (Mint_0 : farray addr Z)
|
|
216
|
(memp_0 : S_g_mem_pack) (mem_0 : addr) : Prop :=
|
|
217
|
((P_g_pack2 Mptr_0 Mint_0 memp_0 mem_0)) /\
|
|
218
|
(((F_g_reg___g_2 (F_g_mem_pack__reg memp_0))
|
|
219
|
= (Mint_0.[ (shiftfield_F_g_reg___g_2
|
|
220
|
((shiftfield_F_g_mem__reg mem_0))) ]))%Z).
|
|
221
|
|
|
222
|
Definition P_init_arrow (mem_in_0 : S__arrow_mem_pack) : Prop :=
|
|
223
|
(1 = (F__arrow_reg__first (F__arrow_mem_pack__reg mem_in_0)))%Z.
|
|
224
|
|
|
225
|
Definition P_init_f (mem_in_0 : S_f_mem_pack) : Prop :=
|
|
226
|
(P_init_arrow (F_f_mem_pack_ni_2 mem_in_0)).
|
|
227
|
|
|
228
|
Definition P_init_g (mem_in_0 : S_g_mem_pack) : Prop :=
|
|
229
|
((P_init_arrow (F_g_mem_pack_ni_1 mem_in_0))) /\
|
|
230
|
((P_init_f (F_g_mem_pack_ni_0 mem_in_0))).
|
|
231
|
|