Implementation Verification Report (v0.6.1 SCM)

This report summarises what is implemented in the v0.6.1 Signed Common Meadows (SCM) codebase and what the current contracts are. v0.6.1 is a compatible containment patch on top of v0.6.0; the material behavior changes are called out inline.

Scope: the v0.6.1 Python packages zeroproof/ and zeroproofml/ (compatibility shim).

Numerical Scope Summary

The ideal SCM algebra remains total: exact singularities produce the absorptive bottom element. Finite IEEE execution is surfaced through the public boundary for each runtime surface:

  • Scalar SCMValue rejects direct non-finite construction (ValueError) and finite-op-finite overflow (OverflowError); from_ieee(NaN/±Inf) is the explicit boundary that maps external non-finite IEEE payloads to ⊥.
  • Vectorized NumPy / Torch / JAX helpers fold incoming masks, non-finite inputs, unsupported real domains, and backend non-finite results into the returned mask, with finite zero placeholders in masked payload slots. Complex vector pow accepts real exponents only; complex exponents are refused.
  • SCMRationalLayer training/autograd is real-valued only. Non-finite inputs, overflowed basis features, non-finite numerator/denominator values, singular denominators, and finite-over-finite quotient overflow are folded into bottom_mask.
  • Strict inference separates finite semantic bottoms from finite-machine faults as semantic_bottom_mask and fault_mask; bottom_mask is their union.

See 01_scm_foundations.md for the canonical table.

✅ Core domain: SCMValue and ⊥

Code: zeroproof/scm/value.py

  • SCMValue represents either a numeric payload (float/complex) or the absorptive bottom element ⊥ (is_bottom=True).
  • Bottom is absorptive for + and ·; division by zero yields bottom.
  • Factories: scm_real, scm_complex, scm_bottom.
  • v0.6.1 (P0-01): __post_init__ refuses non-finite payloads (NaN, ±Inf, complex components) at construction with ValueError. Route non-finite IEEE inputs through zeroproofml.utils.ieee_bridge.from_ieee(...) instead.

✅ Scalar arithmetic helpers

Code: zeroproof/scm/ops.py, zeroproof/scm/value.py

  • Scalar helpers implement totalised arithmetic: scm_add, scm_sub, scm_mul, scm_div, scm_inv, scm_neg, scm_pow.
  • Transcendentals are bottom-aware with domain checks: scm_log, scm_exp, scm_sqrt, scm_sin, scm_cos, scm_tan.
  • v0.6.1 (P0-01): finite-op-finite scalar arithmetic that produces a non-finite result raises OverflowError at the operator boundary. Numerical faults are no longer silently reclassified as algebraic bottom.

✅ Vectorised SCM + masks (NumPy / Torch / JAX)

Code: zeroproof/scm/ops.py

Vectorised entry points propagate a separate boolean bottom mask: - NumPy: scm_*_numpy - Torch: scm_*_torch - JAX: scm_*_jax

Each returns (payload, mask) and treats: - mask=True as ⊥ - division by zero / inverse of zero as ⊥ (adds to the mask) - non-finite inputs, unsupported real domains, and finite IEEE results that overflow to NaN / ±Inf as bottom in the returned mask; masked payloads are zero placeholders, not mathematical values.

v0.6.1 historical note (P1-07): positional mask forms warned during the compatibility window. v0.7.0a1 update: mask_x / mask_y are keyword-only in canonical and compatibility namespaces; the positional and historical interleaved forms now raise TypeError. v0.6.1 (P0/P1 vector containment): vectorized NumPy / Torch / JAX helpers share a finalizer that combines incoming masks, domain failures, and post-operation non-finite results. Hazardous masked operands are substituted before multiplication, division, power, exp, trig, log, sqrt, and reciprocal paths so masked Torch gradients stay finite. Real pow / log / sqrt reject unsupported domains into the mask; complex vector log / sqrt / pow follow the scalar boundary where tested, with pow limited to real exponents and complex exponents refused. NumPy integer reciprocal promotes to floating output instead of returning integer zeros.

✅ IEEE-754 bridge (scalar)

Code: zeroproof/utils/ieee_bridge.py

  • from_ieee: routes NaN and ±Inf to ⊥ at this named boundary. This is the only supported entry point for non-finite IEEE inputs (bare SCMValue(float("nan")) construction raises ValueError).
  • to_ieee: maps ⊥ to NaN (tooling-friendly sentinel).
  • The bridge's non-finite→⊥ mapping is an explicit boundary convention (mirrors zeroproof/scm/fracterm.py::_coerce_numeric), not a covert fault-to-bottom conversion. See the module docstring.

✅ Gradient policies (SCM semantics)

Code: zeroproof/autodiff/policies.py

  • Policy enum: CLAMP, PROJECT, REJECT, PASSTHROUGH
  • Context manager: gradient_policy(...)
  • Utilities: apply_policy, apply_policy_vector

✅ Torch SCM rational layer with bottom mask + policy hook

Code: zeroproof/layers/scm_rational.py

  • SCMRationalLayer.forward(x) -> (output, bottom_mask)
  • Singularities are detected via denominator ≈ 0 and surfaced as bottom_mask.
  • v0.6.1 (P0-03): the forward path classifies non-finite inputs and overflowed basis features before multiplying by trainable parameters, classifies non-finite numerator / denominator values before division, and substitutes finite safe operands at every flagged index. A singular or feature-invalid sample in a mixed batch cannot poison gradients on other batch elements. Sub-float64 inputs get an additional promoted-float64 pre-division overflow bound so the ill-conditioned Jacobian of a finite/finite overflow never enters the autograd graph. The output payload at bottom indices is a documented placeholder (0.0); the bottom_mask is authoritative. singular_epsilon is validated as finite and non-negative at construction.
  • SCMRationalLayer training/autograd is real-valued only in v0.6.1. Complex support remains limited to scalar SCM values and strict-inference decoding paths.
  • Policies are applied by registering a backward hook on output gradients (PROJECT / REJECT / CLAMP); PASSTHROUGH disables the hook (safe because of the basis and pre-division substitution).

✅ Mask-aware layers and losses

Code: zeroproof/layers/normalization.py, zeroproof/losses/*.py

  • v0.6.1: SCMNorm uses where(valid, x, 0) before masked reductions, so a masked NaN payload does not contaminate unmasked means, variances, or a second SCMNorm layer. eps is validated as finite and non-negative.
  • v0.6.1: sign_consistency_loss and margin_loss use safe selection before reduction when masks are provided; masked NaN samples cannot contaminate selected samples or their gradients. scm_separation_losses expands broadcastable masks before reduction.
  • Loss scalars are validated at public boundaries: gamma, tau_train, epsilon_sing, tau_bot, tau_finite, and LossConfig weights must be finite and in their documented domains.

✅ Proof / oracle refusals

Code: zeroproof/scm/_eager_oracle.py, zeroproof/layers/fru.py

  • v0.6.1 (P0-04): evaluate_fru_expression defaults to operational compatibility mode and emits a RuntimeWarning for floating coefficients / assignments. Proof / certificate / checker callers must pass strict=True, which refuses those inputs with FloatingCoefficientRefusal (a ValueError). The repository does not currently provide an exact-rational subprofile.
  • v0.6.1 (P1-04): FRUExpression.flatten() runs a memoized DAG walk to estimate pre-expansion work and refuses FLATTEN_MAX_WORK = 100_000 (or per-term FLATTEN_MAX_TERM_PRODUCT = 10_000) with FRUResourceRefusal(RuntimeError). max_flatten_work / max_term_product keyword arguments raise the budget explicitly.

✅ Strict-inference threshold contract

Code: zeroproof/layers/_capability.py, zeroproof/inference/mode.py, zeroproof/inference/patterns.py, zeroproof/inference/bundle.py, zeroproof/training/trainer.py

  • v0.6.1 (P0-02): shared validators enforce that tau_infer is finite and strictly positive, and that tau_train (if set) is finite, positive, and >= tau_infer. The validators run at every boundary: InferenceConfig(...), decode_strict_censored_3way(...), TrainingConfig(...), validate_bundle(bundle_dir). The historical tau_infer = 0 fail-open path is refused before any prediction is produced. Eager Torch / NumPy / JAX strict decoders also reject positive thresholds that narrow to 0.0 in the denominator dtype, using the real component dtype for complex denominators; classify exact-zero denominators as semantic bottom independently of the threshold comparison; and fold non-finite decoded quotients back into fault_mask / bottom_mask before returning. The regression matrix covers float16/bfloat16 where supported, float32, float64, complex64, and complex128, with the JAX-extra CI lane running the JAX cases on CPU with x64 enabled. Any wording of the form "bottom is unreachable by construction" that depended on tau = 0 no longer applies.

✅ Trainer loop

Code: zeroproof/training/trainer.py

  • SCMTrainer.fit() returns per-step logs including loss and coverage.
  • Coverage is estimated from NaN on decoded tensors or from projective denominators.
  • Supports gradient accumulation and mixed precision (AMP).
  • v0.6.1 (P1-03): partial accumulation groups are flushed at epoch end and scaled by their actual group size; scheduler cadence is explicit (per_batch / per_optimizer_update / per_epoch / per_validation_metric); validation aggregation is sample-count-weighted with per-key custom reducers; early stopping reads the validation aggregate, not the last training-batch metric. Checkpoints use schema v1 (schema_version=1) with scheduler / epoch / global_step / best_metric / rng_state / config_hash in addition to model / optimizer / scaler; pre-v1 checkpoints still load with resume state at defaults. fit() calls optimizer.zero_grad(set_to_none=True) at the declared fit-start boundary and returns cleanly when a resumed checkpoint sits at or beyond max_epochs.

Intentional non-goals (v0.6.1)

  • No Transreal tags (+∞, −∞, Φ) in the core; Transreal-era scripts under examples/archive_tr/ are for historical reference and are not part of the v0.6.x import path.
  • No "Mask-REAL"/"Hybrid" transreal modes in the public API; use gradient policies and/or projective tuples instead.
  • The current release does not provide a multi-axis result taxonomy (CorePresence, CoreStatus, ExecutionStatus, ObservationStatus, OperationalDecision, RepresentationStatus, CompilationStatus), repository-wide gauge-policy centralization, an observation orthogonal axis, a physical zeroproofml.* module migration, or TrainingConfig.learning_rate wiring. Context-local gradient-policy isolation is implemented in this release.

v0.6.0 audit summary

Compact per-issue summary of the audit that motivated v0.6.1.

Release-blocking (P0)

  • P0-01 non-finite carrier escape. SCMValue accepted NaN/±Inf payloads without classification; fixed in v0.6.1 by raising ValueError at construction and OverflowError on scalar overflow.
  • P0-02 fail-open thresholds. tau_infer ∈ {0, negative, NaN, ±Inf} could yield Inf with all rejection masks False; finite P/Q quotient overflow could also escape as an unmasked non-finite decoded payload. Fixed in v0.6.1 with finite-positive validation at every boundary, dtype-narrowing guards across eager Torch / NumPy / JAX, independent exact-zero semantic-bottom classification, and post-division non-finite quotient faulting.
  • P0-03 singular-gradient poisoning. Raw basis overflows and raw division let invalid samples poison unrelated finite samples' gradients in the same batch; fixed in v0.6.1 by substituting finite feature placeholders before parameter multiplication and using a custom torch.autograd.Function that substitutes safe division operands and gates the gradient at every flagged index before any local division Jacobian is evaluated.
  • P0-04 floating proof oracle. The flattener silently treated float coefficients as proof-bearing; fixed in v0.6.1 by making proof / certificate / checker use pass strict=True, which refuses floats (including Fraction with denominator ≠ 1 and SCMValue wrapping a non-exact payload). The default evaluator path remains operational with warnings for compatibility; the repository does not currently provide an exact-rational subprofile.

Experiment-readiness (P1)

  • P1-01 gauge dependence. Projective rejection scores based on raw |Q| are not invariant across every call site so thresholds cannot be reused across bundles/heads/normalization conventions; deferred to v0.7 gauge-policy centralization.
  • P1-02 observation ↔ bottom conflation. Censored / missing / domain-invalid observations route to the same bottom slot as algebraic bottom, losing distinctions operators need; deferred to the v0.7 multi-axis taxonomy.
  • P1-03 trainer defects. Accumulation, validation aggregation, scheduler cadence, early stopping, and checkpoint schema each had correctness gaps; contained in v0.6.1 (schema v1, sample-weighted validation, actual-group scaling, metric-aware ReduceLROnPlateau, Inf-aware coverage, stable SHA-256 config hash, fit-start zero_grad, resume-past-end guard) with full non-finite loss/grad/optimizer-state accounting deferred.
  • P1-04 FRU pre-expansion blow-up. FRUExpression.flatten() walked shared-DAG bombs without a memoized budget; fixed in v0.6.1 by FRUResourceRefusal at FLATTEN_MAX_WORK = 100_000 with output-term counts propagated through FRUMul / FRUAdd / FRUDiv.
  • P1-05 replay gap. Advertised paper-replay commands referenced scripts/ files not shipped in the wheel/sdist so a wheel-only install could not run them; fixed in v0.6.1 by moving the shipped surface to python -m zeroproofml.… and adding wheel/sdist smoke tests to CI. Installed-artifact smoke now runs from neutral temporary working directories, keeps the repository root off sys.path, installs zeroproofml[benchmarks] for benchmark paths, executes a tiny shipped RR IK dataset module, and reaches the DOSE frozen-dirhead follow-up import boundary.
  • P1-06 namespace collision. An unrelated zeroproof distribution on PyPI can shadow the intended zeroproofml import path if installed first; deferred to v0.7 canonical-module migration with a loud-failure shim.
  • P1-07 broken bridge example + vector-API interleaved call. examples/bridge_demo.py did not run and scm_add_numpy(x, mask_x, y, mask_y) silently misinterpreted mask_x as y; both were fixed in v0.6.1. The historical positional form warned during that compatibility period and is now rejected; masks are keyword-only in v0.7.
  • P1-08 gradient-policy stack non-locality. The process-global stack was replaced with a context-local policy value; overlapping asyncio tasks and new threads no longer leak active overrides. Broader gauge-policy design remains deferred.