1654def checkpointDeriveSchema =
1655 (lambda unrestricted program : (family CheckpointProgram) .
1656 (eliminate
1657 CheckpointProgram
1658 (lambda unrestricted current : (family CheckpointProgram) . (family CheckpointSchemaResult))
1659 program
1660 (branch
1661 CheckpointProgramValue
1662 storages
1663 learner
1664 .
1665 (eliminate
1666 CheckpointLearnerComponent
1667 (lambda unrestricted current : (family CheckpointLearnerComponent) .
1668 (family CheckpointSchemaResult))
1669 learner
1670 (branch
1671 CheckpointLearnerComponentValue
1672 policy
1673 .
1674 (app
1675 (lambda unrestricted storageCount : Nat .
1676 (eliminate
1677 CheckpointExtentResult
1678 (lambda unrestricted current : (family CheckpointExtentResult) .
1679 (family CheckpointSchemaResult))
1680 (checkpointStorageFieldsEnd storages)
1681 (branch
1682 CheckpointExtentAccepted
1683 storageEnd
1684 .
1685 (eliminate
1686 CheckpointParameterCountResult
1687 (lambda unrestricted current : (family CheckpointParameterCountResult) .
1688 (family CheckpointSchemaResult))
1689 (checkpointParameterCount storages)
1690 (branch
1691 CheckpointParameterCountAccepted
1692 parameterCount
1693 .
1694 (eliminate
1695 CheckpointLearnerFieldsResult
1696 (lambda unrestricted current : (family CheckpointLearnerFieldsResult) .
1697 (family CheckpointSchemaResult))
1698 (checkpointDeriveLearnerFields policy storages storageEnd)
1699 (branch
1700 CheckpointLearnerFieldsAccepted
1701 learnerFields
1702 learnerEnd
1703 learnerCount
1704 .
1705 (app
1706 (lambda unrestricted allFields : (family CheckpointFields) .
1707 (eliminate
1708 CheckpointPlacementResult
1709 (lambda unrestricted current : (family CheckpointPlacementResult) .
1710 (family CheckpointSchemaResult))
1711 (checkpointPlaceStreamFields allFields modelWord64Zero)
1712 (branch
1713 CheckpointPlacementAccepted
1714 placedFields
1715 payloadBytes
1716 placedCount
1717 .
1718 (eliminate
1719 CheckpointBytesResult
1720 (lambda unrestricted current : (family CheckpointBytesResult) .
1721 (family CheckpointSchemaResult))
1722 (checkpointCanonicalSchema
1723 policy
1724 parameterCount
1725 payloadBytes
1726 placedFields)
1727 (branch
1728 CheckpointBytesSucceeded
1729 material
1730 .
1731 (eliminate
1732 SHA256HexResult
1733 (lambda unrestricted current : (family SHA256HexResult) .
1734 (family CheckpointSchemaResult))
1735 (sha256Hex material)
1736 (branch
1737 SHA256HexSucceeded
1738 digest
1739 digestTelemetry
1740 .
1741 (nat-eliminate
1742 (lambda unrestricted validDigest : Nat .
1743 (family CheckpointSchemaResult))
1744 (constructor
1745 CheckpointSchemaResult
1746 CheckpointSchemaRejected
1747 (checkpointSimpleFailure
1748 (constructor
1749 CheckpointErrorCode
1750 CheckpointSchemaDigestLengthInvalid)
1751 zero)
1752 (checkpointSchemaTelemetryAt
1753 storageCount
1754 storageCount
1755 learnerCount
1756 placedCount
1757 (bytes-length material)
1758 digestTelemetry))
1759 (lambda unrestricted predecessor : Nat .
1760 (lambda unrestricted induction : (family CheckpointSchemaResult) .
1761 (constructor
1762 CheckpointSchemaResult
1763 CheckpointSchemaDerived
1764 (constructor
1765 CheckpointSchema
1766 CheckpointSchemaValue
1767 policy
1768 digest
1769 placedFields
1770 parameterCount
1771 payloadBytes)
1772 (checkpointSchemaTelemetryAt
1773 storageCount
1774 storageCount
1775 learnerCount
1776 placedCount
1777 (bytes-length material)
1778 digestTelemetry))))
1779 (naturalEqual (bytes-length digest) (byte-to-nat (byte 64)))))
1780 (branch
1781 SHA256HexFailed
1782 error
1783 ordinal
1784 digestTelemetry
1785 .
1786 (constructor
1787 CheckpointSchemaResult
1788 CheckpointSchemaRejected
1789 (checkpointSimpleFailure
1790 (constructor
1791 CheckpointErrorCode
1792 CheckpointSchemaDigestFailed)
1793 ordinal)
1794 (checkpointSchemaTelemetryAt
1795 storageCount
1796 storageCount
1797 learnerCount
1798 placedCount
1799 (bytes-length material)
1800 digestTelemetry)))))
1801 (branch
1802 CheckpointBytesFailed
1803 code
1804 .
1805 (constructor
1806 CheckpointSchemaResult
1807 CheckpointSchemaRejected
1808 (checkpointSimpleFailure code zero)
1809 (checkpointSchemaTelemetryAt
1810 storageCount
1811 storageCount
1812 learnerCount
1813 placedCount
1814 zero
1815 checkpointInitialDigestTelemetry)))))
1816 (branch
1817 CheckpointPlacementRejected
1818 ordinal
1819 placedCount
1820 .
1821 (constructor
1822 CheckpointSchemaResult
1823 CheckpointSchemaRejected
1824 (checkpointSimpleFailure
1825 (constructor
1826 CheckpointErrorCode
1827 CheckpointStreamExtentOverflow)
1828 ordinal)
1829 (checkpointSchemaTelemetryAt
1830 storageCount
1831 storageCount
1832 learnerCount
1833 placedCount
1834 zero
1835 checkpointInitialDigestTelemetry)))))
1836 (checkpointFieldsAppend
1837 (checkpointParameterFields storages)
1838 learnerFields)))
1839 (branch
1840 CheckpointLearnerFieldsRejected
1841 code
1842 ordinal
1843 learnerCount
1844 .
1845 (constructor
1846 CheckpointSchemaResult
1847 CheckpointSchemaRejected
1848 (checkpointSimpleFailure code ordinal)
1849 (checkpointSchemaTelemetryAt
1850 storageCount
1851 storageCount
1852 learnerCount
1853 zero
1854 zero
1855 checkpointInitialDigestTelemetry)))))
1856 (branch
1857 CheckpointParameterCountRejected
1858 ordinal
1859 .
1860 (constructor
1861 CheckpointSchemaResult
1862 CheckpointSchemaRejected
1863 (checkpointSimpleFailure
1864 (constructor CheckpointErrorCode CheckpointParameterCountOverflow)
1865 ordinal)
1866 (checkpointSchemaTelemetryAt
1867 storageCount
1868 storageCount
1869 zero
1870 zero
1871 zero
1872 checkpointInitialDigestTelemetry)))))
1873 (branch
1874 CheckpointExtentRejected
1875 code
1876 ordinal
1877 .
1878 (constructor
1879 CheckpointSchemaResult
1880 CheckpointSchemaRejected
1881 (checkpointSimpleFailure code ordinal)
1882 (checkpointSchemaTelemetryAt
1883 storageCount
1884 zero
1885 zero
1886 zero
1887 zero
1888 checkpointInitialDigestTelemetry)))))
1889 (checkpointParameterStorageCount storages)))))))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.