Skip to content

Commit

Permalink
[Spec] Add the initial specs for ed25519 and multi_ed25519
Browse files Browse the repository at this point in the history 
- modeled the native functions with uninterpreted functions
- added functional specifications
  • Loading branch information
@junkil-park
junkil-park committed Nov 22, 2022
1 parent 2ba008c commit 67f4796
Show file tree
Hide file tree
Showing 5 changed files with 25,815 additions and 8 deletions.
83 changes: 83 additions & 0 deletions aptos-move/framework/aptos-stdlib/doc/ed25519.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand Down Expand Up @@ -686,6 +689,82 @@ Returns <code><b>false</b></code> if either:
## Specification


<a name="@Specification_1_new_unvalidated_public_key_from_bytes"></a>

### Function `new_unvalidated_public_key_from_bytes`


<pre><code><b>public</b> <b>fun</b> <a href="ed25519.md#0x1_ed25519_new_unvalidated_public_key_from_bytes">new_unvalidated_public_key_from_bytes</a>(bytes: <a href="../../move-stdlib/doc/vector.md#0x1_vector">vector</a>&lt;u8&gt;): <a href="ed25519.md#0x1_ed25519_UnvalidatedPublicKey">ed25519::UnvalidatedPublicKey</a>
</code></pre>




<pre><code><b>let</b> length = len(bytes);
<b>aborts_if</b> length != <a href="ed25519.md#0x1_ed25519_PUBLIC_KEY_NUM_BYTES">PUBLIC_KEY_NUM_BYTES</a>;
<b>ensures</b> result == <a href="ed25519.md#0x1_ed25519_UnvalidatedPublicKey">UnvalidatedPublicKey</a> { bytes };
</code></pre>



<a name="@Specification_1_new_validated_public_key_from_bytes"></a>

### Function `new_validated_public_key_from_bytes`


<pre><code><b>public</b> <b>fun</b> <a href="ed25519.md#0x1_ed25519_new_validated_public_key_from_bytes">new_validated_public_key_from_bytes</a>(bytes: <a href="../../move-stdlib/doc/vector.md#0x1_vector">vector</a>&lt;u8&gt;): <a href="../../move-stdlib/doc/option.md#0x1_option_Option">option::Option</a>&lt;<a href="ed25519.md#0x1_ed25519_ValidatedPublicKey">ed25519::ValidatedPublicKey</a>&gt;
</code></pre>




<pre><code><b>aborts_if</b> <b>false</b>;
<b>let</b> cond = <a href="ed25519.md#0x1_ed25519_spec_public_key_validate_internal">spec_public_key_validate_internal</a>(bytes);
<b>ensures</b> cond ==&gt; result == <a href="../../move-stdlib/doc/option.md#0x1_option_spec_some">option::spec_some</a>(<a href="ed25519.md#0x1_ed25519_ValidatedPublicKey">ValidatedPublicKey</a>{bytes});
<b>ensures</b> !cond ==&gt; result == <a href="../../move-stdlib/doc/option.md#0x1_option_spec_none">option::spec_none</a>&lt;<a href="ed25519.md#0x1_ed25519_ValidatedPublicKey">ValidatedPublicKey</a>&gt;();
</code></pre>



<a name="@Specification_1_new_signature_from_bytes"></a>

### Function `new_signature_from_bytes`


<pre><code><b>public</b> <b>fun</b> <a href="ed25519.md#0x1_ed25519_new_signature_from_bytes">new_signature_from_bytes</a>(bytes: <a href="../../move-stdlib/doc/vector.md#0x1_vector">vector</a>&lt;u8&gt;): <a href="ed25519.md#0x1_ed25519_Signature">ed25519::Signature</a>
</code></pre>




<pre><code><b>aborts_if</b> len(bytes)!= <a href="ed25519.md#0x1_ed25519_SIGNATURE_NUM_BYTES">SIGNATURE_NUM_BYTES</a>;
<b>ensures</b> result == <a href="ed25519.md#0x1_ed25519_Signature">Signature</a> { bytes };
</code></pre>




<a name="0x1_ed25519_spec_public_key_validate_internal"></a>


<pre><code><b>fun</b> <a href="ed25519.md#0x1_ed25519_spec_public_key_validate_internal">spec_public_key_validate_internal</a>(bytes: <a href="../../move-stdlib/doc/vector.md#0x1_vector">vector</a>&lt;u8&gt;): bool;
</code></pre>




