Luigit
repositories / termux-janitor

termux-janitor

Interactive cleanup assistant for Termux: transparent, safe, confirmed disk reclamation.

owned by admin

tools/spec-engine/src/scaffold.zig

Raw
//! Generators for new and unfinished verification work.
//!
//! Scaffolds are disposable authoring material written to standard output only.
//! They never mutate a registry, never claim coverage, and never pass a gate.
const std = @import("std");
const model_types = @import("model.zig");
const text = @import("text.zig");
const profile = @import("profile");

const tool = profile.tool_invocation;

/// Render every registry delta required to introduce one new verified scenario.
///
/// The output is a complete, ordered authoring plan: prose fixture, verification
/// obligations, test specification, executable binding, and the commands that
/// finish and verify the work.
pub const NewTestOptions = struct {
    /// Explicit fixture path. Defaults to `<fixture root><name>.md`.
    fixture_path: ?[]const u8 = null,
    /// Write the fixture file when it does not exist yet.
    write_fixture: bool = false,
};

pub fn newTest(
    graph: *const model_types.Graph,
    name: []const u8,
    requirement_id: []const u8,
    suite_name: []const u8,
    options: NewTestOptions,
    io: ?std.Io,
    writer: *std.Io.Writer,
) !void {
    if (!text.nameValid(name)) return error.InvalidScaffoldName;
    const requirement = model_types.findRequirement(graph.groups, requirement_id) orelse
        return error.RequirementNotFound;
    const suite = std.meta.stringToEnum(model_types.Suite, suite_name) orelse
        return error.UnknownSuite;
    if (!profile.suiteIsConcrete(suite)) return error.SuiteMustBeConcrete;
    if (!model_types.requirementHasSuite(&requirement, suite)) return error.SuiteNotRequired;

    var upper_buffer: [128]u8 = undefined;
    const upper = try upperName(&upper_buffer, name);
    var symbol_buffer: [128]u8 = undefined;
    const symbol = try lowerSymbol(&symbol_buffer, name);
    var default_path_buffer: [256]u8 = undefined;
    const fixture_file = try fixturePath(&default_path_buffer, name, options.fixture_path);

    try writer.print(
        \\Authoring plan for a new verified scenario.
        \\
        \\name:        {s}
        \\requirement: {s}@{d}
        \\suite:       {s}
        \\
        \\Nothing below has been written. Apply the steps in order.
        \\
        \\
    , .{ name, requirement.id, requirement.revision, @tagName(suite) });

    try writer.print(
        \\Step 1. Create the prose fixture at {s}
        \\
        \\----------------------------------------------------------------------
        \\
    , .{fixture_file});
    try renderFixtureProse(name, upper, writer);
    try writer.writeAll(
        "----------------------------------------------------------------------\n\n",
    );

    try writer.print(
        \\Step 2. Append two verification obligations to {s}
        \\
        \\----------------------------------------------------------------------
        \\    .{{
        \\        .id = "obligation-{s}-holds",
        \\        .revision = 1,
        \\        .requirement = .{{ .id = "{s}", .revision = {d} }},
        \\        .kind = .required,
        \\        .label = "STATE THE REQUIRED OBSERVATION.",
        \\        .suites = .{{.{s}}},
        \\    }},
        \\    .{{
        \\        .id = "obligation-{s}-forbids",
        \\        .revision = 1,
        \\        .requirement = .{{ .id = "{s}", .revision = {d} }},
        \\        .kind = .forbidden,
        \\        .label = "STATE THE FORBIDDEN EFFECT.",
        \\        .suites = .{{.{s}}},
        \\    }},
        \\----------------------------------------------------------------------
        \\
        \\
    , .{
        profile.paths.verification,
        name,
        requirement.id,
        requirement.revision,
        @tagName(suite),
        name,
        requirement.id,
        requirement.revision,
        @tagName(suite),
    });

    try writer.print(
        \\Step 3. Append the test specification to {s}
        \\
        \\----------------------------------------------------------------------
        \\    .{{
        \\        .id = "test-{s}",
        \\        .revision = 1,
        \\        .suite = .{s},
        \\        .fixture = .{{
        \\            .id = "fixture-{s}",
        \\            .revision = 1,
        \\            .path = "{s}",
        \\            .sha256 = "OBTAIN WITH THE COMMAND IN STEP 5",
        \\        }},
        \\        .claims = .{{
        \\            .{{
        \\                .oracle = "INV-{s}",
        \\                .kind = .required,
        \\                .obligations = .{{
        \\                    .{{ .id = "obligation-{s}-holds", .revision = 1 }},
        \\                }},
        \\            }},
        \\            .{{
        \\                .oracle = "NO-{s}",
        \\                .kind = .forbidden,
        \\                .obligations = .{{
        \\                    .{{ .id = "obligation-{s}-forbids", .revision = 1 }},
        \\                }},
        \\            }},
        \\        }},
        \\        .production_boundary = .process,
        \\    }},
        \\----------------------------------------------------------------------
        \\
        \\
    , .{
        profile.paths.test_specs,
        name,
        @tagName(suite),
        name,
        fixture_file,
        upper,
        name,
        upper,
        name,
    });

    try writer.print(
        \\Step 4. Only when the fixture carries instrumentation, append the binding to {s}
        \\
        \\----------------------------------------------------------------------
        \\    .{{
        \\        .test_spec = .{{ .id = "test-{s}", .revision = 1 }},
        \\        .fixture_revision = 1,
        \\        .source = "{s}{s}.zig",
        \\        .source_sha256 = "OBTAIN WITH THE COMMAND IN STEP 5",
        \\        .module = "fixture_{s}",
        \\    }},
        \\----------------------------------------------------------------------
        \\
        \\A prose fixture without an instrumentation fence is a valid specified
        \\test and takes no binding.
        \\
        \\
    , .{
        profile.paths.test_bindings,
        name,
        profile.paths.binding_inventory_root ++ "/",
        symbol,
        symbol,
    });

    if (options.write_fixture) {
        const handle = io orelse return error.FixtureWriteUnavailable;
        try writeFixtureFile(handle, fixture_file, name, upper);
        try writer.print("Wrote {s}. Nothing else was written.\n\n", .{fixture_file});
    }

    try writer.print(
        \\Step 5. Finish and verify
        \\
        \\  {s} scaffold-test test-{s}
        \\  {s} fingerprint {s}
        \\  {s} fingerprint {s}{s}.zig
        \\  {s} impact {s}
        \\  {s}
        \\
        \\Every gate reports its own owner, inspection commands, and resolution.
        \\
    , .{
        tool,
        name,
        tool,
        fixture_file,
        tool,
        profile.paths.binding_inventory_root ++ "/",
        symbol,
        tool,
        requirement.id,
        profile.verify_command,
    });
}

