Skip to content

Commit 04cb779

Browse files
claudeclaude
committed
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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011ZFvhLx1fM9Gerg4dKsZcL
1 parent e946d82 commit 04cb779

1 file changed

Lines changed: 148 additions & 0 deletions

File tree

‎docs/notes/tb-mvp-01-report.md‎

Lines changed: 148 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,148 @@
1+
# TB-MVP-01 — Typed Builder Order vertical slice: report and verdict
2+
3+
**VERDICT: `GO_TYPED_BUILDER_MVP`.**
4+
5+
| | commit |
6+
|---|---|
7+
| base (`main`, H1 merged, #390) | `877ee69f28ba169c1fd68935b41f4ef26d92f186` |
8+
| preregistration | `cf7eb01` ([`tb-mvp-01-preregistration.md`](tb-mvp-01-preregistration.md)) |
9+
| implementation | `95d811b` |
10+
| gate fix (clean-checkout check only) | `e946d82` |
11+
| official run (PASS) | `e946d82a46a5` |
12+
13+
Sample: [`samples/OrderBackend`](../../samples/OrderBackend). Gate:
14+
`scripts/typed_builder_gate.py`.
15+
16+
## Official runs
17+
18+
1. **Run 1 — FAIL**, at `95d811b`: `--clean-checkout --runs 2 --rust`.
19+
- Every step of both worktree runs passed, with 0 failures each, and the evidence digests matched across the two runs.
20+
- 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.
21+
- **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.
22+
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.
23+
24+
| evidence | run 1 | run 2 |
25+
|---|---|---|
26+
| `acceptance.txt` | `ba447304cdf957ee` | `ba447304cdf957ee` |
27+
| `corpus.json` | `62d7b100a2ebd186` | `62d7b100a2ebd186` |
28+
| `orderbackend.facts.json` | `e9a0c81d941d3b50` | `e9a0c81d941d3b50` |
29+
30+
Both runs also equal the committed `samples/OrderBackend/evidence/*`. Full sha256:
31+
- `acceptance.txt` `ba447304cdf957eef3f04adb6d1d5ee7847be3d21262f221101c5e25d9a12cc3`;
32+
- `corpus.json` `62d7b100a2ebd18605cc121920cab4085505eaea08594c5e633adbb2db520722`;
33+
- `orderbackend.facts.json` `e9a0c81d941d3b501b85b2123d2383d2d1edcc6e07c690996825f18a30d4f191`;
34+
- generated `Order.Protocol.cs` `857f02768f6531c7e6e498af5d0528dbdbba435cb610632e2e0c2d65d5f33484`.
35+
36+
**Before the official run.** Three development-time gate failures were fixed in the gate's
37+
own matching. No expectation in the registration changed:
38+
- a comment `Starts a new Order` matched the "no entity created outside `Build()`" regex;
39+
- the compiler names `'Order.Status'` and `'Order.Order()'`, while the gate looked for `'Status'` and `'Order'`.
40+
41+
## Counts
42+
43+
| | |
44+
|---|---|
45+
| generated state types | 4: `DraftOrder`, `SubmittedOrder`, `ApprovedOrder`, `ShippedOrder` |
46+
| generated transitions | 3: `Submit`, `Approve`, `Ship` |
47+
| generated region entries (checked refinement) | 3: `WithDraft`, `WithSubmitted`, `WithApproved` (none for the terminal state) |
48+
| generated builder | `Order.Create().Customer(…).Build()`: 1 required field, 1 step |
49+
| positive fixtures | 8 (P1–P8), all `[]` on both CLIs |
50+
| negative fixtures | 20: 10 compiler, 3 extractor, 7 core (C1–C15 with C7b, C10a–c, C11a–b, C12a–b) |
51+
| stated limits | 2 (K1 `OWN001`, K2 `[]`) |
52+
| HTTP happy-path requests | 5 (create, submit, approve, ship, get) + 1 list |
53+
| HTTP rejected transitions | 9, all `409`; plus 4 `404`, 2 `400` create, 16 `500 corrupt_state`, 1 `400` unknown status |
54+
| EF tracked-identity checks | 3 at run time (`h10-*`) + 1 structural (generated tokens wrap only `order`/`_order`) |
55+
| database persistence checks (raw SQL oracle) | 5 row-content checks (4 happy-path rows + `h11`) + 13 row-unchanged checks (9 × H9, 4 × H8) + `h12` |
56+
| acceptance checks | 44 per run, 2 runs per gate, 2 gates |
57+
58+
## The transitions, with their protocol evidence (P26)
59+
60+
These come from the real sample's facts (`evidence/orderbackend.facts.json`). Verdict `[]` on
61+
Python and Rust, byte-identical CLI output.
62+
63+
| source method | before | transition | after | OwnIR in the region | verdict |
64+
|---|---|---|---|---|---|
65+
| `OrderEndpoints.Create` | (none) | `Order.Create().Customer(c).Build()` | Draft | no region: creation | `[]` |
66+
| `OrderEndpoints.Submit` | Draft | `draft.Submit(now)` | Submitted | `acquire draft`, `call DraftOrder.Submit` | `[]` |
67+
| `OrderEndpoints.Approve` | Submitted | `submitted.Approve(now)` | Approved | `acquire submitted`, `call SubmittedOrder.Approve` | `[]` |
68+
| `OrderEndpoints.Ship` | Approved | `approved.Ship(now, Shipping.TrackingNumber(id))` | Shipped | `acquire approved`, **`proven_call OrderBackend.Shipping.TrackingNumber(int)`**, `call ApprovedOrder.Ship` | `[]` |
69+
70+
**H1 used for real.** `heap_effects` holds the record of
71+
`OrderBackend.Shipping.TrackingNumber(int)` (no writes, no derefs, no calls, inert parameter)
72+
and the record of its call site `site:samples/OrderBackend/OrderBackend/OrderEndpoints.cs:97:36`.
73+
The core admits the site through the unchanged H1 predicate. Nothing in the extractor, the
74+
core or the predicate names the sample.
75+
76+
**Rejected fixtures.** The exact texts are in `evidence/corpus.json`:
77+
78+
| | stage | observed |
79+
|---|---|---|
80+
| C1–C6 | compiler | CS1061: `'DraftOrder'`/`'SubmittedOrder'`/`'ApprovedOrder'` does not contain a definition for the illegal transition |
81+
| C7 | compiler | CS1061: `'ShippedOrder' does not contain a definition for 'Submit'` |
82+
| C7b | compiler | CS0117: `'OrderProtocol' does not contain a definition for 'WithShipped'` |
83+
| C8, C9 | core | `OWN002` |
84+
| C10a | extractor | `'ApplyShip' of 'Order' is not public and belongs to a state protocol` |
85+
| C10b | core | `OWN013` |
86+
| C10c | compiler | CS0272: `'Order.Status' cannot be used in this context because the set accessor is inaccessible` |
87+
| C11a | core | `OWN005` |
88+
| C11b | core | `OWN013` |
89+
| C12a | core | refused: `'…C12aHarmfulHelper.Counter.Next()': writes.static is may` |
90+
| C12b | extractor | `a call to '…LoggerExtensions.LogInformation' inside a protocol region runs code with no stated contract` |
91+
| C13 | compiler | CS1061: `'Order.DraftBuilder.CustomerStep' does not contain a definition for 'Build'` |
92+
| C14 | extractor | `a protocol token 'ApprovedOrder' is created outside the protocol's own types` |
93+
| C15 | compiler | CS0122: `'Order.Order()' is inaccessible due to its protection level` |
94+
95+
## H1–H18
96+
97+
| H | result | evidence |
98+
|---|---|---|
99+
| H1 Draft cannot Approve | PASS | C1 |
100+
| H2 Draft cannot Ship | PASS | C2 |
101+
| H3 Submitted cannot Submit | PASS | C3 |
102+
| H4 Approved cannot Submit | PASS | C5 |
103+
| H5 Shipped has no transition | PASS | C7, C7b |
104+
| H6 stale Draft rejected | PASS | C8 `OWN002` |
105+
| H7 raw Order cannot bypass | PASS | C10a (extractor), C10b `OWN013`, C10c CS0272, C14 |
106+
| H8 invalid DB state never refines | PASS | `h8-corrupt-*` ×4, `h8-storage-strict` |
107+
| H9 wrong HTTP transition writes nothing | PASS | `h9-*` ×9, each with the row byte-unchanged |
108+
| H10 same EF entity tracked | PASS | `h10-same-instance-before/after`, `h10-tracked-change` |
109+
| H11 SaveChanges persists exactly the new state | PASS | `h11-saved-exactly`: raw columns changed = `Status,SubmittedAt` |
110+
| H12 reload refines by the persisted state | PASS | `h12-reload-refine` |
111+
| H13 ordinary LINQ | PASS | P7, `h13-linq-*` (server-side `WHERE "o"."Status" = 'Approved'`) |
112+
| H14 harmless helper via `proven_call` | PASS | P5, P8, the real sample's Ship region |
113+
| H15 harmful/Unknown helper rejected | PASS | C12a (core), C12b (extractor) |
114+
| H16 copy/alias backdoor rejected | PASS | C11a `OWN005`, C11b `OWN013` |
115+
| H17 generator deterministic | PASS | 2 generations per gate run, byte-identical, equal to the committed file |
116+
| H18 full runs deterministic | PASS | digests above |
117+
118+
## The 18 GO conditions
119+
120+
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-*`).
121+
2. **Valid transitions are typed.** P2–P4, P8.
122+
3. **Invalid transitions are absent before run time.** C1–C7b.
123+
4. **Stale reuse is rejected.** C8, C9.
124+
5. **A runtime-loaded Order refines safely.** P6, `h12`.
125+
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.
126+
7. **The ChangeTracker tracks the same entity.** H10.
127+
8. **SaveChanges persists correctly.** H11; `ef-update-emitted`.
128+
9. **DbSet/LINQ stays usable.** H13.
129+
10. **The HTTP happy path passes.** `http-*` and `oracle-*`, with a raw row after each step.
130+
11. **Wrong runtime transitions leave the DB unchanged.** H9.
131+
12. **H1 `proven_call` is exercised.** H14.
132+
13. **Harmful and Unknown calls are fail-closed.** H15.
133+
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.
134+
15. **Generator and full runs are deterministic.** H17, H18.
135+
16. **The clean-checkout run passes.** Official run 2.
136+
17. **H1–H18 pass.**
137+
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.
138+
139+
## What the slice does not claim
140+
141+
- **Concurrency: option A, out of scope.** No concurrency token.
142+
- **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.
143+
- **K2.** `ExecuteUpdate`, metadata writes, raw SQL, reflection and other processes are outside the claim, as in the profile.
144+
- **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).
145+
- **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.
146+
147+
**After this verdict: STOP.** No BCL summaries, typed write targets or second aggregate are
148+
started.

0 commit comments

Comments
 (0)