Convention Engine

Given entity E with fields {f1, f2, f3, f4}
Given operation Op that mutates an existing E

If Op.ensures references assignments to ALL of {f1, f2, f3, f4}:
    -> PUT (full replacement)

If Op.ensures references assignments to a STRICT SUBSET of {f1, f2, f3, f4}:
    -> PATCH (partial update)

If Op.ensures references assignments to ALL fields BUT some are
  conditional (if-then in ensures):
    -> PATCH (conditional update is partial by nature)

operation UpdateUser {
  input: id: UserId, name: String, email: String, bio: String
  requires: id in users
  ensures:
    users'[id].name = name
    users'[id].email = email
    users'[id].bio = bio
    users'[id].created_at = users[id].created_at  // unchanged
}
// All fields accounted for -> PUT

operation UpdateUserEmail {
  input: id: UserId, email: String
  requires: id in users
  ensures:
    users'[id].email = email
    // other fields implicitly unchanged
}
// Only email changes -> PATCH

state {
  orders: OrderId -> Order
  line_items: OrderId -> set LineItem   // LineItem is nested under Order
}

requires:
  id in orders                           // -> 404 if fails
  and orders[id].status = "draft"        // -> 409 if fails
  and total > 0                          // -> 422 if fails

{
  "data": <payload>,
  "meta": {
    "request_id": "uuid",
    "timestamp": "ISO-8601"
  }
}

{
  "error": {
    "code": "VALIDATION_FAILED",
    "message": "Human-readable description",
    "details": [
      {
        "field": "email",
        "constraint": "must be a valid email address",
        "value": "not-an-email"
      }
    ]
  },
  "meta": {
    "request_id": "uuid",
    "timestamp": "ISO-8601"
  }
}

CREATE TABLE orders_line_items_items (
    id           BIGSERIAL PRIMARY KEY,
    order_id     BIGINT NOT NULL REFERENCES orders(id) ON DELETE CASCADE,
    line_item_id BIGINT NOT NULL REFERENCES line_items(id) ON DELETE CASCADE,
    created_at   TIMESTAMPTZ NOT NULL DEFAULT NOW(),
    UNIQUE(order_id, line_item_id)  -- prevent duplicates
);

{
  "error": {
    "code": "VALIDATION_FAILED",
    "message": "Request validation failed",
    "details": [
      { "field": "email", "constraint": "must match pattern ^.+@.+$", "value": "bad" },
      { "field": "age", "constraint": "must be greater than 0", "value": -5 }
    ]
  }
}

conventions {
  // HTTP method override
  Resolve.http_method = "GET"

  // URL path override
  Resolve.http_path = "/{code}"

  // Status code override
  Resolve.http_status_success = 302

  // Custom header
  Resolve.http_header "Location" = output.url

  // DB table name override
  ShortCode.db_table = "codes"

  // DB column type override
  ShortCode.value_db_type = "VARCHAR(12)"

  // DB index override
  ShortCode.value_db_index = "unique"

  // JSON field naming convention (global)
  global.json_naming = "camelCase"    // "snake_case" | "camelCase" | "PascalCase"

  // Envelope format (global)
  global.response_envelope = "bare"   // "standard" | "bare" | "jsonapi"

  // Pagination defaults (global)
  global.pagination_default_limit = 50
  global.pagination_max_limit = 200

  // Authentication requirement
  Shorten.http_auth = "bearer"        // "none" | "bearer" | "api_key" | "basic"
  global.http_auth = "bearer"         // applied to all endpoints

  // Soft delete behavior
  Delete.http_soft_delete = true

  // Custom error message
  Resolve.requires_0_error_message = "Short code not found. It may have expired."

  // Custom error code
  Resolve.requires_0_error_code = "CODE_EXPIRED_OR_NOT_FOUND"

  // Disable auto-generated timestamp columns
  ShortCode.db_timestamps = false

  // Custom plural form
  ShortCode.plural = "codes"

  // Sort the resource name override
  Inventory.db_table = "inventory_levels"
}

service UrlShortener {

  entity ShortCode {
    value: String
    invariant: len(value) >= 6 and len(value) <= 10
    invariant: value matches /^[a-zA-Z0-9]+$/
  }

  entity LongURL {
    value: String
    invariant: isValidURI(value)
  }

  state {
    store: ShortCode -> lone LongURL
    created_at: ShortCode -> DateTime
  }

  operation Shorten {
    input:   url: LongURL
    output:  code: ShortCode, short_url: String

    requires: isValidURI(url.value)

    ensures:
      code not in pre(store)
      store'[code] = url
      short_url = base_url + "/" + code.value
      #store' = #store + 1
  }

  operation Resolve {
    input:  code: ShortCode
    output: url: LongURL

    requires: code in store

    ensures:
      url = store[code]
      store' = store
  }

  operation Delete {
    input:  code: ShortCode

    requires: code in store

    ensures:
      code not in store'
      #store' = #store - 1
  }

  operation ListAll {
    output: entries: Set[UrlMapping]

    ensures:
      entries = store
      store' = store
  }

  conventions {
    Resolve.http_status_success = 302
    Resolve.http_header "Location" = output.url
  }
}

