apophis-fastify/docs/attic/root-history/ARCHITECTURE

# APOPHIS Architecture (Revised)

## Overview

APOPHIS is a Fastify plugin that extends `@fastify/swagger` with contract-driven testing capabilities inspired by APOSTL (API PrOperty SpecificaTion Language) and PETIT (aPi tEsTIng Tool). It enables developers to write API contracts directly in their Fastify route schemas using OpenAPI custom properties (`x-*`), making the API self-documenting and self-testing.

This revision addresses header-sensitive APIs, safe hook ordering, escape hatches, formula safety, scope registries, and symbolic derivation of test properties from contracts.

## Core Concepts

### Design by Contract for APIs

APOPHIS brings Design by Contract principles to REST APIs through OpenAPI extensions:

- **Invariants** (`x-invariants`): Properties that must always hold across the entire API
- **Preconditions** (`x-requires`): Conditions that must hold before an operation executes
- **Postconditions** (`x-ensures`): Conditions that must hold after an operation executes
- **Data Generation** (`x-regex`): Regular expressions for generating valid test data
- **Category Override** (`x-category`): Override PETIT's default HTTP-method-based categorization
- **Header Access** (`request_headers(this).name`, `response_headers(this).name`): Access request/response headers in APOSTL formulas using property syntax. `request_headers(this).x-foo` checks incoming headers (preconditions), `response_headers(this).x-bar` checks outgoing headers (postconditions)

### Operation Categories

Following PETIT's methodology, operations are categorized for testing. APOPHIS uses **path-semantic inference** with HTTP method as fallback:

**Path-Semantic Rules** (checked in order):
- **Utility**: Paths containing `/reset`, `/health`, `/ping`, `/login`, `/logout`, `/auth`, `/callback`, `/purge`, `/clear`, `/initialize`, `/setup`, `/webhook`
- **Observer**: `GET` requests, paths ending with `/search`, `/count`, `/stats`, `/status`
- **Constructor**: `POST` to paths that look like collections (no path parameter after the resource name: `/players`, `/tournaments`)
- **Mutator**: `PUT`, `PATCH`, `DELETE`, or `POST` to specific resources (has path parameter: `/players/{id}`, `/tournaments/{id}/enrollments`)

**HTTP Method Fallback** (if no path-semantic match):
- **Constructors** (POST): Create resources
- **Mutators** (PUT, DELETE): Modify resources
- **Observers** (GET): Read resources without side effects
- **Utility** (arbitrary): Escape hatch for operations that don't fit

**Override with `x-category`:**
```yaml
paths:
  /reset:
    post:
      x-category: utility
      x-requires: [T]
      x-ensures: [T]
```

This ensures `POST /reset` is automatically categorized as `utility` without requiring an explicit override, while `POST /players` correctly becomes a `constructor`.

## Architecture Components

### 1. Schema Extensions (`lib/schema-extensions.js`)

Extends Fastify's JSON Schema with APOSTL annotations:

```javascript
// Example route schema with APOSTL annotations
fastify.post('/players/:playerNIF', {
  schema: {
    description: 'Create a new player',
    tags: ['players'],
    // Preconditions: what must be true before execution (including headers)
    'x-requires': [
      'response_code(GET /players/{playerNIF}) == 404',
      // Request header MUST be present (upset if missing)
      'request_headers(this).x-tenant-id != null',
      // Request header MUST have specific value
      'request_headers(this).content-type == "application/json"'
    ],
    // Postconditions: what must be true after execution (including headers)
    'x-ensures': [
      'response_code(GET /players/{playerNIF}) == 200',
      'response_body(this) == request_body(this)',
      // Response header postcondition
      'response_headers(this).x-ledger-status == "finalized"'
    ],
    params: {
      type: 'object',
      properties: {
        playerNIF: {
          type: 'string',
          'x-regex': '(1|2)[0-9]{8}'  // Data generation pattern
        }
      }
    },
    body: {
      type: 'object',
      properties: {
        playerNIF: { type: 'string' },
        firstName: { type: 'string' },
        lastName: { type: 'string' },
        email: { type: 'string', format: 'email' }
      }
    },
    response: {
      201: {
        description: 'Player created',
        type: 'object'
      }
    }
  }
}, handler)
```

### 2. APOSTL Formula Parser (`lib/formula-parser.js`)

Parses and evaluates APOSTL formulas written in route schemas:

**Extended Grammar (APOSTL + Headers + Arbiter):**

```
formula ::= quantifiedFormula | booleanExpression | conditionalFormula
quantifiedFormula ::= quantifier string in call :- booleanExpression
quantifier ::= for | exists
conditionalFormula ::= if comparison then formula else formula
booleanExpression ::= booleanExpression booleanOperator booleanExpression | clause
clause ::= T | F | comparison
comparison ::= term comparator term
term ::= operation | operationPrevious | param
operationPrevious ::= previous(operation)
operation ::= operationHeader(operationParameter) function?
operationHeader ::= request_body | response_body | response_code | request_headers | response_headers | query_params | cookies | response_time
operationParameter ::= httpRequest | this
httpRequest ::= method url
comparator ::= == | != | <= | >= | < | > | matches
booleanOperator ::= && | || | =>
```

**Key Features:**
- Pure operations only (GET requests for conditions)
- `previous()` keyword to access state before operation
- `this` keyword to reference current request/response
- `request_headers(this).name` to reference incoming request headers
- `response_headers(this).name` to reference outgoing response headers
- `response_headers(GET /url).name` to reference headers from a GET request
- `query_params(this).name` to reference query parameters
- `query_params(GET /url).name` to reference query params from another request
- `cookies(this).name` to reference cookies
- `response_time(this)` to reference response time in milliseconds
- `response_time(GET /url)` to reference response time of another request
- `matches` comparator for regex matching
- Conditional formulas: `if condition then formula else formula`
- Quantifiers: `for` (universal), `exists` (existential)

### 3. Scope Registry (`lib/scope-registry.js`)

Manages tenant/application scope for header-sensitive APIs automatically:

```javascript
class ScopeRegistry {
  constructor(options = {}) {
    this.scopes = new Map()
    this.defaultScope = {
      tenantId: options.defaultTenantId || 'default',
      applicationId: options.defaultApplicationId || 'service-a',
      headers: options.defaultHeaders || {}
    }
    
    // Auto-discover scopes from environment
    this.discoverFromEnvironment()
  }

  // Auto-discover scopes from environment variables
  discoverFromEnvironment() {
    // APOPHIS_SCOPE_tenant-a={"tenantId":"tenant-a",...}
    for (const [key, value] of Object.entries(process.env)) {
      if (key.startsWith('APOPHIS_SCOPE_')) {
        const scopeName = key.replace('APOPHIS_SCOPE_', '').toLowerCase()
        try {
          const config = JSON.parse(value)
          this.register(scopeName, config)
        } catch (e) {
          console.warn(`Invalid APOPHIS scope config for ${scopeName}: ${e.message}`)
        }
      }
    }
  }

  // Derive scope from request headers automatically
  deriveFromRequest(request) {
    const tenantId = request.headers['x-tenant-id']
    const applicationId = request.headers['x-application-id']
    
    if (!tenantId) return this.defaultScope
    
    const scopeName = `${tenantId}-${applicationId || 'default'}`
    
    if (!this.scopes.has(scopeName)) {
      // Auto-register derived scope
      this.register(scopeName, {
        tenantId,
        applicationId: applicationId || 'default',
        headers: Object.fromEntries(
          Object.entries(request.headers)
            .filter(([k]) => k.startsWith('x-'))
        )
      })
    }
    
    return this.get(scopeName)
  }

  register(scopeName, scopeConfig) {
    this.scopes.set(scopeName, {
      tenantId: scopeConfig.tenantId,
      applicationId: scopeConfig.applicationId,
      headers: scopeConfig.headers || {},
      auth: scopeConfig.auth || null
    })
  }

  get(scopeName) {
    return this.scopes.get(scopeName) || this.defaultScope
  }

  // Generate headers for a given scope
  getHeaders(scopeName, overrides = {}) {
    const scope = this.get(scopeName)
    return {
      'x-tenant-id': scope.tenantId,
      'x-application-id': scope.applicationId,
      ...scope.headers,
      ...overrides
    }
  }

  // Get auth header for scope
  getAuth(scopeName) {
    const scope = this.get(scopeName)
    return scope.auth
  }
}

// Usage in APOPHIS - automatic, no manual registration needed:
// Scopes auto-derived from requests or environment variables
// Optional: manually register for test setup
fastify.apophis.scope.register('tenant-a', {
  tenantId: 'tenant-a',
  applicationId: 'app-1'
})
```

### 4. Safe Hook Ordering (`lib/contract-validator.js`)

Validates API contracts at runtime with safe hook placement:

```javascript
// Validates preconditions before route handler
async function validatePreconditions(request, reply, routeSchema) {
  const preconditions = routeSchema['x-requires']
  if (!preconditions) return true
  
  for (const condition of preconditions) {
    const result = await evaluateFormula(condition, { request })
    if (!result) {
      throw new Error(`Precondition failed: ${condition}`)
    }
  }
  return true
}

// Validates postconditions BEFORE serialization (onResponse, not onSend)
// Handles both body and header postconditions via unified APOSTL DSL
async function validatePostconditions(request, reply, routeSchema) {
  const postconditions = routeSchema['x-ensures']
  if (!postconditions) return true
  
  for (const condition of postconditions) {
    const result = await evaluateFormula(condition, { request, reply })
    if (!result) {
      throw new Error(`Postcondition failed: ${condition}`)
    }
  }
  return true
}
```

**Hook Placement:**

```javascript
// SAFE: preHandler for preconditions (before handler)
  // Validates x-requires including request_headers() conditions
fastify.addHook('preHandler', async (request, reply) => {
  await validatePreconditions(request, reply, request.routeSchema)
})

// SAFE: onResponse for postconditions (after handler, before serialization)
// Validates x-ensures including response_headers() conditions
fastify.addHook('onResponse', async (request, reply) => {
  await validatePostconditions(request, reply, request.routeSchema)
})

// UNSAFE: onSend may have already serialized the payload
// DO NOT USE: fastify.addHook('onSend', ...)
```

### 5. Formula Parameter Substitution (`lib/formula-substitutor.js`)

Safe parameter substitution with proper escaping and validation:

```javascript
class FormulaSubstitutor {
  constructor() {
    this.paramPattern = /\{([^}]+)\}/g
    this.validationPattern = /^[a-zA-Z0-9_.-]+$/
  }

  // Safely substitute parameters in a formula
  substitute(formula, params) {
    if (!formula || typeof formula !== 'string') {
      throw new Error('Formula must be a non-empty string')
    }

    return formula.replace(this.paramPattern, (match, paramName) => {
      // Validate parameter name (prevent injection)
      if (!this.validationPattern.test(paramName)) {
        throw new Error(`Invalid parameter name: ${paramName}`)
      }

      // Get parameter value
      const value = this.resolveParam(params, paramName)
      
      if (value === undefined || value === null) {
        throw new Error(`Missing parameter: ${paramName}`)
      }

      // Escape the value for safe insertion
      return this.escapeValue(value)
    })
  }

  // Resolve nested parameters (e.g., "t.tournamentId")
  resolveParam(params, path) {
    const parts = path.split('.')
    let current = params
    
    for (const part of parts) {
      if (current === null || current === undefined) {
        return undefined
      }
      current = current[part]
    }
    
    return current
  }

  // Escape values to prevent formula injection
  escapeValue(value) {
    if (typeof value === 'string') {
      // Escape quotes and backslashes
      return '"' + value.replace(/\\/g, '\\\\').replace(/"/g, '\\"') + '"'
    }
    if (typeof value === 'number' || typeof value === 'boolean') {
      return String(value)
    }
    // For objects/arrays, serialize to JSON
    return JSON.stringify(value)
  }

  // Validate that all required parameters are present
  validateParams(formula, params) {
    const required = new Set()
    let match
    
    while ((match = this.paramPattern.exec(formula)) !== null) {
      required.add(match[1])
    }

    const missing = []
    for (const param of required) {
      if (this.resolveParam(params, param) === undefined) {
        missing.push(param)
      }
    }

    if (missing.length > 0) {
      throw new Error(`Missing required parameters: ${missing.join(', ')}`)
    }

    return true
  }
}
```

### 6. Cleanup Mechanism (`lib/cleanup-manager.js`)

Automatic resource cleanup with deterministic rollback:

```javascript
class CleanupManager {
  constructor(fastify) {
    this.fastify = fastify
    this.createdResources = []
    this.scope = null
    this.autoCleanup = true
    this.registered = false
  }

  // Set scope for cleanup operations
  setScope(scopeName) {
    this.scope = scopeName
  }

  // Automatically track resources from constructor responses
  autoTrack(response, routeSchema) {
    if (!this.autoCleanup) return
    
    // Only track constructors (POST to collections)
    const category = routeSchema?.['x-category'] || this.inferCategory(routeSchema)
    if (category !== 'constructor') return
    
    // Extract resource ID and URL from response
    const resourceId = this.extractResourceId(response)
    const deleteUrl = this.buildDeleteUrl(routeSchema.path, resourceId)
    
    if (resourceId && deleteUrl) {
      this.track(routeSchema.path, resourceId, deleteUrl)
    }
  }

  extractResourceId(response) {
    try {
      const body = typeof response.payload === 'string' 
        ? JSON.parse(response.payload) 
        : response.payload
      
      // Common ID fields: id, uuid, tournamentId, playerNIF, etc.
      return body?.id || body?.uuid || body?.tournamentId || body?.playerNIF
    } catch {
      return null
    }
  }

  buildDeleteUrl(pathTemplate, resourceId) {
    // Convert /players/:playerNIF to /players/123456789
    return pathTemplate.replace(/:\w+/g, resourceId)
  }

  inferCategory(schema) {
    // Path-semantic inference
    const path = schema?.path || ''
    if (/\/(reset|health|ping|login|logout|auth|callback|purge|clear|initialize|setup|webhook)/.test(path)) return 'utility'
    if (schema?.method === 'GET') return 'observer'
    if (schema?.method === 'POST' && !/\{\w+\}/.test(path)) return 'constructor'
    return 'mutator'
  }

  // Track a created resource for later cleanup
  track(resourceType, identifier, deleteUrl) {
    this.createdResources.push({
      type: resourceType,
      id: identifier,
      url: deleteUrl,
      timestamp: Date.now()
    })
  }

  // Cleanup all tracked resources in reverse order
  async cleanup() {
    const headers = this.scope 
      ? this.fastify.apophis.scope.getHeaders(this.scope)
      : {}

    const errors = []
    
    // Delete in reverse order (LIFO)
    for (let i = this.createdResources.length - 1; i >= 0; i--) {
      const resource = this.createdResources[i]
      try {
        await this.fastify.inject({
          method: 'DELETE',
          url: resource.url,
          headers
        })
      } catch (error) {
        errors.push({ resource, error: error.message })
      }
    }

    this.createdResources = []
    
    if (errors.length > 0) {
      console.warn('Cleanup errors:', errors)
    }
    
    return errors
  }

  // Register cleanup on process exit (called automatically)
  registerExitHandler() {
    if (this.registered) return
    this.registered = true
    
    const cleanup = async () => {
      await this.cleanup()
      process.exit(0)
    }
    
    process.on('SIGINT', cleanup)
    process.on('SIGTERM', cleanup)
    process.on('exit', cleanup)
  }

  // Explicit cleanup call for manual control
  async cleanup() {
    return this.cleanup()
  }
}
```

### 7. Test Data Generator (`lib/test-data-generator.js`)

Generates valid test data based on `x-regex` annotations with scope-aware headers:

```javascript
// Generates test data from regex patterns
function generateFromRegex(pattern) {
  // Uses randexp or similar library
  return randexp.generate(pattern)
}

// Generates complete request objects from schema
function generateTestData(schema, scope = null) {
  const data = {}
  for (const [key, propSchema] of Object.entries(schema.properties)) {
    if (propSchema['x-regex']) {
      data[key] = generateFromRegex(propSchema['x-regex'])
    } else if (propSchema.type === 'string') {
      data[key] = generateRandomString(propSchema)
    } else if (propSchema.type === 'integer') {
      data[key] = generateRandomInteger(propSchema)
    }
    // ... handle other types
  }
  return data
}

// Generate headers for a request based on scope
function generateHeaders(schema, scopeName, scopeRegistry) {
  const headers = scopeRegistry.getHeaders(scopeName)
  
  // Extract required headers from x-requires formulas
  // Pattern: request_headers(this).header-name
  if (schema['x-requires']) {
    for (const condition of schema['x-requires']) {
      const headerMatches = condition.matchAll(/request_headers\(this\)\.([a-zA-Z0-9_-]+)/g)
      for (const match of headerMatches) {
        const headerName = match[1]
        if (!headers[headerName]) {
          // Generate default value if not in scope
          headers[headerName] = generateDefaultHeader(headerName)
        }
      }
    }
  }
  
  return headers
}
```

### 8. PETIT Test Runner (`lib/petit-runner.js`)

Automated testing engine with category override and scope support:

```javascript
class PetitRunner {
  constructor(fastify, options = {}) {
    this.fastify = fastify
    this.strategy = options.strategy || 'CMO'
    this.verbose = options.verbose || false
    this.objectPool = new Map()
    this.scope = options.scope || null
    this.cleanupManager = new CleanupManager(fastify)
  }
  
  async run() {
    const apis = this.discoverAPIs()
    const results = []
    
    try {
      for (const api of apis) {
        results.push(await this.testAPI(api))
      }
    } finally {
      // Always cleanup, even on failure
      await this.cleanupManager.cleanup()
    }
    
    return results
  }
  
  categorizeOperations(api) {
    const categories = {
      constructors: [],
      mutators: [],
      observers: [],
      utility: []
    }
    
    for (const op of api.operations) {
      // Check for x-category override first
      const override = op.schema?.['x-category']
      if (override) {
        categories[override].push(op)
        continue
      }
      
      // Default categorization by HTTP method
      switch (op.method.toUpperCase()) {
        case 'POST':
          categories.constructors.push(op)
          break
        case 'PUT':
        case 'DELETE':
          categories.mutators.push(op)
          break
        case 'GET':
          categories.observers.push(op)
          break
        default:
          categories.utility.push(op)
      }
    }
    
    return categories
  }
  
  async testOperation(operation) {
    const headers = this.scope 
      ? this.fastify.apophis.scope.getHeaders(this.scope)
      : {}

    // 1. Verify invariants
    // 2. Generate or recycle test data
    // 3. Verify preconditions (including header preconditions)
    // 4. Execute request with proper headers
    // 5. Verify postconditions (including header postconditions)
    // 6. Track created resources for cleanup
    // 7. Store results
  }
}
```

### 9. Plugin Entry Point (`index.js`)

Main Fastify plugin registration with scope registry:

