Writing Specifications: Multisignature Wallet

This chapter demonstrates how to write formal specifications for the Multisignature Wallet contract using Ursus's specification DSL.

Overview

Specifications in Ursus describe what a function should do, not how it does it. They consist of:

Preconditions - What must be true before execution
Postconditions - What must be true after execution
State changes - How the contract state is modified
Error conditions - When the function should fail

Specification DSL

Ursus provides a domain-specific language for writing specifications:

Core Constructs

execs0 (function args) : ledger1 -> ledger2 - Function execution transforms ledger state
evals (function args) : ledger -> value - Function evaluation produces a value
no_err (function args) ledger - Function does not raise an error
err0 (function args) ledger - Function raises an error
con (condition) - Assert a condition holds
hyp (condition) - Assume a hypothesis
set (name := expression) - Define a local binding
msg_transfer queue - Specify outgoing message

Ledger Projections

Specifications can project specific fields from the ledger:

execs0 (function args) :
    ledger1 | "field1" "field2"  (* only these fields from ledger1 *)
 -> ledger2 | "field3"           (* only this field from ledger2 *)

This indicates that the function only reads field1 and field2 from the initial state, and only modifies field3.

Contract Invariants

Global Invariants

These properties should hold for all contract states:

Custodian Count Invariant

(* The number of custodians matches the size of m_custodians mapping *)
Invariant custodian_count_valid (l: LedgerLRecord) :=
  m_custodianCount = length(keys(m_custodians)).

Request Mask Invariant

