Skip to content

Instantly share code, notes, and snippets.

Last active May 1, 2024 14:54
Show Gist options
  • Save dgpv/514134c9727653b64d675d7513f983dd to your computer and use it in GitHub Desktop.
Save dgpv/514134c9727653b64d675d7513f983dd to your computer and use it in GitHub Desktop.
Alloy specification for simple vault covenant-enforced contract
// Author: Dmitry Petukhov
// License: CC BY-CA 4.0 (Creative Commons Attribution-ShareAlike 4.0)
// This specification models a simple vault that can be implemented
// on Bitcoin-like blockchains with minimal introspection capabilities
// This spec is written to be checked with Alloy (
// One such vault is described in
// This specification demonstrates that this particular vault can be simplified
// by not requiring additional covenant case for 'cancel' transaction,
// and that enforcing number of inputs and outputs is not required except in
// the 'complete withdrawal' case for number of outputs of the previous transaction
// We do not model time, and only deal with the structural model.
// This is possible because the timing properties of the contract
// is very simple: withdrawal completion is simply locked from being
// spendable immediately with relative timelock in the 'complete withdrawal'
// covenant case. We are interested in modelling relationships between
// transactions and their parts, therefore non-temoporal spec is sufficient
// First comes the generic spec to model transactions.
// By representing output scripts with a signature rather than
// an enum, we allow Alloy to generate different addresses
abstract sig Destination {} {
this in TxOutput.dst
sig SomeAddress extends Destination {} {}
// But there will only be one Covenant that we care about
one sig Covenant extends Destination {} {}
// We allow 'dangling' outputs - not attached to any transaction
// This is impossible in reality, but in this model, 'dangling'
// output just means that we do not care from which transaction it comes
sig TxOutput {
index: Int,
value: Int,
dst: Destination,
tx: lone Transaction // this can be empty when output is 'dangling'
} {
value > 0
index >= 0
one tx => this in tx.outputs
// If this is 'dangling' input, it has to be used somewhere as input
no tx => this in Transaction.inputs.prevout
// WitnessType is contract-specific, so it is described later
sig TxInput {
index: Int,
prevout: disj TxOutput,
wit: lone WitnessType,
tx: Transaction // no 'dangling' inputs
} {
index >= 0
this in tx.inputs
// We don't care about witnesses if there's no Covenant
one wit <=> prevout.dst = Covenant
// Inputs and outputs are marked as 'disjoint' to prevent different transactions
// from 'sharing' the same inputs/outputs
sig Transaction {
inputs: disj some TxInput,
outputs: disj some TxOutput,
fee: Int,
} {
fee > 0
// enforce that all indexes are unique and within range
all i: inputs | i.index < #inputs
all o: outputs | o.index < #outputs
#inputs.index = #inputs
#outputs.index = #outputs
// Prevent 'dangling' outputs from entering Transaction->TxOutput relation
all o: outputs | o.tx = this
// Maintain consistent values and fees
(sum i:inputs | i.prevout.value) = (sum o:outputs | o.value).plus[fee]
// Cycles are not possible in blockchain, but here we have to state it as a fact
fact no_cycles {
all t: Transaction | t not in t.^(inputs.prevout.tx)
// Below is the spec related to the contract itself
// We only use two type of witnesses - one enables triggering withdrawal
// or cancelling it, depending on the number of outputs in the transaction.
// The other enables withdrawal, given that the previous trigger transaction
// have exactly two outputs
// Any transaction enabled by trigger_or_cancel that do not have exactly
// two outputs is effectively a cancel transaction
enum WitnessType { trigger_or_cancel, complete_withdrawal }
// This predicate models the 'trigger or cancel' covenant case
// Its argument is TxInput rather than Transaction to model that
// covenant enables spending a particular input
pred trigger_or_cancel_cov [inp: TxInput] {
// This represents the need to enforce curent input index
// This is needed because with the basic introspection available
// using OP_CAT, it is very difficult to address arbitrary input or output
// selectivaly. The inputs and outputs are introspected via calculating
// hashes of concatenated data of all outputs, or all input values,
// all input scripts, etc. Therefore the simple way is to have
// introspected inputs/outputs be at the start of this hashed data chunks,
// and allow 'unrestricted' inputs or outputs to take the rest of these
// data chunks. This should also be true for other introspection mechanisms
// that rely on hashes of concatenated inputs/outputs
// Introspecting inputs/outputs in this way makes it disconnected from the
// index of the current input being spent, so we must explicitly enforce
// the input index to be the same as expected by the introspection machinery
inp.index = 0
// We work with inputs and outputs of the transaction independently
// of the current input, because of the reasoning explained above
one o: inp.tx.outputs | one i: inp.tx.inputs {
// The simple CAT vault enforces these by putting input/output data
// at the start of the respective buffers
o.index = 0
i.index = 0
// These are the main conditions that this covenant case is enforcing
o.value = i.prevout.value
o.dst = i.prevout.dst
// This predicate models the 'complete withdrawal' covenant case
// Its argument is TxInput rather than Transaction to model that
// covenant enables spending a particular input
// It is also modelled as for the covenant that does the
// introspection via hashes of concatenated inputs / outputs, so
// here we also model introspection of inputs and outputs as separate
// from the introspection of the index of the current input
pred complete_withdrawal_cov [inp: TxInput] {
inp.index = 0
one o: inp.tx.outputs | one i: inp.tx.inputs {
o.index = 0
i.index = 0
// This is the core condition that separates
// 'trigger withdrawal' from 'cancel' covenant cases
// If the current input spends an output from the transaction
// that has exactly two inputs, this is a 'trigger' case, and
// this covenant will allow to proceed with withdrawal
// In any other case, as the check for exactly two outputs
// will not pass, and the transaction cannot be used for withdrawal,
// making it effectively a 'cancel' transaction
#(i.prevout.tx.outputs) = 2
// These are conditions that allow the withdrawal, where the value is
// taken from the covenant-locked output, and the destination is taken
// from the adjacent output.
// Note that because there's no known ways to introspect contents
// of the previous transactions (even when there's rich introspection
// available for current transaction, like in Elements), this check
// will be done by calculating the hash of the previous transaction,
// and concatenated output data will be used for that. That means
// that the easiest way to 'address' this outputs is for them to
// be at the start of the concatenated outputs data chunk, at
// indexes 0 and 1
// Because of the first condition, it is required that covenant-locked
// output is always at index 0. Where covenant scripts are not
// enforcing it, the software should. For example, the transaction
// that sends the funds to the vault should not use output with index
// other than 0 for the envaulted funds
all po: i.prevout.tx.outputs {
po.index = 0 => po.value = o.value
po.index = 1 => po.dst = o.dst
// When there's special opcodes available to do introspection,
// like in Elements, covenant code can easily address specific
// inputs and outputs, and there are less reasons to use fixed
// indexes. The following two predicates model a possible two
// covenant that do the same as the ones described above,
// but with assumption that they are implemented using the
// 'rich introspection' opcodes like PUSHCURRENTINPUTINDEX,
pred trigger_or_cancel_cov_rich_introspection [i: TxInput] {
// The trigger case have to use fixed index here.
// This is because the withdrawal case will use fixed index 0
// for the output of the previous transaction that is expected
// to be covenant-locked. This covenant also enforces that
// input index is equal to the output index, so forcing
// input index to be 0 enforces output index to be 0, too,
// and that in turn is what is expected for correct function
// of the withdrawal case
i.index = 0
one o: i.tx.outputs {
// To preserve the covenant-locked value, the most straightforward
// way is to enforce that the output with the same index as the input
// has the same value and destination.
o.index = i.index
o.value = i.prevout.value
o.dst = i.prevout.dst
// In the withdrawal case with 'rich introspection' we don't actually
// need to fix the input index, because there's no next covenant
// that expects a certain index, and there's no disconnection between
// the current input and constructed input / output buffers to be used
// for introspection in the CAT-driven covenant
// It is a good idea to fix input index at 0, though, to prevent abuse of
// accidentally created transactions where funds are locked in the covenant
// at output index 0. Fixing input index will prevent having both inputs
// to the withdrawal transactions coming from the covenant. When both
// inputs come from the covenant when the input index is not fixed at 0,
// the value at input at index 1 may not be equivalent with the value
// at output index 1
pred complete_withdrawal_cov_rich_introspection [i: TxInput] {
one o: i.tx.outputs {
// Note that here, instead of enforcing output index to be
// equal to input index, it can also be enforced to be
// a fixed value like 0. But in that case, the 'contract_holds'
// predicate that is used to check for correctness of the contract,
// will need to be changed accordingly to always expect
// the withdrawal at output 0
o.index = i.index
// The conditions related to previous transaction are the same as for
// the CAT-driven covenant, because previous transaction introspection
// is done in the same manner, not via special opcodes
#(i.prevout.tx.outputs) = 2
all po: i.prevout.tx.outputs {
po.index = 0 => po.value = o.value
po.index = 1 => po.dst = o.dst
// This predicate models the fact that to spend a covenant-locked output,
// the input needs to have appropriate witness. The particular covenant
// that is modelled is expected to have only two cases.
pred covenant_enforced {
all i: TxInput {
i.prevout.dst = Covenant => {
one i.wit
i.wit = trigger_or_cancel => trigger_or_cancel_cov[i]
i.wit = complete_withdrawal => complete_withdrawal_cov[i]
// This predicate is the same as 'covenant_enforced', but it uses
// the 'rich introspection' variants for the covenant predicates
pred covenant_enforced_rich_introspection {
all i: TxInput {
i.prevout.dst = Covenant => {
one i.wit
i.wit = trigger_or_cancel => trigger_or_cancel_cov_rich_introspection[i]
i.wit = complete_withdrawal => complete_withdrawal_cov_rich_introspection[i]
// This predicate is used to check the correctness of the simple vault contract
pred contract_holds {
all i: TxInput | i.prevout.dst = Covenant => {
// If the covenant is unlocked using 'complete_withdrawal' witness,
// it will have an output with the same value as the input.
// While the 'complete withdrawal' covenant case itself enforces
// the output value to be equal to the value of output 0 of the
// previous transaction, the 'trigger' case is expected to enforce
// that the covenant-locked value will always be at output 0.
// By checking `o.value = i.prevout.value` we implicitly check this.
// Implicit check is better because we do not just copying the
// check from the covenant predicate, and so we are checking the
// 'meaning' of the conditions that it enforces, rather than
// just testing that the checks are indeed there.
// The withdrawal transaction can have more than one output,
// and outputs can have same value and destination, but we are only
// interested in one particular output relevant to our covenant.
// If we say that it is a required condition that our covenant expects
// to use the same indexes for input and output relevant to the covenant,
// using `o.index = i.index` here in the test predicate is fine, and
// there's no need to do it in a more roundabout way
i.wit = complete_withdrawal => {
one o: i.tx.outputs {
o.index = i.index
o.value = i.prevout.value
all po: i.prevout.tx.outputs {
// The previous transaction is expected to have
// exactly two outputs
po.index < 2
po.index = 0 => {
po.value = o.value
// while dst being the Covenant is not
// directly enforced by the 'complete_withdrawal'
// case, it is expected to be the Covenant because
// of the structure of the contract, and here we
// check this implicit assumption
po.dst = Covenant
// The second output of the previous transaction
// must supply the dst for this output
po.index = 1 => po.dst = o.dst
// We expect only one input to contain the trigger transaction
// Because the trigger covenant case fixes input and output
// indexes, only one trigger input should be possible.
// Also, the value is expected to be preserved
one pi: i.prevout.tx.inputs {
pi.wit = trigger_or_cancel
pi.prevout.dst = Covenant
pi.prevout.value = o.value
// If the covenant is unlocked using 'trigger_or_cancel' witness,
// the spent output is expected to be a covenant. Note that in
// general this is not the case, because there can be a script that
// allows spending with arbitrary witness, but in our model we
// only have one thing controlling the spending - the Covenant.
i.wit = trigger_or_cancel => {
i.prevout.dst = Covenant
// In the trigger_or_cancel case, one of the outputs is expected
// to have the same value as the input, and to also be locked
// with the Coveanant, as the spent output.
// And the way the inputs and outputs are matched is by the index,
// so the indexes expected to be equal
one o: i.tx.outputs {
o.index = i.index
o.value = i.prevout.value
o.dst = Covenant
// If the number of outputs of the current transaction
// is not 2, there should be no transactions that spend
// any of the outputs of the current transaction using the
// 'complete_withdrawal' case. Note that this is not true
// in general, because one output of the transaction can
// have a script that is different from Covenant, but
// still spendable with complete_withdrawal witness.
// We don't have scripts other than Covenant in our model,
// so we can ignore that possibility.
#i.tx.outputs != 2 => {
all wd_i: TxInput | wd_i.wit = complete_withdrawal => {
no wd_i.prevout & i.tx.outputs
// If output of such transaction is spent that has index equal
// to the current input, the spending input should also have
// 'trigger_or_cancel' witness, unless number of outputs of
// of current transaction is exactly 2, then it can be
// 'complete_withdrawal'
all ii: TxInput | ii.prevout in i.tx.outputs => {
ii.prevout.index = i.index => {
ii.wit = trigger_or_cancel
or (#i.tx.outputs = 2 and ii.wit = complete_withdrawal)
// The covenant-locked output at index 1, if there is only two outputs,
// can be spent using the complete_withdrawal case, but in an incorrect way:
// the value will be taken from the other output (at index 0), but the
// destination will be taken from the covenant-locked output. And what
// should be the 'withdrawal' output will lock some unrelated amount
// at the covenant, while the amount that was locked will be distributed
// between other outputs and transaction fee
// This situation is expected to be prevented by the software that
// implements the infrastructure for this contract. It should prevent
// creating transaction where funds are locked in covenant at output 1
// This predicate is a bit more general: it states that
// no trigger transactions with two outputs will have Covenant as
// destinations for both of the outputs. But it captures the situation
// that we want to exclude from the model, without dealing with indexes.
pred no_trigger_transactions_with_both_outputs_to_covenant {
all i: TxInput | i.wit = trigger_or_cancel and #i.tx.outputs = 2 => {
// The set of destinations must not equal a one-element set {Covenant}
i.tx.outputs.dst != Covenant
// For withdrawal, only contents of one output is enforced, and nothing
// prevents other outputs to have Covenant as destination. But this will
// clash with our contract_holds predicate, where if one withdrawal
// transaction has two outputs with output 1 to Covenant, but another
// withdrawal uses this output at index 1 for incorrect withdrawal,
// as described above. We basically are not interested in what happens
// with the outputs after withdrawal, so we use this predicate
// to exclude any transactions that would spend outputs of the
// withdrawal transaction
pred no_transactions_after_withdrawal {
all i: TxInput | i.wit = complete_withdrawal => {
no i.tx.outputs & Transaction.inputs.prevout
// We expect the software that implements the contract infrastructure
// to never send the funds to the vault using 2-output transaction, because
// it will immediately enable the withdrawal case, without preceeding
// trigger transaction
pred no_2output_envault {
all t: Transaction {
Covenant in t.outputs.dst and Covenant not in t.inputs.prevout.dst => {
#t.outputs != 2
// Some facts about the modelled system to reduce the state space
// We are not interested in the states where there's no covenant spending
fact some_contract_transactions {
some t: Transaction | Covenant in t.inputs.prevout.dst
// We are not interested in transactions that are not directly connected
// to the covenant
fact only_contract_related_transactions {
all t: Transaction | Covenant in t.inputs.prevout.dst + t.outputs.dst
// This is the main 'check' statement that can be used to check that the
// covenant actually ensures that the contract holds
check vault {
// Exclude states that should be prevented by software that
// creates the contract transactions
// Exclude non-interesting states to reduce state space
} => contract_holds
} for 8 // up to 8 instances of each object
// This check statement can be used to check the covenant with predicates
// that model covenant that use 'rich introspection' opcodes
check vault_with_rich_introspection {
} => contract_holds
} for 8
// The following example can be used just to generate different
// instances of the vault
run test_vault { covenant_enforced } for 8
// The following example can demonstrate an instance where
// withdrawal transaction has two covenant-locked inputs.
// This is possible if the 'complete withdraw' covenant case
// does not fix input index, and there is a transaction
// that has covenant-locked funds at output 1.
// Such transaction can be created accidentally or as a result
// of some software bug in the software that creates the
// contract transactions
run example_two_covenant_inputs_at_withdraw {
some t: Transaction | #{
i: t.inputs {
complete_withdrawal in i.wit
Covenant in i.prevout.dst
trigger_or_cancel in i.prevout.tx.inputs.wit
} = 2
} for 8
<?xml version="1.0"?>
<type name="complete_withdrawal"/>
<type name="Covenant"/>
<type name="Int"/>
<type name="SomeAddress"/>
<type name="String"/>
<type name="Transaction"/>
<type name="trigger_or_cancel"/>
<type name="univ"/>
<type name="ordering/Ord"/>
<type name="seq/Int"/>
<node shape="Ellipse" color="Blue">
<type name="TxInput"/>
<node shape="Inv Trapezoid" color="Green">
<type name="TxOutput"/>
<node visible="no">
<type name="Destination"/>
<type name="WitnessType"/>
<edge visible="no">
<relation name="tx"> <type name="TxInput"/> <type name="Transaction"/> </relation>
<edge visible="no" attribute="no">
<relation name="tx"> <type name="TxOutput"/> <type name="Transaction"/> </relation>
<edge visible="no" attribute="yes">
<relation name="dst"> <type name="TxOutput"/> <type name="Destination"/> </relation>
<relation name="fee"> <type name="Transaction"/> <type name="Int"/> </relation>
<relation name="index"> <type name="TxInput"/> <type name="Int"/> </relation>
<relation name="index"> <type name="TxOutput"/> <type name="Int"/> </relation>
<relation name="value"> <type name="TxOutput"/> <type name="Int"/> </relation>
<relation name="wit"> <type name="TxInput"/> <type name="WitnessType"/> </relation>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment