code wiki / (root) / nx_nxa_morf_ingress_gate.nx

nx_nxa_morf_ingress_gate.nx source

↩ module page · 194 lines · 10859 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" 9import "nx_nxa_morf_admit.nx" 10import "nx_wasm_craft.nx" 11 12func mdag_equal(a: *i64,b: *i64,n: i64) -> i64 { 13 var i: i64 = 0 14 while i < n { if a[i] != b[i] { return 0 }; i = i+1 } 15 return 1 16} 17func mdag_text_equal(a: *u8,b: *u8) -> i64 { 18 var i: i64 = 0 19 while a[i] != (0 as u8) { if a[i] != b[i] { return 0 }; i = i+1 } 20 if b[i] != (0 as u8) { return 0 } 21 return 1 22} 23func mdag_run(path: *u8,ctr: *i64) -> i64 { 24 let lp: *i64 = sys_mmap(8) as *i64 25 if (lp as i64) <= 0 { return 0-1 } 26 let bytes: *u8 = sys_read_file(path,lp) 27 if (bytes as i64) <= 0 { return 0-1 } 28 let h: *i64 = bytes as *i64 29 let nv: i64 = nmi_scratch_bytes(bytes,lp[0]) 30 if nv < 1 { return NMI_E_SHAPE } 31 let member: *u8 = sys_mmap(nv) as *u8 32 let admitted: *NmiAsset = sys_mmap(__size_of(NmiAsset)) as *NmiAsset 33 let av: *MvcView = sys_mmap(__size_of(MvcView)) as *MvcView 34 if (member as i64) <= 0 { return 0-4 } 35 if (admitted as i64) <= 0 { return 0-4 } 36 if (av as i64) <= 0 { return 0-4 } 37 admitted.view = av 38 av.channels = 0-999 39 gv_check_eq("undersized membership scratch refuses real asset" as *u8,nmi_admit(bytes,lp[0],member,nv-1,admitted),NMI_E_SCRATCH,ctr) 40 gv_check_eq("refused ingress leaves output view unpublished" as *u8,av.channels,0-999,ctr) 41 let admission: i64 = nmi_admit(bytes,lp[0],member,nv,admitted) 42 gv_check_eq("canonical shared admission accepts real asset" as *u8,admission,0,ctr) 43 if admission < 0 { return admission } 44 gv_check_eq("membership may not overwrite immutable input" as *u8,nmi_admit(bytes,lp[0],bytes,nv,admitted),NMI_E_SCRATCH,ctr) 45 let tw: i64 = nxa_counted_section(bytes,lp[0],nxa_tag4("TRIS" as *u8),MVC_AXES) 46 if tw < 0 { return NMI_E_SHAPE } 47 let nf: i64 = av.faces; let nc: i64 = av.channels 48 let dw: i64 = av.delta_words; let cw: i64 = dw/nc 49 let words: i64 = av.bind_words 50 let bind: *i64 = av.bind 51 let tri: *i64 = ((bytes as i64)+(tw+1)*MVC_WORD) as *i64 52 let face: *i64 = av.face 53 let delta: *i64 = av.delta 54 let seen: *i64 = sys_mmap(nv*8) as *i64 55 let bn: *i64 = sys_mmap(words*8) as *i64 56 let pos: *i64 = sys_mmap(words*8) as *i64 57 let norm: *i64 = sys_mmap(words*8) as *i64 58 let again: *i64 = sys_mmap(words*8) as *i64 59 let norm2: *i64 = sys_mmap(words*8) as *i64 60 let expected: *i64 = sys_mmap(words*8) as *i64 61 let weights: *i64 = sys_mmap(nc*8) as *i64 62 let v: *MvcView = sys_mmap(__size_of(MvcView)) as *MvcView 63 let a: *MrdAsset = sys_mmap(__size_of(MrdAsset)) as *MrdAsset 64 if (seen as i64) <= 0 { return 0-4 }; if (bn as i64) <= 0 { return 0-4 } 65 if (pos as i64) <= 0 { return 0-4 }; if (norm as i64) <= 0 { return 0-4 } 66 if (again as i64) <= 0 { return 0-4 }; if (norm2 as i64) <= 0 { return 0-4 } 67 if (expected as i64) <= 0 { return 0-4 }; if (weights as i64) <= 0 { return 0-4 } 68 if (v as i64) <= 0 { return 0-4 }; if (a as i64) <= 0 { return 0-4 } 69 var i: i64 = 0 70 while i < nv { seen[i] = 0; i = i+1 } 71 i = 0 72 while i < nf { 73 let id: i64 = face[i] 74 if id < 0 { return 0-5 }; if id >= nv { return 0-5 } 75 if seen[id] != 0 { return 0-5 }; seen[id] = 1; i = i+1 76 } 77 // Degree proof admits the actual shared area-weighted owner before baseline. 78 i = 0 79 while i < nv { seen[i] = 0; i = i+1 } 80 var degree: i64 = 0; i = 0 81 while i < h[tw]*3 { 82 let id: i64 = tri[i] 83 if id < 0 { return 0-5 }; if id >= nv { return 0-5 } 84 seen[id] = seen[id]+1 85 if seen[id] > degree { degree = seen[id] }; i = i+1 86 } 87 if mrd_normal_envelope(bind,tri,h[tw],degree) < 0 { return MRD_E_NORMAL_RANGE } 88 if vn_smooth_area(bind,tri,nv,h[tw],bn) < 0 { return 0-6 } 89 var selected: i64 = 0-1; i = 0 90 while i < dw { if delta[i] != 0 { if selected < 0 { selected = i/cw } }; i = i+1 } 91 if selected < 0 { return 0-7 } 92 i = 0 93 while i < nc { weights[i] = 0; i = i+1 } 94 weights[selected] = av.unit 95 i = 0 96 while i < words { expected[i] = bind[i]; i = i+1 } 97 var support: i64 = 0; i = 0 98 while i < nf { 99 var axis: i64 = 0; var changed: i64 = 0 100 while axis < 3 { 101 let d: i64 = delta[selected*cw+i*3+axis] 102 let at: i64 = face[i]*3+axis 103 if mvc_sum_ok(bind[at],d) == 0 { return 0-8 } 104 expected[at] = bind[at]+d 105 if d != 0 { changed = 1 }; axis = axis+1 106 } 107 support = support+changed; i = i+1 108 } 109 v.bind = bind; v.bind_words = words; v.face = face; v.face_words = nf 110 v.delta = delta; v.delta_words = dw; v.vertices = nv; v.faces = nf; v.channels = nc; v.unit = av.unit 111 a.morph = v; a.triangles = tri; a.triangle_words = h[tw]*3 112 a.bind_normals = bn; a.normal_words = words 113 let moved: i64 = mrd_prepare(a,weights,nc,pos,words,norm,words) 114 gv_check("actual channel has nonzero support" as *u8,support > 0,ctr) 115 gv_check_eq("actual support count is exact" as *u8,moved,support,ctr) 116 if moved < 0 { return moved } 117 gv_check("every VERT coordinate matches stored full-weight delta including non-FACE identity" as *u8,mdag_equal(pos,expected,words),ctr) 118 var normals_valid: i64 = 1; i = 0 119 while i < nv { 120 var axis: i64 = 0; var nonzero: i64 = 0 121 while axis < 3 { 122 let value: i64 = norm[i*3+axis] 123 if value < 0-VN_SCALE { normals_valid = 0 } 124 if value > VN_SCALE { normals_valid = 0 } 125 if value != 0 { nonzero = 1 }; axis = axis+1 126 } 127 if nonzero == 0 { normals_valid = 0 }; i = i+1 128 } 129 gv_check("every actual vertex has bounded nonzero geometric normal" as *u8,normals_valid,ctr) 130 gv_check_eq("repeat real draw succeeds" as *u8,mrd_prepare(a,weights,nc,again,words,norm2,words),moved,ctr) 131 gv_check("repeat geometry exact" as *u8,mdag_equal(pos,again,words),ctr) 132 gv_check("repeat normals exact" as *u8,mdag_equal(norm,norm2,words),ctr) 133 weights[selected] = 0 134 gv_check_eq("inactive entity returns zero" as *u8,mrd_prepare(a,weights,nc,again,words,norm2,words),0,ctr) 135 gv_check("inactive positions exact" as *u8,mdag_equal(bind,again,words),ctr) 136 gv_check("inactive supplied normals exact" as *u8,mdag_equal(bn,norm2,words),ctr) 137 gv_check("inactive entity did not overwrite active geometry" as *u8,mdag_equal(pos,expected,words),ctr) 138 // Compose real admitted data into the actual engine's owned arena. 139 let capacity: i64 = wc_morf_storage_bytes(a,admitted.tag_words) 140 if capacity < 0 { return capacity } 141 let base: i64 = sys_mmap(CRAFT_EXT_TOTAL+capacity) as i64 142 if base <= 0 { return 0-4 } 143 let mobs: *i64 = mobp(base) 144 en_init(mobs,MOB_CAP,MOB_NCOMP) 145 en_spawn(mobs); en_spawn(mobs) 146 gv_check_eq("real admitted asset binds engine-owned storage" as *u8,wc_morf_bind(base,capacity,a,admitted.tags,admitted.tag_words),0,ctr) 147 gv_check_eq("real asset tag identity survives ingress" as *u8,wc_morf_channel_tag(base,selected),admitted.tags[selected*NMI_CHANNEL_WORDS],ctr) 148 gv_check_eq("real asset weight unit accepted by engine" as *u8,wc_cast_morf_weight(base,0,selected,av.unit),0,ctr) 149 gv_check_eq("real engine draw moves actual channel support" as *u8,wc_cast_morf(base,0),support,ctr) 150 let draw: *WcmDraw = wc_morf_descriptor(base) 151 gv_check("engine geometry agrees with independent stored-delta oracle" as *u8,mdag_equal(draw.positions,expected,words),ctr) 152 gv_check("engine normals agree with admitted direct draw" as *u8,mdag_equal(draw.normals,norm,words),ctr) 153 gv_check_eq("second real entity stays on incumbent float path" as *u8,wc_cast_morf(base,1),0,ctr) 154 // Corrupt membership with VALID checksums: fail on actual duplicate identity, 155 // not merely on integrity. Restore every changed word before returning. 156 if nf > 1 { 157 let fe: i64 = nxa_section_entry(bytes,lp[0],nxa_tag4("FACE" as *u8)) 158 let old_id: i64 = face[0]; let old_fc: i64 = h[fe+3]; let old_toc: i64 = h[3] 159 face[0] = face[1] 160 h[fe+3] = nxa_check2(1,((bytes as i64)+h[fe+1]) as *i64,h[fe+2]) 161 h[3] = nxa_check2(1,((bytes as i64)+32) as *i64,h[2]*4) 162 gv_check_eq("checksummed duplicate FACE identity refused" as *u8,nmi_admit(bytes,lp[0],member,nv,admitted),NMI_R_FACE_DUPLICATE,ctr) 163 gv_check("duplicate FACE retains exact prior diagnostic" as *u8,mdag_text_equal(nmi_diagnostic(NMI_R_FACE_DUPLICATE),"MORF-REFUSE duplicate FACE vertex ID\n" as *u8),ctr) 164 face[0] = old_id; h[fe+3] = old_fc; h[3] = old_toc 165 gv_check_eq("restored real asset admits again" as *u8,nmi_admit(bytes,lp[0],member,nv,admitted),0,ctr) 166 } 167 let me: i64 = nxa_section_entry(bytes,lp[0],nxa_tag4("MORF" as *u8)) 168 let mp: *i64 = ((bytes as i64)+h[me+1]) as *i64 169 let old_unit: i64 = mp[3]; let old_mc: i64 = h[me+3]; let old_tc: i64 = h[3] 170 mp[3] = 0 171 h[me+3] = nxa_check2(1,mp,h[me+2]) 172 h[3] = nxa_check2(1,((bytes as i64)+32) as *i64,h[2]*4) 173 gv_check_eq("checksummed invalid unit retains precise reason" as *u8,nmi_admit(bytes,lp[0],member,nv,admitted),NMI_R_UNIT,ctr) 174 gv_check("unit retains exact prior diagnostic" as *u8,mdag_text_equal(nmi_diagnostic(NMI_R_UNIT),"MORF-REFUSE declared weight unit is not positive\n" as *u8),ctr) 175 mp[3] = old_unit; h[me+3] = old_mc; h[3] = old_tc 176 let fe2: i64 = nxa_section_entry(bytes,lp[0],nxa_tag4("FACE" as *u8)) 177 let old_tag: i64 = h[fe2]; let old_tc2: i64 = h[3] 178 h[fe2] = nxa_tag4("TEST" as *u8) 179 h[3] = nxa_check2(1,((bytes as i64)+32) as *i64,h[2]*4) 180 let missing: i64 = nmi_admit(bytes,lp[0],member,nv,admitted) 181 gv_check_eq("missing FACE retains precise reason" as *u8,missing,NMI_R_NO_FACE,ctr) 182 gv_check_eq("missing FACE retains missing-section class" as *u8,nmi_missing(missing),1,ctr) 183 gv_check("missing FACE retains exact prior diagnostic" as *u8,mdag_text_equal(nmi_diagnostic(missing),"MORF-REFUSE no FACE section -- run derive first\n" as *u8),ctr) 184 h[fe2] = old_tag; h[3] = old_tc2 185 return 0 186} 187func main(argc: i64,argv: *i64) -> i64 { 188 let ctr: *i64 = gv_ctr() 189 gv_head("shared canonical MORF ingress into actual engine storage" as *u8) 190 var rc: i64 = 0-1 191 if argc == 2 { rc = mdag_run(argv[1] as *u8,ctr) } 192 gv_check_eq("real asset admission and preparation succeeds" as *u8,rc,0,ctr) 193 return gv_verdict("NX-NXA-MORF-INGRESS" as *u8,ctr,"real geometry witness; renderer float32 bypass and both GPU doors remain separate acceptance" as *u8) 194}