Bounded integers

.envrc

@@ -0,0 +1 @@
+use flake

Cargo.toml

@@ -15,6 +15,7 @@ members = [
      "hax-lib-macros/types",
      "hax-lib-protocol",
      "hax-lib-protocol-macros",
+     "hax-bounded-integers",
      "engine/names",
      "engine/names/extract",
 ]
@@ -88,4 +89,5 @@ 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" }

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__refine f
+                   || Ast.Global_ident.eq_name Hax_lib__RefineAs__into_checked f
                    || Ast.Global_ident.eq_name Hax_lib__Refinement__get f ->
                 { e with e = Ascription { typ = e.typ; e = inner } }
             | _ -> super#visit_expr () e

engine/names/src/lib.rs

@@ -52,7 +52,7 @@ fn dummy_hax_concrete_ident_wrapper<I: core::iter::Iterator<Item = u8>>(x: I, mu
 
     fn refinements<T: Refinement, U: RefineAs<T>>(x: T, y: U) -> T {
         T::new(x.get());
-        y.refine()
+        y.into_checked()
     }
 
     const _: () = {

examples/Cargo.toml

@@ -11,3 +11,5 @@ 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" }
+

examples/barrett/proofs/fstar/extraction/Makefile

@@ -4,16 +4,21 @@
 # makes it less portable, so resist temptation, or move to a more
 # sophisticated build system.
 #
-# 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`.
+# 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`.
 #
 # 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
 #
@@ -30,35 +35,80 @@
 # (setq fstar-subp-prover-args #'my-fstar-compute-prover-args-using-make)
 #
 
-HAX_HOME       ?= $(shell git rev-parse --show-toplevel)
-FSTAR_HOME     ?= $(HAX_HOME)/../../../FStar
-HACL_HOME      ?= $(HAX_HOME)/../../../hacl-star
+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")
 
-FSTAR_BIN      ?= $(shell command -v fstar.exe 1>&2 2> /dev/null && echo "fstar.exe" || echo "$(FSTAR_HOME)/bin/fstar.exe")
+CACHE_DIR     ?= .cache
+HINT_DIR      ?= .hints
 
-HAX_PROOF_LIBS_HOME ?= $(HAX_HOME)/proof-libs/fstar
-HAX_LIBS_HOME       ?= $(HAX_HOME)/hax-lib/proofs/fstar/extraction
+SHELL ?= /usr/bin/env bash
 
-CACHE_DIR      ?= $(HAX_PROOF_LIBS)/.cache
-HINT_DIR       ?= $(HAX_PROOF_LIBS)/.hints
+EXECUTABLES = cargo cargo-hax jq
+K := $(foreach bin,$(EXECUTABLES),\
+        $(if $(shell command -v $(bin) 2> /dev/null),,$(error "No $(bin) in PATH")))
 
 .PHONY: all verify clean
 
 all:
 	rm -f .depend && $(MAKE) .depend
 	$(MAKE) verify
 
-# 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)
+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")
 
 FSTAR_FLAGS = --cmi \
   --warn_error -331 \
@@ -68,7 +118,6 @@ 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' > $@
@@ -99,8 +148,6 @@ verify: $(addsuffix .checked, $(addprefix $(CACHE_DIR)/,$(ROOTS)))
 
 # Clean targets
 
-SHELL ?= /usr/bin/env bash
-
 clean:
 	rm -rf $(CACHE_DIR)/*
 	rm *.fst

examples/chacha20/Cargo.toml

@@ -5,5 +5,5 @@ authors = ["Franziskus Kiefer <[email protected]>"]
 edition = "2021"
 
 [dependencies]
-hax-lib-macros.workspace = true
 hax-lib.workspace = true
+hax-bounded-integers.workspace = true

examples/chacha20/proofs/fstar/extraction/Chacha20.fst

@@ -15,46 +15,94 @@ let t_ChaChaKey = t_Array u8 (sz 32)
 unfold
 let t_State = 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 ) =
+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 state:t_Array u32 (sz 16) = m in
   let state:t_Array u32 (sz 16) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize state
+    Rust_primitives.Hax.update_at 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.Monomorphized_update_at.update_at_usize state
-      d
-      ((state.[ d ] <: u32) ^. (state.[ a ] <: u32) <: u32)
+    Rust_primitives.Hax.update_at state d ((state.[ d ] <: u32) ^. (state.[ a ] <: u32) <: u32)
   in
   let state:t_Array u32 (sz 16) =
-    Rust_primitives.Hax.Monomorphized_update_at.update_at_usize state
+    Rust_primitives.Hax.update_at state
       d
       (Core.Num.impl__u32__rotate_left (state.[ d ] <: u32) s <: u32)
   in
   state
 
-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 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 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) (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 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 chacha20_rounds (state: t_Array u32 (sz 16)) : t_Array u32 (sz 16) =
   let st:t_Array u32 (sz 16) = state in
@@ -126,7 +174,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 list
+  Rust_primitives.Hax.array_of_list 16 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