From cf7eb01bee0607b2b6e084b2239fe9e4921d5328 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 3 Oct 2026 16:54:03 +0000 Subject: [PATCH 1/4] docs(tb-mvp): TB-MVP-01 preregistration (base 877ee69f) Registers the Typed Builder + ASP.NET Core + EF Core Order vertical slice before any product code: kill-first answers read off the base, exact layout, entity, persisted state, generated API, refinement boundary, raw-entity contract, HTTP contract, corpus with expected results, hostile controls H1-H18, official run order and the acceptance verdict. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_011ZFvhLx1fM9Gerg4dKsZcL --- docs/notes/tb-mvp-01-preregistration.md | 436 ++++++++++++++++++++++++ 1 file changed, 436 insertions(+) create mode 100644 docs/notes/tb-mvp-01-preregistration.md diff --git a/docs/notes/tb-mvp-01-preregistration.md b/docs/notes/tb-mvp-01-preregistration.md new file mode 100644 index 00000000..3ef58e2f --- /dev/null +++ b/docs/notes/tb-mvp-01-preregistration.md @@ -0,0 +1,436 @@ +# TB-MVP-01 — Typed Builder + ASP.NET Core + EF Core Order vertical slice: preregistration + +**STATUS: REGISTERED BEFORE ANY PRODUCT CODE.** This commit holds only this document. +Everything below is binding on the implementation commit and on the official run. A +semantic change after this commit is an amendment, committed before the affected rerun. + +**Base:** `main` = `877ee69f28ba169c1fd68935b41f4ef26d92f186` (merge of #390: OwnIR v2, +`proven_call`, H0 heap-effect summaries consumed by the core, T0 Amendment 2). H1 is in +`main`: `git merge-base --is-ancestor 450c39b4f79124a7a5ba169868dd768aaab8d37f 877ee69f` holds. + +## P0 — accepted gates on the base + +Run on `877ee69f` before this document was committed. Results are recorded in +§ *P0 results* at the end. + +## P2 — kill-first answers, read off the current codebase + +Each answer names the code or a probe run on the base. A probe is a throwaway copy, not part +of the repository. + +1. **What Typed Builder / generator / runtime pieces exist?** + - **The state-protocol profile** (P-010 pillar 9, first slice): + - `[ProtocolToken]` ref struct tokens and `[ProtocolRegion]` region entries, matched by name; + - the Roslyn lowering, `frontend/roslyn/OwnSharp.Extractor/ProtocolLowering.cs`, to `borrow_mut`, `move` and `proven_call`; + - the boundary and admission checks; + - core verdicts OWN002 (stale), OWN005 (copy) and OWN013 (raw entity in a region) on both engines. + - **A hand-written EF Core backend**, `frontend/roslyn/protocol-samples/efcore`, pinned by `scripts/protocol_gate.py`. + - **No generator exists.** P-010 says so: "What the slice does not have: a declared state graph …, a generator for the tokens, the affine view of a token (an unspent one is OWN001 today)". The efcore sample's `OrderProtocol.cs` says "written by hand (a source generator could emit this file; none exists yet)". + - **No builder exists.** +2. **The accepted protocol annotation and API.** + - A state is a `readonly ref struct` marked `[ProtocolToken]`, holding the entity. + - A transition is an instance METHOD on the token. It consumes the token. A property is a read. + - A region entry is a static method marked `[ProtocolRegion]` taking `(entity, delegate)`. It checks the runtime state, then hands the token to an in-place lambda. + - The attributes are matched by name (`frontend/roslyn/README.md`, *State protocols*). +3. **Can a typed state view refer to the same entity without copying?** Yes. A token is a `readonly ref struct` with one `private readonly Order _order` field. It is constructed from the region entry's own `order` argument, so a transition writes that instance. +4. **Can EF keep tracking that exact entity?** Yes. The efcore acceptance checks `ef-same-instance`, `ef-change-tracked`, `ef-no-reattach` and `ef-saved` against real SQLite on the base (13/13 checks in `protocol_gate.py`). +5. **Can a valid transition change persisted state and keep the ownership guarantees?** Yes. The token writes the tracked instance, and `SaveChangesAsync` emits an ordinary `UPDATE` (efcore check `ef-update-emitted`). Inside the region, the core holds exclusivity: the `borrow_mut` lowering, OWN013 for a raw mention. +6. **Can an EF-loaded entity be refined from runtime state into a typed state?** Yes, at the region entry: a runtime check of the state, then the token. One defect sits under it, found by a probe: + - EF Core 8's `HasConversion()` throws on `'Bogus'`; + - but it maps `'7'` to the undefined value `(OrderStatus)7`; + - and it maps `'approved'` case-insensitively to `Approved`. + + The last is a fabricated valid state. So the registration below uses a **strict** converter. In the probe, a converter that throws a custom exception propagated **unwrapped** out of `Single`/`SingleOrDefaultAsync`. +7. **Can stale typed state be rejected after a transition?** Yes, statically: the core gives OWN002 for use after a transition (case `L1_stale_capability`) and OWN005 for a copy (`L2_copied_capability`). +8. **Do ordinary DbSet/LINQ queries stay ordinary?** Yes. No custom provider is involved: the efcore check `ef-query-translated` gives a server-side `WHERE`. + +**Two facts bind the API shape, both read off the core on the base by probe.** They are +accepted semantics, not things this MVP changes. + +- **F1 — tokens are linear, not affine.** + - A transition result bound to a named local and never spent is OWN001 (case `G6_capability_not_spent`). + - The same result discarded as an expression statement (`draft.Submit(now);`) is not acquired, so it is clean. The chained form `draft.Submit().Approve()` (case `L6b`) is clean too. + - `_ = draft.Submit(now);` is **refused** by the lowering: "'_' (Discard) inside a protocol region is not modelled". +- **F2 — H1 works in a real project scan.** In a probe copy of the efcore backend, a pure static `int` helper called inside a region: + - as a statement, or nested in a transition's argument list (`approved.Ship(Clock.Same(now))`), lowered to `proven_call`; + - had its site record and callee record in `heap_effects`; + - was admitted by the core: verdict clean. + +**Also read off the extractor**, `Program.cs::IsGenerated`: the input scan **skips** `*.g.cs`, +`*.Designer.cs` and `*.AssemblyInfo.cs`. A Roslyn source generator's output never reaches +the scan at all: it lives in the compilation, not on disk. The profile, though, requires the +protocol in the scan **as source** ("one that arrives only as a compiled reference cannot be +admitted"). This decides the generator policy below. + +No question has the answer "impossible". No STOP verdict applies at registration. + +## Layout (exact) + +``` +samples/OrderBackend/ + README.md developer workflow (P29) + nuget.config nuget.org only + .gitignore bin/ obj/ + OrderBackend/ the ASP.NET Core minimal API (Microsoft.NET.Sdk.Web) + OrderBackend.csproj net8.0, C# 12, Microsoft.EntityFrameworkCore.Sqlite 8.0.11 + Program.cs composition root (`Backend.Build`) + `Program` + OrderEndpoints.cs the handlers: no attribute, no reflection + Shipping.cs the harmless helper used inside a region (P19) + Domain/TypedBuilder.cs the marker attributes (hand-written, matched by name) + Domain/Order.cs the annotated entity + its state enum (hand-written input) + Domain/Order.Protocol.cs GENERATED, committed (see Generator) + Data/OrdersDb.cs the DbContext + Acceptance/ console runner: real Kestrel + real SQLite + oracles + corpus/ + positive/.cs.txt + expected.json + negative/.cs.txt + expected.json + limits/.cs.txt + expected.json characterized limits, pinned (not failures) + evidence/ written by the gate with --write, verified otherwise +frontend/roslyn/Own.TypedBuilder/ the generator: a console tool (Microsoft.CodeAnalysis.CSharp 4.9.2) +scripts/typed_builder_gate.py the one gate: every acceptance step below, in order +``` + +Top-level `samples/` is new. It is not under `examples/`, which the #260 shadow sweep +scans as one document, nor under `frontend/roslyn/samples`, which other gates glob. +`frontend/roslyn/protocol-samples/efcore` stays **untouched**: it is the profile's pinned +fixture, and this is the product sample. + +## Domain entity (exact) + +One EF entity, `OrderBackend.Domain.Order`: `public sealed partial class`, no base class, no +interface, materialized through a private parameterless constructor. + +| member | type | notes | +|---|---|---| +| `Id` | `int` | key, private setter, SQLite autoincrement | +| `Customer` | `string` | **required construction field** (`[BuilderRequired]`), private setter | +| `Status` | `OrderStatus` | **the protocol state** (`[ProtocolState]`), private setter | +| `SubmittedAt` / `ApprovedAt` / `ShippedAt` | `DateTime?` | written by the transitions | +| `TrackingNumber` | `int?` | written by Ship | + +`enum OrderStatus { Draft, Submitted, Approved, Shipped }`. + +**Persisted state:** column `Status`, `TEXT`, holding the exact member name (`"Draft"` …). +It goes through a **strict** converter, which is generated: `OrderStatusStorage.ToStore` +/ `FromStore`, wired with `HasConversion(...)`. +- `FromStore` accepts the four canonical names only (ordinal, case-sensitive). Anything else throws `CorruptOrderStateException(raw)`: `"Bogus"`, `"7"`, `"approved"`, `""`. +- `ToStore` of an undefined value throws too. +- No member is ever fabricated: no default, no case folding, no numeric parse. + +No per-state entity classes, no parallel persistence hierarchy: one `Orders` table, one +identity. + +## Declaration (the generator's input, hand-written) + +```csharp +[TypedProtocol] +public sealed partial class Order +{ + [BuilderRequired] public string Customer { get; private set; } = ""; + [ProtocolState] public OrderStatus Status { get; private set; } + + [Transition("Submit", OrderStatus.Draft, OrderStatus.Submitted)] + private void OnSubmit(DateTime at) => SubmittedAt = at; + [Transition("Approve", OrderStatus.Submitted, OrderStatus.Approved)] + private void OnApprove(DateTime at) => ApprovedAt = at; + [Transition("Ship", OrderStatus.Approved, OrderStatus.Shipped)] + private void OnShip(DateTime at, int trackingNumber) { ShippedAt = at; TrackingNumber = trackingNumber; } +} +``` + +A transition's hook writes only the transition's business data. **The state write is the +generator's**: the hook cannot set the wrong next state, because it does not set the state at +all. + +## Generated public API (exact) + +All of it is in `Domain/Order.Protocol.cs`, namespace `OrderBackend.Domain`. From the +declaration above: + +| generated | shape | +|---|---| +| `partial class Order` | `internal void ApplySubmit(DateTime at)` (calls `OnSubmit(at)`, then `Status = Submitted`), likewise `ApplyApprove`, `ApplyShip`; `public static Order.Builder.CustomerStep Create()` | +| `Order.Builder.CustomerStep` | `sealed class`, private ctor: `public Order.Builder.Ready Customer(string customer)` (null → `ArgumentNullException`) | +| `Order.Builder.Ready` | `sealed class`, private ctor: `public Order Build()`, which creates `new Order { Customer = …, Status = OrderStatus.Draft }` | +| `[ProtocolToken] DraftOrder` | `readonly ref struct`, `internal` ctor: `int Id { get; }`; `SubmittedOrder Submit(DateTime at)` | +| `[ProtocolToken] SubmittedOrder` | `int Id`; `ApprovedOrder Approve(DateTime at)` | +| `[ProtocolToken] ApprovedOrder` | `int Id`; `ShippedOrder Ship(DateTime at, int trackingNumber)` | +| `[ProtocolToken] ShippedOrder` | `int Id`; **no method** | +| delegates | `DraftRegion(DraftOrder)`, `SubmittedRegion(SubmittedOrder)`, `ApprovedRegion(ApprovedOrder)` | +| `static class OrderProtocol` | `[ProtocolRegion] WithDraft(Order, DraftRegion)`, `WithSubmitted(Order, SubmittedRegion)`, `WithApproved(Order, ApprovedRegion)`. No `WithShipped`: a state with no outgoing transition gets no region, because its token could never be spent (F1) | +| `InvalidOrderStateException` | `(int Id, OrderStatus Actual, OrderStatus Required)` : `InvalidOperationException` | +| `CorruptOrderStateException` | `(string Raw)` : `InvalidOperationException` | +| `static class OrderStatusStorage` | `ToStore` / `FromStore` (above) | + +- **Invalid transitions are absent.** `DraftOrder` has no `Approve` and no `Ship`, and no generated member throws "invalid transition". C1–C7 are C# compiler errors. +- **Transition return.** A transition returns the next token over the **same** `_order`. Linear tokens (F1) fix two consequences: + - A next token bound to a named local must be spent. A token the handler does not use further is discarded as an expression statement: `draft.Submit(now);`. + - `ShippedOrder shipped = approved.Ship(…);` is OWN001 under the accepted core. This is pinned as limit **K1**, not "fixed": affine tokens are foundation work (G6), out of scope here. + +## Refinement boundary (exact) + +The region entries are the only path from a raw `Order` to a token: +1. `OrderProtocol.WithX(order, x => …)` checks `order` is not null; +2. it checks `order.Status == X`, else throws `InvalidOrderStateException(order.Id, order.Status, X)`; +3. it calls the lambda with `new XOrder(order)`. + +- **No unchecked cast exists.** A token's constructor is `internal`. Creating one anywhere outside the generated protocol types is refused by the lowering's boundary check (`ForgedToken` shape), and also by the C# compiler from a second assembly. +- **Corrupt persisted state never reaches refinement.** It fails at materialization with `CorruptOrderStateException`. +- **An in-memory undefined value** (`(OrderStatus)7`) never equals a required state, so refinement throws `InvalidOrderStateException`. Never a token. + +## Ownership, lifetime, stale state + +These are the accepted semantics, unchanged: +- Inside `WithX` the entity is exclusively borrowed (`borrow_mut`). +- The token is a linear capability. A transition moves it: use after a transition is OWN002, a copy is a move (OWN005). +- A token cannot leave the region. It is a ref struct, the C# compiler forbids capture by a nested lambda or a field, and the lowering refuses `return`, helpers that take a token, and local functions. +- There is no runtime "used" flag anywhere: stale use is a static rejection only. + +## Raw entity contract (P8): chosen direction + +**The raw entity may exist, but every state-changing write is rejected.** +1. **Admission.** Nothing public on `Order` writes the protocol-owned state (`Status`, `SubmittedAt`, `ApprovedAt`, `ShippedAt`, `TrackingNumber`): private setters, `internal` `Apply*`, private `On*` hooks. A public mutator would make the lowering refuse the protocol. +2. **Outside a region.** Calling `Apply*` / `On*` or writing a private setter is refused: + - by the lowering's boundary check (`'ApplyShip' of 'Order' is not public and belongs to a state protocol`) in the same assembly; + - and, for private members, by the C# compiler. +3. **Inside a region.** Any mention of the raw entity is OWN013. + +**Stated limits, outside the claim** (the same as the profile's): +- writes that bypass the entity's C# surface: `ExecuteUpdate`, `Entry(order).Property("Status").CurrentValue = …`, raw SQL; +- reflection, `unsafe`; +- another process. + +`ExecuteUpdate` is pinned in `corpus/limits` as **K2**. + +**Threat model (P23).** Ordinary C# in the scanned project, written by a developer who calls +public and internal APIs. Not malicious reflection, IL rewriting, or the database itself. + +## EF tracking semantics + +Handlers load with an ordinary tracked query, `db.Orders.SingleOrDefaultAsync(o => o.Id == id, ct)`. +The token writes that instance. `SaveChangesAsync` detects the change (snapshot tracking, no +proxies) and writes one `UPDATE`. + +**Identity proof (P4, registered equivalent).** The token's field is private and a ref +struct cannot be boxed, so `ReferenceEquals(entity, token._order)` cannot be evaluated by an +oracle that does not breach the API. The registered proof has four parts: +- (a) **structural**: the generated region entry constructs each token from its own `order` argument, and each transition from its own `_order`, never a copy or a new `Order`. The gate checks the generated syntax; +- (b) **behavioural**: `ReferenceEquals(entry.Entity, order)` holds before and after the region, and `ChangeTracker.Entries().Count() == 1` holds throughout; +- (c) **observed**: `entry.State == Modified`, and exactly the transition's properties are `IsModified`, with `Customer` unmodified; +- (d) **persisted**: after `SaveChangesAsync`, a separate raw SQL connection reads the new state. + +## HTTP contract (exact) + +| request | success | errors | +|---|---|---| +| `POST /orders`, JSON `{"customer":"…"}` | `201`, `Location: /orders/{id}`, `{"id":N,"status":"Draft"}` | blank or missing customer: `400 {"error":"customer_required"}` | +| `POST /orders/{id}/submit` | `200 {"id":N,"status":"Submitted"}` | see below | +| `POST /orders/{id}/approve` | `200 {"id":N,"status":"Approved"}` | | +| `POST /orders/{id}/ship` | `200 {"id":N,"status":"Shipped","trackingNumber":T}` | | +| `GET /orders/{id}` | `200 {"id","customer","status","submittedAt","approvedAt","shippedAt","trackingNumber"}` | | +| `GET /orders?status=S` | `200 [{"id","customer"}…]`, ordered by id (ordinary LINQ: `Where`/`OrderBy`/`Select`) | `S` not a canonical name: `400 {"error":"unknown_status"}` | + +Errors common to every route with `{id}`: +- unknown id: `404`; +- wrong state: `409 {"error":"invalid_transition","id":N,"state":"","required":""}`, and nothing is saved; +- corrupt persisted state: `500 {"error":"corrupt_state","id":N}`, and nothing is saved. + +Each transition handler does four things in order: +1. a tracked load; +2. `WithX` (refinement); +3. one transition, as an expression statement; +4. `SaveChangesAsync`. + +The clock is the DI `TimeProvider`. The acceptance runner substitutes a fixed clock, so its +output is deterministic. + +**Database provider:** SQLite (`Microsoft.EntityFrameworkCore.Sqlite` 8.0.11), one file per +run. **Schema:** `EnsureCreated`; there are **no migrations** (P25), and every acceptance run +starts from a fresh file. **Concurrency: OPTION A, OUT OF SCOPE.** No concurrency token. Two +requests racing on one row are not claimed correct. The README says so in its first section. + +## H1 used for real (P19) + +`OrderBackend.Shipping.TrackingNumber(int orderId)` is a static, pure `int` function. The Ship +handler calls it **inside** the `WithApproved` region, nested in the transition: +`approved.Ship(now, Shipping.TrackingNumber(id))`. +- **Expected facts:** one `proven_call` to `OrderBackend.Shipping.TrackingNumber(int)`, its site record, and its method record in `heap_effects`. +- **Expected verdict:** clean on both engines. + +No special case exists for the sample, and no BCL summary is involved. + +## Generator (P22) + +`frontend/roslyn/Own.TypedBuilder` is a console tool: `dotnet run --project … -- -o `. +- **Input:** it parses the one input file **syntactically** (no semantic model, no compilation). It refuses (exit 2, one line naming the defect) a declaration that is: + - not one `[TypedProtocol]` partial class; + - missing exactly one `[ProtocolState]` property of an enum declared in the same file; + - holding a transition whose states are not members of that enum; + - holding a transition name used twice, or a state with two outgoing transitions under one name; + - holding a `[BuilderRequired]` property that is not `string` or another non-nullable type it can pass through. +- **Output order:** states in enum order, transitions in declaration order, builder steps in declaration order. +- **Output bytes:** `\n` newlines, UTF-8 without BOM, no timestamp, no tool version, no absolute path. +- **File name:** `Order.Protocol.cs`. It is not `*.g.cs`, because the scan skips those and the protocol must be scanned as source. Its header reads "Generated by Own.TypedBuilder from Order.cs — do not edit; regenerate", without the word auto-generated. +- **Policy: the generated file is COMMITTED.** It is inspectable, and the extractor reads it. It is not regenerated at build time: no MSBuild hook, so `dotnet build` stays hermetic. +- **The gate:** + - generates twice into two clean temporary directories; + - requires the two outputs byte-identical (H17); + - requires them byte-identical to the committed file. + +## Test mechanisms + +**Compile-negative / protocol corpus (P17).** Each `corpus//.cs.txt` is a handler +file. The gate stages it **alone** into a fresh copy of the `OrderBackend` project. Then, by +stage: + +- **`compiler`:** `dotnet build` must fail, every error must be the expected `CSxxxx` in the staged file, and the expected member name must be in the message. +- **`extractor`:** the build succeeds, and the real extractor over the project file must exit 2, write no facts, and print the expected text naming the staged file. +- **`core`:** the build succeeds and the extractor writes facts. The verdict of `python -m ownlang ownir` must be the expected code set or refusal text. With `--rust `, the Rust CLI must give byte-identical exit code, stdout and stderr. +- **`clean`** (positive and limits marked accepted): the build succeeds, the extractor writes facts, and the verdict is `[]` on both engines. + +| id | case | stage | expected | +|---|---|---|---| +| C1 | Draft → Approve | compiler | CS1061 `Approve` | +| C2 | Draft → Ship | compiler | CS1061 `Ship` | +| C3 | Submitted → Submit | compiler | CS1061 `Submit` | +| C4 | Submitted → Ship | compiler | CS1061 `Ship` | +| C5 | Approved → Submit | compiler | CS1061 `Submit` | +| C6 | Approved → Approve | compiler | CS1061 `Approve` | +| C7 | Shipped → any (`approved.Ship(…).Submit(…)`) | compiler | CS1061 `Submit` | +| C7b | a Shipped region (`OrderProtocol.WithShipped`) | compiler | CS0117 `WithShipped` | +| C8 | stale Draft after Submit | core | `["OWN002"]` | +| C9 | stale Submitted after Approve | core | `["OWN002"]` | +| C10a | raw `order.ApplyShip(…)` outside a region | extractor | `'ApplyShip' of 'Order' is not public and belongs to a state protocol` | +| C10b | raw entity mention inside a region | core | `["OWN013"]` | +| C10c | raw `order.Status = …` | compiler | CS0272 `Status` | +| C11a | token copy, both used | core | `["OWN005"]` | +| C11b | entity alias inside a region | core | `["OWN013"]` | +| C12a | helper writing a static counter inside a region | core | refusal `… writes.static is may …` | +| C12b | logger call inside a region | extractor | `… LoggerExtensions.LogInformation' inside a protocol region runs code with no stated contract` | +| C13 | builder `Build()` without `Customer` | compiler | CS1061 `Build` | +| C14 | forged token `new DraftOrder(order)` | extractor | `a protocol token 'DraftOrder' is created outside the protocol's own types` | +| C15 | `new Order()` | compiler | CS0122 `Order` | + +| id | positive case (verdict `[]`, both engines) | +|---|---| +| P1 | create a Draft through the builder, `Add`, save | +| P2 | Draft → Submitted | +| P3 | Submitted → Approved | +| P4 | Approved → Shipped | +| P5 | harmless helper inside the region (`proven_call` present in the facts) | +| P6 | EF tracked load + refinement + transition + save | +| P7 | ordinary LINQ (`Where`/`OrderBy`/`Select`) before refinement | +| P8 | the full chain inside one region, with named intermediate tokens all spent | + +| id | limit (pinned so it is stated, not discovered) | expected | +|---|---|---| +| K1 | named terminal token never spent (`ShippedOrder shipped = approved.Ship(…)`) | `["OWN001"]` (linear tokens, G6) | +| K2 | `ExecuteUpdate` writes `Status` past every token | `[]` (outside the claim) | + +The case texts are exact as written above. A case whose result differs from its row is an +acceptance failure. It is never re-labelled after the fact. + +**The real sample itself.** The extractor runs over `samples/OrderBackend/OrderBackend/OrderBackend.csproj` +with `--flow-locals`: +- the facts must hold a region in each of the Submit, Approve and Ship handlers, plus the Ship `proven_call`; +- the verdict must be `[]` on both engines; +- the facts are pinned, JSON-equal, as `evidence/orderbackend.facts.json`. + +**Runtime acceptance (`Acceptance/`).** It runs the real `Backend.Build` on Kestrel at +`127.0.0.1:0`, with a fresh SQLite file and a fixed `TimeProvider`. Its oracles are +independent of the typed API: +- **Persisted state:** a raw `Microsoft.Data.Sqlite` connection reading `SELECT … FROM Orders WHERE Id = $id`. Not EF, not the typed API. +- **Identity:** the ChangeTracker, as in *EF tracking semantics*. +- **HTTP:** status code and response body, compared to the contract above. +- **Database unchanged:** a whole-row snapshot before and after. + +Every check prints one line `ok[]: …` or `FAIL[]: …`. The printed text contains no +port, path, time or GUID. Exit 0 only when every check holds. + +## Hostile controls H1–H18 (bindings) + +| H | bound to | +|---|---| +| H1 | C1 | +| H2 | C2 | +| H3 | C3 | +| H4 | C5 | +| H5 | C7, C7b | +| H6 | C8 | +| H7 | C10a, C10b, C10c (+ C14) | +| H8 | acceptance: raw-SQL `'Bogus'`, `'7'`, `'approved'` rows → every route `500 corrupt_state`, rows unchanged; EF load throws `CorruptOrderStateException` | +| H9 | acceptance: approve Draft, ship Draft, ship Submitted, submit Approved, submit/approve/ship Shipped → `409`, rows byte-unchanged | +| H10 | acceptance: identity proof (b)+(c) on a transition run outside HTTP | +| H11 | acceptance: after `SaveChangesAsync`, the raw row equals the expected one, column by column; the transition's columns change, the others do not | +| H12 | acceptance: a new context reloads the row, `WithX` for the persisted state admits, and `WithX` for any other state throws `InvalidOrderStateException` | +| H13 | P7 + acceptance: `GET /orders?status=Approved`, and `ToQueryString()` holds a server-side `WHERE` on `"Status"` | +| H14 | P5 + the real sample's facts (`proven_call` to `Shipping.TrackingNumber`) + clean verdict | +| H15 | C12a (core refusal), C12b (extractor refusal) | +| H16 | C11a, C11b | +| H17 | generator: two clean generations byte-identical and equal to the committed file | +| H18 | two full gate runs: the acceptance transcript and the gate's evidence files must be byte-identical (sha256 compared) | + +**HTTP happy path (P15):** +1. `POST /orders` gives `Draft`; +2. `/submit` gives `Submitted`; +3. `/approve` gives `Approved`; +4. `/ship` gives `Shipped`, with tracking number `Shipping.TrackingNumber(id)`; +5. `GET` gives `Shipped`. + +All five run against one database. After each step, the raw SQL oracle must read the state the +response claims. + +## Deterministic outputs + +The gate's verdict line and three evidence files (written by `--write`, compared otherwise) +are deterministic: +- `evidence/orderbackend.facts.json`; +- `evidence/corpus.json`, one entry per case: stage, expected, observed; +- `evidence/acceptance.txt`, the runner's transcript. + +## Official run order (P37) and acceptance verdict + +After the implementation commit, `python scripts/typed_builder_gate.py --rust --clean-checkout --runs 2` +does all of the following: +1. creates a `git worktree` of `HEAD` in a temporary directory, with no `bin/`/`obj/` and no generated output; +2. runs every step there: restore, build, generator determinism, positive corpus, negative corpus, real-sample scan, EF + HTTP acceptance with oracles; +3. does it twice from two fresh worktrees; +4. compares the evidence bytes and transcript sha256 across the two runs; +5. prints counts. + +The report goes into `docs/notes/tb-mvp-01-report.md`. + +**`GO_TYPED_BUILDER_MVP`** iff all 18 conditions of TB-MVP-P38 hold, mapped as follows: +- one entity: *Domain*; +- typed API, invalid absent: C1–C7, C7b; +- stale: C8, C9; +- refinement and invalid state: H8, H12; +- tracking: H10; +- save: H11; +- LINQ: H13; +- happy path: P15; +- wrong transitions: H9; +- H1: H14; +- fail-closed: H15; +- oracle: the persisted-state and identity checks; +- determinism: H17, H18; +- clean checkout; +- H1–H18; +- unchanged foundations: no file under `ownlang/`, `rust/`, `spec/`, `frontend/roslyn/OwnSharp.Extractor/` or `docs/evidence/calibration/`, and not `scripts/perf_baseline.py`, changes in the implementation commit (`git diff --stat 877ee69f..HEAD` shows none). + +Otherwise the result is one of the STOP verdicts of TB-MVP-P36. The failing case is preserved, the +reason is classified, and no prerequisite is built inside this slice. + +## P0 results + +Run on `877ee69f28ba169c1fd68935b41f4ef26d92f186`, a clean tree except for this document, before this commit: + +| gate | result | +|---|---| +| `python tests/run_tests.py` | rc 0, zero `FAIL` lines | +| `cargo test --no-fail-fast` (`rust/`) | rc 0, 51 test binaries, 290 passed, 0 failed | +| `python scripts/protocol_gate.py --rust rust/target/debug/own-cli` | 0 failures | +| `python scripts/heap_effects_gate.py` | PASS: samples sidecar, 50 inertness runs | +| `ruff check .` | all checks passed | + +The `protocol_gate.py` run covered 28 cases, 19 lowering refusals, 5 compiler rejections, 5 same-assembly programs, 4 unrelated programs, 24 efcore checks, and 29 documents byte-identical on both CLIs. From 95d811bfb1efb0ebd6c4990918b89d730422b0dc Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 3 Oct 2026 17:10:49 +0000 Subject: [PATCH 2/4] feat(typed-builder): TB-MVP-01 Order vertical slice (generator, ASP.NET Core + EF Core sample, gate) Implements docs/notes/tb-mvp-01-preregistration.md: - frontend/roslyn/Own.TypedBuilder: a syntax-only generator. From one annotated declaration ([TypedProtocol], [ProtocolState], [BuilderRequired], [Transition]) it writes the state tokens, transitions, checked region entries, strict state storage and a staged builder. Output is deterministic and committed (not *.g.cs: the extractor must scan it as source). - samples/OrderBackend: one ordinary EF Core Order entity under all typed states, a minimal API with create/submit/approve/ship/get/list, SQLite. A pure helper inside the Ship region goes through H1 proven_call. - corpus: 8 positive, 20 negative (compiler / extractor / core), 2 stated limits, each pinned to its registered answer. - Acceptance: real HTTP on real SQLite, with raw-SQL, ChangeTracker and HTTP oracles outside the typed API; fixed clock, deterministic transcript. - scripts/typed_builder_gate.py (+ --clean-checkout) and the CI step. No change under ownlang/, rust/, spec/, the extractor or T0 calibration. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_011ZFvhLx1fM9Gerg4dKsZcL --- .gitattributes | 7 + .github/workflows/ci.yml | 10 + .../Own.TypedBuilder/Own.TypedBuilder.csproj | 18 + frontend/roslyn/Own.TypedBuilder/Program.cs | 464 ++++++++++++++ frontend/roslyn/README.md | 5 + samples/OrderBackend/.gitignore | 2 + .../OrderBackend/Acceptance/Acceptance.csproj | 16 + samples/OrderBackend/Acceptance/Program.cs | 358 +++++++++++ .../OrderBackend/Data/OrdersDb.cs | 24 + .../OrderBackend/Domain/Order.Protocol.cs | 223 +++++++ .../OrderBackend/OrderBackend/Domain/Order.cs | 51 ++ .../OrderBackend/Domain/TypedBuilder.cs | 49 ++ .../OrderBackend/OrderBackend.csproj | 15 + .../OrderBackend/OrderEndpoints.cs | 165 +++++ samples/OrderBackend/OrderBackend/Program.cs | 41 ++ samples/OrderBackend/OrderBackend/Shipping.cs | 10 + samples/OrderBackend/README.md | 187 ++++++ .../limits/K1_named_terminal_token.cs.txt | 24 + .../corpus/limits/K2_execute_update.cs.txt | 17 + .../OrderBackend/corpus/limits/expected.json | 14 + .../corpus/negative/C10a_raw_mutator.cs.txt | 20 + .../negative/C10b_raw_entity_in_region.cs.txt | 25 + .../negative/C10c_raw_state_write.cs.txt | 20 + .../corpus/negative/C11a_token_copy.cs.txt | 26 + .../corpus/negative/C11b_entity_alias.cs.txt | 25 + .../negative/C12a_harmful_helper.cs.txt | 31 + .../negative/C12b_logger_in_region.cs.txt | 25 + .../C13_builder_without_customer.cs.txt | 15 + .../corpus/negative/C14_forged_token.cs.txt | 20 + .../negative/C15_entity_constructor.cs.txt | 15 + .../corpus/negative/C1_draft_approve.cs.txt | 24 + .../corpus/negative/C2_draft_ship.cs.txt | 24 + .../negative/C3_submitted_submit.cs.txt | 24 + .../corpus/negative/C4_submitted_ship.cs.txt | 24 + .../corpus/negative/C5_approved_submit.cs.txt | 24 + .../negative/C6_approved_approve.cs.txt | 24 + .../negative/C7_shipped_transition.cs.txt | 24 + .../corpus/negative/C7b_shipped_region.cs.txt | 23 + .../corpus/negative/C8_stale_draft.cs.txt | 26 + .../corpus/negative/C9_stale_submitted.cs.txt | 26 + .../corpus/negative/expected.json | 103 +++ .../corpus/positive/P1_create_draft.cs.txt | 23 + .../corpus/positive/P2_draft_submit.cs.txt | 24 + .../positive/P3_submitted_approve.cs.txt | 24 + .../corpus/positive/P4_approved_ship.cs.txt | 24 + .../corpus/positive/P5_harmless_helper.cs.txt | 24 + .../positive/P6_load_refine_transition.cs.txt | 34 + .../positive/P7_linq_before_refinement.cs.txt | 29 + .../corpus/positive/P8_full_chain.cs.txt | 26 + .../corpus/positive/expected.json | 36 ++ samples/OrderBackend/evidence/acceptance.txt | 45 ++ samples/OrderBackend/evidence/corpus.json | 357 +++++++++++ .../evidence/orderbackend.facts.json | 603 ++++++++++++++++++ samples/OrderBackend/nuget.config | 8 + scripts/typed_builder_gate.py | 419 ++++++++++++ 55 files changed, 3944 insertions(+) create mode 100644 frontend/roslyn/Own.TypedBuilder/Own.TypedBuilder.csproj create mode 100644 frontend/roslyn/Own.TypedBuilder/Program.cs create mode 100644 samples/OrderBackend/.gitignore create mode 100644 samples/OrderBackend/Acceptance/Acceptance.csproj create mode 100644 samples/OrderBackend/Acceptance/Program.cs create mode 100644 samples/OrderBackend/OrderBackend/Data/OrdersDb.cs create mode 100644 samples/OrderBackend/OrderBackend/Domain/Order.Protocol.cs create mode 100644 samples/OrderBackend/OrderBackend/Domain/Order.cs create mode 100644 samples/OrderBackend/OrderBackend/Domain/TypedBuilder.cs create mode 100644 samples/OrderBackend/OrderBackend/OrderBackend.csproj create mode 100644 samples/OrderBackend/OrderBackend/OrderEndpoints.cs create mode 100644 samples/OrderBackend/OrderBackend/Program.cs create mode 100644 samples/OrderBackend/OrderBackend/Shipping.cs create mode 100644 samples/OrderBackend/README.md create mode 100644 samples/OrderBackend/corpus/limits/K1_named_terminal_token.cs.txt create mode 100644 samples/OrderBackend/corpus/limits/K2_execute_update.cs.txt create mode 100644 samples/OrderBackend/corpus/limits/expected.json create mode 100644 samples/OrderBackend/corpus/negative/C10a_raw_mutator.cs.txt create mode 100644 samples/OrderBackend/corpus/negative/C10b_raw_entity_in_region.cs.txt create mode 100644 samples/OrderBackend/corpus/negative/C10c_raw_state_write.cs.txt create mode 100644 samples/OrderBackend/corpus/negative/C11a_token_copy.cs.txt create mode 100644 samples/OrderBackend/corpus/negative/C11b_entity_alias.cs.txt create mode 100644 samples/OrderBackend/corpus/negative/C12a_harmful_helper.cs.txt create mode 100644 samples/OrderBackend/corpus/negative/C12b_logger_in_region.cs.txt create mode 100644 samples/OrderBackend/corpus/negative/C13_builder_without_customer.cs.txt create mode 100644 samples/OrderBackend/corpus/negative/C14_forged_token.cs.txt create mode 100644 samples/OrderBackend/corpus/negative/C15_entity_constructor.cs.txt create mode 100644 samples/OrderBackend/corpus/negative/C1_draft_approve.cs.txt create mode 100644 samples/OrderBackend/corpus/negative/C2_draft_ship.cs.txt create mode 100644 samples/OrderBackend/corpus/negative/C3_submitted_submit.cs.txt create mode 100644 samples/OrderBackend/corpus/negative/C4_submitted_ship.cs.txt create mode 100644 samples/OrderBackend/corpus/negative/C5_approved_submit.cs.txt create mode 100644 samples/OrderBackend/corpus/negative/C6_approved_approve.cs.txt create mode 100644 samples/OrderBackend/corpus/negative/C7_shipped_transition.cs.txt create mode 100644 samples/OrderBackend/corpus/negative/C7b_shipped_region.cs.txt create mode 100644 samples/OrderBackend/corpus/negative/C8_stale_draft.cs.txt create mode 100644 samples/OrderBackend/corpus/negative/C9_stale_submitted.cs.txt create mode 100644 samples/OrderBackend/corpus/negative/expected.json create mode 100644 samples/OrderBackend/corpus/positive/P1_create_draft.cs.txt create mode 100644 samples/OrderBackend/corpus/positive/P2_draft_submit.cs.txt create mode 100644 samples/OrderBackend/corpus/positive/P3_submitted_approve.cs.txt create mode 100644 samples/OrderBackend/corpus/positive/P4_approved_ship.cs.txt create mode 100644 samples/OrderBackend/corpus/positive/P5_harmless_helper.cs.txt create mode 100644 samples/OrderBackend/corpus/positive/P6_load_refine_transition.cs.txt create mode 100644 samples/OrderBackend/corpus/positive/P7_linq_before_refinement.cs.txt create mode 100644 samples/OrderBackend/corpus/positive/P8_full_chain.cs.txt create mode 100644 samples/OrderBackend/corpus/positive/expected.json create mode 100644 samples/OrderBackend/evidence/acceptance.txt create mode 100644 samples/OrderBackend/evidence/corpus.json create mode 100644 samples/OrderBackend/evidence/orderbackend.facts.json create mode 100644 samples/OrderBackend/nuget.config create mode 100644 scripts/typed_builder_gate.py diff --git a/.gitattributes b/.gitattributes index ef087200..51ef9854 100644 --- a/.gitattributes +++ b/.gitattributes @@ -23,3 +23,10 @@ # hashed 79ad1476f219 on Linux and 3dda13ce16d6 on Windows, and a run that # measured exactly the right tree was rejected as evidence for another tree. docs/evidence/*.json text eol=lf + +# TB-MVP-01: the generated protocol surface is compared BY BYTE with what +# `frontend/roslyn/Own.TypedBuilder` writes (`\n`, no BOM), and the Typed Builder +# gate's evidence is the same bytes on every platform. A Windows checkout with +# `core.autocrlf=true` would make a correct generator look stale. +samples/OrderBackend/OrderBackend/Domain/Order.Protocol.cs text eol=lf +samples/OrderBackend/evidence/* text eol=lf diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 7f00e39e..adce4d88 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -3353,6 +3353,16 @@ jobs: # no exit code and no stderr — over every protocol case and refusal and examples/. - name: Heap-effect sidecar (samples + inertness of --heap-effects) run: python scripts/heap_effects_gate.py + # TB-MVP-01 (docs/notes/tb-mvp-01-preregistration.md): the Typed Builder Order + # vertical slice. The generator's output is deterministic and committed; the corpus + # is held to its registered compiler / extractor / core answers; the backend runs + # real HTTP against real SQLite twice with oracles outside the typed API. + - name: Typed Builder MVP (generator, corpus, EF + HTTP acceptance) + if: matrix.os != 'ubuntu-latest' + run: python scripts/typed_builder_gate.py + - name: Typed Builder MVP + both public CLIs on every core-stage document + if: matrix.os == 'ubuntu-latest' + run: python scripts/typed_builder_gate.py --rust "$PWD/rust/target/debug/own-cli" # P-012 slice 1: score the checker against the labeled corpus on REAL C# — not # just the .own reduction tests/test_corpus.py checks. Per case: the bug must be diff --git a/frontend/roslyn/Own.TypedBuilder/Own.TypedBuilder.csproj b/frontend/roslyn/Own.TypedBuilder/Own.TypedBuilder.csproj new file mode 100644 index 00000000..fad706e7 --- /dev/null +++ b/frontend/roslyn/Own.TypedBuilder/Own.TypedBuilder.csproj @@ -0,0 +1,18 @@ + + + + Exe + net8.0 + enable + enable + own-typed-builder + Own.TypedBuilder + + + + + + + + diff --git a/frontend/roslyn/Own.TypedBuilder/Program.cs b/frontend/roslyn/Own.TypedBuilder/Program.cs new file mode 100644 index 00000000..7bb62f2e --- /dev/null +++ b/frontend/roslyn/Own.TypedBuilder/Program.cs @@ -0,0 +1,464 @@ +// own-typed-builder: the Typed Builder generator (TB-MVP-01). +// +// own-typed-builder -o +// +// Reads ONE hand-written declaration file and writes the state-protocol surface the +// Own.NET profile analyses (frontend/roslyn/README.md, "State protocols"): one +// [ProtocolToken] ref struct per state, one transition method per declared transition, +// one [ProtocolRegion] entry per state that has an outgoing transition, the checked +// refinement, a strict storage converter for the state, and a staged builder whose +// Build() exists only once every required field was given. +// +// The declaration (matched by NAME, so the domain depends on nothing): +// +// [TypedProtocol] on the entity: a `partial class` +// [ProtocolState] on exactly one property, of an enum declared in +// the same file; its FIRST member is the state +// Build() creates +// [BuilderRequired] on each construction field, in order +// [Transition("Name", E.From, E.To)] on a non-public void hook: the business data the +// transition writes. The STATE write is generated, +// so a hook cannot move the entity to a wrong state. +// +// It is a generator, not an analysis: syntax only, no compilation, no semantic model. +// The output is a function of the input's syntax alone — `\n` newlines, UTF-8 without a +// BOM, no timestamp, no version, no path — so two runs are byte-identical. The file is +// meant to be COMMITTED and is deliberately not named `*.g.cs`: the extractor's scan +// skips those, and the profile admits a protocol only when it is in the scan as source. +// +// Exit codes: 0 written; 2 the declaration is refused (one line per defect on stderr); +// 64 usage. + +using System.Text; +using Microsoft.CodeAnalysis; +using Microsoft.CodeAnalysis.CSharp; +using Microsoft.CodeAnalysis.CSharp.Syntax; + +if (args.Length != 3 || args[1] != "-o") +{ + Console.Error.WriteLine("usage: own-typed-builder -o "); + return 64; +} + +var input = args[0]; +var text = File.ReadAllText(input).Replace("\r\n", "\n"); +var tree = CSharpSyntaxTree.ParseText(text, path: input); +var errors = tree.GetDiagnostics().Where(d => d.Severity == DiagnosticSeverity.Error).ToList(); +var problems = new List(); +foreach (var e in errors) + problems.Add($"the declaration does not parse: {e.GetMessage()} (line {e.Location.GetLineSpan().StartLinePosition.Line + 1})"); + +Model? model = problems.Count == 0 ? Model.Read(tree.GetRoot(), Path.GetFileName(input), problems) : null; +if (model is null || problems.Count > 0) +{ + foreach (var p in problems) + Console.Error.WriteLine($"own-typed-builder: {Path.GetFileName(input)}: {p}"); + return 2; +} + +var output = Emit.Render(model); +File.WriteAllBytes(args[2], new UTF8Encoding(encoderShouldEmitUTF8Identifier: false).GetBytes(output)); +return 0; + +/// One transition as declared: `[Transition(Name, From, To)]` on `Hook(Parameters)`. +sealed record Transition(string Name, string From, string To, string Hook, IReadOnlyList<(string Type, string Name)> Parameters); + +/// One `[BuilderRequired]` construction field. +sealed record Field(string Name, string Type, bool NullCheck); + +sealed record Model( + string Source, + string? Namespace, + string Entity, + string IdType, + string StateProperty, + string StateEnum, + IReadOnlyList States, + IReadOnlyList Fields, + IReadOnlyList Transitions) +{ + static bool Named(AttributeSyntax a, string name) + { + var n = a.Name switch + { + QualifiedNameSyntax q => q.Right.Identifier.Text, + AliasQualifiedNameSyntax q => q.Name.Identifier.Text, + SimpleNameSyntax s => s.Identifier.Text, + _ => a.Name.ToString(), + }; + return n == name || n == name + "Attribute"; + } + + static IEnumerable Attrs(MemberDeclarationSyntax m) => + m.AttributeLists.SelectMany(l => l.Attributes); + + static readonly HashSet ValueKeywords = new(StringComparer.Ordinal) + { + "bool", "byte", "sbyte", "short", "ushort", "int", "uint", "long", "ulong", + "decimal", "double", "float", "char", + }; + + public static Model? Read(SyntaxNode root, string source, List problems) + { + var entities = root.DescendantNodes().OfType() + .Where(c => Attrs(c).Any(a => Named(a, "TypedProtocol"))).ToList(); + if (entities.Count != 1) + { + problems.Add($"expected exactly one [TypedProtocol] class, found {entities.Count}"); + return null; + } + var entity = entities[0]; + if (!entity.Modifiers.Any(SyntaxKind.PartialKeyword)) + problems.Add($"'{entity.Identifier.Text}' must be a partial class: the generated half is the other part"); + if (entity.TypeParameterList is not null || entity.Parent is TypeDeclarationSyntax) + problems.Add($"'{entity.Identifier.Text}' must be a top-level, non-generic class"); + + var ns = entity.Ancestors().OfType().FirstOrDefault()?.Name.ToString(); + + var enums = root.DescendantNodes().OfType() + .ToDictionary(e => e.Identifier.Text, e => e.Members.Select(m => m.Identifier.Text).ToList()); + + var properties = entity.Members.OfType().ToList(); + var id = properties.FirstOrDefault(p => p.Identifier.Text == "Id"); + if (id is null) + problems.Add($"'{entity.Identifier.Text}' has no 'Id' property: the tokens and the refusal name the entity by it"); + + var stateProps = properties.Where(p => Attrs(p).Any(a => Named(a, "ProtocolState"))).ToList(); + string stateEnum = "", stateProp = ""; + List states = new(); + if (stateProps.Count != 1) + problems.Add($"expected exactly one [ProtocolState] property, found {stateProps.Count}"); + else + { + stateProp = stateProps[0].Identifier.Text; + stateEnum = stateProps[0].Type.ToString(); + if (!enums.TryGetValue(stateEnum, out states!)) + { + problems.Add($"the state property '{stateProp}' has type '{stateEnum}', which is not an enum declared in this file"); + states = new(); + } + else if (states.Count == 0) + problems.Add($"the state enum '{stateEnum}' has no members"); + else if (states.Distinct(StringComparer.Ordinal).Count() != states.Count) + problems.Add($"the state enum '{stateEnum}' declares a member twice"); + if (PubliclyWritable(stateProps[0])) + problems.Add($"the state property '{stateProp}' must not be publicly writable: the tokens are the only way to change it"); + } + + var fields = new List(); + foreach (var p in properties.Where(p => Attrs(p).Any(a => Named(a, "BuilderRequired")))) + { + var type = p.Type.ToString(); + if (type == "string") + fields.Add(new Field(p.Identifier.Text, type, NullCheck: true)); + else if (ValueKeywords.Contains(type)) + fields.Add(new Field(p.Identifier.Text, type, NullCheck: false)); + else + problems.Add($"[BuilderRequired] '{p.Identifier.Text}' has type '{type}': only string and the built-in value types are supported"); + if (p.Identifier.Text == stateProp) + problems.Add($"[BuilderRequired] '{p.Identifier.Text}' is the state: Build() sets it"); + } + + var transitions = new List(); + foreach (var m in entity.Members.OfType()) + foreach (var a in Attrs(m).Where(a => Named(a, "Transition"))) + { + var where = $"[Transition] on '{m.Identifier.Text}'"; + var argsList = a.ArgumentList?.Arguments ?? default; + if (argsList.Count != 3 || argsList.Any(x => x.NameEquals is not null || x.NameColon is not null)) + { + problems.Add($"{where}: expected (\"Name\", {stateEnum}.From, {stateEnum}.To)"); + continue; + } + if (argsList[0].Expression is not LiteralExpressionSyntax lit || !lit.IsKind(SyntaxKind.StringLiteralExpression) + || !SyntaxFacts.IsValidIdentifier(lit.Token.ValueText)) + { + problems.Add($"{where}: the name must be a string literal that is a C# identifier"); + continue; + } + string? State(ExpressionSyntax e) + { + if (e is MemberAccessExpressionSyntax { Expression: IdentifierNameSyntax owner } ma + && owner.Identifier.Text == stateEnum && states.Contains(ma.Name.Identifier.Text)) + return ma.Name.Identifier.Text; + problems.Add($"{where}: '{e}' is not a member of the state enum '{stateEnum}'"); + return null; + } + var from = State(argsList[1].Expression); + var to = State(argsList[2].Expression); + if (m.Modifiers.Any(SyntaxKind.PublicKeyword)) + problems.Add($"{where}: the hook must not be public: a public method writing protocol data is a transition nobody declared"); + if (m.Modifiers.Any(SyntaxKind.StaticKeyword) || m.TypeParameterList is not null + || m.ReturnType.ToString() != "void" || m.Body is null && m.ExpressionBody is null) + problems.Add($"{where}: the hook must be a non-generic instance method returning void, with a body"); + var ps = new List<(string, string)>(); + foreach (var p in m.ParameterList.Parameters) + { + if (p.Modifiers.Count > 0 || p.Default is not null || p.Type is null) + problems.Add($"{where}: parameter '{p.Identifier.Text}' must be a plain by-value parameter with no default"); + ps.Add((p.Type?.ToString() ?? "?", p.Identifier.Text)); + } + if (from is not null && to is not null) + transitions.Add(new Transition(lit.Token.ValueText, from, to, m.Identifier.Text, ps)); + } + if (transitions.Count == 0) + problems.Add("no [Transition] is declared"); + foreach (var dup in transitions.GroupBy(t => t.Name).Where(g => g.Count() > 1)) + problems.Add($"the transition name '{dup.Key}' is declared {dup.Count()} times"); + foreach (var t in transitions) + if (t.Name == "Id") + problems.Add("a transition may not be named 'Id': the tokens expose the entity's Id"); + + return new Model(source, ns, entity.Identifier.Text, id?.Type.ToString() ?? "int", stateProp, stateEnum, + states, fields, transitions); + } + + static bool PubliclyWritable(PropertyDeclarationSyntax p) + { + if (!p.Modifiers.Any(SyntaxKind.PublicKeyword)) + return false; + var setter = p.AccessorList?.Accessors.FirstOrDefault(a => a.IsKind(SyntaxKind.SetAccessorDeclaration)); + return setter is not null && setter.Modifiers.Count == 0; + } +} + +static class Emit +{ + public static string Render(Model m) + { + var o = new StringBuilder(); + void L(string line = "") => o.Append(line).Append('\n'); + string Token(string state) => state + m.Entity; + var outgoing = m.States.Where(s => m.Transitions.Any(t => t.From == s)).ToList(); + var e = m.Entity; + var lower = char.ToLowerInvariant(e[0]) + e[1..]; + var invalid = $"Invalid{e}StateException"; + var corrupt = $"Corrupt{e}StateException"; + var initial = m.States[0]; + + L($"// Generated by Own.TypedBuilder from {m.Source}. Do not edit: change {m.Source} and regenerate."); + L("//"); + L("// The state protocol of " + e + ": one [ProtocolToken] per state, one transition per"); + L("// [Transition], one [ProtocolRegion] per state with a way out, the checked refinement,"); + L("// the strict storage of the state, and the staged builder. Own.NET analyses this file as"); + L("// source: it is the protocol's trusted definition surface."); + L(); + L("using System;"); + L(); + if (m.Namespace is not null) + { + L($"namespace {m.Namespace};"); + L(); + } + + // ---- the entity's generated half -------------------------------------------------- + L($"partial class {e}"); + L("{"); + foreach (var t in m.Transitions) + { + var ps = string.Join(", ", t.Parameters.Select(p => $"{p.Type} {p.Name}")); + var args = string.Join(", ", t.Parameters.Select(p => p.Name)); + L($" // {t.From} -> {t.Name} -> {t.To}"); + L($" internal void Apply{t.Name}({ps})"); + L(" {"); + L($" {t.Hook}({args});"); + L($" {m.StateProperty} = {m.StateEnum}.{t.To};"); + L(" }"); + L(); + } + // the first step is the innermost one (see EmitBuilder) + var first = string.Join(".", m.Fields.Select(f => f.Name + "Step").Reverse().Prepend($"{initial}Builder")); + L($" /// Starts a new {e} in its initial state, {initial}. Build() exists only once every"); + L(" /// required field was given."); + L($" public static {first} Create() => new();"); + L(); + EmitBuilder(m, L, initial); + L("}"); + L(); + + // ---- refusals --------------------------------------------------------------------- + L($"/// The runtime half of the refinement: the state came from data, so it is checked once,"); + L("/// at the region entry."); + L($"public sealed class {invalid}({m.IdType} id, {m.StateEnum} actual, {m.StateEnum} required)"); + L($" : InvalidOperationException($\"{lower} {{id}} is {{actual}}, not {{required}}\")"); + L("{"); + L($" public {m.IdType} Id {{ get; }} = id;"); + L(); + L($" public {m.StateEnum} Actual {{ get; }} = actual;"); + L(); + L($" public {m.StateEnum} Required {{ get; }} = required;"); + L("}"); + L(); + L($"/// A persisted state that is not exactly one of {m.StateEnum}'s names. Never mapped to a"); + L("/// state: no default, no case folding, no number."); + L($"public sealed class {corrupt}(string raw)"); + L($" : InvalidOperationException($\"the persisted {lower} state '{{raw}}' is not {Article(m.StateEnum)} {m.StateEnum}\")"); + L("{"); + L(" public string Raw { get; } = raw;"); + L("}"); + L(); + + // ---- strict storage --------------------------------------------------------------- + L($"/// The one mapping between {m.StateEnum} and its stored text: the exact member name."); + L($"public static class {m.StateEnum}Storage"); + L("{"); + L($" public static string ToStore({m.StateEnum} state) => state switch"); + L(" {"); + foreach (var s in m.States) + L($" {m.StateEnum}.{s} => \"{s}\","); + L($" _ => throw new {corrupt}(state.ToString()),"); + L(" };"); + L(); + L($" public static {m.StateEnum} FromStore(string raw) =>"); + L($" TryFromStore(raw, out var state) ? state : throw new {corrupt}(raw);"); + L(); + L($" public static bool TryFromStore(string? raw, out {m.StateEnum} state)"); + L(" {"); + L(" switch (raw)"); + L(" {"); + foreach (var s in m.States) + { + L($" case \"{s}\":"); + L($" state = {m.StateEnum}.{s};"); + L(" return true;"); + } + L(" default:"); + L(" state = default;"); + L(" return false;"); + L(" }"); + L(" }"); + L("}"); + L(); + + // ---- tokens ----------------------------------------------------------------------- + foreach (var s in m.States) + { + var exits = m.Transitions.Where(t => t.From == s).ToList(); + L(exits.Count == 0 + ? $"/// {e} in state {s}. Terminal: no transition leaves it." + : $"/// {e} in state {s}. A transition spends this token and hands back the next one."); + L("[ProtocolToken]"); + L($"public readonly ref struct {Token(s)}"); + L("{"); + L($" private readonly {e} _{lower};"); + L(); + L($" internal {Token(s)}({e} {lower}) => _{lower} = {lower};"); + L(); + L($" public {m.IdType} Id => _{lower}.Id;"); + foreach (var t in exits) + { + var ps = string.Join(", ", t.Parameters.Select(p => $"{p.Type} {p.Name}")); + var args = string.Join(", ", t.Parameters.Select(p => p.Name)); + L(); + L($" public {Token(t.To)} {t.Name}({ps})"); + L(" {"); + L($" _{lower}.Apply{t.Name}({args});"); + L($" return new {Token(t.To)}(_{lower});"); + L(" }"); + } + L("}"); + L(); + } + + // ---- regions ---------------------------------------------------------------------- + foreach (var s in outgoing) + L($"public delegate void {s}Region({Token(s)} {char.ToLowerInvariant(s[0]) + s[1..]});"); + L(); + L($"/// The checked refinement: {Article(e)} {e} whose state is only known at run time becomes a token"); + L("/// inside the callback, or the call throws and no token exists. A state no transition"); + L("/// leaves has no region: its token could never be spent."); + L($"public static class {e}Protocol"); + L("{"); + for (var i = 0; i < outgoing.Count; i++) + { + var s = outgoing[i]; + if (i > 0) + L(); + L(" [ProtocolRegion]"); + L($" public static void With{s}({e} {lower}, {s}Region body)"); + L(" {"); + L($" ArgumentNullException.ThrowIfNull({lower});"); + L(" ArgumentNullException.ThrowIfNull(body);"); + L($" if ({lower}.{m.StateProperty} != {m.StateEnum}.{s})"); + L($" throw new {invalid}({lower}.Id, {lower}.{m.StateProperty}, {m.StateEnum}.{s});"); + L($" body(new {Token(s)}({lower}));"); + L(" }"); + } + L("}"); + return o.ToString(); + } + + static string Article(string word) => "AEIOUaeiou".Contains(word[0]) ? "an" : "a"; + + // The staged builder, nested inside the entity so it can reach its private constructor + // and setters. The steps nest INWARD from the finished builder: each step constructs the + // type that contains it through a private constructor, so the only way to a Build() is + // through every step, in order. + static void EmitBuilder(Model m, Action L, string initial) + { + var e = m.Entity; + var depth = 1; + string Pad() => new(' ', depth * 4); + string Lower(string s) => char.ToLowerInvariant(s[0]) + s[1..]; + + L($"{Pad()}public sealed class {initial}Builder"); + L($"{Pad()}{{"); + depth++; + foreach (var f in m.Fields) + L($"{Pad()}private readonly {f.Type} _{Lower(f.Name)};"); + if (m.Fields.Count > 0) + L(""); + var all = string.Join(", ", m.Fields.Select(f => $"{f.Type} {Lower(f.Name)}")); + L($"{Pad()}{(m.Fields.Count == 0 ? "internal" : "private")} {initial}Builder({all})"); + L($"{Pad()}{{"); + foreach (var f in m.Fields) + L($"{Pad()} _{Lower(f.Name)} = {Lower(f.Name)};"); + L($"{Pad()}}}"); + L(""); + var init = string.Join(", ", m.Fields.Select(f => $"{f.Name} = _{Lower(f.Name)}") + .Append($"{m.StateProperty} = {m.StateEnum}.{initial}")); + L($"{Pad()}public {e} Build() => new() {{ {init} }};"); + + // step k holds fields [0, k) and takes field k; the steps nest so that step k sits + // inside step k+1 (the last step inside the builder). + var opened = 0; + for (var k = m.Fields.Count - 1; k >= 0; k--) + { + var f = m.Fields[k]; + var held = m.Fields.Take(k).ToList(); + var next = k == m.Fields.Count - 1 ? $"{initial}Builder" : $"{m.Fields[k + 1].Name}Step"; + L(""); + L($"{Pad()}public sealed class {f.Name}Step"); + L($"{Pad()}{{"); + depth++; + foreach (var h in held) + L($"{Pad()}private readonly {h.Type} _{Lower(h.Name)};"); + if (held.Count > 0) + L(""); + var ctor = string.Join(", ", held.Select(h => $"{h.Type} {Lower(h.Name)}")); + // the first step is where Create() starts: it holds nothing, so making one by + // hand gains nothing + L($"{Pad()}{(k == 0 ? "internal" : "private")} {f.Name}Step({ctor})"); + L($"{Pad()}{{"); + foreach (var h in held) + L($"{Pad()} _{Lower(h.Name)} = {Lower(h.Name)};"); + L($"{Pad()}}}"); + L(""); + var pass = string.Join(", ", held.Select(h => $"_{Lower(h.Name)}").Append(Lower(f.Name))); + L($"{Pad()}public {next} {f.Name}({f.Type} {Lower(f.Name)})"); + L($"{Pad()}{{"); + if (f.NullCheck) + L($"{Pad()} ArgumentNullException.ThrowIfNull({Lower(f.Name)});"); + L($"{Pad()} return new {next}({pass});"); + L($"{Pad()}}}"); + opened++; + } + for (var i = 0; i < opened; i++) + { + depth--; + L($"{Pad()}}}"); + } + depth--; + L($"{Pad()}}}"); + } +} diff --git a/frontend/roslyn/README.md b/frontend/roslyn/README.md index 459511e3..1df94062 100644 --- a/frontend/roslyn/README.md +++ b/frontend/roslyn/README.md @@ -114,6 +114,11 @@ API, EF Core, SQLite — is in [`protocol-samples/efcore`](protocol-samples/efcore), and `python scripts/protocol_gate.py` ties every committed fact back to the C# it came from. +The product-shaped version of the same backend, with the protocol **generated** +from one annotated declaration (`frontend/roslyn/Own.TypedBuilder`), a typed +builder, and every transition over HTTP, is +[`samples/OrderBackend`](../../samples/OrderBackend) (TB-MVP-01, +`python scripts/typed_builder_gate.py`). **What is claimed.** The profile protects the local C# capabilities and aliases of an entity that already exists. It does **not** protect the persisted row from diff --git a/samples/OrderBackend/.gitignore b/samples/OrderBackend/.gitignore new file mode 100644 index 00000000..cd42ee34 --- /dev/null +++ b/samples/OrderBackend/.gitignore @@ -0,0 +1,2 @@ +bin/ +obj/ diff --git a/samples/OrderBackend/Acceptance/Acceptance.csproj b/samples/OrderBackend/Acceptance/Acceptance.csproj new file mode 100644 index 00000000..773569a9 --- /dev/null +++ b/samples/OrderBackend/Acceptance/Acceptance.csproj @@ -0,0 +1,16 @@ + + + + Exe + net8.0 + 12 + enable + enable + OrderBackend.Acceptance + + + + + + + diff --git a/samples/OrderBackend/Acceptance/Program.cs b/samples/OrderBackend/Acceptance/Program.cs new file mode 100644 index 00000000..813dc13e --- /dev/null +++ b/samples/OrderBackend/Acceptance/Program.cs @@ -0,0 +1,358 @@ +using System.Net; +using System.Text; +using Microsoft.Data.Sqlite; +using Microsoft.EntityFrameworkCore; +using Microsoft.EntityFrameworkCore.Diagnostics; +using OrderBackend; +using OrderBackend.Data; +using OrderBackend.Domain; + +// TB-MVP-01 acceptance: the real backend, over a real HTTP listener and a real SQLite file. +// +// The oracles do not go through the typed API: +// * persisted state — a raw Microsoft.Data.Sqlite connection, not EF (`Row`); +// * object identity — EF's ChangeTracker, against the reference the query returned; +// * HTTP — the status code and the exact response body. +// +// Every line is `ok[id]: ...` or `FAIL[id]: ...` and holds no port, path, GUID or wall-clock +// time (the backend's clock is fixed), so two runs print the same bytes. Exit 0 only when +// every check holds. + +var failures = 0; +void Check(string id, bool holds, string detail) +{ + Console.WriteLine($"{(holds ? "ok" : "FAIL")}[{id}]: {detail}"); + if (!holds) + failures++; +} + +var dbPath = Path.Combine(Path.GetTempPath(), $"tb-mvp-{Guid.NewGuid():N}.db"); +var clock = new FixedClock(new DateTimeOffset(2026, 1, 2, 3, 4, 5, TimeSpan.Zero)); +var now = clock.GetUtcNow().UtcDateTime; +var sql = new List(); +void Database(DbContextOptionsBuilder options) => options + .UseSqlite($"Data Source={dbPath}") + .LogTo(text => { lock (sql) sql.Add(text); }, new[] { RelationalEventId.CommandExecuted }); + +OrdersDb Fresh() +{ + var options = new DbContextOptionsBuilder(); + Database(options); + return new OrdersDb(options.Options); +} + +// ---- the raw oracle: SQL on its own connection, nothing from EF or the typed API ---------- +const string Columns = "Id, Customer, Status, SubmittedAt, ApprovedAt, ShippedAt, TrackingNumber"; +string[] ColumnNames = Columns.Split(", "); + +string[]? Row(long id) +{ + using var c = new SqliteConnection($"Data Source={dbPath};Pooling=False"); + c.Open(); + using var cmd = c.CreateCommand(); + cmd.CommandText = $"SELECT {Columns} FROM Orders WHERE Id = $id"; + cmd.Parameters.AddWithValue("$id", id); + using var r = cmd.ExecuteReader(); + if (!r.Read()) + return null; + return Enumerable.Range(0, r.FieldCount) + .Select(i => r.IsDBNull(i) ? "NULL" : Convert.ToString(r.GetValue(i), System.Globalization.CultureInfo.InvariantCulture)!) + .ToArray(); +} + +string Show(string[]? row) => row is null ? "" : string.Join(" | ", row); + +long Scalar(string text) +{ + using var c = new SqliteConnection($"Data Source={dbPath};Pooling=False"); + c.Open(); + using var cmd = c.CreateCommand(); + cmd.CommandText = text; + return Convert.ToInt64(cmd.ExecuteScalar(), System.Globalization.CultureInfo.InvariantCulture); +} + +long InsertRaw(string customer, string status) +{ + using var c = new SqliteConnection($"Data Source={dbPath};Pooling=False"); + c.Open(); + using var cmd = c.CreateCommand(); + cmd.CommandText = "INSERT INTO Orders (Customer, Status) VALUES ($c, $s); SELECT last_insert_rowid();"; + cmd.Parameters.AddWithValue("$c", customer); + cmd.Parameters.AddWithValue("$s", status); + return Convert.ToInt64(cmd.ExecuteScalar(), System.Globalization.CultureInfo.InvariantCulture); +} + +// the columns two snapshots differ in +string Diff(string[]? before, string[]? after) => + before is null || after is null + ? "" + : string.Join(",", ColumnNames.Where((_, i) => before[i] != after[i])); + +var app = Backend.Build( + // the host's console log would carry the port and timings: this transcript is the output + new[] { "--urls", "http://127.0.0.1:0", "--Logging:LogLevel:Default=None" }, Database, clock); +await using (var setup = Fresh()) + await setup.Database.EnsureCreatedAsync(); +await app.StartAsync(); +try +{ + using var http = new HttpClient { BaseAddress = new Uri(app.Urls.First()) }; + + async Task<(HttpStatusCode Code, string Body, string? Location)> Send(HttpMethod method, string path, string? json = null) + { + using var request = new HttpRequestMessage(method, path); + if (json is not null) + request.Content = new StringContent(json, Encoding.UTF8, "application/json"); + using var response = await http.SendAsync(request); + return (response.StatusCode, await response.Content.ReadAsStringAsync(), response.Headers.Location?.OriginalString); + } + + Task<(HttpStatusCode Code, string Body, string? Location)> Post(string path, string? json = null) => Send(HttpMethod.Post, path, json); + Task<(HttpStatusCode Code, string Body, string? Location)> Get(string path) => Send(HttpMethod.Get, path); + + const string stamp = "2026-01-02 03:04:05"; // EF's SQLite text for the fixed clock + + Check("db-fresh", Scalar("SELECT COUNT(*) FROM Orders") == 0, + "EnsureCreated made the schema in a new database file: 0 rows"); + + // ---- P15: the HTTP happy path, one database, the raw row after every step --------------- + var created = await Post("/orders", "{\"customer\":\"alice\"}"); + Check("http-create", created.Code == HttpStatusCode.Created && created.Location == "/orders/1" + && created.Body == "{\"id\":1,\"status\":\"Draft\"}", + $"POST /orders -> {(int)created.Code} {created.Location} {created.Body}"); + Check("oracle-create", Show(Row(1)) == "1 | alice | Draft | NULL | NULL | NULL | NULL", + $"raw row: {Show(Row(1))}"); + + var step = await Post("/orders/1/submit"); + Check("http-submit", step.Code == HttpStatusCode.OK && step.Body == "{\"id\":1,\"status\":\"Submitted\"}", + $"POST /orders/1/submit -> {(int)step.Code} {step.Body}"); + Check("oracle-submit", Show(Row(1)) == $"1 | alice | Submitted | {stamp} | NULL | NULL | NULL", + $"raw row: {Show(Row(1))}"); + + step = await Post("/orders/1/approve"); + Check("http-approve", step.Code == HttpStatusCode.OK && step.Body == "{\"id\":1,\"status\":\"Approved\"}", + $"POST /orders/1/approve -> {(int)step.Code} {step.Body}"); + Check("oracle-approve", Show(Row(1)) == $"1 | alice | Approved | {stamp} | {stamp} | NULL | NULL", + $"raw row: {Show(Row(1))}"); + + var tracking = Shipping.TrackingNumber(1); + step = await Post("/orders/1/ship"); + Check("http-ship", step.Code == HttpStatusCode.OK + && step.Body == $"{{\"id\":1,\"status\":\"Shipped\",\"trackingNumber\":{tracking}}}", + $"POST /orders/1/ship -> {(int)step.Code} {step.Body}"); + Check("oracle-ship", Show(Row(1)) == $"1 | alice | Shipped | {stamp} | {stamp} | {stamp} | {tracking}", + $"raw row: {Show(Row(1))}"); + + var got = await Get("/orders/1"); + Check("http-get-shipped", got.Code == HttpStatusCode.OK && got.Body == + "{\"id\":1,\"customer\":\"alice\",\"status\":\"Shipped\",\"submittedAt\":\"2026-01-02T03:04:05\"," + + $"\"approvedAt\":\"2026-01-02T03:04:05\",\"shippedAt\":\"2026-01-02T03:04:05\",\"trackingNumber\":{tracking}}}", + $"GET /orders/1 -> {(int)got.Code} {got.Body}"); + + // ---- P14: the builder's required field, at the HTTP boundary ----------------------------- + var rows = Scalar("SELECT COUNT(*) FROM Orders"); + foreach (var body in new[] { "{}", "{\"customer\":\" \"}" }) + { + var bad = await Post("/orders", body); + Check("http-create-required", bad.Code == HttpStatusCode.BadRequest + && bad.Body == "{\"error\":\"customer_required\"}" && Scalar("SELECT COUNT(*) FROM Orders") == rows, + $"POST /orders {body} -> {(int)bad.Code} {bad.Body}, no row written"); + } + + // ---- H9: wrong runtime transitions are 409 and leave the row byte-identical --------------- + var b = await Post("/orders", "{\"customer\":\"bob\"}"); + Check("http-create-b", b.Code == HttpStatusCode.Created && b.Location == "/orders/2", $"second order -> {b.Location}"); + async Task Refused(string id, long order, string verb, string state, string required) + { + var before = Row(order); + var r = await Post($"/orders/{order}/{verb}"); + var after = Row(order); + Check(id, r.Code == HttpStatusCode.Conflict + && r.Body == $"{{\"error\":\"invalid_transition\",\"id\":{order},\"state\":\"{state}\",\"required\":\"{required}\"}}" + && Show(before) == Show(after), + $"{verb} {(state[0] == 'A' ? "an" : "a")} {state} order -> {(int)r.Code} {r.Body}; row unchanged: {Show(before) == Show(after)}"); + } + await Refused("h9-approve-draft", 2, "approve", "Draft", "Submitted"); + await Refused("h9-ship-draft", 2, "ship", "Draft", "Approved"); + Check("h9-b-submit", (await Post("/orders/2/submit")).Code == HttpStatusCode.OK && Row(2)?[2] == "Submitted", + "the legal submit in between goes through: Submitted"); + await Refused("h9-ship-submitted", 2, "ship", "Submitted", "Approved"); + await Refused("h9-submit-submitted", 2, "submit", "Submitted", "Draft"); + Check("h9-b-approve", (await Post("/orders/2/approve")).Code == HttpStatusCode.OK && Row(2)?[2] == "Approved", + "the legal approve in between goes through: Approved"); + await Refused("h9-submit-approved", 2, "submit", "Approved", "Draft"); + await Refused("h9-approve-approved", 2, "approve", "Approved", "Submitted"); + Check("h9-b-ship", (await Post("/orders/2/ship")).Code == HttpStatusCode.OK && Row(2)?[2] == "Shipped", + "the legal ship in between goes through: Shipped"); + await Refused("h9-submit-shipped", 2, "submit", "Shipped", "Draft"); + await Refused("h9-approve-shipped", 2, "approve", "Shipped", "Submitted"); + await Refused("h9-ship-shipped", 2, "ship", "Shipped", "Approved"); + + foreach (var verb in new[] { "submit", "approve", "ship" }) + { + var missing = await Post($"/orders/999999/{verb}"); + Check($"http-404-{verb}", missing.Code == HttpStatusCode.NotFound, $"{verb} an unknown id -> {(int)missing.Code}"); + } + Check("http-404-get", (await Get("/orders/999999")).Code == HttpStatusCode.NotFound, "GET an unknown id -> 404"); + + // ---- H8: a persisted state that is not a state never becomes a token --------------------- + foreach (var raw in new[] { "Bogus", "7", "approved", "" }) + { + var id = InsertRaw("mallory", raw); + var before = Row(id); + var answers = new List(); + foreach (var verb in new[] { "submit", "approve", "ship" }) + { + var r = await Post($"/orders/{id}/{verb}"); + answers.Add($"{verb}={(int)r.Code}"); + if (r.Code != HttpStatusCode.InternalServerError || r.Body != $"{{\"error\":\"corrupt_state\",\"id\":{id}}}") + answers.Add("WRONG:" + r.Body); + } + var g = await Get($"/orders/{id}"); + answers.Add($"get={(int)g.Code}"); + if (g.Code != HttpStatusCode.InternalServerError || g.Body != $"{{\"error\":\"corrupt_state\",\"id\":{id}}}") + answers.Add("WRONG:" + g.Body); + string thrown; + await using (var db = Fresh()) + { + try + { + var o = await db.Orders.SingleAsync(x => x.Id == id); + thrown = $"loaded as {o.Status}"; + } + catch (CorruptOrderStateException e) + { + thrown = $"CorruptOrderStateException('{e.Raw}')"; + } + } + Check($"h8-corrupt-'{raw}'", !answers.Any(a => a.StartsWith("WRONG", StringComparison.Ordinal)) + && thrown == $"CorruptOrderStateException('{raw}')" && Show(before) == Show(Row(id)), + $"stored '{raw}': {string.Join(" ", answers)}; EF load: {thrown}; row unchanged: {Show(before) == Show(Row(id))}"); + } + var storage = new List(); + foreach (var raw in new[] { "Bogus", "7", "approved", "", " Draft" }) + storage.Add(OrderStatusStorage.TryFromStore(raw, out _) ? $"'{raw}'=state" : $"'{raw}'=refused"); + try + { + OrderStatusStorage.ToStore((OrderStatus)7); + storage.Add("ToStore(7)=written"); + } + catch (CorruptOrderStateException) + { + storage.Add("ToStore(7)=refused"); + } + Check("h8-storage-strict", storage.All(s => s.EndsWith("refused", StringComparison.Ordinal)), + string.Join(" ", storage)); + + // ---- H10/H11: the typed transition writes the instance EF tracks, and nothing else ------- + long c; + await using (var db = Fresh()) + { + var fresh = Order.Create().Customer("carol").Build(); + Check("builder-draft", fresh.Status == OrderStatus.Draft && fresh.Customer == "carol" && fresh.Id == 0, + $"Order.Create().Customer(\"carol\").Build() is a new {fresh.Status} for {fresh.Customer}"); + db.Orders.Add(fresh); + await db.SaveChangesAsync(); + c = fresh.Id; + } + await using (var db = Fresh()) + { + var order = await db.Orders.SingleAsync(o => o.Id == c); + var entry = db.ChangeTracker.Entries().Single(); + Check("h10-same-instance-before", ReferenceEquals(entry.Entity, order) && entry.State == EntityState.Unchanged, + $"the queried Order IS the instance the ChangeTracker holds, {entry.State}"); + + var before = Row(c); + OrderProtocol.WithDraft(order, draft => + { + draft.Submit(now); + }); + db.ChangeTracker.DetectChanges(); + var modified = entry.Properties.Where(p => p.IsModified).Select(p => p.Metadata.Name).OrderBy(n => n, StringComparer.Ordinal); + Check("h10-same-instance-after", ReferenceEquals(db.ChangeTracker.Entries().Single().Entity, order) + && db.ChangeTracker.Entries().Count() == 1 && order.Status == OrderStatus.Submitted, + "after the region the tracked instance is still the queried one, now Submitted; one entry, nothing re-attached"); + Check("h10-tracked-change", entry.State == EntityState.Modified + && string.Join(",", modified) == "Status,SubmittedAt", + $"the ChangeTracker sees {entry.State}: {string.Join(",", modified)}"); + + var written = await db.SaveChangesAsync(); + var after = Row(c); + Check("h11-saved-exactly", written == 1 && Diff(before, after) == "Status,SubmittedAt" + && after![2] == "Submitted" && after[3] == stamp, + $"SaveChangesAsync wrote {written} row; raw columns changed: {Diff(before, after)}; raw row: {Show(after)}"); + } + + // ---- H12: reload, refine by the persisted state -------------------------------------- + await using (var db = Fresh()) + { + var order = await db.Orders.SingleAsync(o => o.Id == c); + string wrong; + try + { + OrderProtocol.WithDraft(order, draft => + { + draft.Submit(now); + }); + wrong = "admitted"; + } + catch (InvalidOrderStateException e) + { + wrong = $"InvalidOrderStateException({e.Actual}, required {e.Required})"; + } + var untouched = db.ChangeTracker.Entries().Single().State; + OrderProtocol.WithSubmitted(order, submitted => + { + submitted.Approve(now); + }); + await db.SaveChangesAsync(); + Check("h12-reload-refine", wrong == "InvalidOrderStateException(Submitted, required Draft)" + && untouched == EntityState.Unchanged && Row(c)?[2] == "Approved", + $"reloaded Submitted: WithDraft -> {wrong} ({untouched}); WithSubmitted -> Approve saved {Row(c)?[2]}"); + } + + // ---- H13: ordinary LINQ ---------------------------------------------------------------- + var list = await Get("/orders?status=Approved"); + Check("h13-linq-endpoint", list.Code == HttpStatusCode.OK && list.Body == $"[{{\"id\":{c},\"customer\":\"carol\"}}]", + $"GET /orders?status=Approved -> {(int)list.Code} {list.Body} (the corrupt 'approved' row is not Approved)"); + var unknown = await Get("/orders?status=approved"); + Check("h13-linq-unknown-status", unknown.Code == HttpStatusCode.BadRequest && unknown.Body == "{\"error\":\"unknown_status\"}", + $"GET /orders?status=approved -> {(int)unknown.Code} {unknown.Body}"); + await using (var db = Fresh()) + { + var text = db.Orders.Where(o => o.Status == OrderStatus.Approved).OrderBy(o => o.Id).Select(o => o.Id).ToQueryString(); + Check("h13-linq-translated", text.Contains("WHERE \"o\".\"Status\" = 'Approved'", StringComparison.Ordinal) + && text.Contains("ORDER BY", StringComparison.Ordinal), + "the predicate is server-side SQL over the stored name: WHERE \"o\".\"Status\" = 'Approved' ... ORDER BY"); + } + + string[] executed; + lock (sql) + executed = sql.ToArray(); + Check("ef-update-emitted", executed.Any(t => t.Contains("UPDATE \"Orders\" SET \"Status\"", StringComparison.Ordinal)), + "the transitions reach the database as ordinary UPDATE statements"); +} +finally +{ + await app.StopAsync(); + await app.DisposeAsync(); + SqliteConnection.ClearAllPools(); + try + { + File.Delete(dbPath); + } + catch (IOException) + { + } +} + +Console.WriteLine(failures == 0 + ? "typed builder acceptance: all checks hold" + : $"typed builder acceptance: {failures} check(s) FAILED"); +return failures == 0 ? 0 : 1; + +/// The backend's clock in this run: fixed, so the transcript is the same bytes every time. +sealed class FixedClock(DateTimeOffset at) : TimeProvider +{ + public override DateTimeOffset GetUtcNow() => at; +} diff --git a/samples/OrderBackend/OrderBackend/Data/OrdersDb.cs b/samples/OrderBackend/OrderBackend/Data/OrdersDb.cs new file mode 100644 index 00000000..0b41d0be --- /dev/null +++ b/samples/OrderBackend/OrderBackend/Data/OrdersDb.cs @@ -0,0 +1,24 @@ +using Microsoft.EntityFrameworkCore; +using OrderBackend.Domain; + +namespace OrderBackend.Data; + +/// A plain DbContext: no custom base, no repository, no interceptor, no query provider. +public sealed class OrdersDb(DbContextOptions options) : DbContext(options) +{ + public DbSet Orders => Set(); + + protected override void OnModelCreating(ModelBuilder modelBuilder) + { + modelBuilder.Entity(order => + { + order.HasKey(o => o.Id); + order.Property(o => o.Customer).IsRequired(); + // the exact member name, strictly: an unknown stored value is an exception at + // materialization, never a state (OrderStatusStorage is generated) + order.Property(o => o.Status).HasConversion( + state => OrderStatusStorage.ToStore(state), + raw => OrderStatusStorage.FromStore(raw)); + }); + } +} diff --git a/samples/OrderBackend/OrderBackend/Domain/Order.Protocol.cs b/samples/OrderBackend/OrderBackend/Domain/Order.Protocol.cs new file mode 100644 index 00000000..18b600af --- /dev/null +++ b/samples/OrderBackend/OrderBackend/Domain/Order.Protocol.cs @@ -0,0 +1,223 @@ +// Generated by Own.TypedBuilder from Order.cs. Do not edit: change Order.cs and regenerate. +// +// The state protocol of Order: one [ProtocolToken] per state, one transition per +// [Transition], one [ProtocolRegion] per state with a way out, the checked refinement, +// the strict storage of the state, and the staged builder. Own.NET analyses this file as +// source: it is the protocol's trusted definition surface. + +using System; + +namespace OrderBackend.Domain; + +partial class Order +{ + // Draft -> Submit -> Submitted + internal void ApplySubmit(DateTime at) + { + OnSubmit(at); + Status = OrderStatus.Submitted; + } + + // Submitted -> Approve -> Approved + internal void ApplyApprove(DateTime at) + { + OnApprove(at); + Status = OrderStatus.Approved; + } + + // Approved -> Ship -> Shipped + internal void ApplyShip(DateTime at, int trackingNumber) + { + OnShip(at, trackingNumber); + Status = OrderStatus.Shipped; + } + + /// Starts a new Order in its initial state, Draft. Build() exists only once every + /// required field was given. + public static DraftBuilder.CustomerStep Create() => new(); + + public sealed class DraftBuilder + { + private readonly string _customer; + + private DraftBuilder(string customer) + { + _customer = customer; + } + + public Order Build() => new() { Customer = _customer, Status = OrderStatus.Draft }; + + public sealed class CustomerStep + { + internal CustomerStep() + { + } + + public DraftBuilder Customer(string customer) + { + ArgumentNullException.ThrowIfNull(customer); + return new DraftBuilder(customer); + } + } + } +} + +/// The runtime half of the refinement: the state came from data, so it is checked once, +/// at the region entry. +public sealed class InvalidOrderStateException(int id, OrderStatus actual, OrderStatus required) + : InvalidOperationException($"order {id} is {actual}, not {required}") +{ + public int Id { get; } = id; + + public OrderStatus Actual { get; } = actual; + + public OrderStatus Required { get; } = required; +} + +/// A persisted state that is not exactly one of OrderStatus's names. Never mapped to a +/// state: no default, no case folding, no number. +public sealed class CorruptOrderStateException(string raw) + : InvalidOperationException($"the persisted order state '{raw}' is not an OrderStatus") +{ + public string Raw { get; } = raw; +} + +/// The one mapping between OrderStatus and its stored text: the exact member name. +public static class OrderStatusStorage +{ + public static string ToStore(OrderStatus state) => state switch + { + OrderStatus.Draft => "Draft", + OrderStatus.Submitted => "Submitted", + OrderStatus.Approved => "Approved", + OrderStatus.Shipped => "Shipped", + _ => throw new CorruptOrderStateException(state.ToString()), + }; + + public static OrderStatus FromStore(string raw) => + TryFromStore(raw, out var state) ? state : throw new CorruptOrderStateException(raw); + + public static bool TryFromStore(string? raw, out OrderStatus state) + { + switch (raw) + { + case "Draft": + state = OrderStatus.Draft; + return true; + case "Submitted": + state = OrderStatus.Submitted; + return true; + case "Approved": + state = OrderStatus.Approved; + return true; + case "Shipped": + state = OrderStatus.Shipped; + return true; + default: + state = default; + return false; + } + } +} + +/// Order in state Draft. A transition spends this token and hands back the next one. +[ProtocolToken] +public readonly ref struct DraftOrder +{ + private readonly Order _order; + + internal DraftOrder(Order order) => _order = order; + + public int Id => _order.Id; + + public SubmittedOrder Submit(DateTime at) + { + _order.ApplySubmit(at); + return new SubmittedOrder(_order); + } +} + +/// Order in state Submitted. A transition spends this token and hands back the next one. +[ProtocolToken] +public readonly ref struct SubmittedOrder +{ + private readonly Order _order; + + internal SubmittedOrder(Order order) => _order = order; + + public int Id => _order.Id; + + public ApprovedOrder Approve(DateTime at) + { + _order.ApplyApprove(at); + return new ApprovedOrder(_order); + } +} + +/// Order in state Approved. A transition spends this token and hands back the next one. +[ProtocolToken] +public readonly ref struct ApprovedOrder +{ + private readonly Order _order; + + internal ApprovedOrder(Order order) => _order = order; + + public int Id => _order.Id; + + public ShippedOrder Ship(DateTime at, int trackingNumber) + { + _order.ApplyShip(at, trackingNumber); + return new ShippedOrder(_order); + } +} + +/// Order in state Shipped. Terminal: no transition leaves it. +[ProtocolToken] +public readonly ref struct ShippedOrder +{ + private readonly Order _order; + + internal ShippedOrder(Order order) => _order = order; + + public int Id => _order.Id; +} + +public delegate void DraftRegion(DraftOrder draft); +public delegate void SubmittedRegion(SubmittedOrder submitted); +public delegate void ApprovedRegion(ApprovedOrder approved); + +/// The checked refinement: an Order whose state is only known at run time becomes a token +/// inside the callback, or the call throws and no token exists. A state no transition +/// leaves has no region: its token could never be spent. +public static class OrderProtocol +{ + [ProtocolRegion] + public static void WithDraft(Order order, DraftRegion body) + { + ArgumentNullException.ThrowIfNull(order); + ArgumentNullException.ThrowIfNull(body); + if (order.Status != OrderStatus.Draft) + throw new InvalidOrderStateException(order.Id, order.Status, OrderStatus.Draft); + body(new DraftOrder(order)); + } + + [ProtocolRegion] + public static void WithSubmitted(Order order, SubmittedRegion body) + { + ArgumentNullException.ThrowIfNull(order); + ArgumentNullException.ThrowIfNull(body); + if (order.Status != OrderStatus.Submitted) + throw new InvalidOrderStateException(order.Id, order.Status, OrderStatus.Submitted); + body(new SubmittedOrder(order)); + } + + [ProtocolRegion] + public static void WithApproved(Order order, ApprovedRegion body) + { + ArgumentNullException.ThrowIfNull(order); + ArgumentNullException.ThrowIfNull(body); + if (order.Status != OrderStatus.Approved) + throw new InvalidOrderStateException(order.Id, order.Status, OrderStatus.Approved); + body(new ApprovedOrder(order)); + } +} diff --git a/samples/OrderBackend/OrderBackend/Domain/Order.cs b/samples/OrderBackend/OrderBackend/Domain/Order.cs new file mode 100644 index 00000000..b68d67f7 --- /dev/null +++ b/samples/OrderBackend/OrderBackend/Domain/Order.cs @@ -0,0 +1,51 @@ +using System; + +namespace OrderBackend.Domain; + +public enum OrderStatus +{ + Draft, + Submitted, + Approved, + Shipped, +} + +/// An ordinary EF Core entity — no base class, no interface — and the declaration its +/// protocol is generated from (Order.Protocol.cs). EF materializes it through the private +/// constructor and tracks THIS instance; every state token wraps the same reference. +[TypedProtocol] +public sealed partial class Order +{ + private Order() + { + } + + public int Id { get; private set; } + + [BuilderRequired] + public string Customer { get; private set; } = ""; + + [ProtocolState] + public OrderStatus Status { get; private set; } + + public DateTime? SubmittedAt { get; private set; } + + public DateTime? ApprovedAt { get; private set; } + + public DateTime? ShippedAt { get; private set; } + + public int? TrackingNumber { get; private set; } + + [Transition("Submit", OrderStatus.Draft, OrderStatus.Submitted)] + private void OnSubmit(DateTime at) => SubmittedAt = at; + + [Transition("Approve", OrderStatus.Submitted, OrderStatus.Approved)] + private void OnApprove(DateTime at) => ApprovedAt = at; + + [Transition("Ship", OrderStatus.Approved, OrderStatus.Shipped)] + private void OnShip(DateTime at, int trackingNumber) + { + ShippedAt = at; + TrackingNumber = trackingNumber; + } +} diff --git a/samples/OrderBackend/OrderBackend/Domain/TypedBuilder.cs b/samples/OrderBackend/OrderBackend/Domain/TypedBuilder.cs new file mode 100644 index 00000000..405ea0c7 --- /dev/null +++ b/samples/OrderBackend/OrderBackend/Domain/TypedBuilder.cs @@ -0,0 +1,49 @@ +using System; + +namespace OrderBackend.Domain; + +// The Typed Builder vocabulary. Matched by NAME — by the generator +// (frontend/roslyn/Own.TypedBuilder) and by the Own.NET extractor — so the domain depends on +// neither of them. + +/// The entity whose state protocol is generated. A `partial class`. +[AttributeUsage(AttributeTargets.Class)] +public sealed class TypedProtocolAttribute : Attribute +{ +} + +/// The one property that holds the state. Its enum's first member is the initial state. +[AttributeUsage(AttributeTargets.Property)] +public sealed class ProtocolStateAttribute : Attribute +{ +} + +/// A field the builder demands before Build() exists. +[AttributeUsage(AttributeTargets.Property)] +public sealed class BuilderRequiredAttribute : Attribute +{ +} + +/// A transition: its name, the state it leaves, the state it enters. On a non-public hook +/// that writes the transition's data; the state itself is written by generated code. +[AttributeUsage(AttributeTargets.Method)] +public sealed class TransitionAttribute(string name, object from, object to) : Attribute +{ + public string Name { get; } = name; + + public object From { get; } = from; + + public object To { get; } = to; +} + +/// A state: a ref struct over the entity (Own.NET state-protocol profile). +[AttributeUsage(AttributeTargets.Struct)] +public sealed class ProtocolTokenAttribute : Attribute +{ +} + +/// A region entry: (entity, callback) (Own.NET state-protocol profile). +[AttributeUsage(AttributeTargets.Method)] +public sealed class ProtocolRegionAttribute : Attribute +{ +} diff --git a/samples/OrderBackend/OrderBackend/OrderBackend.csproj b/samples/OrderBackend/OrderBackend/OrderBackend.csproj new file mode 100644 index 00000000..e7903e27 --- /dev/null +++ b/samples/OrderBackend/OrderBackend/OrderBackend.csproj @@ -0,0 +1,15 @@ + + + + net8.0 + 12 + enable + enable + OrderBackend + + + + + + + diff --git a/samples/OrderBackend/OrderBackend/OrderEndpoints.cs b/samples/OrderBackend/OrderBackend/OrderEndpoints.cs new file mode 100644 index 00000000..241add42 --- /dev/null +++ b/samples/OrderBackend/OrderBackend/OrderEndpoints.cs @@ -0,0 +1,165 @@ +using System; +using System.Linq; +using System.Threading; +using System.Threading.Tasks; +using Microsoft.AspNetCore.Http; +using Microsoft.EntityFrameworkCore; +using OrderBackend.Data; +using OrderBackend.Domain; + +namespace OrderBackend; + +public sealed record CreateOrderRequest(string? Customer); + +/// The endpoints: ordinary ASP.NET Core + EF Core code. Each transition is a tracked load, the +/// checked refinement (`OrderProtocol.WithX`), ONE typed transition, and SaveChangesAsync. A +/// transition the state does not have is not a runtime check here: it has no method. +public static class OrderEndpoints +{ + public static async Task Create(CreateOrderRequest request, OrdersDb db, CancellationToken ct) + { + if (string.IsNullOrWhiteSpace(request.Customer)) + return Results.Json(new { error = "customer_required" }, statusCode: StatusCodes.Status400BadRequest); + + var order = Order.Create() + .Customer(request.Customer) + .Build(); + db.Orders.Add(order); + await db.SaveChangesAsync(ct); + return Results.Created($"/orders/{order.Id}", Summary(order)); + } + + public static async Task Submit(int id, OrdersDb db, TimeProvider clock, CancellationToken ct) + { + try + { + var order = await db.Orders.SingleOrDefaultAsync(o => o.Id == id, ct); + if (order is null) + return Results.NotFound(); + + var now = clock.GetUtcNow().UtcDateTime; + OrderProtocol.WithDraft(order, draft => + { + draft.Submit(now); + }); + + await db.SaveChangesAsync(ct); + return Results.Ok(Summary(order)); + } + catch (InvalidOrderStateException refused) + { + return Refused(refused); + } + catch (CorruptOrderStateException) + { + return Corrupt(id); + } + } + + public static async Task Approve(int id, OrdersDb db, TimeProvider clock, CancellationToken ct) + { + try + { + var order = await db.Orders.SingleOrDefaultAsync(o => o.Id == id, ct); + if (order is null) + return Results.NotFound(); + + var now = clock.GetUtcNow().UtcDateTime; + OrderProtocol.WithSubmitted(order, submitted => + { + submitted.Approve(now); + }); + + await db.SaveChangesAsync(ct); + return Results.Ok(Summary(order)); + } + catch (InvalidOrderStateException refused) + { + return Refused(refused); + } + catch (CorruptOrderStateException) + { + return Corrupt(id); + } + } + + public static async Task Ship(int id, OrdersDb db, TimeProvider clock, CancellationToken ct) + { + try + { + var order = await db.Orders.SingleOrDefaultAsync(o => o.Id == id, ct); + if (order is null) + return Results.NotFound(); + + var now = clock.GetUtcNow().UtcDateTime; + OrderProtocol.WithApproved(order, approved => + { + approved.Ship(now, Shipping.TrackingNumber(id)); + }); + + await db.SaveChangesAsync(ct); + return Results.Ok(new { order.Id, Status = OrderStatusStorage.ToStore(order.Status), order.TrackingNumber }); + } + catch (InvalidOrderStateException refused) + { + return Refused(refused); + } + catch (CorruptOrderStateException) + { + return Corrupt(id); + } + } + + public static async Task Get(int id, OrdersDb db, CancellationToken ct) + { + try + { + var order = await db.Orders.AsNoTracking().SingleOrDefaultAsync(o => o.Id == id, ct); + return order is null + ? Results.NotFound() + : Results.Ok(new + { + order.Id, + order.Customer, + Status = OrderStatusStorage.ToStore(order.Status), + order.SubmittedAt, + order.ApprovedAt, + order.ShippedAt, + order.TrackingNumber, + }); + } + catch (CorruptOrderStateException) + { + return Corrupt(id); + } + } + + /// Ordinary LINQ, translated by the provider: no typed state is involved in a query. + public static async Task List(string? status, OrdersDb db, CancellationToken ct) + { + if (!OrderStatusStorage.TryFromStore(status, out var wanted)) + return Results.Json(new { error = "unknown_status" }, statusCode: StatusCodes.Status400BadRequest); + + var rows = await db.Orders + .Where(o => o.Status == wanted) + .OrderBy(o => o.Id) + .Select(o => new { o.Id, o.Customer }) + .ToListAsync(ct); + return Results.Ok(rows); + } + + private static object Summary(Order order) => + new { order.Id, Status = OrderStatusStorage.ToStore(order.Status) }; + + private static IResult Refused(InvalidOrderStateException refused) => + Results.Json(new + { + error = "invalid_transition", + id = refused.Id, + state = refused.Actual.ToString(), + required = refused.Required.ToString(), + }, statusCode: StatusCodes.Status409Conflict); + + private static IResult Corrupt(int id) => + Results.Json(new { error = "corrupt_state", id }, statusCode: StatusCodes.Status500InternalServerError); +} diff --git a/samples/OrderBackend/OrderBackend/Program.cs b/samples/OrderBackend/OrderBackend/Program.cs new file mode 100644 index 00000000..081197c3 --- /dev/null +++ b/samples/OrderBackend/OrderBackend/Program.cs @@ -0,0 +1,41 @@ +using System; +using Microsoft.AspNetCore.Builder; +using Microsoft.EntityFrameworkCore; +using Microsoft.Extensions.DependencyInjection; +using OrderBackend; +using OrderBackend.Data; + +var app = Backend.Build(args, options => options.UseSqlite("Data Source=orders.db"), TimeProvider.System); + +using (var scope = app.Services.CreateScope()) + scope.ServiceProvider.GetRequiredService().Database.EnsureCreated(); + +app.Run(); + +public partial class Program +{ +} + +namespace OrderBackend +{ + /// The composition root, shared by `Program` and the acceptance runner so both serve + /// exactly the same endpoints over a real HTTP listener. + public static class Backend + { + public static WebApplication Build(string[] args, Action database, TimeProvider clock) + { + var builder = WebApplication.CreateBuilder(args); + builder.Services.AddDbContext(database); + builder.Services.AddSingleton(clock); + + var app = builder.Build(); + app.MapPost("/orders", OrderEndpoints.Create); + app.MapGet("/orders", OrderEndpoints.List); + app.MapGet("/orders/{id:int}", OrderEndpoints.Get); + app.MapPost("/orders/{id:int}/submit", OrderEndpoints.Submit); + app.MapPost("/orders/{id:int}/approve", OrderEndpoints.Approve); + app.MapPost("/orders/{id:int}/ship", OrderEndpoints.Ship); + return app; + } + } +} diff --git a/samples/OrderBackend/OrderBackend/Shipping.cs b/samples/OrderBackend/OrderBackend/Shipping.cs new file mode 100644 index 00000000..900d9cb1 --- /dev/null +++ b/samples/OrderBackend/OrderBackend/Shipping.cs @@ -0,0 +1,10 @@ +namespace OrderBackend; + +public static class Shipping +{ + /// The carrier's tracking number for an order: a pure function of its id. It is called + /// INSIDE the Ship region, where Own.NET admits a call only when the shared heap-effect + /// summaries prove it harmless (OwnIR `proven_call`): it touches no entity, no token, no + /// field and no static. + public static int TrackingNumber(int orderId) => 1_000_000 + orderId * 7_919 % 999_983; +} diff --git a/samples/OrderBackend/README.md b/samples/OrderBackend/README.md new file mode 100644 index 00000000..d1de74fa --- /dev/null +++ b/samples/OrderBackend/README.md @@ -0,0 +1,187 @@ +# OrderBackend: a typed Order lifecycle on ASP.NET Core + EF Core + +`Draft → Submitted → Approved → Shipped`, on one ordinary EF Core entity. The +states are types, so an illegal transition **does not compile**. A stale or copied +state, or the raw entity touched while a state is open, is **rejected by Own.NET**. +None of this changes EF Core: the instance the query returned is the one the +ChangeTracker tracks, the transitions save as ordinary `UPDATE`s, and ordinary LINQ +stays ordinary. + +> **Not claimed: concurrency.** Two requests racing on the same order are out of +> scope here: there is no concurrency token, and nothing below says the sample is +> correct under concurrent writes. The claim also does not cover writes that bypass +> the entity's C# surface: `ExecuteUpdate`, raw SQL, `Entry(order).Property(...)`, +> reflection, another process. Those belong to concurrency tokens, constraints and +> transactions. + +## 1. Declare the protocol + +`OrderBackend/Domain/Order.cs` is the only file you write. The entity is a plain +class: no base class, no interface. + +```csharp +public enum OrderStatus { Draft, Submitted, Approved, Shipped } // first member = initial state + +[TypedProtocol] +public sealed partial class Order +{ + private Order() { } + + public int Id { get; private set; } + + [BuilderRequired] + public string Customer { get; private set; } = ""; + + [ProtocolState] + public OrderStatus Status { get; private set; } + + public DateTime? SubmittedAt { get; private set; } + // ... ApprovedAt, ShippedAt, TrackingNumber + + [Transition("Submit", OrderStatus.Draft, OrderStatus.Submitted)] + private void OnSubmit(DateTime at) => SubmittedAt = at; + + [Transition("Approve", OrderStatus.Submitted, OrderStatus.Approved)] + private void OnApprove(DateTime at) => ApprovedAt = at; + + [Transition("Ship", OrderStatus.Approved, OrderStatus.Shipped)] + private void OnShip(DateTime at, int trackingNumber) { ShippedAt = at; TrackingNumber = trackingNumber; } +} +``` + +A transition's hook writes the transition's data. The **state** itself is +written by generated code, so a hook cannot send the order to the wrong state. + +## 2. Generate + +```sh +dotnet run --project frontend/roslyn/Own.TypedBuilder -- \ + samples/OrderBackend/OrderBackend/Domain/Order.cs \ + -o samples/OrderBackend/OrderBackend/Domain/Order.Protocol.cs +``` + +`Order.Protocol.cs` is committed and readable. Regenerate it whenever `Order.cs` +changes; the gate fails if the committed file is stale. Generation is +deterministic: same input, same bytes. The generator writes: + +| | | +|---|---| +| `DraftOrder`, `SubmittedOrder`, `ApprovedOrder`, `ShippedOrder` | one state type each: a `ref struct` over **the same** `Order` instance | +| `DraftOrder.Submit`, `SubmittedOrder.Approve`, `ApprovedOrder.Ship` | the only transitions. Each returns the next state; `ShippedOrder` has none | +| `OrderProtocol.WithDraft / WithSubmitted / WithApproved` | the checked way from a loaded `Order` to its state | +| `Order.Create().Customer(...).Build()` | the builder. `Build()` does not exist until `Customer` was given | +| `OrderStatusStorage` | the strict text mapping EF uses: an unknown stored value is an error, never a state | + +## 3. Create, refine, transition + +```csharp +// create: the builder only ever makes a Draft +var order = Order.Create().Customer("alice").Build(); +db.Orders.Add(order); +await db.SaveChangesAsync(ct); + +// later: an ordinary EF query, then the checked refinement, then the typed transition +var order = await db.Orders.SingleOrDefaultAsync(o => o.Id == id, ct); +OrderProtocol.WithApproved(order, approved => // throws InvalidOrderStateException unless Approved +{ + approved.Ship(now, Shipping.TrackingNumber(id)); +}); +await db.SaveChangesAsync(ct); +``` + +Inside the callback, code may use only the state value, plain locals and +operators, and calls Own.NET can prove harmless. `Shipping.TrackingNumber` is such +a call: a pure function, admitted by the effect summaries. A logger call, a +`SaveChanges`, or a helper that writes shared state is refused. Read the clock and +log **before** the callback, and save **after** it. + +Use a state only once. A transition you do not need further is written as a +plain statement (`draft.Submit(now);`). A state you bind to a variable must be +used. + +## 4. The illegal ones fail before anything runs + +```csharp +OrderProtocol.WithDraft(order, draft => draft.Approve(now)); +// error CS1061: 'DraftOrder' does not contain a definition for 'Approve' + +Order.Create().Build(); +// error CS1061: 'Order.DraftBuilder.CustomerStep' does not contain a definition for 'Build' +``` + +The compiler cannot see every mistake. Own.NET checks the rest: + +```sh +dotnet build samples/OrderBackend/OrderBackend +dotnet run --project frontend/roslyn/OwnSharp.Extractor -c Release -- \ + samples/OrderBackend/OrderBackend/OrderBackend.csproj --flow-locals -o facts.json +python -m ownlang ownir facts.json +``` + +```csharp +OrderProtocol.WithDraft(order, draft => +{ + var submitted = draft.Submit(now); + draft.Submit(now); // rejected: 'draft' was spent by the Submit above + submitted.Approve(now); +}); +``` + +```text +OrderBackend/C8_stale_draft.cs:18: error: [OWN002] IDisposable local 'draft' is used after it is disposed [resource: disposable] +``` + +The wording is the core's generic resource wording, and the line is the region's. The verdicts mean: +- **OWN002:** a state used after a transition spent it; +- **OWN005:** a copied state; +- **OWN013:** the raw entity touched while a state is open; +- **OWN001:** a bound state never used. + +`corpus/` holds the full set, each with the exact rejection it must produce: +- **8 programs that must pass**; +- **20 that must fail**: every illegal transition, stale and copied states, raw entity access, harmful calls inside the callback, a forged state, the builder without its required field; +- **2 stated limits.** + +## 5. Run it + +```sh +cd samples/OrderBackend +dotnet run --project OrderBackend # SQLite file orders.db, created on first start +``` + +```sh +curl -s -X POST localhost:5000/orders -H 'content-type: application/json' -d '{"customer":"alice"}' +# 201 {"id":1,"status":"Draft"} +curl -s -X POST localhost:5000/orders/1/submit # 200 {"id":1,"status":"Submitted"} +curl -s -X POST localhost:5000/orders/1/approve # 200 {"id":1,"status":"Approved"} +curl -s -X POST localhost:5000/orders/1/ship # 200 {"id":1,"status":"Shipped","trackingNumber":1007919} +curl -s localhost:5000/orders/1 # 200 {..."status":"Shipped"...} +curl -s 'localhost:5000/orders?status=Shipped' # 200 [{"id":1,"customer":"alice"}] +curl -s -X POST localhost:5000/orders/1/ship # 409 {"error":"invalid_transition",...} +``` + +| answer | when | +|---|---| +| `409 invalid_transition` | the order's stored state has no such transition. Nothing is written | +| `404` | no such order | +| `500 corrupt_state` | the stored state is not exactly one of the four names. It is never guessed | + +## Verify everything + +```sh +python scripts/typed_builder_gate.py # from the repository root +python scripts/typed_builder_gate.py --clean-checkout # the same, twice, in fresh worktrees of HEAD +``` + +The gate runs these steps: +1. generates the protocol twice and requires the same bytes, equal to the committed file; +2. builds the backend; +3. checks the backend with Own.NET; +4. holds every corpus program to its registered answer; +5. runs the acceptance twice. + +The acceptance (`Acceptance/`) is real HTTP against a real SQLite file. Its +oracles do not go through the typed API: +- **database:** raw SQL on its own connection; +- **object identity:** EF's ChangeTracker; +- **HTTP:** the exact responses. diff --git a/samples/OrderBackend/corpus/limits/K1_named_terminal_token.cs.txt b/samples/OrderBackend/corpus/limits/K1_named_terminal_token.cs.txt new file mode 100644 index 00000000..d7594c81 --- /dev/null +++ b/samples/OrderBackend/corpus/limits/K1_named_terminal_token.cs.txt @@ -0,0 +1,24 @@ +using System; +using System.Linq; +using System.Threading; +using System.Threading.Tasks; +using Microsoft.EntityFrameworkCore; +using OrderBackend.Data; +using OrderBackend.Domain; + +namespace OrderBackend.Corpus; + +// K1: a named terminal token is never spent. Linear tokens (G6): OWN001 today. +public static class K1NamedTerminalToken +{ + public static async Task Run(OrdersDb db, int id, CancellationToken ct) + { + var order = await db.Orders.SingleAsync(o => o.Id == id, ct); + var now = DateTime.UnixEpoch; + OrderProtocol.WithApproved(order, approved => + { + var shipped = approved.Ship(now, 1); + }); + await db.SaveChangesAsync(ct); + } +} diff --git a/samples/OrderBackend/corpus/limits/K2_execute_update.cs.txt b/samples/OrderBackend/corpus/limits/K2_execute_update.cs.txt new file mode 100644 index 00000000..66534743 --- /dev/null +++ b/samples/OrderBackend/corpus/limits/K2_execute_update.cs.txt @@ -0,0 +1,17 @@ +using System; +using System.Linq; +using System.Threading; +using System.Threading.Tasks; +using Microsoft.EntityFrameworkCore; +using OrderBackend.Data; +using OrderBackend.Domain; + +namespace OrderBackend.Corpus; + +// K2: ExecuteUpdate writes the state past every token. Outside the claim. +public static class K2ExecuteUpdate +{ + public static Task Run(OrdersDb db, int id, CancellationToken ct) => + db.Orders.Where(o => o.Id == id) + .ExecuteUpdateAsync(set => set.SetProperty(o => o.Status, OrderStatus.Shipped), ct); +} diff --git a/samples/OrderBackend/corpus/limits/expected.json b/samples/OrderBackend/corpus/limits/expected.json new file mode 100644 index 00000000..7fdf22c3 --- /dev/null +++ b/samples/OrderBackend/corpus/limits/expected.json @@ -0,0 +1,14 @@ +{ + "K1_named_terminal_token": { + "stage": "core", + "verdict": [ + "OWN001" + ], + "why": "tokens are linear, not affine (P-010; case G6): a named token must be spent, and a terminal one cannot be" + }, + "K2_execute_update": { + "stage": "core", + "verdict": [], + "why": "a bulk write has no entity instance for a token to guard: concurrency tokens, constraints and transactions own it" + } +} diff --git a/samples/OrderBackend/corpus/negative/C10a_raw_mutator.cs.txt b/samples/OrderBackend/corpus/negative/C10a_raw_mutator.cs.txt new file mode 100644 index 00000000..e6097e26 --- /dev/null +++ b/samples/OrderBackend/corpus/negative/C10a_raw_mutator.cs.txt @@ -0,0 +1,20 @@ +using System; +using System.Linq; +using System.Threading; +using System.Threading.Tasks; +using Microsoft.EntityFrameworkCore; +using OrderBackend.Data; +using OrderBackend.Domain; + +namespace OrderBackend.Corpus; + +// C10a: the raw entity's transition is called past every token, outside any region. +public static class C10aRawMutator +{ + public static async Task Run(OrdersDb db, int id, CancellationToken ct) + { + var order = await db.Orders.SingleAsync(o => o.Id == id, ct); + order.ApplyShip(DateTime.UnixEpoch, 1); + await db.SaveChangesAsync(ct); + } +} diff --git a/samples/OrderBackend/corpus/negative/C10b_raw_entity_in_region.cs.txt b/samples/OrderBackend/corpus/negative/C10b_raw_entity_in_region.cs.txt new file mode 100644 index 00000000..365356a4 --- /dev/null +++ b/samples/OrderBackend/corpus/negative/C10b_raw_entity_in_region.cs.txt @@ -0,0 +1,25 @@ +using System; +using System.Linq; +using System.Threading; +using System.Threading.Tasks; +using Microsoft.EntityFrameworkCore; +using OrderBackend.Data; +using OrderBackend.Domain; + +namespace OrderBackend.Corpus; + +// C10b: the raw entity is touched inside the region that borrows it. +public static class C10bRawEntityInRegion +{ + public static async Task Run(OrdersDb db, int id, CancellationToken ct) + { + var order = await db.Orders.SingleAsync(o => o.Id == id, ct); + var now = DateTime.UnixEpoch; + OrderProtocol.WithDraft(order, draft => + { + draft.Submit(now); + var customer = order.Customer; + }); + await db.SaveChangesAsync(ct); + } +} diff --git a/samples/OrderBackend/corpus/negative/C10c_raw_state_write.cs.txt b/samples/OrderBackend/corpus/negative/C10c_raw_state_write.cs.txt new file mode 100644 index 00000000..d94692ef --- /dev/null +++ b/samples/OrderBackend/corpus/negative/C10c_raw_state_write.cs.txt @@ -0,0 +1,20 @@ +using System; +using System.Linq; +using System.Threading; +using System.Threading.Tasks; +using Microsoft.EntityFrameworkCore; +using OrderBackend.Data; +using OrderBackend.Domain; + +namespace OrderBackend.Corpus; + +// C10c: the state's setter is private. +public static class C10cRawStateWrite +{ + public static async Task Run(OrdersDb db, int id, CancellationToken ct) + { + var order = await db.Orders.SingleAsync(o => o.Id == id, ct); + order.Status = OrderStatus.Shipped; + await db.SaveChangesAsync(ct); + } +} diff --git a/samples/OrderBackend/corpus/negative/C11a_token_copy.cs.txt b/samples/OrderBackend/corpus/negative/C11a_token_copy.cs.txt new file mode 100644 index 00000000..706380cb --- /dev/null +++ b/samples/OrderBackend/corpus/negative/C11a_token_copy.cs.txt @@ -0,0 +1,26 @@ +using System; +using System.Linq; +using System.Threading; +using System.Threading.Tasks; +using Microsoft.EntityFrameworkCore; +using OrderBackend.Data; +using OrderBackend.Domain; + +namespace OrderBackend.Corpus; + +// C11a: a token copy is a move; the source is dead. +public static class C11aTokenCopy +{ + public static async Task Run(OrdersDb db, int id, CancellationToken ct) + { + var order = await db.Orders.SingleAsync(o => o.Id == id, ct); + var now = DateTime.UnixEpoch; + OrderProtocol.WithDraft(order, draft => + { + var copy = draft; + draft.Submit(now); + copy.Submit(now); + }); + await db.SaveChangesAsync(ct); + } +} diff --git a/samples/OrderBackend/corpus/negative/C11b_entity_alias.cs.txt b/samples/OrderBackend/corpus/negative/C11b_entity_alias.cs.txt new file mode 100644 index 00000000..d1f53bd3 --- /dev/null +++ b/samples/OrderBackend/corpus/negative/C11b_entity_alias.cs.txt @@ -0,0 +1,25 @@ +using System; +using System.Linq; +using System.Threading; +using System.Threading.Tasks; +using Microsoft.EntityFrameworkCore; +using OrderBackend.Data; +using OrderBackend.Domain; + +namespace OrderBackend.Corpus; + +// C11b: an alias of the borrowed entity, inside the region. +public static class C11bEntityAlias +{ + public static async Task Run(OrdersDb db, int id, CancellationToken ct) + { + var order = await db.Orders.SingleAsync(o => o.Id == id, ct); + var now = DateTime.UnixEpoch; + OrderProtocol.WithDraft(order, draft => + { + var alias = order; + draft.Submit(now); + }); + await db.SaveChangesAsync(ct); + } +} diff --git a/samples/OrderBackend/corpus/negative/C12a_harmful_helper.cs.txt b/samples/OrderBackend/corpus/negative/C12a_harmful_helper.cs.txt new file mode 100644 index 00000000..cfb16224 --- /dev/null +++ b/samples/OrderBackend/corpus/negative/C12a_harmful_helper.cs.txt @@ -0,0 +1,31 @@ +using System; +using System.Linq; +using System.Threading; +using System.Threading.Tasks; +using Microsoft.EntityFrameworkCore; +using OrderBackend.Data; +using OrderBackend.Domain; + +namespace OrderBackend.Corpus; + +// C12a: a direct helper that writes a static, inside the region. +public static class C12aHarmfulHelper +{ + public static async Task Run(OrdersDb db, int id, CancellationToken ct) + { + var order = await db.Orders.SingleAsync(o => o.Id == id, ct); + var now = DateTime.UnixEpoch; + OrderProtocol.WithApproved(order, approved => + { + approved.Ship(now, Counter.Next()); + }); + await db.SaveChangesAsync(ct); + } + + private static class Counter + { + private static int _last; + + public static int Next() => ++_last; + } +} diff --git a/samples/OrderBackend/corpus/negative/C12b_logger_in_region.cs.txt b/samples/OrderBackend/corpus/negative/C12b_logger_in_region.cs.txt new file mode 100644 index 00000000..80ea70ee --- /dev/null +++ b/samples/OrderBackend/corpus/negative/C12b_logger_in_region.cs.txt @@ -0,0 +1,25 @@ +using System; +using System.Linq; +using System.Threading; +using System.Threading.Tasks; +using Microsoft.EntityFrameworkCore; +using OrderBackend.Data; +using OrderBackend.Domain; + +namespace OrderBackend.Corpus; + +// C12b: a logger call inside the region: an external call with no stated contract. +public static class C12bLoggerInRegion +{ + public static async Task Run(OrdersDb db, int id, Microsoft.Extensions.Logging.ILogger log, CancellationToken ct) + { + var order = await db.Orders.SingleAsync(o => o.Id == id, ct); + var now = DateTime.UnixEpoch; + OrderProtocol.WithApproved(order, approved => + { + Microsoft.Extensions.Logging.LoggerExtensions.LogInformation(log, "shipping"); + approved.Ship(now, 1); + }); + await db.SaveChangesAsync(ct); + } +} diff --git a/samples/OrderBackend/corpus/negative/C13_builder_without_customer.cs.txt b/samples/OrderBackend/corpus/negative/C13_builder_without_customer.cs.txt new file mode 100644 index 00000000..4036dd69 --- /dev/null +++ b/samples/OrderBackend/corpus/negative/C13_builder_without_customer.cs.txt @@ -0,0 +1,15 @@ +using System; +using System.Linq; +using System.Threading; +using System.Threading.Tasks; +using Microsoft.EntityFrameworkCore; +using OrderBackend.Data; +using OrderBackend.Domain; + +namespace OrderBackend.Corpus; + +// C13: Build() does not exist before the required Customer was given. +public static class C13BuilderWithoutCustomer +{ + public static Order Run() => Order.Create().Build(); +} diff --git a/samples/OrderBackend/corpus/negative/C14_forged_token.cs.txt b/samples/OrderBackend/corpus/negative/C14_forged_token.cs.txt new file mode 100644 index 00000000..70787fbb --- /dev/null +++ b/samples/OrderBackend/corpus/negative/C14_forged_token.cs.txt @@ -0,0 +1,20 @@ +using System; +using System.Linq; +using System.Threading; +using System.Threading.Tasks; +using Microsoft.EntityFrameworkCore; +using OrderBackend.Data; +using OrderBackend.Domain; + +namespace OrderBackend.Corpus; + +// C14: a token made by hand, outside the protocol's own types. +public static class C14ForgedToken +{ + public static async Task Run(OrdersDb db, int id, CancellationToken ct) + { + var order = await db.Orders.SingleAsync(o => o.Id == id, ct); + new ApprovedOrder(order).Ship(DateTime.UnixEpoch, 1); + await db.SaveChangesAsync(ct); + } +} diff --git a/samples/OrderBackend/corpus/negative/C15_entity_constructor.cs.txt b/samples/OrderBackend/corpus/negative/C15_entity_constructor.cs.txt new file mode 100644 index 00000000..86ff5cda --- /dev/null +++ b/samples/OrderBackend/corpus/negative/C15_entity_constructor.cs.txt @@ -0,0 +1,15 @@ +using System; +using System.Linq; +using System.Threading; +using System.Threading.Tasks; +using Microsoft.EntityFrameworkCore; +using OrderBackend.Data; +using OrderBackend.Domain; + +namespace OrderBackend.Corpus; + +// C15: the entity has no public constructor: the builder is the way in. +public static class C15EntityConstructor +{ + public static Order Run() => new Order(); +} diff --git a/samples/OrderBackend/corpus/negative/C1_draft_approve.cs.txt b/samples/OrderBackend/corpus/negative/C1_draft_approve.cs.txt new file mode 100644 index 00000000..f0c01211 --- /dev/null +++ b/samples/OrderBackend/corpus/negative/C1_draft_approve.cs.txt @@ -0,0 +1,24 @@ +using System; +using System.Linq; +using System.Threading; +using System.Threading.Tasks; +using Microsoft.EntityFrameworkCore; +using OrderBackend.Data; +using OrderBackend.Domain; + +namespace OrderBackend.Corpus; + +// C1: Draft has no Approve. +public static class C1DraftApprove +{ + public static async Task Run(OrdersDb db, int id, CancellationToken ct) + { + var order = await db.Orders.SingleAsync(o => o.Id == id, ct); + var now = DateTime.UnixEpoch; + OrderProtocol.WithDraft(order, draft => + { + draft.Approve(now); + }); + await db.SaveChangesAsync(ct); + } +} diff --git a/samples/OrderBackend/corpus/negative/C2_draft_ship.cs.txt b/samples/OrderBackend/corpus/negative/C2_draft_ship.cs.txt new file mode 100644 index 00000000..ea68f05a --- /dev/null +++ b/samples/OrderBackend/corpus/negative/C2_draft_ship.cs.txt @@ -0,0 +1,24 @@ +using System; +using System.Linq; +using System.Threading; +using System.Threading.Tasks; +using Microsoft.EntityFrameworkCore; +using OrderBackend.Data; +using OrderBackend.Domain; + +namespace OrderBackend.Corpus; + +// C2: Draft has no Ship. +public static class C2DraftShip +{ + public static async Task Run(OrdersDb db, int id, CancellationToken ct) + { + var order = await db.Orders.SingleAsync(o => o.Id == id, ct); + var now = DateTime.UnixEpoch; + OrderProtocol.WithDraft(order, draft => + { + draft.Ship(now, 1); + }); + await db.SaveChangesAsync(ct); + } +} diff --git a/samples/OrderBackend/corpus/negative/C3_submitted_submit.cs.txt b/samples/OrderBackend/corpus/negative/C3_submitted_submit.cs.txt new file mode 100644 index 00000000..e2e65067 --- /dev/null +++ b/samples/OrderBackend/corpus/negative/C3_submitted_submit.cs.txt @@ -0,0 +1,24 @@ +using System; +using System.Linq; +using System.Threading; +using System.Threading.Tasks; +using Microsoft.EntityFrameworkCore; +using OrderBackend.Data; +using OrderBackend.Domain; + +namespace OrderBackend.Corpus; + +// C3: Submitted has no Submit. +public static class C3SubmittedSubmit +{ + public static async Task Run(OrdersDb db, int id, CancellationToken ct) + { + var order = await db.Orders.SingleAsync(o => o.Id == id, ct); + var now = DateTime.UnixEpoch; + OrderProtocol.WithSubmitted(order, submitted => + { + submitted.Submit(now); + }); + await db.SaveChangesAsync(ct); + } +} diff --git a/samples/OrderBackend/corpus/negative/C4_submitted_ship.cs.txt b/samples/OrderBackend/corpus/negative/C4_submitted_ship.cs.txt new file mode 100644 index 00000000..c2f472dd --- /dev/null +++ b/samples/OrderBackend/corpus/negative/C4_submitted_ship.cs.txt @@ -0,0 +1,24 @@ +using System; +using System.Linq; +using System.Threading; +using System.Threading.Tasks; +using Microsoft.EntityFrameworkCore; +using OrderBackend.Data; +using OrderBackend.Domain; + +namespace OrderBackend.Corpus; + +// C4: Submitted has no Ship. +public static class C4SubmittedShip +{ + public static async Task Run(OrdersDb db, int id, CancellationToken ct) + { + var order = await db.Orders.SingleAsync(o => o.Id == id, ct); + var now = DateTime.UnixEpoch; + OrderProtocol.WithSubmitted(order, submitted => + { + submitted.Ship(now, 1); + }); + await db.SaveChangesAsync(ct); + } +} diff --git a/samples/OrderBackend/corpus/negative/C5_approved_submit.cs.txt b/samples/OrderBackend/corpus/negative/C5_approved_submit.cs.txt new file mode 100644 index 00000000..cb70fdaa --- /dev/null +++ b/samples/OrderBackend/corpus/negative/C5_approved_submit.cs.txt @@ -0,0 +1,24 @@ +using System; +using System.Linq; +using System.Threading; +using System.Threading.Tasks; +using Microsoft.EntityFrameworkCore; +using OrderBackend.Data; +using OrderBackend.Domain; + +namespace OrderBackend.Corpus; + +// C5: Approved has no Submit. +public static class C5ApprovedSubmit +{ + public static async Task Run(OrdersDb db, int id, CancellationToken ct) + { + var order = await db.Orders.SingleAsync(o => o.Id == id, ct); + var now = DateTime.UnixEpoch; + OrderProtocol.WithApproved(order, approved => + { + approved.Submit(now); + }); + await db.SaveChangesAsync(ct); + } +} diff --git a/samples/OrderBackend/corpus/negative/C6_approved_approve.cs.txt b/samples/OrderBackend/corpus/negative/C6_approved_approve.cs.txt new file mode 100644 index 00000000..31446489 --- /dev/null +++ b/samples/OrderBackend/corpus/negative/C6_approved_approve.cs.txt @@ -0,0 +1,24 @@ +using System; +using System.Linq; +using System.Threading; +using System.Threading.Tasks; +using Microsoft.EntityFrameworkCore; +using OrderBackend.Data; +using OrderBackend.Domain; + +namespace OrderBackend.Corpus; + +// C6: Approved has no Approve. +public static class C6ApprovedApprove +{ + public static async Task Run(OrdersDb db, int id, CancellationToken ct) + { + var order = await db.Orders.SingleAsync(o => o.Id == id, ct); + var now = DateTime.UnixEpoch; + OrderProtocol.WithApproved(order, approved => + { + approved.Approve(now); + }); + await db.SaveChangesAsync(ct); + } +} diff --git a/samples/OrderBackend/corpus/negative/C7_shipped_transition.cs.txt b/samples/OrderBackend/corpus/negative/C7_shipped_transition.cs.txt new file mode 100644 index 00000000..8c9a9027 --- /dev/null +++ b/samples/OrderBackend/corpus/negative/C7_shipped_transition.cs.txt @@ -0,0 +1,24 @@ +using System; +using System.Linq; +using System.Threading; +using System.Threading.Tasks; +using Microsoft.EntityFrameworkCore; +using OrderBackend.Data; +using OrderBackend.Domain; + +namespace OrderBackend.Corpus; + +// C7: Shipped is terminal: the token it hands back has no transition. +public static class C7ShippedTransition +{ + public static async Task Run(OrdersDb db, int id, CancellationToken ct) + { + var order = await db.Orders.SingleAsync(o => o.Id == id, ct); + var now = DateTime.UnixEpoch; + OrderProtocol.WithApproved(order, approved => + { + approved.Ship(now, 1).Submit(now); + }); + await db.SaveChangesAsync(ct); + } +} diff --git a/samples/OrderBackend/corpus/negative/C7b_shipped_region.cs.txt b/samples/OrderBackend/corpus/negative/C7b_shipped_region.cs.txt new file mode 100644 index 00000000..3494c138 --- /dev/null +++ b/samples/OrderBackend/corpus/negative/C7b_shipped_region.cs.txt @@ -0,0 +1,23 @@ +using System; +using System.Linq; +using System.Threading; +using System.Threading.Tasks; +using Microsoft.EntityFrameworkCore; +using OrderBackend.Data; +using OrderBackend.Domain; + +namespace OrderBackend.Corpus; + +// C7b: a terminal state has no region entry. +public static class C7bShippedRegion +{ + public static async Task Run(OrdersDb db, int id, CancellationToken ct) + { + var order = await db.Orders.SingleAsync(o => o.Id == id, ct); + var now = DateTime.UnixEpoch; + OrderProtocol.WithShipped(order, shipped => + { + }); + await db.SaveChangesAsync(ct); + } +} diff --git a/samples/OrderBackend/corpus/negative/C8_stale_draft.cs.txt b/samples/OrderBackend/corpus/negative/C8_stale_draft.cs.txt new file mode 100644 index 00000000..c0255128 --- /dev/null +++ b/samples/OrderBackend/corpus/negative/C8_stale_draft.cs.txt @@ -0,0 +1,26 @@ +using System; +using System.Linq; +using System.Threading; +using System.Threading.Tasks; +using Microsoft.EntityFrameworkCore; +using OrderBackend.Data; +using OrderBackend.Domain; + +namespace OrderBackend.Corpus; + +// C8: the Draft token is spent by Submit; using it again is a use after a transition. +public static class C8StaleDraft +{ + public static async Task Run(OrdersDb db, int id, CancellationToken ct) + { + var order = await db.Orders.SingleAsync(o => o.Id == id, ct); + var now = DateTime.UnixEpoch; + OrderProtocol.WithDraft(order, draft => + { + var submitted = draft.Submit(now); + draft.Submit(now); + submitted.Approve(now); + }); + await db.SaveChangesAsync(ct); + } +} diff --git a/samples/OrderBackend/corpus/negative/C9_stale_submitted.cs.txt b/samples/OrderBackend/corpus/negative/C9_stale_submitted.cs.txt new file mode 100644 index 00000000..6147dd15 --- /dev/null +++ b/samples/OrderBackend/corpus/negative/C9_stale_submitted.cs.txt @@ -0,0 +1,26 @@ +using System; +using System.Linq; +using System.Threading; +using System.Threading.Tasks; +using Microsoft.EntityFrameworkCore; +using OrderBackend.Data; +using OrderBackend.Domain; + +namespace OrderBackend.Corpus; + +// C9: the Submitted token is spent by Approve; using it again is a use after a transition. +public static class C9StaleSubmitted +{ + public static async Task Run(OrdersDb db, int id, CancellationToken ct) + { + var order = await db.Orders.SingleAsync(o => o.Id == id, ct); + var now = DateTime.UnixEpoch; + OrderProtocol.WithSubmitted(order, submitted => + { + var approved = submitted.Approve(now); + submitted.Approve(now); + approved.Ship(now, 1); + }); + await db.SaveChangesAsync(ct); + } +} diff --git a/samples/OrderBackend/corpus/negative/expected.json b/samples/OrderBackend/corpus/negative/expected.json new file mode 100644 index 00000000..d5fc3bc4 --- /dev/null +++ b/samples/OrderBackend/corpus/negative/expected.json @@ -0,0 +1,103 @@ +{ + "C10a_raw_mutator": { + "stage": "extractor", + "text": "'ApplyShip' of 'Order' is not public and belongs to a state protocol" + }, + "C10b_raw_entity_in_region": { + "stage": "core", + "verdict": [ + "OWN013" + ] + }, + "C10c_raw_state_write": { + "stage": "compiler", + "code": "CS0272", + "member": "Status" + }, + "C11a_token_copy": { + "stage": "core", + "verdict": [ + "OWN005" + ] + }, + "C11b_entity_alias": { + "stage": "core", + "verdict": [ + "OWN013" + ] + }, + "C12a_harmful_helper": { + "stage": "core", + "refusal": "'OrderBackend.Corpus.C12aHarmfulHelper.Counter.Next()': writes.static is may" + }, + "C12b_logger_in_region": { + "stage": "extractor", + "text": "LoggerExtensions.LogInformation' inside a protocol region runs code with no stated contract" + }, + "C13_builder_without_customer": { + "stage": "compiler", + "code": "CS1061", + "member": "Build" + }, + "C14_forged_token": { + "stage": "extractor", + "text": "a protocol token 'ApprovedOrder' is created outside the protocol's own types" + }, + "C15_entity_constructor": { + "stage": "compiler", + "code": "CS0122", + "member": "Order" + }, + "C1_draft_approve": { + "stage": "compiler", + "code": "CS1061", + "member": "Approve" + }, + "C2_draft_ship": { + "stage": "compiler", + "code": "CS1061", + "member": "Ship" + }, + "C3_submitted_submit": { + "stage": "compiler", + "code": "CS1061", + "member": "Submit" + }, + "C4_submitted_ship": { + "stage": "compiler", + "code": "CS1061", + "member": "Ship" + }, + "C5_approved_submit": { + "stage": "compiler", + "code": "CS1061", + "member": "Submit" + }, + "C6_approved_approve": { + "stage": "compiler", + "code": "CS1061", + "member": "Approve" + }, + "C7_shipped_transition": { + "stage": "compiler", + "code": "CS1061", + "member": "Submit" + }, + "C7b_shipped_region": { + "stage": "compiler", + "code": "CS0117", + "member": "WithShipped" + }, + "C8_stale_draft": { + "stage": "core", + "verdict": [ + "OWN002" + ] + }, + "C9_stale_submitted": { + "stage": "core", + "verdict": [ + "OWN002" + ] + } +} diff --git a/samples/OrderBackend/corpus/positive/P1_create_draft.cs.txt b/samples/OrderBackend/corpus/positive/P1_create_draft.cs.txt new file mode 100644 index 00000000..90c7ba51 --- /dev/null +++ b/samples/OrderBackend/corpus/positive/P1_create_draft.cs.txt @@ -0,0 +1,23 @@ +using System; +using System.Linq; +using System.Threading; +using System.Threading.Tasks; +using Microsoft.EntityFrameworkCore; +using OrderBackend.Data; +using OrderBackend.Domain; + +namespace OrderBackend.Corpus; + +// P1: a Draft is created through the typed builder, added and saved. +public static class P1CreateDraft +{ + public static async Task Run(OrdersDb db, CancellationToken ct) + { + var order = Order.Create() + .Customer("alice") + .Build(); + db.Orders.Add(order); + await db.SaveChangesAsync(ct); + return order.Id; + } +} diff --git a/samples/OrderBackend/corpus/positive/P2_draft_submit.cs.txt b/samples/OrderBackend/corpus/positive/P2_draft_submit.cs.txt new file mode 100644 index 00000000..830fc688 --- /dev/null +++ b/samples/OrderBackend/corpus/positive/P2_draft_submit.cs.txt @@ -0,0 +1,24 @@ +using System; +using System.Linq; +using System.Threading; +using System.Threading.Tasks; +using Microsoft.EntityFrameworkCore; +using OrderBackend.Data; +using OrderBackend.Domain; + +namespace OrderBackend.Corpus; + +// P2: Draft -> Submitted. +public static class P2DraftSubmit +{ + public static async Task Run(OrdersDb db, int id, CancellationToken ct) + { + var order = await db.Orders.SingleAsync(o => o.Id == id, ct); + var now = DateTime.UnixEpoch; + OrderProtocol.WithDraft(order, draft => + { + draft.Submit(now); + }); + await db.SaveChangesAsync(ct); + } +} diff --git a/samples/OrderBackend/corpus/positive/P3_submitted_approve.cs.txt b/samples/OrderBackend/corpus/positive/P3_submitted_approve.cs.txt new file mode 100644 index 00000000..785bdcb3 --- /dev/null +++ b/samples/OrderBackend/corpus/positive/P3_submitted_approve.cs.txt @@ -0,0 +1,24 @@ +using System; +using System.Linq; +using System.Threading; +using System.Threading.Tasks; +using Microsoft.EntityFrameworkCore; +using OrderBackend.Data; +using OrderBackend.Domain; + +namespace OrderBackend.Corpus; + +// P3: Submitted -> Approved. +public static class P3SubmittedApprove +{ + public static async Task Run(OrdersDb db, int id, CancellationToken ct) + { + var order = await db.Orders.SingleAsync(o => o.Id == id, ct); + var now = DateTime.UnixEpoch; + OrderProtocol.WithSubmitted(order, submitted => + { + submitted.Approve(now); + }); + await db.SaveChangesAsync(ct); + } +} diff --git a/samples/OrderBackend/corpus/positive/P4_approved_ship.cs.txt b/samples/OrderBackend/corpus/positive/P4_approved_ship.cs.txt new file mode 100644 index 00000000..a424eb90 --- /dev/null +++ b/samples/OrderBackend/corpus/positive/P4_approved_ship.cs.txt @@ -0,0 +1,24 @@ +using System; +using System.Linq; +using System.Threading; +using System.Threading.Tasks; +using Microsoft.EntityFrameworkCore; +using OrderBackend.Data; +using OrderBackend.Domain; + +namespace OrderBackend.Corpus; + +// P4: Approved -> Shipped. +public static class P4ApprovedShip +{ + public static async Task Run(OrdersDb db, int id, CancellationToken ct) + { + var order = await db.Orders.SingleAsync(o => o.Id == id, ct); + var now = DateTime.UnixEpoch; + OrderProtocol.WithApproved(order, approved => + { + approved.Ship(now, 1_000_001); + }); + await db.SaveChangesAsync(ct); + } +} diff --git a/samples/OrderBackend/corpus/positive/P5_harmless_helper.cs.txt b/samples/OrderBackend/corpus/positive/P5_harmless_helper.cs.txt new file mode 100644 index 00000000..83fdbb22 --- /dev/null +++ b/samples/OrderBackend/corpus/positive/P5_harmless_helper.cs.txt @@ -0,0 +1,24 @@ +using System; +using System.Linq; +using System.Threading; +using System.Threading.Tasks; +using Microsoft.EntityFrameworkCore; +using OrderBackend.Data; +using OrderBackend.Domain; + +namespace OrderBackend.Corpus; + +// P5: a harmless direct helper inside the region: admitted as an OwnIR proven_call. +public static class P5HarmlessHelper +{ + public static async Task Run(OrdersDb db, int id, CancellationToken ct) + { + var order = await db.Orders.SingleAsync(o => o.Id == id, ct); + var now = DateTime.UnixEpoch; + OrderProtocol.WithApproved(order, approved => + { + approved.Ship(now, Shipping.TrackingNumber(id)); + }); + await db.SaveChangesAsync(ct); + } +} diff --git a/samples/OrderBackend/corpus/positive/P6_load_refine_transition.cs.txt b/samples/OrderBackend/corpus/positive/P6_load_refine_transition.cs.txt new file mode 100644 index 00000000..2eb8cabd --- /dev/null +++ b/samples/OrderBackend/corpus/positive/P6_load_refine_transition.cs.txt @@ -0,0 +1,34 @@ +using System; +using System.Linq; +using System.Threading; +using System.Threading.Tasks; +using Microsoft.EntityFrameworkCore; +using OrderBackend.Data; +using OrderBackend.Domain; + +namespace OrderBackend.Corpus; + +// P6: an EF tracked load, the checked refinement, a transition, SaveChangesAsync. +public static class P6LoadRefineTransition +{ + public static async Task Run(OrdersDb db, int id, CancellationToken ct) + { + var order = await db.Orders.SingleOrDefaultAsync(o => o.Id == id, ct); + if (order is null) + return false; + var now = DateTime.UnixEpoch; + try + { + OrderProtocol.WithDraft(order, draft => + { + draft.Submit(now); + }); + } + catch (InvalidOrderStateException) + { + return false; + } + await db.SaveChangesAsync(ct); + return true; + } +} diff --git a/samples/OrderBackend/corpus/positive/P7_linq_before_refinement.cs.txt b/samples/OrderBackend/corpus/positive/P7_linq_before_refinement.cs.txt new file mode 100644 index 00000000..fb072ca4 --- /dev/null +++ b/samples/OrderBackend/corpus/positive/P7_linq_before_refinement.cs.txt @@ -0,0 +1,29 @@ +using System; +using System.Linq; +using System.Threading; +using System.Threading.Tasks; +using Microsoft.EntityFrameworkCore; +using OrderBackend.Data; +using OrderBackend.Domain; + +namespace OrderBackend.Corpus; + +// P7: ordinary LINQ picks the order; the refinement starts after it. +public static class P7LinqBeforeRefinement +{ + public static async Task Run(OrdersDb db, CancellationToken ct) + { + var oldest = await db.Orders + .Where(o => o.Status == OrderStatus.Submitted) + .OrderBy(o => o.Id) + .Select(o => o.Id) + .FirstAsync(ct); + var order = await db.Orders.SingleAsync(o => o.Id == oldest, ct); + var now = DateTime.UnixEpoch; + OrderProtocol.WithSubmitted(order, submitted => + { + submitted.Approve(now); + }); + await db.SaveChangesAsync(ct); + } +} diff --git a/samples/OrderBackend/corpus/positive/P8_full_chain.cs.txt b/samples/OrderBackend/corpus/positive/P8_full_chain.cs.txt new file mode 100644 index 00000000..f43b1157 --- /dev/null +++ b/samples/OrderBackend/corpus/positive/P8_full_chain.cs.txt @@ -0,0 +1,26 @@ +using System; +using System.Linq; +using System.Threading; +using System.Threading.Tasks; +using Microsoft.EntityFrameworkCore; +using OrderBackend.Data; +using OrderBackend.Domain; + +namespace OrderBackend.Corpus; + +// P8: the full chain in one region; every named token is spent. +public static class P8FullChain +{ + public static async Task Run(OrdersDb db, int id, CancellationToken ct) + { + var order = await db.Orders.SingleAsync(o => o.Id == id, ct); + var now = DateTime.UnixEpoch; + OrderProtocol.WithDraft(order, draft => + { + var submitted = draft.Submit(now); + var approved = submitted.Approve(now); + approved.Ship(now, Shipping.TrackingNumber(id)); + }); + await db.SaveChangesAsync(ct); + } +} diff --git a/samples/OrderBackend/corpus/positive/expected.json b/samples/OrderBackend/corpus/positive/expected.json new file mode 100644 index 00000000..db3663a3 --- /dev/null +++ b/samples/OrderBackend/corpus/positive/expected.json @@ -0,0 +1,36 @@ +{ + "P1_create_draft": { + "stage": "core", + "verdict": [] + }, + "P2_draft_submit": { + "stage": "core", + "verdict": [] + }, + "P3_submitted_approve": { + "stage": "core", + "verdict": [] + }, + "P4_approved_ship": { + "stage": "core", + "verdict": [] + }, + "P5_harmless_helper": { + "stage": "core", + "verdict": [], + "proven_call": "OrderBackend.Shipping.TrackingNumber(int)" + }, + "P6_load_refine_transition": { + "stage": "core", + "verdict": [] + }, + "P7_linq_before_refinement": { + "stage": "core", + "verdict": [] + }, + "P8_full_chain": { + "stage": "core", + "verdict": [], + "proven_call": "OrderBackend.Shipping.TrackingNumber(int)" + } +} diff --git a/samples/OrderBackend/evidence/acceptance.txt b/samples/OrderBackend/evidence/acceptance.txt new file mode 100644 index 00000000..b6d5d490 --- /dev/null +++ b/samples/OrderBackend/evidence/acceptance.txt @@ -0,0 +1,45 @@ +ok[db-fresh]: EnsureCreated made the schema in a new database file: 0 rows +ok[http-create]: POST /orders -> 201 /orders/1 {"id":1,"status":"Draft"} +ok[oracle-create]: raw row: 1 | alice | Draft | NULL | NULL | NULL | NULL +ok[http-submit]: POST /orders/1/submit -> 200 {"id":1,"status":"Submitted"} +ok[oracle-submit]: raw row: 1 | alice | Submitted | 2026-01-02 03:04:05 | NULL | NULL | NULL +ok[http-approve]: POST /orders/1/approve -> 200 {"id":1,"status":"Approved"} +ok[oracle-approve]: raw row: 1 | alice | Approved | 2026-01-02 03:04:05 | 2026-01-02 03:04:05 | NULL | NULL +ok[http-ship]: POST /orders/1/ship -> 200 {"id":1,"status":"Shipped","trackingNumber":1007919} +ok[oracle-ship]: raw row: 1 | alice | Shipped | 2026-01-02 03:04:05 | 2026-01-02 03:04:05 | 2026-01-02 03:04:05 | 1007919 +ok[http-get-shipped]: GET /orders/1 -> 200 {"id":1,"customer":"alice","status":"Shipped","submittedAt":"2026-01-02T03:04:05","approvedAt":"2026-01-02T03:04:05","shippedAt":"2026-01-02T03:04:05","trackingNumber":1007919} +ok[http-create-required]: POST /orders {} -> 400 {"error":"customer_required"}, no row written +ok[http-create-required]: POST /orders {"customer":" "} -> 400 {"error":"customer_required"}, no row written +ok[http-create-b]: second order -> /orders/2 +ok[h9-approve-draft]: approve a Draft order -> 409 {"error":"invalid_transition","id":2,"state":"Draft","required":"Submitted"}; row unchanged: True +ok[h9-ship-draft]: ship a Draft order -> 409 {"error":"invalid_transition","id":2,"state":"Draft","required":"Approved"}; row unchanged: True +ok[h9-b-submit]: the legal submit in between goes through: Submitted +ok[h9-ship-submitted]: ship a Submitted order -> 409 {"error":"invalid_transition","id":2,"state":"Submitted","required":"Approved"}; row unchanged: True +ok[h9-submit-submitted]: submit a Submitted order -> 409 {"error":"invalid_transition","id":2,"state":"Submitted","required":"Draft"}; row unchanged: True +ok[h9-b-approve]: the legal approve in between goes through: Approved +ok[h9-submit-approved]: submit an Approved order -> 409 {"error":"invalid_transition","id":2,"state":"Approved","required":"Draft"}; row unchanged: True +ok[h9-approve-approved]: approve an Approved order -> 409 {"error":"invalid_transition","id":2,"state":"Approved","required":"Submitted"}; row unchanged: True +ok[h9-b-ship]: the legal ship in between goes through: Shipped +ok[h9-submit-shipped]: submit a Shipped order -> 409 {"error":"invalid_transition","id":2,"state":"Shipped","required":"Draft"}; row unchanged: True +ok[h9-approve-shipped]: approve a Shipped order -> 409 {"error":"invalid_transition","id":2,"state":"Shipped","required":"Submitted"}; row unchanged: True +ok[h9-ship-shipped]: ship a Shipped order -> 409 {"error":"invalid_transition","id":2,"state":"Shipped","required":"Approved"}; row unchanged: True +ok[http-404-submit]: submit an unknown id -> 404 +ok[http-404-approve]: approve an unknown id -> 404 +ok[http-404-ship]: ship an unknown id -> 404 +ok[http-404-get]: GET an unknown id -> 404 +ok[h8-corrupt-'Bogus']: stored 'Bogus': submit=500 approve=500 ship=500 get=500; EF load: CorruptOrderStateException('Bogus'); row unchanged: True +ok[h8-corrupt-'7']: stored '7': submit=500 approve=500 ship=500 get=500; EF load: CorruptOrderStateException('7'); row unchanged: True +ok[h8-corrupt-'approved']: stored 'approved': submit=500 approve=500 ship=500 get=500; EF load: CorruptOrderStateException('approved'); row unchanged: True +ok[h8-corrupt-'']: stored '': submit=500 approve=500 ship=500 get=500; EF load: CorruptOrderStateException(''); row unchanged: True +ok[h8-storage-strict]: 'Bogus'=refused '7'=refused 'approved'=refused ''=refused ' Draft'=refused ToStore(7)=refused +ok[builder-draft]: Order.Create().Customer("carol").Build() is a new Draft for carol +ok[h10-same-instance-before]: the queried Order IS the instance the ChangeTracker holds, Unchanged +ok[h10-same-instance-after]: after the region the tracked instance is still the queried one, now Submitted; one entry, nothing re-attached +ok[h10-tracked-change]: the ChangeTracker sees Modified: Status,SubmittedAt +ok[h11-saved-exactly]: SaveChangesAsync wrote 1 row; raw columns changed: Status,SubmittedAt; raw row: 7 | carol | Submitted | 2026-01-02 03:04:05 | NULL | NULL | NULL +ok[h12-reload-refine]: reloaded Submitted: WithDraft -> InvalidOrderStateException(Submitted, required Draft) (Unchanged); WithSubmitted -> Approve saved Approved +ok[h13-linq-endpoint]: GET /orders?status=Approved -> 200 [{"id":7,"customer":"carol"}] (the corrupt 'approved' row is not Approved) +ok[h13-linq-unknown-status]: GET /orders?status=approved -> 400 {"error":"unknown_status"} +ok[h13-linq-translated]: the predicate is server-side SQL over the stored name: WHERE "o"."Status" = 'Approved' ... ORDER BY +ok[ef-update-emitted]: the transitions reach the database as ordinary UPDATE statements +typed builder acceptance: all checks hold diff --git a/samples/OrderBackend/evidence/corpus.json b/samples/OrderBackend/evidence/corpus.json new file mode 100644 index 00000000..16a2da4d --- /dev/null +++ b/samples/OrderBackend/evidence/corpus.json @@ -0,0 +1,357 @@ +{ + "sample": { + "regions": { + "OrderBackend.OrderEndpoints.Submit$protocol": [ + "acquire", + "call OrderBackend.Domain.DraftOrder.Submit" + ], + "OrderBackend.OrderEndpoints.Approve$protocol": [ + "acquire", + "call OrderBackend.Domain.SubmittedOrder.Approve" + ], + "OrderBackend.OrderEndpoints.Ship$protocol": [ + "acquire", + "proven_call OrderBackend.Shipping.TrackingNumber(int)", + "call OrderBackend.Domain.ApprovedOrder.Ship" + ] + }, + "heap_effects": [ + "OrderBackend.Shipping.TrackingNumber(int)", + "site:samples/OrderBackend/OrderBackend/OrderEndpoints.cs:97:36" + ], + "verdict": [] + }, + "corpus": [ + { + "kind": "positive", + "case": "P1_create_draft", + "expected": { + "stage": "core", + "verdict": [] + }, + "observed": [] + }, + { + "kind": "positive", + "case": "P2_draft_submit", + "expected": { + "stage": "core", + "verdict": [] + }, + "observed": [] + }, + { + "kind": "positive", + "case": "P3_submitted_approve", + "expected": { + "stage": "core", + "verdict": [] + }, + "observed": [] + }, + { + "kind": "positive", + "case": "P4_approved_ship", + "expected": { + "stage": "core", + "verdict": [] + }, + "observed": [] + }, + { + "kind": "positive", + "case": "P5_harmless_helper", + "expected": { + "stage": "core", + "verdict": [], + "proven_call": "OrderBackend.Shipping.TrackingNumber(int)" + }, + "observed": [] + }, + { + "kind": "positive", + "case": "P6_load_refine_transition", + "expected": { + "stage": "core", + "verdict": [] + }, + "observed": [] + }, + { + "kind": "positive", + "case": "P7_linq_before_refinement", + "expected": { + "stage": "core", + "verdict": [] + }, + "observed": [] + }, + { + "kind": "positive", + "case": "P8_full_chain", + "expected": { + "stage": "core", + "verdict": [], + "proven_call": "OrderBackend.Shipping.TrackingNumber(int)" + }, + "observed": [] + }, + { + "kind": "negative", + "case": "C10a_raw_mutator", + "expected": { + "stage": "extractor", + "text": "'ApplyShip' of 'Order' is not public and belongs to a state protocol" + }, + "observed": "exit 2: extractor: protocol lowering refused: OrderBackend/C10a_raw_mutator.cs:17: 'ApplyShip' of 'Order' is not public and belongs to a state protocol: it is called here, outside the protocol's own types, where it is reachable only through a token (the scan holds the protocol to the boundary a separate assembly would give it)" + }, + { + "kind": "negative", + "case": "C10b_raw_entity_in_region", + "expected": { + "stage": "core", + "verdict": [ + "OWN013" + ] + }, + "observed": [ + "OWN013" + ] + }, + { + "kind": "negative", + "case": "C10c_raw_state_write", + "expected": { + "stage": "compiler", + "code": "CS0272", + "member": "Status" + }, + "observed": [ + "C10c_raw_state_write.cs: CS0272: The property or indexer 'Order.Status' cannot be used in this context because the set accessor is inaccessible" + ] + }, + { + "kind": "negative", + "case": "C11a_token_copy", + "expected": { + "stage": "core", + "verdict": [ + "OWN005" + ] + }, + "observed": [ + "OWN005" + ] + }, + { + "kind": "negative", + "case": "C11b_entity_alias", + "expected": { + "stage": "core", + "verdict": [ + "OWN013" + ] + }, + "observed": [ + "OWN013" + ] + }, + { + "kind": "negative", + "case": "C12a_harmful_helper", + "expected": { + "stage": "core", + "refusal": "'OrderBackend.Corpus.C12aHarmfulHelper.Counter.Next()': writes.static is may" + }, + "observed": "refused: OwnIR 'proven_call' to 'OrderBackend.Corpus.C12aHarmfulHelper.Counter.Next()' is not proven harmless: 'OrderBackend.Corpus.C12aHarmfulHelper.Counter.Next()': writes.static is may (OrderBackend/C12a_harmful_helper.cs:20) — refused: an exclusive region admits only calls the effect summaries prove harmless" + }, + { + "kind": "negative", + "case": "C12b_logger_in_region", + "expected": { + "stage": "extractor", + "text": "LoggerExtensions.LogInformation' inside a protocol region runs code with no stated contract" + }, + "observed": "exit 2: extractor: protocol lowering refused: OrderBackend/C12b_logger_in_region.cs:20: a call to 'Microsoft.Extensions.Logging.LoggerExtensions.LogInformation' inside a protocol region runs code with no stated contract; an exclusive region admits only transitions and what the lowering can read" + }, + { + "kind": "negative", + "case": "C13_builder_without_customer", + "expected": { + "stage": "compiler", + "code": "CS1061", + "member": "Build" + }, + "observed": [ + "C13_builder_without_customer.cs: CS1061: 'Order.DraftBuilder.CustomerStep' does not contain a definition for 'Build' and no accessible extension method 'Build' accepting a first argument of type 'Order.DraftBuilder.CustomerStep' could be found (are you missing a using directive or an assembly reference?)" + ] + }, + { + "kind": "negative", + "case": "C14_forged_token", + "expected": { + "stage": "extractor", + "text": "a protocol token 'ApprovedOrder' is created outside the protocol's own types" + }, + "observed": "exit 2: extractor: protocol lowering refused: OrderBackend/C14_forged_token.cs:17: a protocol token 'ApprovedOrder' is created outside the protocol's own types: a token comes only from a region entry or a transition (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)" + }, + { + "kind": "negative", + "case": "C15_entity_constructor", + "expected": { + "stage": "compiler", + "code": "CS0122", + "member": "Order" + }, + "observed": [ + "C15_entity_constructor.cs: CS0122: 'Order.Order()' is inaccessible due to its protection level" + ] + }, + { + "kind": "negative", + "case": "C1_draft_approve", + "expected": { + "stage": "compiler", + "code": "CS1061", + "member": "Approve" + }, + "observed": [ + "C1_draft_approve.cs: CS1061: 'DraftOrder' does not contain a definition for 'Approve' and no accessible extension method 'Approve' accepting a first argument of type 'DraftOrder' could be found (are you missing a using directive or an assembly reference?)" + ] + }, + { + "kind": "negative", + "case": "C2_draft_ship", + "expected": { + "stage": "compiler", + "code": "CS1061", + "member": "Ship" + }, + "observed": [ + "C2_draft_ship.cs: CS1061: 'DraftOrder' does not contain a definition for 'Ship' and no accessible extension method 'Ship' accepting a first argument of type 'DraftOrder' could be found (are you missing a using directive or an assembly reference?)" + ] + }, + { + "kind": "negative", + "case": "C3_submitted_submit", + "expected": { + "stage": "compiler", + "code": "CS1061", + "member": "Submit" + }, + "observed": [ + "C3_submitted_submit.cs: CS1061: 'SubmittedOrder' does not contain a definition for 'Submit' and no accessible extension method 'Submit' accepting a first argument of type 'SubmittedOrder' could be found (are you missing a using directive or an assembly reference?)" + ] + }, + { + "kind": "negative", + "case": "C4_submitted_ship", + "expected": { + "stage": "compiler", + "code": "CS1061", + "member": "Ship" + }, + "observed": [ + "C4_submitted_ship.cs: CS1061: 'SubmittedOrder' does not contain a definition for 'Ship' and no accessible extension method 'Ship' accepting a first argument of type 'SubmittedOrder' could be found (are you missing a using directive or an assembly reference?)" + ] + }, + { + "kind": "negative", + "case": "C5_approved_submit", + "expected": { + "stage": "compiler", + "code": "CS1061", + "member": "Submit" + }, + "observed": [ + "C5_approved_submit.cs: CS1061: 'ApprovedOrder' does not contain a definition for 'Submit' and no accessible extension method 'Submit' accepting a first argument of type 'ApprovedOrder' could be found (are you missing a using directive or an assembly reference?)" + ] + }, + { + "kind": "negative", + "case": "C6_approved_approve", + "expected": { + "stage": "compiler", + "code": "CS1061", + "member": "Approve" + }, + "observed": [ + "C6_approved_approve.cs: CS1061: 'ApprovedOrder' does not contain a definition for 'Approve' and no accessible extension method 'Approve' accepting a first argument of type 'ApprovedOrder' could be found (are you missing a using directive or an assembly reference?)" + ] + }, + { + "kind": "negative", + "case": "C7_shipped_transition", + "expected": { + "stage": "compiler", + "code": "CS1061", + "member": "Submit" + }, + "observed": [ + "C7_shipped_transition.cs: CS1061: 'ShippedOrder' does not contain a definition for 'Submit' and no accessible extension method 'Submit' accepting a first argument of type 'ShippedOrder' could be found (are you missing a using directive or an assembly reference?)" + ] + }, + { + "kind": "negative", + "case": "C7b_shipped_region", + "expected": { + "stage": "compiler", + "code": "CS0117", + "member": "WithShipped" + }, + "observed": [ + "C7b_shipped_region.cs: CS0117: 'OrderProtocol' does not contain a definition for 'WithShipped'" + ] + }, + { + "kind": "negative", + "case": "C8_stale_draft", + "expected": { + "stage": "core", + "verdict": [ + "OWN002" + ] + }, + "observed": [ + "OWN002" + ] + }, + { + "kind": "negative", + "case": "C9_stale_submitted", + "expected": { + "stage": "core", + "verdict": [ + "OWN002" + ] + }, + "observed": [ + "OWN002" + ] + }, + { + "kind": "limits", + "case": "K1_named_terminal_token", + "expected": { + "stage": "core", + "verdict": [ + "OWN001" + ], + "why": "tokens are linear, not affine (P-010; case G6): a named token must be spent, and a terminal one cannot be" + }, + "observed": [ + "OWN001" + ] + }, + { + "kind": "limits", + "case": "K2_execute_update", + "expected": { + "stage": "core", + "verdict": [], + "why": "a bulk write has no entity instance for a token to guard: concurrency tokens, constraints and transactions own it" + }, + "observed": [] + } + ] +} diff --git a/samples/OrderBackend/evidence/orderbackend.facts.json b/samples/OrderBackend/evidence/orderbackend.facts.json new file mode 100644 index 00000000..fb54d597 --- /dev/null +++ b/samples/OrderBackend/evidence/orderbackend.facts.json @@ -0,0 +1,603 @@ +{ + "ownir_version": 2, + "module": "Extracted", + "components": [], + "services": [], + "functions": [ + { + "name": "OrderBackend.OrderEndpoints.Create", + "file": "samples/OrderBackend/OrderBackend/OrderEndpoints.cs", + "sig": "OrderBackend.CreateOrderRequest,OrderBackend.Data.OrdersDb,System.Threading.CancellationToken", + "params": [ + { + "name": "db", + "line": 19 + } + ], + "body": [ + { + "op": "if", + "line": 21, + "then": [ + { + "op": "return", + "var": null, + "line": 22 + } + ], + "else": [] + }, + { + "op": "use", + "var": "db", + "line": 27 + }, + { + "op": "use", + "var": "db", + "line": 28 + }, + { + "op": "return", + "var": null, + "line": 29 + } + ] + }, + { + "name": "OrderBackend.OrderEndpoints.Submit", + "file": "samples/OrderBackend/OrderBackend/OrderEndpoints.cs", + "sig": "System.Int32,OrderBackend.Data.OrdersDb,System.TimeProvider,System.Threading.CancellationToken", + "params": [ + { + "name": "db", + "line": 32 + } + ], + "body": [ + { + "op": "if", + "line": 36, + "then": [ + { + "op": "return", + "var": null, + "line": 34 + } + ], + "else": [] + }, + { + "op": "if", + "line": 37, + "then": [ + { + "op": "return", + "var": null, + "line": 34 + } + ], + "else": [] + }, + { + "op": "if", + "line": 40, + "then": [ + { + "op": "return", + "var": null, + "line": 34 + } + ], + "else": [] + }, + { + "op": "if", + "line": 41, + "then": [ + { + "op": "return", + "var": null, + "line": 34 + } + ], + "else": [] + }, + { + "op": "if", + "line": 46, + "then": [ + { + "op": "return", + "var": null, + "line": 34 + } + ], + "else": [] + }, + { + "op": "use", + "var": "db", + "line": 46 + }, + { + "op": "return", + "var": null, + "line": 34 + } + ] + }, + { + "name": "OrderBackend.OrderEndpoints.Approve", + "file": "samples/OrderBackend/OrderBackend/OrderEndpoints.cs", + "sig": "System.Int32,OrderBackend.Data.OrdersDb,System.TimeProvider,System.Threading.CancellationToken", + "params": [ + { + "name": "db", + "line": 59 + } + ], + "body": [ + { + "op": "if", + "line": 63, + "then": [ + { + "op": "return", + "var": null, + "line": 61 + } + ], + "else": [] + }, + { + "op": "if", + "line": 64, + "then": [ + { + "op": "return", + "var": null, + "line": 61 + } + ], + "else": [] + }, + { + "op": "if", + "line": 67, + "then": [ + { + "op": "return", + "var": null, + "line": 61 + } + ], + "else": [] + }, + { + "op": "if", + "line": 68, + "then": [ + { + "op": "return", + "var": null, + "line": 61 + } + ], + "else": [] + }, + { + "op": "if", + "line": 73, + "then": [ + { + "op": "return", + "var": null, + "line": 61 + } + ], + "else": [] + }, + { + "op": "use", + "var": "db", + "line": 73 + }, + { + "op": "return", + "var": null, + "line": 61 + } + ] + }, + { + "name": "OrderBackend.OrderEndpoints.Ship", + "file": "samples/OrderBackend/OrderBackend/OrderEndpoints.cs", + "sig": "System.Int32,OrderBackend.Data.OrdersDb,System.TimeProvider,System.Threading.CancellationToken", + "params": [ + { + "name": "db", + "line": 86 + } + ], + "body": [ + { + "op": "if", + "line": 90, + "then": [ + { + "op": "return", + "var": null, + "line": 88 + } + ], + "else": [] + }, + { + "op": "if", + "line": 91, + "then": [ + { + "op": "return", + "var": null, + "line": 88 + } + ], + "else": [] + }, + { + "op": "if", + "line": 94, + "then": [ + { + "op": "return", + "var": null, + "line": 88 + } + ], + "else": [] + }, + { + "op": "if", + "line": 95, + "then": [ + { + "op": "return", + "var": null, + "line": 88 + } + ], + "else": [] + }, + { + "op": "if", + "line": 100, + "then": [ + { + "op": "return", + "var": null, + "line": 88 + } + ], + "else": [] + }, + { + "op": "use", + "var": "db", + "line": 100 + }, + { + "op": "return", + "var": null, + "line": 88 + } + ] + }, + { + "name": "OrderBackend.OrderEndpoints.Get", + "file": "samples/OrderBackend/OrderBackend/OrderEndpoints.cs", + "sig": "System.Int32,OrderBackend.Data.OrdersDb,System.Threading.CancellationToken", + "params": [ + { + "name": "db", + "line": 113 + } + ], + "body": [ + { + "op": "if", + "line": 117, + "then": [ + { + "op": "return", + "var": null, + "line": 115 + } + ], + "else": [] + }, + { + "op": "return", + "var": null, + "line": 115 + } + ] + }, + { + "name": "OrderBackend.OrderEndpoints.List", + "file": "samples/OrderBackend/OrderBackend/OrderEndpoints.cs", + "sig": "System.String,OrderBackend.Data.OrdersDb,System.Threading.CancellationToken", + "params": [ + { + "name": "db", + "line": 138 + } + ], + "body": [ + { + "op": "if", + "line": 140, + "then": [ + { + "op": "return", + "var": null, + "line": 141 + } + ], + "else": [] + }, + { + "op": "return", + "var": null, + "line": 148 + } + ] + }, + { + "name": "OrderBackend.OrderEndpoints.Submit$protocol", + "file": "samples/OrderBackend/OrderBackend/OrderEndpoints.cs", + "body": [ + { + "op": "acquire", + "var": "order", + "line": 41 + }, + { + "op": "borrow_mut", + "owner": "order", + "binding": "order.region1", + "line": 41, + "body": [ + { + "op": "acquire", + "var": "draft", + "line": 41 + }, + { + "op": "call", + "callee": "OrderBackend.Domain.DraftOrder.Submit", + "args": [ + "draft", + "order.region1" + ], + "line": 43 + } + ] + }, + { + "op": "release", + "var": "order", + "line": 41 + } + ] + }, + { + "name": "OrderBackend.OrderEndpoints.Approve$protocol", + "file": "samples/OrderBackend/OrderBackend/OrderEndpoints.cs", + "body": [ + { + "op": "acquire", + "var": "order", + "line": 68 + }, + { + "op": "borrow_mut", + "owner": "order", + "binding": "order.region1", + "line": 68, + "body": [ + { + "op": "acquire", + "var": "submitted", + "line": 68 + }, + { + "op": "call", + "callee": "OrderBackend.Domain.SubmittedOrder.Approve", + "args": [ + "submitted", + "order.region1" + ], + "line": 70 + } + ] + }, + { + "op": "release", + "var": "order", + "line": 68 + } + ] + }, + { + "name": "OrderBackend.OrderEndpoints.Ship$protocol", + "file": "samples/OrderBackend/OrderBackend/OrderEndpoints.cs", + "body": [ + { + "op": "acquire", + "var": "order", + "line": 95 + }, + { + "op": "borrow_mut", + "owner": "order", + "binding": "order.region1", + "line": 95, + "body": [ + { + "op": "acquire", + "var": "approved", + "line": 95 + }, + { + "op": "proven_call", + "site": "site:samples/OrderBackend/OrderBackend/OrderEndpoints.cs:97:36", + "callee": "OrderBackend.Shipping.TrackingNumber(int)", + "line": 97 + }, + { + "op": "call", + "callee": "OrderBackend.Domain.ApprovedOrder.Ship", + "args": [ + "approved", + "order.region1" + ], + "line": 97 + } + ] + }, + { + "op": "release", + "var": "order", + "line": 95 + } + ] + }, + { + "name": "OrderBackend.Domain.ApprovedOrder.Ship", + "file": "samples/OrderBackend/OrderBackend/Domain/Order.Protocol.cs", + "params": [ + { + "name": "token", + "effect": "consume", + "line": 167 + }, + { + "name": "entity", + "effect": "borrow_mut", + "line": 167 + } + ], + "body": [ + { + "op": "release", + "var": "token", + "line": 167 + } + ] + }, + { + "name": "OrderBackend.Domain.DraftOrder.Submit", + "file": "samples/OrderBackend/OrderBackend/Domain/Order.Protocol.cs", + "params": [ + { + "name": "token", + "effect": "consume", + "line": 133 + }, + { + "name": "entity", + "effect": "borrow_mut", + "line": 133 + } + ], + "body": [ + { + "op": "release", + "var": "token", + "line": 133 + } + ] + }, + { + "name": "OrderBackend.Domain.SubmittedOrder.Approve", + "file": "samples/OrderBackend/OrderBackend/Domain/Order.Protocol.cs", + "params": [ + { + "name": "token", + "effect": "consume", + "line": 150 + }, + { + "name": "entity", + "effect": "borrow_mut", + "line": 150 + } + ], + "body": [ + { + "op": "release", + "var": "token", + "line": 150 + } + ] + } + ], + "stats": { + "methods_with_local": 6, + "methods_flow_analysed": 6, + "methods_skipped_unmodelled": 0 + }, + "heap_effects": { + "heap_effects_version": 1, + "methods": [ + { + "key": "OrderBackend.Shipping.TrackingNumber(int)", + "file": "samples/OrderBackend/OrderBackend/Shipping.cs", + "line": 9, + "receiver": false, + "return_inert": true, + "params": [ + { + "index": 0, + "name": "orderId", + "inert": true + } + ], + "locals": [], + "derefs": [], + "writes": [], + "stores": [], + "returns": [], + "calls": [], + "unknown": [] + }, + { + "key": "site:samples/OrderBackend/OrderBackend/OrderEndpoints.cs:97:36", + "file": "samples/OrderBackend/OrderBackend/OrderEndpoints.cs", + "line": 97, + "receiver": false, + "return_inert": true, + "params": [], + "locals": [], + "derefs": [], + "writes": [], + "stores": [], + "returns": [], + "calls": [ + { + "id": 0, + "callee": "OrderBackend.Shipping.TrackingNumber(int)", + "dispatch": "direct", + "receiver": null, + "args": [ + [] + ], + "line": 97 + } + ], + "unknown": [] + } + ] + } +} diff --git a/samples/OrderBackend/nuget.config b/samples/OrderBackend/nuget.config new file mode 100644 index 00000000..88397e92 --- /dev/null +++ b/samples/OrderBackend/nuget.config @@ -0,0 +1,8 @@ + + + + + + + + diff --git a/scripts/typed_builder_gate.py b/scripts/typed_builder_gate.py new file mode 100644 index 00000000..f909fe26 --- /dev/null +++ b/scripts/typed_builder_gate.py @@ -0,0 +1,419 @@ +#!/usr/bin/env python3 +"""TB-MVP-01: the Typed Builder + ASP.NET Core + EF Core Order vertical slice, end to end. + +The sample is `samples/OrderBackend`; what it must show, and why, is registered in +`docs/notes/tb-mvp-01-preregistration.md`. Needs `dotnet` on PATH; zero Python dependencies. +Steps, in the registered order: + +1. **generator** — `frontend/roslyn/Own.TypedBuilder` generates `Domain/Order.Protocol.cs` from + `Domain/Order.cs` twice, into two clean directories: both outputs must be the same bytes, and + the committed file must be those bytes. Every token the generated surface constructs wraps + the region entry's own argument or the token's own field: no copy, no second entity. +2. **build** — the backend and its acceptance runner build. +3. **sample** — the real extractor over the backend's project file: a region in each of the + Submit, Approve and Ship handlers, the Ship helper as an OwnIR `proven_call`, and a clean + verdict (on both public CLIs with `--rust`). The facts are pinned in `evidence/`. +4. **corpus** — every `corpus//.cs.txt` is staged ALONE into a copy of the project + and must meet its `expected.json` row: a C# compiler error (`compiler`), an extractor + refusal (`extractor`), or a core verdict (`core`: codes, or a refusal text). +5. **acceptance** — the runner drives real HTTP against a real SQLite file with oracles that do + not go through the typed API, twice: both transcripts must be the same bytes. + +Run: python scripts/typed_builder_gate.py (verify) + python scripts/typed_builder_gate.py --write (rewrite evidence/) + python scripts/typed_builder_gate.py --rust (also compare the two CLIs) + python scripts/typed_builder_gate.py --clean-checkout [--runs N] [--rust ] + (the gate, N times (default 2), each in a fresh `git worktree` of HEAD with no + build output; the evidence of every run must be the same bytes) +""" + +from __future__ import annotations + +import hashlib +import json +import os +import re +import shutil +import subprocess +import sys +import tempfile + +ROOT = os.path.normpath(os.path.join(os.path.dirname(os.path.abspath(__file__)), "..")) +sys.path.insert(0, ROOT) + +from ownlang.ownir import OwnIRError, check_facts # noqa: E402 + +SAMPLE_REL = "samples/OrderBackend" +SAMPLE = os.path.join(ROOT, *SAMPLE_REL.split("/")) +BACKEND = os.path.join(SAMPLE, "OrderBackend") +PROJECT_REL = f"{SAMPLE_REL}/OrderBackend/OrderBackend.csproj" +DECLARATION = os.path.join(BACKEND, "Domain", "Order.cs") +GENERATED = os.path.join(BACKEND, "Domain", "Order.Protocol.cs") +EVIDENCE = os.path.join(SAMPLE, "evidence") +GENERATOR = os.path.join(ROOT, "frontend", "roslyn", "Own.TypedBuilder") +EXTRACTOR = os.path.join(ROOT, "frontend", "roslyn", "OwnSharp.Extractor") + +HANDLER_REGIONS = ("OrderBackend.OrderEndpoints.Submit$protocol", + "OrderBackend.OrderEndpoints.Approve$protocol", + "OrderBackend.OrderEndpoints.Ship$protocol") +HELPER = "OrderBackend.Shipping.TrackingNumber(int)" +ACCEPTANCE_CHECKS = 44 +KINDS = ("positive", "negative", "limits") + + +def _run(cmd: list[str], cwd: str = ROOT) -> subprocess.CompletedProcess[str]: + return subprocess.run(cmd, cwd=cwd, capture_output=True, text=True, encoding="utf-8", + errors="replace", check=False) + + +def _build(path: str, *extra: str, cwd: str = ROOT) -> subprocess.CompletedProcess[str]: + return _run(["dotnet", "build", path, "-nologo", "-v", "q", *extra], cwd=cwd) + + +def _tool(project: str, dll: str, fails: list[str]) -> str | None: + built = _build(project, "-c", "Release") + if built.returncode != 0: + fails.append(f"{os.path.basename(project)} does not build: {built.stdout.strip()[-600:]}") + return None + return os.path.join(project, "bin", "Release", "net8.0", dll) + + +def _verdict(facts: dict[str, object]) -> list[str] | str: + try: + return sorted({f.code for f in check_facts(facts)}) + except OwnIRError as e: + return f"refused: {e}" + + +def _cli_parity(rust: str, facts_path: str, cwd: str, where: str, fails: list[str]) -> None: + args = ["ownir", facts_path, "--format", "human", "--severity", "error"] + py = subprocess.run([sys.executable, "-m", "ownlang", *args], cwd=cwd, capture_output=True, + check=False, env={**os.environ, "PYTHONPATH": ROOT}) + rs = subprocess.run([rust, *args], cwd=cwd, capture_output=True, check=False) + if (py.returncode, py.stdout, py.stderr) != (rs.returncode, rs.stdout, rs.stderr): + fails.append(f"{where}: the two public CLIs differ (python rc={py.returncode}, " + f"rust rc={rs.returncode})") + + +# ---- 1. generator --------------------------------------------------------------------------- + +_NEW_TOKEN = re.compile(r"new (Draft|Submitted|Approved|Shipped)Order\((\w+)\)") + + +def generator(fails: list[str]) -> int: + dll = _tool(GENERATOR, "own-typed-builder.dll", fails) + if dll is None: + return 0 + outputs = [] + for _ in range(2): + with tempfile.TemporaryDirectory() as tmp: + out = os.path.join(tmp, "Order.Protocol.cs") + done = _run(["dotnet", dll, DECLARATION, "-o", out]) + if done.returncode != 0: + fails.append(f"generator: exit {done.returncode}: {done.stderr.strip()}") + return 0 + with open(out, "rb") as f: + outputs.append(f.read()) + if outputs[0] != outputs[1]: + fails.append("generator/determinism: two clean generations differ") + with open(GENERATED, "rb") as f: + committed = f.read() + if committed != outputs[0]: + fails.append("generator/committed: Order.Protocol.cs is not what the generator writes from " + "Order.cs; regenerate it") + text = outputs[0].decode("utf-8") + if b"\r" in outputs[0] or outputs[0].startswith(b"\xef\xbb\xbf"): + fails.append("generator/bytes: the output carries a CR or a BOM") + # identity, structurally: a token wraps `order` (the region entry's argument) or `_order` + # (the token's own field) and nothing else; no entity is created but the builder's one + wrapped = _NEW_TOKEN.findall(text) + if len(wrapped) != 6 or any(arg not in ("order", "_order") for _, arg in wrapped): + fails.append(f"generator/identity: tokens are constructed over {wrapped}") + if text.count("new()") != 2 or re.search(r"new Order\s*[({]", text): + fails.append("generator/identity: the generated surface creates an Order outside Build()") + return 2 + + +# ---- 3. the real sample --------------------------------------------------------------------- + +def sample(dll: str, rust: str | None, write: bool, fails: list[str]) -> dict[str, object]: + with tempfile.TemporaryDirectory() as tmp: + out = os.path.join(tmp, "facts.json") + done = _run(["dotnet", dll, PROJECT_REL, "--flow-locals", "-o", out]) + if done.returncode != 0: + fails.append(f"sample: the extractor exited {done.returncode}: " + f"{done.stderr.strip()[-400:]}") + return {} + with open(out, encoding="utf-8") as f: + facts = json.load(f) + if rust is not None: + _cli_parity(rust, out, ROOT, "sample", fails) + by_name = {fn["name"]: fn for fn in facts.get("functions", [])} + regions = {} + for name in HANDLER_REGIONS: + body = by_name.get(name, {}).get("body", []) + inner = [op for region in body if region.get("op") == "borrow_mut" for op in region["body"]] + regions[name] = [op["op"] + (f" {op['callee']}" if "callee" in op else "") for op in inner] + if not inner: + fails.append(f"sample: no protocol region lowered for {name}") + ship = regions.get("OrderBackend.OrderEndpoints.Ship$protocol", []) + if f"proven_call {HELPER}" not in ship: + fails.append(f"sample: the Ship region has no proven_call to {HELPER}: {ship}") + keys = sorted(m["key"] for m in facts.get("heap_effects", {}).get("methods", [])) + if HELPER not in keys: + fails.append(f"sample: heap_effects has no record of {HELPER}: {keys}") + verdict = _verdict(facts) + if verdict != []: + fails.append(f"sample: verdict {verdict!r}, expected clean") + _evidence("orderbackend.facts.json", json.dumps(facts, indent=2, ensure_ascii=False) + "\n", + write, fails, as_json=True) + return {"regions": regions, "heap_effects": keys, "verdict": verdict} + + +# ---- 4. corpus ------------------------------------------------------------------------------ + +def _stage(tmp: str) -> str: + """A buildable copy of the sample's sources under `/stage/`.""" + stage = os.path.join(tmp, "stage") + shutil.copytree(BACKEND, os.path.join(stage, "OrderBackend"), + ignore=shutil.ignore_patterns("bin", "obj")) + shutil.copyfile(os.path.join(SAMPLE, "nuget.config"), os.path.join(stage, "nuget.config")) + return stage + + +_CS_ERROR = re.compile(r"^(?P[^\n(]+)\(\d+,\d+\): error (?PCS\d+): (?P.*?) \[", + re.M) + + +def corpus(dll: str, rust: str | None, fails: list[str]) -> list[dict[str, object]]: + cases: list[tuple[str, str, dict[str, object]]] = [] + for kind in KINDS: + folder = os.path.join(SAMPLE, "corpus", kind) + with open(os.path.join(folder, "expected.json"), encoding="utf-8") as f: + expected = json.load(f) + on_disk = sorted(n[:-7] for n in os.listdir(folder) if n.endswith(".cs.txt")) + if on_disk != sorted(expected): + fails.append(f"corpus/{kind}: expected.json {sorted(expected)} != sources {on_disk}") + return [] + cases += [(kind, case, expected[case]) for case in on_disk] + + observed: list[dict[str, object]] = [] + with tempfile.TemporaryDirectory() as tmp: + stage = _stage(tmp) + project = "OrderBackend/OrderBackend.csproj" + base = _build(project, cwd=stage) + if base.returncode != 0: + fails.append(f"corpus: the staged backend does not build: {base.stdout.strip()[-400:]}") + return [] + for kind, case, want in cases: + where = f"corpus/{kind}/{case}" + staged = os.path.join(stage, "OrderBackend", f"{case}.cs") + shutil.copyfile(os.path.join(SAMPLE, "corpus", kind, f"{case}.cs.txt"), staged) + try: + got = _one(stage, project, case, want, dll, rust, where, fails) + finally: + os.remove(staged) + observed.append({"kind": kind, "case": case, "expected": want, "observed": got}) + # the staged project, back to its own sources, is still the clean sample + rebuilt = _build(project, cwd=stage) + if rebuilt.returncode != 0: + fails.append("corpus: the staged backend does not rebuild without the staged cases") + return observed + + +def _one(stage: str, project: str, case: str, want: dict[str, object], dll: str, + rust: str | None, where: str, fails: list[str]) -> object: + built = _build(project, cwd=stage) + if want["stage"] == "compiler": + errors = sorted({(os.path.basename(m["file"]), m["code"], m["msg"]) + for m in _CS_ERROR.finditer(built.stdout)}) + got = [f"{f}: {code}: {msg}" for f, code, msg in errors] + if built.returncode == 0: + fails.append(f"{where}: the C# compiler accepts it") + elif not errors or any(f != f"{case}.cs" or code != want["code"] for f, code, _ in errors): + fails.append(f"{where}: expected only {want['code']} in {case}.cs, got {got}") + elif not all(re.search(rf"'[^']*\b{re.escape(str(want['member']))}\b[^']*'", msg) + for _, _, msg in errors): + fails.append(f"{where}: the {want['code']} errors do not name " + f"'{want['member']}': {got}") + return got + if built.returncode != 0: + codes = sorted(set(re.findall(r"error (CS\d+)", built.stdout))) + fails.append(f"{where}: the staged backend does not build: {codes}") + return f"does not build: {codes}" + out = os.path.join(stage, "facts.json") + if os.path.exists(out): + os.remove(out) + done = _run(["dotnet", dll, project, "--flow-locals", "-o", "facts.json"], cwd=stage) + if want["stage"] == "extractor": + line = next((x for x in done.stderr.splitlines() if "refused" in x), done.stderr.strip()) + if done.returncode != 2: + fails.append(f"{where}: the extractor exited {done.returncode}, expected a refusal (2)") + elif os.path.exists(out): + fails.append(f"{where}: a facts file was written despite the refusal") + elif str(want["text"]) not in done.stderr or f"{case}.cs" not in done.stderr: + fails.append(f"{where}: refusal text lacks {want['text']!r}: " + f"{done.stderr.strip()[-300:]}") + return f"exit {done.returncode}: {line}" + # core + if done.returncode != 0: + fails.append(f"{where}: the extractor exited {done.returncode}: " + f"{done.stderr.strip()[-300:]}") + return f"extractor exit {done.returncode}" + with open(out, encoding="utf-8") as f: + facts = json.load(f) + verdict = _verdict(facts) + if "verdict" in want and verdict != want["verdict"]: + fails.append(f"{where}: verdict {verdict!r}, expected {want['verdict']!r}") + if "refusal" in want and not (isinstance(verdict, str) and str(want["refusal"]) in verdict): + fails.append(f"{where}: expected a core refusal with {want['refusal']!r}, got {verdict!r}") + if "proven_call" in want: + calls = re.findall(r'"op": "proven_call",[^}]*"callee": "([^"]+)"', json.dumps(facts)) + if want["proven_call"] not in calls: + fails.append(f"{where}: no proven_call to {want['proven_call']} in the facts: {calls}") + if rust is not None: + _cli_parity(rust, "facts.json", stage, where, fails) + return verdict + + +# ---- 5. acceptance -------------------------------------------------------------------------- + +def acceptance(fails: list[str]) -> str: + runner = os.path.join(SAMPLE, "Acceptance") + built = _build(runner) + if built.returncode != 0: + fails.append(f"acceptance: does not build: {built.stdout.strip()[-400:]}") + return "" + dll = os.path.join(runner, "bin", "Debug", "net8.0", "Acceptance.dll") + transcripts = [] + for n in (1, 2): + ran = _run(["dotnet", dll], cwd=SAMPLE) + oks = len(re.findall(r"^ok\[", ran.stdout, flags=re.M)) + if (ran.returncode != 0 or "all checks hold" not in ran.stdout or oks != ACCEPTANCE_CHECKS + or "FAIL[" in ran.stdout or ran.stderr.strip()): + fails.append(f"acceptance/run{n}: exit {ran.returncode}, " + f"{oks}/{ACCEPTANCE_CHECKS} checks: " + f"{(ran.stdout + ran.stderr).strip()[-600:]}") + transcripts.append(ran.stdout) + if transcripts[0] != transcripts[1]: + fails.append("acceptance/determinism: the two transcripts differ") + return transcripts[0] + + +# ---- evidence ------------------------------------------------------------------------------- + +def _evidence(name: str, text: str, write: bool, fails: list[str], as_json: bool = False) -> None: + path = os.path.join(EVIDENCE, name) + out_dir = os.environ.get("TB_GATE_EVIDENCE_OUT") + if out_dir: + with open(os.path.join(out_dir, name), "w", encoding="utf-8", newline="\n") as f: + f.write(text) + if write: + os.makedirs(EVIDENCE, exist_ok=True) + with open(path, "w", encoding="utf-8", newline="\n") as f: + f.write(text) + return + if not os.path.exists(path): + fails.append(f"evidence/{name}: missing; run with --write") + return + with open(path, encoding="utf-8") as f: + committed = f.read() + same = json.loads(committed) == json.loads(text) if as_json else committed == text + if not same: + fails.append(f"evidence/{name}: the gate no longer produces the committed evidence") + + +def gate(rust: str | None, write: bool) -> int: + fails: list[str] = [] + n_gen = generator(fails) + built = _build(os.path.join(BACKEND, "OrderBackend.csproj")) + if built.returncode != 0: + fails.append(f"build: the backend does not build: {built.stdout.strip()[-400:]}") + dll = _tool(EXTRACTOR, "ownsharp-extract.dll", fails) + summary: dict[str, object] = {} + observed: list[dict[str, object]] = [] + transcript = "" + if dll is not None and built.returncode == 0: + summary = sample(dll, rust, write, fails) + observed = corpus(dll, rust, fails) + transcript = acceptance(fails) + _evidence("corpus.json", json.dumps({"sample": summary, "corpus": observed}, indent=2, + ensure_ascii=False) + "\n", write, fails) + _evidence("acceptance.txt", transcript, write, fails) + counts: dict[str, int] = {} + for row in observed: + counts[str(row["kind"])] = counts.get(str(row["kind"]), 0) + 1 + oks = len(re.findall(r"^ok\[", transcript, flags=re.M)) + for f in fails: + print(f"FAIL: {f}") + print(f"typed builder gate: generator {n_gen} clean generations, " + f"{counts.get('positive', 0)} positive / {counts.get('negative', 0)} negative / " + f"{counts.get('limits', 0)} limit cases, {oks} acceptance checks x2" + + (", both CLIs compared" if rust else "") + + f"; transcript sha256 {hashlib.sha256(transcript.encode()).hexdigest()[:16]}" + + f"; {len(fails)} failure(s)" + (" [evidence written]" if write else "")) + return 1 if fails else 0 + + +def clean_checkout(runs: int, rust: str | None) -> int: + """The gate in `runs` fresh worktrees of HEAD; their evidence must be the same bytes.""" + head = _run(["git", "rev-parse", "HEAD"]).stdout.strip() + digests: list[dict[str, str]] = [] + rc = 0 + for n in range(1, runs + 1): + with tempfile.TemporaryDirectory() as tmp: + tree = os.path.join(tmp, "tree") + evidence = os.path.join(tmp, "evidence") + os.makedirs(evidence) + added = _run(["git", "worktree", "add", "--detach", tree, head]) + if added.returncode != 0: + print(f"FAIL: clean-checkout/run{n}: git worktree add: {added.stderr.strip()}") + return 1 + try: + leftovers = [d for _, dirs, _ in os.walk(tree) for d in dirs + if d in ("bin", "obj")] + if leftovers: + print(f"FAIL: clean-checkout/run{n}: the worktree has build output: " + f"{leftovers}") + rc = 1 + cmd = [sys.executable, os.path.join(tree, "scripts", "typed_builder_gate.py")] + if rust: + cmd += ["--rust", rust] + done = subprocess.run(cmd, cwd=tree, check=False, capture_output=True, text=True, + env={**os.environ, "TB_GATE_EVIDENCE_OUT": evidence}) + last = done.stdout.strip().splitlines()[-1] if done.stdout.strip() else "no output" + print(f"clean-checkout/run{n} @ {head[:12]}: {last}") + if done.returncode != 0: + print(done.stdout + done.stderr) + rc = 1 + run: dict[str, str] = {} + for name in sorted(os.listdir(evidence)): + with open(os.path.join(evidence, name), "rb") as f: + run[name] = hashlib.sha256(f.read()).hexdigest() + digests.append(run) + finally: + _run(["git", "worktree", "remove", "--force", tree]) + for name in sorted(digests[0]) if digests else []: + line = " ".join(d.get(name, "")[:16] for d in digests) + same = len({d.get(name) for d in digests}) == 1 + print(f"clean-checkout/digest {name}: {line} {'identical' if same else 'DIFFER'}") + if not same: + rc = 1 + print(f"typed builder clean-checkout: {runs} run(s) from fresh worktrees of {head[:12]}; " + + ("PASS" if rc == 0 else "FAIL")) + return rc + + +def main() -> int: + argv = sys.argv[1:] + rust = argv[argv.index("--rust") + 1] if "--rust" in argv else None + if rust is not None: + rust = os.path.abspath(rust) + if "--clean-checkout" in argv: + runs = int(argv[argv.index("--runs") + 1]) if "--runs" in argv else 2 + return clean_checkout(runs, rust) + return gate(rust, "--write" in argv) + + +if __name__ == "__main__": + raise SystemExit(main()) From e946d82a46a590d3dc9c4eefdf713baf50e2f853 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 3 Oct 2026 17:19:20 +0000 Subject: [PATCH 3/4] fix(typed-builder): clean-checkout leftover check counts only .NET build output The first official clean-checkout run reported the tracked Rust source directory rust/crates/own-shadow/src/bin as build output. Only a bin/ or obj/ beside a .csproj is .NET build output. Gate mechanics only; no registered expectation changes. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_011ZFvhLx1fM9Gerg4dKsZcL --- scripts/typed_builder_gate.py | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/scripts/typed_builder_gate.py b/scripts/typed_builder_gate.py index f909fe26..ef3494a3 100644 --- a/scripts/typed_builder_gate.py +++ b/scripts/typed_builder_gate.py @@ -370,8 +370,11 @@ def clean_checkout(runs: int, rust: str | None) -> int: print(f"FAIL: clean-checkout/run{n}: git worktree add: {added.stderr.strip()}") return 1 try: - leftovers = [d for _, dirs, _ in os.walk(tree) for d in dirs - if d in ("bin", "obj")] + # .NET build output: a bin/ or obj/ beside a project file (a tracked + # directory that merely has the name, like a Rust `src/bin`, is source) + leftovers = [os.path.relpath(os.path.join(base, d), tree) + for base, dirs, names in os.walk(tree) for d in dirs + if d in ("bin", "obj") and any(n.endswith(".csproj") for n in names)] if leftovers: print(f"FAIL: clean-checkout/run{n}: the worktree has build output: " f"{leftovers}") From 04cb779a4ce8047e563d35edc72bdce9a13eaca8 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 3 Oct 2026 17:30:54 +0000 Subject: [PATCH 4/4] docs(tb-mvp): TB-MVP-01 report and verdict (GO_TYPED_BUILDER_MVP) Official run history (run 1 FAIL on a gate-check defect, fixed in e946d82; run 2 PASS), counts, transition evidence, H1-H18, the 18 GO conditions and what the slice does not claim. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_011ZFvhLx1fM9Gerg4dKsZcL --- docs/notes/tb-mvp-01-report.md | 148 +++++++++++++++++++++++++++++++++ 1 file changed, 148 insertions(+) create mode 100644 docs/notes/tb-mvp-01-report.md diff --git a/docs/notes/tb-mvp-01-report.md b/docs/notes/tb-mvp-01-report.md new file mode 100644 index 00000000..3803fc5d --- /dev/null +++ b/docs/notes/tb-mvp-01-report.md @@ -0,0 +1,148 @@ +# TB-MVP-01 — Typed Builder Order vertical slice: report and verdict + +**VERDICT: `GO_TYPED_BUILDER_MVP`.** + +| | commit | +|---|---| +| base (`main`, H1 merged, #390) | `877ee69f28ba169c1fd68935b41f4ef26d92f186` | +| preregistration | `cf7eb01` ([`tb-mvp-01-preregistration.md`](tb-mvp-01-preregistration.md)) | +| implementation | `95d811b` | +| gate fix (clean-checkout check only) | `e946d82` | +| official run (PASS) | `e946d82a46a5` | + +Sample: [`samples/OrderBackend`](../../samples/OrderBackend). Gate: +`scripts/typed_builder_gate.py`. + +## Official runs + +1. **Run 1 — FAIL**, at `95d811b`: `--clean-checkout --runs 2 --rust`. + - Every step of both worktree runs passed, with 0 failures each, and the evidence digests matched across the two runs. + - The run still failed on the gate's own "no build output in a fresh checkout" check. It reported `rust/crates/own-shadow/src/bin`, which is tracked Rust source, not .NET build output. + - **Defect in the gate check, not in the slice.** `e946d82` narrows it to `bin/`/`obj/` beside a `.csproj`. It changes no registered expectation, and was committed before the rerun. +2. **Run 2 — PASS**, at `e946d82`: same command. Each of two fresh `git worktree`s of HEAD, with no `bin/`/`obj/`, restores, builds, generates, scans, runs the corpus and runs the acceptance twice. + + | evidence | run 1 | run 2 | + |---|---|---| + | `acceptance.txt` | `ba447304cdf957ee` | `ba447304cdf957ee` | + | `corpus.json` | `62d7b100a2ebd186` | `62d7b100a2ebd186` | + | `orderbackend.facts.json` | `e9a0c81d941d3b50` | `e9a0c81d941d3b50` | + + Both runs also equal the committed `samples/OrderBackend/evidence/*`. Full sha256: + - `acceptance.txt` `ba447304cdf957eef3f04adb6d1d5ee7847be3d21262f221101c5e25d9a12cc3`; + - `corpus.json` `62d7b100a2ebd18605cc121920cab4085505eaea08594c5e633adbb2db520722`; + - `orderbackend.facts.json` `e9a0c81d941d3b501b85b2123d2383d2d1edcc6e07c690996825f18a30d4f191`; + - generated `Order.Protocol.cs` `857f02768f6531c7e6e498af5d0528dbdbba435cb610632e2e0c2d65d5f33484`. + +**Before the official run.** Three development-time gate failures were fixed in the gate's +own matching. No expectation in the registration changed: +- a comment `Starts a new Order` matched the "no entity created outside `Build()`" regex; +- the compiler names `'Order.Status'` and `'Order.Order()'`, while the gate looked for `'Status'` and `'Order'`. + +## Counts + +| | | +|---|---| +| generated state types | 4: `DraftOrder`, `SubmittedOrder`, `ApprovedOrder`, `ShippedOrder` | +| generated transitions | 3: `Submit`, `Approve`, `Ship` | +| generated region entries (checked refinement) | 3: `WithDraft`, `WithSubmitted`, `WithApproved` (none for the terminal state) | +| generated builder | `Order.Create().Customer(…).Build()`: 1 required field, 1 step | +| positive fixtures | 8 (P1–P8), all `[]` on both CLIs | +| negative fixtures | 20: 10 compiler, 3 extractor, 7 core (C1–C15 with C7b, C10a–c, C11a–b, C12a–b) | +| stated limits | 2 (K1 `OWN001`, K2 `[]`) | +| HTTP happy-path requests | 5 (create, submit, approve, ship, get) + 1 list | +| HTTP rejected transitions | 9, all `409`; plus 4 `404`, 2 `400` create, 16 `500 corrupt_state`, 1 `400` unknown status | +| EF tracked-identity checks | 3 at run time (`h10-*`) + 1 structural (generated tokens wrap only `order`/`_order`) | +| database persistence checks (raw SQL oracle) | 5 row-content checks (4 happy-path rows + `h11`) + 13 row-unchanged checks (9 × H9, 4 × H8) + `h12` | +| acceptance checks | 44 per run, 2 runs per gate, 2 gates | + +## The transitions, with their protocol evidence (P26) + +These come from the real sample's facts (`evidence/orderbackend.facts.json`). Verdict `[]` on +Python and Rust, byte-identical CLI output. + +| source method | before | transition | after | OwnIR in the region | verdict | +|---|---|---|---|---|---| +| `OrderEndpoints.Create` | (none) | `Order.Create().Customer(c).Build()` | Draft | no region: creation | `[]` | +| `OrderEndpoints.Submit` | Draft | `draft.Submit(now)` | Submitted | `acquire draft`, `call DraftOrder.Submit` | `[]` | +| `OrderEndpoints.Approve` | Submitted | `submitted.Approve(now)` | Approved | `acquire submitted`, `call SubmittedOrder.Approve` | `[]` | +| `OrderEndpoints.Ship` | Approved | `approved.Ship(now, Shipping.TrackingNumber(id))` | Shipped | `acquire approved`, **`proven_call OrderBackend.Shipping.TrackingNumber(int)`**, `call ApprovedOrder.Ship` | `[]` | + +**H1 used for real.** `heap_effects` holds the record of +`OrderBackend.Shipping.TrackingNumber(int)` (no writes, no derefs, no calls, inert parameter) +and the record of its call site `site:samples/OrderBackend/OrderBackend/OrderEndpoints.cs:97:36`. +The core admits the site through the unchanged H1 predicate. Nothing in the extractor, the +core or the predicate names the sample. + +**Rejected fixtures.** The exact texts are in `evidence/corpus.json`: + +| | stage | observed | +|---|---|---| +| C1–C6 | compiler | CS1061: `'DraftOrder'`/`'SubmittedOrder'`/`'ApprovedOrder'` does not contain a definition for the illegal transition | +| C7 | compiler | CS1061: `'ShippedOrder' does not contain a definition for 'Submit'` | +| C7b | compiler | CS0117: `'OrderProtocol' does not contain a definition for 'WithShipped'` | +| C8, C9 | core | `OWN002` | +| C10a | extractor | `'ApplyShip' of 'Order' is not public and belongs to a state protocol` | +| C10b | core | `OWN013` | +| C10c | compiler | CS0272: `'Order.Status' cannot be used in this context because the set accessor is inaccessible` | +| C11a | core | `OWN005` | +| C11b | core | `OWN013` | +| C12a | core | refused: `'…C12aHarmfulHelper.Counter.Next()': writes.static is may` | +| C12b | extractor | `a call to '…LoggerExtensions.LogInformation' inside a protocol region runs code with no stated contract` | +| C13 | compiler | CS1061: `'Order.DraftBuilder.CustomerStep' does not contain a definition for 'Build'` | +| C14 | extractor | `a protocol token 'ApprovedOrder' is created outside the protocol's own types` | +| C15 | compiler | CS0122: `'Order.Order()' is inaccessible due to its protection level` | + +## H1–H18 + +| H | result | evidence | +|---|---|---| +| H1 Draft cannot Approve | PASS | C1 | +| H2 Draft cannot Ship | PASS | C2 | +| H3 Submitted cannot Submit | PASS | C3 | +| H4 Approved cannot Submit | PASS | C5 | +| H5 Shipped has no transition | PASS | C7, C7b | +| H6 stale Draft rejected | PASS | C8 `OWN002` | +| H7 raw Order cannot bypass | PASS | C10a (extractor), C10b `OWN013`, C10c CS0272, C14 | +| H8 invalid DB state never refines | PASS | `h8-corrupt-*` ×4, `h8-storage-strict` | +| H9 wrong HTTP transition writes nothing | PASS | `h9-*` ×9, each with the row byte-unchanged | +| H10 same EF entity tracked | PASS | `h10-same-instance-before/after`, `h10-tracked-change` | +| H11 SaveChanges persists exactly the new state | PASS | `h11-saved-exactly`: raw columns changed = `Status,SubmittedAt` | +| H12 reload refines by the persisted state | PASS | `h12-reload-refine` | +| H13 ordinary LINQ | PASS | P7, `h13-linq-*` (server-side `WHERE "o"."Status" = 'Approved'`) | +| H14 harmless helper via `proven_call` | PASS | P5, P8, the real sample's Ship region | +| H15 harmful/Unknown helper rejected | PASS | C12a (core), C12b (extractor) | +| H16 copy/alias backdoor rejected | PASS | C11a `OWN005`, C11b `OWN013` | +| H17 generator deterministic | PASS | 2 generations per gate run, byte-identical, equal to the committed file | +| H18 full runs deterministic | PASS | digests above | + +## The 18 GO conditions + +1. **One ordinary EF Order underlies all typed states.** One `Orders` table. Every token wraps the region's own `order` (structural check), and the tracked instance is the one transitioned (`h10-*`). +2. **Valid transitions are typed.** P2–P4, P8. +3. **Invalid transitions are absent before run time.** C1–C7b. +4. **Stale reuse is rejected.** C8, C9. +5. **A runtime-loaded Order refines safely.** P6, `h12`. +6. **Invalid persisted state cannot fabricate a state.** H8. EF Core 8's own string converter would have mapped `'7'` to an undefined value and `'approved'` to `Approved`; the generated strict converter refuses all four. +7. **The ChangeTracker tracks the same entity.** H10. +8. **SaveChanges persists correctly.** H11; `ef-update-emitted`. +9. **DbSet/LINQ stays usable.** H13. +10. **The HTTP happy path passes.** `http-*` and `oracle-*`, with a raw row after each step. +11. **Wrong runtime transitions leave the DB unchanged.** H9. +12. **H1 `proven_call` is exercised.** H14. +13. **Harmful and Unknown calls are fail-closed.** H15. +14. **The independent oracle confirms identity and persisted state.** Raw `Microsoft.Data.Sqlite`, the ChangeTracker, and exact HTTP bodies; none goes through the typed API. +15. **Generator and full runs are deterministic.** H17, H18. +16. **The clean-checkout run passes.** Official run 2. +17. **H1–H18 pass.** +18. **Foundations are unchanged.** `git diff --stat 877ee69f..HEAD -- ownlang rust spec frontend/roslyn/OwnSharp.Extractor docs/evidence/calibration scripts/perf_baseline.py` is empty. On HEAD, `protocol_gate.py --rust` gives 0 failures with 29 documents byte-identical, `heap_effects_gate.py` PASS. `tests/run_tests.py` gave rc 0 at `95d811b`; `e946d82` changes only the gate script. + +## What the slice does not claim + +- **Concurrency: option A, out of scope.** No concurrency token. +- **K1.** A named terminal token is `OWN001`: tokens are linear, not affine (P-010, case G6). The handlers discard the terminal token as an expression statement. Affine tokens are foundation work, not done here. +- **K2.** `ExecuteUpdate`, metadata writes, raw SQL, reflection and other processes are outside the claim, as in the profile. +- **The diagnostics' wording** is the core's generic resource wording (`IDisposable local 'draft' is used after it is disposed`). The codes are right. The words are a UX item, not changed here (foundation). +- **No BCL or logger summaries and no typed write targets were needed.** Logging and the clock stay outside the region: the clock is read before it, and nothing is logged. + +**After this verdict: STOP.** No BCL summaries, typed write targets or second aggregate are +started.