Contract - CGP
Address:
ID:

SUMMARY
FULL NAMECommon Goods Pool
STATUSInactive
TRANSACTIONS0
LAST ACTIVATION BLOCK340,008
BALANCES
ASSETAMOUNT
3,620,920.00000001

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

module U32    = FStar.UInt32
module RT     = Zen.ResultT
module Dict   = Zen.Dictionary
module TX     = Zen.TxSkeleton
module CR     = Zen.ContractResult
module Asset  = Zen.Asset
module OptT   = Zen.OptionT
module Wallet = Zen.Wallet



let maxOutputs : nat = 100

let payoutBlock : nat = 100

let intervalLength : nat = 10000



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

// tries to map a function over a list.
// if all of the mappings return Some, then returns Some list.
// otherwise returns None.
val tryMap(#a #b: Type)(#n: nat):
    (a -> option b `cost` n)
    -> ls:list a
    -> option (ls':list b{length ls' == length ls}) `cost` (length ls * (n + 20) + 20)
let rec tryMap #a #b #n f ls = //20
    match ls with
    | hd::tl ->
        let! hd' = f hd in
        let! tl' = tryMap f tl in
        begin match hd', tl' with
        | Some hd', Some tl' ->
            let (result: list b{length result == length ls}) = hd'::tl' in
            OptT.some result
        | _ -> OptT.none end
    | [] -> [] |> OptT.incSome (length ls * (n + 20))

val tryFold (#a #b : Type) (#n : nat) :
    (b -> a -> option b `cost` n)
    -> b
    -> ls:list a
    -> option b `cost` (length ls * (n + 12) + 10)
let rec tryFold #a #b #n f x ls = // 10
    let open OptT in
    match ls with
    | [] ->
        incSome (length ls * (n + 12)) x
    | hd :: tl ->
        tryFold f x tl >>= (fun r -> f r hd) // (length ls * (n + 12))



(*
-------------------------------------------------------------------------------
========== 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 extractSpend :
    list data
    -> option spend `cost` 84
let extractSpend ls = // 17
    match ls with
    | asset' :: amount' :: [] ->
        let open OptT in
        let sAsset  = tryString asset'       in // 2
        let oAsset  = sAsset >>= Asset.parse in // 64
        let oAmount = tryU64 amount'         in // 2
        oAsset  >>= (fun asset  -> // 2
        oAmount >>= (fun amount -> // 3
            OptT.ret ({ asset=asset; amount=amount })
            ))
    | _ ->
        OptT.incNone 73

val trySpend :
    data
    -> option spend `cost` 91
let trySpend d = // 3
    let open OptT in
    tryList d >>= extractSpend

val extractOutput :
    list data
    -> option output `cost` 107
let extractOutput ls = // 9
    match ls with
    | lock' :: spend' :: [] ->
        let open OptT in
        let oLock  = tryLock lock'   in // 2
        let oSpend = trySpend spend' in // 91
        oLock  >>= (fun lock  -> // 2
        oSpend >>= (fun spend -> // 3
            OptT.ret ({ lock=lock; spend=spend })
            ))
    | _ ->
        OptT.incNone 98

val tryOutput :
    data
    -> option output `cost` 114
let tryOutput d = // 3
let open OptT in
    tryList d >>= extractOutput

val extractOutputList :
    ls:list data
    -> option (ls':list output { length ls' == length ls }) `cost` (length ls * 134 + 22)
let extractOutputList ls = // 2
    tryMap tryOutput ls

val toBounded :
    size:nat
    -> list data
    -> option (ls:list data { let len = length ls in 1 <= len && len <= size }) `cost` 11
let toBounded size ls = // 11
    if (let len = length ls in 1 <= len && len <= size)
        then OptT.ret (ls <: ls : list data { length ls <= size })
        else OptT.none

val extractOutputListBounded :
    size:nat
    -> ls:list data { let len = length ls in 1 <= len && len <= size }
    -> option (ls':list output { let len' = length ls' in 1 <= len' && len' <= size }) `cost` (size * 134 + 22 + 11)
let extractOutputListBounded size ls = // 11
    let open OptT in
    (extractOutputList ls 
gt; (fun ls' -> ls' <: ls':list output { let len' = length ls' in 1 <= len' && len' <= size })) |> inc ((size - length ls) * 134) val parseRawOutputs : option (Dict.t data) -> result (ls:list data) `cost` 83 let parseRawOutputs dict = // 4 parseField tryList "Outputs" "Couldn't parse Outputs" dict val parseOutputs : size:nat -> option (Dict.t data) -> result (ls:list output { let len = length ls in 1 <= len && len <= size }) `cost` (83 + 11 + (size * 134 + 22 + 11) + 15) let parseOutputs size dict = // 15 let open RT in ret dict >>= parseRawOutputs // 83 >>= (toBounded size >> ofOptionT "Outputs list size is out of bounds" ) // 11 >>= (extractOutputListBounded size >> ofOptionT "Invalid outputs structure") // (size * 134 + 22 + 11) (* ------------------------------------------------------------------------------- ========== PAYOUT ============================================================= ------------------------------------------------------------------------------- *) val lockOutput : contractId -> (w:wallet) -> txSkeleton -> output -> option txSkeleton `cost` (Wallet.size w * 128 + 192 + 64 + 19) let lockOutput contractId w txSkel outp = // 19 let asset = outp.spend.asset in let amount = outp.spend.amount in let open OptT in ret txSkel >>= TX.fromWallet asset amount contractId w // (Wallet.size w * 128 + 192) >>= (TX.lockToAddress asset amount outp.lock >> liftCost) // 64 val lockOutputs: contractId -> (w:wallet) -> txSkeleton -> (ls:list output) -> option txSkeleton `cost` (length ls * ((Wallet.size w * 128 + 192 + 64 + 19) + 12) + 10 + 5) let lockOutputs contractId w txSkel ls = // 5 tryFold (lockOutput contractId w) txSkel ls val lockOutputsBounded : size:nat -> contractId -> (w:wallet) -> txSkeleton -> (ls:list output { let len = length ls in 1 <= len && len <= size }) -> option txSkeleton `cost` (size * ((Wallet.size w * 128 + 192 + 64 + 19) + 12) + 10 + 5 + 23) let lockOutputsBounded size contractId w txSkel ls = // 23 let open OptT in lockOutputs contractId w txSkel ls |> inc ((size - length ls) * ((Wallet.size w * 128 + 192 + 64 + 19) + 12)) (* ------------------------------------------------------------------------------- ========== VALIDATION ========================================================= ------------------------------------------------------------------------------- *) val isPayoutBlock : context -> bool `cost` 9 let isPayoutBlock context = // 14 let r = context.blockNumber `U32.rem` (U32.uint_to_t intervalLength) in r `U32.eq` (U32.uint_to_t payoutBlock) |> ret val validateBlockNumber (#a:Type) : context -> a -> result a `cost` 16 let validateBlockNumber #_ context txSkel = // 7 let! b = isPayoutBlock context in // 9 if b then RT.ret txSkel else RT.failw "Not a payout block" (* ------------------------------------------------------------------------------- ========== MAIN =============================================================== ------------------------------------------------------------------------------- *) let main txSkel context contractId command sender messageBody w state = // 20 let open RT in ret messageBody >>= validateBlockNumber context // 16 >>= parseDict // 15 >>= parseOutputs maxOutputs // (83 + 11 + (maxOutputs * 134 + 22 + 11) + 15) >>= (lockOutputsBounded maxOutputs contractId w txSkel >> ofOptionT "Insufficient funds") // (maxOutputs * ((Wallet.size w * 128 + 192 + 64 + 19) + 12) + 10 + 5 + 23) >>= CR.ofTxSkel // 3 val cf: txSkel : txSkeleton -> context : context -> command : string -> sender : sender -> messageBody: option data -> w : wallet -> state : option data -> nat `cost` 43 let cf _ _ _ _ _ w _ = ((15 + (83 + 11 + (maxOutputs * 134 + 22 + 11) + 15) + (maxOutputs * ((Wallet.size w * 128 + 192 + 64 + 19) + 12) + 10 + 5 + 23) + 16 + 3 + 20) <: nat) |> ret