# checkpoint-splits-atomic-update

> A checkpoint splits a declared ordinary Cell co-update across atomic units.

Canonical: https://nightshade.dicksonwu.xyz/rules/checkpoint-splits-atomic-update.html
Release: Nightshade 0.1.1 (v0.1.1)

| Field | Value |
| --- | --- |
| Rule ID | `checkpoint-splits-atomic-update` |
| Severity | low |
| Confidence | high |
| Maturity | experimental |
| Selection | Opt-in + policy |
| Policy intent | required |
| Default enabled | no |
| Category | Policy-dependent rules |
| Engine facts used | declared-atomic-update-group, complete-checkpoint-linkage, ordered-cell-writes |
| Release | v0.1.1 |

## Selection and scope

Not selected by default. Select it with `--detectors` or the `detectors` list in nightshade.json, and declare the matching application intent in `policies`. Selecting it alone does not supply that intent.

```sh
./.nightshade/node_modules/.bin/nightshade ./contracts --detectors checkpoint-splits-atomic-update
./.nightshade/node_modules/.bin/nightshade detector show checkpoint-splits-atomic-update
```

The first command runs only this rule; `--detectors` takes a comma-separated list. The second prints the rule's metadata from your installed version.

Severity is review priority. It does not express exploitability or impact. Confidence is detector metadata, not a probability. All built-in rules are experimental.

Compiler scope: the engine supports the pinned profiles 0.28.0, 0.29.0, 0.30.0, 0.31.1, 0.33.0-rc.2, 0.34.0, 0.35.0-rc.1 and 0.35.0, with ZKIR2 by default. Support for this rule can be narrower; the rule documentation below states any narrower scope.

## Corpus checks

Synthetic corpus checks for this rule in the 0.1.1 proof run. A check counts only with compiler acceptance and complete analysis.

| Positive detected | Corrected quiet | Lookalike quiet | Other negative quiet | Incomplete |
| ---: | ---: | ---: | ---: | ---: |
| 1/1 | 1/1 | 1/1 | 0/0 | 0 |

No deviations were recorded for this rule.

These are behavior checks on synthetic fixtures, not a precision or recall estimate. See [evaluation](https://nightshade.dicksonwu.xyz/evaluation.md#synthetic-corpus).

## Rule documentation

From https://github.com/DicksonWu654/nightshade/blob/v0.1.1/docs/detectors/checkpoint-splits-atomic-update.md at v0.1.1.

Availability: **opt-in**, with an explicit `atomicUpdates` application policy.
Severity **low**, confidence **high** for the linked write-occurrence observation.

Compact's canonical `kernel.checkpoint()` marks preceding execution as one atomic
unit and allows partial transaction failures across that boundary. This rule
reviews a declared group of ordinary Cell writes split across those units.
The reference establishes checkpoint semantics; it is not an independent bug
label or evidence that a particular application can fail its later segment.

### Example and review scenario

```compact
import CompactStandardLibrary;
export ledger primary: Field;
export ledger mirror: Field;
export circuit synchronize(value: Field): [] {
  primary = disclose(value);
  kernel.checkpoint();
  mirror = disclose(value);
}
```

```json
{
  "version": 1,
  "detectors": ["checkpoint-splits-atomic-update"],
  "policies": {
    "atomicUpdates": [{"circuit": "synchronize", "ledgers": ["primary", "mirror"]}]
  }
}
```

On a completely analyzed full history that writes every selected field, the rule
reports a linked checkpoint prefix which writes a nonempty proper subset.
It also reports mixed final write occurrences: both fields may have been written
before the boundary, while one receives another write afterward. Values can be
equal; the evidence concerns write occurrences, not numerical inequality.

An example can split related ordinary Cell updates around an explicit checkpoint.
The corrected form writes both snapshots before the boundary. A lookalike writes
both before the boundary and writes unrelated padding afterward.

### Recommendation and known intentional uses

Place coupled writes in the same atomic segment. Intentional staged commits are
normal: omit this policy when the application permits them. Review proof
constraints, privacy and transaction ordering before refactoring.

The group must resolve to two through sixteen distinct canonical ordinary Cells
on an exported entry circuit. Native ledger ADTs are outside this policy.
Projected field writes remain explicitly unavailable. An entry that never has a
complete all-field co-update is outside this rule's matching contract; the policy
does not require every entry invocation to write every field.

The observer links each full proof history directly to its own prefixes before
flat outcome deduplication, retaining repeated/helper/callback invocation sites.
Alternative histories remain separate evidence routes; their effects are never
combined to invent a co-update. Later immutable-input proof checks and saved
pre-boundary ledger-read checks retain the existing proof projection. Unprovable
continuations supply no prefix evidence. Namesakes and unreached boundaries do
not count.

Unsupported effects, incomplete baseline entries, unavailable or truncated links,
unsupported observation modes and exhausted shared step/path/value allowances
remain rule-scoped incomplete. The baseline and other rules retain their separate
completion. No symbolic execution, cross-entry invariant proof, actual partial
failure, permanent loss or deployed impact is established.

## Suppress a match

If a match is intentional, suppress it on the line before with the exact rule ID and a reason of at least eight characters:

```compact
// nightshade-disable-next-line checkpoint-splits-atomic-update -- Reason this match is intentional
```

Diagnostics cannot be suppressed, and an unmatched directive for a selected rule makes analysis incomplete. See [configuration](https://nightshade.dicksonwu.xyz/configuration.md#suppress-an-intentional-match) for fingerprint suppressions and baselines.

## References

- [Rule source document at v0.1.1](https://github.com/DicksonWu654/nightshade/blob/v0.1.1/docs/detectors/checkpoint-splits-atomic-update.md)
- [Catalog entry in rules.json](https://nightshade.dicksonwu.xyz/rules.json)
- [All rules](https://nightshade.dicksonwu.xyz/rules.md#policy-dependent-rules)
- [Limitations](https://nightshade.dicksonwu.xyz/limitations.md)