Add ML-KEM C extraction to CI

[franziskuskiefer]

Work is happening on franziskus/ml-kem-c-extraction. This is currently blocked by issues in #199 .

A way of running the hax verification toolchain that is reproducible and maintainable.

Requirements

• Pin dependencies
• Portable
• Usable on CI and during development
• Extendable for other projects like Bertie

Design
The approach depends on two main parts: configuration, and driver.
A hax.toml defines how to run the hax toolchain, what to extract and how to verify it.
A hax.py script uses the config to drive the toolchain.

Config

• [target]
  • cargo: arguments for cargo
  • target: the hax backend to use
  • include: the -i include string (optional)
  • interfaces: the F* interfaces string (optional)
  • verify: the commands to run verification
  • clean: the commands to clean the target
  • [dependencies]
    • git: the git url to get the dependency from
    • version: the version (tag) to use (optional)
    • rev: the revision to use (optional)
    • build: the commands to build the dependency

Driver
The driver calls all the different tools to

• extract the code for the target
• get the dependencies for the verification and extraction
• verify the target
• extract_c

usage: hax.py [-h] [--clean [CLEAN ...]] target {extract,dependencies,extract_c,verify} ...

Hax driver v0.1

Config:
  - Dependencies are stored in ~/.hax
  - The prove code is expected in ~/repos/libcrux/proofs/target.target/extracted
  - Set environment variables
    - HACL_HOME=~/.hax/hacl-star
    - KRML_HOME=~/.hax/karamel
    - EURYDICE_HOME=~/.hax/eurydice
    - CHARON_HOME=~/.hax/charon
    - FSTAR_HOME=~/.hax/fstar
    - PATH=$PATH:$FSTAR_HOME/bin

positional arguments:
  target                The target from hax.toml to extract.
  {extract,dependencies,extract_c,verify}

options:
  -h, --help            show this help message and exit
  --clean [CLEAN ...]   Clean dependencies and code.
                        Use 'proof' or 'dep' to only clean one or the other

[franziskuskiefer]

Splitting into two. First the extraction is being updated in #209.