[Reference Purpose, No Need for Review] Neo Virtual Machine (NeoVM) Specification #3811
Labels
Comments
Jim8y
added
Discussion
Neo Virtual Machine (NeoVM) Specification (N3 V3.8)Version: 1.0 This document is the a specification for the Neo Virtual Machine (NeoVM). It defines all required behaviors and constraints for compliant implementations. Executive SummaryThe Neo Virtual Machine (NeoVM) is a lightweight, cross-platform virtual machine optimized for blockchain smart contracts. This specification provides a complete and formal definition of the Neo VM architecture, semantics, and implementation requirements. Key FeaturesNeoVM offers the following powerful capabilities:
VM Architecture at a Glance
Comparison with Other Blockchain VMs
Key Differences from Previous VersionsNeoVM v3.0 introduces several improvements over previous versions:
Who Should Read This DocumentThis specification is intended for:
1. Introduction1.1 PurposeThis document defines the formal specification for the Neo Virtual Machine (NeoVM), the execution environment for smart contracts on the Neo blockchain. This specification establishes the normative requirements for implementing a compliant NeoVM. 1.2 ScopeThis specification covers:
1.3 ConformanceA conforming implementation of NeoVM MUST adhere to all REQUIRED behaviors specified in this document. Items marked as RECOMMENDED or OPTIONAL may be implemented at the discretion of the implementer. 1.4 Normative References
1.5 Terminology and ConventionsThe key words "MUST", "MUST NOT", "REQUIRED", "SHALL", "SHALL NOT", "SHOULD", "SHOULD NOT", "RECOMMENDED", "MAY", and "OPTIONAL" in this document are to be interpreted as described in RFC 2119. 1.5.1 Glossary of Key Terms
1.6 Formal NotationThis specification uses the following formal notation techniques to precisely define the behavior of the Neo VM: 1.6.1 Operational Semantics
Small-step operational semantics are used to formally specify state transitions in the VM. The general form is: Where:
1.6.2 Mathematical NotationThe following notation is used throughout the specification:
1.6.3 Functions and Predicates
1.7 Document OrganizationThis specification is organized into the following main sections:
Each section builds on previous ones, with cross-references provided where relevant. 2. Architecture2.1 Design PrinciplesThe NeoVM architecture adheres to the following principles:
2.2 System ArchitectureThe NeoVM architecture consists of the following component layers:
4.1.2 Instruction Set ArchitectureThe NeoVM instruction set is structured as follows: Figure 4.1: Instruction Set Architecture 4.2 Instruction TypesA conforming implementation MUST support the following instruction types: 4.2.1 Control Flow InstructionsControl flow instructions allow for conditional execution and looping.
4.2.2 Stack Manipulation InstructionsStack manipulation instructions allow for pushing, popping, and duplicating values on the stack.
4.2.3 Arithmetic InstructionsArithmetic instructions allow for basic arithmetic operations on the stack.
4.2.4 Static Field InstructionsStatic field instructions allow for loading and storing data in static fields.
4.2.5 Array InstructionsArray instructions allow for manipulating arrays on the stack.
4.2.6 Execution Flow InstructionsExecution flow instructions allow for controlling the execution flow of the VM.
4.2.7 Type Operations InstructionsType operations instructions allow for checking types and performing type conversions.
4.2.8 Slot InstructionsSlot instructions allow for accessing and manipulating slot values.
4.2.9 Stack Operations InstructionsStack operations instructions allow for manipulating local variables and arguments.
4.2.10 Array and Collection InstructionsArray and collection instructions allow for manipulating arrays, maps, and other collections.
4.2.11 Arithmetic InstructionsArithmetic instructions allow for performing arithmetic operations.
4.3 Instruction ExecutionThe NeoVM instruction execution model is as follows: Figure 2: Neo VM State Transition Diagram
2.4.2 State IndicatorsA compliant VM implementation MUST provide a mechanism to query the current execution state, which MUST return one of the enumerated state values defined above. 3. Type System3.1 Type System OverviewThe NeoVM type system provides the data types and operations required for smart contract execution. It is designed to balance expressiveness, safety, and determinism. 3.1.1 Design RequirementsThe NeoVM type system MUST:
3.1.2 Type System ArchitectureThe NeoVM type system is structured as follows: Figure 3.1: Type System Architecture 3.2 Stack Item TypesA conforming implementation MUST support the following fundamental data types, identified by their type code:
3.2.1 Type Hierarchy VisualizationThe following diagram illustrates the hierarchical relationship between Neo VM types: Figure 3.2: Neo VM Type Hierarchy In this hierarchical model:
3.2.2 Type Code AllocationThe type codes are allocated in specific ranges:
Type codes not explicitly defined in this specification are reserved for future use. 3.3 Stack Item InterfaceAll data types MUST implement a common interface with the following operations: 3.3.1 Required Operations
3.3.2 Stack Item Interface VisualizationFigure 3.3: Stack Item Interface Components 3.4 Type Conversion RulesA conforming implementation MUST apply the following rules when converting between types. 3.4.1 Type Conversion Visual ReferenceThe following diagram visualizes the permitted type conversions between Neo VM types: Figure 3.4: Type Conversion Relationships Diagram 3.4.2 Type Conversion ExamplesThe following table provides concrete examples of type conversions:
4. Execution Model4.1 Formal Execution Semantics
4.1.1 Transition RulesWhere:
4.1.2 VM State DefinitionThe state of the VM is formally represented as a tuple
Additionally, the complete VM state includes:
The full VM state transition is denoted as: Where 4.2 Formal Execution ModelA conforming implementation MUST implement the execution model as defined by the following formal transition systems: 4.2.1 Script Loading
4.2.2 Execution LifecycleThe execution lifecycle MUST proceed as follows:
4.2.3 Bytecode Execution ModelThe following diagram illustrates the bytecode execution model of the Neo VM: The diagram illustrates the complete bytecode execution flow in the Neo VM:
The execution process continues until the VM reaches either a HALT state (successful completion) or a FAULT state (execution error). 4.2.3.1 Stack-Based Execution FlowThe Neo VM uses a stack-based execution model where operations consume inputs from and push results to the evaluation stack. The following diagram illustrates this flow: This diagram illustrates the complete execution cycle in Neo VM:
The execute phase consists of three sub-steps:
The example shows an ADD instruction execution that:
This stack-based execution model ensures deterministic behavior across all Neo VM implementations because each instruction has a well-defined effect on the evaluation stack. 4.2.3.2 Common Stack OperationsThe following diagrams illustrate common stack operations in the Neo VM: 4.2.3.3 Operation Instruction Stack EffectsThe following diagrams illustrate how different types of instructions affect the stack: These visualizations provide a clear understanding of how stack operations work in the Neo VM, which is essential for implementers to correctly handle the evaluation stack during execution. 5. Instruction Set5.1 Instruction Categories5.1.1 Constants (0x00-0x20)Constants instructions allow for pushing constant values onto the stack.
5.1.2 Flow Control (0x21-0x41)Flow control instructions allow for controlling the execution flow of the VM.
5.1.3 Stack Operations (0x43-0x55)Stack operations instructions allow for manipulating the elements on the stack.
5.1.4 Slot Operations (0x56-0x87)Slot operations instructions allow for accessing and manipulating local variables, arguments, and static fields.
5.2 Constants and Push OperationsThe following operations push constant values onto the evaluation stack:
5.2.1 PUSHDATA EncodingPUSHDATA instructions MUST use the following encoding:
Where the length field specifies the number of data bytes that follow. 5.3 Flow Control OperationsFlow control operations modify the instruction pointer and control execution flow:
5.3.1 Jump Offset CalculationFor jump operations, the offset is calculated as follows:
5.3.2 TRY-CATCH-FINALLY StructureThe TRY/TRY_L instruction contains two offset operands:
ENDTRY/ENDTRY_L marks the end of a CATCH block with an offset to the end of the entire structure (after FINALLY if present). 5.3.3 Exception Handling Flow VisualizationThe following diagram illustrates the control flow during exception handling: The diagram illustrates the complete exception handling process in Neo VM:
Key points:
5.3.4 Formal Operational Semantics for Flow ControlThe following formal semantics define precisely how flow control operations transform the VM state:
Where:
5.3.4 Flow Control State Transition TableThe following table precisely defines the state transition for flow control operations:
Where:
These formal semantics ensure that flow control operations are implemented consistently across all Neo VM implementations. 5.3 Stack OperationsStack operations manipulate items on the evaluation stack without performing computation on their values:
5.3.1 Stack Operation RequirementsA conforming implementation MUST ensure the following for stack operations:
5.3.2 Formal Operational Semantics for Stack OperationsThe following formal semantics define precisely how stack operations transform the VM state: Where:
5.3.3 State Transition Table for Stack OperationsThe following table precisely defines the state transition for each stack operation:
This table and the formal semantics ensure deterministic behavior for all stack operations across all Neo VM implementations. 5.3.4 Stack Operation VisualizationThe following diagrams visually illustrate how common stack operations affect the evaluation stack: These visualizations illustrate how stack items are manipulated during key operations. The stack grows downward, with the top of the stack at the top of each diagram. In the PICK example, the value 2 indicates that the item at depth 2 (item C) should be copied to the top. In the ROLL example, the value 2 indicates that the item at depth 2 (item C) should be moved to the top. 5.4 Slot OperationsSlot operations manage local variables, arguments, and static fields:
5.4.1 Slot Operation RequirementsA conforming implementation MUST ensure the following for slot operations:
5.5 Type OperationsType operations check and convert between different types:
5.5.1 Type Operation RequirementsA conforming implementation MUST ensure the following for type operations:
5.6 Splice OperationsSplice operations manipulate buffers and strings:
5.6.1 Splice Operation RequirementsA conforming implementation MUST ensure the following for splice operations:
5.7 Comparison OperationsComparison operations compare values on the stack:
5.7.1 Comparison Operation RequirementsA conforming implementation MUST ensure the following for comparison operations:
5.8 Arithmetic OperationsArithmetic operations perform numeric calculations:
5.8.1 Arithmetic Operation RequirementsA conforming implementation MUST ensure the following for arithmetic operations:
5.8.2 Formal Operational Semantics for Arithmetic OperationsThe following formal semantics define precisely how arithmetic operations transform the VM state: Where:
5.8.3 Arithmetic State Transition TableThe following table precisely defines the state transition for arithmetic operations:
Where sign(x) returns:
These formal semantics ensure that arithmetic operations are implemented consistently across all Neo VM implementations. 5.9 Compound Type OperationsCompound type operations create and manipulate complex data structures:
5.9.1 Compound Type Operation RequirementsA conforming implementation MUST ensure the following for compound type operations:
5.9.2 Formal Operational Semantics for Compound Type OperationsThe following formal semantics define precisely how compound type operations transform the VM state: Where:
5.9.3 Reference Counting in Compound OperationsCompound type operations involve creating, copying, and modifying references to objects, requiring careful management of reference counts:
5.9.4 Compound Type State Transition TableThe following table precisely defines the state transitions for compound type operations:
Where:
These formal semantics ensure that compound type operations are implemented consistently across all Neo VM implementations, with proper reference counting to manage memory. 5.10 Control Flow OperationsControl flow operations manage the execution path of the VM:
5.10.1 Control Flow Operation RequirementsA conforming implementation MUST ensure the following for control flow operations:
6. Engine Limits and Restrictions6.1 Execution Engine LimitsA conforming implementation of the Neo VM MUST include a comprehensive set of limits to prevent resource abuse and ensure deterministic execution across different implementations. 6.1.1 Required Execution LimitsThe following limits MUST be enforced by all compliant Neo VM implementations:
6.1.2 Limit Enforcement RequirementsA conforming implementation MUST ensure the following for all execution limits:
6.2.2 Secure Execution Requirements
To be considered conformant with this specification, an implementation MUST:
7.2 Test VectorsImplementations SHOULD be validated against standard test vectors that verify:
7.3 Version CompatibilityImplementations SHOULD clearly indicate which version of the Neo VM specification they conform to. Future versions of this specification will include version numbers and change logs to track modifications. 8. Appendices8.1 Opcode Reference TableThe following table provides a comprehensive reference of all Neo VM opcodes:
8.2 Normative References
8.3 Security Considerations8.3.1 Deterministic ExecutionA conforming implementation MUST guarantee deterministic execution, ensuring that:
8.3.2 Resource IsolationA conforming implementation MUST provide resource isolation, ensuring that:
8.3.3 Exception Handling RequirementsA conforming implementation MUST implement exception handling that:
9. Conclusion9.1 Implementation GuidelinesTo ensure a successful Neo VM implementation, developers SHOULD:
9.2 Version InformationThis document is version 1.0 of the Neo VM Specification. The Neo VM described in this specification is exclusively for Neo N3. 9.3 Future DirectionsFuture versions of this specification may address:
This specification will continue to evolve based on community feedback and practical implementation experience. Implementers are encouraged to participate in the Neo ecosystem to help shape the future of the Neo VM. 10. InteroperabilityInteroperability defines how the Neo VM interfaces with external systems, particularly the Neo blockchain environment. 10.1 Interoperability ModelA conforming implementation MUST support the following interoperability features: 10.1.1 Interop Interface
10.2 System CallsSYSCALL is the primary mechanism for interoperability between the VM and the host environment. 10.2.1 SYSCALL Implementation Requirements
10.3 Standard Interoperability ServicesWhile specific interoperability services depend on the host environment, Neo blockchain implementations SHOULD provide the following standard service categories:
10.4 Interoperability RegistrationA conforming blockchain implementation MUST provide a mechanism to register interoperability services with the VM:
10.5 Cryptographic Operations in Neo N3Cryptographic operations are provided through the interoperability layer using the SYSCALL mechanism. This architectural approach offers greater flexibility and extensibility. 10.5.1 Cryptographic Service CallsCryptographic operations are accessed through the following system calls:
These services are invoked using the SYSCALL opcode (0x41) with the appropriate service identifier. 10.5.2 Example: Signature VerificationTo verify a signature in a Neo N3 smart contract: 11. Blockchain Integration11.1 ApplicationEngine RequirementsWhen integrating the Neo VM with a blockchain environment, implementations SHOULD provide an ApplicationEngine that extends the base ExecutionEngine with the following capabilities: 11.1.1 Smart Contract Execution
11.1.2 Blockchain Integration Services
11.2 Permission ModelA blockchain implementation of the Neo VM MUST implement a robust permission model:
12. References
13. AppendicesAppendix A: NeoVM Bytecode Reference// ... existing bytecode content ... Appendix B: Conformance ValidationB.1 Validation Test SuiteTo validate that an implementation conforms to this specification, a comprehensive test suite is available at https://github.com/neo-project/neo-vm-conformance. This test suite includes tests for:
B.2 Conformance Certification ProcessImplementations seeking conformance certification should follow this process:
B.3 Implementation VariationsThis specification acknowledges that implementations may vary in the following ways while still conforming to the specification:
Appendix C: Implementation GuidanceC.1 Strategy for New ImplementationsWhen implementing the Neo VM from scratch, the following strategy is RECOMMENDED:
C.2 Performance ConsiderationsImplementers should consider the following performance optimizations:
C.3 Common Implementation PitfallsImplementers should be aware of the following common pitfalls:
C.4 Example Implementation Patterns// Example reference counting implementation pattern
public class StackItem
{
private int _stackReferences = 0;
private int _fieldReferences = 0;
public void AddStackReference()
{
Interlocked.Increment(ref _stackReferences);
}
public void AddFieldReference()
{
Interlocked.Increment(ref _fieldReferences);
}
public void RemoveStackReference()
{
if (Interlocked.Decrement(ref _stackReferences) == 0 && _fieldReferences == 0)
Recycle();
}
public void RemoveFieldReference()
{
if (Interlocked.Decrement(ref _fieldReferences) == 0 && _stackReferences == 0)
Recycle();
}
protected virtual void Recycle()
{
// Release resources
}
}Appendix D: Glossary of TermsD.1 Core TerminologyArray: A compound type that stores a sequence of stack items indexed by integers starting from 0. Buffer: A stack item type that represents a mutable byte array with specialized operations. ByteString: A stack item type representing an immutable sequence of bytes. Context: An execution frame containing state for a script invocation Execution Engine: The primary component responsible for executing scripts, maintaining the invocation stack and VM state. Fault State: A VM state indicating that execution has terminated due to an error condition. Halt State: A VM state indicating that execution has completed successfully. Instruction: A single operation in the VM, consisting of an operation code and optional operand. Interoperability: The ability of the VM to interact with the host environment Invocation Stack: A stack data structure that maintains the ordered sequence of execution contexts. Map: A compound type that stores a collection of key-value pairs, where keys and values are stack items. Neo Executable Format (NEF): The binary format used to store Neo smart contracts for execution by the VM. Reference Counting: A memory management technique used to track references to objects and reclaim memory when no references remain. Script Container: An object that encapsulates a script to be executed by the VM. Stack Item: The basic unit of data in the VM, representing various types such as integers, booleans, strings, arrays, etc. Static Fields: Persistent storage accessible across multiple invocations of the same script. Struct: A compound type that stores a collection of stack items indexed by integers similar to an array, but with value semantics for assignments. System Call: A mechanism for the VM to call functions provided by the host environment. D.2 Formal Verification TerminologyAssertion: A logical statement that must be true at a specific point in the program. Invariant: A condition that holds true throughout the execution of a program or function. Operational Semantics: A formal system that describes how the execution of a program happens step by step. Precondition: A condition that must be true before a function is called for the function to behave correctly. Postcondition: A condition that must be true after a function completes execution, assuming its precondition was met. Safety Property: A property stating that "nothing bad happens" during execution. Liveness Property: A property stating that "something good eventually happens" during execution. State Transition: A change from one VM state to another as a result of executing an instruction. Type Safety: The property that operations are only performed on data of appropriate types, preventing type errors during execution. D.3 Blockchain-Specific TerminologyApplication Engine: An extension of the execution engine that integrates with a blockchain environment. Contract: A script deployed on the blockchain that can be invoked by transactions. Native Contract: A contract implemented directly in the blockchain runtime rather than in VM bytecode. Permission Flag: A flag that controls what operations a contract is allowed to perform. Storage Context: An identifier that determines where a contract can read and write persistent data. Witness: A proof that an account has authorized a specific operation. Appendix E: Bytecode Format ReferenceE.1 NEF File FormatThe Neo Executable Format (NEF) is the standard binary format for Neo smart contracts. A NEF file consists of the following sections:
The detailed structure is as follows:
E.2 Script Section EncodingThe script section of a NEF file contains the VM bytecode to be executed. The bytecode is encoded as follows:
E.3 Manifest FormatAccompanying the NEF file, a contract manifest provides metadata about the contract. The manifest is stored in JSON format and includes:
Example manifest structure: {
"name": "ExampleContract",
"groups": [],
"features": {
"storage": true,
"payable": false
},
"abi": {
"methods": [
{
"name": "main",
"parameters": [
{
"name": "operation",
"type": "String"
},
{
"name": "args",
"type": "Array"
}
],
"returntype": "Any"
}
],
"events": []
},
"permissions": [
{
"contract": "*",
"methods": "*"
}
],
"trusts": [],
"extra": null
} |
|
Move to wiki? |
once you enable a wikki for this repo |
Done |
|
This doc is a specification.
May need to distinguish between implementation and specification. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
No description provided.
The text was updated successfully, but these errors were encountered: