Skip to content

Commit 95d811b

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

55 files changed

Lines changed: 3944 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
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>

‎frontend/roslyn/Own.TypedBuilder/Program.cs‎

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

‎frontend/roslyn/README.md‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -114,6 +114,11 @@ API, EF Core, SQLite — is in
114114
[`protocol-samples/efcore`](protocol-samples/efcore), and
115115
`python scripts/protocol_gate.py` ties every committed fact back to the C# it came
116116
from.
117+
The product-shaped version of the same backend, with the protocol **generated**
118+
from one annotated declaration (`frontend/roslyn/Own.TypedBuilder`), a typed
119+
builder, and every transition over HTTP, is
120+
[`samples/OrderBackend`](../../samples/OrderBackend) (TB-MVP-01,
121+
`python scripts/typed_builder_gate.py`).
117122

118123
**What is claimed.** The profile protects the local C# capabilities and aliases of
119124
an entity that already exists. It does **not** protect the persisted row from

‎samples/OrderBackend/.gitignore‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
bin/
2+
obj/
Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
<Project Sdk="Microsoft.NET.Sdk.Web">
2+
3+
<PropertyGroup>
4+
<OutputType>Exe</OutputType>
5+
<TargetFramework>net8.0</TargetFramework>
6+
<LangVersion>12</LangVersion>
7+
<Nullable>enable</Nullable>
8+
<ImplicitUsings>enable</ImplicitUsings>
9+
<RootNamespace>OrderBackend.Acceptance</RootNamespace>
10+
</PropertyGroup>
11+
12+
<ItemGroup>
13+
<ProjectReference Include="..\OrderBackend\OrderBackend.csproj" />
14+
</ItemGroup>
15+
16+
</Project>

‎samples/OrderBackend/Acceptance/Program.cs‎

