>] *)
+(* 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, *)
+(* or 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..0e12c46
--- /dev/null
+++ b/modules/tlc2/overrides/CBOR.java
@@ -0,0 +1,673 @@
+/*******************************************************************************
+ * 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.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;
+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;
+import util.Assert.TLCRuntimeException;
+
+/**
+ * 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 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 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.
+ *
+ *
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 {
+
+ private CBOR() {
+ }
+
+ // Major types, RFC 8949 section 3.1.
+ 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;
+ /** IANA tag 258, "Mathematical finite set", around the array of a set's elements. */
+ 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.
+ * See docs/CBOR.md for the encoding.
+ */
+ 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();
+
+ /** 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 f.toRcd();
+ }
+
+ @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);
+ }
+
+ /** 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.
+ */
+ @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;
+ }
+
+ /**
+ * 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
+ * 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.
+ */
+ 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 || 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);
+ }
+ function((FcnRcdValue) 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 FcnRcdValue f) {
+ final Value form = functionValue(f);
+ if (form instanceof TupleValue) {
+ array(((TupleValue) form).elems);
+ return;
+ }
+ 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++) {
+ domain[i] = new StringValue(r.names[i]);
+ }
+ values = r.values;
+ } else {
+ domain = f.getDomainAsValues();
+ values = f.values;
+ }
+ 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 (record) {
+ head(MAP, keys.length);
+ } else {
+ head(TAG, TAG_FUNCTION);
+ head(ARRAY, keys.length);
+ }
+ for (final int i : order) {
+ if (!record) {
+ 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()));
+ }
+ }
+
+ /**
+ * 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.
+ *
+ *
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 {
+
+ 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) {
+ this.in = in;
+ this.prefix = prefix;
+ }
+
+ Value document() {
+ 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 start = pos;
+ final int ib = initial();
+ 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)));
+ 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();
+ values[i] = member();
+ }
+ return function(start, keys, values);
+ default:
+ return tagged(start, arg);
+ }
+ }
+
+ 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, "TLC cannot represent a floating-point number");
+ case 28:
+ case 29:
+ case 30:
+ case 31:
+ throw notWellFormed(start);
+ default:
+ throw error(start, "a CBOR simple value has no TLA+ counterpart");
+ }
+ }
+
+ private Value tagged(final int start, final long tag) {
+ if (tag == TAG_MODEL_VALUE) {
+ final int at = pos;
+ 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, "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, complaint);
+ final Value[] keys = new Value[n], values = new Value[n];
+ owed += n;
+ for (int i = 0; i < n; i++) {
+ owed--;
+ if (arrayHead(start, complaint) != 2) {
+ throw error(start, complaint);
+ }
+ owed += 2;
+ keys[i] = member();
+ values[i] = member();
+ }
+ 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 String complaint) {
+ final int at = pos;
+ final int ib = initial();
+ 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 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) {
+ 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 Value[] items = new Value[n];
+ owed += n;
+ for (int i = 0; i < n; i++) {
+ items[i] = member();
+ }
+ return items;
+ }
+
+ /** The next of the items that an array or a map has added to owed. */
+ private Value member() {
+ owed--;
+ return item();
+ }
+
+ private int initial() {
+ if (pos == in.length) {
+ throw error(pos, "the input ends inside a CBOR data item");
+ }
+ 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. The bytes owed to the enclosing arrays and maps are not
+ * 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) {
+ 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/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..6e2600f
--- /dev/null
+++ b/tests/CBORTests.tla
@@ -0,0 +1,423 @@
+----------------------------- 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. 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. *)
+(***************************************************************************)
+
+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")
+
+\* 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)
+
+\* 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>>)
+\* 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>>)
+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>>)
+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 |-> {}]
+ 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>>)
+
+\* 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 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>>
+
+\* 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)
+
+-----------------------------------------------------------------------------
+
+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],
+ [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"} |->
+ 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>>)
+
+-----------------------------------------------------------------------------
+
+\* 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.
+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)
+
+\* 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.
+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)
+
+-----------------------------------------------------------------------------
+
+\* 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 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>>))
+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 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>>))
+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("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")
+
+=============================================================================
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/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));
+ }
+}