nx_estate_inventory_gate.nx source

1// nx_estate_inventory_gate.nx -- proves the estate inventory's CONFLICT-REDUCING storage properties by driving 2// the REAL /tmp/nx_estate_inventory.sov.elf over a fresh store: 3// NEVER-LOSE : put 3 assets -> get each back faithfully (the beneficiary survives a round-trip) 4// SINGLE TRUTH : update an asset -> get returns the NEW value, not the old (one authoritative current state) 5// AUDIT TRAIL : history shows BOTH the old AND new versions (immutable; old never destroyed) -> the 6// executor + heirs see the complete, tamper-evident change record = less to dispute 7// FULL INVENTORY : list enumerates EVERY asset (the whole will), each at its CURRENT state, DEDUPED (an 8// asset edited twice appears once) -> the executor sees the complete estate at a glance 9// GREEN iff 10/10. Durable knowledge/status/estate_inventory_gate.log. license_tier: ORIGINAL 10import "nx_syscalls.nx" 11 12func e_puts(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 } 13func e_num(v: i64) -> i64 { let bb: *u8=sys_mmap(28); var m: i64=v; if m<0{m=0-m;sys_write(1,"-" as *u8,1)}; 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 } 14func e_w(fd: i64, s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(fd,s,n); return 0 } 15func e_wn(fd: i64, v: i64) -> i64 { let bb: *u8=sys_mmap(28); var m: i64=v; if m<0{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(fd,bb,k); return 0 } 16func e_strlen(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} return n } 17func e_read_small(path: *u8, buf: *u8, cap: i64) -> i64 { 18 let fd: i64=sys_openat_rd(path); if fd<0 { return 0 } 19 var total: i64=0; var nrd: i64=sys_read(fd, buf, cap) 20 while nrd>0 { total=total+nrd; if total>=cap { nrd=0 } else { nrd=sys_read(fd, ((buf as i64)+total) as *u8, cap-total) } } 21 sys_close(fd); return total 22} 23func e_contains(hay: *u8, n: i64, needle: *u8) -> i64 { 24 let nl: i64=e_strlen(needle); if nl==0 { return 0 } 25 var i: i64=0 26 while i+nl<=n { var j: i64=0; var hit: i64=1; while j<nl { if hay[i+j]!=needle[j] { hit=0; j=nl } else { j=j+1 } } if hit==1 { return 1 } i=i+1 } 27 return 0 28} 29// fork the real estate tool with args[0..nargs); stdout -> out_path; return exit code 30func e_run(args: *i64, nargs: i64, out_path: *u8) -> i64 { 31 let pid: i64=sys_fork() 32 if pid==0 { 33 let o: i64=sys_openat_wr(out_path, 0x1a4); if o>=0 { sys_dup3(o,1,0) } 34 let argv: *i64=sys_mmap(8*16) as *i64 35 argv[0]="/tmp/nx_estate_inventory.sov.elf" as *u8 as i64 36 var i: i64=0; while i<nargs { argv[1+i]=args[i]; i=i+1 } argv[1+nargs]=0 37 let envp: *i64=sys_mmap(16) as *i64; envp[0]="PATH=/usr/bin:/bin" as *u8 as i64; envp[1]=0 38 sys_execve("/tmp/nx_estate_inventory.sov.elf" as *u8, argv, envp); sys_exit(127) 39 } 40 let st: *i64=sys_mmap(16) as *i64; sys_wait4(pid, st, 0); return (st[0]>>8)&0xff 41} 42 43func main() -> i64 { 44 e_puts("=== ESTATE INVENTORY GATE (never-lose + single-truth + immutable audit trail) ===\n" as *u8) 45 let P: *u8="/tmp/estate_gate-" as *u8 46 let outp: *u8="/tmp/estate_gate_out.txt" as *u8 47 let obuf: *u8=sys_mmap(65536) 48 let a: *i64=sys_mmap(8*8) as *i64 49 50 // --- put 3 assets --- 51 a[0]="put" as *u8 as i64; a[1]=P as i64; a[2]="house" as *u8 as i64; a[3]="Family home 123 Main St Salt Lake" as *u8 as i64; a[4]="350000" as *u8 as i64; a[5]="Alice" as *u8 as i64 52 e_run(a, 6, outp) 53 a[2]="car" as *u8 as i64; a[3]="2019 Subaru Outback" as *u8 as i64; a[4]="22000" as *u8 as i64; a[5]="Bob" as *u8 as i64 54 e_run(a, 6, outp) 55 a[2]="savings" as *u8 as i64; a[3]="Credit union savings account" as *u8 as i64; a[4]="80000" as *u8 as i64; a[5]="Carol" as *u8 as i64 56 e_run(a, 6, outp) 57 58 var pass: i64=0 59 let rows: i64=10 60 61 // R1-R3 NEVER-LOSE: get each asset back, beneficiary survives 62 a[0]="get" as *u8 as i64; a[1]=P as i64; a[2]="house" as *u8 as i64 63 e_run(a, 3, outp); var n1: i64=e_read_small(outp, obuf, 65536) 64 e_puts(" R1 get house has 'Alice'? " as *u8); if e_contains(obuf,n1,"Alice" as *u8)==1 { pass=pass+1; e_puts("YES PASS\n" as *u8) } else { e_puts("NO FAIL\n" as *u8) } 65 a[2]="car" as *u8 as i64 66 e_run(a, 3, outp); var n2: i64=e_read_small(outp, obuf, 65536) 67 e_puts(" R2 get car has 'Bob'? " as *u8); if e_contains(obuf,n2,"Bob" as *u8)==1 { pass=pass+1; e_puts("YES PASS\n" as *u8) } else { e_puts("NO FAIL\n" as *u8) } 68 a[2]="savings" as *u8 as i64 69 e_run(a, 3, outp); var n3: i64=e_read_small(outp, obuf, 65536) 70 e_puts(" R3 get savings has 'Carol'? " as *u8); if e_contains(obuf,n3,"Carol" as *u8)==1 { pass=pass+1; e_puts("YES PASS\n" as *u8) } else { e_puts("NO FAIL\n" as *u8) } 71 72 // --- UPDATE house (beneficiary change Alice -> Dave; a new immutable version) --- 73 a[0]="put" as *u8 as i64; a[1]=P as i64; a[2]="house" as *u8 as i64; a[3]="Family home 123 Main St Salt Lake" as *u8 as i64; a[4]="360000" as *u8 as i64; a[5]="Dave" as *u8 as i64 74 e_run(a, 6, outp) 75 76 // R4-R5 SINGLE TRUTH: get house now returns Dave (latest), not Alice (superseded) 77 a[0]="get" as *u8 as i64; a[1]=P as i64; a[2]="house" as *u8 as i64 78 e_run(a, 3, outp); var n4: i64=e_read_small(outp, obuf, 65536) 79 e_puts(" R4 get house now has 'Dave' (latest)? " as *u8); if e_contains(obuf,n4,"Dave" as *u8)==1 { pass=pass+1; e_puts("YES PASS\n" as *u8) } else { e_puts("NO FAIL\n" as *u8) } 80 e_puts(" R5 get house no longer shows 'Alice' (single current truth)? " as *u8); if e_contains(obuf,n4,"Alice" as *u8)==0 { pass=pass+1; e_puts("YES PASS\n" as *u8) } else { e_puts("NO FAIL\n" as *u8) } 81 82 // R6-R7 AUDIT TRAIL: history shows BOTH the new (Dave) and the OLD (Alice) -- nothing destroyed 83 a[0]="history" as *u8 as i64; a[1]=P as i64; a[2]="house" as *u8 as i64 84 e_run(a, 3, outp); var n5: i64=e_read_small(outp, obuf, 65536) 85 e_puts(" R6 history house has 'Dave' (newest)? " as *u8); if e_contains(obuf,n5,"Dave" as *u8)==1 { pass=pass+1; e_puts("YES PASS\n" as *u8) } else { e_puts("NO FAIL\n" as *u8) } 86 e_puts(" R7 history house STILL has 'Alice' (old version NEVER destroyed = audit trail)? " as *u8); if e_contains(obuf,n5,"Alice" as *u8)==1 { pass=pass+1; e_puts("YES PASS\n" as *u8) } else { e_puts("NO FAIL\n" as *u8) } 87 88 // --- FULL INVENTORY: list the whole will (every asset, current state, deduped) --- 89 a[0]="list" as *u8 as i64; a[1]=P as i64 90 e_run(a, 2, outp); var n6: i64=e_read_small(outp, obuf, 65536) 91 e_puts(" R8 list enumerates ALL assets (house+car+savings)? " as *u8) 92 if e_contains(obuf,n6,"house" as *u8)==1 { if e_contains(obuf,n6,"car" as *u8)==1 { if e_contains(obuf,n6,"savings" as *u8)==1 { pass=pass+1; e_puts("YES PASS\n" as *u8) } else { e_puts("NO FAIL\n" as *u8) } } else { e_puts("NO FAIL\n" as *u8) } } else { e_puts("NO FAIL\n" as *u8) } 93 e_puts(" R9 list shows CURRENT state ('Dave' present, 'Alice' gone)? " as *u8) 94 if e_contains(obuf,n6,"Dave" as *u8)==1 { if e_contains(obuf,n6,"Alice" as *u8)==0 { pass=pass+1; e_puts("YES PASS\n" as *u8) } else { e_puts("NO FAIL\n" as *u8) } } else { e_puts("NO FAIL\n" as *u8) } 95 e_puts(" R10 list is DEDUPED/idempotent (assets=3 though house was put twice)? " as *u8) 96 if e_contains(obuf,n6,"assets=3" as *u8)==1 { pass=pass+1; e_puts("YES PASS\n" as *u8) } else { e_puts("NO FAIL\n" as *u8) } 97 98 e_puts("----\nESTATE-INVENTORY rows=" as *u8); e_num(rows); e_puts(" pass=" as *u8); e_num(pass); e_puts("\n" as *u8) 99 let lg: i64=sys_openat_append("knowledge/status/estate_inventory_gate.log" as *u8, 0x1a4) 100 if lg>=0 { e_w(lg, "ESTATE-INVENTORY rows=" as *u8); e_wn(lg, rows); e_w(lg, " pass=" as *u8); e_wn(lg, pass); if pass==rows { e_w(lg, " verdict=GREEN\n" as *u8) } else { e_w(lg, " verdict=RED\n" as *u8) } sys_close(lg) } 101 if pass==rows { e_puts("ESTATE-INVENTORY GREEN (never-lose + single-truth + immutable audit trail = executor-conflict-reducing)\n" as *u8); sys_exit(0); return 0 } 102 e_puts("ESTATE-INVENTORY RED\n" as *u8); sys_exit(1); return 1 103}