Partial evaluation of rules with else

What is the underlying problem you're trying to solve?

When a complete rule with else depends on something unknown, partial evaluation keeps the reference to the rule instead of going through it. The evaluator says so in evalVirtual.eval (v1/topdown/eval.go:2967 at v1.20.2):

// Partial evaluation of ordered rules is not supported currently. Save the
// expression and continue. This could be revisited in the future.

The residual then names the original rule whatever the known part of the input is. Two requests the policy answers differently get the same residual, and whoever consumes it, through the Compile API or an optimized bundle, has to evaluate the original policy again to tell them apart.

A small example:

package example

default allow := false

allow if can_publish

can_publish := true if {
	input.action == "publish"
	"editor" in data.users[input.user].roles
} else := false

{"users": {"alice": {"roles": ["editor"]}, "carol": {"roles": ["viewer"]}}}

opa eval -d example.rego -d data.json -i carol.json --partial --unknowns input.action -f source 'data.example.allow'

With {"user": "carol"} as input:

# Query 1
data.partial.example.allow

# Module 1
package partial.example

default allow := false

allow if data.example.can_publish

and exactly the same with {"user": "alice"}. Written with a default instead of an else,

default can_publish := false

can_publish if {
	input.action == "publish"
	"editor" in data.users[input.user].roles
}

the rule is evaluated: carol is left with the defaults alone, and alice with can_publish if input.action = "publish".

Reproduced with v1.20.2 through the Go API, and with the v1.19.0 CLI for the output above.

Describe the ideal solution

Partial evaluation goes through rules and functions with else.

For a complete rule the evaluator already fixes what an else means: the branches of one definition are tried in order, and the first whose body has a result gives the value (evalVirtualComplete.evalValue, v1/topdown/eval.go:3831 to 3862). That can be written as rules where each branch waits for the ones before it to fail:

p := v0 if B0 else := v1 if B1

behaves as

p := v0 if B0

p := v1 if {
	not b0
	B1
}

b0 if B0

Partial evaluation already builds support rules for a negated expression that depends on unknowns (evalNotPartialSupport, v1/topdown/eval.go:927), so generating the branches as support rules seems to fit what is there.

A function is tried with its output already unified with the value of each branch (v1/topdown/eval.go:2291 and 2308), so a branch whose value does not match the output fails and the next one is tried:

f(x) := 1 if x > 0 else := 2

bound_output if f(1, 2)     # holds

unbound_output if {
	y := f(1)
	y == 2                  # does not hold
}

Branches that exclude each other would make bound_output false, so for a function the value it is asked for would have to stay part of the condition of each branch.

Describe a "Good Enough" solution

Complete rules only, with calls to functions that have an else saved as they are today. That already covers a rule that falls back to a value with else := ....

Additional Context

Petard, which is built on the Go API, rewrites complete rules this way before partial evaluation (the rewrite, the tests). The rewritten policy was checked against the original with ordinary evaluation, rule by rule: the answers match, apart from rules that call nondeterministic builtins. If the approach looks right, I would be glad to work on a PR.