diff --git a/frontend/roslyn/OwnSharp.Extractor/ProtocolLowering.cs b/frontend/roslyn/OwnSharp.Extractor/ProtocolLowering.cs index 35cedcc9..da818355 100644 --- a/frontend/roslyn/OwnSharp.Extractor/ProtocolLowering.cs +++ b/frontend/roslyn/OwnSharp.Extractor/ProtocolLowering.cs @@ -13,6 +13,12 @@ // [ProtocolToken] a ref struct: every instance METHOD is a transition that consumes the // token (and borrows the entity for the call); a PROPERTY is a read. // +// RESERVED NAMES. Matching by name makes the two names a convention the profile owns, but only +// in those shapes: a method marked [ProtocolRegion] that takes a delegate, a ref struct marked +// [ProtocolToken]. An attribute of the same name on anything else (a class, a plain struct, a +// method with no callback) belongs to somebody else's code and is ignored — a scan of a +// codebase that declares no state protocol is never refused over a name. +// // This is a LOWERING, not an analysis. It reads the syntax of one method at a time and looks // symbols up; it never tracks state across statements, never follows aliases, and never // decides whether a program is right. Everything it emits is checked by the core: @@ -93,6 +99,9 @@ private sealed class Ctx public Dictionary Tokens { get; } = new(SymbolEqualityComparer.Default); public HashSet LoweredEntries { get; } = new(); + /// The lambdas that were lowered as region bodies: the only callables in consumer + /// code that may take a token. + public HashSet 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 +127,8 @@ public static Result Lower(Compilation compilation, var model = compilation.GetSemanticModel(tree); var root = tree.GetRoot(); var loweredEntries = new HashSet(); + var loweredBodies = new HashSet(); + var refusedMethods = new List(); foreach (var method in root.DescendantNodes().OfType()) { @@ -189,6 +200,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 @@ -199,9 +211,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()) @@ -481,7 +517,7 @@ bool Outside(INamedTypeSymbol? owner) ? info.ConvertedType : info.Type ?? info.ConvertedType)?.OriginalDefinition; if (IsToken(made) && !Within(api)) refusals.Add(At(file, node, - $"a protocol token '{made!.Name}' is created outside the protocol's own types: a token comes only from a region entry or a transition")); + $"a protocol token '{made!.Name}' is created outside the protocol's own types: a token comes only from a region entry or a transition" + ReservedNames)); else if (node is BaseObjectCreationExpressionSyntax && Bound(model.GetSymbolInfo(node)) is IMethodSymbol { DeclaredAccessibility: not Accessibility.Public } ctor @@ -583,11 +619,37 @@ private static bool HasAttribute(ISymbol? symbol, string name) => symbol is not null && symbol.GetAttributes().Any(a => a.AttributeClass?.Name == name || a.AttributeClass?.Name == name + "Attribute"); - private static bool IsToken(ITypeSymbol? type) => HasAttribute(type, "ProtocolToken"); + // The two attributes are matched by NAME, so the names are reserved — but only in the + // SHAPE the profile gives them. A codebase that never declared a state protocol can own an + // attribute called ProtocolToken (a wire-protocol token class, say), and a name alone must + // not turn its scan into a refusal. So: + // + // 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 not part of a protocol and is left alone. + // The shapes are deliberately the widest ones that still catch a protocol declared wrongly: + // a marked region entry whose callback does not take a token, or takes a marked type that + // is not a ref struct, is still a region entry and is refused where it is used. + + /// Marked [ProtocolToken], whatever it is. Only for saying WHY a marked type is not a token. + private static bool HasTokenName(ITypeSymbol? type) => HasAttribute(type, "ProtocolToken"); + + private static bool IsToken(ITypeSymbol? type) => + type is { IsRefLikeType: true } && HasTokenName(type); + + private static bool IsRegionEntry(IMethodSymbol? method) + { + if (method is null) + return false; + var declared = (method.ReducedFrom ?? method).OriginalDefinition; + // an UNRESOLVED parameter type may be the callback of a degraded scan: keep it in + return HasAttribute(declared, "ProtocolRegion") + && declared.Parameters.Any(p => p.Type.TypeKind is TypeKind.Delegate or TypeKind.Error); + } - private static bool IsRegionEntry(IMethodSymbol? method) => - method is not null && HasAttribute((method.ReducedFrom ?? method).OriginalDefinition, - "ProtocolRegion"); + private const string ReservedNames = + " (the attribute names ProtocolRegion and ProtocolToken are reserved in these shapes: a method marked [ProtocolRegion] that takes a delegate is a region entry, a ref struct marked [ProtocolToken] is a state token)"; private static bool IsApiType(INamedTypeSymbol? type) => type is not null && (IsToken(type) @@ -759,7 +821,7 @@ private static void LowerRegion(Ctx ctx, InvocationExpressionSyntax entry, List< { var args = entry.ArgumentList.Arguments; if (args.Count != 2) - throw Refuse(ctx, entry, "a protocol region entry takes (entity, callback)"); + throw Refuse(ctx, entry, "a protocol region entry takes (entity, callback)" + ReservedNames); var entityExpr = Unparen(args[0].Expression); var entity = ctx.Model.GetSymbolInfo(entityExpr).Symbol; if (entityExpr is not IdentifierNameSyntax || entity is not (ILocalSymbol or IParameterSymbol)) @@ -779,9 +841,9 @@ private static void LowerRegion(Ctx ctx, InvocationExpressionSyntax entry, List< }; if (parameter is null || ctx.Model.GetDeclaredSymbol(parameter) is not IParameterSymbol token - || !IsToken(token.Type)) + || !HasTokenName(token.Type)) throw Refuse(ctx, entry, - "the callback of a protocol region takes exactly one protocol token"); + "the callback of a protocol region takes exactly one protocol token" + ReservedNames); // A token that is not a ref struct can be captured by a nested lambda, stored in a // field, or carried across an await — every one of which lets it reach ANOTHER // region, the shape the core cannot check. The language forbids all three for a @@ -831,6 +893,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, diff --git a/frontend/roslyn/README.md b/frontend/roslyn/README.md index cd7f340f..9c1bb06b 100644 --- a/frontend/roslyn/README.md +++ b/frontend/roslyn/README.md @@ -118,6 +118,18 @@ 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`). +**Reserved names.** Matching by name makes `ProtocolToken` and `ProtocolRegion` +names the profile owns — but only in its own shapes: a **ref struct** marked +`[ProtocolToken]` is a state token, a method marked `[ProtocolRegion]` **that +takes a delegate** is a region entry. An attribute with one of these names on +anything else (a class, a plain struct, a record, a method with no callback) +belongs to somebody else's code and is ignored, so a codebase that declares no +state protocol is not refused over a name. The two shapes themselves stay +reserved: an unrelated attribute of the same name on a ref struct, or on a method +that takes a delegate, is read as a protocol declared wrongly and refused — the +profile cannot tell the two apart, and a mis-declared protocol must not go +unanalysed. + **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 @@ -148,6 +160,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). diff --git a/frontend/roslyn/protocol-samples/refused/R16_token_handed_out_past_a_region_entry.cs.txt b/frontend/roslyn/protocol-samples/refused/R16_token_handed_out_past_a_region_entry.cs.txt new file mode 100644 index 00000000..6d304a7a --- /dev/null +++ b/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 + }); + } +} diff --git a/frontend/roslyn/protocol-samples/refused/R17_token_taken_by_a_local_function.cs.txt b/frontend/roslyn/protocol-samples/refused/R17_token_taken_by_a_local_function.cs.txt new file mode 100644 index 00000000..1b603f09 --- /dev/null +++ b/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); + } +} diff --git a/frontend/roslyn/protocol-samples/refused/expected.json b/frontend/roslyn/protocol-samples/refused/expected.json index 06d8a698..77cdc3a5 100644 --- a/frontend/roslyn/protocol-samples/refused/expected.json +++ b/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", diff --git a/frontend/roslyn/protocol-samples/unrelated/U1_token_name_on_ordinary_types.cs.txt b/frontend/roslyn/protocol-samples/unrelated/U1_token_name_on_ordinary_types.cs.txt new file mode 100644 index 00000000..a2efb48d --- /dev/null +++ b/frontend/roslyn/protocol-samples/unrelated/U1_token_name_on_ordinary_types.cs.txt @@ -0,0 +1,42 @@ +namespace Net.Wire; + +// [ProtocolToken] on everything a state token is NOT: a class, a plain struct, a record, an +// enum, an interface. They are created, copied and passed around like any other value. A +// state token is a REF STRUCT, so none of these is one, and the scan has nothing to say. +[ProtocolToken] +public sealed class SessionToken +{ + public string Value = ""; +} + +[ProtocolToken] +public struct Ticket +{ + public int Id; +} + +[ProtocolToken] +public sealed record Hello(int Version); + +[ProtocolToken] +public enum FrameKind { Data, Control } + +[ProtocolToken] +public interface IFrame +{ + int Size { get; } +} + +public static class U1TokenNameOnOrdinaryTypes +{ + public static int Read(Ticket ticket) => ticket.Id; + + public static int Run(FrameKind kind) + { + var session = new SessionToken { Value = "x" }; + var hello = new Hello((int)kind); + var copy = new Ticket { Id = hello.Version }; + var again = copy; + return Read(again) + session.Value.Length; + } +} diff --git a/frontend/roslyn/protocol-samples/unrelated/U2_region_name_without_a_callback.cs.txt b/frontend/roslyn/protocol-samples/unrelated/U2_region_name_without_a_callback.cs.txt new file mode 100644 index 00000000..e62ed2f5 --- /dev/null +++ b/frontend/roslyn/protocol-samples/unrelated/U2_region_name_without_a_callback.cs.txt @@ -0,0 +1,28 @@ +namespace Net.Wire; + +// [ProtocolRegion] on methods that take no delegate: there is no callback, so there is no +// region body and nothing a region entry could mean. Called from their own class and from +// another one, as a statement and inside an expression. +public static class Frames +{ + [ProtocolRegion] + public static int Parse(byte[] frame) => frame.Length; + + [ProtocolRegion] + public static void Reset(byte[] frame, int offset) + { + frame[offset] = 0; + } + + public static int Own() => Parse(new byte[4]); +} + +public static class U2RegionNameWithoutACallback +{ + public static int Run() + { + var frame = new byte[8]; + Frames.Reset(frame, 0); + return Frames.Parse(frame) + Frames.Own(); + } +} diff --git a/frontend/roslyn/protocol-samples/unrelated/U3_region_name_with_a_callback.cs.txt b/frontend/roslyn/protocol-samples/unrelated/U3_region_name_with_a_callback.cs.txt new file mode 100644 index 00000000..973f0147 --- /dev/null +++ b/frontend/roslyn/protocol-samples/unrelated/U3_region_name_with_a_callback.cs.txt @@ -0,0 +1,29 @@ +using System; + +namespace Net.Wire; + +// THE RESIDUAL, pinned. [ProtocolRegion] on a method that DOES take a delegate has exactly the +// shape of a region entry, and the profile cannot tell it from a protocol whose author forgot +// to mark the token — which must stay a refusal, or a mis-declared protocol would go +// unanalysed in silence. So this collision is still refused; the message says which names are +// reserved and in which shapes. +public static class Bytes +{ + [ProtocolRegion] + public static void Each(byte[] frame, Action body) + { + foreach (var b in frame) + body(b); + } +} + +public static class U3RegionNameWithACallback +{ + public static int Run() + { + var frame = new byte[4]; + var sum = 0; + Bytes.Each(frame, b => { sum += b; }); + return sum; + } +} diff --git a/frontend/roslyn/protocol-samples/unrelated/U4_token_name_on_a_ref_struct.cs.txt b/frontend/roslyn/protocol-samples/unrelated/U4_token_name_on_a_ref_struct.cs.txt new file mode 100644 index 00000000..5576a411 --- /dev/null +++ b/frontend/roslyn/protocol-samples/unrelated/U4_token_name_on_a_ref_struct.cs.txt @@ -0,0 +1,20 @@ +namespace Net.Wire; + +// THE OTHER RESIDUAL, pinned. A REF STRUCT marked [ProtocolToken] is exactly what a state +// token is. Creating one by hand is the forgery the boundary exists to refuse, and the +// profile cannot know that this one belongs to somebody else. Still refused, with the +// reserved-name note. +[ProtocolToken] +public ref struct Cursor +{ + public int Position; +} + +public static class U4TokenNameOnARefStruct +{ + public static int Run() + { + var cursor = new Cursor { Position = 3 }; + return cursor.Position; + } +} diff --git a/frontend/roslyn/protocol-samples/unrelated/WireAttributes.cs.txt b/frontend/roslyn/protocol-samples/unrelated/WireAttributes.cs.txt new file mode 100644 index 00000000..4c8775d8 --- /dev/null +++ b/frontend/roslyn/protocol-samples/unrelated/WireAttributes.cs.txt @@ -0,0 +1,13 @@ +using System; + +namespace Net.Wire; + +// Somebody else's attributes, with the profile's names. A networking library that talks about +// "protocol tokens" and "protocol regions" has every right to them, and has never heard of +// Own.NET. Every program in this directory is scanned WITH this file and WITHOUT the sample +// protocol: it is a codebase that declares no state protocol at all. +[AttributeUsage(AttributeTargets.All)] +public sealed class ProtocolTokenAttribute : Attribute { } + +[AttributeUsage(AttributeTargets.All)] +public sealed class ProtocolRegionAttribute : Attribute { } diff --git a/frontend/roslyn/protocol-samples/unrelated/expected.json b/frontend/roslyn/protocol-samples/unrelated/expected.json new file mode 100644 index 00000000..149e7283 --- /dev/null +++ b/frontend/roslyn/protocol-samples/unrelated/expected.json @@ -0,0 +1,6 @@ +{ + "U1_token_name_on_ordinary_types": null, + "U2_region_name_without_a_callback": null, + "U3_region_name_with_a_callback": "the callback of a protocol region takes exactly one protocol token (the attribute names ProtocolRegion and ProtocolToken are reserved in these shapes", + "U4_token_name_on_a_ref_struct": "a protocol token 'Cursor' is created outside the protocol's own types" +} diff --git a/scripts/protocol_gate.py b/scripts/protocol_gate.py index 213c8f87..88681943 100644 --- a/scripts/protocol_gate.py +++ b/scripts/protocol_gate.py @@ -4,7 +4,7 @@ The Layer 2/3 ledgers freeze the facts the Roslyn lowering emits for the state-protocol surface, and both engines replay them with zero `dotnet`. This script is the other half: it runs the REAL extractor over the C# those facts came from, so a frozen fact can never drift -away from the program it claims to describe. Five questions (needs `dotnet` on PATH; zero +away from the program it claims to describe. Six questions (needs `dotnet` on PATH; zero Python dependencies). Every path below is under `frontend/roslyn/protocol-samples/`: 1. **cases** — every `cases/.cs` is run through the extractor (with the sample API @@ -26,7 +26,15 @@ it all the same: a token made by hand, the protocol's state written past every token. A control with a null expectation must be ACCEPTED: a mention is not an operation. -5. **efcore** — `efcore/` is an ordinary ASP.NET Core + EF Core backend. It must run (its +5. **unrelated** — every `unrelated/.cs.txt` is a program from a codebase that declares + NO state protocol and happens to own attributes named `ProtocolToken` / `ProtocolRegion` + (`unrelated/WireAttributes.cs.txt`). The names are reserved only in the profile's shapes — + a ref struct, a method that takes a delegate — so a case with a null expectation must be + ACCEPTED, with not one region lowered, alone and beside the sample protocol. The two + cases that do have the reserved shape are pinned as refusals: the residual is stated, not + discovered. + +6. **efcore** — `efcore/` is an ordinary ASP.NET Core + EF Core backend. It must run (its acceptance runner drives real HTTP against real SQLite); the extractor must lower its handlers to the committed `tests/fixtures/lowered/typestate_ef_orderbackend.facts.json` with a clean verdict, from the project file alone; a copy whose handlers rely on IMPLICIT @@ -273,6 +281,78 @@ def same_assembly(dll: str, fails: list[str]) -> int: return len(on_disk) +def _lowers_a_region(facts: dict[str, object]) -> bool: + def walk(nodes: object) -> bool: + return isinstance(nodes, list) and any( + isinstance(n, dict) and (n.get("op") == "borrow_mut" or walk(n.get("body")) + or walk(n.get("then")) or walk(n.get("else"))) + for n in nodes) + functions = facts.get("functions") + return isinstance(functions, list) and any( + isinstance(fn, dict) and walk(fn.get("body")) for fn in functions) + + +def unrelated(dll: str, fails: list[str]) -> int: + """A codebase with no state protocol, and attributes that share the profile's names. + + The programs compile on their own (with `WireAttributes.cs.txt`). A null expectation + means the scan must ACCEPT the program — exit 0, a clean verdict, no region lowered — + both alone and with the sample protocol in the same scan; a text means the program has + the reserved shape and the refusal carrying that text is the pinned residual.""" + here = os.path.join(PROTO, "unrelated") + with open(os.path.join(here, "expected.json"), encoding="utf-8") as f: + expected = json.load(f) + shared = "WireAttributes" + on_disk = sorted(n[:-7] for n in os.listdir(here) if n.endswith(".cs.txt") and n[:-7] != shared) + if on_disk != sorted(expected): + fails.append(f"unrelated: expected.json {sorted(expected)} != sources {on_disk}") + return 0 + with tempfile.TemporaryDirectory() as tmp: + one = os.path.join(tmp, "Wire") + os.makedirs(one) + for case in [shared, *on_disk]: + shutil.copyfile(os.path.join(here, f"{case}.cs.txt"), os.path.join(one, f"{case}.cs")) + with open(os.path.join(one, "Wire.csproj"), "w", encoding="utf-8") as f: + f.write(_PROJECT.format(items='')) + built = _run(["dotnet", "build", one, "-nologo", "-v", "q"], cwd=tmp) + if built.returncode != 0: + codes = sorted(set(re.findall(r"error (CS\d+)", built.stdout))) + fails.append(f"unrelated: the programs do not build: {codes}") + attributes = os.path.join(one, f"{shared}.cs") + for case in on_disk: + src = os.path.join(one, f"{case}.cs") + want = expected[case] + scans = [("alone", [attributes, src])] + if want is None: + scans.append(("beside the sample protocol", [API_REL, attributes, src])) + for label, inputs in scans: + out = os.path.join(tmp, f"{case}.json") + if os.path.exists(out): + os.remove(out) + done = _run(["dotnet", dll, *inputs, "--flow-locals", "-o", out]) + where = f"unrelated/{case} ({label})" + if want is None: + if done.returncode != 0: + fails.append(f"{where}: a codebase with no state protocol was not " + f"accepted (exit {done.returncode}): " + f"{done.stderr.strip()[-300:]}") + continue + with open(out, encoding="utf-8") as f: + facts = json.load(f) + got = _verdict(facts) + if got != []: + fails.append(f"{where}: verdict {got!r}, expected clean") + if _lowers_a_region(facts): + fails.append(f"{where}: a region was lowered from a name alone") + elif done.returncode != 2: + fails.append(f"{where}: the extractor exited {done.returncode}; the " + f"reserved shape is pinned as a refusal (2)") + elif want not in done.stderr: + fails.append(f"{where}: refusal text lacks {want!r}: " + f"{done.stderr.strip()[-300:]}") + return len(on_disk) + + EF = os.path.join(PROTO, "efcore") EF_REL = f"{SAMPLES_REL}/efcore/OrderBackend" EF_PROJECT = f"{EF_REL}/OrderBackend.csproj" @@ -502,13 +582,15 @@ def main() -> int: n_refused = refused(dll, fails) n_nocompile = does_not_compile(fails) n_same = same_assembly(dll, fails) + n_unrelated = unrelated(dll, fails) n_ef = efcore(dll, write, fails) n_rust = rust_cli(rust, fails) if rust is not None else 0 for f in fails: print(f"FAIL: {f}") print(f"protocol gate: {n_cases} cases lowered from C# and judged, {n_refused} refused by " f"the lowering, {n_nocompile} rejected by the C# compiler, {n_same} same-assembly " - f"programs held to the boundary, {n_ef} checks on the real " + f"programs held to the boundary, {n_unrelated} programs with the reserved names and " + f"no protocol, {n_ef} checks on the real " f"ASP.NET Core + EF Core backend" + (f", {n_rust} documents byte-identical on both CLIs" if rust else "") + f"; {len(fails)} failure(s)" + (" [fixtures written]" if write else ""))