nx_media_import_gate.nx source

1import "nx_gate_base.nx" 2// nx_media_import_gate.nx -- proves the POLITE-BY-CONSTRUCTION invariants of the general media importer: 3// URL splitting is correct AND a robots.txt Disallow REFUSES the fetch (the importer must never fetch a path the 4// host forbids). Accept-valid (a real import) is proven end-to-end by a live fetch (Wikipedia Cat = 38 images). 5// T1/T2 mi_split extracts host+path (incl the default "/") ; T3 robots Disallow => REFUSE ; T4 Allow-override wins 6// ; T5 no robots.txt => allowed ; T6 our UA token is honored specifically over '*'. GREEN iff 6/6. expect_exit: 0 7import "nx_syscalls.nx" 8import "nx_media_import.nx" // mi_split + MI_UA/MI_UA_LEN 9import "nx_robots.nx" // nx_robots_allowed 10import "nx_gate_verdict.nx" 11 12func grow(name: *u8, ok: i64) -> i64 { if ok==1 { gw(" PASS " as *u8) } else { gw(" FAIL " as *u8) } gw(name); gw(" 13" as *u8); return ok } 14func g_streq(a: *u8, b: *u8) -> i64 { var i: i64=0; while a[i]!=(0 as u8){ if a[i]!=b[i]{return 0} i=i+1 } if b[i]==(0 as u8){return 1} return 0 } 15 16func main() -> i64 { 17 gw("nx_media_import gate (polite-by-construction: robots REFUSES disallowed paths)\n" as *u8) 18 var pass: i64 = 0 19 let host: *u8 = sys_mmap(512); let pidx: *i64 = sys_mmap(8) as *i64 20 21 // T1 full URL 22 let hl: i64 = mi_split("https://shop.example.com/products/dress-42.html" as *u8, host, pidx) 23 var t1: i64 = 0 24 if hl == 16 { if g_streq(host, "shop.example.com" as *u8)==1 { if pidx[0] > 0 { t1 = 1 } } } 25 gw(" host=" as *u8); gw(host); gw("\n" as *u8) 26 pass = pass + grow("T1 mi_split host=shop.example.com + path present\x00" as *u8, t1) 27 28 // T2 no path -> default 29 let host2: *u8 = sys_mmap(512); let pidx2: *i64 = sys_mmap(8) as *i64 30 mi_split("https://cdn.example.org" as *u8, host2, pidx2) 31 pass = pass + grow("T2 mi_split no-path -> path_idx=-1 (default /)\x00" as *u8, pidx2[0] == 0 - 1) 32 33 // robots.txt: block /products/, allow /products/public/, crawl-delay 5 34 let rob: *u8 = "User-agent: *\nDisallow: /products/\nAllow: /products/public/\nCrawl-delay: 5\n" as *u8 35 let rl: i64 = g_slen(rob) 36 // T3 a disallowed path -> REFUSE 37 let a3: i64 = nx_robots_allowed(rob, rl, MI_UA, MI_UA_LEN, "/products/dress-42.html" as *u8, 23) 38 pass = pass + grow("T3 Disallow /products/ REFUSES /products/dress (allowed=0)\x00" as *u8, a3 == 0) 39 // T4 Allow-override longer match wins 40 let a4: i64 = nx_robots_allowed(rob, rl, MI_UA, MI_UA_LEN, "/products/public/x.jpg" as *u8, 22) 41 pass = pass + grow("T4 Allow /products/public/ overrides (allowed=1)\x00" as *u8, a4 == 1) 42 43 // T5 no robots.txt -> allowed (RFC 9309 unavailable = full allow) 44 let a5: i64 = nx_robots_allowed("" as *u8, 0, MI_UA, MI_UA_LEN, "/anything" as *u8, 9) 45 pass = pass + grow("T5 no robots.txt -> allowed (full-allow)\x00" as *u8, a5 == 1) 46 47 // T6 a specific UA group for us beats '*' (host bans '*' from /x but allows us) 48 let rob6: *u8 = "User-agent: *\nDisallow: /x/\n\nUser-agent: NishiMediaImporter\nDisallow:\n" as *u8 49 let a6: i64 = nx_robots_allowed(rob6, g_slen(rob6), MI_UA, MI_UA_LEN, "/x/y.jpg" as *u8, 8) 50 pass = pass + grow("T6 our specific UA group (empty Disallow) beats '*' ban (allowed=1)\x00" as *u8, a6 == 1) 51 52 gw("pass=" as *u8); let b: *u8=sys_mmap(8); b[0]=(48+pass) as u8; sys_write(1,b,1); gw("/6\n" as *u8) 53 // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check 54 // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled 55 // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify. 56 let ctr__dry: *i64 = gv_ctr() 57 ctr__dry[0] = pass 58 ctr__dry[1] = 6 59 let rc__dry: i64 = gv_verdict("MEDIA-IMPORT-GATE" as *u8, ctr__dry, "media importer honors robots.txt: refuses disallowed paths, respects our UA group)" as *u8) 60 sys_exit(rc__dry) 61 return rc__dry 62}