Convention Engine Reference

Overview

The Convention Engine is the bridge between the abstract world of formal specifications and the concrete world of REST APIs, HTTP methods, database schemas, and validation rules. It reads the parsed ServiceIR, classifies each operation against the M1-M10 rules, derives endpoints (method + path + status code), derives a relational schema for the entities, and validates user-supplied convention overrides.

Looking for the design rationale, every rule, edge case, and override mechanism end-to-end? See Convention Engine.

The engine is deterministic: identical IR -> identical endpoint and schema decisions, every run. Authoritative source: convention/convention/.

Operation classification (M1-M10)

The M-rules classify operations, not entities or fields. Each operation in a spec gets exactly one rule, and that rule decides the HTTP method. Field- and entity-level mappings (DB column types, table names, etc.) are handled separately by Schema and Naming (covered below).

OperationKind lives in Types.scala; the dispatch logic lives in Classify.scala. M6 is reserved in the enum (CreateChild) but no current dispatch arm produces it, nested POST /parent/{id}/child is on the roadmap. See Convention Engine section M6 for the planned semantics.

Synthesis strategy (#31)

Each OperationClassification also carries a strategy: SynthesisStrategy (either DirectEmit or LlmSynthesis), orthogonal to the M-rule. It signals whether Phase 6's CEGIS loop drives the body synthesis, even though the convention engine alone decides today's HTTP/path/schema mapping.

The classifier walks each flattened ensures clause and accepts the operation as DirectEmit only when every clause matches one of these shapes:

• preservation s' = s over a state field s,
• delete key not in s',
• cardinality delta #s' = #pre(s) +/- 1 (or #s' = #pre(s) / #s' = #s),
• map insert via plus s' = pre(s) + { k -> v } with leaf key/value,
• pointwise insert/update s'[k] = leaf or s'[k].field = leaf where leaf is a literal, identifier, or enum case,
• output binding out = read where read is a pure lookup (no arithmetic, string ops, calls, or comprehensions).

Anything else (arithmetic on pre-values, string concatenation, set comprehensions, unrecognized calls) flips the operation to LlmSynthesis. The heuristic is intentionally conservative: when in doubt the operation goes to the LLM bucket so direct-emit only fires on shapes we can prove correct from templates.

The strategy is surfaced in inspect:

$ spec-to-rest inspect fixtures/spec/url_shortener.spec
Service: UrlShortener
  1 entities, 0 enums, 4 operations (1 DIRECT_EMIT, 3 LLM_SYNTHESIS), 3 invariants
    Shorten: LLM_SYNTHESIS
    Resolve: LLM_SYNTHESIS
    Delete: DIRECT_EMIT
    ListAll: LLM_SYNTHESIS

inspect --format json adds a top-level synthesis_strategy map keyed by operation name. Every Phase 6 consumer reads it: synth try and synth verify both gate LLM calls on this field, and compile --with-synthesis (#27) uses it to decide which methods need synthesis at all. DirectEmit operations are rejected at the CLI boundary. Graduated fallback (#30) and DafnyPro-style hint augmentation (#229) cover cases where verification needs help.

Dafny signature generation (#32)

The second wedge: inspect --format dafny lifts a ServiceIRFull into a deterministic Dafny skeleton. That skeleton is the prompt input the CEGIS controller hands to the LLM. The translator lives in Generator.scala; no Dafny binary is invoked at runtime, since emission is pure IR-to-string.

What lands in the file:

• An Option<T> datatype + per-spec datatype declarations for enums and entities.
• Type aliases with their where constraints lifted to parallel <T>Where(value) predicates. The <T>Where is then auto-attached to every operation: input params of an aliased type get a requires <T>Where(p) clause, output params get the matching ensures <T>Where(out) clause, which closes the gap so a constrained alias actually constrains the contract.
• Entity invariants become <T>Inv(x) predicates. Field-level where constraints are folded in alongside explicit invariant: clauses so things like id: Int where value > 0 are enforced.
• A class ServiceState { var ... } (preserving spec field declaration order via ListMap) mirroring the spec's state { ... } block, with each invariant clause rolled into a ServiceStateInv(st) predicate.
• One method per spec operation: parameters, returns (...), modifies st, requires/ensures clauses (split per &&), bracketed by ServiceStateInv(st) to make preservation an explicit obligation. The body is a // YOUR CODE HERE placeholder that the M6.3 LLM-integration loop (#28) substitutes during synthesis.
• Axiomatized predicate declarations for any unknown calls (isValidURI, regex matches, etc.) with trivially-true bodies; these are placeholders the CEGIS loop refines.

Two pre-render rewrites help the output type-check more often:

• The p != none ==> body idiom is desugared by replacing bare references to the Option-typed param p inside body with p.value, matching Dafny's Option unwrapping semantics.
• Set comprehensions over a state field of map type project to map values via :: <map>[k], giving the result the value type the spec expects (the alternative set k | k in m would have type set<K>, not set<V>).

Each method's (signature, requires, ensures, modifies) tuple is also exposed as a DafnyMethodHeader on the result, so the diff-checker (synth/DiffChecker.scala) can verify the LLM did not weaken the spec-derived clauses.

Known v1 limitations (deferred follow-ups):

• Calls used in value position (e.g. now() returning a timestamp) emit as predicates, which Dafny rejects on type-check. Context-aware classification is a follow-up.
• Lambdas synthesize as (p: int) => body; the parameter type is a placeholder until type-info propagation lands.
• Specs with partial entity constructors (e.g. Foo { x = 1 } where Foo has more fields) currently fail with a clear error; full constructor inference is a follow-up.

Goldens for safe_counter, url_shortener, and todo_list live under fixtures/golden/dafny/; they lock down the generator's deterministic output, not full dafny resolve correctness.

Path / status derivation

Once an operation is classified, Path.deriveEndpoints builds the EndpointSpec:

The HTTP method comes from a user-supplied http_method override if present, otherwise from the rule's default in the table above. The path comes from http_path if set, otherwise from a kind-specific shape derived via Naming.toPathSegment, with {id} interpolated from the input parameter whose type matches the relation's domain key. The status code comes from http_status_success if set, otherwise 201 for Create/CreateChild, 204 for Delete (and any DELETE method), and 200 everywhere else. GET methods send non-path params as query parameters; everything else sends them in the body.

Entity -> DB schema

Schema.deriveSchema lifts the IR's entities and state relations into a DatabaseSchema of TableSpec records. The engine maps spec types directly to PostgreSQL column types (PrimitiveTypeMap):

State relations with set or some multiplicity (A -> set B, A -> some B) emit junction tables for the many-to-many relationship. Enum values become TEXT columns with a CHECK (col IN (...)) constraint. User type aliases are resolved to their underlying primitive plus any where predicate (translated to a SQL CHECK).

Derivation lives in Schema.scala; naming (pluralization, kebab-case, snake_case, table names) lives in Naming.scala, which carries explicit uncountable and irregular plural tables (person -> people, data -> data, etc.).

Trigger and partial-index derivation are tracked in #57 (M7.6) and not yet emitted.

Override system

All convention overrides live in a service-wide conventions { ... } block. There is no per-operation with clause, the only place to override is the conventions block. Each rule has the shape Target.property [qualifier] = value.

conventions {
  Shorten.http_method         = "POST"
  Shorten.http_path           = "/shorten"
  Shorten.http_status_success = 201

  Resolve.http_method            = "GET"
  Resolve.http_path              = "/{code}"
  Resolve.http_status_success    = 302
  Resolve.http_header "Location" = output.url

  UrlMapping.db_table       = "url_mappings"
  UrlMapping.db_timestamps  = true
  UrlMapping.plural         = "url_mappings"

  ShortCode.strategy = "tests.strategies_user:short_code"
  Status.strategy    = "tests.strategies_user:realistic_status"

  User.test_strategy.password = "tests.strategies_user:strong_password"
}

The full property/target matrix lives in Convention overrides in the spec language. Validation runs in Validate.scala; unknown properties, mismatched targets, missing qualifiers, and duplicate rules surface as structured ConventionDiagnostics. The convention override system was hardened under #10 (M2.3) and the per-field test_strategy work under #134 (M5.6).

Deployment profiles

Profiles bundle target-language and runtime conventions (Python types, SQLAlchemy column mapping, FastAPI imports, etc.). The shipped registry contains exactly one profile:

• python-fastapi-postgres (default), FastAPI + SQLAlchemy 2 (async) + Alembic + PostgreSQL 16. The only profile compile accepts on main.

Multiple-environment overrides (development / staging / production / testing) and additional target profiles (Go/chi, TS/Express) are roadmap work:

• #33 (M7.1), Go/chi Target
• #35 (M7.2), TypeScript/Express Target
• #63 (M7.9), Multi-environment compose overrides (staging/prod)
• #58 (M7.7), Alternative database dialects (SQLite, MySQL)

The registry is a tiny Map[String, DeploymentProfile] in Registry.scala; adding a new profile is a registry insertion plus a Handlebars template tree.