Standard Library Verification

The Ursus standard library provides verified implementations of common operations and data structures. This section documents the verification guarantees.

Verified Components

Arithmetic Operations

All arithmetic operations are verified for correctness and safety.

Addition

Specification:

Theorem plus_correct:
  forall (a b: uint256) (s: ContractState),
    eval (a + b) s = (eval a s) + (eval b s).

Overflow behavior:

Theorem plus_overflow:
  forall (a b: uint256),
    a + b < a -> (* Overflow occurred *)
    a + b = (a + b) mod 2^256.

Subtraction

Specification:

Theorem minus_correct:
  forall (a b: uint256) (s: ContractState),
    eval a s >= eval b s ->
    eval (a - b) s = (eval a s) - (eval b s).

Underflow behavior:

Theorem minus_underflow:
  forall (a b: uint256),
    a < b -> (* Underflow would occur *)
    a - b = 0.  (* Saturating subtraction *)

Multiplication

Specification:

Theorem mult_correct:
  forall (a b: uint256) (s: ContractState),
    eval (a * b) s = (eval a s) * (eval b s) mod 2^256.

Division

Specification:

Theorem div_correct:
  forall (a b: uint256) (s: ContractState),
    eval b s <> 0 ->
    eval (a / b) s = (eval a s) / (eval b s).

Division by zero:

Theorem div_by_zero:
  forall (a: uint256),
    a / {0} = {0}.  (* Returns zero *)

Comparison Operations

Equality

Specification:

Theorem eq_correct:
  forall (a b: uint256) (s: ContractState),
    eval (a == b) s = true <-> eval a s = eval b s.

Less Than

Specification:

Theorem lt_correct:
  forall (a b: uint256) (s: ContractState),
    eval (a < b) s = true <-> eval a s < eval b s.

Logical Operations

AND

Specification:

Theorem and_correct:
  forall (a b: boolean) (s: ContractState),
    eval (a && b) s = (eval a s) && (eval b s).

Short-circuit:

Theorem and_short_circuit:
  forall (a b: boolean) (s: ContractState),
    eval a s = false ->
    eval (a && b) s = false.  (* b not evaluated *)

OR

Specification:

Theorem or_correct:
  forall (a b: boolean) (s: ContractState),
    eval (a || b) s = (eval a s) || (eval b s).

Short-circuit:

Theorem or_short_circuit:
  forall (a b: boolean) (s: ContractState),
    eval a s = true ->
    eval (a || b) s = true.  (* b not evaluated *)

Mapping Operations

Fetch

Specification:

Theorem fetch_correct:
  forall (m: mapping K V) (k: K) (s: ContractState),
    eval (m->fetch(k)) s = lookup (eval m s) (eval k s).

Insert

Specification:

Theorem insert_correct:
  forall (m: mapping K V) (k: K) (v: V) (s s': ContractState),
    exec (m[[k]] := v) s = Some s' ->
    lookup (eval m s') k = Some (eval v s).

Delete

Specification:

Theorem delete_correct:
  forall (m: mapping K V) (k: K) (s s': ContractState),
    exec (m->delete(k)) s = Some s' ->
    lookup (eval m s') k = None.

Optional Operations

HasValue

Specification:

Theorem hasValue_correct:
  forall (x: optional T) (s: ContractState),
    eval (x->hasValue()) s = true <->
    exists v, eval x s = Some v.

Get

Specification:

Theorem get_correct:
  forall (x: optional T) (v: T) (s: ContractState),
    eval x s = Some v ->
    eval (x->get()) s = v.

Precondition:

Theorem get_requires_value:
  forall (x: optional T) (s: ContractState),
    eval x s = None ->
    (* get() panics *)
    exec (x->get()) s = Error.

Array Operations

Length

Specification:

Theorem length_correct:
  forall (arr: array T) (s: ContractState),
    eval (arr->length()) s = length (eval arr s).

Push

Specification:

Theorem push_correct:
  forall (arr: array T) (v: T) (s s': ContractState),
    exec (arr->push(v)) s = Some s' ->
    length (eval arr s') = length (eval arr s) + 1 /\
    last (eval arr s') = Some (eval v s).

Pop

Specification:

Theorem pop_correct:
  forall (arr: array T) (s s': ContractState),
    length (eval arr s) > 0 ->
    exec (arr->pop()) s = Some s' ->
    length (eval arr s') = length (eval arr s) - 1.

Using Verified Library

Import Verified Lemmas

Require Import UrsusStdLib.Verified.Arithmetic.
Require Import UrsusStdLib.Verified.Mappings.
Require Import UrsusStdLib.Verified.Optionals.

Apply in Proofs

Theorem my_function_correct:
  forall x y s s',
    exec_my_function x y s = Some s' ->
    result s' = x + y.
Proof.
  intros.
  unfold exec_my_function in H.
  rewrite plus_correct.  (* Use verified lemma *)
  ...
Qed.

See Also

• Verification Overview - Introduction to verification
• Verification Principles - Core concepts
• Standard Functions - Function reference
• Operators - Operator reference