feat(dafny): definite descriptions over set domains put ecommerce fully on verified kernels

docs/content/docs/roadmap.mdx

@@ -186,7 +186,7 @@ Open follow-ups for the M6 synthesis pipeline. For the prose context, see
 
 | Concern | Tracked in |
 | ------- | ---------- |
-| Dafny `ServiceState` reconciliation (the kernel used to run on fresh per-request state) | shipped for all three targets in [#511](https://github.com/HardMax71/spec_to_rest/pull/511), [#512](https://github.com/HardMax71/spec_to_rest/pull/512), [#513](https://github.com/HardMax71/spec_to_rest/pull/513); CI runs the synthesized url_shortener conformance suites since [#514](https://github.com/HardMax71/spec_to_rest/pull/514). Kernel handlers hydrate state from the database, check the compiled `Requires` twins, and persist mutations in one transaction. Nullable and seq state crossed the go/ts bridges in [#518](https://github.com/HardMax71/spec_to_rest/pull/518); enum fields, scalar collections, query-param kernel ops, and entity/list output shapes followed on all three targets, so todo_list runs every operation on verified kernels fleet-wide. Nested entity collections landed next: ecommerce's `items: Set[LineItem]` hydrates by joining the element rows against the id-list column, optional int query params cross the boundary, and ecommerce runs ten of its eleven operations on verified kernels (RemoveLineItem's definite description over an order's item set stays on the fail-loud stub until TheBy learns set domains). The kernel bodies are Dafny-verified through `synth accept`, with provenance recorded per cache entry. Keyed hydration followed in [#522](https://github.com/HardMax71/spec_to_rest/pull/522): a static contract analysis (`HydrationScope`) scopes each request to the rows its requires and ensures actually touch, so an `UpdateTodo` loads one row instead of the table, inserts hydrate nothing, and the persist delete scan is confined to hydrated rows. The scope is then closed under the service invariants, since the runtime guard and the kernel's precondition evaluate `ServiceStateInv` on the hydrated state. Support loads ([#523](https://github.com/HardMax71/spec_to_rest/pull/523)) keep that closure keyed: a relation an invariant reads through an owner field hydrates by those field values, and a column-guarded existential hydrates through a value-column filter (`payments WHERE order_id IN` the hydrated order keys), executed as wave-ordered phases inside the request transaction. The ecommerce orders/payments reference cycle is cut by the filter itself and the auth users/user_by_email cycle by its bilateral index-equality conjuncts, so a `GetOrder` now touches one order, its line items, its payments, and the referenced skus rather than three whole tables. Content searches, freshness checks, quantifier scans, uncertified cycles, and anything the analyzer does not recognize still fail open to full hydration. |
+| Dafny `ServiceState` reconciliation (the kernel used to run on fresh per-request state) | shipped for all three targets in [#511](https://github.com/HardMax71/spec_to_rest/pull/511), [#512](https://github.com/HardMax71/spec_to_rest/pull/512), [#513](https://github.com/HardMax71/spec_to_rest/pull/513); CI runs the synthesized url_shortener conformance suites since [#514](https://github.com/HardMax71/spec_to_rest/pull/514). Kernel handlers hydrate state from the database, check the compiled `Requires` twins, and persist mutations in one transaction. Nullable and seq state crossed the go/ts bridges in [#518](https://github.com/HardMax71/spec_to_rest/pull/518); enum fields, scalar collections, query-param kernel ops, and entity/list output shapes followed on all three targets, so todo_list runs every operation on verified kernels fleet-wide. Nested entity collections landed next: ecommerce's `items: Set[LineItem]` hydrates by joining the element rows against the id-list column, and optional int query params cross the boundary. With definite descriptions over set domains (`TheBySet`, plus a line-item id uniqueness invariant that makes the description well-defined and nested entity invariants lifted into the owner's state predicate), RemoveLineItem left the fail-loud stub, and every ecommerce operation now runs on a verified kernel or the direct-emit path. The kernel bodies are Dafny-verified through `synth accept`, with provenance recorded per cache entry. Keyed hydration followed in [#522](https://github.com/HardMax71/spec_to_rest/pull/522): a static contract analysis (`HydrationScope`) scopes each request to the rows its requires and ensures actually touch, so an `UpdateTodo` loads one row instead of the table, inserts hydrate nothing, and the persist delete scan is confined to hydrated rows. The scope is then closed under the service invariants, since the runtime guard and the kernel's precondition evaluate `ServiceStateInv` on the hydrated state. Support loads ([#523](https://github.com/HardMax71/spec_to_rest/pull/523)) keep that closure keyed: a relation an invariant reads through an owner field hydrates by those field values, and a column-guarded existential hydrates through a value-column filter (`payments WHERE order_id IN` the hydrated order keys), executed as wave-ordered phases inside the request transaction. The ecommerce orders/payments reference cycle is cut by the filter itself and the auth users/user_by_email cycle by its bilateral index-equality conjuncts, so a `GetOrder` now touches one order, its line items, its payments, and the referenced skus rather than three whole tables. Content searches, freshness checks, quantifier scans, uncertified cycles, and anything the analyzer does not recognize still fail open to full hydration. |
 | Automatic hint discovery, mining proof patterns from verified CEGIS runs instead of hand-curating `HintLibrary` | follow-up, deferred in [the compositional synthesis findings](/research/compositional_synthesis_findings) |
 | Pass@128-scale sampling, raising `CegisBudget.maxIterations` by an order of magnitude for Re:Form-style gains | follow-up, deferred in [the compositional synthesis findings](/research/compositional_synthesis_findings) |
 | Laurel-style assertion localization, inserting `assert` placeholders at the failing line for the model to fill | follow-up |

fixtures/golden/dafny/safe_counter.dfy

@@ -11,6 +11,14 @@ ghost function TheBy<K, V>(m: map<K, V>, p: K -> bool): K
   var k :| k in m && p(k); k
 }
 
+ghost function TheBySet<T>(s: set<T>, p: T -> bool): T
+  requires exists x :: x in s && p(x)
+  requires forall x1, x2 :: x1 in s && x2 in s && p(x1) && p(x2) ==> x1 == x2
+  ensures TheBySet(s, p) in s && p(TheBySet(s, p))
+{
+  var x :| x in s && p(x); x
+}
+
 class ServiceState
 {
   var count: int

fixtures/golden/dafny/todo_list.dfy

@@ -11,6 +11,14 @@ ghost function TheBy<K, V>(m: map<K, V>, p: K -> bool): K
   var k :| k in m && p(k); k
 }
 
+ghost function TheBySet<T>(s: set<T>, p: T -> bool): T
+  requires exists x :: x in s && p(x)
+  requires forall x1, x2 :: x1 in s && x2 in s && p(x1) && p(x2) ==> x1 == x2
+  ensures TheBySet(s, p) in s && p(TheBySet(s, p))
+{
+  var x :| x in s && p(x); x
+}
+
 datatype Status = TODO | IN_PROGRESS | DONE | ARCHIVED
 datatype Priority = LOW | MEDIUM | HIGH | URGENT
 
@@ -219,4 +227,4 @@ method DeleteTodo(st: ServiceState, id: int)
   ensures ServiceStateInv(st)
 {
   // YOUR CODE HERE
-}
+}

fixtures/golden/dafny/url_shortener.dfy

@@ -11,6 +11,14 @@ ghost function TheBy<K, V>(m: map<K, V>, p: K -> bool): K
   var k :| k in m && p(k); k
 }
 
+ghost function TheBySet<T>(s: set<T>, p: T -> bool): T
+  requires exists x :: x in s && p(x)
+  requires forall x1, x2 :: x1 in s && x2 in s && p(x1) && p(x2) ==> x1 == x2
+  ensures TheBySet(s, p) in s && p(TheBySet(s, p))
+{
+  var x :| x in s && p(x); x
+}
+
 type ShortCode = string
 predicate ShortCodeWhere(value: string)
 {