docs/ARCHITECTURE.md

# ROWM Architecture — Complete Technical Specification

**Version:** 1.0.0  
**Status:** Production (Verified 2026-07-27)  
**Authors:** Ahmad Ali Parr, Jessica SNAPKITTYWEST

---

## Executive Summary

ROWM (Read-Once-Write-Many Polymorphic Notebook Iterator) is an executable evidence environment that extends the notebook model from exploratory computation into verifiable execution, formal verification, and cryptographic provenance tracking.

The system separates **execution from authority**: a Prolog/Datalog knowledge engine serves as the canonical source of truth, runtime adapters execute bounded tasks, proof systems produce external evidence artifacts, and receipts are stored in an append-only ledger.

**Core Innovation:** Every execution is a protocol event that can be validated against declarative authorization rules, verified against formal proofs, and sealed into a cryptographic receipt chain.

---

## 1. System Layers (Five-Layer Model)

### Layer 1: User Interface — Notebook & EmojiCode

**Components:**
- Jupyter notebook cells (markdown, code, proof objects)
- EmojiCode domain-specific language (human-readable dispatch)
- Notebook metadata (kernel assignments, execution counts, cell visibility)

**Responsibilities:**
- Accept user input and cell definitions
- Provide human-readable execution status
- Display proof artifacts and receipt chain summaries
- Serve as inspection interface (NOT authoritative)

**Key Property:** Notebook state is never authoritative; it is an interface and evidence workspace.

---

### Layer 2: Canonical Representation — Intermediate Forms

**Components:**
- Unified AST (Abstract Syntax Tree)
- Bytecode IR (Intermediate Representation)
- SUBLEQ memory layout
- ISIR (Isomorphic Shift Intermediate Representation)

**Responsibilities:**
- Normalize source code from 30+ languages into unified AST
- Compile AST to bytecode with register allocation
- Lower bytecode to SUBLEQ memory image for execution
- Provide deterministic canonical encoding for hashing and signing

**Key Property:** All external formats must map to canonical representations before authorization or execution.

---

### Layer 3: Source-of-Truth Authority — Prolog/Datalog Engine

**Components:**
- `logic/facts/` — agents, runtimes, capabilities, notebooks, receipts
- `logic/rules/` — authorization, transitions, proofs, provenance, release readiness
- `logic/queries/` — test suite and verification queries

**Responsibilities:**
- Maintain authoritative facts about agents, capabilities, and state
- Evaluate authorization queries (dispatch_permitted/5, dispatch_gated/5)
- Validate protocol transitions
- Compute release readiness from declarative gates
- Trace receipt chain ancestry and detect tampering

**Key Property:** Prolog/Datalog is the ONLY source of truth for authorization, capabilities, transitions, and release status. No runtime component may maintain a duplicate copy.

**Critical Predicates:**
```prolog

% Authorization gate (SEALED ENTRY POINT)

dispatch_gated(AgentID, CapabilityID, TargetRuntime, Permission, IsPermitted)



% Capability state

capability_active(CapabilityID, IsActive)

capability_revoked(CapabilityID, RevocationReason)



% Protocol transitions

transition_valid(FromState, ToState, Action, IsValid)



% Release readiness (master query)

release_ready(IsReady)

```

---

### Layer 4: Execution Substrate — Polyglot + Verification

**Components:**
- SUBLEQ VM (One-Instruction Set Computer)
- Polyglot Frontend (30+ language parsers)
- Invariant Extractor (symbolic execution + abstract interpretation)
- M4 Morphing Engine (self-modifying cell definitions)
- Jupyter Kernel (notebook cell execution)

**Responsibilities:**
- Parse input code in any of 30+ languages
- Compile to unified bytecode then SUBLEQ
- Execute with mutation tracking and checkpointing
- Extract loop invariants and proof obligations
- Apply M4 transformations with state feedback
- Validate proofs against extracted invariants

**Key Property:** Execution is deterministic, checkpointed, and verifiable. Every mutation is recorded.

**Supported Languages (Tier 1-5):**
- **Tier 1 (Full):** Rust, Python, JavaScript, SUBLEQ
- **Tier 2 (Solid):** Haskell, Ada/SPARK, Agda, Lean 4
- **Tier 3 (Supported):** Prolog, Lisp, Scheme, BQN
- **Tier 4 (Partial):** C, Go, Zig, APL, Forth
- **Tier 5 (Experimental):** Factor, Brainfuck, J, HolyC, EmojiCode

---

### Layer 5: Evidence & Provenance — Receipts & Release

**Components:**
- Bifrost Audit Chain (WORM ledger with Blake3 hashing)
- Cryptographic Receipts (execution event records)
- Release Manifest (versioned snapshot of all 4 version layers)
- Proof Artifacts (proof terms from Agda, Ada/SPARK verification)

**Responsibilities:**
- Generate signed receipts for every execution event
- Link receipts into append-only chain with previous-hash verification
- Store proof artifacts and test results
- Generate release manifests with 4-layer version synchronization
- Enable post-hoc audit and reproducibility verification

**Key Property:** Receipts are externally signed and WORM-sealed; they cannot be modified or reordered after initial issuance.

---

## 2. Authorization & Capability Model

### Trust Hierarchy

Agents are classified by trust tier:

| Tier | Name | Capabilities | Examples |
|------|------|--------------|----------|
| **0** | Sovereign | All operations, unrestricted | metatron, seal-finalize |
| **1** | Administrator | Create agents, revoke capabilities, manage notebooks | sentinel, cipher |
| **2** | Observer | Read-only, logging, metrics collection | phantom, resonance |
| **3** | Executor | Execute code on assigned runtimes | forge, builder |
| **4** | Guest | Limited execution, no modification | test-agents, sandboxed |

### Capability Lifecycle

Each capability has:
- **Issuer:** Agent that granted the capability
- **Target:** Agent that holds the capability
- **Runtime:** Which execution environment (rust, haskell, ada, etc.)
- **Permissions:** [dispatch, execute, verify, seal, finalize, ...]
- **IssuedAt:** Unix timestamp (seconds)
- **ExpiresAt:** Unix timestamp (exclusive boundary: time < ExpiresAt)
- **Status:** active | revoked | expired

### Authorization Protocol (Sealed Entry Point)

All external dispatch MUST pass through **dispatch_gated/5**:



```prolog

dispatch_gated(AgentID, CapabilityID, TargetRuntime, Permission, IsPermitted) :-

    agent_active(AgentID, true),                          % Agent exists & active

    agent_trust_level(AgentID, TrustLevel),

    TrustLevel \= tier_2,                                  % Not observer tier

    capability_issued(CapID, _, AgentID, TargetRuntime, Perms, _, ExpiresAt),

    \+ capability_revoked(CapID, _),                      % Not revoked

    get_time(Now),

    Timestamp is floor(Now),

    Timestamp < ExpiresAt,                                % Not expired

    member(Permission, Perms),                            % Permission granted

    runtime_active(TargetRuntime, true).                  % Runtime available

```



**Critical Property:** Direct queries to `capability_active/2` or `dispatch_permitted/5` MUST be rejected at the API boundary. Only `dispatch_gated/5` is exposed to runtimes.



---



## 3. Execution Model — Five Phases



### Phase 1: Parse & Canonicalize



**Input:** Source code in any of 30+ languages or EmojiCode command  
**Output:** Canonical Instruction (deterministic JSON/CBOR)

```

Source Code (e.g., Python)

↓

Language-Specific Parser (tree-sitter or custom)

↓

Unified AST

↓

Canonicalize (CBOR encode, sort fields, normalize)

↓

Compute source_hash = Blake3(canonical_bytes)

↓

Canonical Instruction ISIR

```

### Phase 2: Authorize

**Input:** Canonical Instruction  
**Output:** Runtime Command (if authorized) or Rejection

```

Query Prolog:

  dispatch_gated(Agent, Capability, Runtime, Permission, ?)

↓

If true:

  ✓ Authorization passed → proceed to compilation

If false:

  ✗ Authorization denied → emit rejection receipt, halt

```

### Phase 3: Compile & Verify

**Input:** Authorized Canonical Instruction  
**Output:** SUBLEQ bytecode + extracted invariants + proof obligations

```

AST → Bytecode (register allocation, instruction selection)

↓

Bytecode → SUBLEQ lowering (memory layout, addressing)

↓

Symbolic execution (trace all possible computation paths)

↓

Abstract interpretation (loop invariants via interval domain)

↓

Proof obligations generated (InvariantPreservation, etc.)

↓

Pattern matching (recognize SUBLEQ idioms: Clear, Copy, Add, Loop)

```

### Phase 4: Execute & Checkpoint

**Input:** SUBLEQ bytecode + checkpoints enabled  
**Output:** Execution result + mutations log + proof violations (if any)

```

Initialize Von Neumann memory (Vec<i64>)

↓

Execute SUBLEQ instructions with mutation tracking

  For each instruction:

    - Record pre-state

    - Execute: M[b] -= M[a]; if M[b] ≤ 0 then IP = c

    - Emit mutation event (address, old_value, new_value)

    - Check invariants at loop headers

    - Checkpoint every N mutations

↓

If invariant violation:

  Rollback to last valid checkpoint

  Emit violation receipt

  Halt execution

↓

If success:

  Return outputs + mutation log

```

### Phase 5: Seal & Release

**Input:** Execution result + proof status + test reports  
**Output:** Receipt + receipt chain extension + release manifest (optional)

```

Generate execution receipt:

  {

    type: "CellExecuted",

    cell_id: "cell_0",

    output_hash: Blake3(outputs),

    invariants_satisfied: [inv1_hash, inv2_hash, ...],

    proofs_verified: [proof1_status, proof2_status, ...],

    previous_receipt_hash: (link to prior receipt),

    timestamp: get_time(),

    signature: Ed25519_sign(canonical_bytes, private_key)

  }

↓

Append to Bifrost chain

↓

If release_requested:

  Check all release gates via Prolog:

    all_proofs_satisfied(true)

    receipt_chain_sealed(true)

    no_revoked_capabilities(true)

    all_cells_complete(true)

  If all true:

    Generate release manifest with 4-layer versions

    Sign manifest

    Append to ledger

  Else:

    Emit gate failure receipt

```

---

## 4. Protocol State Machine (Transitions Module)

The system defines 8 protocol transitions:

| Stage | State | Allowed Actions | Next State |
|-------|-------|-----------------|-----------|
| **1** | Parsed | Authorize | Authorized |
| **2** | Authorized | Compile | Compiled |
| **3** | Compiled | Execute | Executing |
| **4** | Executing | Checkpoint | Checkpoint Stored |
| **5** | Checkpoint Stored | Continue/Halt | Executed |
| **6** | Executed | Verify Proofs | Verified |
| **7** | Verified | Generate Receipt | Receipted |
| **8** | Receipted | Release (optional) | Released |

**State Guard:** Each transition requires a Prolog predicate:
```prolog

transition_valid(FromState, ToState, Action, true) :-

    valid_transition(FromState, ToState),

    action_authorized(Action),

    required_facts_present(FromState).

```

---

## 5. SUBLEQ Substrate

### One-Instruction Set Computer (OISC)

SUBLEQ is the universal instruction set with a single operation:

```

SUBLEQ a b c:

  M[b] ← M[b] - M[a]

  if M[b] ≤ 0 then IP ← c

```

**Memory Model:**
- Unified Von Neumann address space (Vec<i64> in Rust)
- No separate instruction/data memory
- Self-modifying code enabled (can rewrite itself)

**Address Map (Example):**
```

M[0-9]:      Bootstrap and control flow

M[10-19]:    Cell registry (cell count, execution state)

M[20-29]:    Cell outputs (mutable, M4-readable)

M[30-39]:    M4 definitions (feedback loop state)

M[40-49]:    Extracted invariants (bytecode verification)

M[50-59]:    Proof checkpoints (WORM-sealed rollback)

M[60-69]:    Bifrost chain head (ledger anchor)

M[100+]:     Cell bytecode (grows as cells added)

```

### Why SUBLEQ?

- **Turing-complete:** Can execute any algorithm
- **Deterministic:** Every operation has a single outcome
- **Verifiable:** Simple enough for formal proof (12/12 proofs discharged in Phase 3)
- **Self-modifying:** Enables dynamic code transformation via M4
- **Canonical:** No machine-specific encoding (portable across platforms)

---

## 6. M4 Morphing & Feedback Loops

### Self-Modifying Cell Execution

M4 (a macro preprocessor) enables syntactic transformation between cells:

```

Cell N: Rust code

↓

Execute via rust runtime adapter

↓

Output captured: "x = 42; y = 100"

↓

M4 define: LAST_OUTPUT = "x = 42; y = 100"

↓

Cell N+1: M4 template includes prior output

  define(`PREV_RUST_OUTPUT', `include(`README.subleq')')

  The include() macro reads LAST_OUTPUT from Prolog facts

↓

M4 expands to:

  x = 42; y = 100;

  (Cell N+1 code can reference x and y)

↓

Compile Cell N+1 with expanded definitions

```

**Feedback Buffer:** 
- VecDeque of (definition, output) pairs
- Bounded history: 50 definitions, 100 outputs
- Prevents infinite loops via recursion depth limit

**State Preservation:**
- M4 definitions → Prolog facts (notebook_cells.pl)

- Execution outputs → WORM receipts

- Feedback → next cell's M4 context



---



## 7. Proof Integration Points



### Supported External Verifiers



| Verifier | Language | Role | Integration |

|----------|----------|------|-------------|

| **Agda** | Agda | Proof checking | invoke agda-check, capture artifact |

| **Ada/SPARK** | Ada | Contract verification | invoke gnatprove, emit proof term |

| **Haskell** | Haskell | Type-level proofs | Curry-Howard via type checking |

| **Lean 4** | Lean 4 | Interactive proving | invoke lean, parse proof state |

| **Z3** | SMT-LIB | Constraint solving | Z3 interface via smt-lib crate |



### Proof Obligations (4 Required)



Every execution must satisfy:



1. **InvariantPreservation:** All extracted loop invariants remain true

2. **SemanticPreservation:** Meaning of original source = meaning of compiled bytecode

3. **LoopInvariantMaintenance:** Loop bounds and termination conditions hold

4. **ReceiptChainIntegrity:** Receipt chain is monotonic and tamper-evident



**Discharge Mechanism:**

- Automatic: trivial proofs (no loops, pure data flow)

- Manual: user provides proof term in Agda/Ada/Lean

- SMT: Z3 solver for arithmetic constraints



---



## 8. Release Readiness (Four-Layer Versioning)



### Version Layers



A release is valid only when all four version layers are synchronized:



```

┌─────────────────────────────────────────────┐

│ Layer 1: Source Version (Git SHA-256)        │ v1.0.0 release

│ Layer 2: Protocol Version (instruction fmt)  │ format: major.minor.patch

│ Layer 3: Evidence Version (receipt schema)   │ stage 1-9 + evidence count

│ Layer 4: Knowledge Version (Prolog snapshot)  │ ontology/rules/facts identifier

└─────────────────────────────────────────────┘

    ↓ All must be compatible ↓

    release_ready/1 query
```



### Release Stages



1. **Draft** — Experimental, no guarantees

2. **Development** — Builds successfully, tests may fail

3. **Tested** — Unit tests pass in controlled env

4. **Verified** — Proof tools pass, invariants satisfied

5. **Evidence Complete** — Manifests, artifacts, benchmarks ready

6. **Candidate** — Security review complete, locked for final checks

7. **Signed** — Cryptographically signed with Ed25519

8. **Immutable** — WORM ledger seal appended

9. **Archived** — Historical reference, superseded by newer release



### Release Gate (Master Query)



```prolog

release_ready(true) :-

    all_proofs_satisfied(true),

    receipt_chain_sealed(true),

    no_revoked_capabilities(true),

    all_cells_complete(true),

    receipt_chain_valid(true),

    version_layers_compatible(true).

```

---

## 9. Repository Structure

```

rowm-polymorphic-notebook/

├── Cargo.toml                              # Workspace configuration

├── Cargo.lock                              # Dependency lock

├── README.md                               # User-facing overview

├── README.subleq                           # Isomorphic executable notebook

├── LICENSE-MIT.txt                         # MIT license

├── LICENSE-APACHE2.txt                     # Apache 2.0 license

│

├── crates/                                 # Rust implementation

│   ├── subleq-vm/                          # SUBLEQ execution engine

│   │   ├── src/vm.rs                       # VM core (mutation tracking)

│   │   ├── src/memory.rs                   # Von Neumann unified memory

│   │   ├── src/checkpoint.rs               # WORM checkpoint system

│   │   └── src/telemetry.rs                # Live mutation telemetry

│   ├── subleq-ir/                          # Intermediate representation

│   │   ├── src/ast.rs                      # Unified AST

│   │   ├── src/bytecode.rs                 # Stack-based IR

│   │   ├── src/lowering.rs                 # AST → Bytecode

│   │   └── src/subleq_codegen.rs           # Bytecode → SUBLEQ

│   ├── polyglot-frontend/                  # 30+ language parsers

│   ├── invariant-extractor/                # Symbolic + abstract interp

│   ├── proof-validator/                    # Curry-Howard checker

│   ├── m4-morph/                           # M4 macro engine

│   ├── notebook-kernel/                    # Jupyter protocol

│   └── notebook-orchestrator/              # Non-recursive executor

│

├── logic/                                  # Prolog/Datalog authority

│   ├── facts/

