Skip to content

Commit 88cb8cc

Browse files
PhysShellPhysShell
authored
Merge pull request #391 from PhysShell/ccr-d3ed89e2-vnl6fk
feat(typed-builder): OrderBackend vertical-slice MVP over OwnIR v2/H1
2 parents 877ee69 + 04cb779 commit 88cb8cc

57 files changed

Lines changed: 4531 additions & 0 deletions

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎.gitattributes‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -23,3 +23,10 @@
2323
# hashed 79ad1476f219 on Linux and 3dda13ce16d6 on Windows, and a run that
2424
# measured exactly the right tree was rejected as evidence for another tree.
2525
docs/evidence/*.json text eol=lf
26+
27+
# TB-MVP-01: the generated protocol surface is compared BY BYTE with what
28+
# `frontend/roslyn/Own.TypedBuilder` writes (`\n`, no BOM), and the Typed Builder
29+
# gate's evidence is the same bytes on every platform. A Windows checkout with
30+
# `core.autocrlf=true` would make a correct generator look stale.
31+
samples/OrderBackend/OrderBackend/Domain/Order.Protocol.cs text eol=lf
32+
samples/OrderBackend/evidence/* text eol=lf

‎.github/workflows/ci.yml‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3353,6 +3353,16 @@ jobs:
33533353
# no exit code and no stderr — over every protocol case and refusal and examples/.
33543354
- name: Heap-effect sidecar (samples + inertness of --heap-effects)
33553355
run: python scripts/heap_effects_gate.py
3356+
# TB-MVP-01 (docs/notes/tb-mvp-01-preregistration.md): the Typed Builder Order
3357+
# vertical slice. The generator's output is deterministic and committed; the corpus
3358+
# is held to its registered compiler / extractor / core answers; the backend runs
3359+
# real HTTP against real SQLite twice with oracles outside the typed API.
3360+
- name: Typed Builder MVP (generator, corpus, EF + HTTP acceptance)
3361+
if: matrix.os != 'ubuntu-latest'
3362+
run: python scripts/typed_builder_gate.py
3363+
- name: Typed Builder MVP + both public CLIs on every core-stage document
3364+
if: matrix.os == 'ubuntu-latest'
3365+
run: python scripts/typed_builder_gate.py --rust "$PWD/rust/target/debug/own-cli"
33563366

33573367
# P-012 slice 1: score the checker against the labeled corpus on REAL C# — not
33583368
# just the .own reduction tests/test_corpus.py checks. Per case: the bug must be

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

Lines changed: 436 additions & 0 deletions
Large diffs are not rendered by default.

‎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.

‎frontend/roslyn/Own.TypedBuilder/Own.TypedBuilder.csproj‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
<Project Sdk="Microsoft.NET.Sdk">
2+
3+
<PropertyGroup>
4+
<OutputType>Exe</OutputType>
5+
<TargetFramework>net8.0</TargetFramework>
6+
<ImplicitUsings>enable</ImplicitUsings>
7+
<Nullable>enable</Nullable>
8+
<AssemblyName>own-typed-builder</AssemblyName>
9+
<RootNamespace>Own.TypedBuilder</RootNamespace>
10+
</PropertyGroup>
11+
12+
<ItemGroup>
13+
<!-- Syntax only: the generator parses one declaration file, it never builds a
14+
compilation. Same Roslyn as the extractor, so one restore serves both. -->
15+
<PackageReference Include="Microsoft.CodeAnalysis.CSharp" Version="4.9.2" />
16+
</ItemGroup>
17+
18+
</Project>

0 commit comments

Comments
 (0)