Contract - DEX-V2

Address:

czen1qqqqqqq8ptestf6xe72hysaew858j8j2naurpauqljw4cccsqhpfjyk2zcsnmrq85

ID:

00000000e15e60b4e8d9f2ae48772e3d0f23c953ef061ef01f93ab8c6200b853225942c4

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

module Arr = Zen.Array
module CR = Zen.ContractResult
module Dict = Zen.Dictionary
module Hash = Zen.Hash
module RT = Zen.ResultT
module TX = Zen.TxSkeleton
module U32 = FStar.UInt32
module U64 = FStar.UInt64
module W = Zen.Wallet

type order = {
    underlyingAsset: asset;
    underlyingAmount: U64.t; // amount of collateral for the order
    pairAsset: asset;
    orderTotal: U64.t; // the amount of the pair required to take the entire order
    makerPubKey: publicKey; // the public key of the order maker
}

// A double uint64, needed for multiplying two arbitrary uint64s without overflow
type d64 = { hi:U64.t; lo:U64.t }

// compressed public key
type cpk = byte ** hash

// compress a public key
val compress: publicKey -> cpk `cost` 305
let compress pk = let open FStar.UInt8 in // 13
    let parity = (Arr.item 32 pk %^ 2uy) +^ 2uy in
    let aux (i:nat{i < 32}): byte `cost` 5 = ret (Arr.item (31-i) pk) in
    let! x = Arr.init_pure 32 aux in // 292
    ret (parity, x)

// multiply two uint64s without overflow
// algorithm adapted from 'The Art of Computer Programming' by Donald E. Knuth
val dmul64: U64.t -> U64.t -> d64 `cost` 43
let dmul64 x y = let open U64 in // 39
    let m32 = 4294967296UL in // 2^32
    let xlo = x %^ m32 in // 32 low bits of x
    let xhi = x /^ m32 in // 32 high bits of x
    let ylo = y %^ m32 in // 32 low bits of y
    let yhi = y /^ m32 in // 32 high bits of y

    let t0 = xlo *%^ ylo in
    let t1 = (xhi *%^ ylo) +%^ (t0 /^ m32) in
    let t2 = (xlo *%^ yhi) +%^ (t1 %^ m32) in

    let hi = (xhi *%^ yhi) +%^ (t1 /^ m32) +%^ (t2 /^ m32) in
    let lo = ((t2 %^ m32) *%^ m32) +%^ (t0 %^ m32) in
    ret ({hi=hi; lo=lo})

val mkAsset: contractId -> hash -> asset `cost` 4
let mkAsset (version, contractHash) hash = // 4
    ret (version, contractHash, hash)

val hashAsset: asset -> hash `cost` 408
let hashAsset asset = // 4
    Hash.updateAsset asset Hash.empty // 384
    >>= Hash.finalize // 20

val hashU32: U32.t -> hash `cost` 48
let hashU32 x = // 4
    Hash.updateU32 x Hash.empty // 24
    >>= Hash.finalize // 20

val hashU64: U64.t -> hash `cost` 72
let hashU64 x = // 4
    Hash.updateU64 x Hash.empty // 48
    >>= Hash.finalize // 20

val updatePubKey': pk: list byte{length pk == 64} -> Zen.Hash.Sha3.t -> Zen.Hash.Sha3.t `cost` 648
let updatePubKey' pk s = // 4
    Zen.List.foldT (Zen.Base.flip Hash.updateByte) s pk // 64 * 10 + 4
    <: Zen.Hash.Sha3.t `cost` 644

val updatePubKey: publicKey -> Zen.Hash.Sha3.t -> Zen.Hash.Sha3.t `cost` 783
let updatePubKey pk s = // 5
    Zen.Array.toList pk // 130
    >>= Zen.Base.flip updatePubKey' s // 648

val hashPubKey: publicKey -> hash `cost` 807
let hashPubKey pk = // 4
    updatePubKey pk Hash.empty // 783
    >>= Hash.finalize // 20

