From 7dc11a19eb6a56c7c816ac3ac9b6a4c6845bc1f2 Mon Sep 17 00:00:00 2001
From: Jayfromthe13th <jtbfive0@yahoo.com>
Date: Mon, 30 Dec 2024 13:56:29 -0600
Subject: [PATCH] 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<BurnCounter>(@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<BurnCounter>(@ol_framework).lifetime_recycled == 0; // Ensures lifetime_recycled is initialized to 0
+    }
+
+    spec burn_and_track(coin: Coin<LibraCoin>) {
+        requires exists<BurnCounter>(@ol_framework); // Requires a BurnCounter to exist
+        aborts_if !exists<BurnCounter>(@ol_framework); // Aborts if no BurnCounter exists
+        ensures global<BurnCounter>(@ol_framework).lifetime_burned == 
+            old(global<BurnCounter>(@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<UserBurnPreference>(addr); // Ensures UserBurnPreference exists for the address
+        ensures global<UserBurnPreference>(addr).send_community == community; // Ensures send_community is set correctly
+        requires exists<UserBurnPreference>(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<BurnCounter>(@ol_framework).lifetime_burned >= old(global<BurnCounter>(@ol_framework).lifetime_burned); // Ensures lifetime_burned does not decrease
+        requires global<BurnCounter>(@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})TUYQ<D3%<kTCi;DP{VIN;J%7*{s?El&v7jXO
zo;<658(c$c7537xCjnb^z#fE@7M&Y~$w5#e!SafiSJ`N>qJSE2>}}e$nMp>}#(Gz&
zwo<Oz3+t88<J9i7HV+Q+N;HqhGbH63rSy|<s!3-OSZ0sbABzR{ZlK_k!D^+k-}>%~
zej2o2z-A3M3C(E7=*2})ju1Eqtz_C=yq0ei!LI>xiy-K)HxO<W-7@=eof))*8Uc6v
zx!8WdN9DY`{T&-5z~!G@7U(ts*#)fEn^DRPKt%XOGV5tFC6RD4sCE<|gi~{Iu-ll+
z141VbSkfR!j<6e?=M)r`LjuKl;jti*k^W*bWy?%1TWxBg&p>gl`o`?2RI7yX%mt>E
za2fIPDC>~InS2XKz3JZspq4-&gp9{Xl(=)MXYOGGH+*Tup7Xp2%d-;98H62tXEPB-
z-<Mn4;=$Z=U(<zgMa4aVX2Q}O&3yaL%q<CTpdI=quvF@Z-gpQH7Nkz+Lo2k4ME3!S
z{GuUoP_d<Qy=y%!#cY<jVlx?(z6*6wHs<Ri{u5dU<~s2gJakBHeDStc#npdP!D5u=
zMFg0=`e9cSD8%2nkP;9Q8;imr5baa%9>b(?G>l3*-xo5s>k01}Ew3g$_mzCHnC&!a
zh!;I^TLS1g-h9WGJB`@737r-g<Z-Vo(#(h~9>EP=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<JM2wN3o#4xxSv<55L{`n8ifu#7c$F^Ser%
q^a{)_KB`Y7hDR0j@$)Cf_h+7&j=L;d#s^nSn`^YVi{KE@PyYb?K;F{;

literal 1022
zcmcJO%}#?r6ot>)#CKq6H$FhMZrr+Z(Jev#BtqLTfHtPDu6}orf)Q(67&61m<=!*r
zo-@3^Iqj4xR-mm)h00VbQbp{UNUbL=c{<iDS&!ts>WsO6S~)TUB`SDVKi0?87ux7*
zruNjiB~=feQOM~%hVi*O#&1s`J2fz~d`EuH`6*a)9Dd{Pv<IX4>@fm00VySB{kvJr
zQ+=hVzV&*BXquwDxzKYP)g8U5$WCyeB<rgKgA+TiQjP}^8J$NfaC6UY#c2565}kHG
zUmKygIp5G%h;EsmZEXtFL}K1OYQ|}$*T8T`<^!^M-jQQf5o@c<Ji67D>;^5DlXb6a
zzzsBQOy_{{0){bgy4F4Wm{Isn6RpAQ@2Az?=;DaG!2R#M27adJhU^?JTlzLue?z~7
n!^Ypu%CB;C8vhn!vw;1|d+@(Jrgv(}Ac4Wu^#ghwbk6(%d6%h{