spec_to_rest

Spec -> Verify -> Emit

A trimmed view of fixtures/spec/url_shortener.spec, the verifier's check list, and an excerpt of the FastAPI router emitted for the Python target (chi and Express render the same spec into their own stacks), all from one compile invocation:

service UrlShortener {
  type ShortCode = String where
    len(value) >= 6 and len(value) <= 10

  entity UrlMapping {
    code: ShortCode
    url: String where isValidURI(value)
    click_count: Int where value >= 0
  }

  state {
    store: ShortCode -> lone String
    metadata: ShortCode -> lone UrlMapping
  }

  operation Shorten {
    input:  url: String
    output: code: ShortCode

    requires: isValidURI(url)
    ensures:
      code not in pre(store)
      store' = pre(store) + {code -> url}
  }

  invariant metadataConsistent:
    dom(store) = dom(metadata)
}

from fastapi import APIRouter, Depends, HTTPException
from sqlalchemy.ext.asyncio import AsyncSession

from app.database import get_session
from app.schemas.url_mapping import (
    ShortenRequest,
    UrlMappingRead,
)
from app.services.url_mapping import UrlMappingService

router = APIRouter(tags=["url_mapping"])


@router.post("/shorten", status_code=201)
async def shorten(
    body: ShortenRequest,
    session: AsyncSession = Depends(get_session),
) -> UrlMappingRead:
    svc = UrlMappingService(session)
    return await svc.shorten(body)


@router.get("/{code}", status_code=200)
async def resolve(
    code: str,
    session: AsyncSession = Depends(get_session),
) -> UrlMappingRead:
    svc = UrlMappingService(session)
    result = await svc.resolve(code)
    if result is None:
        raise HTTPException(status_code=404, detail="not found")
    return result

If any check above had returned unsat, compile would exit non-zero and write nothing, not even an empty output directory. See Verify-as-gate in compile.

What is a verifying compiler?

Most code generators are scaffolds. They turn a schema into boilerplate and trust you to keep the runtime correct by hand. A verifying compiler treats the specification as a logical theory instead. Each operation becomes a verification condition, a first-order formula that has to be unsatisfiable for the operation to preserve every invariant, and Z3 must settle all of them before a single file is written. That holds for every input the spec admits, not just the cases a test happens to hit: the emitted handlers cannot leave an invariant broken.

How spec_to_rest compares

Behind the compiler

Five stages run on every invocation: Parse (ANTLR4) -> IR Build -> Verify (Z3 + Alloy) -> Map (M1-M10 conventions) -> Emit (Handlebars). A sixth stage, Testgen (per-target native conformance suite), runs by default and is suppressed only when --no-tests is passed. Each stage returns IO; failures land in Either[VerifyError, _].

A static classifier routes each proof obligation to the solver that fits. Z3 owns first-order invariants and preservation; Alloy owns powerset (^) and always/eventually. The two coverage areas do not overlap, and a construct that falls outside both surfaces as a translator_limitation diagnostic rather than slipping through as a silent pass.

Per-check timeouts run inside the solver. SIGINT propagates through fiber cancel to Z3 Context.interrupt(). --parallel n dispatches via parTraverseN.

When verify succeeds, compile emits the full project for the chosen target: source tree, migrations, openapi.yaml, Dockerfile, docker-compose.yml, and a CI workflow (the FastAPI layout is app/ + alembic/; chi and Express emit their own idiomatic trees). When verify fails, each failing check is rendered in prose: which operation, which invariant, which contributing field, with concrete pre and post values lifted from the solver model.

--dump-vc <dir> writes per-check .smt2 and .als files alongside verdicts.json. --explain extracts the Z3 unsat core and surfaces the contributing spec spans. The translator itself is proved correct in Isabelle/HOL, by translate_soundness_standalone (DirectSound.thy) and cat_h_progress_and_preservation_direct (DirectPreservation.thy), both closing with zero sorry.