Skip to content

kernel.md

Latest commit

 

History

History
321 lines (272 loc) · 16.6 KB

kernel.md

File metadata and controls

321 lines (272 loc) · 16.6 KB
Raw

General kernel

This document maps the supervisory-control concepts to the current domain-neutral Go implementation.

Boatstack has one domain-neutral supervisory mechanism and one production domain: software delivery.

external Objective
        │ exact bind
        ▼
ControlState + Program + Domain Observation + Authority
        │
        ▼
canonical transition relation
        │
        ▼
Operator → Effect Facts → fresh observation → verification → receipt

The general mechanism is in boatstack/kernel. It has no Git, repository, branch, worktree, plan, coding-host, test, review, publication, or pull-request types. The software-delivery domain is in boatstack/delivery, boatstack/flow/standard, and boatstack/internal/softwaredelivery.

The dependency rule is:

kernel
  ↑
domain contracts
  ↑
software delivery

The general kernel never imports the software-delivery implementation.

Kernel-owned semantics

  • exact program identity and fingerprint;
  • control-instance identity and monotonic state revision;
  • external Objective and durable exact ObjectiveBinding;
  • objective scopes: none, optional-preserve, and bound-exact;
  • explicit objective lifecycle relations: preserve, bind-initial, advance, replace, and clear, each with its own capability and receipt-provable lineage;
  • explicit per-transition selection: a positive selection rank and a selection mode (implicit or explicit-only), alongside priority;
  • one transition relation used by resolve and apply;
  • state, program, objective, observation, and authority freshness;
  • trusted minimum-capability classification;
  • transition-owned effect facets;
  • operator-neutral execution and fresh postcondition verification;
  • program-defined marked modes;
  • explicit recovery state and recovery transitions;
  • domain-neutral committed receipts;
  • explicit instance provisioning and atomic instance records: current control state plus the complete ordered committed receipt history;
  • idempotent committed-result reconciliation by exact prescription identity.

Software-delivery-owned semantics

  • Git and repository identity;
  • repository policy and coding-host configuration;
  • plans, worktrees, builds, tests, reviews, and evidence;
  • delivery and publication state;
  • provider-authorized pull-request effects;
  • software-specific objective kinds and terminal contracts.

DeliveryController is the software-delivery facade. It retains the existing transactional repository implementation as a domain executor. It projects the compiled software Program ABI into one kernel Program, supplies admissible domain candidates, and delegates ordering, targeted/untargeted selection, marked-state recognition, ambiguity, and authority admission to kernel.Relate. It does not own a second selector.

The complete software manifest is hashed as the kernel Program's domain contract fingerprint. The resulting kernel Program fingerprint is the one identity used by software snapshots, prescriptions, admissions, and receipts. Changing either generic transition data or any software-domain contract makes prior prescriptions stale.

Objective law

An objective is external reference data. Supervisory state stores only an exact binding:

Objective        = id + revision + fingerprint + reference
ObjectiveBinding = objective id + revision + fingerprint

A command-scoped objective cannot reinterpret an existing binding. Changing intent creates a new objective revision. Prescriptions that bind an earlier revision become stale before any operator effect.

Maintenance transitions use optional-preserve: absent remains absent and a known binding remains byte-for-byte exact. Product progress uses bound-exact. Objective binding is an explicit, capability-gated transition.

The software domain retains its typed objective projection so it can evaluate delivery-specific terminal contracts. The kernel freshness envelope binds the exact status/value fingerprint of that projection. Refreshed evidence alone does not change the binding; any semantic objective change does.

Canonical relation

Resolve filters the program by mode, recovery state, objective law, the domain predicate, and authority. Apply reloads the state and observation under the instance lock, verifies prescription freshness, and calls the same relation. It cannot use a separate deterministic legality rule.

Every transition declares its selection behavior explicitly: a positive selection rank and a selection mode. Resolve copies both directly into the relation candidate, so an explicit-only transition stays admissible but is never chosen by untargeted resolution; it is prescribed only when a request names it exactly. Implicit candidates order by selection rank, then priority, then identity; equal preference returns a frontier; capability authority is compared only after selection filtering. Because rank and mode are part of the canonical program representation, changing either changes the program fingerprint and stales prior prescriptions before any effect.

