Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 6 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -47,6 +47,12 @@ factorial — hand-written recursive-descent parser, graded by an independently
implemented `ast`-based oracle (`mathgate/proofbench_lite.py`), 240 seeded
cases, 0 failures, 0 certificate drift, reproducible by anyone.

Those 240 cases are a public development suite: 192 exact answers and 48 expected
refusals. The separate oracle cross-checks the tested expressions; this is not an
independent third-party evaluation or an official leaderboard result. Targeted
regression tests also cover power precedence, nesting, and computation bounds.
See [the supported limits](docs/LIMITATIONS.md) before using untrusted expressions.

The **hosted SuperMath Lab** (symbolic calculus, linear algebra, proof mode,
and the full 1,116-case ProofBench X corpus) is proprietary and lives at
[jvi3.com/packages#tab-supermath](https://jvi3.com/packages#tab-supermath),
Expand Down
19 changes: 17 additions & 2 deletions docs/LIMITATIONS.md
Original file line number Diff line number Diff line change
Expand Up @@ -13,12 +13,27 @@
this lite engine only does exact combination (matching radicands, e.g.
`sqrt(2)*sqrt(2) = 2` or `sqrt(8) = 2*sqrt(2)`), not general symbolic simplification.
- **Factorial is capped at 5000** as a safety bound against unbounded compute in CI/demo
contexts, not a mathematical limitation.
contexts, not a mathematical limitation. The result-size bound below also applies;
`5000!` is refused because its result is too large for this lite engine.
- **Work and output are bounded.** Expressions are limited to 4096 characters;
integer numerators and denominators to 14000 bits; exponent magnitude to 10000.
Non-square radicands above `10^12` are refused before trial factorization.
Perfect-square roots use an exact integer square-root check. Inputs beyond these
limits return `REFUSED`. Excessive recursive nesting and runtime integer-rendering
limits also return `REFUSED`; no process-wide Python safety limit is disabled.
- **Power uses conventional precedence and right association.** `-2^2` is `-4`,
`(-2)^2` is `4`, `2^3^2` is `512`, and `2^-2` is `1/4`.
- **ProofBench-X Lite is 240 cases, not 1,116.** It's a public, honest, independently
oracle-graded subset for *this* engine only — see [BUGS_FOUND.md](BUGS_FOUND.md) for
why an independent oracle (not the engine checking itself) matters, and
[ProofBench X](https://jvi3.com/packages#tab-supermath) for the hosted engine's full
corpus and live scoreboard.
- **The 240 cases are a public development suite, not an independent evaluation.**
The arithmetic oracle is a separate implementation in the same repository.
Passing these cases does not establish correctness for every accepted expression,
performance against other systems, or an official leaderboard placement. Regression
tests separately cover power precedence, excessive nesting, and resource bounds.
- **Refuses rather than guesses.** Malformed input (unbalanced parens, division by
zero, factorial of a negative/non-integer, fractional exponents, sqrt of a negative
number) always comes back `REFUSED` with a reason — never a best-effort answer.
number) comes back `REFUSED` with a reason. This is a scoped parser and arithmetic
implementation, not a general security or correctness guarantee.
71 changes: 51 additions & 20 deletions mathgate/engine.py
Original file line number Diff line number Diff line change
Expand Up @@ -7,10 +7,10 @@
implementation, not the same code checking itself):

expr := term (('+' | '-') term)*
term := factor (('*' | '/') factor)*
factor := unary ('^' unary)?
unary := '-' unary | postfix
postfix := atom '!'?
term := unary (('*' | '/') unary)*
unary := '-' unary | power
power := postfix ('^' unary)?
postfix := atom '!'*
atom := NUMBER | 'sqrt' '(' expr ')' | '(' expr ')'

