Removing hacspec

.github/workflows/build-and-test.yml

@@ -5,6 +5,7 @@ on:
     branches: [main]
     tags: 'v*'
   pull_request:
+  workflow_dispatch:
 
 env:
   CARGO_TERM_COLOR: always
@@ -27,19 +28,15 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        edhoc_lib: [hacspec, rust]
-        crypto: [hacspec, psa]
+        crypto_backend: [crypto-hacspec, crypto-psa]
         ead: [ead-none, ead-zeroconf]
-        exclude:
-          - edhoc_lib: rust
-            crypto: hacspec
 
     steps:
     - name: Checkout repo
       uses: actions/checkout@v3
 
     - name: Run unit tests # note that we only add `--package edhoc-hacspec` when testing the hacspec version of the lib
-      run: cargo test --package edhoc-rs --package edhoc-crypto --package edhoc-ead ${{ matrix.edhoc_lib == 'hacspec' && '--package edhoc-hacspec' || '' }} --no-default-features --features="${{ matrix.edhoc_lib }}-${{ matrix.crypto }}, ${{ matrix.ead }}" --no-fail-fast
+      run: cargo test --package edhoc-rs --package edhoc-crypto --package edhoc-ead --no-default-features --features="${{ matrix.crypto_backend }}, ${{ matrix.ead }}" --no-fail-fast
 
 
   build-edhoc-package:
@@ -49,12 +46,8 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        edhoc_lib: [hacspec, rust]
-        crypto: [hacspec, psa, psa-baremetal, cryptocell310]
+        crypto_backend: [crypto-hacspec, crypto-psa, crypto-psa-baremetal, crypto-cryptocell310]
         ead: [ead-none, ead-zeroconf]
-        exclude:
-          - edhoc_lib: rust
-            crypto: hacspec
 
     steps:
     - name: Checkout repo
@@ -66,19 +59,20 @@ jobs:
       run: sudo apt-get -y update && sudo apt-get -y install gcc-arm-none-eabi
 
     - name: Build
-      run: cargo build --package edhoc-rs --package edhoc-crypto --package edhoc-ead --no-default-features --features="${{ matrix.edhoc_lib }}-${{ matrix.crypto }}, ${{ matrix.ead }}" --release
+      run: cargo build --package edhoc-rs --package edhoc-crypto --package edhoc-ead --no-default-features --features="${{ matrix.crypto_backend }}, ${{ matrix.ead }}" --release
 
 
-  hacspec-to-fstar:
+  generate-fstar:
     needs: unit-tests
     runs-on: ubuntu-latest
+    if: >-
+      (github.event_name == 'workflow_dispatch') ||
+      (github.event_name == 'push' && startsWith(github.event.ref, 'refs/tags'))
+
     steps:
     - name: Checkout edhoc-rs
       uses: actions/checkout@v3
 
-    - name: Patch edhoc-rs features
-      run: git apply ./hacspec/adjust_features_for_hax.patch
-
     - name: Checkout hacspec-v2
       uses: actions/checkout@v3
       with:
@@ -89,9 +83,9 @@ jobs:
       run: docker build -f .docker/Dockerfile . -t hacspec-v2
       working-directory: hacspec-v2-repo
 
-    - name: Generate fstar
+    - name: Generate fstar code using the main library and the hacspec crypto backend
       run: |
-        docker run --rm -v ${{ github.workspace }}:/edhoc-rs hacspec-v2 bash -c "cd edhoc-rs/hacspec && cargo-hax -C -p edhoc-hacspec -p edhoc-crypto -p edhoc-consts -p edhoc-crypto-hacspec \; into fstar"
+        docker run --rm -v ${{ github.workspace }}:/edhoc-rs hacspec-v2 bash -c "cd edhoc-rs && cargo-hax -C -p edhoc-rs -p edhoc-crypto -p edhoc-ead --no-default-features --features='crypto-hacspec, ead-none' --release \; into -i '-c_wrapper::**' fstar"
         zip -j -r edhoc-rs-fstar.zip $(find . -name *fst)
 
     - name: Upload artifact
@@ -108,8 +102,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        edhoc_lib: [rust]
-        crypto: [psa-baremetal, cryptocell310]
+        crypto_backend: [crypto-psa-baremetal, crypto-cryptocell310]
 
     steps:
     - name: Checkout repo
@@ -121,7 +114,7 @@ jobs:
       run: sudo apt-get -y update && sudo apt-get -y install gcc-arm-none-eabi
 
     - name: Build static library, generate headers, and zip to file
-      run: ./build_for_c.sh "${{ matrix.edhoc_lib }}-${{ matrix.crypto }}"
+      run: ./build_for_c.sh "${{ matrix.crypto_backend }}"
 
     - name: Upload artifact
       uses: actions/upload-artifact@v3
