# Proof Spec: januskey
<!-- SPDX-License-Identifier: CC-BY-SA-4.0 -->

**Repo Path**: `/var/mnt/eclipse/repos/januskey`
**Tier**: T1 — Critical
**Total Theorems**: 5
**Primary Prover(s)**: Idris2 (3), Lean4 (1), TLA+ (1)
**Existing Proof Coverage**: 7 .idr ABI files (types/layout); formal proofs pending
**Dependencies**: `proven`

## Status Tracker

| # | Theorem | Prover | Status | Verified |
|---|---------|--------|--------|----------|
| 1 | JK1 Operation invertibility (perfect reversal) | I2 | [ ] Pending | — |
| 2 | JK2 Transaction atomicity (all-or-nothing) | TLA | [ ] Pending | — |
| 3 | JK3 Content-addressed integrity (SHA256) | L4 | [ ] Pending | — |
| 4 | JK4 Append-only log (no deletion) | I2 | [ ] Pending | — |
| 5 | JK5 Cryptographic attestation soundness | I2 | [ ] Pending | — |

## Context

Reversible file operations via Maximal Principle Reduction (MPR). 100% reversibility: every operation stores inverse metadata. Delete stores full content, Modify stores original hash, Move stores original path. SHA256 content-addressed storage, append-only operation log.

### Key files
- `src/januskey/src/operations.rs` (19.9K) — operation inversion logic
- `src/januskey/src/transaction.rs` (12.5K) — atomicity + rollback
- `src/januskey/src/content_store.rs` (6.9K) — SHA256 addressing
- `src/januskey/src/attestation.rs` (17.2K) — cryptographic proof

## Theorems to Prove

### JK1: Operation invertibility

**Target file**: `verification/proofs/idris2/Invertibility.idr`
**Source**: `src/januskey/src/operations.rs`
**Priority**: P0

**Statement**:
> For every operation op and state s, `invert(op)(op(s)) = s`. Every operation has a unique inverse.

**Formal signature**:
```idris
data Op = Delete String | Modify String | Move String String | Create String

apply : Op -> State -> State
invert : Op -> Op
invertCorrect : (op : Op) -> (s : State) -> apply (invert op) (apply op s) = s
```

**Obligations**:
- [ ] Define Op + State
- [ ] Define invert for all 4 op types
- [ ] Prove invertCorrect for each

---

### JK2: Transaction atomicity

**Target file**: `verification/proofs/tlaplus/JKAtomicity.tla`
**Priority**: P0

**Statement**:
> Either all operations in a transaction commit, or none. No partial commits.

**Obligations**:
- [ ] Model transaction with list of ops
- [ ] Model-check atomicity invariant

---

### JK3: Content-addressed integrity

**Target file**: `verification/proofs/lean4/ContentAddress.lean`
**Priority**: P0

**Statement**:
> For any content c stored with key k, `sha256(c) = k`. Content store is a valid hash-addressed structure.

**Obligations**:
- [ ] Model content store as (hash, content) pairs
- [ ] Prove hash(get(k)) = k for all keys

---

### JK4: Append-only log

**Target file**: `verification/proofs/idris2/AppendOnly.idr`
**Priority**: P1

**Statement**:
> Operation log has no delete, overwrite, or reorder operations. Strictly append-only.

**Obligations**:
- [ ] Model log as inductive list with only Cons operation
- [ ] Prove no operation removes entries

---

### JK5: Cryptographic attestation soundness

**Target file**: `verification/proofs/idris2/Attestation.idr`
**Source**: `src/januskey/src/attestation.rs`
**Priority**: P2

**Statement**:
> Attestation signature is valid iff the attested operation actually occurred.

**Obligations**:
- [ ] Model attestation as signed tuple
- [ ] Prove verification requires correct private key

---

## Verification Commands

```bash
cd /var/mnt/eclipse/repos/januskey
just proof-check-all
```

## Handoff Checklist

- [ ] All 5 theorems proven
- [ ] Commit: `proof: complete januskey proofs (5/5 theorems)`
