Metadata-Version: 2.4
Name: flux-certify
Version: 0.1.0
Summary: Compile FLUX-C guard constraints and generate proof certificates
Home-page: https://github.com/SuperInstance/flux-certify
Author: SuperInstance
Author-email: cocapn@example.com
Classifier: Development Status :: 3 - Alpha
Classifier: Intended Audience :: Developers
Classifier: Topic :: Software Development :: Compilers
Classifier: License :: OSI Approved :: Apache Software License
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.8
Classifier: Programming Language :: Python :: 3.9
Classifier: Programming Language :: Python :: 3.10
Classifier: Programming Language :: Python :: 3.11
Requires-Python: >=3.8
Description-Content-Type: text/markdown
Requires-Dist: click>=8.0
Dynamic: author
Dynamic: author-email
Dynamic: classifier
Dynamic: description
Dynamic: description-content-type
Dynamic: home-page
Dynamic: requires-dist
Dynamic: requires-python
Dynamic: summary

# FLUX Certify

Compile FLUX-C guard constraints and generate proof certificates for safety-critical systems.

## Overview

FLUX Certify is a Python package + CLI tool for compiling `.guard` constraint specifications into FLUX-C bytecode and generating proof certificates. Designed for safety-critical deployment in aerospace, automotive, marine, and medical domains.

## Installation

```bash
pip install flux-certify
```

## CLI Usage

```bash
# Compile a guard constraint to FLUX-C bytecode
flux-certify compile "battery_temp in [15, 55] with priority HIGH"

# Generate a proof certificate
flux-certify prove "battery_temp in [15, 55]"

# Generate a signed certificate
flux-certify certify "sonar_frequency in [10, 50]"

# Verify a certificate file
flux-certify verify /path/to/certificate.json

# Show example constraints
flux-certify examples

# Generate signing keys
flux-certify keygen

# Check constraint certification status
flux-certify status "deceleration in [0.1, 0.8]"
```

## Python API

```python
from flux_certify import compile_guard, prove_guard, certify, verify_cert

# Compile
result = compile_guard("battery_temp in [15, 55]")
print(result['asm'])
print(result['guard_hash'])

# Prove
cert = prove_guard("battery_temp in [15, 55]")
print(cert['task_id'])
print(cert['theorem_status'])  # [PROVEN]

# Sign and verify
signed = certify("battery_temp in [15, 55]", signer="my-fleet")
print(verify_cert(signed))  # True
```

## FLUX-C Assembly Format

Each guard constraint compiles to a sequence of FLUX-C opcodes:

```
; FLUX-C Guard Assembly
; Constraint: battery_temp in [15, 55]
LOAD_IMM  r0, 0xBD16E340  ; battery_temp
LOAD_IMM  r1, 0xBD16E341  ; in
LOAD_IMM  r2, 0xBD16E342  ; 15
LOAD_IMM  r3, 0xBD16E343  ; 55
LOAD_IMM  r0, 0xBD16E344  ; with
LOAD_IMM  r1, 0xBD16E345  ; priority
LOAD_IMM  r2, 0xBD16E346  ; HIGH
VERIFY_GUARD                  ; verify constraint
HALT                          ; end
```

## Proof Certificate Structure

```json
{
  "task_id": "uuid-here",
  "constraint": "battery_temp in [15, 55]",
  "guard_hash": "0xBD16E340",
  "verified": true,
  "prover": "FLUX-Certify-0.1.0",
  "proof_type": "constraint_compilation",
  "flux_c_version": "1.0",
  "theorem": "fluxc_terminates",
  "theorem_status": "[PROVEN]",
  "theorem_description": "All FLUX-C programs halt structurally. No backward jumps, bounded call stack (MAX_STACK=100)."
}
```

## Theoretical Foundation

### FLUX-C Turing-Incompleteness Theorem [PROVEN]

**Theorem:** All FLUX-C programs halt in bounded time.

**Proof sketch:**
1. All control-flow opcodes are forward-only (no backward jumps)
2. Call stack is bounded by hardware MAX_STACK=100
3. Therefore no infinite loops, no unbounded recursion
4. Every execution path is finite

This is the foundation for formal verification of FLUX-C programs in safety-critical systems.

**Theorem status:** `[PROVEN]` — mechanized in Coq (flux-certify/FluxC/FluxC.v)

### Key Invariants

| Invariant | Status |
|-----------|--------|
| fluxc_terminates | [PROVEN] |
| fluxc_forward_only | [PROVEN] |
| fluxc_halts_structurally | [PROVEN] |
| MAX_STACK bounded | [PROVEN] |

## License

Apache 2.0

## Links

- GitHub: https://github.com/SuperInstance/flux-certify
- FLUX-C ISA: https://github.com/SuperInstance/flux-research
- Dissertation: https://github.com/SuperInstance/flux-research/tree/main/dissertation
