Expand description
The logical checkpoint and its bounded tail (spec §12).
A checkpoint is not a snapshot of the kernel’s internals. It is a stable, versioned DTO whose shape is a contract in its own right, and every design rule below corrects the retired full-journal recovery format:
- Nothing here is derived from a private layout.
LogicalKernelStateis built by an explicit projection —LogicalStateProjectionfrom the semantic driver, the transition partition from the transaction — so a field added toLoopStateMachinecannot silently change the checkpoint format, and a field this DTO needs cannot silently disappear. The old snapshot serialised the whole last planned step, rendered context and all, which made the blob a function of the rendered prompt rather than of the state. - Every piece of correctness state has exactly one home. The four partitions of §12.1 —
transition / syscall / scheduler / context_vm — partition the state, they do not overlap it:
pending effects, the input replay ledger and the terminal live in
transition, task attempts inscheduler, P3 handles incontext_vm, and the checkpoint header repeats none of them.single_ownership_is_structuralproves it by scanning the serialised document. - The bounded tail is exact.
tail_inputscovers(base_step_seq, through_step_seq]with no hole, no duplicate and nothing outside the range — checked at construction, so a checkpoint that would replay a different history than the journal did is not constructible. - Three digests, three questions.
state_digestanswers “is this the logical state that was captured”,tail_digestanswers “is this the tail that was captured”, andcheckpoint_digestanswers “is this the whole checkpoint, header included”. They all use the record layer’s canonical bytes, so a host validator that already implements §7.1.1 for records needs no second serialiser.
What this module deliberately does not do: install, restore, rebase or ack. §12.3’s second
half is Task 16. What exists here is generation — [KernelTransaction::checkpoint_candidate]
and the shapes it produces — plus the verification a restore will call into.
Structs§
- Accepted
Cancellation State - Accepted
Input State - One entry of the replay ledger (§12.3 rules 7 and 10).
- Authored
Memory Query State - Authored
Memory Write State - Canonical
Input - One accepted input inside a checkpoint’s bounded tail.
- Checkpoint
AckToken - Handle the host returns to
ack_checkpointonce the blob is durably installed (§12.3). - Checkpoint
Candidate - §12.3 · what
kernel.checkpoint_candidate()hands the host. - Checkpoint
Draft - Everything
KernelCheckpoint::assembleneeds. A struct rather than eight positional arguments, because two of them are step sequences and two are digests. - Checkpoint
Revision - The checkpoint format revision, fail-closed on the wire.
- Child
Process State - Context
VmState V1 - §12.1 · the P3 plane: the handle table and its allocator, skills and their leases, the knowledge slots, the signal partition and the compaction/renewal clocks.
- Entropy
State - Entropy
Turn State - Handle
State - One P3 handle.
residencyis the label plus the locator fields that residency carries, so the DTO neither mirrors the internal enum’s shape nor loses what a page-in needs. - Inline
Message Body - Kernel
Checkpoint - One logical checkpoint (§12.1).
- Knowledge
Slot State - One knowledge slot, body included.
- Launch
Token State - Logical
Compression Entry - Logical
Kernel State - The versioned logical state of one operation, partitioned as §12.1 requires.
- Logical
Plan Step - Logical
State Projection - What the semantic driver contributes to a checkpoint.
- Logical
Task State - §12.1 · the durable task board, projected.
- Logical
Tool Call - Milestone
State - Partition
Token State - Pending
Payload Load State - Pending
Provider Call State - Queued
Signal State - Referenced
Message Body - Resolved
Effect State - Scheduler
State V1 - §12.1 · the P2 plane: task control blocks and their attempts, budgets and waits, the workflow graph, queued signals plus dedupe memory, and the milestone cascade.
- Skill
Lease State - Stored
Message State - One stored message, projected (§12.1, adjudication §5q-2).
- Structured
Message Body - Syscall
State V1 - §12.1 · governance revision, the live policy, the rate-limit window, and the provider-tool causation the P1 gate derives a caller from.
- Task
Attempt State - Task
Control State - One task control block, projected. The lifecycle travels as its label rather than as the
internal enum:
TaskLifecycle::Done(TerminationReason)is a semantic-kernel shape, and a checkpoint that mirrored it would be a checkpoint of a private layout. - Transition
State V1 - §12.1 · operation lifecycle, execution focus, the effect ledger, input replay, cancellation and the terminal.
- Workflow
Graph State - Workflow
Node State - One workflow node as source state rather than a snapshot of
TaskGraphinternals.
Enums§
- Checkpoint
Error - Why a checkpoint could not be assembled, decoded or verified.
- Message
Partition - Which partition a
StoredMessageStatebelongs to. - Stored
Message Body - A message body, inline or by reference (§7.10).
Constants§
- CHECKPOINT_
ERROR_ MARKER - Prefix of every checkpoint-layer rejection, so all four hosts classify on one marker.