Skip to main content

​
Architecture Overview

BRIK-64 is a Digital Circuitality architecture — software that works like hardware. Every program is a Printed Circuit Description (PCD), compiled through a formally verified pipeline into a standalone native binary. The compiler is self-hosting: it compiles itself, and the output hash is immutable and reproducible.

​
The Full Pipeline

  ┌─────────────────────────────────────────────────────────────────────────┐
  │                         BRIK-64 Compiler Pipeline                       │
  │                                                                         │
  │  Source (.pcd)                                                          │
  │       │                                                                 │
  │       ▼                                                                 │
  │  ┌──────────────────────────────────────────────────────────────────┐   │
  │  │  hand_parser                                                     │   │
  │  │  • Recursive descent, hand-written (no parser generators)       │   │
  │  │  • MAX_DEPTH = 256 (stack overflow prevention)                  │   │
  │  │  • No binary literals (0b...), no implicit coercions            │   │
  │  │  • Produces: AST (algebraic data types)                         │   │
  │  └──────────────────────────────────────────────────────────────────┘   │
  │       │                                                                 │
  │       ▼  AST                                                            │
  │  ┌──────────────────────────────────────────────────────────────────┐   │
  │  │  planner                                                         │   │
  │  │  • SSA form (Static Single Assignment)                          │   │
  │  │  • Type inference + type checking                               │   │
  │  │  • WhileLoop SSA: loop-carried vars pinned to version 0         │   │
  │  │  • EVA Algebra inference: ⊗ ∥ ⊕ from control flow              │   │
  │  │  • Produces: CPF (Canonical Plan Format, JSON IR)               │   │
  │  └──────────────────────────────────────────────────────────────────┘   │
  │       │                                                                 │
  │       ▼  CPF (JSON IR)                                                  │
  │  ┌──────────────────────────────────────────────────────────────────┐   │
  │  │  TCE (Thermodynamic Coherence Engine)                           │   │
  │  │  • Computes: E_c, H_d, S_d, C_s, ETC, ΔN, Φ_c                 │   │
  │  │  • Φ_c = 1.000 required to proceed                             │   │
  │  │  • Ω = 1 ↔ certified (binary, no partial certification)        │   │
  │  └──────────────────────────────────────────────────────────────────┘   │
  │       │                                                                 │
  │       ▼  CPF (certified)                                                │
  │  ┌──────────────────────────────────────────────────────────────────┐   │
  │  │  Backends (parallel emission)                                   │   │
  │  │                                                                 │   │
  │  │  ┌──────────────┐  ┌───────────────┐  ┌──────────────────────┐ │   │
  │  │  │ Native x86-64│  │  BIR bytecode │  │   Rust / JS / Python │ │   │
  │  │  │ (standalone  │  │  (BRIK IR,    │  │   (transpilation     │ │   │
  │  │  │  ELF, no     │  │   interpreted │  │    backends)         │ │   │
  │  │  │  libc)       │  │   or JIT)     │  │                      │ │   │
  │  │  └──────────────┘  └───────────────┘  └──────────────────────┘ │   │
  │  │                                                                 │   │
  │  │  ┌──────────────────────┐  ┌──────────────────────────────────┐ │   │
  │  │  │ WebAssembly (wasm32) │  │  BPU machine code (future)       │ │   │
  │  │  └──────────────────────┘  └──────────────────────────────────┘ │   │
  │  └──────────────────────────────────────────────────────────────────┘   │
  └─────────────────────────────────────────────────────────────────────────┘

​
Compiler Layers

The parser is entirely hand-written — no nom, no pest, no lalrpop. This is a deliberate architectural decision: parser generators introduce a dependency that is outside the formally verified perimeter.Key properties:
  • MAX_DEPTH = 256 — hard limit on recursion depth, preventing stack exhaustion
  • No binary literals (0b...) — all integers are decimal or hexadecimal
  • No implicit type coercions in the grammar — all conversions are explicit monomer calls
  • Single-pass: the parser does not backtrack
  • Whitespace-insensitive (tokens are delimited by the grammar, not layout)
AST node types produced:
  • Expr: literals, binops, unops, calls, monomer calls, array/struct literals
  • Stmt: let-bindings, assignments, if/else, while, loop(N), return, break, continue
  • FnDef: function definitions with typed parameters and return type
  • Program: list of top-level definitions (functions + imports)
The parser enforces that PCD is a closed language: you cannot refer to undefined identifiers, call undefined functions, or escape the 64-monomer vocabulary.
The planner transforms the AST into CPF (Canonical Plan Format), a JSON-based intermediate representation in Static Single Assignment form.SSA rules:
  • Every variable assignment creates a new versioned slot: x_0, x_1, x_2, …
  • loop(N) loop-carried variables: all rebindings use version 0 (same slot). This is the critical invariant that makes the BIR bootstrap work — the planner and brikc.pcd must agree.
  • while loops: SSA captures the version before the body (known limitation, use loop(N) with if guard as workaround in self-hosting code)
  • bind_let always assigns version 0 for loop-carried vars