fn fixturePath(buffer: []u8, name: []const u8, explicit: ?[]const u8) ![]const u8 {
    if (explicit) |value| {
        if (!std.mem.startsWith(u8, value, profile.paths.fixture_root)) {
            return error.FixtureOutsideFixtureRoot;
        }
        if (!std.mem.endsWith(u8, value, ".md")) return error.FixtureIsNotMarkdown;
        return value;
    }
    return std.fmt.bufPrint(buffer, "{s}{s}.md", .{ profile.paths.fixture_root, name }) catch
        error.ScaffoldNameTooLong;
}

fn writeFixtureFile(io: std.Io, path: []const u8, name: []const u8, upper: []const u8) !void {
    const cwd = std.Io.Dir.cwd();
    if (cwd.access(io, path, .{})) |_| {
        return error.FixtureAlreadyExists;
    } else |_| {}
    var buffer: [8192]u8 = undefined;
    var prose = std.Io.Writer.fixed(&buffer);
    try renderFixtureProse(name, upper, &prose);
    try cwd.writeFile(io, .{ .sub_path = path, .data = prose.buffered() });
}

fn renderFixtureProse(name: []const u8, upper: []const u8, writer: *std.Io.Writer) !void {
    var symbol_buffer: [128]u8 = undefined;
    const symbol = try lowerSymbol(&symbol_buffer, name);
    try writer.print(
        \\# TITLE THIS SCENARIO
        \\
        \\**Fixture:** `fixture-{s}@1`
        \\
        \\## Given
        \\
        \\STATE THE INITIAL CONDITIONS.
        \\
        \\## When
        \\
        \\STATE THE SINGLE STIMULUS.
        \\
        \\## Required invariants
        \\
        \\- **`INV-{s}`:** STATE THE REQUIRED OBSERVATION.
        \\
        \\## Forbidden effects
        \\
        \\- **`NO-{s}`:** STATE THE FORBIDDEN EFFECT.
        \\
        \\## Instrumentation
        \\
        \\```zig tj-test
        \\try fixture.given_SOMETHING();
        \\try fixture.when_SOMETHING();
        \\try fixture.then_inv_{s}();
        \\try fixture.forbid_no_{s}();
        \\```
        \\
        \\## Variations
        \\
        \\STATE RELATED SCENARIOS OWNED ELSEWHERE.
        \\
        \\## Limitations
        \\
        \\STATE WHAT THIS FIXTURE CANNOT OBSERVE.
        \\
    , .{ name, upper, upper, symbol, symbol });
}