<a name="0x1_ed25519_spec_signature_verify_strict_internal"></a>


<pre><code><b>fun</b> <a href="ed25519.md#0x1_ed25519_spec_signature_verify_strict_internal">spec_signature_verify_strict_internal</a>(
signature: <a href="../../move-stdlib/doc/vector.md#0x1_vector">vector</a>&lt;u8&gt;,
public_key: <a href="../../move-stdlib/doc/vector.md#0x1_vector">vector</a>&lt;u8&gt;,
message: <a href="../../move-stdlib/doc/vector.md#0x1_vector">vector</a>&lt;u8&gt;
): bool;
</code></pre>



<a name="@Specification_1_public_key_validate_internal"></a>

### Function `public_key_validate_internal`
Expand All @@ -698,6 +777,8 @@ Returns <code><b>false</b></code> if either:


<pre><code><b>pragma</b> opaque;
<b>aborts_if</b> <b>false</b>;
<b>ensures</b> result == <a href="ed25519.md#0x1_ed25519_spec_public_key_validate_internal">spec_public_key_validate_internal</a>(bytes);
</code></pre>


Expand All @@ -714,6 +795,8 @@ Returns <code><b>false</b></code> if either:


<pre><code><b>pragma</b> opaque;
<b>aborts_if</b> <b>false</b>;
<b>ensures</b> result == <a href="ed25519.md#0x1_ed25519_spec_signature_verify_strict_internal">spec_signature_verify_strict_internal</a>(signature, public_key, message);
</code></pre>


Expand Down
85 changes: 85 additions & 0 deletions aptos-move/framework/aptos-stdlib/doc/multi_ed25519.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand Down Expand Up @@ -669,6 +672,84 @@ Returns <code><b>false</b></code> if either:
## Specification


<a name="@Specification_1_new_unvalidated_public_key_from_bytes"></a>

### Function `new_unvalidated_public_key_from_bytes`


<pre><code><b>public</b> <b>fun</b> <a href="multi_ed25519.md#0x1_multi_ed25519_new_unvalidated_public_key_from_bytes">new_unvalidated_public_key_from_bytes</a>(bytes: <a href="../../move-stdlib/doc/vector.md#0x1_vector">vector</a>&lt;u8&gt;): <a href="multi_ed25519.md#0x1_multi_ed25519_UnvalidatedPublicKey">multi_ed25519::UnvalidatedPublicKey</a>
</code></pre>




<pre><code><b>let</b> length = len(bytes);
<b>aborts_if</b> length / <a href="multi_ed25519.md#0x1_multi_ed25519_INDIVIDUAL_PUBLIC_KEY_NUM_BYTES">INDIVIDUAL_PUBLIC_KEY_NUM_BYTES</a> &gt; <a href="multi_ed25519.md#0x1_multi_ed25519_MAX_NUMBER_OF_PUBLIC_KEYS">MAX_NUMBER_OF_PUBLIC_KEYS</a>;
<b>aborts_if</b> length % <a href="multi_ed25519.md#0x1_multi_ed25519_INDIVIDUAL_PUBLIC_KEY_NUM_BYTES">INDIVIDUAL_PUBLIC_KEY_NUM_BYTES</a> != <a href="multi_ed25519.md#0x1_multi_ed25519_THRESHOLD_SIZE_BYTES">THRESHOLD_SIZE_BYTES</a>;
<b>ensures</b> result == <a href="multi_ed25519.md#0x1_multi_ed25519_UnvalidatedPublicKey">UnvalidatedPublicKey</a> { bytes };
</code></pre>



<a name="@Specification_1_new_validated_public_key_from_bytes"></a>

### Function `new_validated_public_key_from_bytes`


<pre><code><b>public</b> <b>fun</b> <a href="multi_ed25519.md#0x1_multi_ed25519_new_validated_public_key_from_bytes">new_validated_public_key_from_bytes</a>(bytes: <a href="../../move-stdlib/doc/vector.md#0x1_vector">vector</a>&lt;u8&gt;): <a href="../../move-stdlib/doc/option.md#0x1_option_Option">option::Option</a>&lt;<a href="multi_ed25519.md#0x1_multi_ed25519_ValidatedPublicKey">multi_ed25519::ValidatedPublicKey</a>&gt;
</code></pre>




