Proof Generator
The proof generator assembles an evidence package for a defined scope: what the package contains, what it must carry so a reader can recompute its claims without the graph in hand, and what it must leave untouched while doing so. Its requirements also cover the refusal path — when the proof gate reports a scope blocked, no part of a package for that scope comes into existence, and the refusal arrives with the gate’s report attached.
The proof generator shall assemble every evidence package from a design consistency proof, an execution coverage record, a coverage report, and an evidence manifest. |
The proof generator shall include in a package’s scope every node reachable from the requested requirements through strong edges, where a Refines edge leads only from a requirement to the requirements that refine it, never to the requirement it refines. |
The proof generator shall include in a package’s scope every test outcome confirming an in-scope test specification and every waiver excusing an in-scope test outcome. |
The proof generator shall record in every evidence package every input from which that package’s design root is recomputed: the node hashes and the edges of its design set, the requested scope, and the revision the scope was judged against. |
Software Requirement: A package's root is sealed over nothing but the design, scope and revision SEG-SREQ-133
|
The proof generator shall compute every evidence package’s design root over the node hashes and edges of its design set, the requested scope and the revision, and over nothing else. |
The proof generator shall record in every evidence package the scope for which it was generated. |
The proof generator shall report in every evidence package whether that package’s scope includes every requirement that refines no other requirement. |
Note
A requirement that refines no other requirement is top-level — it is
never the source of a refines edge.
The proof generator shall exclude from an evidence package every outcome the gate evaluator reports as stale. |
The proof generator shall leave node, edge and affirmation state unchanged when it generates an evidence package. |
The proof generator shall mint every snapshot identifier using only characters that are valid in a file name on both POSIX and Windows filesystems. |
If the proof gate reports a scope as blocked, then the proof generator shall produce no part of an evidence package for that scope. |
The proof generator shall accompany every refusal with the gate’s report for the refused scope. |
The proof generator shall refuse only those scopes the proof gate reports as blocked. |
The proof generator shall record in every evidence package the digest of every run bundle that supplied a test outcome in the package’s scope. |