(* Each custodian's pending transaction count is accurate *)
Invariant request_mask_valid (l: LedgerLRecord) :=
  forall (i: uint8),
    i < m_custodianCount ->
    _getMaskValue(m_requestsMask, i) =
      count_pending_transactions_for_custodian(i).

Confirmation Threshold Invariant

(* Required confirmations is between 1 and custodian count *)
Invariant confirmation_threshold_valid (l: LedgerLRecord) :=
  1 <= m_defaultRequiredConfirmations <= m_custodianCount.

Transaction Consistency Invariant

(* All pending transactions have valid confirmation state *)
Invariant transaction_valid (l: LedgerLRecord) :=
  forall (id: uint64) (txn: Transaction),
    m_transactions[id] = Some txn ->
    txn.signsReceived < txn.signsRequired /\
    txn.signsReceived = popcount(txn.confirmationsMask) /\
    txn.index < m_custodianCount.

Function Specifications

Helper Functions

_generateId

Purpose: Generate unique transaction ID from timestamp and logical time

Specification:

Definition _generateId_spec (l: LedgerLRecord) : Prop :=
  evals (_generateId rec def) : l -> v_id.
  con (v_id = (block_timestamp << 32) | (tx_logicaltime & 0xFFFFFFFF)).

Properties:

Pure function (no state changes)
Deterministic (same inputs → same output)
Unique (timestamp + logical time combination)

Ursus Implementation:

#[no_body]
#[proof = view]
Ursus Definition _generateId : UExpression (uint64) false.
return  \\ ((uint64(block->timestamp) << {32}) .|
            (tx->logicaltime & {0xFFFFFFFF})) \\ .
Defined.

_getSendFlags

Purpose: Determine message flags based on allBalance parameter

Specification:

Definition _getSendFlags_spec (allBalance: bool) (l: LedgerLRecord) : Prop :=
  evals (_getSendFlags rec def allBalance) : l -> v_flags.
  con (allBalance = true -> v_flags = FLAG_SEND_ALL_REMAINING).
  con (allBalance = false -> v_flags = FLAG_PAY_FWD_FEE_FROM_BALANCE).

Properties:

Pure function
Two cases: send all or pay from balance
No state dependencies

Ursus Implementation:

#[pure, private, returns=result_]
#[proof = pure]
Ursus Definition _getSendFlags (allBalance : bool): UExpression (uint8) false.
{
    ::// var00 flags: uint8 := FLAG_PAY_FWD_FEE_FROM_BALANCE ;_|.
    ::// if (allBalance) then { ->> } .
    {
        ::// flags := FLAG_SEND_ALL_REMAINING |.
    }
    ::// result_ := flags |.
}
return .
Defined.

_findCustodian

Purpose: Verify sender is a custodian and return their index

Specification:

Definition _findCustodian_spec (senderKey: uint256) (l: LedgerLRecord) : Prop :=
  (* Success case *)
  (m_custodians[senderKey] = Some index ->
   evals (_findCustodian rec def senderKey) : l -> index.
   no_err (_findCustodian rec def senderKey) l)
  \/
  (* Error case *)
  (m_custodians[senderKey] = None ->
   err0 (_findCustodian rec def senderKey) l | "m_custodians".
   con (error_code = 100)).

Properties:

View function (reads state, no modifications)
Fails with error 100 if sender not a custodian
Returns custodian index on success

Ursus Implementation:

#[view, private, returns=result_]
#[proof = view]
Ursus Definition _findCustodian (senderKey : uint256): UExpression (uint8) true.
{
    ::// var00 __index__: optional ( uint8 ) := m_custodians->fetch(senderKey) ;_|.
    ::// require_(__index__->hasValue(), #{(IntError 100)}).
    ::// result_ := __index__->get() |.
}
return .
Defined.

Main Functions

submitTransaction - Error Case

Purpose: Specify when submitTransaction should fail

Specification:

Definition MUL1_TRI_def (ll: LedgerLRecord rec)
                        (dest : address) (value__ : uint128)
                        (cc : mapping(uint32)(varUint32)) (bounce : bool)
                        (allBalance : bool) (payload : TvmCell): Prop.
err0 (submitTransaction rec def dest value__ cc bounce allBalance payload) ll
    | "msg_pubkey" "m_custodians" "m_ownerKey" "_min_value".
execs0 (_removeExpiredTransactions rec def ) : ll  -> l2 | "m_requestsMask".
set (index := m_custodians[msg_pubkey]? ).

set (req1 := isSome index).
set (req2 := xIntGeb value__ _min_value).
set (getMaskValue_p1 := xIntBitOpRight m_requestsMask
                         (xIntMult (8:uint256) (uint2N (unMaybe index)))).
set (getMaskValue_ := xIntBitOpAnd getMaskValue_p1 0xFF).
set (req3 := Common.ltb (uint2N getMaskValue_: uint8) MAX_QUEUED_REQUESTS_constant).
con (negb (req1 && req2 && req3)).
Defined.

Explanation:

Function raises an error
After cleaning expired transactions
Error occurs when ANY of these fails:
- req1: Sender is not a custodian
- req2: Value is below minimum
- req3: Custodian has too many pending transactions

Error Codes:

100: Not a custodian (req1 fails)
107: Value too low (req2 fails)
113: Too many requests (req3 fails)

submitTransaction - Fast Path (M=1)

Purpose: Specify immediate execution when only 1 confirmation needed

Specification:

Definition MUL1_TRO_def (ll: LedgerLRecord rec)
                        (dest : address) (value__ : uint128)
                        (cc : mapping(uint32)(varUint32)) (bounce : bool)
                        (allBalance : bool) (payload : TvmCell): Prop.
execs0 (submitTransaction rec def dest value__ cc bounce allBalance payload) :
       ll | "block_timestamp" "m_defaultRequiredConfirmations" "_address"
    -> l1 | "m_defaultRequiredConfirmations" "#msgs#IDefault".
no_err (submitTransaction rec def dest value__ cc bounce allBalance payload) l0.
execs0 (_removeExpiredTransactions rec def ) : ll  -> l2.
set (l2_accepted := exec_state (Uinterpreter tvm_accept) l2).
evals (_getSendFlags rec def allBalance) : l2_accepted -> v_f.

hyp (eqb m_defaultRequiredConfirmations 1 = true).
msg_transfer 0 IDefaultQueue.

split. con false. (*internal*)
split. con dest. (* dest *)
split. con block_timestamp. (* time *)
split. con payload. (* body *)
split. con default. (* stateInit *)
split. con (uint2N (toValue v_f)). (* flags *)
split. con default. (* callback *)
split. con default. (* sig *)
split. con default. (* expire *)
split. con default. (* pubkey *)
split. con default. (* onErrorId *)
split. con default. (* signBox *)
split. con _address. (* sender *)
split. con value__. (* value *)
split. con bounce. (* bounce *)
con cc.
Defined.

Explanation:

No error occurs
Hypothesis: m_defaultRequiredConfirmations = 1
After cleanup and accept
Evaluate send flags
Send message immediately with:
- Destination: dest
- Value: value__
- Payload: payload
- Flags: computed from allBalance
- Bounce: bounce
- CC tokens: cc
No transaction stored (returns 0)

submitTransaction - Queue Path (M>1)

Purpose: Specify transaction creation when multiple confirmations needed

Specification:

Definition MUL21_TRO_def (ll: LedgerLRecord rec)
                        (dest : address) (value__ : uint128)
                        (cc : mapping(uint32)(varUint32)) (bounce : bool)
                        (allBalance : bool) (payload : TvmCell): Prop.
execs0 (submitTransaction rec def dest value__ cc bounce allBalance payload) :
       ll | "m_custodians" "block_timestamp" "m_defaultRequiredConfirmations"
            "_address" "msg_pubkey"
    -> l1 | "m_transactions".
no_err (submitTransaction rec def dest value__ cc bounce allBalance payload) l0.
execs0 (_removeExpiredTransactions rec def ) : ll  -> l2.
set (index := m_custodians[msg_pubkey]? ).
set (l2_accepted := exec_state (Uinterpreter tvm_accept) l2).
evals (_getSendFlags rec def allBalance) : l2_accepted -> v_f.
evals (_generateId rec def) : l2_accepted -> v_i.

hyp (eqb m_defaultRequiredConfirmations 1 = false).
hyp (eqb m_defaultRequiredConfirmations 0 = false).

con (m_transactions [toValue v_i]? = Some _).
split. con (toValue v_i). (* id *)
split. con (xIntBitOpLeft 1 (uint2N (unMaybe index))). (* confirmationsMask *)
split. con m_defaultRequiredConfirmations. (* signsRequired *)
split. con 1. (* signsReceived *)
split. con msg_pubkey. (* creator *)
split. con (unMaybe index). (* index *)
split. con dest. (* dest *)
split. con value__. (* value *)
split. con cc. (* cc *)
split. con (uint2N (toValue v_f)). (* sendFlags *)
split. con payload. (* payload *)
con bounce. (* bounce *)
Defined.

Explanation:

No error occurs
Hypotheses: m_defaultRequiredConfirmations > 1
After cleanup, accept, generate ID and flags
Transaction created in m_transactions[v_i] with:
- id: Generated unique ID
- confirmationsMask: Bit set for submitter (1 << index)
- signsRequired: Default threshold
- signsReceived: 1 (submitter's confirmation)
- creator: Submitter's public key
- index: Submitter's custodian index
- dest, value, cc, payload, bounce: From parameters
- sendFlags: Computed from allBalance
No message sent yet (waiting for more confirmations)

submitTransaction - Request Mask Update

Purpose: Specify request mask increment

Specification:

Definition MUL22_TRO_def (ll: LedgerLRecord rec)
                        (dest : address) (value__ : uint128)
                        (cc : mapping(uint32)(varUint32)) (bounce : bool)
                        (allBalance : bool) (payload : TvmCell): Prop.
execs0 (submitTransaction rec def dest value__ cc bounce allBalance payload) :
       ll | "m_defaultRequiredConfirmations" "m_custodians" "msg_pubkey"
    -> l1 | "m_requestsMask".
no_err (submitTransaction rec def dest value__ cc bounce allBalance payload) l0.
execs0 (_removeExpiredTransactions rec def ) : ll  -> l2 | "m_requestsMask".
set (index := m_custodians[msg_pubkey]? ).

hyp (eqb m_defaultRequiredConfirmations 1 = false).
hyp (eqb m_defaultRequiredConfirmations 0 = false).

con (m_requestsMask = xIntPlus m_requestsMask'
                       (xIntBitOpLeft 1 (xIntMult 8 (uint2N (unMaybe index))))).
Defined.

Explanation:

When M > 1, request mask is incremented
Formula: m_requestsMask += (1 << (8 * index))
This increments the 8-bit counter for custodian index

Specification Patterns

Pattern 1: Error vs Success Cases

Split specifications into separate definitions:

(* Error case *)
Definition FUNC_TRI_def (...): Prop :=
  err0 (function args) ledger.
  con (error_condition).

(* Success case *)
Definition FUNC_TRO_def (...): Prop :=
  execs0 (function args) : ledger1 -> ledger2.
  no_err (function args) ledger1.
  con (success_postconditions).

Pattern 2: Multiple Success Cases

Use numbered variants for different execution paths:

(* Fast path *)
Definition FUNC1_TRO_def (...): Prop :=
  hyp (condition1).
  con (outcome1).

(* Slow path *)
Definition FUNC2_TRO_def (...): Prop :=
  hyp (negb condition1).
  con (outcome2).

Pattern 3: State Projections

Specify only relevant fields:

execs0 (function args) :
    ledger1 | "field_read1" "field_read2"
 -> ledger2 | "field_written".

This documents:

What the function reads
What the function modifies
What remains unchanged

Pattern 4: Intermediate Computations

Use set for clarity:

set (index := m_custodians[msg_pubkey]?).
set (count := _getMaskValue(m_requestsMask, index)).
con (count < MAX_QUEUED_REQUESTS).

Verification Strategy

Specification Completeness

For each function, specify:

All error cases - When should it fail?
All success cases - What are the different execution paths?
State changes - What fields are modified?
Return values - What does it return?
Side effects - What messages are sent?

Specification Hierarchy

submitTransaction
├── MUL1_TRI (error case)
├── MUL1_TRO (M=1, immediate send)
├── MUL21_TRO (M>1, create transaction)
└── MUL22_TRO (M>1, update request mask)

Each specification is proven separately, then combined to show total correctness.

Next Steps

Now that we have specifications, we can:

Direct Proofs - Prove the specifications hold
Verification - Understand verification principles
Standard Library - Use verified library functions

URSUS language Documentation

Writing Specifications: Multisignature Wallet

Overview

Specification DSL

Core Constructs

Ledger Projections

Contract Invariants

Global Invariants

Custodian Count Invariant

Request Mask Invariant

Confirmation Threshold Invariant

Transaction Consistency Invariant

Function Specifications

Helper Functions

_generateId

_getSendFlags

_findCustodian

Main Functions

submitTransaction - Error Case

submitTransaction - Fast Path (M=1)

submitTransaction - Queue Path (M>1)

submitTransaction - Request Mask Update

Specification Patterns

Pattern 1: Error vs Success Cases

Pattern 2: Multiple Success Cases

Pattern 3: State Projections

Pattern 4: Intermediate Computations

Verification Strategy

Specification Completeness

Specification Hierarchy

Next Steps

See Also

Keyboard shortcuts

URSUS language Documentation