Sync with GitHub, license metadata from LICENSE files, commercial license notice

README.md

@@ -1,398 +1,418 @@
-<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>
+---
+license: agpl-3.0
+tags:
+- snapkitty
+---
+
+<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>
+
+---
+
+## License
+
+Licensed under **AGPL-3.0** ([LICENSE](LICENSE)), with these additional license files:
+
+- [LICENSE.tri](LICENSE.tri): SnapKitty Tri-License
+
+### 💼 Commercial License
+
+Snapkitty code is free and open under **AGPL-3.0** for open-source use. Building a commercial product or service? A **proprietary commercial license** from Snapkitty Collective LLC lets you ship this code without the AGPL's source-sharing and network-use obligations.
+
+**[→ Get a commercial license](mailto:A.parr@belespritdaccord.uk?subject=Commercial%20license:%20pure-validity)** · A.parr@belespritdaccord.uk