[Kinflou]

Step 1 of per-format sizing: the specification states, as data, how many bytes each kind of value takes in packed@1, msgpack@1 and json@1, and vectors prove each rule.

What it adds

• sizes on a format's catalog entry (catalog/schema.cue, #Sizes; closed). Rule kinds, defined in catalog/readme.md:
  • scalars: [min, max] bytes per primitive (bool, u8..u128, s8..s128, f32, f64, char, unit);
  • headers: none, varint_leb128, msgpack_str, msgpack_array, delimited {before, after, between};
  • string (header on the byte length + body utf8 or json_escaped, 1-6 bytes a character), array, fixed_array;
  • option {none, some}, struct {header, key_extra?}, enum {tag: varint_index | name + header};
  • upper_bound on a width, for a max no witness reaches. No official rule needs it.
  • Not here, because no generator writes one: unions, and enums with fields (generated Rust refuses unions; enums are unit-only). Maps likewise.
• Profiles carry sizes (#FormatProfile.sizes?, optional for custom formats). For an official format #OfficialProfile requires them equal to the catalog's.
• Vectors: features sizes-packed, sizes-msgpack, sizes-json, new op size (59, 60 and 57 cases): a type (#SizeType, #Type plus fixed_string for char[N]), [min, max], and witnesses (min, max, and values between) with their bytes.
• specs/check.sh (with specs/sizes.jq, needs jq): every rule lists proven_by cases that exist, are in the rule's feature and format, and show its kind of value in their type; a scalar's rule is proven by that scalar's own case with the same bounds; every case proves a rule; every witness is exactly as long as min/max say, and between ones are in range; facts and sizes agree (struct_fields/key_extra, enum_variants/varint_index).
• comline-catalog crate: Encoding::sizes, Sizes and its parts, Header::len, sizes(id), generated by catalog/rust.cue; tests (packed u32 is [4, 4], msgpack u64 [1, 9], json s64 [1, 20], header tiers, every rule proven in its feature).
• Readmes: catalog (the rule definitions), specs, README (size op, Sizes section).

VERSION is not bumped.

The rules, from the runtime's code

• packed: fixed widths, char 1-4, unit 0; varint headers; option tag byte; struct no header; enum varint index.
• msgpack (rmp-serde): smallest-width ints (u64 1-9), u128/s128 as bin8 (18), char as a string (2-5), unit/absent option nil; present option is the value; struct is an array; enum is the variant's name as a string.
• json (serde_json): escapes ", \, controls (\b \t \n \f \r, others \u00xx), nothing else, so 6 bytes a character at worst; f64 is 3-24 bytes and f32 3-16; absent option null (4); struct an object with "name": keys.

What proves the bytes

The witnesses' bytes were produced by an independent model of the three encoders that reproduces all 138 existing format-* encode vectors, not by the runtime. The runtime run in step 2 is the real proof of the bytes, and any mismatch found there is fixed in the spec. check.sh here checks what a file alone can (lengths, references).

Not witnessed by a vector

• a varint of 4 or 5 bytes (a count from 2^21: a witness is 2 MiB or more);
• msgpack's 5-byte array header (count from 65536): 65,536 values make the CUE vet take minutes (quadratic), so the case is left out. msgpack's 5-byte string header is witnessed (string-max-16384, 65 KB);
• that no JSON float is longer than 24 (f64) / 16 (f32): the longest are witnessed, and the bound follows from serde_json's writers (24-byte buffer; an exhaustive check of the one decade that could give an f32 17 bytes finds none).

Float witnesses use only positional notation, which ryu and zmij (serde_json before and after 1.0.149) print identically.