module Std.Numeric.Profile import Std.Natural import Data.Bytes import Model.Word64 -- Numeric profiles as Alpha VALUES, one owner (Language & Testing Evolution -- L13b; PRD 17 H2/H3, HW-005; PRD 08 N6). A profile declares what a float -- realization may assume: storage and accumulation formats, rounding, -- contraction, reduction order, subnormal handling, exceptional values and a -- per-operation approximation table. The two initial profiles are values in -- this module; docs/language/numeric-profiles/.md is the prose each value -- is rendered against (debug/std-numeric-profile-check.py renders the values -- into docs/generated/ALPHA-NUMERIC-PROFILES.md from this module, never by hand). -- Nothing here is measured: a bound that has not been measured says so by -- name (StdApproximationUnmeasured), an operation a profile does not realize -- says so by name (StdApproximationUnsupported) -- a profile may narrow, it may -- never claim more than its lowering delivers. -- the identity a receipt carries for the profile family StdNumericProfileIdentity : Type 0 constructor StdProfileIdentityX86SseScalarStrict constructor StdProfileIdentitySm86CooperativeM0 constructor StdProfileIdentityNamed field unrestricted stdProfileIdentityName : Bytes end-family family StdNumericFormat : Type 0 constructor StdFormatBinary32 constructor StdFormatBinary64 end-family -- only round-to-nearest-even is admitted; the family has one constructor so -- that a profile cannot declare another rounding by mistake family StdRounding : Type 0 constructor StdRoundNearestEven end-family family StdContraction : Type 0 constructor StdContractionForbidden constructor StdContractionPermittedWhereEmitted end-family family StdReductionOrder : Type 0 constructor StdReductionStrictLeftFold constructor StdReductionDeclaredTree end-family -- SM86 flush-to-zero is a MEASURED fact (a pod probe, L26), never assumed family StdSubnormalHandling : Type 0 constructor StdSubnormalsPreserved constructor StdSubnormalsFlushedToZero constructor StdSubnormalsUnmeasured end-family -- IEEE exceptional values: NaN propagates quieted, invalid operations give the -- target's default NaN, signed infinities and zeros; exceptions masked and never -- read back (the profile document spells the rules out) family StdExceptionalValues : Type 0 constructor StdExceptionalIEEE -- Every arithmetic input/output is finite, or execution refuses by name. constructor StdExceptionalFiniteOrRefuse end-family family StdNumericOperation : Type 0 constructor StdOpAdd constructor StdOpSubtract constructor StdOpMultiply constructor StdOpDivide constructor StdOpSquareRoot constructor StdOpReciprocal constructor StdOpReciprocalSquareRoot constructor StdOpExp2 constructor StdOpTanh end-family -- a per-operation bound: exact = correctly rounded (at most half an ulp); -- a measured maximum ulp error; unmeasured (no bound may be relied on); -- unsupported (the profile does not realize the operation) family StdApproximation : Type 0 constructor StdApproximationExact constructor StdApproximationMaxUlp field unrestricted stdApproximationUlp : Nat constructor StdApproximationUnmeasured constructor StdApproximationUnsupported end-family family StdApproximationEntry : Type 0 constructor StdApproximationEntryOf field unrestricted stdApproximationEntryOperation : (family StdNumericOperation) field unrestricted stdApproximationEntryBound : (family StdApproximation) end-family family StdApproximationTable : Type 0 constructor StdApproximationTableEmpty constructor StdApproximationTableCons field unrestricted stdApproximationTableHead : (family StdApproximationEntry) recursive unrestricted stdApproximationTableRest end-family family StdNumericProfile : Type 0 constructor StdNumericProfileOf field unrestricted stdNumericProfileIdentity : (family StdNumericProfileIdentity) field unrestricted stdNumericProfileStorage : (family StdNumericFormat) field unrestricted stdNumericProfileAccumulation : (family StdNumericFormat) field unrestricted stdNumericProfileRounding : (family StdRounding) field unrestricted stdNumericProfileContraction : (family StdContraction) field unrestricted stdNumericProfileReductionOrder : (family StdReductionOrder) field unrestricted stdNumericProfileSubnormals : (family StdSubnormalHandling) field unrestricted stdNumericProfileExceptional : (family StdExceptionalValues) field unrestricted stdNumericProfileApproximations : (family StdApproximationTable) end-family -- H3: how a float case compares its observed value with the expected one; the -- runner refuses a float case that declares none. abs and rel are binary32 bit -- patterns (a Nat below 2^32), ulp a count. family StdNanPolicy : Type 0 constructor StdNanNeverEqual constructor StdNanEqualByBits end-family family StdZeroPolicy : Type 0 constructor StdZerosEqual constructor StdZerosDistinct end-family -- an aggregation that could hide a failure (a mean) is not a constructor family StdErrorAggregation : Type 0 constructor StdAggregateEveryCase constructor StdAggregateMaximum end-family family StdTolerance : Type 0 constructor StdToleranceOf field unrestricted stdToleranceAbsoluteBits : Nat field unrestricted stdToleranceRelativeBits : Nat field unrestricted stdToleranceUlp : Nat field unrestricted stdToleranceNanPolicy : (family StdNanPolicy) field unrestricted stdToleranceZeroPolicy : (family StdZeroPolicy) field unrestricted stdToleranceAggregation : (family StdErrorAggregation) end-family family StdNumericComparison : Type 0 constructor StdCompareExactBits constructor StdCompareExactValue constructor StdCompareTolerance field unrestricted stdCompareTolerance : (family StdTolerance) end-family -- PRD 17 HW-004 / REG-019: whether a profile ADMITS a requested variant. A -- rejection names the capability that is missing (the device, the precision or -- the operation) with its diagnostic code; `alpha check` and `alpha build` -- refuse a root whose `admission` is rejected before anything is emitted. family StdNumericAdmission : Type 0 constructor StdAdmissionAdmitted constructor StdAdmissionRejected field unrestricted stdAdmissionRejectedCode : Bytes field unrestricted stdAdmissionRejectedReason : Bytes end-family -- Conversion is an operation in the numerical program. These constructors -- fix both endpoints; an absent conversion cannot authorize a format change. -- Widening preserves finite binary32 values exactly. Narrowing is an explicit -- nearest-even rounding site, including overflow and subnormal outcomes; it is -- never inferred from a transport or admitted as an exact widening. family StdNumericConversion : Type 0 constructor StdNumericKeepFormat field unrestricted stdNumericKeptFormat : (family StdNumericFormat) constructor StdNumericWidenBinary32 constructor StdNumericRoundBinary64 end-family -- operations as small codes, so two operations can be compared def stdOperationCode = (lambda unrestricted operation : (family StdNumericOperation) . (eliminate StdNumericOperation (lambda unrestricted current : (family StdNumericOperation) . Nat) operation (branch StdOpAdd . (byte-to-nat (byte 1))) (branch StdOpSubtract . (byte-to-nat (byte 2))) (branch StdOpMultiply . (byte-to-nat (byte 3))) (branch StdOpDivide . (byte-to-nat (byte 4))) (branch StdOpSquareRoot . (byte-to-nat (byte 5))) (branch StdOpReciprocal . (byte-to-nat (byte 6))) (branch StdOpReciprocalSquareRoot . (byte-to-nat (byte 7))) (branch StdOpExp2 . (byte-to-nat (byte 8))) (branch StdOpTanh . (byte-to-nat (byte 9))))) def stdOperationEqual = (lambda unrestricted a : (family StdNumericOperation) . (lambda unrestricted b : (family StdNumericOperation) . (naturalEqual (stdOperationCode a) (stdOperationCode b)))) def stdSelectApproximation = (lambda unrestricted flag : Nat . (lambda unrestricted whenTrue : (family StdApproximation) . (lambda unrestricted whenFalse : (family StdApproximation) . (nat-eliminate (lambda unrestricted current : Nat . (family StdApproximation)) whenFalse (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family StdApproximation) . whenTrue)) flag)))) -- the bound a table declares for an operation; an operation the table does not -- name is Unsupported (never silently exact) def stdApproximationOf = (lambda unrestricted operation : (family StdNumericOperation) . (lambda unrestricted table : (family StdApproximationTable) . (eliminate StdApproximationTable (lambda unrestricted current : (family StdApproximationTable) . (family StdApproximation)) table (branch StdApproximationTableEmpty . (constructor StdApproximation StdApproximationUnsupported)) (branch StdApproximationTableCons entry rest restBound . (eliminate StdApproximationEntry (lambda unrestricted current : (family StdApproximationEntry) . (family StdApproximation)) entry (branch StdApproximationEntryOf entryOperation entryBound . (stdSelectApproximation (stdOperationEqual entryOperation operation) entryBound restBound))))))) def stdApproximationIsExact = (lambda unrestricted bound : (family StdApproximation) . (eliminate StdApproximation (lambda unrestricted current : (family StdApproximation) . Nat) bound (branch StdApproximationExact . (succ zero)) (branch StdApproximationMaxUlp ulp . zero) (branch StdApproximationUnmeasured . zero) (branch StdApproximationUnsupported . zero))) -- projections def stdNumericProfileTable = (lambda unrestricted profile : (family StdNumericProfile) . (eliminate StdNumericProfile (lambda unrestricted current : (family StdNumericProfile) . (family StdApproximationTable)) profile (branch StdNumericProfileOf identity storage accumulation rounding contraction order subnormals exceptional table . table))) def stdNumericProfileContractionOf = (lambda unrestricted profile : (family StdNumericProfile) . (eliminate StdNumericProfile (lambda unrestricted current : (family StdNumericProfile) . (family StdContraction)) profile (branch StdNumericProfileOf identity storage accumulation rounding contraction order subnormals exceptional table . contraction))) def stdNumericProfileSubnormalsOf = (lambda unrestricted profile : (family StdNumericProfile) . (eliminate StdNumericProfile (lambda unrestricted current : (family StdNumericProfile) . (family StdSubnormalHandling)) profile (branch StdNumericProfileOf identity storage accumulation rounding contraction order subnormals exceptional table . subnormals))) def stdNumericProfileReductionOrderOf = (lambda unrestricted profile : (family StdNumericProfile) . (eliminate StdNumericProfile (lambda unrestricted current : (family StdNumericProfile) . (family StdReductionOrder)) profile (branch StdNumericProfileOf identity storage accumulation rounding contraction order subnormals exceptional table . order))) def stdNumericProfileIdentityOf = (lambda unrestricted profile : (family StdNumericProfile) . (eliminate StdNumericProfile (lambda unrestricted current : (family StdNumericProfile) . (family StdNumericProfileIdentity)) profile (branch StdNumericProfileOf identity storage accumulation rounding contraction order subnormals exceptional table . identity))) -- is the operation exact (correctly rounded) under the profile? def stdProfileExact = (lambda unrestricted profile : (family StdNumericProfile) . (lambda unrestricted operation : (family StdNumericOperation) . (stdApproximationIsExact (stdApproximationOf operation (stdNumericProfileTable profile))))) -- the common subset of two profiles (PRD 19: the cross-target gate of System A): -- an operation both realize exactly def stdProfilesBothExact = (lambda unrestricted a : (family StdNumericProfile) . (lambda unrestricted b : (family StdNumericProfile) . (lambda unrestricted operation : (family StdNumericOperation) . (nat-eliminate (lambda unrestricted current : Nat . Nat) zero (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . (stdProfileExact b operation))) (stdProfileExact a operation))))) def stdNumericFormatCode = (lambda unrestricted format : (family StdNumericFormat) . (eliminate StdNumericFormat (lambda unrestricted current : (family StdNumericFormat) . Nat) format (branch StdFormatBinary32 . (succ zero)) (branch StdFormatBinary64 . (succ (succ zero))))) -- This is a constructor tag, not identity equality for named profiles. def stdNumericProfileIdentityCode = (lambda unrestricted identity : (family StdNumericProfileIdentity) . (eliminate StdNumericProfileIdentity (lambda unrestricted current : (family StdNumericProfileIdentity) . Nat) identity (branch StdProfileIdentityX86SseScalarStrict . (succ zero)) (branch StdProfileIdentitySm86CooperativeM0 . (succ (succ zero))) (branch StdProfileIdentityNamed name . 3))) def stdNumericProfileStorageOf = (lambda unrestricted profile : (family StdNumericProfile) . (eliminate StdNumericProfile (lambda unrestricted current : (family StdNumericProfile) . (family StdNumericFormat)) profile (branch StdNumericProfileOf identity storage accumulation rounding contraction order subnormals exceptional table . storage))) def stdApproximationIsUnsupported = (lambda unrestricted bound : (family StdApproximation) . (eliminate StdApproximation (lambda unrestricted current : (family StdApproximation) . Nat) bound (branch StdApproximationExact . zero) (branch StdApproximationMaxUlp ulp . zero) (branch StdApproximationUnmeasured . zero) (branch StdApproximationUnsupported . (succ zero)))) def stdAdmissionWhen = (lambda unrestricted flag : Nat . (lambda unrestricted whenTrue : (family StdNumericAdmission) . (lambda unrestricted whenFalse : (family StdNumericAdmission) . (nat-eliminate (lambda unrestricted current : Nat . (family StdNumericAdmission)) whenFalse (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family StdNumericAdmission) . whenTrue)) flag)))) def stdAdmitted : (family StdNumericAdmission) = (constructor StdNumericAdmission StdAdmissionAdmitted) -- does the profile admit an operation at a precision? The precision must be the -- profile's storage format, and the operation must not be Unsupported in its -- table (an Unmeasured bound is admitted: it is realized, only not yet measured) def stdProfileAdmits = (lambda unrestricted profile : (family StdNumericProfile) . (lambda unrestricted format : (family StdNumericFormat) . (lambda unrestricted operation : (family StdNumericOperation) . (stdAdmissionWhen (naturalEqual (stdNumericFormatCode format) (stdNumericFormatCode (stdNumericProfileStorageOf profile))) (stdAdmissionWhen (stdApproximationIsUnsupported (stdApproximationOf operation (stdNumericProfileTable profile))) (constructor StdNumericAdmission StdAdmissionRejected b"ALPHA-ADMISSION-UNSUPPORTED-OPERATION" b"the profile declares the requested operation unsupported") stdAdmitted) (constructor StdNumericAdmission StdAdmissionRejected b"ALPHA-ADMISSION-UNSUPPORTED-PRECISION" b"the requested precision is not the profile's storage format"))))) -- A semantic profile name is extensible; a device package supplies a name and -- its actual behavior record. Distinct names never compare equal merely because -- both use the extension constructor. Version changes must change the name. def stdNumericWord = (lambda unrestricted value : Nat . (dataBytesWord64LE (modelWord64FromNaturalTruncated value))) def stdNumericSizedBytes = (lambda unrestricted value : Bytes . (bytes-append (stdNumericWord (bytes-length value)) value)) def stdNumericProfileIdentityBytes = (lambda unrestricted identity : (family StdNumericProfileIdentity) . (eliminate StdNumericProfileIdentity (lambda unrestricted current : (family StdNumericProfileIdentity) . Bytes) identity (branch StdProfileIdentityX86SseScalarStrict . b"\x01") (branch StdProfileIdentitySm86CooperativeM0 . b"\x02") (branch StdProfileIdentityNamed name . (bytes-append b"\x03" (stdNumericSizedBytes name))))) -- the same on a device: a profile of another device is rejected first def stdProfileAdmitsOn = (lambda unrestricted device : (family StdNumericProfileIdentity) . (lambda unrestricted profile : (family StdNumericProfile) . (lambda unrestricted format : (family StdNumericFormat) . (lambda unrestricted operation : (family StdNumericOperation) . (stdAdmissionWhen (bytes-equal (stdNumericProfileIdentityBytes device) (stdNumericProfileIdentityBytes (stdNumericProfileIdentityOf profile))) (stdProfileAdmits profile format operation) (constructor StdNumericAdmission StdAdmissionRejected b"ALPHA-ADMISSION-UNSUPPORTED-DEVICE" b"the profile belongs to another device than the one requested")))))) def stdEntry = (lambda unrestricted operation : (family StdNumericOperation) . (lambda unrestricted bound : (family StdApproximation) . (constructor StdApproximationEntry StdApproximationEntryOf operation bound))) def stdTableCons = (lambda unrestricted entry : (family StdApproximationEntry) . (lambda unrestricted rest : (family StdApproximationTable) . (constructor StdApproximationTable StdApproximationTableCons entry rest))) def stdExact : (family StdApproximation) = (constructor StdApproximation StdApproximationExact) def stdUnmeasured : (family StdApproximation) = (constructor StdApproximation StdApproximationUnmeasured) def stdUnsupported : (family StdApproximation) = (constructor StdApproximation StdApproximationUnsupported) def stdOpAdd : (family StdNumericOperation) = (constructor StdNumericOperation StdOpAdd) def stdOpSubtract : (family StdNumericOperation) = (constructor StdNumericOperation StdOpSubtract) def stdOpMultiply : (family StdNumericOperation) = (constructor StdNumericOperation StdOpMultiply) def stdOpDivide : (family StdNumericOperation) = (constructor StdNumericOperation StdOpDivide) def stdOpSquareRoot : (family StdNumericOperation) = (constructor StdNumericOperation StdOpSquareRoot) def stdOpReciprocal : (family StdNumericOperation) = (constructor StdNumericOperation StdOpReciprocal) def stdOpReciprocalSquareRoot : (family StdNumericOperation) = (constructor StdNumericOperation StdOpReciprocalSquareRoot) def stdOpExp2 : (family StdNumericOperation) = (constructor StdNumericOperation StdOpExp2) def stdOpTanh : (family StdNumericOperation) = (constructor StdNumericOperation StdOpTanh) def stdTableEmpty : (family StdApproximationTable) = (constructor StdApproximationTable StdApproximationTableEmpty) -- x86-64-sse-scalar-strict (PRD 08 N6): SSE scalar single precision, round to -- nearest even, no contraction, strict left-fold order, subnormals preserved -- (MXCSR FTZ/DAZ clear, asserted at entry), IEEE exceptional values with the -- x86 default NaN. add/subtract/multiply/divide are exact (correctly rounded -- by the hardware); the correctly-rounded square root is the declared -- extension AdamW needs and is NOT realized at HEAD (Unsupported until its -- lowering lands -- the value may narrow, never overstate); the MUFU-style -- operations have no x86 realization. def stdProfileX86SseScalarStrict : (family StdNumericProfile) = (constructor StdNumericProfile StdNumericProfileOf (constructor StdNumericProfileIdentity StdProfileIdentityX86SseScalarStrict) (constructor StdNumericFormat StdFormatBinary32) (constructor StdNumericFormat StdFormatBinary32) (constructor StdRounding StdRoundNearestEven) (constructor StdContraction StdContractionForbidden) (constructor StdReductionOrder StdReductionStrictLeftFold) (constructor StdSubnormalHandling StdSubnormalsPreserved) (constructor StdExceptionalValues StdExceptionalIEEE) (stdTableCons (stdEntry stdOpAdd stdExact) (stdTableCons (stdEntry stdOpSubtract stdExact) (stdTableCons (stdEntry stdOpMultiply stdExact) (stdTableCons (stdEntry stdOpDivide stdExact) (stdTableCons (stdEntry stdOpSquareRoot stdUnsupported) (stdTableCons (stdEntry stdOpReciprocal stdUnsupported) (stdTableCons (stdEntry stdOpReciprocalSquareRoot stdUnsupported) (stdTableCons (stdEntry stdOpExp2 stdUnsupported) (stdTableCons (stdEntry stdOpTanh stdUnsupported) stdTableEmpty)))))))))) -- sm86-cooperative-m0: the profile the D-ladder actually ran. FFMA contraction -- is permitted where the lowering emits it; the reduction order is the -- D-ladder's declared tree; flush-to-zero and every MUFU bound are MEASURED -- facts (PRD 17 H2) and are Unmeasured until the L26 pod probe records them. -- add/subtract/multiply as emitted (FADD/FMUL, or the fused FFMA's own -- rounding) are exact; division on SM86 goes through a reciprocal -- approximation and is Unmeasured, not assumed exact. def stdProfileSm86CooperativeM0 : (family StdNumericProfile) = (constructor StdNumericProfile StdNumericProfileOf (constructor StdNumericProfileIdentity StdProfileIdentitySm86CooperativeM0) (constructor StdNumericFormat StdFormatBinary32) (constructor StdNumericFormat StdFormatBinary32) (constructor StdRounding StdRoundNearestEven) (constructor StdContraction StdContractionPermittedWhereEmitted) (constructor StdReductionOrder StdReductionDeclaredTree) (constructor StdSubnormalHandling StdSubnormalsUnmeasured) (constructor StdExceptionalValues StdExceptionalIEEE) (stdTableCons (stdEntry stdOpAdd stdExact) (stdTableCons (stdEntry stdOpSubtract stdExact) (stdTableCons (stdEntry stdOpMultiply stdExact) (stdTableCons (stdEntry stdOpDivide stdUnmeasured) (stdTableCons (stdEntry stdOpSquareRoot stdUnmeasured) (stdTableCons (stdEntry stdOpReciprocal stdUnmeasured) (stdTableCons (stdEntry stdOpReciprocalSquareRoot stdUnmeasured) (stdTableCons (stdEntry stdOpExp2 stdUnmeasured) (stdTableCons (stdEntry stdOpTanh stdUnmeasured) stdTableEmpty)))))))))) -- the comparison every bit-exact float case declares (KAT rows, the model) def stdCompareExactBits : (family StdNumericComparison) = (constructor StdNumericComparison StdCompareExactBits) def stdCompareExactValue : (family StdNumericComparison) = (constructor StdNumericComparison StdCompareExactValue) def stdNumericProfileAccumulationOf = (lambda unrestricted profile : (family StdNumericProfile) . (eliminate StdNumericProfile (lambda unrestricted current : (family StdNumericProfile) . (family StdNumericFormat)) profile (branch StdNumericProfileOf identity storage accumulation rounding contraction order subnormals exceptional table . accumulation))) def stdNumericProfileRoundingOf = (lambda unrestricted profile : (family StdNumericProfile) . (eliminate StdNumericProfile (lambda unrestricted current : (family StdNumericProfile) . (family StdRounding)) profile (branch StdNumericProfileOf identity storage accumulation rounding contraction order subnormals exceptional table . rounding))) def stdNumericProfileExceptionalOf = (lambda unrestricted profile : (family StdNumericProfile) . (eliminate StdNumericProfile (lambda unrestricted current : (family StdNumericProfile) . (family StdExceptionalValues)) profile (branch StdNumericProfileOf identity storage accumulation rounding contraction order subnormals exceptional table . exceptional))) def stdNumericConversionSource = (lambda unrestricted conversion : (family StdNumericConversion) . (eliminate StdNumericConversion (lambda unrestricted current : (family StdNumericConversion) . (family StdNumericFormat)) conversion (branch StdNumericKeepFormat format . format) (branch StdNumericWidenBinary32 . (constructor StdNumericFormat StdFormatBinary32)) (branch StdNumericRoundBinary64 . (constructor StdNumericFormat StdFormatBinary64)))) def stdNumericConversionDestination = (lambda unrestricted conversion : (family StdNumericConversion) . (eliminate StdNumericConversion (lambda unrestricted current : (family StdNumericConversion) . (family StdNumericFormat)) conversion (branch StdNumericKeepFormat format . format) (branch StdNumericWidenBinary32 . (constructor StdNumericFormat StdFormatBinary64)) (branch StdNumericRoundBinary64 . (constructor StdNumericFormat StdFormatBinary32)))) def stdNumericConversionCode = (lambda unrestricted conversion : (family StdNumericConversion) . (eliminate StdNumericConversion (lambda unrestricted current : (family StdNumericConversion) . Nat) conversion (branch StdNumericKeepFormat format . 0) (branch StdNumericWidenBinary32 . 1) (branch StdNumericRoundBinary64 . 2)))