|
4 | 4 | The Layer 2/3 ledgers freeze the facts the Roslyn lowering emits for the state-protocol |
5 | 5 | surface, and both engines replay them with zero `dotnet`. This script is the other half: it |
6 | 6 | runs the REAL extractor over the C# those facts came from, so a frozen fact can never drift |
7 | | -away from the program it claims to describe. Five questions (needs `dotnet` on PATH; zero |
| 7 | +away from the program it claims to describe. Six questions (needs `dotnet` on PATH; zero |
8 | 8 | Python dependencies). Every path below is under `frontend/roslyn/protocol-samples/`: |
9 | 9 |
|
10 | 10 | 1. **cases** — every `cases/<Case>.cs` is run through the extractor (with the sample API |
|
26 | 26 | it all the same: a token made by hand, the protocol's state written past every token. A |
27 | 27 | control with a null expectation must be ACCEPTED: a mention is not an operation. |
28 | 28 |
|
29 | | -5. **efcore** — `efcore/` is an ordinary ASP.NET Core + EF Core backend. It must run (its |
| 29 | +5. **unrelated** — every `unrelated/<Case>.cs.txt` is a program from a codebase that declares |
| 30 | + NO state protocol and happens to own attributes named `ProtocolToken` / `ProtocolRegion` |
| 31 | + (`unrelated/WireAttributes.cs.txt`). The names are reserved only in the profile's shapes — |
| 32 | + a ref struct, a method that takes a delegate — so a case with a null expectation must be |
| 33 | + ACCEPTED, with not one region lowered, alone and beside the sample protocol. The two |
| 34 | + cases that do have the reserved shape are pinned as refusals: the residual is stated, not |
| 35 | + discovered. |
| 36 | +
|
| 37 | +6. **efcore** — `efcore/` is an ordinary ASP.NET Core + EF Core backend. It must run (its |
30 | 38 | acceptance runner drives real HTTP against real SQLite); the extractor must lower its |
31 | 39 | handlers to the committed `tests/fixtures/lowered/typestate_ef_orderbackend.facts.json` |
32 | 40 | 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: |
273 | 281 | return len(on_disk) |
274 | 282 |
|
275 | 283 |
|
| 284 | +def _lowers_a_region(facts: dict[str, object]) -> bool: |
| 285 | + def walk(nodes: object) -> bool: |
| 286 | + return isinstance(nodes, list) and any( |
| 287 | + isinstance(n, dict) and (n.get("op") == "borrow_mut" or walk(n.get("body")) |
| 288 | + or walk(n.get("then")) or walk(n.get("else"))) |
| 289 | + for n in nodes) |
| 290 | + functions = facts.get("functions") |
| 291 | + return isinstance(functions, list) and any( |
| 292 | + isinstance(fn, dict) and walk(fn.get("body")) for fn in functions) |
| 293 | + |
| 294 | + |
| 295 | +def unrelated(dll: str, fails: list[str]) -> int: |
| 296 | + """A codebase with no state protocol, and attributes that share the profile's names. |
| 297 | +
|
| 298 | + The programs compile on their own (with `WireAttributes.cs.txt`). A null expectation |
| 299 | + means the scan must ACCEPT the program — exit 0, a clean verdict, no region lowered — |
| 300 | + both alone and with the sample protocol in the same scan; a text means the program has |
| 301 | + the reserved shape and the refusal carrying that text is the pinned residual.""" |
| 302 | + here = os.path.join(PROTO, "unrelated") |
| 303 | + with open(os.path.join(here, "expected.json"), encoding="utf-8") as f: |
| 304 | + expected = json.load(f) |
| 305 | + shared = "WireAttributes" |
| 306 | + on_disk = sorted(n[:-7] for n in os.listdir(here) if n.endswith(".cs.txt") and n[:-7] != shared) |
| 307 | + if on_disk != sorted(expected): |
| 308 | + fails.append(f"unrelated: expected.json {sorted(expected)} != sources {on_disk}") |
| 309 | + return 0 |
| 310 | + with tempfile.TemporaryDirectory() as tmp: |
| 311 | + one = os.path.join(tmp, "Wire") |
| 312 | + os.makedirs(one) |
| 313 | + for case in [shared, *on_disk]: |
| 314 | + shutil.copyfile(os.path.join(here, f"{case}.cs.txt"), os.path.join(one, f"{case}.cs")) |
| 315 | + with open(os.path.join(one, "Wire.csproj"), "w", encoding="utf-8") as f: |
| 316 | + f.write(_PROJECT.format(items='<Compile Include="*.cs" />')) |
| 317 | + built = _run(["dotnet", "build", one, "-nologo", "-v", "q"], cwd=tmp) |
| 318 | + if built.returncode != 0: |
| 319 | + codes = sorted(set(re.findall(r"error (CS\d+)", built.stdout))) |
| 320 | + fails.append(f"unrelated: the programs do not build: {codes}") |
| 321 | + attributes = os.path.join(one, f"{shared}.cs") |
| 322 | + for case in on_disk: |
| 323 | + src = os.path.join(one, f"{case}.cs") |
| 324 | + want = expected[case] |
| 325 | + scans = [("alone", [attributes, src])] |
| 326 | + if want is None: |
| 327 | + scans.append(("beside the sample protocol", [API_REL, attributes, src])) |
| 328 | + for label, inputs in scans: |
| 329 | + out = os.path.join(tmp, f"{case}.json") |
| 330 | + if os.path.exists(out): |
| 331 | + os.remove(out) |
| 332 | + done = _run(["dotnet", dll, *inputs, "--flow-locals", "-o", out]) |
| 333 | + where = f"unrelated/{case} ({label})" |
| 334 | + if want is None: |
| 335 | + if done.returncode != 0: |
| 336 | + fails.append(f"{where}: a codebase with no state protocol was not " |
| 337 | + f"accepted (exit {done.returncode}): " |
| 338 | + f"{done.stderr.strip()[-300:]}") |
| 339 | + continue |
| 340 | + with open(out, encoding="utf-8") as f: |
| 341 | + facts = json.load(f) |
| 342 | + got = _verdict(facts) |
| 343 | + if got != []: |
| 344 | + fails.append(f"{where}: verdict {got!r}, expected clean") |
| 345 | + if _lowers_a_region(facts): |
| 346 | + fails.append(f"{where}: a region was lowered from a name alone") |
| 347 | + elif done.returncode != 2: |
| 348 | + fails.append(f"{where}: the extractor exited {done.returncode}; the " |
| 349 | + f"reserved shape is pinned as a refusal (2)") |
| 350 | + elif want not in done.stderr: |
| 351 | + fails.append(f"{where}: refusal text lacks {want!r}: " |
| 352 | + f"{done.stderr.strip()[-300:]}") |
| 353 | + return len(on_disk) |
| 354 | + |
| 355 | + |
276 | 356 | EF = os.path.join(PROTO, "efcore") |
277 | 357 | EF_REL = f"{SAMPLES_REL}/efcore/OrderBackend" |
278 | 358 | EF_PROJECT = f"{EF_REL}/OrderBackend.csproj" |
@@ -502,13 +582,15 @@ def main() -> int: |
502 | 582 | n_refused = refused(dll, fails) |
503 | 583 | n_nocompile = does_not_compile(fails) |
504 | 584 | n_same = same_assembly(dll, fails) |
| 585 | + n_unrelated = unrelated(dll, fails) |
505 | 586 | n_ef = efcore(dll, write, fails) |
506 | 587 | n_rust = rust_cli(rust, fails) if rust is not None else 0 |
507 | 588 | for f in fails: |
508 | 589 | print(f"FAIL: {f}") |
509 | 590 | print(f"protocol gate: {n_cases} cases lowered from C# and judged, {n_refused} refused by " |
510 | 591 | f"the lowering, {n_nocompile} rejected by the C# compiler, {n_same} same-assembly " |
511 | | - f"programs held to the boundary, {n_ef} checks on the real " |
| 592 | + f"programs held to the boundary, {n_unrelated} programs with the reserved names and " |
| 593 | + f"no protocol, {n_ef} checks on the real " |
512 | 594 | f"ASP.NET Core + EF Core backend" |
513 | 595 | + (f", {n_rust} documents byte-identical on both CLIs" if rust else "") |
514 | 596 | + f"; {len(fails)} failure(s)" + (" [fixtures written]" if write else "")) |
|
0 commit comments