YOSHIHIRO Imai yoshihiro503

gh_pages の設定方法

githubプロジェクト作成
circleci プロジェクト登録
$ ssh-keygen -m PEM -t rsa -C "[email protected]" -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にする

通常盤tezos node (mainnnet) の実行

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

sudo apt -y install libev-dev libhidapi-dev

brew install z3

	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

	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.

	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}

	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.(-)".

	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)