Large source region · 2,376 lines
module Checkpoint.Schema
import Data.Bytes
import Data.SHA256Digest
import Data.UTF8
import Model.Parameter
import Model.Word64
import Std.Natural
family CheckpointLearnerStatePolicyTag : Type 0
constructor CheckpointStatelessLearnerState
constructor CheckpointAdamWLearnerState
end-family
family CheckpointLearnerStatePolicy : Type 0
constructor CheckpointStatelessPolicy
constructor CheckpointAdamWPolicy
end-family
family CheckpointLearnerComponent : Type 0
constructor CheckpointLearnerComponentValue
field unrestricted checkpointLearnerComponentPolicy : (family CheckpointLearnerStatePolicy)
end-family
family CheckpointParameterRole : Type 0
constructor CheckpointTrainableParameter
constructor CheckpointFrozenParameter
constructor CheckpointPersistentState
end-family
family CheckpointParameterStorage : Type 0
constructor CheckpointParameterStorageValue
field unrestricted checkpointStorageParameterRole : (family CheckpointParameterRole)
field unrestricted checkpointStorageParameterName : Bytes
field unrestricted checkpointStorageByteOffset : (family ModelWord64)
field unrestricted checkpointStorageByteLength : (family ModelWord64)
field unrestricted checkpointStorageElementCount : (family ModelWord64)
field unrestricted checkpointStorageDomain : Bytes
field unrestricted checkpointStorageInitialization : Bytes
end-family
family CheckpointParameterStorages : Type 0
constructor CheckpointParameterStoragesEnd
constructor CheckpointParameterStoragesNext
field unrestricted checkpointParameterStorageHead : (family CheckpointParameterStorage)
recursive unrestricted checkpointParameterStorageTail
end-family
family CheckpointProgram : Type 0
constructor CheckpointProgramValue
field unrestricted checkpointProgramParameters : (family CheckpointParameterStorages)
field unrestricted checkpointProgramLearner : (family CheckpointLearnerComponent)
end-family
family CheckpointFieldKind : Type 0
constructor CheckpointParameterField
field unrestricted checkpointParameterFieldRole : (family CheckpointParameterRole)
constructor CheckpointAdamWFirstMoment
constructor CheckpointAdamWSecondMoment
end-family
family CheckpointField : Type 0
constructor CheckpointFieldValue
field unrestricted checkpointFieldKind : (family CheckpointFieldKind)
field unrestricted checkpointFieldName : Bytes
field unrestricted checkpointFieldStorageByteOffset : (family ModelWord64)
field unrestricted checkpointFieldStreamByteOffset : (family ModelWord64)
field unrestricted checkpointFieldByteLength : (family ModelWord64)
field unrestricted checkpointFieldElementCount : (family ModelWord64)
field unrestricted checkpointFieldDomain : Bytes
field unrestricted checkpointFieldInitialization : Bytes
end-family
family CheckpointFields : Type 0
constructor CheckpointFieldsEnd
constructor CheckpointFieldsNext
field unrestricted checkpointFieldHead : (family CheckpointField)
recursive unrestricted checkpointFieldTail
end-family
family CheckpointSchema : Type 0
constructor CheckpointSchemaValue
field unrestricted checkpointSchemaPolicy : (family CheckpointLearnerStatePolicy)
field unrestricted checkpointSchemaSHA256 : Bytes
field unrestricted checkpointSchemaFields : (family CheckpointFields)
field unrestricted checkpointSchemaParameterCount : (family ModelWord64)
field unrestricted checkpointSchemaPayloadBytes : (family ModelWord64)
end-family
family CheckpointBlock : Type 0
constructor CheckpointBlockValue
field unrestricted checkpointBlockName : Bytes
field unrestricted checkpointBlockBytes : Bytes
end-family
family CheckpointBlocks : Type 0
constructor CheckpointBlocksEnd
constructor CheckpointBlocksNext
field unrestricted checkpointBlockHead : (family CheckpointBlock)
recursive unrestricted checkpointBlockTail
end-family
family CheckpointImage : Type 0
constructor CheckpointImageValue
field unrestricted checkpointImageSchemaSHA256 : Bytes
field unrestricted checkpointImageBlocks : (family CheckpointBlocks)
end-family
family CheckpointTypedBlock : Type 0
constructor CheckpointTypedBlockValue
field unrestricted checkpointTypedBlockKind : (family CheckpointFieldKind)
field unrestricted checkpointTypedBlockName : Bytes
field unrestricted checkpointTypedBlockStorageByteOffset : (family ModelWord64)
field unrestricted checkpointTypedBlockStreamByteOffset : (family ModelWord64)
field unrestricted checkpointTypedBlockElementCount : (family ModelWord64)
field unrestricted checkpointTypedBlockBytes : Bytes
end-family
family CheckpointTypedBlocks : Type 0
constructor CheckpointTypedBlocksEnd
constructor CheckpointTypedBlocksNext
field unrestricted checkpointTypedBlockHead : (family CheckpointTypedBlock)
recursive unrestricted checkpointTypedBlockTail
end-family
family CheckpointTypedCheckpoint : Type 0
constructor CheckpointTypedCheckpointValue
field unrestricted checkpointTypedPolicy : (family CheckpointLearnerStatePolicy)
field unrestricted checkpointTypedImage : (family CheckpointImage)
field unrestricted checkpointTypedBlocks : (family CheckpointTypedBlocks)
end-family
family CheckpointErrorCode : Type 0
constructor CheckpointParameterExtentOverflow
constructor CheckpointParameterCountOverflow
constructor CheckpointLearnerMomentExtentOverflow
constructor CheckpointLearnerAlignmentOverflow
constructor CheckpointStreamExtentOverflow
constructor CheckpointFieldCountOverflow
constructor CheckpointCanonicalUTF8Invalid
constructor CheckpointCanonicalLengthOverflow
constructor CheckpointCanonicalNumberOverflow
constructor CheckpointSchemaDigestFailed
constructor CheckpointSchemaDigestLengthInvalid
constructor CheckpointSchemaIdentityMismatch
constructor CheckpointFieldCountMismatch
constructor CheckpointFieldNameMismatch
constructor CheckpointPayloadLengthOverflow
constructor CheckpointPayloadLengthMismatch
constructor CheckpointPayloadExtentOverflow
constructor CheckpointPayloadExtentMismatch
constructor CheckpointSchemaVersionUnsupported
end-family
family CheckpointFailure : Type 0
constructor CheckpointFailureValue
field unrestricted checkpointFailureCode : (family CheckpointErrorCode)
field unrestricted checkpointFailureOrdinal : Nat
field unrestricted checkpointFailureExpected : Bytes
field unrestricted checkpointFailureActual : Bytes
end-family
family CheckpointSchemaTelemetry : Type 0
constructor CheckpointSchemaTelemetryValue
field unrestricted checkpointSchemaTelemetryStorageCount : Nat
field unrestricted checkpointSchemaTelemetryParameterFields : Nat
field unrestricted checkpointSchemaTelemetryLearnerFields : Nat
field unrestricted checkpointSchemaTelemetryPlacedFields : Nat
field unrestricted checkpointSchemaTelemetryCanonicalBytes : Nat
field unrestricted checkpointSchemaTelemetrySHA256 : (family SHA256DigestTelemetry)
field unrestricted checkpointSchemaTelemetryHostFallbacks : Nat
end-family
family CheckpointSchemaResult : Type 0
constructor CheckpointSchemaDerived
field unrestricted checkpointDerivedSchema : (family CheckpointSchema)
field unrestricted checkpointDerivedTelemetry : (family CheckpointSchemaTelemetry)
constructor CheckpointSchemaRejected
field unrestricted checkpointSchemaFailure : (family CheckpointFailure)
field unrestricted checkpointSchemaRejectedTelemetry : (family CheckpointSchemaTelemetry)
end-family
family CheckpointValidationTelemetry : Type 0
constructor CheckpointValidationTelemetryValue
field unrestricted checkpointValidationExpectedBlocks : Nat
field unrestricted checkpointValidationActualBlocks : Nat
field unrestricted checkpointValidationValidatedBlocks : Nat
field unrestricted checkpointValidationPayloadBytes : (family ModelWord64)
field unrestricted checkpointValidationCanonicalBytes : Nat
field unrestricted checkpointValidationHostFallbacks : Nat
end-family
family CheckpointLoadResult : Type 0
constructor CheckpointLoaded
field unrestricted checkpointLoadedValue : (family CheckpointTypedCheckpoint)
field unrestricted checkpointLoadedTelemetry : (family CheckpointValidationTelemetry)
constructor CheckpointLoadRejected
field unrestricted checkpointLoadFailure : (family CheckpointFailure)
field unrestricted checkpointLoadRejectedTelemetry : (family CheckpointValidationTelemetry)
end-family
family CheckpointWord64Result : Type 0
constructor CheckpointWord64Succeeded
field unrestricted checkpointWord64Value : (family ModelWord64)
constructor CheckpointWord64Failed
field unrestricted checkpointWord64FailureCode : (family CheckpointErrorCode)
end-family
family CheckpointBytesResult : Type 0
constructor CheckpointBytesSucceeded
field unrestricted checkpointBytesValue : Bytes
constructor CheckpointBytesFailed
field unrestricted checkpointBytesFailureCode : (family CheckpointErrorCode)
end-family
family CheckpointExtentResult : Type 0
constructor CheckpointExtentAccepted
field unrestricted checkpointAcceptedExtent : (family ModelWord64)
constructor CheckpointExtentRejected
field unrestricted checkpointExtentFailureCode : (family CheckpointErrorCode)
field unrestricted checkpointExtentFailureOrdinal : Nat
end-family
family CheckpointParameterCountResult : Type 0
constructor CheckpointParameterCountAccepted
field unrestricted checkpointAcceptedParameterCount : (family ModelWord64)
constructor CheckpointParameterCountRejected
field unrestricted checkpointParameterCountFailureOrdinal : Nat
end-family
family CheckpointLearnerFieldsResult : Type 0
constructor CheckpointLearnerFieldsAccepted
field unrestricted checkpointAcceptedLearnerFields : (family CheckpointFields)
field unrestricted checkpointAcceptedLearnerExtent : (family ModelWord64)
field unrestricted checkpointAcceptedLearnerFieldCount : Nat
constructor CheckpointLearnerFieldsRejected
field unrestricted checkpointLearnerFieldsFailureCode : (family CheckpointErrorCode)
field unrestricted checkpointLearnerFieldsFailureOrdinal : Nat
field unrestricted checkpointRejectedLearnerFieldCount : Nat
end-family
family CheckpointPlacementResult : Type 0
constructor CheckpointPlacementAccepted
field unrestricted checkpointPlacedFields : (family CheckpointFields)
field unrestricted checkpointPlacedPayloadBytes : (family ModelWord64)
field unrestricted checkpointPlacedFieldCount : Nat
constructor CheckpointPlacementRejected
field unrestricted checkpointPlacementFailureOrdinal : Nat
field unrestricted checkpointPlacementPlacedFieldCount : Nat
end-family
family CheckpointSchemaIdentityResult : Type 0
constructor CheckpointSchemaIdentityAccepted
field unrestricted checkpointSchemaIdentityCanonicalBytes : Nat
constructor CheckpointSchemaIdentityRejected
field unrestricted checkpointSchemaIdentityFailure : (family CheckpointFailure)
field unrestricted checkpointSchemaIdentityRejectedCanonicalBytes : Nat
end-family
family CheckpointBlocksValidationResult : Type 0
constructor CheckpointBlocksAccepted
field unrestricted checkpointAcceptedTypedBlocks : (family CheckpointTypedBlocks)
field unrestricted checkpointAcceptedBlockPayloadBytes : (family ModelWord64)
field unrestricted checkpointAcceptedBlockCount : Nat
constructor CheckpointBlocksRejected
field unrestricted checkpointBlocksFailure : (family CheckpointFailure)
field unrestricted checkpointRejectedBlockPayloadBytes : (family ModelWord64)
field unrestricted checkpointRejectedBlockCount : Nat
end-family
def checkpointStatelessLearnerState =
(constructor CheckpointLearnerStatePolicy CheckpointStatelessPolicy)
def checkpointAdamWLearnerState =
(constructor CheckpointLearnerStatePolicy CheckpointAdamWPolicy)
def checkpointLearnerStatePolicyTag =
(lambda unrestricted policy : (family CheckpointLearnerStatePolicy) .
(eliminate
CheckpointLearnerStatePolicy
(lambda unrestricted current : (family CheckpointLearnerStatePolicy) .
(family CheckpointLearnerStatePolicyTag))
policy
(branch
CheckpointStatelessPolicy
.
(constructor CheckpointLearnerStatePolicyTag CheckpointStatelessLearnerState))
(branch
CheckpointAdamWPolicy
.
(constructor CheckpointLearnerStatePolicyTag CheckpointAdamWLearnerState))))
def checkpointLearnerComponent =
(lambda unrestricted policy : (family CheckpointLearnerStatePolicy) .
(constructor CheckpointLearnerComponent CheckpointLearnerComponentValue policy))
def checkpointProgram =
(lambda unrestricted parameters : (family CheckpointParameterStorages) .
(lambda unrestricted learner : (family CheckpointLearnerComponent) .
(constructor CheckpointProgram CheckpointProgramValue parameters learner)))
def checkpointErrorCodeBytes =
(lambda unrestricted code : (family CheckpointErrorCode) .
(eliminate
CheckpointErrorCode
(lambda unrestricted current : (family CheckpointErrorCode) . Bytes)
code
(branch
CheckpointParameterExtentOverflow
.
b"ALPHA-CKPT-SCHEMA-001")
(branch
CheckpointParameterCountOverflow
.
b"ALPHA-CKPT-SCHEMA-002")
(branch
CheckpointLearnerMomentExtentOverflow
.
b"ALPHA-CKPT-SCHEMA-003")
(branch
CheckpointLearnerAlignmentOverflow
.
b"ALPHA-CKPT-SCHEMA-004")
(branch
CheckpointStreamExtentOverflow
.
b"ALPHA-CKPT-SCHEMA-005")
(branch
CheckpointFieldCountOverflow
.
b"ALPHA-CKPT-SCHEMA-006")
(branch
CheckpointCanonicalUTF8Invalid
.
b"ALPHA-CKPT-SCHEMA-007")
(branch
CheckpointCanonicalLengthOverflow
.
b"ALPHA-CKPT-SCHEMA-008")
(branch
CheckpointCanonicalNumberOverflow
.
b"ALPHA-CKPT-SCHEMA-009")
(branch
CheckpointSchemaDigestFailed
.
b"ALPHA-CKPT-SCHEMA-010")
(branch
CheckpointSchemaDigestLengthInvalid
.
b"ALPHA-CKPT-SCHEMA-011")
(branch
CheckpointSchemaIdentityMismatch
.
b"ALPHA-CKPT-SCHEMA-012")
(branch
CheckpointFieldCountMismatch
.
b"ALPHA-CKPT-SCHEMA-013")
(branch
CheckpointFieldNameMismatch
.
b"ALPHA-CKPT-SCHEMA-014")
(branch
CheckpointPayloadLengthOverflow
.
b"ALPHA-CKPT-SCHEMA-015")
(branch
CheckpointPayloadLengthMismatch
.
b"ALPHA-CKPT-SCHEMA-016")
(branch
CheckpointPayloadExtentOverflow
.
b"ALPHA-CKPT-SCHEMA-017")
(branch
CheckpointPayloadExtentMismatch
.
b"ALPHA-CKPT-SCHEMA-018")
(branch
CheckpointSchemaVersionUnsupported
.
b"ALPHA-CKPT-SCHEMA-019")))
def checkpointFailure =
(lambda unrestricted code : (family CheckpointErrorCode) .
(lambda unrestricted ordinal : Nat .
(lambda unrestricted expected : Bytes .
(lambda unrestricted actual : Bytes .
(constructor CheckpointFailure CheckpointFailureValue code ordinal expected actual)))))
def checkpointSimpleFailure =
(lambda unrestricted code : (family CheckpointErrorCode) .
(lambda unrestricted ordinal : Nat . (checkpointFailure code ordinal b"" b"")))
def checkpointSchemaTelemetry =
(lambda unrestricted storages : Nat .
(lambda unrestricted parameters : Nat .
(lambda unrestricted learner : Nat .
(lambda unrestricted placed : Nat .
(lambda unrestricted canonicalBytes : Nat .
(lambda unrestricted digestTelemetry : (family SHA256DigestTelemetry) .
(constructor
CheckpointSchemaTelemetry
CheckpointSchemaTelemetryValue
storages
parameters
learner
placed
canonicalBytes
digestTelemetry
zero)))))))
def checkpointInitialDigestTelemetry =
(sha256DigestTelemetryInitial zero zero)
def checkpointValidationTelemetry =
(lambda unrestricted expected : Nat .
(lambda unrestricted actual : Nat .
(lambda unrestricted validated : Nat .
(lambda unrestricted payload : (family ModelWord64) .
(lambda unrestricted canonicalBytes : Nat .
(constructor
CheckpointValidationTelemetry
CheckpointValidationTelemetryValue
expected
actual
validated
payload
canonicalBytes
zero))))))
def checkpointWord64Four =
(constructor
ModelWord64
ModelWord64Value
(byte 4)
(byte 0)
(byte 0)
(byte 0)
(byte 0)
(byte 0)
(byte 0)
(byte 0))
def checkpointWord64SixtyThree =
(constructor
ModelWord64
ModelWord64Value
(byte 63)
(byte 0)
(byte 0)
(byte 0)
(byte 0)
(byte 0)
(byte 0)
(byte 0))
def checkpointWord64SixtyFour =
(constructor
ModelWord64
ModelWord64Value
(byte 64)
(byte 0)
(byte 0)
(byte 0)
(byte 0)
(byte 0)
(byte 0)
(byte 0))
def checkpointWord64AlignmentMask =
(constructor
ModelWord64
ModelWord64Value
(byte 192)
(byte 255)
(byte 255)
(byte 255)
(byte 255)
(byte 255)
(byte 255)
(byte 255))
def checkpointAddChecked =
(lambda unrestricted code : (family CheckpointErrorCode) .
(lambda unrestricted left : (family ModelWord64) .
(lambda unrestricted right : (family ModelWord64) .
(eliminate
ModelWord64CheckedResult
(lambda unrestricted current : (family ModelWord64CheckedResult) .
(family CheckpointWord64Result))
(modelWord64AddChecked left right)
(branch
ModelWord64CheckedSucceeded
value
.
(constructor CheckpointWord64Result CheckpointWord64Succeeded value))
(branch
ModelWord64CheckedFailed
error
.
(constructor CheckpointWord64Result CheckpointWord64Failed code))))))
def checkpointMultiplyFourChecked =
(lambda unrestricted value : (family ModelWord64) .
(eliminate
ModelWord64MultiplyCheckedResult
(lambda unrestricted current : (family ModelWord64MultiplyCheckedResult) .
(family CheckpointWord64Result))
(modelWord64MultiplyChecked value checkpointWord64Four)
(branch
ModelWord64MultiplySucceeded
product
.
(constructor CheckpointWord64Result CheckpointWord64Succeeded product))
(branch
ModelWord64MultiplyOverflow
.
(constructor
CheckpointWord64Result
CheckpointWord64Failed
(constructor CheckpointErrorCode CheckpointLearnerMomentExtentOverflow)))))
def checkpointAlignUp64 =
(lambda unrestricted value : (family ModelWord64) .
(eliminate
CheckpointWord64Result
(lambda unrestricted current : (family CheckpointWord64Result) .
(family CheckpointWord64Result))
(checkpointAddChecked
(constructor CheckpointErrorCode CheckpointLearnerAlignmentOverflow)
value
checkpointWord64SixtyThree)
(branch
CheckpointWord64Succeeded
rounded
.
(constructor
CheckpointWord64Result
CheckpointWord64Succeeded
(modelWord64And rounded checkpointWord64AlignmentMask)))
(branch
CheckpointWord64Failed
code
.
(constructor CheckpointWord64Result CheckpointWord64Failed code))))
def checkpointNaturalByteAt =
(lambda unrestricted value : Nat .
(lambda unrestricted shift : Nat .
(nat-to-byte
(naturalModuloUnchecked
(naturalDivideUnchecked value (naturalPowerOfTwo shift))
(succ (byte-to-nat (byte 255)))))))
def checkpointNaturalWord64 =
(lambda unrestricted code : (family CheckpointErrorCode) .
(lambda unrestricted value : Nat .
(nat-eliminate
(lambda unrestricted fits : Nat . (family CheckpointWord64Result))
(constructor CheckpointWord64Result CheckpointWord64Failed code)
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : (family CheckpointWord64Result) .
(constructor
CheckpointWord64Result
CheckpointWord64Succeeded
(constructor
ModelWord64
ModelWord64Value
(checkpointNaturalByteAt value zero)
(checkpointNaturalByteAt value (byte-to-nat (byte 8)))
(checkpointNaturalByteAt value (byte-to-nat (byte 16)))
(checkpointNaturalByteAt value (byte-to-nat (byte 24)))
(checkpointNaturalByteAt value (byte-to-nat (byte 32)))
(checkpointNaturalByteAt value (byte-to-nat (byte 40)))
(checkpointNaturalByteAt value (byte-to-nat (byte 48)))
(checkpointNaturalByteAt value (byte-to-nat (byte 56)))))))
(naturalIsZero (naturalDivideUnchecked value (naturalPowerOfTwo (byte-to-nat (byte 64))))))))
def checkpointWord64ToNatural =
(lambda unrestricted value : (family ModelWord64) .
(eliminate
ModelWord64
(lambda unrestricted current : (family ModelWord64) . Nat)
value
(branch
ModelWord64Value
b0
b1
b2
b3
b4
b5
b6
b7
.
(naturalAdd
(byte-to-nat b0)
(naturalAdd
(naturalMultiply (byte-to-nat b1) (naturalPowerOfTwo (byte-to-nat (byte 8))))
(naturalAdd
(naturalMultiply (byte-to-nat b2) (naturalPowerOfTwo (byte-to-nat (byte 16))))
(naturalAdd
(naturalMultiply (byte-to-nat b3) (naturalPowerOfTwo (byte-to-nat (byte 24))))
(naturalAdd
(naturalMultiply (byte-to-nat b4) (naturalPowerOfTwo (byte-to-nat (byte 32))))
(naturalAdd
(naturalMultiply (byte-to-nat b5) (naturalPowerOfTwo (byte-to-nat (byte 40))))
(naturalAdd
(naturalMultiply (byte-to-nat b6) (naturalPowerOfTwo (byte-to-nat (byte 48))))
(naturalMultiply (byte-to-nat b7) (naturalPowerOfTwo (byte-to-nat (byte 56))))))))))))))
def checkpointBytesResultAppend =
(lambda unrestricted left : (family CheckpointBytesResult) .
(lambda unrestricted right : (family CheckpointBytesResult) .
(eliminate
CheckpointBytesResult
(lambda unrestricted current : (family CheckpointBytesResult) .
(family CheckpointBytesResult))
left
(branch
CheckpointBytesSucceeded
leftBytes
.
(eliminate
CheckpointBytesResult
(lambda unrestricted current : (family CheckpointBytesResult) .
(family CheckpointBytesResult))
right
(branch
CheckpointBytesSucceeded
rightBytes
.
(constructor
CheckpointBytesResult
CheckpointBytesSucceeded
(bytes-append leftBytes rightBytes)))
(branch
CheckpointBytesFailed
code
.
(constructor CheckpointBytesResult CheckpointBytesFailed code))))
(branch
CheckpointBytesFailed
code
.
(constructor CheckpointBytesResult CheckpointBytesFailed code)))))
def checkpointBytesSuccess =
(lambda unrestricted value : Bytes .
(constructor CheckpointBytesResult CheckpointBytesSucceeded value))
def checkpointDecimalWithFuel =
(lambda unrestricted fuel : Nat .
(nat-eliminate
(lambda unrestricted current : Nat .
(pi unrestricted value : Nat . (family CheckpointBytesResult)))
(lambda unrestricted value : Nat .
(nat-eliminate
(lambda unrestricted isZero : Nat . (family CheckpointBytesResult))
(constructor
CheckpointBytesResult
CheckpointBytesFailed
(constructor CheckpointErrorCode CheckpointCanonicalNumberOverflow))
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : (family CheckpointBytesResult) .
(constructor CheckpointBytesResult CheckpointBytesSucceeded b"")))
(naturalIsZero value)))
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : (pi unrestricted value : Nat . (family CheckpointBytesResult)) .
(lambda unrestricted value : Nat .
(nat-eliminate
(lambda unrestricted isZero : Nat . (family CheckpointBytesResult))
(eliminate
CheckpointBytesResult
(lambda unrestricted current : (family CheckpointBytesResult) .
(family CheckpointBytesResult))
(induction (naturalDivideUnchecked value (byte-to-nat (byte 10))))
(branch
CheckpointBytesSucceeded
prefix
.
(constructor
CheckpointBytesResult
CheckpointBytesSucceeded
(bytes-append
prefix
(bytes
(nat-to-byte
(naturalAdd
(byte-to-nat (byte 48))
(naturalModuloUnchecked value (byte-to-nat (byte 10)))))))))
(branch
CheckpointBytesFailed
code
.
(constructor CheckpointBytesResult CheckpointBytesFailed code)))
(lambda unrestricted zeroPredecessor : Nat .
(lambda unrestricted zeroInduction : (family CheckpointBytesResult) .
(constructor CheckpointBytesResult CheckpointBytesSucceeded b"")))
(naturalIsZero value)))))
fuel))
def checkpointWord64Decimal =
(lambda unrestricted value : (family ModelWord64) .
(nat-eliminate
(lambda unrestricted isZero : Nat . (family CheckpointBytesResult))
(checkpointDecimalWithFuel (byte-to-nat (byte 20)) (checkpointWord64ToNatural value))
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : (family CheckpointBytesResult) .
(constructor CheckpointBytesResult CheckpointBytesSucceeded b"0")))
(modelWord64IsZero value)))
def checkpointIntegerField =
(lambda unrestricted value : (family ModelWord64) .
(checkpointBytesResultAppend
(checkpointBytesSuccess b";i")
(checkpointWord64Decimal value)))
def checkpointUTF8CodepointCount =
(lambda unrestricted codepoints : (family UTF8Codepoints) .
(eliminate
UTF8Codepoints
(lambda unrestricted current : (family UTF8Codepoints) . Nat)
codepoints
(branch UTF8CodepointsEnd . zero)
(branch UTF8CodepointsNext head tail ih_tail . (succ ih_tail))))
def checkpointSizedField =
(lambda unrestricted value : Bytes .
(eliminate
UTF8DecodeResult
(lambda unrestricted current : (family UTF8DecodeResult) . (family CheckpointBytesResult))
(decodeUTF8 value)
(branch
UTF8DecodeSucceeded
codepoints
.
(eliminate
CheckpointWord64Result
(lambda unrestricted current : (family CheckpointWord64Result) .
(family CheckpointBytesResult))
(checkpointNaturalWord64
(constructor CheckpointErrorCode CheckpointCanonicalLengthOverflow)
(checkpointUTF8CodepointCount codepoints))
(branch
CheckpointWord64Succeeded
length
.
(checkpointBytesResultAppend
(checkpointBytesSuccess b";s")
(checkpointBytesResultAppend
(checkpointWord64Decimal length)
(checkpointBytesSuccess (bytes-append b":" value)))))
(branch
CheckpointWord64Failed
code
.
(constructor CheckpointBytesResult CheckpointBytesFailed code))))
(branch
UTF8DecodeFailed
error
offset
.
(constructor
CheckpointBytesResult
CheckpointBytesFailed
(constructor CheckpointErrorCode CheckpointCanonicalUTF8Invalid)))))
def checkpointFieldsAppend =
(lambda unrestricted left : (family CheckpointFields) .
(lambda unrestricted right : (family CheckpointFields) .
(eliminate
CheckpointFields
(lambda unrestricted current : (family CheckpointFields) . (family CheckpointFields))
left
(branch CheckpointFieldsEnd . right)
(branch
CheckpointFieldsNext
head
tail
ih_tail
.
(constructor CheckpointFields CheckpointFieldsNext head ih_tail)))))
def checkpointParameterStorageCount =
(lambda unrestricted storages : (family CheckpointParameterStorages) .
(eliminate
CheckpointParameterStorages
(lambda unrestricted current : (family CheckpointParameterStorages) . Nat)
storages
(branch CheckpointParameterStoragesEnd . zero)
(branch CheckpointParameterStoragesNext head tail ih_tail . (succ ih_tail))))
def checkpointFieldsCount =
(lambda unrestricted fields : (family CheckpointFields) .
(eliminate
CheckpointFields
(lambda unrestricted current : (family CheckpointFields) . Nat)
fields
(branch CheckpointFieldsEnd . zero)
(branch CheckpointFieldsNext head tail ih_tail . (succ ih_tail))))
def checkpointBlocksCount =
(lambda unrestricted blocks : (family CheckpointBlocks) .
(eliminate
CheckpointBlocks
(lambda unrestricted current : (family CheckpointBlocks) . Nat)
blocks
(branch CheckpointBlocksEnd . zero)
(branch CheckpointBlocksNext head tail ih_tail . (succ ih_tail))))
def checkpointParameterField =
(lambda unrestricted storage : (family CheckpointParameterStorage) .
(eliminate
CheckpointParameterStorage
(lambda unrestricted current : (family CheckpointParameterStorage) . (family CheckpointField))
storage
(branch
CheckpointParameterStorageValue
role
name
offset
byteLength
elements
domain
initialization
.
(constructor
CheckpointField
CheckpointFieldValue
(constructor CheckpointFieldKind CheckpointParameterField role)
(bytes-append b"parameter/" name)
offset
modelWord64Zero
byteLength
elements
domain
initialization))))
def checkpointParameterFields =
(lambda unrestricted storages : (family CheckpointParameterStorages) .
(eliminate
CheckpointParameterStorages
(lambda unrestricted current : (family CheckpointParameterStorages) .
(family CheckpointFields))
storages
(branch CheckpointParameterStoragesEnd . (constructor CheckpointFields CheckpointFieldsEnd))
(branch
CheckpointParameterStoragesNext
head
tail
ih_tail
.
(constructor CheckpointFields CheckpointFieldsNext (checkpointParameterField head) ih_tail))))
def checkpointStorageFieldsEnd =
(lambda unrestricted storages : (family CheckpointParameterStorages) .
(eliminate
CheckpointParameterStorages
(lambda unrestricted current : (family CheckpointParameterStorages) .
(family CheckpointExtentResult))
storages
(branch
CheckpointParameterStoragesEnd
.
(constructor CheckpointExtentResult CheckpointExtentAccepted modelWord64Zero))
(branch
CheckpointParameterStoragesNext
head
tail
ih_tail
.
(eliminate
CheckpointParameterStorage
(lambda unrestricted current : (family CheckpointParameterStorage) .
(family CheckpointExtentResult))
head
(branch
CheckpointParameterStorageValue
role
name
offset
byteLength
elements
domain
initialization
.
(eliminate
CheckpointWord64Result
(lambda unrestricted current : (family CheckpointWord64Result) .
(family CheckpointExtentResult))
(checkpointAddChecked
(constructor CheckpointErrorCode CheckpointParameterExtentOverflow)
offset
byteLength)
(branch
CheckpointWord64Succeeded
headEnd
.
(eliminate
CheckpointExtentResult
(lambda unrestricted current : (family CheckpointExtentResult) .
(family CheckpointExtentResult))
ih_tail
(branch
CheckpointExtentAccepted
tailEnd
.
(constructor
CheckpointExtentResult
CheckpointExtentAccepted
(modelWord64Select (modelWord64LessThan headEnd tailEnd) tailEnd headEnd)))
(branch
CheckpointExtentRejected
code
ordinal
.
(constructor
CheckpointExtentResult
CheckpointExtentRejected
code
(succ ordinal)))))
(branch
CheckpointWord64Failed
code
.
(constructor CheckpointExtentResult CheckpointExtentRejected code zero))))))))
def checkpointParameterCount =
(lambda unrestricted storages : (family CheckpointParameterStorages) .
(eliminate
CheckpointParameterStorages
(lambda unrestricted current : (family CheckpointParameterStorages) .
(family CheckpointParameterCountResult))
storages
(branch
CheckpointParameterStoragesEnd
.
(constructor
CheckpointParameterCountResult
CheckpointParameterCountAccepted
modelWord64Zero))
(branch
CheckpointParameterStoragesNext
head
tail
ih_tail
.
(eliminate
CheckpointParameterCountResult
(lambda unrestricted current : (family CheckpointParameterCountResult) .
(family CheckpointParameterCountResult))
ih_tail
(branch
CheckpointParameterCountAccepted
tailCount
.
(eliminate
CheckpointParameterStorage
(lambda unrestricted current : (family CheckpointParameterStorage) .
(family CheckpointParameterCountResult))
head
(branch
CheckpointParameterStorageValue
role
name
offset
byteLength
elements
domain
initialization
.
(eliminate
CheckpointParameterRole
(lambda unrestricted current : (family CheckpointParameterRole) .
(family CheckpointParameterCountResult))
role
(branch
CheckpointTrainableParameter
.
(eliminate
CheckpointWord64Result
(lambda unrestricted current : (family CheckpointWord64Result) .
(family CheckpointParameterCountResult))
(checkpointAddChecked
(constructor CheckpointErrorCode CheckpointParameterCountOverflow)
elements
tailCount)
(branch
CheckpointWord64Succeeded
count
.
(constructor
CheckpointParameterCountResult
CheckpointParameterCountAccepted
count))
(branch
CheckpointWord64Failed
code
.
(constructor
CheckpointParameterCountResult
CheckpointParameterCountRejected
zero))))
(branch
CheckpointFrozenParameter
.
(eliminate
CheckpointWord64Result
(lambda unrestricted current : (family CheckpointWord64Result) .
(family CheckpointParameterCountResult))
(checkpointAddChecked
(constructor CheckpointErrorCode CheckpointParameterCountOverflow)
elements
tailCount)
(branch
CheckpointWord64Succeeded
count
.
(constructor
CheckpointParameterCountResult
CheckpointParameterCountAccepted
count))
(branch
CheckpointWord64Failed
code
.
(constructor
CheckpointParameterCountResult
CheckpointParameterCountRejected
zero))))
(branch
CheckpointPersistentState
.
(constructor
CheckpointParameterCountResult
CheckpointParameterCountAccepted
tailCount))))))
(branch
CheckpointParameterCountRejected
ordinal
.
(constructor
CheckpointParameterCountResult
CheckpointParameterCountRejected
(succ ordinal)))))))
def checkpointMomentDomain =
(lambda unrestricted elements : (family ModelWord64) .
(checkpointBytesResultAppend
(checkpointBytesSuccess b"DenseF32State(")
(checkpointBytesResultAppend
(checkpointWord64Decimal elements)
(checkpointBytesSuccess b")"))))
def checkpointMomentField =
(lambda unrestricted kind : (family CheckpointFieldKind) .
(lambda unrestricted slot : Bytes .
(lambda unrestricted parameterName : Bytes .
(lambda unrestricted offset : (family ModelWord64) .
(lambda unrestricted byteLength : (family ModelWord64) .
(lambda unrestricted elements : (family ModelWord64) .
(lambda unrestricted domain : Bytes .
(constructor
CheckpointField
CheckpointFieldValue
kind
(bytes-append
b"learner/adamw/"
(bytes-append slot (bytes-append b"/" parameterName)))
offset
modelWord64Zero
byteLength
elements
domain
b"zero"))))))))
def checkpointDeriveAdamWFields =
(lambda unrestricted storages : (family CheckpointParameterStorages) .
(eliminate
CheckpointParameterStorages
(lambda unrestricted current : (family CheckpointParameterStorages) .
(pi unrestricted cursor : (family ModelWord64) . (family CheckpointLearnerFieldsResult)))
-- the scrutinee, which was missing: `eliminate F` takes motive,
-- SCRUTINEE, then one branch per constructor. Without it the End
-- branch's body sat in the scrutinee's slot and the eliminator was
-- handed a `pi cursor : ModelWord64 . ...` where a family belongs.
storages
(branch
CheckpointParameterStoragesEnd
.
(lambda unrestricted cursor : (family ModelWord64) .
(constructor
CheckpointLearnerFieldsResult
CheckpointLearnerFieldsAccepted
(constructor CheckpointFields CheckpointFieldsEnd)
cursor
zero)))
(branch
CheckpointParameterStoragesNext
head
tail
ih_tail
.
(lambda unrestricted cursor : (family ModelWord64) .
(eliminate
CheckpointParameterStorage
(lambda unrestricted current : (family CheckpointParameterStorage) .
(family CheckpointLearnerFieldsResult))
head
(branch
CheckpointParameterStorageValue
role
name
parameterOffset
parameterBytes
elements
domain
initialization
.
(eliminate
CheckpointParameterRole
(lambda unrestricted current : (family CheckpointParameterRole) .
(family CheckpointLearnerFieldsResult))
role
(branch
CheckpointTrainableParameter
.
(eliminate
CheckpointWord64Result
(lambda unrestricted current : (family CheckpointWord64Result) .
(family CheckpointLearnerFieldsResult))
(checkpointAlignUp64 cursor)
(branch
CheckpointWord64Succeeded
firstOffset
.
(eliminate
CheckpointWord64Result
(lambda unrestricted current : (family CheckpointWord64Result) .
(family CheckpointLearnerFieldsResult))
(checkpointMultiplyFourChecked elements)
(branch
CheckpointWord64Succeeded
momentBytes
.
(eliminate
CheckpointWord64Result
(lambda unrestricted current : (family CheckpointWord64Result) .
(family CheckpointLearnerFieldsResult))
(checkpointAddChecked
(constructor
CheckpointErrorCode
CheckpointLearnerMomentExtentOverflow)
firstOffset
momentBytes)
(branch
CheckpointWord64Succeeded
afterFirst
.
(eliminate
CheckpointWord64Result
(lambda unrestricted current : (family CheckpointWord64Result) .
(family CheckpointLearnerFieldsResult))
(checkpointAlignUp64 afterFirst)
(branch
CheckpointWord64Succeeded
secondOffset
.
(eliminate
CheckpointWord64Result
(lambda unrestricted current : (family CheckpointWord64Result) .
(family CheckpointLearnerFieldsResult))
(checkpointAddChecked
(constructor
CheckpointErrorCode
CheckpointLearnerMomentExtentOverflow)
secondOffset
momentBytes)
(branch
CheckpointWord64Succeeded
nextCursor
.
(eliminate
CheckpointBytesResult
(lambda unrestricted current : (family CheckpointBytesResult) .
(family CheckpointLearnerFieldsResult))
(checkpointMomentDomain elements)
(branch
CheckpointBytesSucceeded
momentDomain
.
(eliminate
CheckpointLearnerFieldsResult
(lambda unrestricted current : (family CheckpointLearnerFieldsResult) .
(family CheckpointLearnerFieldsResult))
(ih_tail nextCursor)
(branch
CheckpointLearnerFieldsAccepted
tailFields
finalExtent
tailCount
.
(constructor
CheckpointLearnerFieldsResult
CheckpointLearnerFieldsAccepted
(constructor
CheckpointFields
CheckpointFieldsNext
(checkpointMomentField
(constructor CheckpointFieldKind CheckpointAdamWFirstMoment)
b"first-moment"
name
firstOffset
momentBytes
elements
momentDomain)
(constructor
CheckpointFields
CheckpointFieldsNext
(checkpointMomentField
(constructor
CheckpointFieldKind
CheckpointAdamWSecondMoment)
b"second-moment"
name
secondOffset
momentBytes
elements
momentDomain)
tailFields))
finalExtent
(succ (succ tailCount))))
(branch
CheckpointLearnerFieldsRejected
code
ordinal
count
.
(constructor
CheckpointLearnerFieldsResult
CheckpointLearnerFieldsRejected
code
(succ ordinal)
count))))
(branch
CheckpointBytesFailed
code
.
(constructor
CheckpointLearnerFieldsResult
CheckpointLearnerFieldsRejected
code
zero
zero))))
(branch
CheckpointWord64Failed
code
.
(constructor
CheckpointLearnerFieldsResult
CheckpointLearnerFieldsRejected
code
zero
zero))))
(branch
CheckpointWord64Failed
code
.
(constructor
CheckpointLearnerFieldsResult
CheckpointLearnerFieldsRejected
code
zero
zero))))
(branch
CheckpointWord64Failed
code
.
(constructor
CheckpointLearnerFieldsResult
CheckpointLearnerFieldsRejected
code
zero
zero))))
(branch
CheckpointWord64Failed
code
.
(constructor
CheckpointLearnerFieldsResult
CheckpointLearnerFieldsRejected
code
zero
zero))))
(branch
CheckpointWord64Failed
code
.
(constructor
CheckpointLearnerFieldsResult
CheckpointLearnerFieldsRejected
code
zero
zero))))
(branch CheckpointFrozenParameter . (ih_tail cursor))
(branch CheckpointPersistentState . (ih_tail cursor)))))))))
def checkpointDeriveLearnerFields =
(lambda unrestricted policy : (family CheckpointLearnerStatePolicy) .
(lambda unrestricted storages : (family CheckpointParameterStorages) .
(lambda unrestricted initialOffset : (family ModelWord64) .
(eliminate
CheckpointLearnerStatePolicy
(lambda unrestricted current : (family CheckpointLearnerStatePolicy) .
(family CheckpointLearnerFieldsResult))
policy
(branch
CheckpointStatelessPolicy
.
(constructor
CheckpointLearnerFieldsResult
CheckpointLearnerFieldsAccepted
(constructor CheckpointFields CheckpointFieldsEnd)
initialOffset
zero))
(branch CheckpointAdamWPolicy . (checkpointDeriveAdamWFields storages initialOffset))))))
def checkpointFieldWithStreamOffset =
(lambda unrestricted field : (family CheckpointField) .
(lambda unrestricted streamOffset : (family ModelWord64) .
(eliminate
CheckpointField
(lambda unrestricted current : (family CheckpointField) . (family CheckpointField))
field
(branch
CheckpointFieldValue
kind
name
storageOffset
oldStreamOffset
byteLength
elements
domain
initialization
.
(constructor
CheckpointField
CheckpointFieldValue
kind
name
storageOffset
streamOffset
byteLength
elements
domain
initialization)))))
def checkpointPlaceStreamFields =
(lambda unrestricted fields : (family CheckpointFields) .
(eliminate
CheckpointFields
(lambda unrestricted current : (family CheckpointFields) .
(pi unrestricted offset : (family ModelWord64) . (family CheckpointPlacementResult)))
fields
(branch
CheckpointFieldsEnd
.
(lambda unrestricted offset : (family ModelWord64) .
(constructor
CheckpointPlacementResult
CheckpointPlacementAccepted
(constructor CheckpointFields CheckpointFieldsEnd)
offset
zero)))
(branch
CheckpointFieldsNext
head
tail
ih_tail
.
(lambda unrestricted offset : (family ModelWord64) .
(eliminate
CheckpointField
(lambda unrestricted current : (family CheckpointField) .
(family CheckpointPlacementResult))
head
(branch
CheckpointFieldValue
kind
name
storageOffset
oldStreamOffset
byteLength
elements
domain
initialization
.
(eliminate
CheckpointWord64Result
(lambda unrestricted current : (family CheckpointWord64Result) .
(family CheckpointPlacementResult))
(checkpointAddChecked
(constructor CheckpointErrorCode CheckpointStreamExtentOverflow)
offset
byteLength)
(branch
CheckpointWord64Succeeded
nextOffset
.
(eliminate
CheckpointPlacementResult
(lambda unrestricted current : (family CheckpointPlacementResult) .
(family CheckpointPlacementResult))
(ih_tail nextOffset)
(branch
CheckpointPlacementAccepted
tailFields
payloadBytes
tailCount
.
(constructor
CheckpointPlacementResult
CheckpointPlacementAccepted
(constructor
CheckpointFields
CheckpointFieldsNext
(checkpointFieldWithStreamOffset head offset)
tailFields)
payloadBytes
(succ tailCount)))
(branch
CheckpointPlacementRejected
ordinal
count
.
(constructor
CheckpointPlacementResult
CheckpointPlacementRejected
(succ ordinal)
count))))
(branch
CheckpointWord64Failed
code
.
(constructor CheckpointPlacementResult CheckpointPlacementRejected zero zero)))))))))
def checkpointPolicyName =
(lambda unrestricted policy : (family CheckpointLearnerStatePolicy) .
(eliminate
CheckpointLearnerStatePolicy
(lambda unrestricted current : (family CheckpointLearnerStatePolicy) . Bytes)
policy
(branch CheckpointStatelessPolicy . b"stateless")
(branch
CheckpointAdamWPolicy
.
b"adamw-f32-moments")))
def checkpointFieldKindName =
(lambda unrestricted kind : (family CheckpointFieldKind) .
(eliminate
CheckpointFieldKind
(lambda unrestricted current : (family CheckpointFieldKind) . Bytes)
kind
(branch
CheckpointParameterField
role
.
(eliminate
CheckpointParameterRole
(lambda unrestricted current : (family CheckpointParameterRole) . Bytes)
role
(branch
CheckpointTrainableParameter
.
b"parameter-trainable")
(branch
CheckpointFrozenParameter
.
b"parameter-frozen")
(branch
CheckpointPersistentState
.
b"persistent-state")))
(branch
CheckpointAdamWFirstMoment
.
b"adamw-first-moment")
(branch
CheckpointAdamWSecondMoment
.
b"adamw-second-moment")))
def checkpointCanonicalField =
(lambda unrestricted field : (family CheckpointField) .
(eliminate
CheckpointField
(lambda unrestricted current : (family CheckpointField) . (family CheckpointBytesResult))
field
(branch
CheckpointFieldValue
kind
name
storageOffset
streamOffset
byteLength
elements
domain
initialization
.
(checkpointBytesResultAppend
(checkpointSizedField (checkpointFieldKindName kind))
(checkpointBytesResultAppend
(checkpointSizedField name)
(checkpointBytesResultAppend
(checkpointIntegerField storageOffset)
(checkpointBytesResultAppend
(checkpointIntegerField streamOffset)
(checkpointBytesResultAppend
(checkpointIntegerField byteLength)
(checkpointBytesResultAppend
(checkpointIntegerField elements)
(checkpointBytesResultAppend
(checkpointSizedField domain)
(checkpointSizedField initialization)))))))))))
def checkpointCanonicalFields =
(lambda unrestricted fields : (family CheckpointFields) .
(eliminate
CheckpointFields
(lambda unrestricted current : (family CheckpointFields) . (family CheckpointBytesResult))
fields
(branch
CheckpointFieldsEnd
.
(constructor CheckpointBytesResult CheckpointBytesSucceeded b""))
(branch
CheckpointFieldsNext
head
tail
ih_tail
.
(checkpointBytesResultAppend (checkpointCanonicalField head) ih_tail))))
-- The schema version the canonical material carries and this build supports.
-- A checkpoint whose schema declares another version is refused with both
-- versions named, rather than surfacing as an opaque digest mismatch (CKP-006).
def checkpointSchemaVersion : Bytes =
b"alpha-checkpoint-schema-v1"
def checkpointValidateSchemaVersion =
(lambda unrestricted declared : Bytes .
(nat-eliminate
(lambda unrestricted matched : Nat . (family CheckpointSchemaIdentityResult))
(constructor
CheckpointSchemaIdentityResult
CheckpointSchemaIdentityRejected
(checkpointFailure
(constructor CheckpointErrorCode CheckpointSchemaVersionUnsupported)
zero
checkpointSchemaVersion
declared)
(bytes-length declared))
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : (family CheckpointSchemaIdentityResult) .
(constructor
CheckpointSchemaIdentityResult
CheckpointSchemaIdentityAccepted
(bytes-length declared))))
(bytes-equal declared checkpointSchemaVersion)))
def checkpointCanonicalSchema =
(lambda unrestricted policy : (family CheckpointLearnerStatePolicy) .
(lambda unrestricted parameterCount : (family ModelWord64) .
(lambda unrestricted payloadBytes : (family ModelWord64) .
(lambda unrestricted fields : (family CheckpointFields) .
(eliminate
CheckpointWord64Result
(lambda unrestricted current : (family CheckpointWord64Result) .
(family CheckpointBytesResult))
(checkpointNaturalWord64
(constructor CheckpointErrorCode CheckpointFieldCountOverflow)
(checkpointFieldsCount fields))
(branch
CheckpointWord64Succeeded
fieldCount
.
(checkpointBytesResultAppend
(checkpointBytesSuccess checkpointSchemaVersion)
(checkpointBytesResultAppend
(checkpointIntegerField parameterCount)
(checkpointBytesResultAppend
(checkpointIntegerField payloadBytes)
(checkpointBytesResultAppend
(checkpointSizedField (checkpointPolicyName policy))
(checkpointBytesResultAppend
(checkpointIntegerField fieldCount)
(checkpointCanonicalFields fields)))))))
(branch
CheckpointWord64Failed
code
.
(constructor CheckpointBytesResult CheckpointBytesFailed code)))))))
def checkpointSchemaTelemetryAt =
(lambda unrestricted storageCount : Nat .
(lambda unrestricted parameterFields : Nat .
(lambda unrestricted learnerFields : Nat .
(lambda unrestricted placedFields : Nat .
(lambda unrestricted canonicalBytes : Nat .
(lambda unrestricted digestTelemetry : (family SHA256DigestTelemetry) .
(checkpointSchemaTelemetry
storageCount
parameterFields
learnerFields
placedFields
canonicalBytes
digestTelemetry)))))))
def checkpointDeriveSchema =
(lambda unrestricted program : (family CheckpointProgram) .
(eliminate
CheckpointProgram
(lambda unrestricted current : (family CheckpointProgram) . (family CheckpointSchemaResult))
program
(branch
CheckpointProgramValue
storages
learner
.
(eliminate
CheckpointLearnerComponent
(lambda unrestricted current : (family CheckpointLearnerComponent) .
(family CheckpointSchemaResult))
learner
(branch
CheckpointLearnerComponentValue
policy
.
(app
(lambda unrestricted storageCount : Nat .
(eliminate
CheckpointExtentResult
(lambda unrestricted current : (family CheckpointExtentResult) .
(family CheckpointSchemaResult))
(checkpointStorageFieldsEnd storages)
(branch
CheckpointExtentAccepted
storageEnd
.
(eliminate
CheckpointParameterCountResult
(lambda unrestricted current : (family CheckpointParameterCountResult) .
(family CheckpointSchemaResult))
(checkpointParameterCount storages)
(branch
CheckpointParameterCountAccepted
parameterCount
.
(eliminate
CheckpointLearnerFieldsResult
(lambda unrestricted current : (family CheckpointLearnerFieldsResult) .
(family CheckpointSchemaResult))
(checkpointDeriveLearnerFields policy storages storageEnd)
(branch
CheckpointLearnerFieldsAccepted
learnerFields
learnerEnd
learnerCount
.
(app
(lambda unrestricted allFields : (family CheckpointFields) .
(eliminate
CheckpointPlacementResult
(lambda unrestricted current : (family CheckpointPlacementResult) .
(family CheckpointSchemaResult))
(checkpointPlaceStreamFields allFields modelWord64Zero)
(branch
CheckpointPlacementAccepted
placedFields
payloadBytes
placedCount
.
(eliminate
CheckpointBytesResult
(lambda unrestricted current : (family CheckpointBytesResult) .
(family CheckpointSchemaResult))
(checkpointCanonicalSchema
policy
parameterCount
payloadBytes
placedFields)
(branch
CheckpointBytesSucceeded
material
.
(eliminate
SHA256HexResult
(lambda unrestricted current : (family SHA256HexResult) .
(family CheckpointSchemaResult))
(sha256Hex material)
(branch
SHA256HexSucceeded
digest
digestTelemetry
.
(nat-eliminate
(lambda unrestricted validDigest : Nat .
(family CheckpointSchemaResult))
(constructor
CheckpointSchemaResult
CheckpointSchemaRejected
(checkpointSimpleFailure
(constructor
CheckpointErrorCode
CheckpointSchemaDigestLengthInvalid)
zero)
(checkpointSchemaTelemetryAt
storageCount
storageCount
learnerCount
placedCount
(bytes-length material)
digestTelemetry))
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : (family CheckpointSchemaResult) .
(constructor
CheckpointSchemaResult
CheckpointSchemaDerived
(constructor
CheckpointSchema
CheckpointSchemaValue
policy
digest
placedFields
parameterCount
payloadBytes)
(checkpointSchemaTelemetryAt
storageCount
storageCount
learnerCount
placedCount
(bytes-length material)
digestTelemetry))))
(naturalEqual (bytes-length digest) (byte-to-nat (byte 64)))))
(branch
SHA256HexFailed
error
ordinal
digestTelemetry
.
(constructor
CheckpointSchemaResult
CheckpointSchemaRejected
(checkpointSimpleFailure
(constructor
CheckpointErrorCode
CheckpointSchemaDigestFailed)
ordinal)
(checkpointSchemaTelemetryAt
storageCount
storageCount
learnerCount
placedCount
(bytes-length material)
digestTelemetry)))))
(branch
CheckpointBytesFailed
code
.
(constructor
CheckpointSchemaResult
CheckpointSchemaRejected
(checkpointSimpleFailure code zero)
(checkpointSchemaTelemetryAt
storageCount
storageCount
learnerCount
placedCount
zero
checkpointInitialDigestTelemetry)))))
(branch
CheckpointPlacementRejected
ordinal
placedCount
.
(constructor
CheckpointSchemaResult
CheckpointSchemaRejected
(checkpointSimpleFailure
(constructor
CheckpointErrorCode
CheckpointStreamExtentOverflow)
ordinal)
(checkpointSchemaTelemetryAt
storageCount
storageCount
learnerCount
placedCount
zero
checkpointInitialDigestTelemetry)))))
(checkpointFieldsAppend
(checkpointParameterFields storages)
learnerFields)))
(branch
CheckpointLearnerFieldsRejected
code
ordinal
learnerCount
.
(constructor
CheckpointSchemaResult
CheckpointSchemaRejected
(checkpointSimpleFailure code ordinal)
(checkpointSchemaTelemetryAt
storageCount
storageCount
learnerCount
zero
zero
checkpointInitialDigestTelemetry)))))
(branch
CheckpointParameterCountRejected
ordinal
.
(constructor
CheckpointSchemaResult
CheckpointSchemaRejected
(checkpointSimpleFailure
(constructor CheckpointErrorCode CheckpointParameterCountOverflow)
ordinal)
(checkpointSchemaTelemetryAt
storageCount
storageCount
zero
zero
zero
checkpointInitialDigestTelemetry)))))
(branch
CheckpointExtentRejected
code
ordinal
.
(constructor
CheckpointSchemaResult
CheckpointSchemaRejected
(checkpointSimpleFailure code ordinal)
(checkpointSchemaTelemetryAt
storageCount
zero
zero
zero
zero
checkpointInitialDigestTelemetry)))))
(checkpointParameterStorageCount storages)))))))
def checkpointValidateSchemaIdentity =
(lambda unrestricted schema : (family CheckpointSchema) .
(eliminate
CheckpointSchema
(lambda unrestricted current : (family CheckpointSchema) .
(family CheckpointSchemaIdentityResult))
schema
(branch
CheckpointSchemaValue
policy
digest
fields
parameterCount
payloadBytes
.
(eliminate
CheckpointBytesResult
(lambda unrestricted current : (family CheckpointBytesResult) .
(family CheckpointSchemaIdentityResult))
(checkpointCanonicalSchema policy parameterCount payloadBytes fields)
(branch
CheckpointBytesSucceeded
material
.
(eliminate
SHA256HexResult
(lambda unrestricted current : (family SHA256HexResult) .
(family CheckpointSchemaIdentityResult))
(sha256Hex material)
(branch
SHA256HexSucceeded
computed
telemetry
.
(nat-eliminate
(lambda unrestricted validLength : Nat . (family CheckpointSchemaIdentityResult))
(constructor
CheckpointSchemaIdentityResult
CheckpointSchemaIdentityRejected
(checkpointSimpleFailure
(constructor CheckpointErrorCode CheckpointSchemaDigestLengthInvalid)
zero)
(bytes-length material))
(lambda unrestricted lengthPredecessor : Nat .
(lambda unrestricted lengthInduction : (family CheckpointSchemaIdentityResult) .
(nat-eliminate
(lambda unrestricted matched : Nat .
(family CheckpointSchemaIdentityResult))
(constructor
CheckpointSchemaIdentityResult
CheckpointSchemaIdentityRejected
(checkpointFailure
(constructor CheckpointErrorCode CheckpointSchemaIdentityMismatch)
zero
computed
digest)
(bytes-length material))
(lambda unrestricted matchPredecessor : Nat .
(lambda unrestricted matchInduction : (family CheckpointSchemaIdentityResult) .
(constructor
CheckpointSchemaIdentityResult
CheckpointSchemaIdentityAccepted
(bytes-length material))))
(bytes-equal computed digest))))
(naturalEqual (bytes-length computed) (byte-to-nat (byte 64)))))
(branch
SHA256HexFailed
error
ordinal
telemetry
.
(constructor
CheckpointSchemaIdentityResult
CheckpointSchemaIdentityRejected
(checkpointSimpleFailure
(constructor CheckpointErrorCode CheckpointSchemaDigestFailed)
ordinal)
(bytes-length material)))))
(branch
CheckpointBytesFailed
code
.
(constructor
CheckpointSchemaIdentityResult
CheckpointSchemaIdentityRejected
(checkpointSimpleFailure code zero)
zero))))))
def checkpointValidateBlocks =
(lambda unrestricted fields : (family CheckpointFields) .
(eliminate
CheckpointFields
(lambda unrestricted current : (family CheckpointFields) .
(pi unrestricted blocks : (family CheckpointBlocks) .
(family CheckpointBlocksValidationResult)))
fields
(branch
CheckpointFieldsEnd
.
(lambda unrestricted blocks : (family CheckpointBlocks) .
(eliminate
CheckpointBlocks
(lambda unrestricted current : (family CheckpointBlocks) .
(family CheckpointBlocksValidationResult))
blocks
(branch
CheckpointBlocksEnd
.
(constructor
CheckpointBlocksValidationResult
CheckpointBlocksAccepted
(constructor CheckpointTypedBlocks CheckpointTypedBlocksEnd)
modelWord64Zero
zero))
(branch
CheckpointBlocksNext
head
tail
ih_tail
.
(constructor
CheckpointBlocksValidationResult
CheckpointBlocksRejected
(checkpointSimpleFailure
(constructor CheckpointErrorCode CheckpointFieldCountMismatch)
zero)
modelWord64Zero
zero)))))
(branch
CheckpointFieldsNext
field
remainingFields
ih_fields
.
(lambda unrestricted blocks : (family CheckpointBlocks) .
(eliminate
CheckpointBlocks
(lambda unrestricted current : (family CheckpointBlocks) .
(family CheckpointBlocksValidationResult))
blocks
(branch
CheckpointBlocksEnd
.
(constructor
CheckpointBlocksValidationResult
CheckpointBlocksRejected
(checkpointSimpleFailure
(constructor CheckpointErrorCode CheckpointFieldCountMismatch)
zero)
modelWord64Zero
zero))
(branch
CheckpointBlocksNext
block
remainingBlocks
ih_blocks
.
(eliminate
CheckpointField
(lambda unrestricted current : (family CheckpointField) .
(family CheckpointBlocksValidationResult))
field
(branch
CheckpointFieldValue
kind
expectedName
storageOffset
streamOffset
expectedLength
elements
domain
initialization
.
(eliminate
CheckpointBlock
(lambda unrestricted current : (family CheckpointBlock) .
(family CheckpointBlocksValidationResult))
block
(branch
CheckpointBlockValue
actualName
payload
.
(nat-eliminate
(lambda unrestricted nameMatched : Nat .
(family CheckpointBlocksValidationResult))
(constructor
CheckpointBlocksValidationResult
CheckpointBlocksRejected
(checkpointFailure
(constructor CheckpointErrorCode CheckpointFieldNameMismatch)
zero
expectedName
actualName)
modelWord64Zero
zero)
(lambda unrestricted namePredecessor : Nat .
(lambda unrestricted nameInduction : (family CheckpointBlocksValidationResult) .
(eliminate
CheckpointWord64Result
(lambda unrestricted current : (family CheckpointWord64Result) .
(family CheckpointBlocksValidationResult))
(checkpointNaturalWord64
(constructor CheckpointErrorCode CheckpointPayloadLengthOverflow)
(bytes-length payload))
(branch
CheckpointWord64Succeeded
actualLength
.
(nat-eliminate
(lambda unrestricted lengthMatched : Nat .
(family CheckpointBlocksValidationResult))
(constructor
CheckpointBlocksValidationResult
CheckpointBlocksRejected
(checkpointFailure
(constructor
CheckpointErrorCode
CheckpointPayloadLengthMismatch)
zero
(dataBytesWord64LE expectedLength)
(dataBytesWord64LE actualLength))
modelWord64Zero
zero)
(lambda unrestricted lengthPredecessor : Nat .
(lambda unrestricted lengthInduction : (family CheckpointBlocksValidationResult) .
(eliminate
CheckpointBlocksValidationResult
(lambda unrestricted current : (family CheckpointBlocksValidationResult) .
(family CheckpointBlocksValidationResult))
(ih_fields remainingBlocks)
(branch
CheckpointBlocksAccepted
typedTail
tailPayload
tailCount
.
(eliminate
CheckpointWord64Result
(lambda unrestricted current : (family CheckpointWord64Result) .
(family CheckpointBlocksValidationResult))
(checkpointAddChecked
(constructor
CheckpointErrorCode
CheckpointPayloadExtentOverflow)
actualLength
tailPayload)
(branch
CheckpointWord64Succeeded
total
.
(constructor
CheckpointBlocksValidationResult
CheckpointBlocksAccepted
(constructor
CheckpointTypedBlocks
CheckpointTypedBlocksNext
(constructor
CheckpointTypedBlock
CheckpointTypedBlockValue
kind
expectedName
storageOffset
streamOffset
elements
payload)
typedTail)
total
(succ tailCount)))
(branch
CheckpointWord64Failed
code
.
(constructor
CheckpointBlocksValidationResult
CheckpointBlocksRejected
(checkpointSimpleFailure code zero)
tailPayload
tailCount))))
(branch
CheckpointBlocksRejected
failure
payloadBytes
count
.
(eliminate
CheckpointFailure
(lambda unrestricted current : (family CheckpointFailure) .
(family CheckpointBlocksValidationResult))
failure
(branch
CheckpointFailureValue
code
ordinal
expected
actual
.
(constructor
CheckpointBlocksValidationResult
CheckpointBlocksRejected
(checkpointFailure code (succ ordinal) expected actual)
payloadBytes
count)))))))
(modelWord64Equal expectedLength actualLength)))
(branch
CheckpointWord64Failed
code
.
(constructor
CheckpointBlocksValidationResult
CheckpointBlocksRejected
(checkpointSimpleFailure code zero)
modelWord64Zero
zero)))))
(bytes-equal expectedName actualName))))))))))))
def checkpointLoad =
(lambda unrestricted schema : (family CheckpointSchema) .
(lambda unrestricted image : (family CheckpointImage) .
(eliminate
CheckpointSchemaIdentityResult
(lambda unrestricted current : (family CheckpointSchemaIdentityResult) .
(family CheckpointLoadResult))
(checkpointValidateSchemaIdentity schema)
(branch
CheckpointSchemaIdentityAccepted
canonicalBytes
.
(eliminate
CheckpointSchema
(lambda unrestricted current : (family CheckpointSchema) .
(family CheckpointLoadResult))
schema
(branch
CheckpointSchemaValue
policy
expectedDigest
fields
parameterCount
expectedPayload
.
(eliminate
CheckpointImage
(lambda unrestricted current : (family CheckpointImage) .
(family CheckpointLoadResult))
image
(branch
CheckpointImageValue
actualDigest
blocks
.
(app
(lambda unrestricted expectedCount : Nat .
(app
(lambda unrestricted actualCount : Nat .
(nat-eliminate
(lambda unrestricted digestMatched : Nat .
(family CheckpointLoadResult))
(constructor
CheckpointLoadResult
CheckpointLoadRejected
(checkpointFailure
(constructor CheckpointErrorCode CheckpointSchemaIdentityMismatch)
zero
expectedDigest
actualDigest)
(checkpointValidationTelemetry
expectedCount
actualCount
zero
modelWord64Zero
canonicalBytes))
(lambda unrestricted digestPredecessor : Nat .
(lambda unrestricted digestInduction : (family CheckpointLoadResult) .
(nat-eliminate
(lambda unrestricted countMatched : Nat .
(family CheckpointLoadResult))
(constructor
CheckpointLoadResult
CheckpointLoadRejected
(checkpointSimpleFailure
(constructor CheckpointErrorCode CheckpointFieldCountMismatch)
zero)
(checkpointValidationTelemetry
expectedCount
actualCount
zero
modelWord64Zero
canonicalBytes))
(lambda unrestricted countPredecessor : Nat .
(lambda unrestricted countInduction : (family CheckpointLoadResult) .
(eliminate
CheckpointBlocksValidationResult
(lambda unrestricted current : (family CheckpointBlocksValidationResult) .
(family CheckpointLoadResult))
(checkpointValidateBlocks fields blocks)
(branch
CheckpointBlocksAccepted
typedBlocks
actualPayload
validatedCount
.
(nat-eliminate
(lambda unrestricted payloadMatched : Nat .
(family CheckpointLoadResult))
(constructor
CheckpointLoadResult
CheckpointLoadRejected
(checkpointFailure
(constructor
CheckpointErrorCode
CheckpointPayloadExtentMismatch)
zero
(dataBytesWord64LE expectedPayload)
(dataBytesWord64LE actualPayload))
(checkpointValidationTelemetry
expectedCount
actualCount
validatedCount
actualPayload
canonicalBytes))
(lambda unrestricted payloadPredecessor : Nat .
(lambda unrestricted payloadInduction : (family CheckpointLoadResult) .
(constructor
CheckpointLoadResult
CheckpointLoaded
(constructor
CheckpointTypedCheckpoint
CheckpointTypedCheckpointValue
policy
image
typedBlocks)
(checkpointValidationTelemetry
expectedCount
actualCount
validatedCount
actualPayload
canonicalBytes))))
(modelWord64Equal expectedPayload actualPayload)))
(branch
CheckpointBlocksRejected
failure
payloadBytes
validatedCount
.
(constructor
CheckpointLoadResult
CheckpointLoadRejected
failure
(checkpointValidationTelemetry
expectedCount
actualCount
validatedCount
payloadBytes
canonicalBytes))))))
(naturalEqual expectedCount actualCount))))
(bytes-equal expectedDigest actualDigest)))
(checkpointBlocksCount blocks)))
(checkpointFieldsCount fields)))))))
(branch
CheckpointSchemaIdentityRejected
failure
canonicalBytes
.
(constructor
CheckpointLoadResult
CheckpointLoadRejected
failure
(checkpointValidationTelemetry zero zero zero modelWord64Zero canonicalBytes))))))
def checkpointSeal =
(lambda unrestricted schema : (family CheckpointSchema) .
(lambda unrestricted blocks : (family CheckpointBlocks) .
(eliminate
CheckpointSchema
(lambda unrestricted current : (family CheckpointSchema) . (family CheckpointLoadResult))
schema
(branch
CheckpointSchemaValue
policy
digest
fields
parameterCount
payloadBytes
.
(checkpointLoad schema (constructor CheckpointImage CheckpointImageValue digest blocks))))))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.