Add a CBOR module that reads and writes TLA+ values

[younes-io]

Why

tlaplus/tlaplus#1467 asks for a trace format that harnesses in Rust, Go, TypeScript, and Python can read without losing TLA+ types. JSON cannot tell a set from a sequence, a model value from a string, or a function from a record. This PR adds a CBOR module (RFC 8949) with ToCBOR and FromCBOR for byte sequences and CBORSerialize and CBORDeserialize for files, implemented as TLC overrides in the style of Json. TLC's -dumpTrace can later be a thin layer on top of it.

What changed

• modules/CBOR.tla documents the encoding and tlc2.overrides.CBOR implements the four operators.
• tests/CBORTests.tla pins the bytes of every value kind, and tests/java/tlc2/overrides/CBORGoldenTest.java, a second encoder with no shared code, checks those bytes from ant test.
• The README lists the module.

The encoding

Integers, booleans, and strings are the CBOR types of the same name. A model value is tag 39 (Identifier) around its name. A set is tag 258 (Mathematical finite set) around an array of its elements. A function whose domain is 1..n is an array, which covers sequences, tuples, and the empty function. A function whose domain is a non-empty set of strings is a map, which covers records. Any other function is tag 33000 around an array of [argument, value] pairs.

Set elements, map keys, and pairs are sorted by their encoded bytes, as RFC 8949 section 4.2.1 specifies, so values that TLC considers equal are written as identical bytes whatever their Java class.

Why a new tag

Tags 39 and 258 were already registered with IANA. Tag 33000 was registered for this module on 2026-10-08. It is needed because a TLA+ function can have integers, model values, tuples, sets, or records as arguments, and a CBOR map with such keys does not survive every decoder. Go's fxamacker/cbor rejects a map whose key is an array, and a JavaScript object has only string keys. An array of pairs decodes in every language. Tag 259 does not help, because it marks a map and leaves the key problem in place.

No registered tag describes a function or map encoded as an array of pairs. The closest are 259 and 275, which tag maps, and 281, which tags Lisp cons cells. 33000 is in the First Come First Served range. A comment below holds the registration template as filed; the registry row is at https://www.iana.org/assignments/cbor-tags/cbor-tags.xhtml and the module header links to it.

Scope

• Every finite TLC value round-trips, provided TLC can compare the elements of each set and function domain in it. The header states the depth limit, 512 nested data items, which both directions enforce.
• The form of a function follows its domain, so one variable can be an array in one state and a map or tag 33000 in the next. A reader must accept all three. The header says so.
• Not in this PR: the -dumpTrace cbor option in TLC, and atomic file replacement, which Json does not do either.

Tradeoffs

Deciding the form by the value, not by TLC's Java class, is what makes equal values byte-identical. The cost is the shape change above. A typed reader needs a small custom decoder for functions. The alternative, writing by Java class, would make <<>> and the empty record differ on the wire while TLC says they are equal.

Impact on existing code

A new module. The only change to existing code registers the class in TLCOverrides.java. The build now states Java 11 as its floor, which it already needed: IOUtils uses Java 11 file APIs and the tla2tools.jar it downloads is built for Java 11. ant test runs one JUnit test before TLC.

Verification

• ant test passes. CBORTests.tla has 121 assumptions, among them 31 byte-exact goldens, round trips of exhaustive small value spaces, and 55 inputs that must be refused with an exact message.
• CBORGoldenTest agrees with every golden, and Python's cbor2 reads them as sets, lists, dicts, and tags as intended.
• A counterexample written from a POSTCONDITION decodes with cbor2 and with Go's fxamacker/cbor.
• Three mutants fail the suite: sorting signed bytes, dropping the encoder depth check, and letting a nested length claim bytes an enclosing array still needs.

[younes-io]

Proposed IANA registration for tag 33000

