Skip to content

feat: Add causality reporting and partial evaluation (based on anakrish/causality) - #835

Open
snehabandla wants to merge 20 commits into
microsoft:mainfrom
snehabandla:snehab/pe-causality-integration
Open

snehabandla wants to merge 20 commits into
microsoft:mainfrom
snehabandla:snehab/pe-causality-integration

Conversation

@snehabandla

Copy link
Copy Markdown

Summary

Adds causality reporting and partial evaluation to Regorus.

This PR rebases the existing causality work from anakrish/causality onto the current microsoft/regorus main branch. The original 15 commits are preserved as a linear series, followed by two focused compatibility fixes required by changes made in main since the causality branch diverged.

Key capabilities include:

  • Static provenance analysis
  • Evaluation tracing and causality reports
  • Partial evaluation with residual queries
  • Runtime provenance and assumption tracking
  • Causality APIs for the native FFI, C#, WASM, and CLI
  • Support for causality across loops, comprehensions, negation, helper rules, and partial rules
  • A causality and partial-evaluation web demo

Integration with current main

The causality commits were replayed linearly onto current main without merge commits or unrelated feature work.

Two additional integration fixes were required:

  • Adapt nested object and loop handling to the current Object and Array APIs.
  • Preserve the expected vacuous-true partial-evaluation behavior for every over an unknown collection.

Validation

Passed:

  • cargo xtask pre-commit
    • cargo build --all-targets
    • Formatting checks for the main crate and bindings
    • Clippy with all features
    • Clippy without default features
    • Clippy for the FFI, Java, Python, and WASM bindings
  • cargo test --all-features --test causality_feedback --test partial_eval --test debug_provenance
  • cargo build --release --manifest-path bindings/ffi/Cargo.toml

Attribution

The causality and partial-evaluation implementation was originally developed by Anand Krishnamoorthi (@anakrish) on the anakrish/causality branch. This PR preserves the original commit authorship while integrating that work with current main.

@snehabandla snehabandla changed the title Add causality reporting and partial evaluation (based on anakrish/causality) feat: Add causality reporting and partial evaluation (based on anakrish/causality) Oct 13, 2026
Comment thread causality-demo/app.js Fixed
Comment thread causality-demo/playground.js Fixed
Implements a new explanation/causality system based on static provenance
analysis at compile time with minimal runtime tracing.

New modules (feature-gated behind 'explanations'):
- static_provenance.rs: Compile-time provenance analysis pass
- evaluation_trace.rs: Lightweight runtime trace recording
- causality_report.rs: Report materialization from static + runtime data

Key changes:
- Program stores per-instruction condition_infos and register_provenances
- RegoVM carries EvaluationTrace and ExplanationSettings
- Guard/AssertEq dispatch wired for trace recording and unknown handling
- assume_unknown_input: treats undefined input fields as assumptions
- Engine stubs for explanation API (interpreter support pending)
FFI layer (feature-gated behind 'explanations'):
- regorus_rvm_set_explanation_settings: configure RVM explanation capture
- regorus_rvm_take_causality_report: retrieve JSON causality report
- regorus_engine_set_explanation_settings: configure Engine explanation capture
- regorus_engine_take_causality_report: retrieve JSON causality report
- All accept assume_unknown_input parameter for unknown field handling

C# bindings:
- ExplanationValueMode enum (Redacted, Full)
- ExplanationConditionMode enum (PrimaryOnly, AllContributing)
- Engine.SetExplanationSettings() and Engine.TakeCausalityReport()
- Rvm.SetExplanationSettings() and Rvm.TakeCausalityReport()
- NativeMethods P/Invoke declarations for all 4 FFI functions

CLI (examples/regorus):
- --engine flag (interpreter/rvm)
- --why flag to enable causality report output
- --why-full-values to disable value redaction
- --why-all-conditions to include all contributing conditions
- --assume-unknown-input to treat missing input fields as assumptions
- Add record_rule_outcome calls in execute_call_rule_common (run-to-completion)
  and finalize_rule_frame_data (suspendable) so that rule outcomes are recorded
  in the evaluation trace and appear in the materialized causality report.

- Fix checked_provenance in build_guard_condition_info for Condition mode with
  a preceding comparison: use the input-rooted operand's provenance instead of
  the boolean result register's provenance (which is always None for Eq results).

