Docs

Development Guide

This guide is for extending ZeroProofML v0.6.0 code, examples, or deployment workflows while preserving the SCM contracts documented in the public API.

Development Rules

  • New public examples should use zeroproofml.* imports.
  • Keep zeroproof.* compatibility imports working when a legacy path exists.
  • Treat bottom_mask as authoritative; do not infer bottom status from payload NaNs inside SCM code.
  • Keep stable three-field unpacking as (decoded, bottom_mask, gap_mask).
  • Preserve the stable v0.6.x provenance attributes (fault_mask, semantic_bottom_mask, bottom_provenance) on eager result objects.
  • Preserve schema-v2 ONNX output order (decoded, bottom_mask, gap_mask, fault_mask, semantic_bottom_mask, bottom_provenance) and update strict_inference_schema_version when the contract changes.
  • Prefer ONNX bundle paths for new deployment work.

Stable Versus Experimental

Before promoting a helper, decide where it belongs:

Category Requirements
Stable API Public import path, tests, docs, compatibility expectations
Experimental API Clear opt-in status, no silent dependency from stable code
Example Runnable workflow tied to current docs
Benchmark helper Versioned artifacts and reproducibility context
Archive Kept for history; not a recommended entry point

Use API Reference as the current stable surface map.

Debugging Bottom Propagation

For tensor code, inspect payload, mask, and provenance:

result = strict_inference(P, Q, config=cfg)
decoded, bottom_mask, gap_mask = result

bottom_rate = float(bottom_mask.float().mean())
fault_rate = float(result.fault_mask.float().mean())
semantic_rate = float(result.semantic_bottom_mask.float().mean())

Debug questions to ask:

  • Is a bottom coming from a non-finite payload (fault_mask) or a finite threshold trigger (semantic_bottom_mask)?
  • If fault_rate is unexpectedly high, does the head use IEEE arithmetic where SCM-aware fracterm arithmetic was intended?
  • Did a prior input already carry bottom_mask=True?
  • Is the model over-rejecting to reduce fit loss?
  • Did a downstream conversion drop the mask and keep only NaN payloads?
  • Is tau_infer too aggressive for the held-out denominator distribution or gauge convention?

Logging During Development

Use stable JSONL logs for runs you may compare later:

from zeroproofml.utils.logging import JsonlLogger, metric_log_record

logger = JsonlLogger("runs/debug_metrics.jsonl")
logger(metric_log_record({"coverage": 0.98, "bottom_rate": 0.02}, phase="eval"))

The JSONL schema keeps:

  • schema_name="zeroproofml.metric_log"
  • schema_version=1
  • record_type
  • phase
  • step and epoch when available
  • nested metrics
  • optional context

Experimental helpers can load logs into pandas, aggregate multi-seed runs, and convert metric records to dashboard-friendly row formats. Keep JSONL as the durable artifact.

Testing Checklist

For SCM core changes:

  • Test finite arithmetic and bottom absorption.
  • Test IEEE bridge round-trips (including +Inf, -Inf, and NaN).
  • Test vectorized payload-plus-mask behavior.
  • Test backend parity when touching NumPy, Torch, or JAX helpers.
  • Test strict simplification versus explicit simplification_mode="field_rational" opt-in behavior.

For projective or training changes:

  • Test strict decode near Q=0 and with non-finite payloads.
  • Test sign consistency and orientation-sensitive cases with the singular-only default.
  • Test coverage/rejection behavior for both the hard rejection_loss and the differentiable soft_coverage_loss.
  • Test TrainingConfig logging, validation metrics, and the allow_bottom_unreachable escape hatch when changing the trainer.

For deployment changes:

  • Test validate_bundle(...) on both schema-v1 and schema-v2 bundles.
  • Test ONNX Runtime loading for the six-output schema-v2 contract.
  • Test reference smoke parity against the wrapped model.
  • Test output names and order.
  • Test metadata schema changes explicitly.
  • Test that consumers ignoring bottom_mask fail visibly (bad-consumer contract tests).

Provenance Diagnostics

The v0.6.x fault/semantic mask set is stable and no longer requires an experimental opt-in. When adding or consuming provenance diagnostics:

  • Keep three-field unpacking working.
  • Preserve the bottom_mask == fault_mask | semantic_bottom_mask relation.
  • Route non-finite payloads through fault_mask, not semantic_bottom_mask.
  • Alert on fault_rate, semantic_bottom_rate, and numerical_hazard_rate separately.
  • Keep numerical_hazard_threshold as monitor-only metadata; do not fold finite tiny denominators into fault_mask.

FRU structural-validity provenance (FlattenedFRU.strict_validity_sources, FlattenedFRU.validity_factors) is a separate experimental axis. Any promotion should define a new structural-provenance gate at that time rather than reuse the fault/semantic mask criteria.

FRU And Flattening Work

FRU flattening is intentionally local:

  • flatten small rational heads
  • enforce depth (L <= 5) and degree bounds (16 * d cap by default)
  • record denominator provenance
  • use the flattened artifact for audit/export validation

Strict flattening refuses depth/degree-bound violations rather than using field-rational rescue rewrites. Strict cancellation refuses symbolic factor cancellation unless the factor is a safe numeric constant or is covered by a proven or declared nonzero assumption (DomainAssumption, FlattenedFRU.cancellation_domain_assumptions).

FractermRationalUnit.flatten_expression(..., preserve_unflattened=True) returns UnflattenedFRUAudit instead of raising when strict flattening exceeds the local budget; it is an audit-only record, not a runtime eager-evaluation fallback.

Do not turn FRU flattening into a whole-network symbolic compiler or a per-step training operation. If an expression is outside the supported algebraic fragment, keep it on the projective path.

Example Maintenance

Use this labeling when adding examples:

Label Meaning
Quickstart Short onboarding script for SCM basics
Supported example Maintained workflow aligned with public APIs and docs
Benchmark helper Feeds benchmark/reproduction stack
Archival/experimental Historical or exploratory path

Promoted tutorial path:

python examples/01_quickstart.py
python examples/02_rational_layer.py
python examples/03_projective_mode.py
python examples/05_coverage_control.py
python examples/06_export_bundle.py
python examples/fru_strict_check_demo.py

For robotics, current supported entry points are the benchmark harness, the reference deployment script, and importable zeroproofml.reference_robotics_* helpers. Older examples/robotics/* scripts are mostly archive or experimental unless explicitly documented otherwise.

Release Documentation Checks

Before publishing docs for a release:

  • Search for stale version references.
  • Confirm canonical imports use zeroproofml.*.
  • Confirm old links point to existing doc slugs.
  • Keep design decisions out of onboarding pages unless they affect users.
  • Keep experimental features visibly labeled.
  • Regenerate reports from artifacts instead of manually copying metrics.