nx_f32_q14_encode_test.nx source
↩ module page · 75 lines · 3829 B
1// nx_f32_q14_encode_test.nx -- KAT gate for f32_from_q14, the EXACT Q14->IEEE-754
2// units bridge the arbitrary-mesh STL writer needs. Proves: (a) hand-verified bit
3// patterns for whole-mm and sub-mm values, (b) sign handling, (c) it is the precise
4// inverse of the reader's nx_fp32_bytes_to_q14 (write Q14 -> f32 bytes -> read back
5// == original Q14, exact, for print-bed-range values). expect_exit: 0.
6
7import "nx_syscalls.nx"
8import "nx_le.nx"
9import "nx_f32_encode.nx"
10import "nx_fp32_q14.nx"
11
12func w(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 }
13func wn(v: i64) -> i64 {
14 let b: *u8 = sys_mmap(28); var m: i64 = v
15 if m < 0 { m = 0 - m; sys_write(1, "-" as *u8, 1) }
16 let t: *u8 = sys_mmap(28); var k: i64 = 0
17 if m == 0 { t[0] = 48 as u8; k = 1 }
18 while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }
19 var i: i64 = 0; while i < k { b[i] = t[k - 1 - i]; i = i + 1 }
20 sys_write(1, b, k); return 0
21}
22func chk(cond: i64, pass: *i64, fail: *i64, label: *u8) -> i64 {
23 if cond == 1 { pass[0] = pass[0] + 1; w(" ok " as *u8); w(label); w("\n" as *u8) }
24 else { fail[0] = fail[0] + 1; w(" XX " as *u8); w(label); w("\n" as *u8) }
25 return 0
26}
27func eqi(a: i64, b: i64) -> i64 { if a == b { return 1 } return 0 }
28
29// round-trip: encode q14 -> 4 f32 bytes -> reader's f32->Q14 -> recovered q14
30func roundtrip(q14: i64) -> i64 {
31 let bytes: *u8 = sys_mmap(16)
32 nx_le_write_u32(bytes, 0, f32_from_q14(q14))
33 let outq: *i64 = (sys_mmap(8)) as *i64
34 let nc: i64 = nx_fp32_bytes_to_q14(bytes, 0, 1, outq)
35 if nc != 1 { return 0x7fffffffffffffff }
36 return outq[0]
37}
38
39func main() -> i64 {
40 let pass: *i64 = (sys_mmap(8)) as *i64
41 let fail: *i64 = (sys_mmap(8)) as *i64
42 pass[0] = 0
43 fail[0] = 0
44 w("=== nx_f32_from_q14 KAT (exact Q14->IEEE-754 units bridge) ===\n" as *u8)
45
46 // (a) zero
47 chk(eqi(f32_from_q14(0), 0), pass, fail, "q14 0 -> f32 0x00000000" as *u8)
48 // (b) 1.0 mm (16384 Q14) == f32 of integer 1
49 chk(eqi(f32_from_q14(16384), f32_from_i64(1)), pass, fail, "1.0mm == f32_from_i64(1)" as *u8)
50 // (c) 20.0 mm (the proven cube case) == f32 of integer 20
51 chk(eqi(f32_from_q14(20 * 16384), f32_from_i64(20)), pass, fail, "20.0mm == f32_from_i64(20)" as *u8)
52 // (d) 0.5 mm sub-mm -> 0x3F000000 = 1056964608
53 chk(eqi(f32_from_q14(8192), 1056964608), pass, fail, "0.5mm -> 0x3F000000 (sub-mm exact)" as *u8)
54 // (e) 0.25 mm -> 0x3E800000 = 1048576000
55 chk(eqi(f32_from_q14(4096), 1048576000), pass, fail, "0.25mm -> 0x3E800000 (sub-mm exact)" as *u8)
56 // (f) sign: -1.0 mm -> 0xBF800000 = 3212836864 == f32_from_i64(-1)
57 chk(eqi(f32_from_q14(0 - 16384), 3212836864), pass, fail, "-1.0mm -> 0xBF800000 (sign)" as *u8)
58 chk(eqi(f32_from_q14(0 - 16384), f32_from_i64(0 - 1)), pass, fail, "-1.0mm == f32_from_i64(-1)" as *u8)
59
60 // (g) ROUND-TRIP through the reader's converter == identity (the inverse proof)
61 let r1: i64 = roundtrip(163840) // 10mm
62 w(" rt(10mm=163840)=" as *u8); wn(r1); w("\n" as *u8)
63 chk(eqi(r1, 163840), pass, fail, "round-trip 10mm exact via reader" as *u8)
64 let r2: i64 = roundtrip(3277) // ~0.2mm layer height value
65 w(" rt(3277)=" as *u8); wn(r2); w("\n" as *u8)
66 chk(eqi(r2, 3277), pass, fail, "round-trip 3277 (0.2mm) exact via reader" as *u8)
67 let r3: i64 = roundtrip(0 - 163840) // -10mm
68 chk(eqi(r3, 0 - 163840), pass, fail, "round-trip -10mm exact via reader" as *u8)
69 let r4: i64 = roundtrip(1) // smallest Q14 step (1/16384 mm)
70 chk(eqi(r4, 1), pass, fail, "round-trip 1 ULP (1/16384 mm) exact" as *u8)
71
72 w("=== VERDICT pass=" as *u8); wn(pass[0]); w(" fail=" as *u8); wn(fail[0]); w(" ===\n" as *u8)
73 if fail[0] == 0 { return 0 }
74 return 1
75}