(defun set-request-limit:string (account:string new-limit:decimal)
@doc “Set a new per-request limit for requesting funds from the faucet.”(defun get-limits:object (account:string)
@doc “Read the limits for your account and see how much KDA you can request.”
(with-read accounts account {
“account-limit” := account-limit
, “request-limit” := request-limit
, “funds-requested” := requested
, “funds-returned” := returned
} {
“account-limit”: account-limit
, “request-limit”: request-limit
, “account-limit-remaining”:
(- account-limit (- requested returned))
}
))(defun return-funds:string (account:string amount:decimal)
@doc “Return funds to the faucet (returned funds credit against your limits).”
@model
[ (property (> amount 0.0))
(property (= amount (column-delta accounts “funds-returned”)))
]
(enforce (> amount 0.0) “Amount must be greater than 0.0”)
(with-read accounts account {
“funds-requested” := requested
, “funds-returned” := returned
}
(let ((balance (- requested returned ))
(new-returned (+ returned amount )) )
We didn’t implement a property for this because our table invariants already verify that the funds returned can never exceed the funds requested. You can verify that removing this enforcement check will make the model checker yell at us.
(enforce (<= amount balance)
(format “{} exceeds the amount this account can return to the faucet, which is {}.”
[ amount balance ]))
Next, we transfer from the user account to the faucet account. To transfer funds from the user to the faucet account the user must have signed the transaction and scoped their signature to the (coin.TRANSFER) capability. For examples, please see the faucet.repl file and the return-funds.yaml request file.
(coin.transfer account FAUCET_ACCOUNT amount)
(update accounts account { “funds-returned”: new-returned }))))
)
Initialization
At this point we’ve established our smart contract: we entered a namespace, defined a keyset, and implemented a module. Now it’s time to initialize data.
For a typical smart contract, that simply means creating any tables we defined in the contract. However, more complex contracts may perform other steps, such as calling functions from the module.
Tables are defined in modules, but they are created after them. This ensures that the module can be redefined (ie. upgraded) later without necessarily having to re-create the table.
Speaking of: it’s a common practice to implement the initialization step as an ‘if’ statement that differentiates between an initial deployment and an upgrade. As with our keyset definition at the beginning of the contract, this can be done by sending an “upgrade” field with a boolean value as part of the transaction data
(if (read-msg “upgrade”)
“Upgrade complete”
(create-table free.goliath-faucet.accounts))
We have completed writing a faucet contract that can be deployed on devnet. The next steps will be running a devnet on your local machine, and running the faucet application that calls the functions from the contract.
You can start by following the instructions here: https://github.com/thomashoneyman/real-world-pact/tree/main/02-goliath-wallet
The Kadena.js team hopes that this step-by-step guide was practical and helpful.
Make sure you follow us on our social accounts for more exciting developer updates to come!
