README.md

<p align="center">

```

██████╗ ██╗   ██╗██████╗ ███████╗

██╔══██╗██║   ██║██╔══██╗██╔════╝

██████╔╝██║   ██║██████╔╝█████╗

██╔═══╝ ██║   ██║██╔══██╗██╔══╝

██║     ╚██████╔╝██║  ██║███████╗

╚═╝      ╚═════╝ ╚═╝  ╚═╝╚══════╝



██╗   ██╗ █████╗ ██╗     ██╗██████╗ ██╗████████╗██╗   ██╗

██║   ██║██╔══██╗██║     ██║██╔══██╗██║╚══██╔══╝╚██╗ ██╔╝

██║   ██║███████║██║     ██║██║  ██║██║   ██║    ╚████╔╝

╚██╗ ██╔╝██╔══██║██║     ██║██║  ██║██║   ██║     ╚██╔╝

 ╚████╔╝ ██║  ██║███████╗██║██████╔╝██║   ██║      ██║

  ╚═══╝  ╚═╝  ╚═╝╚══════╝╚═╝╚═════╝ ╚═╝   ╚═╝      ╚═╝

```

</p>

<h3 align="center">Formal verification from NAND gates to proof certificates.</h3>

<p align="center">
  <img src="https://img.shields.io/badge/core-Haskell-5e5086?style=flat-square"/>
  <img src="https://img.shields.io/badge/backend-Fortran-734f96?style=flat-square"/>
  <img src="https://img.shields.io/badge/solver-CDCL+DPLL-blue?style=flat-square"/>
  <img src="https://img.shields.io/badge/kernel-80_LOC-brightgreen?style=flat-square"/>
  <img src="https://img.shields.io/badge/tests-20_passing-brightgreen?style=flat-square"/>
  <img src="https://img.shields.io/badge/deps-containers_only-black?style=flat-square"/>
  <img src="https://img.shields.io/badge/license-AGPL--3.0-red?style=flat-square"/>
</p>

---

## What Is This?

A self-contained formal verification engine built from first principles. No Z3. No SMT solver dependency. No Lean. No Coq. Just:

- A source language (`.nf` files) where NAND is the only primitive
- A compiler that elaborates definitions into Boolean circuits
- A SAT solver (DPLL + CDCL with clause learning) that searches for proofs
- A proof-producing backend that emits resolution certificates
- A **trusted kernel** (~80 lines) that independently verifies those certificates

The foundational principle: **the engine searches, the kernel decides.**

```

╔══════════════════════════════════════════════════════════════════════════╗

║                                                                          ║

║   THE SEPARATION                                                         ║

║                                                                          ║

║   SOLVER (complex, 1000+ LOC)          KERNEL (simple, ~80 LOC)         ║

║   ─────────────────────────            ──────────────────────           ║

║                                                                          ║

║   Heuristics, backtracking,            Resolution step checker           ║

║   clause learning, unit prop,          Clause validation                 ║

║   decision ordering, restarts          Hash verification                 ║

║                                                                          ║

║   MAY HAVE BUGS                        MUST BE CORRECT                   ║

║   (if buggy: proof won't verify)       (if buggy: false validity)        ║

║                                                                          ║

║   A bug in the solver =                A bug in the kernel =             ║

║   "failed to find proof"               "accepted invalid proof"          ║

║   (safe failure)                        (unsound — the only real risk)   ║

║                                                                          ║

╚══════════════════════════════════════════════════════════════════════════╝

```

---

## Quick Start

```bash

git clone https://github.com/SNAPKITTYWEST/pure-validity

cd pure-validity

cabal build

cabal run pure-validity -- examples/gates.nf

```

```

Module: gates

Properties: 16



  [OK] not_true

  [OK] not_false

  [OK] and_tt

  [OK] and_tf

  [OK] and_ft

  [OK] and_ff

  [OK] or_tt

  [OK] or_tf

  [OK] or_ft

  [OK] or_ff

  [OK] xor_tt

  [OK] xor_tf

  [OK] xor_ft

  [OK] xor_ff



16/16 verified.

```

---

## The Language — `.nf` files

NAND is the only hardware primitive. Everything else is defined, not assumed.

```

-- gates.nf — derive all logic from NAND alone



def not(x) = (x | x);



def and(x y) = not((x | y));



def or(x y) = (not(x) | not(y));



def xor(x y) = ((x | (x | y)) | (y | (x | y)));



-- Prove correctness of derived gates

prove and_tt: and(true true) = true;

prove xor_tf: xor(true false) = true;

```

### Syntax Reference

```

╔════════════════════╦═══════════════════════════════════════════════╗

║  CONSTRUCT          ║  MEANING                                      ║

╠════════════════════╬═══════════════════════════════════════════════╣

║  (a | b)           ║  NAND — the only primitive gate               ║

║  def f(x y) = e;  ║  Define a named circuit                       ║

║  prove n: e;       ║  State and verify a property                  ║

║  assert e;         ║  Verify without naming                        ║

║  true / false      ║  Boolean constants                            ║

║  -- comment        ║  Line comment                                 ║

║  module name;      ║  Module declaration                           ║

╚════════════════════╩═══════════════════════════════════════════════╝

```

---

## Verification Pipeline

```

  .nf source file

        │

        ▼

  ┌─────────────────────────────────────────────────────────┐

  │  LEXER + PARSER                                          │

  │  Language/Lexer.hs + Language/Parser.hs                  │

  │  Source text → Token stream → AST (Module of Stmts)     │

  └─────────────────────────────────────────────────────────┘

        │

        ▼

  ┌─────────────────────────────────────────────────────────┐

  │  ELABORATOR                                              │

  │  Language/Elaborator.hs                                  │

  │  AST → Boolean IR (BExpr trees — NAND-only)            │

  │  Inlines function applications, resolves names          │

  └─────────────────────────────────────────────────────────┘

        │

        ▼

  ┌─────────────────────────────────────────────────────────┐

  │  TSEITIN TRANSFORM                                       │

  │  SAT/CNF.hs                                             │

  │  BExpr → CNF (conjunctive normal form)                  │

  │  Introduces auxiliary variables, linear blowup          │

  └─────────────────────────────────────────────────────────┘

        │

        ▼

  ┌─────────────────────────────────────────────────────────┐

  │  SAT SOLVER (DPLL + CDCL)                                │

  │  SAT/DPLL.hs + SAT/CDCL.hs                              │

  │  Unit propagation → decision → conflict → backtrack     │

  │  Clause learning on conflict (CDCL)                     │

  │  Proof-producing: records resolution steps              │

  └─────────────────────────────────────────────────────────┘

        │

        ▼

  ┌─────────────────────────────────────────────────────────┐

  │  PROOF CERTIFICATE                                       │

  │  Proof/Certificate.hs + Proof/Produce.hs                │

  │  Resolution steps + SHA-256 hash                        │

  │  Conclusion: Valid | Unsatisfiable | CounterExample      │

  └─────────────────────────────────────────────────────────┘

        │

        ▼

  ┌─────────────────────────────────────────────────────────┐

  │  TRUSTED KERNEL (~80 LOC)                                │

  │  Checker/Kernel.hs                                      │

  │  Independently verifies every resolution step           │

  │  Accepts or rejects the certificate                     │

  │  THE ONLY CODE THAT MUST BE CORRECT                     │

  └─────────────────────────────────────────────────────────┘

        │

        ▼

  [OK] Property verified  /  [FAIL] Counterexample found

```

---

## Architecture — Why Two Layers?

The insight from proof-carrying code (Necula 1997): separate the **search** from the **checking**.

A solver can be arbitrarily complex — heuristics, restarts, clause deletion, VSIDS scoring. If it has a bug, it just fails to find the proof. The system remains sound.

The kernel is trivial by comparison. It receives a claimed proof (sequence of resolution steps) and mechanically verifies each step: did resolving clause A with clause B on pivot variable P actually produce clause C? That's it. ~80 lines. Auditable by hand.

```

╔══════════════════════════════════════════════════════════════╗

║                                                              ║

║  Solver bug → "could not prove" (safe, retry with better    ║

║               heuristics or more time)                       ║

║                                                              ║

║  Kernel bug → false validity claim (unsound — THE risk)      ║

║               But kernel is 80 LOC, auditable, testable      ║

║                                                              ║

╚══════════════════════════════════════════════════════════════╝

```

---

## Fortran Backend

For hardware-scale verification (thousands of gates), the Fortran backend provides vectorized clause checking and bounded model checking:

```fortran

! bitvec_ops.f90 — bulk NAND evaluation + clause checking

call bulk_clause_check(clauses, num_clauses, clause_lens, assignment, num_vars, satisfied)



! state_machine.f90 — bounded model checking with induction

result = bmc_check(transition_gates, ..., init_state, state_width, bound)

```

The Fortran modules handle:
- Vectorized NAND evaluation over flat gate arrays
- Bulk satisfiability checking across all clauses simultaneously
- Ripple-carry addition for arithmetic circuit verification
- Bounded model checking (BMC) for sequential circuits
- k-induction for unbounded property proofs

---

## Examples

