code wiki / (root) / nx_webp_vp8l_gate.nx
`nx_webp_vp8l_gate.nx` source

↩ module page · 175 lines · 8483 B
1// nx_webp_vp8l_gate.nx -- proves the VP8L pixel-decoder math and the WebP
2// container walk.
3//
4// These are the pieces that decide whether a decoded image is CORRECT rather
5// than merely produced: the 14 predictors, the per-channel average, the
6// distance-plane mapping (VP8L's 2-D neighbourhood addressing, where an
7// off-by-one silently shifts every back-reference), the prefix-code value
8// rule, and the 5-byte header.
9//
10// NON-VACUITY: T10/T11/T12 are negative controls -- a non-RIFF buffer, a RIFF
11// that is not WEBP, and a bad VP8L signature must each be REFUSED. A decoder
12// that returns a plausible buffer for garbage is worse than one that returns
13// nothing.
14//
15// license_tier: ORIGINAL
16import "nx_syscalls.nx"
17import "nx_bitstream.nx"
18import "nx_huffman.nx"
19import "nx_webp_huff.nx"
20import "nx_webp_vp8l.nx"
21import "nx_webp.nx"
22
23func g_puts(s: *u8) -> i64 {
  var i: i64 = 0
  while s[i] != (0 as u8) { i = i + 1 }
  sys_write(1, s, i)
  return i
28}
29
30func main() -> i64 {
  var fails: i64 = 0
32
  // ---- T1: ceil-divide used for every sub-image size ----
  if vl_subsample_size(1, 0) != 1 { fails = fails + 1 }
  if vl_subsample_size(5, 2) != 2 { fails = fails + 1 }
  if vl_subsample_size(8, 3) != 1 { fails = fails + 1 }
  if vl_subsample_size(9, 3) != 2 { fails = fails + 1 }
38
  // ---- T2: per-channel average, no cross-channel carry ----
  // 0xff000000 and 0x00000000 -> alpha 127, everything else 0
  if vl_average2(0xff000000, 0x00000000) != 0x7f000000 { fails = fails + 1 }
  // 0x10203040 with itself is itself
  if vl_average2(0x10203040, 0x10203040) != 0x10203040 { fails = fails + 1 }
44
  // ---- T3: the trivial predictors select the right neighbour ----
  let L: i64 = 0x11111111
  let T: i64 = 0x22222222
  let TL: i64 = 0x33333333
  let TR: i64 = 0x44444444
  if vl_predict(0, L, T, TL, TR) != NX_VP8L_BLACK { fails = fails + 1 }
  if vl_predict(1, L, T, TL, TR) != L { fails = fails + 1 }
  if vl_predict(2, L, T, TL, TR) != T { fails = fails + 1 }
  if vl_predict(3, L, T, TL, TR) != TR { fails = fails + 1 }
  if vl_predict(4, L, T, TL, TR) != TL { fails = fails + 1 }
55
  // ---- T4: clamped add-subtract saturates instead of wrapping ----
  // 0xff + 0xff - 0x00 must clamp to 0xff, never wrap to 0xfe
  if vl_clamp_add_sub_full(0xffffffff, 0xffffffff, 0x00000000) != 0xffffffff { fails = fails + 1 }
  // 0x00 + 0x00 - 0xff must clamp to 0, never wrap high
  if vl_clamp_add_sub_full(0x00000000, 0x00000000, 0xffffffff) != 0x00000000 { fails = fails + 1 }
61
  // ---- T5: Select picks top when the gradient favours it ----
  // identical neighbours -> the rule returns top
  if vl_select(T, T, T) != T { fails = fails + 1 }
65
  // ---- T6: distance-plane mapping ----
  let plane: *i64 = sys_mmap(NX_VP8L_PLANE_CODES * 8 + 64) as *i64
  vl_plane_table(plane)
  // code 1 -> table[0]=0x18 -> y=1, x=8-8=0 -> dist = 1*xsize + 0
  if vl_dist_map(plane, 1, 32) != 32 { fails = fails + 1 }
  // code 2 -> table[1]=0x07 -> y=0, x=8-7=1 -> dist = 1
  if vl_dist_map(plane, 2, 32) != 1 { fails = fails + 1 }
  // beyond the plane table, distances are linear
  if vl_dist_map(plane, 121, 32) != 1 { fails = fails + 1 }
  if vl_dist_map(plane, 130, 32) != 10 { fails = fails + 1 }
  // a mapped distance can never be below 1 (would read forward)
  if vl_dist_map(plane, 97, 32) < 1 { fails = fails + 1 }
78
  // ---- T7: prefix-code values below 4 are literal ----
  let dummy: *u8 = sys_mmap(64)
  dummy[0] = 0x00 as u8; dummy[1] = 0x00 as u8; dummy[2] = 0x00 as u8; dummy[3] = 0x00 as u8
  let bsp: *NxBitStream = nx_bitstream_alloc(dummy, 4)
  if vl_prefix_value(bsp, 0) != 1 { fails = fails + 1 }
  if vl_prefix_value(bsp, 3) != 4 { fails = fails + 1 }
85
  // ---- T8: palette packing thresholds ----
  if wb_palette_bits(2) != 3 { fails = fails + 1 }
  if wb_palette_bits(4) != 2 { fails = fails + 1 }
  if wb_palette_bits(16) != 1 { fails = fails + 1 }
  if wb_palette_bits(17) != 0 { fails = fails + 1 }
91
  // ---- T9: the 5-byte VP8L header, hand-encoded ----
  // {0x2f, 0x0f, 0xc0, 0x01, 0x00} = sig, w-1=15, h-1=7, alpha=0, ver=0
  let hb: *u8 = sys_mmap(64)
  hb[0] = 0x2f as u8; hb[1] = 0x0f as u8; hb[2] = 0xc0 as u8
  hb[3] = 0x01 as u8; hb[4] = 0x00 as u8
  let bsh: *NxBitStream = nx_bitstream_alloc(hb, 5)
  let wh: *i64 = sys_mmap(64) as *i64
  if vp8l_read_header(bsh, wh) != 1 { fails = fails + 1 } else {
      if wh[0] != 16 { fails = fails + 1 }
      if wh[1] != 8 { fails = fails + 1 }
  }
103
  // ---- T10 NEG: a bad VP8L signature is REFUSED ----
  let bad: *u8 = sys_mmap(64)
  bad[0] = 0x2e as u8; bad[1] = 0x00 as u8; bad[2] = 0x00 as u8
  bad[3] = 0x00 as u8; bad[4] = 0x00 as u8
  let bsb: *NxBitStream = nx_bitstream_alloc(bad, 5)
  if vp8l_read_header(bsb, wh) != 0 { fails = fails + 1 }
110
  // ---- T11 NEG: a non-RIFF buffer decodes to nothing ----
  let nr: *u8 = sys_mmap(64)
  var k: i64 = 0
  while k < 32 { nr[k] = 0x41 as u8; k = k + 1 }
  if webp_decode(nr, 32, wh) != (0 as *i64) { fails = fails + 1 }
116
  // ---- T12 NEG: RIFF that is not WEBP (e.g. WAVE audio) is REFUSED ----
  let rw: *u8 = sys_mmap(64)
  rw[0] = 0x52 as u8; rw[1] = 0x49 as u8; rw[2] = 0x46 as u8; rw[3] = 0x46 as u8
  rw[8] = 0x57 as u8; rw[9] = 0x41 as u8; rw[10] = 0x56 as u8; rw[11] = 0x45 as u8
  k = 12
  while k < 32 { rw[k] = 0x00 as u8; k = k + 1 }
  if webp_decode(rw, 32, wh) != (0 as *i64) { fails = fails + 1 }
124
  // ---- T13 NEG: WEBP with no VP8L chunk is REFUSED (not guessed at) ----
  let nv: *u8 = sys_mmap(64)
  nv[0] = 0x52 as u8; nv[1] = 0x49 as u8; nv[2] = 0x46 as u8; nv[3] = 0x46 as u8
  nv[8] = 0x57 as u8; nv[9] = 0x45 as u8; nv[10] = 0x42 as u8; nv[11] = 0x50 as u8
  // a VP8 (lossy) chunk, which this decoder does not handle
  nv[12] = 0x56 as u8; nv[13] = 0x50 as u8; nv[14] = 0x38 as u8; nv[15] = 0x20 as u8
  nv[16] = 0x04 as u8; nv[17] = 0x00 as u8; nv[18] = 0x00 as u8; nv[19] = 0x00 as u8
  if webp_decode(nv, 32, wh) != (0 as *i64) { fails = fails + 1 }
133
  // ---- T14: inverse subtract-green adds green back into red and blue ----
  let px: *i64 = sys_mmap(64) as *i64
  px[0] = vl_argb(0xff, 0x10, 0x20, 0x30)
  vl_inv_subtract_green(px, 1)
  // red = 0x10 + 0x20 = 0x30, blue = 0x30 + 0x20 = 0x50, green unchanged
  if px[0] != vl_argb(0xff, 0x30, 0x20, 0x50) { fails = fails + 1 }
140
  // ---- T15: END-TO-END -- a complete 1x1 lossless WebP decoded to pixels ----
  // Hand-assembled to the spec, byte by byte, so the test depends on no
  // external fixture and no other decoder:
  //   RIFF(24) WEBP VP8L(12)
  //   header  2f | w-1=0 (14b) | h-1=0 (14b) | alpha=0 | ver=0
  //   stream  no transform, no colour cache, no meta image, then five
  //           SIMPLE one-symbol trees: G=64 R=32 B=16 A=255, dist=0
  // Every tree is single-symbol, so all five decode consuming ZERO bits --
  // this exercises the exact zero-bit path the huff gate isolates, but now
  // through the whole container -> stream -> pixel path.
  let f: *u8 = sys_mmap(64)
  f[0]=0x52 as u8;  f[1]=0x49 as u8;  f[2]=0x46 as u8;  f[3]=0x46 as u8
  f[4]=0x18 as u8;  f[5]=0x00 as u8;  f[6]=0x00 as u8;  f[7]=0x00 as u8
  f[8]=0x57 as u8;  f[9]=0x45 as u8;  f[10]=0x42 as u8; f[11]=0x50 as u8
  f[12]=0x56 as u8; f[13]=0x50 as u8; f[14]=0x38 as u8; f[15]=0x4c as u8
  f[16]=0x0c as u8; f[17]=0x00 as u8; f[18]=0x00 as u8; f[19]=0x00 as u8
  f[20]=0x2f as u8; f[21]=0x00 as u8; f[22]=0x00 as u8; f[23]=0x00 as u8
  f[24]=0x00 as u8; f[25]=0x28 as u8; f[26]=0x50 as u8; f[27]=0x41 as u8
  f[28]=0x0a as u8; f[29]=0xd1 as u8; f[30]=0xff as u8; f[31]=0x00 as u8
  let img: *i64 = webp_decode(f, 32, wh)
  if img == (0 as *i64) { fails = fails + 1 } else {
      if wh[0] != 1 { fails = fails + 1 }
      if wh[1] != 1 { fails = fails + 1 }
      if img[0] != vl_argb(255, 32, 64, 16) { fails = fails + 1 }
  }
166
  if fails == 0 {
      g_puts("GATE nx_webp_vp8l verdict=GREEN pass=15/15 (subsample; per-channel average; predictors 0-4; clamp saturates; Select; distance-plane map; prefix values; palette bits; header 16x8; NEG bad-sig/non-RIFF/RIFF-WAVE/no-VP8L refused; inverse subtract-green; END-TO-END 1x1 lossless WebP -> ARGB ff204010)\n" as *u8)
      sys_exit(0)
      return 0
  }
  g_puts("GATE nx_webp_vp8l verdict=RED\n" as *u8)
  sys_exit(1)
  return 1
175}
nx_webp_vp8l_gate.nx source

`nx_webp_vp8l_gate.nx` source
