wai-vector: the independent checker, written from the extension text alone, and a text fix (D7-4) #219
Loading…
Reference in a new issue
No description provided.
Delete branch "wai/d7-4-vector-checker"
Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?
D7-4 of D7: the independent conformance checker for
wai.graphics.vector,wai/tools/wai_vector_check.py, written from the extension text alone; its CI job; and a text fix tographics-vector.mdfor five places the checker had to infer. Stacked on nothing; based onmainat3af82118, which has #217's frame vectors.How it was written
wai/extensions/graphics-vector.md§1–§3 as merged; the notation ofinteger-operators.md§2 and SPEC §7 Digests, which that text cites; and the builder brief's §22.6 D7-4 entry for the deliverable list, CI and tests only.wai/wai-vector/; the D7-2 and D7-3 PR bodies and commits; review A'score.py; the design prototypes.99c12e84is the checker. I committed it before reading any corpus file's contents; until then I had seen only file names.dfa4d5d4is the corpus driver. I wrote it fromvector-conformance/README.md's layout and committed it before the first comparison run.alphaarithmetic vector's input is{"op":"alpha"}, and thevvalues it probes are listed only inexpected/arith/alpha.json. The driver reads thosevvalues and recomputes both quantisers at them.What it does
Python ≥ 3.11, standard library only, run with
python3 -I. It shares no code with the crate.Formats. It parses
WOS1andWVG1and writes each back from its fields, with every count derived and every zero field written as 0. It parses the §2.10 sidecar with a strict parser, re-serialises it, and compares bytes.Refusals. It applies §2.7's steps 1–9 and §2.1's checks 1–11, and reports the code and step of the first failure.
Load-time arithmetic. It computes the §3.4(a) interval check and the §3.4(b) cost, using a sweep in which ends come before starts at equal ticks.
Rendering. It renders R(P, S, z, r, g) using the closed forms in Python's big integers:
⌊(…)/4^n⌋and⌊(…)/8^n⌋;X(y) = xt + ⌊(y − yt)·dx/dy⌋;ya + ⌊(xc − xa)(yb − ya)/(xb − xa)⌋.It never uses the 32-bit forward-difference forms, so agreement on every frame confirms the DDA identity of §3.5–§3.6 on the corpus.
Bounds. It asserts §3.12's bounds on every value it forms, and in addition §3.7's per-fill
D_r ≤ 256·pand|d|, |v| ≤ 512·D_r.Self-test. It first recomputes the text's own worked examples and claims:
div255is half-up over [0, 65025], anddiv255(255x) = x;R_rat's quotient–remainder form;WOS1length at the caps is 31,457,312;Separately, the stated largest sidecar, 111,715 bytes, reproduces with each field at its own cap.
CI. The job
checkerinwai-vector.ymlruns onlinuxwith Python 3.11.wai/tools/wai_vector_*.pywas already in both path filters. The concurrency block is unchanged, and the job runscheck-workflow-concurrency.sh.Agreement
python3 -I tools/wai_vector_check.py corpus vector-conformanceunder Python 3.11.17 on the dev Mac, 2 min 43 s:sN-, "check N", "(step X before …)"), reported at that stepsha256.jsonentries recomputed (thediv255table, every frame list and clip)sidecar_malformed,sidecar_mismatchandlayer_mismatchThe corpus carries no §2.10 sidecar, so the sidecar row exercises the checker's sidecar code against real payloads. It is not a comparison with the crate.
Disagreements
The first comparison run produced two, and both were faults in the checker. The text is clear at each.
Wos1record lacked the slot that the load stores a set's bytes in. This is a checker bug, fixed infd3de87f.text_hash, 20 vectors. The field wastext_hash; every other field of these files agreed.canonical/{clusters, every-table, groups, groups-in-order, held, minimal, ruby, shared, sizes-rates};cost/{attack-b-one-item, ceiling, group, reused-path, touching-windows};geometry/{empty-glyph-edge, x-high-edge, x-low-edge, y-high-edge};refusals/{rich, s5f-string-newline}.canonical/minimalthe checker gavea980ddb4…, and the expected value ise3b0c442…, the SHA-256 of nothing, since that payload has no blocks.TEXTStable followed by theSTRINGSarea, exactly as carried".TEXTSoffset up toSTRINGS, which also takes inITEMS,GLYPHSandCLUSTERS. The text says the table, and is clear. Fixed infd3de87f. I did not copy the expected value: the fix is the slice §2.11 names.There are no crate bugs, and no disagreement caused by the text. After the fix, every file agrees, and the rendering groups were first compared after it.
Text fix (
9b6a4c58, a separate commit)There are five places where the checker had to infer a rule the text does not state. For the first four, the corpus pins the same reading the checker took. The fifth no vector reaches.
refusals/s1-shortandwos1-shortpin this.n_glyphs = 0withpoints_totalpast its cap isoutline_malformed, whichwos1-zero-glyphs-before-points-cappins. The old sentence set the cap rule and the zero rule apart, which reads as two passes.PATH.n_contours's upper bound,n_points, is a later field, and step 4 says no field's rule reads one. The text now saysn_contours ≥ 1atn_contours, andn_contours ≤ n_pointsatn_points, as §2.0 places them.rule0 with no clip" is now stated as checked atref, the later field.refusals/s4-item-rule-no-clippins "at ref".canonical/minimalwitht0 = 1anddur = 100at 25 fps loads, and gets level-1 probesg = 0andg = 1, both out of range.probesholds at least one entry.The checker implements fix 5. No corpus vector has an empty range, so fix 5 changes no comparison.
Falsifications
The checker was committed before these. Each one is a scratch copy of the committed checker with one rule broken, run against the worktree corpus.
fills/{triangle-af5, curves, star-*, random-*, negative, left-fold, comb-16382},runs/{marks, run-4096},composite/{clip-*, groups-depth-4, overlap-opacity},motion/lower-thirdand all fourslicing/*D_r ≤ 256·p, tightened by one (brief (b))fills/comb-16382and itssha256.jsonentry fail, at the bound, and nothing else does (318 of 319). The comb attainsD_r = 256·pexactly (gap 0)s2-*vector, which givepayload_malformedwheretoo_largeis expected; 19 pinned steps are reported as 3, not 2cost/touching-windowsis refused aspayload_malformedat step 9; the cost of the other 310 files does not changecomposite/j3-triplesandcomposite/overlap-opacitydiffer in theirRGBA8P,RGBA8Sand clip digestsBounds reached
These are the largest values the checker formed over the corpus, against §3.12:
D_r= 4,193,792 = 256 × 16,382, on the comb;|L|2^24, against its bound of 2^30;Checks
scripts/check-public-names.sh, with the private denylist from the environment: clean, over the whole tree and over the changed files.scripts/check-comparative-prose.sh: clean.scripts/check-wai-section-refs.py: clean, after the text fix.scripts/check-no-vanity-metrics.sh: clean.scripts/check-workflow-concurrency.sh: 22 workflows, each grouped per ref.Not covered
text_hash(§2.11), but no projection or transcript.🤖 Generated with Claude Code
The first comparison run found two faults in the checker, both mine; the text is clear on each: - text_hash hashed from the TEXTS offset up to STRINGS, taking in ITEMS, GLYPHS and CLUSTERS. Section 2.11: the TEXTS table followed by the STRINGS area. Fixed. - the Wos1 record lacked the slot the load stores a set's bytes in (a crash). Also: - section 3.7's per-fill bound D_r <= 256*p is asserted for every fill, with p its stored point count; fills/comb-16382 attains it (gap 0); - the corpus carries no section 2.10 sidecar, so for every accepted payload that renders, the driver builds the authoring tool's sidecar from the frames, parses and rewrites it, checks every probe and clip, and requires sidecar_malformed, sidecar_mismatch and layer_mismatch from three corruptions; - the probe set's level 1 takes the first and last frame only when the document has a frame at that rate, per the text fix that follows. Co-Authored-By: Claude Opus 5.5 <[email protected]>Found by writing the independent checker (D7-4) from this text alone. In each place the corpus already pins the reading the checker took; the text now states it. - section 2.7 step 1 and section 2.1 check 1: a payload shorter than its 80-byte header, and a set shorter than its 32-byte header, are refused at the first step (refusals/s1-short and wos1-short pin this). The text named only the fields such a file cannot hold. - section 2.1 check 2: the counts are taken one at a time, each against its whole range, so n_glyphs = 0 with points_total past its cap is outline_malformed (wos1-zero-glyphs-before-points-cap). The sentence listed the cap rule and the zero rule apart, which reads as two passes. - section 2.3 PATH: n_contours' upper bound n_points is a later field, which step 4 says no field's rule reads. It is now stated as n_contours >= 1 at n_contours and n_contours <= n_points at n_points, as section 2.0 places it. - section 2.4 ITEM, group begin: 'rule 0 with no clip' is checked at ref, the later field (refusals/s4-item-rule-no-clip pins 'at ref'). - section 2.10, the probe set: level 1 took the first and last frame even for a rate at which the document has none (the first exceeding the last), and the sidecar's own range check then refuses the tool's sidecar. No corpus vector has an empty range, so this one was found only by construction: canonical/minimal with t0 = 1 and dur = 100 at 25 fps loads, and gets level-1 probes g = 0 and 1. Level 1 now applies when the document has a frame at the rate, and a document with no frame at any covered pair has no sidecar, since probes holds at least one entry. Co-Authored-By: Claude Opus 5.5 <[email protected]>