Status: runtime experimental
Contract: 0.2.0-runtime-experimental
Feature flag: experimental.propertyAssertions=true
Stable 0.1 default: disabled
Owners: language and runtime

Problem

N/M 0.1 can expand property/forall blocks and evaluate threshold assertions, but it does not express the three contracts needed for repeatable quantum tests:

finite-shot values need an explicit tolerance and deterministic sampling;
an observable often needs to remain inside a closed physical or application range;
state equivalence needs to state whether global phase is observable.

Without those contracts, a test can silently use an analytic value when the author intended shots, encode a range as two unrelated assertions, or depend on implicit fidelity behavior.

Proposed syntax

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;
}

The three new forms are also valid in ordinary executable, test, observe, and snapshot scopes wherever the corresponding legacy assertion is valid. Property blocks remain the primary counterexample-producing carrier.

Normative semantics

Finite-shot tolerance

~= is inclusive:

text

pass iff abs(sampledValue - expected) <= tolerance + 1e-12

Both @seed(unsignedInteger) and @shots(positiveInteger) are mandatory.
Probability assertions draw shots Bernoulli samples from the analytic basis-state probability.
Expectation assertions reuse N/M's finite-shot Pauli estimator and report analytic value, sampled value, standard error, and shot count.
0 < tolerance <= 1.
Expected probability remains in [0, 1].
Missing deterministic metadata is a parse error, not an implicit fallback to analytic execution.

Property case seed

When the feature is enabled and a program declares @seed, each forall case receives its own random stream:

text

fnv1a32(
  uint32(baseSeed) + NUL +
  propertyName + NUL +
  parameterName + NUL +
  canonicalCaseValue
)

canonicalCaseValue is rounded to 12 decimal places, parsed back as a number, and rendered in base-10 form. The UTF-8 bytes are hashed with FNV-1a 32. The derived unsigned integer seeds mulberry32, matching N/M's existing seeded runtime.

This makes a case independent of the execution and insertion order of other cases. The experimental property stream is restored after the block, so property sampling does not consume the enclosing program's seeded random stream. Stable 0.1 execution keeps its previous random-stream behavior when the feature flag is absent.

Observable range

in [minimum, maximum] is an inclusive, analytic assertion:

text

pass iff actual + 1e-9 >= minimum and actual - 1e-9 <= maximum

minimum <= maximum.
Bounds must be finite and their absolute value cannot exceed 1_000_000.
The full weighted observable is evaluated once; the range does not apply independently to each Pauli term.
@shots does not change this form. Authors who need sampled behavior use ~= ... tolerance ....

Equivalent up to global phase

up_to_phase compares the prepared state with a named reference by state fidelity. Fidelity is the squared magnitude of the complex inner product, so a global factor exp(iφ) does not affect the result.

text

pass iff fidelity >= 1 - 1e-9

The AST and IR record phasePolicy: "global". Legacy assert equivalent("target"); remains source-compatible and retains its existing fidelity behavior, but does not claim the explicit 0.2 policy field.

Runtime evidence

Every experimental property case may expose:

its derived unsigned seed;
ordered assertion evidence;
sampled and analytic values, tolerance, shot count, and standard error;
inclusive range bounds;
phasePolicy: "global" and fidelity;
pass/fail state and diagnostic codes.

Property execution stops at the first failing case and retains that value as failedValue. Evidence collected before the failure remains available. This is intentional counterexample behavior, not exhaustive failure collection.

AST and IR

NMProbabilityAssertion.operator and NMExpectationAssertion.operator add ~= and an optional tolerance.
Observable ranges use the distinct assertExpectationRange statement with minimum and maximum.
NMEquivalentAssertion adds optional phasePolicy: "global".
NMProgram.propertyAssertions records the experimental contract version.
JSON IR and the strict QASM3 sidecar preserve all fields; unknown fields and unknown statement kinds remain fail-closed under the sidecar contract.

Diagnostics

Table 1
Code	Meaning
`NM-PARSE-056`	New syntax used without the feature flag
`NM-PARSE-057`	Malformed tolerance or phase assertion
`NM-PARSE-058`	`@seed` or `@shots` missing for a finite-shot assertion
`NM-PARSE-059`	Non-finite, oversized, or reversed observable range
`NM-ASSERT-007`	Finite-shot probability/expectation is outside tolerance
`NM-ASSERT-008`	Analytic observable is outside the inclusive range
`NM-ASSERT-009`	Named state is not equivalent up to global phase

Unsupported reference targets continue to use the existing NM-RUNTIME-024/025 family because target resolution fails before comparison.

Compatibility and rollout

The stable parser default rejects only the new spellings and does not change existing 0.1 ASTs or execution.
Existing comparison operators, assert equivalent(...), property expansion, and counterexample fields remain unchanged.
Feature negotiation must be explicit in Core callers, CLI, Language Server, VS Code, and browser surfaces.
Promotion requires parser/runtime/IR/QASM conformance, seeded fixtures on Windows and Linux, CLI/LSP parity, EN/TR documentation, package artifact validation, and production smoke evidence.

The G6 promotion ratchet executes the maximum 32-case carrier with @shots(100000) and all four assertion forms. Five packed-Core samples must retain byte-identical seeded property evidence and remain within the versioned p95/RSS budgets in benchmarks/nm-property-assertions-baseline.json. CI runs this check on Windows and Linux with Node 20 and 22; a local pass does not close the remote gate.

Limits and non-goals

Property expansion remains capped at 32 cases.
This RFC does not add arbitrary generators, shrinking, confidence intervals, hypothesis tests, per-assertion shot counts, density-matrix equivalence, local-phase equivalence, or mixed-state trace distance.
FNV-1a is a reproducibility hash, not a security primitive.
Exact exhaustive failure collection is deferred; the first counterexample policy remains bounded and predictable.