Coq: Model subtype check on decoding, IDL-Soundness, Transitive Coherence #171
Conversation
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).
Co-authored-by: Andreas Rossberg <rossberg@dfinity.org>
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?
nomeata
changed the title
|
(Should be merged after #168 hits master) |
rossberg
left a comment
rossberg
left a comment
There was a problem hiding this comment.
Cool stuff. I had to realise far behind the curve my Coq expertise is, so I probably only have superficial comments on definitions and theorems.
| (* 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. | ||
| *) |
There was a problem hiding this comment.
Hm, I'm confused why this does not need a case for e.g. OptT ReservedT?
There was a problem hiding this comment.
Which case exactly are you missing? (coerce has three parameters)
There was a problem hiding this comment.
I guess ResV, ResT, OptT ResT? (I was also wondering about OptT NullT, but I suppose that's covered by the default.)
There was a problem hiding this comment.
That is handled by the final NullV producing catch-all. Remember that the constituent-to-opt rule only applies to t <: opt t if not (null <: opt t).
So reserved <: opt reserved will always result null.
| 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. |
2 participants
A revamp of the Coq development:
It’s very annoying that Github Action artifacts, even if they are HTML, are not directly accessible with the browser.
Maybe setup Github pages?
It is still a Mini-Candid with a limited set of types, but I think it has all the interesting ones to cover the corner cases. Even adding vectors adds a lot of technical noise with little additional insight (see #154.)