begriffs open source - acsl-example/blob - CLAUDE.md

   1 # Coq Proof Development Workflow
   2
   3 This document describes how to work with Coq proofs for C program verification using Frama-C/ACSL.
   4
   5 ## Critical Understanding: File Generation vs. Prover Invocation
   6
   7 **IMPORTANT**: The prove script does two separate things:
   8 1. **Frama-C WP plugin generates .v files for ALL goals** (both successful and failed ones)
   9 2. **Frama-C only invokes Coq prover on goals that automated provers failed to solve**
  10
  11 This means:
  12 - ✅ **Successful Alt-Ergo goals**: Have .v files with empty proofs ready for manual development
  13 - ❌ **Failed goals**: Have .v files and Coq was actually invoked (may show in JSON/logs)
  14
  15 ## Quick Start Workflow
  16
  17 ### 1. Run the Proof Script
  18 ```bash
  19 ./scripts/prove.pl src/progname.c
  20 ```
  21
  22 ### 2. Identify Goals Needing Interactive Proofs
  23 Look at "Failed goals" in script output:
  24 ```
  25 Failed goals:
  26   Lemma 'GoalName1': Timeout (Alt-Ergo 2.6.2)
  27   Lemma 'GoalName2': Timeout (Alt-Ergo 2.6.2)
  28 ```
  29
  30 ### 3. Find and Edit .v Files
  31 - **Location**: `proof/progname/wp/interactive/lemma_GoalName.v`
  32 - **Edit between**: `Proof.` and `Qed.`
  33 - **Start simple**: Try `exact Q_AxiomName.` first
  34
  35 ### 4. Test and Verify
  36 - **Re-run**: `./scripts/prove.pl src/progname.c`
  37 - **Check JSON**: `"success": 1` and `"passed": true` in `build/progname/results/results.json`
  38
  39 ## Understanding Results
  40
  41 ### Script Output Interpretation
  42 - **Goals proved**: `27/31 proved` (example)
  43 - **Status**: `SUCCESS` or `FAILURE`
  44 - **Prover performance**: Only lists successful provers (Coq missing = all attempts failed)
  45
  46 ### JSON Analysis - Understanding Coq Invocation
  47 **Failed goal needing work**:
  48 ```json
  49 { "goal": "typed_lemma_FailedGoal", "passed": false, "verdict": "timeout",
  50   "provers": [
  51     { "prover": "qed", "time": 0.000794, "success": 0 },
  52     { "prover": "Alt-Ergo:2.6.2", "time": 0, "success": 0 }
  53     // ← No Coq entry = Coq returned "Unknown" immediately
  54   ] }
  55 ```
  56
  57 **Successful goal (no work needed)**:
  58 ```json
  59 { "goal": "typed_lemma_SuccessfulGoal", "passed": true, "verdict": "valid",
  60   "provers": [
  61     { "prover": "qed", "time": 0, "success": 0 },
  62     { "prover": "Alt-Ergo:2.6.2", "time": 0.0375, "success": 1 }
  63     // ← No Coq entry = Coq was never invoked
  64   ] }
  65 ```
  66
  67 ## Proof Development Best Practices
  68
  69 ### LLM-Friendly Development Process
  70 1. **Start with failed goals from script output** - Don't guess which proofs to work on
  71 2. **Start simple** - Try `exact axiom_name.` or `apply axiom_name.` first
  72 3. **Test immediately** - Run prove script after each attempt
  73 4. **Read timing carefully**:
  74    - `0ms` = Syntax error or immediate failure
  75    - `>0ms` = Coq processed but found logical issues
  76 5. **Use incremental development** - Add one tactic at a time
  77
  78 ### Debugging Strategy
  79 - **0ms time**: Check syntax, tactics, axiom names
  80 - **>0ms time**: Check theorem statement, axiom parameters, goal structure
  81 - **Use frama.log**: Get exact goal statements and assumptions (`build/progname/results/frama.log`)
  82 - **Match variables exactly**: Copy from theorem, don't guess
  83
  84 ## Quick Reference
  85
  86 ### Essential Commands
  87 ```bash
  88 # Run proofs
  89 ./scripts/prove.pl src/progname.c
  90
  91 # Find failed goals
  92 grep -A 3 '"passed": false' build/progname/results/results.json
  93
  94 # View detailed goals
  95 less build/progname/results/frama.log
  96 ```
  97
  98 ### Success Indicators
  99 - **JSON**: `"success": 1`, `"passed": true`, `"verdict": "valid"`
 100 - **Time**: `>0ms` (Coq processed the proof)
 101
 102 ### Environment Constraints
 103 - ❌ Cannot run `coqc` directly (missing BuiltIn library)
 104 - ❌ No interactive Coq session available
 105 - ✅ Must use prove script for validation
 106 - ✅ Edit .v files directly and test with prove script