Examples · Nightshade

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.

01Private authentication preimage reaches the public ledgerledger-bound-preimage-publicationmedium
02A public key comparison does not prove ownershipspoofable-authorizationhigh
03The signature verification result is discardedignored-validation-resultmedium
04Caller time needs a chain-time boundfreshness-bound-caller-timemedium
05Initialization can run repeatedlyre-initializationlow
06Two shielded mints reuse the same descriptorduplicate-shielded-mintmedium
07The Merkle membership result is ignoredmerkle-membership-not-enforcedmedium
08An unchecked witness value becomes public stateunconstrained-witness-to-statemedium
09A freshness check never consumes the nullifiernullifier-check-without-insertmedium
10A private commitment uses fixed randomnesspredictable-commitment-randomnessmedium

Private authentication preimage reaches the public ledger#

Synthetic exampleledger-bound-preimage-publicationmediumAudit defaultcompact-0.34.0-zkir2

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

Flagged

Compactvulnerable.compactline 12 flagged

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.txtexit 1

$ 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. Changed lines are marked.

Compactcorrected.compactrule quiet

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));
}

corrected-output.txtexit 0

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

Compactlookalike.compactrule quiet

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

lookalike-output.txtexit 0

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

Source fixtures at v0.1.1

Flagged: tests/corpus/vulnerable/direct.compact
Corrected: tests/corpus/safe/hash-only.compact
Lookalike: tests/corpus/safe/ordinary-disclosure.compact

Files from this run

Configuration

JSONconfig.json

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

The command line is shortened from the recorded run to what you would type; the output below it is verbatim, with absolute file paths shortened to the example folder. Long lines wrap. Original compact fixture retained.

A public key comparison does not prove ownership#

Synthetic examplespoofable-authorizationhighAudit defaultcompact-0.34.0-zkir2

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

Flagged

Compactvulnerable.compactline 6 flagged

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

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

output.txtexit 1

$ 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. Changed lines are marked.

Compactcorrected.compactrule quiet

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);
}

corrected-output.txtexit 0

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

Compactlookalike.compactrule quiet

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);
}

lookalike-output.txtexit 0

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

Source fixtures at v0.1.1

Flagged: tests/corpus/vulnerable/spoofable-authorization.compact
Corrected: tests/corpus/safe/spoofable-authorization.compact
Lookalike: tests/corpus/safe/spoofable-authorization-lookalike.compact

Files from this run

Configuration

JSONconfig.json

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

The signature verification result is discarded#

Synthetic exampleignored-validation-resultmediumAudit defaultcompact-0.34.0-zkir2

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

Flagged

Compactvulnerable.compactline 23 flagged

// 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.txtexit 1

$ 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. Changed lines are marked.

Compactcorrected.compactrule quiet

// 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);
}

corrected-output.txtexit 0

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

Compactlookalike.compactrule quiet

// 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);
}

lookalike-output.txtexit 0

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

Source fixtures at v0.1.1

Flagged: tests/corpus/known-bugs/counter-ignored-validation-positive.compact (trimmed here)
Corrected: tests/corpus/known-bugs/counter-ignored-validation-corrected.compact (trimmed here)
Lookalike: tests/corpus/known-bugs/counter-ignored-validation-lookalike.compact

Files from this run

Configuration

JSONconfig.json

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

Caller time needs a chain-time bound#

Synthetic examplefreshness-bound-caller-timemediumAudit defaultcompact-0.34.0-zkir2

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

Flagged

Compactvulnerable.compactline 14 flagged

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.txtexit 1

$ 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. Changed lines are marked.

Compactcorrected.compactrule quiet

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;
}

corrected-output.txtexit 0

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

Compactlookalike.compactrule quiet

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;
}

lookalike-output.txtexit 0

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

Source fixtures at v0.1.1

Files from this run

Configuration

JSONconfig.json

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

Initialization can run repeatedly#

Synthetic examplere-initializationlowOpt-incompact-0.34.0-zkir2

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

Flagged

Compactvulnerable.compactline 3 flagged

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

