Partial evaluation incorrectly evaluates case (true OR undefined) when using default values

[KSpaceer]

Short description

OPA version - 1.30.0

Example policies:

main.rego

package main

default allow := false

allow if {
    data.support.allow
}

support.rego

package support

default allow := false

allow if {
    input.undefined
}

allow if {
    input.defined
}

input.json

{"defined": true}

CLI command:

opa eval -i input.json -d main.rego -d support.rego -u 'input.undefined' -p "data.main.allow == true"

Output:

{
  "partial": {
    "queries": [
      [
        {
          "index": 0,
          "terms": {
            "type": "ref",
            "value": [
              {
                "type": "var",
                "value": "data"
              },
              {
                "type": "string",
                "value": "partial"
              },
              {
                "type": "string",
                "value": "support"
              },
              {
                "type": "string",
                "value": "allow"
              }
            ]
          }
        }
      ]
    ],
    "modules": [
      {
        "package": {
          "path": [
            {
              "type": "var",
              "value": "data"
            },
            {
              "type": "string",
              "value": "partial"
            },
            {
              "type": "string",
              "value": "support"
            }
          ]
        },
        "rules": [
          {
            "body": [
              {
                "index": 0,
                "terms": {
                  "type": "boolean",
                  "value": true
                }
              }
            ],
            "default": true,
            "head": {
              "name": "allow",
              "value": {
                "type": "boolean",
                "value": false
              },
              "ref": [
                {
                  "type": "var",
                  "value": "allow"
                }
              ]
            }
          },
          {
            "body": [
              {
                "index": 0,
                "terms": {
                  "type": "boolean",
                  "value": true
                }
              }
            ],
            "head": {
              "name": "allow",
              "value": {
                "type": "boolean",
                "value": true
              },
              "ref": [
                {
                  "type": "var",
                  "value": "allow"
                }
              ]
            }
          },
          {
            "body": [
              {
                "index": 0,
                "terms": {
                  "type": "ref",
                  "value": [
                    {
                      "type": "var",
                      "value": "input"
                    },
                    {
                      "type": "string",
                      "value": "undefined"
                    }
                  ]
                }
              }
            ],
            "head": {
              "name": "allow",
              "value": {
                "type": "boolean",
                "value": true
              },
              "ref": [
                {
                  "type": "var",
                  "value": "allow"
                }
              ]
            }
          }
        ]
      }
    ]
  }
}

Expecting to have an empty query in the output list (indicating that query can be already evaluated), but it does not appear. Also one of modules contains rule allow := true if { true }, which could be propagated to the whole output, resulting in empty query.

N.B: if we remove defaults from the policies, the output is correct:

main.rego

package main

allow if {
    data.support.allow
}

support.rego

package support

allow if {
    input.defined
}

allow if {
    input.undefined
}

CLI output

{
  "partial": {
    "queries": [
      [],
      [
        {
          "index": 0,
          "terms": {
            "type": "ref",
            "value": [
              {
                "type": "var",
                "value": "input"
              },
              {
                "type": "string",
                "value": "undefined"
              }
            ]
          }
        }
      ]
    ]
  }
}

Expected behavior

Additional context

[srenatus]

Thanks for the write-up! To make it easier to grok the output, I've run it with -fpretty:

with defaults

$ echo '{"defined": true }' | opa eval -I -fpretty -p -u input.undefined -d support.rego -d main.rego 'data.main.allow'
+-----------+-------------------------------------+
| Query 1   | data.partial.main.allow             |
+-----------+-------------------------------------+
| Support 1 | package partial.support             |
|           |                                     |
|           | default allow := false              |
|           |                                     |
|           | allow := true                       |
|           |                                     |
|           | allow if input.undefined            |
+-----------+-------------------------------------+
| Support 2 | package partial.main                |
|           |                                     |
|           | default allow := false              |
|           |                                     |
|           | allow if data.partial.support.allow |
+-----------+-------------------------------------+

without defaults

$ echo '{"defined": true }' | opa eval -I -fpretty -p -u input.undefined -d support-no-default.rego -d main-no-default.rego 'data.main.allow'
+---------+-----------------+
| Query 1 | input.undefined |
+---------+-----------------+
| Query 2 |                 |
+---------+-----------------+

Since these are two different policies, we can't expect the same results. However, let's have a look at the case _with defaults, and what a full eval would give us:

case	input.defined	input.undefined	full eval result	partial + full eval result
(a)	true	undefined or false	true	true
(b)	true	anything else	true	true

So this looks like the basic invariant of PE is not invalidated: full eval with the combined input is the same as PE + subsequent full eval with the previously unknown input.

Now, it's annoying to deal with default rules in PE results, I know that. #1418 is going to improve that. Do you think there's anything here going beyond what that issue describes?

[KSpaceer]

@srenatus thank you for the answer!

First of all, the policies in my issue actually can be rewritten as one policy. Also, in order to reproduce the issue we do not need any defined value - just the undefined one. So, the policy would be written as:

package main

default allow := false

allow := true

allow if {
   input.undefined
}

Secondly, I'm not sure that #1418 is related to the current issue directly, because when implemented it should inline default values if the other rules fail, which is not the case here.

[srenatus]

To put it simply, to convince me that there's a bug here, this is what is needed: A set of inputs, where one part is known and the other unknown, such that

1. when PE is run with that known/unknown setup,
2. and we subsequently evaluate the PE results with the full input,
3. there's a different outcome than if we only evaluated the policies with all the input known in one step.

From my pen and paper exercise above, that isn't the case here. Have I been missing something?

[KSpaceer]

Yes, you're correct so I think we can say calling this issue a bug was a misidentification. It is better to say that we have some sort of inconvenience of PE usage, because of this issue in cases when we could use only PE to achieve our goals, we have to use both PE and full eval (e.g. to build filtering upon PE and decide if we even need to apply any filters; to check if query could be satisfied only using partial input). So I would label this as enhancement or usability.

By saying that #1418 is not related to this issue I meant that improving default values inlining not necessarily will improve and resolve current case