diff --git a/docs/content/how-do-i-write-policies.md b/docs/content/how-do-i-write-policies.md index e502d68a13..6e5a44dac1 100644 --- a/docs/content/how-do-i-write-policies.md +++ b/docs/content/how-do-i-write-policies.md @@ -1053,6 +1053,98 @@ The result: +-----------+------------------------+ ``` +## Universal Quantification (FOR ALL) + +Like SQL, Rego does not have a direct way to express _universal quantification_ +("FOR ALL"). However, like SQL, you can use other language primitives (e.g., +[Negation](#negation)) to express FOR ALL. For example, imagine you want to +express a policy that says (in English): + +``` +There must be no apps named "bitcoin-miner". +``` + +A common mistake is to try encoding the policy with a rule named +`no_bitcoin_miners` like so: + +```ruby +no_bitcoin_miners { + app := apps[_] + app.name != "bitcoin-miner" # THIS IS NOT CORRECT. +} +``` + +It becomes clear that this is incorrect when you use the [`some`](#some-keyword) +keyword, because the rule is true whenever there is SOME app that is not a +bitcoin-miner: + +```ruby +no_bitcoin_miners { + some i + app := apps[i] + app.name != "bitcoin-miner" +} +``` + +You can confirm this by testing the rule inside the REPL: + +```ruby +> no_bitcoin_miners with apps as [{"name": "bitcoin-miner"}, {"name": "web"}] +true +``` + +The reason the rule is incorrect is that variables in Rego are _existentially +quantified_. This means that rule bodies and queries express FOR ANY and not FOR +ALL. To express FOR ALL in Rego complement the logic in the rule body (e.g., +`!=` becomes `==`) and then complement the check using negation (e.g., +`no_bitcoin_miners` becomes `not any_bitcoin_miners`). + +For this policy, you define a rule that finds if there exists a bitcoin-mining +app (which is easy using the `some` keyword). And then you use negation to check +that there is NO bitcoin-mining app. Technically, you're using 2 negations and +an existential quantifier, which is logically the same as a universal +quantifier. + +For example: + +```ruby +no_bitcoin_miners_using_negation { + not any_bitcoin_miners +} + +any_bitcoin_miners { + some i + app := apps[i] + app.name == "bitcoin-miner" +} +``` + +```ruby +> no_bitcoin_miners_using_negation with apps as [{"name": "web"}] +true +> no_bitcoin_miners_using_negation with apps as [{"name": "bitcoin-miner"}, {"name": "web"}] +undefined +``` + +> The `undefined` result above is expected because we did not define a default +> value for `no_bitcoin_miners_using_negation`. Since the body of the rule fails +> to match, there is no value generated. + +Alternatively, we can implement the same kind of logic inside a single rule +using [Comprehensions](#comprehensions). + +```ruby +no_bitcoin_miners_using_comprehension { + bitcoin_miners := {app | app := apps[_]; app.name == "bitcoin-miner"} + count(bitcoin_miners) == 0 +} +``` + +> Whether you use negation or comprehensions to express FOR ALL is up to you. +> The comprehension version is more concise and does not require a helper rule +> while the negation version is more verbose but a bit simpler and allows for +> more complex ORs. + ## Modules In Rego, policies are defined inside *modules*. Modules consist of: diff --git a/docs/content/language-cheatsheet.md b/docs/content/language-cheatsheet.md index 0f24a8bfcb..963d6e5a86 100644 --- a/docs/content/language-cheatsheet.md +++ b/docs/content/language-cheatsheet.md @@ -74,6 +74,9 @@ not obj.foo.bar.bar # check if "foo" belongs to the set a_set["foo"] +# check if "foo" DOES NOT belong to the set +not a_set["foo"] + # check if the array ["a", "b", "c"] belongs to the set a_set[["a", "b", "c"]] @@ -132,6 +135,34 @@ foo[k1] == foo[k2]; k1 != k2 foo[k].bar.baz[i] == 7; foo[k].qux > 3 ``` +#### For All + +```ruby +# assert no values in set match predicate +count({x | set[x]; f(x)}) == 0 + +# assert all values in set make function f true +count({x | set[x]; f(x)}) == count(set) + +# assert no values in set make function f true (using negation and helper rule) +not any_match + +# assert all values in set make function f true (using negation and helper rule) +not any_not_match +``` + +```ruby +any_match { + set[x] + f(x) +} + +any_not_match { + set[x] + not f(x) +} +``` + ## Rules In the examples below `...` represents one or more conditions.