// 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.auto.value.AutoValue;

/** Result object containing the outcome of a CEL AST verification check. */
@AutoValue
public abstract class CelVerificationResult {

  /** Represents the outcome of the verification process. */
  public enum VerificationStatus {
    /** The property was mathematically proven to hold for all possible inputs. */
    VERIFIED,
    /** The property was disproven. A concrete counterexample was found. */
    VIOLATED,
    /** The property could not be verified due to loop truncation or timeout. */
    INCONCLUSIVE
  }

  /** Returns the status of the verification check. */
  public abstract VerificationStatus status();

  /**
   * Returns the primary reason for the verification outcome.
   */
  public abstract String reason();

  /**
   * Returns a detailed counterexample or satisfying model assignment, if one was found.
   */
  public abstract String counterexample();

  /**
   * Returns a message detailing the outcome of the verification check, such as a counterexample
   * input, satisfying model assignments, or truncation reason. May be empty if status is VERIFIED
   * and no model inputs apply (e.g., when verifying isAlwaysTrue without counterexamples).
   */
  public String message() {
    return reason() + counterexample();
  }

  static CelVerificationResult verified() {
    return new AutoValue_CelVerificationResult(VerificationStatus.VERIFIED, "", "");
  }

  static CelVerificationResult verified(String reason) {
    return new AutoValue_CelVerificationResult(VerificationStatus.VERIFIED, reason, "");
  }

  static CelVerificationResult failed(String reason) {
    return new AutoValue_CelVerificationResult(VerificationStatus.VIOLATED, reason, "");
  }

  static CelVerificationResult failed(String reason, String counterexample) {
    return new AutoValue_CelVerificationResult(
        VerificationStatus.VIOLATED, reason, counterexample);
  }

  static CelVerificationResult inconclusive(String reason) {
    return new AutoValue_CelVerificationResult(VerificationStatus.INCONCLUSIVE, reason, "");
  }

  static CelVerificationResult inconclusive(String reason, String counterexample) {
    return new AutoValue_CelVerificationResult(
        VerificationStatus.INCONCLUSIVE, reason, counterexample);
  }
}
