Skip to content
View probatur's full-sized avatar

Achievements

Achievement: Pull Shark

Achievements

Achievement: Pull Shark

Block or report probatur

Block user

Prevent this user from interacting with your repositories and sending you notifications. Learn more about blocking users.

You must be logged in to block users.

Content in all repositories owned by your account will be closed.
Maximum 250 characters. Please don’t include any personal information such as legal names or email addresses. This note will only be visible to you.
Report abuse

Contact GitHub support about this user’s behavior. Learn more about reporting abuse.

Report abuse
probatur/README.md

Probatur

Machine-checked proofs that zero-knowledge circuits accept exactly what their rule allows: sound and complete, for every input, re-checkable with one command. A project of Next Ridge Solutions Ltd.

Published proofs

Repository What is proved
bigmult our BigMult circuit (4 × 64-bit limbs) computes exactly the integer product
bigmodinv our BigModInv circuit accepts exactly the modular inverse
longtoshortnoendcarry our carry-normalisation circuit accepts exactly the correct normalised form

Each covers a circom-bigint template that the 2022 public audit listed as "In Progress". Each proof is checked by the Rocq/Coq kernel and by an independent kernel checker, with no axioms, and rebuilds with docker build ..

Contact: probatur@nxridge.com

Popular repositories Loading

  1. bigmodinv bigmodinv Public

    Machine-checked (Rocq/Coq) soundness and completeness of our BigModInv circuit, a circom-bigint template the 2022 audit left 'In Progress'

    Rocq Prover

  2. bigmult bigmult Public

    Machine-checked (Rocq/Coq) soundness and completeness of our BigMult circuit, a circom-bigint template the 2022 audit left 'In Progress'

    Rocq Prover

  3. longtoshortnoendcarry longtoshortnoendcarry Public

    Machine-checked (Rocq/Coq) soundness and completeness of our LongToShortNoEndCarry circuit, a circom-bigint template the 2022 audit left 'In Progress'

    Rocq Prover

  4. probatur probatur Public

    Profile