AZ-013 — BVM Bytecode Format and Opcode Tables v1

Status

Acest document definește formatul exact al bytecode-ului pentru BVM (Bounded Virtual Machine) din ATLAS ZERO.

AZ-005 a stabilit principiile:

limbaj tipat,
bounded execution,
explicit effects,
host interface controlat,
static analyzability.

AZ-013 fixează forma executabilă exactă:

cum este serializat un modul BVM,
ce secțiuni conține,
ce opcode-uri există,
cum sunt codate,
ce efect au pe stack și memorie,
cât costă în exec units,
ce verificări statice trebuie aplicate înainte de deploy și înainte de execuție.

Acest document se bazează pe:

AZ-002 până la AZ-012, cu accent direct pe AZ-005 și AZ-012.

Termeni:

MUST = obligatoriu
MUST NOT = interzis
SHOULD = recomandat puternic
MAY = opțional

1. Obiectiv

AZ-013 răspunde la 10 întrebări precise:

Cum arată fizic un modul BVM?
Ce secțiuni sunt obligatorii?
Cum se codifică funcțiile, tipurile și constantele?
Ce model de operand și stack există?
Ce opcode-uri sunt permise în v1?
Care este efectul exact al fiecărui opcode?
Cum sunt măsurate exec units?
Ce instrucțiuni sunt interzise?
Cum se verifică static bytecode-ul?
Cum se obține un execution result canonical?

2. Principii de format

2.1 Canonical executable format

Un modul BVM MUST avea o formă binară canonică unică. Aceeași structură logică MUST produce același code_hash.

2.2 Minimal instruction set

Setul de opcode-uri SHOULD rămâne mic, explicit și analizabil.

2.3 Typed stack machine

BVM v1 este o mașină de tip typed stack machine cu:

operand stack bounded,
locals tipați,
memorie liniară bounded,
host calls explicite,
fără pointeri arbitrar accesibili.

2.4 No semantic ambiguity

Niciun opcode MUST NOT avea semantică dependentă de:

arhitectura CPU,
endian local,
floating point mode,
optimizări de compilator,
scheduler concurent.

3. High-level module structure

3.1 Bytecode container

Un modul BVM canonical are forma:

BvmModule {
  magic
  format_version_major
  format_version_minor
  module_flags
  section_count
  section_table
  sections...
}

3.2 magic

Valoare fixă:

0x41 0x5A 0x42 0x56

ASCII: AZBV

3.3 Versioning

format_version_major
format_version_minor

Bytecode v1 MUST fi acceptat doar de runtime-uri compatibile explicit.

3.4 module_flags

Flags canonice, ex:

deterministic_required
no_dynamic_linking
no_external_calls
manifest_present
debug_info_present

Flag-urile MUST fi interpretate identic de toate nodurile conforme.

4. Section table

4.1 Structure

Section table MUST lista secțiunile în ordine canonică:

SectionEntry {
  section_id: uint16
  offset: uint32
  length: uint32
  flags: uint16
}

4.2 Canonical ordering

Secțiunile MUST apărea în ordine strictă crescătoare după section_id. Offset-urile MUST fi strict ne-supravapuse și în interiorul blob-ului.

4.3 Unknown sections

BVM v1 MUST reject secțiuni necunoscute în spațiul obligatoriu de interpretare. Secțiuni opționale extensibile MAY exista doar prin registry/versioning clar.

5. Required sections

5.1 Mandatory sections in v1

Un modul executabil v1 MUST conține:

SEC_MODULE_META
SEC_TYPE_TABLE
SEC_CONST_POOL
SEC_FUNC_SIG_TABLE
SEC_FUNC_BODY_TABLE
SEC_EXPORT_TABLE
SEC_STORAGE_SCHEMA
SEC_EFFECT_TABLE
SEC_STATIC_MANIFEST

5.2 Optional sections in v1

Poate conține:

SEC_DEBUG_INFO
SEC_SOURCE_MAP
SEC_DOC_HASHES

Secțiunile opționale MUST NOT afecta consensul.

6. Section IDs

6.1 Canonical IDs

0x0001 = SEC_MODULE_META
0x0002 = SEC_TYPE_TABLE
0x0003 = SEC_CONST_POOL
0x0004 = SEC_FUNC_SIG_TABLE
0x0005 = SEC_FUNC_BODY_TABLE
0x0006 = SEC_EXPORT_TABLE
0x0007 = SEC_STORAGE_SCHEMA
0x0008 = SEC_EFFECT_TABLE
0x0009 = SEC_STATIC_MANIFEST
0x000A = SEC_DEBUG_INFO
0x000B = SEC_SOURCE_MAP
0x000C = SEC_DOC_HASHES

