Fizzy
Real life insurance contract
The fizzy contract was an insurance against flight delay issued in 2018 by the Axa insurance company :
Below is the direct transcription of the fizzy contract in archetype.
fizzy.arl
1
archetype fizzy
2
3
variable creator : role = @tz1Lc2qBKEWCBeDU8npG6zCeCqpmaegRi6Jg
4
5
enum status =
6
| Created
7
| Before (* flight landed before the limit *)
8
| After (* flight landed after the limit *)
9
| Cancelled (* cancelled by the user *)
10
| FlightCancelled (* flight cancelled by the air company *)
11
| Redirected (* flight redirected *)
12
| Diverted (* flight diverted *)
13
14
asset insurance {
15
productid : string;
16
limit : date;
17
premium : tez;
18
indemnity : tez;
19
product : string;
20
stat : status = Created;
21
}
22
23
asset[@add creator (none)] flight identified by id {
24
id : string;
25
insurances : insurance partition;
26
}
27
28
action addflightinsurance (fi : string, i : insurance) {
29
called by creator
30
31
effect {
32
if (not flight.contains (fi)) then
33
flight.add({ id = fi; insurances = [] });
34
let f = flight.get(fi) in
35
f.insurances.add(i)
36
}
37
}
38
39
(* data should be signed by oracle ... *)
40
action updatestatus (fi : string, arrival : date) {
41
42
called by creator
43
44
effect {
45
let f = flight.get(fi) in
46
for i in f.insurances do
47
match i.stat with
48
| Created ->
49
if arrival > i.limit
50
then i.stat := After
51
| _ -> ()
52
end
53
done
54
}
55
}
56
57
action manual (fi : string, pr : string, newst : status) {
58
59
called by creator
60
61
effect {
62
let f = flight.get(fi) in
63
for i in f.insurances.select(product = pr) do
64
match i.stat with
65
| Created -> i.stat := newst
66
| _ -> ()
67
end
68
done
69
}
70
}
71
72
specification {
73
(* this contract does not transfer any tez *)
74
contract invariant s2 {
75
transfers_by_tx(anytx) = 0
76
}
77
}
78
79
security {
80
(* any action on storage is performed only by the owner *)
81
s1 : only_by_role (anyaction, creator);
82
83
(* transaction "updatestatus" is not the only one to potentially
84
perform an update of insurance status *)
85
s3 : only_in_action (update (insurance.stat), [updatestatus or manual]);
86
}
Copied!
Last modified 1mo ago
Export as PDF
Copy link
Edit on GitHub