From ee8b120a734d6ef5f6c2988ee4cde52bb0cc49d5 Mon Sep 17 00:00:00 2001 From: younes-io Date: Tue, 13 Oct 2026 18:14:06 +0200 Subject: [PATCH 1/2] 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. README.md said Java 9 or higher and now says Java 11 or higher. [Build] Signed-off-by: younes-io --- README.md | 2 +- build.xml | 3 +-- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 71063b1..17938c2 100644 --- a/README.md +++ b/README.md @@ -41,7 +41,7 @@ appear in module `MTheorems.tla`, and proofs of these theorems can be found in ` How to use it ------------- -You must be running [Java 9 or higher](https://github.com/tlaplus/CommunityModules/issues/34#issuecomment-756571840). +You must be running Java 11 or higher. Just copy & paste the snippet, the operators, or the set of modules you are interested in. diff --git a/build.xml b/build.xml index ec19905..e98aed5 100644 --- a/build.xml +++ b/build.xml @@ -29,8 +29,7 @@ From 09448d58e4bb0fc25e10f4e56310aca1d13584c2 Mon Sep 17 00:00:00 2001 From: younes-io Date: Tue, 13 Oct 2026 18:14:36 +0200 Subject: [PATCH 2/2] Add the CBOR module ToCBOR returns the CBOR (RFC 8949) encoding of a finite TLA+ value as a sequence of integers in 0..255, and FromCBOR decodes such a sequence back into a TLA+ value. CBORSerialize and CBORDeserialize do the same through a file. Harnesses in Go, Rust, TypeScript and Python can then read TLC values without the type loss of JSON. Sets, model values and functions with non-string domains keep their TLA+ meaning. Sets use tag 258 and model values tag 39. A function with domain 1..n is an array, a function with a non-empty domain of strings is a map, and any other function uses tag 33000, which IANA registered on 2026-10-08 as "TLA+ function as an array of [argument, value] pairs". Equal values encode as identical bytes. The encoder picks a function's encoding 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. The decoder rejects duplicate set elements and keys, tags it does not know, and model values that the running TLC does not define. CBORTests holds each golden as inline hex literals and requires ToCBOR and FromCBOR to agree with them, and it tests every input the module refuses. CBORGoldenTest, run by ant test, checks the same goldens against a second encoder that shares no code with CBOR.java. https://github.com/tlaplus/tlaplus/issues/1467 [Feature] Signed-off-by: younes-io --- README.md | 1 + build.xml | 14 + modules/CBOR.tla | 64 ++ modules/tlc2/overrides/CBOR.java | 694 ++++++++++++++++++ modules/tlc2/overrides/TLCOverrides.java | 5 +- tests/AllTests.tla | 1 + tests/CBORTests.tla | 423 +++++++++++ tests/CBORTests/empty-object.json | 1 + tests/java/tlc2/overrides/CBORGoldenTest.java | 322 ++++++++ 9 files changed, 1523 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/java/tlc2/overrides/CBORGoldenTest.java diff --git a/README.md b/README.md index 17938c2..d3ebd5f 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 | 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/modules/CBOR.tla b/modules/CBOR.tla new file mode 100644 index 0000000..6f07cab --- /dev/null +++ b/modules/CBOR.tla @@ -0,0 +1,64 @@ +-------------------------------- MODULE CBOR -------------------------------- +(***************************************************************************) +(* 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. *) +(* Values must be finite and encodable: integers within TLC's range and *) +(* strings of valid Unicode. Set elements and function arguments must be *) +(* comparable by TLC for FromCBOR(ToCBOR(v)) = v to hold. Deep nesting *) +(* can exhaust the JVM stack, which a larger -Xss setting can relieve. *) +(***************************************************************************) + +LOCAL INSTANCE TLC + +(***************************************************************************) +(* The CBOR encoding of value as a sequence of integers in 0..255, one *) +(* per byte. Sets use tag 258, model values tag 39, and functions that *) +(* are neither sequences nor records tag 33000 (registered with IANA). *) +(* Equal values give identical bytes. TLC reports an error if value *) +(* cannot be encoded. *) +(***************************************************************************) +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. TLC reports an error for malformed input and for anything *) +(* it cannot represent, such as floats or a model value it does not know. *) +(***************************************************************************) +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. A *) +(* definition without parameters is constant-level, so TLC reuses its *) +(* value instead of reading the file again in each state. *) +(***************************************************************************) +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..8eb39c6 --- /dev/null +++ b/modules/tlc2/overrides/CBOR.java @@ -0,0 +1,694 @@ +/******************************************************************************* + * 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 documents the operators and 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. + */ +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. + */ + 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 reuses its value instead of reading the file again in each state. + */ + @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. + * + *

Representations, by TLA+ value: + *

    + *
  • an integer is a CBOR integer, and TRUE and FALSE are true and false; + *
  • a string is a UTF-8 text string, and a model value is tag 39 around its name; + *
  • a set is tag 258 around an array of its elements; + *
  • a function with domain 1..n, including sequences, tuples and the empty function, is an array; + *
  • a record, a function with a nonempty domain of strings, is a map; + *
  • any other function is tag 33000 around an array of [x, f[x]] arrays. + *
+ * The choice follows the function's domain, not how it was written, so a variable that holds a function + * can change representation from one state to the next. Integers, tags and lengths take their shortest + * form, and all lengths are definite. + * + *

Set elements, map keys and the arguments of tag 33000 are sorted by the unsigned bytes of their + * encodings, not by value: 10, 100 and -1 encode as 0a, 18 64 and 20, in that order. RFC 8949, section + * 4.2.1, orders map keys this way. RFC 7049, section 3.9, orders them by length first instead. + * + *

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 exactly one CBOR data item into TLC values. It reads back what the encoder writes, and also + * accepts integers, tags and lengths wider than necessary, set elements, map keys and tag 33000 + * arguments in any order, and maps with keys that are not strings. A map or tag 33000 function becomes a + * sequence, record or function by its domain, so encoding the result can give other bytes. + * + *

It rejects, naming the zero-based byte offset: + *

    + *
  • duplicate set elements or function arguments, as TLC compares them (01 and 18 01 are both 1), and + * elements or arguments that TLC cannot compare, such as 1 and "a"; + *
  • integers outside -2147483648..2147483647, floating-point numbers, byte strings, null, undefined and + * other simple values; + *
  • indefinite lengths, unsupported tags, truncated input, malformed CBOR or UTF-8, and bytes after + * the data item; + *
  • tag 39 without a text string, tag 258 without an array, and tag 33000 without an array of + * two-element arrays. + *
+ * + *

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)); + } +}