nx_share_convergence_gate.nx source

1// nx_share_convergence_gate.nx -- THE DEDUP PROOF. I built nx_share_plane as a new who-may-see-what 2// primitive and only afterwards found runtime/nx_rebac.nx, which calls itself "the ONE shared authorization 3// plane for every Nishi surface" and exists precisely because the estate once had three incompatible authz 4// philosophies. Mine would be a fourth. The irony is exact: nx_share_plane's whole justification was that 5// shared gallery, shared contacts and gifts must not become three copies of one permission rule. 6// 7// The estate's law is to RETIRE a duplicate by PROVING CONVERGENCE, not by asserting redundancy. So this 8// gate runs the SAME scenarios through both planes and compares verdicts, and it is deliberately built so 9// that agreement is not the only outcome it can report: 10// * an UNDECLARED divergence turns the gate RED -- two planes that disagree about who may see a photo is 11// a privacy bug wearing a refactor's clothes; 12// * a DECLARED divergence is printed with its reason and does NOT fail, because the point of the exercise 13// is to find them. Two are declared below, and each one changes what "retire the duplicate" means. 14// A gate that could only ever say "they agree" would prove nothing about a decision this consequential. 15// license_tier: ORIGINAL expect_exit: 0 16import "nx_rebac.nx" 17import "nx_share_plane.nx" 18 19const CV_CAP: i64 = 64 20const CV_ALICE: i64 = 1001 21const CV_BOB: i64 = 1002 22const CV_CARA: i64 = 1003 23const CV_ALBUM: i64 = 7001 24 25func c_w(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 } 26func c_n(v: i64) -> i64 { 27 let bb: *u8=sys_mmap(28); var m: i64=v 28 if m<0 { m=0-m; sys_write(1,"-" as *u8,1) } 29 let t: *u8=sys_mmap(28); var k: i64=0 30 if m==0 { t[0]=48 as u8; k=1 } 31 while m>0 { t[k]=(48+(m%10)) as u8; m=m/10; k=k+1 } 32 var i: i64=0 33 while i<k { bb[i]=t[k-1-i]; i=i+1 } 34 sys_write(1,bb,k); return 0 35} 36// compare one scenario across both planes. declared=1 means "these are KNOWN to differ and here is why". 37func cv(label: *u8, mine: i64, theirs: i64, declared: i64, why: *u8, agree: *i64, div: *i64, fails: *i64) -> i64 { 38 c_w(" " as *u8); c_w(label) 39 c_w(" share_plane=" as *u8); c_n(mine) 40 c_w(" rebac=" as *u8); c_n(theirs) 41 if mine==theirs { 42 agree[0]=agree[0]+1 43 c_w(" AGREE\n" as *u8) 44 return 0 45 } 46 div[0]=div[0]+1 47 if declared==1 { 48 c_w(" DIVERGE (declared): " as *u8); c_w(why); c_w("\n" as *u8) 49 return 0 50 } 51 fails[0]=fails[0]+1 52 c_w(" DIVERGE (UNDECLARED -- RED): " as *u8); c_w(why); c_w("\n" as *u8) 53 return 0 54} 55func arena() -> *i64 { 56 let a: *i64 = sys_mmap(8*sp_slots_needed(CV_CAP)) as *i64 57 sp_init(a, CV_CAP) 58 return a 59} 60// a fresh isolated seg_store prefix per scenario, so one scenario's tuples cannot leak into the next 61func pfx(tag: i64) -> *u8 { 62 let p: *u8 = sys_mmap(128); var o: i64 = 0 63 o = rb_cat(p, o, "/tmp/shconv_" as *u8); o = rb_catn(p, o, sys_now_us()) 64 o = rb_cat(p, o, "_" as *u8); o = rb_catn(p, o, tag); o = rb_cat(p, o, "_" as *u8) 65 p[o] = 0 as u8 66 return p 67} 68 69func main() -> i64 { 70 let fails: *i64 = sys_mmap(16) as *i64 71 let agree: *i64 = sys_mmap(16) as *i64 72 let div: *i64 = sys_mmap(16) as *i64 73 fails[0]=0; agree[0]=0; div[0]=0 74 c_w("=== nx_share_convergence_gate -- does nx_share_plane duplicate nx_rebac, and exactly where? ===\n" as *u8) 75 c_w("mapping: album -> doc:album1 | actor N -> user:aliceN | SP_VIEW -> perm 'view' | SP_ADMIN -> relation 'owner'\n" as *u8) 76 77 // C1 -- an unclaimed resource shows nothing to anybody 78 let a1: *i64 = arena() 79 let p1: *u8 = pfx(1) 80 cv("C1 unowned, stranger asks view " as *u8, 81 sp_may(a1, CV_BOB, SP_C_ALBUM, CV_ALBUM, SP_VIEW), 82 rb_check(p1, "user:bob" as *u8, "view" as *u8, "doc:album1" as *u8, 0), 83 0, "deny-by-default must hold in both" as *u8, agree, div, fails) 84 85 // C2 -- the owner sees their own resource with no grant row in existence 86 let a2: *i64 = arena() 87 let p2: *u8 = pfx(2) 88 sp_claim(a2, CV_ALICE, SP_C_ALBUM, CV_ALBUM) 89 rb_put(p2, "doc:album1" as *u8, "owner" as *u8, "user:alice" as *u8, "system" as *u8, 1) 90 cv("C2 owner views own album " as *u8, 91 sp_may(a2, CV_ALICE, SP_C_ALBUM, CV_ALBUM, SP_VIEW), 92 rb_check(p2, "user:alice" as *u8, "view" as *u8, "doc:album1" as *u8, 0), 93 0, "ownership must imply access in both" as *u8, agree, div, fails) 94 95 // C3 -- a stranger still sees nothing after the claim 96 cv("C3 stranger views a claimed album " as *u8, 97 sp_may(a2, CV_BOB, SP_C_ALBUM, CV_ALBUM, SP_VIEW), 98 rb_check(p2, "user:bob" as *u8, "view" as *u8, "doc:album1" as *u8, 0), 99 0, "claiming must not open the resource to everyone" as *u8, agree, div, fails) 100 101 // C4 -- a grant is what makes a stranger a viewer 102 let a4: *i64 = arena() 103 let p4: *u8 = pfx(4) 104 sp_claim(a4, CV_ALICE, SP_C_ALBUM, CV_ALBUM) 105 sp_grant(a4, CV_ALICE, CV_BOB, SP_C_ALBUM, CV_ALBUM, SP_VIEW) 106 rb_put(p4, "doc:album1" as *u8, "owner" as *u8, "user:alice" as *u8, "system" as *u8, 1) 107 rb_put(p4, "doc:album1" as *u8, "viewer" as *u8, "user:bob" as *u8, "user:alice" as *u8, 1) 108 cv("C4 granted viewer views " as *u8, 109 sp_may(a4, CV_BOB, SP_C_ALBUM, CV_ALBUM, SP_VIEW), 110 rb_check(p4, "user:bob" as *u8, "view" as *u8, "doc:album1" as *u8, 0), 111 0, "a grant must take effect in both" as *u8, agree, div, fails) 112 113 // C5 -- revocation is total, and in both planes it APPENDS rather than erases 114 let a5: *i64 = arena() 115 let p5: *u8 = pfx(5) 116 sp_claim(a5, CV_ALICE, SP_C_ALBUM, CV_ALBUM) 117 sp_grant(a5, CV_ALICE, CV_BOB, SP_C_ALBUM, CV_ALBUM, SP_VIEW) 118 sp_revoke(a5, CV_ALICE, CV_BOB, SP_C_ALBUM, CV_ALBUM) 119 rb_put(p5, "doc:album1" as *u8, "owner" as *u8, "user:alice" as *u8, "system" as *u8, 1) 120 rb_put(p5, "doc:album1" as *u8, "viewer" as *u8, "user:bob" as *u8, "user:alice" as *u8, 1) 121 rb_put(p5, "doc:album1" as *u8, "viewer" as *u8, "user:bob" as *u8, "user:alice" as *u8, 0) 122 cv("C5 revoked viewer views " as *u8, 123 sp_may(a5, CV_BOB, SP_C_ALBUM, CV_ALBUM, SP_VIEW), 124 rb_check(p5, "user:bob" as *u8, "view" as *u8, "doc:album1" as *u8, 0), 125 0, "a tombstone must win over the grant it revokes, in both" as *u8, agree, div, fails) 126 127 // C6 -- grant, revoke, grant again: the LAST write is the one that counts 128 let a6: *i64 = arena() 129 let p6: *u8 = pfx(6) 130 sp_claim(a6, CV_ALICE, SP_C_ALBUM, CV_ALBUM) 131 sp_grant(a6, CV_ALICE, CV_BOB, SP_C_ALBUM, CV_ALBUM, SP_VIEW) 132 sp_revoke(a6, CV_ALICE, CV_BOB, SP_C_ALBUM, CV_ALBUM) 133 sp_grant(a6, CV_ALICE, CV_BOB, SP_C_ALBUM, CV_ALBUM, SP_VIEW) 134 rb_put(p6, "doc:album1" as *u8, "owner" as *u8, "user:alice" as *u8, "system" as *u8, 1) 135 rb_put(p6, "doc:album1" as *u8, "viewer" as *u8, "user:bob" as *u8, "user:alice" as *u8, 1) 136 rb_put(p6, "doc:album1" as *u8, "viewer" as *u8, "user:bob" as *u8, "user:alice" as *u8, 0) 137 rb_put(p6, "doc:album1" as *u8, "viewer" as *u8, "user:bob" as *u8, "user:alice" as *u8, 1) 138 cv("C6 grant-revoke-grant " as *u8, 139 sp_may(a6, CV_BOB, SP_C_ALBUM, CV_ALBUM, SP_VIEW), 140 rb_check(p6, "user:bob" as *u8, "view" as *u8, "doc:album1" as *u8, 0), 141 0, "latest-wins must be the rule in both" as *u8, agree, div, fails) 142 143 // C7 -- a plain viewer must not be able to re-share (the escalation both planes exist to stop) 144 let a7: *i64 = arena() 145 let p7: *u8 = pfx(7) 146 sp_claim(a7, CV_ALICE, SP_C_ALBUM, CV_ALBUM) 147 sp_grant(a7, CV_ALICE, CV_BOB, SP_C_ALBUM, CV_ALBUM, SP_VIEW) 148 rb_put(p7, "doc:album1" as *u8, "owner" as *u8, "user:alice" as *u8, "system" as *u8, 1) 149 rb_put(p7, "doc:album1" as *u8, "viewer" as *u8, "user:bob" as *u8, "user:alice" as *u8, 1) 150 var mine7: i64 = 0 151 if sp_grant(a7, CV_BOB, CV_CARA, SP_C_ALBUM, CV_ALBUM, SP_VIEW) > 0 { mine7 = 1 } 152 cv("C7 viewer tries to re-share " as *u8, 153 mine7, 154 rb_may_grant(p7, "user:bob" as *u8, "doc:album1" as *u8), 155 0, "no transitive escalation from VIEW, in either plane" as *u8, agree, div, fails) 156 157 // ---- DECLARED DIVERGENCE 1: an UNCLAIMED object ---- 158 // nx_rebac deliberately lets ANYONE make the first grant on an object with no owner tuple, as a 159 // bootstrap path. nx_share_plane refuses (SP_E_NOOWNER) and requires an explicit claim first. Neither 160 // is wrong in the abstract, but they are not the same rule, and for family photos the stricter one is 161 // the one I want: an album nobody has claimed should not be shareable by a passer-by. 162 let a8: *i64 = arena() 163 let p8: *u8 = pfx(8) 164 var mine8: i64 = 0 165 if sp_grant(a8, CV_BOB, CV_CARA, SP_C_ALBUM, CV_ALBUM, SP_VIEW) > 0 { mine8 = 1 } 166 cv("C8 grant on an UNCLAIMED object " as *u8, 167 mine8, 168 rb_may_grant(p8, "user:bob" as *u8, "doc:album1" as *u8), 169 1, "rebac allows a bootstrap first-grant on an ownerless object; share_plane requires an explicit claim. Keep the strict rule for media: claim at creation." as *u8, 170 agree, div, fails) 171 172 // ---- DECLARED DIVERGENCE 2: DELEGATED re-share ---- 173 // nx_share_plane has an explicit ADMIN bit that lets the owner delegate re-sharing. nx_rebac's doc 174 // rewrite table maps manage -> owner ONLY, so under the doc type nobody but the owner can ever grant. 175 // That is a capability nx_rebac's DATA does not currently express for docs -- which means retiring my 176 // plane is not a pure deletion: this rule has to survive, as a rewrite-table row rather than as code. 177 let a9: *i64 = arena() 178 let p9: *u8 = pfx(9) 179 sp_claim(a9, CV_ALICE, SP_C_ALBUM, CV_ALBUM) 180 sp_grant(a9, CV_ALICE, CV_BOB, SP_C_ALBUM, CV_ALBUM, SP_VIEW+SP_ADMIN) 181 rb_put(p9, "doc:album1" as *u8, "owner" as *u8, "user:alice" as *u8, "system" as *u8, 1) 182 rb_put(p9, "doc:album1" as *u8, "editor" as *u8, "user:bob" as *u8, "user:alice" as *u8, 1) 183 var mine9: i64 = 0 184 if sp_grant(a9, CV_BOB, CV_CARA, SP_C_ALBUM, CV_ALBUM, SP_VIEW) > 0 { mine9 = 1 } 185 cv("C9 delegated re-share (ADMIN bit) " as *u8, 186 mine9, 187 rb_may_grant(p9, "user:bob" as *u8, "doc:album1" as *u8), 188 1, "share_plane can delegate re-sharing via an explicit ADMIN bit; rebac's doc rewrite says manage=owner only. Migrating means adding the row, not dropping the rule." as *u8, 189 agree, div, fails) 190 191 c_w("\n scenarios=9 AGREE=" as *u8); c_n(agree[0]) 192 c_w(" DIVERGE=" as *u8); c_n(div[0]) 193 c_w(" undeclared(RED)=" as *u8); c_n(fails[0]); c_w("\n" as *u8) 194 c_w(" READING: the overlapping half is REDUNDANT and must be retired onto nx_rebac. The two declared\n" as *u8) 195 c_w(" divergences are the migration's actual work: keep claim-before-share, and carry delegated\n" as *u8) 196 c_w(" re-sharing across as a rewrite-table row. The GIFT half (ownership transfer + provenance) is in\n" as *u8) 197 c_w(" neither plane's overlap and is the only part that was genuinely new.\n" as *u8) 198 if fails[0]==0 { 199 c_w("VERDICT: verdict=GREEN (convergence proven where it matters; every divergence named, none silent)\n" as *u8) 200 sys_exit(0) 201 } 202 c_w("VERDICT: RED (an UNDECLARED divergence -- two planes disagreeing about who may see what)\n" as *u8) 203 sys_exit(1) 204 return 1 205}