test/f2a-span-verify.py

1#!/usr/bin/env python3

2"""F2a span verifier -- the instrument that decides whether the descriptor's

3spans are exact.

5WHY THIS IS IN PYTHON.

7The acceptance bar for F2a is that span exactness is MEASURED AGAINST SOURCE

8BYTES, not against the parse tree the spans came from. A checker written in

9Sigil, against the descriptor, would share the descriptor's reader, its

10coordinate arithmetic and its idea of where things are; it would agree with

11itself no matter what. That is instrument-failure taxonomy shape 13 in its real

12form -- not "we did not test enough" but "every instrument had the same blind

13spot, so their agreement was one measurement wearing several hats".

15This file opens the manuscript in BINARY mode and recomputes every offset from

16the file itself. It shares no code, no reader and no arithmetic with anything in

17`src/`. In particular `byte_start == len(text[:scalar_start].encode('utf-8'))`

18is computed here by Python's own codec, which is the assertion that a

19"compute the span from characters rather than bytes" regression cannot survive.

21IT MUST BE ABLE TO FAIL, AND IT PROVES THAT ON EVERY RUN. With

22`F2A_SPAN_VERIFY_SELFTEST=1` it corrupts one span in memory, after parsing and

23before checking, and requires its own machinery to report the failure. The gate

24runs both modes. A verifier that has only ever been green has not been shown to

25work; it has been shown to be quiet.

26"""

28import os

29import sys

32class Fail(Exception):

33 pass

36def die(msg):

37 print("F2A_SPAN_VERIFY RED: " + msg, file=sys.stderr)

38 sys.exit(1)

41def unescape(s):

42 out = []

43 i = 0

44 while i < len(s):

45 c = s[i]

46 if c == "\\" and i + 1 < len(s):

47 n = s[i + 1]

48 out.append({"t": "\t", "n": "\n", "r": "\r", "\\": "\\"}.get(n, n))

49 i += 2

50 else:

51 out.append(c)

52 i += 1

53 return "".join(out)

56class Row:

57 def __init__(self, tag, path, extra, span):

58 self.tag = tag

59 self.path = path

60 self.extra = extra

61 (self.byte_start, self.byte_len, self.scalar_start, self.scalar_end,

62 self.line, self.column, self.end_line, self.end_column) = span

65def num(v):

66 return None if v == "-" else int(v)

69def parse_manifest(lines):

70 header = {}

71 diagnostics = []

72 callables = []

73 rows = []

74 no_span = []

75 trailer = None

76 for raw in lines:

77 line = raw.rstrip("\n")

78 if not line:

79 continue

80 if line.startswith("F2A_MANIFEST_DONE "):

81 trailer = line

82 continue

83 parts = line.split("\t")

84 tag = parts[0]

85 if tag in ("SOURCE", "REVISION", "HEADER-END", "PARSED"):

86 header[tag] = parts[1] if len(parts) > 1 else ""

87 elif tag == "LENGTHS":

88 header["BYTE-LENGTH"] = parts[1]

89 header["SCALAR-LENGTH"] = parts[2]

90 elif tag == "DIAGNOSTIC":

91 diagnostics.append(parts[1:])

92 elif tag == "CALLABLE":

93 callables.append(parts[1])

94 elif tag == "FIELD-NO-SPAN":

95 no_span.append(parts[1:])

96 elif tag in ("NODE", "FIELD"):

97 span = [num(x) for x in parts[-8:]]

98 rows.append(Row(tag, parts[1], parts[2:-8], span))

99 else:

100 die("unknown manifest row tag %r" % tag)

101 return header, diagnostics, callables, rows, no_span, trailer

102

103

104def main():

105 if len(sys.argv) != 3:

106 die("usage: f2a-span-verify.py <manuscript> <manifest>")

107 manuscript, manifest_path = sys.argv[1], sys.argv[2]

108

109 raw = open(manuscript, "rb").read()

110 text = raw.decode("utf-8")

111 lines = open(manifest_path, "r", encoding="utf-8").read().splitlines(True)

112

113 header, diagnostics, callables, rows, no_span, trailer = parse_manifest(lines)

114

115 # ---- the manifest must be COMPLETE before any of it is graded ----------

116 # A truncated manifest is indistinguishable from the manifest of a small

117 # document, and every check below would pass on it.

118 if trailer is None:

119 die("manifest has no F2A_MANIFEST_DONE trailer; it is truncated, "

120 "and a truncated manifest passes every check below for free")

