Picus icon indicating copy to clipboard operation
Picus copied to clipboard
verified publisher icon chyanju

Format of Preconditions

Open Koukyosyumei opened this issue 1 year ago • 0 comments

Hi! Thanks for this amazing project!

The original paper mentions using BabyAdd as a precondition to improve verification scalability. How can I specify this in the implementation? I also want to do the something for IsZero and Num2Bits.

Koukyosyumei avatar Mar 22 '25 12:03 Koukyosyumei