code wiki / _hdl_build / nx_pkg_solve.nx
nx_pkg_solve.nx source
↩ module page · 190 lines · 13564 B
1// nx_pkg_solve.nx -- GATE: VERSION-CONSTRAINT DEPENDENCY SOLVING (closes the PACKAGE-MGMT census gap "version-
2// constraint solving"). Reworks nx_pkg (transitive-closure + topo + sha) with the piece it lacked: a real
3// BACKTRACKING resolver over a package UNIVERSE where each package has multiple VERSIONS and each (package,version)
4// declares dependency CONSTRAINTS (semver: exact / >= / caret ^ / tilde ~ / range). Grounded on the banked field
5// research (pp_semver/pp_dephell/pp_sat/pp_backtracking): pick a version of every needed package satisfying ALL
6// dependents' constraints jointly; backtrack on conflict; report unsatisfiable. Complete search, highest-version-
7// first => deterministic (lockfile-stable). Constraints held as inclusive [lo,hi] intervals over encoded versions.
8// T1 DIAMOND: App->B^1,C^1; B->D>=1.2; C->D in[1.5,2.0) -> D resolves to the HIGHEST feasible (1.9.0) via intersection.
9// T2 BACKTRACK: App->B(any),D=1.3.0; B2.0.0->D>=1.5.0 (fails D=1.3.0) -> solver BACKTRACKS to B1.0.0 (the lower ver).
10// T3 CONFLICT: B->D<2.0.0, C->D>=2.0.0 -> UNSATISFIABLE detected (no version of D satisfies both).
11// T4 teeth: the semver operators (exact/gte/caret/tilde) map to the correct intervals (KATs).
12// T5 determinism: the diamond solved twice -> identical selection (reproducible / lockfile-stable).
13// expect_exit: 0 Sovereign: nx_syscalls. NEVER-BRICK: pure resolution, writes 0 firmware.
14import "nx_syscalls.nx"
15import "nx_itoa_lib.nx" // shared MSB-first emitter (zero-alloc)
16const K_MAGIC_1000000: i64 = 1000000
17
18func g_puts(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 }
19// MIGRATED to the shared emitter (debt 1785563586). The old body mmapped a scratch buffer
20// per call and never freed it. At PAGE granularity that is 4096B leaked PER CALL -- the
21// defect that took 28.5GB of a 36GB host in nx_ts_lumadiff (2MB input, ~3.66M calls).
22// nxi_* is MSB-first, allocates NOTHING, and emits identical bytes including the sign.
23func g_pn(v: i64) -> i64 { nxi_out(v); return 0 }
24func ck(name: *u8, c: i64) -> i64 { if c==1 { g_puts(" PASS " as *u8) } else { g_puts(" FAIL " as *u8) } g_puts(name); g_puts("\n" as *u8); return c }
25
26const MAXV: i64 = 4
27const BIG: i64 = 999999999
28// encode major.minor.patch as a single comparable int
29func ver(maj: i64, min: i64, pat: i64) -> i64 { return maj*K_MAGIC_1000000 + min*1000 + pat }
30
31struct Univ {
32 NP: i64,
33 nver: *i64, // nver[p] = #versions of package p
34 vers: *i64, // vers[p*MAXV + j] = encoded version, DESCENDING (j=0 highest)
35 nreq: i64,
36 rSrc: *i64, // requirement r: if package rSrc[r] is at version-INDEX rSrcV[r] ...
37 rSrcV: *i64,
38 rDep: *i64, // ... then package rDep[r] must be within [rLo[r], rHi[r]]
39 rLo: *i64,
40 rHi: *i64,
41 nroot: i64,
42 rootDep: *i64, // always-on root constraints: package rootDep[r] within [rootLo[r], rootHi[r]]
43 rootLo: *i64,
44 rootHi: *i64,
45}
46
47// consistency of a (possibly partial) selection: every ACTIVE constraint whose target is assigned must hold.
48func feasible(u: *Univ, sel: *i64) -> i64 {
49 let NP: i64=u.NP; let vers: *i64=u.vers
50 let nroot: i64=u.nroot; let rootDep: *i64=u.rootDep; let rootLo: *i64=u.rootLo; let rootHi: *i64=u.rootHi
51 var r: i64=0
52 while r<nroot {
53 let dp: i64=rootDep[r]
54 if sel[dp] != (0-1) { let v: i64=vers[dp*MAXV+sel[dp]]; if v<rootLo[r] { return 0 } if v>rootHi[r] { return 0 } }
55 r=r+1
56 }
57 let nreq: i64=u.nreq; let rSrc: *i64=u.rSrc; let rSrcV: *i64=u.rSrcV; let rDep: *i64=u.rDep; let rLo: *i64=u.rLo; let rHi: *i64=u.rHi
58 var q: i64=0
59 while q<nreq {
60 let sp: i64=rSrc[q]
61 if sel[sp]==rSrcV[q] { // this requirement's source version is the chosen one -> active
62 let dp: i64=rDep[q]
63 if sel[dp] != (0-1) { let v: i64=vers[dp*MAXV+sel[dp]]; if v<rLo[q] { return 0 } if v>rHi[q] { return 0 } }
64 }
65 q=q+1
66 }
67 return 1
68}
69// backtracking search: assign a version to each package (highest first), prune inconsistent partials, first
70// complete feasible assignment wins (deterministic). Returns 1 (sel filled) or 0 (unsatisfiable).
71func solve(u: *Univ, idx: i64, sel: *i64) -> i64 {
72 let NP: i64=u.NP; let nver: *i64=u.nver
73 if idx==NP { return feasible(u, sel) }
74 var j: i64=0
75 while j<nver[idx] {
76 sel[idx]=j
77 if feasible(u, sel)==1 { if solve(u, idx+1, sel)==1 { return 1 } }
78 j=j+1
79 }
80 sel[idx]=0-1
81 return 0
82}
83func mk(np: i64, nver: *i64, vers: *i64, nreq: i64, rs: *i64, rsv: *i64, rd: *i64, rl: *i64, rh: *i64, nroot: i64, rod: *i64, rol: *i64, roh: *i64) -> *Univ {
84 let u: *Univ = sys_mmap(256) as *Univ
85 u.NP=np; u.nver=nver; u.vers=vers; u.nreq=nreq; u.rSrc=rs; u.rSrcV=rsv; u.rDep=rd; u.rLo=rl; u.rHi=rh; u.nroot=nroot; u.rootDep=rod; u.rootLo=rol; u.rootHi=roh
86 return u
87}
88func chosen(u: *Univ, sel: *i64, p: i64) -> i64 { if sel[p]==(0-1) { return 0-1 } return u.vers[p*MAXV+sel[p]] }
89
90func main() -> i64 {
91 g_puts("nx_pkg_solve (VERSION-CONSTRAINT solver: semver intervals + backtracking resolver + conflict detection)\n" as *u8)
92 var pass: i64=0; var total: i64=0
93
94 // ===== Instance 1: DIAMOND. App0, B1, C2, D3 =====
95 let d_nver: *i64=sys_mmap(4*8) as *i64; let d_vers: *i64=sys_mmap(4*MAXV*8) as *i64
96 d_nver[0]=1; d_vers[0*MAXV+0]=ver(1,0,0) // App 1.0.0
97 d_nver[1]=1; d_vers[1*MAXV+0]=ver(1,0,0) // B 1.0.0
98 d_nver[2]=1; d_vers[2*MAXV+0]=ver(1,0,0) // C 1.0.0
99 d_nver[3]=4; d_vers[3*MAXV+0]=ver(1,9,0); d_vers[3*MAXV+1]=ver(1,5,0); d_vers[3*MAXV+2]=ver(1,3,0); d_vers[3*MAXV+3]=ver(1,0,0) // D: 1.9,1.5,1.3,1.0
100 // reqs: (B,v0)->D >=1.2.0 ; (C,v0)->D in [1.5.0, 1.999999] (caret 1.x, i.e. <2.0.0 AND >=1.5.0)
101 let d_rs: *i64=sys_mmap(2*8) as *i64; let d_rsv: *i64=sys_mmap(2*8) as *i64; let d_rd: *i64=sys_mmap(2*8) as *i64; let d_rl: *i64=sys_mmap(2*8) as *i64; let d_rh: *i64=sys_mmap(2*8) as *i64
102 d_rs[0]=1; d_rsv[0]=0; d_rd[0]=3; d_rl[0]=ver(1,2,0); d_rh[0]=BIG
103 d_rs[1]=2; d_rsv[1]=0; d_rd[1]=3; d_rl[1]=ver(1,5,0); d_rh[1]=ver(1,999,999)
104 // root: App exact 1.0.0 ; App needs B in [1.0.0,1.999999] (^1) ; App needs C in [1.0.0,1.999999] (^1)
105 let d_rod: *i64=sys_mmap(3*8) as *i64; let d_rol: *i64=sys_mmap(3*8) as *i64; let d_roh: *i64=sys_mmap(3*8) as *i64
106 d_rod[0]=0; d_rol[0]=ver(1,0,0); d_roh[0]=ver(1,0,0)
107 d_rod[1]=1; d_rol[1]=ver(1,0,0); d_roh[1]=ver(1,999,999)
108 d_rod[2]=2; d_rol[2]=ver(1,0,0); d_roh[2]=ver(1,999,999)
109 let U1: *Univ=mk(4, d_nver, d_vers, 2, d_rs, d_rsv, d_rd, d_rl, d_rh, 3, d_rod, d_rol, d_roh)
110 let sel1: *i64=sys_mmap(4*8) as *i64; var z: i64=0; while z<4 { sel1[z]=0-1; z=z+1 }
111 let ok1: i64=solve(U1, 0, sel1)
112 let dver: i64=chosen(U1, sel1, 3)
113 g_puts(" T1 diamond: solved="); g_pn(ok1); g_puts(" D="); g_pn(dver); g_puts(" (expect 1009000=1.9.0, the highest in [1.5,2.0) )\n" as *u8)
114 var t1: i64=0; if ok1==1 { if dver==ver(1,9,0) { if chosen(U1,sel1,1)==ver(1,0,0) { if chosen(U1,sel1,2)==ver(1,0,0) { t1=1 } } } }
115 pass=pass+ck("T1: DIAMOND resolves -- D = highest version satisfying BOTH B and C (intersection -> 1.9.0)" as *u8, t1); total=total+1
116
117 // ===== Instance 2: BACKTRACK. App0, B1, D2 =====
118 let b_nver: *i64=sys_mmap(3*8) as *i64; let b_vers: *i64=sys_mmap(3*MAXV*8) as *i64
119 b_nver[0]=1; b_vers[0*MAXV+0]=ver(1,0,0)
120 b_nver[1]=2; b_vers[1*MAXV+0]=ver(2,0,0); b_vers[1*MAXV+1]=ver(1,0,0) // B: 2.0.0 (highest), 1.0.0
121 b_nver[2]=3; b_vers[2*MAXV+0]=ver(1,5,0); b_vers[2*MAXV+1]=ver(1,3,0); b_vers[2*MAXV+2]=ver(1,0,0) // D: 1.5,1.3,1.0
122 // reqs: (B,2.0.0=v0)->D>=1.5.0 ; (B,1.0.0=v1)->D>=1.0.0
123 let b_rs: *i64=sys_mmap(2*8) as *i64; let b_rsv: *i64=sys_mmap(2*8) as *i64; let b_rd: *i64=sys_mmap(2*8) as *i64; let b_rl: *i64=sys_mmap(2*8) as *i64; let b_rh: *i64=sys_mmap(2*8) as *i64
124 b_rs[0]=1; b_rsv[0]=0; b_rd[0]=2; b_rl[0]=ver(1,5,0); b_rh[0]=BIG
125 b_rs[1]=1; b_rsv[1]=1; b_rd[1]=2; b_rl[1]=ver(1,0,0); b_rh[1]=BIG
126 // root: App exact ; App needs B (any >=1.0.0) ; App needs D EXACT 1.3.0
127 let b_rod: *i64=sys_mmap(3*8) as *i64; let b_rol: *i64=sys_mmap(3*8) as *i64; let b_roh: *i64=sys_mmap(3*8) as *i64
128 b_rod[0]=0; b_rol[0]=ver(1,0,0); b_roh[0]=ver(1,0,0)
129 b_rod[1]=1; b_rol[1]=ver(1,0,0); b_roh[1]=BIG
130 b_rod[2]=2; b_rol[2]=ver(1,3,0); b_roh[2]=ver(1,3,0)
131 let U2: *Univ=mk(3, b_nver, b_vers, 2, b_rs, b_rsv, b_rd, b_rl, b_rh, 3, b_rod, b_rol, b_roh)
132 let sel2: *i64=sys_mmap(3*8) as *i64; z=0; while z<3 { sel2[z]=0-1; z=z+1 }
133 let ok2: i64=solve(U2, 0, sel2)
134 let bver: i64=chosen(U2, sel2, 1); let bdver: i64=chosen(U2, sel2, 2)
135 g_puts(" T2 backtrack: solved="); g_pn(ok2); g_puts(" B="); g_pn(bver); g_puts(" (expect 1000000=1.0.0, NOT the higher 2.0.0) D="); g_pn(bdver); g_puts("\n" as *u8)
136 var t2: i64=0; if ok2==1 { if bver==ver(1,0,0) { if bdver==ver(1,3,0) { t2=1 } } }
137 pass=pass+ck("T2: BACKTRACK -- highest B(2.0.0) conflicts with D=1.3.0 so the solver picks the LOWER B(1.0.0)" as *u8, t2); total=total+1
138
139 // ===== Instance 3: CONFLICT (unsatisfiable). App0, B1, C2, D3 =====
140 let c_nver: *i64=sys_mmap(4*8) as *i64; let c_vers: *i64=sys_mmap(4*MAXV*8) as *i64
141 c_nver[0]=1; c_vers[0*MAXV+0]=ver(1,0,0)
142 c_nver[1]=1; c_vers[1*MAXV+0]=ver(1,0,0)
143 c_nver[2]=1; c_vers[2*MAXV+0]=ver(1,0,0)
144 c_nver[3]=3; c_vers[3*MAXV+0]=ver(2,0,0); c_vers[3*MAXV+1]=ver(1,5,0); c_vers[3*MAXV+2]=ver(1,2,0) // D: 2.0,1.5,1.2
145 // reqs: (B,v0)->D in [1.2.0,1.999999] (<2.0.0) ; (C,v0)->D>=2.0.0
146 let c_rs: *i64=sys_mmap(2*8) as *i64; let c_rsv: *i64=sys_mmap(2*8) as *i64; let c_rd: *i64=sys_mmap(2*8) as *i64; let c_rl: *i64=sys_mmap(2*8) as *i64; let c_rh: *i64=sys_mmap(2*8) as *i64
147 c_rs[0]=1; c_rsv[0]=0; c_rd[0]=3; c_rl[0]=ver(1,2,0); c_rh[0]=ver(1,999,999)
148 c_rs[1]=2; c_rsv[1]=0; c_rd[1]=3; c_rl[1]=ver(2,0,0); c_rh[1]=BIG
149 let c_rod: *i64=sys_mmap(3*8) as *i64; let c_rol: *i64=sys_mmap(3*8) as *i64; let c_roh: *i64=sys_mmap(3*8) as *i64
150 c_rod[0]=0; c_rol[0]=ver(1,0,0); c_roh[0]=ver(1,0,0)
151 c_rod[1]=1; c_rol[1]=ver(1,0,0); c_roh[1]=ver(1,999,999)
152 c_rod[2]=2; c_rol[2]=ver(1,0,0); c_roh[2]=ver(1,999,999)
153 let U3: *Univ=mk(4, c_nver, c_vers, 2, c_rs, c_rsv, c_rd, c_rl, c_rh, 3, c_rod, c_rol, c_roh)
154 let sel3: *i64=sys_mmap(4*8) as *i64; z=0; while z<4 { sel3[z]=0-1; z=z+1 }
155 let ok3: i64=solve(U3, 0, sel3)
156 g_puts(" T3 conflict: solved="); g_pn(ok3); g_puts(" (expect 0 = UNSATISFIABLE: B needs D<2.0.0, C needs D>=2.0.0)\n" as *u8)
157 var t3: i64=0; if ok3==0 { t3=1 }
158 pass=pass+ck("T3: CONFLICT -- an unsatisfiable diamond (D<2.0.0 vs D>=2.0.0) is DETECTED, no false solution" as *u8, t3); total=total+1
159
160 // ===== T4 teeth: semver operator -> interval KATs =====
161 // caret ^1.2.3 = [1.2.3, 1.999.999]: includes 1.9.9, EXCLUDES 2.0.0 and 1.2.2
162 let cLo: i64=ver(1,2,3); let cHi: i64=ver(1,999,999)
163 let caret_ok: i64 = (ver(1,9,9)>=cLo && ver(1,9,9)<=cHi && ver(2,0,0)>cHi && ver(1,2,2)<cLo) as i64
164 // tilde ~1.2.3 = [1.2.3, 1.2.999]: includes 1.2.9, EXCLUDES 1.3.0
165 let tLo: i64=ver(1,2,3); let tHi: i64=ver(1,2,999)
166 let tilde_ok: i64 = (ver(1,2,9)>=tLo && ver(1,2,9)<=tHi && ver(1,3,0)>tHi) as i64
167 // exact =1.2.3 = [1.2.3,1.2.3]: excludes neighbors ; gte >=1.2.0 includes 9.9.9, excludes 1.1.9
168 let exact_ok: i64 = (ver(1,2,3)>=ver(1,2,3) && ver(1,2,3)<=ver(1,2,3) && ver(1,2,4)>ver(1,2,3) && ver(1,2,2)<ver(1,2,3)) as i64
169 let gte_ok: i64 = (ver(9,9,9)>=ver(1,2,0) && ver(1,1,9)<ver(1,2,0)) as i64
170 var t4: i64=0; if caret_ok==1 { if tilde_ok==1 { if exact_ok==1 { if gte_ok==1 { t4=1 } } } }
171 g_puts(" T4 semver intervals: caret="); g_pn(caret_ok); g_puts(" tilde="); g_pn(tilde_ok); g_puts(" exact="); g_pn(exact_ok); g_puts(" gte="); g_pn(gte_ok); g_puts("\n" as *u8)
172 pass=pass+ck("T4 (teeth): semver operators map to correct intervals (caret/tilde/exact/gte KATs)" as *u8, t4); total=total+1
173
174 // ===== T5: determinism -- solve the diamond again, identical selection =====
175 let sel1b: *i64=sys_mmap(4*8) as *i64; z=0; while z<4 { sel1b[z]=0-1; z=z+1 }
176 let ok1b: i64=solve(U1, 0, sel1b)
177 var same: i64=1; z=0; while z<4 { if sel1[z]!=sel1b[z] { same=0 } z=z+1 }
178 var t5: i64=0; if ok1b==1 { if same==1 { t5=1 } }
179 g_puts(" T5 determinism: re-solve identical="); g_pn(same); g_puts(" (reproducible / lockfile-stable)\n" as *u8)
180 pass=pass+ck("T5: the solver is DETERMINISTIC -- re-solving yields the identical selection (lockfile-stable)" as *u8, t5); total=total+1
181
182 var okall: i64=0; if pass==total { okall=1 }
183 g_puts("---- nx_pkg_solve: passed "); g_pn(pass); g_puts(" / "); g_pn(total); g_puts(" ----\n" as *u8)
184 if okall==1 {
185 let logf: i64=sys_openat_append("knowledge/status/pkg_solve.log" as *u8, 420)
186 if logf>=0 { let zz: i64=sys_write(logf,"NXPKGSOLVE GREEN: version-constraint solver -- semver intervals + backtracking resolver (diamond intersection, real backtrack, conflict/unsat detection), deterministic\n" as *u8,158); sys_close(logf) }
187 g_puts("verdict=GREEN (version-constraint solving: semver intervals + backtracking resolver -- diamond, backtrack, and unsat all handled, deterministic; the PACKAGE-MGMT version gap closed)\n" as *u8); sys_exit(0); return 0
188 }
189 g_puts("verdict=RED\n" as *u8); sys_exit(1); return 1
190}