spec: `service` <: `principal` + release candid 0.10.32 by ggreif · Pull Request #748 · dfinity/candid

ggreif · 2026-07-02T16:09:36Z

Summary

A service reference is represented by the principal of its canister, so it is natural to use one wherever a principal is expected. This adds the subtyping rule service <actortype> <: principal and its coercion. Long discussed in caffeinelabs/motoko#2264 (rossberg, chenyan-dfinity, and nomeata converged on it being reasonable at the Candid level).

This PR also cuts the corresponding candid 0.10.32 release (see Release below).

Spec (`spec/Candid.md`)

Modelled exactly on the existing nat <: int rule — an unconditional, premise-free widening in the Primitive Types subsections (principal is itself primitive), with a value-preserving coercion:

subtyping: service <actortype> <: principal
coercion: service <text> : service <actortype> ~> principal <text> : principal

It is a conservative extension: it only enlarges <: (no existing judgment is lost), and it is decode-sound because a service reference is already wire-encoded exactly like a principal — M/R are byte-identical (i8(0) opaque; i8(1) M(v* : vec nat8) transparent) — so the coercion is the identity on the reference. No change to the binary format (T/M/R). The reverse (principal <: service) is intentionally not added.

Reference implementation (`rust/candid`)

types/subtype.rs: (Service(_), Principal) accepted in both matchers, unconditional (like (Nat, Int)).
de.rs: deserialize_principal now matches the wire type directly against principal or service <…> (instead of asserting wire == principal), so a service reference decodes at principal (identical PrincipalBytes). It deliberately does not use the general check_subtype(), which would also admit empty (bottom) <: principal and let a payload be decoded as a principal from arbitrary trailing bytes.

Tests

test/subtypes.test.did: service {} and service {m:()->()} <: principal; principal </: service {}.
test/reference.test.did: a service reference value decodes at principal (empty & non-empty); the reverse was already rejected.

Both were confirmed to fail without the corresponding checker/decoder change.

Metatheory (`coq/`)

MiniCandid.v: extended with ServiceT/PrincipalT + ServiceV/PrincipalV, the rule ServiceT <: PrincipalT (modelled on NatT <: IntT), and the coercion. soundness and transitive_coherence re-verify with the new constructors — the rule is machine-checked sound.
Build: re-pinned coq/nix to a modern nixpkgs that provides coq_8_18 (the nixos-20.09 niv pin no longer evaluates; the default coq is now Rocq 9.x, which renamed Coq.*→Stdlib.* and moved FunInd). Removed the now-unused niv machinery (sources.{nix,json}) and pinned the fetchTarball NAR hash. nix-build -A theories coq is green in CI.

Release (`candid` / `candid_derive` 0.10.32)

This PR also cuts the candid release that carries the change:

Bump candid and candid_derive 0.10.31 → 0.10.32 (kept in lockstep per the "sync with the version" comments) and the internal candid_derive dependency pin; refresh the workspace and rust/bench lockfiles.
CHANGELOG.md: new dated section documenting service <: principal as a non-breaking change.

Follow-ups (not in this PR)

Porting the Coq development to Rocq 9.1.1 (separate issue).

A service reference is represented by the principal of its canister, so every service type is a subtype of `principal` (and a service reference coerces at `principal`). Modelled exactly on `nat <: int`: an unconditional, premise-free widening in the Primitive Types subsections, with a value-preserving coercion. The wire encoding is unchanged — `M`/`R` for `service <actortype>` and `principal` are already byte-identical (`i8(0)` opaque; `i8(1) M(v* : vec nat8)` transparent), so the coercion is the identity on the reference. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Implements the spec rule `service <actortype> <: principal` in both subtype matchers (`subtype_collect_` and the `subtype_` probe): a service type is unconditionally a subtype of `principal`, mirroring `Nat <: Int`. Tests (test/subtypes.test.did): `service {}` and `service {m:()->()}` decode where a `principal` reference is expected; `principal` does NOT decode where a `service {}` is expected (one-directional). Verified the positive cases fail without the checker change. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

…pal) `deserialize_principal` hard-asserted `wire_type == Principal`, rejecting a service reference on the wire even though `service <: principal`. Since it is dispatched only when the expected type is `principal`, replace that assertion with `check_subtype()` (as `deserialize_service`/`deserialize_function` already do): it admits `principal` (reflexive) and `service <actortype>` wire types, both read as the same `PrincipalBytes`, so a service reference decodes as its principal. Tests (test/reference.test.did): an empty and a non-empty service reference value decode at type `principal`. Verified they fail without this change; the reverse (a principal at `service {}`) was already rejected. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

The niv pin (nixos-20.09) no longer evaluates on current nix, and the default `coq` is now Rocq 9.x, which renamed the stdlib namespace (Coq.* -> Stdlib.*) and relocated FunInd — both used by these proofs. Pin nixpkgs to a modern revision and build with coq_8_18 (the newest coq that accepts the proofs unchanged); drop the dead niv/stdenv.lib bits. `nix-build -A theories coq` is green again. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Extend the model with leaf types ServiceT/PrincipalT and reference values ServiceV/PrincipalV, the subtyping rule `ServiceT <: PrincipalT` (modelled exactly on `NatT <: IntT` — unconditional, coercion-preserving), and the matching `coerce` cases. Re-establish every downstream proof with the new constructors: coerce_constituent_eq, the coerce_nice_ind induction principle (new hypotheses + serviceHT/principalHT cases), and UpToNull. soundness and transitive_coherence go through unchanged in shape, so the new rule is machine-checked sound. Verified with coq_8_18. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Copilot

Pull request overview

Adds the Candid subtyping/coercion rule service <actortype> <: principal, aligning the spec, Rust reference implementation, Coq metatheory, and tests so that service references can be used wherever a principal is expected (without changing the wire format).

Changes:

Specify service <actortype> <: principal and the corresponding identity coercion in spec/Candid.md.
Update Rust subtype checking and decoding so principal can decode wire-typed service <…> references.
Extend tests (DID subtyping + reference decoding) and update Coq formalization + Nix pinning for Coq 8.18.

Reviewed changes

Copilot reviewed 8 out of 8 changed files in this pull request and generated 2 comments.

Show a summary per file

File	Description
test/subtypes.test.did	Adds subtype assertions covering `service {} <: principal` and the non-reverse.
test/reference.test.did	Adds decoding assertions that a service reference value can decode as `principal`.
spec/Candid.md	Documents the new subtyping rule and identity coercion for service→principal.
rust/candid/src/types/subtype.rs	Implements unconditional `Service(_) <: Principal` in the subtype checker.
rust/candid/src/de.rs	Adjusts `principal` deserialization to admit service-typed wire values.
coq/nix/default.nix	Re-pins nixpkgs to obtain `coq_8_18` for proof compatibility.
coq/MiniCandid.v	Extends the metatheory with `ServiceT`/`PrincipalT`, subtyping, and coercions.
CHANGELOG.md	Notes the new non-breaking decoding/subtyping behavior.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Co-authored-by: mraszyk <31483726+mraszyk@users.noreply.github.com>

Review dismissed by automation script.

Address code-review feedback on the `service <: principal` decode path: - deserialize_principal: match the wire type directly against `principal` (reflexive) or `service <...>` instead of the general check_subtype(). check_subtype also admits `empty` (bottom) <: principal, which would let a payload declare wire type `empty` yet be decoded as a principal from arbitrary trailing bytes. The direct match is tighter and avoids the subtype-check overhead on this common decode path. - reference.test.did: add a negative test asserting `empty` (bottom) is rejected as a wire type for `principal`. Tests: candid_parser reference suite + candid crate suite pass.

zeropath-ai · 2026-07-03T09:05:29Z

✅ No security or compliance issues detected. Reviewed everything up to 85d9527.

Security Overview

🔎 Scanned files: 14 changed file(s)
🔗 Scan Link: https://zeropath.com/app/repositories/7ddf29dd-76dc-4f78-adfa-47ac8f4643e7?scanId=8c7dc001-a025-45c6-a321-17cdd2f8eef3&codeScanTypes=PrScan&tab=issues

Detected Code Changes

Change Type	Relevant files
Enhancement	► coq/MiniCandid.v Add ServiceT and PrincipalT in type definitions ► coq/MiniCandid.v Add ServiceV and PrincipalV variants ► coq/MiniCandid.v Extend HasType with ServiceHT and PrincipalHT ► coq/MiniCandid.v Extend Subtype with ServicePrincipalST
Enhancement	► coq/nix/default.nix Pin and configure Nix/Nixpkgs for Coq 8.18 compatibility ► coq/nix/default.nix Use coq_8_18 and related OCaml tooling ► coq/nix/default.nix Remove obsolete sources.nix/sources.json references
Enhancement	► rust/candid/src/de.rs Decoding path accepts both Principal and Service wire types for principal coercion
Enhancement	► rust/candid/src/types/subtype.rs Treat Service(_), Principal as subtype relationship; Service <: Principal
Enhancement	► rust/candid_derive/Cargo.toml Bump version to 0.10.32
Enhancement	► rust/candid/Cargo.toml Bump candid version to 0.10.32 and update candid_derive path/version
Enhancement	► spec/Candid.md Document service <: principal coercion and related rules
Enhancement	► test/reference.test.did Add tests for service <: principal decoding and related principal wiring behavior
Enhancement	► test/subtypes.test.did Add tests asserting service references are subtypes of principal

Copilot

Pull request overview

