diff --git a/docs/content/docs/roadmap.mdx b/docs/content/docs/roadmap.mdx
index c77324f9..f32c5681 100644
--- a/docs/content/docs/roadmap.mdx
+++ b/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 |
diff --git a/fixtures/golden/dafny/safe_counter.dfy b/fixtures/golden/dafny/safe_counter.dfy
index 5d15956f..24737c4c 100644
--- a/fixtures/golden/dafny/safe_counter.dfy
+++ b/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
diff --git a/fixtures/golden/dafny/todo_list.dfy b/fixtures/golden/dafny/todo_list.dfy
index b05fad45..1b5da5e3 100644
--- a/fixtures/golden/dafny/todo_list.dfy
+++ b/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
-}
\ No newline at end of file
+}
diff --git a/fixtures/golden/dafny/url_shortener.dfy b/fixtures/golden/dafny/url_shortener.dfy
index bf1d2694..9d90cfbf 100644
--- a/fixtures/golden/dafny/url_shortener.dfy
+++ b/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)
 {
diff --git a/fixtures/golden/ir/ecommerce.json b/fixtures/golden/ir/ecommerce.json
index 81cc9685..4e971f3c 100644
--- a/fixtures/golden/ir/ecommerce.json
+++ b/fixtures/golden/ir/ecommerce.json
@@ -11941,6 +11941,260 @@
         "endCol" : 57
       }
     },
+    {
+      "kind" : "Invariant",
+      "name" : "lineItemIdsUnique",
+      "expr" : {
+        "kind" : "Quantifier",
+        "quantifier" : "all",
+        "bindings" : [
+          {
+            "variable" : "oid",
+            "domain" : {
+              "kind" : "Identifier",
+              "name" : "orders",
+              "span" : {
+                "startLine" : 413,
+                "startCol" : 15,
+                "endLine" : 413,
+                "endCol" : 21
+              }
+            },
+            "bindingKind" : "in",
+            "span" : {
+              "startLine" : 413,
+              "startCol" : 8,
+              "endLine" : 413,
+              "endCol" : 21
+            }
+          }
+        ],
+        "body" : {
+          "kind" : "Quantifier",
+          "quantifier" : "all",
+          "bindings" : [
+            {
+              "variable" : "i1",
+              "domain" : {
+                "kind" : "FieldAccess",
+                "base" : {
+                  "kind" : "Index",
+                  "base" : {
+                    "kind" : "Identifier",
+                    "name" : "orders",
+                    "span" : {
+                      "startLine" : 414,
+                      "startCol" : 16,
+                      "endLine" : 414,
+                      "endCol" : 22
+                    }
+                  },
+                  "index" : {
+                    "kind" : "Identifier",
+                    "name" : "oid",
+                    "span" : {
+                      "startLine" : 414,
+                      "startCol" : 23,
+                      "endLine" : 414,
+                      "endCol" : 26
+                    }
+                  },
+                  "span" : {
+                    "startLine" : 414,
+                    "startCol" : 16,
+                    "endLine" : 414,
+                    "endCol" : 27
+                  }
+                },
+                "field" : "items",
+                "span" : {
+                  "startLine" : 414,
+                  "startCol" : 16,
+                  "endLine" : 414,
+                  "endCol" : 33
+                }
+              },
+              "bindingKind" : "in",
+              "span" : {
+                "startLine" : 414,
+                "startCol" : 10,
+                "endLine" : 414,
+                "endCol" : 33
+              }
+            }
+          ],
+          "body" : {
+            "kind" : "Quantifier",
+            "quantifier" : "all",
+            "bindings" : [
+              {
+                "variable" : "i2",
+                "domain" : {
+                  "kind" : "FieldAccess",
+                  "base" : {
+                    "kind" : "Index",
+                    "base" : {
+                      "kind" : "Identifier",
+                      "name" : "orders",
+                      "span" : {
+                        "startLine" : 415,
+                        "startCol" : 18,
+                        "endLine" : 415,
+                        "endCol" : 24
+                      }
+                    },
+                    "index" : {
+                      "kind" : "Identifier",
+                      "name" : "oid",
+                      "span" : {
+                        "startLine" : 415,
+                        "startCol" : 25,
+                        "endLine" : 415,
+                        "endCol" : 28
+                      }
+                    },
+                    "span" : {
+                      "startLine" : 415,
+                      "startCol" : 18,
+                      "endLine" : 415,
+                      "endCol" : 29
+                    }
+                  },
+                  "field" : "items",
+                  "span" : {
+                    "startLine" : 415,
+                    "startCol" : 18,
+                    "endLine" : 415,
+                    "endCol" : 35
+                  }
+                },
+                "bindingKind" : "in",
+                "span" : {
+                  "startLine" : 415,
+                  "startCol" : 12,
+                  "endLine" : 415,
+                  "endCol" : 35
+                }
+              }
+            ],
+            "body" : {
+              "kind" : "BinaryOp",
+              "op" : "implies",
+              "left" : {
+                "kind" : "BinaryOp",
+                "op" : "=",
+                "left" : {
+                  "kind" : "FieldAccess",
+                  "base" : {
+                    "kind" : "Identifier",
+                    "name" : "i1",
+                    "span" : {
+                      "startLine" : 416,
+                      "startCol" : 10,
+                      "endLine" : 416,
+                      "endCol" : 12
+                    }
+                  },
+                  "field" : "id",
+                  "span" : {
+                    "startLine" : 416,
+                    "startCol" : 10,
+                    "endLine" : 416,
+                    "endCol" : 15
+                  }
+                },
+                "right" : {
+                  "kind" : "FieldAccess",
+                  "base" : {
+                    "kind" : "Identifier",
+                    "name" : "i2",
+                    "span" : {
+                      "startLine" : 416,
+                      "startCol" : 18,
+                      "endLine" : 416,
+                      "endCol" : 20
+                    }
+                  },
+                  "field" : "id",
+                  "span" : {
+                    "startLine" : 416,
+                    "startCol" : 18,
+                    "endLine" : 416,
+                    "endCol" : 23
+                  }
+                },
+                "span" : {
+                  "startLine" : 416,
+                  "startCol" : 10,
+                  "endLine" : 416,
+                  "endCol" : 23
+                }
+              },
+              "right" : {
+                "kind" : "BinaryOp",
+                "op" : "=",
+                "left" : {
+                  "kind" : "Identifier",
+                  "name" : "i1",
+                  "span" : {
+                    "startLine" : 416,
+                    "startCol" : 32,
+                    "endLine" : 416,
+                    "endCol" : 34
+                  }
+                },
+                "right" : {
+                  "kind" : "Identifier",
+                  "name" : "i2",
+                  "span" : {
+                    "startLine" : 416,
+                    "startCol" : 37,
+                    "endLine" : 416,
+                    "endCol" : 39
+                  }
+                },
+                "span" : {
+                  "startLine" : 416,
+                  "startCol" : 32,
+                  "endLine" : 416,
+                  "endCol" : 39
+                }
+              },
+              "span" : {
+                "startLine" : 416,
+                "startCol" : 10,
+                "endLine" : 416,
+                "endCol" : 39
+              }
+            },
+            "span" : {
+              "startLine" : 415,
+              "startCol" : 8,
+              "endLine" : 416,
+              "endCol" : 39
+            }
+          },
+          "span" : {
+            "startLine" : 414,
+            "startCol" : 6,
+            "endLine" : 416,
+            "endCol" : 39
+          }
+        },
+        "span" : {
+          "startLine" : 413,
+          "startCol" : 4,
+          "endLine" : 416,
+          "endCol" : 39
+        }
+      },
+      "span" : {
+        "startLine" : 412,
+        "startCol" : 2,
+        "endLine" : 416,
+        "endCol" : 39
+      }
+    },
     {
       "kind" : "Invariant",
       "name" : "nextOrderIdFresh",
@@ -11954,17 +12208,17 @@
               "kind" : "Identifier",
               "name" : "orders",
               "span" : {
-                "startLine" : 410,
+                "startLine" : 419,
                 "startCol" : 15,
-                "endLine" : 410,
+                "endLine" : 419,
                 "endCol" : 21
               }
             },
             "bindingKind" : "in",
             "span" : {
-              "startLine" : 410,
+              "startLine" : 419,
               "startCol" : 8,
-              "endLine" : 410,
+              "endLine" : 419,
               "endCol" : 21
             }
           }
