code wiki / _hdl_build / nx_media_import_gate.nx

nx_media_import_gate.nx source

↩ module page · 54 lines · 3545 B

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 10 11func grow(name: *u8, ok: i64) -> i64 { if ok==1 { gw(" PASS " as *u8) } else { gw(" FAIL " as *u8) } gw(name); gw(" 12" as *u8); return ok } 13func 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 } 14 15func main() -> i64 { 16 gw("nx_media_import gate (polite-by-construction: robots REFUSES disallowed paths)\n" as *u8) 17 var pass: i64 = 0 18 let host: *u8 = sys_mmap(512); let pidx: *i64 = sys_mmap(8) as *i64 19 20 // T1 full URL 21 let hl: i64 = mi_split("https://shop.example.com/products/dress-42.html" as *u8, host, pidx) 22 var t1: i64 = 0 23 if hl == 16 { if g_streq(host, "shop.example.com" as *u8)==1 { if pidx[0] > 0 { t1 = 1 } } } 24 gw(" host=" as *u8); gw(host); gw("\n" as *u8) 25 pass = pass + grow("T1 mi_split host=shop.example.com + path present\x00" as *u8, t1) 26 27 // T2 no path -> default 28 let host2: *u8 = sys_mmap(512); let pidx2: *i64 = sys_mmap(8) as *i64 29 mi_split("https://cdn.example.org" as *u8, host2, pidx2) 30 pass = pass + grow("T2 mi_split no-path -> path_idx=-1 (default /)\x00" as *u8, pidx2[0] == 0 - 1) 31 32 // robots.txt: block /products/, allow /products/public/, crawl-delay 5 33 let rob: *u8 = "User-agent: *\nDisallow: /products/\nAllow: /products/public/\nCrawl-delay: 5\n" as *u8 34 let rl: i64 = g_slen(rob) 35 // T3 a disallowed path -> REFUSE 36 let a3: i64 = nx_robots_allowed(rob, rl, MI_UA, MI_UA_LEN, "/products/dress-42.html" as *u8, 23) 37 pass = pass + grow("T3 Disallow /products/ REFUSES /products/dress (allowed=0)\x00" as *u8, a3 == 0) 38 // T4 Allow-override longer match wins 39 let a4: i64 = nx_robots_allowed(rob, rl, MI_UA, MI_UA_LEN, "/products/public/x.jpg" as *u8, 22) 40 pass = pass + grow("T4 Allow /products/public/ overrides (allowed=1)\x00" as *u8, a4 == 1) 41 42 // T5 no robots.txt -> allowed (RFC 9309 unavailable = full allow) 43 let a5: i64 = nx_robots_allowed("" as *u8, 0, MI_UA, MI_UA_LEN, "/anything" as *u8, 9) 44 pass = pass + grow("T5 no robots.txt -> allowed (full-allow)\x00" as *u8, a5 == 1) 45 46 // T6 a specific UA group for us beats '*' (host bans '*' from /x but allows us) 47 let rob6: *u8 = "User-agent: *\nDisallow: /x/\n\nUser-agent: NishiMediaImporter\nDisallow:\n" as *u8 48 let a6: i64 = nx_robots_allowed(rob6, g_slen(rob6), MI_UA, MI_UA_LEN, "/x/y.jpg" as *u8, 8) 49 pass = pass + grow("T6 our specific UA group (empty Disallow) beats '*' ban (allowed=1)\x00" as *u8, a6 == 1) 50 51 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) 52 if pass == 6 { gw("verdict=GREEN (media importer honors robots.txt: refuses disallowed paths, respects our UA group)\n" as *u8); sys_exit(0); return 0 } 53 gw("verdict=RED\n" as *u8); sys_exit(1); return 1 54}