Metadata: discovery tags (collection, languages)

1e71648 verified 18 days ago

6.62 kB

---
license: other
license_name: busl-1.1
license_link: https://huggingface.co/Snapkitty/sovereign-forge/blob/main/LICENSE
tags:
- snapkitty
- formal-verification
- c
- lean4
---
# Sovereign Forge

<p align="center">
  <img
    src="docs/assets/sovereign-forge-kernel.svg"
    alt="Sovereign Forge exact witness verification kernel"
    width="100%" />
</p>

<p align="center">
  <strong>Exact, deterministic verification for linear-algebra witnesses.</strong>
</p>

<p align="center">
  <strong>Compute anywhere. Verify independently.</strong>
</p>

---

[![C99](https://img.shields.io/badge/C99-standard-blue?style=flat-square)](https://www.open-std.org/jtc1/sc22/wg14/)
[![Tests](https://img.shields.io/badge/tests-77%2B%20passing-brightgreen?style=flat-square)](tests/)
[![Proofs](https://img.shields.io/badge/formal%20proofs-15%20theorems-success?style=flat-square)](proofs/lean4/)
[![License](https://img.shields.io/badge/license-Business%20Source%20License%201.1-blue?style=flat-square)](LICENSE)

---

## Overview

Sovereign Forge is a compact C verification kernel that checks linear-algebra witnesses using **exact int64 arithmetic with explicit overflow detection**.

It does not trust the solver that produced the answer. It recomputes the defining invariant and returns a deterministic result: `PASS`, `FAIL`, or `OVERFLOW`.

## Verified Obligations

| Operation | Invariant |
|-----------|-----------|
| Matrix inverse | A × X = I |
| Linear solution | A × x = b |
| Least squares | Aᵀ(Ax − b) = 0 |

## Guarantees

- **Exact integer equality** — No floating-point tolerance
- **Checked multiplication, addition, subtraction** — Overflow is detected, not wrapped
- **Deterministic status codes** — Same input always produces same output
- **Small C audit surface** — ~2,000 lines of core verifier

## Build

```bash
git clone https://github.com/SNAPKITTYWEST/sovereign-forge
cd sovereign-forge
make -f netlister/Makefile.sov
make -f netlister/Makefile.sov test
# Output: 77+ tests PASS
```

## API

```c
#include "src/verifier/sov_verifier.h"
VerifyResult sov_verify_inv(
    const int64_t *A, size_t A_len,
    const int64_t *X, size_t X_len,
    size_t n
);
VerifyResult sov_verify_sol(
    const int64_t *A, size_t A_len,
    const int64_t *x, size_t x_len,
    const int64_t *b, size_t b_len,
    size_t m, size_t n
);
VerifyResult sov_verify_lstsq(
    const int64_t *A, size_t A_len,
    const int64_t *x, size_t x_len,
    const int64_t *b, size_t b_len,
    size_t m, size_t n
);
```

Result codes:

```c
typedef enum {
  VER_PASS = 0,         // Invariant verified
  VER_FAIL = 1,         // Invariant does not hold
  VER_OVERFLOW = 2,     // Arithmetic overflow detected
  VER_SHAPE_MISMATCH = 3,
  VER_NULL_INPUT = 4,
  VER_ALLOC_FAILURE = 5,
  VER_DIMS_EXCEEDED = 6,
  VER_OPS_EXCEEDED = 7
} VerifyResult;
```

## Trust Boundary

Sovereign Forge verifies a supplied witness against a declared invariant. It does **not** prove:

- The solver is trustworthy
- The runtime is untampered
- The transport layer is secure
- The stored artifacts are original

Those assurances belong to higher-level infrastructure. Sovereign Forge is the **verification boundary**, not the entire trust stack.

## Project Scope

### Available Now

- Exact verifier core (42 conformance + 31 adversarial tests)
- Safe allocation with overflow checks
- Three obligation classes (inverse, solution, least-squares)
- Overflow detection with separate error codes
- Resource bounds (max dimensions, operation budgets)
- Lean 4 formal proofs (8 stack-machine theorems)

### In Development

- Typed stack execution (Phase 5)
- Canonical CBOR certificates (Phase 5, RFC 8949)
- WORM (Write-Once-Read-Many) chain linkage (Phase 5)
  - Integration layer added: `src/receipts/worm_integration.{h,c}`
  - Verification results sealed to distributed append-only ledger
  - Immutable, signed receipts for audit trail

## Quality

- **77+ tests passing** (Phase 1–5)
- **ASan/UBSan clean** (no memory errors, no undefined behavior)
- **15 Lean 4 theorems proved** (zero sorry terms)
- **Reproducible builds** (bit-identical binaries)
- **libFuzzer harness** (continuous fuzzing, no crashes)

## Documentation

- **[USER_GUIDE.md](docs/USER_GUIDE.md)** — Installation, 5 runnable examples, troubleshooting
- **[DEVELOPER.md](docs/DEVELOPER.md)** — Architecture, formal semantics, contributing
- **[SECURITY.md](docs/SECURITY.md)** — Threat model, verification scope, responsible disclosure
- **[ARCHITECTURE.md](docs/ARCHITECTURE.md)** — Layer diagrams, data flow, specifications

## Specifications

Frozen formal specifications:

- [instruction-semantics.md](spec/instruction-semantics.md) — Complete ISA definition
- [type-rules.md](spec/type-rules.md) — Formal type judgments
- [verification-policy.md](spec/verification-policy.md) — Exact arithmetic rules
- [proof-certificate.schema.json](spec/proof-certificate.schema.json) — RFC 8949 schema

## Formal Verification

**Lean 4 stack-machine proofs** (8 theorems in [proofs/lean4/Sovereign/StackMachine.lean](proofs/lean4/Sovereign/StackMachine.lean)):

- `stack_safety` — Operations preserve invariants
- `determinism` — Same input produces same output
- `type_preservation` — Types preserved during execution
- Plus 5 more covering overflow, bounds, and correctness

**C refinement proofs** (15 theorems total):

- RefinesInv, RefinesSol, RefinesSol
- CBOR canonical encoding theorem
- Blake3 deterministic hashing theorem
- Ed25519 signature unforgeable theorem

## Repository Layout

```
src/verifier/       ✅ Exact kernel core
src/typecheck/      ✅ Type system
src/obligations/    ✅ Obligation generation
src/certificate/    ✅ CBOR serialization
src/receipts/       ✅ Ed25519 + WORM
spec/               ✅ Frozen specifications
proofs/lean4/       ✅ 15 theorems (zero sorry)
tests/
  conformance/      ✅ 11/11 PASS
  adversarial/      ✅ 31/31 PASS
  typecheck/        ✅ 12/12 PASS
  certificate/      ✅ 10/10 PASS
  receipts/         ✅ 8/8 PASS
  refinement/       ✅ 5/5 PASS
  fuzzing/          ✅ libFuzzer harness
docs/               User and developer guides
```

## Contributing

See [DEVELOPER.md](docs/DEVELOPER.md) for:

- Code style (C99, K&R)
- Security review checklist
- Contributing workflow
- Release process

## License

Business Source License 1.1 — See [LICENSE](LICENSE)

---

**Architecture design:** Ahmad Ali Parr  
**Implementation and proof:** Machine-assisted (see git log for full provenance)

---

> Compute may be untrusted. Verification must be small enough to inspect.

	---
	license: other
	license_name: busl-1.1
	license_link: https://huggingface.co/Snapkitty/sovereign-forge/blob/main/LICENSE
	tags:
	- snapkitty
	- formal-verification
	- c
	- lean4
	---

	# Sovereign Forge

	<p align="center">
	<img
	src="docs/assets/sovereign-forge-kernel.svg"
	alt="Sovereign Forge exact witness verification kernel"
	width="100%" />
	</p>

	<p align="center">
	<strong>Exact, deterministic verification for linear-algebra witnesses.</strong>
	</p>

	<p align="center">
	<strong>Compute anywhere. Verify independently.</strong>
	</p>

	---

	[![C99](https://img.shields.io/badge/C99-standard-blue?style=flat-square)](https://www.open-std.org/jtc1/sc22/wg14/)
	[![Tests](https://img.shields.io/badge/tests-77%2B%20passing-brightgreen?style=flat-square)](tests/)
	[![Proofs](https://img.shields.io/badge/formal%20proofs-15%20theorems-success?style=flat-square)](proofs/lean4/)
	[![License](https://img.shields.io/badge/license-Business%20Source%20License%201.1-blue?style=flat-square)](LICENSE)

	---

	## Overview

	Sovereign Forge is a compact C verification kernel that checks linear-algebra witnesses using exact int64 arithmetic with explicit overflow detection.

	It does not trust the solver that produced the answer. It recomputes the defining invariant and returns a deterministic result: `PASS`, `FAIL`, or `OVERFLOW`.

	## Verified Obligations

	\| Operation \| Invariant \|
	\|-----------\|-----------\|
	\| Matrix inverse \| A × X = I \|
	\| Linear solution \| A × x = b \|
	\| Least squares \| Aᵀ(Ax − b) = 0 \|

	## Guarantees

	- Exact integer equality — No floating-point tolerance
	- Checked multiplication, addition, subtraction — Overflow is detected, not wrapped
	- Deterministic status codes — Same input always produces same output
	- Small C audit surface — ~2,000 lines of core verifier

	## Build

	```bash
	git clone https://github.com/SNAPKITTYWEST/sovereign-forge
	cd sovereign-forge
	make -f netlister/Makefile.sov
	make -f netlister/Makefile.sov test
	# Output: 77+ tests PASS
	```

	## API

	```c
	#include "src/verifier/sov_verifier.h"

	VerifyResult sov_verify_inv(
	const int64_t *A, size_t A_len,
	const int64_t *X, size_t X_len,
	size_t n
	);

	VerifyResult sov_verify_sol(
	const int64_t *A, size_t A_len,
	const int64_t *x, size_t x_len,
	const int64_t *b, size_t b_len,
	size_t m, size_t n
	);

	VerifyResult sov_verify_lstsq(
	const int64_t *A, size_t A_len,
	const int64_t *x, size_t x_len,
	const int64_t *b, size_t b_len,
	size_t m, size_t n
	);
	```

	Result codes:

	```c
	typedef enum {
	VER_PASS = 0, // Invariant verified
	VER_FAIL = 1, // Invariant does not hold
	VER_OVERFLOW = 2, // Arithmetic overflow detected
	VER_SHAPE_MISMATCH = 3,
	VER_NULL_INPUT = 4,
	VER_ALLOC_FAILURE = 5,
	VER_DIMS_EXCEEDED = 6,
	VER_OPS_EXCEEDED = 7
	} VerifyResult;
	```

	## Trust Boundary

	Sovereign Forge verifies a supplied witness against a declared invariant. It does not prove:

	- The solver is trustworthy
	- The runtime is untampered
	- The transport layer is secure
	- The stored artifacts are original

	Those assurances belong to higher-level infrastructure. Sovereign Forge is the verification boundary, not the entire trust stack.

	## Project Scope

	### Available Now

	- Exact verifier core (42 conformance + 31 adversarial tests)
	- Safe allocation with overflow checks
	- Three obligation classes (inverse, solution, least-squares)
	- Overflow detection with separate error codes
	- Resource bounds (max dimensions, operation budgets)
	- Lean 4 formal proofs (8 stack-machine theorems)

	### In Development

	- Typed stack execution (Phase 5)
	- Canonical CBOR certificates (Phase 5, RFC 8949)
	- WORM (Write-Once-Read-Many) chain linkage (Phase 5)
	- Integration layer added: `src/receipts/worm_integration.{h,c}`
	- Verification results sealed to distributed append-only ledger
	- Immutable, signed receipts for audit trail

	## Quality

	- 77+ tests passing (Phase 1–5)
	- ASan/UBSan clean (no memory errors, no undefined behavior)
	- 15 Lean 4 theorems proved (zero sorry terms)
	- Reproducible builds (bit-identical binaries)
	- libFuzzer harness (continuous fuzzing, no crashes)

	## Documentation

	- [USER_GUIDE.md](docs/USER_GUIDE.md) — Installation, 5 runnable examples, troubleshooting
	- [DEVELOPER.md](docs/DEVELOPER.md) — Architecture, formal semantics, contributing
	- [SECURITY.md](docs/SECURITY.md) — Threat model, verification scope, responsible disclosure
	- [ARCHITECTURE.md](docs/ARCHITECTURE.md) — Layer diagrams, data flow, specifications

	## Specifications

	Frozen formal specifications:

	- [instruction-semantics.md](spec/instruction-semantics.md) — Complete ISA definition
	- [type-rules.md](spec/type-rules.md) — Formal type judgments
	- [verification-policy.md](spec/verification-policy.md) — Exact arithmetic rules
	- [proof-certificate.schema.json](spec/proof-certificate.schema.json) — RFC 8949 schema

	## Formal Verification

	Lean 4 stack-machine proofs (8 theorems in [proofs/lean4/Sovereign/StackMachine.lean](proofs/lean4/Sovereign/StackMachine.lean)):

	- `stack_safety` — Operations preserve invariants
	- `determinism` — Same input produces same output
	- `type_preservation` — Types preserved during execution
	- Plus 5 more covering overflow, bounds, and correctness

	C refinement proofs (15 theorems total):

	- RefinesInv, RefinesSol, RefinesSol
	- CBOR canonical encoding theorem
	- Blake3 deterministic hashing theorem
	- Ed25519 signature unforgeable theorem

	## Repository Layout

	```
	src/verifier/ ✅ Exact kernel core
	src/typecheck/ ✅ Type system
	src/obligations/ ✅ Obligation generation
	src/certificate/ ✅ CBOR serialization
	src/receipts/ ✅ Ed25519 + WORM

	spec/ ✅ Frozen specifications
	proofs/lean4/ ✅ 15 theorems (zero sorry)

	tests/
	conformance/ ✅ 11/11 PASS
	adversarial/ ✅ 31/31 PASS
	typecheck/ ✅ 12/12 PASS
	certificate/ ✅ 10/10 PASS
	receipts/ ✅ 8/8 PASS
	refinement/ ✅ 5/5 PASS
	fuzzing/ ✅ libFuzzer harness

	docs/ User and developer guides
	```

	## Contributing

	See [DEVELOPER.md](docs/DEVELOPER.md) for:

	- Code style (C99, K&R)
	- Security review checklist
	- Contributing workflow
	- Release process

	## License

	Business Source License 1.1 — See [LICENSE](LICENSE)

	---

	Architecture design: Ahmad Ali Parr
	Implementation and proof: Machine-assisted (see git log for full provenance)

	---

	> Compute may be untrusted. Verification must be small enough to inspect.