Build UnitSentinel's dimensional proof engine

[omar07ibrahim]

Why

ML model contracts usually preserve tensor shape and dtype while losing the physical meaning of features. UnitSentinel treats dimensions, unit scales, affine offsets, and absolute-versus-delta temperature semantics as exact program contracts.

Implemented

Exact trust boundary

• immutable seven-base SI dimension vectors with bounded rational exponents
• exact unit and quantity values with no float coercion
• immutable, content-addressed 33-unit registry with 10 explicit aliases
• affine Celsius/Fahrenheit/Kelvin semantics and explicit temperature deltas
• bounded topological computation-graph IR
• strict canonical UTF-8 JSON decoder that rejects duplicate keys, floats, BOMs, unknown fields, excessive structure, and noncanonical bytes before trust

Tracked formal verification

• Z3 4.16 pinned as the exact runtime solver
• exact constraints for all 15 graph operations
• simultaneous inference of 7-component dimension, quantity kind, scale, and offset
• fail-closed verified, underconstrained, conflict, and unknown outcomes
• explicit scale provenance, so direct m + cm, one + percent, and cross-scale temperature arithmetic cannot silently pass
• exact conversion semantics for km/h to m/s and Fahrenheit to Celsius
• alternate-model queries before any positive result; SAT alone is never called verified
• source-labelled tracked assertions and deterministically minimized conflict witnesses
• monotonic per-check and whole-run deadlines, memory bounds, redacted solver failures, and exact model extraction
• independent Python replay of every SAT model before publication
• content-addressed public results that include exact inferred scale and offset

Verification

• 101 unit, integration, and adversarial tests
• 95% total statement/branch coverage; exact domain layer remains at 100%
• exhaustive audit of 180 built-in temperature arithmetic/conversion combinations with zero semantic mismatches
• a 30-node irrelevant suffix reduces to the same three causal conflict witnesses in four solver checks
• a maximum-size 512-node annotated identity graph verifies in two solver checks
• Ruff, strict mypy, compileall, sdist/wheel build, isolated wheel installation, and dependency audit pass
• independent read-only soundness audit found no remaining false-verified scenario or soundness blocker

Planned in this draft

• canonical proof certificates and offline replay
• bounded repair proposals
• training/serving contract comparison and an ONNX adapter
• reproducible CLI captures, architecture diagrams, benchmark plots, and an end-to-end demo generated from implemented behavior

No repair, certificate-replay, ONNX-support, or model-accuracy claim is made yet.