Admitted when the slot spaces match the declared shapes (with the state's m
words), each program writes only its outputs, every sample has the declared width, at least two
owners exist and the total mass is positive and exactly representable as a
binary64 integer (below 2^53), since realizations carry it in binary64.
301def dataParallelAdmitted =
302 (lambda unrestricted contribution : Nat .
303 (lambda unrestricted update : Nat .
304 (lambda unrestricted system : (family DataParallelSystem contribution update) .
305 (let unrestricted k =
306 (dataParallelParameters contribution update system)
307 in
308 (let unrestricted s =
309 (dataParallelWidth contribution update system)
310 in
311 (let unrestricted m =
312 (dataParallelStateCount contribution update system)
313 in
314 (naturalAnd
315 (naturalNonzero k)
316 (naturalAnd
317 (naturalEqual contribution (naturalAdd (naturalMultiply 2 k) s))
318 (naturalAnd
319 (naturalEqual update (succ (naturalAdd (naturalMultiply 2 k) m)))
320 (naturalAnd
321 (naturalEqual
322 (stdListLength
323 StdU64
324 (dataParallelInitialParameters contribution update system))
325 k)
326 (naturalAnd
327 (dataParallelWritesWithin
328 contribution
329 (dataParallelContributionProgram contribution update system)
330 (naturalAdd k s)
331 contribution)
332 (naturalAnd
333 (dataParallelWritesWithin
334 update
335 (dataParallelUpdateProgram contribution update system)
336 0
337 (naturalAdd k m))
338 (naturalAnd
339 (naturalLessOrEqual 2 (dataParallelOwners contribution update system))
340 (naturalAnd
341 (naturalNonzero (dataParallelTotalMass contribution update system))
342 (naturalAnd
343 (naturalBelowTwoPower
344 53
345 (dataParallelTotalMass contribution update system))
346 (stdListFold
347 (family StdList (family StdList StdU64))
348 Nat
349 (lambda unrestricted owned : (family StdList (family StdList StdU64)) .
350 (lambda unrestricted rest : Nat .
351 (naturalAnd
352 rest
353 (stdListFold
354 (family StdList StdU64)
355 Nat
356 (lambda unrestricted sample : (family StdList StdU64) .
357 (lambda unrestricted more : Nat .
358 (naturalAnd
359 more
360 (naturalEqual (stdListLength StdU64 sample) s))))
361 1
362 owned))))
363 1
364 (dataParallelOwnerSamples contribution update system)))))))))))))))))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.