search

GaloisInc / ckzg-eip-4844-verification

BSD 3-Clause "New" or "Revised" License
2 stars 1 forks source link

Replace `modular_inverse` with built-in `recip` #26

Open b13decker opened 1 month ago

b13decker commented 1 month ago

Note, we will need to add the constraint prime n to div_mod if we do this.

suggestion: If you're not trying to match a spec, you can also call the built-in recip function here.

_Originally posted by @marsella in https://github.com/GaloisInc/ckzg-eip-4844-verification/pull/23#discussion_r1781416388_

b13decker commented 1 month ago

I'm going to hold off on this one until the rest of the Cryptol work is done, since this is just a nice to have.