output.txtexit 1

$ 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. Changed lines are marked.

Compactcorrected.compactrule quiet

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

corrected-output.txtexit 0

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

Compactlookalike.compactrule quiet

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

lookalike-output.txtexit 0

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

Source fixtures at v0.1.1

Flagged: tests/corpus/vulnerable/re-initialization.compact
Corrected: tests/corpus/safe/re-initialization.compact
Lookalike: tests/corpus/safe/re-initialization-lookalike.compact

Files from this run

Configuration

JSONconfig.json

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

Two shielded mints reuse the same descriptor#

Synthetic exampleduplicate-shielded-mintmediumAudit defaultcompact-0.34.0-zkir2

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

Flagged

Compactvulnerable.compactline 7 flagged

// 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.txtexit 1

$ 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. Changed lines are marked.

Compactcorrected.compactrule quiet

// 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);
}

corrected-output.txtexit 0

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

Compactlookalike.compactrule quiet

// 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);
}

lookalike-output.txtexit 0

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

Source fixtures at v0.1.1

Flagged: tests/corpus/known-bugs/sdk-duplicate-mint-positive.compact (trimmed here)
Corrected: tests/corpus/known-bugs/sdk-duplicate-mint-corrected.compact (trimmed here)
Lookalike: tests/corpus/known-bugs/sdk-duplicate-mint-lookalike.compact (trimmed here)

Files from this run

Configuration

JSONconfig.json

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

The Merkle membership result is ignored#

Synthetic examplemerkle-membership-not-enforcedmediumAudit defaultcompact-0.34.0-zkir2

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

Flagged

Compactvulnerable.compactline 7 flagged

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.txtexit 1

$ 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. Changed lines are marked.

Compactcorrected.compactrule quiet

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);
}

corrected-output.txtexit 0

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

Compactlookalike.compactrule quiet

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);
}

lookalike-output.txtexit 0

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

Source fixtures at v0.1.1

Files from this run

Configuration

JSONconfig.json

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

An unchecked witness value becomes public state#

Synthetic exampleunconstrained-witness-to-statemediumOpt-incompact-0.34.0-zkir2

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

Flagged

Compactvulnerable.compactline 7 flagged

// 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.txtexit 1

$ 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. Changed lines are marked.

Compactcorrected.compactrule quiet

// 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);
}

corrected-output.txtexit 0

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

Compactlookalike.compactrule quiet

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

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

lookalike-output.txtexit 0

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

Source fixtures at v0.1.1

Flagged: tests/corpus/known-bugs/sdk-witness-state-positive.compact (trimmed here)
Corrected: tests/corpus/known-bugs/sdk-witness-state-corrected.compact (trimmed here)
Lookalike: tests/corpus/known-bugs/sdk-witness-state-lookalike.compact (trimmed here)

Files from this run

Configuration

JSONconfig.json

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

A freshness check never consumes the nullifier#

Synthetic examplenullifier-check-without-insertmediumOpt-incompact-0.34.0-zkir2

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

Flagged

Compactvulnerable.compactline 7 flagged

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.txtexit 1

$ 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. Changed lines are marked.

Compactcorrected.compactrule quiet

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);
}

corrected-output.txtexit 0

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

Compactlookalike.compactrule quiet

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);
}

lookalike-output.txtexit 0

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

Source fixtures at v0.1.1

Files from this run

Configuration

JSONconfig.json

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

A private commitment uses fixed randomness#

Synthetic examplepredictable-commitment-randomnessmediumAudit defaultcompact-0.34.0-zkir2

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

Flagged

Compactvulnerable.compactline 6 flagged

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.txtexit 1

$ 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. Changed lines are marked.

Compactcorrected.compactrule quiet

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());
}

corrected-output.txtexit 0

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

Source fixtures at v0.1.1

Flagged: tests/corpus/vulnerable/predictable-randomness.compact
Corrected: tests/corpus/safe/predictable-randomness.compact

Files from this run

Configuration

JSONconfig.json

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

How these were produced#

Download the proof packnightshade-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 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.