From 469adebf7357927ddbaaa276329d6ee194d062f6 Mon Sep 17 00:00:00 2001 From: Franziskus Kiefer Date: Mon, 6 May 2024 18:32:53 +0200 Subject: [PATCH] Revert "Bounded integers" --- .envrc | 1 - Cargo.lock | 7 - Cargo.toml | 2 - .../lib/phases/phase_newtype_as_refinement.ml | 2 +- engine/names/src/lib.rs | 2 +- examples/Cargo.lock | 11 +- examples/Cargo.toml | 2 - .../barrett/proofs/fstar/extraction/Makefile | 101 ++----- examples/chacha20/Cargo.toml | 2 +- .../proofs/fstar/extraction/Chacha20.fst | 92 ++---- .../chacha20/proofs/fstar/extraction/Makefile | 109 ++------ examples/chacha20/src/lib.rs | 84 +----- examples/default.nix | 13 +- .../proofs/fstar/extraction/Makefile | 102 ++----- examples/limited-order-book/Cargo.toml | 1 - .../proofs/fstar/extraction/Makefile | 101 ++----- .../sha256/proofs/fstar/extraction/Makefile | 103 ++----- hax-bounded-integers/Cargo.toml | 12 - .../Hax_bounded_integers.Num_traits.fst | 250 ----------------- .../fstar/extraction/Hax_bounded_integers.fst | 40 --- hax-bounded-integers/src/lib.rs | 263 ------------------ hax-bounded-integers/src/num_traits.rs | 141 ---------- hax-lib-macros/src/lib.rs | 32 +-- hax-lib/proofs/fstar/extraction/Makefile | 102 ++----- hax-lib/src/lib.rs | 23 +- .../rust_primitives/Rust_primitives.Hax.fst | 17 -- tests/attributes/src/lib.rs | 2 +- 27 files changed, 221 insertions(+), 1396 deletions(-) delete mode 100644 .envrc delete mode 100644 hax-bounded-integers/Cargo.toml delete mode 100644 hax-bounded-integers/proofs/fstar/extraction/Hax_bounded_integers.Num_traits.fst delete mode 100644 hax-bounded-integers/proofs/fstar/extraction/Hax_bounded_integers.fst delete mode 100644 hax-bounded-integers/src/lib.rs delete mode 100644 hax-bounded-integers/src/num_traits.rs diff --git a/.envrc b/.envrc deleted file mode 100644 index 3550a30f2..000000000 --- a/.envrc +++ /dev/null @@ -1 +0,0 @@ -use flake diff --git a/Cargo.lock b/Cargo.lock index c902c6992..94a65f3e7 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -439,13 +439,6 @@ dependencies = [ "syn 1.0.109", ] -[[package]] -name = "hax-bounded-integers" -version = "0.1.0-pre.1" -dependencies = [ - "hax-lib", -] - [[package]] name = "hax-cli-options" version = "0.1.0-pre.1" diff --git a/Cargo.toml b/Cargo.toml index afa76a8e7..57ed25821 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -15,7 +15,6 @@ members = [ "hax-lib-macros/types", "hax-lib-protocol", "hax-lib-protocol-macros", - "hax-bounded-integers", "engine/names", "engine/names/extract", ] @@ -89,5 +88,4 @@ hax-lint = { path = "frontend/lint", version = "=0.1.0-pre.1" } hax-phase-debug-webapp = { path = "engine/utils/phase-debug-webapp", version = "=0.1.0-pre.1" } hax-lib-macros-types = { path = "hax-lib-macros/types", version = "=0.1.0-pre.1" } hax-lib-macros = { path = "hax-lib-macros", version = "=0.1.0-pre.1" } -hax-lib = { path = "hax-lib", version = "=0.1.0-pre.1" } hax-engine-names = { path = "engine/names", version = "=0.1.0-pre.1" } diff --git a/engine/lib/phases/phase_newtype_as_refinement.ml b/engine/lib/phases/phase_newtype_as_refinement.ml index a80e94a5c..6370ffb10 100644 --- a/engine/lib/phases/phase_newtype_as_refinement.ml +++ b/engine/lib/phases/phase_newtype_as_refinement.ml @@ -24,7 +24,7 @@ module Make (F : Features.T) = match e.e with | App { f = { e = GlobalVar f; _ }; args = [ inner ]; _ } when Ast.Global_ident.eq_name Hax_lib__Refinement__new f - || Ast.Global_ident.eq_name Hax_lib__RefineAs__into_checked f + || Ast.Global_ident.eq_name Hax_lib__RefineAs__refine f || Ast.Global_ident.eq_name Hax_lib__Refinement__get f -> { e with e = Ascription { typ = e.typ; e = inner } } | _ -> super#visit_expr () e diff --git a/engine/names/src/lib.rs b/engine/names/src/lib.rs index 862afb7e0..ebebe1528 100644 --- a/engine/names/src/lib.rs +++ b/engine/names/src/lib.rs @@ -52,7 +52,7 @@ fn dummy_hax_concrete_ident_wrapper>(x: I, mu fn refinements>(x: T, y: U) -> T { T::new(x.get()); - y.into_checked() + y.refine() } const _: () = { diff --git a/examples/Cargo.lock b/examples/Cargo.lock index c9088c7e5..08ecadb86 100644 --- a/examples/Cargo.lock +++ b/examples/Cargo.lock @@ -123,8 +123,8 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" name = "chacha20" version = "0.1.0" dependencies = [ - "hax-bounded-integers", "hax-lib", + "hax-lib-macros", ] [[package]] @@ -220,20 +220,11 @@ version = "0.14.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "f93e7192158dbcda357bdec5fb5788eebf8bbac027f3f33e719d29135ae84156" -[[package]] -name = "hax-bounded-integers" -version = "0.1.0-pre.1" -dependencies = [ - "hax-lib", -] - [[package]] name = "hax-lib" version = "0.1.0-pre.1" dependencies = [ "hax-lib-macros", - "num-bigint", - "num-traits", ] [[package]] diff --git a/examples/Cargo.toml b/examples/Cargo.toml index e4ff82da8..a202d5f0a 100644 --- a/examples/Cargo.toml +++ b/examples/Cargo.toml @@ -11,5 +11,3 @@ resolver = "2" [workspace.dependencies] hax-lib-macros = { path = "../hax-lib-macros" } hax-lib = { path = "../hax-lib" } -hax-bounded-integers = { path = "../hax-bounded-integers", version = "=0.1.0-pre.1" } - diff --git a/examples/barrett/proofs/fstar/extraction/Makefile b/examples/barrett/proofs/fstar/extraction/Makefile index aad27013b..f976e19da 100644 --- a/examples/barrett/proofs/fstar/extraction/Makefile +++ b/examples/barrett/proofs/fstar/extraction/Makefile @@ -4,21 +4,16 @@ # makes it less portable, so resist temptation, or move to a more # sophisticated build system. # -# We expect: -# 1. `fstar.exe` to be in PATH (alternatively, you can also set -# $FSTAR_HOME to be set to your F* repo/install directory) -# -# 2. `cargo`, `rustup`, `hax` and `jq` to be installed and in PATH. -# -# 3. the extracted Cargo crate to have "hax-lib" as a dependency: -# `hax-lib = { version = "0.1.0-pre.1", git = "https://github.com/hacspec/hax"}` -# -# Optionally, you can set `HACL_HOME`. +# We expect FSTAR_HOME to be set to your FSTAR repo/install directory +# We expect HACL_HOME to be set to your HACL* repo location +# We expect HAX_PROOF_LIBS to be set to the folder containing core, rust_primitives etc. +# We expect HAX_LIB to be set to the folder containing the crate `hax-lib`. # # ROOTS contains all the top-level F* files you wish to verify # The default target `verify` verified ROOTS and its dependencies # To lax-check instead, set `OTHERFLAGS="--lax"` on the command-line # +# # To make F* emacs mode use the settings in this file, you need to # add the following lines to your .emacs # @@ -35,17 +30,17 @@ # (setq fstar-subp-prover-args #'my-fstar-compute-prover-args-using-make) # -HACL_HOME ?= $(HOME)/.hax/hacl_home -FSTAR_BIN ?= $(shell command -v fstar.exe 1>&2 2> /dev/null && echo "fstar.exe" || echo "$(FSTAR_HOME)/bin/fstar.exe") +HAX_HOME ?= $(shell git rev-parse --show-toplevel) +FSTAR_HOME ?= $(HAX_HOME)/../../../FStar +HACL_HOME ?= $(HAX_HOME)/../../../hacl-star -CACHE_DIR ?= .cache -HINT_DIR ?= .hints +FSTAR_BIN ?= $(shell command -v fstar.exe 1>&2 2> /dev/null && echo "fstar.exe" || echo "$(FSTAR_HOME)/bin/fstar.exe") -SHELL ?= /usr/bin/env bash +HAX_PROOF_LIBS_HOME ?= $(HAX_HOME)/proof-libs/fstar +HAX_LIBS_HOME ?= $(HAX_HOME)/hax-lib/proofs/fstar/extraction -EXECUTABLES = cargo cargo-hax jq -K := $(foreach bin,$(EXECUTABLES),\ - $(if $(shell command -v $(bin) 2> /dev/null),,$(error "No $(bin) in PATH"))) +CACHE_DIR ?= $(HAX_PROOF_LIBS)/.cache +HINT_DIR ?= $(HAX_PROOF_LIBS)/.hints .PHONY: all verify clean @@ -53,62 +48,17 @@ all: rm -f .depend && $(MAKE) .depend $(MAKE) verify -HAX_CLI = "cargo hax into fstar --z3rlimit 500" - -# If $HACL_HOME doesn't exist, clone it -${HACL_HOME}: - mkdir -p "${HACL_HOME}" - git clone --depth 1 https://github.com/hacl-star/hacl-star.git "${HACL_HOME}" - -# If no any F* file is detected, we run hax -ifeq "$(wildcard *.fst *fsti)" "" -$(shell $(SHELL) -c $(HAX_CLI)) -endif - -# By default, we process all the files in the current directory -ROOTS = $(wildcard *.fst *fsti) - -# Regenerate F* files via hax when Rust sources change -$(ROOTS): $(shell find ../../../src -type f -name '*.rs') - $(shell $(SHELL) -c $(HAX_CLI)) - -# The following is a bash script that discovers F* libraries -define FINDLIBS - # Prints a path if and only if it exists. Takes one argument: the - # path. - function print_if_exists() { - if [ -d "$$1" ]; then - echo "$$1" - fi - } - # Asks Cargo all the dependencies for the current crate or workspace, - # and extract all "root" directories for each. Takes zero argument. - function dependencies() { - cargo metadata --format-version 1 | - jq -r '.packages | .[] | .manifest_path | split("/") | .[:-1] | join("/")' - } - # Find hax libraries *around* a given path. Takes one argument: the - # path. - function find_hax_libraries_at_path() { - path="$$1" - # if there is a `proofs/fstar/extraction` subfolder, then that's a - # F* library - print_if_exists "$$path/proofs/fstar/extraction" - # Maybe the `proof-libs` folder of hax is around? - MAYBE_PROOF_LIBS=$$(realpath -q "$$path/../proof-libs/fstar") - if [ $$? -eq 0 ]; then - print_if_exists "$$MAYBE_PROOF_LIBS/core" - print_if_exists "$$MAYBE_PROOF_LIBS/rust_primitives" - fi - } - { while IFS= read path; do - find_hax_libraries_at_path "$$path" - done < <(dependencies) - } | sort -u -endef -export FINDLIBS - -FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib $(shell bash -c "$$FINDLIBS") +# By default, we process all the files in the current directory. Here, we +# *extend* the set of relevant files with the tests. +ROOTS = Barrett.fst + +$(ROOTS): ../../../src/lib.rs + cargo hax into fstar --z3rlimit 500 + +FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib \ + $(HAX_PROOF_LIBS_HOME)/rust_primitives $(HAX_PROOF_LIBS_HOME)/core \ + $(HAX_PROOF_LIBS_HOME)/hax_lib \ + $(HAX_LIBS_HOME) FSTAR_FLAGS = --cmi \ --warn_error -331 \ @@ -118,6 +68,7 @@ FSTAR_FLAGS = --cmi \ FSTAR = $(FSTAR_BIN) $(FSTAR_FLAGS) + .depend: $(HINT_DIR) $(CACHE_DIR) $(ROOTS) $(info $(ROOTS)) $(FSTAR) --cmi --dep full $(ROOTS) --extract '* -Prims -LowStar -FStar' > $@ @@ -148,6 +99,8 @@ verify: $(addsuffix .checked, $(addprefix $(CACHE_DIR)/,$(ROOTS))) # Clean targets +SHELL ?= /usr/bin/env bash + clean: rm -rf $(CACHE_DIR)/* rm *.fst diff --git a/examples/chacha20/Cargo.toml b/examples/chacha20/Cargo.toml index c8429b87f..1e93cc616 100644 --- a/examples/chacha20/Cargo.toml +++ b/examples/chacha20/Cargo.toml @@ -5,5 +5,5 @@ authors = ["Franziskus Kiefer "] edition = "2021" [dependencies] +hax-lib-macros.workspace = true hax-lib.workspace = true -hax-bounded-integers.workspace = true diff --git a/examples/chacha20/proofs/fstar/extraction/Chacha20.fst b/examples/chacha20/proofs/fstar/extraction/Chacha20.fst index 8740a682a..e224815d4 100644 --- a/examples/chacha20/proofs/fstar/extraction/Chacha20.fst +++ b/examples/chacha20/proofs/fstar/extraction/Chacha20.fst @@ -15,94 +15,46 @@ let t_ChaChaKey = t_Array u8 (sz 32) unfold let t_State = t_Array u32 (sz 16) -unfold -let t_StateIdx = Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15) - -let chacha20_line - (a b d: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (s: u32) - (m: t_Array u32 (sz 16)) - : t_Array u32 (sz 16) = +let chacha20_line (a b d: usize) (s: u32) (m: t_Array u32 (sz 16)) + : Prims.Pure (t_Array u32 (sz 16)) + (requires a <. sz 16 && b <. sz 16 && d <. sz 16) + (fun (res:t_Array u32 (sz 16)) -> True ) = let state:t_Array u32 (sz 16) = m in let state:t_Array u32 (sz 16) = - Rust_primitives.Hax.update_at state + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize state a (Core.Num.impl__u32__wrapping_add (state.[ a ] <: u32) (state.[ b ] <: u32) <: u32) in let state:t_Array u32 (sz 16) = - Rust_primitives.Hax.update_at state d ((state.[ d ] <: u32) ^. (state.[ a ] <: u32) <: u32) + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize state + d + ((state.[ d ] <: u32) ^. (state.[ a ] <: u32) <: u32) in let state:t_Array u32 (sz 16) = - Rust_primitives.Hax.update_at state + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize state d (Core.Num.impl__u32__rotate_left (state.[ d ] <: u32) s <: u32) in state -let chacha20_quarter_round - (a b c d: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (state: t_Array u32 (sz 16)) - : t_Array u32 (sz 16) = +let chacha20_quarter_round (a b c d: usize) (state: t_Array u32 (sz 16)) + : Prims.Pure (t_Array u32 (sz 16)) + (requires a <. sz 16 && b <. sz 16 && c <. sz 16 && d <. sz 16) + (fun _ -> Prims.l_True) = let state:t_Array u32 (sz 16) = chacha20_line a b d 16ul state in let state:t_Array u32 (sz 16) = chacha20_line c d b 12ul state in let state:t_Array u32 (sz 16) = chacha20_line a b d 8ul state in chacha20_line c d b 7ul state let chacha20_double_round (state: t_Array u32 (sz 16)) : t_Array u32 (sz 16) = - let state:t_Array u32 (sz 16) = - chacha20_quarter_round (sz 0 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 4 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 8 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 12 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - state - in - let state:t_Array u32 (sz 16) = - chacha20_quarter_round (sz 1 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 5 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 9 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 13 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - state - in - let state:t_Array u32 (sz 16) = - chacha20_quarter_round (sz 2 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 6 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 10 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 14 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - state - in - let state:t_Array u32 (sz 16) = - chacha20_quarter_round (sz 3 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 7 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 11 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 15 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - state - in - let state:t_Array u32 (sz 16) = - chacha20_quarter_round (sz 0 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 5 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 10 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 15 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - state - in - let state:t_Array u32 (sz 16) = - chacha20_quarter_round (sz 1 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 6 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 11 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 12 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - state - in - let state:t_Array u32 (sz 16) = - chacha20_quarter_round (sz 2 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 7 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 8 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 13 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - state - in - chacha20_quarter_round (sz 3 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 4 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 9 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - (sz 14 <: Hax_bounded_integers.t_BoundedUsize (sz 0) (sz 15)) - state + let state:t_Array u32 (sz 16) = chacha20_quarter_round (sz 0) (sz 4) (sz 8) (sz 12) state in + let state:t_Array u32 (sz 16) = chacha20_quarter_round (sz 1) (sz 5) (sz 9) (sz 13) state in + let state:t_Array u32 (sz 16) = chacha20_quarter_round (sz 2) (sz 6) (sz 10) (sz 14) state in + let state:t_Array u32 (sz 16) = chacha20_quarter_round (sz 3) (sz 7) (sz 11) (sz 15) state in + let state:t_Array u32 (sz 16) = chacha20_quarter_round (sz 0) (sz 5) (sz 10) (sz 15) state in + let state:t_Array u32 (sz 16) = chacha20_quarter_round (sz 1) (sz 6) (sz 11) (sz 12) state in + let state:t_Array u32 (sz 16) = chacha20_quarter_round (sz 2) (sz 7) (sz 8) (sz 13) state in + chacha20_quarter_round (sz 3) (sz 4) (sz 9) (sz 14) state let chacha20_rounds (state: t_Array u32 (sz 16)) : t_Array u32 (sz 16) = let st:t_Array u32 (sz 16) = state in @@ -174,7 +126,7 @@ let chacha20_init (key: t_Array u8 (sz 32)) (iv: t_Array u8 (sz 12)) (ctr: u32) ] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 16); - Rust_primitives.Hax.array_of_list 16 list + Rust_primitives.Hax.array_of_list list let chacha20_key_block (state: t_Array u32 (sz 16)) : t_Array u8 (sz 64) = let state:t_Array u32 (sz 16) = chacha20_core 0ul state in diff --git a/examples/chacha20/proofs/fstar/extraction/Makefile b/examples/chacha20/proofs/fstar/extraction/Makefile index 381ef237b..ef8f09c02 100644 --- a/examples/chacha20/proofs/fstar/extraction/Makefile +++ b/examples/chacha20/proofs/fstar/extraction/Makefile @@ -4,21 +4,16 @@ # makes it less portable, so resist temptation, or move to a more # sophisticated build system. # -# We expect: -# 1. `fstar.exe` to be in PATH (alternatively, you can also set -# $FSTAR_HOME to be set to your F* repo/install directory) -# -# 2. `cargo`, `rustup`, `hax` and `jq` to be installed and in PATH. -# -# 3. the extracted Cargo crate to have "hax-lib" as a dependency: -# `hax-lib = { version = "0.1.0-pre.1", git = "https://github.com/hacspec/hax"}` -# -# Optionally, you can set `HACL_HOME`. +# We expect FSTAR_HOME to be set to your FSTAR repo/install directory +# We expect HACL_HOME to be set to your HACL* repo location +# We expect HAX_PROOF_LIBS_HOME to be set to the folder containing core, rust_primitives etc. +# We expect HAX_LIBS_HOME to be set to the folder containing the crate `hax-lib`. # # ROOTS contains all the top-level F* files you wish to verify # The default target `verify` verified ROOTS and its dependencies # To lax-check instead, set `OTHERFLAGS="--lax"` on the command-line # +# # To make F* emacs mode use the settings in this file, you need to # add the following lines to your .emacs # @@ -35,17 +30,17 @@ # (setq fstar-subp-prover-args #'my-fstar-compute-prover-args-using-make) # -HACL_HOME ?= $(HOME)/.hax/hacl_home -FSTAR_BIN ?= $(shell command -v fstar.exe 1>&2 2> /dev/null && echo "fstar.exe" || echo "$(FSTAR_HOME)/bin/fstar.exe") +HAX_HOME ?= $(shell git rev-parse --show-toplevel) +FSTAR_HOME ?= $(HAX_HOME)/../../../FStar +HACL_HOME ?= $(HAX_HOME)/../../../hacl-star -CACHE_DIR ?= .cache -HINT_DIR ?= .hints +FSTAR_BIN ?= $(shell command -v fstar.exe 1>&2 2> /dev/null && echo "fstar.exe" || echo "$(FSTAR_HOME)/bin/fstar.exe") -SHELL ?= /usr/bin/env bash +HAX_PROOF_LIBS_HOME ?= $(HAX_HOME)/proof-libs/fstar +HAX_LIBS_HOME ?= $(HAX_HOME)/hax-lib/proofs/fstar/extraction -EXECUTABLES = cargo cargo-hax jq -K := $(foreach bin,$(EXECUTABLES),\ - $(if $(shell command -v $(bin) 2> /dev/null),,$(error "No $(bin) in PATH"))) +CACHE_DIR ?= $(HAX_PROOF_LIBS_HOME)/.cache +HINT_DIR ?= $(HAX_PROOF_LIBS_HOME)/.hints .PHONY: all verify clean @@ -53,63 +48,17 @@ all: rm -f .depend && $(MAKE) .depend $(MAKE) verify -# Default hax invocation -HAX_CLI = "cargo hax into fstar" - -# If $HACL_HOME doesn't exist, clone it -${HACL_HOME}: - mkdir -p "${HACL_HOME}" - git clone --depth 1 https://github.com/hacl-star/hacl-star.git "${HACL_HOME}" - -# If no any F* file is detected, we run hax -ifeq "$(wildcard *.fst *fsti)" "" -$(shell $(SHELL) -c $(HAX_CLI)) -endif - -# By default, we process all the files in the current directory -ROOTS = $(wildcard *.fst *fsti) - -# Regenerate F* files via hax when Rust sources change -$(ROOTS): $(shell find ../../../src -type f -name '*.rs') - $(shell $(SHELL) -c $(HAX_CLI)) - -# The following is a bash script that discovers F* libraries -define FINDLIBS - # Prints a path if and only if it exists. Takes one argument: the - # path. - function print_if_exists() { - if [ -d "$$1" ]; then - echo "$$1" - fi - } - # Asks Cargo all the dependencies for the current crate or workspace, - # and extract all "root" directories for each. Takes zero argument. - function dependencies() { - cargo metadata --format-version 1 | - jq -r '.packages | .[] | .manifest_path | split("/") | .[:-1] | join("/")' - } - # Find hax libraries *around* a given path. Takes one argument: the - # path. - function find_hax_libraries_at_path() { - path="$$1" - # if there is a `proofs/fstar/extraction` subfolder, then that's a - # F* library - print_if_exists "$$path/proofs/fstar/extraction" - # Maybe the `proof-libs` folder of hax is around? - MAYBE_PROOF_LIBS=$$(realpath -q "$$path/../proof-libs/fstar") - if [ $$? -eq 0 ]; then - print_if_exists "$$MAYBE_PROOF_LIBS/core" - print_if_exists "$$MAYBE_PROOF_LIBS/rust_primitives" - fi - } - { while IFS= read path; do - find_hax_libraries_at_path "$$path" - done < <(dependencies) - } | sort -u -endef -export FINDLIBS - -FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib $(shell bash -c "$$FINDLIBS") +# By default, we process all the files in the current directory. Here, we +# *extend* the set of relevant files with the tests. +ROOTS = Chacha20.fst Chacha20.Hacspec_helper.fst + +$(ROOTS): ../../../src/lib.rs ../../../src/hacspec_helper.rs + cargo hax into fstar + +FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib \ + $(HAX_PROOF_LIBS_HOME)/rust_primitives $(HAX_PROOF_LIBS_HOME)/core \ + $(HAX_PROOF_LIBS_HOME)/hax_lib \ + $(HAX_LIBS_HOME) FSTAR_FLAGS = --cmi \ --warn_error -331 \ @@ -119,6 +68,7 @@ FSTAR_FLAGS = --cmi \ FSTAR = $(FSTAR_BIN) $(FSTAR_FLAGS) + .depend: $(HINT_DIR) $(CACHE_DIR) $(ROOTS) $(info $(ROOTS)) $(FSTAR) --cmi --dep full $(ROOTS) --extract '* -Prims -LowStar -FStar' > $@ @@ -131,6 +81,9 @@ $(HINT_DIR): $(CACHE_DIR): mkdir -p $@ +$(CACHE_DIR)/Chacha20.Hacspec_helper.fst.checked: | .depend $(HINT_DIR) $(CACHE_DIR) + $(FSTAR) --lax $(OTHERFLAGS) $< $(ENABLE_HINTS) --hint_file $(HINT_DIR)/$(notdir $*).hints + $(CACHE_DIR)/%.checked: | .depend $(HINT_DIR) $(CACHE_DIR) $(FSTAR) $(OTHERFLAGS) $< $(ENABLE_HINTS) --hint_file $(HINT_DIR)/$(notdir $*).hints @@ -149,10 +102,8 @@ verify: $(addsuffix .checked, $(addprefix $(CACHE_DIR)/,$(ROOTS))) # Clean targets +SHELL ?= /usr/bin/env bash + clean: rm -rf $(CACHE_DIR)/* rm *.fst - -# Special rule for `Chacha20.Hacspec_helper` -$(CACHE_DIR)/Chacha20.Hacspec_helper.fst.checked: | .depend $(HINT_DIR) $(CACHE_DIR) - $(FSTAR) --lax $(OTHERFLAGS) $< $(ENABLE_HINTS) --hint_file $(HINT_DIR)/$(notdir $*).hints diff --git a/examples/chacha20/src/lib.rs b/examples/chacha20/src/lib.rs index adcaafae5..2765e2454 100644 --- a/examples/chacha20/src/lib.rs +++ b/examples/chacha20/src/lib.rs @@ -1,16 +1,15 @@ mod hacspec_helper; use hacspec_helper::*; -use hax_lib as hax; +use hax_lib_macros as hax; type State = [u32; 16]; type Block = [u8; 64]; type ChaChaIV = [u8; 12]; type ChaChaKey = [u8; 32]; -type StateIdx = hax_bounded_integers::BoundedUsize<0, 15>; - -fn chacha20_line(a: StateIdx, b: StateIdx, d: StateIdx, s: u32, m: State) -> State { +#[hax::requires(a < 16 && b < 16 && d < 16)] +fn chacha20_line(a: usize, b: usize, d: usize, s: u32, m: State) -> State { let mut state = m; state[a] = state[a].wrapping_add(state[b]); state[d] = state[d] ^ state[a]; @@ -18,79 +17,24 @@ fn chacha20_line(a: StateIdx, b: StateIdx, d: StateIdx, s: u32, m: State) -> Sta state } -pub fn chacha20_quarter_round( - a: StateIdx, - b: StateIdx, - c: StateIdx, - d: StateIdx, - state: State, -) -> State { +#[hax::requires(a < 16 && b < 16 && c < 16 && d < 16)] +pub fn chacha20_quarter_round(a: usize, b: usize, c: usize, d: usize, state: State) -> State { let state = chacha20_line(a, b, d, 16, state); let state = chacha20_line(c, d, b, 12, state); let state = chacha20_line(a, b, d, 8, state); chacha20_line(c, d, b, 7, state) } -use hax_lib::*; - fn chacha20_double_round(state: State) -> State { - let state = chacha20_quarter_round( - 0.into_checked(), - 4.into_checked(), - 8.into_checked(), - 12.into_checked(), - state, - ); - let state = chacha20_quarter_round( - 1.into_checked(), - 5.into_checked(), - 9.into_checked(), - 13.into_checked(), - state, - ); - let state = chacha20_quarter_round( - 2.into_checked(), - 6.into_checked(), - 10.into_checked(), - 14.into_checked(), - state, - ); - let state = chacha20_quarter_round( - 3.into_checked(), - 7.into_checked(), - 11.into_checked(), - 15.into_checked(), - state, - ); - - let state = chacha20_quarter_round( - 0.into_checked(), - 5.into_checked(), - 10.into_checked(), - 15.into_checked(), - state, - ); - let state = chacha20_quarter_round( - 1.into_checked(), - 6.into_checked(), - 11.into_checked(), - 12.into_checked(), - state, - ); - let state = chacha20_quarter_round( - 2.into_checked(), - 7.into_checked(), - 8.into_checked(), - 13.into_checked(), - state, - ); - chacha20_quarter_round( - 3.into_checked(), - 4.into_checked(), - 9.into_checked(), - 14.into_checked(), - state, - ) + let state = chacha20_quarter_round(0, 4, 8, 12, state); + let state = chacha20_quarter_round(1, 5, 9, 13, state); + let state = chacha20_quarter_round(2, 6, 10, 14, state); + let state = chacha20_quarter_round(3, 7, 11, 15, state); + + let state = chacha20_quarter_round(0, 5, 10, 15, state); + let state = chacha20_quarter_round(1, 6, 11, 12, state); + let state = chacha20_quarter_round(2, 7, 8, 13, state); + chacha20_quarter_round(3, 4, 9, 14, state) } pub fn chacha20_rounds(state: State) -> State { diff --git a/examples/default.nix b/examples/default.nix index 74aba3dcd..42759e00e 100644 --- a/examples/default.nix +++ b/examples/default.nix @@ -6,19 +6,16 @@ fstar, hacl-star, hax-env, - jq, }: let - matches = re: path: !builtins.isNull (builtins.match re path); commonArgs = { version = "0.0.1"; src = lib.cleanSourceWith { src = craneLib.path ./..; filter = path: type: - # We include only certain files. FStar files under the example - # directory are listed out. - ( matches ".*(Makefile|.*[.](rs|toml|lock|diff|fsti?))$" path - && !matches ".*examples/.*[.]fsti?$" path - ) || ("directory" == type); + # We include only certain files, notably we exclude generated + # files (`.fst`, `.v`, etc.) + !builtins.isNull (builtins.match ".*(Makefile|.*[.](rs|toml|lock|diff))$" path) + || ("directory" == type); }; doCheck = false; cargoVendorDir = craneLib.vendorMultipleCargoDeps { @@ -46,5 +43,5 @@ in sed -i "s/make -C limited-order-book/HAX_VANILLA_RUSTC=never make -C limited-order-book/g" Makefile make ''; - buildInputs = [hax hax-env fstar jq]; + buildInputs = [hax hax-env fstar]; }) diff --git a/examples/kyber_compress/proofs/fstar/extraction/Makefile b/examples/kyber_compress/proofs/fstar/extraction/Makefile index a48b5139d..2cfa01554 100644 --- a/examples/kyber_compress/proofs/fstar/extraction/Makefile +++ b/examples/kyber_compress/proofs/fstar/extraction/Makefile @@ -4,21 +4,16 @@ # makes it less portable, so resist temptation, or move to a more # sophisticated build system. # -# We expect: -# 1. `fstar.exe` to be in PATH (alternatively, you can also set -# $FSTAR_HOME to be set to your F* repo/install directory) -# -# 2. `cargo`, `rustup`, `hax` and `jq` to be installed and in PATH. -# -# 3. the extracted Cargo crate to have "hax-lib" as a dependency: -# `hax-lib = { version = "0.1.0-pre.1", git = "https://github.com/hacspec/hax"}` -# -# Optionally, you can set `HACL_HOME`. +# We expect FSTAR_HOME to be set to your FSTAR repo/install directory +# We expect HACL_HOME to be set to your HACL* repo location +# We expect HAX_PROOF_LIBS to be set to the folder containing core, rust_primitives etc. +# We expect HAX_LIB to be set to the folder containing the crate `hax-lib`. # # ROOTS contains all the top-level F* files you wish to verify # The default target `verify` verified ROOTS and its dependencies # To lax-check instead, set `OTHERFLAGS="--lax"` on the command-line # +# # To make F* emacs mode use the settings in this file, you need to # add the following lines to your .emacs # @@ -35,17 +30,18 @@ # (setq fstar-subp-prover-args #'my-fstar-compute-prover-args-using-make) # -HACL_HOME ?= $(HOME)/.hax/hacl_home -FSTAR_BIN ?= $(shell command -v fstar.exe 1>&2 2> /dev/null && echo "fstar.exe" || echo "$(FSTAR_HOME)/bin/fstar.exe") +HAX_HOME ?= $(shell git rev-parse --show-toplevel) +FSTAR_HOME ?= $(HAX_HOME)/../../../FStar +HACL_HOME ?= $(HAX_HOME)/../../../hacl-star -CACHE_DIR ?= .cache -HINT_DIR ?= .hints +FSTAR_BIN ?= $(shell command -v fstar.exe 1>&2 2> /dev/null && echo "fstar.exe" || echo "$(FSTAR_HOME)/bin/fstar.exe") -SHELL ?= /usr/bin/env bash -EXECUTABLES = cargo cargo-hax jq -K := $(foreach bin,$(EXECUTABLES),\ - $(if $(shell command -v $(bin) 2> /dev/null),,$(error "No $(bin) in PATH"))) +HAX_PROOF_LIBS_HOME ?= $(HAX_HOME)/proof-libs/fstar +HAX_LIBS_HOME ?= $(HAX_HOME)/hax-lib/proofs/fstar/extraction + +CACHE_DIR ?= $(HAX_PROOF_LIBS_HOME)/.cache +HINT_DIR ?= $(HAX_PROOF_LIBS_HOME)/.hints .PHONY: all verify clean @@ -53,62 +49,17 @@ all: rm -f .depend && $(MAKE) .depend $(MAKE) verify -HAX_CLI = "cargo hax into fstar --z3rlimit 200" - -# If $HACL_HOME doesn't exist, clone it -${HACL_HOME}: - mkdir -p "${HACL_HOME}" - git clone --depth 1 https://github.com/hacl-star/hacl-star.git "${HACL_HOME}" - -# If no any F* file is detected, we run hax -ifeq "$(wildcard *.fst *fsti)" "" -$(shell $(SHELL) -c $(HAX_CLI)) -endif - -# By default, we process all the files in the current directory -ROOTS = $(wildcard *.fst *fsti) - -# Regenerate F* files via hax when Rust sources change -$(ROOTS): $(shell find ../../../src -type f -name '*.rs') - $(shell $(SHELL) -c $(HAX_CLI)) - -# The following is a bash script that discovers F* libraries -define FINDLIBS - # Prints a path if and only if it exists. Takes one argument: the - # path. - function print_if_exists() { - if [ -d "$$1" ]; then - echo "$$1" - fi - } - # Asks Cargo all the dependencies for the current crate or workspace, - # and extract all "root" directories for each. Takes zero argument. - function dependencies() { - cargo metadata --format-version 1 | - jq -r '.packages | .[] | .manifest_path | split("/") | .[:-1] | join("/")' - } - # Find hax libraries *around* a given path. Takes one argument: the - # path. - function find_hax_libraries_at_path() { - path="$$1" - # if there is a `proofs/fstar/extraction` subfolder, then that's a - # F* library - print_if_exists "$$path/proofs/fstar/extraction" - # Maybe the `proof-libs` folder of hax is around? - MAYBE_PROOF_LIBS=$$(realpath -q "$$path/../proof-libs/fstar") - if [ $$? -eq 0 ]; then - print_if_exists "$$MAYBE_PROOF_LIBS/core" - print_if_exists "$$MAYBE_PROOF_LIBS/rust_primitives" - fi - } - { while IFS= read path; do - find_hax_libraries_at_path "$$path" - done < <(dependencies) - } | sort -u -endef -export FINDLIBS - -FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib $(shell bash -c "$$FINDLIBS") +# By default, we process all the files in the current directory. Here, we +# *extend* the set of relevant files with the tests. +ROOTS = Kyber_compress.fst + +$(ROOTS): ../../../src/lib.rs + cargo hax into fstar --z3rlimit 200 + +FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib \ + $(HAX_PROOF_LIBS_HOME)/rust_primitives $(HAX_PROOF_LIBS_HOME)/core \ + $(HAX_PROOF_LIBS_HOME)/hax_lib \ + $(HAX_LIBS_HOME) FSTAR_FLAGS = --cmi \ --warn_error -331 \ @@ -118,6 +69,7 @@ FSTAR_FLAGS = --cmi \ FSTAR = $(FSTAR_BIN) $(FSTAR_FLAGS) + .depend: $(HINT_DIR) $(CACHE_DIR) $(ROOTS) $(info $(ROOTS)) $(FSTAR) --cmi --dep full $(ROOTS) --extract '* -Prims -LowStar -FStar' > $@ @@ -148,6 +100,8 @@ verify: $(addsuffix .checked, $(addprefix $(CACHE_DIR)/,$(ROOTS))) # Clean targets +SHELL ?= /usr/bin/env bash + clean: rm -rf $(CACHE_DIR)/* rm *.fst diff --git a/examples/limited-order-book/Cargo.toml b/examples/limited-order-book/Cargo.toml index a7410d98e..9f437b1ec 100644 --- a/examples/limited-order-book/Cargo.toml +++ b/examples/limited-order-book/Cargo.toml @@ -12,5 +12,4 @@ crate-type = ["cdylib", "lib"] candid = "0.9.6" ic-cdk = "0.10.0" ic-cdk-macros = "0.8.1" -hax-lib.workspace = true serde = { version = "1.0" } diff --git a/examples/limited-order-book/proofs/fstar/extraction/Makefile b/examples/limited-order-book/proofs/fstar/extraction/Makefile index 0183a6dd6..e83a9affc 100644 --- a/examples/limited-order-book/proofs/fstar/extraction/Makefile +++ b/examples/limited-order-book/proofs/fstar/extraction/Makefile @@ -4,21 +4,16 @@ # makes it less portable, so resist temptation, or move to a more # sophisticated build system. # -# We expect: -# 1. `fstar.exe` to be in PATH (alternatively, you can also set -# $FSTAR_HOME to be set to your F* repo/install directory) -# -# 2. `cargo`, `rustup`, `hax` and `jq` to be installed and in PATH. -# -# 3. the extracted Cargo crate to have "hax-lib" as a dependency: -# `hax-lib = { version = "0.1.0-pre.1", git = "https://github.com/hacspec/hax"}` -# -# Optionally, you can set `HACL_HOME`. +# We expect FSTAR_HOME to be set to your FSTAR repo/install directory +# We expect HACL_HOME to be set to your HACL* repo location +# We expect HAX_PROOF_LIBS_HOME to be set to the folder containing core, rust_primitives etc. +# We expect HAX_LIBS_HOME to be set to the folder containing the crate `hax-lib`. # # ROOTS contains all the top-level F* files you wish to verify # The default target `verify` verified ROOTS and its dependencies # To lax-check instead, set `OTHERFLAGS="--lax"` on the command-line # +# # To make F* emacs mode use the settings in this file, you need to # add the following lines to your .emacs # @@ -35,17 +30,17 @@ # (setq fstar-subp-prover-args #'my-fstar-compute-prover-args-using-make) # -HACL_HOME ?= $(HOME)/.hax/hacl_home -FSTAR_BIN ?= $(shell command -v fstar.exe 1>&2 2> /dev/null && echo "fstar.exe" || echo "$(FSTAR_HOME)/bin/fstar.exe") +HAX_HOME ?= $(shell git rev-parse --show-toplevel) +FSTAR_HOME ?= $(HAX_HOME)/../../../FStar +HACL_HOME ?= $(HAX_HOME)/../../../hacl-star -CACHE_DIR ?= .cache -HINT_DIR ?= .hints +FSTAR_BIN ?= $(shell command -v fstar.exe 1>&2 2> /dev/null && echo "fstar.exe" || echo "$(FSTAR_HOME)/bin/fstar.exe") -SHELL ?= /usr/bin/env bash +HAX_PROOF_LIBS_HOME ?= $(HAX_HOME)/proof-libs/fstar +HAX_LIBS_HOME ?= $(HAX_HOME)/hax-lib/proofs/fstar/extraction -EXECUTABLES = cargo cargo-hax jq -K := $(foreach bin,$(EXECUTABLES),\ - $(if $(shell command -v $(bin) 2> /dev/null),,$(error "No $(bin) in PATH"))) +CACHE_DIR ?= $(HAX_PROOF_LIBS_HOME)/.cache +HINT_DIR ?= $(HAX_PROOF_LIBS_HOME)/.hints .PHONY: all verify clean @@ -53,62 +48,17 @@ all: rm -f .depend && $(MAKE) .depend $(MAKE) verify -HAX_CLI = "cargo hax into -i '-** +**::process_order' fstar" - -# If $HACL_HOME doesn't exist, clone it -${HACL_HOME}: - mkdir -p "${HACL_HOME}" - git clone --depth 1 https://github.com/hacl-star/hacl-star.git "${HACL_HOME}" - -# If no any F* file is detected, we run hax -ifeq "$(wildcard *.fst *fsti)" "" -$(shell $(SHELL) -c $(HAX_CLI)) -endif - -# By default, we process all the files in the current directory -ROOTS = $(wildcard *.fst *fsti) - -# Regenerate F* files via hax when Rust sources change -$(ROOTS): $(shell find ../../../src -type f -name '*.rs') - $(shell $(SHELL) -c $(HAX_CLI)) - -# The following is a bash script that discovers F* libraries -define FINDLIBS - # Prints a path if and only if it exists. Takes one argument: the - # path. - function print_if_exists() { - if [ -d "$$1" ]; then - echo "$$1" - fi - } - # Asks Cargo all the dependencies for the current crate or workspace, - # and extract all "root" directories for each. Takes zero argument. - function dependencies() { - cargo metadata --format-version 1 | - jq -r '.packages | .[] | .manifest_path | split("/") | .[:-1] | join("/")' - } - # Find hax libraries *around* a given path. Takes one argument: the - # path. - function find_hax_libraries_at_path() { - path="$$1" - # if there is a `proofs/fstar/extraction` subfolder, then that's a - # F* library - print_if_exists "$$path/proofs/fstar/extraction" - # Maybe the `proof-libs` folder of hax is around? - MAYBE_PROOF_LIBS=$$(realpath -q "$$path/../proof-libs/fstar") - if [ $$? -eq 0 ]; then - print_if_exists "$$MAYBE_PROOF_LIBS/core" - print_if_exists "$$MAYBE_PROOF_LIBS/rust_primitives" - fi - } - { while IFS= read path; do - find_hax_libraries_at_path "$$path" - done < <(dependencies) - } | sort -u -endef -export FINDLIBS - -FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib $(shell bash -c "$$FINDLIBS") +# By default, we process all the files in the current directory. Here, we +# *extend* the set of relevant files with the tests. +ROOTS = Lob_backend.fst + +$(ROOTS): ../../../src/canister.rs ../../../src/lib.rs + cargo hax into -i '-** +**::process_order' fstar + +FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib \ + $(HAX_PROOF_LIBS_HOME)/rust_primitives $(HAX_PROOF_LIBS_HOME)/core \ + $(HAX_PROOF_LIBS_HOME)/hax_lib \ + $(HAX_LIBS_HOME) FSTAR_FLAGS = --cmi \ --warn_error -331 \ @@ -118,6 +68,7 @@ FSTAR_FLAGS = --cmi \ FSTAR = $(FSTAR_BIN) $(FSTAR_FLAGS) + .depend: $(HINT_DIR) $(CACHE_DIR) $(ROOTS) $(info $(ROOTS)) $(FSTAR) --cmi --dep full $(ROOTS) --extract '* -Prims -LowStar -FStar' > $@ @@ -148,6 +99,8 @@ verify: $(addsuffix .checked, $(addprefix $(CACHE_DIR)/,$(ROOTS))) # Clean targets +SHELL ?= /usr/bin/env bash + clean: rm -rf $(CACHE_DIR)/* rm *.fst diff --git a/examples/sha256/proofs/fstar/extraction/Makefile b/examples/sha256/proofs/fstar/extraction/Makefile index df5df7a06..f51e75f8e 100644 --- a/examples/sha256/proofs/fstar/extraction/Makefile +++ b/examples/sha256/proofs/fstar/extraction/Makefile @@ -4,21 +4,16 @@ # makes it less portable, so resist temptation, or move to a more # sophisticated build system. # -# We expect: -# 1. `fstar.exe` to be in PATH (alternatively, you can also set -# $FSTAR_HOME to be set to your F* repo/install directory) -# -# 2. `cargo`, `rustup`, `hax` and `jq` to be installed and in PATH. -# -# 3. the extracted Cargo crate to have "hax-lib" as a dependency: -# `hax-lib = { version = "0.1.0-pre.1", git = "https://github.com/hacspec/hax"}` -# -# Optionally, you can set `HACL_HOME`. +# We expect FSTAR_HOME to be set to your FSTAR repo/install directory +# We expect HACL_HOME to be set to your HACL* repo location +# We expect HAX_PROOF_LIBS_HOME to be set to the folder containing core, rust_primitives etc. +# We expect HAX_LIBS_HOME to be set to the folder containing the crate `hax-lib`. # # ROOTS contains all the top-level F* files you wish to verify # The default target `verify` verified ROOTS and its dependencies # To lax-check instead, set `OTHERFLAGS="--lax"` on the command-line # +# # To make F* emacs mode use the settings in this file, you need to # add the following lines to your .emacs # @@ -35,17 +30,17 @@ # (setq fstar-subp-prover-args #'my-fstar-compute-prover-args-using-make) # -HACL_HOME ?= $(HOME)/.hax/hacl_home -FSTAR_BIN ?= $(shell command -v fstar.exe 1>&2 2> /dev/null && echo "fstar.exe" || echo "$(FSTAR_HOME)/bin/fstar.exe") +HAX_HOME ?= $(shell git rev-parse --show-toplevel) +FSTAR_HOME ?= $(HAX_HOME)/../../../FStar +HACL_HOME ?= $(HAX_HOME)/../../../hacl-star -CACHE_DIR ?= .cache -HINT_DIR ?= .hints +FSTAR_BIN ?= $(shell command -v fstar.exe 1>&2 2> /dev/null && echo "fstar.exe" || echo "$(FSTAR_HOME)/bin/fstar.exe") -SHELL ?= /usr/bin/env bash +HAX_PROOF_LIBS_HOME ?= $(HAX_HOME)/proof-libs/fstar +HAX_LIBS_HOME ?= $(HAX_HOME)/hax-lib/proofs/fstar/extraction -EXECUTABLES = cargo cargo-hax jq -K := $(foreach bin,$(EXECUTABLES),\ - $(if $(shell command -v $(bin) 2> /dev/null),,$(error "No $(bin) in PATH"))) +CACHE_DIR ?= $(HAX_PROOF_LIBS_HOME)/.cache +HINT_DIR ?= $(HAX_PROOF_LIBS_HOME)/.hints .PHONY: all verify clean @@ -53,63 +48,17 @@ all: rm -f .depend && $(MAKE) .depend $(MAKE) verify -# Default hax invocation -HAX_CLI = "cargo hax into fstar" - -# If $HACL_HOME doesn't exist, clone it -${HACL_HOME}: - mkdir -p "${HACL_HOME}" - git clone --depth 1 https://github.com/hacl-star/hacl-star.git "${HACL_HOME}" - -# If no any F* file is detected, we run hax -ifeq "$(wildcard *.fst *fsti)" "" -$(shell $(SHELL) -c $(HAX_CLI)) -endif - -# By default, we process all the files in the current directory -ROOTS = $(wildcard *.fst *fsti) - -# Regenerate F* files via hax when Rust sources change -$(ROOTS): $(shell find ../../../src -type f -name '*.rs') - $(shell $(SHELL) -c $(HAX_CLI)) - -# The following is a bash script that discovers F* libraries -define FINDLIBS - # Prints a path if and only if it exists. Takes one argument: the - # path. - function print_if_exists() { - if [ -d "$$1" ]; then - echo "$$1" - fi - } - # Asks Cargo all the dependencies for the current crate or workspace, - # and extract all "root" directories for each. Takes zero argument. - function dependencies() { - cargo metadata --format-version 1 | - jq -r '.packages | .[] | .manifest_path | split("/") | .[:-1] | join("/")' - } - # Find hax libraries *around* a given path. Takes one argument: the - # path. - function find_hax_libraries_at_path() { - path="$$1" - # if there is a `proofs/fstar/extraction` subfolder, then that's a - # F* library - print_if_exists "$$path/proofs/fstar/extraction" - # Maybe the `proof-libs` folder of hax is around? - MAYBE_PROOF_LIBS=$$(realpath -q "$$path/../proof-libs/fstar") - if [ $$? -eq 0 ]; then - print_if_exists "$$MAYBE_PROOF_LIBS/core" - print_if_exists "$$MAYBE_PROOF_LIBS/rust_primitives" - fi - } - { while IFS= read path; do - find_hax_libraries_at_path "$$path" - done < <(dependencies) - } | sort -u -endef -export FINDLIBS - -FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib $(shell bash -c "$$FINDLIBS") +# By default, we process all the files in the current directory. Here, we +# *extend* the set of relevant files with the tests. +ROOTS = Sha256.fst + +$(ROOTS): + cargo hax into fstar + +FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib \ + $(HAX_PROOF_LIBS_HOME)/rust_primitives $(HAX_PROOF_LIBS_HOME)/core \ + $(HAX_PROOF_LIBS_HOME)/hax_lib \ + $(HAX_LIBS_HOME) FSTAR_FLAGS = --cmi \ --warn_error -331 \ @@ -119,6 +68,7 @@ FSTAR_FLAGS = --cmi \ FSTAR = $(FSTAR_BIN) $(FSTAR_FLAGS) + .depend: $(HINT_DIR) $(CACHE_DIR) $(ROOTS) $(info $(ROOTS)) $(FSTAR) --cmi --dep full $(ROOTS) --extract '* -Prims -LowStar -FStar' > $@ @@ -149,6 +99,7 @@ verify: $(addsuffix .checked, $(addprefix $(CACHE_DIR)/,$(ROOTS))) # Clean targets +SHELL ?= /usr/bin/env bash + clean: rm -rf $(CACHE_DIR)/* - rm *.fst diff --git a/hax-bounded-integers/Cargo.toml b/hax-bounded-integers/Cargo.toml deleted file mode 100644 index 56d4f11cf..000000000 --- a/hax-bounded-integers/Cargo.toml +++ /dev/null @@ -1,12 +0,0 @@ -[package] -name = "hax-bounded-integers" -version.workspace = true -authors.workspace = true -license.workspace = true -homepage.workspace = true -edition.workspace = true -repository.workspace = true -readme.workspace = true - -[dependencies] -hax-lib.workspace = true diff --git a/hax-bounded-integers/proofs/fstar/extraction/Hax_bounded_integers.Num_traits.fst b/hax-bounded-integers/proofs/fstar/extraction/Hax_bounded_integers.Num_traits.fst deleted file mode 100644 index 7ca6c74e7..000000000 --- a/hax-bounded-integers/proofs/fstar/extraction/Hax_bounded_integers.Num_traits.fst +++ /dev/null @@ -1,250 +0,0 @@ -module Hax_bounded_integers.Num_traits -#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" -open Core -open FStar.Mul - -class t_BitOps (v_Self: Type) = { - f_Output:Type; - f_count_ones_pre:v_Self -> bool; - f_count_ones_post:v_Self -> u32 -> bool; - f_count_ones:x0: v_Self - -> Prims.Pure u32 (f_count_ones_pre x0) (fun result -> f_count_ones_post x0 result); - f_count_zeros_pre:v_Self -> bool; - f_count_zeros_post:v_Self -> u32 -> bool; - f_count_zeros:x0: v_Self - -> Prims.Pure u32 (f_count_zeros_pre x0) (fun result -> f_count_zeros_post x0 result); - f_leading_ones_pre:v_Self -> bool; - f_leading_ones_post:v_Self -> u32 -> bool; - f_leading_ones:x0: v_Self - -> Prims.Pure u32 (f_leading_ones_pre x0) (fun result -> f_leading_ones_post x0 result); - f_leading_zeros_pre:v_Self -> bool; - f_leading_zeros_post:v_Self -> u32 -> bool; - f_leading_zeros:x0: v_Self - -> Prims.Pure u32 (f_leading_zeros_pre x0) (fun result -> f_leading_zeros_post x0 result); - f_trailing_ones_pre:v_Self -> bool; - f_trailing_ones_post:v_Self -> u32 -> bool; - f_trailing_ones:x0: v_Self - -> Prims.Pure u32 (f_trailing_ones_pre x0) (fun result -> f_trailing_ones_post x0 result); - f_trailing_zeros_pre:v_Self -> bool; - f_trailing_zeros_post:v_Self -> u32 -> bool; - f_trailing_zeros:x0: v_Self - -> Prims.Pure u32 (f_trailing_zeros_pre x0) (fun result -> f_trailing_zeros_post x0 result); - f_rotate_left_pre:v_Self -> u32 -> bool; - f_rotate_left_post:v_Self -> u32 -> f_Output -> bool; - f_rotate_left:x0: v_Self -> x1: u32 - -> Prims.Pure f_Output (f_rotate_left_pre x0 x1) (fun result -> f_rotate_left_post x0 x1 result); - f_rotate_right_pre:v_Self -> u32 -> bool; - f_rotate_right_post:v_Self -> u32 -> f_Output -> bool; - f_rotate_right:x0: v_Self -> x1: u32 - -> Prims.Pure f_Output - (f_rotate_right_pre x0 x1) - (fun result -> f_rotate_right_post x0 x1 result); - f_from_be_pre:v_Self -> bool; - f_from_be_post:v_Self -> f_Output -> bool; - f_from_be:x0: v_Self - -> Prims.Pure f_Output (f_from_be_pre x0) (fun result -> f_from_be_post x0 result); - f_from_le_pre:v_Self -> bool; - f_from_le_post:v_Self -> f_Output -> bool; - f_from_le:x0: v_Self - -> Prims.Pure f_Output (f_from_le_pre x0) (fun result -> f_from_le_post x0 result); - f_to_be_pre:v_Self -> bool; - f_to_be_post:v_Self -> f_Output -> bool; - f_to_be:x0: v_Self -> Prims.Pure f_Output (f_to_be_pre x0) (fun result -> f_to_be_post x0 result); - f_to_le_pre:v_Self -> bool; - f_to_le_post:v_Self -> f_Output -> bool; - f_to_le:x0: v_Self -> Prims.Pure f_Output (f_to_le_pre x0) (fun result -> f_to_le_post x0 result); - f_pow_pre:v_Self -> u32 -> bool; - f_pow_post:v_Self -> u32 -> f_Output -> bool; - f_pow:x0: v_Self -> x1: u32 - -> Prims.Pure f_Output (f_pow_pre x0 x1) (fun result -> f_pow_post x0 x1 result) -} - -class t_Bounded (v_Self: Type) = { - f_min_value_pre:Prims.unit -> bool; - f_min_value_post:Prims.unit -> v_Self -> bool; - f_min_value:x0: Prims.unit - -> Prims.Pure v_Self (f_min_value_pre x0) (fun result -> f_min_value_post x0 result); - f_max_value_pre:Prims.unit -> bool; - f_max_value_post:Prims.unit -> v_Self -> bool; - f_max_value:x0: Prims.unit - -> Prims.Pure v_Self (f_max_value_pre x0) (fun result -> f_max_value_post x0 result) -} - -class t_CheckedAdd (v_Self: Type) (v_Rhs: Type) = { - f_Output:Type; - f_checked_add_pre:v_Self -> v_Rhs -> bool; - f_checked_add_post:v_Self -> v_Rhs -> Core.Option.t_Option f_Output -> bool; - f_checked_add:x0: v_Self -> x1: v_Rhs - -> Prims.Pure (Core.Option.t_Option f_Output) - (f_checked_add_pre x0 x1) - (fun result -> f_checked_add_post x0 x1 result) -} - -class t_CheckedDiv (v_Self: Type) (v_Rhs: Type) = { - f_Output:Type; - f_checked_div_pre:v_Self -> v_Rhs -> bool; - f_checked_div_post:v_Self -> v_Rhs -> Core.Option.t_Option f_Output -> bool; - f_checked_div:x0: v_Self -> x1: v_Rhs - -> Prims.Pure (Core.Option.t_Option f_Output) - (f_checked_div_pre x0 x1) - (fun result -> f_checked_div_post x0 x1 result) -} - -class t_CheckedMul (v_Self: Type) (v_Rhs: Type) = { - f_Output:Type; - f_checked_mul_pre:v_Self -> v_Rhs -> bool; - f_checked_mul_post:v_Self -> v_Rhs -> Core.Option.t_Option f_Output -> bool; - f_checked_mul:x0: v_Self -> x1: v_Rhs - -> Prims.Pure (Core.Option.t_Option f_Output) - (f_checked_mul_pre x0 x1) - (fun result -> f_checked_mul_post x0 x1 result) -} - -class t_CheckedNeg (v_Self: Type) = { - f_Output:Type; - f_checked_neg_pre:v_Self -> bool; - f_checked_neg_post:v_Self -> Core.Option.t_Option f_Output -> bool; - f_checked_neg:x0: v_Self - -> Prims.Pure (Core.Option.t_Option f_Output) - (f_checked_neg_pre x0) - (fun result -> f_checked_neg_post x0 result) -} - -class t_CheckedSub (v_Self: Type) (v_Rhs: Type) = { - f_Output:Type; - f_checked_sub_pre:v_Self -> v_Rhs -> bool; - f_checked_sub_post:v_Self -> v_Rhs -> Core.Option.t_Option f_Output -> bool; - f_checked_sub:x0: v_Self -> x1: v_Rhs - -> Prims.Pure (Core.Option.t_Option f_Output) - (f_checked_sub_pre x0 x1) - (fun result -> f_checked_sub_post x0 x1 result) -} - -class t_FromBytes (v_Self: Type) = { - f_BYTES:Type; - f_from_le_bytes_pre:f_BYTES -> bool; - f_from_le_bytes_post:f_BYTES -> v_Self -> bool; - f_from_le_bytes:x0: f_BYTES - -> Prims.Pure v_Self (f_from_le_bytes_pre x0) (fun result -> f_from_le_bytes_post x0 result); - f_from_be_bytes_pre:f_BYTES -> bool; - f_from_be_bytes_post:f_BYTES -> v_Self -> bool; - f_from_be_bytes:x0: f_BYTES - -> Prims.Pure v_Self (f_from_be_bytes_pre x0) (fun result -> f_from_be_bytes_post x0 result) -} - -class t_NumOps (v_Self: Type) (v_Rhs: Type) (v_Output: Type) = { - [@@@ FStar.Tactics.Typeclasses.no_method]_super_3420555054487092457:Core.Ops.Arith.t_Add v_Self - v_Rhs; - [@@@ FStar.Tactics.Typeclasses.no_method]_super_16858356355397389837:Core.Ops.Arith.t_Sub v_Self - v_Rhs; - [@@@ FStar.Tactics.Typeclasses.no_method]_super_3009625865770964073:Core.Ops.Arith.t_Mul v_Self - v_Rhs; - [@@@ FStar.Tactics.Typeclasses.no_method]_super_9111207129981210576:Core.Ops.Arith.t_Div v_Self - v_Rhs; - [@@@ FStar.Tactics.Typeclasses.no_method]_super_16804214316696687705:Core.Ops.Arith.t_Rem v_Self - v_Rhs -} - -class t_One (v_Self: Type) = { - f_one_pre:Prims.unit -> bool; - f_one_post:Prims.unit -> v_Self -> bool; - f_one:x0: Prims.unit -> Prims.Pure v_Self (f_one_pre x0) (fun result -> f_one_post x0 result) -} - -class t_ToBytes (v_Self: Type) = { - [@@@ FStar.Tactics.Typeclasses.no_method]_super_4530633244223603628:t_FromBytes v_Self; - f_to_le_bytes_pre:v_Self -> bool; - f_to_le_bytes_post:v_Self -> v_4530633244223603628.f_BYTES -> bool; - f_to_le_bytes:x0: v_Self - -> Prims.Pure v_4530633244223603628.f_BYTES - (f_to_le_bytes_pre x0) - (fun result -> f_to_le_bytes_post x0 result); - f_to_be_bytes_pre:v_Self -> bool; - f_to_be_bytes_post:v_Self -> v_4530633244223603628.f_BYTES -> bool; - f_to_be_bytes:x0: v_Self - -> Prims.Pure v_4530633244223603628.f_BYTES - (f_to_be_bytes_pre x0) - (fun result -> f_to_be_bytes_post x0 result) -} - -class t_WrappingAdd (v_Self: Type) (v_Rhs: Type) = { - f_Output:Type; - f_wrapping_add_pre:v_Self -> v_Rhs -> bool; - f_wrapping_add_post:v_Self -> v_Rhs -> f_Output -> bool; - f_wrapping_add:x0: v_Self -> x1: v_Rhs - -> Prims.Pure f_Output - (f_wrapping_add_pre x0 x1) - (fun result -> f_wrapping_add_post x0 x1 result) -} - -class t_WrappingDiv (v_Self: Type) (v_Rhs: Type) = { - f_Output:Type; - f_wrapping_div_pre:v_Self -> v_Rhs -> bool; - f_wrapping_div_post:v_Self -> v_Rhs -> f_Output -> bool; - f_wrapping_div:x0: v_Self -> x1: v_Rhs - -> Prims.Pure f_Output - (f_wrapping_div_pre x0 x1) - (fun result -> f_wrapping_div_post x0 x1 result) -} - -class t_WrappingMul (v_Self: Type) (v_Rhs: Type) = { - f_Output:Type; - f_wrapping_mul_pre:v_Self -> v_Rhs -> bool; - f_wrapping_mul_post:v_Self -> v_Rhs -> f_Output -> bool; - f_wrapping_mul:x0: v_Self -> x1: v_Rhs - -> Prims.Pure f_Output - (f_wrapping_mul_pre x0 x1) - (fun result -> f_wrapping_mul_post x0 x1 result) -} - -class t_WrappingSub (v_Self: Type) (v_Rhs: Type) = { - f_Output:Type; - f_wrapping_sub_pre:v_Self -> v_Rhs -> bool; - f_wrapping_sub_post:v_Self -> v_Rhs -> f_Output -> bool; - f_wrapping_sub:x0: v_Self -> x1: v_Rhs - -> Prims.Pure f_Output - (f_wrapping_sub_pre x0 x1) - (fun result -> f_wrapping_sub_post x0 x1 result) -} - -class t_Zero (v_Self: Type) = { - f_zero_pre:Prims.unit -> bool; - f_zero_post:Prims.unit -> v_Self -> bool; - f_zero:x0: Prims.unit -> Prims.Pure v_Self (f_zero_pre x0) (fun result -> f_zero_post x0 result) -} - -class t_MachineInt (v_Self: Type) (v_Output: Type) = { - [@@@ FStar.Tactics.Typeclasses.no_method]_super_957087622381469234:Core.Marker.t_Copy v_Self; - [@@@ FStar.Tactics.Typeclasses.no_method]_super_7243498280507755391:t_Bounded v_Self; - [@@@ FStar.Tactics.Typeclasses.no_method]_super_9802961870013064174:Core.Cmp.t_PartialOrd v_Self - v_Self; - [@@@ FStar.Tactics.Typeclasses.no_method]_super_15372362079243870652:Core.Cmp.t_Ord v_Self; - [@@@ FStar.Tactics.Typeclasses.no_method]_super_1959006841676202949:Core.Cmp.t_PartialEq v_Self - v_Self; - [@@@ FStar.Tactics.Typeclasses.no_method]_super_8995075768394296398:Core.Cmp.t_Eq v_Self; - [@@@ FStar.Tactics.Typeclasses.no_method]_super_2630392019625310516:t_Zero v_Self; - [@@@ FStar.Tactics.Typeclasses.no_method]_super_6913784476497246329:t_One v_Self; - [@@@ FStar.Tactics.Typeclasses.no_method]_super_9936546819275964215:Core.Ops.Bit.t_Not v_Self; - [@@@ FStar.Tactics.Typeclasses.no_method]_super_1531387235085686842:t_NumOps v_Self - v_Self - v_Output; - [@@@ FStar.Tactics.Typeclasses.no_method]_super_3786882699227749486:Core.Ops.Bit.t_BitAnd v_Self - v_Self; - [@@@ FStar.Tactics.Typeclasses.no_method]_super_8095144530696857283:Core.Ops.Bit.t_BitOr v_Self - v_Self; - [@@@ FStar.Tactics.Typeclasses.no_method]_super_15313863003467220491:Core.Ops.Bit.t_BitXor v_Self - v_Self; - [@@@ FStar.Tactics.Typeclasses.no_method]_super_13306778606414288955:Core.Ops.Bit.t_Shl v_Self - v_Self; - [@@@ FStar.Tactics.Typeclasses.no_method]_super_2333720355461387358:Core.Ops.Bit.t_Shr v_Self - v_Self; - [@@@ FStar.Tactics.Typeclasses.no_method]_super_10133521522977299931:t_CheckedAdd v_Self v_Self; - [@@@ FStar.Tactics.Typeclasses.no_method]_super_16509367665728242671:t_CheckedSub v_Self v_Self; - [@@@ FStar.Tactics.Typeclasses.no_method]_super_261087305577220356:t_CheckedMul v_Self v_Self; - [@@@ FStar.Tactics.Typeclasses.no_method]_super_4808020806666262858:t_CheckedDiv v_Self v_Self; - [@@@ FStar.Tactics.Typeclasses.no_method]_super_18005178388944789845:t_WrappingAdd v_Self v_Self; - [@@@ FStar.Tactics.Typeclasses.no_method]_super_11471591230230619611:t_WrappingSub v_Self v_Self; - [@@@ FStar.Tactics.Typeclasses.no_method]_super_5940229659009370734:t_WrappingMul v_Self v_Self; - [@@@ FStar.Tactics.Typeclasses.no_method]_super_1640938766960073185:t_WrappingDiv v_Self v_Self; - [@@@ FStar.Tactics.Typeclasses.no_method]_super_12477248635475532096:t_BitOps v_Self -} diff --git a/hax-bounded-integers/proofs/fstar/extraction/Hax_bounded_integers.fst b/hax-bounded-integers/proofs/fstar/extraction/Hax_bounded_integers.fst deleted file mode 100644 index 8bf53bddf..000000000 --- a/hax-bounded-integers/proofs/fstar/extraction/Hax_bounded_integers.fst +++ /dev/null @@ -1,40 +0,0 @@ -module Hax_bounded_integers -#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" -open Core -open FStar.Mul - -///Bounded i128 integers. This struct enforces the invariant that values are greater or equal to `MIN` and less or equal to `MAX`. -let t_BoundedI128 (v_MIN v_MAX: i128) = x: i128{x >=. v_MIN && x <=. v_MAX} - -///Bounded i16 integers. This struct enforces the invariant that values are greater or equal to `MIN` and less or equal to `MAX`. -let t_BoundedI16 (v_MIN v_MAX: i16) = x: i16{x >=. v_MIN && x <=. v_MAX} - -///Bounded i32 integers. This struct enforces the invariant that values are greater or equal to `MIN` and less or equal to `MAX`. -let t_BoundedI32 (v_MIN v_MAX: i32) = x: i32{x >=. v_MIN && x <=. v_MAX} - -///Bounded i64 integers. This struct enforces the invariant that values are greater or equal to `MIN` and less or equal to `MAX`. -let t_BoundedI64 (v_MIN v_MAX: i64) = x: i64{x >=. v_MIN && x <=. v_MAX} - -///Bounded i8 integers. This struct enforces the invariant that values are greater or equal to `MIN` and less or equal to `MAX`. -let t_BoundedI8 (v_MIN v_MAX: i8) = x: i8{x >=. v_MIN && x <=. v_MAX} - -///Bounded isize integers. This struct enforces the invariant that values are greater or equal to `MIN` and less or equal to `MAX`. -let t_BoundedIsize (v_MIN v_MAX: isize) = x: isize{x >=. v_MIN && x <=. v_MAX} - -///Bounded u128 integers. This struct enforces the invariant that values are greater or equal to `MIN` and less or equal to `MAX`. -let t_BoundedU128 (v_MIN v_MAX: u128) = x: u128{x >=. v_MIN && x <=. v_MAX} - -///Bounded u16 integers. This struct enforces the invariant that values are greater or equal to `MIN` and less or equal to `MAX`. -let t_BoundedU16 (v_MIN v_MAX: u16) = x: u16{x >=. v_MIN && x <=. v_MAX} - -///Bounded u32 integers. This struct enforces the invariant that values are greater or equal to `MIN` and less or equal to `MAX`. -let t_BoundedU32 (v_MIN v_MAX: u32) = x: u32{x >=. v_MIN && x <=. v_MAX} - -///Bounded u64 integers. This struct enforces the invariant that values are greater or equal to `MIN` and less or equal to `MAX`. -let t_BoundedU64 (v_MIN v_MAX: u64) = x: u64{x >=. v_MIN && x <=. v_MAX} - -///Bounded u8 integers. This struct enforces the invariant that values are greater or equal to `MIN` and less or equal to `MAX`. -let t_BoundedU8 (v_MIN v_MAX: u8) = x: u8{x >=. v_MIN && x <=. v_MAX} - -///Bounded usize integers. This struct enforces the invariant that values are greater or equal to `MIN` and less or equal to `MAX`. -unfold let t_BoundedUsize (v_MIN v_MAX: usize) = x: usize{x >=. v_MIN && x <=. v_MAX} diff --git a/hax-bounded-integers/src/lib.rs b/hax-bounded-integers/src/lib.rs deleted file mode 100644 index 1f9bbd07e..000000000 --- a/hax-bounded-integers/src/lib.rs +++ /dev/null @@ -1,263 +0,0 @@ -use hax_lib::Refinement; -pub mod num_traits; - -macro_rules! derivate_binop_for_bounded { - ({$t:ident, $bounded_t:ident}; $($tt:tt)*) => { - derivate_binop_for_bounded!({$t, $bounded_t, get, Self::Output}; $($tt)*) ; - }; - ({$t:ident, $bounded_t:ident, $get:ident, $out:ty};) => {}; - ({$t:ident, $bounded_t:ident, $get:ident, $out:ty}; ($trait:ident, $meth:ident), $($tt:tt)*) => { - derivate_binop_for_bounded!(@$t, $bounded_t, $trait, $meth, $get, $out); - derivate_binop_for_bounded!({$t, $bounded_t, $get, $out}; $($tt)*); - }; - (@$t:ident, $bounded_t:ident, $trait:ident, $meth:ident, $get:ident, $out:ty) => { - // BoundedT BoundedT - impl - $trait<$bounded_t> for $bounded_t - { - type Output = $t; - #[inline(always)] - fn $meth(self, other: $bounded_t) -> $out { - (self.$get()).$meth(other.$get()) - } - } - - // BoundedT T - impl $trait<$t> for $bounded_t { - type Output = $t; - #[inline(always)] - fn $meth(self, other: $t) -> $out { - (self.$get()).$meth(other) - } - } - - // T BoundedT - impl $trait<$bounded_t> for $t { - type Output = $t; - #[inline(always)] - fn $meth(self, other: $bounded_t) -> $out { - (self).$meth(other.$get()) - } - } - }; -} - -macro_rules! mk_bounded { - ($bounded_t:ident($t: ident $($bytes:expr)?)$(,)?) => { - #[doc = concat!("Bounded ", stringify!($t)," integers. This struct enforces the invariant that values are greater or equal to `MIN` and less or equal to `MAX`.")] - #[hax_lib::refinement_type(|x| x >= MIN && x <= MAX)] - #[derive(Clone, Copy, Eq, PartialEq, Ord, PartialOrd, Hash)] - pub struct $bounded_t($t); - - #[hax_lib::exclude] - const _: () = { - use core::ops::*; - use num_traits::*; - - derivate_binop_for_bounded!( - {$t, $bounded_t}; - (Add, add), (Sub, sub), (Mul, mul), (Div, div), (Rem, rem), - (BitOr, bitor), (BitAnd, bitand), (BitXor, bitxor), - (Shl, shl), (Shr, shr), - (WrappingAdd, wrapping_add), (WrappingSub, wrapping_sub), - (WrappingMul, wrapping_mul), (WrappingDiv, wrapping_div), - ); - - derivate_binop_for_bounded!( - {$t, $bounded_t, get, Option}; - (CheckedAdd, checked_add), (CheckedSub, checked_sub), - (CheckedMul, checked_mul), (CheckedDiv, checked_div), - ); - - impl CheckedNeg for $bounded_t { - type Output = $t; - #[inline(always)] - fn checked_neg(&self) -> Option<$t> { - self.deref().checked_neg() - } - } - - impl Not for $bounded_t { - type Output = $t; - #[inline(always)] - fn not(self) -> Self::Output { - self.deref().not() - } - } - - impl NumOps for $bounded_t {} - - impl Bounded for $bounded_t { - #[inline(always)] - fn min_value() -> Self { - Self::new(MIN) - } - #[inline(always)] - fn max_value() -> Self { - Self::new(MAX) - } - } - - $( - impl FromBytes for $bounded_t { - type BYTES = [u8; $bytes]; - - #[inline(always)] - fn from_le_bytes(bytes: Self::BYTES) -> Self { - Self::new($t::from_le_bytes(bytes)) - } - #[inline(always)] - fn from_be_bytes(bytes: Self::BYTES) -> Self { - Self::new($t::from_be_bytes(bytes)) - } - } - - impl ToBytes for $bounded_t { - #[inline(always)] - fn to_le_bytes(self) -> Self::BYTES { - self.get().to_le_bytes() - } - #[inline(always)] - fn to_be_bytes(self) -> Self::BYTES { - self.get().to_be_bytes() - } - } - )? - - impl Zero for $bounded_t { - #[inline(always)] - fn zero() -> Self { - Self::new(1) - } - } - - impl One for $bounded_t { - #[inline(always)] - fn one() -> Self { - Self::new(0) - } - } - - impl MachineInt<$t> for $bounded_t { } - - impl BitOps for $bounded_t { - type Output = $t; - - #[inline(always)] - fn count_ones(self) -> u32 { - self.get().count_ones() - } - #[inline(always)] - fn count_zeros(self) -> u32 { - self.get().count_zeros() - } - #[inline(always)] - fn leading_ones(self) -> u32 { - self.get().leading_ones() - } - #[inline(always)] - fn leading_zeros(self) -> u32 { - self.get().leading_zeros() - } - #[inline(always)] - fn trailing_ones(self) -> u32 { - self.get().trailing_ones() - } - #[inline(always)] - fn trailing_zeros(self) -> u32 { - self.get().trailing_zeros() - } - #[inline(always)] - fn rotate_left(self, n: u32) -> Self::Output { - self.get().rotate_left(n) - } - #[inline(always)] - fn rotate_right(self, n: u32) -> Self::Output { - self.get().rotate_right(n) - } - #[inline(always)] - fn from_be(x: Self) -> Self::Output { - Self::Output::from_be(x.get()) - } - #[inline(always)] - fn from_le(x: Self) -> Self::Output { - Self::Output::from_le(x.get()) - } - #[inline(always)] - fn to_be(self) -> Self::Output { - Self::Output::to_be(self.get()) - } - #[inline(always)] - fn to_le(self) -> Self::Output { - Self::Output::to_le(self.get()) - } - #[inline(always)] - fn pow(self, exp: u32) -> Self::Output { - Self::Output::pow(self.get(), exp) - } - } - }; - }; - ($bounded_t:ident($t: ident $($bytes:expr)?), $($tt:tt)+) => { - mk_bounded!($bounded_t($t $($bytes)?)); - mk_bounded!($($tt)+); - }; -} - -mk_bounded!( - BoundedI8(i8 1), - BoundedI16(i16 2), - BoundedI32(i32 4), - BoundedI64(i64 8), - BoundedI128(i128 16), - BoundedIsize(isize), - BoundedU8(u8 1), - BoundedU16(u16 2), - BoundedU32(u32 4), - BoundedU64(u64 8), - BoundedU128(u128 16), - BoundedUsize(usize), -); - -#[hax_lib::exclude] -const _: () = { - impl core::ops::Index> for [T] { - type Output = T; - #[inline(always)] - fn index(&self, index: BoundedUsize) -> &Self::Output { - &self[index.get()] - } - } - - impl core::ops::IndexMut> for [T] { - #[inline(always)] - fn index_mut(&mut self, index: BoundedUsize) -> &mut Self::Output { - &mut self[index.get()] - } - } -}; - -#[test] -fn tests() { - use hax_lib::*; - - let x: BoundedU8<0, 5> = 2.into_checked(); - let y: BoundedU8<5, 10> = (x + x).into_checked(); - - let _ = x >> 3; - let _ = x >> BoundedU8::<0, 5>::new(3); - - let _ = x / y; - let _ = x * y; - let _ = x + y; - let _ = y - x; - - let _ = x / 1; - let _ = x * 1; - let _ = x + 1; - let _ = x - 1; - let _ = 4 / y; - let _ = 4 * y; - let _ = 4 + y; - let _ = 4 - y; -} diff --git a/hax-bounded-integers/src/num_traits.rs b/hax-bounded-integers/src/num_traits.rs deleted file mode 100644 index c34a710e8..000000000 --- a/hax-bounded-integers/src/num_traits.rs +++ /dev/null @@ -1,141 +0,0 @@ -//! This module provides traits for generic mathematics. This is a -//! smaller and more opinionated version of -//! [num_traits](https://docs.rs/num-traits/latest/num_traits/). -//! -//! This module is designed to make bounded integers ergonomic to use: -//! virtually every operation on bounded integers maps to their -//! underlying type. We also want binary operators to be sufficiently -//! polymophic to allow any combination: for instance, we want the -//! addition of differently bounded u8, or bounded u8 with u8 or vice -//! versa to be possible. -//! -//! Also, the traits in this module are designed to work with types -//! that implement `Copy`. - -use core::ops::*; - -pub trait Zero: Sized { - fn zero() -> Self; -} - -pub trait One: Sized { - fn one() -> Self; -} - -pub trait NumOps: - Add - + Sub - + Mul - + Div - + Rem -{ -} - -pub trait Bounded { - fn min_value() -> Self; - fn max_value() -> Self; -} - -pub trait WrappingAdd { - type Output; - fn wrapping_add(self, v: Rhs) -> Self::Output; -} - -pub trait WrappingSub { - type Output; - fn wrapping_sub(self, v: Rhs) -> Self::Output; -} - -pub trait WrappingMul { - type Output; - fn wrapping_mul(self, v: Rhs) -> Self::Output; -} - -pub trait WrappingDiv { - type Output; - fn wrapping_div(self, v: Rhs) -> Self::Output; -} - -pub trait CheckedAdd { - type Output; - fn checked_add(self, v: Rhs) -> Option; -} - -pub trait CheckedSub { - type Output; - fn checked_sub(self, v: Rhs) -> Option; -} - -pub trait CheckedMul { - type Output; - fn checked_mul(self, v: Rhs) -> Option; -} - -pub trait CheckedDiv { - type Output; - fn checked_div(self, v: Rhs) -> Option; -} - -pub trait CheckedNeg { - type Output; - fn checked_neg(&self) -> Option; -} - -pub trait FromBytes { - type BYTES; - - fn from_le_bytes(bytes: Self::BYTES) -> Self; - fn from_be_bytes(bytes: Self::BYTES) -> Self; -} - -pub trait ToBytes: FromBytes { - fn to_le_bytes(self) -> Self::BYTES; - fn to_be_bytes(self) -> Self::BYTES; -} - -pub trait MachineInt: - Copy - + Bounded - + PartialOrd - + Ord - + PartialEq - + Eq - + Zero - + One - + Not - + NumOps - + BitAnd - + BitOr - + BitXor - + Shl - + Shr - + CheckedAdd - + CheckedSub - + CheckedMul - + CheckedDiv - + WrappingAdd - + WrappingSub - + WrappingMul - + WrappingDiv - + BitOps -{ -} - -pub trait BitOps { - type Output; - - fn count_ones(self) -> u32; - fn count_zeros(self) -> u32; - fn leading_ones(self) -> u32; - fn leading_zeros(self) -> u32; - fn trailing_ones(self) -> u32; - fn trailing_zeros(self) -> u32; - fn rotate_left(self, n: u32) -> Self::Output; - fn rotate_right(self, n: u32) -> Self::Output; - fn from_be(x: Self) -> Self::Output; - fn from_le(x: Self) -> Self::Output; - fn to_be(self) -> Self::Output; - fn to_le(self) -> Self::Output; - - fn pow(self, exp: u32) -> Self::Output; -} diff --git a/hax-lib-macros/src/lib.rs b/hax-lib-macros/src/lib.rs index 5edbd8201..fef12ca43 100644 --- a/hax-lib-macros/src/lib.rs +++ b/hax-lib-macros/src/lib.rs @@ -714,16 +714,12 @@ make_quoting_proc_macro!(fstar(fstar_expr, fstar_before, fstar_after, fstar_repl /// that contains a value of type `T` and a proof that this value /// satisfies the formula `f`. /// -/// In debug mode, the refinement will be checked at run-time. This -/// requires the base type `T` to implement `Clone`. Pass a first -/// parameter `no_debug_runtime_check` to disable this behavior. -/// /// When extracted via hax, this is interpreted in the backend as a /// refinement type: the use of such a type yields static proof /// obligations. #[proc_macro_error] #[proc_macro_attribute] -pub fn refinement_type(mut attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream { +pub fn refinement_type(attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream { let mut item = parse_macro_input!(item as syn::ItemStruct); let syn::Fields::Unnamed(fields) = &item.fields else { @@ -745,24 +741,6 @@ pub fn refinement_type(mut attr: pm::TokenStream, item: pm::TokenStream) -> pm:: proc_macro_error::abort!(field.vis.span(), "This field was expected to be private"); } - let no_debug_assert = { - let mut tokens = attr.clone().into_iter(); - if let (Some(pm::TokenTree::Ident(ident)), Some(pm::TokenTree::Punct(comma))) = - (tokens.next(), tokens.next()) - { - if ident.to_string() != "no_debug_runtime_check" { - proc_macro_error::abort!(ident.span(), "Expected 'no_debug_runtime_check'"); - } - if comma.as_char() != ',' { - proc_macro_error::abort!(ident.span(), "Expected a comma"); - } - attr = pm::TokenStream::from_iter(tokens); - true - } else { - false - } - }; - let ExprClosure1 { arg: ret_binder, body: phi, @@ -814,8 +792,6 @@ pub fn refinement_type(mut attr: pm::TokenStream, item: pm::TokenStream) -> pm:: ); item.vis = parse_quote! {pub}; - let debug_assert = - no_debug_assert.then_some(quote! {::core::debug_assert!(Self::invariant(x.clone()));}); let newtype_as_ref_attr = AttrPayload::NewtypeAsRefinement; quote! { #[allow(non_snake_case)] @@ -830,15 +806,11 @@ pub fn refinement_type(mut attr: pm::TokenStream, item: pm::TokenStream) -> pm:: impl #generics ::hax_lib::Refinement for #ident <#generics_args> { type InnerType = #inner_ty; fn new(x: Self::InnerType) -> Self { - #debug_assert Self(x) } fn get(self) -> Self::InnerType { self.0 } - fn invariant(#ret_binder: Self::InnerType) -> bool { - #phi - } } #[::hax_lib::exclude] @@ -851,7 +823,7 @@ pub fn refinement_type(mut attr: pm::TokenStream, item: pm::TokenStream) -> pm:: #[::hax_lib::exclude] impl #generics ::hax_lib::RefineAs<#ident <#generics_args>> for #inner_ty { - fn into_checked(self) -> #ident <#generics_args> { + fn refine(self) -> #ident <#generics_args> { use ::hax_lib::Refinement; #ident::new(self) } diff --git a/hax-lib/proofs/fstar/extraction/Makefile b/hax-lib/proofs/fstar/extraction/Makefile index df5df7a06..b6518ff90 100644 --- a/hax-lib/proofs/fstar/extraction/Makefile +++ b/hax-lib/proofs/fstar/extraction/Makefile @@ -4,21 +4,16 @@ # makes it less portable, so resist temptation, or move to a more # sophisticated build system. # -# We expect: -# 1. `fstar.exe` to be in PATH (alternatively, you can also set -# $FSTAR_HOME to be set to your F* repo/install directory) -# -# 2. `cargo`, `rustup`, `hax` and `jq` to be installed and in PATH. -# -# 3. the extracted Cargo crate to have "hax-lib" as a dependency: -# `hax-lib = { version = "0.1.0-pre.1", git = "https://github.com/hacspec/hax"}` -# -# Optionally, you can set `HACL_HOME`. +# We expect FSTAR_HOME to be set to your FSTAR repo/install directory +# We expect HACL_HOME to be set to your HACL* repo location +# We expect HAX_PROOF_LIBS_HOME to be set to the folder containing core, rust_primitives etc. +# We expect HAX_LIBS_HOME to be set to the folder containing the crate `hax-lib`. # # ROOTS contains all the top-level F* files you wish to verify # The default target `verify` verified ROOTS and its dependencies # To lax-check instead, set `OTHERFLAGS="--lax"` on the command-line # +# # To make F* emacs mode use the settings in this file, you need to # add the following lines to your .emacs # @@ -35,17 +30,17 @@ # (setq fstar-subp-prover-args #'my-fstar-compute-prover-args-using-make) # -HACL_HOME ?= $(HOME)/.hax/hacl_home -FSTAR_BIN ?= $(shell command -v fstar.exe 1>&2 2> /dev/null && echo "fstar.exe" || echo "$(FSTAR_HOME)/bin/fstar.exe") +HAX_HOME ?= $(shell git rev-parse --show-toplevel) +FSTAR_HOME ?= $(HAX_HOME)/../../../FStar +HACL_HOME ?= $(HAX_HOME)/../../../hacl-star -CACHE_DIR ?= .cache -HINT_DIR ?= .hints +FSTAR_BIN ?= $(shell command -v fstar.exe 1>&2 2> /dev/null && echo "fstar.exe" || echo "$(FSTAR_HOME)/bin/fstar.exe") -SHELL ?= /usr/bin/env bash +HAX_PROOF_LIBS_HOME ?= $(HAX_HOME)/proof-libs/fstar +HAX_LIBS_HOME ?= $(HAX_HOME)/hax-lib/proofs/fstar/extraction -EXECUTABLES = cargo cargo-hax jq -K := $(foreach bin,$(EXECUTABLES),\ - $(if $(shell command -v $(bin) 2> /dev/null),,$(error "No $(bin) in PATH"))) +CACHE_DIR ?= $(HAX_PROOF_LIBS_HOME)/.cache +HINT_DIR ?= $(HAX_PROOF_LIBS_HOME)/.hints .PHONY: all verify clean @@ -53,63 +48,14 @@ all: rm -f .depend && $(MAKE) .depend $(MAKE) verify -# Default hax invocation -HAX_CLI = "cargo hax into fstar" - -# If $HACL_HOME doesn't exist, clone it -${HACL_HOME}: - mkdir -p "${HACL_HOME}" - git clone --depth 1 https://github.com/hacl-star/hacl-star.git "${HACL_HOME}" - -# If no any F* file is detected, we run hax -ifeq "$(wildcard *.fst *fsti)" "" -$(shell $(SHELL) -c $(HAX_CLI)) -endif - -# By default, we process all the files in the current directory -ROOTS = $(wildcard *.fst *fsti) - -# Regenerate F* files via hax when Rust sources change -$(ROOTS): $(shell find ../../../src -type f -name '*.rs') - $(shell $(SHELL) -c $(HAX_CLI)) - -# The following is a bash script that discovers F* libraries -define FINDLIBS - # Prints a path if and only if it exists. Takes one argument: the - # path. - function print_if_exists() { - if [ -d "$$1" ]; then - echo "$$1" - fi - } - # Asks Cargo all the dependencies for the current crate or workspace, - # and extract all "root" directories for each. Takes zero argument. - function dependencies() { - cargo metadata --format-version 1 | - jq -r '.packages | .[] | .manifest_path | split("/") | .[:-1] | join("/")' - } - # Find hax libraries *around* a given path. Takes one argument: the - # path. - function find_hax_libraries_at_path() { - path="$$1" - # if there is a `proofs/fstar/extraction` subfolder, then that's a - # F* library - print_if_exists "$$path/proofs/fstar/extraction" - # Maybe the `proof-libs` folder of hax is around? - MAYBE_PROOF_LIBS=$$(realpath -q "$$path/../proof-libs/fstar") - if [ $$? -eq 0 ]; then - print_if_exists "$$MAYBE_PROOF_LIBS/core" - print_if_exists "$$MAYBE_PROOF_LIBS/rust_primitives" - fi - } - { while IFS= read path; do - find_hax_libraries_at_path "$$path" - done < <(dependencies) - } | sort -u -endef -export FINDLIBS - -FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib $(shell bash -c "$$FINDLIBS") +# By default, we process all the files in the current directory. Here, we +# *extend* the set of relevant files with the tests. +ROOTS = $(*.fst) + +FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib \ + $(HAX_PROOF_LIBS_HOME)/rust_primitives $(HAX_PROOF_LIBS_HOME)/core \ + $(HAX_PROOF_LIBS_HOME)/hax_lib \ + $(HAX_LIBS_HOME) FSTAR_FLAGS = --cmi \ --warn_error -331 \ @@ -119,6 +65,7 @@ FSTAR_FLAGS = --cmi \ FSTAR = $(FSTAR_BIN) $(FSTAR_FLAGS) + .depend: $(HINT_DIR) $(CACHE_DIR) $(ROOTS) $(info $(ROOTS)) $(FSTAR) --cmi --dep full $(ROOTS) --extract '* -Prims -LowStar -FStar' > $@ @@ -131,6 +78,9 @@ $(HINT_DIR): $(CACHE_DIR): mkdir -p $@ +$(CACHE_DIR)/Chacha20.Hacspec_helper.fst.checked: | .depend $(HINT_DIR) $(CACHE_DIR) + $(FSTAR) --lax $(OTHERFLAGS) $< $(ENABLE_HINTS) --hint_file $(HINT_DIR)/$(notdir $*).hints + $(CACHE_DIR)/%.checked: | .depend $(HINT_DIR) $(CACHE_DIR) $(FSTAR) $(OTHERFLAGS) $< $(ENABLE_HINTS) --hint_file $(HINT_DIR)/$(notdir $*).hints @@ -149,6 +99,8 @@ verify: $(addsuffix .checked, $(addprefix $(CACHE_DIR)/,$(ROOTS))) # Clean targets +SHELL ?= /usr/bin/env bash + clean: rm -rf $(CACHE_DIR)/* rm *.fst diff --git a/hax-lib/src/lib.rs b/hax-lib/src/lib.rs index 9ebb361b9..67c7b893a 100644 --- a/hax-lib/src/lib.rs +++ b/hax-lib/src/lib.rs @@ -156,25 +156,16 @@ pub trait Refinement { fn new(x: Self::InnerType) -> Self; /// Destructor for the refined type fn get(self) -> Self::InnerType; - /// Tests wether a value satisfies the refinement - fn invariant(value: Self::InnerType) -> bool; } -/// A utilitary trait that provides a `into_checked` method on traits -/// that have a refined counter part. This trait is parametrized by a -/// type `Target`: a base type can be refined in multiple ways. +/// A utilitary trait that provides a `refine` methods on traits that +/// have a refined counter part. This trait is parametrized by a type +/// `Target`: a base type can be refined in multiple ways. /// /// Please never implement this trait yourself, use the /// `refinement_type` macro instead. -pub trait RefineAs { - /// Smart constructor for `RefinedType`, checking the invariant - /// `RefinedType::invariant`. The check is done statically via - /// extraction to hax: extracted code will yield static proof - /// obligations. - /// - /// In addition, in debug mode, the invariant is checked at - /// run-time, unless this behavior was disabled when defining the - /// refinement type `RefinedType` with the `refinement_type` macro - /// and its `no_debug_runtime_check` option. - fn into_checked(self) -> RefinedType; +pub trait RefineAs { + /// Smart constructor for `Target`. Its extraction will yield a + /// proof obligation. + fn refine(self) -> Target; } diff --git a/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.fst b/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.fst index 54b447f80..28ebc5425 100644 --- a/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.fst +++ b/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.fst @@ -30,23 +30,6 @@ instance update_at_tc_array t l n: update_at_tc (t_Array t l) (int_t n) = { update_at = (fun arr i x -> FStar.Seq.upd arr (v i) x); } -/// We have an instance for `int_t n`, but we often work with refined -/// `int_t n`, and F* typeclass inference doesn't support subtyping -/// well, hence the instance below. -instance impl__index_refined t l n r: t_Index (t_Array t l) (x: int_t n {r x}) - = { f_Output = t; - f_index_pre = (fun (s: t_Array t l) (i: int_t n {r i}) -> v i >= 0 && v i < v l); - f_index_post = (fun _ _ _ -> true); - f_index = (fun s i -> Seq.index s (v i)); - } - -/// Similarly to `impl__index_refined`, we need to define a instance -/// for refined `int_t n`. -instance update_at_tc_array_refined t l n r: update_at_tc (t_Array t l) (x: int_t n {r x}) = { - super_index = impl__index_refined t l n r; - update_at = (fun arr i x -> FStar.Seq.upd arr (v i) x); -} - let (.[]<-) #self #idx {| update_at_tc self idx |} (s: self) (i: idx {f_index_pre s i}) = update_at s i diff --git a/tests/attributes/src/lib.rs b/tests/attributes/src/lib.rs index aa40cc7d3..e0363aa60 100644 --- a/tests/attributes/src/lib.rs +++ b/tests/attributes/src/lib.rs @@ -204,7 +204,7 @@ mod refinement_types { #[hax_lib::requires(x < 127)] pub fn double_refine(x: u8) -> Even { - (x + x).into_checked() + (x + x).refine() } /// A string that contains no space.