```javascript
const fp = require('fastify-plugin')

async function apophisPlugin(fastify, options) {
  // Initialize scope registry
  const scopeRegistry = new ScopeRegistry()
  
  // Register with @fastify/swagger if not already registered
  if (!fastify.swagger) {
    await fastify.register(require('@fastify/swagger'), {
      ...options.swagger,
      transform: apophisTransform
    })
  }
  
  // Decorate fastify with APOPHIS utilities
  fastify.decorate('apophis', {
    // Scope registry for header-sensitive APIs (auto-derived + manual override)
    scope: scopeRegistry,
    
    // Generate OpenAPI with APOSTL annotations
    spec: () => generateApophisSpec(fastify),
    
    // Single test entry point: runs contract + property + stateful tests optimized
    test: async (opts = {}) => {
      const {
        mode = 'all',       // 'all' | 'contract' | 'property' | 'stateful'
        depth = 'standard', // 'quick' | 'standard' | 'thorough'
        ...runnerOpts
      } = opts

      const config = {
        quick: { contractRuns: 10, propertyRuns: 50, statefulRuns: 5, maxCommands: 10 },
        standard: { contractRuns: 50, propertyRuns: 100, statefulRuns: 20, maxCommands: 30 },
        thorough: { contractRuns: 200, propertyRuns: 1000, statefulRuns: 100, maxCommands: 50 }
      }[depth]

      const results = { mode, depth, contract: null, property: null, stateful: null }
      const cleanupManager = new CleanupManager(fastify)
      cleanupManager.setScope(runnerOpts.scope || null)

      try {
        if (mode === 'all' || mode === 'contract') {
          results.contract = await new PetitRunner(fastify, {
            ...runnerOpts,
            ...config,
            cleanupManager
          }).run()
        }

        if (mode === 'all' || mode === 'property') {
          results.property = await new ApophisPropertyTester(fastify, {
            ...runnerOpts,
            ...config,
            cleanupManager
          }).runPropertyTests()
        }

        if (mode === 'all' || mode === 'stateful') {
          results.stateful = await new ApophisStatefulRunner(fastify, {
            ...runnerOpts,
            ...config,
            cleanupManager
          }).run()
        }
      } finally {
        // Always cleanup, even on failure
        await cleanupManager.cleanup()
      }

      return results
    },

    // Explicit cleanup for manual resource management
    cleanup: async () => {
      const cleanupManager = new CleanupManager(fastify)
      return cleanupManager.cleanup()
    },
    
    // Validate a specific route's contracts
    validate: (routePath) => validateRouteContracts(fastify, routePath),
    
    // Generate test data for a route
    generateTestData: (routePath) => generateRouteTestData(fastify, routePath)
  })
  
  // Add hooks for runtime contract validation (optional, with per-route opt-out)
  if (options.validateRuntime !== false) {
    // preHandler: validate preconditions before route handler
    fastify.addHook('preHandler', async (request, reply) => {
      // Per-route opt-out via x-validate-runtime: false
      if (request.routeSchema?.['x-validate-runtime'] === false) return
      await validatePreconditions(request, reply, request.routeSchema)
    })
    
    // onResponse: validate postconditions after handler, before serialization
    fastify.addHook('onResponse', async (request, reply) => {
      // Per-route opt-out via x-validate-runtime: false
      if (request.routeSchema?.['x-validate-runtime'] === false) return
      await validatePostconditions(request, reply, request.routeSchema)
    })
  }
}

module.exports = fp(apophisPlugin, {
  name: 'apophis-fastify',
  dependencies: ['@fastify/swagger']
})
```

## Data Flow

### 1. Schema Definition Flow

```
Developer writes route schema with x-* annotations
        |
        v
Fastify validates route schema (ignores x-* properties)
        |
        v
@fastify/swagger generates OpenAPI spec
        |
        v
apophisTransform preserves x-* annotations in output
        |
        v
OpenAPI spec contains self-documenting contracts
```

### 2. Runtime Validation Flow

```
Request arrives
        |
        v
preHandler hook: validate x-requires preconditions
        |
        v
Route handler executes
        |
        v
Handler sets response headers/body
        |
        v
onResponse hook: validate x-ensures postconditions
        |               (before serialization - safe!)
        v
Serialization (onSend)
        |
        v
Response sent
```

### 3. Test Execution Flow (PETIT)

```
Developer calls fastify.apophis.test({ scope: 'tenant-a' })
        |
        v
Discover all routes with x-* annotations
        |
        v
Categorize: Constructors / Mutators / Observers / Utility
        | (respecting x-category overrides)
        v
Apply order strategy (e.g., CMO)
        |
        v
For each operation:
  - Get headers from scope registry
  - Verify API invariants
  - Generate/recycle test data (using x-regex)
  - Verify preconditions (x-requires including request_headers() conditions)
  - Execute HTTP request with scope headers
  - Verify postconditions (x-ensures including response_headers() conditions)
  - Track created resources for cleanup
        |
        v
Cleanup: Remove all generated test data (reverse order)
        |
        v
Return test results
```

## OpenAPI Extensions Reference

### `x-invariants`

API-level invariants that must always hold:

```yaml
paths:
  /tournaments:
    x-invariants:
      - for t in response_body(GET /tournaments) :-
          response_body(GET /tournaments/{t.tournamentId}/enrollments).length <=
          response_body(GET /tournaments/{t.tournamentId}/capacity)
```

### `x-requires`

Operation preconditions:

```yaml
paths:
  /players/{playerNIF}:
    delete:
      x-requires:
        - response_code(GET /players/{playerNIF}) == 200
```

### `x-ensures`

Operation postconditions:

```yaml
paths:
  /players/{playerNIF}:
    delete:
      x-ensures:
        - response_code(GET /players/{playerNIF}) == 404
        - response_body(this) == previous(response_body(GET /players/{playerNIF}))
```

### Header Access in APOSTL Formulas

APOPHIS extends APOSTL with `request_headers` and `response_headers` accessors that use property syntax (via the `function` rule):

**Request headers** (available in preconditions and postconditions):
```yaml
x-requires:
  # Request MUST have x-tenant-id header (upset if missing)
  - request_headers(this).x-tenant-id != null
  
  # Request content-type MUST be application/json
  - request_headers(this).content-type == "application/json"
  
  # Request MUST have either authorization OR txn-token
  - request_headers(this).authorization != null || request_headers(this).txn-token != null
  
  # Optional header: if present must be valid; if absent, ok
  - request_headers(this).x-explain == null || request_headers(this).x-explain == "true"
```

**Response headers** (only available in postconditions):
```yaml
x-ensures:
  # Response MUST include x-ledger-status header
  - response_headers(this).x-ledger-status != null
  
  # Response x-ledger-status MUST be "finalized"
  - response_headers(this).x-ledger-status == "finalized"
  
  # Response content-type MUST be application/json
  - response_headers(this).content-type == "application/json"
```

**Header invariants** (must hold for ALL operations):
```yaml
x-invariants:
  # Every request must have tenant identification
  - request_headers(this).x-tenant-id != null
  
  # Every response must include request ID for tracing
  - response_headers(this).x-request-id != null
```

**Headers from other requests** (in quantifiers and comparisons):
```yaml
x-requires:
  # Verify a GET request returns specific headers
  - response_headers(GET /players/{playerNIF}).content-type == "application/json"
```

### Arbiter-Specific DSL Extensions

APOPHIS extends APOSTL with additional accessors needed for header-sensitive, multi-tenant APIs like Arbiter and Operator:

**Query Parameters:**
```yaml
x-requires:
  # Pagination parameter must be present
  - query_params(this).page != null
  
  # Page size must be within limits
  - query_params(this).limit <= 100
  
  # Format override check
  - query_params(this).format == null || query_params(this).format == "json" || query_params(this).format == "html"

x-ensures:
  # Response respects requested format
  - if query_params(this).format == "json" then response_headers(this).content-type == "application/json" else T
```

**Cookies:**
```yaml
x-requires:
  # Session cookie must exist for authenticated endpoints
  - cookies(this).session_id != null
  
  # CSRF token validation
  - cookies(this).csrf_token == request_headers(this).x-csrf-token
```

**Response Time (Performance Contracts):**
```yaml
x-ensures:
  # Response must be fast enough
  - response_time(this) < 500
  
  # Rate limit check: if too fast, must be rate limited
  - if response_time(GET /health) < 50 then response_headers(this).x-ratelimit-remaining != null else T
```

**Request Body of Other Operations:**
```yaml
x-ensures:
  # Verify the POST body we sent matches what the GET returns
  - response_body(GET /players/{playerNIF}) == request_body(POST /players)
```

**Regex Matching:**
```yaml
x-requires:
  # Email format validation
  - request_body(this).email matches "^[a-zA-Z0-9._%+-]+@[a-zA-Z0-9.-]+\\.[a-zA-Z]{2,}$"
  
  # UUID format check
  - response_body(this).id matches "^[0-9a-f]{8}-[0-9a-f]{4}-[0-9a-f]{4}-[0-9a-f]{4}-[0-9a-f]{12}$"
```

**Conditional Postconditions (Multi-step Flows):**
```yaml
x-ensures:
  # Challenge flow: if challenge required, specific response; otherwise success
  - if response_code(this) == 403 then response_body(this).challenge_type != null else response_code(this) == 200
  
  # Tenant boundary: regular users get 403, admins bypass
  - if request_headers(this).x-user-role == "admin" then response_code(this) == 200 else response_code(this) != 403
```

**State Transition Verification:**
```yaml
x-requires:
  # Before MFA challenge, user must not be MFA-verified
  - response_body(GET /users/{userId}).mfa_verified == false

x-ensures:
  # After submitting MFA code, user is verified
  - response_body(GET /users/{userId}).mfa_verified == true
  
  # Previous state preserved for rollback check
  - previous(response_body(GET /users/{userId}).mfa_verified) == false
```

### `x-regex`

Data generation patterns for properties:

```yaml
paths:
  /players/{playerNIF}:
    get:
      parameters:
        - name: playerNIF
          schema:
            type: string
            x-regex: "(1|2)[0-9]{8}"
```

### `x-category`

Override PETIT's default categorization:

```yaml
paths:
  /reset:
    post:
      x-category: utility
      x-requires: [T]
      x-ensures: [T]
```

Valid values: `constructor`, `mutator`, `observer`, `utility`

## Arbiter Auto-Testing Coverage

### What APOPHIS Can Auto-Test

With the extended DSL, APOPHIS can now automatically verify:

**1. Header Contract Compliance**
- Tenant boundary enforcement (`x-tenant-id` mismatch → 403)
- Token transport rules (ADR-052: txn-token in Authorization rejected)
- Required headers present (`x-application-id`, `content-type`)
- Response headers correct (`X-Ledger-Status`, `X-Request-Id`)

**2. Authentication Flows**
- Access token vs transaction token paths
- Missing auth → 401/403
- Invalid delegation tokens rejected
- S2S workload identity headers validated

**3. Challenge/Remediation Flows**
- Step-up authentication sequences
- MFA challenge → response with challenge options → MFA code → success
- WebAuthn assertion handling
- Conditional postconditions based on challenge state

**4. Rate Limiting**
- Response time checks (`response_time(this) < 500`)
- Rate limit headers present when expected (`X-RateLimit-Remaining`)
- 429 responses after threshold

**5. Tenant Isolation**
- Cross-tenant access blocked (JWT tenant != header tenant → 403)
- Admin bypass rules (`masterInternal`/`rootInternal` scopes)
- Graph store selection per scope

**6. Ledger Operations**
- Billing headers on metered endpoints
- Finalization status tracking
- Resource consumption reporting

**7. Content Negotiation**
- Accept header respected (`text/html` → HTML, `application/json` → JSON)
- Format query parameter overrides (`?format=markdown`)
- HTMX fragment responses (`HX-Request: true` → `html-fragment`)

### What Requires External Testing

Some Arbiter behaviors need specialized testing beyond contract DSL:

**1. Cryptographic Verification**
- HTTP Message Signature validation (`signature`, `signature-input`)
- Workload identity token proof verification
- Certificate chain validation
- *Why*: Requires crypto libraries, not expressible in HTTP contracts

**2. Database State Verification**
- Transaction isolation levels
- Deadlock detection
- Replication lag
- *Why*: Requires direct DB access, not API surface

**3. Infrastructure Behaviors**
- Load balancer health checks
- Graceful shutdown sequences
- Connection pool exhaustion
- *Why*: Requires system-level access

**4. Browser-Specific Flows**
- OAuth2 redirect flows (browser cookies, `sec-fetch-mode`)
- WebAuthn browser integration
- CORS preflight handling
- *Why*: Requires real browser or Playwright

**5. Eventual Consistency**
- Async ledger finalization timing
- Cache invalidation delays
- Graph store replication lag
- *Why*: Time-dependent, flaky in contract tests

**6. Security Penetration**
- SQL injection attempts
- XSS payload handling
- Path traversal
- *Why*: Requires adversarial input generation, not contract validation

### Recommended Test Pyramid for Arbiter

```
Top: Browser/Integration Tests (Playwright)
  - OAuth flows
  - HTMX interactions
  - Full user journeys

Middle: APOPHIS Contract Tests (PETIT + fast-check)
  - Header contracts
  - Auth flows
  - Challenge sequences
  - Rate limiting
  - Tenant isolation
  - Ledger tracking

Bottom: Unit Tests + DB Tests
  - Crypto verification
  - DB transactions
  - Business logic
```

## Testing Strategies

### Order Strategies

Following PETIT's approach:

- **COM**: Constructors → Observers → Mutators
- **CMO**: Constructors → Mutators → Observers
- **MCO**: Mutators → Constructors → Observers
- **MOC**: Mutators → Observers → Constructors
- **OCM**: Observers → Constructors → Mutators
- **OMC**: Observers → Mutators → Constructors
- **RND**: Random order

### Test Outcomes

| Preconditions | Response | Result |
|--------------|----------|--------|
| True | 200 OK | OK (if postconditions pass) |
| True | 4XX | Failed (analyze execution trace) |
| False | 200 | NOT OK (should have failed) |
| False | 4XX | Failed (as expected) |

## Stateful Testing Mechanics

Stateful testing in APOPHIS uses **model-based testing** with fast-check's `fc.modelBased` or command-based testing. The system generates random sequences of API operations, executes them against both a derived state machine model and the real API, and verifies they remain synchronized.

### Core Concepts

**Model State vs Real State**
- **Model State**: An in-memory abstraction tracking what "should" exist (derived from schema + invariants)
- **Real State**: The actual Fastify server state (database, cache, etc.)
- **Synchronization**: After each command, model predictions are verified against real API responses

**Commands**
Each API operation becomes a `Command` in the state machine:

```javascript
class ApiCommand {
  constructor(operation, params, headers) {
    this.operation = operation      // Route schema + metadata
    this.params = params            // Generated parameters (path, query, body)
    this.headers = headers          // Scope headers + generated headers
    this.category = operation.category // constructor | mutator | observer | utility
  }

  // Check if this command can run in current model state (preconditions)
  check(modelState) {
    // Evaluate x-requires against model state
    return evaluatePreconditionsOnModel(this.operation['x-requires'], modelState, this.params)
  }

  // Run the command against the REAL API
  async run(realState) {
    const response = await realState.fastify.inject({
      method: this.operation.method,
      url: substituteParams(this.operation.path, this.params),
      payload: this.params.body,
      query: this.params.query,
      headers: this.headers
    })
    return response
  }

  // Update the MODEL state based on command execution
  runModel(modelState) {
    // Apply state transition based on operation category and x-ensures
    return applyModelTransition(modelState, this.operation, this.params, this.category)
  }

  // Fast-check shrinking: how to simplify this command
  shrink() {
    // Shrink parameters while maintaining schema validity
    return shrinkParams(this.operation.schema, this.params)
  }
}
```

### State Machine Definition

The state machine is derived from the API schema and invariants:

```javascript
class ApophisStateMachine {
  constructor(fastify, options = {}) {
    this.fastify = fastify
    this.scope = options.scope || null
    this.model = this.buildInitialModel()
    this.commands = this.discoverCommands()
    this.invariants = this.extractInvariants()
  }

  // Initial model state derived from schema structure
  buildInitialModel() {
    const model = new Map()
    
    // Discover all resource collections from schemas
    for (const [path, route] of Object.entries(this.fastify.getSchemas())) {
      if (route.response?.[201] || route.response?.[200]) {
        const resourceName = this.extractResourceName(path)
        model.set(resourceName, {
          items: new Map(),
          relationships: new Map(),
          counters: new Map()
        })
      }
    }
    
    return model
  }

  // Discover all possible commands from registered routes
  discoverCommands() {
    const commands = []
    
    for (const route of this.fastify.routes) {
      const category = route.schema?.['x-category'] || this.inferCategory(route.method)
      const schema = route.schema || {}
      
      // Build parameter arbitrary from schema
      const paramsArb = this.buildParamsArbitrary(route)
      
      commands.push({
        name: `${route.method} ${route.path}`,
        category,
        path: route.path,
        method: route.method,
        schema,
        paramsArb,
        // Weight for random selection (observers more frequent than mutators)
        weight: category === 'observer' ? 5 : category === 'constructor' ? 2 : 3
      })
    }
    
    return commands
  }

  // Extract invariants from x-invariants declarations
  extractInvariants() {
    const invariants = []
    
    for (const route of this.fastify.routes) {
      if (route.schema?.['x-invariants']) {
        invariants.push(...route.schema['x-invariants'])
      }
    }
    
    // Also derive invariants from schema constraints
    invariants.push(...this.deriveSchemaInvariants())
    
    return invariants
  }
}
```

### Command Generation Strategy

fast-check generates command sequences by:

1. **Filtering valid commands**: Only commands whose `check()` passes in current model state
2. **Category-aware generation**: Ensure resource exists before mutating it
3. **Biased selection**: Favor observers (safer) over constructors/mutators

```javascript
function generateCommandSequence(stateMachine, maxCommands = 50) {
  return fc.array(
    fc.constantFrom(...stateMachine.commands)
      .chain(command => {
        // Generate valid parameters for this command
        return command.paramsArb.map(params => ({
          ...command,
          params,
          headers: stateMachine.scope 
            ? stateMachine.fastify.apophis.scope.getHeaders(stateMachine.scope)
            : {}
        }))
      })
      .filter(command => {
        // Only include commands that can run in current state
        return command.check(stateMachine.model)
      }),
    { minLength: 1, maxLength: maxCommands }
  )
}
```

### Model-Real Synchronization Verification

After each command executes, verify the model prediction matches reality:

```javascript
async function verifySynchronization(modelState, realResponse, command) {
  const discrepancies = []
  
  // 1. Response code matches prediction
  const predictedCode = predictResponseCode(modelState, command)
  if (predictedCode !== realResponse.statusCode) {
    discrepancies.push({
      type: 'status_code_mismatch',
      predicted: predictedCode,
      actual: realResponse.statusCode
    })
  }
  
  // 2. Response body structure matches schema
  if (realResponse.statusCode < 400) {
    const schema = command.schema.response?.[realResponse.statusCode]
    if (schema) {
      const validation = validateAgainstSchema(realResponse.json(), schema)
      if (!validation.valid) {
        discrepancies.push({
          type: 'schema_violation',
          errors: validation.errors
        })
      }
    }
  }
  
  // 3. Invariants still hold in real state
  for (const invariant of stateMachine.invariants) {
    const holds = await evaluateInvariantOnReal(invariant, realResponse, command)
    if (!holds) {
      discrepancies.push({
        type: 'invariant_violation',
        invariant
      })
    }
  }
  
  // 4. Model-derived postconditions
  if (command.schema?.['x-ensures']) {
    for (const postcondition of command.schema['x-ensures']) {
      const holds = await evaluatePostcondition(postcondition, realResponse, command)
      if (!holds) {
        discrepancies.push({
          type: 'postcondition_failed',
          condition: postcondition
        })
      }
    }
  }
  
  return discrepancies
}
```

### Complete Stateful Test Runner

