juvix/examples/token.mjuvix

module Token;

import Data.Nat;
open Data.Nat using {<=};

import Data.String;
open Data.String using {compare};

--------------------------------------------------------------------------------
-- Boiler plate taken from previous code
--------------------------------------------------------------------------------

{-
total_order : (a:eqtype) (f: (a -> a -> Tot Bool)) =
   (forall a1 a2. (f a1 a2 /\ f a2 a1)  ==> a1 = a2)  (* anti-symmetry *)
 /\ (forall a1 a2 a3. f a1 a2 /\ f a2 a3 ==> f a1 a3)  (* transitivity  *)
 /\ (forall a1 a2. f a1 a2 \/ f a2 a1)                (* totality      *)

string_cmp' s1 s2 =  String.compare s1 s2 <= 0

(* The F* defn just calls down to OCaml, since we know comparison in OCaml is total
 * just admit it
 *)

string_cmpTotal : unit -> Lemma (total_order string string_cmp')
string_cmpTotal () = admit ()

// hack function so, the data structure doesn't forget the proof!
string_cmp : Map.cmp string
string_cmp = string_cmpTotal (); string_cmp'

-}

--------------------------------------------------------------------------------
-- Type definitions
--------------------------------------------------------------------------------

Address : Type;
Address := String;

-- Accounts : Map.ordmap Address Nat string_cmp

inductive Account {
  mkAccount : Nat -> SortedMap Address Nat -> Account;
}

balance : Account -> Nat;
balance (mkAccount n _) := n;

allowances : Account -> SortedMap Address Nat ;
allowances (mkAccount _ s) := s;


add_account_values_acc : Accounts → Nat -> Nat
add_account_values_acc Accounts n  =
 MapProp.fold (fun _key (v : Nat) (acc : Nat) -> v + acc) Accounts n

// we have to specify they are Nats :(
add_account_values : Accounts -> Nat
add_account_values Accounts =
 MapProp.fold (fun _key (v : Nat) (acc : Nat) -> v + acc) Accounts 0

inductive Storage {
  mkStorage : Nat -> Accounts
  total-supply : Nat;
  Accounts : a : Accounts { total-supply = add_account_values a };
}

empty-storage : storage
empty-storage = {
  total-supply = 0;
  Accounts = Map.empty;
}

inductive Token {
  mkToken :
    Storage ->   -- storage
    Nat ->       -- version
    String ->    -- name
    Char ->      -- symbol
    Address ->   -- owner
    Token
}

storage : Token -> Storage;
storage (mkToken s _ _ _ _ _) := s;

version : Token -> Nat;
version (mkToken _ n _ _ _ _) := n;

name    : Token -> String;
name    (mkToken _ _ n _ _ _) := n;

symbol  : Token -> Char;
symbol  (mkToken _ _ _ s _ _) := s;

owner   : Token -> Address;
owner   (mkToken _ _ _ _ _ a) := a;


type txTransfer = {
  from_account    : Address;
  to_account      : Address;
  transfer_amount : Nat
}

type tx_mint = {
  mint_amount     : Nat;
  mintTo_account : Address
}

type tx_burn = {
  burn_amount       : Nat;
  burn_from_account : Address
}

inductive txData {
  transfer : txTransfer -> txData;
  mint     : txMint -> txData;
  burn     : txBurn -> txData;
  }

type tx = {
  tx_data               : tx_data;
  tx_authroized_account : Address;
}

--------------------------------------------------------------------------------
-- Begin Functions On Accounts
--------------------------------------------------------------------------------

has_n : Accounts -> Address -> Nat -> Bool
has_n accounts add toTransfer :=
  match Map.select add Accounts {
   (Some n) -> toTransfer <= n;
   None     -> false;
  }

account-sub :
  (acc : Accounts) ->
  (add : Address) ->
  (num : Nat {has_n acc add num}) ->
  Accounts
account-sub Accounts add number =
  match Map.select add Accounts with
   { Some balance -> Map.update add (balance - number) Accounts };


// No feedback given, so don't know next move :(
transfer-sub : 
  (acc : Accounts) ->
  (add : Address) ->
  (num : Nat) ->
  Lemma ->
  (requires (has_n acc add num)) ->
  (ensures (  add_account_values acc - num
           == add_account_values (account-sub acc add num)))
transfer-sub acc add num :=
  match Map.select add acc {
   Some balance ->;
    remaining : Nat = balance - num in
    admit ()
  };

account_add : acc : Accounts
                -> add : Address
                -> num : Nat
                -> Accounts
account_add acc add num =
  match Map.select add acc with
   Some b' -> Map.update add (b' + num) acc;
   None    -> Map.update add num        acc;

