Add P256 Scalarmult with small table

[miriampolzer]

No description provided.

[andres-erbsen]

See https://github.com/miriampolzer/fiat-crypto/compare/p256_scalarmult...andres-erbsen:fiat-crypto:p256_scalarmult?expand=1

[andres-erbsen]

• From Coq Require Import at top is following your pattern of doing Require in dependency order - if we're already being this sytematic :)
• Abbreviation is a very new rename, let's stick with Notation for new
• Eval cbv in instead of hardcoded constants
• Another moderately impactful example of taking input apart once and reframing goals in terms of putting it back together: https://github.com/miriampolzer/fiat-crypto/compare/p256_scalarmult...andres-erbsen:fiat-crypto:p256_scalarmult?expand=1#diff-f97e4488a80ab830507ff3ed487430ba1570c3305cfdbc2acdb89db017bf7e44R399
• Not sure whether I like rewrite as a lia hook (maybe it's expensive?) but here https://github.com/miriampolzer/fiat-crypto/compare/p256_scalarmult...andres-erbsen:fiat-crypto:p256_scalarmult?expand=1#diff-f97e4488a80ab830507ff3ed487430ba1570c3305cfdbc2acdb89db017bf7e44R75-R77
• I didn't really get to the last proof, and it's late

👍 overall

[andres-erbsen]

I didn't really get to the last proof, and it's late

https://github.com/miriampolzer/fiat-crypto/compare/p256_scalarmult...andres-erbsen:fiat-crypto:p256_scalarmult?expand=1#diff-f97e4488a80ab830507ff3ed487430ba1570c3305cfdbc2acdb89db017bf7e44R397 ought not to be there

[miriampolzer]

Amazing thank you for reviewing! I have updated the proofs with your refactorings (with some small adaptions here and there - but it's mostly what you did). Let's see if the CI passes.

Regarding the lia hook, it didn't seem to add much in terms of timing, so I've even expanded it.

What I learned:

• Override Zify.zify_pre_hook to modify lia. That's pretty cool, but probably to be used very locally and carefully. https://rocq-prover.org/doc/v9.0/refman/addendum/micromega.html#zify-pre-processing-of-arithmetic-goals explicilty calls out how to use the post hook for div and mod equations.
• You can use pattern matching in change. I don't know how I missed this before: change (fold_right _ _ (map _ ?l)) with (positional_signed_bytes (2^w) l).