nx_geo_h3_gate.nx source

1// nx_geo_h3_gate.nx -- GATE for GEO-018 H3-class hexagonal cell index. Proves correctness AND the 2// integer-exact uniform-adjacency exceed over a square grid: 3// cube : axial (2,-1) -> cube (2,-1,-1), q+r+s == 0 4// distance : dist((0,0),(0,0))=0, dist((0,0),(1,0))=1 (neighbour), dist((0,0),(2,-1))=2 5// UNIFORM : all 6 hex neighbours have norm2 == 1 (hex_minN==hex_maxN==1) -- equidistant 6// exceed : square Moore-8 neighbours have norm2 in {1,2} (sq_minN=1, sq_maxN=2) -- NON-uniform 7// ring/disk : ring(0)=1, ring(2)=12, disk(1)=7, disk(2)=19 (centered hexagonal numbers) 8// 9// Evidence -> knowledge/status/geo_h3.log (GEOH3GATE authored=organ ... verdict=GREEN). 10// license_tier: ORIGINAL 11import "nx_geo_h3.nx" 12import "nx_syscalls.nx" 13import "nx_gate_verdict.nx" 14 15const GH3_LOG: *u8 = "knowledge/status/geo_h3.log" 16 17func h3_w(fd: i64, s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(fd, s, n); return 0 } 18func h3_wn(fd: i64, v: i64) -> i64 { let bb: *u8 = sys_mmap(28); var m: i64=v; if m<0 {m=0-m; sys_write(fd,"-" as *u8,1)}; let t: *u8 = sys_mmap(28); var k: i64=0; if m==0 {t[0]=48;k=1}; while m>0 {t[k]=(48+(m%10)) as u8; m=m/10; k=k+1}; var i: i64=0; while i<k {bb[i]=t[k-1-i]; i=i+1}; sys_write(fd, bb, k); return 0 } 19 20func h3_emit(fd: i64, cube_ok: i64, hmin: i64, hmax: i64, smin: i64, smax: i64, r2: i64, d2: i64, ok: i64) -> i64 { 21 h3_w(fd, "GEOH3GATE authored=organ method=hex-cube-coords cube_ok=" as *u8); h3_wn(fd, cube_ok) 22 h3_w(fd, " hex_minN=" as *u8); h3_wn(fd, hmin) 23 h3_w(fd, " hex_maxN=" as *u8); h3_wn(fd, hmax) 24 h3_w(fd, " square_minN=" as *u8); h3_wn(fd, smin) 25 h3_w(fd, " square_maxN=" as *u8); h3_wn(fd, smax) 26 h3_w(fd, " ring2=" as *u8); h3_wn(fd, r2) 27 h3_w(fd, " disk2=" as *u8); h3_wn(fd, d2) 28 if ok == 1 { h3_w(fd, " verdict=GREEN\n" as *u8) } else { h3_w(fd, " verdict=RED\n" as *u8) } 29 return 0 30} 31 32func main() -> i64 { 33 let cube: *i64 = sys_mmap(8 * 3) as *i64 34 geo_hex_axial_to_cube(2, 0 - 1, cube) 35 var cube_ok: i64 = 0 36 if (cube[0] + cube[1] + cube[2]) == 0 { cube_ok = 1 } 37 38 let d0: i64 = geo_hex_distance(0, 0, 0, 0) // 0 39 let d1: i64 = geo_hex_distance(0, 0, 1, 0) // 1 40 let d2d: i64 = geo_hex_distance(0, 0, 2, 0 - 1) // 2 41 42 // hex uniform adjacency: norm2 of all 6 neighbour offsets (from origin). 43 let nb: *i64 = sys_mmap(16) as *i64 44 var hmin: i64 = 0 45 var hmax: i64 = 0 46 var dir: i64 = 0 47 while dir < 6 { 48 geo_hex_neighbor(0, 0, dir, nb) 49 let nn: i64 = geo_hex_norm2(nb[0], nb[1]) 50 if dir == 0 { hmin = nn; hmax = nn } else { 51 if nn < hmin { hmin = nn } 52 if nn > hmax { hmax = nn } 53 } 54 dir = dir + 1 55 } 56 57 // square Moore-8: norm2 = dx^2+dy^2 over the 8 neighbours. 58 var smin: i64 = 0 59 var smax: i64 = 0 60 var first: i64 = 1 61 var dx: i64 = 0 - 1 62 while dx <= 1 { 63 var dy: i64 = 0 - 1 64 while dy <= 1 { 65 var skip: i64 = 0 66 if dx == 0 { if dy == 0 { skip = 1 } } // 1 iff dx==0 && dy==0 (the centre, not a neighbour) 67 if skip == 0 { 68 let sn: i64 = dx * dx + dy * dy 69 if first == 1 { smin = sn; smax = sn; first = 0 } else { 70 if sn < smin { smin = sn } 71 if sn > smax { smax = sn } 72 } 73 } 74 dy = dy + 1 75 } 76 dx = dx + 1 77 } 78 79 let ring2: i64 = geo_hex_ring_size(2) // 12 80 let disk1: i64 = geo_hex_disk_size(1) // 7 81 let disk2: i64 = geo_hex_disk_size(2) // 19 82 let ring0: i64 = geo_hex_ring_size(0) // 1 83 84 var ok: i64 = 1 85 if cube_ok != 1 { ok = 0 } 86 if d0 != 0 { ok = 0 } 87 if d1 != 1 { ok = 0 } 88 if d2d != 2 { ok = 0 } 89 if hmin != 1 { ok = 0 } 90 if hmax != 1 { ok = 0 } // hex: all neighbours equidistant 91 if smin != 1 { ok = 0 } 92 if smax != 2 { ok = 0 } // square: non-uniform (1 vs 2) -> measured exceed 93 if ring2 != 12 { ok = 0 } 94 if disk1 != 7 { ok = 0 } 95 if disk2 != 19 { ok = 0 } 96 if ring0 != 1 { ok = 0 } 97 98 h3_emit(1, cube_ok, hmin, hmax, smin, smax, ring2, disk2, ok) 99 let lf: i64 = sys_openat_append(GH3_LOG, 420) 100 if lf >= 0 { h3_emit(lf, cube_ok, hmin, hmax, smin, smax, ring2, disk2, ok); sys_close(lf) } 101 102 // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check 103 // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled 104 // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify. 105 let ctr__dry: *i64 = gv_ctr() 106 ctr__dry[0] = ok 107 ctr__dry[1] = 1 108 let rc__dry: i64 = gv_verdict("GEO-H3-GATE" as *u8, ctr__dry, "teeth unchanged; verdict emission migrated onto the shared base class" as *u8) 109 sys_exit(rc__dry) 110 return rc__dry 111}