Proof-aware format-report profiles

A numerical family describes its representation, value classes, rounding, execution strategy, theorem groups, and proof limits with one FormatProfile, which supplies the data for #float_info.

Rendering and metaprogramming inspection live in separate modules. Keeping the schema independent lets family packages construct and validate reports without depending on the command UI.

opaque FloatLib.Floats.ExecFloat.floatlib.floatInfo.full : Lean.Option Bool

Whether #float_info should print the complete proof and backend audit.

opaque FloatLib.Floats.ExecFloat.floatlib.floatInfo.errors : Lean.Option Bool

Whether #float_info should focus on checked range, roundoff, and exactness guarantees.

structure FloatLib.Floats.ExecFloat.InfoEntry : Type

One labeled fact in a user-facing format report.

• label : String

  Short name shown on the left of the report.

• value : String

  Human-readable value or explanation.

def FloatLib.Floats.ExecFloat.yesNo (value : Bool) : String

Render a Boolean report field without exposing Lean's constructor names.

inductive FloatLib.Floats.ExecFloat.NumericalAnalysisKind : Type

The numerical role played by a theorem group in range or roundoff analysis.

• range : NumericalAnalysisKind

  An enclosure or a representable-output-range guarantee.

• rounding : NumericalAnalysisKind

  A theorem identifying the exact quantity and rounding rule used by an operation.

• absoluteError : NumericalAnalysisKind

  An absolute roundoff or approximation bound.

• relativeError : NumericalAnalysisKind

  A relative roundoff or approximation bound.

• exactness : NumericalAnalysisKind

  A zero-error or exact-representation result under the stated hypotheses.

structure FloatLib.Floats.ExecFloat.NumericalGuarantee : Type

The concise numerical statement attached to a checked theorem surface.

The statement summarizes the theorem for numerical users; the theorem declaration list and scope remain the authoritative Lean interface.

• kinds : List NumericalAnalysisKind

  Kinds of numerical analysis supported by the theorem group.

• statement : String

  Human-readable statement of the checked guarantee.

inductive FloatLib.Floats.ExecFloat.TheoremApplicability : Type

Whether a checked theorem group can be instantiated for the configured numerical type.

Input-specific premises such as finiteness or a nonzero divisor remain listed in scope. This status records only descriptor-level applicability.

• verifiedForType : TheoremApplicability

  The configured descriptor satisfies the theorem group's format requirements.

• conditional (condition : String) : TheoremApplicability

  The descriptor is supported, but another descriptor or relation must be chosen.

• unavailable (reason : String) : TheoremApplicability

  A descriptor-level premise of the theorem group is false for this type.

structure FloatLib.Floats.ExecFloat.TheoremSurface : Type

A group of checked declarations that gives mathematical meaning to an executable specification.

applicability records whether the configured type satisfies the group's descriptor-level premises. scope records remaining input or relation hypotheses. Declaration names are an index into the Lean API, not a replacement for checking the exact theorem statements.

• topic : String

  Mathematical topic covered by the declarations.

• declarations : List Lean.Name

  Principal public theorems. Every name is checked before the report is printed and must resolve to a theorem.

• definitions : List Lean.Name

  Definitions such as executable specifications or named constructors that the surface deliberately lists alongside its theorems. They are checked for existence only.

• applicability : TheoremApplicability

  Whether this group is available for the configured descriptor.

• scope : String

  Conditions under which the declarations apply.

• numericalGuarantee? : Option NumericalGuarantee

  Optional range, roundoff, or exactness meaning exposed by #float_info [errors].

  Numerical-analysis reports include only groups with an explicit guarantee in this field. The renderer uses that supplied guarantee rather than inferring bounds from declaration names.

structure FloatLib.Floats.ExecFloat.FormatProfile : Type

Family-defined descriptive information for one encoded numerical format.

• family : String

  Representation and semantics family, such as binary interchange or a codebook.

• standard : String

  Standards identity or an explicit statement that the format is nonstandard.

• declarationPrefix : String

  Namespace prefix omitted from declaration names in this family's rendered report.

• representation : List InfoEntry

  Representation parameters that determine the encoded type.

• values : List InfoEntry

  Finite and exceptional value classes represented by the encoding.

• rounding : List InfoEntry

  Rounding and literal-conversion behavior.

• conversions : List InfoEntry

  Installed explicit-conversion capabilities.

  Family elaborators populate this field by synthesizing the same ExactDecoder, Quantizer, and DefaultQuantizer instances used by execution. An empty list is retained for third-party profiles that have not opted into capability inspection yet.

• execution : List InfoEntry

  Runtime carrier and backend-selection behavior.

• specializedOperations : List InfoEntry

  Executable operations that belong to this carrier but not to the universal scalar ExecFloat interface.

  Examples include outward-rounded interval arithmetic, posit-quire accumulation, and explicit bounded-fixed-point overflow policies. Keeping these operations separate prevents a report from either hiding useful family APIs or falsely advertising them as scalar ExecFloat capabilities.

• theoremSurfaces : List TheoremSurface

  Principal semantic theorem surfaces available for this family.

• nonclaims : List String

  Claims deliberately outside the reported proof boundary.

@[reducible, inline]

abbrev FloatLib.Floats.ExecFloat.CoreOperationCoverage : Type

Proof-backed availability of the universal executable operations.

The operation enum defines the supported operation list. The family-specific #float_info elaborator synthesizes the actual proof-carrying capability for each entry, so this report does not maintain a second capability hierarchy that could drift from execution.

def FloatLib.Floats.ExecFloat.CoreOperationCoverage.none : CoreOperationCoverage

Empty universal-operation coverage for a family that does not use the ExecFloat API.

def FloatLib.Floats.ExecFloat.TheoremSurface.validateTheorems (surface : TheoremSurface) : Lean.MetaM Unit

Fail unless every listed theorem surface name is an existing theorem.

def FloatLib.Floats.ExecFloat.TheoremSurface.validateDefinitions (surface : TheoremSurface) : Lean.MetaM Unit

Fail unless every listed definition of a theorem surface exists in the environment.

def FloatLib.Floats.ExecFloat.FormatProfile.validateDeclarations (profile : FormatProfile) : Lean.MetaM Unit

Refuse to render a profile whose theorem surfaces are inconsistent with the environment.

Every rendered name under declarations must be an existing theorem, and every rendered name under definitions must exist. Errors-only mode checks names only in groups with a numerical guarantee. In every mode, all numerical guarantees must name at least one kind and one theorem.

partial def FloatLib.Floats.ExecFloat.unfoldUntilApp? (target : Lean.Name) (arity : Nat) (type : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Unfold project-local type abbreviations until a registered family constructor is exposed.

The target is tested before every unfolding step. This is essential for transparent, zero-cost carrier definitions: the inspector may unfold abbrev MyNumber := Family.Code ..., but must stop at Family.Code rather than normalize onward to its raw BitVec or integer representation.

def FloatLib.Floats.ExecFloat.unfoldUntilAppArgs? (target : Lean.Name) (arity : Nat) (type : Lean.Expr) : Lean.MetaM (Option (Array Lean.Expr))

Unfold project-local abbreviations until target is visible, then return its arguments.

Format inspectors normally need the constructor parameters rather than the application itself. Keeping that extraction here gives every inspector the same stopping point and arity check.