# 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:** ```prolog 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:** ```prolog 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:** ```prolog 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 │ │ 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:** ```prolog 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:** ```prolog 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:** ```prolog 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:** ```prolog 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:** ```prolog 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 ```prolog 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/2`~~ (internal only) - ~~`dispatch_permitted/5`~~ (internal only) - ~~`agent_authorized/3`~~ (internal only) **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) ```json { "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:** ```prolog receipt_sequence_valid(Receipt1, Receipt2) :- Receipt1.sequence < Receipt2.sequence, timestamp(Receipt1) < timestamp(Receipt2). ``` **Hash Linkage:** ```prolog 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:** ```prolog 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 ```prolog 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: ```prolog 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): 1. **Define entry state:** `transition_valid(FromState, CustomState, custom_action, true) :- ...` 2. **Implement Prolog guard:** Add rule to transitions.pl 3. **Update state machine:** Add state record in transitions.pl facts 4. **Test:** Add test case to logic/queries/test_queries.pl 5. **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."*