Ursus Programming Style

Ursus is not just a language—it's a proof-driven development environment built on Coq. Understanding how to work effectively in this environment is essential for productive contract development.

Overview

Programming in Ursus combines:

Interactive Development - Using Coq's REPL for immediate feedback
Proof Mode - Leveraging Coq's goal-directed programming
Tactical Programming - Using tactics to construct code
Holes and Refinement - Incremental program construction

This approach enables:

Type-driven development - Let types guide implementation
Incremental verification - Prove properties as you code
Interactive debugging - Inspect goals and context at any point
Automated code generation - Use tactics to generate boilerplate

The Ursus Workflow

1. Write function signature
   ↓
2. Enter proof mode (see goals)
   ↓
3. Use tactics to refine goals
   ↓
4. Fill holes incrementally
   ↓
5. Complete definition
   ↓
6. Sync with code generator

Key Concepts

REPL (Read-Eval-Print Loop)

Coq provides an interactive environment where you can:

Load contract files
Execute commands
Inspect definitions
Test functions
Prove properties

Learn more: REPL

Goals and Context

When writing Ursus functions, you work in proof mode:

Goal - What you need to construct
Context - Available variables and hypotheses
Tactics - Commands to transform goals

Learn more: Goal and Context

Tactics and Tacticals

Tactics are commands that construct code:

refine - Provide partial term with holes
:: - Ursus-specific statement tactic
apply - Apply a function or lemma
simpl - Simplify expressions
auto - Automated proof search

Learn more: Tactics and Tacticals

Holes

Holes (_) are placeholders for code to be filled later:

Type-checked placeholders
Enable incremental development
Show what needs to be constructed

Learn more: Holes

Example: Interactive Development

Let's see how to develop a function interactively:

1. Start with Signature

Ursus Definition transfer (to: address) (amount: uint256):
  UExpression boolean false.

2. Enter Proof Mode

Coq shows the goal:

1 subgoal
______________________________________(1/1)
UExpression boolean false

3. Use Tactics to Build Code

{
    refine // balances[[msg->sender]] := balances[[msg->sender]] - amount ; _ //.
}

New goal:

1 subgoal
______________________________________(1/1)
UExpression boolean false

4. Continue Refining

{
    refine // balances[[msg->sender]] := balances[[msg->sender]] - amount ; _ //.
    refine // balances[[to]] := balances[[to]] + amount ; _ //.
    refine // @true //.
}

5. Complete Definition

return.
Defined.
Sync.

Modern Ursus Style

The :: tactic provides cleaner syntax:

Old style (verbose):

refine // new 'x : uint256 @ "x" := {1} ; _ //.
refine // y := y + x ; _ //.
refine // _result := y //.

New style (concise):

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

Benefits:

More readable
Less boilerplate
Clearer intent
Easier to maintain

Development Patterns

Pattern 1: Top-Down Development

Start with high-level structure, fill details later:

Ursus Definition complexFunction (x: uint256): UExpression uint256 false.
{
    ::// if x > {100} then { ->> } else { ->> } | .
    {
        (* TODO: Fill then branch *)
        ::// skip_ |.
    }
    {
        (* TODO: Fill else branch *)
        ::// skip_ |.
    }
}
return {0}.
Defined.

Pattern 2: Bottom-Up Development

Build helper functions first:

(* Helper function *)
Ursus Definition calculateFee (amount: uint256): UExpression uint256 false.
{
    ::// var 'fee : uint256 := amount * {3} / {100} |.
}
return fee.
Defined.

(* Main function using helper *)
Ursus Definition processPayment (amount: uint256): UExpression uint256 false.
{
    ::// var 'fee : uint256 := calculateFee(amount) .
    ::// var 'total : uint256 := amount + fee |.
}
return total.
Defined.

Pattern 3: Test-Driven Development

Write tests first, then implement:

(* Test specification *)
Theorem transfer_reduces_sender_balance:
  forall sender to amount s s',
    exec_transfer sender to amount s = Some s' ->
    balance s' sender = balance s sender - amount.
Proof.
  (* Proof guides implementation *)
Admitted.

(* Implementation *)
Ursus Definition transfer (to: address) (amount: uint256):
  UExpression boolean false.
{
    (* Implementation satisfies theorem *)
}
return.
Defined.

Best Practices

1. Use Descriptive Names

Good:

::// var 'totalFee : uint256 := calculateFee(amount) .
::// var 'recipientBalance : uint256 := balances[[recipient]] .

Bad:

::// var 'x : uint256 := calculateFee(amount) .
::// var 'b : uint256 := balances[[recipient]] .

2. Keep Functions Small

Break complex logic into smaller functions:

(* Good: Small, focused functions *)
Ursus Definition validateAmount (amount: uint256): UExpression boolean false.
Ursus Definition updateBalance (addr: address) (amount: uint256): UExpression unit false.
Ursus Definition transfer (to: address) (amount: uint256): UExpression boolean false.

(* Bad: One giant function *)
Ursus Definition doEverything (...): UExpression ... .

3. Use Type Annotations

Help Coq infer types correctly:

::// var 'balance : uint256 := balances[[addr]] .  (* Explicit type *)

4. Leverage Proof Mode

Use Coq's proof mode to explore:

{
    (* Check current goal *)
    Show.

    (* Simplify to see what's needed *)
    simpl.

    (* Continue development *)
    ::// ...
}

Debugging Techniques

Inspect Goals

{
    ::// var 'x : uint256 := {42} .
    Show.  (* See current goal and context *)
    ::// ...
}

Simplify Expressions

{
    simpl.  (* Reduce complex expressions *)
    ::// ...
}

Check Types

Check balances[[addr]].
(* ULValue uint256 *)

Check {42}.
(* URValue uint256 false *)

Next Steps

REPL - Interactive development environment
Goal and Context - Understanding proof mode
Tactics - Building code with tactics
Holes - Incremental program construction

URSUS language Documentation