Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions verifier/src/main/java/dev/cel/verifier/tools/BUILD.bazel
Original file line number Diff line number Diff line change
Expand Up @@ -45,6 +45,8 @@ java_library(
"//common:cel_ast",
"//common:compiler_common",
"//common:options",
"//common/internal:cel_descriptor_pools",
"//common/internal:well_known_proto",
"//common/types",
"//common/types:cel_types",
"//common/types:type_providers",
Expand All @@ -64,6 +66,7 @@ java_library(
"//verifier:verifier_factory",
"@maven//:com_google_errorprone_error_prone_annotations",
"@maven//:com_google_guava_guava",
"@maven//:com_google_protobuf_protobuf_java",
"@maven//:info_picocli_picocli",
],
)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -315,7 +315,9 @@ private static void printHelp(String topic, PrintStream out) {
out.println();
out.println("Supported Types:");
out.println(" - Primitive types: int, uint, string, bool, double, bytes, dyn");
out.println(" - Well-known types: timestamp, duration");
out.println(
" - Well-known types: timestamp, duration, Value, Struct, ListValue, *Value"
+ " (google.protobuf.*)");
out.println(" - List types: list<T> (e.g., list<int>, list<string>)");
out.println(" - Map types: map<K,V> (e.g., map<string,int>, map<string,string>)");
out.println(" - Optional types: optional<T> (e.g., optional<string>, optional<int>)");
Expand All @@ -329,6 +331,7 @@ private static void printHelp(String topic, PrintStream out) {
out.println(" cel-verifier> :var created_at timestamp");
out.println(" cel-verifier> :var timeout duration");
out.println(" cel-verifier> :var opt_flag optional<bool>");
out.println(" cel-verifier> :var count google.protobuf.Int64Value");
break;
case "unknown":
out.println("Command: :unknown <identifier>");
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -14,12 +14,18 @@

package dev.cel.verifier.tools;

import static com.google.common.collect.ImmutableList.toImmutableList;

import com.google.common.collect.ImmutableList;
import com.google.common.collect.ImmutableMap;
import com.google.protobuf.Descriptors.Descriptor;
import dev.cel.bundle.Cel;
import dev.cel.bundle.CelBuilder;
import dev.cel.bundle.CelFactory;
import dev.cel.common.CelAbstractSyntaxTree;
import dev.cel.common.CelOptions;
import dev.cel.common.internal.DefaultDescriptorPool;
import dev.cel.common.internal.WellKnownProto;
import dev.cel.common.types.CelType;
import dev.cel.compiler.CelCompiler;
import dev.cel.compiler.CelCompilerBuilder;
Expand All @@ -42,6 +48,26 @@
/** Core decoupled engine that executes formal verification operations. */
final class CelVerifierToolCore {

private static final ImmutableList<Descriptor> WELL_KNOWN_DESCRIPTORS =
ImmutableList.of(
WellKnownProto.DURATION,
WellKnownProto.JSON_LIST_VALUE,
WellKnownProto.JSON_STRUCT_VALUE,
WellKnownProto.JSON_VALUE,
WellKnownProto.TIMESTAMP,
WellKnownProto.FLOAT_VALUE,
WellKnownProto.INT32_VALUE,
WellKnownProto.INT64_VALUE,
WellKnownProto.STRING_VALUE,
WellKnownProto.BOOL_VALUE,
WellKnownProto.BYTES_VALUE,
WellKnownProto.DOUBLE_VALUE,
WellKnownProto.UINT32_VALUE,
WellKnownProto.UINT64_VALUE)
.stream()
.map(DefaultDescriptorPool::getWellKnownProtoDescriptor)
.collect(toImmutableList());

private CelVerifierToolCore() {}

/** Checks if a single CEL expression is satisfiable. */
Expand Down Expand Up @@ -108,6 +134,7 @@ static CelCompiler buildCompiler(Map<String, CelType> variables) {
CelCompilerBuilder builder =
CelCompilerFactory.standardCelCompilerBuilder()
.setStandardMacros(CelStandardMacro.STANDARD_MACROS)
.addMessageTypes(WELL_KNOWN_DESCRIPTORS)
.addLibraries(
CelExtensions.bindings(),
CelExtensions.comprehensions(),
Expand All @@ -129,6 +156,7 @@ static Cel buildCel(Map<String, CelType> variables) {
CelBuilder celBuilder =
CelFactory.plannerCelBuilder()
.setStandardMacros(CelStandardMacro.STANDARD_MACROS)
.addMessageTypes(WELL_KNOWN_DESCRIPTORS)
.addCompilerLibraries(
CelExtensions.optional(),
CelExtensions.bindings(),
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,7 @@
import dev.cel.common.types.CelType;
import dev.cel.common.types.ListType;
import dev.cel.common.types.MapType;
import dev.cel.common.types.NullableType;
import dev.cel.common.types.OptionalType;
import dev.cel.common.types.SimpleType;
import java.time.Duration;
Expand Down Expand Up @@ -211,6 +212,27 @@ static CelType parseCelType(String typeStr) {
case "duration":
case "google.protobuf.duration":
return SimpleType.DURATION;
case "google.protobuf.value":
return SimpleType.DYN;
case "google.protobuf.struct":
return MapType.create(SimpleType.STRING, SimpleType.DYN);
case "google.protobuf.listvalue":
return ListType.create(SimpleType.DYN);
case "google.protobuf.boolvalue":
return NullableType.create(SimpleType.BOOL);
case "google.protobuf.bytesvalue":
return NullableType.create(SimpleType.BYTES);
case "google.protobuf.doublevalue":
case "google.protobuf.floatvalue":
return NullableType.create(SimpleType.DOUBLE);
case "google.protobuf.int32value":
case "google.protobuf.int64value":
return NullableType.create(SimpleType.INT);
case "google.protobuf.uint32value":
case "google.protobuf.uint64value":
return NullableType.create(SimpleType.UINT);
case "google.protobuf.stringvalue":
return NullableType.create(SimpleType.STRING);
default:
// TODO: Support protobuf message types (coming soon).
throw new IllegalArgumentException(
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -248,6 +248,26 @@ public void repl_optionalQueries() throws Exception {
assertThat(output[1]).isEmpty();
}

@Test
public void repl_wellKnownTypeQueries() throws Exception {
String[] output =
runReplWithCommands(
":help var",
":var count google.protobuf.Int64Value",
":var payload google.protobuf.Struct",
":vars",
"equiv google.protobuf.Int64Value{value: 42} == count <=> count == 42",
"equiv google.protobuf.Struct{fields: {'k': google.protobuf.Value{string_value: 'v'}}}"
+ " <=> {'k': 'v'}",
":quit");

assertThat(output[0]).contains("Value, Struct, ListValue, *Value (google.protobuf.*)");
assertThat(output[0]).contains("Variable declared: count : wrapper(int)");
assertThat(output[0]).contains("Variable declared: payload : map(string, dyn)");
assertThat(output[0]).contains("[VERIFIED]");
assertThat(output[1]).isEmpty();
}

@Test
public void repl_unknownCommandsAndErrors() throws Exception {
String[] output =
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -328,6 +328,79 @@ public void verifyEquivalence_canonicalizedMapComprehension() throws Exception {
assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED);
}

@Test
public void verifyEquivalence_wellKnownTypesSupportedByDefault() throws Exception {
VerificationOptions options =
VerificationOptions.builder().setTimeout(Duration.ofSeconds(5)).build();
ImmutableMap<String, CelType> vars =
VerificationOptions.parseVariables(
Arrays.asList("x:int", "w:google.protobuf.Int64Value", "s:google.protobuf.Struct"));

assertThat(
CelVerifierToolCore.verifyEquivalence(
"google.protobuf.Struct{fields: {'a': google.protobuf.Value{number_value: 1.0},"
+ " ?'b': optional.none()}}",
"{'a': 1.0}",
vars,
options)
.status())
.isEqualTo(VerificationStatus.VERIFIED);
assertThat(
CelVerifierToolCore.verifyEquivalence(
"google.protobuf.ListValue{values: [google.protobuf.Value{string_value: 'x'}]}",
"['x']",
vars,
options)
.status())
.isEqualTo(VerificationStatus.VERIFIED);
assertThat(
CelVerifierToolCore.verifyEquivalence(
"google.protobuf.Int64Value{value: x} == x"
+ " && google.protobuf.Int64Value{} == 0"
+ " && google.protobuf.StringValue{value: 'hi'} == 'hi'",
"true",
vars,
options)
.status())
.isEqualTo(VerificationStatus.VERIFIED);
assertThat(
CelVerifierToolCore.verifyEquivalence(
"google.protobuf.Timestamp{seconds: 100} == timestamp(100)"
+ " && google.protobuf.Timestamp{seconds: 100, nanos: 500} > timestamp(100)"
+ " && google.protobuf.Duration{seconds: 50}"
+ " == timestamp(150) - timestamp(100)",
"true",
vars,
options)
.status())
.isEqualTo(VerificationStatus.VERIFIED);
assertThat(
CelVerifierToolCore.verifyEquivalence(
"w == null || w == google.protobuf.Int64Value{value: w}",
"true",
vars,
options)
.status())
.isEqualTo(VerificationStatus.VERIFIED);
String yamlPolicy =
"name: wkt_policy\n"
+ "rule:\n"
+ " match:\n"
+ " - condition: \"w == google.protobuf.Int64Value{value: 10}\"\n"
+ " output: 'true'\n"
+ " - output: 'false'\n"
+ "verification:\n"
+ " invariants:\n"
+ " - id: wkt_check\n"
+ " assert:\n"
+ " - \"w != 10 || w == google.protobuf.Int64Value{value: 10}\"\n";
assertThat(
CelVerifierToolCore.verifyPolicyInvariants(yamlPolicy, vars, options)
.get("wkt_check")
.status())
.isEqualTo(VerificationStatus.VERIFIED);
}

@Test
public void verifyPolicyInvariants_success() throws Exception {
String yamlPolicy =
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,7 @@
import dev.cel.common.types.CelType;
import dev.cel.common.types.ListType;
import dev.cel.common.types.MapType;
import dev.cel.common.types.NullableType;
import dev.cel.common.types.OptionalType;
import dev.cel.common.types.SimpleType;
import dev.cel.verifier.tools.VerificationOptions.OutputFormat;
Expand Down Expand Up @@ -123,6 +124,36 @@ public void parseCelType_timestampAndDuration() {
.isEqualTo(SimpleType.DURATION);
}

@Test
public void parseCelType_wellKnownTypes() {
assertThat(VerificationOptions.parseCelType("google.protobuf.Value")).isEqualTo(SimpleType.DYN);
assertThat(VerificationOptions.parseCelType("google.protobuf.Struct"))
.isEqualTo(MapType.create(SimpleType.STRING, SimpleType.DYN));
assertThat(VerificationOptions.parseCelType("google.protobuf.ListValue"))
.isEqualTo(ListType.create(SimpleType.DYN));
assertThat(VerificationOptions.parseCelType("google.protobuf.BoolValue"))
.isEqualTo(NullableType.create(SimpleType.BOOL));
assertThat(VerificationOptions.parseCelType("google.protobuf.BytesValue"))
.isEqualTo(NullableType.create(SimpleType.BYTES));
assertThat(VerificationOptions.parseCelType("google.protobuf.DoubleValue"))
.isEqualTo(NullableType.create(SimpleType.DOUBLE));
assertThat(VerificationOptions.parseCelType("google.protobuf.FloatValue"))
.isEqualTo(NullableType.create(SimpleType.DOUBLE));
assertThat(VerificationOptions.parseCelType("google.protobuf.Int32Value"))
.isEqualTo(NullableType.create(SimpleType.INT));
assertThat(VerificationOptions.parseCelType("google.protobuf.Int64Value"))
.isEqualTo(NullableType.create(SimpleType.INT));
assertThat(VerificationOptions.parseCelType("google.protobuf.UInt32Value"))
.isEqualTo(NullableType.create(SimpleType.UINT));
assertThat(VerificationOptions.parseCelType("google.protobuf.UInt64Value"))
.isEqualTo(NullableType.create(SimpleType.UINT));
assertThat(VerificationOptions.parseCelType("google.protobuf.StringValue"))
.isEqualTo(NullableType.create(SimpleType.STRING));
assertThrows(
IllegalArgumentException.class,
() -> VerificationOptions.parseCelType("google.protobuf.Any"));
}

@Test
public void parseCelType_optionalTypes() {
assertThat(VerificationOptions.parseCelType("optional<int>"))
Expand Down
Loading