-- Entity: ShortCode (primary table from the 'store' relation)
CREATE TABLE short_codes (
    id          BIGSERIAL PRIMARY KEY,
    value       VARCHAR(10) NOT NULL
                CHECK (length(value) >= 6 AND length(value) <= 10)
                CHECK (value ~ '^[a-zA-Z0-9]+$'),
    created_at  TIMESTAMPTZ NOT NULL DEFAULT NOW(),
    updated_at  TIMESTAMPTZ NOT NULL DEFAULT NOW()
);

CREATE UNIQUE INDEX idx_short_codes_value ON short_codes(value);

-- Relation: store (ShortCode -> lone LongURL)
-- Since 'lone' means at most one, this is a nullable FK on short_codes
-- But since the relation is the core state, we embed it in the same table:
ALTER TABLE short_codes
    ADD COLUMN long_url TEXT
    CHECK (long_url ~ '^https?://');  -- derived from isValidURI invariant

-- Metadata: created_at relation
-- Already covered by the auto-generated created_at column

-- Trigger: update updated_at on modification
CREATE OR REPLACE FUNCTION update_updated_at()
RETURNS TRIGGER AS $$
BEGIN
    NEW.updated_at = NOW();
    RETURN NEW;
END;
$$ LANGUAGE plpgsql;

CREATE TRIGGER trg_short_codes_updated_at
    BEFORE UPDATE ON short_codes
    FOR EACH ROW
    EXECUTE FUNCTION update_updated_at();

openapi: 3.1.0
info:
  title: UrlShortener API
  version: 1.0.0

paths:
  /short-codes:
    post:
      operationId: shorten
      summary: Create a new short code
      requestBody:
        required: true
        content:
          application/json:
            schema:
              $ref: "#/components/schemas/ShortenRequest"
      responses:
        "201":
          description: Short code created
          headers:
            Location:
              schema:
                type: string
              description: URL of the created resource
          content:
            application/json:
              schema:
                $ref: "#/components/schemas/ShortenResponse"
        "422":
          description: Validation failed
          content:
            application/json:
              schema:
                $ref: "#/components/schemas/ErrorResponse"
    get:
      operationId: listAll
      summary: List all short codes
      parameters:
        - name: page
          in: query
          schema:
            type: integer
            default: 1
            minimum: 1
        - name: limit
          in: query
          schema:
            type: integer
            default: 20
            minimum: 1
            maximum: 100
      responses:
        "200":
          description: List of short codes
          content:
            application/json:
              schema:
                $ref: "#/components/schemas/ListAllResponse"

  /short-codes/{code}:
    get:
      operationId: resolve
      summary: Resolve a short code to its URL
      parameters:
        - name: code
          in: path
          required: true
          schema:
            type: string
            minLength: 6
            maxLength: 10
            pattern: "^[a-zA-Z0-9]+$"
      responses:
        "302":
          description: Redirect to the long URL
          headers:
            Location:
              schema:
                type: string
              description: The original long URL
        "404":
          description: Short code not found
          content:
            application/json:
              schema:
                $ref: "#/components/schemas/ErrorResponse"
    delete:
      operationId: delete
      summary: Delete a short code
      parameters:
        - name: code
          in: path
          required: true
          schema:
            type: string
            minLength: 6
            maxLength: 10
            pattern: "^[a-zA-Z0-9]+$"
      responses:
        "204":
          description: Short code deleted
        "404":
          description: Short code not found
          content:
            application/json:
              schema:
                $ref: "#/components/schemas/ErrorResponse"

components:
  schemas:
    ShortenRequest:
      type: object
      required: [url]
      properties:
        url:
          type: object
          required: [value]
          properties:
            value:
              type: string
              format: uri

    ShortenResponse:
      type: object
      properties:
        data:
          type: object
          properties:
            code:
              type: object
              properties:
                value:
                  type: string
                  minLength: 6
                  maxLength: 10
            short_url:
              type: string
              format: uri

    ListAllResponse:
      type: object
      properties:
        data:
          type: array
          items:
            type: object
            properties:
              code:
                $ref: "#/components/schemas/ShortCodeSchema"
              url:
                $ref: "#/components/schemas/LongURLSchema"
        meta:
          $ref: "#/components/schemas/PaginationMeta"

    ShortCodeSchema:
      type: object
      properties:
        value:
          type: string
          minLength: 6
          maxLength: 10
          pattern: "^[a-zA-Z0-9]+$"

    LongURLSchema:
      type: object
      properties:
        value:
          type: string
          format: uri

    PaginationMeta:
      type: object
      properties:
        page:
          type: integer
        limit:
          type: integer
        total:
          type: integer

    ErrorResponse:
      type: object
      properties:
        error:
          type: object
          properties:
            code:
              type: string
            message:
              type: string
            details:
              type: array
              items:
                type: object
                properties:
                  field:
                    type: string
                  constraint:
                    type: string
                  value: {}