Lines changed: 358 additions & 0 deletions
Large diffs are not rendered by default.
Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
using Microsoft.EntityFrameworkCore;
2+
using OrderBackend.Domain;
3+
4+
namespace OrderBackend.Data;
5+
6+
/// A plain DbContext: no custom base, no repository, no interceptor, no query provider.
7+
public sealed class OrdersDb(DbContextOptions<OrdersDb> options) : DbContext(options)
8+
{
9+
public DbSet<Order> Orders => Set<Order>();
10+
11+
protected override void OnModelCreating(ModelBuilder modelBuilder)
12+
{
13+
modelBuilder.Entity<Order>(order =>
14+
{
15+
order.HasKey(o => o.Id);
16+
order.Property(o => o.Customer).IsRequired();
17+
// the exact member name, strictly: an unknown stored value is an exception at
18+
// materialization, never a state (OrderStatusStorage is generated)
19+
order.Property(o => o.Status).HasConversion(
20+
state => OrderStatusStorage.ToStore(state),
21+
raw => OrderStatusStorage.FromStore(raw));
22+
});
23+
}
24+
}
Lines changed: 223 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,223 @@
1+
// Generated by Own.TypedBuilder from Order.cs. Do not edit: change Order.cs and regenerate.
2+
//
3+
// The state protocol of Order: one [ProtocolToken] per state, one transition per
4+
// [Transition], one [ProtocolRegion] per state with a way out, the checked refinement,
5+
// the strict storage of the state, and the staged builder. Own.NET analyses this file as
6+
// source: it is the protocol's trusted definition surface.
7+
8+
using System;
9+
10+
namespace OrderBackend.Domain;
11+
12+
partial class Order
13+
{
14+
// Draft -> Submit -> Submitted
15+
internal void ApplySubmit(DateTime at)
16+
{
17+
OnSubmit(at);
18+
Status = OrderStatus.Submitted;
19+
}
20+
21+
// Submitted -> Approve -> Approved
22+
internal void ApplyApprove(DateTime at)
23+
{
24+
OnApprove(at);
25+
Status = OrderStatus.Approved;
26+
}
27+
28+
// Approved -> Ship -> Shipped
29+
internal void ApplyShip(DateTime at, int trackingNumber)
30+
{
31+
OnShip(at, trackingNumber);
32+
Status = OrderStatus.Shipped;
33+
}
34+
35+
/// Starts a new Order in its initial state, Draft. Build() exists only once every
36+
/// required field was given.
37+
public static DraftBuilder.CustomerStep Create() => new();
38+
39+
public sealed class DraftBuilder
40+
{
41+
private readonly string _customer;
42+
43+
private DraftBuilder(string customer)
44+
{
45+
_customer = customer;
46+
}
47+
48+
public Order Build() => new() { Customer = _customer, Status = OrderStatus.Draft };
49+
50+
public sealed class CustomerStep
51+
{
52+
internal CustomerStep()
53+
{
54+
}
55+
56+
public DraftBuilder Customer(string customer)
57+
{
58+
ArgumentNullException.ThrowIfNull(customer);
59+
return new DraftBuilder(customer);
60+
}
61+
}
62+
}
63+
}
64+
65+
/// The runtime half of the refinement: the state came from data, so it is checked once,
66+
/// at the region entry.
67+
public sealed class InvalidOrderStateException(int id, OrderStatus actual, OrderStatus required)
68+
: InvalidOperationException($"order {id} is {actual}, not {required}")
69+
{
70+
public int Id { get; } = id;
71+
72+
public OrderStatus Actual { get; } = actual;
73+
74+
public OrderStatus Required { get; } = required;
75+
}
76+
77+
/// A persisted state that is not exactly one of OrderStatus's names. Never mapped to a
78+
/// state: no default, no case folding, no number.
79+
public sealed class CorruptOrderStateException(string raw)
80+
: InvalidOperationException($"the persisted order state '{raw}' is not an OrderStatus")
81+
{
82+
public string Raw { get; } = raw;
83+
}
84+
85+
/// The one mapping between OrderStatus and its stored text: the exact member name.
86+
public static class OrderStatusStorage
87+
{
88+
public static string ToStore(OrderStatus state) => state switch
89+
{
90+
OrderStatus.Draft => "Draft",
91+
OrderStatus.Submitted => "Submitted",
92+
OrderStatus.Approved => "Approved",
93+
OrderStatus.Shipped => "Shipped",
94+
_ => throw new CorruptOrderStateException(state.ToString()),
95+
};
96+
97+
public static OrderStatus FromStore(string raw) =>
98+
TryFromStore(raw, out var state) ? state : throw new CorruptOrderStateException(raw);
99+
100+
public static bool TryFromStore(string? raw, out OrderStatus state)
101+
{
102+
switch (raw)
103+
{
104+
case "Draft":
105+
state = OrderStatus.Draft;
106+
return true;
107+
case "Submitted":
108+
state = OrderStatus.Submitted;
109+
return true;
110+
case "Approved":
111+
state = OrderStatus.Approved;
112+
return true;
113+
case "Shipped":
114+
state = OrderStatus.Shipped;
115+
return true;
116+
default:
117+
state = default;
118+
return false;
119+
}
120+
}
121+
}
122+
123+
/// Order in state Draft. A transition spends this token and hands back the next one.
124+
[ProtocolToken]
125+
public readonly ref struct DraftOrder
126+
{
127+
private readonly Order _order;
128+
129+
internal DraftOrder(Order order) => _order = order;
130+
131+
public int Id => _order.Id;
132+
133+
public SubmittedOrder Submit(DateTime at)
134+
{
135+
_order.ApplySubmit(at);
136+
return new SubmittedOrder(_order);
137+
}
138+
}
139+
140+
/// Order in state Submitted. A transition spends this token and hands back the next one.
141+
[ProtocolToken]
142+
public readonly ref struct SubmittedOrder
143+
{
144+
private readonly Order _order;
145+
146+
internal SubmittedOrder(Order order) => _order = order;
147+
148+
public int Id => _order.Id;
149+
150+
public ApprovedOrder Approve(DateTime at)
151+
{
152+
_order.ApplyApprove(at);
153+
return new ApprovedOrder(_order);
154+
}
155+
}
156+
157+
/// Order in state Approved. A transition spends this token and hands back the next one.
158+
[ProtocolToken]
159+
public readonly ref struct ApprovedOrder
160+
{
161+
private readonly Order _order;
162+
163+
internal ApprovedOrder(Order order) => _order = order;
164+
165+
public int Id => _order.Id;
166+
167+
public ShippedOrder Ship(DateTime at, int trackingNumber)
168+
{
169+
_order.ApplyShip(at, trackingNumber);
170+
return new ShippedOrder(_order);
171+
}
172+
}
173+
174+
/// Order in state Shipped. Terminal: no transition leaves it.
175+
[ProtocolToken]
176+
public readonly ref struct ShippedOrder
177+
{
178+
private readonly Order _order;
179+
180+
internal ShippedOrder(Order order) => _order = order;
181+
182+
public int Id => _order.Id;
183+
}
184+
185+
public delegate void DraftRegion(DraftOrder draft);
186+
public delegate void SubmittedRegion(SubmittedOrder submitted);
187+
public delegate void ApprovedRegion(ApprovedOrder approved);
188+
189+
/// The checked refinement: an Order whose state is only known at run time becomes a token
190+
/// inside the callback, or the call throws and no token exists. A state no transition
191+
/// leaves has no region: its token could never be spent.
192+
public static class OrderProtocol
193+
{
194+
[ProtocolRegion]
195+
public static void WithDraft(Order order, DraftRegion body)
196+
{
197+
ArgumentNullException.ThrowIfNull(order);
198+
ArgumentNullException.ThrowIfNull(body);
199+
if (order.Status != OrderStatus.Draft)
200+
throw new InvalidOrderStateException(order.Id, order.Status, OrderStatus.Draft);
201+
body(new DraftOrder(order));
202+
}
203+
204+
[ProtocolRegion]
205+
public static void WithSubmitted(Order order, SubmittedRegion body)
206+
{
207+
ArgumentNullException.ThrowIfNull(order);
208+
ArgumentNullException.ThrowIfNull(body);
209+
if (order.Status != OrderStatus.Submitted)
210+
throw new InvalidOrderStateException(order.Id, order.Status, OrderStatus.Submitted);
211+
body(new SubmittedOrder(order));
212+
}
213+
214+
[ProtocolRegion]
215+
public static void WithApproved(Order order, ApprovedRegion body)
216+
{
217+
ArgumentNullException.ThrowIfNull(order);
218+
ArgumentNullException.ThrowIfNull(body);
219+
if (order.Status != OrderStatus.Approved)
220+
throw new InvalidOrderStateException(order.Id, order.Status, OrderStatus.Approved);
221+
body(new ApprovedOrder(order));
222+
}
223+
}

0 commit comments

Comments
 (0)