From Data Types to Programs

Building Data Types

Delving Into Simplicity

Building Data Types

Boolean Logic
Bit Adders
Vectors
Option Types
Variable Length Buffers
Conclusion

In the previous chapters, we showed how Simplicity's core set of combinators are enough to implement any finite pure computation. This chapter shows how to build practical data structures and computations from these primitives — the same way computers are built from logic gates.

Boolean Logic

The Boolean type, denoted 𝟚, equals 𝟙 + 𝟙 and has two values: σᴸ⟨⟩ (false) and σᴿ⟨⟩ (true). Using the core combinators, Boolean logic operators can be constructed.

And Operation

The logical and : 𝟚 × 𝟚 ⊢ 𝟚 operation takes two bits and returns one bit. The implementation branches on the first bit: if false, return false; otherwise, return the second bit.

and ≔ case (injl unit) (drop iden) : 𝟚 × 𝟚 ⊢ 𝟚

Testing with ⟨false, false⟩:

⟦and⟧⟨false, false⟩
 = {expand the notation for false}
⟦and⟧⟨σᴸ⟨⟩, σᴸ⟨⟩⟩
 = {expand the definition of and}
⟦case (injl unit) (drop iden)⟧⟨σᴸ⟨⟩, σᴸ⟨⟩⟩
 = {evaluate case for σᴸ}
⟦injl unit⟧⟨⟨⟩, σᴸ⟨⟩⟩
 = {evaluate injl}
σᴸ(⟦unit⟧⟨⟨⟩, σᴸ⟨⟩⟩)
 = {evaluate unit}
σᴸ⟨⟩
 = {by the notation for false}
false

Testing with ⟨true, true⟩:

⟦and⟧⟨true, true⟩
 = {expand the notation for true and the definition of and}
⟦case (injl unit) (drop iden)⟧⟨σᴿ⟨⟩, σᴿ⟨⟩⟩
 = {evaluate case for σᴿ}
⟦drop iden⟧⟨⟨⟩, σᴿ⟨⟩⟩
 = {evaluate drop}
⟦iden⟧(σᴿ⟨⟩)
 = {evaluate iden}
σᴿ⟨⟩
 = {by the notation for true}
true

Other Logic Operations

The not operation requires a helper combinator:

                   f : A ⊢ C    g : B ⊢ C
--------------------------------------------------------------
copair f g ≔ iden ▵ unit ⨾ case (take f) (take g) : A + B ⊢ C

The initial iden ▵ unit : A ⊢ A × 𝟙 adds an empty "environment" to the input, enabling the case combinator to apply. The use of take in the two branches drops this empty environment to execute f or g.

Other Boolean logical operations:

or ≔ case (drop iden) (injr unit) : 𝟚 × 𝟚 ⊢ 𝟚
not ≔ copair (injr unit) (injl unit) : 𝟚 ⊢ 𝟚
xor ≔ case (drop iden) (drop not) : 𝟚 × 𝟚 ⊢ 𝟚

Bit Adders

A "half-adder" takes two bits and adds them, producing a two-bit output: a carry bit and sum bit.

half-adder ≔ and ▵ xor : 𝟚 × 𝟚 ⊢ 𝟚 × 𝟚

A "full-adder" adds three bits, producing two-bit output. The input uses nested tuple (𝟚 × 𝟚) × 𝟚.

For nested tuples, compact notation is used:

O f denotes take f
I f denotes drop f
H denotes iden

For example, I O H means drop (take iden) : A × (B × C) ⊢ B, extracting the middle value. The notation evokes binary digits: when thinking of nested tuples as binary trees, the notation represents reversed binary digits of tree positions. These expressions form De Bruijn indices for Simplicity.

Note: The I, O, and H notation only applies to subexpressions consisting solely of take, drop, and iden.

The full-adder composes two half-adders, taking logical or of the carry bits:

full-adder ≔ take half-adder ▵ I H
           ⨾ O O H ▵ (O I H ▵ I H ⨾ half-adder)
           ⨾ (O H ▵ I O H ⨾ or) ▵ I I H
           : (𝟚 × 𝟚) × 𝟚 ⊢ 𝟚 × 𝟚