```javascript
class ApophisStatefulRunner {
  constructor(fastify) {
    this.fastify = fastify
    this.cleanupManager = new CleanupManager(fastify)
  }

  async run(options = {}) {
    const {
      numRuns = 100,
      maxCommands = 50,
      scope = null,
      seed = undefined // For deterministic replay
    } = options

    const stateMachine = new ApophisStateMachine(this.fastify, { scope })
    
    return fc.assert(
      fc.property(
        generateCommandSequence(stateMachine, maxCommands),
        async (commands) => {
          // Setup: Start with empty state or seed state
          await this.setupInitialState(stateMachine)
          
          try {
            for (const command of commands) {
              // 1. Check preconditions on model
              if (!command.check(stateMachine.model)) {
                // Skip command if preconditions don't hold
                continue
              }
              
              // 2. Execute on REAL API
              const realResponse = await command.run({
                fastify: this.fastify,
                cleanupManager: this.cleanupManager
              })
              
              // 3. Execute on MODEL
              const newModelState = command.runModel(stateMachine.model)
              
              // 4. Verify synchronization
              const discrepancies = await verifySynchronization(
                newModelState, realResponse, command
              )
              
              if (discrepancies.length > 0) {
                throw new StatefulTestError({
                  command: command.name,
                  params: command.params,
                  discrepancies,
                  commandHistory: commands.slice(0, commands.indexOf(command) + 1)
                })
              }
              
              // 5. Update model state
              stateMachine.model = newModelState
              
              // 6. Track resources for cleanup
              if (command.category === 'constructor') {
                this.trackResourceForCleanup(command, realResponse)
              }
            }
          } finally {
            // Always cleanup
            await this.cleanupManager.cleanup()
          }
          
          return true
        }
      ),
      { numRuns, seed }
    )
  }

  setupInitialState(stateMachine) {
    // Reset model to initial state
    stateMachine.model = stateMachine.buildInitialModel()
    
    // Optionally seed with existing data
    // (e.g., if testing against non-empty database)
  }

  trackResourceForCleanup(command, response) {
    // Extract resource ID from response for later deletion
    const resourceId = response.json()?.id || response.json()?.tournamentId
    if (resourceId) {
      this.cleanupManager.track(
        command.operation.path,
        resourceId,
        command.operation.path.replace(/{.*?}/g, resourceId)
      )
    }
  }
}
```

### Handling Stateful Test Failures

When a stateful test fails, APOPHIS provides detailed diagnostics:

```javascript
class StatefulTestError extends Error {
  constructor({ command, params, discrepancies, commandHistory }) {
    super(`Stateful test failed at command: ${command}`)
    this.command = command
    this.params = params
    this.discrepancies = discrepancies
    this.commandHistory = commandHistory
  }

  toString() {
    let msg = `Stateful Test Failure\n`
    msg += `===================\n\n`
    msg += `Failed at command: ${this.command}\n`
    msg += `Parameters: ${JSON.stringify(this.params, null, 2)}\n\n`
    msg += `Command sequence (${this.commandHistory.length} commands):\n`
    this.commandHistory.forEach((cmd, i) => {
      msg += `  ${i + 1}. ${cmd.name} ${JSON.stringify(cmd.params)}\n`
    })
    msg += `\nDiscrepancies:\n`
    this.discrepancies.forEach(d => {
      msg += `  - [${d.type}]: ${JSON.stringify(d)}\n`
    })
    return msg
  }
}
```

### Deterministic Replay

Failed stateful tests can be replayed exactly:

```javascript
// On failure, fast-check provides the seed and path
const failedRun = {
  seed: 12345,
  path: "0:1:2:3:4",  // Which branches were taken
  counterexample: [/* commands that failed */]
}

// Replay the exact same test
await runner.run({
  seed: failedRun.seed,
  // fast-check handles path replay internally
})
```

### Example: Tournament Stateful Test

```javascript
// Derived from the Tournament API schema
const tournamentStatefulTest = async (fastify) => {
  const runner = new ApophisStatefulRunner(fastify)
  
  return runner.run({
    numRuns: 100,
    maxCommands: 30,
    scope: 'tenant-a'
  })
}

// A failing test might produce:
// Stateful Test Failure
// ===================
// Failed at command: POST /tournaments/{tournamentId}/enrollments
// Parameters: { tournamentId: "550e8400-e29b-41d4-a716-446655440000", playerNIF: "123456789" }
//
// Command sequence (5 commands):
//   1. POST /tournaments { name: "Spring Cup", capacity: 2 }
//   2. POST /players { playerNIF: "123456789", ... }
//   3. POST /players { playerNIF: "987654321", ... }
//   4. POST /tournaments/{id}/enrollments { tournamentId: "550e...", playerNIF: "123456789" }
//   5. POST /tournaments/{id}/enrollments { tournamentId: "550e...", playerNIF: "987654321" }
//   6. POST /tournaments/{id}/enrollments { tournamentId: "550e...", playerNIF: "111111111" } <-- FAILED
//
// Discrepancies:
//   - [postcondition_failed]: enrollments.length <= capacity
//     Actual: 3 enrollments, capacity: 2
```

### Invariant Checking Across Command Sequences

Invariants are verified after EVERY command, not just at the end:

```javascript
async function verifyInvariants(stateMachine, modelState, realResponse) {
  for (const invariant of stateMachine.invariants) {
    // Check invariant on model state
    const modelHolds = evaluateInvariantOnModel(invariant, modelState)
    
    // Check invariant on real state via API calls
    const realHolds = await evaluateInvariantOnReal(invariant, realResponse, stateMachine.fastify)
    
    if (modelHolds !== realHolds) {
      return {
        type: 'invariant_divergence',
        invariant,
        modelHolds,
        realHolds
      }
    }
    
    if (!modelHolds || !realHolds) {
      return {
        type: 'invariant_violation',
        invariant,
        violatedIn: !modelHolds ? 'model' : 'real'
      }
    }
  }
  
  return null
}
```

### Integration with Schema-Driven Derivation

Stateful testing combines all previous layers:

1. **Schema-derived model structure** determines model state shape
2. **Schema-derived arbitraries** generate valid command parameters
3. **Derived preconditions** (`check()`) ensure commands are valid in current state
4. **Derived postconditions** verify real API behavior
5. **x-invariants** are checked after every command
6. **x-category** determines valid command transitions

This guarantees that stateful tests explore meaningful state spaces with valid data, catching bugs like:
- Race conditions in resource creation/deletion
- State machine violations (e.g., enrolling in full tournament)
- Missing cleanup or resource leaks
- Invariant violations across multi-step operations

## Symbolic Analysis: Deriving Properties from Contracts

Instead of requiring developers to write redundant `x-properties` and `x-stateful-test` annotations, APOPHIS derives property-based tests and stateful models directly from `x-requires`, `x-ensures`, and `x-invariants` using symbolic analysis.

### Three-Point Pipeline

```
Parser -> Validator -> Extractor
```

**1. Parser**: Parse APOSTL formulas into AST
**2. Validator**: Validate formula well-formedness and type consistency
**3. Extractor**: Extract fast-check properties and stateful models

### Example Derivation

Given:
```yaml
x-invariants:
  - for t in response_body(GET /tournaments) :-
      response_body(GET /tournaments/{t.tournamentId}/enrollments).length <=
      response_body(GET /tournaments/{t.tournamentId}/capacity)
```

**Derived fast-check property:**
```javascript
fc.property(
  fc.array(fc.record({
    tournamentId: fc.integer(),
    capacity: fc.integer({ min: 0 })
  })),
  fc.array(fc.record({
    tournamentId: fc.integer(),
    playerNIF: fc.stringMatching(/(1|2)[0-9]{8}/)
  })),
  (tournaments, enrollments) => {
    // Group enrollments by tournament
    const enrollmentCounts = {}
    for (const e of enrollments) {
      enrollmentCounts[e.tournamentId] = (enrollmentCounts[e.tournamentId] || 0) + 1
    }
    
    // Check invariant
    for (const t of tournaments) {
      const count = enrollmentCounts[t.tournamentId] || 0
      if (count > t.capacity) return false
    }
    return true
  }
)
```

**Derived stateful model:**
```javascript
class TournamentModel {
  constructor() {
    this.tournaments = new Map()
    this.enrollments = new Map()
  }

  createTournament(id, capacity) {
    this.tournaments.set(id, { id, capacity, enrollments: 0 })
  }

  enrollPlayer(tournamentId, playerNIF) {
    const tournament = this.tournaments.get(tournamentId)
    if (!tournament) return { success: false }
    if (tournament.enrollments >= tournament.capacity) {
      return { success: false }
    }
    tournament.enrollments++
    return { success: true }
  }

  checkInvariant() {
    for (const [id, tournament] of this.tournaments) {
      if (tournament.enrollments > tournament.capacity) {
        return false
      }
    }
    return true
  }
}
```

### QuickLogic Integration

APOPHIS can leverage QuickLogic3 from `~/Business/workspace/Operator/libs/QuickLogic` for advanced symbolic analysis:

```javascript
// lib/symbolic-analyzer.js
const { ESSContextQueryEngine } = require('~/Business/workspace/Operator/libs/QuickLogic/core/ContextRuntime')
const { NodeFactory } = require('~/Business/workspace/Operator/libs/QuickLogic/src/ast')

class ApophisSymbolicAnalyzer {
  constructor() {
    this.engine = new ESSContextQueryEngine()
    this.parser = new APOSTLParser()
  }

  // Parse APOSTL formula into QuickLogic AST
  parseToAST(formula) {
    const apophisAST = this.parser.parse(formula)
    return this.convertToQuickLogic(apophisAST)
  }

  // Convert APOSTL AST to QuickLogic PredicateApplication
  convertToQuickLogic(ast) {
    switch (ast.type) {
      case 'comparison':
        return NodeFactory.PredicateApplication({
          predicate: 'equals',
          args: [
            this.convertToQuickLogic(ast.left),
            this.convertToQuickLogic(ast.right)
          ]
        })
      case 'quantified':
        return NodeFactory.ForAll({
          variable: ast.variable,
          body: this.convertToQuickLogic(ast.expression)
        })
      case 'operation':
        return NodeFactory.PredicateApplication({
          predicate: ast.header,
          args: [ast.parameter]
        })
      default:
        return ast
    }
  }

  // Extract properties from contracts using QuickLogic inference
  extractProperties(contracts) {
    const properties = []
    
    for (const contract of contracts) {
      const ast = this.parseToAST(contract)
      
      // Use QuickLogic to analyze the formula
      const result = this.engine.query(ast)
      
      if (result.truthValue === 'TRUE') {
        // Extract property from proven contract
        properties.push(this.generateProperty(ast))
      } else if (result.truthValue === 'UNKNOWN') {
        // Generate questions for unresolved parts
        const questions = result.remainingQuestions
        properties.push(...this.generatePropertiesFromQuestions(questions))
      }
    }
    
    return properties
  }

  // Generate fast-check property from AST
  generateProperty(ast) {
    // Analyze AST structure to determine property type
    if (this.isInvariant(ast)) {
      return this.generateInvariantProperty(ast)
    }
    if (this.isPrecondition(ast)) {
      return this.generatePreconditionProperty(ast)
    }
    if (this.isPostcondition(ast)) {
      return this.generatePostconditionProperty(ast)
    }
    return null
  }

  // Generate stateful model from invariants
  generateStatefulModel(invariants) {
    const model = new Map()
    
    for (const invariant of invariants) {
      const ast = this.parseToAST(invariant)
      
      // Extract collection and constraint
      const collection = this.extractCollection(ast)
      const constraint = this.extractConstraint(ast)
      
      // Add to model
      model.set(collection.name, {
        type: 'collection',
        constraint: constraint,
        operations: this.deriveOperations(collection, constraint)
      })
    }
    
    return model
  }
}
```

## Implementation Phases

### Phase 1: Core Schema Extensions
- Implement `x-requires`, `x-ensures`, `x-invariants`, `x-regex`, `x-category` support
- Integrate with `@fastify/swagger` transform to preserve annotations
- Basic formula parser for simple comparisons
- Safe hook ordering (preHandler + onResponse, NOT onSend)
- Per-route opt-out via `x-validate-runtime: false`

### Phase 2: Header-Sensitive API Support
- Extend APOSTL grammar with `request_headers` and `response_headers` accessors
- Scope registry with auto-discovery from environment (`APOPHIS_SCOPE_*`)
- Automatic scope derivation from incoming request headers
- Header generation from `request_headers(this).x-foo` formulas
- Support for Arbiter/Operator header patterns

### Phase 3: Formula Safety
- Safe parameter substitution with validation and escaping
- Formula injection prevention
- Parameter completeness checking

### Phase 4: Cleanup Mechanism
- Automatic resource tracking from constructor responses
- Path-semantic inference for resource URL construction
- LIFO cleanup with scope-aware deletion
- Automatic cleanup on test completion / process exit
- Explicit `cleanup()` API for manual control

### Phase 5: PETIT Test Runner
- Path-semantic operation categorization (automatic utility detection)
- HTTP method fallback categorization
- `x-category` override support
- Strategy-based ordering
- Scope-aware test execution
- Single `test()` entry point with mode selection

### Phase 6: Symbolic Analysis
- Parser-Validator-Extractor three-point pipeline
- Derive fast-check properties from contracts
- Derive stateful models from invariants
- QuickLogic3 integration for advanced inference

### Phase 7: fast-check Integration
- Schema-to-arbitrary conversion
- Automatic edge case discovery
- Shrinking support for minimal counterexamples
- Named arbitraries for better error messages

### Phase 8: Stateful Testing
- Model-based stateful testing with derived models
- Command registration and discovery from schemas
- Invariant checking across command sequences
- Model-API synchronization verification
- Deterministic replay with seed support

### Phase 9: DX Polish
- Single `test()` with `mode` and `depth` options
- Automatic cleanup integration
- Per-route opt-out support
- Environment-based scope configuration
- Path-semantic category inference
- Better error messages with derived context

## File Structure

```
apophis-fastify/
├── lib/
│   ├── formula-parser.js           # APOSTL formula parsing and evaluation
│   ├── formula-substitutor.js      # Safe parameter substitution
│   ├── schema-extensions.js        # Schema validation and extension handling
│   ├── openapi-transform.js        # Transform for @fastify/swagger integration
│   ├── contract-validator.js       # Runtime contract validation (safe hooks)
│   ├── test-data-generator.js      # Test data generation from x-regex
│   ├── petit-runner.js             # PETIT automated test runner
│   ├── cleanup-manager.js          # Resource cleanup and rollback
│   ├── scope-registry.js           # Tenant/application scope management
│   ├── symbolic-analyzer.js        # Derive properties from contracts
│   ├── fast-check-integration.js   # Property-based testing with fast-check
│   ├── stateful-test-runner.js     # Model-based stateful testing
│   └── utils.js                    # Shared utilities
├── models/                         # Built-in stateful testing models
│   └── tournament-model.js         # Example: Tournament domain model
├── index.js                        # Main plugin entry point
├── package.json
└── README.md
```

## Dependencies

- `@fastify/swagger`: Core swagger integration
- `fastify-plugin`: Plugin wrapper for Fastify
- `randexp`: Regex-based string generation (optional)
- `fast-check`: Property-based testing framework (optional)
- `ajv`: JSON Schema validation (peer dependency via Fastify)
- `quicklogic3`: Symbolic analysis engine (optional, from Operator/libs/QuickLogic)

## Usage Example

```javascript
const fastify = require('fastify')()

// Register APOPHIS (registers @fastify/swagger automatically)
await fastify.register(require('apophis-fastify'), {
  swagger: {
    openapi: '3.0.0',
    info: { title: 'Tournaments API', version: '1.0.0' }
  },
  validateRuntime: true  // Enable runtime contract validation globally
})

// Scopes auto-derived from requests, but can be pre-registered for testing
fastify.apophis.scope.register('tenant-a', {
  tenantId: 'tenant-a',
  applicationId: 'app-1'
})

// Define routes with contracts
fastify.post('/players/:playerNIF', {
  schema: {
    'x-requires': [
      'response_code(GET /players/{playerNIF}) == 404',
      // Request header MUST be present (upset if missing)
      'request_headers(this).x-tenant-id != null',
      // Request header MUST have specific value
      'request_headers(this).content-type == "application/json"'
    ],
    'x-ensures': [
      'response_code(GET /players/{playerNIF}) == 200',
      'response_body(this) == request_body(this)',
      // Response header postcondition
      'response_headers(this).x-ledger-status == "finalized"'
    ],
    params: {
      type: 'object',
      properties: {
        playerNIF: {
          type: 'string',
          'x-regex': '(1|2)[0-9]{8}'
        }
      }
    }
  }
}, async (request, reply) => {
  // Handler implementation
})

// POST /reset auto-categorized as utility (path-semantic inference)
// No x-category override needed!
fastify.post('/reset', {
  schema: {
    'x-requires': [T],
    'x-ensures': [T]
  }
}, async (request, reply) => {
  // Reset implementation
})

// Opt-out of runtime validation for specific routes
fastify.get('/health', {
  schema: {
    'x-validate-runtime': false,  // Skip contract validation
    response: {
      200: {
        type: 'object',
        properties: {
          status: { type: 'string' }
        }
      }
    }
  }
}, async (request, reply) => {
  return { status: 'ok' }
})

// Generate OpenAPI spec with contracts
const spec = fastify.apophis.spec()
console.log(JSON.stringify(spec, null, 2))

// Single test entry point: runs contract + property + stateful tests
const results = await fastify.apophis.test({
  mode: 'all',        // 'all' | 'contract' | 'property' | 'stateful'
  depth: 'standard',  // 'quick' | 'standard' | 'thorough'
  scope: 'tenant-a',
  verbose: true
})

// Results structure:
// {
//   mode: 'all',
//   depth: 'standard',
//   contract: { passed: 45, failed: 2, ... },
//   property: { passed: 100, failed: 0, ... },
//   stateful: { passed: 20, failed: 1, sequences: [...] }
// }

// Automatic cleanup runs after tests complete (or on failure)
// Explicit cleanup if needed:
await fastify.apophis.cleanup()

await fastify.listen({ port: 3000 })
```

## Schema-Driven Derivation

APOPHIS extracts maximal testing value from standard JSON Schema and OpenAPI constructs. The `x-*` annotations provide semantic intent, but the schema itself defines the shape, constraints, and relationships of data. By driving fast-check arbitrary generation, implicit precondition/postcondition derivation, and stateful model structure directly from standard schema properties, we guarantee that generated tests are type-safe, boundary-aware, and semantically valid even when no explicit contracts are written.

### Schema-to-Arbitrary Mapping

Every JSON Schema property maps directly to a `fast-check` arbitrary. This ensures generated test data respects the API's own validation rules.

| JSON Schema Property | fast-check Arbitrary | Notes |
|---|---|---|
| `type: string` | `fc.string()` | Base arbitrary for strings |
| `minLength: n` | `.filter(s => s.length >= n)` | Applied after generation |
| `maxLength: n` | `fc.string({ maxLength: n })` | Direct fast-check support |
| `pattern: "regex"` | `fc.stringMatching(/regex/)` | Standard JSON Schema pattern (not just `x-regex`) |
| `format: email` | `fc.emailAddress()` | Semantic format → semantic arbitrary |
| `format: uuid` | `fc.uuid()` | v4 UUID generation |
| `format: date-time` | `fc.date().map(d => d.toISOString())` | ISO 8601 strings |
| `format: uri` | `fc.webUrl()` | Valid URL generation |
| `enum: ["a", "b"]` | `fc.constantFrom("a", "b")` | Exhaustive or sampled |
| `type: integer` | `fc.integer()` | Whole numbers |
| `minimum: 0` | `fc.integer({ min: 0 })` | Lower bound |
| `maximum: 100` | `fc.integer({ max: 100 })` | Upper bound |
| `exclusiveMinimum: true` + `minimum: 0` | `fc.integer({ min: 1 })` | Exclusive bounds |
| `multipleOf: 5` | `fc.integer().map(n => n * 5)` | Step values |
| `type: number` | `fc.float()` | Floating point |
| `type: boolean` | `fc.boolean()` | True/false |
| `type: array` | `fc.array(itemArb)` | Collection arbitrary |
| `minItems: 1` | `fc.array(itemArb, { minLength: 1 })` | Non-empty arrays |
| `maxItems: 10` | `fc.array(itemArb, { maxLength: 10 })` | Bounded arrays |
| `uniqueItems: true` | `.filter(arr => new Set(arr).size === arr.length)` | Set semantics |
| `type: object` + `properties` | `fc.record({ ... })` | Structured objects |
| `required: ["a", "b"]` | All required keys always present in record | Schema enforcement |
| `additionalProperties: false` | `fc.record({ ... }, { withDeletedKeys: false })` | Strict shape |
| `nullable: true` | `fc.option(arb, { nil: null })` | Null distribution |
| `default: "x"` | Bias toward default value in arbitrary | Edge case coverage |
| `readOnly: true` | Excluded from request body generation | Client cannot set |
| `writeOnly: true` | Excluded from response validation arbitrary | Server-only field |

