openapi: 3.0.0
info:
  title: Lapisla Prover API
  version: 1.0.0
  description: |
    Lapisla Prover is a theorem proving assistant system with a web-based development environment and registry.

servers:
  - url: https://api.example.com/v1
    description: Production server
  - url: https://staging.api.example.com/v1
    description: Staging server

paths:
  /me/files:
    get:
      tags: 
        - me
      summary: Get metadata of all files owned by the user
      responses:
        '200':
          description: File metadata retrieved successfully
          content:
            application/json:
              schema:
                type: array
                items:
                  $ref: '#/components/schemas/PrivateFileMeta'
      security:
        - BearerAuth: []
      operationId: getMyFiles
  /me/files/{fileName}:
    post:
      tags: 
        - me
      summary: Create a new file
      parameters:
        - $ref: '#/components/parameters/fileName'
      responses:
        '201':
          description: File created successfully
          headers:
            Location:
              description: URL of the newly created file
              schema:
                type: string
                format: uri
          content: 
            application/json:
              schema:
                $ref: '#/components/schemas/PrivateFileMeta'
        '400':
          description: Invalid input
        '409':
          description: File already exists
      security:
        - BearerAuth: []
      operationId: createMyFile
      
    get:
      tags: 
        - me
      summary: Fetch a private file
      parameters:
        - $ref: '#/components/parameters/fileName'
      responses:
        '200':
          description: File
          content:
            application/json:
              schema:
                $ref: '#/components/schemas/PrivateFileMeta'
        '404':
          description: File not found
      security:
        - BearerAuth: []
      operationId: getMyFile
      
    delete:
      tags: 
        - me
      summary: Delete a file
      parameters:
        - $ref: '#/components/parameters/fileName'
      responses:
        '204':
          description: File deleted successfully
        '404':
          description: File not found
      security:
        - BearerAuth: []
      operationId: deleteMyFile
    patch:
      tags: 
        - me
      summary: Upload a snapshot of the file
      parameters:
        - $ref: '#/components/parameters/fileName'
      requestBody:
        content:
          application/json:
            schema:
              $ref: '#/components/schemas/SourceCode'
      responses:
        '200':
          description: Snapshot uploaded successfully
          content:
            application/json:
              schema:
                $ref: '#/components/schemas/SnapshotMeta'
        '404':
          description: File not found
      security:
        - BearerAuth: []
      operationId: uploadMySnapshot
  /me/files/{fileName}/{version}/register:
    post:
      tags: 
        - me
      summary: Register a snapshot to the public registry
      parameters:
        - $ref: '#/components/parameters/fileName'
        - $ref: '#/components/parameters/version'
      responses:
        '201':
          description: Snapshot registered successfully
          headers:
            Location:
              description: URL of the registered snapshot
              schema:
                type: string
                format: uri
        '400':
          description: Invalid input
        '404':
          description: File or snapshot not found
      security:
        - BearerAuth: []
      operationId: registerMySnapshot
  /me/files/{fileName}/{version}/permalink:
    post:
      tags: 
        - me
      summary: Create a permalink to the snapshot
      parameters:
        - $ref: '#/components/parameters/fileName'
        - $ref: '#/components/parameters/version'
      responses:
        '201':
          description: Permalink created successfully
          headers:
            Location:
              description: URL of the permalink
              schema:
                type: string
                format: uri
          content:
            application/json:
              schema:
                $ref: '#/components/schemas/PermalinkId'
        '404':
          description: File or snapshot not found
      security:
        - BearerAuth: []
      operationId: createMyPermalink
  
  /login:
    get:
      tags: 
        - login
      summary: Login with GitHub
      responses:
        '302':
          description: Redirect to GitHub login page
          headers:
            Location:
              description: URL of the GitHub login page
              schema:
                type: string
                format: uri
      operationId: loginWithGitHub
  /login/callback:
    get:
      tags: 
        - login
      summary: Callback for GitHub OAuth
      parameters:
        - name: code
          in: query
          required: true
          schema:
            type: string
        - name: state
          in: query
          required: true
          schema:
            type: string
      responses:
        '302':
          description: Redirect to the app
          headers:
            Location:
              description: URL of the app
              schema:
                type: string
                format: uri
      operationId: callbackGitHubOAuth

  /files/{userName}:
    get:
      tags: 
        - files
      summary: Get metadata of all public files owned by the user
      parameters:
        - $ref: '#/components/parameters/userName'
      responses:
        '200':
          description: File metadata retrieved successfully
          content:
            application/json:
              schema:
                type: array
                items:
                  $ref: '#/components/schemas/PublicFileMeta'
        '404':
          description: User not found
      operationId: getPublicFiles
  /files/{userName}/{fileName}:
    get:
      tags: 
        - files
      summary: Fetch a public file
      parameters:
        - $ref: '#/components/parameters/userName'
        - $ref: '#/components/parameters/fileName'
      responses:
        '200':
          description: File
          content:
            application/json:
              schema:
                $ref: '#/components/schemas/PublicFileMeta'
        '404':
          description: File not found
      operationId: getPublicFile
  /files/{userName}/{fileName}/{version}:
    get:
      tags: 
        - files
      summary: Fetch a public snapshot
      parameters:
        - $ref: '#/components/parameters/userName'
        - $ref: '#/components/parameters/fileName'
        - $ref: '#/components/parameters/version'
      responses:
        '200':
          description: Snapshot
          content:
            application/json:
              schema:
                $ref: '#/components/schemas/Snapshot'
        '404':
          description: Snapshot not found
      operationId: getPublicSnapshot
  /permalinks/{permalinkId}:
    get:
      tags: 
        - permalinks
      summary: Fetch a snapshot by permalink
      parameters:
        - $ref: '#/components/parameters/permalinkId'
      responses:
        '200':
          description: Snapshot
          content:
            application/json:
              schema:
                $ref: '#/components/schemas/Snapshot'
        '404':
          description: Permalink not found
      operationId: getPermalink
  /search:
    get:
      tags:
        - search
      summary: Search for public snapshots
      parameters:
        - name: q
          in: query
          required: true
          schema:
            type: string
        - name: before
          in: query
          schema:
            type: string
            format: date-time
        - name: offset
          in: query
          schema:
            type: integer
        - name: limit
          in: query
          schema:
            type: integer
          description: limit must be between 1 and 100 (default = 5)
      responses:
        '200':
          description: Search results
          content:
            application/json:
              schema:
                $ref: '#/components/schemas/SearchResult'
        '400':
          description: Invalid input
      operationId: searchSnapshots
  /registry/{snapshotId}:
    get:
      tags:
        - registry
      summary: Get the project dependencies of a snapshot
      parameters:
        - $ref: '#/components/parameters/snapshotId'
      responses:
        '200':
          description: Project dependencies retrieved successfully
          content:
            application/json:
              schema:
                $ref: '#/components/schemas/Project'
        '404':
          description: Snapshot not found
      operationId: getProjectDependencies

