Skip to content

docs: fix typos #32

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
crStiv wants to merge 3 commits into
base: main
Choose a base branch
from
Open

docs: fix typos #32

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
10ac750
Refactor GatesDef and update GatesGnark versions
crStiv Nov 3, 2025
7d6734f
Fix wording in CONTRIBUTING.md for clarity
crStiv Nov 3, 2025
bb583d8
Fix grammatical error in README.md
crStiv Nov 3, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion CONTRIBUTING.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ with the major components as follows:
dependencies.
- [`ProvenZK.lean`](./ProvenZk.lean): The entry point for the library itself.
- [`ProvenZK`](./ProvenZk): The components of the library. The main interface to
the library lives in this folder, and supporting functionality in subfolders
the library lives in this folder, and supporting functionality lives in subfolders
of this folder.

For a more detailed overview of the components provided by this repository,
Expand Down
3 changes: 2 additions & 1 deletion ProvenZk/Gates.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ def to_binary_12 (a : ZMod N) (d : Nat) (out : List.Vector (ZMod N) d): Prop :=
∃(hp : a.val < 2^d), out = (Fin.toBitsLE ⟨a.val, hp⟩).map Bool.toZMod


-- In gnark 8 the number is decomposed in a binary vector with the length of the field order
-- In gnark 8 the number is decomposed into a binary vector with the length of the field order
-- however this doesn't guarantee that the number is unique.
def cmp_8 (a b out : ZMod N): Prop :=
∃z w: Fin (binary_length N), z.val % N = a.val ∧ w.val % N = b.val ∧
Expand Down Expand Up @@ -113,3 +113,4 @@ def GatesGnark9 (N : Nat) [Fact (Nat.Prime N)] : Gates_base (ZMod N) := {
def GatesGnark12 (N : Nat) [Fact (Nat.Prime N)] : Gates_base (ZMod N) := { GatesGnark9 N with
to_binary := GatesDef.to_binary_12
}

2 changes: 1 addition & 1 deletion README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,7 @@ type from [Mathlib 4](https://leanprover-community.github.io/mathlib4_docs/).
For available operations please see the definitions in
[`Gates.lean`](./ProvenZk/Gates.lean).

The other main components of the library contain of multiple theorems to assist
The other main components of the library contain multiple theorems to assist
with the formal verification of circuits. These are as follows:

- `import ProvenZK.Binary`: The definition of the `Bits` type, as well as
Expand Down