Add Validatable trait by robin-aws · Pull Request #329 · aws/aws-encryption-sdk

robin-aws · 2020-05-22T23:32:55Z

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.

… into validatable

CachingCMM.dfy needs a bit more work

… into validatable

Horray for generic traits and traits on traits!

lavaleri · 2020-05-22T23:38:05Z

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 · 2020-05-22T23:39:14Z

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 · 2020-05-22T23:49:28Z

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 · 2020-05-23T01:28:33Z

src/StandardLibrary/StandardLibrary.dfy

+    // TODO-RS: Better name?
+    twostate predicate ValidAndFresh() 
+      reads this, Repr
+      ensures ValidAndFresh() ==> Valid() && fresh(Repr - old(Repr))


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()).

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 · 2020-05-27T00:10:08Z

src/StandardLibrary/StandardLibrary.dfy

+    // TODO-RS: The style guide actually implies this should be "repr",
+    // but the convention is well-established at this point.


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".

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

RustanLeino · 2020-05-27T00:10:57Z

src/StandardLibrary/StandardLibrary.dfy

+
+    // Convenience predicate for when your object's validity depends on one
+    // or more other objects.
+    predicate ValidComponent(component: Validatable)


Having convenience predicates like this is fantastic!

RustanLeino · 2020-05-27T00:17:39Z

src/StandardLibrary/StandardLibrary.dfy

+      ensures ValidComponent(component) ==> (
+        && component in Repr
+        && component.Repr <= Repr
+        && this !in component.Repr
+        && component.Valid())


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).

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 · 2020-05-27T00:18:31Z

src/StandardLibrary/StandardLibrary.dfy

+    // TODO-RS: Better name?
+    twostate predicate ValidAndFresh() 
+      reads this, Repr
+      ensures ValidAndFresh() ==> Valid() && fresh(Repr - old(Repr))


Ditto. This postcondition is not necessary.

robin-aws · 2020-05-27T16:42:07Z

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 · 2020-05-27T20:19:13Z

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 · 2020-08-05T21:00:56Z

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 · 2021-10-05T22:19:52Z

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

robin-aws added 8 commits May 13, 2020 11:22

Add Validatable trait

2a827ac

Merge branch 'develop' of github.com:awslabs/aws-encryption-sdk-dafny…

4069d96

… into validatable

Added Validatable wherever possible

c1e56a8

CachingCMM.dfy needs a bit more work

Merge branch 'develop' of github.com:awslabs/aws-encryption-sdk-dafny…

7adca18

… into validatable

Revert adding Validatable to CacheEntryEncrypt/Decrypt

bd48a1f

Add Validatable to lots more classes

e1f4fe9

Horray for generic traits and traits on traits!

Update Dafny commit pointer

26d30ec

Remove stale TODOs

d476453

Empty commit to kick build

20e91cd

robin-aws linked an issue May 23, 2020 that may be closed by this pull request

Define a common Validatable trait #319

Closed

alex-chew reviewed May 23, 2020

View reviewed changes

alex-chew approved these changes May 26, 2020

View reviewed changes

RustanLeino suggested changes May 27, 2020

View reviewed changes

farleyb-amazon closed this May 6, 2022

		// TODO-RS: The style guide actually implies this should be "repr",
		// but the convention is well-established at this point.

Comments

Conversation

robin-aws commented May 22, 2020

Uh oh!

lavaleri commented May 22, 2020

AWS CodeBuild CI Report

Uh oh!

lavaleri commented May 22, 2020

AWS CodeBuild CI Report

Uh oh!

lavaleri commented May 22, 2020

AWS CodeBuild CI Report

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

RustanLeino left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

robin-aws commented May 27, 2020

Uh oh!

robin-aws commented May 27, 2020

Uh oh!

robin-aws commented Aug 5, 2020

Uh oh!

robin-aws commented Oct 5, 2021

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants