nx_geo_gate.nx source

1// nx_geo_gate.nx -- GATE (runnable) for the integer-exact geofence floor (nx_geo). Proves: 2// POLYGON: square center IN, EXACT edge resolution (1 microdeg in=IN/out=OUT), concave L notch OUT 3// + both bars IN (true ray-casting), bbox computed + pre-filter agrees 4// RADIUS : within-R fence exact boundary (d2==r2 -> IN, +1 -> OUT) AND cos longitude-compression 5// proven: at 45 deg a point 12000 microdeg EAST is IN while 12000 microdeg NORTH is OUT 6// (a lon microdegree covers less ground than a lat one) -- all integer, no sqrt. 7// 8// Evidence -> knowledge/status/geo_gate.log (GEOGATE authored=organ ... verdict=GREEN). 9// license_tier: ORIGINAL 10import "nx_geo.nx" 11import "nx_syscalls.nx" 12 13const GG_LOG: *u8 = "knowledge/status/geo_gate.log" 14 15func gg_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 } 16func gg_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 } 17 18func gg_set(p: *i64, idx: i64, lat: i64, lon: i64) -> i64 { p[idx * 2] = lat; p[idx * 2 + 1] = lon; return 0 } 19 20func gg_emit(fd: i64, ctr: i64, jin: i64, jout: i64, notch: i64, bar1: i64, bar2: i64, bxagree: i64, rNin: i64, rNout: i64, rEin: i64, rEdge: i64, ok: i64) -> i64 { 21 gg_w(fd, "GEOGATE authored=organ exact=integer-no-float square_center=" as *u8); gg_wn(fd, ctr) 22 gg_w(fd, " edge_1micro_in=" as *u8); gg_wn(fd, jin) 23 gg_w(fd, " edge_1micro_out=" as *u8); gg_wn(fd, jout) 24 gg_w(fd, " concave_notch_out=" as *u8); gg_wn(fd, notch) 25 gg_w(fd, " concave_bar1_in=" as *u8); gg_wn(fd, bar1) 26 gg_w(fd, " concave_bar2_in=" as *u8); gg_wn(fd, bar2) 27 gg_w(fd, " bbox_prefilter_agrees=" as *u8); gg_wn(fd, bxagree) 28 gg_w(fd, " radius_north_in=" as *u8); gg_wn(fd, rNin) 29 gg_w(fd, " radius_north_out=" as *u8); gg_wn(fd, rNout) 30 gg_w(fd, " radius_east_in_coscompress=" as *u8); gg_wn(fd, rEin) 31 gg_w(fd, " radius_edge_exact=" as *u8); gg_wn(fd, rEdge) 32 if ok == 1 { gg_w(fd, " verdict=GREEN\n" as *u8) } else { gg_w(fd, " verdict=RED\n" as *u8) } 33 return 0 34} 35 36func main() -> i64 { 37 // --- polygon fence: a 1-degree square (microdeg), CCW --- 38 let sq: *i64 = sys_mmap(8 * 8) as *i64 39 gg_set(sq, 0, 0, 0) 40 gg_set(sq, 1, 0, 10000000) 41 gg_set(sq, 2, 10000000, 10000000) 42 gg_set(sq, 3, 10000000, 0) 43 let ctr: i64 = geo_point_in_poly(sq, 4, 5000000, 5000000) 44 let jin: i64 = geo_point_in_poly(sq, 4, 5000000, 9999999) 45 let jout: i64 = geo_point_in_poly(sq, 4, 5000000, 10000001) 46 47 // --- concave L fence --- 48 let lp: *i64 = sys_mmap(8 * 12) as *i64 49 gg_set(lp, 0, 0, 0) 50 gg_set(lp, 1, 0, 10000000) 51 gg_set(lp, 2, 4000000, 10000000) 52 gg_set(lp, 3, 4000000, 4000000) 53 gg_set(lp, 4, 10000000, 4000000) 54 gg_set(lp, 5, 10000000, 0) 55 let notch: i64 = geo_point_in_poly(lp, 6, 7000000, 7000000) 56 let bar1: i64 = geo_point_in_poly(lp, 6, 2000000, 2000000) 57 let bar2: i64 = geo_point_in_poly(lp, 6, 7000000, 2000000) 58 59 // --- bbox pre-filter --- 60 let bx: *i64 = sys_mmap(8 * 4) as *i64 61 geo_poly_bbox(sq, 4, bx) 62 let fence_far: i64 = geo_fence_contains(sq, 4, bx, 50000000, 50000000) 63 let poly_far: i64 = geo_point_in_poly(sq, 4, 50000000, 50000000) 64 var bxagree: i64 = 0 65 if fence_far == poly_far { if bx[0] == 0 { if bx[2] == 10000000 { bxagree = 1 } } } 66 67 // --- RADIUS fence: center 45N/45E, lon_scale=cos(45)*1e6=707107, radius 9000 microdeg-lat-eq --- 68 let clat: i64 = 45000000 69 let clon: i64 = 45000000 70 let lscale: i64 = 707107 71 let r2: i64 = 81000000 // 9000^2 72 let rNin: i64 = geo_in_radius(clat, clon, lscale, r2, 45005000, 45000000) // 5000 N -> IN 73 let rNout: i64 = geo_in_radius(clat, clon, lscale, r2, 45012000, 45000000) // 12000 N -> OUT 74 let rEin: i64 = geo_in_radius(clat, clon, lscale, r2, 45000000, 45012000) // 12000 E -> IN (cos-compressed) 75 let rEout: i64 = geo_in_radius(clat, clon, lscale, r2, 45000000, 45014000) // 14000 E -> OUT 76 let rEdgeIn: i64 = geo_in_radius(clat, clon, lscale, r2, 45009000, 45000000) // d2==r2 -> IN 77 let rEdgeOut: i64 = geo_in_radius(clat, clon, lscale, r2, 45009001, 45000000) // d2>r2 -> OUT 78 79 var ok: i64 = 1 80 if ctr != 1 { ok = 0 } 81 if jin != 1 { ok = 0 } 82 if jout != 0 { ok = 0 } 83 if notch != 0 { ok = 0 } 84 if bar1 != 1 { ok = 0 } 85 if bar2 != 1 { ok = 0 } 86 if bxagree != 1 { ok = 0 } 87 if rNin != 1 { ok = 0 } 88 if rNout != 0 { ok = 0 } 89 if rEin != 1 { ok = 0 } // 12000 EAST is IN ... 90 if rEout != 0 { ok = 0 } 91 if rEdgeIn != 1 { ok = 0 } 92 if rEdgeOut != 0 { ok = 0 } 93 // ... while 12000 NORTH (rNout) is OUT -> proves cos longitude-compression is applied. 94 95 var redge: i64 = 0 96 if rEdgeIn == 1 { if rEdgeOut == 0 { redge = 1 } } 97 gg_emit(1, ctr, jin, jout, notch, bar1, bar2, bxagree, rNin, rNout, rEin, redge, ok) 98 let lf: i64 = sys_openat_append(GG_LOG, 420) 99 if lf >= 0 { gg_emit(lf, ctr, jin, jout, notch, bar1, bar2, bxagree, rNin, rNout, rEin, redge, ok); sys_close(lf) } 100 101 if ok == 1 { return 0 } 102 return 1 103}