otter_solana_verify/
lib.rs

1//! > **Formal Verification for SOLANA Programs**
2//!
3//! ## Invariants
4//!
5//! Invariants are properties that should always be true.  For example, the balance of a token account should never be negative. There are two types of invariants in the Solana programs: `account invariants` and `instruction invariants`.
6//!
7//! ### Instruction Invariants
8//!   An instruction invariant specifies sufficient conditions for an instruction to succeed (or fail). These are specified as `succeeds_if` or `errors_if` macro annotations on the instruction handler.
9//!   - `succeeds_if` - The instruction should succeed if and only if the given condition is true.
10//!   ```
11//!  #[succeeds_if(
12//!    ctx.user.balance >= amount
13//!     )]
14//! pub fn withdraw(ctx: Context<Withdraw>, amount: u64) {
15//!    ...
16//! }
17//! ```
18//!
19//!   - `errors_if` - The instruction should fail if and only if the given condition is true.
20//!   ```rust
21//! #[errors_if(
22//!     ctx.user.balance < amount
23//!    )]
24//!     pub fn withdraw(ctx: Context<Withdraw>, amount: u64) {
25//!         ...
26//!     }
27//!    ```
28//!
29//! ### Account Invariants
30//! The other type of invariant is an Account Invariant.
31//! This invariant describes some property of an account that should always hold.
32//! We use the `invariant` macro to specify these invariants.
33//!
34//! - `invariant` - The account invariant should hold if and only if the given condition is true.
35//! For example, the balance of a token account should never be negative.
36//!
37//! ```rust
38//!     #[account]
39//!     #[invariant(
40//!         self.balance >= 0
41//!     )]
42//!     struct User {
43//!         pub balance: i64,
44//!     }
45//! ```
46
47extern crate proc_macro;
48use proc_macro::TokenStream;
49use quote::quote;
50
51/// The instruction should succeed if and only if the given condition is true.
52#[proc_macro_attribute]
53pub fn succeeds_if(_args: TokenStream, input: TokenStream) -> TokenStream {
54    input
55}
56
57/// The instruction should fail if and only if the given condition is true.
58#[proc_macro_attribute]
59pub fn errors_if(_args: TokenStream, input: TokenStream) -> TokenStream {
60    input
61}
62
63/// The account invariant should hold if and only if the given condition is true.
64#[proc_macro_attribute]
65pub fn invariant(_args: TokenStream, input: TokenStream) -> TokenStream {
66    input
67}
68
69/// Ignore the following block of code for verification
70#[proc_macro_attribute]
71pub fn verify_ignore(_args: TokenStream, input: TokenStream) -> TokenStream {
72    input
73}
74
75/// The account has a constraint defined
76#[proc_macro_attribute]
77pub fn has_constraint(_args: TokenStream, input: TokenStream) -> TokenStream {
78    input
79}
80
81#[proc_macro_derive(Arbitrary)]
82pub fn derive_arbitrary(_item: TokenStream) -> TokenStream {
83    (quote! {}).into()
84}
otter_solana_verify/lib.rs

otter_solana_verify/
lib.rs
