Exact value sizes: encoded_len, and the specification's size vectors run against the encoders

runtime/conformance/README.md

@@ -62,6 +62,17 @@ find become `found-*` vectors; the fuzz README says how.
 `profiles_are_proven` checks that every case each profile fact names exists,
 passes against `comline-runtime`, and shows the stated value.
 
+The exception to "computed here" is the `sizes-*` features: their cases (a
+type, its byte range, and values that reach the ends of it with the bytes they
+encode to) are written in the specification, from a model of the encoders, and
+this runtime is what proves them. `run` asks the real encoders to write each
+witness's value as its type, requires exactly the witness's bytes, and
+requires `WireFormat::encoded_len` to give the witness's length;
+`size_rules_are_proven` holds every rule a profile's `sizes` states to cases
+that pass. A witness that disagrees with the encoder is a fault in the
+specification's vectors, fixed there, unless the encoder is what's wrong.
+`tests/properties.rs` checks `encoded_len` against `encode` over random values.
+
 ## Support, and its proof
 
 Rust's claims are in [`support/rust.json`](support/rust.json), held to the

runtime/conformance/reports/rust.json

@@ -566,6 +566,197 @@
         "name-hash/com.acme.custom-format"
       ]
     },
+    "sizes-json": {
+      "state": "supported",
+      "proven_by": [
+        "sizes-json/bool",
+        "sizes-json/u8",
+        "sizes-json/u16",
+        "sizes-json/u32",
+        "sizes-json/u64",
+        "sizes-json/u128",
+        "sizes-json/i8",
+        "sizes-json/i16",
+        "sizes-json/i32",
+        "sizes-json/i64",
+        "sizes-json/i128",
+        "sizes-json/f32",
+        "sizes-json/f64",
+        "sizes-json/char",
+        "sizes-json/unit",
+        "sizes-json/string-unbounded",
+        "sizes-json/string-max-0",
+        "sizes-json/string-max-1",
+        "sizes-json/string-max-3",
+        "sizes-json/string-max-7",
+        "sizes-json/string-max-8",
+        "sizes-json/string-max-31",
+        "sizes-json/string-max-32",
+        "sizes-json/string-max-63",
+        "sizes-json/string-max-64",
+        "sizes-json/string-fixed-3",
+        "sizes-json/string-fixed-8",
+        "sizes-json/string-fixed-32",
+        "sizes-json/array-unbounded",
+        "sizes-json/array-unbounded-strings",
+        "sizes-json/array-max-0",
+        "sizes-json/array-max-1",
+        "sizes-json/array-max-3",
+        "sizes-json/array-max-2-of-strings",
+        "sizes-json/array-max-3-of-options",
+        "sizes-json/fixed-4",
+        "sizes-json/fixed-1",
+        "sizes-json/fixed-2-of-strings",
+        "sizes-json/fixed-3-of-options",
+        "sizes-json/option-u8",
+        "sizes-json/option-bool",
+        "sizes-json/option-string",
+        "sizes-json/option-max-3-chars",
+        "sizes-json/option-struct",
+        "sizes-json/struct-point",
+        "sizes-json/struct-empty",
+        "sizes-json/struct-mixed",
+        "sizes-json/struct-nested",
+        "sizes-json/struct-15-fields",
+        "sizes-json/struct-16-fields",
+        "sizes-json/struct-long-names",
+        "sizes-json/enum-color",
+        "sizes-json/enum-single",
+        "sizes-json/enum-129-variants",
+        "sizes-json/enum-long-names",
+        "sizes-json/recursive-chain-3",
+        "sizes-json/recursive-tree-2"
+      ]
+    },
+    "sizes-msgpack": {
+      "state": "supported",
+      "proven_by": [
+        "sizes-msgpack/bool",
+        "sizes-msgpack/u8",
+        "sizes-msgpack/u16",
+        "sizes-msgpack/u32",
+        "sizes-msgpack/u64",
+        "sizes-msgpack/u128",
+        "sizes-msgpack/i8",
+        "sizes-msgpack/i16",
+        "sizes-msgpack/i32",
+        "sizes-msgpack/i64",
+        "sizes-msgpack/i128",
+        "sizes-msgpack/f32",
+        "sizes-msgpack/f64",
+        "sizes-msgpack/char",
+        "sizes-msgpack/unit",
+        "sizes-msgpack/string-unbounded",
+        "sizes-msgpack/string-max-0",
+        "sizes-msgpack/string-max-1",
+        "sizes-msgpack/string-max-3",
+        "sizes-msgpack/string-max-7",
+        "sizes-msgpack/string-max-8",
+        "sizes-msgpack/string-max-31",
+        "sizes-msgpack/string-max-32",
+        "sizes-msgpack/string-max-63",
+        "sizes-msgpack/string-max-64",
+        "sizes-msgpack/string-max-16384",
+        "sizes-msgpack/string-fixed-3",
+        "sizes-msgpack/string-fixed-8",
+        "sizes-msgpack/string-fixed-32",
+        "sizes-msgpack/array-unbounded",
+        "sizes-msgpack/array-unbounded-strings",
+        "sizes-msgpack/array-max-3",
+        "sizes-msgpack/array-max-15",
+        "sizes-msgpack/array-max-16",
+        "sizes-msgpack/array-max-2-of-strings",
+        "sizes-msgpack/array-max-3-of-options",
+        "sizes-msgpack/fixed-4",
+        "sizes-msgpack/fixed-15",
+        "sizes-msgpack/fixed-16",
+        "sizes-msgpack/fixed-1",
+        "sizes-msgpack/fixed-2-of-strings",
+        "sizes-msgpack/fixed-3-of-options",
+        "sizes-msgpack/option-u8",
+        "sizes-msgpack/option-bool",
+        "sizes-msgpack/option-string",
+        "sizes-msgpack/option-max-3-chars",
+        "sizes-msgpack/option-struct",
+        "sizes-msgpack/struct-point",
+        "sizes-msgpack/struct-empty",
+        "sizes-msgpack/struct-mixed",
+        "sizes-msgpack/struct-nested",
+        "sizes-msgpack/struct-15-fields",
+        "sizes-msgpack/struct-16-fields",
+        "sizes-msgpack/struct-long-names",
+        "sizes-msgpack/enum-color",
+        "sizes-msgpack/enum-single",
+        "sizes-msgpack/enum-129-variants",
+        "sizes-msgpack/enum-long-names",
+        "sizes-msgpack/recursive-chain-3",
+        "sizes-msgpack/recursive-tree-2"
+      ]
+    },
+    "sizes-packed": {
+      "state": "supported",
+      "proven_by": [
+        "sizes-packed/bool",
+        "sizes-packed/u8",
+        "sizes-packed/u16",
+        "sizes-packed/u32",
+        "sizes-packed/u64",
+        "sizes-packed/u128",
+        "sizes-packed/i8",
+        "sizes-packed/i16",
+        "sizes-packed/i32",
+        "sizes-packed/i64",
+        "sizes-packed/i128",
+        "sizes-packed/f32",
+        "sizes-packed/f64",
+        "sizes-packed/char",
+        "sizes-packed/unit",
+        "sizes-packed/string-unbounded",
+        "sizes-packed/string-max-0",
+        "sizes-packed/string-max-1",
+        "sizes-packed/string-max-3",
+        "sizes-packed/string-max-7",
+        "sizes-packed/string-max-8",
+        "sizes-packed/string-max-31",
+        "sizes-packed/string-max-32",
+        "sizes-packed/string-max-63",
+        "sizes-packed/string-max-64",
+        "sizes-packed/string-max-4095",
+        "sizes-packed/string-max-4096",
+        "sizes-packed/string-fixed-3",
+        "sizes-packed/string-fixed-8",
+        "sizes-packed/string-fixed-32",
+        "sizes-packed/array-unbounded",
+        "sizes-packed/array-unbounded-strings",
+        "sizes-packed/array-max-3",
+        "sizes-packed/array-max-127",
+        "sizes-packed/array-max-128",
+        "sizes-packed/array-max-2-of-strings",
+        "sizes-packed/array-max-3-of-options",
+        "sizes-packed/fixed-4",
+        "sizes-packed/fixed-1",
+        "sizes-packed/fixed-2-of-strings",
+        "sizes-packed/fixed-3-of-options",
+        "sizes-packed/option-u8",
+        "sizes-packed/option-bool",
+        "sizes-packed/option-string",
+        "sizes-packed/option-max-3-chars",
+        "sizes-packed/option-struct",
+        "sizes-packed/struct-point",
+        "sizes-packed/struct-empty",
+        "sizes-packed/struct-mixed",
+        "sizes-packed/struct-nested",
+        "sizes-packed/struct-15-fields",
+        "sizes-packed/struct-16-fields",
+        "sizes-packed/struct-long-names",
+        "sizes-packed/enum-color",
+        "sizes-packed/enum-single",
+        "sizes-packed/enum-129-variants",
+        "sizes-packed/enum-long-names",
+        "sizes-packed/recursive-chain-3",
+        "sizes-packed/recursive-tree-2"
+      ]
+    },
     "stream": {
       "state": "supported",
       "proven_by": [

runtime/conformance/spec/README.md

@@ -27,8 +27,8 @@ will read it.
 - [`features.json`](features.json), generated from the catalog: the wire
   features, with stable ids:
   `name-hash`, `handshake`, `envelope`, `framing-datagram`, `framing-datagram2`,
-  `framing-datagram3`, `handshake-comline2`, `framing-jsonrpc`, `stream`, `format-json`, `format-msgpack` and
-  `format-packed`.
+  `framing-datagram3`, `handshake-comline2`, `framing-jsonrpc`, `stream`, `format-json`, `format-msgpack`,
+  `format-packed`, `sizes-packed`, `sizes-msgpack` and `sizes-json`.
 - `vectors/<feature>.json`: that feature's cases.
 - [`benches/`](benches/README.md): the benchmarks every runtime runs, in the
   same value encoding.
@@ -62,6 +62,7 @@ The ops, and what their `input` holds:
 | `stream_prefix` | `len`, `max` | encode and decode: the 4-byte length prefix of a `len`-byte frame under the limit `max` |
 | `comline2_message` | a `comline@2` message: `type` (`hello`, `answer` or `verdict`) and `message` | encode and decode |
 | `comline2_negotiate` | `step`, and as the step needs `side`, `params`, `local` (this end's hello), `pending`; then `reply` and `result` | decode: `bytes`, the peer's message, run through `step` give exactly `reply` (the message this end sends, or `null`) and `result` (`accepted`, or `refused` with its reason and side) |
+| `size` | `format`, `type`, `min`, `max` (`null` for no bound), `witnesses`, and `upper_bound` when `max` is only a bound | encode: every witness's `value`, as `type`, gives its `bytes`, and a witness's length is as the case says (see [Sizes](#sizes)) |
 | `stream_split` | `max`, `frames`, `rest`, `needed` | encode and decode: a byte stream of `frames`, each behind its prefix, then `rest` |
 
 - **Encode and decode:** encoding the input gives exactly `bytes`, and decoding
@@ -309,6 +310,67 @@ check writes (`reports/<runtime>.json`) in its own repository, in the formats
 define. Rust's are in [`runtime/conformance`](https://github.com/ComlineProject/runtime/blob/main/runtime/conformance).
 
 
+## Sizes
+
+How many bytes each kind of value takes in a format is data too: each official
+format's `sizes` in the [catalog](catalog/readme.md#size-rules) (and in its
+profile, which must say the same), from which a compiler computes the least
+and most bytes a type can take, and every rule is proven by `size` cases in
+`vectors/sizes-<format>.json`.
+
+A `size` case gives a `type`, in the notation of a `decode` case's plus
+`{"fixed_string": {"len": N}}` for `char[N]`, a string of exactly N characters
+(`{"string"...}` of any kind counts characters, not bytes), the range
+`[min, max]` the rules give it in `format`, and values that encode to the
+ends of it, with the bytes each encodes to:
+
+```json
+{
+  "id": "sizes-msgpack/string-max-8",
+  "op": "size",
+  "input": {
+    "format": "msgpack@1",
+    "type": { "bounded_string": { "max": 8 } },
+    "min": 1,
+    "max": 34,
+    "witnesses": {
+      "min": { "value": { "string": "" }, "bytes": "a0" },
+      "max": { "value": { "string": "😀😀😀😀😀😀😀😀" }, "bytes": "d920f09f9880..." },
+      "between": [ { "value": { "string": "a" }, "bytes": "a161" } ]
+    }
+  }
+}
+```
+
+- `witnesses.min` encodes to exactly `min` bytes, and `witnesses.max` to exactly
+  `max`. Where `max` is `null` (no bound), no value reaches it and there is no
+  `max` witness. Where `upper_bound` is `true`, `max` is only a bound, which no
+  value is known to reach, and there is none either. No official format's rule
+  is one today: they are all reached.
+- `between` holds values that encode to lengths from `min` to `max`, at the
+  edges of a header's tiers where the format has them: a MessagePack string of 31
+  and 32 bytes, an array of 15 and 16 items, a varint's 127 and 128.
+- A witness's bytes are exactly what `value` encodes to as `type`, not just JSON
+  that is equal: the length of a float's text counts. Floats appear only where
+  `serde_json`'s older and newer float writers (`ryu`, `zmij`) print the same
+  text; a float in exponent notation, which they spell differently, has no
+  witness.
+- The runtime's `encode` writes the bytes of every witness: that run is the
+  proof of them, not this repository's checks. `specs/check.sh` checks what a
+  file alone can: every rule names `proven_by` cases that exist, are for its
+  format and have its kind of value in their type (a scalar's rule is proven by
+  the case of that scalar alone, with the same bounds), every case proves a
+  rule, and each witness is as long as its case says.
+
+What the vectors don't witness, and the rules say all the same, from the
+definitions of the formats: a varint of 4 or 5 bytes (a count from 2^21: a
+witness would be 2 MiB or more), and MessagePack's 5-byte array header (a count
+from 65536: 65,536 values, more than the spec tooling checks in reasonable
+time). A float's longest JSON text is witnessed (24 bytes for an `f64`, 16 for an
+`f32`), but that no float is longer follows from how `serde_json` writes one
+(at most 24 bytes in either writer, and 16 for an `f32`, where an exhaustive
+check of the decade that could be longer finds none), not from a vector.
+
 ## Encoding profiles
 
 [`profiles/`](profiles) holds one profile per official encoding name
@@ -317,7 +379,7 @@ define. Rust's are in [`runtime/conformance`](https://github.com/ComlineProject/
 `comline@2.json`): facts
 about how it encodes, which the version comparison turns into bumps. A format
 states `struct_fields`, `unknown_field`, `missing_optional`, `enum_variants`,
-`unknown_variant`, `integer_width` and `output`; a framing states `calls`,
+`unknown_variant`, `integer_width` and `output`, and may state `sizes`; a framing states `calls`,
 `directions`, `errors` and `payload`. The catalog gives each fact's values and
 what they mean ([`catalog/facts.cue`](catalog/facts.cue)).
 

runtime/conformance/spec/REV

@@ -1 +1 @@
-69d88327431275017ccce99fec43060467515a9f
+9a7142c395b2aefb7d4d77e9b36c74187c6f0199