Alloy specification for simple vault covenant-enforced contract

simple_vault.als

// Author: Dmitry Petukhov https://github.com/dgpv
// 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 (https://alloytools.org/) 

// One such vault is described in https://delvingbitcoin.org/t/basic-vault-prototype-using-op-cat/576/15
// 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,
// INSPECTINPUTVALUE, etc.

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 {
    {
        covenant_enforced

	// Exclude states that should be prevented by software that
	// creates the contract transactions
	
        no_2output_envault
        no_trigger_transactions_with_both_outputs_to_covenant

	// Exclude non-interesting states to reduce state space

	no_transactions_after_withdrawal

    } => 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 {
    {
        covenant_enforced_rich_introspection

        no_2output_envault
        no_trigger_transactions_with_both_outputs_to_covenant
        no_transactions_after_withdrawal
    } => 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 {
    covenant_enforced_rich_introspection
    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

simple_vault.thm

<?xml version="1.0"?>
<alloy>

<view>

<defaultnode/>

<defaultedge/>

<node>
   <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>

<node shape="Ellipse" color="Blue">
   <type name="TxInput"/>
</node>

<node shape="Inv Trapezoid" color="Green">
   <type name="TxOutput"/>
</node>

<node visible="no">
   <type name="Destination"/>
   <type name="WitnessType"/>
</node>

<edge visible="no">
   <relation name="tx"> <type name="TxInput"/> <type name="Transaction"/> </relation>
</edge>

<edge visible="no" attribute="no">
   <relation name="tx"> <type name="TxOutput"/> <type name="Transaction"/> </relation>
</edge>

<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>
</edge>

</view>

</alloy>