module Coppelius.Build.TiledChoices

import Data.Bytes
import Std.Natural

-- GENERATED by scripts/alpha/tiled-choices.py from
-- systems/coppelius/evidence/tiled-choices/choices.json: do not edit.
-- Each Coppelius tiled product's candidate (an index into
-- Coppelius.Build.DeviceImages.coppeliusTiledCandidate), the fastest
-- measured on NVIDIA GB10; a shape
-- not listed has none, and the build refuses it.

-- the kernel source the choices were measured on (its SHA-256)
def coppeliusTiledChoicesKernel : Bytes = b"aee32305677c64bb1a0ca70ebaf7688c2c6be89d663972add73d955a4d4c0f3d"

def coppeliusTiledChoiceNone : Nat = 4

-- residual, A as columns, B as columns, m, n, k -> the candidate
def coppeliusTiledChoice = (lambda unrestricted residual : Nat . (lambda unrestricted aColumns : Nat .
  (lambda unrestricted bColumns : Nat . (lambda unrestricted m : Nat . (lambda unrestricted n : Nat .
  (lambda unrestricted k : Nat .
    (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
    (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
    (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
    (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
    (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
    (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
    (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
    (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
    (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
    (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
    (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
    (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
    (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
    (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
    (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
    (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
coppeliusTiledChoiceNone))))))))))))))))))))))