nx_morf_draw_asset_gate.nx source
↩ module page · 139 lines · 6879 B
1// ORIGINAL. Read-only real NXA witness. Usage: gate.elf <banked-asset.nxa>
2// Container validation stays with nx_nxa; this gate admits the documented payloads.
3// Inactive integer identity is tested here. The renderer must retain its original
4// float32 position/normal buffers when moved==0; this gate cannot prove that seam.
5import "nx_syscalls.nx"
6import "nx_gate_verdict.nx"
7import "nx_nxa.nx"
8import "nx_morf_draw_core.nx"
9
10func mdag_equal(a: *i64,b: *i64,n: i64) -> i64 {
11 var i: i64 = 0
12 while i < n { if a[i] != b[i] { return 0 }; i = i+1 }
13 return 1
14}
15func mdag_run(path: *u8,ctr: *i64) -> i64 {
16 let lp: *i64 = sys_mmap(8) as *i64
17 if (lp as i64) <= 0 { return 0-1 }
18 let bytes: *u8 = sys_read_file(path,lp)
19 if (bytes as i64) <= 0 { return 0-1 }
20 let h: *i64 = bytes as *i64
21 let vw: i64 = nxa_counted_section(bytes,lp[0],nxa_tag4("VERT" as *u8),3)
22 let tw: i64 = nxa_counted_section(bytes,lp[0],nxa_tag4("TRIS" as *u8),3)
23 let fe: i64 = nxa_section_entry(bytes,lp[0],nxa_tag4("FACE" as *u8))
24 let me: i64 = nxa_section_entry(bytes,lp[0],nxa_tag4("MORF" as *u8))
25 if vw < 0 { return 0-2 }; if tw < 0 { return 0-2 }
26 if fe < 0 { return 0-2 }; if me < 0 { return 0-2 }
27 if h[fe+2] < 4 { return 0-3 }; if h[me+2] < 4 { return 0-3 }
28 let f: *i64 = ((bytes as i64)+h[fe+1]) as *i64
29 let m: *i64 = ((bytes as i64)+h[me+1]) as *i64
30 let nv: i64 = h[vw]; let nf: i64 = f[0]; let nc: i64 = m[0]
31 if nv < 1 { return 0-3 }; if nf < 1 { return 0-3 }
32 if nf > nv { return 0-3 }; if nf != h[fe+2]-4 { return 0-3 }
33 if nc < 1 { return 0-3 }; if m[1] != nf { return 0-3 }
34 if m[2] != 3 { return 0-3 }; if m[3] < 1 { return 0-3 }
35 let rem: i64 = h[me+2]-4
36 if nc > rem/2 { return 0-3 }
37 let dw: i64 = rem-nc*2
38 if dw%nc != 0 { return 0-3 }
39 let cw: i64 = dw/nc
40 if cw%3 != 0 { return 0-3 }; if cw/3 != nf { return 0-3 }
41 let words: i64 = nv*3
42 let bind: *i64 = ((bytes as i64)+(vw+1)*8) as *i64
43 let tri: *i64 = ((bytes as i64)+(tw+1)*8) as *i64
44 let face: *i64 = ((f as i64)+4*8) as *i64
45 let delta: *i64 = ((m as i64)+(4+nc*2)*8) as *i64
46 let seen: *i64 = sys_mmap(nv*8) as *i64
47 let bn: *i64 = sys_mmap(words*8) as *i64
48 let pos: *i64 = sys_mmap(words*8) as *i64
49 let norm: *i64 = sys_mmap(words*8) as *i64
50 let again: *i64 = sys_mmap(words*8) as *i64
51 let norm2: *i64 = sys_mmap(words*8) as *i64
52 let expected: *i64 = sys_mmap(words*8) as *i64
53 let weights: *i64 = sys_mmap(nc*8) as *i64
54 let v: *MvcView = sys_mmap(__size_of(MvcView)) as *MvcView
55 let a: *MrdAsset = sys_mmap(__size_of(MrdAsset)) as *MrdAsset
56 if (seen as i64) <= 0 { return 0-4 }; if (bn as i64) <= 0 { return 0-4 }
57 if (pos as i64) <= 0 { return 0-4 }; if (norm as i64) <= 0 { return 0-4 }
58 if (again as i64) <= 0 { return 0-4 }; if (norm2 as i64) <= 0 { return 0-4 }
59 if (expected as i64) <= 0 { return 0-4 }; if (weights as i64) <= 0 { return 0-4 }
60 if (v as i64) <= 0 { return 0-4 }; if (a as i64) <= 0 { return 0-4 }
61 var i: i64 = 0
62 while i < nv { seen[i] = 0; i = i+1 }
63 i = 0
64 while i < nf {
65 let id: i64 = face[i]
66 if id < 0 { return 0-5 }; if id >= nv { return 0-5 }
67 if seen[id] != 0 { return 0-5 }; seen[id] = 1; i = i+1
68 }
69 // Degree proof admits the actual shared area-weighted owner before baseline.
70 i = 0
71 while i < nv { seen[i] = 0; i = i+1 }
72 var degree: i64 = 0; i = 0
73 while i < h[tw]*3 {
74 let id: i64 = tri[i]
75 if id < 0 { return 0-5 }; if id >= nv { return 0-5 }
76 seen[id] = seen[id]+1
77 if seen[id] > degree { degree = seen[id] }; i = i+1
78 }
79 if mrd_normal_envelope(bind,tri,h[tw],degree) < 0 { return MRD_E_NORMAL_RANGE }
80 if vn_smooth_area(bind,tri,nv,h[tw],bn) < 0 { return 0-6 }
81 var selected: i64 = 0-1; i = 0
82 while i < dw { if delta[i] != 0 { if selected < 0 { selected = i/cw } }; i = i+1 }
83 if selected < 0 { return 0-7 }
84 i = 0
85 while i < nc { weights[i] = 0; i = i+1 }
86 weights[selected] = m[3]
87 i = 0
88 while i < words { expected[i] = bind[i]; i = i+1 }
89 var support: i64 = 0; i = 0
90 while i < nf {
91 var axis: i64 = 0; var changed: i64 = 0
92 while axis < 3 {
93 let d: i64 = delta[selected*cw+i*3+axis]
94 let at: i64 = face[i]*3+axis
95 if mvc_sum_ok(bind[at],d) == 0 { return 0-8 }
96 expected[at] = bind[at]+d
97 if d != 0 { changed = 1 }; axis = axis+1
98 }
99 support = support+changed; i = i+1
100 }
101 v.bind = bind; v.bind_words = words; v.face = face; v.face_words = nf
102 v.delta = delta; v.delta_words = dw; v.vertices = nv; v.faces = nf; v.channels = nc; v.unit = m[3]
103 a.morph = v; a.triangles = tri; a.triangle_words = h[tw]*3
104 a.bind_normals = bn; a.normal_words = words
105 let moved: i64 = mrd_prepare(a,weights,nc,pos,words,norm,words)
106 gv_check("actual channel has nonzero support" as *u8,support > 0,ctr)
107 gv_check_eq("actual support count is exact" as *u8,moved,support,ctr)
108 if moved < 0 { return moved }
109 gv_check("every VERT coordinate matches stored full-weight delta including non-FACE identity" as *u8,mdag_equal(pos,expected,words),ctr)
110 var normals_valid: i64 = 1; i = 0
111 while i < nv {
112 var axis: i64 = 0; var nonzero: i64 = 0
113 while axis < 3 {
114 let value: i64 = norm[i*3+axis]
115 if value < 0-VN_SCALE { normals_valid = 0 }
116 if value > VN_SCALE { normals_valid = 0 }
117 if value != 0 { nonzero = 1 }; axis = axis+1
118 }
119 if nonzero == 0 { normals_valid = 0 }; i = i+1
120 }
121 gv_check("every actual vertex has bounded nonzero geometric normal" as *u8,normals_valid,ctr)
122 gv_check_eq("repeat real draw succeeds" as *u8,mrd_prepare(a,weights,nc,again,words,norm2,words),moved,ctr)
123 gv_check("repeat geometry exact" as *u8,mdag_equal(pos,again,words),ctr)
124 gv_check("repeat normals exact" as *u8,mdag_equal(norm,norm2,words),ctr)
125 weights[selected] = 0
126 gv_check_eq("inactive entity returns zero" as *u8,mrd_prepare(a,weights,nc,again,words,norm2,words),0,ctr)
127 gv_check("inactive positions exact" as *u8,mdag_equal(bind,again,words),ctr)
128 gv_check("inactive supplied normals exact" as *u8,mdag_equal(bn,norm2,words),ctr)
129 gv_check("inactive entity did not overwrite active geometry" as *u8,mdag_equal(pos,expected,words),ctr)
130 return 0
131}
132func main(argc: i64,argv: *i64) -> i64 {
133 let ctr: *i64 = gv_ctr()
134 gv_head("real banked MORF draw geometry and shared normals" as *u8)
135 var rc: i64 = 0-1
136 if argc == 2 { rc = mdag_run(argv[1] as *u8,ctr) }
137 gv_check_eq("real asset admission and preparation succeeds" as *u8,rc,0,ctr)
138 return gv_verdict("NX-MORF-DRAW-ASSET" as *u8,ctr,"real geometry witness; renderer float32 bypass and both GPU doors remain separate acceptance" as *u8)
139}