Representation-independent executable numerical values

ExecFloat F is the public runtime carrier selected by an EncodedFormat F. Neither this carrier nor EncodedFormat assumes a floating radix or an IEEE layout. Its runtime representation is exactly the family-chosen FormatCode F type. Semantic interpretation is required only by proof-facing definitions, so noncomputable real semantics cannot disable code generation for the carrier.

The nominal format tag is a proposition attached through Subtype. Lean specifies that a subtype is represented identically to its carrier in compiled code, so a static format using UInt32 continues to cross generated entry points as a native 32-bit word. See the source documentation on Subtype in Lean's Init.Prelude: https://github.com/leanprover/lean4/blob/v4.34.0/src/Init/Prelude.lean#L641-L643. Static format packages may therefore choose UInt8, UInt32, UInt64, fixed limb records, or another direct carrier, while dynamic packages may choose descriptor-bearing or runtime-sized storage without changing the universal API.

The checks under benchmarks/scripts/checks/ validate the carrier specialization used by public operations. Lean's runtime and specialization behavior are specified by the Lean reference manual: https://lean-lang.org/doc/reference/latest/.

inductive FloatLib.Floats.ExecFloatTag (F : Type u) : Prop

Erased nominal evidence distinguishing the executable values of different formats.

This proposition has one constructor and contains no data. Its purpose is type separation, not runtime validation.

• intro {F : Type u} : ExecFloatTag F

@[reducible, inline]

abbrev FloatLib.Floats.ExecFloat (F : Type u) [Numerics.EncodedFormat F] : Type u_1

The executable value of format F.

The value is represented exactly as the arbitrary family-selected FormatCode F; the proof-only tag introduces no runtime descriptor, bit-vector, radix, or exceptional-value assumption.

class FloatLib.Floats.ExecFloat.FormatDisplay (F : Type u) [Numerics.EncodedFormat F] : Type u_1

Human-readable formatting supplied by an encoded numerical family.

The formatter receives the family-selected runtime code directly. Keeping this contract below ExecFloat lets every representation print its mathematical value without requiring a universal radix, exceptional-value model, or conversion through a host floating-point type.

• format : Numerics.FormatCode F → String

  Render one runtime code according to the format's own numerical semantics.

class FloatLib.Floats.ExecFloat.ModelCodec {Plan : Type u} (plan : Plan) (Model : Type v) (Code : outParam (Type w)) : Type (max v w)

Lossless conversion between a runtime carrier and its proof model.

plan is an arbitrary static index used only to distinguish carrier choices during typeclass search. The contract itself is independent of radix, encoding, exceptional values, and arithmetic semantics. Format families therefore share these inverse laws while keeping their storage plans and model types separate.

• toModel : Code → Model

  Decode one runtime code into the proof model.

• ofModel : Model → Code

  Pack one proof-model value into the runtime carrier.

• toModel_ofModel (value : Model) : toModel plan (ofModel plan value) = value

  Decoding after packing is exact.

• ofModel_toModel (value : Code) : ofModel plan (toModel plan value) = value

  Packing after decoding preserves the runtime code.

@[inline]

def FloatLib.Floats.ExecFloat.ofRaw {F : Type u} [Numerics.EncodedFormat F] (raw : Numerics.FormatCode F) : ExecFloat F

Wrap one family-selected code without conversion.

@[inline]

def FloatLib.Floats.ExecFloat.raw {F : Type u} [Numerics.EncodedFormat F] (value : ExecFloat F) : Numerics.FormatCode F

The family-selected code, exposed as a field-like projection for format implementations.

@[inline]

def FloatLib.Floats.ExecFloat.applyUnary {F : Type u} [Numerics.EncodedFormat F] (operation : Numerics.FormatCode F → Numerics.FormatCode F) (value : ExecFloat F) : ExecFloat F

Apply a unary operation directly to the family-selected runtime code.

@[inline]

def FloatLib.Floats.ExecFloat.applyBinary {F : Type u} [Numerics.EncodedFormat F] (operation : Numerics.FormatCode F → Numerics.FormatCode F → Numerics.FormatCode F) (left right : ExecFloat F) : ExecFloat F

