1module Compiler.MachineX86NativeOffset
2
3family X86NativeUnsigned32 : Type 0
4constructor X86NativeUnsigned32Value
5field unrestricted x86NativeUnsigned32Byte0 : Byte
6field unrestricted x86NativeUnsigned32Byte1 : Byte
7field unrestricted x86NativeUnsigned32Byte2 : Byte
8field unrestricted x86NativeUnsigned32Byte3 : Byte
9
10end-family
11
12family X86NativeUnsigned32Result : Type 0
13constructor X86NativeUnsigned32Success
14field unrestricted x86NativeUnsigned32ResultValue : (family X86NativeUnsigned32)
15constructor X86NativeUnsigned32Overflow
16
17end-family
18
19family X86NativeByteSubtractResult : Type 0
20constructor X86NativeByteSubtractValue
21field unrestricted x86NativeByteSubtractDifference : Byte
22field unrestricted x86NativeByteSubtractBorrow : Nat
23
24end-family
25
26family X86NativeUnsigned32SubtractResult : Type 0
27constructor X86NativeUnsigned32SubtractValue
28field unrestricted x86NativeUnsigned32Difference : (family X86NativeUnsigned32)
29field unrestricted x86NativeUnsigned32Borrow : Nat
30
31end-family
32
33family X86NativeRelativeDisplacementResult : Type 0
34constructor X86NativeRelativeDisplacementSuccess
35field unrestricted x86NativeRelativeDisplacementValue : (family X86NativeUnsigned32)
36constructor X86NativeRelativeDisplacementOutOfRange
37
38end-family
39
40-- Field projection for `x86NativeUnsigned32Byte1`, generated from the declaration: the family
41-- has one constructor, so this is the unique total projection.
42def x86NativeUnsigned32Byte1 =
43 (lambda unrestricted value : (family X86NativeUnsigned32) .
44 (eliminate
45 X86NativeUnsigned32
46 (lambda unrestricted current : (family X86NativeUnsigned32) . Byte)
47 value
48 (branch
49 X86NativeUnsigned32Value
50 x86NativeUnsigned32Byte0
51 x86NativeUnsigned32Byte1
52 x86NativeUnsigned32Byte2
53 x86NativeUnsigned32Byte3
54 .
55 x86NativeUnsigned32Byte1)))
56
57-- Field projection for `x86NativeUnsigned32Byte2`, generated from the declaration: the family
58-- has one constructor, so this is the unique total projection.
59def x86NativeUnsigned32Byte2 =
60 (lambda unrestricted value : (family X86NativeUnsigned32) .
61 (eliminate
62 X86NativeUnsigned32
63 (lambda unrestricted current : (family X86NativeUnsigned32) . Byte)
64 value
65 (branch
66 X86NativeUnsigned32Value
67 x86NativeUnsigned32Byte0
68 x86NativeUnsigned32Byte1
69 x86NativeUnsigned32Byte2
70 x86NativeUnsigned32Byte3
71 .
72 x86NativeUnsigned32Byte2)))
73
74-- Field projection for `x86NativeUnsigned32Byte3`, generated from the declaration: the family
75-- has one constructor, so this is the unique total projection.
76def x86NativeUnsigned32Byte3 =
77 (lambda unrestricted value : (family X86NativeUnsigned32) .
78 (eliminate
79 X86NativeUnsigned32
80 (lambda unrestricted current : (family X86NativeUnsigned32) . Byte)
81 value
82 (branch
83 X86NativeUnsigned32Value
84 x86NativeUnsigned32Byte0
85 x86NativeUnsigned32Byte1
86 x86NativeUnsigned32Byte2
87 x86NativeUnsigned32Byte3
88 .
89 x86NativeUnsigned32Byte3)))
90
91-- Field projection for `x86NativeUnsigned32Byte0`, generated from the declaration: the family
92-- has one constructor, so this is the unique total projection.
93def x86NativeUnsigned32Byte0 =
94 (lambda unrestricted value : (family X86NativeUnsigned32) .
95 (eliminate
96 X86NativeUnsigned32
97 (lambda unrestricted current : (family X86NativeUnsigned32) . Byte)
98 value
99 (branch
100 X86NativeUnsigned32Value
101 x86NativeUnsigned32Byte0
102 x86NativeUnsigned32Byte1
103 x86NativeUnsigned32Byte2
104 x86NativeUnsigned32Byte3
105 .
106 x86NativeUnsigned32Byte0)))
107
108def x86NativeUnsigned32Zero : (family X86NativeUnsigned32) =
109 (constructor X86NativeUnsigned32 X86NativeUnsigned32Value (byte 0) (byte 0) (byte 0) (byte 0))
110
111def x86NativeNaturalPredecessor =
112 (lambda unrestricted value : Nat .
113 (nat-eliminate
114 (lambda unrestricted current : Nat . Nat)
115 zero
116 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . predecessor))
117 value))
118
119def x86NativeNaturalSubtract =
120 (lambda unrestricted left : Nat .
121 (lambda unrestricted right : Nat .
122 (nat-eliminate
123 (lambda unrestricted current : Nat . Nat)
124 left
125 (lambda unrestricted predecessor : Nat .
126 (lambda unrestricted induction : Nat . (x86NativeNaturalPredecessor induction)))
127 right)))
128
129def x86NativeNaturalAdd =
130 (lambda unrestricted left : Nat .
131 (lambda unrestricted right : Nat .
132 (nat-eliminate
133 (lambda unrestricted current : Nat . Nat)
134 left
135 (lambda unrestricted predecessor : Nat .
136 (lambda unrestricted induction : Nat . (succ induction)))
137 right)))
138
139def x86NativeNaturalPositive =
140 (lambda unrestricted value : Nat .
141 (nat-eliminate
142 (lambda unrestricted current : Nat . Nat)
143 zero
144 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . (succ zero)))
145 value))
146
147def x86NativeNaturalAnd =
148 (lambda unrestricted left : Nat .
149 (lambda unrestricted right : Nat .
150 (nat-eliminate
151 (lambda unrestricted current : Nat . Nat)
152 zero
153 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . right))
154 left)))
155
156def x86NativeSubtractByte =
157 (lambda unrestricted left : Byte .
158 (lambda unrestricted right : Byte .
159 (lambda unrestricted borrow : Nat .
160 (let unrestricted leftNatural =
161 (byte-to-nat left)
162 in
163 (let unrestricted rightNatural =
164 (x86NativeNaturalAdd (byte-to-nat right) borrow)
165 in
166 (let unrestricted outgoingBorrow =
167 (x86NativeNaturalPositive (x86NativeNaturalSubtract rightNatural leftNatural))
168 in
169 (nat-eliminate
170 (lambda unrestricted hasBorrow : Nat . (family X86NativeByteSubtractResult))
171 (constructor
172 X86NativeByteSubtractResult
173 X86NativeByteSubtractValue
174 (nat-to-byte (x86NativeNaturalSubtract leftNatural rightNatural))
175 zero)
176 (lambda unrestricted predecessor : Nat .
177 (lambda unrestricted induction : (family X86NativeByteSubtractResult) .
178 (constructor
179 X86NativeByteSubtractResult
180 X86NativeByteSubtractValue
181 (nat-to-byte
182 (x86NativeNaturalSubtract
183 (x86NativeNaturalAdd (succ (byte-to-nat (byte 255))) leftNatural)
184 rightNatural))
185 (succ zero))))
186 outgoingBorrow)))))))
187
188def x86NativeSubtractUnsigned32 :
189 (pi unrestricted left : (family X86NativeUnsigned32) .
190 (pi unrestricted right : (family X86NativeUnsigned32) .
191 (family X86NativeUnsigned32SubtractResult))) =
192 (lambda unrestricted left : (family X86NativeUnsigned32) .
193 (lambda unrestricted right : (family X86NativeUnsigned32) .
194 (eliminate
195 X86NativeUnsigned32
196 (lambda unrestricted leftValue : (family X86NativeUnsigned32) .
197 (family X86NativeUnsigned32SubtractResult))
198 left
199 (branch
200 X86NativeUnsigned32Value
201 left0
202 left1
203 left2
204 left3
205 .
206 (eliminate
207 X86NativeUnsigned32
208 (lambda unrestricted rightValue : (family X86NativeUnsigned32) .
209 (family X86NativeUnsigned32SubtractResult))
210 right
211 (branch
212 X86NativeUnsigned32Value
213 right0
214 right1
215 right2
216 right3
217 .
218 (eliminate
219 X86NativeByteSubtractResult
220 (lambda unrestricted result0 : (family X86NativeByteSubtractResult) .
221 (family X86NativeUnsigned32SubtractResult))
222 (x86NativeSubtractByte left0 right0 zero)
223 (branch
224 X86NativeByteSubtractValue
225 difference0
226 borrow1
227 .
228 (eliminate
229 X86NativeByteSubtractResult
230 (lambda unrestricted result1 : (family X86NativeByteSubtractResult) .
231 (family X86NativeUnsigned32SubtractResult))
232 (x86NativeSubtractByte left1 right1 borrow1)
233 (branch
234 X86NativeByteSubtractValue
235 difference1
236 borrow2
237 .
238 (eliminate
239 X86NativeByteSubtractResult
240 (lambda unrestricted result2 : (family X86NativeByteSubtractResult) .
241 (family X86NativeUnsigned32SubtractResult))
242 (x86NativeSubtractByte left2 right2 borrow2)
243 (branch
244 X86NativeByteSubtractValue
245 difference2
246 borrow3
247 .
248 (eliminate
249 X86NativeByteSubtractResult
250 (lambda unrestricted result3 : (family X86NativeByteSubtractResult) .
251 (family X86NativeUnsigned32SubtractResult))
252 (x86NativeSubtractByte left3 right3 borrow3)
253 (branch
254 X86NativeByteSubtractValue
255 difference3
256 finalBorrow
257 .
258 (constructor
259 X86NativeUnsigned32SubtractResult
260 X86NativeUnsigned32SubtractValue
261 (constructor
262 X86NativeUnsigned32
263 X86NativeUnsigned32Value
264 difference0
265 difference1
266 difference2
267 difference3)
268 finalBorrow)))))))))))))))
269
270def x86NativePositiveRel32 =
271 (lambda unrestricted value : (family X86NativeUnsigned32) .
272 (eliminate
273 X86NativeUnsigned32
274 (lambda unrestricted current : (family X86NativeUnsigned32) . Nat)
275 value
276 (branch X86NativeUnsigned32Value byte0 byte1 byte2 byte3 . (byte-less-than byte3 (byte 128)))))
277
278def x86NativeNegativeMagnitudeRel32 =
279 (lambda unrestricted value : (family X86NativeUnsigned32) .
280 (eliminate
281 X86NativeUnsigned32
282 (lambda unrestricted current : (family X86NativeUnsigned32) . Nat)
283 value
284 (branch
285 X86NativeUnsigned32Value
286 byte0
287 byte1
288 byte2
289 byte3
290 .
291 (nat-eliminate
292 (lambda unrestricted below : Nat . Nat)
293 (x86NativeNaturalAnd
294 (byte-equal byte3 (byte 128))
295 (bytes-equal
296 (bytes-cons byte0 (bytes-cons byte1 (bytes-cons byte2 b"")))
297 (bytes 0 0 0)))
298 (lambda unrestricted predecessor : Nat .
299 (lambda unrestricted induction : Nat . (succ zero)))
300 (byte-less-than byte3 (byte 128))))))
301
302def x86NativeIncrementByte =
303 (lambda unrestricted value : Byte . (nat-to-byte (succ (byte-to-nat value))))
304
305def x86NativeComplementByte =
306 (lambda unrestricted value : Byte .
307 (nat-to-byte (x86NativeNaturalSubtract (byte-to-nat (byte 255)) (byte-to-nat value))))
308
309def x86NativeUnsigned32Bytes : (pi unrestricted value : (family X86NativeUnsigned32) . Bytes) =
310 (lambda unrestricted value : (family X86NativeUnsigned32) .
311 (eliminate
312 X86NativeUnsigned32
313 (lambda unrestricted current : (family X86NativeUnsigned32) . Bytes)
314 value
315 (branch
316 X86NativeUnsigned32Value
317 byte0
318 byte1
319 byte2
320 byte3
321 .
322 (bytes-cons byte0 (bytes-cons byte1 (bytes-cons byte2 (bytes-cons byte3 b"")))))))
323
324def x86NativeIncrementUnsigned32Wrapping :
325 (pi unrestricted value : (family X86NativeUnsigned32) . (family X86NativeUnsigned32)) =
326 (lambda unrestricted value : (family X86NativeUnsigned32) .
327 (eliminate
328 X86NativeUnsigned32
329 (lambda unrestricted current : (family X86NativeUnsigned32) . (family X86NativeUnsigned32))
330 value
331 (branch
332 X86NativeUnsigned32Value
333 byte0
334 byte1
335 byte2
336 byte3
337 .
338 (nat-eliminate
339 (lambda unrestricted carry0 : Nat . (family X86NativeUnsigned32))
340 (constructor
341 X86NativeUnsigned32
342 X86NativeUnsigned32Value
343 (x86NativeIncrementByte byte0)
344 byte1
345 byte2
346 byte3)
347 (lambda unrestricted predecessor0 : Nat .
348 (lambda unrestricted induction0 : (family X86NativeUnsigned32) .
349 (nat-eliminate
350 (lambda unrestricted carry1 : Nat . (family X86NativeUnsigned32))
351 (constructor
352 X86NativeUnsigned32
353 X86NativeUnsigned32Value
354 (byte 0)
355 (x86NativeIncrementByte byte1)
356 byte2
357 byte3)
358 (lambda unrestricted predecessor1 : Nat .
359 (lambda unrestricted induction1 : (family X86NativeUnsigned32) .
360 (nat-eliminate
361 (lambda unrestricted carry2 : Nat . (family X86NativeUnsigned32))
362 (constructor
363 X86NativeUnsigned32
364 X86NativeUnsigned32Value
365 (byte 0)
366 (byte 0)
367 (x86NativeIncrementByte byte2)
368 byte3)
369 (lambda unrestricted predecessor2 : Nat .
370 (lambda unrestricted induction2 : (family X86NativeUnsigned32) .
371 (constructor
372 X86NativeUnsigned32
373 X86NativeUnsigned32Value
374 (byte 0)
375 (byte 0)
376 (byte 0)
377 (x86NativeIncrementByte byte3))))
378 (byte-equal byte2 (byte 255)))))
379 (byte-equal byte1 (byte 255)))))
380 (byte-equal byte0 (byte 255))))))
381
382def x86NativeIncrementUnsigned32 :
383 (pi unrestricted value : (family X86NativeUnsigned32) . (family X86NativeUnsigned32Result)) =
384 (lambda unrestricted value : (family X86NativeUnsigned32) .
385 (eliminate
386 X86NativeUnsigned32
387 (lambda unrestricted current : (family X86NativeUnsigned32) .
388 (family X86NativeUnsigned32Result))
389 value
390 (branch
391 X86NativeUnsigned32Value
392 byte0
393 byte1
394 byte2
395 byte3
396 .
397 (nat-eliminate
398 (lambda unrestricted carry0 : Nat . (family X86NativeUnsigned32Result))
399 (constructor
400 X86NativeUnsigned32Result
401 X86NativeUnsigned32Success
402 (constructor
403 X86NativeUnsigned32
404 X86NativeUnsigned32Value
405 (x86NativeIncrementByte byte0)
406 byte1
407 byte2
408 byte3))
409 (lambda unrestricted predecessor0 : Nat .
410 (lambda unrestricted induction0 : (family X86NativeUnsigned32Result) .
411 (nat-eliminate
412 (lambda unrestricted carry1 : Nat . (family X86NativeUnsigned32Result))
413 (constructor
414 X86NativeUnsigned32Result
415 X86NativeUnsigned32Success
416 (constructor
417 X86NativeUnsigned32
418 X86NativeUnsigned32Value
419 (byte 0)
420 (x86NativeIncrementByte byte1)
421 byte2
422 byte3))
423 (lambda unrestricted predecessor1 : Nat .
424 (lambda unrestricted induction1 : (family X86NativeUnsigned32Result) .
425 (nat-eliminate
426 (lambda unrestricted carry2 : Nat . (family X86NativeUnsigned32Result))
427 (constructor
428 X86NativeUnsigned32Result
429 X86NativeUnsigned32Success
430 (constructor
431 X86NativeUnsigned32
432 X86NativeUnsigned32Value
433 (byte 0)
434 (byte 0)
435 (x86NativeIncrementByte byte2)
436 byte3))
437 (lambda unrestricted predecessor2 : Nat .
438 (lambda unrestricted induction2 : (family X86NativeUnsigned32Result) .
439 (nat-eliminate
440 (lambda unrestricted carry3 : Nat . (family X86NativeUnsigned32Result))
441 (constructor
442 X86NativeUnsigned32Result
443 X86NativeUnsigned32Success
444 (constructor
445 X86NativeUnsigned32
446 X86NativeUnsigned32Value
447 (byte 0)
448 (byte 0)
449 (byte 0)
450 (x86NativeIncrementByte byte3)))
451 (lambda unrestricted predecessor3 : Nat .
452 (lambda unrestricted induction3 : (family X86NativeUnsigned32Result) .
453 (constructor X86NativeUnsigned32Result X86NativeUnsigned32Overflow)))
454 (byte-equal byte3 (byte 255)))))
455 (byte-equal byte2 (byte 255)))))
456 (byte-equal byte1 (byte 255)))))
457 (byte-equal byte0 (byte 255))))))
458
459def x86NativeComplementUnsigned32 :
460 (pi unrestricted value : (family X86NativeUnsigned32) . (family X86NativeUnsigned32)) =
461 (lambda unrestricted value : (family X86NativeUnsigned32) .
462 (eliminate
463 X86NativeUnsigned32
464 (lambda unrestricted current : (family X86NativeUnsigned32) . (family X86NativeUnsigned32))
465 value
466 (branch
467 X86NativeUnsigned32Value
468 byte0
469 byte1
470 byte2
471 byte3
472 .
473 (constructor
474 X86NativeUnsigned32
475 X86NativeUnsigned32Value
476 (x86NativeComplementByte byte0)
477 (x86NativeComplementByte byte1)
478 (x86NativeComplementByte byte2)
479 (x86NativeComplementByte byte3)))))
480
481def x86NativeNegateUnsigned32 :
482 (pi unrestricted value : (family X86NativeUnsigned32) . (family X86NativeUnsigned32)) =
483 (lambda unrestricted value : (family X86NativeUnsigned32) .
484 (x86NativeIncrementUnsigned32Wrapping (x86NativeComplementUnsigned32 value)))
485
486def x86NativeRelativeDisplacement :
487 (pi unrestricted target : (family X86NativeUnsigned32) .
488 (pi unrestricted sourceEnd : (family X86NativeUnsigned32) .
489 (family X86NativeRelativeDisplacementResult))) =
490 (lambda unrestricted target : (family X86NativeUnsigned32) .
491 (lambda unrestricted sourceEnd : (family X86NativeUnsigned32) .
492 (eliminate
493 X86NativeUnsigned32SubtractResult
494 (lambda unrestricted result : (family X86NativeUnsigned32SubtractResult) .
495 (family X86NativeRelativeDisplacementResult))
496 (x86NativeSubtractUnsigned32 target sourceEnd)
497 (branch
498 X86NativeUnsigned32SubtractValue
499 forwardDifference
500 borrow
501 .
502 (nat-eliminate
503 (lambda unrestricted negative : Nat . (family X86NativeRelativeDisplacementResult))
504 (nat-eliminate
505 (lambda unrestricted inRange : Nat . (family X86NativeRelativeDisplacementResult))
506 (constructor
507 X86NativeRelativeDisplacementResult
508 X86NativeRelativeDisplacementOutOfRange)
509 (lambda unrestricted predecessor : Nat .
510 (lambda unrestricted induction : (family X86NativeRelativeDisplacementResult) .
511 (constructor
512 X86NativeRelativeDisplacementResult
513 X86NativeRelativeDisplacementSuccess
514 forwardDifference)))
515 (x86NativePositiveRel32 forwardDifference))
516 (lambda unrestricted predecessor : Nat .
517 (lambda unrestricted induction : (family X86NativeRelativeDisplacementResult) .
518 (eliminate
519 X86NativeUnsigned32SubtractResult
520 (lambda unrestricted reverseResult : (family X86NativeUnsigned32SubtractResult) .
521 (family X86NativeRelativeDisplacementResult))
522 (x86NativeSubtractUnsigned32 sourceEnd target)
523 (branch
524 X86NativeUnsigned32SubtractValue
525 magnitude
526 reverseBorrow
527 .
528 (nat-eliminate
529 (lambda unrestricted inRange : Nat .
530 (family X86NativeRelativeDisplacementResult))
531 (constructor
532 X86NativeRelativeDisplacementResult
533 X86NativeRelativeDisplacementOutOfRange)
534 (lambda unrestricted rangePredecessor : Nat .
535 (lambda unrestricted rangeInduction : (family X86NativeRelativeDisplacementResult) .
536 (constructor
537 X86NativeRelativeDisplacementResult
538 X86NativeRelativeDisplacementSuccess
539 (x86NativeNegateUnsigned32 magnitude))))
540 (x86NativeNegativeMagnitudeRel32 magnitude))))))
541 borrow)))))
542
543def x86NativeCountBytes32 : (pi unrestricted input : Bytes . (family X86NativeUnsigned32Result)) =
544 (lambda unrestricted input : Bytes .
545 (bytes-eliminate
546 (lambda unrestricted value : Bytes . (family X86NativeUnsigned32Result))
547 (constructor X86NativeUnsigned32Result X86NativeUnsigned32Success x86NativeUnsigned32Zero)
548 (lambda unrestricted head : Byte .
549 (lambda unrestricted tail : Bytes .
550 (lambda unrestricted induction : (family X86NativeUnsigned32Result) .
551 (eliminate
552 X86NativeUnsigned32Result
553 (lambda unrestricted result : (family X86NativeUnsigned32Result) .
554 (family X86NativeUnsigned32Result))
555 induction
556 (branch X86NativeUnsigned32Success value . (x86NativeIncrementUnsigned32 value))
557 (branch
558 X86NativeUnsigned32Overflow
559 .
560 (constructor X86NativeUnsigned32Result X86NativeUnsigned32Overflow))))))
561 input))
562
563def x86NativeAdvanceUnsigned32ByBytes :
564 (pi unrestricted initial : (family X86NativeUnsigned32) .
565 (pi unrestricted input : Bytes . (family X86NativeUnsigned32Result))) =
566 (lambda unrestricted initial : (family X86NativeUnsigned32) .
567 (lambda unrestricted input : Bytes .
568 (bytes-eliminate
569 (lambda unrestricted value : Bytes . (family X86NativeUnsigned32Result))
570 (constructor X86NativeUnsigned32Result X86NativeUnsigned32Success initial)
571 (lambda unrestricted head : Byte .
572 (lambda unrestricted tail : Bytes .
573 (lambda unrestricted induction : (family X86NativeUnsigned32Result) .
574 (eliminate
575 X86NativeUnsigned32Result
576 (lambda unrestricted result : (family X86NativeUnsigned32Result) .
577 (family X86NativeUnsigned32Result))
578 induction
579 (branch X86NativeUnsigned32Success value . (x86NativeIncrementUnsigned32 value))
580 (branch
581 X86NativeUnsigned32Overflow
582 .
583 (constructor X86NativeUnsigned32Result X86NativeUnsigned32Overflow))))))
584 input)))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.