code wiki / (root) / nx_morf_draw_asset_gate.nx

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}