@@ -11976,9 +12230,9 @@
             "kind" : "Identifier",
             "name" : "oid",
             "span" : {
-              "startLine" : 410,
+              "startLine" : 419,
               "startCol" : 24,
-              "endLine" : 410,
+              "endLine" : 419,
               "endCol" : 27
             }
           },
@@ -11986,30 +12240,30 @@
             "kind" : "Identifier",
             "name" : "next_order_id",
             "span" : {
-              "startLine" : 410,
+              "startLine" : 419,
               "startCol" : 30,
-              "endLine" : 410,
+              "endLine" : 419,
               "endCol" : 43
             }
           },
           "span" : {
-            "startLine" : 410,
+            "startLine" : 419,
             "startCol" : 24,
-            "endLine" : 410,
+            "endLine" : 419,
             "endCol" : 43
           }
         },
         "span" : {
-          "startLine" : 410,
+          "startLine" : 419,
           "startCol" : 4,
-          "endLine" : 410,
+          "endLine" : 419,
           "endCol" : 43
         }
       },
       "span" : {
-        "startLine" : 409,
+        "startLine" : 418,
         "startCol" : 2,
-        "endLine" : 410,
+        "endLine" : 419,
         "endCol" : 43
       }
     },
@@ -12026,17 +12280,17 @@
               "kind" : "Identifier",
               "name" : "payments",
               "span" : {
-                "startLine" : 413,
+                "startLine" : 422,
                 "startCol" : 15,
-                "endLine" : 413,
+                "endLine" : 422,
                 "endCol" : 23
               }
             },
             "bindingKind" : "in",
             "span" : {
-              "startLine" : 413,
+              "startLine" : 422,
               "startCol" : 8,
-              "endLine" : 413,
+              "endLine" : 422,
               "endCol" : 23
             }
           }
@@ -12052,9 +12306,9 @@
                 "kind" : "Identifier",
                 "name" : "payments",
                 "span" : {
-                  "startLine" : 413,
+                  "startLine" : 422,
                   "startCol" : 26,
-                  "endLine" : 413,
+                  "endLine" : 422,
                   "endCol" : 34
                 }
               },
@@ -12062,24 +12316,24 @@
                 "kind" : "Identifier",
                 "name" : "pid",
                 "span" : {
-                  "startLine" : 413,
+                  "startLine" : 422,
                   "startCol" : 35,
-                  "endLine" : 413,
+                  "endLine" : 422,
                   "endCol" : 38
                 }
               },
               "span" : {
-                "startLine" : 413,
+                "startLine" : 422,
                 "startCol" : 26,
-                "endLine" : 413,
+                "endLine" : 422,
                 "endCol" : 39
               }
             },
             "field" : "order_id",
             "span" : {
-              "startLine" : 413,
+              "startLine" : 422,
               "startCol" : 26,
-              "endLine" : 413,
+              "endLine" : 422,
               "endCol" : 48
             }
           },
@@ -12087,30 +12341,30 @@
             "kind" : "Identifier",
             "name" : "orders",
             "span" : {
-              "startLine" : 413,
+              "startLine" : 422,
               "startCol" : 52,
-              "endLine" : 413,
+              "endLine" : 422,
               "endCol" : 58
             }
           },
           "span" : {
-            "startLine" : 413,
+            "startLine" : 422,
             "startCol" : 26,
-            "endLine" : 413,
+            "endLine" : 422,
             "endCol" : 58
           }
         },
         "span" : {
-          "startLine" : 413,
+          "startLine" : 422,
           "startCol" : 4,
-          "endLine" : 413,
+          "endLine" : 422,
           "endCol" : 58
         }
       },
       "span" : {
-        "startLine" : 412,
+        "startLine" : 421,
         "startCol" : 2,
-        "endLine" : 413,
+        "endLine" : 422,
         "endCol" : 58
       }
     }
@@ -12240,9 +12494,9 @@
           "value" : "/orders"
         },
         "span" : {
-          "startLine" : 418,
+          "startLine" : 427,
           "startCol" : 4,
-          "endLine" : 418,
+          "endLine" : 427,
           "endCol" : 42
         }
       },
@@ -12256,9 +12510,9 @@
           "value" : 201
         },
         "span" : {
-          "startLine" : 419,
+          "startLine" : 428,
           "startCol" : 4,
-          "endLine" : 419,
+          "endLine" : 428,
           "endCol" : 46
         }
       },
@@ -12272,9 +12526,9 @@
           "value" : "POST"
         },
         "span" : {
-          "startLine" : 421,
+          "startLine" : 430,
           "startCol" : 4,
-          "endLine" : 421,
+          "endLine" : 430,
           "endCol" : 36
         }
       },
@@ -12288,9 +12542,9 @@
           "value" : "/orders/{order_id}/items"
         },
         "span" : {
-          "startLine" : 422,
+          "startLine" : 431,
           "startCol" : 4,
-          "endLine" : 422,
+          "endLine" : 431,
           "endCol" : 54
         }
       },
@@ -12304,9 +12558,9 @@
           "value" : 201
         },
         "span" : {
-          "startLine" : 423,
+          "startLine" : 432,
           "startCol" : 4,
-          "endLine" : 423,
+          "endLine" : 432,
           "endCol" : 41
         }
       },
@@ -12320,9 +12574,9 @@
           "value" : "DELETE"
         },
         "span" : {
-          "startLine" : 425,
+          "startLine" : 434,
           "startCol" : 4,
-          "endLine" : 425,
+          "endLine" : 434,
           "endCol" : 41
         }
       },
@@ -12336,12 +12590,28 @@
           "value" : "/orders/{order_id}/items/{item_id}"
         },
         "span" : {
-          "startLine" : 426,
+          "startLine" : 435,
           "startCol" : 4,
-          "endLine" : 426,
+          "endLine" : 435,
           "endCol" : 67
         }
       },
+      {
+        "kind" : "ConventionRule",
+        "target" : "RemoveLineItem",
+        "property" : "http_status_success",
+        "qualifier" : null,
+        "value" : {
+          "kind" : "IntLit",
+          "value" : 200
+        },
+        "span" : {
+          "startLine" : 438,
+          "startCol" : 4,
+          "endLine" : 438,
+          "endCol" : 44
+        }
+      },
       {
         "kind" : "ConventionRule",
         "target" : "PlaceOrder",
@@ -12352,9 +12622,9 @@
           "value" : "POST"
         },
         "span" : {
-          "startLine" : 428,
+          "startLine" : 440,
           "startCol" : 4,
-          "endLine" : 428,
+          "endLine" : 440,
           "endCol" : 35
         }
       },
@@ -12368,9 +12638,9 @@
           "value" : "/orders/{order_id}/place"
         },
         "span" : {
-          "startLine" : 429,
+          "startLine" : 441,
           "startCol" : 4,
-          "endLine" : 429,
+          "endLine" : 441,
           "endCol" : 53
         }
       },
@@ -12384,9 +12654,9 @@
           "value" : "POST"
         },
         "span" : {
-          "startLine" : 431,
+          "startLine" : 443,
           "startCol" : 4,
-          "endLine" : 431,
+          "endLine" : 443,
           "endCol" : 38
         }
       },
@@ -12400,9 +12670,9 @@
           "value" : "/orders/{order_id}/payments"
         },
         "span" : {
-          "startLine" : 432,
+          "startLine" : 444,
           "startCol" : 4,
-          "endLine" : 432,
+          "endLine" : 444,
           "endCol" : 59
         }
       },
@@ -12416,9 +12686,9 @@
           "value" : 201
         },
         "span" : {
-          "startLine" : 433,
+          "startLine" : 445,
           "startCol" : 4,
-          "endLine" : 433,
+          "endLine" : 445,
           "endCol" : 43
         }
       },
@@ -12432,9 +12702,9 @@
           "value" : "POST"
         },
         "span" : {
-          "startLine" : 435,
+          "startLine" : 447,
           "startCol" : 4,
-          "endLine" : 435,
+          "endLine" : 447,
           "endCol" : 34
         }
       },
@@ -12448,9 +12718,9 @@
           "value" : "/orders/{order_id}/ship"
         },
         "span" : {
-          "startLine" : 436,
+          "startLine" : 448,
           "startCol" : 4,
-          "endLine" : 436,
+          "endLine" : 448,
           "endCol" : 51
         }
       },
@@ -12464,9 +12734,9 @@
           "value" : "POST"
         },
         "span" : {
-          "startLine" : 438,
+          "startLine" : 450,
           "startCol" : 4,
-          "endLine" : 438,
+          "endLine" : 450,
           "endCol" : 40
         }
       },
@@ -12480,9 +12750,9 @@
           "value" : "/orders/{order_id}/deliver"
         },
         "span" : {
-          "startLine" : 439,
+          "startLine" : 451,
           "startCol" : 4,
-          "endLine" : 439,
+          "endLine" : 451,
           "endCol" : 60
         }
       },
@@ -12496,9 +12766,9 @@
           "value" : "POST"
         },
         "span" : {
-          "startLine" : 441,
+          "startLine" : 453,
           "startCol" : 4,
-          "endLine" : 441,
+          "endLine" : 453,
           "endCol" : 36
         }
       },
@@ -12512,9 +12782,9 @@
           "value" : "/orders/{order_id}/cancel"
         },
         "span" : {
-          "startLine" : 442,
+          "startLine" : 454,
           "startCol" : 4,
-          "endLine" : 442,
+          "endLine" : 454,
           "endCol" : 55
         }
       },
@@ -12528,9 +12798,9 @@
           "value" : "POST"
         },
         "span" : {
-          "startLine" : 444,
+          "startLine" : 456,
           "startCol" : 4,
-          "endLine" : 444,
+          "endLine" : 456,
           "endCol" : 38
         }
       },
@@ -12544,9 +12814,9 @@
           "value" : "/orders/{order_id}/return"
         },
         "span" : {
-          "startLine" : 445,
+          "startLine" : 457,
           "startCol" : 4,
-          "endLine" : 445,
+          "endLine" : 457,
           "endCol" : 57
         }
       },
@@ -12560,9 +12830,9 @@
           "value" : "/orders/{order_id}"
         },
         "span" : {
-          "startLine" : 447,
+          "startLine" : 459,
           "startCol" : 4,
-          "endLine" : 447,
+          "endLine" : 459,
           "endCol" : 45
         }
       },
@@ -12576,9 +12846,9 @@
           "value" : "/orders"
         },
         "span" : {
-          "startLine" : 448,
+          "startLine" : 460,
           "startCol" : 4,
-          "endLine" : 448,
+          "endLine" : 460,
           "endCol" : 36
         }
       },
@@ -12592,24 +12862,24 @@
           "value" : "active = true"
         },
         "span" : {
-          "startLine" : 450,
+          "startLine" : 462,
           "startCol" : 4,
-          "endLine" : 450,
+          "endLine" : 462,
           "endCol" : 52
         }
       }
     ],
     "span" : {
-      "startLine" : 417,
+      "startLine" : 426,
       "startCol" : 2,
-      "endLine" : 451,
+      "endLine" : 463,
       "endCol" : 3
     }
   },
   "span" : {
     "startLine" : 1,
     "startCol" : 0,
-    "endLine" : 452,
+    "endLine" : 464,
     "endCol" : 1
   }
 }