In the first line, take half-adder ▵ I H : (𝟚 × 𝟚) × 𝟚 ⊢ (𝟚 × 𝟚) × 𝟚 runs the half-adder on the first two bits, saving the last bit.

In the second line, O O H ▵ (O I H ▵ I H ⨾ half-adder) : (𝟚 × 𝟚) × 𝟚 ⊢ 𝟚 × (𝟚 × 𝟚) saves the first bit (the carry-out of the first half-adder) and runs the half-adder on the last two bits.

In the last line, (O H ▵ I O H ⨾ or) ▵ I I H: 𝟚 × (𝟚 × 𝟚) ⊢ 𝟚 × 𝟚 takes the logical OR of the first two bits (carry-outs of both half-adders) and returns the sum-out bit of the second half-adder.

This demonstrates Simplicity programming: using I, O, and H notation to reference data bits, forming suitable "environments" for calling other functions via sequential composition.

Users don't define low-level operations directly. Later this series discusses standard library jets implementing common functions. End users aren't expected to program directly in Simplicity, similar to Bitcoin Script. Instead, higher-level languages like SimplicityHL generate Simplicity code, managing subexpression "environments" and translating named variables into appropriate take and drop sequences.

Vectors

Fixed-length vectors are defined by forming iterated products of type A:

A² ≔ A × A
A⁴ ≔ A² × A²
A⁸ ≔ A⁴ × A⁴
…

These may be written as A^2, A^4, A^8, etc.

Vectors are defined only for lengths that are powers of two. Other powers require choosing bracketing conventions.

Given expression f : A ⊢ B, repeated pairing "maps" it over fixed-length vectors:

f² ≔ f ▵ f : A² ⊢ B²
f⁴ ≔ f² ▵ f² : A⁴ ⊢ B⁴
f⁸ ≔ f⁴ ▵ f⁴ : A⁸ ⊢ B⁸

Given function f : A × B ⊢ B, iteration or "folding" over fixed-length vectors:

fold-right-2 f ≔ O O H ▵ (O I H ▵ I H ⨾ f) ⨾ f : A² × B ⊢ B
fold-right-4 f ≔ fold-right-2 (fold-right-2 f) : A⁴ × B ⊢ B
fold-right-8 f ≔ fold-right-2 (fold-right-4 f) : A⁸ × B ⊢ B

Many variations exist. Given f : A × B ⊢ C, "zip" over paired vectors with zip-n f : (Aⁿ × Bⁿ) ⊢ Cⁿ. Given f : (A × B) × C ⊢ C, fold over paired vectors with bifold-right-n f : (Aⁿ × Bⁿ) ⊢ C. Combining map and fold-right creates accumulating combinators: f : A × C ⊢ C × B yields map-accum-right-n f : Aⁿ × C ⊢ C × Bⁿ. Many more variants are possible.

Multi-bit Words

A bit vector yields multi-bit integers. For example, 𝟚³² is a 32-bit word type. 𝟚²⁵⁶ is a 256-bit word type, suitable for hashes and cryptographic operations.

Using the full-adder, a variant of vector operations defines a "ripple carry adder" over multi-bit words:

full-adder-n ≔ zip-accum-right-n full-adder : (𝟚ⁿ × 𝟚ⁿ) × 𝟚 ⊢ 𝟚 × 𝟚ⁿ

full-adder-n takes two n-bit binary numbers and a one-bit carry-input, returning a one-bit carry-out flag and an n-bit sum.

SHA-256

By recursively defining arithmetic operations on multi-bit words — subtraction, multiplication, division — and bit-wise logical operations such as logical AND, OR, XOR, and repeatedly combining these, even SHA-256's block compression function can be built:

sha256-hash-block ≔ … : 𝟚²⁵⁶ × 𝟚⁵¹² ⊢ 𝟚²⁵⁶

The SHA-256 compression is formally defined using Simplicity within the Rocq proof assistant (formerly Coq), with a formal proof that the sha256-hash-block implementation is correct.

The compression runs too slowly as raw Simplicity. Jets execute common functions like SHA-256 compression natively. Pure Simplicity implementations serve as formal specifications for jets.

Option Types

Option types result from taking a sum with the unit type:

Option A ≔ 𝟙 + A

The type Option A may be written as A? or 𝕊 A (where 𝕊 means "successor"). Functions map over option types:

                 f : A ⊢ B
------------------------------------------
f? ≔ copair (injl unit) (injr f) : A? ⊢ B?

Monadic combinators such as bind can be defined:

              f : A ⊢ B?
---------------------------------------
bind f ≔ copair (injl unit) f : A? ⊢ B?

Variable Length Buffers

"Buffers" are types for partially filled vectors:

Aᑉ² ≔ A?
Aᑉ⁴ ≔ A²? × Aᑉ²
Aᑉ⁸ ≔ A⁴? × Aᑉ⁴
…

The type Xᑉ⁸ expands to (1 + X⁴) × ((1 + X²) × (1 + X)). Treating this as a polynomial and expanding yields 1 + X + X² + X³ + X⁴ + X⁵ + X⁶ + X⁷. Interpreting as a type, it represents the sum of all possible tuples of X up to 7, including the empty tuple. This is exactly the type of lists with length strictly less than 8.

Like vectors, mapping and folding operations can be defined over buffers. Stack operations include push-<n : Aᑉⁿ × A ⊢ Aⁿ + Aᑉⁿ and pop-<n : Aᑉⁿ ⊢ (Aᑉⁿ × A)?. push-<n appends an item to the buffer, returning a full vector if overflow occurs. pop-<n removes an item, returning the smaller buffer and removed item, optionally returning nothing if the original buffer was empty.

The push-<n definition, recursively:

push-<2 ≔ case (drop (injr (injr iden))) (injl iden)

push-<4 ≔ ((O I H ▵ IH) ⨾ push-<2) ▵ O O H
        ⨾ case (I H ▵ O H ⨾ case (injr (injr (I H) ▵ injl unit)) (injl iden))
               (injr (I H ▵ O H))

push-<8 ≔ ((O I H ▵ IH) ⨾ push-<4) ▵ O O H
        ⨾ case (I H ▵ O H ⨾ case (injr (injr (I H) ▵ (injl unit ▵ injl unit))) (injl iden))
               (injr (I H ▵ O H))

…

Raw Simplicity becomes difficult to follow beyond certain complexity levels. End users utilize higher-level languages like SimplicityHL generating these idiomatic expressions.

Conclusion

This chapter showed how to build logical operations from bits. From these, bit-level arithmetic emerged, enabling reasoning about execution. Vector types were developed, demonstrating iteration over multi-bit words for arithmetic definition. Continuing, cryptographic operations like SHA-256 and Schnorr signature validation can be defined using Simplicity combinators alone — all actually defined using Simplicity.

This chapter isn't a comprehensive guide to all possible data types and operations buildable in Simplicity, but illustrates achieving practical functionality within Simplicity's constraints. Despite finitely bounded types, useful vectors, buffer types, and operations iterating over these structures can be defined.

Actual standard library operation specifications differ slightly from definitions here. For instance, the full-adder uses a 3-way XOR and "majority" logic function rather than two half-adders.

In practice, Simplicity programs use jets for arithmetic and cryptographic operations. However, jets only replace expressions. Combinators iterating over buffers and vectors cannot be replaced by jets, appearing in actual Simplicity programs. Though rather than directly using these, end users employ higher-level languages like SimplicityHL generating such expressions.

Recursively defined combinators appear to grow exponentially in expression size. This isn't problematic. During serialization, expressions are encoded as DAGs (directed acyclic graphs) rather than trees. Actual representation grows only linearly.

So far, only pure computations were considered. Interaction with transaction data for tasks like signing transactions requires some way for programs to fail if signatures are invalid. The next chapter discusses side-effects in Simplicity.

Quiz

scr4033.1

1/5

What is SimplicityHL and why is it needed?