Code Generation Pipeline

"""Initial schema for UrlShortener service.

Generated by spec-to-rest compiler from the service specification.

Revision ID: 001
Create Date: 2026-04-05
"""

from alembic import op
import sqlalchemy as sa

revision = "001"
down_revision = None
branch_labels = None
depends_on = None


def upgrade() -> None:
    op.create_table(
        "short_codes",
        sa.Column("code", sa.String(length=10), nullable=False),
        sa.Column("url", sa.Text(), nullable=False),
        sa.Column("created_at", sa.DateTime(timezone=True), server_default=sa.func.now(),
                  nullable=False),
        sa.PrimaryKeyConstraint("code"),
        sa.CheckConstraint("length(code) >= 6 AND length(code) <= 10", name="ck_code_length"),
        sa.CheckConstraint("code ~ '^[a-zA-Z0-9]+$'", name="ck_code_pattern"),
        sa.CheckConstraint("url ~ '^https?://'", name="ck_url_valid_uri"),
    )
    op.create_index("ix_short_codes_created_at", "short_codes", ["created_at"])


def downgrade() -> None:
    op.drop_index("ix_short_codes_created_at", table_name="short_codes")
    op.drop_table("short_codes")

from app.models.url_shortener import Base, StoreEntry

__all__ = ["Base", "StoreEntry"]

"""SQLAlchemy ORM models for UrlShortener.

Generated from spec state declarations:
    state {
        store: ShortCode -> lone LongURL
        created_at: ShortCode -> DateTime
    }
"""

from datetime import datetime

from sqlalchemy import CheckConstraint, DateTime, String, Text, func
from sqlalchemy.orm import DeclarativeBase, Mapped, mapped_column


class Base(DeclarativeBase):
    pass


class StoreEntry(Base):
    """Represents one entry in the `store` relation: ShortCode -> lone LongURL.

    Invariants enforced at the database level:
        - len(code) >= 6 and len(code) <= 10
        - code matches [a-zA-Z0-9]+
        - url is a valid URI (basic prefix check)
    """

    __tablename__ = "store"

    code: Mapped[str] = mapped_column(
        String(10), primary_key=True, nullable=False
    )
    url: Mapped[str] = mapped_column(
        Text, nullable=False
    )
    created_at: Mapped[datetime] = mapped_column(
        DateTime(timezone=True), server_default=func.now(), nullable=False
    )

    __table_args__ = (
        CheckConstraint("length(code) >= 6 AND length(code) <= 10", name="ck_code_length"),
        CheckConstraint("code ~ '^[a-zA-Z0-9]+$'", name="ck_code_pattern"),
        CheckConstraint("url ~ '^https?://'", name="ck_url_valid_uri"),
    )

    def __repr__(self) -> str:
        return f"StoreEntry(code={self.code!r}, url={self.url!r})"

from app.schemas.url_shortener import (
    ErrorResponse,
    ShortenRequest,
    ShortenResponse,
    ResolveResponse,
)

__all__ = ["ErrorResponse", "ShortenRequest", "ShortenResponse", "ResolveResponse"]

"""Pydantic schemas for UrlShortener request/response models.

Generated from spec entity and operation declarations.
"""

import re
from datetime import datetime

from pydantic import BaseModel, Field, field_validator


class ShortenRequest(BaseModel):
    """Input schema for the Shorten operation.

    Derived from:
        operation Shorten { input: url: LongURL }
        requires: isValidURI(url.value)
    """

    url: str = Field(
        ...,
        description="The long URL to shorten",
        examples=["https://example.com/very/long/path?query=1"],
    )

    @field_validator("url")
    @classmethod
    def validate_url(cls, v: str) -> str:
        if not re.match(r"^https?://\S+$", v):
            msg = "Must be a valid HTTP or HTTPS URL"
            raise ValueError(msg)
        return v


