TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.P3109.Conversion.Proof

P3109 conversion proofs #

These theorems expose the executable equations, connect conversion output to the proved round-then-saturate projection semantics, and discharge the declared quantizer contract.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.P3109.Conversion.run_eq_success {format : Formats.P3109.Format} (policy : Formats.P3109.ProjectionPolicy) (input : Numerics.NumericalValue ℚ) :
run policy input = ConversionOutcome.success (projectRat input policy.rounding policy.saturation) (status format policy input)

Every P3109 conversion is the policy-selected projection with its computed status.

source
theorem FloatLib.Floats.ExecFloat.P3109.Conversion.run_finite {format : Formats.P3109.Format} (policy : Formats.P3109.ProjectionPolicy) (exact : ℚ) :
run policy (Numerics.NumericalValue.finite exact) = ConversionOutcome.success (ofRat exact policy.rounding policy.saturation) (status format policy (Numerics.NumericalValue.finite exact))

Finite conversion goes through the exact rational projection ofRat.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.P3109.Conversion.run_infinity {format : Formats.P3109.Format} (policy : Formats.P3109.ProjectionPolicy) (negative : Bool) :
run policy (Numerics.NumericalValue.infinity negative) = ConversionOutcome.success (projectRat (Numerics.NumericalValue.infinity negative) policy.rounding policy.saturation) (status format policy (Numerics.NumericalValue.infinity negative))

Converting an infinity follows the P3109 projection policy.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.P3109.Conversion.run_exceptional {format : Formats.P3109.Format} (policy : Formats.P3109.ProjectionPolicy) (exceptional : Numerics.ExceptionalValue) :
run policy (Numerics.NumericalValue.exceptional exceptional) = ConversionOutcome.success (projectRat (Numerics.NumericalValue.exceptional exceptional) policy.rounding policy.saturation) (status format policy (Numerics.NumericalValue.exceptional exceptional))

Converting an exceptional value follows the P3109 projection policy.

source
theorem FloatLib.Floats.ExecFloat.P3109.Conversion.sameDatum_decode_run_value {format : Formats.P3109.Format} (policy : Formats.P3109.ProjectionPolicy) (input : Numerics.NumericalValue ℚ) :
Formats.P3109.Format.SameDatum (projectRat input policy.rounding policy.saturation).decode (format.projectRatValue policy input)

Decoding a conversion result yields the proved P3109 round-then-saturate datum.

source
theorem FloatLib.Floats.ExecFloat.P3109.Conversion.implements_run {format : Formats.P3109.Format} :
spec.Implements run

run meets the quantizer contract spec: word, status, and decoded datum.

source
theorem FloatLib.Floats.ExecFloat.P3109.Conversion.spec_iff_eq_run {format : Formats.P3109.Format} (policy : Formats.P3109.ProjectionPolicy) (input : Numerics.NumericalValue ℚ) (outcome : ConversionOutcome (P3109 format)) :
spec policy input outcome ↔ outcome = run policy input

An outcome meets spec exactly when it is the outcome of run, status included.

source
theorem FloatLib.Floats.ExecFloat.P3109.Conversion.sameDatum_of_spec {format : Formats.P3109.Format} (policy : Formats.P3109.ProjectionPolicy) (input : Numerics.NumericalValue ℚ) (value : P3109 format) (indicators : ConversionStatus) (h : spec policy input (ConversionOutcome.success value indicators)) :
Formats.P3109.Format.SameDatum value.decode (format.projectRatValue policy input)

Any successful outcome admitted by the contract denotes the policy-selected datum.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.P3109.Conversion.exactDecoder_run {format : Formats.P3109.Format} (value : P3109 format) :
ExactDecoder.run value = decodeRat value

The installed P3109 exact decoder is decodeRat.