docs: add source evidence and coding-obligation predicates to uring agent guides

AGENTS.md

@@ -104,7 +104,7 @@ Use the caller-layer packages according to the role they own:
 - Use `code.hybscloud.com/takt` when caller code needs runner movement, completion memory, polling, error-aware stepping, or route-indexed stream carriers. `Advance` and `AdvanceSuspension` resume on dispatcher-level `ErrMore`; generic `Loop` rejects completion-level `ErrMore` as unsupported multishot; `SubscriptionLoop` is the carrier for live stream routes.
 - Use `code.hybscloud.com/sess` when protocol branching, endpoint frontiers, paired protocol execution, or error-aware endpoint stepping sits above the completion stream. Its transport backpressure is `ErrWouldBlock` from `code.hybscloud.com/iox`; `ErrMore` is outside the endpoint transport domain, so live multishot routing must be classified before it reaches a session endpoint.
 
-These packages are general caller-layer tools. The obligations in this guide apply when caller code uses them to wrap or drive a `code.hybscloud.com/uring` boundary action. Error-aware forms from `code.hybscloud.com/takt` and `code.hybscloud.com/sess` carry caller protocol policy; they do not change what a `code.hybscloud.com/uring` boundary helper may own. The detailed utilization guides for these packages live under [`agents/runtime/`](agents/runtime/), starting from [`agents/runtime/INDEX.md`](agents/runtime/INDEX.md).
+These packages are general caller-layer tools. The obligations in this guide apply when caller code uses them to wrap or drive a `code.hybscloud.com/uring` boundary action. Error-aware forms from `code.hybscloud.com/takt` and `code.hybscloud.com/sess` carry caller protocol policy; they do not change what a `code.hybscloud.com/uring` boundary helper may own. The detailed utilization guides for these packages live under [`agents/runtime/`](agents/runtime/), starting from [`agents/runtime/INDEX.md`](agents/runtime/INDEX.md); those files also name the package source files and coding obligations used for review.
 
 Protocol stacks built above or beyond `code.hybscloud.com/uring` can treat the package as a shallow boundary handler: it exposes kernel observations and returns control to the caller. Protocol parsing, retries, route state, and terminal policy stay in the caller's protocol or runtime layer. The handler discipline is defined in [`agents/boundary/protocols.md`](agents/boundary/protocols.md) and restated in each file under [`agents/runtime/`](agents/runtime/) for the package it covers.
 

agents/formalization/INDEX.md

@@ -4,21 +4,19 @@ Use these files when the task needs the formal notation behind the public `code.
 
 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 `code.hybscloud.com/uring` boundary terms. Preserve every group when editing any topic file:
-
-```text
-kernel           := {core, judgment, Ctrl, noHidden, canonicalLevel}
-syntax           := {NameAtoms, facts, Γ, Δ, Θ, χ, Σ, Μ, Φ, Obs, Rel, Π}
-typing           := {typing, resource, session, effect, coeffect}
-reduction        := {reduction, wouldBlock, errMore, shallow_handler, coeffect}
-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, 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}
-```
+The formal vocabulary stays explicit in `code.hybscloud.com/uring` boundary terms, but this index remains a navigation file. When editing a topic file, preserve the vocabulary group it owns:
+
+- Kernel and judgment vocabulary: core boundary facts, `Ctrl`, `noHidden`, and `canonicalLevel`.
+- Syntax vocabulary: `NameAtoms`, facts, `Γ`, `Δ`, `Θ`, `χ`, `Σ`, `Μ`, `Φ`, `Obs`, `Rel`, and `Π`.
+- Typing vocabulary: typing, resource, session, effect, and coeffect judgments.
+- Reduction vocabulary: `wouldBlock`, `errMore`, shallow-handler reduction, and coeffect reduction.
+- Runner and bridge vocabulary: `Reify`, `Reflect`, trampoline, runner, `Suspension`, and coalgebra.
+- Compilation vocabulary: `compile_to_go`, outcome compilation, handler compilation, and contextual compilation.
+- Session and outcome vocabulary: duality, projection, `Outcome`, `Π`, `Backoff`, `ErrWouldBlock`, and `ErrMore`.
+- Metatheory vocabulary: soundness, scope-relative completeness, consistency, preservation, and progress.
+- Workflow vocabulary: `analyze`, `lift`, `formalize`, `typecheck`, `reduce`, `prove`, `compile_to_go`, and `verify`, together with saved-stage records.
+- Middleware vocabulary: shallow-handler composition across `code.hybscloud.com/iox`, `code.hybscloud.com/kont`, `code.hybscloud.com/cove`, and `code.hybscloud.com/takt`.
+- Property vocabulary: `Structural_Soundness`, `Conservativity`, `Composability`, `Parametricity`, and `extension_admissibility`.
 
 Read the formalization files in this order:
 

agents/formalization/go-mapping.md

@@ -8,6 +8,7 @@ The block lifts a `GoSurface` into a `JudgmentSurface` (`lift = ⟦·⟧⁻¹_U`
 
 ```text
 module = pkg("code.hybscloud.com/uring")