class ShortenResponse(BaseModel):
    """Output schema for the Shorten operation.

    Derived from:
        operation Shorten { output: code: ShortCode, short_url: String }
    """

    code: str = Field(
        ...,
        min_length=6,
        max_length=10,
        pattern=r"^[a-zA-Z0-9]+$",
        description="The generated short code",
    )
    short_url: str = Field(
        ...,
        description="The full short URL (base_url + / + code)",
    )
    created_at: datetime = Field(
        ...,
        description="Timestamp when the short URL was created",
    )


class ResolveResponse(BaseModel):
    """Output schema for the Resolve operation.

    Derived from:
        operation Resolve { output: url: LongURL }
    """

    url: str = Field(..., description="The original long URL")


class ErrorResponse(BaseModel):
    """Standard error response body."""

    detail: str = Field(..., description="Human-readable error description")

"""FastAPI route handlers for UrlShortener.

Generated from spec operations via the convention engine:
    Shorten  (mutates state, has input)  -> POST /shorten
    Resolve  (reads state, no mutation)  -> GET  /{code}   (302 redirect per convention override)
    Delete   (removes from state)        -> DELETE /{code}

Convention overrides applied:
    Resolve.http_status_success = 302
    Resolve.http_header "Location" = output.url
"""

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

from app.database import get_session
from app.schemas.url_shortener import (
    ErrorResponse,
    ResolveResponse,
    ShortenRequest,
    ShortenResponse,
)
from app.services.url_shortener import UrlShortenerService

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


@router.post(
    "/shorten",
    response_model=ShortenResponse,
    status_code=201,
    responses={422: {"model": ErrorResponse, "description": "Validation error"}},
    summary="Shorten a URL",
    description="Creates a new short code mapping to the provided long URL.",
)
async def shorten(
    body: ShortenRequest,
    session: AsyncSession = Depends(get_session),
) -> ShortenResponse:
    service = UrlShortenerService(session)
    return await service.shorten(body)


@router.get(
    "/{code}",
    status_code=302,
    responses={
        302: {"description": "Redirect to the long URL"},
        404: {"model": ErrorResponse, "description": "Short code not found"},
    },
    summary="Resolve a short code",
    description="Looks up the short code and redirects to the original URL.",
)
async def resolve(
    code: str,
    session: AsyncSession = Depends(get_session),
) -> Response:
    service = UrlShortenerService(session)
    result = await service.resolve(code)
    if result is None:
        raise HTTPException(status_code=404, detail=f"Short code '{code}' not found")
    return Response(status_code=302, headers={"Location": result.url})


@router.delete(
    "/{code}",
    status_code=204,
    responses={404: {"model": ErrorResponse, "description": "Short code not found"}},
    summary="Delete a short code",
    description="Removes the short code mapping from the store.",
)
async def delete(
    code: str,
    session: AsyncSession = Depends(get_session),
) -> Response:
    service = UrlShortenerService(session)
    deleted = await service.delete(code)
    if not deleted:
        raise HTTPException(status_code=404, detail=f"Short code '{code}' not found")
    return Response(status_code=204)

"""Business logic service for UrlShortener.

Generated by spec-to-rest compiler.

For CRUD operations, the convention engine emits the implementation directly.
For non-trivial logic (e.g., short code generation), the Dafny-verified output
is integrated here. The generate_short_code function below comes from the
verified Dafny compilation; the rest is convention-engine boilerplate.
"""

import secrets
import string
from datetime import datetime, timezone

from sqlalchemy import select, delete as sa_delete
from sqlalchemy.ext.asyncio import AsyncSession

from app.config import settings
from app.models.url_shortener import StoreEntry
from app.schemas.url_shortener import (
    ResolveResponse,
    ShortenRequest,
    ShortenResponse,
)
from app.validators.url_shortener import validate_short_code, validate_long_url


