nx_ale_format_validate.nx source

1// nx_ale_format_validate.nx -- sovereign ALE-FORMAT triple validator (rungs ALE-R0a/R0b). 2// Parses one task/grader/deployer triple file (contract|field|value lines) and 3// ENFORCES the ale_format.spec contracts with NO mocks: 4// (1) all 15 required fields present (5 task + 5 grader + 5 deployer); 5// (2) grader score_range bound to [0,1] -- the value MUST be exactly "0..1" 6// (lower-bound token 0 AND upper-bound token 1; anything else = out of range); 7// (3) grader deterministic -- the value MUST be "yes" (a "no" = non-deterministic). 8// ALE-R0b HARDENING (3 NEW semantic contracts as VALUES, grounded in the real 9// rdi-berkeley/agents-last-exam@6b7f1b98 repo cross-check): 10// (4) grader staged_reference_after -- value MUST be "yes" (reject LEAKAGE: the 11// hidden reference must be staged AFTER the agent completes; lifecycle.py 12// Phase 3 stage_reference proves the real ordering); 13// (5) grader code_graded -- value MUST be "yes" (reject HUMAN-JUDGE: grading is 14// the task's evaluate() code, never a human; a "no" breaks the measure); 15// (6) the numeric [0,1] range -- ENFORCED by check (2) "0..1" (lower bound 0, 16// upper bound 1); a value like "0..5" is rejected as out-of-range. 17// Silent organ: argv[1] = triple path. exit 0 iff ALL checks pass, else exit 1. 18// The refusal is REAL (a check that bites) -- the gate proves it on 5 tampered triples. 19// Landmines respected: nested ifs (no &&/||), flat exprs, <=6 args/func, no empty 20// string literal, strings authored via Write. license_tier: ORIGINAL 21import "nx_syscalls.nx" 22const K_MAGIC_262144: i64 = 262144 23 24// read whole file at path into buf (cap), return byte count (0 on open-fail) 25func av_read(path: *u8, buf: *u8, cap: i64) -> i64 { 26 let fd: i64 = sys_openat_rd(path) 27 if fd < 0 { return 0 } 28 var n: i64 = 0 29 var go: i64 = 1 30 while go == 1 { 31 let r: i64 = sys_read(fd, (buf as i64 + n) as *u8, cap - 1 - n) 32 if r <= 0 { go = 0 } else { n = n + r } 33 if n >= cap - 1 { go = 0 } 34 } 35 sys_close(fd) 36 return n 37} 38 39// length of a C string 40func av_len(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n } 41 42// does buf[pos..] match pat (len pl)? 1/0 43func av_match(buf: *u8, n: i64, pos: i64, pat: *u8, pl: i64) -> i64 { 44 if pos + pl > n { return 0 } 45 var k: i64 = 0 46 while k < pl { 47 if buf[pos + k] != pat[k] { return 0 } 48 k = k + 1 49 } 50 return 1 51} 52 53// is pos a line start? (pos==0 or previous byte is newline) 54func av_is_bol(buf: *u8, pos: i64) -> i64 { 55 if pos == 0 { return 1 } 56 if buf[pos - 1] == (10 as u8) { return 1 } 57 return 0 58} 59 60// find a line beginning with prefix; return its start index, or -1 61func av_find_line(buf: *u8, n: i64, prefix: *u8) -> i64 { 62 let pl: i64 = av_len(prefix) 63 var i: i64 = 0 64 while i < n { 65 if av_is_bol(buf, i) == 1 { 66 if av_match(buf, n, i, prefix, pl) == 1 { return i } 67 } 68 i = i + 1 69 } 70 return 0 - 1 71} 72 73// 1 if a line starting with prefix exists, else 0 74func av_has(buf: *u8, n: i64, prefix: *u8) -> i64 { 75 if av_find_line(buf, n, prefix) >= 0 { return 1 } 76 return 0 77} 78 79// the line with `prefix` exists AND its remainder (value to end-of-line) equals `val`. 80// prefix is e.g. "grader|deterministic|", val is e.g. "yes". 1/0. 81func av_val_is(buf: *u8, n: i64, prefix: *u8, val: *u8) -> i64 { 82 let start: i64 = av_find_line(buf, n, prefix) 83 if start < 0 { return 0 } 84 let pl: i64 = av_len(prefix) 85 let vl: i64 = av_len(val) 86 let vpos: i64 = start + pl 87 if av_match(buf, n, vpos, val, vl) == 0 { return 0 } 88 // require the value to end exactly here (next byte is newline or EOF) 89 let after: i64 = vpos + vl 90 if after >= n { return 1 } 91 if buf[after] == (10 as u8) { return 1 } 92 return 0 93} 94 95func main(argc: i64, argv: *i64) -> i64 { 96 if argc < 2 { sys_exit(2); return 2 } 97 let path: *u8 = argv[1] as *u8 98 let buf: *u8 = sys_mmap(K_MAGIC_262144) 99 let n: i64 = av_read(path, buf, K_MAGIC_262144) 100 if n <= 0 { sys_exit(3); return 3 } 101 102 var bad: i64 = 0 103 104 // CHECK 1: all 15 required fields present (line prefix contract|field|) 105 if av_has(buf, n, "task|id|" as *u8) == 0 { bad = bad + 1 } 106 if av_has(buf, n, "task|industry|" as *u8) == 0 { bad = bad + 1 } 107 if av_has(buf, n, "task|instruction|" as *u8) == 0 { bad = bad + 1 } 108 if av_has(buf, n, "task|input_stage|" as *u8) == 0 { bad = bad + 1 } 109 if av_has(buf, n, "task|artifact_path|" as *u8) == 0 { bad = bad + 1 } 110 if av_has(buf, n, "grader|code_graded|" as *u8) == 0 { bad = bad + 1 } 111 if av_has(buf, n, "grader|deterministic|" as *u8) == 0 { bad = bad + 1 } 112 if av_has(buf, n, "grader|score_range|" as *u8) == 0 { bad = bad + 1 } 113 if av_has(buf, n, "grader|staged_reference_after|" as *u8) == 0 { bad = bad + 1 } 114 if av_has(buf, n, "grader|per_task|" as *u8) == 0 { bad = bad + 1 } 115 if av_has(buf, n, "deployer|provisions_sandbox|" as *u8) == 0 { bad = bad + 1 } 116 if av_has(buf, n, "deployer|stages_input|" as *u8) == 0 { bad = bad + 1 } 117 if av_has(buf, n, "deployer|runs_agent|" as *u8) == 0 { bad = bad + 1 } 118 if av_has(buf, n, "deployer|stages_reference|" as *u8) == 0 { bad = bad + 1 } 119 if av_has(buf, n, "deployer|grades|" as *u8) == 0 { bad = bad + 1 } 120 121 // CHECK 2: grader score_range bound to [0,1] -- value MUST be exactly "0..1" 122 if av_val_is(buf, n, "grader|score_range|" as *u8, "0..1" as *u8) == 0 { bad = bad + 1 } 123 124 // CHECK 3: grader deterministic -- value MUST be "yes" 125 if av_val_is(buf, n, "grader|deterministic|" as *u8, "yes" as *u8) == 0 { bad = bad + 1 } 126 127 // CHECK 4 (ALE-R0b): grader staged_reference_after -- value MUST be "yes" 128 // (reject LEAKAGE; reference is staged only AFTER the agent finishes). 129 if av_val_is(buf, n, "grader|staged_reference_after|" as *u8, "yes" as *u8) == 0 { bad = bad + 1 } 130 131 // CHECK 5 (ALE-R0b): grader code_graded -- value MUST be "yes" 132 // (reject HUMAN-JUDGE; grading is the task's evaluate() code only). 133 if av_val_is(buf, n, "grader|code_graded|" as *u8, "yes" as *u8) == 0 { bad = bad + 1 } 134 135 if bad == 0 { sys_exit(0); return 0 } 136 sys_exit(1) 137 return 1 138}