fn upperName(buffer: []u8, name: []const u8) ![]const u8 {
    if (name.len > buffer.len) return error.ScaffoldNameTooLong;
    for (name, 0..) |byte, index| buffer[index] = std.ascii.toUpper(byte);
    return buffer[0..name.len];
}

/// Fixture methods use underscore symbols derived from the hyphenated name.
fn lowerSymbol(buffer: []u8, name: []const u8) ![]const u8 {
    if (name.len > buffer.len) return error.ScaffoldNameTooLong;
    for (name, 0..) |byte, index| buffer[index] = if (byte == '-') '_' else byte;
    return buffer[0..name.len];
}

/// Render a disposable fixture implementation that cannot pass unfinished.
pub fn renderFixtureScaffold(
    test_spec: *const model_types.TestSpec,
    writer: *std.Io.Writer,
) !void {
    try writer.print("// Authoring scaffold for {s}@{d}.\n", .{
        test_spec.id,
        test_spec.revision,
    });
    try writer.print("// Read {s}.\n", .{test_spec.fixture.path});
    try writer.writeAll("pub const Fixture = struct {\n");
    try writer.writeAll("    pub fn init() !Fixture { return .{}; }\n");
    try writer.writeAll("    pub fn deinit(fixture: *Fixture) void { _ = fixture; }\n");
    try writer.writeAll(
        "};\ncomptime {\n" ++
            "    @compileError(\"Complete this fixture before tracking it.\");\n" ++
            "}\n",
    );
}

pub fn scaffoldTest(
    graph: *const model_types.Graph,
    id: []const u8,
    writer: *std.Io.Writer,
) !void {
    const test_spec = model_types.findTestSpec(graph.test_specs, id) orelse
        return error.TestSpecNotFound;
    try renderFixtureScaffold(&test_spec, writer);
}

test "the authoring plan names every registry it touches" {
    const requirements = [_]model_types.Requirement{.{
        .id = "REQ-EXAMPLE-01",
        .revision = 3,
        .status = .accepted,
        .label = "Example.",
        .owner = "owner.md",
        .suites = &.{model_types.testSuite(0)},
        .limitation_status = .unassessed,
    }};
    const groups = [_]model_types.RequirementGroup{.{
        .title = "Example",
        .requirements = &requirements,
    }};
    const graph: model_types.Graph = .{
        .documents = &.{},
        .concepts = &.{},
        .groups = &groups,
        .test_specs = &.{},
        .test_bindings = &.{},
        .verification = &.{},
        .implementations = &.{},
    };
    var output = std.Io.Writer.Allocating.init(std.testing.allocator);
    defer output.deinit();
    try newTest(
        &graph,
        "example-scenario",
        "REQ-EXAMPLE-01",
        @tagName(model_types.testSuite(0)),
        .{},
        null,
        &output.writer,
    );
    const written = output.written();
    for ([_][]const u8{
        profile.paths.verification,
        profile.paths.test_specs,
        profile.paths.test_bindings,
        "REQ-EXAMPLE-01@3",
        "INV-EXAMPLE-SCENARIO",
        "NO-EXAMPLE-SCENARIO",
        "```zig tj-test",
        "then_inv_example_scenario",
        "fixture_example_scenario",
        "example_scenario.zig",
        profile.verify_command,
    }) |needle| {
        try std.testing.expect(std.mem.indexOf(u8, written, needle) != null);
    }
    try std.testing.expectError(
        error.RequirementNotFound,
        newTest(&graph, "example", "REQ-MISSING-01", "u", .{}, null, &output.writer),
    );
    try std.testing.expectError(
        error.UnknownSuite,
        newTest(&graph, "example", "REQ-EXAMPLE-01", "zz", .{}, null, &output.writer),
    );
}