Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Tactics and Tacticals

Tactics are commands that construct code by transforming goals. In Ursus, tactics are your primary tool for building contract functions.

Core Ursus Tactics

The :: Tactic

The main tactic for writing Ursus statements:

Syntax:

::// statement .
::// statement |.

What it does:

  • Processes Ursus statement notation
  • Automatically sequences statements
  • Handles type inference

Example:

{
    ::// var 'x : uint256 := {42} .
    ::// y := y + x .
    ::// _result := y |.
}

The refine Tactic

Provide a partial term with holes:

Syntax:

refine term.

Example:

{
    refine // var 'x : uint256 := {42} ; _ //.
    refine // _result := x //.
}

Use cases:

  • Low-level control
  • Complex expressions
  • When :: doesn't work

The return Command

Complete function definition:

Syntax:

return.
return value.

Examples:

(* No return value *)
return.

(* With return value *)
return balance.

(* With expression *)
return {0}.

Standard Coq Tactics

simpl - Simplify

Reduce expressions:

{
    simpl.  (* Simplify current goal *)
    ::// ...
}

Example:

(* Before simpl *)
Goal: UExpression (if true then uint256 else uint8) false

(* After simpl *)
Goal: UExpression uint256 false

unfold - Expand Definitions

Expand defined terms:

{
    unfold MyType.
    ::// ...
}

Example:

unfold UExpression.
(* Reveals: ContractState -> Result (A * ContractState) *)

intro / intros - Introduce Variables

Introduce function parameters:

Proof.
    intros x y z.
    (* x, y, z now in context *)

apply - Apply Function

Apply a function or lemma:

{
    apply my_helper_function.
}

exact - Provide Exact Term

Give exact solution:

{
    exact {42}.
}

Tacticals (Tactic Combinators)

; - Sequence

Apply tactic, then apply another to all subgoals:

{
    split; simpl.
    (* Splits goal, then simplifies both subgoals *)
}

|| - Try Alternatives

Try first tactic, if it fails try second:

{
    (apply lemma1 || apply lemma2).
}

try - Try Without Failing

Try tactic, continue if it fails:

{
    try simpl.
    (* Simplifies if possible, continues otherwise *)
}

repeat - Repeat Until Failure

Repeat tactic until it fails:

{
    repeat (simpl; unfold).
}

do - Repeat N Times

Repeat tactic exactly N times:

{
    do 3 intro.
    (* Introduces 3 variables *)
}

Ursus-Specific Patterns

Pattern 1: Variable Declaration

::// var 'name : type := value .

Expands to:

refine (let name := value in _).

Pattern 2: Assignment

::// lvalue := rvalue .

Expands to:

refine (UAssign lvalue rvalue ; _).

Pattern 3: Control Flow

::// if condition then { ->> } else { ->> } | .
{
    (* then branch *)
}
{
    (* else branch *)
}

Creates two subgoals:

  1. Then branch body
  2. Else branch body

Advanced Tactics

Show - Display Goal

Show current goal and context:

{
    ::// var 'x : uint256 := {42} .
    Show.
    ::// ...
}

Check - Type Check

Check type of expression:

{
    Check (x + y).
    (* URValue uint256 false *)
}

assert - Add Hypothesis

Add intermediate fact:

Proof.
    assert (H: x > 0).
    { (* Prove H *) }
    (* Use H in main proof *)

destruct - Case Analysis

Analyze by cases:

Proof.
    destruct b.
    { (* Case: b = true *) }
    { (* Case: b = false *) }

induction - Inductive Proof

Prove by induction:

Proof.
    induction n.
    { (* Base case: n = 0 *) }
    { (* Inductive case: n = S n' *) }

Debugging Tactics

idtac - Print Message

Print debug message:

{
    idtac "Reached this point".
    ::// ...
}

fail - Force Failure

Force tactic to fail (for testing):

{
    fail "This should not happen".
}

admit - Skip Proof

Temporarily skip proof (for development):

Proof.
    admit.
Admitted.

Warning: Don't use in production!

See Also