gistfile1.hs

(* Andrew Miller [email protected]

   Just a scratch buffer. Working towards a model of Bitcoin script.

   Sources:
     State/error monads: http://www.lri.fr/~paulin/MPRI/cours-why.pdf
     Coq monad library: 
       http://coq.inria.fr/pylons/contribs/files/QuicksortComplexity/trunk/monads.html
     Another Coq monad library:
       http://coq.inria.fr/pylons/contribs/files/lc/trunk/lc.Monad.html
     
 *)

Require Import List.

Definition ByteString := list nat.
Record BitcoinTransaction := {
  tx_inputs: list (ByteString * nat * nat);
  tx_outputs: list (ByteString * nat * nat)
}.

Definition BtcState := prod ByteString ByteString.

Definition M (A:Set) := option BtcState -> option (BtcState * A).
Definition bind {A B:Set} (f : M A) (g : A -> M B) : M B 
  := fun s => match f s with None => None
           | Some (s', a) => g a (Some s') end.
Definition ret {A:Set} (x:A) : M A 
  := fun s => match s with None => None
           | Some s' => Some (s', x) end.

Notation "x >>= y" := (bind x y) (at level 55).
Notation "x >> y" := (bind x (fun _ => y)) 
         (at level 30, right associativity).
Notation "x <- y ; z" := (bind y (fun x : _ => z)) 
         (at level 30, right associativity).

Definition fail : M unit := fun _ => None.

Definition get : M (ByteString * ByteString)
  := fun s => match s with Some s => Some (s, s) | None => None end.

Definition put (s': ByteString * ByteString) : M unit
  := fun s => match s with Some s => Some (s, tt) | None => None end.

Definition getMain : M ByteString 
  := s <- get; match s with (main, alt) => ret main end.

Definition putMain (main':ByteString) : M unit
  := s <- get; match s with (main, alt) => put (main', alt) end.

Definition OP_DUP_d : M unit := s <- getMain; 
                     match s with x1::s' => putMain (x1::x1::s') 
                                | _ => fail end.

Definition OP_TOALTSTACK_d : M unit := s <- get;
                     match s with (x1::s', a) => put (s', x1::a)
                                | _ => fail end.   

Definition OP_RETURN_d := fail.