// proof.el — Proof of native interruptibility for Neuron-dispatched agents.
//
// Concatenated after runtime/swarm.el (see run.sh). Demonstrates, with raw
// before/after counts, that a dispatched worker interrupted MID-TASK stops
// instantly (not after finishing the wrong workflow), absorbs a redirect
// (re-plans, keeping progress), or terminates cleanly.
//
// Three scenarios on the SAME 12-step plan, SAME per-step cost, SAME signal
// timing (sent ~50ms in ≈ after step 3):
//   A. BASELINE — the broken Claude-style worker: no mid-loop signal check.
//      A kill sent at step ~3 is ignored until the whole plan finishes → all 12
//      steps run = wasted work on a known-wrong task.
//   B. INTERRUPTIBLE KILL — swarm_worker_run: the kill is absorbed within one
//      step → stops at ~3, status=killed, ~9 steps of waste AVOIDED.
//   C. INTERRUPTIBLE REDIRECT — mirrors the live incident (build-python-synth →
//      native-fetch-render): the correction is absorbed mid-task; the 3 done
//      steps are kept; the worker re-plans onto the new goal and finishes it.

// ── per-step work — one bounded unit (~15ms) ──────────────────────────────────
fn demo_step(arg: String) -> String {
    let goal: String = json_get(arg, "goal")
    let idx: String = json_get(arg, "idx")
    let step: String = json_get(arg, "step")
    sleep_ms(15)
    return "did[" + goal + "] step#" + idx + " (" + step + ")"
}

// ── BASELINE: the broken, non-interruptible worker (Claude-style) ─────────────
// Same shape as swarm_worker_run BUT it never polls the token during the loop.
// It "finishes the workflow" and only notices the signal at the very end — the
// exact pattern Will called out. Reports how many steps it wasted post-signal.
fn broken_worker_run(arg: String) -> String {
    let tok: Int = str_to_int(json_get(arg, "tok"))
    let out_ch: Int = str_to_int(json_get(arg, "out"))
    let step_fn: String = json_get(arg, "step_fn")
    let purview: String = json_get_raw(arg, "purview")
    let goal: String = json_get(purview, "goal")
    let steps: String = json_get_raw(purview, "steps")
    let n: Int = json_array_len(steps)
    let idx: Int = 0
    // NO token check inside the loop — this is the bug.
    while idx < n {
        let step: String = json_array_get(steps, idx)
        let step_arg: String = "{\"goal\":\"" + goal + "\",\"idx\":" +
                               int_to_str(idx) + ",\"step\":" + step + "}"
        let tid: Int = __thread_create(step_fn, step_arg)
        let result: String = __thread_join(tid)
        __channel_send(out_ch, result)
        let idx = idx + 1
    }
    // Only NOW does it look at the control signal — too late.
    let late: String = token_check(tok)
    if str_eq(late, "") {
        __channel_send(out_ch, "[no signal]")
    } else {
        __channel_send(out_ch, "[TOO LATE: absorbed " + json_get(late, "sig") +
                              " only after running ALL " + int_to_str(n) +
                              " steps — wasted work]")
    }
    return "{\"status\":\"ran-to-completion\",\"completed\":" + int_to_str(idx) + "}"
}

// ── helpers ───────────────────────────────────────────────────────────────────

// drain_count — drain out_ch, print each line, return count of real step outputs
// (lines beginning with "did").
fn drain_and_report(out_ch: Int) -> Int {
    let done: Int = 0
    let did: Int = 0
    while done == 0 {
        let m: String = __channel_try_recv(out_ch)
        if str_eq(m, "") {
            let done = 1
        } else {
            println("      | " + m)
            if str_starts_with(m, "did") {
                let did = did + 1
            }
        }
    }
    return did
}

fn twelve_steps() -> String {
    return "[\"s0\",\"s1\",\"s2\",\"s3\",\"s4\",\"s5\",\"s6\",\"s7\",\"s8\",\"s9\",\"s10\",\"s11\"]"
}

fn main() -> Void {
    println("=====================================================================")
    println(" NATIVE INTERRUPTIBILITY — PROOF (canon 1ca4d3e9)")
    println(" plan: 12 bounded steps @ ~15ms; signal sent ~50ms in (≈ after step 3)")
    println("=====================================================================")

    // ── A. BASELINE — broken, non-interruptible ──
    println("")
    println("[A] BASELINE  broken worker (no mid-loop signal check) — Claude-style")
    let tokA: Int = token_new()
    let outA: Int = __channel_new(0)
    let pvA: String = purview_new("A", "build-wrong-thing", twelve_steps())
    let argA: String = "{\"tok\":" + int_to_str(tokA) + ",\"out\":" + int_to_str(outA) +
                       ",\"step_fn\":\"demo_step\",\"purview\":" + pvA + "}"
    let t0A: Int = time_now()
    let tidA: Int = __thread_create("broken_worker_run", argA)
    sleep_ms(50)
    println("      -> coordinator sends KILL at +" + int_to_str(time_now() - t0A) + "ms (≈step 3)")
    token_kill(tokA)
    let finA: String = __thread_join(tidA)
    let elapA: Int = time_now() - t0A
    let didA: Int = drain_and_report(outA)
    println("      RESULT: executed " + int_to_str(didA) + "/12 steps, wall=" +
            int_to_str(elapA) + "ms, final=" + finA)
    println("      >> ignored the kill, RAN ALL 12 — ~9 steps of KNOWN-WRONG waste")

    // ── B. INTERRUPTIBLE KILL ──
    println("")
    println("[B] INTERRUPTIBLE  swarm_worker_run + token_kill")
    let pvB: String = purview_new("B", "build-wrong-thing", twelve_steps())
    let hB: String = swarm_dispatch("demo_step", pvB)
    let tokB: Int = str_to_int(json_get(hB, "tok"))
    let outB: Int = str_to_int(json_get(hB, "out"))
    let tidB: Int = str_to_int(json_get(hB, "tid"))
    let t0B: Int = time_now()
    sleep_ms(50)
    println("      -> coordinator sends KILL at +" + int_to_str(time_now() - t0B) + "ms (≈step 3)")
    token_kill(tokB)
    let finB: String = __thread_join(tidB)
    let elapB: Int = time_now() - t0B
    let didB: Int = drain_and_report(outB)
    println("      RESULT: executed " + int_to_str(didB) + "/12 steps, wall=" +
            int_to_str(elapB) + "ms, final=" + finB)
    println("      >> STOPPED within one step of the signal — no wasted continuation")

    // ── C. INTERRUPTIBLE REDIRECT (the live incident) ──
    println("")
    println("[C] INTERRUPTIBLE  redirect mid-task: build-python-synth -> native-fetch-render")
    let pvC: String = purview_new("C", "build-python-synth-renderer", twelve_steps())
    let hC: String = swarm_dispatch("demo_step", pvC)
    let tokC: Int = str_to_int(json_get(hC, "tok"))
    let outC: Int = str_to_int(json_get(hC, "out"))
    let tidC: Int = str_to_int(json_get(hC, "tid"))
    let t0C: Int = time_now()
    sleep_ms(50)
    println("      -> coordinator REDIRECTS at +" + int_to_str(time_now() - t0C) + "ms (≈step 3)")
    token_redirect(tokC, "native-fetch-render", "[\"fetch\",\"realize\",\"cohere\"]")
    let finC: String = __thread_join(tidC)
    let elapC: Int = time_now() - t0C
    let didC: Int = drain_and_report(outC)
    println("      RESULT: executed " + int_to_str(didC) + " steps total, wall=" +
            int_to_str(elapC) + "ms, final=" + finC)
    println("      >> absorbed the correction mid-task: kept early progress,")
    println("         re-planned onto native-fetch-render, finished the RIGHT plan")

    // ── D. INTERRUPTIBLE PAUSE -> RESUME (hold state, then continue) ──
    println("")
    println("[D] INTERRUPTIBLE  pause mid-task, hold state, then resume to finish")
    let pvD: String = purview_new("D", "long-render", twelve_steps())
    let hD: String = swarm_dispatch("demo_step", pvD)
    let tokD: Int = str_to_int(json_get(hD, "tok"))
    let outD: Int = str_to_int(json_get(hD, "out"))
    let tidD: Int = str_to_int(json_get(hD, "tid"))
    let t0D: Int = time_now()
    sleep_ms(50)
    println("      -> coordinator PAUSES at +" + int_to_str(time_now() - t0D) + "ms (≈step 3)")
    token_pause(tokD)
    sleep_ms(60)
    println("      -> worker held idle for ~60ms; coordinator RESUMES at +" +
            int_to_str(time_now() - t0D) + "ms")
    token_resume(tokD)
    let finD: String = __thread_join(tidD)
    let didD: Int = drain_and_report(outD)
    println("      RESULT: executed " + int_to_str(didD) + "/12 steps, final=" + finD)
    println("      >> paused on the spot, held its plan, resumed and finished it")

    println("")
    println("=====================================================================")
    println(" A ran all 12 wrong steps. B stopped at ~3. C re-planned at ~3.")
    println(" Same plan, same timing, same signal — only the interruptible worker")
    println(" stops the instant it's told, like a human. QED.")
    println("=====================================================================")
}