Ursus Embedding

The Ursus embedding layer provides the formal semantics that map high-level contract syntax to Coq's type theory. This layer is the foundation for verification and code generation.

Overview

Embedding is the process of representing domain-specific constructs (smart contracts) using the host language's primitives (Coq). Ursus achieves this through:

1. Monadic encoding - State and effects as explicit types
2. Type mapping - Contract types to Coq types
3. Semantic functions - Operations with formal meaning
4. Proof infrastructure - Reasoning about contract behavior

The State Monad

UExpression Type

The core of Ursus is the UExpression monad:

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

Type parameters:

• A - Return type of the expression
• b - Panic flag (true = can panic, false = cannot panic)

Semantics:

• Takes current contract state
• Returns either:
  • Success (value, new_state) - Normal execution
  • Error error_code - Exceptional termination

Why a Monad?

Monads allow us to:

1. Sequence operations - Chain state transformations
2. Track side effects - Make state changes explicit
3. Handle errors - Model exceptional control flow
4. Enable verification - Reason about state transitions

Example:

(* High-level Ursus *)
::// balance := balance + amount .

(* Underlying monadic computation *)
do current_balance <- read_balance;
   new_balance <- add current_balance amount;
   write_balance new_balance

Value Types: ULValue and URValue

Ursus distinguishes between left values (assignable) and right values (readable). These are defined as inductive types with multiple constructors.

ULValue (Left Value)

Definition:

Inductive ULValueP : Type -> Type :=
    | ULState  : ... -> ULValueP U
    | ULField  : ... -> ULValueP U -> ULValueP (field_type f)
    | ULIndex  : ... -> ULValueP V
    | ULLocalIndex : ... -> ULValueP V
    | ULTuple : ... -> ULValueP (XProd A B)
    | ULFirst : ... -> ULValueP A
    | ULSecond : ... -> ULValueP B
    | ULUnMaybe: ... -> ULValueP A.

Represents:

• Storage locations (state variables) - ULState
• Record fields - ULField
• Mapping/array entries - ULIndex, ULLocalIndex
• Tuple components - ULTuple, ULFirst, ULSecond
• Optional values - ULUnMaybe

Operations:

• Can be read from (via coercion to URValue)
• Can be written to
• Can be passed by reference

Examples:

→ μ Ledger_MainState : ULValue ContractState
→ balances [[ addr ]] : ULValue uint256
→ user ^^ User_name : ULValue string

Learn more: ULValue Grammar

URValue (Right Value)

Definition:

Inductive URValueP : Type -> bool -> Type :=
    | URScalar : ... -> URValueP X false
    | URResult : ... -> URValueP X b
    | URState  : ... -> URValueP U false
    | URField  : ... -> URValueP (field_type f) b
    | URIndex  : ... -> URValueP V (bK || bM)
    | URLocalIndex : ... -> URValueP V false
    | URTuple : ... -> URValueP (XProd A B) (bA || bB)
    | UR3arn  : ... -> URValueP X (b1 || b2 || b3)
    | URFirst : ... -> URValueP A bA
    | URSecond : ... -> URValueP B bB
    | URUnMaybe: ... -> URValueP A b.

Type parameters:

• Type - Value type
• bool - Panic flag (false = cannot panic, true = may panic)

Represents:

• Literals - URScalar
• Monadic computations - URResult
• State access - URState
• Field access - URField
• Indexing - URIndex, URLocalIndex
• Tuples - URTuple, URFirst, URSecond
• Conditionals - UR3arn
• Optional unwrapping - URUnMaybe

Operations:

• Can be read from
• Cannot be written to
• Passed by value

Examples:

# 42 : URValue uint256 false       (* Literal *)
a + b : URValue uint256 false      (* Expression *)
foo() : URValue uint256 true       (* Function call *)
μ Ledger_MainState : URValue ContractState false
balances [[ addr ]] : URValue uint256 b

Learn more: URValue Grammar

Automatic Coercion

Ursus automatically converts ULValue to URValue when needed:

