parallel_proof_search.chpl

// SPDX-License-Identifier: MPL-2.0
// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
//
// ECHIDNA Chapel Metalayer — Parallel Proof Search
//
// Dispatches theorem proving goals to all 30 prover backends concurrently
// using Chapel's coforall for true data parallelism. Each prover is invoked
// as a subprocess with a timeout; the first successful proof wins.

use Time;
use IO;
use FileSystem;
use Subprocess;
use Path;
use List;

// ---------------------------------------------------------------------------
// Configuration
// ---------------------------------------------------------------------------

config const numProvers = 30;
config const verbose = true;
config const defaultTimeout = 300; // seconds

// ---------------------------------------------------------------------------
// Prover registry — all 30 ECHIDNA backends
// ---------------------------------------------------------------------------

// Prover category tags for reporting
enum ProverCategory {
    InteractiveAssistant,
    SmtSolver,
    FirstOrderAtp,
    DeclarativeProver,
    AutoActive,
    ConstraintSolver
}

record ProverInfo {
    var id: int;
    var name: string;
    var executable: string;
    var category: ProverCategory;
    var fileExt: string;       // file extension for temp input files
    var argTemplate: string;   // how to pass the input file (%FILE% placeholder)
    // Optional spawn hooks. Default empty preserves prior behaviour:
    // inherit parent CWD + use generic `goal_<name>_<nodeId>.<fileExt>`
    // filename. Set per-prover when the prover enforces special
    // requirements at subprocess spawn time:
    //   cwd              — Idris2 resolves its prelude relative to CWD
    //                      and requires the source file to live inside
    //                      the configured source directory (#158).
    //   filenameOverride — Agda + Idris2 enforce module-name = filename;
    //                      generic `goal_<n>_<id>` either fails the Agda
    //                      lexer ("the part 0 is not valid because it is
    //                      a literal") or the Idris2 module/file-mismatch
    //                      check (#159). Use a literal basename (with
    //                      extension) that matches the fixture's module
    //                      declaration.
    var cwd: string;
    var filenameOverride: string;

    proc init(id: int, name: string, executable: string,
              category: ProverCategory, fileExt: string,
              argTemplate: string,
              cwd: string = "",
              filenameOverride: string = "") {
        this.id = id;
        this.name = name;
        this.executable = executable;
        this.category = category;
        this.fileExt = fileExt;
        this.argTemplate = argTemplate;
        this.cwd = cwd;
        this.filenameOverride = filenameOverride;
        init this;
    }

    // Zero-arg init for array default-initialisation
    // (`var provers: [0..29] ProverInfo`). Custom positional init above
    // suppresses the auto-generated zero-arg form, so the array
    // declaration needs this fallback to compile.
    proc init() {
        this.id = -1;
        this.name = "";
        this.executable = "";
        this.category = ProverCategory.InteractiveAssistant;
        this.fileExt = "";
        this.argTemplate = "";
        this.cwd = "";
        this.filenameOverride = "";
        init this;
    }
}

