package gudusoft.gsqlparser.lineage.v2.fold;

import gudusoft.gsqlparser.lineage.v2.Finding;
import gudusoft.gsqlparser.lineage.v2.json.CanonicalJson;
import gudusoft.gsqlparser.lineage.v2.validation.DocumentIndex;

import java.util.ArrayDeque;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.Collections;
import java.util.Comparator;
import java.util.Deque;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Iterator;
import java.util.LinkedHashMap;
import java.util.LinkedHashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;
import java.util.TreeMap;
import java.util.TreeSet;

import static gudusoft.gsqlparser.lineage.v2.validation.DocumentIndex.intRef;
import static gudusoft.gsqlparser.lineage.v2.validation.DocumentIndex.items;

/**
 * FOLD-V1 ({@code lineage-spec/algorithms/fold-v1.md}): folds the ExplainGraph of one statement of a document
 * into its Fact Occurrences, FactCandidates and write requirements.
 *
 * <p>The kernel reads the document the way the reference runner ({@code conformance/run.py}, class
 * {@code Projector}) does, so that a validator built on it reports what the reference reports. It also computes
 * what the reference leaves out and the specification defines: the derived-unit rules of Section 7.3 (every walk
 * of a statement whose derived text is only {@code OBSERVED} is {@code ASSUMED}, every write at most
 * {@code PARTIAL}), the bindings of every Occurrence (Sections 7.1, item 6 and 8.1, item 2), the ordinals of
 * FactCandidates (identity-v1, Section 5.4), and the complete requirements of every write (Sections 7.4 and
 * 7.5).</p>
 *
 * <p>Exploration is over states (node, label, choices, proof) and terminates on every graph (Section 6). Its
 * cost grows with the states reached and, for a group of linked ambiguous references, with the number of worlds
 * (the product of their alternatives); both are bounded, and a statement over a bound throws
 * {@link FoldLimitException}.</p>
 *
 * @since 4.2.17
 */
public final class FoldKernel {

    /** The most exploration states one statement may reach (every state counts, the first and the last too). */
    public static final int DEFAULT_MAX_STATES = 500000;
    /** The most worlds one group of linked references, or one Fact test, may examine. */
    public static final int DEFAULT_MAX_WORLDS = 1 << 16;

    static final String SOURCE = "SOURCE";
    static final String TARGET = "TARGET";
    private static final String PROVEN = "PROVEN";
    private static final String ASSUMED = "ASSUMED";
    private static final List<String> CONTAINER_NODE_KINDS = Arrays.asList("RESULT_SET", "CTE", "SUBQUERY",
            "SET_OPERATION", "TABLE_FUNCTION", "PIVOT");
    private static final Map<String, Integer> RANK = new HashMap<String, Integer>();

    static {
        RANK.put("COMPLETE", 2);
        RANK.put("PARTIAL", 1);
        RANK.put("UNKNOWN", 0);
    }

    /** The alternative "something not listed" of an INCOMPLETE candidate set (Section 7.1, item 1). */
    static final Object NOT_LISTED = new Object() {
        @Override
        public String toString() {
            return "NOT_LISTED";
        }
    };

    private final DocumentIndex index;
    private final int maxStates;
    private final int maxWorlds;
    private final Object defaultCompleteness;
    private final Map<Long, Object> statementCompleteness = new HashMap<Long, Object>();
    /** The candidate sets of the ExplainGraph by ref; the last one with a ref wins, as in the reference. */
    private final Map<Long, Map<?, ?>> graphCsets = new HashMap<Long, Map<?, ?>>();
    private final Map<Object, Set<String>> refSide = new HashMap<Object, Set<String>>();
    private final Map<Object, Position> refPosition = new HashMap<Object, Position>();
    private final List<Map<?, ?>> allEdges;
    private final TreeMap<Long, List<Map<?, ?>>> edgesByStatement = new TreeMap<Long, List<Map<?, ?>>>();
    private final List<Long> statements;

    public FoldKernel(DocumentIndex index) {
        this(index, DEFAULT_MAX_STATES, DEFAULT_MAX_WORLDS);
    }

    public FoldKernel(DocumentIndex index, int maxStates, int maxWorlds) {
        this.index = index;
        this.maxStates = maxStates;
        this.maxWorlds = maxWorlds;
        Map<?, ?> graph = index.graph();
        defaultCompleteness = graph.get("completeness");
        for (Map<?, ?> entry : items(graph.get("statementCompleteness"))) {
            statementCompleteness.put(intRef(entry.get("statementRef")), entry.get("completeness"));
        }
        for (Map<?, ?> cset : items(graph.get("candidateSets"))) {
            Long ref = intRef(cset.get("ref"));
            if (ref != null) {
                graphCsets.put(ref, cset);
            }
        }
        allEdges = index.all("microEdge");
        for (Map<?, ?> edge : allEdges) {
            for (Choice choice : choices(edge)) {
                Set<String> sides = refSide.get(choice.ref);
                if (sides == null) {
                    sides = new TreeSet<String>();
                    refSide.put(choice.ref, sides);
                }
                sides.add(choice.side);
                Position position = Position.of(edge);
                Position known = refPosition.get(choice.ref);
                if (known == null || position.compareTo(known) < 0) {
                    refPosition.put(choice.ref, position);
                }
            }
            Long statement = intRef(edge.get("statementRef"));
            if (statement != null) {
                List<Map<?, ?>> list = edgesByStatement.get(statement);
                if (list == null) {
                    list = new ArrayList<Map<?, ?>>();
                    edgesByStatement.put(statement, list);
                }
                list.add(edge);
            }
        }
        TreeSet<Long> all = new TreeSet<Long>(edgesByStatement.keySet());
        for (Map<?, ?> statement : index.all("statement")) {
            all.add(intRef(statement.get("ref")));
        }
        statements = Collections.unmodifiableList(new ArrayList<Long>(all));
    }

    // ---------------------------------------------------------------------------------------------
    // Values compared the way the reference compares them: integers by value, everything else by equals.
    // ---------------------------------------------------------------------------------------------

    static Object norm(Object value) {
        Long ref = intRef(value);
        return ref != null ? ref : value;
    }

    static boolean same(Object a, Object b) {
        Object x = norm(a);
        Object y = norm(b);
        return x == null ? y == null : x.equals(y);
    }

    static int hash(Object value) {
        Object x = norm(value);
        return x == null ? 0 : x.hashCode();
    }

    /** Orders refs (and null, the key of a reference without a candidate set) the way the reference sorts ints. */
    static final Comparator<Object> REF_ORDER = new Comparator<Object>() {
        @Override
        public int compare(Object a, Object b) {
            Object x = norm(a);
            Object y = norm(b);
            if (x == null || y == null) {
                return x == null ? (y == null ? 0 : -1) : 1;
            }
            if (x instanceof Long && y instanceof Long) {
                return ((Long) x).compareTo((Long) y);
            }
            if (x instanceof Long || y instanceof Long) {
                return x instanceof Long ? -1 : 1;
            }
            return compareCodePoints(String.valueOf(x), String.valueOf(y));
        }
    };

    /** Unsigned UTF-8 byte order, which is code point order. */
    static int compareCodePoints(String a, String b) {
        int i = 0;
        int j = 0;
        while (i < a.length() && j < b.length()) {
            int x = a.codePointAt(i);
            int y = b.codePointAt(j);
            if (x != y) {
                return x < y ? -1 : 1;
            }
            i += Character.charCount(x);
            j += Character.charCount(y);
        }
        return (a.length() - i) == 0 ? ((b.length() - j) == 0 ? 0 : -1) : 1;
    }

    static Set<Set<StatementFold.Pair>> frozenOutcomes(Set<Set<StatementFold.Pair>> outcomes) {
        Set<Set<StatementFold.Pair>> out = new LinkedHashSet<Set<StatementFold.Pair>>();
        for (Set<StatementFold.Pair> outcome : outcomes) {
            out.add(Collections.unmodifiableSet(new LinkedHashSet<StatementFold.Pair>(outcome)));
        }
        return Collections.unmodifiableSet(out);
    }

    // ---------------------------------------------------------------------------------------------
    // Classification (Section 3)
    // ---------------------------------------------------------------------------------------------

    public DocumentIndex getIndex() {
        return index;
    }

    /** Every statement of the document and every statement a micro-edge names, in ref order. */
    public List<Long> getStatements() {
        return statements;
    }

    /** The micro-edges of one statement, in ref order. */
    public List<Map<?, ?>> edgesOf(long statement) {
        List<Map<?, ?>> edges = edgesByStatement.get(statement);
        return edges == null ? Collections.<Map<?, ?>>emptyList() : Collections.unmodifiableList(edges);
    }

    /** The ExplainGraph completeness of a statement: its {@code statementCompleteness} entry or the graph's. */
    public Object completeness(long statement) {
        return statementCompleteness.containsKey(statement) ? statementCompleteness.get(statement)
                : defaultCompleteness;
    }

    public boolean kept(Object ref) {
        return index.get("endpoint", ref) != null;
    }

    Map<?, ?> node(Object ref) {
        return index.get("node", ref);
    }

    public boolean folded(Object ref) {
        Map<?, ?> node = node(ref);
        return node != null && !"TERMINAL".equals(node.get("kind"));
    }

    boolean terminal(Object ref) {
        Map<?, ?> node = node(ref);
        return node != null && "TERMINAL".equals(node.get("kind"));
    }

