//! Aggregate verification state.
//!
//! Status reports what is verified, what is merely specified, and what carries
//! no verification at all. It states evidence; it never claims that evidence is
//! sufficient.
const std = @import("std");
const model_types = @import("model.zig");

/// Derived lifecycle of one verification obligation.
pub const State = enum {
    /// No test specification claims this obligation.
    unclaimed,
    /// Claimed by a test specification whose fixture has no executable binding.
    specified,
    /// Claimed and bound, so a generated test executes it.
    executable,
};

pub const ObligationStatus = struct {
    id: []const u8,
    revision: u32,
    requirement: []const u8,
    kind: model_types.VerificationKind,
    state: State,
    realized: bool,
};

pub const RequirementState = enum {
    done,
    partial,
    missing,
};

pub const RequirementProgress = struct {
    id: []const u8,
    revision: u32,
    label: []const u8,
    state: RequirementState,
    obligations: u32,
    executable: u32,
    unrealized: u32,
};

pub const Summary = struct {
    requirements: u32,
    requirements_with_obligations: u32,
    done: u32,
    partial: u32,
    missing: u32,
    obligations: u32,
    unclaimed: u32,
    specified: u32,
    executable: u32,
    unrealized: u32,
};

pub fn obligationStatus(
    graph: *const model_types.Graph,
    obligation: *const model_types.VerificationObligation,
) ObligationStatus {
    var state: State = .unclaimed;
    for (graph.test_specs) |test_spec| {
        if (!claims(&test_spec, obligation.id)) continue;
        state = .specified;
        if (model_types.findTestBinding(graph.test_bindings, test_spec.id) != null) {
            state = .executable;
            break;
        }
    }
    return .{
        .id = obligation.id,
        .revision = obligation.revision,
        .requirement = obligation.requirement.id,
        .kind = obligation.kind,
        .state = state,
        .realized = realized(graph, obligation.id),
    };
}

pub fn requirementProgress(
    graph: *const model_types.Graph,
    requirement: *const model_types.Requirement,
) RequirementProgress {
    var progress: RequirementProgress = .{
        .id = requirement.id,
        .revision = requirement.revision,
        .label = requirement.label,
        .state = .missing,
        .obligations = 0,
        .executable = 0,
        .unrealized = 0,
    };
    var has_unclaimed = false;
    for (graph.verification) |obligation| {
        if (!std.mem.eql(u8, obligation.requirement.id, requirement.id)) continue;
        progress.obligations += 1;
        const status = obligationStatus(graph, &obligation);
        if (status.state == .executable) progress.executable += 1;
        if (status.state == .unclaimed) has_unclaimed = true;
        if (!status.realized) progress.unrealized += 1;
    }
    if (progress.obligations == 0 or has_unclaimed) return progress;
    if (progress.executable == progress.obligations) {
        progress.state = .done;
    } else {
        progress.state = .partial;
    }
    return progress;
}

pub fn summarize(graph: *const model_types.Graph) Summary {
    var result: Summary = .{
        .requirements = graph.requirementCount(),
        .requirements_with_obligations = 0,
        .done = 0,
        .partial = 0,
        .missing = 0,
        .obligations = @intCast(graph.verification.len),
        .unclaimed = 0,
        .specified = 0,
        .executable = 0,
        .unrealized = 0,
    };
    for (graph.groups) |group| {
        for (group.requirements) |requirement| {
            const progress = requirementProgress(graph, &requirement);
            if (progress.obligations > 0) result.requirements_with_obligations += 1;
            switch (progress.state) {
                .done => result.done += 1,
                .partial => result.partial += 1,
                .missing => result.missing += 1,
            }
        }
    }
    for (graph.verification) |obligation| {
        const status = obligationStatus(graph, &obligation);
        switch (status.state) {
            .unclaimed => result.unclaimed += 1,
            .specified => result.specified += 1,
            .executable => result.executable += 1,
        }
        if (!status.realized) result.unrealized += 1;
    }
    return result;
}

fn nextRequirement(graph: *const model_types.Graph) ?RequirementProgress {
    for (graph.groups) |group| {
        for (group.requirements) |requirement| {
            const progress = requirementProgress(graph, &requirement);
            if (progress.state != .done) return progress;
        }
    }
    return null;
}

