Skip to content

Collatz in Practice

A key example of flushing

On this page we demonstrate column "flushing", a type of constraint, by implementing a prover for Collatz orbits. Collatz orbits were also used for illustrating flushing in M3-base arithmetization in Proving Collatz Orbits. We take that theoretical perspective and build a practical Collatz proof system here, involving not just a constraint system but a prover and verifier. This our first of two end-to-end proof system examples, for the second see Making Lookups.

Some of the gadgets we'll need on this page are not constructed on this page but are used in a blackbox fashion. All gadgets necessary can be found in the full example.

After briefly re-summarizing the Collatz conjecture and reviewing how a channel can serve for proving the Collatz orbit of some integer, we discuss and create the two gadgets even and odd at the center of our constraint system. In order to properly separate the prover and verifier, we define and implement methods for a Collatz type. Lastly we construct prover and verifier functions for a complete working system.

Collatz Using a Channel

The Collatz conjecture states that applying a certain sequence of transitions to every positive integer, the integer travels an "orbit" that always ends at 1. The transitions are as follows:

  • If the integer is even, get the next integer in the orbit by dividing it by 2.
  • If the integer is odd, get the next integer in the orbit by multiplying it by three then adding one.

Suppose the verifier holds an integer x0 that is to be the first integer in a Collatz orbit. The prover must prove that the orbit of x0 indeed ends at 1. Our proof technique will utilize a "channel" (see channels for context). For any integer put into the channel, the prover must prove that the Collatz orbit of that integer ends at 1. To begin, the verifier puts x0 into the channel. The rules of the game allow the prover to remove an integer x from the channel if and only if the correctly calculated integer following x in orbit is put into the channel in exchange. Our rules are thus

  • If x is even, then you may pull x out of the channel if you push x/2 into the channel.
  • If x is odd, then you may pull x out of the channel if you push 3x+1 into the channel.

If the prover correctly follows the orbit of x0 and plays by the rules pulling each integer out of the channel in exchange for pushing the next integer in the orbit into the channel, then ultimately (provided the Collatz conjecture is true), only the number 1 should remain in the channel. The verifier pulls this number 1 out of the channel. By pushing only x0 into the channel, and pulling only 1 out of the channel, the verifier can be sure the Collatz orbit of x0 ends in 1.

Basic Needs

Before we discuss how to build the constraint system and witness, let's mention a few basic things we'll need.

Of course we'll need the channel, and to create it we write

let channel = builder.add_channel();

The prover will need to calculate the orbit of x0. For this we write the function

fn collatz_orbit(x0: u32) -> Vec<u32> {
	let mut res = vec![x0];
	let mut x = x0;
	while x != 1 {
		if x % 2 == 0 {
			x /= 2;
		} else {
			x = 3 * x + 1;
		}
		res.push(x);
	}
	// We ignore the final 1
	res.pop();
	res
}

We will be handling the even values differently from the odd values, so we have the prover compute and partition the orbit as

let (evens, odds) = collatz_orbit(x0).into_iter().partition(|x| x % 2 == 0);

Now we can begin thinking about the constraints.

Even and Odd Gadgets

Suppose the prover counts the number of integers in the orbit and provides that count variable as non-deterministic advice to the verifier. In fact, the prover will provide the counts for both the number of even integers and odd integers. Let us construct two gadgets, one called even and one called odd. These gadgets will not have input or output oracles. Here's what we'll do in the even gadget, and do similarly in the odd gadget.

Inside the even gadget we'll create a committed column holding the 32-bit decomposed values of all even integers. As all columns must be of length a power of 2, if the number of even integers is not a power of 2 we will round up with extra padding zeros. We wish to do three things with this columns of integers.

  • Check all integers are even.
  • Pull all integers out of the channel.
  • Push all integers divided by 2 into the channel.

While the committed column is bit-decomposed, and that will help us check the integers to be even, we don't want to push and pull individual bits into the channel, but rather full integers. To help us we'll assume the existence of two auxiliary gadgets:

  • Suppose there exists a gadget called "half" that takes a column of 32-bit decomposed integers, checks that all integers are even, and returns the column containing the 32-bit decomposed output integers had by dividing each input integer by 2.
  • Suppose there exists a gadget called "packed" that takes a column of 32-bit decomposed integers and returns the column of BinaryField32b elements representing the packed bit decompositions.

Before writing the even gadget, we must discuss one more point. If the prover is the one calling the gadget, how is the prover to compute the values to fill the committed column? We'll assume the prover already computed the even and odd elements of the orbit. Suppose they are saved in a struct

struct Collatz {
	x0: u32,
	evens: Vec<u32>,
	odds: Vec<u32>,
}

Then if we make even a method of this type, we can get access to the even elements of the orbit via self. With the function receiving not only self and the builder as arguments, but also the channel id and the number of even integers, we write even as follows.

