snpz 1.0.1
A foundational language and runtime for defining invariant-first contracts
Requires Python: >=3.10
Keywords: ai, contracts, invariants, safety, verification

# snpz

**Define rules once. Let AI write code safely.**

snpz is a language and runtime for defining invariant-first contracts that constrain AI- and human-driven software changes. Instead of hoping AI follows instructions, you define what's allowed — and snpz deterministically verifies every change.

## The Problem

AI can write code fast, but it can't guarantee safety. Critical rules get missed. Invariants get broken. Production breaks.

snpz flips this: you define the rules once (state, invariants, effects), and snpz acts as a verifier. If a change violates your rules, snpz rejects it with a precise explanation.

## Philosophy

snpz is:
- **Not a framework** — it's a language for contracts
- **Not a code generator** — it's a verifier
- **Not a configuration format** — it's a deterministic runtime

Think of it like:
- **git** for history
- **terraform** for contracts
- **types** for safety

...but applied to AI-driven change verification.

## Installation

### From PyPI (recommended)

```bash
# Install globally
pip install snpz

# Or use pipx for isolated installation
pipx install snpz
```

### From source

```bash
git clone https://github.com/thisiselvinsuleymanov/snpz.git
cd snpz
pip install -e ".[dev]"
```

### Docker

```bash
# Pull from GitHub Container Registry
docker pull ghcr.io/thisiselvinsuleymanov:latest

# Or build locally
docker build -t snpz .
```

## 30-Second Quickstart

Create a contract file `balance.snpz`:

```snpz
contract Balance {
  state {
    balance: number
  }

  invariant NonNegative: balance >= 0 else "Balance must never be negative"

  effect debit(amount: number) {
    require amount >= 0 else "Debit amount must be non-negative"
    set balance = balance - amount
  }
}
```

Create a state file `state.json`:

```json
{
  "balance": 100
}
```

Create an args file `args.json`:

```json
{
  "amount": 30
}
```

Apply the effect:

```bash
snpz apply balance.snpz debit --state state.json --args args.json --pretty
```

Output:
```
✓ Effect applied successfully

New state:
{
  "balance": 70.0
}
```

## Example: REJECT with Explanation

Now try to debit more than the balance:

```json
{
  "amount": 150
}
```

```bash
snpz apply balance.snpz debit --state state.json --args args.json --pretty
```

Output:
```
✗ Effect rejected: Balance must never be negative
  Reason type: INVARIANT_VIOLATION

Trace:
  Requires:
    ✓ amount >= 0
  Sets:
    balance: 100.0 → -50.0
  Invariants:
    ✗ NonNegative
```

The effect was **rejected** because it would violate the `NonNegative` invariant. The trace shows exactly what happened:
1. The `require` passed (amount was positive)
2. The balance was updated to -50
3. The invariant check **failed**

This is the core value of snpz: **deterministic rejection with precise explanations**.

## Language Features

### State

Define the shape of your data:

```snpz
state {
  balance: number
  status: enum{PENDING|APPROVED|REJECTED}
  approved_by: optional<string>
  limits: record {
    daily: number
    monthly: number
  }
}
```

Supported types:
- `number` (Decimal internally)
- `bool`
- `string`
- `enum{A|B|C}`
- `optional<T>`
- `record { field: type, ... }`

### Invariants

Rules that must **always** hold:

```snpz
invariant NonNegativeBalance: balance >= 0 else "Balance cannot be negative"
invariant WithinLimit: balance <= limits.daily else "Exceeds daily limit"
```

Invariants are checked **after** every effect.

### Effects

The **only** allowed mutations:

```snpz
effect debit(amount: number) {
  require amount >= 0 else "Amount must be non-negative"
  require amount <= balance else "Insufficient balance"
  set balance = balance - amount
}
```

- `require` statements are checked **before** mutation
- `set` statements are evaluated on the **old state**
- All mutations are applied **atomically**
- All invariants are checked **after** mutation

### Expressions

Sandboxed and deterministic:
- Arithmetic: `+`, `-`, `*`, `/`
- Comparison: `==`, `!=`, `<`, `<=`, `>`, `>=`
- Boolean: `and`, `or`, `not`
- Built-in functions: `min(a, b)`, `max(a, b)`

No user-defined functions. No loops. No recursion. No I/O. No randomness.

## CLI Commands

### Validate

Check if a contract is valid:

```bash
snpz validate balance.snpz --pretty
```

### Check

Check invariants on a state:

```bash
snpz check balance.snpz --state state.json --pretty
```

### Apply

Apply an effect to a state:

```bash
snpz apply balance.snpz debit --state state.json --args args.json --pretty
```

### Test

Run test cases:

```bash
snpz test balance.snpz --cases examples/balance_cases
```

### Format

Format a contract:

```bash
snpz fmt balance.snpz --write
```

## Docker Usage

### Running with Docker

```bash
# Validate a contract
docker run --rm -v "$PWD:/work" -w /work ghcr.io/thisiselvinsuleymanov:latest validate contract.snpz

# Run tests
docker run --rm -v "$PWD:/work" -w /work ghcr.io/thisiselvinsuleymanov:latest test contract.snpz --cases test_cases/

# Apply an effect
docker run --rm -v "$PWD:/work" -w /work ghcr.io/thisiselvinsuleymanov:latest apply contract.snpz effect_name --state state.json --args args.json
```

### CI/CD Integration

GitHub Actions example:

```yaml
jobs:
  verify:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4

      - name: Validate contracts
        run: |
          docker run --rm -v "$PWD:/work" -w /work ghcr.io/thisiselvinsuleymanov:latest validate contracts/*.snpz

      - name: Run contract tests
        run: |
          docker run --rm -v "$PWD:/work" -w /work ghcr.io/thisiselvinsuleymanov:latest test contracts/main.snpz --cases test_cases/
```

GitLab CI example:

```yaml
verify_contracts:
  image: ghcr.io/thisiselvinsuleymanov:latest
  script:
    - snpz validate contracts/*.snpz
    - snpz test contracts/main.snpz --cases test_cases/
```

## Test Cases

Test cases are JSON files that describe expected outcomes:

```json
{
  "name": "Debit rejected when would cause negative balance",
  "state": {
    "balance": 100
  },
  "apply": {
    "effect": "debit",
    "args": {
      "amount": 150
    }
  },
  "expect": {
    "status": "REJECT",
    "reason_type": "INVARIANT_VIOLATION"
  }
}
```

## Trace Output

Every `apply` produces a deterministic trace:

```json
{
  "status": "REJECT",
  "reason": "Balance must never be negative",
  "reason_type": "INVARIANT_VIOLATION",
  "trace": {
    "requires": [
      {
        "condition": "amount >= 0",
        "result": true
      }
    ],
    "sets": [
      {
        "target": "balance",
        "old_value": 100.0,
        "new_value": -50.0
      }
    ],
    "invariants": [
      {
        "invariant": "NonNegative",
        "result": false
      }
    ]
  }
}
```

This trace is a **first-class feature** — it explains exactly why an effect was rejected.

## Examples

See the `examples/` directory for complete contracts:

- `balance.snpz` — Simple balance with credit/debit
- `approval.snpz` — Approval workflow with status and limits

Run tests on examples:

```bash
snpz test examples/balance.snpz --cases examples/balance_cases
```

## Development

Install dependencies:

```bash
pip install -e ".[dev]"
```

Run tests:

```bash
pytest
```

## Non-Goals

snpz is **not**:
- A code generator
- An IDE plugin
- A database
- An AI prompting system
- An automatic invariant inference tool

It's a **verifier** and **contract language** only.

## License

MIT