# NEXT_STEPS_423.md — Object Inference, Request Structure & Logic/Invariants

## Executive Summary

APOPHIS currently tests routes in isolation with naive resource tracking and no request structure awareness. For Arbiter (11K routes, multi-tenant auth server), we need:

1. **Object Inference**: Schema-driven resource extraction with parent-child relationships
2. **Request Structure**: Path/body/query/header discrimination based on route schemas
3. **Logic/Invariants**: Cross-route temporal assertions, authorization boundaries, state consistency

**Timeline**: 2-3 weeks for core implementation, 1 week for Arbiter-specific invariants
**Impact**: 10-100x more bugs caught, especially authorization leaks and invalid state transitions

---

## 1. OBJECT INFERENCE

### 1.1 Current State (Naive)

**File**: `src/test/petit-runner.ts:205-223`

```typescript
const updateState = (command: ApiCommand, ctx: EvalContext, state: ModelState): ModelState => {
  if (command.route.category !== 'constructor') return state

  const body = ctx.response.body as Record<string, unknown> | undefined
  if (body === undefined) return state

  const id = body.id ?? body.uuid ?? body._id
  if (id === undefined) return state

  const resourceType = command.route.path.split('/').filter(Boolean).pop() ?? 'resource'
  // ... stores flat resource
}
```

**Problems**:
- Only looks for `id`/`uuid`/`_id` in response body
- Resource type = last path segment (e.g., `POST /tenant/applications` → type=`applications`)
- No parent tracking (application is scoped to tenant)
- No nested resource support (e.g., `/tenants/:id/applications/:appId/rules`)
- No schema-driven identity field detection

### 1.2 Required: Schema-Driven Resource Extraction

**New File**: `src/domain/resource-inference.ts`

```typescript
interface ResourceIdentity {
  resourceType: string
  id: string
  parentType?: string
  parentId?: string
  tenantId?: string
  applicationId?: string
  scope: string | null
}

interface ResourceSchema {
  identityField: string           // e.g., 'id', 'appId', 'tenantId'
  parentField?: string            // e.g., 'tenantId' for applications
  identityPattern?: string        // e.g., '^[a-z]+-[0-9]+$'
  scopeFields: string[]          // e.g., ['tenantId', 'applicationId']
}

export const extractResourceIdentity = (
  route: RouteContract,
  responseBody: unknown,
  responseSchema?: Record<string, unknown>
): ResourceIdentity | null => {
  // 1. Determine identity field from schema
  //    - Look for field named 'id', 'uuid', '_id', or ending in 'Id'
  //    - Prefer schema.required fields
  //    - Use schema.pattern if available for validation
  
  // 2. Determine resource type from route path
  //    - /tenants/:id/applications → type='application', parent='tenant'
  //    - /oauth/token → type='token' (special case)
  //    - /graph/nodes/:nodeId/relations → type='relation', parent='node'
  
  // 3. Extract parent from response body (e.g., body.tenantId)
  //    or from route path params (e.g., :id in /tenants/:id/applications)
  
  // 4. Extract scope (tenantId, applicationId) from response or request headers
}

export const inferResourceHierarchy = (path: string): {
  resourceType: string
  parentType?: string
  isNested: boolean
} => {
  const segments = path.split('/').filter(Boolean)
  // e.g., ['tenants', ':id', 'applications', ':appId']
  // resourceType = 'application', parentType = 'tenant'
  
  // Special cases:
  // /oauth/token → resourceType='token', no parent
  // /graph/nodes/:nodeId/relations → resourceType='relation', parentType='node'
  // /authz/evaluate → not a resource (utility)
}
```

**File to Modify**: `src/types.ts`

Add to `ModelState`:
```typescript
export interface ResourceHierarchy {
  readonly id: string
  readonly type: string
  readonly parentId?: string
  readonly parentType?: string
  readonly scope: {
    readonly tenantId?: string
    readonly applicationId?: string
  }
  readonly data: unknown
  readonly createdAt: number
}

export interface ModelState {
  readonly resources: ReadonlyMap<string, ReadonlyMap<string, ResourceHierarchy>>
  readonly counters: ReadonlyMap<string, number>
  readonly relationships: ReadonlyMap<string, ReadonlyArray<{ from: string; to: string; type: string }>>
}
```

### 1.3 Arbiter-Specific Resource Types

**File**: `src/domain/arbiter-resources.ts` (new)