6.2 Rule

No aliasing of section IDs is allowed.

7. SEC_MODULE_META

7.1 Purpose

Descrie metadatele modulului.

7.2 Structure

ModuleMeta {
  language_id
  language_version_major
  language_version_minor
  compiler_id
  compiler_version_major
  compiler_version_minor
  source_hash: hash32
  abi_hash: hash32
  build_flags_hash: hash32
}

7.3 Rule

Aceste câmpuri MUST exista și MUST fi incluse în code_hash derivat deoarece blob-ul întreg este canonical.

8. SEC_TYPE_TABLE

8.1 Purpose

Conține toate tipurile folosite de modul.

8.2 Type kinds

Tipurile v1 suportate:

primitive
struct
enum
fixed_array
bounded_vec
optional
result

8.3 Type table structure

TypeTable {
  type_count: uint32
  entries: [TypeEntry]
}

8.4 Primitive type codes

0x01 = U8
0x02 = U16
0x03 = U32
0x04 = U64
0x05 = U128
0x06 = I8
0x07 = I16
0x08 = I32
0x09 = I64
0x0A = BOOL
0x0B = HASH32
0x0C = RATIO
0x0D = POLICY_REF
0x0E = CELL_REF
0x0F = WITNESS_REF
0x10 = MACHINE_ID
0x11 = ASSET_ID
0x12 = TIMESTAMP_MS
0x13 = EPOCH_INDEX
0x14 = BYTES_FIXED

8.5 Composite type entry

TypeEntry {
  type_kind: uint8
  flags: uint8
  payload_len: uint16
  payload: bytes
}

8.6 Rule

Type entries MUST be canonical and index-addressed by position.

9. SEC_CONST_POOL

9.1 Purpose

Conține constantele module-level.

9.2 Allowed constants

integers
booleans
fixed bytes
hash32
ratio
canonical serialized small structs/enums

9.3 Forbidden constants

large opaque dynamic blobs فوق limitele v1
code pointers
host object handles

9.4 Structure

ConstPool {
  const_count: uint32
  entries: [ConstEntry]
}

ConstEntry {
  type_idx: uint32
  value_len: uint32
  value_bytes: bytes
}

10. SEC_FUNC_SIG_TABLE

10.1 Purpose

Definește semnăturile funcțiilor interne și exportate.

10.2 Structure

FuncSigTable {
  func_count: uint32
  entries: [FuncSigEntry]
}

FuncSigEntry {
  func_idx: uint32
  flags: uint16
  param_type_count: uint16
  param_type_idxs: [uint32]
  return_type_count: uint16
  return_type_idxs: [uint32]
  local_type_count: uint16
  local_type_idxs: [uint32]
  max_stack_words: uint32
  max_call_depth: uint16
}

10.3 Rule

func_idx MUST align with function bodies and export references.

11. SEC_FUNC_BODY_TABLE

11.1 Purpose

Conține corpurile executabile ale funcțiilor.

11.2 Structure

FuncBodyTable {
  body_count: uint32
  bodies: [FuncBody]
}

FuncBody {
  func_idx: uint32
  body_flags: uint16
  instruction_count: uint32
  code_len: uint32
  code_bytes: bytes
}

11.3 Rule

Instrucțiunile MUST fi decodabile liniar și consistent. Jump targets MUST referi offset-uri valide în interiorul corpului.

12. SEC_EXPORT_TABLE

12.1 Purpose

Mapează funcții interne la entry points exportate.

12.2 Structure

ExportTable {
  export_count: uint16
  entries: [ExportEntry]
}

ExportEntry {
  export_idx: uint16
  func_idx: uint32
  selector: hash32
  name_hash: hash32
  arg_schema_hash: hash32
  return_schema_hash: hash32?
  effect_signature_hash: hash32
  max_exec_units: uint64
  max_state_write_bytes: uint32
}

12.3 Rule

Selectorii MUST fi unici în tabelul de export.

13. SEC_STORAGE_SCHEMA

13.1 Purpose

Descrie schema stării persistente.

13.2 Structure

