# Palomar A registry of machine-checked Lean 4 proofs. This host, `submit.palomar-registry.org`, is the only way in. The registry itself is at https://palomar-registry.org. ## Read these first, rather than inferring the rules from this file - Submission policy, what is required of a repository, and what review looks for: https://github.com/PalomarRegistry/PalomarPolicy/blob/main/CONTRIBUTING.md - Repository, review, registration, and publication contract: https://github.com/PalomarRegistry/PalomarPolicy/blob/main/docs/specification.md - The `formalization.yaml` self-reporting format, which a submission must carry: https://github.com/mathlib-initiative/formalization.yaml Nothing about eligibility, metadata, or scoring is restated here. If this file and the policy disagree, the policy is right. ## You may submit, but not by signing in as your user Submitting requires proving that whoever submits can write to the repository being submitted. There are two ways to prove it, and you may drive exactly one. **Do not drive the browser sign-in.** Not with browser automation, not with a stored session, not with credentials your user has given you for other purposes. That flow establishes that a particular person authorised Palomar; an agent completing it makes the record say something false. **You may use the `gh` path below**, which proves the same write access without a browser, from an authenticated `gh`. Confirm with your user first. Show them the repository, the commit, the Comparator configuration path, and which answer you will give for their relationship to the formalization, and get their agreement. The last of those is a claim about *them*, not about the code, and it is recorded permanently. ### The steps, and why there are five 1. POST /api/submit {"repository": "...", "commit": "<40 hex>", "comparator_config_path": "...", "authorization_relationship": "maintainer", "existing_id": "PALOMAR-YYYY-MM-DD-NNNNNN (only for a new version)"} -> {"pending_secret": "...", "challenge": "...", "instructions": "..."} 2. gh api -X POST repos/OWNER/REPO/git/refs \ -f ref=refs/tags/palomar-verify-CHALLENGE -f sha=COMMIT 3. echo '{"public":false,"files":{"palomar.txt":{"content":"CHALLENGE"}}}' \ | gh api -X POST gists --input - 4. POST /api/verify {"pending_secret": "...", "gist_id": "..."} -> {"submission_id": "...", "access_token": "..."} The gist must be secret, and must not predate the intake by more than a minute. A public one is refused: the challenge is a tag name on a public repository, so anybody watching can read it, and a gist anybody could have found says nothing about who you are. Step 3 above already creates the right kind. Each call that takes an attempt spends one of ten, whether or not the proof then holds, and it is taken before anything is checked. Two calls racing on the same state cannot both take one, and the loser is told to try again; a call arriving after an attempt has been taken gets the next one. Ten is the total either way. 5. gh api -X DELETE repos/OWNER/REPO/git/refs/tags/palomar-verify-CHALLENGE gh api -X DELETE gists/GIST_ID That is five steps and six calls, because step 5 is two deletes. If six calls where you expected one looks like a badly designed service, it is not: each one is load-bearing, and there is no shorter route to the same proof. Steps 1 to 4 are one sitting. An intake nobody comes back for is discarded fifteen minutes after step 1, and a `pending_secret` older than that is gone: step 4 answers 404 `that submission has already been verified`, because from here a consumed intake and a discarded one look the same. So do not call step 1 until you are ready to prove it, and do not hold one across a pause for your user. Beginning again is cheap: a fresh step 1 spends no verification attempt. Creating a ref requires the same write access the browser sign-in checks for, which is what makes step 2 a proof rather than a formality. A ref records no author, and a third party cannot ask GitHub who has push, so step 3 is the only part that says who you are — a gist has a GitHub-set owner and answers immediately. Step 5 is not tidiness: those artifacts exist only to be read once. Do not substitute something easier. A commit status is one call and would be accepted by GitHub from any integration holding `statuses: write`, which is not push access. Declaring a login proves nothing. If you cannot complete these steps — a tag ruleset refuses the tag, your token has no `gist` scope — stop and hand back to your user for the browser flow rather than looking for a weaker proof. Palomar records that this path proves less than the browser one: someone who can write to the repository submitted it, and an account named itself, which are not provably the same account. Do not describe them to your user as equivalent. Treat `access_token` as a credential. It reads the private review and it can register permanently. If that token is lost, do not drive the browser recovery sign-in. Hand control back to your user: `/submissions` (the submission form's **Find my submissions** action) lets them authenticate with GitHub and receive a fresh link while the submission is still in progress. ## After that, monitoring is yours With the token you can drive the rest through the HTTPS API. Send it as a header on every call: Authorization: Bearer - `GET /api/submission` — status, events, the verification run, the paths the submission asked for, and an estimate of how long review is taking. - `GET /api/review` — the review, once there is one. Private to the token holder. Do not paste it anywhere public, including a pull request or an issue, before it is registered. - `POST /withdraw` — abandon the submission. Use the header rather than `POST /session`. The browser status page uses the same header and omits cookies so that each open tab remains bound to its own submission. A header is not ambient, nothing else can set it on your behalf, and it does not expire after twelve hours the way a session cookie does. The server retains `/session` only for compatibility with legacy clients. Poll `GET /api/submission` at a human pace; a submission takes minutes, not seconds. Once a minute is fast enough while something is running, and once every five minutes while the status is `awaiting-review` or `review-ready`, whose next move is on a clock nobody here controls. Every ask spends several calls of one GitHub budget shared by every submission there is, so a tight loop does not fail your submission faster, it fails everybody's. The status page starts faster than that and backs off to the same ceiling, and stops asking altogether while nobody is looking at it. On a browser status page, a completed failed run is supplemented with bounded, unauthenticated reads of that public GitHub run's check annotations. An API client receives the run URL in `GET /api/submission` and may inspect the same public annotations itself; Palomar never sends the submission access token to GitHub. A submission is settled at `registered`, `withdrawn`, `verification-failed`, `review-failed`, or `dispatch-lost`. `GET /api/review` tells you whether the automated review identified blocking problems and what it asked for; it does not distinguish a request for revision from rejection, and inferring either from `"blocking_problems_identified": true` would add information that is not there. If `requested_changes` describes something you and your user can correct, correct it and submit the corrected commit as a new submission. Settled means there is nothing useful to poll for; it does not mean every decision is closed. A submitter may still withdraw a `review-failed` or `dispatch-lost` submission. ## Registration is not monitoring `POST /register` consents to making the repository, commit and review public during Palomar's pre-launch testing, and creates immutable source-preservation tags. Send the digest of the review you were shown: {"review_sha256": ""} A registration that names a different review, or names none, is refused with 409. Consent is to the review your user read, not to whichever one is current when the call arrives: a review can be replaced between the two, and the comments in it become public on registration. `GET /api/review` answers 404 until the digest is recorded alongside the review, which is a moment later than the review itself exists. Keep polling; there is nothing to do about it and nothing has gone wrong. Your user's GitHub identity is not made public: a registered record carries the submission and its authorization basis, and the schema has no field for the person who sent it. Until public launch the database itself may still be reshaped; after launch its registered records are append-only. The token is a bearer credential, so this endpoint will accept the call from you. Do not make it on your own initiative. Show your user the review, say what registering would publish, and let them decide and tell you. If they ask you to press it, that is fine; deciding for them is not. ## Practical notes - One repository owner may have at most two submissions verifying at once, and one submitter may have at most one; further ones are refused with 429 until those finish. There is no global admission cap, so unrelated submitters cannot exhaust a shared slot pool. A refusal is not a reason to retry immediately. These refusals happen after `/api/verify` has accepted and consumed the proof: follow its `restart` instruction and begin a new submission when capacity is available. - There is also an interval between starting one submission and starting the next. A 429 that says you started one too recently says how long to wait; wait that long rather than probing for the boundary. - A 503 whose `error` is `submission intake is at capacity` is about Palomar rather than about your submission or your address: more intakes are in progress at once than it will hold. Nothing was consumed and there is nothing to correct. Wait for the `retry-after` and send the same body again. - `/api/verify` allows a bounded number of failed proofs and then refuses and discards the intake. Fix the tag or the gist before retrying, rather than retrying the same broken proof. - A policy or principal-limit refusal after `/api/verify` has accepted the proof says `"proof_consumed": true` and includes a `restart` instruction. Start again at `/api/submit` when the refusal can be addressed. If durable State is damaged or unavailable, no admission commit lands: the response instead says `"proof_consumed": false`, and the same pending secret, tag, and gist may be retried after the service is repaired, subject to the response's `attempts_remaining`. An explicitly `"unknown"` outcome must not be retried automatically: ask the registry operator to inspect State first. - Errors on the `/api/` routes come back as JSON `{"error": "..."}` with a meaningful status, sometimes with `problems` or `detail` beside it. An unknown path, a wrong method, and an unhandled failure give you an HTML page instead, so parse defensively. - `GET /healthz` if you want to know the service is up. - Fields, and their validation, are visible in the form at `/`. - The registry's own data is at `https://data.palomar-registry.org`, read-only and separate from this host. There is no whole-registry document: ask for what is new at `/recent.json`, for one result's versions at `/versions/.json`, for one record at `/entries/-v.json`, and for a repository's active registrations at `/repositories//.json`. An exact registration identity is at `/registration-identities/.json`, where the digest covers the UTF-8 bytes `lowercase_repository + NUL + project_path_or_empty + NUL + comparator_config_path`. If it names one `registration_id`, its schema-version 2 `commits` array names every active source commit already registered for that identity. Do not submit one of those commits again. For a different commit, pass `registration_id` as `existing_id` to create a new version. A query string is refused with 404 there, so do not add cache-busting parameters.