From 0b4e739f6be83e0fe9337f6363343587b35c5752 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 11 Nov 2022 12:46:23 +0100 Subject: Make the Nix build work --- Makefile | 92 +++++++++----- README.md | 6 + compiler/Driver.ml | 7 +- compiler/fstar/Primitives.fst | 287 ------------------------------------------ flake.nix | 29 ++++- fstar/Primitives.fst | 287 ++++++++++++++++++++++++++++++++++++++++++ 6 files changed, 388 insertions(+), 320 deletions(-) delete mode 100644 compiler/fstar/Primitives.fst create mode 100644 fstar/Primitives.fst diff --git a/Makefile b/Makefile index 9f71079b..7f1edf7a 100644 --- a/Makefile +++ b/Makefile @@ -3,27 +3,51 @@ ifeq (3.81,$(MAKE_VERSION)) install make, then invoke gmake instead of make) endif -all: build-tests-verify +all: build -CHARON_HOME = ../charon -DEST_DIR = tests +#################################### +# Variables customizable by the user +#################################### -# We use those variables, whose definition depends on the rule we apply -CHARON_TESTS_DIR = -CHARON_OPTIONS = -CHARON_TESTS_SRC = +# Set this variable to any value to call Charon to regenerate the .llbc source +# files before running the tests +REGEN_LLBC ?= + +# The path to Charon +CHARON_HOME ?= ../charon + +# The paths to the test directories in Charon (Aeneas will look for the .llbc +# files in there). +CHARON_TESTS_REGULAR_DIR ?= $(CHARON_HOME)/tests +CHARON_TESTS_POLONIUS_DIR ?= $(CHARON_HOME)/tests-polonius AENEAS_DRIVER = driver.exe -# The user can specify additional translation options for Aeneas: -OPTIONS += -unfold-monads +# The path to the Aeneas executable to run the tests - we need the ability to +# change this path for the Nix package. +AENEAS_EXE ?= compiler/_build/default/$(AENEAS_DRIVER) -# Default translation options: +# The user can specify additional translation options for Aeneas. +# By default we do: +# - unfold all the monadic let bindings to matches (required by F*) # - insert calls to the normalizer in the translated code to test the # generated unit functions -TRANS_OPTIONS := -test-trans-units $(OPTIONS) +OPTIONS += -unfold-monads -test-trans-units + +# +# The rules use (and update) the following variables +# +# The Charon test directory where to look for the .llbc files +CHARON_TEST_DIR = +# The options with which to call Charon +CHARON_OPTIONS = +# The directory in which to extract the result of the translation SUBDIR := +#################################### +# The rules +#################################### + # Build the project, test it and verify the generated files .PHONY: build-test-verify build-tests-verify: build tests verify @@ -50,7 +74,7 @@ clean: # Test the project by translating test files to F* .PHONY: tests -tests: build trans-no_nested_borrows trans-paper \ +tests: trans-no_nested_borrows trans-paper \ trans-hashmap trans-hashmap_main \ trans-external trans-constants \ trans-polonius-betree_polonius trans-polonius-betree_main \ @@ -67,41 +91,45 @@ format: cd compiler && dune promote # The commands to run Charon to generate the .llbc files -CHARON_CMD = cd $(CHARON_HOME)/$(CHARON_TEST_SUBFOLDER) && NOT_ALL_TESTS=1 $(MAKE) test-$* +ifeq (, $(REGEN_LLBC)) +else +CHARON_CMD = cd $(CHARON_TEST_DIR) && NOT_ALL_TESTS=1 $(MAKE) test-$* +endif # The command to run Aeneas on the proper llbc file -AENEAS_CMD = cd compiler && dune exec -- ./$(AENEAS_DRIVER) ../$(CHARON_TESTS_DIR)/$(FILE).llbc -dest ../$(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS) +AENEAS_CMD = $(AENEAS_EXE) $(CHARON_TEST_DIR)/llbc/$(FILE).llbc -dest ../tests/$(SUBDIR) $(OPTIONS) + # Add specific options to some tests trans-no_nested_borrows trans-paper: \ - TRANS_OPTIONS += -test-units -test-trans-units -no-split-files -no-state -no-decreases-clauses + OPTIONS += -test-units -test-trans-units -no-split-files -no-state -no-decreases-clauses trans-no_nested_borrows trans-paper: SUBDIR:=misc -trans-hashmap: TRANS_OPTIONS += -template-clauses -no-state +trans-hashmap: OPTIONS += -template-clauses -no-state trans-hashmap: SUBDIR:=hashmap -trans-hashmap_main: TRANS_OPTIONS += -template-clauses +trans-hashmap_main: OPTIONS += -template-clauses trans-hashmap_main: SUBDIR:=hashmap_on_disk -trans-polonius-betree_polonius: TRANS_OPTIONS += -test-units -test-trans-units -no-split-files -no-state -no-decreases-clauses +trans-polonius-betree_polonius: OPTIONS += -test-units -test-trans-units -no-split-files -no-state -no-decreases-clauses trans-polonius-betree_polonius: SUBDIR:=misc -trans-constants: TRANS_OPTIONS += -test-units -test-trans-units -no-split-files -no-state -no-decreases-clauses +trans-constants: OPTIONS += -test-units -test-trans-units -no-split-files -no-state -no-decreases-clauses trans-constants: SUBDIR:=misc -trans-external: TRANS_OPTIONS += +trans-external: OPTIONS += trans-external: SUBDIR:=misc BETREE_OPTIONS = -template-clauses -trans-polonius-betree_main: TRANS_OPTIONS += $(BETREE_OPTIONS) -backward-no-state-update +trans-polonius-betree_main: OPTIONS += $(BETREE_OPTIONS) -backward-no-state-update trans-polonius-betree_main: SUBDIR:=betree # Additional test on the betree: translate it without `-backward-no-state-update`. # This generates very ugly code, but is good to test the translation. test-trans-polonius-betree_main: trans-polonius-betree_main -test-trans-polonius-betree_main: TRANS_OPTIONS += $(BETREE_OPTIONS) +test-trans-polonius-betree_main: OPTIONS += $(BETREE_OPTIONS) test-trans-polonius-betree_main: SUBDIR:=betree_back_stateful -test-trans-polonius-betree_main: CHARON_TESTS_DIR = $(CHARON_HOME)/tests-polonius/llbc +test-trans-polonius-betree_main: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR) test-trans-polonius-betree_main: FILE = betree_main test-trans-polonius-betree_main: $(AENEAS_CMD) @@ -110,21 +138,22 @@ test-trans-polonius-betree_main: # We use the rules in Charon's Makefile to generate the .llbc files: the options # vary with the test files. .PHONY: gen-llbc-polonius-% -gen-llbc-polonius-%: CHARON_TEST_SUBFOLDER = tests-polonius -gen-llbc-polonius-%: build +gen-llbc-polonius-%: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR) +gen-llbc-polonius-%: $(CHARON_CMD) .PHONY: gen-llbc-% -gen-llbc-%: CHARON_TEST_SUBFOLDER = tests -gen-llbc-%: build +gen-llbc-%: CHARON_TEST_DIR = $(CHARON_TESTS_REGULAR_DIR) +gen-llbc-%: $(CHARON_CMD) # Generic rule to test the translation of an LLBC file. # Note that the files requiring the Polonius borrow-checker are generated # in the tests-polonius subdirectory. .PHONY: trans-% -trans-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests/llbc -trans-polonius-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests-polonius/llbc +trans-%: +trans-polonius-%: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR) +trans-%: CHARON_TEST_DIR = $(CHARON_TESTS_REGULAR_DIR) trans-polonius-%: FILE = $* trans-polonius-%: gen-llbc-polonius-% @@ -133,3 +162,8 @@ trans-polonius-%: gen-llbc-polonius-% trans-%: FILE = $* trans-%: gen-llbc-% $(AENEAS_CMD) + +# Nix +.PHONY: nix +nix: + nix build .#checks.x86_64-linux.aeneas-tests --show-trace -L diff --git a/README.md b/README.md index f3c8a480..6e60657d 100644 --- a/README.md +++ b/README.md @@ -63,6 +63,12 @@ if [ -e charon ]; then echo "valid"; else echo "invalid"; fi Finally, building the project simply requires to run `make` in the top directory. +You can also use `make tests` and `make verify` to run the tests, and check +the generated files. As `make tests` will run tests which use the Charon tests, +you will need to regenerate the `.llbc` files. You have the following options: +- run `make tests` in the Charon repository +- run `REGEN_LLBC=1 make tests` in the Aeneas repository + ## Documentation If you run `make`, you will generate a documentation accessible from [`doc.html`](./doc.html). diff --git a/compiler/Driver.ml b/compiler/Driver.ml index 304d0f2f..3059ec2f 100644 --- a/compiler/Driver.ml +++ b/compiler/Driver.ml @@ -140,17 +140,18 @@ let () = pure_micro_passes_log#set_level EL.Info; pure_to_extract_log#set_level EL.Info; translate_log#set_level EL.Info; + let log = main_log in (* Load the module *) let json = Yojson.Basic.from_file filename in match crate_of_json json with | Error s -> - main_log#error "error: %s\n" s; + log#error "error: %s\n" s; exit 1 | Ok m -> (* Logging *) - main_log#linfo (lazy ("Imported: " ^ filename)); - main_log#ldebug (lazy ("\n" ^ Print.Crate.crate_to_string m ^ "\n")); + log#linfo (lazy ("Imported: " ^ filename)); + log#ldebug (lazy ("\n" ^ Print.Crate.crate_to_string m ^ "\n")); (* Apply the pre-passes *) let m = PrePasses.apply_passes m in diff --git a/compiler/fstar/Primitives.fst b/compiler/fstar/Primitives.fst deleted file mode 100644 index 96138e46..00000000 --- a/compiler/fstar/Primitives.fst +++ /dev/null @@ -1,287 +0,0 @@ -/// This file lists primitive and assumed functions and types -module Primitives -open FStar.Mul -open FStar.List.Tot - -#set-options "--z3rlimit 15 --fuel 0 --ifuel 1" - -(*** Utilities *) -val list_update (#a : Type0) (ls : list a) (i : nat{i < length ls}) (x : a) : - ls':list a{ - length ls' = length ls /\ - index ls' i == x - } -#push-options "--fuel 1" -let rec list_update #a ls i x = - match ls with - | x' :: ls -> if i = 0 then x :: ls else x' :: list_update ls (i-1) x -#pop-options - -(*** Result *) -type result (a : Type0) : Type0 = -| Return : v:a -> result a -| Fail : result a - -// Monadic bind and return. -// Re-definining those allows us to customize the result of the monadic notations -// like: `y <-- f x;` -let return (#a : Type0) (x:a) : result a = Return x -let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b = - match m with - | Return x -> f x - | Fail -> Fail - -// Monadic assert(...) -let massert (b:bool) : result unit = if b then Return () else Fail - -// Normalize and unwrap a successful result (used for globals). -let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x - -(*** Misc *) -type char = FStar.Char.char -type string = string - -let mem_replace_fwd (a : Type0) (x : a) (y : a) : a = x -let mem_replace_back (a : Type0) (x : a) (y : a) : a = y - -(*** Scalars *) -/// Rk.: most of the following code was at least partially generated - -let isize_min : int = -9223372036854775808 // TODO: should be opaque -let isize_max : int = 9223372036854775807 // TODO: should be opaque -let i8_min : int = -128 -let i8_max : int = 127 -let i16_min : int = -32768 -let i16_max : int = 32767 -let i32_min : int = -2147483648 -let i32_max : int = 2147483647 -let i64_min : int = -9223372036854775808 -let i64_max : int = 9223372036854775807 -let i128_min : int = -170141183460469231731687303715884105728 -let i128_max : int = 170141183460469231731687303715884105727 -let usize_min : int = 0 -let usize_max : int = 4294967295 // TODO: should be opaque -let u8_min : int = 0 -let u8_max : int = 255 -let u16_min : int = 0 -let u16_max : int = 65535 -let u32_min : int = 0 -let u32_max : int = 4294967295 -let u64_min : int = 0 -let u64_max : int = 18446744073709551615 -let u128_min : int = 0 -let u128_max : int = 340282366920938463463374607431768211455 - -type scalar_ty = -| Isize -| I8 -| I16 -| I32 -| I64 -| I128 -| Usize -| U8 -| U16 -| U32 -| U64 -| U128 - -let scalar_min (ty : scalar_ty) : int = - match ty with - | Isize -> isize_min - | I8 -> i8_min - | I16 -> i16_min - | I32 -> i32_min - | I64 -> i64_min - | I128 -> i128_min - | Usize -> usize_min - | U8 -> u8_min - | U16 -> u16_min - | U32 -> u32_min - | U64 -> u64_min - | U128 -> u128_min - -let scalar_max (ty : scalar_ty) : int = - match ty with - | Isize -> isize_max - | I8 -> i8_max - | I16 -> i16_max - | I32 -> i32_max - | I64 -> i64_max - | I128 -> i128_max - | Usize -> usize_max - | U8 -> u8_max - | U16 -> u16_max - | U32 -> u32_max - | U64 -> u64_max - | U128 -> u128_max - -type scalar (ty : scalar_ty) : eqtype = x:int{scalar_min ty <= x && x <= scalar_max ty} - -let mk_scalar (ty : scalar_ty) (x : int) : result (scalar ty) = - if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail - -let scalar_neg (#ty : scalar_ty) (x : scalar ty) : result (scalar ty) = mk_scalar ty (-x) - -let scalar_div (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) = - if y <> 0 then mk_scalar ty (x / y) else Fail - -/// The remainder operation -let int_rem (x : int) (y : int{y <> 0}) : int = - if x >= 0 then (x % y) else -(x % y) - -(* Checking consistency with Rust *) -let _ = assert_norm(int_rem 1 2 = 1) -let _ = assert_norm(int_rem (-1) 2 = -1) -let _ = assert_norm(int_rem 1 (-2) = 1) -let _ = assert_norm(int_rem (-1) (-2) = -1) - -let scalar_rem (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) = - if y <> 0 then mk_scalar ty (int_rem x y) else Fail - -let scalar_add (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) = - mk_scalar ty (x + y) - -let scalar_sub (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) = - mk_scalar ty (x - y) - -let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) = - mk_scalar ty (x * y) - -(** Cast an integer from a [src_ty] to a [tgt_ty] *) -// TODO: check the semantics of casts in Rust -let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) = - mk_scalar tgt_ty x - -/// The scalar types -type isize : eqtype = scalar Isize -type i8 : eqtype = scalar I8 -type i16 : eqtype = scalar I16 -type i32 : eqtype = scalar I32 -type i64 : eqtype = scalar I64 -type i128 : eqtype = scalar I128 -type usize : eqtype = scalar Usize -type u8 : eqtype = scalar U8 -type u16 : eqtype = scalar U16 -type u32 : eqtype = scalar U32 -type u64 : eqtype = scalar U64 -type u128 : eqtype = scalar U128 - -/// Negation -let isize_neg = scalar_neg #Isize -let i8_neg = scalar_neg #I8 -let i16_neg = scalar_neg #I16 -let i32_neg = scalar_neg #I32 -let i64_neg = scalar_neg #I64 -let i128_neg = scalar_neg #I128 - -/// Division -let isize_div = scalar_div #Isize -let i8_div = scalar_div #I8 -let i16_div = scalar_div #I16 -let i32_div = scalar_div #I32 -let i64_div = scalar_div #I64 -let i128_div = scalar_div #I128 -let usize_div = scalar_div #Usize -let u8_div = scalar_div #U8 -let u16_div = scalar_div #U16 -let u32_div = scalar_div #U32 -let u64_div = scalar_div #U64 -let u128_div = scalar_div #U128 - -/// Remainder -let isize_rem = scalar_rem #Isize -let i8_rem = scalar_rem #I8 -let i16_rem = scalar_rem #I16 -let i32_rem = scalar_rem #I32 -let i64_rem = scalar_rem #I64 -let i128_rem = scalar_rem #I128 -let usize_rem = scalar_rem #Usize -let u8_rem = scalar_rem #U8 -let u16_rem = scalar_rem #U16 -let u32_rem = scalar_rem #U32 -let u64_rem = scalar_rem #U64 -let u128_rem = scalar_rem #U128 - -/// Addition -let isize_add = scalar_add #Isize -let i8_add = scalar_add #I8 -let i16_add = scalar_add #I16 -let i32_add = scalar_add #I32 -let i64_add = scalar_add #I64 -let i128_add = scalar_add #I128 -let usize_add = scalar_add #Usize -let u8_add = scalar_add #U8 -let u16_add = scalar_add #U16 -let u32_add = scalar_add #U32 -let u64_add = scalar_add #U64 -let u128_add = scalar_add #U128 - -/// Substraction -let isize_sub = scalar_sub #Isize -let i8_sub = scalar_sub #I8 -let i16_sub = scalar_sub #I16 -let i32_sub = scalar_sub #I32 -let i64_sub = scalar_sub #I64 -let i128_sub = scalar_sub #I128 -let usize_sub = scalar_sub #Usize -let u8_sub = scalar_sub #U8 -let u16_sub = scalar_sub #U16 -let u32_sub = scalar_sub #U32 -let u64_sub = scalar_sub #U64 -let u128_sub = scalar_sub #U128 - -/// Multiplication -let isize_mul = scalar_mul #Isize -let i8_mul = scalar_mul #I8 -let i16_mul = scalar_mul #I16 -let i32_mul = scalar_mul #I32 -let i64_mul = scalar_mul #I64 -let i128_mul = scalar_mul #I128 -let usize_mul = scalar_mul #Usize -let u8_mul = scalar_mul #U8 -let u16_mul = scalar_mul #U16 -let u32_mul = scalar_mul #U32 -let u64_mul = scalar_mul #U64 -let u128_mul = scalar_mul #U128 - -(*** Vector *) -type vec (a : Type0) = v:list a{length v <= usize_max} - -let vec_new (a : Type0) : vec a = assert_norm(length #a [] == 0); [] -let vec_len (a : Type0) (v : vec a) : usize = length v - -// The **forward** function shouldn't be used -let vec_push_fwd (a : Type0) (v : vec a) (x : a) : unit = () -let vec_push_back (a : Type0) (v : vec a) (x : a) : - Pure (result (vec a)) - (requires True) - (ensures (fun res -> - match res with - | Fail -> True - | Return v' -> length v' = length v + 1)) = - if length v < usize_max then begin - (**) assert_norm(length [x] == 1); - (**) append_length v [x]; - (**) assert(length (append v [x]) = length v + 1); - Return (append v [x]) - end - else Fail - -// The **forward** function shouldn't be used -let vec_insert_fwd (a : Type0) (v : vec a) (i : usize) (x : a) : result unit = - if i < length v then Return () else Fail -let vec_insert_back (a : Type0) (v : vec a) (i : usize) (x : a) : result (vec a) = - if i < length v then Return (list_update v i x) else Fail - -// The **backward** function shouldn't be used -let vec_index_fwd (a : Type0) (v : vec a) (i : usize) : result a = - if i < length v then Return (index v i) else Fail -let vec_index_back (a : Type0) (v : vec a) (i : usize) (x : a) : result unit = - if i < length v then Return () else Fail - -let vec_index_mut_fwd (a : Type0) (v : vec a) (i : usize) : result a = - if i < length v then Return (index v i) else Fail -let vec_index_mut_back (a : Type0) (v : vec a) (i : usize) (nx : a) : result (vec a) = - if i < length v then Return (list_update v i nx) else Fail - diff --git a/flake.nix b/flake.nix index 712bc604..a67e2e18 100644 --- a/flake.nix +++ b/flake.nix @@ -26,7 +26,7 @@ aeneas = ocamlPackages.buildDunePackage { pname = "aeneas"; version = "0.1.0"; - src = ./.; + src = ./compiler; buildInputs = [ easy_logging charon.packages.${system}.charon-ml ] ++ (with ocamlPackages; [ calendar @@ -36,11 +36,38 @@ yojson zarith ]); + afterBuild = '' + echo charon.packages.${system}.tests + ''; + }; + # Make sure we don't need to recompile the package whenever we make + # unnecessary changes - we list the exact files and folders the package + # depends upon. + aeneas-tests = pkgs.stdenv.mkDerivation { + name = "aeneas_tests"; + src = pkgs.lib.cleanSourceWith { + src = ./.; + filter = path: type: + path == toString ./Makefile + || pkgs.lib.hasPrefix (toString ./compiler) path + || pkgs.lib.hasPrefix (toString ./fstar) path + || pkgs.lib.hasPrefix (toString ./tests) path; + }; + buildPhase = '' + export CHARON_TESTS_REGULAR_DIR=${charon.checks.${system}.tests} + export CHARON_TESTS_POLONIUS_DIR=${charon.checks.${system}.tests-polonius} + export AENEAS_EXE=${aeneas}/bin/aeneas_driver + + make tests + ''; + installPhase = "touch $out"; }; in { packages = { inherit aeneas; default = aeneas; }; + checks = { inherit aeneas aeneas-tests; }; + hydraJobs = { inherit aeneas aeneas-tests; }; }); } diff --git a/fstar/Primitives.fst b/fstar/Primitives.fst new file mode 100644 index 00000000..96138e46 --- /dev/null +++ b/fstar/Primitives.fst @@ -0,0 +1,287 @@ +/// This file lists primitive and assumed functions and types +module Primitives +open FStar.Mul +open FStar.List.Tot + +#set-options "--z3rlimit 15 --fuel 0 --ifuel 1" + +(*** Utilities *) +val list_update (#a : Type0) (ls : list a) (i : nat{i < length ls}) (x : a) : + ls':list a{ + length ls' = length ls /\ + index ls' i == x + } +#push-options "--fuel 1" +let rec list_update #a ls i x = + match ls with + | x' :: ls -> if i = 0 then x :: ls else x' :: list_update ls (i-1) x +#pop-options + +(*** Result *) +type result (a : Type0) : Type0 = +| Return : v:a -> result a +| Fail : result a + +// Monadic bind and return. +// Re-definining those allows us to customize the result of the monadic notations +// like: `y <-- f x;` +let return (#a : Type0) (x:a) : result a = Return x +let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b = + match m with + | Return x -> f x + | Fail -> Fail + +// Monadic assert(...) +let massert (b:bool) : result unit = if b then Return () else Fail + +// Normalize and unwrap a successful result (used for globals). +let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x + +(*** Misc *) +type char = FStar.Char.char +type string = string + +let mem_replace_fwd (a : Type0) (x : a) (y : a) : a = x +let mem_replace_back (a : Type0) (x : a) (y : a) : a = y + +(*** Scalars *) +/// Rk.: most of the following code was at least partially generated + +let isize_min : int = -9223372036854775808 // TODO: should be opaque +let isize_max : int = 9223372036854775807 // TODO: should be opaque +let i8_min : int = -128 +let i8_max : int = 127 +let i16_min : int = -32768 +let i16_max : int = 32767 +let i32_min : int = -2147483648 +let i32_max : int = 2147483647 +let i64_min : int = -9223372036854775808 +let i64_max : int = 9223372036854775807 +let i128_min : int = -170141183460469231731687303715884105728 +let i128_max : int = 170141183460469231731687303715884105727 +let usize_min : int = 0 +let usize_max : int = 4294967295 // TODO: should be opaque +let u8_min : int = 0 +let u8_max : int = 255 +let u16_min : int = 0 +let u16_max : int = 65535 +let u32_min : int = 0 +let u32_max : int = 4294967295 +let u64_min : int = 0 +let u64_max : int = 18446744073709551615 +let u128_min : int = 0 +let u128_max : int = 340282366920938463463374607431768211455 + +type scalar_ty = +| Isize +| I8 +| I16 +| I32 +| I64 +| I128 +| Usize +| U8 +| U16 +| U32 +| U64 +| U128 + +let scalar_min (ty : scalar_ty) : int = + match ty with + | Isize -> isize_min + | I8 -> i8_min + | I16 -> i16_min + | I32 -> i32_min + | I64 -> i64_min + | I128 -> i128_min + | Usize -> usize_min + | U8 -> u8_min + | U16 -> u16_min + | U32 -> u32_min + | U64 -> u64_min + | U128 -> u128_min + +let scalar_max (ty : scalar_ty) : int = + match ty with + | Isize -> isize_max + | I8 -> i8_max + | I16 -> i16_max + | I32 -> i32_max + | I64 -> i64_max + | I128 -> i128_max + | Usize -> usize_max + | U8 -> u8_max + | U16 -> u16_max + | U32 -> u32_max + | U64 -> u64_max + | U128 -> u128_max + +type scalar (ty : scalar_ty) : eqtype = x:int{scalar_min ty <= x && x <= scalar_max ty} + +let mk_scalar (ty : scalar_ty) (x : int) : result (scalar ty) = + if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail + +let scalar_neg (#ty : scalar_ty) (x : scalar ty) : result (scalar ty) = mk_scalar ty (-x) + +let scalar_div (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) = + if y <> 0 then mk_scalar ty (x / y) else Fail + +/// The remainder operation +let int_rem (x : int) (y : int{y <> 0}) : int = + if x >= 0 then (x % y) else -(x % y) + +(* Checking consistency with Rust *) +let _ = assert_norm(int_rem 1 2 = 1) +let _ = assert_norm(int_rem (-1) 2 = -1) +let _ = assert_norm(int_rem 1 (-2) = 1) +let _ = assert_norm(int_rem (-1) (-2) = -1) + +let scalar_rem (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) = + if y <> 0 then mk_scalar ty (int_rem x y) else Fail + +let scalar_add (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) = + mk_scalar ty (x + y) + +let scalar_sub (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) = + mk_scalar ty (x - y) + +let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) = + mk_scalar ty (x * y) + +(** Cast an integer from a [src_ty] to a [tgt_ty] *) +// TODO: check the semantics of casts in Rust +let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) = + mk_scalar tgt_ty x + +/// The scalar types +type isize : eqtype = scalar Isize +type i8 : eqtype = scalar I8 +type i16 : eqtype = scalar I16 +type i32 : eqtype = scalar I32 +type i64 : eqtype = scalar I64 +type i128 : eqtype = scalar I128 +type usize : eqtype = scalar Usize +type u8 : eqtype = scalar U8 +type u16 : eqtype = scalar U16 +type u32 : eqtype = scalar U32 +type u64 : eqtype = scalar U64 +type u128 : eqtype = scalar U128 + +/// Negation +let isize_neg = scalar_neg #Isize +let i8_neg = scalar_neg #I8 +let i16_neg = scalar_neg #I16 +let i32_neg = scalar_neg #I32 +let i64_neg = scalar_neg #I64 +let i128_neg = scalar_neg #I128 + +/// Division +let isize_div = scalar_div #Isize +let i8_div = scalar_div #I8 +let i16_div = scalar_div #I16 +let i32_div = scalar_div #I32 +let i64_div = scalar_div #I64 +let i128_div = scalar_div #I128 +let usize_div = scalar_div #Usize +let u8_div = scalar_div #U8 +let u16_div = scalar_div #U16 +let u32_div = scalar_div #U32 +let u64_div = scalar_div #U64 +let u128_div = scalar_div #U128 + +/// Remainder +let isize_rem = scalar_rem #Isize +let i8_rem = scalar_rem #I8 +let i16_rem = scalar_rem #I16 +let i32_rem = scalar_rem #I32 +let i64_rem = scalar_rem #I64 +let i128_rem = scalar_rem #I128 +let usize_rem = scalar_rem #Usize +let u8_rem = scalar_rem #U8 +let u16_rem = scalar_rem #U16 +let u32_rem = scalar_rem #U32 +let u64_rem = scalar_rem #U64 +let u128_rem = scalar_rem #U128 + +/// Addition +let isize_add = scalar_add #Isize +let i8_add = scalar_add #I8 +let i16_add = scalar_add #I16 +let i32_add = scalar_add #I32 +let i64_add = scalar_add #I64 +let i128_add = scalar_add #I128 +let usize_add = scalar_add #Usize +let u8_add = scalar_add #U8 +let u16_add = scalar_add #U16 +let u32_add = scalar_add #U32 +let u64_add = scalar_add #U64 +let u128_add = scalar_add #U128 + +/// Substraction +let isize_sub = scalar_sub #Isize +let i8_sub = scalar_sub #I8 +let i16_sub = scalar_sub #I16 +let i32_sub = scalar_sub #I32 +let i64_sub = scalar_sub #I64 +let i128_sub = scalar_sub #I128 +let usize_sub = scalar_sub #Usize +let u8_sub = scalar_sub #U8 +let u16_sub = scalar_sub #U16 +let u32_sub = scalar_sub #U32 +let u64_sub = scalar_sub #U64 +let u128_sub = scalar_sub #U128 + +/// Multiplication +let isize_mul = scalar_mul #Isize +let i8_mul = scalar_mul #I8 +let i16_mul = scalar_mul #I16 +let i32_mul = scalar_mul #I32 +let i64_mul = scalar_mul #I64 +let i128_mul = scalar_mul #I128 +let usize_mul = scalar_mul #Usize +let u8_mul = scalar_mul #U8 +let u16_mul = scalar_mul #U16 +let u32_mul = scalar_mul #U32 +let u64_mul = scalar_mul #U64 +let u128_mul = scalar_mul #U128 + +(*** Vector *) +type vec (a : Type0) = v:list a{length v <= usize_max} + +let vec_new (a : Type0) : vec a = assert_norm(length #a [] == 0); [] +let vec_len (a : Type0) (v : vec a) : usize = length v + +// The **forward** function shouldn't be used +let vec_push_fwd (a : Type0) (v : vec a) (x : a) : unit = () +let vec_push_back (a : Type0) (v : vec a) (x : a) : + Pure (result (vec a)) + (requires True) + (ensures (fun res -> + match res with + | Fail -> True + | Return v' -> length v' = length v + 1)) = + if length v < usize_max then begin + (**) assert_norm(length [x] == 1); + (**) append_length v [x]; + (**) assert(length (append v [x]) = length v + 1); + Return (append v [x]) + end + else Fail + +// The **forward** function shouldn't be used +let vec_insert_fwd (a : Type0) (v : vec a) (i : usize) (x : a) : result unit = + if i < length v then Return () else Fail +let vec_insert_back (a : Type0) (v : vec a) (i : usize) (x : a) : result (vec a) = + if i < length v then Return (list_update v i x) else Fail + +// The **backward** function shouldn't be used +let vec_index_fwd (a : Type0) (v : vec a) (i : usize) : result a = + if i < length v then Return (index v i) else Fail +let vec_index_back (a : Type0) (v : vec a) (i : usize) (x : a) : result unit = + if i < length v then Return () else Fail + +let vec_index_mut_fwd (a : Type0) (v : vec a) (i : usize) : result a = + if i < length v then Return (index v i) else Fail +let vec_index_mut_back (a : Type0) (v : vec a) (i : usize) (nx : a) : result (vec a) = + if i < length v then Return (list_update v i nx) else Fail + -- cgit v1.2.3