Prove associative law of addition by Rust type system

Hi there,
I've been learning Rust for a period. Yesterday someone asked me to try to do formal verification with the Rust type system. So I decided to write one to prove the associative law of addition. One is to exercise my programming skills, the other is for fun :D.

The source code is here.

Target

To prove a + (b + c) = (a + b) + c, for any natural number a, b and c.

Steps

Addition

We need to define what "natural number" exactly are, which are Zero and its successors.

struct Succ<N>(N);
struct Zero;

And then, we define a trait indicates if a type is a natural number.

trait Nature {
    type Add<T: Nature>: Nature;
}

Implement it for Zero to say 0 + n = n.

impl Nature for Zero {
    type Add<T: Nature> = T;
}

For Succ<T> to nest successors.

impl<T> Nature for Succ<T>
where
    T: Nature,
{
    type Add<U: Nature> = Succ<T::Add<U>>;
}

Now we can add two numbers.

type One = Succ<Zero>;
type Two = Succ<Succ<Zero>>;
type Three = Succ<Succ<Succ<Zero>>>;
type Four = Succ<Succ<Succ<Succ<Zero>>>>;

// 2 + 1 + 1 = 4
fn add_test(x: <<Two as Nature>::Add<One> as Nature>::Add<One>) -> Four {
    x
}

Associative Law

It's hard to let Rust understand that two types are equal. Using functions is unintuitive and sounds like cheating because not only uses type system. So I can only put this law into trait bounds. But because of the generic types (B and C), so I cannot put this into Nature trait.

Firstly we define two types, (a + b) + c and a + (b + c), for any natural number a, b, c.

// (a + b) + c
type APlusBPlusC1<A, B, C> = <<A as Nature>::Add<B> as Nature>::Add<C>;

// a + (b + c)
type APlusBPlusC2<A, B, C> = <A as Nature>::Add<<B as Nature>::Add<C>>;

Now our target is to implements Assoc trait for Zero and any of its successors.

trait Assoc<B, C>
where
    Self: Nature,
    B: Nature,
    C: Nature,

    // this is the key trait bound, 
    // satisfying this equivalent to satisfying associative law for
    // specified natural numbers `Self`, `B` and `C`
    <Self as Nature>::Add<B>: Nature<Add<C> = APlusBPlusC2<Self, B, C>>,
{
    fn assoc(x: APlusBPlusC1<Self, B, C>) -> APlusBPlusC2<Self, B, C> {
        x
    }
}

It's more than easy to implement it for Zero.

impl<B, C> Assoc<B, C> for Zero
where
    B: Nature,
    C: Nature,
{
}

But if we want to implement it for Succ<T>, T is required to implement both Nature and Assoc<B, C>.

impl<T, B, C> Assoc<B, C> for Succ<T>
where
    T: Nature,
    B: Nature,
    C: Nature,

    // so we need this
    <T as Nature>::Add<B>: Nature<Add<C> = APlusBPlusC2<T, B, C>>,
    T: Assoc<B, C>,
{
}

So we are done.
Let's take a test.

fn main() {
    let _ = <Two as Assoc<One, Three>>::assoc;
}

This function compiles, indicates Two, One and Three satisfy associative law of addition.

Conclusion

This proof is just a attempt, there is still room for improvement:

  • How to require Nature implements Assoc<B, C> for generic type B, C? Associate functions are not allowed.
  • Is there any other way to prove?

Thanks for reading.
(Double thanks if you have any suggestions for me. :stuck_out_tongue:)

2 Likes

Hi @Fancyflame,

I understand your point... I can't comment on the implementation, my generic with Rust is still not sharp enough to understand others codes quite quickly yet...

I clicked on the Playground link that you provided, unfortunately, it reports the following complaints:

Errors

Exited with status 101

Standard Error

   Compiling playground v0.0.1 (/playground)
error[E0412]: cannot find type `NaN` in this scope
  --> src/main.rs:63:27
   |
63 |     let _ = <Two as Assoc<NaN, Three>>::assoc;
   |                           ^^^ not found in this scope

For more information about this error, try `rustc --explain E0412`.
error: could not compile `playground` (bin "playground") due to previous error

Standard Output

Best regards,

...behai.

Ah, I forgot to modify this :sweat_smile:
I tested NaN seeing whether associative law works on it (yes it does), and forgot to change back. Thanks.