Behavior Actors template-law audit (engineering record)

Historical evidence snapshot: the retained campaign verdicts were last committed at 1f20cc4. They describe that revision. The current repository quality audit tracks later verification and unresolved work.

This is the working record of a proof-driven audit of every reusable Behavior implementation exported by bombay-behavior-actors. It replaces the earlier routing-only review, which incorrectly accepted creator-local delivery from a standalone MessageAdapter and did not test BehaviorBase at the runtime resolution boundary.

This file is not a completion certificate. A verdict is final only after its negative cases have an independent oracle and the full repository gates pass on the recorded revision. Earlier versions of this file incorrectly declared the catalogue complete while several action-loss and hard-coded-path cases were still untested; those declarations are not evidence.

Active owner-contract follow-up ledger

This checkpoint records the four independently reported gaps before any production edit. It is not evidence that any gap is closed.

• Exact blockers and smallest regressions:
  1. A generic framework can declare and finish shutdown phases through associated outputs, but cannot begin the one existing inferred builder without naming its hidden initial proof. A compile-only external-consumer regression must call a generic begin operation, declare two roles, and finish without spelling builder states.
  2. RelayChildReports forwards nested ingress but drops root ShutdownRequested ingress. Pure-fold regressions must cover the relay, FIFO pool, keyed pool, and relay under another transparent composition; the report lane must remain exactly once.
  3. Supervise retains worker installation and replacement facts but exposes no typed evidence to its inner application. An independent lifecycle trace must observe initial readiness with the exact worker nonce, replacement start/unavailability, replacement readiness, and permanent retirement or restart denial without guessing elapsed time.
  4. WorkerPool::new and KeyedWorkerPool::new cannot infer the customer route because no input mentions it. External-user compile tests must compare an associated construction operation, a route witness, and an extension operation, rejecting any dummy value that the pool does not semantically retain.
• Source classification: serialized actor turns, fresh creation, and the absence of a cross-producer arrival-order guarantee are actor-model laws. Root-ingress preservation and the associated-output builder entry are derived static compositions. Lifecycle evidence after a committed ownership transition, its exact fact vocabulary, and restart timing are explicit Bombay policy rather than Agha guarantees.
• Expected files: shutdown builder/re-exports and its interpretation test; report relay plus relay/pool composition tests; supervision protocol, ownership fold, adapter and model/fuzz tests; pool constructors and one external construction test; this audit record. Expected cumulative ceiling: 15 changed files.
• Expected production delta: at most +260 / -40 / net +220. Tests and documentation are measured separately at each checkpoint.
• Expected public API: add at most three public items: one begin operation, one exhaustive lifecycle fact sum (with data carried in its variants), and one owner-defined pool construction operation only if existing inherent syntax cannot express the inference law. Add no wrapper, alias, builder, route marker, registry, or erased envelope. Remove any superseded public machinery discovered in the same semantic path rather than retaining a compatibility layer.
• Existing machinery to reuse: shutdown_after_children and its sole ChildShutdownPhases typestate; InjectEvent/ComposedEvent and the relay's named SendLayer; FixedFleetOwnership, OwnershipFold, and SupervisionEvent; DeliveryRoute, Recipient, BehaviorLayer, and the existing FIFO/keyed pool folds. No parallel planner, lifecycle wrapper, or pool factory object is permitted.
• Toolchain finding: the repository pins Rust 1.95. General type-position ! remains unavailable on that toolchain and on stable 1.98; stabilizing it remains an active Rust 2026 project goal. The existing uninhabited Never remains the MSRV-compatible representation. Neither Never nor ! can constrain a customer route generic that occurs in no constructor input.

Supervision lifecycle design checkpoint

The application-facing lifecycle is one exhaustive event sum, not a wrapper, callback, query API, or second supervisor. One authoritative runtime fact may produce at most one inner lifecycle event. Multi-slot restart policy is carried as one named batch variant so the inner application performs at most one fold per outer turn.

The Ready join is symmetric: worker-first retains the worker fact without notifying, proxy-first retains the proxy fact without notifying, and the matching second success emits exactly one event. Duplicate, stale, wrong-kind, wrong-nonce, and contradictory facts remain the existing typed errors and emit no lifecycle event.

Lifecycle delivery must be an ordinary variant in the inner application's named exhaustive domain/system event sum. That sum owns EventIngress<Here, SupervisionLifecycle<A>>; existing structural EventLayer compositions lift the source-indexed ingress to it without a caller naming or recounting wrapper depth. Supervise must not make the lane optional, silently discard it, invoke a callback, or queue an interpreter-private self-message. Applications needing no lifecycle evidence use the standalone Supervisor topology owner instead.

Controlled-error atomicity requires a prepare/commit transition:

1. validate the authoritative fact against the current ownership sum;
2. prepare the next ownership state, effects, and one lifecycle event without mutating ownership (restart admission is calculated on a staged budget and newly built workers remain owned by the plan);
3. fold the lifecycle event through the inner application;
4. only after that fold succeeds, commit the prepared ownership state and combine the complete inner and ownership Actions products once.

If the inner fold rejects the lifecycle event, the prepared workers are dropped and neither the restart budget nor ownership state commits. This preserves B7 rather than relying on actor termination to hide partial mutation. For lifecycle-free authoritative facts, the existing ownership transition is unchanged.

