Contract - DEX-V2
Address:
ID:

SUMMARY
FULL NAMEDEX
STATUSInactive
TRANSACTIONS0
LAST ACTIVATION BLOCK583,659
BALANCES
ASSETAMOUNT
521.98838185
48.5877236
19.9999974
6.10023968
6
5.10419092
4
2.44551391
2
1.11696505
0.41248299
0.2469148
0.15
0.1
0.04445247
0.0067711
0.0000001
0.00000006
0.00000003
0.00000002
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001
0.00000001

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 )