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, and its runtime representation is the family-chosen FormatCode F type. Only proof-side definitions need a semantic interpretation, 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 still crosses 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.35.0/src/Init/Prelude.lean#L697-L699. 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 no data. It separates types and validates nothing at runtime.

• 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 as the family-selected FormatCode F, and the proof-only tag adds 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. Because this contract sits below ExecFloat, every representation can print its mathematical value without a universal radix, an exceptional-value model or a 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. Nothing in the contract depends on radix, encoding, exceptional values or 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 returns the model value.

• 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 to the family-selected runtime code, without decoding.

@[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 to family-selected runtime codes, without decoding.

@[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 to family-selected runtime codes, without decoding.

@[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

A unary code operation that commutes with toModel is the lift of its model operation.

The executable side stays the code operation, and the model equation is used only in proofs.

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

A binary code operation that commutes with toModel is the lift of its model operation.

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

A ternary code operation that commutes with toModel is the lift of its model operation.

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 text is emitted unquoted, and is parenthesized when it is negative and appears as an argument, as in some (-1.5).

@[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.