Making this lane truthful is intentionally source-breaking: every current Supervise inner event that lacks the lane must be migrated explicitly. A scan finds 20 source/test/fuzz call-site files in addition to the supervision protocol, ownership fold, and adapter. With the nine files already changed in this follow-up, the complete migration necessarily exceeds the 15-file review checkpoint; compatibility modes would only evade that checkpoint while preserving the broken contract.

The audit question is not merely whether a template's fold compiles. For every capability or lifecycle fact, the review traces:

1. who produced or supplied it;
2. which concrete type retains it;
3. which actor namespace owns its interpretation;
4. which Actions lane emits it;
5. which static interpreter authority realizes it; and
6. how rejection or stale input remains typed and observable.

Laws and policies used

The source classification matters. Framework convention is not presented as actor-model law.

Actor-model laws

• A1 — serialized turns: one actor processes one communication at a time; the transition determines communications, fresh creation, and the next behavior.
• A2 — finite acquaintance: a transition may communicate with prior acquaintances, acquaintances in the current communication, and freshly created actors.
• A3 — fresh creation: allocation is fresh; replacing behavior with become is distinct from actor creation.
• A4 — no primitive effect ordering: the actor model does not require a general order among send, create, and become effects.

The primary-source classification and the exact boundary between these laws and Bombay constructions are summarized in the canonical actor-transition algebra and established-capabilities contracts.

Behavior Core laws

• B1 — explicit effects: a successful pure fold returns complete Actions; it does not deliver, allocate, schedule, observe, or stop actors through an ambient side channel.
• B2 — concrete protocols: protocol, event sum, send product, phase, error, and birth algebra remain statically visible.
• B3 — capability distinctions: Recipient, ChildRoute, and EstablishedRecipient mean logical name, creator-local occurrence, and exact installed incarnation respectively. They are not interchangeable.
• B4 — structural child authority: a local child effect resolves only when the running emitter's direct Birth algebra proves the named occurrence.
• B5 — transparent projection: nominal roles cross BehaviorBase only while both canonical protocol and complete direct-birth algebra are equal.
• B6 — compositional initialization: wrappers initialize their inner fold once, preserve its full result, and define how wrapper effects accumulate.
• B7 — typed rejection: rejected creation carries no established capability; controlled transition failures do not partially commit a new behavior state.

Declared Bombay policy

• P1 — staged child routes: a creator-local nonce may name a requested child before interpretation but is neither an address nor freshness proof.
• P2 — commit before dependency: interpreters commit same-action creation before dependent local sends and observation requests.
• P3 — explicit provenance: birth, replacement incarnation, observation relationship, timer generation, and shutdown request provenance travel as typed data.
• P4 — structural return paths: interpreter facts return through the exact typed path selected by the owning composition.
• P5 — explicit root shutdown: the root is composed directly as StopOnShutdown, FinalizeOnShutdown, or a shutdown coordinator; it does not discover a nested shutdown handler.
• P6 — stable logical domains: discovery membership, configured downstream destinations, stable proxy identity, and transport names deliberately remain logical recipients.
• P7 — truthful customer routes: a template that accepts an arbitrary customer capability retains its logical or exact form and emits the matching concrete effect without conversion.
• P8 — creation-dependent shutdown plans: a coordinator may begin before its committed children are known. The topology owner reports its validated plan through Actions to an explicit parent return path; installation is one typed event, happens at most once, and retains any earlier shutdown request.

Hypotheses and verdicts

Failed → fixed means the hypothesis was false in the audited revision and this change repairs it. A pass means both the public type surface and the relevant fold/interpreter seam support the statement.

The repairs require no new Behavior Core algebra, runtime registry, dynamic type, forwarding actor, or address reconstruction. The verification record below is authoritative only when every listed gate is green on the same tree.

Complete template coverage

The hypotheses above were applied to every exported behavior family, not just the templates implicated by the initial blockers.

Routing strategies are policy values owned by Router, not actors with their own effect boundary. Redundant aliases for the same observation and shutdown state machines were removed rather than counted as separate templates.

Adversarial law coverage

The audit does not count a constructor smoke test as proof of a state-machine law. The following independent suites model state after every generated step:

Each model uses different vocabulary and ordinary collections. It compares observable state and complete owned outputs after every operation, including rejection and stale input. Fuzz targets are retained as a separate layer; they do not replace the reference models.

Verification checkpoint — 2026-08-27 working tree

• cargo nextest run --workspace --no-fail-fast: 542 passed, none skipped.
• cargo clippy --workspace --all-targets: pass without Rust warnings.
• The nominal-protocol, pool named-product, keyed/FIFO model, and corrected supervision regressions pass in both debug and optimized profiles.
• The pool state-machine fuzz target completed 5,000 executions after keyed delegation.

This is an intermediate checkpoint, not the final repository gate. The final record must be updated only after cargo nextest run --workspace and nix flake check pass on the same committed tree.

Capability conclusions

The three recipient forms have non-overlapping authority:

EstablishedChild<C, O> intentionally retains the latter two facts together. It is an Actors-level named product over existing capabilities. It neither allocates an actor nor extends the Behavior algebra.

Future changes must repeat the six-step provenance trace above. A test that only inspects the emitted value is insufficient for creator-local effects: the running emitter must also prove that its interpreter can lawfully resolve the same occurrence.