--------------------------------------------------------------------------------
(**** Experimental Proofs on Transfer *)
--------------------------------------------------------------------------------

transfer_add_lemma : acc : Accounts
                       -> add : Address
                       -> num : Nat
                       -> Lemma
                       (ensures
                         (i =
                           match Map.select add acc with
                            None   -> 0;
                            Some v -> v;
                          in i + num = Some?.v (Map.select add (account_add acc add num))))
transfer_add_lemma acc add num = ()

transfer_add_unaffect : acc : Accounts
                          -> add : Address
                          -> num : Nat
                          -> Lemma
                          (ensures
                            (forall x. Map.contains x acc /\ x <> add
                              ==> Map.select x acc = Map.select x (account_add acc add num)))
transfer_add_unaffect acc add num = ()


transfer-same_when_remove : acc : Accounts
                              -> add : Address
                              -> num : Nat
                              -> Lemma
                              (ensures
                                (new_account = account_add acc add num in
                                    add_account_values (Map.remove add acc)
                                 == add_account_values (Map.remove add new_account)))
transfer-same_when_remove acc add num =
  new_account = account_add acc add num in
  assert (Map.equal (Map.remove add acc) (Map.remove add new_account))

// Useful stepping stone to the real answer!
// sadly admitted for now
transfer_acc_behavior : acc : Accounts
                          -> add : Address
                          -> Lemma
                            (ensures
                              (i =
                                match Map.select add acc with
                                 None   -> 0;
                                 Some v -> v;
                                in add_account_values_acc (Map.remove add acc) i
                                  == add_account_values acc))
transfer_acc_behavior acc add =
  admit ()

// No feedback given, so don't know next move :(
transfer_add : acc : Accounts
                 -> add : Address
                 -> num : Nat
                 -> Lemma
                  (ensures ( add_account_values acc + num
                           == add_account_values (account_add acc add num)))
transfer_add acc add num =
  admit ();
  transfer-same_when_remove acc add num;
  transfer_add_unaffect acc add num;
  transfer_add_lemma acc add num

--------------------------------------------------------------------------------
(**** Failed Experimental Proofs Over *)
--------------------------------------------------------------------------------


transfer_acc : acc     : Accounts
                -> add_from : Address
                -> addTo   : Address
                -> num      : Nat {has_n acc add_from num}
                -> Accounts
transfer_acc Accounts add_from addTo number =
  new_Accounts = account-sub Accounts add_from number in
  account_add new_Accounts addTo number

transfer_maintains-supply
  : acc      : Accounts
  -> add_from : Address
  -> addTo   : Address
  -> num      : Nat
  -> Lemma
    (requires (has_n acc add_from num))
    (ensures (add_account_values acc
              == add_account_values (transfer_acc acc add_from addTo num)))
transfer_maintains-supply acc add_from addTo num =
  transfer-sub acc add_from num;
  transfer_add (account-sub acc add_from num) addTo num

transfer-stor
  : stor     : storage
  -> add_from : Address
  -> addTo   : Address
  -> num      : Nat {has_n stor.Accounts add_from num}
  -> storage
transfer-stor stor add_from addTo num =
  new_acc = account_add (account-sub stor.Accounts add_from num) addTo num in
  transfer_maintains-supply stor.Accounts add_from addTo num;
  { total-supply = stor.total-supply;
    Accounts     = new_acc
  }


--------------------------------------------------------------------------------
(* End Type Definitions *)
(**** Begin Validations On Tokens *)
--------------------------------------------------------------------------------