service OrderService {

  entity Product {
    name: String
    price: Decimal
    sku: String
    invariant: price > 0
    invariant: len(sku) = 10
  }

  entity LineItem {
    quantity: Int
    unit_price: Decimal
    invariant: quantity > 0
    invariant: unit_price > 0
  }

  entity Order {
    status: String
    total: Decimal
    customer_email: String
    invariant: status in {"draft", "placed", "paid", "shipped", "cancelled"}
    invariant: total >= 0
    invariant: customer_email matches /^.+@.+$/
  }

  entity InventoryRecord {
    quantity_available: Int
    invariant: quantity_available >= 0
  }

  state {
    products: ProductId -> one Product
    inventory: ProductId -> one InventoryRecord
    orders: OrderId -> one Order
    line_items: OrderId -> set LineItem
    item_product: LineItem -> one Product    // each line item references a product
  }

  // --- CRUD Operations ---

  operation CreateProduct {
    input: name: String, price: Decimal, sku: String, initial_stock: Int
    output: product: Product

    requires: initial_stock >= 0

    ensures:
      product not in pre(products)
      products'[product] = Product{name, price, sku}
      inventory'[product] = InventoryRecord{initial_stock}
  }

  operation GetProduct {
    input: id: ProductId
    output: product: Product, stock: Int

    requires: id in products

    ensures:
      product = products[id]
      stock = inventory[id].quantity_available
      products' = products
  }

  operation ListProducts {
    input: name_filter?: String, min_price?: Decimal, max_price?: Decimal
    output: results: set Product

    ensures:
      results = {p in products | matches_filters(p, name_filter, min_price, max_price)}
      products' = products
  }

  // --- Order Lifecycle ---

  operation CreateOrder {
    input: customer_email: String
    output: order: Order

    requires: customer_email matches /^.+@.+$/

    ensures:
      order not in pre(orders)
      orders'[order] = Order{status: "draft", total: 0, customer_email}
      line_items'[order] = {}
  }

  operation AddLineItem {
    input: order_id: OrderId, product_id: ProductId, quantity: Int
    output: item: LineItem

    requires:
      order_id in orders
      orders[order_id].status = "draft"
      product_id in products
      quantity > 0
      inventory[product_id].quantity_available >= quantity

    ensures:
      item = LineItem{quantity, unit_price: products[product_id].price}
      line_items'[order_id] = line_items[order_id] + {item}
      item_product'[item] = products[product_id]
      orders'[order_id].total = orders[order_id].total + item.quantity * item.unit_price
  }

  operation RemoveLineItem {
    input: order_id: OrderId, item_id: LineItemId

    requires:
      order_id in orders
      orders[order_id].status = "draft"
      item_id in line_items[order_id]

    ensures:
      line_items'[order_id] = line_items[order_id] - {item_id}
      orders'[order_id].total = orders[order_id].total - item_id.quantity * item_id.unit_price
  }

  // --- State Machine Transitions ---

  operation PlaceOrder {
    input: order_id: OrderId

    requires:
      order_id in orders
      orders[order_id].status = "draft"
      #line_items[order_id] > 0      // must have at least one item

    ensures:
      orders'[order_id].status = "placed"
      // reserve inventory
      all item in line_items[order_id] |
        inventory'[item_product[item]].quantity_available =
          inventory[item_product[item]].quantity_available - item.quantity
  }

  operation PayOrder {
    input: order_id: OrderId, payment_token: String

    requires:
      order_id in orders
      orders[order_id].status = "placed"

    ensures:
      orders'[order_id].status = "paid"
  }

  operation ShipOrder {
    input: order_id: OrderId, tracking_number: String

    requires:
      order_id in orders
      orders[order_id].status = "paid"

    ensures:
      orders'[order_id].status = "shipped"
  }

  operation CancelOrder {
    input: order_id: OrderId

    requires:
      order_id in orders
      orders[order_id].status in {"draft", "placed"}

    ensures:
      orders'[order_id].status = "cancelled"
      // release inventory if was placed
      orders[order_id].status = "placed" implies
        all item in line_items[order_id] |
          inventory'[item_product[item]].quantity_available =
            inventory[item_product[item]].quantity_available + item.quantity
  }

  operation GetOrder {
    input: order_id: OrderId
    output: order: Order, items: set LineItem

    requires: order_id in orders

    ensures:
      order = orders[order_id]
      items = line_items[order_id]
      orders' = orders
  }
}

