HOMELAB-2682: feat(sbx-gits): declaration-anchored proof check (gits-proof-suite) #871
No reviewers
Labels
No labels
operator-review
No milestone
No project
No assignees
2 participants
Notifications
Due date
No due date set.
Dependencies
No dependencies set.
Reference
Homelab/infra-core!871
Loading…
Add table
Add a link
Reference in a new issue
No description provided.
Delete branch "plane/HOMELAB-2682-declaration"
Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?
What this delivers
The FULL desired state of the proof tool: the #859 reviewed content (whose file a later
revert took out) as the base, #869's
suite_relpathwork intact on top, plus thedeclaration of the canonical suite (
gits-proof-suite).The sequence this closes
9119eb2b) — the proof tool anchored to the smoke committed at the head: 1623lines, the whole anchor machinery (
git_obj/GIT_NO_REPLACE_OBJECTS=1+core.useReplaceRefs=false,git_path_type,git_blob_shawith the oid binding and thezero-byte refusal, the verdict line, the canonical-red warning,
--tree).22c2c328) — reverted the file (-586/+48), pending this declaration work.Live's tool went back to pre-#859 with #869's forward-compat on top.
a848b717) —suite_relpath: chain_text argument 21, read and written, sothe lines the #859 tool wrote while it was briefly deployed recompute byte for byte.
declaration.
git diff 9119eb2b:<tool> <this>shows only the declaration additions:rel_underis byte-identical to #859's, and thechain_textrecompute call incheckisbyte-identical to #869's (argument 21 included).
1. Declaration support (the format, settled and acked by homelab-33)
gits-proof-suiteat the root of the repo being checked — fixed filename, notenv-configurable (an anchor that can be redefined is not an anchor), read from the head
commit, never from the working tree:
suite=<repo-relative path>line;suite=lines, an emptysuite=, an absolute path, or one that escapes with... Thedeclaration is never half-read;
ghostty-in-the-shelldev) issuite=scripts/ci/gits-sbx-emu-smoke.sh— a copy of the smoke committed in the app repo.2. Resolution order for the canonical suite at head
HHcarriesgits-proof-suiteH, with all of #859's machineryHcarriesEMU_PROOF_SMOKE_RELPATHHA declared path that does not exist in
His rc 1 as well: the declaration and the suite itnames travel in the same commit. No fallback, no substitute suite (B2 preserved).
3. Class output (homelab-33's condition)
The check always prints a class line. When the diff
git diff <merge-base with the live/default branch>..<H> -- gits-proof-suite <declared suite>is non-empty:
Base ref:
origin/HEAD, else the first oforigin/live|origin/dev|origin/main|..., with atimeout-bounded
fetchas a last resort;--base <ref>pins it. No usable base →class unknown — assume gate tooling. Informational only — pass/fail unchanged, printed onboth the OK and the FAIL path.
4. FAIL visibility (homelab-33's FAIL-veto answer)
Unchanged from #859 and now pinned by a test: a red run of the same canonical smoke on
the same head prints
PROOF aviso el smoke CANONICO TAMBIEN CORRIO EN ROJO ... result=FAIL rc=1next to the passing verdict. The red line is neither deleted nor hidden.
5. Cross-version ledger reading stays
class/results_sha256/suite_relpathremain optional; lines from every era (18, 20,21 fields) recompute byte for byte. Nothing about the ledger format changes here.
The pin: this PR does NOT deploy
#870 pinned the
sbx-gits-toolsConfigMap content as an explicitliterals:block, so editingtools/*.shleaves the render byte-identical and ArgoCD has nothing to sync.kustomization.yamland
statefulset.yamlare untouched in this PR. The deployment happens later in a deliberatepin-bump, after GITS
devcarries itsgits-proof-suitedeclaration.Verification
bash -non the tool and on all sixtools/*.sh+ the harness: clean.before/after table; new section 27 covers: declared-repo pass with the anchor on the
declared blob (the repo also carries the infra-core canonical path with different
content, so the case proves the declaration wins), declared-path-missing → rc 1, five
malformed-declaration refusals for
checkandrun(no line written), class on thedeclaration, class on the declared suite,
class unknown — assume gate tooling, FAILvisibility, and "the name is not configurable from the environment".
T7[diff]/17[R159] (d):SBX_GITS_DIFF_SETre-measured for this branch(
M tools/gits-sbx-emu-proof.sh+M README.md). The pre-existing10b[R99]red (documentedas deliberate in README §10.5 after the pin removed
files:) is untouched by this PR.Scope
tools/gits-sbx-emu-proof.sh,README.md(§10.6),docs/gits-sbx/run-proof.md, and theharness. No statefulset, no kustomization, no smoke.
Do not merge on one seat: two gate seats follow (homelab-33's condition).
Verification evidence (head
95b0d62e) — evidence only, NOT a review verdictHarness, SOLO runs (never concurrent)
origin/live=56356d90(pre-PR)95b0d62eThe 6 remaining failures are exactly the 6 that already failed on live —
common the twoFAIL sets reports zero branch-only failures:
The
10b[R99]red is the one documented as deliberate inREADME.md§10.5 (the #870 pinremoved
files:, and the guard has to be re-enunciated for the pin in a separate harnesschange). The other five are manifest/media, untouched by this PR.
The 47 that went green are the revert's own debt: §22, §24, §25 and §26 were written against
the #859 tool and were red on live because live's tool was the reverted one
(
argumento desconocido en check: '--tree').The cases this PR is about
refusal, B6/B7
git replaceforgery, A1 mount signal, B2 no-fallback.suite_relpathforward-read): 7/7 green.check'schain_textrecompute call isbyte-identical to #869's, argument 21 included;
rel_underis byte-identical to#859's.
(b2)/(c)were vacuous on live (the fixture's head was not a commit, so thecheck stopped at the git gate); the fixture is now a real repo, so the chain is really
measured.
declared blob (the fixture also commits the infra-core canonical path with different
content, so the case proves the declaration wins), declared-path-missing → rc 1, five
malformed declarations refused by
checkandrunwith no line written, class onthe declaration, class on the declared suite,
class unknown — assume gate toolingwith anorphan base, FAIL visibility next to the passing verdict, and "the name is not configurable
from the environment".
T7[diff]and17[R159] (d): green, with both mutagens biting(
M README.md+M tools/gits-sbx-emu-proof.sh, re-measured for this branch).Provenance of the tool at this head
kustomization.yaml,statefulset.yamland the smoke are not touched (git diff --stat:README + tool + docs + harness). The #870 pin still holds the ConfigMap, so this PR does not
reach the pod; the delivery is a later pin-bump, after GITS
devcarries its declaration.GITS-508's two review seats, relayed by homelab-33. Neither changes the resolution order. 1. DRIFT VISIBILITY. A declaration names a PATH with no digest, so the repo's copy and the mounted copy can drift unnoticed. The A1 signal already compared the committed blob of the canonical suite against the mounted file — for a DECLARED repo that is the declared blob, which is what we want — and the check now says the two roles out loud, in a dedicated `ANCLA/DERIVA` line (printed on the OK and on the FAIL path): the gate anchors to the COMMITTED blob of the declared path in the head, and the comparison with the mounted file is INFORMATIVE drift detection, not a criterion. 2. SPDX HEADER. The repo copy carries an SPDX/licence header the mounted copy lacks, so a raw comparison always differed — a warning that always fires is noise. The ADVISORY comparison is now normalized: leading comment/blank header lines are stripped from BOTH the committed blob and the mounted file before hashing, and the flag reads IGUAL bytes are the committed blob's IGUAL(sin-cabecera) only the header differs — no content drift DISTINTO the suite's content differs — real drift no-legible the mounted file could not be read The GATE anchor is untouched: `git_blob_sha` (exact blob, header included) still decides, and `ancla_blob` / the line's `script_sha256` are byte-for-byte what they were. Documented in the tool's --help, docs/gits-sbx/run-proof.md and README §10.6. Harness case 27 (h) pins both halves at once: a repo whose committed suite carries SPDX with a mounted copy without it gives rc 0, `ancla_blob` = the EXACT committed blob, `montado=IGUAL(sin-cabecera)`; one extra line in the usable content gives `montado=DISTINTO` WITHOUT moving the anchor; a byte-identical mount gives `montado=IGUAL`.Design additions folded in (GITS-508's two seats) + final harness record (head
4b747c5c)1. Drift visibility for declared repos
A declaration names a path with no digest, so the repo's copy and the mounted copy can drift
unnoticed. The check now prints a dedicated
ANCLA/DERIVAline (on the OK and the FAIL path)that says the two roles out loud: the gate anchors to the COMMITTED blob of the declared path in
the head, and the comparison with the mounted file is advisory drift detection — informative,
never a criterion. The comparison was already pointed at the declared blob (not the infra-core
canonical path); what was missing was the wording that keeps a reader from confusing the two.
2. SPDX header — the advisory comparison is normalized, the anchor is not
The repo copy carries an SPDX/licence header the mounted copy lacks, so a raw comparison always
differed — a warning that always fires is noise.
strip_leading_commentsnow removes the leadingcomment/blank header block from both the committed blob and the mounted file before hashing:
montado=IGUALIGUAL(sin-cabecera)DISTINTOno-legibleThe gate anchor is untouched:
git_blob_sha(exact blob, header included) still decides, andancla_blob/ the line'sscript_sha256are byte-for-byte what they were — the normalizationtouches only the advisory signal. Documented in the tool's
--help,docs/gits-sbx/run-proof.mdand
README.md§10.6, and pinned by harness case 27 (h): repo with SPDX + mounted copy withoutit → rc 0,
ancla_blob= the exact committed blob,montado=IGUAL(sin-cabecera); one extra linein the usable content →
montado=DISTINTOwithout moving the anchor; byte-identical mount →montado=IGUAL.Harness, SOLO runs
origin/live=56356d90607e58244b747c5cZero branch-only failures: the 6 are exactly live's own reds (
common the two FAIL sets isempty).
T7[diff]+17[R159] (d): 6 PASS, 0 FAIL (both mutagens bite).§25/§26/§27: 52 PASS, 0 FAIL.
The one extra red in the middle run —
22[R172c-fix] (n1), the 10-waiter lock stress — was aload flake, not a regression: the queue/lock scripts are byte-identical to live
(
git diff --quiet origin/liveon all three), the reported invariant parts were all empty (norepeated sequence, no mismatched name,
last-seqcorrect — only "corrieron 7 of 10" missed), andit is green in the final run on the same code.
Merge of live
Live moved under the branch (#867 volume floors, #868 gradle-idle pair). Merged
4197ca48in; thethree conflicts were all in the harness's pinned sbx-gits set and were resolved by re-measuring
it against the new tip (
M tools/gits-sbx-emu-proof.sh+M README.md), with the supersededM tools/gits-sbx-android-install.shassignment (already in live via #868) removed and the set'shistory kept as prose.
Head:
4b747c5c. Two gate seats still to go before any merge (homelab-33's condition); this PRdoes not deploy — the delivery is the later pin-bump.
Verdict of record — ld-reviewer — head
4b747c5c0a: APPROVEmodel: deepseek-flash
session: seat2-ds-75943d536293f232-20261106T070626Z
Blockers
None.
Concerns
rc 0) with the right line,PROOF GATE-TOOLING CLASS: this change touches the proof declaration or its named suite — two review seats required (merge-base live..H toca: gits-proof-suite scripts/ci/trivial.sh). Then, same head, same ledger:git branch -f live <H>in the checkout →clase: routine — ni 'gits-proof-suite' ni 'scripts/ci/trivial.sh' cambian entre live y H,rc 0, no class line at all;--base <H>gives the same;check --quietprints 0 bytes and still returns rc 0, so the class line is gone with the FAIL text.proof_class_base's fallback list contains the bare local nameslive dev main masterbehind theorigin/*refs, so a stale (or planted) localliveis not only a spoofing lever but an innocent false-negative generator. Not a blocker: the class is informational by design (pass/fail is unchanged, homelab-33), the anchor is untouched by any of this, and a declaration rewrite is visible in the PR diff the seats read. Suggest dropping the bare local names from the fallback (remote-tracking only) and, since the class line is now the two-seat hint, not letting--quietswallow it.RESULT: FAIL (6 of 673 checks failed, 6 skipped); the 6 are exactly the author's baseline set (probe EMPTY pre-existing --dir,manifest[2],manifest[3],manifest[3b],T7 emulador,T7+R99[10b]). Independently corroborated:statefulset.yamlandkustomization.yamlare byte-identical toorigin/liveon this head, and none of those six assertions appear in the diff. §25+§26: 39 PASS / 0 FAIL; §27: 13 PASS / 0 FAIL.git_path_typemaps mode120000toblob(correct for git), so withsuite=scripts/link.sh -> real.shthe anchor is the sha256 of the link target text whilerunhashes the target's content: the line can never match and the head fails closed withel blob hashea d7b1… ; ninguna linea OK lleva ESE script_sha256. Fail-closed, so no hole — only an opaque dead end if GITS ever symlinks its smoke.What I measured (unit//tmp git fixtures only; no real PR, pod or emulator)
Declaration games — every one fails closed, no silent acceptance found:
suite=../xandsuite=scripts/../../x→ rc 2 (se SALE del repo); absolute → rc 2; a secondsuite=→ rc 2 (MAS DE UNA VEZ); an unknown key → rc 2 naming the key; emptysuite=→ rc 2; a zero-byte or comment-only declaration file → rc 2 (NO declara ninguna suite).runrefuses the same forms and writes no line.es un 'tree', NO un blob); a gitlink declaration → rc 2 (es un 'gitlink', no un fichero); a zero-byte declared blob → rc 1 (B3); a declared path absent from H → rc 1 naming both the declaration and the path, with no fallback to the canonical path that the same commit also carries (B2 intact).suite=scripts/ci/s.shand then rewritinggits-proof-suiteon disk tosuite=other/evil.sh(uncommitted), the check still anchors onscripts/ci/s.sh,rc 0— the declaration is read from the commit, never from disk.suite=…\r\n) → parsed, rc 0.suite = <path>with spaces around=and trailing blanks is also accepted (trimmed); permissive, harmless, no path is invented../or:resolve literally (./ok.sh,:colon.sh→ rc 1 "no existe"); the:(top)<path>pathspec survives a:colon.shsuite (checked: the class diff still matched it).SPDX normalization scope — does not touch the anchor. Committed suite carrying
# SPDX…+# Copyright…, mounted copy with the header stripped:rc 0,montado=IGUAL(sin-cabecera), andancla_blob=1a4f8382c54b…is byte-equal tosha256(cat-file blob H:<declared path>)with the header — the normalization moved the advisory flag only. Changing a comment after the first code line givesmontado=DISTINTO(only the leading comment/blank block is stripped), and theANCLA/DERIVAline keeps saying the anchor is the exact committed blob. (Degenerate: two different comment-only files both normalize toe3b0c442…; advisory only, and a comment-only suite produces no XML and fails ontests_run=0.)Replace-refs / config lever — still closed on the declared anchor.
git replace <H> <F>whereFcarries a different body at the declared path:rc 0with the AVISO naming the refs/replace,ancla_blobunchanged (the real blob of H). Addinggit config core.useReplaceRefs trueto the checkout: identical result —git_obj's-c core.useReplaceRefs=falsestill wins.Regressions on the canonical/declared path still bite.
record→ rc 2, nothing written. B1 before-run:tree_clean=falseline → FAIL naming it. B1 during-run: the suite creating an untracked file →tree_clean_after=false. B5/FAIL visibility: green line 1 plus a red run of the same canonical suite on the same head →rc 0andPROOF aviso el smoke CANONICO TAMBIEN CORRIO EN ROJO … result=FAIL rc=1printed next to the verdict. B4 attribution,class/results_sha256/suite_relpathoptionality and forward-reading are covered by §24–§26 (39 PASS / 0 FAIL).bash -nclean on the tool, the sixtools/*.shand the harness.Claim honesty.
git diff 9119eb2b:<tool> <this head>is+347/-13, and every deleted line is a mount-comparison or declaration line superseded by the normalized advisory comparison —rel_underand thechain_textrecompute (argument 21) are present as described.kustomization.yaml,statefulset.yamland the smoke are untouched, so this PR does not reach the pod: the delivery is a later pin-bump, as stated.One seat. The two-seat condition of homelab-33 is not satisfied by this comment alone.
Verdict of record — ld-reviewer — head
4b747c5c0a: APPROVEmodel: deepseek-flash
session: 01a1afa2-f413-757a-b84d-27ea75679d35
Independent review seat 1 of 2 (gate tooling). Reviewed from primary sources only: the diff at the head, the tool at the head executed against throwaway git fixtures (unit//tmp), and the two frozen predecessors (
git show 9119eb2b:…,git show a848b717:…), plus a read-only pull of the live pod ledger for the cross-era fixture. Not dependent on seat 2.Blockers
None.
Provenance — verified, not taken on trust
origin/live(4197ca48) is byte-identical toa848b717:…(#869), and the head file is #859's content (9119eb2b:…, 1623 lines) plus additions:diff 859 → headis 477 lines and every hunk is declaration / class / SPDX-normalization text — no removal, no behavioural edit of the anchor.rel_underis byte-identical to #859's (8/8 lines).chain_textbody is functionally identical to #859's — the only change is the added comment block; field 21 (suite_relpath) was already emitted by #859 at exactly that position, which is why both eras read each other.checkrecompute call (thechain_textinvocation carrying arguments… "$cclass" "$results_sha_line" "$crel_line") is byte-identical across 859, 869 and head. That is the line that decides whether cross-era lines recompute; it did not drift.Declaration semantics — verified by execution
Resolution order is exactly declared → canonical → fail closed, with no fourth path:
suite=sui/smoke.sh) and infra-core's canonical path with different content: verdict OK,smoke_rel=sui/smoke.sh,suite_sha256= sha256 of the declared blob, and the canonical blob's sha appears nowhere. The declaration wins.gits-proof-suiteas the missing declaration, noPROOF: OKline.checkand byrun, with zero lines written: unknown key (owner=), a non-suite=key, twosuite=lines, emptysuite=, absolute path,..escape, and a non-key=valueline. Seven for seven.gitlink; a zero-byte blob → refused on the byte accounting (no empty-string sha256 as anchor); and replace-proof: withgit replace H Fplusgit config core.useReplaceRefs truein the checkout, the check still reads the real blob, prints the real sha, and never emits the forged blob's sha.Class output — fires correctly and never moves the verdict
gits-proof-suite(comment-only edit):PROOF GATE-TOOLING CLASS: this change touches the proof declaration or its named suite — two review seats required, verdict OK, rc 0.clase: routine, no gate line, verdict unchanged.trunk, no origin, nothing to fetch):GATE-TOOLING CLASS: class unknown — assume gate tooling, verdict unchanged.saybefore the ledger read, andcheck_reportstill emits its reasons). It is informational only — nothing inok_line/gatedepends on it.SPDX normalization — advisory only, gate hash untouched
montado=IGUAL(sin-cabecera), andancla_blob=/suite_sha256=still the exact committed blob (header included).montado=DISTINTO.PROOF: OK). The anchor still includes the header — the normalization touches only the comparison.Cross-era ledger — the pod's real ledger as the fixture
Pulled read-only (
/home/ld/work/.emu-proof/ledger.jsonl, 38 lines) and recomputed every line with the head tool's ownchain_text/sha256_text: 38/38 recompute hash and prev-chain, mixing eras 18 fields, 20 fields (results_sha256, 8 lines) and 21 fields (suite_relpath, lines 33/36/37/38 — the #859-written one included). Nothing in the format change breaks the chain for any era.Harness (SOLO, this branch vs a live baseline, same env/refs)
4b747c5c: 667 PASS / 6 FAIL / 6 SKIP (673 checks).origin/livebaseline, same invocation: 602 PASS / 53 FAIL / 8 SKIP (655 checks) — the ~54 baseline reds the brief warns about.manifest[2]/[3]/[3b]memory+image pins, the T7 emulator resource pin,10b[R99]documented as deliberate in README §10.5, and one unrelated probe). The branch additionally turns 47 live reds green — mostly the §22[R176b]/§25/§26 cases that were red on live because live's tool is the pre-859 one without--treeand the rest of the anchor machinery.class unknown, FAIL visibility beside the passing verdict, the name not being environment-configurable, and three doc invariants. §25/§26: all pass, 52 PASS / 0 FAIL across §25/§26/§27.Scope / pin
Files:
tools/gits-sbx-emu-proof.sh,README.md(§10.6),docs/gits-sbx/run-proof.md,scripts/gits-sbx-epic-test.sh.kustomization.yamlandstatefulset.yamluntouched — merging deploys nothing, as the #870 pin intends.Concerns
gits-proof-suite+ the named suite only. A head that rewrites the proof tool itself (tools/gits-sbx-emu-proof.sh) and nothing else readsclase: routineby that rule — this very PR is such a head. The settled format (homelab-33) says "declaration or its named suite", so the tool is behaving as specified; worth considering in a follow-up whether the tool belongs in that pathspec.strip_leading_commentsalso strips the shebang (it is a#line at the top), so a mounted copy that lost or changed#!/usr/bin/env bashreads as no drift. Advisory only — the gate hash is unaffected — but the signal's name ("sin-cabecera") slightly overstates what was normalized.