Some more tests related to subtyping by nomeata · Pull Request #126 · dfinity/candid

nomeata · 2020-10-30T10:37:08Z

this adds some tests to account for the new behaviour of
https://github.com/dfinity/candid/pull/110f

Just a first stab, untested, and kinda running out of stream.

this adds some tests to account for the new behaviour of https://github.com/dfinity/candid/pull/110f Just a first stab, untested, and kinda running out of stream.

nomeata · 2020-10-30T10:43:00Z

I am getting

Checking 61 opt: parsing null : null...thread 'decode_test_test_construct_test_did' panicked at 'called `Result::unwrap()` on an `Err` value: Custom("type mismatch: null cannot be of type opt empty")', rust/candid/tests/test_suite.rs:11:16

which sounds like a lie (sure null can be of type opt t).

Also, it might be helpful to not number the tests squentially, but use the line number to identify them, makes it easier to to jump to them. This is what the test driver in Motoko is doing.

nomeata · 2020-10-30T11:07:33Z

I could fix this with

--- a/rust/candid/src/parser/value.rs
+++ b/rust/candid/src/parser/value.rs
@@ -154,7 +154,7 @@ impl IDLValue {
                 let ty = crate::types::internal::find_type(id).unwrap();
                 self.annotate_type(from_parser, env, &ty)?
             }