StorageSchemaSection {
  schema_hash: hash32
  root_type_idx: uint32
  state_bound_bytes: uint64
  write_path_count: uint32
  write_paths: [WritePathDescriptor]
}

WritePathDescriptor {
  path_id: uint32
  path_hash: hash32
  type_idx: uint32
  max_write_bytes: uint32
}

13.3 Rule

Orice STORE_STATE_PATH MUST referi un path_id valid din această secțiune.

14. SEC_EFFECT_TABLE

14.1 Purpose

Descrie efectele permise și upper bounds asociate.

14.2 Structure

EffectTable {
  effect_entry_count: uint16
  entries: [EffectEntry]
}

EffectEntry {
  func_idx: uint32
  effect_mask: uint64
  max_cells_consumed: uint32
  max_cells_created: uint32
  max_witness_emits: uint16
  max_state_write_bytes: uint32
  max_exec_units: uint64
}

14.3 Effect mask bits

Bit mapping v1:

bit 0  = READ_STATE
bit 1  = WRITE_STATE
bit 2  = READ_CELL
bit 3  = CONSUME_CELL
bit 4  = CREATE_CELL
bit 5  = READ_WITNESS
bit 6  = EMIT_WITNESS
bit 7  = READ_PROOF
bit 8  = LOCK_VALUE
bit 9  = UNLOCK_VALUE
bit 10 = BURN_VALUE
bit 11 = HALT_SELF
bit 12 = EMIT_LOGICAL_EVENT

15. SEC_STATIC_MANIFEST

15.1 Purpose

Conține rezultatul analizei statice obligatorii.

15.2 Structure

StaticManifest {
  analysis_version_major
  analysis_version_minor
  forbidden_pattern_flags: uint64
  max_linear_memory_bytes: uint32
  max_iter_steps: uint32
  max_exec_units_upper_bound: uint64
  verification_summary_hash: hash32
  proof_of_well_typedness_hash: hash32
}

15.3 Rule

Dacă manifestul nu este consistent cu restul modulului, deploy-ul MUST fail.

16. Instruction encoding model

16.1 Instruction format

Fiecare instrucțiune are formatul general:

Instruction {
  opcode: uint8
  operand_len: uint8
  operands: bytes[operand_len]
}

16.2 Canonical decoding

Operand parsing MUST depinde doar de opcode și operand_len. Unknown opcodes MUST fail verification.

16.3 No prefixes in v1

BVM v1 SHOULD evita prefix/opcode extension chains complexe. Simplicitatea este preferată.

17. Stack model

17.1 Typed operand stack

Stack-ul conține valori tipate. Verifier-ul static MUST cunoaște tipul de pe fiecare poziție la fiecare program point.

17.2 Stack growth

Stack-ul nu poate depăși max_stack_words pentru funcția respectivă.

17.3 Word model

Un „word” BVM este o unitate logică de valoare tipată; implementarea internă MAY folosi alt layout, dar semantica MUST rămâne identică.

17.4 Trap

Orice stack underflow sau overflow MUST trap și invalida apelul.

18. Locals model

18.1 Typed locals

Local variables sunt declarate în semnătura funcției.

18.2 Access

Locals sunt accesați prin index. Index invalid MUST trap.

18.3 Initialization

Toți locals MUST avea stare inițială bine definită:

fie zero/default canonical pentru tip,
fie explicit setați înainte de citire, conform regulii verifier-ului.

BVM v1 SHOULD prefera „must be initialized before read” la nivel static.

19. Linear memory model

19.1 Optional but bounded

BVM v1 poate expune memorie liniară bounded.

19.2 Structure

Linear memory este un blob de bytes cu lungime maximă dată de manifest.

19.3 Access

Accesul se face doar prin opcode-uri standard:

MEM_LOAD
MEM_STORE
MEM_COPY
MEM_FILL

19.4 Trap

Orice acces out-of-bounds MUST trap.

20. Control flow model

20.1 Allowed control forms

fallthrough
conditional jump
unconditional bounded jump
return
revert
abort

20.2 Disallowed

indirect jump arbitrar
computed goto nebounded
self-modifying target tables

20.3 Join points

Type verifier MUST validate stack compatibility at branch merge points.

21. Opcode families overview

BVM v1 definește aceste familii:

Constants and moves
Local access
Integer arithmetic
Comparison and boolean logic
Aggregate construction/access
Memory operations
Control flow
Internal function calls
Hash and canonical serialization helpers
State access
Cell/Witness/Proof host effects
Assertions and termination

