Andres Erbsen

refactoring: https://github.com/mit-plv/bedrock2/blob/semantics-refactor/src/ExprImp.v

I think I am converging to something. Here is what it looks like right now: https://github.com/mit-plv/bedrock2/blob/io-lts/bedrock2/src/ImpWithIO.v

I am guessing we are failing to perform step 12 of https://blog.cr.yp.to/20140323-ecdsa.html: Reduce modulo p "by adding or subtracting a few copies" of p. We should do this by treating...

Complication: the final carry may have multiple bits and may be positive or negative (or zero), so we probably can't do it using unsigned integers only. I still don't know...

> since the first subgoal appears as a dependency in the second subgoal, the first subgoal is shelved, and typeclass search works on the second subgoal This is the part...

Clarification from meeting: the validity conditions are about PHOAS->bedrock2 translator input, not output. Currently the translator proof passes because the validity precondition is too strict.

https://sourceforge.net/p/ed448goldilocks/code/ci/master/tree/src/p448/arch_32/f_impl.c might be good reference code

Yes, this is the intended use case. It looks like H10 has more bignums than the goal, though, so I would expect this goal is not provable. Perhaps you forgot...

We used to have C tests before the new pipeline. Perhaps we can just resurrect them?

I am not happy with the boilerplate either. But what else would we do? Using the module system would have less boilerplate but the boilerplate would be more arcane; using...