Monomers

A monomer is an atomic, formally verified computation unit — the logic gate of Digital Circuitality. Every program in BRIK-64 is built exclusively from monomers composed through EVA Algebra. There are no other primitives. There are no escape hatches.

Monomer := (id: MC_xx, input_type: Type, output_type: Type, proof: Coq_lemma)

Each monomer satisfies four formal properties, proven in Coq:

Property	Definition
Domain	The set of valid inputs. Inputs outside the domain are compile-time errors.
Range	The exact set of possible outputs. Output type is fully specified.
Termination	Every monomer halts in O(1) time (no loops inside a monomer).
Determinism	Same inputs → same output, always, on any hardware.

All Core monomers return Value::I64 (not Value::U8), except DIV8 which returns Value::Tuple([quotient, remainder]). This is a critical implementation invariant — component code must pattern-match on Value::Tuple when calling MC_03.DIV8.

Calling Monomers in PCD

// Direct call
let result = MC_00.ADD8(a, b);

// DIV8 returns a tuple — destructure immediately
let qr     = MC_03.DIV8(dividend, divisor);
let q      = qr[0];   // quotient
let r      = qr[1];   // remainder

// Monomer in a pipeline (EVA sequential ⊗)
let hash   = MC_40.HASH(message);
let mac    = MC_41.HMAC(key, hash);

Monomer identifiers are stable — MC_00.ADD8 will always be MC_00.ADD8. The numeric ID and the symbolic name are both valid; the compiler accepts either form.

Family F0 — Arithmetic (MC_00–MC_07)

Arithmetic over 64-bit integers. All operations are on I64 values.

MC_00 — ADD8: Add two integers

Signature: (I64, I64) → I64
Operation: a + b
Overflow: wrapping (modular 2⁶⁴)
Coq lemma: add8_correct: ∀ a b : i64, ADD8(a,b) = a + b mod 2⁶⁴

let sum = MC_00.ADD8(x, y);

MC_01 — SUB8: Subtract

Signature: (I64, I64) → I64
Operation: a - b (wrapping)
Coq lemma: sub8_correct

let diff = MC_01.SUB8(x, y);

MC_02 — MUL8: Multiply

Signature: (I64, I64) → I64
Operation: a * b (wrapping, lower 64 bits)
Coq lemma: mul8_correct

let product = MC_02.MUL8(x, y);

MC_03 — DIV8: Divide with remainder

Signature: (I64, I64) → Tuple(I64, I64)
Operation: (a / b, a mod b)
Precondition: b ≠ 0 — division by zero is a compile-time error if statically known, runtime trap otherwise
Returns: Value::Tuple([quotient, remainder]) — must destructure
Coq lemma: div8_correct: ∀ a b, b ≠ 0 → DIV8(a,b) = (a÷b, a mod b)

let qr = MC_03.DIV8(100, 7);
let q  = qr[0];   // 14
let r  = qr[1];   // 2

MC_04 — INC: Increment by 1

Signature: I64 → I64
Operation: a + 1 (wrapping)
Coq lemma: inc_correct

let next = MC_04.INC(counter);

MC_05 — DEC: Decrement by 1

Signature: I64 → I64
Operation: a - 1 (wrapping)
Coq lemma: dec_correct

let prev = MC_05.DEC(counter);

MC_06 — MOD: Modulo

Signature: (I64, I64) → I64
Operation: a mod b
Precondition: b ≠ 0
Coq lemma: mod_correct

let rem = MC_06.MOD(n, 256);

MC_07 — NEG: Arithmetic negation

Signature: I64 → I64
Operation: -a (two’s complement)
Coq lemma: neg_correct

let neg = MC_07.NEG(value);

Family F1 — Logic (MC_08–MC_15)

Bitwise logic and shift operations on 64-bit integers.

MC	Name	Signature	Operation
MC_08	AND8	`(I64,I64)→I64`	Bitwise AND
MC_09	OR8	`(I64,I64)→I64`	Bitwise OR
MC_10	XOR8	`(I64,I64)→I64`	Bitwise XOR
MC_11	NOT8	`I64→I64`	Bitwise NOT
MC_12	SHL	`(I64,I64)→I64`	Shift left by N bits
MC_13	SHR	`(I64,I64)→I64`	Logical shift right by N bits
MC_14	ROTL	`(I64,I64)→I64`	Rotate left by N bits
MC_15	ROTR	`(I64,I64)→I64`	Rotate right by N bits

let masked  = MC_08.AND8(flags, 0xFF);
let toggled = MC_10.XOR8(byte, 0x01);
let shifted = MC_12.SHL(value, 3);     // multiply by 8

Control monomers (MC_24–MC_31, Family F3) skip Bool→U64 coercion in the runtime. The IF monomer (MC_24) requires a Bool value, not I64. All comparison results in PCD are Bool; you cannot pass an integer directly to IF without an explicit conversion.

Family F2 — Memory (MC_16–MC_23)

Memory operations. In native ELF mode, these operate on the three memory regions established by the startup stub (vstack, heap, ASCII buffer). In BIR/interpreted mode, they operate on the interpreter’s value store.

MC	Name	Signature	Operation
MC_16	LOAD	`Ptr→I64`	Load 64-bit value from address
MC_17	STORE	`(Ptr,I64)→Unit`	Store 64-bit value at address
MC_18	ALLOC	`I64→Ptr`	Allocate N bytes on the BRIK heap
MC_19	FREE	`Ptr→Unit`	Free a previously allocated block
MC_20	COPY	`(Ptr,Ptr,I64)→Unit`	Copy N bytes from src to dst
MC_21	SWAP	`(Ptr,Ptr)→Unit`	Swap values at two addresses
MC_22	CAS	`(Ptr,I64,I64)→Bool`	Compare-And-Swap (atomic)
MC_23	FENCE	`()→Unit`	Memory fence / barrier

Family F3 — Control (MC_24–MC_31)

Control flow monomers. These are the only monomers that alter the program counter.

MC	Name	Signature	Operation
MC_24	IF	`(Bool,Block,Block)→T`	Conditional branch (requires Bool, not I64)
MC_25	JUMP	`Label→Never`	Unconditional jump
MC_26	CALL	`(FnPtr,Args)→T`	Function call
MC_27	RET	`T→Never`	Return from function
MC_28	LOOP	`(I64,Block)→Unit`	Execute block N times
MC_29	BREAK	`()→Never`	Break from innermost loop
MC_30	CONT	`()→Never`	Continue to next iteration
MC_31	HALT	`I64→Never`	Terminate program with exit code

In PCD, these are expressed through language syntax (if, loop(N), return, etc.) — you rarely call them directly. The planner maps syntax to the corresponding monomer.

Family F4 — I/O (MC_32–MC_39)

File and stream I/O operations. In native ELF mode, these issue direct Linux syscalls (no libc wrappers). In sandboxed WASM mode, they are disabled by the WASM policy circuit.

MC	Name	Signature	Operation
MC_32	READ	`(Fd, Buf, I64)→I64`	Read N bytes from file descriptor
MC_33	WRITE	`(Fd, Buf, I64)→I64`	Write N bytes to file descriptor
MC_34	OPEN	`(Path, Flags)→Fd`	Open file, returns file descriptor
MC_35	CLOSE	`Fd→I64`	Close file descriptor
MC_36	SEEK	`(Fd, I64, I64)→I64`	Seek in file (offset, whence)
MC_37	STAT	`(Path, StatBuf)→I64`	Get file metadata
MC_38	POLL	`(PollFds, I64, I64)→I64`	Poll file descriptors
MC_39	FLUSH	`Fd→I64`	Flush buffered output

// Write to stdout (fd=1)
let n = MC_33.WRITE(1, message, MC_45.LEN(message));

Family F5 — String (MC_40–MC_47)

String operations over BRIK’s built-in String type (UTF-8, immutable, ref-counted).

MC	Name	Signature	Operation
MC_40	CONCAT	`(String,String)→String`	Concatenate two strings
MC_41	SPLIT	`(String,String)→Array(String)`	Split by delimiter
MC_42	SUBSTR	`(String,I64,I64)→String`	Substring [start, end)
MC_43	LEN	`String→I64`	Length in bytes
MC_44	UPPER	`String→String`	ASCII uppercase
MC_45	CHAR_AT	`(String,I64)→I64`	Byte at index (O(1) via `.as_bytes()[idx]`)
MC_46	TRIM	`String→String`	Remove leading/trailing whitespace
MC_47	MATCH	`(String,Pattern)→Bool`	Regex-like pattern match

CHAR_AT (MC_45) runs in O(1) using s.as_bytes()[idx] — not s.chars().nth(idx). This is a critical performance invariant. The tokenizer in brikc.pcd depends on it.

Family F6 — Crypto (MC_48–MC_55)

Cryptographic primitives. All are constant-time by construction (no secret-dependent branches).

MC	Name	Signature	Operation
MC_48	HASH	`Bytes→Hash32`	SHA-256 hash
MC_49	HMAC	`(Key,Bytes)→MAC32`	HMAC-SHA-256
MC_50	AES_ENC	`(Key16,Block16)→Block16`	AES-128 encrypt
MC_51	AES_DEC	`(Key16,Block16)→Block16`	AES-128 decrypt
MC_52	SHA256	`Bytes→Hash32`	SHA-256 (direct, no HMAC wrapping)
MC_53	RAND	`I64→Bytes`	Cryptographically secure N random bytes
MC_54	SIGN	`(PrivKey,Bytes)→Sig`	Ed25519 signature
MC_55	VERIFY	`(PubKey,Bytes,Sig)→Bool`	Ed25519 signature verification

