Skip to content

Commit b0db14a

Browse files
fjahrfjahr
committed
WIP: Add BIP340 example
1 parent af6d100 commit b0db14a

File tree

9 files changed

+911
-2
lines changed

9 files changed

+911
-2
lines changed

‎examples/Cargo.toml‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
[workspace]
22
members = [
3+
"bip-340",
34
"chacha20",
45
"limited-order-book",
56
"sha256",

‎examples/Makefile‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
.PHONY: default
22
default:
33
make -C limited-order-book
4+
make -C bip-340
45
make -C chacha20
56
make -C sha256
67
make -C barrett
@@ -9,6 +10,7 @@ default:
910

1011
clean:
1112
make -C limited-order-book clean
13+
make -C bip-340 clean
1214
make -C chacha20 clean
1315
make -C sha256 clean
1416
make -C barrett clean

‎examples/bip-340/Cargo.toml‎

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
[package]
2+
name = "bip-340"
3+
version = "0.1.0"
4+
authors = ["Jonas Nick <jonasd.nick@gmail.com>", "Fabian Jahr <fjahr@protonmail.com>"]
5+
edition = "2021"
6+
description = "A BIP 340 implementation compatible with https://github.com/bitcoin/bips/blob/master/bip-0340.mediawiki."
7+
8+
[lib]
9+
path = "src/bip-340.rs"
10+
11+
[dependencies]
12+
hax-lib.workspace = true
13+
sha256 = { path = "../sha256" }
14+
num-bigint = "0.4"
15+
num-traits = "0.2"
16+
17+
[dev-dependencies]
18+
quickcheck = "1.0"
19+
serde = { version = "1.0", features = ["derive"] }
20+
serde_json = "1.0"
21+
hex = "0.4"
22+
23+
[package.metadata.hax]
24+
include = ["*"]

‎examples/bip-340/Makefile‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
.PHONY: default clean
2+
default:
3+
make -C proofs/fstar/extraction
4+
5+
clean:
6+
rm -f proofs/fstar/extraction/.depend
7+
rm -f proofs/fstar/extraction/*.fst

‎examples/bip-340/proofs/fstar/extraction/Makefile‎

Lines changed: 153 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,153 @@
1+
# This is a generically useful Makefile for F* that is self-contained
2+
#
3+
# It is tempting to factor this out into multiple Makefiles but that
4+
# makes it less portable, so resist temptation, or move to a more
5+
# sophisticated build system.
6+
#
7+
# We expect:
8+
# 1. `fstar.exe` to be in PATH (alternatively, you can also set
9+
# $FSTAR_HOME to be set to your F* repo/install directory)
10+
#
11+
# 2. `cargo`, `rustup`, `hax` and `jq` to be installed and in PATH.
12+
#
13+
# 3. the extracted Cargo crate to have "hax-lib" as a dependency:
14+
# `hax-lib = { version = "0.1.0-pre.1", git = "https://github.com/hacspec/hax"}`
15+
#
16+
# Optionally, you can set `HACL_HOME`.
17+
#
18+
# ROOTS contains all the top-level F* files you wish to verify
19+
# The default target `verify` verified ROOTS and its dependencies
20+
# To lax-check instead, set `OTHERFLAGS="--lax"` on the command-line
21+
#
22+
# To make F* emacs mode use the settings in this file, you need to
23+
# add the following lines to your .emacs
24+
#
25+
# (setq-default fstar-executable "<YOUR_FSTAR_HOME>/bin/fstar.exe")
26+
# (setq-default fstar-smt-executable "<YOUR_Z3_HOME>/bin/z3")
27+
#
28+
# (defun my-fstar-compute-prover-args-using-make ()
29+
# "Construct arguments to pass to F* by calling make."
30+
# (with-demoted-errors "Error when constructing arg string: %S"
31+
# (let* ((fname (file-name-nondirectory buffer-file-name))
32+
# (target (concat fname "-in"))
33+
# (argstr (car (process-lines "make" "--quiet" target))))
34+
# (split-string argstr))))
35+
# (setq fstar-subp-prover-args #'my-fstar-compute-prover-args-using-make)
36+
#
37+
38+
HACL_HOME ?= $(HOME)/.hax/hacl_home
39+
FSTAR_BIN ?= $(shell command -v fstar.exe 1>&2 2> /dev/null && echo "fstar.exe" || echo "$(FSTAR_HOME)/bin/fstar.exe")
40+
41+
CACHE_DIR ?= .cache
42+
HINT_DIR ?= .hints
43+
44+
SHELL ?= /usr/bin/env bash
45+
46+
EXECUTABLES = cargo cargo-hax jq
47+
K := $(foreach bin,$(EXECUTABLES),\
48+
$(if $(shell command -v $(bin) 2> /dev/null),,$(error "No $(bin) in PATH")))
49+
50+
.PHONY: all verify clean
51+
52+
all:
53+
rm -f .depend && $(MAKE) .depend
54+
$(MAKE) verify
55+
56+
HAX_CLI = "cargo hax into fstar --z3rlimit 100"
57+
58+
# If $HACL_HOME doesn't exist, clone it
59+
${HACL_HOME}:
60+
mkdir -p "${HACL_HOME}"
61+
git clone --depth 1 https://github.com/hacl-star/hacl-star.git "${HACL_HOME}"
62+
63+
# If no any F* file is detected, we run hax
64+
ifeq "$(wildcard *.fst *fsti)" ""
65+
$(shell $(SHELL) -c $(HAX_CLI))
66+
endif
67+
68+
# By default, we process all the files in the current directory
69+
ROOTS = $(wildcard *.fst *fsti)
70+
71+
# Regenerate F* files via hax when Rust sources change
72+
$(ROOTS): $(shell find ../../../src -type f -name '*.rs')
73+
$(shell $(SHELL) -c $(HAX_CLI))
74+
75+
# The following is a bash script that discovers F* libraries
76+
define FINDLIBS
77+
# Prints a path if and only if it exists. Takes one argument: the
78+
# path.
79+
function print_if_exists() {
80+
if [ -d "$$1" ]; then
81+
echo "$$1"
82+
fi
83+
}
84+
# Asks Cargo all the dependencies for the current crate or workspace,
85+
# and extract all "root" directories for each. Takes zero argument.
86+
function dependencies() {
87+
cargo metadata --format-version 1 |
88+
jq -r '.packages | .[] | .manifest_path | split("/") | .[:-1] | join("/")'
89+
}
90+
# Find hax libraries *around* a given path. Takes one argument: the
91+
# path.
92+
function find_hax_libraries_at_path() {
93+
path="$$1"
94+
# if there is a `proofs/fstar/extraction` subfolder, then that's a
95+
# F* library
96+
print_if_exists "$$path/proofs/fstar/extraction"
97+
# Maybe the `proof-libs` folder of hax is around?
98+
MAYBE_PROOF_LIBS=$$(realpath -q "$$path/../proof-libs/fstar")
99+
if [ $$? -eq 0 ]; then
100+
print_if_exists "$$MAYBE_PROOF_LIBS/core"
101+
print_if_exists "$$MAYBE_PROOF_LIBS/rust_primitives"
102+
fi
103+
}
104+
{ while IFS= read path; do
105+
find_hax_libraries_at_path "$$path"
106+
done < <(dependencies)
107+
} | sort -u
108+
endef
109+
export FINDLIBS
110+
111+
FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib $(shell bash -c "$$FINDLIBS")
112+
113+
FSTAR_FLAGS = --cmi \
114+
--warn_error -331 \
115+
--cache_checked_modules --cache_dir $(CACHE_DIR) \
116+
--already_cached "+Prims+FStar+LowStar+C+Spec.Loops+TestLib" \
117+
$(addprefix --include ,$(FSTAR_INCLUDE_DIRS))
118+
119+
FSTAR = $(FSTAR_BIN) $(FSTAR_FLAGS)
120+
121+
.depend: $(HINT_DIR) $(CACHE_DIR) $(ROOTS)
122+
$(info $(ROOTS))
123+
$(FSTAR) --cmi --dep full $(ROOTS) --extract '* -Prims -LowStar -FStar' > $@
124+
125+
include .depend
126+
127+
$(HINT_DIR):
128+
mkdir -p $@
129+
130+
$(CACHE_DIR):
131+
mkdir -p $@
132+
133+
$(CACHE_DIR)/%.checked: | .depend $(HINT_DIR) $(CACHE_DIR)
134+
$(FSTAR) $(OTHERFLAGS) $< $(ENABLE_HINTS) --hint_file $(HINT_DIR)/$(notdir $*).hints
135+
136+
verify: $(addsuffix .checked, $(addprefix $(CACHE_DIR)/,$(ROOTS)))
137+
138+
# Targets for interactive mode
139+
140+
%.fst-in:
141+
$(info $(FSTAR_FLAGS) \
142+
$(ENABLE_HINTS) --hint_file $(HINT_DIR)/$(basename $@).fst.hints)
143+
144+
%.fsti-in:
145+
$(info $(FSTAR_FLAGS) \
146+
$(ENABLE_HINTS) --hint_file $(HINT_DIR)/$(basename $@).fsti.hints)
147+
148+
149+
# Clean targets
150+
151+
clean:
152+
rm -rf $(CACHE_DIR)/*
153+
rm *.fst

0 commit comments

Comments
 (0)