[Spec] Add the initial specs for ed25519 and multi_ed25519
#5677
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,11 +1,53 @@ | ||
| spec aptos_std::ed25519 { | ||
|
|
||
| // ----------------------- | ||
| // Function specifications | ||
| // ----------------------- | ||
|
|
||
| spec new_unvalidated_public_key_from_bytes(bytes: vector<u8>): UnvalidatedPublicKey { | ||
| let length = len(bytes); | ||
| aborts_if length != PUBLIC_KEY_NUM_BYTES; | ||
| ensures result == UnvalidatedPublicKey { bytes }; | ||
| } | ||
|
|
||
| spec new_validated_public_key_from_bytes(bytes: vector<u8>): Option<ValidatedPublicKey> { | ||
| aborts_if false; | ||
| let cond = spec_public_key_validate_internal(bytes); | ||
| ensures cond ==> result == option::spec_some(ValidatedPublicKey{bytes}); | ||
| ensures !cond ==> result == option::spec_none<ValidatedPublicKey>(); | ||
| } | ||
|
|
||
| spec new_signature_from_bytes(bytes: vector<u8>): Signature { | ||
| aborts_if len(bytes)!= SIGNATURE_NUM_BYTES; | ||
| ensures result == Signature { bytes }; | ||
| } | ||
|
|
||
|
|
||
| // ---------------- | ||
| // Native functions | ||
| // ---------------- | ||
|
|
||
| spec fun spec_public_key_validate_internal(bytes: vector<u8>): bool; | ||
|
|
||
| spec fun spec_signature_verify_strict_internal( | ||
| signature: vector<u8>, | ||
| public_key: vector<u8>, | ||
| message: vector<u8> | ||
| ): bool; | ||
|
|
||
| spec public_key_validate_internal(bytes: vector<u8>): bool { | ||
| pragma opaque; | ||
| aborts_if false; | ||
| ensures result == spec_public_key_validate_internal(bytes); | ||
| } | ||
|
|
||
| spec signature_verify_strict_internal( | ||
| signature: vector<u8>, | ||
| public_key: vector<u8>, | ||
| message: vector<u8>) | ||
| : bool { | ||
| pragma opaque; | ||
| aborts_if false; | ||
| ensures result == spec_signature_verify_strict_internal(signature, public_key, message); | ||
| } | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,11 +1,56 @@ | ||
| spec aptos_std::multi_ed25519 { | ||
|
|
||
| // ----------------------- | ||
| // Function specifications | ||
| // ----------------------- | ||
|
|
||
| spec new_unvalidated_public_key_from_bytes(bytes: vector<u8>): UnvalidatedPublicKey { | ||
| let length = len(bytes); | ||
| aborts_if length / INDIVIDUAL_PUBLIC_KEY_NUM_BYTES > MAX_NUMBER_OF_PUBLIC_KEYS; | ||
| aborts_if length % INDIVIDUAL_PUBLIC_KEY_NUM_BYTES != THRESHOLD_SIZE_BYTES; | ||
| ensures result == UnvalidatedPublicKey { bytes }; | ||
| } | ||
|
|
||
| spec new_validated_public_key_from_bytes(bytes: vector<u8>): Option<ValidatedPublicKey> { | ||
| aborts_if len(bytes) % INDIVIDUAL_PUBLIC_KEY_NUM_BYTES == THRESHOLD_SIZE_BYTES | ||
| && len(bytes) / INDIVIDUAL_PUBLIC_KEY_NUM_BYTES > MAX_NUMBER_OF_PUBLIC_KEYS; | ||
| let cond = len(bytes) % INDIVIDUAL_PUBLIC_KEY_NUM_BYTES == THRESHOLD_SIZE_BYTES | ||
| && spec_public_key_validate_internal(bytes); | ||
| ensures cond ==> result == option::spec_some(ValidatedPublicKey{bytes}); | ||
| ensures !cond ==> result == option::spec_none<ValidatedPublicKey>(); | ||
| } | ||
|
|
||
| spec new_signature_from_bytes(bytes: vector<u8>): Signature { | ||
| aborts_if len(bytes) % INDIVIDUAL_SIGNATURE_NUM_BYTES != BITMAP_NUM_OF_BYTES; | ||
| ensures result == Signature { bytes }; | ||
| } | ||
|
|
||
|
|
||
| // ---------------- | ||
| // Native functions | ||
| // ---------------- | ||
|
|
||
| spec fun spec_public_key_validate_internal(bytes: vector<u8>): bool; | ||
|
|
||
| spec fun spec_signature_verify_strict_internal( | ||
| multisignature: vector<u8>, | ||
| public_key: vector<u8>, | ||
| message: vector<u8> | ||
| ): bool; | ||
|
|
||
| spec public_key_validate_internal(bytes: vector<u8>): bool { | ||
| pragma opaque; | ||
| aborts_if len(bytes) / INDIVIDUAL_PUBLIC_KEY_NUM_BYTES > MAX_NUMBER_OF_PUBLIC_KEYS; | ||
|
There was a problem hiding this comment. Hey @junkil-park, I see this says that the native aborts upon this condition, but the native never aborts. There was a problem hiding this comment. I think my initial reply in the discussion above made it seem like the native aborts upon this condition, but it merely returns false. There was a problem hiding this comment. Thank you letting me know! I put up the fix here: https://github.com/aptos-labs/aptos-core/pull/5832/files#diff-ed6845718b5d03098f058edfc43ace50fc05ff3d18bf729521701a36b0c19bc3R45 |
||
| ensures result == spec_public_key_validate_internal(bytes); | ||
| } | ||
|
|
||
| spec signature_verify_strict_internal( | ||
| multisignature: vector<u8>, | ||
| public_key: vector<u8>, | ||
| message: vector<u8> | ||
| ): bool { | ||
| pragma opaque; | ||
| aborts_if false; | ||
| ensures result == spec_signature_verify_strict_internal(multisignature, public_key, message); | ||
| } | ||
| } | ||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
How come you don't do the
length / INDIVIDUAL_PUBLIC_KEY_NUM_BYTES > MAX_NUMBER_OF_PUBLIC_KEYScheck here too?There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@alinush ,
condis here to model the condition in this line: https://github.com/aptos-labs/aptos-core/blob/main/aptos-move/framework/aptos-stdlib/sources/cryptography/multi_ed25519.move#L123Does the Move function
new_validated_public_key_from_bytesactually need the additional check you're mentioning?There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I see: That check is done in the
public_key_validate_internalnative, whichnew_validated_public_key_from_bytescalls. I guess that's why I didn't replicate it.A bit confusing now reading my own code 🤦 ...
Would you mind adding a comment at line 123 (which you linked to) that says:
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks! Added the comment.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Hey @junkil-park, I was taking another look, and now I noticed that you added the
length / INDIVIDUAL_PUBLIC_KEY_NUM_BYTES > MAX_NUMBER_OF_PUBLIC_KEYScheck here too.But, as per my new comment below, this abort will never happen because the native called by
new_validated_public_key_from_byteswould only returns false, not abort.