From f173b92a2d464d06337b95a1bb357efe5ae178f1 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Sat, 30 Jan 2021 10:39:48 +0100 Subject: [PATCH] Meta-Theory: Clarify transitive coherence MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit I tried to prove the “weak transitive coherence” that we claim in Coq: 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. where [= allows more null on the left than on the right. I believed this holds, but the proof doesn't go through. A counter example is `bool <: opt bool <: opt opt bool`. Coercing `true` in two steps goes via `opt true` to `opt opt true`. Coercing directly goes to `null`, because the “constituent-to-opt” rule `t <: opt t'` requires that `t'` is a non-opt type. We added that restriction in 30f719fadbaccac for the reasons discussed in https://github.com/dfinity/candid/issues/135#issuecomment-728833245 This PR just updates the prose to not claim wrong things. (This is a good humbling reminder about how easy it is to go wrong when one does not do formal proofs.) --- spec/Candid.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/spec/Candid.md b/spec/Candid.md index 5e4e11091..f22cf883f 100644 --- a/spec/Candid.md +++ b/spec/Candid.md @@ -718,7 +718,7 @@ To summarize, the subtyping relation for validating upgrades is designed with th * No covert channels: Serialisation never includes any fields in the value that the sender is not aware of. Specifically, when passing on a value to a third party that the sender previously received itself, then that will only contain fields that the sender intends to send out per its type. However, something has to give, so one seemingly desirable property that is not maintained is *transitive coherence*, i.e., given a value serialized at some type, deserialized and serialized at a supertype, and then again deserialized at a supertype of the supertype may yield a diferent result than deserialised directly at the later supertype. -However, the only possible difference can be one of getting `null` for an option vs a non-null value. +However, the only possible difference can be one of getting `null` instead of an optional value, or vica versa. ### Rules @@ -1075,7 +1075,7 @@ The relations above have certain properties. To express them, we need the relati ``` 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 that `R(v3,v3')`, where `R` is the smallest homomorphic, reflexive, symmetric relation `R` that satisfies `∀ v. R(opt v, null)`. The goal of “subtyping completeness” has not been cast into a formal formulation yet.