CONTRIBUTING.md

Contributing to Assertica

Thank you for your interest in contributing to Assertica, a deterministic proof language compiler. This document provides guidelines for participating in the project.

---

Table of Contents

1. Code of Conduct
2. Getting Started
3. Development Setup
4. Contribution Types
5. Coding Standards
6. Testing Requirements
7. Submission Process
8. Review Process
9. DCO: Developer Certificate of Origin
10. Architecture Constraints

---

Code of Conduct

Assertica is committed to providing a welcoming and inclusive environment. All contributors are expected to:

• Be respectful and professional
• Provide constructive feedback
• Focus on the technical merit of ideas
• Respect intellectual property
• Acknowledge contributions appropriately

Violations can be reported to project maintainers privately.

---

Getting Started

Prerequisites

• Haskell GHC: 9.2 or later
• Cabal: 3.6 or later
• Git: For version control
• familiarity with:
  • Haskell programming language
  • Formal verification concepts
  • Type systems and proof theory

Initial Setup

# Fork repository on GitHub
# Clone your fork
git clone https://github.com/YOUR_USERNAME/Assertica.git
cd Assertica

# Add upstream remote for syncing
git remote add upstream https://github.com/SNAPKITTYAGENT9NOVA/Assertica.git

# Create development branch
git checkout -b feature/your-feature-name

# Build and test
cabal build
cabal test

---

Development Setup

Environment Configuration

# Recommended cabal configuration for development
mkdir -p ~/.cabal
cat >> ~/.cabal/cabal.config << 'EOF'
ghc-options: -Wall -Wcompat -Wincomplete-record-updates -Wincomplete-uni-patterns -Wredundant-constraints -fhide-source-paths
tests: True
benchmarks: True
EOF

# Build with coverage
cabal build --enable-coverage

# Install tools for linting (optional but recommended)
cabal install hlint stylish-haskell

Daily Workflow

# After pulling changes
git fetch upstream
git rebase upstream/main

# Before committing
cabal format  # Format .cabal file
cabal build
cabal test --verbose

# Submit
git push origin feature/your-feature-name
# Create pull request on GitHub

---

Contribution Types

1. Bug Fixes

Criteria:

• Clear reproduction steps
• Affects functionality or correctness
• Not a known limitation
• Minimal risk to other components

Process:

1. Create issue describing bug with reproduction
2. Reference issue in PR (Fixes #123)
3. Include test case demonstrating fix
4. Update documentation if needed

Example:

-- Before: incorrect behavior
buggyFunction x = x + 1

-- After: corrected
buggyFunction x = x + 2

-- Test
test_buggy = assertEqual 3 (buggyFunction 2)

2. Feature Enhancements (Non-Kernel)

Eligible Components:

• Standard library (Standard Library module)
• Backend code generation (Code Generator module)
• Verification reporting (Verification Pipeline module)
• CLI tools (Verification Pipeline module)
• Test infrastructure

Ineligible Components (Kernel):

• Core AST (Core AST module)
• Equality checker (Equality Checker module)
• Proof checker (Proof Checker module)
• Type checker (Type Checker module)

Process:

1. Open discussion issue first
2. Wait for maintainer feedback (24-72 hours)
3. If approved, proceed with implementation
4. Follow coding standards
5. Add comprehensive tests (min. 30 tests for new modules)
6. Submit PR with detailed description

3. Documentation Improvements

Eligible:

• README clarifications
• Architecture explanations
• Usage examples
• Inline code comments
• API documentation
• Tutorial content

Process:

1. Submit PR directly (no issue required)
2. Clear, technical writing
3. Example code must be tested
4. Build documentation locally to verify:

   cabal haddock --haddock-html --open
   

4. Test Coverage Expansion

Requirements:

• Tests for uncovered code paths
• Determinism verification tests
• Property tests for invariants
• Negative tests (what should fail)
• Integration tests

Process:

1. Identify untested code
2. Write comprehensive tests
3. Verify code coverage:

   cabal test --enable-coverage
   cat dist/hpc/html/index.html
   

4. Submit PR with test module

5. Refactoring (Non-Kernel Only)

Constraints:

• No behavior change
• No API change (externally)
• Improves readability or performance
• All tests pass unchanged

Process:

1. Open RFC (Request for Comments) issue
2. Wait for approval
3. Refactor with all tests passing
4. Include before/after performance metrics
5. Document rationale in PR

---

Coding Standards

Haskell Style Guide

Module Structure:

{-|
Module      : Assertica.Component.SubComponent
Description : One-line description
Copyright   : (c) 2026 Ahmad Ali Parr
License     : BSL 1.0

Detailed description of module purpose and responsibilities.
Important invariants and guarantees.
-}

{-# LANGUAGE pragmas #-}

module Assertica.Component.SubComponent
  ( -- * Public API
    publicFunction
  , PublicType(..)
    -- * Internal helpers (for testing only)
  , internalHelper
  ) where

import qualified Data.Set as Set
import qualified Data.Map.Strict as Map

Documentation:

• Every public function has a Haddock comment
• Document type signatures with examples
• Explain non-obvious invariants
• Note side effects clearly

Example: ```haskell -- | Check deterministic equality of two terms

-- Two terms are equal if they normalize to the same canonical form -- (modulo alpha equivalence).

-- Examples: -- isEqual (TApp (TAbs x (TVar x)) (TConst "5")) (TConst "5") == True -- isEqual (TVar (Var "x")) (TVar (Var "y")) == False

-- Properties: -- - Deterministic: always returns same result for same input -- - Idempotent: isEqual t1 t2 == isEqual t1 t2 isEqual :: Term -> Term -> Bool isEqual t1 t2 = alphaEquivalent (normalize t1) (normalize t2)

**Naming Conventions:**
- Types: CamelCase (`Term`, `Assertion`)
- Functions: camelCase (`isDefinitionallyEqual`)
- Constants: SCREAMING_SNAKE_CASE (rarely used)
- Type variables: single lowercase letter or descriptive (`a`, `term`)
- Predicates: prefix with `is` or `has` (`isValid`, `hasProperty`)

**Formatting:**
```bash
# Use cabal's built-in formatter
cabal format

# For Haskell code, use consistent indentation
# 2 spaces for indentation (project standard)
# Line length: prefer <100 characters (max 120)

# Example:
foo :: Term -> Term -> Bool
foo t1 t2 =
  let normalized1 = normalize t1
      normalized2 = normalize t2
  in alphaEquivalent normalized1 normalized2

Error Handling:

• Use Either String a for recoverable errors
• Use Maybe a for optional values
• Never use error or undefined in production code
• Provide meaningful error messages

-- Good: clear error message
checkTerm :: Term -> Either String ()
checkTerm t
  | isWellFormed t = Right ()
  | otherwise = Left $ "Malformed term: " ++ show t

-- Bad: unhelpful message
checkTerm _ = Left "Error"

---

Testing Requirements

Minimum Coverage

• New modules: 95% code coverage minimum
• Existing modules: No decrease in coverage
• Critical path (Equality Checker module, 2B): 100% coverage required

Test Structure

module Test.YourModule where

import Test.HUnit
import Test.QuickCheck
import Assertica.YourModule

-- Unit tests
test_basic :: Test
test_basic = TestCase $ assertEqual "basic case"
  expected
  (yourFunction input)

-- Property tests
prop_deterministic :: Term -> Bool
prop_deterministic t = 
  normalize t === normalize t

-- Negative tests (what should fail)
test_rejectInvalid :: Test
test_rejectInvalid = TestCase $ 
  assertEqual "reject invalid"
    (Left "error")
    (validate invalidInput)

-- Comprehensive test suite
main :: IO ()
main = do
  runTestTT $ TestList
    [ test_basic
    , test_another
    ]
  quickCheckResult prop_deterministic

Test Organization

test/Test/Component/
├── SubComponentA.hs       # Tests for Agent/Component
├── SubComponentB.hs       # One file per component
└── Integration.hs         # Cross-component tests

Running Tests

# All tests with verbose output
cabal test --test-show-details=direct

# Specific test
cabal test --test-show-details=direct test:assertica-tests -- --match="Equality"

# With coverage
cabal test --enable-coverage
cabal open dist/hpc/html/index.html

---

Submission Process

Before Submitting

Checklist:

• Code follows style guide
• New functions documented with examples
• All tests pass (cabal test)
• Test coverage >95% for new code
• No compiler warnings (-Wall)
• Determinism verified (property tests)
• Negative tests included
• CONTRIBUTING.md DCO clause signed
• Commit message clear and descriptive

Commit Message Format:

[Component] Brief description (50 chars max)

Detailed explanation of changes. Wrap at 72 characters.
Mention related issues: Fixes #123, Related to #456

Architectural decisions and trade-offs if relevant.

Co-Authored-By: Your Name <email@example.com> (if applicable)

Examples:

[Standard Library module] Add Lattice.absorbptionProof function

Implements the absorption theorem proof for lattice structures:
a ⊔ (a ⊓ b) ≈ a

Adds 24 unit tests covering all absorption cases and
proof composition. Verifies proof terms are checked by
Proof Checker module proof checker.

Fixes #145

Submitting a Pull Request

# Ensure you're up to date
git fetch upstream
git rebase upstream/main

# Push to your fork
git push origin feature/your-feature-name

# Create PR on GitHub with detailed description

PR Template:

## Description
Brief summary of changes

## Motivation
Why is this change needed?

## Changes
- List of modifications
- Affected components
- New files (if any)

## Testing
- Tests added: X unit tests, Y property tests
- Coverage: Z%
- Manual testing: describe what was tested

## Checklist
- [ ] Tests pass locally
- [ ] Coverage maintained/improved
- [ ] Documentation updated
- [ ] DCO signed
- [ ] No breaking changes (if applicable)

## Related Issues
Fixes #123

---

Review Process

Code Review Policy

Kernel Changes (Equality Checker module, 2B):

• Requires 2+ architectural reviews
• 48-hour review period minimum
• All feedback must be addressed
• No force-merge allowed
• Maintainer approval required

Non-Kernel Changes:

• Requires 1 maintainer review
• 24-hour review period (unless urgent)
• Feedback incorporated or explained
• One approval to merge

Review Criteria

Reviewers will evaluate:

1. Correctness

   • Does it solve the stated problem?
   • Are edge cases handled?
   • Are there any logical errors?

2. Quality

   • Code clarity and maintainability
   • Adherence to style guide
   • Test coverage and quality

3. Performance

   • No unnecessary allocations
   • Complexity appropriate to task
   • No regressions in benchmarks

4. Architecture

   • Fits within role pair boundaries
   • Clean interfaces
   • No hidden dependencies

5. Documentation

   • Clear explanations
   • Examples where helpful
   • Updated README if needed

Addressing Feedback

• Respond to every comment
• Acknowledge valid points
• Explain disagreements respectfully
• Use "Resolve conversation" only after feedback addressed
• Push updates to same branch (don't force-push)

---

DCO: Developer Certificate of Origin

By submitting a pull request, you certify that:

Developer Certificate of Origin
Version 1.1

By making a contribution to this project, I certify that:

(a) The contribution was created in whole or in part by me and I
    have the right to submit it under the open source license
    indicated in the file; or

(b) The contribution is based upon previous work that, to the best
    of my knowledge, is covered under an appropriate open source
    license and I have the right under that license to submit that
    work with modifications, whether created in whole or in part
    by me, under the same open source license (unless I am
    permitted to submit under a different license), as indicated
    in the file; or

(c) The contribution was provided directly to me by some other
    person who certified (a), (b) or (c) and I have not modified
    it.

(d) I understand and agree that this project and the contribution
    are public and that a record of the contribution (including all
    personal information I submit with it, including my sign-off) is
    maintained indefinitely and may be redistributed consistent with
    this project or the open source license(s) involved.

Sign-off: Include in commit message:

Signed-off-by: Your Name <your.email@example.com>

Git configuration:

git config --global user.name "Your Name"
git config --global user.email "your.email@example.com"
git commit -s  # Automatically sign-off

---

Architecture Constraints

Module Boundaries

Contributions must respect module architecture boundaries:

Layer	Modules	Contribution Allowed	Contribution Forbidden
Kernel	Core AST, Equality Checker	Tests, documentation	Core AST, equality logic
Verification	Assertion System, Proof Checker	Proof primitives, tests	Proof checker core logic
Syntax	Parser/Elaborator, Type Checker	Surface syntax, type inference tests	Type system fundamentals
Safety	Pattern Compiler, Termination/Positivity	New safety checks	Pattern/termination algorithms
Organization	Module System, Standard Library	Algebraic structures, standard library	Module system core
Emission	Code Generator, Verification Pipeline	Code generation backends, CLI	Pipeline orchestration

Invariants That Cannot Change

These are inviolable (violations rejected in review):

1. Determinism: Same input must produce identical output
2. Fail-Closed: Unknown inputs must be rejected, never silently accepted
3. No Algebraic Axioms: Commutativity, associativity, distributivity forbidden in kernel
4. Proof Requirements: Propositional equality requires explicit proof
5. No SMT Solvers: Zero external theorem prover calls
6. No Unsafe Code: No unsafeCoerce, unsafePerformIO, etc.

Integration Points

When adding features, ensure clean integration:

• Use existing equality checker (Equality Checker module) - don't reimplement
• All proof verification goes through Proof Checker module
• Type environment via Type Checker module's API
• Module resolution via Module System module
• Code generation through Code Generator module's interfaces

---

Common Contribution Patterns

Adding a New Algebraic Structure (Standard Library module)

1. Create new module: src/Assertica/StdLib/YourStructure.hs
2. Define structure (analogous to Setoid, Lattice)
3. Prove algebraic laws with explicit proof terms
4. Create test module: test/Test/StdLib/YourStructure.hs
5. Add 30+ comprehensive tests
6. Update assertica.cabal with new modules
7. Submit PR with architecture discussion

Extending Parser/Elaborator (Parser/Elaborator module)

1. Extend token types in Lexer.hs if needed
2. Add parser rule in Parser.hs
3. Add elaborator case in Elaborator.hs
4. Update surface AST (Surface/AST.hs)
5. Add 20+ parser tests
6. Add 15+ elaborator tests
7. Document syntax in examples
8. Submit PR with grammar specification

Adding Backend Code Generation (Code Generator module)

1. Extend target language support in CodeGen.hs
2. Implement term compilation in appropriate compiler
3. Ensure generated code is type-safe
4. Add 15+ end-to-end tests
5. Verify output compiles with target compiler
6. Benchmark code generation performance
7. Submit PR with performance analysis

---

Frequently Asked Questions

Q: Can I modify the kernel (Equality Checker module)? A: Only for critical bug fixes. Changes require 2+ architectural reviews. Bug fix must have failing test demonstrating issue, and passing test after fix.

Q: What if I disagree with reviewer feedback? A: Respectfully explain your position. If disagreement persists, maintainers make final decision. Disagreement is not grounds for force-merge.

Q: How long does review typically take? A: 24-72 hours for non-kernel, 48+ hours for kernel. Depends on complexity and reviewer availability.

Q: Can I work on multiple features in parallel? A: Yes, use separate branches and PRs. Avoid large PRs (500+ lines) - break into logical units.

Q: What if my contribution introduces a performance regression? A: Regressions must be justified and fixed before merge. Include benchmarks showing impact.

---

Getting Help

• Architecture questions: Open discussion issue
• Technical questions: GitHub Discussions
• Bug reports: GitHub Issues
• Security issues: See SECURITY.md
• Email: Contact project maintainers

---

Last Updated: 2026-10-03 Version: 1.0.0