Update README.md and BUILDING.md to simplified tests script

Signed-off-by: Hanno Becker <[email protected]>

Author: hanno-becker

BUILDING.md

@@ -11,38 +11,50 @@ To build **mlkem-native**, you need `make` and a C90 compiler. To use the test s
 You can build and test **mlkem-native** as follows:
 
 ```bash
-make quickcheck       # With native code backend (if available)
-make OPT=0 quickcheck # With C backend
+make test       # With native code backend (if available)
+make OPT=0 test # With C backend
 ```
 
-To merely build test and benchmarking components, use the following `make` targets:
+To merely build test components, use the following `make` targets:
 
 ```bash
-make mlkem
+make func
 make nistkat
 make kat
+make acvp
 ```
 
-For benchmarking, specify the cycle counting method. Currently, **mlkem-native** is supporting PERF, PMU (AArch64 and x86 only), M1 (Apple Silicon only):
+To run them, add `run_`:
+
+```bash
+make run_func
+make run_nistkat
+make run_kat
+make run_acvp
+```
+
+The resulting binaries can be found in `test/build` (their full path is printed by `make`).
+
+For benchmarking, specify the cycle counting method. Currently, **mlkem-native** is supporting PERF, PMU (AArch64 and
+x86 only), M1 (Apple Silicon only):
+
 ```
 # CYCLES has to be on of PERF, PMU, M1, NO
-make bench CYCLES=PERF
-make bench_components CYCLES=PERF
+make run_bench CYCLES=PERF
+make run_bench_components CYCLES=PERF
 ```
 
-The resulting binaries can then be found in `test/build`.
-
 ### Using `tests` script
 
-We recommend compiling and running tests and benchmarks using the [`./scripts/tests`](scripts/tests) script. For
+For convenience, you can also use the [`./scripts/tests`](scripts/tests) script as a wrapper around `make`. For
 example,
 
 ```bash
 ./scripts/tests func
 ```
 
-will compile and run functionality tests. For detailed information on how to use the script, please refer to the
-`--help` option.
+will compile and run functionality tests. For detailed information on how to use the script, please refer to
+`./scripts/tests --help`.
 
 ### Windows
 
@@ -59,11 +71,15 @@ There are further scripts used for development of mlkem-native, such as `format`
 
 ### nix setup
 
-We specify the development environment for mlkem-native using nix. If you want to help develop mlkem-native, please setup nix using the [nix installer script](https://nixos.org/download/), not your package manager. 
+We specify the development environment for mlkem-native using nix. If you want to help develop mlkem-native, please setup nix using the [nix installer script](https://nixos.org/download/), not your package manager.
 
 All the development and build dependencies are specified in [flake.nix](flake.nix). To execute a bash shell, run
 ```bash
 nix develop --experimental-features 'nix-command flakes'
 ```
 
 To confirm that everything worked, try `lint` or `tests cbmc`.
+
+# Checking the proofs
+
+To check the CBMC proofs, enter the `nix` development environment and use `tests cbmc`.

README.md

@@ -30,11 +30,14 @@ sudo apt-get install make gcc python3 git
 git clone https://github.com/pq-code-package/mlkem-native.git
 cd mlkem-native
 
-# Build and run base tests
-make quickcheck
+# Build and run tests
+make build
+make test
 
-# Build and run all tests
+# The same using `tests`, a convenience wrapper around `make`
 ./scripts/tests all
+# Show all options
+./scripts/tests --help
 ```
 
 See [BUILDING.md](BUILDING.md) for more information.