docs: Add documentation for the future.keywords.not import (#8641)

Fixes: #8556

Signed-off-by: Johan Fylling <johan.dev@fylling.se>

.github/actions/build-opa/action.yml

@@ -0,0 +1,20 @@
+name: 'Build OPA'
+description: 'Build OPA from source and add to PATH'
+
+inputs:
+  go-version-file:
+    description: 'Path to .go-version file'
+    required: false
+    default: '.go-version'
+
+runs:
+  using: 'composite'
+  steps:
+    - name: Setup Go
+      uses: actions/setup-go@4a3601121dd01d1626a1e23e37211e3254c1c06c # v6.4.0
+      with:
+        go-version-file: ${{ inputs.go-version-file }}
+
+    - name: Build OPA
+      shell: bash
+      run: go install .

.github/workflows/pull-request.yaml

@@ -590,10 +590,8 @@ jobs:
       with:
         persist-credentials: false
 
-    - name: Setup OPA
-      uses: open-policy-agent/setup-opa@b2b258e089860efaadaaf71bf6e3aecb4a3eeff1 # v2.4.0
-      with:
-        version: latest
+    - name: Build OPA
+      uses: ./.github/actions/build-opa
 
     - name: Check generated docs are up to date
       run: make docs-gen-check

CHANGELOG.md

@@ -5,6 +5,41 @@ project adheres to [Semantic Versioning](http://semver.org/).
 
 ## Unreleased
 
+### Improved Negation Semantics ([#8387](https://github.com/open-policy-agent/opa/issues/8387))
+
+This OPA release introduces a new [`future.keywords.not` import](https://www.openpolicyagent.org/docs/policy-language#improved-negation-semantics) 
+that fixes a long-standing semantic issue with negation in Rego.
+
+Without the import, the compiler expands a negated composite expression like
+`not f(g(input.x))` into a series of sub-expressions evaluated *before* the
+`not`:
+
+```
+__local0__ = input.x
+g(__local0__, __local1__)
+not f(__local1__)
+```
+
+If any sub-expression fails — for example, `input.x` is undefined or `g`
+produces an undefined result — the entire rule fails rather than the `not` succeeding.
+This is unintuitive: the user's intent is "the condition does not hold," but
+an undefined intermediate value causes a silent failure instead of the expected
+`not` result.
+
+With `import future.keywords.not`, composite-expression negation wraps the full compiler 
+expansion in an implicit body:
+
+```
+not { __local0__ = input.x; g(__local0__, __local1__); f(__local1__) }
+```
+
+Now, if *any* sub-expression is undefined or fails, the body is unsatisfiable
+and the `not` expression succeeds; matching the intuition that "the condition does not hold."
+
+> **_NOTE:_**
+>
+> Users are recommended to import `future.keywords.not` whenever the `not` keyword is used in a policy.
+
 ### Rule Labels in Decision Logs
 
 Rule annotations now support a `labels` field. Labels from all successfully evaluated

docs/docs/operations.md

@@ -174,7 +174,7 @@ Features present in the list are enabled, while features not present are disable
 
 :::info
 It is recommended to use the `rego.v1` import instead of `future.keywords` imports, as this will ensure that your policy is compatible with the future release of [OPA v1.0](./v0-upgrade/)
-If the `rego.v1` import is present in a module, then `future.keywords` and `future.keywords.*` import is implied, and not allowed.
+If the `rego.v1` import is present in a module, then `future.keywords.in`, `future.keywords.every`, `future.keywords.if`, and `future.keywords.contains` imports are implied, and not allowed.
 :::
 
 The availability of future keywords in an OPA version can also be controlled using the capabilities file:

docs/docs/policy-language.md

@@ -1403,6 +1403,139 @@ Have a look at the other examples for
 about using this keyword.
 :::
 
+### Improved Negation Semantics
+
+The `future.keywords.not` import fixes a long-standing semantic issue with
+negation in Rego.
+
+#### The problem with legacy negation
+
+Without the import, the compiler expands a negated composite expression like
+`not f(g(input.x))` into a series of sub-expressions evaluated _before_ the
+`not`:
+
+```
+__local0__ = input.x
+g(__local0__, __local1__)
+not f(__local1__)
+```
+
+If any sub-expression fails — for example, `input.x` is undefined or `g`
+produces an undefined result — the entire rule fails rather than the `not` succeeding.
+This is unintuitive: the user's intent is "the condition does not hold," but
+an undefined intermediate value causes a silent failure instead of the expected
+`not` result.
+
+#### Implicit body wrapping
+
+With `import future.keywords.not`, composite-expression negation wraps the full
+compiler expansion in an implicit body:
+
+```
+not { __local0__ = input.x; g(__local0__, __local1__); f(__local1__) }
+```
+
+Now, if _any_ sub-expression is undefined or fails, the body is unsatisfiable
+and the `not` expression succeeds; matching the intuition that "the condition does not hold."
+
+```json
+{
+  "user": "cesar"
+}
+```
+
+<RunSnippet id="input.negation1.json" />
+
+```rego
+package negation
+
+import future.keywords.not
+
+# Succeeds when input.role is undefined OR when lookup/admin fail
+restricted if {
+    not admin(lookup(input.user))
+}
+
+groups := {
+    "admin": ["alice"],
+    "user": ["bob"]
+}
+
+lookup(user) := group if {
+    some group, members in groups
+    user in members
+}
+
+admin(group) if group in ["admin", "sudo"]
+```
+
+<RunSnippet files="#input.negation1.json" command="data.negation.restricted"/>
+
+:::important
+Notice how if we remove the `future.keywords.not` import in the above policy, the `restricted` rule starts failing.
+This is a consequence of the `lookup()` function failing with an `undefined` value.
+:::
+
+#### Explicit negation bodies
+
+The import also enables a `not` expression to take a curly-brace-enclosed body
+instead of a single expression:
+
+```json
+{
+  "servers": [
+    {
+      "name": "web1",
+      "listener": {
+        "port": 80,
+        "protocol": "tcp"
+      }
+    },
+    {
+      "name": "web2",
+      "listener": {
+        "port": 443,
+        "protocol": "tcp"
+      }
+    },
+    {
+      "name": "web3",
+      "listener": {
+        "port": 443,
+        "protocol": "udp"
+      }
+    }
+  ]
+}
+```
+
+<RunSnippet id="input.negation2.json" />
+
+```rego
+package negation
+
+import future.keywords.not
+
+# Deny any server that doesn't listen on TCP on port 443
+deny contains $"server {server.name} is misconfigured" if {
+    some server in input.servers
+    not {
+        # If any of the following expressions fail, the 'not' succeeds
+        listener := server.listener
+        listener.port == 443
+        listener.protocol == "tcp"
+    }
+}
+```
+
+<RunSnippet files="#input.negation2.json" command="data.negation.deny"/>
+
+The `not` succeeds when the body is **unsatisfiable**; no combination of
+variable bindings makes every expression in the body true.
+
+Variables declared inside the body (`listener` above) are scoped locally and are not
+visible outside the `not` block.
+
 ## Universal Quantification (FOR ALL)
 
 Rego allows for several ways to express universal quantification.

docs/docs/policy-reference/index.md

@@ -355,8 +355,8 @@ The reference documentation for these functions can be found under
 
 ## Reserved Names & Keywords
 
-The following words are reserved and cannot be used as variable names, rule
-names, or dot-access style reference arguments:
+The following words are reserved and cannot be used as variable names or rule
+names:
 
 - `as`
 - `contains` ([Examples](./policy-reference/keywords/contains))
@@ -394,7 +394,7 @@ rule-head-set   = "contains" term [ "if" ] | "[" term "]"
 rule-args       = term { "," term }
 rule-body       = [ "else" [ assign-operator term ] [ "if" ] ] ( "{" query "}" ) | literal
 query           = literal { ( ";" | ( [CR] LF ) ) literal }
-literal         = ( some-decl | expr | "not" expr ) { with-modifier }
+literal         = ( some-decl | expr | "not" ( expr | "{" query "}" ) ) { with-modifier }
 with-modifier   = "with" term "as" term
 some-decl       = "some" term { "," term } { "in" expr }
 expr            = term | expr-call | expr-infix | expr-every | expr-parens | unary-expr

docs/docs/policy-reference/keywords/_examples/not/negation/policy.rego

@@ -1,5 +1,7 @@
 package play
 
+import future.keywords.not
+
 deny contains "must be staff" if {
 	not "staff" in input.roles
 }

docs/docs/policy-reference/keywords/import.md

@@ -78,10 +78,32 @@ output := sprintf("Hello, %v", [p1.name])
   files="#package1.rego"
   command="data.package2"/>
 
+## Importing Future Keywords
+
+The `in`, `every`, `if`, `contains`, and `not` (semantic update) keywords
+have been introduced to the Rego language over time, and in order to prevent
+them from breaking policies that existed before their introduction, an opt-in mechanism
+has been necessary. The `future.keywords.*` imports facilitate this
+opt-in mechanism. With the release of OPA v1.x, the `in`, `every`, `if`, and `contains`
+keywords have become a standard part of the Rego language, and no longer require an import.
+The `not` keyword has always been a standard part of the Rego language, but has since its introduction
+received a semantic update that requires author opt-in through importing `future.keywords.not`.
+
+### Importing `future.keywords.not`
+
+[import future.keywords.not](./not) enables the `not` body syntax
+(`not { ... }`) and implicit body wrapping for single-expression negation.
+This import is independent of the [rego.v1 import](#importing-regov1).
+
+:::important
+The `future.keywords.not` import fixes a long-standing semantic issue with negation in Rego.
+Read more about it in the [Improved Negation Semantics](../../policy-language#improved-negation-semantics) section of the Policy Language overview.
+:::
+
 ## Importing `rego.v1`
 
 In [OPA 1.0](https://www.openpolicyagent.org/docs/v0-upgrade) a number of
-previously optional keywords will be required. These settings for the Rego
+previously optional keywords are required. These settings for the Rego
 language is available in pre-1.0 versions using the `import` keyword. The two
 files that follow are equivalent.
 

docs/docs/policy-reference/keywords/not.md

@@ -14,6 +14,11 @@ allow if {
 }
 ```
 
+:::important
+The `future.keywords.not` import fixes a long-standing semantic issue with negation in Rego.
+Read more about it in the [Improved Negation Semantics](../../policy-language#improved-negation-semantics) section of the Policy Language overview.
+:::
+
 ## Examples
 
 <PlaygroundExample dir={require.context('./_examples/not/undefined/')} />

docs/docs/style-guide.md

@@ -1031,11 +1031,11 @@ of completeness, and to provide context for older policies.
 
 ### Use explicit imports for future keywords
 
-**With the introduction of the `import rego.v1` construct in OPA v0.59.0, this is no longer needed**
+**With the introduction of the `import rego.v1` construct in OPA v0.59.0, this is no longer needed for `in`, `every`, `contains`, and `if`.**
 
 In order to evolve the Rego language without breaking existing policies, many new features require importing
 ["future" keywords](https://www.openpolicyagent.org/docs/policy-language#future-keywords), like `contains`,
-`every`, `if` and `in`. While it might seem convenient to use the "catch-all" form of `import future.keywords` to
+`every`, `if`, `in` and `not`. While it might seem convenient to use the "catch-all" form of `import future.keywords` to
 import all of the future keywords, this construct risks breaking your policies when new keywords are introduced, and
 their names happen to collide with names you've used for variables or rules.
 

docs/docs/v0-compatibility.md

@@ -25,9 +25,9 @@ Users with control over their Rego and OPA deployments are instead encouraged
 to migrate their Rego to be compatible with OPA v1.0 using the below tooling options:
 
 1. The `rego.v1` import makes OPA apply all restrictions that are enforced by default in OPA v1.0.
-   If a Rego module imports `rego.v1`, it means applicable `future.keywords` imports are implied. It is illegal to import both `rego.v1` and `future.keywords` in the same module.
-2. The `--v0-v1` flag on the `opa fmt` command will rewrite existing modules to use the `rego.v1` import instead of `future.keywords` imports.
-3. The `--v0-v1` flag on the `opa check` command will check that either the `rego.v1` import or applicable `future.keywords` imports are present if any of the `in`, `every`, `if` and `contains` keywords are used in a module.
+   If a Rego module imports `rego.v1`, it means applicable `future.keywords` imports are implied. It is illegal to import both `rego.v1` and any of `future.keywords.in`, `future.keywords.every`, `future.keywords.if`, and `future.keywords.contains` in the same module.
+2. The `--v0-v1` flag on the `opa fmt` command will rewrite existing modules to use the `rego.v1` import instead of applicable `future.keywords.*` imports.
+3. The `--v0-v1` flag on the `opa check` command will check that either the `rego.v1` import or applicable `future.keywords.*` imports are present if any of the `in`, `every`, `if` and `contains` keywords are used in a module.
 
 ### v0.x compatibility mode in the OPA binary
 

docs/docs/v0-upgrade/index.md

@@ -292,8 +292,8 @@ adoption of these keywords and their usage is prevalent in the OPA
 documentation, Rego Playground, etc.
 
 In OPA v1.0 the `in`, `every`, `if` and `contains` keywords are part of the
-language by default and the `future.keywords` imports will become a no-op. A
-policy that makes use of these keywords, but doesn't import `future.keywords` is
+language by default and importing these will become a no-op. A
+policy that makes use of these keywords, but doesn't import them is
 valid in OPA v1.0 but not in older versions of OPA.
 
 ### Enforce use of `if` and `contains` keywords in rule head declarations