validTransfer : token -> tx -> Bool
validTransfer token tx =
  match tx.tx_data with
   Transfer {from_account; transfer_amount} ->;
    has_n token.storage.Accounts from_account transfer_amount
    && tx.tx_authroized_account = from_account
   Mint _  Burn _ ->;
    false

valid_mint : token -> tx -> Bool
valid_mint token tx =
  match tx.tx_data with
   Mint mint           -> token.owner = tx.tx_authroized_account;
   Transfer _  Burn _ -> false;

valid_burn : token -> tx -> Bool
valid_burn token tx =
  match tx.tx_data with
   Burn {burn_from_account; burn_amount} ->;
    has_n token.storage.Accounts burn_from_account burn_amount
    && tx.tx_authroized_account = burn_from_account
   Transfer _  Mint _ ->;
    false


--------------------------------------------------------------------------------
(* End validations on tokens *)
(**** Begin Functions On Tokens *)
--------------------------------------------------------------------------------

tokenTransaction : (token -> tx -> Bool) -> Type0
tokenTransaction f =
  tok : token -> tx : tx { f tok tx } -> token

transfer : tokenTransaction validTransfer
transfer token transaction =
  match transaction.tx_data with
   Transfer {from_account; to_account; transfer_amount} ->;
    { token
      with storage = transfer-stor token.storage
                                   from_account
                                   to_account
                                   transfer_amount
    }

mint : tokenTransaction valid_mint
mint token transaction =
  match transaction.tx_data with
   Mint {mint_amount; mintTo_account} ->;
    transfer_add token.storage.Accounts mintTo_account mint_amount;
    { token
      with storage = {
        total-supply = token.storage.total-supply + mint_amount;
        Accounts     = account_add token.storage.Accounts mintTo_account mint_amount
      }}

burn : tokenTransaction valid_burn
burn token transaction =
  match transaction.tx_data with
   Burn {burn_from_account; burn_amount} ->;
    transfer-sub token.storage.Accounts burn_from_account burn_amount;
    { token
      with storage = {
        total-supply = token.storage.total-supply - burn_amount;
        Accounts     = account-sub token.storage.Accounts burn_from_account burn_amount
      }}

type transaction_error =
   Not_enough_funds;
   Not-same_account;
   Not_ownerToken;
   Not_enoughTokens;

executeTransaction : token -> tx -> c_or transaction_error token
executeTransaction token tx =
  match tx.tx_data with
   Transfer _ ->;
    if validTransfer token tx
    then Right (transfer token tx)
    else Left Not_enough_funds // todo determine what the error is
   Mint _ ->;
    if valid_mint token tx
    then Right (mint token tx)
    else Left Not_ownerToken
   Burn _ ->;
    if valid_burn token tx
    then Right (burn token tx)
    else Left Not_enoughTokens

validTransferTransaction
  : tok : token
  -> tx  : tx
  -> Lemma (requires (validTransfer tok tx))
          (ensures (
            Right newTok = executeTransaction tok tx in
            tok.storage.total-supply == newTok.storage.total-supply))
validTransferTransaction tok tx = ()


valid_mintTransaction
  : tok : token
  -> tx  : tx
  -> Lemma (requires (valid_mint tok tx))
          (ensures (
            Right newTok = executeTransaction tok tx in
            Mint {mint_amount} = tx.tx_data in
            tok.storage.total-supply + mint_amount == newTok.storage.total-supply))
valid_mintTransaction tok tx = ()

valid_burnTransaction
  : tok : token
  -> tx  : tx
  -> Lemma (requires (valid_burn tok tx))
          (ensures (
            Right newTok = executeTransaction tok tx in
            Burn {burn_amount} = tx.tx_data in
            tok.storage.total-supply - burn_amount == newTok.storage.total-supply))
valid_burnTransaction tok tx = ()

isLeft = function
   Left _  -> true;
   Right _ -> false;

non_validTransaction
  : tok : token
  -> tx  : tx
  -> Lemma (requires (not (valid_burn tok tx)
                   /\ not (valid_mint tok tx)
                   /\ not (validTransfer tok tx)))
          (ensures (isLeft (executeTransaction tok tx)))
non_validTransaction tok tx = ()