Auto-callable note
This contract is the transcription to archetype of the following auto-callable note from Goldman Sachs:
Thank you to Alain Frisch, CTO at Lexifi, for this example contract and his help to transcode it. Lexifi provides financial services with a DSL (Domain Specific Language) to execute and simulate financial contracts. Alain Frish also provided the corresponding Lexifi code, automatically extracted by Lexifi drivers from the above document.
The key here is that a smart contract is passive regarding decisions to transfer currencies: a smart contract cannot be programmed to transfer or withdraw currencies : a transfer of currency results from a call to the contract, and there is no instruction for a contract to withdraw currencies from another account.
As a result, the contract is designed as follows: the issuer transfers to the contract, interests and redeem amount in due time (the contract serves as an escrow account); the owner can withdraw transferred amount at any time and can check, at any time, the total transferred, if he thinks there is a default in payment. If the total transferred amount does not correspond to the expected amount according to contract rules, then the contract goes to a specific state (Defaulted).
Underlying's values are transferred and logged to the contract in order to compute expected payment. These values are signed by the oracle (typically the exchange institution).
The contract has 2 actions :
  • pay_note : the issuer uses this action to transfer currency to the contract
  • add_fixing : logs underlying values
and 4 transitions :
  • confirm : the owner has transferred the nominal to the contract
  • cancel : the owner can cancel the contract
  • check : the owner can check transferred amount
  • terminate : finalises contract state when everything is ok
