Custom Grammar Extensions

Ursus extends Coq's grammar to provide a domain-specific syntax for smart contracts. This makes Ursus code look like a specialized programming language while remaining valid Coq code.

Overview

Coq allows custom grammar extensions through its notation mechanism and custom entry points. Ursus leverages this to create contract-specific syntax that is:

1. Familiar - Resembles Solidity and other smart contract languages
2. Type-safe - Fully checked by Coq's type system
3. Verifiable - Can be reasoned about using Coq proofs
4. Extractable - Translates to target languages

Contract-Level Grammar

Contract Declaration

Syntax:

Contract ContractName ;

What it does:

• Declares a new contract module
• Initializes contract metadata
• Sets up the contract namespace

Underlying Coq: This is a custom command that generates:

• Module definitions
• Type declarations
• Metadata records

Sends To Declaration

Syntax:

Sends To Interface1 Interface2 ... ;

What it does:

• Declares external interfaces this contract can call
• Enables type checking for inter-contract calls
• Generates interface bindings

Examples:

Sends To IERC20 IOwnable ;  (* Multiple interfaces *)
Sends To ;                   (* No external calls *)

Inherits Declaration

Syntax:

Inherits Parent1 Parent2 ... ;
Inherits Parent => overrides [method1 method2] ;

What it does:

• Specifies parent contracts
• Controls method inheritance
• Enables selective overriding

Types Section

Syntax:

Types
  Record TypeName := {
      field1: type1;
      field2: type2
  },
  Inductive EnumName :=
    | Constructor1
    | Constructor2
  ;

What it does:

• Defines custom data structures
• Creates record types
• Declares enumerations

Constants Section

Syntax:

Constants
  Definition CONSTANT_NAME : type := value
  Definition ANOTHER_CONST : type := value
;

What it does:

• Declares contract-level constants
• Provides compile-time values
• Enables constant folding

Contract Record

Syntax:

Record Contract := {
    field1: type1;
    field2: type2;
    #[static] staticField: type3
}.

What it does:

• Defines contract state structure
• Specifies storage layout
• Marks static (immutable) fields

Function-Level Grammar

Function Declaration

Syntax:

#[attribute1, attribute2]
Ursus Definition functionName (arg1: type1) (arg2: type2):
  UExpression returnType panicFlag.
{
    (* function body *)
}
return.
Defined.
Sync.

Components:

• #[...] - Function attributes (visibility, modifiers)
• Ursus Definition - Function declaration keyword
• UExpression - Monadic return type
• panicFlag - Can function panic? (true/false)
• return - Return statement
• Defined - Coq definition terminator
• Sync - Synchronize with code generator

Function Attributes

#[pure]                    (* No state modification *)
#[view]                    (* Read-only function *)
#[public]                  (* Publicly callable *)
#[external]                (* External interface *)
#[internal]                (* Internal only *)
#[override]                (* Overrides parent *)
#[payable]                 (* Can receive funds *)
#[nonpayable]              (* Cannot receive funds *)
#[returns=varName]         (* Named return variable *)
#[write=arg]               (* Mutable argument *)
#[no_body]                 (* Interface declaration *)

Statement-Level Grammar

Statement Notation

Ursus uses special notation for statements within function bodies:

Basic form:

::// statement .

With continuation:

::// statement1 .
::// statement2 .
::// statement3 |.

Notation symbols:

• :: - Statement introducer (custom tactic)
• // - Statement delimiters
• . - Statement separator (more statements follow)
• | - Statement terminator (last statement)

Variable Declaration

Syntax:

::// var 'varName : type := value .
::// new 'varName : type @ "name" := value .

Examples:

::// var 'x : uint256 := {0} .
::// new 'balance : uint256 @ "balance" := {1000} .

Difference:

• var - Simple local variable
• new - Named variable (appears in generated code with specific name)

Assignment

Syntax:

::// variable := expression .

Examples:

::// balance := balance + amount .
::// owner := msg->sender .
::// approved := @true .

Array/Mapping Access

Syntax:

::// mapping[[key]] := value .
::// value := mapping[[key]] .

Examples:

::// balances[[msg->sender]] := {0} .
::// allowance[[owner]][[spender]] := amount .

Control Flow

If-Then:

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

If-Then-Else:

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

While Loop:

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

For Loop:

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

Panic Flags (Holes)

The ->> and -/> symbols indicate whether a code block can panic:

• ->> - Block completes normally (no panic)
• -/> - Block may panic (can exit early)

Example:

::// if balance < amount then { ->/> } else { ->> } | .
{
    ::// exit_ {1} |.  (* Panic exit *)
}
{
    ::// balance := balance - amount |.  (* Normal execution *)
}

Expression-Level Grammar

Literals

{42}           (* Numeric literal *)
{0xFF}         (* Hex literal *)
@true          (* Boolean true *)
@false         (* Boolean false *)
"string"       (* String literal *)

Operators

Arithmetic:

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

Comparison:

a == b         (* Equality *)
a != b         (* Inequality *)
a < b          (* Less than *)
a > b          (* Greater than *)
a <= b         (* Less or equal *)
a >= b         (* Greater or equal *)

Logical:

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

Bitwise:

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

Message Access

msg->sender    (* Message sender *)
msg->value     (* Message value *)
msg->data      (* Message data *)

Function Calls

Internal:

::// result := functionName(arg1, arg2) .

External:

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

Grammar Levels and Scopes

Ursus grammar is organized into multiple levels:

Level 1: Core Inductive Types

The foundation of Ursus grammar consists of three inductive types defined in UrsusCore.v:

1. URValueP - Right values (expressions)
2. ULValueP - Left values (locations)
3. UExpressionP - Statements and control flow

These types define the abstract syntax tree of Ursus programs.

Learn more:

• URValue Grammar
• ULValue Grammar
• UExpression Grammar

Level 2: Notation Scopes

Notations provide readable syntax for the core types:

ursus_scope - Core Ursus primitives:

Local Open Scope ursus_scope.

# 42                    (* URScalar *)
μ Ledger_MainState     (* URState *)
r ^^ field             (* URField *)
m [[ i ]]              (* URIndex *)

usolidity_scope - Solidity-like syntax:

Local Open Scope usolidity_scope.

::// statement .       (* Statement notation *)
x := e                 (* Assignment *)
a + b                  (* Operators *)
if c then e1 else e2   (* Conditionals *)

record scope - Record field access:

Local Open Scope record.

s.(field)              (* Field projection *)
s <| field := v |>     (* Field update *)

Level 3: Contract-Level Commands

Custom Coq commands for contract structure:

• Contract Name ; - Contract declaration
• Sends To ... ; - Interface declarations
• Inherits ... ; - Inheritance
• Types ... ; - Type definitions
• Constants ... ; - Constant definitions

Level 4: Function-Level Tactics

Tactics for writing function bodies:

• ::// statement . - Statement introducer
• {->>} - Block delimiter
• return - Return statement
• var 'x := e - Variable declaration

Grammar Extension Mechanism

Ursus extends Coq's grammar using:

1. Notations - Syntactic sugar for terms
2. Custom entries - New grammar categories
3. Tactics - Proof mode extensions
4. Commands - Top-level declarations

Example: Assignment notation

Notation "x := e" := (AssignExpression x e default)
  (at level 70, no associativity) : usolidity_scope.

This notation:

• Operates at precedence level 70
• Is non-associative
• Is active in usolidity_scope
• Expands to AssignExpression constructor

See Also

• Ursus Embedding - How syntax maps to semantics
• Notations - Detailed notation definitions
• URValue Grammar - Right value constructors
• ULValue Grammar - Left value constructors
• UExpression Grammar - Statement constructors
• Writing Functions - Function syntax guide