fix(roslyn): a callback that takes a token outside a region entry is refused

A token exists only inside a region. The lowering held that for methods (a token
parameter is refused) and for locals (a token local outside a region is
refused), and not for the one remaining callable: a lambda or a local function.
Those were read only as the in-place body of a region entry. A callback that
took a token any other way was not lowered at all:

    public static class LetterProtocol
    {
        [ProtocolRegion] public static void WithOpen(Letter l, OpenLetterRegion body) => ...;
        public static void Peek(Letter l, OpenLetterRegion body) => body(new OpenLetter(l));
    }

    LetterProtocol.Peek(letter, open => { open.Seal(); open.Seal(); });

`Peek` is a method of the protocol's own type that is not marked as a region
entry. The declaring type is trusted, so nothing objects to the hand-out; the
callback is consumer code, and it was absent from the facts. Exit 0, a token
spent twice, clean.

Now every lambda and local function in consumer code that takes a token must be
the body of a region entry that was lowered; any other one is a refusal. The
protocol's own types are exempt (they hand tokens out), and a method already
refused does not get a second message for its callbacks.

refused/R16 (a lambda) and refused/R17 (a local function passed as a method
group) pin it; both exit 0 on main's extractor. No committed fact moves: every
lambda in the existing cases is a lowered region body.

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

Author: PhysShell

frontend/roslyn/OwnSharp.Extractor/ProtocolLowering.cs

@@ -93,6 +93,9 @@ private sealed class Ctx
         public Dictionary<ISymbol, (string Name, Region Region)> Tokens { get; } =
             new(SymbolEqualityComparer.Default);
         public HashSet<SyntaxNode> LoweredEntries { get; } = new();
+        /// The lambdas that were lowered as region bodies: the only callables in consumer
+        /// code that may take a token.
+        public HashSet<SyntaxNode> LoweredBodies { get; } = new();
         public int Counter;
         /// How many times the scan has lowered a mention of a borrowed entity. A construct
         /// that runs unknown code is refused UNLESS it moved this counter: then the core
