/
compliant-spec.k
79 lines (68 loc) · 2.47 KB
/
compliant-spec.k
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
requires "hcs.k"
module COMPLIANT-SPEC
imports HCS
/*
If and account is not frozen (default value) and has KYC set to false, and setKycPassed() is called, then checkTransferAllowed() should return true
Pre-conditions
* Owner != 0x
* caller = ComplianceManager || caller = Owner
* !Frozen[addr]
* !KycPassed[addr]
Post-conditions
* KycPassed[addr]
* result = true
*/
rule <k> setKycPassed(Target:Int, {caller: Caller})
~>
checkTransferAllowed(Target:Int) => true ...</k>
<tokenOwner> Owner </tokenOwner>
<complianceManager> ComplianceManager </complianceManager>
<kycpassed> ... (Target |-> false => Target |-> true) ... </kycpassed>
<frozen> ... (Target |-> false) ... </frozen>
requires Owner =/=Int 0
andBool (Caller ==Int ComplianceManager orBool Caller ==Int Owner)
/*
If and account is not frozen (default value) and has KYC set to false, and setKycPassed() is called and then freeze() is called,
then checkTransferAllowed() should return false
Pre-conditions
* Owner != 0x
* caller = ComplianceManager || caller = Owner
* !Frozen[addr]
* !KycPassed[addr]
Post-conditions
* KycPassed[addr]
* Frozen[addr]
* result = true
*/
rule <k> setKycPassed(Target:Int, {caller: Caller})
~>
freeze(Target:Int, {caller: Caller})
~>
checkTransferAllowed(Target:Int) => false ...</k>
<tokenOwner> Owner </tokenOwner>
<complianceManager> ComplianceManager </complianceManager>
<supplyManager> SupplyManager </supplyManager>
<enforcementManager> EnforcementManager </enforcementManager>
<kycpassed>... (Target |-> false => Target |-> true) ... </kycpassed>
<frozen> ... (Target |-> false => Target |-> true) ... </frozen>
requires Owner =/=Int 0
andBool (Caller ==Int ComplianceManager orBool Caller ==Int Owner)
andBool Target =/=Int Owner
andBool Target =/=Int SupplyManager
andBool Target =/=Int ComplianceManager
andBool Target =/=Int EnforcementManager
/*
Detect transfer restriction
Pre-conditions
* Owner != 0x
* Frozen[addr] || !KycPassed[addr]
Post-conditions
* result = false
*/
rule <k> checkTransferAllowed(Target:Int) => false ...</k>
<tokenOwner> Owner </tokenOwner>
<kycpassed>... (Target |-> ValK:Bool) ... </kycpassed>
<frozen> ... (Target |-> ValF:Bool) ... </frozen>
requires Owner =/=Int 0
andBool (notBool ValK orBool ValF)
endmodule