Contract - FPC
Address:
ID:

SUMMARY
FULL NAMEFixed Payout Contract
STATUSInactive
TRANSACTIONS0
LAST ACTIVATION BLOCK420,525
BALANCES
ASSETAMOUNT
11.00000102

open Zen.Base
open Zen.Cost
open Zen.Types
open Zen.Data

module U8     = FStar.UInt8
module U64    = FStar.UInt64
module RT     = Zen.ResultT
module Dict   = Zen.Dictionary
module Sha3   = Zen.Sha3
module TX     = Zen.TxSkeleton
module CR     = Zen.ContractResult
module Asset  = Zen.Asset
module Opt    = Zen.Option
module OptT   = Zen.OptionT
module Array  = Zen.Array
module Str    = FStar.String
module CId    = Zen.ContractId
module Merkle = Zen.MerkleTree
module W      = Zen.Wallet
module PK     = Zen.PublicKey



let auditPathMaxLength : nat = 30

type parser (a:Type) (m:nat) =
    option (Dict.t data) -> result a `cost` m

type hashUpdate (a:Type) (m:nat) =
    a -> Sha3.t -> Sha3.t `cost` m

type ticker =
    s:string { Str.length s <= 273 }

type preAuditPath =
    p: list data { length p <= auditPathMaxLength }

type auditPath =
    p: list hash { length p <= auditPathMaxLength }

type commit = {
    c_root      : hash;
    c_timestamp : timestamp;
}

type attestation = {
    commit : commit;
    pubKey : publicKey;
}

type position =
    | Bull
    | Bear

type betEvent = {
    oraclePubKey     : publicKey;
    oracleContractId : contractId;
    ticker           : ticker;
    price            : U64.t;
    start            : U64.t;
    expiry           : option U64.t;
    collateral       : asset;
}

type bet = {
    bevent   : betEvent;
    position : position;
}

type proof = {
    key         : ticker;
    value       : U64.t;
    root        : hash;
    auditPath   : auditPath;
    index       : U64.t;
}

type redemption = {
    bet         : bet;
    attestation : attestation;
    timestamp   : timestamp;
    proof       : proof;
}



(*
-------------------------------------------------------------------------------
========== UTILITY FUNCTIONS ==================================================
-------------------------------------------------------------------------------
*)

let runOpt (#a #s:Type) (#m:nat) (update:a -> s -> s `cost` m) (x:option a) (st:s) : s `cost` (m + 5) =
    Opt.maybe (incRet m) update x st

val lockToSender: asset -> U64.t -> sender -> txSkeleton -> result txSkeleton `cost` 624
let lockToSender asset amount sender txSkel = // 14
    match sender with
    | PK pk ->
        ret txSkel
        >>= TX.lockToPublicKey asset amount pk // 610
        >>= RT.ok
    | Contract cid ->
        ret txSkel
        >>= TX.lockToContract asset amount cid // 64
        >>= RT.incOK 546
    | Anonymous ->
        RT.incFailw 610 "Sender can't be anonymous"



(*
-------------------------------------------------------------------------------
========== DATA PARSING =======================================================
-------------------------------------------------------------------------------
*)

val parseDict: option data -> result (option (Dict.t data)) `cost` 15
let parseDict data = // 11
    match data with
    | Some data ->
        data
        |> tryDict // 4
        |> RT.ofOptionT "Data parsing failed - the message body isn't a dictionary"
        |> RT.map Some
    | None ->
        RT.incFailw 4 "Data parsing failed - the message body is empty"

val parseField (#a:Type) (#m:nat)
    : (data -> option a `cost` m)
    -> fieldName:string
    -> errMsg:string
    -> option (Dict.t data)
    -> result a `cost` (m + 75)
let parseField #_ #_ parser fieldName errMsg dict = // 11
    let! value = dict >!= Dict.tryFind fieldName >?= parser in // (m + 64)
    match value with
    | Some value ->
        RT.ok value
    | None ->
        RT.failw errMsg

val parseOptField (#a:Type) (#m:nat)
    : (data -> option a `cost` m)
    -> fieldName:string
    -> option (Dict.t data)
    -> result (option a) `cost` (m + 71)
let parseOptField #_ #_ parser fieldName dict = // 7
    dict
    >!= Dict.tryFind fieldName // 64
    >?= parser // m
    >>= RT.ok

val parseTicker: string -> string -> option (Dict.t data) -> result ticker `cost` 90
let parseTicker fieldName errMsg dict = // 6
    let open RT in
    parseField tryString fieldName errMsg dict >>= // 77
    begin fun s -> // 7
        if Str.length s <= 273
            then RT.ok (s <: ticker)
            else RT.failw "Ticker size can't be bigger than 4"
    end

val extractHashes: string -> ls:list data -> result (ls':list hash { length ls' == length ls }) `cost` (length ls * (2 + 20) + 20 + 5)
let extractHashes errMsg ls = // 5
    OptT.tryMapT tryHash ls // (length ls * 22 + 20)
    |> RT.ofOptionT errMsg

val extractAuditPath': ls:preAuditPath -> result auditPath `cost` (length ls * 22 + 29)
let extractAuditPath' ls = // 4
    let open RT in
    extractHashes "All the items in the audit path must be hashes" ls // = X * 22 + 25
    
gt; (fun xs -> let (xs:list hash { length xs <= auditPathMaxLength }) = xs in xs) val extractAuditPath: ls:preAuditPath -> result auditPath `cost` (auditPathMaxLength * 22 + 40) let extractAuditPath (ls:preAuditPath) = extractAuditPath' ls |> inc ((auditPathMaxLength - length ls) * 22) |> (fun x -> x <: result auditPath `cost` (auditPathMaxLength * 22 + 29)) val parsePreAuditPath: string -> string -> option (Dict.t data) -> result preAuditPath `cost` 92 let parsePreAuditPath fieldName errMsg dict = // 6 let open RT in parseField tryList fieldName errMsg dict >>= // 79 begin fun ls -> // 7 if length ls <= auditPathMaxLength then RT.ok (ls <: preAuditPath) else RT.failw "AuditPath length must be 256" end val parseAuditPath: string -> string -> option (Dict.t data) -> result auditPath `cost` (auditPathMaxLength * 22 + 139) let parseAuditPath fieldName errMsg dict = // 7 let open RT in ret dict >>= parsePreAuditPath fieldName errMsg // 92 >>= extractAuditPath // (length ls * 22 + 25 + (auditPathMaxLength - length ls) * 22 + 12) val parsePosition: string -> string -> option (Dict.t data) -> result position `cost` 87 let parsePosition fieldName errMsg dict = // 6 let open RT in parseField tryString fieldName errMsg dict >>= // 77 begin fun s -> match s with // 4 | "Bull" -> ret Bull | "Bear" -> ret Bear | _ -> RT.failw "Position must be either Bull or Bear" end val parseContractId: string -> string -> option (Dict.t data) -> result contractId `cost` 158 let parseContractId fieldName errMsg dict = // 6 let open RT in parseField tryString fieldName errMsg dict >>= // 77 begin fun s -> // 11 if Str.length s = 72 then let (s:string { Str.length s = 72 }) = s in s |> CId.parse // 64 |> RT.ofOptionT "The given OracleContractId is not a valid contractId" else RT.incFailw 64 "OracleContractId must be 72 characters long" end val parseAsset: string -> string -> option (Dict.t data) -> result asset `cost` 150 let parseAsset fieldName errMsg dict = // 5 let open RT in parseField tryString fieldName errMsg dict >>= // 73 begin Asset.parse // 64 >> RT.ofOptionT "The given asset is not a valid asset" end val getTimestamp : parser U64.t 82 val getRoot : parser hash 82 val getOraclePubKey : parser publicKey 82 val getTicker : parser ticker 94 val getPrice : parser U64.t 82 val getStart : parser U64.t 82 val getExpiry : parser (option U64.t) 77 val getAuditPath : parser auditPath (auditPathMaxLength * 22 + 139 + 4) val getValue : parser U64.t 82 val getIndex : parser U64.t 82 val getPosition : parser position 91 val getOracleContractId : parser contractId 162 val getCollateral : parser asset 154 let getTimestamp dict = dict |> parseField tryU64 "Timestamp" "Could not parse Timestamp" let getRoot dict = dict |> parseField tryHash "Root" "Could not parse Root" let getOraclePubKey dict = dict |> parseField tryPublicKey "OraclePubKey" "Could not parse OraclePubKey" let getTicker dict = dict |> parseTicker "Ticker" "Could not parse Ticker" let getPrice dict = dict |> parseField tryU64 "Price" "Could not parse Price" let getStart dict = dict |> parseField tryU64 "Start" "Could not parse Start" let getExpiry dict = dict |> parseOptField tryU64 "Expiry" let getAuditPath dict = dict |> parseAuditPath "AuditPath" "Could not parse AuditPath" let getValue dict = dict |> parseField tryU64 "Value" "Could not parse Value" let getIndex dict = dict |> parseField tryU64 "Index" "Could not parse Index" let getPosition dict = dict |> parsePosition "Position" "Could not parse Position" let getOracleContractId dict = dict |> parseContractId "OracleContractId" "Could not parse OracleContractId" let getCollateral dict = dict |> parseAsset "Collateral" "Could not parse Collateral" val parseProof': option (Dict.t data) -> result proof `cost` (94 + (auditPathMaxLength * 22 + 415)) let parseProof' dict = // 31 let open RT in dict |> getTicker >>= (fun key -> // 94 dict |> getValue >>= (fun value -> // 82 dict |> getRoot >>= (fun root -> // 82 dict |> getAuditPath >>= (fun auditPath -> // auditPathMaxLength * 22 + 139 + 4 dict |> getIndex >>= (fun index -> // 82 RT.ok ({ key = key; value = value; root = root; auditPath = auditPath; index = index; })))))) val parseProof: option (Dict.t data) -> result proof `cost` (auditPathMaxLength * 22 + 512) let parseProof dict = parseProof' dict |> (fun x -> x <: result proof `cost` (auditPathMaxLength * 22 + 509)) val parseCommit: option (Dict.t data) -> result commit `cost` 175 let parseCommit dict = // 11 let open RT in dict |> getRoot >>= (fun root -> // 82 dict |> getTimestamp >>= (fun timestamp -> // 82 RT.ok ({ c_root = root; c_timestamp = timestamp; }))) val parseAttestation: option (Dict.t data) -> result attestation `cost` 268 let parseAttestation dict = // 11 let open RT in dict |> parseCommit >>= (fun commit -> // 175 dict |> getOraclePubKey >>= (fun pubKey -> // 82 RT.ok ({ commit = commit; pubKey = pubKey; }))) val parseEvent: option (Dict.t data) -> result betEvent `cost` 769 let parseEvent dict = // 36 let open RT in dict |> getOraclePubKey >>= (fun oraclePubKey -> // 82 dict |> getOracleContractId >>= (fun oracleContractId -> // 162 dict |> getTicker >>= (fun ticker -> // 94 dict |> getPrice >>= (fun price -> // 82 dict |> getStart >>= (fun start -> // 82 dict |> getExpiry >>= (fun expiry -> // 77 dict |> getCollateral >>= (fun collateral -> // 154 RT.ok ({ oraclePubKey = oraclePubKey; oracleContractId = oracleContractId; ticker = ticker; price = price ; start = start; expiry = expiry; collateral = collateral; })))))))) val parseRedemption': option (Dict.t data) -> result redemption `cost` (1051 + (auditPathMaxLength * 22 + 698)) let parseRedemption' dict = // 22 let open RT in dict |> parseEvent >>= (fun bevent -> // 769 dict |> getPosition >>= (fun position -> // 91 dict |> parseAttestation >>= (fun attestation -> // 262 dict |> getTimestamp >>= (fun timestamp -> // 82 dict |> parseProof >>= (fun proof -> // (auditPathMaxLength * 22 + 512) RT.ok ({ bet = { bevent = bevent; position = position; }; attestation = attestation; timestamp = timestamp; proof = proof; })))))) val parseRedemption: option (Dict.t data) -> result redemption `cost` (auditPathMaxLength * 22 + 1752) let parseRedemption dict = // 3 parseRedemption' dict |> (fun x -> x <: result redemption `cost` (auditPathMaxLength * 22 + 1749)) (* ------------------------------------------------------------------------------- ========== TOKENIZATION ======================================================= ------------------------------------------------------------------------------- *) val updatePublicKey : hashUpdate publicKey 517 let updatePublicKey pk s = // 7 let! cpk = PK.compress pk in // 305 ret s >>= Sha3.updateCPK cpk // 205 // Sha3.updateString with a constant cost val updateTicker : hashUpdate ticker 1650 let updateTicker tick s = // 12 ret s >>= Sha3.updateString tick // (6 * Str.length tick) >>= incRet (6 * (273 - Str.length tick)) val updateEvent : hashUpdate betEvent 2953 let updateEvent bevent s = // 30 ret s >>= updatePublicKey bevent.oraclePubKey // 517 >>= Sha3.updateContractId bevent.oracleContractId // 223 >>= updateTicker bevent.ticker // 1650 >>= Sha3.updateU64 bevent.price // 48 >>= Sha3.updateU64 bevent.start // 48 >>= Sha3.updateU64 `runOpt` bevent.expiry // 53 >>= Sha3.updateAsset bevent.collateral // 384 val updatePosition : hashUpdate position 28 let updatePosition position s = // 4 match position with | Bull -> Sha3.updateString "Bull" s // 24 | Bear -> Sha3.updateString "Bear" s // 24 val hashCommit : commit -> hash `cost` 271 let hashCommit commit = // 11 ret Sha3.empty >>= Sha3.updateHash commit.c_root // 192 >>= Sha3.updateU64 commit.c_timestamp // 48 >>= Sha3.finalize // 20 val hashCommitment : attestation -> hash `cost` 1014 let hashCommitment attestation = // 14 let! commitHash = hashCommit attestation.commit in // 271 ret Sha3.empty >>= Sha3.updateHash commitHash // 192 >>= updatePublicKey attestation.pubKey // 517 >>= Sha3.finalize // 20 val hashAttestation : attestation -> hash `cost` 1235 let hashAttestation attestation = // 9 let! commit = hashCommitment attestation in // 1014 ret Sha3.empty >>= Sha3.updateHash commit // 192 >>= Sha3.finalize // 20 val hashBet : bet -> hash `cost` 3012 let hashBet bet = // 11 ret Sha3.empty >>= updateEvent bet.bevent // 2953 >>= updatePosition bet.position // 28 >>= Sha3.finalize // 20 val mkBetToken : contractId -> bet -> asset `cost` 3019 let mkBetToken (v, h) bet = // 7 let! betHash = hashBet bet in ret (v, h, betHash) val mkAttestToken : contractId -> attestation -> asset `cost` 1242 let mkAttestToken (v,h) attestation = // 7 let! attestHash = hashAttestation attestation in // 1235 ret (v, h, attestHash) (* ------------------------------------------------------------------------------- ========== VALIDATION ========================================================= ------------------------------------------------------------------------------- *) val inBounds : U64.t -> option U64.t -> U64.t -> bool `cost` 10 let inBounds low high value = (low `U64.lte` value && Opt.maybe true (U64.lte value) high) |> ret val validateTime: redemption -> result redemption `cost` 24 let validateTime redemption = // 14 let bevent = redemption.bet.bevent in let low = bevent.start in let high = bevent.expiry in let value = redemption.timestamp in let! inb = inBounds low high value in // 10 if inb then RT.ok redemption else RT.failw "Attestation time is not within the given time bounds" val validatePrice: redemption -> result redemption `cost` 17 let validatePrice redemption = // 17 let bevent = redemption.bet.bevent in let price = bevent.price in let value = redemption.proof.value in let pos = redemption.bet.position in match price `U64.lte` value, pos with | true , Bull | false, Bear -> RT.ok redemption | _ -> RT.failw "Position doesn't match the event" val hashLeaf : key:ticker -> U64.t -> hash `cost` 1725 let hashLeaf (key : ticker) (value : U64.t) = // 19 ret Sha3.empty >>= Sha3.updateString key // 6 * 273 >>= Sha3.updateU64 value // 48 >>= Sha3.finalize // 20 |> inc (1638 - 6 * Str.length key) |> (fun x -> x <: hash `cost` 1706) val verifyAuditPath' : proof:proof -> bool `cost` (1754 + (length proof.auditPath * 420 + (auditPathMaxLength * 420 - length proof.auditPath * 420))) let verifyAuditPath' proof = // 25 let! leaf = hashLeaf proof.key proof.value in // 1725 Merkle.verify proof.root proof.auditPath (U64.v proof.index) leaf // (length proof.auditPath * 420 + 4) |> inc (auditPathMaxLength * 420 - length proof.auditPath * 420) val verifyAuditPath : proof:proof -> bool `cost` (auditPathMaxLength * 420 + 1757) let verifyAuditPath proof = // 3 verifyAuditPath' proof |> (fun x -> x <: bool `cost` (auditPathMaxLength * 420 + 1754)) val validateAuditPath: redemption -> result redemption `cost` (auditPathMaxLength * 420 + 1765) let validateAuditPath redemption = // 8 let! b = verifyAuditPath redemption.proof in // (auditPathMaxLength * 420 + 1757) if b then RT.ok redemption else RT.failw "Invalid audit path" val validateRedemption: redemption -> result redemption `cost` (auditPathMaxLength * 420 + 1813) let validateRedemption redemption = // 7 let open RT in ret redemption >>= validateTime // 24 >>= validatePrice // 17 >>= validateAuditPath // (auditPathMaxLength * 420 + 1765) (* ------------------------------------------------------------------------------- ========== COMMAND: Issue ==================================================== ------------------------------------------------------------------------------- *) val issueEvent: txSkeleton -> contractId -> sender -> betEvent -> CR.t `cost` 7597 let issueEvent txSkel contractId sender bevent = // 52 let! bullToken = mkBetToken contractId ({ bevent=bevent; position=Bull }) in // 3019 let! bearToken = mkBetToken contractId ({ bevent=bevent; position=Bear }) in // 3019 let! m = TX.getAvailableTokens bevent.collateral txSkel in // 64 let open RT in ret txSkel >>= (TX.safeMint m bullToken >> ofOptionT "No collateral provided") // 64 >>= (TX.safeMint m bearToken >> ofOptionT "No collateral provided") // 64 >>= lockToSender bullToken m sender // 624 >>= lockToSender bearToken m sender // 624 >>= (TX.lockToContract bevent.collateral m contractId >> liftCost) // 64 >>= CR.ofTxSkel // 3 val issue: txSkeleton -> contractId -> sender -> option data -> CR.t `cost` 8391 let issue txSkel contractId sender dict = // 10 let open RT in ret dict >>= parseDict // 15 >>= parseEvent // 769 >>= issueEvent txSkel contractId sender // 7597 (* ------------------------------------------------------------------------------- ========== COMMAND: Redeem ==================================================== ------------------------------------------------------------------------------- *) val redeemRedemption' : (w:wallet) -> txSkeleton -> contractId -> sender -> redemption -> CR.t `cost` (W.size w * 256 + 5526) let redeemRedemption' w txSkel contractId sender redemption = // 62 let! betToken = mkBetToken contractId redemption.bet in // 3019 let oracleContractId = redemption.bet.bevent.oracleContractId in let attestation = redemption.attestation in let! attestToken = mkAttestToken oracleContractId attestation in // 1242 let! m = TX.getAvailableTokens betToken txSkel in // 64 let open RT in ret txSkel >>= (liftCost << TX.destroy m betToken) // 64 >>= (ofOptionT "Insufficient funds" << TX.fromWallet redemption.bet.bevent.collateral m contractId w) // W.size w * 128 + 192 >>= lockToSender redemption.bet.bevent.collateral m sender // 624 >>= (ofOptionT "Attestation token not found" << TX.fromWallet attestToken 1UL contractId w) // W.size wallet * 128 + 192 >>= (liftCost << TX.lockToContract attestToken 1UL contractId) // 64 >>= CR.ofTxSkel // 3 val redeemRedemption: (w:wallet) -> txSkeleton -> contractId -> sender -> redemption -> CR.t `cost` (W.size w * 256 + 5531) let redeemRedemption w txSkel contractId sender redemption = // 5 redeemRedemption' w txSkel contractId sender redemption // auditPathMaxLength * 442 + Zen.Wallet.size w * 256 + 5526 val redeem' : (w:wallet) -> txSkeleton -> contractId -> sender -> option data -> CR.t `cost` (auditPathMaxLength * 442 + W.size w * 256 + 9124) let redeem' w txSkel contractId sender dict = // 13 let open RT in ret dict >>= parseDict // 15 >>= parseRedemption // (auditPathMaxLength * 22 + 1752) >>= validateRedemption // (auditPathMaxLength * 420 + 1813) >>= redeemRedemption w txSkel contractId sender // (W.size w * 256 + 5531) val redeem: (w:wallet) -> txSkeleton -> contractId -> sender -> option data -> CR.t `cost` (auditPathMaxLength * 442 + W.size w * 256 + 9129) let redeem w txSkel contractId sender dict = // 5 redeem' w txSkel contractId sender dict (* ------------------------------------------------------------------------------- ========== COMMAND: Cancel ==================================================== ------------------------------------------------------------------------------- *) val cancelEqualTokens : contractId -> (w : wallet) -> sender -> U64.t -> asset -> asset -> txSkeleton -> betEvent -> txSkeleton `RT.t` (0 + (W.size w * 128 + 192) + 624 + 64 + 64 + 29) let cancelEqualTokens contractId w sender m bullToken bearToken txSkel bevent = // 29 let open RT in ret txSkel >>= (ofOptionT "Insufficient funds" << TX.fromWallet bevent.collateral m contractId w) // W.size w * 128 + 192 >>= lockToSender bevent.collateral m sender // 624 >>= (liftCost << TX.destroy m bullToken) // 64 >>= (liftCost << TX.destroy m bearToken) // 64 val cancelEvent': (w : wallet) -> contractId -> sender -> txSkeleton -> betEvent -> CR.t `cost` (W.size w * 128 + 7179) let cancelEvent' w contractId sender txSkel bevent = // 37 let! bullToken = mkBetToken contractId ({ bevent=bevent; position=Bull }) in // 3019 let! bearToken = mkBetToken contractId ({ bevent=bevent; position=Bear }) in // 3019 let! mBull = TX.getAvailableTokens bullToken txSkel in // 64 let! mBear = TX.getAvailableTokens bearToken txSkel in // 64 let open RT in begin if U64.eq mBull mBear then cancelEqualTokens contractId w sender mBull bullToken bearToken txSkel bevent // (W.size w * 128 + 978) |> (fun x -> x <: txSkeleton `RT.t` (W.size w * 128 + 973)) else "There must be an equal amount of both bull and bear tokens in the transaction" |> incFailw (W.size w * 128 + 973) end >>= CR.ofTxSkel // 3 val cancelEvent: (w : wallet) -> contractId -> sender -> txSkeleton -> betEvent -> CR.t `cost` (W.size w * 128 + 7184) let cancelEvent w contractId sender txSkel bevent = // 5 cancelEvent' w contractId sender txSkel bevent val cancel' : (w : wallet) -> contractId -> sender -> txSkeleton -> option data -> CR.t `cost` (W.size w * 128 + 7979) let cancel' w contractId sender txSkel dict = // 11 let open RT in ret dict >>= parseDict // 15 >>= parseEvent // 769 >>= cancelEvent w contractId sender txSkel // (W.size w * 128 + 7184) val cancel : (w : wallet) -> contractId -> sender -> txSkeleton -> option data -> CR.t `cost` (W.size w * 128 + 7984) let cancel w contractId sender txSkel dict = // 5 cancel' w contractId sender txSkel dict (* ------------------------------------------------------------------------------- ========== MAIN =============================================================== ------------------------------------------------------------------------------- *) val main: txSkel : txSkeleton -> context : context -> contractId : contractId -> command : string -> sender : sender -> messageBody : option data -> w : wallet -> state : option data -> CR.t `cost` ( match command with | "Issue" -> 8391 + 9 | "Redeem" -> auditPathMaxLength * 442 + W.size w * 256 + 9129 + 9 | "Cancel" -> W.size w * 128 + 7984 + 9 | _ -> 9) let main txSkel context contractId command sender messageBody w state = // 9 match command with | "Issue" -> issue txSkel contractId sender messageBody // 8391 <: CR.t `cost` ( match command with | "Issue" -> 8391 | "Redeem" -> auditPathMaxLength * 442 + W.size w * 256 + 9129 | "Cancel" -> W.size w * 128 + 7984 | _ -> 0) | "Redeem" -> redeem w txSkel contractId sender messageBody // auditPathMaxLength * 442 + W.size w * 256 + 9129 | "Cancel" -> cancel w contractId sender txSkel messageBody // W.size w * 128 + 7984 | _ -> RT.failw "Unsupported command" val cf: txSkel : txSkeleton -> context : context -> command : string -> sender : sender -> messageBody: option data -> w : wallet -> state : option data -> nat `cost` 17 let cf _ _ command _ _ w _ = (( match command with | "Issue" -> 8391 + 9 | "Redeem" -> auditPathMaxLength * 442 + W.size w * 256 + 9129 + 9 | "Cancel" -> W.size w * 128 + 7984 + 9 | _ -> 9 ) <: nat) |> ret