1module Learning.Numerics
2
3import Std.Numeric.Profile
4import Std.Foundation
5import Std.List
6import Std.Natural
7import Data.Bytes
8import Data.SHA256
9import Data.SHA256Digest
10import Data.SHA256Padding
11import Model.Word64
12
13-- A tolerance request is not evidence that a lowering meets it. Exact-order,
14-- bounded per-tensor difference, and an approximate state transition are
15-- distinct semantic choices. The latter two require their own conformance
16-- evidence before this planner can admit execution.
17family NumericalRelation : Type 0
18constructor NumericalExactOrder
19field unrestricted numericalOrderIdentity : Bytes
20constructor NumericalBoundedDifference
21field unrestricted numericalReferenceIdentity : Bytes
22field unrestricted numericalNormIdentity : Bytes
23field unrestricted numericalTensorSetIdentity : Bytes
24field unrestricted numericalDifferenceTolerance : (family StdTolerance)
25constructor NumericalApproximateTransition
26field unrestricted numericalTransitionIdentity : Bytes
27field unrestricted numericalPersistentStateSchema : Bytes
28
29end-family
30
31family NumericalContract : Type 0
32constructor NumericalContractOf
33field unrestricted numericalProfile : (family StdNumericProfile)
34field unrestricted numericalOperations : (family StdList (family StdNumericOperation))
35field unrestricted numericalRelation : (family NumericalRelation)
36
37end-family
38
39family NumericalFailure : Type 0
40constructor NumericalEmptyIdentity
41constructor NumericalUnknownSubnormals
42constructor NumericalUnspecifiedContraction
43constructor NumericalUnsupportedOperation
44constructor NumericalInexactOperation
45constructor NumericalProfileMismatch
46constructor NumericalOrderMismatch
47constructor NumericalBoundEvidenceRequired
48constructor NumericalTransitionEvidenceRequired
49constructor NumericalMissingConversion
50constructor NumericalConversionSourceMismatch
51constructor NumericalConversionDestinationMismatch
52
53end-family
54
55def numericalRequire =
56 (lambda erased value : Type 0 .
57 (lambda unrestricted condition : Nat .
58 (lambda unrestricted reason : (family NumericalFailure) .
59 (lambda unrestricted next : (family StdResult (family NumericalFailure) value) .
60 (nat-eliminate
61 (lambda unrestricted flag : Nat . (family StdResult (family NumericalFailure) value))
62 (constructor StdResult StdFailure (family NumericalFailure) value reason)
63 (lambda unrestricted prior : Nat .
64 (lambda unrestricted ignored : (family StdResult (family NumericalFailure) value) .
65 next))
66 condition)))))
67
68def numericalAccepted =
69 (constructor StdResult StdSuccess (family NumericalFailure) Nat 1)
70
71def numericalProfileOf =
72 (lambda unrestricted contract : (family NumericalContract) .
73 (eliminate
74 NumericalContract
75 (lambda unrestricted current : (family NumericalContract) . (family StdNumericProfile))
76 contract
77 (branch NumericalContractOf profile operations relation . profile)))
78
79def numericalOperationsOf =
80 (lambda unrestricted contract : (family NumericalContract) .
81 (eliminate
82 NumericalContract
83 (lambda unrestricted current : (family NumericalContract) .
84 (family StdList (family StdNumericOperation)))
85 contract
86 (branch NumericalContractOf profile operations relation . operations)))
87
88def numericalRelationOf =
89 (lambda unrestricted contract : (family NumericalContract) .
90 (eliminate
91 NumericalContract
92 (lambda unrestricted current : (family NumericalContract) . (family NumericalRelation))
93 contract
94 (branch NumericalContractOf profile operations relation . relation)))
95
96def numericalContractionCode =
97 (lambda unrestricted value : (family StdContraction) .
98 (eliminate
99 StdContraction
100 (lambda unrestricted current : (family StdContraction) . Nat)
101 value
102 (branch StdContractionForbidden . 0)
103 (branch StdContractionPermittedWhereEmitted . 1)))
104
105def numericalReductionCode =
106 (lambda unrestricted value : (family StdReductionOrder) .
107 (eliminate
108 StdReductionOrder
109 (lambda unrestricted current : (family StdReductionOrder) . Nat)
110 value
111 (branch StdReductionStrictLeftFold . 0)
112 (branch StdReductionDeclaredTree . 1)))
113
114def numericalSubnormalCode =
115 (lambda unrestricted value : (family StdSubnormalHandling) .
116 (eliminate
117 StdSubnormalHandling
118 (lambda unrestricted current : (family StdSubnormalHandling) . Nat)
119 value
120 (branch StdSubnormalsPreserved . 0)
121 (branch StdSubnormalsFlushedToZero . 1)
122 (branch StdSubnormalsUnmeasured . 2)))
123
124def numericalRoundingCode =
125 (lambda unrestricted value : (family StdRounding) .
126 (eliminate
127 StdRounding
128 (lambda unrestricted current : (family StdRounding) . Nat)
129 value
130 (branch StdRoundNearestEven . 0)))
131
132def numericalExceptionalCode =
133 (lambda unrestricted value : (family StdExceptionalValues) .
134 (eliminate
135 StdExceptionalValues
136 (lambda unrestricted current : (family StdExceptionalValues) . Nat)
137 value
138 (branch StdExceptionalIEEE . 0)
139 (branch StdExceptionalFiniteOrRefuse . 1)))
140
141-- Profile identity remains part of exact compatibility: the legacy IEEE
142-- exceptional policy does not specify target-independent NaN payload/default
143-- bits. Different targets need a shared qualified profile, or stronger explicit
144-- conformance evidence; matching operation names alone is insufficient.
145def numericalProfileBytes =
146 (lambda unrestricted profile : (family StdNumericProfile) .
147 (bytes-append
148 (stdNumericProfileIdentityBytes (stdNumericProfileIdentityOf profile))
149 (bytes-append
150 (stdNumericWord (stdNumericFormatCode (stdNumericProfileStorageOf profile)))
151 (bytes-append
152 (stdNumericWord (stdNumericFormatCode (stdNumericProfileAccumulationOf profile)))
153 (bytes-append
154 (stdNumericWord (numericalRoundingCode (stdNumericProfileRoundingOf profile)))
155 (bytes-append
156 (stdNumericWord (numericalContractionCode (stdNumericProfileContractionOf profile)))
157 (bytes-append
158 (stdNumericWord
159 (numericalReductionCode (stdNumericProfileReductionOrderOf profile)))
160 (bytes-append
161 (stdNumericWord (numericalSubnormalCode (stdNumericProfileSubnormalsOf profile)))
162 (bytes-append
163 (stdNumericWord
164 (numericalExceptionalCode (stdNumericProfileExceptionalOf profile)))
165 b"")))))))))
166
167def numericalOperationBytes =
168 (lambda unrestricted operations : (family StdList (family StdNumericOperation)) .
169 (bytes-append
170 (stdNumericWord (stdListLength (family StdNumericOperation) operations))
171 (eliminate
172 StdList
173 (lambda unrestricted current : (family StdList (family StdNumericOperation)) . Bytes)
174 operations
175 (branch StdListEmpty . b"")
176 (branch
177 StdListCons
178 head
179 tail
180 induction
181 .
182 (bytes-append (stdNumericWord (stdOperationCode head)) induction)))))
183
184def numericalExactOrderBytes =
185 (lambda unrestricted relation : (family NumericalRelation) .
186 (eliminate
187 NumericalRelation
188 (lambda unrestricted current : (family NumericalRelation) . Bytes)
189 relation
190 (branch NumericalExactOrder identity . identity)
191 (branch NumericalBoundedDifference reference norm tensors tolerance . b"")
192 (branch NumericalApproximateTransition transition schema . b"")))
193
194-- Only an admitted exact contract is currently encoded for executable identity.
195-- Non-exact requests refuse before emission; no empty hash is a valid identity.
196def numericalExactContractBytes =
197 (lambda unrestricted contract : (family NumericalContract) .
198 (bytes-append
199 b"alpha-numerical-exact-v1"
200 (bytes-append
201 (stdNumericSizedBytes (numericalProfileBytes (numericalProfileOf contract)))
202 (bytes-append
203 (numericalOperationBytes (numericalOperationsOf contract))
204 (stdNumericSizedBytes (numericalExactOrderBytes (numericalRelationOf contract)))))))
205
206def numericalExactContractDigest =
207 (lambda unrestricted contract : (family NumericalContract) .
208 (sha256RawDigestOrEmpty (numericalExactContractBytes contract)))
209
210def numericalIdentityPresent =
211 (lambda unrestricted identity : (family StdNumericProfileIdentity) .
212 (eliminate
213 StdNumericProfileIdentity
214 (lambda unrestricted current : (family StdNumericProfileIdentity) . Nat)
215 identity
216 (branch StdProfileIdentityX86SseScalarStrict . 1)
217 (branch StdProfileIdentitySm86CooperativeM0 . 1)
218 (branch StdProfileIdentityNamed name . (naturalNonzero (bytes-length name)))))
219
220def numericalCheckOperations =
221 (lambda unrestricted profile : (family StdNumericProfile) .
222 (lambda unrestricted operations : (family StdList (family StdNumericOperation)) .
223 (eliminate
224 StdList
225 (lambda unrestricted current : (family StdList (family StdNumericOperation)) .
226 (family StdResult (family NumericalFailure) Nat))
227 operations
228 (branch StdListEmpty . numericalAccepted)
229 (branch
230 StdListCons
231 head
232 tail
233 induction
234 .
235 (eliminate
236 StdApproximation
237 (lambda unrestricted current : (family StdApproximation) .
238 (family StdResult (family NumericalFailure) Nat))
239 (stdApproximationOf head (stdNumericProfileTable profile))
240 (branch StdApproximationExact . induction)
241 (branch
242 StdApproximationMaxUlp
243 ulp
244 .
245 (constructor
246 StdResult
247 StdFailure
248 (family NumericalFailure)
249 Nat
250 (constructor NumericalFailure NumericalInexactOperation)))
251 (branch
252 StdApproximationUnmeasured
253 .
254 (constructor
255 StdResult
256 StdFailure
257 (family NumericalFailure)
258 Nat
259 (constructor NumericalFailure NumericalInexactOperation)))
260 (branch
261 StdApproximationUnsupported
262 .
263 (constructor
264 StdResult
265 StdFailure
266 (family NumericalFailure)
267 Nat
268 (constructor NumericalFailure NumericalUnsupportedOperation))))))))
269
270def numericalCheckExact =
271 (lambda unrestricted contract : (family NumericalContract) .
272 (eliminate
273 NumericalRelation
274 (lambda unrestricted current : (family NumericalRelation) .
275 (family StdResult (family NumericalFailure) Nat))
276 (numericalRelationOf contract)
277 (branch
278 NumericalExactOrder
279 identity
280 .
281 (numericalRequire
282 Nat
283 (naturalAnd
284 (naturalNonzero (bytes-length identity))
285 (numericalIdentityPresent (stdNumericProfileIdentityOf (numericalProfileOf contract))))
286 (constructor NumericalFailure NumericalEmptyIdentity)
287 (numericalRequire
288 Nat
289 (naturalLess
290 (numericalSubnormalCode (stdNumericProfileSubnormalsOf (numericalProfileOf contract)))
291 2)
292 (constructor NumericalFailure NumericalUnknownSubnormals)
293 (numericalRequire
294 Nat
295 (naturalIsZero
296 (numericalContractionCode
297 (stdNumericProfileContractionOf (numericalProfileOf contract))))
298 (constructor NumericalFailure NumericalUnspecifiedContraction)
299 (numericalCheckOperations
300 (numericalProfileOf contract)
301 (numericalOperationsOf contract))))))
302 (branch
303 NumericalBoundedDifference
304 reference
305 norm
306 tensors
307 tolerance
308 .
309 (constructor
310 StdResult
311 StdFailure
312 (family NumericalFailure)
313 Nat
314 (constructor NumericalFailure NumericalBoundEvidenceRequired)))
315 (branch
316 NumericalApproximateTransition
317 transition
318 schema
319 .
320 (constructor
321 StdResult
322 StdFailure
323 (family NumericalFailure)
324 Nat
325 (constructor NumericalFailure NumericalTransitionEvidenceRequired)))))
326
327def numericalCompatibility =
328 (lambda unrestricted required : (family NumericalContract) .
329 (lambda unrestricted realized : (family NumericalContract) .
330 (stdResultBind
331 (family NumericalFailure)
332 Nat
333 Nat
334 (numericalCheckExact required)
335 (lambda unrestricted admitted : Nat .
336 (stdResultBind
337 (family NumericalFailure)
338 Nat
339 Nat
340 (numericalCheckExact realized)
341 (lambda unrestricted realizedAdmitted : Nat .
342 (numericalRequire
343 Nat
344 (bytes-equal
345 (numericalProfileBytes (numericalProfileOf required))
346 (numericalProfileBytes (numericalProfileOf realized)))
347 (constructor NumericalFailure NumericalProfileMismatch)
348 (numericalRequire
349 Nat
350 (naturalAnd
351 (bytes-equal
352 (numericalExactOrderBytes (numericalRelationOf required))
353 (numericalExactOrderBytes (numericalRelationOf realized)))
354 (bytes-equal
355 (numericalOperationBytes (numericalOperationsOf required))
356 (numericalOperationBytes (numericalOperationsOf realized))))
357 (constructor NumericalFailure NumericalOrderMismatch)
358 numericalAccepted))))))))
359
360-- The caller passes the actual produced/consumed formats, including the
361-- accumulation format when crossing an arithmetic boundary. No-conversion
362-- admits only identical formats. These checks authorize a typed operation,
363-- never an implicit transport conversion or an unimplemented lowering.
364def numericalConversion =
365 (lambda unrestricted source : (family StdNumericFormat) .
366 (lambda unrestricted destination : (family StdNumericFormat) .
367 (lambda unrestricted requested : (family StdOption (family StdNumericConversion)) .
368 (eliminate
369 StdOption
370 (lambda unrestricted current : (family StdOption (family StdNumericConversion)) .
371 (family StdResult (family NumericalFailure) (family StdNumericConversion)))
372 requested
373 (branch
374 StdNone
375 .
376 (numericalRequire
377 (family StdNumericConversion)
378 (naturalEqual (stdNumericFormatCode source) (stdNumericFormatCode destination))
379 (constructor NumericalFailure NumericalMissingConversion)
380 (constructor
381 StdResult
382 StdSuccess
383 (family NumericalFailure)
384 (family StdNumericConversion)
385 (constructor StdNumericConversion StdNumericKeepFormat source))))
386 (branch
387 StdSome
388 conversion
389 .
390 (numericalRequire
391 (family StdNumericConversion)
392 (naturalEqual
393 (stdNumericFormatCode source)
394 (stdNumericFormatCode (stdNumericConversionSource conversion)))
395 (constructor NumericalFailure NumericalConversionSourceMismatch)
396 (numericalRequire
397 (family StdNumericConversion)
398 (naturalEqual
399 (stdNumericFormatCode destination)
400 (stdNumericFormatCode (stdNumericConversionDestination conversion)))
401 (constructor NumericalFailure NumericalConversionDestinationMismatch)
402 (constructor
403 StdResult
404 StdSuccess
405 (family NumericalFailure)
406 (family StdNumericConversion)
407 conversion))))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.