verified-spec-code-mapper

Verified Spec-Code Mapper

Overview

Establish explicit, evidence-based traceability between formal specifications and verified code components. Generate structured reports that map each specification to its implementation and correctness proofs, supporting verification auditing, documentation, and reproducibility.

Mapping Workflow

Step 1: Identify Specifications

Locate all formal specifications in the codebase:

1. Preconditions:
2. Coq: forall ... -> P -> ... (hypothesis before conclusion)
3. Dafny: requires clauses
4. Isabelle: assumes clauses
5. Look for: Input constraints, safety conditions

1. Postconditions:
2. Coq: ... -> Q (conclusion of theorem)
3. Dafny: ensures clauses
4. Isabelle: shows clauses
5. Look for: Output guarantees, correctness properties

1. Loop Invariants:
2. Dafny: invariant clauses in loops
3. Coq: Lemmas about recursive functions
4. Look for: Properties maintained across iterations

1. Class/Type Invariants:
2. Dafny: predicate Valid() methods
3. Coq: Well-formedness predicates
4. Look for: Structural constraints, consistency properties

1. Functional Correctness:
2. Theorems stating what function computes
3. Equivalence to specification
4. Look for: Correctness lemmas, specification theorems

Step 2: Map to Code Components

For each specification, identify corresponding code:

1. Direct mapping:
2. Specification mentions function/method name
3. Theorem statement references definition
4. Example: Lemma factorial_positive : forall n, factorial n >= 1

→ Maps to factorial function

1. Contextual mapping:
2. Specification in same file/module
3. Comments linking spec to code
4. Naming conventions (e.g., sort_correct → sort)

1. Structural mapping:
2. Preconditions → Function parameters
3. Postconditions → Return values
4. Invariants → Loop bodies or class fields

1. Record locations:
2. File path
3. Line numbers
4. Function/method/class names

Step 3: Identify Verification Evidence

For each specification-code mapping, find proof evidence:

1. Complete proofs:
2. Coq: Ends with Qed
3. Dafny: Verified by Dafny verifier (no errors)
4. Isabelle: Ends with done or qed
5. Status: ✓ Fully Verified

1. Incomplete proofs:
2. Coq: Ends with Admitted
3. Isabelle: Contains sorry
4. Status: ✗ Unverified

1. Assumed axioms:
2. Coq: Axiom declarations
3. Isabelle: axiomatization
4. Status: ⚠ Assumed (no proof)

1. External verification:
2. SMT solver verification
3. Automated tool checks
4. Status: ✓ Verified (by tool)

1. Record evidence:
2. Theorem/lemma name
3. Proof location
4. Proof method
5. Dependencies (lemmas, axioms used)

Step 4: Analyze Coverage

Determine verification completeness:

1. Specification coverage:

`` Coverage = (Verified Specs / Total Specs) × 100% ``

1. Code coverage:

`` Coverage = (Verified Functions / Total Functions) × 100% ``

1. Proof completeness:

`` Completeness = (Complete Proofs / Total Proofs) × 100% ``

1. Categorize status:
2. ✓ Fully Verified: All specs proved, no assumptions
3. ⚠ Partially Verified: Some specs proved, some assumed
4. ✗ Unverified: No formal verification

1. Identify gaps:
2. Unverified specifications
3. Incomplete proofs
4. Missing specifications
5. Assumed axioms

Step 5: Generate Report

Produce structured Markdown report:

1. Choose report type:
2. Function-centric: One function per section
3. Specification-centric: One spec per section
4. Module-level: Overview of entire module

1. Include required sections:
2. Specification statements (formal)
3. Code component references (with locations)
4. Verification evidence (proofs, theorems)
5. Coverage summary
6. Assumptions and gaps

1. Use clear status indicators:
2. ✓ Fully Verified
3. ⚠ Partially Verified (with assumptions)
4. ✗ Unverified

1. Provide traceability:
2. Link specs to code
3. Link code to proofs
4. Show dependency chains

Mapping Patterns

For detailed patterns and templates, see [mapping_patterns.md](references/mapping_patterns.md).

