add key_hash type and crypto_key_hash operator to pascaligo

This commit is contained in:
Lesenechal Remi 2019-11-21 13:12:52 +01:00
parent 87d0064113
commit 88a0f33fca
23 changed files with 62 additions and 8 deletions

View File

@ -438,6 +438,9 @@ and type_expression : environment -> Solver.state -> ?tv_opt:O.type_value -> I.e
| E_literal (Literal_key s) -> (
return_wrapped (e_key s) state @@ Wrap.literal (t_key ())
)
| E_literal (Literal_key_hash s) -> (
return_wrapped (e_key_hash s) state @@ Wrap.literal (t_key_hash ())
)
| E_literal (Literal_chain_id s) -> (
return_wrapped (e_chain_id s) state @@ Wrap.literal (t_chain_id ())
)
@ -1010,6 +1013,7 @@ let untype_literal (l:O.literal) : I.literal result =
| Literal_int n -> ok (Literal_int n)
| Literal_string s -> ok (Literal_string s)
| Literal_key s -> ok (Literal_key s)
| Literal_key_hash s -> ok (Literal_key_hash s)
| Literal_chain_id s -> ok (Literal_chain_id s)
| Literal_signature s -> ok (Literal_signature s)
| Literal_bytes b -> ok (Literal_bytes b)

View File

@ -406,6 +406,8 @@ and type_expression' : environment -> ?tv_opt:O.type_value -> I.expression -> O.
return (E_literal (Literal_string s)) (t_string ())
| E_literal (Literal_key s) ->
return (E_literal (Literal_key s)) (t_key ())
| E_literal (Literal_key_hash s) ->
return (E_literal (Literal_key_hash s)) (t_key_hash ())
| E_literal (Literal_chain_id s) ->
return (E_literal (Literal_chain_id s)) (t_chain_id ())
| E_literal (Literal_signature s) ->
@ -816,6 +818,7 @@ let untype_literal (l:O.literal) : I.literal result =
| Literal_string s -> ok (Literal_string s)
| Literal_signature s -> ok (Literal_signature s)
| Literal_key s -> ok (Literal_key s)
| Literal_key_hash s -> ok (Literal_key_hash s)
| Literal_chain_id s -> ok (Literal_chain_id s)
| Literal_bytes b -> ok (Literal_bytes b)
| Literal_address s -> ok (Literal_address s)

View File

@ -130,6 +130,7 @@ let rec transpile_type (t:AST.type_value) : type_value result =
| T_constant (Type_name "unit", []) -> ok (T_base Base_unit)
| T_constant (Type_name "operation", []) -> ok (T_base Base_operation)
| T_constant (Type_name "signature", []) -> ok (T_base Base_signature)
| T_constant (Type_name "key_hash", []) -> ok (T_base Base_key_hash)
| T_constant (Type_name "key", []) -> ok (T_base Base_key)
| T_constant (Type_name "chain_id", []) -> ok (T_base Base_chain_id)
| T_constant (Type_name "contract", [x]) ->
@ -241,6 +242,7 @@ let rec transpile_literal : AST.literal -> value = fun l -> match l with
| Literal_address s -> D_string s
| Literal_signature s -> D_string s
| Literal_key s -> D_string s
| Literal_key_hash s -> D_string s
| Literal_chain_id s -> D_string s
| Literal_operation op -> D_operation op
| Literal_unit -> D_unit

View File

@ -156,6 +156,12 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression
get_string v in
return (E_literal (Literal_key n))
)
| T_constant (Type_name "key_hash", []) -> (
let%bind n =
trace_strong (wrong_mini_c_value "key_hash" v) @@
get_string v in
return (E_literal (Literal_key_hash n))
)
| T_constant (Type_name "chain_id", []) -> (
let%bind n =
trace_strong (wrong_mini_c_value "chain_id" v) @@

View File

@ -32,6 +32,7 @@ module Ty = struct
let mutez = Mutez_t None
let string = String_t None
let key = Key_t None
let key_hash = Key_hash_t None
let chain_id = Chain_id_t None
let list a = List_t (a, None , has_big_map a)
let set a = Set_t (a, None)
@ -71,6 +72,7 @@ module Ty = struct
| Base_operation -> fail (not_comparable "operation")
| Base_signature -> fail (not_comparable "signature")
| Base_key -> fail (not_comparable "key")
| Base_key_hash -> fail (not_comparable "key_hash")
| Base_chain_id -> fail (not_comparable "chain_id")
let comparable_type : type_value -> ex_comparable_ty result = fun tv ->
@ -88,7 +90,7 @@ module Ty = struct
let base_type : type_base -> ex_ty result = fun b ->
let return x = ok @@ Ex_ty x in
match b with
match b with
| Base_unit -> return unit
| Base_void -> fail (not_compilable_type "void")
| Base_bool -> return bool
@ -102,6 +104,7 @@ module Ty = struct
| Base_operation -> return operation
| Base_signature -> return signature
| Base_key -> return key
| Base_key_hash -> return key_hash
| Base_chain_id -> return chain_id
let rec type_ : type_value -> ex_ty result =
@ -186,6 +189,7 @@ let base_type : type_base -> O.michelson result =
| Base_operation -> ok @@ O.prim T_operation
| Base_signature -> ok @@ O.prim T_signature
| Base_key -> ok @@ O.prim T_key
| Base_key_hash -> ok @@ O.prim T_key_hash
| Base_chain_id -> ok @@ O.prim T_chain_id
let rec type_ : type_value -> O.michelson result =

View File

@ -36,12 +36,10 @@ let rec translate_value (Ex_typed_value (ty, value)) : value result =
(Tezos_base__TzPervasives.Chain_id.b58check_encoding)
id in
ok @@ D_string str
| (Key_hash_t _ ), n ->
ok @@ D_string (Signature.Public_key_hash.to_b58check n)
| (Key_t _ ), n ->
let%bind s = match n with
| Ed25519 x -> ok @@ TP.Base58.simple_encode (TP.Ed25519.Public_key.b58check_encoding) x
| Secp256k1 x -> ok @@ TP.Base58.simple_encode (TP.Secp256k1.Public_key.b58check_encoding) x
| P256 x -> ok @@ TP.Base58.simple_encode (TP.P256.Public_key.b58check_encoding) x in
ok @@ D_string s
ok @@ D_string (Signature.Public_key.to_b58check n)
| (Timestamp_t _), n ->
let n =
Z.to_int @@

View File

@ -127,6 +127,7 @@ module Typer = struct
t_bytes () ;
t_address () ;
t_timestamp () ;
t_key_hash () ;
] in
ok @@ t_bool ()

View File

@ -80,6 +80,7 @@ module Simplify = struct
("string_concat" , "CONCAT") ;
("string_slice" , "SLICE") ;
("crypto_check", "CHECK_SIGNATURE") ;
("crypto_hash_key", "HASH_KEY") ;
("bytes_concat" , "CONCAT") ;
("bytes_slice" , "SLICE") ;
("bytes_pack" , "PACK") ;

View File

@ -31,6 +31,7 @@ let literal ppf (l:literal) = match l with
| Literal_address s -> fprintf ppf "@%S" s
| Literal_signature s -> fprintf ppf "@%S" s
| Literal_key s -> fprintf ppf "@%S" s
| Literal_key_hash s -> fprintf ppf "@%S" s
| Literal_chain_id s -> fprintf ppf "@%S" s
| Literal_operation _ -> fprintf ppf "Operation(...bytes)"

View File

