Skip to content

§3.2 binary encoding: two worked examples do not decode, and whether a shared tag carries an id is undecidable from the text #72

Description

@s-celles

Summary

Implementing §3.2 from scratch, I transcribed the section's worked byte sequences
into test vectors before writing any code. Two of the three do not decode, and a
third question — whether a tag with the sharing flag also carries an identifier
string — cannot be answered from the document, because the grammar and the prose
disagree.

Four of these look like editorial slips with obvious patches. The fifth is a
genuine ambiguity and is the reason I am filing.

Version: OpenMath 2.0, revision 3 (2019-07-01),
https://openmath.org/standard/om20-2019-07-01/omstd20.html.

I would be glad to submit a PR against omstd20.xml for items 1–4 if the
direction is agreed.


1. Figure 3.5 does not decode: an OpenMath 1 body under an OpenMath 2 header

Byte 1 is 0x58 = [24+64]. §3.2.4.2 says that tag selects the new
interpretation of the sharing flag: "This encoding is signaled by the shared
object tag [88]."

Bytes 41–44 then use the old interpretation, and the figure's own Meaning
column says so — it glosses 0x48 0x01 as "reference to second symbol seen
(arith1:plus)" and 0x45 0x00 as "reference to first variable seen (x)". Those
are §3.2.4.1 back-references.

Under the header the figure declares, 0x48 opens a symbol whose Content
Dictionary name is one byte long, and a decoder desynchronises at byte 42.

Suggested patch: replace bytes 1–3 (58 02 00) with the single byte 18.
Every one of the figure's own byte annotations is then correct, which is the
evidence that the body is what was meant and the header is the slip.

2. Figure 3.6, byte 27 should be 0x01

The Meaning column reads "to the second shared object", which is ordinal 1, but
the Hex column reads 00. As printed the figure decodes to

f(f(f(a,a), f(a,a)), f(a,a))

rather than to the object of Figure 3.1 it is captioned as encoding,

f(f(f(a,a), f(a,a)), f(f(a,a), f(a,a)))

The bytes are well formed, so nothing but the caption catches this — it is a
wrong answer rather than a parse failure, which makes it the more troublesome of
the two. An implementer checking a correct decoder against this figure would
"fix" the decoder to reproduce it.

Suggested patch: byte 27, 00 → 01.

3. Figure 3.3: string → [6+64] [n] bytes:n appears to be missing its id

I audited every alternative in Figure 3.3 carrying the +64 flag. There are 33.
31 carry an id: field. start → [24+64] [m] [n] object [25] is the
thirty-third and correctly has none, since §3.2.4.2 gives the flag a different
meaning there. That leaves exactly one shareable production without an
identifier:

[6+64]       [n]     bytes:n           ← no id
[6+64+128]   {n} {m} bytes:n  id:m     ← id

These are the short and long forms of the same thing.

Suggested patch: [6+64] [n] [m] bytes:n id:m, matching [4+64], which is
the byte-array row of identical shape.

4. Figure 3.3: string → [7+64] … bytes:n should be bytes:2n

Token 7 is the UTF-16 string, where n counts UTF-16 units and the payload is
2n bytes. Every other token-7 alternative says so — [7], [7+32], [7+128],
[7+32+128] and [7+64+128] — and [7+64] alone says bytes:n.

Suggested patch: [7+64] [n] [m] bytes:2n id:m.

5. The question: does a tag with the sharing flag carry an identifier?

This one has no obvious patch, and it is what I could not resolve.

For — Figure 3.3, in 31 of its 32 shareable rows, and §3.2.2, which describes
it in prose and at length:

The symbol tag is followed by the length in bytes in the UTF-8 encoding of the
Content Dictionary name, the symbol name, and the id (if the shared bit was
set)
[…] These are followed by the bytes of the UTF-8 encoding of the Content
Dictionary name, the symbol name, and the id.

Against — Figure 3.6, whose byte 8 is 0x50 = [16+64] and whose byte 9 is
0x05, a variable tag, with no length and no identifier between them; and
§3.2.4.2 twice:

it indicates whether an object will be referenced later in the encoding.
This corresponds to the information, whether an id attribute is set in the
XML encoding.

Note that in the conversion from the XML to the binary encoding the identifiers
on the objects are not preserved.

and §3.2.5, which describes the reader's array purely positionally.

The two readings produce incompatible byte streams: a decoder written to the
grammar cannot read Figure 3.6, and a decoder written to Figure 3.6 cannot read a
stream that follows the grammar. There is no way to tell them apart on the wire,
because the byte after [16+64] is a length under one reading and a tag under
the other.