+B = boundary(module)
 A = above(module)
 D = beyond(module)
 C = caller(module) = A ∪ D
@@ -177,24 +178,32 @@ compile_denotation_preserved(J,w) ⇔
 CompileSubmit(J) ⇔
   defined(⟦J⟧_U)
   ∧ action(J)=submit
-  ∧ ⟦J⟧_U = helper(submit)
-  ∧ emits(Encode(req,ctx))
-  ∧ no_loop(helper)
-  ∧ no_retry(helper)
+  ∧ ∃ req,ctx,h.
+      h = ⟦J⟧_U
+      ∧ h = helper(submit)
+      ∧ emits(h,Encode(req,ctx))
+      ∧ no_loop(h)
+      ∧ no_retry(h)
 
 CompileObserve(J) ⇔
   defined(⟦J⟧_U)
   ∧ action(J)∈{wait,observe,decode}
-  ∧ ⟦J⟧_U = helper(action(J))
-  ∧ reads(cqe)
-  ∧ (operation_cqe(cqe) → projects(CQEToObs(cqe,ctx,r,χ(J))))
-  ∧ (release_ready_carrier(cqe,ctx,r) → projects(ReleaseProjection(cqe,ctx,r,χ(J))))
-  ∧ preserves(cqe.Res,cqe.Flags,cqe.user_data)
+  ∧ ∃ cqe,ctx,r,h.
+      h = ⟦J⟧_U
+      ∧ h = helper(action(J))
+      ∧ reads(h,cqe)
+      ∧ (operation_cqe(cqe) → projects(h,CQEToObs(cqe,ctx,r,χ(J))))
+      ∧ (release_ready_carrier(cqe,ctx,r) →
+          projects(h,ReleaseProjection(cqe,ctx,r,χ(J))))
+      ∧ preserves(h,{cqe.Res,cqe.Flags,cqe.user_data})
 
 CompileResource(J) ⇔
