Files
regorus/docs/knowledge/causality-and-partial-eval.md
copilot-swe-agent[bot] 524aab5528 Add knowledge docs, agent definitions, and skill files
Add comprehensive documentation and GitHub Copilot configuration:

- docs/knowledge/: 17 deep-dive knowledge files covering value semantics,
  RVM architecture, builtins, FFI boundary, feature composition, error
  handling migration, policy evaluation security, Rego semantics,
  interpreter/compiler architecture, Azure Policy/RBAC, engine API,
  time builtins, language extension guide, tooling architecture,
  causality/partial eval, Rego compiler, Azure Policy aliases, and
  telemetry/diagnostics

- .github/agents/: 16 role-specific AI agent definitions (red-teamer,
  semantics-expert, architect, performance-engineer, test-engineer,
  verification-engineer, security-auditor, reliability-engineer,
  support-engineer, ci-engineer, refactorer, api-steward, program-manager,
  demo-engineer, dx-engineer, tech-lead)

- .github/skills/: 6 workflow skill definitions (thorough-review,
  design-alternatives, add-builtin, opa-conformance, security-review,
  verification)

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Co-authored-by: anakrish <35780660+anakrish@users.noreply.github.com>
2026-04-25 21:20:10 +00:00

8.0 KiB

Knowledge: Causality and Partial Evaluation

Design considerations for future causality tracking and partial evaluation features. These are not yet implemented but the architecture is being designed to support them. Read this when making architectural decisions that may affect these future capabilities.

Partial Evaluation

What It Is

Partial evaluation reduces a policy given known inputs while leaving unknown parts symbolic:

Full policy + known data + unknown input
    → Simplified policy (only depends on unknown input)

Example:

allow {
    input.role == "admin"       # Unknown (depends on input)
    data.feature_enabled        # Known: true
    input.department in {"eng", "security"}  # Unknown
}

Partial evaluation with data.feature_enabled = true:

allow {
    input.role == "admin"
    input.department in {"eng", "security"}
}

The data.feature_enabled check is eliminated because it's always true.

Use Cases

  1. Policy optimization: pre-evaluate known parts at compile/load time
  2. Policy simplification: show users what a policy means for their context
  3. Incremental evaluation: only re-evaluate changed parts
  4. Query planning: push policy decisions closer to data sources
  5. Policy diffing: compare simplified policies across configurations

Current Architecture Support

Scheduler dependency analysis: The scheduler already identifies which statements depend on which variables. Statements that only depend on known variables can be evaluated. Statements with unknown dependencies remain symbolic.

RVM register model: Registers could hold symbolic values alongside concrete ones. Instructions that operate on symbolic values produce symbolic results.

Value type extensibility: The Value enum could be extended:

pub enum Value {
    // ... existing variants ...
    Symbolic(SymbolicExpr),  // Future: represents an unknown value
}

Compilation pipeline: The hoister and scheduler already separate ground-truth computations from data-dependent ones. This separation is the foundation for partial evaluation.

Design Principles

  1. Preserve semantics: partially evaluated policy must produce identical results to the original when the remaining unknowns are bound.

  2. Undefined handling: partial evaluation must correctly propagate Undefined through symbolic expressions. This is the hardest part — not Undefined = true means symbolic undefined propagation has non-obvious results.

  3. No information loss: the residual policy must capture all constraints, including those that were partially evaluated.

  4. Composability: partial evaluation results should be further partially evaluatable as more inputs become known.

Implementation Considerations

Phase 1: Ground-truth elimination

  • Identify statements where all variables are known
  • Evaluate them and replace with results
  • Remove always-true conditions, eliminate always-false rule bodies
  • This is the easiest phase and provides immediate value

Phase 2: Symbolic propagation

  • Track symbolic values through expressions
  • Simplify expressions where possible (e.g., true AND xx)
  • Handle Undefined propagation symbolically
  • Generate residual policy/program