```typescript
// Arbiter has specific resource hierarchies we need to understand

export const ARBITER_RESOURCE_PATTERNS = {
  // Tenant hierarchy
  'POST /tenants': { type: 'tenant', identityField: 'id' },
  'POST /tenants/:id/applications': { 
    type: 'application', 
    identityField: 'id',
    parentType: 'tenant',
    parentField: 'tenantId'
  },
  'POST /tenants/:id/users': {
    type: 'user',
    identityField: 'id', 
    parentType: 'tenant',
    parentField: 'tenantId'
  },
  
  // Graph resources
  'POST /graph/nodes': { type: 'node', identityField: 'id' },
  'POST /graph/nodes/:id/relations': {
    type: 'relation',
    identityField: 'id',
    parentType: 'node',
    parentField: 'sourceId'
  },
  
  // OAuth tokens
  'POST /oauth/token': { type: 'token', identityField: 'access_token' },
  'POST /oauth/refresh': { type: 'token', identityField: 'access_token' },
  
  // Sessions
  'POST /sessions': { type: 'session', identityField: 'id' },
  
  // Permissions
  'POST /authz/grants': { type: 'grant', identityField: 'id' },
  
  // Rules
  'POST /tenants/:id/applications/:appId/rules': {
    type: 'rule',
    identityField: 'id',
    parentType: 'application',
    parentField: 'applicationId'
  }
} as const

export const isArbiterResource = (method: string, path: string): boolean => {
  const key = `${method} ${path}`
  return key in ARBITER_RESOURCE_PATTERNS
}
```

### 1.4 Enhanced State Updates

**File**: `src/test/petit-runner.ts` — Replace `updateState` and `makeResource`

```typescript
const updateState = (command: ApiCommand, ctx: EvalContext, state: ModelState): ModelState => {
  if (command.route.category !== 'constructor') return state

  const body = ctx.response.body as Record<string, unknown> | undefined
  if (body === undefined) return state

  const identity = extractResourceIdentity(command.route, body, command.route.schema?.response as Record<string, unknown>)
  if (!identity) return state

  const hierarchy: ResourceHierarchy = {
    id: identity.id,
    type: identity.resourceType,
    parentId: identity.parentId,
    parentType: identity.parentType,
    scope: {
      tenantId: identity.tenantId,
      applicationId: identity.applicationId
    },
    data: body,
    createdAt: Date.now()
  }

  // Store in typed resource map
  const existing = state.resources.get(identity.resourceType) ?? new Map<string, ResourceHierarchy>()
  const updated = new Map(existing)
  updated.set(identity.id, hierarchy)

  const newResources = new Map(state.resources)
  newResources.set(identity.resourceType, updated)

  // Track relationships if present
  let newRelationships = state.relationships
  if (identity.parentId && identity.parentType) {
    const rels = state.relationships.get(identity.resourceType) ?? []
    newRelationships = new Map(state.relationships)
    newRelationships.set(identity.resourceType, [
      ...rels,
      { from: identity.id, to: identity.parentId, type: 'childOf' }
    ])
  }

  return { ...state, resources: newResources, relationships: newRelationships }
}
```

### 1.5 Test Cases

**New File**: `src/test/resource-inference.test.ts`

```typescript
test('extracts tenant resource from POST /tenants', () => {
  const route = makeRoute('POST', '/tenants')
  const body = { id: 'tenant-123', name: 'Acme' }
  const identity = extractResourceIdentity(route, body)
  
  assert.strictEqual(identity?.resourceType, 'tenant')
  assert.strictEqual(identity?.id, 'tenant-123')
  assert.strictEqual(identity?.parentType, undefined)
})

test('extracts nested application with parent tenant', () => {
  const route = makeRoute('POST', '/tenants/:id/applications')
  const body = { id: 'app-456', tenantId: 'tenant-123', name: 'My App' }
  const identity = extractResourceIdentity(route, body)
  
  assert.strictEqual(identity?.resourceType, 'application')
  assert.strictEqual(identity?.id, 'app-456')
  assert.strictEqual(identity?.parentType, 'tenant')
  assert.strictEqual(identity?.parentId, 'tenant-123')
})

test('extracts OAuth token with access_token identity', () => {
  const route = makeRoute('POST', '/oauth/token')
  const body = { access_token: 'tok-789', token_type: 'Bearer' }
  const identity = extractResourceIdentity(route, body)
  
  assert.strictEqual(identity?.resourceType, 'token')
  assert.strictEqual(identity?.id, 'tok-789')
})

test('returns null for non-resource routes', () => {
  const route = makeRoute('GET', '/health')
  const body = { status: 'ok' }
  const identity = extractResourceIdentity(route, body)
  
  assert.strictEqual(identity, null)
})

test('uses schema to find identity field', () => {
  const route = makeRoute('POST', '/custom/resources', {
    response: {
      type: 'object',
      properties: {
        resourceId: { type: 'string' },
        name: { type: 'string' }
      },
      required: ['resourceId']
    }
  })
  const body = { resourceId: 'res-999', name: 'Test' }
  const identity = extractResourceIdentity(route, body, route.schema?.response as Record<string, unknown>)
  
  assert.strictEqual(identity?.id, 'res-999')
})
```

