5e61c50728
take_events kept returning Option<EventBatchView> and defaulting through the question-mark operator, so a batch missing a field read as end of stream and the ConsumerEvents enum added in the previous round described nothing. It returns Batch or Unreadable now, and a test publishes a batch with no droppedBefore, asserts it is reported as unreadable naming the field, and asserts the next real batch still reads. The checkpoint-envelope-v1 amendment cites the rule that lets a required manifest field land with envelopeVersion still 1 while no production file exists.
216 lines
12 KiB
Markdown
216 lines
12 KiB
Markdown
# Checkpoint envelope v1: `FLYSESS1`
|
|
|
|
Status: **draft 1**, 2026-09-22. Specified by CONTRACT-01 of the
|
|
[implementation guide](implementation.md); required by
|
|
[session artifacts, native media and recovery](state-media-v1.md) section 4, which says to
|
|
"use a new envelope version; specify exact byte layout before production files". Reference
|
|
implementations of the layout: `services/flysim/crates/fly-session-types/src/checkpoint.rs`
|
|
and `packages/session-types/src/checkpoint.ts`; fixture:
|
|
`.../fly-session-types/fixtures/checkpoint-envelope.json`.
|
|
|
|
This is the byte layout and the durable commit sequence. The store itself, generations,
|
|
rotation, the writer thread and the capture RPC flow are the STATE-01 slice.
|
|
|
|
## 1. Why a new format
|
|
|
|
The historical envelope (`FLYSIM01`, `crates/flybrain-core/src/envelope.rs`) is a magic, a
|
|
`u32` manifest length, a JSON manifest, `u32`-prefixed chunks in manifest order and a CRC32
|
|
footer, with chunk names restricted to ASCII letters so the TypeScript reader can never name a
|
|
prototype key. It stays exactly as it is, and its reader stays separately readable: nothing in
|
|
this document changes a byte of it, and a `FLYSIM01` file is refused by a `FLYSESS1` reader at
|
|
the magic.
|
|
|
|
A coherent all-participant session checkpoint needs what that format does not have:
|
|
|
|
- payload names that are `Id`s (`agent-fly-a`, `executor-fly-a`), so the letters-only
|
|
constraint is widened **deliberately, in a new version**, rather than quietly;
|
|
- a per-payload content digest, because state-media-v1 section 1 makes digests mandatory on
|
|
checkpoint payloads and a group install must be able to fail one participant's bytes;
|
|
- a payload table with explicit offsets and lengths, so a reader can map one participant's
|
|
payload without walking every preceding chunk;
|
|
- SHA-256 over the whole prefix instead of CRC32, matching the `Digest` type these contracts
|
|
already use everywhere else.
|
|
|
|
## 2. Byte layout
|
|
|
|
All integers are unsigned little-endian. All digests are raw 32-byte SHA-256 (the manifest
|
|
records the same digests as lowercase hex `Digest` strings).
|
|
|
|
### Header, 32 bytes
|
|
|
|
| Offset | Size | Field |
|
|
| ---: | ---: | --- |
|
|
| 0 | 8 | Magic, ASCII `FLYSESS1` |
|
|
| 8 | 4 | `envelopeVersion`, `1` |
|
|
| 12 | 4 | `headerBytes`, `32` |
|
|
| 16 | 4 | `manifestBytes` |
|
|
| 20 | 4 | `payloadCount`, at most 64 |
|
|
| 24 | 4 | `tableOffset` |
|
|
| 28 | 4 | Reserved, must be zero |
|
|
|
|
### Manifest
|
|
|
|
`manifestBytes` bytes of canonical JSON (RFC 8785) at offset 32, no trailing newline. It is
|
|
canonical so the envelope's own digest is stable under reserialization, and a reader rejects a
|
|
manifest that is not already canonical rather than silently accepting a second spelling.
|
|
|
|
### Payload table
|
|
|
|
At `tableOffset`, which is `32 + manifestBytes` rounded up to a multiple of 8.
|
|
`payloadCount` entries of 112 bytes each, in write order:
|
|
|
|
| Offset in entry | Size | Field |
|
|
| ---: | ---: | --- |
|
|
| 0 | 64 | Name: an `Id` in ASCII, NUL-padded, no bytes after the terminator |
|
|
| 64 | 8 | `offset` |
|
|
| 72 | 8 | `byteLength` |
|
|
| 80 | 32 | SHA-256 of exactly `byteLength` bytes at `offset` |
|
|
|
|
### Payloads
|
|
|
|
Each payload starts at its declared offset. The first starts at the end of the table rounded
|
|
up to a multiple of 8; each subsequent one starts at the previous payload's end rounded up the
|
|
same way. Padding bytes are zero. Offsets are ascending and non-overlapping, which a reader
|
|
checks rather than assumes.
|
|
|
|
### Footer, 48 bytes
|
|
|
|
| Offset from end | Size | Field |
|
|
| ---: | ---: | --- |
|
|
| 48 | 8 | `fileBytes`, the total length including the footer |
|
|
| 40 | 32 | SHA-256 of every byte before the footer |
|
|
| 8 | 8 | Magic, ASCII `FLYSESSF` |
|
|
|
|
A truncated file therefore fails at the footer magic or the recorded length, not at an
|
|
arbitrary payload.
|
|
|
|
## 3. Manifest fields
|
|
|
|
State-media-v1 section 4 lists what the manifest records. The names below are the JSON field
|
|
names; a manifest missing any of them is not a complete checkpoint.
|
|
|
|
| Field | Contents |
|
|
| --- | --- |
|
|
| `envelopeVersion` | `1` |
|
|
| `checkpointId` | `Id`, the identity every participant's capture shares |
|
|
| `sourceScope` | `Scope`: session, epoch and the committed step |
|
|
| `episodeId` | `Id` |
|
|
| `worldTime` | `RationalNs`, the environment's logical time at that boundary |
|
|
| `schedulerId` | The coordinator's scheduler identity, `lockstep-v1` in v1 |
|
|
| `compositionDigest` | Coordinator scheduler and configuration identity |
|
|
| `portMap` | The exact port-to-agent map, `[{portId, agentId}]` |
|
|
| `compatibility` | Backend, content, patch, controller, parser and state-format identities |
|
|
| `agents` | Per agent: profile, dataset, **index** and model identities, resolved seed, tick count, remainder and the payload name holding its state |
|
|
| `coordinator` | Task ledger, prior world inspection, per-agent executor state, admission state and event watermarks, each as a payload name or an inline value |
|
|
| `helperState` | External-helper state required for exact resume, as payload names |
|
|
| `payloads` | `[{name, byteLength, digest}]`, mirroring the payload table |
|
|
|
|
**Amendment, 2026-09-22 (PUBLISH-01).** The `agents` row gains `indexDigest`, the index the
|
|
agent attested to at `Agent.Initialize`, and it joins that agent's compatibility identity.
|
|
Without it a replacement fly that built another graph -- the same dataset, the same neuron
|
|
count, another index -- passed the group check and was then published under its predecessor's
|
|
`indexDigest`, which is a graph identity crossing a recovery and exactly what section 5's rules
|
|
exist to prevent. It is recorded from the worker's attestation rather than recomputed from the
|
|
dataset, because the point is that the two can disagree. `envelopeVersion` stays `1`, which the
|
|
required-manifest-field rule below allows only while no production `FLYSESS1` file exists; once
|
|
one does, adding a required manifest field must bump it.
|
|
|
|
**Amendment, 2026-09-22 (STATE-01).** The table above names a holder for every payload except
|
|
the environment's own, although section 6's fixture has one (`world`) and a group install has
|
|
to map it by name like any other participant's. The manifest therefore also records:
|
|
|
|
| Field | Contents |
|
|
| --- | --- |
|
|
| `environment` | `{workerId, payload}`: which worker the world belonged to and the payload name holding its state |
|
|
|
|
The reference implementations' required-field set was also missing `helperState`, which this
|
|
section has listed from the start. Both are now in `REQUIRED_MANIFEST_FIELDS` in Rust and in
|
|
TypeScript, and the fixture was regenerated by the existing example. The schema set is
|
|
untouched, so `contractDigest` is unchanged.
|
|
|
|
`coordinator.eventWatermarks` is `{lastSourceStep, issued}`. The fixture illustrated
|
|
`{lastEventId, lastOrdinal}`, and it is the illustration that changed: an event id is derived
|
|
from the epoch, so a watermark spelled as one cannot be compared across the restore that
|
|
gives the session a new epoch, while a source step and an issued count can.
|
|
|
|
**A required-manifest-field change is compatibility-relevant and `contractDigest` does not
|
|
cover it.** The digest is taken over the schema set, and this manifest is not in it, so
|
|
`envelopeVersion` is the only thing that can carry such a change. It stays `1` here only
|
|
because no production `FLYSESS1` file exists yet: once one does, adding or removing a required
|
|
manifest field **must** bump `envelopeVersion`, because a reader of the older version would
|
|
otherwise accept a file it cannot completely read, or refuse one it could.
|
|
|
|
`payloads` is redundant with the table on purpose: the table is what a reader needs to map
|
|
bytes, and the manifest is what a store lists, compares and reports without opening the
|
|
payload area. A reader checks that the two agree.
|
|
|
|
What the manifest must **not** contain (state-media-v1 section 4): a transient bus `storeId`,
|
|
artifact ID, owner token, mapping or pointer. Payload bytes and durable content identity are
|
|
the only things that survive; on restore the durable store imports fresh bus artifacts, and
|
|
`sourceScope` is provenance, not a claim on the current router.
|
|
|
|
## 4. What a reader enforces
|
|
|
|
In this order, so a corrupt file fails on its own terms rather than on a derived value:
|
|
|
|
1. Length at least header plus footer; magic; version; `headerBytes`; reserved word zero.
|
|
2. Footer magic, `fileBytes` equal to the actual length, and the prefix digest.
|
|
3. Manifest inside the payload area, valid strict JSON (duplicate keys, invalid UTF-8 and
|
|
non-finite numbers refused) and already canonical.
|
|
4. `tableOffset` exactly at the laid-out position; the table inside the payload area.
|
|
5. Per entry: an `Id` name with no bytes after its terminator, names unique, the declared
|
|
offset exactly at the aligned end of the previous payload, the payload inside the payload
|
|
area, and its digest matching its bytes.
|
|
6. No padding between the last payload and the footer.
|
|
7. The required manifest field set, `envelopeVersion` of 1, and a `payloads` list that matches
|
|
the table name for name, length for length and digest for digest.
|
|
|
|
Failing any of these is a corrupt or foreign file. The group install rule of state-media-v1
|
|
section 5 then applies: corrupt any participant and installation fails as a group.
|
|
|
|
## 5. Durable commit
|
|
|
|
State-media-v1 section 6, in the order the writer performs it:
|
|
|
|
1. Write the envelope to a temporary generation file in the store directory.
|
|
2. `fsync` the file.
|
|
3. `rename` it to its final generation name.
|
|
4. `fsync` the store directory.
|
|
5. Write the store manifest to its own temporary file, `fsync`, `rename`, `fsync` the
|
|
directory.
|
|
|
|
**The store manifest rename is the durable commit point.** Before it, the generation file is
|
|
an unreferenced temporary that is never a restore candidate. After it, and only after it, the
|
|
writer reports a saved acknowledgment and moves the high-water mark.
|
|
|
|
Consequences the writer must respect rather than reinterpret:
|
|
|
|
- Bus publications for `captured`, `queued`, `committed`, `failed` and `superseded` are
|
|
distinct events; only durable completion produces the saved acknowledgment.
|
|
- A lost save reply never advances durable metadata: the coordinator resolves the same
|
|
operation or fails the epoch, and an unreferenced generation stays unreferenced.
|
|
- A failed write releases its owned ephemeral captures under the configured retry policy and
|
|
reports the failure. It never reports false durability.
|
|
- The writer owns the bus artifact handles until the bytes are committed or the job fails, and
|
|
drops them afterwards; durable files are outside the bus's ephemeral collection.
|
|
- No per-payload `fsync` inside one envelope: the single file `fsync` in step 2 covers it.
|
|
|
|
## 6. Fixture
|
|
|
|
`fixtures/checkpoint-envelope.json` holds one complete envelope: the manifest, five payloads
|
|
(one agent, one executor, the task ledger, the prior inspection and a world payload), the
|
|
envelope's base64 bytes, its exact layout (header size, manifest offset and length, table
|
|
offset, every entry's offset, length and digest, footer offset, total length) and six
|
|
corruptions a reader must refuse, each naming the byte to flip.
|
|
|
|
The two implementations are held to it from both directions: each parses the fixture and
|
|
checks every recorded offset, and the TypeScript side re-encodes the same manifest and
|
|
payloads and requires the bytes to be identical to the fixture. A layout change that only one
|
|
language makes therefore fails on the next test run.
|
|
|
|
## 7. Out of scope
|
|
|
|
Generations, rotation, hot versus durable copies, the capture queue and its bounds, the
|
|
`State.Capture` / `State.StageRestore` / `State.ActivateRestore` flow, compatibility
|
|
comparison rules and group fencing. Those are STATE-01, over this layout. `FLYSIM01` and the
|
|
legacy composition keep their own format and their own reader, unchanged.
|