The software-delivery projection maps its catalog selection classes onto these generic fields one-to-one — class rank to selection rank, implicit selectability to selection mode, priority to priority — without encoding one axis inside another and without placing software vocabulary in the kernel.

Software delivery uses the same relation through its domain adapter. Its advanced journal and reversible effect machinery remain domain-owned, while the prescription uses the same kernel.Freshness CAS identity as the generic runtime: state revision, Program fingerprint, snapshot fingerprint, objective binding fingerprint, and authority fingerprint.

Programs declare capabilities, but a trusted capability classifier supplies the minimum for each concrete operation. The operator receives only that admitted set. Effect facts must stay inside transition-owned facets.

The generic Store is one durability boundary. Create atomically provisions a new instance record and cannot overwrite an existing one. Load returns the atomic instance record: current control state plus the complete ordered committed receipt history. BeginEffect atomically persists the attempt state — including its recovery obligation — before any operator effect. CommitTransition atomically persists the target control state and its verified receipt; neither may become visible alone. If an operator may have changed domain state but verification or that atomic commit fails, the durable attempt state keeps recovery active against the unchanged pre-commit mode. Program compilation rejects any recovery mapping that cannot run from every source mode of the transition it recovers.

Trusted settlement

Candidate state and accepted state are distinct:

candidate: immutable external content, staged, inspectable, untrusted
accepted:  exact durable ObjectiveBinding + one committed receipt

A candidate becomes accepted state only through the full flow — exact candidate/objective reference, resolve and prescription, current-state revalidation, verification, then one atomic objective-binding-plus-receipt commit. Staging, resolving, model output, an attempted effect, or mutable domain state never constitute acceptance. Any failure before the final atomic commit leaves the prior accepted binding authoritative; rejected or orphaned candidates may persist but remain untrusted.

Each committed receipt records explicit objective lineage — the declared lifecycle relation plus the prior accepted binding, the requested candidate binding, and the resulting accepted binding — so a verifier can prove the exact accepted delta and its declared relation from the receipt alone. Preserve requires no requested binding and an unchanged result; bind-initial requires an absent prior; advance requires the same objective at exactly the next revision; replace requires a different objective identity; clear requires a prior binding and no result. The runtime never synthesizes an unrequested binding or infers a relation from program semantics.

Accepted-state readers reconstruct from durable evidence only: load the exact objective binding, resolve it to immutable candidate content, and require the matching committed receipt. Missing content, a fingerprint mismatch, or a missing or substituted receipt fails closed rather than inventing accepted content. Conformance detects dishonest store or reader implementations; the runtime does not claim to make adversarial ports safe.

Durable control instances

One store holds many durable control instances. The control law is stated over the persistence boundary itself, not over any one caller:

Every persistence operation — create, load, begin-effect, commit — and every lock acquisition names its exact control instance. State, revision compare-and-swap, recovery, locking, and committed receipt history are local to that one instance. A loaded record exposes the current control state and its complete ordered committed history atomically, and fails closed when that history cannot be trusted. Retrying an Apply whose exact prescription already committed returns the original durable receipt with no new observation, execution, verification, state mutation, receipt, or revision. A failed or interrupted attempt without a committed receipt is never reported as successful.

Provisioning is explicit: Runtime.Provision creates the valid initial control state for an instance atomically, concurrent creation yields exactly one initial history, a duplicate is a typed instance-exists result, and a missing instance is a typed not-found result. The kernel never silently manufactures accepted objective state.

Committed-result reconciliation uses the content-addressed prescription identity as the committed request identity. Before observing or executing anything, Apply searches the loaded history for exactly one valid receipt that settles the same prescription on the same instance, revalidates that receipt against the prescription's transition, lineage, revisions, observation, and authority fingerprints, and returns it unchanged. This is reconciliation of a proven historical commit — recovery of a lost successful response — not permission to replay an effect. A pending recovery obligation for the same prescription stays recovery-required.

Every loaded record is validated fail-closed before use: malformed or fabricated receipts, receipts routed from another instance, duplicate settlement of one prescription, rewound or reordered revisions, lineage that does not extend the committed chain, and control state behind its own history are all rejected. A persisted attempt without a final receipt and a state legitimately ahead of its history remain valid recovery shapes.

