feat: add barrett and kyber_compress examples (no patches required)

examples/Cargo.toml

@@ -1,5 +1,11 @@
 [workspace]
-members = ["chacha20", "limited-order-book", "sha256"]
+members = [
+    "chacha20",
+    "limited-order-book",
+    "sha256",
+    "barrett",
+    "kyber_compress",
+]
 resolver = "2"
 
 [workspace.dependencies]

examples/README.md

@@ -5,6 +5,8 @@
 | chacha20           | Typechecks                   |
 | limited-order-book | Typechecks                   |
 | sha256             | Lax-typechecks               |
+| barrett            | Typechecks                   |
+| kyber_compress     | Typechecks                   |
 
 ## How to generate the F\* code and typecheck it for the examples
 

examples/barrett/Cargo.toml

@@ -0,0 +1,9 @@
+[package]
+name = "barrett"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+hax-lib.workspace = true

examples/barrett/proofs/fstar/extraction/Makefile

@@ -0,0 +1,106 @@
+# This is a generically useful Makefile for F* that is self-contained
+#
+# It is tempting to factor this out into multiple Makefiles but that
+# 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`.
+#
+# 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
+#
+# (setq-default fstar-executable "<YOUR_FSTAR_HOME>/bin/fstar.exe")
+# (setq-default fstar-smt-executable "<YOUR_Z3_HOME>/bin/z3")
+#
+# (defun my-fstar-compute-prover-args-using-make ()
+#   "Construct arguments to pass to F* by calling make."
+#   (with-demoted-errors "Error when constructing arg string: %S"
+#     (let* ((fname (file-name-nondirectory buffer-file-name))
+# 	   (target (concat fname "-in"))
+# 	   (argstr (car (process-lines "make" "--quiet" target))))
+#       (split-string argstr))))
+# (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
+
+FSTAR_BIN      ?= $(shell command -v fstar.exe 1>&2 2> /dev/null && echo "fstar.exe" || echo "$(FSTAR_HOME)/bin/fstar.exe")
+
+HAX_PROOF_LIBS ?= $(HAX_HOME)/proof-libs/fstar
+HAX_LIB        ?= $(HAX_HOME)/hax-lib
+
+CACHE_DIR      ?= $(HAX_PROOF_LIBS)/.cache
+HINT_DIR       ?= $(HAX_PROOF_LIBS)/.hints
+
+.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)/rust_primitives $(HAX_PROOF_LIBS)/core \
+	$(HAX_PROOF_LIBS)/hax_lib \
+	$(HAX_LIB)/proofs/fstar/extraction
+
+FSTAR_FLAGS = --cmi \
+  --warn_error -331 \
+  --cache_checked_modules --cache_dir $(CACHE_DIR) \
+  --already_cached "+Prims+FStar+LowStar+C+Spec.Loops+TestLib" \
+  $(addprefix --include ,$(FSTAR_INCLUDE_DIRS))
+
+FSTAR = $(FSTAR_BIN) $(FSTAR_FLAGS)
+
+
+.depend: $(HINT_DIR) $(CACHE_DIR) $(ROOTS)
+	$(info $(ROOTS))
+	$(FSTAR) --cmi --dep full $(ROOTS) --extract '* -Prims -LowStar -FStar' > $@
+
+include .depend
+
+$(HINT_DIR):
+	mkdir -p $@
+
+$(CACHE_DIR):
+	mkdir -p $@
+
+$(CACHE_DIR)/%.checked: | .depend $(HINT_DIR) $(CACHE_DIR)
+	$(FSTAR) $(OTHERFLAGS) $< $(ENABLE_HINTS) --hint_file $(HINT_DIR)/$(notdir $*).hints
+
+verify: $(addsuffix .checked, $(addprefix $(CACHE_DIR)/,$(ROOTS)))
+
+# Targets for interactive mode
+
+%.fst-in:
+	$(info $(FSTAR_FLAGS) \
+	  $(ENABLE_HINTS) --hint_file $(HINT_DIR)/$(basename $@).fst.hints)
+
+%.fsti-in:
+	$(info $(FSTAR_FLAGS) \
+	  $(ENABLE_HINTS) --hint_file $(HINT_DIR)/$(basename $@).fsti.hints)
+
+
+# Clean targets
+
+SHELL ?= /usr/bin/env bash
+
+clean:
+	rm -rf $(CACHE_DIR)/*
+	rm *.fst

examples/barrett/src/lib.rs

@@ -0,0 +1,69 @@
+use hax_lib as hax;
+
+/// Values having this type hold a representative 'x' of the Kyber field.
+/// We use 'fe' as a shorthand for this type.
+pub(crate) type FieldElement = i32;
+
+const BARRETT_SHIFT: i64 = 26;
+const BARRETT_R: i64 = 0x4000000; // 2^26
+
+/// This is calculated as ⌊(BARRETT_R / FIELD_MODULUS) + 1/2⌋
+const BARRETT_MULTIPLIER: i64 = 20159;
+
+pub(crate) const FIELD_MODULUS: i32 = 3329;
+
+/// Signed Barrett Reduction
+///
+/// Given an input `value`, `barrett_reduce` outputs a representative `result`
+/// such that:
+///
+/// - result ≡ value (mod FIELD_MODULUS)
+/// - the absolute value of `result` is bound as follows:
+///
+/// `|result| ≤ FIELD_MODULUS / 2 · (|value|/BARRETT_R + 1)
+///
+/// In particular, if `|value| < BARRETT_R`, then `|result| < FIELD_MODULUS`.
+#[hax::requires((i64::from(value) >= -BARRETT_R && i64::from(value) <= BARRETT_R))]
+#[hax::ensures(|result| result > -FIELD_MODULUS && result < FIELD_MODULUS &&
+                   result % FIELD_MODULUS == value % FIELD_MODULUS)]
+pub fn barrett_reduce(value: FieldElement) -> FieldElement {
+    let t = i64::from(value) * BARRETT_MULTIPLIER;
+    // assert!(9223372036854775807 - (BARRETT_R >> 1) > t);
+    let t = t + (BARRETT_R >> 1);
+
+    let quotient = t >> BARRETT_SHIFT;
+    // assert!(quotient <= 2147483647_i64 || quotient >= -2147483648_i64);
+    let quotient = quotient as i32;
+
+    // assert!(((quotient as i64) * (FIELD_MODULUS as i64)) < 9223372036854775807);
+    let sub = quotient * FIELD_MODULUS;
+
+    hax::fstar!(r"Math.Lemmas.cancel_mul_mod (v $quotient) 3329");
+
+    value - sub
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn it_works() {
+        fn test(val: FieldElement, expected: FieldElement) {
+            let reduced = barrett_reduce(val);
+            assert_eq!(reduced, expected);
+        }
+
+        test(FIELD_MODULUS + 1, 1);
+        test(FIELD_MODULUS, 0);
+        test(FIELD_MODULUS - 1, -1);
+
+        test(FIELD_MODULUS + (FIELD_MODULUS - 1), -1);
+        test(FIELD_MODULUS + (FIELD_MODULUS + 1), 1);
+
+        test(1234, 1234);
+        test(9876, -111);
+
+        test(4327, 4327 % FIELD_MODULUS)
+    }
+}

examples/kyber_compress/Cargo.toml

@@ -0,0 +1,10 @@
+[package]
+name = "kyber_compress"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+hax-lib-macros.workspace = true
+hax-lib.workspace = true