docs: qualify package identity across uring agent guides

AGENTS.md

@@ -41,6 +41,8 @@ When a task uses a fact owned by another package, read that package before using
 - `code.hybscloud.com/sess` for protocol frontiers, branching, endpoint transitions, and session close semantics.
 - `code.hybscloud.com/takt` for runner movement, polling, resumption, completion memory, completion routing, and route-indexed stream carriers.
 
+For broad guide edits, runtime-utilization edits, or review work that changes the cross-package model, read the complete current source of every package whose facts the edited guide relies on. In practice, this usually means `code.hybscloud.com/iox`, `code.hybscloud.com/iofd`, `code.hybscloud.com/sock`, `code.hybscloud.com/kont`, `code.hybscloud.com/cove`, `code.hybscloud.com/takt`, and `code.hybscloud.com/sess` before changing `uring/AGENTS.md` or any file under `uring/agents/`. Extend that set with `code.hybscloud.com/zcall`, `code.hybscloud.com/iobuf`, `code.hybscloud.com/spin`, `code.hybscloud.com/lfq`, or `code.hybscloud.com/framer` whenever the edited guide cites syscall, buffer, spin/yield, mailbox, or framing facts.
+
 Before generating or reviewing code, read every guide file needed by the task. A file is needed when its topic names a fact, action, resource, outcome, frontier, policy, or obligation used by that task.
 
 Read in this order:

agents/boundary/integration.md

@@ -1,12 +1,12 @@
 # Integration Boundary
 
-Using `uring` correctly means using it *with* its neighbours, each in its own lane, and never letting one package's job leak into another's. This file is the map of who owns what. `OwnerMap` assigns every role to exactly one package: outcome and stream vocabulary to `iox`, descriptors to `iofd`, addresses to `sock`, buffers to `iobuf`, suspension and one-shot resumption to `kont`, protocol frontiers to `sess`, route and subscription frontiers to `takt`, and so on. The rules then pin which facts may be projected across the package boundary and which — caller frontier, caller policy, `cove` requirement evidence, resumptions, mailbox policy, and completion-memory policy — must stay strictly in caller code, and require that every action go through the public surface rather than a bypass.
+Using `code.hybscloud.com/uring` correctly means using it *with* its neighbours, each in its own lane, and never letting one package's job leak into another's. This file is the map of who owns what. `OwnerMap` assigns every role to exactly one package: outcome and stream vocabulary to `code.hybscloud.com/iox`, descriptors to `code.hybscloud.com/iofd`, addresses to `code.hybscloud.com/sock`, buffers to `code.hybscloud.com/iobuf`, suspension and one-shot resumption to `code.hybscloud.com/kont`, protocol frontiers to `code.hybscloud.com/sess`, route and subscription frontiers to `code.hybscloud.com/takt`, and so on. The rules then pin which facts may be projected across the package boundary and which — caller frontier, caller policy, `code.hybscloud.com/cove` requirement evidence, resumptions, mailbox policy, and completion-memory policy — must stay strictly in caller code, and require that every action go through the public surface rather than a bypass.
 
 In plain terms, the rules an agent follows here are:
 
-- Every role has exactly one owner, and you read that owner before using its facts. Outcome, stream, datagram, and byte-progress vocabulary belong to `iox`; syscall result and errno to `zcall`; descriptors to `iofd`; socket addresses to `sock`; buffers to `iobuf`; spin, yield, and lock to `spin`; the caller mailbox queue to `lfq`; frame boundaries to `framer`; context, requirement, and safety evidence to `cove`; suspension and one-shot resumption to `kont`; protocol frontiers to `sess`; and route, subscription, runner-movement, and completion-memory vocabulary to `takt`.
+- Every role has exactly one owner, and you read that owner before using its facts. Outcome, stream, datagram, and byte-progress vocabulary belong to `code.hybscloud.com/iox`; syscall result and errno to `code.hybscloud.com/zcall`; descriptors to `code.hybscloud.com/iofd`; socket addresses to `code.hybscloud.com/sock`; buffers to `code.hybscloud.com/iobuf`; spin, yield, and lock to `code.hybscloud.com/spin`; the caller mailbox queue to `code.hybscloud.com/lfq`; frame boundaries to `code.hybscloud.com/framer`; context, requirement, and safety evidence to `code.hybscloud.com/cove`; suspension and one-shot resumption to `code.hybscloud.com/kont`; protocol frontiers to `code.hybscloud.com/sess`; and route, subscription, runner-movement, and completion-memory vocabulary to `code.hybscloud.com/takt`.
 - Only owned boundary inputs may cross into the boundary. The boundary-projectable carriers are the outcome contract, descriptor authority, socket address, buffer fact, spin/yield fact, and frame boundary; nothing else is projected across.
