CI: PalomarServer#150 rebased

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"]

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

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.
  *

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,15 +2345,17 @@ 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
   // consenting and that poll waits longer once; opening the link again fixes it.
   // 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;

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

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"],
+  );
+});

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();

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.