Certified array evaluation¶

dense.enclose and sparse.enclose produce a value and an independently checkable bound trace. Algebraic coefficients and points additionally retain checked root-refinement and containment witnesses in the complete result. The borrowed evidence() is the arithmetic trace only. Their adaptive_evaluate counterparts additionally try to meet explicit accuracy options. The tutorial explains why valid evidence and successful accuracy are separate questions.

Enclosure¶

@fieldwise_init
struct Enclosure[C: AnyType, D: NumericDomain, numerical: Bool, sparse: Bool](_Archive, _QuotientInput, Copyable, Movable)

An enclosing value with its original inputs and independently checkable trace.

Parameters.

• C: The inferred source coefficient ring or numerical domain.
• D: The inferred real or complex ball domain.
• numerical: Whether the source coefficients are numerical.
• sparse: Whether the source is sparse.

Defined in src/poly/evaluation.mojo.

Enclosure.value¶

def value(self, mut budget: Budget) raises PolyError -> Self.D.Scalar

Copy the enclosing scalar.

Arguments.

• budget: The shared work allowance.

Returns. The ball enclosing every evaluation allowed by the stored inputs.

Raises.

• PolyError: LIMIT/CAPACITY on resource limits.

Enclosure.value¶

def value(self, *, max_steps: UInt64 = UInt64.MAX) raises PolyError -> Self.D.Scalar

Copy the enclosing scalar with a work limit.

Arguments.

• max_steps: The complete call's work allowance.

Returns. An independent ball value.

Raises.

• PolyError: LIMIT/CAPACITY on resource limits.

Enclosure.precision¶

def precision(self) -> Int

Return the output midpoint precision in bits.

Returns. The precision used for the last enclosure.

Enclosure.outcome¶

def outcome(self) -> Optional[NumericOutcome]

Return the adaptive accuracy outcome, when accuracy was requested.

Returns. SUCCESS or PRECISION_CEILING for adaptive calls; None for fixed precision.

Enclosure.accurate¶

def accurate(self) -> Bool

Report whether an adaptive accuracy request succeeded.

Returns. True only for an adaptive SUCCESS; call check to verify the evidence.

Enclosure.options¶

def options(self) -> Optional[NumericOptions]

Return the original accuracy request when present.

Returns. The retained numerical options, or None for fixed precision.

Enclosure.evidence¶

def evidence(self) -> ref[ImmOrigin(origin_of(self._data[].proof.evaluation))] EnclosureEvaluation[Self.D]

Borrow the evaluation trace.

For algebraic coefficients, keep the complete result for conversion witnesses checked by evaluation.check; this accessor exposes only the trace.

Returns. Immutable output and rational bounds for every arithmetic step.

check¶

def check[C: AnyType, D: NumericDomain, numerical: Bool, sparse: Bool](result: Enclosure[C, D, numerical, sparse], mut budget: Budget) raises PolyError -> Bool

Verify every enclosure step and any retained accuracy claim.

An inconclusive adaptive result can pass this check. Inspect accurate() or outcome() to learn whether the requested width was reached.

Parameters.

• C: Inferred from the input types.
• D: The numerical coefficient domain.
• numerical: Inferred from the input types.
• sparse: Inferred from the input types.

Arguments.

• result: The result and its retained evidence.
• budget: The shared work allowance.

Returns. Whether the evidence is valid.

Raises.

• PolyError: DOMAIN for invalid input, or LIMIT/CAPACITY on resource limits.

Defined in src/poly/evaluation.mojo.

Incremental witnesses¶

dense.enclose_stream and sparse.enclose_stream accept the same fixed-precision inputs as enclose. Construct enclose_checker with the same inputs and context, forward every event, then check the final receipt. See the streaming tutorial for a complete example.

Algebraic coefficients or points select AlgebraicEnclosureStream. Its producer refines one input per event; its checker verifies that input's root identity, interval containment, and outward numerical bounds. Coefficient events precede point events, then arithmetic events. The receipt remains a core StreamedEnclosure, with steps counting the complete facade event sequence. Pass it to the matching facade checker.

