module Learning.Numerics import Std.Numeric.Profile import Std.Foundation import Std.List import Std.Natural import Data.Bytes import Data.SHA256 import Data.SHA256Digest import Data.SHA256Padding import Model.Word64 -- A tolerance request is not evidence that a lowering meets it. Exact-order, -- bounded per-tensor difference, and an approximate state transition are -- distinct semantic choices. The latter two require their own conformance -- evidence before this planner can admit execution. family NumericalRelation : Type 0 constructor NumericalExactOrder field unrestricted numericalOrderIdentity : Bytes constructor NumericalBoundedDifference field unrestricted numericalReferenceIdentity : Bytes field unrestricted numericalNormIdentity : Bytes field unrestricted numericalTensorSetIdentity : Bytes field unrestricted numericalDifferenceTolerance : (family StdTolerance) constructor NumericalApproximateTransition field unrestricted numericalTransitionIdentity : Bytes field unrestricted numericalPersistentStateSchema : Bytes end-family family NumericalContract : Type 0 constructor NumericalContractOf field unrestricted numericalProfile : (family StdNumericProfile) field unrestricted numericalOperations : (family StdList (family StdNumericOperation)) field unrestricted numericalRelation : (family NumericalRelation) end-family family NumericalFailure : Type 0 constructor NumericalEmptyIdentity constructor NumericalUnknownSubnormals constructor NumericalUnspecifiedContraction constructor NumericalUnsupportedOperation constructor NumericalInexactOperation constructor NumericalProfileMismatch constructor NumericalOrderMismatch constructor NumericalBoundEvidenceRequired constructor NumericalTransitionEvidenceRequired constructor NumericalMissingConversion constructor NumericalConversionSourceMismatch constructor NumericalConversionDestinationMismatch end-family def numericalRequire = (lambda erased value : Type 0 . (lambda unrestricted condition : Nat . (lambda unrestricted reason : (family NumericalFailure) . (lambda unrestricted next : (family StdResult (family NumericalFailure) value) . (nat-eliminate (lambda unrestricted flag : Nat . (family StdResult (family NumericalFailure) value)) (constructor StdResult StdFailure (family NumericalFailure) value reason) (lambda unrestricted prior : Nat . (lambda unrestricted ignored : (family StdResult (family NumericalFailure) value) . next)) condition))))) def numericalAccepted = (constructor StdResult StdSuccess (family NumericalFailure) Nat 1) def numericalProfileOf = (lambda unrestricted contract : (family NumericalContract) . (eliminate NumericalContract (lambda unrestricted current : (family NumericalContract) . (family StdNumericProfile)) contract (branch NumericalContractOf profile operations relation . profile))) def numericalOperationsOf = (lambda unrestricted contract : (family NumericalContract) . (eliminate NumericalContract (lambda unrestricted current : (family NumericalContract) . (family StdList (family StdNumericOperation))) contract (branch NumericalContractOf profile operations relation . operations))) def numericalRelationOf = (lambda unrestricted contract : (family NumericalContract) . (eliminate NumericalContract (lambda unrestricted current : (family NumericalContract) . (family NumericalRelation)) contract (branch NumericalContractOf profile operations relation . relation))) def numericalContractionCode = (lambda unrestricted value : (family StdContraction) . (eliminate StdContraction (lambda unrestricted current : (family StdContraction) . Nat) value (branch StdContractionForbidden . 0) (branch StdContractionPermittedWhereEmitted . 1))) def numericalReductionCode = (lambda unrestricted value : (family StdReductionOrder) . (eliminate StdReductionOrder (lambda unrestricted current : (family StdReductionOrder) . Nat) value (branch StdReductionStrictLeftFold . 0) (branch StdReductionDeclaredTree . 1))) def numericalSubnormalCode = (lambda unrestricted value : (family StdSubnormalHandling) . (eliminate StdSubnormalHandling (lambda unrestricted current : (family StdSubnormalHandling) . Nat) value (branch StdSubnormalsPreserved . 0) (branch StdSubnormalsFlushedToZero . 1) (branch StdSubnormalsUnmeasured . 2))) def numericalRoundingCode = (lambda unrestricted value : (family StdRounding) . (eliminate StdRounding (lambda unrestricted current : (family StdRounding) . Nat) value (branch StdRoundNearestEven . 0))) def numericalExceptionalCode = (lambda unrestricted value : (family StdExceptionalValues) . (eliminate StdExceptionalValues (lambda unrestricted current : (family StdExceptionalValues) . Nat) value (branch StdExceptionalIEEE . 0) (branch StdExceptionalFiniteOrRefuse . 1))) -- Profile identity remains part of exact compatibility: the legacy IEEE -- exceptional policy does not specify target-independent NaN payload/default -- bits. Different targets need a shared qualified profile, or stronger explicit -- conformance evidence; matching operation names alone is insufficient. def numericalProfileBytes = (lambda unrestricted profile : (family StdNumericProfile) . (bytes-append (stdNumericProfileIdentityBytes (stdNumericProfileIdentityOf profile)) (bytes-append (stdNumericWord (stdNumericFormatCode (stdNumericProfileStorageOf profile))) (bytes-append (stdNumericWord (stdNumericFormatCode (stdNumericProfileAccumulationOf profile))) (bytes-append (stdNumericWord (numericalRoundingCode (stdNumericProfileRoundingOf profile))) (bytes-append (stdNumericWord (numericalContractionCode (stdNumericProfileContractionOf profile))) (bytes-append (stdNumericWord (numericalReductionCode (stdNumericProfileReductionOrderOf profile))) (bytes-append (stdNumericWord (numericalSubnormalCode (stdNumericProfileSubnormalsOf profile))) (bytes-append (stdNumericWord (numericalExceptionalCode (stdNumericProfileExceptionalOf profile))) b""))))))))) def numericalOperationBytes = (lambda unrestricted operations : (family StdList (family StdNumericOperation)) . (bytes-append (stdNumericWord (stdListLength (family StdNumericOperation) operations)) (eliminate StdList (lambda unrestricted current : (family StdList (family StdNumericOperation)) . Bytes) operations (branch StdListEmpty . b"") (branch StdListCons head tail induction . (bytes-append (stdNumericWord (stdOperationCode head)) induction))))) def numericalExactOrderBytes = (lambda unrestricted relation : (family NumericalRelation) . (eliminate NumericalRelation (lambda unrestricted current : (family NumericalRelation) . Bytes) relation (branch NumericalExactOrder identity . identity) (branch NumericalBoundedDifference reference norm tensors tolerance . b"") (branch NumericalApproximateTransition transition schema . b""))) -- Only an admitted exact contract is currently encoded for executable identity. -- Non-exact requests refuse before emission; no empty hash is a valid identity. def numericalExactContractBytes = (lambda unrestricted contract : (family NumericalContract) . (bytes-append b"alpha-numerical-exact-v1" (bytes-append (stdNumericSizedBytes (numericalProfileBytes (numericalProfileOf contract))) (bytes-append (numericalOperationBytes (numericalOperationsOf contract)) (stdNumericSizedBytes (numericalExactOrderBytes (numericalRelationOf contract))))))) def numericalExactContractDigest = (lambda unrestricted contract : (family NumericalContract) . (sha256RawDigestOrEmpty (numericalExactContractBytes contract))) def numericalIdentityPresent = (lambda unrestricted identity : (family StdNumericProfileIdentity) . (eliminate StdNumericProfileIdentity (lambda unrestricted current : (family StdNumericProfileIdentity) . Nat) identity (branch StdProfileIdentityX86SseScalarStrict . 1) (branch StdProfileIdentitySm86CooperativeM0 . 1) (branch StdProfileIdentityNamed name . (naturalNonzero (bytes-length name))))) def numericalCheckOperations = (lambda unrestricted profile : (family StdNumericProfile) . (lambda unrestricted operations : (family StdList (family StdNumericOperation)) . (eliminate StdList (lambda unrestricted current : (family StdList (family StdNumericOperation)) . (family StdResult (family NumericalFailure) Nat)) operations (branch StdListEmpty . numericalAccepted) (branch StdListCons head tail induction . (eliminate StdApproximation (lambda unrestricted current : (family StdApproximation) . (family StdResult (family NumericalFailure) Nat)) (stdApproximationOf head (stdNumericProfileTable profile)) (branch StdApproximationExact . induction) (branch StdApproximationMaxUlp ulp . (constructor StdResult StdFailure (family NumericalFailure) Nat (constructor NumericalFailure NumericalInexactOperation))) (branch StdApproximationUnmeasured . (constructor StdResult StdFailure (family NumericalFailure) Nat (constructor NumericalFailure NumericalInexactOperation))) (branch StdApproximationUnsupported . (constructor StdResult StdFailure (family NumericalFailure) Nat (constructor NumericalFailure NumericalUnsupportedOperation)))))))) def numericalCheckExact = (lambda unrestricted contract : (family NumericalContract) . (eliminate NumericalRelation (lambda unrestricted current : (family NumericalRelation) . (family StdResult (family NumericalFailure) Nat)) (numericalRelationOf contract) (branch NumericalExactOrder identity . (numericalRequire Nat (naturalAnd (naturalNonzero (bytes-length identity)) (numericalIdentityPresent (stdNumericProfileIdentityOf (numericalProfileOf contract)))) (constructor NumericalFailure NumericalEmptyIdentity) (numericalRequire Nat (naturalLess (numericalSubnormalCode (stdNumericProfileSubnormalsOf (numericalProfileOf contract))) 2) (constructor NumericalFailure NumericalUnknownSubnormals) (numericalRequire Nat (naturalIsZero (numericalContractionCode (stdNumericProfileContractionOf (numericalProfileOf contract)))) (constructor NumericalFailure NumericalUnspecifiedContraction) (numericalCheckOperations (numericalProfileOf contract) (numericalOperationsOf contract)))))) (branch NumericalBoundedDifference reference norm tensors tolerance . (constructor StdResult StdFailure (family NumericalFailure) Nat (constructor NumericalFailure NumericalBoundEvidenceRequired))) (branch NumericalApproximateTransition transition schema . (constructor StdResult StdFailure (family NumericalFailure) Nat (constructor NumericalFailure NumericalTransitionEvidenceRequired))))) def numericalCompatibility = (lambda unrestricted required : (family NumericalContract) . (lambda unrestricted realized : (family NumericalContract) . (stdResultBind (family NumericalFailure) Nat Nat (numericalCheckExact required) (lambda unrestricted admitted : Nat . (stdResultBind (family NumericalFailure) Nat Nat (numericalCheckExact realized) (lambda unrestricted realizedAdmitted : Nat . (numericalRequire Nat (bytes-equal (numericalProfileBytes (numericalProfileOf required)) (numericalProfileBytes (numericalProfileOf realized))) (constructor NumericalFailure NumericalProfileMismatch) (numericalRequire Nat (naturalAnd (bytes-equal (numericalExactOrderBytes (numericalRelationOf required)) (numericalExactOrderBytes (numericalRelationOf realized))) (bytes-equal (numericalOperationBytes (numericalOperationsOf required)) (numericalOperationBytes (numericalOperationsOf realized)))) (constructor NumericalFailure NumericalOrderMismatch) numericalAccepted)))))))) -- The caller passes the actual produced/consumed formats, including the -- accumulation format when crossing an arithmetic boundary. No-conversion -- admits only identical formats. These checks authorize a typed operation, -- never an implicit transport conversion or an unimplemented lowering. def numericalConversion = (lambda unrestricted source : (family StdNumericFormat) . (lambda unrestricted destination : (family StdNumericFormat) . (lambda unrestricted requested : (family StdOption (family StdNumericConversion)) . (eliminate StdOption (lambda unrestricted current : (family StdOption (family StdNumericConversion)) . (family StdResult (family NumericalFailure) (family StdNumericConversion))) requested (branch StdNone . (numericalRequire (family StdNumericConversion) (naturalEqual (stdNumericFormatCode source) (stdNumericFormatCode destination)) (constructor NumericalFailure NumericalMissingConversion) (constructor StdResult StdSuccess (family NumericalFailure) (family StdNumericConversion) (constructor StdNumericConversion StdNumericKeepFormat source)))) (branch StdSome conversion . (numericalRequire (family StdNumericConversion) (naturalEqual (stdNumericFormatCode source) (stdNumericFormatCode (stdNumericConversionSource conversion))) (constructor NumericalFailure NumericalConversionSourceMismatch) (numericalRequire (family StdNumericConversion) (naturalEqual (stdNumericFormatCode destination) (stdNumericFormatCode (stdNumericConversionDestination conversion))) (constructor NumericalFailure NumericalConversionDestinationMismatch) (constructor StdResult StdSuccess (family NumericalFailure) (family StdNumericConversion) conversion))))))))