ULValue Grammar: Left Values

This section explains the ULValue (Left Value) grammar - the subset of Ursus expressions that represent assignable locations.

Overview

ULValue represents locations in memory or storage that can be:

• Read from - Coerced to URValue
• Written to - Target of assignment
• Passed by reference - Modified by functions

Unlike URValue, ULValue has no panic flag because locations themselves don't panic (only operations on them can).

ULValueP Definition

Inductive ULValueP : Type -> Type := 
    | ULState  : forall {U} {f: LedgerFields}`{EmbeddedType (field_type f) U}, 
                 ULValueP U    
    | ULField  : forall {U:Type} {FU:Set} (f:FU)`{PruvendoRecord U FU}, 
                 ULValueP U -> ULValueP (field_type f)        
    | ULIndex  : forall {K C V} (rk: URValueP K false) (lv:ULValueP C) 
                 `{Container K C V}`{XBoolEquable XBool K}`{XDefault V},
                 ULValueP V
    | ULLocalIndex : forall {K C V} (k: K) (lv:ULValueP C) 
                     `{ContainerLocal K C V} `{XBoolEquable XBool K}`{XDefault V},
                     ULValueP V
    | ULTuple : forall {A B}, ULValueP A -> ULValueP B -> ULValueP (XProd A B) 
    | ULFirst : forall {A B}, ULValueP (XProd A B) -> ULValueP A
    | ULSecond : forall {A B}, ULValueP (XProd A B) -> ULValueP B
    | ULUnMaybe: forall {A}`{XDefault A}, ULValueP (XMaybe A) -> ULValueP A.

Type Parameters

• Single parameter (Type) - The type of value stored at this location
• No panic flag - Locations don't panic

Constructors

ULState - State Variable Location

ULState : forall {U} {f: LedgerFields}`{EmbeddedType (field_type f) U}, 
          ULValueP U

Purpose: Reference to contract state

Notation: → μ e

Examples:

→ μ Ledger_MainState : ULValue ContractState

Usage:

::// → μ Ledger_MainState := new_state .

ULField - Record Field Location

ULField : forall {U:Type} {FU:Set} (f:FU)`{PruvendoRecord U FU}, 
          ULValueP U -> ULValueP (field_type f)

Purpose: Reference to a field within a record

Notation: → r ^^ f

Examples:

→ (μ Ledger_MainState) ^^ Contract_totalSupply : ULValue uint256
→ user ^^ User_balance : ULValue uint256

Usage:

::// → (μ Ledger_MainState) ^^ Contract_totalSupply := {1000000} .

Chaining: Fields can be chained for nested records:

→ (μ Ledger_MainState) ^^ Contract_config ^^ Config_maxSupply

ULIndex - Mapping/Array Entry Location

ULIndex : forall {K C V} (rk: URValueP K false) (lv:ULValueP C) 
          `{Container K C V}`{XBoolEquable XBool K}`{XDefault V},
          ULValueP V

Purpose: Reference to a mapping or array entry

Notation: → m [[ i ]]

Examples:

→ balances [[ addr ]] : ULValue uint256
→ array [[ {0} ]] : ULValue uint256

Usage:

::// → balances [[ msg->sender ]] := {1000} .
::// → array [[ {0} ]] := {42} .

Key constraint: rk: URValueP K false - Key must not panic

Type classes:

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

ULLocalIndex - Static Entry Location

ULLocalIndex : forall {K C V} (k: K) (lv:ULValueP C) 
               `{ContainerLocal K C V} `{XBoolEquable XBool K}`{XDefault V},
               ULValueP V

Purpose: Reference to a mapping entry with compile-time constant key

Notation: → m [[_ i _]]

Examples:

→ local_map [[_ constant_addr _]] : ULValue uint256

Usage:

::// → local_map [[_ {0} _]] := {100} .

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

ULTuple - Tuple Location

ULTuple : forall {A B}, ULValueP A -> ULValueP B -> ULValueP (XProd A B)

Purpose: Reference to a tuple (pair of locations)

Examples:

ULTuple loc_a loc_b : ULValue (A # B)

Usage: Typically used with tuple unpacking:

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

ULFirst / ULSecond - Tuple Component Location

ULFirst : forall {A B}, ULValueP (XProd A B) -> ULValueP A
ULSecond : forall {A B}, ULValueP (XProd A B) -> ULValueP B

Purpose: Reference to first/second component of a tuple location

Examples:

ULFirst tuple_loc : ULValue A
ULSecond tuple_loc : ULValue B

Usage: Access components of tuple variables:

::// → ULFirst pair_var := {42} .

ULUnMaybe - Optional Location

ULUnMaybe: forall {A}`{XDefault A}, ULValueP (XMaybe A) -> ULValueP A

Purpose: Reference to the value inside an optional (with default on None)

Examples:

ULUnMaybe maybe_loc : ULValue A

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

ULValue vs URValue

Key Differences

Automatic Coercion

ULValue automatically coerces to URValue when needed:

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

Coercion rule: ULValue T → URValue T false

Notation Prefix

• ULValue: Uses → prefix in low-level notation
• URValue: No prefix (or # for scalars)

Examples:

→ μ Ledger_MainState        (* ULValue *)
μ Ledger_MainState          (* URValue *)

→ balances [[ addr ]]       (* ULValue *)
balances [[ addr ]]         (* URValue *)

Common Patterns

State Variable Assignment

::// → (μ Ledger_MainState) ^^ Contract_totalSupply := {1000000} .

Mapping Update

::// → balances [[ msg->sender ]] := balance + amount .

Nested Field Update

::// → (μ Ledger_MainState) ^^ Contract_user ^^ User_balance := {1000} .

Array Element Update

::// → array [[ index ]] := value .

See Also

• URValue Grammar - Right value grammar
• UExpression Grammar - Expression grammar
• Assignment Notations - Assignment syntax