I have implemented the Figure 3.6 reading, on the sole ground that it is the only
one under which a byte sequence the standard prints decodes at all. That is a
tie-break, not a deduction, and I would rather follow whatever the intent was.

A related, smaller question

§3.2.4.2 says a reference names "the n+1th shared sub-object … counted in the
order they are generated in the encoding". That admits two readings, and only one
works: under start order, byte 24 of Figure 3.6 would reference the application
that encloses it, which §3.1.3.1 forbids. Under completion order the figure
decodes, and §3.2.5 agrees ("it is read and a pointer to the generated data
structure is stored at the next position"). It would help to say so explicitly.

6. The only base-256 example cannot detect the likeliest implementation error

Not a defect in the text, but a gap in its test coverage, and there is field
evidence for it.

Base 256 is the one base whose digits are bytes rather than characters — §3.2.2
says "as characters for bases 10 and 16 as in the XML encoding, and as bytes
for base 256". The obvious implementation slip is therefore to route the byte
case through the character path.

The standard gives exactly one base-256 example, and it is immune to that
slip:

0x02 0x04 0xab 0xFF 0xFF 0xFF 0xF1        (xfffffff1)

Every digit byte is ≥ 0x10, so an implementation that renders each byte as
hexadecimal without padding it to two characters still gets the right answer.
"ff"+"ff"+"ff"+"f1" is the same string either way.

This is not hypothetical. GAP's openmath package has that exact defect, it has
shipped since 2016, and it passes this example — which is very likely why it was
never noticed. Reported as
gap-packages/openmath#31,
where the full table of cases is.

Suggested addition: a second example containing a digit byte below 0x10,
which would fail immediately for that implementation. For instance

0x02 0x03 0xab 0xFF 0x01 0xFF             (16712191 = 0xff01ff)

The same argument applies to the base-256 example being the one revision 1
already had to correct: it is the least-exercised path in the section and it has
the fewest vectors.


Why this section in particular

§3.2 is the encoding SCSCP puts on the wire, and it is the one encoding with no
schema: XML has Relax NG, JSON has the TypeScript definition of Appendix F, and a
binary stream can be checked only against prose and three figures. Two of those
three do not decode.

It has also gone unexercised. Of the implementations I could find, GAP's
openmath package writes [24] and rejects [24+64] outright, and the INRIA C
library that REDUCE, FriCAS, Axiom and OpenAxiom bind to predates OpenMath 2
entirely. So nothing I could find implements §3.2.4.2 in either direction,
which is a plausible reason the ambiguity in item 5 has not come up before — and
item 6 is the same phenomenon in miniature, where a path that is implemented
turns out to have one test vector that cannot fail.

A guess at how items 1, 3 and 4 arose

Comparing OpenMath 1.1 §4.2 with OpenMath 2 §3.2: in OpenMath 1 a +64 row was a
back-reference whose entire payload was one index byte.

OM 1.1, Figure 4.3
  variable → [5] [n] varname:n | [5+128] {n} varname:n | [5+64] [n]
  symbol   → [8] [n] [m] cdname:n symbname:m | … | [8+64] [n]
  string   → [6] [n] chars:n | [6+128] {n} chars:n
           | [7] [n] chars:2n | [7+128] {n} chars:2n | [7+64] [n]

In OpenMath 2 those rows had to become "the object itself, plus whatever marks it
as shared". Items 3 and 4 are what a partial edit of exactly those rows would
leave: [6+64] [n] bytes:n is the row with the ordinary payload restored and no
identifier, and [7+64] … bytes:n gained an identifier but kept the token-6
payload — OpenMath 1's [7+64] [n] had no payload to copy. Note also that
OpenMath 1's grammar has no [6+64] row at all, though §3.2.4.1 says 8-bit and
16-bit strings share separately, so that row was missing before it was wrong.

Figure 3.5 fits the same account: its body is valid OpenMath 1 and only its first
byte is OpenMath 2.

This is an account, not a finding.

Precedent

Revision 1 (July 2017) corrected two errors in this same section — the base-256
integer example, "the 0xab (base 256/positive) byte was omitted and 0xF1 had been
written 0xFI", and the float example, which "was wrong". Items 1–4 are the same
kind of thing, and item 6 concerns the very example revision 1 had to fix.


Disclosure: this report was prepared with AI assistance. Every byte sequence in
it was executed against a working decoder locally, and every quotation was taken
from the published text of the revision named above. Where something is a guess
rather than a check — the account of how the slips arose — it is labelled as one.

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions