Evidence producer guide

This guide is for authors of tools that write notarizing.check-report/1 reports. A report is the claim of one check attempt about one requirement. Notarizing stores the claim and evaluates it under a reviewed policy. A report never grants trust, approval or a source.

The format is frozen. The normative definitions are:

• the JSON Schema;
• the format rules;
• the example reports.

Example producer

examples/producers/gotestreport converts go test -json output and a mapping file into one report for each mapped check, with the raw test log as its artifact. Your harness runs it after its own test run. Notarizing never runs it. See the producer README.

Import the whole output directory in one command:

notarizing evidence import --dir reports

--dir imports reports/NAME/report.json of each subdirectory, with that subdirectory as the artifacts directory. Each report gets its own receipt. A failed report does not stop the others; the command then lists each file and fails. At most 256 reports are imported in one command.

The mapping file has the format gotestreport.mapping/1. Its JSON Schema is gotestreport-mapping.schema.json.

Fields

Every field is required. Notarizing decodes the report strictly: a duplicate key, an unknown field, malformed UTF-8, an invalid time or UUID, or an oversized value rejects the report before it is stored.

A snapshot reference has repository_id, revision (the full commit ID), path (POSIX, relative) and sha256 of the exact file bytes at that commit.

Targets

The target.kind must agree with the method:

static_analysis and human_review can name any target with a precise scope.

A model result never covers the implementation. To claim that the code follows the model, submit a separate correspondence report.

Methods

static_analysis, implementation_test, component_simulation, integration_test, finite_model_exploration, bounded_symbolic_check, inductive_model_proof, implementation_trace_conformance, implementation_refinement_proof, measurement, human_review.

A method is not a confidence level. The binding of the check names one method. A report with another method does not count for that check.

Scope claims

Write the scope so that a reviewer can see what the result covers and what it does not:

• claim: one statement of what you checked, for example "Refunds above the daily limit are refused for EUR and USD accounts."
• environment: the platform and the configuration of the run.
• assumptions: what the result depends on, for example "The clock is monotonic."
• exclusions: what you did not check.
• bounds: string values such as "cases": "500". Put the configuration name in bounds.configuration, for example "configuration": "linux-amd64". A binding can require a report for each configuration.

Do not write instructions for a reader or an agent in any field. Notarizing shows every field as data.

Coverage

• completed must be a subset of requested. Each ID is unique.
• A complete run lists every requested ID in completed.
• A pass needs complete coverage. An incomplete run can report an observed failure, but it cannot establish the whole claim.
• A single proof obligation can be one requested ID.

Artifacts

Declare each file that the reviewer needs: logs, traces, counterexamples. Notarizing reads each file only below the artifacts directory of the import and checks its length and SHA-256.

• Use relative POSIX paths. Absolute paths, . and .. components, backslashes, NUL characters, devices and symbolic links that escape the directory are refused.
• One bad artifact rejects the whole report.
• Notarizing never opens, runs or fetches what an artifact or a field names.

Import a report with its artifacts:

notarizing evidence import --artifacts ./out report.json

Several report files can share one artifacts directory: notarizing evidence import --artifacts ./out a.json b.json.

Retries and conflicts

The retry key is the source namespace and the report_id.

• The same bytes again return the same receipt. This is safe after a lost response.
• The same report_id with other bytes is a conflict. The first receipt stays.
• To correct a result, write a new report with a new report_id. The operator then records the relation with notarizing evidence correct. A correction does not retire a failure. A reviewer can then retire it with a reviewed supersession in the browser, when the new report is eligible under the policy.

How notarizing evaluates a report

The reported outcome stays visible. The evaluated status comes from the policy, the bindings and the requested context.

Stale is not fail. A stale report was about other inputs. It says nothing about the requested inputs. Run the check again on the requested revision.

Some findings are never a violation:

• target_integrity_failure: the protected target did not match. The status is unknown. It does not show that the property is false.
• induction_counterexample: a proof obligation failed without a reachable witness. The status is unknown, not fail.
• expected_negative_control: the report is about a deliberately broken control, not about the candidate.

A later pass never clears an earlier failure of the same row. Both stay visible as an unresolved contradiction until a reviewed supersession resolves it.

Transport

Notarizing accepts a report from a local file (notarizing evidence import), from an evidence bundle, or over the optional ka2a adapter (evidence-over-ka2a/1). The channel and the verified principal decide the source namespace. A field in the report never does.