Copilot reviewed 8 out of 8 changed files in this pull request and generated 5 comments.

ggreif · 2026-07-03T09:41:14Z

Adversarial review — subtyping soundness & wire-format

I ran an independent adversarial pass over this PR focused on IDL subtyping soundness, wire-format equivalence, decoder correctness, and spec ⇄ impl ⇄ Coq consistency (read the spec/checker/decoder/Coq proof, built the Coq proofs, ran both Rust suites).

Verdict: sound — no real defects found. 3 minor, non-blocking observations.

Checked and OK

Subtyping soundness (rust/candid/src/types/subtype.rs): reflexivity via the t1 == t2 short-circuit; the new unconditional (Service(_), Principal) rule mirrors (Nat, Int); transitivity opens no unsound chain — nothing new is <: service except empty (which already was <: principal), and there is no (Principal, X) rule beyond the generic reserved/opt ones, so no A <: service <: principal <: B admits anything new. Reverse principal <: service correctly falls through to the catch-all Err. Func variance is correct (contravariant args / covariant results), and opt interactions are standard candid behavior, not new holes.
Wire-format equivalence is real: both a principal value and a service value encode as PrincipalBytes (flag | leb128 len | bytes); deserialize_principal and deserialize_service both call PrincipalBytes::read. Service methods live only in the type table, never in the value stream — so the coercion is genuinely the identity on value bytes.
Decoder (rust/candid/src/de.rs): deserialize_principal is reached only when expect_type == Principal, so the direct matches!(wire, Principal | Service(_)) gate protects both the value-level and typed decode paths. Excluding empty (bottom) is correct and necessary — the earlier check_subtype()-based version admitted empty <: principal and would then read attacker-controlled trailing bytes as a principal (a real type-confusion / trailing-bytes vector); the direct match closes it, with a regression test in test/reference.test.did. Recursive / Var / Knot service types resolve to the structural Service(_) head via unroll_type (with a depth guard), and reserved/opt/func/record/vec wire types at principal all correctly fail the check.
Spec ⇄ impl ⇄ Coq consistency: all three model service <: principal (not a weaker/stronger rule). coq/MiniCandid.v encodes the value-level identity coercion (ServiceV r … => PrincipalV r); the Coq proofs build cleanly and subtyping_refl/subtyping_trans still go through with the new constructor.
Tests: cargo test -p candid (93 passed) and cargo test -p candid_parser --test test_suite (6 passed); Coq builds.

Minor observations (all optional, none block merge)

Cost accounting (de.rs, principal path): dropping check_subtype() also dropped its add_cost(self.table.0.len()) charge. This is not a soundness or DoS issue (the path still charges max(30, len)). Arguably it's more correct to charge less now that no subtype traversal is performed; flagging only for awareness if exact per-reference-type quota parity is desired.
Coq scope note: MiniCandid.v models ServiceT/PrincipalT as opaque leaves, so the mechanization proves the reference coercion but abstracts away service method-set depth-subtyping. That's fine for this rule (which ignores methods); the Rust code handles method-set subtyping correctly regardless.
Test-gaps (defense-in-depth): no explicit recursive-service-at-principal decode test, no func/record/opt wire-type-at-principal rejection test, and no transitivity-through-a-Var-alias-to-service test. The logic is sound by inspection; these would just lock it in.

Adversarial review performed with an AI review agent (Claude Code); findings verified against the source.

Defense-in-depth cases from adversarial review (behavior already verified by reasoning; these lock it in): reference.test.did (decode): - recursive service value (method returns the service) decodes at `principal` - `func`, `record`, `opt` wire types are rejected at `principal` (only `principal`/`service` share the PrincipalBytes encoding) subtypes.test.did (subtype check): - a recursive (µ) service type is <: principal (Var-alias chain resolves to the service head) All pass: candid_parser test_suite 6/6.

- CHANGELOG.md, spec/Candid.md: strip stray trailing CR introduced by the GitHub-UI "Apply suggestions" commit; normalize to LF-only. - de.rs: use the terse "principal" message in the principal-path check!, matching the deserializer's convention (e.g. "nat", "blob") rather than a sentence. (PR description bullet for deserialize_principal updated separately to reflect the direct wire-type match instead of check_subtype(). Spec line 759 prose left as-is: it mirrors the existing `nat <: int` phrasing at line 751.) candid_parser test_suite 6/6.

Copilot

Pull request overview

Copilot reviewed 8 out of 8 changed files in this pull request and generated no new comments.

Review dismissed by automation script.

The CHANGELOG announced Candid 0.10.32 but the crate versions were never bumped, so `cargo publish` would have shipped this change as 0.10.31. - Move the 0.10.32 entry to a new dated section at the top of the CHANGELOG (matching the one-release-per-dated-section convention). - Bump `candid` and `candid_derive` to 0.10.32 (kept in lockstep per the "sync with the version" comments) and the internal dependency pin. - Refresh the workspace and bench lockfiles. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

