add a few sample specs

crates/sui-framework/sources/balance.move

@@ -63,26 +63,46 @@ module sui::balance {
         Balance { value: 0 }
     }
 
+    spec zero {
+        aborts_if false;
+        ensures result.value == 0;
+    }
+
     /// Join two balances together.
     public fun join<T>(self: &mut Balance<T>, balance: Balance<T>): u64 {
         let Balance { value } = balance;
         self.value = self.value + value;
         value
     }
 
+    spec join {
+        ensures self.value == old(self.value) + balance.value;
+        ensures result == balance.value;
+    }
+
     /// Split a `Balance` and take a sub balance from it.
     public fun split<T>(self: &mut Balance<T>, value: u64): Balance<T> {
         assert!(self.value >= value, ENotEnough);
         self.value = self.value - value;
         Balance { value }
     }
 
+    spec split {
+        aborts_if self.value < value with ENotEnough;
+        ensures self.value == old(self.value) - value;
+        ensures result.value == value;
+    }
+
     /// Destroy a zero `Balance`.
     public fun destroy_zero<T>(balance: Balance<T>) {
         assert!(balance.value == 0, ENonZero);
         let Balance { value: _ } = balance;
     }
 
+    spec destroy_zero {
+        aborts_if balance.value != 0 with ENonZero;
+    }
+
     #[test_only]
     /// Create a `Balance` of any coin for testing purposes.
     public fun create_for_testing<T>(value: u64): Balance<T> {