Verification Bridges

C3-VERIFY-001 — Exact subjects and semantic adequacy

A verification subject is an exact checked definition, implementation, model, or plan closure under a named edition and semantic profile. A bridge binds: the subject’s actual preimage, its contract and implementation identities, the observation mapping, the logical operational/model semantics, its environment and assumptions, and the exact obligations derived from them. All referenced records must resolve and check; a matching digest without the referenced subject or model is insufficient for verification admission.

The logical model must represent the relevant observable behavior, including errors, termination, effects, nondeterminism, and numeric policy where present. The bridge must account for every applicable contract clause. Omitting a required observation or replacing the pinned challenge with an easier theorem is rejection, even if the replacement has a valid proof.

Kernel checking establishes facts about this model. Correspondence between a real implementation and its encoded model requires either a checked refinement certificate or a named, policy-admitted encoder/backend trust boundary. The receipt must distinguish these cases. A hash of an encoder is identification, not proof of its adequacy. A bridge that is unavailable is unsupported; it must not manufacture an axiom asserting the missing correspondence.

The model record carries checked data types Input, Trace, Outcome, and Observation. In its exact environment, semantics must have type forall (i:Input) (t:Trace) (o:Outcome) -> Prop, and observations must have type forall (t:Trace) (o:Outcome) -> Observation. These are relations and functions over declared logical types, not calls to the actual subject. The declared trace/outcome types must represent every behavior relevant to the claim, including divergence or infinite traces for unbounded progress claims. For example an infinite trace may be modeled as a Nat-indexed function; no coinductive kernel primitive is implied. The adequacy certificate or named trust boundary covers the completeness of this encoding.

A checked contract view supplies its logical input/observation types and pre/post relations in that same environment. The bridge’s observation map has type model.Observation -> contract.Observation; its input representation is part of the subject’s checked contract binding. The loader rejects a contract format without such a checked view. Bounded claims must expose their input/horizon restrictions in the actual quantified statement, not merely in an evidence label. No free-form numeric-profile string establishes the connection to the subject’s actual arithmetic.

C3-VERIFY-002 — Claims and composition

Use an explicit behavior relation Exec(subject,input,trace,outcome) and observation map Obs(trace,outcome). A partial-correctness obligation states that every admitted terminating execution satisfying its precondition has the required observed postcondition. It does not assert that an execution terminates. A total-correctness obligation also proves termination/progress under the declared scheduling and environment assumptions.

Refinement requires inclusion of candidate observations in those permitted by the original contract for every admitted input/environment. Exact equivalence requires both directions. Bounded exploration quantifies only over its declared bound. An invariant proof requires initialization and preservation over all admitted transitions; a liveness proof must disclose fairness assumptions. A finite trace or finite horizon cannot substitute for either unbounded judgment.

Composition substitutes proved conclusions into matching premises with checked types, state ownership, observation domains, and assumptions. Component-wise success alone does not establish an aggregate theorem: interference, ordering, and boundary obligations are part of the composed subject. Proofs convey no permission to execute the subject.

C3-VERIFY-003 — Algorithm model

The Algorithm model includes checked control flow, values, local/heap ownership, declared effects, normal and error returns, traps, and divergence. Preconditions and postconditions refer to specified entry/exit snapshots, not mutable aliases to a later state. Assertions over mathematical integers require a checked encoding to the actual machine width and overflow policy. Modular arithmetic, checked overflow, division by zero, and signedness are distinct behaviors.

A partial proof for a looping program must not satisfy a total obligation. Ownership safety does not imply functional correctness. Interpreted, portable native, JIT, and AOT realizations share a contract only through an admitted semantics-preservation relation; source proofs are not automatically proofs of native machine code. These new rules do not change old checked, verified, or trusted contract modes or relabel their existing evidence.

C3-VERIFY-004 — Compute model

