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

yoshihiro503

Parameter nat : Set.

Parameter int : Set.
Parameter int_plus : int -> int -> int.
Parameter int_sub : int -> int -> int.
Infix "+" := int_plus.
Infix "-" := int_sub.

Parameter nat_plus : nat -> nat -> nat.
Parameter nat_sub : nat -> nat -> nat.

yoshihiro503

open SCaml

type action =
| Transfer of {amount: tz; dest: unit contract}
| Delegate of key_hash option
| ChangeKeys of {threshold : nat; keys : key list}

type parameter =
  {counter: nat; action: action; sigs : signature option list}

yoshihiro503

Require Export ExtrOcamlBasic.
Require Import SCaml.

Extract Inlined Constant int => "SCaml.int".
Extract Inlined Constant operation => "Scaml.operation".

Extract Inlined Constant int_plus => "SCaml.(+)".
Extract Inlined Constant int_sub => "SCaml.(-)".

yoshihiro503

module OrderedTree

type elem = int

type tree =
  | Leaf
  | Node of (tree * elem * tree)

let rec all_tree pred t =
  match t with

yoshihiro503

gh_pages の設定方法

• githubプロジェクト作成
• circleci プロジェクト登録
• $ ssh-keygen -m PEM -t rsa -C "ci-build@proof-ninja.co.jp" -f ./id_rsa_circleci
• githubのプロジェクト設定画面のDeploy keys項目にAllow write accessをONにして↑の公開鍵 id_rsa_circleci.pub を登録する
  • https://github.com/proof-ninja/proof-ninja.github.io/settings/keys/new
• circleciのプロジェクト設定でSSH permissions項目でAdd SSH Key する(秘密鍵登録), ホスト名はgithub.comにする

yoshihiro503

通常盤tezos node (mainnnet) の実行

mainnetブランチのtezosソースコード

実行準備

export PATH=~/tezos:$PATH
source ./src/bin_client/bash-completion.sh
export TEZOS_CLIENT_UNSAFE_DISABLE_DISCLAIMER=Y

yoshihiro503

必要用件

Ubuntuの場合

sudo apt -y install libev-dev libhidapi-dev

MacOSの場合

yoshihiro503

module Fact

open FStar.Mul

val factorial : x:int{x>=0} -> Tot int
let rec factorial n =
  if n = 0 then 1
  else n * factorial (n - 1)

val fact_tlrec_aux : int -> x:int{x>=0} -> Tot int (decreases x)