From c68c4e673ca10b677bd96e84fd8479558db4277b Mon Sep 17 00:00:00 2001 From: Junkil Park Date: Mon, 21 Nov 2022 23:58:18 -0800 Subject: [PATCH] [Spec] Add the initial specs for `ed25519` and `multi_ed25519` - modeled the native functions with uninterpreted functions - added functional specifications --- .../framework/aptos-stdlib/doc/ed25519.md | 83 ++++++++++++++++++ .../aptos-stdlib/doc/multi_ed25519.md | 85 +++++++++++++++++++ .../sources/cryptography/ed25519.spec.move | 50 ++++++++++- .../cryptography/multi_ed25519.spec.move | 52 +++++++++++- 4 files changed, 262 insertions(+), 8 deletions(-) diff --git a/aptos-move/framework/aptos-stdlib/doc/ed25519.md b/aptos-move/framework/aptos-stdlib/doc/ed25519.md index 1ce8f946a7a0b..e217cf024f6b6 100644 --- a/aptos-move/framework/aptos-stdlib/doc/ed25519.md +++ b/aptos-move/framework/aptos-stdlib/doc/ed25519.md @@ -31,6 +31,9 @@ Contains functions for: - [Function `public_key_validate_internal`](#0x1_ed25519_public_key_validate_internal) - [Function `signature_verify_strict_internal`](#0x1_ed25519_signature_verify_strict_internal) - [Specification](#@Specification_1) + - [Function `new_unvalidated_public_key_from_bytes`](#@Specification_1_new_unvalidated_public_key_from_bytes) + - [Function `new_validated_public_key_from_bytes`](#@Specification_1_new_validated_public_key_from_bytes) + - [Function `new_signature_from_bytes`](#@Specification_1_new_signature_from_bytes) - [Function `public_key_validate_internal`](#@Specification_1_public_key_validate_internal) - [Function `signature_verify_strict_internal`](#@Specification_1_signature_verify_strict_internal) @@ -686,6 +689,82 @@ Returns false if either: ## Specification + + +### Function `new_unvalidated_public_key_from_bytes` + + +
public fun new_unvalidated_public_key_from_bytes(bytes: vector<u8>): ed25519::UnvalidatedPublicKey
+
+ + + + +
let length = len(bytes);
+aborts_if length != PUBLIC_KEY_NUM_BYTES;
+ensures result == UnvalidatedPublicKey { bytes };
+
+ + + + + +### Function `new_validated_public_key_from_bytes` + + +
public fun new_validated_public_key_from_bytes(bytes: vector<u8>): option::Option<ed25519::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>();
+
+ + + + + +### Function `new_signature_from_bytes` + + +
public fun new_signature_from_bytes(bytes: vector<u8>): ed25519::Signature
+
+ + + + +
aborts_if len(bytes)!= SIGNATURE_NUM_BYTES;
+ensures result == Signature { bytes };
+
+ + + + + + + +
fun spec_public_key_validate_internal(bytes: vector<u8>): bool;
+
+ + + + + + + +
fun spec_signature_verify_strict_internal(
+   signature: vector<u8>,
+   public_key: vector<u8>,
+   message: vector<u8>
+): bool;
+
+ + + ### Function `public_key_validate_internal` @@ -698,6 +777,8 @@ Returns false if either: 
pragma opaque;
+aborts_if false;
+ensures result == spec_public_key_validate_internal(bytes);
@@ -714,6 +795,8 @@ Returns false if either: 
pragma opaque;
+aborts_if false;
+ensures result == spec_signature_verify_strict_internal(signature, public_key, message);
diff --git a/aptos-move/framework/aptos-stdlib/doc/multi_ed25519.md b/aptos-move/framework/aptos-stdlib/doc/multi_ed25519.md index 221c19f428797..2d98e5ff726d2 100644 --- a/aptos-move/framework/aptos-stdlib/doc/multi_ed25519.md +++ b/aptos-move/framework/aptos-stdlib/doc/multi_ed25519.md @@ -28,6 +28,9 @@ This module has the exact same interface as the Ed25519 module. - [Function `public_key_validate_internal`](#0x1_multi_ed25519_public_key_validate_internal) - [Function `signature_verify_strict_internal`](#0x1_multi_ed25519_signature_verify_strict_internal) - [Specification](#@Specification_1) + - [Function `new_unvalidated_public_key_from_bytes`](#@Specification_1_new_unvalidated_public_key_from_bytes) + - [Function `new_validated_public_key_from_bytes`](#@Specification_1_new_validated_public_key_from_bytes) + - [Function `new_signature_from_bytes`](#@Specification_1_new_signature_from_bytes) - [Function `public_key_validate_internal`](#@Specification_1_public_key_validate_internal) - [Function `signature_verify_strict_internal`](#@Specification_1_signature_verify_strict_internal) @@ -669,6 +672,84 @@ Returns false if either: ## Specification + + +### Function `new_unvalidated_public_key_from_bytes` + + +
public fun new_unvalidated_public_key_from_bytes(bytes: vector<u8>): multi_ed25519::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 };
+
+ + + + + +### Function `new_validated_public_key_from_bytes` + + +
public fun new_validated_public_key_from_bytes(bytes: vector<u8>): option::Option<multi_ed25519::ValidatedPublicKey>
+
+ + + + +
aborts_if false;
+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>();
+
+ + + + + +### Function `new_signature_from_bytes` + + +
public fun new_signature_from_bytes(bytes: vector<u8>): multi_ed25519::Signature
+
+ + + + +
aborts_if len(bytes) % INDIVIDUAL_SIGNATURE_NUM_BYTES != BITMAP_NUM_OF_BYTES;
+ensures result == Signature { bytes };
+
+ + + + + + + +
fun spec_public_key_validate_internal(bytes: vector<u8>): bool;
+
+ + + + + + + +
fun spec_signature_verify_strict_internal(
+   multisignature: vector<u8>,
+   public_key: vector<u8>,
+   message: vector<u8>
+): bool;
+
+ + + ### Function `public_key_validate_internal` @@ -681,6 +762,8 @@ Returns false if either: 
pragma opaque;
+aborts_if false;
+ensures result == spec_public_key_validate_internal(bytes);
@@ -697,6 +780,8 @@ Returns false if either: 
pragma opaque;
+aborts_if false;
+ensures result == spec_signature_verify_strict_internal(multisignature, public_key, message);
diff --git a/aptos-move/framework/aptos-stdlib/sources/cryptography/ed25519.spec.move b/aptos-move/framework/aptos-stdlib/sources/cryptography/ed25519.spec.move index f8a891da319e3..8998aa3d0a39f 100644 --- a/aptos-move/framework/aptos-stdlib/sources/cryptography/ed25519.spec.move +++ b/aptos-move/framework/aptos-stdlib/sources/cryptography/ed25519.spec.move @@ -1,11 +1,53 @@ spec aptos_std::ed25519 { - spec public_key_validate_internal { - // TODO: temporary mockup. + + // ----------------------- + // Function specifications + // ----------------------- + + spec new_unvalidated_public_key_from_bytes(bytes: vector): 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): Option { + 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(); + } + + spec new_signature_from_bytes(bytes: vector): Signature { + aborts_if len(bytes)!= SIGNATURE_NUM_BYTES; + ensures result == Signature { bytes }; + } + + + // ---------------- + // Native functions + // ---------------- + + spec fun spec_public_key_validate_internal(bytes: vector): bool; + + spec fun spec_signature_verify_strict_internal( + signature: vector, + public_key: vector, + message: vector + ): bool; + + spec public_key_validate_internal(bytes: vector): bool { pragma opaque; + aborts_if false; + ensures result == spec_public_key_validate_internal(bytes); } - spec signature_verify_strict_internal { - // TODO: temporary mockup. + spec signature_verify_strict_internal( + signature: vector, + public_key: vector, + message: vector) + : bool { pragma opaque; + aborts_if false; + ensures result == spec_signature_verify_strict_internal(signature, public_key, message); } } diff --git a/aptos-move/framework/aptos-stdlib/sources/cryptography/multi_ed25519.spec.move b/aptos-move/framework/aptos-stdlib/sources/cryptography/multi_ed25519.spec.move index 48ea1963cae7b..69d11d35fb749 100644 --- a/aptos-move/framework/aptos-stdlib/sources/cryptography/multi_ed25519.spec.move +++ b/aptos-move/framework/aptos-stdlib/sources/cryptography/multi_ed25519.spec.move @@ -1,11 +1,55 @@ spec aptos_std::multi_ed25519 { - spec public_key_validate_internal { - // TODO: temporary mockup. + + // ----------------------- + // Function specifications + // ----------------------- + + spec new_unvalidated_public_key_from_bytes(bytes: vector): 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): Option { + aborts_if false; + 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(); + } + + spec new_signature_from_bytes(bytes: vector): 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): bool; + + spec fun spec_signature_verify_strict_internal( + multisignature: vector, + public_key: vector, + message: vector + ): bool; + + spec public_key_validate_internal(bytes: vector): bool { pragma opaque; + aborts_if false; + ensures result == spec_public_key_validate_internal(bytes); } - spec signature_verify_strict_internal { - // TODO: temporary mockup. + spec signature_verify_strict_internal( + multisignature: vector, + public_key: vector, + message: vector + ): bool { pragma opaque; + aborts_if false; + ensures result == spec_signature_verify_strict_internal(multisignature, public_key, message); } }