docs(session-framework): seed derivation v1 and the FLYSESS1 checkpoint envelope

Two specifications CONTRACT-01 owes the slices that cannot be built without them.

seed-derivation-v1: the versioned derivation of independent per-agent seeds from a recorded
master seed and stable agent ids, the exact hashed material, the lane rule that keeps a seed
away from zero (the pinned kernel RNG is an xorshift, whose state must not be zero), the
properties a composition may rely on, and the test vectors both languages reproduce.

checkpoint-envelope-v1: the exact byte layout of the new envelope per state-media-v1 section
4, with the header, canonical-JSON manifest, 112-byte payload table entries, eight-byte
aligned payloads and the digest footer; the manifest field set; what a reader enforces and in
what order; and the durable commit sequence of section 6, whose commit point is the store
manifest rename. FLYSIM01 is unchanged, refused at the magic, and stays separately readable.

Both are specifications with fixtures, not the store: generations, rotation, the capture
queue and the restore flow remain STATE-01.

docs/design/session-framework/README.md

@@ -34,6 +34,15 @@ retroactively to existing [public feed](../../feed-protocol.md),
 6. [Application/presentation boundary](publishing-v1.md) — snapshots, flexible data and effects.
 7. [Implementation guide](implementation.md) — sequenced build tasks and acceptance tests.
 
+Two derived specifications, written by CONTRACT-01 because the slices that need them cannot
+be built without them:
+
+- [Seed derivation v1](seed-derivation-v1.md) — independent per-agent seeds from one recorded
+  master seed and stable agent ids, with test vectors in both languages.
+- [Checkpoint envelope v1](checkpoint-envelope-v1.md) — the exact bytes of the new `FLYSESS1`
+  envelope and the durable commit sequence. `FLYSIM01` is unchanged and stays separately
+  readable.
+
 For context: [modular-session analysis](../malecns-modular-sessions.md) and
 [Melee audit](../melee-framework-audit.md). Each contract owns its named subject; step ordering
 wins over an informal diagram, and Flybus owns transport/resource rules. Resolve contradictions

docs/design/session-framework/checkpoint-envelope-v1.md

@@ -0,0 +1,181 @@
+# 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 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 |
+
+`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.

docs/design/session-framework/seed-derivation-v1.md

@@ -0,0 +1,101 @@
+# Seed derivation v1
+
+Status: **draft 1**, 2026-09-22. Specified by CONTRACT-01 of the
+[implementation guide](implementation.md), required by
+[worker interfaces](workers-v1.md) section 2 before the real-agent slice. Reference
+implementations: `services/flysim/crates/fly-session-types/src/seed.rs` and
+`packages/session-types/src/seed.ts`; test vectors:
+`services/flysim/crates/fly-session-types/fixtures/seed-vectors.json`.
+
+## 1. What this is for
+
+`Agent.Initialize` takes `seed`, a signed 32-bit integer, matching the current RNG input.
+Workers-v1 section 2 requires that the coordinator derive independent per-agent seeds from
+**its recorded master seed and stable agent IDs** under a versioned algorithm, and that the
+algorithm be specified and tested before the real agent slice. This is that algorithm.
+
+It is a reproducibility rule, not a secret: a run manifest records the master seed in the
+clear, and anyone with the manifest can recompute every agent's seed. It is not a key
+derivation function and must not be used as one.
+
+`seed-derivation-v1` is part of composition identity. Changing any byte of it requires a new
+identifier (`seed-derivation-v2`), because two runs that agree on every other identity but
+disagree here are not the same experiment.
+
+## 2. Inputs
+
+| Input | Type | Source |
+| --- | --- | --- |
+| `masterSeed` | `U64` decimal string | Recorded once per run by the application/supervisor |
+| `agentId` | `Id` | The configured agent identity, stable across restarts and epochs |
+
+Both are the ipc-v1 section 2 scalars. An `agentId` that is not an `Id` is an error, not
+something to normalize. The master seed is the whole 64-bit range: a 32-bit master seed would
+be no wider than the seed it derives.
+
+## 3. Derivation
+
+```text
+material = "flybrain/seed-derivation-v1" LF masterSeed LF agentId LF
+digest   = SHA-256(material)
+lanes    = digest read as eight big-endian uint32 values, in order
+seed     = the first nonzero lane, reinterpreted as a two's-complement int32
+```
+
+`LF` is one `0x0a` byte. `masterSeed` is its canonical decimal form: `"0"`, or no leading
+zero. The prefix is a domain separator, so a digest from this algorithm can never collide with
+one taken over some other pair of strings.
+
+Zero lanes are skipped because the pinned kernel's RNG is an xorshift generator, whose state
+must not be zero: a derivation that could hand out `0` would silently produce a stalled
+generator. If every one of the eight lanes were zero, the material is rehashed with a counter
+suffix (`material || "1" LF`, then `"2" LF`, then `"3" LF`) and the search repeats; no input
+has ever needed it, and four rounds exhausted is an error rather than a fallback seed.
+
+The seed is the *negative* number when the lane's high bit is set. That is deliberate: the
+existing RNG input is a signed 32-bit integer, and half the range is negative.
+
+## 4. Properties
+
+- **Deterministic.** The seed is a function of the two recorded inputs and nothing else: not
+  of wall time, agent order, port assignment, worker process or thread count.
+- **Independent per agent.** Distinct agent IDs give unrelated seeds; there is no arithmetic
+  relationship between `fly-a` and `fly-b` for a caller to exploit or accidentally rely on.
+- **Stable across recovery.** Restore, episode reset and a new epoch do not re-derive a
+  different seed for the same agent ID under the same master seed. The seed is persisted as run
+  configuration and state, and the capture compatibility digest covers the resolved seed
+  (workers-v1 section 2), so a checkpoint cannot be installed into a differently seeded
+  instance.
+- **Equal IDs give equal seeds.** That is the only way to get identical seeds, and workers-v1
+  allows identical seeds only when an experiment declares them. A composition therefore
+  refuses a repeated agent ID rather than quietly sharing a seed between two agents.
+
+Non-properties, stated so nobody assumes them: this is not uniform over the int32 range beyond
+what SHA-256 gives, it is not a stream (one seed per agent per run, not per step), and it says
+nothing about how a model consumes its seed.
+
+## 5. Test vectors
+
+`fixtures/seed-vectors.json` carries the full table: five master seeds (`0`, `1`, `42`, `2^63`
+and the `U64` maximum) across four agent IDs, each with the exact material string, its SHA-256
+and the derived seed, plus one four-agent composition and the inputs that must be refused.
+Both implementations reproduce every row, and each records the material as well as the seed so
+a third implementation can find where it diverges.
+
+The first two rows:
+
+| masterSeed | agentId | material | seed |
+| --- | --- | --- | ---: |
+| `0` | `fly-a` | `flybrain/seed-derivation-v1\n0\nfly-a\n` | 1828176714 |
+| `0` | `fly-b` | `flybrain/seed-derivation-v1\n0\nfly-b\n` | 1218785088 |
+
+Refused: an agent ID that is not an `Id` (uppercase, empty, over 64 characters), a master seed
+that is not a canonical `U64`, and a composition with a repeated agent ID.
+
+## 6. Out of scope
+
+Choosing the master seed, recording it in the run manifest, and the hand-selected explicit
+seeds that workers-v1 allows for the first synthetic composition. This document defines only
+the derivation. A profile that needs several independent streams inside one agent derives them
+from the agent's own seed under its own documented rule; that is a profile concern, not a
+session one.