code wiki / (root) / nx_zstd_frame_gate.nx

nx_zstd_frame_gate.nx source

↩ module page · 199 lines · 8945 B

1// nx_zstd_frame_gate.nx -- proves the zstd frame and block layer. 2// 3// T3 pins the 2-BYTE FRAME_CONTENT_SIZE BIAS. A two-byte size stores 4// (size - 256), so a naive reader reports every such frame exactly 256 bytes 5// short. The affected range is 256..65791 bytes, which is where small test 6// files live -- so this bug hides in exactly the frames a developer checks by 7// hand. The test asserts a stored 0 means 256. 8// 9// T2 pins the IRREGULAR field-size tables. Neither FCS nor Dictionary_ID size 10// is the flag value: FCS goes 0/2/4/8 (or 1 when Single_Segment is set with 11// flag 0) and DID goes 0/1/2/4. Treating either as the raw flag mis-sizes the 12// header and every byte after it. 13// 14// T6 proves a real end-to-end decode: a frame of raw and RLE blocks IS a 15// valid zstd file, and this decodes one to exact bytes. 16// 17// T7 proves the honest refusal: a Compressed block returns a DISTINCT code 18// rather than passing undecoded bytes through as if they were output. 19// 20// license_tier: ORIGINAL 21import "nx_syscalls.nx" 22import "nx_zstd_frame.nx" 23 24func g_puts(s: *u8) -> i64 { 25 var i: i64 = 0 26 while s[i] != (0 as u8) { i = i + 1 } 27 sys_write(1, s, i) 28 return i 29} 30 31func g_putn(v: i64) -> i64 { 32 let buf: *u8 = sys_mmap(32) 33 var x: i64 = v 34 if x < 0 { g_puts("-" as *u8); x = 0 - x } 35 if x == 0 { buf[0] = 0x30 as u8; sys_write(1, buf, 1); return 1 } 36 let tmp: *u8 = sys_mmap(32) 37 var d: i64 = 0 38 while x > 0 { tmp[d] = ((x % 10) + 0x30) as u8; x = x / 10; d = d + 1 } 39 var i: i64 = 0 40 while i < d { buf[i] = tmp[d - 1 - i]; i = i + 1 } 41 sys_write(1, buf, d) 42 return d 43} 44 45func main() -> i64 { 46 var fails: i64 = 0 47 var mark: i64 = 0 48 49 // ---- T1: the magic, little-endian ---- 50 let f: *u8 = sys_mmap(4096) 51 if nx_zstd_frame_write(f, 4096, 100) != 9 { fails = fails + 1 } 52 if (f[0] as i64 & 255) != 0x28 { fails = fails + 1 } 53 if (f[1] as i64 & 255) != 0xb5 { fails = fails + 1 } 54 if (f[2] as i64 & 255) != 0x2f { fails = fails + 1 } 55 if (f[3] as i64 & 255) != 0xfd { fails = fails + 1 } 56 if fails > 0 { if mark == 0 { mark = 1 } } 57 58 // ---- T2: the IRREGULAR field-size tables ---- 59 // FCS: flag 0 gives 0 bytes normally but ONE byte with Single_Segment 60 if nx_zstd_fcs_size(0, 0) != 0 { fails = fails + 1 } 61 if nx_zstd_fcs_size(0, 1) != 1 { fails = fails + 1 } 62 if nx_zstd_fcs_size(1, 0) != 2 { fails = fails + 1 } 63 if nx_zstd_fcs_size(2, 0) != 4 { fails = fails + 1 } 64 if nx_zstd_fcs_size(3, 0) != 8 { fails = fails + 1 } 65 // DID: 0/1/2/4 -- flag 3 is FOUR bytes, not three 66 if nx_zstd_did_size(0) != 0 { fails = fails + 1 } 67 if nx_zstd_did_size(1) != 1 { fails = fails + 1 } 68 if nx_zstd_did_size(2) != 2 { fails = fails + 1 } 69 if nx_zstd_did_size(3) != 4 { fails = fails + 1 } 70 if fails > 0 { if mark == 0 { mark = 2 } } 71 72 // ---- T3: the 2-byte content size is BIASED BY 256 ---- 73 let b2: *u8 = sys_mmap(256) 74 b2[0] = 0x28 as u8; b2[1] = 0xb5 as u8; b2[2] = 0x2f as u8; b2[3] = 0xfd as u8 75 // fcs_flag 1 (two bytes), no single-segment, no checksum, no dict 76 b2[4] = (1 << 6) as u8 77 b2[5] = 0x40 as u8 // window descriptor 78 b2[6] = 0x00 as u8; b2[7] = 0x00 as u8 // stored size 0 -> means 256 79 let fl: *i64 = sys_mmap(128) as *i64 80 if nx_zstd_frame_parse(b2, 8, fl) != NX_ZSTD_OK { fails = fails + 1 } else { 81 if fl[NX_ZF_CONTENTSIZE] != 256 { fails = fails + 1 } 82 if fl[NX_ZF_HDRLEN] != 8 { fails = fails + 1 } 83 } 84 // a stored 1000 means 1256 85 b2[6] = 0xe8 as u8; b2[7] = 0x03 as u8 86 if nx_zstd_frame_parse(b2, 8, fl) != NX_ZSTD_OK { fails = fails + 1 } else { 87 if fl[NX_ZF_CONTENTSIZE] != 1256 { fails = fails + 1 } 88 } 89 if fails > 0 { if mark == 0 { mark = 3 } } 90 91 // ---- T4: the window descriptor ---- 92 // exponent 0, mantissa 0 -> the 1KB minimum 93 if nx_zstd_window_size(0) != 1024 { fails = fails + 1 } 94 // exponent 0, mantissa 4 -> 1024 + 128*4 95 if nx_zstd_window_size(4) != 1536 { fails = fails + 1 } 96 // exponent 10, mantissa 0 -> 1MB 97 if nx_zstd_window_size(10 << 3) != 1048576 { fails = fails + 1 } 98 if fails > 0 { if mark == 0 { mark = 4 } } 99 100 // ---- T5: the header length is COMPUTED, and varies ---- 101 // single-segment with a 4-byte size: 4 magic + 1 desc + 4 size = 9, 102 // and NO window descriptor byte 103 let f9: *i64 = sys_mmap(128) as *i64 104 nx_zstd_frame_write(f, 4096, 12345) 105 if nx_zstd_frame_parse(f, 9, f9) != NX_ZSTD_OK { fails = fails + 1 } else { 106 if f9[NX_ZF_HDRLEN] != 9 { fails = fails + 1 } 107 if f9[NX_ZF_CONTENTSIZE] != 12345 { fails = fails + 1 } 108 if f9[NX_ZF_SINGLESEG] != 1 { fails = fails + 1 } 109 // with a single segment the window IS the content size 110 if f9[NX_ZF_WINDOWSIZE] != 12345 { fails = fails + 1 } 111 } 112 if fails > 0 { if mark == 0 { mark = 5 } } 113 114 // ---- T6: a REAL frame of raw + RLE blocks, decoded end to end ---- 115 let payload: *u8 = sys_mmap(1024) 116 var i: i64 = 0 117 while i < 300 { payload[i] = ((i * 11 + 5) & 255) as u8; i = i + 1 } 118 let rle: *u8 = sys_mmap(16) 119 rle[0] = 0x5a as u8 120 121 let doc: *u8 = sys_mmap(4096) 122 // 300 raw bytes then 200 RLE bytes -> 500 total 123 var off: i64 = nx_zstd_frame_write(doc, 4096, 500) 124 if off != 9 { fails = fails + 1 } 125 off = nx_zstd_block_write(doc, 4096, off, 0, NX_ZSTD_BLK_RAW, payload, 300) 126 if off <= 0 { fails = fails + 1 } 127 off = nx_zstd_block_write(doc, 4096, off, 1, NX_ZSTD_BLK_RLE, rle, 200) 128 if off <= 0 { fails = fails + 1 } 129 130 let out: *u8 = sys_mmap(4096) 131 let got: i64 = nx_zstd_decode(doc, off, out, 4096) 132 if got != 500 { fails = fails + 1 } else { 133 var bad: i64 = 0 134 i = 0 135 while i < 300 { 136 if (out[i] as i64 & 255) != (payload[i] as i64 & 255) { bad = bad + 1 } 137 i = i + 1 138 } 139 i = 300 140 while i < 500 { 141 if (out[i] as i64 & 255) != 0x5a { bad = bad + 1 } 142 i = i + 1 143 } 144 if bad != 0 { fails = fails + 1 } 145 } 146 if fails > 0 { if mark == 0 { mark = 6 } } 147 148 // ---- T7: a Compressed block is REFUSED with a DISTINCT code ---- 149 let cdoc: *u8 = sys_mmap(4096) 150 var coff: i64 = nx_zstd_frame_write(cdoc, 4096, 100) 151 coff = nx_zstd_block_write(cdoc, 4096, coff, 1, NX_ZSTD_BLK_COMP, payload, 100) 152 let cr: i64 = nx_zstd_decode(cdoc, coff, out, 4096) 153 if cr != NX_ZSTD_ERR_COMPRESSED { fails = fails + 1 } 154 // and that code must be DISTINCT from the malformed code, so a caller can 155 // tell 'not supported yet' from 'this file is broken' 156 if NX_ZSTD_ERR_COMPRESSED == NX_ZSTD_ERR_MALFORMED { fails = fails + 1 } 157 if fails > 0 { if mark == 0 { mark = 7 } } 158 159 // ---- T8 NEG: refusals ---- 160 // a bad magic 161 doc[0] = 0x29 as u8 162 if nx_zstd_decode(doc, off, out, 4096) != NX_ZSTD_ERR_MALFORMED { fails = fails + 1 } 163 doc[0] = 0x28 as u8 164 if nx_zstd_decode(doc, off, out, 4096) != 500 { fails = fails + 1 } 165 // the reserved bit in the descriptor must be zero 166 doc[4] = ((doc[4] as i64) | 0x08) as u8 167 if nx_zstd_decode(doc, off, out, 4096) != NX_ZSTD_ERR_MALFORMED { fails = fails + 1 } 168 doc[4] = ((doc[4] as i64) & 0xf7) as u8 169 // the unused bit likewise 170 doc[4] = ((doc[4] as i64) | 0x10) as u8 171 if nx_zstd_decode(doc, off, out, 4096) != NX_ZSTD_ERR_MALFORMED { fails = fails + 1 } 172 doc[4] = ((doc[4] as i64) & 0xef) as u8 173 if nx_zstd_decode(doc, off, out, 4096) != 500 { fails = fails + 1 } 174 // a reserved block type 175 let rdoc: *u8 = sys_mmap(4096) 176 var roff: i64 = nx_zstd_frame_write(rdoc, 4096, 10) 177 let bh: i64 = 1 | (3 << 1) | (10 << 3) 178 nx_zstd_le_w(rdoc, roff, bh, 3) 179 if nx_zstd_decode(rdoc, roff + 3 + 10, out, 4096) != NX_ZSTD_ERR_MALFORMED { fails = fails + 1 } 180 // a declared content size that does not match what the blocks produced 181 let mdoc: *u8 = sys_mmap(4096) 182 var moff: i64 = nx_zstd_frame_write(mdoc, 4096, 999) 183 moff = nx_zstd_block_write(mdoc, 4096, moff, 1, NX_ZSTD_BLK_RAW, payload, 100) 184 if nx_zstd_decode(mdoc, moff, out, 4096) != NX_ZSTD_ERR_MALFORMED { fails = fails + 1 } 185 if fails > 0 { if mark == 0 { mark = 8 } } 186 187 if fails == 0 { 188 g_puts("GATE nx_zstd_frame verdict=GREEN pass=8/8 (LE magic 28 B5 2F FD; IRREGULAR field-size tables FCS 0/1/2/4/8 and DID 0/1/2/4; 2-byte content size BIASED BY 256 -- stored 0 means 256; window descriptor exponent+mantissa; header length COMPUTED and single-segment omits the window byte; REAL frame of raw+RLE blocks decoded to 500 exact bytes; Compressed block REFUSED with a code DISTINCT from malformed; NEG bad-magic/reserved-bit/unused-bit/reserved-block-type/size-mismatch refused)\n" as *u8) 189 sys_exit(0) 190 return 0 191 } 192 g_puts("GATE nx_zstd_frame verdict=RED fails=" as *u8) 193 g_putn(fails) 194 g_puts(" first_stage=" as *u8) 195 g_putn(mark) 196 g_puts("\n" as *u8) 197 sys_exit(1) 198 return 1 199}