[Sequela02]

Slice 11a of stage 11 (#83): records, variants with fields and match, per syntax decisions 8 to 10. The conformance cases come in their own commit, before the compiler code.

What it adds

• record Name { field: Type, … }, built Name { field: value, … } with every field named, and read with value.field.
• Variants with fields, Below(limit: i64), built like a call. Labels are optional for one field and required for more.
• match value { | Pattern => result … } with decide's rows, in code and in specifications.
  • One field binds by position, more than one by label; _ binds nothing.
  • Every variant once, with no catch-all. A missing variant is an error that names it.
  • A binding can't hide a name in scope.
• == compares records and variants field by field.

Encoding. Records and variants are SMT-LIB datatypes, declared together. A match is a chain of tests on the variant, and each binding becomes the field it stands for, so an arm's arithmetic, calls and indexes carry obligations under that arm's test alone. The integers and lists inside a record or variant are assumed in range, as a parameter's are. Normalization names records R0 and fields x0 by position, so a rename changes no identity.

Decisions taken within the slice

• Receipt version 5. It adds a record type kind; a variant with fields is {"variant", "fields"}, and a record is an object of its fields. This follows stage 10's 3 → 4 bump.
• A pattern lists every field of its variant, with _ for the ones it doesn't need.
• List elements hold no integer or list, however deep, for the same reason lists of integers wait.
• Not yet allowed: recursive types, and structured data in a machine's state or parameters.
• accord build refuses records, variants with fields and match until 11g.
• Call results, open-case results and contract strength now assume the range facts of their type too, a list's length bound included. Scripts for some existing programs change, so the ledger re-proves them once. No conformance outcome changed.

Verification

• cargo fmt --all --check passes, and cargo clippy --workspace --all-targets --locked -- -D warnings is clean.
• cargo test --workspace --locked with the pinned solvers on Windows: all pass, and the 1 ignored test was already ignored.
• 25 new conformance cases:
  • 11 that check, 4 of them with planted faults. All 4 faults are refuted, with counterexamples replayed in source terms.
  • 14 rejections, each confirmed by hand to fail for the reason it states.
• New tests:
  • renaming a record, its fields or a binding changes no identity, while a field's type or order does;
  • record and variant counterexamples decode in the receipt;
  • accord build refuses structured data.

Not established:

• The scripts/check-*.sh integrations weren't run. The TypeScript cases still match their expected output byte for byte.
• No proof-time measurement.

Risk note

Mostly a two-way door: a language addition behind conformance cases. The one-way part is the receipt schema moving to version 5, which is unstable until the first release. Blast radius: existing programs' outcomes and TypeScript output are unchanged, and some ledger keys change. Evidence: the conformance suite and the test run above.

Refs #83