karamel/krmllib/hints/Spec.Loops.fst.hints at ca4d3daebaaad12b531fd45e343131bc68803b8f · FStarLang/karamel · GitHub

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
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
[
  "ì,ÇbQbá¯æ/ (·ó8Ö",
  [
    [
      "Spec.Loops.seq_map",
      1,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "b80a20fec484a21660f0804994c948e6"
    ],
    [
      "Spec.Loops.seq_map",
      2,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "bddb6bcfeb96ab2feb2d340c9bd5c883"
    ],
    [
      "Spec.Loops.seq_map",
      3,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_b1c102bc33763b5f709e32a86e66e509_5",
        "binder_x_fe28d8bcde588226b4e538b35321de05_2",
        "binder_x_fe28d8bcde588226b4e538b35321de05_3",
        "equality_tok_Prims.LexTop@tok",
        "equation_FStar.Seq.Properties.cons",
        "equation_FStar.Seq.Properties.head",
        "equation_FStar.Seq.Properties.tail", "equation_Prims.eqtype",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "int_typing", "lemma_FStar.Seq.Base.lemma_create_len",
        "lemma_FStar.Seq.Base.lemma_index_app1",
        "lemma_FStar.Seq.Base.lemma_index_app2",
        "lemma_FStar.Seq.Base.lemma_index_create",
        "lemma_FStar.Seq.Base.lemma_index_slice",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
        "refinement_interpretation_Tm_refine_c021012a5183a9d5ee7a9fdb75e57883",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length",
        "well-founded-ordering-on-nat"
      ],
      0,
      "108ae649ec59a814ecdd1ac78817ef68"
    ],
    [
      "Spec.Loops.seq_map2",
      1,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_16da5dd636ef303f4b4402f063fe1ef3",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "5d62dcf736709f63bfe8bf907754b260"
    ],
    [
      "Spec.Loops.seq_map2",
      2,
      0,
      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_aab03343de950d77c26ad9d98d2757b8"
      ],
      0,
      "271d89e8c17326f24dc4432db2e8b62f"
    ],
    [
      "Spec.Loops.seq_map2",
      3,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_47e4abf01510896a8bb55a562b825fad_7",
        "binder_x_bb8275b22c53d0aea56f4be775119f23_8",
        "binder_x_fe28d8bcde588226b4e538b35321de05_3",
        "binder_x_fe28d8bcde588226b4e538b35321de05_4",
        "binder_x_fe28d8bcde588226b4e538b35321de05_5",
        "equality_tok_Prims.LexTop@tok",
        "equation_FStar.Seq.Properties.cons",
        "equation_FStar.Seq.Properties.head",
        "equation_FStar.Seq.Properties.tail", "equation_Prims.eqtype",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "int_typing", "lemma_FStar.Seq.Base.lemma_create_len",
        "lemma_FStar.Seq.Base.lemma_index_app1",
        "lemma_FStar.Seq.Base.lemma_index_app2",
        "lemma_FStar.Seq.Base.lemma_index_create",
        "lemma_FStar.Seq.Base.lemma_index_slice",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_13a07fb1cde7ffdfc00b5d05f14b9231",
        "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d620c9dee68b076ac8d2f9cf47ea2d00",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length",
        "well-founded-ordering-on-nat"
      ],
      0,
      "1fe366d741905197d3d7fb577fb3455a"
    ],
    [
      "Spec.Loops.repeat",
      1,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2",
        "equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
        "int_inversion", "primitive_Prims.op_Equality",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "well-founded-ordering-on-nat"
      ],
      0,
      "7e3fb539602e165622aa59482683b9e9"
    ],
    [
      "Spec.Loops.repeat_induction",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001"
      ],
      0,
      "fa64684ff9db0d1c6da307f3396f10d9"
    ],
    [
      "Spec.Loops.repeat_induction",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001"
      ],
      0,
      "94594de31aa66ae13e1799f646cbef9f"
    ],
    [
      "Spec.Loops.repeat_induction",
      3,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Spec.Loops.repeat.fuel_instrumented",
        "@fuel_irrelevance_Spec.Loops.repeat.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Spec.Loops_interpretation_Tm_arrow_4d0f7779d04a7ae518b122b8529d2ee7",
        "Spec.Loops_interpretation_Tm_arrow_fcd589b21e6efcf1e5d17b07c282a015",
        "binder_x_983a3bbeaa1c076bcf8fe2016a3f7797_3",
        "binder_x_c9f70ab639c9ae669e58190eb4c1b5c9_2",
        "binder_x_e09860b75d8922ab497a3e5bc9347578_4",
        "binder_x_fe28d8bcde588226b4e538b35321de05_1", "equation_Prims.nat",
        "equation_with_fuel_Spec.Loops.repeat.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "primitive_Prims.op_Equality",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "typing_Spec.Loops.repeat", "well-founded-ordering-on-nat"
      ],
      0,
      "199e9a8f23c2041fb6455008dd92bb26"
    ],
    [
      "Spec.Loops.repeat_base",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Spec.Loops.repeat.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Spec.Loops_interpretation_Tm_arrow_4d0f7779d04a7ae518b122b8529d2ee7",
        "Spec.Loops_interpretation_Tm_arrow_fcd589b21e6efcf1e5d17b07c282a015",
        "binder_x_6d92a628296f4be95d4681b34e20780c_2",
        "binder_x_983a3bbeaa1c076bcf8fe2016a3f7797_3",
        "binder_x_e09860b75d8922ab497a3e5bc9347578_4",
        "binder_x_fe28d8bcde588226b4e538b35321de05_1",
        "equation_with_fuel_Spec.Loops.repeat.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "primitive_Prims.op_Equality",
        "refinement_interpretation_Tm_refine_f52d524f7d227b5c40129c018d34fe1d"
      ],
      0,
      "d69e2b229f95e226eb830bd89d3d6b6f"
    ],
    [
      "Spec.Loops.repeat_range",
      1,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_3ecda020b5cf79d02cc346b352c50370_3",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2",
        "equality_tok_Prims.LexTop@tok", "equation_Prims.eqtype",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "int_typing", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_dc48f78fca6f8433edb3d5a9ad647892",
        "well-founded-ordering-on-nat"
      ],
      0,
      "49c7d509c3e5dad41a39e573e6484c29"
    ],
    [
      "Spec.Loops.repeat_range_base",
      1,
      1,
      1,
      [ "@query" ],
      0,
      "2a02929630dd8646f1e560a6a658b52e"
    ],
    [
      "Spec.Loops.repeat_range_base",
      2,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Spec.Loops.repeat_range.fuel_instrumented",
        "@query", "equation_Prims.nat",
        "equation_with_fuel_Spec.Loops.repeat_range.fuel_instrumented",
        "int_inversion", "primitive_Prims.op_Equality",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913"
      ],
      0,
      "ad101cbb850ac7f739bcdaf695e3814a"
    ],
    [
      "Spec.Loops.repeat_range_induction",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "int_inversion", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_8233d76b57e95451540fc312b717fa79"
      ],
      0,
      "93cb62aaa6d0e08d2cd718eeb82a4b05"
    ],
    [
      "Spec.Loops.repeat_range_induction",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "int_inversion", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_8233d76b57e95451540fc312b717fa79"
      ],
      0,
      "9aaf70e501c8d07af378dbb4eea61e08"
    ],
    [
      "Spec.Loops.repeat_range_induction",
      3,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Spec.Loops.repeat_range.fuel_instrumented",
        "@fuel_irrelevance_Spec.Loops.repeat_range.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Spec.Loops_interpretation_Tm_arrow_6c4f136ce4c7836af556685bcd4e8402",
        "Spec.Loops_interpretation_Tm_arrow_991012978bfe18b65525b7a05d6a8a37",
        "binder_x_9c673d367a9aa1ce89b28b4f6e73873f_4",
        "binder_x_b3d004d0a96f90cbd8fd4251fc0ac398_3",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2",
        "binder_x_e09860b75d8922ab497a3e5bc9347578_5",
        "binder_x_fe28d8bcde588226b4e538b35321de05_1",
        "equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
        "equation_with_fuel_Spec.Loops.repeat_range.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
        "refinement_interpretation_Tm_refine_7c6f231fe68d618a805700b3d1db29e1",
        "refinement_interpretation_Tm_refine_852e4cf571f460149e621d5a931a1a57",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "typing_Spec.Loops.repeat_range", "well-founded-ordering-on-nat"
      ],
      0,
      "a0bbd4c20d0004d8e3d8a7ffd15cd594"
    ]
  ]
]