fix(roslyn): protocol attribute names reserved only in the profile's shapes; a token callback outside a region entry is refused - #388
Merged
Conversation
…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>
…profile's shapes
The state-protocol surface is recognised by two attributes matched by NAME, in
any namespace. That made the names reserved everywhere, and a codebase that
never declared a state protocol could be refused over them — the whole scan,
exit 2, under --flow-locals (the own-check default):
[ProtocolToken] public sealed class SessionToken { ... } // a wire-protocol token
var session = new SessionToken();
-> a protocol token 'SessionToken' is created outside the protocol's own types
Measured on main, with unrelated attributes of those names in another namespace:
a marked class, plain struct, record, enum or interface, and a marked method with
no callback (called from its own class or from another one) — all refused.
The names are now reserved only in the shapes the profile gives them:
a state token is a REF STRUCT marked [ProtocolToken]
a region entry is a method marked [ProtocolRegion] that TAKES A DELEGATE
Anything else carrying one of the names is somebody else's code and is ignored.
The shapes are deliberately the widest that still catch a protocol declared
WRONGLY, and none of those became an acceptance:
* a region entry whose callback takes a marked type that is not a ref struct
— still a region entry, still "must be a ref struct" where it is used;
* a region entry whose token lost its attribute — still a region entry, so the
entity is known and the unmarked type's transition is a boundary violation;
* a region entry with the wrong arity — still refused where it is used;
* a "region entry" with no delegate (a callback interface) — no longer one, and
its type stops being a protocol type, so the token it creates is a token
created outside the protocol;
* a marked non-ref struct forged by hand, with no region in sight — its
transition calls the entity's non-public mutator from outside the protocol.
What changes from a refusal to an acceptance is exactly the unrelated code:
the marked class / plain struct / record / enum / interface, and the marked
method without a delegate.
Two collisions keep the reserved shape and stay refused, with a message that
now says which names are reserved and in which shapes: an unrelated ref struct
marked [ProtocolToken], and an unrelated method marked [ProtocolRegion] that
takes a delegate. The profile cannot tell either from a protocol declared
wrongly, and a mis-declared protocol must not go unanalysed.
scripts/protocol_gate.py gains the `unrelated` stage: programs from a codebase
with no state protocol and attributes of these names. The two that are not in a
reserved shape must be accepted with not one region lowered, alone and beside
the sample protocol; the two that are, are pinned as refusals. On main's
extractor the stage fails on the first two.
No committed fact moves, and the extractor's output on every C# input CI scans
is byte-identical to main's (256 of 256).
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Что и зачем
Два изменения в распознавании state-протоколов, двумя коммитами.
1. Имена атрибутов зарезервированы только в форме профиля.
[ProtocolToken]и[ProtocolRegion]распознаются по имени в любом пространстве имён. Из-за этого кодовая база, которая никогда не объявляла state-протокол, но имеет одноимённые атрибуты, получала отказ всего скана (exit 2 под--flow-locals, то есть по умолчанию вown-check):Теперь токен — это
ref structс[ProtocolToken], вход в регион — метод с[ProtocolRegion], принимающий делегат. Всё остальное с этими именами чужое и игнорируется.Формы выбраны самыми широкими из тех, что ещё ловят протокол, объявленный с ошибкой. Ни одна авторская ошибка не стала принятием: токен без
ref, токен без атрибута, неверная арность входа, callback через интерфейс, не-refтокен, подделанный вручную, — всё по-прежнему отказ.Из отказа в принятие перешёл только чужой код: атрибут
ProtocolTokenна классе, обычной структуре, записи, перечислении, интерфейсе; атрибутProtocolRegionна методе без делегата.Две коллизии остаются отказом, потому что имеют зарезервированную форму и неотличимы от протокола, объявленного с ошибкой: чужой
ref structс[ProtocolToken]и чужой метод с[ProtocolRegion]и делегатом. Они закреплены в gate, сообщение теперь называет зарезервированные имена и формы.2. Callback с токеном вне входа в регион — отказ. Найдено при замерах для п. 1. Токен существует только внутри региона; это держалось для методов и локалей, но не для лямбд и локальных функций. Если тип протокола выдаёт токен через метод, не помеченный
[ProtocolRegion], лямбда потребителя не понижалась вовсе: дважды потраченный токен, exit 0, чисто. Теперь лямбда или локальная функция с параметром-токеном в коде потребителя обязана быть телом пониженного входа в регион.Закоммиченные факты не меняются. Вывод экстрактора на всех C#-входах, которые сканирует CI, побайтово совпадает с
main.Тип изменения
Как проверено
python tests/run_tests.pyruff check .иmypypython scripts/<...>.py --selftest)На закоммиченной ветке, свежий Linux-клон (
dotnet8.0.422 и 9.0.315,ruff 0.15.8,mypy 1.19.1), и на Windows.python scripts/protocol_gate.py --rust <own-cli>: 18 программ понижены и оценены, 17 отклонены lowering, 5 отклонены компилятором, 5 «одна сборка», 4 программы с зарезервированными именами без протокола, 24 проверки бэкенда; 0 провалов. Новая стадияunrelated: две программы приняты (ни одного региона не понижено, отдельно и рядом с образцовым протоколом), две закреплены отказом.main: 256 выводов (каждый C#-вход из CI и фикстуры OWN053; с--flow-localsи без; с--fix-candidatesи без) — 256 побайтово идентичны.python tests/run_tests.py— exit 0; 15 реестров эталонов в синхроне;cargo fmt --check,cargo clippy --all-targets— exit 0;cargo test --no-fail-fast— 288/0; паритет CLI наtypestate_*— 37/37.C# leak extractor (Roslyn) -> OwnIR -> core, шаги как написаны вci.yml: все exit 0.1a26aa63fd5f,mergegate_ci.pyна симулированном merge — allowed.--fix-candidatesON/OFF — без изменений.Отрицательные контроли: на экстракторе
mainстадияunrelatedпадает на обеих принимаемых программах (обе отклонены), аrefused/R16иrefused/R17дают exit 0.Не проверено: остальные job CI локально не гонялись; коллизии имён на реальных сторонних кодовых базах не искались — замеры сделаны на синтетических программах.
Связанные issue
Отдельного issue нет. Follow-up после #385 (распознавание по имени) и находка при его замерах.
Чеклист
feat:,fix:,docs:…)Документация:
frontend/roslyn/README.md— абзац «Reserved names» и пункт «Tokens stay in regions» в списке отказов; шапкаProtocolLowering.cs.🤖 Generated with Claude Code