Notational Mechanism

Ursus uses Coq's powerful notation system to provide readable, domain-specific syntax for smart contracts. This section explains how notations work and how they map to underlying Coq terms.

Overview

Notations are syntactic sugar that transforms readable code into formal Coq terms. They enable:

1. Familiar syntax - Code looks like traditional programming languages
2. Type safety - All notations are type-checked by Coq
3. Formal semantics - Each notation has precise mathematical meaning
4. Proof support - Can reason about notations using Coq tactics

Notation Scopes

Ursus defines several notation scopes for different contexts:

usolidity_scope

The main scope for Ursus/Solidity-like syntax:

Local Open Scope usolidity_scope.

Provides:

• Statement notations (::// ... .)
• Expression operators (+, -, *, /, etc.)
• Comparison operators (==, !=, <, >, etc.)
• Logical operators (&&, ||, !)
• Assignment operators (:=, +=, -=, etc.)

Other Scopes

• ursus_scope - Core Ursus primitives
• solidity_scope - Solidity-specific features
• tvm_scope - TVM-specific operations

Statement Notations

Basic Statement Form

Notation:

::// statement .

Expands to:

refine (statement ; _)

Purpose:

• Introduces a statement in function body
• Automatically handles sequencing
• Integrates with Coq's proof mode

Statement Terminator

Notation:

::// statement |.

Expands to:

refine statement

Purpose:

• Marks the last statement in a sequence
• No continuation needed

Statement Separators

With continuation (.):

::// stmt1 .
::// stmt2 .
::// stmt3 |.

Expands to:

refine (stmt1 ; (stmt2 ; stmt3))

Variable Declaration

Simple Variable

Notation:

::// var 'x : T := value .

Expands to:

refine (let x := value in _)

Example:

::// var 'balance : uint256 := {0} .

Named Variable

Notation:

::// new 'x : T @ "name" := value ; _ .

Expands to:

refine (ULet "name" value (fun x => _))

Purpose:

• Creates variable with specific name in generated code
• Useful for debugging and code generation

Example:

::// new 'total : uint256 @ "totalAmount" := {1000} ; _ .

Tuple Declaration

Notation:

::// new ('x : T1, 'y : T2) @ ("x", "y") := value ; _ .

Expands to:

refine (ULetTuple "x" "y" value (fun x y => _))

Example:

::// new ('a : uint256, 'b : uint256) @ ("a", "b") := getPair() ; _ .

Assignment Notations

Simple Assignment

Notation:

x := e

Expands to:

UAssign x e

Type constraint:

• x : ULValue T
• e : URValue T b

Compound Assignment

Addition assignment:

x += e  ≡  x := x + e

Other operators:

x -= e  ≡  x := x - e
x *= e  ≡  x := x * e
x /= e  ≡  x := x / e
x %= e  ≡  x := x % e
x &= e  ≡  x := x & e
x |= e  ≡  x := x | e
x ^= e  ≡  x := x ^ e

Increment/Decrement

Pre-increment:

++x  ≡  x := x + {1}

Post-increment:

x++  ≡  (let tmp := x in x := x + {1}; tmp)

Decrement:

--x  ≡  x := x - {1}
x--  ≡  (let tmp := x in x := x - {1}; tmp)

Expression Notations

Arithmetic Operators

Binary operators:

a + b   (* Addition *)
a - b   (* Subtraction *)
a * b   (* Multiplication *)
a / b   (* Division *)
a % b   (* Modulo *)
a ** b  (* Exponentiation *)

Expands to:

UPlus a b
UMinus a b
UMult a b
UDiv a b
UMod a b
UPow a b

Comparison Operators

a == b  (* Equal *)
a != b  (* Not equal *)
a < b   (* Less than *)
a > b   (* Greater than *)
a <= b  (* Less or equal *)
a >= b  (* Greater or equal *)

Expands to:

UEq a b
UNeq a b
ULt a b
UGt a b
ULe a b
UGe a b

Logical Operators

a && b  (* Logical AND *)
a || b  (* Logical OR *)
!a      (* Logical NOT *)

Expands to:

UAnd a b
UOr a b
UNot a

Bitwise Operators

a & b   (* Bitwise AND *)
a | b   (* Bitwise OR *)
a ^ b   (* Bitwise XOR *)
~a      (* Bitwise NOT *)
a << n  (* Left shift *)
a >> n  (* Right shift *)

Literal Notations

Numeric Literals

Notation:

{42}
{0xFF}
{1000000}

Expands to:

ULiteral (N_to_uint256 42)
ULiteral (N_to_uint256 255)
ULiteral (N_to_uint256 1000000)

Boolean Literals

Notation:

@true
@false

Expands to:

ULiteral true
ULiteral false

String Literals

Notation:

"hello"

Expands to:

ULiteral "hello"

Control Flow Notations

If-Then-Else

Notation:

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

Expands to:

UIf condition
    (then_branch)
    (else_branch)

If-Then (no else)

Notation:

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

Expands to:

UIf condition
    (then_branch)
    USkip

While Loop

Notation:

::// while condition do { ->> } | .
{
    (* loop body *)
}

Expands to:

UWhile condition (loop_body)

For Loop

Notation:

::// for 'i in range do { ->> } | .
{
    (* loop body *)
}

Expands to:

UFor range (fun i => loop_body)

Mapping and Array Access

Mapping Access

Notation:

mapping[[key]]

Expands to:

UMapAccess mapping key

Nested mappings:

mapping[[key1]][[key2]]

Expands to:

UMapAccess (UMapAccess mapping key1) key2

Array Access

Notation:

array[[index]]

Expands to:

UArrayAccess array index

Struct Field Access

Notation:

struct->field

Expands to:

UFieldAccess struct "field"

Chained access:

user->profile->name

Expands to:

UFieldAccess (UFieldAccess user "profile") "name"

Function Call Notations

Internal Call

Notation:

functionName(arg1, arg2, arg3)

Expands to:

UCall functionName [arg1; arg2; arg3]

External Call (Message Send)

Notation:

send Interface.Method(args) => target with params

Expands to:

USend Interface Method args target params

Example:

::// send IERC20.Transfer(from, to, amount)
         => token_address
         with {InternalMessageParams} [$ {2} ⇒ {flag} $] .

Special Notations

Return Statement

Notation:

return value

Expands to:

UReturn value

Skip (No-op)

Notation:

skip_

Expands to:

USkip

Exit (Panic)

Notation:

exit_ code

Expands to:

UExit code

Require

Notation:

require_ condition
require_ condition, error_code

Expands to:

URequire condition default_error
URequire condition error_code

Message Access Notations

Notation:

msg->sender
msg->value
msg->data

Expands to:

UMsgField "sender"
UMsgField "value"
UMsgField "data"

Panic Holes

The ->> and -/> symbols are "holes" that indicate panic behavior:

Non-panicking hole:

{ ->> }

Expands to:

(fun _ => _) : UExpression unit false

Panicking hole:

{ -/> }

Expands to:

(fun _ => _) : UExpression unit true

Purpose:

• Placeholder for code blocks
• Type-level tracking of panic possibility
• Enables panic-aware type checking

Custom Notations

You can define custom notations for your contracts:

Notation "'transfer_from' from 'to' to 'amount' amt" :=
  (UTransfer from to amt)
  (at level 200).

Usage:

::// transfer_from sender to recipient amount {100} .

Notation Precedence

Ursus notations follow standard precedence rules:

See Also

• Custom Grammar - Grammar extensions
• Ursus Embedding - Semantic foundations
• Writing Functions - Practical examples
• Operators - Standard operators