docs(roslyn): the trust boundary is part of the profile's soundness model

The previous commit refused a region opened inside a type that declares the
protocol, and documented it as one more thing the extractor refuses. That
undersells what it is. The declaring types are the profile's trusted
definition surface — token construction, region entry, transition plumbing —
and everything else is the analysed surface. A type is one or the other, never
both, because consumer code inside a declaring type is not a violation the core
missed: it is a program the core never saw.

The README states that as the model, next to what the profile claims, and the
refusal list points at it. The lowering's header says the same. No behaviour
changes: comments and prose only.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>

Author: PhysShell

frontend/roslyn/OwnSharp.Extractor/ProtocolLowering.cs

@@ -30,6 +30,13 @@
 // update, a change-tracker metadata write, raw SQL, another process. Those belong to
 // concurrency tokens, constraints and transactions.
 //
+// THE TRUST BOUNDARY. The types that DECLARE a protocol (the tokens, the type holding a
+// region entry) are the trusted definition surface: token construction, region entry and
+// transition plumbing live there, and their bodies are not lowered. Everything else is
+// consumer code — the analysed surface. A type is one or the other, never both: consumer code
+// inside a declaring type would simply be absent from the analysed program, so a region
+// opened there is refused rather than guessed about.
+//
 // OUTSIDE a region nothing protocol-relevant is live, and a region lowers to a self-contained
 // unit (the entity is acquired and released around it). So whatever surrounds a region —
 // `try`/`catch`, `using`, a loop, a branch, `await` — is walked through and ignored.
@@ -118,10 +125,11 @@ public static Result Lower(Compilation compilation,
                     continue;
                 if (IsApiType(msym.ContainingType))
                 {
-                    // The protocol's own types are TRUSTED: their bodies implement the
-                    // protocol and are not lowered. So a region OPENED in one of them — a
-                    // handler written next to the region entry it calls — would never be
-                    // analysed and would read as clean. Trusted is not the same as checked.
+                    // The trust boundary (see the header): a declaring type's bodies
+                    // implement the protocol and are not lowered. So a region OPENED in one
+                    // of them — a handler written next to the region entry it calls — would
+                    // not be a violation the core missed but a program it never saw, and
+                    // would read as clean. Trusted is not the same as checked.
                     foreach (var opened in method.DescendantNodes().OfType<InvocationExpressionSyntax>()
                                  .Where(i => IsRegionEntry(MethodOf(model, i))))
                         refusals.Add(At(file, opened,

frontend/roslyn/README.md

@@ -118,6 +118,16 @@ SQL, another process. Those belong to concurrency tokens, constraints and
 transactions (two of them are pinned as stated limits under
 `protocol-samples/efcore/known-gaps`).
 
+**The trust boundary.** The types that DECLARE a protocol — the tokens, and the
+type holding a region entry — are its trusted definition surface: they construct
+tokens, enter regions and implement transitions, and their bodies are not
+lowered. Everything else is consumer code, and consumer code is what the profile
+analyses. A type is one or the other, never both. A handler written inside a
+declaring type would not be a violation the core missed; it would be a program
+the core never saw, and it would read as clean. So a region opened inside a
+declaring type is refused, and the profile does not try to guess which method of
+such a type is plumbing and which is a business handler.
+
 **Refusals.** A recognised protocol construct that cannot be lowered safely is
 not skipped: the extractor exits `2` and writes no facts, for the whole scan.
 
@@ -135,10 +145,9 @@ not skipped: the extractor exits `2` and writes no facts, for the whole scan.
   `nameof`, `typeof` and reads are mentions, not operations.
 - *Source.* The protocol and its entity must be in the scan as source; one that
   arrives only as a compiled reference cannot be admitted.
-- *Trusted types.* The types that declare a protocol (the tokens, the class
-  holding a region entry) implement it and are not analysed as user code. A
-  region opened inside one of them is refused rather than skipped: write the
-  code that uses a protocol outside the types that declare it.
+- *Trust boundary.* A region opened inside a type that declares the protocol
+  (see above): write the code that uses a protocol outside the types that
+  declare it.
 - *Binding.* The scan does not read `obj/`, so usings a project only gets
   **implicitly** are not there. A region whose entity does not bind is refused;
   write the usings out in the files that open regions (or qualify the names).