`coq/nix/default.nix` was re-pinned to fetch nixpkgs directly and no longer imports `./sources.nix`, leaving the niv machinery (`sources.nix`, `sources.json`) as dead files. Remove them so the `fetchTarball` pin in `default.nix` is the single authoritative source. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

The re-pinned nixpkgs `fetchTarball` specified a sha256 that did not match the archive's actual unpacked (NAR) hash, so `nix-build -A theories coq` failed on a clean checkout with a hash mismatch. A local build passed only because `fetchTarball` served a TTL-cached copy that bypassed the check. Pin the hash CI computed for nixpkgs@e8273b29fe1390ec8d4603f2477357555291432e. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

cla-idx-bot Bot added the external-contributor label Jul 2, 2026

ggreif changed the title ~~spec: service <: principal~~ spec: service <: principal Jul 2, 2026

ggreif and others added 6 commits July 2, 2026 18:19

docs: changelog for service <: principal (Candid 0.10.32)

7343360

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

ggreif force-pushed the gabor/a-sub-p branch from 9b8f627 to 7343360 Compare July 2, 2026 16:20

mraszyk requested a review from Copilot July 3, 2026 05:41

Copilot started reviewing on behalf of mraszyk July 3, 2026 05:42 View session

Copilot AI reviewed Jul 3, 2026

View reviewed changes

Comment thread rust/candid/src/de.rs Outdated

Comment thread test/reference.test.did

mraszyk reviewed Jul 3, 2026

View reviewed changes

Comment thread spec/Candid.md Outdated

mraszyk reviewed Jul 3, 2026

View reviewed changes

Comment thread CHANGELOG.md Outdated

mraszyk previously approved these changes Jul 3, 2026

View reviewed changes

Apply suggestions from code review

0f07e9c

Co-authored-by: mraszyk <31483726+mraszyk@users.noreply.github.com>

ggreif marked this pull request as ready for review July 3, 2026 09:05

ggreif requested a review from a team as a code owner July 3, 2026 09:05

ggreif requested review from Copilot and mraszyk July 3, 2026 09:05

Copilot started reviewing on behalf of ggreif July 3, 2026 09:05 View session

Copilot AI reviewed Jul 3, 2026

View reviewed changes

Comment thread spec/Candid.md

Comment thread spec/Candid.md Outdated

Comment thread rust/candid/src/de.rs

Comment thread rust/candid/src/de.rs

Comment thread CHANGELOG.md Outdated

ggreif added 2 commits July 3, 2026 11:53

ggreif requested a review from Copilot July 3, 2026 10:25

Copilot started reviewing on behalf of ggreif July 3, 2026 10:26 View session

Copilot AI reviewed Jul 3, 2026

View reviewed changes

mraszyk previously approved these changes Jul 3, 2026

View reviewed changes

Merge branch 'master' into gabor/a-sub-p

253b138

lwshang and others added 3 commits July 6, 2026 09:52

lwshang changed the title ~~spec: service <: principal~~ spec: service <: principal + release candid 0.10.32 Jul 6, 2026

lwshang approved these changes Jul 6, 2026

View reviewed changes

lwshang merged commit d24fb18 into dfinity:master Jul 6, 2026
16 of 17 checks passed

ggreif deleted the gabor/a-sub-p branch July 6, 2026 14:47

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

spec: `service` <: `principal` + release candid 0.10.32#748

spec: `service` <: `principal` + release candid 0.10.32#748
lwshang merged 14 commits into
dfinity:masterfrom
ggreif:gabor/a-sub-p

ggreif commented Jul 2, 2026 •

edited by lwshang

Loading

Uh oh!

Copilot AI left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

zeropath-ai Bot commented Jul 3, 2026 •

edited

Loading

Uh oh!

Copilot AI left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

ggreif commented Jul 3, 2026

Uh oh!

Copilot AI left a comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Uh oh!

Conversation

ggreif commented Jul 2, 2026 • edited by lwshang Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Spec (spec/Candid.md)

Reference implementation (rust/candid)

Tests

Metatheory (coq/)

Release (candid / candid_derive 0.10.32)

Follow-ups (not in this PR)

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

zeropath-ai Bot commented Jul 3, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

ggreif commented Jul 3, 2026

Adversarial review — subtyping soundness & wire-format

Checked and OK

Minor observations (all optional, none block merge)

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

ggreif commented Jul 2, 2026 •

edited by lwshang

Loading

Spec (`spec/Candid.md`)

Reference implementation (`rust/candid`)

Metatheory (`coq/`)

Release (`candid` / `candid_derive` 0.10.32)

zeropath-ai Bot commented Jul 3, 2026 •

edited

Loading