Deterministic property assertions

Purpose and scope

Makes it explicit whether a quantum test checks an analytic probability or an estimate from finitely many measurements. It also defines the meaning of range and state-equivalence assertions.

Core design rules

• Sampled probability assertions bind shot count, seed and tolerance to an explicit contract.
• A closed physical or application range can be expressed by one range assertion.
• State equivalence states explicitly whether global phase participates in the comparison.

Example from the original

This example illustrates the design recorded in the original. It is not by itself a claim of executable or stable support; check required options and the current version.

module property_assertions;
@seed(17);
@shots(256);

fn main() {
  property "phase-safe plus state" {
    forall theta in 0 .. PI step PI / 2 {
      let q: QReg<1> = qreg[1];
      GPhase(theta);
      H(q[0]);

      assert probability(|0>) ~= 0.5 tolerance 0.1;
      assert expectation Z(q[0]) ~= 0 tolerance 0.2;
      assert expectation Z(q[0]) in [-1, 1];
      assert equivalent("plus") up_to_phase;
    }
  }
  return 0;
}

Limits and interpretation

• A finite-shot estimate is not reported as an exact analytic value.
• An experimental assertion result is not evidence of device accuracy or quantum advantage.

Status and implementation boundary

The source defines a runtime-experimental contract and its diagnostics. Retain source, seed, shot count and negotiated options together when recording execution evidence.