Skip to content

Commit fd5af26

Browse files
TristonianJonescopybara-github
TristonianJones
authored and
copybara-github
committed
Support protobuf Well-Known Types in the cel-verifier CLI and REPL.
PiperOrigin-RevId: 1001131884
1 parent 04050ab commit fd5af26

7 files changed

Lines changed: 181 additions & 1 deletion

File tree

‎verifier/src/main/java/dev/cel/verifier/tools/BUILD.bazel‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -45,6 +45,8 @@ java_library(
4545
"//common:cel_ast",
4646
"//common:compiler_common",
4747
"//common:options",
48+
"//common/internal:cel_descriptor_pools",
49+
"//common/internal:well_known_proto",
4850
"//common/types",
4951
"//common/types:cel_types",
5052
"//common/types:type_providers",
@@ -64,6 +66,7 @@ java_library(
6466
"//verifier:verifier_factory",
6567
"@maven//:com_google_errorprone_error_prone_annotations",
6668
"@maven//:com_google_guava_guava",
69+
"@maven//:com_google_protobuf_protobuf_java",
6770
"@maven//:info_picocli_picocli",
6871
],
6972
)

‎verifier/src/main/java/dev/cel/verifier/tools/CelVerifierRepl.java‎

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -315,7 +315,9 @@ private static void printHelp(String topic, PrintStream out) {
315315
out.println();
316316
out.println("Supported Types:");
317317
out.println(" - Primitive types: int, uint, string, bool, double, bytes, dyn");
318-
out.println(" - Well-known types: timestamp, duration");
318+
out.println(
319+
" - Well-known types: timestamp, duration, Value, Struct, ListValue, *Value"
320+
+ " (google.protobuf.*)");
319321
out.println(" - List types: list<T> (e.g., list<int>, list<string>)");
320322
out.println(" - Map types: map<K,V> (e.g., map<string,int>, map<string,string>)");
321323
out.println(" - Optional types: optional<T> (e.g., optional<string>, optional<int>)");
@@ -329,6 +331,7 @@ private static void printHelp(String topic, PrintStream out) {
329331
out.println(" cel-verifier> :var created_at timestamp");
330332
out.println(" cel-verifier> :var timeout duration");
331333
out.println(" cel-verifier> :var opt_flag optional<bool>");
334+
out.println(" cel-verifier> :var count google.protobuf.Int64Value");
332335
break;
333336
case "unknown":
334337
out.println("Command: :unknown <identifier>");

‎verifier/src/main/java/dev/cel/verifier/tools/CelVerifierToolCore.java‎

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,12 +14,18 @@
1414

1515
package dev.cel.verifier.tools;
1616

17+
import static com.google.common.collect.ImmutableList.toImmutableList;
18+
19+
import com.google.common.collect.ImmutableList;
1720
import com.google.common.collect.ImmutableMap;
21+
import com.google.protobuf.Descriptors.Descriptor;
1822
import dev.cel.bundle.Cel;
1923
import dev.cel.bundle.CelBuilder;
2024
import dev.cel.bundle.CelFactory;
2125
import dev.cel.common.CelAbstractSyntaxTree;
2226
import dev.cel.common.CelOptions;
27+
import dev.cel.common.internal.DefaultDescriptorPool;
28+
import dev.cel.common.internal.WellKnownProto;
2329
import dev.cel.common.types.CelType;
2430
import dev.cel.compiler.CelCompiler;
2531
import dev.cel.compiler.CelCompilerBuilder;
@@ -42,6 +48,26 @@
4248
/** Core decoupled engine that executes formal verification operations. */
4349
final class CelVerifierToolCore {
4450

51+
private static final ImmutableList<Descriptor> WELL_KNOWN_DESCRIPTORS =
52+
ImmutableList.of(
53+
WellKnownProto.DURATION,
54+
WellKnownProto.JSON_LIST_VALUE,
55+
WellKnownProto.JSON_STRUCT_VALUE,
56+
WellKnownProto.JSON_VALUE,
57+
WellKnownProto.TIMESTAMP,
58+
WellKnownProto.FLOAT_VALUE,
59+
WellKnownProto.INT32_VALUE,
60+
WellKnownProto.INT64_VALUE,
61+
WellKnownProto.STRING_VALUE,
62+
WellKnownProto.BOOL_VALUE,
63+
WellKnownProto.BYTES_VALUE,
64+
WellKnownProto.DOUBLE_VALUE,
65+
WellKnownProto.UINT32_VALUE,
66+
WellKnownProto.UINT64_VALUE)
67+
.stream()
68+
.map(DefaultDescriptorPool::getWellKnownProtoDescriptor)
69+
.collect(toImmutableList());
70+
4571
private CelVerifierToolCore() {}
4672

4773
/** Checks if a single CEL expression is satisfiable. */
@@ -108,6 +134,7 @@ static CelCompiler buildCompiler(Map<String, CelType> variables) {
108134
CelCompilerBuilder builder =
109135
CelCompilerFactory.standardCelCompilerBuilder()
110136
.setStandardMacros(CelStandardMacro.STANDARD_MACROS)
137+
.addMessageTypes(WELL_KNOWN_DESCRIPTORS)
111138
.addLibraries(
112139
CelExtensions.bindings(),
113140
CelExtensions.comprehensions(),
@@ -129,6 +156,7 @@ static Cel buildCel(Map<String, CelType> variables) {
129156
CelBuilder celBuilder =
130157
CelFactory.plannerCelBuilder()
131158
.setStandardMacros(CelStandardMacro.STANDARD_MACROS)
159+
.addMessageTypes(WELL_KNOWN_DESCRIPTORS)
132160
.addCompilerLibraries(
133161
CelExtensions.optional(),
134162
CelExtensions.bindings(),

‎verifier/src/main/java/dev/cel/verifier/tools/VerificationOptions.java‎

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,7 @@
2121
import dev.cel.common.types.CelType;
2222
import dev.cel.common.types.ListType;
2323
import dev.cel.common.types.MapType;
24+
import dev.cel.common.types.NullableType;
2425
import dev.cel.common.types.OptionalType;
2526
import dev.cel.common.types.SimpleType;
2627
import java.time.Duration;
@@ -211,6 +212,27 @@ static CelType parseCelType(String typeStr) {
211212
case "duration":
212213
case "google.protobuf.duration":
213214
return SimpleType.DURATION;
215+
case "google.protobuf.value":
216+
return SimpleType.DYN;
217+
case "google.protobuf.struct":
218+
return MapType.create(SimpleType.STRING, SimpleType.DYN);
219+
case "google.protobuf.listvalue":
220+
return ListType.create(SimpleType.DYN);
221+
case "google.protobuf.boolvalue":
222+
return NullableType.create(SimpleType.BOOL);
223+
case "google.protobuf.bytesvalue":
224+
return NullableType.create(SimpleType.BYTES);
225+
case "google.protobuf.doublevalue":
226+
case "google.protobuf.floatvalue":
227+
return NullableType.create(SimpleType.DOUBLE);
228+
case "google.protobuf.int32value":
229+
case "google.protobuf.int64value":
230+
return NullableType.create(SimpleType.INT);
231+
case "google.protobuf.uint32value":
232+
case "google.protobuf.uint64value":
233+
return NullableType.create(SimpleType.UINT);
234+
case "google.protobuf.stringvalue":
235+
return NullableType.create(SimpleType.STRING);
214236
default:
215237
// TODO: Support protobuf message types (coming soon).
216238
throw new IllegalArgumentException(

‎verifier/src/test/java/dev/cel/verifier/tools/CelVerifierReplTest.java‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -248,6 +248,26 @@ public void repl_optionalQueries() throws Exception {
248248
assertThat(output[1]).isEmpty();
249249
}
250250

251+
@Test
252+
public void repl_wellKnownTypeQueries() throws Exception {
253+
String[] output =
254+
runReplWithCommands(
255+
":help var",
256+
":var count google.protobuf.Int64Value",
257+
":var payload google.protobuf.Struct",
258+
":vars",
259+
"equiv google.protobuf.Int64Value{value: 42} == count <=> count == 42",
260+
"equiv google.protobuf.Struct{fields: {'k': google.protobuf.Value{string_value: 'v'}}}"
261+
+ " <=> {'k': 'v'}",
262+
":quit");
263+
264+
assertThat(output[0]).contains("Value, Struct, ListValue, *Value (google.protobuf.*)");
265+
assertThat(output[0]).contains("Variable declared: count : wrapper(int)");
266+
assertThat(output[0]).contains("Variable declared: payload : map(string, dyn)");
267+
assertThat(output[0]).contains("[VERIFIED]");
268+
assertThat(output[1]).isEmpty();
269+
}
270+
251271
@Test
252272
public void repl_unknownCommandsAndErrors() throws Exception {
253273
String[] output =

‎verifier/src/test/java/dev/cel/verifier/tools/CelVerifierToolTest.java‎

Lines changed: 73 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -328,6 +328,79 @@ public void verifyEquivalence_canonicalizedMapComprehension() throws Exception {
328328
assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED);
329329
}
330330

331+
@Test
332+
public void verifyEquivalence_wellKnownTypesSupportedByDefault() throws Exception {
333+
VerificationOptions options =
334+
VerificationOptions.builder().setTimeout(Duration.ofSeconds(5)).build();
335+
ImmutableMap<String, CelType> vars =
336+
VerificationOptions.parseVariables(
337+
Arrays.asList("x:int", "w:google.protobuf.Int64Value", "s:google.protobuf.Struct"));
338+
339+
assertThat(
340+
CelVerifierToolCore.verifyEquivalence(
341+
"google.protobuf.Struct{fields: {'a': google.protobuf.Value{number_value: 1.0},"
342+
+ " ?'b': optional.none()}}",
343+
"{'a': 1.0}",
344+
vars,
345+
options)
346+
.status())
347+
.isEqualTo(VerificationStatus.VERIFIED);
348+
assertThat(
349+
CelVerifierToolCore.verifyEquivalence(
350+
"google.protobuf.ListValue{values: [google.protobuf.Value{string_value: 'x'}]}",
351+
"['x']",
352+
vars,
353+
options)
354+
.status())
355+
.isEqualTo(VerificationStatus.VERIFIED);
356+
assertThat(
357+
CelVerifierToolCore.verifyEquivalence(
358+
"google.protobuf.Int64Value{value: x} == x"
359+
+ " && google.protobuf.Int64Value{} == 0"
360+
+ " && google.protobuf.StringValue{value: 'hi'} == 'hi'",
361+
"true",
362+
vars,
363+
options)
364+
.status())
365+
.isEqualTo(VerificationStatus.VERIFIED);
366+
assertThat(
367+
CelVerifierToolCore.verifyEquivalence(
368+
"google.protobuf.Timestamp{seconds: 100} == timestamp(100)"
369+
+ " && google.protobuf.Timestamp{seconds: 100, nanos: 500} > timestamp(100)"
370+
+ " && google.protobuf.Duration{seconds: 50}"
371+
+ " == timestamp(150) - timestamp(100)",
372+
"true",
373+
vars,
374+
options)
375+
.status())
376+
.isEqualTo(VerificationStatus.VERIFIED);
377+
assertThat(
378+
CelVerifierToolCore.verifyEquivalence(
379+
"w == null || w == google.protobuf.Int64Value{value: w}",
380+
"true",
381+
vars,
382+
options)
383+
.status())
384+
.isEqualTo(VerificationStatus.VERIFIED);
385+
String yamlPolicy =
386+
"name: wkt_policy\n"
387+
+ "rule:\n"
388+
+ " match:\n"
389+
+ " - condition: \"w == google.protobuf.Int64Value{value: 10}\"\n"
390+
+ " output: 'true'\n"
391+
+ " - output: 'false'\n"
392+
+ "verification:\n"
393+
+ " invariants:\n"
394+
+ " - id: wkt_check\n"
395+
+ " assert:\n"
396+
+ " - \"w != 10 || w == google.protobuf.Int64Value{value: 10}\"\n";
397+
assertThat(
398+
CelVerifierToolCore.verifyPolicyInvariants(yamlPolicy, vars, options)
399+
.get("wkt_check")
400+
.status())
401+
.isEqualTo(VerificationStatus.VERIFIED);
402+
}
403+
331404
@Test
332405
public void verifyPolicyInvariants_success() throws Exception {
333406
String yamlPolicy =

‎verifier/src/test/java/dev/cel/verifier/tools/VerificationOptionsTest.java‎

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,7 @@
2222
import dev.cel.common.types.CelType;
2323
import dev.cel.common.types.ListType;
2424
import dev.cel.common.types.MapType;
25+
import dev.cel.common.types.NullableType;
2526
import dev.cel.common.types.OptionalType;
2627
import dev.cel.common.types.SimpleType;
2728
import dev.cel.verifier.tools.VerificationOptions.OutputFormat;
@@ -123,6 +124,36 @@ public void parseCelType_timestampAndDuration() {
123124
.isEqualTo(SimpleType.DURATION);
124125
}
125126

127+
@Test
128+
public void parseCelType_wellKnownTypes() {
129+
assertThat(VerificationOptions.parseCelType("google.protobuf.Value")).isEqualTo(SimpleType.DYN);
130+
assertThat(VerificationOptions.parseCelType("google.protobuf.Struct"))
131+
.isEqualTo(MapType.create(SimpleType.STRING, SimpleType.DYN));
132+
assertThat(VerificationOptions.parseCelType("google.protobuf.ListValue"))
133+
.isEqualTo(ListType.create(SimpleType.DYN));
134+
assertThat(VerificationOptions.parseCelType("google.protobuf.BoolValue"))
135+
.isEqualTo(NullableType.create(SimpleType.BOOL));
136+
assertThat(VerificationOptions.parseCelType("google.protobuf.BytesValue"))
137+
.isEqualTo(NullableType.create(SimpleType.BYTES));
138+
assertThat(VerificationOptions.parseCelType("google.protobuf.DoubleValue"))
139+
.isEqualTo(NullableType.create(SimpleType.DOUBLE));
140+
assertThat(VerificationOptions.parseCelType("google.protobuf.FloatValue"))
141+
.isEqualTo(NullableType.create(SimpleType.DOUBLE));
142+
assertThat(VerificationOptions.parseCelType("google.protobuf.Int32Value"))
143+
.isEqualTo(NullableType.create(SimpleType.INT));
144+
assertThat(VerificationOptions.parseCelType("google.protobuf.Int64Value"))
145+
.isEqualTo(NullableType.create(SimpleType.INT));
146+
assertThat(VerificationOptions.parseCelType("google.protobuf.UInt32Value"))
147+
.isEqualTo(NullableType.create(SimpleType.UINT));
148+
assertThat(VerificationOptions.parseCelType("google.protobuf.UInt64Value"))
149+
.isEqualTo(NullableType.create(SimpleType.UINT));
150+
assertThat(VerificationOptions.parseCelType("google.protobuf.StringValue"))
151+
.isEqualTo(NullableType.create(SimpleType.STRING));
152+
assertThrows(
153+
IllegalArgumentException.class,
154+
() -> VerificationOptions.parseCelType("google.protobuf.Any"));
155+
}
156+
126157
@Test
127158
public void parseCelType_optionalTypes() {
128159
assertThat(VerificationOptions.parseCelType("optional<int>"))

0 commit comments

Comments
 (0)