// Build the full 30-prover registry
proc buildProverRegistry(): [0..29] ProverInfo {
    var provers: [0..29] ProverInfo;

    // Tier 1: Interactive proof assistants (10)
    // Agda: --safe rejects postulate/admit/believe_me. Two filename
    // hooks needed for the module-name resolver:
    //   filenameOverride: the source-file basename must be a valid
    //                     identifier (generic `goal_Agda_0` is rejected
    //                     because the part `0` is parsed as a literal).
    //                     The fixture declares `module Trivial where`.
    //   cwd:              the module-name resolver searches relative
    //                     to the cwd (plus agda-stdlib paths). Setting
    //                     cwd to the temp dir makes the override basename
    //                     resolve from the file actually written there.
    provers[0]  = new ProverInfo(0,  "Agda",      "agda",          ProverCategory.InteractiveAssistant, "agda",  "--safe %FILE%",
                                  cwd = "/tmp/echidna-chapel",
                                  filenameOverride = "Trivial.agda");
    provers[1]  = new ProverInfo(1,  "Coq",       "coqc",          ProverCategory.InteractiveAssistant, "v",     "%FILE%");
    provers[2]  = new ProverInfo(2,  "Lean",      "lean",          ProverCategory.InteractiveAssistant, "lean",  "%FILE%");
    provers[3]  = new ProverInfo(3,  "Isabelle",  "isabelle",      ProverCategory.InteractiveAssistant, "thy",   "process %FILE%");
    // Idris2: `--check` resolves the prelude relative to IDRIS2_PREFIX
    // (or the install root) AND the source file must live in the
    // configured source directory. cwd = /tmp/echidna-chapel matches
    // where tryProver writes the temp file; the parent process's
    // IDRIS2_PREFIX is inherited by the subprocess (POSIX spawn
    // default). filenameOverride pins the basename to the fixture's
    // `module Trivial where` declaration.
    provers[4]  = new ProverInfo(4,  "Idris2",    "idris2",        ProverCategory.InteractiveAssistant, "idr",   "--check %FILE%",
                                  cwd = "/tmp/echidna-chapel",
                                  filenameOverride = "Trivial.idr");
    provers[5]  = new ProverInfo(5,  "FStar",     "fstar.exe",     ProverCategory.InteractiveAssistant, "fst",   "%FILE%");
    provers[6]  = new ProverInfo(6,  "HOL4",      "hol",           ProverCategory.InteractiveAssistant, "sml",   "< %FILE%");
    provers[7]  = new ProverInfo(7,  "HOLLight",  "ocaml",         ProverCategory.InteractiveAssistant, "ml",    "%FILE%");
    provers[8]  = new ProverInfo(8,  "Nuprl",     "nuprl",         ProverCategory.InteractiveAssistant, "nuprl", "%FILE%");
    provers[9]  = new ProverInfo(9,  "Minlog",    "minlog",        ProverCategory.InteractiveAssistant, "minlog","%FILE%");

    // Tier 2: SMT solvers (3)
    provers[10] = new ProverInfo(10, "Z3",        "z3",            ProverCategory.SmtSolver,            "smt2",  "%FILE%");
    provers[11] = new ProverInfo(11, "CVC5",      "cvc5",          ProverCategory.SmtSolver,            "smt2",  "--lang smt2 %FILE%");
    provers[12] = new ProverInfo(12, "AltErgo",   "alt-ergo",      ProverCategory.SmtSolver,            "ae",    "%FILE%");

    // Tier 3: First-order ATPs (3)
    provers[13] = new ProverInfo(13, "Vampire",   "vampire",       ProverCategory.FirstOrderAtp,        "p",     "--mode casc %FILE%");
    provers[14] = new ProverInfo(14, "EProver",   "eprover",       ProverCategory.FirstOrderAtp,        "p",     "--auto %FILE%");
    provers[15] = new ProverInfo(15, "SPASS",     "SPASS",         ProverCategory.FirstOrderAtp,        "dfg",   "%FILE%");

    // Tier 4: Declarative provers (7)
    provers[16] = new ProverInfo(16, "Metamath",  "metamath",      ProverCategory.DeclarativeProver,    "mm",    "read %FILE% verify proof *");
    provers[17] = new ProverInfo(17, "Mizar",     "mizf",          ProverCategory.DeclarativeProver,    "miz",   "%FILE%");
    provers[18] = new ProverInfo(18, "PVS",       "pvs",           ProverCategory.DeclarativeProver,    "pvs",   "-batch %FILE%");
    provers[19] = new ProverInfo(19, "ACL2",      "acl2",          ProverCategory.DeclarativeProver,    "lisp",  "< %FILE%");
    provers[20] = new ProverInfo(20, "TLAPS",     "tlapm",         ProverCategory.DeclarativeProver,    "tla",   "%FILE%");
    provers[21] = new ProverInfo(21, "Twelf",     "twelf-server",  ProverCategory.DeclarativeProver,    "elf",   "%FILE%");
    provers[22] = new ProverInfo(22, "Imandra",   "imandra",       ProverCategory.DeclarativeProver,    "iml",   "%FILE%");

    // Tier 5: Auto-active verifiers (2)
    provers[23] = new ProverInfo(23, "Dafny",     "dafny",         ProverCategory.AutoActive,           "dfy",   "verify %FILE%");
    provers[24] = new ProverInfo(24, "Why3",      "why3",          ProverCategory.AutoActive,           "mlw",   "prove %FILE%");

    // Tier 6: Constraint solvers (5)
    provers[25] = new ProverInfo(25, "GLPK",      "glpsol",        ProverCategory.ConstraintSolver,     "lp",    "--lp %FILE%");
    provers[26] = new ProverInfo(26, "SCIP",      "scip",          ProverCategory.ConstraintSolver,     "pip",   "-f %FILE%");
    provers[27] = new ProverInfo(27, "MiniZinc",  "minizinc",      ProverCategory.ConstraintSolver,     "mzn",   "%FILE%");
    provers[28] = new ProverInfo(28, "Chuffed",   "fzn-chuffed",   ProverCategory.ConstraintSolver,     "fzn",   "%FILE%");
    provers[29] = new ProverInfo(29, "ORTools",   "ortools_solve", ProverCategory.ConstraintSolver,     "proto", "%FILE%");

    return provers;
}

// ---------------------------------------------------------------------------
// Proof result
// ---------------------------------------------------------------------------

record ProofResult {
    var success: bool;
    var prover: string;
    var proverId: int;
    var time: real;
    var exitCode: int;
    var output: string;
    var category: ProverCategory;
}

// ---------------------------------------------------------------------------
// Prover availability check
// ---------------------------------------------------------------------------

// Check if a prover executable exists on PATH. `stdout = pipeStyle.pipe`
// stops `which` from leaking the resolved path into the parent's stdout,
// which would otherwise mangle structured output (CSV, JSON) from callers
// like `bench_mrr`.
proc isProverAvailable(info: ProverInfo): bool {
    try {
        var whichProc = spawn(["which", info.executable],
                              stdout = pipeStyle.pipe,
                              stderr = pipeStyle.pipe);
        whichProc.wait();
        return whichProc.exitCode == 0;
    } catch {
        return false;
    }
}

// ---------------------------------------------------------------------------
// Cancellation token (L2.3)
// ---------------------------------------------------------------------------

// A shared cancellation flag used by `parallelProofSearchSpeculative`
// to signal in-flight losers as soon as the first winner has been
// established via the CAS. A `class` (not `record`) so that all
// `coforall` tasks share the same instance by reference.
//
// `cancelled.write(true)` is the only mutation; all readers are
// `read()` polls inside `tryProver`'s wait loop. The atomic semantics
// give us a happens-before edge from the winner's CAS to every
// loser's next poll — no extra synchronisation is required.
class CancelToken {
    var cancelled: atomic bool;
    proc init() {
        // `atomic bool` defaults to `false` after `init this` commits
        // field initialisation; no further write needed.
        init this;
    }
}

// ---------------------------------------------------------------------------
// Real prover invocation via subprocess
// ---------------------------------------------------------------------------

// Write goal content to a temporary file and invoke the prover. If
// `cancelToken` is non-nil and `cancelled.read()` returns true mid-poll,
// SIGKILL the child and return a cancelled-result (exitCode = -5).
// Callers that do not race (sequential / best-of) pass nil.
proc tryProver(info: ProverInfo, goal: string, timeout: int = defaultTimeout,
               cancelToken: borrowed CancelToken? = nil): ProofResult {
    var timer = new stopwatch();
    timer.start();

    // Check availability first
    if !isProverAvailable(info) {
        timer.stop();
        return new ProofResult(
            success = false,
            prover = info.name,
            proverId = info.id,
            time = timer.elapsed(),
            exitCode = -1,
            output = "Prover not available on PATH",
            category = info.category
        );
    }

    // Write goal to temp file
    const tmpDir = "/tmp/echidna-chapel";
    if !exists(tmpDir) then mkdir(tmpDir);

    // #159: provers that enforce module-name = filename (Agda, Idris2)
    // override the generic basename via filenameOverride. Default keeps
    // the locale-id-suffixed form so non-overriding provers stay
    // collision-free across locales.
    const tmpFile = if info.filenameOverride != ""
                    then tmpDir + "/" + info.filenameOverride
                    else tmpDir + "/goal_" + info.name:string + "_" + here.id:string + "." + info.fileExt;

    try {
        var f = open(tmpFile, ioMode.cw);
        var w = f.writer(locking=false);
        w.write(goal);
        w.close();
        f.close();
    } catch e {
        timer.stop();
        return new ProofResult(
            success = false,
            prover = info.name,
            proverId = info.id,
            time = timer.elapsed(),
            exitCode = -2,
            output = "Failed to write temp file: " + e.message(),
            category = info.category
        );
    }

    // Build argument vector. First entry is the executable; the rest come
    // from splitting `argTemplate` after `%FILE%` substitution. `list(string)`
    // is used rather than a fixed array because the argument count is
    // template-driven and varies per prover.
    //
    // #158: when info.cwd is set, wrap the call in `sh -c "cd <cwd> &&
    // exec <executable> <args>"` so the subprocess starts in the
    // configured directory. A shell wrapper (vs process-global chdir)
    // is required because chdir would race against other parallel
    // spawn calls inside a coforall. The parent's full environment
    // (incl. IDRIS2_PREFIX / IDRIS2_DATA_DIR) is inherited regardless
    // — POSIX spawn defaults preserve env.
    var cmdStr = info.argTemplate.replace("%FILE%", tmpFile);
    var argList: list(string);
    if info.cwd != "" {
        argList.pushBack("sh");
        argList.pushBack("-c");
        argList.pushBack("cd " + info.cwd + " && exec " + info.executable + " " + cmdStr);
    } else {
        argList.pushBack(info.executable);
        for part in cmdStr.split(" ") {
            if part.size > 0 then argList.pushBack(part);
        }
    }
    var args = argList.toArray();

    // Invoke prover subprocess. `stdout = pipeStyle.pipe` is required so
    // the parent can read the prover's output once it terminates; without
    // it the subprocess inherits the parent's stdout and `subproc.stdout`
    // is not a readable channel.
    try {
        var subproc = spawn(args, stdout = pipeStyle.pipe);

        // Bounded poll-wait: poll every 100 ms, capped at `timeout` seconds.
        // The previous implementation used `!proc.running` which is true
        // before the child has begun and after it has exited, so it was
        // both racy at startup and stopped polling once running latched.
        // L2.3: also break out if the shared `cancelToken` flips to true,
        // which the speculative-search winner sets after its CAS succeeds.
        var elapsed: real = 0.0;
        const pollInterval: real = 0.1;
        var preempted = false;
        while subproc.running && elapsed < timeout:real {
            sleep(pollInterval);
            elapsed += pollInterval;
            subproc.poll();
            if cancelToken != nil && cancelToken!.cancelled.read() {
                preempted = true;
                break;
            }
        }

        if preempted {
            // L2.3 preemption: the speculative-search winner has been
            // declared elsewhere. SIGKILL ourselves and return a
            // distinct exitCode = -5 so the caller's result table
            // distinguishes preempted-loser from timed-out from failed.
            subproc.sendPosixSignal(9);
            subproc.wait();
            timer.stop();
            try { remove(tmpFile); } catch { }
            return new ProofResult(
                success = false,
                prover = info.name,
                proverId = info.id,
                time = timer.elapsed(),
                exitCode = -5,
                output = "Preempted by speculative-search winner",
                category = info.category
            );
        }

        if subproc.running {
            // Timeout reached while child still alive — SIGKILL it.
            // 2.x renamed `send_signal` → `sendPosixSignal`.
            subproc.sendPosixSignal(9);
            subproc.wait();
            timer.stop();
            try { remove(tmpFile); } catch { }
            return new ProofResult(
                success = false,
                prover = info.name,
                proverId = info.id,
                time = timer.elapsed(),
                exitCode = -3,
                output = "Timeout after " + timeout:string + "s",
                category = info.category
            );
        }

        subproc.wait();
        timer.stop();

        var stdoutText = "";
        try {
            // 2.x: `subproc.stdout` is itself a `fileReader` when the
            // subprocess was spawned with `stdout = pipeStyle.pipe`, so
            // we read directly. The old `.reader(locking=false)` indirection
            // belonged to the 1.x `file`-based API.
            stdoutText = subproc.stdout.readAll(string);
        } catch { }

        try { remove(tmpFile); } catch { }

        return new ProofResult(
            success = subproc.exitCode == 0,
            prover = info.name,
            proverId = info.id,
            time = timer.elapsed(),
            exitCode = subproc.exitCode,
            output = stdoutText,
            category = info.category
        );
    } catch e {
        timer.stop();
        try { remove(tmpFile); } catch { }
        return new ProofResult(
            success = false,
            prover = info.name,
            proverId = info.id,
            time = timer.elapsed(),
            exitCode = -4,
            output = "Subprocess error: " + e.message(),
            category = info.category
        );
    }
}

// ---------------------------------------------------------------------------
// Search strategies
// ---------------------------------------------------------------------------

// Sequential proof search (baseline) — tries provers one by one
proc sequentialProofSearch(goal: string, provers: [] ProverInfo,
                           timeout: int = defaultTimeout): ProofResult {
    if verbose then
        writeln("Sequential search: trying ", provers.size, " provers one by one...");

    var totalTimer = new stopwatch();
    totalTimer.start();

    for prover in provers {
        if verbose then
            write("  Trying ", prover.name, "...");

        var result = tryProver(prover, goal, timeout);

        if verbose then
            writeln(if result.success then " ✓ SUCCESS (" + result.time:string + "s)"
                   else " ✗ " + result.output);

        if result.success {
            totalTimer.stop();
            if verbose then
                writeln("\nFound proof via ", result.prover, " in ",
                       totalTimer.elapsed(), " seconds");
            return result;
        }
    }

    totalTimer.stop();
    if verbose then
        writeln("\nNo proof found after ", totalTimer.elapsed(), " seconds");

    return new ProofResult(
        success = false, prover = "", proverId = -1,
        time = totalTimer.elapsed(), exitCode = -1,
        output = "All provers exhausted",
        category = ProverCategory.InteractiveAssistant
    );
}

// Parallel proof search — tries ALL provers concurrently via coforall
proc parallelProofSearch(goal: string, provers: [] ProverInfo,
                          timeout: int = defaultTimeout): ProofResult {
    if verbose then
        writeln("Parallel search: trying all ", provers.size,
               " provers concurrently...");

    var totalTimer = new stopwatch();
    totalTimer.start();

    // Results array — one per prover
    var results: [provers.domain] ProofResult;

    // Launch all provers in parallel
    coforall (prover, i) in zip(provers, provers.domain) {
        results[i] = tryProver(prover, goal, timeout);

        if verbose && results[i].success {
            writef("  ✓ %s succeeded in %.2dr seconds (exit %i)\n",
                   prover.name, results[i].time, results[i].exitCode);
        }
    }

    totalTimer.stop();

    // Find best successful result (fastest proof time)
    var bestIdx = -1;
    var bestTime = 1e18;

    for i in provers.domain {
        if results[i].success && results[i].time < bestTime {
            bestIdx = i;
            bestTime = results[i].time;
        }
    }

    if verbose {
        var successCount = + reduce [r in results] if r.success then 1 else 0;
        var availCount = + reduce [r in results] if r.exitCode != -1 then 1 else 0;
        writeln("\nParallel search completed in ",
               totalTimer.elapsed(), " seconds");
        writeln("  Available provers: ", availCount, "/", provers.size);
        writeln("  Successful proofs: ", successCount, "/", availCount);
    }

    if bestIdx >= 0 {
        return results[bestIdx];
    } else {
        return new ProofResult(
            success = false, prover = "", proverId = -1,
            time = totalTimer.elapsed(), exitCode = -1,
            output = "All provers exhausted",
            category = ProverCategory.InteractiveAssistant
        );
    }
}

// L2.2 speculative search — race all provers, return the first success.
//
// Semantics vs `parallelProofSearch` (best-of):
//   - parallelProofSearch waits for ALL tasks then picks the fastest
//     success. Wall time is bounded by the slowest prover.
//   - parallelProofSearchSpeculative records the first-completing
//     success via an atomic CAS and SIGKILLs any still-running losers
//     via the shared `CancelToken`. Wall time is bounded by the
//     fastest successful prover plus one poll-interval (~100 ms) of
//     observation lag on the losers.
//
// L2.3 cancellation: the winning task's CAS is paired with a write to
// the shared `CancelToken`. Loser tasks read the token at every poll
// step in `tryProver` and self-SIGKILL their subprocess as soon as
// the flag is observed. The atomic-bool semantics give us a
// happens-before edge from CAS-success to next-loser-poll, so no
// further locking is needed.
//
// Soundness: the monotone first-wins CAS still controls which index
// is returned. The cancellation flag only affects how the LOSERS
// terminate — their results land in the table with exitCode = -5
// instead of running to completion, but they are never returned to
// the caller because `winner` is set before any cancellation could
// race the CAS. See proofs/agda/ParallelSoundness.agda:
// `cancellation-safety` for the formal statement.
proc parallelProofSearchSpeculative(goal: string, provers: [] ProverInfo,
                                    timeout: int = defaultTimeout): ProofResult {
    if verbose then
        writeln("Speculative search: ", provers.size,
                " provers racing, first-success-wins");

    var totalTimer = new stopwatch();
    totalTimer.start();

    var results: [provers.domain] ProofResult;
    var winnerIdx: atomic int;
    winnerIdx.write(-1);
    var cancelToken = new owned CancelToken();

    coforall (prover, i) in zip(provers, provers.domain) {
        results[i] = tryProver(prover, goal, timeout, cancelToken.borrow());

        if results[i].success {
            // Monotone first-wins CAS: only the first successful
            // worker flips the atomic from -1 to its own index. The
            // paired write to cancelToken signals every still-polling
            // loser to SIGKILL its subprocess on the next poll.
            var expected = -1;
            if winnerIdx.compareAndSwap(expected, i) {
                cancelToken.cancelled.write(true);
            }
        }
    }

    totalTimer.stop();

    const winner = winnerIdx.read();
    if winner >= 0 {
        if verbose then
            writeln("\nSpeculative winner: ", results[winner].prover,
                    " in ", totalTimer.elapsed(), " s wall");
        return results[winner];
    }

    return new ProofResult(
        success = false, prover = "", proverId = -1,
        time = totalTimer.elapsed(), exitCode = -1,
        output = "All provers exhausted (speculative)",
        category = ProverCategory.InteractiveAssistant
    );
}

// Category-filtered parallel search — only try provers from a specific category
proc categorySearch(goal: string, provers: [] ProverInfo,
                     category: ProverCategory,
                     timeout: int = defaultTimeout): ProofResult {
    var filtered: list(ProverInfo);
    for p in provers {
        if p.category == category then
            filtered.pushBack(p);
    }

    if verbose then
        writeln("Category search (", category, "): ",
               filtered.size, " provers");

    return parallelProofSearch(goal, filtered.toArray(), timeout);
}

// ---------------------------------------------------------------------------
// Main demonstration
// ---------------------------------------------------------------------------

proc main() {
    var provers = buildProverRegistry();

    writeln("╔═══════════════════════════════════════════════════════════╗");
    writeln("║  ECHIDNA Chapel Metalayer — 30-Prover Parallel Search    ║");
    writeln("╚═══════════════════════════════════════════════════════════╝");
    writeln();

    // Availability check
    writeln("Prover availability:");
    var availCount = 0;
    for p in provers {
        var avail = isProverAvailable(p);
        if avail then availCount += 1;
        if verbose then
            writeln("  ", if avail then "✓" else "✗", " ", p.name,
                   " (", p.executable, ") — ", p.category);
    }
    writeln();
    writeln("Available: ", availCount, "/", provers.size);
    writeln();

    // Example: SMT-LIB goal (works with Z3, CVC5, Alt-Ergo)
    var smtGoal = "(set-logic QF_LIA)\n(declare-fun x () Int)\n(assert (= (+ x 1) (+ 1 x)))\n(check-sat)\n";

    writeln("═══════════════════════════════════════════════════════════");
    writeln("SMT Parallel Search");
    writeln("═══════════════════════════════════════════════════════════");
    var smtResult = categorySearch(smtGoal, provers, ProverCategory.SmtSolver, timeout=30);
    if smtResult.success then
        writeln("Best proof: ", smtResult.prover, " in ", smtResult.time, "s");
    writeln();

    // Full parallel search with a Lean goal
    var leanGoal = "theorem comm_add (n m : Nat) : n + m = m + n := Nat.add_comm n m\n";

    writeln("═══════════════════════════════════════════════════════════");
    writeln("Full 30-Prover Parallel Search (Lean goal)");
    writeln("═══════════════════════════════════════════════════════════");
    var fullResult = parallelProofSearch(leanGoal, provers, timeout=60);
    if fullResult.success then
        writeln("Best proof: ", fullResult.prover, " in ", fullResult.time, "s");

    writeln();
    writeln("╔═══════════════════════════════════════════════════════════╗");
    writeln("║  Chapel Metalayer Complete                                ║");
    writeln("╚═══════════════════════════════════════════════════════════╝");
}