AlphaGitHub
Source/Systems

Coppelius.Build.TiledChoices

systems/coppelius/src/Coppelius/Build/TiledChoices.alpha

38 lines3 declarations4.5 KiBSHA-256 35e9ff143e3d
Download exact fileView at revisionf5034773ad4bb52133

Complete file · line 16

TiledChoices.alpha

Definition view
1module Coppelius.Build.TiledChoices
2
3import Data.Bytes
4import Std.Natural
5
6-- GENERATED by scripts/alpha/tiled-choices.py from
7-- systems/coppelius/evidence/tiled-choices/choices.json: do not edit.
8-- Each Coppelius tiled product's candidate (an index into
9-- Coppelius.Build.DeviceImages.coppeliusTiledCandidate), the fastest
10-- measured on NVIDIA GB10; a shape
11-- not listed has none, and the build refuses it.
12
13-- the kernel source the choices were measured on (its SHA-256)
14def coppeliusTiledChoicesKernel : Bytes = b"aee32305677c64bb1a0ca70ebaf7688c2c6be89d663972add73d955a4d4c0f3d"
15
16def coppeliusTiledChoiceNone : Nat = 4
17
18-- residual, A as columns, B as columns, m, n, k -> the candidate
19def coppeliusTiledChoice = (lambda unrestricted residual : Nat . (lambda unrestricted aColumns : Nat .
20  (lambda unrestricted bColumns : Nat . (lambda unrestricted m : Nat . (lambda unrestricted n : Nat .
21  (lambda unrestricted k : Nat .
22    (naturalSelect (naturalAnd (naturalEqual residual 0) (naturalAnd (naturalEqual aColumns 0) (naturalAnd (naturalEqual bColumns 0) (naturalAnd (naturalEqual m 1024) (naturalAnd (naturalEqual n 1536) (naturalEqual k 512)))))) 1
23    (naturalSelect (naturalAnd (naturalEqual residual 1) (naturalAnd (naturalEqual aColumns 0) (naturalAnd (naturalEqual bColumns 0) (naturalAnd (naturalEqual m 1024) (naturalAnd (naturalEqual n 512) (naturalEqual k 512)))))) 3
24    (naturalSelect (naturalAnd (naturalEqual residual 0) (naturalAnd (naturalEqual aColumns 0) (naturalAnd (naturalEqual bColumns 0) (naturalAnd (naturalEqual m 1024) (naturalAnd (naturalEqual n 1408) (naturalEqual k 512)))))) 3
25    (naturalSelect (naturalAnd (naturalEqual residual 1) (naturalAnd (naturalEqual aColumns 0) (naturalAnd (naturalEqual bColumns 0) (naturalAnd (naturalEqual m 1024) (naturalAnd (naturalEqual n 512) (naturalEqual k 1408)))))) 3
26    (naturalSelect (naturalAnd (naturalEqual residual 0) (naturalAnd (naturalEqual aColumns 0) (naturalAnd (naturalEqual bColumns 0) (naturalAnd (naturalEqual m 1024) (naturalAnd (naturalEqual n 12288) (naturalEqual k 512)))))) 2
27    (naturalSelect (naturalAnd (naturalEqual residual 0) (naturalAnd (naturalEqual aColumns 0) (naturalAnd (naturalEqual bColumns 1) (naturalAnd (naturalEqual m 1024) (naturalAnd (naturalEqual n 512) (naturalEqual k 1536)))))) 3
28    (naturalSelect (naturalAnd (naturalEqual residual 0) (naturalAnd (naturalEqual aColumns 0) (naturalAnd (naturalEqual bColumns 1) (naturalAnd (naturalEqual m 1024) (naturalAnd (naturalEqual n 512) (naturalEqual k 512)))))) 3
29    (naturalSelect (naturalAnd (naturalEqual residual 0) (naturalAnd (naturalEqual aColumns 0) (naturalAnd (naturalEqual bColumns 1) (naturalAnd (naturalEqual m 1024) (naturalAnd (naturalEqual n 512) (naturalEqual k 1408)))))) 3
30    (naturalSelect (naturalAnd (naturalEqual residual 1) (naturalAnd (naturalEqual aColumns 0) (naturalAnd (naturalEqual bColumns 1) (naturalAnd (naturalEqual m 1024) (naturalAnd (naturalEqual n 512) (naturalEqual k 1408)))))) 3
31    (naturalSelect (naturalAnd (naturalEqual residual 0) (naturalAnd (naturalEqual aColumns 0) (naturalAnd (naturalEqual bColumns 1) (naturalAnd (naturalEqual m 1024) (naturalAnd (naturalEqual n 1408) (naturalEqual k 512)))))) 1
32    (naturalSelect (naturalAnd (naturalEqual residual 0) (naturalAnd (naturalEqual aColumns 0) (naturalAnd (naturalEqual bColumns 1) (naturalAnd (naturalEqual m 1024) (naturalAnd (naturalEqual n 512) (naturalEqual k 12288)))))) 2
33    (naturalSelect (naturalAnd (naturalEqual residual 0) (naturalAnd (naturalEqual aColumns 1) (naturalAnd (naturalEqual bColumns 1) (naturalAnd (naturalEqual m 1536) (naturalAnd (naturalEqual n 512) (naturalEqual k 1024)))))) 1
34    (naturalSelect (naturalAnd (naturalEqual residual 0) (naturalAnd (naturalEqual aColumns 1) (naturalAnd (naturalEqual bColumns 1) (naturalAnd (naturalEqual m 512) (naturalAnd (naturalEqual n 512) (naturalEqual k 1024)))))) 2
35    (naturalSelect (naturalAnd (naturalEqual residual 0) (naturalAnd (naturalEqual aColumns 1) (naturalAnd (naturalEqual bColumns 1) (naturalAnd (naturalEqual m 1408) (naturalAnd (naturalEqual n 512) (naturalEqual k 1024)))))) 1
36    (naturalSelect (naturalAnd (naturalEqual residual 0) (naturalAnd (naturalEqual aColumns 1) (naturalAnd (naturalEqual bColumns 1) (naturalAnd (naturalEqual m 512) (naturalAnd (naturalEqual n 1408) (naturalEqual k 1024)))))) 1
37    (naturalSelect (naturalAnd (naturalEqual residual 0) (naturalAnd (naturalEqual aColumns 1) (naturalAnd (naturalEqual bColumns 1) (naturalAnd (naturalEqual m 12288) (naturalAnd (naturalEqual n 512) (naturalEqual k 1024)))))) 3
38coppeliusTiledChoiceNone))))))))))))))))))))))

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.