const std = @import("std");
const profile = @import("profile");

/// Verification lanes are a profile-owned fact.
pub const Suite = profile.Suite;

pub const file_size_max = 1024 * 1024;
pub const document_count_max = 64;
pub const concept_count_max = 256;
pub const requirement_count_max = 512;
pub const group_count_max = 64;
pub const test_spec_count_max = 512;
pub const test_binding_count_max = 512;
pub const verification_count_max = 1024;
pub const implementation_count_max = 256;

comptime {
    std.debug.assert(document_count_max <= concept_count_max);
    std.debug.assert(concept_count_max <= requirement_count_max);
    std.debug.assert(group_count_max <= document_count_max);
}

/// The relationship graph. It carries no product-domain registry.
pub const Graph = struct {
    documents: []const Document,
    concepts: []const Concept,
    groups: []const RequirementGroup,
    test_specs: []const TestSpec,
    test_bindings: []const TestBinding,
    verification: []const VerificationObligation,
    implementations: []const ImplementationUnit,

    pub fn load(allocator: std.mem.Allocator, io: std.Io) !Graph {
        return .{
            .documents = try parseFile(
                []const Document,
                allocator,
                io,
                profile.paths.documents,
            ),
            .concepts = try parseFile(
                []const Concept,
                allocator,
                io,
                profile.paths.concepts,
            ),
            .groups = try parseFile(
                []const RequirementGroup,
                allocator,
                io,
                profile.paths.requirements,
            ),
            .test_specs = try parseFile(
                []const TestSpec,
                allocator,
                io,
                profile.paths.test_specs,
            ),
            .test_bindings = try parseFile(
                []const TestBinding,
                allocator,
                io,
                profile.paths.test_bindings,
            ),
            .verification = try parseFile(
                []const VerificationObligation,
                allocator,
                io,
                profile.paths.verification,
            ),
            .implementations = try parseFile(
                []const ImplementationUnit,
                allocator,
                io,
                profile.paths.implementations,
            ),
        };
    }

    pub fn requirementCount(graph: *const Graph) u32 {
        var count: u32 = 0;
        for (graph.groups) |group| {
            count = std.math.add(u32, count, @intCast(group.requirements.len)) catch unreachable;
        }
        return count;
    }
};

pub const Document = struct {
    name: []const u8,
    description: []const u8,
    location: []const u8,
};

pub const Concept = struct {
    id: []const u8,
    term: []const u8,
    definition: []const u8,
    owner: []const u8,
    invariants: []const []const u8,
    aliases: []const []const u8,
    non_equivalent: []const []const u8,
    requirements: []const []const u8,
};

pub const TestSpec = struct {
    id: []const u8,
    revision: u32,
    suite: Suite,
    fixture: FixtureReference,
    claims: []const VerificationClaim,
    production_boundary: ProductionBoundary,
};

pub const VerificationClaim = struct {
    oracle: []const u8,
    kind: VerificationKind,
    obligations: []const ObligationReference,
};

pub const RequirementReference = struct {
    id: []const u8,
    revision: u32,
};

pub const FixtureReference = struct {
    id: []const u8,
    revision: u32,
    path: []const u8,
    sha256: []const u8,
};

pub const ProductionBoundary = enum {
    process,
    state_transition,
};

pub const TestBinding = struct {
    test_spec: TestSpecReference,
    fixture_revision: u32,
    source: []const u8,
    source_sha256: []const u8,
    module: []const u8,
};

pub const TestSpecReference = struct {
    id: []const u8,
    revision: u32,
};

pub const VerificationObligation = struct {
    id: []const u8,
    revision: u32,
    requirement: RequirementReference,
    kind: VerificationKind,
    label: []const u8,
    suites: []const Suite,
};

pub const VerificationKind = enum {
    required,
    forbidden,
};

pub const ObligationReference = struct {
    id: []const u8,
    revision: u32,
};

pub const ImplementationUnit = struct {
    id: []const u8,
    revision: u32,
    sources: []const SourceReference,
    realizes: []const ObligationReference,
};

pub const SourceReference = struct {
    path: []const u8,
    sha256: []const u8,
};

pub const RequirementGroup = struct {
    title: []const u8,
    requirements: []const Requirement,
};

