Fizzy

The fizzy contract was an insurance against flight delay issued in 2018 by the Axa insurance company :
the insurance contract (in french).
the ethereum smart contract​
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!

Contract library - Previous

Insurance

Health care

Last modified 1mo ago

Export as PDF

Copy link

Edit on GitHub