Direct Proofs: Multisignature Wallet

This chapter demonstrates how to write direct proofs for the Multisignature Wallet specifications using Ursus's proof automation.

Overview

Direct proofs in Ursus verify that the contract implementation satisfies its specifications. The proof process involves:

Starting the proof - Initialize proof state
Symbolic execution - Execute the function symbolically
Simplification - Reduce complex expressions
Automation - Apply automated tactics
Manual steps - Handle remaining goals

Proof Architecture

Proof Structure

Each specification is proven as a separate lemma:

Lemma SPEC_NAME_prf (params...):
  SPEC_NAME_def params...
Proof.
  start_proof.                    (* Initialize *)
  time function_start.            (* Begin symbolic execution *)
  time continue_all @helpers.     (* Expand helper functions *)
  time prepare_all ll.            (* Prepare ledger state *)
  time process_pure_eval_execs.   (* Process pure computations *)
  compute_destructed_ledgers loc_.(* Compute local state *)
  time elpi sort_vars -1.         (* Sort variables with Elpi *)
  time elpi rename_vars.          (* Rename for readability *)
  time fast_solver.               (* Automated solving *)
Qed.

Core Proof Tactics

start_proof - Initialize proof environment
function_start - Begin symbolic execution of the function
continue_all @f1 @f2 ... - Expand calls to helper functions
prepare_all ll - Prepare ledger state for analysis
process_pure_eval_execs - Simplify pure computations
compute_destructed_ledgers loc_ - Compute local variable state
fast_solver - Automated proof search
elpi sort_vars N - Sort variables by dependencies (Elpi automation)
elpi rename_vars - Rename variables for readability
process_no_err_hyp C LEMMA - Use error-case lemma to prove no-error
process_single_optional - Handle optional value cases
process_multiexists - Handle multiple existentials
print_ifs2 - Debug: print conditional branches
single_replace VAR VALUE - Replace variable with value

Helper Function Proofs

_generateId: Purity Proof

Goal: Prove that _generateId doesn't depend on contract state

Lemma _generateId_eval_main_safe : forall (ll: LedgerLRecord rec),
eval_state (Uinterpreter (_generateId rec def)) ll =
eval_state (Uinterpreter (_generateId rec def))
  {$$ ll with Ledger_MainState := default $$}.
Proof.
    intros.
    time _generateId_start.           (* 0.5 secs *)
    check_evals_execs.
    time continue_all.                (* 0.3 secs *)
    time prepare_all ll.              (* 1.2 secs *)
    compute_destructed_ledgers loc_.
    time process_pure_eval_execs.     (* 0.8 secs *)
    time elpi sort_vars -1.           (* 0.7 secs *)
    time elpi rename_vars.            (* 0.2 secs *)
    time fast_solver.                 (* 0.5 secs *)
Qed. (* Total: ~4.2 seconds *)

Meaning: The function only depends on block/transaction context, not contract state.

_getSendFlags: Purity Proofs

Goal: Prove that _getSendFlags is a pure function

(* Evaluation doesn't depend on state *)
Lemma _getSendFlags_eval_pure (allBalance : bool) (ll: LedgerLRecord rec):
eval_state (Uinterpreter (_getSendFlags rec def allBalance)) ll =
eval_state (Uinterpreter (_getSendFlags rec def allBalance)) default.

(* Execution doesn't modify state *)
Lemma _getSendFlags_exec_pure allBalance (ll: LedgerLRecord rec):
exec_state (Uinterpreter (_getSendFlags rec def allBalance)) ll = ll.

(* Function always returns a value *)
Lemma _getSendFlags_eval_exists allBalance (l: LedgerLRecord rec):
exists s, eval_state
  (Uinterpreter (_getSendFlags rec def allBalance)) l = ControlValue _ s.

(* Register as pure function *)
DeclarePureEvalExec (@_getSendFlags)
                    (@_getSendFlags_eval_pure)
                    (@_getSendFlags_exec_pure).
DeclareExistsEval (@_getSendFlags) (@_getSendFlags_eval_exists).

Main Function Proofs

submitTransaction: Error Case

Specification: MUL1_TRI_def - Function fails when preconditions not met

Lemma MUL1_TRI_prf ll dest value__ cc bounce allBalance payload :
      MUL1_TRI_def ll dest value__ cc bounce allBalance payload.
Proof.
    start_proof.
    time submitTransaction_start.         (* 6.1 secs *)
    time continue_all @_findCustodian @_getMaskValue @_incMaskValue @get.
    time prepare_all ll.                  (* 8.1 secs *)
    time process_pure_eval_execs.         (* 5.7 secs *)
    compute_destructed_ledgers loc_.
    time elpi sort_vars -1.               (* 4.7 secs *)
    time process_single_optional.
    (* ... locality rewriting and conditional analysis ... *)
Time Qed. (* Total: ~51 seconds *)

Key techniques: Symbolic execution, helper expansion, optional handling, locality rewriting, conditional analysis.

submitTransaction: Success Case (M=1)

Specification: MUL1_TRO_def - Immediate execution when threshold is 1

Lemma MUL1_TRO_prf ll dest value__ cc bounce allBalance payload :
      MUL1_TRO_def ll dest value__ cc bounce allBalance payload.
Proof.
    start_proof.
    time submitTransaction_start.         (* 5.5 secs *)
    process_no_err_hyp C MUL1_TRI_prf.   (* Reuse error case *)
    time continue_all @_findCustodian @_getMaskValue @_incMaskValue
                      @get @tvm_transfer @deduct_currencies.
    time prepare_all ll.                  (* 19.1 secs *)
    (* ... prove message transfer specification ... *)
Time Qed. (* Total: ~60 seconds *)

Key difference: Uses MUL1_TRI_prf to prove no_err, then verifies message sent correctly.

URSUS language Documentation