diff --git a/spec/Candid.md b/spec/Candid.md index f22cf883..72f0c4d3 100644 --- a/spec/Candid.md +++ b/spec/Candid.md @@ -1,8 +1,8 @@ # Candid Specification -Version: 0.1.2 +Version: 0.1.3 -Date: Aug 25, 2020 +Date: February 3, 2021 ## Motivation @@ -882,139 +882,91 @@ service { : ; ;* } <: service { : ; ### Coercion -This subtyping is implemented during the deserialisation of Candid at an expected type. As described in [Section Deserialisation](#deserialisation), the binary value is conceptually first _decoded_ into an abstract value, and then _coerced_ to the expected type. +This subtyping is implemented during the deserialisation of Candid at an expected type. As described in [Section Deserialisation](#deserialisation), the binary value is conceptually first _decoded_ into the actual type and a value of that type, and then that value is _coerced_ into the expected type. -This section describes the coercion, as a ternary relation `V ~> V' : T` to describe when a value `V` can be coerced to a value `V'` of type `T`. The fields `V` and `T` can be understood as inputs and `V'` as the output of this relation. +To model this, we define, for every `t1, t2` with `t1 <: t2`, a function `C[t1<:t2] : t1 -> t2`. This function maps values of type `t1` to values of type `t2`, and is indeed total. -Here `V` models untyped values, which form an abstract data model of both the message in transit (`V`), as well as the result of the coercion (`V'`). In the following, we re-use the syntax of the textual representation, with the following changes to make it free of overloading: - - * Number literals (``) must be immediately enclosed with an `` that clarifies the precise number type. - * The canonical value of type `reserved` is expressed as `(null : reserved)`. - * No other use of ``. +to describe these values, we re-use the syntax of the textual representation, and use the the `` syntax (i.e. `(v : t)`) if necessary to resolve overloading. #### Primitive Types -Values of primitive types coerce successfully at their own type: +On primitve types, coercion is the identity: ``` --------------------------------------------------- -( : ) ~> ( : ) : - -------------------- -true ~> true : bool - ---------------------- -false ~> false : bool - ------------------------ - ~> : text - -------------------- -null ~> null : null +C[ <: ](x) = x for every ∈ , bool, text, null ``` -Values of type `nat` coerce successfully at type `int`: +Values of type `nat` coerce at type `int`: ``` --------------------------------- -( : nat) ~> ( : int) : int +C[nat <: int]() = ``` -Any value coerces at type `reserved`, producing the canonical value of type `reserved`: - +Coercion into `reserved` is the constant map (this is arbitrarily using `null` as “the” value of `reserved`): ``` ------------------------------------ - ~> (null : reserved) : reserved +C[ <: reserved](_) = null ``` - -NB: No rule is needed for type `empty`, because there are no values of that type. By construction, ` ~> _ : empty` will not hold. +NB: No rule is needed for type `empty`, because there are no values of that type. By construction, `C[empty <: ]` is the unique function on the empty domain. #### Vectors -Only vectors coerce at vector types, and only if all elements coerce successfully. - +Vectors coerce pointwise: ``` - ~> : ------------------------------------------ -vec { ;* } ~> vec { ;* } : vec +C[vec <: vec ]( vec { ;* } ) = vec { C[ <: ]();* } ``` #### Options -The null value coerce at any option type: +The null type coerces into any option type: ``` ----------------------- -null ~> null : opt +C[null <: opt ](null) = null ``` -An optional value coerces at an option type, if the constituent value coerces at the constituent type: -``` - ~> : ------------------------------ -opt ~> opt : opt +An optional value coerces at an option type, if the constituent value has a suitable type, and else goes to `null`: ``` - -If an optional value _fails_ to coerce at an optional type, or the value is `reserved`, the result is `null`, not failure: +C[opt <: opt ](null) = null +C[opt <: opt ](opt ) = opt C[ <: ](v) if <: +C[opt <: opt ](opt ) = null if not( <: ) ``` -not ( ~> _ : ) -------------------------- -opt ~> null : opt ------------------------------------ -(null : reserved) ~> null : opt -``` +NOTE: These rules above imply that a Candid decoder has to be able to decide the subtyping relation at runtime. Coercing a non-null, non-optional and non-reserved value at an option type treats it as an optional value: ``` - ≠ null - ≠ (null : reserved) - ≠ opt _ -not (null <: ) -opt ~> : opt -------------------------- - ~> : opt +C[ <: opt ]() = opt C[ <: ](v) if not (null <: ) and <: +C[ <: opt ](_) = null if not (null <: ) and not ( <: ) +C[reserved <: opt ](_) = null ``` - #### Records -Only records coerce at record type. Missing fields of option or reserved type turn into `null`. +In the following rule: + + * The `*` field names are those present in both the actual and expected type. The values are coerced. + * the `*` field names those only in the actual type. The values are ignored. + * the `*` field names are those only in the expected type, which therefore must be of optional or reserved type. The `null` value is used for these. -In the following rule, the `*` field names are those present in both the value and the type, the `*` field names only those in the value, and `*` are those only in the type. ``` - ~> : -opt empty <: ---------------------------------------------------------------------------------------------------------------------------------------- -record { = ;* = ;* } ~> record { = ;* = null;* } : record { = ;* = ;* } +C[record { = ;* = ;* } <: record { = ;* = ;* }](record { = ;* = ;* }) + = record { = C[ <: ]();* = null;* } ``` - #### Variants Only a variant value with an expected tag coerces at variant type. ``` - ~> : ----------------------------------------------------------------------------------- -variant { = } ~> variant { = } : variant { = ; _;* } +C[variant { = ; _;* } <: variant { = ; _;* }](variant { = }) + = variant { = C[ <: ]() } ``` #### References -Function and services references coerce unconditionally - -``` ------------------------------------------------------- -func . ~> func . : func -``` - -``` ------------------------------------------------------- -service ~> service : service -``` +Function and services reference values are untyped, so the coercion function is the identity here: ``` ------------------------------------------------- -principal ~> principal : principal +C[func <: func ](func .) = func . +C[service <: service ](service ) = service +C[principal <: principal](principal ) = principal ``` #### Tuple types @@ -1022,60 +974,58 @@ principal ~> principal : principal Whole argument and result sequences are coerced with the same rules as tuple-like records. In particular, extra arguments are ignored, and optional parameters read as as `null` if the argument is missing or fails to coerce: ``` -record {;*} ~> record {,*} : record {;*} --------------------------------------------------- -(,*) ~> (,*) : (,*) +C[(,*) <: (,*)]((,*)) = (,*) + if C[record {;*} <: record {,*}](record {;*}) = record {;*} ``` ## Properties -The relations above have certain properties. To express them, we need the relation `V : T`, expressing that `V` has inherently type `T`. Instead of defining this relation on its own, we take the first property below as its definition: +The relations above have certain properties. As in the previous section, ` : ` means that has inherently type ``. -* Correctness and completeness of decoding: +* Reflexivity of subtyping: ``` - (v : T) ⟺ (∃ v'. v' ~> v : T) + <: ``` -* Roundtripping: +* Transitivity of subtyping: ``` - (v : T) ⟺ v ~> v : T + <: , <: ⇒ <: ``` -* Uniqueness of decoding: +* Roundtripping: ``` - v ~> v1 : T ∧ v ~> v2 : T ⇒ v1 = v2 + ( : ) ⟺ C[ <: ]() = ``` -* Soundness of subtyping: +* Soundness of subtyping (or, alternatively, well-definedness of coercion) ``` - T <: T' ⇒ ∀ v : T. ∃ v'. v ~> v' : T + <: ⇒ ∀ : . v[ <: ]() : ``` * Higher-order soundness of subtyping See <./IDL-Soundness.md>, with the following instantiations: ``` s1 ~> s2 ≔ s2 <: s1 - t1 <: t2 ≔ (∀ v. v : t1 ⇒ v ~> _ : t2 ) + t1 <: t2 ≔ t1 <: t2 s1 in t1 <: s2 in t2 ≔ (to be done) s1 <:h s2 ≔ (host-language dependent) ``` -* Transitivity of subtyping: +* NB: Transitive coherence does not hold: ``` - T1 <: T2, T2 <: T3 ⇒ T1 <: T3 + <: , <: ``` - -* Transitive coherence does not hold: + does not imply ``` - T1 <: T2, T2 <: T3 - v1 : T1 - v1 ~> v3 : T3 - v1 ~> v2 : T2, v2 ~> v2 : T3 + C[ <: ] = C[ <: ] ⚬ C[ <: ] ``` - does not imply `v3 = v3'`. - However, it implies that `R(v3,v3')`, where `R` is the smallest homomorphic, reflexive, symmetric relation `R` that satisfies `∀ v. R(opt v, null)`. + However, it implies + ``` + C[ <: ] ~ (C[ <: ] ⚬ C[ <: ]) + ``` + where ~ is the smallest homomorphic, reflexive, symmetric relation that satisfies `∀ v. opt v ~ null`. The goal of “subtyping completeness” has not been cast into a formal formulation yet. @@ -1299,9 +1249,10 @@ Note: Deserialisation at an expected type sequence `(,*)` proceeds by * checking for the magic number `DIDL` - * using the inverse of the `T` function to decode the type definitions `(*)` - * using the inverse of the `M` function, indexed by `(*)`, to decode the values `(*)` - * use the coercion relation `(,*) ~> (,*) : (,*)` to try to understand the decoded values at the expected type. + * using the inverse of the `T` function to decode the type definitions `(,*)` + * check that `(,*) <: (,*)`, else fail + * using the inverse of the `M` function, indexed by `(,*)`, to decode the values `(,*)` + * use the coercion function `C[(,*) <: (,*)]((,*))` to understand the decoded values at the expected type. ### Deserialisation of future types diff --git a/test/construct.test.did b/test/construct.test.did index a517a7ea..168d6bfb 100644 --- a/test/construct.test.did +++ b/test/construct.test.did @@ -1,5 +1,7 @@ /* Encoding tests for construct types + +Corresponding to spec version version 0.1.2 */ // Type definitions diff --git a/test/overshoot.test.did b/test/overshoot.test.did index f563d680..32467639 100644 --- a/test/overshoot.test.did +++ b/test/overshoot.test.did @@ -1,4 +1,6 @@ /* +Corresponding to spec version version 0.1.2 + The tests in this file involve large leb-encoded values that indicate sizes (of tables, arrays, blobs, etc.). In all cases, a decode should be able to catch that eary by noticing that the overall input is too short to potentially diff --git a/test/prim.test.did b/test/prim.test.did index 2035f9ec..ec385b29 100644 --- a/test/prim.test.did +++ b/test/prim.test.did @@ -1,5 +1,7 @@ /* Encoding tests for primitive types + +Corresponding to spec version version 0.1.2 */ // fundamentally wrong diff --git a/test/reference.test.did b/test/reference.test.did index 69a1c555..77b65633 100644 --- a/test/reference.test.did +++ b/test/reference.test.did @@ -1,5 +1,7 @@ /* Encoding tests for reference types + +Corresponding to spec version version 0.1.2 */ // principal