AZ-005 — Contract Language and Bounded Virtual Machine Specification v1

Status

Acest document definește limbajul de contracte și mașina virtuală pentru ATLAS ZERO.

Obiectivul nu este expresivitate maximă. Obiectivul este:

• determinism strict;
• execuție bounded;
• analiză statică puternică;
• efecte explicite;
• risc controlabil;
• auditabilitate pentru oameni, noduri și agenți.

Acest document se bazează pe:

• AZ-002 pentru obiecte canonice;
• AZ-003 pentru reguli de validare și tranziții;
• AZ-004 pentru consens și finalitate.

Termeni:

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

1. Obiectiv

Mașina virtuală ATLAS ZERO, numită în acest document BVM (Bounded Virtual Machine), trebuie să asigure:

1. aceeași intrare produce aceeași ieșire pe orice nod;
2. un contract nu poate consuma resurse neanunțate;
3. un contract nu poate produce efecte în afara suprafeței sale declarate;
4. fiecare apel poate fi limitat prin exec units, state bounds și effect bounds;
5. fiecare contract poate fi inspectat static înainte de deploy.

BVM nu este concepută ca mașină generală „codul poate face orice”. Este concepută ca mașină pentru logică financiară, coordonare, custodie limitată, guvernanță și agenți controlați.

2. Principiile de bază

2.1 Determinism absolut

Execuția contractelor MUST depinde doar de:

• bytecode-ul canonical;
• input-ul canonical;
• starea canonicală;
• witness/proof objects atașate;
• parametrii protocolului activi.

Execuția MUST NOT depinde de:

• timp local de sistem;
• ordine locală de mempool;
• numere pseudo-random neancorate;
• HTTP/network I/O;
• acces la disc local;
• concurență internă nedeterministă;
• floating point.

2.2 Boundedness

Orice contract MUST declara și respecta:

• state_bound_bytes
• effect_bound
• max_exec_units_per_call
• max_stack_words
• max_linear_memory_bytes
• max_iter_steps sau echivalent static
• loss_envelope

2.3 Explicit effects

Contractele MUST declara explicit ce pot face:

• citi stare;
• scrie stare;
• consuma Cells;
• crea Cells;
• emite Witness Records;
• bloca/debloca valoare;
• arde valoare dacă permis.

Nu există efecte implicite.

2.4 Static analyzability

Contractul deployat MUST putea fi analizat pentru:

• terminare bounded;
• tipuri valide;
• acces de memorie bounded;
• instrucțiuni permise;
• efecte potențiale;
• suprafața de permisiuni;
• upper bounds de cost.

3. Componentele sistemului de execuție

BVM are patru componente:

1. AZ-Lang — limbajul sursă de nivel înalt;
2. AZ-IR — reprezentare intermediară tipată și controlată;
3. BVM Bytecode — format executabil canonical;
4. BVM Runtime — executorul deterministic validat de noduri.

4. AZ-Lang

4.1 Natură

AZ-Lang este limbajul sursă recomandat pentru contracte. Este:

• strict tipat;
• fără pointeri arbitrar accesibili;
• fără recursivitate generală;
• fără alocare nelimitată;
• cu efecte declarate în semnătură;
• cu modele de date finite și validate.

4.2 Obiectiv

AZ-Lang SHOULD fie suficient pentru:

• escrow;
• vaults;
• rate limits;
• multi-party approvals;
• auctions simple;
• lending bounded;
• AMM limitate;
• orchestration de agenți;
• treasury logic.

Nu este destinat pentru:

• interpreți generici;
• mașini Turing-complete nebounded;
• simulări arbitrare grele;
• ML on-chain;
• parsing arbitrar al inputurilor externe necanonice.

4.3 Stil semantic

Orice funcție expusă MUST declara:

• ce argumente primește;
• ce state reads face;
• ce state writes poate face;
• ce obiecte externe referă;
• ce efecte produce;
• ce bounds consumă.

Exemplu conceptual:

