CSA proof

[osmanyasar05]

Implementation and verification of Carry Save Adder (CSA) circuit in Lean. The PR includes both a manual proof and automated one using bv_automata.

[luisacicolini]

Left a few comments!

[cowardsa]

Overall an impressive amount of work - I wonder if extending t to w+1 is painful?

Secondly, your main lemma performs a conversion toNat - and I wonder if this is causing a major pain? In particular you could still do bitvector addition right, you'll just need to extend a,b and c to keep any carry-outs.

I would actually advocate that any zeroExtension should be done to inputs to a CSA that way there is space for keeping the carry-out within the bitvector itself - that way you can just do bitvec add of all three inputs

[osmanyasar05]

@cowardsa Thanks for the feedback! Yes, the two questions are related I think. It's a big part/problem of the proof. The reason I use toNat's is to make the addition of s (width w) and t (width w+1) possible. I'll look into how zeroExtension could obviate this.

[osmanyasar05]

@luisacicolini thanks a lot for the review! I addressed the comments.

[cowardsa]

@cowardsa Thanks for the feedback! Yes, the two questions are related I think. It's a big part/problem of the proof. The reason I use toNat's is to make the addition of s (width w) and t (width w+1) possible. I'll look into how zeroExtension could obviate this.

Can't we just keep s and t to be the same width (w) - then you'll need to extend them before performing t<<1 + s?

[osmanyasar05]

@cowardsa Thanks for the feedback! Yes, the two questions are related I think. It's a big part/problem of the proof. The reason I use toNat's is to make the addition of s (width w) and t (width w+1) possible. I'll look into how zeroExtension could obviate this.

Can't we just keep s and t to be the same width (w) - then you'll need to extend them before performing t<<1 + s?

Yes, this approach makes sense! I have just pushed a commit where I modified t to have width w, and changed the proofs accordingly. I will work on overhauling the rest of the proof and see how I can minimize toNat conversions.