121 tparts = dict(p.split("=") for p in trailer.split()[1:])

122 nodes = [r for r in rows if r.tag == "NODE"]

123 fields = [r for r in rows if r.tag == "FIELD"]

124 if int(tparts["nodes"]) != len(nodes):

125 die("trailer claims %s nodes, manifest carries %d"

126 % (tparts["nodes"], len(nodes)))

127 if int(tparts["fields"]) != len(fields) + len(no_span):

128 die("trailer claims %s fields, manifest carries %d"

129 % (tparts["fields"], len(fields) + len(no_span)))

130 if no_span:

131 die("%d argument(s) carried no srcloc: %r" % (len(no_span), no_span))

132 if callables:

133 die("descriptor holds callable values at %r -- it is not inert data"

134 % callables)

135

136 # ---- the manifest must be ABOUT THE FILE WE WERE HANDED ---------------

137 # Nothing previously stopped `f2a-span-verify.py A.sgd B.manifest` from

138 # grading one document's spans against another document's bytes.

139 if header.get("SOURCE") != manuscript:

140 die("manifest is for %r but this run was handed %r"

141 % (header.get("SOURCE"), manuscript))

142 # And the REVISION contract gets a third independent implementation here,

143 # beside coreutils' sha256sum in the gate and whatever the caller used.

144 # `hashlib` is a different codebase from both; the contract is sha256 over

145 # the RAW FILE BYTES, so this is computable from `raw` alone.

146 import hashlib

147 expected_revision = "sha256:" + hashlib.sha256(raw).hexdigest()

148 if header.get("REVISION") != expected_revision:

149 die("descriptor carries revision %r; sha256 of the raw file bytes is %r"

150 % (header.get("REVISION"), expected_revision))

151

152 # ---- the file's own measurements --------------------------------------

153 if int(header["BYTE-LENGTH"]) != len(raw):

154 die("descriptor reports %s bytes, the file is %d"

155 % (header["BYTE-LENGTH"], len(raw)))

156 if int(header["SCALAR-LENGTH"]) != len(text):

157 die("descriptor reports %s scalars, the file decodes to %d"

158 % (header["SCALAR-LENGTH"], len(text)))

159

160 # Cumulative byte offsets, computed HERE, by Python's codec.

161 prefix = [0] * (len(text) + 1)

162 total = 0

163 for i, ch in enumerate(text):

164 prefix[i] = total

165 total += len(ch.encode("utf-8"))

166 prefix[len(text)] = total

167

168 # ---- selftest: corrupt one span, after parsing, before checking -------

169 selftest = os.environ.get("F2A_SPAN_VERIFY_SELFTEST") == "1"

170 if selftest:

171 if not nodes:

172 die("selftest requested but the manifest carries no nodes to corrupt")

173 nodes[0].byte_start += 1

174

175 checks = 0

176 failures = []

177 divergent_nodes = 0

178 divergent_fields = 0

179 # Rows that reached the END of their checks. Every `continue` below is a

180 # real finding AND a silent loss of coverage; without this counter a verifier

181 # that early-exited on every row would print `failed=0` and pass.

182 rows_verified = 0

183

184 def check(ok, msg):

185 nonlocal checks

186 checks += 1

187 if not ok:

188 failures.append(msg)

189

190 by_path = {}

191 for r in nodes:

192 by_path[r.path] = r

193

194 for r in rows:

195 where = "%s %s" % (r.tag, r.path)

196 bs, bl, ss, se = r.byte_start, r.byte_len, r.scalar_start, r.scalar_end

197 check(bs is not None and bl is not None, "%s: no byte span" % where)

198 if bs is None or bl is None:

199 continue

200 check(0 <= bs <= len(raw), "%s: byte start %d outside 0..%d" % (where, bs, len(raw)))

201 check(0 <= bs + bl <= len(raw),

202 "%s: byte end %d outside 0..%d" % (where, bs + bl, len(raw)))

203 if not (0 <= bs <= bs + bl <= len(raw)):

204 continue

205

206 # THE SLICE. Everything else is arithmetic; this is the thing itself.

207 chunk = raw[bs:bs + bl]

208 try:

209 decoded = chunk.decode("utf-8")

210 except UnicodeDecodeError as e:

211 failures.append("%s: byte slice [%d,%d) is not valid UTF-8 (%s) -- "

212 "the span starts or ends inside a multi-byte sequence"

213 % (where, bs, bs + bl, e))

