From 4a203f54752e0dc864f7947bbe0953ab8040dee1 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 20 Jan 2021 15:59:14 +0100 Subject: [PATCH 01/22] Spec: Do a subtyping check when decoding MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit this introduces a subtyping check * before even starting to decode * when decoding `opt` values. An implementation can probably pre-compute something at first, and then at each `opt` occurrence quickly look which way to go… With these changes, the coercion relation never fails on well-typed inputs, and it is anyways right-unique. I am wondering if it makes sense to rewrite it as a family of functions, indexed by the input and output types (like Andreas had it originally). --- spec/Candid.md | 60 ++++++++++++++++++++++++++------------------------ 1 file changed, 31 insertions(+), 29 deletions(-) diff --git a/spec/Candid.md b/spec/Candid.md index 5e4e11091..38979dbc7 100644 --- a/spec/Candid.md +++ b/spec/Candid.md @@ -884,20 +884,22 @@ 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 an abstract value, and then _coerced_ to 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. +In the following, we use `V` as an abstract data model of both the message in transit (`V`), as well as the result of the coercion (`V'`). We re-use the syntax of the textual representation. -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: +Since messages are self-describing, i.e. carry type description, the rules below can refer to the given type of the message using the `` syntax (i.e. `(v : t)`) if the type matters. This is used in particular + * To resolve overloading in number literals (``) + * To express the canonical value of type `reserved` as `(null : reserved)`. + * To do coercion-time subtyping checks in the rule for `opt` + +This section describes the coercion as a ternary relation `V ~> V' : T` to describe that 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. This relation is defined only when the type of `V` is a subtype of `T`. - * 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 ``. #### Primitive Types Values of primitive types coerce successfully at their own type: ``` --------------------------------------------------- -( : ) ~> ( : ) : +------------------------------------ +( : ) ~> : ------------------- true ~> true : bool @@ -909,20 +911,20 @@ false ~> false : bool ~> : text ------------------- -null ~> null : null +null ~> null : null ``` Values of type `nat` coerce successfully at type `int`: ``` --------------------------------- -( : nat) ~> ( : int) : int +------------------------ +( : nat) ~> : int ``` Any value coerces at type `reserved`, producing the canonical value of type `reserved`: ``` ------------------------------------ - ~> (null : reserved) : reserved +---------------------- + ~> null : reserved ``` NB: No rule is needed for type `empty`, because there are no values of that type. By construction, ` ~> _ : empty` will not hold. @@ -945,23 +947,23 @@ The null value coerce at any option type: null ~> null : opt ``` -An optional value coerces at an option type, if the constituent value coerces at the constituent type: +An optional value coerces at an option type, if the constituent value has a suitable type: ``` - ~> : ------------------------------ -opt ~> opt : opt + <: + ~> : +-------------------------------------- +opt ( : ) ~> opt : opt ``` -If an optional value _fails_ to coerce at an optional type, or the value is `reserved`, the result is `null`, not failure: +If an optional value does not have a subtype of the expected type, the result is `null`: ``` -not ( ~> _ : ) -------------------------- -opt ~> null : opt - ------------------------------------ -(null : reserved) ~> null : opt +not ( <: ) +---------------------------------- +opt ( : ) ~> null : opt ``` +NOTE: The two 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 @@ -973,7 +975,6 @@ opt ~> : opt ~> : opt ``` - #### Records Only records coerce at record type. Missing fields of option or reserved type turn into `null`. @@ -1000,7 +1001,7 @@ variant { = } ~> variant { = } : variant { = ; _;* #### References -Function and services references coerce unconditionally +Function and services references coerce unconditionally (note that coercion is only applied when the input value has a subtype of the expected type): ``` ------------------------------------------------------ @@ -1030,7 +1031,7 @@ 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. 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 roundtripping property below as its definition: * Correctness and completeness of decoding: ``` @@ -1066,7 +1067,7 @@ The relations above have certain properties. To express them, we need the relati T1 <: T2, T2 <: T3 ⇒ T1 <: T3 ``` -* Transitive coherence does not hold: +* NB: Transitive coherence does not hold: ``` T1 <: T2, T2 <: T3 v1 : T1 @@ -1299,9 +1300,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 `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 relation `(,*) ~> (,*) : (,*)` to try to understand the decoded values at the expected type. + * use the coercion relation `(,*) ~> (,*) : (,*)` to understand the decoded values at the expected type. ### Deserialisation of future types From ecb3f95ebe1254fc25de7f98ded54ff85d2be557 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 20 Jan 2021 16:30:31 +0100 Subject: [PATCH 02/22] Update spec/Candid.md Co-authored-by: Andreas Rossberg --- spec/Candid.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/Candid.md b/spec/Candid.md index 38979dbc7..d5ecf2b18 100644 --- a/spec/Candid.md +++ b/spec/Candid.md @@ -886,7 +886,7 @@ This subtyping is implemented during the deserialisation of Candid at an expecte In the following, we use `V` as an abstract data model of both the message in transit (`V`), as well as the result of the coercion (`V'`). We re-use the syntax of the textual representation. -Since messages are self-describing, i.e. carry type description, the rules below can refer to the given type of the message using the `` syntax (i.e. `(v : t)`) if the type matters. This is used in particular +Since messages are self-describing, i.e. carry a type description, the rules below can refer to the given type of the message using the `` syntax (i.e. `(v : t)`) if the type matters. This is used in particular * To resolve overloading in number literals (``) * To express the canonical value of type `reserved` as `(null : reserved)`. * To do coercion-time subtyping checks in the rule for `opt` From cbe840e6355040eb6766dbc49af1280f2fc0a6aa Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Tue, 26 Jan 2021 16:09:34 +0100 Subject: [PATCH 03/22] Rewrite using a coercion function --- spec/Candid.md | 167 +++++++++++++++++-------------------------------- 1 file changed, 58 insertions(+), 109 deletions(-) diff --git a/spec/Candid.md b/spec/Candid.md index d5ecf2b18..90bc25952 100644 --- a/spec/Candid.md +++ b/spec/Candid.md @@ -882,140 +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. -In the following, we use `V` as an abstract data model of both the message in transit (`V`), as well as the result of the coercion (`V'`). We re-use the syntax of the textual representation. - -Since messages are self-describing, i.e. carry a type description, the rules below can refer to the given type of the message using the `` syntax (i.e. `(v : t)`) if the type matters. This is used in particular - * To resolve overloading in number literals (``) - * To express the canonical value of type `reserved` as `(null : reserved)`. - * To do coercion-time subtyping checks in the rule for `opt` - -This section describes the coercion as a ternary relation `V ~> V' : T` to describe that 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. This relation is defined only when the type of `V` is a subtype of `T`. +To model this, we defined, for every `t1, t2` with `t1 <: t2`, the function `c[t1<:t2] : t1 -> t2`. This function maps values of type `t1` to values of type `t2`, and is indeed total. +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 +c[nat <: int](x) = x ``` -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 +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: -``` ----------------------- -null ~> null : opt -``` - -An optional value coerces at an option type, if the constituent value has a suitable type: +The null type coerces into any option type: ``` - <: - ~> : --------------------------------------- -opt ( : ) ~> opt : opt +c[null <: opt ](null) = null ``` -If an optional value does not have a subtype of the expected type, the result is `null`: +An optional value coerces at an option type, if the constituent value has a suitable type, and else goes to `null`: ``` -not ( <: ) ----------------------------------- -opt ( : ) ~> null : opt +c[opt <: opt ](null) = null +c[opt <: opt ](opt ) = opt c[ <: ](v') if <: +c[opt <: opt ](opt ) = null if not( <: ) ``` -NOTE: The two rules above imply that a Candid decoder has to be able to decide the subtyping relation at runtime. +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 (note that coercion is only applied when the input value has a subtype of the expected type): - -``` ------------------------------------------------------- -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 @@ -1023,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 roundtripping 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 + <: , <: ``` - -* NB: 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 relation `R` that satisfies `∀ v. R(opt v, null)`. + However, it implies + ``` + c[ <: ] ⊒ c[ <: ] ⚬ c[ <: ] + ``` + where ⊒ is the smallest homomorphic, reflexive relation `R` that satisfies `∀ v. R(opt v, null)`. The goal of “subtyping completeness” has not been cast into a formal formulation yet. @@ -1302,8 +1251,8 @@ 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 `(,*)` * check that `(,*) <: (,*)`, else fail - * using the inverse of the `M` function, indexed by `(*)`, to decode the values `(*)` - * use the coercion relation `(,*) ~> (,*) : (,*)` to understand the decoded values at the expected type. + * 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 From d49cbfe80b7aedccc2b85ea301bc6629de6c5378 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Tue, 26 Jan 2021 16:14:36 +0100 Subject: [PATCH 04/22] Typos --- spec/Candid.md | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/spec/Candid.md b/spec/Candid.md index 90bc25952..d54948029 100644 --- a/spec/Candid.md +++ b/spec/Candid.md @@ -923,17 +923,17 @@ 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 ](opt ) = opt c[ <: ](v) if <: +c[opt <: opt ](opt ) = null if not( <: ) ``` 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: ``` -c[ <: opt ]() = opt c[ <: ](v') if not (null <: ) and <: -c[ <: opt ]() = null if not (null <: ) and not ( <: ) -c[reserved <: opt ]() = null +c[ <: opt ]() = opt c[ <: ](v) if not (null <: ) and <: +c[ <: opt ](_) = null if not (null <: ) and not ( <: ) +c[reserved <: opt ](_) = null ``` #### Records @@ -946,7 +946,7 @@ In the following rule: ``` c[record { = ;* = ;* } <: record { = ;* = ;* }](record { = ;* = ;* }) - = record { = c[ <: ]();* = null;* } + = record { = c[ <: ]();* = null;* } ``` #### Variants From 942bbb6dbf7edcce18c4d529e0ed571b481a735b Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 27 Jan 2021 11:29:55 +0100 Subject: [PATCH 05/22] Coq: Model subtype check on decoding this models #168 in Coq. So far so good. The crucial bit will be connecting this to the IDL Soundness formalization. That requires * adding a function reference type * proving a subtyping-compositionality lemma, namely ``` If t1 <: t2 and s1 in t1 <: s2 in t2 then s1 <: s2. ``` That will be no small untertaking. I will probably remove the other variants in the Coq file then? --- coq/MiniCandid.v | 226 +++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 219 insertions(+), 7 deletions(-) diff --git a/coq/MiniCandid.v b/coq/MiniCandid.v index 6d111c31d..391b61dda 100644 --- a/coq/MiniCandid.v +++ b/coq/MiniCandid.v @@ -11,6 +11,8 @@ Require Import Coq.Relations.Relation_Operators. Require Import Coq.Relations.Relation_Definitions. Require Import Coq.Relations.Operators_Properties. +Require Import Coq.Logic.Decidable. + Set Bullet Behavior "Strict Subproofs". Set Default Goal Selector "!". @@ -87,10 +89,10 @@ Here things are simple and inductive. Reserved Infix "<:" (at level 80, no associativity). CoInductive Subtype : T -> T -> Prop := | ReflST : - case reflSL, + case reflST, forall t, t <: t | NatIntST : - case natIntSL, + case natIntST, NatT <: IntT | NullOptST : case nullOptST, @@ -198,7 +200,7 @@ Proof. inversion H0; subst; clear H0; simpl in H; inversion H. econstructor. named_econstructor; [constructor|named_constructor]. } - [optHT_reflSL]: { + [optHT_reflST]: { specialize (IHHvT t (ReflST _ _)). destruct IHHvT as [v2 Hv2]. eexists. named_econstructor; try eassumption. @@ -232,7 +234,7 @@ Proof. inversion H2; subst; clear H2; name_cases; try (constructor; easy). - [natIntSL_constituentOptST]: { + [natIntST_constituentOptST]: { named_constructor. - assumption. - eapply Hyp; [named_econstructor | assumption]. @@ -268,10 +270,10 @@ This is the variant with the opportunistic `t <: opt t'` rule. Reserved Infix "<:" (at level 80, no associativity). CoInductive Subtype : T -> T -> Prop := | ReflST : - case reflSL, + case reflST, forall t, t <: t | NatIntST : - case natIntSL, + case natIntST, NatT <: IntT | OptST : case optST, @@ -285,6 +287,212 @@ CoInductive Subtype : T -> T -> Prop := forall t, t <: ReservedT where "t1 <: t2" := (Subtype t1 t2). +Module SubtypeCheck. +(* +This is the variant with the subtyping check during decoding. +*) + +(* +Subtyping is undecidable, at least the way we model it in Coq. +So let’s pretend it is. +*) +Axiom subtyping_decidable: + forall t1 t2, {t1 <: t2} + { ~(t1 <: t2) }. +Infix "<:?" := subtyping_decidable (at level 80, no associativity). + +(* +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 RHS of invalid cases. +*) + +Function coerce (t1 : T) (t2 : T) (v1 : V) : 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) + + | SomeV v, OptT t1, OptT t2 => + if t1 <:? t2 + then SomeV (coerce t1 t2 v) + else NullV + + (* This is the rule we would like to have, but + in order to please the termination checker, + we have to duplicate all non-opt rules in their opt variant + | v, t1, OptT t2 => + if not (is_opt_like_type t) && t <: t2 + then SomeV (coerce v t1 t2) + *) + | 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)) + + | v, t, ReservedT => ReservedV + + (* Failure is NullV. This also subsumes “valid” rules for NullV *) + | _, _, _ => NullV + end. + + +(* Let’s try to create a suitable induction principle for this function *) +Lemma coerce_nice_ind: + forall (P : T -> T -> V -> V -> Prop), + (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 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) -> + (case optSomeC, forall t1 t2 v1 v2, + t1 <: t2 -> + P t1 t2 v1 v2 -> + P (OptT t1) (OptT t2) (SomeV v1) (SomeV v2)) -> + (case opportunisticOptC, forall t1 t2 v1, + ~ (t1 <: t2) -> + 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, + is_opt_like_type t1 = false -> + is_opt_like_type t2 = false -> + t1 <: t2 -> + P t1 t2 v1 v2 -> + P t1 (OptT t2) v1 (SomeV v2)) -> + (case opportunisticConstituentOptC, + forall t1 t2 v1, + is_opt_like_type t1 = false -> + is_opt_like_type t2 = true \/ ~ (t1 <: t2) -> + P t1 (OptT t2) v1 NullV) -> + (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)). +Proof. + intros P. + intros NatC IntC NatIntC NullC NullOptC OptNullC OptSomeC OpportunisticOptC ReservedOptC ConstituentOptC OpportunisticConstituentOptC ReservedC. + intros t1 t2 v1 HST HHT. + revert t2 HST. + induction HHT; name_cases. + [natHT]: { + intros. + inversion HST; subst; clear HST; name_cases. + [reflST]: { apply NatC; clear_names. } + [natIntST]: { apply NatIntC; 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. + * destruct (subtyping_decidable NatT t0). + + 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. + - contradict n0. named_constructor. + - contradict n0. named_constructor. + - apply OpportunisticConstituentOptC; clear_names; simpl; intuition. + } + [reservedST]: { apply ReservedC; clear_names. named_constructor. } + } + [intHT]: { + intros. + inversion HST; subst; clear HST; name_cases. + [reflST]: { apply IntC; 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. + * destruct (subtyping_decidable IntT t0). + + 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. + - contradict n0. named_constructor. + - apply OpportunisticConstituentOptC; clear_names; simpl; intuition. + } + [reservedST]: { apply ReservedC; clear_names. named_constructor. } + } + [nullHT]: { + intros. + inversion HST; subst; clear HST; name_cases. + [reflST]: { apply NullC; clear_names. } + [optST]: { apply NullOptC; clear_names. } + [reservedST]: { apply ReservedC; clear_names. named_constructor. } + } + [nullOptHT]: { + intros. + inversion HST; subst; clear HST; name_cases. + [reflST]: { apply OptNullC; clear_names. } + [optST]: { apply OptNullC; clear_names. } + [reservedST]: { apply ReservedC; clear_names. named_constructor. } + } + [optHT]: { + intros. + inversion HST; subst; clear HST; name_cases. + [reflST]: { + simpl. + destruct (t <:? t) as [HST | HNoST]. + * apply OptSomeC; clear_names; intuition. + * contradict HNoST. apply ReflST; clear_names. + } + [optST]: { + simpl. + destruct (t <:? t0) as [HST | HNoST]. + * apply OptSomeC; clear_names; intuition. + * apply OpportunisticOptC; clear_names; intuition. + } + [reservedST]: { apply ReservedC; clear_names. named_constructor; assumption. } + } + [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. } + } +Qed. + +Lemma coerce_roundtrip: + forall t1 v1, + v1 :: t1 -> + coerce t1 t1 v1 = v1. +Proof. + enough (forall t1 t2 v1, + t1 <: t2 -> v1 :: t1 -> t2 = t1 -> + coerce t1 t2 v1 = v1) + by (intros; apply H; intuition; try apply ReflST; clear_names). + apply (coerce_nice_ind (fun t1 t2 v1 v2 => t2 = t1 -> v2 = v1)); + intros; name_cases; subst; simpl in *; try congruence. + Show Existentials. + [optSomeC]: {apply f_equal. apply H0. congruence. } + [opportunisticOptC]: { + inversion H0; subst; clear H0. contradiction H; apply ReflST; clear_names. + } + * (* why is this not named? *) + inversion H; subst; clear H. reflexivity. +Qed. + +Lemma coerce_well_defined: + forall t1 t2 v1, + t1 <: t2 -> v1 :: t1 -> + coerce t1 t2 v1 :: t2. +Proof. + apply coerce_nice_ind with (P := fun t1 t2 v1 v2 => v2 :: t2); intros; name_cases; + named_constructor; assumption. +Qed. + + + +End SubtypeCheck. + + +Module TypeErasure. +(* +This is the variant with type erasure, and dynamic opportnistic decoding. +Not safe in the higher-order case. +*) + (* The coercion relation is not strictly positive, and thus can’t be an inductive relations, so we have to implement it as a function that recurses on the value. @@ -317,6 +525,7 @@ Function coerce (v1 : V) (t : T) : option V := | NatV n, OptT NatT => recover (Some (NatV n)) | IntV n, OptT IntT => recover (Some (IntV n)) | NatV n, OptT IntT => recover (Some (IntV (Z.of_nat n))) + (* OptT never fails (this subsumes NullV and ReservedV) *) | v, OptT _ => Some NullV @@ -510,7 +719,7 @@ Proof. [intHT_optST]: { destruct t2; eexists; reflexivity. } - [optHT_reflSL]: { + [optHT_reflST]: { specialize (IHHvT t (ReflST _ _)). destruct IHHvT as [v2 Hv2]. eexists. unfold Coerces in *. simpl. rewrite Hv2. reflexivity. @@ -539,4 +748,7 @@ Proof. try (constructor; easy). Qed. +End TypeErasure. + + End OpportunisticDecoding. \ No newline at end of file From 4558d0f9301bb0dde0c0fa78c802068ffa472286 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 27 Jan 2021 11:39:44 +0100 Subject: [PATCH 06/22] Cleanup --- coq/MiniCandid.v | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/coq/MiniCandid.v b/coq/MiniCandid.v index 391b61dda..8ae619d40 100644 --- a/coq/MiniCandid.v +++ b/coq/MiniCandid.v @@ -463,8 +463,7 @@ Proof. coerce t1 t2 v1 = v1) by (intros; apply H; intuition; try apply ReflST; clear_names). apply (coerce_nice_ind (fun t1 t2 v1 v2 => t2 = t1 -> v2 = v1)); - intros; name_cases; subst; simpl in *; try congruence. - Show Existentials. + intros; name_cases; subst; simpl in *; try solve [congruence]. [optSomeC]: {apply f_equal. apply H0. congruence. } [opportunisticOptC]: { inversion H0; subst; clear H0. contradiction H; apply ReflST; clear_names. @@ -712,7 +711,6 @@ Proof. induction HvT; intros t1 Hsub; inversion Hsub; subst; clear Hsub; name_cases; try (eexists;reflexivity). - Show Existentials. [natHT_optST]: { destruct t2; eexists; reflexivity. } From d904d417a1cbfbe252851f819c519bbc7a10702f Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 27 Jan 2021 12:13:13 +0100 Subject: [PATCH 07/22] Add FuncT (and memove the other formalizations) --- coq/MiniCandid.v | 516 +++++++---------------------------------------- 1 file changed, 71 insertions(+), 445 deletions(-) diff --git a/coq/MiniCandid.v b/coq/MiniCandid.v index 8ae619d40..694a9c76c 100644 --- a/coq/MiniCandid.v +++ b/coq/MiniCandid.v @@ -26,15 +26,20 @@ CoInductive T := | IntT: T | NullT : T | OptT : T -> T + | FuncT : T -> T -> T | VoidT : T | ReservedT : T . +(* Some unspecified value representation for references *) +Axiom RefV : Type. + Inductive V := | NatV : nat -> V | IntV : Z -> V | NullV : V | SomeV : V -> V + | FuncV : RefV -> V | ReservedV : V . @@ -73,19 +78,15 @@ Inductive HasType : V -> T -> Prop := | OptHT: case optHT, forall v t, v :: t -> SomeV v :: OptT t + | FuncHT: + case funcHT, + forall rv t1 t2, FuncV rv :: FuncT t1 t2 | ReservedHT: case reservedHT, ReservedV :: ReservedT where "v :: t" := (HasType v t). -Module NoOpportunisticDecoding. - -(* -This is the variant without `t <: opt t'`, but with `t <: opt t`. -Here things are simple and inductive. -*) - Reserved Infix "<:" (at level 80, no associativity). CoInductive Subtype : T -> T -> Prop := | ReflST : @@ -94,21 +95,16 @@ CoInductive Subtype : T -> T -> Prop := | NatIntST : case natIntST, NatT <: IntT - | NullOptST : - case nullOptST, - forall t, NullT <: OptT t | OptST : case optST, forall t1 t2, - (* This additional restriction added to fix https://github.com/dfinity/candid/issues/146 *) - (is_opt_like_type t1 = is_opt_like_type t2) -> - t1 <: t2 -> - OptT t1 <: OptT t2 - | ConstituentOptST : - case constituentOptST, - forall t1 t2, - is_opt_like_type t2 = false -> - t1 <: t2 -> t1 <: OptT t2 + t1 <: OptT t2 + | FuncST : + case funcST, + forall ta1 ta2 tr1 tr2, + ta2 <: ta1 -> + tr1 <: tr2 -> + FuncT ta1 tr1 <: FuncT ta2 tr2 | VoidST : case voidST, forall t, VoidT <: t @@ -118,113 +114,9 @@ CoInductive Subtype : T -> T -> Prop := where "t1 <: t2" := (Subtype t1 t2). -Reserved Notation "v1 ~> v2 :: t" (at level 80, v2 at level 50, no associativity). -Inductive Coerces : V -> V -> T -> Prop := - | NatC: - case natC, - forall n, NatV n ~> NatV n :: NatT - | IntC: - case intC, - forall n, IntV n ~> IntV n :: IntT - | NatIntC: - case natIntC, - forall n i, i = Z.of_nat n -> (NatV n ~> IntV i :: IntT) - | NullC: - case nullC, - NullV ~> NullV :: NullT - | NullOptC: - case nullOptC, - forall t, NullV ~> NullV :: OptT t - | SomeOptC: - case someOptC, - forall v1 v2 t, - v1 ~> v2 :: t -> - SomeV v1 ~> SomeV v2 :: OptT t - | ConstituentOptC: - case constituentC, - forall v1 v2 t, - is_not_opt_like_value v1 -> - v1 ~> v2 :: t -> - v1 ~> SomeV v2 :: OptT t - | ReservedC: - case reservedC, - forall v1, - v1 ~> ReservedV :: ReservedT -where "v1 ~> v2 :: t" := (Coerces v1 v2 t). - -Lemma is_opt_like_type_correct: - forall t, - is_opt_like_type t = true <-> NullT <: t. -Proof. - intros. destruct t; simpl; intuition. - all: try inversion H. - all: try named_constructor. -Qed. - -Theorem coercion_correctness: - forall v1 v2 t, v1 ~> v2 :: t -> v2 :: t. -Proof. - intros. induction H; constructor; assumption. -Qed. - -Theorem coercion_roundtrip: - forall v t, v :: t -> v ~> v :: t. -Proof. - intros. induction H; constructor; intuition. -Qed. - -Theorem coercion_uniqueness: - forall v v1 v2 t, v ~> v1 :: t -> v ~> v2 :: t -> v1 = v2. -Proof. - intros. - revert v2 H0. - induction H; intros v2' Hother; - try (inversion Hother; subst; clear Hother; try congruence; firstorder congruence). -Qed. - -Theorem soundness_of_subtyping: - forall t1 t2, - t1 <: t2 -> - forall v1, v1 :: t1 -> exists v2, v1 ~> v2 :: t2. -Proof. - intros t1 t2 Hsub v HvT. revert t2 Hsub. - induction HvT; intros t1 Hsub; inversion Hsub; subst; clear Hsub; - name_cases; - try (eexists;constructor; try constructor; fail). - [natHT_constituentOptST]: { - inversion H0; subst; clear H0; simpl in H; inversion H. - - eexists. named_constructor; [constructor|named_constructor]. - - eexists. named_constructor; [constructor|named_constructor;reflexivity]. - } - [intHT_constituentOptST]: { - inversion H0; subst; clear H0; simpl in H; inversion H. - econstructor. named_econstructor; [constructor|named_constructor]. - } - [optHT_reflST]: { - specialize (IHHvT t (ReflST _ _)). - destruct IHHvT as [v2 Hv2]. - eexists. named_econstructor; try eassumption. - } - [optHT_optST]: { - specialize (IHHvT _ H1). - destruct IHHvT as [v2 Hv2]. - eexists; named_econstructor; eassumption. - } - [optHT_constituentOptST]: { - inversion H0; subst; clear H0; simpl in H; inversion H. - } - [reservedHT_constituentOptST]: { - inversion H0; subst; clear H0; simpl in H; inversion H. - } -Qed. - Theorem subtyping_refl: reflexive _ Subtype. Proof. intros x. apply ReflST; constructor. Qed. -Lemma is_not_opt_like_type_contravariant: - forall t1 t2, - is_opt_like_type t1 = false -> t2 <: t1 -> is_opt_like_type t2 = false. -Proof. intros. destruct t1, t2; easy. Qed. Theorem subtyping_trans: transitive _ Subtype. Proof. @@ -233,65 +125,9 @@ Proof. inversion H1; subst; clear H1; inversion H2; subst; clear H2; name_cases; - try (constructor; easy). - [natIntST_constituentOptST]: { - named_constructor. - - assumption. - - eapply Hyp; [named_econstructor | assumption]. - } - [optST_optST0]: { - named_constructor. - - congruence. - - eapply Hyp; eassumption. - } - [optST_constituentOptST]: { - inversion H3; subst; clear H3; simpl in H1; congruence. - } - [constituentOptST_optST]: { - named_constructor. - - congruence. - - firstorder. - } - [constituentOptST_constituentOptST0]: { - inversion H3; subst; clear H3; try easy. - } - [reservedST_constituentOptST]: { - inversion H0; subst; clear H0; inversion H. - } + try (constructor; firstorder). Qed. -End NoOpportunisticDecoding. - -Module OpportunisticDecoding. -(* -This is the variant with the opportunistic `t <: opt t'` rule. -*) - -Reserved Infix "<:" (at level 80, no associativity). -CoInductive Subtype : T -> T -> Prop := - | ReflST : - case reflST, - forall t, t <: t - | NatIntST : - case natIntST, - NatT <: IntT - | OptST : - case optST, - forall t1 t2, - t1 <: OptT t2 - | VoidST : - case voidST, - forall t, VoidT <: t - | ReservedST : - case reservedST, - forall t, t <: ReservedT -where "t1 <: t2" := (Subtype t1 t2). - -Module SubtypeCheck. -(* -This is the variant with the subtyping check during decoding. -*) - (* Subtyping is undecidable, at least the way we model it in Coq. So let’s pretend it is. @@ -300,6 +136,19 @@ Axiom subtyping_decidable: forall t1 t2, {t1 <: t2} + { ~(t1 <: t2) }. Infix "<:?" := subtyping_decidable (at level 80, no associativity). + +Lemma subtype_dec_true: + forall T t1 t2 (x y : T), t1 <: t2 -> (if t1 <:? t2 then x else y) = x. +Proof. intros. destruct (t1 <:? t2); intuition. Qed. + +Lemma subtype_dec_false: + forall T t1 t2 (x y : T), ~ (t1 <: t2) -> (if t1 <:? t2 then x else y) = y. +Proof. intros. destruct (t1 <:? t2); intuition. Qed. + +Lemma subtype_dec_refl: + forall T t (x y : T), (if t <:? t then x else y) = x. +Proof. intros. apply subtype_dec_true. named_constructor. Qed. + (* The spec defines the coercion function as indexed by the subtyping relation. But that relation is coinductive, so Coq will not allow that. @@ -313,6 +162,7 @@ Function coerce (t1 : T) (t2 : T) (v1 : V) : V := | 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 | SomeV v, OptT t1, OptT t2 => if t1 <:? t2 @@ -329,6 +179,9 @@ Function coerce (t1 : T) (t2 : T) (v1 : V) : V := | 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)) + | FuncV r, FuncT ta1 tr1, OptT (FuncT ta2 tr2) => + if ta2 <:? ta1 + then if tr1 <:? tr2 then SomeV (FuncV r) else NullV else NullV | v, t, ReservedT => ReservedV @@ -367,11 +220,15 @@ Lemma coerce_nice_ind: is_opt_like_type t1 = false -> is_opt_like_type t2 = true \/ ~ (t1 <: t2) -> 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)). Proof. intros P. - intros NatC IntC NatIntC NullC NullOptC OptNullC OptSomeC OpportunisticOptC ReservedOptC ConstituentOptC OpportunisticConstituentOptC ReservedC. + intros NatC IntC NatIntC NullC NullOptC OptNullC OptSomeC OpportunisticOptC ReservedOptC ConstituentOptC OpportunisticConstituentOptC FuncC ReservedC. intros t1 t2 v1 HST HHT. revert t2 HST. induction HHT; name_cases. @@ -392,6 +249,7 @@ Proof. - contradict n0. named_constructor. - contradict n0. named_constructor. - apply OpportunisticConstituentOptC; clear_names; simpl; intuition. + - apply OpportunisticConstituentOptC; clear_names; simpl; intuition. } [reservedST]: { apply ReservedC; clear_names. named_constructor. } } @@ -410,7 +268,39 @@ Proof. - apply OpportunisticConstituentOptC; clear_names; simpl; intuition. - contradict n0. named_constructor. - apply OpportunisticConstituentOptC; clear_names; simpl; intuition. + - apply OpportunisticConstituentOptC; clear_names; simpl; intuition. + } + [reservedST]: { apply ReservedC; clear_names. named_constructor. } + } + [funcHT]: { + intros. + inversion HST; subst; clear HST; name_cases. + [reflST]: { apply FuncC; clear_names; apply ReflST; clear_names. } + [optST]: { + destruct (is_opt_like_type t4) eqn:His_opt_like. + * destruct t4; inversion His_opt_like; simpl; clear His_opt_like; + apply OpportunisticConstituentOptC; clear_names; simpl; intuition. + * destruct (subtyping_decidable (FuncT t1 t2) t4). + + destruct t4; inversion s; subst; clear s; inversion His_opt_like; clear His_opt_like. + - simpl. repeat rewrite subtype_dec_refl. + apply ConstituentOptC; clear_names; simpl; try (intuition;fail). + ** apply ReflST; clear_names; apply ReflST; clear_names. + ** apply FuncC; clear_names; apply ReflST; clear_names. + - simpl. repeat rewrite subtype_dec_true by assumption. + apply ConstituentOptC; clear_names; simpl; try (intuition;fail). + named_constructor; assumption. + + destruct t4; inversion His_opt_like; clear His_opt_like. + - apply OpportunisticConstituentOptC; clear_names; simpl; intuition. + - apply OpportunisticConstituentOptC; clear_names; simpl; intuition. + - simpl. + destruct (t4_1 <:? t1). + ** destruct (t2 <:? t4_2). + ++ contradict n. named_constructor; assumption. + ++ apply OpportunisticConstituentOptC; clear_names; simpl; intuition. + ** apply OpportunisticConstituentOptC; clear_names; simpl; intuition. + - apply OpportunisticConstituentOptC; clear_names; simpl; intuition. } + [funcST]: { apply FuncC; clear_names; assumption. } [reservedST]: { apply ReservedC; clear_names. named_constructor. } } [nullHT]: { @@ -482,271 +372,7 @@ Proof. Qed. - -End SubtypeCheck. - - -Module TypeErasure. -(* -This is the variant with type erasure, and dynamic opportnistic decoding. -Not safe in the higher-order case. -*) - -(* -The coercion relation is not strictly positive, and thus can’t be an inductive -relations, so we have to implement it as a function that recurses on the value. - -This is essentially coercion function, and we can separately try to prove that -it corresponds to the relation. - *) - -Definition recover x := match x with - | None => Some NullV - | Some x => Some (SomeV x) - end. - -Function coerce (v1 : V) (t : T) : option V := - match v1, t with - | NatV n, NatT => Some (NatV n) - | IntV n, IntT => Some (IntV n) - | NatV n, IntT => Some (IntV (Z.of_nat n)) - | NullV, NullT => Some NullV - | SomeV v, OptT t => recover (coerce v t) - - (* This is the rule we would like to have, but - in order to please the termination checker, - we have to duplicate all non-opt rules in their opt variant - | v, OptT t => - if is_opt_like_type t - then None - else option_map SomeV (coerce n v t) - *) - | NatV n, OptT NatT => recover (Some (NatV n)) - | IntV n, OptT IntT => recover (Some (IntV n)) - | NatV n, OptT IntT => recover (Some (IntV (Z.of_nat n))) - - (* OptT never fails (this subsumes NullV and ReservedV) *) - | v, OptT _ => Some NullV - - | v, ReservedT => Some ReservedV - | v, t => None - end. - -Definition Coerces (v1 v2 : V) (t : T) : Prop := coerce v1 t = Some v2. -Notation "v1 ~> v2 :: t" := (Coerces v1 v2 t) (at level 80, v2 at level 50, no associativity). - -Definition DoesNotCoerce (v1 : V) (t : T) : Prop := coerce v1 t = None. -Notation "v1 ~/> :: t" := (DoesNotCoerce v1 t) (at level 80, no associativity). - -(* -Now we can prove that this indeed implements the inductive relation in the spec: -*) - -Lemma NatC: forall n, NatV n ~> NatV n :: NatT. -Proof. intros. reflexivity. Qed. - -Lemma IntC: forall n, IntV n ~> IntV n :: IntT. -Proof. intros. reflexivity. Qed. - -Lemma NatIntC: forall n i, i = Z.of_nat n -> NatV n ~> IntV i :: IntT. -Proof. intros. subst. reflexivity. Qed. - -Lemma NullC: NullV ~> NullV :: NullT. -Proof. intros. reflexivity. Qed. - -Lemma NullOptC: forall t, NullV ~> NullV :: OptT t. -Proof. intros. reflexivity. Qed. - -Lemma SomeOptC: forall v1 v2 t, - v1 ~> v2 :: t -> - SomeV v1 ~> SomeV v2 :: OptT t. -Proof. unfold Coerces. intros. simpl. rewrite H. reflexivity. Qed. - -Lemma OpportunisticOptC: - forall v1 t, - v1 ~/> :: t -> - SomeV v1 ~> NullV :: OptT t. -Proof. - unfold Coerces; unfold DoesNotCoerce. simpl. intros. - rewrite H; reflexivity. -Qed. - -Lemma ReservedOptC: - forall t, ReservedV ~> NullV :: OptT t. -Proof. intros. reflexivity. Qed. - -Lemma ConstituentOptC: - forall v1 v2 t, - is_not_opt_like_value v1 -> - is_opt_like_type t = false -> - v1 ~> v2 :: t -> - v1 ~> SomeV v2 :: OptT t. -Proof. - unfold Coerces. simpl. intros. - destruct v1, t; simpl in *; try contradiction; try congruence. -Qed. - -Lemma OpportunisticConstituentOptC: - forall v1 t, - is_not_opt_like_value v1 -> - is_opt_like_type t = false -> - v1 ~/> :: t -> - v1 ~> NullV :: OptT t. -Proof. - unfold Coerces; unfold DoesNotCoerce. simpl. intros. - destruct v1, t; simpl in *; try contradiction; try congruence. -Qed. - -Lemma ReservedC: forall v, v ~> ReservedV :: ReservedT. -Proof. unfold Coerces. intros. destruct v; reflexivity. Qed. - -(* -Now the induction theorem. As always, ugly and bit. -Note that negative assumptions don’t give you a P predicate. -*) - -Lemma Coerces_ind: - forall P, - (case natC, forall n, P (NatV n) (NatV n) NatT) -> - (case intC, forall n, P (IntV n) (IntV n) IntT) -> - (case natIntC, forall n, P (NatV n) (IntV (Z.of_nat n)) IntT) -> - (case nullC, P NullV NullV NullT) -> - (case nullOptC, forall t, P NullV NullV (OptT t)) -> - (case someOptC, forall v1 v2 t, - v1 ~> v2 :: t -> P v1 v2 t -> P (SomeV v1) (SomeV v2) (OptT t)) -> - (case opportunisticOptC, - forall v1 t, v1 ~/> :: t -> P (SomeV v1) NullV (OptT t)) -> - (case reservedOptC, - forall t, P ReservedV NullV (OptT t)) -> - (case constituentOptC, - forall v1 v2 t, - is_not_opt_like_value v1 -> - is_opt_like_type t = false -> - v1 ~> v2 :: t -> - P v1 v2 t -> - P v1 (SomeV v2) (OptT t)) -> - (case opportunisticConstituentOptC, - forall v1 t, - is_not_opt_like_value v1 -> - is_opt_like_type t = true \/ v1 ~/> :: t -> - P v1 NullV (OptT t)) -> - (case reservedC, forall v, P v ReservedV ReservedT) -> - (forall v1 v2 t, v1 ~> v2 :: t -> P v1 v2 t). -Proof. - unfold Coerces. unfold DoesNotCoerce. - intros P NatC IntC NatIntC NullC NullOptC SomeOptC OpportunisticOptC ReservedOptC ConstituentOptC OpportunisticConstituentOptC ReservedC v1. - induction v1; intros v2 t Hcoerces; destruct t. - all: try (inversion Hcoerces; subst; clear Hcoerces; intuition; fail). - all: simpl in Hcoerces. - * destruct t; - inversion Hcoerces; subst; clear Hcoerces. - + apply ConstituentOptC; clear_names; simpl; intuition. - + apply ConstituentOptC; clear_names; simpl; intuition. - + apply OpportunisticConstituentOptC; clear_names; simpl; intuition. - + apply OpportunisticConstituentOptC; clear_names; simpl; intuition. - + apply OpportunisticConstituentOptC; clear_names; simpl; intuition. - + apply OpportunisticConstituentOptC; clear_names; simpl; intuition. - * destruct t; - inversion Hcoerces; subst; clear Hcoerces. - + apply OpportunisticConstituentOptC; clear_names; simpl; intuition. - + apply ConstituentOptC; clear_names; simpl; intuition. - + apply OpportunisticConstituentOptC; clear_names; simpl; intuition. - + apply OpportunisticConstituentOptC; clear_names; simpl; intuition. - + apply OpportunisticConstituentOptC; clear_names; simpl; intuition. - + apply OpportunisticConstituentOptC; clear_names; simpl; intuition. - * destruct (coerce v1 t) eqn:Heq; simpl in Hcoerces; - inversion Hcoerces; subst; clear Hcoerces. - + apply SomeOptC; clear_names; intuition. - + apply OpportunisticOptC; clear_names; easy. -Qed. - -Lemma is_opt_like_type_correct: - forall t, - is_opt_like_type t = true <-> NullT <: t. -Proof. - intros. destruct t; simpl; intuition. - all: try inversion H. - all: try named_constructor. -Qed. - -Theorem coercion_correctness: - forall v1 v2 t, v1 ~> v2 :: t -> v2 :: t. -Proof. - intros. - revert v2 t H. - induction v1; - intros v2 t Hcoerce; - unfold Coerces in Hcoerce; - functional inversion Hcoerce; simpl in *; subst; clear Hcoerce; - try (named_constructor; named_constructor; fail). - * destruct (coerce v1 t1) eqn:Heq; simpl in *; inversion H0; subst; clear H0. - - specialize (IHv1 _ _ Heq). - named_constructor; assumption. - - named_constructor. -Qed. - -Theorem coercion_roundtrip: - forall v t, v :: t -> v ~> v :: t. -Proof. - intros. - induction H; try reflexivity. - * unfold Coerces in *. simpl. rewrite IHHasType. reflexivity. -Qed. - -Theorem coercion_uniqueness: - forall v v1 v2 t, v ~> v1 :: t -> v ~> v2 :: t -> v1 = v2. -Proof. - intro v. - induction v; intros v1 v2 t Heq1 Heq; - unfold Coerces in *; - congruence. -Qed. - -Theorem soundness_of_subtyping: - forall t1 t2, - t1 <: t2 -> - forall v1, v1 :: t1 -> exists v2, v1 ~> v2 :: t2. -Proof. - intros t1 t2 Hsub v HvT. revert t2 Hsub. - induction HvT; intros t1 Hsub; inversion Hsub; subst; clear Hsub; - name_cases; - try (eexists;reflexivity). - [natHT_optST]: { - destruct t2; eexists; reflexivity. - } - [intHT_optST]: { - destruct t2; eexists; reflexivity. - } - [optHT_reflST]: { - specialize (IHHvT t (ReflST _ _)). - destruct IHHvT as [v2 Hv2]. - eexists. unfold Coerces in *. simpl. rewrite Hv2. reflexivity. - } - [optHT_optST]: { - unfold Coerces. simpl. - destruct (coerce v t2) eqn:Heq; eexists; reflexivity. - } -Qed. - -Theorem subtyping_refl: reflexive _ Subtype. -Proof. intros x. apply ReflST; constructor. Qed. - Lemma is_not_opt_like_type_contravariant: forall t1 t2, is_opt_like_type t1 = false -> t2 <: t1 -> is_opt_like_type t2 = false. Proof. intros. destruct t1, t2; easy. Qed. - -Theorem subtyping_trans: transitive _ Subtype. -Proof. - cofix Hyp. - intros t1 t2 t3 H1 H2. - inversion H1; subst; clear H1; - inversion H2; subst; clear H2; - name_cases; - try (constructor; easy). -Qed. - -End TypeErasure. - - -End OpportunisticDecoding. \ No newline at end of file From 92e9c86892bc97ecb01ed74d06faac2e88682058 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 27 Jan 2021 12:23:21 +0100 Subject: [PATCH 08/22] fix --- coq/MiniCandid.v | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/coq/MiniCandid.v b/coq/MiniCandid.v index 694a9c76c..a67e3de95 100644 --- a/coq/MiniCandid.v +++ b/coq/MiniCandid.v @@ -353,13 +353,12 @@ Proof. coerce t1 t2 v1 = v1) by (intros; apply H; intuition; try apply ReflST; clear_names). apply (coerce_nice_ind (fun t1 t2 v1 v2 => t2 = t1 -> v2 = v1)); - intros; name_cases; subst; simpl in *; try solve [congruence]. + intros; name_cases; try solve [subst; simpl in *; congruence]. [optSomeC]: {apply f_equal. apply H0. congruence. } [opportunisticOptC]: { inversion H0; subst; clear H0. contradiction H; apply ReflST; clear_names. } - * (* why is this not named? *) - inversion H; subst; clear H. reflexivity. + [reservedC]: { inversion H; subst; clear H; congruence. } Qed. Lemma coerce_well_defined: From caf4b3b3bea581f38164a51278b234bcff0c87be Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 27 Jan 2021 15:10:54 +0100 Subject: [PATCH 09/22] stash --- coq/MiniCandid.v | 337 +++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 328 insertions(+), 9 deletions(-) diff --git a/coq/MiniCandid.v b/coq/MiniCandid.v index a67e3de95..652cbce8d 100644 --- a/coq/MiniCandid.v +++ b/coq/MiniCandid.v @@ -169,19 +169,16 @@ Function coerce (t1 : T) (t2 : T) (v1 : V) : V := then SomeV (coerce t1 t2 v) else NullV - (* This is the rule we would like to have, but - in order to please the termination checker, - we have to duplicate all non-opt rules in their opt variant - | v, t1, OptT t2 => - if not (is_opt_like_type t) && t <: t2 - then SomeV (coerce v t1 t2) + (* We’d prefer the equation from coerce_consituent_eq below, + but that will not satisfy the termination checker, + so let’s repeat all the above ruls 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)) | FuncV r, FuncT ta1 tr1, OptT (FuncT ta2 tr2) => if ta2 <:? ta1 - then if tr1 <:? tr2 then SomeV (FuncV r) else NullV else NullV + then if tr1 <:? tr2 then SomeV (FuncV r) else NullV else NullV | v, t, ReservedT => ReservedV @@ -189,6 +186,42 @@ Function coerce (t1 : T) (t2 : T) (v1 : V) : V := | _, _, _ => NullV end. +(* We can prove the desired equation at least as an equality *) +Lemma coerce_consituent_eq: + forall v t1 t2, + v :: t1 -> + is_opt_like_type t1 = 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. +Proof. + intros v t1 t2 HHT His_opt_like. + inversion HHT; subst; clear HHT; inversion His_opt_like; clear His_opt_like; name_cases. + [natHT]: { + destruct (NatT <:? t2) as [HST | HNotST]. + - inversion HST; subst; clear HST; simpl; reflexivity. + - destruct t2; try reflexivity; contradict HNotST; named_constructor. + } + [intHT]: { + destruct (IntT <:? t2) as [HST | HNotST]. + - inversion HST; subst; clear HST; simpl; reflexivity. + - destruct t2; try reflexivity; contradict HNotST; named_constructor. + } + [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. + } +Qed. (* Let’s try to create a suitable induction principle for this function *) Lemma coerce_nice_ind: @@ -201,6 +234,7 @@ Lemma coerce_nice_ind: (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, @@ -213,6 +247,7 @@ Lemma coerce_nice_ind: 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)) -> (case opportunisticConstituentOptC, @@ -238,6 +273,10 @@ Proof. [reflST]: { apply NatC; clear_names. } [natIntST]: { apply NatIntC; clear_names. } [optST]: { + (* oddly, + rewrite coerce_consituent_eq by (try named_constructor; reflexivity). + does not seem to lead to a simpler proof here. + *) 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. @@ -285,10 +324,12 @@ Proof. - simpl. repeat rewrite subtype_dec_refl. apply ConstituentOptC; clear_names; simpl; try (intuition;fail). ** apply ReflST; clear_names; apply ReflST; clear_names. + ** named_constructor. ** apply FuncC; clear_names; apply ReflST; clear_names. - simpl. repeat rewrite subtype_dec_true by assumption. apply ConstituentOptC; clear_names; simpl; try (intuition;fail). - named_constructor; assumption. + ** named_constructor; assumption. + ** named_constructor. + destruct t4; inversion His_opt_like; clear His_opt_like. - apply OpportunisticConstituentOptC; clear_names; simpl; intuition. - apply OpportunisticConstituentOptC; clear_names; simpl; intuition. @@ -354,7 +395,7 @@ Proof. by (intros; apply H; intuition; try apply ReflST; clear_names). apply (coerce_nice_ind (fun t1 t2 v1 v2 => t2 = t1 -> v2 = v1)); intros; name_cases; try solve [subst; simpl in *; congruence]. - [optSomeC]: {apply f_equal. apply H0. congruence. } + [optSomeC]: {apply f_equal. apply H1. congruence. } [opportunisticOptC]: { inversion H0; subst; clear H0. contradiction H; apply ReflST; clear_names. } @@ -375,3 +416,281 @@ Lemma is_not_opt_like_type_contravariant: forall t1 t2, is_opt_like_type t1 = false -> t2 <: t1 -> is_opt_like_type t2 = false. Proof. intros. destruct t1, t2; easy. Qed. + +(* +To work towards IDL soundness, we need a predicate for “Value v contains +a function reference at function type t.”. Moreover, this contains +relation should indicate the position in the value in a way that +the positions match up even after coercions. + +We allow spurious The constructors on this path; this models +the consituent-to-opt rule. +*) + +(* This needs to be extended once we have sequences and records *) +Inductive Path := + | Here : Path + | The : Path -> Path + . + +Fixpoint val_idx (v : V) (p : Path) : option V := + match p with + | Here => Some v + | The p => + match v with + | SomeV v => val_idx v p + | _ => None + end + end. + +Fixpoint val_idx' (v : V) (p : Path) : option V := + match p with + | Here => Some v + | The p => + match v with + | SomeV v => val_idx' v p + | NullV => None + | ReservedV => None + | _ => val_idx' v p + end + end. + + +Fixpoint typ_idx (t : T) (p : Path) : option T := + match p with + | Here => Some t + | The p => + match t with + | OptT t => typ_idx t p + | _ => typ_idx t p + end + end. + +Fixpoint typ_idx' (t : T) (p : Path) : option T := + match p with + | Here => Some t + | The p => + match t with + | OptT t => typ_idx' t p + | NullT => None + | ReservedT => None + | _ => typ_idx' t p + end + end. + +Lemma path_preserves_types: + forall v v' t t' p, + v :: t -> + val_idx v p = Some v' -> + typ_idx t p = Some t' -> + v' :: t'. +Admitted. + +Lemma path_preserves_types': + forall v v' t t' p, + v :: t -> + val_idx' v p = Some v' -> + typ_idx' t p = Some t' -> + v' :: t'. +Proof. + intros v v' t t' p. + revert v v' t t'. + induction p. + * intros v v' t t' HHT Hval_idx Htyp_idx. + inversion Hval_idx; subst; clear Hval_idx; + inversion Htyp_idx; subst; clear Htyp_idx. + assumption. + * intros v v' t t' HHT Hval_idx Htyp_idx. + inversion Hval_idx; subst; clear Hval_idx; + inversion Htyp_idx; subst; clear Htyp_idx. + inversion HHT; subst; clear HHT; name_cases. + all: try congruence. + all: try solve + [eapply IHp; [|eassumption|eassumption]; try assumption; named_constructor]. +Qed. + +Lemma all_paths_typed: + forall v v' t p, + v :: t -> + val_idx' v p = Some v' -> + exists t', typ_idx' t p = Some t'. +Proof. + intros v v' t p. + revert v v' t. + induction p. + * intros v v' t HHT Hval_idx. + inversion Hval_idx; subst; clear Hval_idx. + eexists. reflexivity. + * intros v v' t HHT Hval_idx. + inversion Hval_idx; subst; clear Hval_idx. + inversion HHT; subst; clear HHT; name_cases. + all: try congruence. + Show Existentials. + [natHT]: { + specialize (IHp _ _ NatT ltac:(named_constructor) H0). + destruct IHp as [t' Htyp_idx]. + eexists. + simpl. eassumption. + } + [intHT]: { + specialize (IHp _ _ IntT ltac:(named_constructor) H0). + destruct IHp as [t' Htyp_idx]. + eexists. + simpl. eassumption. + } + [optHT]: { + specialize (IHp _ _ t0 H H0). + destruct IHp as [t' Htyp_idx]. + eexists. + simpl. eassumption. + } + [funcHT]: { + specialize (IHp _ _ (FuncT t1 t2) ltac:(named_constructor) H0). + destruct IHp as [t' Htyp_idx]. + eexists. + simpl. eassumption. + } +Qed. + +(* +Because of our subtyping relation, when we coerce, +we may be introducing some SomeV. This corresponds to +adding some Paths. + +Inductive add_thes : Path -> Path -> Prop := + | HereAT : add_thes Here Here + | UnderTheAT: forall p1 p2, add_thes p1 p2 -> add_thes (The p1) (The p2) + | AddTheAT: forall p1 p2, add_thes p1 p2 -> add_thes p1 (The p2). +*) + +Lemma no_new_values: + forall t1 t2 v1, + t1 <: t2 -> + v1 :: t1 -> + forall p iv2 it2, + val_idx (coerce t1 t2 v1) p = Some iv2 -> + typ_idx t2 p = Some it2 -> + exists iv1 it1, + val_idx v1 p = Some iv1 /\ + typ_idx t1 p = Some it1 /\ + it1 <: it2 /\ + iv1 :: it1 /\ + coerce it1 it2 iv1 = iv2. +Proof. + apply (coerce_nice_ind (fun t1 t2 v1 v2 => + forall p iv2 it2, + val_idx v2 p = Some iv2 -> + typ_idx t2 p = Some it2 -> + exists iv1 it1, + val_idx v1 p = Some iv1 /\ + typ_idx t1 p = Some it1 /\ + it1 <: it2 /\ + iv1 :: it1 /\ + coerce it1 it2 iv1 = iv2 + )); intros; name_cases. + [natC]: { + destruct p; + inversion H; subst; clear H; + inversion H0; subst; clear H0. + * eexists; eexists. + repeat split. + - named_constructor. + - named_constructor. + * simpl. + eexists; eexists. + repeat split. + - eassumption. + - eassumption. + - named_constructor. + - named_constructor. + } + [intC]: { + destruct p2; + inversion H; subst; clear H; + inversion H0; subst; clear H0. + eexists; eexists; eexists. + repeat split. + - constructor. + - reflexivity. + - reflexivity. + - named_constructor. + - named_constructor. + - reflexivity. + } + [natIntC]: { + destruct p2; + inversion H; subst; clear H; + inversion H0; subst; clear H0. + eexists; eexists; eexists. + repeat split. + - constructor. + - reflexivity. + - reflexivity. + - named_constructor. + - named_constructor. + - reflexivity. + } + [nullC]: { + destruct p2; + inversion H; subst; clear H; + inversion H0; subst; clear H0. + eexists; eexists; eexists. + repeat split. + - constructor. + - reflexivity. + - reflexivity. + - named_constructor. + - named_constructor. + - reflexivity. + } + [nullOptC]: { + destruct p2; + inversion H; subst; clear H; + inversion H0; subst; clear H0. + eexists; eexists; eexists. + repeat split. + - constructor. + - reflexivity. + - reflexivity. + - named_constructor. + - named_constructor. + - reflexivity. + } + [optNullC]: { + destruct p2; + inversion H; subst; clear H; + inversion H0; subst; clear H0. + eexists; eexists; eexists. + repeat split. + - constructor. + - reflexivity. + - reflexivity. + - named_constructor. + - named_constructor. + - reflexivity. + } + [optSomeC]: { + destruct p2; + inversion H2; subst; clear H2; + inversion H3; subst; clear H3. + * + specialize (H1 Here v2 t2 ltac:(destruct v2; reflexivity) ltac:(destruct v2; reflexivity)). + destruct H1 as [p1 [iv1 [it1 Hi]]]. + exists (The Here); exists (SomeV iv1); exists (OptT it1). + repeat split. + - + - named_constructor. + - named_constructor; assumption. + - simpl. rewrite subtype_dec_true by assumption. intuition. + - named_constructor. + - named_constructor; assumption. + - simpl. rewrite subtype_dec_true by assumption. simpl. + } + Show Existentials. + + + +Definition + passesThrough + + From b2ecee65fcc18886de12b563aab8325f49e6fc02 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 27 Jan 2021 15:43:47 +0100 Subject: [PATCH 10/22] stash --- coq/MiniCandid.v | 117 +++++++++++++++++++++-------------------------- 1 file changed, 53 insertions(+), 64 deletions(-) diff --git a/coq/MiniCandid.v b/coq/MiniCandid.v index 652cbce8d..6104bd6c8 100644 --- a/coq/MiniCandid.v +++ b/coq/MiniCandid.v @@ -484,7 +484,7 @@ Lemma path_preserves_types: val_idx v p = Some v' -> typ_idx t p = Some t' -> v' :: t'. -Admitted. +Admitted. (* Did that once... *) Lemma path_preserves_types': forall v v' t t' p, @@ -509,7 +509,7 @@ Proof. [eapply IHp; [|eassumption|eassumption]; try assumption; named_constructor]. Qed. -Lemma all_paths_typed: +Lemma all_paths_typed': forall v v' t p, v :: t -> val_idx' v p = Some v' -> @@ -570,9 +570,10 @@ Lemma no_new_values: forall p iv2 it2, val_idx (coerce t1 t2 v1) p = Some iv2 -> typ_idx t2 p = Some it2 -> + ~ (iv2 = NullV) -> exists iv1 it1, - val_idx v1 p = Some iv1 /\ - typ_idx t1 p = Some it1 /\ + val_idx' v1 p = Some iv1 /\ + typ_idx' t1 p = Some it1 /\ it1 <: it2 /\ iv1 :: it1 /\ coerce it1 it2 iv1 = iv2. @@ -581,9 +582,10 @@ Proof. forall p iv2 it2, val_idx v2 p = Some iv2 -> typ_idx t2 p = Some it2 -> + ~ (iv2 = NullV) -> exists iv1 it1, - val_idx v1 p = Some iv1 /\ - typ_idx t1 p = Some it1 /\ + val_idx' v1 p = Some iv1 /\ + typ_idx' t1 p = Some it1 /\ it1 <: it2 /\ iv1 :: it1 /\ coerce it1 it2 iv1 = iv2 @@ -592,100 +594,87 @@ Proof. destruct p; inversion H; subst; clear H; inversion H0; subst; clear H0. - * eexists; eexists. - repeat split. - - named_constructor. - - named_constructor. - * simpl. - eexists; eexists. - repeat split. - - eassumption. - - eassumption. - - named_constructor. - - named_constructor. + eexists; eexists. + repeat split. + - named_constructor. + - named_constructor. } [intC]: { - destruct p2; + destruct p; inversion H; subst; clear H; inversion H0; subst; clear H0. - eexists; eexists; eexists. + eexists; eexists. repeat split. - - constructor. - - reflexivity. - - reflexivity. - named_constructor. - named_constructor. - - reflexivity. } [natIntC]: { - destruct p2; + destruct p; inversion H; subst; clear H; inversion H0; subst; clear H0. - eexists; eexists; eexists. + eexists; eexists. repeat split. - - constructor. - - reflexivity. - - reflexivity. - named_constructor. - named_constructor. - - reflexivity. } [nullC]: { - destruct p2; + destruct p; inversion H; subst; clear H; inversion H0; subst; clear H0. - eexists; eexists; eexists. + eexists; eexists. repeat split. - - constructor. - - reflexivity. - - reflexivity. - named_constructor. - named_constructor. - - reflexivity. } [nullOptC]: { - destruct p2; + destruct p; inversion H; subst; clear H; inversion H0; subst; clear H0. - eexists; eexists; eexists. - repeat split. - - constructor. - - reflexivity. - - reflexivity. - - named_constructor. - - named_constructor. - - reflexivity. + contradiction. } [optNullC]: { - destruct p2; + destruct p; inversion H; subst; clear H; inversion H0; subst; clear H0. - eexists; eexists; eexists. - repeat split. - - constructor. - - reflexivity. - - reflexivity. - - named_constructor. - - named_constructor. - - reflexivity. + contradiction. } [optSomeC]: { - destruct p2; + destruct p; inversion H2; subst; clear H2; inversion H3; subst; clear H3. - * - specialize (H1 Here v2 t2 ltac:(destruct v2; reflexivity) ltac:(destruct v2; reflexivity)). - destruct H1 as [p1 [iv1 [it1 Hi]]]. - exists (The Here); exists (SomeV iv1); exists (OptT it1). + * specialize (H1 Here v2 t2 ltac:(destruct v2; reflexivity) ltac:(destruct v2; reflexivity)). + simpl. + enough (OptT t1 <: OptT t2 /\ SomeV v1 :: OptT t1 /\ coerce (OptT t1) (OptT t2) (SomeV v1) = SomeV v2) + by firstorder. + simpl. + rewrite subtype_dec_true by assumption. + + destruct H1 as [iv1 [it1 Hi]]. + decompose record Hi; clear Hi. + inversion H1; subst; clear H1. + inversion H3; subst; clear H3. + eexists; eexists. repeat split. - - - - named_constructor. - - named_constructor; assumption. - - simpl. rewrite subtype_dec_true by assumption. intuition. - - named_constructor. + - right; named_constructor; assumption. - named_constructor; assumption. - - simpl. rewrite subtype_dec_true by assumption. simpl. + - simpl. rewrite subtype_dec_true by assumption. reflexivity. + * specialize (H1 _ _ _ H5 H4). + destruct H1 as [iv1 [it1 Hi]]. + decompose record Hi; clear Hi. + eexists; eexists; repeat split. + - simpl. eassumption. + - simpl. eassumption. + - assumption. + - assumption. + - assumption. } + [opportunisticOptC]: { + destruct p; + inversion H0; subst; clear H0; + inversion H1; subst; clear H1. + eexists; eexists; repeat split. + - + Show Existentials. From f575117ff351d58495370e75fc4c9932cd319039 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 27 Jan 2021 16:18:36 +0100 Subject: [PATCH 11/22] Prove compositionality --- coq/MiniCandid.v | 175 ++++++++++++++++++++++++++++++++++++----------- 1 file changed, 136 insertions(+), 39 deletions(-) diff --git a/coq/MiniCandid.v b/coq/MiniCandid.v index 6104bd6c8..343b1182a 100644 --- a/coq/MiniCandid.v +++ b/coq/MiniCandid.v @@ -239,6 +239,7 @@ Lemma coerce_nice_ind: P (OptT t1) (OptT t2) (SomeV v1) (SomeV v2)) -> (case opportunisticOptC, forall t1 t2 v1, ~ (t1 <: t2) -> + v1 :: t1 -> P (OptT t1) (OptT t2) (SomeV v1) NullV) -> (case reservedOptC, forall t, P ReservedT (OptT t) ReservedV NullV) -> @@ -252,6 +253,7 @@ Lemma coerce_nice_ind: P t1 (OptT t2) v1 (SomeV v2)) -> (case opportunisticConstituentOptC, forall t1 t2 v1, + v1 :: t1 -> is_opt_like_type t1 = false -> is_opt_like_type t2 = true \/ ~ (t1 <: t2) -> P t1 (OptT t2) v1 NullV) -> @@ -279,7 +281,7 @@ Proof. *) 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. + apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor. * destruct (subtyping_decidable NatT t0). + destruct t0; inversion s; subst; clear s; inversion His_opt_like; clear His_opt_like. - apply ConstituentOptC; clear_names; simpl; intuition; named_constructor. @@ -287,8 +289,8 @@ Proof. + destruct t0; inversion His_opt_like; clear His_opt_like. - contradict n0. named_constructor. - contradict n0. named_constructor. - - apply OpportunisticConstituentOptC; clear_names; simpl; intuition. - - apply OpportunisticConstituentOptC; clear_names; simpl; intuition. + - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor. + - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor. } [reservedST]: { apply ReservedC; clear_names. named_constructor. } } @@ -299,15 +301,15 @@ Proof. [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. + apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor. * destruct (subtyping_decidable IntT t0). + 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. + - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor. - contradict n0. named_constructor. - - apply OpportunisticConstituentOptC; clear_names; simpl; intuition. - - apply OpportunisticConstituentOptC; clear_names; simpl; intuition. + - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor. + - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor. } [reservedST]: { apply ReservedC; clear_names. named_constructor. } } @@ -318,7 +320,7 @@ Proof. [optST]: { destruct (is_opt_like_type t4) eqn:His_opt_like. * destruct t4; inversion His_opt_like; simpl; clear His_opt_like; - apply OpportunisticConstituentOptC; clear_names; simpl; intuition. + apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor. * destruct (subtyping_decidable (FuncT t1 t2) t4). + destruct t4; inversion s; subst; clear s; inversion His_opt_like; clear His_opt_like. - simpl. repeat rewrite subtype_dec_refl. @@ -331,15 +333,15 @@ Proof. ** named_constructor; assumption. ** named_constructor. + destruct t4; inversion His_opt_like; clear His_opt_like. - - apply OpportunisticConstituentOptC; clear_names; simpl; intuition. - - apply OpportunisticConstituentOptC; clear_names; simpl; intuition. + - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor. + - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor. - simpl. destruct (t4_1 <:? t1). ** destruct (t2 <:? t4_2). ++ contradict n. named_constructor; assumption. - ++ apply OpportunisticConstituentOptC; clear_names; simpl; intuition. - ** apply OpportunisticConstituentOptC; clear_names; simpl; intuition. - - apply OpportunisticConstituentOptC; clear_names; simpl; intuition. + ++ 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. } @@ -397,7 +399,7 @@ Proof. intros; name_cases; try solve [subst; simpl in *; congruence]. [optSomeC]: {apply f_equal. apply H1. congruence. } [opportunisticOptC]: { - inversion H0; subst; clear H0. contradiction H; apply ReflST; clear_names. + inversion H1; subst; clear H1. contradiction H; apply ReflST; clear_names. } [reservedC]: { inversion H; subst; clear H; congruence. } Qed. @@ -570,11 +572,10 @@ Lemma no_new_values: forall p iv2 it2, val_idx (coerce t1 t2 v1) p = Some iv2 -> typ_idx t2 p = Some it2 -> - ~ (iv2 = NullV) -> exists iv1 it1, val_idx' v1 p = Some iv1 /\ typ_idx' t1 p = Some it1 /\ - it1 <: it2 /\ + (iv2 = NullV \/ it1 <: it2) /\ iv1 :: it1 /\ coerce it1 it2 iv1 = iv2. Proof. @@ -582,11 +583,10 @@ Proof. forall p iv2 it2, val_idx v2 p = Some iv2 -> typ_idx t2 p = Some it2 -> - ~ (iv2 = NullV) -> exists iv1 it1, val_idx' v1 p = Some iv1 /\ typ_idx' t1 p = Some it1 /\ - it1 <: it2 /\ + (iv2 = NullV \/ it1 <: it2) /\ iv1 :: it1 /\ coerce it1 it2 iv1 = iv2 )); intros; name_cases. @@ -596,7 +596,7 @@ Proof. inversion H0; subst; clear H0. eexists; eexists. repeat split. - - named_constructor. + - right; named_constructor. - named_constructor. } [intC]: { @@ -605,7 +605,7 @@ Proof. inversion H0; subst; clear H0. eexists; eexists. repeat split. - - named_constructor. + - right; named_constructor. - named_constructor. } [natIntC]: { @@ -614,7 +614,7 @@ Proof. inversion H0; subst; clear H0. eexists; eexists. repeat split. - - named_constructor. + - right; named_constructor. - named_constructor. } [nullC]: { @@ -623,20 +623,26 @@ Proof. inversion H0; subst; clear H0. eexists; eexists. repeat split. - - named_constructor. + - right; named_constructor. - named_constructor. } [nullOptC]: { destruct p; inversion H; subst; clear H; inversion H0; subst; clear H0. - contradiction. + eexists; eexists. + repeat split. + - right; named_constructor. + - named_constructor. } [optNullC]: { destruct p; inversion H; subst; clear H; inversion H0; subst; clear H0. - contradiction. + eexists; eexists. + repeat split. + - right; named_constructor. + - named_constructor. } [optSomeC]: { destruct p; @@ -644,18 +650,13 @@ Proof. inversion H3; subst; clear H3. * specialize (H1 Here v2 t2 ltac:(destruct v2; reflexivity) ltac:(destruct v2; reflexivity)). simpl. - enough (OptT t1 <: OptT t2 /\ SomeV v1 :: OptT t1 /\ coerce (OptT t1) (OptT t2) (SomeV v1) = SomeV v2) - by firstorder. - simpl. - rewrite subtype_dec_true by assumption. - + enough (OptT t1 <: OptT t2 /\ SomeV v1 :: OptT t1 /\ coerce (OptT t1) (OptT t2) (SomeV v1) = SomeV v2) by firstorder. destruct H1 as [iv1 [it1 Hi]]. decompose record Hi; clear Hi. inversion H1; subst; clear H1. inversion H3; subst; clear H3. - eexists; eexists. repeat split. - - right; named_constructor; assumption. + - named_constructor; assumption. - named_constructor; assumption. - simpl. rewrite subtype_dec_true by assumption. reflexivity. * specialize (H1 _ _ _ H5 H4). @@ -669,17 +670,113 @@ Proof. - assumption. } [opportunisticOptC]: { + destruct p; + inversion H1; subst; clear H1; + inversion H2; subst; clear H2. + simpl. + eexists; eexists; repeat split. + - left; reflexivity. + - named_constructor. assumption. + - simpl. rewrite subtype_dec_false by assumption. reflexivity. + } + [reservedOptC]: { + destruct p; + inversion H; subst; clear H; + inversion H0; subst; clear H0. + eexists; eexists. + repeat split. + - left; reflexivity. + - named_constructor. + } + [constituentOptC]: { + destruct p; + inversion H4; subst; clear H4; + inversion H5; subst; clear H5. + * specialize (H3 Here v2 t2 ltac:(destruct v2; reflexivity) ltac:(destruct v2; reflexivity)). + simpl. + destruct H3 as [iv1 [it1 Hi]]. + decompose record Hi; clear Hi. + inversion H3; subst; clear H3. + inversion H5; subst; clear H5. + eexists; eexists; repeat split. + - right; named_constructor. + - assumption. + - simpl. + rewrite coerce_consituent_eq by assumption. + rewrite H0. + rewrite subtype_dec_true by assumption. reflexivity. + * specialize (H3 _ _ _ H7 H6). + destruct H3 as [iv1 [it1 Hi]]. + decompose record Hi; clear Hi. + eexists; eexists; repeat split. + - simpl. + rewrite H3. + inversion H2; subst; clear H2; inversion H; subst; clear H; reflexivity. + - simpl. + rewrite H5. + inversion H2; subst; clear H2; inversion H; subst; clear H; reflexivity. + - assumption. + - assumption. + - assumption. + } + [opportunisticConstituentOptC]: { + destruct p; + inversion H2; subst; clear H2; + inversion H3; subst; clear H3. + eexists; eexists; repeat split. + - left; reflexivity. + - assumption. + - rewrite coerce_consituent_eq by assumption. + destruct H1. + * rewrite H1. destruct (t1 <:? t2); reflexivity. + * rewrite subtype_dec_false by assumption. reflexivity. + } + [funcC]: { + destruct p; + inversion H1; subst; clear H1; + inversion H2; subst; clear H2. + eexists; eexists. + repeat split. + - right; named_constructor; assumption. + - named_constructor. + } + [reservedC]: { destruct p; inversion H0; subst; clear H0; inversion H1; subst; clear H1. - eexists; eexists; repeat split. - - - - Show Existentials. - - + eexists; eexists. + repeat split. + - right; named_constructor; assumption. + - assumption. + - destruct t, v; simpl; try reflexivity. + } +Qed. -Definition - passesThrough +Definition passesThrough (s1 : T * T) (t1 : T) (s2 : T * T) (t2 : T) := + exists v1 p r, + v1 :: t1 /\ + val_idx' v1 p = Some (FuncV r) /\ + typ_idx' t1 p = Some (FuncT (fst s1) (snd s1)) /\ + val_idx (coerce t1 t2 v1) p = Some (FuncV r) /\ + typ_idx t2 p = Some (FuncT (fst s2) (snd s2)). +Lemma compositional: + forall t1 t2 s1 s2, + t1 <: t2 -> passesThrough s1 t1 s2 t2 -> (fst s2 <: fst s1 /\ snd s1 <: snd s2). +Proof. + intros. + unfold passesThrough in *. + destruct s1, s2. + simpl in *. + enough (FuncT t t0 <: FuncT t3 t4) + by (inversion H1; subst; clear H1; split; try assumption; named_constructor). + destruct H0 as [v1 [p [r Hpt]]]. + decompose record Hpt; clear Hpt. + pose proof (no_new_values t1 t2 v1 H H0 p _ _ H3 H5). + destruct H4 as [iv1 [it1 Hnnv]]. + decompose record Hnnv; clear Hnnv. + rewrite H2 in H4. inversion H4; subst; clear H4. + rewrite H1 in H7. inversion H7; subst; clear H7. + destruct H6; congruence. +Qed. From ffe1fa41a76ef4972513ba508f6577bdad9de316 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 27 Jan 2021 16:28:59 +0100 Subject: [PATCH 12/22] And Soundness is instantiated --- coq/MiniCandid.v | 39 +++++++++++++++++++++++++++++++++++++-- 1 file changed, 37 insertions(+), 2 deletions(-) diff --git a/coq/MiniCandid.v b/coq/MiniCandid.v index 343b1182a..573ce37b7 100644 --- a/coq/MiniCandid.v +++ b/coq/MiniCandid.v @@ -527,7 +527,6 @@ Proof. inversion Hval_idx; subst; clear Hval_idx. inversion HHT; subst; clear HHT; name_cases. all: try congruence. - Show Existentials. [natHT]: { specialize (IHp _ _ NatT ltac:(named_constructor) H0). destruct IHp as [t' Htyp_idx]. @@ -763,7 +762,7 @@ Definition passesThrough (s1 : T * T) (t1 : T) (s2 : T * T) (t2 : T) := Lemma compositional: forall t1 t2 s1 s2, - t1 <: t2 -> passesThrough s1 t1 s2 t2 -> (fst s2 <: fst s1 /\ snd s1 <: snd s2). + t1 <: t2 -> passesThrough s1 t1 s2 t2 -> (snd s1 <: snd s2 /\ fst s2 <: fst s1). Proof. intros. unfold passesThrough in *. @@ -780,3 +779,39 @@ Proof. rewrite H1 in H7. inversion H7; subst; clear H7. destruct H6; congruence. Qed. + + +Require Import candid.IDLSoundness. + +Theorem soundness: + forall I, + IDLSound T Subtype passesThrough + (fun '(ta2, tr2) '(ta1,tr1) => ta2 <: ta1 /\ tr1 <: tr2) + (fun '(ta1,tr1) '(ta2, tr2) => ta2 <: ta1 /\ tr1 <: tr2) + I. +Proof. + intro. + apply canonical_soundness. + - apply subtyping_refl. + - apply subtyping_trans. + - unfold service_subtyping. + intros. + destruct s1 as [ta1 tr1]. + destruct s2 as [ta2 tr2]. + intuition. + - intros. + pose proof (compositional _ _ _ _ H H0). + unfold service_subtyping. + intros. + destruct s1 as [ta1 tr1]. + destruct s2 as [ta2 tr2]. + intuition. + - intros. + destruct s1 as [ta1 tr1]. + destruct s2 as [ta2 tr2]. + unfold service_subtyping. + intuition. +Qed.f + + + \ No newline at end of file From 526d3491407baab9791f540876aa5abebfcef92e Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 27 Jan 2021 17:00:47 +0100 Subject: [PATCH 13/22] Syntax fix --- coq/MiniCandid.v | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/coq/MiniCandid.v b/coq/MiniCandid.v index 573ce37b7..6d0475609 100644 --- a/coq/MiniCandid.v +++ b/coq/MiniCandid.v @@ -811,7 +811,4 @@ Proof. destruct s2 as [ta2 tr2]. unfold service_subtyping. intuition. -Qed.f - - - \ No newline at end of file +Qed. \ No newline at end of file From a20f8e8e0b81d211656fe006853eabeb52373f74 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 27 Jan 2021 17:03:06 +0100 Subject: [PATCH 14/22] Remove unused lemma --- coq/MiniCandid.v | 7 ------- 1 file changed, 7 deletions(-) diff --git a/coq/MiniCandid.v b/coq/MiniCandid.v index 6d0475609..0f024a1e9 100644 --- a/coq/MiniCandid.v +++ b/coq/MiniCandid.v @@ -480,13 +480,6 @@ Fixpoint typ_idx' (t : T) (p : Path) : option T := end end. -Lemma path_preserves_types: - forall v v' t t' p, - v :: t -> - val_idx v p = Some v' -> - typ_idx t p = Some t' -> - v' :: t'. -Admitted. (* Did that once... *) Lemma path_preserves_types': forall v v' t t' p, From 81a8afe9e41d6a9bedd456f89c6c99383dfbf3b0 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 28 Jan 2021 11:16:41 +0100 Subject: [PATCH 15/22] Some simplifications --- coq/MiniCandid.v | 332 ++++++++++++----------------------------------- 1 file changed, 80 insertions(+), 252 deletions(-) diff --git a/coq/MiniCandid.v b/coq/MiniCandid.v index 0f024a1e9..edcf02254 100644 --- a/coq/MiniCandid.v +++ b/coq/MiniCandid.v @@ -425,297 +425,139 @@ a function reference at function type t.”. Moreover, this contains relation should indicate the position in the value in a way that the positions match up even after coercions. -We allow spurious The constructors on this path; this models -the consituent-to-opt rule. +So we start by giving names to positions +(This needs to be extended once we have sequences and records) *) - -(* This needs to be extended once we have sequences and records *) Inductive Path := | Here : Path | The : Path -> Path . -Fixpoint val_idx (v : V) (p : Path) : option V := +(* +And a function that finds the value at a given path. +It returns None if the path does not make sense for this value. +*) +Fixpoint val_idx (p : Path) (v : V) : option V := match p with | Here => Some v | The p => match v with - | SomeV v => val_idx v p + | SomeV v => val_idx p v | _ => None end end. -Fixpoint val_idx' (v : V) (p : Path) : option V := - match p with - | Here => Some v - | The p => - match v with - | SomeV v => val_idx' v p - | NullV => None - | ReservedV => None - | _ => val_idx' v p - end - end. - +(* +This is a lenitent variant, which is total (returning NoneV +when the path is invalid), which makes proofs simpler. -Fixpoint typ_idx (t : T) (p : Path) : option T := +It also ignores extra [The] on the path; this way one can +use this on the pre-coerced value, and get the right value, +even if the constituent-to-optional rule was used. +*) +Fixpoint val_idx' (p : Path) (v : V) : V := match p with - | Here => Some t + | Here => v | The p => - match t with - | OptT t => typ_idx t p - | _ => typ_idx t p + match v with + | SomeV v => val_idx' p v + | NullV => NullV + | ReservedV => NullV + | _ => val_idx' p v end end. -Fixpoint typ_idx' (t : T) (p : Path) : option T := +(* +The corresponding function for types, also lenitent. +*) +Fixpoint typ_idx' (p : Path) (t : T) : T := match p with - | Here => Some t + | Here => t | The p => match t with - | OptT t => typ_idx' t p - | NullT => None - | ReservedT => None - | _ => typ_idx' t p + | OptT t => typ_idx' p t + | NullT => VoidT + | ReservedT => VoidT + | _ => typ_idx' p t end end. - -Lemma path_preserves_types': - forall v v' t t' p, - v :: t -> - val_idx' v p = Some v' -> - typ_idx' t p = Some t' -> - v' :: t'. -Proof. - intros v v' t t' p. - revert v v' t t'. - induction p. - * intros v v' t t' HHT Hval_idx Htyp_idx. - inversion Hval_idx; subst; clear Hval_idx; - inversion Htyp_idx; subst; clear Htyp_idx. - assumption. - * intros v v' t t' HHT Hval_idx Htyp_idx. - inversion Hval_idx; subst; clear Hval_idx; - inversion Htyp_idx; subst; clear Htyp_idx. - inversion HHT; subst; clear HHT; name_cases. - all: try congruence. - all: try solve - [eapply IHp; [|eassumption|eassumption]; try assumption; named_constructor]. -Qed. - -Lemma all_paths_typed': +Lemma path_preserves_types: forall v v' t p, v :: t -> - val_idx' v p = Some v' -> - exists t', typ_idx' t p = Some t'. + val_idx p v = Some v' -> + v' :: typ_idx' p t. Proof. intros v v' t p. revert v v' t. induction p. * intros v v' t HHT Hval_idx. inversion Hval_idx; subst; clear Hval_idx. - eexists. reflexivity. + assumption. * intros v v' t HHT Hval_idx. inversion Hval_idx; subst; clear Hval_idx. inversion HHT; subst; clear HHT; name_cases. - all: try congruence. - [natHT]: { - specialize (IHp _ _ NatT ltac:(named_constructor) H0). - destruct IHp as [t' Htyp_idx]. - eexists. - simpl. eassumption. - } - [intHT]: { - specialize (IHp _ _ IntT ltac:(named_constructor) H0). - destruct IHp as [t' Htyp_idx]. - eexists. - simpl. eassumption. - } - [optHT]: { - specialize (IHp _ _ t0 H H0). - destruct IHp as [t' Htyp_idx]. - eexists. - simpl. eassumption. - } - [funcHT]: { - specialize (IHp _ _ (FuncT t1 t2) ltac:(named_constructor) H0). - destruct IHp as [t' Htyp_idx]. - eexists. - simpl. eassumption. - } + all: firstorder congruence. Qed. -(* -Because of our subtyping relation, when we coerce, -we may be introducing some SomeV. This corresponds to -adding some Paths. - -Inductive add_thes : Path -> Path -> Prop := - | HereAT : add_thes Here Here - | UnderTheAT: forall p1 p2, add_thes p1 p2 -> add_thes (The p1) (The p2) - | AddTheAT: forall p1 p2, add_thes p1 p2 -> add_thes p1 (The p2). -*) - Lemma no_new_values: forall t1 t2 v1, t1 <: t2 -> v1 :: t1 -> - forall p iv2 it2, - val_idx (coerce t1 t2 v1) p = Some iv2 -> - typ_idx t2 p = Some it2 -> - exists iv1 it1, - val_idx' v1 p = Some iv1 /\ - typ_idx' t1 p = Some it1 /\ - (iv2 = NullV \/ it1 <: it2) /\ - iv1 :: it1 /\ - coerce it1 it2 iv1 = iv2. + 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 /\ + coerce (typ_idx' p t1) (typ_idx' p t2) (val_idx' p v1) = iv2. Proof. apply (coerce_nice_ind (fun t1 t2 v1 v2 => - forall p iv2 it2, - val_idx v2 p = Some iv2 -> - typ_idx t2 p = Some it2 -> - exists iv1 it1, - val_idx' v1 p = Some iv1 /\ - typ_idx' t1 p = Some it1 /\ - (iv2 = NullV \/ it1 <: it2) /\ - iv1 :: it1 /\ - coerce it1 it2 iv1 = iv2 + forall p iv2, + forall (Hval_idx : val_idx p v2 = Some iv2), + (iv2 = NullV \/ typ_idx' p t1 <: typ_idx' p t2) /\ + val_idx' p v1 :: typ_idx' p t1 /\ + coerce (typ_idx' p t1) (typ_idx' p t2) (val_idx' p v1) = iv2 )); intros; name_cases. - [natC]: { - destruct p; - inversion H; subst; clear H; - inversion H0; subst; clear H0. - eexists; eexists. - repeat split. - - right; named_constructor. - - named_constructor. - } - [intC]: { - destruct p; - inversion H; subst; clear H; - inversion H0; subst; clear H0. - eexists; eexists. - repeat split. - - right; named_constructor. - - named_constructor. - } - [natIntC]: { - destruct p; - inversion H; subst; clear H; - inversion H0; subst; clear H0. - eexists; eexists. - repeat split. - - right; named_constructor. - - named_constructor. - } - [nullC]: { - destruct p; - inversion H; subst; clear H; - inversion H0; subst; clear H0. - eexists; eexists. - repeat split. - - right; named_constructor. - - named_constructor. - } - [nullOptC]: { - destruct p; - inversion H; subst; clear H; - inversion H0; subst; clear H0. - eexists; eexists. - repeat split. - - right; named_constructor. - - named_constructor. - } - [optNullC]: { - destruct p; - inversion H; subst; clear H; - inversion H0; subst; clear H0. - eexists; eexists. - repeat split. - - right; named_constructor. - - named_constructor. - } + all: + try solve [destruct p; inversion Hval_idx; subst; clear Hval_idx; intuition (named_constructor; assumption)]. [optSomeC]: { - destruct p; - inversion H2; subst; clear H2; - inversion H3; subst; clear H3. - * specialize (H1 Here v2 t2 ltac:(destruct v2; reflexivity) ltac:(destruct v2; reflexivity)). - simpl. - enough (OptT t1 <: OptT t2 /\ SomeV v1 :: OptT t1 /\ coerce (OptT t1) (OptT t2) (SomeV v1) = SomeV v2) by firstorder. - destruct H1 as [iv1 [it1 Hi]]. - decompose record Hi; clear Hi. - inversion H1; subst; clear H1. - inversion H3; subst; clear H3. + destruct p; inversion Hval_idx; subst; clear Hval_idx. + * specialize (H1 Here v2 eq_refl). + simpl in *. + decompose record H1; clear H1. repeat split. + - right; named_constructor; assumption. - named_constructor; assumption. - - named_constructor; assumption. - - simpl. rewrite subtype_dec_true by assumption. reflexivity. - * specialize (H1 _ _ _ H5 H4). - destruct H1 as [iv1 [it1 Hi]]. - decompose record Hi; clear Hi. - eexists; eexists; repeat split. - - simpl. eassumption. - - simpl. eassumption. - - assumption. - - assumption. - - assumption. + - simpl. rewrite subtype_dec_true by assumption. congruence. + * specialize (H1 _ _ H3). + intuition. } [opportunisticOptC]: { - destruct p; - inversion H1; subst; clear H1; - inversion H2; subst; clear H2. - simpl. - eexists; eexists; repeat split. + destruct p; inversion Hval_idx; subst; clear Hval_idx. + simpl in *. + repeat split. - left; reflexivity. - named_constructor. assumption. - simpl. rewrite subtype_dec_false by assumption. reflexivity. } - [reservedOptC]: { - destruct p; - inversion H; subst; clear H; - inversion H0; subst; clear H0. - eexists; eexists. - repeat split. - - left; reflexivity. - - named_constructor. - } [constituentOptC]: { - destruct p; - inversion H4; subst; clear H4; - inversion H5; subst; clear H5. - * specialize (H3 Here v2 t2 ltac:(destruct v2; reflexivity) ltac:(destruct v2; reflexivity)). - simpl. - destruct H3 as [iv1 [it1 Hi]]. - decompose record Hi; clear Hi. - inversion H3; subst; clear H3. - inversion H5; subst; clear H5. - eexists; eexists; repeat split. + destruct p; inversion Hval_idx; subst; clear Hval_idx. + * specialize (H3 Here v2 eq_refl). + simpl in *. + decompose record H3; clear H3. + repeat split. - right; named_constructor. - assumption. - - simpl. - rewrite coerce_consituent_eq by assumption. + - rewrite coerce_consituent_eq by assumption. rewrite H0. - rewrite subtype_dec_true by assumption. reflexivity. - * specialize (H3 _ _ _ H7 H6). - destruct H3 as [iv1 [it1 Hi]]. - decompose record Hi; clear Hi. - eexists; eexists; repeat split. - - simpl. - rewrite H3. - inversion H2; subst; clear H2; inversion H; subst; clear H; reflexivity. - - simpl. - rewrite H5. - inversion H2; subst; clear H2; inversion H; subst; clear H; reflexivity. - - assumption. - - assumption. - - assumption. + rewrite subtype_dec_true by assumption. congruence. + * specialize (H3 _ _ H5). + decompose record H3; clear H3. + inversion H2; subst; clear H2; inversion H; subst; clear H; intuition. } [opportunisticConstituentOptC]: { - destruct p; - inversion H2; subst; clear H2; - inversion H3; subst; clear H3. - eexists; eexists; repeat split. + destruct p; inversion Hval_idx; subst; clear Hval_idx. + simpl in *. + repeat split. - left; reflexivity. - assumption. - rewrite coerce_consituent_eq by assumption. @@ -723,20 +565,9 @@ Proof. * rewrite H1. destruct (t1 <:? t2); reflexivity. * rewrite subtype_dec_false by assumption. reflexivity. } - [funcC]: { - destruct p; - inversion H1; subst; clear H1; - inversion H2; subst; clear H2. - eexists; eexists. - repeat split. - - right; named_constructor; assumption. - - named_constructor. - } [reservedC]: { - destruct p; - inversion H0; subst; clear H0; - inversion H1; subst; clear H1. - eexists; eexists. + destruct p; inversion Hval_idx; subst; clear Hval_idx. + simpl in *. repeat split. - right; named_constructor; assumption. - assumption. @@ -747,10 +578,10 @@ Qed. Definition passesThrough (s1 : T * T) (t1 : T) (s2 : T * T) (t2 : T) := exists v1 p r, v1 :: t1 /\ - val_idx' v1 p = Some (FuncV r) /\ - typ_idx' t1 p = Some (FuncT (fst s1) (snd s1)) /\ - val_idx (coerce t1 t2 v1) p = Some (FuncV r) /\ - typ_idx t2 p = Some (FuncT (fst s2) (snd s2)). + val_idx' p v1 = FuncV r /\ + typ_idx' p t1 = FuncT (fst s1) (snd s1) /\ + val_idx p (coerce t1 t2 v1) = Some (FuncV r) /\ + typ_idx' p t2 = FuncT (fst s2) (snd s2). Lemma compositional: @@ -765,12 +596,9 @@ Proof. by (inversion H1; subst; clear H1; split; try assumption; named_constructor). destruct H0 as [v1 [p [r Hpt]]]. decompose record Hpt; clear Hpt. - pose proof (no_new_values t1 t2 v1 H H0 p _ _ H3 H5). - destruct H4 as [iv1 [it1 Hnnv]]. + pose proof (no_new_values t1 t2 v1 H H0 p _ H3) as Hnnv. decompose record Hnnv; clear Hnnv. - rewrite H2 in H4. inversion H4; subst; clear H4. - rewrite H1 in H7. inversion H7; subst; clear H7. - destruct H6; congruence. + destruct H4; congruence. Qed. From 0aea59a17f7bdd04ba6a15b9841bdc9d199d629d Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 29 Jan 2021 16:29:12 +0100 Subject: [PATCH 16/22] Some cleanup --- coq/IDLSoundness.v | 44 +++++++++------ coq/MiniCandid.v | 137 +++++++++++++++++++++++++++++++++------------ 2 files changed, 128 insertions(+), 53 deletions(-) diff --git a/coq/IDLSoundness.v b/coq/IDLSoundness.v index c1d617be8..97fcce77e 100644 --- a/coq/IDLSoundness.v +++ b/coq/IDLSoundness.v @@ -1,13 +1,16 @@ -(* This formalizes +(** + +This theory formalizes https://github.com/dfinity/candid/blob/master/spec/IDL-Soundness.md - *) + +*) Require Import Coq.Lists.List. Import ListNotations. Require Import Coq.Sets.Ensembles. (* Odd that this is needed, see - https://www.reddit.com/r/Coq/comments/bmslyy/why_doesnt_ensemble_functions_in_coqs_standard/emzazzd +https://www.reddit.com/r/Coq/comments/bmslyy/why_doesnt_ensemble_functions_in_coqs_standard/emzazzd *) Arguments In {U}. Arguments Add {U}. @@ -23,16 +26,21 @@ Set Bullet Behavior "Strict Subproofs". Section IDL. - (* An abstract theory of IDLs is parametrized as follows: *) - - (* Argument or result types *) + (** + + * The Abstract IDL theory + + An abstract theory of IDLs is parametrized as follows: + *) + + (** The type of (argument or result types) *) Variable T : Set. - (* A service type is a pair of types *) + (** A service type is a pair of types (argument and results) *) Definition S : Set := (T * T). Notation "t1 --> t2" := (t1, t2) (at level 80, no associativity). - (* The prediates of the theory *) + (** The theory has to define the following predicates *) Variable decodesAt : T -> T -> Prop. Notation "t1 <: t2" := (decodesAt t1 t2) (at level 70, no associativity). @@ -46,10 +54,10 @@ Section IDL. Variable hostSubtypeOf : S -> S -> Prop. Notation "s1 <<: s2" := (hostSubtypeOf s1 s2) (at level 70, no associativity). - (* Service Identifiers *) + (** This is generic in the set of service identifiers *) Variable I : Set. - (* Judgements *) + (** ** Judgements *) Inductive Assertion : Set := | HasType : I -> S -> Assertion | HasRef : I -> I -> S -> Assertion. @@ -108,17 +116,19 @@ Section IDL. Definition StateSound (st : State) : Prop := forall A t1 t2 B, CanSend st A t1 t2 B -> t1 <: t2. + + (** The final soundness proposition *) Definition IDLSound : Prop := forall s, clos_refl_trans _ step Empty_set s -> StateSound s. - (* Now we continue with the soundness proof for canonical subtyping. + (** * Canonical subtyping *) - We do so by just adding more hypotheses to this Section. - This is fine for now; when we actually want to instantiate this proof - with an actual IDL, we may want to revisit this, and maybe - modularize this development. - *) + (** + We continue with the soundness proof for canonical subtyping. + + We do so by just adding more hypotheses to this Section. + *) Hypothesis decodesAt_refl: reflexive _ decodesAt. Hypothesis decodesAt_trans: transitive _ decodesAt. @@ -137,7 +147,7 @@ Section IDL. Hypothesis host_subtyping_sound: forall s1 s2, s1 <<: s2 -> s1 <:: s2. - (* + (** Now the actual proofs. When I was writing these, my Coq has become pretty rusty, so these are rather manual proofs, with little automation. The style is heavily influenced by the explicit Isar-style diff --git a/coq/MiniCandid.v b/coq/MiniCandid.v index edcf02254..0b0a0daf8 100644 --- a/coq/MiniCandid.v +++ b/coq/MiniCandid.v @@ -1,4 +1,4 @@ -(* +(** MiniCandid: A formalization of the core ideas of Candid *) @@ -20,7 +20,15 @@ Set Default Goal Selector "!". Require Import candid.NamedCases. Set Printing Goal Names. (* Coqide doesn’t use it yet, will be in 8.13 *) -(* Types are coinductive (we do not want to model the graph structure explicilty) *) +(** +* Types + +We begin by defining the Candid types (or at least some of them). + +Candid types are inherently coinductive (e.g. <>), so we describe +them as a coinductive relation. This way we don’t have to model an explicit graph +structure in Coq. +*) CoInductive T := | NatT: T | IntT: T @@ -31,7 +39,13 @@ CoInductive T := | ReservedT : T . -(* Some unspecified value representation for references *) +(** +* Values + +Values are inductive. + +We use an unspecified type to model refereneces (could have used [String] too) +*) Axiom RefV : Type. Inductive V := @@ -42,8 +56,12 @@ Inductive V := | FuncV : RefV -> V | ReservedV : V . +(** -(* This is a stand in for `null <: t` in places where <: is not allowed yet. *) +* Typing and subtyping + +The following is a stand in for `null <: t` in places where <: is not allowed yet. +*) Definition is_opt_like_type (t : T) : bool := match t with | NullT => true @@ -53,15 +71,7 @@ Definition is_opt_like_type (t : T) : bool := end. -Definition is_not_opt_like_value (v : V) : Prop := -match v with -| NullV => False -| SomeV _ => False -| ReservedV => False -| _ => True -end. - -(* The boring, non-subtyping typing relation. *) +(** The boring, non-subtyping typing relation. *) Inductive HasType : V -> T -> Prop := | NatHT: case natHT, @@ -86,7 +96,7 @@ Inductive HasType : V -> T -> Prop := ReservedV :: ReservedT where "v :: t" := (HasType v t). - +(** The subtyping relation *) Reserved Infix "<:" (at level 80, no associativity). CoInductive Subtype : T -> T -> Prop := | ReflST : @@ -113,6 +123,11 @@ CoInductive Subtype : T -> T -> Prop := forall t, t <: ReservedT where "t1 <: t2" := (Subtype t1 t2). +(** +Subtyping is reflexive and transitive. + +Note that these are coinductive proofs! (And yet so neat) +**) Theorem subtyping_refl: reflexive _ Subtype. Proof. intros x. apply ReflST; constructor. Qed. @@ -124,19 +139,17 @@ Proof. intros t1 t2 t3 H1 H2. inversion H1; subst; clear H1; inversion H2; subst; clear H2; - name_cases; - try (constructor; firstorder). + constructor; firstorder. Qed. -(* +(** Subtyping is undecidable, at least the way we model it in Coq. -So let’s pretend it is. +But for the decoding function we have to pretend it is decidable. *) Axiom subtyping_decidable: forall t1 t2, {t1 <: t2} + { ~(t1 <: t2) }. Infix "<:?" := subtyping_decidable (at level 80, no associativity). - Lemma subtype_dec_true: forall T t1 t2 (x y : T), t1 <: t2 -> (if t1 <:? t2 then x else y) = x. Proof. intros. destruct (t1 <:? t2); intuition. Qed. @@ -149,12 +162,15 @@ Lemma subtype_dec_refl: forall T t (x y : T), (if t <:? t then x else y) = x. Proof. intros. apply subtype_dec_true. named_constructor. Qed. -(* +(** + +* Coercion function + 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 RHS of invalid cases. +We use [NullV] on the right-hand side in invalid branches. *) Function coerce (t1 : T) (t2 : T) (v1 : V) : V := @@ -169,7 +185,7 @@ Function coerce (t1 : T) (t2 : T) (v1 : V) : V := then SomeV (coerce t1 t2 v) else NullV - (* We’d prefer the equation from coerce_consituent_eq below, + (* We’d prefer the equation from [coerce_consituent_eq] below, but that will not satisfy the termination checker, so let’s repeat all the above ruls for OptT again. *) @@ -182,7 +198,7 @@ Function coerce (t1 : T) (t2 : T) (v1 : V) : V := | v, t, ReservedT => ReservedV - (* Failure is NullV. This also subsumes “valid” rules for NullV *) + (* Failure is NullV. Also subsumes “valid” rules that return NullV *) | _, _, _ => NullV end. @@ -223,7 +239,9 @@ Proof. } Qed. -(* Let’s try to create a suitable induction principle for this function *) +(** +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), (case natC, forall n, P NatT NatT (NatV n) (NatV n)) -> @@ -386,6 +404,11 @@ Proof. } Qed. +(** +* Properties of coercion + +Round-tripping +*) Lemma coerce_roundtrip: forall t1 v1, v1 :: t1 -> @@ -404,6 +427,10 @@ Proof. [reservedC]: { inversion H; subst; clear H; congruence. } Qed. +(** +Coercion does not fail (and is well-defined) +*) + Lemma coerce_well_defined: forall t1 t2 v1, t1 <: t2 -> v1 :: t1 -> @@ -414,12 +441,9 @@ Proof. Qed. -Lemma is_not_opt_like_type_contravariant: - forall t1 t2, - is_opt_like_type t1 = false -> t2 <: t1 -> is_opt_like_type t2 = false. -Proof. intros. destruct t1, t2; easy. Qed. +(** +* IDL Soundess -(* To work towards IDL soundness, we need a predicate for “Value v contains a function reference at function type t.”. Moreover, this contains relation should indicate the position in the value in a way that @@ -433,9 +457,10 @@ Inductive Path := | The : Path -> Path . -(* +(** And a function that finds the value at a given path. -It returns None if the path does not make sense for this value. + +It returns [None] if the path does not make sense for this value. *) Fixpoint val_idx (p : Path) (v : V) : option V := match p with @@ -447,8 +472,8 @@ Fixpoint val_idx (p : Path) (v : V) : option V := end end. -(* -This is a lenitent variant, which is total (returning NoneV +(** +This is a lenitent variant, which is total (returning [NullV] when the path is invalid), which makes proofs simpler. It also ignores extra [The] on the path; this way one can @@ -467,7 +492,7 @@ Fixpoint val_idx' (p : Path) (v : V) : V := end end. -(* +(** The corresponding function for types, also lenitent. *) Fixpoint typ_idx' (p : Path) (t : T) : T := @@ -482,6 +507,9 @@ Fixpoint typ_idx' (p : Path) (t : T) : T := end end. +(** +Properties about [val_idx] and [typ_idx'], mostly for sanity-checking +*) Lemma path_preserves_types: forall v v' t p, v :: t -> @@ -500,6 +528,34 @@ Proof. all: firstorder congruence. Qed. +Lemma val_idx_is_val_idx': + forall v v' t p, + v :: t -> + val_idx p v = Some v' -> + val_idx' p v = v'. +Proof. + intros v v' t p. + revert v v' t. + induction p. + * intros v v' t HHT Hval_idx. + inversion Hval_idx; subst; clear Hval_idx. + reflexivity. + * intros v v' t HHT Hval_idx. + inversion Hval_idx; subst; clear Hval_idx. + inversion HHT; subst; clear HHT; name_cases. + all: firstorder congruence. +Qed. + +(** +The core lemma towards compositionality: + +All values in a decoded value originate from a value in the original value, +and their types are related. + +This may be proving a bit more than needed for compositionality, but it my be +handy for other things. +*) + Lemma no_new_values: forall t1 t2 v1, t1 <: t2 -> @@ -575,6 +631,9 @@ Proof. } Qed. +(** +This is the instantiation of [passesThrough] from the IDL-Soundness theory. +*) Definition passesThrough (s1 : T * T) (t1 : T) (s2 : T * T) (t2 : T) := exists v1 p r, v1 :: t1 /\ @@ -583,7 +642,9 @@ Definition passesThrough (s1 : T * T) (t1 : T) (s2 : T * T) (t2 : T) := val_idx p (coerce t1 t2 v1) = Some (FuncV r) /\ typ_idx' p t2 = FuncT (fst s2) (snd s2). - +(** +And indeed subtyping is compositional: +*) Lemma compositional: forall t1 t2 s1 s2, t1 <: t2 -> passesThrough s1 t1 s2 t2 -> (snd s1 <: snd s2 /\ fst s2 <: fst s1). @@ -601,6 +662,9 @@ Proof. destruct H4; congruence. Qed. +(** +Now we can instantiate the soundness theorem from IDLSoundness +*) Require Import candid.IDLSoundness. @@ -632,4 +696,5 @@ Proof. destruct s2 as [ta2 tr2]. unfold service_subtyping. intuition. -Qed. \ No newline at end of file +Qed. + From 854ded5907983ca7c6e506df3fbf3d356d88ad4b Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 29 Jan 2021 16:57:26 +0100 Subject: [PATCH 17/22] Stash transitive coherence --- coq/MiniCandid.v | 93 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 93 insertions(+) diff --git a/coq/MiniCandid.v b/coq/MiniCandid.v index 0b0a0daf8..c75b1dd7c 100644 --- a/coq/MiniCandid.v +++ b/coq/MiniCandid.v @@ -239,6 +239,14 @@ Proof. } Qed. +Lemma coerce_reservedT: + forall v t1, coerce t1 ReservedT v = ReservedV. +Proof. + intros v1 t1. + destruct v1, t1; reflexivity. +Qed. + + (** This beast of a lemma defines and proves a nice induction principle for [coerce]. *) @@ -698,3 +706,88 @@ Proof. intuition. Qed. +(** +* Transitive coherence + +Transitive coherence only holds up to a weaker relation: +*) + +Reserved Infix "[=" (at level 80, no associativity). +CoInductive UpToNull : V -> V -> Prop := + (* This is the interesting rule: *) + | NullSomeUT: + forall v, + NullV [= SomeV v + + (* The rest just form the homomorphic closure *) + | NatUT: + forall n, NatV n [= NatV n + | IntUT: + forall n, IntV n [= IntV n + | NullUT: + NullV [= NullV + | SomeUT: + forall v1 v2, + v1 [= v2 -> + SomeV v1 [= SomeV v2 + | FuncUT: + forall r, FuncV r [= FuncV r + | ReservedUT: + ReservedV [= ReservedV +where "v1 [= v2" := (UpToNull v1 v2). + +Lemma UpToNull_refl: + forall v, UpToNull v v. +Proof. intros. induction v; constructor; assumption. Qed. + +Ltac destruct_match := + match goal with + | [ H :context[match ?a with _ => _ end] |- _] => + let Heq := fresh "Heq" in + destruct a eqn:Heq + | [ |- context[match ?a with _ => _ end]] => + let Heq := fresh "Heq" in + destruct a eqn:Heq + end. + +Theorem transitive_coherence: + forall ta tb tc v1, + ta <: tb -> + tb <: tc -> + v1 :: ta -> + coerce tb tc (coerce ta tb v1) [= coerce ta tc v1. +Proof. + intros ta tb tc v1 HST1 HST2 HHT. + revert tc HST2. + revert ta tb v1 HST1 HHT. + apply (coerce_nice_ind (fun ta tb v1 v2 => + forall tc : T, + forall HST2 : tb <: tc, + coerce tb tc v2 [= coerce ta tc v1 + )); intros; + inversion HST2; subst; clear HST2. + all: simpl. + all: try rewrite coerce_consituent_eq by assumption. + all: try rewrite coerce_reservedT. + all: try rewrite subtype_dec_refl. + all: try rewrite subtype_dec_true by assumption. + all: try apply UpToNull_refl. + all: try solve [destruct t2; try apply UpToNull_refl; apply NullSomeUT]. + all: try solve [repeat destruct_match; try apply UpToNull_refl; try apply NullSomeUT]. + * constructor. apply H1. named_constructor. + * repeat destruct_match; try apply UpToNull_refl; try apply NullSomeUT. + - constructor. apply H1. assumption. + - contradiction n. eapply subtyping_trans; eassumption. + * rewrite H0. + constructor. apply H3. named_constructor. + * (* reservedC_optST *) + repeat destruct_match; try apply UpToNull_refl; try apply NullSomeUT. + - admit. (* stuck here! *) + - constructor. apply H3. assumption. + - contradiction n. eapply subtyping_trans; eassumption. + * destruct t2; try apply UpToNull_refl. + repeat destruct_match; try apply UpToNull_refl; try apply NullSomeUT. + - contradiction n. eapply subtyping_trans; eassumption. + - contradiction n. eapply subtyping_trans; eassumption. + * destruct t, v; simpl; repeat destruct_match; try apply UpToNull_refl; try apply NullSomeUT. +Abort. \ No newline at end of file From 380a0ee4d7ff21de05ef58de3ca81f3cc76615bf Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 1 Feb 2021 10:08:59 +0100 Subject: [PATCH 18/22] Transitive coherence --- coq/MiniCandid.v | 66 +++++++++++++++++++++++++++--------------------- 1 file changed, 37 insertions(+), 29 deletions(-) diff --git a/coq/MiniCandid.v b/coq/MiniCandid.v index c75b1dd7c..5145950ab 100644 --- a/coq/MiniCandid.v +++ b/coq/MiniCandid.v @@ -246,7 +246,6 @@ Proof. destruct v1, t1; reflexivity. Qed. - (** This beast of a lemma defines and proves a nice induction principle for [coerce]. *) @@ -712,34 +711,38 @@ Qed. Transitive coherence only holds up to a weaker relation: *) -Reserved Infix "[=" (at level 80, no associativity). +Reserved Infix "~~" (at level 80, no associativity). CoInductive UpToNull : V -> V -> Prop := (* This is the interesting rule: *) | NullSomeUT: forall v, - NullV [= SomeV v + NullV ~~ SomeV v + | SomeNullUT: + forall v, + SomeV v ~~ NullV (* The rest just form the homomorphic closure *) | NatUT: - forall n, NatV n [= NatV n + forall n, NatV n ~~ NatV n | IntUT: - forall n, IntV n [= IntV n + forall n, IntV n ~~ IntV n | NullUT: - NullV [= NullV + NullV ~~ NullV | SomeUT: forall v1 v2, - v1 [= v2 -> - SomeV v1 [= SomeV v2 + v1 ~~ v2 -> + SomeV v1 ~~ SomeV v2 | FuncUT: - forall r, FuncV r [= FuncV r + forall r, FuncV r ~~ FuncV r | ReservedUT: - ReservedV [= ReservedV -where "v1 [= v2" := (UpToNull v1 v2). + ReservedV ~~ ReservedV +where "v1 ~~ v2" := (UpToNull v1 v2). Lemma UpToNull_refl: forall v, UpToNull v v. Proof. intros. induction v; constructor; assumption. Qed. +(** A small tactic that I keep copying into each development *) Ltac destruct_match := match goal with | [ H :context[match ?a with _ => _ end] |- _] => @@ -755,7 +758,7 @@ Theorem transitive_coherence: ta <: tb -> tb <: tc -> v1 :: ta -> - coerce tb tc (coerce ta tb v1) [= coerce ta tc v1. + coerce tb tc (coerce ta tb v1) ~~ coerce ta tc v1. Proof. intros ta tb tc v1 HST1 HST2 HHT. revert tc HST2. @@ -763,31 +766,36 @@ Proof. apply (coerce_nice_ind (fun ta tb v1 v2 => forall tc : T, forall HST2 : tb <: tc, - coerce tb tc v2 [= coerce ta tc v1 - )); intros; - inversion HST2; subst; clear HST2. + coerce tb tc v2 ~~ coerce ta tc v1 + )); intros; inversion HST2; subst; clear HST2. all: simpl. all: try rewrite coerce_consituent_eq by assumption. all: try rewrite coerce_reservedT. all: try rewrite subtype_dec_refl. all: try rewrite subtype_dec_true by assumption. - all: try apply UpToNull_refl. - all: try solve [destruct t2; try apply UpToNull_refl; apply NullSomeUT]. - all: try solve [repeat destruct_match; try apply UpToNull_refl; try apply NullSomeUT]. - * constructor. apply H1. named_constructor. - * repeat destruct_match; try apply UpToNull_refl; try apply NullSomeUT. + all: try solve [ + repeat destruct_match; + try apply UpToNull_refl; + intuition constructor + ]. + all: name_cases. + [optSomeC_reflST]: { constructor. apply H1. named_constructor. } + [optSomeC_optST]: { + repeat destruct_match; try apply UpToNull_refl; try apply NullSomeUT. - constructor. apply H1. assumption. - contradiction n. eapply subtyping_trans; eassumption. - * rewrite H0. + } + [constituentOptC_reflST]: { + rewrite H0. constructor. apply H3. named_constructor. - * (* reservedC_optST *) + } + [constituentOptC_optST]: { repeat destruct_match; try apply UpToNull_refl; try apply NullSomeUT. - - admit. (* stuck here! *) + - constructor. - constructor. apply H3. assumption. - contradiction n. eapply subtyping_trans; eassumption. - * destruct t2; try apply UpToNull_refl. - repeat destruct_match; try apply UpToNull_refl; try apply NullSomeUT. - - contradiction n. eapply subtyping_trans; eassumption. - - contradiction n. eapply subtyping_trans; eassumption. - * destruct t, v; simpl; repeat destruct_match; try apply UpToNull_refl; try apply NullSomeUT. -Abort. \ No newline at end of file + } + [reservedC_optST]: { + destruct t, v; simpl; repeat destruct_match; try apply UpToNull_refl; try apply NullSomeUT. + } +Qed. \ No newline at end of file From 395e1b2252307ddc84e628183fb675716c05813a Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Tue, 9 Feb 2021 12:45:57 +0100 Subject: [PATCH 19/22] typos --- coq/MiniCandid.v | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/coq/MiniCandid.v b/coq/MiniCandid.v index 5145950ab..8b7c8ffcf 100644 --- a/coq/MiniCandid.v +++ b/coq/MiniCandid.v @@ -185,7 +185,7 @@ Function coerce (t1 : T) (t2 : T) (v1 : V) : V := then SomeV (coerce t1 t2 v) else NullV - (* We’d prefer the equation from [coerce_consituent_eq] below, + (* We’d prefer the equation from [coerce_constituent_eq] below, but that will not satisfy the termination checker, so let’s repeat all the above ruls for OptT again. *) @@ -203,7 +203,7 @@ Function coerce (t1 : T) (t2 : T) (v1 : V) : V := end. (* We can prove the desired equation at least as an equality *) -Lemma coerce_consituent_eq: +Lemma coerce_constituent_eq: forall v t1 t2, v :: t1 -> is_opt_like_type t1 = false -> @@ -301,7 +301,7 @@ Proof. [natIntST]: { apply NatIntC; clear_names. } [optST]: { (* oddly, - rewrite coerce_consituent_eq by (try named_constructor; reflexivity). + rewrite coerce_constituent_eq by (try named_constructor; reflexivity). does not seem to lead to a simpler proof here. *) destruct (is_opt_like_type t0) eqn:His_opt_like. @@ -480,7 +480,7 @@ Fixpoint val_idx (p : Path) (v : V) : option V := end. (** -This is a lenitent variant, which is total (returning [NullV] +This is a lenient variant, which is total (returning [NullV] when the path is invalid), which makes proofs simpler. It also ignores extra [The] on the path; this way one can @@ -500,7 +500,7 @@ Fixpoint val_idx' (p : Path) (v : V) : V := end. (** -The corresponding function for types, also lenitent. +The corresponding function for types, also lenient. *) Fixpoint typ_idx' (p : Path) (t : T) : T := match p with @@ -610,7 +610,7 @@ Proof. repeat split. - right; named_constructor. - assumption. - - rewrite coerce_consituent_eq by assumption. + - rewrite coerce_constituent_eq by assumption. rewrite H0. rewrite subtype_dec_true by assumption. congruence. * specialize (H3 _ _ H5). @@ -623,7 +623,7 @@ Proof. repeat split. - left; reflexivity. - assumption. - - rewrite coerce_consituent_eq by assumption. + - rewrite coerce_constituent_eq by assumption. destruct H1. * rewrite H1. destruct (t1 <:? t2); reflexivity. * rewrite subtype_dec_false by assumption. reflexivity. @@ -769,7 +769,7 @@ Proof. coerce tb tc v2 ~~ coerce ta tc v1 )); intros; inversion HST2; subst; clear HST2. all: simpl. - all: try rewrite coerce_consituent_eq by assumption. + all: try rewrite coerce_constituent_eq by assumption. all: try rewrite coerce_reservedT. all: try rewrite subtype_dec_refl. all: try rewrite subtype_dec_true by assumption. @@ -798,4 +798,4 @@ Proof. [reservedC_optST]: { destruct t, v; simpl; repeat destruct_match; try apply UpToNull_refl; try apply NullSomeUT. } -Qed. \ No newline at end of file +Qed. From ef6fbb5ee148a5c81afbe282aa4c15c2f00a12c3 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 7 Apr 2021 10:01:38 +0200 Subject: [PATCH 20/22] Comment about case constituentOptC --- coq/MiniCandid.v | 3 +++ 1 file changed, 3 insertions(+) diff --git a/coq/MiniCandid.v b/coq/MiniCandid.v index 8b7c8ffcf..61bfc58d4 100644 --- a/coq/MiniCandid.v +++ b/coq/MiniCandid.v @@ -270,6 +270,9 @@ Lemma coerce_nice_ind: 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 -> From 4b56140633b762715c6a8bab9d09915eef5f296a Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 23 Apr 2021 09:52:12 +0200 Subject: [PATCH 21/22] Update spec/Candid.md --- spec/Candid.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/Candid.md b/spec/Candid.md index d7d634ed1..399e83b69 100644 --- a/spec/Candid.md +++ b/spec/Candid.md @@ -910,7 +910,7 @@ NB: No rule is needed for type `empty`, because there are no values of that type Vectors coerce pointwise: ``` -C[vec <: vec ]( vec { ;* } ) = vec { c[ <: ]();* } +C[vec <: vec ]( vec { ;* } ) = vec { C[ <: ]();* } ``` #### Options From abecd6bf739ffb4951b798d32440de06bed28e1b Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 23 Apr 2021 09:53:06 +0200 Subject: [PATCH 22/22] Merge mistake --- spec/Candid.md | 1 + 1 file changed, 1 insertion(+) diff --git a/spec/Candid.md b/spec/Candid.md index 399e83b69..72f0c4d3e 100644 --- a/spec/Candid.md +++ b/spec/Candid.md @@ -916,6 +916,7 @@ C[vec <: vec ]( vec { ;* } ) = vec { C[ <: ]();* } #### Options The null type coerces into any option type: +``` C[null <: opt ](null) = null ```