# ---------------------------------------------------------------------------
# Dafny-verified short code generation
# ---------------------------------------------------------------------------
# The function below is the adapter wrapping Dafny-compiled output.
# Dafny ensures:
#   - len(result) >= 6 and len(result) <= 10
#   - result matches [a-zA-Z0-9]+
#   - result is distinct from all codes in the provided existing_codes set
#
# The Dafny source guarantees these postconditions are met for every call.
# See Section 5 (Dafny Output Integration) for the full compilation pipeline.
# ---------------------------------------------------------------------------

_ALPHABET = string.ascii_letters + string.digits  # [a-zA-Z0-9]


def generate_short_code(existing_codes: set[str], length: int = 8) -> str:
    """Generate a fresh short code not present in existing_codes.

    Verified postconditions (from Dafny):
        ensures len(result) >= 6 and len(result) <= 10
        ensures result matches [a-zA-Z0-9]+
        ensures result not in existing_codes
    """
    if length < 6 or length > 10:
        length = 8
    for _ in range(1000):
        candidate = "".join(secrets.choice(_ALPHABET) for _ in range(length))
        if candidate not in existing_codes:
            return candidate
    # Fallback: extend length within invariant bounds
    for fallback_len in range(6, 11):
        candidate = "".join(secrets.choice(_ALPHABET) for _ in range(fallback_len))
        if candidate not in existing_codes:
            return candidate
    raise RuntimeError("Failed to generate a unique short code after exhaustive attempts")


class UrlShortenerService:
    """Service layer implementing UrlShortener operations.

    Each method corresponds to a spec operation and enforces the spec's
    requires/ensures contract.
    """

    def __init__(self, session: AsyncSession) -> None:
        self._session = session

    async def shorten(self, request: ShortenRequest) -> ShortenResponse:
        """Implements operation Shorten.

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

        # Gather existing codes to satisfy the Dafny-verified uniqueness precondition
        result = await self._session.execute(select(StoreEntry.code))
        existing_codes = {row[0] for row in result.fetchall()}

        code = generate_short_code(existing_codes)

        now = datetime.now(timezone.utc)
        entry = StoreEntry(code=code, url=request.url, created_at=now)
        self._session.add(entry)
        await self._session.flush()

        short_url = f"{settings.base_url}/{code}"
        return ShortenResponse(code=code, short_url=short_url, created_at=now)

    async def resolve(self, code: str) -> ResolveResponse | None:
        """Implements operation Resolve.

        requires: code in store
        ensures:
            url = store[code]
            store' = store   (state unchanged)
        """
        validate_short_code(code)
        result = await self._session.execute(
            select(StoreEntry).where(StoreEntry.code == code)
        )
        entry = result.scalar_one_or_none()
        if entry is None:
            return None
        return ResolveResponse(url=entry.url)

    async def delete(self, code: str) -> bool:
        """Implements operation Delete.

        requires: code in store
        ensures:
            code not in store'
            #store' = #store - 1
        """
        validate_short_code(code)
        result = await self._session.execute(
            sa_delete(StoreEntry).where(StoreEntry.code == code)
        )
        return result.rowcount > 0  # type: ignore[return-value]

"""Validators derived from spec requires clauses and entity invariants.

Generated by spec-to-rest compiler.

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

import re

from fastapi import HTTPException


_SHORT_CODE_PATTERN = re.compile(r"^[a-zA-Z0-9]+$")
_URL_PATTERN = re.compile(r"^https?://\S+$")


def validate_short_code(value: str) -> None:
    """Validate a ShortCode value against entity invariants.

    Raises HTTPException 422 if invalid.
    """
    if len(value) < 6 or len(value) > 10:
        raise HTTPException(
            status_code=422,
            detail=f"Short code must be 6-10 characters, got {len(value)}",
        )
    if not _SHORT_CODE_PATTERN.match(value):
        raise HTTPException(
            status_code=422,
            detail="Short code must contain only alphanumeric characters [a-zA-Z0-9]",
        )


def validate_long_url(value: str) -> None:
    """Validate a LongURL value against entity invariants.

    Raises HTTPException 422 if invalid.
    """
    if not _URL_PATTERN.match(value):
        raise HTTPException(
            status_code=422,
            detail="URL must be a valid HTTP or HTTPS URI",
        )

