From ef21f9f279ee39734dd5086c9fce077b903a7c29 Mon Sep 17 00:00:00 2001 From: HardMax71 Date: Thu, 9 Jul 2026 02:07:10 +0200 Subject: [PATCH 1/4] fix(testgen): go conformance oracle compares integers exactly The generated go test client decoded JSON through float64, so integer comparisons lost exactness above 2 to the 53rd 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 arithmetic helpers stay float64 by design. --- .../go/chi/tests/conf_client.go | 7 +- .../go/chi/tests/conf_runtime.go | 141 +++++++++++++----- 2 files changed, 106 insertions(+), 42 deletions(-) diff --git a/modules/testgen/src/main/resources/testgen-templates/go/chi/tests/conf_client.go b/modules/testgen/src/main/resources/testgen-templates/go/chi/tests/conf_client.go index 12fe4f74..b915e841 100644 --- a/modules/testgen/src/main/resources/testgen-templates/go/chi/tests/conf_client.go +++ b/modules/testgen/src/main/resources/testgen-templates/go/chi/tests/conf_client.go @@ -54,8 +54,13 @@ func (r clientResponse) JSON() any { if len(r.body) == 0 { return map[string]any{} } + // UseNumber delivers numbers as json.Number: plain Unmarshal rounds + // integers through float64, conflating adjacent values above 2^53 before + // the runtime's exact int64 comparisons ever see them. + dec := json.NewDecoder(bytes.NewReader(r.body)) + dec.UseNumber() var v any - if err := json.Unmarshal(r.body, &v); err != nil { + if err := dec.Decode(&v); err != nil { return map[string]any{} } return v diff --git a/modules/testgen/src/main/resources/testgen-templates/go/chi/tests/conf_runtime.go b/modules/testgen/src/main/resources/testgen-templates/go/chi/tests/conf_runtime.go index 3a93d54a..b17ec5cd 100644 --- a/modules/testgen/src/main/resources/testgen-templates/go/chi/tests/conf_runtime.go +++ b/modules/testgen/src/main/resources/testgen-templates/go/chi/tests/conf_runtime.go @@ -6,15 +6,20 @@ // the set/relation/arithmetic semantics Python gets from built-ins (`in`, `==` // on sets, `<`, `+`, `|`/`&`/`-`, powerset) are delegated here, operating over // `any` values decoded from /admin/state and response bodies -// (objects -> map[string]any, arrays -> []any, numbers -> float64). `_Set` is -// a named slice so equality is order-independent for sets and ordered for -// sequences, matching the TypeScript Set-vs-Array distinction. +// (objects -> map[string]any, arrays -> []any, numbers -> json.Number, the +// client decodes with UseNumber). Equality and ordering compare integral +// values exactly as int64, the widest integer the service side can hold (Go +// int64, sqlite INTEGER); fractional values compare as float64, and +// arithmetic stays float64. `_Set` is a named slice so equality is +// order-independent for sets and ordered for sequences, matching the +// TypeScript Set-vs-Array distinction. package tests import ( "crypto/sha256" "encoding/hex" + "encoding/json" "fmt" "math" "regexp" @@ -38,19 +43,65 @@ func _toF(x any) (float64, bool) { return float64(v), true case float64: return v, true + case json.Number: + if f, err := v.Float64(); err == nil { + return f, true + } + return 0, false default: return 0, false } } +// _toI reports x as an exact int64. json.Number and digit strings (JSON +// object keys of Int-keyed relations) parse directly, skipping the float64 +// round-trip that conflates neighbors above 2^53; integral floats convert +// when in int64 range. Integers past int64 cannot originate from the service +// side (Go ints and sqlite INTEGER are 64-bit), so callers fall back to +// float64 for whatever fails here. +func _toI(x any) (int64, bool) { + switch v := x.(type) { + case int: + return int64(v), true + case int32: + return int64(v), true + case int64: + return v, true + case json.Number: + i, err := strconv.ParseInt(v.String(), 10, 64) + return i, err == nil + case string: + i, err := strconv.ParseInt(v, 10, 64) + return i, err == nil + case float32: + return _floatToI(float64(v)) + case float64: + return _floatToI(v) + default: + return 0, false + } +} + +func _floatToI(f float64) (int64, bool) { + // 2^63 is exact in float64 and one past int64 max, hence the >=. NaN + // fails the Trunc self-equality; infinities fail the range checks. + if f != math.Trunc(f) || f < -(1<<63) || f >= 1<<63 { + return 0, false + } + return int64(f), true +} + +// Integral numbers share one canonical string regardless of representation +// (json.Number, int64, integral float64), so map-key lookups and hashes +// agree across decoded and computed values. func _str(x any) string { if s, ok := x.(string); ok { return s } + if i, ok := _toI(x); ok { + return strconv.FormatInt(i, 10) + } if f, ok := _toF(x); ok { - if f == float64(int64(f)) { - return fmt.Sprintf("%d", int64(f)) - } return fmt.Sprintf("%v", f) } return fmt.Sprintf("%v", x) @@ -139,25 +190,12 @@ func _eq(a, b any) bool { if a == nil || b == nil { return a == nil && b == nil } - if fa, oka := _toF(a); oka { - if fb, okb := _toF(b); okb { - return fa == fb - } - // JSON object keys stringify, so an Int-keyed relation iterates as - // digit strings while ids stay numbers; compare numerically when the - // string side parses as a number exactly. - if sb, okb := b.(string); okb { - if fb, err := strconv.ParseFloat(sb, 64); err == nil { - return fa == fb - } - } - return false + if _, oka := _toF(a); oka { + return _numEq(a, b) } - if sa, oka := a.(string); oka { - if fb, okb := _toF(b); okb { - if fa, err := strconv.ParseFloat(sa, 64); err == nil { - return fa == fb - } + if _, oka := a.(string); oka { + if _, okb := _toF(b); okb { + return _numEq(a, b) } } switch av := a.(type) { @@ -213,6 +251,23 @@ func _eq(a, b any) bool { } } +// Number-vs-number and number-vs-digit-string equality (JSON object keys +// stringify, so an Int-keyed relation iterates as digit strings while ids +// stay numbers). Integral pairs compare exactly as int64: json.Number keeps +// full precision past 2^53, where the float64 round-trip conflates adjacent +// integers. Fractional operands, and integers past int64 (which the service +// side cannot produce), fall back to float64. +func _numEq(a, b any) bool { + if ia, oka := _toI(a); oka { + if ib, okb := _toI(b); okb { + return ia == ib + } + } + fa, oka := _num(a) + fb, okb := _num(b) + return oka && okb && fa == fb +} + func _in(x, c any) bool { switch cv := c.(type) { case string: @@ -230,11 +285,9 @@ func _in(x, c any) bool { } } -// Digit strings from JSON object keys compare numerically against numbers, -// matching _eq's coercion (Int-keyed relations stringify their keys). The -// float64 domain is the ceiling of the whole comparison anyway: encoding/json -// decodes every number to float64 before these helpers ever see it, so a -// ParseInt path would imply precision the decoded values no longer carry. +// Float-context coercion for numbers and numeric strings (JSON object keys). +// Exact integral comparison goes through _toI first; this is the fallback +// for fractional values, where float64 is the spec's own numeric domain. func _num(x any) (float64, bool) { if f, ok := _toF(x); ok { return f, true @@ -275,6 +328,18 @@ func _setEq(a, b any) bool { } func _cmp(a, b any) (int, bool) { + if ia, oka := _toI(a); oka { + if ib, okb := _toI(b); okb { + switch { + case ia < ib: + return -1, true + case ia > ib: + return 1, true + default: + return 0, true + } + } + } if fa, oka := _num(a); oka { if fb, okb := _num(b); okb { switch { @@ -616,15 +681,9 @@ func _call(f any, args ...any) any { } func _abs(x any) any { - // JSON-decoded numbers come in as float64; spec ints survive as int64. - // Coerce to float64 and delegate to math.Abs, mirroring TS's Math.abs(Number(x)). - switch v := x.(type) { - case float64: - return math.Abs(v) - case int64: - return math.Abs(float64(v)) - case int: - return math.Abs(float64(v)) + // _toF folds json.Number in; mirrors TS's Math.abs(Number(x)). + if f, ok := _toF(x); ok { + return math.Abs(f) } return math.NaN() } @@ -636,8 +695,8 @@ func _now() any { } func _sha256Hex(s any) any { - // Coerce any value (numbers come from JSON as float64) to its canonical - // string form before hashing, mirroring Python's str(...) coercion. - sum := sha256.Sum256([]byte(fmt.Sprintf("%v", s))) + // _str canonicalizes numbers (json.Number "2", int64 2, and float64 2 + // all hash as "2") so decoded and computed values agree. + sum := sha256.Sum256([]byte(_str(s))) return hex.EncodeToString(sum[:]) } From f7c81c7cb2bb374d3424ce9f2b402cc3b29d1fea Mon Sep 17 00:00:00 2001 From: HardMax71 Date: Thu, 9 Jul 2026 02:09:24 +0200 Subject: [PATCH 2/4] fix(codegen): wrap generated python lines that exceed the ruff limit The admin reset endpoint's counter update and the enum Literal alias grew past 100 characters on ecommerce (three counters, seven variants), the only two ruff findings in any generated app. Both sites now wrap when the single-line form exceeds the limit and stay single-line otherwise, so the other specs' output is byte-identical. --- .../scala/specrest/codegen/python/AdminRouter.scala | 12 ++++++++++-- .../scala/specrest/codegen/python/EmitPython.scala | 9 +++++---- .../src/test/scala/specrest/codegen/EmitTest.scala | 10 ++++++++++ .../scala/specrest/testgen/AdminRouterTest.scala | 8 ++++++++ 4 files changed, 33 insertions(+), 6 deletions(-) diff --git a/modules/codegen/src/main/scala/specrest/codegen/python/AdminRouter.scala b/modules/codegen/src/main/scala/specrest/codegen/python/AdminRouter.scala index 8d42ea7a..1745a2e4 100644 --- a/modules/codegen/src/main/scala/specrest/codegen/python/AdminRouter.scala +++ b/modules/codegen/src/main/scala/specrest/codegen/python/AdminRouter.scala @@ -25,8 +25,16 @@ object AdminRouter: val seeds = ScalarState .fieldsWithSeeds(ir) .map((sf, seed) => s"${ScalarState.columnName(stfName(sf))}=$seed") - .mkString(", ") - s"\n await session.execute(sa_update(ServiceState).values($seeds))" + val single = + s" await session.execute(sa_update(ServiceState).values(${seeds.mkString(", ")}))" + val stmt = + if single.length <= 100 then single + else + (" await session.execute(" :: + " sa_update(ServiceState).values(" :: + seeds.map(s => s" $s,") ::: + List(" )", " )")).mkString("\n") + s"\n$stmt" else "" val deleteStatements = if entities.isEmpty && !hasScalars then " pass" diff --git a/modules/codegen/src/main/scala/specrest/codegen/python/EmitPython.scala b/modules/codegen/src/main/scala/specrest/codegen/python/EmitPython.scala index 3a3fa98c..3817beb0 100644 --- a/modules/codegen/src/main/scala/specrest/codegen/python/EmitPython.scala +++ b/modules/codegen/src/main/scala/specrest/codegen/python/EmitPython.scala @@ -476,10 +476,11 @@ object EmitPython: private def enumAliasDef(ir: ServiceIRFull, typeName: String): Option[String] = svcEnums(ir) .find(e => enumNameFull(e) == typeName) - .map(e => - enumAliasName(typeName) + " = " + - enumValuesFull(e).map(v => s"\"$v\"").mkString("Literal[", ", ", "]") - ) + .map: e => + val values = enumValuesFull(e).map(v => s"\"$v\"").mkString(", ") + val single = s"${enumAliasName(typeName)} = Literal[$values]" + if single.length <= 100 then single + else s"${enumAliasName(typeName)} = Literal[\n $values\n]" private def schemaInputField( f: ProfiledField, diff --git a/modules/codegen/src/test/scala/specrest/codegen/EmitTest.scala b/modules/codegen/src/test/scala/specrest/codegen/EmitTest.scala index b3113544..cf90c344 100644 --- a/modules/codegen/src/test/scala/specrest/codegen/EmitTest.scala +++ b/modules/codegen/src/test/scala/specrest/codegen/EmitTest.scala @@ -634,6 +634,16 @@ class EmitTest extends CatsEffectSuite: s"url_mapping schema should not import SecretStr; got:\n$schema" ) + test("wide enum Literal alias wraps under the ruff line limit"): + SpecFixtures.loadProfiled("ecommerce").map: profiled => + val files = Emit.emitProject(profiled).map(f => f.path -> f.content).toMap + val schema = files("app/schemas/order.py") + val wrapped = + """OrderStatusValue = Literal[ + | "DRAFT", "PLACED", "PAID", "SHIPPED", "DELIVERED", "CANCELLED", "RETURNED" + |]""".stripMargin + assert(schema.contains(wrapped), s"expected wrapped Literal alias; got:\n$schema") + test( "ci.yml renders GitHub Actions ${{ ... }} expressions literally (not Handlebars-substituted)" ): diff --git a/modules/testgen/src/test/scala/specrest/testgen/AdminRouterTest.scala b/modules/testgen/src/test/scala/specrest/testgen/AdminRouterTest.scala index 16daf4c9..8ee5d613 100644 --- a/modules/testgen/src/test/scala/specrest/testgen/AdminRouterTest.scala +++ b/modules/testgen/src/test/scala/specrest/testgen/AdminRouterTest.scala @@ -60,6 +60,14 @@ class AdminRouterTest extends CatsEffectSuite: assert(src.contains("\"count\": state_row.count"), s"src=$src") assert(src.contains("from app.models.service_state import ServiceState"), s"src=$src") + test("ecommerce: multi-counter reset wraps values() one seed per line under the ruff limit"): + loadProfiled("fixtures/spec/ecommerce.spec").map: profiled => + val src = AdminRouter.emit(profiled) + assert(src.contains("sa_update(ServiceState).values(\n"), s"src=$src") + assert(src.contains(" next_order_id=1,"), s"src=$src") + val overlong = src.linesIterator.filter(_.length > 100).toList + assert(overlong.isEmpty, s"overlong lines: ${overlong.mkString("\n")}") + test("entity model imports use snake_case file names matching codegen"): loadProfiled("fixtures/spec/url_shortener.spec").map: profiled => val src = AdminRouter.emit(profiled) From 12bade1b4ccfc5a5abab8385d3df5657f411426d Mon Sep 17 00:00:00 2001 From: HardMax71 Date: Thu, 9 Jul 2026 02:11:31 +0200 Subject: [PATCH 3/4] feat(lint): warn when a 204 response drops declared outputs An operation whose outputs go beyond a single Bool flag while its success status resolves to 204 No Content loses its payload: FastAPI refuses to register the route and the go and ts targets silently drop the body, which is exactly how ecommerce RemoveLineItem failed before its override. L07 resolves the effective status through the same convention functions the endpoint derivation uses and points at the http_status_success fix. A lone Bool output stays exempt as the designed 204-versus-404 selector, and the lint module now depends on convention for the classification. --- build.sbt | 2 +- docs/content/docs/design/architecture.mdx | 4 +- .../developer-experience.md | 3 +- docs/content/docs/roadmap.mdx | 2 +- docs/content/docs/spec-language.mdx | 10 ++- .../specrest/arch/ArchitectureTest.scala | 8 ++- .../scala/specrest/lint/DroppedOutputs.scala | 49 +++++++++++++ .../src/main/scala/specrest/lint/Lint.scala | 3 +- .../specrest/lint/DroppedOutputsTest.scala | 72 +++++++++++++++++++ 9 files changed, 145 insertions(+), 8 deletions(-) create mode 100644 modules/lint/src/main/scala/specrest/lint/DroppedOutputs.scala create mode 100644 modules/lint/src/test/scala/specrest/lint/DroppedOutputsTest.scala diff --git a/build.sbt b/build.sbt index a2c04a43..6783ec4b 100644 --- a/build.sbt +++ b/build.sbt @@ -153,7 +153,7 @@ lazy val dafny = (project in file("modules/dafny")) lazy val lint = (project in file("modules/lint")) .settings(noTestWarts *) - .dependsOn(ir, parser % Test) + .dependsOn(ir, convention, parser % Test) .settings( name := "spec-lint", libraryDependencies ++= commonMainDeps ++ commonTestDeps diff --git a/docs/content/docs/design/architecture.mdx b/docs/content/docs/design/architecture.mdx index d96223b6..cad38bcb 100644 --- a/docs/content/docs/design/architecture.mdx +++ b/docs/content/docs/design/architecture.mdx @@ -66,7 +66,7 @@ flowchart LR The parser auto-injects a short preamble (`isValidURI`, `isValidEmail`). See [Parser Implementation Notes](/pipelines/parser-implementation). 2. IR build. CST becomes `ServiceIR`, a Scala 3 enum/case-class ADT, with span tracking. -3. Verify. `verify` runs structural lints (L01-L06; see +3. Verify. `verify` runs structural lints (L01-L07; see [structural lints](/spec-language#structural-lints)) and then translates each obligation to either Z3 SMT-LIB or Alloy (non-overlapping routing) and checks it. The translator's correctness is mechanically validated by the universal `translate_soundness_standalone` @@ -130,7 +130,7 @@ in [#391](https://github.com/HardMax71/spec_to_rest/issues/391). modules/ ├── ir/ # IR ADT (Isabelle-extracted SpecRestGenerated.scala), circe Serialize, PrettyPrint, VerifyError ├── parser/ # ANTLR4 grammar, Parse, Builder, Preamble injection -├── lint/ # Structural lints L01-L06 +├── lint/ # Structural lints L01-L07 ├── convention/ # M1-M10 classifier, naming, path, schema, validate, Builtins registry (single source of truth for spec-language builtin functions) ├── profile/ # Deployment profiles, type mapping, annotation ├── verify/ # Z3 + Alloy translators, backends, Consistency, Diagnostic, Narration diff --git a/docs/content/docs/research/spec_language_design/developer-experience.md b/docs/content/docs/research/spec_language_design/developer-experience.md index 67835ea2..be3aa51c 100644 --- a/docs/content/docs/research/spec_language_design/developer-experience.md +++ b/docs/content/docs/research/spec_language_design/developer-experience.md @@ -8,7 +8,7 @@ lints over the IR; `verify` hands the operation contracts to a solver. They catc ## Structural lints (`check`) -Once a parse succeeds, `check` runs six lints over the IR. Each carries a stable code. An error +Once a parse succeeds, `check` runs seven lints over the IR. Each carries a stable code. An error exits non-zero; a warning exits zero. | Code | Level | Catches | @@ -19,6 +19,7 @@ exits non-zero; a warning exits zero. | L04 | warning | two operations with the same input and output signature and equivalent `requires` | | L05 | warning | an entity declared but never referenced | | L06 | error | mutually recursive predicates or functions, which the verifier's inlining cannot unfold | +| L07 | warning | an operation whose outputs a resolved `204 No Content` success status would drop | The lints are deliberately narrow. L01 fires only on literals whose type admits no operator at all, so it catches obvious mistakes without standing in for a full type checker. diff --git a/docs/content/docs/roadmap.mdx b/docs/content/docs/roadmap.mdx index f32c5681..7660a37b 100644 --- a/docs/content/docs/roadmap.mdx +++ b/docs/content/docs/roadmap.mdx @@ -148,7 +148,7 @@ Per-feature ledger for the verifier. For the prose explanation of each entry, se | Machine-readable (`--json` / `--json-out`) diagnostics output | shipped | | Richer suggested-fix templates (op/invariant/field-aware; opt-out via `--no-suggestions`) | shipped | | Human-readable "why this fails" narration (opt-out via `--no-narration`) | shipped ([#89](https://github.com/HardMax71/spec_to_rest/issues/89)), covers `invariant_violation_by_operation`, `contradictory_invariants`, `unreachable_operation` | -| Structural spec lints (type mismatch, unused entity, ...) | shipped, `check` runs L01-L06 ([#81](https://github.com/HardMax71/spec_to_rest/issues/81)); L04 ships a syntactic over-approximation, SAT-based overlap is candidate verify-side work | +| Structural spec lints (type mismatch, unused entity, ...) | shipped, `check` runs L01-L07 ([#81](https://github.com/HardMax71/spec_to_rest/issues/81)); L04 ships a syntactic over-approximation, SAT-based overlap is candidate verify-side work | | Per-check VC dump (`--dump-vc `), Z3 SMT-LIB and Alloy `.als` artifacts | shipped | | Unsat-core extraction (`--explain`), surface contributing spec spans on `unsat` diagnostics | shipped (Z3 always; Alloy when `minisat.prover` is bundled) | | Native Alloy CLI cross-check job in CI | shipped | diff --git a/docs/content/docs/spec-language.mdx b/docs/content/docs/spec-language.mdx index d8f6f1da..a30f3573 100644 --- a/docs/content/docs/spec-language.mdx +++ b/docs/content/docs/spec-language.mdx @@ -180,7 +180,7 @@ directly into Python and SMT-LIB: `len`, `dom`, `ran`, `max`, `min`, `now`, `day ## Structural lints -`spec-to-rest check .spec` runs six solver-free structural lints over the IR after parsing +`spec-to-rest check .spec` runs seven solver-free structural lints over the IR after parsing succeeds. Each diagnostic carries a stable code; warnings allow exit `0`, errors cause exit `1`. | Code | Level | What it catches | @@ -191,6 +191,7 @@ succeeds. Each diagnostic carries a stable code; warnings allow exit `0`, errors | L04 | warning | Two operations share input/output signature **and** have equivalent `requires` | | L05 | warning | `entity` declared but never referenced in state, operations, invariants, or types | | L06 | error | Mutually-recursive predicates / functions; verifier inlining would diverge | +| L07 | warning | Operation declares outputs but its success status resolves to `204 No Content`, so they never reach the response | L01 is intentionally narrow: it only fires on literals whose class admits no operator overload (e.g., `flag and 5`, `count + true`, `count > true`). The DSL uses `+`/`-` for set/map union and @@ -205,6 +206,13 @@ caller picks the operation by name; ambiguity only matters at the dispatch layer overlap check on `requires_A and requires_B` is candidate work for `verify` and is tracked separately. +L07 resolves the success status the same way the convention engine does: a per-operation +`http_status_success` override wins, otherwise the default follows from the resolved HTTP method +and operation kind (DELETE and delete-like operations default to `204`). A single `Bool` output is +exempt because that is the designed delete pattern: the flag selects 204-versus-404 and never +becomes a response body. For anything else, set `.http_status_success = 200` in the +`conventions` block. + ## Test-generation coverage `spec-to-rest compile` (test emission is on by default; opt out with `--no-tests`) walks diff --git a/modules/arch/src/test/scala/specrest/arch/ArchitectureTest.scala b/modules/arch/src/test/scala/specrest/arch/ArchitectureTest.scala index 20cce9af..bbdf66df 100644 --- a/modules/arch/src/test/scala/specrest/arch/ArchitectureTest.scala +++ b/modules/arch/src/test/scala/specrest/arch/ArchitectureTest.scala @@ -35,7 +35,13 @@ class ArchitectureTest extends CatsEffectSuite: .layer("bench").definedBy("specrest.bench..") .layer("cli").definedBy("specrest.cli..") .whereLayer("parser").mayOnlyBeAccessedByLayers("bench", "cli") - .whereLayer("convention").mayOnlyBeAccessedByLayers("profile", "codegen", "testgen", "cli") + .whereLayer("convention").mayOnlyBeAccessedByLayers( + "profile", + "codegen", + "testgen", + "lint", + "cli" + ) .whereLayer("dafny").mayOnlyBeAccessedByLayers("synth", "cli") .whereLayer("profile").mayOnlyBeAccessedByLayers("codegen", "testgen", "cli") .whereLayer("verify").mayOnlyBeAccessedByLayers("bench", "cli") diff --git a/modules/lint/src/main/scala/specrest/lint/DroppedOutputs.scala b/modules/lint/src/main/scala/specrest/lint/DroppedOutputs.scala new file mode 100644 index 00000000..c615d615 --- /dev/null +++ b/modules/lint/src/main/scala/specrest/lint/DroppedOutputs.scala @@ -0,0 +1,49 @@ +package specrest.lint + +import specrest.convention.Classify +import specrest.convention.Path +import specrest.ir.generated.SpecRestGenerated.* + +object DroppedOutputs extends LintPass: + val code = "L07" + + def run(ir: service_ir): List[LintDiagnostic] = ir match + case full: ServiceIRFull => svcOperations(full).flatMap(check(_, full)) + + private def check(op: operation_decl, ir: ServiceIRFull): List[LintDiagnostic] = + val outputs = operOutputs(op) + if outputs.isEmpty || isSingleBoolFlag(outputs) then Nil + else + val classification = Classify.classifyOperation(op, ir) + val conv = svcConventions(ir) + val opName = classificationOperationName(classification) + val method = resolveMethod( + Path.getConvention(conv, opName, "http_method").flatMap(parseHttpMethod), + classificationMethod(classification) + ) + val status = resolveStatus( + Path.getConvention(conv, opName, "http_status_success"), + method, + classificationKind(classification) + ) + if status == "204" then + val dropped = outputs.map(p => s"'${prmName(p)}'").mkString(", ") + List( + LintDiagnostic( + code, + LintLevel.Warning, + s"operation '$opName' resolves to HTTP 204 No Content, so its declared outputs ($dropped) never reach the response; set '$opName.http_status_success = 200' in the conventions block", + operSpan(op) + ) + ) + else Nil + + // A lone Bool output on a 204 route is the designed delete pattern: the flag + // selects 204-vs-404 and is never a response body. + private def isSingleBoolFlag(outputs: List[param_decl]): Boolean = + outputs match + case p :: Nil => + prmType(p) match + case NamedTypeF("Bool", _) => true + case _ => false + case _ => false diff --git a/modules/lint/src/main/scala/specrest/lint/Lint.scala b/modules/lint/src/main/scala/specrest/lint/Lint.scala index d028f71c..6835e85f 100644 --- a/modules/lint/src/main/scala/specrest/lint/Lint.scala +++ b/modules/lint/src/main/scala/specrest/lint/Lint.scala @@ -9,7 +9,8 @@ object Lint: MissingEnsures, OperationOverlap, UnusedEntity, - CircularPredicate + CircularPredicate, + DroppedOutputs ) def run(ir: service_ir): List[LintDiagnostic] = diff --git a/modules/lint/src/test/scala/specrest/lint/DroppedOutputsTest.scala b/modules/lint/src/test/scala/specrest/lint/DroppedOutputsTest.scala new file mode 100644 index 00000000..e274559e --- /dev/null +++ b/modules/lint/src/test/scala/specrest/lint/DroppedOutputsTest.scala @@ -0,0 +1,72 @@ +package specrest.lint + +import munit.CatsEffectSuite +import specrest.ir.generated.SpecRestGenerated.SpanT +import specrest.ir.generated.SpecRestGenerated.less_int +import specrest.lint.testutil.SpecFixtures + +class DroppedOutputsTest extends CatsEffectSuite: + + private def deleteSpec(output: String, conventions: String): String = + s"""service DropDemo { + | entity Item { + | id: Int + | name: String + | } + | + | state { + | items: Int -> Item + | } + | + | operation DeleteItem { + | input: id: Int + | output: $output + | + | requires: + | id in items + | + | ensures: + | id not in items' + | } + |$conventions}""".stripMargin + + private val overrideBlock = + """ conventions { + | DeleteItem.http_status_success = 200 + | } + |""".stripMargin + + List( + ("warns on entity output with defaulted 204", "item: Item", "", 1), + ("silent when http_status_success overrides to 200", "item: Item", overrideBlock, 0), + ("silent on single Bool flag output with 204", "deleted: Bool", "", 0) + ).foreach: (label, output, conventions, expected) => + test(s"L07 $label"): + SpecFixtures.buildFromSource("DropDemo", deleteSpec(output, conventions)).map: ir => + val diags = DroppedOutputs.run(ir) + assertEquals(diags.length, expected, diags.map(_.message).toString) + + test("L07 names the op, the 204, the dropped outputs, and the override"): + SpecFixtures.buildFromSource("DropDemo", deleteSpec("item: Item", "")).map: ir => + val diags = DroppedOutputs.run(ir) + assertEquals(diags.length, 1) + val d = diags.head + assertEquals(d.code, "L07") + assertEquals(d.level, LintLevel.Warning) + assert(d.message.contains("DeleteItem"), d.message) + assert(d.message.contains("204"), d.message) + assert(d.message.contains("'item'"), d.message) + assert(d.message.contains("DeleteItem.http_status_success"), d.message) + assert( + d.span.exists { case SpanT(line, _, _, _) => less_int(BigInt(0), line) }, + s"expected span, got ${d.span}" + ) + + test("L07 silent on the all-lints-pass fixture"): + SpecFixtures.loadLintIR("passing").map: ir => + assertEquals(DroppedOutputs.run(ir), Nil) + + List("url_shortener", "todo_list", "auth_service", "ecommerce").foreach: name => + test(s"L07 silent on fixtures/spec/$name.spec"): + SpecFixtures.loadIR(name).map: ir => + assertEquals(DroppedOutputs.run(ir), Nil) From 1216dafd2b40d36ae72fda01f3d4667343071702 Mon Sep 17 00:00:00 2001 From: HardMax71 Date: Thu, 9 Jul 2026 11:45:28 +0200 Subject: [PATCH 4/4] docs: unmangle the L07 table row --- .../docs/research/spec_language_design/developer-experience.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/content/docs/research/spec_language_design/developer-experience.md b/docs/content/docs/research/spec_language_design/developer-experience.md index be3aa51c..6da262d1 100644 --- a/docs/content/docs/research/spec_language_design/developer-experience.md +++ b/docs/content/docs/research/spec_language_design/developer-experience.md @@ -19,7 +19,7 @@ exits non-zero; a warning exits zero. | L04 | warning | two operations with the same input and output signature and equivalent `requires` | | L05 | warning | an entity declared but never referenced | | L06 | error | mutually recursive predicates or functions, which the verifier's inlining cannot unfold | -| L07 | warning | an operation whose outputs a resolved `204 No Content` success status would drop | +| L07 | warning | an operation whose resolved `204 No Content` success status would drop its declared outputs | The lints are deliberately narrow. L01 fires only on literals whose type admits no operator at all, so it catches obvious mistakes without standing in for a full type checker.