Partial evaluation of rules with else

[saluc28]

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.