harness v4 converts a PostgreSQL major; the engine-major gate passes one proven, marked app (09 decision 35)
gates / gates (push) Successful in 2s

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0159rPz1ZhFKsS53msqPYxtS
This commit is contained in:
2026-09-25 13:04:01 +02:00
parent f238a24cd9
commit 6a4a5f0cf7
7 changed files with 364 additions and 9 deletions
+58 -4
View File
@@ -56,7 +56,10 @@ import subprocess
import sys
# Repository basenames that are database engines. A match here means "judge this service's major".
ENGINES = ("mariadb", "mysql", "postgres", "postgresql")
ENGINES = ("mariadb", "mysql", "postgres", "postgresql", "postgis", "pgvector")
# The Postgres family, for the conversion clause below (postgis/postgis:16-3.5 is PostgreSQL 16; it was
# not judged at all before 2026-09-25 — adventurelog's engine could have crossed a major unseen).
PG_FAMILY = ("postgres", "postgresql", "postgis", "pgvector")
# R-469, 2026-09-21 — THE MARIADB HALF OF THE RULE IS LIFTED; THE POSTGRESQL HALF IS NOT.
#
@@ -117,10 +120,40 @@ def engine_of(ref):
def major_of(tag):
m = re.match(r"^v?(\d+)", tag)
m = re.match(r"^(?:v|pg)?(\d+)", tag)
return int(m.group(1)) if m else None
def pg_conversion_proof(rev, compose_path, svc, mb, ma, after):
"""None when the template at `rev` carries a PROVEN two-venue ladder entry for exactly this step with
the matching engine_conversion mark; else the reason, as a sentence fragment."""
import json as _json
fy = compose_path.rsplit("/", 1)[0] + "/.felhom.yml"
rc, text, _ = git("show", "%s:%s" % (rev, fy))
if rc != 0:
return "%s cannot be read" % fy
entries = []
for line in text.splitlines():
m = re.match(r"^ - (\{.*\})\s*$", line)
if m:
try:
entries.append(_json.loads(m.group(1)))
except ValueError:
pass
step = [e for e in entries if e.get("to") == after]
if not step:
return "no ladder entry has `to` = this commit's images"
e = step[-1]
want = {"service": svc, "engine": "postgres", "from": mb, "to": ma}
if e.get("verdict") != "proven":
return "the step's entry is %r, not proven" % e.get("verdict")
if e.get("engine_conversion") != want:
return "the step's entry carries engine_conversion %r, want %r" % (e.get("engine_conversion"), want)
if not (e.get("evidence") and e.get("box_evidence")):
return "the step's entry does not cite BOTH venues' evidence (evidence + box_evidence)"
return None
def resolve_range(spec):
"""'A..B' -> (A, B, note). An all-zero A (a new remote ref) falls back to origin/main."""
if not spec or ".." not in spec:
@@ -195,8 +228,19 @@ def main(argv):
if mb == ma:
continue
row = (path, svc, eng_after[0], mb, ma, before[svc], img_after)
if eng_after[0] in PG_FAMILY:
# `09` §3 decision 35 (2026-09-25): a PostgreSQL major passes ONLY for a template whose ladder
# entry for THIS step is proven on both venues and carries the conversion mark, and only as
# the only image move in its commit (the MariaDB rule). Every other app stays refused.
why = pg_conversion_proof(b, path, svc, mb, ma, after)
others = [o for o in moves if o != svc]
if why is None and not others:
allowed.append(row)
continue
refused.append(row + ((why or "it is bundled with %s" % ", ".join(sorted(others))),))
continue
if eng_after[0] not in LIFTED:
refused.append(row)
refused.append(row + (None,))
continue
# R-469 + R-450: lifted, but it must be the ONLY image this commit moves in this
# template. `others` is named so the refusal can say WHAT it was bundled with.
@@ -211,9 +255,14 @@ def main(argv):
if refused or bundled:
print("")
for path, svc, eng, mb, ma, ib, ia in refused:
for path, svc, eng, mb, ma, ib, ia, pgwhy in refused:
print("ENGINE-MAJOR GATE FAILED: %s service %s moves %s %d -> %d (%s -> %s)."
% (path, svc, eng, mb, ma, ib, ia))
if pgwhy:
print(" NOT PROVEN FOR THIS APP: %s. A PostgreSQL major passes only with a ladder entry for "
"this step that is proven on BOTH venues and carries engine_conversion {service, "
"engine: postgres, from, to} (written by upgrade-test.py --write-ladder), and only as "
"the only image move in its commit (`09` §3 decision 35)." % pgwhy)
print(" WHY: %s performs no datadir conversion of its own and REFUSES to start on an "
"older major's datadir (R-463, eleven templates). The Update takes a backup first "
"since Slice 4, but a backup is a route BACK, not a conversion — the app would "
@@ -239,6 +288,11 @@ def main(argv):
return 2
for path, svc, eng, mb, ma, ib, ia in allowed:
if eng in PG_FAMILY:
print("engine-major gate ALLOWED: %s service %s moves %s %d -> %d (%s -> %s) as its own edge — "
"its ladder entry is proven on both venues and carries the conversion mark (`09` §3 "
"decision 35; the box converts it, controller v0.273.0)." % (path, svc, eng, mb, ma, ib, ia))
continue
print("engine-major gate ALLOWED: %s service %s moves %s %d -> %d (%s -> %s) as its own edge "
"— permitted since R-469 (Slice 4 shipped; MARIADB_AUTO_UPGRADE=1 converts the datadir)."
% (path, svc, eng, mb, ma, ib, ia))