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))))))