v0.25.0

What's New?

Custom Datatypes as Inputs/Outputs, and Their Conditional/Equality Predicates

Motivation

Before v0.24, every Keelung value/expression is of one of three 'native' Keelung types: Boolean, Field, or UInt (unsigned integer), as described in the documentation.
Originally a programmer might want to express complicated data structures in Keelung but find it troublesome to do so.
For example, one might want to define a structure like Person with multiple attributes attached instead of just using the three native types everywhere in their Keelung programs, for the sake of readability and maintainability.

data Person = Person {
  name   :: Field,
  number :: UInt 8,
  parent :: (Boolean, UInt 8)
}

Defining the structure as a Haskell datatype is intuitive, but the programmer might soon face some difficulties if they try to write a Keelung program with it. E.g., it is tedious to declare inputs of the circuit then assemble them as a Person, even more so if this process needs to be done multiple times for different sets of inputs.

inputPeople :: Comp ()
inputPeople = do
  name1         <- inputField Public
  number1       <- inputUInt Public :: Comp (UInt 8)
  hasParent1    <- inputBool Public
  parent1number <- inputUInt Public :: Comp (UInt 8)
  let person1 = Person name1 number1 (hasParent1, parent1numer)
  name2         <- inputField Public
  number2       <- ... -- tedious!

It seems that this process of declaring and assembling inputs can be generalized. Similarly, the programmer might face the same tediousness if they try to compare two values of type Person, or assert properties of one, for Keelung before v0.24 only supports equality predicate on native types.

Predicates for Free with Generic and Inputable typeclass instances

Luckily in v0.25, Keelung compiler makes use of Haskell's DeriveGeneric mechanism to generalize these predicates on custom datatypes. We represent these desired properties all in one Inputable typeclass:

class Inputable a where
  inputData :: InputAccess -> Comp a 
  condData  :: Boolean -> a -> a -> a 
  eqData    :: a -> a -> Boolean
  ...

We have seem that these properties seems generalizable, so Keelung has built-in datatype-generic Inputable instances, such that the programmers can get Inputable instances of their datatypes for free. Generally speaking, a datatype can get input functions, conditionals, and equalities for free if and only if it satisfy following conditions:

1. it is built on top of fields/booleans/ints,
2. it only has one constructor (i.e. it is not s sum type), and
3. it's Generic instance is derivable.

A simple record declaration like Person can be checked to fall under such category simply by

1. adding {-# LANGUAGE DeriveGeneric #-} at the start of the Haskell file to enable the GHC extension,
2. import GHC.Generics,
3. adding deriving Generic at the end of datatype declaration to derive their Generic instance, and
4. adding one line of instance declaration instance Inputable Person without actual instance definitions.

data Person = Person {
  name   :: Field,
  number :: UInt 8,
  parent :: (Boolean, UInt 8)
} deriving Generic

instance Inputable Person

Once this Keelung/Haskell program compiles, the Inputable instance is generated, so instead of a tedious Keelung program sameParent that treats every component of Person separately,

sameParent :: Comp Boolean
sameParent = do
  name1         <- inputField Public
  number1       <- inputUInt Public :: Comp (UInt 8)
  hasParent1    <- inputBool Public
  parent1number <- inputUInt Public :: Comp (UInt 8)
  name2         <- inputField Private
  number2       <- inputUInt Private :: Comp (UInt 8)
  hasParent2    <- inputBool Private
  parent2number <- inputUInt Private :: Comp (UInt 8)
  return (eq hasParent1 hasParent2 .&. eq parent1number parent2number)

we can now treat Person as one of the native Keelung types, using inputData and eqData similarly to their native counterparts to greatly simplify the program:

data Person = Person {
  name   :: Field,
  number :: UInt 8,
  parent :: (Boolean, UInt 8)
} deriving Generic

instance Inputable Person

sameParent :: Comp Boolean
sameParent = do p1 <- inputData Public  :: Comp Person
                p2 <- inputData Private :: Comp Person
                return (eqData (parent p1) (parent p2))

To know more details see documentation and the source code of Inputable.

Compiler Interface with Custom Datatypes

Since now a Keelung program can take a value of custom datatype as inputs, we provide the counterparts of interpreting/proving interface so that instead of giving lists of field elements as public/private inputs, one can provide a value of such type:

• interpret :: (Encode t) => FieldType -> Comp t -> [Integer] -> [Integer] -> IO [Integer]
  ↓
  interpretData :: (Encode t, Inputable a, Inputable b) => FieldType -> Comp t -> a -> b -> IO [Integer]
• interpretEither :: (Encode t) => FieldType -> Comp t -> [Integer] -> [Integer] -> IO (Either Error [Integer])
  ↓
  interpretDataEither :: (Encode t, Inputable a, Inputable b) => FieldType -> Comp t -> a -> b -> IO (Either Error [Integer])
• solveOutput :: (Encode t) => FieldType -> Comp t -> [Integer] -> [Integer] -> IO [Integer]
  ↓
  solveOutputData :: (Encode t, Inputable d, Inputable e) => FieldType -> Comp t -> d -> e -> IO [Integer]
• solveOutputEither :: (Encode t) => FieldType -> Comp t -> [Integer] -> [Integer] -> IO (Either Error [Integer])
  ↓
  solveOutputDataEither :: (Encode t, Inputable d, Inputable e) => FieldType -> Comp t -> d -> e -> IO (Either Error [Integer])
• etc.

See the source code for more such interfaces.

What's Next?

• We are enhancing the witness solver and plan to replace the interpreter's role with this improved witness solver in the future.
• Integration with SnarkJS is also on the way!

v0.24.0

What’s New?

Introducing two new arithmetic operators for UInt division and modulo:

divU :: UInt w -> UInt w -> UInt w
modU :: UInt w -> UInt w -> UInt w

These operators might seem familiar, because we already have performDivMod for computing quotients and remainders:

performDivMod :: UInt w -> UInt w -> Comp (UInt w, UInt w)

You’ll notice the difference in their type signatures.

Monadic v.s. Pure

performDivMod is a monadic function, while divU and modU are pure operators.

Monadic functions can be more cumbersome to use compared to pure operators, especially when you need to use the resulting value in further computations.

For example, if you want to add the remainder of two inputs to a number, pure operators offer a simpler approach:

monadicExample :: UInt 8 -> UInt 8 -> Comp (UInt 8)
monadicExample x y = do 
    (_, remainder) <- performDivMod x y
    return (remainder + 42)

pureExample :: UInt 8 -> UInt 8 -> UInt 8
pureExample x y = (x `modU` y) + 42

Memoization

performDivMod allows us to compute both the quotient and remainder at once, while divU and modU compute them separately. However, as long as the arguments to both divU and modU are the same, there will be no extra overhead because they will share the same set of constraints after compilation.

let quotient  = x `divU` y
let remainder = x `modU` y

We hope these new operators will make working with unsigned integer arithmetic simpler and more enjoyable.

What’s Next?

• We’ve made a lot of progress with user-defined datatypes & structured input/output. Expect a major update on this front in the next release!
• Smarter witness generation on binary fields.
• Protocol for user-programmable hints for witness generation.

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 v

There 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 w

These 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 v

This 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 discarded

What 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?

• slice and join operator
• 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 v

slice 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` v

Compilation 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 Field
• fromBools: [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

This is a patch of v0.19.0 that primarily focuses on bug fixes and dependency updates.

We have upgraded to Stackage LTS 20.26 (GHC 9.2.8) in hopes of addressing issue#35.

Happy coding!

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 fields

And 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.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 quotient

Similar 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 w

Simply 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 .*. 42

What'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!