# unshielded-refund-endpoint-review

> Review a complete local refund-validator endpoint producing a zero remainder send expression.

Canonical: https://nightshade.dicksonwu.xyz/rules/unshielded-refund-endpoint-review.html
Release: Nightshade 0.1.1 (v0.1.1)

| Field | Value |
| --- | --- |
| Rule ID | `unshielded-refund-endpoint-review` |
| Severity | info |
| Confidence | varies |
| Maturity | experimental |
| Selection | Opt-in |
| Policy intent | not required |
| Default enabled | no |
| Category | Other active opt-ins / Token, coin and value transfers |
| Engine facts used | source-local-formula-certificate |
| 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 unshielded-refund-endpoint-review
./.nightshade/node_modules/.bin/nightshade detector show unshielded-refund-endpoint-review
```

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 |
| ---: | ---: | ---: | ---: | ---: |
| 5/5 | 1/1 | 1/3 | 7/9 | 2 |

Deviations recorded for this rule:

| Case | Kind | Expected to observed lines | Issue |
| --- | --- | --- | --- |
| manifest.json / refundEndpoint57/drafts/arithmetic-endpoint57/dynamic-map-snapshots.compact | negative | [] to [] | incomplete or unvalidated |
| manifest.json / refundEndpoint57/drafts/arithmetic-endpoint57/intentional-endpoint.compact | lookalike | [58] to [58] | control hit |
| manifest.json / refundEndpoint57/drafts/arithmetic-endpoint57/intentional.compact | lookalike | [58] to [58] | control hit |
| manifest.json / refundEndpoint57/drafts/arithmetic-endpoint57/scalar-ledger-snapshots.compact | negative | [] to [] | incomplete or unvalidated |

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/unshielded-refund-endpoint-review.md at v0.1.1.

Availability: **opt-in**; severity **info**. Qualified for compiler 0.34.0/ZKIR2
or ZKIR3; experimental Counter mode is unavailable.

`unshielded-refund-endpoint-review` is opt-in and informational. It inspects a complete straight-line pure validator, matches its unsigned bounded floor relation, and evaluates the selected formal witness B=P=A=Q=1 through every statement, assertion, arithmetic intermediate and numeric cast. The validator assertion is tied by resolved lexical snapshot identities to a direct canonical send expression B-Q. Both Q*A+A and checked (Q+1)*A upper expressions are supported.

The result is an independently complete source-local formula certificate. It proves that this selected formal witness satisfies the inspected formula and supported relevant local caller arithmetic checks, and yields zero in the tied remainder expression. It does not certify unrelated caller conditions, ledger reachability, successful histories, transaction or proof feasibility, send rejection or application impact. Intentional endpoints match. A quiet result after rejecting witness1 does not establish that another zero endpoint is impossible.

Rule coverage uses `source-local-formula`. Baseline diagnostics and completion remain intact even when a local certificate completes. It never fills `completedEntries`, fabricates runtime paths or retries a failed ordinary analysis. Experimental Counter mode explicitly refuses the source certificate. The dedicated versioned evidence carrier and issued certificates are checked against the owning Program and compiler profile before emission.

Discovery and evaluation share40k steps per entry,256 candidate mappings per entry and50k cumulative retained values per selected rule. Expression/CFG ownership, recursive operand discovery, formal evaluation, casts, assertions, key strings, source mappings and findings are metered. Failures retain scoped incomplete diagnostics without partial findings from the affected entry. Dynamic reads and raw ledger reads cannot be equated; a local initialized from storage is an opaque value snapshot. Exact tuple leaves and aliases preserve distinct lexical identity.

The initial implementation supports compiler0.34.0/ZKIR2 or3. It refuses loop-contained sends, unsupported pure-body statements/calls, relevant opaque caller checks, mutable operand/guard snapshots, lost argument provenance, unsupported checked types and exhausted budgets. Unrelated caller conditions remain explicitly outside the formula theorem. Nested relevant conditional continuations are inspected as local implications; unresolved relevant conditions refuse rather than being assumed true.

Discovery keeps a private immutable snapshot of caller expressions, source spans and resolved symbols. Public candidate maps cannot alter later certification; shared Program objects are not globally frozen. Finding preparation charges the actual emitted strings, imported source-file key lists and sorting, path normalization, discriminator replacements, fingerprint-key joining and UTF-8 hashing work before emission. These costs share the existing observation allowance.

The initial checker inventory conservatively includes pure checkers from sibling branches. A relevant checker in an exclusive branch can therefore cause an incomplete result even when that branch would not run at the selected witness. This limitation is retained instead of claiming a complete path certificate or broadening branch analysis this checkpoint.

## 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 unshielded-refund-endpoint-review -- 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/unshielded-refund-endpoint-review.md)
- [Catalog entry in rules.json](https://nightshade.dicksonwu.xyz/rules.json)
- [All rules](https://nightshade.dicksonwu.xyz/rules.md#token-coin-and-value-transfers)
- [Limitations](https://nightshade.dicksonwu.xyz/limitations.md)