501def vaCommitReservation =
502 (lambda unrestricted pending : (family VAPendingReservation) .
503 (lambda unrestricted receipt : (family VANativeReservationReceipt) .
504 (eliminate
505 VAPendingReservation
506 (lambda unrestricted current : (family VAPendingReservation) . (family VACommitResult))
507 pending
508 (branch
509 VAPendingReservationValue
510 eventIndex
511 original
512 allocation
513 .
514 (eliminate
515 VAAllocation
516 (lambda unrestricted current : (family VAAllocation) . (family VACommitResult))
517 allocation
518 (branch
519 VAAllocationValue
520 start
521 extent
522 alignment
523 following
524 .
525 (eliminate
526 VANativeReservationReceipt
527 (lambda unrestricted current : (family VANativeReservationReceipt) .
528 (family VACommitResult))
529 receipt
530 (branch
531 VANativeReservationReceiptValue
532 receiptEvent
533 receiptStart
534 receiptExtent
535 succeeded
536 fallbacks
537 .
538 (nat-eliminate
539 (lambda unrestricted noFallbacks : Nat . (family VACommitResult))
540 (vaCommitFailure pending (constructor VAErrorCode VAHostFallbackObserved))
541 (lambda unrestricted fallbackPredecessor : Nat .
542 (lambda unrestricted fallbackInduction : (family VACommitResult) .
543 (nat-eliminate
544 (lambda unrestricted nativeSucceeded : Nat . (family VACommitResult))
545 (vaCommitFailure
546 pending
547 (constructor VAErrorCode VANativeReservationRejected))
548 (lambda unrestricted successPredecessor : Nat .
549 (lambda unrestricted successInduction : (family VACommitResult) .
550 (nat-eliminate
551 (lambda unrestricted startMatches : Nat . (family VACommitResult))
552 (vaCommitFailure
553 pending
554 (constructor VAErrorCode VAReceiptStartMismatch))
555 (lambda unrestricted startPredecessor : Nat .
556 (lambda unrestricted startInduction : (family VACommitResult) .
557 (nat-eliminate
558 (lambda unrestricted extentMatches : Nat .
559 (family VACommitResult))
560 (vaCommitFailure
561 pending
562 (constructor VAErrorCode VAReceiptExtentMismatch))
563 (lambda unrestricted extentPredecessor : Nat .
564 (lambda unrestricted extentInduction : (family VACommitResult) .
565 (eliminate
566 VAAllocator
567 (lambda unrestricted current : (family VAAllocator) .
568 (family VACommitResult))
569 original
570 (branch
571 VAAllocatorValue
572 inputNext
573 .
574 (constructor
575 VACommitResult
576 VACommitted
577 following
578 (vaTelemetrySucceededFor
579 eventIndex
580 inputNext
581 extent
582 allocation))))))
583 (modelWord64Equal
584 (stdByteCountValue receiptExtent)
585 (stdByteCountValue extent)))))
586 (modelWord64Equal
587 (stdDeviceAddressValue receiptStart)
588 (stdDeviceAddressValue start)))))
589 succeeded)))
590 (naturalIsZero fallbacks))))))))))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.