pub const Requirement = struct {
    id: []const u8,
    revision: u32,
    status: RequirementStatus,
    label: []const u8,
    owner: []const u8,
    suites: []const Suite,
    invariant_status: InvariantMappingStatus = .unassessed,
    platform_evidence_status: PlatformEvidenceStatus = .unassessed,
    platform_evidence_references: []const []const u8 = &.{},
    limitation_status: LimitationStatus,
    limitation_references: []const []const u8 = &.{},
};

pub const RequirementStatus = enum {
    accepted,
};

pub const InvariantMappingStatus = enum {
    unassessed,
    mapped,
};

pub const PlatformEvidenceStatus = enum {
    unassessed,
    not_required,
    required_missing,
    recorded,
};

pub const LimitationStatus = enum {
    unassessed,
    none,
    recorded,
};

pub fn parseFile(
    comptime Result: type,
    allocator: std.mem.Allocator,
    io: std.Io,
    path: []const u8,
) !Result {
    const bytes = try std.Io.Dir.cwd().readFileAlloc(
        io,
        path,
        allocator,
        .limited(file_size_max),
    );
    const source = try allocator.dupeZ(u8, bytes);
    return std.zon.parse.fromSliceAlloc(
        Result,
        allocator,
        source,
        null,
        .{ .ignore_unknown_fields = false, .free_on_error = true },
    );
}

test "registered bounds are ordered" {
    try std.testing.expect(group_count_max <= document_count_max);
    try std.testing.expect(document_count_max <= concept_count_max);
    try std.testing.expect(concept_count_max <= requirement_count_max);
}

test "ZON parsing rejects malformed and unknown fields" {
    const Sample = struct { name: []const u8 };
    var arena = std.heap.ArenaAllocator.init(std.testing.allocator);
    defer arena.deinit();
    const allocator = arena.allocator();
    const valid = try std.zon.parse.fromSliceAlloc(
        Sample,
        allocator,
        ".{ .name = \"value\" }",
        null,
        .{ .ignore_unknown_fields = false, .free_on_error = true },
    );
    try std.testing.expectEqualStrings("value", valid.name);

    try std.testing.expectError(error.ParseZon, std.zon.parse.fromSliceAlloc(
        Sample,
        allocator,
        ".{ .name = \"value\", .unknown = true }",
        null,
        .{ .ignore_unknown_fields = false, .free_on_error = true },
    ));
    try std.testing.expectError(error.ParseZon, std.zon.parse.fromSliceAlloc(
        Sample,
        allocator,
        ".{ .name = ",
        null,
        .{ .ignore_unknown_fields = false, .free_on_error = true },
    ));
}
pub fn requirementHasSuite(
    requirement: *const Requirement,
    suite: Suite,
) bool {
    for (requirement.suites) |required| {
        if (profile.suiteMatches(required, suite)) return true;
    }
    return false;
}

pub fn findObligation(
    obligations: []const VerificationObligation,
    id: []const u8,
) ?VerificationObligation {
    for (obligations) |obligation| {
        if (std.mem.eql(u8, obligation.id, id)) return obligation;
    }
    return null;
}

pub fn testSuite(comptime index: usize) Suite {
    return profile.concrete_suites[index];
}

pub fn suiteListContains(suites: []const Suite, expected: Suite) bool {
    for (suites) |suite| if (suite == expected) return true;
    return false;
}

pub fn findRequirement(
    groups: []const RequirementGroup,
    id: []const u8,
) ?Requirement {
    for (groups) |group| {
        for (group.requirements) |requirement| {
            if (std.mem.eql(u8, requirement.id, id)) return requirement;
        }
    }
    return null;
}

pub fn findTestSpec(
    test_specs: []const TestSpec,
    id: []const u8,
) ?TestSpec {
    for (test_specs) |test_spec| if (std.mem.eql(u8, test_spec.id, id)) return test_spec;
    return null;
}

pub fn findTestBinding(
    bindings: []const TestBinding,
    test_spec_id: []const u8,
) ?TestBinding {
    for (bindings) |binding| {
        if (std.mem.eql(u8, binding.test_spec.id, test_spec_id)) return binding;
    }
    return null;
}