fn even<U, F>(
    &self,
    builder: &mut ConstraintSystemBuilder<U, F>,
    channel: ChannelId,
    count: usize,
) -> Result<(), anyhow::Error>
where
    U: PackScalar<F> + PackScalar<BinaryField1b> + PackScalar<BinaryField32b> + Pod,
    F: TowerField + ExtensionField<BinaryField32b>,
{
    let log_1b_rows = 5 + binius_utils::checked_arithmetics::log2_ceil_usize(count);
    let even = builder.add_committed("even", log_1b_rows, BinaryField1b::TOWER_LEVEL);
    if let Some(witness) = builder.witness() {
        debug_assert_eq!(count, self.evens.len());
        witness
            .new_column::<BinaryField1b>(even)
            .as_mut_slice::<u32>()[..count]
            .copy_from_slice(&self.evens);
    }
 
    // Passing Checked flag here makes sure the number is actually even
    let half = arithmetic::u32::half(builder, "half", even, arithmetic::Flags::Checked)?;
 
    let even_packed = arithmetic::u32::packed(builder, "even_packed", even)?;
    builder.flush(FlushDirection::Pull, channel, count, [even_packed]);
 
    let half_packed = arithmetic::u32::packed(builder, "half_packed", half)?;
    builder.flush(FlushDirection::Push, channel, count, [half_packed]);
 
    Ok(())
}

When we call flush on the builder, we are requesting that all values in the even_packed oracle are pulled out of the channel, and all the values in the half_packed oracle are pushed into the channel.

Now we construct the analogous function for the odd elements. To do so we assume three additional auxiliary gadgets:

  • ensure_odd takes an oracle of 32-bit decomposed integers and ensures they are all odd.
  • constant creates an oracle with all values a given constant.
  • mul_const take an oracle of 32-bit decomposed integers and returns the oracle of 32-bit decomposed integers had by multiplying each input by a given constant.
  • add accepts two 32-bit decomposed integer oracles and returns the oracle holding the 32-bit decomposed sums.

Using these gadget helpers we write gadget odd to similarly create a committed column of 32-bit decomposed integers. We'll ensure each of those integers is odd, and we'll pull these out of the channel. We'll also multiply these input integers by 3 and add 1, then push the results into the channel. Again, we don't actually push and pull the bit decomposed integers but rather their packed versions.

fn odd<U, F>(
    &self,
    builder: &mut ConstraintSystemBuilder<U, F>,
    channel: ChannelId,
    count: usize,
) -> Result<(), anyhow::Error>
where
    U: PackScalar<F> + PackScalar<BinaryField1b> + PackScalar<BinaryField32b> + Pod,
    F: TowerField + ExtensionField<BinaryField32b>,
{
    let log_32b_rows = binius_utils::checked_arithmetics::log2_ceil_usize(count);
    let log_1b_rows = 5 + log_32b_rows;
 
    let odd = builder.add_committed("odd", log_1b_rows, BinaryField1b::TOWER_LEVEL);
    if let Some(witness) = builder.witness() {
        debug_assert_eq!(count, self.odds.len());
        witness
            .new_column::<BinaryField1b>(odd)
            .as_mut_slice::<u32>()[..count]
            .copy_from_slice(&self.odds);
    }
 
    // Ensure the number is odd
    ensure_odd(builder, odd, count)?;
 
    let one = arithmetic::u32::constant(builder, "one", log_32b_rows, 1)?;
    let triple =
        arithmetic::u32::mul_const(builder, "triple", odd, 3, arithmetic::Flags::Checked)?;
    let triple_plus_one = arithmetic::u32::add(
        builder,
        "triple_plus_one",
        triple,
        one,
        arithmetic::Flags::Checked,
    )?;
 
    let odd_packed = arithmetic::u32::packed(builder, "odd_packed", odd)?;
    builder.flush(FlushDirection::Pull, channel, count, [odd_packed]);
 
    let triple_plus_one_packed =
        arithmetic::u32::packed(builder, "triple_plus_one_packed", triple_plus_one)?;
    builder.flush(FlushDirection::Push, channel, count, [triple_plus_one_packed]);
 
    Ok(())
}

Now that we have even and odd gadgets, we need to put thing into place to use them.

Implementing Collatz

We'll implement our Collatz struct with several methods besides even and odd. First we'll make a factory method that both the prover and verifier will call

pub fn new(x0: u32) -> Self {
    Self {
        x0,
        evens: vec![],
        odds: vec![],
    }
}

Next we'll make a method that only the prover will call, in order to compute the orbit of x0 and properly fill the struct evens and odds fields.

pub fn init_prover(&mut self) -> Advice {
    let (evens, odds) = collatz_orbit(self.x0).into_iter().partition(|x| x % 2 == 0);
    self.evens = evens;
    self.odds = odds;
 
    (self.evens.len(), self.odds.len())
}

Notice this method returns a tuple of two lengths we call Advice. Within our even and odd gadgets we need to know these lengths to create the committed oracles. The prover computes and returns these lengths such that we may later provide them to the verifier as non-deterministic advice to pass into the even and odd gadgets.

Another method we'll need is responsible for constructing the boundary values that the verifier will pull from and push into the channel. Recall the verifier will push x0 into the channel and pull 1 out of the channel.