// Package main is the entry point for the UrlShortener service.
//
// Generated by spec-to-rest compiler.
package main

import (
    "context"
    "fmt"
    "log/slog"
    "net/http"
    "os"
    "os/signal"
    "syscall"
    "time"

    "github.com/go-chi/chi/v5"
    "github.com/go-chi/chi/v5/middleware"

    "github.com/generated/url-shortener/internal/config"
    "github.com/generated/url-shortener/internal/database"
    "github.com/generated/url-shortener/internal/handlers"
    "github.com/generated/url-shortener/internal/services"
)

func main() {
    logger := slog.New(slog.NewJSONHandler(os.Stdout, nil))
    slog.SetDefault(logger)

    cfg, err := config.Load()
    if err != nil {
        slog.Error("failed to load config", "error", err)
        os.Exit(1)
    }

    pool, err := database.Connect(context.Background(), cfg.DatabaseURL)
    if err != nil {
        slog.Error("failed to connect to database", "error", err)
        os.Exit(1)
    }
    defer pool.Close()

    svc := services.NewUrlShortenerService(pool, cfg.BaseURL)
    h := handlers.NewUrlShortenerHandler(svc)

    r := chi.NewRouter()
    r.Use(middleware.RequestID)
    r.Use(middleware.RealIP)
    r.Use(middleware.Logger)
    r.Use(middleware.Recoverer)
    r.Use(middleware.Timeout(30 * time.Second))

    r.Get("/health", func(w http.ResponseWriter, r *http.Request) {
        w.Header().Set("Content-Type", "application/json")
        w.Write([]byte(`{"status":"ok"}`))
    })

    r.Post("/shorten", h.Shorten)
    r.Get("/{code}", h.Resolve)
    r.Delete("/{code}", h.Delete)

    server := &http.Server{
        Addr:         fmt.Sprintf(":%d", cfg.Port),
        Handler:      r,
        ReadTimeout:  10 * time.Second,
        WriteTimeout: 30 * time.Second,
        IdleTimeout:  60 * time.Second,
    }

    done := make(chan os.Signal, 1)
    signal.Notify(done, os.Interrupt, syscall.SIGTERM)

    go func() {
        slog.Info("starting server", "port", cfg.Port)
        if err := server.ListenAndServe(); err != nil && err != http.ErrServerClosed {
            slog.Error("server error", "error", err)
            os.Exit(1)
        }
    }()

    <-done
    slog.Info("shutting down")
    ctx, cancel := context.WithTimeout(context.Background(), 10*time.Second)
    defer cancel()
    _ = server.Shutdown(ctx)
}

// Package config loads application configuration from environment variables.
//
// Generated by spec-to-rest compiler.
package config

import "github.com/caarlos0/env/v11"

type Config struct {
    DatabaseURL string `env:"DATABASE_URL" envDefault:"postgres://shortener:shortener@localhost:5432/shortener?sslmode=disable"`
    BaseURL     string `env:"BASE_URL"     envDefault:"http://localhost:8080"`
    Port        int    `env:"PORT"         envDefault:"8080"`
    LogLevel    string `env:"LOG_LEVEL"    envDefault:"info"`
}

func Load() (*Config, error) {
    cfg := &Config{}
    if err := env.Parse(cfg); err != nil {
        return nil, err
    }
    return cfg, nil
}

// Package models defines data types for UrlShortener.
//
// Generated from spec entity and state declarations.
package models

import "time"

// StoreEntry represents one row of the `store` relation: ShortCode -> lone LongURL.
type StoreEntry struct {
    Code      string    `json:"code"       db:"code"`
    URL       string    `json:"url"        db:"url"`
    CreatedAt time.Time `json:"created_at" db:"created_at"`
}

// ShortenRequest is the input for operation Shorten.
type ShortenRequest struct {
    URL string `json:"url"`
}

