yoshihiro503

Require Import List.
Import ListNotations.

Fixpoint list_map {A B:Type} (f : A -> B) (xs : list A) :=
  match xs with
  | [] => []
  | x :: xs => f x :: list_map f xs
  end.
  
Theorem list_map_length : forall (A B: Type) (f: A -> B) xs,

yoshihiro503

概要

ブロックチェーン Tezos において、ノードの立ち上げやクライアントを使ったインタラクションをOCaml上で実行できるフレームワーク Tezt が爆誕したので試してみる。

Tezt とはなに？

Tezos開発者がOCamlでTezosの tezos プロジェクトに内包される形で提供されようとして現在 Merge Request が出ている段階である。

• MR: https://gitlab.com/tezos/tezos/-/merge_requests/1881
• source code: https://gitlab.com/nomadic-labs/tezos/-/tree/romain-tezt

yoshihiro503

Preparation

mube@euler:~/gitlab/tezos/tezos-v7-release$ git log -n 1 --pretty=oneline
51977265590ba5fbd166b921e265fa22bf9f66a6 (HEAD -> v7-release, tag: v7.1, origin/v7-release, origin/latest-release) Changelog: add version 7.1 changes

mube@euler:~/gitlab/tezos/tezos-v7-release$ mkdir mockup-base-dir
mube@euler:~/gitlab/tezos/tezos-v7-release$ ./tezos-client --base-dir mockup-base-dir/ list mockup protocols

yoshihiro503

Require Import Premise.

Fixpoint hash node :=
  match node with
  | Bud None => zerohash
  | Bud (Some n) => h 2 (hash n)
  | Leaf v => h 0 (hash_of_value v)
  | Internal n1 n2 => h 1 (hash n1 ^^ hash n2)
  | Extender seg n => hash n ^^ seg
  end.

yoshihiro503

Install

opam switch create flextesa ocaml-base-compiler.4.07.1
eval $(opam env)
opam install dune.1.11.4
opam install -y fmt cohttp-lwt-unix dum
opam install genspio ezjsonm
opam install lwt_log ptime mtime zarith json-data-encoding-bson
opam install lwt-canceler bigstring

yoshihiro503

open SCaml

type balances = (address, nat) map
type storage = balances

type parameter =
  | Activate
  | Send of {to_ : address; amount : nat}

let activate addr (balances : balances) =

yoshihiro503

Environment

• Tezos 28309c81c on mainnnet

Example: Add /hoge RPC API

--- a/src/lib_shell_services/p2p_services.ml
+++ b/src/lib_shell_services/p2p_services.ml
@@ -69,6 +69,13 @@ module S = struct

yoshihiro503

Require Import List.
Import ListNotations.

Lemma fst_injective : forall {A B: Type} (p1 p2: A * B),
    fst p1 <> fst p2 -> p1 <> p2.
Proof.
  intros A B p1 p2. destruct p1, p2. simpl. intros Ha Hp.
  elim Ha. now injection Hp.
Qed.

yoshihiro503

環境

使用マシン

• OS: Ubuntu 18.04
• opam : 2.0.0

使用ディレクトリ

• ~/tezos-mainnet/ : main1 のコードベース
• ~/tezos/ : main2 開始のためのコードベース
• /sandisk/ : 内蔵SSD 1.8 TB

yoshihiro503

open SCaml

type parameter = nat * unit contract * unit

type storage = nat

let main (param: parameter) (storage: storage) =
  let (counter, contr, sigs) = param in
  (*  let counter = counter in *) (* If this line is available then the typecheck will be passed. *)
  if counter <> Nat 1 then failwith "0" else