214 checks += 1

215 continue

216 checks += 1

217

218 # A ROW WITH NO SCALAR COLUMNS IS A FAILURE, NOT A ROW TO SKIP.

219 # `index-scalar` returns #f only when a byte offset is not a scalar

220 # boundary, which is itself the defect this verifier exists to catch. The

221 # previous version put every scalar-dependent assertion behind

222 # `if ss is not None` with no `continue`, so such a row still counted as

223 # "verified to completion": five of its six checks were skipped and the

224 # summary said failed=0 over full coverage.

225 check(ss is not None and se is not None,

226 "%s: no scalar coordinates -- a byte offset that is not a scalar "

227 "boundary, which is a span defect, not a missing field" % where)

228 if ss is not None and se is not None:

229 check(prefix[ss] == bs,

230 "%s: byte start %d but scalar start %d encodes to byte %d"

231 % (where, bs, ss, prefix[ss]))

232 check(prefix[se] == bs + bl,

233 "%s: byte end %d but scalar end %d encodes to byte %d"

234 % (where, bs + bl, se, prefix[se]))

235 check(decoded == text[ss:se],

236 "%s: byte slice and scalar slice disagree" % where)

237 if prefix[ss] != ss:

238 if r.tag == "NODE":

239 divergent_nodes += 1

240 else:

241 divergent_fields += 1

242 # line/column, recomputed from the text

243 before = text[:ss]

244 check(r.line == before.count("\n") + 1,

245 "%s: line %s but the text has %d newlines before it"

246 % (where, r.line, before.count("\n")))

247 col = ss - (before.rfind("\n") + 1) + 1

248 check(r.column == col, "%s: column %s but recomputed %d" % (where, r.column, col))

249 # END line/column were emitted, parsed, and graded by nothing. A

250 # manifest claiming end-line 999 and end-column -4 passed with

251 # failed=0. They are recomputed here the same way the start is.

252 upto_end = text[:se]

253 end_line = upto_end.count("\n") + 1

254 end_col = se - (upto_end.rfind("\n") + 1) + 1

255 check(r.end_line == end_line,

256 "%s: end-line %s but recomputed %d" % (where, r.end_line, end_line))

257 check(r.end_column == end_col,

258 "%s: end-column %s but recomputed %d" % (where, r.end_column, end_col))

259

260 if r.tag == "NODE":

261 kind, name = r.extra[0], r.extra[1]

262 if kind == "command":

263 check(decoded.startswith("@" + name),

264 "%s: a command node's slice must start with @%s, got %r"

265 % (where, name, decoded[:24]))

266 # containment in the parent, and no overlap with the previous sibling

267 if "." in r.path:

268 parent = by_path.get(r.path.rsplit(".", 1)[0])

269 check(parent is not None, "%s: no parent row for this path" % where)

270 if parent is not None:

271 check(parent.byte_start <= bs and bs + bl <= parent.byte_start + parent.byte_len,

272 "%s: [%d,%d) is not contained in its parent's [%d,%d)"

273 % (where, bs, bs + bl, parent.byte_start,

274 parent.byte_start + parent.byte_len))

275 head, idx = r.path.rsplit(".", 1)

276 if int(idx) > 0:

277 prev = by_path.get("%s.%d" % (head, int(idx) - 1))

278 if prev is not None:

279 check(prev.byte_start + prev.byte_len <= bs,

280 "%s: overlaps its previous sibling, which ends at %d"

281 % (where, prev.byte_start + prev.byte_len))

282 else:

283 fname, _index, vtype, vtext = r.extra[0], r.extra[1], r.extra[2], unescape(r.extra[3])

284 parent = by_path.get(r.path)

285 check(parent is not None, "%s: no owning node row" % where)

286 if parent is not None:

287 check(parent.byte_start <= bs and bs + bl <= parent.byte_start + parent.byte_len,

288 "%s: field span [%d,%d) escapes its node's [%d,%d)"

289 % (where, bs, bs + bl, parent.byte_start,

290 parent.byte_start + parent.byte_len))

291 # A FIELD SPAN THAT EQUALS ITS NODE'S SPAN IS THE DEFECT THE PLAN

292 # NAMES: "a task's status span distinct from its body span".

293 check(not (bs == parent.byte_start and bl == parent.byte_len),

294 "%s: field span is identical to the whole node's span" % where)

295 if vtype == "string":

296 check(decoded.startswith('"') and decoded.endswith('"') and len(decoded) >= 2,

297 "%s: a string field's slice must be a quoted literal, got %r"

298 % (where, decoded))

299 if '"' not in vtext and "\\" not in vtext:

300 check(decoded == '"' + vtext + '"',

301 "%s: slice %r does not re-read to the recorded value %r"

302 % (where, decoded, vtext))

303 elif vtype == "symbol":

304 check(decoded == vtext or decoded == "'" + vtext,

305 "%s: slice %r is not the recorded symbol %r" % (where, decoded, vtext))

306 elif vtype == "number":

307 check(decoded.strip() == vtext,

308 "%s: slice %r is not the recorded number %r" % (where, decoded, vtext))

309 elif vtype == "boolean":

310 check(decoded.strip() in ("#t", "#f"),

311 "%s: slice %r is not a boolean literal" % (where, decoded))

312 elif vtype == "list":

313 check((decoded.startswith("'(") or decoded.startswith("(")) and decoded.endswith(")"),

314 "%s: slice %r is not a list form" % (where, decoded))

315

316 rows_verified += 1

317

318 # FAILURES ARE REPORTED BEFORE THE COVERAGE AND VACUITY DIES.

319 #

320 # They used to come last, so a single early-exiting row discarded every

321 # genuine finding on every other row and the transcript showed only a

322 # sentence about coverage. That is "red for the wrong reason" inside the

323 # phase's load-bearing instrument, and it made the sabotage driver's named

324 # signatures depend on which row happened to fail first.

325 if failures:

326 for f in failures[:25]:

327 print(" FAIL: " + f, file=sys.stderr)

328 if len(failures) > 25:

329 print(" ... and %d more" % (len(failures) - 25), file=sys.stderr)

330

331 # ---- NON-VACUITY. --------------------------------------------------------

332 # Without this the byte-versus-scalar assertions above are satisfied for free

333 # by any pure-ASCII manuscript, no matter what the code does: byte == scalar

334 # everywhere, so a characters-for-bytes bug is invisible. The corpus has to

335 # EARN this arm.

336 # NO ENV KNOB. An earlier draft made this floor configurable, which is the

337 # shape of taxonomy 21: a mandatory anti-vacuity rule that the format itself

338 # lets you satisfy trivially. A caller could have silenced the one check

339 # that makes every byte-versus-scalar assertion mean anything, by setting a

340 # variable. Instead EVERY fixture this verifier grades carries multi-byte

341 # text, and a fixture that does not is a fixture that must not be graded.

342 if divergent_nodes < 1:

343 die("only %d node span(s) have byte offset != scalar offset; this "

344 "manuscript cannot distinguish byte spans from character spans, so "

345 "the arm would pass with the arithmetic broken"

346 % divergent_nodes)

347

348 # COVERAGE IS ITSELF AN ASSERTION. "0 failures" over 3 of 95 rows is not a

349 # pass, and it is indistinguishable from a real pass in the summary line.

350 if rows_verified != len(rows):

351 die("only %d of %d manifest rows were verified to completion; the rest "

352 "took an early exit, so 'failed=0' describes a fraction of the "

353 "document" % (rows_verified, len(rows)))

354

355 # EVERY ROW MUST HAVE CONTRIBUTED CHECKS. `checks=` was reported and

356 # floored by nothing, so a verifier performing one check per row would print

357 # a plausible number and pass every assertion the gate makes.

358 if rows and checks < 2 * len(rows):

359 die("only %d checks over %d rows; the per-row assertions are not running"

360 % (checks, len(rows)))

361

362 if failures:

363 print("F2A_SPAN_VERIFY nodes=%d fields=%d divergent=%d divfields=%d checks=%d rows=%d failed=%d"

364 % (len(nodes), len(fields), divergent_nodes, divergent_fields, checks,

365 rows_verified, len(failures)))

366 sys.exit(1)

367

368 # `divergent` counts NODES specifically, because that is the number the

369 # unconditional floor above is written against. Reporting the node+field sum

370 # here while flooring on nodes would be a summary that does not describe the

371 # check it summarises.

372 print("F2A_SPAN_VERIFY nodes=%d fields=%d divergent=%d divfields=%d checks=%d rows=%d failed=0"

373 % (len(nodes), len(fields), divergent_nodes, divergent_fields, checks, rows_verified))

374

375

376if __name__ == "__main__":

377 main()