docs/PROTOCOL.md

# 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<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:**
```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."*