@ -26,6 +26,7 @@ let t_unit : type_expression = T_constant ("unit", [])
let t_address : type_expression = T_constant ("address", [])
let t_signature : type_expression = T_constant ("signature", [])
let t_key : type_expression = T_constant ("key", [])
let t_key_hash : type_expression = T_constant ("key_hash", [])
let t_option o : type_expression = T_constant ("option", [o])
let t_list t : type_expression = T_constant ("list", [t])
let t_variable n : type_expression = T_variable n
@ -66,6 +67,7 @@ let e_address ?loc s : expression = location_wrap ?loc @@ E_literal (Literal_add
let e_mutez ?loc s : expression = location_wrap ?loc @@ E_literal (Literal_mutez s)
let e_signature ?loc s : expression = location_wrap ?loc @@ E_literal (Literal_signature s)
let e_key ?loc s : expression = location_wrap ?loc @@ E_literal (Literal_key s)
let e_key_hash ?loc s : expression = location_wrap ?loc @@ E_literal (Literal_key_hash s)
let e_chain_id ?loc s : expression = location_wrap ?loc @@ E_literal (Literal_chain_id s)
let e'_bytes b : expression' result =
let%bind bytes = generic_try (simple_error "bad hex to bytes") (fun () -> Hex.to_bytes (`Hex b)) in

View File

@ -18,7 +18,8 @@ val t_nat : type_expression
val t_tez : type_expression
val t_unit : type_expression
val t_address : type_expression
val t_key : type_expression
val t_key : type_expression
val t_key_hash : type_expression
val t_signature : type_expression
(*
val t_option : type_expression -> type_expression
@ -55,6 +56,7 @@ val e_string : ?loc:Location.t -> string -> expression
val e_address : ?loc:Location.t -> string -> expression
val e_signature : ?loc:Location.t -> string -> expression
val e_key : ?loc:Location.t -> string -> expression
val e_key_hash : ?loc:Location.t -> string -> expression
val e_chain_id : ?loc:Location.t -> string -> expression
val e_mutez : ?loc:Location.t -> int -> expression
val e'_bytes : string -> expression' result

View File

@ -67,6 +67,9 @@ let assert_literal_eq (a, b : literal * literal) : unit result =
| Literal_key a, Literal_key b when a = b -> ok ()
| Literal_key _, Literal_key _ -> fail @@ different_literals "different key" a b
| Literal_key _, _ -> fail @@ different_literals_because_different_types "key vs non-key" a b
| Literal_key_hash a, Literal_key_hash b when a = b -> ok ()
| Literal_key_hash _, Literal_key_hash _ -> fail @@ different_literals "different key_hash" a b
| Literal_key_hash _, _ -> fail @@ different_literals_because_different_types "key_hash vs non-key_hash" a b
| Literal_chain_id a, Literal_chain_id b when a = b -> ok ()
| Literal_chain_id _, Literal_chain_id _ -> fail @@ different_literals "different chain_id" a b
| Literal_chain_id _, _ -> fail @@ different_literals_because_different_types "chain_id vs non-chain_id" a b

View File

@ -97,6 +97,7 @@ and literal =
| Literal_timestamp of int
| Literal_signature of string
| Literal_key of string
| Literal_key_hash of string
| Literal_chain_id of string
| Literal_operation of Memory_proto_alpha.Protocol.Alpha_context.packed_internal_operation

View File

@ -76,6 +76,7 @@ and literal ppf (l:literal) : unit =
| Literal_address s -> fprintf ppf "@%s" s
| Literal_signature s -> fprintf ppf "@%s" s
| Literal_key s -> fprintf ppf "@%s" s
| Literal_key_hash s -> fprintf ppf "@%s" s
| Literal_operation _ -> fprintf ppf "Operation(...bytes)"
| Literal_chain_id s -> fprintf ppf "@%s" s

View File

@ -246,6 +246,7 @@ let e_timestamp s : expression = E_literal (Literal_timestamp s)
let e_address s : expression = E_literal (Literal_address s)
let e_signature s : expression = E_literal (Literal_signature s)
let e_key s : expression = E_literal (Literal_key s)
let e_key_hash s : expression = E_literal (Literal_key_hash s)
let e_chain_id s : expression = E_literal (Literal_chain_id s)
let e_operation s : expression = E_literal (Literal_operation s)
let e_lambda l : expression = E_lambda l

View File

@ -123,6 +123,7 @@ val e_timestamp : int -> expression
val e_address : string -> expression
val e_signature : string -> expression
val e_key : string -> expression
val e_key_hash : string -> expression
val e_chain_id : string -> expression
val e_operation : Memory_proto_alpha.Protocol.Alpha_context.packed_internal_operation -> expression
val e_lambda : lambda -> expression

View File

@ -386,6 +386,9 @@ let assert_literal_eq (a, b : literal * literal) : unit result =
| Literal_key a, Literal_key b when a = b -> ok ()
| Literal_key _, Literal_key _ -> fail @@ different_literals "different key" a b
| Literal_key _, _ -> fail @@ different_literals_because_different_types "key vs non-key" a b
| Literal_key_hash a, Literal_key_hash b when a = b -> ok ()
| Literal_key_hash _, Literal_key_hash _ -> fail @@ different_literals "different key_hash" a b
| Literal_key_hash _, _ -> fail @@ different_literals_because_different_types "key_hash vs non-key_hash" a b
| Literal_chain_id a, Literal_chain_id b when a = b -> ok ()
| Literal_chain_id _, Literal_chain_id _ -> fail @@ different_literals "different chain_id" a b
| Literal_chain_id _, _ -> fail @@ different_literals_because_different_types "chain_id vs non-chain_id" a b

View File

@ -128,6 +128,7 @@ and literal =
| Literal_address of string
| Literal_signature of string
| Literal_key of string
| Literal_key_hash of string
| Literal_chain_id of string
| Literal_operation of Memory_proto_alpha.Protocol.Alpha_context.packed_internal_operation

View File

@ -22,6 +22,7 @@ let type_base ppf : type_base -> _ = function
| Base_operation -> fprintf ppf "operation"
| Base_signature -> fprintf ppf "signature"
| Base_key -> fprintf ppf "key"
| Base_key_hash -> fprintf ppf "key_hash"
| Base_chain_id -> fprintf ppf "chain_id"
let rec type_ ppf : type_value -> _ = function

View File

@ -7,7 +7,7 @@ type type_base =
| Base_timestamp
| Base_string | Base_bytes | Base_address | Base_key
| Base_operation | Base_signature
| Base_chain_id
| Base_chain_id | Base_key_hash
type 'a annotated = string option * 'a

View File

@ -103,6 +103,7 @@ module Substitution = struct
| (T.Literal_address _ as x)
| (T.Literal_signature _ as x)
| (T.Literal_key _ as x)
| (T.Literal_key_hash _ as x)
| (T.Literal_chain_id _ as x)
| (T.Literal_operation _ as x) ->
ok @@ x

View File

@ -0,0 +1,5 @@
function check_hash_key (const kh1 : key_hash; const k2 : key) : bool*key_hash is block {
var ret : bool := False ;
var kh2 : key_hash := crypto_hash_key(k2) ;
if kh1 = kh2 then ret := True else skip;
} with (ret, kh2)

View File

@ -1277,7 +1277,19 @@ let chain_id () : unit result =
let%bind () = expect_eq program "get_chain_id" make_input make_expected in
ok ()
let key_hash () : unit result =
let open Tezos_crypto in
let (raw_pkh,raw_pk,_) = Signature.generate_key () in
let pkh_str = Signature.Public_key_hash.to_b58check raw_pkh in
let pk_str = Signature.Public_key.to_b58check raw_pk in
let%bind program = type_file "./contracts/key_hash.ligo" in
let make_input = e_pair (e_key_hash pkh_str) (e_key pk_str) in
let make_expected = e_pair (e_bool true) (e_key_hash pkh_str) in
let%bind () = expect_eq program "check_hash_key" make_input make_expected in
ok ()
let main = test_suite "Integration (End to End)" [
test "key hash" key_hash ;
test "chain id" chain_id ;
test "type alias" type_alias ;
test "function" function_ ;