components:
  parameters:
    fileName:
      name: fileName
      in: path
      required: true
      schema:
        $ref: '#/components/schemas/FileName'
    version:
      name: version
      in: path
      required: true
      schema:
        $ref: '#/components/schemas/Version'
    userName:
      name: userName
      in: path
      required: true
      schema:
        $ref: '#/components/schemas/User'
    permalinkId:
      name: permalinkId
      in: path
      required: true
      schema:
        $ref: '#/components/schemas/PermalinkId'
    snapshotId:
      name: snapshotId
      in: path
      required: true
      schema:
        $ref: '#/components/schemas/SnapshotId'

  schemas:
    # common schemas
    Version:
      type: integer
    SourceCode:
      type: string
    PermalinkId:
      type: string
      pattern: '^[a-z\d](?:[a-z\d]|-(?=[a-z\d])){0,38}@[a-z\d](?:[a-z\d]|-(?=[a-z\d])){0,38}@[0-9]+$'
    SnapshotId:
      type: string
      pattern: '^[a-z\d](?:[a-z\d]|-(?=[a-z\d])){0,38}@[a-z\d](?:[a-z\d]|-(?=[a-z\d])){0,38}@[0-9]+$'
    User:
      type: string
      pattern: '/^[a-z\d](?:[a-z\d]|-(?=[a-z\d])){0,38}$/i'
    FileName:
      type: string
      pattern: '/^[a-z\d](?:[a-z\d]|-(?=[a-z\d])){0,38}$/i'
    # metadata schemas
    PrivateFileMeta:
      description: Metadata shown to the owner
      type: object
      properties:
        owner:
          $ref: '#/components/schemas/User'
        fileName:
          $ref: '#/components/schemas/FileName'
        versions:
          type: array
          items:
            $ref: '#/components/schemas/Version'
        registeredVersions:
          type: array
          items:
            $ref: '#/components/schemas/Version'
        createdAt:
          type: string
          format: date-time
        updatedAt:
          type: string
          format: date-time
      required:
        - owner
        - fileName
        - versions
        - registeredVersions
        - createdAt
        - updatedAt
    PublicFileMeta:
      description: Metadata shown to the public
      type: object
      properties:
        owner:
          $ref: '#/components/schemas/User'
        fileName:
          $ref: '#/components/schemas/FileName'
        registeredVersions:
          type: array
          items:
            $ref: '#/components/schemas/Version'
        createdAt:
          type: string
          format: date-time
        updatedAt:
          type: string
          format: date-time
      required:
        - owner
        - fileName
        - registeredVersions
        - createdAt
        - updatedAt
    SnapshotMeta:
      type: object
      properties:
        id:
          $ref: '#/components/schemas/SnapshotId'
        owner:
          $ref: '#/components/schemas/User'
        fileName:
          $ref: '#/components/schemas/FileName'
        version:
          $ref: '#/components/schemas/Version'
        registered:
          type: boolean
        createdAt:
          type: string
          format: date-time
      required:
        - id
        - owner
        - fileName
        - version
        - createdAt
    # content schemas
    PrivateFile:
      type: object
      properties:
        meta:
          $ref: '#/components/schemas/PrivateFileMeta'
        content:
          type: array
          items:
            $ref: '#/components/schemas/SourceCode'
      required:
        - meta
        - content
    PublicFile:
      type: object
      properties:
        meta:
          $ref: '#/components/schemas/PublicFileMeta'
        content:
          type: array
          items:
            $ref: '#/components/schemas/SourceCode'
      required:
        - meta
        - content
    Snapshot:
      type: object
      properties:
        meta:
          $ref: '#/components/schemas/SnapshotMeta'
        content:
          $ref: '#/components/schemas/SourceCode'
      required:
        - meta
        - content
    # search schemas
    SearchResult:
      type: object
      properties:
        before:
          type: string
          format: date-time
        offset:
          type: integer
        results:
          type: array
          items:
            $ref: '#/components/schemas/SnapshotMeta'
      required:
        - before
        - offset
        - results
    # registry schemas
    Dependency:
      type: object
      properties:
        id:
          $ref: '#/components/schemas/SnapshotId'
        snapshot:
          $ref: '#/components/schemas/Snapshot'
      required:
        - id
        - snapshot
    Project:
      type: object
      properties:
        id:
          $ref: '#/components/schemas/SnapshotId'
        dependencies:
          type: array
          items:
            $ref: '#/components/schemas/Dependency'
      required:
        - id
        - dependencies

  securitySchemes:
    GitHubAuth:
      type: oauth2
      flows:
        authorizationCode:
          authorizationUrl: https://github.com/login/oauth/authorize
          tokenUrl: https://github.com/login/oauth/access_token
          scopes:
            read:user: Read user profile data
            user:email: Read user email addresses
      description: 'OAuth 2.0 authentication'
    BearerAuth:
      type: http
      scheme: bearer
      bearerFormat: JWT