fn release_escrow(input: ReleaseInput)
  reads { contract_state, witness(approval), cell(lock_cell) }
  writes { contract_state }
  effects { consume_cell, emit_cell, emit_witness }
  bounds { exec<=12000, writes<=256, emits<=2 }

5. Subsetul semantic permis

5.1 Tipuri primitive

BVM v1 SHOULD suporta:

• u8, u16, u32, u64, u128
• i8, i16, i32, i64
• bool
• bytes<N> pentru N finit
• hash32
• ratio
• policy_ref
• cell_ref
• witness_ref
• machine_id
• asset_id
• timestamp_ms
• epoch_index

5.2 Tipuri compuse

Suportate:

• struct
• enum finit
• fixed_array<T, N>
• bounded_vec<T, N>
• optional<T>
• result<T, E>

5.3 Tipuri interzise în v1

• pointeri raw
• obiecte self-modifying
• dynamic map nelimitat
• string arbitrar nebounded
• reflection generală
• closures arbitrare
• generatori/co-routines
• float / double

6. Modelul de efecte

6.1 Efecte de bază

Fiecare funcție compilată are un Effect Signature.

Setul minim de efecte:

• READ_STATE
• WRITE_STATE
• READ_CELL
• CONSUME_CELL
• CREATE_CELL
• READ_WITNESS
• EMIT_WITNESS
• READ_PROOF
• LOCK_VALUE
• UNLOCK_VALUE
• BURN_VALUE
• HALT_SELF
• EMIT_LOGICAL_EVENT

6.2 Reguli

1. O funcție MUST NOT produce efect în afara semnăturii declarate.
2. Efectele reale MUST fi subset al permission_surface al mașinii.
3. Numărul și volumul efectelor MUST respecta effect_bound.
4. Orice încercare de efect nedeclarat este trap semantic și invalidează apelul.

6.3 Logical events

EMIT_LOGICAL_EVENT nu modifică direct Value Layer. Este folosit pentru receipt și audit runtime intern. În v1, evenimentele logice SHOULD fi transformabile în Witness Records doar dacă configurația o permite.

7. Structura contractului

7.1 Contract module

Un contract module conține:

ContractModule {
  metadata
  type_section
  constant_section
  storage_schema
  effect_signatures
  exported_functions
  bytecode_section
  abi_section
  static_analysis_manifest
}

7.2 metadata

Conține:

• language_version
• compiler_version
• source_hash
• license_hash
• build_flags_hash
• debug_info_hash?

7.3 storage_schema

Descrie forma exactă a stării persistente. Schema MUST fi:

• canonicală;
• hash-uibilă;
• versionată;
• bounded.

7.4 exported_functions

Doar funcțiile exportate pot fi chemate prin TX_MACHINE_CALL. Restul sunt interne.

8. State model

8.1 Persistent state

Fiecare mașină are o stare persistentă serializată canonical:

PersistentStateBlob

Aceasta MUST respecta:

• schema declarată;
• state_bound_bytes;
• eventuale invariants ale contractului.

8.2 Ephemeral execution state

În timpul execuției, BVM folosește:

• stack
• linear memory bounded
• local variables
• read-only execution context
• effect accumulator

Acest stat ephemer MUST fi distrus după execuție. Nu există persistență implicită.

8.3 State root

După execuție, noua stare persistentă este hash-uită canonical. Nodurile MUST produce exact același state_root.

9. Bytecode model

9.1 Obiectiv

Bytecode-ul BVM trebuie să fie:

• compact;
• validabil static;
• interpretabil simplu;
• compilabil eventual și JIT/AOT fără schimbare semantică.

9.2 Format general

Bytecode-ul conține:

• section header
• type table
• function table
• constant pool
• instruction stream
• effect metadata
• analysis metadata

9.3 Canonical bytecode hash

code_hash = H("AZ:BVM_CODE:" || canonical_bytecode_blob)

Acest hash intră în MachineDeploy.

10. Instruction classes

10.1 Clase permise

Instrucțiunile BVM v1 SHOULD aparține doar claselor:

• control flow bounded
• integer arithmetic safe
• boolean logic
• comparison
• struct/array access bounded
• hashing primitive calls
• serialization/deserialization canonicală
• state read/write APIs
• effect APIs
• abort/revert
• assertion
• bounded iteration

10.2 Clase interzise

BVM v1 MUST NOT permite:

• syscall arbitrar
• external I/O
• thread spawn
• floating point ops
• unrestricted recursion
• self-modifying code
• dynamic code loading
• unbounded jumps in unknown targets
• hidden host callbacks

11. Control flow

11.1 Permis

BVM permite:

• if / else
• match pe enum finit
• bucle bounded
• early return
• fail / revert
• funcții interne fără recursivitate generală

11.2 Buclă bounded

O buclă este permisă numai dacă:

• are bound static derivabil;
• sau are bound furnizat explicit și verificat;
• și upper bound-ul intră în max_iter_steps.

Exemple:

• iterare prin bounded_vec<T, 32>
• iterare for i in 0..N, unde N <= MAX_ALLOWED

11.3 Recursivitate

Recursivitatea generală MUST NOT fie permisă în v1. Tail-call elimination nu schimbă regula.

12. Arithmetic semantics

12.1 Integer semantics

Operațiile pe integeri MUST fi precise și deterministe.

Overflow/underflow policy v1:

• implicit = trap
• explicit wrapping MAY fi permis doar prin instrucțiuni dedicate și marcate

12.2 Division

Împărțirea la zero MUST trap.

12.3 Ratio operations

Operațiile pe ratio MUST:

• verifice denominator != 0
• reducă sau normalizeze conform regulii canonice, dacă specificația o cere
• evite overflow prin reguli de checked arithmetic

13. Memory model

13.1 Stack

BVM are stack bounded. Fiecare apel MUST respecta:

• max_stack_words
• max_call_depth

13.2 Call depth

Call depth-ul intern SHOULD fi mic și bounded. În v1, un prag fix este recomandat.

13.3 Linear memory

BVM MAY expune linear memory bounded:

• mărime inițială fixă;
• creștere limitată sau interzisă;
• orice acces out-of-bounds MUST trap.

13.4 No alias chaos

Modelul de memorie SHOULD evita aliasing greu de analizat. Preferința este pentru valori/copii și referințe strict controlate.

14. Host interface

14.1 Definiție

BVM nu operează direct pe starea globală prin pointeri arbitrar. Folosește un host interface strict, canonical.

14.2 Host calls permise

Set minim v1:

• host_read_state(path_ref)
• host_write_state(path_ref, value_blob)
• host_read_cell(cell_ref)
• host_consume_cell(cell_ref)
• host_create_cell(cell_blob)
• host_read_witness(witness_ref)
• host_emit_witness(witness_blob)
• host_read_proof(proof_ref)
• host_get_protocol_param(param_id)
• host_get_current_epoch()
• host_get_machine_metadata()
• host_abort(error_code)

14.3 Reguli

1. Host calls MUST fi deterministe.
2. Host calls MUST verifica permisiunile și bounds.
3. Host calls MUST actualiza effect accumulator-ul.
4. Host calls MUST NOT citi nimic în afara obiectelor referite canonical.

15. Effect accumulator

15.1 Scop

În loc să aplice imediat efectele finale, BVM produce mai întâi un accumulator deterministic.

EffectAccumulator {
  read_set
  write_set
  consumed_cells
  created_cells
  read_witnesses
  emitted_witnesses
  proofs_used
  logical_events
  lock_delta
  burn_delta
}

15.2 Beneficii

• auditabilitate;
• verificare post-execuție;
• comparare cu declared_effect_digest;
• compunere curată cu AZ-003.

15.3 Regula

La finalul execuției:

• accumulator-ul MUST fi complet determinat;
• MUST respecta effect_bound;
• MUST fi compatibil cu permission_surface;
• MUST produce același digest pe toate nodurile.

16. Exec units

16.1 Definiție

BVM folosește o unitate abstractă de cost: exec unit.

Scop:

• limită pe timp de execuție;
• predictibilitate;
• comparabilitate între noduri;
• fee estimation.

