Checkpoint.Envelope

THE CHECKPOINT ENVELOPE: what a native host writes around a system's raw training state, and refuses to resume from unless it holds. A checkpoint file is a header of `headerBytes` (a whole number of pages) and then the payload, unmodified (for Bob and Coppelius: the P/M/V planes). The header, little-endian: 0 magic "ALPHACKP" 8 version (1) 16 header bytes 24 payload bytes 32 chunk bytes 40 full chunks (payload bytes / chunk bytes) 48 tail bytes (payload bytes mod chunk bytes) 56 completed updates (the learner's step count) 64 completed invocations (the sampler's position: batches consumed) 72 SHA-256 of the state schema's identity (model, state layout) 104 SHA-256 of the learner's identity (optimizer, hyperparameters) 136 SHA-256 of the data contract's identity (tokenizer, batch format) 168 SHA-256 of the initialization's identity (the RNG seed) 200 the SHA-256 of each chunk of the payload, in order (the tail last) then zeros to `headerBytes`. The file is complete when its size is exactly header + payload bytes. A system states its contract (below); the first 56 bytes and the four identity digests of any checkpoint it resumes from must be the ones the contract gives, and every chunk must hash to its digest. The first failure is named (`CheckpointEnvelopeVerdict`): a short or long file is truncated, another version or layout is refused, another system's, learner's, data's or seed's state is foreign, and a chunk whose digest differs -- a swapped or corrupted file -- is refused by its index.

46field unrestricted checkpointEnvelopeChunkBytes : Nat