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.
This commit is contained in:
russell@unturf.com 2026-05-09 13:20:29 -04:00
parent 70ffc01ce4
commit 7b7ac3867d
No known key found for this signature in database
9 changed files with 446 additions and 6 deletions

View file

@ -292,6 +292,12 @@ bench-5s-algebra: bootstrap-math ## 5S algebra-symbolic π* (ticket #000030 Phas
PYTHONUNBUFFERED=1 $(PY) -m bench.batteries.runner --battery 5s --sub semantics \
--fixtures bench/fixtures/5s/semantics-algebra-symbolic-v1.jsonl
bench-5s-combinatorics: bootstrap-math ## 5S combinatorics π* (ticket #000032; pure-integer counting kernel)
PYTHONUNBUFFERED=1 $(PY) -m bench.batteries.runner --battery 5s --sub syntax \
--fixtures bench/fixtures/5s/syntax-combinatorics-v1.jsonl
PYTHONUNBUFFERED=1 $(PY) -m bench.batteries.runner --battery 5s --sub semantics \
--fixtures bench/fixtures/5s/semantics-combinatorics-v1.jsonl
bench-5s-time-series: bootstrap ## 5S time-series-quantized π* (SQD §13.5; quantized integer-vector canonicalizer)
PYTHONUNBUFFERED=1 $(PY) -m bench.batteries.runner --battery 5s --sub syntax \
--fixtures bench/fixtures/5s/syntax-time-series-v1.jsonl

View file

@ -29,6 +29,10 @@ Concrete π*'s shipped today (alphabetical):
Optional; gates on ``sympy``.
- ``claim-lattice@v1`` claim lines JSON parsed-claim list.
- ``code-py-ast@v1`` Python source canonical AST S-expression.
- ``combinatorics@v1`` pure-integer counting kernel (binomial,
factorial, Catalan, Bell, partition, ). Fail-closed on
symbolic / negative / non-integer outputs. Tighter sibling of
``algebra-symbolic@v1``. Optional; gates on ``sympy``.
- ``function-sampled@v1`` symbolic expression + sample grid
quantized integer-vector signature in time-series-quantized@v1
format. Optional; gates on ``sympy``.
@ -77,6 +81,7 @@ from arborist.pi_star import calculus_limit # noqa: F401,E402
from arborist.pi_star import calculus_series # noqa: F401,E402
from arborist.pi_star import claim_lattice # noqa: F401,E402
from arborist.pi_star import code # noqa: F401,E402
from arborist.pi_star import combinatorics # noqa: F401,E402
from arborist.pi_star import function_sampled # noqa: F401,E402
from arborist.pi_star import linear_algebra # noqa: F401,E402
from arborist.pi_star import logic # noqa: F401,E402

View file

@ -0,0 +1,150 @@
"""``combinatorics@v1`` π* — pure-integer counting kernel.
Domain: ``combinatorics``. A tighter sibling of
``algebra-symbolic@v1``: same input parser (SymPy ``sympify``),
narrower output discipline. Any input whose canonical reduction is
not a non-negative ``sp.Integer`` raises :class:`PiStarError`.
Why this matters
----------------
Ticket #000032. ``algebra-symbolic@v1`` already accepts inputs
like ``binomial(5, 2)`` and returns ``Integer(10)``, but it
silently accepts cases that fall outside classical counting
semantics:
- Symbolic inputs (``binomial(n, k)`` ``binomial(n, k)``) no
concrete count is implied; the answer is opaque.
- Generalized inputs (``binomial(-3, 2) 6``,
``binomial(Rational(1,2), 3) 1/16``) SymPy extends
combinatorial primitives via the Gamma function; classical
counting interpretation rejects negative or non-integer
arguments.
A combinatorics kernel should fail closed on all of these. That
discipline is what distinguishes ``combinatorics@v1`` from the
expand-only sibling.
Allowed surface
---------------
SymPy combinatorial primitives that produce non-negative integers
on integer inputs: ``binomial``, ``factorial``, ``ff`` (falling),
``rf`` (rising), ``catalan``, ``bell``, ``stirling``,
``partition``. Plus arithmetic compositions over those primitives:
``3*binomial(5, 2) + factorial(4) = 54`` is accepted and
canonicalizes to ``b"54"``.
Rejected (raises :class:`PiStarError`)
--------------------------------------
- Symbolic results (free symbols remain after simplify).
- Negative integer results (counting domain).
- Non-integer results (rationals, floats, complex).
- Boolean / relational inputs (use ``logic-kernel@v1``).
- Empty / unparseable inputs.
Output canonical bytes
----------------------
``str(int(reduced)).encode("utf-8")`` a plain decimal literal
like ``b"10"``, ``b"5040"``. Compose with ``arithmetic@v1`` for
byte-identical agreement with the rational route
(``b"10/1"``); the multi-modality witness (#000028) uses that
composition to pin equivalence-class agreement when both routes
fire on the same question.
Round-trip property
-------------------
Idempotent: ``canonicalize(canonicalize(x))`` matches
``canonicalize(x)`` because the output is a plain decimal literal,
which sympify parses as the same ``Integer`` and simplify is a
no-op on ``Integer``.
Optional dependency
-------------------
SymPy via the ``[math]`` extras (``pip install 'arborist[math]'``).
When SymPy is absent, :func:`canonicalize` raises ``PiStarError``
rather than crashing at import. Tests gate on
:func:`pytest.importorskip("sympy")`.
Source: ticket #000032 — landed 2026-05-09.
"""
from __future__ import annotations
from dataclasses import dataclass
from arborist.pi_star.protocol import PiStarError
from arborist.pi_star.registry import register
try:
import sympy as sp # type: ignore[import-not-found]
except ImportError: # pragma: no cover — optional extra
sp = None # type: ignore[assignment]
_SYMPY_REQUIRED_MSG = (
"combinatorics@v1 requires sympy; install with "
"`pip install 'arborist[math]'`"
)
@dataclass
class CombinatoricsV1:
name: str = "combinatorics"
version: str = "v1"
domain: str = "combinatorics"
def canonicalize(self, raw: bytes) -> bytes:
if sp is None:
raise PiStarError(_SYMPY_REQUIRED_MSG)
if not isinstance(raw, (bytes, bytearray)):
raise PiStarError(
"combinatorics@v1 expects bytes; got "
f"{type(raw).__name__}"
)
try:
text = raw.decode("utf-8", errors="surrogatepass")
except UnicodeDecodeError as exc: # pragma: no cover — defensive
raise PiStarError(f"input not valid UTF-8: {exc}") from exc
text = text.strip()
if not text:
raise PiStarError("combinatorics@v1 input is empty")
try:
expr = sp.sympify(text)
except (sp.SympifyError, SyntaxError, TypeError) as exc:
raise PiStarError(
f"combinatorics@v1 cannot parse {text!r}: {exc}"
) from exc
# Reject relationals + boolean operators; same Expr-vs-Boolean
# filter as algebra_symbolic.py (Symbol inherits from Boolean,
# so the right rejection is "not an Expr" rather than "is Boolean").
if not isinstance(expr, sp.Expr):
raise PiStarError(
f"combinatorics@v1 rejects boolean/relational input "
f"{text!r}; use logic-kernel@v1 for that shape"
)
try:
reduced = sp.simplify(expr)
except (TypeError, ValueError) as exc:
raise PiStarError(
f"combinatorics@v1 simplify failed on {text!r}: {exc}"
) from exc
if not isinstance(reduced, sp.Integer):
raise PiStarError(
f"combinatorics@v1 result is not a concrete integer: "
f"{reduced!r} (input was {text!r})"
)
if reduced < 0:
raise PiStarError(
f"combinatorics@v1 result is negative: {int(reduced)} "
f"(input was {text!r})"
)
return str(int(reduced)).encode("utf-8")
if sp is not None:
register(CombinatoricsV1())

View file