val hashCPK: cpk -> hash `cost` 225
let hashCPK (parity, x) = // 7
    Hash.updateByte parity Hash.empty // 6
    >>= Hash.updateHash x // 192
    >>= Hash.finalize // 20

val hashOrder: order -> hash `cost` 2783
let hashOrder order = // 36
    let! underlyingAssetHash = hashAsset order.underlyingAsset in // 408
    let! underlyingAmountHash = hashU64 order.underlyingAmount in // 72
    let! pairAssetHash = hashAsset order.pairAsset in // 408
    let! orderTotalHash = hashU64 order.orderTotal in // 72
    let! makerPubKeyHash = hashPubKey order.makerPubKey in // 807
    Hash.updateHash underlyingAssetHash Hash.empty // 192
    >>= Hash.updateHash underlyingAmountHash // 192
    >>= Hash.updateHash pairAssetHash // 192
    >>= Hash.updateHash orderTotalHash // 192
    >>= Hash.updateHash makerPubKeyHash // 192
    >>= Hash.finalize // 20

val getAsset: option (Dict.t data) -> string -> option asset `cost` 137
let getAsset dict fieldName = // 7
    dict >!= Dict.tryFind fieldName // 64
         >?= tryString // 2
         >?= Zen.Asset.parse // 64

val getU32: option (Dict.t data) -> string -> option U32.t `cost` 80
let getU32 dict fieldName = // 14
    let! x = dict >!= Dict.tryFind fieldName // 64
                  >?= tryU32 in // 2
    ret ( if x <> Some 0ul then x else None )

val getU64: option (Dict.t data) -> string -> option U64.t `cost` 80
let getU64 dict fieldName = // 14
    let! x = dict >!= Dict.tryFind fieldName // 64
                  >?= tryU64 in // 2
    ret ( if x <> Some 0UL then x else None )

val getHash: option (Dict.t data) -> string -> option hash `cost` 71
let getHash dict fieldName = // 5
    dict >!= Dict.tryFind fieldName // 64
         >?= tryHash // 2

val getMakerPubKey: option (Dict.t data) -> option publicKey `cost` 71
let getMakerPubKey dict = // 5
    dict >!= Dict.tryFind "MakerPubKey" // 64
         >?= tryPublicKey // 2

val getReturnAddress: option (Dict.t data) -> option lock `cost` 71
let getReturnAddress dict = // 5
    dict >!= Dict.tryFind "returnAddress" // 64
                              >?= tryLock // 2

val getOrder: option (Dict.t data) -> result order `cost` 570
let getOrder dict = // 65
    let! underlyingAsset = getAsset dict "UnderlyingAsset" in // 137
    let! underlyingAmount = getU64 dict "UnderlyingAmount" in // 80
    let! pairAsset = getAsset dict "PairAsset"in // 137
    let! orderTotal = getU64 dict "OrderTotal" in // 80
    let! makerPubKey = getMakerPubKey dict in // 71
    match underlyingAsset, underlyingAmount, pairAsset, orderTotal, makerPubKey with
    | Some underlyingAsset, Some underlyingAmount,
      Some pairAsset, Some orderTotal, Some makerPubKey ->
        RT.ok ({ underlyingAsset=underlyingAsset;
                 underlyingAmount=underlyingAmount;
                 pairAsset=pairAsset;
                 orderTotal=orderTotal;
                 makerPubKey=makerPubKey; })
    | None, _, _, _, _ -> RT.autoFailw "Could not parse UnderlyingAsset"
    | _, None, _, _, _ -> RT.autoFailw "Could not parse UnderlyingAmount, or UnderlyingAmount was 0"
    | _, _, None, _, _ -> RT.autoFailw "Could not parse PairAsset"
    | _, _, _, None, _ -> RT.autoFailw "Could not parse OrderTotal, or OrderTotal was 0"
    | _, _, _, _, None -> RT.autoFailw "Could not parse MakerPubKey"

val getOrderAsset: contractId -> order -> asset `cost` 2792
let getOrderAsset contractID order = // 5
    let! orderHash = hashOrder order in // 2783
    mkAsset contractID orderHash // 4

