nx_pose_cnn_gate.nx source

1// nx_pose_cnn_gate.nx -- executed proof of the sovereign f32 pose-CNN FORWARD PASS end-to-end into the integer 2// keypoint back-half. A tiny 8x8 single-channel image with impulses runs through a REAL 3x3 f32 conv backbone 3// (identity weights, so the peak is predictable while the full 9-tap f32 multiply-add path is exercised) + a REAL 4// 1x1 f32 pose head, then the ReLU'd f32 heatmap is fed DIRECTLY (order-isomorphism) into nx_pose_keypoints. 5// Proves: forward peak + quarter-pixel subpixel through the conv, ReLU zeroing, the f32-bits occlusion threshold, 6// the ReLU unit behavior, and (C5) that the ReLU is LOAD-BEARING -- integer argmax picks the wrong cell on a raw 7// negative activation and the right cell only after ReLU. expect_exit: 0 8import "nx_syscalls.nx" 9import "nx_f32_cvt.nx" 10import "nx_pose_cnn.nx" 11import "nx_pose_keypoints.nx" 12 13func gp(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return sys_write(1, s, n) } 14func gn(v: i64) -> i64 { 15 let bb: *u8 = sys_mmap(28); var m: i64 = v 16 if m < 0 { sys_write(1, "-" as *u8, 1); m = 0 - m } 17 let t: *u8 = sys_mmap(28); var k: i64 = 0 18 if m == 0 { t[0] = 48 as u8; k = 1 } 19 while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 } 20 var i: i64 = 0; while i < k { bb[i] = t[k - 1 - i]; i = i + 1 } 21 return sys_write(1, bb, k) 22} 23 24func main(argc: i64, argv: *i64) -> i64 { 25 var pass: i64 = 0 26 let W: i64 = 8; let H: i64 = 8 27 28 // f32 constants (built at runtime from ints -- no hardcoded bit patterns except -0.0). 29 let f1: i64 = nx_i32_to_f32(1) 30 let f2: i64 = nx_i32_to_f32(2) 31 let f5: i64 = nx_i32_to_f32(5) 32 let f60: i64 = nx_i32_to_f32(60) 33 let f100: i64 = nx_i32_to_f32(100) 34 let f200: i64 = nx_i32_to_f32(200) 35 let fn3: i64 = nx_i32_to_f32(0 - 3) 36 let fn50: i64 = nx_i32_to_f32(0 - 50) 37 38 let inp: *i64 = sys_mmap(8 * 64) as *i64 39 let feat: *i64 = sys_mmap(8 * 64) as *i64 40 let heat: *i64 = sys_mmap(8 * 64) as *i64 41 let wbb: *i64 = sys_mmap(8 * 16) as *i64 42 let whd: *i64 = sys_mmap(8 * 16) as *i64 43 let qx: *i64 = sys_mmap(8) as *i64 44 let qy: *i64 = sys_mmap(8) as *i64 45 46 // input: +0.0 everywhere, a 100 peak at (x=3,y=2), a 60 right-neighbor at (x=4,y=2) to drive subpixel +1, 47 // and a NEGATIVE -50 at (x=6,y=6) that the ReLU must zero. 48 var i: i64 = 0; while i < 64 { inp[i] = 0; i = i + 1 } 49 inp[2*8 + 3] = f100 50 inp[2*8 + 4] = f60 51 inp[6*8 + 6] = fn50 52 53 // backbone 3x3 identity: center tap (index 4) = 1.0, all other 8 taps = +0.0. 54 i = 0; while i < 9 { wbb[i] = 0; i = i + 1 } 55 wbb[4] = f1 56 // head 1x1 identity: single tap = 1.0. 57 whd[0] = f1 58 59 let rb: i64 = pose_cnn_backbone3x3(inp, 1, H, W, wbb, 1, 0 as *i64, feat) 60 let rh: i64 = pose_cnn_head1x1(feat, 1, H, W, whd, 1, 0 as *i64, heat) 61 62 // C1: forward peak + subpixel through the real conv. peak (3,2), right neighbor higher -> sx=+1 -> qx=13, qy=8. 63 var c1: i64 = pose_keypoint(heat, W, H, f1, qx, qy) 64 if c1 == f100 { if qx[0] == 13 { if qy[0] == 8 { 65 pass = pass + 1; gp("C1 forward peak (qx=13,qy=8,conf=100.0) through f32 conv OK\n" as *u8) 66 } } } 67 if qx[0] != 13 { gp("C1 FAIL qx=" as *u8); gn(qx[0]); gp(" qy=" as *u8); gn(qy[0]); gp(" conf==f100? " as *u8); gn(c1 == f100); gp("\n" as *u8) } 68 69 // C2: ReLU zeroed the -50 negative -> heatmap at (6,6) is +0.0 bits. 70 if heat[6*8 + 6] == 0 { pass = pass + 1; gp("C2 ReLU zeroed negative activation at (6,6) OK\n" as *u8) } 71 if heat[6*8 + 6] != 0 { gp("C2 FAIL heat(6,6)=" as *u8); gn(heat[6*8 + 6]); gp("\n" as *u8) } 72 73 // C3: occlusion via the f32-bits threshold. conf 100.0 < thresh 200.0 (bit-order-correct for positives) -> -1. 74 var c3: i64 = pose_keypoint(heat, W, H, f200, qx, qy) 75 if c3 == 0 { if qx[0] == 0 - 1 { pass = pass + 1; gp("C3 f32-bits occlusion threshold (100<200) -> occluded OK\n" as *u8) } } 76 if qx[0] != 0 - 1 { gp("C3 FAIL qx=" as *u8); gn(qx[0]); gp("\n" as *u8) } 77 78 // C4: ReLU unit -- [5, -3, -0.0, 2] -> [5, 0, 0, 2]. 79 let rb4: *i64 = sys_mmap(8 * 4) as *i64 80 rb4[0] = f5; rb4[1] = fn3; rb4[2] = 0x80000000; rb4[3] = f2 81 pose_cnn_relu(rb4, 4) 82 if rb4[0] == f5 { if rb4[1] == 0 { if rb4[2] == 0 { if rb4[3] == f2 { 83 pass = pass + 1; gp("C4 ReLU unit [5,-3,-0.0,2]->[5,0,0,2] OK\n" as *u8) 84 } } } } 85 if rb4[1] != 0 { gp("C4 FAIL b1=" as *u8); gn(rb4[1]); gp(" b2=" as *u8); gn(rb4[2]); gp("\n" as *u8) } 86 87 // C5: the ReLU is LOAD-BEARING. Raw [100.0, -50.0]: integer argmax picks index 1 (the negative's sign-bit 88 // pattern sorts above the positive peak) -- WRONG. After ReLU -> [100.0, 0]: argmax picks index 0 -- RIGHT. 89 let t2: *i64 = sys_mmap(8 * 2) as *i64 90 let px: *i64 = sys_mmap(8) as *i64; let py: *i64 = sys_mmap(8) as *i64 91 t2[0] = f100; t2[1] = fn50 92 pose_argmax(t2, 2, 1, px, py) 93 var wrong: i64 = px[0] 94 pose_cnn_relu(t2, 2) 95 pose_argmax(t2, 2, 1, px, py) 96 var right: i64 = px[0] 97 if wrong == 1 { if right == 0 { 98 pass = pass + 1; gp("C5 ReLU load-bearing: pre-ReLU argmax=1 (wrong), post-ReLU argmax=0 (right) OK\n" as *u8) 99 } } 100 if wrong != 1 { gp("C5 FAIL pre=" as *u8); gn(wrong); gp(" post=" as *u8); gn(right); gp("\n" as *u8) } 101 102 gp("POSE-CNN-GATE pass=" as *u8); gn(pass); gp("/5 (rb=" as *u8); gn(rb); gp(" rh=" as *u8); gn(rh); gp(")\n" as *u8) 103 if pass == 5 { gp("POSE-CNN-GATE GREEN 5/5 (f32 conv backbone + 1x1 head -> ReLU heatmap -> integer keypoint, end-to-end)\n" as *u8); sys_exit(0) } 104 sys_exit(1) 105 return 0 106}