@@ -137,7 +130,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        config: [hacspec-psa, rust-psa]
+        crypto_backend: [crypto-psa]
         ead: [ead-none, ead-zeroconf]
 
     steps:
@@ -152,7 +145,7 @@ jobs:
       run: sudo apt-get -y install qemu-system-arm
 
     - name: Run tests in QEMU
-      run: cd examples/edhoc-rs-no_std && cargo run --target="thumbv7m-none-eabi" --no-default-features --features="${{ matrix.config }}, ${{ matrix.ead }}" --release
+      run: cd examples/edhoc-rs-no_std && cargo run --target="thumbv7m-none-eabi" --no-default-features --features="${{ matrix.crypto_backend }}, ${{ matrix.ead }}" --release
 
 
   build-example-for-cortex-m4:
@@ -162,8 +155,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        edhoc_lib: [hacspec, rust]
-        crypto: [psa, cryptocell310]
+        crypto_backend: [crypto-psa, crypto-cryptocell310]
         ead: [ead-none, ead-zeroconf]
 
     steps:
@@ -176,7 +168,7 @@ jobs:
       run: sudo apt-get -y update && sudo apt-get -y install gcc-arm-none-eabi
 
     - name: Build example
-      run: cd examples/edhoc-rs-no_std && cargo build --target="thumbv7em-none-eabihf" --no-default-features --features="${{ matrix.edhoc_lib }}-${{ matrix.crypto }}, ${{ matrix.ead }}, rtt" --release
+      run: cd examples/edhoc-rs-no_std && cargo build --target="thumbv7em-none-eabihf" --no-default-features --features="${{ matrix.crypto_backend }}, ${{ matrix.ead }}, rtt" --release
 
 
   build-coap-example:
@@ -196,10 +188,11 @@ jobs:
 
   release:
     runs-on: ubuntu-latest
-    needs: [build-edhoc-package, run-example-on-qemu, build-example-for-cortex-m4, build-coap-example, hacspec-to-fstar, build-static-lib-and-headers]
+    needs: [build-edhoc-package, run-example-on-qemu, build-example-for-cortex-m4, build-coap-example, generate-fstar, build-static-lib-and-headers]
     if: >-
       github.event_name == 'push' &&
       startsWith(github.event.ref, 'refs/tags')
+
     steps:
       - name: Checkout repo
         uses: actions/checkout@v3

Cargo.toml

@@ -2,7 +2,6 @@
 
 members = [
   "lib",
-  "hacspec",
   "ead",
   "ead/edhoc-ead-none",
   "ead/edhoc-ead-zeroconf",
@@ -20,7 +19,6 @@ members = [
 # tested on the host architecture
 default-members = [
   "lib",
-  "hacspec",
   "ead",
   "crypto",
   "crypto/edhoc-crypto-hacspec",

README.md

@@ -46,7 +46,7 @@ cd ./examples/edhoc-rs-no_std
 cargo build --target="thumbv7em-none-eabihf" --no-default-features --features="hacspec-psa, rtt" --release
 
 # build using the rust version of the lib, and hardware-accelerated crypto
-cargo build --target="thumbv7em-none-eabihf" --no-default-features --features="rust-cryptocell310, rtt"
+cargo build --target="thumbv7em-none-eabihf" --no-default-features --features="crypto-cryptocell310, rtt"
 ```
 
 To build **and** flash to the board, replace the word `build` with `embed` in the commands above (you may need to `cargo install cargo-embed`).

build_for_c.sh

@@ -11,9 +11,9 @@
 
 cargo_features=$1
 
-if [[ $cargo_features != "rust-cryptocell310" && $cargo_features != "rust-psa-baremetal" ]]; then
-    echo "Select one of: rust-cryptocell310, rust-psa-baremetal"
-    echo "Example: ./build_static_lib.sh rust-cryptocell310"
+if [[ $cargo_features != "crypto-cryptocell310" && $cargo_features != "crypto-psa-baremetal" ]]; then
+    echo "Select one of: crypto-cryptocell310, crypto-psa-baremetal"
+    echo "Example: ./build_static_lib.sh crypto-cryptocell310"
     exit 1
 fi
 

consts/Cargo.toml

@@ -6,13 +6,5 @@ authors = ["Mališa Vučinić <[email protected]>"]
 license = "BSD"
 description = "EDHOC crypto library constants crate"
 
-[dependencies]
-hacspec-lib = { version = "0.1.0-beta.1", default-features = false, optional = true }
-
 [build-dependencies]
 cbindgen = "0.24.5"
-
-[features]
-default = [ ]
-hacspec = [ "hacspec-lib/alloc" ]
-rust = [ ]