PaperlayerView exact revision on arXiv

Source-linked AI summary

Sound Debloating of Redundant Checks in Zero-Knowledge Machine-Learning Circuits

Zhantong Xue, Pingchuan Ma, Zhaoyu Wang, Yuguang Zhou, Huaijin Wang, Shuai Wang

arXiv:2609.10149v1cs.CR

TL;DR

ZK-ML circuits contain redundant well-formedness checks, but removing them must not admit witnesses the original circuit rejects. This paper uses whole-circuit abstract interpretation and provenance-guided proof search to justify removals. Across its evaluated circuits, it removes constraints and reduces proving time while preserving the witness set.

  • Problem

    Well-formedness checks can become redundant across composed gadgets, but removing them unsafely can admit witnesses that do not satisfy the original circuit.

    Source: §1 · p. 2, §3.1 · p. 4

  • Method

    Whole-circuit abstract interpretation derives facts and a provenance graph tracks their derivations, allowing checks to be removed only when survivors still entail them.

    Source: §3.3 · pp. 4–5

  • Results

    Across ezkl and zkml circuits from four architecture families, the tool removes 25.5% of constraints and reduces proving time by 33.4% on average while preserving the witness set.

    Source: §1 · p. 2, §9 · p. 12

  • Takeaways & Limitations

    The debloated circuit preserves the original witness set while reducing constraint count and proving time in the evaluated circuits.

    Source: §9 · p. 12

    The sound polynomial-time analysis is incomplete and may miss redundant checks.

    Source: §7 · p. 11

Abstract

from arXiv · show

Zero-knowledge (ZK) proof systems for neural-network inference compile the model into a system of arithmetic constraints. Many of these constraints are redundant checks: range proofs, sign lookups, and bit decompositions who are globally entailed by the rest of the circuit through chains of reasoning that span distant gadgets. Removing them shrinks the circuit and accelerates proving, but the removal must be carefully justified: an unsoundly debloated circuit becomes forgeable, accepting witnesses the original would have rejected and so allowing a prover to claim, for example, that a neural network produced an output it never actually computed. Such soundness vulnerabilities are not hypothetical: under-constrained circuits in deployed ZK systems have enabled attackers to forge transactions and bypass verification entirely. We present an automated framework that removes redundant checks while provably preserving soundness. For each candidate removal, our tool first checks whether the rest of the circuit, on its own, can still rule out every value the removed check was excluding. Using whole-circuit abstract interpretation, the analysis searches for such alternative justifications and records them in a provenance graph; a check is then removed only when an alternative path through the graph still derives the facts that it is checking. This ensures that the debloated circuit opens no new forging strategy to an adversary. We evaluate circuits spanning MLP, CNN, RNN, and transformer architectures generated by two production frameworks (ezkl and zkml), with up to 25.3 million constraints. Our tool removes up to 48.7\% of constraints and reduces prover time by up to 72.8\%, without weakening security.

1 Introduction

ZK-ML circuits contain many well-formedness checks, and composition can make checks redundant across gadgets. The paper presents a sound method for identifying and removing such checks while preserving security.

Motivation

  • Well-formedness checks can account for up to 48.7% of constraints and include activation range checks, sign lookups, division remainder bounds, and bit-decomposition proofs.These checks restrict admissible assignments rather than compute values.Source: §1 · p. 1
  • Composition can make a check redundant when another check on the same variable already enforces a tighter range.For a ReLU output z, a downstream range bound R_rng ≤ R_relu implies the upstream bound [0, R_relu].Source: §1 · p. 2

Debloating & ZK ML security

  • Sound removal is essential because unsound debloating can admit witnesses rejected by the original circuit, enabling a verifier to accept a forged inference proof.Soundness requires every witness accepted by the debloated constraints to satisfy the original constraints.Source: §1 · p. 2, Figure 1 · p. 2

Challenges

  • Redundancy may depend on constraints several layers away, and exact entailment checking is co-NP-hard even for a single constraint.Two checks can each be redundant alone yet unsafe to remove together when each derivation relies on the other.Source: §1 · p. 2

