Update Kyber reference implementation to FIPS-203 draft. #42

	name: hax

	on:
	push:
	branches: ["dev"]
	paths:
	- 'specs/kyber/src/**'
	- 'src/kem/kyber768/**'
	- 'src/kem/kyber768.rs'

	pull_request:
	branches: ["dev"]
	paths:
	- 'specs/kyber/src/**'
	- 'src/kem/kyber768/**'
	- 'src/kem/kyber768.rs'

	schedule:
	- cron: '0 0 * * *'

	workflow_dispatch:

	env:
	CARGO_TERM_COLOR: always

	concurrency:
	group: ${{ github.workflow }}-${{ github.ref }}
	cancel-in-progress: true

	jobs:
	hax:
	runs-on: "ubuntu-latest"

	steps:
	- uses: actions/checkout@v4

	- name: 🔨 OCaml Setup
	uses: ocaml/setup-ocaml@v2
	with:
	ocaml-compiler: 4.14.1

	- name: ⤵ Clone hax repository
	uses: actions/checkout@v4
	with:
	repository: hacspec/hacspec-v2
	path: hax

	- name: 🔨 Setup hax
	working-directory: hax
	run: \|
	sudo apt-get update
	sudo apt-get install --yes nodejs
	./setup.sh

	- name: 🏃🏻‍♀️ Run hax extraction
	run: \|
	eval $(opam env)
	./hax-driver.py --kyber-reference
	# Extract the functions in the compress module individually to test
	# the function-extraction code.
	# Extract functions from the remaining modules to test the
	# module-extraction code.
	./hax-driver.py --crate-path specs/kyber \
	--functions hacspec_kyber::compress::compress \
	hacspec_kyber::compress::decompress \
	hacspec_kyber::compress::compress_d \
	hacspec::kyber::compress::decompress_d \
	--modules ind_cpa \
	hacspec_kyber \
	matrix \
	ntt \
	parameters \
	sampling \
	serialize \
	--exclude-modules libcrux::hacl::sha3 libcrux::digest

Provide feedback