Testing & Debugging

Your code ships with tests. Already.

Writing tests is one of the most time-consuming parts of software development. Teams spend as much time on test suites as on features. Coverage is never complete. When requirements change, tests break. When deadline pressure mounts, tests get skipped — and bugs slip through. BRIK-64 takes a different approach: the compiler generates both the code and its complete test suite at the same time, from the same formal proof.

brikc compile src/main.pcd --target rs --emit-tests

Output:

build/main.rs          ← certified Rust implementation
build/main_spec.rs     ← complete test suite, auto-generated from the proof

Your CI pipeline goes from:

❌  write code  →  write tests manually  →  (hope coverage is complete)  →  deploy

to:

✅  write PCD  →  compile  →  code + test suite arrive together, proven correct  →  deploy

The test suite is not a placeholder or a scaffold. It contains real, runnable assertions derived directly from the formal proof.

What the auto-generated test suite contains

Test type	What it verifies	Source
Property tests	Input/output ranges for every function	CMF proof
Boundary tests	Edge values for every monomer used (overflow, zero, max)	Monomer specification
Composition tests	Each EVA operator chain behaves as the CMF proved	EVA algebra rules
Regression anchors	Canonical input/output pairs that define the proven behavior	Fixpoint hash

The regression anchors are especially important for long-term maintenance. If the generated Rust or JavaScript is ever modified manually downstream — in a refactor, a migration, a dependency upgrade — the regression anchors catch any divergence from the proven logic. The tests are the specification of what the code was guaranteed to do.

Do I still need to write tests?

Yes — but for different things than you might expect. The compiler handles correctness of your logic. What remains for you:

Test type	Who writes it	Purpose
Property / boundary / composition	Compiler — auto-generated	Proves the logic is correct
Regression anchors	Compiler — auto-generated	Detects future deviations
Business requirements	You	”Does it do what the user needs?”
Integration with external systems	You	Database, API, user input boundaries
Performance / load	You	When requirements specify latency or throughput

BRIK-64 proves you built the thing right. You test that you built the right thing.

This is not a small distinction. In a typical project, 60–80% of test surface area is spent verifying that functions behave correctly under various inputs. With BRIK-64, that work is done by the compiler. You focus acceptance testing on what actually varies: requirements, integrations, and performance.

Core programs: what “certified” means for testing

A Core program uses only MC_00–MC_63. When it compiles with Φ_c = 1, the following are structurally guaranteed — not probabilistically:

Guarantee	Meaning
Type safety	No type error can occur at runtime
No undefined behavior	Every branch reaches a defined output
Determinism	Identical inputs always produce identical outputs
No integer overflow	Core arithmetic uses saturating semantics
No null dereference	PCD has no null values
Termination	All loops have proven bounds

A test that checks add(2, 3) == 5 is valid but structurally redundant — the compiler already proved it. What the auto-generated tests do instead is encode the ranges and invariants that are guaranteed, so they serve as executable documentation and future regression detection.

Generated code inherits the proof

When you compile PCD to Rust, JavaScript, Python, or WASM, the generated code inherits the Φ_c = 1 certification:

brikc compile src/main.pcd --target rs      # certified Rust
brikc compile src/main.pcd --target js      # certified JavaScript
brikc compile src/main.pcd --target py      # certified Python
brikc compile src/main.pcd --target wasm32  # certified WebAssembly

The proof happened at compile time in the PCD pipeline. The target language is the deployment vehicle. The generated code is provably correct before any test runner ever executes — and arrives with its own test suite that documents and protects that correctness.

Code written directly in Rust, Python, or JavaScript — even using BRIK-64 monomer libraries — is not CMF-certified and does not receive auto-generated test suites from the proof pipeline. Only PCD programs compiled through brikc produce certified output.

Extended monomers (MC_64–MC_127)

Extended monomers connect certified Core logic to the real world: floating point, networking, graphics, concurrency, FFI. They operate under declared contracts, not formal proofs — because the failure sources are outside the computation. Why Extended monomers can fail:

Monomer	Failure mode	Can the proof prevent it?
TCP_CONN	Server unreachable	No — physics
HTTP_GET	Timeout, 5xx, malformed body	No — network
FADD	NaN propagation (`0.0/0.0`)	No — IEEE 754
FFI_CALL	Segfault in native library	No — native code
SPAWN	Resource exhaustion	No — OS

What BRIK-64 guarantees even in Open programs:

The Core sections remain Φ_c = 1 — formally proven and auto-tested
Extended monomers must be at the boundary of the computation graph, not in the trunk — the compiler enforces this
Data flowing from Extended into Core must pass a validation boundary (typed and bounds-checked)
The program badge shows the verified percentage: ◈ BRIK-64 OPEN | 83% verified

Extended monomers ship with their own test suite covering:

Contract tests (the monomer honors its declared signature)
Error-path tests (network down, NaN, null FFI — all handled gracefully)
Boundary validation tests (data entering Core from Extended is safe)

Mock provider for development:

import "stdlib/mock.pcd";

PC test_pipeline {
    -- Mock external call — no real network needed
    let resp = HTTP_GET.mock("https://api.example.com", 200, "{\"status\": \"ok\"}");

    -- Core logic from here — formally verified
    let data = json_parse(resp.body);
    let status = data.get("status");
    OUTPUT status;
}

Debugging: compile-time errors

BRIK-64 programs fail at compile time, not at runtime. The CMF error is precise:

brikc check circuit.pcd

[CMF] Parsing circuit...              ✓
[CMF] EVA composition valid:          ✓
[CMF] Circuit closedness (Φ_c):       0.917   ← FAIL
[CMF] Unused input ratio (δ):         0.083

Error: E_OPEN_BRANCH
  Function: process_input
  Branch:   'error_path' has no OUTPUT
  Line 47:  if (x < 0) { return -1; }

  Fix: All branches must reach OUTPUT. Either add OUTPUT to the error
  branch, or handle it by propagating to the caller.

No “segmentation fault at runtime.” No “undefined is not a function.” The failure is at the logical design level, before any code runs, where it costs nothing to fix.

Common CMF errors

Error	Meaning	Fix
`Φ_c < 1.000` — open branch	A branch has no OUTPUT	Add `OUTPUT` to all branches
`δ > 0` — unused input	Function parameter is never used	Remove the parameter or prefix with `_`
`Type mismatch at ⊗`	Sequential composition type conflict	Check output type of left matches input of right
`MAX_DEPTH exceeded`	Nesting too deep for parser	Extract logic into named functions
`WhileLoop SSA`	Loop variable lost across iterations	Use `loop(N) { if (cond) { body } }` instead of `while`

→ Full list: Error Guide

Debugging tools

Tool	Command	Purpose
CMF check	`brikc check circuit.pcd`	Verify Φ_c without compiling
JSON output	`brikc check circuit.pcd --json`	Machine-readable for CI/CD
REPL	`brikc repl`	Explore monomers interactively
Type info	`brikc repl` → `:type expr`	Inspect value types
Binary verify	`brikc check --self`	Verify compiler binary integrity

A step-through debugger with breakpoints and variable inspection is planned for a future release. Until then, brikc check locates the issue precisely enough that step-through is rarely needed — the error message tells you the function, the branch, and the fix.

Testing in CI/CD

# .github/workflows/ci.yml
- name: Compile and generate tests
  run: |
    brikc compile src/main.pcd --target rs --emit-tests
    # build/main.rs and build/main_spec.rs are now available

- name: Run generated test suite
  run: cargo test --manifest-path build/Cargo.toml

- name: CMF check (machine-readable)
  run: brikc check src/main.pcd --json | jq '.certified'
  # Fails CI if output is not `true`

The generated tests integrate into any standard test runner in the target language — cargo test, jest, pytest, vitest. No custom test framework required.

Getting Started

PCD Language

CLI Reference

Theory

Testing & Debugging

Testing & Debugging

Your code ships with tests. Already.

What the auto-generated test suite contains

Do I still need to write tests?

Core programs: what “certified” means for testing

Generated code inherits the proof

Extended monomers (MC_64–MC_127)

Debugging: compile-time errors

Common CMF errors

Debugging tools

Testing in CI/CD

Getting Started

PCD Language

CLI Reference

Theory

​Testing & Debugging

​Your code ships with tests. Already.

​What the auto-generated test suite contains

​Do I still need to write tests?

​Core programs: what “certified” means for testing

​Generated code inherits the proof

​Extended monomers (MC_64–MC_127)

​Debugging: compile-time errors

​Common CMF errors

​Debugging tools

​Testing in CI/CD

Testing & Debugging

Your code ships with tests. Already.

What the auto-generated test suite contains

Do I still need to write tests?

Core programs: what “certified” means for testing

Generated code inherits the proof

Extended monomers (MC_64–MC_127)

Debugging: compile-time errors

Common CMF errors

Debugging tools

Testing in CI/CD