val lockToPubKey: asset -> U64.t -> publicKey -> txSkeleton -> txSkeleton `cost` 604
let lockToPubKey asset amount pk tx = // 10
    let! cpk = compress pk in // 305
    let! cpkHash = hashCPK cpk in // 225
    TX.lockToPubKey asset amount cpkHash tx // 64

// mints an order asset and locks it to the contract, as well as the underlying
val createOrder: order -> contractId -> txSkeleton -> txSkeleton `cost` 3003
let createOrder order contractID tx = // 19
    let! orderAsset = getOrderAsset contractID order in // 2792
    TX.mint 1UL orderAsset tx // 64
    >>= TX.lockToContract orderAsset 1UL contractID // 64
    >>= TX.lockToContract order.underlyingAsset order.underlyingAmount contractID // 64

// destroys an order if it exists in the wallet,
// and adds the underlying to the inputs.
val destroyOrder:
    order
    -> contractId
    -> w: wallet
    -> txSkeleton
    -> CR.t `cost` (W.size w * 256 + 3267)
let destroyOrder order contractID w tx = // 24
    // the rewrites are not necessary, but vastly improve verification time
    begin
        let! orderAsset = getOrderAsset contractID order in // 2792
        begin
            begin
                // destroy the order
                begin TX.destroy 1UL orderAsset tx // 64
                      >>= TX.fromWallet orderAsset 1UL contractID w // W.size w * 128 + 192
                      <: option txSkeleton `cost` (W.size w * 128 + 256)
                end
                // add the underlying to the inputs
                >?= TX.fromWallet order.underlyingAsset order.underlyingAmount contractID w // W.size w * 128 + 192
                <: option txSkeleton `cost` (W.size w * 256 + 448)
            end
            >>= CR.ofOptionTxSkel "Could not find order in wallet. Ensure that both the order and the correct amount of the underlying are present." // 3
            <: CR.t `cost` (W.size w * 256 + 451)
        end
    end <: CR.t `cost` (W.size w * 256 + 3243)

//////////////////
// Making an order
//////////////////

val makeTx: txSkeleton -> contractId -> publicKey -> order -> CR.t `cost` 3097
let makeTx tx contractID senderPubKey order = // 27
    let! underlyingReceived = TX.getAvailableTokens order.underlyingAsset tx in // 64
    let! tx = // issue a token with the hash of the order as the subidentifier,
              // and lock it to the contract, with the underlying
              createOrder order contractID tx // 3003
              >>= CR.ofTxSkel in // 3
    match underlyingReceived = order.underlyingAmount, senderPubKey = order.makerPubKey with
    | true, true -> ret tx
    | false, _ -> RT.failw "Incorrect amount of UnderlyingAsset Received"
    | _, false -> RT.failw "SenderPubKey must match MakerPubKey"

val make: txSkeleton -> contractId -> sender -> option data -> CR.t `cost` 3684
let make tx contractID sender messageBody = // 13
    match sender with
    | PK senderPubKey ->
        let! dict = messageBody >!= tryDict in // 4
        getOrder dict // 570
        `RT.bind`
        makeTx tx contractID senderPubKey // 3097
    | _ -> RT.autoFailw "Must authenticate with PubKey"

//////////////////
// Cancel an order
//////////////////

val cancelTx:
    txSkeleton
    -> contractId
    -> w: wallet
    -> publicKey
    -> order
    -> CR.t `cost` (W.size w * 256 + 3889)
let cancelTx tx contractID w senderPubKey order = // 18
    if senderPubKey = order.makerPubKey
    then // lock the underlying to the maker's pk
         lockToPubKey order.underlyingAsset order.underlyingAmount order.makerPubKey tx // 604
         // destroy the order
         >>= destroyOrder order contractID w // W.size w * 256 + 3267
         <: CR.t `cost` (W.size w * 256 + 3871)
    else RT.autoFailw "SenderPubKey must match MakerPubKey"

val cancel:
    txSkeleton
    -> contractId
    -> sender
    -> option data
    -> w: wallet
    -> CR.t `cost` (W.size w * 256 + 4477)