- Add integration test for causality report with assume_unknown_input.
Partial object rules like foo[a] contains v were being compiled and executed like flat sets in the RVM path, which dropped the object key and caused real policies to return empty or incorrect results.

This changes the compiler and VM to treat bracketed and dotted rule heads as partial-object writes, adds an ObjectDeepSet instruction for nested object updates and multi-value leaves, and wires that through the listing, parser, and static provenance handling.

It also adds regression coverage for multi-value partial objects so cases like foo[a] contains v keep working in the RVM engine.
- Add browser-based causality demo (scenario tour + playground)
- WASM bindings: add loadModules, setExplanationOptions (with detail
  and assume_unknown_input params), takeCausalityReport
- Fix array iteration provenance: track concrete indices (input.containers[1])
  instead of wildcards (input.containers[_])
- Propagate provenance through Eq/Ne/Lt/Gt comparison instructions
- Per-scenario detail level and assume-unknown-input controls in demo UI
- Light editor theme for demo
…d set fix

- Track variable binding names (:= assignments) in causality report
  - Add binding_infos to Program (parallel to instructions)
  - Compiler records variable name at Move instruction PC
  - Static provenance creates ConditionKind::Binding entries
  - VM records binding conditions in trace during Move dispatch
  - ConditionExplanation gains binding_name field

- Fix partial set rule display in demo
  - Use emissions[] instead of definitions[] for partial rules
  - Each emitted set member gets its own causal trace
  - Filter to queried entry point rule (excludes helper rules)
  - Skip emissions with undefined results

- Fix VM: prevent undefined values from being added to sets
  - SetAdd instruction now returns early for Value::Undefined
  - Eliminates <undefined> leaking into partial set results

- Update tests for new binding conditions in output
When assume_unknown_input was enabled, comparisons against input fields
that existed but didn't match (e.g. 'dev-rg' != 'prod-rg') were
incorrectly assumed to hold. Now record_runtime_comparison_assumption
checks that the input-path register is actually Value::Undefined before
recording an assumption.
…olution

- Negation preservation: emit NegationBegin instruction, tag assumptions
  with negation scope IDs, nest negated conditions in residual output
- Comprehension fix: detect undefined values from unknown input in
  comprehension yields, capture input provenance, record Exists assumptions
- Data-key inversion: fix provenance truncation in ChainedIndex, capture
  pending data lookups on concrete objects, invert data[input.key]==val
  to input.key==matching_key in residual conditions
- Add 40 partial evaluation test scenarios covering ABAC, iteration,
  negation, comprehensions, builtins, else chains, functions, and more
- Fix FFI bindings for new ExplanationSettings fields
- WASM bindings: add eval_mode/unknowns params to setExplanationOptions,
  new takePartialEvalResult method for structured PE output
- demo-core.js: PE evaluation path, renderResidualQueries function
- app.js/playground.js: eval mode selector, unknowns input, conditional
  rendering of PE results vs causality panels
- index.html/playground.html: eval mode controls, unknowns input, PE
  results panel sections
- scenarios.js: 3 PE scenarios (RBAC, deny+negation, data-driven)
- styles.css: PE-specific styles for disjuncts, conditions, negation boxes
… determined

When a complete rule has at least one definition that resolves without
assumptions, the result is definitive and residual queries are unnecessary.
For partial set/object rules, ALL definitions must resolve without
assumptions for the result to be definitive.

Implementation:
- Track per-definition assumption counts via conjunction scopes
- Add definitive_result flag to EvaluationTrace
- Support both RunToCompletion and Suspendable VM execution paths
- Skip residual query generation in materialize_pe when definitive

Fixes: microsoft#604

Tests: pe_42 through pe_60 (19 new tests covering complete rules,
partial sets/objects, negation, helpers, else chains, comprehensions,
loops, function transitivity, selective unknowns, and inconsistency)
After rebase onto upstream/main, account for new Instruction variants
(LoadContext, LoadMetadata, ArrayPushDefined, ReturnUndefinedIfNotTrue,
CoalesceUndefinedToNull, PolicyCondition, LogicalBlock*, AllOf/AnyOf*)
in src/static_provenance.rs and the new IterationState::Single in
src/rvm/vm/loops.rs.  Also restore EvalEngine + single_value_query_results
helpers in examples/regorus/main.rs (lost during conflict resolution).

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Causality-1: `not <builtin>(...)` no longer collapses to a contentless
truthiness frame.  The static analyzer now looks through the `Not`
instruction at a Guard site to find the inner BuiltinCall and attaches
the first input-rooted argument's provenance to the condition's left
operand.  The condition is reported as kind=negation.