Without algebraic inputs, the return types remain the core EnclosureStream and EnclosureStreamChecker, and events remain NumericBox values. Type inference lets the same forwarding loop work with either family.

AlgebraicEnclosureStream¶

@fieldwise_init
struct AlgebraicEnclosureStream[C: AnyType, D: NumericDomain, numerical: Bool, sparse: Bool, checking: Bool](Movable)

Refine algebraic inputs and check their evidence before streaming arithmetic.

Construct this through dense.enclose_stream or sparse.enclose_stream, and construct its matching checker through enclose_checker. It keeps input storage and the live arithmetic state, but no history of emitted steps.

Parameters.

• C: The original coefficient ring or numerical domain.
• D: The inferred real or complex ball domain.
• numerical: Whether the original polynomial has numerical coefficients.
• sparse: Whether the original polynomial uses sparse storage.
• checking: Whether this instance accepts evidence instead of producing it.

Defined in src/poly/evaluation.mojo.

AlgebraicEnclosureStream.step_count¶

def step_count(self) -> Int

Return the complete stream length, including input evidence.

Returns. The number of refinement and arithmetic events required for completion.

AlgebraicEnclosureStream.next¶

def next(mut self, mut budget: Budget) raises PolyError -> Optional[EnclosureStep[Self.D]]

Refine one input or produce the next arithmetic bound.

Arguments.

• budget: The shared allowance for refinement, storage, and arithmetic.

Returns. The next event, or None after all events have been emitted.

Raises.

• PolyError: DOMAIN for invalid inputs, LIMIT or CAPACITY on resource exhaustion. A failed operation does not consume its event.

AlgebraicEnclosureStream.accept¶

def accept(mut self, var step: EnclosureStep[Self.D], mut budget: Budget) raises PolyError -> Bool

Check the next root witness or arithmetic bound independently.

Root identity, interval containment, and outward bounds are checked without repeating the producer's root refinement.

Arguments.

• step: The next owned event in the producer's order.
• budget: The shared checking allowance.

Returns. True on acceptance. False permanently invalidates this checker.

Raises.

• PolyError: LIMIT or CAPACITY on exhaustion; the event is not consumed.

AlgebraicEnclosureStream.finish¶

def finish(self, mut budget: Budget) raises PolyError -> StreamedEnclosure[Self.D]

Return a receipt after every refinement and arithmetic event.

Arguments.

• budget: The allowance for copying the final enclosure.

Returns. A scalar receipt whose steps include refinement events.

Raises.

• PolyError: DOMAIN for an incomplete stream, LIMIT or CAPACITY on exhaustion.

AlgebraicEnclosureStream.finish¶

def finish(self, receipt: StreamedEnclosure[Self.D], mut budget: Budget) raises PolyError -> Bool

Verify completion and the final scalar against accepted input evidence.

Arguments.

• receipt: The producer's final scalar and total event count.
• budget: The shared allowance for final verification.

Returns. Whether all expected events and the receipt have been checked.

Raises.

• PolyError: LIMIT or CAPACITY on exhaustion.

EnclosureStep¶

@fieldwise_init
struct EnclosureStep[D: NumericDomain](Copyable, Movable)

One coefficient refinement, point refinement, or arithmetic bound.

Forward each step unchanged to the matching checker. Coefficients precede algebraic coordinates, which precede arithmetic. Only the active payload may be present.

Parameters.

• D: The inferred real or complex ball domain.

Defined in src/poly/evaluation.mojo.

RefinedInput¶

@fieldwise_init
struct RefinedInput[D: NumericDomain](Copyable, Movable)

An outward numerical input and exact witnesses for its real and imaginary parts.

Parameters.

• D: The inferred real or complex ball domain.

Defined in src/poly/evaluation.mojo.