code wiki / (root) / nx_f32_conv_transpose2d_gate.nx
`nx_f32_conv_transpose2d_gate.nx` source

1// nx_f32_conv_transpose2d_gate.nx -- exact proof of transposed conv: kernel-spread of a single pixel, stride-2
2// upsample placement, and the guard. expect_exit: 0
3import "nx_syscalls.nx"
4import "nx_f32_cvt.nx"
5import "nx_f32_conv_transpose2d.nx"
6
7func gp(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return sys_write(1, s, n) }
8func gn(v: i64) -> i64 {
9    let bb: *u8 = sys_mmap(28); var m: i64 = v
10    if m < 0 { sys_write(1, "-" as *u8, 1); m = 0 - m }
11    let t: *u8 = sys_mmap(28); var k: i64 = 0
12    if m == 0 { t[0] = 48 as u8; k = 1 }
13    while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }
14    var i: i64 = 0; while i < k { bb[i] = t[k - 1 - i]; i = i + 1 }
15    return sys_write(1, bb, k)
16}
17
18func main(argc: i64, argv: *i64) -> i64 {
19    var pass: i64 = 0
20    let inp: *i64 = sys_mmap(8 * 16) as *i64
21    let wt:  *i64 = sys_mmap(8 * 16) as *i64
22    let out: *i64 = sys_mmap(8 * 32) as *i64
23
24    // T1 kernel-spread: input 1x1=[5], weight 2x2=[1,2,3,4], stride1 pad0 -> 2x2 = [5,10,15,20]
25    inp[0] = nx_i32_to_f32(5)
26    wt[0]=nx_i32_to_f32(1); wt[1]=nx_i32_to_f32(2); wt[2]=nx_i32_to_f32(3); wt[3]=nx_i32_to_f32(4)
27    var t1: i64 = nx_f32_conv_transpose2d(inp, 1, 1, 1, 1, wt, 1, 2, 2, 1, 0, 0, 0 as *i64, out)
28    if out[0]==nx_i32_to_f32(5) { if out[1]==nx_i32_to_f32(10) { if out[2]==nx_i32_to_f32(15) { if out[3]==nx_i32_to_f32(20) {
29        pass = pass + 1; gp("T1 kernel-spread [5,10,15,20] exact OK\n" as *u8)
30    } } } }
31    if out[0]!=nx_i32_to_f32(5) { gp("T1 FAIL o0=" as *u8); gn(out[0]); gp("\n" as *u8) }
32
33    // T2 stride-2 upsample placement: input 2x2=[1,2,3,4], weight 2x2=[1,0,0,0], stride2 pad0 -> 4x4
34    // each input(h,w) lands at out[2h,2w]; rest 0. row0=[1,0,2,0] row2=[3,0,4,0]
35    inp[0]=nx_i32_to_f32(1); inp[1]=nx_i32_to_f32(2); inp[2]=nx_i32_to_f32(3); inp[3]=nx_i32_to_f32(4)
36    wt[0]=nx_i32_to_f32(1); wt[1]=0; wt[2]=0; wt[3]=0
37    var t2: i64 = nx_f32_conv_transpose2d(inp, 1, 1, 2, 2, wt, 1, 2, 2, 2, 0, 0, 0 as *i64, out)
38    // OH=OW=4 ; out[0,0]=1 out[0,2]=2 out[2,0]=3(idx8) out[2,2]=4(idx10) ; out[0,1]=0
39    if out[0]==nx_i32_to_f32(1) { if out[2]==nx_i32_to_f32(2) { if out[8]==nx_i32_to_f32(3) { if out[10]==nx_i32_to_f32(4) { if out[1]==0 {
40        pass = pass + 1; gp("T2 stride-2 upsample places at even cells OK\n" as *u8)
41    } } } } }
42    if out[8]!=nx_i32_to_f32(3) { gp("T2 FAIL o0=" as *u8); gn(out[0]); gp(" o8=" as *u8); gn(out[8]); gp(" o10=" as *u8); gn(out[10]); gp("\n" as *u8) }
43
44    // T3 guard: stride 0 -> ERR
45    var t3: i64 = nx_f32_conv_transpose2d(inp, 1, 1, 2, 2, wt, 1, 2, 2, 0, 0, 0, 0 as *i64, out)
46    if t1==0 { if t2==0 { if t3==4 { pass = pass + 1; gp("T3 rc ok (valid=0, stride0=ERR) OK\n" as *u8) } } }
47    if t3 != 4 { gp("T3 FAIL t3=" as *u8); gn(t3); gp("\n" as *u8) }
48
49    gp("CONV-TRANSPOSE2D-GATE pass=" as *u8); gn(pass); gp("/3\n" as *u8)
50    if pass == 3 { gp("CONV-TRANSPOSE2D-GATE GREEN 3/3 (kernel-spread + stride-2 upsample + guard)\n" as *u8); sys_exit(0) }
51    sys_exit(1)
52    return 0
53}
nx_f32_conv_transpose2d_gate.nx source

`nx_f32_conv_transpose2d_gate.nx` source
