spec: service <: principal + release candid 0.10.32 (#748)

## 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).

---------

Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Co-authored-by: mraszyk <31483726+mraszyk@users.noreply.github.com>
Co-authored-by: Linwei Shang <linwei.shang@dfinity.org>

Author: 4 people

CHANGELOG.md

@@ -1,5 +1,12 @@
 # Changelog
 
+## 2026-07-06
+
+### Candid 0.10.32
+
+* Non-breaking changes:
+  + A service reference now decodes where a `principal` is expected: `service <actortype>` is a subtype of `principal` (spec addition: `service <: principal`, modelled analogously to `nat <: int`). The subtype checker and the deserializer accept a service reference at type `principal`; the two share an identical wire encoding, so the coercion is the identity on the reference. The reverse (a `principal` at a `service` type) remains rejected.
+
 ## 2026-07-03
 
 ### ic_principal 0.1.5

Cargo.lock

@@ -35,6 +35,8 @@ CoInductive T :=
   | NullT : T
   | OptT : T -> T
   | FuncT : T -> T -> T
+  | ServiceT : T
+  | PrincipalT : T
   | VoidT : T
   | ReservedT : T
   .
@@ -54,6 +56,8 @@ Inductive V :=
   | NullV : V
   | SomeV : V -> V
   | FuncV : RefV -> V
+  | ServiceV : RefV -> V
+  | PrincipalV : RefV -> V
   | ReservedV : V
   .
 (**
@@ -91,6 +95,12 @@ Inductive HasType : V -> T -> Prop :=
   | FuncHT:
     case funcHT,
     forall rv t1 t2, FuncV rv :: FuncT t1 t2
+  | ServiceHT:
+    case serviceHT,
+    forall rv, ServiceV rv :: ServiceT
+  | PrincipalHT:
+    case principalHT,
+    forall rv, PrincipalV rv :: PrincipalT
   | ReservedHT:
     case reservedHT,
     ReservedV :: ReservedT
@@ -105,6 +115,9 @@ CoInductive Subtype : T -> T -> Prop :=
   | NatIntST :
     case natIntST,
     NatT <: IntT
+  | ServicePrincipalST :
+    case servicePrincipalST,
+    ServiceT <: PrincipalT
   | OptST :
     case optST,
     forall t1 t2,
@@ -179,6 +192,9 @@ Function coerce (t1 : T) (t2 : T) (v1 : V) : V :=
   | IntV n, IntT, IntT => IntV n
   | NatV n, NatT, IntT => IntV (Z.of_nat n)
   | FuncV r, FuncT ta1 tr1, FuncT ta2 tr2 => FuncV r
+  | ServiceV r, ServiceT, ServiceT => ServiceV r
+  | PrincipalV r, PrincipalT, PrincipalT => PrincipalV r
+  | ServiceV r, ServiceT, PrincipalT => PrincipalV r
 
   | SomeV v, OptT t1, OptT t2 =>
     if t1 <:? t2
@@ -195,6 +211,9 @@ Function coerce (t1 : T) (t2 : T) (v1 : V) : V :=
   | FuncV r, FuncT ta1 tr1, OptT (FuncT ta2 tr2) =>
     if ta2 <:? ta1
     then if tr1 <:? tr2 then SomeV (FuncV r) else NullV else NullV
+  | ServiceV r, ServiceT, OptT ServiceT => SomeV (ServiceV r)
+  | PrincipalV r, PrincipalT, OptT PrincipalT => SomeV (PrincipalV r)
+  | ServiceV r, ServiceT, OptT PrincipalT => SomeV (PrincipalV r)
 
   | v, t, ReservedT => ReservedV
 
@@ -237,6 +256,16 @@ Proof.
       destruct (t3 <:? t2_2); try reflexivity.
       contradict HNotST; named_constructor; assumption.
   }
+  [serviceHT]: {
+    destruct (ServiceT <:? t2) as [HST | HNotST].
+    - inversion HST; subst; clear HST; simpl; reflexivity.
+    - destruct t2; try reflexivity; contradict HNotST; named_constructor.
+  }
+  [principalHT]: {
+    destruct (PrincipalT <:? t2) as [HST | HNotST].
+    - inversion HST; subst; clear HST; simpl; reflexivity.
+    - destruct t2; try reflexivity; contradict HNotST; named_constructor.
+  }
 Qed.
 
 Lemma coerce_reservedT:
@@ -254,6 +283,9 @@ Lemma coerce_nice_ind:
   (case natC, forall n, P NatT NatT (NatV n) (NatV n)) ->
   (case intC, forall n, P IntT IntT (IntV n) (IntV n)) ->
   (case natIntC, forall n, P NatT IntT (NatV n) (IntV (Z.of_nat n))) ->
+  (case serviceC, forall r, P ServiceT ServiceT (ServiceV r) (ServiceV r)) ->
+  (case principalC, forall r, P PrincipalT PrincipalT (PrincipalV r) (PrincipalV r)) ->
+  (case servicePrincipalC, forall r, P ServiceT PrincipalT (ServiceV r) (PrincipalV r)) ->
   (case nullC, P NullT NullT NullV NullV) ->
   (case nullOptC, forall t, P NullT (OptT t) NullV NullV) ->
   (case optNullC, forall t1 t2, P (OptT t1) (OptT t2) NullV NullV) ->
@@ -293,7 +325,7 @@ Lemma coerce_nice_ind:
   (forall t1 t2 v1, t1 <: t2 -> v1 :: t1 -> P t1 t2 v1 (coerce t1 t2 v1)).
 Proof.
   intros P.
-  intros NatC IntC NatIntC NullC NullOptC OptNullC OptSomeC OpportunisticOptC ReservedOptC ConstituentOptC OpportunisticConstituentOptC FuncC ReservedC.
+  intros NatC IntC NatIntC ServiceC PrincipalC ServicePrincipalC NullC NullOptC OptNullC OptSomeC OpportunisticOptC ReservedOptC ConstituentOptC OpportunisticConstituentOptC FuncC ReservedC.
   intros t1 t2 v1 HST HHT.
   revert t2 HST.
   induction HHT; name_cases.
@@ -319,6 +351,8 @@ Proof.
           - contradict n0. named_constructor.
           - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
           - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+          - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+          - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
     }
     [reservedST]: { apply ReservedC; clear_names. named_constructor. }
   }