let cancel tx contractID sender messageBody w = // 14
    match sender with
    | PK senderPubKey ->
        let! dict = messageBody >!= tryDict in // 4
        begin let order = getOrder dict in // 570
        order `RT.bind` cancelTx tx contractID w senderPubKey // W.size w * 256 + 3889
        end <: CR.t `cost` (W.size w * 256 + 4459)
    | _ ->
        RT.autoFailw "Sender must authenticate with public key"

//////////////////
// Taking an order
//////////////////

// check that the requestedPayout is ok
val checkRequestedPayout:
    order
    -> requestedPayout: U64.t
    -> paymentAmount: U64.t
    -> bool `cost` 171
let checkRequestedPayout { underlyingAmount=ua; orderTotal=ot} rp pa = // 85
    // we want to check that
    // 1) requestedPayout <= underlyingAmount
    // 2) paymentAmount <= orderTotal
    // 3) requestedPayout = floor (underlyingAmount * (paymentAmount / orderTotal))

    // note that 3) is equivalent to
    // underlyingAmount * paymentAmount
    // < requestedPayout * orderTotal + orderTotal
    // <= underlyingAmount * paymentAmount + orderTotal

    let open U64 in
    // maximum 64 bit unsigned integer
    let max64 = 0UL -%^ 1UL in

    // compute underlyingAmount * paymentAmount
    let! ua_pa = dmul64 ua pa in // 43
    // compute requestedPayout * orderTotal
    let! rp_ot = dmul64 rp ot in // 43
    // compute requestedPayout * orderTotal + orderTotal
    let rp_ot_ot = { hi = if rp_ot.lo >^ max64 -%^ ot // will adding low 64 bits overflow
                          then rp_ot.hi +%^ 1UL // this never overflows
                          else rp_ot.hi;
                     lo = rp_ot.lo +%^ ot } in
    // compute underlyingAmount * paymentAmount + orderTotal
    let ua_pa_ot = { hi = if ua_pa.lo >^ max64 -%^ ot // will adding low 64 bits overflow
                          then ua_pa.hi +%^ 1UL // this never overflows
                          else ua_pa.hi;
                     lo = ua_pa.lo +%^ ot } in

    // underlyingAmount * paymentAmount < requestedPayout * orderTotal + orderTotal
    let ua_pa_lt_rp_ot_ot = (ua_pa.hi <^ rp_ot_ot.hi)
                         || (ua_pa.hi = rp_ot_ot.hi && ua_pa.lo <^ rp_ot_ot.lo) in
    // requestedPayout * orderTotal + orderTotal <= underlyingAmount * paymentAmount + orderTotal
    let rp_ot_ot_lte_ua_pa_ot = (rp_ot_ot.hi <^ ua_pa_ot.hi)
                             || (rp_ot_ot.hi = ua_pa_ot.hi && rp_ot_ot.lo <=^ ua_pa_ot.lo) in
    // all 3 inequality relations must hold
    ret (rp <=^ ua && pa <=^ ot && ua_pa_lt_rp_ot_ot && rp_ot_ot_lte_ua_pa_ot)

// updates an order in the case of a partial fill
val updateOrder:
    contractId
    -> order
    -> U64.t
    -> U64.t
    -> txSkeleton
    -> txSkeleton `cost` 3020
let updateOrder contractID order paymentAmount payoutAmount tx = let open U64 in // 17
    if paymentAmount <^ order.orderTotal // partial fill, so need to update the order
    then // create the new order
        let newOrder = { order with
                         underlyingAmount=order.underlyingAmount-%^payoutAmount;
                         orderTotal=order.orderTotal-%^paymentAmount } in
        createOrder newOrder contractID tx // 3003
    else incRet 3003 tx

val takeTx:
    txSkeleton
    -> contractId
    -> w: wallet
    -> U64.t
    -> U64.t
    -> order
    -> lock
    -> CR.t `cost` (W.size w * 256 + 6978)
