// Copyright 2026 Google LLC
//
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
//      https://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.

package dev.cel.verifier;

import com.google.common.collect.ImmutableMap;
import dev.cel.policy.CelPolicy;
import dev.cel.policy.CelPolicyValidationException;

/** Public interface for verifying CEL policies. */
public interface CelPolicyVerifier {

  /**
   * Verifies if two policies are strictly equivalent for all possible inputs.
   *
   * @throws CelPolicyValidationException if the provided policies fail policy-specific compilation.
   */
  CelVerificationResult verifyEquivalence(CelPolicy policyA, CelPolicy policyB)
      throws CelPolicyValidationException, CelVerificationException;

  /**
   * Verifies all custom invariants defined in the policy against all possible input states.
   *
   * @return A map of invariant IDs to their verification results.
   * @throws CelPolicyValidationException if the policy or any invariant fails compilation.
   * @throws CelVerificationException if the verification check encounters an internal solver error.
   */
  ImmutableMap<String, CelVerificationResult> verifyInvariants(CelPolicy policy)
      throws CelPolicyValidationException, CelVerificationException;
}