-- Caller frontier and caller policy never cross into the boundary. Context, requirement, and safety evidence from `cove` may guard caller decisions and may justify copied boundary inputs, but the `cove` carriers themselves stay in caller code. Resumptions, mailbox policy, and completion-memory facts and policy also stay strictly in caller code, and projecting any of them into the boundary is rejected.
+- Caller frontier and caller policy never cross into the boundary. Context, requirement, and safety evidence from `code.hybscloud.com/cove` may guard caller decisions and may justify copied boundary inputs, but carriers from `code.hybscloud.com/cove` stay in caller code. Resumptions, mailbox policy, and completion-memory facts and policy also stay strictly in caller code, and projecting any of them into the boundary is rejected.
 - Every action goes through the public surface. An action that bypasses the public surface is rejected.
 
 The block below states these rules formally.

agents/boundary/protocols.md

@@ -6,14 +6,14 @@ The block carries the same discipline onto the Go surface: a `GoHandler` is shal
 
 In plain terms, the rules an agent follows here are:
 
-- Own the protocol; the package only observes. Stream, datagram, outcome, and byte-progress vocabulary belong to `iox`; suspension and one-shot resumption to `kont`; protocol frontiers to `sess`; route, subscription, runner-movement, and completion-memory vocabulary to `takt`; safety evidence to `cove`; spin, yield, and lock to `spin`. The protocol frontier and policy are caller-owned, and the protocol transition taken after an observation is caller-defined and never lives inside the boundary.
+- Own the protocol; the package only observes. Stream, datagram, outcome, and byte-progress vocabulary belong to `code.hybscloud.com/iox`; suspension and one-shot resumption to `code.hybscloud.com/kont`; protocol frontiers to `code.hybscloud.com/sess`; route, subscription, runner-movement, and completion-memory vocabulary to `code.hybscloud.com/takt`; safety evidence to `code.hybscloud.com/cove`; spin, yield, and lock to `code.hybscloud.com/spin`. The protocol frontier and policy are caller-owned, and the protocol transition taken after an observation is caller-defined and never lives inside the boundary.
 - Read multishot completions as frontier facts, using the same four-way decode. A non-negative multishot CQE with `MORE` is a live success that keeps the frontier non-terminal and signals that a successor observation may arrive; a negative multishot CQE with `MORE` is a non-terminal failure. A failure with `MORE` is never `errMore`, never byte progress, and never terminal.
 - Decode zero-copy release separately. A release-ready CQE decodes to a release observation with no control value, carrying the `NOTIF` flag when the release is notification-driven and not when it is the terminal no-notification fallback; a notification that is not release-ready, and an early notification, both produce no outcome and no release.
 - Hand result resources to the caller. A returned descriptor or selected buffer is owned by the caller and never appears on a non-terminal frontier.
 - Treat the package as a shallow handler, never a deep one. A shallow handler handles one visible frontier, resumes at most once per observation, stores no boundary borrow, and leaves policy in the caller; a deep handler that keeps control over successor observations is a hidden runner loop, which is rejected, so repetition is the caller's own explicit loop.
 - Discharge the shallow obligations. A shallow handler must satisfy the outcome, owner, and policy gates and the support-split obligation — defined in [workflow/boundary-gates.md](../workflow/boundary-gates.md) and [workflow/proof-obligations.md](../workflow/proof-obligations.md) — plus the copy-CQE rule.
 - Keep Go handlers, closures, and tables shallow and caller-owned. A Go handler is shallow when it consumes one visible frontier and resumes at most once; a handler closure may capture only copied completion facts or caller-owned state, never a borrowed CQE view; a handler table is keyed by caller-owned event keys, every handler in it is shallow, it is built before dispatch starts, and hot-path dispatch allocates nothing and builds no closures.
