spec: service <: principal + release candid 0.10.32

CHANGELOG.md

@@ -2,6 +2,11 @@
 
 ## 2026-07-02
 
+### 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.
+
 ### ic_principal 0.1.4
 
 * Non-breaking changes:

coq/MiniCandid.v

@@ -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/nix/default.nix

@@ -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 = "sha256-mFP086y1bNA1g9AsY/pCue3H3W2R7ayroHyRbZrcMf0=";
+  };
+
   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; }

rust/candid/src/de.rs

@@ -618,8 +618,20 @@ impl<'de> Deserializer<'de> {
         V: Visitor<'de>,
     {
         self.unroll_type()?;
+        // Dispatched only when the expected type is `principal`. Accept exactly
+        // the two wire types that share the `PrincipalBytes` encoding: `principal`
+        // (reflexive) and `service <actortype>` (spec: `service <: principal`), so
+        // a service reference decodes as its principal. We match the wire type
+        // directly rather than calling `check_subtype()`: the general subtype
+        // relation also admits `empty` (bottom) `<: principal`, which would let a
+        // payload declare wire type `empty` yet be decoded as a principal from
+        // arbitrary trailing bytes. Matching also avoids the subtype-check
+        // overhead on this common decoding path.
         check!(
-            *self.expect_type == TypeInner::Principal && *self.wire_type == TypeInner::Principal,
+            matches!(
+                self.wire_type.as_ref(),
+                TypeInner::Principal | TypeInner::Service(_)
+            ),
             "principal"
         );
         let mut bytes = vec![2u8];

rust/candid/src/types/subtype.rs

@@ -272,6 +272,10 @@ fn subtype_collect_(
         (_, Reserved) => (),
         (Empty, _) => (),
         (Nat, Int) => (),
+        // A service reference is represented by its canister's principal, so any
+        // service type is a subtype of `principal` (spec: `service <: principal`),
+        // unconditionally — like `Nat <: Int`.
+        (Service(_), Principal) => (),
         (Vec(ty1), Vec(ty2)) => {
             subtype_collect_(report, gamma, env, ty1, ty2, depth, path, errors, is_input);
         }
@@ -555,6 +559,7 @@ fn subtype_(
         (_, Reserved) => Ok(()),
         (Empty, _) => Ok(()),
         (Nat, Int) => Ok(()),
+        (Service(_), Principal) => Ok(()),
         (Vec(ty1), Vec(ty2)) => subtype_(report, gamma, env, ty1, ty2, depth),
         (Null, Opt(_)) => Ok(()),
         (Opt(ty1), Opt(ty2)) if subtype_(report, gamma, env, ty1, ty2, depth).is_ok() => Ok(()),

spec/Candid.md

@@ -756,6 +756,14 @@ An exception are integers, which can be specialised to natural numbers:
 nat <: int
 ```
 
+Similarly, a principal can be specialised to any service reference:
+
+```
+
+--------------------------------
+service <actortype> <: principal
+```
+
 Additional rules apply to `empty` and `reserved`, which makes these a bottom resp. top type:
 ```
 
@@ -921,6 +929,12 @@ Values of type `nat` coerce at type `int`:
 <nat> : nat ~> <nat> : int
 ```
 
+A service reference coerces at type `principal` (both share the same value form, so this is the identity on the value):
+```
+---------------------------------------------------------------------
+service <text> : service <actortype> ~> principal <text> : principal
+```
+
 Coercion into `reserved` is the constant map (this is arbitrarily using `null` as “the” value of `reserved`):
 ```
 --------------------------

test/reference.test.did

@@ -26,6 +26,27 @@ assert blob "DIDL\02\6a\01\71\01\7d\00\69\01\03foo\00\01\01\01\03\ca\ff\ee"
 assert blob "DIDL\02\6a\01\71\01\7d\00\69\02\03foo\00\04foo\32\00\01\01\01\03\ca\ff\ee"
   == "(service \"w7x7r-cok77-xa\")" : (service { foo : (text) -> (nat); foo2 : (text) -> (nat) }) "service";
 
+// service <: principal: a service reference value decodes at type `principal`
+// (identical wire encoding). The reverse (a principal at `service {}`) is rejected above.
+assert blob "DIDL\01\69\00\01\00\01\03\ca\ff\ee" == "(principal \"w7x7r-cok77-xa\")" : (principal) "service {} value decodes at principal";
+assert blob "DIDL\02\6a\01\71\01\7d\00\69\01\03foo\00\01\01\01\03\ca\ff\ee"
+  == "(principal \"w7x7r-cok77-xa\")" : (principal) "service {foo} value decodes at principal";
+// ...but `empty` (bottom) must NOT be accepted as a principal wire type: although
+// `empty <: principal` holds, an `empty`-typed value carries no bytes, so admitting
+// it would let a payload declare wire type `empty` yet be decoded as a principal
+// from arbitrary trailing bytes. Same trailing bytes as the `\68` principal above.
+assert blob "DIDL\00\01\6f\01\03\ca\ff\ee" !: (principal) "principal: reject empty (bottom) wire type";
+// A recursive service type (its method returns the service itself) still decodes
+// at `principal`: the wire type unrolls to a `service` head and only the
+// PrincipalBytes are read from the value stream.
+assert blob "DIDL\02\69\01\01m\01\6a\00\01\01\00\01\00\01\03\ca\ff\ee"
+  == "(principal \"w7x7r-cok77-xa\")" : (principal) "recursive service value decodes at principal";
+// Only `principal`/`service` wire types coerce to `principal`; other reference and
+// aggregate wire types are rejected (they do not share the PrincipalBytes encoding).
+assert blob "DIDL\01\6a\00\00\00\01\00\01\01\03\ca\ff\ee\01\61" !: (principal) "principal: reject func wire type";
+assert blob "DIDL\01\6c\00\01\00"                               !: (principal) "principal: reject record wire type";
+assert blob "DIDL\01\6e\7d\01\00\00"                            !: (principal) "principal: reject opt wire type";
+
 assert blob "DIDL\02\6a\01\71\01\7d\00\69\03\03foo\00\04foo\32\00\01\01\01\03\ca\ff\ee" !: (service { foo : (text) -> (nat); foo2 : (text) -> (nat) }) "service: too long";
 assert blob "DIDL\02\6a\01\71\01\7d\00\69\01\03foo\00\04foo\32\00\01\01\01\03\ca\ff\ee" !: (service { foo : (text) -> (nat); foo2 : (text) -> (nat) }) "service: too short";
 assert blob "DIDL\02\6a\01\71\01\7d\00\69\02\04foo\32\00\03foo\00\01\01\01\03\ca\ff\ee" !: (service { foo : (text) -> (nat); foo2 : (text) -> (nat) }) "service: unsorted";

test/subtypes.test.did

@@ -157,6 +157,19 @@ assert blob "DIDL\02\6a\00\01\01\00\6d\01\01\00\01\01\00\01m"
 assert blob "DIDL\03\6a\00\01\01\00\6d\02\6d\02\01\00\01\01\00\01m"
    == "(opt func \"aaaaa-aa\".m)" : (opt func () -> (Vec)) "vec {µ vec} <: (µ vec)";
 
+// service references: every service type is a subtype of `principal`
+// (spec: `service <actortype> <: principal`), but not vice versa.
+assert blob "DIDL\02\6a\00\01\01\00\69\00\01\00\01\01\00\01m"
+   == "(opt func \"aaaaa-aa\".m)" : (opt func () -> (principal)) "service {} <: principal";
+assert blob "DIDL\03\6a\00\01\01\00\69\01\01m\02\6a\00\00\00\01\00\01\01\00\01m"
+   == "(opt func \"aaaaa-aa\".m)" : (opt func () -> (principal)) "service {m:()->()} <: principal";
+assert blob "DIDL\01\6a\00\01\68\00\01\00\01\01\00\01m"
+   == "(null)" : (opt func () -> (service {})) "principal </: service {}";
+// a recursive (µ) service type is still <: principal (Var-alias chain resolves to
+// the service head, which is unconditionally a subtype of principal)
+assert blob "DIDL\03\6a\00\01\01\00\69\01\01m\02\6a\00\01\01\00\01\00\01\01\00\01m"
+   == "(opt func \"aaaaa-aa\".m)" : (opt func () -> (principal)) "(µ service) <: principal";
+
 // future types
 // This uses 0x67 for the “future type”; bump (well, decrement) once that
 // becomes a concrete future type