nx_scratch_probe.nx source
↩ module page · 35 lines · 1421 B
1// nx_scratch_probe.nx -- R0.0b proof kernel: uses the WASM-lane nx_scratch to allocate DISTINCT framed
2// buffers, the multi-word-local idiom that the wat lane previously had no allocator for. If nx_scratch
3// handed back the same address (the old no-op-alloca failure mode), a and b would alias and the sum would
4// be wrong; distinct buffers give the correct native-equivalent answer. Pure (imports only nx_wasm_scratch).
5import "nx_wasm_scratch.nx"
6
7// two DISTINCT 128-byte (16 x i64) scratch buffers, interleaved fill, then sum a[j]*b[j].
8func sp_two(n: i64) -> i64 {
9 let a: *i64 = nx_scratch(128) as *i64
10 let b: *i64 = nx_scratch(128) as *i64
11 var i: i64 = 0
12 while i < n { a[i] = i + 1; b[i] = (i + 1) * 10; i = i + 1 }
13 var s: i64 = 0
14 var j: i64 = 0
15 while j < n { s = s + a[j] * b[j]; j = j + 1 }
16 return s
17}
18
19// the address gap between two consecutive 128-byte allocs -- must be exactly 128 (distinct + sequential).
20func sp_gap() -> i64 {
21 let m: i64 = nx_scratch_save()
22 let a: i64 = nx_scratch(128) as i64
23 let b: i64 = nx_scratch(128) as i64
24 nx_scratch_restore(m)
25 return b - a
26}
27
28// composite KAT: sp_two twice with save/restore between (proves reclamation + repeatable distinct buffers).
29func sp_probe() -> i64 {
30 let m: i64 = nx_scratch_save()
31 let r1: i64 = sp_two(16)
32 nx_scratch_restore(m)
33 let r2: i64 = sp_two(16)
34 return r1 * 100000 + r2
35}