---

## 2. REQUEST STRUCTURE INFERENCE

### 2.1 Current State (Blind Parameter Passing)

**File**: `src/test/petit-runner.ts:111-168`

```typescript
const executeCommand = async (fastify: FastifyInstance, command: ApiCommand): Promise<EvalContext> => {
  const method = command.route.method
  let url = command.route.path

  // Replace path params with generated values
  const params = command.params
  for (const [key, value] of Object.entries(params)) {
    if (url.includes(`:${key}`)) {
      url = url.replace(`:${key}`, String(value))
    }
  }

  // Everything else goes to query (GET/DELETE) or body (others)
  const queryParams: Record<string, string> = {}
  const bodyParams: Record<string, unknown> = {}

  for (const [key, value] of Object.entries(params)) {
    if (!command.route.path.includes(`:${key}`)) {
      if (method === 'GET' || method === 'DELETE') {
        queryParams[key] = String(value)
      } else {
        bodyParams[key] = value
      }
    }
  }
  // ...
}
```

**Problems**:
- Assumes ALL non-path params are body params for POST/PUT/PATCH
- No understanding of `body.properties` from schema
- No handling of nested body structures (`body.nested.field`)
- No automatic header injection (x-tenant-id, authorization)
- No content-type negotiation
- Query params for GET/DELETE are just dumped as-is

### 2.2 Required: Schema-Aware Request Building

**New File**: `src/domain/request-builder.ts`

```typescript
interface RequestStructure {
  method: string
  url: string                    // With path params replaced
  headers: Record<string, string>
  query?: Record<string, string>
  body?: unknown
  contentType?: string
}

interface RouteParamSchema {
  pathParams: string[]          // e.g., ['tenantId', 'appId']
  bodySchema?: Record<string, unknown>
  querySchema?: Record<string, unknown>
  headerRequirements: string[]   // e.g., ['x-tenant-id', 'authorization']
}

export const parseRouteParams = (path: string): string[] => {
  const params: string[] = []
  const segments = path.split('/')
  for (const segment of segments) {
    if (segment.startsWith(':')) {
      params.push(segment.slice(1))
    } else if (segment.startsWith('{') && segment.endsWith('}')) {
      params.push(segment.slice(1, -1))
    }
  }
  return params
}

export const buildRequest = (
  route: RouteContract,
  generatedData: Record<string, unknown>,
  scopeHeaders: Record<string, string>,
  state: ModelState
): RequestStructure => {
  const pathParams = parseRouteParams(route.path)
  const url = substitutePathParams(route.path, generatedData, state)
  
  // Extract body params from schema
  const bodySchema = route.schema?.body as Record<string, unknown> | undefined
  const body = bodySchema 
    ? extractBodyParams(generatedData, bodySchema)
    : undefined
  
  // Extract query params from schema
  const querySchema = route.schema?.querystring as Record<string, unknown> | undefined
  const query = querySchema
    ? extractQueryParams(generatedData, querySchema)
    : extractRemainingParams(generatedData, pathParams, body)
  
  // Build headers
  const headers = buildHeaders(route, scopeHeaders, generatedData, state)
  
  // Determine content type
  const contentType = body ? 'application/json' : undefined
  
  return { method: route.method, url, headers, query, body, contentType }
}

const substitutePathParams = (
  path: string, 
  data: Record<string, unknown>,
  state: ModelState
): string => {
  let url = path
  const pathParams = parseRouteParams(path)
  
  for (const param of pathParams) {
    let value = data[param]
    
    // If param is an ID reference, try to find it in state
    if (value === undefined && param.endsWith('Id')) {
      const resourceType = param.replace(/Id$/, '')
      const resources = state.resources.get(resourceType)
      if (resources && resources.size > 0) {
        // Pick a random existing resource
        const ids = Array.from(resources.keys())
        value = ids[Math.floor(Math.random() * ids.length)]
      }
    }
    
    if (value !== undefined) {
      url = url.replace(`:${param}`, String(value))
    }
  }
  
  return url
}

const extractBodyParams = (
  data: Record<string, unknown>,
  bodySchema: Record<string, unknown>
): Record<string, unknown> => {
  const properties = bodySchema.properties as Record<string, Record<string, unknown>> | undefined
  if (!properties) return data
  
  const body: Record<string, unknown> = {}
  for (const key of Object.keys(properties)) {
    if (key in data) {
      body[key] = data[key]
    }
  }
  
  // Handle nested objects
  for (const [key, propSchema] of Object.entries(properties)) {
    if (propSchema.type === 'object' && propSchema.properties) {
      body[key] = extractBodyParams(data, propSchema)
    }
  }
  
  return body
}

const buildHeaders = (
  route: RouteContract,
  scopeHeaders: Record<string, string>,
  data: Record<string, unknown>,
  state: ModelState
): Record<string, string> => {
  const headers: Record<string, string> = { ...scopeHeaders }
  
  // Auto-inject tenant ID if route requires it
  if (route.requires.some(r => r.includes('x-tenant-id'))) {
    const tenantId = data['tenantId'] || scopeHeaders['x-tenant-id']
    if (tenantId) {
      headers['x-tenant-id'] = String(tenantId)
    }
  }
  
  // Auto-inject authorization if required
  if (route.requires.some(r => r.includes('authorization'))) {
    // Could look up session/token from state
    const tokens = state.resources.get('token')
    if (tokens && tokens.size > 0) {
      const token = Array.from(tokens.values())[0]
      headers['authorization'] = `Bearer ${token.id}`
    }
  }
  
  // Content-Type for body requests
  if (route.schema?.body) {
    headers['content-type'] = 'application/json'
  }
  
  return headers
}
```

