1577def linuxValidateExactIOReceipt =
1578 (lambda unrestricted plan : (family LinuxExactIOPlan) .
1579 (lambda unrestricted receipt : (family LinuxExactIOReceipt) .
1580 (eliminate
1581 LinuxExactIOPlan
1582 (lambda unrestricted current : (family LinuxExactIOPlan) . (family LinuxExactIOValidation))
1583 plan
1584 (branch
1585 LinuxExactIOPlanValue
1586 expectedIdentity
1587 expectedKind
1588 descriptor
1589 expected
1590 maximumChunk
1591 .
1592 (eliminate
1593 LinuxExactIOReceipt
1594 (lambda unrestricted current : (family LinuxExactIOReceipt) .
1595 (family LinuxExactIOValidation))
1596 receipt
1597 (branch
1598 LinuxExactIOReceiptValue
1599 actualIdentity
1600 actualKind
1601 actual
1602 telemetry
1603 .
1604 (nat-eliminate
1605 (lambda unrestricted current : Nat . (family LinuxExactIOValidation))
1606 (linuxRejectExactIO
1607 (constructor LinuxSyscallContractErrorCode LinuxReceiptIdentityMismatch)
1608 expected
1609 actual
1610 telemetry)
1611 (lambda unrestricted identityPredecessor : Nat .
1612 (lambda unrestricted ignoredIdentity : (family LinuxExactIOValidation) .
1613 (nat-eliminate
1614 (lambda unrestricted current : Nat . (family LinuxExactIOValidation))
1615 (linuxRejectExactIO
1616 (constructor LinuxSyscallContractErrorCode LinuxReceiptExactIOPlanMismatch)
1617 expected
1618 actual
1619 telemetry)
1620 (lambda unrestricted kindPredecessor : Nat .
1621 (lambda unrestricted ignoredKind : (family LinuxExactIOValidation) .
1622 (nat-eliminate
1623 (lambda unrestricted current : Nat . (family LinuxExactIOValidation))
1624 (linuxRejectExactIO
1625 (linuxExactIOShortError expectedKind telemetry)
1626 expected
1627 actual
1628 telemetry)
1629 (lambda unrestricted extentPredecessor : Nat .
1630 (lambda unrestricted ignoredExtent : (family LinuxExactIOValidation) .
1631 (nat-eliminate
1632 (lambda unrestricted current : Nat .
1633 (family LinuxExactIOValidation))
1634 (nat-eliminate
1635 (lambda unrestricted current : Nat .
1636 (family LinuxExactIOValidation))
1637 (constructor
1638 LinuxExactIOValidation
1639 LinuxExactIOAccepted
1640 receipt)
1641 (lambda unrestricted cleanupPredecessor : Nat .
1642 (lambda unrestricted ignoredCleanup : (family LinuxExactIOValidation) .
1643 (linuxRejectExactIO
1644 (constructor
1645 LinuxSyscallContractErrorCode
1646 LinuxReceiptCleanupFailed)
1647 expected
1648 actual
1649 telemetry)))
1650 (linuxCleanupFailureCount telemetry))
1651 (lambda unrestricted fallbackPredecessor : Nat .
1652 (lambda unrestricted ignoredFallback : (family LinuxExactIOValidation) .
1653 (linuxRejectExactIO
1654 (constructor
1655 LinuxSyscallContractErrorCode
1656 LinuxReceiptHostFallbackRejected)
1657 expected
1658 actual
1659 telemetry)))
1660 (linuxCleanupHostFallbackCount telemetry))))
1661 (modelWord64Equal expected actual))))
1662 (naturalEqual
1663 (linuxExactIOKindRank expectedKind)
1664 (linuxExactIOKindRank actualKind)))))
1665 (linuxIdentityEqual expectedIdentity actualIdentity))))))))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.