diff --git a/browser/preflight-policy.json b/browser/preflight-policy.json index 74bd9e9..403e9a0 100644 --- a/browser/preflight-policy.json +++ b/browser/preflight-policy.json @@ -19,7 +19,7 @@ }, "comparator": { "required_keys": ["challenge_module", "permitted_axioms", "solution_module", "theorem_names"], - "allowed_keys": ["challenge_module", "definition_names", "enable_nanoda", "permitted_axioms", "solution_module", "theorem_names"], + "allowed_keys": ["challenge_module", "definition_names", "enable_nanoda", "permitted_axioms", "solution_module", "theorem_names", "verification_profile"], "standard_axioms": ["Classical.choice", "Quot.sound", "propext"] }, "deferred_checks": ["classification-taxonomies", "git-attributes-lfs", "lakefile-toml", "licensee", "release-tag", "substantive-repository", "trusted-hashes"] diff --git a/public/llms.txt b/public/llms.txt index 7bc2936..c5a2372 100644 --- a/public/llms.txt +++ b/public/llms.txt @@ -15,6 +15,21 @@ is the only way in. The registry itself is at https://palomar-registry.org. Nothing about eligibility, metadata, or scoring is restated here. If this file and the policy disagree, the policy is right. +## Mechanical preflight + +Before `POST /api/submit`, run Palomar's complete reusable workflow at +`PalomarRegistry/PalomarSubmission/.github/workflows/submission.yml` for the +exact repository, commit, project paths, and Comparator configuration under +`palomar-standard-v1`. Pin both the workflow reference and its +`pipeline_commit` input to the same full commit. A local `lake build`, +repository-specific CI job, or standalone Comparator run is not equivalent. + +Submit only after the mechanical report says `status: pass`. An OOM, timeout, +missing terminal resource record, or other provider-owned error is inconclusive: +retry the same commit as instructed rather than changing the proof. Such an +error does not increase submission backoff. Mechanical preflight predicts the +mechanical gate; editorial review remains separate. + ## You may make an ordinary submission, but not by signing in as your user An ordinary submission requires proving that whoever submits can write to the @@ -223,7 +238,10 @@ 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 +`verification-error`, `review-failed`, or `dispatch-lost`. A +`verification-error` is Palomar-owned and refunds the attempt's backoff +increase; retry the same commit after addressing any stated capacity issue. +`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 diff --git a/src/admission-contract.js b/src/admission-contract.js index 4de7460..32df88b 100644 --- a/src/admission-contract.js +++ b/src/admission-contract.js @@ -214,6 +214,21 @@ export function resetRateRecord(value, resetAt) { return result; } +/** Undo the most recent backoff increase after Palomar could not verify. */ +export function refundRateRecord(value, refundedAt) { + const current = rateRecord(value).value; + timestamp(refundedAt, "next_allowed_at"); + const result = { + schema_version: 1, + starts: current.starts, + interval_seconds: Math.max(RATE_FLOOR_SECONDS, Math.floor(current.interval_seconds / 2)), + last_start_at: current.last_start_at, + next_allowed_at: refundedAt, + }; + rateRecord(result); + return result; +} + /** * Decide whether one more proved submission fits the principal admission caps. * diff --git a/src/index.js b/src/index.js index d1a801f..769f847 100644 --- a/src/index.js +++ b/src/index.js @@ -41,6 +41,7 @@ import { RateContractError, rateDecision, rateRecord, + refundRateRecord, resetRateRecord, } from "./admission-contract.js"; import { MAX_PREFLIGHT_REPAIR_BYTES, validateIntake } from "./intake-contract.js"; @@ -2344,7 +2345,9 @@ async function refresh(env, entry) { const record = entry.record; // A completed registration puts a submitter's interval back to a minute. A // small number of first-pass metadata corrections gets the same concession, - // but repeated failed preflights retain their accumulated backoff. + // while an infrastructure-owned verification error refunds the one increase + // caused by the attempt Palomar could not complete. Reproducible submission + // failures and repeated failed preflights retain their accumulated backoff. // This is where the server sees it: the status page and an agent both poll // until the status settles, and `registered` is settled, so the good news and // the reset arrive on the same request. Somebody who closes the tab between @@ -2352,7 +2355,7 @@ async function refresh(env, entry) { // The alternative, letting the reviewer reset it, would need TOKEN_PEPPER in // reviewer CI, and that pepper exists so a leaked state repository yields no // live links. - if (["registered", "changes-required"].includes(record.status) + if (["registered", "changes-required", "verification-error"].includes(record.status) && !record.rate_reset_at && record.push_proof?.principal?.id) { const path = await ratePath(env, record.push_proof.principal.id); const resetAt = recordedAt(); @@ -2365,8 +2368,14 @@ async function refresh(env, entry) { current = await readRateState(env, path); const correctionConcession = record.status === "changes-required" && current.value?.starts <= 2; - if (current.sha !== null && (record.status === "registered" || correctionConcession)) { - projected = atRatePath(path, () => resetRateRecord(current.value, resetAt)); + if (current.sha !== null && ( + record.status === "registered" + || correctionConcession + || record.status === "verification-error" + )) { + projected = atRatePath(path, () => record.status === "verification-error" + ? refundRateRecord(current.value, resetAt) + : resetRateRecord(current.value, resetAt)); } } catch (error) { if (!(error instanceof RateContractError)) throw error; diff --git a/tests/admission-contract.test.js b/tests/admission-contract.test.js index 72c294c..9c9a442 100644 --- a/tests/admission-contract.test.js +++ b/tests/admission-contract.test.js @@ -8,6 +8,7 @@ import { RateContractError, rateDecision, rateRecord, + refundRateRecord, resetRateRecord, } from "../src/admission-contract.js"; @@ -234,6 +235,29 @@ test("registration reset preserves rate history and returns to the floor", () => ); }); +test("an infrastructure refund removes one backoff step and permits an immediate retry", () => { + const refunded = refundRateRecord({ + schema_version: 1, + starts: 12, + interval_seconds: 122880, + last_start_at: "2026-08-07T00:00:00Z", + next_allowed_at: "2026-08-08T10:08:00Z", + }, "2026-08-07T01:00:00Z"); + assert.deepEqual(refunded, { + schema_version: 1, + starts: 12, + interval_seconds: 61440, + last_start_at: "2026-08-07T00:00:00Z", + next_allowed_at: "2026-08-07T01:00:00Z", + }); + assert.equal(nextRateRecord({ + starts: refunded.starts, + interval: refunded.interval_seconds, + startedAt: "2026-08-07T01:00:00Z", + at: Date.parse("2026-08-07T01:00:00Z"), + }).interval_seconds, 122880, "retry increased the pre-failure interval"); +}); + test("a reset sheds every identifying field an older document left", () => { // A spread would carry these forward forever, which is exactly how they // outlived the writers that produced them, so ordinary registration traffic diff --git a/tests/browser-preflight.test.js b/tests/browser-preflight.test.js index 7d05267..4d37ca7 100644 --- a/tests/browser-preflight.test.js +++ b/tests/browser-preflight.test.js @@ -415,3 +415,23 @@ test("the lazy browser bundle stays below its compressed page-weight budget", as const bundle = await readFile(new URL("../public/preflight.js", import.meta.url)); assert.ok(gzipSync(bundle).byteLength < 100 * 1024); }); + +test("the Comparator configuration may name Palomar's verification profile", () => { + const config = { + challenge_module: "Challenge", + solution_module: "Solution", + theorem_names: ["Example.main"], + definition_names: [], + permitted_axioms: ["propext", "Quot.sound", "Classical.choice"], + enable_nanoda: true, + }; + assert.deepEqual(validateComparator(JSON.stringify(config)), []); + assert.deepEqual( + validateComparator(JSON.stringify({ ...config, verification_profile: "palomar-standard-v1" })), + [], + ); + assert.deepEqual( + validateComparator(JSON.stringify({ ...config, memory_limit: "64G" })).map((item) => item.code), + ["comparator.unknown_key"], + ); +}); diff --git a/tests/decisions.test.js b/tests/decisions.test.js index dc6e2c2..705142c 100644 --- a/tests/decisions.test.js +++ b/tests/decisions.test.js @@ -4363,6 +4363,31 @@ test("a registration puts the interval back to a minute", async () => { ); }); +test("an infrastructure verification error refunds one backoff step", async () => { + const stub = stubAgent(); + const begun = await agentSubmit(); + stub.state.tag = { exists: true, sha: "1".repeat(40) }; + stub.state.gist = { exists: true, content: begun.challenge }; + const verified = await (await agentVerify({ + pending_secret: begun.pending_secret, gist_id: "abc123", + })).json(); + const rate = await agentRatePath(); + stub.store.set(rate, { + ...stub.store.get(rate), starts: 12, interval_seconds: 122880, + }); + const record = statePath(verified.submission_id, "state.json"); + stub.store.set(record, { ...stub.store.get(record), status: "verification-error" }); + + const response = await worker.fetch(new Request( + "https://submit.palomar-registry.org/api/submission", + { headers: { authorization: `Bearer ${verified.access_token}` } }, + ), ENV); + assert.equal(response.status, 200); + assert.equal((await response.json()).status, "verification-error"); + assert.equal(stub.store.get(rate).interval_seconds, 61440); + assert.match(stub.store.get(record).rate_reset_at, /^\d{4}-\d{2}-\d{2}T/); +}); + test("repeated metadata failures do not erase the accumulated admission backoff", async () => { const stub = stubAgent(); const begun = await agentSubmit(); diff --git a/tests/intake.test.js b/tests/intake.test.js index 626c3f3..1d33d5d 100644 --- a/tests/intake.test.js +++ b/tests/intake.test.js @@ -1061,6 +1061,11 @@ test("what agents are told about this service is true of this service", async () assert.match(guide, /\/register/); // And that it does not sell the agent path as equivalent to the browser one. assert.match(guide, /not provably the same account/i); + assert.match(guide, /^## Mechanical preflight$/m); + assert.match(guide, /PalomarRegistry\/PalomarSubmission\/\.github\/workflows\/submission\.yml/); + assert.match(guide, /`pipeline_commit` input to the same full commit/); + assert.match(guide, /provider-owned error is inconclusive/i); + assert.match(guide, /does not increase submission backoff/i); // It points at the policy rather than paraphrasing it, because a paraphrase // is a second copy that goes stale silently.