Skip to content

Commit 6c09d6e

Browse files
l46kokcopybara-github
l46kok
authored and
copybara-github
committed
Implement custom policy invariants verification
Enables policy authors to declare custom logical invariants (`assume` preconditions and `assert` clauses) on `CelPolicy` definitions, mathematically verifying that properties hold across all possible input states. PiperOrigin-RevId: 915170572
1 parent 4cd8411 commit 6c09d6e

23 files changed

Lines changed: 1336 additions & 16 deletions

‎policy/src/main/java/dev/cel/policy/CelPolicy.java‎

Lines changed: 144 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@
1515
package dev.cel.policy;
1616

1717
import static com.google.common.base.Preconditions.checkNotNull;
18+
import static java.util.stream.Collectors.joining;
1819

1920
import com.google.auto.value.AutoOneOf;
2021
import com.google.auto.value.AutoValue;
@@ -53,6 +54,10 @@ public abstract class CelPolicy {
5354

5455
public abstract ImmutableList<Import> imports();
5556

57+
public abstract ImmutableList<Invariant> invariants();
58+
59+
public abstract ImmutableList<Variable> verificationVariables();
60+
5661
/** Creates a new builder to construct a {@link CelPolicy} instance. */
5762
public static Builder newBuilder() {
5863
return new AutoValue_CelPolicy.Builder()
@@ -74,6 +79,8 @@ public abstract static class Builder {
7479

7580
public abstract Builder setDisplayName(ValueString displayName);
7681

82+
public abstract Rule rule();
83+
7784
public abstract Builder setRule(Rule rule);
7885

7986
public abstract Builder setPolicySource(CelPolicySource policySource);
@@ -90,6 +97,14 @@ public List<Import> imports() {
9097
return Collections.unmodifiableList(importList);
9198
}
9299

100+
abstract ImmutableList<Invariant> invariants();
101+
102+
abstract ImmutableList.Builder<Invariant> invariantsBuilder();
103+
104+
abstract ImmutableList<Variable> verificationVariables();
105+
106+
abstract ImmutableList.Builder<Variable> verificationVariablesBuilder();
107+
93108
public Map<String, Object> metadata() {
94109
return Collections.unmodifiableMap(metadata);
95110
}
@@ -106,6 +121,24 @@ public Builder addImports(Collection<Import> values) {
106121
return this;
107122
}
108123

124+
@CanIgnoreReturnValue
125+
public Builder addInvariant(Invariant value) {
126+
invariantsBuilder().add(value);
127+
return this;
128+
}
129+
130+
@CanIgnoreReturnValue
131+
public Builder addVerificationVariable(Variable value) {
132+
verificationVariablesBuilder().add(value);
133+
return this;
134+
}
135+
136+
@CanIgnoreReturnValue
137+
public Builder addVerificationVariables(Collection<Variable> values) {
138+
verificationVariablesBuilder().addAll(values);
139+
return this;
140+
}
141+
109142
@CanIgnoreReturnValue
110143
public Builder putMetadata(String key, Object value) {
111144
metadata.put(key, value);
@@ -328,4 +361,115 @@ public static Import create(long id, ValueString name) {
328361
return new AutoValue_CelPolicy_Import(id, name);
329362
}
330363
}
364+
365+
/**
366+
* Invariant declares a required logical property that must hold true under specified
367+
* preconditions.
368+
*/
369+
@AutoValue
370+
public abstract static class Invariant {
371+
public abstract long id();
372+
373+
public abstract ValueString invariantId();
374+
375+
public abstract Optional<ValueString> description();
376+
377+
public abstract ImmutableList<ValueString> assume();
378+
379+
public abstract ImmutableList<ValueString> assertClause();
380+
381+
public String assumeSourceString() {
382+
if (assume().isEmpty()) {
383+
return "true";
384+
}
385+
if (assume().size() == 1) {
386+
return assume().get(0).value();
387+
}
388+
return assume().stream().map(v -> "(" + v.value() + ")").collect(joining(" && "));
389+
}
390+
391+
public String assertSourceString() {
392+
if (assertClause().isEmpty()) {
393+
return "true";
394+
}
395+
if (assertClause().size() == 1) {
396+
return assertClause().get(0).value();
397+
}
398+
return assertClause().stream().map(v -> "(" + v.value() + ")").collect(joining(" && "));
399+
}
400+
401+
/** Builder for {@link Invariant}. */
402+
@AutoValue.Builder
403+
public abstract static class Builder implements RequiredFieldsChecker {
404+
public abstract Builder setId(long value);
405+
406+
abstract Optional<ValueString> invariantId();
407+
408+
abstract ImmutableList<ValueString> assume();
409+
410+
abstract ImmutableList.Builder<ValueString> assumeBuilder();
411+
412+
abstract ImmutableList<ValueString> assertClause();
413+
414+
abstract ImmutableList.Builder<ValueString> assertClauseBuilder();
415+
416+
public abstract Builder setInvariantId(ValueString value);
417+
418+
public abstract Builder setDescription(ValueString value);
419+
420+
public Builder setAssume(ValueString value) {
421+
return setAssume(ImmutableList.of(value));
422+
}
423+
424+
abstract Builder setAssume(ImmutableList<ValueString> values);
425+
426+
@CanIgnoreReturnValue
427+
public Builder addAssume(ValueString value) {
428+
assumeBuilder().add(value);
429+
return this;
430+
}
431+
432+
@CanIgnoreReturnValue
433+
public Builder addAssume(Iterable<ValueString> values) {
434+
assumeBuilder().addAll(values);
435+
return this;
436+
}
437+
438+
public Builder setAssertClause(ValueString value) {
439+
return setAssertClause(ImmutableList.of(value));
440+
}
441+
442+
abstract Builder setAssertClause(ImmutableList<ValueString> values);
443+
444+
@CanIgnoreReturnValue
445+
public Builder addAssertClause(ValueString value) {
446+
assertClauseBuilder().add(value);
447+
return this;
448+
}
449+
450+
@CanIgnoreReturnValue
451+
public Builder addAssertClause(Iterable<ValueString> values) {
452+
assertClauseBuilder().addAll(values);
453+
return this;
454+
}
455+
456+
@Override
457+
public ImmutableList<RequiredField> requiredFields() {
458+
return ImmutableList.of(
459+
RequiredField.of("id", this::invariantId),
460+
RequiredField.of(
461+
"assert",
462+
() ->
463+
assertClause().isEmpty()
464+
? Optional.empty()
465+
: Optional.of(assertClause().get(0))));
466+
}
467+
468+
public abstract Invariant build();
469+
}
470+
471+
public static Builder newBuilder(long id) {
472+
return new AutoValue_CelPolicy_Invariant.Builder().setId(id);
473+
}
474+
}
331475
}

‎policy/src/main/java/dev/cel/policy/CelPolicyYamlParser.java‎

Lines changed: 141 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@
1515
package dev.cel.policy;
1616

1717
import static com.google.common.base.Preconditions.checkNotNull;
18+
import static com.google.common.collect.ImmutableSet.toImmutableSet;
1819
import static dev.cel.common.formats.YamlHelper.ERROR;
1920
import static dev.cel.common.formats.YamlHelper.assertRequiredFields;
2021
import static dev.cel.common.formats.YamlHelper.assertYamlType;
@@ -28,6 +29,7 @@
2829
import dev.cel.common.formats.YamlParserContextImpl;
2930
import dev.cel.common.internal.CelCodePointArray;
3031
import dev.cel.policy.CelPolicy.Import;
32+
import dev.cel.policy.CelPolicy.Invariant;
3133
import dev.cel.policy.CelPolicy.Match;
3234
import dev.cel.policy.CelPolicy.Match.Result;
3335
import dev.cel.policy.CelPolicy.Variable;
@@ -47,6 +49,8 @@ final class CelPolicyYamlParser implements CelPolicyParser {
4749
Match.newBuilder(0).setCondition(ERROR_VALUE).setResult(Result.ofOutput(ERROR_VALUE)).build();
4850
private static final Variable ERROR_VARIABLE =
4951
Variable.newBuilder().setExpression(ERROR_VALUE).setName(ERROR_VALUE).build();
52+
private static final Invariant ERROR_INVARIANT =
53+
Invariant.newBuilder(0).setInvariantId(ERROR_VALUE).setAssertClause(ERROR_VALUE).build();
5054

5155
private final TagVisitor<Node> tagVisitor;
5256
private final boolean enableSimpleVariables;
@@ -137,17 +141,82 @@ public CelPolicy parsePolicy(PolicyParserContext<Node> ctx, Node node) {
137141
case "rule":
138142
policyBuilder.setRule(parseRule(ctx, policyBuilder, valueNode));
139143
break;
144+
case "verification":
145+
parseVerification(policyBuilder, ctx, valueNode);
146+
break;
140147
default:
141148
tagVisitor.visitPolicyTag(ctx, keyId, fieldName, valueNode, policyBuilder);
142149
break;
143150
}
144151
}
145152

153+
ImmutableSet<String> ruleVarNames =
154+
policyBuilder.rule().variables().stream()
155+
.map(v -> v.name().value())
156+
.filter(name -> !name.equals(ERROR_VALUE.value()))
157+
.collect(toImmutableSet());
158+
for (Variable verVar : policyBuilder.verificationVariables()) {
159+
if (verVar.name().id() != 0
160+
&& !verVar.name().value().equals(ERROR_VALUE.value())
161+
&& ruleVarNames.contains(verVar.name().value())) {
162+
ctx.reportError(
163+
verVar.name().id(),
164+
"Duplicate variable name '"
165+
+ verVar.name().value()
166+
+ "' in verification.variables; already defined in rule.variables");
167+
}
168+
}
169+
146170
return policyBuilder
147171
.setPolicySource(policySource.toBuilder().setPositionsMap(ctx.getIdToOffsetMap()).build())
148172
.build();
149173
}
150174

175+
private void parseVerification(
176+
CelPolicy.Builder policyBuilder, PolicyParserContext<Node> ctx, Node node) {
177+
long id = ctx.collectMetadata(node);
178+
if (!assertYamlType(ctx, id, node, YamlNodeType.MAP)) {
179+
return;
180+
}
181+
MappingNode mappingNode = (MappingNode) node;
182+
for (NodeTuple nodeTuple : mappingNode.getValue()) {
183+
Node key = nodeTuple.getKeyNode();
184+
long keyId = ctx.collectMetadata(key);
185+
if (!assertYamlType(ctx, keyId, key, YamlNodeType.STRING, YamlNodeType.TEXT)) {
186+
continue;
187+
}
188+
String fieldName = ((ScalarNode) key).getValue();
189+
Node valueNode = nodeTuple.getValueNode();
190+
switch (fieldName) {
191+
case "invariants": {
192+
long valueId = ctx.collectMetadata(valueNode);
193+
if (!assertYamlType(ctx, valueId, valueNode, YamlNodeType.LIST)) {
194+
continue;
195+
}
196+
SequenceNode invariantListNode = (SequenceNode) valueNode;
197+
for (Node invariantNode : invariantListNode.getValue()) {
198+
policyBuilder.addInvariant(parseInvariant(ctx, policyBuilder, invariantNode));
199+
}
200+
break;
201+
}
202+
case "variables": {
203+
long valueId = ctx.collectMetadata(valueNode);
204+
if (!assertYamlType(ctx, valueId, valueNode, YamlNodeType.LIST)) {
205+
continue;
206+
}
207+
SequenceNode variableListNode = (SequenceNode) valueNode;
208+
for (Node varNode : variableListNode.getValue()) {
209+
policyBuilder.addVerificationVariable(parseVariable(ctx, policyBuilder, varNode));
210+
}
211+
break;
212+
}
213+
default:
214+
ctx.reportError(keyId, "Unexpected key in verification block: " + fieldName);
215+
break;
216+
}
217+
}
218+
}
219+
151220
private void parseImports(
152221
CelPolicy.Builder policyBuilder, PolicyParserContext<Node> ctx, Node node) {
153222
long id = ctx.collectMetadata(node);
@@ -409,6 +478,78 @@ private Variable parseVariableObject(
409478
return builder.build();
410479
}
411480

481+
@Override
482+
public CelPolicy.Invariant parseInvariant(
483+
PolicyParserContext<Node> ctx, CelPolicy.Builder policyBuilder, Node node) {
484+
long id = ctx.collectMetadata(node);
485+
Invariant.Builder builder = Invariant.newBuilder(id);
486+
if (!assertYamlType(ctx, id, node, YamlNodeType.MAP)) {
487+
return ERROR_INVARIANT;
488+
}
489+
490+
MappingNode invariantMap = (MappingNode) node;
491+
for (NodeTuple nodeTuple : invariantMap.getValue()) {
492+
Node keyNode = nodeTuple.getKeyNode();
493+
long keyId = ctx.collectMetadata(keyNode);
494+
if (!assertYamlType(ctx, keyId, keyNode, YamlNodeType.STRING, YamlNodeType.TEXT)) {
495+
continue;
496+
}
497+
Node valueNode = nodeTuple.getValueNode();
498+
String keyName = ((ScalarNode) keyNode).getValue();
499+
switch (keyName) {
500+
case "id":
501+
builder.setInvariantId(ctx.newYamlString(valueNode));
502+
break;
503+
case "description":
504+
builder.setDescription(ctx.newYamlString(valueNode));
505+
break;
506+
case "assume":
507+
if (assertYamlType(
508+
ctx,
509+
ctx.collectMetadata(valueNode),
510+
valueNode,
511+
YamlNodeType.STRING,
512+
YamlNodeType.TEXT,
513+
YamlNodeType.LIST)) {
514+
if (valueNode instanceof SequenceNode) {
515+
for (Node itemNode : ((SequenceNode) valueNode).getValue()) {
516+
builder.addAssume(ctx.newSourceString(itemNode));
517+
}
518+
} else {
519+
builder.addAssume(ctx.newSourceString(valueNode));
520+
}
521+
}
522+
break;
523+
case "assert":
524+
if (assertYamlType(
525+
ctx,
526+
ctx.collectMetadata(valueNode),
527+
valueNode,
528+
YamlNodeType.STRING,
529+
YamlNodeType.TEXT,
530+
YamlNodeType.LIST)) {
531+
if (valueNode instanceof SequenceNode) {
532+
for (Node itemNode : ((SequenceNode) valueNode).getValue()) {
533+
builder.addAssertClause(ctx.newSourceString(itemNode));
534+
}
535+
} else {
536+
builder.addAssertClause(ctx.newSourceString(valueNode));
537+
}
538+
}
539+
break;
540+
default:
541+
ctx.reportError(keyId, "Unexpected key in invariant block: " + keyName);
542+
break;
543+
}
544+
}
545+
546+
if (!assertRequiredFields(ctx, id, builder.getMissingRequiredFieldNames())) {
547+
return ERROR_INVARIANT;
548+
}
549+
550+
return builder.build();
551+
}
552+
412553
private ParserImpl(
413554
TagVisitor<Node> tagVisitor,
414555
boolean enableSimpleVariables,

‎policy/src/main/java/dev/cel/policy/PolicyParserContext.java‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@
1616

1717
import com.google.auto.value.AutoValue;
1818
import dev.cel.common.formats.ParserContext;
19+
import dev.cel.policy.CelPolicy.Invariant;
1920
import dev.cel.policy.CelPolicy.Match;
2021
import dev.cel.policy.CelPolicy.Rule;
2122
import dev.cel.policy.CelPolicy.Variable;
@@ -51,4 +52,6 @@ static NewPolicyMetadata create(CelPolicySource source, long id) {
5152
Match parseMatch(PolicyParserContext<T> ctx, CelPolicy.Builder policyBuilder, T node);
5253

5354
Variable parseVariable(PolicyParserContext<T> ctx, CelPolicy.Builder policyBuilder, T node);
55+
56+
Invariant parseInvariant(PolicyParserContext<T> ctx, CelPolicy.Builder policyBuilder, T node);
5457
}

‎policy/src/test/java/dev/cel/policy/BUILD.bazel‎

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -8,9 +8,7 @@ package(
88
java_library(
99
name = "tests",
1010
testonly = True,
11-
srcs = glob(
12-
["*.java"],
13-
),
11+
srcs = glob(["*.java"]),
1412
data = [
1513
"@cel_policy//conformance:testdata",
1614
],

0 commit comments

Comments
 (0)