Our solution

  • Whole-circuit abstract interpretation derives facts about variables, while provenance tracking records their constraint-based derivations for proof search.A check is removed only when every fact it enforces remains derivable; cycle detection excludes circular mutual derivations.Source: §1 · p. 2
  • 25.5% of constraints are removed on average and proving time falls by 33.4% on average, with maxima of 48.7% and 72.8%, respectively.The evaluation covers MLP, CNN, RNN, and transformer circuits from ezkl and zkml, scaling to 25.3 million constraints.Source: §1 · p. 2

2 Background

ZK systems encode computation as constraints over a finite field, while ZK-ML frameworks compile quantized model operations into shared-variable gadgets. Their well-formedness checks create semantic redundancies that existing syntactic or algebraic optimizers generally do not detect.

2.1 Constraints in ZK Proof Systems

  • Both R1CS and PLONKish represent witness assignments over a field, but differ in constraint form; PLONKish uses gates, lookups, and copy constraints.R1CS expresses quadratic identities, while PLONKish organizes variables in a table with advice and fixed columns.Source: §2.1 · pp. 2–3

2.2 ZK Machine Learning Frameworks

  • ZK-ML frameworks compile quantized model operators into gadgets whose constraints share variables across adjacent operations, and every inference step must be constrained.Field arithmetic lacks IEEE floating-point semantics, so the toolchain represents real values as scaled integers and re-expresses operations over the prime field.Source: §2.2 · p. 3

2.3 Constraint Optimization in ZK Systems

  • Existing compiler and circuit-reduction tools mainly use syntactic or algebraic simplifications, whereas entailment-based debloating removes up to 48.7% of constraints on the benchmarks.The prior tools remove at most 0.4% on those benchmarks.Source: §2.3 · p. 3

3 Problem and Motivation

The paper formulates safe debloating as removing constraints only when the survivors entail them, then uses circuit examples to expose the global, compositional, and computational challenges. These challenges motivate whole-circuit reasoning with tracked derivations and careful removal.

3.1 Problem Formulation

  • A removal set R is safe when the remaining constraints entail every removed constraint, ensuring that the debloated system accepts no witness outside the original system.The ideal target is a maximum safe removal set, but exact computation is intractable.Source: §3.1 · p. 4

3.2 Motivating Example

  • In the motivating circuit, a downstream range check can subsume a ReLU bound, while other surviving bounds can force a decomposition digit to zero.The digit conclusion depends on the stated bounds and the low-digit check remaining in place.Source: §3.2 · p. 4

3.3 Design Challenges

  • Non-local subsumption means that proving a check redundant may require bounds from constraints elsewhere in the circuit, with information flowing in either direction.The paper uses worklist abstract interpretation to propagate facts to a fixpoint without a designated traversal direction.Source: §3.3 · p. 4
  • Premise asymmetry makes individually redundant checks unsafe to remove together when each check’s alternative derivation depends on the other.A provenance graph records alternate derivations, and proof search rejects circular dependencies.Source: §3.3 · pp. 4–5
  • Exact safe-debloating decisions are co-NP-hard for a single constraint, and optimizing across subsets is harder still.The proposed response is a polynomial-time sound over-approximation that grows removals greedily, reuses derivations, and targets proof obligations with a heuristic filter.Source: §3.3 · p. 5

4 Approach

The approach derives facts across the whole constraint system, records how they were proved, and removes a check only when its obligations remain derivable without it.

4.1 Abstract Interpretation over Constraints

  • Abstract interpretation tracks constants, signed intervals, and known bits, propagating constraints bidirectionally to a sound fixpoint while guarding against field wrap-around.Transfer rules contribute refinements only when the integer interpretation agrees with field arithmetic.Source: §4.1 · pp. 5–6

4.2 Provenance Graph

  • The provenance graph records facts and the constraints and premises deriving them, with minimal-premise trimming; its construction takes O(n·d^3) time.Facts are projected into lower-bound, upper-bound, and known-bits atoms so entailment checks can use the relevant fact granularity.Source: §4.2 · p. 6