-            (IDLValue::Null, Type::Opt(_)) if from_parser => IDLValue::None,
+            (IDLValue::Null, Type::Opt(_)) => IDLValue::None,
             (IDLValue::Float64(n), Type::Float32) if from_parser => IDLValue::Float32(*n as f32),
             (IDLValue::Number(str), t) if from_parser => match t {
                 Type::Int => IDLValue::Int(str.parse::<Int>()?),

but then it seems the distinction between IDLValue::Null and IDLValue::None may not be needed. It is not clear to me why we’d need that – in the algebra of untyped values, they are the same, aren’t they?

Now at

Checking 67 opt: parsing opt true : opt bool...thread 'decode_test_test_construct_test_did' panicked at 'called `Result::unwrap()` on an `Err` value: Custom("type mismatch: false cannot be of type opt bool")', rust/candid/tests/test_suite.rs:11:16

which means that the rule

not (null <: <datatype>)
<datatype> <: <datatype'>
-----------------------------
<datatype> <: opt <datatype'>

(which I find dubious, non-compositional, and wouldn’t be surprised if it breaks stuff) is not implemented. Will leave this to @chenyan-dfinity at this point.

chenyan-dfinity · 2020-10-30T17:06:52Z

it seems the distinction between IDLValue::Null and IDLValue::None may not be needed.

In the untype setting, we need IDLValue::Null to represent null of type null and IDLValue::None to represent null of type opt T. The parser always parses null to be IDLValue::Null, and we need the if from_parser guard to ensure we don't change between null and none after the first type annotation.

The whole set of opt subtyping rules are not implemented. I will take a look to see the right place to add these.

chenyan-dfinity · 2020-10-30T17:10:46Z

+assert blob "DIDL\00\01\7e\02"                                                 !: (opt bool) "opt: parsing invalid bool at opt bool";
+assert blob "DIDL\01\6e\7f\01\00\00" == "(null)"                                : (opt opt null) "opt: parsing (null : opt null) at opt opt null gives null, not opt null";
+
+// special opt and record subtyping


Also some tests for opt variant?

yes, didn't get to variant yes :-)

nomeata · 2020-11-02T09:11:20Z

it seems the distinction between IDLValue::Null and IDLValue::None may not be needed.

In the untype setting, we need IDLValue::Null to represent null of type null and IDLValue::None to represent null of type opt T. The parser always parses null to be IDLValue::Null, and we need the if from_parser guard to ensure we don't change between null and none after the first type annotation.

Right, but why do you even have to distinguish the two? It’s not that IDLValue::None tells you the type of it (you still don’t know T). What breaks if you only use IDLValue::Null everywhere?

This is a significant rewirte of the section in the spec describing deserialization. Some points worth noting: * This replaces the elaboration relation with one that takes a value and a type as input, and returns a value. This makes it clearer that there is no “input _type_” of deeper relevance. * One great benefit: No more long prose about how the rules assume these types to be principal, even if they aren’t. This clarifies questions like [this one](#126 (comment)) * Also, the existing rules about “elaborating function values” were kinda bogus, as function values are just accepted as they are. This is much easier now, also good. * Unfortuantely for this application, our textual representation has overloading. Instead of defining yet another abstract value algebra, I did a bit of hand-waving, and defined an “overloading-free fragment” of the textual format for this section. * A fair number of rules becomes simpler. Promising! * I was able to phrase some interesting properties more formally. Also promising! Didn’t actually prove them, though, althogh we should. * Still unclear to me what we mean with “subtyping is complete”, see the section there. * Decoding is still an inductive relation, so not fully algorithmic. This may be an issue with a stright-forward formalization; not all theorem provers like negative occurrences of inductive relations in their rules. * Syntax of the relations up for discussion.

chenyan-dfinity · 2020-11-02T17:54:49Z

Right, but why do you even have to distinguish the two? It’s not that IDLValue::None tells you the type of it (you still don’t know T). What breaks if you only use IDLValue::Null everywhere?

Ah right. It was a workaround when we don't have type annotations. Yes, this is not necessary now.

nomeata · 2020-11-03T09:36:33Z

Ah right. It was a workaround when we don't have type annotations. Yes, this is not necessary now.

Gave it a shot, but still needed internally in the current code structure, because idl_serialize only takes an IDLValue, but not the type, so when serializing null it is unclear which form it should take. This is a bit fishy, and is also the reason why the IDLValue takes this idx that doesn’t really make sense for the generic IDLValue type.

The Spec solves this by making the M function indexed by the type to encode at, but I don’t feel like refactoring the rust code now :-)

nomeata · 2020-11-03T10:03:16Z

Just added a few nat <: int subtyping tests, and tried to add the subtyping.

It’s a bit hard that the test suite will panc (rather than report an error and continue) upon bad subtyping. The unwrap in HostTest.from_assert is causing problems.

…new-subtyping

nomeata · 2020-11-03T11:08:47Z

The rust code chanes might need some cleanup, feel free to push to this branch.

(see #131, spec update in #128)

This is a significant rewirte of the section in the spec describing deserialization. Some points worth noting: * This replaces the elaboration relation with one that takes a value and a type as input, and returns a value. This makes it clearer that there is no “input _type_” of deeper relevance. * One great benefit: No more long prose about how the rules assume these types to be principal, even if they aren’t. This clarifies questions like [this one](#126 (comment)) * Also, the existing rules about “elaborating function values” were kinda bogus, as function values are just accepted as they are. This is much easier now, also good. * Unfortuantely for this application, our textual representation has overloading. Instead of defining yet another abstract value algebra, I did a bit of hand-waving, and defined an “overloading-free fragment” of the textual format for this section. * A fair number of rules becomes simpler. Promising! * I was able to phrase some interesting properties more formally. Also promising! Didn’t actually prove them, though, although we should. * Still unclear to me what we mean with “subtyping is complete”, see the section there. * Decoding is still an inductive relation, so not fully algorithmic. This may be an issue with a stright-forward formalization; not all theorem provers like negative occurrences of inductive relations in their rules.

as per #134

causes a stack overflow. also see discussion in #135

this updates the test suite as per #137 and implements them (in a shoddy way)

this propagates coercion errors (via a special sentinel value), and recovers when parsing opt. It also implements subtyping-to-consitutient-type. The updated Candid test suite from dfinity/candid#126 passes, but I am not overly confident in it. More thorough randomized testing would be needed.

nomeata · 2020-11-20T08:03:13Z

Thanks for looking at the code. Feel free to take over and change the rust code in whatever way you see fit.

…d into joachim/test-new-subtyping

chenyan-dfinity

LGTM

nomeata added 2 commits October 30, 2020 11:35

Some more tests related to subtyping

57bdd3b

this adds some tests to account for the new behaviour of https://github.com/dfinity/candid/pull/110f Just a first stab, untested, and kinda running out of stream.

I guess this one is good now

671c80f

nomeata mentioned this pull request Oct 30, 2020

Meta-issue: Mercury backlog burndown caffeinelabs/motoko#2078

Closed

30 tasks

Allow null : opt t subtyping?

92fa86c

chenyan-dfinity reviewed Oct 30, 2020

View reviewed changes

nomeata mentioned this pull request Nov 2, 2020

Spec: Refactor description of deserialization #128

Merged

nomeata added 3 commits November 3, 2020 10:43

Test case: add nat <: int tests

23520f6

nat/int subtyping

c666291

Can the test suite be more liberal?

82b71f4

nomeata added 8 commits November 3, 2020 11:08

stash

0b3e1a9

Merge branch 'master' of github.com:dfinity/candid into joachim/test-…

a4a3af9

…new-subtyping

Undo changes to test suite runnter

688b236

comment

2173a51

reserved <: opt t

7196f9b

Fix test cases (forgot about a-normal-form)

66624c2

Fix more test cases

4cb1d32

Optional record fiels are optional

47d5fc5

nomeata marked this pull request as ready for review November 3, 2020 11:08

Reserved fields may be missing

429ea4a

(see #131, spec update in #128)

Merge branch 'master' into joachim/test-new-subtyping

236638f

nomeata added 7 commits November 13, 2020 14:19

Run cargo-fmt

b6a246e

Test case for reserved <: opt nat

e96249c

as per #134

Add true : fix opt test

7aae87f

causes a stack overflow. also see discussion in #135

Update tests for opt-via-consituent type rules

3924e4c

this updates the test suite as per #137 and implements them (in a shoddy way)

cargo-fmt

4634331

More tests about variants

55f0e8c

fix maxint tests

eb1547d

nomeata mentioned this pull request Nov 18, 2020

Candid deserialization: New opt subtyping caffeinelabs/motoko#2129

Merged

nomeata and others added 7 commits November 19, 2020 12:17

Fun test case with fix record <: fix (opt . record)

f037f1d

It shouldn’t actually decode

dc5deec

Run cargo fix

007e7bd

Fix cargo clippy

e6492ab

Merge branch 'master' into joachim/test-new-subtyping

52fa2bd

More clippy

5e2813a

refactor

1d841b9

nomeata and others added 4 commits November 20, 2020 15:53

More tests (this one showed a bug in Motoko)

a5a7f5a

Fix escaping of escapes

a259759

fix

5337a14

Merge branch 'joachim/test-new-subtyping' of github.com:dfinity/candi…

4038a19

…d into joachim/test-new-subtyping

chenyan-dfinity approved these changes Nov 20, 2020

View reviewed changes

Merge branch 'master' into joachim/test-new-subtyping

12a7795

nomeata merged commit f6f794f into master Nov 21, 2020

nomeata deleted the joachim/test-new-subtyping branch November 21, 2020 14:01

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Some more tests related to subtyping#126

Some more tests related to subtyping#126
nomeata merged 35 commits intomasterfrom
joachim/test-new-subtyping

nomeata commented Oct 30, 2020

Uh oh!

nomeata commented Oct 30, 2020

Uh oh!

nomeata commented Oct 30, 2020

Uh oh!

chenyan-dfinity commented Oct 30, 2020

Uh oh!

Uh oh!

chenyan-dfinity Oct 30, 2020

Uh oh!

nomeata Nov 2, 2020

Uh oh!

nomeata commented Nov 2, 2020

Uh oh!

chenyan-dfinity commented Nov 2, 2020

Uh oh!

nomeata commented Nov 3, 2020 •

edited

Loading

Uh oh!

nomeata commented Nov 3, 2020

Uh oh!

nomeata commented Nov 3, 2020

Uh oh!

nomeata commented Nov 20, 2020

Uh oh!

chenyan-dfinity left a comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

nomeata commented Oct 30, 2020

Uh oh!

nomeata commented Oct 30, 2020

Uh oh!

nomeata commented Oct 30, 2020

Uh oh!

chenyan-dfinity commented Oct 30, 2020

Uh oh!

Uh oh!

chenyan-dfinity Oct 30, 2020

Choose a reason for hiding this comment

Uh oh!

nomeata Nov 2, 2020

Choose a reason for hiding this comment

Uh oh!

nomeata commented Nov 2, 2020

Uh oh!

chenyan-dfinity commented Nov 2, 2020

Uh oh!

nomeata commented Nov 3, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

nomeata commented Nov 3, 2020

Uh oh!

nomeata commented Nov 3, 2020

Uh oh!

nomeata commented Nov 20, 2020

Uh oh!

chenyan-dfinity left a comment

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

nomeata commented Nov 3, 2020 •

edited

Loading