candor-query 0.24.0

//! `candor unverified` — the provable-purity disclosure (a policy-guidance companion to `fix`, from
//! eval/fixloop/DISPATCH-NOTE.md). A `deny <E>` or `pure` rule PASSES a function that carries none of its
//! forbidden effects — but if that function is `Unknown` (candor could not resolve one of its calls), the
//! pass is UNVERIFIED: the Unknown could hide the very effect the rule forbids (the classic case is a
//! fn/closure-injected "port" — the layer reads as Unknown, so `deny Net domain`/`pure domain` clear it even
//! though the domain may reach Net at runtime). This names every such function in a governed layer and the
//! `deny <E> Unknown <scope>` upgrade that makes the intent provable. Advisory: exit 0, or `--strict` → exit
//! 1 so CI can REQUIRE provable purity. The gate's verdict is untouched — this only discloses the gap.
//!
//! ⟨0.24⟩ It ALSO names every function `gate --report` could not JUDGE (SPEC §3.2, candor-spec
//! `4fd140c`: *an advisory verb may be LESS certain than the gate, never more*) — with the MISSING
//! EVIDENCE as the reason, the gate's `unevaluated` shape beside it, and `--strict` → exit 2 there,
//! matching the gate.
//!
//! ⟨0.24⟩ …and over an INCOMPLETE report it omits `ok` entirely (SPEC §3.2, candor-spec `ec1a441`) —
//! see [`crate::completeness`], where the measurement and the reasoning live. **This verb is the
//! sharpest case in the family**: it exists to say *"your green gate is not provably green"*, and a
//! function in an unanalyzed file is absent from `functions`, so it cannot be enumerated as an
//! unverified pass at all — that absence is exactly what the verb would have to report.

use crate::grammar::{parse, report_or_discover, Shape};
use crate::load::load_entries;
use candor_classify::policy::{rule_and_upgrade, unverified_hole_rule, PolicyRule};
use candor_report::ReportEntry;

// ⟨0.24⟩ **THE REASON-CLASS FIXPOINT USED TO LIVE HERE, AND THAT WAS THE DEFECT'S HOME ADDRESS** (SPEC
// §3.2, candor-spec `4fd140c`). `reason_class_acc` was this verb's own copy of the gate's accumulator —
// the same two faults reasoned through twice, in two files — and *"an advisory verb may be LESS certain
// than the gate, never more"* is a COMPARISON between the two, which two copies can only ever satisfy by
// coincidence. Both this verb and `fix-gate` now read [`crate::gate::report_signature`], the accumulator
// `gate --report` itself is judged from, and take the ANSWERABILITY set from the same object.