4.3 Provenance-Guided Debloating

  • The filter proposes entailed checks, then cycle-aware AND/OR search removes each only if its obligations remain derivable under cumulative masking, preserving the original witness set.Unsupported constraint shapes are retained unless an implemented rule can certify them.Source: §4.3 · pp. 7–8
  • Because finding the largest removal set is coNP-hard, a greedy low-uniqueness-first order affects removal size, not soundness.Candidates with many alternative proofs are tried before those that uniquely support facts.Source: §4.3 · pp. 7–8

5 Implementation

The implementation handles R1CS and PLONKish circuits, orders candidate removals greedily, cleans up unreachable auxiliary structure, and mechanizes the soundness argument.

5 Implementation

  • R1CS circuits are loaded from Circom and emitted back to Circom, while PLONKish circuits are recorded during a mock-prover synthesis pass and rebuilt from JSON.Both formats use the existing prover and verifier unchanged.Source: §5 · p. 8
  • The loader assumes model weights in PLONKish advice columns are unknown, so the analysis does not use weight-specific optimizations.Source: §5 · p. 8
  • Candidates are ordered by how many facts they uniquely support, trying zero-score constraints with alternative proofs first.The uniqueness score is computed once from the initial provenance graph.Source: §5 · p. 8
  • A backward-reachability pass removes only unreachable auxiliary constraints, then prunes advice and fixed columns unused by surviving constraints.Source: §5 · p. 8
  • A Rocq development proves local soundness for implemented rules and checks emitted certificates; unsupported constraint shapes are retained unless a covered rule certifies removal.Source: §5 · p. 8

6 Evaluation

Across seven architectures and two compilation pipelines, the evaluation measures constraint reduction, proof-system impact, scalability, and comparisons with existing tools. The debloater finds substantial reductions across benchmarks, scales to large circuits, and outperforms the compared reduction methods.

6.1 Experimental Setup

  • The corpus covers seven architectures across ezkl and zkml where supported, with circuits ranging from approximately 6,000 to 25 million constraints.MobileNet-v2 runs only through ezkl; for some zkml models, the largest completed scale is used because of memory limits.Source: §6.1 · p. 9, §6 · p. 9

6.2 RQ1: Effectiveness

  • Constraint reductions span 3.20%–24.90% on ezkl and 22.30%–48.70% on zkml; all 13 pipeline–model pairs lose redundant constraints.The median reductions are 12.90% on ezkl and 40.25% on zkml.Source: Table 2 · p. 9, §6.2 · p. 10
  • Proving-time savings occur on every benchmark, with ranges of 1.10%–72.80% on ezkl and 16.80%–43.70% on zkml.Proof-size reductions range from 1%–74% on ezkl and 3%–46% on zkml; zkml primarily sheds lookup invocations, while ezkl’s largest gains come from pruning advice columns.Source: §6.2 · p. 10

6.3 RQ2: Scalability

  • Analysis time scales efficiently with circuit size, while reduction percentages stay stable across scale on both pipelines.Endpoint fits yield exponents of 0.90–1.70 on ezkl and 1.30–2.50 on zkml; a 38.40-million-constraint ezkl circuit completes in 2.90 hours. zkml reductions are especially stable, while some ezkl families decline modestly at high multipliers.Source: §6.3 · p. 10

6.4 RQ3: Comparison

  • Circom O2 and Distilling rely on algebraic simplifications, while Clap and korrekt test syntactic duplication or dead gates rather than entailment.The No-Graph ablation reaches the LSTM result but exhausts its four-hour budget on the other circuits; the provenance graph completes all five in 4 seconds to 11 minutes.Source: §6.4 · p. 11
  • Across five R1CS architectures, the tool achieves 15.90%–51.60% reduction, while syntactic tools reach at most 0.40% and Clap and korrekt remove nothing.Exact SMT terminates only on the 116-constraint MLP instance, matching the tool’s removal set after 11.4 hours; the tool computes it in 0.06 seconds.Source: Table 3 · p. 10, §6.4 · p. 11

7 Discussion

The analysis is sound but incomplete at the target scale, so it may miss redundant checks. Its scope and evaluation are bounded by cross-constraint soundness checks and prover memory for larger models.

Incompleteness

  • Polynomial-time approximations may miss redundant checks, although every removal is justified by provenance-guided proof search over surviving constraints.The analysis uses interval, known-bits, and constant domains, template-based entailment rules, and greedy removal; exact maximum debloating is intractable at the target scale.Source: §7 · pp. 11–12

Scope

  • The tool targets cross-constraint entailment among soundness checks, not algebraic simplifications, which existing passes can handle in a separate, composable pass.The two classes touch disjoint constraints.Source: §7 · p. 12

Generality on Non-ML Domains

  • The method consumes generic R1CS and PLONKish systems, but non-ML evaluation is absent and reductions there are expected to be smaller.The cited signature-verification and bignum examples range-check limb decompositions, while field arithmetic and Merkle-path hashing account for most constraints; porting requires domain-matched abstract domains and transfer functions.Source: §7 · p. 12

Scalability on Complex ML Models

  • BERT-tiny reductions remain stable as its circuit scales 32×, but evaluation beyond that scale is precluded by prover memory.The passage cites GPT-2 as requiring roughly 1 TB of RAM and describes the bottleneck as one for ZK ML at large, not for the analysis.Source: §7 · p. 12

8 Related Work

Prior work accelerates ZK inference, verifies neural networks, detects circuit under-constraint, or removes software redundancy. This debloater instead asks whether individual circuit constraints follow from the survivors.

ZK machine learning and acceleration

  • ZK-ML acceleration methods include folding, lookup arguments, GKR protocols, and hardware; debloating is a complementary post-pass.Those choices are made at authoring time or per operation, whereas this method removes constraints already redundant by composition.Source: §8 · p. 12

DNN verification

  • Neural-network verifiers prove input-output properties, while this work analyzes entailment in compiled ZK constraint systems, including lookups, copy constraints, and decompositions.The shared use of abstract domains does not make their analysis targets the same.Source: §8 · p. 12

Program analysis on ZK circuits

  • Circuit-analysis tools such as QED2, Coda, AC4, and Ecne detect under-constraint; this work asks whether particular constraints are needed to keep the witness set small.The analyses are complementary.Source: §8 · p. 12

Software debloating

  • Software debloaters operate over control-flow IRs; LClean is closer in shape, but uses per-label SMT entailment rather than a precomputed provenance graph.This setting has no control flow and requires exact witness-set preservation; the described method scales to 10^7 constraints.Source: §8 · p. 12

9 Conclusion

The paper concludes that provenance-guided abstract interpretation can remove redundant constraints while preserving the witness set. It reports the evaluation and provides its artifacts, alongside statements on ethics and generative AI use.

9 Conclusion

  • 25.5% of constraints were removed and proving time fell by 33.4% on average across ezkl and zkml circuits from four architecture families, while preserving the witness set.Source: §9 · p. 12

A Open Science

  • The complete Rust implementation and evaluation artifact are available, including the tool, circuit corpus, prover/verifier sources, experiment drivers, and results.Source: A Open Science · p. 14

B Ethical Considerations

  • The authors report no human subjects, personal data, or vulnerability disclosure, and foresee no negative ethical implications.Source: B Ethical Considerations · p. 14

C Generative AI Usage

  • The authors used OpenAI GPT and Anthropic Claude for proofreading, rephrasing, formatting, debugging, and implementation suggestions, then reviewed and verified generated content and code.Source: C Generative AI Usage · p. 15

D Proof Sketches

The proof sketches justify the analysis and removal procedure, while the walkthrough traces interval facts through abstract interpretation, provenance construction, and debloating. The appendix introduces three benchmark cases that isolate distinct removal mechanisms.

D Proof Sketches

  • Theorem 4.1's proof sketch gives O(nd^3) overall complexity, with O(d^2) work per constraint-fact pair.Source: D Proof Sketches · p. 15
  • Theorem 4.2's induction argues that provenance proof trees derive facts satisfied by any witness to the surviving constraints.Source: D Proof Sketches · p. 15
  • Theorem 4.3's proof iterates sound removals in reverse order to show that satisfying the reduced system implies satisfying the original.Source: D Proof Sketches · p. 15

E Illustrative Walkthrough

  • In the walkthrough, interval propagation tightens z to [0, 5], and provenance-guided filtering removes c_relu and c_x while retaining c_rng and c_y.The c_y derivation would require c_x and then c_y itself, so cycle detection retains it.Source: E Illustrative Walkthrough · p. 15

F Case Studies of Removed Constraints

F.1 Range subsumption (zkml/MNIST-MLP)

Three range-subsumption patterns explain nearly all lookup trims in the zkml/MNIST-MLP benchmark: a surviving constraint already pins each removed lookup’s variable to a sufficient range.

F.1 Range subsumption (zkml/MNIST-MLP)

  • Of 791 removed constraints, 788 are lookups; nearly all lookup trims follow three patterns where another constraint already pins the variable’s range.Figure 5 marks the redundant lookups with dashed boxes.Source: §F.1 · p. 15, Figure 5 · p. 15
  • A ReLU lookup pins its output to [0, 128], making a downstream check against the wider interval [0, 256] redundant.The downstream check is on the same variable.Source: §F.1 · pp. 15–16
  • The ReLU bound x ∈ [0, 128] implies the Packer’s shifted-value check x+128 ∈ [0, 256].The bound gives x+128 ∈ [128, 256], which is contained in the checked interval.Source: §F.1 · p. 16
  • In VarDiv, the gate fixing b=16 and lookup on 2b−r together imply r ∈ [0, 32], making the standalone r-lookup redundant.When the divisor’s constant value is independently provable, the divisor-fixing gate can also be dropped, removing two constraints per such VarDiv.Source: §F.1 · p. 16

F.2 Activation-bound cascade (ezkl/BERT-tiny)

The section traces how range bounds trigger removable constraints in BERT-tiny and PTB-LSTM, then describes adversarial testing of the debloater and the limits of that sampling cross-check.

F.2 Activation-bound cascade (ezkl/BERT-tiny)

  • On BERT-tiny, 715,517 of 2.87 M post-merge constraints are removed through two cascades seeded by an upstream range bound on x.The analysis leaves all 309,696 dot-product gates intact because ezkl’s private model weights remain unknown to it.Source: §F.2 · p. 16
  • One BERT-tiny cascade discharges two mask-enforcing gates when the upstream bound pins the activation input to zero or excludes zero.The other subsumes one lookup in each matched sign-and-digit pair; when that lookup’s input is pinned to a constant, rewriting it as an equality gate accounts for 101,439 gate trims.Source: §F.2 · p. 16

F.3 Recurrent amplification (zkml/PTB-LSTM)

  • PTB-LSTM removes 15,240 of 31,280 post-merge constraints, with repeated LSTM gadget infrastructure across timesteps amplifying the range-subsumption patterns.The trims include 11,200 from intra-VarDiv, 4,000 from Packer-after-activation, and 40 terminal output range checks; computational-core constraints survive.Source: §F.3 · p. 16, Figure 7 · p. 16

G Empirical Soundness Validation

  • The debloater commits to a removal only when its AND/OR provenance graph shows an alternative proof for every fact supported by that constraint.The study is an independent cross-check of the pipeline, intended to detect implementation bugs rather than extend the soundness arguments.Source: G Empirical Soundness Validation · p. 16

G.1 Test design

  • For each pipeline-model pair, testing compares pre- and post-debloat constraint sets by perturbing one advice cell in a removed lookup’s input.Perturbations target values just outside the lookup’s integer range or field wrap-around values; the loop is random but coverage-prioritized, testing each removed lookup at least once within a three-day budget.Source: §G.1 · p. 16
  • The testing pipeline is a sampling cross-check, not a soundness proof, and does not test coordinated multi-cell witnesses.Coverage is at least once per removed lookup, not exhaustive across rows or attack patterns; worst-case soundness rests on the proofs, not this study.Source: §G.1 · p. 17

G.2 Results

Across all 13 pipeline-model pairs, adversarial testing found zero divergences between the original and debloated circuits, with every removed lookup tested at least once.

G.2 Results

  • Every removed lookup was tested at least once, and removed lookups on the smaller zkml side were typically tested thousands of times.Source: §G.2 · p. 17
  • Across 13 pipeline-model pairs, 3.62 × 10^11 adversarial iterations found zero divergences between the original and debloated circuits.Table 4 reports the empirical soundness validation results.Source: Table 4 · p. 17, §G.2 · p. 17

Related papers

Loading 2609.10149v1…