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

**Repo Path**: `/var/mnt/eclipse/repos/conflow`
**Tier**: T2 — High
**Total Theorems**: 4
**Primary Prover(s)**: Lean4 (2), Idris2 (2)
**Existing Proof Coverage**: property_test.rs only (no formal proofs)

## Status Tracker

| # | Theorem | Prover | Status | Verified |
|---|---------|--------|--------|----------|
| 1 | CF1 DAG acyclicity preservation | L4 | [ ] Pending | — |
| 2 | CF2 Topological execution order | L4 | [ ] Pending | — |
| 3 | CF3 BLAKE3 cache immutability | I2 | [ ] Pending | — |
| 4 | CF4 Executor isolation (no escape) | I2 | [ ] Pending | — |

## Context

CUE/Nickel configuration orchestrator. DAG-based stages, content-addressed caching (BLAKE3), RSR compliance.

### Key files
- `src/pipeline/dag.rs` (petgraph)
- `src/pipeline/executor.rs`
- `src/cache/filesystem.rs`
- `src/executors/cue.rs`
- `src/rsr/compliance.rs`

## Theorems to Prove

### CF1: DAG acyclicity

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

**Statement**: Adding a stage never creates a cycle.

**Obligations**:
- [ ] Model DAG as reflexive-antisymmetric-transitive relation
- [ ] Prove add_stage preserves acyclicity

---

### CF2: Topological execution order

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

**Statement**: Stage dependencies execute before dependents.

**Obligations**:
- [ ] Define topological sort
- [ ] Prove ordering

---

### CF3: BLAKE3 cache immutability

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

**Statement**: Once written, cache entries never modified.

**Obligations**:
- [ ] Model content-addressed store
- [ ] Prove append-only

---

### CF4: Executor isolation

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

**Statement**: Tool output confined to working directory.

**Obligations**:
- [ ] Model filesystem boundaries
- [ ] Prove no escape

---

## Verification Commands

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

## Handoff Checklist

- [ ] All 4 theorems proven
- [ ] Commit: `proof: complete conflow proofs (4/4)`
