# Get submission spec

```http
GET /api/public/v1/competitions/lean-kernel-challenge/submission-spec
```

**Scope**: `competition.read`.

Returns the current formal source contract, pinned rules, supported Problems, and limits required to create a Lean Kernel submission.

## Response fields

| Field | Type and meaning |
| :--- | :--- |
| `kind` | `"lean-kernel-package"` — Submission discriminator for this competition. |
| `competitionId` | `"lean-kernel-challenge"` — Competition identifier. |
| `contractVersion` | `string` — Opaque version for the current rules and Problem workspaces. Pass it through unchanged when submitting. |
| `problems` | `string[]` — Ordered Problem IDs supported by this contract. Membership and order match [List problems](./list-problems.md); check each Problem's `availability` before creating a submission. |
| `requiredSubmissionShape` | [`RequiredSubmissionShape`](#requiredsubmissionshape) — Declarations required in `Submission.lean`. |
| `rulesDocs` | [`RulesDocs`](#rulesdocs) — Rules pages pinned to `contractVersion`. |
| `source` | [`SubmissionSource`](#submissionsource) — Logical one-file shape represented by `payload.text` when submitting. |
| `limits` | [`SubmissionLimits`](#submissionlimits) — Current source and team limits. |

### RequiredSubmissionShape

| Field | Type and meaning |
| :--- | :--- |
| `functionName` | `"impl"` — Required implementation declaration name. |
| `proofName` | `"impl_correct"` — Required correctness proof declaration name. |
| `proofForm` | `"forall n, impl n = spec n"` — Schematic proof form. The concrete input, output, and specification declaration come from the selected Problem workspace. |

### RulesDocs

| Field | Type and meaning |
| :--- | :--- |
| `overview` | `string` — Absolute URL for the overview pinned to `contractVersion`. |
| `evaluation` | `string` — Absolute URL for the evaluation rules pinned to `contractVersion`. |

### SubmissionSource

| Field | Type and meaning |
| :--- | :--- |
| `requiredRoot` | `"Submission.lean"` — Logical filename assigned to the submitted Lean text. |
| `extensions` | `string[]` — Accepted logical source extensions; currently only `".lean"`. |

### SubmissionLimits

| Field | Type and meaning |
| :--- | :--- |
| `maxUploadBytes` | `integer` — Maximum decoded UTF-8 byte size of `payload.text`; currently `1048576` (1 MiB). The field name is retained by the machine-readable contract. |
| `maxPackageFiles` | `integer` — Maximum participant files in a formal submission; currently `1`. |
| `maxTeamSize` | `integer` — Current competition team headcount limit, including the team owner. |

## Example request

```bash
export SAIR_API_BASE="https://api.sair.foundation/api/public/v1"

curl "$SAIR_API_BASE/competitions/lean-kernel-challenge/submission-spec" \
  -H "Authorization: Bearer $SAIR_API_KEY"
```

## Example response

The version, Problem list, links, and limits below are illustrative. Always use the live response.

```json
{
  "ok": true,
  "data": {
    "kind": "lean-kernel-package",
    "competitionId": "lean-kernel-challenge",
    "contractVersion": "7a0abb4a80d635740a91aed1894f714dfbb82edd",
    "problems": [
      "fib",
      "partition",
      "mertens",
      "primecount",
      "permanent",
      "saw",
      "ca-rule110",
      "sha256",
      "polydisc"
    ],
    "requiredSubmissionShape": {
      "functionName": "impl",
      "proofName": "impl_correct",
      "proofForm": "forall n, impl n = spec n"
    },
    "rulesDocs": {
      "overview": "https://github.com/SAIRcompetition/lean-kernel-challenge/blob/7a0abb4a80d635740a91aed1894f714dfbb82edd/rules/overview.md",
      "evaluation": "https://github.com/SAIRcompetition/lean-kernel-challenge/blob/7a0abb4a80d635740a91aed1894f714dfbb82edd/rules/evaluation.md"
    },
    "source": {
      "requiredRoot": "Submission.lean",
      "extensions": [".lean"]
    },
    "limits": {
      "maxUploadBytes": 1048576,
      "maxPackageFiles": 1,
      "maxTeamSize": 5
    }
  }
}
```

## Using the contract

1. Read this endpoint immediately before a formal submission. Do not cache `contractVersion` as an application constant.
2. Select an `available` Problem from [List problems](./list-problems.md) and use its pinned workspace for the concrete declarations and starter files.
3. Submit exactly one non-empty Lean source string as `payload.text` within the live byte limit.
4. Pass `contractVersion` through unchanged as `contractVersionAcknowledged` in [Submit a Lean file](./submit-package.md).
5. If submission returns `RULE_VERSION_MISMATCH`, discard the stale value, read this endpoint again, review the new pinned rules, and retry the same logical submission with the same idempotency key.

`contractVersion` is a transport value for snapshot consistency. Do not parse it, hardcode it, or present it as a participant-facing confirmation. In a valid response, the Problem IDs, rules links, and current approved Problem workspaces belong to the same contract revision.

## Errors

| HTTP | Code | When |
| :---: | :--- | :--- |
| `404` | `NOT_FOUND` | The competition is not publicly visible. |
| `404` | `DISCOVERY_NOT_LAUNCHED` | The submission contract is not public yet. |
| `502` | `PLATFORM_UNAVAILABLE` | Competition visibility or the current team limit cannot be verified. |
| `502` | `SERVICE_UNAVAILABLE` | The authoritative Lean Kernel service or its current contract is unavailable or inconsistent. |

See [Errors](../../../errors.md) for shared authentication, scope, and rate-limit errors.