Proof Verifier
The proof verifier reads an evidence package and checks it. A package is sealed by its design root, and the other three documents are not. So the verifier makes several checks and names each one. A check that needs more than the package, such as the run bundles or the case, is made only when the operator gives them. The verifier names every check it did not make, so a pass never says more than the package supports.
Some checks need only the package: the root, the identity, the agreement of the documents and the verdict the package records. They are made whatever else is given. A package named by the path of its directory is read whether or not a configuration file or a case exists (A package named by its path... (SEG-SREQ-270)).
The verifier judges a package at the revision the package records. It reads no repository and needs no current revision.
When it rebuilds the evidence from run bundles, the verifier first checks that the readers the configuration names supply the design the package records (The configured design must ... (SEG-SREQ-244)). It then takes the design edges of the package as affirmed. A package exists only for a scope that the gate found ready, so every design edge was affirmed when the package was sealed. The check of the affirmations (Affirmations stand behind t... (SEG-SREQ-241)) checks that separately, against the case.
The proof verifier shall report, for every check it makes of an evidence package, whether the package passes that check. |
The proof verifier shall recompute the design root of an evidence package from the node hashes, the design edges, the scope and the revision that the package’s design consistency proof records, and report whether it equals the recorded root. |
The proof verifier shall report whether the documents of an evidence package agree on the snapshot, the requested scope and the revision. |
The proof verifier shall report whether every outcome and every finding that the documents of an evidence package name is a member of the package’s scope, and whether the execution coverage record and the coverage report agree on which outcomes are set aside, skipped and excused. |
The proof verifier shall report whether the coverage report of an evidence package records the scope as not blocked. |
While it is given a case, the proof verifier shall report, for every strong edge of an evidence package’s design set, whether the case holds a review event that binds the edge’s endpoints to the node hashes the package records for them. |
If a run bundle given to the proof verifier has a digest that the evidence package does not list, then the proof verifier shall report a mismatch. |
If an evidence package lists the digest of a run bundle and the proof verifier is given run bundles but none with that digest, then the proof verifier shall report that the evidence cannot be judged. |
If the readers the configuration names do not supply a design node of an evidence package with the node hash the package records, or do not supply a design edge the package records, then the proof verifier shall report that the evidence cannot be judged. |
While it is given run bundles whose digests the package lists, the proof verifier shall report whether the outcomes and findings it rebuilds from those run bundles at the revision the package records, judged at the date of the snapshot timestamp that the recorded snapshot identifier carries, equal the outcomes and findings the package records. |
While it rebuilds the evidence of an evidence package, the proof verifier shall report whether the snapshot identifier minted from the rebuilt scope, with the timestamp the recorded identifier carries, equals the recorded identifier. |
The proof verifier shall report whether the snapshot identifier that an evidence package records equals the name of the package’s directory. |
The proof verifier shall report whether every outcome in the execution coverage record of an evidence package carries the revision the package records. |
The proof verifier shall report whether any outcome of an evidence package’s execution coverage record is also listed as stale in its coverage report. |
The proof verifier shall report whether the member scope of an evidence package is exactly the nodes of its design consistency proof, the outcomes of its execution coverage record and its coverage report, and the waivers its execution coverage record names. |
The proof verifier shall report whether the coverage report of an evidence package lists any unready edge. |
The proof verifier shall report whether the coverage report of an evidence package holds any finding that blocks. |