Tutorials

Check an evaluation and request an accuracy

Use dense.enclose or sparse.enclose when you need an evaluation result that another calculation can check independently. These functions retain the original polynomial, argument enclosures, and a trace of rational bounds. evaluation.check verifies that trace without rerunning floating-point evaluation.

array_extension_certified.mojo Download
"""Check evaluation bounds separately from requested accuracy."""
from apn_mojo import Rational, Ball, BallContext, contains
from polynomials import NumericOptions, NumericOutcome
from poly import dense, evaluation
from std.testing import assert_equal, assert_true


def main() raises:
    var fixed = dense.enclose([1, 2, 3], Rational(1, 3), context=BallContext(precision=80))
    assert_true(evaluation.check(fixed))
    assert_true(contains(fixed.value(), Rational(2)))
    var options = NumericOptions(initial_precision=16, max_precision=128, absolute_bits=64)
    var refined = dense.adaptive_evaluate([1, 2, 3], Rational(1, 3), options=options)
    assert_true(evaluation.check(refined))
    assert_true(refined.accurate())
    assert_true(contains(refined.value(), Rational(2)))
    var uncertain = dense.adaptive_evaluate([0, 1], Ball(Rational(0), Rational(1), precision=80), options=options)
    assert_true(evaluation.check(uncertain))
    assert_true(not uncertain.accurate())
    assert_equal(uncertain.outcome().value(), NumericOutcome.PRECISION_CEILING)
    print("Evaluation enclosure checked; requested accuracy reached")
    print("Uncertain input: valid enclosure, precision ceiling reached")

Run from the repository root pixi run mojo run -I build docs/examples/array_extension_certified.mojo

Output

Evaluation enclosure checked; requested accuracy reached
Uncertain input: valid enclosure, precision ceiling reached

The polynomial \(1+2x+3x^2\) equals 2 at \(x=1/3\). The first call encloses that value at a fixed precision. The second starts at 16 bits and increases the working precision until it establishes the requested width or reaches 128 bits. absolute_bits=64 requests a width no greater than \(2^{-64}\). A nonzero relative_bits adds a scale-dependent relative allowance.

Read the result's claim

value() returns an independent Ball or ComplexBall. precision() reports the last working midpoint precision; evidence() borrows its immutable trace. For adaptive calls, options() retains the original request and outcome() is SUCCESS or PRECISION_CEILING. Fixed-precision calls have no accuracy outcome.

A successful evaluation.check(result) proves the enclosure and validates any reported accuracy outcome. Check result.accurate() as well when your application needs the requested width. The final example evaluates \(x\) on \([-1,1]\). Its uncertainty persists at every precision, so it returns a valid enclosure with PRECISION_CEILING. The checker accepts that truthful outcome.

Choose inputs and precision

Both workflows accept integer, rational, Gaussian-rational, AA, and QQbar coefficient sequences, or prepared numerical arrays. Modular coefficients are rejected. Fixed evaluation requires a BallContext with an explicit precision. Adaptive evaluation requires NumericOptions; it preserves the original coefficients through all refinement attempts. Scalar arguments are converted outward to a ball. Adaptive calls perform that conversion at the configured maximum precision and retain the resulting argument enclosure throughout refinement.

Sparse inputs use a coordinate tuple in the original axis order; univariate inputs also accept a scalar argument. Complex coefficients or coordinates select a ComplexBall result. Ball coefficients describe an entire polynomial family, and the returned enclosure covers every member of that family at every allowed argument. Raising working precision cannot remove uncertainty supplied with the inputs.

For algebraic coefficients, each attempt refines their exact root bounds at the current working precision. The result retains those witnesses and the numerical coefficient enclosures. Its checker verifies the original and refined root evidence, containment, and the arithmetic trace without repeating root refinement or floating-point evaluation. Algebraic coordinates also retain conversion witnesses. Keep the complete result: evidence() exposes the core arithmetic trace, not the additional algebraic conversion evidence.