// ShortenResponse is the output for operation Shorten.
type ShortenResponse struct {
    Code      string    `json:"code"`
    ShortURL  string    `json:"short_url"`
    CreatedAt time.Time `json:"created_at"`
}

// ErrorResponse is the standard error body.
type ErrorResponse struct {
    Detail string `json:"detail"`
}

// Package handlers contains HTTP route handlers for UrlShortener.
//
// Generated from spec operations via the convention engine.
package handlers

import (
    "encoding/json"
    "net/http"

    "github.com/go-chi/chi/v5"

    "github.com/generated/url-shortener/internal/models"
    "github.com/generated/url-shortener/internal/services"
    "github.com/generated/url-shortener/internal/validators"
)

type UrlShortenerHandler struct {
    svc *services.UrlShortenerService
}

func NewUrlShortenerHandler(svc *services.UrlShortenerService) *UrlShortenerHandler {
    return &UrlShortenerHandler{svc: svc}
}

func (h *UrlShortenerHandler) Shorten(w http.ResponseWriter, r *http.Request) {
    var req models.ShortenRequest
    if err := json.NewDecoder(r.Body).Decode(&req); err != nil {
        writeError(w, http.StatusBadRequest, "Invalid JSON body")
        return
    }

    if err := validators.ValidateLongURL(req.URL); err != nil {
        writeError(w, http.StatusUnprocessableEntity, err.Error())
        return
    }

    resp, err := h.svc.Shorten(r.Context(), req)
    if err != nil {
        writeError(w, http.StatusInternalServerError, "Failed to shorten URL")
        return
    }

    w.Header().Set("Content-Type", "application/json")
    w.WriteHeader(http.StatusCreated)
    json.NewEncoder(w).Encode(resp)
}

func (h *UrlShortenerHandler) Resolve(w http.ResponseWriter, r *http.Request) {
    code := chi.URLParam(r, "code")
    if err := validators.ValidateShortCode(code); err != nil {
        writeError(w, http.StatusUnprocessableEntity, err.Error())
        return
    }

    entry, err := h.svc.Resolve(r.Context(), code)
    if err != nil {
        writeError(w, http.StatusInternalServerError, "Failed to resolve code")
        return
    }
    if entry == nil {
        writeError(w, http.StatusNotFound, "Short code not found")
        return
    }

    // Convention override: Resolve.http_status_success = 302
    http.Redirect(w, r, entry.URL, http.StatusFound)
}

func (h *UrlShortenerHandler) Delete(w http.ResponseWriter, r *http.Request) {
    code := chi.URLParam(r, "code")
    if err := validators.ValidateShortCode(code); err != nil {
        writeError(w, http.StatusUnprocessableEntity, err.Error())
        return
    }

    deleted, err := h.svc.Delete(r.Context(), code)
    if err != nil {
        writeError(w, http.StatusInternalServerError, "Failed to delete code")
        return
    }
    if !deleted {
        writeError(w, http.StatusNotFound, "Short code not found")
        return
    }

    w.WriteHeader(http.StatusNoContent)
}

func writeError(w http.ResponseWriter, status int, detail string) {
    w.Header().Set("Content-Type", "application/json")
    w.WriteHeader(status)
    json.NewEncoder(w).Encode(models.ErrorResponse{Detail: detail})
}

// Package services contains business logic for UrlShortener.
//
// Generated by spec-to-rest compiler.
package services

import (
    "context"
    "crypto/rand"
    "errors"
    "fmt"
    "math/big"
    "time"

    "github.com/jackc/pgx/v5"
    "github.com/jackc/pgx/v5/pgxpool"

    "github.com/generated/url-shortener/internal/models"
)

const alphabet = "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789"

type UrlShortenerService struct {
    pool    *pgxpool.Pool
    baseURL string
}

func NewUrlShortenerService(pool *pgxpool.Pool, baseURL string) *UrlShortenerService {
    return &UrlShortenerService{pool: pool, baseURL: baseURL}
}