    /** True when the ref names a candidate set of the ExplainGraph (the source of an UNRESOLVED reference). */
    public boolean graphCset(Object ref) {
        Long key = intRef(ref);
        return key != null && graphCsets.containsKey(key);
    }

    /**
     * The kept field-class endpoints (Section 3.1, 3.2): fields, declared variables and routine parameters, which have
     * a value a later statement can read; a write targets one of them.
     */
    static final java.util.List<String> FIELD_CLASS_KINDS = java.util.Arrays.asList("FIELD", "VARIABLE", "PARAMETER");

    boolean isField(Object ref) {
        Map<?, ?> endpoint = index.get("endpoint", ref);
        return endpoint != null && FIELD_CLASS_KINDS.contains(endpoint.get("kind"));
    }

    private String endClass(Object ref) {
        Map<?, ?> endpoint = index.get("endpoint", ref);
        if (endpoint != null) {
            Object kind = endpoint.get("kind");
            return "ROW_SET".equals(kind) ? "ROWSET" : FIELD_CLASS_KINDS.contains(kind) ? "FIELD" : null;
        }
        Map<?, ?> node = node(ref);
        if (node != null) {
            Object kind = node.get("kind");
            if ("ROW_SET".equals(kind)) {
                return "ROWSET";
            }
            return CONTAINER_NODE_KINDS.contains(kind) ? null : "FIELD";
        }
        return graphCset(ref) ? "FIELD" : null;
    }

    /** True when the statement lies in a derived source unit whose text is only observed (Section 7.3). */
    public boolean observed(long statement) {
        Map<?, ?> record = index.get("statement", statement);
        Map<?, ?> unit = record == null ? null : index.get("sourceUnit", record.get("sourceUnitRef"));
        return unit != null && "OBSERVED".equals(unit.get("derivedTextStatus"));
    }

    // ---------------------------------------------------------------------------------------------
    // Ambiguous references (Sections 6 and 7.1)
    // ---------------------------------------------------------------------------------------------

    static final class Choice {
        final Object ref;
        final Object alternative;
        final String side;

        Choice(Object ref, Object alternative, String side) {
            this.ref = norm(ref);
            this.alternative = alternative == NOT_LISTED || alternative == UNPAIRED ? alternative : norm(alternative);
            this.side = side;
        }
    }

    static boolean ambiguous(Object binding) {
        if (!(binding instanceof Map<?, ?>)) {
            return false;
        }
        Object status = ((Map<?, ?>) binding).get("status");
        return "CANDIDATE".equals(status) || "UNRESOLVED".equals(status);
    }

    /**
     * (reference, alternative, side) for each ambiguous binding of a micro-edge, source side first. A walk keeps the
     * references as written (they make its group, Section 7.1, item 4); the worlds are those of their deciding
     * references (decidedSigma).
     */
    List<Choice> choices(Map<?, ?> edge) {
        return rawChoices(edge);
    }

    /** Whether a reference is decided by another (its candidate set has decidedBy, Section 4.3). */
    boolean isDecided(Object ref) {
        Map<?, ?> cset = ref instanceof Long ? graphCsets.get(ref) : null;
        return cset != null && cset.get("decidedBy") instanceof Map<?, ?>;
    }

    /**
     * Sigma.extend, and two references decided by one reference take one of its alternatives (Section 7.1, item 1):
     * null when they take two.
     */
    Sigma extend(Sigma sigma, List<Choice> choices) {
        Sigma out = sigma.extend(choices);
        if (out == null || choices.isEmpty()) {
            return out;
        }
        boolean decided = false;
        for (Object r : out.refs) {
            decided |= isDecided(r);
        }
        if (!decided) {
            return out;
        }
        // every choice as worlds see it, the deciding reference's own included (Codex 13a #4)
        Map<Object, Object> taken = new HashMap<Object, Object>();
        for (int i = 0; i < out.refs.length; i++) {
            Choice d = decide(new Choice(out.refs[i], out.alternatives[i], null));
            if (taken.containsKey(d.ref) && !sameAlternative(taken.get(d.ref), d.alternative)) {
                return null;
            }
            taken.put(d.ref, d.alternative);
        }
        return out;
    }

    /** The choices of a walk as worlds see them: a decided reference's as its deciding reference's (Section 7.1). */
    Sigma decidedSigma(Sigma sigma) {
        boolean decided = false;
        for (Object r : sigma.refs) {
            decided |= isDecided(r);
        }
        if (!decided) {
            return sigma;
        }
        TreeMap<Object, Object> chosen = new TreeMap<Object, Object>(REF_ORDER);
        for (int i = 0; i < sigma.refs.length; i++) {
            Choice d = decide(new Choice(sigma.refs[i], sigma.alternatives[i], null));
            if (!chosen.containsKey(d.ref)) {
                chosen.put(d.ref, d.alternative);
            }
        }
        return new Sigma(chosen.keySet().toArray(), chosen.values().toArray());
    }

    /** A decided reference's alternative of an edge that its alignment pairs with no alternative. */
    static final Object UNPAIRED = new Object() {
        @Override
        public String toString() {
            return "UNPAIRED";
        }
    };

    /**
     * The choice of the deciding reference that a decided reference's choice is: the alternative its alignment pairs
     * with the candidate (UNPAIRED when none, which the shape check reports). Other choices are returned as they are.
     */
    Choice decide(Choice choice) {
        Map<?, ?> cset = choice.ref instanceof Long ? graphCsets.get(choice.ref) : null;
        Object decided = cset == null ? null : cset.get("decidedBy");
        if (!(decided instanceof Map<?, ?>)) {
            return choice;
        }
        Object deciding = ((Map<?, ?>) decided).get("candidateSetRef");
        if (choice.alternative != NOT_LISTED) {
            for (Map<?, ?> pair : items(((Map<?, ?>) decided).get("alignment"))) {
                if (sameAlternative(norm(pair.get("candidateRef")), choice.alternative)) {
                    return new Choice(deciding, pair.get("alternativeRef"), choice.side);
                }
            }
        }
        return new Choice(deciding, UNPAIRED, choice.side);
    }

    /** The candidate set a binding names, as the reference the fold chooses for: its deciding set when it is decided. */
    Object choiceRef(Object candidateSetRef) {
        Long key = intRef(candidateSetRef);
        Map<?, ?> cset = key == null ? null : graphCsets.get(key);
        Object decided = cset == null ? null : cset.get("decidedBy");
        return decided instanceof Map<?, ?> ? norm(((Map<?, ?>) decided).get("candidateSetRef")) : norm(candidateSetRef);
    }

    /** (reference, alternative, side) for each ambiguous binding of a micro-edge as written, source side first. */
    List<Choice> rawChoices(Map<?, ?> edge) {
        List<Choice> out = new ArrayList<Choice>(2);
        Object binding = edge.get("sourceBinding");
        if (ambiguous(binding)) {
            Object source = edge.get("sourceRef");
            out.add(new Choice(((Map<?, ?>) binding).get("candidateSetRef"), graphCset(source) ? NOT_LISTED : source,
                    SOURCE));
        }
        binding = edge.get("targetBinding");
        if (ambiguous(binding)) {
            out.add(new Choice(((Map<?, ?>) binding).get("candidateSetRef"), edge.get("targetRef"), TARGET));
        }
        return out;
    }

    /** The members of a candidate set of the graph. */
    List<Object> members(Object ref) {
        List<Object> out = alternatives(ref);
        out.remove(NOT_LISTED);
        return out;
    }

    /** The alternatives of a reference: its members, and NOT_LISTED unless its membership is COMPLETE. */
    List<Object> alternatives(Object ref) {
        Long key = intRef(ref);
        Map<?, ?> cset = key == null ? null : graphCsets.get(key);
        List<Object> out = new ArrayList<Object>();
        if (cset != null && cset.get("candidateRefs") instanceof List<?>) {
            for (Object member : (List<?>) cset.get("candidateRefs")) {
                if (intRef(member) != null) {
                    out.add(intRef(member));
                }
            }
        }
        if (cset == null || !"COMPLETE".equals(cset.get("membership"))) {
            out.add(NOT_LISTED);
        }
        return out;
    }

    boolean referenceComplete(Object ref) {
        Long key = intRef(ref);
        Map<?, ?> cset = key == null ? null : graphCsets.get(key);
        return cset != null && "COMPLETE".equals(cset.get("membership"));
    }

    Set<String> sidesOf(Object ref) {
        Set<String> sides = refSide.get(norm(ref));
        return sides == null ? Collections.<String>emptySet() : sides;
    }

    /** The choices of a walk: one alternative per reference, as an immutable sorted map. */
    static final class Sigma {
        static final Sigma EMPTY = new Sigma(new Object[0], new Object[0]);
        final Object[] refs;
        final Object[] alternatives;
        private final int hash;

        private Sigma(Object[] refs, Object[] alternatives) {
            this.refs = refs;
            this.alternatives = alternatives;
            int h = 1;
            for (int i = 0; i < refs.length; i++) {
                h = h * 31 + hash(refs[i]);
                h = h * 31 + (alternatives[i] == NOT_LISTED ? 7 : hash(alternatives[i]));
            }
            this.hash = h;
        }

        boolean isEmpty() {
            return refs.length == 0;
        }

        int indexOf(Object ref) {
            for (int i = 0; i < refs.length; i++) {
                if (same(refs[i], ref)) {
                    return i;
                }
            }
            return -1;
        }