<pre><code><b>aborts_if</b> <b>false</b>;
<b>let</b> cond = len(bytes) % <a href="multi_ed25519.md#0x1_multi_ed25519_INDIVIDUAL_PUBLIC_KEY_NUM_BYTES">INDIVIDUAL_PUBLIC_KEY_NUM_BYTES</a> == <a href="multi_ed25519.md#0x1_multi_ed25519_THRESHOLD_SIZE_BYTES">THRESHOLD_SIZE_BYTES</a>
&& <a href="multi_ed25519.md#0x1_multi_ed25519_spec_public_key_validate_internal">spec_public_key_validate_internal</a>(bytes);
<b>ensures</b> cond ==&gt; result == <a href="../../move-stdlib/doc/option.md#0x1_option_spec_some">option::spec_some</a>(<a href="multi_ed25519.md#0x1_multi_ed25519_ValidatedPublicKey">ValidatedPublicKey</a>{bytes});
<b>ensures</b> !cond ==&gt; result == <a href="../../move-stdlib/doc/option.md#0x1_option_spec_none">option::spec_none</a>&lt;<a href="multi_ed25519.md#0x1_multi_ed25519_ValidatedPublicKey">ValidatedPublicKey</a>&gt;();
</code></pre>



<a name="@Specification_1_new_signature_from_bytes"></a>

### Function `new_signature_from_bytes`


<pre><code><b>public</b> <b>fun</b> <a href="multi_ed25519.md#0x1_multi_ed25519_new_signature_from_bytes">new_signature_from_bytes</a>(bytes: <a href="../../move-stdlib/doc/vector.md#0x1_vector">vector</a>&lt;u8&gt;): <a href="multi_ed25519.md#0x1_multi_ed25519_Signature">multi_ed25519::Signature</a>
</code></pre>




<pre><code><b>aborts_if</b> len(bytes) % <a href="multi_ed25519.md#0x1_multi_ed25519_INDIVIDUAL_SIGNATURE_NUM_BYTES">INDIVIDUAL_SIGNATURE_NUM_BYTES</a> != <a href="multi_ed25519.md#0x1_multi_ed25519_BITMAP_NUM_OF_BYTES">BITMAP_NUM_OF_BYTES</a>;
<b>ensures</b> result == <a href="multi_ed25519.md#0x1_multi_ed25519_Signature">Signature</a> { bytes };
</code></pre>




<a name="0x1_multi_ed25519_spec_public_key_validate_internal"></a>


<pre><code><b>fun</b> <a href="multi_ed25519.md#0x1_multi_ed25519_spec_public_key_validate_internal">spec_public_key_validate_internal</a>(bytes: <a href="../../move-stdlib/doc/vector.md#0x1_vector">vector</a>&lt;u8&gt;): bool;
</code></pre>




<a name="0x1_multi_ed25519_spec_signature_verify_strict_internal"></a>


<pre><code><b>fun</b> <a href="multi_ed25519.md#0x1_multi_ed25519_spec_signature_verify_strict_internal">spec_signature_verify_strict_internal</a>(
multisignature: <a href="../../move-stdlib/doc/vector.md#0x1_vector">vector</a>&lt;u8&gt;,
public_key: <a href="../../move-stdlib/doc/vector.md#0x1_vector">vector</a>&lt;u8&gt;,
message: <a href="../../move-stdlib/doc/vector.md#0x1_vector">vector</a>&lt;u8&gt;
): bool;
</code></pre>



<a name="@Specification_1_public_key_validate_internal"></a>

### Function `public_key_validate_internal`
Expand All @@ -681,6 +762,8 @@ Returns <code><b>false</b></code> if either:


<pre><code><b>pragma</b> opaque;
<b>aborts_if</b> <b>false</b>;
<b>ensures</b> result == <a href="multi_ed25519.md#0x1_multi_ed25519_spec_public_key_validate_internal">spec_public_key_validate_internal</a>(bytes);
</code></pre>


Expand All @@ -697,6 +780,8 @@ Returns <code><b>false</b></code> if either:


<pre><code><b>pragma</b> opaque;
<b>aborts_if</b> <b>false</b>;
<b>ensures</b> result == <a href="multi_ed25519.md#0x1_multi_ed25519_spec_signature_verify_strict_internal">spec_signature_verify_strict_internal</a>(multisignature, public_key, message);
</code></pre>


Expand Down
Loading

0 comments on commit 67f4796

Please sign in to comment.