-  preserves(Θ(J),Θ'(J))
-  ∧ no_hidden_pool_policy(helper)
-  ∧ no_hidden_gc_root(helper)
+  defined(⟦J⟧_U)
+  ∧ ∃ h.
+      h = ⟦J⟧_U
+      ∧ preserves(h,{Θ(J),Θ'(J)})
+      ∧ no_hidden_pool_policy(h)
+      ∧ no_hidden_gc_root(h)
 
 CompilePolicy(J) ⇔
   defined(⟦J⟧_U)
@@ -212,6 +221,9 @@ compilation_sound(J) ⇔
   ∧ DesignDirection(J)
   ∧ Roundtrip1(J)
   ∧ ∃ w ∈ World_U. compile_denotation_preserved(J,w)
+  ∧ (action(J)=submit → CompileSubmit(J))
+  ∧ (action(J)∈{wait,observe,decode} → CompileObserve(J))
+  ∧ CompileResource(J)
   ∧ CompilePolicy(J)
 
 reject(defined(⟦J⟧_U) ∧ hidden(CallerFrontier ∪ CallerPolicy, support(⟦J⟧_U)))

agents/formalization/notation.md

@@ -16,9 +16,11 @@ The block below fixes the module strata (boundary `B`, caller `C = A ∪ D`, bel
 
 ```text
 module = pkg("code.hybscloud.com/uring")
+B = boundary(module)
 A = above(module)
 D = beyond(module)
 C = caller(module) = A ∪ D
+K = below(module)
 
 ASCIIAlpha = { c | "A" ≤ c ≤ "Z" ∨ "a" ≤ c ≤ "z" }
 ASCIIDigit = { c | "0" ≤ c ≤ "9" }
@@ -252,6 +254,13 @@ capital_sort_or_identifier(x) ⇔ x ∈ SortOrKind ∪ IdentifierCapital
 ∀x. bound_instance(x) → x ∉ SortOrKind ∧ x ∉ IdentifierCapital
 ∀cqe. field_access(cqe) ⊆ {cqe.Res, cqe.Flags, cqe.user_data}
 
+PathName = {p | finite_string(p)}
+Path = {path(p) | p ∈ PathName}
+SourceFile = {f ∈ Path | checked_out_source_file(f)}
+read_current_source : SourceFile → Bool
+read_current_source(f) ⇔
+  f ∈ SourceFile ∧ file_exists(f) ∧ read_at_current_revision(f)
+
 capital_allowed(Ctx) ⇔ kind_position(Ctx) ∨ sort_annotation(Ctx)
 capital_allowed(CQE) ⇔ sort_position(CQE) ∨ type_annotation(CQE)
 capital_allowed(R[κ]) ⇔ kind_family(R[κ])

agents/formalization/sessions.md

@@ -14,10 +14,10 @@ The block below states these rules formally.
 
 ```text
 module = pkg("code.hybscloud.com/uring")
+B = boundary(module)
 A = above(module)
 D = beyond(module)
 C = caller(module) = A ∪ D
-B = boundary(module)
 World_U = { w | world_for(module,w) }
 Denotation_U(w) = { d | denotation_at(module,w,d) }
 

agents/lift/protocols-runtime.md

@@ -311,6 +311,26 @@ RuntimeOwnerFact_rc =
   {runtime_owner_pkg(p) | p ∈ RuntimeOwnerPkg}
 support(RuntimeOwnerFact_rc) ⊆ C
 RuntimeOwnerFact_rc ∩ support(B) = ∅
+RuntimeSource_rc =
+  { path("kont/effect.go"), path("kont/cont.go"), path("kont/frame.go"),
+    path("kont/bridge.go"), path("kont/step.go"), path("kont/trampoline.go"),
+    path("kont/index.go"), path("kont/affine.go"), path("kont/marker_pool.go"),
+    path("kont/pool.go"), path("kont/dispatch.go"),
+    path("cove/constraint.go"), path("cove/view.go"), path("cove/cmd.go"),
+    path("cove/req.go"), path("cove/req_expr.go"), path("cove/rule.go"),
+    path("cove/rule_expr.go"), path("cove/checked.go"),
+    path("cove/checked_expr.go"), path("cove/step.go"),
+    path("cove/kripke.go"), path("cove/bridge.go"),
+    path("takt/backend.go"), path("takt/takt.go"), path("takt/bridge.go"),
+    path("takt/step.go"), path("takt/error.go"), path("takt/loop.go"),
+    path("takt/option.go"), path("takt/subscription_backend.go"),
+    path("takt/subscription.go"), path("takt/subscription_option.go"),
+    path("takt/completion_memory.go"),
+    path("sess/op.go"), path("sess/session.go"), path("sess/step.go"),
+    path("sess/error.go"), path("sess/run.go"), path("sess/bridge.go"),
+    path("sess/fused.go"), path("sess/fused_expr.go"),
+    path("sess/rec.go"), path("sess/exec.go"), path("sess/serial.go") }
+source_checked(RuntimeSource_rc) ⇔ ∀ f ∈ RuntimeSource_rc. read_current_source(f)
 
 RuntimeTheoryRoute_rc =
   { pkg("code.hybscloud.com/kont")
@@ -358,6 +378,16 @@ current_suspension_rc(c) =
 current_suspension_rc(op) =
   ιs. s ∈ OneShotSuspension ∧ pending_op(s)=op
   if ∃!s. s ∈ OneShotSuspension ∧ pending_op(s)=op
+runtime_resume_value_rc(cqe) =
+  copy({cqe.Res, cqe.Flags, cqe.user_data, selected_buffer_metadata(cqe)})
+BoundaryContextFact_rc(cqe) =
+  copy({cqe.Res, cqe.Flags, cqe.user_data, selected_buffer_metadata(cqe),
+        capability_fact(cqe), ownership_fact(cqe)})
+ContextExtension_rc(ctx,cqe) =
+  extend(ctx,BoundaryContextFact_rc(cqe))
+support(ContextExtension_rc(ctx,cqe)) ⊆ C
+project(ContextExtension_rc(ctx,cqe),B) = ∅
+borrowed_cqe_pointer ∉ BoundaryContextFact_rc(cqe)
 more_flag_rc(c) = c.More
 more_flag_rc(c) ∈ Bool
 More_rc(c) ⇔ more_flag_rc(c) = true
@@ -392,6 +422,8 @@ ErrDisposed_rc =
   err_symbol(pkg("code.hybscloud.com/takt"),"ErrDisposed")
 ErrMore_rc ∈ ErrorSymbol
 ErrWouldBlock_rc ∈ ErrorSymbol
+SessTransportDomain_rc = {nil, ErrWouldBlock_rc}
+ErrMore_rc ∉ SessTransportDomain_rc
 TaktFatalSymbol_rc =
   {ErrUnsupportedMultishot_rc, ErrLiveTokenReuse_rc,
    ErrLiveRouteReuse_rc, ErrInvalidRouteID_rc, ErrDisposed_rc}
@@ -413,12 +445,65 @@ SessCarrier =
    Reify, Reflect, Step, Advance, StepError, AdvanceError,
    Run, RunExpr, RunError, RunErrorExpr,
    Exec, ExecExpr, ExecError, ExecErrorExpr, Loop, ExprLoop}
+SessOp_rc = {Send[T], Recv[T], Close, SelectL, SelectR, Offer}
+BoundaryProtocolStep_rc(step) ⇔
+  defined(bind(step)) ∧ bind(step) ∈ boundary_action(B)
+∀ protocol_io_step_rc.
+  BoundaryProtocolStep_rc(protocol_io_step_rc) →
+    one_boundary_action(bind(protocol_io_step_rc))
 
 Carrier_rc = KontCarrier ∪ CoveCarrier ∪ TaktCarrier ∪ SessCarrier
 support(Carrier_rc) ⊆ C
 project(Carrier_rc,B) = ∅
 support({PendingTable_rc,RouteTable_rc}) ⊆ C
 project({PendingTable_rc,RouteTable_rc},B) = ∅
+CodingObligation_kont_rc(op,s,cqe) ⇔
+  source_checked(RuntimeSource_rc)
+  ∧ BoundarySuspension(s,op)
+  ∧ one_shot(op)
+  ∧ copied_facts(runtime_resume_value_rc(cqe))
+  ∧ borrowed_cqe_view ∉ runtime_resume_value_rc(cqe)
+  ∧ project({s,resume,try_resume,discard},B) = ∅
+CodingObligation_cove_rc(ctx,s,guard,cqe) ⇔
+  source_checked(RuntimeSource_rc)
+  ∧ CoveRequirementGate(ctx,s,guard)
+  ∧ support(ContextExtension_rc(ctx,cqe)) ⊆ C
+  ∧ borrowed_cqe_pointer ∉ ContextExtension_rc(ctx,cqe)
+  ∧ project(CoveCarrier,B) = ∅
+CodingObligation_takt_rc(op,token,cqe) ⇔
+  source_checked(RuntimeSource_rc)
+  ∧ submit_token_rc(token,op)
+  ∧ token_indexes(token,user_data(op))
+  ∧ copied_facts(runtime_resume_value_rc(cqe))
+  ∧ classify_takt_dispatch(ErrMore_rc) ≠ classify_takt_completion_loop(ErrMore_rc)
+  ∧ project(TaktCarrier ∪ {PendingTable_rc,RouteTable_rc},B) = ∅
+CodingObligation_takt_stream_rc(op,route,c,cqe) ⇔
+  source_checked(RuntimeSource_rc)
+  ∧ multishot(op)
+  ∧ carrier(op) = SubscriptionLoop(pkg("code.hybscloud.com/takt"))
+  ∧ route ∈ RouteID
+  ∧ route = route_rc(c)
+  ∧ boundary_stream_completion_rc(c,cqe)
+  ∧ project(TaktCarrier ∪ {RouteTable_rc},B) = ∅
+CodingObligation_sess_rc(ep,op,err) ⇔
+  source_checked(RuntimeSource_rc)
+  ∧ single_owner(ep)
+  ∧ op ∈ SessOp_rc
+  ∧ ∃ protocol_io_step_rc.
+      BoundaryProtocolStep_rc(protocol_io_step_rc)
+      ∧ bind(protocol_io_step_rc) = op
+  ∧ err ∈ SessTransportDomain_rc
+  ∧ classify_sess_transport(err) ∈ {ok,wouldBlock}
+  ∧ classify_sess_transport(ErrMore_rc) = unexpected(ErrMore_rc)
+  ∧ protocol_frontier(session(ep)) ∈ CallerFrontier
+  ∧ support(protocol_frontier(session(ep))) ⊆ C
+  ∧ project(SessCarrier,B) = ∅
+RuntimeCodingObligation_rc =
+  {CodingObligation_kont_rc, CodingObligation_cove_rc,
+   CodingObligation_takt_rc, CodingObligation_takt_stream_rc,
+   CodingObligation_sess_rc}
+support(RuntimeCodingObligation_rc) ⊆ C
+project(RuntimeCodingObligation_rc,B) = ∅
 
 CoveRequirementGate(ctx,s,guard) ⇔
   owner(ctx) = pkg("code.hybscloud.com/cove")
@@ -597,6 +682,8 @@ Preservation_rc =
   ∧ support(BoundaryFacts) ⊆ B
   ∧ project(Carrier_rc ∪ RuntimePolicy,B)=∅
   ∧ project(RuntimeTheoryUse_rc,B)=∅
+  ∧ support(RuntimeCodingObligation_rc) ⊆ C
+  ∧ project(RuntimeCodingObligation_rc,B)=∅
   ∧ classify_takt_dispatch(ErrMore_rc)
        ≠ classify_takt_completion_loop(ErrMore_rc)
   ∧ classify_takt_dispatch(ErrMore_rc)

agents/runtime/INDEX.md

@@ -2,7 +2,7 @@
 
 This directory explains how caller-side code combines `code.hybscloud.com/uring` with four caller-layer support packages: `code.hybscloud.com/kont` for suspension and one-shot resumption, `code.hybscloud.com/cove` for explicit context and requirement evidence, `code.hybscloud.com/takt` for runner movement, completion routing, and error-aware stepping, and `code.hybscloud.com/sess` for session-typed protocol frontiers, paired execution, and endpoint stepping. The packages themselves stay in the caller layer. A boundary helper may receive copied facts derived from them, but it must not import their policy, route state, endpoint state, completion memory, or long-lived control logic into `code.hybscloud.com/uring`.
 
-Each file describes one package: which boundary facts it consumes, which caller-owned decisions it carries, and which obligations apply when its carriers wrap a `code.hybscloud.com/uring` boundary action. The packages remain general caller-layer tools; the formulas in this directory constrain their boundary-wrapped use, not every possible use of those packages. The shallow handler discipline defined in [uring/agents/boundary/protocols.md](../boundary/protocols.md) is restated inside each file for the package it covers: every carrier handles one boundary observation and returns control to the caller. Read the package source named by a file before relying on its facts, following the checklist in [uring/agents/workflow/task-checklists.md](../workflow/task-checklists.md).
+Each file describes one package: which boundary facts it consumes, which caller-owned decisions it carries, and which obligations apply when its carriers wrap a `code.hybscloud.com/uring` boundary action. The packages remain general caller-layer tools; the formulas in this directory constrain their boundary-wrapped use, not every possible use of those packages. The shallow handler discipline defined in [uring/agents/boundary/protocols.md](../boundary/protocols.md) is restated inside each file for the package it covers: every carrier handles one boundary observation and returns control to the caller. Each runtime file also names the package source evidence and a `CodingObligation_*` predicate so code review can check the guide against the current public package surface. Read the package source named by a file before relying on its facts, following the checklist in [uring/agents/workflow/task-checklists.md](../workflow/task-checklists.md).
 
 ## Reading Order
 

agents/runtime/cove.md

@@ -52,6 +52,13 @@ MonotoneFacts =
   {capability_present, registration_done, terminal_observed}
 NonMonotoneFacts =
   {frontier_live, buffer_owned, fd_open, ring_not_closed, token_live}
+Source_cove =
+  {path("cove/constraint.go"), path("cove/view.go"), path("cove/cmd.go"),
+   path("cove/req.go"), path("cove/req_expr.go"), path("cove/rule.go"),
+   path("cove/rule_expr.go"), path("cove/checked.go"),
+   path("cove/checked_expr.go"), path("cove/step.go"),
+   path("cove/kripke.go"), path("cove/bridge.go")}
+source_checked(Source_cove) ⇔ ∀ f ∈ Source_cove. read_current_source(f)
 World = (MonotoneFactsState, EphemeralFactsState, Requirements, Epoch)
 monotone_facts(w) ⊆ MonotoneFacts
 ephemeral_facts(w) ⊆ NonMonotoneFacts
@@ -92,6 +99,14 @@ GuardedSuspensionView(ctx,s,guard) ⇔
   SuspensionView(ctx,s)
   ∧ guard ∈ Guard
   ∧ guard_holds(ctx,guard)
+CodingObligation_cove(ctx,s,guard,cqe) ⇔
+  source_checked(Source_cove)
+  ∧ GuardedSuspensionView(ctx,s,guard)
+  ∧ support(ContextExtension(ctx,cqe)) ⊆ C
+  ∧ borrowed_cqe_pointer ∉ ContextExtension(ctx,cqe)
+  ∧ ∀ F ∈ NonMonotoneFacts. check_at_use_epoch(F)
+  ∧ ∀ F ∈ NonMonotoneFacts. reject(cache_across(F,suspension_frontier))
+  ∧ project(CtxCarrier ∪ ExprCarrier ∪ KripkeCarrier ∪ {World},B) = ∅
 resume(GuardedSuspensionView(ctx,s,guard),v) →
   requirement_evidence(guard,ctx) ∈ C
 ¬requirements_hold(ctx) → decision_owner({wait, reroute, abandon}) = C