| <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> | |