const std = @import("std");
const model_types = @import("model.zig");
const diag = @import("diag.zig");
const fail = diag.fail;
const on = diag.subject;
const text = @import("text.zig");
const profile = @import("profile");
pub const output_size_max = 2 * 1024 * 1024;
const marker_begin = "";
const marker_end = "";
comptime {
std.debug.assert(model_types.file_size_max < output_size_max);
}
pub fn checkDerived(
allocator: std.mem.Allocator,
io: std.Io,
model: *const model_types.Graph,
stderr: *std.Io.Writer,
) !void {
var catalog = std.Io.Writer.Allocating.init(allocator);
defer catalog.deinit();
try renderCatalog(model.documents, &catalog.writer);
const expected_agents = try agentsWithCatalog(allocator, io, catalog.written());
try checkFileEqual(allocator, io, profile.paths.agents, expected_agents, stderr);
var requirements = std.Io.Writer.Allocating.init(allocator);
defer requirements.deinit();
try renderRequirements(model, &requirements.writer);
try checkFileEqual(
allocator,
io,
profile.paths.requirements_index,
requirements.written(),
stderr,
);
var glossary = std.Io.Writer.Allocating.init(allocator);
defer glossary.deinit();
try renderGlossary(model.concepts, &glossary.writer);
try checkFileEqual(allocator, io, profile.paths.glossary, glossary.written(), stderr);
}
pub fn runGenerate(
allocator: std.mem.Allocator,
io: std.Io,
model: *const model_types.Graph,
args: []const []const u8,
stderr: *std.Io.Writer,
) !void {
if (args.len > 1) return error.UnexpectedArgument;
_ = stderr;
const target = if (args.len == 1) args[0] else "all";
const agents = std.mem.eql(u8, target, "agents") or std.mem.eql(u8, target, "all");
const requirements = std.mem.eql(u8, target, "requirements") or
std.mem.eql(u8, target, "all");
const glossary = std.mem.eql(u8, target, "glossary") or std.mem.eql(u8, target, "all");
if (!agents and !requirements and !glossary) return error.UnknownGenerationTarget;
if (agents) try generateAgents(allocator, io, model);
if (requirements) try generateRequirements(allocator, io, model);
if (glossary) try generateGlossary(allocator, io, model);
}
pub fn generateAgents(
allocator: std.mem.Allocator,
io: std.Io,
model: *const model_types.Graph,
) !void {
var catalog = std.Io.Writer.Allocating.init(allocator);
defer catalog.deinit();
try renderCatalog(model.documents, &catalog.writer);
const output = try agentsWithCatalog(allocator, io, catalog.written());
try replaceFile(io, profile.paths.agents, profile.paths.agents ++ ".spec-tool.tmp", output);
}
pub fn generateRequirements(
allocator: std.mem.Allocator,
io: std.Io,
model: *const model_types.Graph,
) !void {
var output = std.Io.Writer.Allocating.init(allocator);
defer output.deinit();
try renderRequirements(model, &output.writer);
try replaceFile(
io,
profile.paths.requirements_index,
profile.paths.requirements_index ++ ".spec-tool.tmp",
output.written(),
);
}
pub fn generateGlossary(
allocator: std.mem.Allocator,
io: std.Io,
model: *const model_types.Graph,
) !void {
var output = std.Io.Writer.Allocating.init(allocator);
defer output.deinit();
try renderGlossary(model.concepts, &output.writer);
try replaceFile(
io,
profile.paths.glossary,
profile.paths.glossary ++ ".spec-tool.tmp",
output.written(),
);
}
pub fn renderCatalog(documents: []const model_types.Document, writer: *std.Io.Writer) !void {
try writer.writeAll("\n");
for (documents) |document| {
try writer.writeAll(" \n ");
try text.writeXmlEscaped(writer, document.name, false);
try writer.writeAll("\n");
try text.writeXmlWrappedDescription(writer, document.description);
try writer.writeAll(" ");
try text.writeXmlEscaped(writer, document.location, false);
try writer.writeAll("\n \n");
}
try writer.writeAll("\n");
}
pub fn renderGlossary(concepts: []const model_types.Concept, writer: *std.Io.Writer) !void {
try writer.writeAll(profile.projections.glossary_preamble);
try writer.writeByte('\n');
for (concepts) |concept| {
try writer.print("## {s}\n\n**ID:** `{s}`\n\n", .{ concept.term, concept.id });
try text.writeWrapped(writer, concept.definition, "", "", 100);
try writer.writeAll("\n\n**Invariants**\n\n");
for (concept.invariants) |invariant| {
try text.writeWrapped(writer, invariant, "- ", " ", 100);
try writer.writeByte('\n');
}
try writer.writeAll("\n**Aliases:** ");
try text.renderInlineList(concept.aliases, writer);
try writer.writeAll(".\n\n**Non-equivalent concepts:** ");
try text.renderInlineCodeList(concept.non_equivalent, writer);
try writer.writeAll(".\n\n**Requirements:** ");
try text.renderInlineCodeList(concept.requirements, writer);
try writer.writeAll(".\n\n");
}
}
pub fn renderRequirements(model: *const model_types.Graph, writer: *std.Io.Writer) !void {
try writer.writeAll(profile.projections.requirements_preamble);
try writer.writeByte('\n');
for (model.groups) |group| {
try writer.print("## {s}\n\n", .{group.title});
for (group.requirements) |requirement| {
try writer.print(
"- **{s}@{d}**, {s}.\n Owner: [source]({s}).\n Suites: ",
.{
requirement.id,
requirement.revision,
requirement.label,
profile.requirementOwnerLink(requirement.owner),
},
);
try renderSuites(requirement.suites, writer);
try writer.print(
".\n Invariant mapping: {s}.\n Platform evidence: {s}.\n Platform evidence references: ",
.{
@tagName(requirement.invariant_status),
@tagName(requirement.platform_evidence_status),
},
);
try text.renderInlineCodeList(requirement.platform_evidence_references, writer);
try writer.print(".\n Limitation status: {s}.\n Limitation references: ", .{
@tagName(requirement.limitation_status),
});
try text.renderInlineCodeList(requirement.limitation_references, writer);
try writer.writeAll(".\n Registered obligations: ");
try renderRequirementObligations(model.verification, requirement.id, writer);
try writer.writeByte('.');
try writer.writeByte('\n');
}
try writer.writeByte('\n');
}
try writer.writeAll(
\\## Maintenance rule
\\
\\Every normative addition changes the canonical model in the same integration change.
\\A requirement is removed only when its owner text, model record, tests, and references are
\\removed together. Splitting or merging requirements preserves old identifiers as aliases
\\for one release unless doing so would create a safety ambiguity.
\\
);
}
fn renderRequirementObligations(
obligations: []const model_types.VerificationObligation,
requirement_id: []const u8,
writer: *std.Io.Writer,
) !void {
var found = false;
for (obligations) |obligation| {
if (!std.mem.eql(u8, obligation.requirement.id, requirement_id)) continue;
if (found) try writer.writeAll(", ");
try writer.print("`{s}`", .{obligation.id});
found = true;
}
if (!found) try writer.writeAll("none");
}
pub fn renderSuites(suites: []const model_types.Suite, writer: *std.Io.Writer) !void {
for (suites, 0..) |suite, index| {
if (index > 0) try writer.writeAll(", ");
const name = @tagName(suite);
if (!profile.suiteIsConcrete(suite)) {
try writer.writeAll(name);
} else {
for (name) |byte| try writer.writeByte(std.ascii.toUpper(byte));
}
}
}
pub fn agentsWithCatalog(
allocator: std.mem.Allocator,
io: std.Io,
catalog: []const u8,
) ![]const u8 {
const source = try std.Io.Dir.cwd().readFileAlloc(
io,
profile.paths.agents,
allocator,
.limited(model_types.file_size_max),
);
return replaceMarkedRegion(allocator, source, catalog);
}
pub fn replaceMarkedRegion(
allocator: std.mem.Allocator,
source: []const u8,
replacement: []const u8,
) ![]const u8 {
return replaceNamedRegion(allocator, source, marker_begin, marker_end, replacement);
}
/// Replace one uniquely named generated region while preserving all surrounding bytes.
pub fn replaceNamedRegion(
allocator: std.mem.Allocator,
source: []const u8,
begin_marker: []const u8,
end_marker: []const u8,
replacement: []const u8,
) ![]const u8 {
if (begin_marker.len == 0) return error.EmptyBeginMarker;
if (end_marker.len == 0) return error.EmptyEndMarker;
const begin = std.mem.indexOf(u8, source, begin_marker) orelse return error.MissingBeginMarker;
const content_start = begin + begin_marker.len;
if (std.mem.indexOfPos(u8, source, content_start, begin_marker) != null) {
return error.DuplicateBeginMarker;
}
const end = std.mem.indexOfPos(u8, source, content_start, end_marker) orelse
return error.MissingEndMarker;
if (std.mem.indexOfPos(u8, source, end + end_marker.len, end_marker) != null) {
return error.DuplicateEndMarker;
}
if (content_start >= source.len or source[content_start] != '\n') {
return error.InvalidMarkerLayout;
}
var output = std.Io.Writer.Allocating.init(allocator);
errdefer output.deinit();
try output.writer.writeAll(source[0 .. content_start + 1]);
try output.writer.writeAll(replacement);
try output.writer.writeAll(source[end..]);
if (output.written().len > output_size_max) return error.OutputTooLarge;
return output.toOwnedSlice();
}
pub fn checkFileEqual(
allocator: std.mem.Allocator,
io: std.Io,
path: []const u8,
expected: []const u8,
stderr: *std.Io.Writer,
) !void {
const actual = try std.Io.Dir.cwd().readFileAlloc(
io,
path,
allocator,
.limited(output_size_max),
);
defer allocator.free(actual);
if (!std.mem.eql(u8, actual, expected)) {
return fail(stderr, on.projection, "generated projection is stale: {s}", .{path});
}
}
pub fn replaceFile(io: std.Io, path: []const u8, temporary: []const u8, data: []const u8) !void {
if (data.len > output_size_max) return error.OutputTooLarge;
const cwd = std.Io.Dir.cwd();
cwd.writeFile(io, .{ .sub_path = temporary, .data = data }) catch |err| return err;
errdefer cwd.deleteFile(io, temporary) catch {};
try cwd.rename(temporary, cwd, path, io);
}
test "marked replacement preserves handwritten bytes" {
const source = "before\n" ++ marker_begin ++ "\nold\n" ++ marker_end ++ "\nafter\n";
const expected = "before\n" ++ marker_begin ++ "\nnew\n" ++ marker_end ++ "\nafter\n";
const actual = try replaceMarkedRegion(std.testing.allocator, source, "new\n");
defer std.testing.allocator.free(actual);
try std.testing.expectEqualStrings(expected, actual);
}
test "marked replacement rejects malformed markers" {
const duplicate = marker_begin ++ "\n" ++ marker_begin ++ "\n" ++ marker_end;
try std.testing.expectError(
error.DuplicateBeginMarker,
replaceMarkedRegion(std.testing.allocator, duplicate, "new\n"),
);
try std.testing.expectError(
error.MissingEndMarker,
replaceMarkedRegion(std.testing.allocator, marker_begin ++ "\n", "new\n"),
);
try std.testing.expectError(
error.MissingBeginMarker,
replaceMarkedRegion(std.testing.allocator, marker_end, "new\n"),
);
}
test "catalog rendering is deterministic and escaped" {
const documents = [_]model_types.Document{.{
.name = "test-document",
.description = "Use for & checks.",
.location = "spec/TESTING.md",
}};
var output = std.Io.Writer.Allocating.init(std.testing.allocator);
defer output.deinit();
try renderCatalog(&documents, &output.writer);
try std.testing.expectEqualStrings(
"\n" ++
" \n" ++
" test-document\n" ++
" \n" ++
" Use for <tests> & checks.\n" ++
" \n" ++
" spec/TESTING.md\n" ++
" \n" ++
"\n",
output.written(),
);
}