Family F7 — System (MC_56–MC_63)

System-level operations. In the BPU hardware future, these are the operations that require a Policy Circuit approval before execution — the hardware-enforced ALLOW/BLOCK boundary.

MC	Name	Signature	Operation
MC_56	TIME	`()→I64`	Monotonic clock (nanoseconds)
MC_57	SLEEP	`I64→Unit`	Sleep N nanoseconds
MC_58	ENV	`String→String`	Read environment variable
MC_59	EXIT	`I64→Never`	Exit with code
MC_60	PID	`()→I64`	Current process ID
MC_61	SIGNAL	`(I64,Handler)→Unit`	Install signal handler
MC_62	MMAP	`(I64,Flags)→Ptr`	Memory-map N bytes
MC_63	SYSINFO	`SysinfoPtr→I64`	System information (uname, meminfo)

MC_58 (ENV) is used internally by the compiler to read BRIK_NATIVE_TIMEOUT_MS and BRIK_CWD. Do not confuse MC_58.ENV with MC_32.READ — they are different monomers with different semantics and different Coq proofs.

Complete Monomer Reference Table

ID	Family	Name	Input	Output
MC_00	F0 Arithmetic	ADD8	(I64,I64)	I64
MC_01	F0 Arithmetic	SUB8	(I64,I64)	I64
MC_02	F0 Arithmetic	MUL8	(I64,I64)	I64
MC_03	F0 Arithmetic	DIV8	(I64,I64)	Tuple(I64,I64)
MC_04	F0 Arithmetic	INC	I64	I64
MC_05	F0 Arithmetic	DEC	I64	I64
MC_06	F0 Arithmetic	MOD	(I64,I64)	I64
MC_07	F0 Arithmetic	NEG	I64	I64
MC_08	F1 Logic	AND8	(I64,I64)	I64
MC_09	F1 Logic	OR8	(I64,I64)	I64
MC_10	F1 Logic	XOR8	(I64,I64)	I64
MC_11	F1 Logic	NOT8	I64	I64
MC_12	F1 Logic	SHL	(I64,I64)	I64
MC_13	F1 Logic	SHR	(I64,I64)	I64
MC_14	F1 Logic	ROTL	(I64,I64)	I64
MC_15	F1 Logic	ROTR	(I64,I64)	I64
MC_16	F2 Memory	LOAD	Ptr	I64
MC_17	F2 Memory	STORE	(Ptr,I64)	Unit
MC_18	F2 Memory	ALLOC	I64	Ptr
MC_19	F2 Memory	FREE	Ptr	Unit
MC_20	F2 Memory	COPY	(Ptr,Ptr,I64)	Unit
MC_21	F2 Memory	SWAP	(Ptr,Ptr)	Unit
MC_22	F2 Memory	CAS	(Ptr,I64,I64)	Bool
MC_23	F2 Memory	FENCE	()	Unit
MC_24	F3 Control	IF	(Bool,Block,Block)	T
MC_25	F3 Control	JUMP	Label	Never
MC_26	F3 Control	CALL	(FnPtr,Args)	T
MC_27	F3 Control	RET	T	Never
MC_28	F3 Control	LOOP	(I64,Block)	Unit
MC_29	F3 Control	BREAK	()	Never
MC_30	F3 Control	CONT	()	Never
MC_31	F3 Control	HALT	I64	Never
MC_32	F4 I/O	READ	(Fd,Buf,I64)	I64
MC_33	F4 I/O	WRITE	(Fd,Buf,I64)	I64
MC_34	F4 I/O	OPEN	(Path,Flags)	Fd
MC_35	F4 I/O	CLOSE	Fd	I64
MC_36	F4 I/O	SEEK	(Fd,I64,I64)	I64
MC_37	F4 I/O	STAT	(Path,StatBuf)	I64
MC_38	F4 I/O	POLL	(PollFds,I64,I64)	I64
MC_39	F4 I/O	FLUSH	Fd	I64
MC_40	F5 String	CONCAT	(String,String)	String
MC_41	F5 String	SPLIT	(String,String)	Array(String)
MC_42	F5 String	SUBSTR	(String,I64,I64)	String
MC_43	F5 String	LEN	String	I64
MC_44	F5 String	UPPER	String	String
MC_45	F5 String	CHAR_AT	(String,I64)	I64
MC_46	F5 String	TRIM	String	String
MC_47	F5 String	MATCH	(String,Pattern)	Bool
MC_48	F6 Crypto	HASH	Bytes	Hash32
MC_49	F6 Crypto	HMAC	(Key,Bytes)	MAC32
MC_50	F6 Crypto	AES_ENC	(Key16,Block16)	Block16
MC_51	F6 Crypto	AES_DEC	(Key16,Block16)	Block16
MC_52	F6 Crypto	SHA256	Bytes	Hash32
MC_53	F6 Crypto	RAND	I64	Bytes
MC_54	F6 Crypto	SIGN	(PrivKey,Bytes)	Sig
MC_55	F6 Crypto	VERIFY	(PubKey,Bytes,Sig)	Bool
MC_56	F7 System	TIME	()	I64
MC_57	F7 System	SLEEP	I64	Unit
MC_58	F7 System	ENV	String	String
MC_59	F7 System	EXIT	I64	Never
MC_60	F7 System	PID	()	I64
MC_61	F7 System	SIGNAL	(I64,Handler)	Unit
MC_62	F7 System	MMAP	(I64,Flags)	Ptr
MC_63	F7 System	SYSINFO	SysinfoPtr	I64

