nx_tar_gate.nx source
↩ module page · 185 lines · 7641 B
1// nx_tar_gate.nx -- proves the USTAR reader/writer by ROUND-TRIP.
2//
3// T4 builds a real two-file archive and walks it back, recovering both names,
4// both sizes and every content byte. Symmetric proof: only a correct pair can
5// pass, since a writer bug and a matching reader bug would still have to
6// agree with the absolute assertions in T1-T3.
7//
8// T2 pins OCTAL, not binary: size 8 must be the ASCII digits "10", because
9// tar's numeric fields are octal text. A binary writer produces headers that
10// look fine in a hex dump and no tar on earth can read.
11//
12// T6 pins the two-block terminator. One zero block is not an archive end;
13// readers scan for two.
14//
15// T7 is the integrity proof: corrupt one header byte and the entry must be
16// REFUSED by checksum, then restored and re-accepted so the test is shown to
17// have measured that byte.
18//
19// NON-VACUITY: T8 covers refusals -- an over-long name, an oversize field, a
20// short output buffer and a bad magic must each be rejected.
21//
22// license_tier: ORIGINAL
23import "nx_syscalls.nx"
24import "nx_tar.nx"
25
26func g_puts(s: *u8) -> i64 {
27 var i: i64 = 0
28 while s[i] != (0 as u8) { i = i + 1 }
29 sys_write(1, s, i)
30 return i
31}
32
33func g_putn(v: i64) -> i64 {
34 let buf: *u8 = sys_mmap(32)
35 var x: i64 = v
36 if x == 0 { buf[0] = 0x30 as u8; sys_write(1, buf, 1); return 1 }
37 let tmp: *u8 = sys_mmap(32)
38 var d: i64 = 0
39 while x > 0 { tmp[d] = ((x % 10) + 0x30) as u8; x = x / 10; d = d + 1 }
40 var i: i64 = 0
41 while i < d { buf[i] = tmp[d - 1 - i]; i = i + 1 }
42 sys_write(1, buf, d)
43 return d
44}
45
46func main() -> i64 {
47 var fails: i64 = 0
48 var mark: i64 = 0
49
50 // ---- T1/T2: octal fields are ASCII TEXT, not binary ----
51 let ob: *u8 = sys_mmap(64)
52 if nxtar_octal_w(ob, 0, 8, 8) != 1 { fails = fails + 1 }
53 // 8 decimal = 10 octal -> "0000010" + NUL in an 8-byte field
54 if (ob[5] as i64 & 255) != 0x31 { fails = fails + 1 }
55 if (ob[6] as i64 & 255) != 0x30 { fails = fails + 1 }
56 if (ob[7] as i64 & 255) != 0 { fails = fails + 1 }
57 if nxtar_octal_r(ob, 0, 8) != 8 { fails = fails + 1 }
58 // 0644 octal = 420 decimal, round-trip
59 if nxtar_octal_w(ob, 8, 8, 420) != 1 { fails = fails + 1 }
60 if nxtar_octal_r(ob, 8, 8) != 420 { fails = fails + 1 }
61 // a value too wide for the field is REFUSED, never truncated
62 if nxtar_octal_w(ob, 16, 8, 9999999999) != 0 { fails = fails + 1 }
63 if fails > 0 { if mark == 0 { mark = 2 } }
64
65 // ---- T3: the checksum reads its own field as spaces ----
66 let hdr: *u8 = sys_mmap(1024)
67 let nm: *u8 = sys_mmap(64)
68 nm[0] = 0x61 as u8; nm[1] = 0x2e as u8; nm[2] = 0x74 as u8; nm[3] = 0x78 as u8
69 nm[4] = 0x74 as u8; nm[5] = 0 as u8
70 if nxtar_header_build(nm, 5, 420, 1700000000, NX_TAR_TYPE_FILE, hdr) != 1 { fails = fails + 1 }
71 let stored: i64 = nxtar_octal_r(hdr, NX_TAR_CHK_OFF, NX_TAR_CHK_LEN)
72 if stored != nxtar_checksum(hdr) { fails = fails + 1 }
73 if stored <= 0 { fails = fails + 1 }
74 if fails > 0 { if mark == 0 { mark = 3 } }
75
76 // ---- T4: a real two-file archive, built and walked back ----
77 let ar: *u8 = sys_mmap(16384)
78 let d1: *u8 = sys_mmap(1024)
79 var i: i64 = 0
80 while i < 5 { d1[i] = (0x41 + i) as u8; i = i + 1 } // "ABCDE"
81 let d2: *u8 = sys_mmap(2048)
82 while i < 700 { d2[i] = ((i * 3 + 1) & 255) as u8; i = i + 1 }
83 i = 0
84 while i < 700 { d2[i] = ((i * 3 + 1) & 255) as u8; i = i + 1 }
85
86 let n2: *u8 = sys_mmap(64)
87 n2[0] = 0x62 as u8; n2[1] = 0x2e as u8; n2[2] = 0x62 as u8; n2[3] = 0x69 as u8
88 n2[4] = 0x6e as u8; n2[5] = 0 as u8
89
90 var off: i64 = 0
91 off = nxtar_append(ar, 16384, off, nm, d1, 5, 420, 1700000000)
92 if off != 1024 { fails = fails + 1 }
93 off = nxtar_append(ar, 16384, off, n2, d2, 700, 420, 1700000001)
94 // 700 bytes pads to 1024, plus a 512 header -> 1024 + 512 + 1024
95 if off != 2560 { fails = fails + 1 }
96 let total: i64 = nxtar_finalize(ar, 16384, off)
97 if total != 3584 { fails = fails + 1 }
98 if fails > 0 { if mark == 0 { mark = 4 } }
99
100 // ---- T5: walk it back and compare every byte ----
101 let fld: *i64 = sys_mmap(128) as *i64
102 var pos: i64 = 0
103 var count: i64 = 0
104 var content_bad: i64 = 0
105 var go: i64 = 1
106 while go == 1 {
107 let r: i64 = nxtar_read(ar, total, pos, fld)
108 if r == 0 { go = 0 } else {
109 if r < 0 { fails = fails + 1; go = 0 } else {
110 count = count + 1
111 let doff: i64 = fld[NX_TAR_FLD_DATAOFF]
112 let sz: i64 = fld[NX_TAR_FLD_SIZE]
113 if count == 1 {
114 if sz != 5 { fails = fails + 1 }
115 if fld[NX_TAR_FLD_NAMELEN] != 5 { fails = fails + 1 }
116 if fld[NX_TAR_FLD_MODE] != 420 { fails = fails + 1 }
117 if fld[NX_TAR_FLD_TYPE] != NX_TAR_TYPE_FILE { fails = fails + 1 }
118 var k: i64 = 0
119 while k < 5 {
120 if (ar[doff+k] as i64 & 255) != (d1[k] as i64 & 255) { content_bad = content_bad + 1 }
121 k = k + 1
122 }
123 }
124 if count == 2 {
125 if sz != 700 { fails = fails + 1 }
126 if fld[NX_TAR_FLD_MTIME] != 1700000001 { fails = fails + 1 }
127 var k2: i64 = 0
128 while k2 < 700 {
129 if (ar[doff+k2] as i64 & 255) != (d2[k2] as i64 & 255) { content_bad = content_bad + 1 }
130 k2 = k2 + 1
131 }
132 }
133 pos = fld[NX_TAR_FLD_NEXT]
134 } }
135 }
136 if count != 2 { fails = fails + 1 }
137 if content_bad != 0 { fails = fails + 1 }
138 if fails > 0 { if mark == 0 { mark = 5 } }
139
140 // ---- T6: the archive ends with TWO zero blocks ----
141 var zeros: i64 = 0
142 i = 0
143 while i < 1024 {
144 if (ar[total - 1024 + i] as i64 & 255) == 0 { zeros = zeros + 1 }
145 i = i + 1
146 }
147 if zeros != 1024 { fails = fails + 1 }
148 if fails > 0 { if mark == 0 { mark = 6 } }
149
150 // ---- T7: one corrupted header byte must be REFUSED by checksum ----
151 ar[10] = ((ar[10] as i64) ^ 0xff) as u8
152 if nxtar_read(ar, total, 0, fld) != (0 - 1) { fails = fails + 1 }
153 ar[10] = ((ar[10] as i64) ^ 0xff) as u8
154 if nxtar_read(ar, total, 0, fld) != 1 { fails = fails + 1 }
155 if fails > 0 { if mark == 0 { mark = 7 } }
156
157 // ---- T8 NEG: refusals ----
158 // a name at or past the 100-byte field
159 let longn: *u8 = sys_mmap(256)
160 i = 0
161 while i < 120 { longn[i] = 0x78 as u8; i = i + 1 }
162 longn[120] = 0 as u8
163 if nxtar_header_build(longn, 1, 420, 0, NX_TAR_TYPE_FILE, hdr) != 0 { fails = fails + 1 }
164 // an output buffer that cannot hold header + padded data
165 if nxtar_append(ar, 600, 0, nm, d1, 5, 420, 0) != 0 { fails = fails + 1 }
166 // no room for the two terminator blocks
167 if nxtar_finalize(ar, 600, 0) != 0 { fails = fails + 1 }
168 // a broken ustar magic
169 ar[NX_TAR_MAGIC_OFF] = 0x41 as u8
170 if nxtar_read(ar, total, 0, fld) != (0 - 1) { fails = fails + 1 }
171 if fails > 0 { if mark == 0 { mark = 8 } }
172
173 if fails == 0 {
174 g_puts("GATE nx_tar verdict=GREEN pass=8/8 (octal is ASCII text, oversize refused; self-referential checksum; 2-file archive build 3584B; walk-back recovers 2 entries with names/sizes/modes/mtimes and 705 content bytes EXACT; two-block terminator; corrupted header byte refused then restored-and-accepted; NEG long-name/short-buffer/no-terminator-room/bad-magic refused)\n" as *u8)
175 sys_exit(0)
176 return 0
177 }
178 g_puts("GATE nx_tar verdict=RED fails=" as *u8)
179 g_putn(fails)
180 g_puts(" first_stage=" as *u8)
181 g_putn(mark)
182 g_puts("\n" as *u8)
183 sys_exit(1)
184 return 1
185}