Contracts for numerical operations

Relations between executable functions and their denotations, starting with indexed inputs and specializing to unary, binary, and ternary functions. The contracts distinguish total, finite, checked, cast, and quantizer semantics. They live in Prop and add no runtime data.

See Operation.Status for result flags, Operation.Context for rounding policies, and Operation.Entropy for explicit randomness. Operation.Proof contains application and composition lemmas.

Indexed input contracts

@[reducible, inline]

abbrev FloatLib.Numerics.Operation.InputCodes {ι : Type u} (inputs : ι → NumericalSystem) : Type (max u u_1)

Runtime inputs indexed by their numerical systems.

@[reducible, inline]

abbrev FloatLib.Numerics.Operation.InputValues {ι : Type u} (inputs : ι → NumericalSystem) : Type (max u u_2)

Complete denotations of indexed numerical inputs.

@[reducible, inline]

abbrev FloatLib.Numerics.Operation.InputScalars {ι : Type u} (inputs : ι → NumericalSystem) : Type (max u u_2)

Ordinary finite scalar values indexed by their numerical systems.

def FloatLib.Numerics.Operation.InputsRepresent {ι : Type u} (inputs : ι → NumericalSystem) (codes : InputCodes inputs) (values : InputScalars inputs) : Prop

Every indexed runtime input represents its corresponding finite scalar.

def FloatLib.Numerics.Operation.Refines {ι : Type u} (inputs : ι → NumericalSystem) {Result : Type v} (run : InputCodes inputs → Result) (post : InputValues inputs → Result → Prop) : Prop

An executable operation satisfies a relational contract over the complete denotations of all inputs.

Result is deliberately unconstrained: it may be a code, an Option, a status-bearing result, an entropy-producing computation, or a block value.

def FloatLib.Numerics.Operation.RefinesFinite {ι : Type u} (inputs : ι → NumericalSystem) {Result : Type v} (run : InputCodes inputs → Result) (post : InputScalars inputs → Result → Prop) : Prop

An executable operation satisfies a relational contract on represented finite inputs.

Unary, binary, and ternary relations

def FloatLib.Numerics.Operation.Refines1 (A : NumericalSystem) {Result : Type u} (run : A.Code → Result) (post : NumericalValue A.Scalar → Result → Prop) : Prop

A unary executable operation satisfies a relation on complete input denotations.

def FloatLib.Numerics.Operation.Refines2 (A : NumericalSystem) (B : NumericalSystem) {Result : Type u} (run : A.Code → B.Code → Result) (post : NumericalValue A.Scalar → NumericalValue B.Scalar → Result → Prop) : Prop

A two-input executable operation satisfies a relation on complete input denotations.

def FloatLib.Numerics.Operation.Refines3 (A : NumericalSystem) (B : NumericalSystem) (C : NumericalSystem) {Result : Type u} (run : A.Code → B.Code → C.Code → Result) (post : NumericalValue A.Scalar → NumericalValue B.Scalar → NumericalValue C.Scalar → Result → Prop) : Prop

A three-input executable operation satisfies a relation on complete input denotations.

def FloatLib.Numerics.Operation.RefinesFinite1 (A : NumericalSystem) {Result : Type u} (run : A.Code → Result) (post : A.Scalar → Result → Prop) : Prop

A unary executable operation satisfies a relation on represented finite inputs.

def FloatLib.Numerics.Operation.RefinesFinite2 (A : NumericalSystem) (B : NumericalSystem) {Result : Type u} (run : A.Code → B.Code → Result) (post : A.Scalar → B.Scalar → Result → Prop) : Prop

A two-input executable operation satisfies a relation on represented finite inputs.

def FloatLib.Numerics.Operation.RefinesFinite3 (A : NumericalSystem) (B : NumericalSystem) (C : NumericalSystem) {Result : Type u} (run : A.Code → B.Code → C.Code → Result) (post : A.Scalar → B.Scalar → C.Scalar → Result → Prop) : Prop

A three-input executable operation satisfies a relation on represented finite inputs.

Total, finite, checked, and quantizer semantics

def FloatLib.Numerics.Operation.Total1 (A : NumericalSystem) (B : NumericalSystem) (run : A.Code → B.Code) (spec : NumericalValue A.Scalar → NumericalValue B.Scalar) : Prop

Correctness of a unary total operation, including exceptional values.

def FloatLib.Numerics.Operation.Total2 (A : NumericalSystem) (B : NumericalSystem) (C : NumericalSystem) (run : A.Code → B.Code → C.Code) (spec : NumericalValue A.Scalar → NumericalValue B.Scalar → NumericalValue C.Scalar) : Prop

Correctness of a two-input total operation, including exceptional values.

def FloatLib.Numerics.Operation.Total3 (A : NumericalSystem) (B : NumericalSystem) (C : NumericalSystem) (D : NumericalSystem) (run : A.Code → B.Code → C.Code → D.Code) (spec : NumericalValue A.Scalar → NumericalValue B.Scalar → NumericalValue C.Scalar → NumericalValue D.Scalar) : Prop

