Raptor/invariants/GRAPH_COMPUTE_BATCH_INVARIANT.md

# Graph Compute Batch Physical-Fragment Invariant

## Status

This document is **normative** for Raptor's Spatial graph IR.

Every developer or coding agent modifying Spatial graph construction, graph
verification, Blueprint handling, or `MergeComputeNodes` must read this file
after `README.md` and `AGENTS.md`.

`AGENTS.md` must contain this instruction:

```text
* Always read the full invariants/GRAPH_COMPUTE_BATCH_INVARIANT.md before modifying Spatial graph IR, Blueprint handling, or MergeComputeNodes.
```

## Scope

This invariant applies to:

- `spat.graph_compute_batch`;
- graph-level values produced by it;
- `tensor.parallel_insert_slice` operations that publish its lane results;
- `spat.blueprint` operations that describe logical reconstruction;
- graph analyses and transformations that consume those values;
- the graph-to-scheduled transition in `MergeComputeNodes`.

It does **not** impose the same representation on:

- `spat.scheduled_compute`;
- `spat.scheduled_compute_batch`;
- `pim.core` or `pim.core_batch`;
- values whose cross-core movement is already represented by explicit
  `spat.channel_send` and `spat.channel_receive` operations.

Scheduled IR represents execution on assigned cores. Communication and value
availability there are defined by local SSA forwarding and explicit
send/receive operations, not by the graph physical-fragment invariant.

## Core invariant

For every result of a `spat.graph_compute_batch` with `N` graph lanes:

1. Every graph lane produces exactly one fragment for that result.
2. All lanes produce fragments with the same exact ranked tensor type `F`.
3. The graph result is a physical collection of those fragments with type:

   ```text
   tensor<N x shape(F) x element-type(F)>
   ```

   Conceptually, the result is `N × F`: one leading physical fragment-slot
   dimension followed by the complete per-lane fragment shape.
4. Physical slot `i` identifies a fragment publication. It does not, by itself,
   identify a row, column, channel, tile, or any other logical tensor position.
5. The result type carries no logical reconstruction order.

The leading dimension is therefore a **physical fragment-slot dimension**, not
a logical tensor dimension.

## Per-lane computation is unrestricted

The invariant constrains the published result representation, not what a lane
may compute.

A graph lane may:

- read several input slices;
- perform reductions;
- add or combine multiple columns;
- execute matrix/vector operations;
- produce a fragment that corresponds to any logical region;
- participate in a multi-stage or logarithmic reduction tree implemented by
  following `spat.graph_compute` or `spat.graph_compute_batch` operations.

Arithmetic combination is graph computation. `spat.blueprint` is not an
arithmetic reduction operation.

### Example: `16×4 -> 16×2`

Two graph lanes may compute:

```text
lane 0: input[:, 0] + input[:, 1] -> tensor<16x1>
lane 1: input[:, 2] + input[:, 3] -> tensor<16x1>
```

The physical graph result is:

```text
tensor<2x16x1>
```

A Blueprint then maps:

```text
physical slot 0 -> logical output[:, 0:1]
physical slot 1 -> logical output[:, 1:2]
```

and describes the logical result `tensor<16x2>`.

For a larger reduction, following graph compute batches may reduce fragments in
`ceil(log2(N))` stages. Every intermediate batch still publishes a physical
`batch × fragment` collection.

## Physical publication inside `spat.graph_compute_batch`

The batch body must publish each lane's fragment into the physical result.

For one result with fragment type `F`, the corresponding
`tensor.parallel_insert_slice` must insert the fragment into one slot of the
physical `N × F` destination:

```text
physical offsets = [slot, 0, 0, ...]
physical sizes   = [1, shape(F)...]
physical strides = [1, 1, 1, ...]
```

The slot may be the graph lane directly or a statically analyzable permutation
of it. The insertion describes physical slot placement only. It must not use a
logical output dimension as the physical batch dimension.

For each graph result, the body must contain exactly one physical publication
per graph lane. Since the body executes once per lane, this normally means one
`tensor.parallel_insert_slice` operation targeting that result.

## Logical reconstruction

Logical reconstruction is separate from physical publication.

The reconstruction descriptor defines, for every physical fragment slot:

- which physical batch operand owns the fragment;
- which physical slot contains it;
- its destination offsets in the logical tensor;
- its destination sizes;
- its destination strides;
- coverage and conflict policy where relevant.

The persistent owner of this information is `spat.blueprint` or an equivalent
explicit graph-level reconstruction operation.

A logical consumer must not infer reconstruction from the physical tensor type
or assume that physical slot order equals logical order.

The logical mapping may be arbitrary. For example:

```text
physical slot 0 -> logical row 13
physical slot 1 -> logical row 4
physical slot 2 -> logical row 10
```

The physical result remains a regular `batch × fragment` tensor.

## Relationship between `parallel_insert_slice` and Blueprint

During graph construction, an algorithm may naturally describe logical
placement with `tensor.parallel_insert_slice` geometry. Before the graph is in
its canonical form:

1. that geometry must be separated from physical fragment publication;
2. the graph batch result must be normalized to `N × F`;
3. the logical insertion geometry must be transferred to a persistent
   `spat.blueprint` reconstruction descriptor.

After normalization:

- `parallel_insert_slice` inside `spat.graph_compute_batch` publishes into
  physical fragment slots;
- `spat.blueprint` describes reconstruction into the logical tensor.

The original graph operation may be erased only after all reconstruction
information needed by later stages has a persistent owner.

## Blueprint semantics

Blueprint is placement/reconstruction metadata. It may:

- concatenate fragments;
- reorder fragments;
- insert fragments into arbitrary disjoint logical regions;
- describe complete or partial logical coverage;
- expose a logical tensor view when materialization is required.

Blueprint must not silently perform arithmetic such as addition, multiplication,
maximum, or reduction. Such transformations must be represented by following
`spat.graph_compute` or `spat.graph_compute_batch` operations.

A Blueprint consuming a physical fragment batch must explicitly identify the
physical source slot for every logical fragment. It must not derive that slot
from operand order unless that convention is explicitly represented and
verified.

## Multiple results

A `spat.graph_compute_batch` may have several results.

For each result `r` independently:

- every lane produces one fragment of type `F_r`;
- the graph result type is `N × F_r`;
- its physical publication and logical reconstruction descriptor are verified
  independently.

Different results may use different fragment shapes.

## Graph consumers

A graph consumer of a batch result may:

1. consume fragments directly as physical fragments;
2. select one or more physical slots in a `spat.deferred_communication` body;
3. use a Blueprint to obtain or describe a logical reconstruction;
4. feed fragments to following graph computes or graph compute batches.

A consumer must not treat the leading physical slot dimension as a logical
model dimension unless an explicit graph operation intentionally performs such
an interpretation.

All constant selection, slicing, reshaping, concatenation, and other
compile-time shaping needed for a scheduled consumer must be encoded inside the
corresponding `spat.deferred_communication` body. Phase 2 must not recover
missing graph semantics by inspecting consumers after the deferred operation.

## Graph lane, scheduled lane, and physical core are different identities

These concepts must never be conflated:

- **graph lane**: the lane of the original `spat.graph_compute_batch`;
- **physical fragment slot**: the slot in the graph batch result;
- **scheduled lane**: one lane of a `spat.scheduled_compute_batch` equivalence
  class;
- **physical core**: the core selected by PEFT.

The graph batch body or its Blueprint defines graph-lane-to-fragment-slot and
fragment-slot-to-logical-region mappings.

PEFT defines graph-instance-to-core placement.

Scheduled communication defines how values move between cores.

## Scheduled IR exclusion

Do not add a verifier requiring `spat.scheduled_compute_batch` results to have
`laneCount` as their first dimension.

Do not rewrite scheduled values merely to resemble graph physical fragment
collections.

When lowering graph IR into scheduled IR:

- resolve graph fragments and reconstruction metadata before erasing their
  graph owners;
- create local forwarding or `spat.channel_send`/`spat.channel_receive` for
  cross-core dependencies;
- allow scheduled result representation to follow the scheduled IR contract;
- preserve numerical and deadlock correctness.

The graph invariant is an input contract for scheduling, not a scheduled-value
layout contract.

## Required verifier properties

`spat.graph_compute_batch` verification must establish, for every result:

1. the result is a static or otherwise supported ranked tensor;
2. result rank is exactly `fragment rank + 1`;
3. result dimension 0 equals `laneCount`;
4. every lane publication source has the same exact fragment type;
5. the physical insertion targets the corresponding result block argument;
6. physical insertion offsets have the fragment slot in dimension 0;
7. all remaining physical offsets are zero;
8. physical sizes are `[1] + fragment shape`;
9. physical strides are unit;
10. exactly one publication is defined for each graph result in the per-lane
    body.

These checks apply only to `spat.graph_compute_batch`, not to
`spat.scheduled_compute_batch`.

Blueprint verification must establish that every logical reconstruction entry:

- references an existing physical batch operand;
- references a valid physical fragment slot;
- maps a fragment compatible with the declared logical slice;
- stays within logical bounds;
- follows the declared conflict and coverage policies.

## Invalid representations

The following are invariant violations.

### Logical aggregate returned directly by graph batch

```text
laneCount = 16
result     = tensor<1x4x16x16>
```

with each lane inserting into logical dimension 2.

This is a logical assembly masquerading as a graph batch result. The graph
result must instead be `16 × per-row-fragment`, and a Blueprint must describe
placement into `tensor<1x4x16x16>`.

### Physical storage derived from logical destination shape

Code equivalent to:

```cpp
shape = logicalDestinationType.getShape();
shape[logicalInsertionDimension] = laneCount;
```

is invalid.

Physical graph storage must be derived from the per-lane fragment type:

```cpp
physicalShape = [laneCount] + fragmentType.getShape();
```

### Reconstruction inferred from result type

It is invalid to assume that physical slot `i` belongs at logical offset `i`.
The Blueprint or another explicit reconstruction descriptor must state the
mapping.

### Blueprint used for arithmetic

It is invalid to encode `fragment0 + fragment1` as Blueprint reconstruction.
Create a following graph compute or graph compute batch for the addition.

## Ownership

- ONNX-to-Spatial lowering owns creation of valid graph fragment batches.
- Graph canonicalization owns normalization of temporary logical-assembly forms
  into physical graph batches plus Blueprints.
- `spat.graph_compute_batch` verifier rejects invalid physical publications.
- `spat.blueprint` owns persistent logical reconstruction metadata.
- Deferred communication Phase 1 owns complete consumer-side constant shaping.
- Merge scheduling consumes this graph contract and introduces explicit
  communication.
- Scheduled IR verifiers validate scheduled execution and communication, not
  the graph fragment representation.

## No repair downstream

If graph IR violates this invariant, fix the graph producer or graph
canonicalization.

Do not repair an invalid graph batch by:

- guessing a lane dimension in `MergeComputeNodes`;
- deriving physical storage from a logical destination tensor;
- inspecting deferred-result users;
- reconstructing omitted Blueprint data after graph erasure;
- weakening graph verifiers;
- imposing the graph representation on scheduled operations.