| --- |
| license: bsl-1.0 |
| tags: |
| - snapkitty |
| - october-2026-drop |
| - haskell |
| - compiler |
| - proof-language |
| - formal-verification |
| --- |
| |
| > Mirrored from [https://github.com/SNAPKITTYAGENT9NOVA/Assertica](https://github.com/SNAPKITTYAGENT9NOVA/Assertica) at commit `849932a`. Part of the **SnapKitty October 2026 main drop**. |
|
|
| # Assertica: Deterministic Proof Language Compiler |
|
|
|  |
|  |
|  |
|  |
|  |
|  |
|
|
| --- |
|
|
| ## Executive Summary |
|
|
| Assertica is a formally verifiable proof language compiler architected for mathematical certainty and institutional trust. Unlike systems that rely on external theorem provers or statistical verification, Assertica implements a deterministic, fail-closed verification architecture where all mathematical claims require explicit proof terms passing through a small, auditable kernel. |
|
|
| The compiler implements a complete verification pipeline from source code through verified code generation. Every stage is deterministic, every unknown input is rejected, and every proof is explicit. |
|
|
| **Designed for:** Academic institutions, formal verification teams, mathematical research, regulatory compliance contexts requiring auditable computation. |
|
|
| --- |
|
|
| ## Table of Contents |
|
|
| 1. [Architecture Overview](#architecture-overview) |
| 2. [System Design Principles](#system-design-principles) |
| 3. [Verification Pipeline](#verification-pipeline) |
| 4. [Compiler Components](#compiler-components) |
| 5. [Installation & Building](#installation--building) |
| 6. [Usage Guide](#usage-guide) |
| 7. [Testing & Validation](#testing--validation) |
| 8. [Integration Guidelines](#integration-guidelines) |
| 9. [Performance Characteristics](#performance-characteristics) |
| 10. [Security Model](#security-model) |
| 11. [Contributing](#contributing) |
| 12. [Citation](#citation) |
|
|
| --- |
|
|
| ## Architecture Overview |
|
|
| ### Compiler Organization |
|
|
| ``` |
| SOURCE CODE (.as files) |
| β |
| VERIFICATION PIPELINE |
| (9 stages: parse, type-check, verify, generate) |
| β |
| ACCEPT (all checks passed) / REJECT (first error) |
| ``` |
|
|
| ### System Composition |
|
|
| The compiler is built from carefully integrated components that implement the complete verification pipeline. The system is organized for correctness and auditability, not performance optimization. |
|
|
| | Aspect | Details | |
| |--------|---------| |
| | **Total Implementation** | 11,621 lines of Haskell | |
| | **Test Coverage** | 768+ comprehensive tests (>95% coverage) | |
| | **Kernel Size** | ~450 lines (auditable trusted core) | |
| | **Build Time** | ~5 minutes | |
| | **Dependencies** | Zero external theorem provers | |
|
|
| --- |
|
|
| ## System Design Principles |
|
|
| ### 1. Determinism as a First-Class Property |
|
|
| Every computation is deterministic. Given identical input, the compiler produces identical output across all stages. This property is enforced and verified by property-based tests. |
|
|
| **Impact:** |
| - Reproducible builds and verification results |
| - Auditable computation traces |
| - No nondeterministic choice points in verification logic |
| - Property tests confirm: `β input. verify(input) = verify(input)` |
|
|
| ### 2. Fail-Closed Architecture |
|
|
| Unknown inputs are rejected. The system never silently accepts unverified claims. |
|
|
| **Policy:** |
| - Unknown equality β REJECT (not assume equal) |
| - Unproven proposition β REJECT (not assume true) |
| - Invalid proof term β REJECT (not recover) |
| - Missing module β REJECT (not search) |
|
|
| ### 3. Explicit Proof Terms Required |
|
|
| Propositional equality requires proof; definitional equality is deterministically checked. No hidden algebraic axioms. |
|
|
| **Axioms Forbidden:** |
| - Commutativity (a + b = b + a assumed without proof) |
| - Associativity ((a + b) + c = a + (b + c) assumed without proof) |
| - Distributivity (a * (b + c) = a * b + a * c assumed without proof) |
|
|
| **Proof Primitives:** |
| - `Refl`: reflexivity (a = a) |
| - `Symm`: symmetry (a = b β b = a) |
| - `Trans`: transitivity (a = b β b = c β a = c) |
| - `Cong`: congruence (f a = f b from a = b) |
| - `Exact`: exact proof term inclusion |
|
|
| ### 4. Small Trusted Core |
|
|
| The kernel is minimal: 243 lines of deterministic equality checking. Every kernel rule has explicit input, output, and failure case. |
|
|
| **Kernel Properties:** |
| - 243 lines of code |
| - 49+ unit and property tests |
| - No external dependencies |
| - Deterministic semantics |
| - Complete documentation of invariants |
|
|
| ### 5. No External Solvers |
|
|
| Zero reliance on SMT solvers (Z3, CVC5, etc.) or external theorem provers. All reasoning is internal and explicit. |
|
|
| **Prohibited:** |
| - SMT-LIB invocation |
| - Heuristic search |
| - Statistical inference |
| - External solver calls |
| - Probabilistic reasoning |
|
|
| --- |
|
|
| ## Verification Pipeline |
|
|
| ### Complete Pipeline Flow |
|
|
| ``` |
| ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ |
| β SOURCE CODE (Assertica .as files) β |
| βββββββββββββββββββββββββββ¬βββββββββββββββββββββββββββββββββββββββ |
| β |
| ββββββββββββββββββββββββββββββββββ |
| β STAGE 1: LEXICAL ANALYSIS β |
| β β’ Tokenization β |
| β β’ Source location tracking β |
| β β’ Comment handling β |
| ββββββββββββββ¬ββββββββββββββββββ |
| β |
| ββββββββββββββββββββββββββββββββββ |
| β STAGE 2: PARSING β |
| β β’ Recursive descent parsing β |
| β β’ Operator precedence (7 lvl) β |
| β β’ Error recovery β |
| ββββββββββββββ¬ββββββββββββββββββ |
| β |
| ββββββββββββββββββββββββββββββββββ |
| β STAGE 3: ELABORATION β |
| β β’ Surface β Core AST β |
| β β’ Name resolution β |
| β β’ Syntactic sugar expansion β |
| ββββββββββββββ¬ββββββββββββββββββ |
| β |
| ββββββββββββββββββββββββββββββββββ |
| β STAGE 4: TYPE CHECKING β |
| β β’ Type inference β |
| β β’ Universe hierarchy check β |
| β β’ Dependent type validation β |
| ββββββββββββββ¬ββββββββββββββββββ |
| β |
| ββββββββββββββββββββββββββββββββββ |
| β STAGE 5: PROOF VERIFICATION β |
| β β’ Proof term validation β |
| β β’ Explicit proof checking β |
| β β’ No hidden axioms β |
| ββββββββββββββ¬ββββββββββββββββββ |
| β |
| ββββββββββββββββββββββββββββββββββ |
| β STAGE 6: PATTERN ANALYSIS β |
| β β’ Exhaustiveness checking β |
| β β’ Constructor coverage β |
| β β’ Type preservation β |
| ββββββββββββββ¬ββββββββββββββββββ |
| β |
| ββββββββββββββββββββββββββββββββββ |
| β STAGE 7: STRUCTURAL CHECKS β |
| β β’ Termination validation β |
| β β’ Positivity checking β |
| β β’ Mutual recursion analysis β |
| ββββββββββββββ¬ββββββββββββββββββ |
| β |
| ββββββββββββββββββββββββββββββββββ |
| β STAGE 8: MODULE RESOLUTION β |
| β β’ Import resolution β |
| β β’ Circular dependency detectionβ |
| β β’ Topological sorting β |
| ββββββββββββββ¬ββββββββββββββββββ |
| β |
| ββββββββββββββββββββββββββββββββββ |
| β STAGE 9: CODE GENERATION β |
| β β’ AST β Haskell translation β |
| β β’ Type-safe code emission β |
| β β’ GHC-valid syntax β |
| ββββββββββββββ¬ββββββββββββββββββ |
| β |
| ββββββββββββββββββββββββββββββββββ |
| β FINAL VERDICT β |
| β β ACCEPT (all checks passed) β |
| β β REJECT (first error halts) β |
| ββββββββββββββββββββββββββββββββββ |
| ``` |
|
|
| ### Pipeline Semantics |
|
|
| **Fail-Closed Execution:** The pipeline halts at the first error. No error recovery. No continuation after failure. |
|
|
| **Deterministic Ordering:** Each stage executes sequentially. No parallel execution that could introduce nondeterminism. |
|
|
| **Complete Error Reporting:** Every rejection includes: |
| - Error category (SyntaxError, TypeError, ProofObligation, etc.) |
| - Source location (file:line:column) |
| - Error message (clear, actionable description) |
| - Context (source code snippet) |
| - Suggested fix (when applicable) |
|
|
| --- |
|
|
| ## Installation & Building |
|
|
| ### Prerequisites |
|
|
| - **Haskell GHC:** 9.2 or later |
| - **Cabal:** 3.6 or later |
| - **Build time:** ~5 minutes on standard hardware |
|
|
| ### Build Instructions |
|
|
| ```bash |
| # Clone repository |
| git clone https://github.com/SNAPKITTYAGENT9NOVA/Assertica.git |
| cd Assertica |
| |
| # Build library |
| cabal build lib:assertica |
| |
| # Build and run tests |
| cabal test |
| |
| # Build CLI tool |
| cabal build exe:assertica-verify |
| |
| # Install to PATH |
| cabal install |
| ``` |
|
|
| ### Verification |
|
|
| After build, verify installation: |
|
|
| ```bash |
| # Run all 768+ tests |
| cabal test --verbose |
| |
| # Check library loads |
| ghci |
| > import Assertica.Core.Equality |
| > isDefinitionallyEqual (TConst "x") (TConst "x") |
| True |
| ``` |
|
|
| --- |
|
|
| ## Usage Guide |
|
|
| ### Command-Line Interface |
|
|
| ```bash |
| # Verify single file |
| assertica-verify --file program.as |
| |
| # Verify entire directory |
| assertica-verify --dir ./programs |
| |
| # Generate Haskell code |
| assertica-verify --file program.as --generate-haskell |
| |
| # JSON output for CI |
| assertica-verify --dir ./programs --output json > report.json |
| |
| # Strict mode (warnings become errors) |
| assertica-verify --strict --dir ./programs |
| ``` |
|
|
| ### Programmatic Usage (Haskell) |
|
|
| ```haskell |
| import Assertica.Verify.Pipeline |
| import Assertica.Verify.Report |
| |
| -- Verify single file |
| report <- verifyFile "example.as" |
| case verdict report of |
| Accept -> putStrLn "Verification successful" |
| Reject -> putStrLn $ "Verification failed: " ++ show (errors report) |
| |
| -- Batch verification |
| reports <- verifyDirectory "./programs" |
| let passCount = length $ filter (\r -> verdict r == Accept) reports |
| putStrLn $ "Verified " ++ show passCount ++ " files" |
| ``` |
|
|
| ### Example: Proof with Explicit Terms |
|
|
| ```assertica |
| -- Theorem: reflexivity of equality |
| theorem refl_eq : β(a : Type), a = a |
| proof := Refl |
| |
| -- Theorem: transitivity |
| theorem trans_eq : β(a b c : Type), (a = b) β (b = c) β (a = c) |
| proof := Ξ» a b c hab hbc. Trans hab hbc |
| |
| -- Lattice absorption |
| theorem absorption : β(L : Lattice)(a b : L.carrier), |
| (a β (a β b)) = a |
| proof := absorbptionProof a b |
| ``` |
|
|
| --- |
|
|
| ## Testing & Validation |
|
|
| ### Test Suite Structure |
|
|
| | Category | Count | Purpose | |
| |----------|-------|---------| |
| | Unit tests | 450+ | Individual component verification | |
| | Integration tests | 200+ | Cross-component interaction | |
| | Property tests | 80+ | Determinism, idempotence | |
| | Negative tests | 38+ | Rejection of invalid input | |
| | **TOTAL** | **768+** | Complete system validation | |
|
|
| ### Running Tests |
|
|
| ```bash |
| # All tests |
| cabal test |
| |
| # Single module |
| cabal test --test-show-details=direct test:assertica-tests -- --match="Equality" |
| |
| # With coverage |
| cabal test --enable-coverage |
| ``` |
|
|
| ### Coverage |
|
|
| **Current Coverage:** >95% across all modules |
|
|
| **Critical Path:** 100% coverage for kernel (Equality, Proof Checker core) |
|
|
| --- |
|
|
| ## Integration Guidelines |
|
|
| ### For Academic Institutions |
|
|
| **Use Cases:** |
| - Formal methods courses (graduate-level) |
| - Proof assistant teaching |
| - Mathematical verification research |
|
|
| **Integration:** |
| 1. Review `CONTRIBUTING.md` for contribution policy |
| 2. Study kernel architecture (243 lines, Equality module) |
| 3. Extend algebraic hierarchy in Standard Library |
| 4. Contribute new proof strategies (non-invasive) |
|
|
| ### For Verification Teams |
|
|
| **Use Cases:** |
| - Critical system verification |
| - Safety-critical software verification |
| - Mathematical proof of correctness |
|
|
| **Integration:** |
| 1. Use CLI for batch verification |
| 2. Integrate with CI/CD via JSON output |
| 3. Custom error handling via Report module |
| 4. Code generation for executable verification |
|
|
| ### For Compiler Developers |
|
|
| **Use Cases:** |
| - Language design exploration |
| - Proof language implementation |
| - Verification infrastructure |
|
|
| **Integration:** |
| 1. Study complete pipeline (9 stages) |
| 2. Extend surface syntax (Parser/Elaborator) |
| 3. Add new proof primitives (Proof Checker) |
| 4. Implement custom backends (Code Generator) |
|
|
| --- |
|
|
| ## Performance Characteristics |
|
|
| ### Compilation Speed |
|
|
| | Stage | Time (ms) | Complexity | |
| |-------|-----------|------------| |
| | Lexing | 0-5 | O(n) | |
| | Parsing | 5-50 | O(n log n) | |
| | Elaboration | 10-100 | O(nΒ²) | |
| | Type checking | 50-500 | O(nΒ³) | |
| | Proof checking | 10-100 | O(m) (proof size) | |
| | Pattern analysis | 5-50 | O(cΒ²) (constructors) | |
| | Termination check | 50-200 | O(eΒ²) (edges in call graph) | |
| | Module resolution | 5-20 | O(m log m) (modules) | |
| | Code generation | 20-100 | O(n) | |
|
|
| **Total End-to-End:** 160-1,120 ms for typical 1,000-line program |
|
|
| ### Memory Usage |
|
|
| - Small programs (<10 KB): ~10 MB resident |
| - Medium programs (100 KB): ~50 MB resident |
| - Large programs (1 MB): ~200 MB resident |
|
|
| ### Scalability |
|
|
| - **Deterministic:** No degradation with repeated runs |
| - **Linear in source size:** Proportional to input LOC |
| - **Quadratic in recursion depth:** Mutual recursion analysis O(eΒ²) |
|
|
| --- |
|
|
| ## Security Model |
|
|
| ### Threat Model |
|
|
| This system addresses formal verification threats, not cryptographic security. See `SECURITY.md` for detailed security analysis. |
|
|
| **Protected Against:** |
| - Silent acceptance of unproven claims |
| - Hidden algebraic axiom invocation |
| - Nondeterministic verification results |
| - Circular module dependencies |
| - Non-terminating recursion |
| - Logically inconsistent types |
|
|
| **Not Protected Against:** |
| - Malicious hardware |
| - Side-channel attacks |
| - Compiler bugs in GHC (outside scope) |
| - Denial-of-service via infinite recursion (mitigated by termination checker) |
|
|
| ### Kernel Auditing |
|
|
| The kernel (243 lines, Equality Checker) is sized for complete human auditing: |
|
|
| 1. Read source code (15 minutes) |
| 2. Understand invariants (15 minutes) |
| 3. Trace execution (30 minutes) |
| 4. Review tests (30 minutes) |
| 5. **Total audit time:** ~90 minutes for one person |
|
|
| --- |
|
|
| ## Contributing |
|
|
| See [CONTRIBUTING.md](./CONTRIBUTING.md) for complete contribution guidelines. |
|
|
| **Quick Start:** |
| 1. Fork repository |
| 2. Create feature branch (`git checkout -b feature/name`) |
| 3. Implement with tests (maintain >95% coverage) |
| 4. Run full test suite (`cabal test`) |
| 5. Submit PR with description |
|
|
| **Code Review Process:** |
| - Kernel changes: 2+ institutional reviews required |
| - Non-kernel changes: 1+ review required |
| - All contributors sign DCO (Developer Certificate of Origin) |
|
|
| --- |
|
|
| ## Citation |
|
|
| If you use Assertica in research or publication, please cite: |
|
|
| ```bibtex |
| @software{assertica2026, |
| title={Assertica: Deterministic Proof Language Compiler}, |
| author={Parr, Ahmad Ali}, |
| year={2026}, |
| url={https://github.com/SNAPKITTYAGENT9NOVA/Assertica}, |
| note={Haskell implementation, v1.0.0} |
| } |
| ``` |
|
|
| --- |
|
|
| ## Appendix: Statistics Summary |
|
|
| | Metric | Value | |
| |--------|-------| |
| | Total lines of code | 11,621 | |
| | Kernel lines (critical path) | 243 | |
| | Test lines | 4,200+ | |
| | Test cases | 768+ | |
| | Test coverage | >95% | |
| | Compiler modules | 6 layers | |
| | Pipeline stages | 9 | |
| | Proof primitives | 7 | |
| | Proposition types | 8 | |
| | Error categories | 6 | |
| | Universe levels | β (Hierarchy) | |
| | Build time | ~5 minutes | |
| | Total documentation | 15,000+ words | |
|
|
| --- |
|
|
| ## License |
|
|
| Licensed under **BSL-1.0 (Boost)**. Full text: [LICENSE](LICENSE). |
|
|
| ## Support |
|
|
| - **Issues:** GitHub Issues for bug reports and feature requests |
| - **Discussions:** GitHub Discussions for architecture questions |
| - **Security:** See SECURITY.md for vulnerability reporting |
| - **Academic:** Contact maintainers for research collaboration |
|
|
| --- |
|
|
| **Last Updated:** 2026-10-03 |
| **Version:** 1.0.0 |
| **Status:** Production Ready |
|
|