22. Opcode registry v1

22.1 Canonical assignment

0x01 CONST_U8
0x02 CONST_U16
0x03 CONST_U32
0x04 CONST_U64
0x05 CONST_U128
0x06 CONST_I32
0x07 CONST_I64
0x08 CONST_BOOL
0x09 CONST_POOL_REF

0x10 MOVE_TOP
0x11 DUP
0x12 DROP
0x13 SWAP

0x20 LOAD_LOCAL
0x21 STORE_LOCAL

0x30 ADD_U
0x31 SUB_U
0x32 MUL_U
0x33 DIV_U
0x34 MOD_U
0x35 ADD_I
0x36 SUB_I
0x37 MUL_I
0x38 DIV_I
0x39 NEG_I
0x3A CHECKED_CAST
0x3B WRAP_ADD_U
0x3C WRAP_SUB_U

0x40 EQ
0x41 NEQ
0x42 LT_U
0x43 LTE_U
0x44 GT_U
0x45 GTE_U
0x46 LT_I
0x47 LTE_I
0x48 GT_I
0x49 GTE_I
0x4A AND
0x4B OR
0x4C NOT
0x4D IS_NONE
0x4E IS_ERR

0x50 PACK_STRUCT
0x51 UNPACK_STRUCT
0x52 LOAD_FIELD
0x53 SET_FIELD
0x54 PACK_ENUM
0x55 UNPACK_ENUM
0x56 ARRAY_NEW_FIXED
0x57 ARRAY_GET
0x58 ARRAY_SET
0x59 BVEC_PUSH
0x5A BVEC_GET
0x5B BVEC_SET
0x5C BVEC_LEN

0x60 MEM_LOAD
0x61 MEM_STORE
0x62 MEM_COPY
0x63 MEM_FILL

0x70 JUMP
0x71 JUMP_IF_TRUE
0x72 JUMP_IF_FALSE
0x73 RETURN
0x74 REVERT
0x75 ABORT
0x76 ASSERT

0x80 CALL_INTERNAL

0x90 HASH_BLAKE3_32
0x91 HASH_SHA256
0x92 SERIALIZE_CANONICAL
0x93 DESERIALIZE_CANONICAL
0x94 COMPUTE_RATIO
0x95 NORMALIZE_RATIO

0xA0 HOST_READ_STATE
0xA1 HOST_WRITE_STATE
0xA2 HOST_READ_CELL
0xA3 HOST_CONSUME_CELL
0xA4 HOST_CREATE_CELL
0xA5 HOST_READ_WITNESS
0xA6 HOST_EMIT_WITNESS
0xA7 HOST_READ_PROOF
0xA8 HOST_GET_PROTOCOL_PARAM
0xA9 HOST_GET_CURRENT_EPOCH
0xAA HOST_GET_MACHINE_METADATA
0xAB HOST_EMIT_LOGICAL_EVENT
0xAC HOST_HALT_SELF

22.2 Reserved ranges

0xB0-0xCF reserved for future bounded extensions
0xD0-0xEF reserved for experimental non-mainnet families
0xF0-0xFF permanently invalid in v1

23. Constants and moves

23.1 CONST_U8 ... CONST_BOOL

Push constantă imediată pe stack.

Operands

CONST_U8: 1 byte
CONST_U16: 2 bytes big-endian
CONST_U32: 4 bytes
CONST_U64: 8 bytes
CONST_U128: 16 bytes
CONST_I32: 4 bytes
CONST_I64: 8 bytes
CONST_BOOL: 1 byte (0x00 or 0x01)

Stack effect

[] -> [value]

Exec cost

Base cost:

tiny immediate: 1 unit
64-bit: 2 units
128-bit: 3 units

23.2 CONST_POOL_REF

Push constantă din const pool.

Operands

const_idx:uint32

Stack effect

[] -> [const_value]

Cost

2 units + small decode overhead

23.3 MOVE_TOP

Identity move semantic pentru optimizare canonicală limitată. SHOULD rarely be emitted.

Stack effect

[a] -> [a]

Cost

1 unit

23.4 DUP

[a] -> [a, a]

Cost: 1 unit

23.5 DROP

[a] -> []

Cost: 1 unit

23.6 SWAP

[a, b] -> [b, a]

Cost: 1 unit

24. Local access opcodes

24.1 LOAD_LOCAL

Operands

local_idx:uint16

