PostgreSQL

This page documents what the compiler emits when a spec is compiled against the ts-express-postgres target. It is the concrete companion to the target-agnostic Code Generation Pipeline research doc.

The canonical source of truth is the emitter at codegen/ts/EmitTs.scala, which renders the Handlebars templates under codegen/resources/templates/ts/express/. Running

sbt "cli/run compile --framework express --db postgres --ignore-verify --out /tmp/out fixtures/spec/url_shortener.spec"

produces the tree this page describes. If this page and the emitter disagree, the emitter wins; file an issue or PR to correct the doc. The full byte-level shape of the output for url_shortener.spec is checked in under fixtures/golden/codegen/ts/express/postgres/url_shortener/ and asserted by EmitTsTest.

At a glance

Project layout

.
├── package.json
├── tsconfig.json
├── prisma/
│   └── schema.prisma                   # Prisma model + @@map for tables
├── src/
│   ├── index.ts                        # entrypoint; SIGTERM/SIGINT shutdown
│   ├── app.ts                          # express() + routes + error middleware
│   ├── config.ts                       # zod-validated env config
│   ├── prisma.ts                       # PrismaClient singleton
│   ├── middleware/
│   │   ├── error.ts                    # HttpError + zod 422 + 500 fallback
│   │   └── validate.ts                 # validateBody(schema)
│   ├── routes/
│   │   ├── index.ts                    # mountRoutes(app) wires per-entity
│   │   └── {entity_plural}.ts          # express handlers (1 per operation)
│   ├── services/
│   │   └── {entity}.ts                 # Prisma-backed business logic
│   ├── schemas/
│   │   └── {entity}.ts                 # Zod request schemas
│   └── types/
│       └── {entity}.ts                 # TS interfaces (Model + Create/Read DTOs)
├── Dockerfile                          # multi-stage build → node:20-alpine
├── docker-compose.yml                  # app + db services
├── Makefile                            # install / build / test / prisma-*
├── .env.example
├── .gitignore
├── .dockerignore
├── README.md
├── .github/workflows/ci.yml
├── tests/health.test.ts
└── openapi.yaml                        # target-agnostic OpenAPI 3.1

Type mapping

The mapping lives in profile/TypeMap.scala.

Int deliberately maps to INTEGER (not BIGINT): the JSON bigint serialization story is fragile in v0, so 32-bit integers are the conservative default for the API surface. Surrogate primary keys still use BIGSERIAL via Prisma's @id @default(autoincrement()) and TypeScript number.

Operation routing

RouteKind.classify (target-agnostic) maps each operation to one of create, read, list, delete, redirect, other. The TS emitter renders the matching route/service template. Operations whose body shape does not match the entity's field set route to other and emit a stub the user fills in (the spec contract is preserved by the verify gate, so the stub still has a known interface).

For lookups by a non-id column the emitter uses Prisma's findFirst / deleteMany (which do not require a @unique constraint). Lookups by id use findUnique / delete.

Path-parameter conversion

Spec paths use {name} placeholders (chi/OpenAPI style); Express expects :name. The emitter converts /{code} → /:code before rendering the route template.

Dafny → JavaScript integration

When compile --framework express --db postgres --with-synthesis is invoked and the verified-body cache is populated, the compiler:

1. Routes through dafny translate js (via TargetLanguage.JavaScript).
2. Lays the produced JS files under src/dafnyKernel/.
3. Emits operation bindings of the form dafnyKernel.{OperationName}.

The kernel is only emitted when at least one operation is classified as LLM_SYNTHESIS; otherwise the TS project is purely CRUD/Prisma.

CI gate

.github/workflows/ts-build.yml is a {postgres, sqlite, mysql} matrix. On every PR that touches the TS templates, profile, emitter, or the shared migration renderer it re-runs compile --framework express --db <dialect>, then npm install && npx prisma generate && npx tsc --noEmit && npm test && npm run build against the emitted project and a Prisma migration round-trip (migrate deploy → migrate reset → migrate deploy) against a real postgres:17 / mysql:8.4 service (SQLite uses a file) — so the emitted prisma/migrations/** is proven to apply and replay on every supported dialect, not just that the TypeScript compiles.

Test generation

Conformance / property / stateful test generation (--with-tests) is available for ts-express-* on every dialect (postgres, sqlite, mysql), emitted in the target's own language: Vitest + fast-check property tests, not Python. testgen plugs the TypeScript renderers into the shared Backend.scala seam (ExprBackend / StrategyBackend / HarnessTemplates); the same spec-derived derivation engine feeds the Python (fastapi) path, which stays the byte-identical differential oracle (#278, #280; closes #265).

--with-tests emits under tests/: behavioral (<svc>.behavioral.test.ts, positive-ensures via fc.asyncProperty), stateful (<svc>.stateful.test.ts, random operation sequences asserting invariants per step), and structural-lite (<svc>.structural.test.ts, fuzzes every non-stub operation with type-valid input and asserts no 5xx — schemathesis's core check minus full schema validation; fail-loud stubs are honest-skipped exactly as the Python schemathesis renderer excludes them, recorded in tests/_testgen_skips.json), plus the _runtime.ts / _client.ts / _predicates.ts / _strategies.ts harness and vitest.config.ts. The /__test_admin__/* reset/state/seed router is emitted as src/routes/testAdmin.ts, mounted only when ENABLE_TEST_ADMIN=1 (the production build leaves it unmounted).

Run it against a running service:

ENABLE_TEST_ADMIN=1 npm start &
node tests/run_conformance.mjs smoke     # or: npm test

ts-express -> conformance suite runs this in CI (ts-build.yml) across all four fixtures × postgres/sqlite, mirroring the python-build.yml pattern. (The spec-to-rest test CLI wrapper still drives only the Python runner; see CLI Reference.)