Extended Monomers: MC_64–MC_127

Extended Monomers (MC_64–MC_127) are WORK IN PROGRESS and NOT YET IMPLEMENTED. The families F8–F15 below represent the planned roadmap only. No Coq proofs exist yet for these monomers. No backend implementations exist. Do not use MC_64+ in production PCD programs.

The Extended set adds 64 more monomers in 8 additional families, targeting higher-level domains not covered by the Core set:

Family	Range	Domain	Status
F8	MC_64–MC_71	Network (TCP/UDP/TLS)	Planned
F9	MC_72–MC_79	Concurrency (spawn, channel, mutex)	Planned
F10	MC_80–MC_87	Floating point (F64 arithmetic)	Planned
F11	MC_88–MC_95	SIMD / vector operations	Planned
F12	MC_96–MC_103	Database (KV operations)	Planned
F13	MC_104–MC_111	Codec (JSON, CBOR, MessagePack)	Planned
F14	MC_112–MC_119	ML inference primitives	Planned
F15	MC_120–MC_127	BPU policy (hardware-enforced)	Planned

The total extended vocabulary (128 monomers) is the target for BRIK-64 v4.0.0. Each extended monomer will require the same rigorous Coq treatment as the Core set: domain, range, termination, and a formal proof of determinism.

Coq Proof Structure

Every Core monomer is backed by a Coq proof in theory/papers/. The proof structure for each monomer follows this template:

(* MC_00 ADD8 — from theory/papers/F0_arithmetic.v *)
Lemma add8_correct : forall (a b : Z),
  let r := (a + b) mod (2^64) in
  ADD8 a b = r.
Proof.
  intros a b.
  unfold ADD8.
  (* ... proof steps ... *)
Qed.

Lemma add8_terminates : forall (a b : Z),
  exists n, steps ADD8 a b n.
Proof.
  intros. exists 1. apply step_add8.
Qed.

207 .v files in theory/papers/
0 Admitted lemmas — all replaced with DEFERRED comments (audit 2026-03-07)
Proof coverage: 100% of Core monomers, all EVA Algebra laws, TCE bound theorems

Getting Started

Architecture

PCD Language

CLI Reference

Theory

Monomers — The 64 Atomic Operations

Monomers

Calling Monomers in PCD

Family F0 — Arithmetic (MC_00–MC_07)

Family F1 — Logic (MC_08–MC_15)

Family F2 — Memory (MC_16–MC_23)

Family F3 — Control (MC_24–MC_31)

Family F4 — I/O (MC_32–MC_39)

Family F5 — String (MC_40–MC_47)

Family F6 — Crypto (MC_48–MC_55)

Family F7 — System (MC_56–MC_63)

Complete Monomer Reference Table

Extended Monomers: MC_64–MC_127

Coq Proof Structure

Getting Started

Architecture

PCD Language

CLI Reference

Theory

​Monomers

​Calling Monomers in PCD

​Family F0 — Arithmetic (MC_00–MC_07)

​Family F1 — Logic (MC_08–MC_15)

​Family F2 — Memory (MC_16–MC_23)

​Family F3 — Control (MC_24–MC_31)

​Family F4 — I/O (MC_32–MC_39)

​Family F5 — String (MC_40–MC_47)

​Family F6 — Crypto (MC_48–MC_55)

​Family F7 — System (MC_56–MC_63)

​Complete Monomer Reference Table

​Extended Monomers: MC_64–MC_127

​Coq Proof Structure

Monomers

Calling Monomers in PCD

Family F0 — Arithmetic (MC_00–MC_07)

Family F1 — Logic (MC_08–MC_15)

Family F2 — Memory (MC_16–MC_23)

Family F3 — Control (MC_24–MC_31)

Family F4 — I/O (MC_32–MC_39)

Family F5 — String (MC_40–MC_47)

Family F6 — Crypto (MC_48–MC_55)

Family F7 — System (MC_56–MC_63)

Complete Monomer Reference Table

Extended Monomers: MC_64–MC_127

Coq Proof Structure