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 four public operators and the encoding. tlc2.overrides.CBOR implements them, and the Javadoc of its Encoder and Decoder states the exact rules for writing and reading.
• 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.

Map keys use the unsigned lexicographic encoded-byte ordering in RFC 8949 section 4.2.1. This module also applies that ordering to set elements and function arguments. That additional contract gives supported TLC-equal values identical bytes regardless of their Java representation or string interning order.

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 avoids requiring function arguments to fit a host language's native map keys. Consumers still need to interpret the tags. Tag 259 does not help, because it marks a map and leaves the key problem in place.

Before this registration, no registered tag described 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.

Scope

• Supported finite values round-trip when TLC can enumerate their sets and function domains and compare the elements within each. Strings must be valid Unicode, integers must fit TLC's range, and decoded model values must already be known to TLC.
• There is no fixed nesting limit. Deep values can cause StackOverflowError; increasing JVM -Xss can allow deeper values.
• ToCBOR can export mixed sets such as {1, "a"}, but FromCBOR rejects them because TLC cannot compare their elements. The header of CBOR.tla states this round-trip restriction.
• 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 of arbitrary functions must accept all three forms.
• 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

The new module is registered in TLCOverrides.java and included in AllTests.tla. A separate first commit makes the build and the README state Java 11 as the floor, which the build 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 on the current source. The build downloaded the v1.8.0 tla2tools.jar, which reports version 2026.10.13.011403, revision 210df3a, and ran on Homebrew Java 17.0.20.1 on macOS. This run does not cover the other CI platforms.
• CBORTests.tla contains 119 assumptions covering byte-exact encodings, equivalent TLC representations, round trips over exhaustive small value spaces, malformed-input rejection, file operations, and nesting beyond the former fixed limits.
• CBORGoldenTest passes all 31 golden cases using a second encoder with no shared implementation code. It runs before TLC in ant test.
• Earlier revisions were checked with Python's cbor2 and Go's fxamacker/cbor, including a counterexample written from a POSTCONDITION. Those interoperability checks have not been rerun for the latest revision.
• Earlier mutation checks covered unsigned byte ordering and nested-length allocation accounting. They have not been rerun for the latest revision. The former depth-check mutation is no longer applicable because the fixed limit was removed.

[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]

LGTM (this is ready (modulo readme file) to be experimented with more broadly).

[younes-io]

@lemmy btw, I don't see the merge button

[Copilot]

🟡 Changes recommended

The promised encoding specification is missing, and the documented Java requirement conflicts with the new Java 11 build target.

2 open findings

• Update runtime documentation for the new Java 11 requirement · New
• Add the missing CBOR encoding contract documentation · New

1 resolved since last review

• Use Java 8-compatible unsigned byte-array comparison

🧠 Review effort: Balanced

[lemmy]

LGTM