Tags from 32768 up are First Come First Served. IANA asks for the four-line template from RFC 8949 section 9.2 plus a URL that describes the semantics. Before I file it, here is what I would send, so that the number, the data item, and the wording can be agreed in this PR. The description text lives in a gist, https://gist.github.com/younes-io/8bbc63cffd4811f6aa2776c7301eb360, which I will keep in step with this thread; its current text is also below. The module header gets the registry link when the row appears.

Update 2026-10-08. The request went to IANA with the template below and both contacts.

Update 2026-10-09. IANA registered tag 33000 on 2026-10-08, with the template below as filed: https://www.iana.org/assignments/cbor-tags/cbor-tags.xhtml (row 33000, template https://www.iana.org/assignments/cbor-tags/template/33000). The module header and CBOR.java now point at the registry.

Template

Tag: 33000
Data Item: array
Semantics: TLA+ function as an array of [argument, value] pairs
Point of Contact: Younes Akhouayri, Markus Alexander Kuppe
Description of Semantics: https://gist.github.com/younes-io/8bbc63cffd4811f6aa2776c7301eb360

Description of semantics

A function in TLA+ is a finite table from arguments to values. Its arguments can be integers, strings, booleans, model values, tuples, sets, records, or other functions. CBOR maps allow such keys, but the native dictionaries of several host languages do not. Go cannot use an array as a map key, and a JavaScript object turns every key into a string. Tag 33000 therefore writes a function as an array of pairs, which every language reads.

The tagged data item is an array. Each element is an array of exactly two data items, the argument first and then the value at that argument.

• No two arguments are equal. A reader rejects a tagged item with a repeated argument.
• The pairs may appear in any order. A producer that wants a deterministic encoding sorts the pairs by the encoded bytes of their arguments, as RFC 8949 section 4.2.1 sorts map keys. The reference implementation writes that order and reads any.
• Arguments and values are any CBOR data items, including nested tag 33000 items.
• An empty array denotes the empty function. The reference implementation writes the empty function as a plain empty array (0x80) without this tag, and a reader accepts both.

The producer of this tag, the CBOR module of the TLA+ CommunityModules, writes a function as a plain CBOR array when its domain is 1..n (a sequence) and as a CBOR map when its domain is a non-empty set of text strings (a record). Tag 33000 covers every other domain. Related registered tags used by the same module are 39 (identifier, for model values) and 258 (mathematical finite set).

Examples. The function 0 :> "x" @@ 1 :> "y":

d9 80e8        tag 33000
   82          array of 2 pairs
      82 00 61 78    [0, "x"]
      82 01 61 79    [1, "y"]

The function on the tuples <<1, 2>> and <<2, 1>> that maps both to 3:

d9 80e8 82
   82 82 01 02 03    [[1, 2], 3]
   82 82 02 01 03    [[2, 1], 3]

Open points for reviewers

• The number. Settled: IANA assigned 33000 on 2026-10-08. Nothing else in the registry describes a pair list as a function or map.
• Pairs versus a map. Tag 259 marks a CBOR map with arbitrary keys. It would avoid a new registration, but the map underneath still fails in Go when a key is an array, and loses integer keys in JavaScript objects. That is why the module writes pairs.
• Point of contact. Settled: @lemmy agreed below, and both names are on the request.

[lemmy]

First reaction: Could the Python testing be adapted and merged into the current Java test suite?

[lemmy]

• Point of contact. It would be good to have a TLA+ Foundation maintainer on the registration as well, so that the contact outlives any single contributor. @lemmy, would you like to be listed alongside me? If so, tell me the name and email to use.

Yes (shared my email privately).

[younes-io]

IANA registered tag 33000 today. The row is live at https://www.iana.org/assignments/cbor-tags/cbor-tags.xhtml, with the semantics as proposed above and both of us as contacts. Thanks, @lemmy.

[lemmy]

A StackOverflowError is a perfectly acceptable failure mode, so there is no need to impose an arbitrary recursion-depth limit. Users can adjust the JVM's thread stack size using -Xss (e.g., -Xss4m) if needed.

[younes-io]

Removed the fixed depth limit and the depth tracking from both the encoder and decoder. Deep values can now reach the JVM stack limit. The docs mention StackOverflowError and adjusting -Xss.

