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}