(* balance is ULValue, automatically coerced to URValue *)
::// total := balance + {100} .

Coercion rule: ULValue T → URValue T false

Type Mapping

Primitive Types

Complex Types

Mapping:

mapping K V := K -> option V

Optional:

optional T := option T

Arrays:

array T := list T

Records:

Record User := {
    user_id: uint256;
    balance: uint256
}.
(* Maps to Coq record with same structure *)

Contract State

State Record

The contract state is a Coq record containing all state variables:

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

State Access

Reading state:

get_balance : UExpression uint256 false :=
  fun s => Success (s.(balances), s)

Writing state:

set_balance (new_bal: uint256) : UExpression unit false :=
  fun s => Success (tt, s <| balances := new_bal |>)

State Transformations

State updates use Coq's record update syntax:

s <| field := new_value |>

Multiple updates:

s <| field1 := value1 |>
  <| field2 := value2 |>

Expression Semantics

Literals

Numeric literals:

{42} : URValue uint256 false
(* Semantics: λs. Success (42, s) *)

Boolean literals:

@true : URValue boolean false
(* Semantics: λs. Success (true, s) *)

Operators

Arithmetic:

a + b : URValue uint256 b
(* Semantics:
   do va <- eval a;
      vb <- eval b;
      return (va + vb)
*)

Comparison:

a < b : URValue boolean b
(* Semantics:
   do va <- eval a;
      vb <- eval b;
      return (va <? vb)
*)

Assignment

x := e : UExpression unit b
(* Semantics:
   do v <- eval e;
      write_location x v
*)

Control Flow

Conditional

if c then e1 else e2 : UExpression A b
(* Semantics:
   do vc <- eval c;
      if vc then eval e1 else eval e2
*)

Loops

While loop:

while c do body : UExpression unit true
(* Semantics: Fixed-point iteration with termination check *)

For loop:

for i in range do body : UExpression unit true
(* Semantics: Bounded iteration over range *)

Function Calls

Internal Calls

f(arg1, arg2) : UExpression RetType b
(* Semantics: Direct function application *)

External Calls

send Interface.Method(args) => target with params
(* Semantics: Message construction and dispatch *)

Error Handling

Panic Flag

The boolean parameter b in UExpression A b indicates panic possibility:

• false - Cannot panic (total function)
• true - May panic (partial function)

Type safety:

(* OK: Combining non-panicking expressions *)
e1 : UExpression A false
e2 : UExpression B false
e1 >> e2 : UExpression B false

(* Panicking propagates *)
e1 : UExpression A true
e2 : UExpression B false
e1 >> e2 : UExpression B true

Exit and Require

Exit:

exit_ code : UExpression A true
(* Semantics: λs. Error code *)

Require:

require_ condition : UExpression unit true
(* Semantics:
   if condition then Success (tt, s)
   else Error default_error_code
*)

Verification Support

Hoare Logic

Ursus supports Hoare-style reasoning:

{{ P }}  (* Precondition *)
  code
{{ Q }}  (* Postcondition *)

Example:

{{ balance >= amount }}
  balance := balance - amount
{{ balance_old = balance + amount }}

Invariants

Contract invariants can be expressed and proven:

Definition total_supply_invariant (s: ContractState) : Prop :=
  s.(totalSupply) = sum_balances s.(balances).

Theorem transfer_preserves_invariant:
  forall s s' from to amount,
    total_supply_invariant s ->
    exec_transfer from to amount s = Some s' ->
    total_supply_invariant s'.

Code Generation

Extraction Process

1. Monadic code → Imperative code
2. UExpression → Statements
3. State monad → State mutations

Example transformation:

(* Ursus/Coq *)
do x <- read_balance;
   write_balance (x + 1)

(* Generated Solidity *)
uint256 x = balance;
balance = x + 1;

Target Languages

• Solidity - Ethereum/EVM
• C++ - TON/TVM
• Rust - Various platforms

See Also

• Custom Grammar - Syntax extensions
• Notations - Notation definitions
• Verification - Proving properties
• Writing Functions - Practical usage