fn get_boundaries<F>(&self, channel_id: usize) -> Vec<Boundary<F>>
where
    F: TowerField + From<BinaryField32b>,
{
    vec![
        Boundary {
            channel_id,
            direction: FlushDirection::Push,
            values: vec![BinaryField32b::new(self.x0).into()],
            multiplicity: 1,
        },
        Boundary {
            channel_id,
            direction: FlushDirection::Pull,
            values: vec![BinaryField32b::new(1).into()],
            multiplicity: 1,
        },
    ]
}

The multiplicity field may be nonzero in special cases we won't discuss. Notice that while new and init_prover are public methods, get_boundaries is private. The reason is, we will call it locally from another function build. The build function will be public and called by both the prover and verifier. It is the entry point to creating the constraint system.

Within build we'll create the channel, invoke the even and odds gadgets, then get and return the boundaries with get_boundaries. In addition to the builder, our build function will accept Advice that we may pass to even and odd.

pub fn build<U, F>(
    self,
    builder: &mut ConstraintSystemBuilder<U, F>,
    advice: Advice,
) -> Result<Vec<Boundary<F>>, anyhow::Error>
where
    U: PackScalar<F> + PackScalar<BinaryField1b> + PackScalar<BinaryField32b> + Pod,
    F: TowerField + ExtensionField<BinaryField32b>,
{
    let (evens_count, odds_count) = advice;
 
    let channel = builder.add_channel();
 
    self.even(builder, channel, evens_count)?;
    self.odd(builder, channel, odds_count)?;
 
    let boundaries = self.get_boundaries(channel);
 
    Ok(boundaries)
}

Putting Things Together

Finally let us put together all our functions and see how they interact. We will construct prove and verify functions. We'll call these functions in sequence from a main function.

fn main() -> Result<()> {
	let args = Args::parse();
 
	let x0 = args.starting_value;
	println!("Verifying collatz orbit over u32 with starting value {}", x0);
 
	let log_inv_rate = args.log_inv_rate as usize;
 
	let (advice, proof) = prove(x0, log_inv_rate)?;
 
	verify(x0, advice, proof, log_inv_rate)?;
 
	Ok(())
}

Notice the prove function is responsible for turning advice and the proof, while the verify function consumes the advice and the proof.

Constructing the prover

The prove function receives the starting integer x0 as input and returns both advice and a Binius proof. Note the steps involved: We instantiate a Collatz instance with x0, call init_prover and receive the advice, create the builder, call build with the builder and the advice to receive the boundaries, and finally extract the witness and the constraint system from the builder. At that point we can validate that the witness is valid with respect to the constraint system and the boundaries, then lastly we can generate the Binius proof.

fn prove(x0: u32, log_inv_rate: usize) -> Result<(Advice, Proof), anyhow::Error> {
	let mut collatz = Collatz::new(x0);
	let advice = collatz.init_prover();
 
	let allocator = bumpalo::Bump::new();
	let mut builder = ConstraintSystemBuilder::<U, F>::new_with_witness(&allocator);
 
	let boundaries = collatz.build(&mut builder, advice)?;
 
	let witness = builder
		.take_witness()
		.expect("builder created with witness");
	let constraint_system = builder.build()?;
 
	constraint_system::validate::validate_witness(&constraint_system, &boundaries, &witness)?;
 
	let domain_factory = DefaultEvaluationDomainFactory::default();
	let proof = constraint_system::prove::<
		U,
		CanonicalTowerFamily,
		BinaryField32b,
		_,
		_,
		GroestlHasher<_>,
		GroestlDigestCompression<_>,
		HasherChallenger<Groestl256>,
		_,
	>(
		&constraint_system,
		log_inv_rate,
		SECURITY_BITS,
		witness,
		&domain_factory,
		&make_portable_backend(),
	)?;
 
	Ok((advice, proof))
}

Constructing the verifier

To construct the verifier, we also instantiate a new Collatz instance, but we don't call init_prover on it but instead are already given advice as an argument. We instantiate the builder, and call build as we did for the prover. Lastly we build extract the constraint system from the builder, and then verify the constraint system with respect to the boundaries and the Binius proof.

fn verify(x0: u32, advice: Advice, proof: Proof, log_inv_rate: usize) -> Result<(), anyhow::Error> {
	let collatz = Collatz::new(x0);
 
	let mut builder = ConstraintSystemBuilder::<U, F>::new();
 
	let boundaries = collatz.build(&mut builder, advice)?;
 
	let constraint_system = builder.build()?;
 
	constraint_system::verify::<
		U,
		CanonicalTowerFamily,
		_,
		GroestlHasher<_>,
		GroestlDigestCompression<_>,
		HasherChallenger<Groestl256>,
	>(&constraint_system, log_inv_rate, SECURITY_BITS, boundaries, proof)?;
 
	Ok(())
}

The Full Example

To see the example in full, visit circuits/collatz for the implementation of Collatz, and visited examples/collatz for the prove and verify functions.