Releases: btq-ag/keelung-compiler
v0.23.0
What’s New?
Introducing 4 new arithmetic operators for UInt!
add :: UInt w -> UInt w -> UInt (w + 1)
addV :: [UInt w] -> UInt v
mul :: UInt w -> UInt w -> UInt (w * 2)
mulV :: UInt w -> UInt w -> UInt vThere are two operators for addition and two for multiplication.
You can probably guess the functions of these operators from their type signatures.
Limitation of the existing operators
The existing addition and multiplication operators have type signatures as follows:
(+) :: UInt w -> UInt w -> UInt w
(*) :: UInt w -> UInt w -> UInt wThese operators produce unsigned integers with fixed widths that must match those of their operands. This can lead to overflow if the values of the operands are too large, with no means to salvage the overflowed bits. That's why we're introducing new operators that allow you to choose the result widths for addressing these limitations.
Let’s take a closer look.
Full Sum Addition
add :: UInt w -> UInt w -> UInt (w + 1)As the name suggests, this function produces a slightly longer unsigned integer with the carry bit preserved.
Example usage:
example :: Comp (UInt 9)
example = do
x <- input Public
y <- input Public
return (x `add` y)Variable-width Batch Addition
addV :: [UInt w] -> UInt vThis is the most general form of addition, allowing you to sum a batch of unsigned integers and decide how many carry bits you want to preserve or discard. The result will be zero-extended if it is longer than expected, and truncated if it is shorter than actually produced.
Example usage:
example :: Comp (UInt 10)
example = do
x <- input Public :: Comp (UInt 8)
y <- input Public
z <- input Public
return [x, y, z]Full Product Multiplication
Similar to add, but for multiplication. It produces an unsigned integer double the width of its operands, allowing the full product of multiplication to be preserved.
Example usage:
example :: Comp (UInt 16)
example = do
x <- input Public
y <- input Public
return (x `mul` y)Variable-width Multiplication
This is the most general form of multiplication, allowing you to multiply two unsigned integers and decide how many carry bits you want to preserve or discard. The result will be zero-extended if it is longer than expected, and truncated if it is shorter than actually produced.
Example usage:
example :: Comp (UInt 12)
example = do
x <- input Public :: Comp (UInt 8)
y <- input Public
return (x `mulV` y) -- 4 higher bits discardedWhat Else?
As always, bug fixes and performance improvements!
Noticeably, unsigned integer division/modulo should produce less number of constraints that before.
What’s Next?
- User-defined datatypes with (automatically) structured input/output: Instead of using lists for representing input/output, we want something more structured, like JSON values!
- Smarter witness generation + user-programmable hints for witness generation.
v0.22.0
What’s New?
sliceandjoinoperator- Compilation speedup
slice and join operator
We've found that cryptographic primitives, such as hashing functions, are largely about shuffling bits around. Therefore, we have introduced two new operators for manipulating bit arrays (i.e. UInt).
slice for bit array slicing
slice :: UInt w -> (Int, Int) -> UInt vslice takes an unsigned integer UInt w, along with a range, and returns a slice UInt v of that integer. The range is inclusive at the start and exclusive at the end.
For example, here’s a program that slices the 3rd and 4th bits off a byte:
program :: Comp (UInt 2)
program = do
x <- input Public :: Comp (UInt 8)
return $ slice x (2, 4)join for bit array concatenation
join :: UInt u -> UInt v -> UInt (u + v)The join function concatenates two unsigned integers, UInt u and UInt v, producing a new unsigned integer UInt (u + v). This function combines the bit representations of the two input unsigned integers into a single unsigned integer whose width is the sum of the widths of the two inputs.
For example:
program :: Comp (UInt 8)
program = do
u <- input Public :: Comp (UInt 2)
v <- input Public :: Comp (UInt 6)
return $ u `join` vCompilation Speedup
You should notice a nice speedup when compiling programs that involve a lot of UInts.
Polynomials play a central role in the compiler, as they represent constraints and relations within a program. These data structures have internal states (or invariants) that require maintenance after each operation, and it can really slow things down if this maintenance is not performed properly.
We've recently managed to improve the invariant maintenance of the polynomial insertion operation, making it 9 times faster.
We recognize that there are still other performance bottlenecks within the compiler, and we plan to continue optimizing them in future releases.
What’s Next?
- API of the R1CS Witness Solver: We’ve been using the witness solver as a means of testing the correctness of the compilation. We believe that this tool will also greatly aid the testing and development of Keelung programs.
- Make the R1CS witness solver smarter.
- Optimization for the implementation of AES in the standard library.
v0.21.0
What’s New?
- A new reference counter
- Functions for converting datatypes
New Reference Counter
Most programming languages today feature automatic garbage collection, so that programmers don’t have to manage memory manually. Keelung a bit differently since we don't deal with memory, but we do manage something equally important: variables.
Variable Allocation/De-allocation
The compiler allocates variables for each input and output in a Keelung program, as well as when users define computations or constraints between variables.
However, not every variable proves to be essential; many of these variables will be eliminated by the optimizer at a later stage.
Variable Renaming/Reindexing
Variables in the constraint system are indexed by integers. Some of these indices may be skipped after optimization, creating empty “holes” in the constraint systems.
To address this, we reassign variables with new indices so that no numbers are skipped, and the constraint system becomes compact again.
Reference Counting
To identify which variables are skipped, we keep track of each variable's occurrence within a constraint system. This allows us to remove variables whose counts drop to zero.
Precise Counting of Unsigned Integer Bits
However, in our previous implementation, we treated each unsigned integer as a singular variable, resulting in all bit variables of an unsigned integer being retained, even if only a subset was actually used elsewhere.
We've addressed this issue by implementing a new reference counter that differentiates between the individual bits of an unsigned integer. This allows for precise reference counting without compromising the counter's performance.
Datatype conversion
The functions for converting between the primitive datatypes have been rewritten and renamed:
fromField: Field → Comp n (UInt w)toField: UInt w → Comp n FieldfromBools: [Boolean] → Comp n (UInt w)
You'll notice that all operations are centered around UInt in this design: Field ↔ UInt ↔ Boolean. For example, if you want to convert [Boolean] into UInt, you need to convert it into UInt first.
Check out our documentation site for more on how to use them!
What’s Next?
- Operators for slicing and joining unsigned integers (
join,slice, …) - Optimization for the implementation of AES
v0.20.0
What’s New?
Well, not much. At least you won’t feel it at the moment. But we have integrated a new optimizer specialized for UInts!
What is this for?
The core of Keelung’s constraint optimizer is the Union-Find data structure.
This data structure allows us to maintain the relationship between variables, so that we can substitute one for another, thereby reducing the number of variables and constriants.
For example, if we have two constraints: A = B and C = D. We can use Union-Find to construct two equivalence classes:
And if later we learn that A = C:
Then the original two equivalence classes would be united into a larger equivalence class like this:
This way, we can substitute A, B, and C with D every time we see them in the constraint system.
What’s the problem?
Union-Find only works on individual variables like A and B in our example, which is fine for variables of Field and Boolean. However, UInts are a different story – they're bit arrays under the hood.
If we want to maintain the relationship between UInt variables, we need something more powerful then the traditional Union-Find.
How to solve this?
After weeks of development, we’ve came up with a generalized version of the Union-Find data structure. This new data structure allows us to effectively manage the relationships between arrays of variables!
Let’s say we have unsigned integers A, B and C, and we learned that A[2 .. 7] = B[4 .. 9]:
Later, we also discovered that, B[6 .. 10] = C[5 .. 9]:
From this, we can create three new equivalence classes based on the initial ones:
A[2 .. 3] = B[4 .. 5]A[4 .. 7] = B[6 .. 9] = C[5 .. 8]B[10] = C[9]
How does this impact the compilation?
Consider the UInt left shift operation. Previously, each bit had to be associated individually, as shown below:
Now, this operation can be performed using just one equivalence class:
This approach significantly speeds up the compilation process. Instead of maintaining multiple equivalence classes, which are proportional to the width of UInt, it now requires just one. This simplification also allows potential optimizations on UInts to kick in, resulting in less constraints.
What’s next?
Our next step is to rewrite the compilation of UInt operators to leverage the capabilities of our new optimizer.
The upcoming version should also come with a new linker that allows variables and constraints to be arranged in a much more compact manner.
Stay tuned for more exciting development of Keelung!
v0.19.1
v0.19.0
What's new?
Binary field compilation
Keelung now supports compilation over any prime field or binary extension field!
What is this for?
This update enables developers to utilize proving systems that are optimized for binary fields. In binary fields, operations like XOR are inherently more efficient, leading to a reduction in constraints when compared to prime fields. For applications that heavily rely on such operations, adopting binary fields can lead to substantial performance improvements.
How to enable this?
To switch to binary fields, simply replace the FieldType in your commands:
compile gf181 program [...] [...] -- prime fields
compile (Binary 283) program [...] [...] -- binary fieldsAnd that’s all it takes!
Checkout the documentation if you want to know more about FieldType.
What's Next?
The integration of Snarkjs/Circom’s toolchain should be around the corner, as we’ve made a lot of progress in the past few weeks.
Stay tuned for the coming releases!
v0.18.0
What's New?
(Experimental) Snarkjs Compatiblity
Two new commands that can be invoked from GHCi have been added: genCircuitBin and genWtns, which generate R1CS circuit files and witness files in Snarkjs' formats repecively. Read our doc to know how to use them
For now, Keelung defaults to using the Aurora protocol. However, we have broader industry use cases in mind, such as Groth16 and PLONK. Our integration with Snarkjs, a powerful tool for generating and verifying proofs using Groth16 and PLONK protocols, will save us from reinventing the wheel.
The key to the integration lies in Snarkjs' R1CS and witness formats, which differ from ours.
Again, you can find detailed instructions for using these commands and what to do with the generated files using Snarkjs in our documentation.
Notes & Warning
Caution: Snarkjs-related functionalities currently have known issues and are not considered production-ready. One of the primary challenges is a bug in Snarkjs that prevents it from generating correct zkeys. As a result, proof generation and verification with Keelung and Snarkjs are not currently feasible.
What's Next?
We're currently working on compiling constraint systems for binary fields. Certain operations, like XOR, are more efficient in binary fields, making it a sensible choice to develop your application using proofing systems tailored to these fields. You'll have the flexibility to target any binary field of your choice by specifying the irreducible polynomial for that field. Stay tuned for more updates!
v0.17.0
What's new?
Carry-less Division/Modulo
(This image actually represents carry-less multiplication. We couldn't find an image for carry-less division and modulo, but they operate in a similar, opposite fashion. (source: [Wikipedia)
Following the introduction of carry-less multiplication, we're excited to present carry-less division and carry-less modulo.
What is it?
Carry-less division performs schoolbook long division on two UInt numbers and discards all carry values generated in the process.
What for?
When combined with carry-less multiplication and addition (bitwise XOR), we can effectively simulate binary field arithmetic on prime fields.
How to use it?
Like the "carry-preserving" division/modulo on UInts. They are expressed with the performCLDivMod statement in the Comp monad.
performCLDivMod ::
KnownNat w =>
-- | The dividend
UInt w ->
-- | The devisor
UInt w ->
-- | The quotient and remainder
Comp (UInt w, UInt w)The quotient and remainder are computed together, as demonstrated in this example:
program :: Comp (UInt 32)
program = do
dividend <- input
divisor <- input
(quotient, remainder) <- performCLDivMod dividend divisor
return quotientSimilar to assertDivMod, there's also an assertion called assertCLDivMod for making carry-less division/modulo relations.
What's Next?
Our next focus is on accelerating the integration with the Snarkjs/Circom toolchain.
Stay tuned for the coming releases!
v0.16.0
What's new?
Carry-less Multiplication
We are introducing Carry-less multiplication into Keelung.
What is it?
Carry-less multiplication (also known as XOR multiplication) takes two UInt numbers and multiplies them by performing schoolbook long multiplication, except that all carries are discarded along the way.
What for?
Carry-less multiplication allows us to simulate multiplication of binary fields on prime fields. It's a critical component for implementing cryptographic primitives like the AES cipher.
Intel even has an instruction set called CLMUL with specialized hardware dedicated to accelerate this operation!
How to use it?
It is defined as an infix operator .*. on unsigned integers UInt.
(.*.) :: KnownNat w => UInt w -> UInt w -> UInt wSimply drop them in between two UInt like you would with normal multiplication:
example :: Comp (UInt 8)
example = do
x <- input Public
y <- input Public
return $ x .*. y .*. 42What's Next?
The carry-less modulo is the next operator on our roadmap after the multiplication operator. We’re also working on integrating with the Snarkjs/Circom toolchain to streamline witness generation.
Stay tuned for more exciting developments in the coming releases!
v0.15.0
What's new?
Command Line Interface (CLI)
Previously, commands like compile or verify were only available in the GHCi REPL as Haskell functions for testing and interactive development. Now, all of these commands have command-line counterparts, making it easier to compile or generate proofs directly from your terminal or scripts!
Check out our new CLI documentation for more information!
Program entry point
In order to connect your Keelung program to the Haskell main function for CLI execution, you'll need a function like this:
keelung :: Comp t -> IO ()Which allows you to mount your program onto main:
main :: IO ()
main = keelung yourProgramBigInt Multiplication Compilation Improvement
In this release, we've made significant improvements to big unsigned integer multiplication. You should notice a considerable reduction in the number of constraints generated.
What's Next?
Our upcoming plans include the integration of Circom/Snarkjs witness generation into Keelung. This integration will allow Keelung to target Circom/Snarkjs as backends.
We hope these updates will enhance your Keelung experience. Stay tuned for more exciting developments!