# impossible-assertion

> A nonliteral assertion fails on every reaching path, or an entry has no successful path.

Canonical: https://nightshade.dicksonwu.xyz/rules/impossible-assertion.html
Release: Nightshade 0.1.1 (v0.1.1)

| Field | Value |
| --- | --- |
| Rule ID | `impossible-assertion` |
| Severity | medium |
| Confidence | high |
| Maturity | experimental |
| Selection | Audit default |
| Policy intent | not required |
| Default enabled | yes |
| Category | Audit-default ordinary rules |
| Engine facts used | cfg, constants, path-constraints, failed-assertions, assertion-reaches, completed-entries |
| Release | v0.1.1 |

## Selection and scope

Selected by the default audit profile, so an ordinary scan runs it.

```sh
./.nightshade/node_modules/.bin/nightshade ./contracts --detectors impossible-assertion
./.nightshade/node_modules/.bin/nightshade detector show impossible-assertion
```

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 |
| ---: | ---: | ---: | ---: | ---: |
| 2/2 | 2/2 | 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/impossible-assertion.md at v0.1.1.

Availability: **default**; no policy required. Severity **medium**, confidence
**high** for modeled universal rejection.

Reports a nonliteral-false assertion that fails on every modeled path reaching
its source site, with complete caller coverage. It can also report a completely
analyzed entrypoint with no successful path, without duplicating an entry already
explained by an assertion finding.

### Example and review scenario

The compiler-qualified owned [fixture](#example-1)
requires `flag` and then its negation. The
[correction](#example-2) keeps compatible
checks. Review contradictory validation when an intended entrypoint appears
unusable; inspect the preceding constraints as well as the reported assertion.

Recommendation: preserve guards that reject invalid inputs while allowing the
intended inputs to succeed. Correct contradictory operands or document an
intentionally disabled entrypoint. Checked arithmetic and casts may also explain
an entrypoint-level rejection.

### False positives and limitations

Deliberately disabled entrypoints can match. Ordinary rejecting guards are quiet
if some reaching invocation passes, even if that caller aborts later. Literal
`assert(false)` revert sites are suppressed as assertion findings; nonliteral
constant-false expressions remain reportable. Incomplete or unselected potential
callers block universal assertion claims. A finding concerns modeled invocation
constraints, not cross-transaction reachability or a successful state change.
Unknown effects and exhausted budgets remain incomplete.

### 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/contradictory-assertion.compact`).

```compact
pragma language_version >= 0.26.0;
export circuit verify(flag: Boolean): [] {
  assert(flag, "flag required");
  assert(!flag, "flag forbidden");
}
```

#### Example 2

Correction (source: `tests/corpus/safe/contradictory-assertion.compact`).

```compact
pragma language_version >= 0.26.0;
export circuit verify(flag: Boolean): [] {
  assert(flag, "flag required");
  assert(flag, "flag still required");
}
```

## 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 impossible-assertion -- 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/impossible-assertion.md)
- [Catalog entry in rules.json](https://nightshade.dicksonwu.xyz/rules.json)
- [All rules](https://nightshade.dicksonwu.xyz/rules.md#audit-default-ordinary-rules)
- [Limitations](https://nightshade.dicksonwu.xyz/limitations.md)