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
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
|
[
".ڃ|6o4o_",
[
[
"LowStar.ConstBuffer.qbuf_cases",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_LowStar.ConstBuffer.IMMUTABLE",
"disc_equation_LowStar.ConstBuffer.MUTABLE",
"fuel_guarded_inversion_LowStar.ConstBuffer.qual"
],
0,
"16ae8f911604a83907097c7bfff61e81"
],
[
"LowStar.ConstBuffer.q_preorder",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_LowStar.ConstBuffer.IMMUTABLE",
"disc_equation_LowStar.ConstBuffer.MUTABLE",
"fuel_guarded_inversion_LowStar.ConstBuffer.qual"
],
0,
"1e3fbe9f6286d8db39805fb4b1e9b2fc"
],
[
"LowStar.ConstBuffer.qbuf_mbuf",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"LowStar.ConstBuffer_pretyping_4dc8c797bc0c0a619c5d226a788d601a",
"data_elim_Prims.Mkdtuple2",
"data_typing_intro_LowStar.ConstBuffer.IMMUTABLE@tok",
"equation_FStar.Pervasives.dfst", "equation_LowStar.Buffer.buffer",
"equation_LowStar.ConstBuffer.q_preorder",
"equation_LowStar.ConstBuffer.qbuf",
"equation_LowStar.ConstBuffer.qbuf_cases",
"equation_LowStar.ConstBuffer.qbuf_pre",
"equation_LowStar.ConstBuffer.qbuf_qual",
"equation_LowStar.ImmutableBuffer.ibuffer",
"fuel_guarded_inversion_LowStar.ConstBuffer.qual",
"fuel_guarded_inversion_Prims.dtuple2",
"interpretation_Tm_abs_68316c920d170978472d5b9e8ae4e447",
"kinding_LowStar.ConstBuffer.qual@tok",
"proj_equation_Prims.Mkdtuple2__2", "typing_FStar.Pervasives.dsnd",
"typing_LowStar.ConstBuffer.qbuf_qual"
],
0,
"75804105aca787b37efbdde6c62b1895"
],
[
"LowStar.ConstBuffer.of_buffer",
1,
2,
1,
[
"@query", "constructor_distinct_LowStar.ConstBuffer.MUTABLE",
"equality_tok_LowStar.ConstBuffer.MUTABLE@tok",
"equation_LowStar.ConstBuffer.q_preorder",
"equation_LowStar.ConstBuffer.qbuf_pre"
],
0,
"293faf620ddd54b2ec323e24c314304c"
],
[
"LowStar.ConstBuffer.of_ibuffer",
1,
2,
1,
[
"@query", "constructor_distinct_LowStar.ConstBuffer.IMMUTABLE",
"equality_tok_LowStar.ConstBuffer.IMMUTABLE@tok",
"equation_LowStar.ConstBuffer.q_preorder",
"equation_LowStar.ConstBuffer.qbuf_pre"
],
0,
"4d0d919572603339d9652eb745380d2b"
],
[
"LowStar.ConstBuffer.of_qbuf",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"LowStar.ConstBuffer_pretyping_4dc8c797bc0c0a619c5d226a788d601a",
"data_typing_intro_LowStar.ConstBuffer.IMMUTABLE@tok",
"equation_LowStar.ConstBuffer.qbuf",
"equation_LowStar.ConstBuffer.qbuf_pre",
"fuel_guarded_inversion_Prims.dtuple2",
"typing_LowStar.ConstBuffer.as_qbuf"
],
0,
"075e85c3e92d3e0fe453db809699fc93"
],
[
"LowStar.ConstBuffer.index",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "b2t_def",
"equation_FStar.UInt.fits", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_LowStar.ConstBuffer.as_mbuf",
"equation_LowStar.ConstBuffer.as_seq",
"equation_LowStar.ConstBuffer.length",
"equation_LowStar.ConstBuffer.qbuf_pre",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_3a60089398cfb9444106602ea3510e1b",
"typing_LowStar.ConstBuffer.as_mbuf",
"typing_LowStar.ConstBuffer.as_qbuf",
"typing_LowStar.ConstBuffer.qbuf_pre"
],
0,
"3ef15a58686cb2b7511f3773f4fed465"
],
[
"LowStar.ConstBuffer.gsub",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_LowStar.ConstBuffer.as_mbuf",
"equation_LowStar.ConstBuffer.length",
"refinement_interpretation_Tm_refine_8c25eb5d104cf052a48c588da1c89322"
],
0,
"cedd10caa71fca2a5ab9934ead6b4bf4"
],
[
"LowStar.ConstBuffer.to_buffer",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_LowStar.ConstBuffer.MUTABLE",
"equality_tok_LowStar.ConstBuffer.MUTABLE@tok",
"equation_LowStar.ConstBuffer.q_preorder",
"equation_LowStar.ConstBuffer.qbuf_pre",
"refinement_interpretation_Tm_refine_21418a2a27aecfef27831185fbcf6700"
],
0,
"8be08014eccb1ea482e3858280df9031"
],
[
"LowStar.ConstBuffer.to_ibuffer",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_LowStar.ConstBuffer.IMMUTABLE",
"equality_tok_LowStar.ConstBuffer.IMMUTABLE@tok",
"equation_LowStar.ConstBuffer.q_preorder",
"equation_LowStar.ConstBuffer.qbuf_pre",
"refinement_interpretation_Tm_refine_6a2d5aa361ca14de4e02d11c40d62bd3"
],
0,
"a1bd30e187762037153ebb4c171d8a7e"
],
[
"LowStar.ConstBuffer.test",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
"FStar.UInt32_pretyping_041e3a67a2d2b51fd702f1f88cfc3b44",
"LowStar.ConstBuffer_pretyping_4dc8c797bc0c0a619c5d226a788d601a",
"b2t_def", "bool_inversion", "bool_typing",
"constructor_distinct_LowStar.ConstBuffer.IMMUTABLE",
"constructor_distinct_LowStar.ConstBuffer.MUTABLE",
"data_elim_Prims.Mkdtuple2",
"data_typing_intro_LowStar.ConstBuffer.IMMUTABLE@tok",
"equality_tok_LowStar.ConstBuffer.IMMUTABLE@tok",
"equality_tok_LowStar.ConstBuffer.MUTABLE@tok",
"equation_FStar.Monotonic.HyperStack.live_region",
"equation_FStar.Pervasives.dfst", "equation_FStar.Pervasives.dsnd",
"equation_FStar.Preorder.preorder",
"equation_FStar.Preorder.preorder_rel",
"equation_FStar.Preorder.reflexive",
"equation_FStar.Seq.Properties.replace_subseq",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.ConstBuffer.as_mbuf",
"equation_LowStar.ConstBuffer.as_seq",
"equation_LowStar.ConstBuffer.const_sub_buffer",
"equation_LowStar.ConstBuffer.gsub",
"equation_LowStar.ConstBuffer.length",
"equation_LowStar.ConstBuffer.live",
"equation_LowStar.ConstBuffer.q_preorder",
"equation_LowStar.ConstBuffer.qbuf",
"equation_LowStar.ConstBuffer.qbuf_cases",
"equation_LowStar.ConstBuffer.qbuf_mbuf",
"equation_LowStar.ConstBuffer.qbuf_pre",
"equation_LowStar.ConstBuffer.qbuf_qual",
"equation_LowStar.ImmutableBuffer.ibuffer",
"equation_LowStar.ImmutableBuffer.immutable_preorder",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_LowStar.Monotonic.Buffer.get",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"fuel_guarded_inversion_Prims.dtuple2",
"function_token_typing_FStar.UInt32.t",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"int_inversion", "int_typing",
"interpretation_Tm_abs_289262f073cd8588d3c054b90f90e81a",
"interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
"interpretation_Tm_abs_68316c920d170978472d5b9e8ae4e447",
"kinding_LowStar.ConstBuffer.qual@tok",
"lemma_FStar.Ghost.reveal_hide",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.Seq.Base.lemma_index_app1",
"lemma_FStar.Seq.Base.lemma_index_app2",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_index_upd1",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv",
"lemma_FStar.UInt32.vu_inv",
"lemma_LowStar.Monotonic.Buffer.as_seq_gsub",
"lemma_LowStar.Monotonic.Buffer.len_gsub",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.live_gsub",
"lemma_LowStar.Monotonic.Buffer.live_region_frameOf",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction", "proj_equation_Prims.Mkdtuple2__1",
"proj_equation_Prims.Mkdtuple2__2",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_3084ff1dc7a1cf712f44d9369b7a7be3",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_4fa8e2dd96f8bb1e23e6574326e9e019",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_77a2e5e1e83ec81cdf1a6f0de42e0dcc",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
"refinement_interpretation_Tm_refine_bd10f09297e0e7dc08314f7d9211801c",
"refinement_interpretation_Tm_refine_c6c18a7ceb46d419c35ff8551117551e",
"refinement_interpretation_Tm_refine_caf420e019c39e197ae17a59091cbbc8",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"true_interp", "typing_FStar.Monotonic.HyperStack.live_region",
"typing_FStar.Pervasives.dsnd", "typing_FStar.Seq.Base.append",
"typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice",
"typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.ConstBuffer.as_qbuf",
"typing_LowStar.ConstBuffer.of_qbuf",
"typing_LowStar.ConstBuffer.qbuf_pre",
"typing_LowStar.ImmutableBuffer.immutable_preorder",
"typing_LowStar.Monotonic.Buffer.as_seq",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.length",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.mgsub",
"typing_tok_LowStar.ConstBuffer.IMMUTABLE@tok"
],
0,
"2dfb5c65a57d5eeb9422c716dbcaa81d"
]
]
]
|