### 2.3 Enhanced Execution

**File**: `src/test/petit-runner.ts` — Replace `executeCommand`

```typescript
const executeCommand = async (
  fastify: FastifyInstance,
  command: ApiCommand,
  state: ModelState
): Promise<EvalContext> => {
  const request = buildRequest(command.route, command.params, command.headers, state)
  
  // Build query string
  const queryString = request.query
    ? Object.entries(request.query)
        .map(([k, v]) => `${encodeURIComponent(k)}=${encodeURIComponent(v)}`)
        .join('&')
    : ''
  
  const fullUrl = queryString ? `${request.url}?${queryString}` : request.url
  
  const response = await fastify.inject({
    method: request.method,
    url: fullUrl,
    payload: request.body,
    headers: request.headers
  })

  return {
    request: {
      body: request.body,
      headers: request.headers,
      query: request.query || {},
      params: extractPathParams(command.route.path, request.url)
    },
    response: {
      body: response.json(),
      headers: Object.fromEntries(
        Object.entries(response.headers).map(([k, v]) => [k, String(v)])
      ),
      statusCode: response.statusCode
    }
  }
}
```

### 2.4 Arbiter-Specific Request Patterns

**File**: `src/domain/arbiter-requests.ts` (new)

```typescript
// Arbiter has specific request structure patterns

export const ARBITER_REQUEST_PATTERNS = {
  'POST /oauth/token': {
    bodyFields: ['grant_type', 'code', 'refresh_token', 'client_id', 'client_secret'],
    headerFields: ['authorization'],
    contentType: 'application/x-www-form-urlencoded'
  },
  
  'POST /oauth/authorize': {
    queryFields: ['client_id', 'response_type', 'redirect_uri', 'scope', 'state'],
    headerFields: ['cookie']
  },
  
  'POST /tenant/applications': {
    bodyFields: ['name', 'slug', 'description', 'callbackURLs', 'allowedOrigins'],
    headerFields: ['x-tenant-id', 'authorization'],
    pathParams: []  // No path params, tenant from header
  },
  
  'GET /tenant/applications/:appId': {
    pathParams: ['appId'],
    headerFields: ['x-tenant-id', 'authorization']
  },
  
  'POST /tenants/:tenantId/applications/:appId/rules': {
    pathParams: ['tenantId', 'appId'],
    bodyFields: ['dsl', 'priority', 'enabled'],
    headerFields: ['x-tenant-id', 'authorization']
  },
  
  'POST /graph/nodes/:nodeId/relations': {
    pathParams: ['nodeId'],
    bodyFields: ['targetId', 'relationType', 'metadata'],
    headerFields: ['x-tenant-id', 'authorization']
  },
  
  'POST /authz/evaluate': {
    bodyFields: ['userId', 'resourceId', 'permission', 'context'],
    headerFields: ['x-tenant-id', 'authorization']
  }
} as const

export const getArbiterRequestPattern = (method: string, path: string) => {
  const key = `${method} ${path}`
  return ARBITER_REQUEST_PATTERNS[key as keyof typeof ARBITER_REQUEST_PATTERNS]
}
```

### 2.5 Test Cases

**New File**: `src/test/request-builder.test.ts`

