[WIP] Specification language for Liquidity

Makefile

@@ -27,14 +27,16 @@ distclean: clean
 
 # All of these tests must be run with with_tezos=true
 
-NTESTS=20
+NTESTS=32
+NTESTS=21
+NREVTESTS=6
 SIMPLE_TESTS= `seq -f 'test%.0f' 0 $(NTESTS)`
 MORE_TESTS=test_ifcons test_if test_loop test_option test_transfer test_left \
   test_extfun test_left_constr test_closure test_closure2 test_closure3 \
   test_map test_rev test_reduce_closure test_map_closure test_mapreduce_closure \
   test_mapmap_closure test_setreduce_closure test_left_match
 OTHER_TESTS=others/broker others/demo others/auction
-REV_TESTS=`seq -f  'test%.0f' 0 5`
+REV_TESTS=`seq -f  'test%.0f' 0 $(NREVTESTS)`
 
 NEW_TEZOS_TESTS= fail weather_insurance
 FAILING_TEZOS_TESTS= originator

check.sh

@@ -7,28 +7,32 @@ test=$1
 echo "\n[check.sh] test = $test"
 
 LIQUIDITY=liquidity
+TEZOS_FULL_PATH=./tezos/_obuild/tezos-client/tezos-client.asm
+LIQUID_FULL_PATH=./_obuild/${LIQUIDITY}/${LIQUIDITY}.asm
+LIQARGS=--verbose
+LIQEXEC="${LIQUID_FULL_PATH} ${LIQARGS}"
 
-echo ./_obuild/${LIQUIDITY}/${LIQUIDITY}.asm tests/$test.liq
-./_obuild/${LIQUIDITY}/${LIQUIDITY}.asm tests/$test.liq || exit 2
+echo ${LIQEXEC} tests/$test.liq
+${LIQEXEC} tests/$test.liq || exit 2
 
-if [ -f ./tezos/_obuild/tezos-client/tezos-client.asm ] ; then
-    ./tezos/_obuild/tezos-client/tezos-client.asm typecheck program tests/$test.liq.tz || exit 2
+if [ -f ${TEZOS_FULL_PATH} ] ; then
+    ${TEZOS_FULL_PATH} typecheck program tests/$test.liq.tz || exit 2
 else
-    echo "\n${RED}./tezos/_obuild/tezos-client/tezos-client.asm not present ! typechecking of tests/$test.liq.tz skipped${DEFAULT}\n"
+    echo "\n${RED}${TEZOS_FULL_PATH} not present ! typechecking of tests/$test.liq.tz skipped${DEFAULT}\n"
 fi
 
-echo ./_obuild/${LIQUIDITY}/${LIQUIDITY}.asm tests/$test.liq.tz
-./_obuild/${LIQUIDITY}/${LIQUIDITY}.asm tests/$test.liq.tz || exit 2
+echo ${LIQEXEC} tests/$test.liq.tz
+${LIQEXEC} tests/$test.liq.tz || exit 2
 
-echo ./_obuild/${LIQUIDITY}/${LIQUIDITY}.asm tests/$test.liq.tz.liq 
-./_obuild/${LIQUIDITY}/${LIQUIDITY}.asm tests/$test.liq.tz.liq || exit 2
+echo ${LIQEXEC} tests/$test.liq.tz.liq 
+${LIQEXEC} tests/$test.liq.tz.liq || exit 2
 
-if [ -f ./tezos/_obuild/tezos-client/tezos-client.asm ] ; then
-    ./tezos/_obuild/tezos-client/tezos-client.asm typecheck program tests/$test.liq.tz.liq.tz || exit 2
+if [ -f ${TEZOS_FULL_PATH} ] ; then
+    ${TEZOS_FULL_PATH} typecheck program tests/$test.liq.tz.liq.tz || exit 2
 else
-    echo "\n${RED}./tezos/_obuild/tezos-client/tezos-client.asm not present ! typechecking of tests/$test.liq.tz.liq.tz skipped${DEFAULT}\n"
+    echo "\n${RED}${TEZOS_FULL_PATH} not present ! typechecking of tests/$test.liq.tz.liq.tz skipped${DEFAULT}\n"
 fi
 
 echo ./_obuild/ocp-liquidity-comp/ocp-liquidity-comp.asm -I +../zarith zarith.cma -I _obuild/liquidity-env ./_obuild/liquidity-env/liquidity-env.cma -impl tests/$test.liq
