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.

This topic was automatically closed 90 days after the last reply. We invite you to open a new topic if you have further questions or comments.