Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Core Grammar: URValue and ULValue

This section explains the core grammar of Ursus, focusing on the inductive types that define right values (URValue) and left values (ULValue).

Overview

Ursus's grammar is built on three fundamental inductive types defined in UrsusCore.v:

  1. URValueP - Right values (expressions that produce values)
  2. ULValueP - Left values (locations that can be assigned to)
  3. UExpressionP - Statements and control flow

These types form a custom grammar that extends Coq's syntax to support smart contract programming.

URValueP: Right Value Grammar

Definition

Inductive URValueP : Type -> bool -> Type := 
    | URScalar : forall {X}, X -> URValueP X false
    | URResult : forall {b X}, LedgerT (ControlResultP X b) -> URValueP X b
    | URState  : forall {U} {f: LedgerFields}`{EmbeddedType (field_type f) U}, 
                 URValueP U false               
    | URField  : forall {b} {U:Type} {FU:Set} (f:FU)`{PruvendoRecord U FU}, 
                 URValueP U b -> URValueP (field_type f) b
    | URIndex  : forall {bK bM} {K C V} (rk: URValueP K bK) (lv: URValueP C bM) 
                 `{Container K C V} `{XBoolEquable XBool K}`{XDefault V}, 
                 URValueP V (bK || bM)
    | URLocalIndex : forall {K C V} (k: K) (lv: URValueP C false) 
                     `{ContainerLocal K C V} `{XBoolEquable XBool K}`{XDefault V}, 
                     URValueP V false
    | URTuple : forall {A bA B bB}, URValueP A bA -> URValueP B bB -> 
                URValueP (XProd A B) (bA || bB)
    | UR3arn  : forall {b1 b2 b3 X}, URValueP XBool b1 -> URValueP X b2 -> 
                URValueP X b3 -> URValueP X (b1 || b2 || b3)
    | URFirst : forall {A B bA}, URValueP (XProd A B) bA -> URValueP A bA
    | URSecond : forall {A B bB}, URValueP (XProd A B) bB -> URValueP B bB
    | URUnMaybe: forall {A}`{XDefault A} {b}, URValueP (XMaybe A) b -> URValueP A b.

Type Parameters

  • First parameter (Type) - The value type (e.g., uint256, address)
  • Second parameter (bool) - Panic flag:
    • false - Cannot panic (pure computation)
    • true - May panic (can fail at runtime)

Constructors

URScalar - Literal Values

URScalar : forall {X}, X -> URValueP X false

Purpose: Embed Coq values as Ursus literals

Notation: # e

Examples:

# 42 : URValue uint256 false
# true : URValue boolean false
# "hello" : URValue string false

Panic flag: Always false (literals never panic)

URResult - Monadic Computations

URResult : forall {b X}, LedgerT (ControlResultP X b) -> URValueP X b

Purpose: Wrap monadic computations (function calls, state access)

Examples:

URResult (balanceOf(addr)) : URValue uint256 true
URResult (pure_function(x)) : URValue uint256 false

Panic flag: Inherited from the computation

URState - State Variable Access

URState : forall {U} {f: LedgerFields}`{EmbeddedType (field_type f) U}, 
          URValueP U false

Purpose: Access contract state variables

Notation: μ e

Examples:

μ Ledger_MainState : URValue ContractState false

Panic flag: Always false (state access is pure)

URField - Record Field Access

URField : forall {b} {U:Type} {FU:Set} (f:FU)`{PruvendoRecord U FU}, 
          URValueP U b -> URValueP (field_type f) b

Purpose: Access fields of records/structs

Notation: r ^^ f

Examples:

user ^^ User_balance : URValue uint256 b
(μ Ledger_MainState) ^^ Contract_totalSupply : URValue uint256 false

Panic flag: Inherited from the record expression

URIndex - Mapping/Array Indexing

URIndex : forall {bK bM} {K C V} (rk: URValueP K bK) (lv: URValueP C bM) 
          `{Container K C V} `{XBoolEquable XBool K}`{XDefault V}, 
          URValueP V (bK || bM)

Purpose: Index into mappings, arrays, or other containers

Notation: m [[ i ]]

Examples:

balances [[ addr ]] : URValue uint256 (b_addr || b_balances)
array [[ {0} ]] : URValue uint256 b_array

Panic flag: bK || bM (panics if either key or container can panic)

Type classes:

  • Container K C V - C is a container with keys K and values V
  • XBoolEquable XBool K - Keys are comparable
  • XDefault V - Values have a default (for missing keys)

URLocalIndex - Static Indexing

URLocalIndex : forall {K C V} (k: K) (lv: URValueP C false) 
               `{ContainerLocal K C V} `{XBoolEquable XBool K}`{XDefault V}, 
               URValueP V false

Purpose: Index with a compile-time constant key

Notation: m [[_ i _]]

Examples:

local_map [[_ addr_constant _]] : URValue uint256 false

Panic flag: Always false (static indexing is safe)

Difference from URIndex: Key is a Coq value, not an URValue

URTuple - Tuple Construction

URTuple : forall {A bA B bB}, URValueP A bA -> URValueP B bB -> 
          URValueP (XProd A B) (bA || bB)

Purpose: Create pairs/tuples

Examples:

URTuple (# 42) (# "hello") : URValue (uint256 # string) false

Panic flag: bA || bB (panics if either component can panic)

UR3arn - Ternary Operator

UR3arn : forall {b1 b2 b3 X}, URValueP XBool b1 -> URValueP X b2 -> 
         URValueP X b3 -> URValueP X (b1 || b2 || b3)

Purpose: Conditional expression (ternary ? :)

Examples:

UR3arn condition then_value else_value : URValue X (b1 || b2 || b3)

Panic flag: b1 || b2 || b3 (panics if any branch can panic)

URFirst / URSecond - Tuple Projection

URFirst : forall {A B bA}, URValueP (XProd A B) bA -> URValueP A bA
URSecond : forall {A B bB}, URValueP (XProd A B) bB -> URValueP B bB

Purpose: Extract components from tuples

Examples:

URFirst pair : URValue A b
URSecond pair : URValue B b

Panic flag: Inherited from the tuple

URUnMaybe - Optional Unwrapping

URUnMaybe: forall {A}`{XDefault A} {b}, URValueP (XMaybe A) b -> URValueP A b

Purpose: Unwrap optional values (with default on None)

Examples:

URUnMaybe maybe_value : URValue A b

Panic flag: Inherited from the optional value

Type class: XDefault A - Type A must have a default value

See Also