📖Metadata

It’s a best practice to document interfaces, modules, functions, table schemas, and other Pact code using the @doc metadata field. We’ll do that throughout our contract, beginning with the module itself.

The second metadata type is @model. It allows us to specify properties that functions must satisfy and invariants that table schemas must satisfy. Pact, via the Z3 theorem prover, can prove that there is no possible set of variable assignments in our code that will violate the given property or invariant. Or, if it does find a violation, it can tell us so we can fix it!

Properties (but not invariants) can be defined at the top level of the module so they can be reused in multiple functions.

We have a few functions that should never succeed unless they were called in a transaction signed by the nucredit-faucet faucet keyset. We can capture that property in a reusable definition. We’ll see examples of using this property within a function later on.

// pact
@model  [ (defproperty faucet-authorized (authorized-by "free.nucredit-faucet-faucet-keyset"))]