Coq Embedded DSL

Ursus is implemented as an embedded domain-specific language (eDSL) within the Coq proof assistant. This design choice enables formal verification of smart contracts while maintaining a familiar programming syntax.

What is an Embedded DSL?

An embedded DSL is a specialized language implemented within a host language (in this case, Coq). Unlike standalone languages that require their own parser and compiler, embedded DSLs leverage the host language's infrastructure while providing domain-specific abstractions.

Benefits of Embedding in Coq

1. Formal Verification - Prove mathematical properties about contracts
2. Type Safety - Leverage Coq's powerful type system
3. Proof Automation - Use Coq's tactics for automated reasoning
4. Extraction - Generate executable code in multiple target languages
5. Reusability - Share proofs and abstractions across contracts

Ursus Architecture

┌─────────────────────────────────────────┐
│         Ursus Contract Code             │
│    (Custom Coq syntax + notations)      │
└──────────────┬──────────────────────────┘
               │
               ▼
┌─────────────────────────────────────────┐
│      Coq Custom Grammar Extension       │
│   (Defines Ursus-specific syntax)       │
└──────────────┬──────────────────────────┘
               │
               ▼
┌─────────────────────────────────────────┐
│         Ursus Embedding Layer           │
│  (Maps syntax to Coq terms/types)       │
└──────────────┬──────────────────────────┘
               │
               ▼
┌─────────────────────────────────────────┐
│      Coq Core (Gallina + Tactics)       │
│   (Type checking, proof verification)   │
└──────────────┬──────────────────────────┘
               │
               ├──────────────┬─────────────┐
               ▼              ▼             ▼
         Verification    Extraction    Simulation
         (Proofs)        (Solidity)    (Testing)

Key Components

1. Custom Grammar

Ursus extends Coq's grammar to support smart contract syntax through three core inductive types:

• URValue - Right values (expressions that produce values)
• ULValue - Left values (assignable locations)
• UExpression - Statements and control flow

Contract ERC20 ;
Sends To IERC20 ;
Inherits ;

This looks like a domain-specific language but is actually valid Coq code thanks to custom grammar rules.

Learn more:

• Custom Grammar - Contract-level syntax
• URValue Grammar - Right value constructors
• ULValue Grammar - Left value constructors
• UExpression Grammar - Statement constructors

2. Embedding Layer

The embedding layer maps high-level contract constructs to Coq's type theory:

• Contracts → Coq records
• Functions → Coq definitions with monadic types
• State → Coq record fields
• Expressions → Typed Coq terms (URValue/ULValue/UExpression)

Learn more: Ursus Embedding

3. Notational Mechanism

Notations make Ursus code readable and familiar to smart contract developers:

(* Ursus notation *)
balance := balance + amount

(* Underlying Coq term *)
AssignExpression (ULState balance) (URIndex (URState balance) (URScalar amount))

Learn more: Notations

How Ursus Works

Writing a Contract

When you write an Ursus contract:

#[translation = on]
#[language = solidity]
Contract Token ;
Sends To ;
Inherits ;

Record Contract := {
    totalSupply: uint256;
    balances: mapping address uint256
}.

Ursus Definition transfer (to: address) (amount: uint256): UExpression boolean false.
{
    :// balances[msg->sender] := balances[msg->sender] - amount.
    :// balances[to] := balances[to] + amount.
    :// return true.
}
return.
Defined.

What Happens Internally

1. Parsing - Coq parser processes custom syntax using grammar extensions
2. Elaboration - Ursus notations expand to Coq terms
3. Type Checking - Coq verifies type correctness
4. Embedding - Contract constructs map to formal semantics
5. Extraction - Code generator produces target language (Solidity/C++/Rust)

The Monadic Foundation

Ursus uses a state monad to model contract execution:

UExpression (A: Type) (b: bool) :=
  ContractState -> (A * ContractState) + Error

This encoding:

• Tracks state changes explicitly
• Enables reasoning about side effects
• Supports formal verification
• Allows extraction to imperative code

Verification Workflow

1. Write Contract
   ↓
2. Define Properties (Specifications)
   ↓
3. Prove Properties (Using Coq tactics)
   ↓
4. Extract Verified Code
   ↓
5. Deploy to Blockchain

Example property:

Theorem transfer_preserves_total_supply:
  forall (from to: address) (amount: uint256) (s s': ContractState),
    exec_transfer from to amount s = Some s' ->
    total_supply s = total_supply s'.

Comparison with Other Approaches

Getting Started

1. Learn Coq Basics - Understand Coq's type system and tactics
2. Study Custom Grammar - See how Ursus extends Coq syntax
3. Understand Embedding - Learn how contracts map to Coq terms
4. Master Notations - Write idiomatic Ursus code
5. Practice Verification - Prove properties about your contracts

Next Steps

• Custom Grammar - Ursus syntax extensions
• Ursus Embedding - Semantic foundations
• Notations - Writing readable contracts
• Simple Example - Complete contract walkthrough

Further Reading

• Coq Reference Manual
• Software Foundations
• Certified Programming with Dependent Types