# Examples

> Ten synthetic Nightshade findings with the flagged Compact code, the exact CLI output, a corrected version that stays quiet and a lookalike.

Canonical: https://nightshade.dicksonwu.xyz/examples.html
Release: Nightshade 0.1.1 (v0.1.1)

Ten synthetic examples, each for a different rule. Every example shows the flagged code, the exact output from the released 0.1.1 CLI, a corrected version that the rule no longer flags and, for nine of them, a lookalike that resembles the problem but stays quiet. Every file passed Compact 0.34.0 compiler validation in the same run.

1. Private authentication preimage reaches the public ledger (`ledger-bound-preimage-publication`, medium)
2. A public key comparison does not prove ownership (`spoofable-authorization`, high)
3. The signature verification result is discarded (`ignored-validation-result`, medium)
4. Caller time needs a chain-time bound (`freshness-bound-caller-time`, medium)
5. Initialization can run repeatedly (`re-initialization`, low)
6. Two shielded mints reuse the same descriptor (`duplicate-shielded-mint`, medium)
7. The Merkle membership result is ignored (`merkle-membership-not-enforced`, medium)
8. An unchecked witness value becomes public state (`unconstrained-witness-to-state`, medium)
9. A freshness check never consumes the nullifier (`nullifier-check-without-insert`, medium)
10. A private commitment uses fixed randomness (`predictable-commitment-randomness`, medium)

## Private authentication preimage reaches the public ledger

Synthetic example 1 of 10. Rule: [ledger-bound-preimage-publication](https://nightshade.dicksonwu.xyz/rules/ledger-bound-preimage-publication.md). Severity: medium. Selection: Audit default. Compiler profile: compact-0.34.0-zkir2.

A secret checked against a stored hash is then written directly to public state.

### Flagged

vulnerable.compact, line 12 flagged:

```compact
pragma language_version >= 0.26.0;
import CompactStandardLibrary;
export ledger ownerHash: Bytes<32>;
export ledger published: Field;
witness ownerSecret(): Field;
constructor(initialHash: Bytes<32>) {
  ownerHash = disclose(initialHash);
}
export circuit update(): [] {
  const secret = ownerSecret();
  assert(persistentHash<Field>(secret) == ownerHash, "not authorized");
  published = disclose(secret);
}
```

Output (exit code 1):

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

MEDIUM — Ledger-bound private preimage is published [ledger-bound-preimage-publication]
vulnerable.compact:12:3
  12 |   published = disclose(secret);
     |   ^
Private value from ownerSecret reaches ledger-write published without a hiding transformation. A hash of this value is asserted equal to ledger ownerHash on the same potential successful path. Ledger operation data is public. If an untrusted observer obtains a reusable authentication secret through this boundary, secrecy is lost. An intentional reveal protocol may permit this flow.
Source: vulnerable.compact:10:18
Constraint: vulnerable.compact:11:3
Call path: update
Remediation: Keep reusable authentication preimages private; publish a suitable commitment or non-secret result. If this is intentional reveal, confirm that the revealed value grants no remaining authority and document that policy.

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; 2/2 entrypoint(s) completed; analysis complete. Compiler validation passed.
```

### Corrected

Publish the hash instead of the secret.

```compact
pragma language_version >= 0.26.0;
import CompactStandardLibrary;
export ledger ownerHash: Bytes<32>;
export ledger published: Bytes<32>;
witness ownerSecret(): Field;
constructor(initialHash: Bytes<32>) {
  ownerHash = disclose(initialHash);
}
export circuit update(): [] {
  const secret = ownerSecret();
  assert(persistentHash<Field>(secret) == ownerHash, "not authorized");
  published = disclose(persistentHash<Field>(secret));
}
```

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; 2/2 entrypoint(s) completed; analysis complete. Compiler validation passed.
```

### Lookalike

A witness value is published, but it is never checked against a ledger hash, so it is not an authentication preimage.

```compact
pragma language_version >= 0.26.0;
export ledger published: Field;
witness publicReading(): Field;
export circuit record(): [] {
  published = disclose(publicReading());
}
```

Output (exit code 0):

```text
$ nightshade lookalike.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.
```

Configuration (config.json):

```json
{
  "version": 1,
  "compilerVersion": "0.34.0",
  "zkirVersion": 2,
  "detectors": [
    "ledger-bound-preimage-publication"
  ]
}
```

Source fixtures at v0.1.1: https://github.com/DicksonWu654/nightshade/blob/v0.1.1/tests/corpus/vulnerable/direct.compact, https://github.com/DicksonWu654/nightshade/blob/v0.1.1/tests/corpus/safe/hash-only.compact, https://github.com/DicksonWu654/nightshade/blob/v0.1.1/tests/corpus/safe/ordinary-disclosure.compact. Original compact fixture retained. Paths in the output are shortened to the example folder.

## A public key comparison does not prove ownership

Synthetic example 2 of 10. Rule: [spoofable-authorization](https://nightshade.dicksonwu.xyz/rules/spoofable-authorization.md). Severity: high. Selection: Audit default. Compiler profile: compact-0.34.0-zkir2.

Comparing a caller-supplied public identity with the stored owner does not prove possession of its secret.

### Flagged

vulnerable.compact, line 6 flagged:

```compact
import CompactStandardLibrary;
export ledger owner: ZswapCoinPublicKey;
export ledger stored: Field;

export circuit change(next: Field): [] {
  assert(ownPublicKey() == owner, "owner");
  stored = disclose(next);
}
```

Output (exit code 1):

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

HIGH — Public-key equality gates a state-changing effect [spoofable-authorization]
vulnerable.compact:6:3
  6 |   assert(ownPublicKey() == owner, "owner");
    |   ^
change requires raw witness data from ownPublicKey to equal ledger owner on every modeled successful reach. The guard covers 1 effect site: ledger-write stored. Every successful history reaching these effects has only raw-witness/public-data checks; no additional modeled gate is present. Equality alone does not demonstrate possession of a secret; review the intended authentication and protocol role.
Source: vulnerable.compact:6:10
Constraint: vulnerable.compact:6:3
Call path: change
Remediation: If this check is intended as authentication, enforce a suitable secret-preimage or protocol-specific proof. Review key initialization, secrecy and replay assumptions. Document and triage intentional public-data validation.

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

Authorize with a private key preimage checked against the stored owner hash.

```compact
import CompactStandardLibrary;
export ledger owner: Bytes<32>;
export ledger stored: Field;
witness privateKey(): Bytes<32>;

export circuit change(next: Field): [] {
  assert(persistentHash<Bytes<32>>(privateKey()) == owner, "secret preimage");
  stored = disclose(next);
}
```

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.
```

### Lookalike

A local helper named ownPublicKey returns ledger data, and a witness comparison is returned rather than enforced.

```compact
export ledger owner: Bytes<32>;
export ledger stored: Field;
witness identity(): Bytes<32>;

circuit ownPublicKey(): Bytes<32> { return owner; }
export circuit publicValidation(next: Field): [] {
  assert(ownPublicKey() == owner, "public value, no witness");
  stored = disclose(next);
}
export circuit onlyComparison(): Boolean {
  return disclose(identity() == owner);
}
```

Output (exit code 0):

```text
$ nightshade lookalike.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; 2/2 entrypoint(s) completed; analysis complete. Compiler validation passed.
```

Configuration (config.json):

```json
{
  "version": 1,
  "compilerVersion": "0.34.0",
  "zkirVersion": 2,
  "detectors": [
    "spoofable-authorization"
  ]
}
```

Source fixtures at v0.1.1: https://github.com/DicksonWu654/nightshade/blob/v0.1.1/tests/corpus/vulnerable/spoofable-authorization.compact, https://github.com/DicksonWu654/nightshade/blob/v0.1.1/tests/corpus/safe/spoofable-authorization.compact, https://github.com/DicksonWu654/nightshade/blob/v0.1.1/tests/corpus/safe/spoofable-authorization-lookalike.compact. Original compact fixture retained. Paths in the output are shortened to the example folder.

## The signature verification result is discarded

Synthetic example 3 of 10. Rule: [ignored-validation-result](https://nightshade.dicksonwu.xyz/rules/ignored-validation-result.md). Severity: medium. Selection: Audit default. Compiler profile: compact-0.34.0-zkir2.

The signature verifier returns a boolean, but the state change proceeds without asserting that it is true.

### Flagged

vulnerable.compact, line 23 flagged:

```compact
// This file is part of midnightntwrk/example-counter.
// Copyright (C) Midnight Foundation
// SPDX-License-Identifier: Apache-2.0
// Licensed under the Apache License, Version 2.0 (the "License");
// You may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
// http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.

// Synthetic regression mutation; no upstream-project finding is claimed.
pragma language_version >= 0.20;
import CompactStandardLibrary;
export ledger round: Counter;

export circuit signedIncrement(msg: Vector<1, Field>, sig: JubjubSchnorrSignature, pk: JubjubPoint): [] {
  assert(pk != default<JubjubPoint>, "nonidentity signer");
  jubjubSchnorrVerify<1>(msg, sig, pk);
  round.increment(1);
}
```

Output (exit code 1):

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

MEDIUM — Signature verification outcome is discarded [ignored-validation-result]
vulnerable.compact:23:3
  23 |   jubjubSchnorrVerify<1>(msg, sig, pk);
     |   ^
The Boolean outcome of the canonical jubjubSchnorrVerify is discarded. The call may impose internal constraints, but its signature-validity result does not constrain this caller through this use.
Remediation: Assert the verification result, or reject the false branch before the transaction can succeed. Preserve intentional Boolean checker APIs; suppress intentional verifier-only tests with a reason.

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

Assert the verifier's result.

```compact
// This file is part of midnightntwrk/example-counter.
// Copyright (C) Midnight Foundation
// SPDX-License-Identifier: Apache-2.0
// Licensed under the Apache License, Version 2.0 (the "License");
// You may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
// http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.

// Synthetic regression mutation; no upstream-project finding is claimed.
pragma language_version >= 0.20;
import CompactStandardLibrary;
export ledger round: Counter;

export circuit signedIncrement(msg: Vector<1, Field>, sig: JubjubSchnorrSignature, pk: JubjubPoint): [] {
  assert(pk != default<JubjubPoint>, "nonidentity signer");
  assert(jubjubSchnorrVerify<1>(msg, sig, pk), "signature");
  round.increment(1);
}
```

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.
```

### Lookalike

The circuit asserts a local Boolean check and never calls a signature verifier.

```compact
// This file is part of midnightntwrk/example-counter.
// Copyright (C) Midnight Foundation
// SPDX-License-Identifier: Apache-2.0
// Licensed under the Apache License, Version 2.0 (the "License");
// You may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
// http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.

pragma language_version >= 0.20;

import CompactStandardLibrary;

// public state
export ledger round: Counter;

// transition function changing public state
export circuit increment(): [] {
  round.increment(1);
}

circuit ownedCheck(): Boolean { return true; }

export circuit signedIncrement(msg: Vector<1, Field>, sig: JubjubSchnorrSignature, pk: JubjubPoint): [] {
  assert(pk != default<JubjubPoint>, "nonidentity signer");
  assert(ownedCheck(), "owned public validation");
  round.increment(1);
}
```

Output (exit code 0):

```text
$ nightshade lookalike.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; 2/2 entrypoint(s) completed; analysis complete. Compiler validation passed.
```

Configuration (config.json):

```json
{
  "version": 1,
  "compilerVersion": "0.34.0",
  "zkirVersion": 2,
  "detectors": [
    "ignored-validation-result"
  ]
}
```

Source fixtures at v0.1.1: https://github.com/DicksonWu654/nightshade/blob/v0.1.1/tests/corpus/known-bugs/counter-ignored-validation-positive.compact (trimmed here), https://github.com/DicksonWu654/nightshade/blob/v0.1.1/tests/corpus/known-bugs/counter-ignored-validation-corrected.compact (trimmed here), https://github.com/DicksonWu654/nightshade/blob/v0.1.1/tests/corpus/known-bugs/counter-ignored-validation-lookalike.compact. Unrelated baseline circuits and ledgers removed; original licence header retained where present. Paths in the output are shortened to the example folder.

## Caller time needs a chain-time bound

Synthetic example 4 of 10. Rule: [freshness-bound-caller-time](https://nightshade.dicksonwu.xyz/rules/freshness-bound-caller-time.md). Severity: medium. Selection: Audit default. Compiler profile: compact-0.34.0-zkir2.

The circuit accepts a caller-supplied time window without bounding it against chain time.

### Flagged

vulnerable.compact, line 14 flagged:

```compact
pragma language_version >= 0.23;
import CompactStandardLibrary;

export ledger startedAt: Uint<64>;
export ledger authenticated: Boolean;

constructor() {
  startedAt = 0;
  authenticated = false;
}

export circuit authenticate(expectedTimeWindow: Uint<64>): [] {
  assert(disclose(expectedTimeWindow >= startedAt), "window");
  startedAt = disclose(expectedTimeWindow);
  authenticated = true;
}
```

Output (exit code 1):

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

MEDIUM — Caller time is not bound to protocol time [freshness-bound-caller-time]
vulnerable.compact:14:3
  14 |   startedAt = disclose(expectedTimeWindow);
     |   ^
authenticate accepts caller-supplied expectedTimeWindow and uses it in a state-changing or public effect without an asserted canonical block-time bound. A delayed, future-dated or stale proof may remain valid outside the intended freshness window. This source/effect review does not establish transaction ordering or exploitability.
Source: vulnerable.compact:12:29
Call path: authenticate
Remediation: Compare the caller value with block time using canonical blockTimeGte/blockTimeGt and blockTimeLte/blockTimeLt checks, or derive the deadline solely from a kernel-bound timestamp. Keep the bound on the same successful path as the state-changing effect.

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; 2/2 entrypoint(s) completed; analysis complete. Compiler validation passed.
```

### Corrected

Bound the caller's time with blockTimeGte before using it.

```compact
pragma language_version >= 0.23;
import CompactStandardLibrary;

export ledger startedAt: Uint<64>;
export ledger authenticated: Boolean;

constructor() {
  startedAt = 0;
  authenticated = false;
}

export circuit authenticate(expectedTimeWindow: Uint<64>): [] {
  assert(blockTimeGte(disclose(expectedTimeWindow)), "future window");
  assert(disclose(expectedTimeWindow >= startedAt), "window");
  startedAt = disclose(expectedTimeWindow);
  authenticated = true;
}
```

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; 2/2 entrypoint(s) completed; analysis complete. Compiler validation passed.
```

### Lookalike

A caller-supplied amount is compared with a ledger minimum; it is not a time value.

```compact
pragma language_version >= 0.23;
import CompactStandardLibrary;

export ledger minimum: Uint<64>;
export ledger accepted: Boolean;

constructor() {
  minimum = 1;
  accepted = false;
}

export circuit accept(amount: Uint<64>): [] {
  assert(disclose(amount >= minimum), "amount");
  accepted = true;
}
```

Output (exit code 0):

```text
$ nightshade lookalike.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; 2/2 entrypoint(s) completed; analysis complete. Compiler validation passed.
```

Configuration (config.json):

```json
{
  "version": 1,
  "compilerVersion": "0.34.0",
  "zkirVersion": 2,
  "detectors": [
    "freshness-bound-caller-time"
  ]
}
```

Source fixtures at v0.1.1: https://github.com/DicksonWu654/nightshade/blob/v0.1.1/tests/corpus/drafts/rule-gaps-20261016/freshness-positive.compact, https://github.com/DicksonWu654/nightshade/blob/v0.1.1/tests/corpus/drafts/rule-gaps-20261016/freshness-corrected.compact, https://github.com/DicksonWu654/nightshade/blob/v0.1.1/tests/corpus/drafts/rule-gaps-20261016/freshness-lookalike.compact. Original compact fixture retained. Paths in the output are shortened to the example folder.

## Initialization can run repeatedly

Synthetic example 5 of 10. Rule: [re-initialization](https://nightshade.dicksonwu.xyz/rules/re-initialization.md). Severity: low. Selection: Opt-in. Compiler profile: compact-0.34.0-zkir2.

An exported initializer can overwrite state again because it has no one-time guard.

### Flagged

vulnerable.compact, line 3 flagged:

```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.
```

### Lookalike

A circuit that is meant to be callable more than once and leaves no different state on a second call.

```compact
import CompactStandardLibrary;
export ledger ready: Boolean;
// Intentionally callable more than once, with no surviving second-call change.
export circuit initialize(): [] { ready = true; }
```

Output (exit code 0):

```text
$ nightshade lookalike.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.
```

Configuration (config.json):

```json
{
  "version": 1,
  "compilerVersion": "0.34.0",
  "zkirVersion": 2,
  "detectors": [
    "re-initialization"
  ]
}
```

Source fixtures at v0.1.1: https://github.com/DicksonWu654/nightshade/blob/v0.1.1/tests/corpus/vulnerable/re-initialization.compact, https://github.com/DicksonWu654/nightshade/blob/v0.1.1/tests/corpus/safe/re-initialization.compact, https://github.com/DicksonWu654/nightshade/blob/v0.1.1/tests/corpus/safe/re-initialization-lookalike.compact. Original compact fixture retained. Paths in the output are shortened to the example folder.

## Two shielded mints reuse the same descriptor

Synthetic example 6 of 10. Rule: [duplicate-shielded-mint](https://nightshade.dicksonwu.xyz/rules/duplicate-shielded-mint.md). Severity: medium. Selection: Audit default. Compiler profile: compact-0.34.0-zkir2.

Two mint calls use identical token, amount, nonce and recipient inputs on the same path.

### Flagged

vulnerable.compact, line 7 flagged:

```compact
// Owned synthetic duplicate-mint regression.
import CompactStandardLibrary;

export circuit rewardTwice(nonce: Bytes<32>, recipient: ZswapCoinPublicKey): [] {
  const to = left<ZswapCoinPublicKey,ContractAddress>(disclose(recipient));
  mintShieldedToken(pad(32,"sdk:reward"),1,disclose(evolveNonce(0,nonce)),to);
  mintShieldedToken(pad(32,"sdk:reward"),1,disclose(evolveNonce(0,nonce)),to);
}
```

Output (exit code 1):

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

MEDIUM — Duplicate shielded mint commitment [duplicate-shielded-mint]
vulnerable.compact:7:3
  7 |   mintShieldedToken(pad(32,"sdk:reward"),1,disclose(evolveNonce(0,nonce)),to);
    |   ^
rewardTwice invokes mintShieldedToken twice with provably identical token domain, amount, nonce and active recipient on one modeled successful history. The pinned library derives the same coin commitment in this contract context; duplicate commitments are rejected by the ledger. This is a transaction availability defect, not proof of token theft or a generic commitment-opening vulnerability.
Source: vulnerable.compact:6:3
Call path: rewardTwice → mintShieldedToken
Remediation: Use a distinct nonce for each minted output, for example evolveNonce with a distinct index. Review freshness across separate transactions independently.

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

Give the second mint a distinct nonce.

```compact
// Owned synthetic duplicate-mint regression.
import CompactStandardLibrary;

export circuit rewardTwice(nonce: Bytes<32>, recipient: ZswapCoinPublicKey): [] {
  const to = left<ZswapCoinPublicKey,ContractAddress>(disclose(recipient));
  mintShieldedToken(pad(32,"sdk:reward"),1,disclose(evolveNonce(0,nonce)),to);
  mintShieldedToken(pad(32,"sdk:reward"),1,disclose(evolveNonce(1,nonce)),to);
}
```

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.
```

### Lookalike

Two mints share a nonce but use different amounts, so the descriptors differ.

```compact
// Owned synthetic duplicate-mint regression.
import CompactStandardLibrary;

export circuit rewardTwice(nonce: Bytes<32>, recipient: ZswapCoinPublicKey): [] {
  const to = left<ZswapCoinPublicKey,ContractAddress>(disclose(recipient));
  mintShieldedToken(pad(32,"sdk:reward"),1,disclose(evolveNonce(0,nonce)),to);
  mintShieldedToken(pad(32,"sdk:reward"),2,disclose(evolveNonce(0,nonce)),to);
}
```

Output (exit code 0):

```text
$ nightshade lookalike.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.
```

Configuration (config.json):

```json
{
  "version": 1,
  "compilerVersion": "0.34.0",
  "zkirVersion": 2,
  "detectors": [
    "duplicate-shielded-mint"
  ]
}
```

Source fixtures at v0.1.1: https://github.com/DicksonWu654/nightshade/blob/v0.1.1/tests/corpus/known-bugs/sdk-duplicate-mint-positive.compact (trimmed here), https://github.com/DicksonWu654/nightshade/blob/v0.1.1/tests/corpus/known-bugs/sdk-duplicate-mint-corrected.compact (trimmed here), https://github.com/DicksonWu654/nightshade/blob/v0.1.1/tests/corpus/known-bugs/sdk-duplicate-mint-lookalike.compact (trimmed here). Unrelated baseline circuits and ledgers removed; original licence header retained where present. Paths in the output are shortened to the example folder.

## The Merkle membership result is ignored

Synthetic example 7 of 10. Rule: [merkle-membership-not-enforced](https://nightshade.dicksonwu.xyz/rules/merkle-membership-not-enforced.md). Severity: medium. Selection: Audit default. Compiler profile: compact-0.34.0-zkir2.

Computing and checking a Merkle root does not enforce membership when the boolean result is discarded.

### Flagged

vulnerable.compact, line 7 flagged:

```compact
import CompactStandardLibrary;
ledger tree: MerkleTree<2,Field>;
export ledger accepted: Field;
witness suppliedPath(): MerkleTreePath<2,Field>;
export circuit accept(): [] {
  const proof = suppliedPath();
  const digest = merkleTreePathRoot<2,Field>(proof);
  tree.checkRoot(disclose(digest));
  accepted = disclose(proof.leaf);
}
```

Output (exit code 1):

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

MEDIUM — Proof-related effect lacks enforced trusted-root membership [merkle-membership-not-enforced]
vulnerable.compact:7:18
  7 |   const digest = merkleTreePathRoot<2,Field>(proof);
    |                  ^
accept has a modeled successful history where proof-related data influences accepted, without a required check of that digest against definite preexisting ledger root data. Computing or ignoring a membership result does not enforce it. Review whether this effect requires membership; public deposits and root-management flows may be intentional.
Source: vulnerable.compact:7:18
Call path: accept → merkleTreePathRoot
Remediation: If membership is required, constrain successful execution with the exact digest's ledger-tree checkRoot result or equality with the intended trusted root. Preserve valid alternate checks and intentional public behavior.

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

Assert the result of checkRoot.

```compact
import CompactStandardLibrary;
ledger tree: MerkleTree<2,Field>;
export ledger accepted: Field;
witness suppliedPath(): MerkleTreePath<2,Field>;
export circuit accept(): [] {
  const proof = suppliedPath();
  const digest = merkleTreePathRoot<2,Field>(proof);
  assert(tree.checkRoot(disclose(digest)), "member");
  accepted = disclose(proof.leaf);
}
```

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.
```

### Lookalike

A local function named merkleTreePathRoot returns a default digest and no ledger tree is involved.

```compact
import { MerkleTreePath, MerkleTreeDigest } from CompactStandardLibrary;
export ledger accepted: Field;
witness suppliedPath(): MerkleTreePath<2,Field>;
circuit merkleTreePathRoot(proof: MerkleTreePath<2,Field>): MerkleTreeDigest { return default<MerkleTreeDigest>; }
export circuit accept(): [] {
  const proof = suppliedPath();
  const digest = merkleTreePathRoot(proof);
  accepted = disclose(proof.leaf);
}
```

Output (exit code 0):

```text
$ nightshade lookalike.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.
```

Configuration (config.json):

```json
{
  "version": 1,
  "compilerVersion": "0.34.0",
  "zkirVersion": 2,
  "detectors": [
    "merkle-membership-not-enforced"
  ]
}
```

Source fixtures at v0.1.1: https://github.com/DicksonWu654/nightshade/blob/v0.1.1/tests/corpus/vulnerable/merkle-membership-not-enforced.compact, https://github.com/DicksonWu654/nightshade/blob/v0.1.1/tests/corpus/safe/merkle-membership-not-enforced.compact, https://github.com/DicksonWu654/nightshade/blob/v0.1.1/tests/corpus/safe/merkle-membership-not-enforced-lookalike.compact. Original compact fixture retained. Paths in the output are shortened to the example folder.

## An unchecked witness value becomes public state

Synthetic example 8 of 10. Rule: [unconstrained-witness-to-state](https://nightshade.dicksonwu.xyz/rules/unconstrained-witness-to-state.md). Severity: medium. Selection: Opt-in. Compiler profile: compact-0.34.0-zkir2.

A witness chooses the allocation written to the ledger without a preceding bound on that value.

### Flagged

vulnerable.compact, line 7 flagged:

```compact
// Owned synthetic witness-to-state regression.
import CompactStandardLibrary;

export ledger allocation: Uint<64>;
witness rewardAmount(): Uint<64>;
export circuit allocate(): [] {
  const value=rewardAmount();
  allocation=disclose(value);
}
```

Output (exit code 1):

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

MEDIUM — Raw witness value reaches ledger state without a value-specific assertion [unconstrained-witness-to-state]
vulnerable.compact:7:15
  7 |   const value=rewardAmount();
    |               ^
allocate writes raw output of rewardAmount into allocation on a modeled successful history without an assertion depending on that witness leaf. Disclosure permits publication; it does not validate the value. An unrelated caller guard or a witness attestation about the value supplies no circuit validation. Public registration and prover-chosen metadata can be intentional; review the required application relation.
Source: vulnerable.compact:7:15
Call path: allocate
Remediation: If this field must represent an independently established fact, enforce the required relationship in the circuit using the exact supplied value. Document intentionally prover-chosen data. Review authorization and the adequacy of the check 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

Assert a bound on the witness value before writing it.

```compact
// Owned synthetic witness-to-state regression.
import CompactStandardLibrary;

export ledger allocation: Uint<64>;
witness rewardAmount(): Uint<64>;
export circuit allocate(): [] {
  const value=rewardAmount();
  assert(value<=100,"reward allocation");
  allocation=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.
```

### Lookalike

The value written to the ledger comes from a circuit argument, not a witness.

```compact
// Owned synthetic witness-to-state regression.
import CompactStandardLibrary;

export ledger allocation: Uint<64>;
export circuit allocate(value: Uint<64>): [] {
  allocation=disclose(value);
}
```

Output (exit code 0):

```text
$ nightshade lookalike.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.
```

Configuration (config.json):

```json
{
  "version": 1,
  "compilerVersion": "0.34.0",
  "zkirVersion": 2,
  "detectors": [
    "unconstrained-witness-to-state"
  ]
}
```

Source fixtures at v0.1.1: https://github.com/DicksonWu654/nightshade/blob/v0.1.1/tests/corpus/known-bugs/sdk-witness-state-positive.compact (trimmed here), https://github.com/DicksonWu654/nightshade/blob/v0.1.1/tests/corpus/known-bugs/sdk-witness-state-corrected.compact (trimmed here), https://github.com/DicksonWu654/nightshade/blob/v0.1.1/tests/corpus/known-bugs/sdk-witness-state-lookalike.compact (trimmed here). Unrelated baseline circuits and ledgers removed; original licence header retained where present. Paths in the output are shortened to the example folder.

## A freshness check never consumes the nullifier

Synthetic example 9 of 10. Rule: [nullifier-check-without-insert](https://nightshade.dicksonwu.xyz/rules/nullifier-check-without-insert.md). Severity: medium. Selection: Opt-in. Compiler profile: compact-0.34.0-zkir2.

The circuit checks that an identifier is unused but never inserts it into the used set.

### Flagged

vulnerable.compact, line 7 flagged:

```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.
```

### Lookalike

A local member function checks a value without any ledger set.

```compact
import CompactStandardLibrary;
export ledger accepted: Field;
witness token(): Field;
circuit member(id: Field): Boolean { return id == (0 as Field); }
export circuit accept(): [] {
  const id = token();
  assert(!member(id), "nonzero");
  accepted = disclose(id);
}
```

Output (exit code 0):

```text
$ nightshade lookalike.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.
```

Configuration (config.json):

```json
{
  "version": 1,
  "compilerVersion": "0.34.0",
  "zkirVersion": 2,
  "detectors": [
    "nullifier-check-without-insert"
  ]
}
```

Source fixtures at v0.1.1: https://github.com/DicksonWu654/nightshade/blob/v0.1.1/tests/corpus/vulnerable/nullifier-check-without-insert.compact, https://github.com/DicksonWu654/nightshade/blob/v0.1.1/tests/corpus/safe/nullifier-check-without-insert.compact, https://github.com/DicksonWu654/nightshade/blob/v0.1.1/tests/corpus/safe/nullifier-check-without-insert-lookalike.compact. Original compact fixture retained. Paths in the output are shortened to the example folder.

## A private commitment uses fixed randomness

Synthetic example 10 of 10. Rule: [predictable-commitment-randomness](https://nightshade.dicksonwu.xyz/rules/predictable-commitment-randomness.md). Severity: medium. Selection: Audit default. Compiler profile: compact-0.34.0-zkir2.

Publishing a commitment with fixed randomness can expose a small private input domain to guessing.

### Flagged

vulnerable.compact, line 6 flagged:

```compact
pragma language_version >= 0.26.0;
import CompactStandardLibrary;
export ledger published: Bytes<32>;
witness secret(): Field;
export circuit publish(): [] {
  published = persistentCommit<Field>(secret(), pad(32, ""));
}
```

Output (exit code 1):

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

MEDIUM — Public commitment uses predictable randomness [predictable-commitment-randomness]
vulnerable.compact:6:3
  6 |   published = persistentCommit<Field>(secret(), pad(32, ""));
    |   ^
persistentCommit commits private-derived input using statically known randomness, and its result influences ledger-write published. This removes the protection supplied by secret, unpredictable commitment randomness; low-entropy inputs can remain guessable. Intentional deterministic commitments require review.
Source: vulnerable.compact:6:15
Call path: publish
Remediation: Use independently generated, sufficiently entropic private randomness appropriate to the primitive and protocol. Do not replace intentional deterministic protocol commitments without reviewing compatibility.

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

Take commitment randomness from a witness instead of a constant.

```compact
pragma language_version >= 0.26.0;
import CompactStandardLibrary;
export ledger published: Bytes<32>;
witness secret(): Field;
witness randomness(): Bytes<32>;
export circuit publish(): [] {
  published = persistentCommit<Field>(secret(), randomness());
}
```

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.
```

Configuration (config.json):

```json
{
  "version": 1,
  "compilerVersion": "0.34.0",
  "zkirVersion": 2,
  "detectors": [
    "predictable-commitment-randomness"
  ]
}
```

Source fixtures at v0.1.1: https://github.com/DicksonWu654/nightshade/blob/v0.1.1/tests/corpus/vulnerable/predictable-randomness.compact, https://github.com/DicksonWu654/nightshade/blob/v0.1.1/tests/corpus/safe/predictable-randomness.compact. Original compact fixture retained. Paths in the output are shortened to the example folder.

## How these were produced

[Download the proof pack](https://nightshade.dicksonwu.xyz/downloads/nightshade-proof-0.1.1.tar.gz) (`nightshade-proof-0.1.1.tar.gz`, 1.7 MB, 4692 files). SHA-256: `9d95e631dc318006610882911c0d58b7c25fa7754c39b49205c309d2e2e57b3b`

It holds the synthetic input snapshot, every raw scan output with its recorded command and exit code, the per-scan configs, these ten examples, the report and the scripts that produced and check them. Local paths in it are replaced with placeholders such as `<pack>` and `<compact-toolchains>`, the release tarball is left out (it is the v0.1.1 release asset) and real-contract records keep only the aggregate numbers on the [evaluation](https://nightshade.dicksonwu.xyz/evaluation.md) page. `PUBLIC-PACK.md` inside lists every change.

Each example is a synthetic contract written for the Nightshade test corpus. Some are deliberate mutations of upstream teaching examples. None of them is a finding about a real project.

Each scan selects only the named rule through the example's `config.json` and uses the compiler profile `compact-0.34.0-zkir2`. The `--compiler` flag adds compiler validation (`--skip-zk` compilation with Compact 0.34.0). Normal scans do not need a compiler. Some of these rules are opt-in; the configuration selects them explicitly.

Outputs are copied from the proof run. The first line of each output shows the command as you would type it: the recorded run called the installed binary by its full path under `taskset` and passed a local compiler path, which I replaced with `nightshade` and `/path/to/compactc`. In the output itself I shortened absolute file paths to paths relative to the example folder. Long lines wrap on screen. Nothing else is changed. Each example links its source fixture in the repository at v0.1.1; where the showcase file was trimmed, the fixture is the untrimmed original.

A quiet corrected or lookalike scan shows that this one rule stopped firing. It does not show that the contract is secure. For the corpus-wide results, including misses, see [evaluation](https://nightshade.dicksonwu.xyz/evaluation.md).