ROWM Protocol Specification — State Machine & Transitions
Version: 1.0.0
Status: Normative (verified 2026-07-27)
Authors: Ahmad Ali Parr, Jessica SNAPKITTYWEST
1. Protocol Overview
The ROWM protocol defines the formal state machine for cell execution, authorization, verification, and release. All state transitions are guarded by Prolog predicates; no transition may occur without passing source-of-truth validation.
Core Principle: Execution is NOT a black-box computation — it is a sequence of validated protocol events, each linked to the prior event via cryptographic receipt chain.
2. Eight-Stage Execution Pipeline
Stage 1: PARSED
Entry: External instruction (EmojiCode, notebook cell, CLI command)
State: Source representation parsed into AST
┌─────────────────────────────────┐
│ PARSED │
│ │
│ Input: raw source code │
│ Language: any of 30+ │
│ Kernel: optional (inferred) │
│ │
│ Output: Unified AST │
│ Hash: Blake3(canonical_source) │
└─────────────────────────────────┘
↓ transition: authorize
[AUTHORIZED]
Actions:
- Parse source in language-specific parser
- Emit AST events (function def, assignment, loop, etc.)
- Compute source_hash
Prolog Guard:
transition_valid(parsed, authorized, authorize, true) :-
instruction_well_formed(Instr),
language_supported(Instr.language).
Stage 2: AUTHORIZED
Entry: Canonical instruction ISIR (parsed state)
State: Authorization decision recorded
┌─────────────────────────────────┐
│ AUTHORIZED │
│ │
│ Agent: (from ISIR) │
│ Capability: (from ISIR) │
│ Runtime: (from ISIR) │
│ Permission: dispatch|execute... │
│ │
│ Authorization result: PASS/FAIL │
└─────────────────────────────────┘
↓ [if PASS]
transition: compile
[COMPILED]
↓ [if FAIL]
emit: AuthorizationDeniedReceipt
[RECEIPTED] → end
Actions:
- Query Prolog:
dispatch_gated(Agent, Cap, Runtime, Permission, ?) - If true: record authorization event, proceed
- If false: emit denial receipt, halt
Prolog Guard:
transition_valid(authorized, compiled, compile, true) :-
dispatch_gated(Agent, CapID, Runtime, Perm, true),
action_authorized(compile, Runtime).
Stage 3: COMPILED
Entry: Authorized ISIR
State: Bytecode generated, invariants extracted
┌─────────────────────────────────┐
│ COMPILED │
│ │
│ Bytecode: stack-based IR │
│ Registers: R0-R15 allocated │
│ SUBLEQ layout: M[0+] mapped │
│ │
│ Invariants extracted: │
│ - Loop invariants (interval) │
│ - Proof obligations (4) │
│ Proof obligations: │
│ - InvariantPreservation │
│ - SemanticPreservation │
│ - LoopInvariantMaintenance │
│ - ReceiptChainIntegrity │
│ │
│ Status: ready_to_execute │
└─────────────────────────────────┘
↓ transition: execute
[EXECUTING]
Actions:
- AST → bytecode with register allocation
- Bytecode → SUBLEQ memory layout
- Symbolic execution trace (all paths)
- Abstract interpretation (loop invariants)
- Extract proof obligations
- Emit compilation receipt
Prolog Guard:
transition_valid(compiled, executing, execute, true) :-
bytecode_valid(Bytecode),
\+ proof_obligation_unsatisfiable(ProofObl),
invariants_extracted(Invariants).
Stage 4: EXECUTING
Entry: Compiled SUBLEQ bytecode
State: Virtual machine running with mutation tracking
┌─────────────────────────────────┐
│ EXECUTING │
│ │
│ Von Neumann memory: Vec<i64> │
│ Instruction pointer: IP │
│ Mutations: tracked & logged │
│ │
│ For each SUBLEQ step: │
│ M[b] -= M[a] │
│ if M[b] <= 0 then IP = c │
│ emit MutationEvent │
│ check_invariants() │
│ periodic_checkpoint() │
│ │
│ Exception handling: │
│ - Infinite loop? (timeout) │
│ - Invariant violation? │
│ → rollback to checkpoint │
└─────────────────────────────────┘
↓ [success or timeout]
transition: checkpoint
[CHECKPOINT_STORED]
↓ [invariant violation]
emit: InvariantViolationReceipt
rollback(checkpoint_id)
[RECEIPTED] → end
Actions:
- Initialize memory with cell code
- Execute SUBLEQ instructions
- Emit mutation events (address, old_val, new_val)
- Check invariants at loop entry points
- Create checkpoints every N mutations
- Detect timeouts (default 30s)
Prolog Guard:
transition_valid(executing, checkpoint_stored, checkpoint, true) :-
execution_terminated(normal),
checkpoint_valid(CheckpointID).
transition_valid(executing, receipted, halt_on_violation, true) :-
invariant_violated(InvariantID),
rollback_succeeded(CheckpointID).
Stage 5: CHECKPOINT_STORED
Entry: Execution halted (normal or via rollback)
State: Checkpoint is WORM-sealed (write-once)
┌─────────────────────────────────┐
│ CHECKPOINT_STORED │
│ │
│ Checkpoint record: │
│ - cell_id: string │
│ - output_hash: Blake3 │
│ - invariants: [hash, ...] │
│ - timestamp: Unix timestamp │
│ - predecessor_hash: parent │
│ - status: valid | violated │
│ │
│ WORM sealed: no further writes │
└─────────────────────────────────┘
↓ transition: verify
[VERIFIED]
Actions:
- Record checkpoint to WORM storage
- Compute checkpoint_hash = Blake3(record)
- Link to previous checkpoint (DAG structure)
- Mark as immutable
Prolog Guard:
transition_valid(checkpoint_stored, verified, verify, true) :-
checkpoint_worm_sealed(CheckpointID),
checkpoint_hash_valid(CheckpointID).
Stage 6: VERIFIED
Entry: Checkpoint sealed
State: Proof obligations validated
┌─────────────────────────────────┐
│ VERIFIED │
│ │
│ Proof validation: │
│ - InvariantPreservation │
│ Verified: ALL loop invs │
│ maintained │
│ - SemanticPreservation │
│ Verified: source meaning = │
│ compiled meaning │
│ - LoopInvariantMaintenance │
│ Verified: bounds & exit │
│ - ReceiptChainIntegrity │
│ Verified: monotonic seq │
│ │
│ Status: all_proofs_pass OR │
│ some_proofs_manual │
└─────────────────────────────────┘
↓ transition: seal
[RECEIPTED]
Actions:
- Run automated proof (Z3 for arithmetic, simple patterns)
- Query external verifiers (Agda, Ada/SPARK) if requested
- Emit proof status receipt
- Link to prior receipt
Prolog Guard:
transition_valid(verified, receipted, seal, true) :-
all_proofs_satisfied(true),
proof_status_recorded(ProofStatus),
previous_receipt_linked(PriorReceiptHash).
Stage 7: RECEIPTED
Entry: Proof verified (or manual override)
State: Receipt is signed and chained
┌─────────────────────────────────┐
│ RECEIPTED │
│ │
│ Receipt record (WORM): │
│ type: CellExecuted │
│ cell_id: string │
│ output_hash: Blake3 │
│ invariants_satisfied: [...] │
│ proofs_verified: [...] │
│ previous_receipt_hash: link │
│ timestamp: now() │
│ signature: Ed25519(bytes) │
│ │
│ Chain link: receipt_hash ←→ │
│ prior receipt via hash │
└─────────────────────────────────┘
↓ transition: release [optional]
[RELEASED]
or stay in RECEIPTED
(release is not mandatory)
Actions:
- Generate receipt JSON/CBOR
- Compute receipt_hash = Blake3(canonical_receipt_bytes)
- Sign with Ed25519 private key (issuer = Agent)
- Append to Bifrost chain
- Emit receipt-added event to listeners
Prolog Guard:
transition_valid(receipted, released, release, true) :-
receipt_chain_valid(true),
release_gates_passed(AllGates, true),
version_layers_compatible(true).
% Alternative: stay in receipted indefinitely
transition_valid(receipted, receipted, noop, true) :-
\+ release_requested.
Stage 8: RELEASED
Entry: All release gates passed
State: Release manifest generated and signed
┌─────────────────────────────────┐
│ RELEASED │
│ │
│ Release manifest: │
│ - source_version: Git SHA │
│ - protocol_version: 1.0.0 │
│ - evidence_version: stage+cnt │
│ - knowledge_version: Prolog ID│
│ - git_commit: HEAD sha │
│ - receipt_chain_head: hash │
│ - signer: Agent identity │
│ - signature: Ed25519 sig │
│ - previous_release_hash: link │
│ │
│ Status: immutable (archived) │
└─────────────────────────────────┘
↓ Final state
(no further transitions)
Or Archive:
↓ transition: archive
[ARCHIVED]
Actions:
- Query all release gates via Prolog
- Verify 4-layer versions sync
- Generate release manifest
- Sign manifest with Agent's Ed25519 key
- Append manifest receipt to ledger
- Tag in Git (if applicable)
- Mark cells as complete
Prolog Guard:
transition_valid(receipted, released, release, true) :-
readiness_check('proofs_satisfied', true),
readiness_check('receipt_chain_sealed', true),
readiness_check('no_revoked_capabilities', true),
readiness_check('all_cells_complete', true),
readiness_check('receipt_chain_integrity', true),
version_layers_compatible(SourceVer, ProtocolVer, EvidenceVer, KnowledgeVer).
transition_valid(released, archived, archive, true) :-
release_manifest_sealed(ManifestHash).
3. Authorization Protocol (Sealed Entry Point)
All external dispatch MUST pass through dispatch_gated/5.
dispatch_gated/5 Predicate
dispatch_gated(AgentID, CapabilityID, TargetRuntime, Permission, IsPermitted) :-
% Step 1: Verify agent exists and is active
agent_active(AgentID, true),
% Step 2: Verify agent trust tier is not observer (tier_2)
agent_trust_level(AgentID, TrustLevel),
TrustLevel \= tier_2,
% Step 3: Verify capability is held by agent for this runtime
capability_issued(CapabilityID, _IssuerID, AgentID, TargetRuntime, Permissions, _IssuedAt, ExpiresAt),
% Step 4: Verify capability is active (not revoked, not expired)
\+ capability_revoked(CapabilityID, _),
get_time(Now),
Timestamp is floor(Now),
Timestamp < ExpiresAt, % CRITICAL: exclusive boundary
% Step 5: Verify permission is in capability grant
member(Permission, Permissions),
% Step 6: Verify target runtime is active
runtime_active(TargetRuntime, true).
dispatch_gated(_, _, _, _, false). % Default: deny
Critical Enforcement
PROHIBITED DIRECT QUERIES:
capability_active/2dispatch_permitted/5agent_authorized/3
ALLOWED QUERIES:
dispatch_gated/5(sealed entry point)release_ready/1(release readiness)readiness_check/2(diagnostic)
4. Receipt Chain Structure
Receipt Record (WORM Ledger)
{
"receipt_id": "sha256_of_contents",
"sequence": 42,
"type": "CellExecuted",
"cell_id": "cell_0",
"agent": "forge",
"timestamp": 1719432000,
"output_hash": "blake3_hash_of_output",
"invariants_satisfied": [
"inv_1_loop_bound",
"inv_2_array_bounds",
"inv_3_type_safety"
],
"proofs_verified": [
"proof_invariant_preservation",
"proof_semantic_equivalence"
],
"previous_receipt_hash": "hash_of_prior_receipt",
"signature": "ed25519_signature",
"chain_position": "N in DAG"
}
Chain Integrity Checks
Monotonic Sequencing:
receipt_sequence_valid(Receipt1, Receipt2) :-
Receipt1.sequence < Receipt2.sequence,
timestamp(Receipt1) < timestamp(Receipt2).
Hash Linkage:
receipt_chain_valid(ReceiptID) :-
receipt_issued(ReceiptID, _Seq, _Agent, _Cap, _Instr, _Action, _InHash, _OutHash, _Timestamp),
receipt_issued(PriorReceiptID, PriorSeq, _, _, _, _, _, _, _),
PriorSeq + 1 = _Seq,
receipt_hash(PriorReceiptID, PriorHash),
receipt_data(ReceiptID, Data),
Data.previous_receipt_hash == PriorHash.
Tamper Detection:
receipt_tampered(ReceiptID) :-
receipt_issued(ReceiptID, _, _, _, _, _, InHash, OutHash, _),
stored_in_hash = hash(stored_data),
(stored_in_hash \= InHash ; stored_out_hash \= OutHash).
5. Capability Lifecycle
States
Issued → Active → (Revoked OR Expired)
Issued:
- created by issuer agent
- stored in capabilities.pl
- has future ExpiresAt timestamp
Active:
- \+ capability_revoked(CapID, _)
- get_time() < ExpiresAt
- can be used in dispatch_gated/5
Revoked:
- capability_revoked(CapID, RevocationReason) fact exists
- cannot be used, period
- reason recorded for audit
Expired:
- get_time() >= ExpiresAt (at boundary: exclusive <)
- automatically inactive
- new capability must be issued
Revocation Protocol
revoke_capability(CapID, Reason) :-
% Only sovereign or admin agents can revoke
agent_trust_level(Revoker, Tier),
(Tier = tier_0 ; Tier = tier_1),
% Record revocation as WORM fact
assertz(capability_revoked(CapID, Reason)),
% Emit revocation receipt
emit_receipt(type=CapabilityRevoked, cap_id=CapID, reason=Reason).
6. Release Gates (12-Point Checklist)
Before transitioning to RELEASED, all gates must pass:
release_ready(true) :-
gate_1_all_proofs_satisfied,
gate_2_receipt_chain_sealed,
gate_3_no_revoked_capabilities,
gate_4_all_cells_complete,
gate_5_receipt_chain_integrity,
gate_6_no_code_mutation_after_seal,
gate_7_no_untested_paths,
gate_8_version_layers_compatible,
gate_9_manifests_generated,
gate_10_signatures_valid,
gate_11_no_active_dependencies,
gate_12_performance_acceptable.
For production release: All 12 gates must return true.
For staged release: Progressively check gates; advance stage when satisfied.
7. Transition Error Handling
Invalid Transition Attempt
If transition_valid(FromState, ToState, Action, false):
1. Emit TransitionDeniedReceipt
{
type: "TransitionDenied",
from_state: FromState,
to_state: ToState,
action: Action,
reason: failed_predicate_name,
prolog_query_result: false
}
2. Record in Prolog: transition_failed(FromState, Action, Reason)
3. Optionally: Rollback to prior checkpoint
4. Stay in FromState (no transition occurs)
5. Let user/agent retry or handle error
Automatic Rollback on Invariant Violation
If invariant_violated during EXECUTING:
1. Emit InvariantViolationReceipt
{
type: "InvariantViolated",
invariant_id: InvID,
violated_at: instruction_pointer,
expected: predicate_formula,
actual: observed_state
}
2. Query Prolog: checkpoint_valid(CheckpointID)
3. If valid: restore memory from checkpoint
4. Transition: EXECUTING → CHECKPOINT_STORED → VERIFIED
(with violation recorded)
5. Emit post-rollback receipt with new state
6. Release readiness check will fail (gate 4)
8. Concurrency & Isolation
Single-Cell Execution (No Concurrency)
The protocol assumes:
- One cell executes at a time
- No concurrent dispatch_gated calls
- Receipt chain is linearized (no branches)
Rationale: Formal verification of concurrent state is intractable; linearization enables proof certification.
Multi-Notebook Isolation
Each notebook:
- Has independent Prolog instance (or isolated rule set)
- Maintains separate receipt chain
- Cannot interfere with other notebooks
- Can cross-reference via signed manifests
9. State Diagram
┌─────────────────────┐
│ PARSED │
│ (AST generated) │
└─────────────────────┘
↓ authorize
┌─────────────────────┐
┌──→│ AUTHORIZED │───────┐
│ │ (dispatch_gated OK)│ │
│ └─────────────────────┘ ↓ [DENY]
│ ↓ compile [AuthorizationDenied]
│ ┌─────────────────────┐ ↓
│ │ COMPILED │ [RECEIPTED] → END
│ │ (bytecode ready) │
│ └─────────────────────┘
│ ↓ execute
│ ┌─────────────────────┐
│ │ EXECUTING │
│ │ (mutations logged) │
│ │ [invariant check] │
│ └─────────────────────┘
[VIOLATION] ↓ checkpoint
↓ ┌─────────────────────┐
[ROLLBACK] │ CHECKPOINT_STORED │
│ │ (WORM sealed) │
└───────→└─────────────────────┘
↓ verify
┌─────────────────────┐
│ VERIFIED │
│ (proofs checked) │
└─────────────────────┘
↓ seal
┌─────────────────────┐
│ RECEIPTED │◄──────┐
│ (receipt chained) │ │
└─────────────────────┘ │
↓ release [NOOP] │
│ (stay) │
├─────────────────────────→┤
↓
┌─────────────────────┐
│ RELEASED │
│ (manifest signed) │
└─────────────────────┘
↓ archive (optional)
┌─────────────────────┐
│ ARCHIVED │
│ (historical ref) │
└─────────────────────┘
10. Extensibility
Adding New Transitions
To add a new transition (e.g., CUSTOM_ACTION):
- Define entry state:
transition_valid(FromState, CustomState, custom_action, true) :- ... - Implement Prolog guard: Add rule to transitions.pl
- Update state machine: Add state record in transitions.pl facts
- Test: Add test case to logic/queries/test_queries.pl
- Document: Update this PROTOCOL.md
Version Compatibility
Protocol 1.0.0 is IMMUTABLE for releases tagged "1.x.y". New protocol features (2.0.0) must:
- Be backward-compatible with 1.x read paths
- OR version-gate old vs. new logic
- Include migration documentation
GOVERNANCE: EVIDENCE OR SILENCE.
All transitions are logged, verified, and sealed. The protocol is not just specification — it is executable law.
"LOC WRITES. LEDGER CERTIFIES. METATRON SEALS."