-- Keep parser, route, and completion-memory policy in the caller. Parser state and branch policy, route lookup and retirement, completion pool and GC-root policy, and completion-memory facts and policy are all caller-owned (completion-memory facts owned by `takt`), and none of them may hide inside the boundary.
+- Keep parser, route, and completion-memory policy in the caller. Parser state and branch policy, route lookup and retirement, completion pool and GC-root policy, and completion-memory facts and policy are all caller-owned (completion-memory facts owned by `code.hybscloud.com/takt`), and none of them may hide inside the boundary.
 
 The block below states these rules formally.
 

agents/boundary/resources.md

@@ -161,7 +161,7 @@ Buffers are resources with a lifecycle of their own — `allocate → own → pu
 
 In plain terms, the rules an agent follows here are:
 
-- A buffer has its own lifecycle, owned by `iobuf`. It moves `allocate → own → publish → select → consume → recycle → release`, and the buffer-shaping facts (pool index, aligned region, iovec view, array copy, typed slice view, reset-without-zero) belong to `iobuf`.
+- A buffer has its own lifecycle, owned by `code.hybscloud.com/iobuf`. It moves `allocate → own → publish → select → consume → recycle → release`, and the buffer-shaping facts (pool index, aligned region, iovec view, array copy, typed slice view, reset-without-zero) belong to `code.hybscloud.com/iobuf`.
 - While the kernel may own a buffer, you may not touch it. Reuse, return, mutate, unregister, and recycle are all disabled for a buffer the kernel may still be reading or writing.
 - Register, provide, select, and consume under explicit preconditions. Registration needs an owned, aligned, stable-address buffer and a valid slot; a provided buffer is published to a valid group and id; a selected buffer comes from a CQE carrying the buffer-select flag and a selected-buffer frontier; after consuming the first `n` bytes the buffer is recycled, copied-then-recycled, or released.
 - Release a zero-copy window exactly once, and only when it is safe. The release fires after both the data and notification frontiers are observed, or through an explicit terminal no-notification fallback, and never more than once; while pending it stays kernel-owned.

agents/formalization/INDEX.md

@@ -2,9 +2,9 @@
 
 Use these files when the task needs the formal notation behind the public `code.hybscloud.com/uring` agent guide. They cover caller code that directly invokes the package and broader systems built above that caller layer. They also describe abstraction from Go into the guide notation and compilation from checked notation back into Go. The files are ordered from notation basics to verification closure.
 
-The formalization guide family is checked as a composed guide: each topic file states an internal well property, and the topic judgments must remain provably composable under the closure conditions in [uring/agents/formalization/overview.md](overview.md), [uring/agents/formalization/guarantees.md](guarantees.md), and [uring/agents/formalization/verification.md](verification.md).
+The formalization guide family is checked as a composed guide: each topic file is checked by `GuideInternalWell_U(f)`, defined in [uring/agents/formalization/guarantees.md](guarantees.md), and the topic judgments must remain provably composable under the closure conditions in [uring/agents/formalization/overview.md](overview.md), [uring/agents/formalization/guarantees.md](guarantees.md), and [uring/agents/formalization/verification.md](verification.md).
 
-The formal vocabulary stays explicit in `uring` terms. Preserve every group when editing any topic file:
+The formal vocabulary stays explicit in `code.hybscloud.com/uring` boundary terms. Preserve every group when editing any topic file:
 
 ```text
 kernel           := {core, judgment, Ctrl, noHidden, canonicalLevel}
@@ -15,8 +15,8 @@ reify_runner     := {Reify, Reflect, trampoline, runner, Suspension, coalgebra}
 compilation      := {compile_to_go, outcome_compilation, handler_compilation, contextual_compilation}
 sessions_outcomes := {duality, projection, Outcome, Π, Backoff, ErrWouldBlock, ErrMore}
 metatheory       := {soundness, completeness, consistency, preservation, progress}
