solid-grinder 0.4.0

A CLI that goes along with building blocks of smart contract. Along with our front-end snippets, this toolbox can reduce L2 gas cost by encoding calldata for dApps development to use as little bytes of calldata as possible.
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108

import "helpers/helpers.spec"
import "methods/IOwnable2Step.spec"

methods {
    restricted()
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Function correctness: transferOwnership sets the pending owner                                                      │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule transferOwnership(env e) {
    require nonpayable(e);

    address newOwner;
    address current = owner();

    transferOwnership@withrevert(e, newOwner);
    bool success = !lastReverted;

    assert success <=> e.msg.sender == current, "unauthorized caller";
    assert success => pendingOwner() == newOwner, "pending owner not set";
    assert success => owner() == current, "current owner changed";
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Function correctness: renounceOwnership removes the owner and the pendingOwner                                      │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule renounceOwnership(env e) {
    require nonpayable(e);

    address current = owner();

    renounceOwnership@withrevert(e);
    bool success = !lastReverted;

    assert success <=> e.msg.sender == current, "unauthorized caller";
    assert success => pendingOwner() == 0, "pending owner not cleared";
    assert success => owner() == 0, "owner not cleared";
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Function correctness: acceptOwnership changes owner and reset pending owner                                         │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule acceptOwnership(env e) {

    require nonpayable(e);

    address current = owner();
    address pending = pendingOwner();

    acceptOwnership@withrevert(e);
    bool success = !lastReverted;

    assert success <=> e.msg.sender == pending, "unauthorized caller";
    assert success => pendingOwner() == 0, "pending owner not cleared";
    assert success => owner() == pending, "owner not transferred";
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Access control: only current owner can call restricted functions                                                    │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule onlyCurrentOwnerCanCallOnlyOwner(env e) {
    require nonpayable(e);

    address current = owner();

    calldataarg args;
    restricted@withrevert(e, args);

    assert !lastReverted <=> e.msg.sender == current, "access control failed";
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: ownership and pending ownership can only change in specific ways                                              │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule ownerOrPendingOwnerChange(env e, method f) {
    address oldCurrent = owner();
    address oldPending = pendingOwner();

    calldataarg args;
    f(e, args);

    address newCurrent = owner();
    address newPending = pendingOwner();

    // If owner changes, must be either acceptOwnership or renounceOwnership
    assert oldCurrent != newCurrent => (
        (e.msg.sender == oldPending && newCurrent == oldPending && newPending == 0 && f.selector == acceptOwnership().selector) ||
        (e.msg.sender == oldCurrent && newCurrent == 0          && newPending == 0 && f.selector == renounceOwnership().selector)
    );

    // If pending changes, must be either acceptance or reset
    assert oldPending != newPending => (
        (e.msg.sender == oldCurrent && newCurrent == oldCurrent &&                    f.selector == transferOwnership(address).selector) ||
        (e.msg.sender == oldPending && newCurrent == oldPending && newPending == 0 && f.selector == acceptOwnership().selector) ||
        (e.msg.sender == oldCurrent && newCurrent == 0          && newPending == 0 && f.selector == renounceOwnership().selector)
    );
}