Revert "Bounded integers"

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" }

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

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.into_checked()
+        y.refine()
     }
 
     const _: () = {

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" }
-

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,80 +30,35 @@
 # (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
 
 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

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,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