fix: Compile run-time constraint checks for newtypes in comprehensions

[RustanLeino]

Comprehensions can declare their bound variables to be of types that have constraint (e.g., subset types). These are (in the general case) compiled into run-time checks. However, this machinery did not pay attention to newtypes, which also have constraints. This PR fixes this, so that bound comprehension variables of newtype types also compile into run-time checks.

The new functionality is tested in git-issues/git-issue-697i.dfy and git-issues/git-issue-697j.dfy.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[keyboardDrummer]

Can newtypes not be converted to subset types before code generation? Why is there back-end specific code for them?

[RustanLeino]

Can newtypes not be converted to subset types before code generation? Why is there back-end specific code for them?

No. Well, at least not all newtypes. Because a newtype is kept separate from its base type, compilers are given the freedom to use a different binary representation for the newtype. This means that a newtype may, for example, be represented as a 32-bit integer at run time, whereas its base type may be a BigInteger.

[keyboardDrummer]

Can newtypes not be converted to subset types before code generation? Why is there back-end specific code for them?

No. Well, at least not all newtypes. Because a newtype is kept separate from its base type, compilers are given the freedom to use a different binary representation for the newtype. This means that a newtype may, for example, be represented as a 32-bit integer at run time, whereas its base type may be a BigInteger.

I see.

Still, I have a feeling lots of code generation elements are conflated at the moment. Would you mind helping me come up with a plan to extract much of the subset and newtype handling in code generation to a separate pass? I think it would already be a great step if we only write down what we'd like.

I imagine we could have a pass "InstantiateComprehensionPredicateTypeFilters" that inlines the predicates from subset and newtypes in comprehensions, so that the implicit filter operation (if I understand correctly), is made explicit. Should this pass run as part of the resolver? Could it help with verification as well?

A phase after the comprehension filter instantiation, could annotate matching newtypes with {:extern "nameOfNativeType"} so they map to native types, and then remove their predicate. Another phase could replace subset types with their basetypes.

[RustanLeino]

Still, I have a feeling lots of code generation elements are conflated at the moment. Would you mind helping me come up with a plan to extract much of the subset and newtype handling in code generation to a separate pass? I think it would already be a great step if we only write down what we'd like.

Yes. Great! There are many little things to improve. The main difference between subset types and newtypes is in the resolver. The compiler could do well to focus on what types are to be compiled as "nativeType" or, as you put it, "extern". There's also a slight (but really unnecessary) difference in the handling of subset types / newtypes, because a newtype may not have a .Var and thus its base type is retrieved in a different way in the code. The RedirectingTypeDecl interface also includes type synonyms (I think), so this would also be nice to make more specific for subset types + newtypes.

[keyboardDrummer]

Still, I have a feeling lots of code generation elements are conflated at the moment. Would you mind helping me come up with a plan to extract much of the subset and newtype handling in code generation to a separate pass? I think it would already be a great step if we only write down what we'd like.

Yes. Great! There are many little things to improve. The main difference between subset types and newtypes is in the resolver. The compiler could do well to focus on what types are to be compiled as "nativeType" or, as you put it, "extern". There's also a slight (but really unnecessary) difference in the handling of subset types / newtypes, because a newtype may not have a .Var and thus its base type is retrieved in a different way in the code. The RedirectingTypeDecl interface also includes type synonyms (I think), so this would also be nice to make more specific for subset types + newtypes.

How do you feel about what I described though, which I hope would make all back-ends completely agnostic to subset and newtypes?

[RustanLeino]

@keyboardDrummer Yes, I like your suggested plan. A pass to compute the predicates would fit nicely in the resolver, so that all compilers could use the information. Here are some thoughts from the top of my head:

• When gathering those predicates, one needs to be mindful of the types when going up the base-type chain, because those types may have different native types. For example:

  type Nat = w: int | 0 <= w
  newtype Word = x: Nat | x < 0x1_0000_0000
  type EvenWord = y: Word | y % 2 == 0
  newtype EvenByte = z: EvenWord | z < 256

  Here, a Word is probably represented in the target language as a uint32 and an EvenByte as a uint8. So, to make sure an arbitrary uint8 b is an EvenByte, one needs a predicate like:

  0 <= (b as Word as int) && (b as Word) < 0x1_0000_0000 && (b as Word) % 2 == 0 && b < 256

  Going in the other direction, as would be required as run time to evaluate i is EvenByte where i has Dafny type int, one needs a predicate like:

  0 <= i && i < 0x1_0000_0000 && (i as Word) % 2 == 0 && (i as Word) < 256

• The verifier already encodes the information about each type using predicates like $Is(..., EvenWord). It has no notion of "native types"--the verifier encodes everything as its ancestor type (int in the example above). The verifier doesn't distinguish between subtype types and newtypes, except that, for newtypes, it needs to check constraints for every intermediate subexpression--this type information is already computed by the resolver.

• It would not be a good idea for the resolver to replace subset types / newtypes with their base types, because the verifier needs to know the name of the type. For example, the verifier knows that a reference of type array<nat> is different from a reference of type array<int>, even though they have the same compiler-target representation.