        /** The choices extended by one micro-edge's, or null when the edge takes another alternative. */
        Sigma extend(List<Choice> choices) {
            TreeMap<Object, Object> chosen = null;
            for (Choice choice : choices) {
                boolean has;
                Object current;
                if (chosen != null) {
                    has = chosen.containsKey(choice.ref);
                    current = chosen.get(choice.ref);
                } else {
                    int at = indexOf(choice.ref);
                    has = at >= 0;
                    current = has ? alternatives[at] : null;
                }
                if (has) {
                    if (!sameAlternative(current, choice.alternative)) {
                        return null;
                    }
                    continue;
                }
                if (chosen == null) {
                    chosen = new TreeMap<Object, Object>(REF_ORDER);
                    for (int i = 0; i < refs.length; i++) {
                        chosen.put(refs[i], alternatives[i]);
                    }
                }
                chosen.put(choice.ref, choice.alternative);
            }
            return chosen == null ? this : new Sigma(chosen.keySet().toArray(), chosen.values().toArray());
        }

        @Override
        public boolean equals(Object other) {
            if (!(other instanceof Sigma)) {
                return false;
            }
            Sigma sigma = (Sigma) other;
            if (sigma.hash != hash || sigma.refs.length != refs.length) {
                return false;
            }
            for (int i = 0; i < refs.length; i++) {
                if (!same(refs[i], sigma.refs[i]) || !sameAlternative(alternatives[i], sigma.alternatives[i])) {
                    return false;
                }
            }
            return true;
        }

        @Override
        public int hashCode() {
            return hash;
        }
    }

    static boolean sameAlternative(Object a, Object b) {
        if (a == NOT_LISTED || b == NOT_LISTED) {
            return a == b;
        }
        return same(a, b);
    }

    /**
     * Section 7.1, item 2 ({@code COVERS} of Section 9): the choice sets hold in every world. Splits the worlds on
     * the smallest reference at a time, with an explicit stack.
     */
    boolean covers(Set<Sigma> sigmas) {
        final class Frame {
            final List<Sigma> sets;
            Object ref;
            List<Object> alternatives;
            int next;

            Frame(List<Sigma> sets) {
                this.sets = sets;
            }
        }
        Deque<Frame> stack = new ArrayDeque<Frame>();
        List<Sigma> worlds = new ArrayList<Sigma>();
        for (Sigma sigma : sigmas) {
            worlds.add(decidedSigma(sigma)); // a decided reference holds in its deciding reference's worlds
        }
        stack.push(new Frame(worlds));
        Boolean returned = null;
        long work = 0;
        while (!stack.isEmpty()) {
            Frame frame = stack.peek();
            if (returned != null) {
                if (!returned) {
                    stack.pop();
                    continue;
                }
                returned = null;
            }
            if (frame.alternatives == null) {
                if (++work > maxWorlds) {
                    throw new FoldLimitException("deciding a Fact needs more than " + maxWorlds + " worlds");
                }
                boolean anyEmpty = false;
                Object smallest = null;
                boolean first = true;
                for (Sigma sigma : frame.sets) {
                    if (sigma.isEmpty()) {
                        anyEmpty = true;
                        break;
                    }
                    if (first || REF_ORDER.compare(sigma.refs[0], smallest) < 0) {
                        smallest = sigma.refs[0];
                        first = false;
                    }
                }
                if (anyEmpty || frame.sets.isEmpty()) {
                    returned = anyEmpty;
                    stack.pop();
                    continue;
                }
                frame.ref = smallest;
                frame.alternatives = alternatives(smallest);
            }
            if (frame.next < frame.alternatives.size()) {
                Object alternative = frame.alternatives.get(frame.next++);
                List<Sigma> rest = new ArrayList<Sigma>();
                for (Sigma sigma : frame.sets) {
                    int at = sigma.indexOf(frame.ref);
                    if (at < 0) {
                        rest.add(sigma);
                    } else if (sameAlternative(sigma.alternatives[at], alternative)) {
                        rest.add(without(sigma, at));
                    }
                }
                stack.push(new Frame(rest));
                continue;
            }
            returned = Boolean.TRUE;
            stack.pop();
        }
        return returned != null && returned;
    }

    private static Sigma without(Sigma sigma, int at) {
        Object[] refs = new Object[sigma.refs.length - 1];
        Object[] alternatives = new Object[refs.length];
        for (int i = 0, j = 0; i < sigma.refs.length; i++) {
            if (i != at) {
                refs[j] = sigma.refs[i];
                alternatives[j++] = sigma.alternatives[i];
            }
        }
        return refs.length == 0 ? Sigma.EMPTY : new Sigma(refs, alternatives);
    }

    // ---------------------------------------------------------------------------------------------
    // Section 4.1: micro-edge shapes
    // ---------------------------------------------------------------------------------------------

    /** {@code SEMANTIC_FOLD_MALFORMED_EDGE} for every micro-edge of the document whose shape is not conformant. */
    public List<Finding> malformedEdges() {
        List<Finding> findings = new ArrayList<Finding>();
        for (Map<?, ?> edge : allEdges) {
            String problem = shapeProblem(edge);
            if (problem != null) {
                findings.add(new Finding("SEMANTIC_FOLD_MALFORMED_EDGE", "explainGraph.microEdges ref " + edge.get("ref"),
                        problem));
            }
        }
        return findings;
    }

    String shapeProblem(Map<?, ?> edge) {
        Object source = edge.get("sourceRef");
        Object target = edge.get("targetRef");
        String sourceClass = endClass(source);
        String targetClass = endClass(target);
        Object statement = edge.get("statementRef");
        String problem = null;
        if (sourceClass == null || targetClass == null) {
            problem = "an end is neither field-class nor row-set-class";
        } else if ("VALUE".equals(edge.get("kind")) && ("ROWSET".equals(sourceClass) || "ROWSET".equals(targetClass))) {
            problem = "a VALUE micro-edge touches a row set";
        } else if ("ROW".equals(edge.get("kind")) && "FIELD".equals(sourceClass) && "FIELD".equals(targetClass)
                && "ROW_PROPAGATION".equals(edge.get("role"))) {
            problem = "a field-to-field ROW micro-edge with role ROW_PROPAGATION";
        } else if (terminal(target)) {
            problem = "a micro-edge into a TERMINAL node";
        } else if (graphCset(source) && !(edge.get("sourceBinding") instanceof Map<?, ?>
                && "UNRESOLVED".equals(((Map<?, ?>) edge.get("sourceBinding")).get("status")))) {
            problem = "a micro-edge from a candidate set without an UNRESOLVED source binding";
        } else {
            for (Object end : new Object[] {source, target}) {
                Map<?, ?> node = node(end);
                if (node != null && !same(node.get("statementRef"), statement)) {
                    problem = "an end belongs to another statement";
                }
            }
            for (Choice choice : rawChoices(edge)) {
                if (!(choice.ref instanceof Long) || !graphCsets.containsKey(choice.ref)) {
                    problem = "an ambiguous binding names no candidate set of the graph";
                } else if (choice.alternative != NOT_LISTED && !containsAlternative(members(choice.ref),
                        choice.alternative)) {
                    problem = "an ambiguous binding's edge reads or writes no member of its candidate set";
                } else {
                    Choice decided = decide(choice);
                    if (decided.alternative == UNPAIRED || !(decided.ref instanceof Long)
                            || !graphCsets.containsKey(decided.ref)) {
                        problem = "a decided reference's candidate has no alternative of a deciding set";
                    }
                }
            }
        }
        return problem;
    }

    private static boolean containsAlternative(List<Object> alternatives, Object alternative) {
        for (Object a : alternatives) {
            if (sameAlternative(a, alternative)) {
                return true;
            }
        }
        return false;
    }

    // ---------------------------------------------------------------------------------------------
    // Section 9: exploration
    // ---------------------------------------------------------------------------------------------

    static FoldLabel edgeLabel(Map<?, ?> edge) {
        return FoldLabel.of(edge.get("kind"), edge.get("role"));
    }

    /** Section 7.2, item 1, for one micro-edge; observed is Section 7.3, item 2. */
    static boolean assumed(Map<?, ?> edge, boolean observed) {
        if (observed) {
            return true;
        }
        for (String member : new String[] {"sourceBinding", "targetBinding"}) {
            Object binding = edge.get(member);
            if (binding instanceof Map<?, ?> && ASSUMED.equals(((Map<?, ?>) binding).get("status"))) {
                return true;
            }
        }
        return ASSUMED.equals(edge.get("proofStatus"));
    }

    private static final class State {
        final Object node;
        final FoldLabel label;
        final Sigma sigma;
        final boolean assumed;
        private final int hash;

        State(Object node, FoldLabel label, Sigma sigma, boolean assumed) {
            this.node = norm(node);
            this.label = label;
            this.sigma = sigma;
            this.assumed = assumed;
            this.hash = ((hash(this.node) * 31 + label.hashCode()) * 31 + sigma.hashCode()) * 2 + (assumed ? 1 : 0);
        }

        @Override
        public boolean equals(Object other) {
            if (!(other instanceof State)) {
                return false;
            }
            State state = (State) other;
            return state.hash == hash && state.assumed == assumed && same(node, state.node)
                    && label.equals(state.label) && sigma.equals(state.sigma);
        }

        @Override
        public int hashCode() {
            return hash;
        }
    }

    /** One fold walk, or several with the same first edge, target, label, choices and proof. */
    static final class Walk {
        final Map<?, ?> first;
        final Object source;
        final Object target;
        final FoldLabel label;
        final Sigma sigma;
        final boolean assumed;
        final Set<Long> support = new TreeSet<Long>();
        final List<Map<?, ?>> lastEdges = new ArrayList<Map<?, ?>>();
        /** Fold walks (micro-edge refs in walk order) that together cover {@link #support}. */
        final List<List<Long>> covering = new ArrayList<List<Long>>();

        Walk(Map<?, ?> first, State end) {
            this.first = first;
            this.source = norm(first.get("sourceRef"));
            this.target = end.node;
            this.label = end.label;
            this.sigma = end.sigma;
            this.assumed = end.assumed;
        }
    }

    private static final class Predecessor {
        final State state;
        final Long edge;

        Predecessor(State state, Long edge) {
            this.state = state;
            this.edge = edge;
        }
    }

    /** Every fold walk of a statement, in the order the reference emits them, merged as {@link Walk} says. */
    List<Walk> walks(long statement) {
        List<Map<?, ?>> edges = edgesOf(statement);
        boolean observed = observed(statement);
        Map<Object, List<Map<?, ?>>> out = new HashMap<Object, List<Map<?, ?>>>();
        for (Map<?, ?> edge : edges) {
            Object source = norm(edge.get("sourceRef"));
            List<Map<?, ?>> list = out.get(source);
            if (list == null) {
                list = new ArrayList<Map<?, ?>>();
                out.put(source, list);
            }
            list.add(edge);
        }
        List<Walk> walks = new ArrayList<Walk>();
        long[] states = {0};
        for (Map<?, ?> first : edges) {
            Object source = first.get("sourceRef");
            if (!(kept(source) || graphCset(source))) {
                continue;
            }
            Sigma sigma0 = extend(Sigma.EMPTY, choices(first));
            if (sigma0 == null) {
                continue;
            }
            State x0 = new State(first.get("targetRef"), edgeLabel(first), sigma0, assumed(first, observed));
            count(states, statement);
            Long firstRef = intRef(first.get("ref"));
            LinkedHashMap<State, Walk> emitted = new LinkedHashMap<State, Walk>();
            Map<State, List<State>> befores = new HashMap<State, List<State>>();
            Map<State, List<Predecessor>> pred = new HashMap<State, List<Predecessor>>();
            if (kept(x0.node)) {
                Walk walk = new Walk(first, x0);
                walk.lastEdges.add(first);
                walk.support.add(firstRef);
                walk.covering.add(Collections.singletonList(firstRef));
                emitted.put(x0, walk);
            } else {
                List<Predecessor> start = new ArrayList<Predecessor>(1);
                start.add(new Predecessor(null, firstRef));
                pred.put(x0, start);
                Set<State> visited = new HashSet<State>();
                visited.add(x0);
                ArrayDeque<State> queue = new ArrayDeque<State>();
                queue.add(x0);
                while (!queue.isEmpty()) {
                    State state = queue.poll();
                    List<Map<?, ?>> next = out.get(state.node);
                    if (next == null) {
                        continue;
                    }
                    for (Map<?, ?> edge : next) {
                        Sigma chosen = extend(state.sigma, choices(edge));
                        if (chosen == null) {
                            continue;
                        }
                        State y = new State(edge.get("targetRef"), state.label.compose(edgeLabel(edge)), chosen,
                                state.assumed || assumed(edge, observed));
                        Long edgeRef = intRef(edge.get("ref"));
                        if (kept(y.node)) {
                            Walk walk = emitted.get(y);
                            if (walk == null) {
                                count(states, statement);
                                walk = new Walk(first, y);
                                emitted.put(y, walk);
                                befores.put(y, new ArrayList<State>());
                            }
                            walk.lastEdges.add(edge);
                            walk.support.add(edgeRef);
                            befores.get(y).add(state);
                        } else {
                            List<Predecessor> list = pred.get(y);
                            if (list == null) {
                                list = new ArrayList<Predecessor>(2);
                                pred.put(y, list);
                            }
                            list.add(new Predecessor(state, edgeRef));
                            if (visited.add(y)) {
                                count(states, statement);
                                queue.add(y);
                            }
                        }
                    }
                }
            }
            for (Map.Entry<State, Walk> entry : emitted.entrySet()) {
                Walk walk = entry.getValue();
                List<State> from = befores.get(entry.getKey());
                if (from != null) {
                    // insertion order, so that the covering walks are the same on every JVM
                    Set<State> reaching = new LinkedHashSet<State>(from);
                    Deque<State> stack = new ArrayDeque<State>(from);
                    while (!stack.isEmpty()) {
                        State s = stack.pop();
                        List<Predecessor> list = pred.get(s);
                        if (list == null) {
                            continue;
                        }
                        for (Predecessor p : list) {
                            walk.support.add(p.edge);
                            if (p.state != null && reaching.add(p.state)) {
                                stack.push(p.state);
                            }
                        }
                    }
                    cover(walk, x0, from, reaching, pred);
                }
                walks.add(walk);
            }
        }
        return walks;
    }

    private void count(long[] states, long statement) {
        if (++states[0] > maxStates) {
            throw new FoldLimitException("statement ref " + statement + " needs more than " + maxStates
                    + " exploration states");
        }
    }

    /**
     * Section 8.2, items 3 and 4: fold walks that each yield the record and that together contain every micro-edge
     * of its support subgraph. Each walk is a path of the explored state graph from the first edge to an emission of
     * the record, so it holds in the record's worlds; one walk is added for each micro-edge not yet covered.
     */
    private static void cover(Walk walk, State x0, List<State> befores, Set<State> reaching,
                              Map<State, List<Predecessor>> pred) {
        // the emissions: the state before the last edge, and that edge, in the order they were found
        List<Object[]> emissions = new ArrayList<Object[]>();
        for (int k = 0; k < befores.size(); k++) {
            emissions.add(new Object[] {befores.get(k), intRef(walk.lastEdges.get(k).get("ref"))});
        }
        Map<State, List<Object[]>> successors = new LinkedHashMap<State, List<Object[]>>();
        for (State s : reaching) {
            List<Predecessor> list = pred.get(s);
            if (list == null) {
                continue;
            }
            for (Predecessor p : list) {
                if (p.state != null && reaching.contains(p.state)) {
                    List<Object[]> next = successors.get(p.state);
                    if (next == null) {
                        next = new ArrayList<Object[]>();
                        successors.put(p.state, next);
                    }
                    next.add(new Object[] {s, p.edge});
                }
            }
        }
        Set<Long> uncovered = new TreeSet<Long>(walk.support);
        while (!uncovered.isEmpty()) {
            Long edge = uncovered.iterator().next();
            List<Long> found = null;
            for (Object[] emission : emissions) {
                if (edge.equals(emission[1])) {
                    found = concat(prefix(x0, (State) emission[0], pred, reaching), (Long) emission[1]);
                    break;
                }
            }
            for (Iterator<State> it = reaching.iterator(); found == null && it.hasNext(); ) {
                State s = it.next();
                for (Predecessor p : pred.get(s)) {
                    if (!edge.equals(p.edge)) {
                        continue;
                    }
                    List<Long> head = p.state == null ? new ArrayList<Long>() : prefix(x0, p.state, pred, reaching);
                    head.add(p.edge);
                    found = suffix(head, s, successors, emissions);
                    break;
                }
            }
            if (found == null) {
                throw new IllegalStateException("micro-edge " + edge + " of a support subgraph lies on no walk");
            }
            uncovered.removeAll(found);
            walk.covering.add(Collections.unmodifiableList(found));
        }
    }

    private static List<Long> concat(List<Long> head, Long edge) {
        head.add(edge);
        return head;
    }

    /** The micro-edges of a shortest walk from the first edge to the given state, the first edge included. */
    private static List<Long> prefix(State x0, State to, Map<State, List<Predecessor>> pred, Set<State> reaching) {
        Map<State, Predecessor> parent = new HashMap<State, Predecessor>();
        Deque<State> queue = new ArrayDeque<State>();
        queue.add(to);
        parent.put(to, null);
        State start = null;
        while (!queue.isEmpty()) {
            State s = queue.poll();
            for (Predecessor p : pred.get(s)) {
                if (p.state == null) {
                    start = s;
                    break;
                }
                if (!parent.containsKey(p.state)) {
                    parent.put(p.state, new Predecessor(s, p.edge));
                    queue.add(p.state);
                }
            }
            if (start != null) {
                break;
            }
        }
        // start is x0; follow the parents (each names the state after it and the edge between) back to `to`
        List<Long> out = new ArrayList<Long>();
        out.add(pred.get(start).get(0).edge);
        for (State s = start; parent.get(s) != null; s = parent.get(s).state) {
            out.add(parent.get(s).edge);
        }
        return out;
    }

    /** The walk extended from a state to an emission along the explored successors. */
    private static List<Long> suffix(List<Long> head, State from, Map<State, List<Object[]>> successors,
                                     List<Object[]> emissions) {
        Map<State, Object[]> parent = new HashMap<State, Object[]>();
        Deque<State> queue = new ArrayDeque<State>();
        queue.add(from);
        parent.put(from, null);
        while (!queue.isEmpty()) {
            State s = queue.poll();
            for (Object[] emission : emissions) {
                if (emission[0].equals(s)) {
                    List<Long> tail = new ArrayList<Long>();
                    for (State t = s; parent.get(t) != null; t = (State) parent.get(t)[0]) {
                        tail.add(0, (Long) parent.get(t)[1]);
                    }
                    List<Long> out = new ArrayList<Long>(head);
                    out.addAll(tail);
                    out.add((Long) emission[1]);
                    return out;
                }
            }
            List<Object[]> next = successors.get(s);
            if (next == null) {
                continue;
            }
            for (Object[] step : next) {
                State t = (State) step[0];
                if (!parent.containsKey(t)) {
                    parent.put(t, new Object[] {s, step[1]});
                    queue.add(t);
                }
            }
        }
        return null;
    }

    // ---------------------------------------------------------------------------------------------
    // Section 7.1: Facts and the remainder
    // ---------------------------------------------------------------------------------------------

    private static final class PropositionKey {
        final Object source;
        final Object target;
        final FoldLabel label;

        PropositionKey(Object source, Object target, FoldLabel label) {
            this.source = source;
            this.target = target;
            this.label = label;
        }

        @Override
        public boolean equals(Object other) {
            if (!(other instanceof PropositionKey)) {
                return false;
            }
            PropositionKey key = (PropositionKey) other;
            return same(source, key.source) && same(target, key.target) && label.equals(key.label);
        }

        @Override
        public int hashCode() {
            return (hash(source) * 31 + hash(target)) * 31 + label.hashCode();
        }
    }

    /** One Fact Occurrence before its ordinal is known: (source, target, label, path, offset). */
    private static final class FactKey {
        final PropositionKey proposition;
        final Object path;
        final Long offset;

        FactKey(PropositionKey proposition, Object path, Long offset) {
            this.proposition = proposition;
            this.path = path;
            this.offset = offset;
        }

        @Override
        public boolean equals(Object other) {
            if (!(other instanceof FactKey)) {
                return false;
            }
            FactKey key = (FactKey) other;
            return proposition.equals(key.proposition) && same(path, key.path) && same(offset, key.offset);
        }

        @Override
        public int hashCode() {
            return (proposition.hashCode() * 31 + hash(path)) * 31 + hash(offset);
        }
    }

    private static final class FactEntry {
        boolean proven;
        final Set<Long> support = new TreeSet<Long>();
        final List<Walk> walks = new ArrayList<Walk>();
    }

    static Long offsetOf(Object position) {
        return position instanceof Map<?, ?> ? intRef(((Map<?, ?>) position).get("utf8ByteOffset0")) : null;
    }

    /** Folds one statement (Section 9). */
    public StatementFold fold(long statement) {
        List<Walk> walks = walks(statement);
        LinkedHashMap<PropositionKey, List<Walk>> propositions = new LinkedHashMap<PropositionKey, List<Walk>>();
        for (Walk walk : walks) {
            PropositionKey key = new PropositionKey(walk.source, walk.target, walk.label);
            List<Walk> list = propositions.get(key);
            if (list == null) {
                list = new ArrayList<Walk>();
                propositions.put(key, list);
            }
            list.add(walk);
        }
        LinkedHashMap<FactKey, FactEntry> facts = new LinkedHashMap<FactKey, FactEntry>();
        List<Walk> remainder = new ArrayList<Walk>();
        for (Map.Entry<PropositionKey, List<Walk>> entry : propositions.entrySet()) {
            PropositionKey proposition = entry.getKey();
            Set<Sigma> sigmas = new LinkedHashSet<Sigma>();
            for (Walk walk : entry.getValue()) {
                sigmas.add(walk.sigma);
            }
            if (kept(proposition.source) && covers(sigmas)) {
                for (Walk walk : entry.getValue()) {
                    FactKey key = new FactKey(proposition, walk.first.get("referencePath"),
                            offsetOf(walk.first.get("referenceStart")));
                    FactEntry fact = facts.get(key);
                    if (fact == null) {
                        fact = new FactEntry();
                        facts.put(key, fact);
                    }
                    if (walk.sigma.isEmpty() && !walk.assumed) {
                        fact.proven = true;
                    }
                    fact.support.addAll(walk.support);
                    fact.walks.add(walk);
                }
            } else {
                for (Walk walk : entry.getValue()) {
                    if (!walk.sigma.isEmpty()) {
                        remainder.add(walk);
                    }
                }
            }
        }
        List<StatementFold.FactOccurrence> occurrences = factOccurrences(facts);
        List<StatementFold.Candidate> candidates = candidates(remainder);
        assignCandidateOrdinals(candidates);
        return new StatementFold(statement, occurrences, candidates, writes(statement, occurrences, candidates));
    }

    private static final Comparator<Long> OFFSET_ORDER = new Comparator<Long>() {
        @Override
        public int compare(Long a, Long b) {
            if (a == null || b == null) {
                return a == null ? (b == null ? 0 : 1) : -1;
            }
            return a.compareTo(b);
        }
    };

    private List<StatementFold.FactOccurrence> factOccurrences(LinkedHashMap<FactKey, FactEntry> facts) {
        // Section 8.1: the ordinal ranks the Occurrences of one Fact and path by position, missing positions last.
        LinkedHashMap<List<Object>, List<FactKey>> groups = new LinkedHashMap<List<Object>, List<FactKey>>();
        for (FactKey key : facts.keySet()) {
            List<Object> group = Arrays.<Object>asList(subjectKey(key.proposition.source),
                    subjectKey(key.proposition.target), key.proposition.label, new PathKey(key.path));
            List<FactKey> list = groups.get(group);
            if (list == null) {
                list = new ArrayList<FactKey>();
                groups.put(group, list);
            }
            list.add(key);
        }
        List<StatementFold.FactOccurrence> out = new ArrayList<StatementFold.FactOccurrence>();
        for (List<FactKey> list : groups.values()) {
            Collections.sort(list, new Comparator<FactKey>() {
                @Override
                public int compare(FactKey a, FactKey b) {
                    int c = OFFSET_ORDER.compare(a.offset, b.offset);
                    if (c == 0) {
                        c = REF_ORDER.compare(a.proposition.source, b.proposition.source);
                    }
                    return c != 0 ? c : REF_ORDER.compare(a.proposition.target, b.proposition.target);
                }
            });
            for (int ordinal = 0; ordinal < list.size(); ordinal++) {
                FactKey key = list.get(ordinal);
                FactEntry entry = facts.get(key);
                List<List<Long>> covering = new ArrayList<List<Long>>();
                for (Walk walk : entry.walks) {
                    covering.addAll(walk.covering);
                }
                List<Walk> deciding = decidingWalks(entry);
                List<Map<?, ?>> firsts = new ArrayList<Map<?, ?>>();
                List<Map<?, ?>> lasts = new ArrayList<Map<?, ?>>();
                for (Walk walk : deciding) {
                    firsts.add(walk.first);
                    lasts.addAll(walk.lastEdges);
                }
                out.add(new StatementFold.FactOccurrence(key.proposition.source, key.proposition.target,
                        key.proposition.label, key.path, key.offset, ordinal, entry.proven ? PROVEN : ASSUMED,
                        entry.support, earliestBinding(firsts, "sourceBinding"), earliestBinding(lasts, "targetBinding"),
                        minimalCover(covering, entry.support)));
            }
        }
        Collections.sort(out, new Comparator<StatementFold.FactOccurrence>() {
            @Override
            public int compare(StatementFold.FactOccurrence a, StatementFold.FactOccurrence b) {
                int c = REF_ORDER.compare(a.getSourceRef(), b.getSourceRef());
                if (c == 0) {
                    c = REF_ORDER.compare(a.getTargetRef(), b.getTargetRef());
                }
                if (c == 0) {
                    c = a.getLabel().sortText().compareTo(b.getLabel().sortText());
                }
                if (c == 0) {
                    c = PathKey.ORDER.compare(new PathKey(a.getPath()), new PathKey(b.getPath()));
                }
                return c != 0 ? c : a.getOrdinal() - b.getOrdinal();
            }
        });
        return out;
    }

    /** The walks whose bindings an Occurrence reports: those that decide its proof (Section 7.2, item 2). */
    private static List<Walk> decidingWalks(FactEntry entry) {
        List<Walk> unconditional = new ArrayList<Walk>();
        for (Walk walk : entry.walks) {
            if (walk.sigma.isEmpty() && (!entry.proven || !walk.assumed)) {
                unconditional.add(walk);
            }
        }
        return unconditional.isEmpty() ? entry.walks : unconditional;
    }

    /**
     * The identity an endpoint stands for in an Occurrence subject (identity-v1, Section 5.4): its portable id when
     * it has one, so that two refs of one endpoint rank as one subject; otherwise its ref.
     */
    Object subjectKey(Object ref) {
        Map<?, ?> endpoint = index.get("endpoint", ref);
        Object identity = endpoint == null ? null : endpoint.get("identity");
        if (identity instanceof Map<?, ?> && "PORTABLE".equals(((Map<?, ?>) identity).get("status"))
                && ((Map<?, ?>) identity).get("id") instanceof String) {
            return "id:" + ((Map<?, ?>) identity).get("id");
        }
        return "ref:" + norm(ref);
    }

    /** The walks of a cover, dropping each walk whose edges the others already cover, in order. */
    static List<List<Long>> minimalCover(List<List<Long>> walks, Set<Long> support) {
        List<List<Long>> distinct = new ArrayList<List<Long>>(new LinkedHashSet<List<Long>>(walks));
        Set<Long> covered = new HashSet<Long>();
        List<List<Long>> out = new ArrayList<List<Long>>();
        for (List<Long> walk : distinct) {
            if (!covered.containsAll(walk)) {
                out.add(walk);
                covered.addAll(walk);
            }
        }
        if (!covered.containsAll(support)) {
            throw new IllegalStateException("covering walks miss " + support);
        }
        return out;
    }

    /** A path value with a total order: absent first, then strings in code point order. */
    static final class PathKey {
        static final Comparator<PathKey> ORDER = new Comparator<PathKey>() {
            @Override
            public int compare(PathKey a, PathKey b) {
                if (a.path == null || b.path == null) {
                    return a.path == null ? (b.path == null ? 0 : -1) : 1;
                }
                return compareCodePoints(String.valueOf(a.path), String.valueOf(b.path));
            }
        };
        final Object path;

        PathKey(Object path) {
            this.path = path;
        }

        @Override
        public boolean equals(Object other) {
            return other instanceof PathKey && same(path, ((PathKey) other).path);
        }

        @Override
        public int hashCode() {
            return hash(path);
        }
    }

    /** The position of a reference: its offset (absent last), then its path in code point order. */
    static final class Position implements Comparable<Position> {
        final Long offset;
        final String path;

        Position(Long offset, String path) {
            this.offset = offset;
            this.path = path;
        }

        static Position of(Map<?, ?> edge) {
            Object path = edge.get("referencePath");
            return new Position(offsetOf(edge.get("referenceStart")),
                    path instanceof String && !((String) path).isEmpty() ? (String) path : "");
        }

        @Override
        public int compareTo(Position other) {
            int c = OFFSET_ORDER.compare(offset, other.offset);
            return c != 0 ? c : compareCodePoints(path, other.path);
        }
    }

    /**
     * The binding on the given side of the micro-edge earliest in the text (position, then the canonical JSON of
     * the binding), so that equal inputs give equal bindings whatever their refs.
     */
    static Map<?, ?> earliestBinding(List<Map<?, ?>> edges, String member) {
        Map<?, ?> best = null;
        Position bestPosition = null;
        byte[] bestBytes = null;
        for (Map<?, ?> edge : edges) {
            Object binding = edge.get(member);
            Map<?, ?> map = binding instanceof Map<?, ?> ? (Map<?, ?>) binding : null;
            Position position = Position.of(edge);
            byte[] bytes = map == null ? new byte[0] : CanonicalJson.jcsBytes(map);
            if (bestPosition == null) {
                best = map;
                bestPosition = position;
                bestBytes = bytes;
                continue;
            }
            int c = position.compareTo(bestPosition);
            if (c < 0 || (c == 0 && CanonicalJson.compareUnsigned(bytes, bestBytes) < 0)) {
                best = map;
                bestPosition = position;
                bestBytes = bytes;
            }
        }
        return best;
    }

    // ---------------------------------------------------------------------------------------------
    // Section 7.1, items 4 to 6: FactCandidates
    // ---------------------------------------------------------------------------------------------

    private List<StatementFold.Candidate> candidates(List<Walk> remainder) {
        TreeMap<String, List<Walk>> byLabel = new TreeMap<String, List<Walk>>();
        for (Walk walk : remainder) {
            String key = walk.label.sortText();
            List<Walk> list = byLabel.get(key);
            if (list == null) {
                list = new ArrayList<Walk>();
                byLabel.put(key, list);
            }
            list.add(walk);
        }
        List<StatementFold.Candidate> results = new ArrayList<StatementFold.Candidate>();
        for (List<Walk> group : byLabel.values()) {
            Map<Object, Object> parent = new HashMap<Object, Object>();
            for (Walk walk : group) {
                Object[] refs = walk.sigma.refs;
                for (Object r : refs) {
                    if (!parent.containsKey(r)) {
                        parent.put(r, r);
                    }
                }
                for (int i = 1; i < refs.length; i++) {
                    parent.put(find(parent, refs[i]), find(parent, refs[0]));
                }
            }
            TreeMap<Object, List<Walk>> components = new TreeMap<Object, List<Walk>>(REF_ORDER);
            for (Walk walk : group) {
                Object root = find(parent, walk.sigma.refs[0]);
                List<Walk> list = components.get(root);
                if (list == null) {
                    list = new ArrayList<Walk>();
                    components.put(root, list);
                }
                list.add(walk);
            }
            for (List<Walk> component : components.values()) {
                results.add(candidate(component.get(0).label, component));
            }
        }
        return results;
    }

    private static Object find(Map<Object, Object> parent, Object x) {
        Object current = x;
        while (!same(parent.get(current), current)) {
            current = parent.get(current);
        }
        return current;
    }

    private StatementFold.Candidate candidate(FoldLabel label, List<Walk> walks) {
        // the references of the group as written (sides, deciding reference), and those whose alternatives make the
        // worlds: a decided reference's deciding reference (Section 7.1, items 1 and 5)
        TreeSet<Object> rawSet = new TreeSet<Object>(REF_ORDER);
        TreeSet<Object> refSet = new TreeSet<Object>(REF_ORDER);
        List<Sigma> worldSigmas = new ArrayList<Sigma>();
        for (Walk walk : walks) {
            rawSet.addAll(Arrays.asList(walk.sigma.refs));
            Sigma decided = decidedSigma(walk.sigma);
            worldSigmas.add(decided);
            refSet.addAll(Arrays.asList(decided.refs));
        }
        List<Object> rawRefs = new ArrayList<Object>(rawSet);
        List<Object> refs = new ArrayList<Object>(refSet);
        List<List<Object>> alternatives = new ArrayList<List<Object>>();
        long worlds = 1;
        for (Object r : refs) {
            List<Object> list = alternatives(r);
            alternatives.add(list);
            worlds *= list.size();
            if (worlds > maxWorlds) {
                throw new FoldLimitException("a group of " + refs.size() + " linked references has more than "
                        + maxWorlds + " worlds");
            }
        }
        List<Set<StatementFold.Pair>> outcomes = new ArrayList<Set<StatementFold.Pair>>();
        boolean emptyWorld = false;
        String proof = PROVEN;
        int n = walks.size();
        int[][] at = new int[n][];
        int[][] alt = new int[n][];
        StatementFold.Pair[] pairOf = new StatementFold.Pair[n];
        for (int k = 0; k < n; k++) {
            Sigma sigma = worldSigmas.get(k);
            at[k] = new int[sigma.refs.length];
            alt[k] = new int[sigma.refs.length];
            for (int j = 0; j < sigma.refs.length; j++) {
                at[k][j] = refs.indexOf(sigma.refs[j]);
                alt[k][j] = -1;
                List<Object> options = alternatives.get(at[k][j]);
                for (int a = 0; a < options.size(); a++) {
                    if (sameAlternative(options.get(a), sigma.alternatives[j])) {
                        alt[k][j] = a;
                        break;
                    }
                }
            }
            pairOf[k] = new StatementFold.Pair(walks.get(k).source, walks.get(k).target);
        }
        // an alternative listed twice is one value: compare slots by the first slot holding their value
        int[][] canonical = new int[refs.size()][];
        for (int r = 0; r < refs.size(); r++) {
            List<Object> options = alternatives.get(r);
            canonical[r] = new int[options.size()];
            for (int a = 0; a < options.size(); a++) {
                canonical[r][a] = a;
                for (int b = 0; b < a; b++) {
                    if (sameAlternative(options.get(a), options.get(b))) {
                        canonical[r][a] = b;
                        break;
                    }
                }
            }
        }
        int[] choice = new int[refs.size()];
        // per world of a single deciding reference: its alternative and its pairs (the decision of an end)
        boolean decides = refs.size() == 1 && !rawRefs.equals(refs);
        List<Object> worldAlternative = new ArrayList<Object>();
        List<Set<StatementFold.Pair>> worldPairs = new ArrayList<Set<StatementFold.Pair>>();
        for (long w = 0; w < worlds; w++) {
            Set<StatementFold.Pair> pairs = new LinkedHashSet<StatementFold.Pair>();
            Set<StatementFold.Pair> proven = new HashSet<StatementFold.Pair>();
            for (int k = 0; k < n; k++) {
                boolean holds = true;
                for (int j = 0; j < at[k].length && holds; j++) {
                    holds = alt[k][j] >= 0 && canonical[at[k][j]][choice[at[k][j]]] == alt[k][j];
                }
                if (holds) {
                    pairs.add(pairOf[k]);
                    if (!walks.get(k).assumed) {
                        proven.add(pairOf[k]);
                    }
                }
            }
            if (!proven.containsAll(pairs)) {
                proof = ASSUMED;
            }
            if (pairs.isEmpty()) {
                emptyWorld = true;
            } else {
                outcomes.add(pairs);
            }
            if (decides) {
                worldAlternative.add(alternatives.get(0).get(choice[0]));
                worldPairs.add(pairs);
            }
            for (int i = refs.size() - 1; i >= 0; i--) {
                if (++choice[i] < alternatives.get(i).size()) {
                    break;
                }
                choice[i] = 0;
            }
        }
        boolean unresolved = false;
        TreeSet<Object> sourceSet = new TreeSet<Object>(REF_ORDER);
        TreeSet<Object> targetSet = new TreeSet<Object>(REF_ORDER);
        for (Walk walk : walks) {
            if (graphCset(walk.source)) {
                unresolved = true;
            } else {
                sourceSet.add(walk.source);
            }
            targetSet.add(walk.target);
        }
        List<Object> sources = new ArrayList<Object>(sourceSet);
        List<Object> targets = new ArrayList<Object>(targetSet);
        Set<String> sides = new HashSet<String>();
        boolean complete = !emptyWorld && !unresolved;
        for (Object r : rawRefs) {
            sides.addAll(sidesOf(r));
            complete &= referenceComplete(r);
        }
        for (Object r : refs) {
            complete &= referenceComplete(r);
        }
        StatementFold.End targetEnd = !sides.contains(TARGET) && targets.size() == 1
                ? StatementFold.End.fixed(targets.get(0))
                : StatementFold.End.set(targets, complete && targets.size() >= 2 ? "COMPLETE" : "INCOMPLETE",
                decides ? decision(refs.get(0), targets, false, worldAlternative, worldPairs) : null);
        StatementFold.End sourceEnd = !targetEnd.isFixed() && !sides.contains(SOURCE) && sources.size() == 1 && !unresolved
                ? StatementFold.End.fixed(sources.get(0))
                : StatementFold.End.set(sources, complete && sources.size() >= 2 ? "COMPLETE" : "INCOMPLETE",
                decides ? decision(refs.get(0), sources, true, worldAlternative, worldPairs) : null);
        Set<Set<StatementFold.Pair>> effective = new LinkedHashSet<Set<StatementFold.Pair>>();
        for (Set<StatementFold.Pair> outcome : outcomes) {
            Set<StatementFold.Pair> kept = new LinkedHashSet<StatementFold.Pair>();
            for (StatementFold.Pair pair : outcome) {
                if (!graphCset(pair.getSource())) {
                    kept.add(pair);
                }
            }
            if (!kept.isEmpty()) {
                effective.add(kept);
            }
        }
        Set<Set<StatementFold.Pair>> implied = impliedOutcomes(sourceEnd, targetEnd);
        Object deciding = null;
        Position decidingPosition = null;
        for (Object r : rawRefs) {
            Position position = refPosition.get(r);
            if (position == null) {
                position = new Position(null, "");
            }
            if (decidingPosition == null || position.compareTo(decidingPosition) < 0) {
                deciding = r;
                decidingPosition = position;
            }
        }
        Set<Long> support = new TreeSet<Long>();
        for (Walk walk : walks) {
            support.addAll(walk.support);
        }
        Position known = refPosition.get(deciding);
        Object path = known == null || known.path.isEmpty() ? null : known.path;
        List<List<Long>> covering = new ArrayList<List<Long>>();
        for (Walk walk : walks) {
            covering.addAll(walk.covering);
        }
        StatementFold.Candidate result = new StatementFold.Candidate(label, rawRefs, sourceEnd, targetEnd,
                effective.equals(implied) ? null : effective, effective.isEmpty() ? implied : effective, proof, support,
                path, known == null ? null : known.offset, minimalCover(covering, support));
        result.sourceBinding = candidateBinding(SOURCE, sourceEnd, rawRefs, walks, support);
        result.targetBinding = candidateBinding(TARGET, targetEnd, rawRefs, walks, support);
        return result;
    }

    /**
     * Section 7.1, item 5: the decision of a candidate-set end whose group's worlds are those of one deciding reference:
     * each member is paired with the one alternative in whose world it is an end of a pair; null when a member is one in
     * several worlds or none, or an alternative would be paired twice (then the end is not decided).
     */
    private StatementFold.Decision decision(Object deciding, List<Object> members, boolean source,
            List<Object> worldAlternative, List<Set<StatementFold.Pair>> worldPairs) {
        if (members.isEmpty()) {
            return null;
        }
        List<StatementFold.Pair> alignment = new ArrayList<StatementFold.Pair>();
        List<Object> used = new ArrayList<Object>();
        for (Object member : members) {
            Object found = null;
            int count = 0;
            for (int w = 0; w < worldPairs.size(); w++) {
                if (worldAlternative.get(w) == NOT_LISTED) {
                    continue;
                }
                for (StatementFold.Pair pair : worldPairs.get(w)) {
                    if (same(source ? pair.getSource() : pair.getTarget(), member)) {
                        found = worldAlternative.get(w);
                        count++;
                        break;
                    }
                }
            }
            if (count != 1 || containsAlternative(used, found)) {
                return null;
            }
            used.add(found);
            alignment.add(new StatementFold.Pair(found, member));
        }
        Map<?, ?> cset = graphCsets.get(intRef(deciding));
        return new StatementFold.Decision(deciding, members(deciding), cset == null ? null : cset.get("membership"),
                alignment);
    }

    static Set<Set<StatementFold.Pair>> impliedOutcomes(StatementFold.End source, StatementFold.End target) {
        List<Object> sources = source.isFixed() ? Collections.singletonList(source.getEndpointRef()) : source.getMembers();
        List<Object> targets = target.isFixed() ? Collections.singletonList(target.getEndpointRef()) : target.getMembers();
        Set<Set<StatementFold.Pair>> out = new LinkedHashSet<Set<StatementFold.Pair>>();
        for (Object s : sources) {
            for (Object t : targets) {
                out.add(Collections.singleton(new StatementFold.Pair(s, t)));
            }
        }
        return out;
    }

    /** Section 7.1, item 6. */
    private StatementFold.CandidateBinding candidateBinding(String side, StatementFold.End end, List<Object> refs,
                                                            List<Walk> walks, Set<Long> support) {
        String member = SOURCE.equals(side) ? "sourceBinding" : "targetBinding";
        if (!end.isFixed()) {
            Object deciding = null;
            Position decidingPosition = null;
            for (Object r : refs) {
                if (!sidesOf(r).contains(side)) {
                    continue;
                }
                Position position = refPosition.get(r);
                if (position == null) {
                    position = new Position(null, "");
                }
                if (decidingPosition == null || position.compareTo(decidingPosition) < 0) {
                    deciding = r;
                    decidingPosition = position;
                }
            }
            if (decidingPosition != null) {
                List<Map<?, ?>> edges = new ArrayList<Map<?, ?>>();
                for (Long ref : support) {
                    Map<?, ?> edge = index.get("microEdge", ref);
                    Object binding = edge == null ? null : edge.get(member);
                    if (ambiguous(binding) && same(((Map<?, ?>) binding).get("candidateSetRef"), deciding)) {
                        edges.add(edge);
                    }
                }
                if (!edges.isEmpty()) {
                    return new StatementFold.CandidateBinding(earliestBinding(edges, member), true);
                }
            }
        }
        List<Map<?, ?>> edges = new ArrayList<Map<?, ?>>();
        for (Walk walk : walks) {
            if (SOURCE.equals(side)) {
                edges.add(walk.first);
            } else {
                edges.addAll(walk.lastEdges);
            }
        }
        return new StatementFold.CandidateBinding(earliestBinding(edges, member), false);
    }

    /** identity-v1, Section 5.4: the rank among FactCandidates of the same subject and path, by position. */
    private void assignCandidateOrdinals(List<StatementFold.Candidate> candidates) {
        LinkedHashMap<List<Object>, List<StatementFold.Candidate>> groups =
                new LinkedHashMap<List<Object>, List<StatementFold.Candidate>>();
        for (StatementFold.Candidate candidate : candidates) {
            List<Object> subject = Arrays.<Object>asList(candidate.getLabel(), endKey(candidate.getSource()),
                    endKey(candidate.getTarget()), new PathKey(candidate.getPath()));
            List<StatementFold.Candidate> list = groups.get(subject);
            if (list == null) {
                list = new ArrayList<StatementFold.Candidate>();
                groups.put(subject, list);
            }
            list.add(candidate);
        }
        for (List<StatementFold.Candidate> list : groups.values()) {
            List<StatementFold.Candidate> sorted = new ArrayList<StatementFold.Candidate>(list);
            Collections.sort(sorted, new Comparator<StatementFold.Candidate>() {
                @Override
                public int compare(StatementFold.Candidate a, StatementFold.Candidate b) {
                    int c = OFFSET_ORDER.compare(a.getOffset(), b.getOffset());
                    if (c != 0) {
                        return c;
                    }
                    List<Object> x = a.getReferences();
                    List<Object> y = b.getReferences();
                    for (int i = 0; i < Math.min(x.size(), y.size()); i++) {
                        c = REF_ORDER.compare(x.get(i), y.get(i));
                        if (c != 0) {
                            return c;
                        }
                    }
                    return x.size() - y.size();
                }
            });
            for (int i = 0; i < sorted.size(); i++) {
                sorted.get(i).ordinal = i;
            }
        }
    }

    /** A FactCandidate side as identity-v1 frames it: one endpoint identity, or a membership and sorted identities. */
    private List<Object> endKey(StatementFold.End end) {
        if (end.isFixed()) {
            return Arrays.<Object>asList("ENDPOINT", subjectKey(end.getEndpointRef()));
        }
        TreeSet<String> members = new TreeSet<String>();
        for (Object member : end.getMembers()) {
            members.add(String.valueOf(subjectKey(member)));
        }
        return Arrays.<Object>asList("CANDIDATE_SET", end.getMembership(), new ArrayList<String>(members));
    }

    // ---------------------------------------------------------------------------------------------
    // Sections 7.4 and 7.5: what each write needs
    // ---------------------------------------------------------------------------------------------

    /** The micro-edges of one statement by source. */
    Map<Object, List<Map<?, ?>>> outOf(long statement) {
        Map<Object, List<Map<?, ?>>> out = new LinkedHashMap<Object, List<Map<?, ?>>>();
        for (Map<?, ?> edge : edgesOf(statement)) {
            Object source = norm(edge.get("sourceRef"));
            List<Map<?, ?>> list = out.get(source);
            if (list == null) {
                list = new ArrayList<Map<?, ?>>();
                out.put(source, list);
            }
            list.add(edge);
        }
        return out;
    }

    /**
     * The kept nodes a node reaches (fold-v1, Section 1): along walks, so a sequence that takes two alternatives of
     * one reference does not count (Section 7.1, item 1), through folded interior nodes; VALUE micro-edges only when
     * asked.
     */
    Set<Object> reachFrom(Map<Object, List<Map<?, ?>>> out, Object start, boolean valueOnly, long statement) {
        Set<Object> reached = new TreeSet<Object>(REF_ORDER);
        Set<List<Object>> seen = new HashSet<List<Object>>();
        Deque<Object[]> stack = new ArrayDeque<Object[]>();
        stack.push(new Object[] {norm(start), Sigma.EMPTY});
        long[] states = {0};
        while (!stack.isEmpty()) {
            Object[] state = stack.pop();
            List<Map<?, ?>> next = out.get(state[0]);
            if (next == null) {
                continue;
            }
            for (Map<?, ?> edge : next) {
                if (valueOnly && !"VALUE".equals(edge.get("kind"))) {
                    continue;
                }
                Sigma chosen = extend((Sigma) state[1], choices(edge));
                if (chosen == null) {
                    continue;
                }
                Object target = norm(edge.get("targetRef"));
                if (kept(target)) {
                    reached.add(target);
                } else if (folded(target) && seen.add(Arrays.<Object>asList(target, chosen))) {
                    count(states, statement);
                    stack.push(new Object[] {target, chosen});
                }
            }
        }
        return reached;
    }

    /**
     * Section 7.4: for each kept node that an UNKNOWN_INPUT terminal or a folded node whose upstreamCompleteness is
     * not COMPLETE reaches, the lowest such completeness and the diagnostics of those nodes.
     */
    Map<Object, Object[]> lowering(long statement, Map<Object, List<Map<?, ?>>> out) {
        Map<Object, Object[]> lowered = new HashMap<Object, Object[]>();
        for (Object source : out.keySet()) {
            Map<?, ?> node = node(source);
            Object completeness;
            if (terminal(source) && "UNKNOWN_INPUT".equals(node.get("inputKind"))) {
                completeness = "PARTIAL";
            } else if (folded(source) && node.containsKey("upstreamCompleteness")
                    && !"COMPLETE".equals(node.get("upstreamCompleteness"))) {
                completeness = node.get("upstreamCompleteness");
            } else {
                continue;
            }
            for (Object target : reachFrom(out, source, false, statement)) {
                Object[] entry = lowered.get(target);
                if (entry == null) {
                    entry = new Object[] {"COMPLETE", new TreeSet<Long>()};
                    lowered.put(target, entry);
                }
                entry[0] = lower((String) entry[0], completeness);
                @SuppressWarnings("unchecked")
                Set<Long> diagnostics = (Set<Long>) entry[1];
                addRefs(diagnostics, node.get("diagnosticRefs"));
            }
        }
        return lowered;
    }

    /** Section 7.5: the kept fields each terminal of the statement reaches through VALUE micro-edges, as inputs. */
    Map<Object, Set<StatementFold.TerminalInput>> terminalInputs(long statement, Map<Object, List<Map<?, ?>>> out) {
        Map<Object, Set<StatementFold.TerminalInput>> inputs =
                new TreeMap<Object, Set<StatementFold.TerminalInput>>(REF_ORDER);
        for (Map<?, ?> node : index.all("node")) {
            if ("TERMINAL".equals(node.get("kind")) && same(node.get("statementRef"), statement)) {
                for (Object target : reachFrom(out, node.get("ref"), true, statement)) {
                    if (isField(target)) {
                        Set<StatementFold.TerminalInput> set = inputs.get(target);
                        if (set == null) {
                            set = new LinkedHashSet<StatementFold.TerminalInput>();
                            inputs.put(target, set);
                        }
                        set.add(terminalInput(node.get("inputKind"), node));
                    }
                }
            }
        }
        return inputs;
    }

    /** A terminal input as Section 7.5 compares it; two REDACTED literals of one write are indistinguishable. */
    static StatementFold.TerminalInput terminalInput(Object kind, Map<?, ?> obj) {
        Object disclosure = obj.get("disclosure");
        Object value = "PRESENT".equals(disclosure) ? obj.get("literal")
                : "HASHED".equals(disclosure) ? CanonicalJson.jcsText(obj.get("token")) : null;
        boolean parameter = "PARAMETER".equals(kind);
        return new StatementFold.TerminalInput(kind, disclosure, value, parameter ? obj.get("parameterText") : null,
                parameter ? obj.get("parameterOrdinal") : null);
    }

    static String lower(String bound, Object completeness) {
        Integer rank = completeness instanceof String ? RANK.get(completeness) : null;
        return rank != null && rank < RANK.get(bound) ? (String) completeness : bound;
    }

    static int rank(Object completeness) {
        Integer rank = completeness instanceof String ? RANK.get(completeness) : null;
        return rank == null ? 0 : rank;
    }

    /** The written fields of a statement: those a micro-edge enters, and the targets of its write records. */
    Set<Object> writtenFields(long statement) {
        TreeSet<Object> out = new TreeSet<Object>(REF_ORDER);
        for (Map<?, ?> edge : edgesOf(statement)) {
            if (isField(edge.get("targetRef"))) {
                out.add(norm(edge.get("targetRef")));
            }
        }
        for (Map<?, ?> write : index.all("tfo")) {
            if (same(write.get("statementRef"), statement) && isField(write.get("targetRef"))) {
                out.add(norm(write.get("targetRef")));
            }
        }
        return out;
    }

    private List<StatementFold.WriteRequirement> writes(long statement, List<StatementFold.FactOccurrence> facts,
                                                        List<StatementFold.Candidate> candidates) {
        boolean observed = observed(statement);
        Map<Object, List<Map<?, ?>>> out = outOf(statement);
        Map<Object, Set<StatementFold.TerminalInput>> terminals = terminalInputs(statement, out);
        Map<Object, Object[]> lowered = lowering(statement, out);
        TreeSet<Object> targets = new TreeSet<Object>(REF_ORDER);
        targets.addAll(writtenFields(statement));
        targets.addAll(terminals.keySet());
        List<StatementFold.WriteRequirement> requirements = new ArrayList<StatementFold.WriteRequirement>();
        for (Object target : targets) {
            String bound = observed ? "PARTIAL" : "COMPLETE";
            Set<Long> diagnostics = new TreeSet<Long>();
            List<StatementFold.FactOccurrence> inputs = new ArrayList<StatementFold.FactOccurrence>();
            Set<PropositionKey> seen = new HashSet<PropositionKey>();
            for (StatementFold.FactOccurrence fact : facts) {
                if (same(fact.getTargetRef(), target)
                        && seen.add(new PropositionKey(fact.getSourceRef(), fact.getTargetRef(), fact.getLabel()))) {
                    inputs.add(fact);
                }
            }
            List<StatementFold.Candidate> candidateInputs = new ArrayList<StatementFold.Candidate>();
            for (StatementFold.Candidate candidate : candidates) {
                StatementFold.End end = candidate.getTarget();
                boolean reaches = end.isFixed() ? same(end.getEndpointRef(), target) : containsRef(end.getMembers(), target);
                if (reaches) {
                    candidateInputs.add(candidate);
                    bound = lower(bound, "PARTIAL");
                }
            }
            if (enteredByChoice(statement, target)) {
                bound = lower(bound, "PARTIAL"); // written only in some worlds (Section 7.4)
            }
            Object[] lowering = lowered.get(target);
            if (lowering != null) {
                bound = lower(bound, lowering[0]);
                @SuppressWarnings("unchecked")
                Set<Long> lowering1 = (Set<Long>) lowering[1];
                diagnostics.addAll(lowering1);
            }
            Set<StatementFold.TerminalInput> inputsOfKind = terminals.get(target);
            requirements.add(new StatementFold.WriteRequirement(target, bound, inputs, candidateInputs,
                    inputsOfKind == null ? Collections.<StatementFold.TerminalInput>emptySet() : inputsOfKind,
                    diagnostics));
        }
        return requirements;
    }

    /**
     * Section 7.4: whether every micro-edge of the statement that enters the target has a CANDIDATE or UNRESOLVED
     * target-side binding: the statement writes it only when one of those references denotes it.
     */
    boolean enteredByChoice(long statement, Object target) {
        boolean entered = false;
        for (Map<?, ?> edge : edgesOf(statement)) {
            if (same(edge.get("targetRef"), target)) {
                if (!ambiguous(edge.get("targetBinding"))) {
                    return false;
                }
                entered = true;
            }
        }
        return entered;
    }

    static boolean containsRef(List<Object> refs, Object ref) {
        for (Object r : refs) {
            if (same(r, ref)) {
                return true;
            }
        }
        return false;
    }

    static void addRefs(Set<Long> out, Object refs) {
        if (refs instanceof List<?>) {
            for (Object r : (List<?>) refs) {
                if (intRef(r) != null) {
                    out.add(intRef(r));
                }
            }
        }
    }
}