Verification Principles

This section covers the fundamental principles and techniques for verifying Ursus smart contracts.

Core Principles

1. Specification Before Implementation

Principle: Define what the code should do before writing it.

Example:

(* Specification *)
Definition transfer_spec (from to: address) (amount: uint256)
                         (s s': ContractState) : Prop :=
  balance s' to = balance s to + amount /\
  balance s' from = balance s from - amount /\
  total_supply s' = total_supply s.

(* Implementation *)
Ursus Definition transfer (to: address) (amount: uint256):
  UExpression boolean false.
{
    ::// balances[[msg->sender]] := balances[[msg->sender]] - amount .
    ::// balances[[to]] := balances[[to]] + amount .
    ::// _result := @true |.
}
return.
Defined.

(* Verification *)
Theorem transfer_correct:
  forall from to amount s s',
    exec_transfer from to amount s = Some s' ->
    transfer_spec from to amount s s'.

2. Invariants

Principle: Identify properties that must always hold.

Example:

Definition total_supply_invariant (s: ContractState) : Prop :=
  s.(totalSupply) = sum_balances s.(balances).

Theorem all_operations_preserve_invariant:
  forall op s s',
    total_supply_invariant s ->
    exec_operation op s = Some s' ->
    total_supply_invariant s'.

3. Preconditions and Postconditions

Principle: Specify what must be true before and after execution.

Example:

(* Precondition *)
Definition transfer_pre (from: address) (amount: uint256) (s: ContractState) : Prop :=
  balance s from >= amount.

(* Postcondition *)
Definition transfer_post (from to: address) (amount: uint256)
                         (s s': ContractState) : Prop :=
  balance s' to = balance s to + amount /\
  balance s' from = balance s from - amount.

(* Hoare triple *)
Theorem transfer_hoare:
  forall from to amount s s',
    transfer_pre from amount s ->
    exec_transfer from to amount s = Some s' ->
    transfer_post from to amount s s'.

4. Compositionality

Principle: Verify components independently, then compose.

Example:

(* Verify helper function *)
Theorem validate_amount_correct:
  forall amount,
    exec_validate_amount amount = (amount > 0).
Proof. ... Qed.

(* Use in main function proof *)
Theorem transfer_correct:
  forall from to amount s s',
    exec_transfer from to amount s = Some s' ->
    ...
Proof.
  intros.
  unfold exec_transfer in H.
  rewrite validate_amount_correct.  (* Use helper proof *)
  ...
Qed.

Verification Techniques

Hoare Logic

Triple: {{ P }} c {{ Q }}

• P - Precondition
• c - Code
• Q - Postcondition

Rules:

Assignment:

{{ Q[x := e] }}
  x := e
{{ Q }}

Sequence:

{{ P }} c1 {{ R }}    {{ R }} c2 {{ Q }}
─────────────────────────────────────────
{{ P }} c1; c2 {{ Q }}

Conditional:

{{ P ∧ b }} c1 {{ Q }}    {{ P ∧ ¬b }} c2 {{ Q }}
──────────────────────────────────────────────────
{{ P }} if b then c1 else c2 {{ Q }}

Weakest Precondition

Definition: The weakest condition that guarantees postcondition.

Example:

Definition wp_assign (x: ULValue T) (e: URValue T) (Q: ContractState -> Prop) :=
  fun s => Q (update_state s x (eval e s)).

Theorem wp_assign_correct:
  forall x e Q s s',
    wp_assign x e Q s ->
    exec_assign x e s = Some s' ->
    Q s'.

Strongest Postcondition

Definition: The strongest condition guaranteed after execution.

Example:

Definition sp_assign (x: ULValue T) (e: URValue T) (P: ContractState -> Prop) :=
  fun s' => exists s, P s /\ s' = update_state s x (eval e s).

Common Proof Patterns

Pattern 1: Induction on Structure

Theorem sum_correct:
  forall n,
    exec_sum n = n * (n + 1) / 2.
Proof.
  induction n.
  { (* Base: n = 0 *)
    simpl. reflexivity.
  }
  { (* Step: n = S n' *)
    simpl.
    rewrite IHn.
    (* Arithmetic *)
    ...
  }
Qed.

Pattern 2: Case Analysis

Theorem conditional_correct:
  forall b x y,
    exec_if b x y = if b then x else y.
Proof.
  intros.
  destruct b.
  { (* Case: b = true *)
    simpl. reflexivity.
  }
  { (* Case: b = false *)
    simpl. reflexivity.
  }
Qed.

Pattern 3: Invariant Preservation

Theorem loop_preserves_invariant:
  forall n s,
    invariant s ->
    invariant (exec_loop n s).
Proof.
  induction n; intros.
  { (* Base case *)
    assumption.
  }
  { (* Inductive case *)
    simpl.
    apply IHn.
    apply step_preserves_invariant.
    assumption.
  }
Qed.

See Also

• Verification Overview - Introduction to verification
• StdLib Verification - Verified standard library
• QuickChick - Property-based testing