# Submit a Lean file

```http
POST /api/public/v1/competitions/lean-kernel-challenge/submissions
Content-Type: application/json
```

**Scope**: `competition.write`.

Creates an immutable formal submission for one Lean Kernel Problem. The request contains the exact text of one `Submission.lean`; this operation does not accept multipart bodies, uploaded files, saved-Solution IDs, auxiliary files, or archives.

The caller must have a verified email, be enrolled, have a current effective entrant, and submit during the open submission window. An individual entrant submits for themselves. Any active member of a team entrant may submit for that team. Use [Get my participation](./get-my-participation.md) as a preflight; this endpoint rechecks all mutable conditions.

## Request body

Send UTF-8 `application/json` with this shape:

```ts
type SubmitLeanFileRequest = {
  idempotencyKey: string;
  contractVersionAcknowledged: string;
  payload: {
    problem: string;
    text: string;
  };
  meta?: {
    description?: string;
  };
};
```

| Field | Type, requirement, and meaning |
| :--- | :--- |
| `idempotencyKey` | **Required string.** Client-generated key for this logical submission. After trimming, it must contain at least one character and be at most 200 UTF-8 bytes. |
| `contractVersionAcknowledged` | **Required string.** Current opaque `contractVersion` returned by [Get submission spec](./get-submission-spec.md). Pass it through unchanged. |
| `payload` | **Required object.** Contains only `problem` and `text`. |
| `payload.problem` | **Required string.** Exact, case-sensitive ID of an `available` Problem returned by [List problems](./list-problems.md). |
| `payload.text` | **Required string.** Complete non-empty `Submission.lean` source. Its decoded UTF-8 byte length must not exceed the live `limits.maxUploadBytes`. |
| `meta` | **Optional object.** Contains only `description`; it cannot be `null`. |
| `meta.description` | **Optional string.** Submission note of at most 5,000 Unicode code points after trimming. Empty or whitespace-only text is omitted from the response. |

Unknown fields are rejected. JSON escaping is transport syntax only: size limits and hashes apply to the UTF-8 bytes of the decoded `payload.text`. The source must not depend on auxiliary files from a Playground Workspace.

## Idempotency

Generate one opaque `idempotencyKey` for each intended submission. The key is scoped to the current effective entrant and identifies the complete normalized request: Problem, source text, description, and acknowledged contract version.

- The first successful creation returns `201 Created`.
- Retrying the same request with the same key returns the stored submission with `200 OK`. It does not create another history row, consume another daily submission, or change candidate ordering.
- Reusing a stored key with a different request returns `409 IDEMPOTENCY_CONFLICT`.

After a timeout, lost response, or transient `5xx`, retry the exact request with the same key. If the endpoint returns `RULE_VERSION_MISMATCH`, reload the submission spec, review the new pinned rules, update only `contractVersionAcknowledged`, and retry the same logical submission with the same key.

## Example request

Read the current submission spec immediately before submitting. The following command preserves the Lean source as one JSON string without using multipart:

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

SAIR_LEAN_KERNEL_CONTRACT_VERSION="$(
  curl -fsS "$SAIR_API_BASE/competitions/lean-kernel-challenge/submission-spec" \
    -H "Authorization: Bearer $SAIR_API_KEY" \
    | jq -r '.data.contractVersion'
)"
SAIR_IDEMPOTENCY_KEY="lkc-fib-$(openssl rand -hex 16)"

jq -n \
  --arg key "$SAIR_IDEMPOTENCY_KEY" \
  --arg contract "$SAIR_LEAN_KERNEL_CONTRACT_VERSION" \
  --rawfile source ./Submission.lean \
  '{
    idempotencyKey: $key,
    contractVersionAcknowledged: $contract,
    payload: { problem: "fib", text: $source },
    meta: { description: "Fast-doubling candidate" }
  }' |
curl -X POST "$SAIR_API_BASE/competitions/lean-kernel-challenge/submissions" \
  -H "Authorization: Bearer $SAIR_API_KEY" \
  -H "Content-Type: application/json" \
  --data-binary @-
