[lwshang]

Drafts the first section of a new Candid spec in lean/Spec/TextValues.md, covering the textual value syntax. It is a separate document rather than an edit to spec/Candid.md, and is meant as an example of how the new spec is organized and worded. It will become a Verso chapter later.

Until it replaces Candid.md under the conditions of REWRITE.md §6, Candid.md governs wherever the two disagree.

Shape

It follows RFC and Wasm-spec conventions:

• Status, abstract, and the BCP 14 paragraph on requirement keywords.
• Grammar in ABNF over Unicode scalar values, with case-sensitive strings.
• Two steps, as in Wasm's text format: parsing text into an expression (§3–4), then elaborating the expression at a type, e ⇐ t ⇝ v (§5).
• Sections on conformance and security considerations, and normative and informative references.
• Appendices: the textual form of principals (A), differences from Candid.md and candid 0.10 (B), and examples (C).

What it decides

Candid.md gives the value grammar but says only that types are "known from context", so the meaning of text at a type is new here. Most rules agree with candid 0.10, such as ignoring extra record fields and filling in missing optional fields and arguments. Appendix B.2 lists where they differ. Points for review:

• Annotations. (e : s) is accepted only where s is the same type as the expected one, which rejects (5 : nat) at int. The alternative, any subtype followed by coercion, is described in B.3.
• Literals. A float literal is rounded once, directly to the target width. A sign must be attached to its number. Underscores follow the grammar, and hex floats are accepted.
• Text literals cannot contain raw control characters.

The model

lean/Candid/Text/ implements the draft: a lexer, a parser into the document's abstract syntax, and elaboration, one function per rule. It also needed:

• type equivalence (Candid/Equiv.lean), for annotations. It reuses the subtype procedure's worklist and its termination measure.
• the textual form of principals (Candid/Principal.lean): CRC-32 and base32.
• float literals rounded once and exactly (Candid/Float.lean), deciding an extreme exponent like 1e999999999 before multiplying anything out.

Vectors

A new vector kind, parse: text, its types, and the values or a rejection.

• 86 hand-written vectors follow the document section by section, with expectations written from it.
• Every assertion of test/ is now checked. The 7 with text on the left are parse vectors, which completes the "all 471" condition for deleting test/. Text on the right of == is read by the model too, and the oracle checks that the model reads every text in test/ as candid_parser does. It does.
• The candid-0.10 runner asks parse vectors through candid_parser. It reports 14,465 agreeing, and 17 new known divergences, each a row of Appendix B.2.

Bugs found in candid 0.10 (not fixed here)

• annotate_types panics when there are more arguments than types: (1, 2) at (nat). This is the path candid_parser's own test runner takes.
• 0X10 panics, even in a release build.
• record { 4294967295 = 1; 2 } panics in a debug build. In a release build the second field silently gets id 0.
• The text lexer builds a String that may not be UTF-8 before checking it.

🤖 Generated with Claude Code

[Copilot]

🟡 Changes recommended

The specification cannot parse function-type annotations or hexadecimal labels as intended, and its text elaboration rule omits the UTF-8 decoding needed to produce Unicode scalar values.

4 open issues

• Add -> to punctuation tokens for function type annotations · New
• Parse numeric labels as single unsigned integer tokens · New
• Decode byte sequences as UTF-8 before producing text values · New
• Align the grammar and prose on C1 control character handling · New

What changed in this PR

Adds a standalone draft specification for Candid textual values, intended to become a Verso chapter. The existing spec/Candid.md remains authoritative until the replacement conditions are met.

Changes:

• Defines lexical syntax, expressions, and type-directed elaboration.
• Documents conformance, security considerations, and principal text encoding.
• Records differences from candid 0.10, open decisions, and examples; parser implementation and conformance vectors remain future work.

File	Description
lean/​Spec/​TextValues.md	Introduces the draft textual-value specification, compatibility notes, and examples.

_{Review effort: Balanced}

[Copilot]

🟡 Changes recommended

Function annotations still accept duplicate parameter/result names and invalid UTF-8 names because names are discarded without completing validation.

2 open issues

• Reject duplicate parameter and result names in annotations · New
• Propagate invalid UTF-8 parameter and result name errors · New

4 resolved since last review

• Decode byte sequences as UTF-8 before producing text values
• Parse numeric labels as single unsigned integer tokens
• Add -> to punctuation tokens for function type annotations
• Align the grammar and prose on C1 control character handling

1 file not reviewed

• conformance/vectors/handwritten.json: Generated file

_{Review effort: Balanced}

[Copilot]

🔵 Needs a closer look

Missing tests for floating-point rounding boundaries and recursive-type equivalence leave subnormal, tie, carry, and cycle-handling behavior unverified.

No open issues 🎉

2 previously missed issues

In code that hasn't changed since last review

Test recursive type equivalence and mismatching fields

lean/​Candid/​Equiv.lean:65

All current calls to decEquiv come through annotations, whose flattened type tables are acyclic trees. Consequently, the repeated-reference shortcut here is not exercised by the oracle, despite recursive-type equivalence being part of this procedure's contract. Please add direct checks for an equivalent one-node/two-node cycle and for recursive types with a mismatching nonrecursive field; these distinguish correct coinductive comparison from accepting a cycle before checking its remaining obligations.

Add rounding tests for subnormal and halfway boundaries

lean/​Candid/​Float.lean:51

The new rounding routine has no parse vectors for a nonzero subnormal, an exact halfway tie, or a carry from the largest subnormal to the smallest normal. The existing tiny-literal case only produces zero, and binary decoding vectors bypass this routine. Please add independent bit-pattern expectations for these boundaries in both formats—for example, 0x1p-149 and 0x1p-150 at float32, plus the corresponding float64 cases—so these rules are checked before their results become conformance expectations.

2 resolved since last review

• Propagate invalid UTF-8 parameter and result name errors
• Reject duplicate parameter and result names in annotations

1 file not reviewed

• conformance/vectors/handwritten.json: Generated file

_{Review effort: Balanced}