# zero-amount-initial-membership

> Under a declared zero-amount policy, every modeled successful invocation requires the same Map entry to have been present initially.

Canonical: https://nightshade.dicksonwu.xyz/rules/zero-amount-initial-membership.html
Release: Nightshade 0.1.1 (v0.1.1)

| Field | Value |
| --- | --- |
| Rule ID | `zero-amount-initial-membership` |
| Severity | low |
| Confidence | low |
| Maturity | experimental |
| Selection | Opt-in + policy |
| Policy intent | required |
| Default enabled | no |
| Category | Policy-dependent rules |
| Engine facts used | declared-zero-entry, exact-map-preconditions, all-successful-predicates, ordered-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 zero-amount-initial-membership
./.nightshade/node_modules/.bin/nightshade detector show zero-amount-initial-membership
```

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 | 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/zero-amount-initial-membership.md at v0.1.1.

Availability: **opt-in policy**. Severity/confidence: **low/high**. Select with
`--detectors zero-amount-initial-membership` and declare intended zero semantics:

```json
{"version":1,"policies":{"zeroAmountMembership":[
  {"circuit":"credit","amount":"amount","map":"balances"}
]}}
```

The rule reports when **every modeled full successful invocation of the selected
entry, with its declared amount input fixed to zero, requires the same exact Map
entry to have been present initially**. At least one modeled zero success is
required. Other inputs and initial storage remain unknown. This is ordinary
bounded abstract interpretation, with no solver, transaction execution or
cross-transaction proof. The actual amounts passed to helpers retain their values:
an entry-zero call can still pass `amount + 1` to a helper.

```compact
export ledger balances: Map<Bytes<32>, Uint<64>>;
export circuit credit(key: Bytes<32>, amount: Uint<64>): [] {
  const old = balances.lookup(disclose(key));
  balances.insert(disclose(key), disclose((old + amount) as Uint<64>));
}
```

If zero operations must succeed without an existing balance/allowance entry,
bypass lookup **and membership assertions** at zero, or supply the entry locally.
A member assertion still requires initial membership. An optional
`if (balances.member(key)) { ... }` is quiet when its absent route completes;
prior insertion also supplies the entry and stays quiet. Intentional rejection
is a known policy-dependent review shape; do not enable the policy for it.

This diagnostic does not establish that an entry is missing in deployment, that
any modeled history is concretely feasible, or that a runtime failure occurs.

Only an exported circuit, scalar `Uint`/`Field` amount parameter and root Map
ledger can be selected. Nested Map receivers have separate outer/inner atoms.
Successful lookup preconditions are captured **before** membership refinement.
Required saved member predicates retain their original query/write position.
Ordered insertions, descendant value writes and known-empty receiver replacement
are distinguished; wildcard keys, may-alias writes, unknown nested replacements,
lost predicate structure and exhausted evidence remain explicitly unavailable.
Reached checkpoints are unavailable because committed prefixes do not establish
full entry success. No zero success normally supplies no clean rule result.
One narrow exception certifies intentional rejection: an unconditional direct
`Uint` amount comparison against zero fails with the exact declared input fixed
to zero, while a separate complete ordinary analysis retains successful
invocations. Both analyses share the step/value budgets, and the failed assertion
remains in the evidence. Unrelated always-failing entries, contradictory guards,
missing identity, reached checkpoints and exhausted evidence stay unavailable.

The observation uses the existing budgets (40k steps/256 paths/50k values by
default), including evidence traversal. Multiple declared inputs share entry work
and the rule's value allowance. Storage summaries and compressed fold/hash/source
histories are disabled until they can preserve these precondition snapshots.
Both engines and cached/uncached modes have regression coverage. Rule failures
remain rule/entry-scoped and do not change baseline default completion.

## 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 zero-amount-initial-membership -- 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/zero-amount-initial-membership.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)