Every value is either an exact ``Fraction`` or a ``Sqrt`` (coefficient *
Expand Down Expand Up @@ -50,6 +50,20 @@ class Sqrt:

Value = Union[Fraction, Sqrt]

# Limits are part of this lite engine's supported input domain. In particular,
# do not disable Python's process-wide integer-to-string safety limit.
MAX_QUERY_CHARS = 4096
MAX_VALUE_BITS = 14000
MAX_EXPONENT = 10000
MAX_SURD_RADICAND = 10**12


def _bounded(v: Value) -> Value:
coeff = v.coeff if isinstance(v, Sqrt) else v
if max(coeff.numerator.bit_length(), coeff.denominator.bit_length()) > MAX_VALUE_BITS:
raise Refused("exact value exceeds this lite engine's 14000-bit size bound")
return v


# ---------------------------------------------------------------------------
# Tokenizer
Expand Down Expand Up @@ -134,15 +148,15 @@ def _expr(self) -> Value:
return val

def _term(self) -> Value:
val = self._factor()
val = self._unary()
while self._peek() and self._peek()[0] in ("*", "/"):
op = self._advance()[0]
rhs = self._factor()
rhs = self._unary()
val = _mul(val, rhs) if op == "*" else _div(val, rhs)
return val

def _factor(self) -> Value:
val = self._unary()
def _power(self) -> Value:
val = self._postfix()
if self._peek() and self._peek()[0] == "^":
self._advance()
exp = self._unary()
Expand All @@ -153,7 +167,7 @@ def _unary(self) -> Value:
if self._peek() and self._peek()[0] == "-":
self._advance()
return _neg(self._unary())
return self._postfix()
return self._power()

def _postfix(self) -> Value:
val = self._atom()
Expand Down Expand Up @@ -186,7 +200,7 @@ def _atom(self) -> Value:
def _num(text: str) -> Fraction:
if text.count(".") > 1:
raise Refused(f"malformed number '{text}'")
return Fraction(text)
return _bounded(Fraction(text))


# ---------------------------------------------------------------------------
Expand All @@ -198,6 +212,11 @@ def _simplify_sqrt(coeff: Fraction, radicand: int) -> Value:
raise Refused("sqrt of a negative number is not real-exact in this engine")
if radicand == 0:
return Fraction(0)
root = math.isqrt(radicand)
if root * root == radicand:
return _bounded(coeff * root)
if radicand > MAX_SURD_RADICAND:
raise Refused("non-square radicand exceeds this lite engine's factorization bound (10^12)")
extracted = 1
r = radicand
d = 2
Expand All @@ -206,7 +225,7 @@ def _simplify_sqrt(coeff: Fraction, radicand: int) -> Value:
r //= d * d
extracted *= d
d += 1
coeff = coeff * extracted
coeff = _bounded(coeff * extracted)
if r == 1:
return coeff
return Sqrt(coeff, r)
Expand All @@ -228,7 +247,7 @@ def _neg(v: Value) -> Value:

def _add(a: Value, b: Value) -> Value:
if isinstance(a, Fraction) and isinstance(b, Fraction):
return a + b
return _bounded(a + b)
a_rad = a.radicand if isinstance(a, Sqrt) else 1
b_rad = b.radicand if isinstance(b, Sqrt) else 1
if a_rad != b_rad:
Expand All @@ -243,7 +262,7 @@ def _add(a: Value, b: Value) -> Value:

def _mul(a: Value, b: Value) -> Value:
if isinstance(a, Fraction) and isinstance(b, Fraction):
return a * b
return _bounded(a * b)
a_rad = a.radicand if isinstance(a, Sqrt) else 1
a_coeff = a.coeff if isinstance(a, Sqrt) else a
b_rad = b.radicand if isinstance(b, Sqrt) else 1
Expand All @@ -257,8 +276,8 @@ def _div(a: Value, b: Value) -> Value:
raise Refused("division by zero")
raise Refused("division by a symbolic surd is out of scope for this lite engine")
if isinstance(a, Sqrt):
return Sqrt(a.coeff / b, a.radicand)
return a / b
return _bounded(Sqrt(a.coeff / b, a.radicand))
return _bounded(a / b)


def _pow(base: Value, exp: Value) -> Value:
Expand All @@ -267,6 +286,8 @@ def _pow(base: Value, exp: Value) -> Value:
if exp.denominator != 1:
raise Refused("non-integer exponent is out of scope for this lite engine (would not be exact)")
e = int(exp)
if abs(e) > MAX_EXPONENT:
raise Refused("exponent exceeds this lite engine's magnitude bound (10000)")
if isinstance(base, Sqrt):
if e < 0:
raise Refused("negative exponent on a symbolic surd is out of scope for this lite engine")
Expand All @@ -278,11 +299,16 @@ def _pow(base: Value, exp: Value) -> Value:
if base == 0:
raise Refused("0^0 is undefined")
return Fraction(1)
# Refuse oversized powers before allocating them. This lower bound is
# conservative; the exact result is checked again after computation.
base_bits = max(base.numerator.bit_length(), base.denominator.bit_length())
if (base_bits - 1) * abs(e) + 1 > MAX_VALUE_BITS:
raise Refused("exact power exceeds this lite engine's 14000-bit size bound")
if e > 0:
return base ** e
return _bounded(base ** e)
if base == 0:
raise Refused("division by zero (negative exponent of 0)")
return Fraction(1) / (base ** (-e))
return _bounded(Fraction(1) / (base ** (-e)))


def _factorial(v: Value) -> Value:
Expand All @@ -293,7 +319,7 @@ def _factorial(v: Value) -> Value:
raise Refused("factorial of a negative number is undefined")
if n > 5000:
raise Refused("factorial argument too large for this lite engine's safety bound (5000)")
return Fraction(math.factorial(n))
return _bounded(Fraction(math.factorial(n)))


# ---------------------------------------------------------------------------
Expand Down Expand Up @@ -343,20 +369,25 @@ def _certificate(query: str, status: str, result: str) -> str:


def calculate(query: str) -> Result:
"""Evaluate ``query`` exactly. Never raises — malformed/out-of-scope
"""Evaluate a string ``query`` exactly. Malformed/out-of-scope
input comes back as a ``Result`` with ``status == "REFUSED"``, sealed
with the same certificate scheme as a successful result, so a refusal
is just as replayable and auditable as an answer."""
normalized = query.strip()
try:
if len(normalized) > MAX_QUERY_CHARS:
raise Refused("expression exceeds this lite engine's length bound (4096 characters)")
tokens = _tokenize(normalized)
value = _Parser(tokens).parse()
rendered = _render(value)
except Refused as exc:
cert = _certificate(normalized, "REFUSED", "")
return Result(normalized, "REFUSED", "", "", str(exc), cert)
except (ZeroDivisionError, ValueError, OverflowError) as exc:
cert = _certificate(normalized, "REFUSED", "")
return Result(normalized, "REFUSED", "", "", f"invalid expression: {exc}", cert)
rendered = _render(value)
except RecursionError:
cert = _certificate(normalized, "REFUSED", "")
return Result(normalized, "REFUSED", "", "", "expression nesting exceeds this runtime's safe parsing depth", cert)
cert = _certificate(normalized, "OK", rendered)
return Result(normalized, "OK", rendered, _exactness(value), "", cert)
35 changes: 34 additions & 1 deletion tests/test_mathgate.py
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
import unittest

from mathgate.engine import calculate
from mathgate.proofbench_lite import run
from mathgate.proofbench_lite import oracle_calculate, run


class TestEngine(unittest.TestCase):
Expand Down Expand Up @@ -35,6 +35,39 @@ def test_sign_drop_regression(self):
self.assertEqual(calculate("(-3)*(-4)").result, "12")
self.assertEqual(calculate("-(3*4)").result, "-12")

def test_power_precedence_and_associativity_match_independent_oracle(self):
for query in ("-2^2", "(-2)^2", "2^3^2", "2^-2", "-2^-2", "2*-3^2"):
with self.subTest(query=query):
result = calculate(query)
expected = oracle_calculate(query.replace("^", "**"))
self.assertEqual(result.status, "OK")
self.assertEqual(result.result, str(expected))

def test_large_factorial_returns_replayable_refusal(self):
# 5000! previously escaped calculate() as ValueError on Python >= 3.11
# because its rendered value exceeds the default 4300-digit limit.
first = calculate("5000!")
second = calculate("5000!")
self.assertEqual(first.status, "REFUSED")
self.assertIn("size bound", first.reason)
self.assertEqual(first.certificate_hash, second.certificate_hash)

def test_deep_expression_returns_refusal_instead_of_recursion_error(self):
for query in ("(" * 600 + "1" + ")" * 600, "-" * 2000 + "1"):
with self.subTest(length=len(query)):
result = calculate(query)
self.assertEqual(result.status, "REFUSED")
self.assertIn("parsing depth", result.reason)
self.assertEqual(result.certificate_hash, calculate(query).certificate_hash)

def test_work_limits_refuse_oversized_computation(self):
for query in ("2^1000000000", "99999^9999", "sqrt(1000000000001)", "1" * 4097):
with self.subTest(query=query[:50]):
self.assertEqual(calculate(query).status, "REFUSED")
# Useful large exact results and fast perfect-square checks still work.
self.assertEqual(calculate("2^10000").result, str(2**10000))
self.assertEqual(calculate("sqrt(10^20)").result, "10000000000")

def test_refuses_malformed_input(self):
self.assertEqual(calculate("1 + + * 2 )(").status, "REFUSED")
self.assertEqual(calculate("").status, "REFUSED")
Expand Down
Loading