-abstraction      := {LIFT, SAVE, ANALYZE, FIX, REPORT, UPDATE, formalize, typecheck, reduce, prove, verify}
-middleware       := {middleware, shallow_handler, iox, kont, cove, takt}
+abstraction      := {LIFT, SAVE, ANALYZE, FIX, REPORT, UPDATE, analyze, lift, formalize, typecheck, reduce, prove, verify}
+middleware       := {middleware, shallow_handler, pkg("code.hybscloud.com/iox"), pkg("code.hybscloud.com/kont"), pkg("code.hybscloud.com/cove"), pkg("code.hybscloud.com/takt")}
 properties       := {Structural_Soundness, Conservativity, Composability, Parametricity, extension_admissibility}
 ```
 

agents/formalization/go-mapping.md

@@ -1,6 +1,6 @@
 # Go Mapping
 
-The model in the other topic files only matters because it maps faithfully to real Go. This file is that bridge, in both directions. *Abstraction* lifts a Go surface up into a judgment so you can reason about it; *compilation* sends a judgment back down to Go and demands that the round trip preserve denotation and never smuggle caller frontier or policy into the boundary. When you change `uring` code, this is the file that says your change still *means* what the model says it means: same outcomes, same release evidence, ownership and epochs intact, nothing hidden in the boundary.
+The model in the other topic files only matters because it maps faithfully to real Go. This file is that bridge, in both directions. *Abstraction* lifts a Go surface up into a judgment so you can reason about it; *compilation* sends a judgment back down to Go and demands that the round trip preserve denotation and never smuggle caller frontier or policy into the boundary. When you change `code.hybscloud.com/uring` code, this is the file that says your change still *means* what the model says it means: same outcomes, same release evidence, ownership and epochs intact, nothing hidden in the boundary.
 
 ## Abstraction: Go To Guide
 

agents/formalization/guarantees.md

@@ -208,7 +208,7 @@ Completeness_relative(surface) ⇔
 ```
 ## The Properties A Change Must Satisfy
 
-The theorems above are about the system; the properties below are about *your* judgment and *your* Go. Each is a predicate you can check directly: owner unique, resources affine, outcomes separated, policy kept out of the boundary, denotation defined, round trip closed. `Accept(J, go_surface)` bundles them into the bar a change must clear — it is the formal restatement of "this change uses `uring` correctly".
+The theorems above are about the system; the properties below are about *your* judgment and *your* Go. Each is a predicate you can check directly: owner unique, resources affine, outcomes separated, policy kept out of the boundary, denotation defined, round trip closed. `Accept(J, go_surface)` bundles them into the bar a change must clear — it is the formal restatement of "this change uses `code.hybscloud.com/uring` correctly".
 
 ```text
 module = pkg("code.hybscloud.com/uring")

agents/formalization/handler.md

@@ -1,6 +1,6 @@
 # Handler
 
-`uring` is a *shallow* effect handler: it observes one boundary action and hands control straight back to the caller. It never owns the loop, never reinstalls itself to interpret the next completion, and never captures caller policy. This file is the operational heart of that claim. Read it to know exactly how a boundary action steps, what counts as a normal form, and how a suspension is resumed at most once per observation — because the moment a change makes the handler *deep* (a hidden runner loop, a retained continuation, policy baked into the step), every separation the guide promises collapses.
+`code.hybscloud.com/uring` is a *shallow* effect handler: it observes one boundary action and hands control straight back to the caller. It never owns the loop, never reinstalls itself to interpret the next completion, and never captures caller policy. This file is the operational heart of that claim. Read it to know exactly how a boundary action steps, what counts as a normal form, and how a suspension is resumed at most once per observation — because the moment a change makes the handler *deep* (a hidden runner loop, a retained continuation, policy baked into the step), every separation the guide promises collapses.
 
 The three sections move from the small-step calculus, to the reduction that says when stepping is done, to the suspend/resume boundary where a kernel observation is delivered to the caller's continuation.
 
@@ -180,7 +180,7 @@ ReductionSound(J,J_nf) ⇔
 
 ## Suspend, Resume, And The Observation Boundary
 
-This is where one kernel observation crosses into the caller's continuation. A suspension is resumed at most once per observation, the continuation is owned by the caller layer (not the boundary), and the runner loop is the caller's, not the package's. The two rejections at the end — no hidden runner loop, no boundary-owned caller frontier — are what keep `uring` shallow rather than silently deep.
+This is where one kernel observation crosses into the caller's continuation. A suspension is resumed at most once per observation, the continuation is owned by the caller layer (not the boundary), and the runner loop is the caller's, not the package's. The two rejections at the end — no hidden runner loop, no boundary-owned caller frontier — are what keep `code.hybscloud.com/uring` shallow rather than silently deep.
 
 ```text
 module = pkg("code.hybscloud.com/uring")