Evidence¶
Read a result as a claim about exact inputs under stated assumptions. Identify the property, model, configuration, bounds, outcome and retained artifacts before drawing a conclusion.
Three teaching packages¶
The payment, identity and priority models introduce narrow mechanisms. Their results do not replace the broader reference-profile evidence.
Complete selected reference profile¶
The subject pages explain how to assess each family’s configurations, ordinary companions, deliberate controls and supplier limits. The complete package page retains all individual records and every available full trace.
- Costs and payment: evidence scope
- Objects and lifetime: evidence scope
- Schema and setup: evidence scope
- Turns and objectives: evidence scope
- Traversal and inspection: evidence scope
- Object operations and instructions: evidence scope
- Abilities and timing: evidence scope
- Registry and lifecycle: evidence scope
- Checkpoint composition: evidence scope
- Selected scope and correspondence
- Reference-profile evidence
The visible release label identifies this documentation artifact. Each result also binds its own input revision. A model’s presence in the reference does not imply that every property passed, every branch was reached or a broader implementation was qualified.
Ask what kind of result it is¶
Class |
What to inspect |
|---|---|
Prepared assertion |
The concrete inputs and expression evaluated. A self-loop fixture is not a stateful procedure driver. |
Finite state exploration |
Starting states, permitted steps, explored bounds, constraints and named properties. |
Temporal check |
The behavior property, actual fairness and provider assumptions, and the finite configuration. |
Intended negative control |
The explicit defect, ordinary companion, expected property and actual diagnostic. A tool or resource error is not the intended failure. |
Correspondence check |
Both exact models, typed mapping, compared state/initial/labelled-edge content and finite scope. |
A completed exploration does not establish every instance size. Source written in a formal language is not itself an unbounded theorem. An independently admitted theorem proof would need its own evidence.
Read the whole outcome¶
The receipt retains source/configuration identities, tool identity, command, properties, bounds, assumptions, actual exit and terminal diagnostics. Missing artifacts, unexpected outcomes, timeouts and resource-limited attempts remain unadmitted. Checker warnings are retained with their actual scope rather than discarded.
A negative control belongs to its deliberately defective variant. A witness uses an observation condition to illustrate legal behavior. An authored example explains a mechanism. These are different evidential roles.
Inspect a complete trace¶
A trace preserves explicit value kinds, state order, edge metadata and any captured back or stuttering edge. Changed values have text indicators. A representation change can occur without a value change.
Large traces store repeated values once in a complete typed pool. Every field, item and finite-function entry remains inspectable through static links. State selection enhances the page without removing the complete sequence. Successful checks can have no counterexample trace; they do not invent an example execution.
Preserve source scope¶
The selected source inventory and finite correspondence checks are broader than the teaching models. Candidate branch anchors are a mechanical inventory. A branch can be retained in its exact counterpart while having no individual execution measurement; that limitation is recorded separately.
Current source, interpretation, bounded checking, runtime implementation, full-game execution and universal proof remain distinct claims. Begin with invariants and checking or Meet the reference profile when a result’s boundary is unclear.