lib/choir/src/properties/evidence.zig
daab053ee43316e1809a84551d573ddd1e5bf3d2
1 const std = @import("std");
2 const cfg = @import("cfg.zig");
3 const evidence_options = @import("evidence_options");
4 const hypothesis = @import("hypothesis");
5 const pretty = @import("pretty");
6 const sys = @import("sys");
7
8 const property_source = @embedFile("cfg.zig");
9 const output_bytes_max = 32 * 1024;
10 const revision_file_bytes_max = 128;
11 const status_file_bytes_max = 64 * 1024;
12
13 const Fact = struct {
14 name: []const u8,
15 value: []const u8,
16 };
17
18 const Source = struct {
19 path: []const u8,
20 sha256: []const u8,
21 };
22
23 const Receipt = struct {
24 schema: []const u8 = "tiny.verification.evidence/v1",
25 id: []const u8 = "choir.cfg.predecessor-mirror.property",
26 kind: []const u8 = "property",
27 outcome: []const u8 = "passed",
28 source_revision: []const u8,
29 source_clean: bool = true,
30 command: []const u8 = "zig build choir-cfg-evidence",
31 producer: []const u8 = "choir-cfg-evidence/v1",
32 sources: []const Source,
33 bounds: []const Fact,
34 coverage: []const Fact,
35 checks: []const Fact,
36 nonclaims: []const []const u8,
37 };
38
39 const RunEvidence = struct {
40 coverage: cfg.EvidenceCoverage,
41 valid_examples: usize,
42 seed: u64,
43 };
44
45 const bounds = cfg.EvidenceBounds{};
46 const bound_facts = [_]Fact{
47 .{ .name = "actions_per_example_max", .value = std.fmt.comptimePrint("{d}", .{
48 bounds.actions_per_example_max,
49 }) },
50 .{ .name = "actions_per_example_min", .value = std.fmt.comptimePrint("{d}", .{
51 bounds.actions_per_example_min,
52 }) },
53 .{ .name = "blocks", .value = std.fmt.comptimePrint("{d}", .{bounds.blocks}) },
54 .{ .name = "examples", .value = std.fmt.comptimePrint("{d}", .{bounds.examples}) },
55 .{ .name = "operations", .value = std.fmt.comptimePrint("{d}", .{bounds.operations}) },
56 .{ .name = "seed", .value = std.fmt.comptimePrint("0x{x}", .{bounds.seed}) },
57 .{ .name = "successors_per_operation_max", .value = std.fmt.comptimePrint("{d}", .{
58 bounds.successors_per_operation_max,
59 }) },
60 };
61
62 const nonclaims = [_][]const u8{
63 "Zig-to-Lean refinement proof or Zig source correctness proof",
64 "allocation and out-of-memory rollback",
65 "arbitrary block, operation, successor, or trace sizes",
66 "concurrency",
67 "dominance",
68 "nested regions",
69 "operation-order cache repair",
70 "pointer identity",
71 "traits and interfaces",
72 "use-def chains",
73 };
74
75 comptime {
76 std.debug.assert(output_bytes_max >= 1024);
77 std.debug.assert(revision_file_bytes_max > 40);
78 std.debug.assert(status_file_bytes_max >= 1024);
79 std.debug.assert(bound_facts.len == 7);
80 std.debug.assert(nonclaims.len == 10);
81 }
82
83 var recorded_coverage = cfg.EvidenceCoverage{};
84
85 const AuditedProperty = struct {
86 pub fn property(
87 conjecture: *hypothesis.ConjectureData,
88 allocator: std.mem.Allocator,
89 ) !void {
90 try cfg.propertyWithCoverage(conjecture, allocator, &recorded_coverage);
91 }
92 };
93
94 pub fn main(init: sys.process.Init) u8 {
95 run(init) catch |err| {
96 writeFailure(init, err);
97 return 1;
98 };
99 return 0;
100 }
101
102 fn run(init: sys.process.Init) !void {
103 const args = try init.minimal.args.toSlice(init.arena.allocator());
104 if (args.len != 4) return error.InvalidArgumentCount;
105 var revision_storage: [revision_file_bytes_max]u8 = undefined;
106 const revision_text = try std.Io.Dir.cwd().readFile(
107 init.io,
108 args[1],
109 &revision_storage,
110 );
111 const source_revision = std.mem.trim(u8, revision_text, " \t\r\n");
112 if (!validRevision(source_revision)) return error.InvalidSourceRevision;
113 var status_storage: [status_file_bytes_max]u8 = undefined;
114 const status_text = try std.Io.Dir.cwd().readFile(
115 init.io,
116 args[2],
117 &status_storage,
118 );
119 if (std.mem.trim(u8, status_text, " \t\r\n").len != 0) {
120 return error.DirtyEvidenceSource;
121 }
122 const actual = try exercise(init.gpa);
123 if (actual.valid_examples != bounds.examples or actual.seed != bounds.seed) {
124 return error.UnexpectedPropertyRun;
125 }
126 if (!actual.coverage.complete()) return error.InsufficientCoverage;
127 var encoded: [output_bytes_max]u8 = undefined;
128 const receipt = try encode(actual.coverage, source_revision, &encoded);
129 try std.Io.Dir.cwd().writeFile(init.io, .{
130 .sub_path = args[3],
131 .data = receipt,
132 });
133 }
134
135 fn exercise(allocator: std.mem.Allocator) !RunEvidence {
136 recorded_coverage = .{};
137 var result = try hypothesis.checkFn(
138 allocator,
139 &AuditedProperty.property,
140 cfg.evidenceSettings(),
141 );
142 defer result.deinit();
143 if (!result.passed) return result.failing_error orelse error.PropertyFailed;
144 if (result.invalid_examples != 0 or result.replayed_examples != 0) {
145 return error.UnexpectedPropertyRun;
146 }
147 return .{
148 .coverage = recorded_coverage,
149 .valid_examples = result.valid_examples,
150 .seed = result.seed,
151 };
152 }
153
154 fn encode(
155 coverage: cfg.EvidenceCoverage,
156 source_revision: []const u8,
157 output: []u8,
158 ) ![]const u8 {
159 var property_digest: [32]u8 = undefined;
160 std.crypto.hash.sha2.Sha256.hash(property_source, &property_digest, .{});
161 var property_hex = std.fmt.bytesToHex(property_digest, .lower);
162 const sources = [_]Source{
163 .{
164 .path = "lib/choir/build/tests.zig",
165 .sha256 = evidence_options.build_source_sha256,
166 },
167 .{ .path = "lib/choir/src/properties/cfg.zig", .sha256 = &property_hex },
168 .{
169 .path = "lib/choir/src/properties/evidence.zig",
170 .sha256 = evidence_options.producer_source_sha256,
171 },
172 };
173 var coverage_storage: [5][32]u8 = undefined;
174 var check_storage: [4][32]u8 = undefined;
175 const coverage_facts = try makeCoverageFacts(coverage, &coverage_storage);
176 const check_facts = try makeCheckFacts(coverage, &check_storage);
177 const value = Receipt{
178 .source_revision = source_revision,
179 .sources = &sources,
180 .bounds = &bound_facts,
181 .coverage = &coverage_facts,
182 .checks = &check_facts,
183 .nonclaims = &nonclaims,
184 };
185 var writer = std.Io.Writer.fixed(output);
186 var json = pretty.json.Writer.init(&writer, .minified);
187 try json.write(value);
188 try json.newline();
189 return writer.buffered();
190 }
191
192 fn makeCoverageFacts(
193 coverage: cfg.EvidenceCoverage,
194 storage: *[5][32]u8,
195 ) ![5]Fact {
196 return .{
197 .{ .name = "tiny.choir.Block.addOperation", .value = try countText(
198 &storage[0],
199 coverage.attach,
200 ) },
201 .{ .name = "tiny.choir.Block.detachOperation", .value = try countText(
202 &storage[1],
203 coverage.detach,
204 ) },
205 .{ .name = "tiny.choir.Block.removeOperation", .value = try countText(
206 &storage[2],
207 coverage.remove,
208 ) },
209 .{ .name = "tiny.choir.Operation.moveToEnd", .value = try countText(
210 &storage[3],
211 coverage.move,
212 ) },
213 .{ .name = "tiny.choir.Operation.setSuccessors", .value = try countText(
214 &storage[4],
215 coverage.replace,
216 ) },
217 };
218 }
219
220 fn makeCheckFacts(
221 coverage: cfg.EvidenceCoverage,
222 storage: *[4][32]u8,
223 ) ![4]Fact {
224 return .{
225 .{ .name = "model.operation.parent", .value = try countText(
226 &storage[0],
227 coverage.parent,
228 ) },
229 .{ .name = "tiny.choir.Block.getNumPredecessors", .value = try countText(
230 &storage[1],
231 coverage.predecessor_count,
232 ) },
233 .{ .name = "tiny.choir.Block.hasPredecessor", .value = try countText(
234 &storage[2],
235 coverage.has_predecessor,
236 ) },
237 .{ .name = "tiny.choir.ir.verifyBlock", .value = try countText(
238 &storage[3],
239 coverage.verifier,
240 ) },
241 };
242 }
243
244 fn countText(storage: *[32]u8, count: u64) ![]const u8 {
245 return std.fmt.bufPrint(storage, "{d}", .{count});
246 }
247
248 fn validRevision(revision: []const u8) bool {
249 if (revision.len != 40) return false;
250 for (revision) |byte| {
251 if (!std.ascii.isDigit(byte) and !(byte >= 'a' and byte <= 'f')) return false;
252 }
253 return true;
254 }
255
256 fn writeFailure(init: sys.process.Init, err: anyerror) void {
257 var stderr_buffer: [1024]u8 = undefined;
258 var stderr_writer = sys.stdio.stderr().writer(init.io, &stderr_buffer);
259 defer stderr_writer.interface.flush() catch {};
260 var text_buffer: [1024]u8 = undefined;
261 var text = pretty.TextWriter.init(
262 &stderr_writer.interface,
263 &text_buffer,
264 .{ .width = 100 },
265 );
266 text.writer.print("choir CFG evidence: {s}\n", .{@errorName(err)}) catch {};
267 text.writer.flush() catch {};
268 }
269
270 test "CFG evidence coverage rejects an unexercised API" {
271 var coverage = cfg.EvidenceCoverage{
272 .examples = bounds.examples,
273 .attach = 1,
274 .replace = 1,
275 .detach = 1,
276 .move = 1,
277 .remove = 1,
278 .parent = 1,
279 .has_predecessor = 1,
280 .predecessor_count = 1,
281 .verifier = 1,
282 };
283 try std.testing.expect(coverage.complete());
284 coverage.replace = 0;
285 try std.testing.expect(!coverage.complete());
286 }
287
288 test "CFG evidence freshness accepts only lowercase Git identities" {
289 try std.testing.expect(validRevision("0000000000000000000000000000000000000000"));
290 try std.testing.expect(!validRevision("000000000000000000000000000000000000000"));
291 try std.testing.expect(!validRevision("000000000000000000000000000000000000000A"));
292 }
293
294 test "CFG evidence receipt keeps the common typed envelope" {
295 const coverage = cfg.EvidenceCoverage{
296 .examples = bounds.examples,
297 .attach = 1,
298 .replace = 1,
299 .detach = 1,
300 .move = 1,
301 .remove = 1,
302 .parent = 1,
303 .has_predecessor = 1,
304 .predecessor_count = 1,
305 .verifier = 1,
306 };
307 var output: [output_bytes_max]u8 = undefined;
308 const receipt = try encode(
309 coverage,
310 "0000000000000000000000000000000000000000",
311 &output,
312 );
313 try std.testing.expect(std.mem.endsWith(u8, receipt, "\n"));
314 try std.testing.expect(std.mem.indexOf(
315 u8,
316 receipt,
317 "\"schema\":\"tiny.verification.evidence/v1\"",
318 ) != null);
319 try std.testing.expect(std.mem.indexOf(
320 u8,
321 receipt,
322 "\"tiny.choir.Operation.setSuccessors\"",
323 ) != null);
324 }