pub(crate) fn cmd_unverified(args: &[String]) -> i32 {
    let g = parse(args, Shape { verb_args: 0, sentinel: true, has_policy: true });
    let Some(prefix) = report_or_discover(&g) else {
        eprintln!("candor: no report found (no --report and no .candor/ discovered) — scan the crate first.");
        return 2;
    };
    let prefix = &prefix;
    let want_json = g.want_json;
    let strict = g.strict;
    let policy_path = g.policy.clone().or_else(|| std::env::var("CANDOR_POLICY").ok());
    let Some(pp) = policy_path else {
        eprintln!("candor unverified: a policy is required (the check is relative to your pure/deny layers).");
        return 2;
    };
    // ⟨0.24⟩ Through the SHARED loader, and here the old bare `parse_policy` LOST A DISCLOSURE rather
    // than adding one: a hole is a function that PASSES its rule while being `Unknown`, so widening
    // `deny Unknown[<alias>]` to a bare `deny Unknown` reclassified real holes as violations-that-aren't
    // and this verb answered "every function in a pure/deny layer is PROVABLY clean ✓". §6.2: the gate
    // and the disclosure MUST apply the same rule.
    let parsed = match crate::policy::load_policy_as_the_gate_does("unverified", &pp) {
        Ok(p) => p,
        Err(code) => return code,
    };
    let rules = &parsed.rules;
    let entries = load_entries(prefix);
    if entries.is_empty() {
        eprintln!("candor unverified: no report for `{prefix}` — scan the crate first.");
        return 2;
    }

    // A hole: a function that is Unknown, sits in a deny/pure scope, and PASSES that rule (carries none of its
    // forbidden real effects). The predicate is `unverified_hole_rule` — the SAME one candor-scan's gate note
    // uses (candor_classify::policy), so the disclosure can never drift between the two paths.
    struct Hole<'a> {
        func: &'a ReportEntry,
        rule: &'a PolicyRule,
    }
    // `--class <c,…>` (SPEC §3.1 ⟨0.20⟩, semantics pinned normative at §6.2 ⟨0.24⟩): keep only holes
    // whose Unknown is of a matching reason class — resolved TRANSITIVELY, over the same reach the
    // `deny E Unknown[class]` gate resolves, and failing CLOSED on a hole nothing classified.
    // §6.2 ⟨0.24⟩: an unrecognised token is a USAGE ERROR (exit 2), never a silently narrowed filter —
    // see `parse_class_filter` for why this half of the rule is not the policy side's drop-with-warning.
    let class_filter = match g.class.as_deref().map(crate::containment::parse_class_filter).transpose() {
        Ok(v) => v,
        Err(msg) => {
            eprintln!("{msg}");
            return 2;
        }
    };
    let want: Option<std::collections::BTreeSet<&str>> = class_filter
        .as_ref()
        .map(|set| set.iter().map(|c| c.token()).collect());
    // Computed once. ⟨0.24⟩ UNCONDITIONALLY, where it used to be built only for `--class`: the hole
    // predicate itself needs it now, because a rule with a narrowing `Unknown[…]` filter PASSES or FIRES
    // on this very set, and the disclosure names the holes the gate did not clear. Making the fixpoint
    // conditional on the POLICY's shape as well would be a third place that has to agree about which
    // rules narrow — the arithmetic that decides is one traversal of a report already in memory.
    //
    // ⟨0.24⟩ AND IT IS THE GATE'S OWN SIGNATURE, not a second accumulator beside it (SPEC §3.2) — see the
    // note where `reason_class_acc` used to live.
    let sig = crate::gate::report_signature(&entries);
    let reason_acc = &sig.reason_classes;
    let class_matches = |e: &ReportEntry| -> bool {
        match &want {
            Some(w) => candor_classify::policy::reason_class_matches(reason_acc.get(&e.func), w),
            None => true, // no --class ⇒ no filter
        }
    };
    let no_classes: Vec<String> = Vec::new();
    let holes: Vec<Hole> = entries
        .iter()
        .filter_map(|e| {
            // ⟨0.20⟩ `netClass` is read VERBATIM off the wire, exactly as `gate --report` reads it — the
            // gate does not recompute it from the hosts on this route and neither may the disclosure.
            let nets = if e.net_class.is_empty() { &no_classes } else { &e.net_class };
            unverified_hole_rule(&e.func, &e.inferred, reason_acc.get(&e.func), nets, rules)
                .filter(|_| class_matches(e))
                .map(|rule| Hole { func: e, rule })
        })
        .collect();

    // ⟨0.24⟩ **THE FUNCTIONS THE GATE COULD NOT JUDGE AT ALL** — SPEC §3.2, candor-spec `4fd140c`:
    // *"where the gate would refuse for want of evidence, `unverified` MUST NAME the function."*
    //
    // THE DEFECT, measured four-way by conformance R11 and here on this engine before the fix: over a
    // report carrying `hosts` and no `netClass`, under `deny Net[unknown-host] app`, `gate --report`
    // exits 2 — §3.1 answerability, it CANNOT judge `app.noClass` — and this verb printed
    // `{"ok": false, "unverified": [app.nativeHole]}`, exit 0. It named a hole, so every "the verb said
    // SOMETHING" check passed; the function the gate withheld on was cleared in silence. **The verb whose
    // entire job is "your green gate is not provably green" was more confident than the gate over
    // identical bytes.**
    //
    // A function the gate COULD NOT JUDGE is an unverified hole in the strongest sense this verb has, so
    // it is named — and the reason recorded is **the MISSING EVIDENCE**, `why` verbatim from the gate's
    // own refusal. Recording what a derivation would have concluded instead (this engine could floor
    // `app.noClass` at `unknown-host` from its `hosts` in one line) is the move the ruling forbids: a
    // derivation is not a hedge, it is a second opinion, and it would restate the defect as a disclosure.
    //
    // **NOT SUBJECT TO `--class`.** That filter selects holes by REASON CLASS, and the whole content of
    // an entry here is that the class evidence is the thing missing — narrowing it away would be the
    // absence-keyed relaxation this rung exists to close, arriving through a flag.
    let unanswered = crate::gate::unanswerable_pairs(&parsed, &sig);

    // ⟨0.24⟩ **AND WHAT THE PRODUCING SCAN COULD NOT SEE AT ALL** — SPEC §3.2, candor-spec `ec1a441`.
    // The two disclosures are independent and both are needed: `unanswered` is a function candor DID
    // analyze and the gate could not JUDGE; this is source the scan never read, so there is no function
    // to name. MEASURED on the release build over a report declaring one `unanalyzed` unit, NO holes and
    // `deny Net app` that nothing violates: `{"ok": true, "unverified": []}`, exit 0 under `--strict`,
    // and the stdout line *"every function in a pure/deny layer is PROVABLY clean (no Unknown holes) ✓"*
    // — over a report that declares source candor could not read.
    let comp = crate::completeness::report_completeness(prefix);
    comp.warn_unreadable("unverified");

    if want_json {
        let mut items: Vec<_> = holes
            .iter()
            .map(|h| {
                let (rule, upgrade) = rule_and_upgrade(h.rule);
                serde_json::json!({
                    "fn": h.func.func,
                    "rule": rule,
                    "unknownWhy": h.func.unknown_why,
                    "upgrade": upgrade,
                })
            })
            .collect();
        // `rule` is the join field a consumer already uses against `unevaluated` (SPEC §3.1), and `why`
        // is the SAME string the pair carries — one function built both, so the two cannot drift. There
        // is no `upgrade`: no policy edit makes a missing field appear, and printing one would advise a
        // remedy for the wrong problem.
        items.extend(unanswered.iter().map(|u| {
            serde_json::json!({ "fn": u.func, "rule": u.rule, "why": u.why })
        }));
        let out = serde_json::json!({
            "ok": items.is_empty(),
            "unverified": items,
            // ⟨0.24⟩ THE GATE'S OWN SHAPE, `[{rule, why}]` (SPEC §3.1 `fc4b5f6`), one entry per RULE —
            // deliberately NOT a second spelling. Omitted entirely when everything was answerable, so an
            // ordinary document stays byte-identical to a pre-ruling one.
            "unevaluated": unevaluated_json(&unanswered),
        });
        let mut out = out;
        if unanswered.is_empty() {
            out.as_object_mut().unwrap().remove("unevaluated");
        }
        // ⟨0.24⟩ `ok` is REMOVED, not set to `false` (SPEC §3.2 `ec1a441`): `false` here would assert
        // "an unverified hole exists, here it is" beside an empty array — a finding the analysis never
        // made. `unverified` and `unevaluated` still ship: a partial answer that says it is partial
        // beats a refusal. On a COMPLETE report nothing below fires and the document is byte-identical.
        //
        // ⟨0.24⟩ **AND THE WITHHELD-RULE TRIGGER TAKES THE SAME ANSWER** (SPEC §3.2 `142740a`). This
        // engine emitted `ok: false` there, which `4fd140c` argued for deliberately and which was wrong
        // by that same clause's own reasoning: where a rule was WITHHELD, no hole was FOUND — the
        // question was declined — so `false` asserts the finding that did not happen. The two triggers
        // were ruled a day apart and looked like two cases; they are one shape and one answer.
        // MEASURED here before the change: `deny Net[unknown-host] app` over a `hosts`-only entry gave
        // `{"ok": false, …}` while `gate --report` refused outright. `fix-gate` was already right.
        if comp.incomplete() || !unanswered.is_empty() {
            out.as_object_mut().unwrap().remove("ok");
            comp.write_json(&mut out);
        }
        println!("{}", serde_json::to_string_pretty(&out).unwrap());
        return unverified_exit(strict, !holes.is_empty(), !unanswered.is_empty(), comp.incomplete());
    }

    // ⟨0.24⟩ THE HUMAN CHANNEL, AND IT IS THE ONE A TEST CANNOT SEE. A mutant that kept the whole JSON
    // fix and deleted this call survived the entire suite (SPEC §3.2 `ec1a441`) — the prose `✓` IS the
    // prose `ok: true`. Printed FIRST, so it qualifies the lists below as much as the verdict.
    comp.print_note(
        "the functions named below are only those candor could see",
        "A function in one of those is ABSENT from the report, so it cannot be named here at all. \
         `gate --report` exits 2 over these bytes. Re-scan for a complete answer.",
    );

    if holes.is_empty() && unanswered.is_empty() {
        if comp.incomplete() {
            // NO `✓`, and not "PROVABLY" anything. The withheld tick is the same withdrawal `ok` is:
            // a claim of provable purity over a set candor is on record as not having seen.
            println!(
                "candor unverified: nothing candor COULD SEE is an unverified hole — but see the \
                 INCOMPLETE note above; this is NOT the provably-clean all-clear."
            );
            return unverified_exit(strict, false, false, true);
        }
        println!("candor unverified: every function in a pure/deny layer is PROVABLY clean (no Unknown holes) ✓");
        return 0;
    }
    if !holes.is_empty() {
        println!(
            "candor unverified — {} function(s) PASS their policy but aren't PROVABLY clean:\n",
            holes.len()
        );
    }
    let mut upgrades: std::collections::BTreeSet<String> = std::collections::BTreeSet::new();
    for h in &holes {
        let (rule, upgrade) = rule_and_upgrade(h.rule);
        upgrades.insert(upgrade.clone());
        println!("  `{}`  (in `{rule}`)", h.func.func);
        let why = if h.func.unknown_why.is_empty() {
            "an unresolvable call".to_string()
        } else {
            h.func.unknown_why.join(", ")
        };
        println!("     is Unknown ({why}) — candor can't confirm it's free of the forbidden effect(s);");
        println!("     the Unknown could hide the very effect the rule forbids (e.g. a fn/closure-injected port).");
        println!("     → make it provable:  add  `{upgrade}`");
        println!();
    }
    if !unanswered.is_empty() {
        println!(
            "candor unverified — {} function(s) the GATE COULD NOT JUDGE over this report (`candor-query \
             gate --report` refuses on them, SPEC §3.1):\n",
            unanswered.len()
        );
        for u in &unanswered {
            println!("  `{}`  (in `{}`)", u.func, u.rule);
            println!("     {}", u.why);
            println!();
        }
    }
    if !holes.is_empty() {
        // "on these" ONLY when the unanswered block is also on screen, where an unqualified "the gate
        // still PASSES" would be false. With nothing unanswered the sentence is the pre-ruling one, to
        // the byte — measured across 224 OLD/NEW runs over four corpora and eight policies, where this
        // line was the ONLY difference until it was made conditional.
        //
        // ⟨0.24⟩ …and over an INCOMPLETE report it is not narrowed but WITHDRAWN, because it is false:
        // `gate --report` over these bytes exits 2, so "the gate still PASSES" is a claim about the
        // gate that the gate contradicts. Found by reading this verb's every printed sentence for the
        // claim it makes, which is what `ec1a441`'s every-channel clause asks for — the `✓` was not the
        // only one.
        if comp.incomplete() {
            println!(
                "  The gate does NOT pass over this report — it declares unanalyzed unit(s) (above) and \
                 `gate --report` exits 2. Once the scan is complete, to REQUIRE provable purity add:"
            );
        } else {
            let scope = if unanswered.is_empty() { "" } else { " on these" };
            println!("  The gate still PASSES{scope} — this is advisory. To REQUIRE provable purity, add:");
        }
        for u in &upgrades {
            println!("      {u}");
        }
    }
    unverified_exit(strict, !holes.is_empty(), !unanswered.is_empty(), comp.incomplete())
}

