arborist/bench/batteries/base.py
russell@unturf.com 7b7ac3867d
ticket #000032: combinatorics@v1 π* (pure-integer counting kernel)
A new π* kernel that canonicalizes pure-integer counting
expressions and FAILS CLOSED on any input whose result isn't a
non-negative sp.Integer. Tighter domain than algebra-symbolic@v1,
which already accepts the same input surface but happily returns
symbolic / negative / non-integer outputs.

Distinguishing feature versus algebra-symbolic@v1:
  algebra-symbolic@v1: binomial(n, k) → "binomial(n, k)" (symbolic
                       passthrough)
  combinatorics@v1:    binomial(n, k) → PiStarError (fail-closed
                       on free-symbol output)

  algebra-symbolic@v1: binomial(Rational(1,2), 3) → 1/16 (rational)
  combinatorics@v1:    binomial(Rational(1,2), 3) → PiStarError
                       (output not Integer)

Boundary kept explicit: binomial(-3, 2) = 6 IS accepted because the
output is an integer 6. The fail-closed rule is on output shape
(Integer ≥ 0), not input range. Documented as
test_generalized_binomial_negative_args_accepted_when_integer.

Output format: plain decimal literal (b"10", b"5040"). Composes
with arithmetic@v1 for byte-identical agreement with the rational
route (b"10/1") so the multi-modality witness (#000028) can pin
equivalence-class agreement when both routes fire on the same
question.

Allowed surface (via SymPy primitives): binomial, factorial, ff /
rf (falling/rising), catalan, bell, partition, stirling, plus
arithmetic compositions over those primitives
(3*binomial(5,2) + factorial(4) = 54).

Coverage:
- 43 unit tests including binomial symmetry C(n,k)=C(n,n-k),
  Pascal's rule C(n,k)=C(n-1,k-1)+C(n-1,k), the C(n,k) =
  factorial(n)/(factorial(k)·factorial(n-k)) identity,
  fail-closed paths (symbolic/negative/non-integer/relational/
  parse), round-trip idempotence, composition with arithmetic@v1.
- 10 syntax + 12 semantics bench fixtures, 100% pass.
- bench/batteries/base.py PHASE_1_CARRIERS gains "combinatorics".
- Makefile bench-5s-combinatorics target.

All gate on pytest.importorskip("sympy") so a sympy-less suite
stays green. Full make test: 1537 passed / 28 skipped.

Sequencing rationale honored: this kernel lands FIRST so that
#000033 (claim-pack pillar VII for combinatorics) can bind its
records to the tighter integer kernel from day one — avoids
rebind churn on pi_star_ref fields.
2026-05-09 13:20:29 -04:00

157 lines
4.7 KiB
Python

"""Battery base classes.
A Battery runs a fixture file end-to-end against a specified runtime
(usually arborist's existing surface) and emits a deterministic
:class:`BatteryResult`. Determinism: same fixture digest + same code
digest → identical result (modulo wall-clock fields).
"""
from __future__ import annotations
import hashlib
import json
import time
from dataclasses import asdict, dataclass, field
from pathlib import Path
from typing import Any, Iterable, Optional, Protocol
@dataclass
class TaskResult:
"""Per-task outcome inside a battery run."""
task_id: str
passed: bool
detail: dict[str, Any] = field(default_factory=dict)
@dataclass
class BatteryResult:
"""End-to-end battery result; deterministic given fixed inputs."""
battery: str
sub_battery: str
fixture_path: str
fixture_digest: str
pass_count: int
fail_count: int
metrics: dict[str, float] = field(default_factory=dict)
per_task: list[TaskResult] = field(default_factory=list)
runtime_digest: str = ""
timestamp: int = field(default_factory=lambda: int(time.time()))
def to_dict(self) -> dict:
d = asdict(self)
return d
class Battery(Protocol):
"""One sub-battery (e.g., 5S Syntax)."""
name: str
def run(self, fixtures_path: Path) -> BatteryResult:
...
def fixture_digest(fixtures_path: Path) -> str:
"""SHA-256 over the raw fixture-file bytes.
Used as the canonical identity of a battery run; bench results
cite this digest so cross-run comparisons are unambiguous.
"""
return hashlib.sha256(
Path(fixtures_path).read_bytes()
).hexdigest()
def iter_tasks(fixtures_path: Path) -> Iterable[dict]:
"""Yield non-meta task dicts from a JSONL fixture file."""
with open(fixtures_path, "r", encoding="utf-8") as fh:
for line in fh:
line = line.strip()
if not line:
continue
obj = json.loads(line)
if "_meta" in obj:
continue
yield obj
def fixture_meta(fixtures_path: Path) -> dict:
"""Return the ``_meta`` dict if present at the top of the JSONL."""
with open(fixtures_path, "r", encoding="utf-8") as fh:
for line in fh:
line = line.strip()
if not line:
continue
obj = json.loads(line)
if "_meta" in obj:
return obj["_meta"]
return {}
return {}
# Phase-1 carrier whitelist (per tickets #000023/#000024/#000025).
# Tasks lacking ``carrier`` default to "text" for backward compat with
# Phase-1a fixtures (syntax-v1, semantics-v1, transfer-v1) — those
# digests stay pinned and the carrier field is purely additive.
PHASE_1_CARRIERS = frozenset({
"text",
"claim_lattice",
"prose",
"memory_snapshot",
"selfmodel_snapshot",
"providence_record",
"audit_event",
"verifier_strategies",
"propositional_logic",
"relation_graph",
"qa_answer",
"capability_transition",
"memory_root",
# First non-text carrier, landed via code-py-ast@v1 graduation.
"code",
# Math π*'s — arithmetic@v1 + logic-kernel@v1 graduations
# (SQD §14.1 + §14.3).
"arithmetic",
"logic",
# Sensor / temporal-signal carrier — time-series-quantized@v1.
"time_series",
# Symbolic-algebra carrier — algebra-symbolic@v1 (ticket #000030).
# Calculus-derivative shares this carrier (its output is itself an
# algebraic expression).
"symbolic_algebra",
# Calculus / linear-algebra / function-sampled / tabular — ticket
# #000030 Phases 4-7 + last-stub graduation. Each closes one more
# modality the substrate paper reserved.
"calculus",
"linear-algebra",
"function-sampled",
"tabular",
# Pure-integer counting kernel — combinatorics@v1 (ticket #000032).
# Tighter sibling of symbolic_algebra; fail-closed on non-integer
# outputs.
"combinatorics",
})
def validate_carrier(task: dict) -> Optional[str]:
"""Validate the task's ``carrier`` field against the Phase-1 whitelist.
Returns ``None`` if the carrier is allowed (or absent — defaults
to ``"text"`` for backward compat). Returns a reason string if
the carrier is set to something Phase-1 doesn't support, so the
caller can mark the task ``failed`` with
``reason="unsupported_carrier"`` per the cross-modality
discipline.
"""
carrier = task.get("carrier")
if carrier is None:
# Phase-1a fixtures have no carrier field; default to "text".
return None
if not isinstance(carrier, str):
return f"unsupported_carrier: non-string carrier {carrier!r}"
if carrier in PHASE_1_CARRIERS:
return None
return f"unsupported_carrier: {carrier!r} not in Phase-1 whitelist"