/// Report verification state for the whole graph, or for one requirement.
pub fn report(
    graph: *const model_types.Graph,
    filter: ?[]const u8,
    json: bool,
    writer: *std.Io.Writer,
) !void {
    if (filter) |id| {
        if (model_types.findRequirement(graph.groups, id) == null) return error.RequirementNotFound;
    }
    if (json) return reportJson(graph, filter, writer);

    const summary = summarize(graph);
    if (filter == null) {
        try writer.print(
            "requirements: {d} total, {d} with an obligation, {d} with none\n",
            .{
                summary.requirements,
                summary.requirements_with_obligations,
                summary.requirements - summary.requirements_with_obligations,
            },
        );
        try writer.print(
            "obligations:  {d} total, {d} executable, {d} specified, {d} unclaimed, " ++
                "{d} unrealized\n",
            .{
                summary.obligations,
                summary.executable,
                summary.specified,
                summary.unclaimed,
                summary.unrealized,
            },
        );
        try writer.print("progress:    {d} done, {d} partial, {d} missing\n", .{
            summary.done,
            summary.partial,
            summary.missing,
        });
        if (nextRequirement(graph)) |next| {
            try writer.print("next:        {s}@{d}: {s}\n\n", .{
                next.id,
                next.revision,
                next.label,
            });
        } else {
            try writer.writeAll("next:        none\n\n");
        }
    }
    for (graph.groups) |group| {
        for (group.requirements) |requirement| {
            if (filter) |id| {
                if (!std.mem.eql(u8, id, requirement.id)) continue;
            }
            if (filter == null and !hasObligation(graph, requirement.id)) continue;
            const progress = requirementProgress(graph, &requirement);
            try writer.print("{s}@{d}: {s}\nprogress: {s}\n", .{
                requirement.id,
                requirement.revision,
                requirement.label,
                @tagName(progress.state),
            });
            for (graph.verification) |obligation| {
                if (!std.mem.eql(u8, obligation.requirement.id, requirement.id)) continue;
                const status = obligationStatus(graph, &obligation);
                try writer.print("  {s:<12} {s:<10} {s}\n", .{
                    @tagName(status.state),
                    if (status.realized) "realized" else "unrealized",
                    obligation.id,
                });
            }
        }
    }
    if (filter == null and summary.requirements_with_obligations < summary.requirements) {
        try writer.writeAll("\nrequirements without any verification obligation:\n");
        for (graph.groups) |group| {
            for (group.requirements) |requirement| {
                if (hasObligation(graph, requirement.id)) continue;
                try writer.print("  {s}@{d}: {s}\n", .{
                    requirement.id,
                    requirement.revision,
                    requirement.label,
                });
            }
        }
    }
}

fn reportJson(
    graph: *const model_types.Graph,
    filter: ?[]const u8,
    writer: *std.Io.Writer,
) !void {
    const summary = summarize(graph);
    try writer.print("{{\"summary\":{f},\"next\":", .{std.json.fmt(summary, .{})});
    if (filter == null) {
        if (nextRequirement(graph)) |next| {
            try writer.print("{f}", .{std.json.fmt(next, .{})});
        } else {
            try writer.writeAll("null");
        }
    } else {
        try writer.writeAll("null");
    }
    try writer.writeAll(",\"requirements\":[");
    var requirements_written: u32 = 0;
    for (graph.groups) |group| {
        for (group.requirements) |requirement| {
            if (filter) |id| {
                if (!std.mem.eql(u8, id, requirement.id)) continue;
            }
            if (requirements_written > 0) try writer.writeByte(',');
            const progress = requirementProgress(graph, &requirement);
            try writer.print("{f}", .{std.json.fmt(progress, .{})});
            requirements_written += 1;
        }
    }
    try writer.writeAll("],\"obligations\":[");
    var obligations_written: u32 = 0;
    for (graph.verification) |obligation| {
        if (filter) |id| {
            if (!std.mem.eql(u8, obligation.requirement.id, id)) continue;
        }
        if (obligations_written > 0) try writer.writeByte(',');
        const status = obligationStatus(graph, &obligation);
        try writer.print("{f}", .{std.json.fmt(status, .{})});
        obligations_written += 1;
    }
    try writer.writeAll("]}\n");
}

fn claims(test_spec: *const model_types.TestSpec, obligation_id: []const u8) bool {
    for (test_spec.claims) |claim| {
        for (claim.obligations) |reference| {
            if (std.mem.eql(u8, reference.id, obligation_id)) return true;
        }
    }
    return false;
}

fn realized(graph: *const model_types.Graph, obligation_id: []const u8) bool {
    for (graph.implementations) |unit| {
        for (unit.realizes) |reference| {
            if (std.mem.eql(u8, reference.id, obligation_id)) return true;
        }
    }
    return false;
}

fn hasObligation(graph: *const model_types.Graph, requirement_id: []const u8) bool {
    for (graph.verification) |obligation| {
        if (std.mem.eql(u8, obligation.requirement.id, requirement_id)) return true;
    }
    return false;
}

test "status distinguishes unclaimed, specified, and executable evidence" {
    const obligations = [_]model_types.VerificationObligation{
        .{
            .id = "obligation-alpha",
            .revision = 1,
            .requirement = .{ .id = "REQ-EXAMPLE-01", .revision = 1 },
            .kind = .required,
            .label = "Alpha.",
            .suites = &.{model_types.testSuite(0)},
        },
        .{
            .id = "obligation-beta",
            .revision = 1,
            .requirement = .{ .id = "REQ-EXAMPLE-01", .revision = 1 },
            .kind = .forbidden,
            .label = "Beta.",
            .suites = &.{model_types.testSuite(0)},
        },
        .{
            .id = "obligation-gamma",
            .revision = 1,
            .requirement = .{ .id = "REQ-EXAMPLE-02", .revision = 1 },
            .kind = .required,
            .label = "Gamma.",
            .suites = &.{model_types.testSuite(0)},
        },
    };
    const claim_set = [_]model_types.VerificationClaim{
        .{
            .oracle = "INV-ALPHA",
            .kind = .required,
            .obligations = &.{.{ .id = "obligation-alpha", .revision = 1 }},
        },
        .{
            .oracle = "NO-BETA",
            .kind = .forbidden,
            .obligations = &.{.{ .id = "obligation-beta", .revision = 1 }},
        },
    };
    const test_specs = [_]model_types.TestSpec{.{
        .id = "test-example",
        .revision = 1,
        .suite = model_types.testSuite(0),
        .fixture = .{
            .id = "fixture-example",
            .revision = 1,
            .path = "fixtures/example.md",
            .sha256 = "0000000000000000000000000000000000000000000000000000000000000000",
        },
        .claims = &claim_set,
        .production_boundary = .process,
    }};
    const implementations = [_]model_types.ImplementationUnit{.{
        .id = "implementation-example",
        .revision = 1,
        .sources = &.{.{
            .path = "sources/example.zig",
            .sha256 = "0000000000000000000000000000000000000000000000000000000000000000",
        }},
        .realizes = &.{.{ .id = "obligation-alpha", .revision = 1 }},
    }};
    const graph: model_types.Graph = .{
        .documents = &.{},
        .concepts = &.{},
        .groups = &.{},
        .test_specs = &test_specs,
        .test_bindings = &.{},
        .verification = &obligations,
        .implementations = &implementations,
    };
    try std.testing.expectEqual(State.specified, obligationStatus(&graph, &obligations[0]).state);
    try std.testing.expect(obligationStatus(&graph, &obligations[0]).realized);
    try std.testing.expectEqual(State.unclaimed, obligationStatus(&graph, &obligations[2]).state);
    try std.testing.expect(!obligationStatus(&graph, &obligations[2]).realized);

    const bindings = [_]model_types.TestBinding{.{
        .test_spec = .{ .id = "test-example", .revision = 1 },
        .fixture_revision = 1,
        .source = "bindings/example.zig",
        .source_sha256 = "0000000000000000000000000000000000000000000000000000000000000000",
        .module = "fixture_example",
    }};
    var bound = graph;
    bound.test_bindings = &bindings;
    try std.testing.expectEqual(State.executable, obligationStatus(&bound, &obligations[0]).state);

    const summary = summarize(&bound);
    try std.testing.expectEqual(@as(u32, 3), summary.obligations);
    try std.testing.expectEqual(@as(u32, 2), summary.executable);
    try std.testing.expectEqual(@as(u32, 1), summary.unclaimed);
    try std.testing.expectEqual(@as(u32, 2), summary.unrealized);
}