Stack effect

[] -> [local_value]

Cost

1 unit

24.2 STORE_LOCAL

Operands

local_idx:uint16

Stack effect

[value] -> []

Cost

1 unit

Rule

Type of value MUST match local declared type.

25. Unsigned arithmetic opcodes

25.1 ADD_U / SUB_U / MUL_U / DIV_U / MOD_U

Operands

arith_width:uint8 Allowed widths:

1 = 8-bit
2 = 16-bit
3 = 32-bit
4 = 64-bit
5 = 128-bit

Stack effect

[a, b] -> [result]

Semantics

checked arithmetic
overflow or underflow traps
division/mod by zero traps

Cost

add/sub: 2 units
mul: 4 units
div/mod: 6 units

25.2 WRAP_ADD_U / WRAP_SUB_U

Same widths. Wrapping semantics explicit. Should be used only when logic requires modular arithmetic.

Cost same as ADD_U/SUB_U.

26. Signed arithmetic opcodes

26.1 ADD_I / SUB_I / MUL_I / DIV_I / NEG_I

Operands

arith_width:uint8 Allowed widths:

3 = 32-bit
4 = 64-bit

Stack effects

binary ops: [a, b] -> [result]
NEG_I: [a] -> [result]

Semantics

Checked arithmetic. Overflow traps.

Cost

add/sub/neg: 2 units
mul: 4 units
div: 6 units

26.2 CHECKED_CAST

Operands

from_type:uint8, to_type:uint8

Stack effect

[value] -> [cast_value]

Semantics

Fails if cast would truncate or invalidate.

Cost: 2 units

27. Comparison and boolean opcodes

27.1 EQ / NEQ

Stack effect

[a, b] -> [bool]

Rule

Types MUST be comparable and equal. Structural equality for aggregates MUST be well-defined and canonical.

Cost: 2 units, plus proportional small cost for bounded aggregate width.

27.2 LT/LTE/GT/GTE

Unsigned and signed variants separate.

Stack effect

[a, b] -> [bool]

Cost: 2 units

27.3 AND / OR / NOT

Boolean only.

Stack effects

AND: [a, b] -> [bool]
OR: [a, b] -> [bool]
NOT: [a] -> [bool]

Cost: 1 unit

27.4 IS_NONE / IS_ERR

For optional<T> and result<T,E>.

Cost: 1 unit

28. Aggregate construction and access

28.1 PACK_STRUCT

Operands

type_idx:uint32

Stack effect

[field_1, ..., field_n] -> [struct]

Rule

Field count and field types MUST match schema.

Cost: 2 units + 1 per field

28.2 UNPACK_STRUCT

Operands

type_idx:uint32

Stack effect

[struct] -> [field_1, ..., field_n]

Cost: 2 units + 1 per field

28.3 LOAD_FIELD

Operands

field_idx:uint16

Stack effect

[struct] -> [field_value]

Cost: 2 units

28.4 SET_FIELD

Operands

field_idx:uint16

Stack effect

[struct, value] -> [new_struct]

Cost: 3 units

28.5 PACK_ENUM / UNPACK_ENUM

Operands

enum type idx
variant idx where relevant

Costs similar to struct packing/unpacking.

28.6 ARRAY_NEW_FIXED

Operands

elem_type_idx:uint32, len:uint16

Stack effect

[elem_1, ..., elem_n] -> [array]

Cost: 2 + n units

28.7 ARRAY_GET / ARRAY_SET

Stack effect

get: [array, idx] -> [elem]
set: [array, idx, elem] -> [new_array]

Bounds

Out-of-range MUST trap.

Costs:

get: 3 units
set: 4 units

28.8 BVEC_PUSH / BVEC_GET / BVEC_SET / BVEC_LEN

For bounded vectors only.

Rule

Push beyond declared max length MUST trap.

Costs:

push: 4 units
get: 3 units
set: 4 units
len: 1 unit

29. Memory opcodes

29.1 MEM_LOAD

Operands

width:uint8 Allowed widths: 1,2,4,8,16,32

Stack effect

[offset] -> [bytes_fixed<width>]

Cost

2 + width/4 units rounded up

29.2 MEM_STORE

Operands

width:uint8

Stack effect

[offset, value] -> []

Cost

2 + width/4 units

29.3 MEM_COPY

Stack effect

[dst, src, len] -> []

Rule

len MUST be bounded by memory size and static/dynamic checks.

Cost: 2 + len/8 units rounded

29.4 MEM_FILL

Stack effect

[dst, byte_value, len] -> []

Cost: 2 + len/8 units rounded

30. Control flow opcodes

30.1 JUMP

Operands

target_offset:uint32

Rule

Target MUST be valid instruction boundary.

Stack effect

unchanged

Cost: 1 unit

30.2 JUMP_IF_TRUE / JUMP_IF_FALSE

Stack effect

[bool] -> []

Cost: 1 unit

30.3 RETURN

Stack effect

[ret_1, ..., ret_n] -> function return

Cost: 1 unit

30.4 REVERT

Operands

status_code:uint32

Semantics

Controlled failure with no persistent state application.

Cost: 1 unit to execute; overall exec_units used until that point still count.

30.5 ABORT

Operands

status_code:uint32

Semantics

Fatal runtime abort. Equivalent to trap class in result model.

Cost: 1 unit

30.6 ASSERT

Operands

status_code:uint32

Stack effect

[bool] -> []

Rule

If bool=false, abort with status_code.

Cost: 1 unit

31. Internal call opcode

31.1 CALL_INTERNAL

Operands

func_idx:uint32

Stack effect

Consumes callee params, pushes callee returns.

Rule

func_idx must exist
static verifier must know exact callee signature
cumulative call depth MUST remain within bound
recursion cycles forbidden by verifier

Cost

2 units call overhead + callee body units

32. Hash and canonical serialization opcodes

32.1 HASH_BLAKE3_32

Stack effect

[bytes] -> [hash32]

Cost

base 4 + proportional per byte chunk

32.2 HASH_SHA256

Same pattern. V1 SHOULD select one primary hash family at protocol level; if both exist, semantics and allowed contexts MUST be explicit.

32.3 SERIALIZE_CANONICAL

Operands

type_idx:uint32

Stack effect

[typed_value] -> [bytes]

Rule

Must produce exact canonical serialization used by protocol rules.

Cost: base 3 + proportional to serialized size

32.4 DESERIALIZE_CANONICAL

Operands

type_idx:uint32

Stack effect

[bytes] -> [typed_value]

Rule

Non-canonical encoding MUST fail.

Cost: base 4 + proportional to size

32.5 COMPUTE_RATIO

Stack effect

[num, den] -> [ratio]

Rule

den != 0 or trap

32.6 NORMALIZE_RATIO

Stack effect

[ratio] -> [ratio]

Rule

Normalization semantics MUST be canonical if used.

33. Host interface opcodes

33.1 HOST_READ_STATE

Operands

path_id:uint32

Stack effect

[] -> [value]

Rule

Path must exist in storage schema. Read-only.

Cost

base 8 + proportional to value size class

33.2 HOST_WRITE_STATE

Operands

path_id:uint32

Stack effect

[value] -> []

Rule

path writable
value type matches schema
effect accumulator updated
write bytes counted

Cost

base 10 + proportional to write size

33.3 HOST_READ_CELL

Stack effect

[cell_ref] -> [cell_object_or_projection]

Rule

Visible shape returned MUST be standardized.

Cost: 10 units

33.4 HOST_CONSUME_CELL

Stack effect

[cell_ref] -> []

Rule

effect permission required
accumulator updated
validation layer rechecks legality

Cost: 12 units

33.5 HOST_CREATE_CELL

Stack effect

[cell_blob] -> [cell_id]

Rule

canonical cell validation
effect permission required
accumulator updated

Cost: 14 + proportional to object size

33.6 HOST_READ_WITNESS

Stack effect

[witness_ref] -> [witness_object_or_projection]

Cost: 10 units

33.7 HOST_EMIT_WITNESS

Stack effect

[witness_blob] -> [witness_id]

Rule:

canonical validation
effect permission required
accumulator updated

Cost: 14 + proportional size + proof linkage overhead if any

33.8 HOST_READ_PROOF

Stack effect

[proof_ref] -> [proof_object_or_projection]

Cost: 12 units + verifier preparation overhead

33.9 HOST_GET_PROTOCOL_PARAM

Operands

param_id:uint32

Stack effect

[] -> [param_value]

Cost: 4 units

33.10 HOST_GET_CURRENT_EPOCH

Stack effect

[] -> [epoch_index]

Cost: 2 units

33.11 HOST_GET_MACHINE_METADATA

Stack effect

[] -> [metadata_projection]

Cost: 4 units