```typescript
test('builds request with path params substituted', () => {
  const route = makeRoute('GET', '/users/:id')
  const data = { id: 'user-123' }
  const request = buildRequest(route, data, {}, emptyState())
  
  assert.strictEqual(request.url, '/users/user-123')
})

test('builds request with body from schema', () => {
  const route = makeRoute('POST', '/users', {
    body: {
      type: 'object',
      properties: {
        name: { type: 'string' },
        email: { type: 'string' }
      }
    }
  })
  const data = { name: 'John', email: 'john@example.com', extra: 'ignored' }
  const request = buildRequest(route, data, {}, emptyState())
  
  assert.deepStrictEqual(request.body, { name: 'John', email: 'john@example.com' })
  assert.strictEqual(request.body?.extra, undefined)
})

test('injects tenant ID from scope headers', () => {
  const route = makeRoute('GET', '/tenant/applications', {
    'x-requires': ['request_headers(this).x-tenant-id != null']
  })
  const scopeHeaders = { 'x-tenant-id': 'tenant-123' }
  const request = buildRequest(route, {}, scopeHeaders, emptyState())
  
  assert.strictEqual(request.headers['x-tenant-id'], 'tenant-123')
})

test('looks up path param from state if not in data', () => {
  const route = makeRoute('GET', '/users/:userId')
  const state = stateWithResource('user', 'user-456', {})
  const request = buildRequest(route, {}, {}, state)
  
  assert.strictEqual(request.url, '/users/user-456')
})

test('handles OAuth token request with form encoding', () => {
  const route = makeRoute('POST', '/oauth/token')
  const data = { 
    grant_type: 'authorization_code',
    code: 'auth-code-123',
    client_id: 'client-456'
  }
  const request = buildRequest(route, data, {}, emptyState())
  
  assert.strictEqual(request.headers['content-type'], 'application/x-www-form-urlencoded')
  assert.strictEqual(request.body, undefined)  // Form data handled differently
})
```

---

## 3. LOGIC & INVARIANTS

### 3.1 Current State (Status Code Only)

**File**: `src/test/petit-runner.ts:186-199`

```typescript
const checkPostconditions = (command: ApiCommand, ctx: EvalContext): EvalResult => {
  for (const ensure of command.route.ensures) {
    if (ensure.startsWith('status:')) {
      const expected = parseInt(ensure.replace('status:', ''), 10)
      if (ctx.response.statusCode !== expected) {
        return { success: false, error: `Expected status ${expected}, got ${ctx.response.statusCode}` }
      }
    }
  }
  return { success: true, value: ctx.response.statusCode }
}
```

**Problems**:
- Only checks `status:###` patterns
- Ignores actual APOSTL formulas in `x-ensures`
- No cross-route invariant checking
- No temporal logic (what happens after state changes)
- No authorization boundary verification

### 3.2 Required: Full Formula Evaluation

**File**: `src/test/petit-runner.ts` — Replace `checkPostconditions`

```typescript
import { parse } from '../formula/parser.js'
import { evaluateBooleanResult } from '../formula/evaluator.js'

const checkPostconditions = (command: ApiCommand, ctx: EvalContext): EvalResult => {
  for (const ensure of command.route.ensures) {
    // Legacy status check
    if (ensure.startsWith('status:')) {
      const expected = parseInt(ensure.replace('status:', ''), 10)
      if (ctx.response.statusCode !== expected) {
        return { 
          success: false, 
          error: `Expected status ${expected}, got ${ctx.response.statusCode}` 
        }
      }
      continue
    }
    
    // Full APOSTL formula evaluation
    try {
      const ast = parse(ensure)
      const result = evaluateBooleanResult(ast.ast, ctx)
      if (!result) {
        return { 
          success: false, 
          error: `Contract violation: ${ensure}` 
        }
      }
    } catch (err) {
      return {
        success: false,
        error: `Formula error in "${ensure}": ${err instanceof Error ? err.message : String(err)}`
      }
    }
  }
  return { success: true, value: ctx.response.statusCode }
}
```

### 3.3 Required: Cross-Route Invariant Registry

**New File**: `src/domain/invariant-registry.ts`

