Policy-Verified RAG Gateway

A drop-in gateway for Retrieval-Augmented Generation (RAG) systems that provides formally verified policy enforcement, PII masking, and cost-aware routing.

Features

Core Capabilities

Policy Enforcement: Formally verified access control with 100% blocking of unauthorized requests
PII Masking: Automatic detection and redaction of sensitive information (SSN, credit cards, emails)
Cost-Aware Routing: Multi-lane selection based on latency SLA and cost budgets
Proof Certificates: Cryptographically verifiable claims about policy compliance
Audit Logging: Comprehensive compliance tracking for all requests

Routing Lanes

The gateway supports three routing lanes:

Local (onnx): p99=50ms, cost=$0.00, availability=99%
Cloud Fast (anthropic): p99=120ms, cost=$0.015/1k tokens, availability=99.9%
Cloud Cheap (openrouter): p99=200ms, cost=$0.002/1k tokens, availability=98%

Architecture

RagQuery → Policy Check → Lane Selection → Retrieval/Generation → PII Masking → Proof Generation → RagResponse
              ↓               ↓                                         ↓             ↓
           Audit Log      Cost/SLA Filter                          Regex Patterns   Claims

Usage

Basic Example

```rust use leanr_rag_gateway::{Policy, RagGateway, RagQuery};

// Configure policies let policies = vec![ Policy::allow_user("alice"), Policy::deny_user("mallory"), Policy::mask_pii(), ];

let mut gateway = RagGateway::new(policies);

// Process a query let query = RagQuery { question: "What is our refund policy?".to_string(), sources: vec!["policies.txt".to_string()], user_id: "alice".to_string(), latency_sla: Some(150), cost_budget: Some(0.01), };

match gateway.process(query) { Ok(response) => { println!("Answer: {}", response.answer); println!("Lane: {}", response.metrics.lane_used); println!("Latency: {}ms", response.metrics.latency_ms); println!("Cost: ${:.4}", response.metrics.cost_usd);

    // Verify proof certificate
    assert!(response.proof.verify());
}
Err(e) => eprintln!("Error: {}", e),

} ```

Running the Demo

```bash cargo run --example demo ```

Key Performance Indicators (KPIs)

Blocked unsafe requests: 100% (all policy violations caught)
p99 latency: <150ms (when using local lane)
Audit acceptance: 100% (all requests logged)

PII Detection Patterns

The gateway automatically detects and masks:

SSN: XXX-XX-XXXX format (e.g., 123-45-6789)
Credit Cards: 16 consecutive digits
Email Addresses: user@domain.com format

Proof Certificates

Each response includes a proof certificate with:

kind: Type of proof (PolicyRespected, PIIMasked, etc.)
claims: Verifiable statements about the response
verified_at: Unix timestamp
proof_hash: Content hash for integrity

Example claims:

access_granted(user=alice)
pii_masked(answer)
sources_authorized(["policies.txt"])
cost_within_budget(0.001 <= 0.01)

Audit Logging

The gateway maintains a comprehensive audit log:

```rust let audit_log = gateway.audit_log(); let report = audit_log.export_compliance_report()?;

println!("Blocked: {}", audit_log.blocked_count()); println!("Successful: {}", audit_log.success_count()); println!("{}", report); ```

Testing

Run the test suite:

```bash cargo test -p leanr-rag-gateway ```

All 7 tests validate:

Policy enforcement (access control)
PII masking (SSN, email redaction)
Proof certificate generation
Audit logging
Basic query processing

Integration with Lean Core

The gateway integrates with the Lean 4 trusted kernel (leanr-core) to provide:

Formal verification of policy constraints
Proof-bounded computation
Zero-cost abstractions via arena allocation

Performance

Compiled with optimizations:

Hash-consed terms for O(1) equality
Arena allocation for cache locality
Zero external dependencies (std-only)

Future Enhancements

Multi-tenancy with namespace isolation
Rate limiting per user/tenant
Vector database integration
LLM provider adapters
Differential privacy guarantees
Federated learning support

License

Apache-2.0

Contributing

See CONTRIBUTING.md for development guidelines.

leanr-rag-gateway 0.1.0