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 = @tz1bfVgcJC4ukaQSHUe1EbrUd5SekXeP9CWk
4
constant owner : role = @tz1Lc2qBKEWCBeDU8npG6zCeCqpmaegRi6Jg
5
constant oracle : role = @tz1iawHeddgggn6P5r5jtq2wDRqcJVksGVSa (* 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 key_efirst = etrigger.nth(0) in
99
let some efirst = etrigger[key_efirst] in
100
if i.iobservation = f.fobservation and i.iobservation <= efirst.eobservation
101
then (* barrier condition *)
102
f.bac >= bac_strike
103
and f.sg >= sg_strike
104
and f.ubs >= ubs_strike
105
else false
106
otherwise false
107
otherwise false
108
}
109
110
(* TODO finish specs *)
111
(** expected is the sum of redemption nominal and interests *)
112
postcondition p_expected {
113
let expected : tez =
114
let some ftrigger_key = etrigger.nth(0) in
115
let some ftrigger = early[ftrigger_key] in
116
(* early redemption *)
117
ftrigger.value * nominal
118
otherwise
119
(* redemption *)
120
(let some f = fixing[gredemption] in
121
if f.bac >= bac_strike
122
and f.sg >= sg_strike
123
and f.ubs >= ubs_strike
124
then
125
nominal
126
else
127
let bac_trigger = f.bac / bac_strike in
128
let sg_trigger = f.sg / sg_strike in
129
let ubs_trigger = f.ubs / ubs_strike in
130
let worst = min ((min (bac_trigger, sg_trigger)), ubs_trigger) in
131
worst * nominal
132
otherwise 0tz)
133
134
otherwise
135
(* redemption *)
136
let some f = fixing[gredemption] in
137
if f.bac >= bac_strike
138
and f.sg >= sg_strike
139
and f.ubs >= ubs_strike
140
then
141
nominal
142
else
143
let bac_trigger = f.bac / bac_strike in
144
let sg_trigger = f.sg / sg_strike in
145
let ubs_trigger = f.ubs / ubs_strike in
146
let worst = min ((min (bac_trigger, sg_trigger)), ubs_trigger) in
147
worst * nominal
148
otherwise 0tz
149
in
150
(* interests *)
151
let interests =
152
if expected = 0tz then 0tz else
153
(let some lbarrier_key = ibarrier.nth(abs(ibarrier.count() - 1)) in
154
let some lbarrier = interest[lbarrier_key] in
155
let some v = fixing[lbarrier.iobservation] in
156
if v.bac >= lbarrier.barrier * bac_initial
157
and v.sg >= lbarrier.barrier * sg_initial
158
and v.ubs >= lbarrier.barrier * ubs_initial
159
then lbarrier.rate * nominal
160
else 0tz
161
otherwise 0tz
162
otherwise 0tz
163
otherwise 0tz)
164
in
165
result = expected + interests
166
}
167
}
168
169
effect {
170
var expected = 0tz;
171
var terminated = false;
172
var redeem_date = final;
173
(* early redemption *)
174
for : redeemloop e in early do
175
if early[e].redemption <= d
176
then ( (* is there early redemption ? *)
177
var ee = early[e].eobservation;
178
if fixing[ee].bac >= early[e].trigger * bac_initial
179
and fixing[ee].sg >= early[e].trigger * sg_initial
180
and fixing[ee].ubs >= early[e].trigger * ubs_initial
181
then (
182
expected += early[e].value * nominal;
183
redeem_date := early[e].eobservation;
184
terminated := true
185
))
186
done;
187
(* redemption *)
188
if not terminated and gredemption <= d
189
then
190
if fixing[gredemption].bac >= bac_strike
191
and fixing[gredemption].sg >= sg_strike
192
and fixing[gredemption].ubs >= ubs_strike
193
then
194
expected += nominal
195
else (
196
var bac_trigger = fixing[gredemption].bac / bac_strike;
197
var sg_trigger = fixing[gredemption].sg / sg_strike;
198
var ubs_trigger = fixing[gredemption].ubs / ubs_strike;
199
var worst = min ((min (bac_trigger, sg_trigger)), ubs_trigger);
200
expected += worst * nominal
201
);
202
(* expected interests *)
203
var exp_interests = 0tz;
204
for : interestloop i in interest do
205
if interest[i].iobservation <= redeem_date and interest[i].payment <= d
206
then (
207
var ii = interest[i].iobservation;
208
if fixing[ii].bac >= interest[i].barrier * bac_initial
209
and fixing[ii].sg >= interest[i].barrier * sg_initial
210
and fixing[ii].ubs >= interest[i].barrier * ubs_initial
211
then exp_interests := interest[i].rate * nominal
212
)
213
done;
214
expected += exp_interests;
215
return expected
216
}
217
}
218
219
(* PAYMENT action *)
220
variable actual_payment : tez = 0tz
221
222
entry pay_note () {
223
called by issuer
224
effect {
225
actual_payment += transferred
226
}
227
}
228
229
entry add_fixing (ffobservation : date, fbac : rational, fsg : rational, fubs : rational) {
230
effect {
231
fixing.add({ffobservation; fbac; fsg; fubs})
232
}
233
}
234
235
(* STATE MACHINE *)
236
states =
237
| Created initial (** doc initial state. *)
238
| Canceled (** owner or issuer has canceled the transaction. *)
239
| Confirmed (** owner has confirmed. *)
240
| Defaulted
241
| Terminated
242
243
(** Used by owner to confirm transaction. It transfers the price of contract (nominal) *)
244
transition confirm () {
245
called by owner
246
from Created
247
to Confirmed when { transferred = nominal }
248
}
249
250
transition cancel () {
251
called by owner or issuer
252
from Created
253
to Canceled
254
}
255
256
transition check () {
257
called by owner
258
from Confirmed
259
to Defaulted when { actual_payment < compute_expected(now) }
260
}
261
262
transition terminate () {
263
called by issuer
264
from Confirmed
265
to Terminated when { actual_payment >= compute_expected(now) }
266
}
267
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 1yr ago
Export as PDF
Copy link