ADR-0018 — Legacy SCMValue literals are exact assertions¶

Status: proposed
Date: 2026-08-31
Owners: ZeroProofML maintainers
Supersedes / superseded by: none

Context¶

Legacy SCMValue division maps a raw zero denominator to algebraic bottom. Typed SemanticResult and ResultTensor division instead require certified PROVEN_ZERO; an unannotated integer or floating zero is only machine evidence and yields ambiguous rejected NO_CORE. Without a named distinction, the same glyph appeared to have contradictory semantics.

Decision¶

Retain SCMValue as the compatibility/exact-assertion carrier. Values passed to SCMValue, scm_real, or scm_complex assert exact algebraic literals for that legacy API, so raw zero remains a bottom-producing denominator. Add scm_assert_exact_real and scm_assert_exact_complex as unambiguous spellings.

New evidence-bearing code uses SemanticResult/ResultTensor. In those APIs, the Python type of 0 or 0.0 never proves exactness. Only typed exact-zero evidence with its certificate can produce semantic bottom.

Legacy scalar overflow is not algebraic bottom. Operators and helper functions share one checked kernel and raise OverflowError for non-finite finite-input results.

Consequences¶

Compatibility behavior remains available without weakening typed APIs. Docs and examples must say which assertion is made. SCMValue.value stores None for bottom; it does not use a numeric sentinel.

Alternatives considered¶

Changing SCMValue division to require new certificates would be a larger compatibility break and would blur its role beside the typed result APIs. Treating typed integer zero as proof would reintroduce the evidence ambiguity ADR-0012 removed.

Verification and rollout¶

Tests pin legacy raw-zero bottom, typed raw-zero ambiguity, certified typed bottom, and uniform operator/helper overflow. Maintainer approval is required before changing this ADR from proposed to accepted.