-./_obuild/ocp-liquidity-comp/ocp-liquidity-comp.asm -I +../zarith zarith.cma -I _obuild/liquidity-env ./_obuild/liquidity-env/liquidity-env.cma -dsource -impl tests/$test.liq
+./_obuild/ocp-liquidity-comp/ocp-liquidity-comp.asm -I +../zarith zarith.cma -I _obuild/liquidity-env unix.cma ./_obuild/liquidity-env/liquidity-env.cma -dsource -impl tests/$test.liq || exit 2
 rm -f a.out

libs/deps-michelson/build.ocp2

@@ -10,15 +10,14 @@
 (* This part of the library is made to create a minimal set of dependencies
 to be able to run code that was directly extracted from Tezos *)
 
-if( with_tezos ) {
 
-OCaml.library("michelson-deps", ocaml + {
-     bytelink = [ "-custom" ];
-     files = [
+OCaml.library("ocplib-blockchain-crypto", ocaml + {
+  bytelink = [ "-custom" ];
+  files = [
 
         "sha256.c"; (* from Polar SSL *)
         "sha256-stubs.c";
-        
+
         "tweetnacl.c";
         "blake2b-ref.c";    (* from BLAKE/BLAKE *)
         "blake2b-stubs.c";
@@ -32,6 +31,18 @@ OCaml.library("michelson-deps", ocaml + {
         "mBytes.ml";
         "hex_encode.ml"; 
         "nocrypto.ml";
+  ];
+  requires = [
+     "ocplib-endian";
+  ];
+   cclib = [ "-lsecp256k1" ]
+  });
+
+if( with_tezos ) {
+
+OCaml.library("michelson-deps", ocaml + {
+     files = [
+
 
         "sodium.ml";
 
@@ -50,9 +61,9 @@ OCaml.library("michelson-deps", ocaml + {
         "updater.ml";
      ];
      requires = [
-        "ocplib-endian";     (* mBytes *)
+
+        "ocplib-blockchain-crypto";
      ];
-     cclib = [ "-lsecp256k1" ]
 }); 
 
 }

libs/deps-michelson/mBytes.ml

@@ -1,6 +1,6 @@
 type t = bytes
 
-let create = String.create
+let create = Bytes.create
 let length = String.length
 let compare = compare
 
@@ -11,7 +11,7 @@ let of_string s = s
 let blit = String.blit
 let blit_from_string = String.blit
 let blit_to_bytes = String.blit
-let copy = String.copy
+let copy = Bytes.copy
 let sub = String.sub
 let substring = String.sub
 let concat = (^)

libs/deps-michelson/mBytes.mli

@@ -1,11 +1,3 @@
-(**************************************************************************)
-(*                                                                        *)
-(*    Copyright (c) 2014 - 2016.                                          *)
-(*    Dynamic Ledger Solutions, Inc. <[email protected]>                  *)
-(*                                                                        *)
-(*    All rights reserved. No warranty, explicit or implicit, provided.   *)
-(*                                                                        *)
-(**************************************************************************)
 
 type t = bytes
 
@@ -14,12 +6,6 @@ val create: int -> t
 val length: t -> int
 
 val compare : t -> t -> int
-(*
-
-open Bigarray
-
-type t = (char, int8_unsigned_elt, c_layout) Array1.t
- *)
 
 val copy: t -> t
 
@@ -28,22 +14,13 @@ val sub: t -> int -> int -> t
     and of length [len]. No copying of elements is involved: the
     sub-array and the original array share the same storage space. *)
 
-                                               (*
-
-val shift: t -> int -> t
-(** [shift src ofs] is equivalent to [sub src ofs (length src - ofs)] *)
- *)
-
 val blit: t -> int -> t -> int -> int -> unit
 (** [blit src ofs_src dst ofs_dst len] copy [len] bytes from [src]
     starting at [ofs_src] into [dst] starting at [ofs_dst].] *)
 
 val blit_from_string: string -> int -> t -> int -> int -> unit
 (** See [blit] *)
 
-val blit_to_bytes: t -> int -> bytes -> int -> int -> unit
-(** See [blit] *)
-
 val of_string: string -> t
 (** [of_string s] create an byte array filled with the same content than [s]. *)
 
@@ -74,7 +51,6 @@ val set_int8: t -> int -> int -> unit
 (** [set_int8 buff i v] writes the least significant 8 bits of [v]
     to [buff] at offset [i] *)
 
-(** Functions reading according to Big Endian byte order *)
 
 val get_uint16: t -> int -> int
 (** [get_uint16 buff i] reads 2 bytes at offset i as an unsigned int
@@ -90,9 +66,6 @@ val get_int32: t -> int -> int32
 val get_int64: t -> int -> int64
 (** [get_int64 buff i] reads 8 bytes at offset i as an int64. *)
 
-val get_float: t -> int -> float
-(** [get_float buff i] reads 4 bytes at offset i as an IEEE754 float. *)
-
 val get_double: t -> int -> float
 (** [get_float buff i] reads 8 bytes at offset i as an IEEE754 double. *)
 
@@ -106,52 +79,8 @@ val set_int32: t -> int -> int32 -> unit
 val set_int64: t -> int -> int64 -> unit
 (** [set_int64 buff i v] writes [v] to [buff] at offset [i] *)
 
+
 val set_double: t -> int -> float -> unit
 (** [set_double buff i v] writes [v] to [buff] at offset [i] *)
 
-(*
-
-val set_float: t -> int -> float -> unit
-(** [set_float buff i v] writes [v] to [buff] at offset [i] *)
-val of_float: float -> t
-
-module LE: sig
-
-  (** Functions reading according to Little Endian byte order *)
-
-  val get_uint16: t -> int -> int
-  (** [get_uint16 buff i] reads 2 bytes at offset i as an unsigned int
-      of 16 bits. i.e. It returns a value between 0 and 2^16-1 *)
-
-  val get_int16: t -> int -> int
-  (** [get_int16 buff i] reads 2 byte at offset i as a signed int of
-      16 bits. i.e. It returns a value between -2^15 and 2^15-1 *)
-
-  val get_int32: t -> int -> int32
-  (** [get_int32 buff i] reads 4 bytes at offset i as an int32. *)
-
-  val get_int64: t -> int -> int64
-  (** [get_int64 buff i] reads 8 bytes at offset i as an int64. *)
-
-  val set_int16: t -> int -> int -> unit
-  (** [set_int16 buff i v] writes the least significant 16 bits of [v]
-      to [buff] at offset [i] *)
-
-  val set_int32: t -> int -> int32 -> unit
-  (** [set_int32 buff i v] writes [v] to [buff] at offset [i] *)
-
-  val set_int64: t -> int -> int64 -> unit
-  (** [set_int64 buff i v] writes [v] to [buff] at offset [i] *)
-
-end
-
-val (=) : t -> t -> bool
-val (<>) : t -> t -> bool
-val (<) : t -> t -> bool
-val (<=) : t -> t -> bool
-val (>=) : t -> t -> bool
-val (>) : t -> t -> bool
-val compare : t -> t -> int
- *)
-
 val concat: t -> t -> t

libs/deps-michelson/secp256k1-stubs.c

@@ -386,8 +386,8 @@ value secp256k1_ec_pubkey_create_ml
  const secp256k1_context* ctx =
     (const secp256k1_context*)
     String_val(ctx_v);
- const secp256k1_pubkey *pubkey =
-   (const secp256k1_pubkey *)
+ secp256k1_pubkey *pubkey =
+   (secp256k1_pubkey *)
    String_val(pubkey_v);
  const unsigned char *seckey =
    (const unsigned char *)

libs/michelson/base58.ml

@@ -1 +1,2 @@
+
 #include "../../tezos/src/utils/base58.ml"

libs/michelson/seed_storage.ml

@@ -4,4 +4,6 @@ open Hash
 open Utils
 open Tezos_data
 
+open Storage.Seed
+open Level_repr
 #include "../../tezos/src/proto/alpha/seed_storage.ml"

libs/michelson/vote_storage.ml

@@ -4,4 +4,6 @@ open Hash
 open Utils
 open Tezos_data
 
+open Vote_repr
+open Voting_period_repr
 #include "../../tezos/src/proto/alpha/vote_storage.ml"

tests/others/auction.liq

@@ -1,6 +1,6 @@
 (* Auction contract from https://www.michelson-lang.com/contract-a-day.html *)
 
-[%%version 0.11]
+[%%version 0.13]
 
 type storage = {
   auction_end : timestamp;
@@ -11,11 +11,14 @@ type storage = {
 let%entry main
     (parameter : key_hash)
     (storage : storage)
-    : unit * storage =
+  : unit * storage
+    [@requires storage.highest_bid < Current.balance () ]
+    [@ensures  @storage.highest_bid < Current.balance () ]
+  =
 
   (* Check if auction has ended *)
   if Current.time () > storage.auction_end then Current.fail ();
-  
+
   let new_bid = Current.amount () in
   let new_bidder = parameter in
   (* Check if new bid is higher that the last *)

tests/others/broker.liq

@@ -1,5 +1,5 @@
 
-[%%version 0.11]
+[%%version 0.13]
 
 type storage = {
   state : string;

tests/others/demo.liq

@@ -1,5 +1,5 @@
 
-[%%version 0.11]
+[%%version 0.13]
 
 let%entry main
   (parameter : string)