33.12 HOST_EMIT_LOGICAL_EVENT

Stack effect

[event_blob] -> []

Rule:

bounded size
event goes to effect accumulator, not direct consensus state unless mapped later

Cost: 8 + proportional size

33.13 HOST_HALT_SELF

Stack effect

[] -> []

Rule:

only valid if machine tier/policy allows
effect accumulator updated with HALT_SELF bit

Cost: 6 units

34. Forbidden instruction patterns

34.1 Static verifier MUST reject:

unreachable invalid opcodes
recursive call cycles
jumps into middle of instruction
stack type mismatch at merge points
unbounded loops
local reads before guaranteed initialization
host calls inconsistent with effect signatures
impossible max_stack claims
body offsets outside section bounds
duplicated func_idx bodies

34.2 Runtime MUST trap if somehow encountered:

invalid opcode
malformed operand lengths
corrupted stack layout
out-of-bounds memory access
impossible type tag mismatch
exec units exhaustion

35. Static verification phases

35.1 Phase 1: structural

Checks:

module header
section presence/order
section bounds
no overlaps
valid counts/indexes

35.2 Phase 2: typing

Checks:

instruction operand types
stack evolution
locals types
return types
branch merge typing

35.3 Phase 3: control flow

Checks:

valid jump targets
no forbidden cycles
call graph acyclic
bounded loop proofs
max call depth

35.4 Phase 4: effects

Checks:

all host calls accounted
per-function effect subset matches effect table
no hidden state writes
export signatures align with effect declarations

35.5 Phase 5: bounds

Checks:

max stack
max memory
max iter steps
max exec upper bound
max writes and emits consistent with tables

36. Loop boundedness encoding

36.1 Need

BVM v1 allows loops only if bounded.

36.2 Model

Backward jumps MUST carry a loop-bound annotation via verifier metadata or structured form derivable from code.

36.3 Rule

A loop is admissible only if verifier can prove:

max_iterations <= declared bound
cumulative effect on exec units remains within manifest bound

36.4 Simplest approach

Reference compiler SHOULD emit structured loops compiled into patterns recognisable by verifier.

37. Exec units cost model

37.1 Principle

Every instruction has:

ExecCost = base_cost(opcode) + operand_dependent_cost + size_dependent_cost + host_side_cost

37.2 Integer arithmetic

Defined above in opcode sections.

37.3 Aggregate ops

Cost grows with bounded field count or size class.

37.4 Serialization / hashing

Cost grows with bytes processed, rounded in canonical chunk sizes.

37.5 Host operations

Highest cost family. Must reflect:

data access burden
validation burden
object construction burden
effect tracking burden

37.6 Determinism

Cost calculation MUST use integer arithmetic only.

38. Cost table summary

38.1 Minimal reference table

CONST small          = 1
CONST 64             = 2
CONST 128            = 3
LOAD/STORE_LOCAL     = 1
ADD/SUB              = 2
MUL                  = 4
DIV/MOD              = 6
COMPARE              = 2
BOOL op              = 1
PACK/UNPACK field    = 1 per field + base
ARRAY/vec get        = 3
ARRAY/vec set        = 4
JUMP                 = 1
ASSERT               = 1
CALL_INTERNAL        = 2 overhead
HASH base            = 4 + per-chunk
SERIALIZE base       = 3 + per-size
DESERIALIZE base     = 4 + per-size
HOST_GET_PARAM       = 4
HOST_READ_STATE      = 8 + size_class
HOST_WRITE_STATE     = 10 + size_class
HOST_READ_CELL       = 10
HOST_CONSUME_CELL    = 12
HOST_CREATE_CELL     = 14 + size_class
HOST_READ_WITNESS    = 10
HOST_EMIT_WITNESS    = 14 + size_class
HOST_READ_PROOF      = 12 + verifier prep
HOST_EMIT_EVENT      = 8 + size_class
HOST_HALT_SELF       = 6

38.2 Final protocol note

Numerical constants MAY be tuned by governance only through structural/economic process allowed by constitution. Semantic categories MUST remain stable.

39. Execution result canonical structure

39.1 Result object

BvmExecutionResult {
  version_major
  version_minor
  status_class
  status_code
  return_value_hash?
  next_state_root
  next_state_size_bytes
  effect_digest
  exec_units_used
  emitted_cell_ids
  emitted_witness_ids
  logical_event_root?
}

39.2 status_class

