code wiki / _hdl_build / _cegis_validator.nx
_cegis_validator.nx source
↩ module page · 64 lines · 1865 B
1// CONVERGED BY THE NISHI TEAM CEGIS LOOP (_cegis_authored): counterexample-guided,
2// zero disagreements with the oracle on the full probe domain. NOT retrieved.
3import "nx_syscalls.nx"
4func _c_le(a: i64, b: i64) -> i64 { if a <= b { return 1 } return 0 }
5func _c_and(a: i64, b: i64) -> i64 { return a & b }
6func _c_shr(a: i64, b: i64) -> i64 { return a >> (b & 63) }
7func _c_min(a: i64, b: i64) -> i64 { if a < b { return a } return b }
8func _c_max(a: i64, b: i64) -> i64 { if a > b { return a } return b }
9func _c_add(a: i64, b: i64) -> i64 { return a + b }
10func _c_sub(a: i64, b: i64) -> i64 { return a - b }
11func _c_mul(a: i64, b: i64) -> i64 { return a * b }
12func _c_shl(a: i64, b: i64) -> i64 { return a << (b & 63) }
13func _c_div(a: i64, b: i64) -> i64 { if b == 0 { return 0 } return a / b }
14func _c_mod(a: i64, b: i64) -> i64 { if b == 0 { return 0 } return a % b }
15func _c_abs(a: i64) -> i64 { if a < 0 { return 0 - a } return a }
16func resynth(a: i64, b: i64) -> i64 { return _c_and(_c_le(b, 99), _c_le(10, a)) }
17func main() -> i64 {
18 let ka: *i64 = sys_mmap(256) as *i64
19 let kb: *i64 = sys_mmap(256) as *i64
20 let kx: *i64 = sys_mmap(256) as *i64
21 ka[0] = 0
22 kb[0] = 0
23 kx[0] = 0
24 ka[1] = 1
25 kb[1] = 1
26 kx[1] = 0
27 ka[2] = 16
28 kb[2] = 8
29 kx[2] = 1
30 ka[3] = 100
31 kb[3] = 50
32 kx[3] = 1
33 ka[4] = 3
34 kb[4] = 0 - 60
35 kx[4] = 0
36 ka[5] = 0 - 60
37 kb[5] = 3
38 kx[5] = 0
39 ka[6] = 7
40 kb[6] = 0 - 60
41 kx[6] = 0
42 ka[7] = 0 - 60
43 kb[7] = 7
44 kx[7] = 0
45 ka[8] = 10
46 kb[8] = 100
47 kx[8] = 0
48 ka[9] = 10
49 kb[9] = 0 - 60
50 kx[9] = 1
51 ka[10] = 10
52 kb[10] = 10
53 kx[10] = 1
54 ka[11] = 10
55 kb[11] = 99
56 kx[11] = 1
57 var i: i64 = 0
58 while i < 12 {
59 if resynth(ka[i], kb[i]) != kx[i] { sys_exit(1) }
60 i = i + 1
61 }
62 sys_exit(0)
63 return 0
64}