Every call accepts max_steps= or a shared Budget. Exhaustion raises PolyError with kind LIMIT; it is distinct from completing an adaptive request at its precision ceiling. See the evaluation reference for signatures and the numerical design for the underlying proof schedule.

Check one witness step at a time

Use enclose_stream and enclose_checker when retaining a complete trace would cost too much memory. They accept the same exact or numerical inputs and explicit BallContext as fixed enclose.

array_parity_stream.mojo Download
"""Check an enclosure without keeping the full witness trace."""
from apn_mojo import BallContext, Rational, contains
from polynomials import Budget
from poly import dense
from std.testing import assert_true


def main() raises:
    var budget = Budget()
    var context = BallContext(precision=80)
    var stream = dense.enclose_stream([1, 2, 3], Rational(1, 3), budget, context=context)
    var checker = dense.enclose_checker([1, 2, 3], Rational(1, 3), budget, context=context)
    while True:
        var step = stream.next(budget)
        if not step:
            break
        assert_true(checker.accept(step.take(), budget))
    var receipt = stream.finish(budget)
    assert_true(checker.finish(receipt, budget))
    assert_true(contains(receipt.value(budget), Rational(2)))
    print("Streamed enclosure verified")

Run from the repository root pixi run mojo run -I build docs/examples/array_parity_stream.mojo

Output

Streamed enclosure verified

Forward every event in order. accept checks the next event; finish checks completeness and the final receipt. A receipt alone is not a proof. Calling the producer's finish before consuming its steps raises DOMAIN. A rejected event permanently invalidates that checker. If a call raises LIMIT, give it more budget and retry the same event; its position has not advanced.

Refine algebraic inputs automatically

Use the same calls with AA or QQbar coefficients or algebraic evaluation points. Each real and imaginary component is refined at the requested BallContext precision before it enters the arithmetic trace. You don't need to call algebraic.refine first.

array_algebraic_stream.mojo Download
"""Refine and check algebraic inputs without retaining the event history."""
from apn_mojo import BallContext, Rational, contains
from polynomials import Budget
from poly import dense, coefficients
from std.testing import assert_true


def main() raises:
    var budget = Budget()
    var root = dense.root_between([-2, 0, 1], 1, 2)
    var p = dense.asarray(coefficients((0, root.copy())))
    var context = BallContext(precision=80)
    var stream = dense.enclose_stream(p, root, budget, context=context)
    var checker = dense.enclose_checker(p, root, budget, context=context)
    while True:
        var step = stream.next(budget)
        if not step:
            break
        assert_true(checker.accept(step.take(), budget))
    var receipt = stream.finish(budget)
    assert_true(checker.finish(receipt, budget))
    assert_true(contains(receipt.value(budget), Rational(2)))
    print("Algebraic stream verified")

Run from the repository root pixi run mojo run -I build docs/examples/array_algebraic_stream.mojo

Output

Algebraic stream verified

Here the coefficient and evaluation point both represent \(\sqrt{2}\). Their product is \(2\), which lies inside the returned enclosure. The checker verifies the root identities and narrower intervals before checking the multiplication. It does not repeat the producer's root search. The original coefficients and point are unchanged.

For algebraic inputs, next returns an evaluation.EnclosureStep. The stream sends coefficient refinements in canonical coefficient order, algebraic point refinements in axis order, then arithmetic bounds. Your forwarding loop stays the same. step_count() and the receipt's steps include all these events. Streams without algebraic inputs emit NumericBox steps.

Higher precision narrows the algebraic input intervals and reduces arithmetic rounding. It does not promise a particular final width: cancellation, repeated use of the same uncertain value, or numerical input uncertainty can leave a wider result. Use retained adaptive_evaluate when you need an explicit absolute or relative accuracy target. Streaming evaluation performs one pass at the supplied precision.

The producer refines one input when you request its event. Neither producer nor checker keeps a history of refinement witnesses or arithmetic events. They do retain the input polynomial, prepared instruction graph, and live intermediate values, so memory depends on the input and calculation. Preparation, refinement, checking, and completion all use your shared work budget.