# Coq Proof Development Workflow

This document describes how to work with Coq proofs for C program verification using Frama-C/ACSL.

## Critical Understanding: File Generation vs. Prover Invocation

**IMPORTANT**: The prove script does two separate things:
1. **Frama-C WP plugin generates .v files for ALL goals** (both successful and failed ones)
2. **Frama-C only invokes Coq prover on goals that automated provers failed to solve**

This means:
- ✅ **Successful Alt-Ergo goals**: Have .v files with empty proofs ready for manual development
- ❌ **Failed goals**: Have .v files and Coq was actually invoked (may show in JSON/logs)

## Quick Start Workflow

### 1. Run the Proof Script
```bash
./scripts/prove.pl src/progname.c
```

### 2. Identify Goals Needing Interactive Proofs
Look at "Failed goals" in script output:
```
Failed goals:
  Lemma 'GoalName1': Timeout (Alt-Ergo 2.6.2)
  Lemma 'GoalName2': Timeout (Alt-Ergo 2.6.2)
```

### 3. Find and Edit .v Files
- **Location**: `proof/progname/wp/interactive/lemma_GoalName.v`
- **Edit between**: `Proof.` and `Qed.`
- **Start simple**: Try `exact Q_AxiomName.` first

### 4. Test and Verify
- **Re-run**: `./scripts/prove.pl src/progname.c`
- **Check JSON**: `"success": 1` and `"passed": true` in `build/progname/results/results.json`

## Understanding Results

### Script Output Interpretation
- **Goals proved**: `27/31 proved` (example)
- **Status**: `SUCCESS` or `FAILURE`
- **Prover performance**: Only lists successful provers (Coq missing = all attempts failed)

### JSON Analysis - Understanding Coq Invocation
**Failed goal needing work**:
```json
{ "goal": "typed_lemma_FailedGoal", "passed": false, "verdict": "timeout",
  "provers": [
    { "prover": "qed", "time": 0.000794, "success": 0 },
    { "prover": "Alt-Ergo:2.6.2", "time": 0, "success": 0 }
    // ← No Coq entry = Coq returned "Unknown" immediately
  ] }
```

**Successful goal (no work needed)**:
```json
{ "goal": "typed_lemma_SuccessfulGoal", "passed": true, "verdict": "valid",
  "provers": [
    { "prover": "qed", "time": 0, "success": 0 },
    { "prover": "Alt-Ergo:2.6.2", "time": 0.0375, "success": 1 }
    // ← No Coq entry = Coq was never invoked
  ] }
```

## Proof Development Best Practices

### LLM-Friendly Development Process
1. **Start with failed goals from script output** - Don't guess which proofs to work on
2. **Start simple** - Try `exact axiom_name.` or `apply axiom_name.` first
3. **Test immediately** - Run prove script after each attempt
4. **Read timing carefully**:
   - `0ms` = Syntax error or immediate failure
   - `>0ms` = Coq processed but found logical issues
5. **Use incremental development** - Add one tactic at a time

### Debugging Strategy
- **0ms time**: Check syntax, tactics, axiom names
- **>0ms time**: Check theorem statement, axiom parameters, goal structure
- **Use frama.log**: Get exact goal statements and assumptions (`build/progname/results/frama.log`)
- **Match variables exactly**: Copy from theorem, don't guess

## Quick Reference

### Essential Commands
```bash
# Run proofs
./scripts/prove.pl src/progname.c

# Find failed goals
grep -A 3 '"passed": false' build/progname/results/results.json

# View detailed goals
less build/progname/results/frama.log
```

### Success Indicators
- **JSON**: `"success": 1`, `"passed": true`, `"verdict": "valid"`
- **Time**: `>0ms` (Coq processed the proof)

### Environment Constraints
- ❌ Cannot run `coqc` directly (missing BuiltIn library)
- ❌ No interactive Coq session available
- ✅ Must use prove script for validation
- ✅ Edit .v files directly and test with prove script