4. Specs for mint and burn

Now that we have seen rules for transfer, think of some properties for mint and burn and write them in the src/certora/spec.rs file. To run them, create your own .conf files under confs/ by looking at the existing conf files. You will only need to change the names of the rules passed into the "rule" field. The rest should be the same.

You can see several rules we have written for these functions in solutions/solution_specs.rs of branch solutions.

Solution

solution_specs.rs

// Exercise 4
#[rule]
fn burn_is_correct(e: Env, from: Address, amount: i64) {
    let balance_before = Token::balance(&e, from.clone());
    Token::burn(&e, from.clone(), amount);
    let balance_after = Token::balance(&e, from.clone());
    cvt::assert!(balance_after == balance_before - amount);
}

// Exercise 4
#[rule]
fn mint_is_authorized(e: Env, to: Address, amount: i64) {
    let admin = e
            .storage()
            .persistent()
            .get::<_, Address>(&"ADMIN")
            .unwrap();
    require!(is_auth(admin), "admin is authorized");
    Token::mint(&e, to, amount);
    cvt::satisfy!(true);
}

// Exercise 4
#[rule]
fn mint_not_authorized_fails(e: Env, to: Address, amount: i64) {
    let admin = e
            .storage()
            .persistent()
            .get::<_, Address>(&"ADMIN")
            .unwrap();
    require!(!is_auth(admin), "admin is not authorized");
    Token::mint(&e, to, amount);
    cvt::assert!(false); // should pass
}

// Exercise 4
#[rule]
fn mint_is_correct(e: Env, to: Address, amount: i64) {
    let balance_before = Token::balance(&e, to.clone());
    Token::mint(&e, to.clone(), amount);
    let balance_after = Token::balance(&e, to.clone());
    cvt::assert!(balance_after == balance_before + amount);
}