// generateShortCode produces a fresh alphanumeric code of the given length.
// Dafny-verified postconditions:
//   - len(result) >= 6 && len(result) <= 10
//   - result matches [a-zA-Z0-9]+
//   - result is not in the current store
func generateShortCode(length int) (string, error) {
    if length < 6 || length > 10 {
        length = 8
    }
    b := make([]byte, length)
    for i := range b {
        n, err := rand.Int(rand.Reader, big.NewInt(int64(len(alphabet))))
        if err != nil {
            return "", fmt.Errorf("crypto/rand failed: %w", err)
        }
        b[i] = alphabet[n.Int64()]
    }
    return string(b), nil
}

func (s *UrlShortenerService) Shorten(ctx context.Context, req models.ShortenRequest) (*models.ShortenResponse, error) {
    // Retry loop to guarantee code uniqueness (Dafny postcondition: code not in pre(store))
    for attempts := 0; attempts < 10; attempts++ {
        code, err := generateShortCode(8)
        if err != nil {
            return nil, err
        }

        now := time.Now().UTC()
        tag, err := s.pool.Exec(ctx,
            `INSERT INTO store (code, url, created_at) VALUES ($1, $2, $3) ON CONFLICT (code) DO NOTHING`,
            code, req.URL, now,
        )
        if err != nil {
            return nil, fmt.Errorf("insert failed: %w", err)
        }
        if tag.RowsAffected() == 1 {
            return &models.ShortenResponse{
                Code:      code,
                ShortURL:  fmt.Sprintf("%s/%s", s.baseURL, code),
                CreatedAt: now,
            }, nil
        }
        // Conflict: code already exists, retry with new code
    }
    return nil, fmt.Errorf("failed to generate unique short code after 10 attempts")
}

func (s *UrlShortenerService) Resolve(ctx context.Context, code string) (*models.StoreEntry, error) {
    row := s.pool.QueryRow(ctx, `SELECT code, url, created_at FROM store WHERE code = $1`, code)
    var entry models.StoreEntry
    err := row.Scan(&entry.Code, &entry.URL, &entry.CreatedAt)
    if err != nil {
        if errors.Is(err, pgx.ErrNoRows) {
            return nil, nil
        }
        return nil, fmt.Errorf("query failed: %w", err)
    }
    return &entry, nil
}

func (s *UrlShortenerService) Delete(ctx context.Context, code string) (bool, error) {
    tag, err := s.pool.Exec(ctx, `DELETE FROM store WHERE code = $1`, code)
    if err != nil {
        return false, fmt.Errorf("delete failed: %w", err)
    }
    return tag.RowsAffected() > 0, nil
}

/** Express route handlers for UrlShortener.
 *
 * Generated from spec operations via the convention engine.
 */

import { Router, type Request, type Response } from "express";
import { ShortenRequestSchema, ShortCodeSchema } from "../validators/urlShortener";
import * as service from "../services/urlShortener";

export const urlShortenerRouter = Router();

// POST /shorten — operation Shorten (mutates state, has input)
urlShortenerRouter.post("/shorten", async (req: Request, res: Response) => {
  const parsed = ShortenRequestSchema.safeParse(req.body);
  if (!parsed.success) {
    res.status(422).json({ detail: parsed.error.issues[0].message });
    return;
  }

  try {
    const result = await service.shorten(parsed.data);
    res.status(201).json(result);
  } catch (err) {
    console.error("Shorten error:", err);
    res.status(500).json({ detail: "Failed to shorten URL" });
  }
});