```typescript
interface Invariant {
  readonly name: string
  readonly description: string
  readonly check: (state: ModelState, history: ReadonlyArray<EvalContext>) => InvariantResult
}

interface InvariantResult {
  readonly success: boolean
  readonly error?: string
}

// Built-in invariants
export const BUILTIN_INVARIANTS: Invariant[] = [
  {
    name: 'resource-consistency',
    description: 'Created resources must be retrievable',
    check: (state, history) => {
      // For each constructor in history, check that GET returns same data
      const constructors = history.filter((ctx, i) => {
        // Would need to track which history entries are constructors
        // This requires enhancing the history tracking
        return false
      })
      return { success: true }
    }
  },
  
  {
    name: 'tenant-isolation',
    description: 'Resources from tenant A must not be accessible in tenant B',
    check: (state) => {
      for (const [type, resources] of state.resources) {
        for (const [id, resource] of resources) {
          if (resource.scope.tenantId) {
            // Check no other tenant has access
            // Would need to simulate cross-tenant requests
          }
        }
      }
      return { success: true }
    }
  },
  
  {
    name: 'authorization-transitivity',
    description: 'If parent has permission, child must inherit it',
    check: (state) => {
      // For graph relations: if node A -> node B, then B inherits A's permissions
      const relations = state.relationships.get('relation') || []
      // Would need to check authorization evaluations
      return { success: true }
    }
  }
]

// Arbiter-specific invariants
export const ARBITER_INVARIANTS: Invariant[] = [
  {
    name: 'oauth-token-validity',
    description: 'Issued tokens must be valid until revoked',
    check: (state, history) => {
      const tokens = state.resources.get('token') || new Map()
      // Check each token was issued properly and hasn't expired
      return { success: true }
    }
  },
  
  {
    name: 'session-consistency',
    description: 'Active sessions must have valid users',
    check: (state) => {
      const sessions = state.resources.get('session') || new Map()
      const users = state.resources.get('user') || new Map()
      
      for (const [sessionId, session] of sessions) {
        const userId = (session.data as Record<string, unknown>)?.userId
        if (userId && !users.has(String(userId))) {
          return {
            success: false,
            error: `Session ${sessionId} references non-existent user ${userId}`
          }
        }
      }
      return { success: true }
    }
  },
  
  {
    name: 'permission-graph-acyclic',
    description: 'Permission inheritance graph must not have cycles',
    check: (state) => {
      // Detect cycles in relation graph
      const relations = state.relationships.get('relation') || []
      // Run cycle detection algorithm
      return { success: true }
    }
  },
  
  {
    name: 'tenant-application-consistency',
    description: 'Applications must belong to existing tenants',
    check: (state) => {
      const tenants = state.resources.get('tenant') || new Map()
      const applications = state.resources.get('application') || new Map()
      
      for (const [appId, app] of applications) {
        const tenantId = app.parentId
        if (tenantId && !tenants.has(tenantId)) {
          return {
            success: false,
            error: `Application ${appId} references non-existent tenant ${tenantId}`
          }
        }
      }
      return { success: true }
    }
  }
]

export const checkInvariants = (
  invariants: ReadonlyArray<Invariant>,
  state: ModelState,
  history: ReadonlyArray<EvalContext>
): Array<{ name: string; result: InvariantResult }> => {
  return invariants.map(inv => ({
    name: inv.name,
    result: inv.check(state, history)
  }))
}
```

### 3.4 Required: Temporal Logic in APOSTL

**File**: `src/formula/parser.ts` — Extend grammar

Add temporal operators:

```typescript
// New node types for temporal logic
export type FormulaNode =
  | ...existing nodes...
  | { type: 'temporal'; operator: 'eventually' | 'always' | 'until'; body: FormulaNode }
  | { type: 'previous'; inner: FormulaNode }
```

**File**: `src/formula/evaluator.ts` — Extend evaluation

```typescript
// Temporal evaluation requires history context
function evaluateTemporal(
  operator: string,
  body: FormulaNode,
  ctx: EvalContext,
  history: ReadonlyArray<EvalContext>
): boolean {
  switch (operator) {
    case 'eventually':
      // True if body is true at some point in future
      // For testing: check if body will be true after some operation
      return true // Placeholder
      
    case 'always':
      // True if body is true at all points
      return history.every(h => evaluateNode(body, h))
      
    case 'until':
      // True if left is true until right becomes true
      // Requires binary temporal operator
      return true // Placeholder
      
    default:
      throw new Error(`Unknown temporal operator: ${operator}`)
  }
}
```

### 3.5 Required: Stateful Test Runner Enhancement

**File**: `src/test/petit-runner.ts` — Add invariant checking to main loop

