feat(dafny): definite descriptions over set domains put ecommerce fully on verified kernels#524
Merged
Merged
Conversation
Line-item ids had no per-order uniqueness invariant, so the item addressed by id (and the DELETE route itself) was ambiguous: lineItemIdsUnique now mirrors oneLineItemPerSku. The op also declares an order output, which the DELETE convention default of 204 would discard (FastAPI refuses to register such a route at all), so its success status overrides to 200. Z3 consistency grows 188 to 199 checks, all passing.
TheF now dispatches on its domain: map and relation state fields keep the TheBy lowering, and a set-typed expression (an entity's collection field) lowers to a TheBySet twin whose witness is the element itself. The set lambda carries no membership guard, since a domain like old(m)[k].items inside the lambda would re-read the map where the call site's guard cannot reach. TheF domains now contribute well-formedness guards (the read inside the i in pre(orders)[oid].items shape), nested entity-set fields lift their element invariants into the owner's predicate (stored line items had no quantity bound, so inventory non-negativity was unprovable), and the set sum helpers gain a NonNeg induction lemma (subtotal stays a Money after a removal only through the ghost sum equality).
The RemoveLineItem body picks the item by assign-such-that, discharges uniqueness from lineItemIdsUnique, applies the sum Remove and NonNeg lemmas for the subtotal obligations, and restores the removed quantity to inventory. The strengthened ServiceStateInv also invalidates the verified claim on every cached ecommerce body, so all ten ran through the accept gate again; none needed changes.
📝 WalkthroughWalkthroughAdds a ChangesTheBySet Set-Domain Support
Estimated code review effort: 3 (Moderate) | ~25 minutes Possibly related PRs
🚥 Pre-merge checks | ✅ 5✅ Passed checks (5 passed)
✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
![cubic-dev-ai[bot]](https://avatars.githubusercontent.com/in/1082092?s=60&v=4){kind=small}
There was a problem hiding this comment.
All reported issues were addressed across 18 files
Reply with feedback, questions, or to request a fix.
Re-trigger cubic
…bility The nested entity-set lift covered only the plain predicates, so a nested element's sum-based invariant would vanish from ServiceStateInvGhost, and an owner whose predicate exists only through nesting was never referenced by its own owner. Both sides now close transitively over entity-set fields through a shared reachability helper, the ghost lift mirrors the plain one, and the method-contract flag follows the same closure so the ghost predicate and its references cannot drift apart. Emitted output for every current fixture is byte-identical.
HardMax71
added a commit
that referenced
this pull request
Jul 9, 2026
…racle exactness riders (#525) Three hardening items left over from the last arcs, none changing behavior for the current fixture suite. ## L07: declared outputs dropped by a 204 The RemoveLineItem seam in #524 showed the failure class: an operation declaring outputs while its success status resolves to 204 No Content loses the payload, fatally on python (FastAPI refuses to register a 204 route with a response body) and silently on go and ts. The new lint pass resolves the effective status through the same convention functions the endpoint derivation uses (classification, method override, `resolveStatus`), warns naming the dropped outputs, and points at the `http_status_success` override. A lone Bool output stays exempt, since a success flag feeding 204-versus-404 semantics is the designed pattern. The lint module gains a dependency on convention for the classification, asserted in ArchitectureTest; all four fixture specs stay silent under the rule (RemoveLineItem now overrides to 200), and the docs' lint tables grow the L07 row. ## Generated python stays ruff-clean Ecommerce's scale pushed two generated lines past the 100-character limit: the admin reset endpoint's three-counter `values(...)` call and the seven-variant enum `Literal` alias, the only ruff findings in any generated app. Both emitters now wrap when the single-line form exceeds the limit and stay single-line otherwise, so the other specs' generated output is byte-identical. Verified by before/after generation diffs across all four specs, ruff and mypy strict on the results, and the ecommerce smoke suite (124 passing) against the wrapped app. ## Go conformance oracle compares integers exactly The deferred follow-up from #518's review: the generated go test client decoded JSON through float64, so integer comparisons lost exactness above 2^53 and adjacent ids could conflate. The client now decodes with `UseNumber`, equality and ordering take an exact int64 path when both sides are integral, and map-key lookups and set hashing canonicalize integral values through one string form so `json.Number`, int64, and integral float64 agree; fractional values keep the float64 fallback and the arithmetic helpers stay float64 by design. A standalone probe shows the old path conflating 9007199254740993 with its neighbor and the new helpers distinguishing them in equality, ordering, string form, and hashes. All four go conformance suites pass unchanged. ## Validation Each slice was validated in isolation (lint 40/40 with the end-to-end CLI warning surfaced on a trap spec, python before/after diffs plus conformance, go suites on all four specs plus the exactness probe), and the assembled branch passes the full sbt suite (12 modules, zero failures). <!-- This is an auto-generated description by cubic. --> --- ## Summary by cubic Adds L07 lint to catch operations that resolve to 204 No Content and would drop outputs. Also keeps generated Python ruff-clean and makes Go conformance tests compare integers exactly to avoid precision loss. - New Features - L07 warns when an operation with outputs resolves to 204; resolves status via conventions; single Bool output is exempt. Suggests setting <Op>.http_status_success = 200. - Bug Fixes - Python codegen: wrap long counter `values(...)` and wide enum `Literal[...]` aliases when lines exceed 100 chars; other specs remain byte-identical. - Go conformance runtime: decode JSON with UseNumber, compare integers exactly as int64, and canonicalize numeric keys/hashes; fractional numbers still use float64. - Docs: list L01–L07 in lint tables and fix the L07 table row formatting. <sup>Written for commit 1216daf. Summary will update on new commits.</sup> <a href="https://cubic.dev/pr/HardMax71/spec_to_rest/pull/525?utm_source=github" target="_blank" rel="noopener noreferrer" data-no-image-dialog="true"><picture><source media="(prefers-color-scheme: dark)" srcset="https://www.cubic.dev/buttons/review-in-cubic-dark.svg"><source media="(prefers-color-scheme: light)" srcset="https://www.cubic.dev/buttons/review-in-cubic-light.svg"><img alt="Review in cubic" src="https://www.cubic.dev/buttons/review-in-cubic-dark.svg"></picture></a> <!-- End of auto-generated description by cubic. --> <!-- This is an auto-generated comment: release notes by coderabbit.ai --> ## Summary by CodeRabbit * **New Features** * Added warning **L07** for operations that resolve to **`204 No Content`** while declaring outputs that can never be returned. * **Bug Fixes** * Improved numeric handling in generated test/runtime helpers for more consistent decoding, comparisons, hashing, and ordering. * **Documentation** * Updated docs and verification/structural lint coverage to include the new **L07** check. * **Improvements** * Enhanced generated code formatting (Python enum aliases and SQLAlchemy seed resets) to better respect line-length limits. <!-- end of auto-generated comment: release notes by coderabbit.ai -->
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
![https://www.cubic.dev/buttons/review-in-cubic-dark.svg"><source](https://www.cubic.dev/buttons/review-in-cubic-dark.svg"><source){kind=link}
![https://www.cubic.dev/buttons/review-in-cubic-light.svg"><img](https://www.cubic.dev/buttons/review-in-cubic-light.svg"><img){kind=link}
![https://www.cubic.dev/buttons/review-in-cubic-dark.svg"></picture></a](https://www.cubic.dev/buttons/review-in-cubic-dark.svg"></picture></a){kind=link}
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
RemoveLineItem was the one ecommerce operation still on the fail-loud stub: its ensures binds
the i in pre(orders)[order_id].items | i.id = item_id, a definite description over a set value, and the Dafny contract lowering only knew map and relation domains. This PR teaches it set domains and lands the verified body, so every ecommerce operation now runs on a verified kernel or the direct-emit path.Spec
The description was not actually well-defined: line items had sku uniqueness per order but no id uniqueness, so two items could share the id the DELETE route addresses. A
lineItemIdsUniqueinvariant (the id twin ofoneLineItemPerSku) closes that; Z3 consistency grows from 188 to 199 checks, all passing with no encoder work. The op also declares anorderoutput, which the DELETE convention default of 204 would discard; FastAPI goes further and refuses to register a 204 route with a response body at all, so the conventions block overrides the success status to 200, the same escape hatch AddLineItem uses for 201. Changing the convention default itself would flip DeleteTodo and every other DELETE-with-output across specs, so it stays.Lowering
TheFnow dispatches on its domain type. Map and relation state fields keep theTheByghost-function lowering unchanged. A set-typed expression lowers to aTheBySettwin whose witness is the element itself, with the same existence and uniqueness preconditions, and without the membership guard inside the lambda: a domain likeold(m)[k].itemsre-read there fails Dafny's standalone lambda well-formedness even when the call site is guarded. Three supporting gaps surfaced while proving the body and are fixed in the generator rather than the spec: TheF domains now contribute well-formedness guards (the map read inside the domain needsk in mhoisted before the let), nested entity-set fields lift their element entity's invariant into the owner's predicate (stored line items had noquantity > 0in the proof context, so inventory non-negativity was unprovable; the typed Z3 encoding already assumes exactly this), and the generated set-sum helpers gain aNonNeginduction lemma, since a subtotal staying non-negative after a removal only follows through the ghost sum equality.Body and cache
The RemoveLineItem body picks the witness by assign-such-that, discharges uniqueness from the new invariant, applies the sum
RemoveandNonNeglemmas for the subtotal and total obligations, and restores the removed quantity to inventory. StrengtheningServiceStateInvinvalidates the verified claim on every cached ecommerce body (their cache keys are header-derived and stay put, but the predicate they were proved against changed), so all ten ran through thesynth acceptgate again; none needed changes.Validation
Z3 verify 199/199. All three targets generated from the committed cache with zero stubs; the DELETE route resolves to 200 with the order payload on each (previously python crashed at FastAPI route registration and go/ts silently dropped the body on 204). Conformance: python 124 passed (four new tests cover the formerly stubbed op), go 23 passed, ts 23 passed, zero failures. End-to-end probe on every target: add a line item, DELETE it, response carries the updated order, inventory restores by the removed quantity, and a sibling order is untouched. mypy strict clean; full sbt suite green (12 modules). The dafny goldens change only by the unconditionally emitted
TheBySetfunction, and the ecommerce IR golden by the new invariant and status override.Summary by cubic
Adds definite descriptions over set domains with
TheBySetand lands a verified RemoveLineItem kernel; ecommerce now runs fully on verified kernels (or direct-emit). The spec adds per-order line-item id uniqueness and the DELETE route returns 200 with the updated order.New Features
TheBySet;TheFnow dispatches on map/relation/set domains and adds domain well-formedness guards.ServiceStateInvandServiceStateInvGhost, closed transitively over entity-set fields so ghost sum constraints stay on contracts.NonNeglemma.lineItemIdsUnique; override RemoveLineItem success status to 200.Migration
Written for commit 78b9918. Summary will update on new commits.
Summary by CodeRabbit
New Features
Bug Fixes
Documentation