**Implementation (`lib/schema-to-arbitrary.js`):**

```javascript
const fc = require('fast-check')

class SchemaToArbitrary {
  convert(schema, context = 'request') {
    if (schema.$ref) {
      return this.resolveRef(schema.$ref)
    }

    // Handle nullable: type can be ["string", "null"] or nullable: true
    const isNullable = schema.nullable === true || 
      (Array.isArray(schema.type) && schema.type.includes('null'))
    
    const baseArb = this.convertBaseType(schema, context)
    
    if (isNullable) {
      return fc.option(baseArb, { nil: null, freq: 5 })
    }
    
    return baseArb
  }

  convertBaseType(schema, context) {
    const type = Array.isArray(schema.type) 
      ? schema.type.find(t => t !== 'null') 
      : schema.type

    switch (type) {
      case 'string':
        return this.stringArbitrary(schema)
      case 'integer':
        return this.integerArbitrary(schema)
      case 'number':
        return this.numberArbitrary(schema)
      case 'boolean':
        return fc.boolean()
      case 'array':
        return this.arrayArbitrary(schema, context)
      case 'object':
        return this.objectArbitrary(schema, context)
      default:
        // Union types (anyOf, oneOf)
        if (schema.anyOf) {
          return fc.oneof(...schema.anyOf.map(s => this.convert(s, context)))
        }
        if (schema.oneOf) {
          return fc.oneof(...schema.oneOf.map(s => this.convert(s, context)))
        }
        return fc.anything()
    }
  }

  stringArbitrary(schema) {
    // format takes precedence over pattern
    if (schema.format) {
      switch (schema.format) {
        case 'email': return fc.emailAddress()
        case 'uuid': return fc.uuid()
        case 'date-time': return fc.date().map(d => d.toISOString())
        case 'date': return fc.date().map(d => d.toISOString().split('T')[0])
        case 'uri': return fc.webUrl()
        case 'hostname': return fc.domain()
        case 'ipv4': return fc.ipV4()
        case 'ipv6': return fc.ipV6()
      }
    }

    if (schema.pattern) {
      return fc.stringMatching(new RegExp(schema.pattern))
    }

    if (schema.x-regex) {
      return fc.stringMatching(new RegExp(schema['x-regex']))
    }

    // Handle length constraints
    const minLength = schema.minLength || 0
    const maxLength = schema.maxLength || 100
    
    if (minLength === maxLength) {
      return fc.string({ minLength, maxLength })
    }
    
    return fc.string({ minLength, maxLength })
  }

  integerArbitrary(schema) {
    const min = schema.minimum !== undefined ? schema.minimum : Number.MIN_SAFE_INTEGER
    const max = schema.maximum !== undefined ? schema.maximum : Number.MAX_SAFE_INTEGER
    
    // Handle exclusive bounds
    const effectiveMin = schema.exclusiveMinimum ? min + 1 : min
    const effectiveMax = schema.exclusiveMaximum ? max - 1 : max
    
    let arb = fc.integer({ min: effectiveMin, max: effectiveMax })
    
    if (schema.multipleOf) {
      arb = arb.map(n => Math.round(n / schema.multipleOf) * schema.multipleOf)
        .filter(n => n >= effectiveMin && n <= effectiveMax)
    }
    
    return arb
  }

  numberArbitrary(schema) {
    const min = schema.minimum !== undefined ? schema.minimum : -1e308
    const max = schema.maximum !== undefined ? schema.maximum : 1e308
    
    let arb = fc.float({ min, max })
    
    if (schema.multipleOf) {
      arb = arb.map(n => Math.round(n / schema.multipleOf) * schema.multipleOf)
    }
    
    return arb
  }

  arrayArbitrary(schema, context) {
    const itemArb = schema.items 
      ? this.convert(schema.items, context) 
      : fc.anything()
    
    const minItems = schema.minItems || 0
    const maxItems = schema.maxItems || 10
    
    let arb = fc.array(itemArb, { minLength: minItems, maxLength: maxItems })
    
    if (schema.uniqueItems) {
      arb = arb.filter(arr => new Set(arr).size === arr.length)
    }
    
    return arb
  }

  objectArbitrary(schema, context) {
    const properties = {}
    const required = new Set(schema.required || [])
    
    for (const [key, propSchema] of Object.entries(schema.properties || {})) {
      // Skip readOnly properties in request context, writeOnly in response context
      if (context === 'request' && propSchema.readOnly) continue
      if (context === 'response' && propSchema.writeOnly) continue
      
      properties[key] = this.convert(propSchema, context)
    }
    
    // Handle additionalProperties
    const withDeletedKeys = schema.additionalProperties === false 
      ? false 
      : true
    
    return fc.record(properties, { 
      withDeletedKeys,
      requiredKeys: Array.from(required) 
    })
  }

  resolveRef(refPath) {
    // Resolve $ref against OpenAPI components/schemas
    return this.refResolver.resolve(refPath)
  }
}
```

### Implicit Precondition Derivation

Standard schema properties encode preconditions that APOPHIS can extract automatically. These augment explicit `x-requires` annotations.

| Schema Property | Derived Precondition | APOSTL Formula Equivalent |
|---|---|---|
| `required: ["field"]` | Field must be present in request | `request_body(this).field != null` |
| `type: string` on param | Parameter must be string | `typeof request_body(this).field == "string"` |
| `format: email` | Must match email format | `request_body(this).field matches "^[^@]+@[^@]+$"` |
| `minimum: 0` | Must be non-negative | `request_body(this).field >= 0` |
| `enum: ["a", "b"]` | Must be one of allowed values | `request_body(this).field == "a" \|\| request_body(this).field == "b"` |
| `readOnly: true` on property | Must NOT be present in request | `request_body(this).field == null` |
| `maxLength: 255` | Must not exceed length | `request_body(this).field.length <= 255` |
| `pattern: "^[A-Z]+$"` | Must match pattern | `request_body(this).field matches "^[A-Z]+$"` |

**Example - Full Schema with Derived Preconditions:**

```yaml
paths:
  /players/{playerNIF}:
    post:
      parameters:
        - name: playerNIF
          in: path
          required: true
          schema:
            type: string
            pattern: "^(1|2)[0-9]{8}$"
      requestBody:
        content:
          application/json:
            schema:
              type: object
              required: [firstName, lastName, email]
              properties:
                firstName:
                  type: string
                  minLength: 1
                  maxLength: 100
                lastName:
                  type: string
                  minLength: 1
                  maxLength: 100
                email:
                  type: string
                  format: email
                age:
                  type: integer
                  minimum: 0
                  maximum: 150
                  nullable: true
                role:
                  type: string
                  enum: [player, coach, referee]
                  default: player
                createdAt:
                  type: string
                  format: date-time
                  readOnly: true
```

**Derived preconditions (automatically added to `x-requires`):**

```javascript
// From path parameter
'request_body(this).playerNIF matches "^(1|2)[0-9]{8}$"'

// From required fields
'request_body(this).firstName != null'
'request_body(this).lastName != null'  
'request_body(this).email != null'

// From type constraints
'typeof request_body(this).firstName == "string"'
'typeof request_body(this).age == "integer" || request_body(this).age == null'

// From format constraints
'request_body(this).email matches "^[^@]+@[^@]+$"'

// From length constraints
'request_body(this).firstName.length >= 1'
'request_body(this).firstName.length <= 100'

// From numeric bounds
'request_body(this).age >= 0 || request_body(this).age == null'
'request_body(this).age <= 150 || request_body(this).age == null'

// From enum
'request_body(this).role == "player" || request_body(this).role == "coach" || request_body(this).role == "referee"'

// From readOnly (MUST NOT be sent by client)
'request_body(this).createdAt == null'
```

### Implicit Postcondition Derivation

Response schemas implicitly define postconditions about the shape and constraints of returned data.

| Schema Property | Derived Postcondition | APOSTL Formula Equivalent |
|---|---|---|
| `type: object` with `properties` | Response has expected shape | `response_body(this).field != null` (for required) |
| `readOnly: true` | Field preserved from creation | `response_body(this).field == previous(response_body(this).field)` |
| `format: uuid` on response | Returned ID is valid UUID | `response_body(this).id matches "^[0-9a-f-]{36}$"` |
| `nullable: false` | Field must be present | `response_body(this).field != null` |
| `writeOnly: true` | Field must NOT appear in response | `response_body(this).password == null` |
| `default: "x"` | If not set, defaults to x | `response_body(this).status == "x"` (when not explicitly set) |

### Model Structure Derivation

The schema topology itself defines the stateful model's structure, resource graph, and valid state transitions.

**Resource Graph from Schema Relationships:**

```yaml
components:
  schemas:
    Tournament:
      type: object
      properties:
        tournamentId:
          type: string
          format: uuid
          readOnly: true
        name:
          type: string
        capacity:
          type: integer
          minimum: 1
        enrollments:
          type: array
          items:
            $ref: '#/components/schemas/Enrollment'
          readOnly: true
        organizer:
          $ref: '#/components/schemas/Player'
          
    Enrollment:
      type: object
      properties:
        playerNIF:
          type: string
          pattern: "^(1|2)[0-9]{8}$"
        tournamentId:
          type: string
          format: uuid
        status:
          type: string
          enum: [pending, confirmed, cancelled]
          default: pending
```