Apply a binary operation directly to family-selected runtime codes.

@[inline]

def FloatLib.Floats.ExecFloat.applyTernary {F : Type u} [Numerics.EncodedFormat F] (operation : Numerics.FormatCode F → Numerics.FormatCode F → Numerics.FormatCode F → Numerics.FormatCode F) (left right third : ExecFloat F) : ExecFloat F

Apply a ternary operation directly to family-selected runtime codes.

@[simp]

theorem FloatLib.Floats.ExecFloat.raw_ofRaw {F : Type u} [Numerics.EncodedFormat F] (raw : Numerics.FormatCode F) : (ofRaw raw).raw = raw

Reading the raw code immediately after wrapping it returns the original code.

@[simp]

theorem FloatLib.Floats.ExecFloat.ofRaw_raw {F : Type u} [Numerics.EncodedFormat F] (value : ExecFloat F) : ofRaw value.raw = value

Wrapping the raw code of an executable value reconstructs that value.

theorem FloatLib.Floats.ExecFloat.ext {F : Type u} [Numerics.EncodedFormat F] {left right : ExecFloat F} (h : left.raw = right.raw) : left = right

Two executable values are equal when their family-selected codes are equal.

theorem FloatLib.Floats.ExecFloat.ext_iff {F : Type u} [Numerics.EncodedFormat F] {left right : ExecFloat F} : left = right ↔ left.raw = right.raw

@[inline]

def FloatLib.Floats.ExecFloat.ModelCodec.decode {F : Type u} [Numerics.EncodedFormat F] {Plan : Type v} {plan : Plan} {Model : Type w} [codec : ModelCodec plan Model (Numerics.FormatCode F)] (value : ExecFloat F) : Model

Decode an executable value through its lossless proof-model codec.

@[inline]

def FloatLib.Floats.ExecFloat.ModelCodec.encode {F : Type u} [Numerics.EncodedFormat F] {Plan : Type v} {plan : Plan} {Model : Type w} [codec : ModelCodec plan Model (Numerics.FormatCode F)] (value : Model) : ExecFloat F

Encode a proof-model value through its lossless runtime codec.

@[inline]

def FloatLib.Floats.ExecFloat.ModelCodec.liftUnary {F : Type u} [Numerics.EncodedFormat F] {Plan : Type v} {plan : Plan} {Model : Type w} [codec : ModelCodec plan Model (Numerics.FormatCode F)] (operation : Model → Model) (value : ExecFloat F) : ExecFloat F

Lift a unary proof-model operation to the executable carrier.

@[inline]

def FloatLib.Floats.ExecFloat.ModelCodec.liftBinary {F : Type u} [Numerics.EncodedFormat F] {Plan : Type v} {plan : Plan} {Model : Type w} [codec : ModelCodec plan Model (Numerics.FormatCode F)] (operation : Model → Model → Model) (left right : ExecFloat F) : ExecFloat F

Lift a binary proof-model operation to the executable carrier.

@[inline]

def FloatLib.Floats.ExecFloat.ModelCodec.liftTernary {F : Type u} [Numerics.EncodedFormat F] {Plan : Type v} {plan : Plan} {Model : Type w} [codec : ModelCodec plan Model (Numerics.FormatCode F)] (operation : Model → Model → Model → Model) (left right third : ExecFloat F) : ExecFloat F

Lift a ternary proof-model operation to the executable carrier.

@[simp]

theorem FloatLib.Floats.ExecFloat.ModelCodec.decode_encode {F : Type u} [Numerics.EncodedFormat F] {Plan : Type v} {plan : Plan} {Model : Type w} [codec : ModelCodec plan Model (Numerics.FormatCode F)] (value : Model) : decode (encode value) = value

Decoding immediately after encoding recovers the proof-model value.

@[simp]

theorem FloatLib.Floats.ExecFloat.ModelCodec.encode_decode {F : Type u} [Numerics.EncodedFormat F] {Plan : Type v} {plan : Plan} {Model : Type w} [codec : ModelCodec plan Model (Numerics.FormatCode F)] (value : ExecFloat F) : encode (decode value) = value

Encoding immediately after decoding recovers the executable value.

@[simp]

theorem FloatLib.Floats.ExecFloat.ModelCodec.decode_liftUnary {F : Type u} [Numerics.EncodedFormat F] {Plan : Type v} {plan : Plan} {Model : Type w} [codec : ModelCodec plan Model (Numerics.FormatCode F)] (operation : Model → Model) (value : ExecFloat F) : decode (liftUnary operation value) = operation (decode value)

Decoding a lifted unary operation exposes the underlying proof-model operation.

@[simp]

theorem FloatLib.Floats.ExecFloat.ModelCodec.decode_liftBinary {F : Type u} [Numerics.EncodedFormat F] {Plan : Type v} {plan : Plan} {Model : Type w} [codec : ModelCodec plan Model (Numerics.FormatCode F)] (operation : Model → Model → Model) (left right : ExecFloat F) : decode (liftBinary operation left right) = operation (decode left) (decode right)

Decoding a lifted binary operation exposes the underlying proof-model operation.

@[simp]

theorem FloatLib.Floats.ExecFloat.ModelCodec.decode_liftTernary {F : Type u} [Numerics.EncodedFormat F] {Plan : Type v} {plan : Plan} {Model : Type w} [codec : ModelCodec plan Model (Numerics.FormatCode F)] (operation : Model → Model → Model → Model) (left right third : ExecFloat F) : decode (liftTernary operation left right third) = operation (decode left) (decode right) (decode third)

Decoding a lifted ternary operation exposes the underlying proof-model operation.

theorem FloatLib.Floats.ExecFloat.ModelCodec.decode_injective {F : Type u} [Numerics.EncodedFormat F] {Plan : Type v} {plan : Plan} {Model : Type w} [codec : ModelCodec plan Model (Numerics.FormatCode F)] {left right : ExecFloat F} (equality : decode left = decode right) : left = right

Codec decoding is injective because encoding is its inverse.

theorem FloatLib.Floats.ExecFloat.ModelCodec.applyUnary_eq_lift {F : Type u} [Numerics.EncodedFormat F] {Plan : Type v} {plan : Plan} {Model : Type w} [codec : ModelCodec plan Model (Numerics.FormatCode F)] (operation : Numerics.FormatCode F → Numerics.FormatCode F) (modelOperation : Model → Model) (operation_eq : ∀ (value : Numerics.FormatCode F), toModel plan (operation value) = modelOperation (toModel plan value)) (value : ExecFloat F) : applyUnary operation value = liftUnary modelOperation value

Lift a proved unary code operation to ExecFloat.

The executable side remains the direct code operation; the model equation is proof-only.

theorem FloatLib.Floats.ExecFloat.ModelCodec.applyBinary_eq_lift {F : Type u} [Numerics.EncodedFormat F] {Plan : Type v} {plan : Plan} {Model : Type w} [codec : ModelCodec plan Model (Numerics.FormatCode F)] (operation : Numerics.FormatCode F → Numerics.FormatCode F → Numerics.FormatCode F) (modelOperation : Model → Model → Model) (operation_eq : ∀ (left right : Numerics.FormatCode F), toModel plan (operation left right) = modelOperation (toModel plan left) (toModel plan right)) (left right : ExecFloat F) : applyBinary operation left right = liftBinary modelOperation left right

Lift a proved binary code operation to ExecFloat.

The executable side remains the direct code operation; the model equation is proof-only.

theorem FloatLib.Floats.ExecFloat.ModelCodec.applyTernary_eq_lift {F : Type u} [Numerics.EncodedFormat F] {Plan : Type v} {plan : Plan} {Model : Type w} [codec : ModelCodec plan Model (Numerics.FormatCode F)] (operation : Numerics.FormatCode F → Numerics.FormatCode F → Numerics.FormatCode F → Numerics.FormatCode F) (modelOperation : Model → Model → Model → Model) (operation_eq : ∀ (left right third : Numerics.FormatCode F), toModel plan (operation left right third) = modelOperation (toModel plan left) (toModel plan right) (toModel plan third)) (left right third : ExecFloat F) : applyTernary operation left right third = liftTernary modelOperation left right third

Lift a proved ternary code operation to ExecFloat.