diff --git a/fixtures/spec/ecommerce.spec b/fixtures/spec/ecommerce.spec
index 6e3ca2e7..13b7387d 100644
--- a/fixtures/spec/ecommerce.spec
+++ b/fixtures/spec/ecommerce.spec
@@ -406,6 +406,15 @@ service OrderService {
         all i2 in orders[oid].items |
           i1.product_sku = i2.product_sku implies i1 = i2
 
+  // RemoveLineItem addresses an item by id, so `the i in items | i.id = item_id`
+  // must be well-defined: without this, two items could share an id and the
+  // definite description (and the DELETE route) would be ambiguous.
+  invariant lineItemIdsUnique:
+    all oid in orders |
+      all i1 in orders[oid].items |
+        all i2 in orders[oid].items |
+          i1.id = i2.id implies i1 = i2
+
   invariant nextOrderIdFresh:
     all oid in orders | oid < next_order_id
 
@@ -424,6 +433,9 @@ service OrderService {
 
     RemoveLineItem.http_method = "DELETE"
     RemoveLineItem.http_path = "/orders/{order_id}/items/{item_id}"
+    // The op declares `output: order`, so the DELETE default of 204 (no
+    // body) would discard it; FastAPI even refuses to register such a route.
+    RemoveLineItem.http_status_success = 200
 
     PlaceOrder.http_method = "POST"
     PlaceOrder.http_path = "/orders/{order_id}/place"
diff --git a/fixtures/synth-cache/verified/3c/3c6cff507d8b686609f46799b9f0a2548da845286c2a81375041e741d676a86e.json b/fixtures/synth-cache/verified/3c/3c6cff507d8b686609f46799b9f0a2548da845286c2a81375041e741d676a86e.json
index 434a85ec..7503d8e9 100644
--- a/fixtures/synth-cache/verified/3c/3c6cff507d8b686609f46799b9f0a2548da845286c2a81375041e741d676a86e.json
+++ b/fixtures/synth-cache/verified/3c/3c6cff507d8b686609f46799b9f0a2548da845286c2a81375041e741d676a86e.json
@@ -1,5 +1,5 @@
 {
-  "candidate" : "var o := st.orders[order_id];\nvar product := st.products[sku];\nvar item := LineItem(st.next_line_item_id, order_id, sku, quantity, product.price, product.price * quantity);\nassert item.line_total > 0;\nassert forall i :: i in o.items ==> i.id < st.next_line_item_id;\nassert item !in o.items;\nSumBy_LineItem_line_totalAdd(o.items, item);\norder := o.(items := o.items + {item}, subtotal := o.subtotal + item.line_total, total := o.subtotal + item.line_total + o.tax);\nst.orders := st.orders[order_id := order];\nst.next_line_item_id := st.next_line_item_id + 1;\nst.inventory := st.inventory[sku := st.inventory[sku].(available := st.inventory[sku].available - quantity)];\n",
+  "candidate" : "var o := st.orders[order_id];\nvar product := st.products[sku];\nvar item := LineItem(st.next_line_item_id, order_id, sku, quantity, product.price, product.price * quantity);\nassert item.line_total > 0;\nassert forall i :: i in o.items ==> i.id < st.next_line_item_id;\nassert item !in o.items;\nSumBy_LineItem_line_totalAdd(o.items, item);\norder := o.(items := o.items + {item}, subtotal := o.subtotal + item.line_total, total := o.subtotal + item.line_total + o.tax);\nst.orders := st.orders[order_id := order];\nst.next_line_item_id := st.next_line_item_id + 1;\nst.inventory := st.inventory[sku := st.inventory[sku].(available := st.inventory[sku].available - quantity)];",
   "body" : "var o := st.orders[order_id];\nvar product := st.products[sku];\nvar item := LineItem(st.next_line_item_id, order_id, sku, quantity, product.price, product.price * quantity);\nassert item.line_total > 0;\nassert forall i :: i in o.items ==> i.id < st.next_line_item_id;\nassert item !in o.items;\nSumBy_LineItem_line_totalAdd(o.items, item);\norder := o.(items := o.items + {item}, subtotal := o.subtotal + item.line_total, total := o.subtotal + item.line_total + o.tax);\nst.orders := st.orders[order_id := order];\nst.next_line_item_id := st.next_line_item_id + 1;\nst.inventory := st.inventory[sku := st.inventory[sku].(available := st.inventory[sku].available - quantity)];",
   "usage" : {
     "inputTokens" : 0,
diff --git a/fixtures/synth-cache/verified/70/70ac30228e87ef92c27a443ebec4a8b31b7036db80bdcdb955a0efd9acb5d061.json b/fixtures/synth-cache/verified/70/70ac30228e87ef92c27a443ebec4a8b31b7036db80bdcdb955a0efd9acb5d061.json
index 3010c5bc..d644109c 100644
--- a/fixtures/synth-cache/verified/70/70ac30228e87ef92c27a443ebec4a8b31b7036db80bdcdb955a0efd9acb5d061.json
+++ b/fixtures/synth-cache/verified/70/70ac30228e87ef92c27a443ebec4a8b31b7036db80bdcdb955a0efd9acb5d061.json
@@ -1,5 +1,5 @@
 {
-  "candidate" : "var o := st.orders[order_id];\nvar t := now();\norder := o.(status := CANCELLED);\nif o.status == PAID {\n  var pid := st.next_payment_id;\n  var payment := Payment(pid, order_id, o.total, REFUNDED, t);\n  assert pid !in st.payments;\n  assert pid > 0;\n  assert |o.items| > 0;\n  assert o.total > 0;\n  st.orders := st.orders[order_id := order];\n  st.payments := st.payments[pid := payment];\n  st.next_payment_id := pid + 1;\n  assert forall pk :: pk in old(st.payments) ==> pk in st.payments && st.payments[pk] == old(st.payments)[pk];\n  assert payment.id in st.payments && st.payments[payment.id].order_id == order_id && st.payments[payment.id].status == REFUNDED;\n} else {\n  assert forall pid :: pid in st.payments && st.payments[pid].order_id == order_id ==> st.payments[pid].status != CAPTURED;\n  st.orders := st.orders[order_id := order];\n}\n",
+  "candidate" : "var o := st.orders[order_id];\nvar t := now();\norder := o.(status := CANCELLED);\nif o.status == PAID {\n  var pid := st.next_payment_id;\n  var payment := Payment(pid, order_id, o.total, REFUNDED, t);\n  assert pid !in st.payments;\n  assert pid > 0;\n  assert |o.items| > 0;\n  assert o.total > 0;\n  st.orders := st.orders[order_id := order];\n  st.payments := st.payments[pid := payment];\n  st.next_payment_id := pid + 1;\n  assert forall pk :: pk in old(st.payments) ==> pk in st.payments && st.payments[pk] == old(st.payments)[pk];\n  assert payment.id in st.payments && st.payments[payment.id].order_id == order_id && st.payments[payment.id].status == REFUNDED;\n} else {\n  assert forall pid :: pid in st.payments && st.payments[pid].order_id == order_id ==> st.payments[pid].status != CAPTURED;\n  st.orders := st.orders[order_id := order];\n}",
   "body" : "var o := st.orders[order_id];\nvar t := now();\norder := o.(status := CANCELLED);\nif o.status == PAID {\n  var pid := st.next_payment_id;\n  var payment := Payment(pid, order_id, o.total, REFUNDED, t);\n  assert pid !in st.payments;\n  assert pid > 0;\n  assert |o.items| > 0;\n  assert o.total > 0;\n  st.orders := st.orders[order_id := order];\n  st.payments := st.payments[pid := payment];\n  st.next_payment_id := pid + 1;\n  assert forall pk :: pk in old(st.payments) ==> pk in st.payments && st.payments[pk] == old(st.payments)[pk];\n  assert payment.id in st.payments && st.payments[payment.id].order_id == order_id && st.payments[payment.id].status == REFUNDED;\n} else {\n  assert forall pid :: pid in st.payments && st.payments[pid].order_id == order_id ==> st.payments[pid].status != CAPTURED;\n  st.orders := st.orders[order_id := order];\n}",
   "usage" : {
     "inputTokens" : 0,
diff --git a/fixtures/synth-cache/verified/7c/7c52059857bb2897828f8c2f91017ce51b2943a7f3225ae75e0441d53f1cb832.json b/fixtures/synth-cache/verified/7c/7c52059857bb2897828f8c2f91017ce51b2943a7f3225ae75e0441d53f1cb832.json
new file mode 100644
index 00000000..2daa4706
--- /dev/null
+++ b/fixtures/synth-cache/verified/7c/7c52059857bb2897828f8c2f91017ce51b2943a7f3225ae75e0441d53f1cb832.json
@@ -0,0 +1,11 @@
+{
+  "candidate" : "var o := st.orders[order_id];\nvar removed :| removed in o.items && removed.id == item_id;\nassert forall i1, i2 :: i1 in o.items && i2 in o.items && i1.id == i2.id ==> i1 == i2;\nassert LineItemInv(removed);\nassert removed.product_sku in st.inventory;\nghost var rest := o.items - {removed};\nassert o.subtotal == SumBy_LineItem_line_total(o.items);\nSumBy_LineItem_line_totalRemove(o.items, removed);\nSumBy_LineItem_line_totalNonNeg(rest);\nif rest != {} {\n  ghost var w :| w in rest;\n  SumBy_LineItem_line_totalEq(rest, w);\n  SumBy_LineItem_line_totalNonNeg(rest - {w});\n  assert SumBy_LineItem_line_total(rest) > 0;\n}\norder := o.(items := o.items - {removed}, subtotal := o.subtotal - removed.line_total, total := o.subtotal - removed.line_total + o.tax);\nst.orders := st.orders[order_id := order];\nst.inventory := st.inventory[removed.product_sku := st.inventory[removed.product_sku].(available := st.inventory[removed.product_sku].available + removed.quantity)];\nassert st.payments == old(st.payments);\nassert forall oid :: oid in st.orders && oid != order_id ==> st.orders[oid] == old(st.orders)[oid];\nassert st.orders[order_id].status == old(st.orders)[order_id].status;\n",
+  "body" : "var o := st.orders[order_id];\nvar removed :| removed in o.items && removed.id == item_id;\nassert forall i1, i2 :: i1 in o.items && i2 in o.items && i1.id == i2.id ==> i1 == i2;\nassert LineItemInv(removed);\nassert removed.product_sku in st.inventory;\nghost var rest := o.items - {removed};\nassert o.subtotal == SumBy_LineItem_line_total(o.items);\nSumBy_LineItem_line_totalRemove(o.items, removed);\nSumBy_LineItem_line_totalNonNeg(rest);\nif rest != {} {\n  ghost var w :| w in rest;\n  SumBy_LineItem_line_totalEq(rest, w);\n  SumBy_LineItem_line_totalNonNeg(rest - {w});\n  assert SumBy_LineItem_line_total(rest) > 0;\n}\norder := o.(items := o.items - {removed}, subtotal := o.subtotal - removed.line_total, total := o.subtotal - removed.line_total + o.tax);\nst.orders := st.orders[order_id := order];\nst.inventory := st.inventory[removed.product_sku := st.inventory[removed.product_sku].(available := st.inventory[removed.product_sku].available + removed.quantity)];\nassert st.payments == old(st.payments);\nassert forall oid :: oid in st.orders && oid != order_id ==> st.orders[oid] == old(st.orders)[oid];\nassert st.orders[order_id].status == old(st.orders)[order_id].status;",
+  "usage" : {
+    "inputTokens" : 0,
+    "outputTokens" : 0
+  },
+  "model" : "claude-fable-5",
+  "promptVersion" : "v2",
+  "outcome" : "verified"
+}
diff --git a/fixtures/synth-cache/verified/a8/a8b9e2efce4e095d63116798f21dfd94deefc688502dbecbd3e82becad10dbcd.json b/fixtures/synth-cache/verified/a8/a8b9e2efce4e095d63116798f21dfd94deefc688502dbecbd3e82becad10dbcd.json
index 057958c8..ef66c8b2 100644
--- a/fixtures/synth-cache/verified/a8/a8b9e2efce4e095d63116798f21dfd94deefc688502dbecbd3e82becad10dbcd.json
+++ b/fixtures/synth-cache/verified/a8/a8b9e2efce4e095d63116798f21dfd94deefc688502dbecbd3e82becad10dbcd.json
@@ -1,5 +1,5 @@
 {
-  "candidate" : "order := st.orders[order_id].(status := DELIVERED, delivered_at := Some(now()));\nassert exists pid :: pid in st.payments && st.payments[pid].order_id == order_id && st.payments[pid].status == CAPTURED;\nst.orders := st.orders[order_id := order];\n",
+  "candidate" : "order := st.orders[order_id].(status := DELIVERED, delivered_at := Some(now()));\nassert exists pid :: pid in st.payments && st.payments[pid].order_id == order_id && st.payments[pid].status == CAPTURED;\nst.orders := st.orders[order_id := order];",
   "body" : "order := st.orders[order_id].(status := DELIVERED, delivered_at := Some(now()));\nassert exists pid :: pid in st.payments && st.payments[pid].order_id == order_id && st.payments[pid].status == CAPTURED;\nst.orders := st.orders[order_id := order];",
   "usage" : {
     "inputTokens" : 0,
diff --git a/fixtures/synth-cache/verified/ad/add73cce0e09598e3d50705d5f034086ce6ceb1882e6f57361125f64f3b07c6b.json b/fixtures/synth-cache/verified/ad/add73cce0e09598e3d50705d5f034086ce6ceb1882e6f57361125f64f3b07c6b.json
index 355f63b2..93d03026 100644
--- a/fixtures/synth-cache/verified/ad/add73cce0e09598e3d50705d5f034086ce6ceb1882e6f57361125f64f3b07c6b.json
+++ b/fixtures/synth-cache/verified/ad/add73cce0e09598e3d50705d5f034086ce6ceb1882e6f57361125f64f3b07c6b.json
@@ -1,5 +1,5 @@
 {
-  "candidate" : "var t := now();\norder := st.orders[order_id].(status := SHIPPED, shipped_at := Some(t));\nassert exists pid :: pid in st.payments && st.payments[pid].order_id == order_id && st.payments[pid].status == CAPTURED;\nst.orders := st.orders[order_id := order];\n",
+  "candidate" : "var t := now();\norder := st.orders[order_id].(status := SHIPPED, shipped_at := Some(t));\nassert exists pid :: pid in st.payments && st.payments[pid].order_id == order_id && st.payments[pid].status == CAPTURED;\nst.orders := st.orders[order_id := order];",
   "body" : "var t := now();\norder := st.orders[order_id].(status := SHIPPED, shipped_at := Some(t));\nassert exists pid :: pid in st.payments && st.payments[pid].order_id == order_id && st.payments[pid].status == CAPTURED;\nst.orders := st.orders[order_id := order];",
   "usage" : {
     "inputTokens" : 0,
diff --git a/fixtures/synth-cache/verified/b9/b9a7663a96a244a0f2dd9d819d9c3c8f0780be2e3bf2c10a6f5b6d355add42f7.json b/fixtures/synth-cache/verified/b9/b9a7663a96a244a0f2dd9d819d9c3c8f0780be2e3bf2c10a6f5b6d355add42f7.json
index 66cfc0ae..a9787ca0 100644
--- a/fixtures/synth-cache/verified/b9/b9a7663a96a244a0f2dd9d819d9c3c8f0780be2e3bf2c10a6f5b6d355add42f7.json
+++ b/fixtures/synth-cache/verified/b9/b9a7663a96a244a0f2dd9d819d9c3c8f0780be2e3bf2c10a6f5b6d355add42f7.json
@@ -1,5 +1,5 @@
 {
-  "candidate" : "results := [];\nvar remaining := st.orders.Keys;\nwhile remaining != {}\n  invariant remaining <= st.orders.Keys\n  invariant forall o :: (o in results) ==> (((o in st.orders.Values && (customer_id == None || o.customer_id == customer_id.value)) && (status_filter == None || o.status == status_filter.value)))\n  decreases |remaining|\n{\n  var k :| k in remaining;\n  var o := st.orders[k];\n  if (customer_id == None || o.customer_id == customer_id.value) && (status_filter == None || o.status == status_filter.value) {\n    results := results + [o];\n  }\n  remaining := remaining - {k};\n}\n",
+  "candidate" : "results := [];\nvar remaining := st.orders.Keys;\nwhile remaining != {}\n  invariant remaining <= st.orders.Keys\n  invariant forall o :: (o in results) ==> (((o in st.orders.Values && (customer_id == None || o.customer_id == customer_id.value)) && (status_filter == None || o.status == status_filter.value)))\n  decreases |remaining|\n{\n  var k :| k in remaining;\n  var o := st.orders[k];\n  if (customer_id == None || o.customer_id == customer_id.value) && (status_filter == None || o.status == status_filter.value) {\n    results := results + [o];\n  }\n  remaining := remaining - {k};\n}",
   "body" : "results := [];\nvar remaining := st.orders.Keys;\nwhile remaining != {}\n  invariant remaining <= st.orders.Keys\n  invariant forall o :: (o in results) ==> (((o in st.orders.Values && (customer_id == None || o.customer_id == customer_id.value)) && (status_filter == None || o.status == status_filter.value)))\n  decreases |remaining|\n{\n  var k :| k in remaining;\n  var o := st.orders[k];\n  if (customer_id == None || o.customer_id == customer_id.value) && (status_filter == None || o.status == status_filter.value) {\n    results := results + [o];\n  }\n  remaining := remaining - {k};\n}",
   "usage" : {
     "inputTokens" : 0,
diff --git a/fixtures/synth-cache/verified/b9/b9a8d926a22236d798be362de2a18d7fbe6c1bff64950b96bddf9b717d7a3b6c.json b/fixtures/synth-cache/verified/b9/b9a8d926a22236d798be362de2a18d7fbe6c1bff64950b96bddf9b717d7a3b6c.json
index e9e65485..1af865c4 100644
--- a/fixtures/synth-cache/verified/b9/b9a8d926a22236d798be362de2a18d7fbe6c1bff64950b96bddf9b717d7a3b6c.json
+++ b/fixtures/synth-cache/verified/b9/b9a8d926a22236d798be362de2a18d7fbe6c1bff64950b96bddf9b717d7a3b6c.json
@@ -1,5 +1,5 @@
 {
-  "candidate" : "var o := st.orders[order_id];\nvar t := now();\norder := o.(status := RETURNED);\nst.orders := st.orders[order_id := order];\nvar pid := st.next_payment_id;\nvar payment := Payment(pid, order_id, o.total, REFUNDED, t);\nst.payments := st.payments[pid := payment];\nassert forall pk :: pk in old(st.payments) ==> pk in st.payments && st.payments[pk] == old(st.payments)[pk];\nst.next_payment_id := pid + 1;\n",
+  "candidate" : "var o := st.orders[order_id];\nvar t := now();\norder := o.(status := RETURNED);\nst.orders := st.orders[order_id := order];\nvar pid := st.next_payment_id;\nvar payment := Payment(pid, order_id, o.total, REFUNDED, t);\nst.payments := st.payments[pid := payment];\nassert forall pk :: pk in old(st.payments) ==> pk in st.payments && st.payments[pk] == old(st.payments)[pk];\nst.next_payment_id := pid + 1;",
   "body" : "var o := st.orders[order_id];\nvar t := now();\norder := o.(status := RETURNED);\nst.orders := st.orders[order_id := order];\nvar pid := st.next_payment_id;\nvar payment := Payment(pid, order_id, o.total, REFUNDED, t);\nst.payments := st.payments[pid := payment];\nassert forall pk :: pk in old(st.payments) ==> pk in st.payments && st.payments[pk] == old(st.payments)[pk];\nst.next_payment_id := pid + 1;",
   "usage" : {
     "inputTokens" : 0,
diff --git a/fixtures/synth-cache/verified/ca/ca6e89bbec3a27bb3bb414146963f14975ef7d3a08e7846b83a1c59e87f9372a.json b/fixtures/synth-cache/verified/ca/ca6e89bbec3a27bb3bb414146963f14975ef7d3a08e7846b83a1c59e87f9372a.json
index c141597d..4ab4b520 100644
--- a/fixtures/synth-cache/verified/ca/ca6e89bbec3a27bb3bb414146963f14975ef7d3a08e7846b83a1c59e87f9372a.json
+++ b/fixtures/synth-cache/verified/ca/ca6e89bbec3a27bb3bb414146963f14975ef7d3a08e7846b83a1c59e87f9372a.json
@@ -1,5 +1,5 @@
 {
-  "candidate" : "var oid := st.next_order_id;\norder := Order(oid, customer_id, DRAFT, {}, 0, 0, 0, 0, 0, None, None);\nassert oid !in st.orders;\nassert forall pid :: pid in st.payments ==> st.payments[pid].order_id != oid;\nst.orders := st.orders[oid := order];\nst.next_order_id := oid + 1;\n",
+  "candidate" : "var oid := st.next_order_id;\norder := Order(oid, customer_id, DRAFT, {}, 0, 0, 0, 0, 0, None, None);\nassert oid !in st.orders;\nassert forall pid :: pid in st.payments ==> st.payments[pid].order_id != oid;\nst.orders := st.orders[oid := order];\nst.next_order_id := oid + 1;",
   "body" : "var oid := st.next_order_id;\norder := Order(oid, customer_id, DRAFT, {}, 0, 0, 0, 0, 0, None, None);\nassert oid !in st.orders;\nassert forall pid :: pid in st.payments ==> st.payments[pid].order_id != oid;\nst.orders := st.orders[oid := order];\nst.next_order_id := oid + 1;",
   "usage" : {
     "inputTokens" : 0,
diff --git a/fixtures/synth-cache/verified/e5/e578e20459dc30b5b6c83acd963baedae4c2acd4701381fb7da9d6863d3c60fb.json b/fixtures/synth-cache/verified/e5/e578e20459dc30b5b6c83acd963baedae4c2acd4701381fb7da9d6863d3c60fb.json
index 42d0b9e9..f72ca9bc 100644
--- a/fixtures/synth-cache/verified/e5/e578e20459dc30b5b6c83acd963baedae4c2acd4701381fb7da9d6863d3c60fb.json
+++ b/fixtures/synth-cache/verified/e5/e578e20459dc30b5b6c83acd963baedae4c2acd4701381fb7da9d6863d3c60fb.json
@@ -1,5 +1,5 @@
 {
-  "candidate" : "order := st.orders[order_id].(status := PLACED);\nassert forall pid :: pid in st.payments && st.payments[pid].order_id == order_id ==> st.payments[pid].status != CAPTURED;\nst.orders := st.orders[order_id := order];\n",
+  "candidate" : "order := st.orders[order_id].(status := PLACED);\nassert forall pid :: pid in st.payments && st.payments[pid].order_id == order_id ==> st.payments[pid].status != CAPTURED;\nst.orders := st.orders[order_id := order];",
   "body" : "order := st.orders[order_id].(status := PLACED);\nassert forall pid :: pid in st.payments && st.payments[pid].order_id == order_id ==> st.payments[pid].status != CAPTURED;\nst.orders := st.orders[order_id := order];",
   "usage" : {
     "inputTokens" : 0,
diff --git a/fixtures/synth-cache/verified/fa/fa1ed670c375e93a946e64357e882ed2b4d50695699b31fc6a0e8d67a7531ede.json b/fixtures/synth-cache/verified/fa/fa1ed670c375e93a946e64357e882ed2b4d50695699b31fc6a0e8d67a7531ede.json
index 7d96d637..4b84dc9e 100644
--- a/fixtures/synth-cache/verified/fa/fa1ed670c375e93a946e64357e882ed2b4d50695699b31fc6a0e8d67a7531ede.json
+++ b/fixtures/synth-cache/verified/fa/fa1ed670c375e93a946e64357e882ed2b4d50695699b31fc6a0e8d67a7531ede.json
@@ -1,5 +1,5 @@
 {
-  "candidate" : "var pid := st.next_payment_id;\npayment := Payment(pid, order_id, amount, CAPTURED, now());\nassert pid !in st.payments;\nassert pid > 0;\nassert |st.orders[order_id].items| > 0;\nassert amount > 0;\nvar ord := st.orders[order_id].(status := PAID);\nst.orders := st.orders[order_id := ord];\nst.payments := st.payments[pid := payment];\nst.next_payment_id := pid + 1;\nassert forall p :: p in old(st.payments) ==> p in st.payments && st.payments[p] == old(st.payments)[p];\nassert payment.id in st.payments && st.payments[payment.id].order_id == order_id && st.payments[payment.id].status == CAPTURED;\nassert forall oid :: oid in st.orders && oid != order_id ==> payment.order_id != oid;\n",
+  "candidate" : "var pid := st.next_payment_id;\npayment := Payment(pid, order_id, amount, CAPTURED, now());\nassert pid !in st.payments;\nassert pid > 0;\nassert |st.orders[order_id].items| > 0;\nassert amount > 0;\nvar ord := st.orders[order_id].(status := PAID);\nst.orders := st.orders[order_id := ord];\nst.payments := st.payments[pid := payment];\nst.next_payment_id := pid + 1;\nassert forall p :: p in old(st.payments) ==> p in st.payments && st.payments[p] == old(st.payments)[p];\nassert payment.id in st.payments && st.payments[payment.id].order_id == order_id && st.payments[payment.id].status == CAPTURED;\nassert forall oid :: oid in st.orders && oid != order_id ==> payment.order_id != oid;",
   "body" : "var pid := st.next_payment_id;\npayment := Payment(pid, order_id, amount, CAPTURED, now());\nassert pid !in st.payments;\nassert pid > 0;\nassert |st.orders[order_id].items| > 0;\nassert amount > 0;\nvar ord := st.orders[order_id].(status := PAID);\nst.orders := st.orders[order_id := ord];\nst.payments := st.payments[pid := payment];\nst.next_payment_id := pid + 1;\nassert forall p :: p in old(st.payments) ==> p in st.payments && st.payments[p] == old(st.payments)[p];\nassert payment.id in st.payments && st.payments[payment.id].order_id == order_id && st.payments[payment.id].status == CAPTURED;\nassert forall oid :: oid in st.orders && oid != order_id ==> payment.order_id != oid;",
   "usage" : {
     "inputTokens" : 0,
diff --git a/modules/dafny/src/main/scala/specrest/dafny/Generator.scala b/modules/dafny/src/main/scala/specrest/dafny/Generator.scala
index fce75cbd..2917271c 100644
--- a/modules/dafny/src/main/scala/specrest/dafny/Generator.scala
+++ b/modules/dafny/src/main/scala/specrest/dafny/Generator.scala
@@ -101,11 +101,19 @@ object Generator:
         case RelationTypeF(_, _, to, _) => namedType(to)
         case _                          => None
       val stateEntityNames = stateFields.values.flatMap(stateValueEntity).toSet
+      // Sum invariants reach the state predicate through the value entity
+      // itself or through any chain of entity-set fields below it, matching
+      // the nested lifting in renderEntities.
+      val ghostReach = closeOverEntitySets(
+        ir,
+        svcEntities(ir)
+          .filter(e => entInvariants(e).exists(containsSumCall))
+          .map(entName)
+          .toSet
+      )
       val anyGhostInv =
         svcInvariants(ir).exists(inv => containsSumCall(invBody(inv))) ||
-          svcEntities(ir).exists(e =>
-            stateEntityNames.contains(entName(e)) && entInvariants(e).exists(containsSumCall)
-          )
+          stateEntityNames.exists(ghostReach)
       val ctx = Ctx(
         ir = ir,
         stateFields = stateFields,
@@ -122,6 +130,7 @@ object Generator:
       sb ++= header(svcName(ir))
       sb ++= optionDatatype()
       sb ++= theByFunction()
+      sb ++= theBySetFunction()
       sb ++= sumFunctions(sumSpecs)
 
       val enumDecls   = renderEnums(svcEnums(ir))
@@ -202,6 +211,18 @@ object Generator:
       "  var k :| k in m && p(k); k\n" +
       "}\n"
 
+  // Set-domain twin of TheBy for `the x in s | P(x)` where s is a set value
+  // (an entity's collection field) rather than a state map: the witness is
+  // the element itself, under the same existence + uniqueness preconditions.
+  private def theBySetFunction(): String =
+    "\nghost function TheBySet<T>(s: set<T>, p: T -> bool): T\n" +
+      "  requires exists x :: x in s && p(x)\n" +
+      "  requires forall x1, x2 :: x1 in s && x2 in s && p(x1) && p(x2) ==> x1 == x2\n" +
+      "  ensures TheBySet(s, p) in s && p(TheBySet(s, p))\n" +
+      "{\n" +
+      "  var x :| x in s && p(x); x\n" +
+      "}\n"
+
   private def renderEnums(decls: List[enum_decl])(using DafnyLabel): String =
     val parts = decls.map { d =>
       val ctors = enmVariants(d).mkString(" | ")
@@ -232,6 +253,24 @@ object Generator:
       case _                                  => false
     }
 
+  // Entities whose predicate is transitively nonempty: seeded by entities
+  // with clauses of their own, closed over entity-set fields, since a nested
+  // element's predicate lifts into its owner's.
+  private def closeOverEntitySets(ir: ServiceIRFull, seed: Set[String]): Set[String] =
+    val elemsOf: Map[String, List[String]] =
+      svcEntities(ir).map { e =>
+        entName(e) -> entFields(e).flatMap(f =>
+          fldType(f) match
+            case SetTypeF(NamedTypeF(n, _), _) => Some(n)
+            case _                             => None
+        )
+      }.toMap
+    @annotation.tailrec
+    def loop(s: Set[String]): Set[String] =
+      val next = s ++ elemsOf.collect { case (owner, elems) if elems.exists(s) => owner }
+      if next.sizeIs == s.size then s else loop(next)
+    loop(seed)
+
   private def renderEntities(
       ctx: Ctx,
       decls: List[entity_decl]
@@ -239,14 +278,10 @@ object Generator:
     val sb           = new StringBuilder
     val withInv      = Set.newBuilder[String]
     val withGhostInv = Set.newBuilder[String]
-    decls.foreach: d =>
+    val baseClauses = decls.map { d =>
       val name       = entName(d)
       val fields     = entFields(d)
       val invariants = entInvariants(d)
-      val ctorFields = fields.map { f =>
-        s"${fldName(f)}: ${renderType(ctx, fldType(f))}"
-      }
-      sb ++= s"datatype $name = $name(${ctorFields.mkString(", ")})\n"
 
       val fieldWhereClauses = fields.flatMap { f =>
         fldDefault(f).map { whereExpr =>
@@ -271,16 +306,49 @@ object Generator:
       val ghostClauses =
         ghostInvariants.map(e => s"(${renderEntityInvariant(invCtx, e, name)})")
 
-      val allClauses = (fieldWhereClauses ++ aliasFieldClauses ++ invClauses).distinct
+      (d, (fieldWhereClauses ++ aliasFieldClauses ++ invClauses).distinct, ghostClauses)
+    }
+    val invEntityNames = closeOverEntitySets(
+      ctx.ir,
+      baseClauses.collect { case (d, all, _) if all.nonEmpty => entName(d) }.toSet
+    )
+    val ghostEntityNames = closeOverEntitySets(
+      ctx.ir,
+      baseClauses.collect { case (d, _, ghost) if ghost.nonEmpty => entName(d) }.toSet
+    )
+
+    baseClauses.foreach: (d, base, ghostClauses) =>
+      val name   = entName(d)
+      val fields = entFields(d)
+      val ctorFields = fields.map { f =>
+        s"${fldName(f)}: ${renderType(ctx, fldType(f))}"
+      }
+      sb ++= s"datatype $name = $name(${ctorFields.mkString(", ")})\n"
+
+      // An entity-set field's elements satisfy their own invariant (the
+      // runtime marshals every stored element through the same checks), so
+      // it lifts into the owner: the state predicate reaches nested items
+      // exactly as the typed Z3 encoding already assumes. The ghost side
+      // lifts the same way so nested sum constraints stay on the contracts.
+      def nestedSetClauses(members: Set[String], suffix: String): List[String] =
+        fields.flatMap { f =>
+          fldType(f) match
+            case SetTypeF(NamedTypeF(en, _), _) if members(en) =>
+              Some(s"(forall i :: i in x.${fldName(f)} ==> $en$suffix(i))")
+            case _ => None
+        }
+
+      val allClauses = base ++ nestedSetClauses(invEntityNames, "Inv")
       if allClauses.nonEmpty then
         withInv += name
         sb ++= s"\npredicate ${name}Inv(x: $name)\n{\n"
         sb ++= s"  ${allClauses.mkString("\n  && ")}\n"
         sb ++= "}\n"
-      if ghostClauses.nonEmpty then
+      val allGhostClauses = ghostClauses ++ nestedSetClauses(ghostEntityNames, "InvGhost")
+      if allGhostClauses.nonEmpty then
         withGhostInv += name
         sb ++= s"\nghost predicate ${name}InvGhost(x: $name)\n{\n"
-        sb ++= s"  ${ghostClauses.mkString("\n  && ")}\n"
+        sb ++= s"  ${allGhostClauses.mkString("\n  && ")}\n"
         sb ++= "}\n"
     (sb.toString, withInv.result(), withGhostInv.result())
 
@@ -684,6 +752,17 @@ object Generator:
           |{
           |  ${fn}Eq(s, x);
           |}
+          |
+          |lemma ${fn}NonNeg(s: set<$elem>)
+          |  requires forall x :: x in s ==> x.$fld >= 0
+          |  ensures $fn(s) >= 0
+          |  decreases |s|
+          |{
+          |  if s != {} {
+          |    var y :| y in s && $fn(s) == y.$fld + $fn(s - {y});
+          |    ${fn}NonNeg(s - {y});
+          |  }
+          |}
           |""".stripMargin
     }
     parts.mkString
@@ -848,20 +927,35 @@ object Generator:
       s"(set $v | $v in $domStr && $predStr :: $projection)"
     case TheF(v, dom, body, _) =>
       // `the v in dom | body` = the unique element satisfying body. Lowered to a
-      // call to the deterministic spec-level helper TheBy so the SAME witness is
-      // referenced across ensures + body within one proof obligation. Inlining
-      // `var x :| ...` instead would give Dafny a fresh witness each occurrence
-      // and CEGIS cannot converge. Uniqueness + existence are the helper's
-      // preconditions, discharged from spec invariants at the call site.
+      // call to the deterministic spec-level helper TheBy (or its set twin) so
+      // the SAME witness is referenced across ensures + body within one proof
+      // obligation. Inlining `var x :| ...` instead would give Dafny a fresh
+      // witness each occurrence and CEGIS cannot converge. Uniqueness +
+      // existence are the helper's preconditions, discharged from spec
+      // invariants at the call site.
       //
-      // The lambda body is guarded with `v in dom &&` because the body usually
-      // dereferences `dom[v]` (a partial operation); without the guard, Dafny
-      // rejects with "element might not be in domain" at every call site.
+      // The lambda body is guarded with `v in dom &&` because a map-domain
+      // body usually dereferences `dom[v]` (a partial operation); without the
+      // guard, Dafny rejects with "element might not be in domain" at every
+      // call site.
       val innerCtx = ctx.copy(boundVars = ctx.boundVars + v)
       val domStr   = renderExpr(ctx, dom)
       val bodyStr  = renderExpr(innerCtx, body)
-      val keyType  = theByKeyType(ctx, dom)
-      s"TheBy($domStr, ($v: $keyType) => $v in $domStr && $bodyStr)"
+      if isMapDomain(ctx, dom) then
+        val keyType = theByKeyType(ctx, dom)
+        s"TheBy($domStr, ($v: $keyType) => $v in $domStr && $bodyStr)"
+      else
+        exprType(ctx, dom) match
+          case Some(SetTypeF(elem, _)) =>
+            // No membership guard here: the set element is the value itself,
+            // and a domain expression like `old(m)[k].items` inside the
+            // lambda would re-read the map where the call site's guard
+            // cannot reach (lambda well-formedness is checked standalone).
+            s"TheBySet($domStr, ($v: ${renderType(ctx, elem)}) => $bodyStr)"
+          case _ =>
+            failDafny(
+              s"TheBy: unsupported domain — expected a map/relation state field or a set-typed expression, got ${dom.getClass.getSimpleName}"
+            )
     case WithF(base, fields, _) =>
       val parts = fields.map { fa =>
         s"${fasName(fa)} := ${renderExpr(ctx, fasValue(fa))}"
@@ -877,6 +971,31 @@ object Generator:
   private def isMapDomain(ctx: Ctx, dom: expr): Boolean =
     peelRelationRef(dom).exists(isMapStateField(ctx, _))
 
+  // The type of a domain expression, for the shapes a TheF domain can take:
+  // a named binding, a map/relation read, and an entity field access, through
+  // pre()/prime wrappers. Anything else stays None and the op fails loud.
+  private def exprType(ctx: Ctx, e: expr): Option[type_expr] = e match
+    case PreF(inner, _)   => exprType(ctx, inner)
+    case PrimeF(inner, _) => exprType(ctx, inner)
+    case IdentifierF(n, _) =>
+      ctx.stateFields.get(n).orElse(ctx.inputTypes.get(n)).orElse(ctx.outputTypes.get(n))
+    case IndexF(m, _, _) =>
+      exprType(ctx, m).flatMap {
+        case MapTypeF(_, v, _)          => Some(v)
+        case RelationTypeF(_, _, to, _) => Some(to)
+        case _                          => None
+      }
+    case FieldAccessF(base, f, _) =>
+      exprType(ctx, base).flatMap {
+        case NamedTypeF(en, _) =>
+          svcEntities(ctx.ir)
+            .find(d => entName(d) == en)
+            .flatMap(d => entFields(d).find(fd => fldName(fd) == f))
+            .map(fldType)
+        case _ => None
+      }
+    case _ => None
+
   // Extract the key type of the map/relation `dom` refers to, so the lambda passed
   // to TheBy is fully type-annotated (Dafny cannot infer the parameter type through
   // a generic call).
@@ -984,7 +1103,11 @@ object Generator:
       case IfF(c, _, _, _)      => walk(c)
       case SomeWrapF(x, _)      => walk(x)
       case LetF(_, value, _, _) => walk(value)
-      case _                    => ()
+      // The binder's own membership is implicit, but the domain expression
+      // may dereference a state map (`the i in pre(orders)[oid].items｜..`),
+      // and that read needs its guard like any other.
+      case TheF(_, dom, _, _) => walk(dom)
+      case _                  => ()
     walk(e)
     acc.toList
 
diff --git a/modules/testgen/src/test/scala/specrest/testgen/SkipRateProbeTest.scala b/modules/testgen/src/test/scala/specrest/testgen/SkipRateProbeTest.scala
index 766a6278..5d0c2192 100644
--- a/modules/testgen/src/test/scala/specrest/testgen/SkipRateProbeTest.scala
+++ b/modules/testgen/src/test/scala/specrest/testgen/SkipRateProbeTest.scala
@@ -83,7 +83,7 @@ class SkipRateProbeTest extends CatsEffectSuite:
     ),
     (
       "ecommerce",
-      83,
+      84,
       9,
       "next_order_id, next_payment_id and next_line_item_id are scalar-backed now, but the nine counter ensures only check when the ops route through the kernel; without one (as in this probe) they skip as before"
     ),