code wiki / _hdl_build / _loopsynth_hash31.nx
_loopsynth_hash31.nx source
↩ module page · 59 lines · 1997 B
1// SYNTHESIZED BY THE NISHI TEAM (fold schema, _loop_synth_authored): the loop skeleton
2// is the sketch; INIT+STEP were derived from oracle queries and held-out-verified.
3import "nx_syscalls.nx"
4func _c_le(a: i64, b: i64) -> i64 { if a <= b { return 1 } return 0 }
5func _c_add(a: i64, b: i64) -> i64 { return a + b }
6func _c_max(a: i64, b: i64) -> i64 { if a > b { return a } return b }
7func _c_min(a: i64, b: i64) -> i64 { if a < b { return a } return b }
8func _c_mul(a: i64, b: i64) -> i64 { return a * b }
9func _c_and(a: i64, b: i64) -> i64 { return a & b }
10func _c_shr(a: i64, b: i64) -> i64 { return a >> (b & 63) }
11func _c_sub(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 step(a: i64, b: i64) -> i64 { return _c_add(b, _c_mul(a, 31)) }
17func synth(buf: *u8, n: i64) -> i64 {
18 var acc: i64 = 0
19 var i: i64 = 0
20 while i < n { acc = step(acc, buf[i] as i64); i = i + 1 }
21 return acc
22}
23func _g_byte(seed: i64, i: i64) -> i64 {
24 if (seed + i) % 3 == 0 { return 0 }
25 return (seed * 131 + i * 37) & 255
26}
27func main() -> i64 {
28 let s: *i64 = sys_mmap(64) as *i64
29 let l: *i64 = sys_mmap(64) as *i64
30 let e: *i64 = sys_mmap(64) as *i64
31 s[0] = 1
32 l[0] = 0
33 e[0] = 0
34 s[1] = 5
35 l[1] = 0
36 e[1] = 0
37 s[2] = 1
38 l[2] = 7
39 e[2] = 121079911201
40 s[3] = 5
41 l[3] = 7
42 e[3] = 127120999695
43 s[4] = 1
44 l[4] = 11
45 e[4] = 111819840676257408
46 s[5] = 5
47 l[5] = 11
48 e[5] = 117398912759508778
49 let buf: *u8 = sys_mmap(64)
50 var t: i64 = 0
51 while t < 6 {
52 var j: i64 = 0
53 while j < l[t] { buf[j] = _g_byte(s[t], j) as u8; j = j + 1 }
54 if synth(buf, l[t]) != e[t] { sys_exit(1) }
55 t = t + 1
56 }
57 sys_exit(0)
58 return 0
59}