```

Do not send a multipart form and do not substitute `solutionId` for `payload.text`.

## Response

```ts
type SubmitLeanFileResponse = {
  ok: true;
  data: {
    submissionId: string;
    status: "submitted";
    note?: string;
    contractVersion: string;
    snapshotId: string;
    canonicalSourceTreeSha256: string;
    rawUploadSha256: string;
    manifestSha256: string;
  };
};
```

| Field | Meaning |
| :--- | :--- |
| `submissionId` | Stable formal-submission ID used by history, downloads, and published results. |
| `status` | `submitted` means the immutable formal submission exists and formal evaluation has not started. |
| `note` | Stored `meta.description`; omitted when no non-empty description was supplied. |
| `contractVersion` | Contract version recorded with the source snapshot. |
| `snapshotId` | Stable ID of the immutable source snapshot. |
| `canonicalSourceTreeSha256` | SHA-256 digest of the canonical one-file source-tree representation. |
| `rawUploadSha256` | SHA-256 digest of the decoded `payload.text` UTF-8 bytes. |
| `manifestSha256` | SHA-256 digest of the canonical source manifest. |

```json
{
  "ok": true,
  "data": {
    "submissionId": "42",
    "status": "submitted",
    "note": "Fast-doubling candidate",
    "contractVersion": "7a0abb4a80d635740a91aed1894f714dfbb82edd",
    "snapshotId": "42",
    "canonicalSourceTreeSha256": "8c04fd5b1f4c20a1dfd19cb46bcb4aa12c589712e072024920d444852a17ff05",
    "rawUploadSha256": "9d72b952efa332d915c3dd7f27adc6028f4c85b68d910570208b7377e169fa48",
    "manifestSha256": "24fcb69b9f98ac0d67bdab4ff6e5f03b0bbbd772e63a78bdd6db460fce3f275d"
  }
}
```

## Candidate and evaluation behavior

A successful creation becomes the newest active candidate for the current entrant and Problem. The server retains at most the live `activeCandidateLimit` returned by [Get my participation](./get-my-participation.md). After the cutoff, the platform freezes the latest eligible active candidate for formal evaluation. Playground checks are not formal results.

## Errors

### Request and source

- `400 MALFORMED_BODY` — The media type is not `application/json`, the JSON is invalid, or the request shape or field types are invalid.
- `400 MISSING_FIELD` — A required request field is missing.
- `400 RULE_ACK_REQUIRED` — `contractVersionAcknowledged` is missing or empty.
- `400 IDEMPOTENCY_KEY_REQUIRED` — `idempotencyKey` is missing or empty after trimming.
- `400 IDEMPOTENCY_KEY_TOO_LONG` — `idempotencyKey` exceeds 200 UTF-8 bytes after trimming.
- `400 NOTE_TOO_LONG` — `meta.description` exceeds 5,000 Unicode code points.
- `400 SUBMISSION_REJECTED` — The Problem or another service-validated request field is invalid.
- `413 FILE_TOO_LARGE` — The decoded `payload.text` exceeds the live `limits.maxUploadBytes`.
- `422 PACKAGE_INVALID` — `payload.text` is empty or violates the single-file Lean source contract.

### Eligibility and conflicts

- `403 EMAIL_NOT_VERIFIED` — The caller's email is not verified.
- `403 ENROLL_REQUIRED` — The caller has not completed enrollment.
- `403 TEAM_REQUIRED` — The participant context has no current effective entrant.
- `403 SUBMISSION_WINDOW_NOT_OPEN` — The submission window has not opened or is not configured.
- `403 SUBMISSION_WINDOW_CLOSED` — The submission window or competition has closed.
- `403 SUBMISSION_NOT_ALLOWED` — Another participant-context rule blocks formal submission.
- `404 NOT_FOUND` — The competition does not exist or is not publicly visible.
- `409 PROBLEM_UNAVAILABLE` — The selected Problem is not currently available.
- `409 IDEMPOTENCY_CONFLICT` — The same stored `idempotencyKey` identifies a different normalized request.
- `409 RULE_VERSION_MISMATCH` — The acknowledged contract version is no longer current.
- `429 DAILY_SUBMISSION_LIMIT_EXCEEDED` — The current entrant has reached the UTC-day formal-submission limit.

### Service failures

- `502 PLATFORM_UNAVAILABLE` — Formal eligibility could not be verified with the platform service.
- `502 PLATFORM_RESPONSE_INVALID` — The platform returned an invalid participant context or candidate limit.
- `502 SERVICE_UNAVAILABLE` — The authoritative Lean Kernel service or its current contract is unavailable.
- `503 DATABASE_BUSY` — Submission processing is temporarily busy; retry the exact request with the same idempotency key.

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