nx_codec_caps_gate.nx source
↩ module page · 180 lines · 8541 B
1// nx_codec_caps_gate.nx -- proves the advertised header equals the capability.
2//
3// The property under test is an IFF, in both directions, over the whole
4// registry: a format appears in the emitted header if and only if we can
5// decode it. T1 walks every registry entry and checks both directions at
6// once, so neither an over-claim (advertise what we cannot read) nor an
7// under-claim (hide what we can) can survive.
8//
9// T3 and T4 pin the two live defects by name. `image/avif` and `br` were
10// being advertised by nx_http_client and nx_polite_browser respectively with
11// no decoder behind either. If someone flips those registry flags to 1
12// without landing the decoders, T1 still passes -- so T3/T4 assert the
13// SPECIFIC absence, and they are meant to be deleted by the same commit that
14// lands the decoder, not before.
15//
16// T7 is the non-vacuity control: an unknown format must answer 0, not a
17// plausible 1. If the query answered 1 for anything it did not recognise,
18// T1's forward direction would be satisfiable by an empty registry.
19//
20// license_tier: ORIGINAL
21import "nx_syscalls.nx"
22import "nx_codec_caps.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 let tmp: *u8 = sys_mmap(32)
34 var x: i64 = v
35 var d: i64 = 0
36 var i: i64 = 0
37 if x < 0 { g_puts("-" as *u8); x = 0 - x }
38 if x == 0 { buf[0] = 0x30 as u8; sys_write(1, buf, 1); return 1 }
39 while x > 0 { tmp[d] = ((x % 10) + 0x30) as u8; x = x / 10; d = d + 1 }
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 var i: i64 = 0
49 var present: i64 = 0
50 var declared: i64 = 0
51 var avail: i64 = 0
52
53 let img: *u8 = sys_mmap(1024)
54 let enc: *u8 = sys_mmap(512)
55 let doc: *u8 = sys_mmap(2048)
56 let hdr: *u8 = sys_mmap(4096)
57
58 nx_codec_caps_accept_image(img)
59 nx_codec_caps_accept_encoding(enc)
60 nx_codec_caps_accept_document(doc)
61 nx_codec_caps_headers(hdr)
62
63 // ---- T1: IN THE HEADER IFF WE CAN DECODE IT (images) ----
64 i = 0
65 avail = 0
66 while i < NX_CC_N_IMAGE {
67 present = 0
68 if nx_cc_find(img, cc_image_name(i)) >= 0 { present = 1 }
69 declared = cc_image_have(i)
70 if present != declared { fails = fails + 1 }
71 // the query and the table must agree too, or the header could be
72 // right while callers asking "can we decode X" get the wrong answer
73 if nx_codec_caps_have_image(cc_image_name(i)) != declared { fails = fails + 1 }
74 if declared == 1 { avail = avail + 1 }
75 i = i + 1
76 }
77 // exactly as many tokens as the registry says are available -- catches a
78 // hand-added entry that no registry row backs
79 if nx_cc_count_tokens(img) != avail { fails = fails + 1 }
80 if fails > 0 { if mark == 0 { mark = 1 } }
81
82 // ---- T2: same IFF over the encodings ----
83 i = 0
84 avail = 0
85 while i < NX_CC_N_ENCODING {
86 present = 0
87 if nx_cc_find(enc, cc_encoding_name(i)) >= 0 { present = 1 }
88 declared = cc_encoding_have(i)
89 if present != declared { fails = fails + 1 }
90 if nx_codec_caps_have_encoding(cc_encoding_name(i)) != declared { fails = fails + 1 }
91 if declared == 1 { avail = avail + 1 }
92 i = i + 1
93 }
94 if nx_cc_count_tokens(enc) != avail { fails = fails + 1 }
95 if fails > 0 { if mark == 0 { mark = 2 } }
96
97 // ---- T3: the nx_http_client defect, pinned by name ----
98 // three fetchers send `image/avif` today with no AVIF pixel codec
99 if nx_codec_caps_have_image("image/avif" as *u8) != 0 { fails = fails + 1 }
100 if nx_cc_find(img, "image/avif" as *u8) >= 0 { fails = fails + 1 }
101 if nx_cc_find(doc, "image/avif" as *u8) >= 0 { fails = fails + 1 }
102 if nx_cc_find(hdr, "image/avif" as *u8) >= 0 { fails = fails + 1 }
103 // ...while webp, which we DID build this session, must now be claimed
104 if nx_codec_caps_have_image("image/webp" as *u8) != 1 { fails = fails + 1 }
105 if nx_cc_find(img, "image/webp" as *u8) < 0 { fails = fails + 1 }
106 if fails > 0 { if mark == 0 { mark = 3 } }
107
108 // ---- T4: the nx_polite_browser defect, pinned by name ----
109 if nx_codec_caps_have_encoding("br" as *u8) != 0 { fails = fails + 1 }
110 if nx_cc_find(enc, "br" as *u8) >= 0 { fails = fails + 1 }
111 if nx_cc_find(hdr, "br" as *u8) >= 0 { fails = fails + 1 }
112 // zstd has ten gated modules but no proven bytes -- an unproven decoder
113 // is not a capability, and must not be advertised
114 if nx_codec_caps_have_encoding("zstd" as *u8) != 0 { fails = fails + 1 }
115 if nx_cc_find(enc, "zstd" as *u8) >= 0 { fails = fails + 1 }
116 if fails > 0 { if mark == 0 { mark = 4 } }
117
118 // ---- T5: the OPPOSITE defect -- capability left on the floor ----
119 // nine fetchers send `Accept-Encoding: identity` while inflate exists
120 if nx_codec_caps_have_encoding("gzip" as *u8) != 1 { fails = fails + 1 }
121 if nx_cc_find(enc, "gzip" as *u8) < 0 { fails = fails + 1 }
122 if nx_codec_caps_have_encoding("deflate" as *u8) != 1 { fails = fails + 1 }
123 if nx_cc_find(enc, "deflate" as *u8) < 0 { fails = fails + 1 }
124 if fails > 0 { if mark == 0 { mark = 5 } }
125
126 // ---- T6: the header is never empty and never malformed ----
127 if nx_cc_len(enc) == 0 { fails = fails + 1 }
128 if nx_cc_len(img) == 0 { fails = fails + 1 }
129 // identity is true by construction and must always answer yes
130 if nx_codec_caps_have_encoding("identity" as *u8) != 1 { fails = fails + 1 }
131 // the document Accept must SPLICE the image list, not restate it
132 if nx_cc_find(doc, img) < 0 { fails = fails + 1 }
133 // and the composed block must carry both headers, CRLF-terminated
134 if nx_cc_find(hdr, "Accept: " as *u8) < 0 { fails = fails + 1 }
135 if nx_cc_find(hdr, "Accept-Encoding: " as *u8) < 0 { fails = fails + 1 }
136 if nx_cc_find(hdr, doc) < 0 { fails = fails + 1 }
137 if nx_cc_find(hdr, enc) < 0 { fails = fails + 1 }
138 if fails > 0 { if mark == 0 { mark = 6 } }
139
140 // ---- T7 NEG: an unknown format answers 0, never a plausible 1 ----
141 if nx_codec_caps_have_image("image/jxl" as *u8) != 0 { fails = fails + 1 }
142 if nx_codec_caps_have_image("" as *u8) != 0 { fails = fails + 1 }
143 if nx_codec_caps_have_encoding("lzma" as *u8) != 0 { fails = fails + 1 }
144 // a name that is a PREFIX of a real one must not match it
145 if nx_codec_caps_have_image("image/web" as *u8) != 0 { fails = fails + 1 }
146 if nx_codec_caps_have_encoding("gzi" as *u8) != 0 { fails = fails + 1 }
147 // ...and a name that CONTAINS a real one must not match either
148 if nx_codec_caps_have_encoding("gzipx" as *u8) != 0 { fails = fails + 1 }
149 if fails > 0 { if mark == 0 { mark = 7 } }
150
151 // ---- T8 NEG: the find primitive itself can fail ----
152 if nx_cc_find("abc" as *u8, "d" as *u8) != (0 - 1) { fails = fails + 1 }
153 if nx_cc_find("abc" as *u8, "abcd" as *u8) != (0 - 1) { fails = fails + 1 }
154 if nx_cc_find("abc" as *u8, "c" as *u8) != 2 { fails = fails + 1 }
155 if nx_cc_find("abc" as *u8, "abc" as *u8) != 0 { fails = fails + 1 }
156 if nx_cc_eq("a" as *u8, "ab" as *u8) != 0 { fails = fails + 1 }
157 if nx_cc_eq("ab" as *u8, "ab" as *u8) != 1 { fails = fails + 1 }
158 if nx_cc_count_tokens("" as *u8) != 0 { fails = fails + 1 }
159 if nx_cc_count_tokens("a" as *u8) != 1 { fails = fails + 1 }
160 if nx_cc_count_tokens("a,b,c" as *u8) != 3 { fails = fails + 1 }
161 if fails > 0 { if mark == 0 { mark = 8 } }
162
163 if fails == 0 {
164 g_puts("GATE nx_codec_caps verdict=GREEN pass=8/8 (a format is IN the emitted header IFF a decoder exists -- checked in BOTH directions over every registry row, with a token count so a hand-added entry has nowhere to hide; the two live lies pinned by name: image/avif absent from Accept and br absent from Accept-Encoding, zstd withheld because its bytes are unproven; the opposite defect closed too -- gzip and deflate now advertised where nine fetchers sent identity; unknown/prefix/superstring names all answer 0; find and eq proven able to fail)\n" as *u8)
165 sys_exit(0)
166 return 0
167 }
168 g_puts("GATE nx_codec_caps verdict=RED fails=" as *u8)
169 g_putn(fails)
170 g_puts(" first_stage=" as *u8)
171 g_putn(mark)
172 g_puts("\n" as *u8)
173 g_puts(" accept_image=" as *u8)
174 g_puts(img)
175 g_puts("\n accept_encoding=" as *u8)
176 g_puts(enc)
177 g_puts("\n" as *u8)
178 sys_exit(1)
179 return 1
180}