Skip to content

test: initial commit of ESDK TestVectors - #678

Merged
josecorella merged 127 commits into
mainlinefrom
jocorell/dafny-test-vectors
Nov 13, 2024
Merged

test: initial commit of ESDK TestVectors#678
josecorella merged 127 commits into
mainlinefrom
jocorell/dafny-test-vectors

Conversation

@josecorella

Copy link
Copy Markdown
Contributor

Issue #, if available:

Description of changes:

Squash/merge commit message, if applicable:

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

@josecorella
josecorella marked this pull request as ready for review November 4, 2024 22:32
@josecorella
josecorella requested a review from a team as a code owner November 4, 2024 22:32
Comment thread TestVectors/dafny/TestVectors/src/VectorsComposition/AllEsdkV4NoReqEc.dfy Outdated
Comment thread TestVectors/dafny/TestVectors/src/VectorsComposition/AllEsdkV4NoReqEc.dfy Outdated
Comment thread TestVectors/dafny/TestVectors/src/VectorsComposition/AllEsdkV4WithReqEc.dfy Outdated
Comment thread TestVectors/README.md Outdated
Comment thread TestVectors/dafny/TestVectors/src/EsdkTestVectors.dfy Outdated
Comment thread TestVectors/dafny/TestVectors/src/EsdkTestVectors.dfy Outdated

@seebees seebees left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think we should also order the test vectors.

I'm thinking something like:
description, algorithmSuiteId

Comment thread TestVectors/dafny/TestVectors/src/EsdkTestVectors.dfy
seebees
seebees previously approved these changes Nov 13, 2024

@seebees seebees left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM left one nit for later :)

Comment on lines +170 to +172
predicate DescriptionLessThan(x: EsdkTestVectors.EsdkEncryptTestVector, y: EsdkTestVectors.EsdkEncryptTestVector) {
Below(x.description, y.description)
}

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Likely too much work ATM, but we should come back and change this to:

Suggested change
predicate DescriptionLessThan(x: EsdkTestVectors.EsdkEncryptTestVector, y: EsdkTestVectors.EsdkEncryptTestVector) {
Below(x.description, y.description)
}
predicate DescriptionLessThan(x: EsdkTestVectors.EsdkEncryptTestVector, y: EsdkTestVectors.EsdkEncryptTestVector) {
&& Below(x.description, y.description)
&& Below(x.algorithmSuiteId, y.algorithmSuiteId)
}

I know that this might be complicated so I won't block on it.

@seebees seebees left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good.

@josecorella
josecorella merged commit fdd25ad into mainline Nov 13, 2024
@josecorella
josecorella deleted the jocorell/dafny-test-vectors branch November 13, 2024 18:57
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants