Skip to main content

BRIK-64 Glossary

This glossary defines every term used in the BRIK-64 ecosystem. Terms are grouped thematically, not alphabetically, because many concepts build on each other.

Core Concepts

Digital Circuitality

The formal property of a computational system that operates as a closed circuit. A system has Digital Circuitality when: every input domain is bounded, every operation is formally verified, every output range is proven, and no external noise can introduce undefined behavior. Measured by the Φ_c metric. Φ_c = 1 means the circuit is closed. Φ_c < 1 means it is not.

Digital Circuitry

The discipline of building programs as circuits. Just as electrical engineering has circuit design rules (Kirchhoff’s laws, impedance matching), Digital Circuitry has formal composition rules (EVA algebra, CMF certification). BRIK-64 is the first complete implementation of this discipline.

PCD — Printed Circuit Description

The programming language of BRIK-64. A PCD file (.pcd) is a circuit schematic — not a script. It describes computation in terms of monomer calls and EVA compositions. The name is intentional: a PCD program is to software what a PCB (Printed Circuit Board) layout is to hardware.
PC add_circuit {
    let result = MC_00.ADD8(a, b);
    OUTPUT result;
}

Monomer

An atomic verified operation. The smallest unit of computation in BRIK-64. A monomer has a formally proven domain (input range), codomain (output range), postcondition, and termination guarantee. Analogous to a logic gate in electronics. 128 monomers are defined: 64 Core (MC_00–MC_63) with Coq proofs and 64 Extended (MC_64–MC_127) with CONTRACT closure.

Polymer

A composition of monomers. Just as polymers in chemistry are chains of monomers, a BRIK-64 polymer is a program built by composing monomers via EVA operators. A polymer inherits the formal properties of its constituent monomers if composed correctly (i.e., if Φ_c = 1 holds across the composition).

PC (Program Circuit)

A named polymer — a top-level PCD construct that defines a complete computation. A PC block is the unit of compilation and certification.
PC my_circuit {
    // monomer calls and EVA compositions
    OUTPUT 0;
}

The 128 Monomers

MC_XX (Monomer Code)

Notation for a specific monomer. MC_00 is ADD8, MC_63 is SYSINFO. The two-digit decimal index identifies the monomer uniquely across all targets and representations. Always padded to two digits (MC_07, not MC_7).

MC_00–MC_63 · Core Monomers

The 64 formally verified atomic operations that form the BRIK-64 certified tier. Organized in 8 families of 8:
FamilyRangeDomain
F0 ArithmeticMC_00–07Saturating integer math
F1 LogicMC_08–15Bitwise operations, shifts, rotations
F2 MemoryMC_16–23Load, store, alloc, free, CAS, fence
F3 ControlMC_24–31IF, JUMP, CALL, RET, LOOP
F4 I/OMC_32–39Read, write, open, close, seek
F5 StringMC_40–47Concat, split, length, match
F6 CryptoMC_48–55Hash, HMAC, AES, signing
F7 SystemMC_56–63Time, sleep, env, PID

MC_64–MC_127 · Extended Monomers

64 additional monomers covering floating point, networking, graphics, audio, concurrency, and FFI. Operate under declared contracts (CONTRACT closure), not Coq proofs. Implemented in v4.0.0-beta.2. See the Roadmap.

Saturating Arithmetic

The behavior of BRIK-64 arithmetic monomers when results would overflow or underflow: they clamp to the boundary value instead of wrapping or trapping. ADD8(200, 100)255, not 44. This is a formal domain guarantee — overflow is impossible by construction.

EVA Algebra

EVA (Equation-Verified Assembly)

The formal composition algebra of BRIK-64. Three operators allow monomers and polymers to be composed while preserving formal properties.

⊗ Sequential Composition

f ⊗ g — apply f, then apply g to the result. The output type of f must match the input type of g. Implemented as eva.seq(f, g) in all libraries.
const process = eva.seq(mc.add8, mc.mod8);
// Φ_c = 1 if both monomers are Core

∥ Parallel Composition

f ∥ g — apply f and g independently to separate inputs, producing a tuple of outputs. Implemented as eva.par(f, g).
combined = eva.par(mc.add8, mc.hash_sha256)
result_tuple = combined(10, b"data")

⊕ Conditional Composition

pred ⊕ (f, g) — apply predicate, route to f if true, to g if false. Implemented as eva.cond(pred, f, g).
let route = eva::cond(|x| x > 128, mc::add8, mc::sub8);

Closure (Φ_c = 1)

A composition is closed if every path through it stays within proven domains. An EVA composition of Core monomers is closed by construction. The CMF verifies closure at compile time. If Φ_c ≠ 1, the program does not compile.

CMF — Coherence Metric Framework

CMF

The Coherence Metric Framework. The component of the brikc compiler that measures and enforces formal structural properties. It runs on every compilation and rejects programs that do not meet certification thresholds. All CMF metrics are structural/graph-theoretical — they analyze program topology, not physical energy.

Φ_c (Phi-c) — Circuit Closure

The primary certification metric. Computed as: Φ_c(C) = (n_consumed / n_in) · (n_produced / n_out) · 𝟙[V(C) = 1]. Φ_c = 1 means the program is a closed circuit — every input is consumed, every output is produced, and the verification function passes. Φ_c < 1 means the circuit is open and will not compile in certified mode.

δ (delta) — Unused Input Ratio

The fraction of declared inputs that are never consumed by the circuit. δ = 0 means every input is used. δ > 0 indicates dead inputs — a structural defect that prevents certification. The compiler rejects programs with δ ≠ 0 in certified mode.

V(C) — Verification Status

Binary. V(C) = 1 means every monomer in the circuit has a valid Coq proof and every composition satisfies type compatibility. V(C) = 0 means at least one component is unverified.

e — Operational Complexity

The number of monomer invocations in the circuit. A structural measure of program size.

h — Signature Distance

The type-distance between input and output types across compositions. Measures how much type transformation occurs through the circuit.

s — Structural Entropy

A measure of branching complexity across all conditional (⊕) nodes. Higher s means more decision points.

c — Cyclomatic Complexity

The number of linearly independent paths through the circuit. Derived from the control-flow graph.

t — Termination Depth

The maximum nesting depth of loops and recursive calls. Bounded by MAX_DEPTH = 256.

Ω (Omega) — Certification Status

Binary. Ω = 1 means the program satisfies all primary metrics (Φ_c = 1, δ = 0, V(C) = 1) and holds a valid certificate in the public registry. Ω = 0 means it does not. A program with Ω = 1 is a certified circuit.

Compilation Targets and Formats

BIR — BRIK Intermediate Representation

The bytecode format produced by the BRIK-64 compiler frontend before backend code generation. Human-readable text format (similar to LLVM IR). BIR is the canonical representation from which all backends (native, Rust, JS, Python, WASM) are generated. A Gen1 BIR is the BIR produced by the Rust bootstrapper; Gen2 is produced by compiling that BIR with itself.
FUNC fn::add_and_mod
  LOAD $a
  LOAD $b
  CALL_MC 0        ; MC_00 ADD8
  STORE $tmp
  LOAD $tmp
  CALL_MC 6        ; MC_06 MOD8
  STORE $result
  RET $result
END

ELF — Executable and Linkable Format

The binary format used for native Linux/Unix executables and shared libraries. The brikc compiler produces a standalone ELF — a self-contained x86-64 binary that requires no Rust runtime, no libc, and no dynamic linker. The brikc compiler itself is a 708 KB ELF.

CPF — Canonical Plan Format

The intermediate JSON representation produced by the BRIK-64 planner (after type checking and SSA transformation, before backend emission). All backends consume CPF. It is the stable API between the frontend and all code generators.

SSA — Static Single Assignment

A compiler IR property where every variable is assigned exactly once. The BRIK-64 planner transforms PCD programs into SSA form, enabling formal verification of data flow. Loop-carried variables are handled by the bind_let mechanism.

WASM / WebAssembly

One of the five compilation targets. brikc compile src/main.pcd --target wasm32 produces a .wasm binary that runs in any WebAssembly host (browsers, Node.js, WASI runtimes).

Self-Hosting Fixpoint

The state where the brikc compiler can compile its own source code and produce an identical binary across multiple generations. Gen1 = Gen2 = Gen3 = Gen4 (hash 7229cfcde961...). Achieved in v2.0.0. This is the mathematical proof that the compiler is correct: if it were not, it would produce different output when compiling itself.

Certification Registry

Registry

The public, immutable database of certified BRIK-64 programs. Every program with Ω = 1 can be submitted to the registry. Its certificate (hash + CMF metrics + timestamp) is recorded in the BRIK-64 Certification Registry and is queryable via REST API and live badge endpoints.

Circuit Package

A certified PCD program (Ω = 1) published to the BRIK-64 registry. Analogous to an npm package, a Cargo crate, or a PyPI package — but instead of distributing source code or compiled binaries, the registry distributes formally proven circuits. Any consumer of a circuit package receives the Coq-backed guarantee that the circuit’s behavior is exactly what the certificate describes.

Live Badge

An SVG badge served by https://badge.brik64.dev/{hash} that reflects real-time certification status. If the program’s hash matches the registry entry, the badge shows CERTIFIED. If the hash changes (program modified), the badge shows INVALID automatically — without any action from the author.

Merkle Anchor

The cryptographic proof of a registry entry. The certificate hash is included in a Merkle tree whose root is recorded in the certification registry with a unique hash. This makes the certification timestamp permanently verifiable without trusting any central server.

Pro Tier

The BRIK-64 subscription tier that enables:
  • Submitting certified programs (Ω = 1) to the public registry
  • Publishing circuit packages for others to import
  • Receiving live badge endpoints for README integration
  • Revocation management
  • Private registry for internal programs

Hardware

BPU — BRIK Processing Unit

A hardware coprocessor where all 64 Core monomers are implemented in silicon. The EVA Router connects them as an electrical network. The TCE Unit enforces Φ_c = 1 at clock speed and emits a non-maskable BLOCK signal when a violation is detected. Software cannot override a BLOCK. See the Roadmap for the development timeline.

EVA Router

The hardware component of the BPU that routes data between monomer units according to EVA composition rules (⊗, ∥, ⊕). Implemented as configurable wiring — the compiler generates a routing configuration from the PCD source, and the BPU executes it deterministically.

CMF Unit

The hardware component of the BPU that continuously measures Φ_c during execution. If the circuit closure metric drops below 1 (a forbidden state is reached), the CMF Unit asserts a BLOCK signal that halts execution at the pin level — before the CPU has a chance to process the result.

Non-Maskable BLOCK

A hardware signal from the BPU’s CMF Unit that cannot be suppressed by software. Analogous to a non-maskable interrupt (NMI) but stronger: it prevents the instruction from completing, not just interrupts it afterward. Once a BPU is configured with a policy circuit (Ω = 1), the circuit’s constraints are enforced at the hardware level.

Libraries and Packages

brik64-core (Rust)

The official Rust crate providing all 128 monomers (64 Core + 64 Extended) and EVA operators. Available on crates.io. Install: cargo add brik64-core.

@brik64/core (JavaScript/TypeScript)

The official npm package providing all 128 monomers (64 Core + 64 Extended) and EVA operators. Dual ESM/CJS build with TypeScript types. Available on npmjs.com. Install: npm install @brik64/core.

brik64 (Python)

The official PyPI package providing all 128 monomers (64 Core + 64 Extended) and EVA operators. Requires Python 3.10+. Available on pypi.org. Install: pip install brik64.

brik64-bir (Rust)

The BIR bytecode interpreter, available as a standalone Rust crate. Used for stage-by-stage bootstrap verification and embedding the BRIK-64 runtime in other Rust programs.

Certification Badges

BadgeMeaning
🟢 BRIK-64 CERTIFIEDΦ_c = 1, Ω = 1, 100% Core monomers. Structurally impossible to have logic errors.
🔵 BRIK-64 OPEN 84%Core + Extended monomers. Core coverage percentage shown. Boundary enforced by compiler.
🟡 PENDINGSubmitted to registry, audit in progress.
🔴 INVALIDHash mismatch — program has been modified after certification.
UNVERIFIEDNot submitted to registry. No formal claim made.