16.2 Surse de cost

Exec units SHOULD acoperi:

• instrucțiuni CPU-like;
• hashing;
• serializare/deserializare;
• reads/writes de stare;
• efecte pe Cells;
• witness/proof access;
• memory expansion bounded;
• loop iterations.

16.3 Regula

Fiecare instrucțiune sau host call are cost normativ fix sau formulă deterministă.

16.4 Limită

Dacă exec_units_used > max_exec_units_per_call, execuția MUST fail.

16.5 Trap semantics

Depășirea exec units MUST produce eșec deterministic, fără aplicare parțială a stării.

17. Static analysis manifest

17.1 Scop

Fiecare contract compilat MUST include un manifest de analiză statică.

StaticAnalysisManifest {
  analysis_version
  max_stack_words
  max_call_depth
  max_linear_memory_bytes
  max_exec_units_upper_bound
  max_iter_steps
  effect_summary
  storage_schema_hash
  exported_function_signatures
  forbidden_pattern_flags
  proof_of_well_typedness
}

17.2 Verificare la deploy

Nodul MUST verifica:

• manifestul există;
• este coerent cu bytecode-ul;
• nu declară patternuri interzise;
• upper bounds sunt acceptabile pentru parametrii protocolului.

17.3 Fără manifest

Un contract fără manifest static valid MUST NOT fi deployat.

18. Exported function signatures

18.1 Formă

O funcție exportată are semnătură canonicală:

ExportedFunctionSig {
  selector: hash32
  name_hash: hash32
  arg_schema_hash: hash32
  return_schema_hash: hash32?
  read_set_schema_hash: hash32
  write_set_schema_hash: hash32
  effect_signature_hash: hash32
  max_exec_units: uint64
  max_state_write_bytes: uint32
}

18.2 Reguli

1. selector MUST fi unic în cadrul contractului.
2. arg_schema_hash MUST descrie exact input-ul.
3. effect_signature_hash MUST corespunde funcției reale.
4. max_exec_units funcțional MUST NOT depăși limita mașinii.
5. max_state_write_bytes MUST NOT depăși effect_bound.

19. Deterministic serialization inside contracts

19.1 Regula

Orice obiect serializat de contract pentru hashing sau persistare MUST folosi aceleași reguli canonice ale protocolului.

19.2 Interdicție

Contractele MUST NOT produce hash-uri peste reprezentări locale necanonice.

Motiv: altfel două noduri pot obține state roots diferite pentru aceeași logică.

20. Error and revert model

20.1 Tipuri de eșec

BVM distinge:

• TRAP
• REVERT
• ASSERT_FAIL
• BOUND_EXCEEDED
• PERMISSION_DENIED
• INVALID_EXTERNAL_OBJECT
• TYPE_VIOLATION
• INTERNAL_VM_FAULT

20.2 Revert

REVERT înseamnă:

• execuția eșuează controlat;
• nicio modificare persistentă a stării nu se aplică;
• effect accumulator-ul final nu produce state transition;
• fee/exec cost handling se aplică conform regulii de protocol.

20.3 Trap

TRAP înseamnă eroare severă de execuție:

• divide by zero
• out-of-bounds
• invalid opcode
• overflow implicit
• illegal host call
• cost exhausted

Rezultatul este invalidarea apelului.

21. State write model

21.1 Write granularity

BVM SHOULD folosi path-based writes pe storage schema, nu blob rewriting arbitrar total, chiar dacă starea finală se hash-uiește ca blob canonical.

21.2 Reguli

1. Orice write MUST targeta un path permis de schema.
2. Orice write MUST produce stare validă schema-wise.
3. Total bytes modificate MUST respecta max_state_write_bytes.
4. Nicio zonă nedeclarată a stării nu poate fi scrisă.

21.3 Invariant checks

Contractul MAY declara invariants interne. Runtime-ul sau checker-ul post-execuție MUST putea valida acele invariants.

22. Read model

22.1 Tipuri de citiri

Permise:

• citire stare proprie
• citire Cells atașate sau referite
• citire witnessuri atașate
• citire proof bundles atașate
• citire parametri de protocol
• citire metadata a mașinii proprii

22.2 Citiri interzise

Interzise:

• citirea directă a stării altor mașini fără mecanism explicit viitor standardizat
• citire nelimitată din istoric global
• scanări globale
• query-uri dependente de ordinea mempool

Motiv: determinism și boundedness.

23. Cross-contract model

23.1 v1 restriction

BVM v1 SHOULD evita apeluri arbitrare contract-la-contract.

23.2 Alternativă

Compoziția între mașini SHOULD avea loc prin:

• Cells;
• Witness Records;
• Intent flows;
• tranzacții separate și explicite.

23.3 Motiv

Apelurile cross-contract directe cresc drastic:

• complexitatea static analysis;
• riscul reentrancy;
• ambiguitatea costului;
• suprafața de atac.

24. Reentrancy

24.1 Regula

Reentrancy generală MUST NOT exista în BVM v1.

24.2 Consecință

Niciun contract nu poate intra din nou în aceeași tranziție prin apel extern reentrant. Astfel se elimină o clasă mare de exploit-uri.

25. Randomness and entropy

25.1 Interdicție de bază

Contractele MUST NOT folosi randomness neancorată.

25.2 Surse permise

Dacă este necesară entropie, aceasta MAY veni numai din:

• parametri de protocol deja finalizați;
• witness/proof standardizate;
• beacons definite de protocol în documente ulterioare.

25.3 Regula

Orice sursă de entropie MUST fi:

• deterministic accesibilă tuturor nodurilor;
• canonical referită;
• rezistentă la manipulare în limitele modelului de consens.

26. Upgradeability

26.1 Contract code immutability

code_hash al unei mașini deployate este imuabil.

26.2 Upgrade model

Upgrade-ul unei mașini SHOULD însemna:

• deploy al unei noi versiuni;
• migrare explicită de stare;
• anchoring prin upgrade_policy;
• witness/audit trail.

26.3 In-place mutation

Modificarea in-place a codului MUST NOT fi permisă în v1.

27. Formal verification hooks

27.1 Scop

BVM SHOULD fi prietenoasă cu:

• model checking;
• property testing;
• symbolic execution;
• proof generation pentru invariants.

27.2 Requirements

Contractele și ABI-ul SHOULD permite exprimarea:

• invariants de stare;
• preconditions;
• postconditions;
• safety properties;
• bounded liveness assumptions.

28. Contract classes recomandate

28.1 Escrow

Proprietăți:

• release condiționat de witness;
• timeout path;
• amount conservation;
• max two or few effect paths.

28.2 Vault

Proprietăți:

• deposits/withdrawals bounded;
• rate limits;
• guard policies;
• journaling.

28.3 Treasury

Proprietăți:

• proposal queue bounded;
• quorum witness;
• timelock;
• spend caps.

28.4 Auction/RFQ

Proprietăți:

• bounded participant count per lot;
• deterministic clearing;
• explicit tie-breakers.

28.5 Agent orchestrator

Proprietăți:

• delegated roles;
• daily notional caps;
• required logging;
• halt hooks.

29. Forbidden patterns

BVM v1 MUST reject contracte care conțin sau ascund:

1. recursivitate generală;
2. bucle fără upper bound demonstrabil;
3. acces nebounded la colecții;
4. host calls dinamice nevalidate;
5. code reflection capabilă de path semnatic variabil nelimitat;
6. scrieri în stare în afara schemei;
7. efecte dependente de ordinea mempool;
8. self-upgrade implicit;
9. dispatch indirect nebounded;
10. semnături de efect contradictorii cu bytecode-ul.

30. Deployment validation

30.1 Nodul MUST verifica la deploy:

1. bytecode canonical valid;
2. manifest static coerent;
3. type sections consistente;
4. storage schema validă și bounded;
5. exported signatures coerente;
6. effect summaries coerente;
7. lipsa patternurilor interzise;
8. limitele de resurse sub maximele de protocol;
9. code_hash și abi_hash corecte;
10. compatibilitatea cu MachineDeploy descriptor.

30.2 Eșec

Dacă oricare verificare eșuează, contractul MUST NOT fi deployat.

31. Call-time validation inside runtime

31.1 La execuția unei funcții exportate, runtime-ul MUST verifica:

1. selector valid;
2. input conform cu arg_schema_hash;
3. caller policy satisfăcută extern;
4. state blob conform cu schema;
5. witness/proof refs accesibile și valide;
6. exec units disponibile;
7. mașina nu este halted.

31.2 Pe parcursul execuției, runtime-ul MUST verifica:

1. bounds de memorie;
2. bounds de stack;
3. host call permissions;
4. effect counts;
5. write limits;
6. arithmetic safety.

31.3 La final, runtime-ul MUST verifica:

1. accumulator valid;
2. noua stare validă schema-wise;
3. invariants de contract;
4. effect_bound;
5. loss_envelope;
6. digest-ul efectelor.

32. Loss envelope integration

32.1 Principiu

Loss envelope nu este doar metadată economică. Runtime-ul și validatorii MUST o trateze ca bound normativ.

32.2 Exemple de verificări

• valoarea totală ieșită nu depășește plafonul per call;
• valoarea blocată nu depășește durata maximă;
• activele atinse sunt în lista permisă;
• numărul dependențelor externe nu depășește limita.

32.3 Consecință

Dacă logica contractului ar produce o stare profitabilă dar cu risc peste envelope, apelul este invalid.

33. Permission surface integration

33.1 Contract runtime MUST map every effect la un permission bit / class.

33.2 Exemple

• CREATE_CELL cere can_emit_cells
• EMIT_WITNESS cere can_emit_witnesses
• LOCK_VALUE cere can_lock_value
• BURN_VALUE cere can_burn_value

33.3 Regula

O diferență între efectele reale și permission_surface este invalidare directă.

34. ABI rules

34.1 ABI objectives

ABI-ul BVM trebuie să fie:

• canonical;
• versioned;
• hash-uibil;
• ușor de generat pentru toolchains;
• sigur pentru decode.

34.2 ABI MUST define:

• numele funcției la nivel logic
• selectorul
• schema argumentelor
• schema rezultatului
• efectele
• erorile posibile
• bounds maxime

34.3 ABI stability

Orice schimbare breaking în ABI SHOULD schimba abi_hash.

35. Debuggability and audit traces

35.1 Audit traces

Runtime-ul MAY produce trace-uri pentru debugging, dar acestea MUST NOT afecta consensul.

35.2 Consensus-safe traces

Dacă se produce trace consensus-safe, acesta SHOULD fi derivabil determinist și hash-uibil.

35.3 Recomandare

În producție, nodurile pot dezactiva trace extins, dar MUST păstra posibilitatea de a reconstrui receipt-ul și effect digest-ul.

36. Bytecode verification phases

36.1 Faza 1 — Structural verification

• header valid
• sections valide
• offsets valide
• opcodes cunoscute

36.2 Faza 2 — Type verification

• operand stack typing
• local typing
• call signature compatibility
• branch merge compatibility

36.3 Faza 3 — Boundedness verification

• no forbidden recursion
• loop bounds known
• memory caps known
• stack caps known
• effect paths bounded

36.4 Faza 4 — Effect verification

• host calls compatibile cu signatures
• effect summary exact sau supra-approx sigur
• permission classes derivabile

37. Canonical execution result

37.1 Orice execuție validă produce:

BvmExecutionResult {
  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?
}

37.2 Reguli

1. next_state_root MUST corespunde exact stării serializate canonice.
2. effect_digest MUST corespunde accumulator-ului.
3. exec_units_used MUST fi identic pe toate nodurile.
4. status_code MUST aparține setului standardizat.

38. Gas griefing and denial resistance

38.1 Obiectiv

BVM trebuie să minimizeze contractele care par ieftine static dar explodează dinamic.

38.2 Măsuri

• loop bounds obligatorii;
• cost pentru acces la stări și serializare;
• no global scans;
• no dynamic dispatch nebounded;
• max object counts;
• exec limit per call.

38.3 Principiu

Costul maxim SHOULD fi aproximabil conservator înainte de execuție.

39. Security advantages of BVM

BVM urmărește să elimine sau reducă structural:

• reentrancy generală
• gas bombs nebounded
• hidden external dependencies
• nondeterministic state roots
• floating-point divergence
• unbounded storage growth per call
• upgrade opac
• code injection
• read-after-write ambiguity cross-contract

40. Security limitations

BVM nu elimină:

• buguri logice în contract;
• parametri economici proști;
• witness/oracle greșite;
• politici de delegare prost setate;
• model de afaceri nesustenabil.

BVM reduce suprafața execuțională, nu garantează inteligență economică.

41. Recommended compiler responsibilities

Compilatorul AZ-Lang -> BVM SHOULD:

1. genereze bytecode canonical;
2. emită manifest static coerent;
3. refuze programe nebounded;
4. semnaleze efectele reale;
5. optimizeze fără schimbare semantică;
6. producă mapare clară sursă -> bytecode pentru audit.

42. Minimal opcode families for v1

Set minimal orientativ:

• CONST
• MOVE
• LOAD_LOCAL
• STORE_LOCAL
• ADD/SUB/MUL/DIV/MOD_CHECKED
• CMP_*
• AND/OR/NOT
• JUMP_IF
• JUMP_BOUNDED
• PACK_STRUCT
• UNPACK_STRUCT
• LOAD_FIELD
• STORE_FIELD
• HASH_BLAKE_OR_SHA_FAMILY (final choice separat)
• CALL_INTERNAL
• HOST_CALL
• ASSERT
• RETURN
• REVERT
• ABORT

Setul exact final poate fi rafinat, dar MUST rămâne mic și analizabil.

43. Machine classes by capability tier

43.1 Tier 0 — Passive bounded state

• state read/write
• no value custody
• witness emission limitată

43.2 Tier 1 — Custody bounded

• poate consuma/crea Cells
• loss envelope strict
• no burn by default

43.3 Tier 2 — Market logic bounded

• multiple asset interactions
• stronger effect bounds
• stricter static analysis and fees

43.4 Tier 3 — Agent coordination bounded

• delegated roles
• required journaling
• halt hooks
• witness-heavy flows

Capability tier-ul SHOULD influența deploy cost, audit requirements și parametrii de risc.

44. Formal goals

BVM urmărește trei obiective formale:

1. Determinism theorem target
   aceeași stare + același input + același cod + aceleași obiecte externe => același rezultat.

2. Boundedness theorem target
   orice execuție validă consumă resurse în limitele declarate și verificate.

3. Effect soundness target
   efectele observate sunt subset exact sau supra-approx sigur al efectelor declarate și permise.

Demonstrațiile complete aparțin unei documentații matematice separate, dar specificația MUST fie compatibilă cu ele.

45. Relația cu restul protocolului

• AZ-002 definește obiectele.
• AZ-003 definește validarea și tranziția de stare.
• AZ-004 definește când tranzițiile devin finale.
• AZ-005 definește cum este produsă logic tranziția internă a unei mașini.

Pe scurt: BVM este motorul bounded care generează schimbarea de stare fără a sparge determinismul protocolului.

46. Formula mașinii virtuale

BVM = typed code + bounded memory + explicit effects + deterministic host interface + static proofs of boundedness

47. Ce urmează

După AZ-005, documentul corect este:

AZ-006 — Witness, Proof, and Attestation Rules

Acolo trebuie definit:

• tipologia de witness;
• validarea revocării;
• reguli pentru dovezi;
• accountability pentru oracles și atestatori;
• cum devine memoria verificabilă utilă pentru aplicații și agenți.

Închidere

ATLAS ZERO nu tratează contractele ca pe programe nelimitate care „poate ies bine”. Le tratează ca pe mașini finite, tipate, controlabile și inspectabile înainte să primească dreptul de a atinge valoare.

Acolo începe disciplina protocolului.