# CLAUDE.md

This file provides guidance to Claude Code (claude.ai/code) when working with code in this repository.

## Project Overview

This is an ACSL (ANSI/ISO C Specification Language) formal verification project demonstrating array search algorithms with varying specification complexity. The project uses Frama-C with the WP plugin for automated proof verification.

## Architecture

### Header Organization
The project uses a layered header architecture separating user-facing API from proof infrastructure:

- **`inc/types.h`** - Basic type definitions
- **`inc/algos.h`** - Public API with function declarations  
- **`inc/proof/`** - Proof infrastructure (separate from user-facing API)
  - **`existence.h`** - Element existence predicates and lemmas
  - **`search.h`** - Logic functions with comprehensive lemmas

### Selective Axiom Architecture
Each source file includes only the axioms it needs for optimal verification performance. This design achieves both elegant organization and fast verification by avoiding unnecessary axiom verification overhead.

## Build System

Uses Meson build system with custom Frama-C verification tests.

### Build Commands
```bash
meson setup build
meson compile -C build
```

### Testing Commands
```bash
# Run all verification tests
meson test -C build

# Run specific test by name
meson test -C build [test_name]

# Verbose test output (shows detailed Frama-C profiling)
meson test -C build --verbose
```

### Performance Analysis
The verbose test output provides detailed profiling information including individual proof goal timing, timeout identification, prover statistics, and total verification time. Use this for identifying performance bottlenecks.

## Verification Details

### ACSL Contracts
Functions use ACSL contracts with varying levels of abstraction - from basic behavioral contracts with inline quantifiers to abstract logic functions. The choice depends on verification performance vs specification elegance trade-offs.

### Frama-C Configuration  
Tests run with comprehensive verification flags: `-wp -wp-rte -wp-prover cvc4 -verbose 2 -wp-verbose 3 -wp-debug 1 -wp-proof-trace`

## Development Workflow

When adding new algorithms or modifying specifications:
1. Create source files with inline ACSL contracts
2. Include appropriate headers from `inc/proof/` for needed axioms
3. Update `meson.build` to add new test cases
4. Run verification tests to ensure proofs pass
5. Use verbose output to optimize performance if needed
6. Never commit unless verification succeeds

The architecture prioritizes both mathematical elegance and verification performance through selective axiom inclusion.