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
archetype fizzy
variable creator : role = @tz1fake
enum status =
| Created
| Before (* flight landed before the limit *)
| After (* flight landed after the limit *)
| Cancelled (* cancelled by the user *)
| FlightCancelled (* flight cancelled by the air company *)
| Redirected (* flight redirected *)
| Diverted (* flight diverted *)
asset insurance {
productid : string;
limit : date;
premium : tez;
indemnity : tez;
stat : status = Created;
}
asset[@add creator (none)] flight identified by id {
id : string;
insurances : insurance partition;
}
action addflightinsurance (fi : string, i : insurance) {
called by creator
effect {
if (not flight.contains (fi)) then
flight.add({ id = fi; insurances = [] });
let f = flight.get(fi) in
f.insurances.add(i)
}
}
(* data should be signed by oracle ... *)
action updatestatus (fi : string, arrival : date) {
called by creator
effect {
let f = flight.get(fi) in
for i in f.insurances do
match i.stat with
| Created ->
if arrival > i.limit
then i.stat := After
| _ -> ()
end
done
}
}
action manual (fi : string, pr : string, newst : status) {
called by creator
effect {
let f = flight.get(fi) in
for i in f.insurances.select(product = pr) do
match i.status with
| Created -> i.status := newst
| _ -> none
end
done
}
}
specification {
(* this contract does not transfer any tez *)
contract invariant s2 {
transfers_by_tx(anytx) = 0
}
}
security {
(* any action on storage is performed only by the owner *)
s1 : only_by_role (anyaction, creator);
(* transaction "updatestatus" is not the only one to potentially
perform an update of insurance status *)
s3 : only_in_action (update (insurance.stat), [updatestatus or manual]);
}