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

Goal and Context

When developing Ursus contracts, you work in Coq's proof mode, where you construct code by transforming goals using tactics. Understanding goals and context is essential for effective development.

What is a Goal?

A goal is what you need to construct. In Ursus, goals are typically:

  • Function bodies - UExpression T b
  • Expressions - URValue T b
  • Statements - UExpression unit b
  • Proofs - Prop (for verification)

Goal Display

When you enter proof mode, Coq shows:

n subgoals
var1 : type1
var2 : type2
...
______________________________________(1/n)
GoalType

Components:

  • Context (above line) - Available variables and hypotheses
  • Separator - Horizontal line with goal number
  • Goal (below line) - What you need to construct

Example: Function Development

Initial Goal

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

Coq shows:

1 subgoal
to : address
amount : uint256
______________________________________(1/1)
UExpression boolean false

Interpretation:

  • Context: You have to and amount available
  • Goal: You need to construct UExpression boolean false

After First Statement

{
    ::// var 'sender_balance : uint256 := balances[[msg->sender]] .

Coq shows:

1 subgoal
to : address
amount : uint256
sender_balance : ULValue uint256
______________________________________(1/1)
UExpression boolean false

Interpretation:

  • Context: Now includes sender_balance
  • Goal: Still need to construct UExpression boolean false

After More Statements

    ::// balances[[msg->sender]] := sender_balance - amount .
    ::// balances[[to]] := balances[[to]] + amount .

Coq shows:

1 subgoal
to : address
amount : uint256
sender_balance : ULValue uint256
______________________________________(1/1)
UExpression boolean false

Interpretation:

  • Context: Unchanged (statements don't add variables)
  • Goal: Still need final return value

Final Statement

    ::// _result := @true |.
}
return.
Defined.

Goal satisfied!

Understanding Context

The context contains everything available for constructing the goal:

Types of Context Entries

1. Function parameters:

to : address
amount : uint256

2. Local variables:

sender_balance : ULValue uint256
fee : ULValue uint256

3. Hypotheses (in proofs):

H1 : amount > 0
H2 : balance >= amount

4. Implicit arguments:

T : Type
b : bool

Using Context

You can use any variable from the context:

{
    ::// var 'total : uint256 := amount + fee .  (* Uses amount and fee from context *)
    ::// balances[[to]] := total .               (* Uses to and total from context *)
}

Multiple Goals

Some tactics create multiple goals:

Example: If-Then-Else

{
    ::// if amount > {100} then { ->> } else { ->> } | .

Coq shows:

2 subgoals
to : address
amount : uint256
______________________________________(1/2)
UExpression unit false

______________________________________(2/2)
UExpression unit false

Interpretation:

  • Goal 1: Then branch
  • Goal 2: Else branch

Solving Multiple Goals

Solve first goal (then branch):

{
    ::// balances[[to]] := balances[[to]] + amount |.
}

Coq shows:

1 subgoal
to : address
amount : uint256
______________________________________(1/1)
UExpression unit false

Solve second goal (else branch):

{
    ::// skip_ |.
}

All goals solved!

Goal Transformations

Tactics transform goals in various ways:

Refinement

Before:

______________________________________(1/1)
UExpression uint256 false

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

x : ULValue uint256
______________________________________(1/1)
UExpression uint256 false

Simplification

Before:

______________________________________(1/1)
UExpression (if true then uint256 else uint8) false

After simpl:

______________________________________(1/1)
UExpression uint256 false

Unfolding

Before:

______________________________________(1/1)
MyType

After unfold MyType:

______________________________________(1/1)
UExpression uint256 false

Inspecting Goals and Context

Show Command

Display current goal:

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

Output:

1 subgoal
x : ULValue uint256
______________________________________(1/1)
UExpression uint256 false

Show Proof

Display proof term constructed so far:

Show Proof.

Output:

(let x := {42} in ?Goal)

Check in Context

Check type of expression in current context:

{
    ::// var 'x : uint256 := {42} .
    Check (x + {1}).
    (* URValue uint256 false *)
}

Common Goal Patterns

Pattern 1: Expression Goal

______________________________________(1/1)
UExpression T b

Solution: Construct expression of type T with panic flag b

Pattern 2: Value Goal

______________________________________(1/1)
URValue T b

Solution: Provide value of type T

Pattern 3: Unit Goal

______________________________________(1/1)
UExpression unit false

Solution: Execute statements (side effects only)

Pattern 4: Boolean Goal

______________________________________(1/1)
UExpression boolean false

Solution: Return boolean value

Pattern 5: Proof Goal

______________________________________(1/1)
balance_after = balance_before + amount

Solution: Prove the proposition

Working with Complex Goals

Nested Structures

Goal:

______________________________________(1/1)
UExpression (optional (mapping address uint256)) false

Strategy:

  1. Understand the type structure
  2. Build from inside out
  3. Use helper functions if needed

Dependent Types

Goal:

______________________________________(1/1)
UExpression (if b then uint256 else uint8) false

Strategy:

  1. Simplify the condition
  2. Case analysis on b
  3. Solve each case

Debugging with Goals

Problem: Wrong Type

Goal:

______________________________________(1/1)
UExpression uint256 false

Attempt:

::// _result := "hello" |.

Error:

Error: The term "hello" has type "string"
while it is expected to have type "URValue uint256 false"

Solution: Check types match goal

Problem: Missing Variable

Goal:

______________________________________(1/1)
UExpression uint256 false

Attempt:

::// _result := undefined_var |.

Error:

Error: The reference undefined_var was not found

Solution: Check context for available variables

Problem: Wrong Panic Flag

Goal:

______________________________________(1/1)
UExpression uint256 false

Attempt:

::// _result := may_panic_function() |.

Error:

Error: Cannot unify "UExpression uint256 true"
with "UExpression uint256 false"

Solution: Use non-panicking expression or change function signature

See Also