│   │   ├── agents.pl                       # Agent definitions

│   │   ├── runtimes.pl                     # Runtime manifests

│   │   ├── capabilities.pl                 # Capability leases

│   │   ├── notebook_cells.pl               # Cell inventory

│   │   └── receipts.pl                     # Receipt chain

│   ├── rules/

│   │   ├── authorization.pl                # Dispatch gates

│   │   ├── transitions.pl                  # State machine

│   │   ├── proofs.pl                       # Proof obligations

│   │   ├── provenance.pl                   # Receipt tracing

│   │   └── release.pl                      # Release readiness

│   └── queries/

│       └── test_queries.pl                 # Validation tests

│

├── schemas/                                # JSON/CBOR schemas

│   ├── instruction_schema.json             # Canonical instruction

│   ├── capability_schema.json              # Capability object

│   └── receipt_schema.json                 # Receipt record

│

├── isomorphic-shift/                       # Formal translation layer

│   ├── schemas/

│   │   ├── domains.schema.json             # 14 domain definitions

│   │   └── canonical.schema.json           # ISIR specification

│   ├── logic/

│   │   ├── shifts.pl                       # 8 shift registrations

│   │   ├── domains.pl                      # Domain facts

│   │   ├── invariants.pl                   # 23 invariants

│   │   ├── shift_authorization.pl          # Auth matrix

│   │   ├── semantic_equivalence.pl         # Round-trip laws

│   │   └── shift_release.pl                # 12 release gates

│   └── docs/

│       └── architecture.md                 # Mapping specifications

│

└── docs/                                   # User documentation

    ├── ARCHITECTURE.md                     # This file

    ├── PROTOCOL.md                         # State machine (next)

    ├── THREAT_MODEL.md                     # Security analysis

    ├── API_REFERENCE.md                    # Crate APIs

    └── CONTRIBUTING.md                     # Contributor guide

```

---

## 10. Build & Deployment

### Prerequisites

- Rust 1.78+
- GNU M4 (for morphing engine)
- SWI-Prolog 8.x+ (for logic engine)
- (Optional) Agda, Ada/SPARK, Lean 4 for proof verification

### Build

```bash

cd rowm-polymorphic-notebook

cargo build --release --workspace

```

### Test

```bash

# Rust tests (82/82 passing)

cargo test --all --lib



# Prolog tests (13/13 passing)

swipl -f logic/facts/*.pl -f logic/rules/*.pl -f logic/queries/test_queries.pl -t run_tests



# Release readiness check

swipl -f logic/facts/*.pl -f logic/rules/*.pl -t "release_ready(R), format('Result: ~w~n', [R])."

```

### Deployment Targets

- **Docker:** `docker build -t rowm:1.0.0 .` (when Dockerfile created)
- **Crates.io:** `cargo publish` (when build is stable)
- **GitHub Pages:** Docs auto-deploy on push to main

---

## 11. Security Model

### Threat Model Summary

**In-Scope Threats:**
- Unauthorized code execution (mitigated by dispatch_gated)

- Capability bypass (mitigated by Prolog authority)

- Expired/revoked capability reuse (mitigated by timestamp checks)

- Receipt tampering (mitigated by Blake3 + Ed25519)

- Out-of-order execution (mitigated by monotonic sequencing)



**Out-of-Scope Threats:**

- Physical attacks on hardware

- Compromised Rust runtime or Prolog interpreter

- Malicious kernel/OS interference

- Supply chain attacks on dependencies



**Design Principle:** Assume Prolog/Datalog engine is trustworthy. All external code is untrusted until authorized.



---



## 12. Known Limitations



- **HMAC Cryptography:** Current implementation uses HMAC-SHA256 (symmetric); Ed25519 (asymmetric) not yet deployed

- **Timestamp Nondeterminism:** Receipt timestamps make reproducibility imperfect; recommend canonical time injection

- **No Cross-System Replay Protection:** Receipts can be replayed if system clock is manipulated

- **Notebook Mutation Detection:** No enforcement preventing post-seal cell edits in .ipynb files

- **Jupyter Integration:** Kernel exists but integration tests are incomplete

- **Proof Tool Integration:** Agda/Ada/Lean invocations are stubs; manual proof term submission required



See `docs/THREAT_MODEL.md` for detailed security analysis.

---

**Built with Ahmad's Sovereign Architecture + Jessica's SNAPKITTYWEST engineering discipline.**

*"LOC WRITES. LEDGER CERTIFIES. METATRON SEALS."*