Quick Reference

| Specification Type | Typical Location | Verification Evidence | |-------------------|------------------|----------------------| | Precondition | requires, hypothesis | Checked by verifier or proved | | Postcondition | ensures, conclusion | Theorem proving property | | Loop Invariant | invariant, lemma | Induction proof | | Class Invariant | predicate Valid() | Maintained by all methods | | Functional Correctness | Theorem statement | Complete proof |

Examples

Example 1: Simple Function Mapping (Coq)

Input Code:

Definition divide (n m : nat) : option nat :=
  if m =? 0 then None else Some (n / m).

Lemma divide_safe : forall n m : nat,
  m <> 0 -> exists q, divide n m = Some q.
Proof.
  intros n m Hm.
  unfold divide.
  destruct (m =? 0) eqn:E.
  - apply Nat.eqb_eq in E. contradiction.
  - exists (n / m). reflexivity.
Qed.

Generated Report:

# Verification Report: divide

## Function Signature

Definition divide (n m : nat) : option nat

## Specifications

### Precondition: Non-zero Divisor
- **Specification:** `m <> 0`
- **Location:** divide.v:4 (lemma hypothesis)
- **Status:** ✓ Fully Verified

### Postcondition: Returns Quotient
- **Specification:** `exists q, divide n m = Some q`
- **Location:** divide.v:4 (lemma conclusion)
- **Status:** ✓ Fully Verified

## Verification Evidence

### Theorem: divide_safe
- **Statement:** `forall n m, m <> 0 -> exists q, divide n m = Some q`
- **Location:** divide.v:4-10
- **Proof Status:** ✓ Complete (ends with Qed)
- **Proof Method:** Case analysis on `m =? 0`
- **Dependencies:** None

## Coverage Summary
- Specifications: 2 total, 2 verified (100%)
- Status: ✓ Fully Verified

Example 2: Class with Invariants (Dafny)

Input Code:

class BankAccount {
  var balance: int

  predicate Valid()
    reads this
  {
    balance >= 0
  }

  constructor(initial: int)
    requires initial >= 0
    ensures Valid()
    ensures balance == initial
  {
    balance := initial;
  }

  method Deposit(amount: int)
    requires Valid()
    requires amount >= 0
    modifies this
    ensures Valid()
    ensures balance == old(balance) + amount
  {
    balance := balance + amount;
  }
}

Generated Report:

# Verification Report: BankAccount

## Class Invariant

### Invariant: Non-negative Balance
- **Specification:** `balance >= 0`
- **Location:** BankAccount.dfy:5 (Valid predicate)
- **Status:** ✓ Fully Verified

## Method: constructor

### Specifications
1. **Precondition: Non-negative Initial**
   - Specification: `requires initial >= 0`
   - Location: BankAccount.dfy:10
   - Status: ✓ Verified by Dafny

2. **Postcondition: Establishes Invariant**
   - Specification: `ensures Valid()`
   - Location: BankAccount.dfy:11
   - Status: ✓ Verified by Dafny

3. **Postcondition: Correct Balance**
   - Specification: `ensures balance == initial`
   - Location: BankAccount.dfy:12
   - Status: ✓ Verified by Dafny

## Method: Deposit

### Specifications
1. **Precondition: Valid State**
   - Specification: `requires Valid()`
   - Location: BankAccount.dfy:18
   - Status: ✓ Verified by Dafny

2. **Precondition: Non-negative Amount**
   - Specification: `requires amount >= 0`
   - Location: BankAccount.dfy:19
   - Status: ✓ Verified by Dafny

3. **Postcondition: Maintains Invariant**
   - Specification: `ensures Valid()`
   - Location: BankAccount.dfy:21
   - Status: ✓ Verified by Dafny

4. **Postcondition: Correct Balance Update**
   - Specification: `ensures balance == old(balance) + amount`
   - Location: BankAccount.dfy:22
   - Status: ✓ Verified by Dafny

## Coverage Summary
- Total Specifications: 7
- Fully Verified: