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
260
261
262
263
264
265
|
[
"´p’¶„Ù¶°cøù©UyÄ™",
[
[
"LowStar.BufferView.Down.view",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b"
],
0,
"5c069096e8cbc02d7cb8b67f4b938964"
],
[
"LowStar.BufferView.Down.__proj__View__item__get",
1,
2,
1,
[ "@query" ],
0,
"82ada7726fce03944c527eff52aa3d18"
],
[
"LowStar.BufferView.Down.__proj__View__item__get",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_LowStar.BufferView.Down.view",
"proj_equation_LowStar.BufferView.Down.View_n",
"projection_inverse_LowStar.BufferView.Down.View_n"
],
0,
"fce20f67365cc6c918a53bbbcdd4d793"
],
[
"LowStar.BufferView.Down.__proj__View__item__put",
1,
2,
1,
[ "@query" ],
0,
"c45b2b3887bdc136c294403dd6e84391"
],
[
"LowStar.BufferView.Down.__proj__View__item__put",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"data_elim_LowStar.BufferView.Down.View",
"fuel_guarded_inversion_LowStar.BufferView.Down.view",
"proj_equation_LowStar.BufferView.Down.View_get",
"proj_equation_LowStar.BufferView.Down.View_n",
"projection_inverse_LowStar.BufferView.Down.View_get",
"projection_inverse_LowStar.BufferView.Down.View_n",
"projection_inverse_LowStar.BufferView.Down.View_put",
"refinement_interpretation_Tm_refine_f9ebca0c0880771b4cd34415a8fab184"
],
0,
"02944de9d8973d2e855ca45bd621088d"
],
[
"LowStar.BufferView.Down.as_buffer_mk_buffer_view",
1,
2,
1,
[ "@query" ],
0,
"54495b3074aadbd2a82d535da37cbb50"
],
[
"LowStar.BufferView.Down.get_view_mk_buffer_view",
1,
2,
1,
[ "@query" ],
0,
"9fd471d44f4f9d55ab23356f40f1c45e"
],
[
"LowStar.BufferView.Down.indexing",
1,
2,
1,
[ "@query" ],
0,
"6570923ff02ddb9cd9408777bf290c18"
],
[
"LowStar.BufferView.Down.sel_upd",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_9b448e7302c8037f5e88bf0160d1d4d1"
],
0,
"0b9b378b1fe2c4c1d2a64016f3c4445d"
],
[
"LowStar.BufferView.Down.lemma_upd_with_sel",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_9b448e7302c8037f5e88bf0160d1d4d1"
],
0,
"2a52b37d18e946cb5fee9f0b302c9488"
],
[
"LowStar.BufferView.Down.as_seq_sel",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_FStar.Seq.Properties.lseq",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"typing_LowStar.BufferView.Down.as_seq"
],
0,
"8f23becbb9627fb484330da2eac553e6"
],
[
"LowStar.BufferView.Down.get_sel",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"data_elim_FStar.Pervasives.Mkdtuple4",
"data_elim_LowStar.BufferView.Down.View",
"equation_FStar.Seq.Properties.lseq", "equation_FStar.UInt.min_int",
"equation_LowStar.BufferView.Down.as_buffer_t",
"equation_LowStar.BufferView.Down.buffer",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.logical",
"equation_Prims.nat", "equation_Prims.pos",
"fuel_guarded_inversion_FStar.Pervasives.dtuple4",
"fuel_guarded_inversion_LowStar.BufferView.Down.view",
"function_token_typing_Prims.logical", "int_inversion",
"interpretation_Tm_abs_2f52ee49857d060e683109f5fabb70fa",
"interpretation_Tm_abs_a8f4e254db91d3480d350b4b0b5a6525",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"primitive_Prims.op_Division", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply",
"proj_equation_FStar.Pervasives.Mkdtuple4__1",
"proj_equation_FStar.Pervasives.Mkdtuple4__2",
"proj_equation_FStar.Pervasives.Mkdtuple4__3",
"proj_equation_LowStar.BufferView.Down.View_n",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_711945fd2e915275d963923222fc0916",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"typing_FStar.Pervasives.__proj__Mkdtuple4__item___1",
"typing_FStar.Pervasives.__proj__Mkdtuple4__item___2",
"typing_FStar.Pervasives.__proj__Mkdtuple4__item___3",
"typing_LowStar.BufferView.Down.as_buffer",
"typing_LowStar.BufferView.Down.get_view"
],
0,
"5ae26b86d0783cfa785716faf022a6ea"
],
[
"LowStar.BufferView.Down.put_sel",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"bool_inversion", "data_elim_FStar.Pervasives.Mkdtuple4",
"data_elim_LowStar.BufferView.Down.View",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Seq.Properties.lseq", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int",
"equation_LowStar.BufferView.Down.as_buffer_t",
"equation_LowStar.BufferView.Down.buffer",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.logical",
"equation_Prims.nat", "equation_Prims.pos",
"fuel_guarded_inversion_FStar.Pervasives.dtuple4",
"fuel_guarded_inversion_LowStar.BufferView.Down.view",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Prims.logical", "int_inversion", "int_typing",
"interpretation_Tm_abs_2f52ee49857d060e683109f5fabb70fa",
"interpretation_Tm_abs_a8f4e254db91d3480d350b4b0b5a6525",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.UInt.pow2_values",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_FStar.Pervasives.Mkdtuple4__1",
"proj_equation_FStar.Pervasives.Mkdtuple4__2",
"proj_equation_FStar.Pervasives.Mkdtuple4__3",
"proj_equation_LowStar.BufferView.Down.View_n",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_711945fd2e915275d963923222fc0916",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_845322fb4513a913d6b544d4f805d91a",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.Pervasives.__proj__Mkdtuple4__item___1",
"typing_FStar.Pervasives.__proj__Mkdtuple4__item___2",
"typing_FStar.Pervasives.__proj__Mkdtuple4__item___3",
"typing_LowStar.BufferView.Down.as_buffer",
"typing_LowStar.BufferView.Down.as_seq",
"typing_LowStar.BufferView.Down.get_view"
],
0,
"cd0877d7c9fad808ed4b610980dd2c52"
],
[
"LowStar.BufferView.Down.upd_seq",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"89ab8a8298c486bd4a91c4ef61e67344"
],
[
"LowStar.BufferView.Down.upd_seq_spec",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_FStar.Seq.Properties.lseq", "equation_Prims.eqtype",
"equation_Prims.nat", "function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e"
],
0,
"c7729ee95c78b3b7ddc9d565aa73028a"
]
]
]
|
