# nullifier-check-without-insert

> Required collection absence lacks a definite surviving insertion on a state-changing history.

Canonical: https://nightshade.dicksonwu.xyz/rules/nullifier-check-without-insert.html
Release: Nightshade 0.1.1 (v0.1.1)

| Field | Value |
| --- | --- |
| Rule ID | `nullifier-check-without-insert` |
| Severity | medium |
| Confidence | low |
| Maturity | experimental |
| Selection | Opt-in |
| Policy intent | not required |
| Default enabled | no |
| Category | Other active opt-ins / Source structure and validation |
| Engine facts used | collection-observations, successful-predicates, state-writes, completed-entries |
| Release | v0.1.1 |

## Selection and scope

Not selected by default. Select it with `--detectors` or the `detectors` list in nightshade.json. Either one replaces profile selection, so list every rule you want.

```sh
./.nightshade/node_modules/.bin/nightshade ./contracts --detectors nullifier-check-without-insert
./.nightshade/node_modules/.bin/nightshade detector show nullifier-check-without-insert
```

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.

## Verified example

Synthetic example from the proof run of the released CLI. The circuit checks that an identifier is unused but never inserts it into the used set. Full example: https://nightshade.dicksonwu.xyz/examples.md#nullifier-check-without-insert

```compact
import CompactStandardLibrary;
ledger used: Set<Field>;
export ledger accepted: Field;
witness token(): Field;
export circuit accept(): [] {
  const id = token();
  assert(!used.member(disclose(id)), "fresh");
  accepted = disclose(id);
}
```

Output (exit code 1):

```text
$ nightshade vulnerable.compact --config config.json --compiler /path/to/compactc

MEDIUM — Required absence lacks a surviving matching insertion [nullifier-check-without-insert]
vulnerable.compact:7:11
  7 |   assert(!used.member(disclose(id)), "fresh");
    |           ^
accept has a modeled successful state-changing history requiring absence from used, without a definite surviving insertion of that exact value/key into the same collection. Review whether this check is intended to consume a one-use identifier.
Source: vulnerable.compact:7:11
Call path: accept
Remediation: If this is a one-use identifier, insert the checked value/key into the same persistent collection on every successful history and retain it through transaction completion. Review intentional absence validation separately.

Semantic profile: compact-0.34.0-zkir2.
Baseline analysis: complete; selected rules: complete.
Rule coverage: 1 selected rule(s); 0 with incomplete entries.
1 finding(s), 0 suppressed, 0 baseline; 1/1 entrypoint(s) completed; analysis complete. Compiler validation passed.
```

Corrected: Insert the identifier into the used set.

```compact
import CompactStandardLibrary;
ledger used: Set<Field>;
export ledger accepted: Field;
witness token(): Field;
export circuit accept(): [] {
  const id = token();
  assert(!used.member(disclose(id)), "fresh");
  used.insert(disclose(id));
  accepted = disclose(id);
}
```

Output (exit code 0):

```text
$ nightshade corrected.compact --config config.json --compiler /path/to/compactc

Semantic profile: compact-0.34.0-zkir2.
Baseline analysis: complete; selected rules: complete.
Rule coverage: 1 selected rule(s); 0 with incomplete entries.
0 finding(s), 0 suppressed, 0 baseline; 1/1 entrypoint(s) completed; analysis complete. Compiler validation passed.
```

Paths are shortened to the example folder. A quiet result shows that this rule stopped firing, not that the contract is secure.

## 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 |
| ---: | ---: | ---: | ---: | ---: |
| 2/2 | 2/2 | 2/2 | 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/nullifier-check-without-insert.md at v0.1.1.

Availability: **opt-in** with `--detectors nullifier-check-without-insert`; no policy
required. Severity **medium**, confidence **low**. Explicit selection replaces
the default detector set.

### Owned example and review scenario

The compiler-qualified [fixture](#example-1)
requires collection absence before changing state. If the application intends
one-time consumption, the [correction](#example-2)
retains an insertion in the same collection:

```compact
assert(!used.member(disclose(id)), "fresh");
used.insert(disclose(id));
accepted = disclose(id);
```

Recommendation: first confirm nullifier intent, then consume that exact member/key
on every successful relevant history and preserve the insertion. Absence checks
used for ordinary collection administration need not consume a nullifier.

### Evidence and limitations

A candidate is a modeled successful nonconstructor history that requires absence
of an exact value/key in a ledger Set/Map and performs a persistent or canonical
token effect, but does not leave that value/key inserted in the same collection.
This is a structural replay-prevention review, not proof that the value is intended
to be a nullifier or that another transaction can replay it. Read-only membership
helpers and user namesakes do not establish a missing-consumption finding.

The matcher must preserve the actual query Boolean and its value/receiver
snapshots. Ignored queries and tautologies are not guards. Different keys, witness
invocations, collection instances and stale aliases cannot supply insertion
credit. Saved absence results and late atomic assertions remain meaningful;
insert-then-remove/reset does not consume a key. Alternate successful paths and
nested helper calls remain separate. Unknown overlap/equality must not invent
proof of consumption. Unsupported effects and exhausted observation/decoding
budgets must be explicitly incomplete, discarding partial rule findings after
query exhaustion.

The default engine now correlates repeated dynamic membership queries by exact
receiver selectors, member operands and ledger revision, retaining the observation
across local cleanup. It never identifies two reads merely by a wildcard region.
The opt-in observations also retain immutable hash/commitment operands and the
ordered query/write positions. Component equalities rebuild aggregate identities;
bounded Boolean equality/negation propagation handles indirect absence guards.
Inserts survive descendant value updates, but removal, reset or possible ancestor
replacement revokes credit. Each operand traversal is bounded to 4,096 visits and
charged to analysis work; rule matching shares a 1,000,000-work allowance. Any
exhaustion discards partial rule candidates and emits an incomplete diagnostic.

Read-only absence checks can be intentional for collection administration and
need not consume a key. A match is a replay-prevention review prompt; it does not
establish that the checked value is a protocol nullifier or that another
transaction can replay an operation.

### Source examples

These short regression examples are included here for installed-package readers.
Rule-specific policy requirements and limits above still apply.

#### Example 1

Fixture (source: `tests/corpus/vulnerable/nullifier-check-without-insert.compact`).

```compact
import CompactStandardLibrary;
ledger used: Set<Field>;
export ledger accepted: Field;
witness token(): Field;
export circuit accept(): [] {
  const id = token();
  assert(!used.member(disclose(id)), "fresh");
  accepted = disclose(id);
}
```

#### Example 2

Correction (source: `tests/corpus/safe/nullifier-check-without-insert.compact`).

```compact
import CompactStandardLibrary;
ledger used: Set<Field>;
export ledger accepted: Field;
witness token(): Field;
export circuit accept(): [] {
  const id = token();
  assert(!used.member(disclose(id)), "fresh");
  used.insert(disclose(id));
  accepted = disclose(id);
}
```

## 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 nullifier-check-without-insert -- 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/nullifier-check-without-insert.md)
- [Catalog entry in rules.json](https://nightshade.dicksonwu.xyz/rules.json)
- [Verified example](https://nightshade.dicksonwu.xyz/examples.md#nullifier-check-without-insert)
- [All rules](https://nightshade.dicksonwu.xyz/rules.md#source-structure-and-validation)
- [Limitations](https://nightshade.dicksonwu.xyz/limitations.md)