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:

• Coq: forall ... -> P -> ... (hypothesis before conclusion)
• Dafny: requires clauses
• Isabelle: assumes clauses
• Look for: Input constraints, safety conditions

1. Postconditions:

• Coq: ... -> Q (conclusion of theorem)
• Dafny: ensures clauses
• Isabelle: shows clauses
• Look for: Output guarantees, correctness properties

1. Loop Invariants:

• Dafny: invariant clauses in loops
• Coq: Lemmas about recursive functions
• Look for: Properties maintained across iterations

1. Class/Type Invariants:

• Dafny: predicate Valid() methods
• Coq: Well-formedness predicates
• Look for: Structural constraints, consistency properties

1. Functional Correctness:

• Theorems stating what function computes
• Equivalence to specification
• Look for: Correctness lemmas, specification theorems

Step 2: Map to Code Components

For each specification, identify corresponding code:

1. Direct mapping:

• Specification mentions function/method name
• Theorem statement references definition
• Example: Lemma factorial_positive : forall n, factorial n >= 1

→ Maps to factorial function

1. Contextual mapping:

• Specification in same file/module
• Comments linking spec to code
• Naming conventions (e.g., sort_correct → sort)

1. Structural mapping:

• Preconditions → Function parameters
• Postconditions → Return values
• Invariants → Loop bodies or class fields

1. Record locations:

• File path
• Line numbers
• Function/method/class names

Step 3: Identify Verification Evidence

For each specification-code mapping, find proof evidence:

1. Complete proofs:

• Coq: Ends with Qed
• Dafny: Verified by Dafny verifier (no errors)
• Isabelle: Ends with done or qed
• Status: ✓ Fully Verified

1. Incomplete proofs:

• Coq: Ends with Admitted
• Isabelle: Contains sorry
• Status: ✗ Unverified

1. Assumed axioms:

• Coq: Axiom declarations
• Isabelle: axiomatization
• Status: ⚠ Assumed (no proof)

1. External verification:

• SMT solver verification
• Automated tool checks
• Status: ✓ Verified (by tool)

1. Record evidence:

• Theorem/lemma name
• Proof location
• Proof method
• 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:

• ✓ Fully Verified: All specs proved, no assumptions
• ⚠ Partially Verified: Some specs proved, some assumed
• ✗ Unverified: No formal verification

1. Identify gaps:

• Unverified specifications
• Incomplete proofs
• Missing specifications
• Assumed axioms

Step 5: Generate Report

Produce structured Markdown report:

1. Choose report type:

• Function-centric: One function per section
• Specification-centric: One spec per section
• Module-level: Overview of entire module

1. Include required sections:

• Specification statements (formal)
• Code component references (with locations)
• Verification evidence (proofs, theorems)
• Coverage summary
• Assumptions and gaps

1. Use clear status indicators:

• ✓ Fully Verified
• ⚠ Partially Verified (with assumptions)
• ✗ Unverified

1. Provide traceability:

• Link specs to code
• Link code to proofs
• Show dependency chains

Mapping Patterns

For detailed patterns and templates, see mapping_patterns.md.

Quick Reference

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: 7 (100%)
- Status: ✓ Fully Verified
- Verification Method: Dafny automatic verifier

Example 3: Module with Assumptions (Coq)

Input Code:

Require Import FunctionalExtensionality.

Definition compose {A B C : Type} (g : B -> C) (f : A -> B) : A -> C :=
  fun x => g (f x).

Lemma compose_assoc : forall (A B C D : Type)
  (f : A -> B) (g : B -> C) (h : C -> D),
  compose h (compose g f) = compose (compose h g) f.
Proof.
  intros.
  apply functional_extensionality.
  intro x. reflexivity.
Qed.

Generated Report:

# Verification Report: compose

## Function Signature

Definition compose {A B C : Type} (g : B -> C) (f : A -> B) : A -> C

## Specifications

### Functional Correctness: Associativity
- **Specification:** `compose h (compose g f) = compose (compose h g) f`
- **Location:** compose.v:6-8
- **Status:** ⚠ Verified with Assumptions

## Verification Evidence

### Theorem: compose_assoc
- **Statement:** Composition is associative
- **Location:** compose.v:6-13
- **Proof Status:** ✓ Complete (ends with Qed)
- **Proof Method:** Functional extensionality + reflexivity
- **Dependencies:**
  - ⚠ **Axiom:** `functional_extensionality` (assumed)

