Proved static-byte binary-interchange formats

This is the public entry point for the static-byte representation and table certificates, exact conversion capabilities, default proved ExecFloat backends, and optional policy-driven planning infrastructure.

Backend

This module exposes family-selected operations, their refinement theorems, and the default ExecFloat capability instances. Runtime-only consumers should import StaticByte.Backend.Runtime.

Core

This module exposes the compact static-byte runtime, lazy verified table construction, and the proof bridges used by nominal binary formats. Runtime-only consumers should import StaticByte.Core.Runtime.

Conversion

This module exposes exact-rational decoding, explicit-policy quantization, installed conversion instances, and their reduction theorems. Runtime-only consumers should import StaticByte.Conversion.Runtime.

Plan

This module exposes static-byte cost estimates, first-order dispatch, its correctness theorems, and verified ExecFloat capability constructors. Runtime-only consumers should import StaticByte.Plan.Runtime.