# Fixed contracts

Two assertions whose requirement is fixed by a named contract and decided in exact rational arithmetic.

Canonical page: https://www.geospec.xyz/docs/reference/contracts

These two assertions take no arguments. Each checks one fixed, named contract over a narrow admitted domain in exact rational arithmetic, and records the plan hash and the checker's source hash in its evidence (`planHash`, `verifierSourceHash`). A subject outside the domain refuses.

`plate` is the site's demo model; `gauge` and `gapBoxes` are repository fixtures: a STEP file whose declaration allows 0.95 to 1.05 mm between two parallel faces, and two 10 mm boxes 2 mm apart. Python adds `rational_plate`, the repository fixture `rational-plate.json` admitted through `engine.ingest_subject`; `load_model` reads STEP and glTF only, and no loader in `geospec@beta` admits a `rational-plate` subject. Python matchers are snake\_case. A failed or refused call throws `GeoSpecAssertionError` in TypeScript and raises it in Python. Refusal codes add to the [common refusals](https://www.geospec.xyz/docs/reference/overview.mdx#common-refusals).

**TypeScript**

```ts title="check.ts"
import { readFile } from 'node:fs/promises';
import { expectGeo } from 'geospec';
import { createModelLoader } from 'geospec/model';
import { Engine } from 'geospec-engine/node';

const engine = new Engine();
const loadModel = createModelLoader({
  engine,
  readSource: async (source) => new Uint8Array(await readFile(source as string)),
});
const plate = await loadModel({ source: 'plate-with-through-bore.step', format: 'step' });
const gauge = await loadModel({
  source: 'packages/geospec-engine/native/occt/rust/tests/fixtures/parallel-plane-distance-source.step',
  format: 'step',
});
const gapBoxes = await loadModel({
  source: 'packages/geospec-engine/native/occt/rust/tests/fixtures/box-clearance/two-mm.step',
  format: 'step',
});
```

**Python**

```python title="check.py"
from pathlib import Path

from geospec import GeoSpecEngine, expect_geo, load_model

with GeoSpecEngine(model_root=".") as engine:
    plate = load_model(file="plate-with-through-bore.step", format="step")
    gauge = load_model(
        file="packages/geospec-engine/native/occt/rust/tests/fixtures/parallel-plane-distance-source.step",
        format="step",
    )
    gap_boxes = load_model(
        file="packages/geospec-engine/native/occt/rust/tests/fixtures/box-clearance/two-mm.step",
        format="step",
    )
    rational_plate = engine.ingest_subject(
        Path("packages/geospec-engine/bench/fixtures/performance-lab/rational-plate.json").read_bytes(),
        format="rational-plate", coordinate_system="z-up", source_unit="mm", output_unit="mm",
    )
```

## toSatisfyRationalPlate [#tosatisfyrationalplate]

Asserts that a rational plate subject satisfies the contract `geospec.plate-two-windows/v1`: a 10 × 10 × 2 mm plate with two 1 mm square through-windows.

**Signature**

**TypeScript**

```ts
expectGeo(part).toSatisfyRationalPlate(): GeoSpecAssertion
```

**Python**

```python
expect_geo(part).to_satisfy_rational_plate() -> GeoSpecAssertionReport
```

**Fields**

None. The contract holds when all four predicates hold:

| Predicate | Requirement                                                      |
| --------- | ---------------------------------------------------------------- |
| P1        | The plate spans `[0, 0, 0]` to `[10, 10, 2]` exactly             |
| P2        | The material volume is exactly 196 mm³                           |
| P3        | No material lies in window A, `[1.5, 1.5, 0]` to `[2.5, 2.5, 2]` |
| P4        | No material lies in window B, `[7.5, 7.5, 0]` to `[8.5, 8.5, 2]` |

**Admitted geometry**

* Only a `rational-plate` subject, admitted in a z-up, millimetre frame with no resources; the Python setup above shows the call. Its source is canonical JSON with `schema: 'geospec.rational-orthogonal-plate/v1'`, `unit: 'mm'`, `frame: 'artifact-xyz'`, a `plate` box and up to 16 `windows` boxes. Coordinates are reduced fractions spelt `"n/d"`, such as `"3/2"`.
* Every window runs the plate's full height, lies strictly inside it in x and y, and is separated from every other window in x or y.
* Source within 64 KiB and integers below 2⁶³; `ingest_subject` rejects more as a `ProtocolError`, before any claim.
* A STEP, mesh or glTF subject refuses. The engine does not extract a plate from other geometry.

