pre-push(17.4): a file new in head is new, not comparison unknown

ChangeContext records the paths Git reports as added. An entailed,
undischarged operation in an added file, with complete head evidence and no
identical operation in any base answer, is classified new
(file_added_in_head) instead of base_incomplete; admission accepts that reason
as change evidence. Unpaired add/delete pushes and every other unknown
comparison keep their vetoes. An engine finding whose novelty is established
and whose only vetoes are capability vetoes is shown as an advisory engine
finding, not an alert. Requirement 9.4.

Co-Authored-By: Claude Opus 5.5 <[email protected]>
Claude-Session: https://claude.ai/code/session_01EmM1j46qgKMh3zqD1QMwEo
This commit is contained in:
Marius Ciepluch
2026-10-02 22:24:24 +02:00
co-authored by Claude Opus 5.5
parent 15999a09e1
commit 511de4b75f
6 changed files with 163 additions and 1 deletions
+4
View File
@@ -111,6 +111,9 @@ class ChangeContext(Contract):
# are not encoded or decoded by this field.
path_encoding: Literal["text", "filesystem-bytes-hex"] = "text"
line_correspondences: tuple[LineCorrespondence, ...] = ()
# Paths Git reports as added (status A) in head, in this context's path encoding. A rename
# target is not added. Only a lexical fact: novelty still needs complete head evidence.
added_paths: tuple[str, ...] = ()
def decode_path(self, path: str) -> str:
"""Return the filesystem spelling for matching ordinary question paths.
@@ -130,6 +133,7 @@ class ChangeContext(Contract):
*(s.path for s in self.spans),
*(p for r in self.renames for p in (r.base_path, r.head_path)),
*(p for m in self.line_correspondences for p in (m.base_path, m.head_path)),
*self.added_paths,
]
for path in paths:
try:
+11
View File
@@ -658,6 +658,16 @@ def _compare_evidence(
reason = "head_context_incomplete"
elif execution_budget is not None and time.monotonic() >= execution_budget.deadline_monotonic:
reason = "deadline_exhausted"
elif op.path in {context.decode_path(p) for p in context.added_paths}:
# The file did not exist in the base, so no base line or counterpart question can hold
# this operation (task 17.4, Requirement 9.4). Code moved here from elsewhere is still
# movement: an identical operation in any base answer keeps it out of `new`, and an
# unpaired add/delete in the same push already blocked above as context.
reason = "operation_moved_within_change"
if not any(b.operation == op.operation and b.mechanism == op.mechanism for b in base_ops):
reason = "file_added_unsupported_claim"
if change and finding.rung == Rung.ENTAILED and not op.discharged:
novelty, reason = "new", "file_added_in_head"
elif enumerated:
same = tuple(b for b in old if b.source == op.source)
reason = "operation_correspondence_unresolved"
@@ -926,6 +936,7 @@ def admit_candidates(candidates: Sequence[AdmissionCandidate], *, capabilities:
elif not delta.change_evidence or (delta.novelty, delta.reason) not in (
("new", "source_connection_absent_from_comparable_base"),
("new", "operation_absent_from_comparable_base"),
("new", "file_added_in_head"),
("worsened", "discharge_removed"),
):
reasons.append("change_unsupported")
+45
View File
@@ -219,6 +219,50 @@ def _experimental_line(experimental: Mapping[str, object]) -> str:
)
# Vetoes that say only "this capability is not qualified yet". A candidate whose novelty is established
# and whose only vetoes are these is shown as an advisory engine finding (task 17.4, Requirement 9.4);
# any comparison, evidence or location veto keeps it out of the terminal.
_CAPABILITY_VETOES = frozenset(
{
"capability_unavailable",
"capability_disabled",
"capability_unevaluated",
"capability_ambiguous",
"operation_semantics_mismatch",
"consequence_unsupported",
"repair_unsupported",
}
)
def _advisory_engine_lines(report: PushReport) -> list[str]:
shown: dict[str, list[str]] = {}
for disposition in report.admission.dispositions:
delta = disposition.candidate.delta
op = delta.head_operation
if (
disposition.admitted
or delta.novelty not in ("new", "worsened")
or not set(disposition.reasons) <= _CAPABILITY_VETOES
or op is None
or delta.witness is None
or delta.defect_id in shown
):
continue
how = "new" if delta.novelty == "new" else "worsened"
shown[delta.defect_id] = [
f"- {_short(delta.family)} at {_short(op.path, 4096)}:{op.line} ({how}): {_short(redact_secrets(delta.witness))}"
]
if not shown:
return []
lines = [f"Engine: {len(shown)} finding(s) this push introduced. Advisory: the capability is not yet qualified, so not an alert."]
for entry in list(shown.values())[:3]:
lines.extend(entry)
if len(shown) > 3:
lines.append(f"{len(shown) - 3} more advisory engine findings retained in the detailed result.")
return lines
# Quick-rule matches shown per comparison; the artifact keeps every one.
_QUICK_LINES = 5
@@ -285,6 +329,7 @@ def render_report(report: PushReport, *, artifact: Path | None, error: str | Non
)
if len(defects) > 3:
lines.append(f"{len(defects) - 3} more actionable defects retained in the detailed result.")
lines.extend(_advisory_engine_lines(report))
for payload in report.quick:
lines.extend(_quick_lines(payload))
if not defects:
+5
View File
@@ -249,6 +249,7 @@ class SnapshotAdapter:
boundaries = ["declaration_paths_unavailable"] if declaration_paths is None else []
changed: list[str] = []
deleted: list[str] = []
added: list[str] = []
spans: list[ChangedSpan] = []
renames: list[PathRename] = []
mappings: list[LineCorrespondence] = []
@@ -305,6 +306,9 @@ class SnapshotAdapter:
if status == "D":
assert path_base is not None
deleted.append(path_base.hex())
if status == "A":
assert path_head is not None
added.append(path_head.hex())
if status == "R":
assert path_base is not None and path_head is not None
renames.append(PathRename(path_base.hex(), path_head.hex()))
@@ -432,6 +436,7 @@ class SnapshotAdapter:
tuple(boundaries),
"filesystem-bytes-hex",
tuple(mappings),
tuple(added),
)
@contextmanager