-- Entity: Product
CREATE TABLE products (
    id          BIGSERIAL PRIMARY KEY,
    name        TEXT NOT NULL,
    price       NUMERIC(19,4) NOT NULL CHECK (price > 0),
    sku         VARCHAR(10) NOT NULL CHECK (length(sku) = 10),
    created_at  TIMESTAMPTZ NOT NULL DEFAULT NOW(),
    updated_at  TIMESTAMPTZ NOT NULL DEFAULT NOW()
);

CREATE UNIQUE INDEX idx_products_sku ON products(sku);

-- Entity: InventoryRecord (1:1 with Product via 'inventory' relation)
CREATE TABLE inventory_records (
    id                  BIGSERIAL PRIMARY KEY,
    product_id          BIGINT NOT NULL UNIQUE REFERENCES products(id) ON DELETE CASCADE,
    quantity_available  INTEGER NOT NULL CHECK (quantity_available >= 0),
    created_at          TIMESTAMPTZ NOT NULL DEFAULT NOW(),
    updated_at          TIMESTAMPTZ NOT NULL DEFAULT NOW()
);

CREATE INDEX idx_inventory_records_product_id ON inventory_records(product_id);

-- Entity: Order
CREATE TABLE orders (
    id              BIGSERIAL PRIMARY KEY,
    status          VARCHAR(20) NOT NULL DEFAULT 'draft'
                    CHECK (status IN ('draft', 'placed', 'paid', 'shipped', 'cancelled')),
    total           NUMERIC(19,4) NOT NULL DEFAULT 0 CHECK (total >= 0),
    customer_email  TEXT NOT NULL CHECK (customer_email ~ '.+@.+'),
    created_at      TIMESTAMPTZ NOT NULL DEFAULT NOW(),
    updated_at      TIMESTAMPTZ NOT NULL DEFAULT NOW()
);

CREATE INDEX idx_orders_status ON orders(status);
CREATE INDEX idx_orders_customer_email ON orders(customer_email);

-- Entity: LineItem (child of Order via 'line_items' relation)
CREATE TABLE line_items (
    id          BIGSERIAL PRIMARY KEY,
    order_id    BIGINT NOT NULL REFERENCES orders(id) ON DELETE CASCADE,
    product_id  BIGINT NOT NULL REFERENCES products(id) ON DELETE RESTRICT,
    quantity    INTEGER NOT NULL CHECK (quantity > 0),
    unit_price  NUMERIC(19,4) NOT NULL CHECK (unit_price > 0),
    created_at  TIMESTAMPTZ NOT NULL DEFAULT NOW(),
    updated_at  TIMESTAMPTZ NOT NULL DEFAULT NOW()
);

CREATE INDEX idx_line_items_order_id ON line_items(order_id);
CREATE INDEX idx_line_items_product_id ON line_items(product_id);

-- updated_at trigger (applied to all tables)
CREATE OR REPLACE FUNCTION update_updated_at()
RETURNS TRIGGER AS $$
BEGIN
    NEW.updated_at = NOW();
    RETURN NEW;
END;
$$ LANGUAGE plpgsql;

CREATE TRIGGER trg_products_updated_at BEFORE UPDATE ON products
    FOR EACH ROW EXECUTE FUNCTION update_updated_at();
CREATE TRIGGER trg_inventory_records_updated_at BEFORE UPDATE ON inventory_records
    FOR EACH ROW EXECUTE FUNCTION update_updated_at();
CREATE TRIGGER trg_orders_updated_at BEFORE UPDATE ON orders
    FOR EACH ROW EXECUTE FUNCTION update_updated_at();
CREATE TRIGGER trg_line_items_updated_at BEFORE UPDATE ON line_items
    FOR EACH ROW EXECUTE FUNCTION update_updated_at();

