#!/usr/bin/env bb
;; Launch-sealed adapter between Beagle Store's server proof protocol and Beagle's
;; module-overlay checker. The server owns invocation; callers never submit
;; receipts or choose a checker per request.
;;
;; Required launch environment:
;;   BEAGLE_STORE_EDIT_VERIFIER_RACKET  exact Racket executable (BEAGLE_STORE_RACKET fallback)
;;   BEAGLE_HOME                exact Beagle root
;;
;; Optional:
;;   BEAGLE_STORE_EDIT_VERIFIER_OVERLAY_CHECK
;;     exact facts-check-overlay.rkt path
;;
;; stdout is protocol-only: one closed success/failure JSON receipt. Adapter or
;; toolchain failures write stderr and exit 2, which keeps the candidate
;; retryable. Deterministic candidate rejection writes a closed failure receipt
;; and exits 1.

(require '[cheshire.core :as json]
         '[clojure.java.io :as io]
         '[clojure.string :as str])

(import '(java.io File FileInputStream)
        '(java.nio.charset StandardCharsets)
        '(java.nio.file Files)
        '(java.security MessageDigest)
        '(java.util ArrayList)
        '(java.util.concurrent TimeUnit))

(def request-schema "beagle-store-edit-verifier-request-v1")
(def command-protocol "beagle-store-edit-verifier-command-v1")
(def receipt-schema "beagle-store-edit-verifier-receipt-v1")
(def toolchain-schema "beagle-store-edit-verifier-toolchain-v1")
(def checker-timeout-ms 120000)
(def checker-rejection-sentinel
  "REJECTED: coherent candidate overlay failed — nothing emitted")

(def request-keys
  #{:schema :protocol :input-digest :candidate :base-version
    :ops-digest :edn-digest :closure-digest :overlay-digest
    :checked-modules :closure :overlay})
(def closure-row-keys #{:source :namespace :source-digest})
(def overlay-row-keys #{:source :namespace :source-digest :edn})
(def checker-result-keys #{:schemaVersion :ok :overlayDigest :modules})
(def checker-module-keys
  #{:source :namespace :sourceDigest :interfaceDigest :emitted})

(def hex64-re #"[0-9a-f]{64}")
(def racket-digest-re #"sha256:([0-9a-f]{64})")

(defn fail! [message & [data]]
  (throw (ex-info message (or data {}))))

(defn require! [condition message & [data]]
  (when-not condition
    (fail! message data)))

(defn exact-keys! [value expected label]
  (require! (map? value) (str label " must be an object"))
  (require! (= expected (set (keys value)))
            (str label " has a non-protocol key set")
            {:expected expected :actual (set (keys value))})
  value)

(defn hex64? [value]
  (and (string? value) (boolean (re-matches hex64-re value))))

(defn digest-bytes [^bytes bytes]
  (let [digest (.digest (MessageDigest/getInstance "SHA-256") bytes)]
    (apply str (map #(format "%02x" %) digest))))

(defn digest-string [value]
  (digest-bytes (.getBytes ^String value StandardCharsets/UTF_8)))

(defn digest-file [^File file]
  (let [digest (MessageDigest/getInstance "SHA-256")
        buffer (byte-array 65536)]
    (with-open [in (FileInputStream. file)]
      (loop []
        (let [n (.read in buffer)]
          (when (pos? n)
            (.update digest buffer 0 n)
            (recur)))))
    (apply str (map #(format "%02x" %) (.digest digest)))))

(defn canonical-file! [path label kind]
  (require! (and (string? path) (not (str/blank? path)))
            (str label " is not configured"))
  (let [file (.getCanonicalFile (io/file path))]
    (case kind
      :file
      (require! (.isFile file)
                (str label " is not a regular file: " (.getPath file)))

      :dir
      (require! (.isDirectory file)
                (str label " is not a directory: " (.getPath file)))

      :executable
      (do
        (require! (.isFile file)
                  (str label " is not a regular file: " (.getPath file)))
        (require! (.canExecute file)
                  (str label " is not executable: " (.getPath file)))))
    file))

(defn relative-path [^File root ^File child]
  (-> (.toPath root)
      (.relativize (.toPath child))
      str
      (str/replace File/separator "/")))

(defn tree-manifest-digest [^File root include-compiled?]
  (let [rows
        (->> (file-seq root)
             (filter #(.isFile ^File %))
             (keep
              (fn [^File file]
                (let [relative (relative-path root file)]
                  ;; The checker is launched with Racket `-c`, so compiled/
                  ;; caches are explicitly not executable inputs. Excluding
                  ;; them makes the measured closure match reality and prevents
                  ;; another Racket version's cache maintenance from creating
                  ;; false toolchain drift.
                  (when (or include-compiled?
                            (not (re-find #"(?:^|/)compiled(?:/|$)" relative)))
                    [relative (.length file) (digest-file file)]))))
             (sort-by first)
             vec)]
    (digest-string (pr-str rows))))

(defn current-executable []
  (try
    ;; Linux exposes the running native Babashka image exactly. Other targets
    ;; still bind the interpreter version below; packaged scripts additionally
    ;; have their absolute store interpreter in the launch-sealed shebang.
    (let [self (io/file "/proc/self/exe")]
      (when (.exists self)
        (.getCanonicalPath self)))
    (catch Throwable _ nil)))

(defn toolchain-snapshot []
  (let [beagle-home
        (canonical-file!
         (System/getenv "BEAGLE_HOME")
         "BEAGLE_HOME"
         :dir)
        beagle-lib
        (canonical-file!
         (.getPath (io/file beagle-home "beagle-lib"))
         "Beagle library root"
         :dir)
        racket
        (canonical-file!
         (or (System/getenv "BEAGLE_STORE_EDIT_VERIFIER_RACKET")
             (System/getenv "BEAGLE_STORE_RACKET"))
         "BEAGLE_STORE_EDIT_VERIFIER_RACKET/BEAGLE_STORE_RACKET"
         :executable)
        checker
        (canonical-file!
         (or (System/getenv "BEAGLE_STORE_EDIT_VERIFIER_OVERLAY_CHECK")
             (.getPath
              (io/file beagle-home
                       "beagle-lib/private/facts-check-overlay.rkt")))
         "BEAGLE_STORE_EDIT_VERIFIER_OVERLAY_CHECK"
         :file)
        checker-path (.getPath checker)
        beagle-lib-path (.getPath beagle-lib)
        _ (require! (or (= checker-path beagle-lib-path)
                        (str/starts-with?
                         checker-path
                         (str beagle-lib-path File/separator)))
                    "module-overlay checker must be inside BEAGLE_HOME/beagle-lib")
        executable-path (current-executable)
        executable (when executable-path
                     (canonical-file! executable-path
                                      "current verifier interpreter"
                                      :executable))
        freshness (io/file beagle-home ".beagle/zo-fresh")
        use-compiled?
        (and (str/starts-with? (.getPath beagle-home) "/nix/store/")
             (.isFile freshness)
             (= (.getPath racket) (str/trim (slurp freshness))))
        identity
        [toolchain-schema
         ["interpreter"
          (some-> executable .getPath)
          (some-> executable digest-file)
          (System/getProperty "babashka.version")]
         ["racket" (.getPath racket) (digest-file racket)]
         ["beagle-lib" beagle-lib-path
          (tree-manifest-digest beagle-lib use-compiled?)]
         ["compiled" use-compiled?]
         ["checker" (relative-path beagle-lib checker) (digest-file checker)]]]
    {:digest (digest-string (pr-str identity))
     :racket (.getPath racket)
     :beagle-lib beagle-lib-path
     :checker checker-path
     :use-compiled use-compiled?}))

(defn validate-namespace! [value label]
  (require! (or (nil? value)
                (and (string? value) (not (str/blank? value))))
            (str label " namespace must be a nonblank string or null")))

(defn validate-closure-row! [row index]
  (let [label (str "closure[" index "]")]
    (exact-keys! row closure-row-keys label)
    (require! (and (string? (:source row))
                   (not (str/blank? (:source row))))
              (str label " source must be a nonblank string"))
    (validate-namespace! (:namespace row) label)
    (require! (hex64? (:source-digest row))
              (str label " source-digest must be 64 lowercase hex"))
    row))

(defn validate-overlay-row! [row index]
  (let [label (str "overlay[" index "]")]
    (exact-keys! row overlay-row-keys label)
    (require! (and (string? (:source row))
                   (not (str/blank? (:source row))))
              (str label " source must be a nonblank string"))
    (validate-namespace! (:namespace row) label)
    (require! (hex64? (:source-digest row))
              (str label " source-digest must be 64 lowercase hex"))
    (require! (string? (:edn row)) (str label " edn must be a string"))
    (require! (= (:source-digest row) (digest-string (:edn row)))
              (str label " source-digest does not match its EDN bytes"))
    (require! (= (str "@file " (:source row))
                 (first (str/split-lines (:edn row))))
              (str label " EDN @file identity does not match source"))
    row))

(defn validate-request! [request]
  (exact-keys! request request-keys "request")
  (require! (= request-schema (:schema request))
            "request schema mismatch")
  (require! (= command-protocol (:protocol request))
            "request protocol mismatch")
  (doseq [field [:input-digest :ops-digest :edn-digest
                 :closure-digest :overlay-digest]]
    (require! (hex64? (get request field))
              (str (name field) " must be 64 lowercase hex")))
  (require! (and (string? (:candidate request))
                 (not (str/blank? (:candidate request))))
            "candidate must be a nonblank string")
  (require! (and (integer? (:base-version request))
                 (not (neg? (:base-version request))))
            "base-version must be a nonnegative integer")
  (require! (and (vector? (:checked-modules request))
                 (every? #(and (string? %) (not (str/blank? %)))
                         (:checked-modules request)))
            "checked-modules must be a vector of nonblank source IDs")
  (require! (vector? (:closure request)) "closure must be a vector")
  (require! (seq (:closure request)) "closure must not be empty")
  (require! (vector? (:overlay request)) "overlay must be a vector")
  (require! (seq (:overlay request)) "overlay must not be empty")
  (let [closure (mapv validate-closure-row!
                      (:closure request)
                      (range))
        overlay (mapv validate-overlay-row!
                      (:overlay request)
                      (range))
        checked (:checked-modules request)
        closure-sources (mapv :source closure)
        overlay-sources (mapv :source overlay)
        overlay-by-source (into {} (map (juxt :source identity)) overlay)]
    (require! (= checked (vec (sort checked)))
              "checked-modules must be sorted lexicographically")
    (require! (= checked closure-sources)
              "closure order must exactly match checked-modules")
    (require! (= overlay-sources (vec (sort overlay-sources)))
              "overlay must be sorted lexicographically by source")
    (require! (= (count overlay-sources) (count (set overlay-sources)))
              "overlay contains duplicate source IDs")
    (require! (= (count closure-sources) (count (set closure-sources)))
              "closure contains duplicate source IDs")
    (doseq [row closure]
      (let [overlay-row (get overlay-by-source (:source row))]
        (require! overlay-row
                  (str "checked source is absent from overlay: "
                       (:source row)))
        (require! (= row
                     (select-keys overlay-row
                                  [:source :namespace :source-digest]))
                  (str "closure row disagrees with overlay: "
                       (:source row)))))
    (let [closure-digest
          (digest-string
           (pr-str
            (mapv (juxt :source :namespace :source-digest) closure)))
          overlay-digest
          (digest-string
           (pr-str
            (mapv (juxt :source :namespace :source-digest) overlay)))
          input-digest
          (digest-string
           (pr-str
            [request-schema
             (:candidate request)
             (:base-version request)
             (:ops-digest request)
             (:edn-digest request)
             closure-digest
             overlay-digest]))]
      (require! (= closure-digest (:closure-digest request))
                "closure-digest mismatch")
      (require! (= overlay-digest (:overlay-digest request))
                "overlay-digest mismatch")
      (require! (= input-digest (:input-digest request))
                "input-digest mismatch"))
    (assoc request
           :closure closure
           :overlay overlay)))

(defn delete-tree! [^File root]
  (doseq [^File file (reverse (file-seq root))]
    (when (.exists file)
      (Files/deleteIfExists (.toPath file)))))

(defn with-temp-overlay [toolchain request f]
  (let [root (.toFile
              (Files/createTempDirectory
               "beagle-store-edit-verifier-"
               (make-array java.nio.file.attribute.FileAttribute 0)))
        collects (io/file root "collects")
        beagle-collection (io/file collects "beagle")]
    (try
      (let [_ (require! (.mkdirs collects)
                        "cannot create verifier collection root")
            _ (Files/createSymbolicLink
               (.toPath beagle-collection)
               (.toPath (io/file (:beagle-lib toolchain)))
               (make-array java.nio.file.attribute.FileAttribute 0))
            paths
            (mapv
             (fn [index row]
               (let [path (io/file root (format "%06d.edn" index))]
                 (spit path (:edn row))
                 (.getPath path)))
             (range)
             (:overlay request))]
        (f paths (.getPath collects)))
      (finally
        ;; file-seq follows directory symlinks, so unlink the collection before
        ;; recursively deleting the private overlay directory.
        (Files/deleteIfExists (.toPath beagle-collection))
        (delete-tree! root)))))

(defn bounded [value limit]
  (let [value (str (or value ""))]
    (if (> (count value) limit)
      (str (subs value 0 limit) "…")
      value)))

(defn run-checker [toolchain request paths collects]
  (let [selectors
        (mapcat (fn [source] ["--check-source" source])
                (:checked-modules request))
        command
        ;; Mutable checkouts disable compiled files because their caches can be
        ;; shared by incompatible Racket versions. Immutable Nix packages may
        ;; use bytecode only when .beagle/zo-fresh names this exact Racket; that
        ;; bytecode is included in the measured toolchain digest above.
        (into (cond-> [(:racket toolchain) "-U"]
                (not (:use-compiled toolchain)) (conj "-c")
                true (conj "-S" collects (:checker toolchain)))
              (concat selectors paths))
        builder
        (ProcessBuilder.
         ^java.util.List
         (ArrayList. ^java.util.Collection command))
        environment (.environment builder)
        ;; The proof subprocess is a closed toolchain invocation. Ambient
        ;; Racket collection/cache knobs, startup hooks, and caller PATH/HOME
        ;; must not be able to redirect what the launch-sealed adapter checks.
        _ (.clear environment)
        _ (.put environment "HOME" "/homeless-shelter")
        _ (.put environment "LANG" "C")
        _ (.put environment "LC_ALL" "C")
        _ (.put environment "PLTUSERHOME" "/homeless-shelter")
        process
        (.start builder)
        stdout-f (future (slurp (.getInputStream process)))
        stderr-f (future (slurp (.getErrorStream process)))]
    (if-not (.waitFor process
                      (long checker-timeout-ms)
                      TimeUnit/MILLISECONDS)
      (do
        (.destroyForcibly process)
        (.waitFor process)
        (fail! (str "module-overlay checker exceeded "
                    checker-timeout-ms
                    "ms")))
      {:exit (.exitValue process)
       :stdout (bounded (deref stdout-f 5000 "") 1048576)
       :stderr (bounded (deref stderr-f 5000 "") 1048576)})))

(defn deterministic-overlay-rejection? [checker-result]
  (and
   (= 1 (:exit checker-result))
   (= checker-rejection-sentinel
      (last
       (remove str/blank?
               (str/split-lines (str (:stderr checker-result))))))))

(defn normalized-racket-digest [value label]
  (let [match (and (string? value)
                   (re-matches racket-digest-re value))]
    (require! match (str label " must be sha256:<64 lowercase hex>"))
    (second match)))

(defn parse-checker-success [result request toolchain-digest]
  (require! (zero? (:exit result))
            (str "module-overlay checker failed unexpectedly (exit "
                 (:exit result)
                 "): "
                 (:stderr result)))
  (let [payload
        (try
          (json/parse-string (:stdout result) true)
          (catch Throwable _
            (fail! "module-overlay checker emitted malformed JSON")))
        _ (exact-keys! payload checker-result-keys "checker receipt")
        _ (require! (= 1 (:schemaVersion payload))
                    "module-overlay checker schemaVersion mismatch")
        _ (require! (true? (:ok payload))
                    "module-overlay checker success receipt is not ok")
        modules (:modules payload)
        _ (require! (vector? modules)
                    "module-overlay checker modules must be a vector")
        checked
        (mapv
         (fn [row index]
           (let [label (str "checker modules[" index "]")]
             (exact-keys! row checker-module-keys label)
             (require! (and (string? (:source row))
                            (not (str/blank? (:source row))))
                       (str label " source must be nonblank"))
             (validate-namespace! (:namespace row) label)
             (normalized-racket-digest (:sourceDigest row)
                                       (str label " sourceDigest"))
             (normalized-racket-digest (:interfaceDigest row)
                                       (str label " interfaceDigest"))
             (require! (string? (:emitted row))
                       (str label " emitted must be a string"))
             row))
         modules
         (range))
        by-source (into {} (map (juxt :source identity)) checked)
        _ (require! (= (count checked) (count by-source))
                    "module-overlay checker returned duplicate module sources")
        _ (require! (= (set (:checked-modules request))
                       (set (keys by-source)))
                    "module-overlay checker returned the wrong selected modules")
        receipt-modules
        (mapv
         (fn [closure-row]
           (let [source (:source closure-row)
                 checked-row (get by-source source)]
             (require! (= (:namespace closure-row)
                          (:namespace checked-row))
                       (str "checker namespace disagrees for " source))
             {:source source
              :namespace (:namespace closure-row)
              ;; This is deliberately the exact candidate-EDN digest sealed by
              ;; Beagle Store. Beagle's sourceDigest is a different canonical AST digest.
              :source-digest (:source-digest closure-row)
              :interface-digest
              (normalized-racket-digest
               (:interfaceDigest checked-row)
               (str "interface digest for " source))
              :emitted-digest (digest-string (:emitted checked-row))}))
         (:closure request))]
    {:schema receipt-schema
     :ok true
     :input-digest (:input-digest request)
     :overlay-digest
     (normalized-racket-digest (:overlayDigest payload) "overlayDigest")
     :toolchain-closure-digest toolchain-digest
     :modules receipt-modules}))

(defn rejection-errors [stderr]
  (let [errors
        (->> (str/split-lines (str (or stderr "")))
             (remove str/blank?)
             ;; Keep a deterministic rejection comfortably inside the
             ;; server's closed-receipt envelope. Detailed diagnostics
             ;; remain available on the verifier's bounded stderr channel.
             (map #(bounded % 320))
             (take 8)
             vec)]
    (if (seq errors)
      errors
      ["coherent candidate overlay rejected"])))

(defn verify-request [request]
  ;; A mutable development checkout can change while the checker is running.
  ;; Never bless that drifting run: retry once and issue a proof only when the
  ;; measured source/toolchain closure is identical before and after. Mutable
  ;; checkout caches are not inputs because run-checker uses `-c`; immutable
  ;; package bytecode is measured with the source closure.
  (loop [attempt 0
         before (toolchain-snapshot)]
    (let [checker-result
          (with-temp-overlay
            before
            request
            #(run-checker before request %1 %2))
          after (toolchain-snapshot)]
      (if-not (= (:digest before) (:digest after))
        (if (zero? attempt)
          (recur (inc attempt) after)
          (fail! "verifier toolchain changed during module-overlay checking"))
        (cond
          (zero? (:exit checker-result))
          {:exit 0
           :receipt
           (parse-checker-success
            checker-result
            request
            (:digest before))}

          (deterministic-overlay-rejection? checker-result)
          {:exit 1
           :receipt
           {:schema receipt-schema
            :ok false
            :input-digest (:input-digest request)
            :code "beagle-overlay-rejected"
            :errors (rejection-errors (:stderr checker-result))}}

          :else
          (fail!
           (str "module-overlay checker infrastructure failure (exit "
                (:exit checker-result)
                "): "
                (:stderr checker-result))))))))

(try
  (let [wire (slurp *in*)
        _ (require! (not (str/blank? wire))
                    "verifier request is empty")
        request
        (try
          (json/parse-string wire true)
          (catch Throwable _
            (fail! "verifier request is malformed JSON")))
        {:keys [exit receipt]} (verify-request (validate-request! request))]
    (println (json/generate-string receipt))
    (flush)
    (System/exit exit))
  (catch Throwable error
    (binding [*out* *err*]
      (println
       (str "beagle-store-edit-verifier: "
            (or (.getMessage error)
                (.getName (class error))))))
    (System/exit 2)))
