code wiki / (root) / nx_companion_rel_gate.nx
`nx_companion_rel_gate.nx` source

↩ module page · 106 lines · 7078 B
1// nx_companion_rel_gate.nx -- GATE for R1d (nx_companion_rel): relationship state evolves correctly and safely.
2// Proves: (T1) round-trip; (T2) facts APPEND additively (a new fact never erases a prior one); (T3) trust is
3// CLAMPED to 0..100 at both ends (never-brick numeric bound); (T4) a mutation preserves the other fields
4// (read-modify-write is lossless); (T5) the projected context carries stage + facts; (T6) neg -- unknown
5// (persona,user) yields empty context; (T7) ISOLATION -- one persona's relationship with a user is independent
6// of another persona's. Timestamp-fresh /tmp store -> deterministic re-runs. license_tier: ORIGINAL  expect_exit: 0
7import "nx_companion_rel.nx"
8import "nx_gate_verdict.nx"
9
10func rw(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 }
11func rn(v: i64) -> i64 { let bb: *u8=sys_mmap(28); var m: i64=v; if m<0{sys_write(1,"-" as *u8,1);m=0-m} let t: *u8=sys_mmap(28); var k: i64=0; if m==0{t[0]=48 as u8;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(1,bb,k); return 0 }
12func r_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 0} return 1 }
13func r_find(hay: *u8, hlen: i64, needle: *u8) -> i64 {
  var nl: i64=0; while needle[nl]!=(0 as u8){nl=nl+1}
  if nl==0 { return 1 }
  if hlen<nl { return 0 }
  var i: i64=0
  while i<=hlen-nl { var m: i64=1; var c: i64=0; while c<nl { if hay[i+c]!=needle[c]{m=0;c=nl} else {c=c+1} } if m==1 {return 1} i=i+1 }
  return 0
20}
21func r_slen(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} return n }
22
23func main() -> i64 {
  rw("=== nx_companion_rel_gate (R1d: relationship state -- evolving, additive, clamped, isolated) ===\n" as *u8)
  let EPT: *u8 = sys_mmap(256)
  var po: i64 = 0
  var i: i64=0; let pre: *u8="/tmp/rel-test-" as *u8; while pre[i]!=(0 as u8){EPT[po]=pre[i];po=po+1;i=i+1}
  var ms: i64 = sys_now_ms() % 100000000; var d: i64=7
  while d>=0 { EPT[po+d]=(48+(ms%10)) as u8; ms=ms/10; d=d-1 } po=po+8
  EPT[po]=0x2D as u8; po=po+1; EPT[po]=0 as u8
31
  let cap: i64 = 8192
  let sb: *u8 = sys_mmap(cap); let fb: *u8 = sys_mmap(cap); let mb: *u8 = sys_mmap(cap); let hb: *u8 = sys_mmap(cap)
  var pass: i64 = 0
  var tot: i64 = 0
36
  // seed the (aria, ellery) relationship
  rel_update_pfx(EPT, "aria" as *u8, "ellery" as *u8, "acquaintance" as *u8, 20, "likes gardenias" as *u8, "content" as *u8, "met in spring" as *u8)
39
  // T1 round-trip
  tot = tot + 1
  var t1: i64 = 0
  var tr: i64 = rel_read5(EPT, "aria" as *u8, "ellery" as *u8, sb, fb, mb, hb, cap)
  if tr == 20 { if r_streq(sb, "acquaintance" as *u8) == 1 { t1 = 1 } }
  if t1 == 1 { pass=pass+1; rw("PASS T1 round-trip: stage=acquaintance, trust=20\n" as *u8) } else { rw("FAIL T1 tr=" as *u8); rn(tr); rw(" stage=" as *u8); rw(sb); rw("\n" as *u8) }
46
  // T2 additive facts
  rel_note_fact_pfx(EPT, "aria" as *u8, "ellery" as *u8, "has a dog named Max" as *u8)
  tot = tot + 1
  rel_read5(EPT, "aria" as *u8, "ellery" as *u8, sb, fb, mb, hb, cap)
  var t2: i64 = 0
  if r_find(fb, r_slen(fb), "gardenias" as *u8) == 1 { if r_find(fb, r_slen(fb), "Max" as *u8) == 1 { t2 = 1 } }
  if t2 == 1 { pass=pass+1; rw("PASS T2 additive facts: both 'gardenias' and 'Max' retained (no loss)\n" as *u8) } else { rw("FAIL T2 facts=" as *u8); rw(fb); rw("\n" as *u8) }
54
  // T3 trust clamp -- high then low
  rel_bump_trust_pfx(EPT, "aria" as *u8, "ellery" as *u8, 90)     // 20+90=110 -> 100
  tot = tot + 1
  var thi: i64 = rel_read5(EPT, "aria" as *u8, "ellery" as *u8, sb, fb, mb, hb, cap)
  rel_bump_trust_pfx(EPT, "aria" as *u8, "ellery" as *u8, 0 - 500) // ->0
  var tlo: i64 = rel_read5(EPT, "aria" as *u8, "ellery" as *u8, sb, fb, mb, hb, cap)
  if thi == 100 { if tlo == 0 { pass=pass+1; rw("PASS T3 trust clamp: +90 -> 100 (max), -500 -> 0 (min)\n" as *u8) } else { rw("FAIL T3 tlo=" as *u8); rn(tlo); rw("\n" as *u8) } } else { rw("FAIL T3 thi=" as *u8); rn(thi); rw("\n" as *u8) }
62
  // restore a realistic trust, then change stage -- proving RMW preserves the other fields
  rel_bump_trust_pfx(EPT, "aria" as *u8, "ellery" as *u8, 75)     // 0+75=75
  rel_set_stage_pfx(EPT, "aria" as *u8, "ellery" as *u8, "close" as *u8)
  tot = tot + 1
  var tfin: i64 = rel_read5(EPT, "aria" as *u8, "ellery" as *u8, sb, fb, mb, hb, cap)
  var t4: i64 = 0
  if r_streq(sb, "close" as *u8) == 1 { if tfin == 75 { if r_find(fb, r_slen(fb), "gardenias" as *u8) == 1 { if r_find(fb, r_slen(fb), "Max" as *u8) == 1 { t4 = 1 } } } }
  if t4 == 1 { pass=pass+1; rw("PASS T4 lossless RMW: set stage=close, trust=75 preserved, facts intact\n" as *u8) } else { rw("FAIL T4 stage=" as *u8); rw(sb); rw(" trust=" as *u8); rn(tfin); rw("\n" as *u8) }
71
  // T5 context projection
  tot = tot + 1
  let ctx: *u8 = sys_mmap(4096)
  let cl: i64 = rel_context_pfx(EPT, "aria" as *u8, "ellery" as *u8, ctx, 4096)
  var t5: i64 = 0
  if cl > 0 { if r_find(ctx, cl, "close" as *u8) == 1 { if r_find(ctx, cl, "gardenias" as *u8) == 1 { if r_find(ctx, cl, "Max" as *u8) == 1 { t5 = 1 } } } }
  if t5 == 1 { pass=pass+1; rw("PASS T5 context projection: carries stage + durable facts\n" as *u8) } else { rw("FAIL T5 ctx=" as *u8); rw(ctx); rw("\n" as *u8) }
79
  // T6 neg -- unknown relationship
  tot = tot + 1
  let cl2: i64 = rel_context_pfx(EPT, "vera" as *u8, "nobody" as *u8, ctx, 4096)
  if cl2 == 0 { pass=pass+1; rw("PASS T6 neg-control: unknown (persona,user) -> empty context\n" as *u8) } else { rw("FAIL T6 cl2=" as *u8); rn(cl2); rw("\n" as *u8) }
84
  // T7 ISOLATION -- vera's relationship with ellery is independent of aria's
  rel_update_pfx(EPT, "vera" as *u8, "ellery" as *u8, "stranger" as *u8, 5, "guards her privacy" as *u8, "reserved" as *u8, "just met" as *u8)
  tot = tot + 1
  var t7: i64 = 0
  rel_read5(EPT, "aria" as *u8, "ellery" as *u8, sb, fb, mb, hb, cap)   // aria unchanged?
  if r_streq(sb, "close" as *u8) == 1 {
      rel_read5(EPT, "vera" as *u8, "ellery" as *u8, sb, fb, mb, hb, cap)
      if r_streq(sb, "stranger" as *u8) == 1 { t7 = 1 }
  }
  if t7 == 1 { pass=pass+1; rw("PASS T7 isolation: (aria,ellery)=close is independent of (vera,ellery)=stranger\n" as *u8) } else { rw("FAIL T7 stage=" as *u8); rw(sb); rw("\n" as *u8) }
95
  rw("nx_companion_rel_gate pass=" as *u8); rn(pass); rw("/" as *u8); rn(tot)
  // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check
  // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled
  // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify.
  let ctr__dry: *i64 = gv_ctr()
  ctr__dry[0] = pass
  ctr__dry[1] = tot
  let rc__dry: i64 = gv_verdict("COMPANION-REL-GATE" as *u8, ctr__dry, "Elder's relationship state evolves per-user: additive facts, clamped trust, lossless, isolated)" as *u8)
  sys_exit(rc__dry)
  return rc__dry
106}
nx_companion_rel_gate.nx source

`nx_companion_rel_gate.nx` source