service SocialFeed {

  entity User {
    username: String
    display_name: String
    bio: String
    invariant: len(username) >= 3 and len(username) <= 30
    invariant: username matches /^[a-zA-Z0-9_]+$/
  }

  entity Post {
    content: String
    posted_at: DateTime
    invariant: len(content) >= 1 and len(content) <= 280
  }

  entity Comment {
    content: String
    commented_at: DateTime
    invariant: len(content) >= 1 and len(content) <= 500
  }

  state {
    users: UserId -> one User
    posts: PostId -> one Post
    post_author: Post -> one User
    comments: PostId -> set Comment
    comment_author: Comment -> one User

    // M:N relations
    follows: User -> set User          // who a user follows
    likes: User -> set Post            // which posts a user liked
  }

  // --- User Operations ---

  operation CreateUser {
    input: username: String, display_name: String, bio: String
    output: user: User

    requires:
      len(username) >= 3
      // username must be unique (not already a value in users)
      all u in users | users[u].username != username

    ensures:
      user not in pre(users)
      users'[user] = User{username, display_name, bio}
  }

  operation GetUser {
    input: id: UserId
    output: user: User, follower_count: Int, following_count: Int

    requires: id in users

    ensures:
      user = users[id]
      follower_count = #{u in users | id in follows[u]}
      following_count = #follows[id]
  }

  // --- Post Operations ---

  operation CreatePost {
    input: author_id: UserId, content: String
    output: post: Post

    requires:
      author_id in users
      len(content) >= 1 and len(content) <= 280

    ensures:
      post not in pre(posts)
      posts'[post] = Post{content, posted_at: now()}
      post_author'[post] = users[author_id]
  }

  operation GetFeed {
    input: user_id: UserId, page: Int, limit: Int
    output: feed: list Post

    requires:
      user_id in users
      page >= 1
      limit >= 1 and limit <= 100

    ensures:
      feed = sorted_by_time(
        {p in posts | post_author[p] in follows[users[user_id]]},
        descending
      )
      // paginated to (page, limit)
  }

  // --- Social Graph ---

  operation Follow {
    input: follower_id: UserId, followee_id: UserId

    requires:
      follower_id in users
      followee_id in users
      follower_id != followee_id
      users[followee_id] not in follows[users[follower_id]]

    ensures:
      follows'[users[follower_id]] = follows[users[follower_id]] + {users[followee_id]}
  }

  operation Unfollow {
    input: follower_id: UserId, followee_id: UserId

    requires:
      follower_id in users
      followee_id in users
      users[followee_id] in follows[users[follower_id]]

    ensures:
      follows'[users[follower_id]] = follows[users[follower_id]] - {users[followee_id]}
  }

  // --- Likes ---

  operation LikePost {
    input: user_id: UserId, post_id: PostId

    requires:
      user_id in users
      post_id in posts
      posts[post_id] not in likes[users[user_id]]

    ensures:
      likes'[users[user_id]] = likes[users[user_id]] + {posts[post_id]}
  }

  operation UnlikePost {
    input: user_id: UserId, post_id: PostId

    requires:
      user_id in users
      post_id in posts
      posts[post_id] in likes[users[user_id]]

    ensures:
      likes'[users[user_id]] = likes[users[user_id]] - {posts[post_id]}
  }

  // --- Comments ---

  operation AddComment {
    input: post_id: PostId, author_id: UserId, content: String
    output: comment: Comment

    requires:
      post_id in posts
      author_id in users
      len(content) >= 1 and len(content) <= 500

    ensures:
      comment not in pre(comments[post_id])
      comments'[post_id] = comments[post_id] + {comment}
      comment = Comment{content, commented_at: now()}
      comment_author'[comment] = users[author_id]
  }

  operation GetComments {
    input: post_id: PostId, page: Int, limit: Int
    output: results: list Comment

    requires: post_id in posts

    ensures:
      results = sorted_by_time(comments[post_id], descending)
  }
}

-- Entity: User
CREATE TABLE users (
    id            BIGSERIAL PRIMARY KEY,
    username      VARCHAR(30) NOT NULL
                  CHECK (length(username) >= 3 AND length(username) <= 30)
                  CHECK (username ~ '^[a-zA-Z0-9_]+$'),
    display_name  TEXT NOT NULL,
    bio           TEXT NOT NULL DEFAULT '',
    created_at    TIMESTAMPTZ NOT NULL DEFAULT NOW(),
    updated_at    TIMESTAMPTZ NOT NULL DEFAULT NOW()
);

CREATE UNIQUE INDEX idx_users_username ON users(username);

-- Entity: Post
CREATE TABLE posts (
    id          BIGSERIAL PRIMARY KEY,
    author_id   BIGINT NOT NULL REFERENCES users(id) ON DELETE CASCADE,
    content     VARCHAR(280) NOT NULL
                CHECK (length(content) >= 1 AND length(content) <= 280),
    posted_at   TIMESTAMPTZ NOT NULL DEFAULT NOW(),
    created_at  TIMESTAMPTZ NOT NULL DEFAULT NOW(),
    updated_at  TIMESTAMPTZ NOT NULL DEFAULT NOW()
);

CREATE INDEX idx_posts_author_id ON posts(author_id);
CREATE INDEX idx_posts_posted_at ON posts(posted_at DESC);

-- Entity: Comment
CREATE TABLE comments (
    id            BIGSERIAL PRIMARY KEY,
    post_id       BIGINT NOT NULL REFERENCES posts(id) ON DELETE CASCADE,
    author_id     BIGINT NOT NULL REFERENCES users(id) ON DELETE CASCADE,
    content       VARCHAR(500) NOT NULL
                  CHECK (length(content) >= 1 AND length(content) <= 500),
    commented_at  TIMESTAMPTZ NOT NULL DEFAULT NOW(),
    created_at    TIMESTAMPTZ NOT NULL DEFAULT NOW(),
    updated_at    TIMESTAMPTZ NOT NULL DEFAULT NOW()
);

CREATE INDEX idx_comments_post_id ON comments(post_id);
CREATE INDEX idx_comments_author_id ON comments(author_id);
CREATE INDEX idx_comments_commented_at ON comments(commented_at DESC);