@@ -338,6 +372,8 @@ Proof.
           - contradict n0. named_constructor.
           - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
           - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+          - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+          - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
     }
     [reservedST]: { apply ReservedC; clear_names. named_constructor. }
   }
@@ -370,6 +406,8 @@ Proof.
                ++ apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
             ** apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
           - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+          - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+          - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
     }
     [funcST]: { apply FuncC; clear_names; assumption. }
     [reservedST]: { apply ReservedC; clear_names. named_constructor. }
@@ -405,13 +443,57 @@ Proof.
     }
     [reservedST]: { apply ReservedC; clear_names. named_constructor; assumption. }
   }
-  [reservedHT]: { 
+  [reservedHT]: {
     intros.
     inversion HST; subst; clear HST; name_cases.
     [reflST]: { apply ReservedC; clear_names. named_constructor. }
     [optST]: { apply ReservedOptC; clear_names. }
     [reservedST]: { apply ReservedC; clear_names.  named_constructor. }
   }
+  [serviceHT]: {
+    intros.
+    inversion HST; subst; clear HST; name_cases.
+    [reflST]: { apply ServiceC; clear_names. }
+    [servicePrincipalST]: { apply ServicePrincipalC; clear_names. }
+    [optST]: {
+      destruct (is_opt_like_type t0) eqn:His_opt_like.
+      * destruct t0; inversion His_opt_like; simpl; clear His_opt_like;
+        apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+      * destruct (subtyping_decidable ServiceT t0) as [s | Hn].
+        + destruct t0; inversion s; subst; clear s; inversion His_opt_like; clear His_opt_like.
+          - apply ConstituentOptC; clear_names; simpl; intuition; named_constructor.
+          - apply ConstituentOptC; clear_names; simpl; intuition; named_constructor.
+        + destruct t0; inversion His_opt_like; clear His_opt_like.
+          - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+          - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+          - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+          - contradict Hn. named_constructor.
+          - contradict Hn. named_constructor.
+          - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+    }
+    [reservedST]: { apply ReservedC; clear_names. named_constructor. }
+  }
+  [principalHT]: {
+    intros.
+    inversion HST; subst; clear HST; name_cases.
+    [reflST]: { apply PrincipalC; clear_names. }
+    [optST]: {
+      destruct (is_opt_like_type t0) eqn:His_opt_like.
+      * destruct t0; inversion His_opt_like; simpl; clear His_opt_like;
+        apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+      * destruct (subtyping_decidable PrincipalT t0) as [s | Hn].
+        + destruct t0; inversion s; subst; clear s; inversion His_opt_like; clear His_opt_like.
+          - apply ConstituentOptC; clear_names; simpl; intuition; named_constructor.
+        + destruct t0; inversion His_opt_like; clear His_opt_like.
+          - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+          - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+          - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+          - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+          - contradict Hn. named_constructor.
+          - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+    }
+    [reservedST]: { apply ReservedC; clear_names. named_constructor. }
+  }
 Qed.
 
 (**
@@ -737,6 +819,10 @@ CoInductive UpToNull : V -> V -> Prop :=
     SomeV v1 ~~ SomeV v2
   | FuncUT:
     forall r, FuncV r ~~ FuncV r
+  | ServiceUT:
+    forall r, ServiceV r ~~ ServiceV r
+  | PrincipalUT:
+    forall r, PrincipalV r ~~ PrincipalV r
   | ReservedUT:
     ReservedV ~~ ReservedV
 where "v1 ~~ v2" := (UpToNull v1 v2).

coq/MiniCandid.v

@@ -1,22 +1,29 @@
 {}:
 let
-  sources =  import ./sources.nix;
-
   subpath = import ./gitSource.nix;
 
+  # Re-pinned to a modern nixpkgs that provides coq_8_18.
+  #
+  # The previous 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 of which these proofs use.
+  # coq_8_18 is the newest coq that still accepts them unchanged.
+  nixpkgs = fetchTarball {
+    url = "https://github.com/NixOS/nixpkgs/archive/e8273b29fe1390ec8d4603f2477357555291432e.tar.gz";
+    sha256 = "1k8idy9ka87c7gjb9aiqrcx4l9kwblv8fs4pwf0byjivsmbjfdhi";
+  };
+
   overlays = [
     (pkgs: super: { local = {
-      # Fetch niv from nix/sources.json, newer than nixpkgs
-      niv = (import sources.niv {}).niv;
-
       # the main product: building the theories
       theories = pkgs.stdenv.mkDerivation {
         name = "candid-coq";
         src = subpath ./..;
         buildInputs = [
           pkgs.dune_2
-          pkgs.coq
-          pkgs.ocaml
+          pkgs.coq_8_18
+          pkgs.coq_8_18.ocaml
+          pkgs.coq_8_18.ocamlPackages.findlib
         ];
         buildPhase = ''
           dune build --display=short
@@ -31,24 +38,8 @@ let
         inputsFrom = [
           pkgs.local.theories
         ];
-        propagatedBuildInputs = [
-          pkgs.niv
-        ];
-
-        # This helps with using GUI programs like coqide
-        LOCALE_ARCHIVE = pkgs.stdenv.lib.optionalString pkgs.stdenv.isLinux "${pkgs.glibcLocales}/lib/locale/locale-archive";
-
-        # allow building this as a derivation, so that CI can biuld and cache
-        # the dependencies of shell
-        phases = ["installPhase" "fixupPhase"];
-        installPhase = ''
-          mkdir $out
-        '';
-        preferLocalBuild = true;
-        allowSubstitutes = true;
       };
     };})
   ];
 
-in import sources.nixpkgs { inherit overlays; }
-
+in import nixpkgs { inherit overlays; }