// GET /:code — operation Resolve (reads state, no mutation; convention override: 302)
urlShortenerRouter.get("/:code", async (req: Request, res: Response) => {
  const parsed = ShortCodeSchema.safeParse(req.params.code);
  if (!parsed.success) {
    res.status(422).json({ detail: parsed.error.issues[0].message });
    return;
  }

  try {
    const result = await service.resolve(parsed.data);
    if (!result) {
      res.status(404).json({ detail: "Short code not found" });
      return;
    }
    // Convention override: Resolve.http_status_success = 302
    res.redirect(302, result.url);
  } catch (err) {
    console.error("Resolve error:", err);
    res.status(500).json({ detail: "Failed to resolve code" });
  }
});

// DELETE /:code — operation Delete (removes from state)
urlShortenerRouter.delete("/:code", async (req: Request, res: Response) => {
  const parsed = ShortCodeSchema.safeParse(req.params.code);
  if (!parsed.success) {
    res.status(422).json({ detail: parsed.error.issues[0].message });
    return;
  }

  try {
    const deleted = await service.deleteCode(parsed.data);
    if (!deleted) {
      res.status(404).json({ detail: "Short code not found" });
      return;
    }
    res.status(204).end();
  } catch (err) {
    console.error("Delete error:", err);
    res.status(500).json({ detail: "Failed to delete code" });
  }
});

/** Business logic service for UrlShortener.
 *
 * Generated by spec-to-rest compiler.
 */

import { PrismaClient } from "@prisma/client";
import crypto from "node:crypto";
import { config } from "../config";
import type { ShortenRequest, ShortenResponse, ResolveResponse } from "../types/urlShortener";

const ALPHABET = "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789";

const prisma = new PrismaClient();

/**
 * Generate a fresh short code.
 *
 * Dafny-verified postconditions:
 *   - length >= 6 && length <= 10
 *   - matches /^[a-zA-Z0-9]+$/
 */
function generateShortCode(length: number = 8): string {
  const clampedLen = Math.max(6, Math.min(10, length));
  const bytes = crypto.randomBytes(clampedLen);
  let result = "";
  for (let i = 0; i < clampedLen; i++) {
    result += ALPHABET[bytes[i] % ALPHABET.length];
  }
  return result;
}

export async function shorten(req: ShortenRequest): Promise<ShortenResponse> {
  for (let attempt = 0; attempt < 10; attempt++) {
    const code = generateShortCode(8);
    try {
      const entry = await prisma.store.create({
        data: { code, url: req.url },
      });
      return {
        code: entry.code,
        short_url: `${config.baseUrl}/${entry.code}`,
        created_at: entry.createdAt.toISOString(),
      };
    } catch (err: unknown) {
      // Unique constraint violation — retry with new code
      if (isPrismaUniqueViolation(err)) continue;
      throw err;
    }
  }
  throw new Error("Failed to generate unique short code after 10 attempts");
}

export async function resolve(code: string): Promise<ResolveResponse | null> {
  const entry = await prisma.store.findUnique({ where: { code } });
  if (!entry) return null;
  return { url: entry.url };
}

export async function deleteCode(code: string): Promise<boolean> {
  try {
    await prisma.store.delete({ where: { code } });
    return true;
  } catch (err: unknown) {
    if (isPrismaNotFound(err)) return false;
    throw err;
  }
}

function isPrismaUniqueViolation(err: unknown): boolean {
  return (err as { code?: string })?.code === "P2002";
}

function isPrismaNotFound(err: unknown): boolean {
  return (err as { code?: string })?.code === "P2025";
}

/** Validators derived from spec requires clauses and entity invariants.
 *
 * Generated by spec-to-rest compiler.
 */

import { z } from "zod";

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

export const LongURLSchema = z
  .string()
  .regex(/^https?:\/\/\S+$/, "Must be a valid HTTP or HTTPS URL");

export const ShortenRequestSchema = z.object({
  url: LongURLSchema,
});

/** Request/response types for UrlShortener.
 *
 * Generated from spec entity and operation declarations.
 */

export interface ShortenRequest {
  url: string;
}

export interface ShortenResponse {
  code: string;
  short_url: string;
  created_at: string;
}

export interface ResolveResponse {
  url: string;
}

export interface ErrorResponse {
  detail: string;
}