let takeTx tx contractID w paymentAmount payoutAmount order returnAddress = // 23
    //  lock the payout to the taker
    TX.lockToAddress order.underlyingAsset payoutAmount returnAddress tx // 64
    // lock the paymentAmount to the maker
    >>= lockToPubKey order.pairAsset paymentAmount order.makerPubKey // 604
    //  create a new order if partial fill, locking the remainder of the underlying to the contract
    >>= updateOrder contractID order paymentAmount payoutAmount // 3020
    // add inputs from wallet, destroying the order
    >>= destroyOrder order contractID w // W.size w * 256 + 3267

val take':
    txSkeleton
    -> contractId
    -> w: wallet
    -> U64.t
    -> U64.t
    -> lock
    -> order
    -> CR.t `cost` (W.size w * 256 + 7164)
let take' tx contractID w requestedPayout providedAmount returnAddress order = // 15
    begin
    let! paymentAmountOK = checkRequestedPayout order requestedPayout providedAmount in // 171
    if paymentAmountOK then
        takeTx tx contractID w providedAmount requestedPayout order returnAddress // W.size w * 256 + 6978
    else
        RT.incFailw (W.size w * 256 + 6978) "Incorrect requestedPayout"
    end <: CR.t `cost` (W.size w * 256 + 7149)

val take:
    txSkeleton
    -> contractId
    -> option data
    -> w: wallet
    -> CR.t `cost` (W.size w * 256 + 8011)
let take tx contractID messageBody w = // 42
    let! dict = messageBody >!= tryDict in // 4
    let! requestedPayout = getU64 dict "RequestedPayout" in // 80
    let! returnAddress = getReturnAddress dict in // 71
    let! providedAmount = getU64 dict "ProvidedAmount" in // 80
    match requestedPayout, providedAmount, returnAddress with
    | Some requestedPayout, Some providedAmount, Some returnAddress ->
        let order = getOrder dict in // 570
        order `RT.bind` take' tx contractID w requestedPayout providedAmount returnAddress // W.size w * 256 + 7164
        <: CR.t `cost` (W.size w * 256 + 7734)
    | None, _, _ ->
        RT.autoFailw "Could not parse RequestedPayout, or RequestedPayout was 0"
    | _, None, _ ->
        RT.autoFailw "Could not parse ProvidedAmount, or ProvidedAmount was 0"
    | _, _, None ->
        RT.autoFailw "Could not parse returnAddress"

//////////
// exports
//////////

val main:
    txSkeleton
    -> context
    -> contractId
    -> command: string
    -> sender
    -> option data
    -> w: wallet
    -> option data
    -> CR.t `cost` ( 9 + begin match command with
                         | "Make" -> 3684
                         | "Cancel" -> W.size w * 256 + 4477
                         | "Take" -> W.size w * 256 + 8011
                         | _ -> 0 end )
let main tx _ contractID command sender messageBody w _ = // 9
    begin
    match command with
    | "Make" ->
        make tx contractID sender messageBody // 3684
        <: CR.t `cost` begin match command with
                       | "Make" -> 3684
                       | "Cancel" -> W.size w * 256 + 4477
                       | "Take" -> W.size w * 256 + 8011
                       | _ -> 0 end
    | "Cancel" ->
        cancel tx contractID sender messageBody w // W.size w * 256 + 4477
    | "Take" ->
        take tx contractID messageBody w // W.size w * 256 + 8011
    | _ ->
        RT.failw "Unrecognised command"
    end <: CR.t `cost` begin match command with
                       | "Make" -> 3684
                       | "Cancel" -> W.size w * 256 + 4477
                       | "Take" -> W.size w * 256 + 8011
                       | _ -> 0 end

val cf:
    txSkeleton
    -> context
    -> string
    -> sender
    -> option data
    -> wallet
    -> option data
    -> nat `cost` 12
let cf _ _ command _ _ w _ = // 12
    ret ( 9 + begin match command with
              | "Make" -> 3684
              | "Cancel" -> W.size w * 256 + 4477
              | "Take" -> W.size w * 256 + 8011
              | _ -> 0 end )