nx_auction_proxybid.nx source

1// nx_auction_proxybid.nx -- MANHEIM-BUILD-L1: PROXY BIDDING ("set your max" / automatic bidding, the 2// OVE + Manheim Timed-Sales convenience primitive), COMPOSED on the shared nx_auction_core engine. 3// Sovereign (nx_cc->nxasm, no gcc), pure integer-exact + deterministic. 4// 5// MODEL: each dealer submits a standing MAX (a proxy). proxy_resolve settles the eBay-style second-price 6// outcome: the WINNER is the highest valid max (ties -> earliest submission), and pays the MINIMUM needed 7// to beat the runner-up = min(top1_max, top2_max + increment), floored to the opening, and JUMPED to the 8// reserve when the winner's max covers it. A max below the opening is REJECTED. 9// valid iff start <= t <= end AND max >= opening. 10// out[]: [winner, price, status(1=SOLD/0=NOSALE), accepted, rejected, runnerup_bidder, runnerup_max] 11// 12// EXCEED axis (honest, not yet benched): (1) proxy bidding is SNIPE-IMMUNE BY CONSTRUCTION -- maxes are 13// pre-committed, so there is no last-tick advantage to extend against (the timed channel needs anti-snipe; 14// the proxy channel eliminates the attack); (2) the winner provably pays the minimum to beat the runner-up 15// (Vickrey-fair, auditable, no shill ambiguity). 16// 17// COMPOSITION PROOF: the gate also expands the proxy outcome into the implied concrete 2-bid stream 18// (runner-up @ their max, winner @ the settling price) and feeds it to the SHARED core at_resolve -- 19// asserting the core settles to the SAME winner+price. One settlement engine, two channels. 20// 21// GATE (self-validating): A normal 3-proxy sale (cross-checked vs core), B no-sale (top max < reserve), 22// C neg-control (a below-opening max REJECTED + the reserve-jump when the winner is uncontested). A broken 23// rule diverges a checked value -> verdict=RED. Evidence -> knowledge/status/auction_proxybid.log. 24// license_tier: ORIGINAL 25import "nx_syscalls.nx" 26import "nx_auction_core.nx" 27const PX_MAGIC_1100000: i64 = 1100000 28const PX_MAGIC_1050000: i64 = 1050000 29const PX_MAGIC_950000: i64 = 950000 30const PX_MAGIC_900000: i64 = 900000 31const PX_MAGIC_25000: i64 = 25000 32const PX_MAGIC_1000000: i64 = 1000000 33const PX_MAGIC_925000: i64 = 925000 34const PX_MAGIC_800000: i64 = 800000 35const PX_MAGIC_1075000: i64 = 1075000 36 37const PX_LOG: *u8 = "knowledge/status/auction_proxybid.log" 38 39func px_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 } 40func px_wn(fd: i64, v: i64) -> i64 { let bb: *u8 = sys_mmap(28); var m: i64=v; if m<0 {m=0-m; sys_write(fd,"-" as *u8,1)}; let t: *u8 = sys_mmap(28); var k: i64=0; if m==0 {t[0]=48;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 } 41 42// resolve a proxy (max-bid) auction. writes 7 results into out (see header). 43func proxy_resolve(opening: i64, increment: i64, reserve: i64, start: i64, end: i64, bidder: *i64, maxamt: *i64, time: *i64, n: i64, out: *i64) -> i64 { 44 var top1b: i64 = 0 45 var top1m: i64 = 0 46 var top1t: i64 = 0 47 var top2b: i64 = 0 48 var top2m: i64 = 0 49 var accepted: i64 = 0 50 var rejected: i64 = 0 51 var i: i64 = 0 52 while i < n { 53 let b: i64 = bidder[i] 54 let m: i64 = maxamt[i] 55 let t: i64 = time[i] 56 var valid: i64 = 1 57 if t < start { valid = 0 } 58 if t > end { valid = 0 } 59 if m < opening { valid = 0 } 60 if valid == 1 { 61 accepted = accepted + 1 62 // takes the lead iff a strictly higher max, or an equal max submitted EARLIER (tie -> earlier) 63 var take: i64 = 0 64 if m > top1m { take = 1 } 65 if m == top1m { if t < top1t { take = 1 } } 66 if take == 1 { 67 top2b = top1b; top2m = top1m // demote old leader to runner-up 68 top1b = b; top1m = m; top1t = t 69 } else { 70 if m > top2m { top2b = b; top2m = m } 71 } 72 } else { 73 rejected = rejected + 1 74 } 75 i = i + 1 76 } 77 var price: i64 = opening 78 if top2m > 0 { 79 let p2: i64 = top2m + increment 80 if p2 < top1m { price = p2 } else { price = top1m } 81 if price < opening { price = opening } 82 } 83 var status: i64 = AT_NOSALE 84 var winner: i64 = 0 85 if top1m >= reserve { 86 status = AT_SOLD 87 winner = top1b 88 if price < reserve { price = reserve } // reserve jump: winner's max covers it 89 } else { 90 price = 0 91 } 92 out[0] = winner 93 out[1] = price 94 out[2] = status 95 out[3] = accepted 96 out[4] = rejected 97 out[5] = top2b 98 out[6] = top2m 99 return 0 100} 101 102func main() -> i64 { 103 let bidder: *i64 = sys_mmap(8 * 16) as *i64 104 let maxamt: *i64 = sys_mmap(8 * 16) as *i64 105 let time: *i64 = sys_mmap(8 * 16) as *i64 106 let out: *i64 = sys_mmap(8 * 8) as *i64 107 // cross-check scratch (feeds the shared core) 108 let cb: *i64 = sys_mmap(8 * 4) as *i64 109 let ca: *i64 = sys_mmap(8 * 4) as *i64 110 let ct: *i64 = sys_mmap(8 * 4) as *i64 111 let o2: *i64 = sys_mmap(8 * 8) as *i64 112 113 // --- Scenario A: 3 proxies, second-price settlement (opening 900000, incr 25000, reserve 1000000) --- 114 bidder[0]=1; maxamt[0]=PX_MAGIC_1100000; time[0]=110 115 bidder[1]=2; maxamt[1]=PX_MAGIC_1050000; time[1]=120 116 bidder[2]=3; maxamt[2]=PX_MAGIC_950000; time[2]=130 117 proxy_resolve(PX_MAGIC_900000, PX_MAGIC_25000, PX_MAGIC_1000000, 100, 200, bidder, maxamt, time, 3, out) 118 let aw: i64 = out[0]; let ap: i64 = out[1]; let as_: i64 = out[2]; let aacc: i64 = out[3]; let arej: i64 = out[4] 119 let arub: i64 = out[5]; let arum: i64 = out[6] 120 121 // COMPOSITION PROOF: expand A to the implied concrete stream + settle via the SHARED core engine. 122 cb[0]=arub; ca[0]=arum; ct[0]=150 // runner-up bids their max 123 cb[1]=aw; ca[1]=ap; ct[1]=151 // winner bids the settling price 124 at_resolve(PX_MAGIC_900000, PX_MAGIC_25000, PX_MAGIC_1000000, 100, 200, 0, 0, cb, ca, ct, 2, o2) 125 let xw: i64 = o2[0]; let xp: i64 = o2[1]; let xs: i64 = o2[2] 126 127 // --- Scenario B: no-sale (every max below reserve) --- 128 bidder[0]=1; maxamt[0]=PX_MAGIC_950000; time[0]=110 129 bidder[1]=2; maxamt[1]=PX_MAGIC_925000; time[1]=120 130 proxy_resolve(PX_MAGIC_900000, PX_MAGIC_25000, PX_MAGIC_1000000, 100, 200, bidder, maxamt, time, 2, out) 131 let bw: i64 = out[0]; let bs: i64 = out[2]; let bacc: i64 = out[3] 132 133 // --- Control C: a below-opening max REJECTED + reserve-jump for the uncontested winner --- 134 bidder[0]=1; maxamt[0]=PX_MAGIC_1100000; time[0]=110 135 bidder[1]=2; maxamt[1]=PX_MAGIC_800000; time[1]=120 // PX_MAGIC_800000 < opening PX_MAGIC_900000 -> rejected 136 proxy_resolve(PX_MAGIC_900000, PX_MAGIC_25000, PX_MAGIC_1000000, 100, 200, bidder, maxamt, time, 2, out) 137 let cw: i64 = out[0]; let cp: i64 = out[1]; let cs: i64 = out[2]; let cacc: i64 = out[3]; let crej: i64 = out[4] 138 139 // --- assertions (tight, hand-computed) --- 140 var ok: i64 = 1 141 // A: SOLD to bidder 1 at runner-up(1050000)+increment(25000)=1075000, 3 accepted / 0 rejected 142 if aw != 1 { ok = 0 } 143 if ap != PX_MAGIC_1075000 { ok = 0 } 144 if as_ != AT_SOLD { ok = 0 } 145 if aacc != 3 { ok = 0 } 146 if arej != 0 { ok = 0 } 147 // A composition: the shared core settles the expanded stream to the SAME winner+price+status 148 if xw != aw { ok = 0 } 149 if xp != ap { ok = 0 } 150 if xs != as_ { ok = 0 } 151 // B: NO-SALE (top max 950000 < reserve 1000000), 2 accepted 152 if bw != 0 { ok = 0 } 153 if bs != AT_NOSALE { ok = 0 } 154 if bacc != 2 { ok = 0 } 155 // C: below-opening REJECTED -> 1 accepted / 1 rejected; uncontested winner reserve-JUMPS to 1000000 156 if cw != 1 { ok = 0 } 157 if cp != PX_MAGIC_1000000 { ok = 0 } 158 if cs != AT_SOLD { ok = 0 } 159 if cacc != 1 { ok = 0 } 160 if crej != 1 { ok = 0 } 161 if cp == PX_MAGIC_900000 { ok = 0 } // reserve jump MUST have moved price off the opening (rule-sensitivity) 162 163 px_w(1, "PROXYGATE engine=nx_auction_proxybid A{winner=" as *u8); px_wn(1, aw) 164 px_w(1, " price=" as *u8); px_wn(1, ap); px_w(1, " status=" as *u8); px_wn(1, as_) 165 px_w(1, " acc=" as *u8); px_wn(1, aacc); px_w(1, " rej=" as *u8); px_wn(1, arej) 166 px_w(1, "} core-crosscheck{winner=" as *u8); px_wn(1, xw); px_w(1, " price=" as *u8); px_wn(1, xp) 167 px_w(1, " agree=" as *u8); if xw == aw { if xp == ap { px_wn(1, 1) } else { px_wn(1, 0) } } else { px_wn(1, 0) } 168 px_w(1, "} B{winner=" as *u8); px_wn(1, bw); px_w(1, " status=" as *u8); px_wn(1, bs) 169 px_w(1, "} C{winner=" as *u8); px_wn(1, cw); px_w(1, " price=" as *u8); px_wn(1, cp) 170 px_w(1, " rej=" as *u8); px_wn(1, crej); px_w(1, "}" as *u8) 171 if ok == 1 { px_w(1, " verdict=GREEN\n" as *u8) } else { px_w(1, " verdict=RED\n" as *u8) } 172 173 let lf: i64 = sys_openat_append(PX_LOG, 420) 174 if lf >= 0 { 175 px_w(lf, "PROXYGATE engine=nx_auction_proxybid A{winner=" as *u8); px_wn(lf, aw) 176 px_w(lf, " price=" as *u8); px_wn(lf, ap); px_w(lf, " acc=" as *u8); px_wn(lf, aacc) 177 px_w(lf, " rej=" as *u8); px_wn(lf, arej); px_w(lf, "} core-agree=" as *u8) 178 if xw == aw { if xp == ap { px_wn(lf, 1) } else { px_wn(lf, 0) } } else { px_wn(lf, 0) } 179 px_w(lf, " B{winner=" as *u8); px_wn(lf, bw); px_w(lf, " status=" as *u8); px_wn(lf, bs) 180 px_w(lf, "} C{winner=" as *u8); px_wn(lf, cw); px_w(lf, " price=" as *u8); px_wn(lf, cp) 181 px_w(lf, " rej=" as *u8); px_wn(lf, crej); px_w(lf, "}" as *u8) 182 if ok == 1 { px_w(lf, " verdict=GREEN\n" as *u8) } else { px_w(lf, " verdict=RED\n" as *u8) } 183 sys_close(lf) 184 } 185 186 if ok == 1 { return 0 } 187 return 1 188}