Below is the contract state machine diagram :
auto-callable state diagram
autocallable.arl
1
archetype autocallable
2
3
constant issuer : role = @tz1KksC8RvjUWAbXYJuNrUbontHGor25Cztk
4
constant owner : role = @tz1uNrUbontHGor25CztkKksC8RvjUWAbXYJ
5
constant oracle : role = @tz1r25CztkKksC8RvjuNrUWAbXYJUbontHGo (* exchange *)
6
7
constant nominal : tez = 1000tz
8
9
constant trade : date = 2017-03-14T00:00:00
10
constant init : date = 2017-03-14T00:00:00
11
constant issue : date = 2017-03-28T00:00:00
12
constant final : date = 2020-03-16T00:00:00
13
constant gredemption : date = 2020-03-30T00:00:00
14
15
(* UNDERLYINGS *)
16
constant bac_initial : rational = 25.32
17
constant sg_initial : rational = 46.945
18
constant ubs_initial : rational = 15.98
19
20
constant bac_strike : rational = 12.66 (* ~ 0.5 * bac_initial *)
21
constant sg_strike : rational = 23.4725 (* ~ 0.5 * sg_initial *)
22
constant ubs_strike : rational = 15.98 (* ~ 0.5 * ubs_initial *)
23
24
(* CONTRACT DATA *)
25
asset early identified by eobservation {
26
eobservation : date;
27
redemption : date;
28
trigger : rational;
29
value : rational;
30
} with {
31
i1 : 0 <= trigger <= 1;
32
i2 : 0 <= value <= 1;
33
} initialized by [
34
{ 2018-03-14T00:00:00; 2018-03-28T00:00:00; 0.95; 1 };
35
{ 2018-06-14T00:00:00; 2018-06-28T00:00:00; 0.95; 1 };
36
{ 2018-09-14T00:00:00; 2018-09-28T00:00:00; 0.95; 1 };
37
{ 2018-12-14T00:00:00; 2019-01-02T00:00:00; 0.95; 1 };
38
{ 2019-03-14T00:00:00; 2019-03-28T00:00:00; 0.80; 1 };
39
{ 2019-06-14T00:00:00; 2019-06-28T00:00:00; 0.80; 1 };
40
{ 2019-09-16T00:00:00; 2020-09-30T00:00:00; 0.70; 1 };
41
{ 2019-12-16T00:00:00; 2020-01-02T00:00:00; 0.70; 1 };
42
{ 2020-03-16T00:00:00; 2020-03-30T00:00:00; 0.70; 1 }
43
]
44
45
asset interest identified by iobservation {
46
iobservation : date;
47
payment : date;
48
barrier : rational;
49
rate : rational;
50
} with {
51
i3 : 0 <= barrier <= 1;
52
} initialized by [
53
{ 2017-06-14T00:00:00; 2017-06-28T00:00:00; 0.5; 2.025 };
54
{ 2017-09-14T00:00:00; 2017-09-28T00:00:00; 0.5; 4.05 };
55
{ 2017-12-14T00:00:00; 2018-01-02T00:00:00; 0.5; 6.075 };
56
{ 2018-03-14T00:00:00; 2018-03-28T00:00:00; 0.5; 8.1 };
57
{ 2018-06-14T00:00:00; 2018-06-28T00:00:00; 0.5; 10.125 };
58
{ 2018-09-14T00:00:00; 2018-09-28T00:00:00; 0.5; 12.15 };
59
{ 2018-12-14T00:00:00; 2019-01-02T00:00:00; 0.5; 14.175 };
60
{ 2019-03-14T00:00:00; 2019-03-28T00:00:00; 0.5; 16.2 };
61
{ 2019-06-14T00:00:00; 2019-06-28T00:00:00; 0.5; 18.225 };
62
{ 2019-09-16T00:00:00; 2019-09-30T00:00:00; 0.5; 20.25 };
63
{ 2019-12-16T00:00:00; 2020-01-02T00:00:00; 0.5; 22.275 };
64
{ 2020-03-16T00:00:00; 2020-03-30T00:00:00; 0.5; 24.3 }
65
]
66
67
(* underlyings values *)
68
asset fixing identified by fobservation {
69
fobservation : date;
70
bac : rational; (* Bank of America Corporation *)
71
sg : rational; (* Societe Generale *)
72
ubs : rational; (* Union des Banques Suisses *)
73
}
74
75
(* EXPECTED PAYMENT COMPUTATION *)
76
77
function compute_expected (d : date) : tez {
78
79
specification {
80
81
(** etrigger is defined as the set of early assets for which
82
the trigger condition is true *)
83
definition etrigger { e : early |
84
forall f in fixing,
85
if e.eobservation = f.fobservation
86
then (* trigger condition *)
87
f.bac >= e.trigger * bac_initial
88
and f.sg >= e.trigger * sg_initial
89
and f.ubs >= e.trigger * ubs_initial
90
else false
91
}
92
93
(** ibarrier is defined as the set of interest assets for which
94
the barrier condition is true *)
95
definition ibarrier { i : interest |
96
forall f in fixing,
97
(* retrieving the first element of etrigger *)
98
let some efirst = etrigger.nth(0) in
99
if i.iobservation = f.fobservation and i.iobservation <= efirst.eobservation
100
then (* barrier condition *)
101
f.bac >= bac_strike
102
and f.sg >= sg_strike
103
and f.ubs >= ubs_strike
104
else false
105
otherwise false
106
}
107
108
(* TODO finish specs *)
109
(** expected is the sum of redemption nominal and interests *)
110
postcondition p_expected {
111
let expected : tez =
112
let some ftrigger = etrigger.nth(0) in
113
(* early redemption *)
114
ftrigger.value * nominal
115
otherwise
116
(* redemption *)
117
let some f = fixing.get(gredemption) in
118
if f.bac >= bac_strike
119
and f.sg >= sg_strike
120
and f.ubs >= ubs_strike
121
then
122
nominal
123
else
124
let bac_trigger = f.bac / bac_strike in
125
let sg_trigger = f.sg / sg_strike in
126
let ubs_trigger = f.ubs / ubs_strike in
127
let worst = min ((min (bac_trigger, sg_trigger)), ubs_trigger) in
128
worst * nominal
129
otherwise true
130
in
131
(* interests *)
132
let interests =
133
let some lbarrier = ibarrier.last(0) in
134
let v = fixing.get(lbarrier.iobservation) in
135
if v.bac >= lbarrier.barrier * bac_initial
136
and v.sg >= lbarrier.barrier * sg_initial
137
and v.ubs >= lbarrier.barrier * ubs_initial
138
then lbarrier.rate * nominal
139
else 0tz
140
otherwise 0tz
141
in
142
result = expected + interests
143
}
144
}
145
146
effect {
147
let expected = 0tz in
148
let terminated = false in
149
let redeem_date = final in
150
(* early redemption *)
151
for : redeemloop e in early do
152
if e.redemption <= d
153
then (* is there early redemption ? *)
154
let v = fixing.get(e.eobservation) in
155
if v.bac >= e.trigger * bac_initial
156
and v.sg >= e.trigger * sg_initial
157
and v.ubs >= e.trigger * ubs_initial
158
then (
159
expected += e.value * nominal;
160
redeem_date := e.eobservation;
161
terminated := true
162
)
163
done;
164
(* redemption *)
165
if not terminated and gredemption <= d
166
then
167
let f = fixing.get(gredemption) in
168
if f.bac >= bac_strike
169
and f.sg >= sg_strike
170
and f.ubs >= ubs_strike
171
then
172
expected += nominal
173
else
174
let bac_trigger = f.bac / bac_strike in
175
let sg_trigger = f.sg / sg_strike in
176
let ubs_trigger = f.ubs / ubs_strike in
177
let worst = min ((min (bac_trigger, sg_trigger)), ubs_trigger) in
178
expected += worst * nominal;
179
(* expected interests *)
180
let exp_interests = 0.0 in
181
for : interestloop i in interest do
182
if i.iobservation <= redeem_date and i.payment <= d
183
then
184
let v = fixing.get(i.iobservation) in
185
if v.bac >= i.barrier * bac_initial
186
and v.sg >= i.barrier * sg_initial
187
and v.ubs >= i.barrier * ubs_initial
188
then exp_interests := i.rate * nominal
189
done;
190
expected += exp_interests;
191
return expected
192
}
193
}
194
195
(* PAYMENT action *)
196
variable actual_payment : tez = 0tz
197
198
action pay_note () {
199
called by issuer
200
effect {
201
actual_payment += transferred
202
}
203
}
204
205
action add_fixing (f[%signedby (oracle)%] : fixing) {
206
effect {
207
fixing.add(f)
208
}
209
}
210
211
(* STATE MACHINE *)
212
states =
213
| Created initial (** doc initial state. *)
214
| Canceled (** owner or issuer has canceled the transaction. *)
215
| Confirmed (** owner has confirmed. *)
216
| Defaulted
217
| Terminated
218
219
(** Used by owner to confirm transaction. It transfers the price of contract (nominal) *)
220
transition confirm () {
221
called by owner
222
from Created
223
to Confirmed when { transferred = nominal }
224
}
225
226
transition cancel () {
227
called by owner or issuer
228
from Created
229
to Canceled
230
}
231
232
transition check () {
233
called by owner
234
from Confirmed
235
to Defaulted when { actual_payment < compute_expected(now) }
236
}
237
238
transition terminate () {
239
called by issuer
240
from Confirmed
241
to Terminated when { actual_payment >= compute_expected(now) }
242
}
Copied!
The simulation sheet of this contract is available here.
This contract supposes that fixing values are public, which is an issue because banks usually have to pay Exchange institutions a licence to use them. One could easily imagine a contract crawler which would retrieve and consolidate all fixing data.
There are two solutions :
  • find a way to cipher fixing data
  • provide exchange institutions with a business model which does not rely on fixing data licensing
One could imagine for example that exchange institutions provide fixing data for free and provide SCAAS (smart contract as a service); typically this auto-callable note as a service to deploy on the blockchain.
Note that if underlying values were quoted on the blockchain itself, then the data could be natively public and available. The contract could then rely on calls to the exchange contract.
TODO :
  • Search for quotation contracts. Are existing market places a model of that?
  • Add formal properties :
    • Sum of payments are above a constant (here 0, that is proving that payments are positive)
    • Temporal consistency : adding a fixing at time t does not change the amount due at time before t
Last modified 1mo ago
Export as PDF
Copy link
Edit on GitHub