The Compute subject binds tensor shapes, element types, strides/layout, views, aliasing and lifetime constraints, index spaces, kernel operations, and the execution/numeric profile. Bounds, shape compatibility, and reduction domains are quantified explicitly, including zero-sized axes and boundary indices. Parallel correctness quantifies over the permitted schedule; race freedom and reduction ordering require their own obligations.

Exact integer, strict floating-point, relaxed floating-point, and real-number models are different. An approximate result must name its norm, tolerance, input domain, and permitted nondeterminism; it is not a proof of exact equality. Proofs of real algebra alone cannot justify reassociation of machine floats.

C3-VERIFY-005 — State model

The State model binds schema, invariant, transaction relation, atomic commit point, isolation/conflict policy, graph schedule, delays, and externally observable committed outputs. Invariant preservation consists of a proof for initial states and each admitted transaction/commit transition, including abort paths and concurrent conflicts under the selected isolation model.

Outbox effects are separate post-commit actions. A logical atomic commit must not imply atomicity with a network or device effect. A changed schema or transaction relation requires refreshed evidence or a checked migration relation covering preserved invariants.

C3-VERIFY-006 — Flow model

The Flow subject includes definition/code epochs, activity boundaries, durable history schema, journal guarantees, replay and recovery rules, retries, compensation, checkpoints, and observations. Replay equivalence compares recorded activity results under the exact admitted history/code relation; it does not re-execute an activity to obtain a favorable result.

Safety and progress are separate. Progress must disclose scheduler, storage, and external-service assumptions. Compensation is a declared subsequent action, not universal rollback. A proof of a workflow’s journal protocol must preserve indeterminate outcomes for crashes between irreversible external effects and durable receipts unless the named external protocol resolves them.

C3-VERIFY-007 — Optimize model

The Optimize model binds the candidate space and its order, constraints, signals, numeric/tie policy, evaluator semantics, budget accounting, and evidence acceptance policy. Proving candidate admissibility does not prove optimality. Optimality must quantify over the whole declared space or clearly state its finite/approximate/search-bound restriction.

No test score, solver status, agent confidence, or favorable sample is a kernel certificate. An external solver may emit a certificate that is translated to checked terms; otherwise its result retains its separate evidence kind and trust boundary. Optimize signals remain pure and cannot invoke Intent.

C3-VERIFY-008 — Hardware model

The Hardware model binds ports, hierarchy, logic domain, state, clocks/resets, CDC bridges, timing laws, simultaneous-update and scheduling semantics, environment assumptions, and observation horizon. Two-state reasoning cannot silently discharge four-state X/Z obligations. Functional equivalence, timing, reset/CDC safety, and physical implementation constraints are separate claims.

Reference simulation establishes only its recorded finite observations. RTL lowering, synthesis, place-and-route, and device execution require separate refinement/trust links. Digital CDC laws do not constitute a theorem about analog metastability in an actual device.

C3-VERIFY-009 — Physics model

The Physics subject binds quantities/units/frames, fields, geometry, equations, constitutive and boundary/initial conditions, regularity, discretization, analysis, and the exact mathematical number system. Well-posedness, existence, uniqueness, conservation, and error estimates are independent obligations; one does not imply the others.

A theorem about a continuum equation is not automatically a theorem about a discretized solver. A discretization proof must bind its mesh, transfer law, norm and convergence assumptions. Measurement/calibration and model fidelity remain empirical evidence with provenance and uncertainty, even when the mathematical model is fully proved. No proof receipt means an idea is physically real without this separate connection to observation.

C3-VERIFY-010 — Admission and dependency changes

A proof-required obligation passes only after checking its exact expected statement, allowed assumptions, semantic bindings, and required backend links. All applicable obligations must pass. Missing proof, unsupported semantics, resource exhaustion, and counterexample are distinct outcomes. Policies may permit weaker evidence for other obligations, but must not present it as proof.

Changing the body, contract, model, observation map, or assumption environment invalidates affected verification links. Unchanged independent theorems remain mathematically checked. Reuse requires exact dependency validation or a checked transport/refinement certificate; cache presence or approval alone is not reuse authority. Canonical dependency rules are in logical ZLM4.