Holes

Holes (_) are placeholders in Coq that represent code to be filled in later. They are essential for incremental development in Ursus.

What are Holes?

A hole is a placeholder that:

1. Type-checked - Must have correct type
2. Named or anonymous - Can be referenced
3. Filled incrementally - Complete step by step
4. Verified - Type system ensures correctness

Syntax:

_           (* Anonymous hole *)
?name       (* Named hole *)

Holes in Ursus

Statement Holes

Pattern:

refine // statement ; _ //.

Example:

{
    refine // var 'x : uint256 := {42} ; _ //.
    (* Hole for rest of function *)
}

Coq shows:

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

Expression Holes

Pattern:

refine (some_function _ _).

Example:

{
    refine (UPlus _ _).
    (* Two holes for operands *)
}

Control Flow Holes

Pattern:

::// if condition then { ->> } else { ->> } | .

The ->> and -/> are special holes:

• ->> - Non-panicking code block
• -/> - Potentially panicking code block

Example:

::// if balance > amount then { ->> } else { -/> } | .
{
    (* Non-panicking branch *)
    ::// balance := balance - amount |.
}
{
    (* Panicking branch *)
    ::// exit_ {1} |.
}

Panic Holes

Non-Panicking Hole (->>)

Indicates code that completes normally:

{ ->> }

Type:

UExpression unit false

Use when:

• Code always succeeds
• No exit_ or require_ calls
• No panicking function calls

Example:

::// if x > {0} then { ->> } | .
{
    ::// y := x + {1} |.  (* Always succeeds *)
}

Panicking Hole (-/>)

Indicates code that may panic:

{ -/> }

Type:

UExpression unit true

Use when:

• Code may call exit_
• Code may call require_
• Code calls panicking functions

Example:

::// if balance < amount then { -/> } | .
{
    ::// exit_ {1} |.  (* Panics *)
}

Hole with Placeholder (_)

Use _ for complex conditions:

::// if _ then { ->> } else { ->> } | .
(complex_condition)  (* Condition specified after *)
{
    (* then branch *)
}
{
    (* else branch *)
}

Example:

::// if _ then { ->> } else { ->> } | .
(balance[[sender]] >= amount && amount > {0})
{
    ::// transfer_internal(sender, recipient, amount) |.
}
{
    ::// skip_ |.
}

Incremental Development with Holes

Step 1: Skeleton

Start with high-level structure:

Ursus Definition transfer (to: address) (amount: uint256):
  UExpression boolean false.
{
    refine // _ //.  (* Hole for entire body *)
}
return @false.
Defined.

Step 2: Add Structure

Fill in control flow:

Ursus Definition transfer (to: address) (amount: uint256):
  UExpression boolean false.
{
    refine // if _ then { ->> } else { ->> } ; _ //.
    (balances[[msg->sender]] >= amount)
    {
        refine // _ //.  (* Hole for then branch *)
    }
    {
        refine // _ //.  (* Hole for else branch *)
    }
    refine // _ //.  (* Hole for rest *)
}
return @false.
Defined.

Step 3: Fill Branches

Complete each branch:

Ursus Definition transfer (to: address) (amount: uint256):
  UExpression boolean false.
{
    refine // if _ then { ->> } else { ->> } ; _ //.
    (balances[[msg->sender]] >= amount)
    {
        refine // balances[[msg->sender]] := balances[[msg->sender]] - amount ; _ //.
        refine // balances[[to]] := balances[[to]] + amount //.
    }
    {
        refine // skip_ //.
    }
    refine // @true //.
}
return.
Defined.

Named Holes

Use named holes for complex development:

Syntax:

?hole_name

Example:

{
    refine (UPlus ?left ?right).
}

Coq shows:

2 subgoals
______________________________________(1/2)
URValue uint256 false  (* ?left *)

______________________________________(2/2)
URValue uint256 false  (* ?right *)

Hole Errors

Type Mismatch

Error:

Error: Cannot infer type of hole

Solution: Provide type annotation

Before:

refine _.

After:

refine (_ : UExpression uint256 false).

Unfilled Holes

Error:

Error: Attempt to save an incomplete proof

Solution: Fill all holes before Defined

Wrong Panic Flag

Error:

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

Solution: Use correct hole type (->> vs -/>)

Best Practices

1. Start with Holes

Begin with skeleton, fill incrementally:

{
    refine // _ ; _ ; _ //.  (* Three statements *)
}

2. Use Descriptive Names

For complex holes:

{
    refine (calculate_fee ?amount ?rate).
}

3. Check Types

Verify hole types match:

{
    Check (_ : UExpression uint256 false).
}

4. Fill Systematically

Complete one hole at a time:

{
    refine // stmt1 ; _ //.
    (* Fill first hole *)
    refine // stmt2 ; _ //.
    (* Fill second hole *)
    refine // stmt3 //.
}

See Also

• REPL - Interactive development
• Goal and Context - Understanding goals
• Tactics - Filling holes with tactics
• Control Sub-language - Control flow holes