nx_cpuid_gate.nx source

1// nx_cpuid_gate.nx -- proves the cpuid(7,0):EBX decode, including features THIS BOX DOES NOT HAVE. 2// 3// The load-bearing cells are T7/T8: they decode AVX-512 correctly on a V1500B (Zen 1, NO AVX-512) by 4// feeding synthetic registers. A feature detector that can only be tested on silicon you already own is 5// worthless for the exact question it exists to answer -- 'will the next machine be faster'. 6// Every policy cell is a gv_bite (fires on bad, silent on good). license_tier: ORIGINAL expect_exit: 0 7import "nx_cpuid_lib.nx" 8import "nx_gate_verdict.nx" 9 10const CG_BUF: i64 = 512 11const CG_ALL_ONES: i64 = 4294967295 12const CG_ONLY_AVX2: i64 = 32 13const CG_ONLY_AVX512F: i64 = 65536 14// V1500B-SHAPED synthetic vector (bits 0,3,5,7,8,18,19,20,23,29 from its /proc/cpuinfo flags). 15// Labelled SHAPED, not measured: the live register may carry additional bits. Live agreement is the 16// ORGAN's job (triangulation vs /proc/cpuinfo); this gate proves the DECODE, not the silicon. 17const CG_V1500B_SHAPED: i64 = 547094953 18 19func cg_cpy(d: *u8, s: *u8) -> i64 { 20 var i: i64 = 0 21 while s[i] != (0 as u8) { d[i] = s[i]; i = i + 1 } 22 d[i] = 0 as u8 23 return i 24} 25func cg_eq(a: i64, b: i64) -> i64 { if a == b { return 1 } return 0 } 26 27func main() -> i64 { 28 let ctr: *i64 = gv_ctr() 29 gv_head("nx_cpuid_gate -- cpuid(7,0):EBX decode, proven for silicon we do NOT own" as *u8) 30 31 gv_check("T1 an all-zero register reports every feature absent" as *u8, 32 cg_eq(cf_avx2(0) + cf_bmi2(0) + cf_sha(0) + cf_avx512f(0), 0), ctr) 33 gv_check("T2 an all-ones register reports every feature present" as *u8, 34 cg_eq(cf_avx2(CG_ALL_ONES) + cf_bmi2(CG_ALL_ONES) + cf_sha(CG_ALL_ONES) + cf_avx512f(CG_ALL_ONES), 4), ctr) 35 gv_bite("T3 bit-5 alone means AVX2 and ONLY AVX2 (no neighbouring-bit bleed)" as *u8, 36 cg_eq(cf_avx2(CG_ONLY_AVX2), 1), 37 cg_eq(cf_bmi2(CG_ONLY_AVX2) + cf_avx512f(CG_ONLY_AVX2) + cf_sha(CG_ONLY_AVX2), 1), ctr) 38 gv_check("T4 tier(scalar)=0 when nothing vector is present" as *u8, 39 cg_eq(cf_simd_tier(0), CF_TIER_SCALAR), ctr) 40 gv_check("T5 tier(AVX2-only)=1" as *u8, cg_eq(cf_simd_tier(CG_ONLY_AVX2), CF_TIER_AVX2), ctr) 41 42 // ---- the cells that matter for FUTURE hardware ---- 43 gv_bite("T6 AVX-512F decodes on a box with NO AVX-512 (synthetic register)" as *u8, 44 cg_eq(cf_avx512f(CG_ONLY_AVX512F), 1), 45 cg_eq(cf_avx512f(CG_V1500B_SHAPED), 1), ctr) 46 gv_bite("T7 AVX-512F alone promotes the dispatch tier to 2" as *u8, 47 cg_eq(cf_simd_tier(CG_ONLY_AVX512F), CF_TIER_AVX512), 48 cg_eq(cf_simd_tier(CG_V1500B_SHAPED), CF_TIER_AVX512), ctr) 49 gv_check("T8 the four AVX-512 refinement bits decode independently of F" as *u8, 50 cg_eq(cf_avx512dq(CG_ONLY_AVX512F) + cf_avx512cd(CG_ONLY_AVX512F) + cf_avx512bw(CG_ONLY_AVX512F) + cf_avx512vl(CG_ONLY_AVX512F), 0), ctr) 51 52 // ---- this machine's shape: AVX2 + BMI2 + SHA yes, AVX-512 no ---- 53 var t9: i64 = 0 54 if cf_avx2(CG_V1500B_SHAPED) == 1 { if cf_bmi2(CG_V1500B_SHAPED) == 1 { if cf_sha(CG_V1500B_SHAPED) == 1 { if cf_adx(CG_V1500B_SHAPED) == 1 { if cf_avx512f(CG_V1500B_SHAPED) == 0 { t9 = 1 } } } } } 55 gv_check("T9 V1500B-shaped decodes AVX2+BMI2+SHA+ADX present, AVX-512 absent" as *u8, t9, ctr) 56 gv_check("T10 V1500B-shaped lands on dispatch tier 1 (AVX2)" as *u8, 57 cg_eq(cf_simd_tier(CG_V1500B_SHAPED), CF_TIER_AVX2), ctr) 58 59 // ---- fail-closed on nonsense: a bad bit index must never fabricate a feature ---- 60 gv_bite("T11 cf_bit REFUSES an out-of-range bit index instead of fabricating one" as *u8, 61 cg_eq(cf_bit(CG_ALL_ONES, 32), 0 - 1), 62 cg_eq(cf_bit(CG_ALL_ONES, 31), 0 - 1), ctr) 63 gv_bite("T12 cf_bit REFUSES a negative register (sign-extension would lie)" as *u8, 64 cg_eq(cf_bit(0 - 1, 5), 0 - 1), 65 cg_eq(cf_bit(CG_ONLY_AVX2, 5), 0 - 1), ctr) 66 67 // ---- the independent oracle, and the substring lie it must not tell ---- 68 let fb: *u8 = sys_mmap(CG_BUF) 69 let n: i64 = cg_cpy(fb, "flags\t\t: fpu vme de pse avx2 sha_ni bmi2 adx clflushopt\n" as *u8) 70 gv_check("T13 cf_flag finds a real token in a /proc/cpuinfo flags line" as *u8, 71 cg_eq(cf_flag(fb, n, "avx2" as *u8), 1), ctr) 72 gv_bite("T14 cf_flag REFUSES 'avx' inside 'avx2' -- the substring lie" as *u8, 73 cg_eq(cf_flag(fb, n, "avx" as *u8), 0), 74 cg_eq(cf_flag(fb, n, "avx2" as *u8), 0), ctr) 75 gv_check("T15 cf_flag matches the LAST token on the line (newline delimiter)" as *u8, 76 cg_eq(cf_flag(fb, n, "clflushopt" as *u8), 1), ctr) 77 gv_check("T16 cf_flag reports absent for a feature this box lacks" as *u8, 78 cg_eq(cf_flag(fb, n, "avx512f" as *u8), 0), ctr) 79 80 // ---- CPUID.1:EBX -- cache line + SMT topology, the two facts nx_hw HARDCODES ---- 81 // Synthetic register shaped like this NAS: CLFLUSH field (bits 15:8) = 8 -> 8x8 = 64 bytes, which is 82 // exactly what /proc/cpuinfo reports as `clflush size: 64` and `cache_alignment: 64`. Logical-procs 83 // field (bits 23:16) = 8 -> 8 threads per package, the SMT fact nx_hw_envelope reports as "cores". 84 let ebx1: i64 = (8 << 8) | (8 << 16) 85 gv_check("T17 CPUID.1:EBX[15:8] x8 = the REAL 64-byte cache line (nx_hw hardcodes this)" as *u8, 86 cg_eq(cf_cache_line(ebx1), 64), ctr) 87 gv_check("T18 CPUID.1:EBX[23:16] = 8 logical procs per package (the SMT fact nx_hw lacks)" as *u8, 88 cg_eq(cf_logical_procs(ebx1), 8), ctr) 89 gv_bite("T19 a ZERO cache-line field REFUSES rather than returning a plausible default" as *u8, 90 cg_eq(cf_cache_line(0), 0 - 1), 91 cg_eq(cf_cache_line(ebx1), 0 - 1), ctr) 92 gv_bite("T20 a ZERO logical-procs field REFUSES (assumed != measured, and a spore must know)" as *u8, 93 cg_eq(cf_logical_procs(0), 0 - 1), 94 cg_eq(cf_logical_procs(ebx1), 0 - 1), ctr) 95 gv_check("T21 a 128-byte line decodes too (field 16) -- not pinned to this machine" as *u8, 96 cg_eq(cf_cache_line(16 << 8), 128), ctr) 97 98 let rc: i64 = gv_verdict("CPUID-GATE" as *u8, ctr, "cpuid(7,0):EBX decode proven incl. silicon we do not own" as *u8) 99 sys_exit(rc) 100 return rc 101}