```typescript
export const runPetitTests = async (
  fastify: FastifyInstance,
  config: TestConfig
): Promise<TestSuite> => {
  const startTime = Date.now()
  const depth = DEPTH_CONFIGS[config.depth]

  const allRoutes = discoverRoutes(fastify)
  const filtered = filterByMode(allRoutes, config.mode)
  const routes = sortByCategory(filtered)

  const { commands: commandGroups, cacheHits, cacheMisses } = generateCommands(routes, depth, config.seed)
  const allCommands = commandGroups.flat()

  let state: ModelState = {
    resources: new Map(),
    counters: new Map(),
    relationships: new Map()
  }

  const resources: TrackedResource[] = []
  const results: TestResult[] = []
  const history: EvalContext[] = []  // Track all request/response contexts
  let testId = 0

  for (const command of allCommands) {
    testId++
    const name = `${command.route.method} ${command.route.path} (#${testId})`

    // Check preconditions
    const preOk = checkPreconditions(command, state)
    if (!preOk) {
      results.push({
        ok: true,
        name,
        id: testId,
        directive: 'SKIP preconditions not met'
      })
      continue
    }

    // Execute command
    let ctx: EvalContext
    try {
      ctx = await executeCommand(fastify, command, state)
      history.push(ctx)
    } catch (err) {
      results.push({
        ok: false,
        name,
        id: testId,
        diagnostics: { error: err instanceof Error ? err.message : String(err) }
      })
      continue
    }

    // Check postconditions
    const post = checkPostconditions(command, ctx)
    if (!post.success) {
      results.push({
        ok: false,
        name,
        id: testId,
        diagnostics: { error: post.error, statusCode: ctx.response.statusCode }
      })
    } else {
      results.push({ ok: true, name, id: testId })
    }

    // Update state
    state = updateState(command, ctx, state)
    
    // Check invariants after state change
    const invariantResults = checkInvariants(ARBITER_INVARIANTS, state, history)
    for (const inv of invariantResults) {
      if (!inv.result.success) {
        results.push({
          ok: false,
          name: `INVARIANT: ${inv.name} (#${testId})`,
          id: testId,
          diagnostics: { error: inv.result.error }
        })
      }
    }
    
    const resource = makeResource(command, ctx)
    if (resource !== null) {
      resources.push(resource)
    }
  }

  // Final invariant check
  const finalInvariantResults = checkInvariants(BUILTIN_INVARIANTS, state, history)
  for (const inv of finalInvariantResults) {
    if (!inv.result.success) {
      results.push({
        ok: false,
        name: `FINAL INVARIANT: ${inv.name}`,
        id: testId + 1,
        diagnostics: { error: inv.result.error }
      })
    }
  }

  const passed = results.filter((r) => r.ok && r.directive === undefined).length
  const failed = results.filter((r) => !r.ok).length
  const skipped = results.filter((r) => r.directive !== undefined).length

  return {
    version: 13,
    plan: { start: 1, end: results.length },
    tests: results,
    summary: { passed, failed, skipped, timeMs: Date.now() - startTime, cacheHits, cacheMisses }
  }
}
```

### 3.6 Arbiter-Specific Contract Examples

**Example contracts for Arbiter routes**:

```javascript
// Tenant isolation
{
  'x-requires': [
    'request_headers(this).x-tenant-id != null',
    'request_headers(this).authorization matches "^Bearer .+"'
  ],
  'x-ensures': [
    'response_code(this) == 200',
    'response_body(this).tenantId == request_headers(this).x-tenant-id',
    'if request_headers(this).x-tenant-id != response_body(this).tenantId then response_code(this) == 403 else T'
  ],
  'x-invariants': [
    'response_body(this).resources.all(r => r.tenantId == request_headers(this).x-tenant-id)'
  ]
}

// OAuth authorization
{
  'x-requires': [
    'query_params(this).client_id != null',
    'query_params(this).response_type == "code"',
    'request_headers(this).cookie != null'
  ],
  'x-ensures': [
    'response_code(this) == 302',
    'response_headers(this).location matches "\\?code="'
  ]
}

// Token issuance
{
  'x-requires': [
    'request_body(this).grant_type in ["authorization_code", "refresh_token"]',
    'request_body(this).code != null || request_body(this).refresh_token != null'
  ],
  'x-ensures': [
    'response_code(this) == 200',
    'response_body(this).access_token != null',
    'response_body(this).token_type == "Bearer"',
    'response_body(this).expires_in > 0'
  ]
}

// Graph authorization evaluation
{
  'x-requires': [
    'request_body(this).userId != null',
    'request_body(this).resourceId != null',
    'request_body(this).permission != null'
  ],
  'x-ensures': [
    'response_code(this) == 200',
    'response_body(this).allowed == true || response_body(this).allowed == false',
    'if response_body(this).allowed == true then response_body(this).reason != null else T'
  ]
}

// Rule creation
{
  'x-requires': [
    'request_headers(this).x-tenant-id != null',
    'request_body(this).dsl != null',
    'request_body(this).priority >= 0'
  ],
  'x-ensures': [
    'response_code(this) == 201',
    'response_body(this).id != null',
    'response_body(this).dsl == request_body(this).dsl',
    'response_body(this).tenantId == request_headers(this).x-tenant-id'
  ]
}
```

---

## 4. IMPLEMENTATION ROADMAP

### Week 1: Object Inference & Request Structure

**Day 1-2**: Resource Inference
- [ ] Create `src/domain/resource-inference.ts`
- [ ] Implement `extractResourceIdentity()`
- [ ] Implement `inferResourceHierarchy()`
- [ ] Add `ResourceHierarchy` to types
- [ ] Write tests (10+ cases)

**Day 3-4**: Request Builder
- [ ] Create `src/domain/request-builder.ts`
- [ ] Implement `buildRequest()`
- [ ] Implement `substitutePathParams()`
- [ ] Implement `extractBodyParams()`
- [ ] Implement `buildHeaders()`
- [ ] Write tests (10+ cases)

**Day 5**: Integration
- [ ] Update `petit-runner.ts` to use new modules
- [ ] Update `executeCommand()` signature
- [ ] Update `updateState()` for hierarchies
- [ ] Run full test suite
- [ ] Fix regressions

### Week 2: Logic & Invariants

**Day 1-2**: Formula Evaluation in Tests
- [ ] Update `checkPostconditions()` to use formula evaluator
- [ ] Handle parse errors gracefully
- [ ] Add formula error diagnostics
- [ ] Write tests for formula-based postconditions

**Day 3-4**: Invariant Registry
- [ ] Create `src/domain/invariant-registry.ts`
- [ ] Implement builtin invariants
- [ ] Implement Arbiter-specific invariants
- [ ] Add invariant checking to test runner loop
- [ ] Write tests for invariant detection

**Day 5**: Temporal Logic (Basic)
- [ ] Add `previous()` operator support
- [ ] Implement basic history tracking
- [ ] Add `always` temporal operator
- [ ] Write tests for temporal assertions

### Week 3: Stateful Testing & Polish

**Day 1-2**: Command Sequences
- [ ] Implement fast-check `commands()` arbitrary
- [ ] Generate valid command sequences respecting preconditions
- [ ] Add sequence shrinkers
- [ ] Write property tests for sequences

**Day 3-4**: Arbiter Integration
- [ ] Create Arbiter-specific resource patterns
- [ ] Create Arbiter request patterns
- [ ] Add Arbiter-specific invariants
- [ ] Test against Arbiter route samples

**Day 5**: Documentation & Performance
- [ ] Update README with advanced examples
- [ ] Update SKILL.md with new patterns
- [ ] Profile performance with 1000+ routes
- [ ] Optimize hot paths
- [ ] Final test suite: 250+ tests

---

## 5. TEST COVERAGE TARGETS

### Current: 198 tests

### Target after implementation:
- **Resource inference**: +30 tests
- **Request builder**: +25 tests
- **Formula evaluation in tests**: +20 tests
- **Invariant registry**: +25 tests
- **Temporal logic**: +15 tests
- **Stateful sequences**: +20 tests
- **Arbiter-specific**: +20 tests
- **Total**: ~353 tests

---

## 6. FILES TO CREATE/MODIFY

### New Files
```
src/domain/resource-inference.ts
src/domain/request-builder.ts
src/domain/invariant-registry.ts
src/domain/arbiter-resources.ts
src/domain/arbiter-requests.ts
src/test/resource-inference.test.ts
src/test/request-builder.test.ts
src/test/invariant-registry.test.ts
src/test/temporal-logic.test.ts
```

### Modified Files
```
src/types.ts                    — Add ResourceHierarchy, update ModelState
src/test/petit-runner.ts        — Use resource inference, request builder, invariants
src/formula/parser.ts           — Add temporal operators (if needed)
src/formula/evaluator.ts        — Add history context support
src/domain/category.ts          — Add Arbiter-specific category rules
```

---

## 7. ACCEPTANCE CRITERIA

### Object Inference
- [ ] Can extract resource identity from response body using schema
- [ ] Can determine parent-child relationships from route paths
- [ ] Can handle OAuth tokens, sessions, graph nodes/relations
- [ ] Returns null for non-resource routes (health, utility)
- [ ] All Arbiter resource types are correctly identified

### Request Structure
- [ ] Path params are substituted from generated data or state
- [ ] Body params match schema properties (no extra fields)
- [ ] Query params are extracted for GET/DELETE
- [ ] Headers include x-tenant-id from scope
- [ ] Authorization header is injected when required
- [ ] Content-Type is set correctly (JSON vs form-encoded)

### Logic & Invariants
- [ ] APOSTL formulas in x-ensures are evaluated (not just status:###)
- [ ] Cross-route invariants are checked after each state change
- [ ] Tenant isolation is verified
- [ ] Resource consistency is verified (created resources are retrievable)
- [ ] Authorization transitivity is checked
- [ ] Session consistency is verified
- [ ] Temporal operators work (previous, always)

### Performance
- [ ] < 2s overhead for 1000 routes
- [ ] < 5s overhead for 10,000 routes
- [ ] Incremental cache still provides 10x+ speedup
- [ ] Memory usage < 500MB for full Arbiter test run

---

## 8. RISKS & MITIGATIONS

| Risk | Impact | Mitigation |
|------|--------|------------|
| Formula evaluation too slow | High | Cache parsed ASTs, use WeakMap |
| Invariant checking O(n²) | Medium | Batch checks, use Set lookups |
| Memory leak in history | Medium | Limit history size, use ring buffer |
| Arbiter routes lack schemas | High | Fallback to path-based inference |
| Fastify v5 compatibility | Low | Already using inject() API |
| Breaking changes to existing tests | Medium | Maintain backward compatibility for status:### |

---

**Next Action**: Start with `src/domain/resource-inference.ts` — this is the foundation everything else builds on.