Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / optim / oversampling / out / typed / Axiomatic.v @ 6a93d814

History | View | Annotate | Download (8.96 KB)

1 6a93d814 xthirioux
(* ---------------------------------------------------------- *)
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))).