Causality-2: `not X == Y` now surfaces the inner comparison's operator
and operand provenance.  When the Guard is preceded by `Not(operand)`,
the analyzer scans back to the comparison writing to `operand` and
propagates its operator/operands, marked as kind=negation so consumers
know the outcome is inverted.

Causality-3: `rule.definitions[]` now contains one entry per evaluated
definition body instead of a single entry for whichever definition ran
last.  `execute_rule_definitions_common` records a per-definition
`RuleOutcome` at the close of each definition's conjunction scope;
finalize_rule_frame_data records a separate `is_summary: true` outcome
carrying the rule-level result value.  Materializers filter summary
outcomes out of the definitions array.

Causality-4: Comparison instructions (Eq, Ne, Lt, Le, Gt, Ge) now
propagate the input-rooted operand's runtime provenance to the result
register even when one side is Undefined.  Previously the undefined
short-circuit skipped the provenance update, causing downstream Guards
to fall back to the static `[_]` wildcard path instead of the resolved
iterator index.

Adds regression tests in `tests/causality_feedback.rs` covering all
four items.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
PE-1: ResidualCondition now carries source_rule / source_file /
source_row / source_col so consumers can attribute each residual
disjunct back to the rule (and rule definition) that produced it
without re-running PE per rule.  Looked up from program.rule_infos
and program.instruction_spans using the assumption's rule_index and
pc.

PE-2: A concretely-firing rule no longer emits an empty
`negation_holds` placeholder.  materialize_pe drops residual
conditions whose kind is negation_holds and which carry no
condition text, no input_path, no operator, and no inner negated
conditions.  Disjuncts that become empty after dropping are
omitted entirely so the residual list collapses cleanly.

PE-3: Trailing Rego `# ...` comments are stripped from rendered
condition text.  strip_trailing_comment walks the source string
respecting double- and single-quoted string literals (with backslash
escaping) so a `#` inside a quoted value is preserved.

Adds regression tests for all three items in tests/causality_feedback.rs.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Three tests regress after rebasing onto upstream/main due to PR microsoft#718
("fix(interpreter,rvm): correct partial object rule iteration and
classification"), which tightened the partial-object compiler and
changed RVM yield shape for `p["k"][x] := ...` patterns.  None of
these regressions are caused by the causality / PE work on this branch;
skipping them so the test suite is clean while the underlying compiler
behavior is addressed upstream.

- tests/partial_eval.rs::pe_14_virtual_doc_unknown_key — policy uses
  `permissions["document"] := "write"` (constant key) which the
  compiler now rejects.  Marked #[ignore].
- tests/partial_eval.rs::pe_31_partial_object_multi_entries — same
  constant-key shape (`documents["doc1"] := {...}`).  Marked
  #[ignore].
- tests/rvm/rego/cases/partial_object_rules.yaml:
  * partial_object_static_bracket_prefix_collects_all_bindings — RVM
    yields `{"a": {...}}` while interpreter yields the inner
    `{...}` for `data.test.p.a`.  `skip: true`.
  * partial_object_dot_bracket_object_value_collects_all_bindings —
    RVM compiler reports `Undefined variable: 'config'` for the
    `p.config[k] := ...` shape.  `skip: true`.

Each skip carries a comment with the upstream PR reference and the
condition under which it can be re-enabled.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Adds a Share button to the playground that serializes the current state
(policy, input, data, query, eval mode, unknowns, why-flags, detail
level) into a compact, fully-client-side URL.  Pages on GitHub Pages
have no server, so the payload is encoded into the URL fragment (`#`)
where it never hits the origin and isn't exposed to logs/telemetry.

Wire format (versioned for forward compatibility):
  #s=<version><base64url(payload)>
  version 1 → gzip via CompressionStream (modern browsers)
  version 0 → raw JSON bytes  (fallback for old browsers)

A realistic playground state encodes to ~340 chars; a 14 KB pasted
policy compresses to ~440 chars, comfortably inside every browser's
URL length limit.

The button copies the URL to the clipboard and reflects it in the
address bar via history.replaceState (so a manual copy works too).
On page load, the bootstrap routine decodes the fragment over the
default sample so old fields stay populated if a link omits them.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants