The Coq mailing list

[Andrew Miller<amiller AT cs.ucf.edu>]

Bitcoin uses a simple stack-based script language with cryptographic 
primitives
(such as a secure hash, digital signature validation) and resource-consuming
operations (such as queries to a DHT to reference earlier Bitcoin
transactions).

There are a few things I hope to accomplish by modeling Bitcoin in Coq:
- Show that bitcoin validation can be done by a machine with a termination
proof
- Generalize about the resource bounds, parameterized by families of script
(similar to Quicksort worst-case proof [1])
- Theorems about families of scripts, extensional equivalence between scripts

I started with a pure functional script evaluator. [*] I was able to use my
novice ability (and whatever I could remember from the CPDT book) to prove
simple examples about �scripts� under this specification. [**] Unfortunately
there�s a lot of repetition, and it doesn�t seem like I�d be able to reuse 
this
code if I add more features. I�d like to end up with the flexibility of [1]
where a monadic definition of the machine is �upgraded� by passing it a monad
with �virtual instruments� that enable proofs about resource counting, etc. It
was easy enough to make an adhoc form of this monad [***], but it would be
better to use more general components. (thanks to Russel O�Connor for an
elegant haskell bitcoin validator)

It seems like the code in [1] would be easier to use if it took advantage of
typeclasses. In fact, mattam�s typeclass-based port of the Haskell Prelude [2]
looks promising, but I couldn�t find a Coq version to compile it correctly, 
nor
was I able to nudge the typeclass syntax into compatibility with 8.3pl3. Other
alternatives may be to use the HoareStateMonad [3] or Ynot [4], although I now
think these rule out termination proofs are are not a necessary abstraction 
for
my needs.

So my questions are, 
    a. What is the preferred choice for monadic frameworks in Coq? How should 
I
evaluate these alternatives[1-4], any of which I might use with a bit more
effort? 
    b. am I on the right track at all?

[1] Eelis QuicksortComplexity especially (monads) and (qs_definitions).
http://coq.inria.fr/pylons/pylons/contribs/view/QuicksortComplexity/trunk
[2] Matthieu Sozeau�s port of Haskell Prelude to Coq
http://mattam.org/repos/coq/prelude/
[3] Wouter Swiestra
http://www.cs.ru.nl/~wouters/Publications/HoareLogicStateMonad.pdf
[4] Ynot http://ynot.cs.harvard.edu/papers/ynot08.pdf

[*]
https://github.com/amiller/CoinCoq/blob/626d26e312af650a15d403c51c9bde1690d13d7
1/BitcoinScript.v 
[*]
https://github.com/amiller/CoinCoq/blob/626d26e312af650a15d403c51c9bde1690d13d7
1/Examples.v
[***] http://coq.xelpaste.org/4387