roconnor-blockstream

> I meant how would the user know by looking their string needed corrections in the first place. But now, I realize if the checksum worksheet is performed as part...

Rebased.

Fixed.

The way I expected this to work (but isn't implemented yet) is that a Simplicity compiler / optimizer would recognize fragments of Simplicity expressions that match existing jets and substitute...

Unless I am mistaken, there is no correctness proof for the translation from whatever Fiat Crypto's algorithm representation format is into C code, so mucking about with that translation layer...

It was my intention on proving the field, then group operations correct after finishing (one of) the modular inverse implementation. I think performance should probably be the primary concern. However...

Sure thing. I was really hoping we'd land at a place where we could do both. https://github.com/mit-plv/fiat-crypto/issues/1560#issuecomment-1652241177 mentions some bedrock2 thing which sounds like we might eventually get there, but...

Here are my notes on the topic of caveats of formal proofs: ## Regarding using VST * The C-lightgen program to convert C to Coq is proprietary and requires a...

Ooph! Sounds like hypothetical bedrock2 generated C would end up containing a lot of `uintptr_t` to pointer casts. I wonder how libsecp256k1 maintainers would feel about that? Sure technically it...

I've finished the correctness proofs in VST of `secp256k1_fe_mul_inner` and `secp256k1_fe_sqr_inner`. You can find the rendered proof at . The proof itself is probably not all that interesting beyond the...