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