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

Formal verification from NAND gates to proof certificates.

--- ## 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). ---

Built by Ahmad Ali Parr + SnapKitty Collective

``` ╔══════════════════════════════════════════════════════╗ ║ ║ ║ The engine searches. ║ ║ The kernel decides. ║ ║ ║ ║ If the kernel is correct, the system is sound. ║ ║ The kernel is 80 lines. ║ ║ Read them yourself. ║ ║ ║ ╚══════════════════════════════════════════════════════╝ ```