**Derived stateful model:**

```javascript
class TournamentModel {
  constructor() {
    // From schema properties + types
    this.tournaments = new Map() // tournamentId -> Tournament
    this.enrollments = new Map() // compositeKey -> Enrollment
    this.players = new Map() // playerNIF -> Player
    
    // Track relationships implied by schema structure
    this.tournamentEnrollments = new Map() // tournamentId -> Set<playerNIF>
  }

  // Constructor derived from POST /tournaments schema
  createTournament(name, capacity, organizerNIF) {
    // Implicit precondition: capacity >= 1 (from minimum: 1)
    if (capacity < 1) return { success: false, error: 'capacity < 1' }
    
    // Implicit precondition: organizer must exist (from $ref relationship)
    if (!this.players.has(organizerNIF)) return { success: false, error: 'organizer not found' }
    
    const tournamentId = generateUUID() // from format: uuid
    this.tournaments.set(tournamentId, {
      tournamentId,
      name,
      capacity,
      organizer: organizerNIF,
      enrollments: [], // derived from array property
      status: 'active'
    })
    this.tournamentEnrollments.set(tournamentId, new Set())
    
    return { success: true, tournamentId }
  }

  // Mutator derived from POST /tournaments/{id}/enrollments
  enrollPlayer(tournamentId, playerNIF) {
    // Implicit precondition: tournament exists (from path param reference)
    if (!this.tournaments.has(tournamentId)) return { success: false, error: 'tournament not found' }
    
    // Implicit precondition: player exists (from $ref: '#/components/schemas/Player')
    if (!this.players.has(playerNIF)) return { success: false, error: 'player not found' }
    
    const tournament = this.tournaments.get(tournamentId)
    const currentEnrollments = this.tournamentEnrollments.get(tournamentId)
    
    // Invariant derived from x-invariants or schema constraints
    if (currentEnrollments.size >= tournament.capacity) {
      return { success: false, error: 'tournament full' }
    }
    
    // Implicit postcondition: enrollment status defaults to "pending"
    const enrollment = {
      playerNIF,
      tournamentId,
      status: 'pending' // from default: pending
    }
    
    this.enrollments.set(`${tournamentId}:${playerNIF}`, enrollment)
    currentEnrollments.add(playerNIF)
    tournament.enrollments.push(enrollment)
    
    return { success: true, enrollment }
  }

  // Observer derived from GET /tournaments/{id}
  getTournament(tournamentId) {
    return this.tournaments.get(tournamentId) || null
  }

  // Invariant check derived from schema + x-invariants
  checkInvariants() {
    for (const [id, tournament] of this.tournaments) {
      // Schema-derived: capacity must be >= 1
      if (tournament.capacity < 1) return false
      
      // Schema-derived: tournamentId must be UUID format
      if (!isValidUUID(tournament.tournamentId)) return false
      
      // x-invariant-derived: enrollments <= capacity
      const enrollmentCount = this.tournamentEnrollments.get(id).size
      if (enrollmentCount > tournament.capacity) return false
    }
    return true
  }
}
```

### Semantic Hint Extraction

Descriptions and examples provide testing guidance:

| Source | Extraction | Testing Use |
|---|---|---|
| `description: "Player's fiscal identification number"` | Field semantic meaning | Better error messages, named arbitraries |
| `example: "123456789"` | Concrete valid value | Seed for fast-check, baseline test case |
| `description: "Must be unique within tournament"` | Uniqueness constraint | Implicit postcondition / model invariant |
| `description: "Automatically set on creation"` | readOnly semantic | Skip in request generation |

**Named Arbitraries from Descriptions:**

```javascript
// Instead of anonymous fc.string(), generate named arbitraries:
fc.string().map(s => ({ value: s, _name: 'playerNIF' }))

// This enables better shrinking messages:
// "Property failed with playerNIF = 'abc' (must match /^(1|2)[0-9]{8}$/)"
```

### Integration: Layered Derivation

APOPHIS combines standard schema derivation with explicit APOSTL contracts in layers:

```
Layer 1: Standard JSON Schema
  → Type-safe arbitrary generation
  → Basic preconditions (required, type, format)
  → Model structure ($ref, array relationships)

Layer 2: x-regex annotations
  → Refined arbitrary generation (regex instead of format)
  → Edge case generation (boundary values from regex)

Layer 3: x-requires / x-ensures
  → Semantic pre/postconditions
  → Cross-resource conditions
  → Header and state conditions

Layer 4: x-invariants
  → Model invariants
  → Stateful property generation

Layer 5: x-category
  → Operation classification for test ordering
```

**Complete Example - All Layers Combined:**

```yaml
paths:
  /tournaments/{tournamentId}/enrollments:
    post:
      x-category: constructor
      x-requires:
        # Layer 3: Semantic preconditions
        - response_body(GET /tournaments/{tournamentId}) != null
      x-ensures:
        # Layer 3: Semantic postconditions
        - response_code(this) == 201
        - response_body(this).status == "pending"
      parameters:
        - name: tournamentId
          in: path
          required: true
          schema:
            type: string
            format: uuid  # Layer 1: Type constraint
      requestBody:
        content:
          application/json:
            schema:
              type: object
              required: [playerNIF]  # Layer 1: Required field
              properties:
                playerNIF:
                  type: string
                  x-regex: "(1|2)[0-9]{8}"  # Layer 2: Refined generation
                  description: "Player fiscal ID"
                notes:
                  type: string
                  maxLength: 500  # Layer 1: Length constraint
                  nullable: true
```

**Derived test artifacts:**

```javascript
// Layer 1: Standard schema arbitrary
const enrollmentRequestArb = fc.record({
  playerNIF: fc.string(), // Base type constraint
  notes: fc.option(fc.string({ maxLength: 500 }), { nil: null })
}, { 
  requiredKeys: ['playerNIF'] // required field enforcement
})

// Layer 2: x-regex refines the arbitrary
const refinedArb = fc.record({
  playerNIF: fc.stringMatching(/(1|2)[0-9]{8}/), // Refined by x-regex
  notes: fc.option(fc.string({ maxLength: 500 }), { nil: null })
}, { 
  requiredKeys: ['playerNIF']
})

// Layer 1+3: Derived preconditions
const preconditions = [
  'request_body(this).playerNIF != null',        // from required
  'typeof request_body(this).playerNIF == "string"', // from type
  'request_body(this).notes.length <= 500 || request_body(this).notes == null', // from maxLength + nullable
  'response_body(GET /tournaments/{tournamentId}) != null' // from x-requires
]

// Layer 1+3: Derived postconditions
const postconditions = [
  'response_code(this) == 201',                    // from x-ensures
  'response_body(this).status == "pending"',       // from x-ensures
  'typeof response_body(this).playerNIF == "string"', // from response schema type
  'response_body(this).playerNIF matches "^(1|2)[0-9]{8}$"' // from x-regex on response
]

// Layer 4+5: Derived stateful model
class EnrollmentStatefulModel {
  constructor() {
    this.tournaments = new Map()
    this.enrollments = new Map() // tournamentId -> Map<playerNIF, enrollment>
  }

  createEnrollment(tournamentId, playerNIF, notes) {
    // Layer 3: Explicit precondition
    if (!this.tournaments.has(tournamentId)) return { success: false }
    
    // Layer 1: Schema-derived model structure
    const enrollment = {
      playerNIF,
      notes,
      status: 'pending', // from x-ensures
      tournamentId
    }
    
    if (!this.enrollments.has(tournamentId)) {
      this.enrollments.set(tournamentId, new Map())
    }
    this.enrollments.get(tournamentId).set(playerNIF, enrollment)
    
    return { success: true, enrollment }
  }
}

// fast-check property combining all layers
fc.assert(
  fc.property(
    fc.uuid(), // tournamentId from format: uuid
    fc.stringMatching(/(1|2)[0-9]{8}/), // playerNIF from x-regex
    fc.option(fc.string({ maxLength: 500 }), { nil: null }), // notes from schema
    (tournamentId, playerNIF, notes) => {
      // Execute API call (injected request)
      // Verify all preconditions + postconditions
      // Check model synchronization
    }
  )
)
```

### Guarantees of Schema-Driven Derivation

By deriving from standard schema:

1. **No false positives from type mismatches**: Generated data always passes Fastify's own JSON Schema validation
2. **Boundary coverage**: `minimum`, `maximum`, `minLength`, `maxLength` ensure edge cases are tested
3. **Semantic validity**: `format`, `pattern`, `enum` guarantee data makes business sense
4. **Relationship integrity**: `$ref`, array `items` build correct resource graphs in models
5. **Reduced annotation burden**: APIs with good schemas need fewer `x-*` annotations to be fully testable
6. **Schema drift detection**: If schema changes, derived tests automatically adapt

## Future Extensions

- **RAML Support**: Extend beyond OpenAPI to RAML specifications
- **GraphQL**: Adapt contract concepts to GraphQL schemas
- **Mutation Testing**: Verify contract completeness
- **Performance Contracts**: Add latency and throughput requirements
- **Visual Testing**: Contract-based screenshot comparison for UI APIs
- **Chaos Engineering**: Inject failures based on contract boundaries

## References

- Ribeiro, A.C.M. (2021). "Invariant-Driven Automated Testing". MSc Thesis, NOVA University of Lisbon.
- APOSTL: API PrOperty SpecificaTion Language
- PETIT: aPi tEsTIng Tool
- OpenAPI Specification v3.0
- Fastify Plugin Architecture
- Design by Contract (Meyer, 1988)
- Hoare Logic (Hoare, 1969)
- QuickLogic3: Contextual Four-Valued Reasoning Runtime