From 924d18e3267a2ad8c4a5d371fa7edfe24aa1d99c Mon Sep 17 00:00:00 2001 From: younes-io Date: Tue, 6 Oct 2026 18:32:47 +0200 Subject: [PATCH 1/9] Add the CBOR module's encoder with golden tests ToCBOR returns the CBOR (RFC 8949) encoding of any finite TLA+ value as a sequence of integers in 0..255, and CBORSerialize writes the same bytes to a file, so harnesses in Go, Rust, TypeScript and Python can read TLC values without the type loss of JSON. Sets, model values and functions with non-string domains keep their TLA+ meaning. Equal values encode as identical bytes. The encoder decides how a function is written from its domain, not from its Java class, and sorts set elements and keys by their encoded bytes instead of by TLC's intern order. It never normalizes the values it reads. CBORTests writes each golden inline as a sequence of hex literals and requires ToCBOR to return exactly those bytes, for every row of the encoding table and for groups of TLC-equal values held in different Java classes. tests/CBORTests/fixtures.py is a second encoder that shares no code with CBOR.java; run by hand, it checks every golden sequence in CBORTests.tla against its own output. FromCBOR and CBORDeserialize keep their fallback bodies until the decoder lands. https://github.com/tlaplus/tlaplus/issues/1467 [Feature] Signed-off-by: younes-io --- modules/CBOR.tla | 92 ++++++ modules/tlc2/overrides/CBOR.java | 343 +++++++++++++++++++++++ modules/tlc2/overrides/TLCOverrides.java | 5 +- tests/AllTests.tla | 1 + tests/CBORTests.tla | 153 ++++++++++ tests/CBORTests/empty-object.json | 1 + tests/CBORTests/fixtures.py | 181 ++++++++++++ 7 files changed, 774 insertions(+), 2 deletions(-) create mode 100644 modules/CBOR.tla create mode 100644 modules/tlc2/overrides/CBOR.java create mode 100644 tests/CBORTests.tla create mode 100644 tests/CBORTests/empty-object.json create mode 100644 tests/CBORTests/fixtures.py diff --git a/modules/CBOR.tla b/modules/CBOR.tla new file mode 100644 index 0000000..dcd7c0f --- /dev/null +++ b/modules/CBOR.tla @@ -0,0 +1,92 @@ +-------------------------------- MODULE CBOR -------------------------------- +(***************************************************************************) +(* Encodes TLA+ values as CBOR (RFC 8949), either as a sequence of bytes *) +(* or in a file, and decodes them back. Any finite TLA+ value v survives *) +(* the round trip: *) +(* *) +(* FromCBOR(ToCBOR(v)) = v *) +(* CBORSerialize(f, v) => CBORDeserialize(f) = v *) +(* *) +(* TLC implements all four operators in Java (tlc2.overrides.CBOR in the *) +(* CommunityModules). The definitions below only stop TLC with an error *) +(* message when that implementation is not on TLC's classpath. *) +(* *) +(* Encoding. Every value has exactly one encoding, so values that TLC *) +(* considers equal are written as identical bytes: *) +(* *) +(* integer CBOR integer (major type 0 or 1) *) +(* TRUE, FALSE CBOR true, false *) +(* string CBOR text string (UTF-8) *) +(* model value tag 39 around its name as a text string *) +(* set tag 258 around an array of its elements *) +(* function f with DOMAIN f = 1..n, including every sequence, every *) +(* tuple, and the empty function *) +(* array of f[1], ..., f[n] *) +(* function f whose domain is a non-empty set of strings (a record) *) +(* map from each x \in DOMAIN f to f[x] *) +(* any other function f *) +(* tag 33000 around an array of the pairs *) +(* [x, f[x]], one for each x \in DOMAIN f *) +(* *) +(* The elements of a set, the keys of a map, and the pairs of tag 33000 *) +(* are sorted by their encoded bytes (RFC 8949, section 4.2.1). This is *) +(* not length-first order: the key "z" precedes "aa", and the integer 10 *) +(* precedes -1. Integers and lengths use their shortest form, and all *) +(* lengths are definite. *) +(* *) +(* A CBOR map always holds a record, so a decoder in any language can *) +(* read it into a native dictionary or struct. Functions keyed by *) +(* integers, model values, tuples, sets, or records use tag 33000 because *) +(* the default decoders of several languages (Go, JavaScript) fail on CBOR *) +(* maps whose keys are arrays or tagged items. *) +(* *) +(* Producers in other languages need not sort anything, because FromCBOR *) +(* and CBORDeserialize read elements, keys, and pairs in any order. The *) +(* "canonical" modes of CBOR libraries agree with this module on maps, *) +(* whose keys are all strings, but not on sets or tag 33000, which they *) +(* sort length-first. A producer that wants byte-identical output must *) +(* sort by encoded bytes as RFC 8949, section 4.2.1 says. *) +(* *) +(* FromCBOR and CBORDeserialize also read integers and lengths that are *) +(* not in shortest form, and maps whose keys are not strings. They reject *) +(* duplicate set elements and duplicate keys, integers that TLC cannot *) +(* represent (outside -2^31 .. 2^31-1), floating-point numbers, byte *) +(* strings, null, undefined, indefinite lengths, other tags, invalid *) +(* UTF-8, data items nested more than 512 deep, and bytes after the first *) +(* data item. A model value must be defined in the model (for example in *) +(* the configuration file); neither operator creates one. *) +(***************************************************************************) + +LOCAL INSTANCE TLC + +(***************************************************************************) +(* The CBOR encoding of value as a sequence of integers in 0..255, one per *) +(* byte. If value cannot be encoded (an infinite set, an operator, a *) +(* string that is not valid Unicode), TLC reports an error. *) +(***************************************************************************) +ToCBOR(value) == + Assert(FALSE, "ToCBOR needs CommunityModules.jar on TLC's classpath.") + +(***************************************************************************) +(* The TLA+ value of the CBOR data item in bytes, a sequence of integers *) +(* in 0..255. *) +(***************************************************************************) +FromCBOR(bytes) == + Assert(FALSE, "FromCBOR needs CommunityModules.jar on TLC's classpath.") + +(***************************************************************************) +(* Writes the bytes of ToCBOR(value) to the file absoluteFilename and *) +(* equals TRUE. Creates missing parent directories and replaces an *) +(* existing file. If value cannot be encoded, TLC reports an error and *) +(* leaves the file untouched. *) +(***************************************************************************) +CBORSerialize(absoluteFilename, value) == + Assert(FALSE, "CBORSerialize needs CommunityModules.jar on TLC's classpath.") + +(***************************************************************************) +(* FromCBOR applied to the bytes of the file absoluteFilename. *) +(***************************************************************************) +CBORDeserialize(absoluteFilename) == + Assert(FALSE, "CBORDeserialize needs CommunityModules.jar on TLC's classpath.") + +============================================================================= diff --git a/modules/tlc2/overrides/CBOR.java b/modules/tlc2/overrides/CBOR.java new file mode 100644 index 0000000..19cd1ff --- /dev/null +++ b/modules/tlc2/overrides/CBOR.java @@ -0,0 +1,343 @@ +/******************************************************************************* + * Copyright (c) 2026 Younes Akhouayri. All rights reserved. + * + * The MIT License (MIT) + * + * Permission is hereby granted, free of charge, to any person obtaining a copy + * of this software and associated documentation files (the "Software"), to deal + * in the Software without restriction, including without limitation the rights + * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies + * of the Software, and to permit persons to whom the Software is furnished to do + * so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS + * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR + * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN + * AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION + * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + * + * Contributors: + * Younes Akhouayri - initial API and implementation + ******************************************************************************/ +package tlc2.overrides; + +import java.io.ByteArrayOutputStream; +import java.io.IOException; +import java.nio.ByteBuffer; +import java.nio.CharBuffer; +import java.nio.charset.CharacterCodingException; +import java.nio.charset.StandardCharsets; +import java.nio.file.Files; +import java.nio.file.InvalidPathException; +import java.nio.file.Path; +import java.nio.file.Paths; +import java.util.Arrays; + +import tlc2.output.EC; +import tlc2.tool.EvalException; +import tlc2.value.Values; +import tlc2.value.impl.BoolValue; +import tlc2.value.impl.EnumerableValue; +import tlc2.value.impl.FcnLambdaValue; +import tlc2.value.impl.FcnRcdValue; +import tlc2.value.impl.IntValue; +import tlc2.value.impl.ModelValue; +import tlc2.value.impl.RecordValue; +import tlc2.value.impl.SetEnumValue; +import tlc2.value.impl.StringValue; +import tlc2.value.impl.TupleValue; +import tlc2.value.impl.Value; + +/** + * Module overrides for CBOR.tla: encode a finite TLA+ value as CBOR (RFC 8949), as a sequence of bytes or + * in a file, and decode it back. CBOR.tla documents the encoding; this class is its only implementation. + * + *

