#!/usr/bin/env bash
set -u

artifact="${1:-}"
evidence_dir="${2:-}"
require_lean="${TOKITAI_REQUIRE_LEAN:-0}"
lean_timeout_seconds="${TOKITAI_LEAN_TIMEOUT_SECONDS:-20}"
generated_default_trace="0"

if [ -z "$artifact" ]; then
  generated_default_trace="1"
  evidence_dir="${TOKITAI_AUDIT_TRACE_DIR:-target/tokitai-optional-lean}"
  mkdir -p "$evidence_dir"
  TOKITAI_AUDIT_TRACE_DIR="$evidence_dir" \
    TOKITAI_AUDIT_TRACE_KEY_ID="${TOKITAI_AUDIT_TRACE_KEY_ID:-optional lean key}" \
    TOKITAI_AUDIT_TRACE_SECRET="${TOKITAI_AUDIT_TRACE_SECRET:-optional-lean-secret}" \
    cargo run --quiet --offline --example audit_traces \
    > "$evidence_dir/audit-traces.stdout" \
    2> "$evidence_dir/audit-traces.stderr"
  artifact="$evidence_dir/matmul.lean-checkable.lean"
fi

if [ ! -f "$artifact" ]; then
  if [ "$generated_default_trace" = "1" ]; then
    evidence_file="$evidence_dir/matmul.optional-lean-evidence.txt"
    {
      echo "artifact=$artifact"
      echo "required=$require_lean"
      echo "default_gate=unchanged_no_lean"
      echo "status=skipped"
      echo "reason=checkable_artifact_not_generated_by_default_audit_trace"
      echo "note=pass an explicit *.lean-checkable.lean artifact from a native checker fixture or paper artifact run"
    } > "$evidence_file"
    if [ "$require_lean" = "1" ]; then
      echo "tokitai optional lean check: default audit trace did not generate $artifact and TOKITAI_REQUIRE_LEAN=1" >&2
      exit 1
    fi
    echo "$evidence_file"
    exit 0
  fi
  echo "tokitai optional lean check: missing artifact $artifact" >&2
  exit 2
fi

if [ -z "$evidence_dir" ]; then
  evidence_dir="$(dirname "$artifact")"
fi
mkdir -p "$evidence_dir"

stem="$(basename "$artifact" .lean-checkable.lean)"
evidence_file="$evidence_dir/${stem}.optional-lean-evidence.txt"
stdout_file="$evidence_dir/${stem}.optional-lean.stdout"
stderr_file="$evidence_dir/${stem}.optional-lean.stderr"

sha256_cmd=""
if command -v sha256sum >/dev/null 2>&1; then
  sha256_cmd="sha256sum"
elif command -v shasum >/dev/null 2>&1; then
  sha256_cmd="shasum -a 256"
fi

{
  echo "artifact=$artifact"
  echo "required=$require_lean"
  echo "default_gate=unchanged_no_lean"
  if [ -n "$sha256_cmd" ]; then
    # shellcheck disable=SC2086
    echo "artifact_sha256=$($sha256_cmd "$artifact" | awk '{print $1}')"
  else
    echo "artifact_sha256=unavailable"
  fi
} > "$evidence_file"

if ! command -v lean >/dev/null 2>&1; then
  {
    echo "status=skipped"
    echo "reason=lean_not_found"
    echo "lean_status=missing"
    echo "lean_version=unavailable"
    echo "exit_status=skipped"
    echo "note=Lean is optional unless TOKITAI_REQUIRE_LEAN=1"
  } >> "$evidence_file"
  if [ "$require_lean" = "1" ]; then
    echo "tokitai optional lean check: Lean missing and TOKITAI_REQUIRE_LEAN=1" >&2
    exit 1
  fi
  echo "$evidence_file"
  exit 0
fi

lean --version >> "$evidence_file" 2>&1
status=0
lean_status="ran"
if command -v timeout >/dev/null 2>&1; then
  timeout -k 2s "$lean_timeout_seconds" lean "$artifact" > "$stdout_file" 2> "$stderr_file" || status=$?
  if [ "$status" -eq 124 ]; then
    lean_status="timeout"
  fi
else
  lean "$artifact" > "$stdout_file" 2> "$stderr_file" || status=$?
fi
{
  if [ "$status" -eq 0 ]; then
    echo "status=accepted"
    echo "success_transcript=captured"
  else
    echo "status=failed_optional"
  fi
  echo "lean_status=$lean_status"
  echo "stdout_file=$stdout_file"
  echo "stderr_file=$stderr_file"
  echo "exit_status=$status"
  echo "timeout_seconds=$lean_timeout_seconds"
} >> "$evidence_file"

if [ "$status" -ne 0 ] && [ "$require_lean" = "1" ]; then
  echo "tokitai optional lean check: Lean failed and TOKITAI_REQUIRE_LEAN=1" >&2
  exit "$status"
fi

echo "$evidence_file"
exit 0