-- Junction Table: follows (User -> set User, M:N self-relation)
CREATE TABLE user_follows (
    id           BIGSERIAL PRIMARY KEY,
    follower_id  BIGINT NOT NULL REFERENCES users(id) ON DELETE CASCADE,
    followee_id  BIGINT NOT NULL REFERENCES users(id) ON DELETE CASCADE,
    created_at   TIMESTAMPTZ NOT NULL DEFAULT NOW(),
    CHECK (follower_id != followee_id),  -- from requires: follower_id != followee_id
    UNIQUE(follower_id, followee_id)
);

CREATE INDEX idx_user_follows_follower_id ON user_follows(follower_id);
CREATE INDEX idx_user_follows_followee_id ON user_follows(followee_id);

-- Junction Table: likes (User -> set Post, M:N)
CREATE TABLE user_post_likes (
    id          BIGSERIAL PRIMARY KEY,
    user_id     BIGINT NOT NULL REFERENCES users(id) ON DELETE CASCADE,
    post_id     BIGINT NOT NULL REFERENCES posts(id) ON DELETE CASCADE,
    created_at  TIMESTAMPTZ NOT NULL DEFAULT NOW(),
    UNIQUE(user_id, post_id)
);

CREATE INDEX idx_user_post_likes_user_id ON user_post_likes(user_id);
CREATE INDEX idx_user_post_likes_post_id ON user_post_likes(post_id);

GET /users/{user_id}/feed?page=1&limit=20

Response:
{
  "data": [
    {"id": 42, "content": "Hello world", "posted_at": "2026-04-05T10:30:00Z", ...},
    ...
  ],
  "meta": {
    "page": 1,
    "limit": 20,
    "total": 1523,
    "has_next": true,
    "has_prev": false
  }
}

GET /users/{user_id}/feed?after=eyJpZCI6NDJ9&limit=20

operation IncrementViewCount {
  input: code: ShortCode
  output: new_count: Int

  requires: code in store

  ensures:
    view_count'[code] = view_count[code] + 1
    new_count = view_count'[code]
    store' = store
}

operation Transfer {
  input: from_id: AccountId, to_id: AccountId, amount: Decimal

  requires:
    from_id in accounts
    to_id in accounts
    from_id != to_id
    accounts[from_id].balance >= amount
    amount > 0

  ensures:
    accounts'[from_id].balance = accounts[from_id].balance - amount
    accounts'[to_id].balance = accounts[to_id].balance + amount
}

conventions {
  global.http_idempotency_key = true
}

CREATE TABLE idempotency_keys (
    key         UUID PRIMARY KEY,
    endpoint    TEXT NOT NULL,
    request_hash TEXT NOT NULL,
    response_status INTEGER NOT NULL,
    response_body JSONB,
    created_at  TIMESTAMPTZ NOT NULL DEFAULT NOW(),
    expires_at  TIMESTAMPTZ NOT NULL DEFAULT NOW() + INTERVAL '24 hours'
);

parameters:
  - name: page
    in: query
    schema: { type: integer, default: 1, minimum: 1 }
  - name: limit
    in: query
    schema: { type: integer, default: 20, minimum: 1, maximum: 100 }
  - name: sort_by
    in: query
    schema: { type: string, enum: [created_at, name, price] }
  - name: sort_order
    in: query
    schema: { type: string, enum: [asc, desc], default: desc }

entity Attachment {
  filename: String
  content_type: String
  data: Bytes
}

POST /attachments
Content-Type: multipart/form-data

--boundary
Content-Disposition: form-data; name="filename"
document.pdf
--boundary
Content-Disposition: form-data; name="content_type"
application/pdf
--boundary
Content-Disposition: form-data; name="data"; filename="document.pdf"
Content-Type: application/octet-stream
<binary data>
--boundary--

operation ProcessLargeImport {
  input: file: Bytes
  output: job_id: JobId

  requires: len(file) > 0

  ensures:
    // async: result available later
    job_id not in pre(jobs)
    jobs'[job_id].status = "pending"
}

conventions {
  PlaceOrder.http_webhook = "order.placed"
}

generated/
  app/
    main.py                   # FastAPI app, middleware, exception handlers
    models/
      short_code.py           # SQLAlchemy model
    schemas/
      short_code.py           # Pydantic request/response schemas
    routers/
      short_codes.py          # FastAPI router with endpoint functions
    services/
      short_code_service.py   # Business logic (requires checks, state transitions)
    db/
      session.py              # Async DB session factory
      migrations/
        versions/
          001_initial.py      # Alembic migration
    tests/
      test_short_codes.py     # Pytest + httpx async tests
      conftest.py             # Fixtures (test DB, client)

from pydantic import BaseModel, Field, field_validator

class ShortenRequest(BaseModel):
    url: str = Field(..., description="The long URL to shorten")

    @field_validator('url')
    @classmethod
    def validate_url(cls, v: str) -> str:
        # Generated from: invariant: isValidURI(value)
        from urllib.parse import urlparse
        result = urlparse(v)
        if not all([result.scheme, result.netloc]):
            raise ValueError('Must be a valid URI')
        return v

from fastapi import HTTPException

class NotFoundError(HTTPException):
    def __init__(self, entity: str, id: str):
        super().__init__(
            status_code=404,
            detail={
                "error": {
                    "code": f"{entity.upper()}_NOT_FOUND",
                    "message": f"{entity} with the given ID was not found",
                }
            }
        )

class ConflictError(HTTPException):
    def __init__(self, code: str, message: str):
        super().__init__(
            status_code=409,
            detail={"error": {"code": code, "message": message}}
        )

generated/
  cmd/
    server/
      main.go                 # HTTP server setup, dependency injection
  internal/
    models/
      models.go               # Go structs for entities
    handlers/
      short_codes.go          # HTTP handler functions
    services/
      short_code_service.go   # Business logic
    db/
      queries.sql             # SQL queries (input for sqlc)
      sqlc.yaml               # sqlc configuration
      query.sql.go            # sqlc-generated Go code (DO NOT EDIT)
      migrations/
        001_initial.up.sql
        001_initial.down.sql
    middleware/
      error.go                # Error rendering middleware
      validate.go             # Request validation middleware
  go.mod
  go.sum

type ShortenRequest struct {
    URL string `json:"url" validate:"required,url"`
}

type ShortCode struct {
    Value string `json:"value" validate:"required,min=6,max=10,alphanum"`
}

type AppError struct {
    Code    string `json:"code"`
    Message string `json:"message"`
    Status  int    `json:"-"`
}

func (e *AppError) Error() string { return e.Message }

var ErrCodeNotFound = &AppError{
    Code:    "SHORT_CODE_NOT_FOUND",
    Message: "Short code not found",
    Status:  http.StatusNotFound,
}

generated/
  src/
    index.ts                    # Express app setup
    prisma/
      schema.prisma             # Prisma schema
      migrations/
        001_initial/
          migration.sql
    models/
      shortCode.ts              # TypeScript interfaces
    schemas/
      shortCode.schema.ts       # Zod validation schemas
    routes/
      shortCodes.ts             # Express routes
    services/
      shortCodeService.ts       # Business logic
    middleware/
      errorHandler.ts           # Global error handler
      validate.ts               # Zod validation middleware
    errors/
      index.ts                  # Custom error classes
  package.json
  tsconfig.json

import { z } from "zod";

export const ShortenRequestSchema = z.object({
  url: z.string().url("Must be a valid URI"),
});

export const ShortCodeParamSchema = z.object({
  code: z
    .string()
    .min(6, "Code must be at least 6 characters")
    .max(10, "Code must be at most 10 characters")
    .regex(/^[a-zA-Z0-9]+$/, "Code must be alphanumeric"),
});

generated/
  src/main/java/com/example/urlshortener/
    UrlShortenerApplication.java
    model/
      ShortCode.java                # JPA entity
    dto/
      ShortenRequest.java           # Request DTO with Bean Validation
      ShortenResponse.java          # Response DTO
    repository/
      ShortCodeRepository.java      # Spring Data JPA interface
    service/
      ShortCodeService.java         # Business logic
    controller/
      ShortCodeController.java      # REST controller
    exception/
      GlobalExceptionHandler.java   # @ControllerAdvice
      ResourceNotFoundException.java
      ConflictException.java
  src/main/resources/
    application.yml
    db/migration/
      V1__initial.sql               # Flyway migration
  pom.xml

public class ShortenRequest {
    @NotNull
    @URL(message = "Must be a valid URI")
    private String url;
}

@Entity
@Table(name = "short_codes")
public class ShortCode {
    @Id
    @GeneratedValue(strategy = GenerationType.IDENTITY)
    private Long id;

    @Column(nullable = false, length = 10)
    @Size(min = 6, max = 10)
    @Pattern(regexp = "^[a-zA-Z0-9]+$")
    private String value;
}

ConventionEngine(spec_ir: SpecIR, profile: Profile, overrides: Overrides) -> ConventionOutput

enum EntityClassification derives CanEqual:
  case Root, Child, Value, Junction

final case class EntityInfo(
    name: String,
    classification: EntityClassification,
    fields: List[FieldDecl],
    invariants: List[Expr],
    parent: Option[String],            // for child entities
    children: List[String],            // for root entities
    relations: List[RelationInfo]      // all relations involving this entity
)

enum OperationKind derives CanEqual:
  case Create, Read, Replace, PartialUpdate, Delete, CreateChild,
       FilteredRead, SideEffect, BatchMutation, Transition

final case class AnalysisSignals(
    mutatedRelations: List[String],
    preservedRelations: List[String],
    createsNewKey: Boolean,
    deletesKey: Boolean,
    targetEntityFieldCount: Option[Int],
    withFieldCount: Option[Int],
    filterParamCount: Int,
    isTransition: Boolean,
    hasCollectionInput: Boolean
)

final case class OperationClassification(
    operationName: String,
    kind: OperationKind,
    method: HttpMethod,
    matchedRule: String,        // "M1".."M10"
    targetEntity: Option[String],
    signals: AnalysisSignals
)

final case class ConventionRule(
    name: String,
    priority: Int,                                 // lower = higher priority
    appliesTo: OperationClassification => Boolean,
    apply: (OperationClassification, EntityInfo) => ConventionDecision
)

val HttpMethodRules: List[ConventionRule] = List(
  ConventionRule("M1_create",          priority = 10, appliesTo = isCreate,         apply = (_, _) => POST),
  ConventionRule("M2_read",            priority = 10, appliesTo = isRead,           apply = (_, _) => GET),
  ConventionRule("M3_update_full",     priority = 10, appliesTo = isFullUpdate,     apply = (_, _) => PUT),
  ConventionRule("M4_update_partial",  priority = 10, appliesTo = isPartialUpdate,  apply = (_, _) => PATCH),
  ConventionRule("M5_delete",          priority = 10, appliesTo = isDelete,         apply = (_, _) => DELETE),
  ConventionRule("M6_child_create",    priority =  5, appliesTo = isChildCreate,    apply = (_, _) => POST),
  ConventionRule("M7_search",          priority = 20, appliesTo = isComplexSearch,  apply = decideSearchMethod),
  ConventionRule("M8_action",          priority = 30, appliesTo = isAction,         apply = (_, _) => POST),
  ConventionRule("M9_batch",           priority = 15, appliesTo = isBatch,          apply = (_, _) => POST),
  ConventionRule("M10_transition",     priority =  5, appliesTo = isTransition,     apply = (_, _) => POST)
)

def resolve(
    property: String,
    op: OperationClassification,
    overrides: Map[String, Expr],
    profile: DeploymentProfile
): Option[String] =
  // 1. Operation-level override
  overrides.get(s"${op.operationName}.$property").flatMap(exprToString)
    // 2. Entity-level override
    .orElse(op.targetEntity.flatMap(t => overrides.get(s"$t.$property")).flatMap(exprToString))
    // 3. Global override
    .orElse(overrides.get(s"global.$property").flatMap(exprToString))
    // 4. Profile default
    .orElse(profile.defaults.get(property))
    // 5. Engine default
    .orElse(engineDefault(property, op))

final case class EndpointSpec(
    operationName: String,
    method: HttpMethod,            // GET, POST, PUT, PATCH, DELETE
    path: String,                  // /orders/{order_id}/line-items
    pathParams: List[ParamSpec],
    queryParams: List[ParamSpec],
    bodyParams: List[ParamSpec],
    successStatus: Int             // 200, 201, 204, 302
)

final case class ColumnSpec(
    name: String,
    sqlType: String,
    nullable: Boolean,
    defaultValue: Option[String]
)

final case class ForeignKeySpec(
    column: String,
    refTable: String,
    refColumn: String,
    onDelete: String
)

final case class IndexSpec(name: String, columns: List[String], unique: Boolean)

final case class TableSpec(
    name: String,
    entityName: String,
    columns: List[ColumnSpec],
    primaryKey: String,
    foreignKeys: List[ForeignKeySpec],
    checks: List[String],          // CHECK constraint SQL expressions
    indexes: List[IndexSpec]
)

final case class DatabaseSchema(tables: List[TableSpec])

conventions {
  rules {
    // Any operation whose name starts with "Admin" requires admin auth
    match: op.name starts_with "Admin"
    set: op.http_auth = "bearer"
    set: op.http_path_prefix = "/admin"
  }
}

trait ProfilePlugin:
  /** Convert generic schema to profile-specific format. */
  def transformSchema(schema: DatabaseSchema): ProfileSchema

  /** Convert generic endpoint to profile-specific route definition. */
  def transformEndpoint(endpoint: EndpointSpec): ProfileEndpoint

  /** Generate additional files (Dockerfile, config, etc.) keyed by output path. */
  def additionalArtifacts(output: ConventionOutput): Map[String, String]

test("create operation maps to POST"):
  val op     = makeOp(kind = OperationKind.Create, target = "Order")
  val result = Classify.classifyOperation(op, ir)
  assertEquals(result.method, HttpMethod.POST)

test("read operation maps to GET"):
    op = make_op(kind="read_one", target="Order")
    result = HTTP_METHOD_RULES.apply(op)
  val op2     = makeOp(kind = OperationKind.Read, target = "Order")
  val result2 = Classify.classifyOperation(op2, ir)
  assertEquals(result2.method, HttpMethod.GET)