System Context (sys::)
The sys:: namespace describes the execution environment for the current
route (time, self address, balance, and related host fields). Values are
available in route actions, where clauses, macros, and member transforms —
not in pure fn or pure routes.
Fields commonly used on EVM
| Field | Description | Typical EVM lowering | Lean |
|---|---|---|---|
sys::now / sys::timestamp | Block / host timestamp | block.timestamp | yes |
sys::block_number | Block number | block.number | yes |
sys::chainid | Chain id | block.chainid | yes |
sys::address | This entity’s address | address(this) | yes |
sys::balance | This entity’s native balance | address(this).balance | yes |
sys::coinbase | Block coinbase | block.coinbase | — |
sys::basefee | Block base fee | block.basefee | — |
sys::blobbasefee | Blob base fee (EIP-4844) | block.blobbasefee | — |
sys::prevrandao | Block randomness | block.prevrandao | — |
sys::gas_left | Remaining gas | gasleft() | — |
sys::origin | tx.origin (use sparingly) | tx.origin | — |
sys::gasprice | Transaction gas price | tx.gasprice | — |
Fields marked “—” are EVM-only: the Lean model has no counterpart, and they are rejected when compiling for Lean.
For property / invariant ctx blocks, the validated context names are the portable subset: msg::{sender,value} and sys::{now,timestamp,chainid,block_number,balance} (T20).
Time guards
routes {
claim()
where (sys::now >= m_unlock_time) : throw TooEarly()
=> [
~> msg::sender with { value: m_amount }
]
}
m_last_action: u64 {
in deposit() => sys::now
in withdraw(_) => sys::now
}
Own address and balance
routes {
sweep(to: address) => [
~> to with { value: sys::balance }
]
}
Prefer sys::balance for “this entity’s balance.” Use evm::balance(addr) when you need another account’s balance on EVM (see EVM Intrinsics).
Not for pure code
pure fn and pure routes cannot read sys::* (or msg::*) — those namespaces are impure by definition.