nx_zstd_bits_gate.nx source

1// nx_zstd_bits_gate.nx -- proves zstd's BACKWARD reader and Huffman weights. 2// 3// T2 pins the SENTINEL. zstd streams carry no length: the final byte's highest 4// SET bit marks the end of the data, and everything above it is padding. The 5// test uses two last bytes with the marker at OPPOSITE ends -- 0x81 (marker at 6// bit 7, so almost nothing is padding) and 0x01 (marker at bit 0, so the whole 7// final byte is consumed by the sentinel). A reader that assumes a fixed 8// padding width passes one and fails the other. 9// 10// T3 is the clean identity: with a final byte of 0x01 the readable data is 11// exactly the preceding bytes, so reading 8 bits must return that byte's own 12// value. Bits are packed LSB-first within a byte but the stream is walked 13// HIGH-to-LOW overall; only getting both right reproduces the byte. 14// 15// T6 pins the INFERRED LAST WEIGHT via KRAFT EQUALITY. zstd never stores the 16// final Huffman weight -- it is whatever completes the set to an exact power 17// of two. The check is that after completion, sum of 2^(tableLog - length) 18// over all present symbols equals 2^tableLog EXACTLY. A decoder that reads 19// only the stored weights builds a table missing its last symbol, decodes most 20// literals correctly, and produces one wrong byte wherever that symbol appears. 21// 22// license_tier: ORIGINAL 23import "nx_syscalls.nx" 24import "nx_zstd_bits.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 { g_puts("-" as *u8); x = 0 - x } 37 if x == 0 { buf[0] = 0x30 as u8; sys_write(1, buf, 1); return 1 } 38 let tmp: *u8 = sys_mmap(32) 39 var d: i64 = 0 40 while x > 0 { tmp[d] = ((x % 10) + 0x30) as u8; x = x / 10; d = d + 1 } 41 var i: i64 = 0 42 while i < d { buf[i] = tmp[d - 1 - i]; i = i + 1 } 43 sys_write(1, buf, d) 44 return d 45} 46 47func main() -> i64 { 48 var fails: i64 = 0 49 var mark: i64 = 0 50 51 // ---- T1: highest-set-bit, including the zero case ---- 52 if nx_zb_highbit8(0x80) != 7 { fails = fails + 1 } 53 if nx_zb_highbit8(0x81) != 7 { fails = fails + 1 } 54 if nx_zb_highbit8(0x01) != 0 { fails = fails + 1 } 55 if nx_zb_highbit8(0x40) != 6 { fails = fails + 1 } 56 if nx_zb_highbit8(0x1f) != 4 { fails = fails + 1 } 57 if nx_zb_highbit8(0x00) != (0 - 1) { fails = fails + 1 } 58 if fails > 0 { if mark == 0 { mark = 1 } } 59 60 // ---- T2: the SENTINEL, at opposite ends of the final byte ---- 61 let d1: *u8 = sys_mmap(64) 62 d1[0] = 0xab as u8; d1[1] = 0x81 as u8 63 let b1: *NxZstdBits = nx_zstd_bits_init(d1, 2) 64 if b1 == (0 as *NxZstdBits) { fails = fails + 1 } else { 65 // marker at bit 7 of byte 1 -> 15 readable bits below it 66 if nx_zstd_bits_remaining(b1) != 15 { fails = fails + 1 } 67 } 68 let d2: *u8 = sys_mmap(64) 69 d2[0] = 0xc3 as u8; d2[1] = 0x01 as u8 70 let b2: *NxZstdBits = nx_zstd_bits_init(d2, 2) 71 if b2 == (0 as *NxZstdBits) { fails = fails + 1 } else { 72 // marker at bit 0 of byte 1 -> the whole final byte is sentinel+padding 73 if nx_zstd_bits_remaining(b2) != 8 { fails = fails + 1 } 74 } 75 if fails > 0 { if mark == 0 { mark = 2 } } 76 77 // ---- T3: the identity case -- 8 bits back out as the byte itself ---- 78 if nx_zstd_bits_read(b2, 8) != 0xc3 { fails = fails + 1 } 79 if nx_zstd_bits_remaining(b2) != 0 { fails = fails + 1 } 80 if fails > 0 { if mark == 0 { mark = 3 } } 81 82 // ---- T4: a hand-computed walk down the 0xab 0x81 stream ---- 83 // bits 14..11 are byte1 bits 6..3 = 0,0,0,0 84 if nx_zstd_bits_read(b1, 4) != 0 { fails = fails + 1 } 85 // bits 10..7 = byte1 bits 2,1,0 then byte0 bit 7 = 0,0,1,1 86 if nx_zstd_bits_read(b1, 4) != 3 { fails = fails + 1 } 87 // bits 6..3 = byte0 bits 6,5,4,3 = 0,1,0,1 88 if nx_zstd_bits_read(b1, 4) != 5 { fails = fails + 1 } 89 // bits 2..0 = byte0 bits 2,1,0 = 0,1,1 90 if nx_zstd_bits_read(b1, 3) != 3 { fails = fails + 1 } 91 if nx_zstd_bits_remaining(b1) != 0 { fails = fails + 1 } 92 // reading past the end sets overflow rather than inventing bits 93 if nx_zstd_bits_read(b1, 1) != 0 { fails = fails + 1 } 94 if b1.overflow != 1 { fails = fails + 1 } 95 if fails > 0 { if mark == 0 { mark = 4 } } 96 97 // ---- T5: direct Huffman weights, high nibble FIRST ---- 98 let w: *u8 = sys_mmap(64) 99 w[0] = 0x21 as u8; w[1] = 0x43 as u8 100 let out: *i64 = sys_mmap(512 * 8) as *i64 101 // header 3 means FOUR weights 102 if nx_zstd_weights_direct(w, 2, 0, 3, out) != 4 { fails = fails + 1 } else { 103 if out[0] != 2 { fails = fails + 1 } 104 if out[1] != 1 { fails = fails + 1 } 105 if out[2] != 4 { fails = fails + 1 } 106 if out[3] != 3 { fails = fails + 1 } 107 } 108 // an odd count still fits in ceil(count/2) bytes 109 w[0] = 0x50 as u8 110 if nx_zstd_weights_direct(w, 2, 0, 0, out) != 1 { fails = fails + 1 } else { 111 if out[0] != 5 { fails = fails + 1 } 112 } 113 // a header at or above 128 is not the direct form 114 if nx_zstd_weights_direct(w, 2, 0, 128, out) != (0 - 1) { fails = fails + 1 } 115 // a buffer too short for the declared weight count 116 if nx_zstd_weights_direct(w, 1, 0, 3, out) != (0 - 1) { fails = fails + 1 } 117 if fails > 0 { if mark == 0 { mark = 5 } } 118 119 // ---- T6: the INFERRED last weight, checked by KRAFT EQUALITY ---- 120 out[0] = 2; out[1] = 1; out[2] = 4; out[3] = 3 121 let last: i64 = nx_zstd_weights_complete(out, 4) 122 // 2+1+8+4 = 15, next power of two is 16, remainder 1 -> weight 1 123 if last != 1 { fails = fails + 1 } 124 if out[4] != 1 { fails = fails + 1 } 125 let tl: i64 = nx_zstd_weights_tablelog(out, 5) 126 if tl != 4 { fails = fails + 1 } 127 128 let lens: *i64 = sys_mmap(512 * 8) as *i64 129 if nx_zstd_weights_to_lengths(out, 5, tl, lens) != 5 { fails = fails + 1 } else { 130 if lens[0] != 3 { fails = fails + 1 } 131 if lens[1] != 4 { fails = fails + 1 } 132 if lens[2] != 1 { fails = fails + 1 } 133 if lens[3] != 2 { fails = fails + 1 } 134 if lens[4] != 4 { fails = fails + 1 } 135 // KRAFT: sum of 2^(tableLog - length) must equal 2^tableLog EXACTLY 136 var kraft: i64 = 0 137 var i: i64 = 0 138 while i < 5 { 139 if lens[i] > 0 { kraft = kraft + (1 << (tl - lens[i])) } 140 i = i + 1 141 } 142 if kraft != (1 << tl) { fails = fails + 1 } 143 } 144 if fails > 0 { if mark == 0 { mark = 6 } } 145 146 // ---- T7: a second weight set, and Kraft again ---- 147 // 1+1+2 = 4, next power of two is 8, remainder 4 -> 2^(w-1)=4 -> weight THREE 148 out[0] = 1; out[1] = 1; out[2] = 2 149 if nx_zstd_weights_complete(out, 3) != 3 { fails = fails + 1 } 150 let tl2: i64 = nx_zstd_weights_tablelog(out, 4) 151 if tl2 != 3 { fails = fails + 1 } 152 if nx_zstd_weights_to_lengths(out, 4, tl2, lens) != 4 { fails = fails + 1 } else { 153 var kraft2: i64 = 0 154 var j: i64 = 0 155 while j < 4 { 156 if lens[j] > 0 { kraft2 = kraft2 + (1 << (tl2 - lens[j])) } 157 j = j + 1 158 } 159 if kraft2 != (1 << tl2) { fails = fails + 1 } 160 } 161 // a weight of ZERO means the symbol is ABSENT -- length 0, no Kraft mass 162 // 4 + 0 + 2 + 1 = 7, remainder 1 -> weight 1; the zero symbol is ABSENT 163 out[0] = 3; out[1] = 0; out[2] = 2; out[3] = 1 164 if nx_zstd_weights_complete(out, 4) < 0 { fails = fails + 1 } else { 165 let tl3: i64 = nx_zstd_weights_tablelog(out, 5) 166 if nx_zstd_weights_to_lengths(out, 5, tl3, lens) != 5 { fails = fails + 1 } else { 167 if lens[1] != 0 { fails = fails + 1 } 168 var kraft3: i64 = 0 169 var k: i64 = 0 170 while k < 5 { 171 if lens[k] > 0 { kraft3 = kraft3 + (1 << (tl3 - lens[k])) } 172 k = k + 1 173 } 174 if kraft3 != (1 << tl3) { fails = fails + 1 } 175 } 176 } 177 if fails > 0 { if mark == 0 { mark = 7 } } 178 179 // ---- T8 NEG: refusals ---- 180 // a final byte of ZERO carries no sentinel and is corrupt by definition 181 let z: *u8 = sys_mmap(64) 182 z[0] = 0xff as u8; z[1] = 0x00 as u8 183 if nx_zstd_bits_init(z, 2) != (0 as *NxZstdBits) { fails = fails + 1 } 184 // an empty buffer 185 if nx_zstd_bits_init(z, 0) != (0 as *NxZstdBits) { fails = fails + 1 } 186 // an all-zero weight set completes to nothing 187 out[0] = 0; out[1] = 0; out[2] = 0 188 if nx_zstd_weights_complete(out, 3) != (0 - 1) { fails = fails + 1 } 189 // a weight beyond the maximum table log 190 out[0] = 1; out[1] = 13 191 if nx_zstd_weights_complete(out, 2) != (0 - 1) { fails = fails + 1 } 192 // a weight set whose remainder is NOT a power of two is malformed: 193 // 4 + 4 + 2 = 10, next power of two is 16, remainder 6 -> not representable 194 out[0] = 3; out[1] = 3; out[2] = 2 195 if nx_zstd_weights_complete(out, 3) != (0 - 1) { fails = fails + 1 } 196 if fails > 0 { if mark == 0 { mark = 8 } } 197 198 if fails == 0 { 199 g_puts("GATE nx_zstd_bits verdict=GREEN pass=8/8 (highbit incl zero; SENTINEL found at BOTH ends of the final byte -- 0x81 leaves 15 readable bits, 0x01 leaves 8 so a fixed-padding reader cannot pass; identity read returns the byte itself; hand-computed 15-bit backward walk then overflow instead of invented bits; direct weights high-nibble-first with odd count and bad header refused; INFERRED last weight verified by KRAFT EQUALITY sum 2^(tableLog-len) == 2^tableLog on three weight sets incl a zero-weight absent symbol; NEG zero-final-byte/empty/all-zero-weights/oversize-weight/non-power-of-two-remainder refused)\n" as *u8) 200 sys_exit(0) 201 return 0 202 } 203 g_puts("GATE nx_zstd_bits verdict=RED fails=" as *u8) 204 g_putn(fails) 205 g_puts(" first_stage=" as *u8) 206 g_putn(mark) 207 g_puts("\n" as *u8) 208 sys_exit(1) 209 return 1 210}