openapi: 3.1.0
info:
  title: Formagine API
  version: 0.1.0
  description: |
    Algebraic smart contract compiler. Define verified Forms — algebraic types
    with embedded invariants — and compile them to optimized WASM for deployment
    on CosmWasm, Near, Stylus, and Polkadot.

    Forms are proven correct at compile time. If it compiles, every invariant
    holds for all possible executions.
  contact:
    email: api@formagine.com
    url: https://formagine.com
  license:
    name: Proprietary
    url: https://formagine.com/terms

servers:
  - url: https://formagine.com/api
    description: Production

paths:
  /verify:
    post:
      operationId: verifyForm
      summary: Verify a Form definition
      description: |
        Accepts a Form definition and algebraically verifies all invariants
        against all transitions. Returns a proof report or rejection with
        counterexample. Free — no authentication required.
      requestBody:
        required: true
        content:
          application/json:
            schema:
              $ref: '#/components/schemas/FormDefinition'
      responses:
        '200':
          description: Verification complete
          content:
            application/json:
              schema:
                $ref: '#/components/schemas/VerificationReport'
        '400':
          description: Malformed Form definition
          content:
            application/json:
              schema:
                $ref: '#/components/schemas/Error'

  /build:
    post:
      operationId: buildForm
      summary: Compile a verified Form to WASM
      description: |
        Accepts a Form definition and target chain. Verifies, compiles, and
        returns an optimized WASM artifact. Requires membership authentication.
      security:
        - bearerAuth: []
      requestBody:
        required: true
        content:
          application/json:
            schema:
              $ref: '#/components/schemas/BuildRequest'
      responses:
        '200':
          description: Compilation successful
          content:
            application/json:
              schema:
                $ref: '#/components/schemas/BuildArtifact'
        '400':
          description: Malformed request
          content:
            application/json:
              schema:
                $ref: '#/components/schemas/Error'
        '402':
          description: Membership required
          content:
            application/json:
              schema:
                $ref: '#/components/schemas/Error'
        '422':
          description: Verification failed — Form has invariant violations
          content:
            application/json:
              schema:
                $ref: '#/components/schemas/VerificationReport'

  /forms:
    get:
      operationId: listTemplates
      summary: List base Form templates
      description: |
        Returns the catalog of base Form templates: Token, Vault, Escrow,
        Governor, Marketplace. Each template includes default state variables,
        invariants, and transitions that can be customized.
      responses:
        '200':
          description: Template catalog
          content:
            application/json:
              schema:
                type: array
                items:
                  $ref: '#/components/schemas/FormTemplate'

  /chains:
    get:
      operationId: listChains
      summary: List supported target chains
      description: Returns supported WASM-compatible chains and their runtime specs.
      responses:
        '200':
          description: Chain catalog
          content:
            application/json:
              schema:
                type: array
                items:
                  $ref: '#/components/schemas/ChainTarget'

  /explain:
    post:
      operationId: explainForm
      summary: Explain a Form in plain language
      description: |
        Accepts a Form definition and returns a human-readable explanation
        of its behavior, guarantees, and what the invariants protect against.
      requestBody:
        required: true
        content:
          application/json:
            schema:
              $ref: '#/components/schemas/FormDefinition'
      responses:
        '200':
          description: Explanation
          content:
            application/json:
              schema:
                $ref: '#/components/schemas/Explanation'

components:
  securitySchemes:
    bearerAuth:
      type: http
      scheme: bearer
      description: Membership API key

  schemas:
    StateVariable:
      type: object
      required: [name, type]
      properties:
        name:
          type: string
          example: balance
        type:
          type: string
          enum: [Nat, Int, Bool, Address, Bytes, String]
          example: Nat
        per:
          type: string
          description: Creates a mapping from this type to the variable type
          example: Address
        parameterized:
          type: string
          description: For Map, Set, List, Option types
          example: "Map(Address, Nat)"

    Invariant:
      type: object
      required: [name, expr]
      properties:
        name:
          type: string
          example: conservation
        expr:
          type: string
          description: Algebraic expression that must hold across all transitions
          example: "sum(balance) == supply"

    Transition:
      type: object
      required: [name, params, updates]
      properties:
        name:
          type: string
          example: transfer
        params:
          type: array
          items:
            type: object
            required: [name, type]
            properties:
              name:
                type: string
              type:
                type: string
        requires:
          type: array
          items:
            type: string
          description: Preconditions (runtime guards)
          example: ["balance[from] >= amount"]
        updates:
          type: array
          items:
            type: string
          description: State mutations
          example: ["balance[from] -= amount", "balance[to] += amount"]

    FormDefinition:
      type: object
      required: [name, state, invariants, transitions]
      properties:
        name:
          type: string
          example: Token
        state:
          type: array
          items:
            $ref: '#/components/schemas/StateVariable'
        invariants:
          type: array
          items:
            $ref: '#/components/schemas/Invariant'
        transitions:
          type: array
          items:
            $ref: '#/components/schemas/Transition'

    VerificationReport:
      type: object
      required: [status, form, invariants]
      properties:
        status:
          type: string
          enum: [verified, rejected]
        form:
          type: string
        invariants:
          type: array
          items:
            type: object
            properties:
              name:
                type: string
              result:
                type: string
                enum: [proven, violated]
              method:
                type: string
              detail:
                type: string
              counterexample:
                type: object
        transitions_checked:
          type: integer
        proof_time_ms:
          type: integer

    BuildRequest:
      type: object
      required: [form, target]
      properties:
        form:
          $ref: '#/components/schemas/FormDefinition'
        target:
          type: string
          enum: [cosmwasm, near, stylus, polkadot]
        options:
          type: object
          properties:
            optimize:
              type: boolean
              default: true
            debug_names:
              type: boolean
              default: false

    BuildArtifact:
      type: object
      properties:
        status:
          type: string
          enum: [compiled]
        artifact:
          type: object
          properties:
            wasm_base64:
              type: string
            wasm_size_bytes:
              type: integer
            target:
              type: string
            checksum:
              type: string
            invariants_erased:
              type: integer
            runtime_guards:
              type: integer
        verification:
          $ref: '#/components/schemas/VerificationReport'

    FormTemplate:
      type: object
      properties:
        name:
          type: string
        description:
          type: string
        default_state:
          type: array
          items:
            $ref: '#/components/schemas/StateVariable'
        default_invariants:
          type: array
          items:
            $ref: '#/components/schemas/Invariant'
        default_transitions:
          type: array
          items:
            $ref: '#/components/schemas/Transition'

    ChainTarget:
      type: object
      properties:
        id:
          type: string
        name:
          type: string
        runtime:
          type: string
        max_wasm_size_bytes:
          type: integer
        documentation_url:
          type: string

    Explanation:
      type: object
      properties:
        summary:
          type: string
        state_description:
          type: string
        invariant_descriptions:
          type: array
          items:
            type: object
            properties:
              name:
                type: string
              plain_english:
                type: string
        transition_descriptions:
          type: array
          items:
            type: object
            properties:
              name:
                type: string
              plain_english:
                type: string

    Error:
      type: object
      properties:
        error:
          type: string
        detail:
          type: string