Skip to content

lean: textual values, as a draft spec, the model, and parse vectors #785

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
lwshang wants to merge 4 commits into
base: rewrite
Choose a base branch
from
Draft

lean: textual values, as a draft spec, the model, and parse vectors #785

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
8032ada
lean: draft spec for textual values
lwshang Nov 10, 2026
e9ab8bb
lean: address review of the textual values draft
lwshang Nov 10, 2026
b80e2bf
lean: textual values, after the draft spec, as parse vectors
lwshang Nov 11, 2026
7be06d4
lean: check parameter names in annotated function types
lwshang Nov 11, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
47 changes: 34 additions & 13 deletions conformance/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,9 +1,10 @@
# `conformance/` — machine-readable Candid conformance suite

**Status: subtyping, coercion and decoding.** Vectors for the field-id hash, type-table
well-formedness, subtyping, coercion and decoding, generated by the Lean model, and a
runner that checks them against `candid` 0.10. The decoding assertions of
[test/](../test/) are vectors too. See [REWRITE.md](../REWRITE.md) for why this exists.
**Status: subtyping, coercion, decoding and textual values.** Vectors for the field-id
hash, type-table well-formedness, subtyping, coercion, decoding, and reading textual
values, generated by the Lean model, and a runner that checks them against `candid`
0.10. Every assertion of [test/](../test/) is a vector too. See
[REWRITE.md](../REWRITE.md) for why this exists.

```
vectors/ the suite: JSON, one vector per line
Expand Down Expand Up @@ -65,12 +66,12 @@ where each expectation is stated independently of the model and checked against

| File | Origin | |
|---|---|---|
| `handwritten.json` | written by hand | named for what each shows; can catch the model being wrong |
| `handwritten.json` | written by hand | named for what each shows; can catch the model being wrong. The `parse` vectors follow [lean/Spec/TextValues.md](../lean/Spec/TextValues.md) |
| `subtype-primitives.json` | generated | every primitive against every primitive |
| `subtype-small.json` | generated | every pair from a universe of small types, including recursive ones |
| `coerce-small.json` | generated | sample values of each type in that universe, coerced at every type in it |
| `decode-small.json` | generated | each of those samples encoded at its own type, and decoded at it |
| `test-did.json` | from `test/*.test.did` | each message an assertion there names, at its types |
| `test-did.json` | from `test/*.test.did` | each message an assertion there names, bytes or text, at its types |

The ways a message can be malformed are all in `handwritten.json`, with their bytes
written out by hand: an encoder produces only well-formed messages, and the model's
Expand Down Expand Up @@ -98,7 +99,9 @@ the source: [tools/test-did/](tools/test-did/) translates them into Lean with
{"id":"...","kind":"coerce","value":<value>,"from":<type>,"to":<type>,"expect":"reject"},
{"id":"...","kind":"decode","bytes":"4449444c...","types":<types>,"expect":{"values":[<value>, ...]}},
{"id":"...","kind":"decode","bytes":"4449444c...","types":<types>,"expect":"reject"},
{"id":"...","kind":"decode","bytes":"4449444c...","types":<types>,"expect":"costly"}
{"id":"...","kind":"decode","bytes":"4449444c...","types":<types>,"expect":"costly"},
{"id":"...","kind":"parse","text":"(opt 5)","types":<types>,"expect":{"values":[<value>, ...]}},
{"id":"...","kind":"parse","text":"(5)","types":<types>,"expect":"reject"}
]}
```

Expand Down Expand Up @@ -128,6 +131,10 @@ the format, so it changes in place.
(`spec/Candid.md`, "Resource limits"). A runner passes if the implementation decodes
the message or rejects it, and fails if it panics or aborts. How long it takes, and
what it allocates, is for a runner to bound as its environment would.
- **`parse`**: `text`, read as an argument sequence at `types`
([lean/Spec/TextValues.md](../lean/Spec/TextValues.md)), is the `values`, one per
type, or is rejected. `types` is as for `decode`, with no environment of type
definitions, so a type name in an annotation in the text is rejected.

A `<type>` is `{"table": [<entry>, ...], "root": <slot>}`. A `<slot>` is a primitive's
name (`"nat"`, `"principal"`, ...) or a table index (`3`). An `<entry>` is a composite,
Expand Down Expand Up @@ -197,7 +204,10 @@ compares the values while leaving their representation in `IDLValue` to 0.10. It
workspace, not a member of the root one.

A `decode` vector is asked through `IDLArgs::from_bytes_with_types`, and the result
compared by encoding, as for `coerce`. Where 0.10 cannot represent an expected value,
compared by encoding, as for `coerce`. A `parse` vector is asked the way `candid_parser`'s
own test runner reads text: `candid_parser::parse_idl_args`, then
`IDLArgs::annotate_types` with the parser's rules (`from_parser`). A panic is a
disagreement. Where 0.10 cannot represent an expected value,
that is reported as a disagreement rather than a broken vector: the question translated,
and the answer is what 0.10 cannot hold.

Expand Down Expand Up @@ -244,6 +254,18 @@ What the runners have found, recorded so that they outlive the run that found th
rules give: every type is a subtype of `reserved` and of every option. The model adds
only that a future type is a subtype of itself, which no decoder can be asked.

- **The model and 0.10 read every text in `test/` alike**, on both sides of `==`. The
model reads text by [lean/Spec/TextValues.md](../lean/Spec/TextValues.md), which
differs from 0.10 elsewhere, in its Appendix B.2; the `parse` vectors there are
0.10's known divergences.
- **`candid_parser` 0.10 panics on some text.** `0X10` passes its lexer, which then
strips only `0x` and unwraps the failed parse. `IDLArgs::annotate_types` slices
`types[args.len()..]`, so `(1, 2)` at `(nat)` panics, in the path its own test runner
takes. And a positional field after id 4294967295 overflows `id + 1`, a panic in a
debug build and id 0 in a release one. Vectors: `text: the hexadecimal prefix is
lowercase (3.4)`, `text: an argument beyond the types is ignored (5.9)`, `text: a
positional field after the last id (4.2)`.

### Still to come

- **Encoding**, against the relation rather than fixed bytes. The binary format is
Expand All @@ -266,11 +288,10 @@ What the runners have found, recorded so that they outlive the run that found th
## Migration

All 471 existing assertions must exist as vectors and pass before
[test/](../test/) is deleted. 464 do, in `test-did.json`: the 17 in
`spacebomb.test.did` as `costly` vectors: they assert that a decoder with
self-metering rejects valid messages, and the spec leaves which ones to the
implementation. The other 7 have text on the left, which is a question for
the textual syntax, and wait on it.
[test/](../test/) is deleted. All 471 do, in `test-did.json`, and the model and 0.10
agree on every one. The 17 in `spacebomb.test.did` are `costly` vectors: they assert
that a decoder with self-metering rejects valid messages, and the spec leaves which
ones to the implementation. The 7 with text on the left are `parse` vectors.

For now the `.test.did` files stay the source, translated by
[tools/test-did/](tools/test-did/), so `candid_parser`'s own test suite and these
Expand Down
Loading
Loading