22 lines
2.2 KiB
Markdown
22 lines
2.2 KiB
Markdown
## Protocol properties and invariants
|
|
|
|
Below is a list of all documented properties and invariants of this project that must hold true.
|
|
|
|
- **Property** - Describes the property of the project / protocol that should ultimately be tested and formaly verified.
|
|
- **Type** - Properties are split into 5 main types: **Valid State**, **State Transition**, **Variable Transition**,
|
|
**High-Level Property**, **Unit Test**
|
|
- **Risk** - One of **High**, **Medium** and **Low**, depending on the property's risk factor
|
|
- **Tested** - Whether this property has been (fuzz) tested
|
|
|
|
| **Property** | **Type** | **Risk** | **Tested** |
|
|
| --------------------------------------------------------------------------------------------------------- | ------------------- | -------- | ---------- |
|
|
| Only allows deployment with valid signature | Unit test | High | Yes |
|
|
| Adds Owner token entry to registry upon deployment | Unit test | Low | Yes |
|
|
| Only one deployment per account allowed | Unit test | Medium | Yes |
|
|
| One and only one owner token address exists in the registry per community | Valid state | High | Yes |
|
|
| If deployment registry address changes, sender must be owner | Variable transition | High | Yes |
|
|
| If owner token factory address changes, sender must be owner | Variable transition | High | Yes |
|
|
| If master token factory address changes, sender must be owner | Variable transition | High | Yes |
|
|
| Registry grows as the more accounts perform a deployment | High-Level Property | Low | No |
|
|
| No addresses other than the receiver addresses change an addresse's balance when batch transfering tokens | High-Level Property | High | Yes |
|