@@ -118,6 +121,8 @@ public static Result Lower(Compilation compilation,
             var model = compilation.GetSemanticModel(tree);
             var root = tree.GetRoot();
             var loweredEntries = new HashSet<SyntaxNode>();
+            var loweredBodies = new HashSet<SyntaxNode>();
+            var refusedMethods = new List<SyntaxNode>();
 
             foreach (var method in root.DescendantNodes().OfType<BaseMethodDeclarationSyntax>())
             {
@@ -189,6 +194,7 @@ public static Result Lower(Compilation compilation,
                             throw new Refused(At(file, v,
                                 $"protocol token '{l.Name}' is declared outside a protocol region"));
                     loweredEntries.UnionWith(ctx.LoweredEntries);
+                    loweredBodies.UnionWith(ctx.LoweredBodies);
 
                     if (ops.Count > 0)
                         functions.Add(new Dictionary<string, object?>
@@ -199,9 +205,33 @@ public static Result Lower(Compilation compilation,
                 catch (Refused r)
                 {
                     refusals.Add(r.Message);
+                    refusedMethods.Add(method);
                 }
             }
 
+            // A token exists only inside a region. A method cannot take one (refused above),
+            // and a lambda or local function may take one only as the in-place body of a
+            // region entry that was lowered. Any other callable with a token parameter is
+            // consumer code that receives a token some other way — from a method of the
+            // protocol's own type that is not marked as a region entry, typically — and that
+            // nothing reads: without this it is simply absent from the facts, and a token
+            // spent twice in it is clean.
+            foreach (var callable in root.DescendantNodes().Where(n =>
+                         n is AnonymousFunctionExpressionSyntax or LocalFunctionStatementSyntax))
+            {
+                if (loweredBodies.Contains(callable)
+                    || refusedMethods.Any(m => m.Span.Contains(callable.Span)))
+                    continue;   // a lowered region body, or inside a method already refused
+                var symbol = callable is LocalFunctionStatementSyntax
+                    ? model.GetDeclaredSymbol(callable) as IMethodSymbol
+                    : model.GetSymbolInfo(callable).Symbol as IMethodSymbol;
+                var taken = symbol?.Parameters.FirstOrDefault(p => IsToken(p.Type));
+                if (taken is null || Enclosing(model, callable).Any(IsApiType))
+                    continue;   // no token; or the protocol's own types, which hand tokens out
+                refusals.Add(At(file, callable,
+                    $"a callback that takes protocol token '{taken.Type.Name}' is not the in-place body of a region entry: a token exists only inside a region, and code that receives one any other way is not analysed"));
+            }
+
             // A region entry outside any method body (an accessor, a field initializer, a
             // top-level statement) is not modelled either.
             foreach (var inv in root.DescendantNodes().OfType<InvocationExpressionSyntax>())
@@ -831,6 +861,7 @@ private static void LowerRegion(Ctx ctx, InvocationExpressionSyntax entry, List<
         if (existing is null)
             ops.Add(Release(owner, line));
         ctx.LoweredEntries.Add(entry);
+        ctx.LoweredBodies.Add(lambda);
     }
 
     private static void LowerTokenLocal(Ctx ctx, ILocalSymbol local, ExpressionSyntax? init,

frontend/roslyn/README.md

@@ -148,6 +148,10 @@ not skipped: the extractor exits `2` and writes no facts, for the whole scan.
 - *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.
+- *Tokens stay in regions.* A lambda or local function that takes a token must be
+  the in-place body of a region entry. A token handed to a callback any other
+  way — by a method of the protocol's own type that is not marked
+  `[ProtocolRegion]`, for one — reaches consumer code nobody lowered.
 - *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).

frontend/roslyn/protocol-samples/refused/R16_token_handed_out_past_a_region_entry.cs.txt

@@ -0,0 +1,48 @@
+using System;
+using Own.Protocols.Sample;
+
+namespace Own.Protocols.Cases;
+
+// A token exists only inside a region. Here the protocol's own type hands one out through a
+// method that is NOT marked as a region entry, so the consumer's callback is not a region
+// body: nothing lowers it, and before this was refused it was simply absent from the facts —
+// a token spent twice, clean. The declaring type is trusted; the callback is consumer code,
+// and consumer code that receives a token is either a lowered region or a refusal.
+public sealed class Letter
+{
+    public bool Sealed { get; private set; }
+
+    internal void MarkSealed() => Sealed = true;
+}
+
+[ProtocolToken]
+public readonly ref struct OpenLetter
+{
+    private readonly Letter _letter;
+    internal OpenLetter(Letter letter) => _letter = letter;
+
+    public void Seal() => _letter.MarkSealed();
+}
+
+public delegate void OpenLetterRegion(OpenLetter open);
+
+public static class LetterProtocol
+{
+    [ProtocolRegion]
+    public static void WithOpen(Letter letter, OpenLetterRegion body) => body(new OpenLetter(letter));
+
+    // the same hand-out, without the mark
+    public static void Peek(Letter letter, OpenLetterRegion body) => body(new OpenLetter(letter));
+}
+
+public static class R16TokenHandedOutPastARegionEntry
+{
+    public static void Run(Letter letter)
+    {
+        LetterProtocol.Peek(letter, open =>
+        {
+            open.Seal();
+            open.Seal();             // a stale token: OWN002 inside a region
+        });
+    }
+}

frontend/roslyn/protocol-samples/refused/R17_token_taken_by_a_local_function.cs.txt

@@ -0,0 +1,47 @@
+using System;
+using Own.Protocols.Sample;
+
+namespace Own.Protocols.Cases;
+
+// The same escape with no lambda at all: a LOCAL FUNCTION that takes the token, passed as a
+// method group to a hand-out that is not a region entry. A method may not take a token; a
+// local function is a method the consumer can write inside a handler.
+public sealed class Crate
+{
+    public bool Shipped { get; private set; }
+
+    internal void MarkShipped() => Shipped = true;
+}
+
+[ProtocolToken]
+public readonly ref struct PackedCrate
+{
+    private readonly Crate _crate;
+    internal PackedCrate(Crate crate) => _crate = crate;
+
+    public void Ship() => _crate.MarkShipped();
+}
+
+public delegate void PackedCrateRegion(PackedCrate packed);
+
+public static class CrateProtocol
+{
+    [ProtocolRegion]
+    public static void WithPacked(Crate crate, PackedCrateRegion body) => body(new PackedCrate(crate));
+
+    public static void Borrow(Crate crate, PackedCrateRegion body) => body(new PackedCrate(crate));
+}
+
+public static class R17TokenTakenByALocalFunction
+{
+    public static void Run(Crate crate)
+    {
+        void Twice(PackedCrate packed)
+        {
+            packed.Ship();
+            packed.Ship();
+        }
+
+        CrateProtocol.Borrow(crate, Twice);
+    }
+}

frontend/roslyn/protocol-samples/refused/expected.json

@@ -5,6 +5,8 @@
   "R13_public_mutator_reaches_protocol_state": "'Doc.Publish' is public and writes 'Published', state the protocol's transitions own",
   "R14_public_setter_of_protocol_state": "'Ticket.State' is public and writes 'State', state the protocol's transitions own",
   "R15_region_opened_inside_protocol_type": "a protocol region is opened inside 'ParcelHandlers', one of the protocol's own types",
+  "R16_token_handed_out_past_a_region_entry": "a callback that takes protocol token 'OpenLetter' is not the in-place body of a region entry",
+  "R17_token_taken_by_a_local_function": "a callback that takes protocol token 'PackedCrate' is not the in-place body of a region entry",
   "R1_default_token": "has no lowerable origin",
   "R2_token_outside_region": "is declared outside a protocol region",
   "R3_return_inside_region": "`return` inside a protocol region",