# re-initialization

> Opt-in review of initializer-named entries with a state-changing second invocation.

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

| Field | Value |
| --- | --- |
| Rule ID | `re-initialization` |
| Severity | low |
| Confidence | low |
| Maturity | experimental |
| Selection | Opt-in |
| Policy intent | not required |
| Default enabled | no |
| Category | Other active opt-ins / State and collections |
| Engine facts used | consecutive-invocations, 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 re-initialization
./.nightshade/node_modules/.bin/nightshade detector show re-initialization
```

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. An exported initializer can overwrite state again because it has no one-time guard. Full example: https://nightshade.dicksonwu.xyz/examples.md#re-initialization

```compact
import CompactStandardLibrary;
export ledger payload: Field;
export circuit initialize(value: Field): [] { payload = disclose(value); }
```

Output (exit code 1):

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

LOW — Initializer has a modeled state-changing second invocation [re-initialization]
vulnerable.compact:3:1
  3 | export circuit initialize(value: Field): [] { payload = disclose(value); }
    | ^
initialize has two consecutive modeled successful invocations from constructor/default storage, with fresh inputs and a potentially different surviving value in payload after the second invocation. Review whether this entry is intended to run only once; its name alone does not establish that requirement.
Call path: initialize
Remediation: If initialization must run once, require the pre-initialized state and preserve its transition on every successful invocation. Review intentional reconfiguration 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: Guard the initializer with a one-time flag.

```compact
import CompactStandardLibrary;
ledger done: Boolean;
export ledger payload: Field;
export circuit initialize(value: Field): [] {
  assert(!done, "already initialized");
  done = true;
  payload = disclose(value);
}
```

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/re-initialization.md at v0.1.1.

Availability: **opt-in**; no policy required. Severity **low**, confidence **low**.
Explicit detector selection replaces the default set.

Owned example: the compiler-qualified [fixture](#example-1)
allows an initializer-named entry to replace stored payload. The
[correction](#example-2) requires the old
`done` flag to be false and retains its true update. Review whether configuration
is intended to be set once; recommendation: enforce that flag invariant when it
is, or document intentional reconfiguration.

Opt-in, low severity and low confidence. From a built source checkout, use:
`node dist/src/cli.js scan examples/review/contract.compact --detectors re-initialization`.

This review selects exported circuit declarations named `initialize`, `initializer`,
or either name followed by an underscore suffix, that transitively write storage.
It evaluates actual modeled construction/default storage, then two calls to that
entry with fresh parameters and witness identities. A finding requires two modeled
successful calls and a potentially different surviving ledger value after the second.
Allocation IDs, revisions and temporary writes alone are insufficient.

```compact
import CompactStandardLibrary;
ledger configured: Field;
export circuit initialize(value: Field): [] { configured = disclose(value); }
```

If `configured` was intended to be set once, a repeated initialization could replace
the application's configuration. The finding does not prove that intention, concrete
path feasibility, deployed reachability or exploitability. Intentional reconfiguration
is a known false-positive shape. Naming is candidate evidence only; this is why the
rule is opt-in and low confidence.

For one-time behavior, assert the old initialization flag and preserve its update on
every successful path. A late assertion on the saved old flag is also effective under
the modeled atomic semantics. Setting and then restoring the flag does not establish
one-time behavior. An idempotent write of the same final value stays quiet.

The analysis retains storage, revisions, collection facts and scalar constraints
across calls. It clears invocation-local guards, environments, call counters and
effect histories. Historical private dependencies retain their original invocation;
they do not become fresh caller evidence or certified trusted storage. Sequence
assertions never contribute to the ordinary `impossible-assertion` rule.

Ordinary entry analysis and the sequence share the existing per-entry step budget;
retained first histories/pairs and abstract values also remain bounded. Exhaustion
is incomplete. Transaction/context effects such as Kernel operations and coin
qualification are not carried across calls. Counter scalar contents, zero updates
and bounded net offsets from fixed checked updates are compared across calls.
Other surviving ADT contents remain unsupported. Either boundary reports explicit incomplete diagnostics and no
initialization finding for that entry. A guarded initializer that has no successful
second call needs no final ADT-content comparison.

### 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/re-initialization.compact`).

```compact
import CompactStandardLibrary;
export ledger payload: Field;
export circuit initialize(value: Field): [] { payload = disclose(value); }
```

#### Example 2

Correction (source: `tests/corpus/safe/re-initialization.compact`).

```compact
import CompactStandardLibrary;
ledger done: Boolean;
export ledger payload: Field;
export circuit initialize(value: Field): [] {
  assert(!done, "already initialized");
  done = true;
  payload = disclose(value);
}
```

## 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 re-initialization -- 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/re-initialization.md)
- [Catalog entry in rules.json](https://nightshade.dicksonwu.xyz/rules.json)
- [Verified example](https://nightshade.dicksonwu.xyz/examples.md#re-initialization)
- [All rules](https://nightshade.dicksonwu.xyz/rules.md#state-and-collections)
- [Limitations](https://nightshade.dicksonwu.xyz/limitations.md)