Allowed values:

SUCCESS
REVERT
ABORT
TRAP
VERIFICATION_FAILURE

39.3 Rule

Two compliant runtimes MUST produce the same canonical result for the same execution context.

40. Effect digest derivation

40.1 Need

Effects must be comparable cross-node.

40.2 Canonical effect digest

effect_digest = H("AZ:BVM_EFFECTS:" || canonical_effect_accumulator)

40.3 Effect accumulator components

Must include ordered canonical representations of:

read_set
write_set
consumed_cells
created_cells
read_witnesses
emitted_witnesses
proofs_used
logical_events
lock_delta
burn_delta
halt_self flag

41. Export call entry semantics

41.1 Invocation

A TX_MACHINE_CALL references an exported selector. Runtime resolves:

selector -> export entry
export entry -> func_idx
args decode via arg_schema_hash
execute with declared bounds

41.2 Rule

Any mismatch between external args and export signature MUST fail before runtime execution proceeds.

42. Bytecode verifier output

42.1 Canonical verifier result

BvmVerificationResult {
  status
  code_hash
  validated_section_hashes
  export_summary_hash
  effect_summary_hash
  max_exec_units_upper_bound
  verifier_error_code?
}

42.2 Status

VERIFIED
REJECTED

42.3 Rule

Deploy requires VERIFIED.

43. Deterministic replay requirements

43.1 For any executed machine call, a node SHOULD be able to reconstruct:

code hash
module blob
selected export
input args canonical bytes
prior state root and state blob
parameter state
attached object refs
execution result

43.2 Rule

If replay cannot reconstruct exact result, either implementation or archival discipline is broken.

44. Versioning and forward compatibility

44.1 Bytecode version separation

BVM runtimes MUST reject modules with unsupported major format version.

44.2 Minor version behavior

Minor version MAY add:

optional metadata
stricter verifier checks
new reserved opcodes only if compatibility rules say so

But MUST NOT silently change old opcode semantics.

44.3 Rule

Opcode semantics are version-bound, never inferred informally.

45. Test vector requirements for bytecode

45.1 AZ-011 integration

AZ-013 compliant implementations MUST provide vectors for:

module parsing
type verification
invalid jump targets
recursion rejection
opcode cost accounting
deterministic execution
effect digest equality
host call permission mismatch
memory bound traps

45.2 Cross-language requirement

At least two implementations SHOULD agree on:

verification result
execution result
exec units used

46. Security-sensitive anti-patterns

Implementers SHOULD avoid:

mapping opcodes to host-language dynamic behavior
using native integer overflow semantics accidentally
serializer shortcuts not matching canonical encoding
optimizing away effect accounting
parallel BVM execution that changes observed ordering or error class
different hash provider behavior hidden under same opcode
permissive verifier that “fixes” malformed bytecode
JIT fast path with semantics subtly different from interpreter
zero-cost host calls in local mode
hidden debug opcodes accepted in production

47. Reference implementation recommendations

47.1 Preferred architecture

Reference node SHOULD implement:

one simple interpreter first
one strict verifier
optional optimized backend only after conformance proven

47.2 Golden path

The interpreter SHOULD be treated as semantic oracle. Any optimized runtime MUST match it on AZ-011/AZ-013 suites.

48. Bytecode formula

BVM Bytecode = canonical module container + typed sections + bounded opcode set + deterministic cost model + explicit host effects + replayable execution result

49. Relația cu restul suitei

AZ-005 a definit principiile VM.
AZ-012 a definit locul VM în nod.
AZ-013 definește exact limbajul executabil pe care nodurile îl verifică și rulează.

Pe scurt: din acest punct, BVM nu mai este doar o idee de VM bounded. Este un format binar normativ.

50. Ce urmează

După AZ-013, documentul corect este:

AZ-014 — Fraud Proof and Slashing Evidence Formats

Acolo trebuie fixate:

formatele exacte ale dovezilor de fraudă,
dovada de double-signing,
dovada de notarizare incompatibilă,
dovezile de issuer/oracle fraud,
legătura dintre evidență, verdict și execuția slash-ului.

Închidere

O mașină virtuală nu devine interoperabilă când toată lumea este de acord în principiu ce ar trebui să facă. Devine interoperabilă când bytecode-ul, opcode-ul, costul și rezultatul sunt atât de precise încât două implementări independente nu mai au loc de interpretare.

Acolo începe execuția normativă reală.