Prolog8 — Byte-Capped Proof Engine

A compact, deterministic inference engine for proof generation and receipt-chain validation.

Purpose

Prolog8 evaluates queries against fact blocks and Horn rules, emitting typed proof DAGs with BLAKE3 receipt chains. Designed for lightweight embedded use cases where bounded memory is critical.

Use cases:

• Proof-of-admissibility gates in autonomic systems
• Receipt chain validation in manufacturing pipelines
• Bounded-recursion logic programming with cryptographic proof

Capabilities

Byte Caps (MVPs)

Query & Proof Flow

1. Admission — Validate atoms and rules against caps via admit_atom() / admit_rule()
2. Fact loading — Load FactBlock8 into kernel
3. Query execution — kernel.query() evaluates atoms, returns typed proofs
4. Proof DAG — Typed nodes: ProofKind::Fact, ProofKind::Rule, ProofKind::MissingFact
5. Receipt chain — BLAKE3 six-root receipt with integrity hash

Rule Chaining

Currently supports: One-step chaining only (depth-1 recursion).

Planned: Bounded recursion via FeatureBit::BoundedRecursion (out of scope for MVP).

Decision Types

API

Rust (Public Interface)

use prolog8::{
    Kernel, Catalog, PredicateMeta, PredicateProofPolicy,
    Atom8, Rule8, FactBlock8, QueryAtom8, ProofMode,
    admit_atom, admit_rule, replay,
};

// 1. Build catalog
let mut cat = Catalog::new(CatalogId(1));
cat.add_predicate(PredicateMeta { ... });

// 2. Create kernel
let mut kernel = Kernel::new(cat);

// 3. Load facts
kernel.load_facts(FactBlock8::new(pred_id, arity, facts))?;

// 4. Load rules
kernel.load_rule(rule)?;

// 5. Query
let result = kernel.query(&QueryAtom8 { ... });

// 6. Verify receipt
let status = replay(&kernel, &query, &receipt);
assert_eq!(status, ReplayStatus::Verified);

WASM (JavaScript/Node.js)

const wasm = require('@wasm4pm/prolog8');

const input = {
  catalog: { /* Catalog */ },
  facts: [ /* FactBlock8 */ ],
  rules: [ /* Rule8 */ ],
  query: { /* QueryAtom8 */ }
};

const result = JSON.parse(wasm.prolog8_query(JSON.stringify(input)));
// result = { ok/answered: [...], denied, invalid }

// Verify receipt
const verifyInput = { ...input, receipt: result.receipt };
const status = JSON.parse(wasm.prolog8_replay(JSON.stringify(verifyInput)));
// status = { Verified | ReceiptInvalid | Mismatch }

Testing

Unit Tests (31 tests)

• Inline tests in src/**/*.rs
• Test internal correctness, bounds checking, serialization

Integration Tests (11 tests)

Location: tests/kernel_integration.rs

• Public API: fact admission, queries, receipts, replay
• Covers known-fact/unknown-fact paths
• Rule chaining
• Receipt determinism

AAT Live Counterfactual Tests (36 tests)

Location: tests/aat_live_counterfactual.rs

8 families of adversarial probes:

Running Tests

# All tests
cargo test -p prolog8 --lib
cargo test -p prolog8 --test kernel_integration
cargo test -p prolog8 --test aat_live_counterfactual

# Single test
cargo test -p prolog8 --test aat_live_counterfactual cf1_arity_beyond_cap_rejected

# With output
cargo test -p prolog8 --test aat_live_counterfactual -- --nocapture

Known Limits (Documented)

Out of Scope for MVP

• Multi-step recursion — Only depth-1 rule chaining supported
• Negation as failure — Declared in feature bit, not wired
• Aggregates — Declared in feature bit, not wired
• Built-in predicates — Declared in feature bit, not wired
• Foreign predicates — Declared but not accessible

Acceptable Behavior

• Sentinel term ID — TermId(0) may be used in queries without explicit error (no boundary check)
• Feature mask validation — Always passes (no-op, FeatureBit::ALL = 0xFF masks 8 bits, guard never fires)

Production Readiness Checklist

• 31 unit tests pass
• 11 integration tests pass (proof + receipt flows)
• 36 AAT counterfactual tests pass (adversarial boundaries)
• No compiler warnings (cargo build -p prolog8 --features wasm)
• Admission boundaries enforced (arity, body_len, binding_mask)
• Receipt integrity verified via replay()
• Deterministic across independent runs
• Domain keys (BLAKE3) pairwise distinct

Build & Deploy

Rust Library

cd wasm4pm
cargo build -p prolog8 --release

WASM (Node.js target)

cd crates/prolog8
wasm-pack build --target nodejs --out-dir ../../packages/prolog8/pkg

npm Package

Published as @wasm4pm/prolog8 (TypeScript bindings in packages/prolog8/src/).

Architecture

Directory Structure

crates/prolog8/
├── src/
│   ├── lib.rs              # Root, module exports
│   ├── types.rs            # Atom8, Rule8, Receipt, domain constants
│   ├── catalog.rs          # Predicate registry and term internment
│   ├── kernel.rs           # Query evaluation, one-step rule chaining
│   ├── admission.rs        # Atom/rule boundary enforcement
│   ├── hash.rs             # BLAKE3 domain-separated hashing
│   ├── replay.rs           # Receipt verification
│   └── wasm.rs             # wasm-bindgen exports (ARD section 13)
├── tests/
│   ├── kernel_integration.rs      # 11 integration tests
│   └── aat_live_counterfactual.rs # 36 AAT tests (8 families)
└── Cargo.toml

Key Modules

• types — Atom8, Rule8, FactBlock8, FactRow8, QueryAtom8, Receipt, ProofNode, Decision
• catalog — Catalog::new(), add_predicate(), intern_term(), term_id()
• kernel — Kernel::new(), load_facts(), load_rule(), query(), scan_rules()
• admission — admit_atom(), admit_rule(), RejectionCode enum
• hash — BLAKE3 domain keys (6 roots: catalog, rule, fact, input, proof, output)
• replay — replay(), ReplayStatus enum

Proof DAG Structure

Decision {
  kind: Allow | Deny | Invalid,
  proof: [ProofNode],      // Typed nodes forming DAG
  receipt: Receipt,         // BLAKE3 six-root chain
  timestamp: u64
}

ProofNode {
  kind: Fact | Rule | MissingFact,
  id: u32,
  atom: Atom8,
  children: Vec<u32>,      // Indices into proof vec
  proof_root: [u8; 32]     // BLAKE3 hash of this node
}

Receipt {
  receipt_hash: [u8; 32],  // compute_hash() for integrity
  proof_root: [u8; 32],
  catalog_root: [u8; 32],
  rule_root: [u8; 32],
  fact_root: [u8; 32],
  input_root: [u8; 32],
  output_root: [u8; 32]
}

WASM Constraints

• Single-threaded execution — No Arc<RwLock>, use RefCell<HashMap>
• No async — All operations synchronous
• Input limit — 10MiB max (validated in wasm.rs)
• Serialization — JSON in, JSON out (via serde_json)

References

• ARD Section 13 — WASM ABI byte-buffer surface
• Chicago TDD Constitution — Van der Aalst event-log-as-proof doctrine
• AAT (Adversarial Admissibility Testing) — Oracle Ranks 1-5 (TESTING.md)