nx_adc_acc_kat.nx source
↩ module page · 56 lines · 2202 B
1// nx_adc_acc_kat.nx -- isolated KAT for the G3 __adc_acc intrinsic with DIRECT
2// 3-word {acc0,acc1,acc2} assertions. REQUIRED before the consumer swap: the
3// byte-exact multiply fuzz CANNOT catch a mis-encoded adcq or a swapped
4// 8(%r11)/16(%r11) offset whose corruption lands outside the compared 512-bit
5// window (FIX-8). Includes the FIX-6 carry-equivalence boundary (cy1 <= 1).
6// __adc_acc(acc_ptr, lo, hi): acc0+=lo (carry); acc1+=hi+carry (carry); acc2+=carry.
7// exit 0 = all correct; nonzero encodes the failing case+word. license_tier: ORIGINAL
8
9import "nx_syscalls.nx"
10
11func chk(acc: *i64, e0: i64, e1: i64, e2: i64, code: i64) -> i64 {
12 if acc[0] != e0 { return code }
13 if acc[1] != e1 { return code + 1 }
14 if acc[2] != e2 { return code + 2 }
15 return 0
16}
17
18func main() -> i64 {
19 let acc: *i64 = sys_mmap(64) as *i64
20 let M: i64 = 0 - 1 // 0xFFFFFFFFFFFFFFFF
21 var r: i64 = 0
22
23 // case 1: {0,0,0} + (hi=7 : lo=5) -> {5,7,0}
24 acc[0] = 0; acc[1] = 0; acc[2] = 0
25 __adc_acc(acc, 5, 7)
26 r = chk(acc, 5, 7, 0, 10); if r != 0 { return r }
27
28 // case 2: carry out of acc0. {10,0,0} + (hi=0 : lo=M) -> {9,1,0}
29 acc[0] = 10; acc[1] = 0; acc[2] = 0
30 __adc_acc(acc, M, 0)
31 r = chk(acc, 9, 1, 0, 20); if r != 0 { return r }
32
33 // case 3: carry into acc2. {0,M,0} + (hi=5 : lo=0) -> {0,4,1}
34 acc[0] = 0; acc[1] = M; acc[2] = 0
35 __adc_acc(acc, 0, 5)
36 r = chk(acc, 0, 4, 1, 30); if r != 0 { return r }
37
38 // case 4: FIX-6 boundary acc1=M, hi=1, carry_in=1 -> single carry-out (cy1<=1).
39 // {M,M,0} + (hi=1 : lo=1): acc0=M+1=0 (c=1); acc1=M+1+1=1 (c=1); acc2=0+1=1.
40 acc[0] = M; acc[1] = M; acc[2] = 0
41 __adc_acc(acc, 1, 1)
42 r = chk(acc, 0, 1, 1, 40); if r != 0 { return r }
43
44 // case 5: lo=0, hi=max -> {0,M,0} (no carry, M < 2^64)
45 acc[0] = 0; acc[1] = 0; acc[2] = 0
46 __adc_acc(acc, 0, M)
47 r = chk(acc, 0, M, 0, 50); if r != 0 { return r }
48
49 // case 6: full cascade {M,M,M} + (hi=0 : lo=1) -> {0,0,0}? no: acc0=M+1=0 c=1;
50 // acc1=M+0+1=0 c=1; acc2=M+1=0. -> {0,0,0}
51 acc[0] = M; acc[1] = M; acc[2] = M
52 __adc_acc(acc, 1, 0)
53 r = chk(acc, 0, 0, 0, 60); if r != 0 { return r }
54
55 return 0
56}