/* Offline comparison of supplied extractions, never an import of review authority. */
(() => {
  "use strict";
  const limit = 16 * 1024 * 1024;
  const ignored = new Set(["proofReferences", "sourceLine", "review"]);
  const hash = value => typeof value === "string" && /^[a-f0-9]{64}$/.test(value);
  const ensure = (condition, message) => { if (!condition) throw new Error(message); };
  const canonical = value => JSON.stringify(value, function (_key, item) {
    return item && typeof item === "object" && !Array.isArray(item)
      ? Object.fromEntries(Object.keys(item).sort().map(key => [key, item[key]])) : item;
  });
  const specification = node => Object.fromEntries(Object.entries(node).filter(([key]) => !ignored.has(key)));
  function explicitSpecification(node) {
    const result = structuredClone(specification(node));
    // Only known readable fields with a nonempty explicit counterpart may be
    // omitted. Unknown metadata and all scope, binding and reference data stay.
    const omit = (item, pairs) => {
      if (!item || typeof item !== "object" || Array.isArray(item)) return;
      for (const [readable, explicit] of pairs) {
        if (Object.hasOwn(item, readable) && Object.hasOwn(item, explicit) &&
            typeof item[readable] === "string" && typeof item[explicit] === "string" && item[explicit])
          delete item[readable];
      }
    };
    const type = [["type", "explicitType"]];
    const each = (items, action) => { if (Array.isArray(items)) items.forEach(action); };
    omit(result, [...type, ["body", "explicitBody"]]);
    each(result.fields, field => { omit(field, type); omit(field.context, type); });
    each(result.parents, parent => omit(parent, type));
    each(result.recursorRules, rule => omit(rule, [["rhs", "explicitRhs"]]));
    for (const context of [result.statement, result.constructorTelescope]) {
      omit(context, [["conclusion", "explicitConclusion"]]);
      each(context?.binders, binder => omit(binder, type));
    }
    omit(result.structureContext, [["result", "explicitResult"]]);
    each(result.structureContext?.parameters, parameter => omit(parameter, type));
    omit(result.localStatementContext, [["conclusion", "explicitConclusion"]]);
    each(result.localStatementContext?.entries, entry => omit(entry, [...type, ["value", "explicitValue"]]));
    each(result.appliedPredicates?.entries, entry => omit(entry, [["expression", "explicitExpression"]]));
    return result;
  }
  function unique(values, key) {
    ensure(Array.isArray(values) && values.length <= 20000, "Invalid or oversized declaration inventory.");
    const result = new Map();
    for (const item of values) {
      const name = key ? item?.[key] : item;
      ensure(typeof name === "string" && name && !result.has(name), "Missing or duplicate declaration/reference.");
      result.set(name, item);
    }
    return result;
  }
  function closure(index, name) {
    const project = new Set(), boundary = new Set(), pending = [name];
    while (pending.length) {
      const item = pending.pop();
      if (project.has(item) || boundary.has(item)) continue;
      if (index.external.has(item)) { boundary.add(item); continue; }
      ensure(index.nodes.has(item), "Unresolved meaning dependency: " + item);
      project.add(item); pending.push(...index.nodes.get(item).dependencies);
    }
    return { project: [...project].sort(), boundary: [...boundary].sort() };
  }
  function meaningPath(indexed, root, target) {
    ensure(indexed.roots.has(root), "The starting argument must be a selected statement.");
    ensure(indexed.all.has(target), "Unknown target declaration: " + target);
    const parents = new Map([[root, null]]), queue = [root];
    // Breadth-first traversal retains cycles without following proof references
    // or expanding external boundaries. Sorted neighbors settle equal-length ties.
    for (let position = 0; position < queue.length && !parents.has(target); position++) {
      const name = queue[position];
      if (indexed.external.has(name)) continue;
      for (const dependency of [...indexed.nodes.get(name).dependencies].sort()) {
        if (parents.has(dependency)) continue;
        parents.set(dependency, name); queue.push(dependency);
      }
    }
    if (!parents.has(target)) return null;
    const path = [];
    for (let name = target; name !== null; name = parents.get(name)) path.push(name);
    return path.reverse();
  }
  function validateLocalContext(node) {
    if (!node.proofValued) {
      ensure(!("localStatementContext" in node), "Local statement context attached to nonproof.");
      return;
    }
    ensure("localStatementContext" in node, "Missing local statement context.");
    const context = node.localStatementContext;
    if (context === null) return;
    ensure(context && canonical(Object.keys(context).sort()) === canonical([
      "conclusion", "conclusionReferences", "entries", "explicitConclusion", "reconstructionChecked"]) &&
      context.reconstructionChecked === true && Array.isArray(context.entries) &&
      ["conclusion", "explicitConclusion"].every(key => typeof context[key] === "string" && context[key]),
      "Invalid local statement reconstruction.");
    const parts = [], prefix = [], used = new Set();
    let hasDefinition = false;
    context.entries.forEach((entry, position) => {
      ensure(entry && typeof entry.defined === "boolean" && typeof entry.propositionValued === "boolean" &&
        ["explicit", "implicit", "strictImplicit", "instance"].includes(entry.binding) &&
        ["name", "type", "explicitType"].every(key => typeof entry[key] === "string" && entry[key]),
        "Invalid local statement entry.");
      parts.push([position, entry.references]);
      if (entry.defined) {
        hasDefinition = true;
        ensure(entry.binding === "explicit" && ["value", "explicitValue"].every(key =>
          typeof entry[key] === "string" && entry[key]), "Missing assigned local value.");
        parts.push([position, entry.valueReferences]);
      } else {
        ensure(!["value", "explicitValue", "valueReferences"].some(key => key in entry), "Parameter has an assigned value.");
        if (!hasDefinition) prefix.push({ binding: entry.binding,
          hypothesis: entry.propositionValued, references: entry.references });
      }
    });
    const outer = node.statement?.binders?.map(binder => ({ binding: binder.binding,
      hypothesis: binder.hypothesis, references: binder.references }));
    ensure(hasDefinition && canonical(prefix) === canonical(outer),
      "Local context changed the outer parameter prefix.");
    parts.push([context.entries.length, context.conclusionReferences]);
    for (const [position, references] of parts) {
      ensure(references && canonical(Object.keys(references).sort()) === canonical(["binders", "declarations"]) &&
        Array.isArray(references.binders), "Missing local statement references.");
      const names = unique(references.declarations), indices = references.binders;
      ensure(canonical(references.declarations) === canonical([...names.keys()].sort()) &&
        [...names.keys()].every(name => node.dependencies.includes(name)), "Invalid local statement declarations.");
      ensure(indices.every(index => Number.isInteger(index) && index >= 0 && index < position) &&
        indices.every((index, i) => i === 0 || indices[i - 1] < index), "Invalid local statement scope.");
      names.forEach((_, name) => used.add(name));
    }
    ensure(canonical([...used].sort()) === canonical([...node.dependencies].sort()), "Incomplete local statement references.");
  }
  function validateAppliedPredicates(node, nodes) {
    if (!node.proofValued) {
      ensure(!("appliedPredicates" in node), "Applied predicates attached to nonproof."); return;
    }
    const local = !!node.localStatementContext, context = node.localStatementContext || node.statement;
    const binders = context[local ? "entries" : "binders"], expansions = node.appliedPredicates;
    ensure(expansions && canonical(Object.keys(expansions).sort()) === canonical(["entries", "scope"]) &&
      expansions.scope === (local ? "local" : "statement") && Array.isArray(expansions.entries),
      "Invalid applied-predicate scope.");
    let previous = -1;
    for (const entry of expansions.entries) {
      ensure(entry && canonical(Object.keys(entry).sort()) === canonical([
        "definition", "explicitExpression", "expression", "kernelChecked", "part", "references"]) &&
        entry.kernelChecked === true && ["part", "definition", "expression", "explicitExpression"].every(key =>
          typeof entry[key] === "string" && entry[key]), "Invalid applied-predicate expansion.");
      const position = entry.part === "conclusion" ? binders.length : binders.findIndex((_, i) => entry.part === String(i));
      ensure(previous < position && position <= binders.length, "Invalid applied-predicate order."); previous = position;
      ensure(position === binders.length || binders[position][local ? "propositionValued" : "hypothesis"],
        "Applied predicate attached to nonproposition.");
      const original = position === binders.length ? context.conclusionReferences : binders[position].references;
      const definition = nodes.get(entry.definition);
      ensure(definition?.kind === "definition" && !definition.proofValued && original.declarations.includes(entry.definition),
        "Applied predicate is not a referenced project definition.");
      const refs = entry.references;
      ensure(refs && canonical(Object.keys(refs).sort()) === canonical(["binders", "declarations"]) &&
        Array.isArray(refs.binders), "Missing applied-predicate references.");
      const names = unique(refs.declarations), allowed = new Set([...definition.dependencies, ...original.declarations]);
      ensure(canonical(refs.declarations) === canonical([...names.keys()].sort()) &&
        [...names.keys()].every(name => allowed.has(name)), "Invalid one-step predicate dependencies.");
      ensure(refs.binders.every(index => Number.isInteger(index) && index >= 0 && index < position) &&
        refs.binders.every((index, i) => i === 0 || refs.binders[i - 1] < index), "Invalid applied-predicate binder scope.");
    }
  }
  function index(report) {
    ensure([4, 5, 6, 7].includes(report?.schemaVersion) && report.humanSemanticApproval === false &&
      report.externalDefinitionsExpanded === false, "Unsupported extraction schema or scope.");
    const opened = "displayOpenNamespaces" in report ? report.displayOpenNamespaces : [];
    ensure(Array.isArray(opened) && opened.every(name => typeof name === "string" && name.length > 0) &&
      new Set(opened).size === opened.length, "Invalid display open namespaces.");
    const nodes = unique(report.nodes, "name"), external = unique(report.externalNodes, "name");
    const roots = unique(report.roots, "root"), all = new Map([...nodes, ...external]);
    ensure(all.size === nodes.size + external.size && roots.size > 0, "Invalid project/boundary/root inventory.");
    ensure(report.sourceFiles && Object.values(report.sourceFiles).every(hash) && hash(report.sourceSnapshot),
      "Missing extraction source fingerprints.");
    if ("interpretationContext" in report) {
      const context = report.interpretationContext;
      const fields = ["filename", "title", "subtitle", "scope", "source_label", "source_link", "source_note", "source_file"];
      ensure(context && canonical(Object.keys(context).sort()) === canonical([...fields, "exercises"].sort()) &&
        fields.every(key => typeof context[key] === "string" && context[key].trim()) &&
        Array.isArray(context.exercises) && canonical(context.exercises) === canonical(report.reviewExercises),
        "Invalid or inconsistent review interpretation context.");
      ensure(context.source_file.startsWith("docs/papers/") && !context.source_file.split("/").includes("..") &&
        hash(report.sourceFiles[context.source_file]), "Missing local interpretation-source fingerprint.");
    }
    for (const node of all.values()) {
      ensure(typeof node.type === "string" && typeof node.explicitType === "string" && typeof node.module === "string",
        "Missing declaration type or module.");
    }
    for (const node of external.values()) {
      ensure(Object.keys(node).every(key => ["name", "module", "kind", "type", "explicitType"].includes(key)),
        "External boundaries must contain declaration types only.");
    }
    for (const node of nodes.values()) {
      const dependencies = unique(node.dependencies), references = unique(node.proofReferences);
      ensure([...dependencies.keys(), ...references.keys()].every(name => all.has(name)), "Unresolved declaration reference.");
      ensure(Array.isArray(node.parents) && Array.isArray(node.recursorRules), "Missing structure or recursor inventory.");
      const fields = unique(node.fields, "name");
      ensure(node.isStructure || (!fields.size && !node.parents.length), "Fields attached to a nonstructure.");
      if (report.schemaVersion === 4) {
        ensure(!("structureContext" in node) && !("constructorTelescope" in node) && node.fields.every(field => !("context" in field)),
          "Constructor contexts require extraction schema 5.");
      } else if (node.isStructure) {
        const context = node.structureContext, constructor = all.get(context?.constructor);
        ensure(context && Array.isArray(context.parameters) && constructor?.kind === "constructor" &&
          dependencies.has(constructor.name) && Array.isArray(constructor.dependencies), "Missing contextual constructor.");
        const binders = [...context.parameters, ...node.fields.map(field => field.context)], used = new Set();
        const telescope = constructor.constructorTelescope;
        ensure(constructor.constructorInductive === node.name &&
          constructor.constructorParameters === context.parameters.length && constructor.constructorFields === node.fields.length &&
          telescope && canonical(telescope.binders) === canonical(binders) &&
          telescope.conclusion === context.result && telescope.explicitConclusion === context.explicitResult &&
          canonical(telescope.conclusionReferences) === canonical(context.resultReferences),
          "Field context differs from its constructor telescope.");
        binders.forEach((binder, position) => {
          ensure(binder && typeof binder.name === "string" && binder.name &&
            ["explicit", "implicit", "strictImplicit", "instance"].includes(binder.binding) &&
            typeof binder.hypothesis === "boolean" && ["type", "explicitType"].every(key =>
              typeof binder[key] === "string" && binder[key]), "Invalid contextual binder.");
          ensure(position < context.parameters.length || binder.binding === node.fields[position - context.parameters.length].binding,
            "Contextual field binding mismatch.");
        });
        ensure(["result", "explicitResult"].every(key => typeof context[key] === "string" && context[key]),
          "Missing contextual constructor result.");
        [...binders.map(binder => binder.references), context.resultReferences].forEach((part, position) => {
          ensure(part && canonical(Object.keys(part).sort()) === canonical(["binders", "declarations"]) &&
            Array.isArray(part.binders), "Missing constructor-part references.");
          const names = unique(part.declarations), indices = part.binders;
          ensure(canonical(part.declarations) === canonical([...names.keys()].sort()), "Unsorted constructor-part declarations.");
          ensure([...names.keys()].every(name => constructor.dependencies.includes(name)), "Invalid constructor-part declaration.");
          ensure(indices.every(index => Number.isInteger(index) && index >= 0 && index < position) &&
            indices.every((index, i) => i === 0 || indices[i - 1] < index), "Invalid constructor-part binder reference.");
          names.forEach((_, name) => used.add(name));
        });
        ensure(canonical([...used].sort()) === canonical([...constructor.dependencies].sort()),
          "Incomplete constructor-part declarations.");
      } else ensure(!("structureContext" in node), "Constructor context attached to a nonstructure.");
      node.fields.forEach((field, position) => {
        ensure(field.position === position && dependencies.has(field.name) &&
          ["explicit", "implicit", "strictImplicit", "instance"].includes(field.binding), "Invalid ordered field inventory.");
        ensure(field.subobject === null || all.has(field.subobject), "Unresolved embedded structure.");
        ensure(field.type === all.get(field.name).type && field.explicitType === all.get(field.name).explicitType,
          "Field type differs from its projection.");
      });
      const parents = unique(node.parents, "projection");
      node.parents.forEach((parent, position) => {
        ensure(parent.position === position && typeof parent.embedded === "boolean" &&
          dependencies.has(parent.structure) && dependencies.has(parent.projection), "Invalid parent inventory.");
        ensure(parent.type === all.get(parent.projection).type && parent.explicitType === all.get(parent.projection).explicitType,
          "Parent type differs from its projection.");
        ensure(parent.embedded ? fields.get(parent.projection)?.subobject === parent.structure : !fields.has(parent.projection),
          "Embedded and reconstructed parent fields disagree.");
      });
      ensure(node.fields.every(field => field.subobject === null || parents.has(field.name)), "Missing embedded parent.");
      ensure(!node.proofValued || (node.statement && !("body" in node) && !("explicitBody" in node)),
        "Proof implementation is not a semantic specification.");
      if (report.schemaVersion >= 6) validateLocalContext(node);
      else ensure(!("localStatementContext" in node), "Local statement contexts require extraction schema 6.");
      if (report.schemaVersion >= 7) validateAppliedPredicates(node, nodes);
      else ensure(!("appliedPredicates" in node), "Applied predicates require extraction schema 7.");
    }
    const result = { report, nodes, external, roots, all };
    for (const root of roots.values()) {
      ensure(nodes.has(root.root), "Selected statement is not expanded.");
      const reached = closure(result, root.root);
      ensure(canonical(reached.project) === canonical([...unique(root.declarations).keys()].sort()) &&
        canonical(reached.boundary) === canonical([...unique(root.externalBoundaries).keys()].sort()),
        "Selected meaning closure is incomplete.");
    }
    return result;
  }
  function encode(report) {
    index(report);
    const output = JSON.stringify({ format: "physicslogic-review-extraction", version: 1, report });
    ensure(new TextEncoder().encode(output).length <= limit, "Extraction exceeds the 16 MiB comparison limit.");
    return output;
  }
  function decode(text) {
    ensure(new TextEncoder().encode(text).length <= limit, "Extraction exceeds the 16 MiB comparison limit.");
    const parsed = JSON.parse(text);
    // Our compact export round-trips exactly; duplicate keys cannot silently disappear.
    ensure(JSON.stringify(parsed) === text && parsed.format === "physicslogic-review-extraction" && parsed.version === 1,
      "Use the unmodified compact JSON export from a review page; HTML and duplicate keys are not accepted.");
    return index(parsed.report);
  }
  function sources(indexed, names) {
    const paths = new Set(["lean-toolchain", "lake-manifest.json", "lakefile.toml"]);
    if (indexed.report.interpretationContext) paths.add(indexed.report.interpretationContext.source_file);
    for (const name of names) {
      const module = indexed.nodes.get(name).module;
      paths.add(indexed.report.moduleSources?.[module] || module.replaceAll(".", "/") + ".lean");
    }
    ensure([...paths].every(path => hash(indexed.report.sourceFiles[path])), "Missing owning-source fingerprint.");
    return Object.fromEntries([...paths].sort().map(path => [path, indexed.report.sourceFiles[path]]));
  }
  function compare(before, after, root) {
    ensure(before.roots.has(root), "This statement was not selected in the supplied earlier extraction.");
    ensure(after.roots.has(root), "This statement is not selected in the current extraction.");
    const oldScope = closure(before, root), newScope = closure(after, root);
    const previous = new Set([...oldScope.project, ...oldScope.boundary]);
    const current = new Set([...newScope.project, ...newScope.boundary]);
    const added = [...current].filter(name => !previous.has(name)).sort();
    const removed = [...previous].filter(name => !current.has(name)).sort();
    const different = [...current].filter(name => previous.has(name) &&
      (before.external.has(name) !== after.external.has(name) ||
        canonical(specification(before.all.get(name))) !== canonical(specification(after.all.get(name))))).sort();
    const schemaChanged = before.report.schemaVersion !== after.report.schemaVersion;
    const readableOnly = different.filter(name => !schemaChanged &&
      before.external.has(name) === after.external.has(name) &&
      canonical(explicitSpecification(before.all.get(name))) === canonical(explicitSpecification(after.all.get(name))));
    const readableNames = new Set(readableOnly);
    const changed = different.filter(name => !readableNames.has(name));
    const leftSources = sources(before, oldScope.project), rightSources = sources(after, newScope.project);
    const changedSources = [...new Set([...Object.keys(leftSources), ...Object.keys(rightSources)])]
      .filter(path => leftSources[path] !== rightSources[path]).sort();
    const interpretationChanges = differences(before.report.interpretationContext, after.report.interpretationContext);
    return { added, removed, changed, readableOnly, changedSources, interpretationChanges,
      unchanged: current.size - added.length - different.length, schemaChanged };
  }
  function differences(before, after, path = []) {
    if (canonical(before) === canonical(after)) return [];
    const object = item => item !== null && typeof item === "object";
    if (object(before) && object(after) && Array.isArray(before) === Array.isArray(after)) {
      return [...new Set([...Object.keys(before), ...Object.keys(after)])].flatMap(key =>
        differences(before[key], after[key], [...path, key]));
    }
    return [{ path, before, after }];
  }
  function compareScopes(indexed, left, right) {
    ensure(indexed.roots.has(left) && indexed.roots.has(right),
      "Both arguments must be selected statements in this extraction.");
    const first = closure(indexed, left), second = closure(indexed, right);
    const result = { left, right };
    for (const role of ["project", "boundary"]) {
      const a = new Set(first[role]), b = new Set(second[role]);
      result[role] = {
        shared: first[role].filter(name => b.has(name)),
        leftOnly: first[role].filter(name => !b.has(name)),
        rightOnly: second[role].filter(name => !a.has(name)),
      };
    }
    return result;
  }
  globalThis.PhysicsLogicComparison = Object.freeze({ limit, index, encode, decode, compare,
    compareScopes, meaningPath, specification, differences });
})();