The executable side remains the direct code operation; the model equation is proof-only.

theorem FloatLib.Floats.ExecFloat.ModelCodec.liftUnary_congr {F : Type u} [Numerics.EncodedFormat F] {Plan : Type v} {plan : Plan} {Model : Type w} [codec : ModelCodec plan Model (Numerics.FormatCode F)] {leftOperation rightOperation : Model → Model} (equal : ∀ (value : Model), leftOperation value = rightOperation value) (value : ExecFloat F) : liftUnary leftOperation value = liftUnary rightOperation value

Pointwise-equal unary model operations have equal executable lifts.

theorem FloatLib.Floats.ExecFloat.ModelCodec.liftBinary_congr {F : Type u} [Numerics.EncodedFormat F] {Plan : Type v} {plan : Plan} {Model : Type w} [codec : ModelCodec plan Model (Numerics.FormatCode F)] {leftOperation rightOperation : Model → Model → Model} (equal : ∀ (left right : Model), leftOperation left right = rightOperation left right) (left right : ExecFloat F) : liftBinary leftOperation left right = liftBinary rightOperation left right

Pointwise-equal binary model operations have equal executable lifts.

theorem FloatLib.Floats.ExecFloat.ModelCodec.liftTernary_congr {F : Type u} [Numerics.EncodedFormat F] {Plan : Type v} {plan : Plan} {Model : Type w} [codec : ModelCodec plan Model (Numerics.FormatCode F)] {leftOperation rightOperation : Model → Model → Model → Model} (equal : ∀ (left right third : Model), leftOperation left right third = rightOperation left right third) (left right third : ExecFloat F) : liftTernary leftOperation left right third = liftTernary rightOperation left right third

Pointwise-equal ternary model operations have equal executable lifts.

@[inline]

def FloatLib.Floats.ExecFloat.denote {F : Type u} [Numerics.EncodedFormat F] [Numerics.FormatSemantics F] (value : ExecFloat F) : Numerics.NumericalValue (Numerics.FormatScalar F)

Complete semantic interpretation inherited from FormatSemantics F.

@[reducible, inline]

abbrev FloatLib.Floats.ExecFloat.Represents {F : Type u} [Numerics.EncodedFormat F] [Numerics.FormatSemantics F] (value : ExecFloat F) (scalar : Numerics.FormatScalar F) : Prop

value represents the ordinary finite scalar scalar.

@[reducible, inline]

abbrev FloatLib.Floats.ExecFloat.At {F : Type u} [Numerics.EncodedFormat F] [Numerics.FormatSemantics F] (value : Numerics.NumericalValue (Numerics.FormatScalar F)) : Type u_1

One runtime value with an erased proof of its complete denotation.

@[reducible, inline]

abbrev FloatLib.Floats.ExecFloat.AtFinite {F : Type u} [Numerics.EncodedFormat F] [Numerics.FormatSemantics F] (value : Numerics.FormatScalar F) : Type u_1

One runtime value with an erased proof of its ordinary finite denotation.

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.instInhabitedOfFormatCode {F : Type u} [Numerics.EncodedFormat F] [Inhabited (Numerics.FormatCode F)] : Inhabited (ExecFloat F)

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.instDecidableEqOfFormatCode {F : Type u} [Numerics.EncodedFormat F] [DecidableEq (Numerics.FormatCode F)] : DecidableEq (ExecFloat F)

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.instToStringOfFormatDisplay {F : Type u} [Numerics.EncodedFormat F] [FormatDisplay F] : ToString (ExecFloat F)

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.instReprOfFormatDisplay {F : Type u} [Numerics.EncodedFormat F] [FormatDisplay F] : Repr (ExecFloat F)

#eval uses a format's mathematical display when one is available.

The resulting text is emitted directly rather than represented as a quoted Lean string.

@[instance_reducible, instance 100]

instance FloatLib.Floats.ExecFloat.instReprOfFormatCode {F : Type u} [Numerics.EncodedFormat F] [Repr (Numerics.FormatCode F)] : Repr (ExecFloat F)

Low-priority structural representation for internal families without a mathematical display. Public numerical families should provide FormatDisplay.