```

╔═══════════════════╦══════════════════════════════════════════════════╗

║  FILE              ║  WHAT IT PROVES                                  ║

╠═══════════════════╬══════════════════════════════════════════════════╣

║  nand.nf          ║  NAND truth table (the primitive)                ║

║  gates.nf         ║  NOT/AND/OR/XOR all correct from NAND alone      ║

║  half_adder.nf    ║  Binary arithmetic: sum and carry correct         ║

║  demorgan.nf      ║  De Morgan's Laws hold for NAND-derived gates    ║

║  mux.nf           ║  2-to-1 multiplexer selects correctly            ║

╚═══════════════════╩══════════════════════════════════════════════════╝

```

Run all examples:

```bash

for f in examples/*.nf; do cabal run pure-validity -- "$f"; echo; done

```

---

## Project Layout

```

pure-validity/

├── pure-validity.cabal         Build configuration

├── README.md                   This file

│

├── src/

│   ├── Main.hs                 Entry point — file → parse → prove → check

│   ├── Language/

│   │   ├── AST.hs             Abstract syntax (Expr, Stmt, Module)

│   │   ├── Lexer.hs           Tokenizer (keywords, operators, idents)

│   │   ├── Parser.hs          Recursive descent parser

│   │   └── Elaborator.hs      AST → Boolean IR (inline + resolve)

│   ├── IR/

│   │   ├── Boolean.hs         BExpr type + eval + NAND/AND/OR/XOR

│   │   ├── NAND.hs            NAND normal form transformation

│   │   └── BitVec.hs          Bit-vector arithmetic (add, eq, const)

│   ├── SAT/

│   │   ├── CNF.hs             Clause/literal types + Tseitin transform

│   │   ├── UnitProp.hs        Unit propagation (BCP)

│   │   ├── DPLL.hs            Davis-Putnam-Logemann-Loveland solver

│   │   └── CDCL.hs            Conflict-Driven Clause Learning solver

│   ├── Proof/

│   │   ├── Certificate.hs     ProofStep, ProofCertificate types

│   │   └── Produce.hs         Validity/UNSAT proof generation

│   └── Checker/

│       └── Kernel.hs          THE TRUSTED KERNEL (~80 LOC)

│

├── fortran/

│   ├── bitvec_ops.f90          Vectorized NAND + bulk clause check

│   └── state_machine.f90       BMC + k-induction for sequential circuits

│

├── examples/

│   ├── nand.nf                 NAND primitive proofs

│   ├── gates.nf                All gates from NAND

│   ├── half_adder.nf           Arithmetic correctness

│   ├── demorgan.nf             De Morgan's Laws

│   └── mux.nf                  Multiplexer properties

│

└── test/

    └── Spec.hs                 20 tests — IR, solver, kernel, parser

```

---

## Run Tests

```bash

cabal test

```

```

[OK]  NAND truth table

[OK]  NOT from NAND

[OK]  AND from NAND

[OK]  OR from NAND

[OK]  XOR from NAND

[OK]  Half adder sum

[OK]  Half adder carry

[OK]  BitVec add 3+5=8

[OK]  Tseitin preserves satisfiability

[OK]  DPLL finds SAT

[OK]  DPLL finds UNSAT

[OK]  Unit propagation

[OK]  Proof certificate valid

[OK]  Checker accepts valid

[OK]  Checker rejects invalid

[OK]  Parse module

[OK]  Elaborate module

[OK]  NAND normal form

[OK]  De Morgan via eval

[OK]  MUX correctness



20/20 tests passed.

```

---

## Requirements

- GHC 8.10+ (Haskell compiler)
- Cabal 3.0+
- gfortran (for Fortran backend, optional)
- Zero external solver dependencies (no Z3, no MiniSat, no SMT-LIB)

```bash

# Install GHC + Cabal (if needed)

curl --proto '=https' --tlsv1.2 -sSf https://get-ghcup.haskell.org | sh



# Build and run

cabal build

cabal run pure-validity -- examples/gates.nf

cabal test

```

---

## Theory

The verification approach combines:

1. **Tseitin transformation** — Boolean formula to CNF with linear blowup (not exponential)
2. **DPLL** — systematic backtracking search with unit propagation
3. **CDCL** — conflict-driven clause learning for exponential speedup on structured problems
4. **Resolution proofs** — the solver records why it concluded UNSAT
5. **Proof checking** — independent verification that each resolution step is valid

To prove a property P holds: negate P, convert to CNF, prove UNSAT. If the negation is unsatisfiable, the original property is valid (true under all assignments).

---

<p align="center">
  <b>Built by Ahmad Ali Parr + SnapKitty Collective</b>
</p>

<p align="center">

```

╔══════════════════════════════════════════════════════╗

║                                                      ║

║  The engine searches.                                ║

║  The kernel decides.                                 ║

║                                                      ║

║  If the kernel is correct, the system is sound.      ║

║  The kernel is 80 lines.                             ║

║  Read them yourself.                                 ║

║                                                      ║

╚══════════════════════════════════════════════════════╝

```

</p>