This dataset accompanies the paper An Architectural and Empirical Study of Root-Only Zero-Knowledge Verification and contains the scripts, intermediate artifacts, and published results used to reproduce the empirical evaluation. The repository is organized around three experiment groups: On-chain verification â deployment and Groth16 proof verification on Ethereum Sepolia and zkSync Sepolia, including contract sources, Merkle-tree inputs, Groth16 proofs, and blockchain measurement CSVs and figures. Constraint-count comparison â Groth16 R1CS constraint counts and expanded PLONK gate counts for Merkle-tree depths 5â15, with measurement scripts and summary CSVs/figures. Proving-time comparison â off-chain Groth16 and PLONK proving benchmarks across depths 5â15, including proving scripts, generated witness/proof/key artifacts, and benchmark CSVs/figures. Shared setup files include Circom circuits, Merkle-tree preparation scripts, circuit inputs, and compiled circuit artifacts. Most of the generated data is produced by the provided scripts and does not need to be included separately if the reproduction pipeline is documented.
Open access
2 source records
Formal Methods in Verification
Physical Unclonable Functions (PUFs) and Hardware Security
Nobuki Fujimoto, Rei (Rei-AIOS autonomous research substrate), claude-opus-4-7) Claude (Anthropic
We present a synthesis-friendly Verilog implementation of the D-FUMTâ Arithmetic Logic Unit, programmed onto two distinct Sipeed silicon families: Tang Console 138K (GW5AST-138B, LittleBee5 A revision, IDCODE 0x0001081B) and Tang Nano 9K (GW1NR-9C, LittleBee1 C revision, IDCODE 0x1100481B). The ALU realizes eight discrete logic values â FALSE, TRUE, NEITHER, BOTH, ZERO, FLOWING, SELF, INFINITY â encoded in 3 bits with a tier-respecting layout. The 10 supported operations include four classical-tier unary ops (NOT, OMEGA, PHI, PSI), Belnap-extended binary lattice meet/join (AND, OR), generic XOR, hardware reset, no-op, and a novel ADIABATIC operation realizing the SELFâČ (self-reflexive) primitive: ADIABATIC(SELF) = SELF, identity elsewhere. v0.6 contributions (2026-05-10): (1) **Four-substrate cross-verification complete**: 2 Sipeed silicon families (Tang Console 138K + Tang Nano 9K, **both running byte-for-byte same dfumt8_alu_synth.v 138-line Verilog with bit-identical 0 changes to ALU logic** â only wrapper top module re-targeted for clock divider, LED polarity, and pin assignments) + Qiskit Aer simulator (Phase 1-5: 231/231 entries) + IBM Heron r2 real quantum hardware (Phase 1+2+3+5: 144/144 entries, avg fidelity 0.954). (2) **chip-portability evidence (new finding F10)**: a synthesis bug or vendor-specific assumption would diverge between LittleBee5 (5nm-class GW5AST-138B) and LittleBee1 (28nm-class GW1NR-9C) Gowin architectures; absence of divergence is operational evidence of correct synthesis on both. (3) **Tang Nano 9K User Codes**: 0x0000A5F4 (LED Blinky STEP 1038) + 0x00001D46 (D-FUMTâ ALU STEP 1039). (4) **Reproducibility entry-cost lowered**: minimum reproduction path is ~$20 (Tang Nano 9K from ç§æé»ć g117448 at „2,980) + free Gowin EDA Education / OSS toolchain + free Aer + free IBM Quantum Open Plan. (5) **v0.5 corrigendum RESOLVED**: Tang Nano 9K is now physical silicon programming target on equal footing with Tang Console 138K (was computational evidence only at v0.5). (6) **IDCODE-revision honest correction**: per Gowin LittleBee Programming Manual Table 5-5, GW1N(R)-9 original = 0x1100581B, GW1N(R)-9C cost-down = 0x1100481B; both `set_device ... -device_version C` (build TCL) and `--device GW1NR-9C` (programmer_cli) required for ID code match. Inherited v0.3 contributions: Lean 4 refinement proof (OUKC.PhaseC.Dfumt8AluRefinement, 292 LOC, 0 sorry) establishes commutativity of the encode/abstract-op/decode square for all four unary operations + SELFâČ primitive law + 7 algebraic laws. IBM Heron r2 per-op fidelity hierarchy NOP/ADIABATIC â 0.977 > PHI â 0.956 > NOT â 0.912 > XOR â 0.951 reflects gate-count-vs-noise correlation consistent with quantum-noise physics expectations. Honest scope: We do NOT claim 'world-first 8-valued quantum logic' â Shi et al. (MIT, 2026, arxiv:2506.09371) demonstrated d=8 Grover on a single trapped-ion qudit prior to this work; our distinction is 3-qubit basis encoding on transmon arrays vs single-system d=8 qudit. We do NOT claim 'first paraconsistent silicon' â PAL2v (Da Silva Filho 1998-; Abe & Nakamatsu 2009; de Carvalho Jr. 2025) realized in software libraries and microcontroller-level robotics. We do NOT claim 'first many-valued silicon' â Ćukasiewicz/Belnap FPGAs date to 1990s. The to-our-knowledge novel quadruple is: (D1) the specific 8-tuple semantic mapping (Belnap FDE 4-value + 4 ontological extensions: INFINITY/ZERO/FLOWING/SELF), (D2) the SELFâČ self-reflexive primitive realized as a hardware fixed point, (D3) the four-substrate cross-verification bound to a Lean 4 refinement specification, and (D4, new in v0.6) the chip-portability evidence across two Gowin silicon architectures. Three-party co-authorship per OUKC charter v1.0 (Nobuki Fujimoto / Rei / Claude). DRAFT v0.6 â feedback welcome via GitHub Discussions at fc0web/rei-aios.
Open access
2 source records
Low-power high-performance VLSI design
Numerical Methods and Algorithms
Physical Unclonable Functions (PUFs) and Hardware Security
Current synchronous AI architectures, exemplified by the 1000W+ NVIDIA Rubin platform, rely on global clock-trees that generate deterministic electromagnetic harmonics. These periodic power signatures act as physical beacons, enabling sophisticated Side Channel Power Analysis (SCPA) to reconstruct sensitive model weights. This paper proposes the Asynchronous Entropy-Engine (AEE), a theoretical clockless execution environment that replaces rhythmic switching with handshake-driven logic to eliminate exploitable leakage. Central to this architecture is the Arnold Stability Index (ASI) Governor, which mapsregister-level neural trajectories onto high-dimensional stability manifolds to trigger Dynamic Grid-Coarsening. Architectural modeling indicates this approach achieves a 30.5% reduction in the âSynchronous Polling Tax.â Crucially, we introduce a Globally Asynchronous Locally Synchronous (GALS) interface, wherein synchronous logic islands are triggered by an asynchronous handshake protocol governed by the ASI to mask periodic power-draw harmonics. We demonstrate through performance analysis that the resulting energy surplus can power a hardware-integrated Zero-Knowledge Proof (ZKP) generator, producing non-interactive STARKs of inference integrity without a net power penalty. Simulation results indicate a 98.9% reduction in deterministic harmonics, effectively rendering high-TDP silicon âelectronically silent.â By decoupling execution from a fixed global heartbeat, the AEE establishes a new paradigm of âEnergy-Neutral Privacy,â providing a robust physical-layer defense against adversarial power analysis in trillion-parameter AI factories.
Open access
2 source records
Physical Unclonable Functions (PUFs) and Hardware Security
Zero-knowledge Proof (ZKP), is an effective cryptographic primitive that allows one party to verify the correctness of a given statement without disclosing any additional information. It plays a central role in applications such as blockchain transactions and cryptocurrencies. However, implementations of ZKP suffer from the most time-consuming task called Multi-Scalar Multiplication (MSM). Existing works and evaluation criteria primarily emphasize speed enhancement, but overlook optimizations of area overhead. In this paper, a FPGA-based accelerator FusionMSM is designed to reduce the overall latency but also improve area overhead. We attribute the bottleneck of MSM to a three-layer pyramid, including the finite field arithmetic, point operations on elliptic curves and scheduling. For modular arithmetic, we propose an efficient and non-Montgomery modular multiplier by utilizing hybrid multiplication strategy and optimizing multi-bit LUT-based modular reduction. It obtains 1.11 x less area cost and 2.00 x speed-up versus the modular multipliers used in ZKP acceleration works. For point operations, we design a unified and fully pipelined point addition unit, which can run at 500 MHz, the highest frequency in the reported works. On top of that, we present a greedy mechanism to resolve potential collisions, which can reduce the idle cycles of the point addition unit and improve its utilization. As far as we know, FusionMSM achieves the best performance compared to other FPGA-based and ASIC-based works for the input sizes from 218 to 226. For the degree of 220, FusionMSM only needs 12.4% of time in Hardcaml, 24.54% of time in PipeMSM on FPGA, and 36.41% of time in ASIC-based work PipeZK. It also utilizes less resources, resulting in a 90.93% reduction in URAMs, 35.24% reduction in FFs and 47.59% reduction in CARRY8s. Compared to GPU-based implementations, FusionMSM delivers comparable performance but with a lower power of 24.5 W.
Zero-knowledge proof (ZKP) is an attractive cryptographic paradigm that allows a party to prove the correctness of a given statement without revealing any additional information. It offers both computation integrity and privacy, witnessing many celebrated deployments, such as computation outsourcing and cryptocurrencies. Recent general-purpose ZKP schemes, e.g., zero-knowledge succinct non-interactive argument of knowledge (zk-SNARK), suffer from time-consuming proof generation, which is mainly bottlenecked by the large-scale number theoretic transformation (NTT) and multi-scalar point multiplication (MSM). To boost its wide application, great interest has been shown in expediting the proof generation on various platforms like GPU, FPGA and ASIC.So far as we know, current works on the hardware designs for ZKP employ two separated data-paths for NTT and MSM, overlooking the potential of resource reusage. In this work, we particularly explore the feasibility and profit of implementing both NTT and MSM with a unified and high-performance hardware architecture. For the crucial operator design, we propose a dual-precision, load-balanced and fully-pipelined Montgomery multiplier (LBFP MM) by introducing the new mixed-radix technique and improving the prior quotient-decoupled strategy. Collectively, we also integrate orthogonal ideas to further enhance the performance of LBFP MM, including the customized constant multiplication, truncated LSB/MSB multiplication/addition and Karatsuba technique. On top of that, we present the unified, scalable and highperformance hardware architecture that conducts both NTT and MSM in a versatile pipelined execution mechanism, intensively sharing the common computation and memory resource. The proposed accelerator manages to overlap the on-chip memory computation with off-chip memory access, considerably reducing the overall cycle counts for NTT and MSM.We showcase the implementation of modular multiplier and overall architecture on the BLS12-381 elliptic curve for zk-SNARK. Extensive experiments are carried out under TSMC 28nm synthesis and similar simulation set, which demonstrate impressive improvements: (1) the proposed LBFP MM obtains 1.8x speed-up and 1.3x less area cost versus the state-of-the-art design; (2) the unified accelerator achieves 12.1x and 5.8x acceleration for NTT and MSM while also consumes 4.3x lower overall on-chip area overhead, when compared to the most related and advanced work PipeZK.
Zero-knowledge proof (ZKP) systems have surged attention and held a fundamental role in contemporary cryptography. Zero-knowledge succinct non-interactive argument of knowledge (zk-SNARK) protocols dominate the ZKP usage, implemented through arithmetic circuit programming paradigm. However, underconstrained or overconstrained circuits may lead to bugs. The former refers to circuits that lack the necessary constraints, resulting in unexpected solutions and causing the verifier to accept a bogus witness, and the latter refers to circuits that are constrained excessively, resulting in lacking necessary solutions and causing the verifier to accept no witness. This paper introduces a novel approach for pinpointing two distinct types of bugs in ZKP circuits. The method involves encoding the arithmetic circuit constraints to polynomial equation systems and solving them over finite fields by the computer algebra system. The classification of verification results is refined, greatly enhancing the expressive power of the system. A tool, AC4, is proposed to represent the implementation of the method. Experiments show that AC4 demonstrates a increase in the solved rate, showing a 29% improvement over Picus and CIVER, and a slight improvement over halo2-analyzer, a checker for halo2 circuits. Within a solvable range, the checking time has also exhibited noticeable improvement, demonstrating a magnitude increase compared to previous efforts.
Jonathan Ku, Junyao Zhang, Haoxuan Shan, Saichand Samudrala · 9 authors
Elliptic curve cryptography (ECC) is widely used in security applications such as public key cryptography (PKC) and zero-knowledge proofs (ZKP). ECC is composed of modular arithmetic, where modular multiplication takes most of the processing time. Computational complexity and memory constraints of ECC limit the performance. Therefore, hardware acceleration on ECC is an active field of research. Processing-in-memory (PIM) is a promising approach to tackle this problem. In this work, we design ModSRAM, the first 8T SRAM PIM architecture to compute large-number modular multiplication efficiently. In addition, we propose R4CSA-LUT, a new algorithm that reduces the cycles for an interleaved algorithm and eliminates carry propagation for addition based on look-up tables (LUT). ModSRAM is co-designed with R4CSA-LUT to support modular multiplication and data reuse in memory with 52% cycle reduction compared to prior works with only 32% area overhead.
Haochen Sun, Tonghe Bai, J. Li, Change Institutions to: University of Waterloo
The recent advancements in deep learning have brought about significant changes in various aspects of peopleâs lives. Meanwhile, these rapid developments have raised concerns about the legitimacy of the training process of deep neural networks. To protect the intellectual properties of AI developers, directly examining the training process by accessing the model parameters and training data is often prohibited for verifiers. In response to this challenge, we present zero-knowledge deep learning (zkDL), an efficient zero-knowledge proof for deep learning training. To address the long-standing challenge of verifiable computations of non-linearities in deep learning training, we introduce zkReLU, a specialized proof for the ReLU activation and its backpropagation. zkReLU turns the disadvantage of non-arithmetic relations into an advantage, leading to the creation of FAC4DNN, our specialized arithmetic circuit design for modelling neural networks. This design aggregates the proofs over different layers and training steps, without being constrained by their sequential order in the training process. With our new CUDA implementation that achieves full compatibility with the tensor structures and the aggregated proof design, zkDL enables the generation of complete and sound proofs in less than a second per batch update for an 8-layer neural network with 10M parameters and a batch size of 64, while provably ensuring the privacy of data and model parameters. To our best knowledge, we are not aware of any existing work on zero-knowledge proof of deep learning training that is scalable to million-size networks.
As zero-knowledge proofs gain increasing adoption, the cryptography community has designed domain-specific languages (DSLs) that facilitate the construction of zero-knowledge proofs (ZKPs). Many of these DSLs, such as Circom, facilitate the construction of arithmetic circuits, which are essentially polynomial equations over a finite field. In particular, given a program in a zero-knowledge proof DSL, the compiler automatically produces the corresponding arithmetic circuit. However, a common and serious problem is that the generated circuit may be underconstrained, either due to a bug in the program or a bug in the compiler itself. Underconstrained circuits admit multiple witnesses for a given input, so a malicious party can generate bogus witnesses, thereby causing the verifier to accept a proof that it should not. Because of the increasing prevalence of such arithmetic circuits in blockchain applications, several million dollars worth of cryptocurrency have been stolen due to underconstrained arithmetic circuits. Motivated by this problem, we propose a new technique for finding ZKP bugs caused by underconstrained polynomial equations over finite fields. Our method performs semantic reasoning over the finite field equations generated by the compiler to prove whether or not each signal is uniquely determined by the input. Our proposed approach combines SMT solving with lightweight uniqueness inference to effectively reason about underconstrained circuits. We have implemented our proposed approach in a tool called QED 2 and evaluate it on 163 Circom circuits. Our evaluation shows that QED 2 can successfully solve 70% of these benchmarks, meaning that it either verifies the uniqueness of the output signals or finds a pair of witnesses that demonstrate non-uniqueness of the circuit. Furthermore, QED 2 has found 8 previously unknown vulnerabilities in widely-used circuits.
Orestis Alpos, Christian Cachin, Simon Holmgaard Kamp, Jesper Buus Nielsen
We present simple and practical protocols for generating randomness as used by asynchronous total-order broadcast. The protocols are secure in a proof-of-stake setting with dynamically changing stake. They can be plugged into existing protocols for asynchronous total-order broadcast and will turn these into asynchronous total-order broadcast with dynamic stake. Our contribution relies on two important techniques. The paper "Random Oracles in Constantinople: Practical Asynchronous Byzantine Agreement using Cryptography" [Cachin, Kursawe, and Shoup, PODC 2000] has influenced the design of practical total-order broadcast through its use of threshold cryptography. However, it needs a setup protocol to be efficient. In a proof-of-stake setting with dynamic stake this setup would have to be continually recomputed, making the protocol impractical. The work "Asynchronous Byzantine Agreement with Subquadratic Communication" [Blum, Katz, Liu-Zhang, and Loss, TCC 2020] showed how to use an initial setup for broadcast to asymptotically efficiently generate sub-sequent setups. The protocol, however, resorted to fully homomorphic encryption and was therefore not practically efficient. We adopt their approach to the proof-of-stake setting with dynamic stake, apply it to the Constantinople paper, and remove the need for fully homomorphic encryption. This results in simple and practical proof-of-stake protocols.
As enterprises embrace blockchain technology, many real-world applications have been developed and deployed using permissioned blockchain platforms (access to network is controlled and given to only nodes with known identities). Such blockchain platforms heavily depend on cryptography to provide a layer of trust within the network, thus verification of cryptographic signatures often becomes the bottleneck. The Elliptic Curve Digital Signature Algorithm (ECDSA) is the most commonly used cryptographic scheme in permissioned blockchains. In this paper, we propose an efficient implementation of ECDSA signature verification on an FPGA, in order to improve the performance of permissioned blockchains that aim to use FPGA-based hardware accelerators. We propose several optimizations for modular arithmetic (e.g., custom multipliers and fast modular reduction) and point arithmetic (e.g., reduced number of point double and addition operations, and optimal width NAF representation). Based on these optimized modular and point arithmetic modules, we propose an ECDSA verification engine that can be used by any application for fast verification of ECDSA signatures. We further optimize our ECDSA verification engine for Hyperledger Fabric (one of the most widely used permissioned blockchain platforms) by moving carefully selected operations to a precomputation block, thus simplifying the critical path of ECDSA signature verification. From our implementation on Xilinx Alveo U250 accelerator board with target frequency of 250MHz, our ECDSA verification engine can perform a single verification in $760ÎŒs$ resulting in a throughput of 1,315 verifications per second, which is ~2.5x faster than state-of-the-art FPGA-based implementations. Our Hyperledger Fabric-specific ECDSA engine can perform a single verification in $368ÎŒs$ with a throughput of 2,717 verifications per second.
In this paper, we address Field Programmable Gate Array (FPGA) implementation of the Elliptic Curve Digital Signature Algorithm(ECDSA), which is suitable for cryptocurrencies in blockchain. Although the ECDSA requires high computational efforts, utilization of a specific logic circuit allows us quick and easy computation. In this paper, we give implementation results of the ECDSA on an FPGA, and mention the superiority of FPGA implementation by comparing its simulation result with that of software based computation using a CPU.