## Assumptions

### Axiom: functional_extensionality
- **Statement:** `forall (A B : Type) (f g : A -> B), (forall x, f x = g x) -> f = g`
- **Source:** Coq standard library
- **Justification:** Standard axiom for function equality
- **Used in:** compose_assoc
- **Impact:** Widely accepted axiom, consistent with Coq's logic

## Coverage Summary
- Specifications: 1 total, 1 verified (100%)
- Status: ⚠ Partially Verified (relies on standard axiom)
- Confidence: High (standard axiom)

Example 4: Traceability Matrix

Generated Report:

# Verification Traceability Matrix: Sorting Module

| Spec ID | Specification | Code Component | Proof/Theorem | Status |
|---------|---------------|----------------|---------------|--------|
| SORT-001 | Permutation preservation | `sort` (sort.v:15) | `sort_permutes` (sort.v:45) | ✓ |
| SORT-002 | Output is sorted | `sort` (sort.v:15) | `sort_sorted` (sort.v:62) | ✓ |
| SORT-003 | Combined correctness | `sort` (sort.v:15) | `sort_correct` (sort.v:78) | ✓ |
| SORT-004 | Stability (equal elements) | `sort` (sort.v:15) | - | ✗ |
| SORT-005 | Time complexity O(n log n) | `sort` (sort.v:15) | - | ✗ |

## Summary
- Total Specifications: 5
- Fully Verified: 3 (60%)
- Unverified: 2 (40%)

## Verification Gaps

### SORT-004: Stability
- **Status:** ✗ Unverified
- **Reason:** Stability not formally specified or proved
- **Impact:** Cannot guarantee order of equal elements
- **Priority:** Medium

### SORT-005: Time Complexity
- **Status:** ✗ Unverified
- **Reason:** Complexity analysis not formalized
- **Impact:** Performance guarantees not verified
- **Priority:** Low (functional correctness verified)

Constraints and Requirements

MUST Requirements

1. Evidence-based mapping:

• Only map specifications with explicit proof evidence
• Do not infer mappings without verification
• Clearly mark assumptions and axioms

1. Preserve specification integrity:

• Report complete specifications (don't drop preconditions)
• Don't merge distinct specifications
• Don't weaken specifications

1. Honest status reporting:

• ✓ Only for fully verified (complete proofs, no assumptions)
• ⚠ For verified with assumptions/axioms
• ✗ For unverified or incomplete

1. Clear distinction:

• Separate verified from assumed
• Distinguish complete from incomplete proofs
• Mark external verification (SMT, automated tools)

MUST NOT Requirements

1. Do not infer:

• Don't assume specifications are verified without proof
• Don't guess at verification status
• Don't create mappings without evidence

1. Do not merge:

• Keep specifications separate
• Don't combine preconditions and postconditions
• Maintain granularity

1. Do not weaken:

• Report full specifications
• Include all preconditions
• Don't simplify for convenience

Best Practices

1. Be explicit: Include file paths, line numbers, exact statements
2. Be honest: Report verification status accurately
3. Be complete: Document all assumptions and dependencies
4. Be structured: Use consistent report format
5. Be traceable: Link specs → code → proofs clearly
6. Be auditable: Provide enough detail for independent verification

Report Format Guidelines

Required Sections

1. Specification Statement: Formal specification (exact syntax)
2. Code Component: Function/method name and location
3. Verification Evidence: Theorem/proof name and status
4. Coverage Summary: Statistics and overall status
5. Assumptions: Any axioms or assumptions used
6. Gaps: Unverified specifications or incomplete proofs

Status Indicators

• ✓ Fully Verified: Complete proof, no assumptions
• ⚠ Partially Verified: Proof with assumptions/axioms
• ✗ Unverified: No proof or incomplete proof

Location Format

• File: filename.ext
• Line: filename.ext:line
• Range: filename.ext:start-end

Resources

• Mapping patterns: See mapping_patterns.md for comprehensive patterns and templates
• Coq documentation: https://coq.inria.fr/documentation
• Dafny documentation: https://dafny.org/
• Isabelle documentation: https://isabelle.in.tum.de/documentation.html