/// ⟨0.24⟩ The `unevaluated` disclosure — the gate's `[{rule, why}]`, ONE ENTRY PER RULE.
///
/// Per-rule rather than per-function because that is the shape `gate --report` emits and SPEC §3.1
/// `fc4b5f6` fixes; the per-FUNCTION detail is in `unverified` itself, where the ruling puts it, and the
/// two join on `rule`.
fn unevaluated_json(unanswered: &[crate::gate::Unanswerable]) -> Vec<serde_json::Value> {
    let mut seen: std::collections::BTreeSet<&str> = std::collections::BTreeSet::new();
    unanswered
        .iter()
        .filter(|u| seen.insert(u.rule.as_str()))
        .map(|u| serde_json::json!({ "rule": u.rule, "why": u.why }))
        .collect()
}

/// ⟨0.24⟩ `--strict`'s exit code, with the REFUSAL DOMINATING (SPEC §3.2, candor-spec `4fd140c`:
/// *"`--strict` exits 2, matching the gate"*).
///
/// **THE PRECEDENCE IS THE OPPOSITE OF THE GATE'S, AND FOR THE GATE'S OWN REASON.** There, a firing rule
/// dominates a refusal because `Reject` is upward-closed: exit 1 is CERTAIN and no missing evidence can
/// un-reject it. Here neither outcome is certain — both are advisory — and the question the exit code
/// answers is *did this verb evaluate the policy you gave it?*. Where the gate answered "no" with a 2,
/// this verb answering 1 would claim it got further than the gate did on identical bytes, which is the
/// bound the ruling sets. So 2 wins, and the holes are still all named in the document either way.
///
/// Without `--strict` the verb is advisory and exits 0, unchanged: the ruling is about the DISCLOSURE,
/// and minting a non-zero exit for the default agent-loop invocation would fail builds this verb has
/// never failed.
///
/// ⟨0.24⟩ **AN INCOMPLETE REPORT JOINS THE 2**, SPEC §3.2 `ec1a441` — *"`--strict` (the CI form) exits
/// 2"* — and it is the same argument one rung along: `gate --report` exits 2 over these bytes, so
/// answering 0 (or 1) claims this verb got further than the gate on identical input. It sits beside the
/// refusal rather than under it because both are the SAME answer, *this verb did not evaluate the
/// policy you gave it over the code you gave it*.
fn unverified_exit(strict: bool, any_holes: bool, any_unanswered: bool, incomplete: bool) -> i32 {
    match (strict, any_unanswered || incomplete, any_holes) {
        (true, true, _) => 2,
        (true, false, true) => 1,
        _ => 0,
    }
}