**Refusal codes**

* `GEOSPEC_UNSUPPORTED_EVIDENCE`: the subject is not a rational plate, or a window breaks the layout rules.
* `GEOSPEC_ANALYSIS_LIMIT`: the retained plate geometry exceeds the contract's fixed capacity, which no host limit raises, or the engine's `maxMeshBytes`.

A failed claim carries `GEOSPEC_RATIONAL_PLATE_MISMATCH`, listing the predicates that do not hold.

**Examples**

**TypeScript**

```ts
// refused (GEOSPEC_UNSUPPORTED_EVIDENCE): plate, a STEP subject is outside geospec.rational-orthogonal-plate/v1
expectGeo(plate).toSatisfyRationalPlate();
```

The passed case is Python only: no loader in geospec\@beta admits `rational_plate`.

**Python**

```python
# passed: rational_plate, material volume 196/1 with both windows clear
expect_geo(rational_plate).to_satisfy_rational_plate()
# refused (GEOSPEC_UNSUPPORTED_EVIDENCE): plate, a STEP subject is outside geospec.rational-orthogonal-plate/v1
expect_geo(plate).to_satisfy_rational_plate()
```

## toSatisfyParallelPlaneDistance [#tosatisfyparallelplanedistance]

Asserts that the distance between two parallel planar faces of a STEP file lies within the limits the file itself declares.

**Signature**

**TypeScript**

```ts
expectGeo(part).toSatisfyParallelPlaneDistance(): GeoSpecAssertion
```

**Python**

```python
expect_geo(part).to_satisfy_parallel_plane_distance() -> GeoSpecAssertionReport
```

**Fields**

None. The file carries the requirement: exactly one `DIMENSIONAL_LOCATION` named `geospec.pmi.parallel-plane-distance/v1`, whose two `SHAPE_ASPECT`s identify the faces, with a `lower limit` and an `upper limit` length in the unit the file declares. The engine reads both planes from the STEP source, places them, and checks `lower <= distance <= upper` exactly.

**Admitted geometry**

* A STEP file of at most 1 MiB with exact BRep faces and one such declaration.
* The two aspects name distinct planar faces or occurrence routes, and the placed planes are exactly parallel.
* Source limits: 8,192 entity records, 32 list items and 32 levels of occurrence route.

**Refusal codes**

* `GEOSPEC_CERTIFICATE_UNVERIFIED`: the subject has no retained STEP source within 1 MiB, or the declaration is missing, repeated or malformed. The diagnostic's `details.reason` is `unsupported-source` or `invalid-input`.
* `GEOSPEC_UNSUPPORTED_EVIDENCE`: the placed planes are not parallel, or the source is otherwise outside the proof's domain. `details.reason` is `unsupported-domain`, and `details.applicability.condition` names the condition, such as `parallel-source-planes`.
* `GEOSPEC_ANALYSIS_LIMIT`: a source limit above was reached. `details.reason` is `resource-limit`, with `limit` and `required`; the limits are fixed by the proof profile, so no host limit raises them.

A failed claim carries `GEOSPEC_PARALLEL_PLANE_DISTANCE_MISMATCH`.

**Examples**

**TypeScript**

```ts
// passed: gauge, measured.satisfiesSourceInterval is true for the declared 0.95 to 1.05 mm band
expectGeo(gauge).toSatisfyParallelPlaneDistance();
// refused (GEOSPEC_CERTIFICATE_UNVERIFIED): gapBoxes, no declaration; details.reason is unsupported-source
expectGeo(gapBoxes).toSatisfyParallelPlaneDistance();
```

**Python**

```python
# passed: gauge, measured.satisfiesSourceInterval is true for the declared 0.95 to 1.05 mm band
expect_geo(gauge).to_satisfy_parallel_plane_distance()
# refused (GEOSPEC_CERTIFICATE_UNVERIFIED): gap_boxes, no declaration; details.reason is unsupported-source
expect_geo(gap_boxes).to_satisfy_parallel_plane_distance()
```