What would be an example of a thing we can prove with Simplicity and Coq?

[fiatjaf]

My understanding is that since there is a Simplicity implementation in Coq we can write a Simplicity script in a higher level language or maybe in Haskell and that can be translated automatically into a Coq implementation of that same script that can then be analyzed along with the Simplicity core and then we prove things about it. Is that correct?

I have zero experience with Coq or mathematical proofs, but from some readings I made recently my impression is that given a program you can say generic statements about it and get a response from Coq on if those are true or false. Is that correct?

What are some examples of such generic statements?

---

What I have in mind is something like this (please be patient, I'm a newbie):

1. I write a (very silly) Simplicity program that checks the block height, if < x then check signature A, otherwise check signature B, then check for something else in each case, doesn't matter.
2. But my program is too complex, I can't really know if I wrote it correctly to account for all cases.
3. I then ask Coq: "is there a case in which signature A will not be provided but this script will still succeed even if blockheight > x"?
4. I wait Coq to give a false answer, but if not then I tweak my code to fix that.

[roconnor-blockstream]

Coq works as a proof verification engine. That is, you give Coq your Simplicity expression, a logical statement regarding that expression, a alleged proof that the logical statement is true, and then Coq will tell you whether it believes your proof or not. Note that your statement can be true, but if your proof is wrong, Coq will not accept your proof. In reality, Coq does more than just this check. It is a platform for helping you create your formal proofs.

https://www.youtube.com/watch?v=M4XnDrRIKx8 illustrates an example of proving the correctness of a Simplicity expression for addition of integers. The video uses Agda instead of Coq, but the principles are the two proof assistants are the same. An equivalent proof in Coq can be found at: https://github.com/ElementsProject/simplicity/blob/35627fc49ad96fcb844cca72ffbc69b6e934cb4c/Coq/Simplicity/Word.v#L487-L488

This lemma states that given two n-bit words, a, and b, if you execute the adder Simplicity program on the input containing the pair (a, b) and interpret the result as an integer, that integer is equal to the result of interpreting each of a and b as an integer and adding them together using the mathematical definition of integer addition (Z is often used in mathematics to denote the type of mathematical integers). This proof can also be found written out as regular mathematics in the Simplicity Tech Report. (Note: however, the Simplicity expression for addition has changed a bit in Haskell and eventually the Coq proof will need to be updated.)

This was an example of using proofs about Simplicity "in the small", where you take some sub-expression and prove a property about it. As you observe, we will also want to create proofs "in the large" about the behaviour of entire Simplicity programs. For example, one participant in an HTLC wants to prove two things:

1. That the program can be satisfied with their signature and a locktime value that exceeds some specific threshold τ.
2. That if the program has been satisfied, then either they signed for it, or the preimage of a specific hash has been revealed.

The other participant of the HTLC has a similar set of conditions they want to prove about the program, but with a few clauses swapped around.

How exactly to formalize these cryptographic statements in Coq is still an open research question for me.

[ProofOfKeags]

Quick addendum to this. IIRC Coq does have a means of Haskell program extraction. I'm not sure how flexible this engine is but it might be possible to generate the Haskell-embedded simplicity program directly from Coq, allowing you to do your development directly in Coq (expressions + proofs) and then generate Haskell-embedded simplicity from Coq and then simplicity from Haskell-embedded simplicity. This could be unnecessarily complicated, but it could also prove useful.

Another thing to note @fiatjaf, All dependently typed languages have the property that they can serve as what are called "proof assistants". This is due to the equivalence between functional programming and logic. Idris, Agda, and Coq are the three languages usually referenced here, but -XDependentTypes in Haskell (if it ever actually lands), could give you the ability to do this in Haskell as well.