1891def checkpointValidateSchemaIdentity =
1892 (lambda unrestricted schema : (family CheckpointSchema) .
1893 (eliminate
1894 CheckpointSchema
1895 (lambda unrestricted current : (family CheckpointSchema) .
1896 (family CheckpointSchemaIdentityResult))
1897 schema
1898 (branch
1899 CheckpointSchemaValue
1900 policy
1901 digest
1902 fields
1903 parameterCount
1904 payloadBytes
1905 .
1906 (eliminate
1907 CheckpointBytesResult
1908 (lambda unrestricted current : (family CheckpointBytesResult) .
1909 (family CheckpointSchemaIdentityResult))
1910 (checkpointCanonicalSchema policy parameterCount payloadBytes fields)
1911 (branch
1912 CheckpointBytesSucceeded
1913 material
1914 .
1915 (eliminate
1916 SHA256HexResult
1917 (lambda unrestricted current : (family SHA256HexResult) .
1918 (family CheckpointSchemaIdentityResult))
1919 (sha256Hex material)
1920 (branch
1921 SHA256HexSucceeded
1922 computed
1923 telemetry
1924 .
1925 (nat-eliminate
1926 (lambda unrestricted validLength : Nat . (family CheckpointSchemaIdentityResult))
1927 (constructor
1928 CheckpointSchemaIdentityResult
1929 CheckpointSchemaIdentityRejected
1930 (checkpointSimpleFailure
1931 (constructor CheckpointErrorCode CheckpointSchemaDigestLengthInvalid)
1932 zero)
1933 (bytes-length material))
1934 (lambda unrestricted lengthPredecessor : Nat .
1935 (lambda unrestricted lengthInduction : (family CheckpointSchemaIdentityResult) .
1936 (nat-eliminate
1937 (lambda unrestricted matched : Nat .
1938 (family CheckpointSchemaIdentityResult))
1939 (constructor
1940 CheckpointSchemaIdentityResult
1941 CheckpointSchemaIdentityRejected
1942 (checkpointFailure
1943 (constructor CheckpointErrorCode CheckpointSchemaIdentityMismatch)
1944 zero
1945 computed
1946 digest)
1947 (bytes-length material))
1948 (lambda unrestricted matchPredecessor : Nat .
1949 (lambda unrestricted matchInduction : (family CheckpointSchemaIdentityResult) .
1950 (constructor
1951 CheckpointSchemaIdentityResult
1952 CheckpointSchemaIdentityAccepted
1953 (bytes-length material))))
1954 (bytes-equal computed digest))))
1955 (naturalEqual (bytes-length computed) (byte-to-nat (byte 64)))))
1956 (branch
1957 SHA256HexFailed
1958 error
1959 ordinal
1960 telemetry
1961 .
1962 (constructor
1963 CheckpointSchemaIdentityResult
1964 CheckpointSchemaIdentityRejected
1965 (checkpointSimpleFailure
1966 (constructor CheckpointErrorCode CheckpointSchemaDigestFailed)
1967 ordinal)
1968 (bytes-length material)))))
1969 (branch
1970 CheckpointBytesFailed
1971 code
1972 .
1973 (constructor
1974 CheckpointSchemaIdentityResult
1975 CheckpointSchemaIdentityRejected
1976 (checkpointSimpleFailure code zero)
1977 zero))))))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.