Add Validatable trait

[robin-aws]

Closes #319

See issue for motivation.

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

[lavaleri]

AWS CodeBuild CI Report

• CodeBuild project: DafnyESDK
• Commit ID: 26d30ec
• Result: SUCCEEDED
• Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

[lavaleri]

AWS CodeBuild CI Report

• CodeBuild project: DafnyESDK
• Commit ID: d476453
• Result: FAILED
• Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

[lavaleri]

AWS CodeBuild CI Report

• CodeBuild project: DafnyESDK
• Commit ID: 20e91cd
• Result: FAILED
• Build Logs (available for 30 days)

Powered by github-codebuild-logs, available on the AWS Serverless Application Repository

[alex-chew]

Is there a benefit to writing ValidAndFresh() as opposed to Valid() && Fresh()? The former doesn't seem much more convenient, whereas the latter is easier to name (except perhaps for confusion between fresh() and Fresh()).

[robin-aws]

It's questionable whether this is worth the trouble. I definitely DON'T think just "Fresh" is the right word anyway, so I'd rather come up with better or just drop this predicate. I'm more just observing this is a very common pattern.

[RustanLeino]

This is great, since it gives us a central place to talk about the standard dynamic-frames idiom. Two general questions I have are:

• All members of trait Validatable are ghost. Yet, I imagine that there will be some code generated (in C# and Java) that says a class implements this empty interface. Does that have any negative consequences? (If so, we could think of some compiler directive that would say to ignore traits with only ghost members.)

• I'm thinking there may be a better name than Validable. Given the ValidComponent member, should the trait perhaps have a name like Composite?

[RustanLeino]

I think we should update the style guide. I suggest it be updated to say that "public" fields (or, at least, public ghost fields) be capitalized, where "public" means "intended to be used and understood by clients".

[robin-aws]

Should that also align with the set of symbols you export then?

[RustanLeino]

Having convenience predicates like this is fantastic!

[RustanLeino]

This postcondition is not necessary, since it just restates the body and functions are transparent (non-opaque) in Dafny (unless you limit visibility with an export clause, but you're not).

[robin-aws]

I was convinced this was necessary for validation for some reason, perhaps it was confounded with whatever the real fix was. Will try removing.

[RustanLeino]

Ditto. This postcondition is not necessary.

[robin-aws]

• All members of trait Validatable are ghost. Yet, I imagine that there will be some code generated (in C# and Java) that says a class implements this empty interface. Does that have any negative consequences? (If so, we could think of some compiler directive that would say to ignore traits with only ghost members.)

None that I can see. Empty "marker" interfaces are definitely already a thing (e.g. Java's RandomAccess interface). This may fall into the general bucket of hiding compiled components that aren't explicitly externed from target language code: #244 That is, I'll be even less worried if the compiled name is __DAFNY_INTERNAL__Validatable.

• I'm thinking there may be a better name than Validable. Given the ValidComponent member, should the trait perhaps have a name like Composite?

Agreed, although I think Composite is too narrow - that implies a validatable object has to either contain others or be contained by others, and there are examples in here like SeqReader that are completely self-contained.

It's also worth noting that as defined, these kind of have to be "mutably validatable" because it forces this in Repr, whereas some classes like CacheEntryEncrypt have a Valid() method that does not read the heap at all. I tried adding the reads clause to classes like that and it became a rathole to keep everything validating so I avoided it. I also experimented with supporting empty Repr sets but didn't get too far, and I'm not sure if that's worthwhile. Finally, if we add support for traits on datatypes, I'm not sure whether this trait would ever apply and if we care.

If this is codifying the dynamic-frames idiom, should we call it Framed? :)

[robin-aws]

If this is codifying the dynamic-frames idiom, should we call it Framed? :)

On second thought that conflicts pretty badly with message body frames. :)

[robin-aws]

Note that having this in a public Dafny standard library might help guide new users to use the idioms: dafny-lang/dafny#292

[robin-aws]

I've cut a standard library PR for this instead now, so it makes more sense to use that version if it gets in: dafny-lang/libraries#22