[lemmy]

Consider using established TLA+ terminology, such as sequences/tuples, records, and functions. It's not immediately clear to me what “Pair” refers to or how it relates to these existing concepts.

[younes-io]

Removed the Shape enum, including PAIRS. The code now uses TLC's sequence, record, and function conversions. The remaining mentions of pairs describe the [argument, value] entries in the CBOR encoding, not a separate TLA+ type.

[lemmy]

Consider using TLC's conversion methods on Value. Each returns null when the value isn't of that kind:

• v.toTuple() != null means v is a sequence. The domain is exactly 1..n, including the empty case.
• v.toRcd() != null means v is a record. The domain is a finite set of strings, including the empty case.
• v.toFcnRcd() != null means v is a function.

[younes-io]

Replaced the custom shape checks with toFcnRcd(), toTuple(), and toRcd(). Tuple conversion comes first so empty functions keep their existing array encoding.

I only try toRcd() when all domain elements are strings. It normalizes before checking their types, which can fail on mixed domains that the encoder otherwise accepts. The finite-domain check also stays before expanding a function.

[lemmy]

I suggest calling normalize() before writing, as Json does. TLC normalizes values in place everywhere, so avoiding it here doesn't buy much, and it adds subtle code: dodging toFcnRcd(), and removing duplicates from set elements by comparing their bytes. Once a set is normalized, its elements are already in a fixed order with no duplicates. Only record fields still need sorting by their encoded bytes, which RFC 8949, section 4.2.1 requires for CBOR maps.

[younes-io]

I removed the special handling that avoided toFcnRcd() and the claim that encoding never changes TLC values in place.

I kept byte sorting because TLC's order differs from this module's existing encoding order. For example, TLC orders the values as -1, 10, 100, while their encoded bytes sort as 10, 100, -1. Using TLC's order for sets and function arguments would change the output.

I also kept byte-based duplicate removal for sets. Normalizing every set would reject inputs such as {1, "a"}, which ToCBOR currently accepts. FromCBOR still rejects that mixed set, as documented.

[lemmy]

This paragraph should would benefit from using TLA+ terminology. Also, what other languages and why do they matter here?

[younes-io]

Rewrote this using the TLA+ types the decoder returns. The paragraph now states which input forms it accepts and rejects, without the vague reference to other languages.

[lemmy]

This should either be moved or clarified to state that Decoder handles MVs. It appears to look up and reuse existing MVs, failing if none exists. This is reasonable.

[younes-io]

Clarified this. The decoder handles model values by looking up and reusing existing ones. An unknown name causes an error. Decoding never creates a new model value.

[lemmy]

TLA+ does have Reals. The real limitation is TLC's, not the language's: TLC has no value class for non-integer reals.

"TLC cannot represent a floating-point number"

[younes-io]

Changed the message to "TLC cannot represent a floating-point number" and updated the test. The error now describes TLC's limitation, not a limitation of TLA+.

[lemmy]

"a CBOR simple value has..."?

[younes-io]

Changed it to "a CBOR simple value has no TLA+ counterpart" and updated the test.

[lemmy]

Should ToCBOR and FromCBOR be declared LOCAL? Apart from tests, under what circumstances would a spec need to call them directly?

[younes-io]

I've kept them public for specs that work with bytes without using files. For example, Len(ToCBOR(message)) can check an encoded message-size limit. FromCBOR(bytes) can interpret a byte sequence already available to the spec.

I don't have an existing non-test consumer to point to yet. These are the intended uses, and I've added examples to the documentation.

[lemmy]

This header comment seems overly technical and focused on implementation details. Consider moving it elsewhere or replacing it with a high-level description aimed at users of the CBOR module, who presumably don't need to know the internals of TLA+ serialization and deserialization.

[younes-io]

Shortened the header to explain how to use the operators, with examples and the main limitations. Moved the encoding rules and interoperability details to docs/CBOR.md, with references from the module and README.