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
|
[
"=\u0013#Q\u0014a-u]",
[
[
"LowStar.BufferView.Up.view",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b"
],
0,
"7b53f2b6626b9e1957cddf49e9410c3a"
],
[
"LowStar.BufferView.Up.__proj__View__item__get",
1,
2,
1,
[ "@query" ],
0,
"ec6b56b0cfd26d8c540f77362fb18eaa"
],
[
"LowStar.BufferView.Up.__proj__View__item__get",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_LowStar.BufferView.Up.view",
"proj_equation_LowStar.BufferView.Up.View_n",
"projection_inverse_LowStar.BufferView.Up.View_n"
],
0,
"f7783ac6848544f97203953ded29e91e"
],
[
"LowStar.BufferView.Up.__proj__View__item__put",
1,
2,
1,
[ "@query" ],
0,
"091e9a1145ca7ccf0844ac06ef9fd982"
],
[
"LowStar.BufferView.Up.__proj__View__item__put",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"data_elim_LowStar.BufferView.Up.View",
"fuel_guarded_inversion_LowStar.BufferView.Up.view",
"proj_equation_LowStar.BufferView.Up.View_get",
"proj_equation_LowStar.BufferView.Up.View_n",
"projection_inverse_LowStar.BufferView.Up.View_n",
"projection_inverse_LowStar.BufferView.Up.View_put",
"refinement_interpretation_Tm_refine_28e5c211c74c3e8b3637e7a738fe6ec6",
"token_correspondence_LowStar.BufferView.Up.inverses"
],
0,
"7bc4e6383dd49a9c26660f51700263a8"
],
[
"LowStar.BufferView.Up.mk_buffer",
1,
2,
1,
[ "@query" ],
0,
"fff1ee1da53ced3beeb81ccb7492449d"
],
[
"LowStar.BufferView.Up.as_buffer_mk_buffer",
1,
2,
1,
[ "@query" ],
0,
"56415f5dd638a72f7dbda35fe736ee5b"
],
[
"LowStar.BufferView.Up.length_eq",
1,
2,
1,
[ "@query" ],
0,
"4bd9e5493b31504f15e5ec3324530d53"
],
[
"LowStar.BufferView.Up.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_31ff657caa99ed4c833e78322430b57b",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"685cf364df5037916566f50d7c1638ae"
],
[
"LowStar.BufferView.Up.lemma_upd_with_sel",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_31ff657caa99ed4c833e78322430b57b"
],
0,
"416d9049c98bc68024d3e6210260b66f"
],
[
"LowStar.BufferView.Up.as_seq_sel",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_FStar.Seq.Properties.lseq",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"typing_LowStar.BufferView.Up.as_seq"
],
0,
"9779e069b15bf8f99d8f8a89083965a8"
],
[
"LowStar.BufferView.Up.get_sel",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"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_Prims.nat",
"equation_Prims.pos",
"fuel_guarded_inversion_LowStar.BufferView.Up.view",
"function_token_typing_FStar.Monotonic.Heap.heap", "int_inversion",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_LowStar.BufferView.Up.View_n",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_281fe5c1b73a8d7995401c6b1ea9f2d9",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6d5ab57ac719f3d34aaa0ac8c62a3164",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"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_LowStar.BufferView.Down.as_seq",
"typing_LowStar.BufferView.Down.length",
"typing_LowStar.BufferView.Up.__proj__View__item__n",
"typing_LowStar.BufferView.Up.as_down_buffer",
"typing_LowStar.BufferView.Up.buffer_src",
"typing_LowStar.BufferView.Up.get_view"
],
0,
"ae48be0e3086516b5766807132a9aa80"
],
[
"LowStar.BufferView.Up.put_sel",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_FStar.Seq.Properties.lseq", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_LowStar.BufferView.Up.View_n",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6d5ab57ac719f3d34aaa0ac8c62a3164",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"typing_LowStar.BufferView.Down.as_seq",
"typing_LowStar.BufferView.Down.length",
"typing_LowStar.BufferView.Up.__proj__View__item__n",
"typing_LowStar.BufferView.Up.as_down_buffer",
"typing_LowStar.BufferView.Up.buffer_src",
"typing_LowStar.BufferView.Up.get_view"
],
0,
"87e0f1aeb57d812d1d3e789100950d12"
]
]
]
|