There is no intermediate data model. {@link Encoder} walks TLC values and writes bytes, and the + * operators are thin shells around it. Both directions decide how a function is written by one rule, + * {@link #shape(Value[])}. The class depends only on TLC and the JDK. + * + *

Every error is an {@link EvalException}, never a Java exception that TLC would wrap as error 2154. + * A wrong argument type uses the CommunityModules argument codes; errors about a value or a file use + * {@link EC#GENERAL}, whose message TLC prints verbatim. + */ +public final class CBOR { + + private CBOR() { + } + + // Major types, RFC 8949 section 3.1. + private static final int UNSIGNED = 0, NEGATIVE = 1, TEXT = 3, ARRAY = 4, MAP = 5, TAG = 6; + + /** IANA tag 39, "Identifier", around a model value's name. */ + private static final int TAG_MODEL_VALUE = 39; + /** IANA tag 258, "Mathematical finite set", around the array of a set's elements. */ + private static final int TAG_SET = 258; + /** + * Around the [x, f[x]] pairs of a function that is neither a sequence nor a record. Not yet registered + * with IANA; 33000 lies in the First Come First Served range. CBOR.tla is the only other place that + * names it. + */ + private static final int TAG_FUNCTION = 33000; + + /** + * Guards file reads and writes, not encoding, so that a read in one worker never sees half of + * another worker's write to the same file. + */ + private static final Object FILES = new Object(); + + /** How a function is written. TLC equates functions across Java classes, so only the domain decides. */ + private enum Shape { + /** DOMAIN f = 1..n for some n >= 0: an array. Includes the empty function and the empty record. */ + SEQUENCE, + /** A non-empty set of strings: a map keyed by text. */ + RECORD, + /** Anything else: tag 33000 around [x, f[x]] pairs. */ + PAIRS + } + + private static Shape shape(final Value[] domain) { + final boolean[] seen = new boolean[domain.length + 1]; + int indices = 0; + boolean strings = domain.length > 0; + for (final Value d : domain) { + strings &= d instanceof StringValue; + if (d instanceof IntValue) { + final int i = ((IntValue) d).val; + if (1 <= i && i <= domain.length && !seen[i]) { + seen[i] = true; + indices++; + } + } + } + return indices == domain.length ? Shape.SEQUENCE : strings ? Shape.RECORD : Shape.PAIRS; + } + + @TLAPlusOperator(identifier = "ToCBOR", module = "CBOR", warn = false) + public static TupleValue toCBOR(final Value value) { + final byte[] bytes = Encoder.encode(value, "ToCBOR"); + final Value[] elems = new Value[bytes.length]; + for (int i = 0; i < elems.length; i++) { + elems[i] = IntValue.gen(bytes[i] & 0xff); + } + return new TupleValue(elems); + } + + /** + * Encodes the whole value before it touches the file, so a value it refuses leaves an existing file + * as it was. + */ + @TLAPlusOperator(identifier = "CBORSerialize", module = "CBOR", warn = false) + public static BoolValue serialize(final Value absoluteFilename, final Value value) { + if (!(absoluteFilename instanceof StringValue)) { + throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, + new String[] { "first", "CBORSerialize", "string", Values.ppr(absoluteFilename.toString()) }); + } + final String file = ((StringValue) absoluteFilename).val.toString(); + final byte[] bytes = Encoder.encode(value, "CBORSerialize"); + synchronized (FILES) { + try { + final Path path = Paths.get(file); + final Path parent = path.toAbsolutePath().getParent(); + if (parent != null) { + Files.createDirectories(parent); + } + Files.write(path, bytes); + } catch (IOException | InvalidPathException e) { + throw new EvalException(EC.GENERAL, "CBORSerialize could not write " + file + ": " + e + "."); + } + } + return BoolValue.ValTrue; + } + + /** + * Writes the one encoding of a TLC value. Values that TLC considers equal produce identical bytes, + * whatever their Java class and whatever order TLC interned their strings in, so the encoder sorts by + * encoded bytes and never consults TLC's normalized order. It never calls normalize() either, so it + * mutates nothing that other workers read. + * + *

Set elements and the keys of maps and pairs are the sort keys. Each is encoded once into its own + * array, sorted, and copied into the parent. Map and pair values stream straight into the output. + */ + private static final class Encoder { + + private final ByteArrayOutputStream out = new ByteArrayOutputStream(); + private final String operator; + + private Encoder(final String operator) { + this.operator = operator; + } + + static byte[] encode(final Value v, final String operator) { + final Encoder e = new Encoder(operator); + e.value(v); + return e.out.toByteArray(); + } + + private void value(final Value v) { + if (v instanceof IntValue) { + integer(((IntValue) v).val); + } else if (v instanceof BoolValue) { + out.write(((BoolValue) v).val ? 0xf5 : 0xf4); + } else if (v instanceof StringValue) { + text(((StringValue) v).val.toString()); + } else if (v instanceof ModelValue) { + head(TAG, TAG_MODEL_VALUE); + text(((ModelValue) v).val.toString()); + } else if (v instanceof TupleValue) { + array(((TupleValue) v).elems); + } else if (v instanceof RecordValue) { + // Not toFcnRcd(), which normalizes the record in place. + final RecordValue r = (RecordValue) v; + final Value[] names = new Value[r.names.length]; + for (int i = 0; i < names.length; i++) { + names[i] = new StringValue(r.names[i]); + } + function(names, r.values); + } else if (v instanceof FcnRcdValue) { + final FcnRcdValue f = (FcnRcdValue) v; + function(f.getDomainAsValues(), f.values); + } else if (v instanceof FcnLambdaValue) { + // The domain, not the function: TLC prints a function's body as its source location. + final Value domain = ((FcnLambdaValue) v).getDomain(); + if (!domain.isFinite()) { + throw cannotEncode("a function with the infinite domain", domain); + } + value(v.toFcnRcd()); + } else if (v instanceof EnumerableValue) { + if (!v.isFinite()) { + throw cannotEncode("an infinite set", v); + } + set(((SetEnumValue) v.toSetEnum()).elems.toArray()); + } else { + throw cannotEncode(v.getKindString(), v); + } + } + + private void function(final Value[] domain, final Value[] values) { + final Shape shape = shape(domain); + if (shape == Shape.SEQUENCE) { + final Value[] elems = new Value[domain.length]; + for (int i = 0; i < domain.length; i++) { + elems[((IntValue) domain[i]).val - 1] = values[i]; + } + array(elems); + return; + } + final byte[][] keys = encodeEach(domain); + final Integer[] order = new Integer[keys.length]; + for (int i = 0; i < order.length; i++) { + order[i] = i; + } + Arrays.sort(order, (i, j) -> Arrays.compareUnsigned(keys[i], keys[j])); + if (shape == Shape.RECORD) { + head(MAP, keys.length); + } else { + head(TAG, TAG_FUNCTION); + head(ARRAY, keys.length); + } + for (final int i : order) { + if (shape == Shape.PAIRS) { + head(ARRAY, 2); + } + write(keys[i]); + value(values[i]); + } + } + + private void array(final Value[] elems) { + head(ARRAY, elems.length); + for (final Value e : elems) { + value(e); + } + } + + /** + * An unnormalized set may hold an element twice, possibly in two Java classes. Equal elements have + * equal encodings, so dropping equal neighbours after sorting removes exactly TLC's duplicates. + */ + private void set(final Value[] elems) { + final byte[][] items = encodeEach(elems); + Arrays.sort(items, Arrays::compareUnsigned); + int n = 0; + for (final byte[] item : items) { + if (n == 0 || !Arrays.equals(item, items[n - 1])) { + items[n++] = item; + } + } + head(TAG, TAG_SET); + head(ARRAY, n); + for (int i = 0; i < n; i++) { + write(items[i]); + } + } + + private byte[][] encodeEach(final Value[] values) { + final byte[][] encoded = new byte[values.length][]; + for (int i = 0; i < values.length; i++) { + encoded[i] = encode(values[i], operator); + } + return encoded; + } + + private void integer(final int n) { + if (n >= 0) { + head(UNSIGNED, n); + } else { + head(NEGATIVE, -1 - n); + } + } + + /** + * Uses a CharsetEncoder, which reports errors, because String.getBytes turns an unpaired UTF-16 + * surrogate (SubSeq can cut one out of a string) into '?' without notice. + */ + private void text(final String s) { + final ByteBuffer utf8; + try { + utf8 = StandardCharsets.UTF_8.newEncoder().encode(CharBuffer.wrap(s)); + } catch (CharacterCodingException e) { + throw new EvalException(EC.GENERAL, + operator + " cannot encode a string that contains an unpaired UTF-16 surrogate."); + } + head(TEXT, utf8.remaining()); + out.write(utf8.array(), utf8.arrayOffset() + utf8.position(), utf8.remaining()); + } + + /** + * The initial byte and the shortest argument. Every argument fits in four bytes: integers are + * 32-bit, so -1 - n never exceeds Integer.MAX_VALUE, and lengths are Java array sizes. + */ + private void head(final int major, final int n) { + final int ib = major << 5; + if (n < 24) { + out.write(ib | n); + } else if (n <= 0xff) { + out.write(ib | 24); + out.write(n); + } else if (n <= 0xffff) { + out.write(ib | 25); + out.write(n >>> 8); + out.write(n); + } else { + out.write(ib | 26); + out.write(n >>> 24); + out.write(n >>> 16); + out.write(n >>> 8); + out.write(n); + } + } + + private void write(final byte[] bytes) { + out.write(bytes, 0, bytes.length); + } + + private EvalException cannotEncode(final String kind, final Value v) { + return new EvalException(EC.GENERAL, + operator + " cannot encode " + kind + ":\n" + Values.ppr(v.toString())); + } + } +} diff --git a/modules/tlc2/overrides/TLCOverrides.java b/modules/tlc2/overrides/TLCOverrides.java index 8938f53..1d1b637 100644 --- a/modules/tlc2/overrides/TLCOverrides.java +++ b/modules/tlc2/overrides/TLCOverrides.java @@ -46,7 +46,7 @@ public Class[] get() { return new Class[] { IOUtils.class, SVG.class, SequencesExt.class, Json.class, Bitwise.class, FiniteSetsExt.class, Functions.class, CSV.class, Combinatorics.class, BagsExt.class, DyadicRationals.class, Statistics.class, VectorClocks.class, GraphViz.class, Graphs.class, - UndirectedGraphs.class }; + UndirectedGraphs.class, CBOR.class }; } catch (NoClassDefFoundError e) { // Remove this catch when this Class is moved to `TLC`. System.out.println("gson dependencies of Json overrides not found, Json module won't work unless " @@ -54,6 +54,7 @@ public Class[] get() { } return new Class[] { IOUtils.class, SVG.class, SequencesExt.class, Bitwise.class, FiniteSetsExt.class, Functions.class, CSV.class, Combinatorics.class, BagsExt.class, DyadicRationals.class, - Statistics.class, VectorClocks.class, GraphViz.class, Graphs.class, UndirectedGraphs.class }; + Statistics.class, VectorClocks.class, GraphViz.class, Graphs.class, UndirectedGraphs.class, + CBOR.class }; } } diff --git a/tests/AllTests.tla b/tests/AllTests.tla index 8005e59..dc14bb2 100644 --- a/tests/AllTests.tla +++ b/tests/AllTests.tla @@ -8,6 +8,7 @@ EXTENDS RelationTests, SequencesExtTests, SVGTests, JsonTests, + CBORTests, BitwiseTests, IOUtilsTests, FiniteSetsExtTests, diff --git a/tests/CBORTests.tla b/tests/CBORTests.tla new file mode 100644 index 0000000..0a088c0 --- /dev/null +++ b/tests/CBORTests.tla @@ -0,0 +1,153 @@ +----------------------------- MODULE CBORTests ----------------------------- +EXTENDS CBOR, Integers, Sequences, FiniteSets, TLC, TLCExt + +(***************************************************************************) +(* TLC sorts strings and record fields by the order in which it first saw *) +(* them, not by their text. These strings and field names appear here in *) +(* the reverse of their CBOR order, before any other use, so TLC's own *) +(* order disagrees with the CBOR order. An encoder that relies on TLC's *) +(* order then fails the golden tests "set-strings" and "record". *) +(***************************************************************************) +LOCAL CBORInternFirst == + <<"cbor-zz", "cbor-aa", "cbor-a", [cborzz |-> 0, cboraa |-> 0, cbora |-> 0]>> + +ASSUME LET T == INSTANCE TLC IN T!PrintT("CBORTests") + +ASSUME AssertEq(ToString({"cbor-a", "cbor-zz"}), "{\"cbor-zz\", \"cbor-a\"}") +ASSUME AssertEq(ToString(DOMAIN [cbora |-> 0, cborzz |-> 0]), "{\"cborzz\", \"cbora\"}") + +(***************************************************************************) +(* A golden test is an ASSUME that calls Golden or SameBytes with a name *) +(* and the bytes that ToCBOR must return. tests/CBORTests/fixtures.py, an *) +(* encoder that shares no code with CBOR.java, checks those bytes against *) +(* its own encoding of the value it has under that name. *) +(* *) +(* All definitions are LOCAL because AllTests extends every test module. *) +(***************************************************************************) + +LOCAL INSTANCE IOUtils +LOCAL INSTANCE Json + +\* The model value that tests/AllTests.cfg defines, without redeclaring the +\* constant that JsonTests declares. +LOCAL MV == TLCModelValue("ModelValue") + +LOCAL Golden(name, value, bytes) == AssertEq(ToCBOR(value), bytes) + +\* TLC-equal values held in different Java classes encode as the same bytes. +LOCAL SameBytes(name, reps, bytes) == \A i \in DOMAIN reps : AssertEq(ToCBOR(reps[i]), bytes) + +\* The bytes of a file as a string, one character per byte. A missing file fails instead of reading as "". +LOCAL FileText(file) == + LET r == Deserialize(file, [format |-> "TXT", charset |-> "ISO-8859-1"]) + IN IF r.exitValue = 0 THEN r.stdout ELSE Assert(FALSE, r.stderr) + +----------------------------------------------------------------------------- + +ASSUME Golden("int", <<0, 23, 24, 255, 256, 65535, 65536, 2147483647, + -1, -24, -25, -256, -257, -2147483647 - 1>>, + <<\h8e, \h00, \h17, \h18, \h18, \h18, \hff, \h19, \h01, \h00, \h19, \hff, \hff, \h1a, \h00, \h01, + \h00, \h00, \h1a, \h7f, \hff, \hff, \hff, \h20, \h37, \h38, \h18, \h38, \hff, \h39, \h01, \h00, + \h3a, \h7f, \hff, \hff, \hff>>) +ASSUME Golden("bool", <>, <<\h82, \hf5, \hf4>>) +ASSUME Golden("modelvalue", MV, <<\hd8, \h27, \h6a, \h4d, \h6f, \h64, \h65, \h6c, \h56, \h61, \h6c, \h75, \h65>>) +\* Bytewise order is 10, 100, -1. Length-first order is 10, -1, 100. TLC's order is -1, 10, 100. +ASSUME Golden("set", {100, -1, 10}, <<\hd9, \h01, \h02, \h83, \h0a, \h18, \h64, \h20>>) +ASSUME Golden("set-strings", {"cbor-zz", "cbor-a", "cbor-aa"}, + <<\hd9, \h01, \h02, \h83, \h66, \h63, \h62, \h6f, \h72, \h2d, \h61, \h67, \h63, \h62, \h6f, \h72, + \h2d, \h61, \h61, \h67, \h63, \h62, \h6f, \h72, \h2d, \h7a, \h7a>>) +ASSUME Golden("set-nested", {{}, {1}, {1, 2}, {2}}, + <<\hd9, \h01, \h02, \h84, \hd9, \h01, \h02, \h80, \hd9, \h01, \h02, \h81, \h01, \hd9, \h01, \h02, + \h81, \h02, \hd9, \h01, \h02, \h82, \h01, \h02>>) +ASSUME Golden("emptyset", {}, <<\hd9, \h01, \h02, \h80>>) +ASSUME Golden("interval", {1, 2, 3}, <<\hd9, \h01, \h02, \h83, \h01, \h02, \h03>>) +ASSUME Golden("seq", <<"a", "b">>, <<\h82, \h61, \h61, \h61, \h62>>) +ASSUME Golden("empty", <<>>, <<\h80>>) +ASSUME Golden("record", [cborzz |-> 1, cbora |-> 2, cboraa |-> 3], + <<\ha3, \h65, \h63, \h62, \h6f, \h72, \h61, \h02, \h66, \h63, \h62, \h6f, \h72, \h61, \h61, \h03, + \h66, \h63, \h62, \h6f, \h72, \h7a, \h7a, \h01>>) +ASSUME Golden("fcn-int", 0 :> "x" @@ 1 :> "y", + <<\hd9, \h80, \he8, \h82, \h82, \h00, \h61, \h78, \h82, \h01, \h61, \h79>>) +ASSUME Golden("fcn-tuple", [t \in {<<1, 2>>, <<2, 1>>} |-> 3], + <<\hd9, \h80, \he8, \h82, \h82, \h82, \h01, \h02, \h03, \h82, \h82, \h02, \h01, \h03>>) +ASSUME Golden("fcn-set", [s \in SUBSET {1} |-> Cardinality(s)], + <<\hd9, \h80, \he8, \h82, \h82, \hd9, \h01, \h02, \h80, \h00, \h82, \hd9, \h01, \h02, \h81, \h01, + \h01>>) +ASSUME Golden("fcn-record", [r \in [a : {1, 2}] |-> r.a], + <<\hd9, \h80, \he8, \h82, \h82, \ha1, \h61, \h61, \h01, \h01, \h82, \ha1, \h61, \h61, \h02, \h02>>) +ASSUME Golden("fcn-modelvalue", [m \in {MV} |-> 0], + <<\hd9, \h80, \he8, \h81, \h82, \hd8, \h27, \h6a, \h4d, \h6f, \h64, \h65, \h6c, \h56, \h61, \h6c, + \h75, \h65, \h00>>) + +LOCAL DumpedTrace == + LET s1 == [x |-> 0, y |-> {}] + s2 == [x |-> 1, y |-> {MV}] + loc == [beginLine |-> 5, beginColumn |-> 9, endLine |-> 5, endColumn |-> 33, module |-> "T"] + IN [counterexample |-> [state |-> {<<1, s1>>, <<2, s2>>}, + action |-> {<< <<1, s1>>, [name |-> "Next", location |-> loc], <<2, s2>> >>}], + vars |-> {"x", "y"}] + +ASSUME Golden("trace", DumpedTrace, + <<\ha2, \h64, \h76, \h61, \h72, \h73, \hd9, \h01, \h02, \h82, \h61, \h78, \h61, \h79, \h6e, \h63, + \h6f, \h75, \h6e, \h74, \h65, \h72, \h65, \h78, \h61, \h6d, \h70, \h6c, \h65, \ha2, \h65, \h73, + \h74, \h61, \h74, \h65, \hd9, \h01, \h02, \h82, \h82, \h01, \ha2, \h61, \h78, \h00, \h61, \h79, + \hd9, \h01, \h02, \h80, \h82, \h02, \ha2, \h61, \h78, \h01, \h61, \h79, \hd9, \h01, \h02, \h81, + \hd8, \h27, \h6a, \h4d, \h6f, \h64, \h65, \h6c, \h56, \h61, \h6c, \h75, \h65, \h66, \h61, \h63, + \h74, \h69, \h6f, \h6e, \hd9, \h01, \h02, \h81, \h83, \h82, \h01, \ha2, \h61, \h78, \h00, \h61, + \h79, \hd9, \h01, \h02, \h80, \ha2, \h64, \h6e, \h61, \h6d, \h65, \h64, \h4e, \h65, \h78, \h74, + \h68, \h6c, \h6f, \h63, \h61, \h74, \h69, \h6f, \h6e, \ha5, \h66, \h6d, \h6f, \h64, \h75, \h6c, + \h65, \h61, \h54, \h67, \h65, \h6e, \h64, \h4c, \h69, \h6e, \h65, \h05, \h69, \h62, \h65, \h67, + \h69, \h6e, \h4c, \h69, \h6e, \h65, \h05, \h69, \h65, \h6e, \h64, \h43, \h6f, \h6c, \h75, \h6d, + \h6e, \h18, \h21, \h6b, \h62, \h65, \h67, \h69, \h6e, \h43, \h6f, \h6c, \h75, \h6d, \h6e, \h09, + \h82, \h02, \ha2, \h61, \h78, \h01, \h61, \h79, \hd9, \h01, \h02, \h81, \hd8, \h27, \h6a, \h4d, + \h6f, \h64, \h65, \h6c, \h56, \h61, \h6c, \h75, \h65>>) + +----------------------------------------------------------------------------- + +ASSUME SameBytes("seq", << <<"a", "b">>, + [i \in 1..2 |-> IF i = 1 THEN "a" ELSE "b"], + 2 :> "b" @@ 1 :> "a", + Tail(<<"z", "a", "b">>) >>, + <<\h82, \h61, \h61, \h61, \h62>>) + +\* JsonDeserialize reads {} as a record without fields. +ASSUME SameBytes("empty", << <<>>, + [x \in {} |-> x], + JsonDeserialize("tests/CBORTests/empty-object.json") >>, + <<\h80>>) + +ASSUME SameBytes("record", << [cbora |-> 2, cboraa |-> 3, cborzz |-> 1], + "cbora" :> 2 @@ "cborzz" :> 1 @@ "cboraa" :> 3, + [f \in {"cborzz", "cbora", "cboraa"} |-> + CASE f = "cbora" -> 2 [] f = "cboraa" -> 3 [] OTHER -> 1] >>, + <<\ha3, \h65, \h63, \h62, \h6f, \h72, \h61, \h02, \h66, \h63, \h62, \h6f, \h72, \h61, \h61, \h03, + \h66, \h63, \h62, \h6f, \h72, \h7a, \h7a, \h01>>) + +ASSUME SameBytes("interval", << {3, 1, 2}, + 1..3, + {x \in -5..5 : x > 0 /\ x < 4}, + {1, 1, 2, 3, 2} >>, + <<\hd9, \h01, \h02, \h83, \h01, \h02, \h03>>) + +ASSUME SameBytes("set", << {10, 100, 10, -1}, {x \in -1..100 : x \in {-1, 10, 100}} >>, + <<\hd9, \h01, \h02, \h83, \h0a, \h18, \h64, \h20>>) +ASSUME SameBytes("set-nested", << SUBSET {1, 2}, {{1}, {2}} \cup {{}, {1, 2}} >>, + <<\hd9, \h01, \h02, \h84, \hd9, \h01, \h02, \h80, \hd9, \h01, \h02, \h81, \h01, \hd9, \h01, \h02, + \h81, \h02, \hd9, \h01, \h02, \h82, \h01, \h02>>) +ASSUME SameBytes("emptyset", << 1..0, {x \in {1} : FALSE}, {1} \ {1} >>, + <<\hd9, \h01, \h02, \h80>>) +ASSUME SameBytes("fcn-int", << [x \in 0..1 |-> IF x = 0 THEN "x" ELSE "y"], 1 :> "y" @@ 0 :> "x" >>, + <<\hd9, \h80, \he8, \h82, \h82, \h00, \h61, \h78, \h82, \h01, \h61, \h79>>) +ASSUME SameBytes("fcn-tuple", << (<<2, 1>> :> 3) @@ (<<1, 2>> :> 3), + [t \in ({1, 2} \X {1, 2}) \ {<<1, 1>>, <<2, 2>>} |-> 3] >>, + <<\hd9, \h80, \he8, \h82, \h82, \h82, \h01, \h02, \h03, \h82, \h82, \h02, \h01, \h03>>) + +----------------------------------------------------------------------------- + +\* CBORSerialize writes the bytes of ToCBOR and creates missing parent directories. The bytes +\* of "CBOR" read as text: 0x64, the head of a text string of four bytes, is the letter d. +ASSUME /\ CBORSerialize("build/cbor/a/b/c/text.cbor", "CBOR") + /\ AssertEq(ToCBOR("CBOR"), <<\h64, \h43, \h42, \h4f, \h52>>) + /\ AssertEq(FileText("build/cbor/a/b/c/text.cbor"), "dCBOR") + +============================================================================= diff --git a/tests/CBORTests/empty-object.json b/tests/CBORTests/empty-object.json new file mode 100644 index 0000000..0967ef4 --- /dev/null +++ b/tests/CBORTests/empty-object.json @@ -0,0 +1 @@ +{} diff --git a/tests/CBORTests/fixtures.py b/tests/CBORTests/fixtures.py new file mode 100644 index 0000000..782bef5 --- /dev/null +++ b/tests/CBORTests/fixtures.py @@ -0,0 +1,181 @@ +"""Checks the golden bytes in tests/CBORTests.tla against a second CBOR encoder. + + python3 tests/CBORTests/fixtures.py + +Run it by hand after changing the encoding or a golden row; CI does not run it. It needs only the +standard library. If the third-party decoder cbor2 (pip install cbor2) is importable, it also prints +how cbor2 reads every golden, so a reviewer can check their meaning independently of TLC. + +The encoder below is a second implementation of the encoding table in modules/CBOR.tla that shares +no code with CBOR.java. CBORTests.tla states each golden as an ASSUME that calls Golden or SameBytes +with the golden's name and its bytes as a TLA+ sequence of hex literals (<<\\h82, \\h61, ...>>). +TLC checks that ToCBOR writes those bytes; this script checks that they are the bytes this encoder +writes for the value of the same name. It exits non-zero on a mismatch, printing the expected +sequence, on a name it does not know, and on a value it has that no ASSUME states. +""" +import os +import re +import struct +import sys + +TAG_MODEL_VALUE = 39 +TAG_SET = 258 +TAG_FUNCTION = 33000 + + +class MV: + def __init__(self, name): self.name = name + + +class Set: + def __init__(self, *elems): self.elems = elems + + +class Fn: + """A function given by its (x, f[x]) pairs.""" + def __init__(self, *pairs): self.pairs = pairs + + +def head(major, n): + if n < 24: + return bytes([major << 5 | n]) + for ai, fmt, limit in ((24, ">B", 0xFF), (25, ">H", 0xFFFF), (26, ">I", 0xFFFFFFFF), (27, ">Q", 2**64 - 1)): + if n <= limit: + return bytes([major << 5 | ai]) + struct.pack(fmt, n) + raise ValueError(n) + + +def keyed(pairs, as_map): + entries = sorted((enc(k), v) for k, v in pairs) + assert all(a[0] != b[0] for a, b in zip(entries, entries[1:])), "duplicate key" + out = head(5, len(entries)) if as_map else head(6, TAG_FUNCTION) + head(4, len(entries)) + for k, v in entries: + out += k + enc(v) if as_map else head(4, 2) + k + enc(v) + return out + + +def function(pairs): + keys = [k for k, _ in pairs] + if sorted(k for k in keys if type(k) is int) == list(range(1, len(keys) + 1)): + return enc(tuple(v for _, v in sorted(pairs, key=lambda p: p[0]))) + return keyed(pairs, as_map=all(type(k) is str for k in keys)) + + +def enc(v): + if type(v) is bool: + return b"\xf5" if v else b"\xf4" + if type(v) is int: + assert -(2**31) <= v < 2**31, "TLC integers are 32-bit" + return head(0, v) if v >= 0 else head(1, -1 - v) + if type(v) is str: + b = v.encode("utf-8") + return head(3, len(b)) + b + if isinstance(v, MV): + return head(6, TAG_MODEL_VALUE) + enc(v.name) + if isinstance(v, Set): + items = sorted(set(enc(e) for e in v.elems)) + return head(6, TAG_SET) + head(4, len(items)) + b"".join(items) + if isinstance(v, tuple): + return head(4, len(v)) + b"".join(enc(e) for e in v) + if isinstance(v, dict): + return function(list(v.items())) + if isinstance(v, Fn): + return function(list(v.pairs)) + raise TypeError(type(v)) + + +MODEL_VALUE = MV("ModelValue") # tests/AllTests.cfg: CONSTANT ModelValueConstant = ModelValue + +S1 = {"x": 0, "y": Set()} +S2 = {"x": 1, "y": Set(MODEL_VALUE)} +LOCATION = {"beginLine": 5, "beginColumn": 9, "endLine": 5, "endColumn": 33, "module": "T"} + +# name -> value. CBORTests.tla states each value again in TLA+, next to its bytes. +GOLDEN = { + "int": (0, 23, 24, 255, 256, 65535, 65536, 2147483647, -1, -24, -25, -256, -257, -2147483648), + "bool": (True, False), + "modelvalue": MODEL_VALUE, + "set": Set(100, -1, 10), + "set-strings": Set("cbor-zz", "cbor-a", "cbor-aa"), + "set-nested": Set(Set(), Set(1), Set(1, 2), Set(2)), + "emptyset": Set(), + "interval": Set(1, 2, 3), + "seq": ("a", "b"), + "empty": (), + "record": {"cborzz": 1, "cbora": 2, "cboraa": 3}, + "fcn-int": Fn((0, "x"), (1, "y")), + "fcn-tuple": Fn(((1, 2), 3), ((2, 1), 3)), + "fcn-set": Fn((Set(), 0), (Set(1), 1)), + "fcn-record": Fn(({"a": 1}, 1), ({"a": 2}, 2)), + "fcn-modelvalue": Fn((MODEL_VALUE, 0)), + "trace": {"counterexample": {"state": Set((1, S1), (2, S2)), + "action": Set(((1, S1), {"name": "Next", "location": LOCATION}, (2, S2)))}, + "vars": Set("x", "y")}, +} + +NAME = re.compile(r'\b(?:Golden|SameBytes)\("([^"]+)"') +HEX_SEQUENCE = re.compile(r'<<\s*(\\h[0-9a-fA-F]{2}(?:\s*,\s*\\h[0-9a-fA-F]{2})*)\s*>>') + + +def tla(data): + """data as a TLA+ sequence of hex literals, 16 to a line.""" + lines = [", ".join(f"\\h{b:02x}" for b in data[i:i + 16]) for i in range(0, len(data), 16)] + return "<<" + ",\n ".join(lines) + ">>" + + +def statements(text): + """Yields each top-level unit of the module, which starts at column 0, with its first line number.""" + line = 1 + for chunk in re.split(r"\n(?=\S)", text): + yield line, chunk + line += chunk.count("\n") + 1 + + +def check(path): + failures = [] + seen = set() + for line, stmt in statements(open(path, encoding="ascii").read()): + names = NAME.findall(stmt) + if not names: + continue + literals = HEX_SEQUENCE.findall(stmt) + if len(set(names)) != 1 or len(literals) != 1: + failures.append(f"line {line}: expected one golden name and one hex sequence, found {names} and " + f"{len(literals)} sequences") + continue + name = names[0] + if name not in GOLDEN: + failures.append(f"line {line}: no value for the golden {name!r}") + continue + seen.add(name) + stated = bytes(int(h[2:], 16) for h in re.findall(r"\\h[0-9a-fA-F]{2}", literals[0])) + expected = enc(GOLDEN[name]) + if stated == expected: + print(f"ok {name} (line {line})") + else: + failures.append(f"line {line}: the bytes of {name!r} differ; this encoder writes\n{tla(expected)}") + failures += [f"no ASSUME states the golden {name!r}" for name in GOLDEN if name not in seen] + for f in failures: + print("FAIL " + f) + return not failures + + +def show_cbor2(): + try: + import cbor2 + except ImportError: + return + print("\ncbor2 reads the goldens as:") + for name, value in GOLDEN.items(): + try: + text = repr(cbor2.loads(enc(value))) + except cbor2.CBORDecodeError as e: + text = f"error: {e}" + print(f" {name}: {text if len(text) <= 200 else text[:200] + '...'}") + + +if __name__ == "__main__": + here = os.path.dirname(os.path.abspath(__file__)) + ok = check(sys.argv[1] if len(sys.argv) > 1 else os.path.join(here, os.pardir, "CBORTests.tla")) + show_cbor2() + sys.exit(0 if ok else 1) From cc5d8402be6299b89d200e69989f307ab36952b0 Mon Sep 17 00:00:00 2001 From: younes-io Date: Tue, 6 Oct 2026 18:32:47 +0200 Subject: [PATCH 2/9] Read CBOR bytes and files back as TLA+ values FromCBOR decodes one CBOR data item from a sequence of integers in 0..255, and CBORDeserialize from a file, so a spec can load a trace or state that a harness wrote. Both use one decoder. It decides the TLC class of a map or a pair list with the same shape rule the encoder uses to pick the form, and builds values already normalized in TLC's order. The decoder is lenient on form and strict on meaning. It accepts set elements, keys and pairs in any order, integers and lengths in any width, and maps with keys that are not strings, because Python, Go and Rust encoders differ on exactly these by default. It rejects duplicates under TLC equality, values TLC cannot represent or compare, and nesting deeper than 512 data items, and names the operator, the file if there is one, and the byte offset. It looks model values up among the model's and never creates one, because TLC reads model values back from its disk queues by index. The tests read every golden back, read inline inputs that TLC never writes and require them to encode again in canonical form, round-trip exhaustive small value spaces, and check that a file CBORSerialize wrote reads back as FromCBOR(ToCBOR(v)). https://github.com/tlaplus/tlaplus/issues/1467 [Feature] Signed-off-by: younes-io --- modules/tlc2/overrides/CBOR.java | 356 ++++++++++++++++++++++++++++++- tests/CBORTests.tla | 99 ++++++++- tests/CBORTests/fixtures.py | 1 + 3 files changed, 451 insertions(+), 5 deletions(-) diff --git a/modules/tlc2/overrides/CBOR.java b/modules/tlc2/overrides/CBOR.java index 19cd1ff..1367f5a 100644 --- a/modules/tlc2/overrides/CBOR.java +++ b/modules/tlc2/overrides/CBOR.java @@ -27,15 +27,19 @@ import java.io.ByteArrayOutputStream; import java.io.IOException; +import java.math.BigInteger; import java.nio.ByteBuffer; import java.nio.CharBuffer; import java.nio.charset.CharacterCodingException; import java.nio.charset.StandardCharsets; import java.nio.file.Files; import java.nio.file.InvalidPathException; +import java.nio.file.NoSuchFileException; import java.nio.file.Path; import java.nio.file.Paths; import java.util.Arrays; +import java.util.HashMap; +import java.util.Map; import tlc2.output.EC; import tlc2.tool.EvalException; @@ -51,14 +55,17 @@ import tlc2.value.impl.StringValue; import tlc2.value.impl.TupleValue; import tlc2.value.impl.Value; +import util.Assert.TLCRuntimeException; +import util.UniqueString; /** * Module overrides for CBOR.tla: encode a finite TLA+ value as CBOR (RFC 8949), as a sequence of bytes or * in a file, and decode it back. CBOR.tla documents the encoding; this class is its only implementation. * - *

There is no intermediate data model. {@link Encoder} walks TLC values and writes bytes, and the - * operators are thin shells around it. Both directions decide how a function is written by one rule, - * {@link #shape(Value[])}. The class depends only on TLC and the JDK. + *

There is no intermediate data model. {@link Encoder} walks TLC values and writes bytes, and + * {@link Decoder} reads bytes and builds TLC values. The four operators are thin shells around them. Both + * decide how a function is written by one rule, {@link #shape(Value[])}, so the form the encoder writes and + * the class the decoder builds cannot drift apart. The class depends only on TLC and the JDK. * *

Every error is an {@link EvalException}, never a Java exception that TLC would wrap as error 2154. * A wrong argument type uses the CommunityModules argument codes; errors about a value or a file use @@ -70,7 +77,7 @@ private CBOR() { } // Major types, RFC 8949 section 3.1. - private static final int UNSIGNED = 0, NEGATIVE = 1, TEXT = 3, ARRAY = 4, MAP = 5, TAG = 6; + private static final int UNSIGNED = 0, NEGATIVE = 1, BYTES = 2, TEXT = 3, ARRAY = 4, MAP = 5, TAG = 6, SIMPLE = 7; /** IANA tag 39, "Identifier", around a model value's name. */ private static final int TAG_MODEL_VALUE = 39; @@ -126,6 +133,30 @@ public static TupleValue toCBOR(final Value value) { return new TupleValue(elems); } + /** Accepts any value that TLC converts to a sequence, such as [i \in 1..n |-> ...]. */ + @TLAPlusOperator(identifier = "FromCBOR", module = "CBOR", warn = false) + public static Value fromCBOR(final Value bytes) { + final Value seq = bytes.toTuple(); + if (seq == null) { + throw notBytes(bytes); + } + final Value[] elems = ((TupleValue) seq).elems; + final byte[] in = new byte[elems.length]; + for (int i = 0; i < in.length; i++) { + final int b = elems[i] instanceof IntValue ? ((IntValue) elems[i]).val : -1; + if (b < 0 || b > 255) { + throw notBytes(bytes); + } + in[i] = (byte) b; + } + return new Decoder(in, "FromCBOR").document(); + } + + private static EvalException notBytes(final Value v) { + return new EvalException(EC.TLC_MODULE_ONE_ARGUMENT_ERROR, + new String[] { "FromCBOR", "sequence of integers in 0..255", Values.ppr(v.toString()) }); + } + /** * Encodes the whole value before it touches the file, so a value it refuses leaves an existing file * as it was. @@ -153,6 +184,31 @@ public static BoolValue serialize(final Value absoluteFilename, final Value valu return BoolValue.ValTrue; } + /** + * With the default minLevel, a zero-arity definition such as Log == CBORDeserialize("log.cbor") is + * constant-level, so TLC reads the file once, before it starts checking. + */ + @TLAPlusOperator(identifier = "CBORDeserialize", module = "CBOR", warn = false) + public static Value deserialize(final Value absoluteFilename) { + if (!(absoluteFilename instanceof StringValue)) { + throw new EvalException(EC.TLC_MODULE_ONE_ARGUMENT_ERROR, + new String[] { "CBORDeserialize", "string", Values.ppr(absoluteFilename.toString()) }); + } + final String file = ((StringValue) absoluteFilename).val.toString(); + final byte[] bytes; + synchronized (FILES) { + try { + bytes = Files.readAllBytes(Paths.get(file)); + } catch (NoSuchFileException e) { + throw new EvalException(EC.GENERAL, + "CBORDeserialize could not read " + file + ": the file does not exist."); + } catch (IOException | InvalidPathException e) { + throw new EvalException(EC.GENERAL, "CBORDeserialize could not read " + file + ": " + e + "."); + } + } + return new Decoder(bytes, "CBORDeserialize could not read " + file).document(); + } + /** * Writes the one encoding of a TLC value. Values that TLC considers equal produce identical bytes, * whatever their Java class and whatever order TLC interned their strings in, so the encoder sorts by @@ -340,4 +396,296 @@ private EvalException cannotEncode(final String kind, final Value v) { operator + " cannot encode " + kind + ":\n" + Values.ppr(v.toString())); } } + + /** + * Reads one CBOR data item into a TLC value. Liberal about form, strict about meaning: it accepts set + * elements, map keys and pairs in any order, integers and lengths in any width, and maps with keys that + * are not strings. Encoders in other languages differ on exactly these by default, and none of them + * changes the TLA+ value. It rejects every item whose TLA+ meaning is missing, out of TLC's range, or + * ambiguous, and names the source and the byte offset of the item. + * + *

It never creates a model value. ModelValue.make at run time leaves ModelValue.mvs stale, and TLC + * reads model values back from its disk queues by index into mvs. + */ + private static final class Decoder { + + /** Bounds the recursion, so hostile input is an error instead of a stack overflow. */ + private static final int MAX_DEPTH = 512; + + private final byte[] in; + private final String prefix; + private int pos; + private Map modelValues; + + Decoder(final byte[] in, final String prefix) { + this.in = in; + this.prefix = prefix; + } + + Value document() { + final Value v = item(1); + if (pos != in.length) { + throw error(pos, "there are bytes after the first CBOR data item"); + } + return v; + } + + private Value item(final int depth) { + final int start = pos; + final int ib = initial(depth); + final int major = ib >>> 5; + if (major == SIMPLE) { + return simple(start, ib & 0x1f); + } + final long arg = argument(start, major, ib & 0x1f); + switch (major) { + case UNSIGNED: + case NEGATIVE: + return integer(start, arg, major == NEGATIVE); + case BYTES: + throw error(start, "a byte string has no TLA+ counterpart"); + case TEXT: + return new StringValue(text(start, arg)); + case ARRAY: + return new TupleValue(items(count(start, arg, 1), depth + 1)); + case MAP: + final int n = count(start, arg, 2); + final Value[] keys = new Value[n], values = new Value[n]; + for (int i = 0; i < n; i++) { + keys[i] = item(depth + 1); + values[i] = item(depth + 1); + } + return function(start, keys, values); + default: + return tagged(start, arg, depth); + } + } + + private Value simple(final int start, final int ai) { + switch (ai) { + case 20: + return BoolValue.ValFalse; + case 21: + return BoolValue.ValTrue; + case 22: + throw error(start, "null has no TLA+ counterpart"); + case 23: + throw error(start, "undefined has no TLA+ counterpart"); + case 25: + case 26: + case 27: + throw error(start, "a floating-point number has no TLA+ counterpart"); + case 28: + case 29: + case 30: + case 31: + throw notWellFormed(start); + default: + throw error(start, "a simple value has no TLA+ counterpart"); + } + } + + private Value tagged(final int start, final long tag, final int depth) { + if (tag == TAG_MODEL_VALUE) { + final int at = pos; + final int ib = initial(depth + 1); + if (ib >>> 5 != TEXT) { + throw error(start, "tag 39 must enclose a text string"); + } + return modelValue(start, text(at, argument(at, TEXT, ib & 0x1f))); + } + if (tag == TAG_SET) { + return set(start, items(arrayHead(start, depth + 1, "tag 258 must enclose an array"), depth + 2)); + } + if (tag == TAG_FUNCTION) { + final String complaint = "tag " + TAG_FUNCTION + " must enclose an array of [key, value] arrays"; + final int n = arrayHead(start, depth + 1, complaint); + final Value[] keys = new Value[n], values = new Value[n]; + for (int i = 0; i < n; i++) { + if (arrayHead(start, depth + 2, complaint) != 2) { + throw error(start, complaint); + } + keys[i] = item(depth + 3); + values[i] = item(depth + 3); + } + return function(start, keys, values); + } + throw error(start, "tag " + Long.toUnsignedString(tag) + " has no TLA+ counterpart"); + } + + /** The length of the array that must follow the tag at start. */ + private int arrayHead(final int start, final int depth, final String complaint) { + final int at = pos; + final int ib = initial(depth); + if (ib >>> 5 != ARRAY) { + throw error(start, complaint); + } + return count(at, argument(at, ARRAY, ib & 0x1f), 1); + } + + private Value function(final int start, final Value[] keys, final Value[] values) { + final Integer[] order = distinct(start, keys, "key"); + final int n = keys.length; + switch (shape(keys)) { + case SEQUENCE: + final Value[] elems = new Value[n]; + for (int i = 0; i < n; i++) { + elems[((IntValue) keys[i]).val - 1] = values[i]; + } + return new TupleValue(elems); + case RECORD: + final UniqueString[] names = new UniqueString[n]; + final Value[] fields = new Value[n]; + for (int i = 0; i < n; i++) { + names[i] = ((StringValue) keys[order[i]]).val; + fields[i] = values[order[i]]; + } + return new RecordValue(names, fields, true); + default: + final Value[] domain = new Value[n], range = new Value[n]; + for (int i = 0; i < n; i++) { + domain[i] = keys[order[i]]; + range[i] = values[order[i]]; + } + return new FcnRcdValue(domain, range, true); + } + } + + private Value set(final int start, final Value[] elems) { + final Integer[] order = distinct(start, elems, "element"); + final Value[] sorted = new Value[elems.length]; + for (int i = 0; i < sorted.length; i++) { + sorted[i] = elems[order[i]]; + } + return new SetEnumValue(sorted, true); + } + + /** + * Sorts indices into TLC's order, which lets the caller build normalized values. Equality is TLC's, + * not bytewise: 01 and 18 01 are the same element. TLC's compareTo fails on values it cannot + * compare (1 and "a"); reporting that here is clearer than a failure at first use in the spec. + */ + private Integer[] distinct(final int start, final Value[] items, final String what) { + final Integer[] order = new Integer[items.length]; + for (int i = 0; i < order.length; i++) { + order[i] = i; + } + Arrays.sort(order, (i, j) -> { + try { + return items[i].compareTo(items[j]); + } catch (TLCRuntimeException e) { + throw error(start, "TLC cannot compare the " + what + "s " + ppr(items[Math.min(i, j)]) + " and " + + ppr(items[Math.max(i, j)])); + } + }); + for (int k = 1; k < order.length; k++) { + if (items[order[k - 1]].compareTo(items[order[k]]) == 0) { + throw error(start, "the " + what + " " + ppr(items[order[k]]) + " occurs twice"); + } + } + return order; + } + + /** arg is an unsigned 64-bit number. */ + private Value integer(final int start, final long arg, final boolean negative) { + if (arg < 0 || arg > Integer.MAX_VALUE) { + final BigInteger n = new BigInteger(Long.toUnsignedString(arg)); + throw error(start, "the integer " + (negative ? n.not() : n) + + " is outside TLC's range -2147483648..2147483647"); + } + return IntValue.gen(negative ? (int) ~arg : (int) arg); + } + + /** A strict decoder: malformed UTF-8 is an error, never U+FFFD. */ + private String text(final int start, final long length) { + final int n = count(start, length, 1); + final String s; + try { + s = StandardCharsets.UTF_8.newDecoder().decode(ByteBuffer.wrap(in, pos, n)).toString(); + } catch (CharacterCodingException e) { + throw error(start, "a text string is not valid UTF-8"); + } + pos += n; + return s; + } + + private ModelValue modelValue(final int start, final String name) { + if (modelValues == null) { + modelValues = new HashMap<>(); + for (final ModelValue mv : ModelValue.mvs) { + modelValues.put(mv.val.toString(), mv); + } + } + final ModelValue mv = modelValues.get(name); + if (mv == null) { + throw new EvalException(EC.GENERAL, + message(start, "the model value " + name + " is not defined in the model") + + " Declare it in the .cfg or create it with TLCExt!TLCModelValue(\"" + name + "\")."); + } + return mv; + } + + private Value[] items(final int n, final int depth) { + final Value[] items = new Value[n]; + for (int i = 0; i < n; i++) { + items[i] = item(depth); + } + return items; + } + + private int initial(final int depth) { + if (pos == in.length) { + throw error(pos, "the input ends inside a CBOR data item"); + } + if (depth > MAX_DEPTH) { + throw error(pos, "data items are nested more than " + MAX_DEPTH + " deep"); + } + return in[pos++] & 0xff; + } + + private long argument(final int start, final int major, final int ai) { + if (ai < 24) { + return ai; + } + if (ai == 31 && BYTES <= major && major <= MAP) { + throw error(start, "indefinite-length items are not supported"); + } + if (ai > 27) { + throw notWellFormed(start); + } + final int size = 1 << (ai - 24); + if (in.length - pos < size) { + throw error(start, "the input ends inside a CBOR data item"); + } + long arg = 0; + for (int i = 0; i < size; i++) { + arg = arg << 8 | in[pos++] & 0xff; + } + return arg; + } + + /** Checked before anything is allocated, so a corrupt length cannot exhaust memory. */ + private int count(final int start, final long n, final int minBytesPerItem) { + if (n < 0 || n > (in.length - pos) / minBytesPerItem) { + throw error(start, "the input ends inside a CBOR data item"); + } + return (int) n; + } + + private EvalException notWellFormed(final int start) { + return error(start, String.format("the initial byte 0x%02x is not well-formed", in[start] & 0xff)); + } + + private EvalException error(final int offset, final String problem) { + return new EvalException(EC.GENERAL, message(offset, problem)); + } + + private String message(final int offset, final String problem) { + return prefix + ": " + problem + " at byte " + offset + "."; + } + + private static String ppr(final Value v) { + return Values.ppr(v.toString()); + } + } } diff --git a/tests/CBORTests.tla b/tests/CBORTests.tla index 0a088c0..9fd0964 100644 --- a/tests/CBORTests.tla +++ b/tests/CBORTests.tla @@ -32,7 +32,9 @@ LOCAL INSTANCE Json \* constant that JsonTests declares. LOCAL MV == TLCModelValue("ModelValue") -LOCAL Golden(name, value, bytes) == AssertEq(ToCBOR(value), bytes) +LOCAL Golden(name, value, bytes) == + /\ AssertEq(ToCBOR(value), bytes) + /\ AssertEq(FromCBOR(bytes), value) \* TLC-equal values held in different Java classes encode as the same bytes. LOCAL SameBytes(name, reps, bytes) == \A i \in DOMAIN reps : AssertEq(ToCBOR(reps[i]), bytes) @@ -102,6 +104,19 @@ ASSUME Golden("trace", DumpedTrace, \h82, \h02, \ha2, \h61, \h78, \h01, \h61, \h79, \hd9, \h01, \h02, \h81, \hd8, \h27, \h6a, \h4d, \h6f, \h64, \h65, \h6c, \h56, \h61, \h6c, \h75, \h65>>) +\* Non-ASCII strings enter as bytes, so this file stays ASCII. The fifth string is U+1F600, +\* which TLC holds as two UTF-16 code units. +ASSUME LET bytes == <<\h85, \h60, \h61, \h61, \h62, \hc3, \hbc, \h66, \he6, \h97, \ha5, \he6, \h9c, \hac, \h64, \hf0, + \h9f, \h98, \h80>> + s == FromCBOR(bytes) + IN /\ Golden("string", s, bytes) + /\ AssertEq(<>, <<"", "a">>) + /\ AssertEq(<>, <<1, 2, 2>>) + +\* The deepest nesting FromCBOR reads: 512 sequences, one inside the other. +ASSUME LET bytes == [i \in 1..512 |-> IF i < 512 THEN \h81 ELSE \h80] + IN AssertEq(ToCBOR(FromCBOR(bytes)), bytes) + ----------------------------------------------------------------------------- ASSUME SameBytes("seq", << <<"a", "b">>, @@ -144,10 +159,92 @@ ASSUME SameBytes("fcn-tuple", << (<<2, 1>> :> 3) @@ (<<1, 2>> :> 3), ----------------------------------------------------------------------------- +LOCAL RoundTrips(v) == AssertEq(FromCBOR(ToCBOR(v)), v) + +\* Re-encoding a decoded value gives the bytes it was decoded from. +LOCAL Stable(v) == AssertEq(ToCBOR(FromCBOR(ToCBOR(v))), ToCBOR(v)) + +LOCAL CBORSamples == << + -2147483647 - 1, 2147483647, "", + {MV, 1}, + <<<<>>, {}>>, + [x \in {<<>>} |-> 1], + [p \in {1, 2} \X {"a", "b"} |-> p[1]], + [f \in [{1, 2} -> {TRUE, FALSE}] |-> f[1] /\ f[2]], + {[a |-> 1, b |-> {<<1, "x">>}], [a |-> 2, b |-> {}]}, + <<[c |-> <<>>], {{{}}}, 3 :> [d |-> MV]>>, + {TLCModelValue("C_cbor1"), TLCModelValue("C_cbor2")} +>> + +ASSUME \A i \in DOMAIN CBORSamples : RoundTrips(CBORSamples[i]) /\ Stable(CBORSamples[i]) + +ASSUME \A S \in SUBSET {-2147483647 - 1, -25, -1, 0, 23, 24, 2147483647} : RoundTrips(S) +ASSUME \A s \in UNION {[1..n -> {"", "a", "cbor-zz"}] : n \in 0..2} : RoundTrips(s) +ASSUME \A r \in [{"a", "b"} -> BOOLEAN] : RoundTrips(r) +ASSUME \A f \in [{0, 2} -> {"x", "y"}] : RoundTrips(f) +ASSUME \A f \in [SUBSET {1, 2} -> {0, 1}] : RoundTrips(f) /\ Stable(f) +ASSUME \A f \in [{<<1, 2>>, <<2, 1>>} -> BOOLEAN] : RoundTrips(f) /\ Stable(f) +ASSUME \A f \in [{[a |-> 1], [a |-> 2]} -> {1, 2}] : RoundTrips(f) +ASSUME \A f \in [{MV, 1} -> {MV, "s"}] : RoundTrips(f) /\ Stable(f) +ASSUME RoundTrips(SUBSET SUBSET {1, 2}) /\ Stable(SUBSET SUBSET {1, 2}) +ASSUME RoundTrips(DumpedTrace) /\ Stable(DumpedTrace) + +\* Decoded values are marked normalized, so their order must be TLC's: TLC finds an +\* element of a normalized set, and an argument of a normalized function with at +\* least 32 entries, by bisection. +ASSUME LET s == FromCBOR(<<\hd9, \h01, \h02, \h83, \h0a, \h20, \h18, \h64>>) + IN /\ \A x \in {-1, 10, 100} : x \in s + /\ 0 \notin s +ASSUME LET f == FromCBOR(ToCBOR([x \in 0..40 |-> -x])) IN \A x \in 0..40 : f[x] = -x +ASSUME LET t == FromCBOR(ToCBOR(DumpedTrace)) + IN /\ Cardinality(t.counterexample.state) = 2 + /\ \E p \in t.counterexample.state : p[1] = 2 /\ MV \in p[2].y + /\ t.vars = {"x", "y"} +ASSUME LET f == FromCBOR(ToCBOR([t \in {<<1, 2>>, <<2, 1>>} |-> 3])) + IN DOMAIN f = {<<1, 2>>, <<2, 1>>} /\ f[<<2, 1>>] = 3 + +----------------------------------------------------------------------------- + +\* FromCBOR reads bytes that TLC never writes, and ToCBOR writes the value it read in the one +\* canonical form. +LOCAL Accepts(bytes, value) == + /\ AssertEq(FromCBOR(bytes), value) + /\ AssertEq(ToCBOR(FromCBOR(bytes)), ToCBOR(value)) + +\* Set elements, map keys, and pairs in any order, including the length-first order of +\* cbor2's canonical=True. +ASSUME Accepts(<<\hd9, \h01, \h02, \h82, \h02, \h01>>, {1, 2}) +ASSUME Accepts(<<\hd9, \h01, \h02, \h83, \h0a, \h20, \h18, \h64>>, {100, -1, 10}) +ASSUME Accepts(<<\ha2, \h61, \h62, \h01, \h61, \h61, \h02>>, [a |-> 2, b |-> 1]) +ASSUME Accepts(<<\hd9, \h80, \he8, \h82, \h82, \h02, \h01, \h82, \h01, \h00>>, <<0, 1>>) +\* Integers and lengths in a wider form than needed. +ASSUME Accepts(<<\h1b, \h00, \h00, \h00, \h00, \h00, \h00, \h00, \h01>>, 1) +ASSUME Accepts(<<\h98, \h01, \h78, \h01, \h61>>, <<"a">>) +\* Maps whose keys are not strings, as Python writes a dict. +ASSUME Accepts(<<\ha2, \h00, \h61, \h78, \h01, \h61, \h79>>, 0 :> "x" @@ 1 :> "y") +ASSUME Accepts(<<\ha2, \h01, \h61, \h61, \h02, \h61, \h62>>, <<"a", "b">>) +ASSUME Accepts(<<\ha1, \h82, \h01, \h02, \h03>>, <<1, 2>> :> 3) +\* Pairs that form a record, and the empty function as an empty map and as no pairs. +ASSUME Accepts(<<\hd9, \h80, \he8, \h81, \h82, \h61, \h61, \h01>>, [a |-> 1]) +ASSUME Accepts(<<\ha0>>, <<>>) +ASSUME Accepts(<<\hd9, \h80, \he8, \h80>>, <<>>) + +----------------------------------------------------------------------------- + \* CBORSerialize writes the bytes of ToCBOR and creates missing parent directories. The bytes \* of "CBOR" read as text: 0x64, the head of a text string of four bytes, is the letter d. ASSUME /\ CBORSerialize("build/cbor/a/b/c/text.cbor", "CBOR") /\ AssertEq(ToCBOR("CBOR"), <<\h64, \h43, \h42, \h4f, \h52>>) /\ AssertEq(FileText("build/cbor/a/b/c/text.cbor"), "dCBOR") +\* CBORDeserialize reads a file as FromCBOR reads its bytes. +ASSUME \A i \in DOMAIN CBORSamples : + /\ CBORSerialize("build/cbor/roundtrip.cbor", CBORSamples[i]) + /\ AssertEq(CBORDeserialize("build/cbor/roundtrip.cbor"), FromCBOR(ToCBOR(CBORSamples[i]))) + +\* A shorter value replaces a longer one; leftover bytes would be rejected as trailing. +ASSUME /\ CBORSerialize("build/cbor/overwrite.cbor", 1..100) + /\ CBORSerialize("build/cbor/overwrite.cbor", 0) + /\ AssertEq(CBORDeserialize("build/cbor/overwrite.cbor"), 0) + ============================================================================= diff --git a/tests/CBORTests/fixtures.py b/tests/CBORTests/fixtures.py index 782bef5..2e1840d 100644 --- a/tests/CBORTests/fixtures.py +++ b/tests/CBORTests/fixtures.py @@ -94,6 +94,7 @@ def enc(v): GOLDEN = { "int": (0, 23, 24, 255, 256, 65535, 65536, 2147483647, -1, -24, -25, -256, -257, -2147483648), "bool": (True, False), + "string": ("", "a", "\u00fc", "\u65e5\u672c", "\U0001F600"), "modelvalue": MODEL_VALUE, "set": Set(100, -1, 10), "set-strings": Set("cbor-zz", "cbor-a", "cbor-aa"), From 118e55a521f9bf23d93885e726c4b9c2729cab7a Mon Sep 17 00:00:00 2001 From: younes-io Date: Tue, 6 Oct 2026 18:32:47 +0200 Subject: [PATCH 3/9] Test every input the CBOR module refuses CBORTests matches the exact message of every input FromCBOR rejects with AssertError, each input written inline as a sequence of hex literals, so every rejection is shown to be an EvalException that names the byte offset rather than a 2154 stack trace. The cases cover truncation, hostile lengths, trailing bytes, types and tags without a TLA+ meaning, integers outside TLC's range, invalid UTF-8, duplicates and incomparable values under TLC equality, unknown model values, and nesting deeper than 512. The tests also cover arguments that are not byte sequences or strings, a missing file, a decoding error that names the file, and values ToCBOR and CBORSerialize cannot encode, and show that a refused value leaves the existing file as it was. https://github.com/tlaplus/tlaplus/issues/1467 [Tests] Signed-off-by: younes-io --- tests/CBORTests.tla | 119 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 119 insertions(+) diff --git a/tests/CBORTests.tla b/tests/CBORTests.tla index 9fd0964..2def3a8 100644 --- a/tests/CBORTests.tla +++ b/tests/CBORTests.tla @@ -247,4 +247,123 @@ ASSUME /\ CBORSerialize("build/cbor/overwrite.cbor", 1..100) /\ CBORSerialize("build/cbor/overwrite.cbor", 0) /\ AssertEq(CBORDeserialize("build/cbor/overwrite.cbor"), 0) +----------------------------------------------------------------------------- + +\* AssertError needs its message as a literal. + +ASSUME AssertError("FromCBOR: the input ends inside a CBOR data item at byte 0.", + FromCBOR(<<>>)) +\* An array of two items that holds one. +ASSUME AssertError("FromCBOR: the input ends inside a CBOR data item at byte 0.", + FromCBOR(<<\h82, \h01>>)) +ASSUME AssertError("FromCBOR: the input ends inside a CBOR data item at byte 0.", + FromCBOR(<<\h1a, \h00, \h00>>)) +\* An array that claims 2^31 - 1 items is refused before anything is allocated. +ASSUME AssertError("FromCBOR: the input ends inside a CBOR data item at byte 0.", + FromCBOR(<<\h9a, \h7f, \hff, \hff, \hff>>)) +ASSUME AssertError("FromCBOR: there are bytes after the first CBOR data item at byte 1.", + FromCBOR(<<\h01, \h01>>)) +\* The offset names the innermost offending item. +ASSUME AssertError("FromCBOR: null has no TLA+ counterpart at byte 2.", + FromCBOR(<<\h82, \h01, \hf6>>)) +ASSUME AssertError("FromCBOR: a floating-point number has no TLA+ counterpart at byte 0.", + FromCBOR(<<\hf9, \h3c, \h00>>)) +ASSUME AssertError("FromCBOR: null has no TLA+ counterpart at byte 0.", + FromCBOR(<<\hf6>>)) +ASSUME AssertError("FromCBOR: undefined has no TLA+ counterpart at byte 0.", + FromCBOR(<<\hf7>>)) +ASSUME AssertError("FromCBOR: a simple value has no TLA+ counterpart at byte 0.", + FromCBOR(<<\hf0>>)) +ASSUME AssertError("FromCBOR: a byte string has no TLA+ counterpart at byte 0.", + FromCBOR(<<\h41, \h00>>)) +ASSUME AssertError("FromCBOR: indefinite-length items are not supported at byte 0.", + FromCBOR(<<\h9f, \h01, \hff>>)) +ASSUME AssertError("FromCBOR: indefinite-length items are not supported at byte 0.", + FromCBOR(<<\h7f, \h61, \h61, \hff>>)) +ASSUME AssertError("FromCBOR: the initial byte 0x1c is not well-formed at byte 0.", + FromCBOR(<<\h1c>>)) +ASSUME AssertError("FromCBOR: the initial byte 0xff is not well-formed at byte 0.", + FromCBOR(<<\hff>>)) +ASSUME AssertError("FromCBOR: tag 1 has no TLA+ counterpart at byte 0.", + FromCBOR(<<\hc1, \h00>>)) +\* A bignum. +ASSUME AssertError("FromCBOR: tag 2 has no TLA+ counterpart at byte 0.", + FromCBOR(<<\hc2, \h41, \h01>>)) +ASSUME AssertError("FromCBOR: tag 39 must enclose a text string at byte 0.", + FromCBOR(<<\hd8, \h27, \h01>>)) +ASSUME AssertError("FromCBOR: tag 258 must enclose an array at byte 0.", + FromCBOR(<<\hd9, \h01, \h02, \ha0>>)) +ASSUME AssertError("FromCBOR: tag 33000 must enclose an array of [key, value] arrays at byte 0.", + FromCBOR(<<\hd9, \h80, \he8, \ha0>>)) +ASSUME AssertError("FromCBOR: tag 33000 must enclose an array of [key, value] arrays at byte 0.", + FromCBOR(<<\hd9, \h80, \he8, \h81, \h01>>)) +ASSUME AssertError("FromCBOR: the integer 2147483648 is outside TLC's range -2147483648..2147483647 at byte 0.", + FromCBOR(<<\h1a, \h80, \h00, \h00, \h00>>)) +ASSUME AssertError("FromCBOR: the integer -2147483649 is outside TLC's range -2147483648..2147483647 at byte 0.", + FromCBOR(<<\h3a, \h80, \h00, \h00, \h00>>)) +ASSUME AssertError("FromCBOR: the integer 18446744073709551615 is outside TLC's range -2147483648..2147483647 at byte 0.", + FromCBOR(<<\h1b, \hff, \hff, \hff, \hff, \hff, \hff, \hff, \hff>>)) +ASSUME AssertError("FromCBOR: the integer -18446744073709551616 is outside TLC's range -2147483648..2147483647 at byte 0.", + FromCBOR(<<\h3b, \hff, \hff, \hff, \hff, \hff, \hff, \hff, \hff>>)) +ASSUME AssertError("FromCBOR: a text string is not valid UTF-8 at byte 0.", + FromCBOR(<<\h61, \hff>>)) +\* U+D800 encoded as if it were a character. +ASSUME AssertError("FromCBOR: a text string is not valid UTF-8 at byte 0.", + FromCBOR(<<\h63, \hed, \ha0, \h80>>)) +ASSUME AssertError("FromCBOR: the key \"a\" occurs twice at byte 0.", + FromCBOR(<<\ha2, \h61, \h61, \h01, \h61, \h61, \h02>>)) +\* The second 1 is not in shortest form: duplicates are found by TLC equality, not by bytes. +ASSUME AssertError("FromCBOR: the element 1 occurs twice at byte 0.", + FromCBOR(<<\hd9, \h01, \h02, \h82, \h01, \h18, \h01>>)) +\* An empty array and an empty map both denote the empty function. +ASSUME AssertError("FromCBOR: the element <<>> occurs twice at byte 0.", + FromCBOR(<<\hd9, \h01, \h02, \h82, \h80, \ha0>>)) +ASSUME AssertError("FromCBOR: the key 0 occurs twice at byte 0.", + FromCBOR(<<\hd9, \h80, \he8, \h82, \h82, \h00, \h01, \h82, \h00, \h02>>)) +ASSUME AssertError("FromCBOR: TLC cannot compare the elements 1 and \"a\" at byte 0.", + FromCBOR(<<\hd9, \h01, \h02, \h82, \h01, \h61, \h61>>)) +ASSUME AssertError("FromCBOR: TLC cannot compare the keys 1 and \"a\" at byte 0.", + FromCBOR(<<\ha2, \h01, \h00, \h61, \h61, \h00>>)) +ASSUME AssertError("FromCBOR: the model value p99 is not defined in the model at byte 0. Declare it in the .cfg or create it with TLCExt!TLCModelValue(\"p99\").", + FromCBOR(<<\hd8, \h27, \h63, \h70, \h39, \h39>>)) +ASSUME AssertError("FromCBOR: data items are nested more than 512 deep at byte 512.", + FromCBOR([i \in 1..513 |-> IF i < 513 THEN \h81 ELSE \h80])) + +ASSUME AssertError("The argument of FromCBOR should be a sequence of integers in 0..255, but instead it is:\n42", + FromCBOR(42)) +ASSUME AssertError("The argument of FromCBOR should be a sequence of integers in 0..255, but instead it is:\n<<1, 256>>", + FromCBOR(<<1, 256>>)) +ASSUME AssertError("The argument of FromCBOR should be a sequence of integers in 0..255, but instead it is:\n<<-1>>", + FromCBOR(<<-1>>)) +ASSUME AssertError("The argument of FromCBOR should be a sequence of integers in 0..255, but instead it is:\n<<\"a\">>", + FromCBOR(<<"a">>)) + +\* The offending value is named even when it is nested. +ASSUME AssertError("ToCBOR cannot encode a special set constant:\nNat", + ToCBOR([a |-> {Nat}])) +ASSUME AssertError("ToCBOR cannot encode an infinite set:\nSUBSET Nat", + ToCBOR(SUBSET Nat)) +ASSUME AssertError("ToCBOR cannot encode a function with the infinite domain:\nNat", + ToCBOR([x \in Nat |-> x])) +\* SubSeq cuts U+1F600 in half, leaving an unpaired surrogate that UTF-8 cannot carry. +ASSUME AssertError("ToCBOR cannot encode a string that contains an unpaired UTF-16 surrogate.", + ToCBOR(SubSeq(FromCBOR(<<\h64, \hf0, \h9f, \h98, \h80>>), 1, 1))) + +ASSUME AssertError("CBORDeserialize could not read tests/CBORTests/missing.cbor: the file does not exist.", + CBORDeserialize("tests/CBORTests/missing.cbor")) +\* A decoding error names the file. The JSON text {} starts with 0x7b, the head of a text string +\* whose length takes the next eight bytes. +ASSUME AssertError("CBORDeserialize could not read tests/CBORTests/empty-object.json: the input ends inside a CBOR data item at byte 0.", + CBORDeserialize("tests/CBORTests/empty-object.json")) +ASSUME AssertError("The first argument of CBORSerialize should be a string, but instead it is:\n42", + CBORSerialize(42, 1)) +ASSUME AssertError("The argument of CBORDeserialize should be a string, but instead it is:\n42", + CBORDeserialize(42)) + +\* A refused value leaves the existing file as it was. +ASSUME /\ CBORSerialize("build/cbor/refused.cbor", "CBOR") + /\ AssertError("CBORSerialize cannot encode a special set constant:\nNat", + CBORSerialize("build/cbor/refused.cbor", <<"a", Nat>>)) + /\ AssertEq(FileText("build/cbor/refused.cbor"), "dCBOR") + ============================================================================= From 2a82e2d819a42042e0ab37a93570482de3611739 Mon Sep 17 00:00:00 2001 From: younes-io Date: Tue, 6 Oct 2026 18:32:47 +0200 Subject: [PATCH 4/9] List the CBOR module in the README The row sits between Bitwise and Combinatorics, where the table's case-insensitive alphabetical order puts it, and links the Java override like the other rows. https://github.com/tlaplus/tlaplus/issues/1467 [Doc] Signed-off-by: younes-io --- README.md | 1 + 1 file changed, 1 insertion(+) diff --git a/README.md b/README.md index 71063b1..42f9cd6 100644 --- a/README.md +++ b/README.md @@ -13,6 +13,7 @@ The Modules | ---: | ---- | :--: | ---- | | [`BagsExt.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/BagsExt.tla) | Additional operators on bags (e.g. `BagAdd`, `BagRemove`, `FoldBag`, etc.) | [✔](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/BagsExt.java) | [@muenchnerkindl](https://github.com/muenchnerkindl), [@lemmy](https://github.com/lemmy) | | [`Bitwise.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/Bitwise.tla) | Bitwise And and shift-right. | [✔](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/Bitwise.java) | [@lemmy](https://github.com/lemmy), [@pfeodrippe](https://github.com/pfeodrippe) | +| [`CBOR.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/CBOR.tla) | CBOR (RFC 8949) encoding and decoding of TLA+ values, in memory or in files, including sets, model values, and functions. | [✔](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/CBOR.java) | [@younes-io](https://github.com/younes-io) | | [`Combinatorics.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/Combinatorics.tla) | Binomial coefficient (N choose K) and factorial operator | [✔](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/Combinatorics.java) | [@lemmy](https://github.com/lemmy) | | [`CSV.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/CSV.tla) | Operations on CSV files | [✔](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/CSV.java) | [@lemmy](https://github.com/lemmy) | | [`DifferentialEquations.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/DifferentialEquations.tla) | see page 178 of [Specifying Systems](https://lamport.azurewebsites.net/tla/book-02-08-08.pdf) | | Leslie Lamport | From 1d77888f1b84ed4ab350f1fcb7851c068e4b0209 Mon Sep 17 00:00:00 2001 From: younes-io Date: Tue, 6 Oct 2026 22:03:22 +0200 Subject: [PATCH 5/9] Make the CBOR module keep the promises its header makes ToCBOR wrote values that FromCBOR refused for their depth. The encoder now counts data items as the decoder does and refuses a value nested more than 512 deep, so an integer can lie inside at most 511 sequences or records, 255 sets, or 170 functions that use tag 33000. The round trip law in CBOR.tla now excludes the values it never held for: those with a set or a function domain whose elements TLC cannot compare, such as {1, "a"}. The decoder checked each length against the bytes that remain, but each of 512 nested arrays could claim those bytes again, and a 4 MB file exhausted a 4 GB heap. A length may now claim only the bytes that the enclosing arrays and maps do not still need. The header of CBOR.tla is the format's specification for producers and readers in other languages, and several statements in it were wrong. Its two ordering examples held under shortest-first order as well; the example is now 10, 100, -1. CBOR libraries do not sort the pairs of tag 33000. Go's fxamacker/cbor rejects only map keys that are arrays, not integers or tagged items. The header now also says that tag 33000 is not registered with IANA yet, and that a function is an array, a map, or tag 33000 depending on its domain alone, so a reader must accept all three forms for the same variable. No golden compared encodings that first differ at a byte of 0x80 or more, so an encoder that sorted signed bytes passed every test. Four goldens now do: two sets of integers and model values, a set of non-ASCII strings, and a function whose domain mixes a model value and an integer. CI runs tests/CBORTests/fixtures.py on Ubuntu, so the golden bytes are checked against the second encoder on every build. https://github.com/tlaplus/tlaplus/issues/1467 [Bug] Signed-off-by: younes-io --- .github/workflows/main.yml | 3 + .github/workflows/pr.yml | 3 + modules/CBOR.tla | 56 +++++++++++------ modules/tlc2/overrides/CBOR.java | 102 +++++++++++++++++++++---------- tests/CBORTests.tla | 44 +++++++++++++ tests/CBORTests/fixtures.py | 7 ++- 6 files changed, 162 insertions(+), 53 deletions(-) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index c658627..399588f 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -35,6 +35,9 @@ jobs: run: echo "date=$(date +'%Y%m%d%H%M')" >> "$GITHUB_OUTPUT" - name: Build with Ant run: ant -noinput -buildfile build.xml -Dtimestamp=${{steps.date.outputs.date}} + - name: Check the CBOR golden bytes against a second encoder + if: matrix.os == 'ubuntu-latest' + run: python3 tests/CBORTests/fixtures.py - name: Create Release id: create_release if: github.event_name == 'push' && matrix.os == 'ubuntu-latest' diff --git a/.github/workflows/pr.yml b/.github/workflows/pr.yml index 48d70a2..1d5cd9f 100644 --- a/.github/workflows/pr.yml +++ b/.github/workflows/pr.yml @@ -22,6 +22,9 @@ jobs: run: echo "date=$(date +'%Y%m%d%H%M')" >> "$GITHUB_OUTPUT" - name: Build with Ant run: ant -noinput -buildfile build.xml -Dtimestamp=${{steps.date.outputs.date}} + - name: Check the CBOR golden bytes against a second encoder + if: matrix.os == 'ubuntu-latest' + run: python3 tests/CBORTests/fixtures.py tlaps: name: Verify TLAPS proofs diff --git a/modules/CBOR.tla b/modules/CBOR.tla index dcd7c0f..044f221 100644 --- a/modules/CBOR.tla +++ b/modules/CBOR.tla @@ -1,12 +1,16 @@ -------------------------------- MODULE CBOR -------------------------------- (***************************************************************************) (* Encodes TLA+ values as CBOR (RFC 8949), either as a sequence of bytes *) -(* or in a file, and decodes them back. Any finite TLA+ value v survives *) -(* the round trip: *) +(* or in a file, and decodes them back. A value v that ToCBOR accepts *) +(* survives the round trip *) (* *) (* FromCBOR(ToCBOR(v)) = v *) (* CBORSerialize(f, v) => CBORDeserialize(f) = v *) (* *) +(* if TLC can compare the elements of every set in v with each other, and *) +(* likewise the elements of every function's domain. TLC cannot compare 1 *) +(* with "a", so ToCBOR writes {1, "a"} and FromCBOR rejects the bytes. *) +(* *) (* TLC implements all four operators in Java (tlc2.overrides.CBOR in the *) (* CommunityModules). The definitions below only stop TLC with an error *) (* message when that implementation is not on TLC's classpath. *) @@ -28,24 +32,36 @@ (* tag 33000 around an array of the pairs *) (* [x, f[x]], one for each x \in DOMAIN f *) (* *) +(* IANA has registered tags 39 and 258. Tag 33000 is not registered yet; *) +(* it lies in the First Come First Served range. *) +(* *) (* The elements of a set, the keys of a map, and the pairs of tag 33000 *) -(* are sorted by their encoded bytes (RFC 8949, section 4.2.1). This is *) -(* not length-first order: the key "z" precedes "aa", and the integer 10 *) -(* precedes -1. Integers and lengths use their shortest form, and all *) -(* lengths are definite. *) +(* are sorted by their encoded bytes (RFC 8949, section 4.2.1). 10 *) +(* precedes 100, which precedes -1, because their encodings are 0a, 18 64, *) +(* and 20. This is neither the order of the values nor the shortest-first *) +(* order of RFC 7049, which puts -1 before 100. Integers and lengths use *) +(* their shortest form, and all lengths are definite. *) (* *) (* A CBOR map always holds a record, so a decoder in any language can *) -(* read it into a native dictionary or struct. Functions keyed by *) -(* integers, model values, tuples, sets, or records use tag 33000 because *) -(* the default decoders of several languages (Go, JavaScript) fail on CBOR *) -(* maps whose keys are arrays or tagged items. *) +(* read it into a native dictionary or struct with string keys. Every *) +(* other function uses tag 33000, because a map with other keys does not *) +(* survive every decoder. Go's fxamacker/cbor rejects a map key that is *) +(* an array, and a JavaScript object turns every key into a string. *) +(* *) +(* The form of a function follows its domain alone. [x \in S |-> 0] is *) +(* an array if S = {} or S = 1..3, a map if S = {"a"}, and tag 33000 if *) +(* S = {1, 3} or S is a set of model values. A variable that holds a *) +(* function can therefore change form from one state to the next, and an *) +(* empty record arrives as the empty array. A reader must accept an *) +(* array, a map, and tag 33000 wherever the spec has a function. *) (* *) (* Producers in other languages need not sort anything, because FromCBOR *) -(* and CBORDeserialize read elements, keys, and pairs in any order. The *) -(* "canonical" modes of CBOR libraries agree with this module on maps, *) -(* whose keys are all strings, but not on sets or tag 33000, which they *) -(* sort length-first. A producer that wants byte-identical output must *) -(* sort by encoded bytes as RFC 8949, section 4.2.1 says. *) +(* and CBORDeserialize read elements, keys, and pairs in any order. A *) +(* producer that wants byte-identical output must sort by encoded bytes *) +(* itself. The "canonical" mode of a CBOR library does not do that. Such *) +(* a mode sorts the keys of a map, where both orders agree because the *) +(* keys are strings, but it leaves the pairs of tag 33000 as given, *) +(* and Python's cbor2 sorts the elements of a set shortest-first. *) (* *) (* FromCBOR and CBORDeserialize also read integers and lengths that are *) (* not in shortest form, and maps whose keys are not strings. They reject *) @@ -53,8 +69,11 @@ (* represent (outside -2^31 .. 2^31-1), floating-point numbers, byte *) (* strings, null, undefined, indefinite lengths, other tags, invalid *) (* UTF-8, data items nested more than 512 deep, and bytes after the first *) -(* data item. A model value must be defined in the model (for example in *) -(* the configuration file); neither operator creates one. *) +(* data item. ToCBOR and CBORSerialize refuse a value that nests deeper. *) +(* A tag is a data item, so an integer can lie inside at most 511 *) +(* sequences or records, 255 sets, or 170 functions that use tag 33000. *) +(* A model value must be defined in the model (for example in the *) +(* configuration file); neither operator creates one. *) (***************************************************************************) LOCAL INSTANCE TLC @@ -62,7 +81,8 @@ LOCAL INSTANCE TLC (***************************************************************************) (* The CBOR encoding of value as a sequence of integers in 0..255, one per *) (* byte. If value cannot be encoded (an infinite set, an operator, a *) -(* string that is not valid Unicode), TLC reports an error. *) +(* string that is not valid Unicode, a value nested too deep), TLC reports *) +(* an error. *) (***************************************************************************) ToCBOR(value) == Assert(FALSE, "ToCBOR needs CommunityModules.jar on TLC's classpath.") diff --git a/modules/tlc2/overrides/CBOR.java b/modules/tlc2/overrides/CBOR.java index 1367f5a..e0c9d12 100644 --- a/modules/tlc2/overrides/CBOR.java +++ b/modules/tlc2/overrides/CBOR.java @@ -67,9 +67,10 @@ * decide how a function is written by one rule, {@link #shape(Value[])}, so the form the encoder writes and * the class the decoder builds cannot drift apart. The class depends only on TLC and the JDK. * - *

Every error is an {@link EvalException}, never a Java exception that TLC would wrap as error 2154. - * A wrong argument type uses the CommunityModules argument codes; errors about a value or a file use - * {@link EC#GENERAL}, whose message TLC prints verbatim. + *

Every error this class raises is an {@link EvalException}, never a Java exception that TLC would wrap + * as error 2154. A wrong argument type uses the CommunityModules argument codes; errors about a value or a + * file use {@link EC#GENERAL}, whose message TLC prints verbatim. An error that TLC raises itself while the + * encoder enumerates a value, such as {x \in Nat : x < 3}, still arrives wrapped. */ public final class CBOR { @@ -90,6 +91,14 @@ private CBOR() { */ private static final int TAG_FUNCTION = 33000; + /** + * The deepest nesting of data items that the decoder reads, which bounds its recursion, so hostile input + * is an error instead of a stack overflow. The encoder refuses to write deeper, so it writes nothing the + * decoder rejects for its depth. A tag is a data item: a set takes two levels and the pairs of tag 33000 + * three. + */ + private static final int MAX_DEPTH = 512; + /** * Guards file reads and writes, not encoding, so that a read in one worker never sees half of * another worker's write to the same file. @@ -125,7 +134,7 @@ private static Shape shape(final Value[] domain) { @TLAPlusOperator(identifier = "ToCBOR", module = "CBOR", warn = false) public static TupleValue toCBOR(final Value value) { - final byte[] bytes = Encoder.encode(value, "ToCBOR"); + final byte[] bytes = Encoder.encode(value, "ToCBOR", 1); final Value[] elems = new Value[bytes.length]; for (int i = 0; i < elems.length; i++) { elems[i] = IntValue.gen(bytes[i] & 0xff); @@ -168,7 +177,7 @@ public static BoolValue serialize(final Value absoluteFilename, final Value valu new String[] { "first", "CBORSerialize", "string", Values.ppr(absoluteFilename.toString()) }); } final String file = ((StringValue) absoluteFilename).val.toString(); - final byte[] bytes = Encoder.encode(value, "CBORSerialize"); + final byte[] bytes = Encoder.encode(value, "CBORSerialize", 1); synchronized (FILES) { try { final Path path = Paths.get(file); @@ -227,13 +236,15 @@ private Encoder(final String operator) { this.operator = operator; } - static byte[] encode(final Value v, final String operator) { + static byte[] encode(final Value v, final String operator, final int depth) { final Encoder e = new Encoder(operator); - e.value(v); + e.value(v, depth); return e.out.toByteArray(); } - private void value(final Value v) { + /** depth is the level of the data item that v becomes, counted as the decoder counts it. */ + private void value(final Value v, final int depth) { + level(depth); if (v instanceof IntValue) { integer(((IntValue) v).val); } else if (v instanceof BoolValue) { @@ -242,9 +253,10 @@ private void value(final Value v) { text(((StringValue) v).val.toString()); } else if (v instanceof ModelValue) { head(TAG, TAG_MODEL_VALUE); + level(depth + 1); text(((ModelValue) v).val.toString()); } else if (v instanceof TupleValue) { - array(((TupleValue) v).elems); + array(((TupleValue) v).elems, depth); } else if (v instanceof RecordValue) { // Not toFcnRcd(), which normalizes the record in place. final RecordValue r = (RecordValue) v; @@ -252,38 +264,47 @@ private void value(final Value v) { for (int i = 0; i < names.length; i++) { names[i] = new StringValue(r.names[i]); } - function(names, r.values); + function(names, r.values, depth); } else if (v instanceof FcnRcdValue) { final FcnRcdValue f = (FcnRcdValue) v; - function(f.getDomainAsValues(), f.values); + function(f.getDomainAsValues(), f.values, depth); } else if (v instanceof FcnLambdaValue) { // The domain, not the function: TLC prints a function's body as its source location. final Value domain = ((FcnLambdaValue) v).getDomain(); if (!domain.isFinite()) { throw cannotEncode("a function with the infinite domain", domain); } - value(v.toFcnRcd()); + value(v.toFcnRcd(), depth); } else if (v instanceof EnumerableValue) { if (!v.isFinite()) { throw cannotEncode("an infinite set", v); } - set(((SetEnumValue) v.toSetEnum()).elems.toArray()); + set(((SetEnumValue) v.toSetEnum()).elems.toArray(), depth); } else { throw cannotEncode(v.getKindString(), v); } } - private void function(final Value[] domain, final Value[] values) { + private void level(final int depth) { + if (depth > MAX_DEPTH) { + throw new EvalException(EC.GENERAL, + operator + " cannot encode a value nested more than " + MAX_DEPTH + " CBOR data items deep."); + } + } + + private void function(final Value[] domain, final Value[] values, final int depth) { final Shape shape = shape(domain); if (shape == Shape.SEQUENCE) { final Value[] elems = new Value[domain.length]; for (int i = 0; i < domain.length; i++) { elems[((IntValue) domain[i]).val - 1] = values[i]; } - array(elems); + array(elems, depth); return; } - final byte[][] keys = encodeEach(domain); + // A pair is an array inside the array inside the tag. + final int entry = shape == Shape.RECORD ? depth + 1 : depth + 3; + final byte[][] keys = encodeEach(domain, entry); final Integer[] order = new Integer[keys.length]; for (int i = 0; i < order.length; i++) { order[i] = i; @@ -300,14 +321,14 @@ private void function(final Value[] domain, final Value[] values) { head(ARRAY, 2); } write(keys[i]); - value(values[i]); + value(values[i], entry); } } - private void array(final Value[] elems) { + private void array(final Value[] elems, final int depth) { head(ARRAY, elems.length); for (final Value e : elems) { - value(e); + value(e, depth + 1); } } @@ -315,8 +336,9 @@ private void array(final Value[] elems) { * An unnormalized set may hold an element twice, possibly in two Java classes. Equal elements have * equal encodings, so dropping equal neighbours after sorting removes exactly TLC's duplicates. */ - private void set(final Value[] elems) { - final byte[][] items = encodeEach(elems); + private void set(final Value[] elems, final int depth) { + level(depth + 1); + final byte[][] items = encodeEach(elems, depth + 2); Arrays.sort(items, Arrays::compareUnsigned); int n = 0; for (final byte[] item : items) { @@ -331,10 +353,10 @@ private void set(final Value[] elems) { } } - private byte[][] encodeEach(final Value[] values) { + private byte[][] encodeEach(final Value[] values, final int depth) { final byte[][] encoded = new byte[values.length][]; for (int i = 0; i < values.length; i++) { - encoded[i] = encode(values[i], operator); + encoded[i] = encode(values[i], operator, depth); } return encoded; } @@ -409,12 +431,11 @@ private EvalException cannotEncode(final String kind, final Value v) { */ private static final class Decoder { - /** Bounds the recursion, so hostile input is an error instead of a stack overflow. */ - private static final int MAX_DEPTH = 512; - private final byte[] in; private final String prefix; private int pos; + /** The bytes that the unread items of the enclosing arrays and maps need, at one byte an item. */ + private int owed; private Map modelValues; Decoder(final byte[] in, final String prefix) { @@ -451,9 +472,10 @@ private Value item(final int depth) { case MAP: final int n = count(start, arg, 2); final Value[] keys = new Value[n], values = new Value[n]; + owed += 2 * n; for (int i = 0; i < n; i++) { - keys[i] = item(depth + 1); - values[i] = item(depth + 1); + keys[i] = member(depth + 1); + values[i] = member(depth + 1); } return function(start, keys, values); default: @@ -501,12 +523,15 @@ private Value tagged(final int start, final long tag, final int depth) { final String complaint = "tag " + TAG_FUNCTION + " must enclose an array of [key, value] arrays"; final int n = arrayHead(start, depth + 1, complaint); final Value[] keys = new Value[n], values = new Value[n]; + owed += n; for (int i = 0; i < n; i++) { + owed--; if (arrayHead(start, depth + 2, complaint) != 2) { throw error(start, complaint); } - keys[i] = item(depth + 3); - values[i] = item(depth + 3); + owed += 2; + keys[i] = member(depth + 3); + values[i] = member(depth + 3); } return function(start, keys, values); } @@ -627,12 +652,19 @@ private ModelValue modelValue(final int start, final String name) { private Value[] items(final int n, final int depth) { final Value[] items = new Value[n]; + owed += n; for (int i = 0; i < n; i++) { - items[i] = item(depth); + items[i] = member(depth); } return items; } + /** The next of the items that an array or a map has added to owed. */ + private Value member(final int depth) { + owed--; + return item(depth); + } + private int initial(final int depth) { if (pos == in.length) { throw error(pos, "the input ends inside a CBOR data item"); @@ -664,9 +696,13 @@ private long argument(final int start, final int major, final int ai) { return arg; } - /** Checked before anything is allocated, so a corrupt length cannot exhaust memory. */ + /** + * Checked before anything is allocated. The bytes owed to the enclosing arrays and maps are not + * available. Otherwise each of 512 nested arrays could claim the rest of the input, and the decoder + * would allocate 512 times the input's size instead of an amount in proportion to it. + */ private int count(final int start, final long n, final int minBytesPerItem) { - if (n < 0 || n > (in.length - pos) / minBytesPerItem) { + if (n < 0 || n > (in.length - pos - owed) / minBytesPerItem) { throw error(start, "the input ends inside a CBOR data item"); } return (int) n; diff --git a/tests/CBORTests.tla b/tests/CBORTests.tla index 2def3a8..99accd4 100644 --- a/tests/CBORTests.tla +++ b/tests/CBORTests.tla @@ -32,6 +32,9 @@ LOCAL INSTANCE Json \* constant that JsonTests declares. LOCAL MV == TLCModelValue("ModelValue") +\* U+00E9, which enters as bytes so that this file stays ASCII. +LOCAL EAcute == FromCBOR(<<\h62, \hc3, \ha9>>) + LOCAL Golden(name, value, bytes) == /\ AssertEq(ToCBOR(value), bytes) /\ AssertEq(FromCBOR(bytes), value) @@ -61,6 +64,14 @@ ASSUME Golden("set-strings", {"cbor-zz", "cbor-a", "cbor-aa"}, ASSUME Golden("set-nested", {{}, {1}, {1, 2}, {2}}, <<\hd9, \h01, \h02, \h84, \hd9, \h01, \h02, \h80, \hd9, \h01, \h02, \h81, \h01, \hd9, \h01, \h02, \h81, \h02, \hd9, \h01, \h02, \h82, \h01, \h02>>) +\* In the next three sets, and in "fcn-mixed", the encodings first differ at a byte that is 0x80 +\* or more, which a comparison of signed bytes would order the other way. +ASSUME Golden("set-wide", {200, 24}, <<\hd9, \h01, \h02, \h82, \h18, \h18, \h18, \hc8>>) +ASSUME Golden("set-modelvalue", {MV, 1}, + <<\hd9, \h01, \h02, \h82, \h01, \hd8, \h27, \h6a, \h4d, \h6f, \h64, \h65, \h6c, \h56, \h61, \h6c, + \h75, \h65>>) +ASSUME Golden("set-utf8", {EAcute, "zz"}, + <<\hd9, \h01, \h02, \h82, \h62, \h7a, \h7a, \h62, \hc3, \ha9>>) ASSUME Golden("emptyset", {}, <<\hd9, \h01, \h02, \h80>>) ASSUME Golden("interval", {1, 2, 3}, <<\hd9, \h01, \h02, \h83, \h01, \h02, \h03>>) ASSUME Golden("seq", <<"a", "b">>, <<\h82, \h61, \h61, \h61, \h62>>) @@ -80,6 +91,9 @@ ASSUME Golden("fcn-record", [r \in [a : {1, 2}] |-> r.a], ASSUME Golden("fcn-modelvalue", [m \in {MV} |-> 0], <<\hd9, \h80, \he8, \h81, \h82, \hd8, \h27, \h6a, \h4d, \h6f, \h64, \h65, \h6c, \h56, \h61, \h6c, \h75, \h65, \h00>>) +ASSUME Golden("fcn-mixed", [x \in {MV, 1} |-> 0], + <<\hd9, \h80, \he8, \h82, \h82, \h01, \h00, \h82, \hd8, \h27, \h6a, \h4d, \h6f, \h64, \h65, \h6c, + \h56, \h61, \h6c, \h75, \h65, \h00>>) LOCAL DumpedTrace == LET s1 == [x |-> 0, y |-> {}] @@ -117,6 +131,20 @@ ASSUME LET bytes == <<\h85, \h60, \h61, \h61, \h62, \hc3, \hbc, \h66, \he6, \h97 ASSUME LET bytes == [i \in 1..512 |-> IF i < 512 THEN \h81 ELSE \h80] IN AssertEq(ToCBOR(FromCBOR(bytes)), bytes) +\* The bytes of the integer 0 inside n values, one inside the other, that each start with wrap. +\* A recursive operator cannot build values this deep: TLC's own evaluation overflows the stack. +LOCAL CBORNested(wrap, n) == + [i \in 1..(n * Len(wrap) + 1) |-> IF i > n * Len(wrap) THEN 0 ELSE wrap[((i - 1) % Len(wrap)) + 1]] +LOCAL CBORInSeq == <<\h81>> +LOCAL CBORInRecord == <<\ha1, \h61, \h61>> +LOCAL CBORInSet == <<\hd9, \h01, \h02, \h81>> +LOCAL CBORInFcn == <<\hd9, \h80, \he8, \h81, \h82, \h00>> + +\* The deepest values ToCBOR writes. A tag is a data item, so a set takes two of the 512 levels +\* and a function that uses tag 33000 three. +ASSUME \A d \in {<>, <>, <>, <>} : + LET bytes == CBORNested(d[1], d[2]) IN AssertEq(ToCBOR(FromCBOR(bytes)), bytes) + ----------------------------------------------------------------------------- ASSUME SameBytes("seq", << <<"a", "b">>, @@ -263,6 +291,9 @@ ASSUME AssertError("FromCBOR: the input ends inside a CBOR data item at byte 0." FromCBOR(<<\h9a, \h7f, \hff, \hff, \hff>>)) ASSUME AssertError("FromCBOR: there are bytes after the first CBOR data item at byte 1.", FromCBOR(<<\h01, \h01>>)) +\* The inner array claims the three bytes that the outer array still needs for its other items. +ASSUME AssertError("FromCBOR: the input ends inside a CBOR data item at byte 1.", + FromCBOR(<<\h84, \h83, \h00, \h00, \h00>>)) \* The offset names the innermost offending item. ASSUME AssertError("FromCBOR: null has no TLA+ counterpart at byte 2.", FromCBOR(<<\h82, \h01, \hf6>>)) @@ -345,6 +376,19 @@ ASSUME AssertError("ToCBOR cannot encode an infinite set:\nSUBSET Nat", ToCBOR(SUBSET Nat)) ASSUME AssertError("ToCBOR cannot encode a function with the infinite domain:\nNat", ToCBOR([x \in Nat |-> x])) +\* One level more than the deepest values: ToCBOR refuses what FromCBOR could not read back. +ASSUME AssertError("ToCBOR cannot encode a value nested more than 512 CBOR data items deep.", + ToCBOR(<>)) +ASSUME AssertError("ToCBOR cannot encode a value nested more than 512 CBOR data items deep.", + ToCBOR([a |-> FromCBOR(CBORNested(CBORInRecord, 511))])) +ASSUME AssertError("ToCBOR cannot encode a value nested more than 512 CBOR data items deep.", + ToCBOR({FromCBOR(CBORNested(CBORInSet, 255))})) +ASSUME AssertError("ToCBOR cannot encode a value nested more than 512 CBOR data items deep.", + ToCBOR(0 :> FromCBOR(CBORNested(CBORInFcn, 170)))) +ASSUME AssertError("FromCBOR: data items are nested more than 512 deep at byte 1024.", + FromCBOR(CBORNested(CBORInSet, 256))) +ASSUME AssertError("FromCBOR: data items are nested more than 512 deep at byte 1024.", + FromCBOR(CBORNested(CBORInFcn, 171))) \* SubSeq cuts U+1F600 in half, leaving an unpaired surrogate that UTF-8 cannot carry. ASSUME AssertError("ToCBOR cannot encode a string that contains an unpaired UTF-16 surrogate.", ToCBOR(SubSeq(FromCBOR(<<\h64, \hf0, \h9f, \h98, \h80>>), 1, 1))) diff --git a/tests/CBORTests/fixtures.py b/tests/CBORTests/fixtures.py index 2e1840d..e2e52f5 100644 --- a/tests/CBORTests/fixtures.py +++ b/tests/CBORTests/fixtures.py @@ -2,8 +2,7 @@ python3 tests/CBORTests/fixtures.py -Run it by hand after changing the encoding or a golden row; CI does not run it. It needs only the -standard library. If the third-party decoder cbor2 (pip install cbor2) is importable, it also prints +CI runs it after the build, and it needs only the standard library. If the third-party decoder cbor2 (pip install cbor2) is importable, it also prints how cbor2 reads every golden, so a reviewer can check their meaning independently of TLC. The encoder below is a second implementation of the encoding table in modules/CBOR.tla that shares @@ -99,6 +98,9 @@ def enc(v): "set": Set(100, -1, 10), "set-strings": Set("cbor-zz", "cbor-a", "cbor-aa"), "set-nested": Set(Set(), Set(1), Set(1, 2), Set(2)), + "set-wide": Set(200, 24), + "set-modelvalue": Set(MODEL_VALUE, 1), + "set-utf8": Set("\u00e9", "zz"), "emptyset": Set(), "interval": Set(1, 2, 3), "seq": ("a", "b"), @@ -109,6 +111,7 @@ def enc(v): "fcn-set": Fn((Set(), 0), (Set(1), 1)), "fcn-record": Fn(({"a": 1}, 1), ({"a": 2}, 2)), "fcn-modelvalue": Fn((MODEL_VALUE, 0)), + "fcn-mixed": Fn((MODEL_VALUE, 0), (1, 0)), "trace": {"counterexample": {"state": Set((1, S1), (2, S2)), "action": Set(((1, S1), {"name": "Next", "location": LOCATION}, (2, S2)))}, "vars": Set("x", "y")}, From 6e149ce9a21d19bf38b188e0c2eafc0d35d20658 Mon Sep 17 00:00:00 2001 From: younes-io Date: Thu, 8 Oct 2026 20:09:37 +0200 Subject: [PATCH 6/9] Require Java 11 to build the module overrides build.xml compiled the overrides with source and target 1.8, but IOUtils already calls Files.readString and Files.writeString, which Java 11 added, and the tla2tools.jar that the build downloads is class version 55 and needs Java 11 to run. The build has needed Java 11 since 2021, when IOUtils adopted those calls. The javac task now passes release 11 instead. With release, javac checks every call against the Java 11 class library rather than the library of the JDK that runs the build, so a call to a newer API fails to compile instead of surfacing in review. [Build] Signed-off-by: younes-io --- build.xml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/build.xml b/build.xml index ec19905..e98aed5 100644 --- a/build.xml +++ b/build.xml @@ -29,8 +29,7 @@ From a932594e2ba9c33de7b9b21f66a21518daad6051 Mon Sep 17 00:00:00 2001 From: younes-io Date: Thu, 8 Oct 2026 20:17:06 +0200 Subject: [PATCH 7/9] Check the CBOR golden bytes from a JUnit test instead of Python tests/CBORTests/fixtures.py checked the golden bytes in CBORTests.tla against a second CBOR encoder, but only CI ran it, only on Ubuntu, and only as a separate workflow step. CBORGoldenTest is a JUnit 4 port of it: the same encoder, the same table of golden values under the same names, and the same checks. Every stated golden must match the bytes this encoder writes, every name must have a value, and every value must be stated by some ASSUME. The test fails once and lists every problem, each with its line in CBORTests.tla and, for a mismatch, the expected bytes as a TLA+ sequence ready to paste. The optional cbor2 printout is gone. The test uses JUnit alone, not tla2tools.jar or CBOR.java, so the two encoders still share no code. The compile target builds tests/java, and the test target runs the test with JUnitCore before TLC, so a golden mismatch fails the build in seconds on every operating system. JUnitCore runs through the plain java task, because Ant's junit task needs ant-junit on the runner. The CI step that ran the Python script is removed, which leaves the workflows as they are upstream. [Tests][Build] Signed-off-by: younes-io --- .github/workflows/main.yml | 3 - .github/workflows/pr.yml | 3 - build.xml | 14 + tests/CBORTests.tla | 7 +- tests/CBORTests/fixtures.py | 185 ---------- tests/java/tlc2/overrides/CBORGoldenTest.java | 322 ++++++++++++++++++ 6 files changed, 340 insertions(+), 194 deletions(-) delete mode 100644 tests/CBORTests/fixtures.py create mode 100644 tests/java/tlc2/overrides/CBORGoldenTest.java diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 399588f..c658627 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -35,9 +35,6 @@ jobs: run: echo "date=$(date +'%Y%m%d%H%M')" >> "$GITHUB_OUTPUT" - name: Build with Ant run: ant -noinput -buildfile build.xml -Dtimestamp=${{steps.date.outputs.date}} - - name: Check the CBOR golden bytes against a second encoder - if: matrix.os == 'ubuntu-latest' - run: python3 tests/CBORTests/fixtures.py - name: Create Release id: create_release if: github.event_name == 'push' && matrix.os == 'ubuntu-latest' diff --git a/.github/workflows/pr.yml b/.github/workflows/pr.yml index 1d5cd9f..48d70a2 100644 --- a/.github/workflows/pr.yml +++ b/.github/workflows/pr.yml @@ -22,9 +22,6 @@ jobs: run: echo "date=$(date +'%Y%m%d%H%M')" >> "$GITHUB_OUTPUT" - name: Build with Ant run: ant -noinput -buildfile build.xml -Dtimestamp=${{steps.date.outputs.date}} - - name: Check the CBOR golden bytes against a second encoder - if: matrix.os == 'ubuntu-latest' - run: python3 tests/CBORTests/fixtures.py tlaps: name: Verify TLAPS proofs diff --git a/build.xml b/build.xml index e98aed5..b86c5cd 100644 --- a/build.xml +++ b/build.xml @@ -31,6 +31,9 @@ + @@ -102,6 +105,17 @@ + + + + + + + + + + + diff --git a/tests/CBORTests.tla b/tests/CBORTests.tla index 99accd4..3217aed 100644 --- a/tests/CBORTests.tla +++ b/tests/CBORTests.tla @@ -18,9 +18,10 @@ ASSUME AssertEq(ToString(DOMAIN [cbora |-> 0, cborzz |-> 0]), "{\"cborzz\", \"cb (***************************************************************************) (* A golden test is an ASSUME that calls Golden or SameBytes with a name *) -(* and the bytes that ToCBOR must return. tests/CBORTests/fixtures.py, an *) -(* encoder that shares no code with CBOR.java, checks those bytes against *) -(* its own encoding of the value it has under that name. *) +(* and the bytes that ToCBOR must return. The JUnit test *) +(* tests/java/tlc2/overrides/CBORGoldenTest.java, an encoder that shares *) +(* no code with CBOR.java, checks those bytes against its own encoding of *) +(* the value it has under that name. *) (* *) (* All definitions are LOCAL because AllTests extends every test module. *) (***************************************************************************) diff --git a/tests/CBORTests/fixtures.py b/tests/CBORTests/fixtures.py deleted file mode 100644 index e2e52f5..0000000 --- a/tests/CBORTests/fixtures.py +++ /dev/null @@ -1,185 +0,0 @@ -"""Checks the golden bytes in tests/CBORTests.tla against a second CBOR encoder. - - python3 tests/CBORTests/fixtures.py - -CI runs it after the build, and it needs only the standard library. If the third-party decoder cbor2 (pip install cbor2) is importable, it also prints -how cbor2 reads every golden, so a reviewer can check their meaning independently of TLC. - -The encoder below is a second implementation of the encoding table in modules/CBOR.tla that shares -no code with CBOR.java. CBORTests.tla states each golden as an ASSUME that calls Golden or SameBytes -with the golden's name and its bytes as a TLA+ sequence of hex literals (<<\\h82, \\h61, ...>>). -TLC checks that ToCBOR writes those bytes; this script checks that they are the bytes this encoder -writes for the value of the same name. It exits non-zero on a mismatch, printing the expected -sequence, on a name it does not know, and on a value it has that no ASSUME states. -""" -import os -import re -import struct -import sys - -TAG_MODEL_VALUE = 39 -TAG_SET = 258 -TAG_FUNCTION = 33000 - - -class MV: - def __init__(self, name): self.name = name - - -class Set: - def __init__(self, *elems): self.elems = elems - - -class Fn: - """A function given by its (x, f[x]) pairs.""" - def __init__(self, *pairs): self.pairs = pairs - - -def head(major, n): - if n < 24: - return bytes([major << 5 | n]) - for ai, fmt, limit in ((24, ">B", 0xFF), (25, ">H", 0xFFFF), (26, ">I", 0xFFFFFFFF), (27, ">Q", 2**64 - 1)): - if n <= limit: - return bytes([major << 5 | ai]) + struct.pack(fmt, n) - raise ValueError(n) - - -def keyed(pairs, as_map): - entries = sorted((enc(k), v) for k, v in pairs) - assert all(a[0] != b[0] for a, b in zip(entries, entries[1:])), "duplicate key" - out = head(5, len(entries)) if as_map else head(6, TAG_FUNCTION) + head(4, len(entries)) - for k, v in entries: - out += k + enc(v) if as_map else head(4, 2) + k + enc(v) - return out - - -def function(pairs): - keys = [k for k, _ in pairs] - if sorted(k for k in keys if type(k) is int) == list(range(1, len(keys) + 1)): - return enc(tuple(v for _, v in sorted(pairs, key=lambda p: p[0]))) - return keyed(pairs, as_map=all(type(k) is str for k in keys)) - - -def enc(v): - if type(v) is bool: - return b"\xf5" if v else b"\xf4" - if type(v) is int: - assert -(2**31) <= v < 2**31, "TLC integers are 32-bit" - return head(0, v) if v >= 0 else head(1, -1 - v) - if type(v) is str: - b = v.encode("utf-8") - return head(3, len(b)) + b - if isinstance(v, MV): - return head(6, TAG_MODEL_VALUE) + enc(v.name) - if isinstance(v, Set): - items = sorted(set(enc(e) for e in v.elems)) - return head(6, TAG_SET) + head(4, len(items)) + b"".join(items) - if isinstance(v, tuple): - return head(4, len(v)) + b"".join(enc(e) for e in v) - if isinstance(v, dict): - return function(list(v.items())) - if isinstance(v, Fn): - return function(list(v.pairs)) - raise TypeError(type(v)) - - -MODEL_VALUE = MV("ModelValue") # tests/AllTests.cfg: CONSTANT ModelValueConstant = ModelValue - -S1 = {"x": 0, "y": Set()} -S2 = {"x": 1, "y": Set(MODEL_VALUE)} -LOCATION = {"beginLine": 5, "beginColumn": 9, "endLine": 5, "endColumn": 33, "module": "T"} - -# name -> value. CBORTests.tla states each value again in TLA+, next to its bytes. -GOLDEN = { - "int": (0, 23, 24, 255, 256, 65535, 65536, 2147483647, -1, -24, -25, -256, -257, -2147483648), - "bool": (True, False), - "string": ("", "a", "\u00fc", "\u65e5\u672c", "\U0001F600"), - "modelvalue": MODEL_VALUE, - "set": Set(100, -1, 10), - "set-strings": Set("cbor-zz", "cbor-a", "cbor-aa"), - "set-nested": Set(Set(), Set(1), Set(1, 2), Set(2)), - "set-wide": Set(200, 24), - "set-modelvalue": Set(MODEL_VALUE, 1), - "set-utf8": Set("\u00e9", "zz"), - "emptyset": Set(), - "interval": Set(1, 2, 3), - "seq": ("a", "b"), - "empty": (), - "record": {"cborzz": 1, "cbora": 2, "cboraa": 3}, - "fcn-int": Fn((0, "x"), (1, "y")), - "fcn-tuple": Fn(((1, 2), 3), ((2, 1), 3)), - "fcn-set": Fn((Set(), 0), (Set(1), 1)), - "fcn-record": Fn(({"a": 1}, 1), ({"a": 2}, 2)), - "fcn-modelvalue": Fn((MODEL_VALUE, 0)), - "fcn-mixed": Fn((MODEL_VALUE, 0), (1, 0)), - "trace": {"counterexample": {"state": Set((1, S1), (2, S2)), - "action": Set(((1, S1), {"name": "Next", "location": LOCATION}, (2, S2)))}, - "vars": Set("x", "y")}, -} - -NAME = re.compile(r'\b(?:Golden|SameBytes)\("([^"]+)"') -HEX_SEQUENCE = re.compile(r'<<\s*(\\h[0-9a-fA-F]{2}(?:\s*,\s*\\h[0-9a-fA-F]{2})*)\s*>>') - - -def tla(data): - """data as a TLA+ sequence of hex literals, 16 to a line.""" - lines = [", ".join(f"\\h{b:02x}" for b in data[i:i + 16]) for i in range(0, len(data), 16)] - return "<<" + ",\n ".join(lines) + ">>" - - -def statements(text): - """Yields each top-level unit of the module, which starts at column 0, with its first line number.""" - line = 1 - for chunk in re.split(r"\n(?=\S)", text): - yield line, chunk - line += chunk.count("\n") + 1 - - -def check(path): - failures = [] - seen = set() - for line, stmt in statements(open(path, encoding="ascii").read()): - names = NAME.findall(stmt) - if not names: - continue - literals = HEX_SEQUENCE.findall(stmt) - if len(set(names)) != 1 or len(literals) != 1: - failures.append(f"line {line}: expected one golden name and one hex sequence, found {names} and " - f"{len(literals)} sequences") - continue - name = names[0] - if name not in GOLDEN: - failures.append(f"line {line}: no value for the golden {name!r}") - continue - seen.add(name) - stated = bytes(int(h[2:], 16) for h in re.findall(r"\\h[0-9a-fA-F]{2}", literals[0])) - expected = enc(GOLDEN[name]) - if stated == expected: - print(f"ok {name} (line {line})") - else: - failures.append(f"line {line}: the bytes of {name!r} differ; this encoder writes\n{tla(expected)}") - failures += [f"no ASSUME states the golden {name!r}" for name in GOLDEN if name not in seen] - for f in failures: - print("FAIL " + f) - return not failures - - -def show_cbor2(): - try: - import cbor2 - except ImportError: - return - print("\ncbor2 reads the goldens as:") - for name, value in GOLDEN.items(): - try: - text = repr(cbor2.loads(enc(value))) - except cbor2.CBORDecodeError as e: - text = f"error: {e}" - print(f" {name}: {text if len(text) <= 200 else text[:200] + '...'}") - - -if __name__ == "__main__": - here = os.path.dirname(os.path.abspath(__file__)) - ok = check(sys.argv[1] if len(sys.argv) > 1 else os.path.join(here, os.pardir, "CBORTests.tla")) - show_cbor2() - sys.exit(0 if ok else 1) diff --git a/tests/java/tlc2/overrides/CBORGoldenTest.java b/tests/java/tlc2/overrides/CBORGoldenTest.java new file mode 100644 index 0000000..8f79285 --- /dev/null +++ b/tests/java/tlc2/overrides/CBORGoldenTest.java @@ -0,0 +1,322 @@ +/******************************************************************************* + * Copyright (c) 2026 Younes Akhouayri. All rights reserved. + * + * The MIT License (MIT) + * + * Permission is hereby granted, free of charge, to any person obtaining a copy + * of this software and associated documentation files (the "Software"), to deal + * in the Software without restriction, including without limitation the rights + * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies + * of the Software, and to permit persons to whom the Software is furnished to do + * so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS + * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR + * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN + * AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION + * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + * + * Contributors: + * Younes Akhouayri - initial API and implementation + ******************************************************************************/ +package tlc2.overrides; + +import static org.junit.Assert.assertEquals; +import static org.junit.Assert.assertTrue; + +import java.io.ByteArrayOutputStream; +import java.io.IOException; +import java.nio.charset.StandardCharsets; +import java.nio.file.Files; +import java.nio.file.Paths; +import java.util.ArrayList; +import java.util.Arrays; +import java.util.Comparator; +import java.util.HashSet; +import java.util.LinkedHashMap; +import java.util.List; +import java.util.Map; +import java.util.TreeSet; +import java.util.regex.Matcher; +import java.util.regex.Pattern; + +import org.junit.Test; + +/** + * Checks the golden bytes in tests/CBORTests.tla against a second CBOR encoder. {@code ant test} runs it on + * every operating system before TLC, and it needs JUnit alone. + * + *

The encoder below is a second implementation of the encoding table in modules/CBOR.tla that shares no + * code with CBOR.java. CBORTests.tla states each golden as an ASSUME that calls Golden or SameBytes with the + * golden's name and its bytes as a TLA+ sequence of hex literals ({@code <<\h82, \h61, ...>>}). TLC checks + * that ToCBOR writes those bytes; this test checks that they are the bytes this encoder writes for the value + * of the same name. It fails on a mismatch, printing the expected sequence, on a name it does not know, and + * on a value it has that no ASSUME states. + */ +public class CBORGoldenTest { + + private static final int TAG_MODEL_VALUE = 39; + private static final int TAG_SET = 258; + private static final int TAG_FUNCTION = 33000; + + private static final Comparator BYTEWISE = Arrays::compareUnsigned; + + private static final class Mv { + final String name; + + Mv(final String name) { + this.name = name; + } + } + + private static final class Set { + final Object[] elems; + + Set(final Object... elems) { + this.elems = elems; + } + } + + /** A function given by its (x, f[x]) pairs. */ + private static final class Fn { + final Object[][] pairs; + + Fn(final Object[]... pairs) { + this.pairs = pairs; + } + } + + private static Object[] pair(final Object x, final Object fx) { + return new Object[] { x, fx }; + } + + private static Map record(final Object... keysAndValues) { + final Map r = new LinkedHashMap<>(); + for (int i = 0; i < keysAndValues.length; i += 2) { + r.put((String) keysAndValues[i], keysAndValues[i + 1]); + } + return r; + } + + private static byte[] head(final int major, final long n) { + final ByteArrayOutputStream out = new ByteArrayOutputStream(); + if (n < 24) { + out.write(major << 5 | (int) n); + return out.toByteArray(); + } + final int ai = n <= 0xFFL ? 24 : n <= 0xFFFFL ? 25 : n <= 0xFFFFFFFFL ? 26 : 27; + final int width = 1 << ai - 24; + out.write(major << 5 | ai); + for (int i = width - 1; i >= 0; i--) { + out.write((int) (n >>> 8 * i)); + } + return out.toByteArray(); + } + + private static byte[] keyed(final List pairs, final boolean asMap) { + final List entries = new ArrayList<>(); + for (final Object[] p : pairs) { + entries.add(new Object[] { encode(p[0]), p[1] }); + } + entries.sort((a, b) -> BYTEWISE.compare((byte[]) a[0], (byte[]) b[0])); + for (int i = 1; i < entries.size(); i++) { + assertTrue("duplicate key", + BYTEWISE.compare((byte[]) entries.get(i - 1)[0], (byte[]) entries.get(i)[0]) != 0); + } + final ByteArrayOutputStream out = new ByteArrayOutputStream(); + if (asMap) { + out.writeBytes(head(5, entries.size())); + } else { + out.writeBytes(head(6, TAG_FUNCTION)); + out.writeBytes(head(4, entries.size())); + } + for (final Object[] e : entries) { + if (!asMap) { + out.writeBytes(head(4, 2)); + } + out.writeBytes((byte[]) e[0]); + out.writeBytes(encode(e[1])); + } + return out.toByteArray(); + } + + private static byte[] function(final List pairs) { + final List intKeys = new ArrayList<>(); + boolean allStrings = true; + for (final Object[] p : pairs) { + if (p[0] instanceof Integer) { + intKeys.add((Integer) p[0]); + } + allStrings &= p[0] instanceof String; + } + intKeys.sort(null); + final List oneToN = new ArrayList<>(); + for (int i = 1; i <= pairs.size(); i++) { + oneToN.add(i); + } + if (intKeys.equals(oneToN)) { + final Object[] values = new Object[pairs.size()]; + for (final Object[] p : pairs) { + values[(Integer) p[0] - 1] = p[1]; + } + return encode(Arrays.asList(values)); + } + return keyed(pairs, allStrings); + } + + private static byte[] encode(final Object v) { + final ByteArrayOutputStream out = new ByteArrayOutputStream(); + if (v instanceof Boolean) { + out.write((Boolean) v ? 0xf5 : 0xf4); + } else if (v instanceof Integer) { + final int n = (Integer) v; + out.writeBytes(n >= 0 ? head(0, n) : head(1, -1L - n)); + } else if (v instanceof String) { + final byte[] b = ((String) v).getBytes(StandardCharsets.UTF_8); + out.writeBytes(head(3, b.length)); + out.writeBytes(b); + } else if (v instanceof Mv) { + out.writeBytes(head(6, TAG_MODEL_VALUE)); + out.writeBytes(encode(((Mv) v).name)); + } else if (v instanceof Set) { + final TreeSet items = new TreeSet<>(BYTEWISE); + for (final Object e : ((Set) v).elems) { + items.add(encode(e)); + } + out.writeBytes(head(6, TAG_SET)); + out.writeBytes(head(4, items.size())); + items.forEach(out::writeBytes); + } else if (v instanceof List) { + final List tuple = (List) v; + out.writeBytes(head(4, tuple.size())); + for (final Object e : tuple) { + out.writeBytes(encode(e)); + } + } else if (v instanceof Map) { + final List pairs = new ArrayList<>(); + ((Map) v).forEach((k, fk) -> pairs.add(pair(k, fk))); + out.writeBytes(function(pairs)); + } else if (v instanceof Fn) { + out.writeBytes(function(Arrays.asList(((Fn) v).pairs))); + } else { + throw new AssertionError("no CBOR encoding for a " + v.getClass().getName() + + "; TLC integers are 32-bit, so a golden integer is an Integer"); + } + return out.toByteArray(); + } + + private static final Mv MODEL_VALUE = new Mv("ModelValue"); + + private static final Map S1 = record("x", 0, "y", new Set()); + private static final Map S2 = record("x", 1, "y", new Set(MODEL_VALUE)); + private static final Map LOCATION = record("beginLine", 5, "beginColumn", 9, "endLine", 5, + "endColumn", 33, "module", "T"); + + private static final Map GOLDEN = record( + "int", List.of(0, 23, 24, 255, 256, 65535, 65536, 2147483647, -1, -24, -25, -256, -257, -2147483648), + "bool", List.of(true, false), + "string", List.of("", "a", "\u00fc", "\u65e5\u672c", "\uD83D\uDE00"), + "modelvalue", MODEL_VALUE, + "set", new Set(100, -1, 10), + "set-strings", new Set("cbor-zz", "cbor-a", "cbor-aa"), + "set-nested", new Set(new Set(), new Set(1), new Set(1, 2), new Set(2)), + "set-wide", new Set(200, 24), + "set-modelvalue", new Set(MODEL_VALUE, 1), + "set-utf8", new Set("\u00e9", "zz"), + "emptyset", new Set(), + "interval", new Set(1, 2, 3), + "seq", List.of("a", "b"), + "empty", List.of(), + "record", record("cborzz", 1, "cbora", 2, "cboraa", 3), + "fcn-int", new Fn(pair(0, "x"), pair(1, "y")), + "fcn-tuple", new Fn(pair(List.of(1, 2), 3), pair(List.of(2, 1), 3)), + "fcn-set", new Fn(pair(new Set(), 0), pair(new Set(1), 1)), + "fcn-record", new Fn(pair(record("a", 1), 1), pair(record("a", 2), 2)), + "fcn-modelvalue", new Fn(pair(MODEL_VALUE, 0)), + "fcn-mixed", new Fn(pair(MODEL_VALUE, 0), pair(1, 0)), + "trace", record( + "counterexample", record( + "state", new Set(List.of(1, S1), List.of(2, S2)), + "action", new Set(List.of(List.of(1, S1), record("name", "Next", "location", LOCATION), + List.of(2, S2)))), + "vars", new Set("x", "y"))); + + private static final Pattern NAME = Pattern.compile("\\b(?:Golden|SameBytes)\\(\"([^\"]+)\""); + private static final Pattern HEX_SEQUENCE = Pattern + .compile("<<\\s*(\\\\h[0-9a-fA-F]{2}(?:\\s*,\\s*\\\\h[0-9a-fA-F]{2})*)\\s*>>"); + private static final Pattern HEX = Pattern.compile("\\\\h([0-9a-fA-F]{2})"); + private static final Pattern TOP_LEVEL_STATEMENT_BREAK = Pattern.compile("\n(?=\\S)"); + + private static List findAll(final Pattern p, final String s) { + final List found = new ArrayList<>(); + final Matcher m = p.matcher(s); + while (m.find()) { + found.add(m.group(1)); + } + return found; + } + + private static String tlaHexSequence(final byte[] data) { + final List lines = new ArrayList<>(); + for (int i = 0; i < data.length; i += 16) { + final List line = new ArrayList<>(); + for (int j = i; j < Math.min(i + 16, data.length); j++) { + line.add(String.format("\\h%02x", data[j] & 0xff)); + } + lines.add(String.join(", ", line)); + } + return "<<" + String.join(",\n ", lines) + ">>"; + } + + @Test + public void goldensMatchASecondEncoder() throws IOException { + final String text = Files.readString(Paths.get(System.getProperty("basepath", "tests"), "CBORTests.tla"), + StandardCharsets.US_ASCII); + final List failures = new ArrayList<>(); + final HashSet seen = new HashSet<>(); + int line = 1; + for (final String stmt : TOP_LEVEL_STATEMENT_BREAK.split(text, -1)) { + final int stmtLine = line; + line += stmt.chars().filter(c -> c == '\n').count() + 1; + final List names = findAll(NAME, stmt); + if (names.isEmpty()) { + continue; + } + final List literals = findAll(HEX_SEQUENCE, stmt); + if (new HashSet<>(names).size() != 1 || literals.size() != 1) { + failures.add(String.format( + "line %d: expected one golden name and one hex sequence, found %s and %d sequences", stmtLine, + names, literals.size())); + continue; + } + final String name = names.get(0); + if (!GOLDEN.containsKey(name)) { + failures.add(String.format("line %d: no value for the golden '%s'", stmtLine, name)); + continue; + } + seen.add(name); + final List hex = findAll(HEX, literals.get(0)); + final byte[] stated = new byte[hex.size()]; + for (int i = 0; i < stated.length; i++) { + stated[i] = (byte) Integer.parseInt(hex.get(i), 16); + } + final byte[] expected = encode(GOLDEN.get(name)); + if (Arrays.equals(stated, expected)) { + System.out.printf("ok %s (line %d)%n", name, stmtLine); + } else { + failures.add(String.format("line %d: the bytes of '%s' differ; this encoder writes\n%s", stmtLine, + name, tlaHexSequence(expected))); + } + } + for (final String name : GOLDEN.keySet()) { + if (!seen.contains(name)) { + failures.add(String.format("no ASSUME states the golden '%s'", name)); + } + } + assertEquals("", String.join("\n", failures)); + } +} From 9b1d5712de1a594e68afbb5628af749b0c334df2 Mon Sep 17 00:00:00 2001 From: younes-io Date: Fri, 9 Oct 2026 06:50:42 +0200 Subject: [PATCH 8/9] Record that IANA registered tag 33000 The module header and the TAG_FUNCTION comment said the tag was not registered yet. IANA assigned it on 2026-10-08, with the semantics the header describes: https://www.iana.org/assignments/cbor-tags/cbor-tags.xhtml [Doc] Signed-off-by: younes-io --- modules/CBOR.tla | 4 ++-- modules/tlc2/overrides/CBOR.java | 6 +++--- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/modules/CBOR.tla b/modules/CBOR.tla index 044f221..e018497 100644 --- a/modules/CBOR.tla +++ b/modules/CBOR.tla @@ -32,8 +32,8 @@ (* tag 33000 around an array of the pairs *) (* [x, f[x]], one for each x \in DOMAIN f *) (* *) -(* IANA has registered tags 39 and 258. Tag 33000 is not registered yet; *) -(* it lies in the First Come First Served range. *) +(* IANA has registered tags 39, 258, and 33000; see *) +(* https://www.iana.org/assignments/cbor-tags/cbor-tags.xhtml *) (* *) (* The elements of a set, the keys of a map, and the pairs of tag 33000 *) (* are sorted by their encoded bytes (RFC 8949, section 4.2.1). 10 *) diff --git a/modules/tlc2/overrides/CBOR.java b/modules/tlc2/overrides/CBOR.java index e0c9d12..cbb1fe3 100644 --- a/modules/tlc2/overrides/CBOR.java +++ b/modules/tlc2/overrides/CBOR.java @@ -85,9 +85,9 @@ private CBOR() { /** IANA tag 258, "Mathematical finite set", around the array of a set's elements. */ private static final int TAG_SET = 258; /** - * Around the [x, f[x]] pairs of a function that is neither a sequence nor a record. Not yet registered - * with IANA; 33000 lies in the First Come First Served range. CBOR.tla is the only other place that - * names it. + * IANA tag 33000, "TLA+ function as an array of [argument, value] pairs", registered for this module on + * 2026-10-08, around the [x, f[x]] pairs of a function that is neither a sequence nor a record. CBOR.tla + * is the only other place that names it. */ private static final int TAG_FUNCTION = 33000; From cabdf530e7fa1b08eac2136c07085e1dcb5caa2c Mon Sep 17 00:00:00 2001 From: younes-io Date: Fri, 9 Oct 2026 18:27:35 +0200 Subject: [PATCH 9/9] Address CBOR review feedback Use TLC conversions for function representations while preserving encoded-byte ordering and supported mixed inputs. Remove the fixed nesting limit, clarify decoder errors and model-value handling, and add regression coverage. Keep the in-memory operators public. Shorten the module header and move the encoding contract to docs/CBOR.md. Signed-off-by: younes-io --- README.md | 2 +- docs/CBOR.md | 141 ++++++++++++++++++ modules/CBOR.tla | 104 ++++--------- modules/tlc2/overrides/CBOR.java | 244 ++++++++++++------------------- tests/CBORTests.tla | 57 +++++--- 5 files changed, 297 insertions(+), 251 deletions(-) create mode 100644 docs/CBOR.md diff --git a/README.md b/README.md index 42f9cd6..185f97d 100644 --- a/README.md +++ b/README.md @@ -13,7 +13,7 @@ The Modules | ---: | ---- | :--: | ---- | | [`BagsExt.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/BagsExt.tla) | Additional operators on bags (e.g. `BagAdd`, `BagRemove`, `FoldBag`, etc.) | [✔](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/BagsExt.java) | [@muenchnerkindl](https://github.com/muenchnerkindl), [@lemmy](https://github.com/lemmy) | | [`Bitwise.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/Bitwise.tla) | Bitwise And and shift-right. | [✔](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/Bitwise.java) | [@lemmy](https://github.com/lemmy), [@pfeodrippe](https://github.com/pfeodrippe) | -| [`CBOR.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/CBOR.tla) | CBOR (RFC 8949) encoding and decoding of TLA+ values, in memory or in files, including sets, model values, and functions. | [✔](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/CBOR.java) | [@younes-io](https://github.com/younes-io) | +| [`CBOR.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/CBOR.tla) | CBOR (RFC 8949) encoding and decoding of TLA+ values, in memory or in files, including sets, model values, and functions. [Encoding reference](docs/CBOR.md). | [✔](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/CBOR.java) | [@younes-io](https://github.com/younes-io) | | [`Combinatorics.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/Combinatorics.tla) | Binomial coefficient (N choose K) and factorial operator | [✔](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/Combinatorics.java) | [@lemmy](https://github.com/lemmy) | | [`CSV.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/CSV.tla) | Operations on CSV files | [✔](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/CSV.java) | [@lemmy](https://github.com/lemmy) | | [`DifferentialEquations.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/DifferentialEquations.tla) | see page 178 of [Specifying Systems](https://lamport.azurewebsites.net/tla/book-02-08-08.pdf) | | Leslie Lamport | diff --git a/docs/CBOR.md b/docs/CBOR.md new file mode 100644 index 0000000..c0a6089 --- /dev/null +++ b/docs/CBOR.md @@ -0,0 +1,141 @@ +# CBOR encoding reference + +The `CBOR` module encodes TLA+ values as [CBOR, defined by RFC 8949](https://www.rfc-editor.org/rfc/rfc8949.html), and decodes CBOR into TLC values. The rules below define this module's encoding contract. + +All four public operators require the CommunityModules Java overrides on TLC's classpath, including `tlc2.overrides.CBOR`. The TLA+ definitions report an error when the overrides are absent. The repository [README](../README.md#how-to-use-it) describes library and classpath setup. + +## Operators + +| Operator | Result and effects | +| --- | --- | +| `ToCBOR(value)` | The encoding of `value` as a sequence of integers in `0..255`, one per byte. No file I/O. | +| `FromCBOR(bytes)` | The TLC value represented by one CBOR data item. `bytes` is a sequence of integers in `0..255`. No file I/O. | +| `CBORSerialize(absoluteFilename, value)` | Writes the same bytes as `ToCBOR(value)` and returns `TRUE`. Creates missing parent directories and replaces an existing file. | +| `CBORDeserialize(absoluteFilename)` | Reads a file and decodes its bytes with the same rules as `FromCBOR`. | + +`FromCBOR` also accepts functions that TLC can convert to sequences, such as `[i \in 1..n |-> b[i]]`. The file operators take a filename string. `CBORSerialize` encodes the entire value before it touches the file, so an encoding failure leaves an existing file unchanged. A file I/O failure reports an error. + +### In-memory expressions + +The public `ToCBOR` operator supports encoded message-size checks without temporary files. The public `FromCBOR` operator interprets byte inputs directly, including byte sequences held in model state. + +```tla +EXTENDS Naturals, Sequences, CBOR + +Message == [id |-> 1, payload |-> <>] +FitsPacket(message, maxBytes) == Len(ToCBOR(message)) <= maxBytes +Fits == FitsPacket(Message, 1024) +Decoded == FromCBOR(<<130, 1, 245>>) \* equals <<1, TRUE>> +RoundTrip == FromCBOR(ToCBOR(Message)) = Message +``` + +`Len(ToCBOR(message))` counts CBOR bytes, not characters or transport framing bytes. `Naturals` supplies `<=`, and `Sequences` supplies `Len`. + +### File expressions + +The file operators exchange values with external programs or load CBOR fixtures. + +```tla +EXTENDS CBOR + +Message == [id |-> 1, payload |-> <>] +WriteMessage == CBORSerialize("/tmp/message.cbor", Message) +ReadMessage == CBORDeserialize("/tmp/message.cbor") +``` + +The read expression requires an existing file. A zero-argument definition such as `ReadMessage` is constant-level, so TLC reads the file once before model checking. These definitions do not establish an execution order between the write and the read. + +## Encoding types and tags + +For supported values, values that TLC considers equal produce identical bytes, regardless of their internal Java representation or string interning order. + +| TLA+ value | CBOR representation | +| --- | --- | +| Integer | Integer, major type 0 for nonnegative values or major type 1 for negative values. | +| `TRUE`, `FALSE` | CBOR `true`, `false`. | +| String | UTF-8 text string. | +| Model value | Tag 39 around its name as a text string. | +| Finite set | Tag 258 around an array of its elements. | +| Function `f` with `DOMAIN f = 1..n` | Array of `f[1]`, ..., `f[n]`. This includes sequences, tuples, and the empty function. | +| Function with a nonempty domain of strings, a record | Map from each domain element `x` to `f[x]`. | +| Other finite function | Tag 33000 around an array of two-element arrays `[x, f[x]]`, one for each domain element `x`. | + +The [IANA CBOR tag registry](https://www.iana.org/assignments/cbor-tags/cbor-tags.xhtml) lists tag 39, "Identifier", tag 258, "Mathematical finite set", and tag 33000, "TLA+ function as an array of [argument, value] pairs". The two-element arrays in tag 33000 are CBOR arrays, not TLA+ record syntax. + +### Function representation follows the domain + +The encoding depends on the function's domain, not how the function was written in TLA+. For `[x \in S |-> 0]`, the representations are: + +| Domain `S` | Representation | +| --- | --- | +| `{}` | Empty array. | +| `1..3` | Array. | +| `{"a"}` | Map with a text key. | +| `{1, 3}` | Tag 33000 with argument-value pairs. | +| A nonempty set of model values | Tag 33000 with argument-value pairs. | + +A variable that holds a function can change CBOR representation between states. The empty record encodes as an empty array. A consumer of an arbitrary TLA+ function must account for arrays, maps, and tag 33000. Sequences remain arrays. Other functions that are not records use tag 33000. + +### Deterministic ordering and widths + +The encoder sorts map keys by unsigned lexicographic order of their complete encoded bytes, as in [RFC 8949, section 4.2.1](https://www.rfc-editor.org/rfc/rfc8949.html#section-4.2.1). It uses the same ordering for set elements and for arguments in tag 33000 arrays. Sequence elements retain their sequence order. + +For example, `10` precedes `100`, which precedes `-1`, because their encodings are `0a`, `18 64`, and `20`. This is not numeric order. It is also not the length-first ordering in [RFC 7049, section 3.9](https://www.rfc-editor.org/rfc/rfc7049.html#section-3.9), which puts `-1` before `100`. + +Integers, tags, and lengths use their shortest available argument widths. All lengths are definite. The encoder removes duplicate representations of equal set elements, so internal duplicates do not change a set's encoding. + +## Interoperability + +The encoder emits CBOR maps only for records with string keys. Such maps fit native dictionaries or structures with string keys. Sequences use arrays, and other functions use tag 33000 rather than maps with arbitrary keys. + +Arbitrary map keys do not fit every language's native dictionary representation. For example, an array-valued map key can fail when fxamacker/cbor decodes it into a Go map because Go slices cannot be map keys. JavaScript objects convert their keys to strings. The tagged array of pairs preserves function arguments without requiring a native dictionary to support them as keys. A consumer still needs to interpret the module's tags. + +Foreign producers need not sort set elements, map keys, or function pairs for these decoders. They must follow this module's ordering and width rules to produce byte-identical output. + +A library option called "canonical" is not sufficient evidence of compatibility. Map-key sorting alone does not sort the pairs inside tag 33000. For shortest-form text keys, bytewise and length-first map ordering agree, but those orderings differ for general set elements and function arguments. Python cbor2's canonical set encoding uses length-first ordering, which can differ from this module's ordering. Library behavior can vary with versions and options. The module's rules above are authoritative for byte-identical output. + +## Decoder acceptance and rejection + +`FromCBOR` and `CBORDeserialize` decode exactly one CBOR data item. They return TLC integers, booleans, strings, sequences, sets, records, functions, or existing model values. + +The decoders accept these noncanonical forms: + +- Integers, tags, and lengths with argument widths longer than necessary, within the supported value and input limits. +- Set elements, map keys, and tag 33000 pairs in any order. +- Maps with non-string keys, when TLC can represent and compare those keys. + +Maps and tag 33000 functions are converted according to their domains. A function with domain `1..n` becomes a sequence, a function with a nonempty string domain becomes a record, and another function remains a function. Re-encoding a decoded value uses the encoder's representation and ordering, not necessarily the original bytes. + +The decoders reject these inputs: + +- Duplicate set elements or duplicate function keys, including map keys. Duplicates are determined by TLC value comparison, not by byte equality. For example, `01` and `18 01` both encode the integer `1`. +- Set elements or function keys that TLC cannot compare with one another. +- Integers outside `-2147483648..2147483647`. +- Floating-point numbers, CBOR byte strings, `null`, `undefined`, and other unsupported simple values. +- Indefinite-length items, unsupported tags, and malformed CBOR, including truncated input. +- Tag 39 without a text string, tag 258 without an array, or tag 33000 without an array of two-element arrays. +- Invalid UTF-8 text. +- Model value names that are not known to the current TLC model. +- Any bytes after the first data item. + +Decode errors identify a zero-based byte offset. An invalid `FromCBOR` argument, such as a non-sequence or an integer outside `0..255`, produces an argument error instead. + +## Round trips and limits + +For a value `v` accepted by the encoder, the round-trip equation is: + +```tla +FromCBOR(ToCBOR(v)) = v +``` + +The equation requires TLC to be able to compare the elements of each set in `v`, and the domain elements of each function in `v`. TLC cannot compare `1` with `"a"`. `ToCBOR` can encode `{1, "a"}`, but `FromCBOR` rejects those bytes. The same comparability restriction applies to file round trips. + +After a successful `CBORSerialize(f, v)`, decoding the unchanged file with `CBORDeserialize(f)` returns `v`, subject to those round-trip requirements. The serialization operator itself returns `TRUE`, not the encoded value. + +Sets and function domains must be finite, and TLC must be able to enumerate them. Function arguments and values must themselves be encodable. Operators and other unsupported TLC values cannot be encoded. Integers are limited to TLC's signed 32-bit range. + +Strings must contain valid Unicode. The encoder rejects an unpaired UTF-16 surrogate rather than silently replacing it. The decoder rejects malformed UTF-8 rather than inserting a replacement character. + +Tag 39 decoding reuses model values already known to TLC, for example values declared in the model's configuration file. It never creates a model value from an input name. Unknown names are errors. + +There is no fixed nesting limit. Deep values can exhaust the JVM stack and cause `StackOverflowError` during encoding or decoding. A larger JVM `-Xss` setting can allow deeper values but does not remove that limit. diff --git a/modules/CBOR.tla b/modules/CBOR.tla index e018497..049ad1e 100644 --- a/modules/CBOR.tla +++ b/modules/CBOR.tla @@ -1,88 +1,38 @@ -------------------------------- MODULE CBOR -------------------------------- (***************************************************************************) -(* Encodes TLA+ values as CBOR (RFC 8949), either as a sequence of bytes *) -(* or in a file, and decodes them back. A value v that ToCBOR accepts *) -(* survives the round trip *) -(* *) -(* FromCBOR(ToCBOR(v)) = v *) -(* CBORSerialize(f, v) => CBORDeserialize(f) = v *) -(* *) -(* if TLC can compare the elements of every set in v with each other, and *) -(* likewise the elements of every function's domain. TLC cannot compare 1 *) -(* with "a", so ToCBOR writes {1, "a"} and FromCBOR rejects the bytes. *) -(* *) -(* TLC implements all four operators in Java (tlc2.overrides.CBOR in the *) -(* CommunityModules). The definitions below only stop TLC with an error *) -(* message when that implementation is not on TLC's classpath. *) -(* *) -(* Encoding. Every value has exactly one encoding, so values that TLC *) -(* considers equal are written as identical bytes: *) -(* *) -(* integer CBOR integer (major type 0 or 1) *) -(* TRUE, FALSE CBOR true, false *) -(* string CBOR text string (UTF-8) *) -(* model value tag 39 around its name as a text string *) -(* set tag 258 around an array of its elements *) -(* function f with DOMAIN f = 1..n, including every sequence, every *) -(* tuple, and the empty function *) -(* array of f[1], ..., f[n] *) -(* function f whose domain is a non-empty set of strings (a record) *) -(* map from each x \in DOMAIN f to f[x] *) -(* any other function f *) -(* tag 33000 around an array of the pairs *) -(* [x, f[x]], one for each x \in DOMAIN f *) -(* *) -(* IANA has registered tags 39, 258, and 33000; see *) -(* https://www.iana.org/assignments/cbor-tags/cbor-tags.xhtml *) -(* *) -(* The elements of a set, the keys of a map, and the pairs of tag 33000 *) -(* are sorted by their encoded bytes (RFC 8949, section 4.2.1). 10 *) -(* precedes 100, which precedes -1, because their encodings are 0a, 18 64, *) -(* and 20. This is neither the order of the values nor the shortest-first *) -(* order of RFC 7049, which puts -1 before 100. Integers and lengths use *) -(* their shortest form, and all lengths are definite. *) -(* *) -(* A CBOR map always holds a record, so a decoder in any language can *) -(* read it into a native dictionary or struct with string keys. Every *) -(* other function uses tag 33000, because a map with other keys does not *) -(* survive every decoder. Go's fxamacker/cbor rejects a map key that is *) -(* an array, and a JavaScript object turns every key into a string. *) -(* *) -(* The form of a function follows its domain alone. [x \in S |-> 0] is *) -(* an array if S = {} or S = 1..3, a map if S = {"a"}, and tag 33000 if *) -(* S = {1, 3} or S is a set of model values. A variable that holds a *) -(* function can therefore change form from one state to the next, and an *) -(* empty record arrives as the empty array. A reader must accept an *) -(* array, a map, and tag 33000 wherever the spec has a function. *) -(* *) -(* Producers in other languages need not sort anything, because FromCBOR *) -(* and CBORDeserialize read elements, keys, and pairs in any order. A *) -(* producer that wants byte-identical output must sort by encoded bytes *) -(* itself. The "canonical" mode of a CBOR library does not do that. Such *) -(* a mode sorts the keys of a map, where both orders agree because the *) -(* keys are strings, but it leaves the pairs of tag 33000 as given, *) -(* and Python's cbor2 sorts the elements of a set shortest-first. *) -(* *) -(* FromCBOR and CBORDeserialize also read integers and lengths that are *) -(* not in shortest form, and maps whose keys are not strings. They reject *) -(* duplicate set elements and duplicate keys, integers that TLC cannot *) -(* represent (outside -2^31 .. 2^31-1), floating-point numbers, byte *) -(* strings, null, undefined, indefinite lengths, other tags, invalid *) -(* UTF-8, data items nested more than 512 deep, and bytes after the first *) -(* data item. ToCBOR and CBORSerialize refuse a value that nests deeper. *) -(* A tag is a data item, so an integer can lie inside at most 511 *) -(* sequences or records, 255 sets, or 170 functions that use tag 33000. *) -(* A model value must be defined in the model (for example in the *) -(* configuration file); neither operator creates one. *) +(* Encodes TLA+ values as CBOR (RFC 8949) and decodes them back. *) +(* CBORSerialize and CBORDeserialize exchange values through files. *) +(* Public ToCBOR and FromCBOR work in memory, without file I/O. *) +(* ToCBOR returns a sequence of integers in 0..255, one per encoded byte. *) +(* Use its length to check message sizes, or FromCBOR to interpret bytes. *) +(* *) +(* In a module that uses CBOR: *) +(* EXTENDS Naturals, Sequences, CBOR *) +(* Message == [id |-> 1, payload |-> <>] *) +(* Fits == Len(ToCBOR(Message)) <= 1024 *) +(* Decoded == FromCBOR(<<130, 1, 245>>) \* equals <<1, TRUE>> *) +(* *) +(* For files, using the same imports and Message definition: *) +(* WriteMessage == CBORSerialize("/tmp/message.cbor", Message) *) +(* ReadMessage == CBORDeserialize("/tmp/message.cbor") *) +(* *) +(* Requires CommunityModules.jar or CommunityModules-deps.jar on TLC's *) +(* classpath. See README.md for setup. *) +(* Sets and function domains must be finite and enumerable by TLC. *) +(* Integers must fit TLC's range, and strings must be valid Unicode. *) +(* Decoding reuses existing model values only. *) +(* Set elements and function domain elements must be TLC-comparable for *) +(* round trips. FromCBOR rejects the encoding of {1, "a"}. *) +(* Unsupported or malformed inputs fail. Deep nesting can exhaust the *) +(* JVM stack. See docs/CBOR.md in this repository for the full contract. *) (***************************************************************************) LOCAL INSTANCE TLC (***************************************************************************) (* The CBOR encoding of value as a sequence of integers in 0..255, one per *) -(* byte. If value cannot be encoded (an infinite set, an operator, a *) -(* string that is not valid Unicode, a value nested too deep), TLC reports *) -(* an error. *) +(* byte. If value cannot be encoded (an infinite set, an operator, *) +(* or a string that is not valid Unicode), TLC reports an error. *) (***************************************************************************) ToCBOR(value) == Assert(FALSE, "ToCBOR needs CommunityModules.jar on TLC's classpath.") diff --git a/modules/tlc2/overrides/CBOR.java b/modules/tlc2/overrides/CBOR.java index cbb1fe3..0e12c46 100644 --- a/modules/tlc2/overrides/CBOR.java +++ b/modules/tlc2/overrides/CBOR.java @@ -56,20 +56,21 @@ import tlc2.value.impl.TupleValue; import tlc2.value.impl.Value; import util.Assert.TLCRuntimeException; -import util.UniqueString; /** * Module overrides for CBOR.tla: encode a finite TLA+ value as CBOR (RFC 8949), as a sequence of bytes or - * in a file, and decode it back. CBOR.tla documents the encoding; this class is its only implementation. + * in a file, and decode it back. CBOR.tla describes the operators. docs/CBOR.md specifies the encoding. * *

There is no intermediate data model. {@link Encoder} walks TLC values and writes bytes, and - * {@link Decoder} reads bytes and builds TLC values. The four operators are thin shells around them. Both - * decide how a function is written by one rule, {@link #shape(Value[])}, so the form the encoder writes and - * the class the decoder builds cannot drift apart. The class depends only on TLC and the JDK. + * {@link Decoder} reads bytes and builds TLC values. The encoder and the decoder's map and tagged-function + * paths use {@link #functionValue(FcnRcdValue)} to select a TLC representation. The class depends only on + * TLC and the JDK. * - *

Every error this class raises is an {@link EvalException}, never a Java exception that TLC would wrap - * as error 2154. A wrong argument type uses the CommunityModules argument codes; errors about a value or a - * file use {@link EC#GENERAL}, whose message TLC prints verbatim. An error that TLC raises itself while the + *

There is no fixed nesting limit. Deep values may cause a {@link StackOverflowError}. + * Increasing -Xss can allow deeper values. The module reports validation and file failures with + * {@link EvalException}, rather than Java exceptions that TLC would wrap as error 2154. + * A wrong argument type uses the CommunityModules argument codes. Errors about a value or a file use + * {@link EC#GENERAL}, whose message TLC prints verbatim. An error that TLC raises itself while the * encoder enumerates a value, such as {x \in Nat : x < 3}, still arrives wrapped. */ public final class CBOR { @@ -86,55 +87,35 @@ private CBOR() { private static final int TAG_SET = 258; /** * IANA tag 33000, "TLA+ function as an array of [argument, value] pairs", registered for this module on - * 2026-10-08, around the [x, f[x]] pairs of a function that is neither a sequence nor a record. CBOR.tla - * is the only other place that names it. + * 2026-10-08, around the [x, f[x]] pairs of a function that is neither a sequence nor a record. + * See docs/CBOR.md for the encoding. */ private static final int TAG_FUNCTION = 33000; - /** - * The deepest nesting of data items that the decoder reads, which bounds its recursion, so hostile input - * is an error instead of a stack overflow. The encoder refuses to write deeper, so it writes nothing the - * decoder rejects for its depth. A tag is a data item: a set takes two levels and the pairs of tag 33000 - * three. - */ - private static final int MAX_DEPTH = 512; - /** * Guards file reads and writes, not encoding, so that a read in one worker never sees half of * another worker's write to the same file. */ private static final Object FILES = new Object(); - /** How a function is written. TLC equates functions across Java classes, so only the domain decides. */ - private enum Shape { - /** DOMAIN f = 1..n for some n >= 0: an array. Includes the empty function and the empty record. */ - SEQUENCE, - /** A non-empty set of strings: a map keyed by text. */ - RECORD, - /** Anything else: tag 33000 around [x, f[x]] pairs. */ - PAIRS - } - - private static Shape shape(final Value[] domain) { - final boolean[] seen = new boolean[domain.length + 1]; - int indices = 0; - boolean strings = domain.length > 0; - for (final Value d : domain) { - strings &= d instanceof StringValue; - if (d instanceof IntValue) { - final int i = ((IntValue) d).val; - if (1 <= i && i <= domain.length && !seen[i]) { - seen[i] = true; - indices++; - } + /** Tuple conversion must precede record conversion, including for empty functions. */ + private static Value functionValue(final FcnRcdValue f) { + final Value tuple = f.toTuple(); + if (tuple != null) { + return tuple; + } + // toRcd normalizes before checking types, which rejects incomparable domains. + for (final Value key : f.getDomainAsValues()) { + if (!(key instanceof StringValue)) { + return f; } } - return indices == domain.length ? Shape.SEQUENCE : strings ? Shape.RECORD : Shape.PAIRS; + return f.toRcd(); } @TLAPlusOperator(identifier = "ToCBOR", module = "CBOR", warn = false) public static TupleValue toCBOR(final Value value) { - final byte[] bytes = Encoder.encode(value, "ToCBOR", 1); + final byte[] bytes = Encoder.encode(value, "ToCBOR"); final Value[] elems = new Value[bytes.length]; for (int i = 0; i < elems.length; i++) { elems[i] = IntValue.gen(bytes[i] & 0xff); @@ -177,7 +158,7 @@ public static BoolValue serialize(final Value absoluteFilename, final Value valu new String[] { "first", "CBORSerialize", "string", Values.ppr(absoluteFilename.toString()) }); } final String file = ((StringValue) absoluteFilename).val.toString(); - final byte[] bytes = Encoder.encode(value, "CBORSerialize", 1); + final byte[] bytes = Encoder.encode(value, "CBORSerialize"); synchronized (FILES) { try { final Path path = Paths.get(file); @@ -221,8 +202,8 @@ public static Value deserialize(final Value absoluteFilename) { /** * Writes the one encoding of a TLC value. Values that TLC considers equal produce identical bytes, * whatever their Java class and whatever order TLC interned their strings in, so the encoder sorts by - * encoded bytes and never consults TLC's normalized order. It never calls normalize() either, so it - * mutates nothing that other workers read. + * encoded bytes rather than relying on TLC's normalized order. TLC's record and lambda conversions + * may normalize their inputs in place. * *

Set elements and the keys of maps and pairs are the sort keys. Each is encoded once into its own * array, sorted, and copied into the parent. Map and pair values stream straight into the output. @@ -236,15 +217,13 @@ private Encoder(final String operator) { this.operator = operator; } - static byte[] encode(final Value v, final String operator, final int depth) { + static byte[] encode(final Value v, final String operator) { final Encoder e = new Encoder(operator); - e.value(v, depth); + e.value(v); return e.out.toByteArray(); } - /** depth is the level of the data item that v becomes, counted as the decoder counts it. */ - private void value(final Value v, final int depth) { - level(depth); + private void value(final Value v) { if (v instanceof IntValue) { integer(((IntValue) v).val); } else if (v instanceof BoolValue) { @@ -253,82 +232,72 @@ private void value(final Value v, final int depth) { text(((StringValue) v).val.toString()); } else if (v instanceof ModelValue) { head(TAG, TAG_MODEL_VALUE); - level(depth + 1); text(((ModelValue) v).val.toString()); } else if (v instanceof TupleValue) { - array(((TupleValue) v).elems, depth); - } else if (v instanceof RecordValue) { - // Not toFcnRcd(), which normalizes the record in place. - final RecordValue r = (RecordValue) v; - final Value[] names = new Value[r.names.length]; - for (int i = 0; i < names.length; i++) { - names[i] = new StringValue(r.names[i]); - } - function(names, r.values, depth); - } else if (v instanceof FcnRcdValue) { - final FcnRcdValue f = (FcnRcdValue) v; - function(f.getDomainAsValues(), f.values, depth); + array(((TupleValue) v).elems); + } else if (v instanceof RecordValue || v instanceof FcnRcdValue) { + function((FcnRcdValue) v.toFcnRcd()); } else if (v instanceof FcnLambdaValue) { // The domain, not the function: TLC prints a function's body as its source location. final Value domain = ((FcnLambdaValue) v).getDomain(); if (!domain.isFinite()) { throw cannotEncode("a function with the infinite domain", domain); } - value(v.toFcnRcd(), depth); + function((FcnRcdValue) v.toFcnRcd()); } else if (v instanceof EnumerableValue) { if (!v.isFinite()) { throw cannotEncode("an infinite set", v); } - set(((SetEnumValue) v.toSetEnum()).elems.toArray(), depth); + set(((SetEnumValue) v.toSetEnum()).elems.toArray()); } else { throw cannotEncode(v.getKindString(), v); } } - private void level(final int depth) { - if (depth > MAX_DEPTH) { - throw new EvalException(EC.GENERAL, - operator + " cannot encode a value nested more than " + MAX_DEPTH + " CBOR data items deep."); + private void function(final FcnRcdValue f) { + final Value form = functionValue(f); + if (form instanceof TupleValue) { + array(((TupleValue) form).elems); + return; } - } - - private void function(final Value[] domain, final Value[] values, final int depth) { - final Shape shape = shape(domain); - if (shape == Shape.SEQUENCE) { - final Value[] elems = new Value[domain.length]; + final boolean record = form instanceof RecordValue; + final Value[] domain, values; + if (record) { + final RecordValue r = (RecordValue) form; + domain = new Value[r.names.length]; for (int i = 0; i < domain.length; i++) { - elems[((IntValue) domain[i]).val - 1] = values[i]; + domain[i] = new StringValue(r.names[i]); } - array(elems, depth); - return; + values = r.values; + } else { + domain = f.getDomainAsValues(); + values = f.values; } - // A pair is an array inside the array inside the tag. - final int entry = shape == Shape.RECORD ? depth + 1 : depth + 3; - final byte[][] keys = encodeEach(domain, entry); + final byte[][] keys = encodeEach(domain); final Integer[] order = new Integer[keys.length]; for (int i = 0; i < order.length; i++) { order[i] = i; } Arrays.sort(order, (i, j) -> Arrays.compareUnsigned(keys[i], keys[j])); - if (shape == Shape.RECORD) { + if (record) { head(MAP, keys.length); } else { head(TAG, TAG_FUNCTION); head(ARRAY, keys.length); } for (final int i : order) { - if (shape == Shape.PAIRS) { + if (!record) { head(ARRAY, 2); } write(keys[i]); - value(values[i], entry); + value(values[i]); } } - private void array(final Value[] elems, final int depth) { + private void array(final Value[] elems) { head(ARRAY, elems.length); for (final Value e : elems) { - value(e, depth + 1); + value(e); } } @@ -336,9 +305,8 @@ private void array(final Value[] elems, final int depth) { * An unnormalized set may hold an element twice, possibly in two Java classes. Equal elements have * equal encodings, so dropping equal neighbours after sorting removes exactly TLC's duplicates. */ - private void set(final Value[] elems, final int depth) { - level(depth + 1); - final byte[][] items = encodeEach(elems, depth + 2); + private void set(final Value[] elems) { + final byte[][] items = encodeEach(elems); Arrays.sort(items, Arrays::compareUnsigned); int n = 0; for (final byte[] item : items) { @@ -353,10 +321,10 @@ private void set(final Value[] elems, final int depth) { } } - private byte[][] encodeEach(final Value[] values, final int depth) { + private byte[][] encodeEach(final Value[] values) { final byte[][] encoded = new byte[values.length][]; for (int i = 0; i < values.length; i++) { - encoded[i] = encode(values[i], operator, depth); + encoded[i] = encode(values[i], operator); } return encoded; } @@ -420,14 +388,13 @@ private EvalException cannotEncode(final String kind, final Value v) { } /** - * Reads one CBOR data item into a TLC value. Liberal about form, strict about meaning: it accepts set - * elements, map keys and pairs in any order, integers and lengths in any width, and maps with keys that - * are not strings. Encoders in other languages differ on exactly these by default, and none of them - * changes the TLA+ value. It rejects every item whose TLA+ meaning is missing, out of TLC's range, or - * ambiguous, and names the source and the byte offset of the item. + * Reads one CBOR data item into a TLC integer, boolean, string, sequence, set, record, function, + * or existing model value. It accepts non-minimal integer and length encodings, set elements, + * map keys, and tag 33000 function arguments in any order, and maps with non-string keys. It rejects duplicate + * elements and keys, values TLC cannot represent, and unknown model values, naming the byte offset. * - *

It never creates a model value. ModelValue.make at run time leaves ModelValue.mvs stale, and TLC - * reads model values back from its disk queues by index into mvs. + *

Known model values are reused, never created. ModelValue.make at run time leaves ModelValue.mvs + * stale, and TLC reads model values back from its disk queues by index into mvs. */ private static final class Decoder { @@ -444,16 +411,16 @@ private static final class Decoder { } Value document() { - final Value v = item(1); + final Value v = item(); if (pos != in.length) { throw error(pos, "there are bytes after the first CBOR data item"); } return v; } - private Value item(final int depth) { + private Value item() { final int start = pos; - final int ib = initial(depth); + final int ib = initial(); final int major = ib >>> 5; if (major == SIMPLE) { return simple(start, ib & 0x1f); @@ -468,18 +435,18 @@ private Value item(final int depth) { case TEXT: return new StringValue(text(start, arg)); case ARRAY: - return new TupleValue(items(count(start, arg, 1), depth + 1)); + return new TupleValue(items(count(start, arg, 1))); case MAP: final int n = count(start, arg, 2); final Value[] keys = new Value[n], values = new Value[n]; owed += 2 * n; for (int i = 0; i < n; i++) { - keys[i] = member(depth + 1); - values[i] = member(depth + 1); + keys[i] = member(); + values[i] = member(); } return function(start, keys, values); default: - return tagged(start, arg, depth); + return tagged(start, arg); } } @@ -496,42 +463,42 @@ private Value simple(final int start, final int ai) { case 25: case 26: case 27: - throw error(start, "a floating-point number has no TLA+ counterpart"); + throw error(start, "TLC cannot represent a floating-point number"); case 28: case 29: case 30: case 31: throw notWellFormed(start); default: - throw error(start, "a simple value has no TLA+ counterpart"); + throw error(start, "a CBOR simple value has no TLA+ counterpart"); } } - private Value tagged(final int start, final long tag, final int depth) { + private Value tagged(final int start, final long tag) { if (tag == TAG_MODEL_VALUE) { final int at = pos; - final int ib = initial(depth + 1); + final int ib = initial(); if (ib >>> 5 != TEXT) { throw error(start, "tag 39 must enclose a text string"); } return modelValue(start, text(at, argument(at, TEXT, ib & 0x1f))); } if (tag == TAG_SET) { - return set(start, items(arrayHead(start, depth + 1, "tag 258 must enclose an array"), depth + 2)); + return set(start, items(arrayHead(start, "tag 258 must enclose an array"))); } if (tag == TAG_FUNCTION) { final String complaint = "tag " + TAG_FUNCTION + " must enclose an array of [key, value] arrays"; - final int n = arrayHead(start, depth + 1, complaint); + final int n = arrayHead(start, complaint); final Value[] keys = new Value[n], values = new Value[n]; owed += n; for (int i = 0; i < n; i++) { owed--; - if (arrayHead(start, depth + 2, complaint) != 2) { + if (arrayHead(start, complaint) != 2) { throw error(start, complaint); } owed += 2; - keys[i] = member(depth + 3); - values[i] = member(depth + 3); + keys[i] = member(); + values[i] = member(); } return function(start, keys, values); } @@ -539,9 +506,9 @@ private Value tagged(final int start, final long tag, final int depth) { } /** The length of the array that must follow the tag at start. */ - private int arrayHead(final int start, final int depth, final String complaint) { + private int arrayHead(final int start, final String complaint) { final int at = pos; - final int ib = initial(depth); + final int ib = initial(); if (ib >>> 5 != ARRAY) { throw error(start, complaint); } @@ -550,30 +517,12 @@ private int arrayHead(final int start, final int depth, final String complaint) private Value function(final int start, final Value[] keys, final Value[] values) { final Integer[] order = distinct(start, keys, "key"); - final int n = keys.length; - switch (shape(keys)) { - case SEQUENCE: - final Value[] elems = new Value[n]; - for (int i = 0; i < n; i++) { - elems[((IntValue) keys[i]).val - 1] = values[i]; - } - return new TupleValue(elems); - case RECORD: - final UniqueString[] names = new UniqueString[n]; - final Value[] fields = new Value[n]; - for (int i = 0; i < n; i++) { - names[i] = ((StringValue) keys[order[i]]).val; - fields[i] = values[order[i]]; - } - return new RecordValue(names, fields, true); - default: - final Value[] domain = new Value[n], range = new Value[n]; - for (int i = 0; i < n; i++) { - domain[i] = keys[order[i]]; - range[i] = values[order[i]]; - } - return new FcnRcdValue(domain, range, true); + final Value[] domain = new Value[keys.length], range = new Value[keys.length]; + for (int i = 0; i < domain.length; i++) { + domain[i] = keys[order[i]]; + range[i] = values[order[i]]; } + return functionValue(new FcnRcdValue(domain, range, true)); } private Value set(final int start, final Value[] elems) { @@ -650,28 +599,25 @@ private ModelValue modelValue(final int start, final String name) { return mv; } - private Value[] items(final int n, final int depth) { + private Value[] items(final int n) { final Value[] items = new Value[n]; owed += n; for (int i = 0; i < n; i++) { - items[i] = member(depth); + items[i] = member(); } return items; } /** The next of the items that an array or a map has added to owed. */ - private Value member(final int depth) { + private Value member() { owed--; - return item(depth); + return item(); } - private int initial(final int depth) { + private int initial() { if (pos == in.length) { throw error(pos, "the input ends inside a CBOR data item"); } - if (depth > MAX_DEPTH) { - throw error(pos, "data items are nested more than " + MAX_DEPTH + " deep"); - } return in[pos++] & 0xff; } @@ -698,8 +644,8 @@ private long argument(final int start, final int major, final int ai) { /** * Checked before anything is allocated. The bytes owed to the enclosing arrays and maps are not - * available. Otherwise each of 512 nested arrays could claim the rest of the input, and the decoder - * would allocate 512 times the input's size instead of an amount in proportion to it. + * available. Otherwise each nested array could claim the rest of the input, and total allocation + * would grow with nesting depth instead of remaining proportional to the input size. */ private int count(final int start, final long n, final int minBytesPerItem) { if (n < 0 || n > (in.length - pos - owed) / minBytesPerItem) { diff --git a/tests/CBORTests.tla b/tests/CBORTests.tla index 3217aed..6e2600f 100644 --- a/tests/CBORTests.tla +++ b/tests/CBORTests.tla @@ -128,10 +128,6 @@ ASSUME LET bytes == <<\h85, \h60, \h61, \h61, \h62, \hc3, \hbc, \h66, \he6, \h97 /\ AssertEq(<>, <<"", "a">>) /\ AssertEq(<>, <<1, 2, 2>>) -\* The deepest nesting FromCBOR reads: 512 sequences, one inside the other. -ASSUME LET bytes == [i \in 1..512 |-> IF i < 512 THEN \h81 ELSE \h80] - IN AssertEq(ToCBOR(FromCBOR(bytes)), bytes) - \* The bytes of the integer 0 inside n values, one inside the other, that each start with wrap. \* A recursive operator cannot build values this deep: TLC's own evaluation overflows the stack. LOCAL CBORNested(wrap, n) == @@ -141,9 +137,8 @@ LOCAL CBORInRecord == <<\ha1, \h61, \h61>> LOCAL CBORInSet == <<\hd9, \h01, \h02, \h81>> LOCAL CBORInFcn == <<\hd9, \h80, \he8, \h81, \h82, \h00>> -\* The deepest values ToCBOR writes. A tag is a data item, so a set takes two of the 512 levels -\* and a function that uses tag 33000 three. -ASSUME \A d \in {<>, <>, <>, <>} : +\* Byte roundtrips beyond the former limits, without recursive value equality. +ASSUME \A d \in {<>, <>, <>, <>} : LET bytes == CBORNested(d[1], d[2]) IN AssertEq(ToCBOR(FromCBOR(bytes)), bytes) ----------------------------------------------------------------------------- @@ -157,9 +152,14 @@ ASSUME SameBytes("seq", << <<"a", "b">>, \* JsonDeserialize reads {} as a record without fields. ASSUME SameBytes("empty", << <<>>, [x \in {} |-> x], + [x \in 1..0 |-> x], + [x \in {}, y \in {1} |-> <>], JsonDeserialize("tests/CBORTests/empty-object.json") >>, <<\h80>>) +\* A materialized sequence domain need not arrive in index order. +ASSUME AssertEq(ToCBOR(3 :> 30 @@ 1 :> 10 @@ 2 :> 20), <<\h83, \h0a, \h14, \h18, \h1e>>) + ASSUME SameBytes("record", << [cbora |-> 2, cboraa |-> 3, cborzz |-> 1], "cbora" :> 2 @@ "cborzz" :> 1 @@ "cboraa" :> 3, [f \in {"cborzz", "cbora", "cboraa"} |-> @@ -188,6 +188,23 @@ ASSUME SameBytes("fcn-tuple", << (<<2, 1>> :> 3) @@ (<<1, 2>> :> 3), ----------------------------------------------------------------------------- +\* Encoding does not require TLC to compare heterogeneous elements or arguments. +ASSUME LET sets == <<{1, "a", 1}, {"a", 1}>> + IN \A i \in DOMAIN sets : + AssertEq(ToCBOR(sets[i]), <<\hd9, \h01, \h02, \h82, \h01, \h61, \h61>>) +ASSUME AssertEq(ToCBOR({{1, "a"}, {"a", 1}}), + <<\hd9, \h01, \h02, \h81, \hd9, \h01, \h02, \h82, \h01, \h61, \h61>>) +ASSUME LET functions == <<1 :> 10 @@ MV :> 20, MV :> 20 @@ 1 :> 10>> + IN \A i \in DOMAIN functions : + AssertEq(ToCBOR(functions[i]), + <<\hd9, \h80, \he8, \h82, \h82, \h01, \h0a, \h82, \hd8, \h27, \h6a, + \h4d, \h6f, \h64, \h65, \h6c, \h56, \h61, \h6c, \h75, \h65, \h14>>) + +\* The values stay aligned with negative arguments when byte order differs from TLC order. +ASSUME AssertEq(ToCBOR(-1 :> "m" @@ 10 :> "t" @@ 100 :> "h"), + <<\hd9, \h80, \he8, \h83, \h82, \h0a, \h61, \h74, + \h82, \h18, \h64, \h61, \h68, \h82, \h20, \h61, \h6d>>) + LOCAL RoundTrips(v) == AssertEq(FromCBOR(ToCBOR(v)), v) \* Re-encoding a decoded value gives the bytes it was decoded from. @@ -218,6 +235,13 @@ ASSUME \A f \in [{MV, 1} -> {MV, "s"}] : RoundTrips(f) /\ Stable(f) ASSUME RoundTrips(SUBSET SUBSET {1, 2}) /\ Stable(SUBSET SUBSET {1, 2}) ASSUME RoundTrips(DumpedTrace) /\ Stable(DumpedTrace) +\* Comparing function arguments must also compare their nested function domains correctly. +ASSUME LET f == ((0 :> 10 @@ 2 :> 20) :> 1) @@ ((2 :> 20 @@ 0 :> 11) :> 2) + decoded == FromCBOR(ToCBOR(f)) + IN /\ RoundTrips(f) /\ Stable(f) + /\ AssertEq(decoded[2 :> 20 @@ 0 :> 10], 1) + /\ AssertEq(decoded[0 :> 11 @@ 2 :> 20], 2) + \* Decoded values are marked normalized, so their order must be TLC's: TLC finds an \* element of a normalized set, and an argument of a normalized function with at \* least 32 entries, by bisection. @@ -298,13 +322,13 @@ ASSUME AssertError("FromCBOR: the input ends inside a CBOR data item at byte 1." \* The offset names the innermost offending item. ASSUME AssertError("FromCBOR: null has no TLA+ counterpart at byte 2.", FromCBOR(<<\h82, \h01, \hf6>>)) -ASSUME AssertError("FromCBOR: a floating-point number has no TLA+ counterpart at byte 0.", +ASSUME AssertError("FromCBOR: TLC cannot represent a floating-point number at byte 0.", FromCBOR(<<\hf9, \h3c, \h00>>)) ASSUME AssertError("FromCBOR: null has no TLA+ counterpart at byte 0.", FromCBOR(<<\hf6>>)) ASSUME AssertError("FromCBOR: undefined has no TLA+ counterpart at byte 0.", FromCBOR(<<\hf7>>)) -ASSUME AssertError("FromCBOR: a simple value has no TLA+ counterpart at byte 0.", +ASSUME AssertError("FromCBOR: a CBOR simple value has no TLA+ counterpart at byte 0.", FromCBOR(<<\hf0>>)) ASSUME AssertError("FromCBOR: a byte string has no TLA+ counterpart at byte 0.", FromCBOR(<<\h41, \h00>>)) @@ -358,8 +382,6 @@ ASSUME AssertError("FromCBOR: TLC cannot compare the keys 1 and \"a\" at byte 0. FromCBOR(<<\ha2, \h01, \h00, \h61, \h61, \h00>>)) ASSUME AssertError("FromCBOR: the model value p99 is not defined in the model at byte 0. Declare it in the .cfg or create it with TLCExt!TLCModelValue(\"p99\").", FromCBOR(<<\hd8, \h27, \h63, \h70, \h39, \h39>>)) -ASSUME AssertError("FromCBOR: data items are nested more than 512 deep at byte 512.", - FromCBOR([i \in 1..513 |-> IF i < 513 THEN \h81 ELSE \h80])) ASSUME AssertError("The argument of FromCBOR should be a sequence of integers in 0..255, but instead it is:\n42", FromCBOR(42)) @@ -377,19 +399,6 @@ ASSUME AssertError("ToCBOR cannot encode an infinite set:\nSUBSET Nat", ToCBOR(SUBSET Nat)) ASSUME AssertError("ToCBOR cannot encode a function with the infinite domain:\nNat", ToCBOR([x \in Nat |-> x])) -\* One level more than the deepest values: ToCBOR refuses what FromCBOR could not read back. -ASSUME AssertError("ToCBOR cannot encode a value nested more than 512 CBOR data items deep.", - ToCBOR(<>)) -ASSUME AssertError("ToCBOR cannot encode a value nested more than 512 CBOR data items deep.", - ToCBOR([a |-> FromCBOR(CBORNested(CBORInRecord, 511))])) -ASSUME AssertError("ToCBOR cannot encode a value nested more than 512 CBOR data items deep.", - ToCBOR({FromCBOR(CBORNested(CBORInSet, 255))})) -ASSUME AssertError("ToCBOR cannot encode a value nested more than 512 CBOR data items deep.", - ToCBOR(0 :> FromCBOR(CBORNested(CBORInFcn, 170)))) -ASSUME AssertError("FromCBOR: data items are nested more than 512 deep at byte 1024.", - FromCBOR(CBORNested(CBORInSet, 256))) -ASSUME AssertError("FromCBOR: data items are nested more than 512 deep at byte 1024.", - FromCBOR(CBORNested(CBORInFcn, 171))) \* SubSeq cuts U+1F600 in half, leaving an unpaired surrogate that UTF-8 cannot carry. ASSUME AssertError("ToCBOR cannot encode a string that contains an unpaired UTF-16 surrogate.", ToCBOR(SubSeq(FromCBOR(<<\h64, \hf0, \h9f, \h98, \h80>>), 1, 1)))