@ -129,6 +129,10 @@ PHASE_1_CARRIERS = frozenset({
"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",
})

View file

@ -0,0 +1,13 @@
{"_meta":{"battery":"5s","sub_battery":"semantics","version":"v1","task_count":12,"notes":"combinatorics@v1 equivalence-class tests. Equal counts collapse to identical bytes (decimal literal); distinct counts do not. Includes binomial symmetry C(n,k)=C(n,n-k) and Pascal's rule C(n,k) = C(n-1,k-1) + C(n-1,k)."}}
{"id":"5s-sem-comb-001","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"combinatorics","domain":"counting","pi_star_ref":"combinatorics@v1","input_a":"binomial(5,2)","input_b":"10","expected_equivalent":true}
{"id":"5s-sem-comb-002","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"combinatorics","domain":"counting","pi_star_ref":"combinatorics@v1","input_a":"binomial(7,3)","input_b":"binomial(7,4)","expected_equivalent":true}
{"id":"5s-sem-comb-003","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"combinatorics","domain":"counting","pi_star_ref":"combinatorics@v1","input_a":"binomial(7,3)","input_b":"binomial(6,2) + binomial(6,3)","expected_equivalent":true}
{"id":"5s-sem-comb-004","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"combinatorics","domain":"counting","pi_star_ref":"combinatorics@v1","input_a":"factorial(0)","input_b":"1","expected_equivalent":true}
{"id":"5s-sem-comb-005","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"combinatorics","domain":"counting","pi_star_ref":"combinatorics@v1","input_a":"binomial(5,2)","input_b":"factorial(5)/(factorial(2)*factorial(3))","expected_equivalent":true}
{"id":"5s-sem-comb-006","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"combinatorics","domain":"counting","pi_star_ref":"combinatorics@v1","input_a":"catalan(5)","input_b":"binomial(10,5)/(5+1)","expected_equivalent":true}
{"id":"5s-sem-comb-007","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"combinatorics","domain":"counting","pi_star_ref":"combinatorics@v1","input_a":"binomial(0,0)","input_b":"binomial(7,7)","expected_equivalent":true}
{"id":"5s-sem-comb-008","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"combinatorics","domain":"counting","pi_star_ref":"combinatorics@v1","input_a":"binomial(5,7)","input_b":"0","expected_equivalent":true}
{"id":"5s-sem-comb-009","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"combinatorics","domain":"counting","pi_star_ref":"combinatorics@v1","input_a":"factorial(5)","input_b":"factorial(6)","expected_equivalent":false}
{"id":"5s-sem-comb-010","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"combinatorics","domain":"counting","pi_star_ref":"combinatorics@v1","input_a":"binomial(7,2)","input_b":"binomial(8,2)","expected_equivalent":false}
{"id":"5s-sem-comb-011","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"combinatorics","domain":"counting","pi_star_ref":"combinatorics@v1","input_a":"catalan(5)","input_b":"catalan(6)","expected_equivalent":false}
{"id":"5s-sem-comb-012","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"combinatorics","domain":"counting","pi_star_ref":"combinatorics@v1","input_a":"partition(5)","input_b":"partition(7)","expected_equivalent":false}

View file

@ -0,0 +1,11 @@
{"_meta":{"battery":"5s","sub_battery":"syntax","version":"v1","task_count":10,"notes":"combinatorics@v1 parse-pass tests. Each input is a counting expression that reduces to a non-negative integer; the kernel canonicalizes without raising. Reject-paths (symbolic, negative, non-integer) live in tests/test_pi_star_combinatorics.py per the syntax-fixture convention."}}
{"id":"5s-syn-comb-001","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"combinatorics","domain":"counting","pi_star_ref":"combinatorics@v1","input":"binomial(5,2)","expected":"pass"}
{"id":"5s-syn-comb-002","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"combinatorics","domain":"counting","pi_star_ref":"combinatorics@v1","input":"factorial(7)","expected":"pass"}
{"id":"5s-syn-comb-003","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"combinatorics","domain":"counting","pi_star_ref":"combinatorics@v1","input":"binomial(0,0)","expected":"pass"}
{"id":"5s-syn-comb-004","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"combinatorics","domain":"counting","pi_star_ref":"combinatorics@v1","input":"factorial(0)","expected":"pass"}
{"id":"5s-syn-comb-005","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"combinatorics","domain":"counting","pi_star_ref":"combinatorics@v1","input":"binomial(5,7)","expected":"pass"}
{"id":"5s-syn-comb-006","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"combinatorics","domain":"counting","pi_star_ref":"combinatorics@v1","input":"catalan(5)","expected":"pass"}
{"id":"5s-syn-comb-007","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"combinatorics","domain":"counting","pi_star_ref":"combinatorics@v1","input":"bell(5)","expected":"pass"}
{"id":"5s-syn-comb-008","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"combinatorics","domain":"counting","pi_star_ref":"combinatorics@v1","input":"partition(7)","expected":"pass"}
{"id":"5s-syn-comb-009","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"combinatorics","domain":"counting","pi_star_ref":"combinatorics@v1","input":"3*binomial(5,2) + factorial(4)","expected":"pass"}
{"id":"5s-syn-comb-010","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"combinatorics","domain":"counting","pi_star_ref":"combinatorics@v1","input":"100","expected":"pass"}

View file

@ -62,7 +62,7 @@ Newest first. Update on every open/close.
| ID | Title | Status | Opened | Directive |
|----------|------------------------------------------------|-----------------------|------------|-----------|
| #000033 | Claim-pack pillar VII (combinatorics) | open · awaiting go/no-go | 2026-05-09 | — |
| #000032 | combinatorics@v1 π* (integer counting kernel) | open · awaiting go/no-go | 2026-05-09 | — |
| #000032 | combinatorics@v1 π* (integer counting kernel) | closed · landed 2026-05-09 | 2026-05-09 | — |
| #000031 | Surface-ingest cited textbooks for claim-pack warrant promotion | open · awaiting go/no-go | 2026-05-09 | — |
| #000030 | Math π* expansion: SymPy substrate (algebra · calculus · linalg) | closed · Phases 1+2+1b+3 landed 2026-05-09 (4-7 future work) | 2026-05-09 | — |
| #000029 | Claim-pack source (axiom/theorem JSON bundles) | closed · landed 2026-05-09 | 2026-05-09 | — |

View file

@ -1,6 +1,6 @@
# Ticket #000032 — combinatorics@v1 π*
**Status:** open · awaiting go/no-go
**Status:** closed · landed 2026-05-09
**Opened:** 2026-05-09
**Scope:** A new π* kernel that canonicalizes pure-integer
counting expressions — binomials, factorials, permutations,
@ -342,8 +342,42 @@ def test_composes_with_arithmetic(ps):
## 8. Status
Open · awaiting go/no-go.
**Landed 2026-05-09 in a single commit.**
Estimated size: ~120 LOC module + ~80 LOC tests + ~22 fixtures +
~5 LOC carrier-whitelist + ~5 LOC Makefile. Single-commit feasible
alongside #000033 if both land together; otherwise standalone.
Landed scope:
- `arborist/pi_star/combinatorics.py``CombinatoricsV1` class.
Parser is `sp.sympify`; reduction is `sp.simplify`; output filter
is `isinstance(reduced, sp.Integer) and reduced >= 0`. Emits a
plain decimal literal (`b"10"`).
- `arborist/pi_star/__init__.py` — registers the module at package
load, alphabetical between `code` and `function_sampled`.
- `bench/fixtures/5s/syntax-combinatorics-v1.jsonl` — 10 fixtures.
- `bench/fixtures/5s/semantics-combinatorics-v1.jsonl` — 12
fixtures 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), and the C(n,k) =
factorial(n)/(factorial(k)·factorial(n-k)) identity.
- `bench/batteries/base.py PHASE_1_CARRIERS` gains
`"combinatorics"`.
- `Makefile bench-5s-combinatorics` target — 100% pass on both
syntax and semantics fixtures.
- `tests/test_pi_star_combinatorics.py` — 43 tests covering
integer collapse, equivalence-class behavior (binomial
symmetry, Pascal's rule), distinct-counts-stay-distinct,
round-trip idempotence, all fail-closed paths (symbolic /
negative / non-integer / parse / shape), and the
`combinatorics@v1 ∘ arithmetic@v1` byte-identical-witness
composition.
- Full test suite: 1537 passed / 28 skipped.
One design decision worth noting: `binomial(-3, 2) = 6` is
ACCEPTED by the kernel because the OUTPUT is integer 6, not the
input. The fail-closed rule is on output shape (Integer ≥ 0), not
input range. Documented as an explicit boundary test in
`test_generalized_binomial_negative_args_accepted_when_integer`.
A stricter "classical-counting-domain" variant could reject
negative arguments at the input layer; reserved for a future
ticket if a consumer needs it.
Phase 2 (claim-pack pillar VII binding) lives in #000033, which
can now bind records to `combinatorics@v1` from day one.

View file

@ -0,0 +1,217 @@
"""combinatorics@v1 π* tests (ticket #000032).
Pure-integer counting kernel that fails closed on symbolic /
negative / non-integer outputs. Whole file skips when SymPy is
absent.
"""
from __future__ import annotations
import pytest
sympy = pytest.importorskip("sympy") # entire file skipped if absent
from arborist.pi_star import compose, get # noqa: E402
from arborist.pi_star.protocol import ( # noqa: E402
PiStarError,
assert_round_trip,
equivalence_class_id,
)
@pytest.fixture
def ps():
return get("combinatorics@v1")
# --- registry presence ------------------------------------------------
def test_registry_contains_combinatorics():
ps = get("combinatorics@v1")
assert ps.name == "combinatorics"
assert ps.version == "v1"
assert ps.domain == "combinatorics"
# --- positive cases — integer collapse -------------------------------
@pytest.mark.parametrize(
"input_str,expected_int",
[
("binomial(5,2)", 10),
("binomial(10,3)", 120),
("factorial(0)", 1),
("factorial(1)", 1),
("factorial(7)", 5040),
("binomial(0,0)", 1),
("binomial(7,0)", 1),
("binomial(7,7)", 1),
("binomial(5,7)", 0), # k > n → 0
("catalan(0)", 1),
("catalan(5)", 42),
("bell(5)", 52),
("partition(7)", 15),
# Arithmetic compositions over integer primitives.
("3*binomial(5,2) + factorial(4)", 54),
("2**10", 1024),
("100", 100),
],
)
def test_integer_collapse(ps, input_str, expected_int):
assert ps.canonicalize(input_str.encode()) == str(expected_int).encode()
def test_byte_format_is_plain_decimal(ps):
"""Output must be the bare decimal literal — no quotes, no
Integer(...) wrapper, no fraction-form denominator."""
out = ps.canonicalize(b"binomial(5,2)")
assert out == b"10"
assert b"/" not in out
assert b"Integer" not in out
# --- equivalence classes preserved -----------------------------------
def test_binomial_symmetry_collapses(ps):
"""C(n, k) = C(n, n-k) — same canonical bytes."""
assert ps.canonicalize(b"binomial(7, 3)") == ps.canonicalize(b"binomial(7, 4)")
assert (
equivalence_class_id(ps, b"binomial(7, 3)")
== equivalence_class_id(ps, b"binomial(7, 4)")
)
def test_pascals_rule_holds(ps):
"""Pascal's rule: C(n,k) = C(n-1,k-1) + C(n-1,k)."""
lhs = ps.canonicalize(b"binomial(7, 3)")
rhs = ps.canonicalize(b"binomial(6, 2) + binomial(6, 3)")
assert lhs == rhs
# --- distinct counts stay distinct -----------------------------------
@pytest.mark.parametrize(
"left,right",
[
# Note: binomial(5,2) = binomial(5,3) by symmetry — pick a pair
# that's actually distinct.
("binomial(5, 2)", "binomial(7, 2)"),
("factorial(5)", "factorial(6)"),
("catalan(5)", "catalan(6)"),
("partition(5)", "partition(7)"),
],
)
def test_distinct_counts_distinct(ps, left, right):
assert ps.canonicalize(left.encode()) != ps.canonicalize(right.encode())
# --- round-trip / idempotence ----------------------------------------
@pytest.mark.parametrize(
"expr",
[
"binomial(5, 2)",
"factorial(7)",
"100",
"2**10",
"3*binomial(5, 2) + factorial(4)",
],
)
def test_round_trip_idempotent(ps, expr):
assert_round_trip(ps, expr.encode())
# --- fail-closed: symbolic results -----------------------------------
@pytest.mark.parametrize(
"expr",
[
"binomial(n, k)", # both symbolic
"factorial(n)", # symbolic
"factorial(n + 1)", # symbolic
"binomial(5, k)", # one symbolic
"x + 1", # not combinatorial at all, still symbolic
],
)
def test_symbolic_input_rejected(ps, expr):
with pytest.raises(PiStarError, match="not a concrete integer"):
ps.canonicalize(expr.encode())
# --- fail-closed: non-integer / generalized inputs -------------------
def test_negative_result_rejected(ps):
"""Hand-crafted: factorial(4) - 100 = -76 → counting domain rejects."""
with pytest.raises(PiStarError, match="negative"):
ps.canonicalize(b"factorial(4) - 100")
def test_generalized_binomial_non_integer_rejected(ps):
"""binomial(Rational(1,2), 3) = 1/16 — SymPy supports the
generalized binomial via Gamma; combinatorics@v1 rejects
non-integer outputs."""
with pytest.raises(PiStarError, match="not a concrete integer"):
ps.canonicalize(b"binomial(Rational(1,2), 3)")
def test_rational_arithmetic_rejected(ps):
"""1/2 reduces to a Rational — not an Integer, rejected."""
with pytest.raises(PiStarError, match="not a concrete integer"):
ps.canonicalize(b"1/2")
def test_generalized_binomial_negative_args_accepted_when_integer(ps):
"""SymPy's binomial extends to negative integers via Gamma; the
output of binomial(-3, 2) is the integer 6. Counting-domain
semantics would arguably reject negative-argument binomials, but
the kernel's fail-closed rule is on the OUTPUT shape (integer
vs. not), not input. Document the boundary explicitly."""
# binomial(-3, 2) = 6 as an integer — the kernel accepts.
out = ps.canonicalize(b"binomial(-3, 2)")
assert out == b"6"
# --- fail-closed: parse / shape errors -------------------------------
def test_empty_input_raises(ps):
with pytest.raises(PiStarError, match="empty"):
ps.canonicalize(b"")
with pytest.raises(PiStarError, match="empty"):
ps.canonicalize(b" \n\t ")
def test_unparseable_input_raises(ps):
with pytest.raises(PiStarError, match="cannot parse"):
ps.canonicalize(b"$$$ % nope")
def test_non_bytes_input_raises(ps):
with pytest.raises(PiStarError, match="expects bytes"):
ps.canonicalize("not bytes") # type: ignore[arg-type]
def test_relational_input_rejected(ps):
with pytest.raises(PiStarError, match="boolean/relational"):
ps.canonicalize(b"x > 0")
# --- composition -----------------------------------------------------
def test_composes_with_arithmetic_for_byte_identical_witness():
"""combinatorics@v1 ∘ arithmetic@v1 — counting output (b"10")
becomes arithmetic-route bytes (b"10/1") so the multi-modality
witness can pin equivalence-class agreement when both routes
fire on the same question."""
chain = compose("combinatorics@v1", "arithmetic@v1")
assert chain.canonicalize(b"binomial(5, 2)") == b"10/1"
assert chain.canonicalize(b"factorial(7)") == b"5040/1"
assert chain.canonicalize(b"binomial(0, 0)") == b"1/1"