Correctness of a three-input total operation, including exceptional values.

def FloatLib.Numerics.Operation.Finite1 (A : NumericalSystem) (B : NumericalSystem) (run : A.Code → B.Code) (spec : A.Scalar → B.Scalar) : Prop

Correctness of a unary operation on represented finite inputs.

def FloatLib.Numerics.Operation.Finite2 (A : NumericalSystem) (B : NumericalSystem) (C : NumericalSystem) (run : A.Code → B.Code → C.Code) (spec : A.Scalar → B.Scalar → C.Scalar) : Prop

Correctness of a two-input operation on represented finite inputs.

def FloatLib.Numerics.Operation.Finite3 (A : NumericalSystem) (B : NumericalSystem) (C : NumericalSystem) (D : NumericalSystem) (run : A.Code → B.Code → C.Code → D.Code) (spec : A.Scalar → B.Scalar → C.Scalar → D.Scalar) : Prop

Correctness of a three-input operation on represented finite inputs.

def FloatLib.Numerics.Operation.Finite1If (A : NumericalSystem) (B : NumericalSystem) (run : A.Code → B.Code) (spec : A.Scalar → B.Scalar) (accept : A.Code → B.Code → Prop) : Prop

Correctness of a unary operation when a predicate on the concrete input and result holds.

The predicate captures executable side conditions such as a floating-point result remaining finite. It is proof-only and does not change the direct runtime function.

def FloatLib.Numerics.Operation.Finite2If (A : NumericalSystem) (B : NumericalSystem) (C : NumericalSystem) (run : A.Code → B.Code → C.Code) (spec : A.Scalar → B.Scalar → C.Scalar) (accept : A.Code → B.Code → C.Code → Prop) : Prop

Correctness of a two-input operation when a predicate on its concrete inputs and result holds.

def FloatLib.Numerics.Operation.Finite3If (A : NumericalSystem) (B : NumericalSystem) (C : NumericalSystem) (D : NumericalSystem) (run : A.Code → B.Code → C.Code → D.Code) (spec : A.Scalar → B.Scalar → C.Scalar → D.Scalar) (accept : A.Code → B.Code → C.Code → D.Code → Prop) : Prop

Correctness of a three-input operation when a predicate on its concrete inputs and result holds.

def FloatLib.Numerics.Operation.Checked1 (A : NumericalSystem) (B : NumericalSystem) (run : A.Code → Option B.Code) (spec : A.Scalar → NumericalValue B.Scalar) : Prop

Correctness of a checked unary operation on represented finite inputs.

def FloatLib.Numerics.Operation.Checked2 (A : NumericalSystem) (B : NumericalSystem) (C : NumericalSystem) (run : A.Code → B.Code → Option C.Code) (spec : A.Scalar → B.Scalar → NumericalValue C.Scalar) : Prop

Correctness of a checked two-input operation on represented finite inputs.

def FloatLib.Numerics.Operation.Checked3 (A : NumericalSystem) (B : NumericalSystem) (C : NumericalSystem) (D : NumericalSystem) (run : A.Code → B.Code → C.Code → Option D.Code) (spec : A.Scalar → B.Scalar → C.Scalar → NumericalValue D.Scalar) : Prop

Correctness of a checked three-input operation on represented finite inputs.

def FloatLib.Numerics.Operation.Checked1On (A : NumericalSystem) (B : NumericalSystem) (run : A.Code → Option B.Code) (spec : A.Scalar → NumericalValue B.Scalar) (pre : A.Scalar → Prop) : Prop

A checked unary operation is correct whenever its scalar precondition holds.

def FloatLib.Numerics.Operation.Checked2On (A : NumericalSystem) (B : NumericalSystem) (C : NumericalSystem) (run : A.Code → B.Code → Option C.Code) (spec : A.Scalar → B.Scalar → NumericalValue C.Scalar) (pre : A.Scalar → B.Scalar → Prop) : Prop

A checked two-input operation is correct whenever its scalar precondition holds.

def FloatLib.Numerics.Operation.Checked3On (A : NumericalSystem) (B : NumericalSystem) (C : NumericalSystem) (D : NumericalSystem) (run : A.Code → B.Code → C.Code → Option D.Code) (spec : A.Scalar → B.Scalar → C.Scalar → NumericalValue D.Scalar) (pre : A.Scalar → B.Scalar → C.Scalar → Prop) : Prop

A checked three-input operation is correct whenever its scalar precondition holds.

def FloatLib.Numerics.Operation.CastFiniteOn (A : NumericalSystem) (B : NumericalSystem) (run : A.Code → B.Code) (embed : A.Scalar → B.Scalar) (pre : A.Scalar → Prop) : Prop

A conversion implements embed on every represented value accepted by pre.

def FloatLib.Numerics.Operation.QuantizerOn (S : NumericalSystem) (quantize : S.Scalar → S.Code) (round : S.Scalar → S.Scalar) (pre : S.Scalar → Prop) : Prop

A quantizer implements a named rounding map on values satisfying pre.