From 00c5c579528e6774b797631537cf0065d1504685 Mon Sep 17 00:00:00 2001 From: Jayfromthe13th Date: Sun, 17 Nov 2024 13:28:42 -0600 Subject: [PATCH 1/6] 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 2/6] 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 a66f12c1e56bc324e654eb5e6cbbcee26895a21c Mon Sep 17 00:00:00 2001 From: Jay <83922342+Jayfromthe13th@users.noreply.github.com> Date: Sun, 17 Nov 2024 14:25:40 -0600 Subject: [PATCH 3/6] Update vouch.spec.move --- .../sources/ol_sources/vouch.spec.move | Bin 1022 -> 3575 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 75607e11825ba929235bc61041f8f703c5d085ff..93888b8e9ad2f692cc0312e06a33a280b7c48f92 100644 GIT binary patch literal 3575 zcmbtWU2oeq6n!7C|G>Tk5@xu`Fzi7~f_bT%8t`nxc7qnfK+qCx6Ol!Oq?`mn{`>Bg zM3J(THtvETFr52&&f&dR?|DpQO4o|*_=8mUQFM@byd}>+|3u&?*PJAR?|g$;itG>f z@1}PuR*F$HiJ~!nzG+%(lSGjgn~WcX5F!;>U2lfOXQ|vi${_Iqs^$>^!=I8cU2{-puLvlajG|a(2HMa8=rK=CkFaC-OR9*7 zNdEh8mA4?5KSIk9u~_G6#Qr1xMQYhGI|bq(>jS7UsZ^jS=r1Vwbo%Q7Z?V_|EuiWO ze;{NfW$Lr=ePBzxu$mT>4eIN3VUJYBw8T}E59*TlJlH6Ba1shWD~Cyslp>-mj%Dsw z?bn-fLn_Z=xPVkj_b95Gq;hRz+x&>XdnK;rW+0dmg^Fzfo(l$e5N1obQc!Y)Pag?j zYLo8(;b6F&f2E7z_#?fWe!lrc=flBx{MFCzvc9Wk!YvGh?9L7Zzn1U~skLE-2gBR> zV6vRf>14X3qseILr*thBs9`#Qs}kZjvU?-dtGdPh1_SnGZZ@zW>XCFzW9X{*K8huH z*vrT1=g9|b#<|;<{_MWOh}hd+YLLZ`G>8%2{r}cpIv*-51)51i`Qu(Fo}4lrv8y;& z3dBW=fep<0t1^l<+|Y(a(9OL^;Ww9&$GQX9Vs1BFJxbm%UHxZkiGm?f>_Ml)?#<{G zV_kzaOogOJ1T4LJ6p1Y1kNDzk;MR)7L4Opj2t>}#a6%T<^cyP?XYVg$_+>Vl50<0p zgbv4p*<$#C4rkMwPYZJ0B*uZ&EdmV-AC8vdp^xmL;bY_OhJDx3GgSKb4z{Q#b6=H=PXXtqy{OMohVS^q7sahDXd-T~3 z7q)Blg>X2w{aP^21wB7M_l!El)#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 002172e1eee81eaa1e92937e4869a28bd09efd32 Mon Sep 17 00:00:00 2001 From: Jay <83922342+Jayfromthe13th@users.noreply.github.com> Date: Sun, 17 Nov 2024 15:37:41 -0600 Subject: [PATCH 4/6] Create burn.spec.move added indepth spec for burn.move module --- .../sources/ol_sources/burn.spec.move | 86 +++++++++++++++++++ 1 file changed, 86 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..92d75a985 --- /dev/null +++ b/framework/libra-framework/sources/ol_sources/burn.spec.move @@ -0,0 +1,86 @@ +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 = true; + + // Global invariant: BurnCounter must be initialized before any operations + invariant [suspendable] exists(@ol_framework); + } + + spec BurnCounter { + // Resource invariant + invariant lifetime_burned <= MAX_U64; + invariant lifetime_recycled <= MAX_U64; + } + + spec initialize { + let addr = signer::address_of(vm); + + // Preconditions + requires system_addresses::is_ol_framework_address(addr); + + // Abort conditions + aborts_if !system_addresses::is_ol_framework_address(addr); + aborts_if exists(@ol_framework); + + // Postconditions + ensures exists(@ol_framework); + ensures global(@ol_framework).lifetime_burned == 0; + ensures global(@ol_framework).lifetime_recycled == 0; + } + + spec epoch_burn_fees { + let addr = signer::address_of(vm); + let initial_value = coin::value(coins); + let pre_burned = global(@ol_framework).lifetime_burned; + + // Preconditions + requires system_addresses::is_ol_framework_address(addr); + requires exists(@ol_framework); + requires pre_burned + initial_value <= MAX_U64; + + // Abort conditions + aborts_if !system_addresses::is_ol_framework_address(addr); + aborts_if !exists(@ol_framework); + aborts_if pre_burned + initial_value > MAX_U64; + + // Postconditions + ensures exists(@ol_framework); + ensures result_1 ==> global(@ol_framework).lifetime_burned > pre_burned; + ensures !result_1 ==> global(@ol_framework).lifetime_burned == pre_burned; + } + + spec burn_and_track(coin: Coin) { + let pre_burned = global(@ol_framework).lifetime_burned; + let amount = coin::value(coin); + + // Preconditions + requires exists(@ol_framework); + requires pre_burned + amount <= MAX_U64; + + // Abort conditions + aborts_if !exists(@ol_framework); + aborts_if pre_burned + amount > MAX_U64; + + // Postconditions + ensures global(@ol_framework).lifetime_burned == pre_burned + amount; + ensures global(@ol_framework).lifetime_recycled == + old(global(@ol_framework).lifetime_recycled); + } + + 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; + + // Postconditions + ensures exists(addr); + ensures global(addr).send_community == community; + } +} From aeeee43d6990d3e8769187252cca7991dae7d545 Mon Sep 17 00:00:00 2001 From: Jay <83922342+Jayfromthe13th@users.noreply.github.com> Date: Tue, 19 Nov 2024 20:05:54 -0600 Subject: [PATCH 5/6] Update burn.spec.move --- framework/libra-framework/sources/ol_sources/burn.spec.move | 5 ----- 1 file changed, 5 deletions(-) diff --git a/framework/libra-framework/sources/ol_sources/burn.spec.move b/framework/libra-framework/sources/ol_sources/burn.spec.move index 92d75a985..a07736e1a 100644 --- a/framework/libra-framework/sources/ol_sources/burn.spec.move +++ b/framework/libra-framework/sources/ol_sources/burn.spec.move @@ -1,9 +1,4 @@ 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 = true; From 47baa5b930c61445fdab8034419005438b2163a7 Mon Sep 17 00:00:00 2001 From: Jay <83922342+Jayfromthe13th@users.noreply.github.com> Date: Thu, 21 Nov 2024 00:00:21 -0600 Subject: [PATCH 6/6] Forgot to update comment --- framework/libra-framework/sources/ol_sources/vouch.spec.move | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/framework/libra-framework/sources/ol_sources/vouch.spec.move b/framework/libra-framework/sources/ol_sources/vouch.spec.move index 93888b8e9..763e92179 100644 --- a/framework/libra-framework/sources/ol_sources/vouch.spec.move +++ b/framework/libra-framework/sources/ol_sources/vouch.spec.move @@ -15,7 +15,7 @@ spec ol_framework::vouch { len(global(addr).epoch_vouched); } - // Previous specs remain the same... + spec true_friends(addr: address): vector
{ pragma aborts_if_is_partial = true;