Execution Semantics

⚠️ Work in Progress: This section is under development.

This chapter covers the execution semantics of Ursus contracts.

Topics to be Covered

Execution Model

• State transitions
• Message handling
• Call stack
• Gas consumption

Semantics

• Operational semantics
• Denotational semantics
• Execution traces

State Management

• State reads
• State writes
• State rollback
• State persistence

Error Handling

• Exceptions
• Reverts
• Panics
• Error propagation

Understanding Execution

Execution Steps

1. Message reception
2. State loading
3. Function execution
4. State updates
5. Return value

Gas Model

• Gas costs
• Gas limits
• Out-of-gas errors

Coming Soon

This section will include:

• Formal semantics
• Execution examples
• Trace analysis
• Gas analysis

See Also

• Direct Proofs - Previous step
• Multi-Contract Systems - Next step
• Verification Principles - Verification basics