# Evidence Design Reference Read this only while designing or repairing Contract Checks and proof. ## General Proof Rules - Every Outcome has at least one executable Check and one non-Result atomic Claim. - Keep four authorities separate: Source/Context/canonical resources/Contract own Expected; a package-admitted adapter owns current Actual; Harness owns comparison/result identity and verdict; the sole current-snapshot Final Gate owns terminal status. No project runner or Oracle may own two of these layers for a machine-closing obligation. - Required proof surfaces are non-empty, unique and all-of. Every Claim-bearing Assertion proves exactly one Claim at one exact applicability profile and uses explicit comparable Observations and expected values; every Claim/applicability/proof-surface cell must be covered. - `truthy`/`falsy` are diagnostic-only. `exists` proves only implementation-structure obligations. Missing or type-incomparable Observation never proves a Claim; negative proof uses an explicit value such as `equals: false`. - Claim and Population proof is emitted only after the entire Check passes. Exit failure, missing artifact, failed population, failed Assertion or invalid Counterfactual yields no Claim proof. - Verification inputs include entrypoints, helpers, fixtures/config, package scripts and lockfiles and cannot overlap implementation carriers. The frozen runner identity recursively includes the supported direct-literal local verifier module/config/data graph; runtime-owned Check inputs/outputs/artifacts are explicitly excluded from Oracle identity, while non-literal loaders, `createRequire` and package scripts without a recoverable static Node entry fail closed. Declaring other indirect/custom Oracle access as a named TCB does not admit it for machine completion; use a package-admitted adapter or blocking External Confirmation. - Runners receive the minimum environment whitelist plus only declared environment requirements. Never expose actual secret values in findings. ## Runner And Observation Identity Runner kind still selects payload decoding, but payload decoding is not observation authority. Raw Execution identity binds the runner, its recursively frozen local dependency closure and canonical declared Environment Requirements, not actual values. Bare installed packages and the Harness/runtime remain named trusted-computing-boundary components rather than silently mutable project helpers. A project-authored verifier, `node_oracle`, wrapper or Playwright payload can provide diagnostics only unless a separate admitted package observer independently extracts the current Actual. Across all Checks sharing a Raw Execution, one Claim-bearing Observation belongs to one Assertion. Shared setup may execute once only when independent per-Check observations and artifacts remain unambiguous. ## Observation Authority Admission Compile derives one immutable internal observation-authority plan for every machine Claim or Fact × required-method obligation. It binds the obligation/Fact/Assertion/target/proof-surface/method, expected identity/value, locator policy, carriers and runtime requirements. This is a rebuildable projection, never a new Contract Authority, state or Observer registry. A machine-closing row has exactly one of these first-slice authorities: - `package_static_json_exact`: plain `exact_value + exact` content for a static implementation/configuration structure. The UTF-8 JSON carrier must already exist in the pre-run workspace manifest; its no-follow path/type/size/digest/file identity remains unchanged after the runner; it matches the declared production Binding; and it is not Source, Context, Contract, expected authority, verifier output, evidence, report, status or Receipt. Harness, not the project, selects the fixed RFC 6901 `/observations/` locator and applies the package duplicate-key, UTF-8, size, depth and pointer limits. A generated bundle/configuration is eligible only when it was already in the candidate snapshot. This proves only current static content, never runtime consumption, interaction or liveness. - `package_process_json_exact`: plain exact output from a declared `runtime_family: process`, `role: product` root. The Check uses `project_binary`, its target and complete argv equal the Source-backed root invocation exactly, no project wrapper intervenes and its effect is read-only or test-sandbox. The target's canonical Source obligation, Source Claim disposition and execution target agree on key, role, family, root, complete argv and capabilities. Compile creates one internal process-runtime closure containing that invocation, the Claim/Counterfactual production carriers and only finite argv values that resolve to production Binding members. It examines a standalone argument or explicit `--key=value`, resolves safe repository-relative values from declared `cwd`, and admits a path only when an exact or pattern Binding covers it; glob-owned and extensionless files are supported. An unmatched safe relative value is ignored and not copied. Absolute paths, repository escapes, `file:` URLs and network URLs fail closed unless explicitly routed to the existing external TCB/External Confirmation boundary. It neither broadly role-scans nor copies all `input_paths`; role separation applies only to actual closure members. Global Checks use internal scoped Binding records `{ outcome_key, local_key, binding_ref, binding }` with `.`, preserving logical refs while deduplicating identical physical paths without changing authored Contract Bindings or adding a registry. Every closure member is disjoint from Source/Context/Contract/canonical expected authority, verification inputs, verifier/evidence/status/report/comparison/Receipt/Long-Task workdir, historical session/evidence, `expected_output_paths`, `artifact_globs` and other proof-output roles. Harness copies only this compiled closure into an OS-temporary snapshot, then directly spawns/owns the root there. The child receives the minimal runner environment and no observation-path, challenge or protocol variable. It writes exactly one bounded `ty-context-product-observation-v1` envelope to stdout with exact keys `schema_version` and identity-keyed `observations`; Harness captures stdout, requires the exact compiled identity set, extracts multiple values, records host execution attestation bound to the closure identity, verifies the closure again and deletes the snapshot. The envelope proves only exact values actually emitted by that root on the declared JSON output surface. Project-authored instrumentation or mapping cannot elevate arbitrary internal/UI facts into package-observed truth; a Claim that cannot bind directly to that surface remains External Confirmation. The per-execution nonce is generated and retained only inside host attestation; it is neither a child-visible challenge nor a trust root. Everything else is unsupported and therefore a blocking External Confirmation: custom or `named_external_tcb` Oracle, indirect wrapper, browser/native/device session, layout, pixel, accessibility, motion, protected raw observation, tolerance/mask and custom locator. Target family must equal observer family. Project-submitted v3 actual/value digest, comparison result, `passed`, verdict and capability records remain optional diagnostics and never own Actual or completion. Current package derivation covers exact/presence plus host-derived `target_runtime`; `interaction_trace`, `state_delta`, `design_conformance` and every other capability without package derivation require External Confirmation even when a project record is present. A diagnostic copy that disagrees with a derived result fails closed. The public project result remains `long-task-check-result-v3`; the stdout product observation envelope is a separate v1 protocol, so no v4 is introduced. ## Scenario And Evidence Capabilities - Every Check declares non-empty keyed `scenario.given` and `scenario.when` steps. One Check covers one materially coherent journey; a different success path belongs in another Check or vertical Outcome. A Claim-bearing Assertion's `applicability_ref` must match the Check target, journey role, duplicate-free atomic dimension assignments, all keyed Given refs and ordered When refs exactly. - Every Assertion declares a non-empty all-of `evidence_capabilities` set. `presence` proves static existence only and cannot alone prove a behavioral Claim. A project payload may contain one typed current-execution compatibility record per capability, but a machine Claim is satisfied only by a matching package-derived result. In the current slice that means exact/presence and, for a direct process root, host `target_runtime`; missing admission, duplicate/unknown/undeclared records or disagreement with a submitted copy fail closed. - `interaction_trace` names the exact target plus the declared Given keys and ordered action keys, but no package derivation currently owns those semantics. Project/Playwright trace rows are diagnostic and the obligation remains External Confirmation, including on a direct process root. - `state_delta` compatibility rows still require different before/after hashes and named changed fields, but they are not package-derived machine proof. The same external boundary applies to `durable_readback`, `cross_surface_consistency`, `boundary_invocation`, `external_side_effect`, `failure_injection`, `input_variation`, `visual_render`, `design_conformance` and `design_method` until a package adapter derives the applicable result. - `target_runtime` binds the exact target/root and is host-derived only for a direct process product root. Runtime Fact refs and every admitted package-derived exact/presence result remain set-equal to the compiled obligation cells; no aggregate project record fills a missing cell. - Structured runners emit `long-task-check-result-v3` for capability records. V2 payloads remain decodable only for presence-only compatibility; they cannot satisfy a declared non-presence capability. Evidence records contain bounded hashes/ids/refs, not unrestricted raw payloads. ## Non-UI Semantic Fact Evidence Every machine `semantic_fact` proof binding compiles one immutable expectation row identified by manifest/digest, Outcome, Fact, proof method, Claim, applicability, subject/relation/population, exact condition and property. It freezes the Source-located expected value digest, sensitivity, comparator/mode/parameters/tolerance/mask, admitted observer identity and environment definition. Runtime evidence cannot rewrite any field, and Compile rejects a machine row whose method/surface/target/sensitivity/comparison mode has no admitted observer. The owning Check may submit compatibility data, but the package observer derives exactly one authoritative current `semantic_fact` result for every and only every admitted expectation assigned to it. Each result records: - exact assertion/manifest/Outcome/target/Fact/proof/method/subject/condition/property identity; - an attributable actual-observation artifact, current digest, typed locator and value digest; - an attributable actual-environment artifact, current digest, typed locator and value digest; - the frozen expected located authority and comparison tuple, plus a current comparison artifact/locator/result digest; - explicit `passed|failed` comparison and verdict; - the exact Oracle/environment identity; and - one result for every declared independent observer where applicable. V1 ground, V2 symbolic, non-UI semantic Fact, static observer and process observer all call the same Harness-owned `evaluateExactDigestComparison` with identity, actual/expected value digests, comparator/mode and parameter/tolerance/mask digests. The admitted exact slice permits only `exact_value + exact`, requires empty tolerance/mask and fails whenever actual differs from expected. Harness recomputes result identity; submitted `passed`/verdict never participates and any submitted comparison field that disagrees fails closed. Protected and tolerance/mask observations are not admitted in this slice and remain External Confirmation; secrets, tokens, personal or regulated values never enter Contract, logs, findings, Context or artifacts in raw form. Result identities and primary observations are duplicate-free. One aggregate Boolean/report/log/screenshot, one reused artifact+locator+value tuple, one all-states row or one Check exit code cannot satisfy several Facts or methods. A Fact may legitimately require several independently admitted methods/observers, and all must pass. Population/quantified Facts additionally prove exact expected universe = eligible = observed plus valid exclusions. Evidence must reach the furthest independently failing admitted boundary; parser/request/queue acceptance or implementation self-report does not prove storage, downstream delivery, recovery, security or external effect. Final Gate requires exact expectation/result set equality on its one current snapshot and rejects missing, extra, duplicate, stale, failed, authority-drifted, environment-mismatched, proxy-only, reused or indistinguishable results. External-confirmation obligations emit no fabricated machine row and remain pending through terminal reporting. Manifest/preflight success, hashes, Census, schema validation, focused tests and Progress prove only their own input/integrity/intermediate claims. ## Live Target Runtime Evidence - Machine target-runtime authority exists only for `package_process_json_exact`: Harness directly spawns the exact declared `runtime_family: process`, `role: product` root entrypoint and derives host execution attestation, target liveness, current exact/presence Actuals and exit result. This does not derive the semantic Given/action sequence required by `interaction_trace`. A project `target_runtime`, new `session_id`, `cold_start: true`, historical session, wrapper or child self-report is diagnostic only. - Static package observation proves structure/configuration content only. It cannot prove runtime consumption, interaction, liveness or production reachability merely because its path appears in a Binding or `input_paths`. - Browser/native/desktop/device runtime and layout/pixel/accessibility/motion observations have no admitted adapter in this slice. Playwright, H5/browser proxies, project binaries, screenshots and session payloads cannot close those machine Claims; retain a blocking External Confirmation. - Target family must equal admitted observer family. A proxy may prove only its own separately admitted Fact; it cannot substitute when proxy and required target can fail independently. - Historical reports, screenshots, binaries and logs are review material. Current-run diagnostics may accompany a Check as Artifacts, but only package extraction from the current frozen static carrier or Harness-owned direct process creates accepting Actual. - Bind every process runtime dependency through the Source-backed root plus its production owner/Binding. For argv, use only a standalone argument or explicit `--key=value`; Harness resolves a safe repository-relative value from declared `cwd` and includes it only when a production Binding exact path or pattern covers the result. Glob-owned and extensionless files are valid. An unmatched safe relative value is not copied; absolute, escaping, `file:` and network values fail closed unless explicitly external. Bind modules/configuration and Claim/Counterfactual carriers directly. Keep `input_paths` as ordinary Check scope/freshness and project verifier/helper material in `verification_inputs`: it is neither broadly role-scanned nor promoted into the snapshot. The declaration-stable compiled process closure is the only snapshot-copy input, and role separation checks only its actual members. Exact planned members may be absent through Preflight/Compile but must materialize at Final Gate. Compatible Cross-Check and implicit-preserved Facts may share one Raw Execution/envelope, but every Fact keeps its own obligation/comparison identity. A missing production binding for an actual dependency, forbidden closure-role overlap or absent Final member fails closed. This lets existing Progress freshness identify when rolling feedback is stale without a new trigger registry or dependency parser. ### Process Containment TCB The isolated runtime-closure snapshot, minimal environment, bounded stdout capture, no-follow/digest checks, direct process handle, timeout, process-tree monitoring and cleanup reduce self-attestation and cross-execution priming. Static observation likewise retains prepare-all mutation watching plus per-file pre/post identity/hash. Subtraction controls reopen transient/persistent carrier swaps or descendant/timeout leaks when those owner responsibilities are removed, so do not replace either pair with prose or a new edge mechanism. They are not an absolute security sandbox. The TCB includes the host OS/filesystem/process APIs, Node runtime and process-enumeration/termination behavior. Harness does not claim to contain a deliberately malicious executable that escapes the copied closure, accesses ambient filesystem/network resources or evades every OS process-tree mechanism. If a Claim needs that adversary boundary, run the target inside an independently controlled sandbox and retain External Confirmation until that observer is separately admitted. ## Causal Boundary Review After Revision - When a rolling blocker causes a semantic or proof revision, review only the affected weak-observability or high-risk Outcomes before adoption. Ask whether a cheaper proxy, fixed response or self-reported success could pass while the declared result still fails at a farther independent boundary. - Evidence must reach the furthest independently failing boundary named by the Claim. A proxy may prove its own result, but it cannot prove a downstream state or effect merely by reporting success. - Every behavioral Claim-bearing Assertion requires a same-Check claim-local semantic Counterfactual with admitted baseline and mutated observations. Use `replace_json_value` or `replace_text` to alter only the asserted semantic field/fragment while preserving the production carrier; the designated affected Fact set must change, `preserved_assertions` and preserved Facts/liveness must remain unchanged, other changes must belong to the explicit allowed fan-out set and the obligation universe must remain identical. `replace_file` remains compatibility-only and cannot establish semantic binding; `remove_paths` remains for non-behavioral existence/structure claims. A machine-closing Check with no admitted entries fails with `counterfactual_admitted_observation_required`; it never skips impact validation. - Static Counterfactuals prove only the mutated structure object itself. Runtime production reachability requires `Harness mutation of a compiled production carrier → direct execution of the same Source-backed process product root → package-observed actual change`; baseline and mutated execution bind the same process-closure identity and neither closure contains Authority, verification or evidence input. Binding/path declarations, synthetic status, evidence output and generated verifier carrier do not establish causality. - Keep this risk-proportional and internal. Do not create an evidence matrix, product-effect taxonomy, universal restart/end-to-end suite or persistent review state. For semantic Product Conformance, require one separate read-only Global `conformance` Check only when `weak_observability` combines with multiple Stages or multiple required product runtime families. It starts from a required root product target, uses a Raw Execution identity independent of Outcome Checks and runs inside the existing Final Gate. It can carry machine `target_runtime` only for an admitted direct-process root; unsupported families remain blocking External Confirmation and the conformance Check cannot bypass that boundary. Single-Stage/single-family weak work keeps the existing same-Check sensitivity path and does not pay this extra runtime cost. ## Playwright Playwright is a diagnostic project verifier in the current observer slice, not machine Actual authority. `[ac:]` may still bind one declared AC per Test Instance for failure localization; ordinary tags are ignored and legacy `[]` binds only a declared key. Missing, skipped, flaky, unexpected, timed-out, interrupted, failed, multi-AC and duplicate-within-project cases remain failed diagnostics. The same AC across distinct projects aggregates all-of for that diagnostic Check, and aggregate status/count fields remain diagnostic-only. None can close a browser/UI machine Claim. Standard frozen Playwright content remains a stable diagnostic verifier input, not an admitted Actual source. Browser/UI machine obligations are External Confirmation in the current slice. Playwright Counterfactual output can localize repairs but cannot create machine acceptance, target-runtime authority or capability proof. ## Visual UI Evidence - A selected implementation handoff must already pass `ty-context design-resource preflight`, including frozen-Inspector Census, exact manifest↔handoff universe equality, complete per-resource/Fact Cell/Fact/proof closure, non-sampling/non-truncation and exact-target layout/pixel defaults. Preserve exact handoff `fact_refs`, every property-required Fact × verification-method obligation and its exact expectation. Under the current observer slice, layout, pixel, visual, interaction, motion, accessibility, browser/native/device, protected and tolerance/mask methods bind blocking External Confirmations; project `design_method`, `fact_results`, screenshots and Playwright attachments are repair diagnostics only. A future package-admitted adapter may reuse these identities, but no project verdict can pre-admit it. - Keep separately attributable evidence where geometry/pixel/token/content, interaction/state, motion/haptic/sound timeline, accessibility semantic/navigation/visual adaptation and asset integrity cannot falsifiably share one observation method. This preserves the complete selected-design proof universe; it does not admit those currently unsupported methods for machine completion. - Never accept an aggregate Boolean, screenshot pass or one `all-states` result in place of per-Fact authority. The expected target cannot be generated from the implementation under test. Plain static/process exact observations remain attributable through package extraction; protected and tolerance/mask obligations remain External Confirmation until an admitted adapter owns their Actual and comparison. - Keep `design_resource_integrity` and `design_implementation_conformance` distinct. Stable paths/hashes, provider/export success, manifest/registry membership and expected counts prove resource integrity; `visual_render` proves a current artifact exists. Neither proves the production implementation matches a selected target. - When external design resources are Source, account for every selected exact-target/constraint condition that the Contract explicitly adopts. Candidate comparison, a mutable provider link, extraction success, metadata-only output, resource digest or an isolated prototype run is authoring/integrity material and cannot become product acceptance. Resolve each acceptance-affecting fact through a typed locator plus immutable path/hash and declared target/condition applicability before Compile. Include the handoff and every source-profile entry/dependency in `verification_inputs`; unsupported method-specific design, interaction and target-runtime obligations remain separate blocking External Confirmations on the real production target. - The decoder may validate a project `design_conformance` record against its compiled target/Assertion/current Check target, conditions and artifacts for diagnostics, but that record is not admitted Actual or comparison authority in this slice. Missing or swapped bindings fail the diagnostic Check; a matching record still cannot machine-close visual conformance or make the implementation render its own comparison authority. - Playwright may exercise declared `ui_browser` visual ACs for diagnostic localization. Give each independently falsifiable AC one `[ac:]` Test Instance, but Playwright is not an admitted machine observer in this slice. Bind every browser visual obligation to blocking External Confirmation; a broad screenshot or one passing page case cannot waive an applicable cell. - Make the test environment deterministic enough for its claim: freeze the relevant browser/project, viewport, theme/mode, locale/timezone, font loading, fixtures/data and animation/motion policy in declared verifier inputs or configuration. - Any reviewed screenshot baseline that affects pass/fail must exist for the accepting Compile and be included in `verification_inputs`. Generated screenshots, diffs and reports are Artifacts and review material; they are not editable acceptance authority. Creating or replacing a baseline after Authority Lock is verifier-material revision and must never be silently auto-updated to make a failure pass. - Confirm that each baseline is a selected `exact-target` for the named surface/viewport/theme/state or implements a named `constraint`; an inspiration reference cannot become a fidelity oracle merely because it is available. The implementation's current screenshot is never its own target. - Screenshot comparison is diagnostic only under the current admitted boundary. Keep DOM/layout/accessibility/motion/responsive/input obligations distinct and blocking; one generic `design_conformance` record cannot erase Source Claims, verification methods or their External Confirmations. - Keep evidence aligned with stable surface/control/target keys. Visual similarity, interaction/navigation, validation/recovery, permission behavior, accessibility and target-runtime conformance are independently failing claims and need their own Assertions/capabilities when declared; one broad screenshot or UI pass cannot prove all Control fields. - Run diagnostic checks against production components or real product routes. Host `target_runtime` is available only when Harness directly executes the process product root; `interaction_trace` has no package derivation in the current slice and remains External Confirmation together with browser/native/device journeys. A detached kit/mock/deep-link harness cannot substitute for the production carrier or root journey. - Keep subjective visual quality and approval external. A new visual direction or baseline that needs human judgment remains an explicit external confirmation even when all machine checks pass. - `ui_browser` does not create machine proof in the current slice. Browser output cannot close native/mobile/desktop Claims; all such runtime reviews stay external until a package-owned adapter is admitted. - Preserve each handoff blocker's non-empty `required_capabilities`. A machine Claim closes it only when one admitted adapter for the exact target supplies every required observation; physical device, sensor, camera, orientation, haptic, screen-reader, pixel-density, safe-area and comparable observations are currently target-blocking External Confirmations and cannot be borrowed from a proxy. ## Symbolic Noninterference Evidence For every non-interference method, require a digest-identified frozen executable Oracle with the exact `symbolic_noninterference..` capability. Source proof must use the canonical package-owned restricted Source IR in the complete current Inspector inputs; package preflight binds its current bytes to target/certificate/Rule scope and derives and memoizes the static dependency DAG, exact predicate/axis-erased equivalence or every finite-domain evaluation itself. Submitted graph/predicate/evaluation/pass fields and the artifact are recomputable cache only, and the artifact is excluded from semantic inputs. Executable/CSS/implicit-DOM/template/dynamic/reflected/computed/unfrozen/external Source blocks; production remains limited to package-parsed static HTML plus inert JSON. Both sides bind implementation closure/version/capability, environment, exact current inputs, side snapshot, scopes, omitted axes, derived result, artifact and witness. When proofs exist, Source and production proof digests must match the current Final-Gate certificate expectation/result. Extraction outside admitted representations remains an explicit TCB boundary. ## Structured Evidence And Sensitivity Every machine claim-bearing `structured_json_v2` Check needs same-Check Claim-related Counterfactual sensitivity backed by the compiled admitted observer; the project payload alone never supplies Actual. Population declares a real `universe_binding_key`; every universe carrier is an owning-Check `input_path`, and package observation proves exact universe = eligible = observed plus valid exclusions by entity id. Population never substitutes for the claim-local narrow semantic witness and host-derived target-runtime liveness required by an admitted process behavioral Claim. Artifacts and another Check never substitute for sensitivity. Outcome Counterfactual V2 names an Outcome `binding_key`; Global Counterfactual V2 resolves an Outcome-owned `binding_ref`. A Counterfactual mutates only a package-proven subset of implementation carriers, never Source, Context, runners, verification inputs, expected authority, evidence, reports or status. Behavioral witnesses use claim-local `replace_json_value` or `replace_text`, list their designated affected Fact/Assertion set, preserved Fact/liveness set and allowed fan-out set, and require package observations to establish the exact permitted actual changes. An `existing` mutation target must exist at Preflight/Compile and the JSON pointer/text fragment must resolve uniquely. An exact `planned` target, process root or argv dependency may be absent until implementation but must exist at Final Gate; materializing the declared path preserves compiled/Authority identity, while later content changes stale targeted Progress. Artifacts remain review material. They do not prove Claim sensitivity by themselves.