nx_nxa_bounds_gate.nx source
↩ module page · 118 lines · 6443 B
1// NXA v1 section boundaries: malformed inputs must fail before payload access.
2import "nx_syscalls.nx"
3import "nx_nxa.nx"
4import "nx_gate_verdict.nx"
5
6// Exact v1 wire layout, not resource limits.
7const NB_WORD: i64 = 8
8const NB_HEADER_WORDS: i64 = 4
9const NB_ENTRY_WORDS: i64 = 4
10// Boundary witness: 2^64 / the eight-byte wire word; multiplying wraps to zero.
11const NB_WORD_MULTIPLICATION_WRAP: i64 = 2305843009213693952
12const NB_FIXTURE_WORDS: i64 = NB_HEADER_WORDS + NB_ENTRY_WORDS + 1
13
14func nb_seal(h: *i64) -> i64 {
15 h[3]=nxa_check2(1,((h as i64)+NB_HEADER_WORDS*NB_WORD) as *i64,h[2]*NB_ENTRY_WORDS)
16 return 0
17}
18func nb_fixture() -> *i64 {
19 let h: *i64=sys_mmap(NB_FIXTURE_WORDS*NB_WORD) as *i64
20 h[0]=nxa_magic();h[1]=NXA_VER;h[2]=1
21 h[4]=nxa_tag4("VERT" as *u8)
22 h[5]=(NB_HEADER_WORDS+NB_ENTRY_WORDS)*NB_WORD
23 h[6]=1;h[8]=0;h[7]=nxa_check2(1,((h as i64)+(NB_HEADER_WORDS+NB_ENTRY_WORDS)*NB_WORD) as *i64,1)
24 nb_seal(h)
25 return h
26}
27func main(argc: i64,argv: *i64) -> i64 {
28 let c: *i64=gv_ctr()
29 let h: *i64=nb_fixture()
30 let n: i64=NB_FIXTURE_WORDS*NB_WORD
31 let tag: i64=nxa_tag4("VERT" as *u8)
32 gv_check_eq("valid section reaches exact EOF",nxa_find(h as *u8,n,tag),8,c)
33 gv_check_eq("empty counted array valid",nxa_counted_section(h as *u8,n,tag,3),8,c)
34 h[8]=0-1;h[7]=nxa_check2(1,((h as i64)+h[5]) as *i64,h[6]);nb_seal(h)
35 gv_check_eq("negative element count refused",nxa_counted_section(h as *u8,n,tag,3),0-3,c)
36 h[8]=NB_WORD_MULTIPLICATION_WRAP;h[7]=nxa_check2(1,((h as i64)+h[5]) as *i64,h[6]);nb_seal(h)
37 gv_check_eq("overflowing element count refused",nxa_counted_section(h as *u8,n,tag,3),0-3,c)
38 h[8]=0;h[7]=nxa_check2(1,((h as i64)+h[5]) as *i64,h[6]);nb_seal(h)
39 gv_check_eq("invalid stride refused",nxa_counted_section(h as *u8,n,tag,0),0-3,c)
40 let shape_words: i64=NB_HEADER_WORDS+NB_ENTRY_WORDS+1+3
41 let shape: *i64=sys_mmap(shape_words*NB_WORD) as *i64
42 shape[0]=nxa_magic();shape[1]=NXA_VER;shape[2]=1;shape[4]=tag
43 shape[5]=(NB_HEADER_WORDS+NB_ENTRY_WORDS)*NB_WORD;shape[6]=1+3
44 shape[8]=1;shape[9]=10;shape[10]=20;shape[11]=30
45 shape[7]=nxa_check2(1,((shape as i64)+shape[5]) as *i64,shape[6]);nb_seal(shape)
46 gv_check_eq("one xyz element valid",nxa_counted_section(shape as *u8,shape_words*NB_WORD,tag,3),8,c)
47 shape[6]=3
48 shape[7]=nxa_check2(1,((shape as i64)+shape[5]) as *i64,shape[6]);nb_seal(shape)
49 gv_check_eq("partial element payload refused",nxa_counted_section(shape as *u8,shape_words*NB_WORD,tag,3),0-3,c)
50 shape[6]=4;shape[8]=0
51 shape[7]=nxa_check2(1,((shape as i64)+shape[5]) as *i64,shape[6]);nb_seal(shape)
52 gv_check_eq("undeclared extra elements refused",nxa_counted_section(shape as *u8,shape_words*NB_WORD,tag,3),0-3,c)
53 sys_munmap(shape as *u8,shape_words*NB_WORD)
54 gv_check_eq("short header refused",nxa_find(h as *u8,NB_HEADER_WORDS*NB_WORD-1,tag),0-1,c)
55 gv_check_eq("truncated TOC refused",nxa_find(h as *u8,h[5]-1,tag),0-3,c)
56 gv_check_eq("truncated payload refused",nxa_find(h as *u8,n-1,tag),0-3,c)
57 h[6]=0-1;h[7]=1;nb_seal(h)
58 gv_check_eq("negative word length refused",nxa_find(h as *u8,n,tag),0-3,c)
59 h[6]=NB_WORD_MULTIPLICATION_WRAP;nb_seal(h)
60 gv_check_eq("multiplication wrap length refused",nxa_find(h as *u8,n,tag),0-3,c)
61 h[6]=0;h[5]=n+1;nb_seal(h)
62 gv_check_eq("offset beyond EOF refused",nxa_find(h as *u8,n,tag),0-3,c)
63 h[5]=n-1;nb_seal(h)
64 gv_check_eq("unaligned zero length section refused",nxa_find(h as *u8,n,tag),0-3,c)
65 h[5]=0;nb_seal(h)
66 gv_check_eq("header overlap refused",nxa_find(h as *u8,n,tag),0-3,c)
67 h[5]=n;nb_seal(h)
68 gv_check_eq("empty section at aligned EOF valid",nxa_find(h as *u8,n,tag),NB_FIXTURE_WORDS,c)
69 gv_check_eq("missing count header refused",nxa_counted_section(h as *u8,n,tag,3),0-3,c)
70 h[1]=NXA_VER+1
71 gv_check_eq("future version distinguished",nxa_find(h as *u8,n,tag),0-2,c)
72 h[1]=0
73 gv_check_eq("invalid old version refused",nxa_find(h as *u8,n,tag),0-3,c)
74 h[1]=NXA_VER;h[2]=NB_WORD_MULTIPLICATION_WRAP
75 gv_check_eq("overflowing TOC count refused before checksum",nxa_find(h as *u8,n,tag),0-3,c)
76 h[2]=1;nb_seal(h);h[3]=h[3]+1
77 gv_check_eq("TOC checksum mismatch refused",nxa_find(h as *u8,n,tag),0-3,c)
78 nb_seal(h)
79 gv_check_eq("absent optional tag distinguished",nxa_find(h as *u8,n,nxa_tag4("NONE" as *u8)),0-1,c)
80 h[5]=(NB_HEADER_WORDS+NB_ENTRY_WORDS)*NB_WORD;h[6]=1;h[7]=0;nb_seal(h)
81 gv_check_eq("payload checksum mismatch refused",nxa_find(h as *u8,n,tag),0-3,c)
82 // 65 is the boundary witness immediately beyond the former undocumented ceiling.
83 let sections: i64=65
84 let words: i64=NB_HEADER_WORDS+sections*NB_ENTRY_WORDS
85 let many: *i64=sys_mmap(words*NB_WORD) as *i64
86 many[0]=nxa_magic();many[1]=NXA_VER;many[2]=sections
87 var i: i64=0
88 while i<sections {
89 let e: i64=NB_HEADER_WORDS+i*NB_ENTRY_WORDS
90 many[e]=i+1;many[e+1]=words*NB_WORD;many[e+2]=0;many[e+3]=1
91 i=i+1
92 }
93 many[NB_HEADER_WORDS+(sections-1)*NB_ENTRY_WORDS]=tag;nb_seal(many)
94 gv_check_eq("section count bounded by file not historical ceiling",nxa_find(many as *u8,words*NB_WORD,tag),words,c)
95 if argc>1 {
96 let lengths: *i64=sys_mmap(2*NB_WORD) as *i64
97 let asset: *u8=sys_map_file(argv[1] as *u8,lengths)
98 if lengths[0]<NB_HEADER_WORDS*NB_WORD {
99 gv_check("real asset readable",0,c)
100 } else {
101 let a: *i64=asset as *i64
102 gv_check("real asset VERT shape valid",(nxa_counted_section(asset,lengths[0],tag,3)>=0) as i64,c)
103 gv_check("real asset TRIS shape valid",(nxa_counted_section(asset,lengths[0],nxa_tag4("TRIS" as *u8),3)>=0) as i64,c)
104 if a[2]>0 { if a[2]<=(lengths[0]-NB_HEADER_WORDS*NB_WORD)/(NB_ENTRY_WORDS*NB_WORD) {
105 i=0
106 while i<a[2] {
107 gv_check("real asset declared section validates",(nxa_find(asset,lengths[0],a[NB_HEADER_WORDS+i*NB_ENTRY_WORDS])>=0) as i64,c)
108 i=i+1
109 }
110 } }
111 }
112 if (asset as i64)>0 { if lengths[0]>0 { sys_munmap(asset,lengths[0]) } }
113 sys_munmap(lengths as *u8,2*NB_WORD)
114 }
115 sys_munmap(h as *u8,n)
116 sys_munmap(many as *u8,words*NB_WORD)
117 return gv_verdict("NXA-BOUNDS",c,"wire extents checked before arithmetic and payload access; optional real asset sections validated")
118}