From 41a84c8d6b9eac9456da9f51dcf67ee9fa99b951 Mon Sep 17 00:00:00 2001 From: Yan Chen Date: Tue, 11 Jan 2022 17:04:49 -0800 Subject: [PATCH 1/7] spec: subtype checking only for reference types --- spec/Candid.md | 62 +++++++++++++++++++++++++------------------------- 1 file changed, 31 insertions(+), 31 deletions(-) diff --git a/spec/Candid.md b/spec/Candid.md index 576ac1c68..a6d5db56e 100644 --- a/spec/Candid.md +++ b/spec/Candid.md @@ -1,8 +1,8 @@ # Candid Specification -Version: 0.1.3 +Version: 0.1.4 -Date: February 3, 2021 +Date: January 11, 2022 ## Motivation @@ -885,63 +885,61 @@ service { : ; ;* } <: service { : ; 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. -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. +To model this, we define a partial coercion function `C[t1 ~> t2] : t1 -> t2`. This function maps values of type `t1` to values of type `t2`. For every `t1, t2` with `t1 <: t2`, the function is always defined, but not every `t1, t2` has a coercion. -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. +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 On primitve types, coercion is the identity: ``` -C[ <: ](x) = x for every ∈ , bool, text, null +C[ ~> ](x) = x for every ∈ , bool, text, null ``` Values of type `nat` coerce at type `int`: ``` -C[nat <: int]() = +C[nat ~> int]() = ``` Coercion into `reserved` is the constant map (this is arbitrarily using `null` as “the” value of `reserved`): ``` -C[ <: reserved](_) = null +C[ ~> reserved](_) = null ``` -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. +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 Vectors coerce pointwise: ``` -C[vec <: vec ]( vec { ;* } ) = vec { C[ <: ]();* } +C[vec ~> vec ]( vec { ;* } ) = vec { C[ ~> ]();* } ``` #### Options The null type and the reserved type coerce into any option type: ``` -C[null <: opt ](null) = null +C[null ~> opt ](null) = null ``` An optional value coerces at an option type, if the constituent value has a suitable type, and else goes to `null`: ``` -C[opt <: opt ](null) = null -C[opt <: opt ](opt ) = opt C[ <: ](v) if <: -C[opt <: opt ](opt ) = null if not( <: ) +C[opt ~> opt ](null) = null +C[opt ~> opt ](opt ) = opt C[t ~> t'](v) if t ~> t' +C[opt ~> opt ](opt ) = null if not (t ~> t') ``` Coercing a non-null, non-optional and non-reserved type at an option type treats it as an optional value, if it has a suitable type: ``` -C[ <: opt ]() = opt C[ <: ](v) if not (null <: ) and <: +C[ ~> opt ]() = opt C[ ~> ](v) if not (null <: ) and ~> ``` Any other type goes to `null`: ``` -C[reserved <: opt ](_) = null -C[ <: opt ](_) = null if not (null <: ) and not ( <: ) -C[ <: opt ](_) = null if null <: and not (null <: ) +C[reserved ~> opt ](_) = null +C[ ~> opt ](_) = null if not (null <: ) and not ( ~> ) +C[ ~> opt ](_) = null if null <: and not (null ~> ) ``` -NOTE: These rules above imply that a Candid decoder has to be able to decide the subtyping relation at runtime. - #### Records In the following rule: @@ -951,8 +949,8 @@ In the following rule: * 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. ``` -C[record { = ;* = ;* } <: record { = ;* = ;* }](record { = ;* = ;* }) - = record { = C[ <: ]();* = null;* } +C[record { = ;* = ;* } ~> record { = ;* = ;* }](record { = ;* = ;* }) + = record { = C[ ~> ]();* = null;* } ``` #### Variants @@ -960,8 +958,8 @@ C[record { = ;* = ;* } <: record { = ;* Only a variant value with an expected tag coerces at variant type. ``` -C[variant { = ; _;* } <: variant { = ; _;* }](variant { = }) - = variant { = C[ <: ]() } +C[variant { = ; _;* } ~> variant { = ; _;* }](variant { = }) + = variant { = C[ ~> ]() } ``` @@ -970,18 +968,20 @@ C[variant { = ; _;* } <: variant { = ; _;* }](variant { Function and services reference values are untyped, so the coercion function is the identity here: ``` -C[func <: func ](func .) = func . -C[service <: service ](service ) = service -C[principal <: principal](principal ) = principal +C[func ~> func ](func .) = func . if func <: func +C[service ~> service ](service ) = service if service <: service +C[principal ~> principal](principal ) = principal ``` +NOTE: These rules above imply that a Candid decoder has to be able to decide the subtyping relation for reference types. + #### Tuple types 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: ``` -C[(,*) <: (,*)]((,*)) = (,*) - if C[record {;*} <: record {,*}](record {;*}) = record {;*} +C[(,*) ~> (,*)]((,*)) = (,*) + if C[record {;*} ~> record {,*}](record {;*}) = record {;*} ``` @@ -1001,7 +1001,7 @@ The relations above have certain properties. As in the previous section, ` : * Roundtripping: ``` - ( : ) ⟺ C[ <: ]() = + ( : ) ⟺ C[ ~> ]() = ``` * Soundness of subtyping (or, alternatively, well-definedness of coercion) @@ -1024,12 +1024,12 @@ The relations above have certain properties. As in the previous section, ` : ``` does not imply ``` - C[ <: ] = C[ <: ] ⚬ C[ <: ] + C[ ~> ] = C[ ~> ] ⚬ C[ ~> ] ``` However, it implies ``` - C[ <: ] ~ (C[ <: ] ⚬ C[ <: ]) + C[ ~> ] ~ (C[ ~> ] ⚬ C[ ~> ]) ``` where ~ is the smallest homomorphic, reflexive, symmetric relation that satisfies `∀ v. opt v ~ null`. From b4510275298d98f871c05c94ffa099ee654e29f9 Mon Sep 17 00:00:00 2001 From: Yan Chen Date: Wed, 12 Jan 2022 19:22:14 -0800 Subject: [PATCH 2/7] use inference rule instead of partial function --- spec/Candid.md | 92 ++++++++++++++++++++++++++++++++++---------------- 1 file changed, 63 insertions(+), 29 deletions(-) diff --git a/spec/Candid.md b/spec/Candid.md index a6d5db56e..85b9c138a 100644 --- a/spec/Candid.md +++ b/spec/Candid.md @@ -885,59 +885,80 @@ service { : ; ;* } <: service { : ; 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. -To model this, we define a partial coercion function `C[t1 ~> t2] : t1 -> t2`. This function maps values of type `t1` to values of type `t2`. For every `t1, t2` with `t1 <: t2`, the function is always defined, but not every `t1, t2` has a coercion. - -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. +This section describes the coercion, as a relation `V : T ~> V' : T'` to describe when a value `V` of type `T` can be coerced to a value `V'` of type `T'`. The fields `V`, `T` and `T'` can be understood as inputs and `V'` as the output of this relation. +To describe these values, we re-use the syntax of the textual representation. #### Primitive Types On primitve types, coercion is the identity: ``` -C[ ~> ](x) = x for every ∈ , bool, text, null + ∈ , bool, text, null +--------------------------------- + : ~> : ``` Values of type `nat` coerce at type `int`: ``` -C[nat ~> int]() = +-------------------------- + : nat ~> : int ``` Coercion into `reserved` is the constant map (this is arbitrarily using `null` as “the” value of `reserved`): ``` -C[ ~> reserved](_) = null +-------------------------- +_ : ~> null : reserved ``` -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. + +NB: No rule is needed for type `empty`, because there are no values of that type. By construction, ` : ~> _ : empty` will not hold. #### Vectors Vectors coerce pointwise: ``` -C[vec ~> vec ]( vec { ;* } ) = vec { C[ ~> ]();* } + : ~> : +---------------------------------------------------- +vec { ;* } : vec ~> vec { ;* } : vec ``` #### Options -The null type and the reserved type coerce into any option type: +The null value coerces into any option type: ``` -C[null ~> opt ](null) = null +----------------------------- +null : _ ~> null : opt ``` An optional value coerces at an option type, if the constituent value has a suitable type, and else goes to `null`: ``` -C[opt ~> opt ](null) = null -C[opt ~> opt ](opt ) = opt C[t ~> t'](v) if t ~> t' -C[opt ~> opt ](opt ) = null if not (t ~> t') + : ~> : +---------------------------------------- +opt : opt ~> opt : opt + +not ( : ~> _ : ) +---------------------------------------- +opt : opt ~> null : opt ``` Coercing a non-null, non-optional and non-reserved type at an option type treats it as an optional value, if it has a suitable type: ``` -C[ ~> opt ]() = opt C[ ~> ](v) if not (null <: ) and ~> +not (null <: ) + : ~> : +-------------------------------- + : ~> opt : opt ``` -Any other type goes to `null`: +Any other value goes to `null`: ``` -C[reserved ~> opt ](_) = null -C[ ~> opt ](_) = null if not (null <: ) and not ( ~> ) -C[ ~> opt ](_) = null if null <: and not (null ~> ) + +not (null <: ) +not ( : ~> _ : ) +-------------------------------- + : ~> null : opt + +null <: +not (null <: ) +---------------------------- + : ~> null : opt ``` #### Records @@ -949,8 +970,11 @@ In the following rule: * 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. ``` -C[record { = ;* = ;* } ~> record { = ;* = ;* }](record { = ;* = ;* }) - = record { = C[ ~> ]();* = null;* } + : ~> : +opt empty <: +------------------------------------------------------------------------------------------- +record { = ;* = ;* } : record { : ;* : ;* } ~> +record { = ;* = null;* } : record { : ;* : ;* } ``` #### Variants @@ -958,8 +982,10 @@ C[record { = ;* = ;* } ~> record { = ;* Only a variant value with an expected tag coerces at variant type. ``` -C[variant { = ; _;* } ~> variant { = ; _;* }](variant { = }) - = variant { = C[ ~> ]() } + : ~> : +---------------------------------------------------------- +variant { = ; } : variant { : ; _;* } ~> +variant { = } : variant { : ; _;* } ``` @@ -968,9 +994,16 @@ C[variant { = ; _;* } ~> variant { = ; _;* }](variant { Function and services reference values are untyped, so the coercion function is the identity here: ``` -C[func ~> func ](func .) = func . if func <: func -C[service ~> service ](service ) = service if service <: service -C[principal ~> principal](principal ) = principal +func <: func +--------------------------------------------------------------------- +func .id : func ~> func .id : func + +service <: service +----------------------------------------------------------------------------- +service : service ~> service : service + +------------------------------------------------------------ +principal : principal ~> principal : principal ``` NOTE: These rules above imply that a Candid decoder has to be able to decide the subtyping relation for reference types. @@ -980,8 +1013,9 @@ NOTE: These rules above imply that a Candid decoder has to be able to decide the 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: ``` -C[(,*) ~> (,*)]((,*)) = (,*) - if C[record {;*} ~> record {,*}](record {;*}) = record {;*} +record { ;* } : record { ;* } ~> record { ;* } : record { ;* } +---------------------------------------------------------------------------- +(,*) : (,*) ~> (,*) : (,*) ``` @@ -1001,12 +1035,12 @@ The relations above have certain properties. As in the previous section, ` : * Roundtripping: ``` - ( : ) ⟺ C[ ~> ]() = + ( : ) ⟺ : ~> : ``` * Soundness of subtyping (or, alternatively, well-definedness of coercion) ``` - <: ⇒ ∀ : . v[ <: ]() : + <: ⇒ ∀ : ∃ . : ~> : ``` * Higher-order soundness of subtyping From fa36bc09e7d1ffc284c38cff5df6e3fb20a84be8 Mon Sep 17 00:00:00 2001 From: Yan Chen <48968912+chenyan-dfinity@users.noreply.github.com> Date: Thu, 13 Jan 2022 13:45:51 -0800 Subject: [PATCH 3/7] Apply suggestions from code review Co-authored-by: Joachim Breitner --- spec/Candid.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/spec/Candid.md b/spec/Candid.md index 85b9c138a..8cae58ea9 100644 --- a/spec/Candid.md +++ b/spec/Candid.md @@ -909,7 +909,7 @@ Coercion into `reserved` is the constant map (this is arbitrarily using `null` a _ : ~> null : reserved ``` -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, `_ : empty ~> _ : _` will not hold. #### Vectors @@ -939,7 +939,7 @@ not ( : ~> _ : ) opt : opt ~> null : opt ``` -Coercing a non-null, non-optional and non-reserved type at an option type treats it as an optional value, if it has a suitable type: +Coercing a non-null, non-optional and non-reserved type at an option type treats it as an optional value, if it can be decoded successfully: ``` not (null <: ) : ~> : @@ -991,7 +991,7 @@ variant { = } : variant { : ; _;* } #### References -Function and services reference values are untyped, so the coercion function is the identity here: +For function and services reference values, the coercion relation checks whether the given types are actually subtypes of the expected type, and fails else: ``` func <: func From a9a03b4127f907f48b36efb05f377803271132d8 Mon Sep 17 00:00:00 2001 From: Yan Chen Date: Thu, 13 Jan 2022 13:56:24 -0800 Subject: [PATCH 4/7] fix --- spec/Candid.md | 21 ++++++++++++++------- 1 file changed, 14 insertions(+), 7 deletions(-) diff --git a/spec/Candid.md b/spec/Candid.md index 8cae58ea9..1be9261a1 100644 --- a/spec/Candid.md +++ b/spec/Candid.md @@ -924,8 +924,9 @@ vec { ;* } : vec ~> vec { ;* } : vec The null value coerces into any option type: ``` +null <: ----------------------------- -null : _ ~> null : opt +null : ~> null : opt ``` An optional value coerces at an option type, if the constituent value has a suitable type, and else goes to `null`: @@ -949,6 +950,8 @@ not (null <: ) Any other value goes to `null`: ``` +--------------------------------- + : reserved ~> null : opt not (null <: ) not ( : ~> _ : ) @@ -1038,6 +1041,11 @@ The relations above have certain properties. As in the previous section, ` : ( : ) ⟺ : ~> : ``` +* Well-typedness: + ``` + : ~> : ⇒ : + ``` + * Soundness of subtyping (or, alternatively, well-definedness of coercion) ``` <: ⇒ ∀ : ∃ . : ~> : @@ -1054,17 +1062,16 @@ The relations above have certain properties. As in the previous section, ` : * NB: Transitive coherence does not hold: ``` - <: , <: + : ~> : + : ~> : + : ~> : ``` does not imply ``` - C[ ~> ] = C[ ~> ] ⚬ C[ ~> ] + = ``` - However, it implies - ``` - C[ ~> ] ~ (C[ ~> ] ⚬ C[ ~> ]) - ``` + However, it implies ` ~ `, 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. From cb6fce75d583b3c8a2b6ffd4e47557945f0644a0 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 10 Feb 2022 12:30:21 +0100 Subject: [PATCH 5/7] Exploration towards including #311 in Coq --- coq/MiniCandid.v | 118 ++++++++++++++++++++++++++--------------------- 1 file changed, 65 insertions(+), 53 deletions(-) diff --git a/coq/MiniCandid.v b/coq/MiniCandid.v index 61bfc58d4..939a6ab15 100644 --- a/coq/MiniCandid.v +++ b/coq/MiniCandid.v @@ -170,36 +170,48 @@ The spec defines the coercion function as indexed by the subtyping relation. But that relation is coinductive, so Coq will not allow that. We thus define the function by recursion on the value. -We use [NullV] on the right-hand side in invalid branches. *) -Function coerce (t1 : T) (t2 : T) (v1 : V) : V := +Function coerce (t1 : T) (t2 : T) (v1 : V) : option V := match v1, t1, t2 with - | NatV n, NatT, NatT => NatV n - | 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 - + | NatV n, NatT, NatT => Some (NatV n) + | IntV n, IntT, IntT => Some (IntV n) + | NatV n, NatT, IntT => Some (IntV (Z.of_nat n)) + | FuncV r, FuncT ta1 tr1, FuncT ta2 tr2 => + if FuncT ta1 tr1 <:? (FuncT ta2 tr2) + then Some (FuncV r) + else None + + | NullV, NullT, NullT => Some NullV + + | NullV, NullT, OptT t2 => Some NullV + | NullV, OptT t1, OptT t2 => Some NullV | SomeV v, OptT t1, OptT t2 => - if t1 <:? t2 - then SomeV (coerce t1 t2 v) - else NullV - + match coerce t1 t2 v with + | None => Some NullV + | Some t => Some (SomeV t) + end + (* We’d prefer the equation from [coerce_constituent_eq] below, + but that looks like it recurses on t2, and that’s coinductive, but that will not satisfy the termination checker, - so let’s repeat all the above ruls for OptT again. + so we have to repeat all the above rules for OptT again. *) - | NatV n, NatT, OptT NatT => SomeV (NatV n) - | IntV n, IntT, OptT IntT => SomeV (IntV n) - | NatV n, NatT, OptT IntT => SomeV (IntV (Z.of_nat n)) + | NatV n, NatT, OptT NatT => Some (SomeV (NatV n)) + | IntV n, IntT, OptT IntT => Some (SomeV (IntV n)) + | NatV n, NatT, OptT IntT => Some (SomeV (IntV (Z.of_nat n))) | FuncV r, FuncT ta1 tr1, OptT (FuncT ta2 tr2) => - if ta2 <:? ta1 - then if tr1 <:? tr2 then SomeV (FuncV r) else NullV else NullV + if FuncT ta1 tr1 <:? (FuncT ta2 tr2) + then Some (SomeV (FuncV r)) + else Some NullV - | v, t, ReservedT => ReservedV + (* The final catch-all for OptT *) + | _, _, OptT t => Some NullV - (* Failure is NullV. Also subsumes “valid” rules that return NullV *) - | _, _, _ => NullV + + | v, t, ReservedT => Some ReservedV + + | _, _, _ => None end. (* We can prove the desired equation at least as an equality *) @@ -207,47 +219,39 @@ Lemma coerce_constituent_eq: forall v t1 t2, v :: t1 -> is_opt_like_type t1 = false -> + is_opt_like_type t2 = false -> coerce t1 (OptT t2) v = - if t1 <:? t2 - then if is_opt_like_type t2 - then NullV - else SomeV (coerce t1 t2 v) - else NullV. + match coerce t1 t2 v with + | None => Some NullV + | Some t => Some (SomeV t) + end. Proof. - intros v t1 t2 HHT His_opt_like. - inversion HHT; subst; clear HHT; inversion His_opt_like; clear His_opt_like; name_cases. + intros v t1 t2 HHT His_opt_like_t1 His_opt_like_t2. + inversion HHT; subst; clear HHT; inversion His_opt_like_t1; clear His_opt_like_t1; name_cases. [natHT]: { - destruct (NatT <:? t2) as [HST | HNotST]. - - inversion HST; subst; clear HST; simpl; reflexivity. - - destruct t2; try reflexivity; contradict HNotST; named_constructor. + destruct t2; subst; inversion His_opt_like_t2; clear His_opt_like_t2; simpl; try reflexivity. } [intHT]: { - destruct (IntT <:? t2) as [HST | HNotST]. - - inversion HST; subst; clear HST; simpl; reflexivity. - - destruct t2; try reflexivity; contradict HNotST; named_constructor. + destruct t2; subst; inversion His_opt_like_t2; clear His_opt_like_t2; simpl; try reflexivity. } [funcHT]: { - destruct (FuncT t0 t3 <:? t2) as [HST | HNotST]. - - inversion HST; subst; clear HST; simpl;try reflexivity. - * repeat rewrite subtype_dec_refl. reflexivity. - * repeat rewrite subtype_dec_true by assumption. reflexivity. - - destruct t2; try reflexivity. - simpl. - destruct (t2_1 <:? t0); try reflexivity. - destruct (t3 <:? t2_2); try reflexivity. - contradict HNotST; named_constructor; assumption. + destruct t2; subst; inversion His_opt_like_t2; clear His_opt_like_t2; simpl; try reflexivity. + destruct (FuncT t0 t3 <:? FuncT t2_1 t2_2); try reflexivity. } Qed. Lemma coerce_reservedT: - forall v t1, coerce t1 ReservedT v = ReservedV. + forall v t1, coerce t1 ReservedT v = Some ReservedV. Proof. intros v1 t1. destruct v1, t1; reflexivity. Qed. +(** TODO: What to make of this now + + (** -This beast of a lemma defines and proves a nice induction principle for [coerce]. +This beast of a lemma defines and proves a nice induction principle for [coerce], *) Lemma coerce_nice_ind: forall (P : T -> T -> V -> V -> Prop), @@ -258,24 +262,19 @@ Lemma coerce_nice_ind: (case nullOptC, forall t, P NullT (OptT t) NullV NullV) -> (case optNullC, forall t1 t2, P (OptT t1) (OptT t2) NullV NullV) -> (case optSomeC, forall t1 t2 v1 v2, - t1 <: t2 -> v1 :: t1 -> P t1 t2 v1 v2 -> P (OptT t1) (OptT t2) (SomeV v1) (SomeV v2)) -> (case opportunisticOptC, forall t1 t2 v1, - ~ (t1 <: t2) -> + coerce t1 t2 v = None -> v1 :: t1 -> P (OptT t1) (OptT t2) (SomeV v1) NullV) -> (case reservedOptC, forall t, P ReservedT (OptT t) ReservedV NullV) -> (case constituentOptC, forall t1 t2 v1 v2, - (* The following assumption is redundant, as it follows from the - two subsequent onces, but it is convenient when using this - induction theorem *) is_opt_like_type t1 = false -> is_opt_like_type t2 = false -> - t1 <: t2 -> v1 :: t1 -> P t1 t2 v1 v2 -> P t1 (OptT t2) v1 (SomeV v2)) -> @@ -283,14 +282,15 @@ Lemma coerce_nice_ind: forall t1 t2 v1, v1 :: t1 -> is_opt_like_type t1 = false -> - is_opt_like_type t2 = true \/ ~ (t1 <: t2) -> + is_opt_like_type t2 = true \/ coerce t1 t2 v1 = None -> P t1 (OptT t2) v1 NullV) -> (case funcC, forall ta1 tr1 ta2 tr2 v, ta2 <: ta1 -> tr1 <: tr2 -> P (FuncT ta1 tr1) (FuncT ta2 tr2) (FuncV v) (FuncV v)) -> (case reservedC, forall t v, v :: t -> P t ReservedT v ReservedV) -> - (forall t1 t2 v1, t1 <: t2 -> v1 :: t1 -> P t1 t2 v1 (coerce t1 t2 v1)). + (forall t1 t2 v1, + 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. @@ -413,6 +413,8 @@ Proof. [reservedST]: { apply ReservedC; clear_names. named_constructor. } } Qed. +**) + (** * Properties of coercion @@ -422,8 +424,9 @@ Round-tripping Lemma coerce_roundtrip: forall t1 v1, v1 :: t1 -> - coerce t1 t1 v1 = v1. + coerce t1 t1 v1 = Some v1. Proof. +(** enough (forall t1 t2 v1, t1 <: t2 -> v1 :: t1 -> t2 = t1 -> coerce t1 t2 v1 = v1) @@ -435,6 +438,15 @@ Proof. inversion H1; subst; clear H1. contradiction H; apply ReflST; clear_names. } [reservedC]: { inversion H; subst; clear H; congruence. } +*) + intros t1 v1 HHT. + induction HHT; name_cases. all: simpl; try reflexivity. + + * rewrite IHHHT; reflexivity. + * (* This doesn’t work: The :: relation does not say anything about FuncV. + But including the type of the function in the FuncV makes types + and terms mutally recursive, so also not good. *) + Qed. (** From 2b71d78926b65720c05ab382708b35723633e0ff Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Sat, 19 Feb 2022 16:21:43 +0100 Subject: [PATCH 6/7] Some more experiments, but still not good --- coq/MiniCandid.v | 73 ++++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 61 insertions(+), 12 deletions(-) diff --git a/coq/MiniCandid.v b/coq/MiniCandid.v index 939a6ab15..ac80b6578 100644 --- a/coq/MiniCandid.v +++ b/coq/MiniCandid.v @@ -6,6 +6,7 @@ Require Import FunInd. Require Import Coq.ZArith.BinInt. Require Import Coq.Init.Datatypes. +Require Import Coq.Strings.String. Require Import Coq.Relations.Relation_Operators. Require Import Coq.Relations.Relation_Definitions. @@ -44,16 +45,17 @@ CoInductive T := Values are inductive. -We use an unspecified type to model refereneces (could have used [String] too) +Function reference values are modeled as a string, together with their “true type”. +Since they always have function type, we store the argument and result type. *) -Axiom RefV : Type. +Inductive Ref := MkRef : string -> T -> T -> Ref. Inductive V := | NatV : nat -> V | IntV : Z -> V | NullV : V | SomeV : V -> V - | FuncV : RefV -> V + | FuncV : Ref -> V | ReservedV : V . (** @@ -90,7 +92,7 @@ Inductive HasType : V -> T -> Prop := forall v t, v :: t -> SomeV v :: OptT t | FuncHT: case funcHT, - forall rv t1 t2, FuncV rv :: FuncT t1 t2 + forall rn t1 t2, FuncV (MkRef rn t1 t2) :: FuncT t1 t2 | ReservedHT: case reservedHT, ReservedV :: ReservedT @@ -440,24 +442,71 @@ Proof. [reservedC]: { inversion H; subst; clear H; congruence. } *) intros t1 v1 HHT. - induction HHT; name_cases. all: simpl; try reflexivity. - + induction HHT; name_cases. all: simpl; try rewrite subtype_dec_refl; try reflexivity. * rewrite IHHHT; reflexivity. - * (* This doesn’t work: The :: relation does not say anything about FuncV. - But including the type of the function in the FuncV makes types - and terms mutally recursive, so also not good. *) - Qed. (** -Coercion does not fail (and is well-defined) +Coercion does not fail on subtypes and well-typed values *) Lemma coerce_well_defined: forall t1 t2 v1, t1 <: t2 -> v1 :: t1 -> - coerce t1 t2 v1 :: t2. + coerce t1 t2 v1 <> None. Proof. + intros t1 t2 v1 HST HHT. + revert t2 HST. + induction HHT; name_cases; intros t3 HST; inversion HST. + all: try (simpl; congruence). + all: try (destruct t2; simpl; congruence). + * simpl; rewrite coerce_roundtrip; [|assumption]; congruence. + * simpl; destruct (coerce t t2 v) eqn:H2; try congruence. + * simpl; rewrite subtype_dec_refl; congruence. + * simpl. destruct t4;simpl; try congruence. + destruct (_ <:? _); congruence. + * simpl. destruct (_ <:? _); congruence. +Qed. + + +(** +Coercion returns well-typed values +*) + +Lemma coerce_well_typed: + forall t1 t2 v1 v2, v1 :: t1 -> + coerce t1 t2 v1 = Some v2 -> + v2 :: t2. +Proof. + intros t1 t2 v1 v2 HHT Heq. + revert t2 v2 Heq. + induction HHT; name_cases; intros t3 v3 Heq. + all: simpl in Heq; destruct t3; try congruence. + all: inversion Heq; clear Heq; try named_constructor. + + destruct t3; try congruence; + inversion H0; try named_constructor; try named_constructor. + + destruct t3; try congruence; + inversion H0; try named_constructor; try named_constructor. + + destruct (coerce t t3 v) eqn:Heq. + - specialize (IHHHT _ _ Heq). + inversion H0; clear H0. + named_constructor; assumption. + - inversion H0; clear H0; named_constructor. + + destruct t3; try congruence. + all: inversion H0; clear H0; try named_constructor; try named_constructor. + - destruct (FuncT t1 t2 <:? FuncT t3_1 t3_2) eqn:Hst. + * inversion H1; clear H1. + named_constructor. + (* This doesn’t quite work: Looks like :: needs to take <: into account in + the FuncT case *) + (* apply FuncHT. *) + admit. + + + + revert t1 t2 v2 Heq. + destruct t3; inversion Heq; try named_constructor. + * exact apply coerce_nice_ind with (P := fun t1 t2 v1 v2 => v2 :: t2); intros; name_cases; named_constructor; assumption. Qed. From 12da438bc82137f3057d681f98334ef036513eeb Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 7 Apr 2022 21:21:00 +0200 Subject: [PATCH 7/7] Introduce type environment for refs; a bit of progress --- coq/MiniCandid.v | 115 ++++++++++++++++++++++++++++------------------- 1 file changed, 68 insertions(+), 47 deletions(-) diff --git a/coq/MiniCandid.v b/coq/MiniCandid.v index ac80b6578..93c7fb162 100644 --- a/coq/MiniCandid.v +++ b/coq/MiniCandid.v @@ -45,10 +45,9 @@ CoInductive T := Values are inductive. -Function reference values are modeled as a string, together with their “true type”. -Since they always have function type, we store the argument and result type. +Function reference values are modeled as an abstract type. *) -Inductive Ref := MkRef : string -> T -> T -> Ref. +Axiom Ref : Type. Inductive V := | NatV : nat -> V @@ -73,30 +72,40 @@ Definition is_opt_like_type (t : T) : bool := end. -(** The boring, non-subtyping typing relation. *) -Inductive HasType : V -> T -> Prop := +(** The boring, non-subtyping typing relation. + +This is parametrized by a typing relation for references. +*) +Reserved Notation "G '|-' v ':::' T" (at level 80). + +Inductive HasType (G : Ref -> T -> T -> Prop) : V -> T -> Prop := | NatHT: case natHT, - forall n, NatV n :: NatT + forall n, + G |- NatV n ::: NatT | IntHT: case intHT, - forall n, IntV n :: IntT + forall n, + G |- IntV n ::: IntT | NullHT: case nullHT, - NullV :: NullT + G |- NullV ::: NullT | NullOptHT: case nullOptHT, - forall t, NullV :: OptT t + forall t, + G |- NullV ::: OptT t | OptHT: case optHT, - forall v t, v :: t -> SomeV v :: OptT t + forall v t, G |- v ::: t -> + G |- SomeV v ::: OptT t | FuncHT: case funcHT, - forall rn t1 t2, FuncV (MkRef rn t1 t2) :: FuncT t1 t2 + forall r t1 t2, G r t1 t2 -> + G |- FuncV r ::: FuncT t1 t2 | ReservedHT: case reservedHT, - ReservedV :: ReservedT -where "v :: t" := (HasType v t). + G |- ReservedV ::: ReservedT +where "G |- v ::: t" := (HasType G v t). (** The subtyping relation *) Reserved Infix "<:" (at level 80, no associativity). @@ -218,8 +227,8 @@ Function coerce (t1 : T) (t2 : T) (v1 : V) : option V := (* We can prove the desired equation at least as an equality *) Lemma coerce_constituent_eq: - forall v t1 t2, - v :: t1 -> + forall G v t1 t2, + G |- v ::: t1 -> is_opt_like_type t1 = false -> is_opt_like_type t2 = false -> coerce t1 (OptT t2) v = @@ -228,7 +237,7 @@ Lemma coerce_constituent_eq: | Some t => Some (SomeV t) end. Proof. - intros v t1 t2 HHT His_opt_like_t1 His_opt_like_t2. + intros G v t1 t2 HHT His_opt_like_t1 His_opt_like_t2. inversion HHT; subst; clear HHT; inversion His_opt_like_t1; clear His_opt_like_t1; name_cases. [natHT]: { destruct t2; subst; inversion His_opt_like_t2; clear His_opt_like_t2; simpl; try reflexivity. @@ -424,8 +433,8 @@ Qed. Round-tripping *) Lemma coerce_roundtrip: - forall t1 v1, - v1 :: t1 -> + forall G t1 v1, + G |- v1 ::: t1 -> coerce t1 t1 v1 = Some v1. Proof. (** @@ -441,7 +450,7 @@ Proof. } [reservedC]: { inversion H; subst; clear H; congruence. } *) - intros t1 v1 HHT. + intros G t1 v1 HHT. induction HHT; name_cases. all: simpl; try rewrite subtype_dec_refl; try reflexivity. * rewrite IHHHT; reflexivity. Qed. @@ -451,16 +460,16 @@ Coercion does not fail on subtypes and well-typed values *) Lemma coerce_well_defined: - forall t1 t2 v1, - t1 <: t2 -> v1 :: t1 -> + forall G t1 t2 v1, + t1 <: t2 -> G |- v1 ::: t1 -> coerce t1 t2 v1 <> None. Proof. - intros t1 t2 v1 HST HHT. + intros G t1 t2 v1 HST HHT. revert t2 HST. induction HHT; name_cases; intros t3 HST; inversion HST. all: try (simpl; congruence). all: try (destruct t2; simpl; congruence). - * simpl; rewrite coerce_roundtrip; [|assumption]; congruence. + * simpl. rewrite (coerce_roundtrip G _ _ HHT). congruence. * simpl; destruct (coerce t t2 v) eqn:H2; try congruence. * simpl; rewrite subtype_dec_refl; congruence. * simpl. destruct t4;simpl; try congruence. @@ -469,16 +478,21 @@ Proof. Qed. +Definition Ok_ref_env (G : Ref -> T -> T -> Prop) := + forall r ta1 tr1 ta2 tr2, + G r ta1 tr1 -> ta2 <: ta1 -> tr1 <: tr2 -> G r ta2 tr2. + (** Coercion returns well-typed values *) Lemma coerce_well_typed: - forall t1 t2 v1 v2, v1 :: t1 -> + forall G, Ok_ref_env G -> + forall t1 t2 v1 v2, G |- v1 ::: t1 -> coerce t1 t2 v1 = Some v2 -> - v2 :: t2. + G |- v2 ::: t2. Proof. - intros t1 t2 v1 v2 HHT Heq. + intros G HG t1 t2 v1 v2 HHT Heq. revert t2 v2 Heq. induction HHT; name_cases; intros t3 v3 Heq. all: simpl in Heq; destruct t3; try congruence. @@ -493,22 +507,26 @@ Proof. named_constructor; assumption. - inversion H0; clear H0; named_constructor. + destruct t3; try congruence. - all: inversion H0; clear H0; try named_constructor; try named_constructor. + all: inversion H1; clear H1; try named_constructor; try named_constructor. - destruct (FuncT t1 t2 <:? FuncT t3_1 t3_2) eqn:Hst. - * inversion H1; clear H1. + * inversion H2; clear H2. + named_constructor. named_constructor. (* This doesn’t quite work: Looks like :: needs to take <: into account in the FuncT case *) (* apply FuncHT. *) - admit. - - - - revert t1 t2 v2 Heq. - destruct t3; inversion Heq; try named_constructor. - * exact - apply coerce_nice_ind with (P := fun t1 t2 v1 v2 => v2 :: t2); intros; name_cases; - named_constructor; assumption. + inversion s; subst; clear s Hst. + ++ apply H. + ++ apply (HG _ _ _ _ _ H H4 H6). + * inversion H2; clear H2. + subst. + named_constructor. + + destruct (FuncT t1 t2 <:? FuncT t3_1 t3_2) eqn:Hst; try congruence. + inversion H1; subst; clear H1. + named_constructor. + inversion s; subst; clear s Hst. + ++ apply H. + ++ apply (HG _ _ _ _ _ H H3 H5). Qed. @@ -582,12 +600,12 @@ Fixpoint typ_idx' (p : Path) (t : T) : T := Properties about [val_idx] and [typ_idx'], mostly for sanity-checking *) Lemma path_preserves_types: - forall v v' t p, - v :: t -> + forall G v v' t p, + G |- v ::: t -> val_idx p v = Some v' -> - v' :: typ_idx' p t. + G |- v' ::: typ_idx' p t. Proof. - intros v v' t p. + intros G v v' t p. revert v v' t. induction p. * intros v v' t HHT Hval_idx. @@ -600,12 +618,12 @@ Proof. Qed. Lemma val_idx_is_val_idx': - forall v v' t p, - v :: t -> + forall G v v' t p, + G |- v ::: t -> val_idx p v = Some v' -> val_idx' p v = v'. Proof. - intros v v' t p. + intros G v v' t p. revert v v' t. induction p. * intros v v' t HHT Hval_idx. @@ -627,14 +645,17 @@ This may be proving a bit more than needed for compositionality, but it my be handy for other things. *) +(* TODO: Update to option-returning coerce + (although we know it can't be Null due to coerce_well_defined) *) + Lemma no_new_values: - forall t1 t2 v1, + forall G t1 t2 v1, t1 <: t2 -> - v1 :: t1 -> + G |- v1 ::: t1 -> forall p iv2, val_idx p (coerce t1 t2 v1) = Some iv2 -> (iv2 = NullV \/ typ_idx' p t1 <: typ_idx' p t2) /\ - val_idx' p v1 :: typ_idx' p t1 /\ + G |- val_idx' p v1 ::: typ_idx' p t1 /\ coerce (typ_idx' p t1) (typ_idx' p t2) (val_idx' p v1) = iv2. Proof. apply (coerce_nice_ind (fun t1 t2 v1 v2 =>