Type inference:
  • All monomers have fixed input/output types (specified in Coq proofs)
  • The planner infers the type of every SSA variable by propagation
  • Type errors are hard errors — no implicit coercions
EVA Algebra inference:
  • The planner classifies every composition: sequential ⊗, parallel ∥, conditional ⊕
  • This classification is embedded in the CPF and later verified by the TCE
CPF is the universal intermediate representation shared by all backends. It is a JSON document with a stable schema (versioned). Any backend consumes CPF; the pipeline from source to CPF is backend-agnostic.
{
  "version": "2.0",
  "functions": [
    {
      "name": "add_two",
      "params": [{"name": "a", "type": "I64"}, {"name": "b", "type": "I64"}],
      "return_type": "I64",
      "body": [
        {"op": "CALL_MC", "mc": 0, "args": ["a_0", "b_0"], "out": "r_0"},
        {"op": "RET", "val": "r_0"}
      ],
      "eva": "sequential"
    }
  ]
}
CPF is designed to be:
  • Deterministic: same source always produces the same CPF (no random IDs, no timestamps)
  • Diffable: human-readable JSON, suitable for version control
  • Complete: contains all type information, EVA algebra annotations, and TCE pre-images
Native x86-64 ELF (primary):
Produces a fully standalone ELF binary. No libc, no dynamic linker, no runtime. The binary contains only: startup stub + monomer implementations + EVA router + program logic.BIR Bytecode:
BRIK IR — a stack-less, register-based bytecode interpreted by the BIR interpreter (Rust). Used during bootstrap: Gen0 compiles brikc.pcd to BIR, BIR executes to produce Gen1.Rust / JS / Python:
Transpilation backends that emit idiomatic code in each target language. Each monomer maps to a verified library function in the target language. Used for interoperability.WebAssembly:
All 22 CPF PlanNode variants are covered. Produces .wasm modules that run in any WASM runtime. Sandboxed — no filesystem access by default.

​
The 14 Rust Crates

brik_parser

software/system/brik_parser/
The hand-written recursive descent parser. Produces AST from .pcd source text. MAX_DEPTH=256 enforced here.

brik_planner

software/system/brik_planner/
SSA transformation, type inference, EVA algebra classification. Produces CPF.

brik_tce

software/system/brik_tce/
Thermodynamic Coherence Engine. Computes all 7 metrics and Φ_c. Blocks compilation if Φ_c ≠ 1.

brik_codegen

software/system/brik_codegen/
Native x86-64 code generator. Emits raw machine code bytes from CPF.

brik_linker

software/system/brik_linker/
ELF linker. Assembles .text, .rodata, .bss sections into a valid ELF64 executable. rodata-aware: string constants are placed in .rodata, referenced by RIP-relative addressing.

brik_bir

software/system/brik_bir/
BIR compiler: CPF → BIR bytecode. BIR interpreter: executes BIR at ~28M instructions/second.

brik_native

software/system/brik_native/
Native runtime: startup stub, monomer implementations, EVA router, system call wrappers.

brik_eva

software/system/brik_eva/
EVA Algebra runtime: ⊗ ∥ ⊕ combinators, compatibility checker, composition verifier.

brik_monomers

software/system/brik_monomers/
All 64 Core monomer implementations (MC_00–MC_63) + Coq proof bindings.

brik_stdlib

software/system/brik_stdlib/
Standard library in PCD: math.pcd, string.pcd, array.pcd, io.pcd, fmt.pcd, json.pcd.

brik_wasm

software/system/brik_wasm/
WebAssembly backend. All 22 PlanNode variants implemented.

brik_transpile

software/system/brik_transpile/
Rust/JS/Python transpilation backends. Monomer-to-stdlib mappings for each target.

brik_cli

software/system/brik_cli/
CLI frontend: brikc build, brikc check, brikc fmt, brikc repl, brikc lsp, brikc wasm32.

brik_self

software/system/brik_self/
Self-compilation driver: bootstrap chain, Ralph loop, fixpoint verifier.

​
Native x86-64 ELF: Startup Stub

Every BRIK-64 native binary begins with a 197-byte startup stub that establishes the runtime environment before the first monomer executes. The stub uses dedicated registers as global pointers:
RegisterPurposeSize
R15vstack base pointer4 MB
R13ASCII scratch buffer512 bytes
R12heap base pointer16 MB
RSPcall stack (64 MB mmap)64 MB
; BRIK-64 startup stub (conceptual assembly, ~197 bytes)
_start:
    ; 64 MB call stack
    mov  rdi, 0
    mov  rsi, 67108864          ; 64 MB
    mov  rdx, PROT_READ | PROT_WRITE
    mov  r10, MAP_PRIVATE | MAP_ANONYMOUS
    mov  r8,  -1
    xor  r9d, r9d
    mov  rax, 9                  ; sys_mmap
    syscall
    lea  rsp, [rax + 67108864]   ; stack grows down

    ; 4 MB virtual stack (R15)
    ; 16 MB heap (R12)
    ; 512B ASCII buffer (R13)
    ; ... (similar mmap calls)

    call main_program
    mov  rax, 60                 ; sys_exit
    xor  rdi, rdi
    syscall
The startup stub is not linked from a .o file — it is emitted as raw bytes by brik_linker directly into the ELF .text section header. This eliminates any dependency on system assemblers or linkers (ld, as). The entire toolchain is self-contained.

​
Self-Compilation Fixpoint

The most important property of BRIK-64: the compiler compiles itself and produces an identical hash across all generations. This is the 4-stage fixpoint, verified on 2026-03-10.
1

Stage 0 — Bootstrap Generation

The Rust-implemented bootstrap (brik_self) compiles brikc.pcd using the BIR interpreter. This produces Gen1 BIR: 285,978 bytes, 109 functions, 20,709 BIR instructions. Duration: ~348 seconds on ECO server.
2

Stage 1 — Gen1 Compiles brikc.pcd

Gen1 BIR executes under the BIR interpreter to compile brikc.pcd again. Produces Gen2 BIR. Duration: ~178 seconds additional.
3

Stage 2 — Gen2 Compiles brikc.pcd

Gen2 BIR compiles brikc.pcd → Gen3 BIR. Duration: ~155 seconds additional. Total elapsed: ~681 seconds.
4

Stage 3 — Fixpoint Verification

SHA256(Gen1) == SHA256(Gen2) == SHA256(Gen3) == SHA256(Gen4)
All four generations produce the same hash:
7229cfcde9613de42eda4dd207da3bac80d2bf2b5f778f3270c2321e8e489e95
Test stage_gen3_gen4_fixedpoint passes in the integration test suite. Dispatch ELF fixpoint: 9cbad73a5f5699abc5654ace9a396f7af042be56b80de3de49d5ce03cd23dcfa
The fixpoint is not a property of the hash algorithm. It is a mathematical consequence of EVA Algebra’s closure theorem: if every monomer is verified (Φ_c = 1) and every composition preserves Φ_c = 1, then the compiler’s output is determined solely by its input — there is no hidden state, no non-determinism, no timestamp. The hash is therefore stable across machines, operating systems, and time.

​
Trust Layer Diagram

  ┌──────────────────────────────────────────────────────┐
  │  Layer 4: Coq Proofs (207 files)                     │  ← Mathematical bedrock
  │  Lemmas: monomer correctness, EVA closure, TCE bounds │
  └──────────────────────────────────────────────────────┘
                         │ verifies
  ┌──────────────────────────────────────────────────────┐
  │  Layer 3: TCE (Φ_c = 1 certification)               │  ← Formal certification gate
  │  E_c, H_d, S_d, C_s, ETC, ΔN, Φ_c for every CPF    │
  └──────────────────────────────────────────────────────┘
                         │ certifies
  ┌──────────────────────────────────────────────────────┐
  │  Layer 2: EVA Algebra (⊗ ∥ ⊕)                       │  ← Composition laws
  │  Closure theorem: certified ⊗ certified = certified  │
  └──────────────────────────────────────────────────────┘
                         │ composes
  ┌──────────────────────────────────────────────────────┐
  │  Layer 1: 64 Core Monomers (MC_00–MC_63)             │  ← Atomic verified units
  │  Each: domain, range, termination, determinism       │
  └──────────────────────────────────────────────────────┘
                         │ executes on
  ┌──────────────────────────────────────────────────────┐
  │  Layer 0: Hardware (x86-64 / BPU future)             │  ← Physical substrate
  │  10⁻¹⁹ error rate — only failure mode for certified  │
  └──────────────────────────────────────────────────────┘

​
Test Suite Statistics

SuiteTestsStatus
Workspace total1,900+All green
Integration (fixpoint)34 suites0 FAILED
Stage1 bootstrap11PASS (13s)
Coq proofs (admitted)0All replaced with DEFERRED comments
# Build and test
cargo build --workspace
cargo test --workspace          # 1,900+ tests, must be 0 failures
cargo clippy --workspace        # must be 0 warnings
Do not run cargo test --workspace locally if your machine has less than 32 GB RAM and an SSD. The full test suite including bootstrap integration tests takes more than 10 minutes. Use the ECO server (ssh eco-ts) for test runs.