From 00c5c579528e6774b797631537cf0065d1504685 Mon Sep 17 00:00:00 2001 From: Jayfromthe13th Date: Sun, 17 Nov 2024 13:28:42 -0600 Subject: [PATCH 01/12] feat: add comprehensive vouch specifications - Added global invariants for vector alignment - Added specs for true_friends, revoke, all_not_expired - Added VouchInvariant schema - Added specs for bulk_set and get_vouch_price --- framework/libra-framework/sources/ol_sources/vouch.spec.move | 1 + 1 file changed, 1 insertion(+) create mode 100644 framework/libra-framework/sources/ol_sources/vouch.spec.move diff --git a/framework/libra-framework/sources/ol_sources/vouch.spec.move b/framework/libra-framework/sources/ol_sources/vouch.spec.move new file mode 100644 index 000000000..0519ecba6 --- /dev/null +++ b/framework/libra-framework/sources/ol_sources/vouch.spec.move @@ -0,0 +1 @@ + \ No newline at end of file From 88f2829e71b290e51880718c228b46800f8a899b Mon Sep 17 00:00:00 2001 From: Jayfromthe13th Date: Sun, 17 Nov 2024 14:10:22 -0600 Subject: [PATCH 02/12] feat: add vouch specifications --- .../sources/ol_sources/vouch.spec.move | Bin 1 -> 1022 bytes 1 file changed, 0 insertions(+), 0 deletions(-) diff --git a/framework/libra-framework/sources/ol_sources/vouch.spec.move b/framework/libra-framework/sources/ol_sources/vouch.spec.move index 0519ecba6ea913e21689ec692e81e9e4973fbf73..75607e11825ba929235bc61041f8f703c5d085ff 100644 GIT binary patch literal 1022 zcmcJO%}#?r6ot>)#CKq6H$FhMZrr+Z(Jev#BtqLTfHtPDu6}orf)Q(67&61m<=!*r zo-@3^Iqj4xR-mm)h00VbQbp{UNUbL=c{WsO6S~)TUB`SDVKi0?87ux7* zruNjiB~=feQOM~%hVi*O#&1s`J2fz~d`EuH`6*a)9Dd{Pv@fm00VySB{kvJr zQ+=hVzV&*BXquwDxzKYP)g8U5$WCyeB;^5DlXb6a zzzsBQOy_{{0){bgy4F4Wm{Isn6RpAQ@2Az?=;DaG!2R#M27adJhU^?JTlzLue?z~7 n!^Ypu%CB;C8vhn!vw;1|d+@(Jrgv(}Ac4Wu^#ghwbk6(%d6%h{ literal 1 IcmY!Y001EXApigX From 7dc11a19eb6a56c7c816ac3ac9b6a4c6845bc1f2 Mon Sep 17 00:00:00 2001 From: Jayfromthe13th Date: Mon, 30 Dec 2024 13:56:29 -0600 Subject: [PATCH 03/12] Update burn and vouch specifications with detailed comments and overflow checks --- .../sources/ol_sources/burn.spec.move | 53 ++++++++++++++++++ .../sources/ol_sources/vouch.spec.move | Bin 1022 -> 3909 bytes 2 files changed, 53 insertions(+) create mode 100644 framework/libra-framework/sources/ol_sources/burn.spec.move diff --git a/framework/libra-framework/sources/ol_sources/burn.spec.move b/framework/libra-framework/sources/ol_sources/burn.spec.move new file mode 100644 index 000000000..bbecd3b3b --- /dev/null +++ b/framework/libra-framework/sources/ol_sources/burn.spec.move @@ -0,0 +1,53 @@ +spec ol_framework::burn { + spec module { + pragma verify = true; // Enables verification of the module + pragma aborts_if_is_strict = true; // Ensures strict checking of aborts_if conditions + invariant [suspendable] exists(@ol_framework); // Ensures a BurnCounter always exists + } + + spec initialize { + pragma aborts_if_is_partial = true; // Allows partial aborts + let addr = signer::address_of(vm); + requires system_addresses::is_ol_framework_address(addr); // Checks if the address is a system address + ensures global(@ol_framework).lifetime_recycled == 0; // Ensures lifetime_recycled is initialized to 0 + } + + spec burn_and_track(coin: Coin) { + requires exists(@ol_framework); // Requires a BurnCounter to exist + aborts_if !exists(@ol_framework); // Aborts if no BurnCounter exists + ensures global(@ol_framework).lifetime_burned == + old(global(@ol_framework).lifetime_burned) + coin::value(coin); // Ensures lifetime_burned is incremented by the coin value + pragma aborts_if_is_partial = true; // Allows partial aborts + } + + spec set_send_community(sender: &signer, community: bool) { + let addr = signer::address_of(sender); + + // No aborts_if conditions needed since function handles both cases + aborts_if false; // Never aborts + + // Postconditions + ensures exists(addr); // Ensures UserBurnPreference exists for the address + ensures global(addr).send_community == community; // Ensures send_community is set correctly + requires exists(signer::address_of(sender)); // Ensures UserBurnPreference can be set for the address + } + + spec epoch_burn_fees { + pragma aborts_if_is_partial = true; // Allows partial aborts + ensures global(@ol_framework).lifetime_burned >= old(global(@ol_framework).lifetime_burned); // Ensures lifetime_burned does not decrease + requires global(@ol_framework).lifetime_burned < MAX_U64; // Requires lifetime_burned to be less than MAX_U64 + } + + spec vm_migration { + pragma aborts_if_is_partial = true; // Allows partial aborts + } + + spec vm_burn_with_user_preference { + pragma aborts_if_is_partial = true; // Allows partial aborts + } + + spec BurnCounter { + invariant lifetime_burned <= MAX_U64; // Ensures lifetime_burned does not exceed MAX_U64 + invariant lifetime_recycled <= MAX_U64; // Ensures lifetime_recycled does not exceed MAX_U64 + } +} diff --git a/framework/libra-framework/sources/ol_sources/vouch.spec.move b/framework/libra-framework/sources/ol_sources/vouch.spec.move index 75607e11825ba929235bc61041f8f703c5d085ff..90e330e6af8af7b7b841553a098a78c6e784e13e 100644 GIT binary patch literal 3909 zcmd^C--{bJ5PlEjf0#b?49?}AowMOuQYe%>w9uCj7VT=*tDL-YC9UsFx&OU0`eE(u ztsMes3Dj`lvqqztPcz?qa(isR=&H41hY!ZyuT}>$G#&i?`W4W}@%qllL1X@jf8JZM z-3d6LRqYYh;O&6#;O$#@--}wKiz})TUYQqJSE2>}}e$nMp>}#(Gz& zwo%~ zej2o2z-A3M3C(E7=*2})ju1Eqtz_C=yq0ei!LI>xiy-K)HxOgl`o`?2RI7yX%mt>E za2fIPDC>~InS2XKz3JZspq4-&gp9{Xl(=)MXYOGGH+*Tup7Xp2%d-;98H62tXEPB- z-b(?G>l3*-xo5s>k01}Ew3g$_mzCHnC&!a zh!;I^TLS1g-h9WGJB`@737r-gEP=N5xjrITc2W?{RQamnOE!grC_y z;{LK!Cif9{&+zi)!CL(OKZekkYpNdfJvj8989dYy-ArSw9P2PPs>tYy816)2OQ;7a zkCi4-@j{I){$)A#%QxqEl2;R91k#}EfAo>1m)yG@qttYw-(tdt5zcgWR$viqQD2=@ z^#_yO@Zik^n)u<2fS5)XXU8&~4s{TyX$-2l@XigJQ*`Ntz$x)ZqldjAJ+_8(^v7G@ zm8Rld)L6d-@ynxODx^;Oj$Raw27{odga!O-AYty!sGy$voHRcNHKWmp$0vrRKo{{T zlSF!?OuFB|$N1PF5os_6uI6(16D3#vqtxCfozFBAgel8+dQH)52W7ELzqrf51tr`| zekak>fza@$Qech$-0gTY+(}7lt3yq%kRo>oz@50KxW=z9j*fiMM3(%Hiy?+FK{APg zuiQ{mXIG}J3R+=gR0QUWzP{Y_E2xdp)#CKq6H$FhMZrr+Z(Jev#BtqLTfHtPDu6}orf)Q(67&61m<=!*r zo-@3^Iqj4xR-mm)h00VbQbp{UNUbL=c{WsO6S~)TUB`SDVKi0?87ux7* zruNjiB~=feQOM~%hVi*O#&1s`J2fz~d`EuH`6*a)9Dd{Pv@fm00VySB{kvJr zQ+=hVzV&*BXquwDxzKYP)g8U5$WCyeB;^5DlXb6a zzzsBQOy_{{0){bgy4F4Wm{Isn6RpAQ@2Az?=;DaG!2R#M27adJhU^?JTlzLue?z~7 n!^Ypu%CB;C8vhn!vw;1|d+@(Jrgv(}Ac4Wu^#ghwbk6(%d6%h{ From ff1cff0299ae59658b60e84400eb983840d18eec Mon Sep 17 00:00:00 2001 From: Jayfromthe13th Date: Thu, 2 Jan 2025 17:21:25 -0600 Subject: [PATCH 04/12] Trigger workflow rerun --- .../backup_specs/burn.spec.move | 15 +++ .../backup_specs/demo.spec.move | 23 ++++ .../backup_specs/libra_coin.spec.move | 43 ++++++++ .../backup_specs/ol_account.spec.move | 101 ++++++++++++++++++ .../backup_specs/sacred_cows.spec.move | 46 ++++++++ .../backup_specs/slow_wallet.spec.move | 25 +++++ .../backup_specs/vouch.spec.move | Bin 0 -> 1020 bytes 7 files changed, 253 insertions(+) create mode 100644 framework/libra-framework/backup_specs/burn.spec.move create mode 100644 framework/libra-framework/backup_specs/demo.spec.move create mode 100644 framework/libra-framework/backup_specs/libra_coin.spec.move create mode 100644 framework/libra-framework/backup_specs/ol_account.spec.move create mode 100644 framework/libra-framework/backup_specs/sacred_cows.spec.move create mode 100644 framework/libra-framework/backup_specs/slow_wallet.spec.move create mode 100644 framework/libra-framework/backup_specs/vouch.spec.move diff --git a/framework/libra-framework/backup_specs/burn.spec.move b/framework/libra-framework/backup_specs/burn.spec.move new file mode 100644 index 000000000..a96f5af17 --- /dev/null +++ b/framework/libra-framework/backup_specs/burn.spec.move @@ -0,0 +1,15 @@ +spec ol_framework::burn { + use std::signer; + use diem_framework::system_addresses; + use ol_framework::libra_coin::LibraCoin; + use ol_framework::coin; + + spec module { + pragma verify = true; + pragma aborts_if_is_strict = false; + } + + spec initialize(vm: &signer) { + aborts_if !system_addresses::is_ol_framework_address(signer::address_of(vm)); + } +} diff --git a/framework/libra-framework/backup_specs/demo.spec.move b/framework/libra-framework/backup_specs/demo.spec.move new file mode 100644 index 000000000..4d426607c --- /dev/null +++ b/framework/libra-framework/backup_specs/demo.spec.move @@ -0,0 +1,23 @@ +spec ol_framework::demo { + spec module { + pragma verify = true; + } + + spec print_this(account: &signer) { + // should not abort + pragma aborts_if_is_strict; + } + + // TODO in strict mode + spec set_message(account: &signer, message: string::String) { + // pragma aborts_if_is_strict; + // let events = borrow_global(signer::address_of(account)).message_change_events; + // aborts_if event::counter(events) > MAX_U64; + } + + spec get_message(addr: address): string::String { + pragma aborts_if_is_strict; + aborts_if !exists(addr); + + } +} diff --git a/framework/libra-framework/backup_specs/libra_coin.spec.move b/framework/libra-framework/backup_specs/libra_coin.spec.move new file mode 100644 index 000000000..06a6cfdf1 --- /dev/null +++ b/framework/libra-framework/backup_specs/libra_coin.spec.move @@ -0,0 +1,43 @@ +spec ol_framework::libra_coin { + spec module { + pragma verify = true; + pragma aborts_if_is_strict; + } + + spec initialize { + pragma aborts_if_is_partial; + let addr = signer::address_of(diem_framework); + ensures exists(addr); + ensures exists>(addr); + } + + spec destroy_mint_cap { + let addr = signer::address_of(diem_framework); + aborts_if addr != @diem_framework; + aborts_if !exists(@diem_framework); + } + + // Test function,not needed verify. + spec configure_accounts_for_test { + pragma verify = false; + } + + // // Only callable in tests and testnets.not needed verify. + // spec mint { + // pragma verify = false; + // } + + // Only callable in tests and testnets.not needed verify. + spec delegate_mint_capability { + pragma verify = false; + } + + // Only callable in tests and testnets.not needed verify. + spec claim_mint_capability(account: &signer) { + pragma verify = false; + } + + spec find_delegation(addr: address): Option { + aborts_if !exists(@core_resources); + } +} diff --git a/framework/libra-framework/backup_specs/ol_account.spec.move b/framework/libra-framework/backup_specs/ol_account.spec.move new file mode 100644 index 000000000..5c8495c69 --- /dev/null +++ b/framework/libra-framework/backup_specs/ol_account.spec.move @@ -0,0 +1,101 @@ +spec ol_framework::ol_account { + spec module { + pragma verify = true; + // pragma aborts_if_is_strict; + invariant [suspendable] chain_status::is_operating() ==> exists(@diem_framework); + invariant [suspendable] chain_status::is_operating() ==> exists>(@diem_framework); + + } + + // /// Check if the bytes of the auth_key is 32. + // /// The Account does not exist under the auth_key before creating the account. + // /// Limit the address of auth_key is not @vm_reserved / @diem_framework / @diem_toke. + // spec create_account(auth_key: address) { + // include CreateAccountAbortsIf; + // ensures exists(auth_key); + // ensures exists>(auth_key); + // } + spec schema CreateAccountAbortsIf { + auth_key: address; + aborts_if exists(auth_key); + aborts_if length_judgment(auth_key); + aborts_if auth_key == @vm_reserved || auth_key == @diem_framework || auth_key == @diem_token; + } + + spec fun length_judgment(auth_key: address): bool { + use std::bcs; + + let authentication_key = bcs::to_bytes(auth_key); + len(authentication_key) != 32 + } + + // ol_account::withdraw can never use more than the slow wallet limit + spec withdraw(sender: &signer, amount: u64): Coin{ + include AssumeCoinRegistered; + + let account_addr = signer::address_of(sender); + aborts_if amount == 0; + + let coin_store = global>(account_addr); + let balance = coin_store.coin.value; + + aborts_if balance < amount; + + // in the case of slow wallets + let slow_store = global(account_addr); + aborts_if exists(account_addr) && + slow_store.unlocked < amount; + + ensures result == Coin{value: amount}; + } + + spec schema AssumeCoinRegistered { + sender: &signer; + let account_addr = signer::address_of(sender); + aborts_if !coin::is_account_registered(account_addr); + } + + spec assert_account_exists(addr: address) { + aborts_if !account::exists_at(addr); + } + + /// Check if the address existed. + /// Check if the LibraCoin under the address existed. + spec assert_account_is_registered_for_gas(addr: address) { + aborts_if !account::exists_at(addr); + aborts_if !coin::is_account_registered(addr); + } + + spec set_allow_direct_coin_transfers(account: &signer, allow: bool) { + let addr = signer::address_of(account); + include !exists(addr) ==> account::NewEventHandleAbortsIf; + } + + // spec batch_transfer(source: &signer, recipients: vector
, amounts: vector) { + // // TODO: missing aborts_if spec + // pragma verify=false; + // } + + spec can_receive_direct_coin_transfers(account: address): bool { + aborts_if false; + ensures result == ( + !exists(account) || + global(account).allow_arbitrary_coin_transfers + ); + } + + // spec batch_transfer_coins(from: &signer, recipients: vector
, amounts: vector) { + // // TODO: missing aborts_if spec + // pragma verify=false; + // } + + // spec deposit_coins(to: address, coins: Coin) { + // // TODO: missing aborts_if spec + // pragma verify=false; + // } + + // spec transfer_coins(from: &signer, to: address, amount: u64) { + // // TODO: missing aborts_if spec + // pragma verify=false; + // } +} diff --git a/framework/libra-framework/backup_specs/sacred_cows.spec.move b/framework/libra-framework/backup_specs/sacred_cows.spec.move new file mode 100644 index 000000000..b05229721 --- /dev/null +++ b/framework/libra-framework/backup_specs/sacred_cows.spec.move @@ -0,0 +1,46 @@ +spec ol_framework::sacred_cows { + spec module { + use diem_framework::chain_status; + pragma verify = true; + pragma aborts_if_is_strict; + + invariant [suspendable] chain_status::is_operating() ==> + exists>(@0x2); + + invariant [suspendable] chain_status::is_operating() ==> + borrow_global>(@0x2).value == 30000 * 1000000; + } + + // only 0x2 can init + spec init(zero_x_two_sig: &signer) { + use std::signer; + aborts_if signer::address_of(zero_x_two_sig) != @0x2; + aborts_if exists>(@0x2); + + } + + // only 0x2 can init + spec get_stored(): u64 { + + } + + // only 0x2 can init + spec assert_same(stored: u64, code: u64) { + aborts_if stored != code; + } + + // only 0x2 can init + spec bless_this_cow(zero_x_two_sig: &signer, value: u64) { + use std::signer; + use diem_framework::chain_status; + aborts_if signer::address_of(zero_x_two_sig) != @0x2; + aborts_if exists>(@0x2); + aborts_if !chain_status::is_genesis(); + } + + + spec get_slow_drip_const(): u64 { + aborts_if !exists>(@0x2); + aborts_if borrow_global>(@0x2).value != SLOW_WALLET_EPOCH_DRIP; + } +} diff --git a/framework/libra-framework/backup_specs/slow_wallet.spec.move b/framework/libra-framework/backup_specs/slow_wallet.spec.move new file mode 100644 index 000000000..c663b7bee --- /dev/null +++ b/framework/libra-framework/backup_specs/slow_wallet.spec.move @@ -0,0 +1,25 @@ +spec ol_framework::slow_wallet { + spec module { + pragma verify = true; + // pragma aborts_if_is_strict; + } + + // setting a slow wallet should abort only if there is no SlowWalletList + // present in the 0x1 address + spec set_slow(sig: &signer) { + aborts_if !exists(@ol_framework); + } + + // at epoch boundaries the slow wallet drip should never abort + // if genesis is initialized properly + spec on_new_epoch(vm: &signer): (bool, u64) { + use ol_framework::sacred_cows::{SacredCow, SlowDrip}; + + aborts_if !system_addresses::signer_is_ol_root(vm); + + aborts_if !exists>(@0x2); + + aborts_if borrow_global>(@0x2).value != 35000 * 1000000; + + } +} diff --git a/framework/libra-framework/backup_specs/vouch.spec.move b/framework/libra-framework/backup_specs/vouch.spec.move new file mode 100644 index 0000000000000000000000000000000000000000..673fd6a37281f96c9ff49ba1c110d1f7a0f85f53 GIT binary patch literal 1020 zcmcJOy-veG5QL}ZDO{3<2S^AFEfoc=W&DSQokTu65FuV2`1TIRMwlQ9WSzaY*`1r6 zxxBwQ?UXB3q^)YjD%2`bL+*)8t4A$)_QX9^57fQrjCXi?IVvM%s`xfP_NVk$+GsV? zd+OYpu6xfY=JbGJd~S~U>l4UM9n7rWQD1U?4%Qrp-}pNn!00|_OhC;*%E{UMZWi;@ zTsf+5y`C|e<|uD21a70cqc;uJ84lD`eRW`PV&_#V@gSjM@6jsUJg{4{I)3lTPN$#m zO;FsN@0cq_x5B?IHU(NTDc^uva9Zs(Fx-*(fNY-csj;qv*!l{OZhbYoLCfVN4!TC% zK-0!_j#$rN7z3wE-Lg+vm7g@z9hl*MTJM$4kGKom|ITaRXL@d^F5$9eZe#T~^b0s_ j{M~GPRHD=PZ!tCt*sr|@|I1@~r=|=t7))J%MGspaCRVA5 literal 0 HcmV?d00001 From 947d8ae4419bde1fb301e05ba10905a7bd10db9f Mon Sep 17 00:00:00 2001 From: Jay <83922342+Jayfromthe13th@users.noreply.github.com> Date: Thu, 2 Jan 2025 17:36:04 -0600 Subject: [PATCH 05/12] Delete framework/libra-framework/backup_specs/slow_wallet.spec.move --- .../backup_specs/slow_wallet.spec.move | 25 ------------------- 1 file changed, 25 deletions(-) delete mode 100644 framework/libra-framework/backup_specs/slow_wallet.spec.move diff --git a/framework/libra-framework/backup_specs/slow_wallet.spec.move b/framework/libra-framework/backup_specs/slow_wallet.spec.move deleted file mode 100644 index c663b7bee..000000000 --- a/framework/libra-framework/backup_specs/slow_wallet.spec.move +++ /dev/null @@ -1,25 +0,0 @@ -spec ol_framework::slow_wallet { - spec module { - pragma verify = true; - // pragma aborts_if_is_strict; - } - - // setting a slow wallet should abort only if there is no SlowWalletList - // present in the 0x1 address - spec set_slow(sig: &signer) { - aborts_if !exists(@ol_framework); - } - - // at epoch boundaries the slow wallet drip should never abort - // if genesis is initialized properly - spec on_new_epoch(vm: &signer): (bool, u64) { - use ol_framework::sacred_cows::{SacredCow, SlowDrip}; - - aborts_if !system_addresses::signer_is_ol_root(vm); - - aborts_if !exists>(@0x2); - - aborts_if borrow_global>(@0x2).value != 35000 * 1000000; - - } -} From 24369107b50979ac4b0f978b04c88825768df979 Mon Sep 17 00:00:00 2001 From: Jay <83922342+Jayfromthe13th@users.noreply.github.com> Date: Thu, 2 Jan 2025 17:36:53 -0600 Subject: [PATCH 06/12] Delete framework/libra-framework/backup_specs/burn.spec.move --- .../libra-framework/backup_specs/burn.spec.move | 15 --------------- 1 file changed, 15 deletions(-) delete mode 100644 framework/libra-framework/backup_specs/burn.spec.move diff --git a/framework/libra-framework/backup_specs/burn.spec.move b/framework/libra-framework/backup_specs/burn.spec.move deleted file mode 100644 index a96f5af17..000000000 --- a/framework/libra-framework/backup_specs/burn.spec.move +++ /dev/null @@ -1,15 +0,0 @@ -spec ol_framework::burn { - use std::signer; - use diem_framework::system_addresses; - use ol_framework::libra_coin::LibraCoin; - use ol_framework::coin; - - spec module { - pragma verify = true; - pragma aborts_if_is_strict = false; - } - - spec initialize(vm: &signer) { - aborts_if !system_addresses::is_ol_framework_address(signer::address_of(vm)); - } -} From ba480b607c314b672ccf525e05392989a19865c8 Mon Sep 17 00:00:00 2001 From: Jay <83922342+Jayfromthe13th@users.noreply.github.com> Date: Thu, 2 Jan 2025 17:37:23 -0600 Subject: [PATCH 07/12] Delete framework/libra-framework/backup_specs/demo.spec.move --- .../backup_specs/demo.spec.move | 23 ------------------- 1 file changed, 23 deletions(-) delete mode 100644 framework/libra-framework/backup_specs/demo.spec.move diff --git a/framework/libra-framework/backup_specs/demo.spec.move b/framework/libra-framework/backup_specs/demo.spec.move deleted file mode 100644 index 4d426607c..000000000 --- a/framework/libra-framework/backup_specs/demo.spec.move +++ /dev/null @@ -1,23 +0,0 @@ -spec ol_framework::demo { - spec module { - pragma verify = true; - } - - spec print_this(account: &signer) { - // should not abort - pragma aborts_if_is_strict; - } - - // TODO in strict mode - spec set_message(account: &signer, message: string::String) { - // pragma aborts_if_is_strict; - // let events = borrow_global(signer::address_of(account)).message_change_events; - // aborts_if event::counter(events) > MAX_U64; - } - - spec get_message(addr: address): string::String { - pragma aborts_if_is_strict; - aborts_if !exists(addr); - - } -} From f2c55f906c5c6337114131279929a21883342be9 Mon Sep 17 00:00:00 2001 From: Jay <83922342+Jayfromthe13th@users.noreply.github.com> Date: Thu, 2 Jan 2025 17:37:49 -0600 Subject: [PATCH 08/12] Delete framework/libra-framework/backup_specs/libra_coin.spec.move --- .../backup_specs/libra_coin.spec.move | 43 ------------------- 1 file changed, 43 deletions(-) delete mode 100644 framework/libra-framework/backup_specs/libra_coin.spec.move diff --git a/framework/libra-framework/backup_specs/libra_coin.spec.move b/framework/libra-framework/backup_specs/libra_coin.spec.move deleted file mode 100644 index 06a6cfdf1..000000000 --- a/framework/libra-framework/backup_specs/libra_coin.spec.move +++ /dev/null @@ -1,43 +0,0 @@ -spec ol_framework::libra_coin { - spec module { - pragma verify = true; - pragma aborts_if_is_strict; - } - - spec initialize { - pragma aborts_if_is_partial; - let addr = signer::address_of(diem_framework); - ensures exists(addr); - ensures exists>(addr); - } - - spec destroy_mint_cap { - let addr = signer::address_of(diem_framework); - aborts_if addr != @diem_framework; - aborts_if !exists(@diem_framework); - } - - // Test function,not needed verify. - spec configure_accounts_for_test { - pragma verify = false; - } - - // // Only callable in tests and testnets.not needed verify. - // spec mint { - // pragma verify = false; - // } - - // Only callable in tests and testnets.not needed verify. - spec delegate_mint_capability { - pragma verify = false; - } - - // Only callable in tests and testnets.not needed verify. - spec claim_mint_capability(account: &signer) { - pragma verify = false; - } - - spec find_delegation(addr: address): Option { - aborts_if !exists(@core_resources); - } -} From d9565ce627e14fefe693ce9ef88a90390361f315 Mon Sep 17 00:00:00 2001 From: Jay <83922342+Jayfromthe13th@users.noreply.github.com> Date: Thu, 2 Jan 2025 17:38:09 -0600 Subject: [PATCH 09/12] Delete framework/libra-framework/backup_specs/ol_account.spec.move --- .../backup_specs/ol_account.spec.move | 101 ------------------ 1 file changed, 101 deletions(-) delete mode 100644 framework/libra-framework/backup_specs/ol_account.spec.move diff --git a/framework/libra-framework/backup_specs/ol_account.spec.move b/framework/libra-framework/backup_specs/ol_account.spec.move deleted file mode 100644 index 5c8495c69..000000000 --- a/framework/libra-framework/backup_specs/ol_account.spec.move +++ /dev/null @@ -1,101 +0,0 @@ -spec ol_framework::ol_account { - spec module { - pragma verify = true; - // pragma aborts_if_is_strict; - invariant [suspendable] chain_status::is_operating() ==> exists(@diem_framework); - invariant [suspendable] chain_status::is_operating() ==> exists>(@diem_framework); - - } - - // /// Check if the bytes of the auth_key is 32. - // /// The Account does not exist under the auth_key before creating the account. - // /// Limit the address of auth_key is not @vm_reserved / @diem_framework / @diem_toke. - // spec create_account(auth_key: address) { - // include CreateAccountAbortsIf; - // ensures exists(auth_key); - // ensures exists>(auth_key); - // } - spec schema CreateAccountAbortsIf { - auth_key: address; - aborts_if exists(auth_key); - aborts_if length_judgment(auth_key); - aborts_if auth_key == @vm_reserved || auth_key == @diem_framework || auth_key == @diem_token; - } - - spec fun length_judgment(auth_key: address): bool { - use std::bcs; - - let authentication_key = bcs::to_bytes(auth_key); - len(authentication_key) != 32 - } - - // ol_account::withdraw can never use more than the slow wallet limit - spec withdraw(sender: &signer, amount: u64): Coin{ - include AssumeCoinRegistered; - - let account_addr = signer::address_of(sender); - aborts_if amount == 0; - - let coin_store = global>(account_addr); - let balance = coin_store.coin.value; - - aborts_if balance < amount; - - // in the case of slow wallets - let slow_store = global(account_addr); - aborts_if exists(account_addr) && - slow_store.unlocked < amount; - - ensures result == Coin{value: amount}; - } - - spec schema AssumeCoinRegistered { - sender: &signer; - let account_addr = signer::address_of(sender); - aborts_if !coin::is_account_registered(account_addr); - } - - spec assert_account_exists(addr: address) { - aborts_if !account::exists_at(addr); - } - - /// Check if the address existed. - /// Check if the LibraCoin under the address existed. - spec assert_account_is_registered_for_gas(addr: address) { - aborts_if !account::exists_at(addr); - aborts_if !coin::is_account_registered(addr); - } - - spec set_allow_direct_coin_transfers(account: &signer, allow: bool) { - let addr = signer::address_of(account); - include !exists(addr) ==> account::NewEventHandleAbortsIf; - } - - // spec batch_transfer(source: &signer, recipients: vector
, amounts: vector) { - // // TODO: missing aborts_if spec - // pragma verify=false; - // } - - spec can_receive_direct_coin_transfers(account: address): bool { - aborts_if false; - ensures result == ( - !exists(account) || - global(account).allow_arbitrary_coin_transfers - ); - } - - // spec batch_transfer_coins(from: &signer, recipients: vector
, amounts: vector) { - // // TODO: missing aborts_if spec - // pragma verify=false; - // } - - // spec deposit_coins(to: address, coins: Coin) { - // // TODO: missing aborts_if spec - // pragma verify=false; - // } - - // spec transfer_coins(from: &signer, to: address, amount: u64) { - // // TODO: missing aborts_if spec - // pragma verify=false; - // } -} From b91a2794c890872e4f5c3aa622e80b1b0df92693 Mon Sep 17 00:00:00 2001 From: Jay <83922342+Jayfromthe13th@users.noreply.github.com> Date: Thu, 2 Jan 2025 17:38:43 -0600 Subject: [PATCH 10/12] Delete framework/libra-framework/backup_specs/sacred_cows.spec.move --- .../backup_specs/sacred_cows.spec.move | 46 ------------------- 1 file changed, 46 deletions(-) delete mode 100644 framework/libra-framework/backup_specs/sacred_cows.spec.move diff --git a/framework/libra-framework/backup_specs/sacred_cows.spec.move b/framework/libra-framework/backup_specs/sacred_cows.spec.move deleted file mode 100644 index b05229721..000000000 --- a/framework/libra-framework/backup_specs/sacred_cows.spec.move +++ /dev/null @@ -1,46 +0,0 @@ -spec ol_framework::sacred_cows { - spec module { - use diem_framework::chain_status; - pragma verify = true; - pragma aborts_if_is_strict; - - invariant [suspendable] chain_status::is_operating() ==> - exists>(@0x2); - - invariant [suspendable] chain_status::is_operating() ==> - borrow_global>(@0x2).value == 30000 * 1000000; - } - - // only 0x2 can init - spec init(zero_x_two_sig: &signer) { - use std::signer; - aborts_if signer::address_of(zero_x_two_sig) != @0x2; - aborts_if exists>(@0x2); - - } - - // only 0x2 can init - spec get_stored(): u64 { - - } - - // only 0x2 can init - spec assert_same(stored: u64, code: u64) { - aborts_if stored != code; - } - - // only 0x2 can init - spec bless_this_cow(zero_x_two_sig: &signer, value: u64) { - use std::signer; - use diem_framework::chain_status; - aborts_if signer::address_of(zero_x_two_sig) != @0x2; - aborts_if exists>(@0x2); - aborts_if !chain_status::is_genesis(); - } - - - spec get_slow_drip_const(): u64 { - aborts_if !exists>(@0x2); - aborts_if borrow_global>(@0x2).value != SLOW_WALLET_EPOCH_DRIP; - } -} From f489889fe0be29ec4e871a491cdb52231231ffcb Mon Sep 17 00:00:00 2001 From: Jayfromthe13th Date: Thu, 2 Jan 2025 19:32:57 -0600 Subject: [PATCH 11/12] Remove backup_specs folder --- .../libra-framework/backup_specs/vouch.spec.move | Bin 1020 -> 0 bytes 1 file changed, 0 insertions(+), 0 deletions(-) delete mode 100644 framework/libra-framework/backup_specs/vouch.spec.move diff --git a/framework/libra-framework/backup_specs/vouch.spec.move b/framework/libra-framework/backup_specs/vouch.spec.move deleted file mode 100644 index 673fd6a37281f96c9ff49ba1c110d1f7a0f85f53..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 1020 zcmcJOy-veG5QL}ZDO{3<2S^AFEfoc=W&DSQokTu65FuV2`1TIRMwlQ9WSzaY*`1r6 zxxBwQ?UXB3q^)YjD%2`bL+*)8t4A$)_QX9^57fQrjCXi?IVvM%s`xfP_NVk$+GsV? zd+OYpu6xfY=JbGJd~S~U>l4UM9n7rWQD1U?4%Qrp-}pNn!00|_OhC;*%E{UMZWi;@ zTsf+5y`C|e<|uD21a70cqc;uJ84lD`eRW`PV&_#V@gSjM@6jsUJg{4{I)3lTPN$#m zO;FsN@0cq_x5B?IHU(NTDc^uva9Zs(Fx-*(fNY-csj;qv*!l{OZhbYoLCfVN4!TC% zK-0!_j#$rN7z3wE-Lg+vm7g@z9hl*MTJM$4kGKom|ITaRXL@d^F5$9eZe#T~^b0s_ j{M~GPRHD=PZ!tCt*sr|@|I1@~r=|=t7))J%MGspaCRVA5 From a7b3feb21c489dead8ed718eced87fac09b33fd0 Mon Sep 17 00:00:00 2001 From: Jayfromthe13th Date: Thu, 2 Jan 2025 19:32:57 -0600 Subject: [PATCH 12/12] Trigger workflow