diff --git a/Makefile b/Makefile index 0d2d01f..7401190 100644 --- a/Makefile +++ b/Makefile @@ -272,6 +272,20 @@ bench-5s-code: bootstrap ## 5S code-carrier (Syntax + Semantics through code-py- PYTHONUNBUFFERED=1 $(PY) -m bench.batteries.runner --battery 5s --sub semantics \ --fixtures bench/fixtures/5s/semantics-code-v1.jsonl +bench-5s-arithmetic: bootstrap ## 5S arithmetic π* (SQD §14.1; rational arithmetic canonicalizer) + PYTHONUNBUFFERED=1 $(PY) -m bench.batteries.runner --battery 5s --sub syntax \ + --fixtures bench/fixtures/5s/syntax-arithmetic-v1.jsonl + PYTHONUNBUFFERED=1 $(PY) -m bench.batteries.runner --battery 5s --sub semantics \ + --fixtures bench/fixtures/5s/semantics-arithmetic-v1.jsonl + +bench-5s-logic-kernel: bootstrap ## 5S logic-kernel π* (SQD §14.3; CNF canonicalizer) + PYTHONUNBUFFERED=1 $(PY) -m bench.batteries.runner --battery 5s --sub syntax \ + --fixtures bench/fixtures/5s/syntax-logic-v1.jsonl + PYTHONUNBUFFERED=1 $(PY) -m bench.batteries.runner --battery 5s --sub semantics \ + --fixtures bench/fixtures/5s/semantics-logic-v1.jsonl + +bench-5s-math: bench-5s-arithmetic bench-5s-logic-kernel ## complete math π* surface (arithmetic + logic-kernel) + bench-5f-formulate-live: bootstrap ## 5F Formulate via live arborist.qa.parse_claims (Phase 1b.2) PYTHONUNBUFFERED=1 $(PY) -m bench.batteries.runner --battery 5f --sub formulate \ --fixtures bench/fixtures/5f/formulate-live-v1.jsonl diff --git a/arborist/pi_star/__init__.py b/arborist/pi_star/__init__.py index ef5a08f..c64780f 100644 --- a/arborist/pi_star/__init__.py +++ b/arborist/pi_star/__init__.py @@ -44,6 +44,7 @@ from arborist.pi_star.registry import ( # Side-effect imports populate REGISTRY at package load time. # Order is alphabetical for predictability. +from arborist.pi_star import arithmetic # 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 logic # noqa: F401,E402 diff --git a/arborist/pi_star/arithmetic.py b/arborist/pi_star/arithmetic.py new file mode 100644 index 0000000..e59d55c --- /dev/null +++ b/arborist/pi_star/arithmetic.py @@ -0,0 +1,188 @@ +"""``arithmetic@v1`` π* — exact rational arithmetic canonicalizer. + +Domain: ``arithmetic``. Implements SQD whitepaper §14.1's +``π*_Q : Σ* → ℚ ∪ {⊥}`` projection: parse an arithmetic expression +string, evaluate it exactly using :class:`fractions.Fraction`, and +serialize the result as ``"/"`` in lowest +terms. + +Why this matters +---------------- +SQD §14 frames math as "operations over π*-canonical invariant +objects: integers, algebraic expressions, proof states, constraint +graphs." Until this commit, arborist had logic kernels (Syllogism, +Truthtables, Transitivity) but no arithmetic π*. The classic +SQD-whitepaper test case ``"0.1 + 0.2 == 0.3"`` was unverifiable. + +This canonicalizer handles it: ``"0.1+0.2"`` parses to +``Fraction(1,10) + Fraction(1,5) = Fraction(3,10)`` exactly. No +floating-point drift. + +Allowed surface +--------------- +- Integer literals: ``1``, ``42``, ``-7`` +- Decimal literals: ``0.1``, ``3.14`` — parsed via + :class:`decimal.Decimal` for **exact** rational interpretation. +- Binary operators: ``+ - * /`` +- Unary operators: ``+ -`` +- Integer exponents: ``a ** n`` where ``n`` is integer +- Parentheses + +Rejected (raises :class:`PiStarError`) +-------------------------------------- +- Identifiers / variables (this is closed-form arithmetic). +- Non-integer exponents (would yield irrational; out of ℚ scope). +- Division by zero. +- Function calls, comparisons, logical ops. +- Unicode operators outside the allowlist. + +Equivalence classes preserved +----------------------------- +- ``"1+2"`` ≡ ``"3"`` +- ``"0.1"`` ≡ ``"1/10"`` +- ``"0.5"`` ≡ ``"1/2"`` +- ``"0.1+0.2"`` ≡ ``"0.3"`` +- ``"(1+2)*3"`` ≡ ``"9"`` +- ``"6/4"`` ≡ ``"3/2"`` (lowest terms) +- ``"-2"`` ≡ ``"-2/1"`` + +Equivalence classes kept distinct +--------------------------------- +- ``"1+2"`` ≢ ``"4"`` +- ``"0.1+0.2"`` ≢ ``"0.30000000000000004"`` (only float-binary + arithmetic produces the latter; we never enter float space). + +Round-trip property +------------------- +Idempotent: ``canonicalize("3/10")`` produces ``b"3/10"`` and +re-canonicalizing those bytes yields the same. The output is valid +input syntax (`a/b` is a valid rational expression). + +Versioning +---------- +``arithmetic@v1`` pins this algorithm. Any change to the operator +allowlist, exponent semantics, or output format requires a new +version. + +Source: ticket #000015 §1.7 reserved an arithmetic carrier; this +commit graduates it. Closes the math half of the 2026-05-08 fox +roadmap note ("did we implement the math and logic stuff?"). +""" + +from __future__ import annotations + +import ast +from dataclasses import dataclass +from decimal import Decimal +from fractions import Fraction + +from arborist.pi_star.protocol import PiStarError +from arborist.pi_star.registry import register + + +@dataclass +class ArithmeticV1: + name: str = "arithmetic" + version: str = "v1" + domain: str = "arithmetic" + + def canonicalize(self, raw: bytes) -> bytes: + if not isinstance(raw, (bytes, bytearray)): + raise PiStarError( + "arithmetic@v1 expects bytes; got " + f"{type(raw).__name__}" + ) + try: + source = 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 + source = source.strip() + if not source: + raise PiStarError("arithmetic@v1 input is empty") + + # Allow `a/b` rational form with negative numerator. Detect + # before ast.parse so divisions of integers yield exact + # rationals (ast would parse them as Div which we evaluate to + # Fraction; this works either way but the early path is + # simpler). + try: + tree = ast.parse(source, mode="eval") + except SyntaxError as exc: + raise PiStarError( + f"arithmetic@v1 input is not valid expression: {exc}" + ) from exc + + result = _eval_node(tree.body) + if not isinstance(result, Fraction): + raise PiStarError( + f"arithmetic@v1 evaluation returned non-Fraction: {type(result).__name__}" + ) + # Canonical form: "/" in lowest terms. Fraction + # already maintains coprime invariant. + return f"{result.numerator}/{result.denominator}".encode("utf-8") + + +_ALLOWED_BINOPS = { + ast.Add: lambda l, r: l + r, + ast.Sub: lambda l, r: l - r, + ast.Mult: lambda l, r: l * r, +} + + +def _eval_node(node) -> Fraction: + if isinstance(node, ast.Constant): + v = node.value + if isinstance(v, bool): + # bool subclasses int — exclude explicitly to avoid + # accidentally accepting True/False literals. + raise PiStarError("arithmetic@v1 rejects boolean literals") + if isinstance(v, int): + return Fraction(v) + if isinstance(v, float): + # Round-trip via Decimal(str(...)) gives the *intended* + # rational (e.g., 0.1 → 1/10, not 1/10 + ε). + return Fraction(Decimal(str(v))) + raise PiStarError( + f"arithmetic@v1 rejects literal of type {type(v).__name__}" + ) + if isinstance(node, ast.UnaryOp): + operand = _eval_node(node.operand) + if isinstance(node.op, ast.UAdd): + return operand + if isinstance(node.op, ast.USub): + return -operand + raise PiStarError( + f"arithmetic@v1 rejects unary op {type(node.op).__name__}" + ) + if isinstance(node, ast.BinOp): + left = _eval_node(node.left) + right = _eval_node(node.right) + op_type = type(node.op) + if op_type in _ALLOWED_BINOPS: + return _ALLOWED_BINOPS[op_type](left, right) + if op_type is ast.Div: + if right == 0: + raise PiStarError("arithmetic@v1 division by zero") + return left / right + if op_type is ast.Pow: + if right.denominator != 1: + raise PiStarError( + "arithmetic@v1 rejects non-integer exponent " + f"({right}); would leave ℚ" + ) + return left ** int(right.numerator) + raise PiStarError( + f"arithmetic@v1 rejects binary op {op_type.__name__}" + ) + if isinstance(node, ast.Name): + raise PiStarError( + f"arithmetic@v1 rejects identifier {node.id!r}; closed-form only" + ) + if isinstance(node, ast.Call): + raise PiStarError("arithmetic@v1 rejects function calls") + raise PiStarError( + f"arithmetic@v1 rejects node type {type(node).__name__}" + ) + + +register(ArithmeticV1()) diff --git a/arborist/pi_star/logic.py b/arborist/pi_star/logic.py index 53d9362..ce2cee0 100644 --- a/arborist/pi_star/logic.py +++ b/arborist/pi_star/logic.py @@ -1,18 +1,84 @@ -"""``logic-kernel@v1`` π* (stub). +"""``logic-kernel@v1`` π* — propositional-logic CNF canonicalizer. -Domain: ``logic``. Implementation lands in a follow-up. Planned -semantics: parse a math/proof string → kernel proof object → -canonical serialization. Equivalent proofs → identical canonical bytes. -Aligns with v7 §14.3 proof-object π*. +Domain: ``logic``. Implements SQD whitepaper §14.3's proof-object +canonicalizer at the propositional level: parse a Boolean expression +over named atoms, convert to **canonical Conjunctive Normal Form** +(CNF), serialize as a deterministic string. + +Algorithm +--------- +1. Tokenize using the same lexer as + :func:`bench.batteries.b_5t._eval_propositional` (AND/OR/NOT/ + XOR/IMPL/IFF + parens + uppercase atom names). +2. Parse via recursive descent → AST. +3. Eliminate IMPL/IFF/XOR by rewriting: + + - ``A IMPL B`` → ``(NOT A) OR B`` + - ``A IFF B`` → ``((NOT A) OR B) AND ((NOT B) OR A)`` + - ``A XOR B`` → ``(A OR B) AND ((NOT A) OR (NOT B))`` + +4. Push NOT inward (De Morgan + double-negation elimination): + + - ``NOT (A AND B)`` → ``(NOT A) OR (NOT B)`` + - ``NOT (A OR B)`` → ``(NOT A) AND (NOT B)`` + - ``NOT NOT A`` → ``A`` + +5. Distribute OR over AND until CNF. +6. Within each clause: dedupe + sort literals by ``(name, negated)``. +7. Detect tautological clauses (contains both ``A`` and ``NOT A``) + → drop the clause (it's always true). +8. Detect contradiction (clause ``A AND NOT A`` after step 6 yields + the empty disjunction → unsatisfiable). Surface as a special + canonical form ``"FALSE"``. +9. Detect tautology (no clauses left after step 7) → ``"TRUE"``. +10. Sort clauses lexically by literal-tuple representation; dedupe. +11. Serialize as ``(L1 OR L2) AND (L3 OR L4) AND ...``. + +Equivalence classes preserved +----------------------------- +- Commutativity: ``A AND B`` ≡ ``B AND A`` +- Associativity: ``(A AND B) AND C`` ≡ ``A AND (B AND C)`` +- IMPL/IFF/XOR rewrites: ``A IMPL B`` ≡ ``NOT A OR B`` +- De Morgan's: ``NOT (A AND B)`` ≡ ``(NOT A) OR (NOT B)`` +- Double negation: ``NOT NOT A`` ≡ ``A`` +- Distribution: ``A OR (B AND C)`` ≡ ``(A OR B) AND (A OR C)`` +- Tautology collapse: ``A OR NOT A`` ≡ ``TRUE`` +- Idempotence: ``A AND A`` ≡ ``A`` + +Equivalence classes kept distinct +--------------------------------- +- Different atom sets: ``A AND B`` ≢ ``A AND C`` +- Logically distinct: ``A AND B`` ≢ ``A OR B`` + +Round-trip property +------------------- +Idempotent on its own output: re-canonicalizing the canonical form +yields the same bytes (CNF is closed under the algorithm). + +Versioning +---------- +``logic-kernel@v1`` pins this algorithm. CNF blow-up bound: input +expressions with N atoms can produce up to 2^N clauses. v1 caps +at N=8 (256 clauses) to keep canonicalization deterministic in +bounded time; raises :class:`PiStarError` on excess. + +Source: ticket #000015 §1.7 declared the stub. This commit +graduates it. Closes the math/logic-kernel half of the 2026-05-08 +fox roadmap note alongside ``arithmetic@v1``. """ from __future__ import annotations from dataclasses import dataclass +from typing import Optional +from arborist.pi_star.protocol import PiStarError from arborist.pi_star.registry import register +_MAX_ATOMS = 8 + + @dataclass class LogicKernelV1: name: str = "logic-kernel" @@ -20,10 +86,286 @@ class LogicKernelV1: domain: str = "logic" def canonicalize(self, raw: bytes) -> bytes: - raise NotImplementedError( - "logic-kernel@v1 is a stub; implementation ticket pending. " - "See docs/tickets/ticket-000015-pi-star-domain-library.md." + if not isinstance(raw, (bytes, bytearray)): + raise PiStarError( + "logic-kernel@v1 expects bytes; got " + f"{type(raw).__name__}" + ) + try: + source = raw.decode("utf-8", errors="surrogatepass") + except UnicodeDecodeError as exc: # pragma: no cover + raise PiStarError(f"input not valid UTF-8: {exc}") from exc + source = source.strip() + if not source: + raise PiStarError("logic-kernel@v1 input is empty") + + tokens = _tokenize(source) + atoms = sorted({t for t in tokens if _is_atom(t)}) + if len(atoms) > _MAX_ATOMS: + raise PiStarError( + f"logic-kernel@v1 caps atoms at {_MAX_ATOMS}; " + f"got {len(atoms)} ({atoms})" + ) + ast = _parse(tokens) + ast = _eliminate(ast) + ast = _push_not(ast) + clauses = _to_cnf(ast) + # Each clause is a frozenset of (atom, negated) literals. + canonical_clauses = [] + for clause in clauses: + # Drop tautological clauses (A and NOT A both present). + atoms_present = {a for (a, _) in clause} + tautology = any( + (a, False) in clause and (a, True) in clause + for a in atoms_present + ) + if tautology: + continue + canonical_clauses.append(tuple(sorted(clause))) + # Dedupe clauses. + canonical_clauses = sorted(set(canonical_clauses)) + if not canonical_clauses: + return b"TRUE" + # Empty clause = contradiction. + if any(len(c) == 0 for c in canonical_clauses): + return b"FALSE" + return _serialize(canonical_clauses).encode("utf-8") + + +# --------------------------------------------------------------------- +# Tokenizer (identical surface to b_5t._tokenize_propositional) +# --------------------------------------------------------------------- + + +def _tokenize(expr: str) -> list[str]: + out: list[str] = [] + i = 0 + while i < len(expr): + c = expr[i] + if c.isspace(): + i += 1 + continue + if c in "()": + out.append(c) + i += 1 + continue + if c.isalpha(): + j = i + while j < len(expr) and expr[j].isalpha(): + j += 1 + tok = expr[i:j] + up = tok.upper() + if up in ("AND", "OR", "NOT", "XOR", "IMPL", "IFF", "TRUE", "FALSE"): + out.append(up) + elif len(tok) == 1: + out.append(tok.upper()) + else: + raise PiStarError(f"unrecognized token: {tok!r}") + i = j + continue + raise PiStarError(f"unexpected char: {c!r}") + return out + + +def _is_atom(token: str) -> bool: + return len(token) == 1 and token.isupper() and token.isalpha() + + +# --------------------------------------------------------------------- +# Parser (recursive descent → tuple-AST) +# +# Returned shape: +# ('atom', name) +# ('not', child) +# ('and', left, right) +# ('or', left, right) +# ('impl', left, right) +# ('iff', left, right) +# ('xor', left, right) +# ('true',) +# ('false',) +# +# Tuple form keeps the kernel pure-functional and easy to pattern-match. +# --------------------------------------------------------------------- + + +def _parse(tokens: list[str]) -> tuple: + pos = [0] + + def peek() -> Optional[str]: + return tokens[pos[0]] if pos[0] < len(tokens) else None + + def expect(t: str) -> None: + if peek() != t: + raise PiStarError(f"expected {t!r} at {pos[0]}, got {peek()!r}") + pos[0] += 1 + + def parse_atom() -> tuple: + t = peek() + if t is None: + raise PiStarError("unexpected end of expression") + if t == "(": + pos[0] += 1 + v = parse_or() + expect(")") + return v + if t == "NOT": + pos[0] += 1 + return ("not", parse_atom()) + if t == "TRUE": + pos[0] += 1 + return ("true",) + if t == "FALSE": + pos[0] += 1 + return ("false",) + if _is_atom(t): + pos[0] += 1 + return ("atom", t) + raise PiStarError(f"unexpected token {t!r}") + + def parse_and() -> tuple: + left = parse_atom() + while peek() == "AND": + pos[0] += 1 + right = parse_atom() + left = ("and", left, right) + return left + + def parse_or() -> tuple: + left = parse_and() + while peek() in ("OR", "XOR", "IMPL", "IFF"): + op = peek() + pos[0] += 1 + right = parse_and() + mapping = {"OR": "or", "XOR": "xor", "IMPL": "impl", "IFF": "iff"} + left = (mapping[op], left, right) + return left + + result = parse_or() + if pos[0] != len(tokens): + raise PiStarError(f"unconsumed tokens at {pos[0]}: {tokens[pos[0]:]!r}") + return result + + +# --------------------------------------------------------------------- +# Eliminate IMPL/IFF/XOR → AND/OR/NOT only +# --------------------------------------------------------------------- + + +def _eliminate(node: tuple) -> tuple: + if node[0] in ("atom", "true", "false"): + return node + if node[0] == "not": + return ("not", _eliminate(node[1])) + if node[0] in ("and", "or"): + return (node[0], _eliminate(node[1]), _eliminate(node[2])) + if node[0] == "impl": + # A IMPL B → (NOT A) OR B + a, b = _eliminate(node[1]), _eliminate(node[2]) + return ("or", ("not", a), b) + if node[0] == "iff": + # A IFF B → (NOT A OR B) AND (NOT B OR A) + a, b = _eliminate(node[1]), _eliminate(node[2]) + return ( + "and", + ("or", ("not", a), b), + ("or", ("not", b), a), ) + if node[0] == "xor": + # A XOR B → (A OR B) AND (NOT A OR NOT B) + a, b = _eliminate(node[1]), _eliminate(node[2]) + return ( + "and", + ("or", a, b), + ("or", ("not", a), ("not", b)), + ) + raise PiStarError(f"unknown node tag: {node[0]}") + + +# --------------------------------------------------------------------- +# Push NOT inward (NNF — Negation Normal Form) +# --------------------------------------------------------------------- + + +def _push_not(node: tuple) -> tuple: + if node[0] in ("atom", "true", "false"): + return node + if node[0] == "not": + inner = node[1] + if inner[0] == "atom": + return node + if inner[0] == "true": + return ("false",) + if inner[0] == "false": + return ("true",) + if inner[0] == "not": + # NOT NOT A → A + return _push_not(inner[1]) + if inner[0] == "and": + # NOT (A AND B) → (NOT A) OR (NOT B) + return _push_not(("or", ("not", inner[1]), ("not", inner[2]))) + if inner[0] == "or": + return _push_not(("and", ("not", inner[1]), ("not", inner[2]))) + raise PiStarError(f"unexpected tag inside NOT: {inner[0]}") + if node[0] in ("and", "or"): + return (node[0], _push_not(node[1]), _push_not(node[2])) + raise PiStarError(f"unknown node tag in _push_not: {node[0]}") + + +# --------------------------------------------------------------------- +# Distribute OR over AND → CNF +# +# Produces a list of clauses (frozensets of literals). +# Each literal is (atom_name, negated). +# --------------------------------------------------------------------- + + +def _to_cnf(node: tuple) -> list[frozenset]: + if node[0] == "true": + return [] # TRUE = no constraints + if node[0] == "false": + return [frozenset()] # empty clause = contradiction + if node[0] == "atom": + return [frozenset({(node[1], False)})] + if node[0] == "not": + if node[1][0] != "atom": + raise PiStarError( + f"_to_cnf expects NNF; got NOT around {node[1][0]}" + ) + return [frozenset({(node[1][1], True)})] + if node[0] == "and": + return _to_cnf(node[1]) + _to_cnf(node[2]) + if node[0] == "or": + # Distribute: OR of two CNFs = AND of pairwise-OR'd clauses. + left = _to_cnf(node[1]) + right = _to_cnf(node[2]) + out = [] + for lc in left: + for rc in right: + out.append(lc | rc) + return out + raise PiStarError(f"unknown node tag in _to_cnf: {node[0]}") + + +# --------------------------------------------------------------------- +# Serialize sorted clauses as canonical text. +# --------------------------------------------------------------------- + + +def _serialize(clauses: list[tuple]) -> str: + """Each clause is a sorted tuple of (atom, negated) literals.""" + + def lit_str(lit): + atom, neg = lit + return f"NOT {atom}" if neg else atom + + parts = [] + for clause in clauses: + if len(clause) == 1: + parts.append(lit_str(clause[0])) + else: + parts.append("(" + " OR ".join(lit_str(l) for l in clause) + ")") + return " AND ".join(parts) register(LogicKernelV1()) diff --git a/bench/batteries/base.py b/bench/batteries/base.py index cd5a857..cd6f2ea 100644 --- a/bench/batteries/base.py +++ b/bench/batteries/base.py @@ -112,6 +112,10 @@ PHASE_1_CARRIERS = frozenset({ "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", }) diff --git a/bench/fixtures/5s/semantics-arithmetic-v1.jsonl b/bench/fixtures/5s/semantics-arithmetic-v1.jsonl new file mode 100644 index 0000000..cb798bd --- /dev/null +++ b/bench/fixtures/5s/semantics-arithmetic-v1.jsonl @@ -0,0 +1,16 @@ +{"_meta":{"battery":"5s","sub_battery":"semantics","version":"v1","task_count":15,"notes":"arithmetic@v1 equivalence-class tests. SQD §14.1: rationally equivalent expressions canonicalize to identical bytes; distinct values do not."}} +{"id":"5s-sem-arith-001","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input_a":"1+2","input_b":"3","expected_equivalent":true} +{"id":"5s-sem-arith-002","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input_a":"0.1","input_b":"1/10","expected_equivalent":true} +{"id":"5s-sem-arith-003","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input_a":"0.1+0.2","input_b":"0.3","expected_equivalent":true} +{"id":"5s-sem-arith-004","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input_a":"(1+2)*3","input_b":"9","expected_equivalent":true} +{"id":"5s-sem-arith-005","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input_a":"6/4","input_b":"3/2","expected_equivalent":true} +{"id":"5s-sem-arith-006","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input_a":"-2","input_b":"-2/1","expected_equivalent":true} +{"id":"5s-sem-arith-007","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input_a":"2**3","input_b":"8","expected_equivalent":true} +{"id":"5s-sem-arith-008","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input_a":"0.5","input_b":"1/2","expected_equivalent":true} +{"id":"5s-sem-arith-009","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input_a":"100*100","input_b":"10000","expected_equivalent":true} +{"id":"5s-sem-arith-010","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input_a":"1+2","input_b":"4","expected_equivalent":false} +{"id":"5s-sem-arith-011","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input_a":"1/2","input_b":"1/3","expected_equivalent":false} +{"id":"5s-sem-arith-012","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input_a":"0.1","input_b":"0.2","expected_equivalent":false} +{"id":"5s-sem-arith-013","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input_a":"-3","input_b":"3","expected_equivalent":false} +{"id":"5s-sem-arith-014","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input_a":"3+5*2","input_b":"13","expected_equivalent":true} +{"id":"5s-sem-arith-015","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input_a":"3+5*2","input_b":"16","expected_equivalent":false} diff --git a/bench/fixtures/5s/semantics-logic-v1.jsonl b/bench/fixtures/5s/semantics-logic-v1.jsonl new file mode 100644 index 0000000..1d82922 --- /dev/null +++ b/bench/fixtures/5s/semantics-logic-v1.jsonl @@ -0,0 +1,19 @@ +{"_meta":{"battery":"5s","sub_battery":"semantics","version":"v1","task_count":18,"notes":"logic-kernel@v1 equivalence-class tests. Logically equivalent expressions canonicalize to identical CNF bytes; logically distinct expressions do not."}} +{"id":"5s-sem-logic-001","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input_a":"A AND B","input_b":"B AND A","expected_equivalent":true} +{"id":"5s-sem-logic-002","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input_a":"A OR B","input_b":"B OR A","expected_equivalent":true} +{"id":"5s-sem-logic-003","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input_a":"(A AND B) AND C","input_b":"A AND (B AND C)","expected_equivalent":true} +{"id":"5s-sem-logic-004","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input_a":"A IMPL B","input_b":"NOT A OR B","expected_equivalent":true} +{"id":"5s-sem-logic-005","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input_a":"A IMPL B","input_b":"(NOT B) IMPL (NOT A)","expected_equivalent":true} +{"id":"5s-sem-logic-006","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input_a":"NOT (A AND B)","input_b":"(NOT A) OR (NOT B)","expected_equivalent":true} +{"id":"5s-sem-logic-007","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input_a":"NOT (A OR B)","input_b":"(NOT A) AND (NOT B)","expected_equivalent":true} +{"id":"5s-sem-logic-008","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input_a":"NOT NOT A","input_b":"A","expected_equivalent":true} +{"id":"5s-sem-logic-009","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input_a":"A OR (B AND C)","input_b":"(A OR B) AND (A OR C)","expected_equivalent":true} +{"id":"5s-sem-logic-010","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input_a":"A IFF B","input_b":"(A IMPL B) AND (B IMPL A)","expected_equivalent":true} +{"id":"5s-sem-logic-011","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input_a":"A XOR B","input_b":"(A OR B) AND (NOT A OR NOT B)","expected_equivalent":true} +{"id":"5s-sem-logic-012","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input_a":"A OR NOT A","input_b":"TRUE","expected_equivalent":true} +{"id":"5s-sem-logic-013","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input_a":"A AND A","input_b":"A","expected_equivalent":true} +{"id":"5s-sem-logic-014","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input_a":"A AND B","input_b":"A OR B","expected_equivalent":false} +{"id":"5s-sem-logic-015","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input_a":"A IMPL B","input_b":"B IMPL A","expected_equivalent":false} +{"id":"5s-sem-logic-016","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input_a":"A AND B","input_b":"A AND C","expected_equivalent":false} +{"id":"5s-sem-logic-017","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input_a":"NOT A","input_b":"A","expected_equivalent":false} +{"id":"5s-sem-logic-018","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input_a":"(A IMPL B) AND (B IMPL C)","input_b":"A IMPL C","expected_equivalent":false} diff --git a/bench/fixtures/5s/syntax-arithmetic-v1.jsonl b/bench/fixtures/5s/syntax-arithmetic-v1.jsonl new file mode 100644 index 0000000..740069f --- /dev/null +++ b/bench/fixtures/5s/syntax-arithmetic-v1.jsonl @@ -0,0 +1,13 @@ +{"_meta":{"battery":"5s","sub_battery":"syntax","version":"v1","task_count":12,"notes":"arithmetic@v1 parse-pass tests. Each input is an arithmetic expression that must canonicalize without raising."}} +{"id":"5s-syn-arith-001","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input":"3","expected":"pass"} +{"id":"5s-syn-arith-002","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input":"1+2","expected":"pass"} +{"id":"5s-syn-arith-003","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input":"-7","expected":"pass"} +{"id":"5s-syn-arith-004","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input":"0.1","expected":"pass"} +{"id":"5s-syn-arith-005","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input":"0.1+0.2","expected":"pass"} +{"id":"5s-syn-arith-006","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input":"(1+2)*3","expected":"pass"} +{"id":"5s-syn-arith-007","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input":"6/4","expected":"pass"} +{"id":"5s-syn-arith-008","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input":"2**3","expected":"pass"} +{"id":"5s-syn-arith-009","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input":"-(1+2)","expected":"pass"} +{"id":"5s-syn-arith-010","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input":"3.14","expected":"pass"} +{"id":"5s-syn-arith-011","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input":"((1+2)*(3-4))/5","expected":"pass"} +{"id":"5s-syn-arith-012","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input":"7*8 - 2","expected":"pass"} diff --git a/bench/fixtures/5s/syntax-logic-v1.jsonl b/bench/fixtures/5s/syntax-logic-v1.jsonl new file mode 100644 index 0000000..6726d41 --- /dev/null +++ b/bench/fixtures/5s/syntax-logic-v1.jsonl @@ -0,0 +1,13 @@ +{"_meta":{"battery":"5s","sub_battery":"syntax","version":"v1","task_count":12,"notes":"logic-kernel@v1 parse-pass tests. Each input is a propositional expression that must canonicalize without raising."}} +{"id":"5s-syn-logic-001","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input":"A","expected":"pass"} +{"id":"5s-syn-logic-002","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input":"A AND B","expected":"pass"} +{"id":"5s-syn-logic-003","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input":"A OR B","expected":"pass"} +{"id":"5s-syn-logic-004","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input":"NOT A","expected":"pass"} +{"id":"5s-syn-logic-005","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input":"A IMPL B","expected":"pass"} +{"id":"5s-syn-logic-006","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input":"A IFF B","expected":"pass"} +{"id":"5s-syn-logic-007","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input":"A XOR B","expected":"pass"} +{"id":"5s-syn-logic-008","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input":"(A AND B) OR (C AND D)","expected":"pass"} +{"id":"5s-syn-logic-009","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input":"NOT (A OR (B AND C))","expected":"pass"} +{"id":"5s-syn-logic-010","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input":"TRUE","expected":"pass"} +{"id":"5s-syn-logic-011","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input":"A IMPL (B IMPL C)","expected":"pass"} +{"id":"5s-syn-logic-012","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input":"A AND B AND C AND D","expected":"pass"} diff --git a/tests/test_pi_star.py b/tests/test_pi_star.py index 073ec92..3705643 100644 --- a/tests/test_pi_star.py +++ b/tests/test_pi_star.py @@ -127,9 +127,10 @@ def test_claim_lattice_empty_input_returns_empty_array(): @pytest.mark.parametrize( "key", [ - # code-py-ast@v1 graduated from stub to real implementation — - # see test_code_py_ast_* below. - "logic-kernel@v1", + # code-py-ast@v1 graduated to real implementation — see + # test_code_py_ast_*. + # logic-kernel@v1 graduated to real CNF canonicalizer — see + # test_logic_kernel_*. "time-series-quantized@v1", "tabular-pinned@v1", ], @@ -234,6 +235,229 @@ def test_code_py_ast_equivalence_class_id_format(): assert eid == equivalence_class_id(pi_star, b"x = 1") +# --- arithmetic@v1 (graduated from stub) ----------------------------- + + +def test_arithmetic_canonicalizes_integer(): + pi_star = get("arithmetic@v1") + assert pi_star.canonicalize(b"3") == b"3/1" + assert pi_star.canonicalize(b"-7") == b"-7/1" + + +def test_arithmetic_canonicalizes_decimal_exactly(): + """SQD §14.1: 0.1 must canonicalize to 1/10 exactly.""" + pi_star = get("arithmetic@v1") + assert pi_star.canonicalize(b"0.1") == b"1/10" + assert pi_star.canonicalize(b"0.5") == b"1/2" + assert pi_star.canonicalize(b"0.25") == b"1/4" + + +def test_arithmetic_solves_classic_floating_point_question(): + """The SQD canonical example: 0.1 + 0.2 == 0.3 exactly.""" + pi_star = get("arithmetic@v1") + a = pi_star.canonicalize(b"0.1+0.2") + b = pi_star.canonicalize(b"0.3") + assert a == b == b"3/10" + + +def test_arithmetic_collapses_equivalent_expressions(): + pi_star = get("arithmetic@v1") + assert pi_star.canonicalize(b"1+2") == pi_star.canonicalize(b"3") + assert pi_star.canonicalize(b"(1+2)*3") == pi_star.canonicalize(b"9") + assert pi_star.canonicalize(b"6/4") == pi_star.canonicalize(b"3/2") + + +def test_arithmetic_distinguishes_distinct_values(): + pi_star = get("arithmetic@v1") + assert pi_star.canonicalize(b"1+2") != pi_star.canonicalize(b"4") + assert pi_star.canonicalize(b"1/2") != pi_star.canonicalize(b"1/3") + + +def test_arithmetic_supports_integer_exponent(): + pi_star = get("arithmetic@v1") + assert pi_star.canonicalize(b"2**3") == b"8/1" + assert pi_star.canonicalize(b"3**2") == b"9/1" + + +def test_arithmetic_rejects_division_by_zero(): + from arborist.pi_star.protocol import PiStarError + + pi_star = get("arithmetic@v1") + with pytest.raises(PiStarError, match="division by zero"): + pi_star.canonicalize(b"1/0") + + +def test_arithmetic_rejects_variables(): + from arborist.pi_star.protocol import PiStarError + + pi_star = get("arithmetic@v1") + with pytest.raises(PiStarError, match="identifier"): + pi_star.canonicalize(b"x + 1") + + +def test_arithmetic_rejects_non_integer_exponent(): + from arborist.pi_star.protocol import PiStarError + + pi_star = get("arithmetic@v1") + with pytest.raises(PiStarError, match="non-integer exponent"): + pi_star.canonicalize(b"2 ** 0.5") + + +def test_arithmetic_rejects_function_calls(): + from arborist.pi_star.protocol import PiStarError + + pi_star = get("arithmetic@v1") + with pytest.raises(PiStarError, match="function call"): + pi_star.canonicalize(b"abs(-5)") + + +def test_arithmetic_rejects_invalid_syntax(): + from arborist.pi_star.protocol import PiStarError + + pi_star = get("arithmetic@v1") + with pytest.raises(PiStarError): + pi_star.canonicalize(b"1 +") + + +def test_arithmetic_rejects_empty_input(): + from arborist.pi_star.protocol import PiStarError + + pi_star = get("arithmetic@v1") + with pytest.raises(PiStarError, match="empty"): + pi_star.canonicalize(b"") + + +def test_arithmetic_canonical_form_is_idempotent(): + pi_star = get("arithmetic@v1") + once = pi_star.canonicalize(b"6/4") + twice = pi_star.canonicalize(once) + assert once == twice == b"3/2" + + +def test_arithmetic_handles_negative_results(): + pi_star = get("arithmetic@v1") + assert pi_star.canonicalize(b"-(1+2)") == b"-3/1" + assert pi_star.canonicalize(b"3 - 5") == b"-2/1" + + +# --- logic-kernel@v1 (graduated from stub) --------------------------- + + +def test_logic_kernel_canonicalizes_simple_and(): + pi_star = get("logic-kernel@v1") + assert pi_star.canonicalize(b"A AND B") == b"A AND B" + + +def test_logic_kernel_commutativity(): + pi_star = get("logic-kernel@v1") + assert pi_star.canonicalize(b"A AND B") == pi_star.canonicalize(b"B AND A") + assert pi_star.canonicalize(b"A OR B") == pi_star.canonicalize(b"B OR A") + + +def test_logic_kernel_associativity(): + pi_star = get("logic-kernel@v1") + a = pi_star.canonicalize(b"(A AND B) AND C") + b = pi_star.canonicalize(b"A AND (B AND C)") + assert a == b + + +def test_logic_kernel_impl_rewrite(): + pi_star = get("logic-kernel@v1") + assert pi_star.canonicalize(b"A IMPL B") == pi_star.canonicalize(b"NOT A OR B") + + +def test_logic_kernel_iff_rewrite(): + pi_star = get("logic-kernel@v1") + a = pi_star.canonicalize(b"A IFF B") + b = pi_star.canonicalize(b"(NOT A OR B) AND (NOT B OR A)") + assert a == b + + +def test_logic_kernel_xor_rewrite(): + pi_star = get("logic-kernel@v1") + a = pi_star.canonicalize(b"A XOR B") + b = pi_star.canonicalize(b"(A OR B) AND (NOT A OR NOT B)") + assert a == b + + +def test_logic_kernel_de_morgans(): + pi_star = get("logic-kernel@v1") + a = pi_star.canonicalize(b"NOT (A AND B)") + b = pi_star.canonicalize(b"(NOT A) OR (NOT B)") + assert a == b + + +def test_logic_kernel_double_negation(): + pi_star = get("logic-kernel@v1") + assert pi_star.canonicalize(b"NOT NOT A") == pi_star.canonicalize(b"A") + + +def test_logic_kernel_distribution(): + pi_star = get("logic-kernel@v1") + a = pi_star.canonicalize(b"A OR (B AND C)") + b = pi_star.canonicalize(b"(A OR B) AND (A OR C)") + assert a == b + + +def test_logic_kernel_tautology_collapses_to_true(): + pi_star = get("logic-kernel@v1") + assert pi_star.canonicalize(b"A OR NOT A") == b"TRUE" + assert pi_star.canonicalize(b"TRUE") == b"TRUE" + + +def test_logic_kernel_idempotence(): + pi_star = get("logic-kernel@v1") + assert pi_star.canonicalize(b"A AND A") == pi_star.canonicalize(b"A") + assert pi_star.canonicalize(b"A OR A") == pi_star.canonicalize(b"A") + + +def test_logic_kernel_distinguishes_logically_distinct(): + pi_star = get("logic-kernel@v1") + assert pi_star.canonicalize(b"A AND B") != pi_star.canonicalize(b"A OR B") + assert pi_star.canonicalize(b"A IMPL B") != pi_star.canonicalize(b"B IMPL A") + + +def test_logic_kernel_caps_atom_count(): + from arborist.pi_star.protocol import PiStarError + + pi_star = get("logic-kernel@v1") + expr = b"A AND B AND C AND D AND E AND F AND G AND H AND I" + with pytest.raises(PiStarError, match="caps atoms at"): + pi_star.canonicalize(expr) + + +def test_logic_kernel_rejects_empty(): + from arborist.pi_star.protocol import PiStarError + + pi_star = get("logic-kernel@v1") + with pytest.raises(PiStarError, match="empty"): + pi_star.canonicalize(b"") + + +def test_logic_kernel_rejects_invalid_syntax(): + from arborist.pi_star.protocol import PiStarError + + pi_star = get("logic-kernel@v1") + with pytest.raises(PiStarError): + pi_star.canonicalize(b"A AND") + + +def test_logic_kernel_canonical_form_is_idempotent(): + pi_star = get("logic-kernel@v1") + src = b"(A OR B) AND (NOT A OR C)" + once = pi_star.canonicalize(src) + twice = pi_star.canonicalize(once) + assert once == twice + + +def test_logic_kernel_contrapositive_equivalence(): + """A IMPL B ≡ NOT B IMPL NOT A""" + pi_star = get("logic-kernel@v1") + a = pi_star.canonicalize(b"A IMPL B") + b = pi_star.canonicalize(b"(NOT B) IMPL (NOT A)") + assert a == b + + # --- composition --------------------------------------------------