Status-bearing numerical operation contracts

Status-bearing operations differ in their concrete result structures: IEEE arithmetic returns exception flags, checked integer operations may report overflow, and quantizers may report saturation. These contracts express correctness in terms of result and status projections, without imposing a common runtime wrapper.

def FloatLib.Numerics.Operation.RefinesStatus1 (A : NumericalSystem) (B : NumericalSystem) {Outcome : Type u} {Status : Type v} (run : A.Code → Outcome) (value : Outcome → B.Code) (status : Outcome → Status) (post : NumericalValue A.Scalar → NumericalValue B.Scalar → Status → Prop) : Prop

Complete semantics of a unary operation whose concrete result carries a code and status.

def FloatLib.Numerics.Operation.RefinesStatus2 (A : NumericalSystem) (B : NumericalSystem) (C : NumericalSystem) {Outcome : Type u} {Status : Type v} (run : A.Code → B.Code → Outcome) (value : Outcome → C.Code) (status : Outcome → Status) (post : NumericalValue A.Scalar → NumericalValue B.Scalar → NumericalValue C.Scalar → Status → Prop) : Prop

Complete semantics of a two-input operation whose result carries a code and status.

def FloatLib.Numerics.Operation.RefinesStatus3 (A : NumericalSystem) (B : NumericalSystem) (C : NumericalSystem) (D : NumericalSystem) {Outcome : Type u} {Status : Type v} (run : A.Code → B.Code → C.Code → Outcome) (value : Outcome → D.Code) (status : Outcome → Status) (post : NumericalValue A.Scalar → NumericalValue B.Scalar → NumericalValue C.Scalar → NumericalValue D.Scalar → Status → Prop) : Prop

Complete semantics of a three-input operation whose result carries a code and status.

def FloatLib.Numerics.Operation.RefinesStatusFinite1 (A : NumericalSystem) (B : NumericalSystem) {Outcome : Type u} {Status : Type v} (run : A.Code → Outcome) (value : Outcome → B.Code) (status : Outcome → Status) (post : A.Scalar → B.Scalar → Status → Prop) : Prop

Finite semantics of a unary status-bearing operation.

def FloatLib.Numerics.Operation.RefinesStatusFinite2 (A : NumericalSystem) (B : NumericalSystem) (C : NumericalSystem) {Outcome : Type u} {Status : Type v} (run : A.Code → B.Code → Outcome) (value : Outcome → C.Code) (status : Outcome → Status) (post : A.Scalar → B.Scalar → C.Scalar → Status → Prop) : Prop

Finite semantics of a two-input status-bearing operation.

def FloatLib.Numerics.Operation.RefinesStatusFinite3 (A : NumericalSystem) (B : NumericalSystem) (C : NumericalSystem) (D : NumericalSystem) {Outcome : Type u} {Status : Type v} (run : A.Code → B.Code → C.Code → Outcome) (value : Outcome → D.Code) (status : Outcome → Status) (post : A.Scalar → B.Scalar → C.Scalar → D.Scalar → Status → Prop) : Prop

Finite semantics of a three-input status-bearing operation.