InstanceStoreConformance in boatstack/kernel/conformance proves the law for any Store: creation, restart, isolation, per-instance CAS and locking, atomic state-plus-receipt commits, append-only history, exact committed retry with zero side effects, failed-attempt retries staying recovery-required, cross-instance replay rejection, concurrent retries returning one durable result, corrupted-history fail-closure, and restart reconstruction. White-box counterexamples prove the suite rejects a singleton store that ignores the requested instance, torn state-receipt commits, a blind global compare-and-swap, latest-receipt rather than exact-prescription lookup, replaced or truncated history, and synthetic success after an unresolved attempt. The suite runs against the integer memory store, the settlement register store, and the reviewer's on-disk file store.

Non-software proof fixtures

boatstack/kernel/runtime_test.go runs an integer control instance:

objective.bind → increment → increment → marked(value = 2)
                         ↘ interruption → reset recovery

It binds reach-two@1, invokes deterministic functions, verifies fresh integer observations, advances revisions, commits receipts, rejects stale objective and observation bindings, denies missing capability authority, and recovers an interrupted operator. The fixture imports no software-delivery package and requires no Git executable or repository.

boatstack/kernel/settlement_test.go runs a revisioned-register instance that proves the trusted-settlement laws. Immutable candidate records are identified by content fingerprint and staged outside control state; the accepted-value reader reconstructs only from the durable objective binding plus its committed receipt and fails closed on damaged evidence. The suite covers staging and read-only resolve, verified initial acceptance, verification rejection, freshness drift across all five identities, candidate substitution, atomic commit failure with recovery, racing candidates settling at most once, same-instance and cross-instance replay, restart reconstruction, and fail-closed reading. White-box counterexamples prove the laws reject a mutable candidate store, a latest-staged reader, a torn or blind state-receipt commit, receipt substitution, and restart state reset.

kernel/conformance.GovernedProgressionConformance runs a domain-neutral progression from operator selection through projection, validation, applicability, solving, exact candidate assurance, and receipt-backed admission. Its adapter keeps result candidates, untrusted history, and failure evidence outside accepted control state; releases dependencies only from exact accepted predecessor receipts; and bounds claim strength by both evidence and verifier ceilings. The suite runs over memory, revisioned-register, and file stores and covers substitution, stage bypass, stale state, exact replay, restart, interrupted effects, recovery, missing dependencies, missing authority, over-claiming, and corrupted history. Projection completeness and producer/verifier separation are explicitly fixture-relative structural claims. See governed progression conformance.

Enforced properties

  1. Program determinacy: executable law is bound to one program fingerprint.
  2. Prescription soundness: resolve and apply share one relation.
  3. Freshness: state, program, objective binding, observation, and authority are exact.
  4. Authority non-escalation: program and operator declarations grant nothing.
  5. Effect containment: trusted capabilities and owned facets bound effects.
  6. Objective separation: only an exact binding enters control state.
  7. Objective preservation: unowned transitions cannot change the binding.
  8. Domain isolation: the kernel has no software-delivery dependency.
  9. State ownership: control and effect mutations have explicit owners.
  10. Fact fidelity: receipts contain committed effects and verified observations.
  11. Recovery liveness: uncertain outcomes enter explicit recovery state.
  12. Marked-state generality: the program defines accepted modes.
  13. Operator neutrality: the fixture uses deterministic functions, not an agent.
  14. Domain substitution: the integer domain runs without kernel changes.
  15. Trusted settlement: only an exact committed binding plus receipt is accepted state.
  16. Receipt lineage: receipts prove the prior, requested, and resulting bindings.
  17. Lifecycle explicitness: every binding mutation declares exactly one of bind-initial, advance, replace, or clear, satisfies that relation's own capability, and commits a receipt that independently proves the relation.
  18. Instance isolation: state, revisions, CAS, recovery, locking, and receipt history are local to one explicitly named control instance.
  19. Explicit provisioning: instances are created atomically, never overwritten, and never manufactured for a missing identity.
  20. Committed-result reconciliation: an exact committed retry returns the original durable receipt with zero side effects, and an uncommitted attempt is never reported as successful.
  21. Governed progression composition: the public conformance fixture composes ordered adapter gates with kernel objective, freshness, recovery, and receipt mechanics while keeping external authority and domain-evidence claims explicit.

Current implementation anchors