roconnor-blockstream

Okay. I will build and alternative PR that uses `_mod`.

I wrote up a version that uses `_mod` and the testsuite (correctly) fails. There is actually a problem with that proposal. https://github.com/BlockstreamResearch/secp256k1-zkp/blob/03aecafe4c45f51736ce05b339d2e8bcc2e5da55/src/modules/generator/main_impl.h#L200 `shallue_van_de_woestijne` calls `secp256k1_fe_is_odd(t)` which means that `shallue_van_de_woestijne` has...

Prune first and share later is correct. Sharing should simply be considered part of the serialization format, and thus must occur last/in tandem with serialization.

@andres-erbsen I can start. I've done verification of the int128_struct module using [VST](https://vst.cs.princeton.edu/). The specification and proofs can be found at https://github.com/BlockstreamResearch/simplicity/blob/139ab8d6f455e8d1cc10ad3693e917d2852e1bf3/Coq/C/secp256k1/verif_int128_impl.v, and there is a interactive log of the...

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 more relevant bit is the formal specification of the functions...

The deserialized code for this program is as follows. I've adjusted the references to refer to absolute line numbers instead of relative line numbers to make reading the code "easier"....

Based on a combination of inspecting the above "assembly code" and hand computing the Simfony to Simplicity compilation process, I believe the following is the the Simplicity program that should...

It looks to me like that for some reason rust-simplicity is improperly implementing sharing when serializing this expression. 13: Pair 10 12 This line is `(ooh &&& (unit >>> constWord...

I've got the following program to fail fn main() { let _ : () = (); {let _ : () = (); ()}; let c : () = (); c;...

I think there are really two bugs here. The first bug is that decoding this encoded program should throw a occurs-check failure instead of panicking with what appears to be...