Fizzy

fizzy.arl
archetype fizzy
​
variable creator : role = @tz1Lc2qBKEWCBeDU8npG6zCeCqpmaegRi6Jg
​
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;
  product   : string;
  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.stat with
         | Created -> i.stat := newst
         | _ -> ()
        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]);
}
​