Booleans

Booleans are a fundamental data type in Keelung that are primarily used to construct logical and conditional expressions, although they are essentially just field elements in disguise.

Unlike numeric values that come with a user-friendly interface, Boolean values and logical operators are constructed using specific constructors and functions listed below.

Construction

Booleans have 2 inhabitants, they are:

true  :: Boolean
false :: Boolean

Conversion

From Haskell Booleans

The following constructor converts Haskell Booleans to Keelung Booleans:

Boolean :: Bool -> Boolean

true and false are made this way under the hood:

true :: Boolean
true = Boolean True 

false :: Boolean
false = Boolean False

From Keelung unsigned integers

The !!! operator allows you to inspect the bit value at a specific position in an unsigned integer.

(!!!) :: UInt w -> Int -> Boolean

To Keelung field elements

BtoF converts to Booleans to field elements:

BtoF :: Boolean -> Field

To Keelung unsigned integers

BtoU converts to Booleans to field elements:

BtoU :: Boolean -> UInt w

Functions

Conditionals

cond :: Boolean -> Field   -> Field   -> Field  
cond :: Boolean -> Boolean -> Boolean -> Boolean
cond :: Boolean -> UInt w  -> UInt w  -> UInt w 

Unlike in most imperative languages, conditionals are expressions rather than just statements. Both branches have to be present and must be of the same type. That means you cannot omit the else ... branch like in C.

Here's a simple calculator has only 2 operations: addition and multiplication. It takes a Boolean operation flag and 2 inputs, and returns the result.

calculator :: Comp Field
calculator = do
  addOrMultiply <- input Public -- Booloean
  x             <- input Public -- Field
  y             <- input Public -- Field
  return $
    cond
      addOrMultiply
      (x + y)
      (x * y)

Conjunction

(.&.) :: Boolean -> Boolean -> Boolean

Example usage: x .&. true

Disjunction

(.|.) :: Boolean -> Boolean -> Boolean

Example usage: false .|. x

Exclusive disjunction

(.^.) :: Boolean -> Boolean -> Boolean

Example usage: false .^. x

Complement

complement :: Boolean -> Boolean

Example usage: complement x

Equality

Returns true when two field elements are the same:

eq :: Boolean -> Boolean -> Boolean

Example usage: false `eq` false or eq false true.

You can also use EqB , which is the underlying implementation of eq on Booleans.

Binary function such as eq can be treated like an infix operator by surrounding it with a pair of backticks `eq`

Inequality

Returns false when two Booleans are the same:

neq :: Boolean -> Boolean -> Boolean

neq is implemented as such under the hood:

neq x y = Not (x `eq` y)