Phase 3: Cross-rule analysis

  • Partially evaluate virtual documents
  • Propagate known rule results into dependent rules
  • Handle default rules in partial context

Challenges

  • Undefined propagation: not (Undefined) = true makes symbolic analysis non-trivial. A symbolic expression that might be Undefined has different semantics under negation.

  • Set/Object construction: if any element is symbolic, the entire collection construction may need to remain symbolic.

  • Comprehensions: partial evaluation of comprehensions requires knowing which iterations are ground vs symbolic.

  • Builtins: some builtins are pure (suitable for partial evaluation), others have side effects or depend on runtime state (time.now_ns()).

Causality Tracking

What It Is

Causality tracking answers why a policy produced its result:

  • Which rules contributed to the decision?
  • What input/data values were decisive?
  • What would need to change to get a different result?

Use Cases

  1. Audit: prove why a request was allowed/denied
  2. Debugging: understand unexpected policy decisions
  3. Compliance: demonstrate that decisions follow documented logic
  4. Counterfactual: "what if the user had role X instead of Y?"

Current Infrastructure

Coverage tracking (coverage feature):

  • Records which expressions were evaluated
  • Binary: evaluated or not evaluated
  • Doesn't track values or decision flow

Tracing (eval_query(query, tracing=true)):

  • Captures evaluation steps
  • Provides more detail than coverage
  • Performance cost limits production use

RVM frame stack (suspendable mode):

  • Frame-by-frame execution history
  • Instruction-level granularity available via single-step mode
  • Only in suspendable mode (not run-to-completion)

Active rules stack (interpreter):

  • Tracks which rules are currently being evaluated
  • Used for cycle detection
  • Could be repurposed for causality

Design Vision

Decision Tree

A tree structure recording the evaluation path:

allow = true
├── Rule: data.auth.allow (body 1 succeeded)
│   ├── Statement: input.role == "admin" → true
│   │   └── input.role = "admin" (from input)
│   └── Statement: input.active == true → true
│       └── input.active = true (from input)
└── Default: data.auth.deny = false (not triggered)

Value Provenance

Track where each value came from:

  • input.role → from user input
  • data.allowed_roles → from data document loaded at path X
  • count(data.items) → computed by builtin from data

Counterfactual Analysis

"What would change if input.role were "viewer" instead?"

  • Re-evaluate with modified input
  • Compare decision trees
  • Report which statements changed outcome

Architecture Implications

  1. Opt-in overhead: causality tracking adds memory and CPU cost. Must be behind a feature flag or runtime configuration. Never in the hot path for production evaluation.

  2. Value annotation: Values may need optional metadata:

    struct AnnotatedValue {
        value: Value,
        provenance: Option<Provenance>,  // Where it came from
    }
    
  3. Evaluation hooks: the interpreter/RVM need "observation points" where causality information is recorded. These should be no-ops when tracking is disabled.

  4. Serializable traces: decision trees and provenance information need to be serializable (JSON) for audit logging and external tooling.

  5. Deterministic replay: for counterfactual analysis, the evaluation must be deterministic. This means:

    • time.now_ns() must be mockable
    • Random builtins must be seedable
    • External data must be snapshotted

Connection to Partial Evaluation

Causality and partial evaluation complement each other:

  • Partial evaluation identifies the relevant parts of a policy
  • Causality tracking explains the decisions within those parts
  • Together they answer: "given what we know, what decisions were made and why?"

Design Principles for Both Features

  1. Keep evaluation logic pure — side-effect-free functions are easier to partially evaluate and track causally.

  2. Document invariants explicitly — invariants that hold during evaluation are the foundation for symbolic reasoning.

  3. Prefer exhaustive pattern matching — every case handled explicitly makes symbolic analysis tractable.

  4. Separate observation from computation — tracking infrastructure should be orthogonal to evaluation logic.

  5. Correct today, analyzable tomorrow — current code should be designed so these features can be added without fundamental restructuring.