[Spec] Add the initial specs for `ed25519` and `multi_ed25519` #5677

junkil-park · 2022-11-22T07:59:10Z

Description

modeled the native functions with uninterpreted functions
added functional specifications
the axioms of the uninterpreted functions will be added when needed.

Test Plan

aptos move prove

movekevin · 2022-11-29T04:11:52Z

Can you remove output.bpl?

junkil-park · 2022-11-29T20:18:03Z

Can you remove output.bpl?

I just removed it. Good call!

alinush · 2022-11-29T23:04:30Z

aptos-move/framework/aptos-stdlib/sources/cryptography/multi_ed25519.spec.move

+
+    spec new_validated_public_key_from_bytes(bytes: vector<u8>): Option<ValidatedPublicKey> {
+        aborts_if false;
+        let cond = len(bytes) % INDIVIDUAL_PUBLIC_KEY_NUM_BYTES == THRESHOLD_SIZE_BYTES


How come you don't do the length / INDIVIDUAL_PUBLIC_KEY_NUM_BYTES > MAX_NUMBER_OF_PUBLIC_KEYS check here too?

@alinush , cond is 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#L123

Does the Move function new_validated_public_key_from_bytes actually need the additional check you're mentioning?

I see: That check is done in the public_key_validate_internal native, which new_validated_public_key_from_bytes calls. 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:

// Note that `public_key_validate_internal` will check that `vector::length(&bytes) / INDIVIDUAL_PUBLIC_KEY_NUM_BYTES <= MAX_NUMBER_OF_PUBLIC_KEYS`

Thanks! Added the comment.

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_KEYS check here too.

But, as per my new comment below, this abort will never happen because the native called by new_validated_public_key_from_bytes would only returns false, not abort.

- modeled the native functions with uninterpreted functions - added functional specifications

github-actions · 2022-12-05T10:02:42Z

✅ Forge suite `land_blocking` success on `594878f1b0f389b5cc981953149259fe212cf804`

performance benchmark with full nodes : 6630 TPS, 5971 ms latency, 9600 ms p99 latency,(!) expired 440 out of 2831720 txns
Test Ok

Grafana dashboard
Humio Logs
Test runner output
Test run is land-blocking

github-actions · 2022-12-05T10:05:06Z

✅ Forge suite `compat` success on `testnet_2d8b1b57553d869190f61df1aaf7f31a8fc19a7b` ==> `594878f1b0f389b5cc981953149259fe212cf804`

Compatibility test results for testnet_2d8b1b57553d869190f61df1aaf7f31a8fc19a7b ==> 594878f1b0f389b5cc981953149259fe212cf804 (PR)
1. Check liveness of validators at old version: testnet_2d8b1b57553d869190f61df1aaf7f31a8fc19a7b
compatibility::simple-validator-upgrade::liveness-check : 7628 TPS, 5203 ms latency, 7000 ms p99 latency,no expired txns
2. Upgrading first Validator to new version: 594878f1b0f389b5cc981953149259fe212cf804
compatibility::simple-validator-upgrade::single-validator-upgrade : 4789 TPS, 8217 ms latency, 11400 ms p99 latency,no expired txns
3. Upgrading rest of first batch to new version: 594878f1b0f389b5cc981953149259fe212cf804
compatibility::simple-validator-upgrade::half-validator-upgrade : 5102 TPS, 7977 ms latency, 10300 ms p99 latency,no expired txns
4. upgrading second batch to new version: 594878f1b0f389b5cc981953149259fe212cf804
compatibility::simple-validator-upgrade::rest-validator-upgrade : 6744 TPS, 5789 ms latency, 9500 ms p99 latency,no expired txns
5. check swarm health
Compatibility test for testnet_2d8b1b57553d869190f61df1aaf7f31a8fc19a7b ==> 594878f1b0f389b5cc981953149259fe212cf804 passed
Test Ok

Grafana dashboard
Humio Logs
Test runner output
Test run is land-blocking

alinush · 2022-12-08T03:34:28Z

aptos-move/framework/aptos-stdlib/sources/cryptography/multi_ed25519.spec.move

        pragma opaque;
+        aborts_if len(bytes) / INDIVIDUAL_PUBLIC_KEY_NUM_BYTES > MAX_NUMBER_OF_PUBLIC_KEYS;


Hey @junkil-park, I see this says that the native aborts upon this condition, but the native never aborts.
See

aptos-core/aptos-move/framework/src/natives/cryptography/multi_ed25519.rs

Line 31 in 8218008

fn native_public_key_validate(

I think my initial reply in the discussion above made it seem like the native aborts upon this condition, but it merely returns false.

Thank you letting me know! I put up the fix here: https://github.com/aptos-labs/aptos-core/pull/5832/files#diff-ed6845718b5d03098f058edfc43ace50fc05ff3d18bf729521701a36b0c19bc3R45

…-labs#5677) - modeled the native functions with uninterpreted functions - added functional specifications

junkil-park requested review from davidiw, movekevin and wrwg as code owners November 22, 2022 07:59

junkil-park requested review from meng-xu-cs and rahxephon89 November 22, 2022 07:59

junkil-park force-pushed the jpark/spec-ed25519 branch from 67f4796 to c68c4e6 Compare November 29, 2022 20:17

movekevin requested a review from alinush November 29, 2022 22:05

movekevin approved these changes Nov 29, 2022

View reviewed changes

alinush reviewed Nov 29, 2022

View reviewed changes

alinush approved these changes Nov 30, 2022

View reviewed changes

[Spec] Add the initial specs for ed25519 and multi_ed25519

594878f

- modeled the native functions with uninterpreted functions - added functional specifications

junkil-park force-pushed the jpark/spec-ed25519 branch from c68c4e6 to 594878f Compare December 5, 2022 09:17

junkil-park requested a review from areshand as a code owner December 5, 2022 09:17

junkil-park enabled auto-merge (squash) December 5, 2022 09:18

This comment has been minimized.

Sign in to view

junkil-park merged commit 621f2c9 into main Dec 5, 2022

junkil-park deleted the jpark/spec-ed25519 branch December 5, 2022 10:05

Markuze mentioned this pull request Dec 5, 2022

perf tools #5772

Closed

alinush reviewed Dec 8, 2022

View reviewed changes

areshand pushed a commit to areshand/aptos-core-1 that referenced this pull request Dec 18, 2022

[Spec] Add the initial specs for ed25519 and multi_ed25519 (aptos…

c07a789

…-labs#5677) - modeled the native functions with uninterpreted functions - added functional specifications

Markuze mentioned this pull request Dec 26, 2022

markuze/aptos perf #5998

Closed

Markuze mentioned this pull request Jan 3, 2023

[Network] Adding AptosPerf Client #6054

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Spec] Add the initial specs for `ed25519` and `multi_ed25519` #5677

[Spec] Add the initial specs for `ed25519` and `multi_ed25519` #5677

junkil-park commented Nov 22, 2022 •

edited

Loading

movekevin commented Nov 29, 2022

junkil-park commented Nov 29, 2022

alinush Nov 29, 2022

junkil-park Nov 30, 2022

alinush Nov 30, 2022 •

edited

Loading

junkil-park Dec 5, 2022

alinush Dec 8, 2022 •

edited

Loading

This comment has been minimized.

This comment has been minimized.

github-actions bot commented Dec 5, 2022

github-actions bot commented Dec 5, 2022

alinush Dec 8, 2022

alinush Dec 8, 2022 •

edited

Loading

junkil-park Dec 14, 2022

		pragma opaque;
		aborts_if len(bytes) / INDIVIDUAL_PUBLIC_KEY_NUM_BYTES > MAX_NUMBER_OF_PUBLIC_KEYS;

[Spec] Add the initial specs for ed25519 and multi_ed25519 #5677

[Spec] Add the initial specs for ed25519 and multi_ed25519 #5677

Conversation

junkil-park commented Nov 22, 2022 • edited Loading

Description

Test Plan

movekevin commented Nov 29, 2022

junkil-park commented Nov 29, 2022

alinush Nov 29, 2022

Choose a reason for hiding this comment

junkil-park Nov 30, 2022

Choose a reason for hiding this comment

alinush Nov 30, 2022 • edited Loading

Choose a reason for hiding this comment

junkil-park Dec 5, 2022

Choose a reason for hiding this comment

alinush Dec 8, 2022 • edited Loading

Choose a reason for hiding this comment

This comment has been minimized.

This comment has been minimized.

github-actions bot commented Dec 5, 2022

✅ Forge suite land_blocking success on 594878f1b0f389b5cc981953149259fe212cf804

github-actions bot commented Dec 5, 2022

✅ Forge suite compat success on testnet_2d8b1b57553d869190f61df1aaf7f31a8fc19a7b ==> 594878f1b0f389b5cc981953149259fe212cf804

alinush Dec 8, 2022

Choose a reason for hiding this comment

alinush Dec 8, 2022 • edited Loading

Choose a reason for hiding this comment

junkil-park Dec 14, 2022

Choose a reason for hiding this comment

[Spec] Add the initial specs for `ed25519` and `multi_ed25519` #5677

[Spec] Add the initial specs for `ed25519` and `multi_ed25519` #5677

junkil-park commented Nov 22, 2022 •

edited

Loading

alinush Nov 30, 2022 •

edited

Loading

alinush Dec 8, 2022 •

edited

Loading

✅ Forge suite `land_blocking` success on `594878f1b0f389b5cc981953149259fe212cf804`

✅ Forge suite `compat` success on `testnet_2d8b1b57553d869190f61df1aaf7f31a8fc19a7b` ==> `594878f1b0f389b5cc981953149259fe212cf804`

alinush Dec 8, 2022 •

edited

Loading