repositories / termux-janitor
termux-janitor
Interactive cleanup assistant for Termux: transparent, safe, confirmed disk reclamation.
owned by admin
tools/spec-engine/src/status.zig
Raw//! 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);
}