test "requirement progress derives done, partial, and missing states" {
    const requirements = [_]model_types.Requirement{
        .{
            .id = "REQ-EXAMPLE-01",
            .revision = 1,
            .status = .accepted,
            .label = "Done.",
            .owner = "spec/example.md",
            .suites = &.{model_types.testSuite(0)},
            .limitation_status = .unassessed,
        },
        .{
            .id = "REQ-EXAMPLE-02",
            .revision = 1,
            .status = .accepted,
            .label = "Partial.",
            .owner = "spec/example.md",
            .suites = &.{model_types.testSuite(0)},
            .limitation_status = .unassessed,
        },
        .{
            .id = "REQ-EXAMPLE-03",
            .revision = 1,
            .status = .accepted,
            .label = "Missing.",
            .owner = "spec/example.md",
            .suites = &.{model_types.testSuite(0)},
            .limitation_status = .unassessed,
        },
    };
    const groups = [_]model_types.RequirementGroup{.{
        .title = "Examples",
        .requirements = &requirements,
    }};
    const obligations = [_]model_types.VerificationObligation{
        .{
            .id = "obligation-done",
            .revision = 1,
            .requirement = .{ .id = "REQ-EXAMPLE-01", .revision = 1 },
            .kind = .required,
            .label = "Done.",
            .suites = &.{model_types.testSuite(0)},
        },
        .{
            .id = "obligation-partial",
            .revision = 1,
            .requirement = .{ .id = "REQ-EXAMPLE-02", .revision = 1 },
            .kind = .required,
            .label = "Partial.",
            .suites = &.{model_types.testSuite(0)},
        },
    };
    const done_claim = [_]model_types.VerificationClaim{.{
        .oracle = "INV-DONE",
        .kind = .required,
        .obligations = &.{.{ .id = "obligation-done", .revision = 1 }},
    }};
    const partial_claim = [_]model_types.VerificationClaim{.{
        .oracle = "INV-PARTIAL",
        .kind = .required,
        .obligations = &.{.{ .id = "obligation-partial", .revision = 1 }},
    }};
    const specs = [_]model_types.TestSpec{
        .{
            .id = "test-done",
            .revision = 1,
            .suite = model_types.testSuite(0),
            .fixture = .{
                .id = "fixture-done",
                .revision = 1,
                .path = "fixtures/done.md",
                .sha256 = "0000000000000000000000000000000000000000000000000000000000000000",
            },
            .claims = &done_claim,
            .production_boundary = .process,
        },
        .{
            .id = "test-partial",
            .revision = 1,
            .suite = model_types.testSuite(0),
            .fixture = .{
                .id = "fixture-partial",
                .revision = 1,
                .path = "fixtures/partial.md",
                .sha256 = "0000000000000000000000000000000000000000000000000000000000000000",
            },
            .claims = &partial_claim,
            .production_boundary = .process,
        },
    };
    const bindings = [_]model_types.TestBinding{.{
        .test_spec = .{ .id = "test-done", .revision = 1 },
        .fixture_revision = 1,
        .source = "fixtures/done.zig",
        .source_sha256 = "0000000000000000000000000000000000000000000000000000000000000000",
        .module = "fixture_done",
    }};
    const graph: model_types.Graph = .{
        .documents = &.{},
        .concepts = &.{},
        .groups = &groups,
        .test_specs = &specs,
        .test_bindings = &bindings,
        .verification = &obligations,
        .implementations = &.{},
    };
    try std.testing.expectEqual(.done, requirementProgress(&graph, &requirements[0]).state);
    try std.testing.expectEqual(.partial, requirementProgress(&graph, &requirements[1]).state);
    try std.testing.expectEqual(.missing, requirementProgress(&graph, &requirements[2]).state);
    const summary = summarize(&graph);
    try std.testing.expectEqual(@as(u32, 1), summary.done);
    try std.testing.expectEqual(@as(u32, 1), summary.partial);
    try std.testing.expectEqual(@as(u32, 1), summary.missing);
}