Skip to content

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

Merged
Kinflou merged 5 commits into
mainfrom
conformance/sizes
Nov 11, 2026
Merged

Kinflou merged 5 commits into
mainfrom
conformance/sizes

Conversation

@Kinflou

@Kinflou Kinflou commented Nov 10, 2026 •

Copy link
Copy Markdown
Member

Step 2 of per-format sizing (the plan: exact value sizes, and proof of the specification's size vectors against the real encoders).

Vendors the specification at 9a7142c395b2aefb7d4d77e9b36c74187c6f0199, the merge commit of ComlineProject/specification#4. Its witness bytes came from an independent model of the encoders, not from the runtime, and this PR first proved them against the real runtime while #4 was open (at f3df87b); every one of the 1,049 witnesses matched. The merge commit has the same content.

What it adds

  • WireFormat::encoded_len(&value) -> Result<usize, RuntimeError>, a default method on the trait. It runs encode into a CountBuf (the existing counting BufMut: no allocation, no_std), so it is the length of what encode writes by construction, and fails as encode does (a value over its bounds). json@1 and msgpack@1 write through std::io::Write over the same BufMut, so they count there too; no per-format counter is needed.
  • The size op in the conformance crate (Op::Size, Input::Size(SizeIn)):
    • a case has no bytes; questions asks the implementation one encode question per witness (as the case's type), so the ops protocol gains nothing and other runtimes answer the encodes they already do;
    • judge requires each answer to be exactly the witness's bytes, and the case to be self-consistent (min witness is min bytes, max witness max bytes, between in range, no max witness where max is null);
    • run also requires encoded_len to give each witness's length.
  • Type::FixedString { len } for {"fixed_string": {"len": N}} (char[N]), written as a string like the others.
  • sizes-packed, sizes-msgpack and sizes-json are claimed in support/rust.json and reported in reports/rust.json. Their vectors are written by the specification, so vectors_are_current doesn't regenerate them (a feature of only size cases is "proven, not produced").
  • size_rules_are_proven: every proven_by in a profile's sizes names a case that exists and passes.
  • Property tests: encoded_len(v) == encode(v).len() for random values in each format; a core test for the same and for a bound error.

Nothing to revert

origin/main has neither the comline-core dependency nor a format/size.rs stub (those are only in the local checkout's uncommitted work), so there is nothing to revert here. comline-runtime stays free of core. Cargo.lock is unchanged.

Test plan

CI only: the conformance crate's tests (rust_support_is_proven, size_rules_are_proven, the_runner_passes_the_reference, vectors_write_back_as_read), the reference process replay, the new properties, check.sh.

Kinflou added 5 commits November 11, 2026 07:49
…'s size vectors

encoded_len(&value) encodes into a CountBuf, so it is the length of what
encode writes by construction, with no allocation (packed@1 stays no_std);
JSON and MessagePack write through std::io::Write over the same sink.

The conformance crate reads the new `size` op: each witness's value is
encoded as the case's type (a new fixed_string, char[N], for it) and must give
the witness's bytes exactly, encoded_len must agree, and the case must say what
it holds. The sizes-* features are claimed and reported, a proptest checks
encoded_len against encode in every format, and each rule a profile's sizes
states is checked to be proven by passing cases.
@Kinflou
Kinflou marked this pull request as ready for review November 11, 2026 00:14
@Kinflou
Kinflou merged commit d9fc417 into main Nov 11, 2026
40 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant