Document

State Machine

**Verifiable Semantic Execution Layer (VSEL)**

Verifiable Semantic Execution Layer (VSEL)

1. Purpose

This document defines the concrete operational state machine of VSEL.

While FORMAL_SPECIFICATION.md defines correctness at an abstract level, this document specifies:

concrete state representation
transition classes
execution rules
preconditions and postconditions
error semantics

This is the bridge between:

“what is correct” and “what actually runs”

If this document diverges from the formal specification, the implementation is wrong.

2. State Structure

A concrete state ( s \in S ) is defined as:

[ s = (C, D, E, \tau) ]

Where:

2.1 Canonical State ( C )

Represents the minimal semantic state:

account balances / resources
ownership mappings
contract storage
system-defined data structures

Properties:

fully deterministic
minimal representation
sufficient to reconstruct all semantics

2.2 Derived State ( D )

Computed from ( C ):

Merkle roots
aggregate values
indexing structures

Constraint:

[ D = Derive(C) ]

Derived state must not introduce new semantics.

2.3 Environment ( E )

Represents external context:

timestamp
block height
execution domain
randomness (if modeled)

All environmental influence must be explicit.

2.4 Trace Metadata ( \tau )

Includes:

sequence index
previous state commitment
execution epoch

Ensures ordering and trace consistency.

3. State Encoding

State encoding must satisfy:

canonical serialization
deterministic hashing
structural integrity

Let:

[ Encode: S \rightarrow Bytes ]

[ Hash: Bytes \rightarrow Commitment ]

Requirement:

[ Hash(Encode(s)) = Commitment(s) ]

Any mismatch invalidates the state.

4. Transition Model

A transition is defined as:

[ (s, \sigma) \rightarrow s' ]

Where:

( s ) is current state
( \sigma ) is input
( s' ) is resulting state

Transitions are deterministic:

[ (s, \sigma) \Rightarrow s' \text{ is unique} ]

5. Transition Classes

Transitions are categorized into explicit classes.

No implicit transition types are allowed.

5.1 Initialization Transition

[ Init \rightarrow s_0 ]

Creates a valid initial state.

Preconditions:

no prior state

Postconditions:

( s_0 \in I )

5.2 State Update Transition

[ (s, \sigma_{update}) \rightarrow s' ]

Represents standard state mutation.

Preconditions:

input is valid
authorization passes
invariants hold on ( s )

Postconditions:

invariants hold on ( s' )
state updated deterministically

5.3 No-Op Transition

[ (s, \sigma_{noop}) \rightarrow s ]

Used for:

invalid input handling
rejected operations

Preconditions:

input fails validation

Postconditions:

state unchanged
rejection observable emitted

5.4 Error Transition

[ (s, \sigma_{error}) \rightarrow s_{error} ]

Explicit error state handling.

Constraint:

( s_{error} \in S )
invariants must still hold

No undefined behavior allowed.

5.5 Batch Transition

[ (s, [\sigma_1, ..., \sigma_n]) \rightarrow s' ]

Equivalent to sequential application:

[ Apply(s, \sigma_1, ..., \sigma_n) ]

Constraint:

ordering must be preserved
no implicit reordering

5.5.1 Batch Intermediate Invariant Policy

Batch execution is sequential application with per-step invariant validation. Each input σ_i in the batch is executed through the full 7-step pipeline (§6), including postcondition validation (step 5) and derived state recalculation (step 6). If any intermediate state s_i violates any invariant, the entire batch is rejected — no partial application is committed.

Formally:

[ \forall i \in [1, n]: \text{Invariants}(s_i) \text{ must hold} ]

If there exists any i such that the intermediate state s_i produced by applying σ_i violates an invariant, then:

[ \text{execute_batch}(s, [\sigma_1, ..., \sigma_n]) = \text{Error} ]

even if the final state s_n would restore the invariant. This policy prevents transient invariant violations from being masked by subsequent operations within the same batch.

This is a deliberate design choice: batch execution provides no "transaction-level" invariant relaxation. Every intermediate state must be independently valid.